PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0548.opb
MD5SUM	6f47095f2d417d23ced995954e641689
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	15249
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 numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1236.38
Number of variables	548
Total number of constraints	724
Number of constraints which are clauses	40
Number of constraints which are cardinality constraints (but not clauses)	550
Number of constraints which are nor clauses,nor cardinality constraints	134
Minimum length of a constraint	1
Maximum length of a constraint	143
Trace number 15588

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        675128 kB
Buffers:         21180 kB
Cached:         306716 kB
SwapCached:          0 kB
Active:         143948 kB
Inactive:       186764 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        674876 kB
SwapTotal:     2097892 kB
SwapFree:      2097824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            23176 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:25:51 (client local time) WITH STATUS 0 IN 1200.1 SECONDS
stats: 17157 7 1200.1 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]---> Adder-cost: 66   maxlim: 856   bits: 11/10
c ---[ 163]---> Adder-cost: 73   maxlim: 258   bits: 10/9
c ---[ 162]---> Adder-cost: 56   maxlim: 650   bits: 11/10
c ---[ 161]---> Adder-cost: 64   maxlim: 847   bits: 11/10
c ---[ 160]---> Adder-cost: 69   maxlim: 354   bits: 10/9
c ---[ 159]---> Adder-cost: 50   maxlim: 668   bits: 11/10
c ---[ 157]---> Adder-cost: 73   maxlim: 419   bits: 10/9
c ---[ 156]---> Adder-cost: 61   maxlim: 227   bits: 9/8
c ---[ 154]---> Adder-cost: 67   maxlim: 479   bits: 10/9
c ---[ 153]---> Adder-cost: 34   maxlim: 106   bits: 8/7
c ---[ 152]---> Adder-cost: 92   maxlim: 333   bits: 10/9
c ---[ 151]---> Adder-cost: 77   maxlim: 407   bits: 10/9
c ---[ 150]---> Adder-cost: 82   maxlim: 615   bits: 11/10
c ---[ 149]---> Adder-cost: 96   maxlim: 1156   bits: 12/11
c ---[ 148]---> Adder-cost: 34   maxlim: 332   bits: 10/9
c ---[ 147]---> Adder-cost: 86   maxlim: 433   bits: 10/9
c ---[ 146]---> Adder-cost: 77   maxlim: 385   bits: 10/9
c ---[ 145]---> Adder-cost: 88   maxlim: 1134   bits: 12/11
c ---[ 144]---> Adder-cost: 93   maxlim: 249   bits: 9/8
c ---[ 143]---> Adder-cost: 100   maxlim: 295   bits: 10/9
c ---[ 142]---> Adder-cost: 97   maxlim: 249   bits: 9/8
c ---[ 141]---> Adder-cost: 108   maxlim: 494   bits: 10/9
c ---[ 140]---> Adder-cost: 98   maxlim: 506   bits: 10/9
c ---[ 139]---> Adder-cost: 53   maxlim: 259   bits: 10/9
c ---[ 138]---> Adder-cost: 55   maxlim: 439   bits: 10/9
c ---[ 136]---> Adder-cost: 61   maxlim: 393   bits: 10/9
c ---[ 135]---> Adder-cost: 94   maxlim: 1081   bits: 12/11
c ---[ 134]---> Adder-cost: 86   maxlim: 681   bits: 11/10
c ---[ 133]---> Adder-cost: 82   maxlim: 512   bits: 11/10
c ---[ 131]---> Adder-cost: 88   maxlim: 558   bits: 11/10
c ---[ 130]---> Adder-cost: 36   maxlim: 441   bits: 10/9
c ---[ 129]---> Adder-cost: 67   maxlim: 430   bits: 10/9
c ---[ 128]---> Adder-cost: 61   maxlim: 482   bits: 10/9
c ---[ 127]---> Adder-cost: 46   maxlim: 819   bits: 11/10
c ---[ 126]---> Adder-cost: 47   maxlim: 275   bits: 10/9
c ---[ 125]---> Adder-cost: 51   maxlim: 308   bits: 10/9
c ---[ 123]---> Adder-cost: 53   maxlim: 894   bits: 11/10
c ---[ 121]---> Adder-cost: 36   maxlim: 131   bits: 9/8
c ---[ 120]---> Adder-cost: 45   maxlim: 730   bits: 11/10
c ---[ 119]---> Adder-cost: 38   maxlim: 121   bits: 8/7
c ---[ 118]---> Adder-cost: 64   maxlim: 932   bits: 11/10
c ---[ 117]---> Adder-cost: 53   maxlim: 733   bits: 11/10
c ---[ 116]---> Adder-cost: 43   maxlim: 751   bits: 11/10
c ---[ 115]---> Adder-cost: 58   maxlim: 837   bits: 11/10
c ---[ 114]---> Adder-cost: 41   maxlim: 605   bits: 11/10
c ---[ 112]---> Adder-cost: 22   maxlim: 405   bits: 10/9
c ---[ 111]---> Adder-cost: 62   maxlim: 1052   bits: 12/11
c ---[ 110]---> Adder-cost: 53   maxlim: 811   bits: 11/10
c ---[ 109]---> Adder-cost: 47   maxlim: 603   bits: 11/10
c ---[ 107]---> Adder-cost: 18   maxlim: 360   bits: 10/9
c ---[ 106]---> Adder-cost: 47   maxlim: 785   bits: 11/10
c ---[ 105]---> Adder-cost: 49   maxlim: 833   bits: 11/10
c ---[ 104]---> Adder-cost: 49   maxlim: 0   bits: 1/0
c ---[ 103]---> Adder-cost: 59   maxlim: 1277   bits: 12/11
c ---[ 102]---> Adder-cost: 60   maxlim: 1324   bits: 12/11
c ---[ 101]---> Adder-cost: 67   maxlim: 1287   bits: 12/11
c ---[ 100]---> Adder-cost: 62   maxlim: 1125   bits: 12/11
c ---[  99]---> Adder-cost: 61   maxlim: 933   bits: 11/10
c ---[  98]---> Adder-cost: 41   maxlim: 715   bits: 11/10
c ---[  97]---> Adder-cost: 47   maxlim: 374   bits: 10/9
c ---[  96]---> Adder-cost: 72   maxlim: 972   bits: 11/10
c ---[  95]---> Adder-cost: 50   maxlim: 684   bits: 11/10
c ---[  93]---> Adder-cost: 64   maxlim: 390   bits: 10/9
c ---[  92]---> Adder-cost: 55   maxlim: 731   bits: 11/10
c ---[  91]---> Adder-cost: 61   maxlim: 866   bits: 11/10
c ---[  90]---> Adder-cost: 88   maxlim: 1313   bits: 12/11
c ---[  89]---> Adder-cost: 59   maxlim: 888   bits: 11/10
c ---[  88]---> Adder-cost: 28   maxlim: 141   bits: 9/8
c ---[  87]---> Adder-cost: 39   maxlim: 694   bits: 11/10
c ---[  86]---> Adder-cost: 25   maxlim: 447   bits: 10/9
c ---[  83]---> Adder-cost: 39   maxlim: 751   bits: 11/10
c ---[  81]---> Adder-cost: 28   maxlim: 646   bits: 11/10
c ---[  80]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[  79]---> Adder-cost: 126   maxlim: 381   bits: 10/9
c ---[  78]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  77]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  76]---> Adder-cost: 48   maxlim: 173   bits: 8/8
c ---[  75]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  73]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  71]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  69]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  67]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  61]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  59]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  57]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  55]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  53]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  47]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  41]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  33]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  31]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  29]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  27]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  25]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  21]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  19]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  17]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  15]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  13]---> Adder-cost: 98   maxlim: 48   bits: 7/6
c ---[  12]---> Adder-cost: 98   maxlim: 48   bits: 7/6
c ---[  11]---> Adder-cost: 52   maxlim: 25   bits: 6/5
c ---[  10]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[   9]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[   8]---> Adder-cost: 28   maxlim: 114   bits: 8/7
c ---[   7]---> Adder-cost: 24   maxlim: 141   bits: 9/8
c ---[   6]---> Adder-cost: 26   maxlim: 105   bits: 8/7
c ---[   5]---> Adder-cost: 50   maxlim: 158   bits: 9/8
c ---[   4]---> Adder-cost: 21   maxlim: 83   bits: 8/7
c ---[   3]---> Adder-cost: 4   maxlim: 68   bits: 8/7
c ---[   2]---> Adder-cost: 33   maxlim: 122   bits: 8/7
c ---[   1]---> Adder-cost: 4   maxlim: 68   bits: 8/7
c ---[   0]---> Adder-cost: 16   maxlim: 82   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   38053   135144 |   12684       0        0     nan |  0.000 % |
c |       100 |   38046   135121 |   13952      98      344     3.5 |  6.965 % |
c |       250 |   38046   135121 |   15347     248     1172     4.7 |  6.965 % |
c |       475 |   38046   135121 |   16882     473     2437     5.2 |  6.965 % |
c |       813 |   38046   135121 |   18570     811     5286     6.5 |  6.965 % |
c |      1319 |   38046   135121 |   20427    1317    11341     8.6 |  6.965 % |
c |      2079 |   38046   135121 |   22470    2077    26694    12.9 |  6.965 % |
c |      3218 |   38000   134951 |   24717    3211    50668    15.8 |  6.979 % |
c |      4926 |   38000   134951 |   27189    4919    95762    19.5 |  6.979 % |
c |      7494 |   38000   134951 |   29908    7487   192830    25.8 |  6.979 % |
c |     11338 |   38000   134951 |   32899   11331   351409    31.0 |  6.979 % |
c |     17105 |   38000   134951 |   36188   17098   551679    32.3 |  6.979 % |
c |     25757 |   38000   134951 |   39807   25750   903072    35.1 |  6.979 % |
c |     38731 |   37995   134935 |   43788   38723  1593201    41.1 |  6.993 % |
c |     58193 |   37995   134935 |   48167   27938   973445    34.8 |  6.993 % |
c |     87387 |   37995   134935 |   52984   22059  1143015    51.8 |  6.993 % |
c |    131176 |   37995   134935 |   58282   26575  1093824    41.2 |  6.993 % |
c |    196860 |   37995   134935 |   64110   50068  2036691    40.7 |  6.993 % |
c |    295386 |   37995   134935 |   70521   51695  3048990    59.0 |  6.993 % |
c |    443176 |   37995   134935 |   77574   40603  1677127    41.3 |  6.993 % |
c |    664859 |   37927   134690 |   85331   73978  4091325    55.3 |  7.022 % |
#### 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.94 0.90 2/54 12169
Raw data (stat): 12169 (runsolver) R 12168 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542422035 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 1982 0 0 0 993 5 0 0 25 0 1 0 542422035 9945088 1959 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2428 1959 603 41 0 2387 0
vsize: 9712
[startup+20.0021 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 2761 0 0 0 1990 8 0 0 25 0 1 0 542422035 13164544 2738 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3214 2738 603 41 0 3173 0
vsize: 12856
[startup+30.0029 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 3209 0 0 0 2988 11 0 0 25 0 1 0 542422035 15048704 3186 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3674 3186 603 41 0 3633 0
vsize: 14696
[startup+40.0033 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 3269 0 0 0 3988 11 0 0 25 0 1 0 542422035 15319040 3246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3740 3246 603 41 0 3699 0
vsize: 14960
[startup+50.0045 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 3269 0 0 0 4987 12 0 0 25 0 1 0 542422035 15319040 3246 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3740 3246 603 41 0 3699 0
vsize: 14960
[startup+60.0043 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 3343 0 0 0 5987 12 0 0 25 0 1 0 542422035 15585280 3320 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3805 3320 603 41 0 3764 0
vsize: 15220
[startup+70.0047 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 3741 0 0 0 6985 14 0 0 25 0 1 0 542422035 17182720 3718 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4195 3718 603 41 0 4154 0
vsize: 16780
[startup+80.0059 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 3741 0 0 0 7985 15 0 0 25 0 1 0 542422035 17182720 3718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4195 3718 603 41 0 4154 0
vsize: 16780
[startup+90.0067 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 3741 0 0 0 8985 15 0 0 25 0 1 0 542422035 17182720 3718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4195 3718 603 41 0 4154 0
vsize: 16780
[startup+100.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4067 0 0 0 9984 16 0 0 25 0 1 0 542422035 18530304 4044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4524 4044 603 41 0 4483 0
vsize: 18096
[startup+110.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4191 0 0 0 10983 17 0 0 25 0 1 0 542422035 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4654 4168 603 41 0 4613 0
vsize: 18616
[startup+120.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4191 0 0 0 11982 17 0 0 25 0 1 0 542422035 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4654 4168 603 41 0 4613 0
vsize: 18616
[startup+130.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4191 0 0 0 12982 17 0 0 25 0 1 0 542422035 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4654 4168 603 41 0 4613 0
vsize: 18616
[startup+140.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4192 0 0 0 13982 18 0 0 25 0 1 0 542422035 19062784 4169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4654 4169 603 41 0 4613 0
vsize: 18616
[startup+150.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4192 0 0 0 14982 18 0 0 25 0 1 0 542422035 19062784 4169 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4654 4169 603 41 0 4613 0
vsize: 18616
[startup+160.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4394 0 0 0 15981 19 0 0 25 0 1 0 542422035 19877888 4371 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4853 4371 603 41 0 4812 0
vsize: 19412
[startup+170.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4450 0 0 0 16981 19 0 0 25 0 1 0 542422035 20148224 4427 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4427 603 41 0 4878 0
vsize: 19676
[startup+180.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4450 0 0 0 17981 19 0 0 25 0 1 0 542422035 20148224 4427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4427 603 41 0 4878 0
vsize: 19676
[startup+190.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4460 0 0 0 18981 20 0 0 25 0 1 0 542422035 20148224 4437 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4437 603 41 0 4878 0
vsize: 19676
[startup+200.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4461 0 0 0 19981 20 0 0 25 0 1 0 542422035 20148224 4438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4438 603 41 0 4878 0
vsize: 19676
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4467 0 0 0 20981 20 0 0 25 0 1 0 542422035 20148224 4444 4294967295 134512640 134672761 3221224544 3221223556 1075351040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4444 603 41 0 4878 0
vsize: 19676
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4468 0 0 0 21981 20 0 0 25 0 1 0 542422035 20148224 4445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4445 603 41 0 4878 0
vsize: 19676
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4703 0 0 0 22980 21 0 0 25 0 1 0 542422035 21213184 4680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5179 4680 603 41 0 5138 0
vsize: 20716
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4974 0 0 0 23978 23 0 0 25 0 1 0 542422035 22282240 4951 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5440 4951 603 41 0 5399 0
vsize: 21760
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4983 0 0 0 24978 23 0 0 25 0 1 0 542422035 22282240 4960 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5440 4960 603 41 0 5399 0
vsize: 21760
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4986 0 0 0 25978 23 0 0 25 0 1 0 542422035 22282240 4963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5440 4963 603 41 0 5399 0
vsize: 21760
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4986 0 0 0 26978 23 0 0 25 0 1 0 542422035 22282240 4963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5440 4963 603 41 0 5399 0
vsize: 21760
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 4998 0 0 0 27978 24 0 0 25 0 1 0 542422035 22462464 4975 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5484 4975 603 41 0 5443 0
vsize: 21936
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 5002 0 0 0 28978 24 0 0 25 0 1 0 542422035 22462464 4979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5484 4979 603 41 0 5443 0
vsize: 21936
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 5111 0 0 0 29977 25 0 0 25 0 1 0 542422035 22843392 5088 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5577 5088 603 41 0 5536 0
vsize: 22308
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 5392 0 0 0 30975 26 0 0 25 0 1 0 542422035 24039424 5369 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5369 603 41 0 5828 0
vsize: 23476
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 5671 0 0 0 31975 27 0 0 25 0 1 0 542422035 25231360 5648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6160 5648 603 41 0 6119 0
vsize: 24640
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 5914 0 0 0 32974 28 0 0 25 0 1 0 542422035 26161152 5891 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6387 5891 603 41 0 6346 0
vsize: 25548
[startup+340.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6159 0 0 0 33973 29 0 0 25 0 1 0 542422035 27295744 6136 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6664 6136 603 41 0 6623 0
vsize: 26656
[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6284 0 0 0 34972 30 0 0 25 0 1 0 542422035 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6284 0 0 0 35972 30 0 0 25 0 1 0 542422035 27885568 6261 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6284 0 0 0 36973 30 0 0 25 0 1 0 542422035 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6284 0 0 0 37973 30 0 0 25 0 1 0 542422035 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6291 0 0 0 38973 30 0 0 25 0 1 0 542422035 27885568 6268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6268 603 41 0 6767 0
vsize: 27232
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6291 0 0 0 39973 30 0 0 25 0 1 0 542422035 27885568 6268 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6268 603 41 0 6767 0
vsize: 27232
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6291 0 0 0 40973 30 0 0 25 0 1 0 542422035 27885568 6268 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6268 603 41 0 6767 0
vsize: 27232
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6294 0 0 0 41973 30 0 0 25 0 1 0 542422035 27885568 6271 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6271 603 41 0 6767 0
vsize: 27232
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6299 0 0 0 42973 30 0 0 25 0 1 0 542422035 28147712 6276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6872 6276 603 41 0 6831 0
vsize: 27488
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6301 0 0 0 43973 30 0 0 25 0 1 0 542422035 28147712 6278 4294967295 134512640 134672761 3221224544 3221223728 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6872 6278 603 41 0 6831 0
vsize: 27488
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6301 0 0 0 44973 30 0 0 25 0 1 0 542422035 28147712 6278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6872 6278 603 41 0 6831 0
vsize: 27488
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6301 0 0 0 45973 30 0 0 25 0 1 0 542422035 28147712 6278 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6872 6278 603 41 0 6831 0
vsize: 27488
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6317 0 0 0 46973 30 0 0 25 0 1 0 542422035 28299264 6294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6294 603 41 0 6868 0
vsize: 27636
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6319 0 0 0 47974 30 0 0 25 0 1 0 542422035 28299264 6296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6296 603 41 0 6868 0
vsize: 27636
[startup+490.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6334 0 0 0 48974 30 0 0 25 0 1 0 542422035 28299264 6311 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6311 603 41 0 6868 0
vsize: 27636
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6372 0 0 0 49974 30 0 0 25 0 1 0 542422035 28463104 6349 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6949 6349 603 41 0 6908 0
vsize: 27796
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6384 0 0 0 50974 31 0 0 25 0 1 0 542422035 28626944 6361 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6361 603 41 0 6948 0
vsize: 27956
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6385 0 0 0 51974 31 0 0 25 0 1 0 542422035 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6362 603 41 0 6948 0
vsize: 27956
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6385 0 0 0 52974 31 0 0 25 0 1 0 542422035 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6362 603 41 0 6948 0
vsize: 27956
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6385 0 0 0 53974 31 0 0 25 0 1 0 542422035 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6362 603 41 0 6948 0
vsize: 27956
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6387 0 0 0 54975 31 0 0 25 0 1 0 542422035 28626944 6364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6364 603 41 0 6948 0
vsize: 27956
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6387 0 0 0 55975 31 0 0 25 0 1 0 542422035 28626944 6364 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6364 603 41 0 6948 0
vsize: 27956
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6387 0 0 0 56975 31 0 0 25 0 1 0 542422035 28626944 6364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6364 603 41 0 6948 0
vsize: 27956
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6388 0 0 0 57975 31 0 0 25 0 1 0 542422035 28626944 6365 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6365 603 41 0 6948 0
vsize: 27956
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6400 0 0 0 58975 31 0 0 25 0 1 0 542422035 28626944 6377 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6377 603 41 0 6948 0
vsize: 27956
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6421 0 0 0 59975 31 0 0 25 0 1 0 542422035 28823552 6398 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6398 603 41 0 6996 0
vsize: 28148
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6435 0 0 0 60976 31 0 0 25 0 1 0 542422035 28823552 6412 4294967295 134512640 134672761 3221224544 3221223536 134565743 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6435 0 0 0 61976 31 0 0 25 0 1 0 542422035 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6435 0 0 0 62976 31 0 0 25 0 1 0 542422035 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6435 0 0 0 63976 31 0 0 25 0 1 0 542422035 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6435 0 0 0 64976 31 0 0 25 0 1 0 542422035 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+660.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6435 0 0 0 65976 31 0 0 25 0 1 0 542422035 28823552 6412 4294967295 134512640 134672761 3221224544 3221223728 134558771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6435 0 0 0 66976 31 0 0 25 0 1 0 542422035 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6435 0 0 0 67976 31 0 0 25 0 1 0 542422035 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6436 0 0 0 68976 31 0 0 25 0 1 0 542422035 28823552 6413 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6413 603 41 0 6996 0
vsize: 28148
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6441 0 0 0 69976 31 0 0 25 0 1 0 542422035 28823552 6418 4294967295 134512640 134672761 3221224544 3221223648 134554926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6418 603 41 0 6996 0
vsize: 28148
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6448 0 0 0 70975 31 0 0 25 0 1 0 542422035 28823552 6425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6425 603 41 0 6996 0
vsize: 28148
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6450 0 0 0 71975 31 0 0 25 0 1 0 542422035 28823552 6427 4294967295 134512640 134672761 3221224544 3221223728 134559611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6427 603 41 0 6996 0
vsize: 28148
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6467 0 0 0 72975 32 0 0 25 0 1 0 542422035 28987392 6444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7077 6444 603 41 0 7036 0
vsize: 28308
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6467 0 0 0 73974 32 0 0 25 0 1 0 542422035 28987392 6444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7077 6444 603 41 0 7036 0
vsize: 28308
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6474 0 0 0 74974 32 0 0 25 0 1 0 542422035 28987392 6451 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7077 6451 603 41 0 7036 0
vsize: 28308
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6488 0 0 0 75974 32 0 0 25 0 1 0 542422035 29151232 6465 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7117 6465 603 41 0 7076 0
vsize: 28468
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6496 0 0 0 76973 32 0 0 25 0 1 0 542422035 29151232 6473 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7117 6473 603 41 0 7076 0
vsize: 28468
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6510 0 0 0 77973 33 0 0 25 0 1 0 542422035 29151232 6487 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7117 6487 603 41 0 7076 0
vsize: 28468
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6549 0 0 0 78973 33 0 0 25 0 1 0 542422035 29347840 6526 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7165 6526 603 41 0 7124 0
vsize: 28660
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6662 0 0 0 79973 33 0 0 25 0 1 0 542422035 29904896 6639 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7301 6639 603 41 0 7260 0
vsize: 29204
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6662 0 0 0 80972 33 0 0 25 0 1 0 542422035 29904896 6639 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6639 603 41 0 7260 0
vsize: 29204
[startup+820.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6662 0 0 0 81971 34 0 0 25 0 1 0 542422035 29904896 6639 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7301 6639 603 41 0 7260 0
vsize: 29204
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6663 0 0 0 82972 34 0 0 25 0 1 0 542422035 29904896 6640 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7301 6640 603 41 0 7260 0
vsize: 29204
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6674 0 0 0 83972 34 0 0 25 0 1 0 542422035 29904896 6651 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7301 6651 603 41 0 7260 0
vsize: 29204
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6681 0 0 0 84972 34 0 0 25 0 1 0 542422035 29904896 6658 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7301 6658 603 41 0 7260 0
vsize: 29204
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6697 0 0 0 85972 34 0 0 25 0 1 0 542422035 30040064 6674 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7334 6674 603 41 0 7293 0
vsize: 29336
[startup+870.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6704 0 0 0 86972 34 0 0 25 0 1 0 542422035 30040064 6681 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7334 6681 603 41 0 7293 0
vsize: 29336
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6704 0 0 0 87972 34 0 0 25 0 1 0 542422035 30040064 6681 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7334 6681 603 41 0 7293 0
vsize: 29336
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6720 0 0 0 88972 34 0 0 25 0 1 0 542422035 30203904 6697 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6697 603 41 0 7333 0
vsize: 29496
[startup+900.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6725 0 0 0 89971 34 0 0 25 0 1 0 542422035 30203904 6702 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6702 603 41 0 7333 0
vsize: 29496
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6734 0 0 0 90970 34 0 0 25 0 1 0 542422035 30203904 6711 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+920.031 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6734 0 0 0 91970 34 0 0 25 0 1 0 542422035 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+930.031 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6734 0 0 0 92969 34 0 0 25 0 1 0 542422035 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+940.032 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6734 0 0 0 93969 34 0 0 25 0 1 0 542422035 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+950.032 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6734 0 0 0 94969 34 0 0 25 0 1 0 542422035 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+960.032 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6734 0 0 0 95969 34 0 0 25 0 1 0 542422035 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+970.033 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6734 0 0 0 96970 34 0 0 25 0 1 0 542422035 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+980.032 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6734 0 0 0 97970 34 0 0 25 0 1 0 542422035 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+990.033 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6734 0 0 0 98970 34 0 0 25 0 1 0 542422035 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+1000.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 6867 0 0 0 99970 35 0 0 25 0 1 0 542422035 30875648 6844 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7538 6844 603 41 0 7497 0
vsize: 30152
[startup+1010.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7127 0 0 0 100969 36 0 0 25 0 1 0 542422035 31944704 7104 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7799 7104 603 41 0 7758 0
vsize: 31196
[startup+1020.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7379 0 0 0 101969 36 0 0 25 0 1 0 542422035 32878592 7356 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8027 7356 603 41 0 7986 0
vsize: 32108
[startup+1030.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7619 0 0 0 102968 37 0 0 25 0 1 0 542422035 33951744 7596 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8289 7596 603 41 0 8248 0
vsize: 33156
[startup+1040.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7850 0 0 0 103967 37 0 0 25 0 1 0 542422035 34897920 7827 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8520 7827 603 41 0 8479 0
vsize: 34080
[startup+1050.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7939 0 0 0 104967 37 0 0 25 0 1 0 542422035 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7939 0 0 0 105968 37 0 0 25 0 1 0 542422035 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7939 0 0 0 106968 37 0 0 25 0 1 0 542422035 35164160 7916 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7939 0 0 0 107968 37 0 0 25 0 1 0 542422035 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7939 0 0 0 108968 37 0 0 25 0 1 0 542422035 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7939 0 0 0 109968 37 0 0 25 0 1 0 542422035 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7956 0 0 0 110969 37 0 0 25 0 1 0 542422035 35315712 7933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8622 7933 603 41 0 8581 0
vsize: 34488
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 7992 0 0 0 111969 38 0 0 25 0 1 0 542422035 35479552 7969 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8662 7969 603 41 0 8621 0
vsize: 34648
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 8006 0 0 0 112969 38 0 0 25 0 1 0 542422035 35479552 7983 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8662 7983 603 41 0 8621 0
vsize: 34648
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 8008 0 0 0 113969 38 0 0 25 0 1 0 542422035 35479552 7985 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8662 7985 603 41 0 8621 0
vsize: 34648
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 8021 0 0 0 114969 38 0 0 25 0 1 0 542422035 35676160 7998 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8710 7998 603 41 0 8669 0
vsize: 34840
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 8022 0 0 0 115969 38 0 0 25 0 1 0 542422035 35676160 7999 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8710 7999 603 41 0 8669 0
vsize: 34840
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 8035 0 0 0 116970 38 0 0 25 0 1 0 542422035 35676160 8012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8710 8012 603 41 0 8669 0
vsize: 34840
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 8035 0 0 0 117969 38 0 0 25 0 1 0 542422035 35676160 8012 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8710 8012 603 41 0 8669 0
vsize: 34840
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 8035 0 0 0 118969 38 0 0 25 0 1 0 542422035 35676160 8012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8710 8012 603 41 0 8669 0
vsize: 34840
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12171
Raw data (stat): 12169 (minisat+) R 12168 11931 11930 0 -1 0 8045 0 0 0 119969 38 0 0 25 0 1 0 542422035 35676160 8022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8710 8022 603 41 0 8669 0
vsize: 34840
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 12171
Raw data (stat): 12169 (minisat+) Z 12168 11931 11930 0 -1 12 8047 0 0 0 119969 40 0 0 25 0 1 0 542422035 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.06
CPU time (s): 1200.1
CPU user time (s): 1199.7
CPU system time (s): 0.400939
CPU usage (%): 100.003
Max. virtual memory (Kb): 34840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####