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/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-mkc.opb
MD5SUM	44934b498b6e9897bcf8e950d9d30136
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
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	2946
Biggest coefficient in the objective function	20000
Number of bits for the biggest coefficient in the objective function	15
Sum of the numbers in the objective function	31442101
Number of bits of the sum of numbers in the objective function	25
Biggest number in a constraint	65536000
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	629010691
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.11
Number of variables	5363
Total number of constraints	8734
Number of constraints which are clauses	2977
Number of constraints which are cardinality constraints (but not clauses)	5731
Number of constraints which are nor clauses,nor cardinality constraints	26
Minimum length of a constraint	1
Maximum length of a constraint	2942
Trace number 18642

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 15:55:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17703 boxname=wulflinc19 idbench=1362 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  44934b498b6e9897bcf8e950d9d30136  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-mkc.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-mkc.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-mkc.opb
IDLAUNCH: 17703
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        715536 kB
Buffers:         25388 kB
Cached:         269108 kB
SwapCached:        556 kB
Active:          41716 kB
Inactive:       254848 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        715284 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5164 kB
Slab:            16908 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 16:15:39 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 17703 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3225 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[3223]---> Adder-cost: 26498   maxlim: 479706816   bits: 29/29
c ---[3222]---> Adder-cost: 1604   maxlim: 1898736   bits: 21/21
c ---[3221]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[3210]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[3199]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[3188]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[3177]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[3138]---> Adder-cost: 304   maxlim: 153   bits: 8/8
c ---[3135]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[3114]---> Adder-cost: 1804   maxlim: 2264275   bits: 22/22
c ---[3113]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[3102]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[3091]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[3080]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[3069]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[3058]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[3037]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[3026]---> Adder-cost: 20   maxlim: 13   bits: 4/4
c ---[3015]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[3004]---> Adder-cost: 1870   maxlim: 2337035   bits: 22/22
c ---[3003]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[2992]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[2981]---> Adder-cost: 16   maxlim: 14   bits: 5/4
c ---[2970]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2959]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[2948]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[2930]---> Adder-cost: 322   maxlim: 161   bits: 8/8
c ---[2927]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2916]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2905]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2894]---> Adder-cost: 1342   maxlim: 1417292   bits: 21/21
c ---[2893]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2872]---> Adder-cost: 14   maxlim: 10   bits: 4/4
c ---[2839]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2828]---> Adder-cost: 8   maxlim: 9   bits: 4/4
c ---[2796]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[2785]---> Adder-cost: 1248   maxlim: 1408937   bits: 21/21
c ---[2784]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2773]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2752]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2741]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2730]---> Adder-cost: 18   maxlim: 14   bits: 5/4
c ---[2711]---> Adder-cost: 304   maxlim: 153   bits: 8/8
c ---[2699]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2688]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[2677]---> Adder-cost: 1438   maxlim: 1767687   bits: 21/21
c ---[2665]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2654]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2632]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2621]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2610]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[2589]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[2568]---> Adder-cost: 1090   maxlim: 131883   bits: 18/18
c ---[2567]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2524]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2505]---> Adder-cost: 304   maxlim: 153   bits: 8/8
c ---[2503]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[2472]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2461]---> Adder-cost: 822   maxlim: 923028   bits: 20/20
c ---[2460]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2438]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2367]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2356]---> Adder-cost: 664   maxlim: 77334   bits: 17/17
c ---[2355]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2324]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2305]---> Adder-cost: 304   maxlim: 153   bits: 8/8
c ---[2283]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2261]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2250]---> Adder-cost: 288   maxlim: 35124   bits: 16/16
c ---[2239]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[2218]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[2207]---> Adder-cost: 4   maxlim: 3   bits: 3/2
c ---[2196]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[2166]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2143]---> Adder-cost: 477   maxlim: 2053920   bits: 22/21
c ---[2142]---> Adder-cost: 166   maxlim: 9439   bits: 14/14
c ---[2141]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2130]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2119]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2108]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2099]---> Adder-cost: 348   maxlim: 175   bits: 8/8
c ---[2097]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2086]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2075]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2033]---> Adder-cost: 250   maxlim: 226108   bits: 19/18
c ---[2011]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2000]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1989]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1978]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1967]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1946]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1935]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[1924]---> Adder-cost: 190   maxlim: 180458   bits: 18/18
c ---[1923]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1912]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1880]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1869]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1865]---> Adder-cost: 362   maxlim: 183   bits: 8/8
c ---[1858]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1848]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1827]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1816]---> Adder-cost: 144   maxlim: 136658   bits: 18/18
c ---[1815]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1794]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1773]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1752]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1741]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1712]---> Adder-cost: 122   maxlim: 7109   bits: 14/13
c ---[1711]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1693]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1672]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1661]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1650]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1639]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1628]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1627]---> Adder-cost: 322   maxlim: 162   bits: 8/8
c ---[1612]---> Adder-cost: 78   maxlim: 8644   bits: 14/14
c ---[1611]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1602]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1594]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1577]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1558]---> Adder-cost: 8   maxlim: 9   bits: 4/4
c ---[1547]---> Adder-cost: 4   maxlim: 7   bits: 4/3
c ---[1526]---> Adder-cost: 56   maxlim: 1713   bits: 12/11
c ---[1518]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[1513]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1482]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1462]---> Adder-cost: 220   maxlim: 111   bits: 7/7
c ---[1451]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1430]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1339]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1338]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1327]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1316]---> Adder-cost: 274   maxlim: 138   bits: 8/8
c ---[1306]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1295]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1284]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1273]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1262]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1251]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1240]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1229]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1218]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1207]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1196]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1185]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1163]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1152]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1141]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1130]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1128]---> Adder-cost: 170   maxlim: 86   bits: 7/7
c ---[1119]---> Adder-cost: 2340   maxlim: 3201964   bits: 22/22
c ---[1118]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1117]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1106]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1095]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1084]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1073]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1062]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1051]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1019]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1008]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1007]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 996]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 988]---> Adder-cost: 140   maxlim: 70   bits: 7/7
c ---[ 985]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 974]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 963]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 952]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 931]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 920]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 909]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 891]---> Adder-cost: 106   maxlim: 53   bits: 6/6
c ---[ 888]---> Adder-cost: 8   maxlim: 13   bits: 4/4
c ---[ 877]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 866]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 855]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 844]---> Adder-cost: 12   maxlim: 11   bits: 4/4
c ---[ 814]---> Adder-cost: 44   maxlim: 21   bits: 5/5
c ---[ 813]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 802]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 790]---> Adder-cost: 20   maxlim: 14   bits: 5/4
c ---[ 780]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 779]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 761]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[ 739]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 738]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 727]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 719]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 704]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 695]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 689]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 684]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 683]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 678]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 672]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 669]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 666]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 664]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 663]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 662]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 661]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 660]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 659]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 658]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 657]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 656]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 655]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 654]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 653]---> Adder-cost: 8   maxlim: 9   bits: 4/4
c ---[ 652]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 651]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 650]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 649]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 648]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 647]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 644]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 643]---> Adder-cost: 12   maxlim: 13   bits: 4/4
c ---[ 642]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 641]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 640]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 639]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 637]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 636]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 635]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 634]---> Adder-cost: 4   maxlim: 7   bits: 4/3
c ---[ 633]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 628]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 627]---> Adder-cost: 1130   maxlim: 1417320   bits: 21/21
c ---[ 626]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 625]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 624]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 623]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 622]---> Adder-cost: 18   maxlim: 14   bits: 5/4
c ---[ 621]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 620]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 619]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 618]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 616]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 615]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 614]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 613]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 612]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 611]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 610]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 609]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 608]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 607]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 606]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 604]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 603]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 602]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 601]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 600]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 598]---> Adder-cost: 12   maxlim: 11   bits: 4/4
c ---[ 597]---> Adder-cost: 8   maxlim: 9   bits: 4/4
c ---[ 596]---> Adder-cost: 18   maxlim: 14   bits: 5/4
c ---[ 595]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 594]---> Adder-cost: 10   maxlim: 11   bits: 4/4
c ---[ 593]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 592]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 591]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 590]---> Adder-cost: 8   maxlim: 13   bits: 4/4
c ---[ 584]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 581]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 580]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 579]---> Adder-cost: 432   maxlim: 219   bits: 8/8
c ---[ 575]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 554]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 543]---> Adder-cost: 1584   maxlim: 1898736   bits: 21/21
c ---[ 542]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 477]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 466]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 444]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 433]---> Adder-cost: 1568   maxlim: 1898736   bits: 21/21
c ---[ 422]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 400]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 378]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 367]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 356]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 345]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 324]---> Adder-cost: 1704   maxlim: 2180627   bits: 22/22
c ---[ 312]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 279]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 268]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 260]---> Adder-cost: 202   maxlim: 101   bits: 7/7
c ---[ 246]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 235]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 224]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 213]---> Adder-cost: 1576   maxlim: 1898736   bits: 21/21
c ---[ 212]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[ 201]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 190]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 179]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 158]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 118]---> Adder-cost: 304   maxlim: 153   bits: 8/8
c ---[ 115]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 1630   maxlim: 1978736   bits: 21/21
c ---[  83]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[  72]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  61]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  40]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  412890  1468626 |  137630       0        0     nan |  0.000 % |
c |       100 |  412850  1468492 |  151393      95      303     3.2 |  2.596 % |
c |       250 |  412426  1467011 |  166532     188      618     3.3 |  2.713 % |
c |       475 |  412408  1466945 |  183185     411     1425     3.5 |  2.718 % |
c |       812 |  412305  1466594 |  201504     732     3045     4.2 |  2.743 % |
c |      1318 |  412290  1466541 |  221654    1237     5943     4.8 |  2.748 % |
c |      2077 |  412136  1466019 |  243819    1970    10794     5.5 |  2.784 % |
c |      3218 |  412097  1465886 |  268201    3102    63039    20.3 |  2.793 % |
c |      4927 |  411655  1464353 |  295022    4747   176053    37.1 |  2.907 % |
c |      7489 |  411027  1462189 |  324524    7222   218469    30.3 |  3.074 % |
c |     11333 |  410125  1459020 |  356976   10944   328235    30.0 |  3.271 % |
c |     17099 |  409967  1458472 |  392674   16685   593574    35.6 |  3.302 % |
c |     25748 |  409207  1455849 |  431941   25237   914517    36.2 |  3.472 % |
c |     38723 |  408894  1454762 |  475136   38161  1646510    43.1 |  3.549 % |
c |     58186 |  407088  1448465 |  522649   56889  2419373    42.5 |  3.972 % |
c |     87378 |  406446  1446263 |  574914   85967  3701932    43.1 |  4.120 % |
c |    131167 |  405114  1441676 |  632406  129437  5751544    44.4 |  4.432 % |
c |    196854 |  403326  1435512 |  695646  193200  8360169    43.3 |  4.855 % |
c |    295380 |  401531  1429332 |  765211  291477 13208176    45.3 |  5.276 % |
#### 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.79 0.93 0.91 2/55 2547
Raw data (stat): 2547 (runsolver) R 2546 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546319107 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.82 0.93 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 7679 0 0 0 981 17 0 0 25 0 1 0 546319107 37572608 7513 4294967295 134512640 134672761 3221224544 3221223648 134560285 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9173 7513 603 41 0 9132 0
vsize: 36692
[startup+20.0007 s]
Raw data (loadavg): 0.85 0.93 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 7763 0 0 0 1981 17 0 0 25 0 1 0 546319107 37978112 7597 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9272 7597 603 41 0 9231 0
vsize: 37088
[startup+30.0013 s]
Raw data (loadavg): 0.87 0.93 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 8037 0 0 0 2981 17 0 0 25 0 1 0 546319107 39104512 7871 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9547 7871 603 41 0 9506 0
vsize: 38188
[startup+40.001 s]
Raw data (loadavg): 0.89 0.93 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 8440 0 0 0 3979 18 0 0 25 0 1 0 546319107 40697856 8274 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9936 8275 603 41 0 9895 0
vsize: 39744
[startup+50.0013 s]
Raw data (loadavg): 0.91 0.94 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 8511 0 0 0 4979 18 0 0 25 0 1 0 546319107 40964096 8345 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10001 8345 603 41 0 9960 0
vsize: 40004
[startup+60.0016 s]
Raw data (loadavg): 0.92 0.94 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 9019 0 0 0 5977 21 0 0 25 0 1 0 546319107 43110400 8853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10525 8853 603 41 0 10484 0
vsize: 42100
[startup+70.0014 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 9504 0 0 0 6976 22 0 0 25 0 1 0 546319107 45117440 9338 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11015 9338 603 41 0 10974 0
vsize: 44060
[startup+80.0024 s]
Raw data (loadavg): 0.94 0.94 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 9979 0 0 0 7975 23 0 0 25 0 1 0 546319107 47128576 9813 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11506 9813 603 41 0 11465 0
vsize: 46024
[startup+90.002 s]
Raw data (loadavg): 0.95 0.94 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 10320 0 0 0 8974 24 0 0 25 0 1 0 546319107 48455680 10154 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11830 10154 603 41 0 11789 0
vsize: 47320
[startup+100.002 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 10512 0 0 0 9973 25 0 0 25 0 1 0 546319107 49262592 10346 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12027 10346 603 41 0 11986 0
vsize: 48108
[startup+110.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 10551 0 0 0 10973 25 0 0 25 0 1 0 546319107 49397760 10385 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12060 10385 603 41 0 12019 0
vsize: 48240
[startup+120.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 10719 0 0 0 11973 26 0 0 25 0 1 0 546319107 50069504 10553 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12224 10553 603 41 0 12183 0
vsize: 48896
[startup+130.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 11178 0 0 0 12971 27 0 0 25 0 1 0 546319107 52219904 11012 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12749 11012 603 41 0 12708 0
vsize: 50996
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 11376 0 0 0 13971 28 0 0 25 0 1 0 546319107 53022720 11210 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12945 11210 603 41 0 12904 0
vsize: 51780
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 11559 0 0 0 14971 28 0 0 25 0 1 0 546319107 53694464 11393 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13109 11393 603 41 0 13068 0
vsize: 52436
[startup+160.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 11828 0 0 0 15970 29 0 0 25 0 1 0 546319107 54767616 11662 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13371 11662 603 41 0 13330 0
vsize: 53484
[startup+170.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 12061 0 0 0 16970 30 0 0 25 0 1 0 546319107 55705600 11895 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13600 11895 603 41 0 13559 0
vsize: 54400
[startup+180.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 12307 0 0 0 17969 30 0 0 25 0 1 0 546319107 56762368 12141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13858 12141 603 41 0 13817 0
vsize: 55432
[startup+190.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 12506 0 0 0 18969 31 0 0 25 0 1 0 546319107 57561088 12340 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14053 12340 603 41 0 14012 0
vsize: 56212
[startup+200.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 12704 0 0 0 19969 31 0 0 25 0 1 0 546319107 58376192 12538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14252 12538 603 41 0 14211 0
vsize: 57008
[startup+210.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 12894 0 0 0 20968 32 0 0 25 0 1 0 546319107 59170816 12728 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14446 12728 603 41 0 14405 0
vsize: 57784
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 13133 0 0 0 21968 33 0 0 25 0 1 0 546319107 60108800 12967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14675 12967 603 41 0 14634 0
vsize: 58700
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 13376 0 0 0 22967 34 0 0 25 0 1 0 546319107 61042688 13210 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14903 13210 603 41 0 14862 0
vsize: 59612
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 13574 0 0 0 23967 34 0 0 25 0 1 0 546319107 61861888 13408 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15103 13408 603 41 0 15062 0
vsize: 60412
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2547
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 13778 0 0 0 24967 34 0 0 25 0 1 0 546319107 62681088 13612 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15303 13612 603 41 0 15262 0
vsize: 61212
[startup+260.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2549
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 14045 0 0 0 25967 35 0 0 25 0 1 0 546319107 63746048 13879 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15563 13879 603 41 0 15522 0
vsize: 62252
[startup+270.007 s]
Raw data (loadavg): 1.15 0.99 0.93 2/57 2592
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 14249 0 0 0 26961 41 0 0 25 0 1 0 546319107 64552960 14083 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15760 14083 603 41 0 15719 0
vsize: 63040
[startup+280.006 s]
Raw data (loadavg): 1.13 0.99 0.93 2/55 2602
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 14459 0 0 0 27953 48 0 0 25 0 1 0 546319107 65515520 14293 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15995 14293 603 41 0 15954 0
vsize: 63980
[startup+290.008 s]
Raw data (loadavg): 1.11 0.99 0.93 2/55 2602
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 14616 0 0 0 28952 49 0 0 25 0 1 0 546319107 66183168 14450 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16158 14450 603 41 0 16117 0
vsize: 64632
[startup+300.007 s]
Raw data (loadavg): 1.09 0.99 0.93 2/55 2602
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 14781 0 0 0 29951 50 0 0 25 0 1 0 546319107 66719744 14615 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16289 14615 603 41 0 16248 0
vsize: 65156
[startup+310.007 s]
Raw data (loadavg): 1.08 0.99 0.93 2/55 2602
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 14911 0 0 0 30951 51 0 0 25 0 1 0 546319107 67768320 14745 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16545 14745 603 41 0 16504 0
vsize: 66180
[startup+320.007 s]
Raw data (loadavg): 1.07 0.99 0.93 2/55 2602
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 15035 0 0 0 31950 51 0 0 25 0 1 0 546319107 68300800 14869 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16675 14869 603 41 0 16634 0
vsize: 66700
[startup+330.006 s]
Raw data (loadavg): 1.06 0.99 0.93 2/55 2602
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 15175 0 0 0 32949 52 0 0 25 0 1 0 546319107 68837376 15009 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16806 15009 603 41 0 16765 0
vsize: 67224
[startup+340.006 s]
Raw data (loadavg): 1.05 0.99 0.93 2/55 2602
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 15288 0 0 0 33949 53 0 0 25 0 1 0 546319107 69365760 15122 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16935 15122 603 41 0 16894 0
vsize: 67740
[startup+350.007 s]
Raw data (loadavg): 1.04 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 15464 0 0 0 34948 54 0 0 25 0 1 0 546319107 70029312 15298 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17097 15298 603 41 0 17056 0
vsize: 68388
[startup+360.008 s]
Raw data (loadavg): 1.03 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 15720 0 0 0 35947 55 0 0 25 0 1 0 546319107 71098368 15554 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17358 15554 603 41 0 17317 0
vsize: 69432
[startup+370.008 s]
Raw data (loadavg): 1.03 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 15875 0 0 0 36947 56 0 0 25 0 1 0 546319107 71634944 15709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17489 15709 603 41 0 17448 0
vsize: 69956
[startup+380.008 s]
Raw data (loadavg): 1.02 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 16075 0 0 0 37946 57 0 0 25 0 1 0 546319107 72429568 15909 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17683 15909 603 41 0 17642 0
vsize: 70732
[startup+390.008 s]
Raw data (loadavg): 1.02 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 16217 0 0 0 38945 57 0 0 25 0 1 0 546319107 73105408 16051 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17848 16051 603 41 0 17807 0
vsize: 71392
[startup+400.008 s]
Raw data (loadavg): 1.02 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 16329 0 0 0 39945 58 0 0 25 0 1 0 546319107 73498624 16163 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17944 16163 603 41 0 17903 0
vsize: 71776
[startup+410.008 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 16412 0 0 0 40944 59 0 0 25 0 1 0 546319107 73900032 16246 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18042 16246 603 41 0 18001 0
vsize: 72168
[startup+420.009 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 16600 0 0 0 41944 60 0 0 25 0 1 0 546319107 74567680 16434 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18205 16434 603 41 0 18164 0
vsize: 72820
[startup+430.008 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 16821 0 0 0 42943 60 0 0 25 0 1 0 546319107 75501568 16655 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18433 16655 603 41 0 18392 0
vsize: 73732
[startup+440.009 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 17002 0 0 0 43942 62 0 0 25 0 1 0 546319107 76169216 16836 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18596 16836 603 41 0 18555 0
vsize: 74384
[startup+450.008 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 17236 0 0 0 44941 63 0 0 25 0 1 0 546319107 77111296 17070 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18826 17070 603 41 0 18785 0
vsize: 75304
[startup+460.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 17472 0 0 0 45940 64 0 0 25 0 1 0 546319107 78041088 17306 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19053 17306 603 41 0 19012 0
vsize: 76212
[startup+470.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 17671 0 0 0 46939 65 0 0 25 0 1 0 546319107 78970880 17505 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19280 17505 603 41 0 19239 0
vsize: 77120
[startup+480.008 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 17904 0 0 0 47938 66 0 0 25 0 1 0 546319107 79912960 17738 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19510 17738 603 41 0 19469 0
vsize: 78040
[startup+490.008 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 18098 0 0 0 48937 67 0 0 25 0 1 0 546319107 80723968 17932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19708 17932 603 41 0 19667 0
vsize: 78832
[startup+500.008 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 18270 0 0 0 49936 68 0 0 25 0 1 0 546319107 81416192 18104 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19877 18104 603 41 0 19836 0
vsize: 79508
[startup+510.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 18455 0 0 0 50936 69 0 0 25 0 1 0 546319107 82079744 18289 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20039 18289 603 41 0 19998 0
vsize: 80156
[startup+520.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 18500 0 0 0 51935 70 0 0 25 0 1 0 546319107 82345984 18334 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20104 18334 603 41 0 20063 0
vsize: 80416
[startup+530.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 18611 0 0 0 52934 71 0 0 25 0 1 0 546319107 82763776 18445 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20206 18445 603 41 0 20165 0
vsize: 80824
[startup+540.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 18772 0 0 0 53934 71 0 0 25 0 1 0 546319107 83447808 18606 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20373 18606 603 41 0 20332 0
vsize: 81492
[startup+550.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2604
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 18861 0 0 0 54933 72 0 0 25 0 1 0 546319107 83714048 18695 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20438 18695 603 41 0 20397 0
vsize: 81752
[startup+560.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2606
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 19123 0 0 0 55932 73 0 0 25 0 1 0 546319107 84787200 18957 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20700 18957 603 41 0 20659 0
vsize: 82800
[startup+570.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2606
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 19301 0 0 0 56932 74 0 0 25 0 1 0 546319107 85454848 19135 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20863 19135 603 41 0 20822 0
vsize: 83452
[startup+580.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2606
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 19513 0 0 0 57931 75 0 0 25 0 1 0 546319107 86388736 19347 4294967295 134512640 134672761 3221224544 3221223668 134566054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21091 19347 603 41 0 21050 0
vsize: 84364
[startup+590.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2606
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 19675 0 0 0 58931 75 0 0 25 0 1 0 546319107 87052288 19509 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21253 19509 603 41 0 21212 0
vsize: 85012
[startup+600.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2606
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 19871 0 0 0 59931 76 0 0 25 0 1 0 546319107 87863296 19705 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21451 19705 603 41 0 21410 0
vsize: 85804
[startup+610.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2606
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 20090 0 0 0 60930 76 0 0 25 0 1 0 546319107 88653824 19924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21644 19924 603 41 0 21603 0
vsize: 86576
[startup+620.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2606
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 20274 0 0 0 61929 77 0 0 25 0 1 0 546319107 89448448 20108 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21838 20108 603 41 0 21797 0
vsize: 87352
[startup+630.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2606
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 20405 0 0 0 62929 78 0 0 25 0 1 0 546319107 89985024 20239 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21969 20239 603 41 0 21928 0
vsize: 87876
[startup+640.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2606
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 20535 0 0 0 63929 78 0 0 25 0 1 0 546319107 90521600 20369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 20369 603 41 0 22059 0
vsize: 88400
[startup+650.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 20987 0 0 0 64927 80 0 0 25 0 1 0 546319107 92401664 20821 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22559 20821 603 41 0 22518 0
vsize: 90236
[startup+660.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 21137 0 0 0 65927 80 0 0 25 0 1 0 546319107 92946432 20971 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22692 20971 603 41 0 22651 0
vsize: 90768
[startup+670.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 21240 0 0 0 66927 80 0 0 25 0 1 0 546319107 93474816 21074 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22821 21074 603 41 0 22780 0
vsize: 91284
[startup+680.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 21402 0 0 0 67927 81 0 0 25 0 1 0 546319107 94146560 21236 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22985 21236 603 41 0 22944 0
vsize: 91940
[startup+690.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 21879 0 0 0 68926 82 0 0 25 0 1 0 546319107 96018432 21713 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23442 21713 603 41 0 23401 0
vsize: 93768
[startup+700.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 22238 0 0 0 69924 84 0 0 25 0 1 0 546319107 97484800 22072 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23800 22072 603 41 0 23759 0
vsize: 95200
[startup+710.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 22424 0 0 0 70924 84 0 0 25 0 1 0 546319107 99340288 22258 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24253 22258 603 41 0 24212 0
vsize: 97012
[startup+720.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 22659 0 0 0 71924 85 0 0 25 0 1 0 546319107 100274176 22493 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24481 22493 603 41 0 24440 0
vsize: 97924
[startup+730.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 22952 0 0 0 72923 86 0 0 25 0 1 0 546319107 101478400 22786 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24775 22786 603 41 0 24734 0
vsize: 99100
[startup+740.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 23125 0 0 0 73923 86 0 0 25 0 1 0 546319107 102162432 22959 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24942 22959 603 41 0 24901 0
vsize: 99768
[startup+750.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 23368 0 0 0 74922 87 0 0 25 0 1 0 546319107 103092224 23202 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25169 23202 603 41 0 25128 0
vsize: 100676
[startup+760.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 23522 0 0 0 75922 87 0 0 25 0 1 0 546319107 103755776 23356 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25331 23356 603 41 0 25290 0
vsize: 101324
[startup+770.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 23604 0 0 0 76921 88 0 0 25 0 1 0 546319107 104022016 23438 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25396 23438 603 41 0 25355 0
vsize: 101584
[startup+780.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 23654 0 0 0 77921 88 0 0 25 0 1 0 546319107 104288256 23488 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25461 23488 603 41 0 25420 0
vsize: 101844
[startup+790.009 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 23794 0 0 0 78921 88 0 0 25 0 1 0 546319107 104824832 23628 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25592 23628 603 41 0 25551 0
vsize: 102368
[startup+800.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 23959 0 0 0 79921 89 0 0 25 0 1 0 546319107 105488384 23793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25754 23793 603 41 0 25713 0
vsize: 103016
[startup+810.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 24227 0 0 0 80919 91 0 0 25 0 1 0 546319107 106557440 24061 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26015 24061 603 41 0 25974 0
vsize: 104060
[startup+820.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 24460 0 0 0 81918 91 0 0 25 0 1 0 546319107 107495424 24294 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26244 24294 603 41 0 26203 0
vsize: 104976
[startup+830.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 24671 0 0 0 82918 92 0 0 25 0 1 0 546319107 108429312 24505 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26472 24505 603 41 0 26431 0
vsize: 105888
[startup+840.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 24910 0 0 0 83917 93 0 0 25 0 1 0 546319107 109363200 24744 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26700 24744 603 41 0 26659 0
vsize: 106800
[startup+850.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2608
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 25283 0 0 0 84917 93 0 0 25 0 1 0 546319107 110837760 25117 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27060 25117 603 41 0 27019 0
vsize: 108240
[startup+860.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 25558 0 0 0 85917 94 0 0 25 0 1 0 546319107 111910912 25392 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27322 25392 603 41 0 27281 0
vsize: 109288
[startup+870.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 25813 0 0 0 86916 94 0 0 25 0 1 0 546319107 112988160 25647 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27585 25647 603 41 0 27544 0
vsize: 110340
[startup+880.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 25998 0 0 0 87916 95 0 0 25 0 1 0 546319107 113672192 25832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27752 25832 603 41 0 27711 0
vsize: 111008
[startup+890.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 26129 0 0 0 88916 95 0 0 25 0 1 0 546319107 114208768 25963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27883 25963 603 41 0 27842 0
vsize: 111532
[startup+900.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 26308 0 0 0 89915 96 0 0 25 0 1 0 546319107 114896896 26142 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28051 26142 603 41 0 28010 0
vsize: 112204
[startup+910.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 26450 0 0 0 90915 96 0 0 25 0 1 0 546319107 115564544 26284 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28214 26284 603 41 0 28173 0
vsize: 112856
[startup+920.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 26547 0 0 0 91915 96 0 0 25 0 1 0 546319107 115961856 26381 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28311 26381 603 41 0 28270 0
vsize: 113244
[startup+930.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 26717 0 0 0 92915 97 0 0 25 0 1 0 546319107 116633600 26551 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28475 26551 603 41 0 28434 0
vsize: 113900
[startup+940.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 26886 0 0 0 93914 97 0 0 25 0 1 0 546319107 117309440 26720 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28640 26720 603 41 0 28599 0
vsize: 114560
[startup+950.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 27075 0 0 0 94914 98 0 0 25 0 1 0 546319107 118116352 26909 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28837 26909 603 41 0 28796 0
vsize: 115348
[startup+960.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 27193 0 0 0 95914 98 0 0 25 0 1 0 546319107 118550528 27027 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28943 27027 603 41 0 28902 0
vsize: 115772
[startup+970.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 27292 0 0 0 96913 99 0 0 25 0 1 0 546319107 118956032 27126 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29042 27126 603 41 0 29001 0
vsize: 116168
[startup+980.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 27399 0 0 0 97913 99 0 0 25 0 1 0 546319107 119361536 27233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29141 27233 603 41 0 29100 0
vsize: 116564
[startup+990.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 27539 0 0 0 98913 100 0 0 25 0 1 0 546319107 119898112 27373 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29272 27373 603 41 0 29231 0
vsize: 117088
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 27656 0 0 0 99913 100 0 0 25 0 1 0 546319107 120426496 27490 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29401 27490 603 41 0 29360 0
vsize: 117604
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 27796 0 0 0 100913 100 0 0 25 0 1 0 546319107 120963072 27630 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29532 27630 603 41 0 29491 0
vsize: 118128
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 27949 0 0 0 101912 101 0 0 25 0 1 0 546319107 121634816 27783 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29696 27783 603 41 0 29655 0
vsize: 118784
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 28072 0 0 0 102912 101 0 0 25 0 1 0 546319107 122036224 27906 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29794 27906 603 41 0 29753 0
vsize: 119176
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 28192 0 0 0 103912 102 0 0 25 0 1 0 546319107 122572800 28026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29925 28026 603 41 0 29884 0
vsize: 119700
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 28318 0 0 0 104912 102 0 0 25 0 1 0 546319107 123105280 28152 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30055 28152 603 41 0 30014 0
vsize: 120220
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 28434 0 0 0 105911 103 0 0 25 0 1 0 546319107 123514880 28268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30155 28268 603 41 0 30114 0
vsize: 120620
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 28539 0 0 0 106911 104 0 0 25 0 1 0 546319107 123916288 28373 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30253 28373 603 41 0 30212 0
vsize: 121012
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 28646 0 0 0 107910 104 0 0 25 0 1 0 546319107 124350464 28480 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30359 28480 603 41 0 30318 0
vsize: 121436
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 28744 0 0 0 108910 105 0 0 25 0 1 0 546319107 124747776 28578 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30456 28578 603 41 0 30415 0
vsize: 121824
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 28877 0 0 0 109909 105 0 0 25 0 1 0 546319107 125292544 28711 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30589 28711 603 41 0 30548 0
vsize: 122356
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 28969 0 0 0 110909 106 0 0 25 0 1 0 546319107 125698048 28803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30688 28803 603 41 0 30647 0
vsize: 122752
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 29045 0 0 0 111909 106 0 0 25 0 1 0 546319107 125972480 28879 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30755 28879 603 41 0 30714 0
vsize: 123020
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 29148 0 0 0 112909 106 0 0 25 0 1 0 546319107 126382080 28982 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30855 28982 603 41 0 30814 0
vsize: 123420
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 29258 0 0 0 113909 107 0 0 25 0 1 0 546319107 126943232 29092 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30992 29092 603 41 0 30951 0
vsize: 123968
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2610
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 29346 0 0 0 114909 107 0 0 25 0 1 0 546319107 127352832 29180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31092 29180 603 41 0 31051 0
vsize: 124368
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2612
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 29447 0 0 0 115908 107 0 0 25 0 1 0 546319107 127762432 29281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31192 29281 603 41 0 31151 0
vsize: 124768
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2612
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 29539 0 0 0 116908 108 0 0 25 0 1 0 546319107 128028672 29373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31257 29373 603 41 0 31216 0
vsize: 125028
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2612
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 29604 0 0 0 117908 108 0 0 25 0 1 0 546319107 128299008 29438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31323 29438 603 41 0 31282 0
vsize: 125292
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2612
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 29686 0 0 0 118908 108 0 0 25 0 1 0 546319107 128700416 29520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31421 29520 603 41 0 31380 0
vsize: 125684
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 2612
Raw data (stat): 2547 (minisat+) R 2546 22929 22928 0 -1 0 29765 0 0 0 119907 109 0 0 25 0 1 0 546319107 128966656 29599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31486 29599 603 41 0 31445 0
vsize: 125944
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.93 1/55 2612
Raw data (stat): 2547 (minisat+) Z 2546 22929 22928 0 -1 12 29767 0 0 0 119907 115 0 0 25 0 1 0 546319107 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.23
CPU user time (s): 1199.07
CPU system time (s): 1.15282
CPU usage (%): 100.013
Max. virtual memory (Kb): 125944
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####