Some explanations

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

General information on the benchmark

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl50_55_pb.cnf.cr.opb
MD5SUM88aaed929c30a489c8806c3852596de3
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 56
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.173973
Number of variables5500
Total number of constraints210
Number of constraints which are clauses110
Number of constraints which are cardinality constraints (but not clauses)100
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint50
Maximum length of a constraint55

Trace number 4630 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-13 19:26:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3405 boxname=wulflinc10 idbench=21 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  88aaed929c30a489c8806c3852596de3  /oldhome/oroussel/tmp/wulflinc10/normalized-chnl50_55_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc10/normalized-chnl50_55_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc10/normalized-chnl50_55_pb.cnf.cr.opb
IDLAUNCH: 3405
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        911156 kB
Buffers:         33684 kB
Cached:          70736 kB
SwapCached:        164 kB
Active:          48332 kB
Inactive:        59100 kB
HighTotal:      131008 kB
HighFree:        56532 kB
LowTotal:       903652 kB
LowFree:        854624 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10568 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:46:49 (client local time) WITH STATUS 0 IN 1210.05 SECONDS
stats: 3405 7 1210.05 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 210 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................
c ---[  99]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  98]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  97]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  96]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  95]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  94]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  93]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  92]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  91]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  90]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  89]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  88]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  87]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  86]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  85]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  84]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  83]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  82]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  81]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  80]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  79]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  78]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  77]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  76]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  75]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  74]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  73]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  72]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  71]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  70]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  69]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  68]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  67]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  66]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  65]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  64]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  63]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  62]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  61]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  60]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  59]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  58]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  57]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  56]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  55]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  54]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  53]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  52]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  51]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  50]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  49]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  48]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  47]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  46]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  45]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  44]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  43]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  42]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  41]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  40]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  39]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  38]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  37]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  36]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  35]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  34]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  33]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  32]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  31]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  30]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  29]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  28]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  27]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  26]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  25]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  24]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  23]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  22]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  21]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  20]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  19]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  18]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  17]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  16]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  15]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  14]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  13]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  12]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  11]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  10]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[   9]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[   8]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[   7]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[   6]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[   5]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[   4]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[   3]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[   2]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[   1]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[   0]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   67510   245600 |   22503       0        0     nan |  0.000 % |
c |       100 |   65601   238462 |   24753      16       46     2.9 |  6.395 % |
c |       250 |   65217   237034 |   27228     147      755     5.1 |  6.987 % |
c |       475 |   65103   236649 |   29951     351     2166     6.2 |  7.127 % |
c |       812 |   64809   235637 |   32946     639     3458     5.4 |  7.439 % |
c |      1318 |   63971   232777 |   36241    1010     5069     5.0 |  8.338 % |
c |      2078 |   63138   229962 |   39865    1652     7937     4.8 |  9.268 % |
c |      3217 |   61355   223789 |   43851    2543    12445     4.9 | 11.223 % |
c |      4925 |   57213   209241 |   48237    3647    18463     5.1 | 15.783 % |
c |      7488 |   42371   157791 |   53060    3824    24288     6.4 | 32.159 % |
c |     11332 |   30179   116769 |   58366    5840    55029     9.4 | 46.771 % |
c |     17098 |   30046   116340 |   64203   11589  1874749   161.8 | 46.955 % |
c |     25747 |   30046   116340 |   70624   20238  7059827   348.8 | 46.955 % |
c |     38722 |   30046   116340 |   77686   33213 14957649   450.4 | 46.955 % |
c |     58188 |   30037   116311 |   85455   52678 27272121   517.7 | 46.968 % |
c |     87380 |   29803   115557 |   94000   81843 47107142   575.6 | 47.299 % |
c |    131172 |   29803   115557 |  103400   38513 25800335   669.9 | 47.299 % |
#### 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.08 0.02 0.01 2/54 27192
Raw data (stat): 27192 (runsolver) R 27191 25347 25346 0 -1 64 2 0 0 0 0 0 0 0 19 0 1 0 420246710 1052672 97 4294967295 134512640 135381576 3221224432 3221219840 134517031 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.22 0.05 0.02 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 1820 0 1 0 982 5 0 0 25 0 1 0 420246710 9146368 1753 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1753 603 41 0 2192 0
vsize: 8932
[startup+20.0016 s]
Raw data (loadavg): 0.34 0.08 0.02 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 1826 0 1 0 1982 5 0 0 25 0 1 0 420246710 9146368 1759 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1759 603 41 0 2192 0
vsize: 8932
[startup+30.0027 s]
Raw data (loadavg): 0.44 0.11 0.03 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 1830 0 1 0 2982 5 0 0 25 0 1 0 420246710 9146368 1763 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1763 603 41 0 2192 0
vsize: 8932
[startup+40.0026 s]
Raw data (loadavg): 0.53 0.14 0.04 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 1831 0 1 0 3982 5 0 0 25 0 1 0 420246710 9146368 1764 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1764 603 41 0 2192 0
vsize: 8932
[startup+50.0032 s]
Raw data (loadavg): 0.60 0.17 0.05 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 1833 0 1 0 4981 6 0 0 25 0 1 0 420246710 9146368 1766 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1766 603 41 0 2192 0
vsize: 8932
[startup+60.0033 s]
Raw data (loadavg): 0.66 0.19 0.06 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 1835 0 1 0 5981 6 0 0 25 0 1 0 420246710 9146368 1768 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1768 603 41 0 2192 0
vsize: 8932
[startup+70.0043 s]
Raw data (loadavg): 0.71 0.22 0.07 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 1842 0 1 0 6981 6 0 0 25 0 1 0 420246710 9281536 1775 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2266 1775 603 41 0 2225 0
vsize: 9064
[startup+80.0049 s]
Raw data (loadavg): 0.76 0.24 0.08 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 1844 0 1 0 7980 6 0 0 25 0 1 0 420246710 9281536 1777 4294967295 134512640 134672761 3221224544 3221223800 134562287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2266 1777 603 41 0 2225 0
vsize: 9064
[startup+90.005 s]
Raw data (loadavg): 0.79 0.27 0.09 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 2088 0 1 0 8980 7 0 0 25 0 1 0 420246710 10227712 2021 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2497 2021 603 41 0 2456 0
vsize: 9988
[startup+100.005 s]
Raw data (loadavg): 0.82 0.29 0.10 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 3660 0 1 0 9976 11 0 0 25 0 1 0 420246710 16732160 3593 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4085 3593 603 41 0 4044 0
vsize: 16340
[startup+110.006 s]
Raw data (loadavg): 0.85 0.31 0.11 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 6107 0 1 0 10970 17 0 0 25 0 1 0 420246710 26726400 6040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6525 6040 603 41 0 6484 0
vsize: 26100
[startup+120.006 s]
Raw data (loadavg): 0.87 0.34 0.12 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 7939 0 1 0 11965 21 0 0 25 0 1 0 420246710 34299904 7872 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8374 7872 603 41 0 8333 0
vsize: 33496
[startup+130.007 s]
Raw data (loadavg): 0.89 0.36 0.13 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 9426 0 1 0 12961 26 0 0 25 0 1 0 420246710 40378368 9359 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9858 9359 603 41 0 9817 0
vsize: 39432
[startup+140.007 s]
Raw data (loadavg): 0.91 0.38 0.14 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 10946 0 1 0 13957 30 0 0 25 0 1 0 420246710 46604288 10879 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11378 10879 603 41 0 11337 0
vsize: 45512
[startup+150.007 s]
Raw data (loadavg): 0.92 0.40 0.15 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 12208 0 1 0 14954 33 0 0 25 0 1 0 420246710 51744768 12141 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12633 12141 603 41 0 12592 0
vsize: 50532
[startup+160.007 s]
Raw data (loadavg): 0.93 0.42 0.15 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 13330 0 1 0 15950 36 0 0 25 0 1 0 420246710 56348672 13263 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13757 13263 603 41 0 13716 0
vsize: 55028
[startup+170.007 s]
Raw data (loadavg): 0.94 0.44 0.16 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 14222 0 1 0 16948 38 0 0 25 0 1 0 420246710 60030976 14155 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14656 14155 603 41 0 14615 0
vsize: 58624
[startup+180.007 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 14886 0 1 0 17946 41 0 0 25 0 1 0 420246710 62738432 14819 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15317 14819 603 41 0 15276 0
vsize: 61268
[startup+190.008 s]
Raw data (loadavg): 0.96 0.47 0.18 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 15618 0 1 0 18944 43 0 0 25 0 1 0 420246710 65847296 15551 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16076 15551 603 41 0 16035 0
vsize: 64304
[startup+200.008 s]
Raw data (loadavg): 0.96 0.49 0.19 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 16138 0 1 0 19942 45 0 0 25 0 1 0 420246710 67870720 16071 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16570 16071 603 41 0 16529 0
vsize: 66280
[startup+210.008 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 16799 0 1 0 20939 48 0 0 25 0 1 0 420246710 70574080 16732 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17230 16732 603 41 0 17189 0
vsize: 68920
[startup+220.009 s]
Raw data (loadavg): 0.97 0.52 0.20 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 17437 0 1 0 21938 49 0 0 25 0 1 0 420246710 73416704 17370 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17924 17370 603 41 0 17883 0
vsize: 71696
[startup+230.009 s]
Raw data (loadavg): 0.98 0.54 0.21 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 18753 0 1 0 22935 53 0 0 25 0 1 0 420246710 78815232 18686 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19242 18686 603 41 0 19201 0
vsize: 76968
[startup+240.009 s]
Raw data (loadavg): 0.98 0.55 0.22 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 19645 0 1 0 23932 55 0 0 25 0 1 0 420246710 82464768 19578 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20133 19578 603 41 0 20092 0
vsize: 80532
[startup+250.009 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 20551 0 1 0 24929 58 0 0 25 0 1 0 420246710 86114304 20484 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21024 20484 603 41 0 20983 0
vsize: 84096
[startup+260.01 s]
Raw data (loadavg): 0.98 0.58 0.24 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 21396 0 1 0 25926 61 0 0 25 0 1 0 420246710 89624576 21329 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21881 21329 603 41 0 21840 0
vsize: 87524
[startup+270.009 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 22066 0 1 0 26923 64 0 0 25 0 1 0 420246710 92323840 21999 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22540 21999 603 41 0 22499 0
vsize: 90160
[startup+280.01 s]
Raw data (loadavg): 0.99 0.61 0.25 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 22695 0 1 0 27921 66 0 0 25 0 1 0 420246710 94892032 22628 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23167 22628 603 41 0 23126 0
vsize: 92668
[startup+290.011 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 23409 0 1 0 28919 68 0 0 25 0 1 0 420246710 97873920 23342 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23895 23342 603 41 0 23854 0
vsize: 95580
[startup+300.011 s]
Raw data (loadavg): 0.99 0.63 0.27 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 24055 0 1 0 29918 69 0 0 25 0 1 0 420246710 100446208 23988 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24523 23988 603 41 0 24482 0
vsize: 98092
[startup+310.012 s]
Raw data (loadavg): 0.99 0.64 0.28 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 24798 0 1 0 30916 71 0 0 25 0 1 0 420246710 103555072 24731 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25282 24731 603 41 0 25241 0
vsize: 101128
[startup+320.011 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 25604 0 1 0 31914 73 0 0 25 0 1 0 420246710 106795008 25537 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26073 25537 603 41 0 26032 0
vsize: 104292
[startup+330.012 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 26203 0 1 0 32912 75 0 0 25 0 1 0 420246710 109264896 26136 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26676 26136 603 41 0 26635 0
vsize: 106704
[startup+340.012 s]
Raw data (loadavg): 0.99 0.67 0.30 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 26980 0 1 0 33910 78 0 0 25 0 1 0 420246710 112508928 26913 4294967295 134512640 134672761 3221224544 3221223636 1075351193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27468 26913 603 41 0 27427 0
vsize: 109872
[startup+350.012 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 27785 0 1 0 34907 80 0 0 25 0 1 0 420246710 115752960 27718 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28260 27718 603 41 0 28219 0
vsize: 113040
[startup+360.014 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 28491 0 1 0 35905 82 0 0 25 0 1 0 420246710 118743040 28424 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28990 28424 603 41 0 28949 0
vsize: 115960
[startup+370.013 s]
Raw data (loadavg): 0.99 0.70 0.32 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 29035 0 1 0 36904 83 0 0 25 0 1 0 420246710 120930304 28968 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29524 28968 603 41 0 29483 0
vsize: 118096
[startup+380.014 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 29550 0 1 0 37903 84 0 0 25 0 1 0 420246710 122957824 29483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30019 29483 603 41 0 29978 0
vsize: 120076
[startup+390.014 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 30686 0 1 0 38900 88 0 0 25 0 1 0 420246710 127651840 30619 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31165 30619 603 41 0 31124 0
vsize: 124660
[startup+400.015 s]
Raw data (loadavg): 0.99 0.73 0.34 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 31039 0 1 0 39899 89 0 0 25 0 1 0 420246710 129183744 30972 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31539 30972 603 41 0 31498 0
vsize: 126156
[startup+410.016 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 31106 0 1 0 40898 89 0 0 25 0 1 0 420246710 129458176 31039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31606 31039 603 41 0 31565 0
vsize: 126424
[startup+420.016 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 31126 0 1 0 41898 90 0 0 25 0 1 0 420246710 129593344 31059 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31639 31059 603 41 0 31598 0
vsize: 126556
[startup+430.017 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 31366 0 1 0 42897 90 0 0 25 0 1 0 420246710 130555904 31299 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31874 31299 603 41 0 31833 0
vsize: 127496
[startup+440.017 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 31887 0 1 0 43896 92 0 0 25 0 1 0 420246710 132722688 31820 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32403 31820 603 41 0 32362 0
vsize: 129612
[startup+450.017 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 33335 0 1 0 44892 95 0 0 25 0 1 0 420246710 138678272 33268 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33857 33268 603 41 0 33816 0
vsize: 135428
[startup+460.017 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 34587 0 1 0 45888 99 0 0 25 0 1 0 420246710 143773696 34520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35101 34520 603 41 0 35060 0
vsize: 140404
[startup+470.018 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 35723 0 1 0 46885 102 0 0 25 0 1 0 420246710 148459520 35656 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36245 35656 603 41 0 36204 0
vsize: 144980
[startup+480.018 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 36613 0 1 0 47882 105 0 0 25 0 1 0 420246710 152104960 36546 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37135 36546 603 41 0 37094 0
vsize: 148540
[startup+490.019 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 37364 0 1 0 48880 107 0 0 25 0 1 0 420246710 155209728 37297 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37893 37297 603 41 0 37852 0
vsize: 151572
[startup+500.02 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 38025 0 1 0 49879 108 0 0 25 0 1 0 420246710 158171136 37958 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38616 37958 603 41 0 38575 0
vsize: 154464
[startup+510.02 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 38771 0 1 0 50877 111 0 0 25 0 1 0 420246710 161259520 38704 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39370 38704 603 41 0 39329 0
vsize: 157480
[startup+520.02 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 39821 0 1 0 51873 114 0 0 25 0 1 0 420246710 165580800 39754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40425 39754 603 41 0 40384 0
vsize: 161700
[startup+530.021 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 40933 0 1 0 52871 117 0 0 25 0 1 0 420246710 170049536 40866 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41516 40866 603 41 0 41475 0
vsize: 166064
[startup+540.022 s]
Raw data (loadavg): 0.99 0.83 0.42 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 41979 0 1 0 53868 120 0 0 25 0 1 0 420246710 174379008 41912 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42573 41912 603 41 0 42532 0
vsize: 170292
[startup+550.021 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 43062 0 1 0 54866 122 0 0 25 0 1 0 420246710 178843648 42995 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43663 42995 603 41 0 43622 0
vsize: 174652
[startup+560.022 s]
Raw data (loadavg): 0.99 0.84 0.43 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 44059 0 1 0 55863 125 0 0 25 0 1 0 420246710 182894592 43992 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44652 43992 603 41 0 44611 0
vsize: 178608
[startup+570.023 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 44825 0 1 0 56861 127 0 0 25 0 1 0 420246710 186003456 44758 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45411 44758 603 41 0 45370 0
vsize: 181644
[startup+580.023 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 45437 0 1 0 57859 128 0 0 25 0 1 0 420246710 188563456 45370 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46036 45370 603 41 0 45995 0
vsize: 184144
[startup+590.024 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 46051 0 1 0 58857 130 0 0 25 0 1 0 420246710 191115264 45984 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46659 45984 603 41 0 46618 0
vsize: 186636
[startup+600.024 s]
Raw data (loadavg): 0.99 0.85 0.46 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 46784 0 1 0 59856 132 0 0 25 0 1 0 420246710 194093056 46717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47386 46717 603 41 0 47345 0
vsize: 189544
[startup+610.025 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 47497 0 1 0 60854 134 0 0 25 0 1 0 420246710 197074944 47430 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48114 47430 603 41 0 48073 0
vsize: 192456
[startup+620.024 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 48342 0 1 0 61851 137 0 0 25 0 1 0 420246710 200450048 48275 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48938 48275 603 41 0 48897 0
vsize: 195752
[startup+630.025 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 49137 0 1 0 62848 140 0 0 25 0 1 0 420246710 203698176 49070 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49731 49070 603 41 0 49690 0
vsize: 198924
[startup+640.025 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 49923 0 1 0 63845 143 0 0 25 0 1 0 420246710 206929920 49856 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50520 49856 603 41 0 50479 0
vsize: 202080
[startup+650.025 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 50894 0 1 0 64843 145 0 0 25 0 1 0 420246710 210980864 50827 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51509 50827 603 41 0 51468 0
vsize: 206036
[startup+660.025 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 52843 0 1 0 65837 151 0 0 25 0 1 0 420246710 218943488 52776 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53453 52776 603 41 0 53412 0
vsize: 213812
[startup+670.026 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 54772 0 1 0 66831 156 0 0 25 0 1 0 420246710 226881536 54705 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55391 54705 603 41 0 55350 0
vsize: 221564
[startup+680.027 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 56377 0 1 0 67827 161 0 0 25 0 1 0 420246710 233443328 56310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56993 56310 603 41 0 56952 0
vsize: 227972
[startup+690.027 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 57884 0 1 0 68823 165 0 0 25 0 1 0 420246710 239579136 57817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58491 57817 603 41 0 58450 0
vsize: 233964
[startup+700.027 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 59233 0 1 0 69818 169 0 0 25 0 1 0 420246710 245100544 59166 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59839 59166 603 41 0 59798 0
vsize: 239356
[startup+710.028 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 60386 0 1 0 70815 172 0 0 25 0 1 0 420246710 249823232 60319 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60992 60319 603 41 0 60951 0
vsize: 243968
[startup+720.028 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 61643 0 1 0 71812 176 0 0 25 0 1 0 420246710 254967808 61576 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62248 61576 603 41 0 62207 0
vsize: 248992
[startup+730.029 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 62883 0 1 0 72808 180 0 0 25 0 1 0 420246710 260112384 62816 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63504 62816 603 41 0 63463 0
vsize: 254016
[startup+740.029 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 63833 0 1 0 73805 182 0 0 25 0 1 0 420246710 264048640 63766 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64465 63766 603 41 0 64424 0
vsize: 257860
[startup+750.029 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 64740 0 1 0 74803 185 0 0 25 0 1 0 420246710 267718656 64673 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65361 64673 603 41 0 65320 0
vsize: 261444
[startup+760.029 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 65580 0 1 0 75800 187 0 0 25 0 1 0 420246710 271216640 65513 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66215 65513 603 41 0 66174 0
vsize: 264860
[startup+770.03 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66003 0 1 0 76799 188 0 0 25 0 1 0 420246710 272965632 65936 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65936 603 41 0 66601 0
vsize: 266568
[startup+780.031 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66005 0 1 0 77799 189 0 0 25 0 1 0 420246710 272965632 65938 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65938 603 41 0 66601 0
vsize: 266568
[startup+790.032 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66006 0 1 0 78798 189 0 0 25 0 1 0 420246710 272965632 65939 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65939 603 41 0 66601 0
vsize: 266568
[startup+800.031 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66006 0 1 0 79798 190 0 0 25 0 1 0 420246710 272965632 65939 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65939 603 41 0 66601 0
vsize: 266568
[startup+810.032 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66006 0 1 0 80798 190 0 0 25 0 1 0 420246710 272965632 65939 4294967295 134512640 134672761 3221224544 3221223728 134558930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65939 603 41 0 66601 0
vsize: 266568
[startup+820.033 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66006 0 1 0 81797 190 0 0 25 0 1 0 420246710 272965632 65939 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65939 603 41 0 66601 0
vsize: 266568
[startup+830.033 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66008 0 1 0 82797 191 0 0 25 0 1 0 420246710 272965632 65941 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65941 603 41 0 66601 0
vsize: 266568
[startup+840.034 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66008 0 1 0 83797 191 0 0 25 0 1 0 420246710 272965632 65941 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65941 603 41 0 66601 0
vsize: 266568
[startup+850.034 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66011 0 1 0 84797 191 0 0 25 0 1 0 420246710 272965632 65944 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65944 603 41 0 66601 0
vsize: 266568
[startup+860.035 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66015 0 1 0 85796 191 0 0 25 0 1 0 420246710 272965632 65948 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65948 603 41 0 66601 0
vsize: 266568
[startup+870.035 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66016 0 1 0 86796 192 0 0 25 0 1 0 420246710 272965632 65949 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65949 603 41 0 66601 0
vsize: 266568
[startup+880.037 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66016 0 1 0 87796 192 0 0 25 0 1 0 420246710 272965632 65949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65949 603 41 0 66601 0
vsize: 266568
[startup+890.038 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66017 0 1 0 88796 192 0 0 25 0 1 0 420246710 272965632 65950 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65950 603 41 0 66601 0
vsize: 266568
[startup+900.037 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66018 0 1 0 89796 192 0 0 25 0 1 0 420246710 272965632 65951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65951 603 41 0 66601 0
vsize: 266568
[startup+910.038 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66018 0 1 0 90795 192 0 0 25 0 1 0 420246710 272965632 65951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65951 603 41 0 66601 0
vsize: 266568
[startup+920.038 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66019 0 1 0 91795 193 0 0 25 0 1 0 420246710 272965632 65952 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65952 603 41 0 66601 0
vsize: 266568
[startup+930.039 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66019 0 1 0 92795 193 0 0 25 0 1 0 420246710 272965632 65952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65952 603 41 0 66601 0
vsize: 266568
[startup+940.039 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66019 0 1 0 93794 194 0 0 25 0 1 0 420246710 272965632 65952 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65952 603 41 0 66601 0
vsize: 266568
[startup+950.039 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66019 0 1 0 94794 194 0 0 25 0 1 0 420246710 272965632 65952 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65952 603 41 0 66601 0
vsize: 266568
[startup+960.039 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66019 0 1 0 95794 194 0 0 25 0 1 0 420246710 272965632 65952 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65952 603 41 0 66601 0
vsize: 266568
[startup+970.04 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66019 0 1 0 96794 194 0 0 25 0 1 0 420246710 272965632 65952 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65952 603 41 0 66601 0
vsize: 266568
[startup+980.04 s]
Raw data (loadavg): 1.07 0.96 0.63 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66019 0 1 0 97794 194 0 0 25 0 1 0 420246710 272965632 65952 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65952 603 41 0 66601 0
vsize: 266568
[startup+990.04 s]
Raw data (loadavg): 1.06 0.96 0.63 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66019 0 1 0 98793 195 0 0 25 0 1 0 420246710 272965632 65952 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66642 65952 603 41 0 66601 0
vsize: 266568
[startup+1000.04 s]
Raw data (loadavg): 1.05 0.97 0.64 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66020 0 1 0 99793 195 0 0 25 0 1 0 420246710 272965632 65953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65953 603 41 0 66601 0
vsize: 266568
[startup+1010.04 s]
Raw data (loadavg): 1.04 0.97 0.64 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66020 0 1 0 100793 195 0 0 25 0 1 0 420246710 272965632 65953 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65953 603 41 0 66601 0
vsize: 266568
[startup+1020.04 s]
Raw data (loadavg): 1.03 0.97 0.64 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66020 0 1 0 101794 195 0 0 25 0 1 0 420246710 272965632 65953 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65953 603 41 0 66601 0
vsize: 266568
[startup+1030.04 s]
Raw data (loadavg): 1.03 0.97 0.65 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 102794 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1040.04 s]
Raw data (loadavg): 1.02 0.97 0.65 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 103794 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1050.04 s]
Raw data (loadavg): 1.02 0.97 0.65 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 104794 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1060.04 s]
Raw data (loadavg): 1.02 0.97 0.65 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 105795 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223728 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1070.04 s]
Raw data (loadavg): 1.01 0.97 0.66 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 106795 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1080.04 s]
Raw data (loadavg): 1.01 0.97 0.66 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 107795 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1090.04 s]
Raw data (loadavg): 1.01 0.97 0.66 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 108795 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1100.04 s]
Raw data (loadavg): 1.01 0.97 0.67 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 109795 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.97 0.67 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 110796 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.97 0.67 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 111796 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 112796 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 113796 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 114796 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 115796 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 116797 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 117797 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 118797 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.97 0.70 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 119797 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
[startup+1210.04 s]
Raw data (loadavg): 1.00 0.97 0.70 2/54 27192
Raw data (stat): 27192 (minisat+) R 27191 25347 25346 0 -1 0 66021 0 1 0 120797 195 0 0 25 0 1 0 420246710 272965632 65954 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66642 65954 603 41 0 66601 0
vsize: 266568
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.17 s]
Raw data (loadavg): 1.00 0.97 0.70 1/54 27192
Raw data (stat): 27192 (minisat+) Z 27191 25347 25346 0 -1 12 66023 0 1 0 120798 207 0 0 25 0 1 0 420246710 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1210.17
CPU time (s): 1210.05
CPU user time (s): 1207.98
CPU system time (s): 2.07368
CPU usage (%): 99.9908
Max. virtual memory (Kb): 266568
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####