Some explanations

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

General information on the benchmark

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga40_40_sat_pb.cnf.cr.opb
MD5SUMf9a3a990ebca4aa5457d0675d3f1fe27
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 41
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.9477
Number of variables2400
Total number of constraints1720
Number of constraints which are clauses1640
Number of constraints which are cardinality constraints (but not clauses)80
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint40

Trace number 4817 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-13 20:26:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=482 boxname=wulflinc11 idbench=54 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  f9a3a990ebca4aa5457d0675d3f1fe27  /oldhome/oroussel/tmp/wulflinc11/normalized-fpga40_40_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc11/normalized-fpga40_40_sat_pb.cnf.cr.opb
IDLAUNCH: 482
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        920068 kB
Buffers:         34172 kB
Cached:          56096 kB
SwapCached:       4932 kB
Active:          53232 kB
Inactive:        44848 kB
HighTotal:      131008 kB
HighFree:        71092 kB
LowTotal:       903652 kB
LowFree:        848976 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10944 kB
Committed_AS:    63452 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:46:05 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 482 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1720 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  79]---> BDD-cost:   77
c ---[  78]---> BDD-cost:   77
c ---[  77]---> BDD-cost:   77
c ---[  76]---> BDD-cost:   77
c ---[  75]---> BDD-cost:   77
c ---[  74]---> BDD-cost:   77
c ---[  73]---> BDD-cost:   77
c ---[  72]---> BDD-cost:   77
c ---[  71]---> BDD-cost:   77
c ---[  70]---> BDD-cost:   77
c ---[  69]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  67]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  65]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  63]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   77
c ---[  61]---> BDD-cost:   77
c ---[  60]---> BDD-cost:   77
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   37
c ---[  38]---> BDD-cost:   37
c ---[  37]---> BDD-cost:   37
c ---[  36]---> BDD-cost:   37
c ---[  35]---> BDD-cost:   37
c ---[  34]---> BDD-cost:   37
c ---[  33]---> BDD-cost:   37
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   37
c ---[  30]---> BDD-cost:   37
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12920    64560 |    4306       0        0     nan |  0.000 % |
c |       100 |   12920    64560 |    4736     100    26004   260.0 |  1.149 % |
c |       252 |   12920    64560 |    5210     252    37714   149.7 |  1.150 % |
c |       477 |   12920    64560 |    5731     477    76875   161.2 |  1.149 % |
c |       814 |   12920    64560 |    6304     814   161811   198.8 |  1.149 % |
c |      1321 |   12920    64560 |    6934    1321   261531   198.0 |  1.149 % |
c |      2084 |   12920    64560 |    7628    2084   359745   172.6 |  1.149 % |
c |      3223 |   12920    64560 |    8391    3223   791517   245.6 |  1.149 % |
c |      4932 |   12920    64560 |    9230    4932  1197916   242.9 |  1.149 % |
c |      7496 |   12920    64560 |   10153    7496  2266760   302.4 |  1.150 % |
c |     11341 |   12920    64560 |   11168   11341  3377694   297.8 |  1.149 % |
c |     17108 |   12920    64560 |   12285   11438  4096533   358.2 |  1.149 % |
c |     25758 |   12920    64560 |   13514   12002  3744055   312.0 |  1.149 % |
c |     38732 |   12920    64560 |   14865   15473  2381199   153.9 |  1.149 % |
c |     58193 |   12920    64560 |   16352   17728  7855736   443.1 |  1.149 % |
c |     87385 |   12920    64560 |   17987   17936  6971394   388.7 |  1.149 % |
c |    131175 |   12920    64560 |   19785   15044  2526709   168.0 |  1.149 % |
c |    196861 |   12920    64560 |   21764   20319  9340279   459.7 |  1.149 % |
c |    295389 |   12920    64560 |   23941   18363  2895214   157.7 |  1.149 % |
#### 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.83 0.90 0.89 2/54 3185
Raw data (stat): 3185 (runsolver) R 3184 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420594268 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.86 0.90 0.89 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 3102 0 0 0 990 8 0 0 25 0 1 0 420594268 14258176 3080 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3481 3080 603 41 0 3440 0
vsize: 13924
[startup+20.0017 s]
Raw data (loadavg): 0.88 0.90 0.89 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 4473 0 0 0 1986 11 0 0 25 0 1 0 420594268 19931136 4451 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4866 4451 603 41 0 4825 0
vsize: 19464
[startup+30.0011 s]
Raw data (loadavg): 0.90 0.90 0.89 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 5195 0 0 0 2985 13 0 0 25 0 1 0 420594268 22892544 5173 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5589 5173 603 41 0 5548 0
vsize: 22356
[startup+40.0015 s]
Raw data (loadavg): 0.91 0.91 0.89 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 6723 0 0 0 3981 16 0 0 25 0 1 0 420594268 29102080 6701 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7105 6701 603 41 0 7064 0
vsize: 28420
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.91 0.89 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 6759 0 0 0 4981 16 0 0 25 0 1 0 420594268 29237248 6737 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7138 6737 603 41 0 7097 0
vsize: 28552
[startup+60.0025 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 6759 0 0 0 5981 16 0 0 25 0 1 0 420594268 29237248 6737 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7138 6737 603 41 0 7097 0
vsize: 28552
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 6759 0 0 0 6981 16 0 0 25 0 1 0 420594268 29237248 6737 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7138 6737 603 41 0 7097 0
vsize: 28552
[startup+80.0044 s]
Raw data (loadavg): 0.95 0.92 0.89 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 6759 0 0 0 7982 16 0 0 25 0 1 0 420594268 29237248 6737 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7138 6737 603 41 0 7097 0
vsize: 28552
[startup+90.0049 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 6759 0 0 0 8982 16 0 0 25 0 1 0 420594268 29237248 6737 4294967295 134512640 134672761 3221224624 3221223728 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7138 6737 603 41 0 7097 0
vsize: 28552
[startup+100.005 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 7299 0 0 0 9980 18 0 0 25 0 1 0 420594268 31539200 7277 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7700 7277 603 41 0 7659 0
vsize: 30800
[startup+110.006 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 7637 0 0 0 10980 18 0 0 25 0 1 0 420594268 32882688 7615 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8028 7615 603 41 0 7987 0
vsize: 32112
[startup+120.006 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 7637 0 0 0 11980 18 0 0 25 0 1 0 420594268 32882688 7615 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8028 7615 603 41 0 7987 0
vsize: 32112
[startup+130.006 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 7666 0 0 0 12980 19 0 0 25 0 1 0 420594268 33038336 7644 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8066 7644 603 41 0 8025 0
vsize: 32264
[startup+140.007 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 7906 0 0 0 13980 19 0 0 25 0 1 0 420594268 33988608 7884 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8298 7884 603 41 0 8257 0
vsize: 33192
[startup+150.008 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 8517 0 0 0 14979 21 0 0 25 0 1 0 420594268 36552704 8495 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8924 8495 603 41 0 8883 0
vsize: 35696
[startup+160.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 9246 0 0 0 15977 22 0 0 25 0 1 0 420594268 39530496 9224 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9651 9224 603 41 0 9610 0
vsize: 38604
[startup+170.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 9748 0 0 0 16975 24 0 0 25 0 1 0 420594268 41545728 9726 4294967295 134512640 134672761 3221224624 3221223808 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+180.008 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 9748 0 0 0 17975 24 0 0 25 0 1 0 420594268 41545728 9726 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+190.009 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 9748 0 0 0 18975 24 0 0 25 0 1 0 420594268 41545728 9726 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+200.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 9748 0 0 0 19975 24 0 0 25 0 1 0 420594268 41545728 9726 4294967295 134512640 134672761 3221224624 3221223808 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+210.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 9748 0 0 0 20975 24 0 0 25 0 1 0 420594268 41545728 9726 4294967295 134512640 134672761 3221224624 3221223756 1075347104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+220.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 9748 0 0 0 21975 24 0 0 25 0 1 0 420594268 41545728 9726 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+230.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 9748 0 0 0 22975 24 0 0 25 0 1 0 420594268 41545728 9726 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+240.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 9748 0 0 0 23976 24 0 0 25 0 1 0 420594268 41545728 9726 4294967295 134512640 134672761 3221224624 3221223808 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+250.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 9748 0 0 0 24976 24 0 0 25 0 1 0 420594268 41545728 9726 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+260.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 10023 0 0 0 25975 25 0 0 25 0 1 0 420594268 42827776 10001 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10456 10001 603 41 0 10415 0
vsize: 41824
[startup+270.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 10038 0 0 0 26975 25 0 0 25 0 1 0 420594268 42827776 10016 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10456 10016 603 41 0 10415 0
vsize: 41824
[startup+280.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 10058 0 0 0 27976 25 0 0 25 0 1 0 420594268 42983424 10036 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10494 10036 603 41 0 10453 0
vsize: 41976
[startup+290.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 10102 0 0 0 28976 25 0 0 25 0 1 0 420594268 43180032 10080 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10542 10080 603 41 0 10501 0
vsize: 42168
[startup+300.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 10135 0 0 0 29976 25 0 0 25 0 1 0 420594268 43376640 10113 4294967295 134512640 134672761 3221224624 3221223808 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10590 10113 603 41 0 10549 0
vsize: 42360
[startup+310.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 30972 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223376 134565834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+320.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 31972 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223728 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+330.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 32972 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+340.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 33972 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+350.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 34972 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+360.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 35973 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+370.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 36973 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+380.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 37973 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+390.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 38973 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+400.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 39973 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+410.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 40974 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223728 134560150 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+420.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 41974 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+430.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 42974 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+440.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 43974 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 11213 0 0 0 44974 29 0 0 25 0 1 0 420594268 47816704 11191 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 12450 0 0 0 45972 32 0 0 25 0 1 0 420594268 52944896 12428 4294967295 134512640 134672761 3221224624 3221223728 134560019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 12428 603 41 0 12885 0
vsize: 51704
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 13790 0 0 0 46969 34 0 0 25 0 1 0 420594268 58351616 13768 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14246 13768 603 41 0 14205 0
vsize: 56984
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 13896 0 0 0 47969 35 0 0 25 0 1 0 420594268 58892288 13874 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13874 603 41 0 14337 0
vsize: 57512
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 13896 0 0 0 48969 35 0 0 25 0 1 0 420594268 58892288 13874 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13874 603 41 0 14337 0
vsize: 57512
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 13896 0 0 0 49970 35 0 0 25 0 1 0 420594268 58892288 13874 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13874 603 41 0 14337 0
vsize: 57512
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 13896 0 0 0 50970 35 0 0 25 0 1 0 420594268 58892288 13874 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13874 603 41 0 14337 0
vsize: 57512
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14182 0 0 0 51969 35 0 0 25 0 1 0 420594268 59973632 14160 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14642 14160 603 41 0 14601 0
vsize: 58568
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14376 0 0 0 52969 36 0 0 25 0 1 0 420594268 60788736 14354 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14841 14354 603 41 0 14800 0
vsize: 59364
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14376 0 0 0 53969 36 0 0 25 0 1 0 420594268 60788736 14354 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14841 14354 603 41 0 14800 0
vsize: 59364
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14376 0 0 0 54969 36 0 0 25 0 1 0 420594268 60788736 14354 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14841 14354 603 41 0 14800 0
vsize: 59364
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14376 0 0 0 55969 36 0 0 25 0 1 0 420594268 60788736 14354 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14841 14354 603 41 0 14800 0
vsize: 59364
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14376 0 0 0 56970 36 0 0 25 0 1 0 420594268 60788736 14354 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14841 14354 603 41 0 14800 0
vsize: 59364
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14377 0 0 0 57970 36 0 0 25 0 1 0 420594268 60788736 14355 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14841 14355 603 41 0 14800 0
vsize: 59364
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14377 0 0 0 58969 36 0 0 25 0 1 0 420594268 60788736 14355 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14841 14355 603 41 0 14800 0
vsize: 59364
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14377 0 0 0 59969 36 0 0 25 0 1 0 420594268 60788736 14355 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14841 14355 603 41 0 14800 0
vsize: 59364
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14377 0 0 0 60970 36 0 0 25 0 1 0 420594268 60788736 14355 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14841 14355 603 41 0 14800 0
vsize: 59364
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14549 0 0 0 61969 37 0 0 25 0 1 0 420594268 61464576 14527 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15006 14527 603 41 0 14965 0
vsize: 60024
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14549 0 0 0 62969 37 0 0 25 0 1 0 420594268 61464576 14527 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15006 14527 603 41 0 14965 0
vsize: 60024
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14549 0 0 0 63970 37 0 0 25 0 1 0 420594268 61464576 14527 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15006 14527 603 41 0 14965 0
vsize: 60024
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14549 0 0 0 64970 37 0 0 25 0 1 0 420594268 61464576 14527 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15006 14527 603 41 0 14965 0
vsize: 60024
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14549 0 0 0 65970 37 0 0 25 0 1 0 420594268 61464576 14527 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15006 14527 603 41 0 14965 0
vsize: 60024
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 66969 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223784 134559749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 67970 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 68970 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 69970 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 70970 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 71970 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 72970 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 73971 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 74971 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 75971 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 76971 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223808 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 77971 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223728 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 78972 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 79972 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 80972 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14670 0 0 0 81972 37 0 0 25 0 1 0 420594268 62005248 14648 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 82972 37 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 83973 37 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+850.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 84973 37 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 85973 37 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 86973 37 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 87973 37 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 88973 37 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 89974 37 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 90973 38 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 91973 38 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 92973 38 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 93973 38 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 94974 38 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 95974 38 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+970.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14671 0 0 0 96974 38 0 0 25 0 1 0 420594268 62005248 14649 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+980.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 14908 0 0 0 97973 38 0 0 25 0 1 0 420594268 62951424 14886 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15369 14886 603 41 0 15328 0
vsize: 61476
[startup+990.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 15738 0 0 0 98971 41 0 0 25 0 1 0 420594268 66465792 15716 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16227 15716 603 41 0 16186 0
vsize: 64908
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 16448 0 0 0 99970 42 0 0 25 0 1 0 420594268 69304320 16426 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16920 16426 603 41 0 16879 0
vsize: 67680
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17107 0 0 0 100968 44 0 0 25 0 1 0 420594268 72007680 17085 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17580 17085 603 41 0 17539 0
vsize: 70320
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17454 0 0 0 101967 45 0 0 25 0 1 0 420594268 73494528 17432 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17432 603 41 0 17902 0
vsize: 71772
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17455 0 0 0 102967 45 0 0 25 0 1 0 420594268 73494528 17433 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17433 603 41 0 17902 0
vsize: 71772
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17456 0 0 0 103967 45 0 0 25 0 1 0 420594268 73494528 17434 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17434 603 41 0 17902 0
vsize: 71772
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17456 0 0 0 104968 45 0 0 25 0 1 0 420594268 73494528 17434 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17434 603 41 0 17902 0
vsize: 71772
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17457 0 0 0 105968 45 0 0 25 0 1 0 420594268 73494528 17435 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17435 603 41 0 17902 0
vsize: 71772
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17457 0 0 0 106968 45 0 0 25 0 1 0 420594268 73494528 17435 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17435 603 41 0 17902 0
vsize: 71772
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17457 0 0 0 107968 45 0 0 25 0 1 0 420594268 73494528 17435 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17435 603 41 0 17902 0
vsize: 71772
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17457 0 0 0 108968 45 0 0 25 0 1 0 420594268 73494528 17435 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17435 603 41 0 17902 0
vsize: 71772
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17460 0 0 0 109969 45 0 0 25 0 1 0 420594268 73494528 17438 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17438 603 41 0 17902 0
vsize: 71772
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17460 0 0 0 110969 45 0 0 25 0 1 0 420594268 73494528 17438 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17438 603 41 0 17902 0
vsize: 71772
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17460 0 0 0 111969 45 0 0 25 0 1 0 420594268 73494528 17438 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17438 603 41 0 17902 0
vsize: 71772
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17460 0 0 0 112969 45 0 0 25 0 1 0 420594268 73494528 17438 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17943 17438 603 41 0 17902 0
vsize: 71772
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 17729 0 0 0 113968 47 0 0 25 0 1 0 420594268 74575872 17707 4294967295 134512640 134672761 3221224624 3221223808 134559548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18207 17707 603 41 0 18166 0
vsize: 72828
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 18226 0 0 0 114967 48 0 0 25 0 1 0 420594268 76603392 18204 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18702 18204 603 41 0 18661 0
vsize: 74808
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 18834 0 0 0 115965 50 0 0 25 0 1 0 420594268 79171584 18812 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19329 18812 603 41 0 19288 0
vsize: 77316
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 19283 0 0 0 116964 51 0 0 25 0 1 0 420594268 80928768 19261 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19758 19261 603 41 0 19717 0
vsize: 79032
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 19719 0 0 0 117963 52 0 0 25 0 1 0 420594268 82698240 19697 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20190 19697 603 41 0 20149 0
vsize: 80760
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 20297 0 0 0 118963 53 0 0 25 0 1 0 420594268 85135360 20275 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20785 20275 603 41 0 20744 0
vsize: 83140
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3185
Raw data (stat): 3185 (minisat+) R 3184 32461 32460 0 -1 0 20734 0 0 0 119962 54 0 0 25 0 1 0 420594268 86892544 20712 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21214 20712 603 41 0 21173 0
vsize: 84856
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3185
Raw data (stat): 3185 (minisat+) Z 3184 32461 32460 0 -1 12 20736 0 0 0 119962 58 0 0 25 0 1 0 420594268 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.21
CPU user time (s): 1199.63
CPU system time (s): 0.580911
CPU usage (%): 100.011
Max. virtual memory (Kb): 84856
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####