problem.path
|
|
problem.expected_res
|
unknown
|
res
|
unsat
|
rtime
|
1.3s
|
stime
|
0.000s
|
utime
|
0.000s
|
errcode
|
20
|
WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 37452 | | Number of clauses: 110919 | | Parse time: 0.07 s | | Eliminated vars: 30453 | | Vars set : 55 | | Eliminated clauses: 1.39 Mb | | Simplification time: 0.28 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6944 43540 174283 | 15964 100 12 | 0.147 % | | 250 | 6895 43540 174283 | 17561 248 13 | 0.278 % | | 475 | 6895 43540 174283 | 19317 473 20 | 0.278 % | | 812 | 6868 43540 174283 | 21248 808 18 | 0.350 % | | 1318 | 6868 42750 171487 | 23373 1299 19 | 0.350 % | | 2077 | 6868 42750 171487 | 25711 2058 17 | 0.350 % | | 3216 | 6868 42750 171487 | 28282 3197 18 | 0.350 % | | 4924 | 6868 42750 171487 | 31110 4905 18 | 0.350 % | | 7486 | 6311 36576 149111 | 34221 7184 19 | 1.837 % | | 11330 | 6311 36576 149111 | 37643 11028 19 | 1.837 % | =============================================================================== restarts : 62 conflicts : 15473 (15138 /sec) decisions : 40301 (0.00 % random) (39429 /sec) propagations : 1767068 (1728835 /sec) conflict literals : 284911 (38.38 % deleted) Memory used : 26.39 MB CPU time : 1.02212 s UNSATISFIABLE
prover.name
|
minisat
|
prover.cmd
|
<unknown>
|
prover.version
|
<unknown>
|
prover.sat
|
^SATISFIABLE
|
prover.unsat
|
^UNSATISFIABLE
|
prover.unknown
|
INDETERMINATE
|
prover.timeout
|
<none>
|
prover.memory
|
<none>
|