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-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-cracpb1.opb
MD5SUM098fe473d82d5f7d4121673eb775be76
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 22199
Optimality of the best value was proved NO
Number of terms in the objective function 572
Biggest coefficient in the objective function 5000
Number of bits for the biggest coefficient in the objective function 13
Sum of the numbers in the objective function 547769
Number of bits of the sum of numbers in the objective function 20
Biggest number in a constraint 5000
Number of bits of the biggest number in a constraint 13
Biggest sum of numbers in a constraint 547769
Number of bits of the biggest sum of numbers20
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark30.8603
Number of variables572
Total number of constraints716
Number of constraints which are clauses3
Number of constraints which are cardinality constraints (but not clauses)644
Number of constraints which are nor clauses,nor cardinality constraints69
Minimum length of a constraint1
Maximum length of a constraint518

Trace number 19332 

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        838388 kB
Buffers:         15676 kB
Cached:         154024 kB
SwapCached:         28 kB
Active:          57264 kB
Inactive:       115288 kB
HighTotal:      131008 kB
HighFree:        14364 kB
LowTotal:       903652 kB
LowFree:        824024 kB
SwapTotal:     2097892 kB
SwapFree:      2097796 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            18220 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 19:09:39 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 16757 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 215 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #########################################################################################
c   -- Clauses(.)/Splits(s): ...
c ---[ 214]---> Adder-cost: 1416   maxlim: 2733   bits: 12/12
c ---[ 213]---> Sorter-cost:  634     Base:
c ---[ 212]---> Sorter-cost:  238     Base:
c ---[ 211]---> Sorter-cost:  238     Base:
c ---[ 210]---> Sorter-cost:  206     Base:
c ---[ 209]---> Sorter-cost:  356     Base:
c ---[ 208]---> Sorter-cost:  356     Base:
c ---[ 207]---> Sorter-cost:  264     Base:
c ---[ 206]---> Sorter-cost:  126     Base:
c ---[ 205]---> Sorter-cost:  356     Base:
c ---[ 204]---> Sorter-cost:  106     Base:
c ---[ 203]---> BDD-cost:   43
c ---[ 202]---> BDD-cost:   34
c ---[ 201]---> Sorter-cost:  170     Base:
c ---[ 200]---> BDD-cost:   29
c ---[ 199]---> Sorter-cost:  180     Base:
c ---[ 198]---> BDD-cost:   31
c ---[ 197]---> BDD-cost:   21
c ---[ 195]---> Sorter-cost:  561     Base:
c ---[ 193]---> BDD-cost:   41
c ---[ 191]---> Sorter-cost:  255     Base:
c ---[ 189]---> Sorter-cost:  207     Base:
c ---[ 187]---> Sorter-cost:  491     Base:
c ---[ 185]---> Sorter-cost:  239     Base:
c ---[ 183]---> Sorter-cost:  281     Base:
c ---[ 181]---> Sorter-cost:  181     Base:
c ---[ 179]---> Sorter-cost:  291     Base:
c ---[ 177]---> Sorter-cost:  127     Base:
c ---[ 175]---> BDD-cost:   33
c ---[ 173]---> Sorter-cost:  207     Base:
c ---[ 171]---> Sorter-cost:  117     Base:
c ---[ 169]---> Sorter-cost:   77     Base:
c ---[ 167]---> Sorter-cost:  171     Base:
c ---[ 165]---> Sorter-cost:  127     Base:
c ---[ 163]---> BDD-cost:   29
c ---[ 161]---> BDD-cost:   25
c ---[ 159]---> Adder-cost: 155   maxlim: 27   bits: 6/5
c ---[ 157]---> Sorter-cost:  631     Base:
c ---[ 155]---> Sorter-cost:  689     Base:
c ---[ 153]---> Sorter-cost:  609     Base:
c ---[ 151]---> Sorter-cost:  971     Base:
c ---[ 149]---> Sorter-cost:  991     Base:
c ---[ 147]---> Sorter-cost:  755     Base:
c ---[ 145]---> Sorter-cost:  371     Base:
c ---[ 143]---> Sorter-cost:  927     Base:
c ---[ 141]---> Sorter-cost:  355     Base:
c ---[ 139]---> Sorter-cost:  313     Base:
c ---[ 137]---> Sorter-cost:  279     Base:
c ---[ 135]---> Sorter-cost:  501     Base:
c ---[ 133]---> Sorter-cost:  225     Base:
c ---[ 131]---> Sorter-cost:  517     Base:
c ---[ 129]---> Sorter-cost:  197     Base:
c ---[ 127]---> BDD-cost:   66
c ---[ 126]---> Adder-cost: 732   maxlim: 1601   bits: 12/11
c ---[ 125]---> Adder-cost: 1184   maxlim: 406   bits: 10/9
c ---[ 124]---> Adder-cost: 255   maxlim: 863   bits: 11/10
c ---[ 123]---> BDD-cost:   27
c ---[ 122]---> BDD-cost:   35
c ---[ 121]---> Sorter-cost:  172     Base:
c ---[ 120]---> BDD-cost:   31
c ---[ 118]---> BDD-cost:   51
c ---[ 115]---> BDD-cost:   80
c ---[ 114]---> Sorter-cost:  238     Base:
c ---[ 113]---> Sorter-cost:  478     Base:
c ---[ 112]---> Sorter-cost:  254     Base:
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> Sorter-cost:  474     Base:
c ---[ 109]---> BDD-cost:   29
c ---[ 108]---> BDD-cost:   23
c ---[ 106]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:    5
c ---[ 100]---> BDD-cost:   43
c ---[  98]---> BDD-cost:   92
c ---[  96]---> BDD-cost:  183
c ---[  94]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   29
c ---[  90]---> BDD-cost:   29
c ---[  88]---> BDD-cost:   19
c ---[  86]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   31
c ---[  80]---> BDD-cost:   23
c ---[  78]---> BDD-cost:    7
c ---[  76]---> BDD-cost:   13
c ---[  74]---> BDD-cost:   14
c ---[  72]---> BDD-cost:   38
c ---[  70]---> BDD-cost:   23
c ---[  68]---> BDD-cost:   35
c ---[  66]---> BDD-cost:   37
c ---[  64]---> BDD-cost:    7
c ---[  62]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   17
c ---[  58]---> BDD-cost:   43
c ---[  56]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   29
c ---[  52]---> BDD-cost:    7
c ---[  50]---> BDD-cost:   16
c ---[  48]---> BDD-cost:   24
c ---[  46]---> BDD-cost:    5
c ---[  44]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   11
c ---[  40]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   19
c ---[  34]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   19
c ---[  30]---> BDD-cost:   11
c ---[  28]---> BDD-cost:    4
c ---[  26]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   15
c ---[  20]---> BDD-cost:   48
c ---[  18]---> BDD-cost:   51
c ---[  16]---> BDD-cost:   11
c ---[  14]---> BDD-cost:    6
c ---[  12]---> BDD-cost:   51
c ---[  10]---> BDD-cost:    8
c ---[   8]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   43
c ---[   4]---> BDD-cost:   31
c ---[   2]---> BDD-cost:   22
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   67939   195555 |   22646       0        0     nan |  0.000 % |
c |       100 |   67862   195385 |   24910      96     1024    10.7 |  2.636 % |
c |       250 |   67626   194856 |   27401     168     1418     8.4 |  3.012 % |
c |       475 |   67213   193932 |   30141     362     3093     8.5 |  3.698 % |
c |       812 |   67166   193828 |   33156     695    14012    20.2 |  3.772 % |
c |      1318 |   66656   192653 |   36471    1147    23771    20.7 |  4.563 % |
c |      2077 |   66084   191337 |   40118    1847    30811    16.7 |  5.422 % |
c |      3216 |   65666   190398 |   44130    2926    85116    29.1 |  6.126 % |
c |      4924 |   65289   189510 |   48543    4602   161836    35.2 |  6.697 % |
c |      7486 |   64879   188564 |   53398    7110   452576    63.7 |  7.372 % |
c |     11330 |   64473   187562 |   58737   10913   683305    62.6 |  7.983 % |
c |     17096 |   63798   186003 |   64611   16614  1038263    62.5 |  9.074 % |
c |     25745 |   63601   185525 |   71072   25238  1695999    67.2 |  9.379 % |
c |     38720 |   63580   185480 |   78180   38210  2907699    76.1 |  9.414 % |
c |     58183 |   63250   184652 |   85998   57643  5496284    95.4 |  9.904 % |
c |     87378 |   63094   184239 |   94597   86809  9124448   105.1 | 10.123 % |
c |    131168 |   62940   183865 |  104057   49841  5416549   108.7 | 10.354 % |
c |    196852 |   62652   183106 |  114463   24518  1690817    69.0 | 10.741 % |
c |    295380 |   62156   181879 |  125909   22629  1840136    81.3 | 11.502 % |
#### 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 23382
Raw data (stat): 23382 (runsolver) R 23381 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547365419 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.96 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 2385 0 0 0 992 6 0 0 25 0 1 0 547365419 12300288 2305 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3003 2305 603 41 0 2962 0
vsize: 12012
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.96 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 2947 0 0 0 1990 8 0 0 25 0 1 0 547365419 14626816 2867 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3571 2867 603 41 0 3530 0
vsize: 14284
[startup+30.001 s]
Raw data (loadavg): 0.95 0.96 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 3361 0 0 0 2989 10 0 0 25 0 1 0 547365419 16379904 3281 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3281 603 41 0 3958 0
vsize: 15996
[startup+40.0006 s]
Raw data (loadavg): 0.95 0.96 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 3778 0 0 0 3987 11 0 0 25 0 1 0 547365419 17993728 3698 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3698 603 41 0 4352 0
vsize: 17572
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.96 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 4197 0 0 0 4986 12 0 0 25 0 1 0 547365419 19734528 4117 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4818 4117 603 41 0 4777 0
vsize: 19272
[startup+60.0028 s]
Raw data (loadavg): 0.97 0.96 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 4781 0 0 0 5985 14 0 0 25 0 1 0 547365419 22024192 4701 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5377 4701 603 41 0 5336 0
vsize: 21508
[startup+70.0029 s]
Raw data (loadavg): 0.97 0.96 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 5339 0 0 0 6984 15 0 0 25 0 1 0 547365419 24432640 5259 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5965 5259 603 41 0 5924 0
vsize: 23860
[startup+80.004 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 5645 0 0 0 7983 16 0 0 25 0 1 0 547365419 25767936 5565 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6291 5565 603 41 0 6250 0
vsize: 25164
[startup+90.0038 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 6141 0 0 0 8982 17 0 0 25 0 1 0 547365419 27787264 6061 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6784 6061 603 41 0 6743 0
vsize: 27136
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 6902 0 0 0 9981 19 0 0 25 0 1 0 547365419 30887936 6822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7541 6822 603 41 0 7500 0
vsize: 30164
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 7476 0 0 0 10980 20 0 0 25 0 1 0 547365419 33169408 7396 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8098 7396 603 41 0 8057 0
vsize: 32392
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 8124 0 0 0 11977 22 0 0 25 0 1 0 547365419 35864576 8044 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8756 8044 603 41 0 8715 0
vsize: 35024
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 8570 0 0 0 12976 24 0 0 25 0 1 0 547365419 37613568 8490 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9183 8490 603 41 0 9142 0
vsize: 36732
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 8915 0 0 0 13975 25 0 0 25 0 1 0 547365419 38957056 8835 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9511 8835 603 41 0 9470 0
vsize: 38044
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 9282 0 0 0 14974 26 0 0 25 0 1 0 547365419 40837120 9202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9970 9202 603 41 0 9929 0
vsize: 39880
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 9753 0 0 0 15973 27 0 0 25 0 1 0 547365419 42713088 9673 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10428 9673 603 41 0 10387 0
vsize: 41712
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 10261 0 0 0 16972 28 0 0 25 0 1 0 547365419 44724224 10181 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10919 10181 603 41 0 10878 0
vsize: 43676
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 10592 0 0 0 17971 30 0 0 25 0 1 0 547365419 46063616 10512 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11246 10512 603 41 0 11205 0
vsize: 44984
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 11049 0 0 0 18970 31 0 0 25 0 1 0 547365419 47947776 10969 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11706 10969 603 41 0 11665 0
vsize: 46824
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 11512 0 0 0 19969 32 0 0 25 0 1 0 547365419 49823744 11432 4294967295 134512640 134672761 3221224544 3221223648 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12164 11432 603 41 0 12123 0
vsize: 48656
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 11970 0 0 0 20968 34 0 0 25 0 1 0 547365419 51703808 11890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12623 11890 603 41 0 12582 0
vsize: 50492
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 12309 0 0 0 21966 35 0 0 25 0 1 0 547365419 53047296 12229 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12951 12229 603 41 0 12910 0
vsize: 51804
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 12675 0 0 0 22965 36 0 0 25 0 1 0 547365419 54517760 12595 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13310 12595 603 41 0 13269 0
vsize: 53240
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13121 0 0 0 23963 38 0 0 25 0 1 0 547365419 56393728 13041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13768 13041 603 41 0 13727 0
vsize: 55072
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13578 0 0 0 24962 40 0 0 25 0 1 0 547365419 58277888 13498 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13498 603 41 0 14187 0
vsize: 56912
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 25962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223752 1075346913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 26962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 27962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223696 134559753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 28962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 29962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 30962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 31963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 32962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 33963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 34963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 35963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 36963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 37963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 38963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 39964 41 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 40964 41 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 41964 41 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13517 603 41 0 14187 0
vsize: 56912
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13599 0 0 0 42964 41 0 0 25 0 1 0 547365419 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13519 603 41 0 14187 0
vsize: 56912
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13599 0 0 0 43964 41 0 0 25 0 1 0 547365419 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13519 603 41 0 14187 0
vsize: 56912
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13599 0 0 0 44965 41 0 0 25 0 1 0 547365419 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13519 603 41 0 14187 0
vsize: 56912
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13599 0 0 0 45965 41 0 0 25 0 1 0 547365419 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13519 603 41 0 14187 0
vsize: 56912
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13599 0 0 0 46965 41 0 0 25 0 1 0 547365419 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 13519 603 41 0 14187 0
vsize: 56912
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13666 0 0 0 47965 41 0 0 25 0 1 0 547365419 58548224 13586 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13586 603 41 0 14253 0
vsize: 57176
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14058 0 0 0 48964 42 0 0 25 0 1 0 547365419 60157952 13978 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14687 13978 603 41 0 14646 0
vsize: 58748
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14365 0 0 0 49963 43 0 0 25 0 1 0 547365419 61370368 14285 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14983 14285 603 41 0 14942 0
vsize: 59932
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 50963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 51962 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 52962 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 53962 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 54963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 55963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 56963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 57963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 58963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 59964 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 60964 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 23382
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 61964 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+630.017 s]
Raw data (loadavg): 1.23 1.02 0.96 3/57 23421
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 62963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+640.017 s]
Raw data (loadavg): 1.20 1.02 0.96 2/54 23435
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 63963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+650.018 s]
Raw data (loadavg): 1.17 1.02 0.96 2/54 23435
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 64963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+660.018 s]
Raw data (loadavg): 1.14 1.02 0.96 2/54 23435
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 65963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+670.018 s]
Raw data (loadavg): 1.12 1.02 0.96 2/54 23435
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 66963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+680.018 s]
Raw data (loadavg): 1.10 1.02 0.96 2/54 23435
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 67963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+690.018 s]
Raw data (loadavg): 1.08 1.01 0.96 2/54 23435
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 68963 46 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+700.019 s]
Raw data (loadavg): 1.07 1.01 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 69963 46 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+710.019 s]
Raw data (loadavg): 1.06 1.01 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 70963 47 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+720.02 s]
Raw data (loadavg): 1.05 1.01 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 71962 47 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+730.02 s]
Raw data (loadavg): 1.04 1.01 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 72962 48 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+740.021 s]
Raw data (loadavg): 1.04 1.01 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 73962 48 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+750.022 s]
Raw data (loadavg): 1.03 1.01 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 74962 48 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+760.022 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 75961 48 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14507 603 41 0 15172 0
vsize: 60852
[startup+770.023 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14589 0 0 0 76961 49 0 0 25 0 1 0 547365419 62312448 14509 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14509 603 41 0 15172 0
vsize: 60852
[startup+780.023 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14591 0 0 0 77961 49 0 0 25 0 1 0 547365419 62312448 14511 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15213 14511 603 41 0 15172 0
vsize: 60852
[startup+790.023 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14679 0 0 0 78961 49 0 0 25 0 1 0 547365419 62713856 14599 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15311 14599 603 41 0 15270 0
vsize: 61244
[startup+800.024 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14945 0 0 0 79960 50 0 0 25 0 1 0 547365419 63782912 14865 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15572 14865 603 41 0 15531 0
vsize: 62288
[startup+810.025 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 80959 52 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+820.024 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 81958 52 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+830.025 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 82958 52 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+840.025 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 83958 53 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+850.026 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 84958 53 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+860.026 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 85958 53 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+870.027 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 86957 54 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223676 1075347104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+880.027 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 87957 55 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+890.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 88957 55 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+900.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 89957 55 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+910.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 90956 56 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+920.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 91956 56 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+930.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 92956 56 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+940.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 93956 56 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+950.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 94956 56 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+960.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23437
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 95956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+970.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 96956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+980.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 97956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+990.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 98956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 99956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 100956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 101957 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 102957 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223600 134565132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 103957 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15709 14988 603 41 0 15668 0
vsize: 62836
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15368 0 0 0 104956 58 0 0 25 0 1 0 547365419 65568768 15288 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16008 15288 603 41 0 15967 0
vsize: 64032
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15739 0 0 0 105956 58 0 0 25 0 1 0 547365419 67072000 15659 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16375 15659 603 41 0 16334 0
vsize: 65500
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 16092 0 0 0 106955 59 0 0 25 0 1 0 547365419 68554752 16012 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16737 16012 603 41 0 16696 0
vsize: 66948
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 16441 0 0 0 107955 60 0 0 25 0 1 0 547365419 69906432 16361 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17067 16361 603 41 0 17026 0
vsize: 68268
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 16786 0 0 0 108953 62 0 0 25 0 1 0 547365419 71438336 16706 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17441 16706 603 41 0 17400 0
vsize: 69764
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 17147 0 0 0 109952 63 0 0 25 0 1 0 547365419 72925184 17067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17804 17067 603 41 0 17763 0
vsize: 71216
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 17518 0 0 0 110951 64 0 0 25 0 1 0 547365419 74407936 17438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18166 17438 603 41 0 18125 0
vsize: 72664
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 17917 0 0 0 111950 65 0 0 25 0 1 0 547365419 76017664 17837 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18559 17837 603 41 0 18518 0
vsize: 74236
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 18275 0 0 0 112950 66 0 0 25 0 1 0 547365419 77492224 18195 4294967295 134512640 134672761 3221224544 3221223648 134560070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18919 18195 603 41 0 18878 0
vsize: 75676
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 18607 0 0 0 113949 67 0 0 25 0 1 0 547365419 78831616 18527 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19246 18527 603 41 0 19205 0
vsize: 76984
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 18925 0 0 0 114949 68 0 0 25 0 1 0 547365419 80166912 18845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19572 18845 603 41 0 19531 0
vsize: 78288
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 19276 0 0 0 115947 69 0 0 25 0 1 0 547365419 81649664 19196 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19934 19196 603 41 0 19893 0
vsize: 79736
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 19631 0 0 0 116946 71 0 0 25 0 1 0 547365419 83173376 19551 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20306 19551 603 41 0 20265 0
vsize: 81224
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 19999 0 0 0 117945 71 0 0 25 0 1 0 547365419 84652032 19919 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20667 19919 603 41 0 20626 0
vsize: 82668
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 20342 0 0 0 118945 72 0 0 25 0 1 0 547365419 85991424 20262 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20994 20262 603 41 0 20953 0
vsize: 83976
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 23439
Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 20601 0 0 0 119944 73 0 0 25 0 1 0 547365419 87064576 20521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21256 20521 603 41 0 21215 0
vsize: 85024
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 23439
Raw data (stat): 23382 (minisat+) Z 23381 11931 11930 0 -1 12 20603 0 0 0 119944 76 0 0 25 0 1 0 547365419 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.08
CPU time (s): 1200.22
CPU user time (s): 1199.45
CPU system time (s): 0.768883
CPU usage (%): 100.012
Max. virtual memory (Kb): 85024
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####