PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-l152lav.opb
MD5SUM	00855a9538cee8df79108d56ee6867b4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5046
Optimality of the best value was proved	NO
Number of terms in the objective function	1989
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	382524
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	268
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	382524
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.28
Number of variables	1989
Total number of constraints	2086
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2085
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1989
Trace number 22297

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-22 02:39:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11906 boxname=wulflinc4 idbench=916 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00855a9538cee8df79108d56ee6867b4  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-l152lav.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-l152lav.opb /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-l152lav.opb
IDLAUNCH: 11906
/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:        761772 kB
Buffers:         18124 kB
Cached:         234472 kB
SwapCached:        364 kB
Active:          27044 kB
Inactive:       227772 kB
HighTotal:      131008 kB
HighFree:         1316 kB
LowTotal:       903652 kB
LowFree:        760456 kB
SwapTotal:     2097136 kB
SwapFree:      2096008 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            12524 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:59:05 (client local time) WITH STATUS 0 IN 1200.35 SECONDS
stats: 11906 7 1200.35 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 192]---> Adder-cost: 5478   maxlim: 25152   bits: 15/15
c ---[ 190]---> BDD-cost:    3
c ---[ 188]---> BDD-cost:  255
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:   83
c ---[ 182]---> BDD-cost:   93
c ---[ 180]---> BDD-cost:  149
c ---[ 178]---> BDD-cost:  235
c ---[ 176]---> BDD-cost:  339
c ---[ 174]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:  301
c ---[ 168]---> BDD-cost:  181
c ---[ 166]---> BDD-cost:   87
c ---[ 164]---> BDD-cost:   71
c ---[ 162]---> BDD-cost:   67
c ---[ 160]---> BDD-cost:   57
c ---[ 158]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:   39
c ---[ 154]---> BDD-cost:   85
c ---[ 152]---> BDD-cost:  147
c ---[ 150]---> BDD-cost:  189
c ---[ 148]---> BDD-cost:  211
c ---[ 146]---> BDD-cost:   95
c ---[ 144]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   35
c ---[ 140]---> BDD-cost:   59
c ---[ 138]---> BDD-cost:  171
c ---[ 136]---> BDD-cost:   59
c ---[ 134]---> BDD-cost:   51
c ---[ 132]---> BDD-cost:  151
c ---[ 130]---> BDD-cost:  147
c ---[ 128]---> BDD-cost:  317
c ---[ 126]---> BDD-cost:  201
c ---[ 124]---> BDD-cost:  105
c ---[ 122]---> BDD-cost:  101
c ---[ 120]---> BDD-cost:  121
c ---[ 118]---> BDD-cost:  133
c ---[ 116]---> BDD-cost:  149
c ---[ 114]---> BDD-cost:  189
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:  201
c ---[ 108]---> BDD-cost:   49
c ---[ 106]---> BDD-cost:   81
c ---[ 104]---> BDD-cost:  121
c ---[ 102]---> BDD-cost:  433
c ---[ 100]---> BDD-cost:  191
c ---[  98]---> BDD-cost:   81
c ---[  96]---> BDD-cost:   71
c ---[  94]---> BDD-cost:  103
c ---[  92]---> BDD-cost:   93
c ---[  90]---> BDD-cost:   85
c ---[  88]---> BDD-cost:  189
c ---[  86]---> BDD-cost:  231
c ---[  84]---> BDD-cost:  101
c ---[  82]---> BDD-cost:  109
c ---[  80]---> BDD-cost:  171
c ---[  78]---> BDD-cost:  183
c ---[  76]---> BDD-cost:  173
c ---[  74]---> BDD-cost:  239
c ---[  72]---> BDD-cost:   91
c ---[  70]---> BDD-cost:  271
c ---[  68]---> BDD-cost:  239
c ---[  66]---> BDD-cost:  105
c ---[  64]---> BDD-cost:  117
c ---[  62]---> BDD-cost:  221
c ---[  60]---> BDD-cost:  213
c ---[  58]---> BDD-cost:  145
c ---[  56]---> BDD-cost:  179
c ---[  54]---> BDD-cost:  213
c ---[  52]---> BDD-cost:  143
c ---[  50]---> BDD-cost:  209
c ---[  48]---> BDD-cost:   81
c ---[  46]---> BDD-cost:  205
c ---[  44]---> BDD-cost:   61
c ---[  42]---> BDD-cost:  225
c ---[  40]---> BDD-cost:  129
c ---[  38]---> BDD-cost:  253
c ---[  36]---> BDD-cost:   71
c ---[  34]---> BDD-cost:  203
c ---[  32]---> BDD-cost:   45
c ---[  30]---> BDD-cost:  133
c ---[  28]---> BDD-cost:  323
c ---[  26]---> BDD-cost:  155
c ---[  24]---> BDD-cost:   89
c ---[  22]---> BDD-cost:   93
c ---[  20]---> BDD-cost:   83
c ---[  18]---> BDD-cost:   67
c ---[  16]---> BDD-cost:  133
c ---[  14]---> BDD-cost:  247
c ---[  12]---> BDD-cost:   97
c ---[  10]---> BDD-cost:   97
c ---[   8]---> BDD-cost:  151
c ---[   6]---> BDD-cost:  181
c ---[   4]---> BDD-cost:  151
c ---[   2]---> BDD-cost:  181
c ---[   0]---> Adder-cost: 3598   maxlim: 1961   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   97126   314221 |   29137       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24129          
c   -- var.elim.:  2000/24129          
c   -- var.elim.:  3000/24129          
c   -- var.elim.:  4000/24129          
c   -- var.elim.:  5000/24129          
c   -- var.elim.:  6000/24129          
c   -- var.elim.:  7000/24129          
c   -- var.eli#### 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.91 2/54 21591
Raw data (stat): 21591 (runsolver) R 21590 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491959489 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 6475 0 0 0 983 15 0 0 25 0 1 0 491959489 27369472 5574 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6682 5574 603 41 0 6641 0
vsize: 26728
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 6860 0 0 0 1982 17 0 0 25 0 1 0 491959489 28954624 5959 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7069 5959 603 41 0 7028 0
vsize: 28276
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 7312 0 0 0 2980 18 0 0 25 0 1 0 491959489 30822400 6411 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7525 6411 603 41 0 7484 0
vsize: 30100
[startup+40.0029 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 7866 0 0 0 3979 20 0 0 25 0 1 0 491959489 33058816 6965 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8071 6965 603 41 0 8030 0
vsize: 32284
[startup+50.0035 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 8474 0 0 0 4978 21 0 0 25 0 1 0 491959489 35565568 7573 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8683 7573 603 41 0 8642 0
vsize: 34732
[startup+60.0036 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 9216 0 0 0 5976 23 0 0 25 0 1 0 491959489 38572032 8315 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9417 8315 603 41 0 9376 0
vsize: 37668
[startup+70.0042 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 10049 0 0 0 6974 26 0 0 25 0 1 0 491959489 41992192 9148 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10252 9148 603 41 0 10211 0
vsize: 41008
[startup+80.0051 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 11810 0 0 0 7968 31 0 0 25 0 1 0 491959489 49348608 10909 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12048 10909 603 41 0 12007 0
vsize: 48192
[startup+90.0052 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 12452 0 0 0 8966 34 0 0 25 0 1 0 491959489 51859456 11551 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12661 11551 603 41 0 12620 0
vsize: 50644
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 13319 0 0 0 9964 36 0 0 25 0 1 0 491959489 55406592 12418 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13527 12418 603 41 0 13486 0
vsize: 54108
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 14214 0 0 0 10962 39 0 0 25 0 1 0 491959489 59133952 13313 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14437 13313 603 41 0 14396 0
vsize: 57748
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 14675 0 0 0 11961 40 0 0 25 0 1 0 491959489 60997632 13774 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14892 13774 603 41 0 14851 0
vsize: 59568
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 16109 0 0 0 12958 43 0 0 25 0 1 0 491959489 66793472 15208 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16307 15208 603 41 0 16266 0
vsize: 65228
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 17248 0 0 0 13956 45 0 0 25 0 1 0 491959489 71528448 16347 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17463 16347 603 41 0 17422 0
vsize: 69852
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 18259 0 0 0 14954 46 0 0 25 0 1 0 491959489 75599872 17358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18457 17358 603 41 0 18416 0
vsize: 73828
[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 19445 0 0 0 15952 49 0 0 25 0 1 0 491959489 80482304 18544 4294967295 134512640 134672761 3221224544 3221223584 134614268 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19649 18544 603 41 0 19608 0
vsize: 78596
[startup+170.013 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 20454 0 0 0 16949 52 0 0 25 0 1 0 491959489 84545536 19553 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20641 19553 603 41 0 20600 0
vsize: 82564
[startup+180.013 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 21597 0 0 0 17946 56 0 0 25 0 1 0 491959489 89546752 20696 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21862 20696 603 41 0 21821 0
vsize: 87448
[startup+190.013 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 22844 0 0 0 18943 60 0 0 25 0 1 0 491959489 94560256 21943 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23086 21943 603 41 0 23045 0
vsize: 92344
[startup+200.013 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 23836 0 0 0 19939 63 0 0 25 0 1 0 491959489 98643968 22935 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24083 22935 603 41 0 24042 0
vsize: 96332
[startup+210.014 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 24861 0 0 0 20937 65 0 0 25 0 1 0 491959489 102858752 23960 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25112 23960 603 41 0 25071 0
vsize: 100448
[startup+220.014 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 26723 0 0 0 21932 71 0 0 25 0 1 0 491959489 110497792 25822 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26977 25822 603 41 0 26936 0
vsize: 107908
[startup+230.014 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 27742 0 0 0 22930 73 0 0 25 0 1 0 491959489 114634752 26841 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27987 26841 603 41 0 27946 0
vsize: 111948
[startup+240.014 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 28630 0 0 0 23928 75 0 0 25 0 1 0 491959489 118304768 27729 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28883 27729 603 41 0 28842 0
vsize: 115532
[startup+250.014 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 29718 0 0 0 24924 79 0 0 25 0 1 0 491959489 122650624 28817 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29944 28817 603 41 0 29903 0
vsize: 119776
[startup+260.015 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 30951 0 0 0 25922 82 0 0 25 0 1 0 491959489 127692800 30050 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31175 30050 603 41 0 31134 0
vsize: 124700
[startup+270.015 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 31857 0 0 0 26919 84 0 0 25 0 1 0 491959489 131379200 30956 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32075 30956 603 41 0 32034 0
vsize: 128300
[startup+280.015 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 32703 0 0 0 27917 87 0 0 25 0 1 0 491959489 134946816 31802 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32946 31802 603 41 0 32905 0
vsize: 131784
[startup+290.015 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 33763 0 0 0 28914 90 0 0 25 0 1 0 491959489 139276288 32862 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34003 32862 603 41 0 33962 0
vsize: 136012
[startup+300.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 34522 0 0 0 29911 93 0 0 25 0 1 0 491959489 142307328 33621 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34743 33621 603 41 0 34702 0
vsize: 138972
[startup+310.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 35518 0 0 0 30909 95 0 0 25 0 1 0 491959489 146399232 34617 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35742 34617 603 41 0 35701 0
vsize: 142968
[startup+320.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 36620 0 0 0 31907 98 0 0 25 0 1 0 491959489 150884352 35719 4294967295 134512640 134672761 3221224544 3221223680 134614710 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36837 35719 603 41 0 36796 0
vsize: 147348
[startup+330.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 37459 0 0 0 32905 100 0 0 25 0 1 0 491959489 154284032 36558 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37667 36558 603 41 0 37626 0
vsize: 150668
[startup+340.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 38483 0 0 0 33903 102 0 0 25 0 1 0 491959489 158519296 37582 4294967295 134512640 134672761 3221224544 3221223584 134614348 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 37582 603 41 0 38660 0
vsize: 154804
[startup+350.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 39436 0 0 0 34901 105 0 0 25 0 1 0 491959489 162459648 38535 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39663 38535 603 41 0 39622 0
vsize: 158652
[startup+360.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 40585 0 0 0 35899 107 0 0 25 0 1 0 491959489 167165952 39684 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40812 39684 603 41 0 40771 0
vsize: 163248
[startup+370.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 41438 0 0 0 36897 108 0 0 25 0 1 0 491959489 170553344 40537 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41639 40537 603 41 0 41598 0
vsize: 166556
[startup+380.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 42042 0 0 0 37896 109 0 0 25 0 1 0 491959489 173027328 41141 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42243 41141 603 41 0 42202 0
vsize: 168972
[startup+390.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 42792 0 0 0 38896 110 0 0 25 0 1 0 491959489 176181248 41891 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43013 41891 603 41 0 42972 0
vsize: 172052
[startup+400.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 43120 0 0 0 39895 111 0 0 25 0 1 0 491959489 177508352 42219 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43337 42219 603 41 0 43296 0
vsize: 173348
[startup+410.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 43615 0 0 0 40893 113 0 0 25 0 1 0 491959489 179486720 42714 4294967295 134512640 134672761 3221224544 3221223688 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43820 42714 603 41 0 43779 0
vsize: 175280
[startup+420.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 43972 0 0 0 41892 114 0 0 25 0 1 0 491959489 180944896 43071 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44176 43071 603 41 0 44135 0
vsize: 176704
[startup+430.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 44390 0 0 0 42890 116 0 0 25 0 1 0 491959489 182640640 43489 4294967295 134512640 134672761 3221224544 3221223688 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44590 43489 603 41 0 44549 0
vsize: 178360
[startup+440.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 44931 0 0 0 43888 118 0 0 25 0 1 0 491959489 184885248 44030 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45138 44030 603 41 0 45097 0
vsize: 180552
[startup+450.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 45804 0 0 0 44886 120 0 0 25 0 1 0 491959489 188465152 44903 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46012 44903 603 41 0 45971 0
vsize: 184048
[startup+460.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 46717 0 0 0 45884 122 0 0 25 0 1 0 491959489 192126976 45816 4294967295 134512640 134672761 3221224544 3221223688 134616178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46906 45816 603 41 0 46865 0
vsize: 187624
[startup+470.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 47209 0 0 0 46884 123 0 0 25 0 1 0 491959489 194646016 46308 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47521 46308 603 41 0 47480 0
vsize: 190084
[startup+480.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 47955 0 0 0 47882 125 0 0 25 0 1 0 491959489 197775360 47054 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48285 47054 603 41 0 48244 0
vsize: 193140
[startup+490.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 48360 0 0 0 48881 126 0 0 25 0 1 0 491959489 199348224 47459 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48669 47459 603 41 0 48628 0
vsize: 194676
[startup+500.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 49112 0 0 0 49880 127 0 0 25 0 1 0 491959489 202506240 48211 4294967295 134512640 134672761 3221224544 3221223416 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49440 48212 603 41 0 49399 0
vsize: 197760
[startup+510.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 49841 0 0 0 50879 129 0 0 25 0 1 0 491959489 205418496 48940 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50151 48940 603 41 0 50110 0
vsize: 200604
[startup+520.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 50919 0 0 0 51876 132 0 0 25 0 1 0 491959489 209879040 50018 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51240 50018 603 41 0 51199 0
vsize: 204960
[startup+530.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 51608 0 0 0 52874 134 0 0 25 0 1 0 491959489 212672512 50707 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51922 50707 603 41 0 51881 0
vsize: 207688
[startup+540.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 52358 0 0 0 53873 136 0 0 25 0 1 0 491959489 215691264 51457 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52659 51457 603 41 0 52618 0
vsize: 210636
[startup+550.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 53014 0 0 0 54871 138 0 0 25 0 1 0 491959489 218439680 52113 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53330 52113 603 41 0 53289 0
vsize: 213320
[startup+560.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 53650 0 0 0 55870 139 0 0 25 0 1 0 491959489 220946432 52749 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53942 52749 603 41 0 53901 0
vsize: 215768
[startup+570.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 54563 0 0 0 56868 142 0 0 25 0 1 0 491959489 224739328 53662 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54868 53662 603 41 0 54827 0
vsize: 219472
[startup+580.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 55868 0 0 0 57865 144 0 0 25 0 1 0 491959489 230031360 54967 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56160 54967 603 41 0 56119 0
vsize: 224640
[startup+590.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 56666 0 0 0 58864 146 0 0 25 0 1 0 491959489 233295872 55765 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56957 55765 603 41 0 56916 0
vsize: 227828
[startup+600.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 57432 0 0 0 59862 148 0 0 25 0 1 0 491959489 236449792 56531 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57727 56531 603 41 0 57686 0
vsize: 230908
[startup+610.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 57999 0 0 0 60860 150 0 0 25 0 1 0 491959489 238833664 57098 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58309 57098 603 41 0 58268 0
vsize: 233236
[startup+620.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 58795 0 0 0 61858 152 0 0 25 0 1 0 491959489 242003968 57894 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59083 57894 603 41 0 59042 0
vsize: 236332
[startup+630.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 59686 0 0 0 62856 154 0 0 25 0 1 0 491959489 245653504 58785 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59974 58785 603 41 0 59933 0
vsize: 239896
[startup+640.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 60469 0 0 0 63854 156 0 0 25 0 1 0 491959489 248815616 59568 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60746 59568 603 41 0 60705 0
vsize: 242984
[startup+650.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 61259 0 0 0 64853 158 0 0 25 0 1 0 491959489 252116992 60358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61552 60358 603 41 0 61511 0
vsize: 246208
[startup+660.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 61990 0 0 0 65850 161 0 0 25 0 1 0 491959489 255135744 61089 4294967295 134512640 134672761 3221224544 3221223728 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62289 61089 603 41 0 62248 0
vsize: 249156
[startup+670.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 62806 0 0 0 66849 163 0 0 25 0 1 0 491959489 258428928 61905 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63093 61905 603 41 0 63052 0
vsize: 252372
[startup+680.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 63640 0 0 0 67847 164 0 0 25 0 1 0 491959489 261832704 62739 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63924 62739 603 41 0 63883 0
vsize: 255696
[startup+690.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 64528 0 0 0 68846 166 0 0 25 0 1 0 491959489 265515008 63627 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64823 63627 603 41 0 64782 0
vsize: 259292
[startup+700.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 65616 0 0 0 69843 169 0 0 25 0 1 0 491959489 269959168 64715 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65908 64715 603 41 0 65867 0
vsize: 263632
[startup+710.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 66327 0 0 0 70840 172 0 0 25 0 1 0 491959489 272867328 65426 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66618 65426 603 41 0 66577 0
vsize: 266472
[startup+720.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 67171 0 0 0 71838 174 0 0 25 0 1 0 491959489 276262912 66270 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67447 66270 603 41 0 67406 0
vsize: 269788
[startup+730.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 68057 0 0 0 72836 176 0 0 25 0 1 0 491959489 279896064 67156 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68334 67156 603 41 0 68293 0
vsize: 273336
[startup+740.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 69244 0 0 0 73834 179 0 0 25 0 1 0 491959489 284725248 68343 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69513 68343 603 41 0 69472 0
vsize: 278052
[startup+750.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 70391 0 0 0 74831 182 0 0 25 0 1 0 491959489 289460224 69490 4294967295 134512640 134672761 3221224544 3221223728 134615514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70669 69490 603 41 0 70628 0
vsize: 282676
[startup+760.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 71419 0 0 0 75829 184 0 0 25 0 1 0 491959489 293629952 70518 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71687 70518 603 41 0 71646 0
vsize: 286748
[startup+770.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 72714 0 0 0 76825 188 0 0 25 0 1 0 491959489 299008000 71813 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73000 71813 603 41 0 72959 0
vsize: 292000
[startup+780.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 73651 0 0 0 77823 190 0 0 25 0 1 0 491959489 302829568 72750 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73933 72750 603 41 0 73892 0
vsize: 295732
[startup+790.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 74928 0 0 0 78822 192 0 0 25 0 1 0 491959489 308064256 74027 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75211 74027 603 41 0 75170 0
vsize: 300844
[startup+800.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76133 0 0 0 79818 195 0 0 25 0 1 0 491959489 312975360 75232 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76410 75232 603 41 0 76369 0
vsize: 305640
[startup+810.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 80816 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+820.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 81816 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+830.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 82816 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+840.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 83817 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+850.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 84817 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+860.035 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 85817 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+870.035 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 86817 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+880.035 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 87817 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+890.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 88817 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+900.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 89817 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+910.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 90817 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+920.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 91818 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+930.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 92818 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+940.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 93818 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+950.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 94818 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+960.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 95818 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+970.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 96818 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+980.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 97819 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+990.039 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 98819 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 99819 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 100819 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 101819 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 102820 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 103820 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 104820 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134616005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 105820 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 106820 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 107820 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 108821 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 109821 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 110821 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 111821 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 112821 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 113821 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 114822 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 115822 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 116822 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 117822 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 118822 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21591
Raw data (stat): 21591 (minisat+) R 21590 5897 5896 0 -1 0 76845 0 0 0 119822 198 0 0 25 0 1 0 491959489 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 21591
Raw data (stat): 21591 (minisat+) Z 21590 5897 5896 0 -1 12 76845 0 0 0 119823 212 0 0 25 0 1 0 491959489 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.18
CPU time (s): 1200.35
CPU user time (s): 1198.23
CPU system time (s): 2.12268
CPU usage (%): 100.014
Max. virtual memory (Kb): 308016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####