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-fpga40_40_sat_pb.cnf.cr.opb
MD5SUM	f9a3a990ebca4aa5457d0675d3f1fe27
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	41
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.9477
Number of variables	2400
Total number of constraints	1720
Number of constraints which are clauses	1640
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	20
Maximum length of a constraint	40
Trace number 4648

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-13 19:28:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3438 boxname=wulflinc29 idbench=54 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f9a3a990ebca4aa5457d0675d3f1fe27  /oldhome/oroussel/tmp/wulflinc29/normalized-fpga40_40_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc29/normalized-fpga40_40_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc29/normalized-fpga40_40_sat_pb.cnf.cr.opb
IDLAUNCH: 3438
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        862136 kB
Buffers:         35504 kB
Cached:          99804 kB
SwapCached:         12 kB
Active:          52228 kB
Inactive:        85936 kB
HighTotal:      131008 kB
HighFree:        27748 kB
LowTotal:       903652 kB
LowFree:        834388 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            28972 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:48:13 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 3438 7 1200.29 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1720 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  79]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  78]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  77]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  76]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  75]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  74]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  73]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  72]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  71]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  70]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  69]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  68]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  67]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  66]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  65]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  64]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  63]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  62]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  61]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  60]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  59]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  58]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  57]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  56]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  55]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  54]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  53]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  52]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  51]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  50]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  49]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  48]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  47]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  46]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  45]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  44]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  43]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  42]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  41]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  40]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  39]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  38]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  37]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  36]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  35]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  34]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  33]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  32]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  31]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  30]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  29]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  28]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  27]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  26]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  25]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  24]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  23]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  22]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  21]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  20]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  19]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  18]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  17]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  16]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  15]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  14]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  13]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  12]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  11]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  10]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   9]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   8]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   7]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   6]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   5]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   4]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   3]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   2]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   1]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   0]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   29720   134960 |    9906       0        0     nan |  0.000 % |
c |       100 |   29720   134960 |   10896      99      212     2.1 |  7.373 % |
c |       251 |   29441   133985 |   11986     201      466     2.3 |  7.881 % |
c |       476 |   28980   132395 |   13184     336     1151     3.4 |  8.785 % |
c |       813 |   28638   131221 |   14503     606     3288     5.4 |  9.477 % |
c |      1320 |   28472   130654 |   15953    1083     5888     5.4 |  9.859 % |
c |      2079 |   27861   128586 |   17549    1745     9217     5.3 | 11.370 % |
c |      3218 |   26689   124627 |   19303    2643    13671     5.2 | 14.153 % |
c |      4926 |   23989   115348 |   21234    3848    20104     5.2 | 20.381 % |
c |      7489 |   18728    97346 |   23357    5445   336476    61.8 | 32.839 % |
c |     11333 |   18214    95592 |   25693    9159  1179555   128.8 | 34.068 % |
c |     17099 |   17328    92588 |   28262   14741  3028740   205.5 | 36.285 % |
c |     25748 |   17231    92265 |   31089   23370  8029621   343.6 | 36.554 % |
c |     38724 |   17164    92040 |   34198   36330 13445152   370.1 | 36.737 % |
c |     58185 |   17137    91951 |   37618   29100 11056798   380.0 | 36.808 % |
c |     87378 |   16752    90646 |   41379   29340 23522573   801.7 | 37.768 % |
c |    131171 |   16699    90469 |   45517   41040 36693086   894.1 | 37.924 % |
#### 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.64 0.20 0.07 2/54 29135
Raw data (stat): 29135 (runsolver) R 29134 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478467791 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0007 s]
Raw data (loadavg): 0.69 0.23 0.08 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 1048 0 0 0 995 3 0 0 25 0 1 0 478467791 5783552 1026 4294967295 134512640 134672761 3221224528 3221223652 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1412 1026 603 41 0 1371 0
vsize: 5648
[startup+20.0009 s]
Raw data (loadavg): 0.74 0.25 0.09 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 1057 0 0 0 1994 3 0 0 25 0 1 0 478467791 5918720 1035 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1445 1035 603 41 0 1404 0
vsize: 5780
[startup+30.0012 s]
Raw data (loadavg): 0.78 0.28 0.10 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 2099 0 0 0 2993 5 0 0 25 0 1 0 478467791 10231808 2077 4294967295 134512640 134672761 3221224528 3221223712 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2498 2077 603 41 0 2457 0
vsize: 9992
[startup+40.0017 s]
Raw data (loadavg): 0.81 0.30 0.11 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 3736 0 0 0 3989 8 0 0 25 0 1 0 478467791 16846848 3714 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4113 3714 603 41 0 4072 0
vsize: 16452
[startup+50.0022 s]
Raw data (loadavg): 0.84 0.32 0.11 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 5229 0 0 0 4986 12 0 0 25 0 1 0 478467791 23015424 5207 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5619 5207 603 41 0 5578 0
vsize: 22476
[startup+60.0025 s]
Raw data (loadavg): 0.86 0.34 0.12 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 6470 0 0 0 5983 15 0 0 25 0 1 0 478467791 28151808 6448 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6873 6448 603 41 0 6832 0
vsize: 27492
[startup+70.003 s]
Raw data (loadavg): 0.88 0.37 0.13 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 7474 0 0 0 6981 18 0 0 25 0 1 0 478467791 32210944 7452 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7864 7452 603 41 0 7823 0
vsize: 31456
[startup+80.0035 s]
Raw data (loadavg): 0.90 0.39 0.14 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 8398 0 0 0 7978 20 0 0 25 0 1 0 478467791 35995648 8376 4294967295 134512640 134672761 3221224528 3221223632 134560483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8788 8377 603 41 0 8747 0
vsize: 35152
[startup+90.0036 s]
Raw data (loadavg): 0.92 0.41 0.15 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 9856 0 0 0 8973 25 0 0 25 0 1 0 478467791 42041344 9834 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10264 9834 603 41 0 10223 0
vsize: 41056
[startup+100.003 s]
Raw data (loadavg): 0.93 0.42 0.16 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 11303 0 0 0 9969 30 0 0 25 0 1 0 478467791 47841280 11281 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11680 11281 603 41 0 11639 0
vsize: 46720
[startup+110.003 s]
Raw data (loadavg): 0.94 0.44 0.17 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 13164 0 0 0 10965 34 0 0 25 0 1 0 478467791 55508992 13142 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13552 13142 603 41 0 13511 0
vsize: 54208
[startup+120.004 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 14537 0 0 0 11962 37 0 0 25 0 1 0 478467791 61300736 14515 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14966 14515 603 41 0 14925 0
vsize: 59864
[startup+130.004 s]
Raw data (loadavg): 0.96 0.48 0.18 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 15255 0 0 0 12959 40 0 0 25 0 1 0 478467791 64270336 15233 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15691 15233 603 41 0 15650 0
vsize: 62764
[startup+140.004 s]
Raw data (loadavg): 0.96 0.50 0.19 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 16166 0 0 0 13956 43 0 0 25 0 1 0 478467791 67911680 16144 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16580 16144 603 41 0 16539 0
vsize: 66320
[startup+150.005 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 16935 0 0 0 14954 45 0 0 25 0 1 0 478467791 71155712 16913 4294967295 134512640 134672761 3221224528 3221223712 134559033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17372 16913 603 41 0 17331 0
vsize: 69488
[startup+160.005 s]
Raw data (loadavg): 0.97 0.53 0.21 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 16936 0 0 0 15954 45 0 0 25 0 1 0 478467791 71155712 16914 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17372 16914 603 41 0 17331 0
vsize: 69488
[startup+170.005 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 16936 0 0 0 16954 45 0 0 25 0 1 0 478467791 71155712 16914 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17372 16914 603 41 0 17331 0
vsize: 69488
[startup+180.005 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 16936 0 0 0 17955 45 0 0 25 0 1 0 478467791 71155712 16914 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17372 16914 603 41 0 17331 0
vsize: 69488
[startup+190.006 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 16936 0 0 0 18955 45 0 0 25 0 1 0 478467791 71155712 16914 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17372 16914 603 41 0 17331 0
vsize: 69488
[startup+200.006 s]
Raw data (loadavg): 0.98 0.58 0.24 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 16936 0 0 0 19955 45 0 0 25 0 1 0 478467791 71155712 16914 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17372 16914 603 41 0 17331 0
vsize: 69488
[startup+210.005 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 16936 0 0 0 20955 45 0 0 25 0 1 0 478467791 71155712 16914 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17372 16914 603 41 0 17331 0
vsize: 69488
[startup+220.007 s]
Raw data (loadavg): 0.99 0.61 0.25 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 16936 0 0 0 21955 45 0 0 25 0 1 0 478467791 71155712 16914 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17372 16914 603 41 0 17331 0
vsize: 69488
[startup+230.006 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 16936 0 0 0 22956 45 0 0 25 0 1 0 478467791 71155712 16914 4294967295 134512640 134672761 3221224528 3221223632 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17372 16914 603 41 0 17331 0
vsize: 69488
[startup+240.007 s]
Raw data (loadavg): 0.99 0.63 0.27 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 16936 0 0 0 23956 45 0 0 25 0 1 0 478467791 71155712 16914 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17372 16914 603 41 0 17331 0
vsize: 69488
[startup+250.007 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 17269 0 0 0 24955 46 0 0 25 0 1 0 478467791 72503296 17247 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17701 17247 603 41 0 17660 0
vsize: 70804
[startup+260.007 s]
Raw data (loadavg): 0.99 0.66 0.28 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 19491 0 0 0 25951 50 0 0 25 0 1 0 478467791 81559552 19469 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19912 19469 603 41 0 19871 0
vsize: 79648
[startup+270.007 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 21899 0 0 0 26943 58 0 0 25 0 1 0 478467791 91402240 21877 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22315 21877 603 41 0 22274 0
vsize: 89260
[startup+280.007 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 22881 0 0 0 27941 60 0 0 25 0 1 0 478467791 95465472 22859 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23307 22859 603 41 0 23266 0
vsize: 93228
[startup+290.008 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 22881 0 0 0 28941 60 0 0 25 0 1 0 478467791 95465472 22859 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23307 22859 603 41 0 23266 0
vsize: 93228
[startup+300.008 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 22881 0 0 0 29942 60 0 0 25 0 1 0 478467791 95465472 22859 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23307 22859 603 41 0 23266 0
vsize: 93228
[startup+310.008 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 22881 0 0 0 30942 60 0 0 25 0 1 0 478467791 95465472 22859 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23307 22859 603 41 0 23266 0
vsize: 93228
[startup+320.008 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 22881 0 0 0 31942 60 0 0 25 0 1 0 478467791 95465472 22859 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23307 22859 603 41 0 23266 0
vsize: 93228
[startup+330.009 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 22881 0 0 0 32942 60 0 0 25 0 1 0 478467791 95465472 22859 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23307 22859 603 41 0 23266 0
vsize: 93228
[startup+340.01 s]
Raw data (loadavg): 0.99 0.73 0.34 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 22881 0 0 0 33942 60 0 0 25 0 1 0 478467791 95465472 22859 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23307 22859 603 41 0 23266 0
vsize: 93228
[startup+350.01 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 22881 0 0 0 34943 60 0 0 25 0 1 0 478467791 95465472 22859 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23307 22859 603 41 0 23266 0
vsize: 93228
[startup+360.009 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 22881 0 0 0 35943 60 0 0 25 0 1 0 478467791 95465472 22859 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23307 22859 603 41 0 23266 0
vsize: 93228
[startup+370.01 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 22881 0 0 0 36943 60 0 0 25 0 1 0 478467791 95465472 22859 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23307 22859 603 41 0 23266 0
vsize: 93228
[startup+380.01 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 22881 0 0 0 37943 60 0 0 25 0 1 0 478467791 95465472 22859 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23307 22859 603 41 0 23266 0
vsize: 93228
[startup+390.01 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 23472 0 0 0 38942 62 0 0 25 0 1 0 478467791 97882112 23450 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23897 23450 603 41 0 23856 0
vsize: 95588
[startup+400.01 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 24835 0 0 0 39939 65 0 0 25 0 1 0 478467791 103391232 24813 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25242 24813 603 41 0 25201 0
vsize: 100968
[startup+410.01 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 25585 0 0 0 40938 66 0 0 25 0 1 0 478467791 106504192 25563 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26002 25563 603 41 0 25961 0
vsize: 104008
[startup+420.011 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 26302 0 0 0 41936 68 0 0 25 0 1 0 478467791 109473792 26280 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26727 26280 603 41 0 26686 0
vsize: 106908
[startup+430.012 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 26888 0 0 0 42935 69 0 0 25 0 1 0 478467791 111939584 26866 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27329 26866 603 41 0 27288 0
vsize: 109316
[startup+440.012 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 27844 0 0 0 43932 72 0 0 25 0 1 0 478467791 115867648 27822 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28288 27822 603 41 0 28247 0
vsize: 113152
[startup+450.012 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 29842 0 0 0 44928 77 0 0 25 0 1 0 478467791 124104704 29820 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30299 29820 603 41 0 30258 0
vsize: 121196
[startup+460.012 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 31524 0 0 0 45924 80 0 0 25 0 1 0 478467791 130985984 31502 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31979 31502 603 41 0 31938 0
vsize: 127916
[startup+470.013 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 33488 0 0 0 46919 86 0 0 25 0 1 0 478467791 138952704 33466 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33924 33466 603 41 0 33883 0
vsize: 135696
[startup+480.012 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 35274 0 0 0 47915 90 0 0 25 0 1 0 478467791 146386944 35252 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35739 35252 603 41 0 35698 0
vsize: 142956
[startup+490.013 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 36961 0 0 0 48910 95 0 0 25 0 1 0 478467791 153288704 36939 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37424 36939 603 41 0 37383 0
vsize: 149696
[startup+500.013 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 38444 0 0 0 49908 98 0 0 25 0 1 0 478467791 159399936 38422 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38916 38422 603 41 0 38875 0
vsize: 155664
[startup+510.013 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 39902 0 0 0 50904 101 0 0 25 0 1 0 478467791 165347328 39880 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40368 39880 603 41 0 40327 0
vsize: 161472
[startup+520.013 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 51902 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+530.014 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 52902 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+540.014 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 53902 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+550.014 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 54902 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+560.014 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 55902 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+570.014 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 56903 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223712 134559592 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+580.014 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 57903 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+590.015 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 58903 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+600.016 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 59903 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+610.015 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 60903 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+620.016 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 61904 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+630.017 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 62904 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+640.018 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 63904 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+650.018 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 64904 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+660.017 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 65904 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+670.018 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 66905 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+680.018 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41022 0 0 0 67905 104 0 0 25 0 1 0 478467791 169934848 41000 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41000 603 41 0 41447 0
vsize: 165952
[startup+690.018 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41023 0 0 0 68905 104 0 0 25 0 1 0 478467791 169934848 41001 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41001 603 41 0 41447 0
vsize: 165952
[startup+700.019 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41023 0 0 0 69905 104 0 0 25 0 1 0 478467791 169934848 41001 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41001 603 41 0 41447 0
vsize: 165952
[startup+710.019 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41023 0 0 0 70905 104 0 0 25 0 1 0 478467791 169934848 41001 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41001 603 41 0 41447 0
vsize: 165952
[startup+720.02 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41023 0 0 0 71906 104 0 0 25 0 1 0 478467791 169934848 41001 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41488 41001 603 41 0 41447 0
vsize: 165952
[startup+730.02 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41023 0 0 0 72906 104 0 0 25 0 1 0 478467791 169934848 41001 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41488 41001 603 41 0 41447 0
vsize: 165952
[startup+740.021 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 41248 0 0 0 73905 104 0 0 25 0 1 0 478467791 170741760 41226 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41685 41226 603 41 0 41644 0
vsize: 166740
[startup+750.02 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 42127 0 0 0 74904 106 0 0 25 0 1 0 478467791 174403584 42105 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42579 42105 603 41 0 42538 0
vsize: 170316
[startup+760.02 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 42414 0 0 0 75903 107 0 0 25 0 1 0 478467791 175644672 42392 4294967295 134512640 134672761 3221224528 3221223700 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42882 42392 603 41 0 42841 0
vsize: 171528
[startup+770.021 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 43241 0 0 0 76901 109 0 0 25 0 1 0 478467791 179007488 43219 4294967295 134512640 134672761 3221224528 3221223712 134559522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43703 43219 603 41 0 43662 0
vsize: 174812
[startup+780.021 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 45242 0 0 0 77895 115 0 0 25 0 1 0 478467791 187285504 45220 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45724 45220 603 41 0 45683 0
vsize: 182896
[startup+790.021 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46651 0 0 0 78892 118 0 0 25 0 1 0 478467791 192974848 46629 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46629 603 41 0 47072 0
vsize: 188452
[startup+800.021 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46651 0 0 0 79892 118 0 0 25 0 1 0 478467791 192974848 46629 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46629 603 41 0 47072 0
vsize: 188452
[startup+810.021 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46651 0 0 0 80893 118 0 0 25 0 1 0 478467791 192974848 46629 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46629 603 41 0 47072 0
vsize: 188452
[startup+820.021 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46651 0 0 0 81893 118 0 0 25 0 1 0 478467791 192974848 46629 4294967295 134512640 134672761 3221224528 3221223712 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46629 603 41 0 47072 0
vsize: 188452
[startup+830.021 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46651 0 0 0 82893 118 0 0 25 0 1 0 478467791 192974848 46629 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46629 603 41 0 47072 0
vsize: 188452
[startup+840.022 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46651 0 0 0 83893 118 0 0 25 0 1 0 478467791 192974848 46629 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46629 603 41 0 47072 0
vsize: 188452
[startup+850.023 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46651 0 0 0 84893 118 0 0 25 0 1 0 478467791 192974848 46629 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46629 603 41 0 47072 0
vsize: 188452
[startup+860.023 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46651 0 0 0 85894 118 0 0 25 0 1 0 478467791 192974848 46629 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46629 603 41 0 47072 0
vsize: 188452
[startup+870.024 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46651 0 0 0 86894 118 0 0 25 0 1 0 478467791 192974848 46629 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46629 603 41 0 47072 0
vsize: 188452
[startup+880.024 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46651 0 0 0 87894 118 0 0 25 0 1 0 478467791 192974848 46629 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46629 603 41 0 47072 0
vsize: 188452
[startup+890.025 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46651 0 0 0 88894 118 0 0 25 0 1 0 478467791 192974848 46629 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46629 603 41 0 47072 0
vsize: 188452
[startup+900.025 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 89894 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+910.025 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 90895 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+920.025 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 91895 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+930.026 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 92895 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+940.027 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 93895 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+950.028 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 94896 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+960.028 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 95896 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+970.028 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 96896 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+980.028 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 97896 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+990.029 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 98896 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 99897 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 100897 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 101897 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 102897 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 103897 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 104898 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 105898 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 106898 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 107898 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 108898 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 109898 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 110899 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 111899 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 112899 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 113900 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 114901 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46652 0 0 0 115901 118 0 0 25 0 1 0 478467791 192974848 46630 4294967295 134512640 134672761 3221224528 3221223528 1075349917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46630 603 41 0 47072 0
vsize: 188452
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46654 0 0 0 116901 118 0 0 25 0 1 0 478467791 192974848 46632 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46632 603 41 0 47072 0
vsize: 188452
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46654 0 0 0 117901 118 0 0 25 0 1 0 478467791 192974848 46632 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46632 603 41 0 47072 0
vsize: 188452
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.71 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46654 0 0 0 118901 118 0 0 25 0 1 0 478467791 192974848 46632 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46632 603 41 0 47072 0
vsize: 188452
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.71 2/54 29135
Raw data (stat): 29135 (minisat+) R 29134 27222 27221 0 -1 0 46654 0 0 0 119901 118 0 0 25 0 1 0 478467791 192974848 46632 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47113 46632 603 41 0 47072 0
vsize: 188452
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.71 1/54 29135
Raw data (stat): 29135 (minisat+) Z 29134 27222 27221 0 -1 12 46656 0 0 0 119902 127 0 0 25 0 1 0 478467791 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.13
CPU time (s): 1200.29
CPU user time (s): 1199.02
CPU system time (s): 1.27281
CPU usage (%): 100.013
Max. virtual memory (Kb): 188452
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####