|
problem.path
|
|
|
problem.expected_res
|
unknown
|
|
res
|
sat
|
|
rtime
|
2.3s
|
|
stime
|
0.000s
|
|
utime
|
0.000s
|
|
errcode
|
10
|
WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 39598 | | Number of clauses: 193434 | | Parse time: 0.13 s | | Eliminated vars: 17979 | | Vars set : 7096 | | Eliminated clauses: 0.92 Mb | | Simplification time: 0.45 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 14517 104976 346898 | 38491 95 26 | 17.935 % | | 250 | 14514 104976 346898 | 42340 242 20 | 17.943 % | | 475 | 14514 104976 346898 | 46574 467 17 | 17.943 % | | 812 | 14407 103434 342027 | 51231 777 20 | 18.213 % | | 1318 | 14407 103434 342027 | 56354 1283 32 | 18.213 % | | 2077 | 14351 103015 340663 | 61990 2031 33 | 18.354 % | | 3216 | 14351 102829 339905 | 68189 3169 39 | 18.354 % | | 4924 | 14286 102388 338298 | 75008 4864 37 | 18.519 % | =============================================================================== restarts : 31 conflicts : 6831 (3240 /sec) decisions : 20397 (0.00 % random) (9675 /sec) propagations : 6661610 (3159888 /sec) conflict literals : 249834 (43.39 % deleted) Memory used : 33.87 MB CPU time : 2.10818 s SATISFIABLE
|
prover.name
|
minisat
|
|
prover.cmd
|
<unknown>
|
|
prover.version
|
<unknown>
|
|
prover.sat
|
^SATISFIABLE
|
|
prover.unsat
|
^UNSATISFIABLE
|
|
prover.unknown
|
INDETERMINATE
|
|
prover.timeout
|
<none>
|
|
prover.memory
|
<none>
|