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 4815

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-13 20:25:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=437 boxname=wulflinc8 idbench=49 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  d4fd8917eebbcee2e1b2df9714e1fab8  /oldhome/oroussel/tmp/wulflinc8/normalized-fpga35_33_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc8/normalized-fpga35_33_sat_pb.cnf.cr.opb
IDLAUNCH: 437
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        913488 kB
Buffers:         36568 kB
Cached:          65228 kB
SwapCached:          0 kB
Active:          72508 kB
Inactive:        32140 kB
HighTotal:      131008 kB
HighFree:        61908 kB
LowTotal:       903652 kB
LowFree:        851580 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            10936 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:45:19 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 437 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.95 0.96 0.91 2/54 28800
Raw data (stat): 28800 (runsolver) R 28799 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 407027298 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 2437 0 0 0 991 6 0 0 25 0 1 0 407027298 11681792 2415 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2852 2415 603 41 0 2811 0
vsize: 11408
[startup+20.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 3775 0 0 0 1987 9 0 0 25 0 1 0 407027298 17186816 3753 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4196 3753 603 41 0 4155 0
vsize: 16784
[startup+30.0033 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 4307 0 0 0 2985 11 0 0 25 0 1 0 407027298 19345408 4285 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4723 4285 603 41 0 4682 0
vsize: 18892
[startup+40.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 4831 0 0 0 3984 12 0 0 25 0 1 0 407027298 21504000 4809 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5250 4809 603 41 0 5209 0
vsize: 21000
[startup+50.0028 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 4832 0 0 0 4984 12 0 0 25 0 1 0 407027298 21504000 4810 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5250 4810 603 41 0 5209 0
vsize: 21000
[startup+60.0038 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 4833 0 0 0 5984 12 0 0 25 0 1 0 407027298 21504000 4811 4294967295 134512640 134672761 3221224624 3221223728 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5250 4811 603 41 0 5209 0
vsize: 21000
[startup+70.0041 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 4833 0 0 0 6984 12 0 0 25 0 1 0 407027298 21504000 4811 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5250 4811 603 41 0 5209 0
vsize: 21000
[startup+80.0055 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 5253 0 0 0 7983 14 0 0 25 0 1 0 407027298 23252992 5231 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5677 5231 603 41 0 5636 0
vsize: 22708
[startup+90.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 5469 0 0 0 8982 14 0 0 25 0 1 0 407027298 24059904 5447 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5874 5447 603 41 0 5833 0
vsize: 23496
[startup+100.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 5539 0 0 0 9982 15 0 0 25 0 1 0 407027298 24358912 5517 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5947 5517 603 41 0 5906 0
vsize: 23788
[startup+110.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 6155 0 0 0 10981 17 0 0 25 0 1 0 407027298 26955776 6133 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6581 6133 603 41 0 6540 0
vsize: 26324
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 6628 0 0 0 11980 17 0 0 25 0 1 0 407027298 29028352 6606 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7087 6606 603 41 0 7046 0
vsize: 28348
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 6919 0 0 0 12979 18 0 0 25 0 1 0 407027298 30261248 6897 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6897 603 41 0 7347 0
vsize: 29552
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 6919 0 0 0 13979 18 0 0 25 0 1 0 407027298 30261248 6897 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6897 603 41 0 7347 0
vsize: 29552
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 6922 0 0 0 14980 18 0 0 25 0 1 0 407027298 30261248 6900 4294967295 134512640 134672761 3221224624 3221223728 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7388 6900 603 41 0 7347 0
vsize: 29552
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 6923 0 0 0 15979 19 0 0 25 0 1 0 407027298 30261248 6901 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 6923 0 0 0 16979 19 0 0 25 0 1 0 407027298 30261248 6901 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 6923 0 0 0 17979 19 0 0 25 0 1 0 407027298 30261248 6901 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 6923 0 0 0 18980 19 0 0 25 0 1 0 407027298 30261248 6901 4294967295 134512640 134672761 3221224624 3221223728 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 6923 0 0 0 19980 19 0 0 25 0 1 0 407027298 30261248 6901 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 6923 0 0 0 20980 19 0 0 25 0 1 0 407027298 30261248 6901 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6901 603 41 0 7347 0
vsize: 29552
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 7055 0 0 0 21980 19 0 0 25 0 1 0 407027298 30806016 7033 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7521 7033 603 41 0 7480 0
vsize: 30084
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 7055 0 0 0 22980 19 0 0 25 0 1 0 407027298 30806016 7033 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7521 7033 603 41 0 7480 0
vsize: 30084
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 7550 0 0 0 23980 20 0 0 25 0 1 0 407027298 32825344 7528 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8014 7528 603 41 0 7973 0
vsize: 32056
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 7550 0 0 0 24980 20 0 0 25 0 1 0 407027298 32825344 7528 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8014 7528 603 41 0 7973 0
vsize: 32056
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 8337 0 0 0 25978 21 0 0 25 0 1 0 407027298 36073472 8315 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8807 8315 603 41 0 8766 0
vsize: 35228
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 8699 0 0 0 26977 23 0 0 25 0 1 0 407027298 37576704 8677 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9174 8677 603 41 0 9133 0
vsize: 36696
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 8699 0 0 0 27977 23 0 0 25 0 1 0 407027298 37576704 8677 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9174 8677 603 41 0 9133 0
vsize: 36696
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 9653 0 0 0 28976 24 0 0 25 0 1 0 407027298 41508864 9631 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10134 9631 603 41 0 10093 0
vsize: 40536
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 9749 0 0 0 29976 25 0 0 25 0 1 0 407027298 41914368 9727 4294967295 134512640 134672761 3221224624 3221223728 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10233 9727 603 41 0 10192 0
vsize: 40932
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 9749 0 0 0 30976 25 0 0 25 0 1 0 407027298 41914368 9727 4294967295 134512640 134672761 3221224624 3221223792 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10233 9727 603 41 0 10192 0
vsize: 40932
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10049 0 0 0 31975 25 0 0 25 0 1 0 407027298 43220992 10027 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10552 10027 603 41 0 10511 0
vsize: 42208
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 32973 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 33972 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 34972 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 35973 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 36973 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 37973 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223728 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 38973 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 39973 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 40974 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 41974 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 42974 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 43974 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 44974 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 45975 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 46974 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 47974 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 48974 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10096 0 0 0 49975 26 0 0 25 0 1 0 407027298 43356160 10074 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 10074 603 41 0 10544 0
vsize: 42340
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10216 0 0 0 50974 27 0 0 25 0 1 0 407027298 43896832 10194 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10717 10194 603 41 0 10676 0
vsize: 42868
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10216 0 0 0 51975 27 0 0 25 0 1 0 407027298 43896832 10194 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10717 10194 603 41 0 10676 0
vsize: 42868
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10216 0 0 0 52975 27 0 0 25 0 1 0 407027298 43896832 10194 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10717 10194 603 41 0 10676 0
vsize: 42868
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 10724 0 0 0 53974 28 0 0 25 0 1 0 407027298 46059520 10702 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11245 10702 603 41 0 11204 0
vsize: 44980
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11272 0 0 0 54973 29 0 0 25 0 1 0 407027298 48218112 11250 4294967295 134512640 134672761 3221224624 3221223812 1075347023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11772 11250 603 41 0 11731 0
vsize: 47088
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11272 0 0 0 55973 29 0 0 25 0 1 0 407027298 48218112 11250 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11772 11250 603 41 0 11731 0
vsize: 47088
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11272 0 0 0 56973 29 0 0 25 0 1 0 407027298 48218112 11250 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11772 11250 603 41 0 11731 0
vsize: 47088
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11272 0 0 0 57973 29 0 0 25 0 1 0 407027298 48218112 11250 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11772 11250 603 41 0 11731 0
vsize: 47088
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11358 0 0 0 58974 29 0 0 25 0 1 0 407027298 48619520 11336 4294967295 134512640 134672761 3221224624 3221223728 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11870 11336 603 41 0 11829 0
vsize: 47480
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11358 0 0 0 59974 29 0 0 25 0 1 0 407027298 48619520 11336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11870 11336 603 41 0 11829 0
vsize: 47480
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11358 0 0 0 60974 29 0 0 25 0 1 0 407027298 48619520 11336 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11870 11336 603 41 0 11829 0
vsize: 47480
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11550 0 0 0 61974 30 0 0 25 0 1 0 407027298 49426432 11528 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12067 11528 603 41 0 12026 0
vsize: 48268
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11550 0 0 0 62974 30 0 0 25 0 1 0 407027298 49426432 11528 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12067 11528 603 41 0 12026 0
vsize: 48268
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11550 0 0 0 63974 30 0 0 25 0 1 0 407027298 49426432 11528 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12067 11528 603 41 0 12026 0
vsize: 48268
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11550 0 0 0 64974 30 0 0 25 0 1 0 407027298 49426432 11528 4294967295 134512640 134672761 3221224624 3221223808 134558934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12067 11528 603 41 0 12026 0
vsize: 48268
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11550 0 0 0 65974 30 0 0 25 0 1 0 407027298 49426432 11528 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12067 11528 603 41 0 12026 0
vsize: 48268
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11586 0 0 0 66975 30 0 0 25 0 1 0 407027298 49561600 11564 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11564 603 41 0 12059 0
vsize: 48400
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 67975 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 68975 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 69975 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+710.029 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 70976 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+720.029 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 71976 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+730.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 72976 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+740.031 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 73976 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+750.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 74976 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223824 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+760.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 75977 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+770.031 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 76977 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+780.031 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 77977 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+790.031 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 78977 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+800.032 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 79977 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+810.032 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 80978 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+820.032 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 81978 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+830.033 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 82978 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+840.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 83978 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+850.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 84978 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+860.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 85979 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223728 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+870.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11587 0 0 0 86978 30 0 0 25 0 1 0 407027298 49561600 11565 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11565 603 41 0 12059 0
vsize: 48400
[startup+880.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 87979 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223840 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+890.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 88979 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+900.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 89979 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+910.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 90979 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+920.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 91979 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+930.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 92980 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+940.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 93980 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+950.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 94980 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+960.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 95980 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+970.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 96980 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+980.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 97981 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+990.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 98981 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 99981 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 100981 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 101981 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 102981 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 103981 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 104982 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 105982 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 106982 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 107982 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 108982 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 109983 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 110983 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 111983 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 112983 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 113983 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 114984 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 115984 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223808 134559611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 116983 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223728 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11590 0 0 0 117983 30 0 0 25 0 1 0 407027298 49561600 11568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11568 603 41 0 12059 0
vsize: 48400
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11591 0 0 0 118984 30 0 0 25 0 1 0 407027298 49561600 11569 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11569 603 41 0 12059 0
vsize: 48400
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28800
Raw data (stat): 28800 (minisat+) R 28799 26667 26666 0 -1 0 11635 0 0 0 119984 30 0 0 25 0 1 0 407027298 49696768 11613 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12133 11613 603 41 0 12092 0
vsize: 48532
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 28800
Raw data (stat): 28800 (minisat+) Z 28799 26667 26666 0 -1 12 11637 0 0 0 119984 33 0 0 25 0 1 0 407027298 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.17
CPU user time (s): 1199.84
CPU system time (s): 0.331949
CPU usage (%): 100.009
Max. virtual memory (Kb): 48532
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####