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/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-air02.opb
MD5SUM	75acdcffdd43b3d3a30d0459a6bffe45
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6106
Optimality of the best value was proved	NO
Number of terms in the objective function	6774
Biggest coefficient in the objective function	4804
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	6613094
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	4804
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	6613094
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.21
Number of variables	6774
Total number of constraints	6824
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	6824
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	3729
Trace number 19396

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 18:56:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16624 boxname=wulflinc28 idbench=1279 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  75acdcffdd43b3d3a30d0459a6bffe45  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-air02.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-air02.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-air02.opb
IDLAUNCH: 16624
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        499184 kB
Buffers:         34600 kB
Cached:         473392 kB
SwapCached:        104 kB
Active:         207924 kB
Inactive:       302496 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        498932 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            19356 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 19:16:37 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 16624 7 1200.3 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 100 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[  98]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  96]---> Adder-cost: 18   maxlim: 19   bits: 5/5
c ---[  94]---> Adder-cost: 224   maxlim: 115   bits: 7/7
c ---[  92]---> Adder-cost: 62   maxlim: 115   bits: 7/7
c ---[  90]---> Adder-cost: 354   maxlim: 182   bits: 8/8
c ---[  88]---> Adder-cost: 84   maxlim: 182   bits: 8/8
c ---[  86]---> Adder-cost: 690   maxlim: 352   bits: 9/9
c ---[  84]---> Adder-cost: 730   maxlim: 374   bits: 9/9
c ---[  82]---> Adder-cost: 794   maxlim: 507   bits: 9/9
c ---[  80]---> Adder-cost: 1114   maxlim: 571   bits: 10/10
c ---[  78]---> Adder-cost: 1224   maxlim: 646   bits: 10/10
c ---[  76]---> Adder-cost: 1246   maxlim: 635   bits: 10/10
c ---[  74]---> Adder-cost: 1394   maxlim: 724   bits: 10/10
c ---[  72]---> Adder-cost: 1532   maxlim: 801   bits: 10/10
c ---[  70]---> Adder-cost: 254   maxlim: 801   bits: 10/10
c ---[  68]---> Adder-cost: 1296   maxlim: 735   bits: 10/10
c ---[  66]---> Adder-cost: 234   maxlim: 735   bits: 10/10
c ---[  64]---> Adder-cost: 1438   maxlim: 775   bits: 10/10
c ---[  62]---> Adder-cost: 254   maxlim: 775   bits: 10/10
c ---[  60]---> Adder-cost: 1836   maxlim: 1013   bits: 10/10
c ---[  58]---> Adder-cost: 1852   maxlim: 982   bits: 10/10
c ---[  56]---> Adder-cost: 272   maxlim: 982   bits: 10/10
c ---[  54]---> Adder-cost: 1594   maxlim: 878   bits: 10/10
c ---[  52]---> Adder-cost: 264   maxlim: 878   bits: 10/10
c ---[  50]---> Adder-cost: 2172   maxlim: 1336   bits: 11/11
c ---[  48]---> Adder-cost: 1940   maxlim: 1129   bits: 11/11
c ---[  46]---> Adder-cost: 2482   maxlim: 1360   bits: 11/11
c ---[  44]---> Adder-cost: 2380   maxlim: 1299   bits: 11/11
c ---[  42]---> Adder-cost: 344   maxlim: 1299   bits: 11/11
c ---[  40]---> Adder-cost: 2282   maxlim: 1360   bits: 11/11
c ---[  38]---> Adder-cost: 2818   maxlim: 1694   bits: 11/11
c ---[  36]---> Adder-cost: 2498   maxlim: 1408   bits: 11/11
c ---[  34]---> Adder-cost: 2356   maxlim: 1568   bits: 11/11
c ---[  32]---> Adder-cost: 2754   maxlim: 1671   bits: 11/11
c ---[  30]---> Adder-cost: 2890   maxlim: 1762   bits: 11/11
c ---[  28]---> Adder-cost: 2748   maxlim: 1652   bits: 11/11
c ---[  26]---> Adder-cost: 388   maxlim: 1652   bits: 11/11
c ---[  24]---> Adder-cost: 3178   maxlim: 1804   bits: 11/11
c ---[  22]---> Adder-cost: 3418   maxlim: 1807   bits: 11/11
c ---[  20]---> Adder-cost: 432   maxlim: 1807   bits: 11/11
c ---[  18]---> Adder-cost: 432   maxlim: 1807   bits: 11/11
c ---[  16]---> Adder-cost: 3538   maxlim: 1881   bits: 11/11
c ---[  14]---> Adder-cost: 3750   maxlim: 1966   bits: 11/11
c ---[  12]---> Adder-cost: 3864   maxlim: 2106   bits: 12/12
c ---[  10]---> Adder-cost: 3550   maxlim: 1952   bits: 11/11
c ---[   8]---> Adder-cost: 4028   maxlim: 2237   bits: 12/12
c ---[   6]---> Adder-cost: 3642   maxlim: 2444   bits: 12/12
c ---[   4]---> Adder-cost: 4412   maxlim: 2486   bits: 12/12
c ---[   2]---> Adder-cost: 4162   maxlim: 2494   bits: 12/12
c ---[   0]---> Adder-cost: 5306   maxlim: 3728   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  630475  2250451 |  210158       0        0     nan |  0.000 % |
c |       100 |  630433  2250303 |  231173      95      325     3.4 |  1.071 % |
c |       250 |  628983  2245159 |  254291      36      113     3.1 |  1.319 % |
c |       476 |  627685  2240565 |  279720      91      282     3.1 |  1.541 % |
c |       813 |  625070  2231326 |  307692      90      267     3.0 |  1.983 % |
c |      1319 |  621682  2219342 |  338461     202      615     3.0 |  2.547 % |
c |      2080 |  617002  2202764 |  372307     389     1310     3.4 |  3.346 % |
c |      3219 |  612060  2185228 |  409538     893     3498     3.9 |  4.155 % |
c |      4928 |  604308  2157764 |  450492    1518     6974     4.6 |  5.453 % |
c |      7490 |  601016  2146034 |  495541    3647    20385     5.6 |  5.990 % |
c |     11334 |  598547  2137181 |  545095    7220    61755     8.6 |  6.387 % |
c |     17100 |  596682  2130422 |  599605   12784   113268     8.9 |  6.685 % |
c |     25750 |  589452  2104606 |  659565   20568   187232     9.1 |  7.833 % |
c |     38724 |  572714  2044664 |  725522   31146   287256     9.2 | 10.600 % |
#### 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.95 2/54 29753
Raw data (stat): 29753 (runsolver) R 29752 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547415067 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.95 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11181 0 0 0 970 28 0 0 25 0 1 0 547415067 50688000 10844 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12375 10844 603 41 0 12334 0
vsize: 49500
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.96 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11267 0 0 0 1969 28 0 0 25 0 1 0 547415067 50958336 10930 4294967295 134512640 134672761 3221224544 3221223712 134564467 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12441 10930 603 41 0 12400 0
vsize: 49764
[startup+30.001 s]
Raw data (loadavg): 0.95 0.96 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11318 0 0 0 2970 28 0 0 25 0 1 0 547415067 51228672 10981 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 10981 603 41 0 12466 0
vsize: 50028
[startup+40.0011 s]
Raw data (loadavg): 0.95 0.96 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11369 0 0 0 3969 29 0 0 25 0 1 0 547415067 51363840 11032 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12540 11032 603 41 0 12499 0
vsize: 50160
[startup+50.0006 s]
Raw data (loadavg): 0.96 0.96 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11405 0 0 0 4968 29 0 0 25 0 1 0 547415067 51499008 11068 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12573 11068 603 41 0 12532 0
vsize: 50292
[startup+60.001 s]
Raw data (loadavg): 0.97 0.96 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11437 0 0 0 5968 29 0 0 25 0 1 0 547415067 51634176 11100 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12606 11100 603 41 0 12565 0
vsize: 50424
[startup+70.0008 s]
Raw data (loadavg): 0.97 0.96 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11502 0 0 0 6968 29 0 0 25 0 1 0 547415067 51904512 11165 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12672 11165 603 41 0 12631 0
vsize: 50688
[startup+80.0017 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11549 0 0 0 7967 30 0 0 25 0 1 0 547415067 52174848 11212 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12738 11212 603 41 0 12697 0
vsize: 50952
[startup+90.001 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11573 0 0 0 8967 30 0 0 25 0 1 0 547415067 52174848 11236 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12738 11236 603 41 0 12697 0
vsize: 50952
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11598 0 0 0 9968 30 0 0 25 0 1 0 547415067 52310016 11261 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12771 11261 603 41 0 12730 0
vsize: 51084
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11615 0 0 0 10968 30 0 0 25 0 1 0 547415067 52445184 11278 4294967295 134512640 134672761 3221224544 3221223708 134564515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12804 11278 603 41 0 12763 0
vsize: 51216
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11637 0 0 0 11968 30 0 0 25 0 1 0 547415067 52445184 11300 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12804 11300 603 41 0 12763 0
vsize: 51216
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11645 0 0 0 12968 30 0 0 25 0 1 0 547415067 52580352 11308 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12837 11308 603 41 0 12796 0
vsize: 51348
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11651 0 0 0 13968 30 0 0 25 0 1 0 547415067 52580352 11314 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12837 11314 603 41 0 12796 0
vsize: 51348
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11660 0 0 0 14968 30 0 0 25 0 1 0 547415067 52580352 11323 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12837 11323 603 41 0 12796 0
vsize: 51348
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11665 0 0 0 15968 30 0 0 25 0 1 0 547415067 52580352 11328 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12837 11328 603 41 0 12796 0
vsize: 51348
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11681 0 0 0 16968 30 0 0 25 0 1 0 547415067 52580352 11344 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12837 11344 603 41 0 12796 0
vsize: 51348
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11686 0 0 0 17969 30 0 0 25 0 1 0 547415067 52580352 11349 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12837 11349 603 41 0 12796 0
vsize: 51348
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11691 0 0 0 18969 30 0 0 25 0 1 0 547415067 52580352 11354 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12837 11354 603 41 0 12796 0
vsize: 51348
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 29753
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11695 0 0 0 19969 30 0 0 25 0 1 0 547415067 52715520 11358 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11358 603 41 0 12829 0
vsize: 51480
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.95 4/58 29785
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11697 0 0 0 20968 31 0 0 25 0 1 0 547415067 52715520 11360 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11360 603 41 0 12829 0
vsize: 51480
[startup+220.003 s]
Raw data (loadavg): 1.07 0.99 0.95 2/54 29806
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11703 0 0 0 21967 32 0 0 25 0 1 0 547415067 52715520 11366 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11366 603 41 0 12829 0
vsize: 51480
[startup+230.004 s]
Raw data (loadavg): 1.06 0.99 0.95 2/54 29806
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11710 0 0 0 22967 32 0 0 25 0 1 0 547415067 52715520 11373 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11373 603 41 0 12829 0
vsize: 51480
[startup+240.004 s]
Raw data (loadavg): 1.05 0.99 0.95 2/54 29806
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11711 0 0 0 23967 33 0 0 25 0 1 0 547415067 52715520 11374 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11374 603 41 0 12829 0
vsize: 51480
[startup+250.004 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 29806
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11712 0 0 0 24967 33 0 0 25 0 1 0 547415067 52715520 11375 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11375 603 41 0 12829 0
vsize: 51480
[startup+260.004 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 29806
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11714 0 0 0 25967 33 0 0 25 0 1 0 547415067 52715520 11377 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11377 603 41 0 12829 0
vsize: 51480
[startup+270.003 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 29806
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11716 0 0 0 26967 33 0 0 25 0 1 0 547415067 52715520 11379 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11379 603 41 0 12829 0
vsize: 51480
[startup+280.003 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11716 0 0 0 27967 33 0 0 25 0 1 0 547415067 52715520 11379 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11379 603 41 0 12829 0
vsize: 51480
[startup+290.004 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11716 0 0 0 28968 33 0 0 25 0 1 0 547415067 52715520 11379 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11379 603 41 0 12829 0
vsize: 51480
[startup+300.004 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11717 0 0 0 29968 33 0 0 25 0 1 0 547415067 52715520 11380 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11380 603 41 0 12829 0
vsize: 51480
[startup+310.004 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11717 0 0 0 30968 33 0 0 25 0 1 0 547415067 52715520 11380 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11380 603 41 0 12829 0
vsize: 51480
[startup+320.004 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11718 0 0 0 31968 33 0 0 25 0 1 0 547415067 52715520 11381 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11381 603 41 0 12829 0
vsize: 51480
[startup+330.005 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11719 0 0 0 32968 33 0 0 25 0 1 0 547415067 52715520 11382 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11382 603 41 0 12829 0
vsize: 51480
[startup+340.004 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11719 0 0 0 33968 33 0 0 25 0 1 0 547415067 52715520 11382 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11382 603 41 0 12829 0
vsize: 51480
[startup+350.004 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11720 0 0 0 34969 33 0 0 25 0 1 0 547415067 52715520 11383 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11383 603 41 0 12829 0
vsize: 51480
[startup+360.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11721 0 0 0 35969 33 0 0 25 0 1 0 547415067 52715520 11384 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11384 603 41 0 12829 0
vsize: 51480
[startup+370.004 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11726 0 0 0 36969 33 0 0 25 0 1 0 547415067 52715520 11389 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11389 603 41 0 12829 0
vsize: 51480
[startup+380.004 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11733 0 0 0 37969 33 0 0 25 0 1 0 547415067 52715520 11396 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11396 603 41 0 12829 0
vsize: 51480
[startup+390.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11739 0 0 0 38969 33 0 0 25 0 1 0 547415067 52715520 11402 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11402 603 41 0 12829 0
vsize: 51480
[startup+400.004 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11741 0 0 0 39969 33 0 0 25 0 1 0 547415067 52715520 11404 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11404 603 41 0 12829 0
vsize: 51480
[startup+410.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11745 0 0 0 40969 33 0 0 25 0 1 0 547415067 52715520 11408 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11408 603 41 0 12829 0
vsize: 51480
[startup+420.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11745 0 0 0 41969 33 0 0 25 0 1 0 547415067 52715520 11408 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11408 603 41 0 12829 0
vsize: 51480
[startup+430.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11747 0 0 0 42969 33 0 0 25 0 1 0 547415067 52715520 11410 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11410 603 41 0 12829 0
vsize: 51480
[startup+440.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11749 0 0 0 43969 33 0 0 25 0 1 0 547415067 52715520 11412 4294967295 134512640 134672761 3221224544 3221223712 134564725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11412 603 41 0 12829 0
vsize: 51480
[startup+450.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11750 0 0 0 44970 33 0 0 25 0 1 0 547415067 52715520 11413 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11413 603 41 0 12829 0
vsize: 51480
[startup+460.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11751 0 0 0 45970 33 0 0 25 0 1 0 547415067 52715520 11414 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11414 603 41 0 12829 0
vsize: 51480
[startup+470.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11751 0 0 0 46970 33 0 0 25 0 1 0 547415067 52715520 11414 4294967295 134512640 134672761 3221224544 3221223696 134564785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11414 603 41 0 12829 0
vsize: 51480
[startup+480.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11751 0 0 0 47970 33 0 0 25 0 1 0 547415067 52715520 11414 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11414 603 41 0 12829 0
vsize: 51480
[startup+490.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11756 0 0 0 48970 33 0 0 25 0 1 0 547415067 52715520 11419 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11419 603 41 0 12829 0
vsize: 51480
[startup+500.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11757 0 0 0 49971 33 0 0 25 0 1 0 547415067 52715520 11420 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11420 603 41 0 12829 0
vsize: 51480
[startup+510.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11757 0 0 0 50971 33 0 0 25 0 1 0 547415067 52715520 11420 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11420 603 41 0 12829 0
vsize: 51480
[startup+520.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11759 0 0 0 51971 33 0 0 25 0 1 0 547415067 52715520 11422 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11422 603 41 0 12829 0
vsize: 51480
[startup+530.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11763 0 0 0 52971 33 0 0 25 0 1 0 547415067 52846592 11426 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12902 11426 603 41 0 12861 0
vsize: 51608
[startup+540.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11780 0 0 0 53971 33 0 0 25 0 1 0 547415067 52846592 11443 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12902 11443 603 41 0 12861 0
vsize: 51608
[startup+550.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11781 0 0 0 54971 33 0 0 25 0 1 0 547415067 52846592 11444 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12902 11444 603 41 0 12861 0
vsize: 51608
[startup+560.005 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11800 0 0 0 55972 33 0 0 25 0 1 0 547415067 52989952 11463 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12937 11463 603 41 0 12896 0
vsize: 51748
[startup+570.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29808
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11804 0 0 0 56972 33 0 0 25 0 1 0 547415067 52989952 11467 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12937 11467 603 41 0 12896 0
vsize: 51748
[startup+580.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11811 0 0 0 57972 33 0 0 25 0 1 0 547415067 52989952 11474 4294967295 134512640 134672761 3221224544 3221223744 134557916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12937 11474 603 41 0 12896 0
vsize: 51748
[startup+590.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11817 0 0 0 58972 33 0 0 25 0 1 0 547415067 52989952 11480 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12937 11480 603 41 0 12896 0
vsize: 51748
[startup+600.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11820 0 0 0 59972 33 0 0 25 0 1 0 547415067 52989952 11483 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12937 11483 603 41 0 12896 0
vsize: 51748
[startup+610.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11836 0 0 0 60972 33 0 0 25 0 1 0 547415067 53125120 11499 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12970 11499 603 41 0 12929 0
vsize: 51880
[startup+620.006 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11841 0 0 0 61973 33 0 0 25 0 1 0 547415067 53125120 11504 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12970 11504 603 41 0 12929 0
vsize: 51880
[startup+630.007 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11842 0 0 0 62973 33 0 0 25 0 1 0 547415067 53125120 11505 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12970 11505 603 41 0 12929 0
vsize: 51880
[startup+640.007 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11847 0 0 0 63973 33 0 0 25 0 1 0 547415067 53125120 11510 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12970 11510 603 41 0 12929 0
vsize: 51880
[startup+650.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11852 0 0 0 64973 33 0 0 25 0 1 0 547415067 53125120 11515 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12970 11515 603 41 0 12929 0
vsize: 51880
[startup+660.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11857 0 0 0 65974 33 0 0 25 0 1 0 547415067 53125120 11520 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12970 11520 603 41 0 12929 0
vsize: 51880
[startup+670.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11860 0 0 0 66974 33 0 0 25 0 1 0 547415067 53125120 11523 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12970 11523 603 41 0 12929 0
vsize: 51880
[startup+680.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11865 0 0 0 67974 33 0 0 25 0 1 0 547415067 53125120 11528 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12970 11528 603 41 0 12929 0
vsize: 51880
[startup+690.008 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11870 0 0 0 68974 33 0 0 25 0 1 0 547415067 53260288 11533 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13003 11533 603 41 0 12962 0
vsize: 52012
[startup+700.008 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11888 0 0 0 69974 33 0 0 25 0 1 0 547415067 53411840 11551 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13040 11551 603 41 0 12999 0
vsize: 52160
[startup+710.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11888 0 0 0 70974 33 0 0 25 0 1 0 547415067 53411840 11551 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13040 11551 603 41 0 12999 0
vsize: 52160
[startup+720.008 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11889 0 0 0 71974 33 0 0 25 0 1 0 547415067 53411840 11552 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13040 11552 603 41 0 12999 0
vsize: 52160
[startup+730.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11891 0 0 0 72975 33 0 0 25 0 1 0 547415067 53411840 11554 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13040 11554 603 41 0 12999 0
vsize: 52160
[startup+740.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11894 0 0 0 73975 33 0 0 25 0 1 0 547415067 53411840 11557 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13040 11557 603 41 0 12999 0
vsize: 52160
[startup+750.008 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11941 0 0 0 74974 34 0 0 25 0 1 0 547415067 53547008 11604 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13073 11604 603 41 0 13032 0
vsize: 52292
[startup+760.008 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11944 0 0 0 75974 34 0 0 25 0 1 0 547415067 53547008 11607 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13073 11607 603 41 0 13032 0
vsize: 52292
[startup+770.008 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11947 0 0 0 76974 34 0 0 25 0 1 0 547415067 53547008 11610 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13073 11610 603 41 0 13032 0
vsize: 52292
[startup+780.008 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11952 0 0 0 77975 34 0 0 25 0 1 0 547415067 53547008 11615 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13073 11615 603 41 0 13032 0
vsize: 52292
[startup+790.008 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11954 0 0 0 78975 34 0 0 25 0 1 0 547415067 53547008 11617 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13073 11617 603 41 0 13032 0
vsize: 52292
[startup+800.008 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11961 0 0 0 79975 34 0 0 25 0 1 0 547415067 53682176 11624 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13106 11624 603 41 0 13065 0
vsize: 52424
[startup+810.008 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11966 0 0 0 80975 34 0 0 25 0 1 0 547415067 53682176 11629 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13106 11629 603 41 0 13065 0
vsize: 52424
[startup+820.008 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11968 0 0 0 81975 34 0 0 25 0 1 0 547415067 53682176 11631 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13106 11631 603 41 0 13065 0
vsize: 52424
[startup+830.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11972 0 0 0 82976 34 0 0 25 0 1 0 547415067 53682176 11635 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13106 11635 603 41 0 13065 0
vsize: 52424
[startup+840.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11972 0 0 0 83976 34 0 0 25 0 1 0 547415067 53682176 11635 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13106 11635 603 41 0 13065 0
vsize: 52424
[startup+850.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11978 0 0 0 84976 34 0 0 25 0 1 0 547415067 53682176 11641 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13106 11641 603 41 0 13065 0
vsize: 52424
[startup+860.111 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11982 0 0 0 85986 34 0 0 25 0 1 0 547415067 53682176 11645 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13106 11645 603 41 0 13065 0
vsize: 52424
[startup+870.11 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11987 0 0 0 86986 34 0 0 25 0 1 0 547415067 53682176 11650 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13106 11650 603 41 0 13065 0
vsize: 52424
[startup+880.116 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11990 0 0 0 87987 34 0 0 25 0 1 0 547415067 53682176 11653 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13106 11653 603 41 0 13065 0
vsize: 52424
[startup+890.117 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11993 0 0 0 88987 34 0 0 25 0 1 0 547415067 53682176 11656 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13106 11656 603 41 0 13065 0
vsize: 52424
[startup+900.116 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11998 0 0 0 89988 34 0 0 25 0 1 0 547415067 53817344 11661 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13139 11661 603 41 0 13098 0
vsize: 52556
[startup+910.116 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 11998 0 0 0 90988 34 0 0 25 0 1 0 547415067 53817344 11661 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13139 11661 603 41 0 13098 0
vsize: 52556
[startup+920.116 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12001 0 0 0 91988 34 0 0 25 0 1 0 547415067 53817344 11664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13139 11664 603 41 0 13098 0
vsize: 52556
[startup+930.116 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12006 0 0 0 92988 34 0 0 25 0 1 0 547415067 53817344 11669 4294967295 134512640 134672761 3221224544 3221223696 134565119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13139 11669 603 41 0 13098 0
vsize: 52556
[startup+940.116 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12009 0 0 0 93988 34 0 0 25 0 1 0 547415067 53817344 11672 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13139 11672 603 41 0 13098 0
vsize: 52556
[startup+950.116 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12013 0 0 0 94988 34 0 0 25 0 1 0 547415067 53817344 11676 4294967295 134512640 134672761 3221224544 3221223724 134553584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13139 11676 603 41 0 13098 0
vsize: 52556
[startup+960.116 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12016 0 0 0 95989 34 0 0 25 0 1 0 547415067 53817344 11679 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13139 11679 603 41 0 13098 0
vsize: 52556
[startup+970.116 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12023 0 0 0 96989 34 0 0 25 0 1 0 547415067 53817344 11686 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13139 11686 603 41 0 13098 0
vsize: 52556
[startup+980.117 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12027 0 0 0 97989 34 0 0 25 0 1 0 547415067 53817344 11690 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13139 11690 603 41 0 13098 0
vsize: 52556
[startup+990.117 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12032 0 0 0 98989 34 0 0 25 0 1 0 547415067 53952512 11695 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13172 11695 603 41 0 13131 0
vsize: 52688
[startup+1000.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12040 0 0 0 99989 34 0 0 25 0 1 0 547415067 53952512 11703 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13172 11703 603 41 0 13131 0
vsize: 52688
[startup+1010.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12046 0 0 0 100990 34 0 0 25 0 1 0 547415067 53952512 11709 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13172 11709 603 41 0 13131 0
vsize: 52688
[startup+1020.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12049 0 0 0 101990 34 0 0 25 0 1 0 547415067 53952512 11712 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13172 11712 603 41 0 13131 0
vsize: 52688
[startup+1030.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12050 0 0 0 102989 34 0 0 25 0 1 0 547415067 53952512 11713 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 11713 603 41 0 13131 0
vsize: 52688
[startup+1040.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12057 0 0 0 103988 35 0 0 25 0 1 0 547415067 53952512 11720 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 11720 603 41 0 13131 0
vsize: 52688
[startup+1050.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12063 0 0 0 104987 35 0 0 25 0 1 0 547415067 53952512 11726 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13172 11726 603 41 0 13131 0
vsize: 52688
[startup+1060.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12104 0 0 0 105987 35 0 0 25 0 1 0 547415067 54349824 11767 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11767 603 41 0 13228 0
vsize: 53076
[startup+1070.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12104 0 0 0 106988 35 0 0 25 0 1 0 547415067 54349824 11767 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11767 603 41 0 13228 0
vsize: 53076
[startup+1080.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12105 0 0 0 107988 35 0 0 25 0 1 0 547415067 54349824 11768 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11768 603 41 0 13228 0
vsize: 53076
[startup+1090.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12105 0 0 0 108988 35 0 0 25 0 1 0 547415067 54349824 11768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11768 603 41 0 13228 0
vsize: 53076
[startup+1100.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12105 0 0 0 109988 35 0 0 25 0 1 0 547415067 54349824 11768 4294967295 134512640 134672761 3221224544 3221223716 134556669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11768 603 41 0 13228 0
vsize: 53076
[startup+1110.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12105 0 0 0 110988 35 0 0 25 0 1 0 547415067 54349824 11768 4294967295 134512640 134672761 3221224544 3221223708 134564508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11768 603 41 0 13228 0
vsize: 53076
[startup+1120.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12105 0 0 0 111989 35 0 0 25 0 1 0 547415067 54349824 11768 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11768 603 41 0 13228 0
vsize: 53076
[startup+1130.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12106 0 0 0 112989 35 0 0 25 0 1 0 547415067 54349824 11769 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11769 603 41 0 13228 0
vsize: 53076
[startup+1140.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12107 0 0 0 113989 35 0 0 25 0 1 0 547415067 54349824 11770 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11770 603 41 0 13228 0
vsize: 53076
[startup+1150.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12108 0 0 0 114989 35 0 0 25 0 1 0 547415067 54349824 11771 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11771 603 41 0 13228 0
vsize: 53076
[startup+1160.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12110 0 0 0 115990 35 0 0 25 0 1 0 547415067 54349824 11773 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11773 603 41 0 13228 0
vsize: 53076
[startup+1170.12 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12112 0 0 0 116990 35 0 0 25 0 1 0 547415067 54349824 11775 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11775 603 41 0 13228 0
vsize: 53076
[startup+1180.13 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12114 0 0 0 117991 35 0 0 25 0 1 0 547415067 54349824 11777 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11777 603 41 0 13228 0
vsize: 53076
[startup+1190.13 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12117 0 0 0 118991 35 0 0 25 0 1 0 547415067 54349824 11780 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11780 603 41 0 13228 0
vsize: 53076
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 29810
Raw data (stat): 29753 (minisat+) R 29752 10614 10613 0 -1 0 12119 0 0 0 119991 35 0 0 25 0 1 0 547415067 54349824 11782 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13269 11782 603 41 0 13228 0
vsize: 53076
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.00 0.99 0.95 1/54 29810
Raw data (stat): 29753 (minisat+) Z 29752 10614 10613 0 -1 12 12121 0 0 0 119991 38 0 0 25 0 1 0 547415067 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.16
CPU time (s): 1200.3
CPU user time (s): 1199.92
CPU system time (s): 0.380942
CPU usage (%): 100.012
Max. virtual memory (Kb): 53076
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####