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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.95:100.opb
MD5SUM	b2c6bc03457d15976fdaf81252d9cdae
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3
Optimality of the best value was proved	NO
Number of terms in the objective function	435
Biggest coefficient in the objective function	282
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	1168
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	282
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	1168
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02284
Number of variables	435
Total number of constraints	935
Number of constraints which are clauses	403
Number of constraints which are cardinality constraints (but not clauses)	532
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	16
Trace number 5285

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-13 23:17:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3749 boxname=wulflinc3 idbench=365 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b2c6bc03457d15976fdaf81252d9cdae  /oldhome/oroussel/tmp/wulflinc3/normalized-10:10:4.5:0.95:100.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc3/normalized-10:10:4.5:0.95:100.opb /oldhome/oroussel/tmp/wulflinc3/normalized-10:10:4.5:0.95:100.opb
IDLAUNCH: 3749
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        886424 kB
Buffers:         35324 kB
Cached:          89920 kB
SwapCached:       3276 kB
Active:          68092 kB
Inactive:        63328 kB
HighTotal:      131008 kB
HighFree:        37128 kB
LowTotal:       903652 kB
LowFree:        849296 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11200 kB
Committed_AS:    71664 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:37:03 (client local time) WITH STATUS 10 IN 1200.13 SECONDS
stats: 3749 7 1200.13 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 500 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  97]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  96]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  95]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  94]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  93]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  92]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  91]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  90]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  89]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  88]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  87]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  86]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  82]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  81]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  79]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 6   maxlim: 1   bits: 2/1
c ---[  73]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  72]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  71]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  70]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  69]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  68]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  67]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  66]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  65]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  64]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  63]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  62]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  61]---> Adder-cost: 11   maxlim: 2   bits: 3/2
c ---[  60]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  59]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  58]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  57]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  56]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  54]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  53]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  52]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  51]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  49]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  48]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  47]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  46]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  45]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  44]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  43]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  42]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  41]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  40]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  39]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  38]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  37]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  36]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  35]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  34]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  33]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  32]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  31]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  30]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  29]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  28]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  27]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  26]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  25]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  24]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  23]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  22]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  21]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  20]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  19]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  18]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  17]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  16]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  15]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  14]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  13]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  12]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  11]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  10]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   9]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   8]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   7]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   6]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   5]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   4]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   3]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   2]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   1]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   0]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    7345    25243 |    2448       0        0     nan |  0.000 % |
c |       100 |    7333    25209 |    2692      98      402     4.1 | 10.152 % |
c ==============================================================================
c [1mFound solution: 105[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1016   maxlim: 499   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       176 |   14409    50475 |    4803     174      769     4.4 | 10.152 % |
c ==============================================================================
c [1mFound solution: 80[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 524   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       235 |   14418    50513 |    4806     233     1125     4.8 | 10.152 % |
c |       335 |   14418    50513 |    5286     333     1538     4.6 |  6.871 % |
c |       486 |   14418    50513 |    5815     484     5566    11.5 |  6.871 % |
c |       711 |   14418    50513 |    6396     709     6643     9.4 |  6.871 % |
c ==============================================================================
c [1mFound solution: 73[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 531   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       797 |   14421    50529 |    4807     795     7082     8.9 |  6.871 % |
c |       898 |   14421    50529 |    5287     896     8297     9.3 |  6.934 % |
c |      1048 |   14421    50529 |    5816    1046     9207     8.8 |  6.934 % |
c ==============================================================================
c [1mFound solution: 52[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 552   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1084 |   14424    50551 |    4808    1082     9436     8.7 |  6.934 % |
c |      1186 |   14424    50551 |    5288    1184    14003    11.8 |  7.031 % |
c |      1336 |   14424    50551 |    5817    1334    14681    11.0 |  7.031 % |
c |      1561 |   14424    50551 |    6399    1559    16199    10.4 |  7.031 % |
c |      1898 |   14424    50551 |    7039    1896    25371    13.4 |  7.031 % |
c |      2404 |   14424    50551 |    7743    2402    35210    14.7 |  7.031 % |
c |      3163 |   14424    50551 |    8517    3161    57661    18.2 |  7.031 % |
c |      4303 |   14424    50551 |    9369    4301    95142    22.1 |  7.031 % |
c |      6012 |   14424    50551 |   10306    6010   174065    29.0 |  7.031 % |
c ==============================================================================
c [1mFound solution: 51[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 553   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6277 |   14425    50560 |    4808    6275   178481    28.4 |  7.031 % |
c |      6377 |   14425    50560 |    5288    3238    90357    27.9 |  7.063 % |
c |      6527 |   14425    50560 |    5817    3388    93958    27.7 |  7.063 % |
c |      6752 |   14425    50560 |    6399    3613    96135    26.6 |  7.063 % |
c |      7090 |   14425    50560 |    7039    3951   105767    26.8 |  7.063 % |
c ==============================================================================
c [1mFound solution: 32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 572   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7167 |   14430    50593 |    4810    4028   106717    26.5 |  7.063 % |
c |      7267 |   14430    50593 |    5291    4128   108116    26.2 |  7.190 % |
c |      7417 |   14430    50593 |    5820    4278   113933    26.6 |  7.190 % |
c |      7643 |   14430    50593 |    6402    4504   118254    26.3 |  7.190 % |
c |      7984 |   14430    50593 |    7042    4845   138004    28.5 |  7.190 % |
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 574   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8450 |   14436    50628 |    4812    5311   152319    28.7 |  7.190 % |
c |      8550 |   14436    50628 |    5293    2756    58660    21.3 |  7.254 % |
c |      8701 |   14436    50628 |    5822    2907    61760    21.2 |  7.254 % |
c |      8926 |   14436    50628 |    6404    3132    67531    21.6 |  7.254 % |
c |      9263 |   14436    50628 |    7045    3469    73166    21.1 |  7.254 % |
c |      9769 |   14436    50628 |    7749    3975    88038    22.1 |  7.254 % |
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 580   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9906 |   14440    50652 |    4813    4112    90509    22.0 |  7.254 % |
c |     10007 |   14440    50652 |    5294    4213    93637    22.2 |  7.348 % |
c |     10158 |   14440    50652 |    5823    4364    96375    22.1 |  7.348 % |
c |     10384 |   14440    50652 |    6406    4590   100135    21.8 |  7.348 % |
c |     10724 |   14440    50652 |    7046    4930   108872    22.1 |  7.348 % |
c |     11231 |   14440    50652 |    7751    5437   122263    22.5 |  7.348 % |
c |     11992 |   14440    50652 |    8526    6198   157264    25.4 |  7.348 % |
c |     13131 |   14440    50652 |    9379    7337   195834    26.7 |  7.348 % |
c |     14839 |   14440    50652 |   10317    9045   281870    31.2 |  7.348 % |
c |     17402 |   14440    50652 |   11348   11608   437872    37.7 |  7.348 % |
c |     21247 |   14440    50652 |   12483    9649   511191    53.0 |  7.348 % |
c |     27014 |   14440    50652 |   13732    8546   472436    55.3 |  7.348 % |
c |     35663 |   14440    50652 |   15105    9391   826233    88.0 |  7.348 % |
c |     48638 |   14440    50652 |   16615   14018  1224149    87.3 |  7.348 % |
c |     68102 |   14440    50652 |   18277   15726  1495947    95.1 |  7.348 % |
c |     97294 |   14440    50652 |   20105   15330  1854900   121.0 |  7.348 % |
c |    141083 |   14440    50652 |   22115   15873  2323771   146.4 |  7.348 % |
c |    206767 |   14440    50652 |   24327   12004  1034878    86.2 |  7.348 % |
c |    305293 |   14440    50652 |   26759   19139  2153512   112.5 |  7.348 % |
c |    453082 |   14440    50652 |   29435   24383  2530332   103.8 |  7.348 % |
c |    674765 |   14440    50652 |   32379   23589  2741083   116.2 |  7.348 % |
#### 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.94 0.90 2/54 17179
Raw data (stat): 17179 (runsolver) R 17178 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421618519 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+9.9999 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 1237 0 0 0 995 3 0 0 25 0 1 0 421618519 6565888 1215 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1603 1215 603 41 0 1562 0
vsize: 6412
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 1937 0 0 0 1993 6 0 0 25 0 1 0 421618519 9519104 1915 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2324 1915 603 41 0 2283 0
vsize: 9296
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 2311 0 0 0 2991 7 0 0 25 0 1 0 421618519 11124736 2289 4294967295 134512640 134672761 3221224544 3221223500 1075349993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2716 2289 603 41 0 2675 0
vsize: 10864
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 2325 0 0 0 3991 7 0 0 25 0 1 0 421618519 11124736 2303 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2716 2303 603 41 0 2675 0
vsize: 10864
[startup+50.0037 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 2390 0 0 0 4990 8 0 0 25 0 1 0 421618519 11395072 2368 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2782 2368 603 41 0 2741 0
vsize: 11128
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 2881 0 0 0 5988 10 0 0 25 0 1 0 421618519 13402112 2859 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3272 2859 603 41 0 3231 0
vsize: 13088
[startup+70.0039 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 2881 0 0 0 6988 10 0 0 25 0 1 0 421618519 13402112 2859 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3272 2859 603 41 0 3231 0
vsize: 13088
[startup+80.0052 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 3130 0 0 0 7986 12 0 0 25 0 1 0 421618519 14344192 3108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3502 3108 603 41 0 3461 0
vsize: 14008
[startup+90.0056 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 3652 0 0 0 8984 14 0 0 25 0 1 0 421618519 16486400 3630 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3630 603 41 0 3984 0
vsize: 16100
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 3652 0 0 0 9983 14 0 0 25 0 1 0 421618519 16486400 3630 4294967295 134512640 134672761 3221224544 3221223648 134560311 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3630 603 41 0 3984 0
vsize: 16100
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 3654 0 0 0 10983 14 0 0 25 0 1 0 421618519 16486400 3632 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3632 603 41 0 3984 0
vsize: 16100
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 3688 0 0 0 11982 15 0 0 25 0 1 0 421618519 16752640 3666 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4090 3666 603 41 0 4049 0
vsize: 16360
[startup+130.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 3698 0 0 0 12982 15 0 0 25 0 1 0 421618519 16752640 3676 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4090 3676 603 41 0 4049 0
vsize: 16360
[startup+140.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4255 0 0 0 13979 18 0 0 25 0 1 0 421618519 19050496 4233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4233 603 41 0 4610 0
vsize: 18604
[startup+150.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4255 0 0 0 14979 18 0 0 25 0 1 0 421618519 19050496 4233 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4233 603 41 0 4610 0
vsize: 18604
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4431 0 0 0 15978 19 0 0 25 0 1 0 421618519 19714048 4409 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4813 4409 603 41 0 4772 0
vsize: 19252
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4444 0 0 0 16978 19 0 0 25 0 1 0 421618519 19849216 4422 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4422 603 41 0 4805 0
vsize: 19384
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4445 0 0 0 17977 20 0 0 25 0 1 0 421618519 19849216 4423 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4423 603 41 0 4805 0
vsize: 19384
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4445 0 0 0 18977 20 0 0 25 0 1 0 421618519 19849216 4423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4846 4423 603 41 0 4805 0
vsize: 19384
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4445 0 0 0 19977 20 0 0 25 0 1 0 421618519 19816448 4423 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4838 4423 603 41 0 4797 0
vsize: 19352
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4445 0 0 0 20976 21 0 0 25 0 1 0 421618519 19816448 4423 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4838 4423 603 41 0 4797 0
vsize: 19352
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4445 0 0 0 21976 21 0 0 25 0 1 0 421618519 19816448 4423 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4838 4423 603 41 0 4797 0
vsize: 19352
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4445 0 0 0 22976 21 0 0 25 0 1 0 421618519 19816448 4423 4294967295 134512640 134672761 3221224544 3221223648 134555076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4838 4423 603 41 0 4797 0
vsize: 19352
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4445 0 0 0 23975 21 0 0 25 0 1 0 421618519 19816448 4423 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4838 4423 603 41 0 4797 0
vsize: 19352
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4445 0 0 0 24975 21 0 0 25 0 1 0 421618519 19812352 4423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4837 4423 603 41 0 4796 0
vsize: 19348
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4445 0 0 0 25975 22 0 0 25 0 1 0 421618519 19812352 4423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4837 4423 603 41 0 4796 0
vsize: 19348
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4445 0 0 0 26974 22 0 0 25 0 1 0 421618519 19812352 4423 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4837 4423 603 41 0 4796 0
vsize: 19348
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4448 0 0 0 27974 22 0 0 25 0 1 0 421618519 19812352 4426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4837 4426 603 41 0 4796 0
vsize: 19348
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4448 0 0 0 28973 23 0 0 25 0 1 0 421618519 19812352 4426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4837 4426 603 41 0 4796 0
vsize: 19348
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4448 0 0 0 29973 23 0 0 25 0 1 0 421618519 19812352 4426 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4837 4426 603 41 0 4796 0
vsize: 19348
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4448 0 0 0 30972 24 0 0 25 0 1 0 421618519 19812352 4426 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4837 4426 603 41 0 4796 0
vsize: 19348
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4448 0 0 0 31972 24 0 0 25 0 1 0 421618519 19812352 4426 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4837 4426 603 41 0 4796 0
vsize: 19348
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4448 0 0 0 32971 25 0 0 25 0 1 0 421618519 19812352 4426 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4837 4426 603 41 0 4796 0
vsize: 19348
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4448 0 0 0 33971 25 0 0 25 0 1 0 421618519 19812352 4426 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4837 4426 603 41 0 4796 0
vsize: 19348
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4701 0 0 0 34969 26 0 0 25 0 1 0 421618519 20885504 4679 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5099 4679 603 41 0 5058 0
vsize: 20396
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4701 0 0 0 35969 26 0 0 25 0 1 0 421618519 20885504 4679 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4679 603 41 0 5058 0
vsize: 20396
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4701 0 0 0 36969 26 0 0 25 0 1 0 421618519 20885504 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4679 603 41 0 5058 0
vsize: 20396
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4703 0 0 0 37970 26 0 0 25 0 1 0 421618519 20885504 4681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4681 603 41 0 5058 0
vsize: 20396
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4713 0 0 0 38970 26 0 0 25 0 1 0 421618519 20885504 4691 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4691 603 41 0 5058 0
vsize: 20396
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4713 0 0 0 39970 26 0 0 25 0 1 0 421618519 20885504 4691 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4691 603 41 0 5058 0
vsize: 20396
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4713 0 0 0 40970 26 0 0 25 0 1 0 421618519 20885504 4691 4294967295 134512640 134672761 3221224544 3221223728 134559342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4691 603 41 0 5058 0
vsize: 20396
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4713 0 0 0 41971 26 0 0 25 0 1 0 421618519 20885504 4691 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4691 603 41 0 5058 0
vsize: 20396
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4713 0 0 0 42970 27 0 0 25 0 1 0 421618519 20885504 4691 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4691 603 41 0 5058 0
vsize: 20396
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4715 0 0 0 43970 27 0 0 25 0 1 0 421618519 20885504 4693 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4693 603 41 0 5058 0
vsize: 20396
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4715 0 0 0 44970 27 0 0 25 0 1 0 421618519 20885504 4693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4693 603 41 0 5058 0
vsize: 20396
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4715 0 0 0 45970 27 0 0 25 0 1 0 421618519 20885504 4693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4693 603 41 0 5058 0
vsize: 20396
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4715 0 0 0 46971 27 0 0 25 0 1 0 421618519 20885504 4693 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4693 603 41 0 5058 0
vsize: 20396
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4715 0 0 0 47971 27 0 0 25 0 1 0 421618519 20885504 4693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4693 603 41 0 5058 0
vsize: 20396
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4734 0 0 0 48971 27 0 0 25 0 1 0 421618519 21020672 4712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5132 4712 603 41 0 5091 0
vsize: 20528
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4734 0 0 0 49971 27 0 0 25 0 1 0 421618519 21020672 4712 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5132 4712 603 41 0 5091 0
vsize: 20528
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4739 0 0 0 50972 27 0 0 25 0 1 0 421618519 21020672 4717 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5132 4717 603 41 0 5091 0
vsize: 20528
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4746 0 0 0 51972 27 0 0 25 0 1 0 421618519 21020672 4724 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5132 4724 603 41 0 5091 0
vsize: 20528
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4875 0 0 0 52972 27 0 0 25 0 1 0 421618519 21557248 4853 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5263 4853 603 41 0 5222 0
vsize: 21052
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4879 0 0 0 53972 27 0 0 25 0 1 0 421618519 21557248 4857 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5263 4857 603 41 0 5222 0
vsize: 21052
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4879 0 0 0 54972 27 0 0 25 0 1 0 421618519 21557248 4857 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5263 4857 603 41 0 5222 0
vsize: 21052
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4879 0 0 0 55972 27 0 0 25 0 1 0 421618519 21557248 4857 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5263 4857 603 41 0 5222 0
vsize: 21052
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4879 0 0 0 56972 27 0 0 25 0 1 0 421618519 21557248 4857 4294967295 134512640 134672761 3221224544 3221223744 134557820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5263 4857 603 41 0 5222 0
vsize: 21052
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4879 0 0 0 57972 27 0 0 25 0 1 0 421618519 21557248 4857 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5263 4857 603 41 0 5222 0
vsize: 21052
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4987 0 0 0 58972 28 0 0 25 0 1 0 421618519 22089728 4965 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5393 4965 603 41 0 5352 0
vsize: 21572
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4987 0 0 0 59972 28 0 0 25 0 1 0 421618519 22089728 4965 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5393 4965 603 41 0 5352 0
vsize: 21572
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4987 0 0 0 60973 28 0 0 25 0 1 0 421618519 22089728 4965 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5393 4965 603 41 0 5352 0
vsize: 21572
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4987 0 0 0 61973 28 0 0 25 0 1 0 421618519 22089728 4965 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5393 4965 603 41 0 5352 0
vsize: 21572
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4987 0 0 0 62973 28 0 0 25 0 1 0 421618519 22089728 4965 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5393 4965 603 41 0 5352 0
vsize: 21572
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4987 0 0 0 63973 28 0 0 25 0 1 0 421618519 22089728 4965 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5393 4965 603 41 0 5352 0
vsize: 21572
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4987 0 0 0 64973 28 0 0 25 0 1 0 421618519 22089728 4965 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5393 4965 603 41 0 5352 0
vsize: 21572
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 4987 0 0 0 65973 28 0 0 25 0 1 0 421618519 22089728 4965 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5393 4965 603 41 0 5352 0
vsize: 21572
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5073 0 0 0 66974 28 0 0 25 0 1 0 421618519 22360064 5051 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5459 5051 603 41 0 5418 0
vsize: 21836
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5079 0 0 0 67974 28 0 0 25 0 1 0 421618519 22503424 5057 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 5057 603 41 0 5453 0
vsize: 21976
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5081 0 0 0 68973 28 0 0 25 0 1 0 421618519 22503424 5059 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5494 5059 603 41 0 5453 0
vsize: 21976
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5081 0 0 0 69972 28 0 0 25 0 1 0 421618519 22503424 5059 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 5059 603 41 0 5453 0
vsize: 21976
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5082 0 0 0 70973 28 0 0 25 0 1 0 421618519 22503424 5060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 5060 603 41 0 5453 0
vsize: 21976
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5082 0 0 0 71973 28 0 0 25 0 1 0 421618519 22503424 5060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 5060 603 41 0 5453 0
vsize: 21976
[startup+730.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5082 0 0 0 72973 28 0 0 25 0 1 0 421618519 22503424 5060 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 5060 603 41 0 5453 0
vsize: 21976
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5082 0 0 0 73973 28 0 0 25 0 1 0 421618519 22503424 5060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 5060 603 41 0 5453 0
vsize: 21976
[startup+750.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5082 0 0 0 74973 28 0 0 25 0 1 0 421618519 22503424 5060 4294967295 134512640 134672761 3221224544 3221223680 134565054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 5060 603 41 0 5453 0
vsize: 21976
[startup+760.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5082 0 0 0 75973 28 0 0 25 0 1 0 421618519 22503424 5060 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 5060 603 41 0 5453 0
vsize: 21976
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5082 0 0 0 76974 28 0 0 25 0 1 0 421618519 22503424 5060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 5060 603 41 0 5453 0
vsize: 21976
[startup+780.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5227 0 0 0 77973 29 0 0 25 0 1 0 421618519 23040000 5205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5625 5205 603 41 0 5584 0
vsize: 22500
[startup+790.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5744 0 0 0 78972 30 0 0 25 0 1 0 421618519 25190400 5722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6150 5722 603 41 0 6109 0
vsize: 24600
[startup+800.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5744 0 0 0 79973 30 0 0 25 0 1 0 421618519 25190400 5722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6150 5722 603 41 0 6109 0
vsize: 24600
[startup+810.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5749 0 0 0 80973 30 0 0 25 0 1 0 421618519 25190400 5727 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6150 5727 603 41 0 6109 0
vsize: 24600
[startup+820.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5759 0 0 0 81973 30 0 0 25 0 1 0 421618519 25190400 5737 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6150 5737 603 41 0 6109 0
vsize: 24600
[startup+830.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5759 0 0 0 82973 30 0 0 25 0 1 0 421618519 25190400 5737 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6150 5737 603 41 0 6109 0
vsize: 24600
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5760 0 0 0 83973 30 0 0 25 0 1 0 421618519 25190400 5738 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6150 5738 603 41 0 6109 0
vsize: 24600
[startup+850.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5767 0 0 0 84974 30 0 0 25 0 1 0 421618519 25337856 5745 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6186 5745 603 41 0 6145 0
vsize: 24744
[startup+860.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5767 0 0 0 85974 30 0 0 25 0 1 0 421618519 25337856 5745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6186 5745 603 41 0 6145 0
vsize: 24744
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5773 0 0 0 86974 30 0 0 25 0 1 0 421618519 25337856 5751 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6186 5751 603 41 0 6145 0
vsize: 24744
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5774 0 0 0 87974 30 0 0 25 0 1 0 421618519 25337856 5752 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6186 5752 603 41 0 6145 0
vsize: 24744
[startup+890.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5774 0 0 0 88974 30 0 0 25 0 1 0 421618519 25337856 5752 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6186 5752 603 41 0 6145 0
vsize: 24744
[startup+900.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5774 0 0 0 89974 30 0 0 25 0 1 0 421618519 25337856 5752 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6186 5752 603 41 0 6145 0
vsize: 24744
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5774 0 0 0 90974 30 0 0 25 0 1 0 421618519 25337856 5752 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6186 5752 603 41 0 6145 0
vsize: 24744
[startup+920.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5863 0 0 0 91975 30 0 0 25 0 1 0 421618519 25616384 5841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6254 5841 603 41 0 6213 0
vsize: 25016
[startup+930.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5867 0 0 0 92975 30 0 0 25 0 1 0 421618519 25755648 5845 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5845 603 41 0 6247 0
vsize: 25152
[startup+940.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5867 0 0 0 93975 30 0 0 25 0 1 0 421618519 25755648 5845 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5845 603 41 0 6247 0
vsize: 25152
[startup+950.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5867 0 0 0 94975 30 0 0 25 0 1 0 421618519 25755648 5845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5845 603 41 0 6247 0
vsize: 25152
[startup+960.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5873 0 0 0 95975 30 0 0 25 0 1 0 421618519 25755648 5851 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5851 603 41 0 6247 0
vsize: 25152
[startup+970.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5874 0 0 0 96976 30 0 0 25 0 1 0 421618519 25755648 5852 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5852 603 41 0 6247 0
vsize: 25152
[startup+980.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5874 0 0 0 97976 30 0 0 25 0 1 0 421618519 25755648 5852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5852 603 41 0 6247 0
vsize: 25152
[startup+990.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5874 0 0 0 98976 30 0 0 25 0 1 0 421618519 25755648 5852 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5852 603 41 0 6247 0
vsize: 25152
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5874 0 0 0 99976 30 0 0 25 0 1 0 421618519 25755648 5852 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5852 603 41 0 6247 0
vsize: 25152
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5875 0 0 0 100976 30 0 0 25 0 1 0 421618519 25755648 5853 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5853 603 41 0 6247 0
vsize: 25152
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5875 0 0 0 101977 30 0 0 25 0 1 0 421618519 25755648 5853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5853 603 41 0 6247 0
vsize: 25152
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5875 0 0 0 102977 30 0 0 25 0 1 0 421618519 25755648 5853 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5853 603 41 0 6247 0
vsize: 25152
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5875 0 0 0 103977 30 0 0 25 0 1 0 421618519 25755648 5853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5853 603 41 0 6247 0
vsize: 25152
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5875 0 0 0 104977 30 0 0 25 0 1 0 421618519 25755648 5853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5853 603 41 0 6247 0
vsize: 25152
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5875 0 0 0 105977 30 0 0 25 0 1 0 421618519 25755648 5853 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5853 603 41 0 6247 0
vsize: 25152
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5875 0 0 0 106978 30 0 0 25 0 1 0 421618519 25755648 5853 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5853 603 41 0 6247 0
vsize: 25152
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5875 0 0 0 107978 30 0 0 25 0 1 0 421618519 25755648 5853 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5853 603 41 0 6247 0
vsize: 25152
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5875 0 0 0 108978 30 0 0 25 0 1 0 421618519 25755648 5853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5853 603 41 0 6247 0
vsize: 25152
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 5875 0 0 0 109978 30 0 0 25 0 1 0 421618519 25755648 5853 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6288 5853 603 41 0 6247 0
vsize: 25152
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 6185 0 0 0 110977 31 0 0 25 0 1 0 421618519 27086848 6163 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6613 6163 603 41 0 6572 0
vsize: 26452
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 6188 0 0 0 111978 31 0 0 25 0 1 0 421618519 27086848 6166 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6613 6166 603 41 0 6572 0
vsize: 26452
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 6188 0 0 0 112978 31 0 0 25 0 1 0 421618519 27086848 6166 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6613 6166 603 41 0 6572 0
vsize: 26452
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 6205 0 0 0 113978 31 0 0 25 0 1 0 421618519 27230208 6183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6648 6183 603 41 0 6607 0
vsize: 26592
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 6205 0 0 0 114978 31 0 0 25 0 1 0 421618519 27230208 6183 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6648 6183 603 41 0 6607 0
vsize: 26592
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 6205 0 0 0 115978 31 0 0 25 0 1 0 421618519 27230208 6183 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6648 6183 603 41 0 6607 0
vsize: 26592
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 6205 0 0 0 116978 31 0 0 25 0 1 0 421618519 27230208 6183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6648 6183 603 41 0 6607 0
vsize: 26592
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 6205 0 0 0 117979 31 0 0 25 0 1 0 421618519 27230208 6183 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6648 6183 603 41 0 6607 0
vsize: 26592
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 6205 0 0 0 118979 31 0 0 25 0 1 0 421618519 27230208 6183 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6648 6183 603 41 0 6607 0
vsize: 26592
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17179
Raw data (stat): 17179 (minisat+) R 17178 10720 10719 0 -1 0 6205 0 0 0 119979 31 0 0 25 0 1 0 421618519 27230208 6183 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6648 6183 603 41 0 6607 0
vsize: 26592
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 17179
Raw data (stat): 17179 (minisat+) Z 17178 10720 10719 0 -1 12 6208 0 0 0 119979 33 0 0 25 0 1 0 421618519 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: 10
Real time (s): 1200.06
CPU time (s): 1200.13
CPU user time (s): 1199.8
CPU system time (s): 0.330949
CPU usage (%): 100.006
Max. virtual memory (Kb): 26592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####