PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl15_25_pb.cnf.cr.opb
MD5SUM	808390b13d2d87ec4e78f628ed3af9ba
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(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	26
Number of bits of the biggest sum of numbers	5
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.021995
Number of variables	750
Total number of constraints	80
Number of constraints which are clauses	50
Number of constraints which are cardinality constraints (but not clauses)	30
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	15
Maximum length of a constraint	25
Trace number 5705

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-14 01:30:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4143 boxname=wulflinc9 idbench=7 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  808390b13d2d87ec4e78f628ed3af9ba  /oldhome/oroussel/tmp/wulflinc9/normalized-chnl15_25_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc9/normalized-chnl15_25_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc9/normalized-chnl15_25_pb.cnf.cr.opb
IDLAUNCH: 4143
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        893920 kB
Buffers:         36188 kB
Cached:          84424 kB
SwapCached:        564 kB
Active:          53392 kB
Inactive:        70576 kB
HighTotal:      131008 kB
HighFree:        42672 kB
LowTotal:       903652 kB
LowFree:        851248 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11136 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:50:51 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 4143 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  29]---> BDD-cost:   47
c ---[  28]---> BDD-cost:   47
c ---[  27]---> BDD-cost:   47
c ---[  26]---> BDD-cost:   47
c ---[  25]---> BDD-cost:   47
c ---[  24]---> BDD-cost:   47
c ---[  23]---> BDD-cost:   47
c ---[  22]---> BDD-cost:   47
c ---[  21]---> BDD-cost:   47
c ---[  20]---> BDD-cost:   47
c ---[  19]---> BDD-cost:   47
c ---[  18]---> BDD-cost:   47
c ---[  17]---> BDD-cost:   47
c ---[  16]---> BDD-cost:   47
c ---[  15]---> BDD-cost:   47
c ---[  14]---> BDD-cost:   47
c ---[  13]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   47
c ---[  11]---> BDD-cost:   47
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   7]---> BDD-cost:   47
c ---[   6]---> BDD-cost:   47
c ---[   5]---> BDD-cost:   47
c ---[   4]---> BDD-cost:   47
c ---[   3]---> BDD-cost:   47
c ---[   2]---> BDD-cost:   47
c ---[   1]---> BDD-cost:   47
c ---[   0]---> BDD-cost:   47
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3530     9810 |    1176       0        0     nan |  0.000 % |
c |       103 |    3530     9810 |    1293     103     5007    48.6 |  1.389 % |
c |       253 |    3530     9810 |    1422     253    13026    51.5 |  1.389 % |
c |       478 |    3530     9810 |    1565     478    27883    58.3 |  1.390 % |
c |       818 |    3530     9810 |    1721     818    54244    66.3 |  1.389 % |
c |      1324 |    3530     9810 |    1893    1324    89008    67.2 |  1.389 % |
c |      2084 |    3530     9810 |    2083    2084   154915    74.3 |  1.389 % |
c |      3224 |    3530     9810 |    2291    1835   146216    79.7 |  1.389 % |
c |      4932 |    3530     9810 |    2520    2209   220568    99.8 |  1.389 % |
c |      7494 |    3530     9810 |    2772    1902   214616   112.8 |  1.389 % |
c |     11338 |    3530     9810 |    3050    2643   352193   133.3 |  1.389 % |
c |     17107 |    3530     9810 |    3355    3014   336789   111.7 |  1.389 % |
c |     25756 |    3530     9810 |    3690    2249   281918   125.4 |  1.389 % |
c |     38731 |    3530     9810 |    4059    2796   359962   128.7 |  1.389 % |
c |     58192 |    3530     9810 |    4465    2453   289039   117.8 |  1.389 % |
c |     87386 |    3530     9810 |    4912    2518   277999   110.4 |  1.389 % |
c |    131177 |    3530     9810 |    5403    3570   478640   134.1 |  1.389 % |
c |    196861 |    3530     9810 |    5944    4748   630300   132.8 |  1.389 % |
c |    295392 |    3530     9810 |    6538    4647   519495   111.8 |  1.389 % |
c |    443181 |    3530     9810 |    7192    6344   768707   121.2 |  1.389 % |
c |    664866 |    3530     9810 |    7911    7564   930517   123.0 |  1.389 % |
c |    997394 |    3530     9810 |    8702    5038   677958   134.6 |  1.389 % |
#### 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.93 0.98 0.91 2/54 2688
Raw data (stat): 2688 (runsolver) R 2687 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422425295 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.0011 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1059 0 0 0 995 3 0 0 25 0 1 0 422425295 5955584 1037 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1454 1037 603 41 0 1413 0
vsize: 5816
[startup+20.0013 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1203 0 0 0 1995 3 0 0 25 0 1 0 422425295 6483968 1181 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1583 1181 603 41 0 1542 0
vsize: 6332
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1349 0 0 0 2994 4 0 0 25 0 1 0 422425295 7159808 1327 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1748 1327 603 41 0 1707 0
vsize: 6992
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1370 0 0 0 3994 4 0 0 25 0 1 0 422425295 7159808 1348 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1748 1348 603 41 0 1707 0
vsize: 6992
[startup+50.0031 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1419 0 0 0 4993 5 0 0 25 0 1 0 422425295 7430144 1397 4294967295 134512640 134672761 3221224544 3221223712 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1814 1397 603 41 0 1773 0
vsize: 7256
[startup+60.0038 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1453 0 0 0 5992 5 0 0 25 0 1 0 422425295 7565312 1431 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1847 1431 603 41 0 1806 0
vsize: 7388
[startup+70.0042 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1556 0 0 0 6992 6 0 0 25 0 1 0 422425295 7970816 1534 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1946 1534 603 41 0 1905 0
vsize: 7784
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1636 0 0 0 7991 7 0 0 25 0 1 0 422425295 8376320 1614 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2045 1614 603 41 0 2004 0
vsize: 8180
[startup+90.0051 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1667 0 0 0 8991 7 0 0 25 0 1 0 422425295 8523776 1645 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2081 1645 603 41 0 2040 0
vsize: 8324
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1677 0 0 0 9990 7 0 0 25 0 1 0 422425295 8523776 1655 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2081 1655 603 41 0 2040 0
vsize: 8324
[startup+110.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1756 0 0 0 10990 8 0 0 25 0 1 0 422425295 8794112 1734 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2147 1734 603 41 0 2106 0
vsize: 8588
[startup+120.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1759 0 0 0 11990 8 0 0 25 0 1 0 422425295 8794112 1737 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1737 603 41 0 2106 0
vsize: 8588
[startup+130.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1762 0 0 0 12990 8 0 0 25 0 1 0 422425295 8933376 1740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2181 1740 603 41 0 2140 0
vsize: 8724
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1783 0 0 0 13990 8 0 0 25 0 1 0 422425295 8933376 1761 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2181 1761 603 41 0 2140 0
vsize: 8724
[startup+150.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1890 0 0 0 14991 8 0 0 25 0 1 0 422425295 9482240 1868 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2315 1868 603 41 0 2274 0
vsize: 9260
[startup+160.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 1936 0 0 0 15991 8 0 0 25 0 1 0 422425295 9617408 1914 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2348 1914 603 41 0 2307 0
vsize: 9392
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2029 0 0 0 16989 9 0 0 25 0 1 0 422425295 10022912 2007 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2447 2007 603 41 0 2406 0
vsize: 9788
[startup+180.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2030 0 0 0 17989 9 0 0 25 0 1 0 422425295 10010624 2008 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2444 2008 603 41 0 2403 0
vsize: 9776
[startup+190.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2031 0 0 0 18989 9 0 0 25 0 1 0 422425295 10010624 2009 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2444 2009 603 41 0 2403 0
vsize: 9776
[startup+200.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2031 0 0 0 19990 9 0 0 25 0 1 0 422425295 10010624 2009 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2444 2009 603 41 0 2403 0
vsize: 9776
[startup+210.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2032 0 0 0 20990 9 0 0 25 0 1 0 422425295 10010624 2010 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2444 2010 603 41 0 2403 0
vsize: 9776
[startup+220.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2100 0 0 0 21990 9 0 0 25 0 1 0 422425295 10285056 2078 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2511 2078 603 41 0 2470 0
vsize: 10044
[startup+230.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2125 0 0 0 22990 9 0 0 25 0 1 0 422425295 10420224 2103 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2544 2103 603 41 0 2503 0
vsize: 10176
[startup+240.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2125 0 0 0 23990 9 0 0 25 0 1 0 422425295 10420224 2103 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2544 2103 603 41 0 2503 0
vsize: 10176
[startup+250.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2209 0 0 0 24990 10 0 0 25 0 1 0 422425295 10698752 2187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2187 603 41 0 2571 0
vsize: 10448
[startup+260.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2250 0 0 0 25990 10 0 0 25 0 1 0 422425295 10833920 2228 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2228 603 41 0 2604 0
vsize: 10580
[startup+270.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2250 0 0 0 26990 10 0 0 25 0 1 0 422425295 10833920 2228 4294967295 134512640 134672761 3221224544 3221223728 134558856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2228 603 41 0 2604 0
vsize: 10580
[startup+280.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2278 0 0 0 27990 10 0 0 25 0 1 0 422425295 10969088 2256 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2678 2256 603 41 0 2637 0
vsize: 10712
[startup+290.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2299 0 0 0 28990 10 0 0 25 0 1 0 422425295 11104256 2277 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2711 2277 603 41 0 2670 0
vsize: 10844
[startup+300.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2319 0 0 0 29991 10 0 0 25 0 1 0 422425295 11239424 2297 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2297 603 41 0 2703 0
vsize: 10976
[startup+310.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2323 0 0 0 30991 10 0 0 25 0 1 0 422425295 11239424 2301 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2301 603 41 0 2703 0
vsize: 10976
[startup+320.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2329 0 0 0 31991 10 0 0 25 0 1 0 422425295 11239424 2307 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2307 603 41 0 2703 0
vsize: 10976
[startup+330.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2335 0 0 0 32991 10 0 0 25 0 1 0 422425295 11239424 2313 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2313 603 41 0 2703 0
vsize: 10976
[startup+340.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2391 0 0 0 33991 10 0 0 25 0 1 0 422425295 11517952 2369 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2812 2369 603 41 0 2771 0
vsize: 11248
[startup+350.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2395 0 0 0 34991 10 0 0 25 0 1 0 422425295 11517952 2373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2812 2373 603 41 0 2771 0
vsize: 11248
[startup+360.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2416 0 0 0 35992 10 0 0 25 0 1 0 422425295 11673600 2394 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2850 2394 603 41 0 2809 0
vsize: 11400
[startup+370.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2424 0 0 0 36992 10 0 0 25 0 1 0 422425295 11673600 2402 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2850 2402 603 41 0 2809 0
vsize: 11400
[startup+380.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2451 0 0 0 37992 10 0 0 25 0 1 0 422425295 11808768 2429 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2883 2429 603 41 0 2842 0
vsize: 11532
[startup+390.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2477 0 0 0 38992 10 0 0 25 0 1 0 422425295 11964416 2455 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2921 2455 603 41 0 2880 0
vsize: 11684
[startup+400.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2500 0 0 0 39992 10 0 0 25 0 1 0 422425295 12099584 2478 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2954 2478 603 41 0 2913 0
vsize: 11816
[startup+410.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2657 0 0 0 40991 11 0 0 25 0 1 0 422425295 12775424 2635 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3119 2635 603 41 0 3078 0
vsize: 12476
[startup+420.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2704 0 0 0 41992 11 0 0 25 0 1 0 422425295 12910592 2682 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3152 2682 603 41 0 3111 0
vsize: 12608
[startup+430.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2743 0 0 0 42992 11 0 0 25 0 1 0 422425295 13045760 2721 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3185 2721 603 41 0 3144 0
vsize: 12740
[startup+440.018 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2748 0 0 0 43992 11 0 0 25 0 1 0 422425295 13189120 2726 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3220 2726 603 41 0 3179 0
vsize: 12880
[startup+450.017 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2749 0 0 0 44992 11 0 0 25 0 1 0 422425295 13189120 2727 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3220 2727 603 41 0 3179 0
vsize: 12880
[startup+460.018 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2769 0 0 0 45992 11 0 0 25 0 1 0 422425295 13189120 2747 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3220 2747 603 41 0 3179 0
vsize: 12880
[startup+470.018 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2774 0 0 0 46992 11 0 0 25 0 1 0 422425295 13189120 2752 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3220 2752 603 41 0 3179 0
vsize: 12880
[startup+480.018 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2786 0 0 0 47992 11 0 0 25 0 1 0 422425295 13352960 2764 4294967295 134512640 134672761 3221224544 3221223632 134554824 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3260 2764 603 41 0 3219 0
vsize: 13040
[startup+490.018 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2850 0 0 0 48992 11 0 0 25 0 1 0 422425295 13623296 2828 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2828 603 41 0 3285 0
vsize: 13304
[startup+500.018 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2851 0 0 0 49992 11 0 0 25 0 1 0 422425295 13623296 2829 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2829 603 41 0 3285 0
vsize: 13304
[startup+510.019 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2852 0 0 0 50993 12 0 0 25 0 1 0 422425295 13623296 2830 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2830 603 41 0 3285 0
vsize: 13304
[startup+520.019 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2859 0 0 0 51993 12 0 0 25 0 1 0 422425295 13623296 2837 4294967295 134512640 134672761 3221224544 3221223716 134559125 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2837 603 41 0 3285 0
vsize: 13304
[startup+530.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2859 0 0 0 52993 12 0 0 25 0 1 0 422425295 13623296 2837 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2837 603 41 0 3285 0
vsize: 13304
[startup+540.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2859 0 0 0 53993 12 0 0 25 0 1 0 422425295 13623296 2837 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2837 603 41 0 3285 0
vsize: 13304
[startup+550.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2865 0 0 0 54993 12 0 0 25 0 1 0 422425295 13623296 2843 4294967295 134512640 134672761 3221224544 3221223728 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3326 2843 603 41 0 3285 0
vsize: 13304
[startup+560.02 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2870 0 0 0 55993 12 0 0 25 0 1 0 422425295 13770752 2848 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2848 603 41 0 3321 0
vsize: 13448
[startup+570.021 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2870 0 0 0 56994 12 0 0 25 0 1 0 422425295 13770752 2848 4294967295 134512640 134672761 3221224544 3221223648 134554988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2848 603 41 0 3321 0
vsize: 13448
[startup+580.02 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2870 0 0 0 57994 12 0 0 25 0 1 0 422425295 13770752 2848 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2848 603 41 0 3321 0
vsize: 13448
[startup+590.021 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2875 0 0 0 58994 12 0 0 25 0 1 0 422425295 13770752 2853 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2853 603 41 0 3321 0
vsize: 13448
[startup+600.021 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2879 0 0 0 59994 12 0 0 25 0 1 0 422425295 13770752 2857 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2857 603 41 0 3321 0
vsize: 13448
[startup+610.02 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2881 0 0 0 60994 12 0 0 25 0 1 0 422425295 13770752 2859 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3362 2859 603 41 0 3321 0
vsize: 13448
[startup+620.021 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2881 0 0 0 61995 12 0 0 25 0 1 0 422425295 13770752 2859 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3362 2859 603 41 0 3321 0
vsize: 13448
[startup+630.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 2891 0 0 0 62994 12 0 0 25 0 1 0 422425295 13905920 2869 4294967295 134512640 134672761 3221224544 3221223720 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3395 2869 603 41 0 3354 0
vsize: 13580
[startup+640.021 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3084 0 0 0 63994 12 0 0 25 0 1 0 422425295 14716928 3062 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3593 3062 603 41 0 3552 0
vsize: 14372
[startup+650.021 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3109 0 0 0 64994 12 0 0 25 0 1 0 422425295 14716928 3087 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3593 3087 603 41 0 3552 0
vsize: 14372
[startup+660.021 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3135 0 0 0 65994 12 0 0 25 0 1 0 422425295 14864384 3113 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3629 3113 603 41 0 3588 0
vsize: 14516
[startup+670.021 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3147 0 0 0 66994 12 0 0 25 0 1 0 422425295 15028224 3125 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3669 3125 603 41 0 3628 0
vsize: 14676
[startup+680.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3149 0 0 0 67994 12 0 0 25 0 1 0 422425295 15028224 3127 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3669 3127 603 41 0 3628 0
vsize: 14676
[startup+690.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3154 0 0 0 68995 12 0 0 25 0 1 0 422425295 15028224 3132 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3669 3132 603 41 0 3628 0
vsize: 14676
[startup+700.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3178 0 0 0 69995 12 0 0 25 0 1 0 422425295 15028224 3156 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3669 3156 603 41 0 3628 0
vsize: 14676
[startup+710.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3178 0 0 0 70995 12 0 0 25 0 1 0 422425295 15028224 3156 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3669 3156 603 41 0 3628 0
vsize: 14676
[startup+720.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3188 0 0 0 71995 12 0 0 25 0 1 0 422425295 15183872 3166 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3707 3166 603 41 0 3666 0
vsize: 14828
[startup+730.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3231 0 0 0 72995 12 0 0 25 0 1 0 422425295 15319040 3209 4294967295 134512640 134672761 3221224544 3221223728 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3740 3209 603 41 0 3699 0
vsize: 14960
[startup+740.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3236 0 0 0 73996 12 0 0 25 0 1 0 422425295 15319040 3214 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3740 3214 603 41 0 3699 0
vsize: 14960
[startup+750.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3236 0 0 0 74996 12 0 0 25 0 1 0 422425295 15319040 3214 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3740 3214 603 41 0 3699 0
vsize: 14960
[startup+760.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3257 0 0 0 75996 12 0 0 25 0 1 0 422425295 15462400 3235 4294967295 134512640 134672761 3221224544 3221223728 134559588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3775 3235 603 41 0 3734 0
vsize: 15100
[startup+770.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3257 0 0 0 76996 12 0 0 25 0 1 0 422425295 15462400 3235 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3775 3235 603 41 0 3734 0
vsize: 15100
[startup+780.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3264 0 0 0 77996 12 0 0 25 0 1 0 422425295 15462400 3242 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3775 3242 603 41 0 3734 0
vsize: 15100
[startup+790.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3276 0 0 0 78996 13 0 0 25 0 1 0 422425295 15626240 3254 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3815 3254 603 41 0 3774 0
vsize: 15260
[startup+800.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3298 0 0 0 79996 13 0 0 25 0 1 0 422425295 15790080 3276 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3855 3276 603 41 0 3814 0
vsize: 15420
[startup+810.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3305 0 0 0 80996 13 0 0 25 0 1 0 422425295 15790080 3283 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3855 3283 603 41 0 3814 0
vsize: 15420
[startup+820.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3305 0 0 0 81997 13 0 0 25 0 1 0 422425295 15790080 3283 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3855 3283 603 41 0 3814 0
vsize: 15420
[startup+830.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3333 0 0 0 82997 13 0 0 25 0 1 0 422425295 15953920 3311 4294967295 134512640 134672761 3221224544 3221222476 134566322 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3895 3311 603 41 0 3854 0
vsize: 15580
[startup+840.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3338 0 0 0 83997 13 0 0 25 0 1 0 422425295 15953920 3316 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3895 3316 603 41 0 3854 0
vsize: 15580
[startup+850.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3396 0 0 0 84997 13 0 0 25 0 1 0 422425295 16232448 3374 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3963 3374 603 41 0 3922 0
vsize: 15852
[startup+860.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3413 0 0 0 85997 13 0 0 25 0 1 0 422425295 16232448 3391 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3963 3391 603 41 0 3922 0
vsize: 15852
[startup+870.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3415 0 0 0 86997 13 0 0 25 0 1 0 422425295 16232448 3393 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3963 3393 603 41 0 3922 0
vsize: 15852
[startup+880.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3416 0 0 0 87998 13 0 0 25 0 1 0 422425295 16232448 3394 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3963 3394 603 41 0 3922 0
vsize: 15852
[startup+890.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3416 0 0 0 88998 13 0 0 25 0 1 0 422425295 16232448 3394 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3963 3394 603 41 0 3922 0
vsize: 15852
[startup+900.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3422 0 0 0 89998 13 0 0 25 0 1 0 422425295 16384000 3400 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3400 603 41 0 3959 0
vsize: 16000
[startup+910.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3424 0 0 0 90998 13 0 0 25 0 1 0 422425295 16384000 3402 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3402 603 41 0 3959 0
vsize: 16000
[startup+920.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3425 0 0 0 91999 13 0 0 25 0 1 0 422425295 16384000 3403 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3403 603 41 0 3959 0
vsize: 16000
[startup+930.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3425 0 0 0 92999 13 0 0 25 0 1 0 422425295 16384000 3403 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3403 603 41 0 3959 0
vsize: 16000
[startup+940.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3425 0 0 0 93999 13 0 0 25 0 1 0 422425295 16384000 3403 4294967295 134512640 134672761 3221224544 3221223712 134561701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3403 603 41 0 3959 0
vsize: 16000
[startup+950.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3425 0 0 0 94999 13 0 0 25 0 1 0 422425295 16384000 3403 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3403 603 41 0 3959 0
vsize: 16000
[startup+960.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3425 0 0 0 95999 13 0 0 25 0 1 0 422425295 16384000 3403 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3403 603 41 0 3959 0
vsize: 16000
[startup+970.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3425 0 0 0 97000 13 0 0 25 0 1 0 422425295 16384000 3403 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3403 603 41 0 3959 0
vsize: 16000
[startup+980.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3425 0 0 0 98000 13 0 0 25 0 1 0 422425295 16384000 3403 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3403 603 41 0 3959 0
vsize: 16000
[startup+990.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3427 0 0 0 99000 13 0 0 25 0 1 0 422425295 16384000 3405 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3405 603 41 0 3959 0
vsize: 16000
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3427 0 0 0 100000 13 0 0 25 0 1 0 422425295 16384000 3405 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3405 603 41 0 3959 0
vsize: 16000
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3427 0 0 0 101000 13 0 0 25 0 1 0 422425295 16384000 3405 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3405 603 41 0 3959 0
vsize: 16000
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3447 0 0 0 101999 13 0 0 25 0 1 0 422425295 16384000 3425 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3425 603 41 0 3959 0
vsize: 16000
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3497 0 0 0 102998 14 0 0 25 0 1 0 422425295 16654336 3475 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4066 3475 603 41 0 4025 0
vsize: 16264
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3510 0 0 0 103998 14 0 0 25 0 1 0 422425295 16654336 3488 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4066 3488 603 41 0 4025 0
vsize: 16264
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3521 0 0 0 104998 14 0 0 25 0 1 0 422425295 16793600 3499 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4100 3499 603 41 0 4059 0
vsize: 16400
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3521 0 0 0 105999 14 0 0 25 0 1 0 422425295 16793600 3499 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4100 3499 603 41 0 4059 0
vsize: 16400
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3521 0 0 0 106999 14 0 0 25 0 1 0 422425295 16793600 3499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4100 3499 603 41 0 4059 0
vsize: 16400
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3521 0 0 0 107999 14 0 0 25 0 1 0 422425295 16793600 3499 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4100 3499 603 41 0 4059 0
vsize: 16400
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3532 0 0 0 108999 14 0 0 25 0 1 0 422425295 16793600 3510 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4100 3510 603 41 0 4059 0
vsize: 16400
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3568 0 0 0 109999 14 0 0 25 0 1 0 422425295 16928768 3546 4294967295 134512640 134672761 3221224544 3221223624 134553505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4133 3546 603 41 0 4092 0
vsize: 16532
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3602 0 0 0 110999 14 0 0 25 0 1 0 422425295 17063936 3580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4166 3580 603 41 0 4125 0
vsize: 16664
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3602 0 0 0 112000 14 0 0 25 0 1 0 422425295 17063936 3580 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4166 3580 603 41 0 4125 0
vsize: 16664
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3602 0 0 0 113000 14 0 0 25 0 1 0 422425295 17063936 3580 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4166 3580 603 41 0 4125 0
vsize: 16664
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3602 0 0 0 114000 14 0 0 25 0 1 0 422425295 17063936 3580 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4166 3580 603 41 0 4125 0
vsize: 16664
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3602 0 0 0 115000 14 0 0 25 0 1 0 422425295 17063936 3580 4294967295 134512640 134672761 3221224544 3221223728 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4166 3580 603 41 0 4125 0
vsize: 16664
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3641 0 0 0 116000 14 0 0 25 0 1 0 422425295 17334272 3619 4294967295 134512640 134672761 3221224544 3221223712 134561009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4232 3619 603 41 0 4191 0
vsize: 16928
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3672 0 0 0 117000 14 0 0 25 0 1 0 422425295 17489920 3650 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4270 3650 603 41 0 4229 0
vsize: 17080
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3674 0 0 0 118000 14 0 0 25 0 1 0 422425295 17489920 3652 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4270 3652 603 41 0 4229 0
vsize: 17080
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3684 0 0 0 119001 14 0 0 25 0 1 0 422425295 17489920 3662 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4270 3662 603 41 0 4229 0
vsize: 17080
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2688
Raw data (stat): 2688 (minisat+) R 2687 30854 30853 0 -1 0 3703 0 0 0 120001 14 0 0 25 0 1 0 422425295 17625088 3681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4303 3681 603 41 0 4262 0
vsize: 17212
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 2688
Raw data (stat): 2688 (minisat+) Z 2687 30854 30853 0 -1 12 3705 0 0 0 120001 15 0 0 25 0 1 0 422425295 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.04
CPU time (s): 1200.17
CPU user time (s): 1200.01
CPU system time (s): 0.154976
CPU usage (%): 100.011
Max. virtual memory (Kb): 17212
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####