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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-opt1217.opb
MD5SUMdf52a42b636b50954671d81e4d85c221
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -16384
Optimality of the best value was proved NO
Number of terms in the objective function 19
Biggest coefficient in the objective function 262144
Number of bits for the biggest coefficient in the objective function 19
Sum of the numbers in the objective function 524287
Number of bits of the sum of numbers in the objective function 19
Biggest number in a constraint 393216
Number of bits of the biggest number in a constraint 19
Biggest sum of numbers in a constraint 917503
Number of bits of the biggest sum of numbers20
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.03
Number of variables787
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 constraint67

Trace number 16618 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        676764 kB
Buffers:          2668 kB
Cached:         328932 kB
SwapCached:        512 kB
Active:          23952 kB
Inactive:       309668 kB
HighTotal:      131008 kB
HighFree:        14616 kB
LowTotal:       903652 kB
LowFree:        662148 kB
SwapTotal:     2097892 kB
SwapFree:      2096484 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            18652 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 08:22:07 (client local time) WITH STATUS 0 IN 1200.31 SECONDS
stats: 12882 7 1200.31 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]---> BDD-cost: 1472
c ---[ 110]---> BDD-cost: 1400
c ---[ 109]---> BDD-cost: 1650
c ---[ 108]---> BDD-cost: 1517
c ---[ 107]---> BDD-cost: 1701
c ---[ 106]---> BDD-cost: 1477
c ---[ 105]---> BDD-cost: 1174
c ---[ 104]---> BDD-cost:  883
c ---[ 102]---> BDD-cost:   29
c ---[ 100]---> BDD-cost:   29
c ---[  98]---> BDD-cost:   29
c ---[  97]---> BDD-cost: 1670
c ---[  95]---> BDD-cost:   29
c ---[  93]---> BDD-cost:   29
c ---[  91]---> BDD-cost:   29
c ---[  89]---> BDD-cost:   29
c ---[  87]---> BDD-cost:   29
c ---[  85]---> BDD-cost:   29
c ---[  83]---> BDD-cost:   29
c ---[  81]---> BDD-cost:   29
c ---[  79]---> BDD-cost:   29
c ---[  77]---> BDD-cost:   29
c ---[  76]---> BDD-cost: 1605
c ---[  74]---> BDD-cost:   29
c ---[  72]---> BDD-cost:   29
c ---[  70]---> BDD-cost:   29
c ---[  68]---> BDD-cost:   29
c ---[  66]---> BDD-cost:   29
c ---[  64]---> BDD-cost:   29
c ---[  62]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   29
c ---[  58]---> BDD-cost:   29
c ---[  56]---> BDD-cost:   29
c ---[  55]---> BDD-cost: 1826
c ---[  53]---> BDD-cost:   29
c ---[  51]---> BDD-cost:   29
c ---[  49]---> BDD-cost:   29
c ---[  47]---> BDD-cost:   29
c ---[  45]---> BDD-cost:   29
c ---[  43]---> BDD-cost:   29
c ---[  41]---> BDD-cost:   29
c ---[  39]---> BDD-cost:   29
c ---[  37]---> BDD-cost:   29
c ---[  35]---> BDD-cost:   29
c ---[  34]---> BDD-cost: 1452
c ---[  32]---> BDD-cost:   29
c ---[  30]---> BDD-cost:   29
c ---[  28]---> BDD-cost:   29
c ---[  26]---> BDD-cost:   29
c ---[  24]---> BDD-cost:   29
c ---[  22]---> BDD-cost:   29
c ---[  20]---> BDD-cost:   29
c ---[  18]---> BDD-cost:   29
c ---[  16]---> BDD-cost:   29
c ---[  14]---> BDD-cost:   29
c ---[  13]---> BDD-cost: 1049
c ---[  11]---> BDD-cost:   29
c ---[   9]---> BDD-cost:   29
c ---[   7]---> BDD-cost:   29
c ---[   5]---> BDD-cost:   29
c ---[   3]---> BDD-cost:   29
c ---[   2]---> BDD-cost: 1962
c ---[   1]---> BDD-cost: 1619
c ---[   0]---> BDD-cost: 1856
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   72565   214434 |   24188       0        0     nan |  0.000 % |
c |       100 |   72565   214434 |   26606     100     5083    50.8 |  0.249 % |
c |       250 |   72565   214434 |   29267     250    10143    40.6 |  0.249 % |
c |       475 |   72565   214434 |   32194     475    33055    69.6 |  0.249 % |
c |       812 |   72565   214434 |   35413     812    63527    78.2 |  0.249 % |
c |      1320 |   72565   214434 |   38955    1320   105118    79.6 |  0.249 % |
c |      2080 |   72565   214434 |   42850    2080   165349    79.5 |  0.249 % |
c |      3223 |   72565   214434 |   47135    3223   310552    96.4 |  0.249 % |
c |      4935 |   72565   214434 |   51849    4935   616325   124.9 |  0.249 % |
c |      7499 |   72565   214434 |   57034    7499   840033   112.0 |  0.249 % |
c |     11343 |   72565   214434 |   62737   11343  1277041   112.6 |  0.249 % |
c |     17109 |   72565   214434 |   69011   17109  1791043   104.7 |  0.249 % |
c |     25759 |   72565   214434 |   75912   25759  3016387   117.1 |  0.249 % |
c |     38733 |   72565   214434 |   83503   38733  4967013   128.2 |  0.249 % |
c |     58194 |   72565   214434 |   91853   58194  7631175   131.1 |  0.249 % |
c |     87386 |   72565   214434 |  101039   87386 12988322   148.6 |  0.249 % |
c |    131175 |   72565   214434 |  111143   32958  4319172   131.1 |  0.249 % |
c |    196859 |   72565   214434 |  122257   98642 12523288   127.0 |  0.249 % |
#### 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.61 0.90 0.89 2/54 15940
Raw data (stat): 15940 (runsolver) R 15939 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543479889 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 0.67 0.90 0.89 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 2831 0 0 0 992 6 0 0 25 0 1 0 543479889 13537280 2753 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3305 2753 603 41 0 3264 0
vsize: 13220
[startup+20.0021 s]
Raw data (loadavg): 0.72 0.90 0.90 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 3271 0 0 0 1991 8 0 0 25 0 1 0 543479889 15421440 3193 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3765 3193 603 41 0 3724 0
vsize: 15060
[startup+30.0025 s]
Raw data (loadavg): 0.76 0.90 0.90 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 3447 0 0 0 2990 8 0 0 25 0 1 0 543479889 16097280 3369 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3930 3369 603 41 0 3889 0
vsize: 15720
[startup+40.0027 s]
Raw data (loadavg): 0.80 0.91 0.90 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 3555 0 0 0 3990 9 0 0 25 0 1 0 543479889 16633856 3477 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4061 3477 603 41 0 4020 0
vsize: 16244
[startup+50.0035 s]
Raw data (loadavg): 0.83 0.91 0.90 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 4031 0 0 0 4989 10 0 0 25 0 1 0 543479889 18518016 3953 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4521 3953 603 41 0 4480 0
vsize: 18084
[startup+60.004 s]
Raw data (loadavg): 0.85 0.91 0.90 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 4381 0 0 0 5986 13 0 0 25 0 1 0 543479889 19996672 4303 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4882 4303 603 41 0 4841 0
vsize: 19528
[startup+70.0085 s]
Raw data (loadavg): 0.88 0.91 0.90 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 4761 0 0 0 6985 14 0 0 25 0 1 0 543479889 21585920 4683 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5270 4683 603 41 0 5229 0
vsize: 21080
[startup+80.01 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 5286 0 0 0 7984 16 0 0 25 0 1 0 543479889 23744512 5208 4294967295 134512640 134672761 3221224528 3221223664 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5797 5208 603 41 0 5756 0
vsize: 23188
[startup+90.0104 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 5722 0 0 0 8982 18 0 0 25 0 1 0 543479889 25501696 5644 4294967295 134512640 134672761 3221224528 3221223664 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5644 603 41 0 6185 0
vsize: 24904
[startup+100.011 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 6158 0 0 0 9981 19 0 0 25 0 1 0 543479889 27262976 6080 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6656 6080 603 41 0 6615 0
vsize: 26624
[startup+110.011 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 6480 0 0 0 10980 20 0 0 25 0 1 0 543479889 28614656 6402 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6986 6402 603 41 0 6945 0
vsize: 27944
[startup+120.012 s]
Raw data (loadavg): 0.94 0.92 0.91 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 6886 0 0 0 11978 22 0 0 25 0 1 0 543479889 30351360 6808 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7410 6808 603 41 0 7369 0
vsize: 29640
[startup+130.013 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 7299 0 0 0 12977 23 0 0 25 0 1 0 543479889 31956992 7221 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7802 7221 603 41 0 7761 0
vsize: 31208
[startup+140.014 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 7740 0 0 0 13975 25 0 0 25 0 1 0 543479889 33837056 7662 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8261 7662 603 41 0 8220 0
vsize: 33044
[startup+150.014 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 8120 0 0 0 14975 26 0 0 25 0 1 0 543479889 35446784 8042 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8654 8042 603 41 0 8613 0
vsize: 34616
[startup+160.015 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 8509 0 0 0 15974 27 0 0 25 0 1 0 543479889 36929536 8431 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9016 8431 603 41 0 8975 0
vsize: 36064
[startup+170.015 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 8856 0 0 0 16973 28 0 0 25 0 1 0 543479889 38408192 8778 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9377 8778 603 41 0 9336 0
vsize: 37508
[startup+180.015 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 9204 0 0 0 17971 30 0 0 25 0 1 0 543479889 39755776 9126 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9706 9126 603 41 0 9665 0
vsize: 38824
[startup+190.016 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 9519 0 0 0 18970 31 0 0 25 0 1 0 543479889 41099264 9441 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10034 9441 603 41 0 9993 0
vsize: 40136
[startup+200.017 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 9788 0 0 0 19969 32 0 0 25 0 1 0 543479889 42160128 9710 4294967295 134512640 134672761 3221224528 3221223684 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10293 9710 603 41 0 10252 0
vsize: 41172
[startup+210.017 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 10099 0 0 0 20968 34 0 0 25 0 1 0 543479889 43507712 10021 4294967295 134512640 134672761 3221224528 3221223632 134560065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10622 10021 603 41 0 10581 0
vsize: 42488
[startup+220.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15940
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 10393 0 0 0 21967 35 0 0 25 0 1 0 543479889 44580864 10315 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10884 10315 603 41 0 10843 0
vsize: 43536
[startup+230.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 10681 0 0 0 22966 36 0 0 25 0 1 0 543479889 45785088 10603 4294967295 134512640 134672761 3221224528 3221223588 1075346629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11178 10603 603 41 0 11137 0
vsize: 44712
[startup+240.02 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 10895 0 0 0 23965 37 0 0 25 0 1 0 543479889 46739456 10817 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11411 10817 603 41 0 11370 0
vsize: 45644
[startup+250.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 11192 0 0 0 24964 38 0 0 25 0 1 0 543479889 47955968 11114 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11708 11114 603 41 0 11667 0
vsize: 46832
[startup+260.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 11579 0 0 0 25963 39 0 0 25 0 1 0 543479889 49573888 11501 4294967295 134512640 134672761 3221224528 3221223632 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12103 11501 603 41 0 12062 0
vsize: 48412
[startup+270.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 11966 0 0 0 26961 41 0 0 25 0 1 0 543479889 51056640 11888 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11888 603 41 0 12424 0
vsize: 49860
[startup+280.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 12372 0 0 0 27960 43 0 0 25 0 1 0 543479889 53067776 12294 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12956 12294 603 41 0 12915 0
vsize: 51824
[startup+290.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 12750 0 0 0 28959 43 0 0 25 0 1 0 543479889 54546432 12672 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13317 12672 603 41 0 13276 0
vsize: 53268
[startup+300.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 13092 0 0 0 29958 45 0 0 25 0 1 0 543479889 55898112 13014 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13647 13014 603 41 0 13606 0
vsize: 54588
[startup+310.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 13399 0 0 0 30957 45 0 0 25 0 1 0 543479889 57241600 13321 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13975 13321 603 41 0 13934 0
vsize: 55900
[startup+320.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 13705 0 0 0 31957 46 0 0 25 0 1 0 543479889 58454016 13627 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14271 13627 603 41 0 14230 0
vsize: 57084
[startup+330.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 14035 0 0 0 32956 47 0 0 25 0 1 0 543479889 59805696 13957 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14601 13957 603 41 0 14560 0
vsize: 58404
[startup+340.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 14350 0 0 0 33955 48 0 0 25 0 1 0 543479889 61149184 14272 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14929 14272 603 41 0 14888 0
vsize: 59716
[startup+350.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 14700 0 0 0 34954 50 0 0 25 0 1 0 543479889 62496768 14622 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15258 14622 603 41 0 15217 0
vsize: 61032
[startup+360.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 15036 0 0 0 35952 51 0 0 25 0 1 0 543479889 63991808 14958 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15623 14958 603 41 0 15582 0
vsize: 62492
[startup+370.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 15374 0 0 0 36952 52 0 0 25 0 1 0 543479889 65339392 15296 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15952 15296 603 41 0 15911 0
vsize: 63808
[startup+380.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 15691 0 0 0 37950 54 0 0 25 0 1 0 543479889 66703360 15613 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16285 15613 603 41 0 16244 0
vsize: 65140
[startup+390.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 15935 0 0 0 38949 55 0 0 25 0 1 0 543479889 67670016 15857 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16521 15857 603 41 0 16480 0
vsize: 66084
[startup+400.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 16308 0 0 0 39948 56 0 0 25 0 1 0 543479889 69152768 16230 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16883 16230 603 41 0 16842 0
vsize: 67532
[startup+410.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 16562 0 0 0 40947 58 0 0 25 0 1 0 543479889 70221824 16484 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17144 16484 603 41 0 17103 0
vsize: 68576
[startup+420.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 16801 0 0 0 41946 58 0 0 25 0 1 0 543479889 71163904 16723 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17374 16723 603 41 0 17333 0
vsize: 69496
[startup+430.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 16979 0 0 0 42945 59 0 0 25 0 1 0 543479889 71831552 16901 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17537 16901 603 41 0 17496 0
vsize: 70148
[startup+440.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 17183 0 0 0 43945 59 0 0 25 0 1 0 543479889 72765440 17105 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17765 17105 603 41 0 17724 0
vsize: 71060
[startup+450.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 17380 0 0 0 44944 60 0 0 25 0 1 0 543479889 73568256 17302 4294967295 134512640 134672761 3221224528 3221223664 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17961 17302 603 41 0 17920 0
vsize: 71844
[startup+460.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 17559 0 0 0 45944 60 0 0 25 0 1 0 543479889 74244096 17481 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18126 17481 603 41 0 18085 0
vsize: 72504
[startup+470.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 17760 0 0 0 46943 62 0 0 25 0 1 0 543479889 75038720 17682 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18320 17682 603 41 0 18279 0
vsize: 73280
[startup+480.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 17979 0 0 0 47942 62 0 0 25 0 1 0 543479889 75968512 17901 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18547 17901 603 41 0 18506 0
vsize: 74188
[startup+490.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 18177 0 0 0 48942 63 0 0 25 0 1 0 543479889 76763136 18099 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18741 18099 603 41 0 18700 0
vsize: 74964
[startup+500.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 18372 0 0 0 49941 64 0 0 25 0 1 0 543479889 77586432 18294 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18942 18294 603 41 0 18901 0
vsize: 75768
[startup+510.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 18575 0 0 0 50940 66 0 0 25 0 1 0 543479889 78393344 18497 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19139 18497 603 41 0 19098 0
vsize: 76556
[startup+520.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 18772 0 0 0 51939 66 0 0 25 0 1 0 543479889 79192064 18694 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19334 18694 603 41 0 19293 0
vsize: 77336
[startup+530.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 18979 0 0 0 52938 68 0 0 25 0 1 0 543479889 79994880 18901 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19530 18901 603 41 0 19489 0
vsize: 78120
[startup+540.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 19187 0 0 0 53938 68 0 0 25 0 1 0 543479889 80928768 19109 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19758 19109 603 41 0 19717 0
vsize: 79032
[startup+550.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 19389 0 0 0 54937 69 0 0 25 0 1 0 543479889 81735680 19311 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19955 19311 603 41 0 19914 0
vsize: 79820
[startup+560.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 19583 0 0 0 55936 70 0 0 25 0 1 0 543479889 82538496 19505 4294967295 134512640 134672761 3221224528 3221223712 134559176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20151 19505 603 41 0 20110 0
vsize: 80604
[startup+570.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 19801 0 0 0 56935 71 0 0 25 0 1 0 543479889 83345408 19723 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20348 19723 603 41 0 20307 0
vsize: 81392
[startup+580.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20022 0 0 0 57935 72 0 0 25 0 1 0 543479889 84299776 19944 4294967295 134512640 134672761 3221224528 3221223632 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20581 19944 603 41 0 20540 0
vsize: 82324
[startup+590.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20107 0 0 0 58934 72 0 0 25 0 1 0 543479889 84701184 20029 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20679 20029 603 41 0 20638 0
vsize: 82716
[startup+600.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20107 0 0 0 59934 73 0 0 25 0 1 0 543479889 84701184 20029 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20679 20029 603 41 0 20638 0
vsize: 82716
[startup+610.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20107 0 0 0 60934 73 0 0 25 0 1 0 543479889 84701184 20029 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20679 20029 603 41 0 20638 0
vsize: 82716
[startup+620.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20107 0 0 0 61934 73 0 0 25 0 1 0 543479889 84701184 20029 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20679 20029 603 41 0 20638 0
vsize: 82716
[startup+630.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 62934 73 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+640.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 63934 73 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+650.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 64934 73 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+660.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 65935 73 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223684 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+670.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 66934 73 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223712 134558667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+680.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 67935 73 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+690.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 68935 73 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223712 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+700.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 69935 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+710.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 70934 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+720.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 71935 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223664 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+730.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 72935 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+740.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 73935 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+750.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 74935 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+760.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 75935 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+770.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 76935 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+780.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 77936 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223712 134559345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+790.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 78936 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+800.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 79936 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+810.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 80936 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+820.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 81936 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+830.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 82937 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+840.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 83937 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+850.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 84938 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+860.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 85938 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+870.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 86938 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+880.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 87938 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+890.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 88939 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+900.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 89939 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+910.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 90939 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+920.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 91940 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+930.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 92940 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+940.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 93941 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223632 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+950.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 94941 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 95941 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 96941 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+980.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 97942 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+990.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 98943 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 99944 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223664 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 100945 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 101945 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1030.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 102947 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1040.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 103947 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1050.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 104947 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1060.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 105948 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1070.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 106948 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1080.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 107948 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223584 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1090.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 108947 74 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1100.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 109948 75 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1110.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 110947 75 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1120.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 111946 76 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1130.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 112946 76 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1140.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 113946 76 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1150.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 114947 76 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1160.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 115948 76 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1170.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 116949 76 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1180.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 117949 76 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1190.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20109 0 0 0 118949 76 0 0 25 0 1 0 543479889 84701184 20031 4294967295 134512640 134672761 3221224528 3221223632 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20031 603 41 0 20638 0
vsize: 82716
[startup+1200.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15942
Raw data (stat): 15940 (minisat+) R 15939 18865 18864 0 -1 0 20110 0 0 0 119950 76 0 0 25 0 1 0 543479889 84701184 20032 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 20032 603 41 0 20638 0
vsize: 82716
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.25 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 15942
Raw data (stat): 15940 (minisat+) Z 15939 18865 18864 0 -1 12 20112 0 0 0 119950 80 0 0 24 0 1 0 543479889 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.25
CPU time (s): 1200.31
CPU user time (s): 1199.5
CPU system time (s): 0.802877
CPU usage (%): 100.005
Max. virtual memory (Kb): 82716
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####