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-chnl30_35_pb.cnf.cr.opb
MD5SUM	b1c5adb5438ceaf1c654cfedb79b695e
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	36
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.06099
Number of variables	2100
Total number of constraints	130
Number of constraints which are clauses	70
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	30
Maximum length of a constraint	35
Trace number 4582

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        872052 kB
Buffers:         30472 kB
Cached:          89500 kB
SwapCached:        524 kB
Active:          37548 kB
Inactive:        85772 kB
HighTotal:      131008 kB
HighFree:        37828 kB
LowTotal:       903652 kB
LowFree:        834224 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:               0 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            33832 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:44:31 (client local time) WITH STATUS 0 IN 1200.09 SECONDS
stats: 3396 7 1200.09 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 130 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................
c ---[  59]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  58]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  57]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  56]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  55]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  54]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  53]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  52]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  51]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  50]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  49]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  48]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  47]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  46]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  45]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  44]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  43]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  42]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  41]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  40]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  39]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  38]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  37]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  36]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  35]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  34]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  33]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  32]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  31]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  30]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  29]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  28]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  27]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  26]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  25]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  24]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  23]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  22]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  21]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  20]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  19]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  18]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  17]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  16]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  15]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  14]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  13]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  12]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  11]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[  10]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[   9]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[   8]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[   7]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[   6]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[   5]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[   4]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[   3]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[   2]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[   1]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[   0]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   22810    82800 |    7603       0        0     nan |  0.000 % |
c |       100 |   22780    82702 |    8363      96      556     5.8 | 12.205 % |
c |       252 |   22713    82483 |    9199     238     1231     5.2 | 12.391 % |
c |       477 |   22533    81875 |   10119     437     2165     5.0 | 12.879 % |
c |       817 |   22299    81101 |   11131     738     3453     4.7 | 13.586 % |
c |      1323 |   21532    78424 |   12244    1128     6214     5.5 | 15.640 % |
c |      2082 |   18706    68664 |   13469    1460     8272     5.7 | 23.838 % |
c |      3221 |   13126    49566 |   14816    1734    12026     6.9 | 40.606 % |
c |      4931 |   11148    43094 |   16297    3147   218533    69.4 | 47.323 % |
c |      7494 |   11089    42903 |   17927    5701  1412060   247.7 | 47.525 % |
c |     11339 |   11089    42903 |   19720    9546  3417051   358.0 | 47.525 % |
c |     17106 |   11073    42851 |   21692   15310  6179762   403.6 | 47.576 % |
c |     25757 |   11073    42851 |   23861   23961 10181045   424.9 | 47.576 % |
c |     38734 |   11073    42851 |   26247   21753  9721861   446.9 | 47.576 % |
c |     58196 |   11073    42851 |   28872   23698 11657154   491.9 | 47.576 % |
c |     87388 |   11073    42851 |   31759   16220  7928247   488.8 | 47.576 % |
c |    131178 |   11073    42851 |   34935   19782 10020233   506.5 | 47.576 % |
#### 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.00 0.00 0.00 2/54 27731
Raw data (stat): 27731 (runsolver) R 27730 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478446402 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.15 0.03 0.01 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 854 0 1 0 985 2 0 0 25 0 1 0 478446402 5169152 833 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1262 833 603 41 0 1221 0
vsize: 5048
[startup+20.0004 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 3147 0 1 0 1980 7 0 0 25 0 1 0 478446402 14618624 3126 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3569 3126 603 41 0 3528 0
vsize: 14276
[startup+30.0016 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 5078 0 1 0 2975 12 0 0 25 0 1 0 478446402 22564864 5057 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5509 5057 603 41 0 5468 0
vsize: 22036
[startup+40.0017 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 7147 0 1 0 3970 16 0 0 25 0 1 0 478446402 30945280 7126 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 7126 603 41 0 7514 0
vsize: 30220
[startup+50.0015 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 8139 0 1 0 4968 19 0 0 25 0 1 0 478446402 35041280 8118 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8555 8118 603 41 0 8514 0
vsize: 34220
[startup+60.0014 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 9076 0 1 0 5966 21 0 0 25 0 1 0 478446402 38961152 9055 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9512 9055 603 41 0 9471 0
vsize: 38048
[startup+70.0008 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 10249 0 1 0 6964 23 0 0 25 0 1 0 478446402 43679744 10228 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10664 10228 603 41 0 10623 0
vsize: 42656
[startup+80.0016 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 11301 0 1 0 7962 25 0 0 25 0 1 0 478446402 47988736 11280 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11716 11280 603 41 0 11675 0
vsize: 46864
[startup+90.0015 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 12376 0 1 0 8959 28 0 0 25 0 1 0 478446402 52428800 12355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12800 12355 603 41 0 12759 0
vsize: 51200
[startup+100.001 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 13151 0 1 0 9958 29 0 0 25 0 1 0 478446402 55681024 13130 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13594 13130 603 41 0 13553 0
vsize: 54376
[startup+110.002 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 13151 0 1 0 10958 29 0 0 25 0 1 0 478446402 55681024 13130 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13594 13130 603 41 0 13553 0
vsize: 54376
[startup+120.002 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 13152 0 1 0 11958 29 0 0 25 0 1 0 478446402 55681024 13131 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13594 13131 603 41 0 13553 0
vsize: 54376
[startup+130.002 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 13152 0 1 0 12959 29 0 0 25 0 1 0 478446402 55681024 13131 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13594 13131 603 41 0 13553 0
vsize: 54376
[startup+140.002 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 14118 0 1 0 13957 31 0 0 25 0 1 0 478446402 59600896 14097 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14551 14097 603 41 0 14510 0
vsize: 58204
[startup+150.002 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 15326 0 1 0 14955 34 0 0 25 0 1 0 478446402 64593920 15305 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15770 15305 603 41 0 15729 0
vsize: 63080
[startup+160.001 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 15326 0 1 0 15955 34 0 0 25 0 1 0 478446402 64593920 15305 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15770 15305 603 41 0 15729 0
vsize: 63080
[startup+170.001 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 15326 0 1 0 16955 34 0 0 25 0 1 0 478446402 64593920 15305 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15770 15305 603 41 0 15729 0
vsize: 63080
[startup+180.001 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 15327 0 1 0 17955 34 0 0 25 0 1 0 478446402 64593920 15306 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15770 15306 603 41 0 15729 0
vsize: 63080
[startup+190.001 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 15328 0 1 0 18955 34 0 0 25 0 1 0 478446402 64593920 15307 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15770 15307 603 41 0 15729 0
vsize: 63080
[startup+200.001 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 15328 0 1 0 19955 34 0 0 25 0 1 0 478446402 64593920 15307 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15770 15307 603 41 0 15729 0
vsize: 63080
[startup+210.001 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 15328 0 1 0 20954 34 0 0 25 0 1 0 478446402 64593920 15307 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15770 15307 603 41 0 15729 0
vsize: 63080
[startup+220 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 15328 0 1 0 21954 34 0 0 25 0 1 0 478446402 64593920 15307 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15770 15307 603 41 0 15729 0
vsize: 63080
[startup+230.001 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 15328 0 1 0 22955 34 0 0 25 0 1 0 478446402 64593920 15307 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15770 15307 603 41 0 15729 0
vsize: 63080
[startup+240.001 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 15806 0 1 0 23954 35 0 0 25 0 1 0 478446402 66506752 15785 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16237 15785 603 41 0 16196 0
vsize: 64948
[startup+250 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 16361 0 1 0 24953 36 0 0 25 0 1 0 478446402 68829184 16340 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16804 16340 603 41 0 16763 0
vsize: 67216
[startup+260.001 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 16718 0 1 0 25952 37 0 0 25 0 1 0 478446402 70316032 16697 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17167 16697 603 41 0 17126 0
vsize: 68668
[startup+270.001 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17127 0 1 0 26952 38 0 0 25 0 1 0 478446402 72073216 17106 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17596 17106 603 41 0 17555 0
vsize: 70384
[startup+280.001 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17634 0 1 0 27950 39 0 0 25 0 1 0 478446402 74100736 17613 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18091 17613 603 41 0 18050 0
vsize: 72364
[startup+290.001 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17986 0 1 0 28949 40 0 0 25 0 1 0 478446402 75718656 17965 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17965 603 41 0 18445 0
vsize: 73944
[startup+300.001 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17987 0 1 0 29950 40 0 0 25 0 1 0 478446402 75718656 17966 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17966 603 41 0 18445 0
vsize: 73944
[startup+310.002 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17987 0 1 0 30950 40 0 0 25 0 1 0 478446402 75718656 17966 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17966 603 41 0 18445 0
vsize: 73944
[startup+320.001 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17987 0 1 0 31950 40 0 0 25 0 1 0 478446402 75718656 17966 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17966 603 41 0 18445 0
vsize: 73944
[startup+330.001 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17987 0 1 0 32950 40 0 0 25 0 1 0 478446402 75718656 17966 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17966 603 41 0 18445 0
vsize: 73944
[startup+340.001 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17987 0 1 0 33950 40 0 0 25 0 1 0 478446402 75718656 17966 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17966 603 41 0 18445 0
vsize: 73944
[startup+350 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17987 0 1 0 34950 40 0 0 25 0 1 0 478446402 75718656 17966 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17966 603 41 0 18445 0
vsize: 73944
[startup+360.002 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17988 0 1 0 35951 40 0 0 25 0 1 0 478446402 75718656 17967 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17967 603 41 0 18445 0
vsize: 73944
[startup+370.001 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17989 0 1 0 36951 40 0 0 25 0 1 0 478446402 75718656 17968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17968 603 41 0 18445 0
vsize: 73944
[startup+380 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17989 0 1 0 37951 40 0 0 25 0 1 0 478446402 75718656 17968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17968 603 41 0 18445 0
vsize: 73944
[startup+390 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17989 0 1 0 38951 40 0 0 25 0 1 0 478446402 75718656 17968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17968 603 41 0 18445 0
vsize: 73944
[startup+400 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 17989 0 1 0 39951 40 0 0 25 0 1 0 478446402 75718656 17968 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18486 17968 603 41 0 18445 0
vsize: 73944
[startup+410 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 40951 41 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223728 134558667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+420 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 41950 41 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+430 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 42950 41 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+440 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 43949 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+449.999 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 44949 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+460 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 45949 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+470 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 46950 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+480 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 47950 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+489.999 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 48950 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+499.999 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 49950 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+509.998 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 50950 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+519.998 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 51950 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+529.999 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 52951 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+539.999 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 53951 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+549.999 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 54951 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+559.999 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 55951 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+569.999 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 56951 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+579.999 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18452 0 1 0 57951 42 0 0 25 0 1 0 478446402 77611008 18431 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18948 18431 603 41 0 18907 0
vsize: 75792
[startup+589.998 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 18515 0 1 0 58951 42 0 0 25 0 1 0 478446402 77881344 18494 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19014 18494 603 41 0 18973 0
vsize: 76056
[startup+599.998 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 19103 0 1 0 59950 43 0 0 25 0 1 0 478446402 80314368 19082 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19608 19082 603 41 0 19567 0
vsize: 78432
[startup+609.999 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 19592 0 1 0 60950 44 0 0 25 0 1 0 478446402 82341888 19571 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20103 19571 603 41 0 20062 0
vsize: 80412
[startup+619.998 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 19976 0 1 0 61949 45 0 0 25 0 1 0 478446402 83828736 19955 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20466 19955 603 41 0 20425 0
vsize: 81864
[startup+629.999 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20445 0 1 0 62948 46 0 0 25 0 1 0 478446402 85741568 20424 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20933 20424 603 41 0 20892 0
vsize: 83732
[startup+639.999 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20806 0 1 0 63947 47 0 0 25 0 1 0 478446402 87228416 20785 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21296 20785 603 41 0 21255 0
vsize: 85184
[startup+649.998 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20985 0 1 0 64947 47 0 0 25 0 1 0 478446402 88039424 20964 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20964 603 41 0 21453 0
vsize: 85976
[startup+659.998 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20985 0 1 0 65947 47 0 0 25 0 1 0 478446402 88039424 20964 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20964 603 41 0 21453 0
vsize: 85976
[startup+669.999 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20985 0 1 0 66947 47 0 0 25 0 1 0 478446402 88039424 20964 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20964 603 41 0 21453 0
vsize: 85976
[startup+679.999 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20985 0 1 0 67948 47 0 0 25 0 1 0 478446402 88039424 20964 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20964 603 41 0 21453 0
vsize: 85976
[startup+689.999 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20985 0 1 0 68948 47 0 0 25 0 1 0 478446402 88039424 20964 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20964 603 41 0 21453 0
vsize: 85976
[startup+699.999 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20985 0 1 0 69948 47 0 0 25 0 1 0 478446402 88039424 20964 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20964 603 41 0 21453 0
vsize: 85976
[startup+709.999 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20988 0 1 0 70948 47 0 0 25 0 1 0 478446402 88039424 20967 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20967 603 41 0 21453 0
vsize: 85976
[startup+719.999 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20988 0 1 0 71948 47 0 0 25 0 1 0 478446402 88039424 20967 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20967 603 41 0 21453 0
vsize: 85976
[startup+730 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20988 0 1 0 72949 47 0 0 25 0 1 0 478446402 88039424 20967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20967 603 41 0 21453 0
vsize: 85976
[startup+740 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20988 0 1 0 73949 47 0 0 25 0 1 0 478446402 88039424 20967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20967 603 41 0 21453 0
vsize: 85976
[startup+749.999 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20989 0 1 0 74949 47 0 0 25 0 1 0 478446402 88039424 20968 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20968 603 41 0 21453 0
vsize: 85976
[startup+759.999 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20989 0 1 0 75949 47 0 0 25 0 1 0 478446402 88039424 20968 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20968 603 41 0 21453 0
vsize: 85976
[startup+770 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20989 0 1 0 76949 47 0 0 25 0 1 0 478446402 88039424 20968 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20968 603 41 0 21453 0
vsize: 85976
[startup+780 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20989 0 1 0 77949 47 0 0 25 0 1 0 478446402 88039424 20968 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20968 603 41 0 21453 0
vsize: 85976
[startup+789.999 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20989 0 1 0 78949 47 0 0 25 0 1 0 478446402 88039424 20968 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20968 603 41 0 21453 0
vsize: 85976
[startup+799.999 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20989 0 1 0 79950 47 0 0 25 0 1 0 478446402 88039424 20968 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20968 603 41 0 21453 0
vsize: 85976
[startup+809.998 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20989 0 1 0 80950 47 0 0 25 0 1 0 478446402 88039424 20968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20968 603 41 0 21453 0
vsize: 85976
[startup+819.998 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20989 0 1 0 81950 47 0 0 25 0 1 0 478446402 88039424 20968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20968 603 41 0 21453 0
vsize: 85976
[startup+829.999 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20989 0 1 0 82950 47 0 0 25 0 1 0 478446402 88039424 20968 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20968 603 41 0 21453 0
vsize: 85976
[startup+839.999 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 20989 0 1 0 83950 47 0 0 25 0 1 0 478446402 88039424 20968 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20968 603 41 0 21453 0
vsize: 85976
[startup+849.998 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21226 0 1 0 84950 48 0 0 25 0 1 0 478446402 88985600 21205 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21205 603 41 0 21684 0
vsize: 86900
[startup+859.999 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21226 0 1 0 85950 48 0 0 25 0 1 0 478446402 88985600 21205 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21205 603 41 0 21684 0
vsize: 86900
[startup+869.999 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21226 0 1 0 86951 48 0 0 25 0 1 0 478446402 88985600 21205 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21205 603 41 0 21684 0
vsize: 86900
[startup+879.999 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21227 0 1 0 87950 48 0 0 25 0 1 0 478446402 88985600 21206 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21206 603 41 0 21684 0
vsize: 86900
[startup+889.998 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 88950 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+899.998 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 89950 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+909.999 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 90951 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+919.998 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 91951 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+929.999 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 92951 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+939.999 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 93951 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+949.998 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 94951 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+959.998 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 95951 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+969.998 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 96952 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+979.998 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 97952 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+989.998 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 98952 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+999.998 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 99952 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+1010 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 100952 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+1020 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21228 0 1 0 101953 48 0 0 25 0 1 0 478446402 88985600 21207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21207 603 41 0 21684 0
vsize: 86900
[startup+1030 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 102953 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1040 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 103953 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1050 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 104953 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1060 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 105953 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1070 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 106953 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1080 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 107954 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1090 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 108954 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1100 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 109954 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1110 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 110954 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1120 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 111954 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1130 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 112955 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1140 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 113955 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1150 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 114955 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1160 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 115955 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 116955 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 117956 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 118956 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 27731
Raw data (stat): 27731 (minisat+) R 27730 26298 26297 0 -1 0 21229 0 1 0 119956 48 0 0 25 0 1 0 478446402 88985600 21208 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21725 21208 603 41 0 21684 0
vsize: 86900
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 27731
Raw data (stat): 27731 (minisat+) Z 27730 26298 26297 0 -1 12 21231 0 1 0 119956 52 0 0 25 0 1 0 478446402 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.04
CPU time (s): 1200.09
CPU user time (s): 1199.57
CPU system time (s): 0.52492
CPU usage (%): 100.004
Max. virtual memory (Kb): 86900
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####