PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga40_38_sat_pb.cnf.cr.opb
MD5SUM	69d239b72e8d1a72f9c55329043493e1
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	41
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	15.9626
Number of variables	2280
Total number of constraints	1636
Number of constraints which are clauses	1558
Number of constraints which are cardinality constraints (but not clauses)	78
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	20
Maximum length of a constraint	40
Trace number 4647

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        866060 kB
Buffers:         33444 kB
Cached:          92948 kB
SwapCached:       3828 kB
Active:          46268 kB
Inactive:        86844 kB
HighTotal:      131008 kB
HighFree:        35700 kB
LowTotal:       903652 kB
LowFree:        830360 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            29972 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:48:06 (client local time) WITH STATUS 0 IN 1200.15 SECONDS
stats: 3436 7 1200.15 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1636 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  77]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  76]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  75]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  74]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  73]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  72]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  71]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  70]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  69]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  68]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  67]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  66]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  65]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  64]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  63]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  62]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  61]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  60]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  59]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  58]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  57]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  56]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  55]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  54]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  53]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  52]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  51]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  50]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  49]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  48]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  47]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  46]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  45]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  44]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  43]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  42]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  41]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  40]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  39]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  38]---> Adder-cost: 70   maxlim: 36   bits: 6/6
c ---[  37]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  36]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  35]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  34]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  33]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  32]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  31]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  30]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  29]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  28]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  27]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  26]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  25]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  24]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  23]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  22]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  21]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  20]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  19]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  18]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  17]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  16]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  15]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  14]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  13]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  12]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  11]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  10]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   9]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   8]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   7]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   6]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   5]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   4]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   3]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   2]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   1]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   0]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27130   122922 |    9043       0        0     nan |  0.000 % |
c |       101 |   27130   122922 |    9947     101      386     3.8 |  9.509 % |
c |       251 |   27092   122786 |   10942     245     1025     4.2 |  9.585 % |
c |       476 |   27050   122630 |   12036     464     2165     4.7 |  9.676 % |
c |       814 |   26975   122365 |   13239     789     3658     4.6 |  9.827 % |
c |      1320 |   26614   121076 |   14563    1240     5808     4.7 | 10.706 % |
c |      2079 |   25633   117675 |   16020    1847     8751     4.7 | 13.280 % |
c |      3219 |   23385   110021 |   17622    2575    12310     4.8 | 19.110 % |
c |      4929 |   18969    94975 |   19384    3454   172860    50.0 | 30.769 % |
c |      7491 |   17824    91055 |   21322    5791   733460   126.7 | 33.783 % |
c |     11335 |   17784    90918 |   23455    9628  2024861   210.3 | 33.873 % |
c |     17105 |   17374    89522 |   25800   15319  5040831   329.1 | 34.933 % |
c |     25755 |   16551    86703 |   28380   23790  8965336   376.9 | 37.068 % |
c |     38731 |   16316    85902 |   31218   16403  6885865   419.8 | 37.644 % |
c |     58192 |   15736    83934 |   34340   35762 16436461   459.6 | 39.143 % |
c |     87389 |   15446    82949 |   37774   14571 11840518   812.6 | 39.900 % |
c |    131178 |   15209    82145 |   41552   30057 26954590   896.8 | 40.506 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.00 0.00 0.00 2/54 30804
Raw data (stat): 30804 (runsolver) R 30803 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478466130 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.0005 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 982 0 1 0 983 3 0 0 25 0 1 0 478466130 5632000 961 4294967295 134512640 134672761 3221224528 3221223700 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1375 961 603 41 0 1334 0
vsize: 5500
[startup+20.0014 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 1722 0 1 0 1980 5 0 0 25 0 1 0 478466130 8613888 1701 4294967295 134512640 134672761 3221224528 3221223700 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2103 1701 603 41 0 2062 0
vsize: 8412
[startup+30.0019 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 3268 0 1 0 2977 9 0 0 25 0 1 0 478466130 14962688 3247 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3247 603 41 0 3612 0
vsize: 14612
[startup+40.0014 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 5542 0 1 0 3973 13 0 0 25 0 1 0 478466130 24268800 5521 4294967295 134512640 134672761 3221224528 3221223712 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5925 5521 603 41 0 5884 0
vsize: 23700
[startup+50.0014 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 6681 0 1 0 4970 16 0 0 25 0 1 0 478466130 29085696 6660 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7101 6660 603 41 0 7060 0
vsize: 28404
[startup+60.0018 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 7970 0 1 0 5967 19 0 0 25 0 1 0 478466130 34349056 7949 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8386 7949 603 41 0 8345 0
vsize: 33544
[startup+70.0014 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 9602 0 1 0 6963 23 0 0 25 0 1 0 478466130 40968192 9581 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10002 9582 603 41 0 9961 0
vsize: 40008
[startup+80.0025 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 12015 0 1 0 7957 29 0 0 25 0 1 0 478466130 50827264 11994 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12409 11994 603 41 0 12368 0
vsize: 49636
[startup+90.0031 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 12951 0 1 0 8955 32 0 0 25 0 1 0 478466130 54628352 12930 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13337 12930 603 41 0 13296 0
vsize: 53348
[startup+100.003 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 14091 0 1 0 9953 34 0 0 25 0 1 0 478466130 59359232 14070 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14492 14070 603 41 0 14451 0
vsize: 57968
[startup+110.004 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 15083 0 1 0 10950 38 0 0 25 0 1 0 478466130 63537152 15062 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15062 603 41 0 15471 0
vsize: 62048
[startup+120.004 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 15083 0 1 0 11950 38 0 0 25 0 1 0 478466130 63537152 15062 4294967295 134512640 134672761 3221224528 3221223652 134566045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15062 603 41 0 15471 0
vsize: 62048
[startup+130.005 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 15083 0 1 0 12950 38 0 0 25 0 1 0 478466130 63537152 15062 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15062 603 41 0 15471 0
vsize: 62048
[startup+140.005 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 15083 0 1 0 13950 38 0 0 25 0 1 0 478466130 63537152 15062 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15512 15062 603 41 0 15471 0
vsize: 62048
[startup+150.005 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 15083 0 1 0 14950 38 0 0 25 0 1 0 478466130 63537152 15062 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15062 603 41 0 15471 0
vsize: 62048
[startup+160.006 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 15083 0 1 0 15950 38 0 0 25 0 1 0 478466130 63537152 15062 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15062 603 41 0 15471 0
vsize: 62048
[startup+170.006 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 15083 0 1 0 16950 38 0 0 25 0 1 0 478466130 63537152 15062 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15512 15062 603 41 0 15471 0
vsize: 62048
[startup+180.006 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 15505 0 1 0 17950 38 0 0 25 0 1 0 478466130 65290240 15484 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15940 15484 603 41 0 15899 0
vsize: 63760
[startup+190.007 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 16593 0 1 0 18948 40 0 0 25 0 1 0 478466130 69742592 16572 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17027 16572 603 41 0 16986 0
vsize: 68108
[startup+200.006 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 17574 0 1 0 19946 43 0 0 25 0 1 0 478466130 73793536 17553 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18016 17553 603 41 0 17975 0
vsize: 72064
[startup+210.007 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 18534 0 1 0 20945 44 0 0 25 0 1 0 478466130 77762560 18513 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18985 18513 603 41 0 18944 0
vsize: 75940
[startup+220.007 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 18913 0 1 0 21943 45 0 0 25 0 1 0 478466130 79257600 18892 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19350 18892 603 41 0 19309 0
vsize: 77400
[startup+230.007 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 19823 0 1 0 22942 47 0 0 25 0 1 0 478466130 83034112 19802 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20272 19802 603 41 0 20231 0
vsize: 81088
[startup+240.007 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 19929 0 1 0 23941 48 0 0 25 0 1 0 478466130 83570688 19908 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20403 19908 603 41 0 20362 0
vsize: 81612
[startup+250.007 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 19929 0 1 0 24941 48 0 0 25 0 1 0 478466130 83570688 19908 4294967295 134512640 134672761 3221224528 3221223632 134555093 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20403 19908 603 41 0 20362 0
vsize: 81612
[startup+260.008 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 19929 0 1 0 25942 48 0 0 25 0 1 0 478466130 83570688 19908 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20403 19908 603 41 0 20362 0
vsize: 81612
[startup+270.007 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 19929 0 1 0 26942 48 0 0 25 0 1 0 478466130 83570688 19908 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20403 19908 603 41 0 20362 0
vsize: 81612
[startup+280.008 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 19929 0 1 0 27942 48 0 0 25 0 1 0 478466130 83570688 19908 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20403 19908 603 41 0 20362 0
vsize: 81612
[startup+290.009 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 19929 0 1 0 28942 48 0 0 25 0 1 0 478466130 83570688 19908 4294967295 134512640 134672761 3221224528 3221223712 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20403 19908 603 41 0 20362 0
vsize: 81612
[startup+300.008 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 20617 0 1 0 29941 49 0 0 25 0 1 0 478466130 86405120 20596 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21095 20596 603 41 0 21054 0
vsize: 84380
[startup+310.008 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 22648 0 1 0 30937 53 0 0 25 0 1 0 478466130 94666752 22627 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23112 22627 603 41 0 23071 0
vsize: 92448
[startup+320.009 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 24494 0 1 0 31933 57 0 0 25 0 1 0 478466130 102227968 24473 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24958 24473 603 41 0 24917 0
vsize: 99832
[startup+330.01 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 26867 0 1 0 32928 62 0 0 25 0 1 0 478466130 111923200 26846 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27325 26846 603 41 0 27284 0
vsize: 109300
[startup+340.009 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 28901 0 1 0 33924 67 0 0 25 0 1 0 478466130 120324096 28880 4294967295 134512640 134672761 3221224528 3221223696 134559063 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29376 28881 603 41 0 29335 0
vsize: 117504
[startup+350.009 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 30468 0 1 0 34921 70 0 0 25 0 1 0 478466130 126779392 30447 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30952 30447 603 41 0 30911 0
vsize: 123808
[startup+360.009 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 31701 0 1 0 35919 72 0 0 25 0 1 0 478466130 131751936 31680 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32166 31680 603 41 0 32125 0
vsize: 128664
[startup+370.009 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32677 0 1 0 36918 74 0 0 25 0 1 0 478466130 135770112 32656 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32656 603 41 0 33106 0
vsize: 132588
[startup+380.01 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 37918 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+390.011 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 38918 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+400.01 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 39918 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+410.011 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 40918 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+420.011 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 41918 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+430.012 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 42918 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+440.012 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 43919 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223712 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+450.012 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 44919 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+460.013 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 45919 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+470.012 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 46919 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+480.013 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 47919 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+490.013 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 48919 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+500.013 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 49920 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+510.013 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 50920 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+520.013 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 51920 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+530.013 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 52920 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+540.013 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 32678 0 1 0 53920 74 0 0 25 0 1 0 478466130 135770112 32657 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33147 32657 603 41 0 33106 0
vsize: 132588
[startup+550.013 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 33306 0 1 0 54918 76 0 0 25 0 1 0 478466130 138461184 33285 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33804 33285 603 41 0 33763 0
vsize: 135216
[startup+560.013 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 34092 0 1 0 55916 78 0 0 25 0 1 0 478466130 141697024 34071 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34594 34071 603 41 0 34553 0
vsize: 138376
[startup+570.013 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 35094 0 1 0 56914 81 0 0 25 0 1 0 478466130 145752064 35073 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35584 35073 603 41 0 35543 0
vsize: 142336
[startup+580.014 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 36034 0 1 0 57912 83 0 0 25 0 1 0 478466130 149643264 36013 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36534 36013 603 41 0 36493 0
vsize: 146136
[startup+590.014 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 36761 0 1 0 58911 85 0 0 25 0 1 0 478466130 152600576 36740 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37256 36740 603 41 0 37215 0
vsize: 149024
[startup+600.014 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37450 0 1 0 59910 86 0 0 25 0 1 0 478466130 155455488 37429 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37429 603 41 0 37912 0
vsize: 151812
[startup+610.014 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 60910 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+620.013 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 61910 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+630.013 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 62910 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+640.014 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 63910 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+650.013 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 64910 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+660.013 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 65910 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+670.013 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 66911 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+680.012 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 67911 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+690.012 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 68911 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+700.012 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 69911 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+710.013 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 70911 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+720.012 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 71911 86 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+730.012 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 72911 87 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+740.013 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 73911 87 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+750.013 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 74912 87 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+760.013 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 75912 87 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+770.013 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 76912 87 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+780.012 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 77912 87 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+790.012 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 78912 87 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+800.012 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37451 0 1 0 79912 87 0 0 25 0 1 0 478466130 155455488 37430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37430 603 41 0 37912 0
vsize: 151812
[startup+810.013 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37452 0 1 0 80912 87 0 0 25 0 1 0 478466130 155455488 37431 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37953 37431 603 41 0 37912 0
vsize: 151812
[startup+820.013 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37452 0 1 0 81912 87 0 0 25 0 1 0 478466130 155455488 37431 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37431 603 41 0 37912 0
vsize: 151812
[startup+830.013 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37453 0 1 0 82912 87 0 0 25 0 1 0 478466130 155455488 37432 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37432 603 41 0 37912 0
vsize: 151812
[startup+840.013 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37453 0 1 0 83912 87 0 0 25 0 1 0 478466130 155455488 37432 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37432 603 41 0 37912 0
vsize: 151812
[startup+850.013 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37453 0 1 0 84912 87 0 0 25 0 1 0 478466130 155455488 37432 4294967295 134512640 134672761 3221224528 3221223600 134553544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37432 603 41 0 37912 0
vsize: 151812
[startup+860.014 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37453 0 1 0 85912 87 0 0 25 0 1 0 478466130 155455488 37432 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37432 603 41 0 37912 0
vsize: 151812
[startup+870.014 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 37453 0 1 0 86912 87 0 0 25 0 1 0 478466130 155455488 37432 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37953 37432 603 41 0 37912 0
vsize: 151812
[startup+880.014 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 38353 0 1 0 87911 89 0 0 25 0 1 0 478466130 159088640 38332 4294967295 134512640 134672761 3221224528 3221223632 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38840 38332 603 41 0 38799 0
vsize: 155360
[startup+890.014 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 39601 0 1 0 88909 91 0 0 25 0 1 0 478466130 164175872 39580 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40082 39580 603 41 0 40041 0
vsize: 160328
[startup+900.014 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 40744 0 1 0 89907 93 0 0 25 0 1 0 478466130 168882176 40723 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41231 40723 603 41 0 41190 0
vsize: 164924
[startup+910.014 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 41696 0 1 0 90905 95 0 0 25 0 1 0 478466130 172777472 41675 4294967295 134512640 134672761 3221224528 3221223544 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42182 41675 603 41 0 42141 0
vsize: 168728
[startup+920.014 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 42864 0 1 0 91903 98 0 0 25 0 1 0 478466130 177614848 42843 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43363 42843 603 41 0 43322 0
vsize: 173452
[startup+930.014 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 43816 0 1 0 92901 100 0 0 25 0 1 0 478466130 181526528 43795 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44318 43795 603 41 0 44277 0
vsize: 177272
[startup+940.015 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44777 0 1 0 93900 101 0 0 25 0 1 0 478466130 185421824 44756 4294967295 134512640 134672761 3221224528 3221223632 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44756 603 41 0 45228 0
vsize: 181076
[startup+950.014 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44777 0 1 0 94900 101 0 0 25 0 1 0 478466130 185421824 44756 4294967295 134512640 134672761 3221224528 3221223632 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44756 603 41 0 45228 0
vsize: 181076
[startup+960.015 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44777 0 1 0 95900 102 0 0 25 0 1 0 478466130 185421824 44756 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44756 603 41 0 45228 0
vsize: 181076
[startup+970.015 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44777 0 1 0 96900 102 0 0 25 0 1 0 478466130 185421824 44756 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44756 603 41 0 45228 0
vsize: 181076
[startup+980.014 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44777 0 1 0 97900 102 0 0 25 0 1 0 478466130 185421824 44756 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44756 603 41 0 45228 0
vsize: 181076
[startup+990.015 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44777 0 1 0 98900 102 0 0 25 0 1 0 478466130 185421824 44756 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44756 603 41 0 45228 0
vsize: 181076
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44777 0 1 0 99900 102 0 0 25 0 1 0 478466130 185421824 44756 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44756 603 41 0 45228 0
vsize: 181076
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44777 0 1 0 100900 102 0 0 25 0 1 0 478466130 185421824 44756 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44756 603 41 0 45228 0
vsize: 181076
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44778 0 1 0 101901 102 0 0 25 0 1 0 478466130 185421824 44757 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44757 603 41 0 45228 0
vsize: 181076
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44778 0 1 0 102901 102 0 0 25 0 1 0 478466130 185421824 44757 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44757 603 41 0 45228 0
vsize: 181076
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44779 0 1 0 103901 102 0 0 25 0 1 0 478466130 185421824 44758 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44758 603 41 0 45228 0
vsize: 181076
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44779 0 1 0 104901 102 0 0 25 0 1 0 478466130 185421824 44758 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44758 603 41 0 45228 0
vsize: 181076
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44779 0 1 0 105901 102 0 0 25 0 1 0 478466130 185421824 44758 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44758 603 41 0 45228 0
vsize: 181076
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 106902 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 107902 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 108902 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 109902 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 110902 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 111902 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 112902 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 113903 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 114903 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 115903 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 116903 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 117903 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 118904 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 30804
Raw data (stat): 30804 (minisat+) R 30803 28546 28545 0 -1 0 44780 0 1 0 119904 102 0 0 25 0 1 0 478466130 185421824 44759 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45269 44759 603 41 0 45228 0
vsize: 181076
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 30804
Raw data (stat): 30804 (minisat+) Z 30803 28546 28545 0 -1 12 44782 0 1 0 119904 111 0 0 25 0 1 0 478466130 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.1
CPU time (s): 1200.15
CPU user time (s): 1199.04
CPU system time (s): 1.11183
CPU usage (%): 100.004
Max. virtual memory (Kb): 181076
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####