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 5779

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-14 01:44:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4190 boxname=wulflinc28 idbench=54 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f9a3a990ebca4aa5457d0675d3f1fe27  /oldhome/oroussel/tmp/wulflinc28/normalized-fpga40_40_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc28/normalized-fpga40_40_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc28/normalized-fpga40_40_sat_pb.cnf.cr.opb
IDLAUNCH: 4190
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        887676 kB
Buffers:         35636 kB
Cached:          74452 kB
SwapCached:          4 kB
Active:          53600 kB
Inactive:        60296 kB
HighTotal:      131008 kB
HighFree:        51940 kB
LowTotal:       903652 kB
LowFree:        835736 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27608 kB
Committed_AS:    63448 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:04:34 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 4190 7 1200.19 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]---> BDD-cost:   77
c ---[  78]---> BDD-cost:   77
c ---[  77]---> BDD-cost:   77
c ---[  76]---> BDD-cost:   77
c ---[  75]---> BDD-cost:   77
c ---[  74]---> BDD-cost:   77
c ---[  73]---> BDD-cost:   77
c ---[  72]---> BDD-cost:   77
c ---[  71]---> BDD-cost:   77
c ---[  70]---> BDD-cost:   77
c ---[  69]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  67]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  65]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  63]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   77
c ---[  61]---> BDD-cost:   77
c ---[  60]---> BDD-cost:   77
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   37
c ---[  38]---> BDD-cost:   37
c ---[  37]---> BDD-cost:   37
c ---[  36]---> BDD-cost:   37
c ---[  35]---> BDD-cost:   37
c ---[  34]---> BDD-cost:   37
c ---[  33]---> BDD-cost:   37
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   37
c ---[  30]---> BDD-cost:   37
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12920    64560 |    4306       0        0     nan |  0.000 % |
c |       100 |   12920    64560 |    4736     100    26004   260.0 |  1.149 % |
c |       252 |   12920    64560 |    5210     252    37714   149.7 |  1.150 % |
c |       477 |   12920    64560 |    5731     477    76875   161.2 |  1.149 % |
c |       814 |   12920    64560 |    6304     814   161811   198.8 |  1.149 % |
c |      1321 |   12920    64560 |    6934    1321   261531   198.0 |  1.149 % |
c |      2084 |   12920    64560 |    7628    2084   359745   172.6 |  1.149 % |
c |      3223 |   12920    64560 |    8391    3223   791517   245.6 |  1.149 % |
c |      4932 |   12920    64560 |    9230    4932  1197916   242.9 |  1.149 % |
c |      7496 |   12920    64560 |   10153    7496  2266760   302.4 |  1.150 % |
c |     11341 |   12920    64560 |   11168   11341  3377694   297.8 |  1.149 % |
c |     17108 |   12920    64560 |   12285   11438  4096533   358.2 |  1.149 % |
c |     25758 |   12920    64560 |   13514   12002  3744055   312.0 |  1.149 % |
c |     38732 |   12920    64560 |   14865   15473  2381199   153.9 |  1.149 % |
c |     58193 |   12920    64560 |   16352   17728  7855736   443.1 |  1.149 % |
c |     87385 |   12920    64560 |   17987   17936  6971394   388.7 |  1.149 % |
c |    131175 |   12920    64560 |   19785   15044  2526709   168.0 |  1.149 % |
c |    196861 |   12920    64560 |   21764   20319  9340279   459.7 |  1.149 % |
c |    295389 |   12920    64560 |   23941   18363  2895214   157.7 |  1.149 % |
#### 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.73 0.85 0.88 2/54 19511
Raw data (stat): 19511 (runsolver) R 19510 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480733302 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9998 s]
Raw data (loadavg): 0.77 0.85 0.88 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 3092 0 0 0 990 8 0 0 25 0 1 0 480733302 14258176 3070 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3481 3071 603 41 0 3440 0
vsize: 13924
[startup+20.0002 s]
Raw data (loadavg): 0.81 0.86 0.88 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 4473 0 0 0 1987 11 0 0 25 0 1 0 480733302 19931136 4451 4294967295 134512640 134672761 3221224528 3221223632 134559974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4866 4451 603 41 0 4825 0
vsize: 19464
[startup+30.0001 s]
Raw data (loadavg): 0.84 0.86 0.88 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 5183 0 0 0 2985 13 0 0 25 0 1 0 480733302 22757376 5161 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5556 5161 603 41 0 5515 0
vsize: 22224
[startup+40.0005 s]
Raw data (loadavg): 0.86 0.86 0.88 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 6735 0 0 0 3981 17 0 0 25 0 1 0 480733302 29102080 6713 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7105 6713 603 41 0 7064 0
vsize: 28420
[startup+50.0002 s]
Raw data (loadavg): 0.88 0.87 0.89 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 6759 0 0 0 4981 17 0 0 25 0 1 0 480733302 29237248 6737 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7138 6737 603 41 0 7097 0
vsize: 28552
[startup+60.0002 s]
Raw data (loadavg): 0.90 0.87 0.89 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 6759 0 0 0 5981 17 0 0 25 0 1 0 480733302 29237248 6737 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7138 6737 603 41 0 7097 0
vsize: 28552
[startup+70.0009 s]
Raw data (loadavg): 0.91 0.87 0.89 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 6759 0 0 0 6981 17 0 0 25 0 1 0 480733302 29237248 6737 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7138 6737 603 41 0 7097 0
vsize: 28552
[startup+80.0003 s]
Raw data (loadavg): 0.93 0.88 0.89 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 6759 0 0 0 7981 17 0 0 25 0 1 0 480733302 29237248 6737 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7138 6737 603 41 0 7097 0
vsize: 28552
[startup+90.0002 s]
Raw data (loadavg): 0.94 0.88 0.89 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 6759 0 0 0 8981 17 0 0 25 0 1 0 480733302 29237248 6737 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7138 6737 603 41 0 7097 0
vsize: 28552
[startup+99.9996 s]
Raw data (loadavg): 0.95 0.89 0.89 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 7312 0 0 0 9980 19 0 0 25 0 1 0 480733302 31539200 7290 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7700 7290 603 41 0 7659 0
vsize: 30800
[startup+109.999 s]
Raw data (loadavg): 0.95 0.89 0.89 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 7637 0 0 0 10979 19 0 0 25 0 1 0 480733302 32882688 7615 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8028 7615 603 41 0 7987 0
vsize: 32112
[startup+119.999 s]
Raw data (loadavg): 0.96 0.89 0.89 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 7637 0 0 0 11979 19 0 0 25 0 1 0 480733302 32882688 7615 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8028 7615 603 41 0 7987 0
vsize: 32112
[startup+129.999 s]
Raw data (loadavg): 0.97 0.89 0.89 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 7666 0 0 0 12979 19 0 0 25 0 1 0 480733302 33038336 7644 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8066 7644 603 41 0 8025 0
vsize: 32264
[startup+139.999 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 7916 0 0 0 13979 20 0 0 25 0 1 0 480733302 34123776 7894 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8331 7894 603 41 0 8290 0
vsize: 33324
[startup+149.999 s]
Raw data (loadavg): 0.98 0.90 0.90 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 8536 0 0 0 14977 22 0 0 25 0 1 0 480733302 36552704 8514 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8924 8514 603 41 0 8883 0
vsize: 35696
[startup+159.999 s]
Raw data (loadavg): 0.98 0.90 0.90 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 9260 0 0 0 15976 23 0 0 25 0 1 0 480733302 39530496 9238 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9651 9238 603 41 0 9610 0
vsize: 38604
[startup+170 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 9748 0 0 0 16974 25 0 0 25 0 1 0 480733302 41545728 9726 4294967295 134512640 134672761 3221224528 3221223712 134558768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+179.999 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 9748 0 0 0 17973 25 0 0 25 0 1 0 480733302 41545728 9726 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+190 s]
Raw data (loadavg): 0.99 0.91 0.90 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 9748 0 0 0 18974 25 0 0 25 0 1 0 480733302 41545728 9726 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+200 s]
Raw data (loadavg): 0.99 0.91 0.90 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 9748 0 0 0 19974 25 0 0 25 0 1 0 480733302 41545728 9726 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+210 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 9748 0 0 0 20974 25 0 0 25 0 1 0 480733302 41545728 9726 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+220.001 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 9748 0 0 0 21974 25 0 0 25 0 1 0 480733302 41545728 9726 4294967295 134512640 134672761 3221224528 3221223668 134560629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+230 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 9748 0 0 0 22974 25 0 0 25 0 1 0 480733302 41545728 9726 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+240 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 9748 0 0 0 23974 25 0 0 25 0 1 0 480733302 41545728 9726 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+250 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 9748 0 0 0 24975 25 0 0 25 0 1 0 480733302 41545728 9726 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10143 9726 603 41 0 10102 0
vsize: 40572
[startup+260 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 10023 0 0 0 25974 26 0 0 25 0 1 0 480733302 42827776 10001 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10456 10001 603 41 0 10415 0
vsize: 41824
[startup+270 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 10038 0 0 0 26974 26 0 0 25 0 1 0 480733302 42827776 10016 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10456 10016 603 41 0 10415 0
vsize: 41824
[startup+279.999 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 10058 0 0 0 27974 26 0 0 25 0 1 0 480733302 42983424 10036 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10494 10036 603 41 0 10453 0
vsize: 41976
[startup+290 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 10102 0 0 0 28974 26 0 0 25 0 1 0 480733302 43180032 10080 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10542 10080 603 41 0 10501 0
vsize: 42168
[startup+300 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 10135 0 0 0 29974 26 0 0 25 0 1 0 480733302 43376640 10113 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10590 10113 603 41 0 10549 0
vsize: 42360
[startup+310 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 30971 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223632 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+320 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 31970 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223712 134559514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+330 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 32970 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+340 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 33970 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+350 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 34970 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223632 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+360 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 35970 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+370 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 36971 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+380 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 37971 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+390 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 38971 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223680 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+400 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 39971 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+410 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 40971 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223632 134559953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+420 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 41971 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+429.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 42972 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223664 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+440 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 43972 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+450 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 11213 0 0 0 44972 30 0 0 25 0 1 0 480733302 47816704 11191 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11674 11191 603 41 0 11633 0
vsize: 46696
[startup+459.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 12473 0 0 0 45969 33 0 0 25 0 1 0 480733302 53080064 12451 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12959 12451 603 41 0 12918 0
vsize: 51836
[startup+470 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 13812 0 0 0 46966 36 0 0 25 0 1 0 480733302 58486784 13790 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14279 13790 603 41 0 14238 0
vsize: 57116
[startup+480 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 13896 0 0 0 47966 36 0 0 25 0 1 0 480733302 58892288 13874 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14378 13874 603 41 0 14337 0
vsize: 57512
[startup+490.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 13896 0 0 0 48966 36 0 0 25 0 1 0 480733302 58892288 13874 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14378 13874 603 41 0 14337 0
vsize: 57512
[startup+500 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 13896 0 0 0 49966 36 0 0 25 0 1 0 480733302 58892288 13874 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14378 13874 603 41 0 14337 0
vsize: 57512
[startup+510 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 13896 0 0 0 50966 36 0 0 25 0 1 0 480733302 58892288 13874 4294967295 134512640 134672761 3221224528 3221223712 134558856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14378 13874 603 41 0 14337 0
vsize: 57512
[startup+519.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14199 0 0 0 51966 37 0 0 25 0 1 0 480733302 60108800 14177 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14675 14177 603 41 0 14634 0
vsize: 58700
[startup+529.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14376 0 0 0 52966 38 0 0 25 0 1 0 480733302 60788736 14354 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14841 14354 603 41 0 14800 0
vsize: 59364
[startup+540 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14376 0 0 0 53965 38 0 0 25 0 1 0 480733302 60788736 14354 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14841 14354 603 41 0 14800 0
vsize: 59364
[startup+550.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14376 0 0 0 54965 38 0 0 25 0 1 0 480733302 60788736 14354 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14841 14354 603 41 0 14800 0
vsize: 59364
[startup+560 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14376 0 0 0 55965 38 0 0 25 0 1 0 480733302 60788736 14354 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14841 14354 603 41 0 14800 0
vsize: 59364
[startup+570 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14376 0 0 0 56965 38 0 0 25 0 1 0 480733302 60788736 14354 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14841 14354 603 41 0 14800 0
vsize: 59364
[startup+580 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14377 0 0 0 57965 38 0 0 25 0 1 0 480733302 60788736 14355 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14841 14355 603 41 0 14800 0
vsize: 59364
[startup+590 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14377 0 0 0 58966 38 0 0 25 0 1 0 480733302 60788736 14355 4294967295 134512640 134672761 3221224528 3221223680 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14841 14355 603 41 0 14800 0
vsize: 59364
[startup+600 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14377 0 0 0 59966 38 0 0 25 0 1 0 480733302 60788736 14355 4294967295 134512640 134672761 3221224528 3221223712 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14841 14355 603 41 0 14800 0
vsize: 59364
[startup+610 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14377 0 0 0 60966 38 0 0 25 0 1 0 480733302 60788736 14355 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14841 14355 603 41 0 14800 0
vsize: 59364
[startup+620 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14549 0 0 0 61966 38 0 0 25 0 1 0 480733302 61464576 14527 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15006 14527 603 41 0 14965 0
vsize: 60024
[startup+630 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14549 0 0 0 62966 38 0 0 25 0 1 0 480733302 61464576 14527 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15006 14527 603 41 0 14965 0
vsize: 60024
[startup+640 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14549 0 0 0 63966 38 0 0 25 0 1 0 480733302 61464576 14527 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15006 14527 603 41 0 14965 0
vsize: 60024
[startup+650 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14549 0 0 0 64966 38 0 0 25 0 1 0 480733302 61464576 14527 4294967295 134512640 134672761 3221224528 3221223712 134558890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15006 14527 603 41 0 14965 0
vsize: 60024
[startup+660 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14549 0 0 0 65966 38 0 0 25 0 1 0 480733302 61464576 14527 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15006 14527 603 41 0 14965 0
vsize: 60024
[startup+670.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 66966 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+680.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 67966 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+690.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 68966 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+700 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 69966 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+710 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 70966 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+720 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 71966 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223712 134558943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+730 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 72967 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+740 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 73967 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223632 134559802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+750 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 74967 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+760 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 75967 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+769.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 76967 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+779.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 77967 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+790 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 78968 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+799.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 79968 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+809.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 80968 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+820 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14670 0 0 0 81968 39 0 0 25 0 1 0 480733302 62005248 14648 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14648 603 41 0 15097 0
vsize: 60552
[startup+829.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 82968 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+839.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 83968 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+850 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 84969 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223696 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+859.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 85969 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+869.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 86969 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+879.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 87969 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+889.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 88969 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223712 134558930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+899.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 89969 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+909.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 90968 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+919.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 91969 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+929.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19511
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 92969 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+940 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 19564
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 93969 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+949.999 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 19564
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 94969 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+960.012 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 19564
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 95971 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+970.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 19564
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 14671 0 0 0 96971 39 0 0 25 0 1 0 480733302 62005248 14649 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15138 14649 603 41 0 15097 0
vsize: 60552
[startup+980.012 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 19564
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 15031 0 0 0 97971 39 0 0 25 0 1 0 480733302 63492096 15009 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15501 15009 603 41 0 15460 0
vsize: 62004
[startup+990.013 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 19564
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 15884 0 0 0 98969 41 0 0 25 0 1 0 480733302 67006464 15862 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16359 15862 603 41 0 16318 0
vsize: 65436
[startup+1000.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 19564
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 16580 0 0 0 99968 43 0 0 25 0 1 0 480733302 69844992 16558 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17052 16558 603 41 0 17011 0
vsize: 68208
[startup+1010.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 19564
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17165 0 0 0 100967 44 0 0 25 0 1 0 480733302 72278016 17143 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17646 17143 603 41 0 17605 0
vsize: 70584
[startup+1020.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17455 0 0 0 101966 44 0 0 25 0 1 0 480733302 73494528 17433 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17433 603 41 0 17902 0
vsize: 71772
[startup+1030.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17456 0 0 0 102967 44 0 0 25 0 1 0 480733302 73494528 17434 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17434 603 41 0 17902 0
vsize: 71772
[startup+1040.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17457 0 0 0 103967 44 0 0 25 0 1 0 480733302 73494528 17435 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17435 603 41 0 17902 0
vsize: 71772
[startup+1050.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17457 0 0 0 104967 44 0 0 25 0 1 0 480733302 73494528 17435 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17435 603 41 0 17902 0
vsize: 71772
[startup+1060.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17458 0 0 0 105967 44 0 0 25 0 1 0 480733302 73494528 17436 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17436 603 41 0 17902 0
vsize: 71772
[startup+1070.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17458 0 0 0 106967 44 0 0 25 0 1 0 480733302 73494528 17436 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17436 603 41 0 17902 0
vsize: 71772
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17458 0 0 0 107967 44 0 0 25 0 1 0 480733302 73494528 17436 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17436 603 41 0 17902 0
vsize: 71772
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17458 0 0 0 108968 44 0 0 25 0 1 0 480733302 73494528 17436 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17436 603 41 0 17902 0
vsize: 71772
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17461 0 0 0 109968 44 0 0 25 0 1 0 480733302 73494528 17439 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17439 603 41 0 17902 0
vsize: 71772
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17461 0 0 0 110968 44 0 0 25 0 1 0 480733302 73494528 17439 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17439 603 41 0 17902 0
vsize: 71772
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17461 0 0 0 111968 44 0 0 25 0 1 0 480733302 73494528 17439 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17439 603 41 0 17902 0
vsize: 71772
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17461 0 0 0 112969 44 0 0 25 0 1 0 480733302 73494528 17439 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 17439 603 41 0 17902 0
vsize: 71772
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 17876 0 0 0 113968 45 0 0 25 0 1 0 480733302 75116544 17854 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18339 17854 603 41 0 18298 0
vsize: 73356
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 18331 0 0 0 114967 46 0 0 25 0 1 0 480733302 77008896 18309 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18801 18309 603 41 0 18760 0
vsize: 75204
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 18977 0 0 0 115965 48 0 0 25 0 1 0 480733302 79716352 18955 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19462 18955 603 41 0 19421 0
vsize: 77848
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 19393 0 0 0 116964 49 0 0 25 0 1 0 480733302 81469440 19371 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19890 19371 603 41 0 19849 0
vsize: 79560
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 19900 0 0 0 117963 51 0 0 25 0 1 0 480733302 83509248 19878 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20388 19878 603 41 0 20347 0
vsize: 81552
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 20442 0 0 0 118962 52 0 0 25 0 1 0 480733302 85676032 20420 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20917 20420 603 41 0 20876 0
vsize: 83668
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19566
Raw data (stat): 19511 (minisat+) R 19510 10614 10613 0 -1 0 20799 0 0 0 119961 53 0 0 25 0 1 0 480733302 87162880 20777 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21280 20777 603 41 0 21239 0
vsize: 85120
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 19566
Raw data (stat): 19511 (minisat+) Z 19510 10614 10613 0 -1 12 20801 0 0 0 119961 57 0 0 25 0 1 0 480733302 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.19
CPU user time (s): 1199.62
CPU system time (s): 0.572912
CPU usage (%): 100.011
Max. virtual memory (Kb): 85120
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####