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/miplib3/normalized-mps-v2-13-7-mkc.opb
MD5SUM	b9e9aa470fdb3341d7e10860fcc70cec
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 18083

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        805972 kB
Buffers:         28844 kB
Cached:         178116 kB
SwapCached:        440 kB
Active:          12880 kB
Inactive:       196244 kB
HighTotal:      131008 kB
HighFree:        62720 kB
LowTotal:       903652 kB
LowFree:        743252 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            13912 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:47:50 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 18613 7 1200.24 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.89 0.97 0.93 2/54 8788
Raw data (stat): 8788 (runsolver) R 8787 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487212418 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.91 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 7680 0 0 0 978 20 0 0 25 0 1 0 487212418 37572608 7514 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9173 7514 603 41 0 9132 0
vsize: 36692
[startup+20.0019 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 7763 0 0 0 1977 20 0 0 25 0 1 0 487212418 37978112 7597 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9272 7597 603 41 0 9231 0
vsize: 37088
[startup+30.0024 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 8026 0 0 0 2976 21 0 0 25 0 1 0 487212418 38969344 7860 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9514 7860 603 41 0 9473 0
vsize: 38056
[startup+40.0031 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 8435 0 0 0 3975 23 0 0 25 0 1 0 487212418 40697856 8269 4294967295 134512640 134672761 3221224544 3221223724 134556674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9936 8269 603 41 0 9895 0
vsize: 39744
[startup+50.0032 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 8504 0 0 0 4975 23 0 0 25 0 1 0 487212418 40964096 8338 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10001 8338 603 41 0 9960 0
vsize: 40004
[startup+60.0037 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 8976 0 0 0 5973 25 0 0 25 0 1 0 487212418 42844160 8810 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10460 8810 603 41 0 10419 0
vsize: 41840
[startup+70.0045 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 9448 0 0 0 6972 26 0 0 25 0 1 0 487212418 44982272 9282 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10982 9282 603 41 0 10941 0
vsize: 43928
[startup+80.0047 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 9905 0 0 0 7971 27 0 0 25 0 1 0 487212418 46723072 9739 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11407 9739 603 41 0 11366 0
vsize: 45628
[startup+90.0052 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 10283 0 0 0 8971 28 0 0 25 0 1 0 487212418 48324608 10117 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 10117 603 41 0 11757 0
vsize: 47192
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 10493 0 0 0 9970 29 0 0 25 0 1 0 487212418 49127424 10327 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11994 10327 603 41 0 11953 0
vsize: 47976
[startup+110.006 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 10541 0 0 0 10970 29 0 0 25 0 1 0 487212418 49397760 10375 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12060 10375 603 41 0 12019 0
vsize: 48240
[startup+120.007 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 10670 0 0 0 11970 29 0 0 25 0 1 0 487212418 49934336 10504 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12191 10504 603 41 0 12150 0
vsize: 48764
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 11045 0 0 0 12969 30 0 0 25 0 1 0 487212418 51421184 10879 4294967295 134512640 134672761 3221224544 3221223648 134555087 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12554 10879 603 41 0 12513 0
vsize: 50216
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 11306 0 0 0 13969 31 0 0 25 0 1 0 487212418 52756480 11140 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12880 11140 603 41 0 12839 0
vsize: 51520
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 11501 0 0 0 14968 32 0 0 25 0 1 0 487212418 53424128 11335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13043 11335 603 41 0 13002 0
vsize: 52172
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 11747 0 0 0 15968 32 0 0 25 0 1 0 487212418 54497280 11581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13305 11581 603 41 0 13264 0
vsize: 53220
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 12009 0 0 0 16967 33 0 0 25 0 1 0 487212418 55570432 11843 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13567 11843 603 41 0 13526 0
vsize: 54268
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 12250 0 0 0 17967 34 0 0 25 0 1 0 487212418 56496128 12084 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13793 12084 603 41 0 13752 0
vsize: 55172
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 12436 0 0 0 18966 35 0 0 25 0 1 0 487212418 57298944 12270 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13989 12270 603 41 0 13948 0
vsize: 55956
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 12615 0 0 0 19966 35 0 0 25 0 1 0 487212418 57962496 12449 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14151 12449 603 41 0 14110 0
vsize: 56604
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 12807 0 0 0 20966 35 0 0 25 0 1 0 487212418 58773504 12641 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14349 12641 603 41 0 14308 0
vsize: 57396
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 13049 0 0 0 21965 37 0 0 25 0 1 0 487212418 59711488 12883 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14578 12883 603 41 0 14537 0
vsize: 58312
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 13284 0 0 0 22965 37 0 0 25 0 1 0 487212418 60641280 13118 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14805 13118 603 41 0 14764 0
vsize: 59220
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 13495 0 0 0 23964 38 0 0 25 0 1 0 487212418 61579264 13329 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15034 13329 603 41 0 14993 0
vsize: 60136
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 13681 0 0 0 24963 39 0 0 25 0 1 0 487212418 62279680 13515 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15205 13515 603 41 0 15164 0
vsize: 60820
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 13906 0 0 0 25963 39 0 0 25 0 1 0 487212418 63213568 13740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15433 13740 603 41 0 15392 0
vsize: 61732
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 14146 0 0 0 26962 40 0 0 25 0 1 0 487212418 64151552 13980 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15662 13980 603 41 0 15621 0
vsize: 62648
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 14370 0 0 0 27961 41 0 0 25 0 1 0 487212418 65093632 14204 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15892 14204 603 41 0 15851 0
vsize: 63568
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 14535 0 0 0 28961 42 0 0 25 0 1 0 487212418 65781760 14369 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16060 14369 603 41 0 16019 0
vsize: 64240
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 14682 0 0 0 29961 42 0 0 25 0 1 0 487212418 66453504 14516 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16224 14516 603 41 0 16183 0
vsize: 64896
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 14831 0 0 0 30961 42 0 0 25 0 1 0 487212418 66981888 14665 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 14665 603 41 0 16312 0
vsize: 65412
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 14996 0 0 0 31960 43 0 0 25 0 1 0 487212418 68165632 14830 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16642 14830 603 41 0 16601 0
vsize: 66568
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 15075 0 0 0 32960 43 0 0 25 0 1 0 487212418 68435968 14909 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16708 14909 603 41 0 16667 0
vsize: 66832
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 15207 0 0 0 33960 44 0 0 25 0 1 0 487212418 68968448 15041 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16838 15041 603 41 0 16797 0
vsize: 67352
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 15317 0 0 0 34959 44 0 0 25 0 1 0 487212418 69500928 15151 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16968 15151 603 41 0 16927 0
vsize: 67872
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 15544 0 0 0 35958 45 0 0 25 0 1 0 487212418 70295552 15378 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17162 15378 603 41 0 17121 0
vsize: 68648
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 15731 0 0 0 36958 46 0 0 25 0 1 0 487212418 71098368 15565 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17358 15565 603 41 0 17317 0
vsize: 69432
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 15977 0 0 0 37957 47 0 0 25 0 1 0 487212418 72163328 15811 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17618 15811 603 41 0 17577 0
vsize: 70472
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 16117 0 0 0 38957 48 0 0 25 0 1 0 487212418 72699904 15951 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17749 15951 603 41 0 17708 0
vsize: 70996
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 16249 0 0 0 39956 48 0 0 25 0 1 0 487212418 73236480 16083 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17880 16083 603 41 0 17839 0
vsize: 71520
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 16340 0 0 0 40957 48 0 0 25 0 1 0 487212418 73498624 16174 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17944 16174 603 41 0 17903 0
vsize: 71776
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 16452 0 0 0 41957 48 0 0 25 0 1 0 487212418 74035200 16286 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18075 16286 603 41 0 18034 0
vsize: 72300
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 16637 0 0 0 42956 49 0 0 25 0 1 0 487212418 74698752 16471 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 16471 603 41 0 18196 0
vsize: 72948
[startup+440.018 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 16851 0 0 0 43956 49 0 0 25 0 1 0 487212418 75632640 16685 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18465 16685 603 41 0 18424 0
vsize: 73860
[startup+450.018 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 17061 0 0 0 44955 50 0 0 25 0 1 0 487212418 76431360 16895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18660 16895 603 41 0 18619 0
vsize: 74640
[startup+460.019 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 17260 0 0 0 45955 51 0 0 25 0 1 0 487212418 77246464 17094 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18859 17094 603 41 0 18818 0
vsize: 75436
[startup+470.019 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 17484 0 0 0 46954 52 0 0 25 0 1 0 487212418 78172160 17318 4294967295 134512640 134672761 3221224544 3221223712 134559675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19085 17318 603 41 0 19044 0
vsize: 76340
[startup+480.018 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 17677 0 0 0 47954 52 0 0 25 0 1 0 487212418 78970880 17511 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19280 17511 603 41 0 19239 0
vsize: 77120
[startup+490.019 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 17917 0 0 0 48953 53 0 0 25 0 1 0 487212418 79912960 17751 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19510 17751 603 41 0 19469 0
vsize: 78040
[startup+500.019 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 18108 0 0 0 49953 54 0 0 25 0 1 0 487212418 80723968 17942 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19708 17942 603 41 0 19667 0
vsize: 78832
[startup+510.019 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 18282 0 0 0 50952 55 0 0 25 0 1 0 487212418 81416192 18116 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19877 18116 603 41 0 19836 0
vsize: 79508
[startup+520.02 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 18459 0 0 0 51950 56 0 0 25 0 1 0 487212418 82079744 18293 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20039 18293 603 41 0 19998 0
vsize: 80156
[startup+530.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 18504 0 0 0 52950 56 0 0 25 0 1 0 487212418 82345984 18338 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20104 18338 603 41 0 20063 0
vsize: 80416
[startup+540.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 18608 0 0 0 53950 56 0 0 25 0 1 0 487212418 82763776 18442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20206 18442 603 41 0 20165 0
vsize: 80824
[startup+550.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 18770 0 0 0 54950 57 0 0 25 0 1 0 487212418 83447808 18604 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20373 18604 603 41 0 20332 0
vsize: 81492
[startup+560.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 18852 0 0 0 55949 57 0 0 25 0 1 0 487212418 83714048 18686 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20438 18686 603 41 0 20397 0
vsize: 81752
[startup+570.021 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 19121 0 0 0 56949 58 0 0 25 0 1 0 487212418 84787200 18955 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20700 18955 603 41 0 20659 0
vsize: 82800
[startup+580.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 19295 0 0 0 57949 58 0 0 25 0 1 0 487212418 85454848 19129 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20863 19129 603 41 0 20822 0
vsize: 83452
[startup+590.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 19499 0 0 0 58948 59 0 0 25 0 1 0 487212418 86257664 19333 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21059 19333 603 41 0 21018 0
vsize: 84236
[startup+600.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 19662 0 0 0 59947 60 0 0 25 0 1 0 487212418 86921216 19496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21221 19496 603 41 0 21180 0
vsize: 84884
[startup+610.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 19867 0 0 0 60947 61 0 0 25 0 1 0 487212418 87863296 19701 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21451 19701 603 41 0 21410 0
vsize: 85804
[startup+620.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 20075 0 0 0 61946 61 0 0 25 0 1 0 487212418 88653824 19909 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21644 19909 603 41 0 21603 0
vsize: 86576
[startup+630.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 20266 0 0 0 62946 62 0 0 25 0 1 0 487212418 89448448 20100 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21838 20100 603 41 0 21797 0
vsize: 87352
[startup+640.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 20392 0 0 0 63945 63 0 0 25 0 1 0 487212418 89853952 20226 4294967295 134512640 134672761 3221224544 3221223712 134564716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21937 20226 603 41 0 21896 0
vsize: 87748
[startup+650.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 20527 0 0 0 64945 63 0 0 25 0 1 0 487212418 90521600 20361 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22100 20361 603 41 0 22059 0
vsize: 88400
[startup+660.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 20938 0 0 0 65944 64 0 0 25 0 1 0 487212418 92131328 20772 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22493 20772 603 41 0 22452 0
vsize: 89972
[startup+670.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 21118 0 0 0 66944 65 0 0 25 0 1 0 487212418 92946432 20952 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22692 20952 603 41 0 22651 0
vsize: 90768
[startup+680.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 21235 0 0 0 67944 65 0 0 25 0 1 0 487212418 93339648 21069 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22788 21069 603 41 0 22747 0
vsize: 91152
[startup+690.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 21378 0 0 0 68943 66 0 0 25 0 1 0 487212418 94015488 21212 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22953 21212 603 41 0 22912 0
vsize: 91812
[startup+700.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 21827 0 0 0 69942 67 0 0 25 0 1 0 487212418 95883264 21661 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23409 21661 603 41 0 23368 0
vsize: 93636
[startup+710.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 22210 0 0 0 70941 68 0 0 25 0 1 0 487212418 97353728 22044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23768 22044 603 41 0 23727 0
vsize: 95072
[startup+720.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 22404 0 0 0 71941 68 0 0 25 0 1 0 487212418 99209216 22238 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24221 22238 603 41 0 24180 0
vsize: 96884
[startup+730.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 22627 0 0 0 72941 69 0 0 25 0 1 0 487212418 100143104 22461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24449 22461 603 41 0 24408 0
vsize: 97796
[startup+740.023 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 22893 0 0 0 73940 70 0 0 25 0 1 0 487212418 101212160 22727 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24710 22727 603 41 0 24669 0
vsize: 98840
[startup+750.023 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 23097 0 0 0 74940 70 0 0 25 0 1 0 487212418 102027264 22931 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24909 22931 603 41 0 24868 0
vsize: 99636
[startup+760.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 23330 0 0 0 75939 71 0 0 25 0 1 0 487212418 102957056 23164 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25136 23164 603 41 0 25095 0
vsize: 100544
[startup+770.024 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 23497 0 0 0 76939 71 0 0 25 0 1 0 487212418 103620608 23331 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25298 23331 603 41 0 25257 0
vsize: 101192
[startup+780.023 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 23586 0 0 0 77939 72 0 0 25 0 1 0 487212418 104022016 23420 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25396 23420 603 41 0 25355 0
vsize: 101584
[startup+790.023 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 23647 0 0 0 78939 72 0 0 25 0 1 0 487212418 104288256 23481 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25461 23481 603 41 0 25420 0
vsize: 101844
[startup+800.023 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 23765 0 0 0 79939 72 0 0 25 0 1 0 487212418 104685568 23599 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25558 23599 603 41 0 25517 0
vsize: 102232
[startup+810.023 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 23943 0 0 0 80938 73 0 0 25 0 1 0 487212418 105488384 23777 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25754 23777 603 41 0 25713 0
vsize: 103016
[startup+820.024 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 24121 0 0 0 81938 73 0 0 25 0 1 0 487212418 106160128 23955 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25918 23955 603 41 0 25877 0
vsize: 103672
[startup+830.024 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 24407 0 0 0 82936 75 0 0 25 0 1 0 487212418 107360256 24241 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26211 24241 603 41 0 26170 0
vsize: 104844
[startup+840.025 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 24630 0 0 0 83935 76 0 0 25 0 1 0 487212418 108163072 24464 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26407 24464 603 41 0 26366 0
vsize: 105628
[startup+850.025 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 24843 0 0 0 84934 77 0 0 25 0 1 0 487212418 109096960 24677 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26635 24677 603 41 0 26594 0
vsize: 106540
[startup+860.025 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 25225 0 0 0 85934 77 0 0 25 0 1 0 487212418 110571520 25059 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26995 25059 603 41 0 26954 0
vsize: 107980
[startup+870.026 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 25507 0 0 0 86933 78 0 0 25 0 1 0 487212418 111775744 25341 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27289 25341 603 41 0 27248 0
vsize: 109156
[startup+880.026 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 25767 0 0 0 87932 79 0 0 25 0 1 0 487212418 112721920 25601 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27520 25601 603 41 0 27479 0
vsize: 110080
[startup+890.027 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 25977 0 0 0 88932 80 0 0 25 0 1 0 487212418 113672192 25811 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27752 25811 603 41 0 27711 0
vsize: 111008
[startup+900.027 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 26106 0 0 0 89931 81 0 0 25 0 1 0 487212418 114073600 25940 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27850 25940 603 41 0 27809 0
vsize: 111400
[startup+910.027 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 26272 0 0 0 90931 81 0 0 25 0 1 0 487212418 114749440 26106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28015 26106 603 41 0 27974 0
vsize: 112060
[startup+920.027 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 26430 0 0 0 91931 81 0 0 25 0 1 0 487212418 115433472 26264 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28182 26264 603 41 0 28141 0
vsize: 112728
[startup+930.027 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 26530 0 0 0 92931 81 0 0 25 0 1 0 487212418 115830784 26364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28279 26364 603 41 0 28238 0
vsize: 113116
[startup+940.027 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 26672 0 0 0 93931 82 0 0 25 0 1 0 487212418 116367360 26506 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28410 26506 603 41 0 28369 0
vsize: 113640
[startup+950.028 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 26858 0 0 0 94930 83 0 0 25 0 1 0 487212418 117174272 26692 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28607 26692 603 41 0 28566 0
vsize: 114428
[startup+960.027 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 27019 0 0 0 95930 83 0 0 25 0 1 0 487212418 117841920 26853 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28770 26853 603 41 0 28729 0
vsize: 115080
[startup+970.028 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 27169 0 0 0 96930 83 0 0 25 0 1 0 487212418 118403072 27003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28907 27003 603 41 0 28866 0
vsize: 115628
[startup+980.028 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 27277 0 0 0 97930 84 0 0 25 0 1 0 487212418 118816768 27111 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29008 27111 603 41 0 28967 0
vsize: 116032
[startup+990.029 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 27359 0 0 0 98930 84 0 0 25 0 1 0 487212418 119226368 27193 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29108 27193 603 41 0 29067 0
vsize: 116432
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 27510 0 0 0 99929 85 0 0 25 0 1 0 487212418 119767040 27344 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29240 27344 603 41 0 29199 0
vsize: 116960
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 27628 0 0 0 100929 85 0 0 25 0 1 0 487212418 120295424 27462 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29369 27462 603 41 0 29328 0
vsize: 117476
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 27761 0 0 0 101929 85 0 0 25 0 1 0 487212418 120827904 27595 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29499 27595 603 41 0 29458 0
vsize: 117996
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 27923 0 0 0 102929 86 0 0 25 0 1 0 487212418 121499648 27757 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29663 27757 603 41 0 29622 0
vsize: 118652
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 28052 0 0 0 103928 86 0 0 25 0 1 0 487212418 122036224 27886 4294967295 134512640 134672761 3221224544 3221223728 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29794 27886 603 41 0 29753 0
vsize: 119176
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 28164 0 0 0 104928 87 0 0 25 0 1 0 487212418 122441728 27998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 27998 603 41 0 29852 0
vsize: 119572
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 28290 0 0 0 105927 87 0 0 25 0 1 0 487212418 122970112 28124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30022 28124 603 41 0 29981 0
vsize: 120088
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 28407 0 0 0 106927 88 0 0 25 0 1 0 487212418 123379712 28241 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30122 28241 603 41 0 30081 0
vsize: 120488
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 28517 0 0 0 107927 88 0 0 25 0 1 0 487212418 123916288 28351 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30253 28351 603 41 0 30212 0
vsize: 121012
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 28623 0 0 0 108927 88 0 0 25 0 1 0 487212418 124350464 28457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30359 28457 603 41 0 30318 0
vsize: 121436
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 28721 0 0 0 109927 89 0 0 25 0 1 0 487212418 124747776 28555 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30456 28555 603 41 0 30415 0
vsize: 121824
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 28819 0 0 0 110927 89 0 0 25 0 1 0 487212418 125145088 28653 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30553 28653 603 41 0 30512 0
vsize: 122212
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 28951 0 0 0 111926 90 0 0 25 0 1 0 487212418 125562880 28785 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30655 28785 603 41 0 30614 0
vsize: 122620
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 29024 0 0 0 112926 90 0 0 25 0 1 0 487212418 125972480 28858 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30755 28858 603 41 0 30714 0
vsize: 123020
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 29099 0 0 0 113926 90 0 0 25 0 1 0 487212418 126238720 28933 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30820 28933 603 41 0 30779 0
vsize: 123280
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 29229 0 0 0 114926 91 0 0 25 0 1 0 487212418 126791680 29063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30955 29063 603 41 0 30914 0
vsize: 123820
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 29326 0 0 0 115926 91 0 0 25 0 1 0 487212418 127217664 29160 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31059 29160 603 41 0 31018 0
vsize: 124236
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 29392 0 0 0 116925 92 0 0 25 0 1 0 487212418 127483904 29226 4294967295 134512640 134672761 3221224544 3221223728 134558638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31124 29226 603 41 0 31083 0
vsize: 124496
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 29519 0 0 0 117925 92 0 0 25 0 1 0 487212418 128028672 29353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31257 29353 603 41 0 31216 0
vsize: 125028
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 29589 0 0 0 118925 92 0 0 25 0 1 0 487212418 128299008 29423 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31323 29423 603 41 0 31282 0
vsize: 125292
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 8788
Raw data (stat): 8788 (minisat+) R 8787 29151 29150 0 -1 0 29666 0 0 0 119925 92 0 0 25 0 1 0 487212418 128569344 29500 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31389 29500 603 41 0 31348 0
vsize: 125556
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.94 1/54 8788
Raw data (stat): 8788 (minisat+) Z 8787 29151 29150 0 -1 12 29668 0 0 0 119925 98 0 0 25 0 1 0 487212418 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.09
CPU time (s): 1200.24
CPU user time (s): 1199.26
CPU system time (s): 0.98085
CPU usage (%): 100.013
Max. virtual memory (Kb): 125556
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####