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/een/normalized-p0548.opb
MD5SUM422c0da7d5380a26c4dac413428db5c9
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 14670
Optimality of the best value was proved NO
Number of terms in the objective function 416
Biggest coefficient in the objective function 11000
Number of bits for the biggest coefficient in the objective function 14
Sum of the numbers in the objective function 96797
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 11000
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 96797
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1230.14
Number of variables527
Total number of constraints156
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints116
Minimum length of a constraint2
Maximum length of a constraint134

Trace number 7149 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-14 21:37:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5231 boxname=wulflinc10 idbench=403 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  422c0da7d5380a26c4dac413428db5c9  /oldhome/oroussel/tmp/wulflinc10/normalized-p0548.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc10/normalized-p0548.opb
IDLAUNCH: 5231
/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:        827428 kB
Buffers:         36000 kB
Cached:         150972 kB
SwapCached:        164 kB
Active:          74580 kB
Inactive:       115432 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        827176 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11556 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:57:42 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 5231 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 156 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................ss.ssssss.s.s.
c ---[ 125]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    3
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    3
c ---[ 118]---> BDD-cost:    3
c ---[ 117]---> BDD-cost:    3
c ---[ 116]---> BDD-cost:    3
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:    3
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    3
c ---[ 110]---> BDD-cost:    3
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    3
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:    3
c ---[ 105]---> BDD-cost:    3
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    5
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    8
c ---[  99]---> BDD-cost:    6
c ---[  98]---> BDD-cost:    7
c ---[  96]---> BDD-cost:   19
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:    4
c ---[  89]---> BDD-cost:   24
c ---[  88]---> BDD-cost:   14
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   28
c ---[  85]---> BDD-cost:   13
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:    9
c ---[  80]---> BDD-cost:   25
c ---[  76]---> BDD-cost:   32
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   19
c ---[  72]---> BDD-cost:   24
c ---[  70]---> BDD-cost:   23
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:   27
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   56
c ---[  64]---> BDD-cost:   50
c ---[  63]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   33
c ---[  60]---> BDD-cost:   12
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:   34
c ---[  56]---> BDD-cost:   33
c ---[  55]---> BDD-cost:   23
c ---[  54]---> BDD-cost:   75
c ---[  53]---> BDD-cost:   24
c ---[  52]---> BDD-cost:   37
c ---[  51]---> BDD-cost:   37
c ---[  50]---> BDD-cost:   95
c ---[  49]---> BDD-cost:   11
c ---[  48]---> BDD-cost:  107
c ---[  47]---> BDD-cost:  115
c ---[  46]---> BDD-cost:  120
c ---[  45]---> BDD-cost:  104
c ---[  44]---> BDD-cost:   29
c ---[  43]---> BDD-cost:   51
c ---[  42]---> BDD-cost:   35
c ---[  41]---> BDD-cost:   24
c ---[  39]---> BDD-cost:   61
c ---[  38]---> BDD-cost:  109
c ---[  37]---> BDD-cost:  153
c ---[  36]---> BDD-cost:  120
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   25
c ---[  33]---> BDD-cost:  121
c ---[  32]---> BDD-cost:   32
c ---[  31]---> BDD-cost:   70
c ---[  30]---> BDD-cost:   56
c ---[  29]---> BDD-cost:   78
c ---[  28]---> BDD-cost:   84
c ---[  27]---> BDD-cost:   36
c ---[  26]---> BDD-cost:   91
c ---[  25]---> BDD-cost:   42
c ---[  23]---> BDD-cost:   39
c ---[  22]---> BDD-cost:  128
c ---[  21]---> BDD-cost:   61
c ---[  19]---> BDD-cost:   85
c ---[  18]---> BDD-cost:   55
c ---[  17]---> BDD-cost:   79
c ---[  16]---> Sorter-cost: 1212     Base: 2 3 2 3
c ---[  15]---> BDD-cost:   26
c ---[  14]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  13]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  12]---> BDD-cost:   49
c ---[  11]---> BDD-cost:   49
c ---[  10]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[   9]---> BDD-cost:    2
c ---[   8]---> BDD-cost:    2
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    2
c ---[   5]---> BDD-cost:    4
c ---[   4]---> BDD-cost:    7
c ---[   3]---> BDD-cost:    5
c ---[   2]---> BDD-cost:   11
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   19074    57624 |    6358       0        0     nan |  0.000 % |
c |       100 |   19074    57624 |    6993     100      383     3.8 |  2.252 % |
c |       250 |   19050    57540 |    7693     243     1471     6.1 |  2.288 % |
c |       475 |   19050    57540 |    8462     468     4052     8.7 |  2.288 % |
c |       812 |   19011    57410 |    9308     799     7772     9.7 |  2.361 % |
c |      1321 |   19011    57410 |   10239    1308    21339    16.3 |  2.361 % |
c |      2080 |   19011    57410 |   11263    2067    39807    19.3 |  2.361 % |
c |      3219 |   19002    57379 |   12389    3203    61387    19.2 |  2.379 % |
c |      4929 |   18969    57279 |   13628    4905   111590    22.8 |  2.434 % |
c |      7491 |   18952    57224 |   14991    7466   185570    24.9 |  2.470 % |
c |     11335 |   18952    57224 |   16491   11310   302929    26.8 |  2.470 % |
c |     17101 |   18905    57066 |   18140    8619   230651    26.8 |  2.579 % |
c |     25754 |   18905    57066 |   19954   17272   547223    31.7 |  2.579 % |
c |     38729 |   18877    56968 |   21949   20002   728606    36.4 |  2.633 % |
c |     58190 |   18855    56892 |   24144   17072   501826    29.4 |  2.688 % |
c |     87383 |   18855    56892 |   26558   21476  1433413    66.7 |  2.688 % |
c ==============================================================================
c Found solution: 52559
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2954   maxlim: 44238   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115060 |   39469   130542 |   13156   21856  1211248    55.4 |  2.688 % |
c |    115160 |   39469   130542 |   14471   11028   574450    52.1 |  1.865 % |
c |    115310 |   39469   130542 |   15918   11178   576227    51.6 |  1.865 % |
c |    115535 |   39469   130542 |   17510   11403   580967    50.9 |  1.865 % |
c |    115872 |   39469   130542 |   19261   11740   589305    50.2 |  1.865 % |
c |    116378 |   39469   130542 |   21187   12246   599863    49.0 |  1.865 % |
c |    117137 |   39469   130542 |   23306   13005   616416    47.4 |  1.865 % |
c |    118277 |   39469   130542 |   25637   14145   652577    46.1 |  1.865 % |
c |    119985 |   39469   130542 |   28201   15853   698827    44.1 |  1.865 % |
c |    122547 |   39469   130542 |   31021   18415   771171    41.9 |  1.865 % |
c |    126392 |   39469   130542 |   34123   22260   874497    39.3 |  1.865 % |
c |    132160 |   39469   130542 |   37535   28028  1200711    42.8 |  1.865 % |
c |    140809 |   39469   130542 |   41289   36677  1563685    42.6 |  1.865 % |
c |    153784 |   39469   130542 |   45418   21376   978593    45.8 |  1.865 % |
c |    173246 |   39469   130542 |   49959   40838  1783298    43.7 |  1.865 % |
c |    202439 |   39469   130542 |   54955   34214  1463768    42.8 |  1.865 % |
c |    246229 |   39469   130542 |   60451   37728  1678400    44.5 |  1.865 % |
c |    311913 |   39469   130542 |   66496   56527  2405637    42.6 |  1.865 % |
c |    410440 |   39469   130542 |   73146   55718  2558579    45.9 |  1.865 % |
c |    558229 |   39469   130542 |   80460   33120  1706066    51.5 |  1.865 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/54 6191
Raw data (stat): 6191 (runsolver) R 6190 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429674464 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0004 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 1547 0 0 0 995 3 0 0 25 0 1 0 429674464 8048640 1517 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1965 1517 603 41 0 1924 0
vsize: 7860
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 1832 0 0 0 1994 4 0 0 25 0 1 0 429674464 9121792 1802 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2227 1802 603 41 0 2186 0
vsize: 8908
[startup+30.0001 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 2007 0 0 0 2993 4 0 0 25 0 1 0 429674464 9932800 1977 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2425 1977 603 41 0 2384 0
vsize: 9700
[startup+39.9997 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 2133 0 0 0 3992 5 0 0 25 0 1 0 429674464 10330112 2103 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2522 2103 603 41 0 2481 0
vsize: 10088
[startup+49.9996 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 2583 0 0 0 4991 7 0 0 25 0 1 0 429674464 12214272 2553 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2553 603 41 0 2941 0
vsize: 11928
[startup+59.9999 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 2677 0 0 0 5991 7 0 0 25 0 1 0 429674464 12619776 2647 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3081 2647 603 41 0 3040 0
vsize: 12324
[startup+70 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 3001 0 0 0 6989 9 0 0 25 0 1 0 429674464 13967360 2971 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3410 2971 603 41 0 3369 0
vsize: 13640
[startup+80.0003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 3001 0 0 0 7988 9 0 0 25 0 1 0 429674464 13967360 2971 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3410 2971 603 41 0 3369 0
vsize: 13640
[startup+90.0005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 4338 0 0 0 8985 12 0 0 25 0 1 0 429674464 18755584 4008 4294967295 134512640 134672761 3221224640 3221223824 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4579 4008 603 41 0 4538 0
vsize: 18316
[startup+100 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 4496 0 0 0 9985 13 0 0 25 0 1 0 429674464 19427328 4166 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4743 4166 603 41 0 4702 0
vsize: 18972
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5003 0 0 0 10984 14 0 0 25 0 1 0 429674464 21557248 4673 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5263 4673 603 41 0 5222 0
vsize: 21052
[startup+120.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5094 0 0 0 11984 14 0 0 25 0 1 0 429674464 21958656 4764 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4764 603 41 0 5320 0
vsize: 21444
[startup+130.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5094 0 0 0 12984 14 0 0 25 0 1 0 429674464 21958656 4764 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4764 603 41 0 5320 0
vsize: 21444
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5160 0 0 0 13984 14 0 0 25 0 1 0 429674464 22228992 4830 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5427 4830 603 41 0 5386 0
vsize: 21708
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5494 0 0 0 14984 15 0 0 25 0 1 0 429674464 23580672 5164 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5757 5164 603 41 0 5716 0
vsize: 23028
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5624 0 0 0 15984 15 0 0 25 0 1 0 429674464 24125440 5294 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5890 5294 603 41 0 5849 0
vsize: 23560
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5624 0 0 0 16984 15 0 0 25 0 1 0 429674464 24125440 5294 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5890 5294 603 41 0 5849 0
vsize: 23560
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5652 0 0 0 17984 15 0 0 25 0 1 0 429674464 24289280 5322 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5930 5322 603 41 0 5889 0
vsize: 23720
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5652 0 0 0 18984 15 0 0 25 0 1 0 429674464 24289280 5322 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5930 5322 603 41 0 5889 0
vsize: 23720
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5652 0 0 0 19984 15 0 0 25 0 1 0 429674464 24289280 5322 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5930 5322 603 41 0 5889 0
vsize: 23720
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5715 0 0 0 20984 15 0 0 25 0 1 0 429674464 24559616 5385 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5996 5385 603 41 0 5955 0
vsize: 23984
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5800 0 0 0 21984 15 0 0 25 0 1 0 429674464 24961024 5470 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6094 5470 603 41 0 6053 0
vsize: 24376
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5811 0 0 0 22984 16 0 0 25 0 1 0 429674464 24961024 5481 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6094 5481 603 41 0 6053 0
vsize: 24376
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5811 0 0 0 23985 16 0 0 25 0 1 0 429674464 24961024 5481 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6094 5481 603 41 0 6053 0
vsize: 24376
[startup+250.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5826 0 0 0 24985 16 0 0 25 0 1 0 429674464 25120768 5496 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6133 5496 603 41 0 6092 0
vsize: 24532
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5917 0 0 0 25985 16 0 0 25 0 1 0 429674464 25391104 5587 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6199 5587 603 41 0 6158 0
vsize: 24796
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6192 0 0 0 26984 17 0 0 25 0 1 0 429674464 26599424 5862 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6494 5862 603 41 0 6453 0
vsize: 25976
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6363 0 0 0 27984 17 0 0 25 0 1 0 429674464 27287552 6033 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 6033 603 41 0 6621 0
vsize: 26648
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6376 0 0 0 28984 17 0 0 25 0 1 0 429674464 27287552 6046 4294967295 134512640 134672761 3221224640 3221223808 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 6046 603 41 0 6621 0
vsize: 26648
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6376 0 0 0 29984 17 0 0 25 0 1 0 429674464 27287552 6046 4294967295 134512640 134672761 3221224640 3221223808 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 6046 603 41 0 6621 0
vsize: 26648
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6377 0 0 0 30984 17 0 0 25 0 1 0 429674464 27287552 6047 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6662 6047 603 41 0 6621 0
vsize: 26648
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6411 0 0 0 31984 17 0 0 25 0 1 0 429674464 27430912 6081 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6697 6081 603 41 0 6656 0
vsize: 26788
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6412 0 0 0 32984 17 0 0 25 0 1 0 429674464 27430912 6082 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6697 6082 603 41 0 6656 0
vsize: 26788
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6429 0 0 0 33985 17 0 0 25 0 1 0 429674464 27578368 6099 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6733 6099 603 41 0 6692 0
vsize: 26932
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6454 0 0 0 34984 18 0 0 25 0 1 0 429674464 27725824 6124 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6769 6124 603 41 0 6728 0
vsize: 27076
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6676 0 0 0 35982 19 0 0 25 0 1 0 429674464 28835840 6346 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7040 6346 603 41 0 6999 0
vsize: 28160
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6694 0 0 0 36982 19 0 0 25 0 1 0 429674464 28971008 6364 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7073 6364 603 41 0 7032 0
vsize: 28292
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6694 0 0 0 37982 19 0 0 25 0 1 0 429674464 28971008 6364 4294967295 134512640 134672761 3221224640 3221223808 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7073 6364 603 41 0 7032 0
vsize: 28292
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6705 0 0 0 38983 19 0 0 25 0 1 0 429674464 28971008 6375 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7073 6375 603 41 0 7032 0
vsize: 28292
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6717 0 0 0 39983 19 0 0 25 0 1 0 429674464 29122560 6387 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7110 6387 603 41 0 7069 0
vsize: 28440
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6719 0 0 0 40983 19 0 0 25 0 1 0 429674464 29122560 6389 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7110 6389 603 41 0 7069 0
vsize: 28440
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6738 0 0 0 41983 19 0 0 25 0 1 0 429674464 29122560 6408 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7110 6408 603 41 0 7069 0
vsize: 28440
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6760 0 0 0 42983 19 0 0 25 0 1 0 429674464 29286400 6430 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7150 6430 603 41 0 7109 0
vsize: 28600
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6859 0 0 0 43983 19 0 0 25 0 1 0 429674464 29691904 6529 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7249 6529 603 41 0 7208 0
vsize: 28996
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6859 0 0 0 44983 19 0 0 25 0 1 0 429674464 29691904 6529 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7249 6529 603 41 0 7208 0
vsize: 28996
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6862 0 0 0 45984 19 0 0 25 0 1 0 429674464 29691904 6532 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7249 6532 603 41 0 7208 0
vsize: 28996
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6870 0 0 0 46984 19 0 0 25 0 1 0 429674464 29691904 6540 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7249 6540 603 41 0 7208 0
vsize: 28996
[startup+480.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6871 0 0 0 47984 19 0 0 25 0 1 0 429674464 29691904 6541 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7249 6541 603 41 0 7208 0
vsize: 28996
[startup+490.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6871 0 0 0 48984 19 0 0 25 0 1 0 429674464 29691904 6541 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7249 6541 603 41 0 7208 0
vsize: 28996
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6893 0 0 0 49984 19 0 0 25 0 1 0 429674464 29839360 6563 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7285 6563 603 41 0 7244 0
vsize: 29140
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7009 0 0 0 50983 20 0 0 25 0 1 0 429674464 30388224 6679 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7419 6679 603 41 0 7378 0
vsize: 29676
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7270 0 0 0 51982 21 0 0 25 0 1 0 429674464 31461376 6940 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 6940 603 41 0 7640 0
vsize: 30724
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7364 0 0 0 52982 22 0 0 25 0 1 0 429674464 31862784 7034 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7779 7034 603 41 0 7738 0
vsize: 31116
[startup+540.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7384 0 0 0 53982 22 0 0 25 0 1 0 429674464 31862784 7054 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7779 7054 603 41 0 7738 0
vsize: 31116
[startup+550.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7408 0 0 0 54982 22 0 0 25 0 1 0 429674464 32026624 7078 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7078 603 41 0 7778 0
vsize: 31276
[startup+560.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7416 0 0 0 55982 22 0 0 25 0 1 0 429674464 32026624 7086 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7819 7086 603 41 0 7778 0
vsize: 31276
[startup+570.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7434 0 0 0 56982 22 0 0 25 0 1 0 429674464 32190464 7104 4294967295 134512640 134672761 3221224640 3221223808 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7859 7104 603 41 0 7818 0
vsize: 31436
[startup+580.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7434 0 0 0 57982 22 0 0 25 0 1 0 429674464 32190464 7104 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7859 7104 603 41 0 7818 0
vsize: 31436
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7447 0 0 0 58983 22 0 0 25 0 1 0 429674464 32190464 7117 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7859 7117 603 41 0 7818 0
vsize: 31436
[startup+600.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 59983 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7859 7118 603 41 0 7818 0
vsize: 31436
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 60983 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7859 7118 603 41 0 7818 0
vsize: 31436
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 61983 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7859 7118 603 41 0 7818 0
vsize: 31436
[startup+630.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 62984 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7859 7118 603 41 0 7818 0
vsize: 31436
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 63984 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7859 7118 603 41 0 7818 0
vsize: 31436
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 64984 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7859 7118 603 41 0 7818 0
vsize: 31436
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7454 0 0 0 65984 22 0 0 25 0 1 0 429674464 32190464 7124 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7859 7124 603 41 0 7818 0
vsize: 31436
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7464 0 0 0 66984 22 0 0 25 0 1 0 429674464 32354304 7134 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7899 7134 603 41 0 7858 0
vsize: 31596
[startup+680.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7479 0 0 0 67984 22 0 0 25 0 1 0 429674464 32354304 7149 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7899 7149 603 41 0 7858 0
vsize: 31596
[startup+690.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7748 0 0 0 68984 22 0 0 25 0 1 0 429674464 33415168 7418 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8158 7418 603 41 0 8117 0
vsize: 32632
[startup+700.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8085 0 0 0 69983 23 0 0 25 0 1 0 429674464 34881536 7755 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8516 7755 603 41 0 8475 0
vsize: 34064
[startup+710.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8311 0 0 0 70983 24 0 0 25 0 1 0 429674464 35844096 7981 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8751 7981 603 41 0 8710 0
vsize: 35004
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8505 0 0 0 71982 25 0 0 25 0 1 0 429674464 36638720 8175 4294967295 134512640 134672761 3221224640 3221223744 134559760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8945 8175 603 41 0 8904 0
vsize: 35780
[startup+730.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8505 0 0 0 72982 25 0 0 25 0 1 0 429674464 36638720 8175 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8945 8175 603 41 0 8904 0
vsize: 35780
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8505 0 0 0 73982 25 0 0 25 0 1 0 429674464 36638720 8175 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8945 8175 603 41 0 8904 0
vsize: 35780
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8523 0 0 0 74981 26 0 0 25 0 1 0 429674464 36638720 8193 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8945 8193 603 41 0 8904 0
vsize: 35780
[startup+760.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8530 0 0 0 75982 26 0 0 25 0 1 0 429674464 36782080 8200 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8980 8200 603 41 0 8939 0
vsize: 35920
[startup+770.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8541 0 0 0 76982 26 0 0 25 0 1 0 429674464 36782080 8211 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8980 8211 603 41 0 8939 0
vsize: 35920
[startup+780.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8558 0 0 0 77982 26 0 0 25 0 1 0 429674464 36782080 8228 4294967295 134512640 134672761 3221224640 3221223824 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8980 8228 603 41 0 8939 0
vsize: 35920
[startup+790.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8559 0 0 0 78982 26 0 0 25 0 1 0 429674464 36782080 8229 4294967295 134512640 134672761 3221224640 3221223700 1075349617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8980 8229 603 41 0 8939 0
vsize: 35920
[startup+800.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8580 0 0 0 79982 26 0 0 25 0 1 0 429674464 36925440 8250 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9015 8250 603 41 0 8974 0
vsize: 36060
[startup+810.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8602 0 0 0 80982 26 0 0 25 0 1 0 429674464 37089280 8272 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9055 8272 603 41 0 9014 0
vsize: 36220
[startup+820.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8603 0 0 0 81982 26 0 0 25 0 1 0 429674464 37089280 8273 4294967295 134512640 134672761 3221224640 3221223744 134560070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9055 8273 603 41 0 9014 0
vsize: 36220
[startup+830.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8614 0 0 0 82982 26 0 0 25 0 1 0 429674464 37089280 8284 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9055 8284 603 41 0 9014 0
vsize: 36220
[startup+840.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8615 0 0 0 83983 26 0 0 25 0 1 0 429674464 37089280 8285 4294967295 134512640 134672761 3221224640 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9055 8285 603 41 0 9014 0
vsize: 36220
[startup+850.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8637 0 0 0 84983 26 0 0 25 0 1 0 429674464 37285888 8307 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8307 603 41 0 9062 0
vsize: 36412
[startup+860.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8653 0 0 0 85983 26 0 0 25 0 1 0 429674464 37285888 8323 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8323 603 41 0 9062 0
vsize: 36412
[startup+870.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8657 0 0 0 86983 26 0 0 25 0 1 0 429674464 37285888 8327 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8327 603 41 0 9062 0
vsize: 36412
[startup+880.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8659 0 0 0 87984 26 0 0 25 0 1 0 429674464 37285888 8329 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8329 603 41 0 9062 0
vsize: 36412
[startup+890.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8661 0 0 0 88984 26 0 0 25 0 1 0 429674464 37285888 8331 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8331 603 41 0 9062 0
vsize: 36412
[startup+900.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8663 0 0 0 89984 26 0 0 25 0 1 0 429674464 37285888 8333 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8333 603 41 0 9062 0
vsize: 36412
[startup+910.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8690 0 0 0 90984 26 0 0 25 0 1 0 429674464 37482496 8360 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9151 8360 603 41 0 9110 0
vsize: 36604
[startup+920.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8709 0 0 0 91984 26 0 0 25 0 1 0 429674464 37679104 8379 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8379 603 41 0 9158 0
vsize: 36796
[startup+930.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8712 0 0 0 92984 26 0 0 25 0 1 0 429674464 37679104 8382 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8382 603 41 0 9158 0
vsize: 36796
[startup+940.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8713 0 0 0 93985 26 0 0 25 0 1 0 429674464 37679104 8383 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8383 603 41 0 9158 0
vsize: 36796
[startup+950.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8718 0 0 0 94985 26 0 0 25 0 1 0 429674464 37679104 8388 4294967295 134512640 134672761 3221224640 3221223808 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8388 603 41 0 9158 0
vsize: 36796
[startup+960.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8727 0 0 0 95985 26 0 0 25 0 1 0 429674464 37679104 8397 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8397 603 41 0 9158 0
vsize: 36796
[startup+970.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 96985 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8399 603 41 0 9158 0
vsize: 36796
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 97985 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223744 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8399 603 41 0 9158 0
vsize: 36796
[startup+990.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 98986 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8399 603 41 0 9158 0
vsize: 36796
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 99986 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8399 603 41 0 9158 0
vsize: 36796
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 100986 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8399 603 41 0 9158 0
vsize: 36796
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 101986 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8399 603 41 0 9158 0
vsize: 36796
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8733 0 0 0 102986 26 0 0 25 0 1 0 429674464 37679104 8403 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8403 603 41 0 9158 0
vsize: 36796
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8743 0 0 0 103986 26 0 0 25 0 1 0 429674464 37679104 8413 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8413 603 41 0 9158 0
vsize: 36796
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8743 0 0 0 104987 26 0 0 25 0 1 0 429674464 37679104 8413 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8413 603 41 0 9158 0
vsize: 36796
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8743 0 0 0 105987 26 0 0 25 0 1 0 429674464 37679104 8413 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8413 603 41 0 9158 0
vsize: 36796
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8743 0 0 0 106987 26 0 0 25 0 1 0 429674464 37679104 8413 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8413 603 41 0 9158 0
vsize: 36796
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8767 0 0 0 107987 27 0 0 25 0 1 0 429674464 37875712 8437 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8437 603 41 0 9206 0
vsize: 36988
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8770 0 0 0 108987 27 0 0 25 0 1 0 429674464 37875712 8440 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8440 603 41 0 9206 0
vsize: 36988
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8771 0 0 0 109987 27 0 0 25 0 1 0 429674464 37875712 8441 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8441 603 41 0 9206 0
vsize: 36988
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8771 0 0 0 110988 27 0 0 25 0 1 0 429674464 37875712 8441 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8441 603 41 0 9206 0
vsize: 36988
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8771 0 0 0 111988 27 0 0 25 0 1 0 429674464 37875712 8441 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8441 603 41 0 9206 0
vsize: 36988
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8773 0 0 0 112988 27 0 0 25 0 1 0 429674464 37875712 8443 4294967295 134512640 134672761 3221224640 3221223824 134558771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8443 603 41 0 9206 0
vsize: 36988
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8785 0 0 0 113988 27 0 0 25 0 1 0 429674464 37875712 8455 4294967295 134512640 134672761 3221224640 3221223808 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8455 603 41 0 9206 0
vsize: 36988
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8785 0 0 0 114989 27 0 0 25 0 1 0 429674464 37875712 8455 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8455 603 41 0 9206 0
vsize: 36988
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8785 0 0 0 115989 27 0 0 25 0 1 0 429674464 37875712 8455 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8455 603 41 0 9206 0
vsize: 36988
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8785 0 0 0 116989 27 0 0 25 0 1 0 429674464 37875712 8455 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8455 603 41 0 9206 0
vsize: 36988
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8785 0 0 0 117989 27 0 0 25 0 1 0 429674464 37875712 8455 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8455 603 41 0 9206 0
vsize: 36988
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8786 0 0 0 118990 27 0 0 25 0 1 0 429674464 37875712 8456 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8456 603 41 0 9206 0
vsize: 36988
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6191
Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8788 0 0 0 119990 27 0 0 25 0 1 0 429674464 37875712 8458 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9247 8458 603 41 0 9206 0
vsize: 36988
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 6191
Raw data (stat): 6191 (minisat+) Z 6190 25347 25346 0 -1 12 8791 0 0 0 119990 28 0 0 25 0 1 0 429674464 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: 10
Real time (s): 1200.03
CPU time (s): 1200.19
CPU user time (s): 1199.9
CPU system time (s): 0.287956
CPU usage (%): 100.013
Max. virtual memory (Kb): 36988
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####