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/miplib3/normalized-mps-v2-13-7-p0548.opb
MD5SUM10547c6c0f11ab5df74fcaff6ba6d160
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 14938
Optimality of the best value was proved NO
Number of terms in the objective function 416
Biggest coefficient in the objective function 11000
Number of bits for the biggest coefficient in the objective function 14
Sum of the numbers in the objective function 96797
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 11000
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 96797
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1244.18
Number of variables548
Total number of constraints724
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)550
Number of constraints which are nor clauses,nor cardinality constraints134
Minimum length of a constraint1
Maximum length of a constraint143

Trace number 18000 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-21 13:04:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18725 boxname=wulflinc26 idbench=1441 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  10547c6c0f11ab5df74fcaff6ba6d160  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-p0548.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-p0548.opb
IDLAUNCH: 18725
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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:        534528 kB
Buffers:         29200 kB
Cached:         440340 kB
SwapCached:         68 kB
Active:          55888 kB
Inactive:       416540 kB
HighTotal:      131008 kB
HighFree:          308 kB
LowTotal:       903652 kB
LowFree:        534220 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6876 kB
Slab:            21968 kB
Committed_AS:    63712 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:24:18 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 18725 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 156 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssss.s..ssss........................................
c ---[ 164]---> BDD-cost:   12
c ---[ 163]---> BDD-cost:   46
c ---[ 162]---> BDD-cost:   27
c ---[ 161]---> BDD-cost:    8
c ---[ 160]---> BDD-cost:   48
c ---[ 159]---> BDD-cost:    7
c ---[ 157]---> BDD-cost:   75
c ---[ 156]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   54
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:  105
c ---[ 151]---> BDD-cost:  104
c ---[ 150]---> BDD-cost:  120
c ---[ 149]---> BDD-cost:   79
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:  115
c ---[ 146]---> BDD-cost:  107
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:   55
c ---[ 143]---> BDD-cost:   87
c ---[ 142]---> BDD-cost:   54
c ---[ 141]---> BDD-cost:  164
c ---[ 140]---> BDD-cost:  151
c ---[ 139]---> BDD-cost:   31
c ---[ 138]---> BDD-cost:   26
c ---[ 136]---> BDD-cost:   28
c ---[ 135]---> BDD-cost:   77
c ---[ 134]---> BDD-cost:  153
c ---[ 133]---> BDD-cost:  109
c ---[ 131]---> BDD-cost:  137
c ---[ 130]---> BDD-cost:    6
c ---[ 129]---> BDD-cost:   56
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:    7
c ---[ 126]---> BDD-cost:   32
c ---[ 125]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   14
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:   19
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:   24
c ---[ 116]---> BDD-cost:   11
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:   29
c ---[ 112]---> BDD-cost:    6
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> BDD-cost:   29
c ---[ 109]---> BDD-cost:   51
c ---[ 107]---> BDD-cost:    8
c ---[ 106]---> BDD-cost:   35
c ---[ 105]---> BDD-cost:   24
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   16
c ---[ 102]---> BDD-cost:   29
c ---[ 101]---> BDD-cost:   13
c ---[ 100]---> BDD-cost:   49
c ---[  99]---> BDD-cost:   60
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:   12
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   16
c ---[  93]---> BDD-cost:   68
c ---[  92]---> BDD-cost:   78
c ---[  91]---> BDD-cost:   47
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   68
c ---[  88]---> BDD-cost:    8
c ---[  87]---> BDD-cost:   20
c ---[  86]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   12
c ---[  80]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[  79]---> Sorter-cost: 1212     Base: 2 3 2 3
c ---[  78]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  77]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  76]---> BDD-cost:   37
c ---[  75]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  71]---> BDD-cost:    3
c ---[  69]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  57]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  53]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  41]---> BDD-cost:    3
c ---[  33]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  13]---> BDD-cost:   49
c ---[  12]---> BDD-cost:   49
c ---[  11]---> BDD-cost:   26
c ---[  10]---> BDD-cost:    5
c ---[   9]---> BDD-cost:    7
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:   11
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:    4
c ---[   3]---> BDD-cost:    2
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    2
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   19073    57623 |    6357       0        0     nan |  0.000 % |
c |       100 |   19073    57623 |    6992     100      672     6.7 |  2.555 % |
c |       252 |   19057    57569 |    7691     247     1692     6.9 |  2.591 % |
c |       477 |   19057    57569 |    8461     472     5450    11.5 |  2.591 % |
c |       815 |   19057    57569 |    9307     810    10043    12.4 |  2.591 % |
c |      1321 |   19042    57516 |   10238    1311    18125    13.8 |  2.609 % |
c |      2080 |   19012    57412 |   11261    2062    40134    19.5 |  2.664 % |
c |      3220 |   19012    57412 |   12387    3202    69123    21.6 |  2.664 % |
c |      4929 |   18949    57203 |   13626    4904   116688    23.8 |  2.772 % |
c |      7491 |   18925    57134 |   14989    7465   185728    24.9 |  2.808 % |
c |     11337 |   18925    57134 |   16488   11311   347696    30.7 |  2.809 % |
c |     17104 |   18925    57134 |   18137    8643   242756    28.1 |  2.808 % |
c |     25753 |   18925    57134 |   19950   17292   503434    29.1 |  2.808 % |
c |     38727 |   18925    57134 |   21946   20110   621158    30.9 |  2.808 % |
c |     58188 |   18885    57000 |   24140   16745   543948    32.5 |  2.917 % |
c |     87380 |   18885    57000 |   26554   20873   764650    36.6 |  2.917 % |
c |    131169 |   18869    56944 |   29210   23294   693331    29.8 |  2.953 % |
c |    196854 |   18869    56944 |   32131   25433  1047150    41.2 |  2.953 % |
c |    295382 |   18869    56944 |   35344   17901   689696    38.5 |  2.954 % |
c |    443173 |   18869    56944 |   38878   17949   602270    33.6 |  2.953 % |
c |    664857 |   18869    56944 |   42766   27238  1062812    39.0 |  2.953 % |
#### 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.85 0.95 0.90 2/54 31760
Raw data (stat): 31760 (runsolver) R 31759 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545301058 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 1561 0 0 0 994 4 0 0 25 0 1 0 545301058 8118272 1528 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1982 1528 603 41 0 1941 0
vsize: 7928
[startup+20.001 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 1717 0 0 0 1994 5 0 0 25 0 1 0 545301058 8785920 1684 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2145 1684 603 41 0 2104 0
vsize: 8580
[startup+30.0013 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 1923 0 0 0 2993 5 0 0 25 0 1 0 545301058 9588736 1890 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2341 1890 603 41 0 2300 0
vsize: 9364
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2171 0 0 0 3993 6 0 0 25 0 1 0 545301058 10530816 2138 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2571 2138 603 41 0 2530 0
vsize: 10284
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2341 0 0 0 4991 8 0 0 25 0 1 0 545301058 11337728 2308 4294967295 134512640 134672761 3221224624 3221223728 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2768 2308 603 41 0 2727 0
vsize: 11072
[startup+60.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2388 0 0 0 5990 8 0 0 25 0 1 0 545301058 11485184 2355 4294967295 134512640 134672761 3221224624 3221223640 1075353074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2804 2355 603 41 0 2763 0
vsize: 11216
[startup+70.0027 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2404 0 0 0 6990 9 0 0 25 0 1 0 545301058 11485184 2371 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2804 2371 603 41 0 2763 0
vsize: 11216
[startup+80.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2437 0 0 0 7990 9 0 0 25 0 1 0 545301058 11632640 2404 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2840 2404 603 41 0 2799 0
vsize: 11360
[startup+90.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2437 0 0 0 8989 10 0 0 25 0 1 0 545301058 11632640 2404 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2840 2404 603 41 0 2799 0
vsize: 11360
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2444 0 0 0 9989 10 0 0 25 0 1 0 545301058 11796480 2411 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2880 2411 603 41 0 2839 0
vsize: 11520
[startup+110.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2468 0 0 0 10988 11 0 0 25 0 1 0 545301058 11796480 2435 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2880 2435 603 41 0 2839 0
vsize: 11520
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2490 0 0 0 11988 11 0 0 25 0 1 0 545301058 11943936 2457 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2916 2457 603 41 0 2875 0
vsize: 11664
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2551 0 0 0 12988 11 0 0 25 0 1 0 545301058 12210176 2518 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2981 2518 603 41 0 2940 0
vsize: 11924
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2679 0 0 0 13987 12 0 0 25 0 1 0 545301058 12746752 2646 4294967295 134512640 134672761 3221224624 3221223748 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3112 2646 603 41 0 3071 0
vsize: 12448
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2691 0 0 0 14987 13 0 0 25 0 1 0 545301058 12746752 2658 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3112 2658 603 41 0 3071 0
vsize: 12448
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2867 0 0 0 15986 13 0 0 25 0 1 0 545301058 13557760 2834 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3310 2834 603 41 0 3269 0
vsize: 13240
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2883 0 0 0 16986 14 0 0 25 0 1 0 545301058 13557760 2850 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3310 2850 603 41 0 3269 0
vsize: 13240
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2993 0 0 0 17986 14 0 0 25 0 1 0 545301058 14233600 2960 4294967295 134512640 134672761 3221224624 3221223760 134565134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3475 2960 603 41 0 3434 0
vsize: 13900
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 2996 0 0 0 18986 14 0 0 25 0 1 0 545301058 14233600 2963 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3475 2963 603 41 0 3434 0
vsize: 13900
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3013 0 0 0 19985 15 0 0 25 0 1 0 545301058 14385152 2980 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3512 2980 603 41 0 3471 0
vsize: 14048
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3014 0 0 0 20985 16 0 0 25 0 1 0 545301058 14385152 2981 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3512 2981 603 41 0 3471 0
vsize: 14048
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3030 0 0 0 21985 16 0 0 25 0 1 0 545301058 14385152 2997 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3512 2997 603 41 0 3471 0
vsize: 14048
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3052 0 0 0 22985 16 0 0 25 0 1 0 545301058 14581760 3019 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3560 3019 603 41 0 3519 0
vsize: 14240
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3054 0 0 0 23984 16 0 0 25 0 1 0 545301058 14581760 3021 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3560 3021 603 41 0 3519 0
vsize: 14240
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3080 0 0 0 24984 17 0 0 25 0 1 0 545301058 14729216 3047 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3596 3047 603 41 0 3555 0
vsize: 14384
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3100 0 0 0 25984 17 0 0 25 0 1 0 545301058 14729216 3067 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3596 3067 603 41 0 3555 0
vsize: 14384
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3116 0 0 0 26984 17 0 0 25 0 1 0 545301058 14893056 3083 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3636 3083 603 41 0 3595 0
vsize: 14544
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3131 0 0 0 27984 17 0 0 25 0 1 0 545301058 14893056 3098 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3636 3098 603 41 0 3595 0
vsize: 14544
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3131 0 0 0 28984 18 0 0 25 0 1 0 545301058 14893056 3098 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3636 3098 603 41 0 3595 0
vsize: 14544
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3131 0 0 0 29983 18 0 0 25 0 1 0 545301058 14893056 3098 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3636 3098 603 41 0 3595 0
vsize: 14544
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3150 0 0 0 30983 18 0 0 25 0 1 0 545301058 15040512 3117 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3672 3117 603 41 0 3631 0
vsize: 14688
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3169 0 0 0 31983 19 0 0 25 0 1 0 545301058 15040512 3136 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3672 3136 603 41 0 3631 0
vsize: 14688
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3190 0 0 0 32983 19 0 0 25 0 1 0 545301058 15204352 3157 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3157 603 41 0 3671 0
vsize: 14848
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3190 0 0 0 33983 19 0 0 25 0 1 0 545301058 15204352 3157 4294967295 134512640 134672761 3221224624 3221223776 134541828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3157 603 41 0 3671 0
vsize: 14848
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3199 0 0 0 34982 19 0 0 25 0 1 0 545301058 15204352 3166 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3166 603 41 0 3671 0
vsize: 14848
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3210 0 0 0 35982 20 0 0 25 0 1 0 545301058 15204352 3177 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3177 603 41 0 3671 0
vsize: 14848
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3210 0 0 0 36982 20 0 0 25 0 1 0 545301058 15204352 3177 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3177 603 41 0 3671 0
vsize: 14848
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3210 0 0 0 37982 20 0 0 25 0 1 0 545301058 15204352 3177 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3177 603 41 0 3671 0
vsize: 14848
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3210 0 0 0 38982 20 0 0 25 0 1 0 545301058 15204352 3177 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3177 603 41 0 3671 0
vsize: 14848
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3211 0 0 0 39982 21 0 0 25 0 1 0 545301058 15204352 3178 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3178 603 41 0 3671 0
vsize: 14848
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3212 0 0 0 40982 21 0 0 25 0 1 0 545301058 15204352 3179 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3179 603 41 0 3671 0
vsize: 14848
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3277 0 0 0 41981 22 0 0 25 0 1 0 545301058 15474688 3244 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3778 3244 603 41 0 3737 0
vsize: 15112
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3285 0 0 0 42981 22 0 0 25 0 1 0 545301058 15618048 3252 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3252 603 41 0 3772 0
vsize: 15252
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3312 0 0 0 43981 22 0 0 25 0 1 0 545301058 15761408 3279 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3848 3279 603 41 0 3807 0
vsize: 15392
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3325 0 0 0 44981 23 0 0 25 0 1 0 545301058 15761408 3292 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3848 3292 603 41 0 3807 0
vsize: 15392
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3327 0 0 0 45981 23 0 0 25 0 1 0 545301058 15761408 3294 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3848 3294 603 41 0 3807 0
vsize: 15392
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3348 0 0 0 46980 23 0 0 25 0 1 0 545301058 15941632 3315 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3892 3315 603 41 0 3851 0
vsize: 15568
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3358 0 0 0 47980 23 0 0 25 0 1 0 545301058 15941632 3325 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3892 3325 603 41 0 3851 0
vsize: 15568
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3358 0 0 0 48980 24 0 0 25 0 1 0 545301058 15941632 3325 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3892 3325 603 41 0 3851 0
vsize: 15568
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3367 0 0 0 49980 24 0 0 25 0 1 0 545301058 15941632 3334 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3892 3334 603 41 0 3851 0
vsize: 15568
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3379 0 0 0 50980 24 0 0 25 0 1 0 545301058 16105472 3346 4294967295 134512640 134672761 3221224624 3221223808 134559033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3932 3346 603 41 0 3891 0
vsize: 15728
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3383 0 0 0 51980 25 0 0 25 0 1 0 545301058 16105472 3350 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3932 3350 603 41 0 3891 0
vsize: 15728
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3402 0 0 0 52979 25 0 0 25 0 1 0 545301058 16105472 3369 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3932 3369 603 41 0 3891 0
vsize: 15728
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3453 0 0 0 53979 25 0 0 25 0 1 0 545301058 16375808 3420 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3998 3420 603 41 0 3957 0
vsize: 15992
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3469 0 0 0 54979 26 0 0 25 0 1 0 545301058 16375808 3436 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3998 3436 603 41 0 3957 0
vsize: 15992
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3481 0 0 0 55979 26 0 0 25 0 1 0 545301058 16515072 3448 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4032 3448 603 41 0 3991 0
vsize: 16128
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3558 0 0 0 56978 27 0 0 25 0 1 0 545301058 16781312 3525 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4097 3525 603 41 0 4056 0
vsize: 16388
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3573 0 0 0 57978 27 0 0 25 0 1 0 545301058 16928768 3540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4133 3540 603 41 0 4092 0
vsize: 16532
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3585 0 0 0 58977 28 0 0 25 0 1 0 545301058 16928768 3552 4294967295 134512640 134672761 3221224624 3221223728 134560483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4133 3552 603 41 0 4092 0
vsize: 16532
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3589 0 0 0 59977 29 0 0 25 0 1 0 545301058 16928768 3556 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4133 3556 603 41 0 4092 0
vsize: 16532
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3617 0 0 0 60977 29 0 0 25 0 1 0 545301058 17063936 3584 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4166 3584 603 41 0 4125 0
vsize: 16664
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3617 0 0 0 61977 29 0 0 25 0 1 0 545301058 17063936 3584 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4166 3584 603 41 0 4125 0
vsize: 16664
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3649 0 0 0 62978 29 0 0 25 0 1 0 545301058 17207296 3616 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3616 603 41 0 4160 0
vsize: 16804
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3651 0 0 0 63978 29 0 0 25 0 1 0 545301058 17207296 3618 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3618 603 41 0 4160 0
vsize: 16804
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3651 0 0 0 64978 29 0 0 25 0 1 0 545301058 17207296 3618 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3618 603 41 0 4160 0
vsize: 16804
[startup+660.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3659 0 0 0 65978 30 0 0 25 0 1 0 545301058 17207296 3626 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3626 603 41 0 4160 0
vsize: 16804
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3663 0 0 0 66978 30 0 0 25 0 1 0 545301058 17207296 3630 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3630 603 41 0 4160 0
vsize: 16804
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3663 0 0 0 67978 30 0 0 25 0 1 0 545301058 17207296 3630 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4201 3630 603 41 0 4160 0
vsize: 16804
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3673 0 0 0 68978 31 0 0 25 0 1 0 545301058 17371136 3640 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3640 603 41 0 4200 0
vsize: 16964
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3674 0 0 0 69977 31 0 0 25 0 1 0 545301058 17371136 3641 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3641 603 41 0 4200 0
vsize: 16964
[startup+710.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3715 0 0 0 70977 31 0 0 25 0 1 0 545301058 17506304 3682 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4274 3682 603 41 0 4233 0
vsize: 17096
[startup+720.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3718 0 0 0 71977 32 0 0 25 0 1 0 545301058 17506304 3685 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4274 3685 603 41 0 4233 0
vsize: 17096
[startup+730.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3734 0 0 0 72977 32 0 0 25 0 1 0 545301058 17670144 3701 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4314 3701 603 41 0 4273 0
vsize: 17256
[startup+740.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3764 0 0 0 73976 33 0 0 25 0 1 0 545301058 17833984 3731 4294967295 134512640 134672761 3221224624 3221223760 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4354 3731 603 41 0 4313 0
vsize: 17416
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3785 0 0 0 74976 33 0 0 25 0 1 0 545301058 17833984 3752 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4354 3752 603 41 0 4313 0
vsize: 17416
[startup+760.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3788 0 0 0 75976 33 0 0 25 0 1 0 545301058 17833984 3755 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4354 3755 603 41 0 4313 0
vsize: 17416
[startup+770.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3806 0 0 0 76976 34 0 0 25 0 1 0 545301058 17985536 3773 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4391 3773 603 41 0 4350 0
vsize: 17564
[startup+780.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3809 0 0 0 77976 34 0 0 25 0 1 0 545301058 17985536 3776 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4391 3776 603 41 0 4350 0
vsize: 17564
[startup+790.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3812 0 0 0 78976 34 0 0 25 0 1 0 545301058 17985536 3779 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4391 3779 603 41 0 4350 0
vsize: 17564
[startup+800.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3820 0 0 0 79975 35 0 0 25 0 1 0 545301058 17985536 3787 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4391 3787 603 41 0 4350 0
vsize: 17564
[startup+810.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3825 0 0 0 80975 35 0 0 25 0 1 0 545301058 18137088 3792 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4428 3792 603 41 0 4387 0
vsize: 17712
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3825 0 0 0 81975 36 0 0 25 0 1 0 545301058 18137088 3792 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4428 3792 603 41 0 4387 0
vsize: 17712
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3825 0 0 0 82975 36 0 0 25 0 1 0 545301058 18137088 3792 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4428 3792 603 41 0 4387 0
vsize: 17712
[startup+840.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3825 0 0 0 83974 36 0 0 25 0 1 0 545301058 18137088 3792 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4428 3792 603 41 0 4387 0
vsize: 17712
[startup+850.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 3949 0 0 0 84974 37 0 0 25 0 1 0 545301058 18538496 3916 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4526 3916 603 41 0 4485 0
vsize: 18104
[startup+860.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4026 0 0 0 85973 37 0 0 25 0 1 0 545301058 18952192 3993 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4627 3993 603 41 0 4586 0
vsize: 18508
[startup+870.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4038 0 0 0 86973 38 0 0 25 0 1 0 545301058 18952192 4005 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4627 4005 603 41 0 4586 0
vsize: 18508
[startup+880.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4041 0 0 0 87973 38 0 0 25 0 1 0 545301058 18952192 4008 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4627 4008 603 41 0 4586 0
vsize: 18508
[startup+890.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4104 0 0 0 88972 39 0 0 25 0 1 0 545301058 19218432 4071 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4692 4071 603 41 0 4651 0
vsize: 18768
[startup+900.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4266 0 0 0 89972 40 0 0 25 0 1 0 545301058 19947520 4233 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4870 4233 603 41 0 4829 0
vsize: 19480
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4277 0 0 0 90972 40 0 0 25 0 1 0 545301058 19947520 4244 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4870 4244 603 41 0 4829 0
vsize: 19480
[startup+920.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4289 0 0 0 91971 40 0 0 25 0 1 0 545301058 20086784 4256 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4904 4256 603 41 0 4863 0
vsize: 19616
[startup+930.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4295 0 0 0 92971 41 0 0 25 0 1 0 545301058 20086784 4262 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4904 4262 603 41 0 4863 0
vsize: 19616
[startup+940.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4295 0 0 0 93970 41 0 0 25 0 1 0 545301058 20086784 4262 4294967295 134512640 134672761 3221224624 3221223792 134560819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4904 4262 603 41 0 4863 0
vsize: 19616
[startup+950.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4295 0 0 0 94970 41 0 0 25 0 1 0 545301058 20086784 4262 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4262 603 41 0 4863 0
vsize: 19616
[startup+960.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4295 0 0 0 95970 41 0 0 25 0 1 0 545301058 20086784 4262 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4262 603 41 0 4863 0
vsize: 19616
[startup+970.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4295 0 0 0 96970 41 0 0 25 0 1 0 545301058 20086784 4262 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4262 603 41 0 4863 0
vsize: 19616
[startup+980.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4306 0 0 0 97971 41 0 0 25 0 1 0 545301058 20086784 4273 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4273 603 41 0 4863 0
vsize: 19616
[startup+990.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4306 0 0 0 98971 41 0 0 25 0 1 0 545301058 20086784 4273 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4273 603 41 0 4863 0
vsize: 19616
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4312 0 0 0 99971 41 0 0 25 0 1 0 545301058 20086784 4279 4294967295 134512640 134672761 3221224624 3221223776 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4279 603 41 0 4863 0
vsize: 19616
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4313 0 0 0 100971 41 0 0 25 0 1 0 545301058 20086784 4280 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4280 603 41 0 4863 0
vsize: 19616
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4324 0 0 0 101971 41 0 0 25 0 1 0 545301058 20234240 4291 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4291 603 41 0 4899 0
vsize: 19760
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4329 0 0 0 102972 41 0 0 25 0 1 0 545301058 20234240 4296 4294967295 134512640 134672761 3221224624 3221223840 134557665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4296 603 41 0 4899 0
vsize: 19760
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4334 0 0 0 103972 42 0 0 25 0 1 0 545301058 20234240 4301 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4301 603 41 0 4899 0
vsize: 19760
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4334 0 0 0 104972 42 0 0 25 0 1 0 545301058 20234240 4301 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4301 603 41 0 4899 0
vsize: 19760
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4344 0 0 0 105972 42 0 0 25 0 1 0 545301058 20398080 4311 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4311 603 41 0 4939 0
vsize: 19920
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4346 0 0 0 106972 42 0 0 25 0 1 0 545301058 20398080 4313 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4313 603 41 0 4939 0
vsize: 19920
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4346 0 0 0 107972 42 0 0 25 0 1 0 545301058 20398080 4313 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4313 603 41 0 4939 0
vsize: 19920
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4346 0 0 0 108972 42 0 0 25 0 1 0 545301058 20398080 4313 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4313 603 41 0 4939 0
vsize: 19920
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4346 0 0 0 109972 42 0 0 25 0 1 0 545301058 20398080 4313 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4313 603 41 0 4939 0
vsize: 19920
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4349 0 0 0 110972 42 0 0 25 0 1 0 545301058 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4349 0 0 0 111972 42 0 0 25 0 1 0 545301058 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4349 0 0 0 112972 43 0 0 25 0 1 0 545301058 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4349 0 0 0 113973 43 0 0 25 0 1 0 545301058 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4349 0 0 0 114973 43 0 0 25 0 1 0 545301058 20398080 4316 4294967295 134512640 134672761 3221224624 3221223808 134558671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4349 0 0 0 115973 43 0 0 25 0 1 0 545301058 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4349 0 0 0 116973 43 0 0 25 0 1 0 545301058 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4349 0 0 0 117973 43 0 0 25 0 1 0 545301058 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4367 0 0 0 118973 43 0 0 25 0 1 0 545301058 20398080 4334 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4334 603 41 0 4939 0
vsize: 19920
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31762
Raw data (stat): 31760 (minisat+) R 31759 22612 22611 0 -1 0 4401 0 0 0 119973 43 0 0 25 0 1 0 545301058 20533248 4368 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5013 4368 603 41 0 4972 0
vsize: 20052
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31762
Raw data (stat): 31760 (minisat+) Z 31759 22612 22611 0 -1 12 4403 0 0 0 119973 44 0 0 25 0 1 0 545301058 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.05
CPU time (s): 1200.18
CPU user time (s): 1199.74
CPU system time (s): 0.442932
CPU usage (%): 100.011
Max. virtual memory (Kb): 20052
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####