|
problem.path
|
|
|
problem.expected_res
|
unknown
|
|
res
|
sat
|
|
rtime
|
0.035s
|
|
stime
|
0.000s
|
|
utime
|
0.000s
|
|
errcode
|
10
|
WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 718 | | Number of clauses: 4806 | | Parse time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 541 3912 9674 | 1434 100 10 | 24.653 % | | 250 | 529 3800 9399 | 1577 247 9 | 26.323 % | | 475 | 528 3790 9375 | 1735 471 11 | 26.463 % | | 812 | 511 3625 8970 | 1909 776 10 | 28.830 % | | 1318 | 511 3625 8970 | 2100 1282 11 | 28.830 % | | 2077 | 510 3606 8929 | 2310 2039 11 | 28.970 % | =============================================================================== restarts : 15 conflicts : 2659 (88850 /sec) decisions : 4455 (0.00 % random) (148862 /sec) propagations : 191028 (6383132 /sec) conflict literals : 28722 (30.99 % deleted) Memory used : 11.00 MB CPU time : 0.029927 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>
|