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-chnl20_25_pb.cnf.cr.opb
MD5SUM	6c328ef6f9d8d5a179eec9bf3550b7fd
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	26
Number of bits of the biggest sum of numbers	5
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.027995
Number of variables	1000
Total number of constraints	90
Number of constraints which are clauses	50
Number of constraints which are cardinality constraints (but not clauses)	40
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	20
Maximum length of a constraint	25
Trace number 4578

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        921772 kB
Buffers:         34048 kB
Cached:          54724 kB
SwapCached:       4932 kB
Active:          51872 kB
Inactive:        44684 kB
HighTotal:      131008 kB
HighFree:        72492 kB
LowTotal:       903652 kB
LowFree:        849280 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10780 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:43:57 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 3393 7 1200.16 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 90 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  39]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  38]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  37]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  36]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  35]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  34]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  33]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  32]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  31]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  30]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  29]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  28]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  27]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  26]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  25]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  24]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  23]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  22]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  21]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  20]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  19]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  18]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  17]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  16]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  15]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  14]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  13]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  12]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  11]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  10]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   9]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   8]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   7]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   6]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   5]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   4]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   3]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   2]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   1]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   0]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10890    39280 |    3630       0        0     nan |  0.000 % |
c |       100 |    9810    35576 |    3993       9       69     7.7 | 12.836 % |
c |       250 |    9448    34324 |    4392     119      464     3.9 | 15.336 % |
c |       477 |    9198    33452 |    4831     316     1554     4.9 | 17.164 % |
c |       814 |    8428    30842 |    5314     551     2994     5.4 | 22.276 % |
c |      1320 |    6875    25575 |    5846     825     6395     7.8 | 33.022 % |
c |      2080 |    6782    25266 |    6430    1570   128047    81.6 | 33.619 % |
c |      3219 |    6764    25208 |    7073    2706   351404   129.9 | 33.769 % |
c |      4927 |    6755    25179 |    7781    4413   679105   153.9 | 33.843 % |
c |      7490 |    6716    25052 |    8559    6968  1319851   189.4 | 34.104 % |
c |     11335 |    6716    25052 |    9415    5864  1272883   217.1 | 34.105 % |
c |     17103 |    6716    25052 |   10356    6222  1306788   210.0 | 34.104 % |
c |     25754 |    6716    25052 |   11392    9029  1966278   217.8 | 34.104 % |
c |     38728 |    6716    25052 |   12531    9224  1994219   216.2 | 34.104 % |
c |     58190 |    6716    25052 |   13784    7788  1658320   212.9 | 34.104 % |
c |     87384 |    6683    24941 |   15163   14251  3568264   250.4 | 34.366 % |
c |    131175 |    6683    24941 |   16679    8519  1711727   200.9 | 34.366 % |
c |    196863 |    6642    24808 |   18347   11020  2483657   225.4 | 34.664 % |
c |    295393 |    6642    24808 |   20182   10845  2318096   213.7 | 34.664 % |
#### 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.78 0.31 0.15 2/54 2130
Raw data (stat): 2130 (runsolver) R 2129 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420221357 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.81 0.33 0.16 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 2317 0 0 0 993 5 0 0 25 0 1 0 420221357 11116544 2295 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2714 2295 603 41 0 2673 0
vsize: 10856
[startup+20.0011 s]
Raw data (loadavg): 0.84 0.35 0.17 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 2738 0 0 0 1991 6 0 0 25 0 1 0 420221357 12861440 2716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3140 2716 603 41 0 3099 0
vsize: 12560
[startup+30.0008 s]
Raw data (loadavg): 0.87 0.37 0.17 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 3222 0 0 0 2990 8 0 0 25 0 1 0 420221357 14876672 3200 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3632 3200 603 41 0 3591 0
vsize: 14528
[startup+40.0009 s]
Raw data (loadavg): 0.89 0.39 0.18 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 3369 0 0 0 3990 8 0 0 25 0 1 0 420221357 15413248 3347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3763 3347 603 41 0 3722 0
vsize: 15052
[startup+50.0014 s]
Raw data (loadavg): 0.90 0.41 0.19 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 3510 0 0 0 4989 8 0 0 25 0 1 0 420221357 16084992 3488 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3927 3488 603 41 0 3886 0
vsize: 15708
[startup+60.0012 s]
Raw data (loadavg): 0.92 0.43 0.20 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 3862 0 0 0 5988 10 0 0 25 0 1 0 420221357 17436672 3840 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4257 3840 603 41 0 4216 0
vsize: 17028
[startup+70.0013 s]
Raw data (loadavg): 0.93 0.45 0.21 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 3862 0 0 0 6988 10 0 0 25 0 1 0 420221357 17436672 3840 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4257 3840 603 41 0 4216 0
vsize: 17028
[startup+80.0007 s]
Raw data (loadavg): 0.94 0.47 0.21 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 4162 0 0 0 7988 10 0 0 25 0 1 0 420221357 18644992 4140 4294967295 134512640 134672761 3221224544 3221223696 134541819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4552 4140 603 41 0 4511 0
vsize: 18208
[startup+90.0005 s]
Raw data (loadavg): 0.95 0.48 0.22 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 4335 0 0 0 8988 11 0 0 25 0 1 0 420221357 19447808 4313 4294967295 134512640 134672761 3221224544 3221223712 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4748 4313 603 41 0 4707 0
vsize: 18992
[startup+100.001 s]
Raw data (loadavg): 0.96 0.50 0.23 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 4366 0 0 0 9988 11 0 0 25 0 1 0 420221357 19582976 4344 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4781 4344 603 41 0 4740 0
vsize: 19124
[startup+110.001 s]
Raw data (loadavg): 0.96 0.52 0.24 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 4366 0 0 0 10987 11 0 0 25 0 1 0 420221357 19582976 4344 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4344 603 41 0 4740 0
vsize: 19124
[startup+120.002 s]
Raw data (loadavg): 0.97 0.53 0.25 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 4366 0 0 0 11986 11 0 0 25 0 1 0 420221357 19582976 4344 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4344 603 41 0 4740 0
vsize: 19124
[startup+130.002 s]
Raw data (loadavg): 0.97 0.55 0.25 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 4540 0 0 0 12985 12 0 0 25 0 1 0 420221357 20267008 4518 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4948 4518 603 41 0 4907 0
vsize: 19792
[startup+140.002 s]
Raw data (loadavg): 0.98 0.56 0.26 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 4845 0 0 0 13984 13 0 0 25 0 1 0 420221357 21483520 4823 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5245 4823 603 41 0 5204 0
vsize: 20980
[startup+150.002 s]
Raw data (loadavg): 0.98 0.58 0.27 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 4845 0 0 0 14984 13 0 0 25 0 1 0 420221357 21483520 4823 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5245 4823 603 41 0 5204 0
vsize: 20980
[startup+160.002 s]
Raw data (loadavg): 0.98 0.59 0.28 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 4845 0 0 0 15984 13 0 0 25 0 1 0 420221357 21483520 4823 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5245 4823 603 41 0 5204 0
vsize: 20980
[startup+170.002 s]
Raw data (loadavg): 0.98 0.60 0.28 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5182 0 0 0 16984 13 0 0 25 0 1 0 420221357 22851584 5160 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5579 5160 603 41 0 5538 0
vsize: 22316
[startup+180.002 s]
Raw data (loadavg): 0.99 0.61 0.29 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5218 0 0 0 17984 14 0 0 25 0 1 0 420221357 22986752 5196 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5612 5196 603 41 0 5571 0
vsize: 22448
[startup+190.003 s]
Raw data (loadavg): 0.99 0.63 0.30 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5218 0 0 0 18984 14 0 0 25 0 1 0 420221357 22986752 5196 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5612 5196 603 41 0 5571 0
vsize: 22448
[startup+200.002 s]
Raw data (loadavg): 0.99 0.64 0.30 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5277 0 0 0 19984 14 0 0 25 0 1 0 420221357 23318528 5255 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5693 5255 603 41 0 5652 0
vsize: 22772
[startup+210.002 s]
Raw data (loadavg): 0.99 0.65 0.31 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5277 0 0 0 20984 14 0 0 25 0 1 0 420221357 23318528 5255 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5693 5255 603 41 0 5652 0
vsize: 22772
[startup+220.002 s]
Raw data (loadavg): 0.99 0.66 0.32 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5277 0 0 0 21984 14 0 0 25 0 1 0 420221357 23318528 5255 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5693 5255 603 41 0 5652 0
vsize: 22772
[startup+230.001 s]
Raw data (loadavg): 0.99 0.67 0.32 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5277 0 0 0 22984 14 0 0 25 0 1 0 420221357 23318528 5255 4294967295 134512640 134672761 3221224544 3221223640 1075347230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5693 5255 603 41 0 5652 0
vsize: 22772
[startup+240.002 s]
Raw data (loadavg): 0.99 0.68 0.33 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5534 0 0 0 23983 15 0 0 25 0 1 0 420221357 24408064 5512 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5959 5512 603 41 0 5918 0
vsize: 23836
[startup+250.001 s]
Raw data (loadavg): 0.99 0.69 0.34 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5637 0 0 0 24983 15 0 0 25 0 1 0 420221357 24977408 5615 4294967295 134512640 134672761 3221224544 3221223728 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6098 5615 603 41 0 6057 0
vsize: 24392
[startup+260.002 s]
Raw data (loadavg): 0.99 0.70 0.35 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5637 0 0 0 25983 15 0 0 25 0 1 0 420221357 24977408 5615 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6098 5615 603 41 0 6057 0
vsize: 24392
[startup+270.002 s]
Raw data (loadavg): 0.99 0.71 0.35 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5637 0 0 0 26983 15 0 0 25 0 1 0 420221357 24977408 5615 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6098 5615 603 41 0 6057 0
vsize: 24392
[startup+280.002 s]
Raw data (loadavg): 0.99 0.72 0.36 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5637 0 0 0 27984 15 0 0 25 0 1 0 420221357 24977408 5615 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6098 5615 603 41 0 6057 0
vsize: 24392
[startup+290.002 s]
Raw data (loadavg): 0.99 0.73 0.37 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5637 0 0 0 28984 15 0 0 25 0 1 0 420221357 24977408 5615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6098 5615 603 41 0 6057 0
vsize: 24392
[startup+300.002 s]
Raw data (loadavg): 0.99 0.74 0.37 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5649 0 0 0 29984 15 0 0 25 0 1 0 420221357 24977408 5627 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6098 5627 603 41 0 6057 0
vsize: 24392
[startup+310.003 s]
Raw data (loadavg): 0.99 0.75 0.38 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5649 0 0 0 30984 15 0 0 25 0 1 0 420221357 24977408 5627 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6098 5627 603 41 0 6057 0
vsize: 24392
[startup+320.003 s]
Raw data (loadavg): 0.99 0.75 0.38 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5667 0 0 0 31984 15 0 0 25 0 1 0 420221357 24977408 5645 4294967295 134512640 134672761 3221224544 3221223728 134559334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6098 5645 603 41 0 6057 0
vsize: 24392
[startup+330.002 s]
Raw data (loadavg): 0.99 0.76 0.39 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5667 0 0 0 32984 15 0 0 25 0 1 0 420221357 24977408 5645 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6098 5645 603 41 0 6057 0
vsize: 24392
[startup+340.002 s]
Raw data (loadavg): 0.99 0.77 0.39 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5667 0 0 0 33984 15 0 0 25 0 1 0 420221357 24977408 5645 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6098 5645 603 41 0 6057 0
vsize: 24392
[startup+350.002 s]
Raw data (loadavg): 0.99 0.78 0.40 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5667 0 0 0 34985 15 0 0 25 0 1 0 420221357 24977408 5645 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6098 5645 603 41 0 6057 0
vsize: 24392
[startup+360.003 s]
Raw data (loadavg): 0.99 0.78 0.41 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5673 0 0 0 35985 15 0 0 25 0 1 0 420221357 25149440 5651 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6140 5651 603 41 0 6099 0
vsize: 24560
[startup+370.003 s]
Raw data (loadavg): 0.99 0.79 0.41 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5674 0 0 0 36985 15 0 0 25 0 1 0 420221357 25149440 5652 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6140 5652 603 41 0 6099 0
vsize: 24560
[startup+380.002 s]
Raw data (loadavg): 0.99 0.80 0.42 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5674 0 0 0 37985 15 0 0 25 0 1 0 420221357 25149440 5652 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6140 5652 603 41 0 6099 0
vsize: 24560
[startup+390.002 s]
Raw data (loadavg): 0.99 0.80 0.42 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5674 0 0 0 38985 15 0 0 25 0 1 0 420221357 25149440 5652 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6140 5652 603 41 0 6099 0
vsize: 24560
[startup+400.002 s]
Raw data (loadavg): 0.99 0.81 0.43 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5881 0 0 0 39984 16 0 0 25 0 1 0 420221357 25956352 5859 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6337 5859 603 41 0 6296 0
vsize: 25348
[startup+410.003 s]
Raw data (loadavg): 0.99 0.81 0.44 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5881 0 0 0 40984 16 0 0 25 0 1 0 420221357 25956352 5859 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6337 5859 603 41 0 6296 0
vsize: 25348
[startup+420.003 s]
Raw data (loadavg): 0.99 0.82 0.44 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5881 0 0 0 41985 16 0 0 25 0 1 0 420221357 25956352 5859 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6337 5859 603 41 0 6296 0
vsize: 25348
[startup+430.002 s]
Raw data (loadavg): 0.99 0.83 0.45 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5881 0 0 0 42985 16 0 0 25 0 1 0 420221357 25956352 5859 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6337 5859 603 41 0 6296 0
vsize: 25348
[startup+440.003 s]
Raw data (loadavg): 0.99 0.83 0.45 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 5881 0 0 0 43985 16 0 0 25 0 1 0 420221357 25956352 5859 4294967295 134512640 134672761 3221224544 3221223648 134560269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6337 5859 603 41 0 6296 0
vsize: 25348
[startup+450.003 s]
Raw data (loadavg): 0.99 0.83 0.46 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6250 0 0 0 44984 17 0 0 25 0 1 0 420221357 27443200 6228 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6228 603 41 0 6659 0
vsize: 26800
[startup+460.004 s]
Raw data (loadavg): 0.99 0.84 0.46 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6250 0 0 0 45984 17 0 0 25 0 1 0 420221357 27443200 6228 4294967295 134512640 134672761 3221224544 3221223556 1075351040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6228 603 41 0 6659 0
vsize: 26800
[startup+470.003 s]
Raw data (loadavg): 0.99 0.84 0.47 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6250 0 0 0 46984 17 0 0 25 0 1 0 420221357 27443200 6228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6228 603 41 0 6659 0
vsize: 26800
[startup+480.004 s]
Raw data (loadavg): 0.99 0.85 0.47 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6250 0 0 0 47984 17 0 0 25 0 1 0 420221357 27443200 6228 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6228 603 41 0 6659 0
vsize: 26800
[startup+490.004 s]
Raw data (loadavg): 0.99 0.85 0.48 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6250 0 0 0 48985 17 0 0 25 0 1 0 420221357 27443200 6228 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6228 603 41 0 6659 0
vsize: 26800
[startup+500.004 s]
Raw data (loadavg): 0.99 0.86 0.48 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6250 0 0 0 49985 17 0 0 25 0 1 0 420221357 27443200 6228 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6228 603 41 0 6659 0
vsize: 26800
[startup+510.004 s]
Raw data (loadavg): 0.99 0.86 0.49 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6250 0 0 0 50985 17 0 0 25 0 1 0 420221357 27443200 6228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6228 603 41 0 6659 0
vsize: 26800
[startup+520.003 s]
Raw data (loadavg): 0.99 0.87 0.49 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6250 0 0 0 51985 17 0 0 25 0 1 0 420221357 27443200 6228 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6228 603 41 0 6659 0
vsize: 26800
[startup+530.003 s]
Raw data (loadavg): 0.99 0.87 0.50 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6250 0 0 0 52985 17 0 0 25 0 1 0 420221357 27443200 6228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6228 603 41 0 6659 0
vsize: 26800
[startup+540.004 s]
Raw data (loadavg): 0.99 0.87 0.50 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6250 0 0 0 53985 17 0 0 25 0 1 0 420221357 27443200 6228 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6228 603 41 0 6659 0
vsize: 26800
[startup+550.004 s]
Raw data (loadavg): 0.99 0.88 0.51 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6250 0 0 0 54986 17 0 0 25 0 1 0 420221357 27443200 6228 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6228 603 41 0 6659 0
vsize: 26800
[startup+560.004 s]
Raw data (loadavg): 0.99 0.88 0.51 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6269 0 0 0 55986 17 0 0 25 0 1 0 420221357 27574272 6247 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6732 6247 603 41 0 6691 0
vsize: 26928
[startup+570.005 s]
Raw data (loadavg): 0.99 0.89 0.52 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6269 0 0 0 56985 18 0 0 25 0 1 0 420221357 27574272 6247 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6732 6247 603 41 0 6691 0
vsize: 26928
[startup+580.004 s]
Raw data (loadavg): 0.99 0.89 0.52 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6329 0 0 0 57985 18 0 0 25 0 1 0 420221357 27852800 6307 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6800 6307 603 41 0 6759 0
vsize: 27200
[startup+590.004 s]
Raw data (loadavg): 0.99 0.89 0.53 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6857 0 0 0 58984 19 0 0 25 0 1 0 420221357 30031872 6835 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7332 6835 603 41 0 7291 0
vsize: 29328
[startup+600.004 s]
Raw data (loadavg): 0.99 0.89 0.53 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6857 0 0 0 59984 19 0 0 25 0 1 0 420221357 30031872 6835 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7332 6835 603 41 0 7291 0
vsize: 29328
[startup+610.004 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6876 0 0 0 60985 19 0 0 25 0 1 0 420221357 30195712 6854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7372 6854 603 41 0 7331 0
vsize: 29488
[startup+620.004 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6934 0 0 0 61985 19 0 0 25 0 1 0 420221357 30466048 6912 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7438 6912 603 41 0 7397 0
vsize: 29752
[startup+630.004 s]
Raw data (loadavg): 0.99 0.90 0.55 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6934 0 0 0 62985 19 0 0 25 0 1 0 420221357 30466048 6912 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7438 6912 603 41 0 7397 0
vsize: 29752
[startup+640.005 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6934 0 0 0 63985 19 0 0 25 0 1 0 420221357 30466048 6912 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7438 6912 603 41 0 7397 0
vsize: 29752
[startup+650.004 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6934 0 0 0 64985 19 0 0 25 0 1 0 420221357 30466048 6912 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7438 6912 603 41 0 7397 0
vsize: 29752
[startup+660.006 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6967 0 0 0 65985 19 0 0 25 0 1 0 420221357 30601216 6945 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6945 603 41 0 7430 0
vsize: 29884
[startup+670.006 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6979 0 0 0 66986 19 0 0 25 0 1 0 420221357 30601216 6957 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6957 603 41 0 7430 0
vsize: 29884
[startup+680.006 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 67986 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+690.007 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 68986 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+700.006 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 69986 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+710.006 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 70986 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+720.008 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 71986 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+730.007 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 72987 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+740.007 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 73987 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+750.007 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 74987 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+760.007 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 75987 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+770.007 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 76987 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+780.007 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 77986 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+790.007 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 78987 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+800.007 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 6981 0 0 0 79987 19 0 0 25 0 1 0 420221357 30601216 6959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6959 603 41 0 7430 0
vsize: 29884
[startup+810.007 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 7597 0 0 0 80985 21 0 0 25 0 1 0 420221357 33161216 7575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8096 7575 603 41 0 8055 0
vsize: 32384
[startup+820.008 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 7621 0 0 0 81986 21 0 0 25 0 1 0 420221357 33316864 7599 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8134 7599 603 41 0 8093 0
vsize: 32536
[startup+830.008 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 7621 0 0 0 82986 21 0 0 25 0 1 0 420221357 33316864 7599 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8134 7599 603 41 0 8093 0
vsize: 32536
[startup+840.008 s]
Raw data (loadavg): 0.99 0.94 0.63 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 7621 0 0 0 83986 21 0 0 25 0 1 0 420221357 33316864 7599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8134 7599 603 41 0 8093 0
vsize: 32536
[startup+850.008 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8009 0 0 0 84985 22 0 0 25 0 1 0 420221357 34832384 7987 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8504 7987 603 41 0 8463 0
vsize: 34016
[startup+860.008 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8009 0 0 0 85985 22 0 0 25 0 1 0 420221357 34832384 7987 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8504 7987 603 41 0 8463 0
vsize: 34016
[startup+870.008 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8009 0 0 0 86985 22 0 0 25 0 1 0 420221357 34832384 7987 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8504 7987 603 41 0 8463 0
vsize: 34016
[startup+880.008 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8009 0 0 0 87986 22 0 0 25 0 1 0 420221357 34832384 7987 4294967295 134512640 134672761 3221224544 3221223648 134559769 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8504 7987 603 41 0 8463 0
vsize: 34016
[startup+890.007 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8009 0 0 0 88986 22 0 0 25 0 1 0 420221357 34832384 7987 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8504 7987 603 41 0 8463 0
vsize: 34016
[startup+900.008 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8009 0 0 0 89986 22 0 0 25 0 1 0 420221357 34832384 7987 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8504 7987 603 41 0 8463 0
vsize: 34016
[startup+910.008 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8009 0 0 0 90986 22 0 0 25 0 1 0 420221357 34832384 7987 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8504 7987 603 41 0 8463 0
vsize: 34016
[startup+920.008 s]
Raw data (loadavg): 0.99 0.95 0.65 3/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8010 0 0 0 91986 22 0 0 25 0 1 0 420221357 34832384 7988 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8504 7988 603 41 0 8463 0
vsize: 34016
[startup+930.008 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8010 0 0 0 92986 22 0 0 25 0 1 0 420221357 34832384 7988 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8504 7988 603 41 0 8463 0
vsize: 34016
[startup+940.008 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8030 0 0 0 93987 22 0 0 25 0 1 0 420221357 34967552 8008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 8008 603 41 0 8496 0
vsize: 34148
[startup+950.008 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8047 0 0 0 94987 22 0 0 25 0 1 0 420221357 34967552 8025 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 8025 603 41 0 8496 0
vsize: 34148
[startup+960.009 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8047 0 0 0 95987 22 0 0 25 0 1 0 420221357 34967552 8025 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 8025 603 41 0 8496 0
vsize: 34148
[startup+970.01 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8048 0 0 0 96987 22 0 0 25 0 1 0 420221357 34967552 8026 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 8026 603 41 0 8496 0
vsize: 34148
[startup+980.009 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8048 0 0 0 97987 22 0 0 25 0 1 0 420221357 34967552 8026 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 8026 603 41 0 8496 0
vsize: 34148
[startup+990.009 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8048 0 0 0 98988 22 0 0 25 0 1 0 420221357 34967552 8026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 8026 603 41 0 8496 0
vsize: 34148
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8048 0 0 0 99988 22 0 0 25 0 1 0 420221357 34967552 8026 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 8026 603 41 0 8496 0
vsize: 34148
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8048 0 0 0 100988 22 0 0 25 0 1 0 420221357 34967552 8026 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 8026 603 41 0 8496 0
vsize: 34148
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8048 0 0 0 101988 22 0 0 25 0 1 0 420221357 34967552 8026 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 8026 603 41 0 8496 0
vsize: 34148
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8048 0 0 0 102988 22 0 0 25 0 1 0 420221357 34967552 8026 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 8026 603 41 0 8496 0
vsize: 34148
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8048 0 0 0 103988 22 0 0 25 0 1 0 420221357 34967552 8026 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 8026 603 41 0 8496 0
vsize: 34148
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8123 0 0 0 104988 22 0 0 25 0 1 0 420221357 35373056 8101 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8636 8101 603 41 0 8595 0
vsize: 34544
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8124 0 0 0 105989 22 0 0 25 0 1 0 420221357 35373056 8102 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8636 8102 603 41 0 8595 0
vsize: 34544
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8124 0 0 0 106989 22 0 0 25 0 1 0 420221357 35373056 8102 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8636 8102 603 41 0 8595 0
vsize: 34544
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8124 0 0 0 107989 22 0 0 25 0 1 0 420221357 35373056 8102 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8636 8102 603 41 0 8595 0
vsize: 34544
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8145 0 0 0 108989 22 0 0 25 0 1 0 420221357 35536896 8123 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8676 8123 603 41 0 8635 0
vsize: 34704
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.71 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8334 0 0 0 109989 23 0 0 25 0 1 0 420221357 36212736 8312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8841 8312 603 41 0 8800 0
vsize: 35364
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.71 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8393 0 0 0 110989 23 0 0 25 0 1 0 420221357 36478976 8371 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8906 8371 603 41 0 8865 0
vsize: 35624
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.71 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8393 0 0 0 111989 23 0 0 25 0 1 0 420221357 36478976 8371 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8906 8371 603 41 0 8865 0
vsize: 35624
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.72 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8393 0 0 0 112989 23 0 0 25 0 1 0 420221357 36478976 8371 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8906 8371 603 41 0 8865 0
vsize: 35624
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.72 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8406 0 0 0 113989 23 0 0 25 0 1 0 420221357 36638720 8384 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8945 8384 603 41 0 8904 0
vsize: 35780
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.72 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8406 0 0 0 114989 23 0 0 25 0 1 0 420221357 36638720 8384 4294967295 134512640 134672761 3221224544 3221223712 134561009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8945 8384 603 41 0 8904 0
vsize: 35780
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.72 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8406 0 0 0 115990 23 0 0 25 0 1 0 420221357 36638720 8384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8945 8384 603 41 0 8904 0
vsize: 35780
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8406 0 0 0 116990 23 0 0 25 0 1 0 420221357 36638720 8384 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8945 8384 603 41 0 8904 0
vsize: 35780
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8406 0 0 0 117990 23 0 0 25 0 1 0 420221357 36638720 8384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8945 8384 603 41 0 8904 0
vsize: 35780
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8406 0 0 0 118990 23 0 0 25 0 1 0 420221357 36638720 8384 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8945 8384 603 41 0 8904 0
vsize: 35780
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 2130
Raw data (stat): 2130 (minisat+) R 2129 32461 32460 0 -1 0 8406 0 0 0 119990 23 0 0 25 0 1 0 420221357 36638720 8384 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8945 8384 603 41 0 8904 0
vsize: 35780
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.73 1/54 2130
Raw data (stat): 2130 (minisat+) Z 2129 32461 32460 0 -1 12 8408 0 0 0 119990 25 0 0 25 0 1 0 420221357 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.03
CPU time (s): 1200.16
CPU user time (s): 1199.91
CPU system time (s): 0.251961
CPU usage (%): 100.011
Max. virtual memory (Kb): 35780
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####