|
problem.path
|
|
|
problem.expected_res
|
unknown
|
|
res
|
sat
|
|
rtime
|
0.488s
|
|
stime
|
0.000s
|
|
utime
|
0.000s
|
|
errcode
|
10
|
WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 1931 | | Number of clauses: 14103 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 1463 12063 29804 | 4423 95 12 | 24.236 % | | 250 | 1435 12063 29804 | 4865 243 10 | 25.686 % | | 475 | 1435 11410 28203 | 5351 457 11 | 25.686 % | | 812 | 1435 11410 28203 | 5887 794 10 | 25.686 % | | 1318 | 1434 11400 28179 | 6475 1299 11 | 25.738 % | | 2077 | 1414 11241 27789 | 7123 2041 12 | 26.774 % | | 3216 | 1413 11196 27675 | 7835 3176 12 | 26.826 % | | 4924 | 1395 11016 27227 | 8619 4822 13 | 27.758 % | | 7486 | 1378 10792 26699 | 9481 7276 15 | 28.638 % | | 11330 | 1366 10646 26341 | 10429 6024 17 | 29.259 % | | 17096 | 1357 10553 26109 | 11472 6116 14 | 29.726 % | | 25745 | 1353 10480 25934 | 12619 8281 13 | 29.933 % | =============================================================================== restarts : 115 conflicts : 31111 (65948 /sec) decisions : 58869 (0.00 % random) (124787 /sec) propagations : 2342107 (4964679 /sec) conflict literals : 489336 (27.31 % deleted) Memory used : 12.00 MB CPU time : 0.471754 s SATISFIABLE
|
prover.name
|
minisat
|
|
prover.cmd
|
<unknown>
|
|
prover.version
|
<unknown>
|
|
prover.sat
|
^SATISFIABLE
|
|
prover.unsat
|
UNSATISFIABLE
|
|
prover.unknown
|
<none>
|
|
prover.timeout
|
<none>
|
|
prover.memory
|
<none>
|