PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga35_33_sat_pb.cnf.cr.opb
MD5SUM	d4fd8917eebbcee2e1b2df9714e1fab8
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
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	36
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.59276
Number of variables	1733
Total number of constraints	1256
Number of constraints which are clauses	1188
Number of constraints which are cardinality constraints (but not clauses)	68
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	17
Maximum length of a constraint	35
Trace number 5777

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-14 01:44:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4185 boxname=wulflinc19 idbench=49 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d4fd8917eebbcee2e1b2df9714e1fab8  /oldhome/oroussel/tmp/wulflinc19/normalized-fpga35_33_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-fpga35_33_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc19/normalized-fpga35_33_sat_pb.cnf.cr.opb
IDLAUNCH: 4185
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        882604 kB
Buffers:         35128 kB
Cached:          82932 kB
SwapCached:         56 kB
Active:          48728 kB
Inactive:        72320 kB
HighTotal:      131008 kB
HighFree:        43960 kB
LowTotal:       903652 kB
LowFree:        838644 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25244 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:04:08 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 4185 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1256 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  67]---> BDD-cost:   63
c ---[  66]---> BDD-cost:   63
c ---[  65]---> BDD-cost:   63
c ---[  64]---> BDD-cost:   63
c ---[  63]---> BDD-cost:   63
c ---[  62]---> BDD-cost:   63
c ---[  61]---> BDD-cost:   63
c ---[  60]---> BDD-cost:   63
c ---[  59]---> BDD-cost:   63
c ---[  58]---> BDD-cost:   63
c ---[  57]---> BDD-cost:   63
c ---[  56]---> BDD-cost:   63
c ---[  55]---> BDD-cost:   63
c ---[  54]---> BDD-cost:   63
c ---[  53]---> BDD-cost:   63
c ---[  52]---> BDD-cost:   63
c ---[  51]---> BDD-cost:   63
c ---[  50]---> BDD-cost:   63
c ---[  49]---> BDD-cost:   63
c ---[  48]---> BDD-cost:   63
c ---[  47]---> BDD-cost:   63
c ---[  46]---> BDD-cost:   63
c ---[  45]---> BDD-cost:   63
c ---[  44]---> BDD-cost:   63
c ---[  43]---> BDD-cost:   63
c ---[  42]---> BDD-cost:   63
c ---[  41]---> BDD-cost:   63
c ---[  40]---> BDD-cost:   63
c ---[  39]---> BDD-cost:   63
c ---[  38]---> BDD-cost:   63
c ---[  37]---> BDD-cost:   63
c ---[  36]---> BDD-cost:   63
c ---[  35]---> BDD-cost:   63
c ---[  34]---> BDD-cost:   63
c ---[  33]---> BDD-cost:   63
c ---[  32]---> BDD-cost:   31
c ---[  31]---> BDD-cost:   31
c ---[  30]---> BDD-cost:   31
c ---[  29]---> BDD-cost:   31
c ---[  28]---> BDD-cost:   31
c ---[  27]---> BDD-cost:   31
c ---[  26]---> BDD-cost:   31
c ---[  25]---> BDD-cost:   31
c ---[  24]---> BDD-cost:   31
c ---[  23]---> BDD-cost:   31
c ---[  22]---> BDD-cost:   31
c ---[  21]---> BDD-cost:   31
c ---[  20]---> BDD-cost:   31
c ---[  19]---> BDD-cost:   31
c ---[  18]---> BDD-cost:   31
c ---[  17]---> BDD-cost:   31
c ---[  16]---> BDD-cost:   33
c ---[  15]---> BDD-cost:   33
c ---[  14]---> BDD-cost:   33
c ---[  13]---> BDD-cost:   33
c ---[  12]---> BDD-cost:   33
c ---[  11]---> BDD-cost:   33
c ---[  10]---> BDD-cost:   33
c ---[   9]---> BDD-cost:   33
c ---[   8]---> BDD-cost:   33
c ---[   7]---> BDD-cost:   33
c ---[   6]---> BDD-cost:   33
c ---[   5]---> BDD-cost:   33
c ---[   4]---> BDD-cost:   33
c ---[   3]---> BDD-cost:   33
c ---[   2]---> BDD-cost:   33
c ---[   1]---> BDD-cost:   33
c ---[   0]---> BDD-cost:   33
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9241    42349 |    3080       0        0     nan |  0.000 % |
c |       100 |    9241    42349 |    3388     100    15655   156.6 |  1.361 % |
c |       251 |    9241    42349 |    3726     251    45524   181.4 |  1.361 % |
c |       477 |    9241    42349 |    4099     477    72619   152.2 |  1.361 % |
c |       815 |    9241    42349 |    4509     815   137613   168.9 |  1.361 % |
c |      1322 |    9241    42349 |    4960    1322   223413   169.0 |  1.361 % |
c |      2081 |    9241    42349 |    5456    2081   293330   141.0 |  1.362 % |
c |      3223 |    9241    42349 |    6002    3223   525259   163.0 |  1.361 % |
c |      4931 |    9241    42349 |    6602    4931   873479   177.1 |  1.361 % |
c |      7494 |    9241    42349 |    7262    7494  1597298   213.1 |  1.361 % |
c |     11339 |    9241    42349 |    7988    7592  1338646   176.3 |  1.361 % |
c |     17107 |    9241    42349 |    8787    7763  2704212   348.3 |  1.361 % |
c |     25757 |    9241    42349 |    9666   10514  3001293   285.5 |  1.361 % |
c |     38731 |    9241    42349 |   10632   11242  1345782   119.7 |  1.361 % |
c |     58192 |    9241    42349 |   11696   11240  4033306   358.8 |  1.361 % |
c |     87385 |    9241    42349 |   12865    9358  1029457   110.0 |  1.361 % |
c |    131177 |    9241    42349 |   14152   14128  7100707   502.6 |  1.361 % |
c |    196865 |    9241    42349 |   15567   17525  2100766   119.9 |  1.361 % |
c |    295391 |    9241    42349 |   17124   17347  7062254   407.1 |  1.361 % |
c |    443181 |    9241    42349 |   18836   11564  1917772   165.8 |  1.361 % |
#### 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.81 0.94 0.91 2/55 28060
Raw data (stat): 28060 (runsolver) R 28059 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480721520 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.84 0.94 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 2437 0 0 0 992 6 0 0 25 0 1 0 480721520 11681792 2415 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2852 2415 603 41 0 2811 0
vsize: 11408
[startup+20.0018 s]
Raw data (loadavg): 0.86 0.94 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 3773 0 0 0 1987 11 0 0 25 0 1 0 480721520 17186816 3751 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4196 3751 603 41 0 4155 0
vsize: 16784
[startup+30.0022 s]
Raw data (loadavg): 0.88 0.94 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 4294 0 0 0 2985 13 0 0 25 0 1 0 480721520 19210240 4272 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4690 4272 603 41 0 4649 0
vsize: 18760
[startup+40.0019 s]
Raw data (loadavg): 0.90 0.94 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 4831 0 0 0 3983 14 0 0 25 0 1 0 480721520 21504000 4809 4294967295 134512640 134672761 3221224528 3221223712 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5250 4809 603 41 0 5209 0
vsize: 21000
[startup+50.0029 s]
Raw data (loadavg): 0.91 0.94 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 4832 0 0 0 4984 14 0 0 25 0 1 0 480721520 21504000 4810 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5250 4810 603 41 0 5209 0
vsize: 21000
[startup+60.0026 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 4833 0 0 0 5984 14 0 0 25 0 1 0 480721520 21504000 4811 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5250 4811 603 41 0 5209 0
vsize: 21000
[startup+70.0033 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 4833 0 0 0 6983 14 0 0 25 0 1 0 480721520 21504000 4811 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5250 4811 603 41 0 5209 0
vsize: 21000
[startup+80.0044 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 5238 0 0 0 7981 16 0 0 25 0 1 0 480721520 23117824 5216 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5644 5216 603 41 0 5603 0
vsize: 22576
[startup+90.0039 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 5469 0 0 0 8981 16 0 0 25 0 1 0 480721520 24059904 5447 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5874 5447 603 41 0 5833 0
vsize: 23496
[startup+100.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 5526 0 0 0 9981 17 0 0 25 0 1 0 480721520 24358912 5504 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5947 5504 603 41 0 5906 0
vsize: 23788
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 6145 0 0 0 10979 18 0 0 25 0 1 0 480721520 26955776 6123 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6581 6123 603 41 0 6540 0
vsize: 26324
[startup+120.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 28060
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 6621 0 0 0 11978 20 0 0 25 0 1 0 480721520 29028352 6599 4294967295 134512640 134672761 3221224528 3221223632 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7087 6599 603 41 0 7046 0
vsize: 28348
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 6919 0 0 0 12977 21 0 0 25 0 1 0 480721520 30261248 6897 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7388 6897 603 41 0 7347 0
vsize: 29552
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 6919 0 0 0 13977 21 0 0 25 0 1 0 480721520 30261248 6897 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7388 6897 603 41 0 7347 0
vsize: 29552
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 6922 0 0 0 14978 21 0 0 25 0 1 0 480721520 30261248 6900 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6900 603 41 0 7347 0
vsize: 29552
[startup+160.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 6923 0 0 0 15977 21 0 0 25 0 1 0 480721520 30261248 6901 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 6923 0 0 0 16978 21 0 0 25 0 1 0 480721520 30261248 6901 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 6923 0 0 0 17978 21 0 0 25 0 1 0 480721520 30261248 6901 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 6923 0 0 0 18978 21 0 0 25 0 1 0 480721520 30261248 6901 4294967295 134512640 134672761 3221224528 3221223632 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 6923 0 0 0 19978 21 0 0 25 0 1 0 480721520 30261248 6901 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 6923 0 0 0 20978 21 0 0 25 0 1 0 480721520 30261248 6901 4294967295 134512640 134672761 3221224528 3221223712 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 7053 0 0 0 21978 21 0 0 25 0 1 0 480721520 30801920 7031 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7520 7031 603 41 0 7479 0
vsize: 30080
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 7053 0 0 0 22978 21 0 0 25 0 1 0 480721520 30801920 7031 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7520 7031 603 41 0 7479 0
vsize: 30080
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 7548 0 0 0 23977 23 0 0 25 0 1 0 480721520 32821248 7526 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8013 7526 603 41 0 7972 0
vsize: 32052
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 7548 0 0 0 24977 23 0 0 25 0 1 0 480721520 32821248 7526 4294967295 134512640 134672761 3221224528 3221223712 134558756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8013 7526 603 41 0 7972 0
vsize: 32052
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 8310 0 0 0 25976 24 0 0 25 0 1 0 480721520 35934208 8288 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8773 8288 603 41 0 8732 0
vsize: 35092
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 8700 0 0 0 26975 25 0 0 25 0 1 0 480721520 37568512 8678 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9172 8678 603 41 0 9131 0
vsize: 36688
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 8700 0 0 0 27975 25 0 0 25 0 1 0 480721520 37568512 8678 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9172 8678 603 41 0 9131 0
vsize: 36688
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 9587 0 0 0 28974 26 0 0 25 0 1 0 480721520 41230336 9565 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10066 9565 603 41 0 10025 0
vsize: 40264
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 9749 0 0 0 29974 27 0 0 25 0 1 0 480721520 41906176 9727 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10231 9727 603 41 0 10190 0
vsize: 40924
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 9749 0 0 0 30974 27 0 0 25 0 1 0 480721520 41906176 9727 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10231 9727 603 41 0 10190 0
vsize: 40924
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10022 0 0 0 31973 28 0 0 25 0 1 0 480721520 43085824 10000 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10519 10000 603 41 0 10478 0
vsize: 42076
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 32972 28 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223632 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 33973 28 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 34973 29 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 35973 29 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223632 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 36973 29 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 37973 29 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 38973 29 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 39973 29 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 40974 29 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28062
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 41974 29 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 42974 29 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 43974 29 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223632 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 44974 29 0 0 25 0 1 0 480721520 43356160 10075 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10075 603 41 0 10544 0
vsize: 42340
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 45974 29 0 0 25 0 1 0 480721520 43339776 10075 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10581 10075 603 41 0 10540 0
vsize: 42324
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 46974 29 0 0 25 0 1 0 480721520 43339776 10075 4294967295 134512640 134672761 3221224528 3221223632 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10581 10075 603 41 0 10540 0
vsize: 42324
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 47974 29 0 0 25 0 1 0 480721520 43339776 10075 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10581 10075 603 41 0 10540 0
vsize: 42324
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 48974 29 0 0 25 0 1 0 480721520 43339776 10075 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10581 10075 603 41 0 10540 0
vsize: 42324
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10097 0 0 0 49975 29 0 0 25 0 1 0 480721520 43339776 10075 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10581 10075 603 41 0 10540 0
vsize: 42324
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10214 0 0 0 50975 29 0 0 25 0 1 0 480721520 43880448 10192 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10713 10192 603 41 0 10672 0
vsize: 42852
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10214 0 0 0 51975 29 0 0 25 0 1 0 480721520 43880448 10192 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10713 10192 603 41 0 10672 0
vsize: 42852
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10214 0 0 0 52975 29 0 0 25 0 1 0 480721520 43880448 10192 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10713 10192 603 41 0 10672 0
vsize: 42852
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 10731 0 0 0 53974 31 0 0 25 0 1 0 480721520 46043136 10709 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11241 10709 603 41 0 11200 0
vsize: 44964
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11267 0 0 0 54972 32 0 0 25 0 1 0 480721520 48205824 11245 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11769 11245 603 41 0 11728 0
vsize: 47076
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11267 0 0 0 55972 32 0 0 25 0 1 0 480721520 48205824 11245 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11769 11245 603 41 0 11728 0
vsize: 47076
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11267 0 0 0 56972 33 0 0 25 0 1 0 480721520 48205824 11245 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11769 11245 603 41 0 11728 0
vsize: 47076
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11267 0 0 0 57972 33 0 0 25 0 1 0 480721520 48205824 11245 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11769 11245 603 41 0 11728 0
vsize: 47076
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11359 0 0 0 58972 33 0 0 25 0 1 0 480721520 48611328 11337 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11868 11337 603 41 0 11827 0
vsize: 47472
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11359 0 0 0 59972 33 0 0 25 0 1 0 480721520 48611328 11337 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11868 11337 603 41 0 11827 0
vsize: 47472
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11359 0 0 0 60972 33 0 0 25 0 1 0 480721520 48611328 11337 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11868 11337 603 41 0 11827 0
vsize: 47472
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11559 0 0 0 61972 34 0 0 25 0 1 0 480721520 49442816 11537 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12071 11537 603 41 0 12030 0
vsize: 48284
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11559 0 0 0 62972 34 0 0 25 0 1 0 480721520 49442816 11537 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12071 11537 603 41 0 12030 0
vsize: 48284
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11559 0 0 0 63972 34 0 0 25 0 1 0 480721520 49442816 11537 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12071 11537 603 41 0 12030 0
vsize: 48284
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11559 0 0 0 64972 34 0 0 25 0 1 0 480721520 49442816 11537 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12071 11537 603 41 0 12030 0
vsize: 48284
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11559 0 0 0 65972 34 0 0 25 0 1 0 480721520 49442816 11537 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12071 11537 603 41 0 12030 0
vsize: 48284
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11595 0 0 0 66972 34 0 0 25 0 1 0 480721520 49577984 11573 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11573 603 41 0 12063 0
vsize: 48416
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11595 0 0 0 67973 34 0 0 25 0 1 0 480721520 49577984 11573 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11573 603 41 0 12063 0
vsize: 48416
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11595 0 0 0 68973 34 0 0 25 0 1 0 480721520 49577984 11573 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11573 603 41 0 12063 0
vsize: 48416
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 69973 34 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223528 1075350371 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 70973 34 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28064
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 71973 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 72973 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 73973 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 74974 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 75974 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 76974 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 77974 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 78974 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 79974 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 80974 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 81975 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 82975 35 0 0 25 0 1 0 480721520 49577984 11574 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12104 11574 603 41 0 12063 0
vsize: 48416
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 83975 35 0 0 25 0 1 0 480721520 49500160 11570 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12085 11570 603 41 0 12044 0
vsize: 48340
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 84975 35 0 0 25 0 1 0 480721520 49500160 11570 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12085 11570 603 41 0 12044 0
vsize: 48340
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 85975 35 0 0 25 0 1 0 480721520 49491968 11568 4294967295 134512640 134672761 3221224528 3221223632 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12083 11568 603 41 0 12042 0
vsize: 48332
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11596 0 0 0 86975 35 0 0 25 0 1 0 480721520 49491968 11568 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11568 603 41 0 12042 0
vsize: 48332
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 87975 35 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 88975 35 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 89975 35 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 90975 35 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 91975 35 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+930.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 92975 35 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 93976 36 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+950.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28066
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 94976 36 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+960.025 s]
Raw data (loadavg): 1.07 0.99 0.92 3/58 28107
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 95975 36 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+970.026 s]
Raw data (loadavg): 1.06 0.99 0.92 2/55 28119
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 96975 36 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223712 134559553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+980.027 s]
Raw data (loadavg): 1.05 0.99 0.92 2/55 28119
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 97975 36 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+990.026 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 28119
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 98974 36 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1000.03 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 28119
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 99974 36 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1010.03 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 28119
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 100974 36 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223712 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1020.03 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 28119
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 101974 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1030.03 s]
Raw data (loadavg): 1.09 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 102974 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223632 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1040.03 s]
Raw data (loadavg): 1.08 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 103974 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1050.03 s]
Raw data (loadavg): 1.07 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 104974 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1060.03 s]
Raw data (loadavg): 1.06 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 105974 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1070.03 s]
Raw data (loadavg): 1.05 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 106975 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1080.03 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 107975 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1090.03 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 108975 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1100.03 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 109975 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1110.03 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 110975 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1120.03 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 111975 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1130.03 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 112975 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1140.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 113975 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1150.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 114976 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223600 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1160.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 115976 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223624 134555595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1170.03 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 116975 37 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223632 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11599 0 0 0 117976 38 0 0 25 0 1 0 480721520 49491968 11571 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11571 603 41 0 12042 0
vsize: 48332
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11600 0 0 0 118976 38 0 0 25 0 1 0 480721520 49491968 11572 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12083 11572 603 41 0 12042 0
vsize: 48332
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 28123
Raw data (stat): 28060 (minisat+) R 28059 22929 22928 0 -1 0 11699 0 0 0 119976 38 0 0 25 0 1 0 480721520 50036736 11671 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11671 603 41 0 12175 0
vsize: 48864
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.93 1/55 28123
Raw data (stat): 28060 (minisat+) Z 28059 22929 22928 0 -1 12 11701 0 0 0 119976 40 0 0 25 0 1 0 480721520 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.05
CPU time (s): 1200.17
CPU user time (s): 1199.76
CPU system time (s): 0.404938
CPU usage (%): 100.01
Max. virtual memory (Kb): 48864
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####