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-chnl50_55_pb.cnf.cr.opb
MD5SUM	88aaed929c30a489c8806c3852596de3
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	56
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.173973
Number of variables	5500
Total number of constraints	210
Number of constraints which are clauses	110
Number of constraints which are cardinality constraints (but not clauses)	100
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	50
Maximum length of a constraint	55
Trace number 4812

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        918292 kB
Buffers:         36616 kB
Cached:          60624 kB
SwapCached:          0 kB
Active:          71984 kB
Inactive:        28156 kB
HighTotal:      131008 kB
HighFree:        66360 kB
LowTotal:       903652 kB
LowFree:        851932 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10668 kB
Committed_AS:    63516 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:43:58 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 185 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 210 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................
c ---[  99]---> BDD-cost:  107
c ---[  98]---> BDD-cost:  107
c ---[  97]---> BDD-cost:  107
c ---[  96]---> BDD-cost:  107
c ---[  95]---> BDD-cost:  107
c ---[  94]---> BDD-cost:  107
c ---[  93]---> BDD-cost:  107
c ---[  92]---> BDD-cost:  107
c ---[  91]---> BDD-cost:  107
c ---[  90]---> BDD-cost:  107
c ---[  89]---> BDD-cost:  107
c ---[  88]---> BDD-cost:  107
c ---[  87]---> BDD-cost:  107
c ---[  86]---> BDD-cost:  107
c ---[  85]---> BDD-cost:  107
c ---[  84]---> BDD-cost:  107
c ---[  83]---> BDD-cost:  107
c ---[  82]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  107
c ---[  80]---> BDD-cost:  107
c ---[  79]---> BDD-cost:  107
c ---[  78]---> BDD-cost:  107
c ---[  77]---> BDD-cost:  107
c ---[  76]---> BDD-cost:  107
c ---[  75]---> BDD-cost:  107
c ---[  74]---> BDD-cost:  107
c ---[  73]---> BDD-cost:  107
c ---[  72]---> BDD-cost:  107
c ---[  71]---> BDD-cost:  107
c ---[  70]---> BDD-cost:  107
c ---[  69]---> BDD-cost:  107
c ---[  68]---> BDD-cost:  107
c ---[  67]---> BDD-cost:  107
c ---[  66]---> BDD-cost:  107
c ---[  65]---> BDD-cost:  107
c ---[  64]---> BDD-cost:  107
c ---[  63]---> BDD-cost:  107
c ---[  62]---> BDD-cost:  107
c ---[  61]---> BDD-cost:  107
c ---[  60]---> BDD-cost:  107
c ---[  59]---> BDD-cost:  107
c ---[  58]---> BDD-cost:  107
c ---[  57]---> BDD-cost:  107
c ---[  56]---> BDD-cost:  107
c ---[  55]---> BDD-cost:  107
c ---[  54]---> BDD-cost:  107
c ---[  53]---> BDD-cost:  107
c ---[  52]---> BDD-cost:  107
c ---[  51]---> BDD-cost:  107
c ---[  50]---> BDD-cost:  107
c ---[  49]---> BDD-cost:  107
c ---[  48]---> BDD-cost:  107
c ---[  47]---> BDD-cost:  107
c ---[  46]---> BDD-cost:  107
c ---[  45]---> BDD-cost:  107
c ---[  44]---> BDD-cost:  107
c ---[  43]---> BDD-cost:  107
c ---[  42]---> BDD-cost:  107
c ---[  41]---> BDD-cost:  107
c ---[  40]---> BDD-cost:  107
c ---[  39]---> BDD-cost:  107
c ---[  38]---> BDD-cost:  107
c ---[  37]---> BDD-cost:  107
c ---[  36]---> BDD-cost:  107
c ---[  35]---> BDD-cost:  107
c ---[  34]---> BDD-cost:  107
c ---[  33]---> BDD-cost:  107
c ---[  32]---> BDD-cost:  107
c ---[  31]---> BDD-cost:  107
c ---[  30]---> BDD-cost:  107
c ---[  29]---> BDD-cost:  107
c ---[  28]---> BDD-cost:  107
c ---[  27]---> BDD-cost:  107
c ---[  26]---> BDD-cost:  107
c ---[  25]---> BDD-cost:  107
c ---[  24]---> BDD-cost:  107
c ---[  23]---> BDD-cost:  107
c ---[  22]---> BDD-cost:  107
c ---[  21]---> BDD-cost:  107
c ---[  20]---> BDD-cost:  107
c ---[  19]---> BDD-cost:  107
c ---[  18]---> BDD-cost:  107
c ---[  17]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  107
c ---[  15]---> BDD-cost:  107
c ---[  14]---> BDD-cost:  107
c ---[  13]---> BDD-cost:  107
c ---[  12]---> BDD-cost:  107
c ---[  11]---> BDD-cost:  107
c ---[  10]---> BDD-cost:  107
c ---[   9]---> BDD-cost:  107
c ---[   8]---> BDD-cost:  107
c ---[   7]---> BDD-cost:  107
c ---[   6]---> BDD-cost:  107
c ---[   5]---> BDD-cost:  107
c ---[   4]---> BDD-cost:  107
c ---[   3]---> BDD-cost:  107
c ---[   2]---> BDD-cost:  107
c ---[   1]---> BDD-cost:  107
c ---[   0]---> BDD-cost:  107
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   26710    74700 |    8903       0        0     nan |  0.000 % |
c |       101 |   26710    74700 |    9793     101    19540   193.5 |  0.617 % |
c |       254 |   26710    74700 |   10772     254    57136   224.9 |  0.617 % |
c |       479 |   26710    74700 |   11849     479   106928   223.2 |  0.617 % |
c |       820 |   26710    74700 |   13034     820   228012   278.1 |  0.617 % |
c |      1327 |   26710    74700 |   14338    1327   407337   307.0 |  0.617 % |
c |      2089 |   26710    74700 |   15772    2089   607183   290.7 |  0.617 % |
c |      3232 |   26710    74700 |   17349    3232   926679   286.7 |  0.617 % |
c |      4943 |   26710    74700 |   19084    4943  1483658   300.2 |  0.617 % |
c |      7507 |   26710    74700 |   20992    7507  2510030   334.4 |  0.617 % |
c |     11351 |   26710    74700 |   23092   11351  4018398   354.0 |  0.617 % |
c |     17118 |   26710    74700 |   25401   17118  7441464   434.7 |  0.617 % |
c |     25771 |   26710    74700 |   27941   25771 13547867   525.7 |  0.617 % |
c |     38747 |   26710    74700 |   30735   11992  5242030   437.1 |  0.617 % |
c |     58209 |   26710    74700 |   33809   31454 12687777   403.4 |  0.617 % |
c |     87404 |   26710    74700 |   37190   27207 15612638   573.8 |  0.617 % |
c |    131194 |   26710    74700 |   40909   35274 17941262   508.6 |  0.617 % |
#### 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.92 0.97 0.91 2/54 25174
Raw data (stat): 25174 (runsolver) R 25173 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420587987 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0005 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 3351 0 0 0 990 8 0 0 25 0 1 0 420587987 15249408 3283 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3723 3283 603 41 0 3682 0
vsize: 14892
[startup+19.9998 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 4908 0 0 0 1985 12 0 0 25 0 1 0 420587987 21569536 4840 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5266 4840 603 41 0 5225 0
vsize: 21064
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 6541 0 0 0 2981 16 0 0 25 0 1 0 420587987 28188672 6473 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6882 6473 603 41 0 6841 0
vsize: 27528
[startup+40.0004 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 7892 0 0 0 3978 20 0 0 25 0 1 0 420587987 33718272 7824 4294967295 134512640 134672761 3221224624 3221223728 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8232 7824 603 41 0 8191 0
vsize: 32928
[startup+50.0006 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 9128 0 0 0 4974 24 0 0 25 0 1 0 420587987 38871040 9060 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9490 9060 603 41 0 9449 0
vsize: 37960
[startup+60.0007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 10558 0 0 0 5970 28 0 0 25 0 1 0 420587987 44814336 10490 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10941 10490 603 41 0 10900 0
vsize: 43764
[startup+70.0003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 11797 0 0 0 6967 31 0 0 25 0 1 0 420587987 49815552 11729 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12162 11729 603 41 0 12121 0
vsize: 48648
[startup+80.0006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 12882 0 0 0 7965 33 0 0 25 0 1 0 420587987 54280192 12814 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13252 12814 603 41 0 13211 0
vsize: 53008
[startup+90.0005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 13918 0 0 0 8962 36 0 0 25 0 1 0 420587987 58511360 13850 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14285 13850 603 41 0 14244 0
vsize: 57140
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 14790 0 0 0 9961 37 0 0 25 0 1 0 420587987 62017536 14722 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15141 14722 603 41 0 15100 0
vsize: 60564
[startup+110.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 16132 0 0 0 10958 41 0 0 25 0 1 0 420587987 67571712 16064 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16497 16064 603 41 0 16456 0
vsize: 65988
[startup+120.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 18263 0 0 0 11953 46 0 0 25 0 1 0 420587987 76320768 18195 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18633 18196 603 41 0 18592 0
vsize: 74532
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 19448 0 0 0 12950 48 0 0 25 0 1 0 420587987 81305600 19380 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19850 19380 603 41 0 19809 0
vsize: 79400
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 20653 0 0 0 13948 51 0 0 25 0 1 0 420587987 86306816 20585 4294967295 134512640 134672761 3221224624 3221223808 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21071 20585 603 41 0 21030 0
vsize: 84284
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21485 0 0 0 14947 53 0 0 25 0 1 0 420587987 89714688 21417 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21903 21417 603 41 0 21862 0
vsize: 87612
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21827 0 0 0 15946 53 0 0 25 0 1 0 420587987 91082752 21759 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21827 0 0 0 16946 53 0 0 25 0 1 0 420587987 91082752 21759 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21827 0 0 0 17946 53 0 0 25 0 1 0 420587987 91082752 21759 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21827 0 0 0 18947 53 0 0 25 0 1 0 420587987 91082752 21759 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21827 0 0 0 19947 53 0 0 25 0 1 0 420587987 91082752 21759 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21827 0 0 0 20947 53 0 0 25 0 1 0 420587987 91082752 21759 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21827 0 0 0 21947 53 0 0 25 0 1 0 420587987 91082752 21759 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21827 0 0 0 22947 53 0 0 25 0 1 0 420587987 91082752 21759 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21827 0 0 0 23948 53 0 0 25 0 1 0 420587987 91082752 21759 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21827 0 0 0 24947 53 0 0 25 0 1 0 420587987 91082752 21759 4294967295 134512640 134672761 3221224624 3221223728 134559796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21827 0 0 0 25948 53 0 0 25 0 1 0 420587987 91082752 21759 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21828 0 0 0 26948 53 0 0 25 0 1 0 420587987 91082752 21760 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21760 603 41 0 22196 0
vsize: 88948
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21829 0 0 0 27948 53 0 0 25 0 1 0 420587987 91082752 21761 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21761 603 41 0 22196 0
vsize: 88948
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 21830 0 0 0 28948 53 0 0 25 0 1 0 420587987 91082752 21762 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21762 603 41 0 22196 0
vsize: 88948
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 22185 0 0 0 29947 54 0 0 25 0 1 0 420587987 92569600 22117 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22600 22117 603 41 0 22559 0
vsize: 90400
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23122 0 0 0 30945 57 0 0 25 0 1 0 420587987 96374784 23054 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23529 23054 603 41 0 23488 0
vsize: 94116
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23554 0 0 0 31944 58 0 0 25 0 1 0 420587987 98140160 23486 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23486 603 41 0 23919 0
vsize: 95840
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23556 0 0 0 32944 58 0 0 25 0 1 0 420587987 98140160 23488 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23488 603 41 0 23919 0
vsize: 95840
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23556 0 0 0 33944 58 0 0 25 0 1 0 420587987 98140160 23488 4294967295 134512640 134672761 3221224624 3221223728 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23488 603 41 0 23919 0
vsize: 95840
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23557 0 0 0 34944 58 0 0 25 0 1 0 420587987 98140160 23489 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23489 603 41 0 23919 0
vsize: 95840
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23557 0 0 0 35944 58 0 0 25 0 1 0 420587987 98140160 23489 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23489 603 41 0 23919 0
vsize: 95840
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23559 0 0 0 36945 58 0 0 25 0 1 0 420587987 98140160 23491 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23491 603 41 0 23919 0
vsize: 95840
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23559 0 0 0 37945 58 0 0 25 0 1 0 420587987 98140160 23491 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23491 603 41 0 23919 0
vsize: 95840
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23559 0 0 0 38945 58 0 0 25 0 1 0 420587987 98140160 23491 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23491 603 41 0 23919 0
vsize: 95840
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23560 0 0 0 39945 58 0 0 25 0 1 0 420587987 98140160 23492 4294967295 134512640 134672761 3221224624 3221223808 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23492 603 41 0 23919 0
vsize: 95840
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23560 0 0 0 40945 58 0 0 25 0 1 0 420587987 98140160 23492 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23492 603 41 0 23919 0
vsize: 95840
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23560 0 0 0 41946 58 0 0 25 0 1 0 420587987 98140160 23492 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23492 603 41 0 23919 0
vsize: 95840
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23560 0 0 0 42946 58 0 0 25 0 1 0 420587987 98140160 23492 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23492 603 41 0 23919 0
vsize: 95840
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23560 0 0 0 43946 58 0 0 25 0 1 0 420587987 98140160 23492 4294967295 134512640 134672761 3221224624 3221223728 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23492 603 41 0 23919 0
vsize: 95840
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23561 0 0 0 44946 58 0 0 25 0 1 0 420587987 98140160 23493 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23493 603 41 0 23919 0
vsize: 95840
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23561 0 0 0 45946 59 0 0 25 0 1 0 420587987 98140160 23493 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23493 603 41 0 23919 0
vsize: 95840
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23561 0 0 0 46946 59 0 0 25 0 1 0 420587987 98140160 23493 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23493 603 41 0 23919 0
vsize: 95840
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23561 0 0 0 47946 59 0 0 25 0 1 0 420587987 98140160 23493 4294967295 134512640 134672761 3221224624 3221223728 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23493 603 41 0 23919 0
vsize: 95840
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 23804 0 0 0 48946 59 0 0 25 0 1 0 420587987 99221504 23736 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24224 23736 603 41 0 24183 0
vsize: 96896
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 24816 0 0 0 49943 62 0 0 25 0 1 0 420587987 103272448 24748 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25213 24748 603 41 0 25172 0
vsize: 100852
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 25760 0 0 0 50941 64 0 0 25 0 1 0 420587987 107192320 25692 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26170 25692 603 41 0 26129 0
vsize: 104680
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 26590 0 0 0 51939 67 0 0 25 0 1 0 420587987 110702592 26522 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27027 26522 603 41 0 26986 0
vsize: 108108
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 27457 0 0 0 52937 69 0 0 25 0 1 0 420587987 114225152 27389 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27887 27389 603 41 0 27846 0
vsize: 111548
[startup+540.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 28269 0 0 0 53933 72 0 0 25 0 1 0 420587987 117628928 28201 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28718 28201 603 41 0 28677 0
vsize: 114872
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29018 0 0 0 54932 74 0 0 25 0 1 0 420587987 120741888 28950 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29478 28950 603 41 0 29437 0
vsize: 117912
[startup+560.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29609 0 0 0 55930 76 0 0 25 0 1 0 420587987 123183104 29541 4294967295 134512640 134672761 3221224624 3221223728 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29541 603 41 0 30033 0
vsize: 120296
[startup+570.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29609 0 0 0 56930 76 0 0 25 0 1 0 420587987 123183104 29541 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29541 603 41 0 30033 0
vsize: 120296
[startup+580.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29615 0 0 0 57931 76 0 0 25 0 1 0 420587987 123183104 29547 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29547 603 41 0 30033 0
vsize: 120296
[startup+590.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29617 0 0 0 58931 76 0 0 25 0 1 0 420587987 123183104 29549 4294967295 134512640 134672761 3221224624 3221223808 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29549 603 41 0 30033 0
vsize: 120296
[startup+600.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29617 0 0 0 59931 76 0 0 25 0 1 0 420587987 123183104 29549 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29549 603 41 0 30033 0
vsize: 120296
[startup+610.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29617 0 0 0 60931 76 0 0 25 0 1 0 420587987 123183104 29549 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29549 603 41 0 30033 0
vsize: 120296
[startup+620.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29617 0 0 0 61931 76 0 0 25 0 1 0 420587987 123183104 29549 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29549 603 41 0 30033 0
vsize: 120296
[startup+630.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29617 0 0 0 62932 76 0 0 25 0 1 0 420587987 123183104 29549 4294967295 134512640 134672761 3221224624 3221223728 134560019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29549 603 41 0 30033 0
vsize: 120296
[startup+640.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29617 0 0 0 63932 76 0 0 25 0 1 0 420587987 123183104 29549 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29549 603 41 0 30033 0
vsize: 120296
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29617 0 0 0 64932 76 0 0 25 0 1 0 420587987 123183104 29549 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29549 603 41 0 30033 0
vsize: 120296
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29617 0 0 0 65932 76 0 0 25 0 1 0 420587987 123183104 29549 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29549 603 41 0 30033 0
vsize: 120296
[startup+670.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29618 0 0 0 66932 76 0 0 25 0 1 0 420587987 123183104 29550 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29550 603 41 0 30033 0
vsize: 120296
[startup+680.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29623 0 0 0 67933 76 0 0 25 0 1 0 420587987 123183104 29555 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29555 603 41 0 30033 0
vsize: 120296
[startup+690.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29628 0 0 0 68933 76 0 0 25 0 1 0 420587987 123183104 29560 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+700.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29628 0 0 0 69933 76 0 0 25 0 1 0 420587987 123183104 29560 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+710.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29628 0 0 0 70933 76 0 0 25 0 1 0 420587987 123183104 29560 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+720.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29628 0 0 0 71933 76 0 0 25 0 1 0 420587987 123183104 29560 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+730.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29628 0 0 0 72933 76 0 0 25 0 1 0 420587987 123183104 29560 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+740.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29628 0 0 0 73934 76 0 0 25 0 1 0 420587987 123183104 29560 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+750.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29629 0 0 0 74934 76 0 0 25 0 1 0 420587987 123183104 29561 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29561 603 41 0 30033 0
vsize: 120296
[startup+760.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29629 0 0 0 75934 76 0 0 25 0 1 0 420587987 123183104 29561 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29561 603 41 0 30033 0
vsize: 120296
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29629 0 0 0 76934 76 0 0 25 0 1 0 420587987 123183104 29561 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30074 29561 603 41 0 30033 0
vsize: 120296
[startup+780.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29629 0 0 0 77933 76 0 0 25 0 1 0 420587987 123183104 29561 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29561 603 41 0 30033 0
vsize: 120296
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29629 0 0 0 78934 76 0 0 25 0 1 0 420587987 123183104 29561 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29561 603 41 0 30033 0
vsize: 120296
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29629 0 0 0 79934 76 0 0 25 0 1 0 420587987 123183104 29561 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29561 603 41 0 30033 0
vsize: 120296
[startup+810.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29629 0 0 0 80934 76 0 0 25 0 1 0 420587987 123183104 29561 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29561 603 41 0 30033 0
vsize: 120296
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29629 0 0 0 81934 76 0 0 25 0 1 0 420587987 123183104 29561 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29561 603 41 0 30033 0
vsize: 120296
[startup+830.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29630 0 0 0 82934 76 0 0 25 0 1 0 420587987 123183104 29562 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29562 603 41 0 30033 0
vsize: 120296
[startup+840.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29631 0 0 0 83935 76 0 0 25 0 1 0 420587987 123183104 29563 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29563 603 41 0 30033 0
vsize: 120296
[startup+850.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 84935 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+860.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 85935 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+870.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 86935 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+880.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 87935 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+890.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 88936 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+900.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 89936 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+910.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 90936 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+920.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 91936 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+930.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 92936 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+940.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 93937 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+950.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 94937 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+960.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 95937 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+970.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 96937 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+980.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 97937 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+990.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 98937 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 99938 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 100938 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 101938 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 102938 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 103939 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 104939 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 105939 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 106939 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 107939 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 108940 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 109940 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 110940 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223728 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 111940 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 112940 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 113941 76 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 114941 77 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 115941 77 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 116941 77 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 117941 77 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 118941 77 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25174
Raw data (stat): 25174 (minisat+) R 25173 22932 22931 0 -1 0 29632 0 0 0 119942 77 0 0 25 0 1 0 420587987 122654720 29459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29459 603 41 0 29904 0
vsize: 119780
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25174
Raw data (stat): 25174 (minisat+) Z 25173 22932 22931 0 -1 12 29634 0 0 0 119942 82 0 0 25 0 1 0 420587987 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.07
CPU time (s): 1200.25
CPU user time (s): 1199.42
CPU system time (s): 0.825874
CPU usage (%): 100.015
Max. virtual memory (Kb): 120296
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####