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-chnl40_45_pb.cnf.cr.opb
MD5SUM	df5f31774bab40070962f7d0b16d093c
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
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	46
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.107983
Number of variables	3600
Total number of constraints	170
Number of constraints which are clauses	90
Number of constraints which are cardinality constraints (but not clauses)	80
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	40
Maximum length of a constraint	45
Trace number 4599

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        899948 kB
Buffers:         32436 kB
Cached:          67200 kB
SwapCached:       2636 kB
Active:          42360 kB
Inactive:        62724 kB
HighTotal:      131008 kB
HighFree:        60088 kB
LowTotal:       903652 kB
LowFree:        839860 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24044 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:46:10 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 3402 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 170 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................
c ---[  79]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  78]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  77]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  76]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  75]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  74]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  73]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  72]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  71]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  70]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  69]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  68]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  67]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  66]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  65]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  64]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  63]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  62]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  61]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  60]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  59]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  58]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  57]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  56]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  55]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  54]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  53]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  52]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  51]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  50]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  49]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  48]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  47]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  46]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  45]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  44]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  43]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  42]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  41]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  40]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  39]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  38]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  37]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  36]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  35]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  34]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  33]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  32]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  31]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  30]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  29]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  28]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  27]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  26]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  25]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  24]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  23]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  22]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  21]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  20]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  19]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  18]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  17]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  16]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  15]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  14]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  13]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  12]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  11]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  10]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   9]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   8]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   7]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   6]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   5]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   4]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   3]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   2]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   1]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   0]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   42250   153600 |   14083       0        0     nan |  0.000 % |
c |       100 |   42067   152995 |   15491      48       96     2.0 |  6.565 % |
c |       250 |   41337   150441 |   17040      45      130     2.9 |  7.539 % |
c |       475 |   41050   149366 |   18744     230      993     4.3 |  7.923 % |
c |       812 |   40770   148342 |   20618     540     2558     4.7 |  8.425 % |
c |      1318 |   39799   144795 |   22680     940     4228     4.5 | 10.236 % |
c |      2077 |   37745   137507 |   24948    1450     7509     5.2 | 13.907 % |
c |      3216 |   32386   119160 |   27443    1796    11095     6.2 | 23.307 % |
c |      4924 |   27786   103284 |   30188    2838    19049     6.7 | 31.486 % |
c |      7488 |   20374    78272 |   33206    4270   146413    34.3 | 44.774 % |
c |     11333 |   20030    77146 |   36527    8063  1653661   205.1 | 45.472 % |
c |     17099 |   19976    76972 |   40180   13823  4719915   341.5 | 45.591 % |
c |     25751 |   19976    76972 |   44198   22475 10894593   484.7 | 45.591 % |
c |     38726 |   19976    76972 |   48618   35450 19836348   559.6 | 45.591 % |
c |     58187 |   19976    76972 |   53480   14078  6038387   428.9 | 45.591 % |
c |     87384 |   19967    76943 |   58828   43274 32696873   755.6 | 45.610 % |
#### 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.08 0.02 0.01 2/54 29403
Raw data (stat): 29403 (runsolver) R 29402 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478457347 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0003 s]
Raw data (loadavg): 0.22 0.05 0.02 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 1272 0 1 0 983 3 0 0 25 0 1 0 478457347 7155712 1248 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1747 1248 603 41 0 1706 0
vsize: 6988
[startup+20.0011 s]
Raw data (loadavg): 0.34 0.08 0.02 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 1277 0 1 0 1982 4 0 0 25 0 1 0 478457347 7155712 1253 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1747 1253 603 41 0 1706 0
vsize: 6988
[startup+30.0018 s]
Raw data (loadavg): 0.44 0.11 0.03 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 1281 0 1 0 2982 4 0 0 25 0 1 0 478457347 7155712 1257 4294967295 134512640 134672761 3221224544 3221223712 134564725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1747 1257 603 41 0 1706 0
vsize: 6988
[startup+40.0014 s]
Raw data (loadavg): 0.53 0.14 0.04 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 1708 0 1 0 3981 5 0 0 25 0 1 0 478457347 8916992 1684 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1684 603 41 0 2136 0
vsize: 8708
[startup+50.0021 s]
Raw data (loadavg): 0.60 0.17 0.05 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 4156 0 1 0 4976 10 0 0 25 0 1 0 478457347 18894848 4132 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4613 4133 603 41 0 4572 0
vsize: 18452
[startup+60.0018 s]
Raw data (loadavg): 0.66 0.19 0.06 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 6029 0 1 0 5971 15 0 0 25 0 1 0 478457347 26660864 6005 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6509 6005 603 41 0 6468 0
vsize: 26036
[startup+70.0025 s]
Raw data (loadavg): 0.71 0.22 0.07 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 6774 0 1 0 6969 17 0 0 25 0 1 0 478457347 29601792 6750 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7227 6750 603 41 0 7186 0
vsize: 28908
[startup+80.0025 s]
Raw data (loadavg): 0.76 0.24 0.08 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 7593 0 1 0 7967 19 0 0 25 0 1 0 478457347 32944128 7569 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8043 7569 603 41 0 8002 0
vsize: 32172
[startup+90.0019 s]
Raw data (loadavg): 0.79 0.27 0.09 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 9138 0 1 0 8962 24 0 0 25 0 1 0 478457347 39337984 9114 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9604 9114 603 41 0 9563 0
vsize: 38416
[startup+100.002 s]
Raw data (loadavg): 0.82 0.29 0.10 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 10637 0 1 0 9958 29 0 0 25 0 1 0 478457347 45510656 10613 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11111 10613 603 41 0 11070 0
vsize: 44444
[startup+110.001 s]
Raw data (loadavg): 0.85 0.31 0.11 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 11955 0 1 0 10954 33 0 0 25 0 1 0 478457347 50864128 11931 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12418 11931 603 41 0 12377 0
vsize: 49672
[startup+120.001 s]
Raw data (loadavg): 0.87 0.34 0.12 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 13275 0 1 0 11950 37 0 0 25 0 1 0 478457347 56270848 13251 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13738 13251 603 41 0 13697 0
vsize: 54952
[startup+130.001 s]
Raw data (loadavg): 0.89 0.36 0.13 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 14830 0 1 0 12947 40 0 0 25 0 1 0 478457347 62701568 14806 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15308 14806 603 41 0 15267 0
vsize: 61232
[startup+140.001 s]
Raw data (loadavg): 0.91 0.38 0.14 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 16152 0 1 0 13944 44 0 0 25 0 1 0 478457347 68145152 16128 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16637 16128 603 41 0 16596 0
vsize: 66548
[startup+150.001 s]
Raw data (loadavg): 0.92 0.40 0.15 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 17334 0 1 0 14941 46 0 0 25 0 1 0 478457347 72978432 17310 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17817 17310 603 41 0 17776 0
vsize: 71268
[startup+160.001 s]
Raw data (loadavg): 0.93 0.42 0.15 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 18572 0 1 0 15938 49 0 0 25 0 1 0 478457347 78041088 18548 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19053 18548 603 41 0 19012 0
vsize: 76212
[startup+170.001 s]
Raw data (loadavg): 0.94 0.44 0.16 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 19377 0 1 0 16936 52 0 0 25 0 1 0 478457347 81276928 19353 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19843 19353 603 41 0 19802 0
vsize: 79372
[startup+180 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 20286 0 1 0 17934 54 0 0 25 0 1 0 478457347 85176320 20262 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20795 20262 603 41 0 20754 0
vsize: 83180
[startup+190 s]
Raw data (loadavg): 0.96 0.47 0.18 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 21105 0 1 0 18931 57 0 0 25 0 1 0 478457347 88522752 21081 4294967295 134512640 134672761 3221224544 3221223648 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21612 21081 603 41 0 21571 0
vsize: 86448
[startup+200 s]
Raw data (loadavg): 0.96 0.49 0.19 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 22604 0 1 0 19926 62 0 0 25 0 1 0 478457347 94732288 22580 4294967295 134512640 134672761 3221224544 3221223712 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23128 22580 603 41 0 23087 0
vsize: 92512
[startup+210 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 24444 0 1 0 20924 65 0 0 25 0 1 0 478457347 102137856 24420 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24936 24420 603 41 0 24895 0
vsize: 99744
[startup+220 s]
Raw data (loadavg): 0.97 0.52 0.20 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 26109 0 1 0 21919 69 0 0 25 0 1 0 478457347 109019136 26085 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26616 26085 603 41 0 26575 0
vsize: 106464
[startup+230 s]
Raw data (loadavg): 0.98 0.54 0.21 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 27358 0 1 0 22917 71 0 0 25 0 1 0 478457347 114135040 27334 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27865 27334 603 41 0 27824 0
vsize: 111460
[startup+240 s]
Raw data (loadavg): 0.98 0.55 0.22 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 28583 0 1 0 23915 74 0 0 25 0 1 0 478457347 119115776 28559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29081 28559 603 41 0 29040 0
vsize: 116324
[startup+250 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 29628 0 1 0 24913 76 0 0 25 0 1 0 478457347 123424768 29604 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30133 29604 603 41 0 30092 0
vsize: 120532
[startup+260 s]
Raw data (loadavg): 0.98 0.58 0.24 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 30539 0 1 0 25911 79 0 0 25 0 1 0 478457347 127201280 30515 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31055 30515 603 41 0 31014 0
vsize: 124220
[startup+270.001 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31871 0 1 0 26907 83 0 0 25 0 1 0 478457347 132599808 31847 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32373 31847 603 41 0 32332 0
vsize: 129492
[startup+280 s]
Raw data (loadavg): 0.99 0.61 0.25 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 27907 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+290 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 28907 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+300 s]
Raw data (loadavg): 0.99 0.63 0.27 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 29907 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+310 s]
Raw data (loadavg): 0.99 0.64 0.28 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 30907 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+320.001 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 31907 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+330.001 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 32907 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+340.001 s]
Raw data (loadavg): 0.99 0.67 0.30 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 33908 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+350.002 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 34908 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+360.001 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 35908 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+370.002 s]
Raw data (loadavg): 0.99 0.70 0.32 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 36908 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223648 134555093 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+380.002 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 37908 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+390.002 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 38908 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+400.002 s]
Raw data (loadavg): 0.99 0.73 0.34 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 39908 83 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+410.002 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 40908 84 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+420.002 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 41909 84 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+430.002 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 42909 84 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+440.002 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 43909 84 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+450.003 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 44909 84 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+460.002 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 45909 84 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+470.002 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 46909 84 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+480.002 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 47909 84 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+490.001 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 48909 84 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+500.002 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 31963 0 1 0 49910 84 0 0 25 0 1 0 478457347 133005312 31939 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32472 31939 603 41 0 32431 0
vsize: 129888
[startup+510.001 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 32128 0 1 0 50909 84 0 0 25 0 1 0 478457347 133685248 32104 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32638 32104 603 41 0 32597 0
vsize: 130552
[startup+520.002 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 32633 0 1 0 51909 85 0 0 25 0 1 0 478457347 135733248 32609 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33138 32609 603 41 0 33097 0
vsize: 132552
[startup+530.002 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 33186 0 1 0 52908 86 0 0 25 0 1 0 478457347 138043392 33162 4294967295 134512640 134672761 3221224544 3221223728 134558909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33702 33162 603 41 0 33661 0
vsize: 134808
[startup+540.001 s]
Raw data (loadavg): 0.99 0.83 0.42 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 33695 0 1 0 53906 88 0 0 25 0 1 0 478457347 140070912 33671 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34197 33671 603 41 0 34156 0
vsize: 136788
[startup+550.001 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 34033 0 1 0 54906 88 0 0 25 0 1 0 478457347 141541376 34009 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34556 34009 603 41 0 34515 0
vsize: 138224
[startup+560.001 s]
Raw data (loadavg): 0.99 0.84 0.43 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 34431 0 1 0 55905 89 0 0 25 0 1 0 478457347 143163392 34407 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34952 34407 603 41 0 34911 0
vsize: 139808
[startup+570.001 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 34875 0 1 0 56905 90 0 0 25 0 1 0 478457347 144924672 34851 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35382 34851 603 41 0 35341 0
vsize: 141528
[startup+580.001 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 35270 0 1 0 57904 91 0 0 25 0 1 0 478457347 146550784 35246 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35779 35246 603 41 0 35738 0
vsize: 143116
[startup+590.001 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 35520 0 1 0 58903 92 0 0 25 0 1 0 478457347 147636224 35496 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36044 35496 603 41 0 36003 0
vsize: 144176
[startup+600.001 s]
Raw data (loadavg): 0.99 0.85 0.46 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 35828 0 1 0 59902 92 0 0 25 0 1 0 478457347 148856832 35804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36342 35804 603 41 0 36301 0
vsize: 145368
[startup+610.001 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 36173 0 1 0 60902 93 0 0 25 0 1 0 478457347 150343680 36149 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36705 36149 603 41 0 36664 0
vsize: 146820
[startup+620.002 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 36503 0 1 0 61901 94 0 0 25 0 1 0 478457347 151703552 36479 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37037 36479 603 41 0 36996 0
vsize: 148148
[startup+630.002 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 36847 0 1 0 62901 95 0 0 25 0 1 0 478457347 153055232 36823 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37367 36823 603 41 0 37326 0
vsize: 149468
[startup+640.002 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 37251 0 1 0 63900 95 0 0 25 0 1 0 478457347 154669056 37227 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37761 37227 603 41 0 37720 0
vsize: 151044
[startup+650.002 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 37566 0 1 0 64899 96 0 0 25 0 1 0 478457347 156012544 37542 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38089 37542 603 41 0 38048 0
vsize: 152356
[startup+660.003 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 38150 0 1 0 65898 98 0 0 25 0 1 0 478457347 158445568 38126 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38683 38126 603 41 0 38642 0
vsize: 154732
[startup+670.003 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 38726 0 1 0 66897 99 0 0 25 0 1 0 478457347 160747520 38702 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39245 38702 603 41 0 39204 0
vsize: 156980
[startup+680.004 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 39319 0 1 0 67896 100 0 0 25 0 1 0 478457347 163176448 39295 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39838 39295 603 41 0 39797 0
vsize: 159352
[startup+690.004 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 39947 0 1 0 68895 102 0 0 25 0 1 0 478457347 165736448 39923 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40463 39923 603 41 0 40422 0
vsize: 161852
[startup+700.004 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 40561 0 1 0 69893 103 0 0 25 0 1 0 478457347 168304640 40537 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41090 40537 603 41 0 41049 0
vsize: 164360
[startup+710.003 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 40995 0 1 0 70892 104 0 0 25 0 1 0 478457347 170082304 40971 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41524 40971 603 41 0 41483 0
vsize: 166096
[startup+720.004 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 41494 0 1 0 71891 105 0 0 25 0 1 0 478457347 172118016 41470 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42021 41470 603 41 0 41980 0
vsize: 168084
[startup+730.004 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 41980 0 1 0 72890 107 0 0 25 0 1 0 478457347 174145536 41956 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42516 41956 603 41 0 42475 0
vsize: 170064
[startup+740.004 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 42604 0 1 0 73889 107 0 0 25 0 1 0 478457347 176701440 42580 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43140 42580 603 41 0 43099 0
vsize: 172560
[startup+750.004 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 43141 0 1 0 74888 109 0 0 25 0 1 0 478457347 178855936 43117 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43666 43117 603 41 0 43625 0
vsize: 174664
[startup+760.004 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 43801 0 1 0 75886 111 0 0 25 0 1 0 478457347 181563392 43777 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44327 43777 603 41 0 44286 0
vsize: 177308
[startup+770.004 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 44295 0 1 0 76885 112 0 0 25 0 1 0 478457347 183611392 44271 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44827 44271 603 41 0 44786 0
vsize: 179308
[startup+780.003 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 44672 0 1 0 77885 113 0 0 25 0 1 0 478457347 185229312 44648 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45222 44648 603 41 0 45181 0
vsize: 180888
[startup+790.003 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 45114 0 1 0 78883 114 0 0 25 0 1 0 478457347 186990592 45090 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45652 45090 603 41 0 45611 0
vsize: 182608
[startup+800.003 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 45470 0 1 0 79882 115 0 0 25 0 1 0 478457347 188489728 45446 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46018 45446 603 41 0 45977 0
vsize: 184072
[startup+810.002 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 45816 0 1 0 80882 116 0 0 25 0 1 0 478457347 189976576 45792 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46381 45792 603 41 0 46340 0
vsize: 185524
[startup+820.003 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 46121 0 1 0 81881 117 0 0 25 0 1 0 478457347 191193088 46097 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46678 46097 603 41 0 46637 0
vsize: 186712
[startup+830.004 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 46642 0 1 0 82880 119 0 0 25 0 1 0 478457347 193359872 46618 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47207 46618 603 41 0 47166 0
vsize: 188828
[startup+840.003 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 47230 0 1 0 83878 120 0 0 25 0 1 0 478457347 195809280 47206 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47805 47206 603 41 0 47764 0
vsize: 191220
[startup+850.003 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 47663 0 1 0 84877 122 0 0 25 0 1 0 478457347 197566464 47639 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48234 47639 603 41 0 48193 0
vsize: 192936
[startup+860.003 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 48190 0 1 0 85876 122 0 0 25 0 1 0 478457347 199733248 48166 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48763 48166 603 41 0 48722 0
vsize: 195052
[startup+870.004 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 48673 0 1 0 86875 124 0 0 25 0 1 0 478457347 201629696 48649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49226 48649 603 41 0 49185 0
vsize: 196904
[startup+880.003 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 49130 0 1 0 87875 124 0 0 25 0 1 0 478457347 203534336 49106 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49691 49106 603 41 0 49650 0
vsize: 198764
[startup+890.003 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 49523 0 1 0 88874 125 0 0 25 0 1 0 478457347 205172736 49499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50091 49499 603 41 0 50050 0
vsize: 200364
[startup+900.004 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 49946 0 1 0 89873 126 0 0 25 0 1 0 478457347 206938112 49922 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50522 49922 603 41 0 50481 0
vsize: 202088
[startup+910.003 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 50395 0 1 0 90872 127 0 0 25 0 1 0 478457347 208838656 50371 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50986 50371 603 41 0 50945 0
vsize: 203944
[startup+920.003 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 50909 0 1 0 91870 130 0 0 25 0 1 0 478457347 210862080 50885 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51480 50885 603 41 0 51439 0
vsize: 205920
[startup+930.004 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 51246 0 1 0 92869 131 0 0 25 0 1 0 478457347 212209664 51222 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51809 51222 603 41 0 51768 0
vsize: 207236
[startup+940.004 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 51836 0 1 0 93868 132 0 0 25 0 1 0 478457347 214638592 51812 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52402 51812 603 41 0 52361 0
vsize: 209608
[startup+950.003 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 52375 0 1 0 94867 133 0 0 25 0 1 0 478457347 216936448 52351 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52963 52351 603 41 0 52922 0
vsize: 211852
[startup+960.003 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 52971 0 1 0 95865 135 0 0 25 0 1 0 478457347 219365376 52947 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53556 52947 603 41 0 53515 0
vsize: 214224
[startup+970.004 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 53609 0 1 0 96863 137 0 0 25 0 1 0 478457347 221937664 53585 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54184 53585 603 41 0 54143 0
vsize: 216736
[startup+980.004 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 54090 0 1 0 97862 139 0 0 25 0 1 0 478457347 223846400 54066 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54650 54066 603 41 0 54609 0
vsize: 218600
[startup+990.003 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 54451 0 1 0 98861 140 0 0 25 0 1 0 478457347 225349632 54427 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55017 54427 603 41 0 54976 0
vsize: 220068
[startup+1000 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 54871 0 1 0 99860 141 0 0 25 0 1 0 478457347 227106816 54847 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55446 54847 603 41 0 55405 0
vsize: 221784
[startup+1010 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 55352 0 1 0 100858 143 0 0 25 0 1 0 478457347 229003264 55328 4294967295 134512640 134672761 3221224544 3221223712 134559063 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55909 55328 603 41 0 55868 0
vsize: 223636
[startup+1020 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 55832 0 1 0 101857 145 0 0 25 0 1 0 478457347 231030784 55808 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56404 55809 603 41 0 56363 0
vsize: 225616
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 56556 0 1 0 102855 147 0 0 25 0 1 0 478457347 234045440 56532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57140 56532 603 41 0 57099 0
vsize: 228560
[startup+1040 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57040 0 1 0 103854 148 0 0 25 0 1 0 478457347 235933696 57016 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57601 57016 603 41 0 57560 0
vsize: 230404
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57514 0 1 0 104852 150 0 0 25 0 1 0 478457347 237957120 57490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58095 57490 603 41 0 58054 0
vsize: 232380
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57801 0 1 0 105851 151 0 0 25 0 1 0 478457347 239439872 57777 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57777 603 41 0 58416 0
vsize: 233828
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57801 0 1 0 106851 151 0 0 25 0 1 0 478457347 239439872 57777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57777 603 41 0 58416 0
vsize: 233828
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57801 0 1 0 107851 151 0 0 25 0 1 0 478457347 239439872 57777 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57777 603 41 0 58416 0
vsize: 233828
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57801 0 1 0 108851 152 0 0 25 0 1 0 478457347 239439872 57777 4294967295 134512640 134672761 3221224544 3221223728 134559540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57777 603 41 0 58416 0
vsize: 233828
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57802 0 1 0 109851 152 0 0 25 0 1 0 478457347 239439872 57778 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57778 603 41 0 58416 0
vsize: 233828
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57802 0 1 0 110852 152 0 0 25 0 1 0 478457347 239439872 57778 4294967295 134512640 134672761 3221224544 3221223728 134559379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57778 603 41 0 58416 0
vsize: 233828
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57802 0 1 0 111852 152 0 0 25 0 1 0 478457347 239439872 57778 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57778 603 41 0 58416 0
vsize: 233828
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57802 0 1 0 112852 152 0 0 25 0 1 0 478457347 239439872 57778 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57778 603 41 0 58416 0
vsize: 233828
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57802 0 1 0 113852 152 0 0 25 0 1 0 478457347 239439872 57778 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57778 603 41 0 58416 0
vsize: 233828
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57802 0 1 0 114852 152 0 0 25 0 1 0 478457347 239439872 57778 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57778 603 41 0 58416 0
vsize: 233828
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57803 0 1 0 115852 152 0 0 25 0 1 0 478457347 239439872 57779 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57779 603 41 0 58416 0
vsize: 233828
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57803 0 1 0 116852 152 0 0 25 0 1 0 478457347 239439872 57779 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57779 603 41 0 58416 0
vsize: 233828
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57803 0 1 0 117852 152 0 0 25 0 1 0 478457347 239439872 57779 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57779 603 41 0 58416 0
vsize: 233828
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57803 0 1 0 118853 152 0 0 25 0 1 0 478457347 239439872 57779 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57779 603 41 0 58416 0
vsize: 233828
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 29403
Raw data (stat): 29403 (minisat+) R 29402 27565 27564 0 -1 0 57803 0 1 0 119853 153 0 0 25 0 1 0 478457347 239439872 57779 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58457 57779 603 41 0 58416 0
vsize: 233828
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 29403
Raw data (stat): 29403 (minisat+) Z 29402 27565 27564 0 -1 12 57805 0 1 0 119853 163 0 0 25 0 1 0 478457347 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.12
CPU time (s): 1200.17
CPU user time (s): 1198.53
CPU system time (s): 1.63875
CPU usage (%): 100.004
Max. virtual memory (Kb): 233828
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####