Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl15_20_pb.cnf.cr.opb
MD5SUMce39bf71367df072c91f9b7587480c93
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 21
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.017996
Number of variables600
Total number of constraints70
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint15
Maximum length of a constraint20

Trace number 6084 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-14 03:21:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4518 boxname=wulflinc30 idbench=6 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ce39bf71367df072c91f9b7587480c93  /oldhome/oroussel/tmp/wulflinc30/normalized-chnl15_20_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc30/normalized-chnl15_20_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc30/normalized-chnl15_20_pb.cnf.cr.opb
IDLAUNCH: 4518
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        720472 kB
Buffers:         38244 kB
Cached:         235388 kB
SwapCached:          0 kB
Active:          84324 kB
Inactive:       192144 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        720220 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32196 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:41:11 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 4518 7 1200.16 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 70 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4900    14040 |    1633       0        0     nan |  0.000 % |
c |       100 |    4835    13845 |    1796      80     3771    47.1 |  2.516 % |
c |       250 |    4775    13665 |    1975     207    11184    54.0 |  3.216 % |
c |       478 |    4755    13605 |    2173     426    23687    55.6 |  3.450 % |
c |       815 |    4685    13395 |    2390     730    42860    58.7 |  4.327 % |
c |      1323 |    4675    13365 |    2629    1225    96257    78.6 |  4.386 % |
c |      2084 |    4635    13245 |    2892    1969   181261    92.1 |  4.854 % |
c |      3224 |    4630    13230 |    3182    3108   308324    99.2 |  4.912 % |
c |      4936 |    4625    13215 |    3500    3114   337841   108.5 |  4.971 % |
c |      7498 |    4577    13075 |    3850    1955   200193   102.4 |  5.556 % |
c |     11343 |    4557    13015 |    4235    3611   415129   115.0 |  5.790 % |
c |     17110 |    4527    12925 |    4659    2495   268702   107.7 |  6.140 % |
c |     25761 |    4435    12655 |    5125    3400   348800   102.6 |  7.251 % |
c |     38736 |    4380    12490 |    5637    5241   535365   102.1 |  7.895 % |
c |     58198 |    4285    12205 |    6201    3652   380665   104.2 |  9.006 % |
c |     87391 |    3982    11300 |    6821    5962   753102   126.3 | 12.573 % |
c |    131180 |    3757    10625 |    7503    5564   601200   108.1 | 15.205 % |
c |    196865 |    3493     9835 |    8253    6297   671946   106.7 | 18.304 % |
c |    295391 |    3083     8605 |    9079    6972   682719    97.9 | 23.099 % |
c |    443183 |    2719     7525 |    9987    7729   839792   108.7 | 27.427 % |
c |    664869 |    2450     6720 |   10986    9036   794435    87.9 | 30.585 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 18758
Raw data (stat): 18758 (runsolver) R 18757 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481306076 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.92 0.95 0.90 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1096 0 0 0 996 2 0 0 25 0 1 0 481306076 5992448 1074 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1463 1074 603 41 0 1422 0
vsize: 5852
[startup+20.0013 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1194 0 0 0 1995 3 0 0 25 0 1 0 481306076 6402048 1172 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1563 1172 603 41 0 1522 0
vsize: 6252
[startup+30.0025 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1332 0 0 0 2994 4 0 0 25 0 1 0 481306076 7094272 1310 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1732 1310 603 41 0 1691 0
vsize: 6928
[startup+40.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1413 0 0 0 3993 5 0 0 25 0 1 0 481306076 7372800 1391 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1800 1391 603 41 0 1759 0
vsize: 7200
[startup+50.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1455 0 0 0 4993 5 0 0 25 0 1 0 481306076 7520256 1433 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1836 1433 603 41 0 1795 0
vsize: 7344
[startup+60.0029 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1503 0 0 0 5993 6 0 0 25 0 1 0 481306076 7794688 1481 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1903 1481 603 41 0 1862 0
vsize: 7612
[startup+70.0037 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1556 0 0 0 6993 6 0 0 25 0 1 0 481306076 7925760 1534 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1935 1534 603 41 0 1894 0
vsize: 7740
[startup+80.0041 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1583 0 0 0 7992 7 0 0 25 0 1 0 481306076 8069120 1561 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1970 1561 603 41 0 1929 0
vsize: 7880
[startup+90.0043 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1586 0 0 0 8992 7 0 0 25 0 1 0 481306076 8069120 1564 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1970 1564 603 41 0 1929 0
vsize: 7880
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1617 0 0 0 9991 8 0 0 25 0 1 0 481306076 8212480 1595 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2005 1595 603 41 0 1964 0
vsize: 8020
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1693 0 0 0 10991 8 0 0 25 0 1 0 481306076 8630272 1671 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2107 1671 603 41 0 2066 0
vsize: 8428
[startup+120.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1755 0 0 0 11991 9 0 0 25 0 1 0 481306076 8921088 1733 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2178 1733 603 41 0 2137 0
vsize: 8712
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1865 0 0 0 12990 10 0 0 25 0 1 0 481306076 9326592 1843 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2277 1843 603 41 0 2236 0
vsize: 9108
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 1993 0 0 0 13989 10 0 0 25 0 1 0 481306076 9867264 1971 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2409 1971 603 41 0 2368 0
vsize: 9636
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2048 0 0 0 14989 11 0 0 25 0 1 0 481306076 10149888 2026 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2478 2026 603 41 0 2437 0
vsize: 9912
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2104 0 0 0 15989 11 0 0 25 0 1 0 481306076 10285056 2082 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2511 2082 603 41 0 2470 0
vsize: 10044
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2148 0 0 0 16989 12 0 0 25 0 1 0 481306076 10575872 2126 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2582 2126 603 41 0 2541 0
vsize: 10328
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2158 0 0 0 17989 12 0 0 25 0 1 0 481306076 10575872 2136 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2582 2136 603 41 0 2541 0
vsize: 10328
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2162 0 0 0 18989 12 0 0 25 0 1 0 481306076 10575872 2140 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2582 2140 603 41 0 2541 0
vsize: 10328
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2169 0 0 0 19988 12 0 0 25 0 1 0 481306076 10575872 2147 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2582 2147 603 41 0 2541 0
vsize: 10328
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2177 0 0 0 20988 12 0 0 25 0 1 0 481306076 10719232 2155 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2617 2155 603 41 0 2576 0
vsize: 10468
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2177 0 0 0 21988 13 0 0 25 0 1 0 481306076 10719232 2155 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2617 2155 603 41 0 2576 0
vsize: 10468
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2178 0 0 0 22988 13 0 0 25 0 1 0 481306076 10719232 2156 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2617 2156 603 41 0 2576 0
vsize: 10468
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2203 0 0 0 23988 13 0 0 25 0 1 0 481306076 10719232 2181 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2617 2181 603 41 0 2576 0
vsize: 10468
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2276 0 0 0 24987 14 0 0 25 0 1 0 481306076 11124736 2254 4294967295 134512640 134672761 3221224544 3221223648 134554721 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2716 2254 603 41 0 2675 0
vsize: 10864
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2286 0 0 0 25986 15 0 0 25 0 1 0 481306076 11124736 2264 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2716 2264 603 41 0 2675 0
vsize: 10864
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2308 0 0 0 26986 15 0 0 25 0 1 0 481306076 11264000 2286 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2750 2286 603 41 0 2709 0
vsize: 11000
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2313 0 0 0 27986 15 0 0 25 0 1 0 481306076 11264000 2291 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2750 2291 603 41 0 2709 0
vsize: 11000
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2360 0 0 0 28986 16 0 0 25 0 1 0 481306076 11558912 2338 4294967295 134512640 134672761 3221224544 3221223728 134559559 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2822 2338 603 41 0 2781 0
vsize: 11288
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2360 0 0 0 29986 16 0 0 25 0 1 0 481306076 11558912 2338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2822 2338 603 41 0 2781 0
vsize: 11288
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2360 0 0 0 30986 16 0 0 25 0 1 0 481306076 11558912 2338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2822 2338 603 41 0 2781 0
vsize: 11288
[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2371 0 0 0 31986 17 0 0 25 0 1 0 481306076 11558912 2349 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2822 2349 603 41 0 2781 0
vsize: 11288
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2388 0 0 0 32985 17 0 0 25 0 1 0 481306076 11694080 2366 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2855 2366 603 41 0 2814 0
vsize: 11420
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2394 0 0 0 33985 17 0 0 25 0 1 0 481306076 11694080 2372 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2855 2372 603 41 0 2814 0
vsize: 11420
[startup+350.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2397 0 0 0 34985 17 0 0 25 0 1 0 481306076 11694080 2375 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2855 2375 603 41 0 2814 0
vsize: 11420
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2420 0 0 0 35985 18 0 0 25 0 1 0 481306076 11829248 2398 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2888 2398 603 41 0 2847 0
vsize: 11552
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2490 0 0 0 36985 18 0 0 25 0 1 0 481306076 12099584 2468 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2954 2468 603 41 0 2913 0
vsize: 11816
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2538 0 0 0 37985 18 0 0 25 0 1 0 481306076 12365824 2516 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3019 2516 603 41 0 2978 0
vsize: 12076
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2569 0 0 0 38984 19 0 0 25 0 1 0 481306076 12509184 2547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2547 603 41 0 3013 0
vsize: 12216
[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2596 0 0 0 39984 19 0 0 25 0 1 0 481306076 12673024 2574 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3094 2574 603 41 0 3053 0
vsize: 12376
[startup+410.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2619 0 0 0 40984 19 0 0 25 0 1 0 481306076 12673024 2597 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3094 2597 603 41 0 3053 0
vsize: 12376
[startup+420.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2626 0 0 0 41984 20 0 0 25 0 1 0 481306076 12836864 2604 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2604 603 41 0 3093 0
vsize: 12536
[startup+430.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2627 0 0 0 42984 20 0 0 25 0 1 0 481306076 12836864 2605 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2605 603 41 0 3093 0
vsize: 12536
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2641 0 0 0 43984 20 0 0 25 0 1 0 481306076 12836864 2619 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2619 603 41 0 3093 0
vsize: 12536
[startup+450.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2646 0 0 0 44984 20 0 0 25 0 1 0 481306076 12836864 2624 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2624 603 41 0 3093 0
vsize: 12536
[startup+460.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2669 0 0 0 45984 21 0 0 25 0 1 0 481306076 13000704 2647 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3174 2647 603 41 0 3133 0
vsize: 12696
[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2671 0 0 0 46984 21 0 0 25 0 1 0 481306076 13000704 2649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3174 2649 603 41 0 3133 0
vsize: 12696
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2672 0 0 0 47983 21 0 0 25 0 1 0 481306076 13000704 2650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3174 2650 603 41 0 3133 0
vsize: 12696
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2673 0 0 0 48983 22 0 0 25 0 1 0 481306076 13000704 2651 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3174 2651 603 41 0 3133 0
vsize: 12696
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2674 0 0 0 49983 22 0 0 25 0 1 0 481306076 13000704 2652 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3174 2652 603 41 0 3133 0
vsize: 12696
[startup+510.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2674 0 0 0 50982 23 0 0 25 0 1 0 481306076 13000704 2652 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3174 2652 603 41 0 3133 0
vsize: 12696
[startup+520.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2680 0 0 0 51982 23 0 0 25 0 1 0 481306076 13000704 2658 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3174 2658 603 41 0 3133 0
vsize: 12696
[startup+530.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2691 0 0 0 52982 24 0 0 25 0 1 0 481306076 13164544 2669 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3214 2669 603 41 0 3173 0
vsize: 12856
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2691 0 0 0 53982 24 0 0 25 0 1 0 481306076 13164544 2669 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3214 2669 603 41 0 3173 0
vsize: 12856
[startup+550.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2696 0 0 0 54981 24 0 0 25 0 1 0 481306076 13164544 2674 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3214 2674 603 41 0 3173 0
vsize: 12856
[startup+560.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2719 0 0 0 55981 25 0 0 25 0 1 0 481306076 13312000 2697 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3250 2697 603 41 0 3209 0
vsize: 13000
[startup+570.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2727 0 0 0 56981 25 0 0 25 0 1 0 481306076 13312000 2705 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3250 2705 603 41 0 3209 0
vsize: 13000
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2842 0 0 0 57980 25 0 0 25 0 1 0 481306076 13717504 2820 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3349 2820 603 41 0 3308 0
vsize: 13396
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2868 0 0 0 58980 26 0 0 25 0 1 0 481306076 13873152 2846 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3387 2846 603 41 0 3346 0
vsize: 13548
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2872 0 0 0 59980 26 0 0 25 0 1 0 481306076 13873152 2850 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3387 2850 603 41 0 3346 0
vsize: 13548
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2902 0 0 0 60980 26 0 0 25 0 1 0 481306076 14012416 2880 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3421 2880 603 41 0 3380 0
vsize: 13684
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2903 0 0 0 61980 27 0 0 25 0 1 0 481306076 14012416 2881 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3421 2881 603 41 0 3380 0
vsize: 13684
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2909 0 0 0 62980 27 0 0 25 0 1 0 481306076 14176256 2887 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 2887 603 41 0 3420 0
vsize: 13844
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2911 0 0 0 63979 27 0 0 25 0 1 0 481306076 14176256 2889 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 2889 603 41 0 3420 0
vsize: 13844
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2912 0 0 0 64979 27 0 0 25 0 1 0 481306076 14176256 2890 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 2890 603 41 0 3420 0
vsize: 13844
[startup+660.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2912 0 0 0 65979 28 0 0 25 0 1 0 481306076 14176256 2890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 2890 603 41 0 3420 0
vsize: 13844
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2925 0 0 0 66979 28 0 0 25 0 1 0 481306076 14176256 2903 4294967295 134512640 134672761 3221224544 3221223728 134558433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 2903 603 41 0 3420 0
vsize: 13844
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 2962 0 0 0 67979 28 0 0 25 0 1 0 481306076 14340096 2940 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3501 2940 603 41 0 3460 0
vsize: 14004
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3063 0 0 0 68979 29 0 0 25 0 1 0 481306076 14757888 3041 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3603 3041 603 41 0 3562 0
vsize: 14412
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3067 0 0 0 69978 29 0 0 25 0 1 0 481306076 14757888 3045 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3603 3045 603 41 0 3562 0
vsize: 14412
[startup+710.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3067 0 0 0 70978 30 0 0 25 0 1 0 481306076 14757888 3045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3603 3045 603 41 0 3562 0
vsize: 14412
[startup+720.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3067 0 0 0 71978 30 0 0 25 0 1 0 481306076 14757888 3045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3603 3045 603 41 0 3562 0
vsize: 14412
[startup+730.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3067 0 0 0 72978 30 0 0 25 0 1 0 481306076 14757888 3045 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3603 3045 603 41 0 3562 0
vsize: 14412
[startup+740.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3067 0 0 0 73977 31 0 0 25 0 1 0 481306076 14757888 3045 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3603 3045 603 41 0 3562 0
vsize: 14412
[startup+750.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3079 0 0 0 74977 31 0 0 25 0 1 0 481306076 14917632 3057 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3642 3057 603 41 0 3601 0
vsize: 14568
[startup+760.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3088 0 0 0 75977 31 0 0 25 0 1 0 481306076 14917632 3066 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3642 3066 603 41 0 3601 0
vsize: 14568
[startup+770.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3091 0 0 0 76977 32 0 0 25 0 1 0 481306076 14917632 3069 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3642 3069 603 41 0 3601 0
vsize: 14568
[startup+780.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3091 0 0 0 77977 32 0 0 25 0 1 0 481306076 14917632 3069 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3642 3069 603 41 0 3601 0
vsize: 14568
[startup+790.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3181 0 0 0 78977 32 0 0 25 0 1 0 481306076 15319040 3159 4294967295 134512640 134672761 3221224544 3221223776 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3740 3159 603 41 0 3699 0
vsize: 14960
[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3193 0 0 0 79976 33 0 0 25 0 1 0 481306076 15319040 3171 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3740 3171 603 41 0 3699 0
vsize: 14960
[startup+810.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3213 0 0 0 80976 33 0 0 25 0 1 0 481306076 15454208 3191 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3773 3191 603 41 0 3732 0
vsize: 15092
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3224 0 0 0 81976 33 0 0 25 0 1 0 481306076 15454208 3202 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3773 3202 603 41 0 3732 0
vsize: 15092
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3226 0 0 0 82976 33 0 0 25 0 1 0 481306076 15454208 3204 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3773 3204 603 41 0 3732 0
vsize: 15092
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3238 0 0 0 83976 33 0 0 25 0 1 0 481306076 15609856 3216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3216 603 41 0 3770 0
vsize: 15244
[startup+850.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3243 0 0 0 84976 33 0 0 25 0 1 0 481306076 15609856 3221 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3221 603 41 0 3770 0
vsize: 15244
[startup+860.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3264 0 0 0 85976 33 0 0 25 0 1 0 481306076 15609856 3242 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3242 603 41 0 3770 0
vsize: 15244
[startup+870.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3277 0 0 0 86977 33 0 0 25 0 1 0 481306076 15773696 3255 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3851 3255 603 41 0 3810 0
vsize: 15404
[startup+880.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3299 0 0 0 87977 34 0 0 25 0 1 0 481306076 15937536 3277 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3891 3277 603 41 0 3850 0
vsize: 15564
[startup+890.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3308 0 0 0 88977 34 0 0 25 0 1 0 481306076 15937536 3286 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3891 3286 603 41 0 3850 0
vsize: 15564
[startup+900.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3316 0 0 0 89977 34 0 0 25 0 1 0 481306076 15937536 3294 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3891 3294 603 41 0 3850 0
vsize: 15564
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3333 0 0 0 90977 34 0 0 25 0 1 0 481306076 16101376 3311 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3311 603 41 0 3890 0
vsize: 15724
[startup+920.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3333 0 0 0 91977 34 0 0 25 0 1 0 481306076 16101376 3311 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3311 603 41 0 3890 0
vsize: 15724
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3333 0 0 0 92977 34 0 0 25 0 1 0 481306076 16101376 3311 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3311 603 41 0 3890 0
vsize: 15724
[startup+940.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3339 0 0 0 93977 34 0 0 25 0 1 0 481306076 16101376 3317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3317 603 41 0 3890 0
vsize: 15724
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3445 0 0 0 94977 34 0 0 25 0 1 0 481306076 16506880 3423 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4030 3423 603 41 0 3989 0
vsize: 16120
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3486 0 0 0 95978 34 0 0 25 0 1 0 481306076 16642048 3464 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4063 3464 603 41 0 4022 0
vsize: 16252
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3535 0 0 0 96978 34 0 0 25 0 1 0 481306076 16936960 3513 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4135 3513 603 41 0 4094 0
vsize: 16540
[startup+980.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3557 0 0 0 97978 34 0 0 25 0 1 0 481306076 16936960 3535 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4135 3535 603 41 0 4094 0
vsize: 16540
[startup+990.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3587 0 0 0 98978 34 0 0 25 0 1 0 481306076 17100800 3565 4294967295 134512640 134672761 3221224544 3221223648 134555214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3565 603 41 0 4134 0
vsize: 16700
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3596 0 0 0 99978 34 0 0 25 0 1 0 481306076 17100800 3574 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3574 603 41 0 4134 0
vsize: 16700
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3596 0 0 0 100978 34 0 0 25 0 1 0 481306076 17100800 3574 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3574 603 41 0 4134 0
vsize: 16700
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3596 0 0 0 101978 35 0 0 25 0 1 0 481306076 17100800 3574 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3574 603 41 0 4134 0
vsize: 16700
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3596 0 0 0 102978 35 0 0 25 0 1 0 481306076 17100800 3574 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3574 603 41 0 4134 0
vsize: 16700
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3596 0 0 0 103978 35 0 0 25 0 1 0 481306076 17100800 3574 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3574 603 41 0 4134 0
vsize: 16700
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3608 0 0 0 104978 35 0 0 25 0 1 0 481306076 17264640 3586 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3586 603 41 0 4174 0
vsize: 16860
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3608 0 0 0 105978 35 0 0 25 0 1 0 481306076 17264640 3586 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3586 603 41 0 4174 0
vsize: 16860
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3608 0 0 0 106978 35 0 0 25 0 1 0 481306076 17264640 3586 4294967295 134512640 134672761 3221224544 3221223688 134565969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3586 603 41 0 4174 0
vsize: 16860
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3609 0 0 0 107977 35 0 0 25 0 1 0 481306076 17264640 3587 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3587 603 41 0 4174 0
vsize: 16860
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3609 0 0 0 108978 35 0 0 25 0 1 0 481306076 17264640 3587 4294967295 134512640 134672761 3221224544 3221223728 134559540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3587 603 41 0 4174 0
vsize: 16860
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3609 0 0 0 109978 35 0 0 25 0 1 0 481306076 17264640 3587 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3587 603 41 0 4174 0
vsize: 16860
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3634 0 0 0 110978 35 0 0 25 0 1 0 481306076 17264640 3612 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3612 603 41 0 4174 0
vsize: 16860
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3647 0 0 0 111978 35 0 0 25 0 1 0 481306076 17428480 3625 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4255 3625 603 41 0 4214 0
vsize: 17020
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3699 0 0 0 112978 35 0 0 25 0 1 0 481306076 17592320 3677 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4295 3677 603 41 0 4254 0
vsize: 17180
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3699 0 0 0 113978 35 0 0 25 0 1 0 481306076 17592320 3677 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4295 3677 603 41 0 4254 0
vsize: 17180
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3705 0 0 0 114978 35 0 0 25 0 1 0 481306076 17592320 3683 4294967295 134512640 134672761 3221224544 3221223500 1075350254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4295 3683 603 41 0 4254 0
vsize: 17180
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3717 0 0 0 115978 35 0 0 25 0 1 0 481306076 17756160 3695 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4335 3695 603 41 0 4294 0
vsize: 17340
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3724 0 0 0 116978 35 0 0 25 0 1 0 481306076 17756160 3702 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4335 3702 603 41 0 4294 0
vsize: 17340
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3735 0 0 0 117978 36 0 0 25 0 1 0 481306076 17756160 3713 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4335 3713 603 41 0 4294 0
vsize: 17340
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3737 0 0 0 118978 36 0 0 25 0 1 0 481306076 17756160 3715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4335 3715 603 41 0 4294 0
vsize: 17340
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18758
Raw data (stat): 18758 (minisat+) R 18757 11931 11930 0 -1 0 3737 0 0 0 119978 36 0 0 25 0 1 0 481306076 17756160 3715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4335 3715 603 41 0 4294 0
vsize: 17340
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 18758
Raw data (stat): 18758 (minisat+) Z 18757 11931 11930 0 -1 12 3739 0 0 0 119978 37 0 0 25 0 1 0 481306076 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.05
CPU time (s): 1200.16
CPU user time (s): 1199.79
CPU system time (s): 0.370943
CPU usage (%): 100.009
Max. virtual memory (Kb): 17340
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####