Some explanations

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

General information on the benchmark

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-opt1217.opb
MD5SUM697fa5beb3d240bccfa43a29ef9b4fb8
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -2048
Optimality of the best value was proved NO
Number of terms in the objective function 16
Biggest coefficient in the objective function 32768
Number of bits for the biggest coefficient in the objective function 16
Sum of the numbers in the objective function 65535
Number of bits of the sum of numbers in the objective function 16
Biggest number in a constraint 49152
Number of bits of the biggest number in a constraint 16
Biggest sum of numbers in a constraint 114687
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.03
Number of variables784
Total number of constraints833
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)816
Number of constraints which are nor clauses,nor cardinality constraints17
Minimum length of a constraint1
Maximum length of a constraint64

Trace number 18542 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        821664 kB
Buffers:         17088 kB
Cached:         175148 kB
SwapCached:        544 kB
Active:          24724 kB
Inactive:       169492 kB
HighTotal:      131008 kB
HighFree:        49252 kB
LowTotal:       903652 kB
LowFree:        772412 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13104 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:48:31 (client local time) WITH STATUS 0 IN 1200.4 SECONDS
stats: 17872 7 1200.4 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 113 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 111]---> Adder-cost: 113   maxlim: 16382   bits: 15/14
c ---[ 110]---> Adder-cost: 115   maxlim: 16382   bits: 15/14
c ---[ 109]---> Adder-cost: 133   maxlim: 16382   bits: 15/14
c ---[ 108]---> Adder-cost: 148   maxlim: 16382   bits: 15/14
c ---[ 107]---> Adder-cost: 139   maxlim: 16382   bits: 15/14
c ---[ 106]---> Adder-cost: 142   maxlim: 16382   bits: 15/14
c ---[ 105]---> Adder-cost: 120   maxlim: 16382   bits: 15/14
c ---[ 104]---> Adder-cost: 124   maxlim: 16382   bits: 15/14
c ---[ 102]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 100]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  98]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  97]---> Adder-cost: 107   maxlim: 16382   bits: 15/14
c ---[  95]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  93]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  91]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  89]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  87]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  85]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  83]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  81]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  79]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  77]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  76]---> Adder-cost: 113   maxlim: 16382   bits: 15/14
c ---[  74]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  72]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  70]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  68]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  66]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  64]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  62]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  60]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  58]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  56]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  55]---> Adder-cost: 139   maxlim: 16382   bits: 15/14
c ---[  53]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  51]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  49]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  47]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  45]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  43]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  41]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  39]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  37]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  35]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  34]---> Adder-cost: 121   maxlim: 16382   bits: 15/14
c ---[  32]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  30]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  28]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  26]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  24]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  22]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  20]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  18]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  16]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  14]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  13]---> Adder-cost: 100   maxlim: 16382   bits: 15/14
c ---[  11]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[   9]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[   7]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[   5]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[   3]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[   2]---> Adder-cost: 129   maxlim: 16382   bits: 15/14
c ---[   1]---> Adder-cost: 135   maxlim: 16382   bits: 15/14
c ---[   0]---> Adder-cost: 119   maxlim: 16382   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   21876    78120 |    7292       0        0     nan |  0.000 % |
c |       100 |   21868    78094 |    8021      99      362     3.7 | 14.190 % |
c |       251 |   21835    77991 |    8823     247      900     3.6 | 14.320 % |
c |       476 |   21596    77218 |    9705     450     1770     3.9 | 15.289 % |
c |       813 |   21417    76623 |   10676     764     3606     4.7 | 15.935 % |
c |      1319 |   21067    75499 |   11743    1228     6196     5.0 | 17.442 % |
c |      2078 |   20292    72922 |   12918    1877    11535     6.1 | 20.693 % |
c |      3217 |   20227    72703 |   14210    3003    31398    10.5 | 20.952 % |
c |      4927 |   19928    71732 |   15631    4681    52269    11.2 | 22.351 % |
c |      7489 |   19902    71640 |   17194    7241    99684    13.8 | 22.459 % |
c |     11333 |   19695    70963 |   18913   11059   176427    16.0 | 23.342 % |
c |     17099 |   19695    70963 |   20804   16825   304249    18.1 | 23.342 % |
c |     25748 |   19695    70963 |   22885   14464   283712    19.6 | 23.342 % |
c |     38723 |   19695    70963 |   25173   15407   282092    18.3 | 23.342 % |
c |     58184 |   19082    68948 |   27691   21491   569806    26.5 | 25.818 % |
c |     87377 |   19048    68838 |   30460   20452   519547    25.4 | 25.969 % |
c |    131166 |   19022    68758 |   33506   28770  1036681    36.0 | 26.098 % |
c |    196850 |   19014    68732 |   36857   18076   474669    26.3 | 26.120 % |
c |    295376 |   18997    68681 |   40542   27163   872421    32.1 | 26.206 % |
c |    443165 |   18997    68681 |   44597   17834   451110    25.3 | 26.206 % |
c |    664848 |   18757    67887 |   49056   34288  1349622    39.4 | 27.175 % |
#### 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.69 0.92 0.93 2/54 18522
Raw data (stat): 18522 (runsolver) R 18521 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487939497 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 0.74 0.92 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 1367 0 0 0 995 3 0 0 25 0 1 0 487939497 7282688 1344 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1778 1344 603 41 0 1737 0
vsize: 7112
[startup+20.0024 s]
Raw data (loadavg): 0.78 0.92 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 1530 0 0 0 1994 4 0 0 25 0 1 0 487939497 7962624 1507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1944 1507 603 41 0 1903 0
vsize: 7776
[startup+30.0031 s]
Raw data (loadavg): 0.81 0.93 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 1673 0 0 0 2994 5 0 0 25 0 1 0 487939497 8658944 1650 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2114 1650 603 41 0 2073 0
vsize: 8456
[startup+40.0037 s]
Raw data (loadavg): 0.84 0.93 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 1929 0 0 0 3993 5 0 0 25 0 1 0 487939497 9740288 1906 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2378 1906 603 41 0 2337 0
vsize: 9512
[startup+50.0048 s]
Raw data (loadavg): 0.86 0.93 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 1959 0 0 0 4994 5 0 0 25 0 1 0 487939497 9879552 1936 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2412 1936 603 41 0 2371 0
vsize: 9648
[startup+60.0056 s]
Raw data (loadavg): 0.88 0.93 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 1990 0 0 0 5993 6 0 0 25 0 1 0 487939497 9879552 1967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2412 1967 603 41 0 2371 0
vsize: 9648
[startup+70.0071 s]
Raw data (loadavg): 0.90 0.93 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2180 0 0 0 6994 6 0 0 25 0 1 0 487939497 10690560 2157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2610 2157 603 41 0 2569 0
vsize: 10440
[startup+80.0082 s]
Raw data (loadavg): 0.92 0.94 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2255 0 0 0 7994 6 0 0 25 0 1 0 487939497 11100160 2232 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2710 2232 603 41 0 2669 0
vsize: 10840
[startup+90.009 s]
Raw data (loadavg): 0.93 0.94 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2428 0 0 0 8994 7 0 0 25 0 1 0 487939497 11767808 2405 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2873 2405 603 41 0 2832 0
vsize: 11492
[startup+100.01 s]
Raw data (loadavg): 0.94 0.94 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2506 0 0 0 9994 7 0 0 25 0 1 0 487939497 12169216 2483 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2971 2483 603 41 0 2930 0
vsize: 11884
[startup+110.011 s]
Raw data (loadavg): 0.95 0.94 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2596 0 0 0 10993 8 0 0 25 0 1 0 487939497 12562432 2573 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3067 2573 603 41 0 3026 0
vsize: 12268
[startup+120.011 s]
Raw data (loadavg): 0.95 0.94 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2613 0 0 0 11993 8 0 0 25 0 1 0 487939497 12718080 2590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3105 2590 603 41 0 3064 0
vsize: 12420
[startup+130.012 s]
Raw data (loadavg): 0.96 0.94 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2638 0 0 0 12994 8 0 0 25 0 1 0 487939497 12865536 2615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3141 2615 603 41 0 3100 0
vsize: 12564
[startup+140.013 s]
Raw data (loadavg): 0.97 0.94 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2649 0 0 0 13994 8 0 0 25 0 1 0 487939497 12865536 2626 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3141 2626 603 41 0 3100 0
vsize: 12564
[startup+150.014 s]
Raw data (loadavg): 0.97 0.95 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2658 0 0 0 14994 8 0 0 25 0 1 0 487939497 13008896 2635 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3176 2635 603 41 0 3135 0
vsize: 12704
[startup+160.014 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2674 0 0 0 15994 8 0 0 25 0 1 0 487939497 13008896 2651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3176 2651 603 41 0 3135 0
vsize: 12704
[startup+170.014 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2680 0 0 0 16994 9 0 0 25 0 1 0 487939497 13008896 2657 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3176 2657 603 41 0 3135 0
vsize: 12704
[startup+180.013 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2680 0 0 0 17995 9 0 0 25 0 1 0 487939497 13008896 2657 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3176 2657 603 41 0 3135 0
vsize: 12704
[startup+190.013 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2837 0 0 0 18994 10 0 0 25 0 1 0 487939497 13680640 2814 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3340 2814 603 41 0 3299 0
vsize: 13360
[startup+200.012 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2858 0 0 0 19994 10 0 0 25 0 1 0 487939497 13819904 2835 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3374 2835 603 41 0 3333 0
vsize: 13496
[startup+210.012 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 2891 0 0 0 20994 10 0 0 25 0 1 0 487939497 13967360 2868 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3410 2868 603 41 0 3369 0
vsize: 13640
[startup+220.012 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3118 0 0 0 21994 11 0 0 25 0 1 0 487939497 14888960 3095 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3635 3095 603 41 0 3594 0
vsize: 14540
[startup+230.012 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3140 0 0 0 22994 11 0 0 25 0 1 0 487939497 14888960 3117 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3635 3117 603 41 0 3594 0
vsize: 14540
[startup+240.012 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3151 0 0 0 23994 11 0 0 25 0 1 0 487939497 15085568 3128 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3683 3128 603 41 0 3642 0
vsize: 14732
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3155 0 0 0 24994 11 0 0 25 0 1 0 487939497 15085568 3132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3683 3132 603 41 0 3642 0
vsize: 14732
[startup+260.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3155 0 0 0 25995 11 0 0 25 0 1 0 487939497 15085568 3132 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3683 3132 603 41 0 3642 0
vsize: 14732
[startup+270.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3172 0 0 0 26995 11 0 0 25 0 1 0 487939497 15085568 3149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3683 3149 603 41 0 3642 0
vsize: 14732
[startup+280.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3183 0 0 0 27995 11 0 0 25 0 1 0 487939497 15249408 3160 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3723 3160 603 41 0 3682 0
vsize: 14892
[startup+290.013 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3198 0 0 0 28996 11 0 0 25 0 1 0 487939497 15249408 3175 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3723 3175 603 41 0 3682 0
vsize: 14892
[startup+300.013 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3198 0 0 0 29996 11 0 0 25 0 1 0 487939497 15249408 3175 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3723 3175 603 41 0 3682 0
vsize: 14892
[startup+310.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3208 0 0 0 30996 11 0 0 25 0 1 0 487939497 15249408 3185 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3723 3185 603 41 0 3682 0
vsize: 14892
[startup+320.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3208 0 0 0 31996 11 0 0 25 0 1 0 487939497 15249408 3185 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3723 3185 603 41 0 3682 0
vsize: 14892
[startup+330.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3236 0 0 0 32996 11 0 0 25 0 1 0 487939497 15413248 3213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3763 3213 603 41 0 3722 0
vsize: 15052
[startup+340.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3242 0 0 0 33997 11 0 0 25 0 1 0 487939497 15413248 3219 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3763 3219 603 41 0 3722 0
vsize: 15052
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3279 0 0 0 34997 11 0 0 25 0 1 0 487939497 15609856 3256 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3256 603 41 0 3770 0
vsize: 15244
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3279 0 0 0 35998 11 0 0 25 0 1 0 487939497 15609856 3256 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3256 603 41 0 3770 0
vsize: 15244
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3279 0 0 0 36998 12 0 0 25 0 1 0 487939497 15609856 3256 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3256 603 41 0 3770 0
vsize: 15244
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3279 0 0 0 37999 12 0 0 25 0 1 0 487939497 15609856 3256 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3256 603 41 0 3770 0
vsize: 15244
[startup+390.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3279 0 0 0 38999 12 0 0 25 0 1 0 487939497 15609856 3256 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3256 603 41 0 3770 0
vsize: 15244
[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3289 0 0 0 39999 12 0 0 25 0 1 0 487939497 15806464 3266 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3266 603 41 0 3818 0
vsize: 15436
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3290 0 0 0 40999 12 0 0 25 0 1 0 487939497 15806464 3267 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3267 603 41 0 3818 0
vsize: 15436
[startup+420.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3290 0 0 0 42001 12 0 0 25 0 1 0 487939497 15806464 3267 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3267 603 41 0 3818 0
vsize: 15436
[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3290 0 0 0 43002 12 0 0 25 0 1 0 487939497 15806464 3267 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3267 603 41 0 3818 0
vsize: 15436
[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3290 0 0 0 44002 12 0 0 25 0 1 0 487939497 15806464 3267 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3267 603 41 0 3818 0
vsize: 15436
[startup+450.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3301 0 0 0 45002 12 0 0 25 0 1 0 487939497 15806464 3278 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3278 603 41 0 3818 0
vsize: 15436
[startup+460.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3306 0 0 0 46002 12 0 0 25 0 1 0 487939497 15806464 3283 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3283 603 41 0 3818 0
vsize: 15436
[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3309 0 0 0 47003 12 0 0 25 0 1 0 487939497 15806464 3286 4294967295 134512640 134672761 3221224544 3221223680 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3286 603 41 0 3818 0
vsize: 15436
[startup+480.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3319 0 0 0 48003 12 0 0 25 0 1 0 487939497 15806464 3296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3296 603 41 0 3818 0
vsize: 15436
[startup+490.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3334 0 0 0 49003 12 0 0 25 0 1 0 487939497 16003072 3311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3311 603 41 0 3866 0
vsize: 15628
[startup+500.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3334 0 0 0 50003 12 0 0 25 0 1 0 487939497 16003072 3311 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3311 603 41 0 3866 0
vsize: 15628
[startup+510.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3334 0 0 0 51003 12 0 0 25 0 1 0 487939497 16003072 3311 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3311 603 41 0 3866 0
vsize: 15628
[startup+520.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3334 0 0 0 52003 12 0 0 25 0 1 0 487939497 16003072 3311 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3311 603 41 0 3866 0
vsize: 15628
[startup+530.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3346 0 0 0 53003 12 0 0 25 0 1 0 487939497 16003072 3323 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3323 603 41 0 3866 0
vsize: 15628
[startup+540.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3346 0 0 0 54004 12 0 0 25 0 1 0 487939497 16003072 3323 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3323 603 41 0 3866 0
vsize: 15628
[startup+550.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3370 0 0 0 55004 12 0 0 25 0 1 0 487939497 16166912 3347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3947 3347 603 41 0 3906 0
vsize: 15788
[startup+560.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3371 0 0 0 56004 12 0 0 25 0 1 0 487939497 16166912 3348 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3947 3348 603 41 0 3906 0
vsize: 15788
[startup+570.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3404 0 0 0 57005 12 0 0 25 0 1 0 487939497 16330752 3381 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3987 3381 603 41 0 3946 0
vsize: 15948
[startup+580.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3428 0 0 0 58005 13 0 0 25 0 1 0 487939497 16330752 3405 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3987 3405 603 41 0 3946 0
vsize: 15948
[startup+590.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3449 0 0 0 59005 13 0 0 25 0 1 0 487939497 16474112 3426 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4022 3426 603 41 0 3981 0
vsize: 16088
[startup+600.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3483 0 0 0 60005 13 0 0 25 0 1 0 487939497 16670720 3460 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4070 3460 603 41 0 4029 0
vsize: 16280
[startup+610.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3753 0 0 0 61005 14 0 0 25 0 1 0 487939497 17743872 3730 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4332 3730 603 41 0 4291 0
vsize: 17328
[startup+620.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3762 0 0 0 62005 14 0 0 25 0 1 0 487939497 17743872 3739 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4332 3739 603 41 0 4291 0
vsize: 17328
[startup+630.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3776 0 0 0 63005 14 0 0 25 0 1 0 487939497 17891328 3753 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4368 3753 603 41 0 4327 0
vsize: 17472
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3800 0 0 0 64006 14 0 0 25 0 1 0 487939497 18038784 3777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4404 3777 603 41 0 4363 0
vsize: 17616
[startup+650.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 3964 0 0 0 65005 15 0 0 25 0 1 0 487939497 18710528 3941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4568 3941 603 41 0 4527 0
vsize: 18272
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4036 0 0 0 66005 15 0 0 25 0 1 0 487939497 18980864 4013 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4013 603 41 0 4593 0
vsize: 18536
[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4043 0 0 0 67005 15 0 0 25 0 1 0 487939497 18980864 4020 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4020 603 41 0 4593 0
vsize: 18536
[startup+680.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4059 0 0 0 68006 15 0 0 25 0 1 0 487939497 19161088 4036 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4678 4036 603 41 0 4637 0
vsize: 18712
[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4065 0 0 0 69006 15 0 0 25 0 1 0 487939497 19161088 4042 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4678 4042 603 41 0 4637 0
vsize: 18712
[startup+700.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4098 0 0 0 70006 15 0 0 25 0 1 0 487939497 19296256 4075 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4711 4075 603 41 0 4670 0
vsize: 18844
[startup+710.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4098 0 0 0 71007 15 0 0 25 0 1 0 487939497 19296256 4075 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4711 4075 603 41 0 4670 0
vsize: 18844
[startup+720.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4111 0 0 0 72007 15 0 0 25 0 1 0 487939497 19296256 4088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4711 4088 603 41 0 4670 0
vsize: 18844
[startup+730.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4123 0 0 0 73007 15 0 0 25 0 1 0 487939497 19431424 4100 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4744 4100 603 41 0 4703 0
vsize: 18976
[startup+740.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4124 0 0 0 74008 15 0 0 25 0 1 0 487939497 19431424 4101 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4744 4101 603 41 0 4703 0
vsize: 18976
[startup+750.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4246 0 0 0 75007 16 0 0 25 0 1 0 487939497 19881984 4223 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4854 4223 603 41 0 4813 0
vsize: 19416
[startup+760.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4246 0 0 0 76008 16 0 0 25 0 1 0 487939497 19881984 4223 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4854 4223 603 41 0 4813 0
vsize: 19416
[startup+770.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4251 0 0 0 77008 16 0 0 25 0 1 0 487939497 19881984 4228 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4854 4228 603 41 0 4813 0
vsize: 19416
[startup+780.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4255 0 0 0 78008 16 0 0 25 0 1 0 487939497 19881984 4232 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4854 4232 603 41 0 4813 0
vsize: 19416
[startup+790.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4295 0 0 0 79009 16 0 0 25 0 1 0 487939497 20164608 4272 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4923 4272 603 41 0 4882 0
vsize: 19692
[startup+800.037 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4296 0 0 0 80009 16 0 0 25 0 1 0 487939497 20164608 4273 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4923 4273 603 41 0 4882 0
vsize: 19692
[startup+810.037 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4296 0 0 0 81009 16 0 0 25 0 1 0 487939497 20164608 4273 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4923 4273 603 41 0 4882 0
vsize: 19692
[startup+820.038 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4296 0 0 0 82009 16 0 0 25 0 1 0 487939497 20164608 4273 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4923 4273 603 41 0 4882 0
vsize: 19692
[startup+830.037 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4297 0 0 0 83009 16 0 0 25 0 1 0 487939497 20164608 4274 4294967295 134512640 134672761 3221224544 3221223712 134560900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4923 4274 603 41 0 4882 0
vsize: 19692
[startup+840.038 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4311 0 0 0 84009 16 0 0 25 0 1 0 487939497 20164608 4288 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4923 4288 603 41 0 4882 0
vsize: 19692
[startup+850.038 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4323 0 0 0 85009 16 0 0 25 0 1 0 487939497 20164608 4300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4923 4300 603 41 0 4882 0
vsize: 19692
[startup+860.038 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4336 0 0 0 86010 16 0 0 25 0 1 0 487939497 20361216 4313 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4313 603 41 0 4930 0
vsize: 19884
[startup+870.038 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4346 0 0 0 87010 16 0 0 25 0 1 0 487939497 20361216 4323 4294967295 134512640 134672761 3221224544 3221223648 134559805 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4323 603 41 0 4930 0
vsize: 19884
[startup+880.037 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4361 0 0 0 88010 17 0 0 25 0 1 0 487939497 20361216 4338 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4338 603 41 0 4930 0
vsize: 19884
[startup+890.037 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4387 0 0 0 89010 17 0 0 25 0 1 0 487939497 20525056 4364 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4364 603 41 0 4970 0
vsize: 20044
[startup+900.038 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4397 0 0 0 90011 17 0 0 25 0 1 0 487939497 20688896 4374 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5051 4374 603 41 0 5010 0
vsize: 20204
[startup+910.038 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4397 0 0 0 91011 17 0 0 25 0 1 0 487939497 20688896 4374 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5051 4374 603 41 0 5010 0
vsize: 20204
[startup+920.038 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4398 0 0 0 92011 17 0 0 25 0 1 0 487939497 20688896 4375 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5051 4375 603 41 0 5010 0
vsize: 20204
[startup+930.038 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4426 0 0 0 93011 17 0 0 25 0 1 0 487939497 20885504 4403 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5099 4403 603 41 0 5058 0
vsize: 20396
[startup+940.037 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4452 0 0 0 94012 17 0 0 25 0 1 0 487939497 20885504 4429 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5099 4429 603 41 0 5058 0
vsize: 20396
[startup+950.037 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4452 0 0 0 95012 17 0 0 25 0 1 0 487939497 20885504 4429 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5099 4429 603 41 0 5058 0
vsize: 20396
[startup+960.037 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4454 0 0 0 96012 17 0 0 25 0 1 0 487939497 20885504 4431 4294967295 134512640 134672761 3221224544 3221223728 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5099 4431 603 41 0 5058 0
vsize: 20396
[startup+970.038 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4455 0 0 0 97013 17 0 0 25 0 1 0 487939497 20885504 4432 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5099 4432 603 41 0 5058 0
vsize: 20396
[startup+980.038 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4460 0 0 0 98013 17 0 0 25 0 1 0 487939497 20885504 4437 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5099 4437 603 41 0 5058 0
vsize: 20396
[startup+990.038 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4469 0 0 0 99013 17 0 0 25 0 1 0 487939497 21049344 4446 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5139 4446 603 41 0 5098 0
vsize: 20556
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4469 0 0 0 100013 17 0 0 25 0 1 0 487939497 21049344 4446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5139 4446 603 41 0 5098 0
vsize: 20556
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4469 0 0 0 101014 17 0 0 25 0 1 0 487939497 21049344 4446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5139 4446 603 41 0 5098 0
vsize: 20556
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4469 0 0 0 102014 17 0 0 25 0 1 0 487939497 21049344 4446 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5139 4446 603 41 0 5098 0
vsize: 20556
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4473 0 0 0 103015 17 0 0 25 0 1 0 487939497 21049344 4450 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5139 4450 603 41 0 5098 0
vsize: 20556
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4511 0 0 0 104015 17 0 0 25 0 1 0 487939497 21241856 4488 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5186 4488 603 41 0 5145 0
vsize: 20744
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4535 0 0 0 105015 17 0 0 25 0 1 0 487939497 21438464 4512 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4512 603 41 0 5193 0
vsize: 20936
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4535 0 0 0 106016 17 0 0 25 0 1 0 487939497 21438464 4512 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4512 603 41 0 5193 0
vsize: 20936
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4535 0 0 0 107016 17 0 0 25 0 1 0 487939497 21438464 4512 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4512 603 41 0 5193 0
vsize: 20936
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4535 0 0 0 108016 17 0 0 25 0 1 0 487939497 21438464 4512 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4512 603 41 0 5193 0
vsize: 20936
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4535 0 0 0 109017 17 0 0 25 0 1 0 487939497 21438464 4512 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4512 603 41 0 5193 0
vsize: 20936
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4536 0 0 0 110017 17 0 0 25 0 1 0 487939497 21438464 4513 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4513 603 41 0 5193 0
vsize: 20936
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4540 0 0 0 111017 17 0 0 25 0 1 0 487939497 21438464 4517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4517 603 41 0 5193 0
vsize: 20936
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4540 0 0 0 112018 17 0 0 25 0 1 0 487939497 21438464 4517 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4517 603 41 0 5193 0
vsize: 20936
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4540 0 0 0 113018 17 0 0 25 0 1 0 487939497 21438464 4517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4517 603 41 0 5193 0
vsize: 20936
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4540 0 0 0 114018 17 0 0 25 0 1 0 487939497 21438464 4517 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4517 603 41 0 5193 0
vsize: 20936
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4552 0 0 0 115019 17 0 0 25 0 1 0 487939497 21438464 4529 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4529 603 41 0 5193 0
vsize: 20936
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4555 0 0 0 116019 17 0 0 25 0 1 0 487939497 21438464 4532 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4532 603 41 0 5193 0
vsize: 20936
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4555 0 0 0 117019 17 0 0 25 0 1 0 487939497 21438464 4532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4532 603 41 0 5193 0
vsize: 20936
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4555 0 0 0 118020 17 0 0 25 0 1 0 487939497 21438464 4532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4532 603 41 0 5193 0
vsize: 20936
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4555 0 0 0 119021 17 0 0 25 0 1 0 487939497 21438464 4532 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4532 603 41 0 5193 0
vsize: 20936
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 18522
Raw data (stat): 18522 (minisat+) R 18521 29653 29652 0 -1 0 4555 0 0 0 120021 17 0 0 25 0 1 0 487939497 21438464 4532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4532 603 41 0 5193 0
vsize: 20936
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.94 1/54 18522
Raw data (stat): 18522 (minisat+) Z 18521 29653 29652 0 -1 12 4557 0 0 0 120021 18 0 0 25 0 1 0 487939497 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.4
CPU user time (s): 1200.21
CPU system time (s): 0.187971
CPU usage (%): 100.029
Max. virtual memory (Kb): 20936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####