|
problem.path
|
|
|
problem.expected_res
|
unknown
|
|
res
|
unsat
|
|
rtime
|
1.5s
|
|
stime
|
0.000s
|
|
utime
|
0.000s
|
|
errcode
|
20
|
WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 37002 | | Number of clauses: 109569 | | Parse time: 0.06 s | | Eliminated vars: 30017 | | Vars set : 56 | | Eliminated clauses: 1.37 Mb | | Simplification time: 0.28 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 6929 43348 173672 | 15894 100 14 | 0.151 % | | 250 | 6929 43348 173672 | 17483 250 16 | 0.151 % | | 475 | 6929 43348 173672 | 19232 475 20 | 0.151 % | | 812 | 6892 43348 173672 | 21155 811 22 | 0.251 % | | 1318 | 6846 43348 173672 | 23270 1316 20 | 0.376 % | | 2077 | 6846 42558 170947 | 25597 2075 20 | 0.376 % | | 3216 | 6846 42558 170947 | 28157 3214 19 | 0.376 % | | 4924 | 6419 42529 170876 | 30973 4920 19 | 1.530 % | | 7486 | 6291 36342 148573 | 34070 7276 21 | 1.876 % | | 11330 | 6290 36339 148565 | 37477 11118 21 | 1.878 % | | 17096 | 6064 36325 148519 | 41225 16861 21 | 2.489 % | =============================================================================== restarts : 63 conflicts : 19073 (15101 /sec) decisions : 44185 (0.00 % random) (34983 /sec) propagations : 2097013 (1660299 /sec) conflict literals : 381765 (39.68 % deleted) Memory used : 26.01 MB CPU time : 1.26303 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>
|