Some explanations

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

General information on the benchmark

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-air02.opb
MD5SUM75acdcffdd43b3d3a30d0459a6bffe45
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers23
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1190.1
Number of variables6774
Total number of constraints6824
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)6824
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint3729

Trace number 17234 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-21 09:49:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11632 boxname=wulflinc4 idbench=895 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  75acdcffdd43b3d3a30d0459a6bffe45  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-air02.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-air02.opb /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-air02.opb
IDLAUNCH: 11632
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        374652 kB
Buffers:         17668 kB
Cached:         619016 kB
SwapCached:          0 kB
Active:          34296 kB
Inactive:       605160 kB
HighTotal:      131008 kB
HighFree:        26768 kB
LowTotal:       903652 kB
LowFree:        347884 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14916 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 10:09:03 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 11632 7 1200.23 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.84 0.94 0.92 2/54 5208
Raw data (stat): 5208 (runsolver) R 5207 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485898578 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.87 0.94 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11181 0 0 0 971 27 0 0 25 0 1 0 485898578 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.0005 s]
Raw data (loadavg): 0.89 0.94 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11265 0 0 0 1970 27 0 0 25 0 1 0 485898578 50958336 10928 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12441 10928 603 41 0 12400 0
vsize: 49764
[startup+30.0013 s]
Raw data (loadavg): 0.90 0.94 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11317 0 0 0 2970 27 0 0 25 0 1 0 485898578 51228672 10980 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 10980 603 41 0 12466 0
vsize: 50028
[startup+40.0012 s]
Raw data (loadavg): 0.92 0.94 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11369 0 0 0 3969 27 0 0 25 0 1 0 485898578 51363840 11032 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12540 11032 603 41 0 12499 0
vsize: 50160
[startup+50.0023 s]
Raw data (loadavg): 0.93 0.94 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11402 0 0 0 4970 27 0 0 25 0 1 0 485898578 51499008 11065 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12573 11065 603 41 0 12532 0
vsize: 50292
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11437 0 0 0 5970 27 0 0 25 0 1 0 485898578 51634176 11100 4294967295 134512640 134672761 3221224544 3221223760 134561993 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.0017 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11502 0 0 0 6969 28 0 0 25 0 1 0 485898578 51904512 11165 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12672 11165 603 41 0 12631 0
vsize: 50688
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11543 0 0 0 7970 28 0 0 25 0 1 0 485898578 52174848 11206 4294967295 134512640 134672761 3221224544 3221223712 134564496 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12738 11206 603 41 0 12697 0
vsize: 50952
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11573 0 0 0 8970 28 0 0 25 0 1 0 485898578 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.002 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11598 0 0 0 9970 28 0 0 25 0 1 0 485898578 52310016 11261 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.97 0.95 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11615 0 0 0 10970 28 0 0 25 0 1 0 485898578 52445184 11278 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.98 0.95 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11635 0 0 0 11970 28 0 0 25 0 1 0 485898578 52445184 11298 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12804 11298 603 41 0 12763 0
vsize: 51216
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11644 0 0 0 12970 28 0 0 25 0 1 0 485898578 52580352 11307 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12837 11307 603 41 0 12796 0
vsize: 51348
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11651 0 0 0 13970 28 0 0 25 0 1 0 485898578 52580352 11314 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.003 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11660 0 0 0 14970 28 0 0 25 0 1 0 485898578 52580352 11323 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.003 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11665 0 0 0 15970 28 0 0 25 0 1 0 485898578 52580352 11328 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.003 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11681 0 0 0 16971 28 0 0 25 0 1 0 485898578 52580352 11344 4294967295 134512640 134672761 3221224544 3221223712 134560882 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.003 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11685 0 0 0 17971 28 0 0 25 0 1 0 485898578 52580352 11348 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12837 11348 603 41 0 12796 0
vsize: 51348
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11691 0 0 0 18971 28 0 0 25 0 1 0 485898578 52580352 11354 4294967295 134512640 134672761 3221224544 3221223716 134556596 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.004 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11694 0 0 0 19971 28 0 0 25 0 1 0 485898578 52715520 11357 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11357 603 41 0 12829 0
vsize: 51480
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11697 0 0 0 20971 28 0 0 25 0 1 0 485898578 52715520 11360 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11360 603 41 0 12829 0
vsize: 51480
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11702 0 0 0 21971 28 0 0 25 0 1 0 485898578 52715520 11365 4294967295 134512640 134672761 3221224544 3221223724 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11365 603 41 0 12829 0
vsize: 51480
[startup+230.004 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11709 0 0 0 22972 28 0 0 25 0 1 0 485898578 52715520 11372 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11372 603 41 0 12829 0
vsize: 51480
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11711 0 0 0 23972 28 0 0 25 0 1 0 485898578 52715520 11374 4294967295 134512640 134672761 3221224544 3221223716 134556598 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): 0.99 0.96 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11712 0 0 0 24972 28 0 0 25 0 1 0 485898578 52715520 11375 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11375 603 41 0 12829 0
vsize: 51480
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11714 0 0 0 25972 28 0 0 25 0 1 0 485898578 52715520 11377 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11377 603 41 0 12829 0
vsize: 51480
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11716 0 0 0 26972 28 0 0 25 0 1 0 485898578 52715520 11379 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11379 603 41 0 12829 0
vsize: 51480
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11716 0 0 0 27972 28 0 0 25 0 1 0 485898578 52715520 11379 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11379 603 41 0 12829 0
vsize: 51480
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11716 0 0 0 28973 28 0 0 25 0 1 0 485898578 52715520 11379 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11379 603 41 0 12829 0
vsize: 51480
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11717 0 0 0 29973 28 0 0 25 0 1 0 485898578 52715520 11380 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11380 603 41 0 12829 0
vsize: 51480
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11717 0 0 0 30973 28 0 0 25 0 1 0 485898578 52715520 11380 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11380 603 41 0 12829 0
vsize: 51480
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11718 0 0 0 31973 28 0 0 25 0 1 0 485898578 52715520 11381 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11381 603 41 0 12829 0
vsize: 51480
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11719 0 0 0 32973 28 0 0 25 0 1 0 485898578 52715520 11382 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11382 603 41 0 12829 0
vsize: 51480
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11719 0 0 0 33973 28 0 0 25 0 1 0 485898578 52715520 11382 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11382 603 41 0 12829 0
vsize: 51480
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11720 0 0 0 34974 28 0 0 25 0 1 0 485898578 52715520 11383 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11383 603 41 0 12829 0
vsize: 51480
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11721 0 0 0 35974 28 0 0 25 0 1 0 485898578 52715520 11384 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11384 603 41 0 12829 0
vsize: 51480
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11726 0 0 0 36974 28 0 0 25 0 1 0 485898578 52715520 11389 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11389 603 41 0 12829 0
vsize: 51480
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11730 0 0 0 37974 28 0 0 25 0 1 0 485898578 52715520 11393 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12870 11393 603 41 0 12829 0
vsize: 51480
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11739 0 0 0 38974 28 0 0 25 0 1 0 485898578 52715520 11402 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11402 603 41 0 12829 0
vsize: 51480
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11741 0 0 0 39974 28 0 0 25 0 1 0 485898578 52715520 11404 4294967295 134512640 134672761 3221224544 3221223712 134564451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11404 603 41 0 12829 0
vsize: 51480
[startup+410.014 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11745 0 0 0 40974 29 0 0 25 0 1 0 485898578 52715520 11408 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11408 603 41 0 12829 0
vsize: 51480
[startup+420.014 s]
Raw data (loadavg): 1.14 1.00 0.93 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11745 0 0 0 41975 29 0 0 25 0 1 0 485898578 52715520 11408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11408 603 41 0 12829 0
vsize: 51480
[startup+430.015 s]
Raw data (loadavg): 1.11 1.00 0.93 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11747 0 0 0 42975 29 0 0 25 0 1 0 485898578 52715520 11410 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11410 603 41 0 12829 0
vsize: 51480
[startup+440.015 s]
Raw data (loadavg): 1.18 1.02 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11749 0 0 0 43975 29 0 0 25 0 1 0 485898578 52715520 11412 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11412 603 41 0 12829 0
vsize: 51480
[startup+450.016 s]
Raw data (loadavg): 1.15 1.02 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11750 0 0 0 44975 29 0 0 25 0 1 0 485898578 52715520 11413 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11413 603 41 0 12829 0
vsize: 51480
[startup+460.025 s]
Raw data (loadavg): 1.13 1.02 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11751 0 0 0 45976 29 0 0 25 0 1 0 485898578 52715520 11414 4294967295 134512640 134672761 3221224544 3221223716 134556669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11414 603 41 0 12829 0
vsize: 51480
[startup+470.025 s]
Raw data (loadavg): 1.11 1.02 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11751 0 0 0 46976 29 0 0 25 0 1 0 485898578 52715520 11414 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11414 603 41 0 12829 0
vsize: 51480
[startup+480.025 s]
Raw data (loadavg): 1.09 1.01 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11751 0 0 0 47977 29 0 0 25 0 1 0 485898578 52715520 11414 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11414 603 41 0 12829 0
vsize: 51480
[startup+490.025 s]
Raw data (loadavg): 1.08 1.01 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11756 0 0 0 48977 29 0 0 25 0 1 0 485898578 52715520 11419 4294967295 134512640 134672761 3221224544 3221223712 134564726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11419 603 41 0 12829 0
vsize: 51480
[startup+500.026 s]
Raw data (loadavg): 1.06 1.01 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11757 0 0 0 49977 29 0 0 25 0 1 0 485898578 52715520 11420 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11420 603 41 0 12829 0
vsize: 51480
[startup+510.026 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11757 0 0 0 50977 29 0 0 25 0 1 0 485898578 52715520 11420 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11420 603 41 0 12829 0
vsize: 51480
[startup+520.026 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11759 0 0 0 51977 29 0 0 25 0 1 0 485898578 52715520 11422 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12870 11422 603 41 0 12829 0
vsize: 51480
[startup+530.027 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11763 0 0 0 52978 29 0 0 25 0 1 0 485898578 52846592 11426 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12902 11426 603 41 0 12861 0
vsize: 51608
[startup+540.026 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11780 0 0 0 53978 29 0 0 25 0 1 0 485898578 52846592 11443 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12902 11443 603 41 0 12861 0
vsize: 51608
[startup+550.028 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11782 0 0 0 54978 29 0 0 25 0 1 0 485898578 52846592 11445 4294967295 134512640 134672761 3221224544 3221223712 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12902 11445 603 41 0 12861 0
vsize: 51608
[startup+560.027 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11800 0 0 0 55978 29 0 0 25 0 1 0 485898578 52989952 11463 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12937 11463 603 41 0 12896 0
vsize: 51748
[startup+570.027 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11804 0 0 0 56978 29 0 0 25 0 1 0 485898578 52989952 11467 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12937 11467 603 41 0 12896 0
vsize: 51748
[startup+580.027 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11811 0 0 0 57978 29 0 0 25 0 1 0 485898578 52989952 11474 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12937 11474 603 41 0 12896 0
vsize: 51748
[startup+590.027 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11817 0 0 0 58978 29 0 0 25 0 1 0 485898578 52989952 11480 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12937 11480 603 41 0 12896 0
vsize: 51748
[startup+600.028 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11820 0 0 0 59979 29 0 0 25 0 1 0 485898578 52989952 11483 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12937 11483 603 41 0 12896 0
vsize: 51748
[startup+610.028 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11836 0 0 0 60979 29 0 0 25 0 1 0 485898578 53125120 11499 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12970 11499 603 41 0 12929 0
vsize: 51880
[startup+620.027 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11841 0 0 0 61979 29 0 0 25 0 1 0 485898578 53125120 11504 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12970 11504 603 41 0 12929 0
vsize: 51880
[startup+630.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11842 0 0 0 62979 29 0 0 25 0 1 0 485898578 53125120 11505 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12970 11505 603 41 0 12929 0
vsize: 51880
[startup+640.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11849 0 0 0 63979 29 0 0 25 0 1 0 485898578 53125120 11512 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12970 11512 603 41 0 12929 0
vsize: 51880
[startup+650.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11853 0 0 0 64979 29 0 0 25 0 1 0 485898578 53125120 11516 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12970 11516 603 41 0 12929 0
vsize: 51880
[startup+660.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5208
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11857 0 0 0 65980 29 0 0 25 0 1 0 485898578 53125120 11520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12970 11520 603 41 0 12929 0
vsize: 51880
[startup+670.029 s]
Raw data (loadavg): 1.08 1.02 0.94 2/54 5261
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11861 0 0 0 66980 29 0 0 25 0 1 0 485898578 53125120 11524 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12970 11524 603 41 0 12929 0
vsize: 51880
[startup+680.03 s]
Raw data (loadavg): 1.07 1.02 0.94 2/54 5261
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11866 0 0 0 67980 29 0 0 25 0 1 0 485898578 53260288 11529 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13003 11529 603 41 0 12962 0
vsize: 52012
[startup+690.03 s]
Raw data (loadavg): 1.06 1.01 0.94 2/54 5261
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11870 0 0 0 68980 29 0 0 25 0 1 0 485898578 53260288 11533 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13003 11533 603 41 0 12962 0
vsize: 52012
[startup+700.03 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 5261
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11888 0 0 0 69980 29 0 0 25 0 1 0 485898578 53411840 11551 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13040 11551 603 41 0 12999 0
vsize: 52160
[startup+710.032 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 5261
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11888 0 0 0 70980 29 0 0 25 0 1 0 485898578 53411840 11551 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13040 11551 603 41 0 12999 0
vsize: 52160
[startup+720.031 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 5261
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11889 0 0 0 71980 29 0 0 25 0 1 0 485898578 53411840 11552 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13040 11552 603 41 0 12999 0
vsize: 52160
[startup+730.032 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 5261
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11891 0 0 0 72981 29 0 0 25 0 1 0 485898578 53411840 11554 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13040 11554 603 41 0 12999 0
vsize: 52160
[startup+740.033 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11894 0 0 0 73981 29 0 0 25 0 1 0 485898578 53411840 11557 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13040 11557 603 41 0 12999 0
vsize: 52160
[startup+750.034 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11942 0 0 0 74980 29 0 0 25 0 1 0 485898578 53547008 11605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13073 11605 603 41 0 13032 0
vsize: 52292
[startup+760.035 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11945 0 0 0 75980 29 0 0 25 0 1 0 485898578 53547008 11608 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13073 11608 603 41 0 13032 0
vsize: 52292
[startup+770.035 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11948 0 0 0 76980 29 0 0 25 0 1 0 485898578 53547008 11611 4294967295 134512640 134672761 3221224544 3221223680 134560686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13073 11611 603 41 0 13032 0
vsize: 52292
[startup+780.035 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11952 0 0 0 77980 30 0 0 25 0 1 0 485898578 53547008 11615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13073 11615 603 41 0 13032 0
vsize: 52292
[startup+790.035 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11956 0 0 0 78980 30 0 0 25 0 1 0 485898578 53547008 11619 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13073 11619 603 41 0 13032 0
vsize: 52292
[startup+800.036 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11961 0 0 0 79981 30 0 0 25 0 1 0 485898578 53682176 11624 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13106 11624 603 41 0 13065 0
vsize: 52424
[startup+810.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11966 0 0 0 80981 30 0 0 25 0 1 0 485898578 53682176 11629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13106 11629 603 41 0 13065 0
vsize: 52424
[startup+820.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11968 0 0 0 81981 30 0 0 25 0 1 0 485898578 53682176 11631 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13106 11631 603 41 0 13065 0
vsize: 52424
[startup+830.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11972 0 0 0 82981 30 0 0 25 0 1 0 485898578 53682176 11635 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13106 11635 603 41 0 13065 0
vsize: 52424
[startup+840.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11974 0 0 0 83982 30 0 0 25 0 1 0 485898578 53682176 11637 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13106 11637 603 41 0 13065 0
vsize: 52424
[startup+850.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11978 0 0 0 84982 30 0 0 25 0 1 0 485898578 53682176 11641 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13106 11641 603 41 0 13065 0
vsize: 52424
[startup+860.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11983 0 0 0 85982 30 0 0 25 0 1 0 485898578 53682176 11646 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13106 11646 603 41 0 13065 0
vsize: 52424
[startup+870.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11987 0 0 0 86982 30 0 0 25 0 1 0 485898578 53682176 11650 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13106 11650 603 41 0 13065 0
vsize: 52424
[startup+880.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11990 0 0 0 87982 30 0 0 25 0 1 0 485898578 53682176 11653 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13106 11653 603 41 0 13065 0
vsize: 52424
[startup+890.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11994 0 0 0 88982 30 0 0 25 0 1 0 485898578 53682176 11657 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13106 11657 603 41 0 13065 0
vsize: 52424
[startup+900.042 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11998 0 0 0 89983 30 0 0 25 0 1 0 485898578 53817344 11661 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13139 11661 603 41 0 13098 0
vsize: 52556
[startup+910.043 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 11998 0 0 0 90983 30 0 0 25 0 1 0 485898578 53817344 11661 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13139 11661 603 41 0 13098 0
vsize: 52556
[startup+920.043 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12002 0 0 0 91983 30 0 0 25 0 1 0 485898578 53817344 11665 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13139 11665 603 41 0 13098 0
vsize: 52556
[startup+930.044 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12007 0 0 0 92984 30 0 0 25 0 1 0 485898578 53817344 11670 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13139 11670 603 41 0 13098 0
vsize: 52556
[startup+940.046 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12009 0 0 0 93984 30 0 0 25 0 1 0 485898578 53817344 11672 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13139 11672 603 41 0 13098 0
vsize: 52556
[startup+950.048 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12013 0 0 0 94984 30 0 0 25 0 1 0 485898578 53817344 11676 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13139 11676 603 41 0 13098 0
vsize: 52556
[startup+960.049 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12017 0 0 0 95984 30 0 0 25 0 1 0 485898578 53817344 11680 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13139 11680 603 41 0 13098 0
vsize: 52556
[startup+970.049 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12023 0 0 0 96984 30 0 0 25 0 1 0 485898578 53817344 11686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13139 11686 603 41 0 13098 0
vsize: 52556
[startup+980.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12028 0 0 0 97985 30 0 0 25 0 1 0 485898578 53817344 11691 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13139 11691 603 41 0 13098 0
vsize: 52556
[startup+990.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12033 0 0 0 98985 30 0 0 25 0 1 0 485898578 53952512 11696 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 11696 603 41 0 13131 0
vsize: 52688
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12041 0 0 0 99985 30 0 0 25 0 1 0 485898578 53952512 11704 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 11704 603 41 0 13131 0
vsize: 52688
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12047 0 0 0 100986 30 0 0 25 0 1 0 485898578 53952512 11710 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 11710 603 41 0 13131 0
vsize: 52688
[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12049 0 0 0 101986 30 0 0 25 0 1 0 485898578 53952512 11712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 11712 603 41 0 13131 0
vsize: 52688
[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5263
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12051 0 0 0 102985 30 0 0 25 0 1 0 485898578 53952512 11714 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 11714 603 41 0 13131 0
vsize: 52688
[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12058 0 0 0 103985 30 0 0 25 0 1 0 485898578 53952512 11721 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 11721 603 41 0 13131 0
vsize: 52688
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12063 0 0 0 104986 30 0 0 25 0 1 0 485898578 53952512 11726 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 11726 603 41 0 13131 0
vsize: 52688
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12104 0 0 0 105986 30 0 0 25 0 1 0 485898578 54349824 11767 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11767 603 41 0 13228 0
vsize: 53076
[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12104 0 0 0 106986 30 0 0 25 0 1 0 485898578 54349824 11767 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11767 603 41 0 13228 0
vsize: 53076
[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12105 0 0 0 107986 30 0 0 25 0 1 0 485898578 54349824 11768 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11768 603 41 0 13228 0
vsize: 53076
[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12105 0 0 0 108987 30 0 0 25 0 1 0 485898578 54349824 11768 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11768 603 41 0 13228 0
vsize: 53076
[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12105 0 0 0 109987 30 0 0 25 0 1 0 485898578 54349824 11768 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11768 603 41 0 13228 0
vsize: 53076
[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12105 0 0 0 110987 30 0 0 25 0 1 0 485898578 54349824 11768 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11768 603 41 0 13228 0
vsize: 53076
[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12105 0 0 0 111987 30 0 0 25 0 1 0 485898578 54349824 11768 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11768 603 41 0 13228 0
vsize: 53076
[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12106 0 0 0 112988 30 0 0 25 0 1 0 485898578 54349824 11769 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11769 603 41 0 13228 0
vsize: 53076
[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12107 0 0 0 113988 30 0 0 25 0 1 0 485898578 54349824 11770 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11770 603 41 0 13228 0
vsize: 53076
[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12109 0 0 0 114988 30 0 0 25 0 1 0 485898578 54349824 11772 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11772 603 41 0 13228 0
vsize: 53076
[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12110 0 0 0 115988 30 0 0 25 0 1 0 485898578 54349824 11773 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11773 603 41 0 13228 0
vsize: 53076
[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12113 0 0 0 116988 30 0 0 25 0 1 0 485898578 54349824 11776 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11776 603 41 0 13228 0
vsize: 53076
[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12115 0 0 0 117989 31 0 0 25 0 1 0 485898578 54349824 11778 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11778 603 41 0 13228 0
vsize: 53076
[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12117 0 0 0 118989 31 0 0 25 0 1 0 485898578 54349824 11780 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11780 603 41 0 13228 0
vsize: 53076
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5265
Raw data (stat): 5208 (minisat+) R 5207 5897 5896 0 -1 0 12119 0 0 0 119989 31 0 0 25 0 1 0 485898578 54349824 11782 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13269 11782 603 41 0 13228 0
vsize: 53076
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 5265
Raw data (stat): 5208 (minisat+) Z 5207 5897 5896 0 -1 12 12121 0 0 0 119989 33 0 0 25 0 1 0 485898578 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.09
CPU time (s): 1200.23
CPU user time (s): 1199.9
CPU system time (s): 0.331949
CPU usage (%): 100.011
Max. virtual memory (Kb): 53076
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####