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-vpm1.opb
MD5SUM	ec9e3281577e2d3f7b25c1cc88cac9ea
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	20
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	168
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	615983
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06884
Number of variables	2124
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	64
Trace number 14946

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 02:12:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18938 boxname=wulflinc15 idbench=1457 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ec9e3281577e2d3f7b25c1cc88cac9ea  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-vpm1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-vpm1.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-vpm1.opb
IDLAUNCH: 18938
/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:        731964 kB
Buffers:         33908 kB
Cached:         244600 kB
SwapCached:       2060 kB
Active:         115744 kB
Inactive:       167612 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        731712 kB
SwapTotal:     2097136 kB
SwapFree:      2094988 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            13664 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 02:32:26 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 18938 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 484]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 483]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 482]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 481]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 480]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 479]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 478]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 477]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 474]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 473]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 472]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 471]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 468]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 467]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 466]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 465]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 462]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 459]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 458]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 457]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 454]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 453]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 452]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 451]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 450]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 448]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 447]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 446]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 445]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 444]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 441]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 440]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 439]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 433]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 427]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 422]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 421]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 415]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 409]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 408]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 402]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 397]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 396]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 391]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 390]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 386]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 385]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 384]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 380]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 379]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 378]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 374]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 373]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 372]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 368]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 367]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 366]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 365]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 364]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 359]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 353]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 347]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 339]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 333]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 327]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 321]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 317]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 316]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 315]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 314]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 313]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 312]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 310]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 309]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 308]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 307]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 306]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 302]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 301]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 300]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 295]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 294]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 290]---> Adder-cost: 30   maxlim: 27134   bits: 16/15
c ---[ 289]---> Adder-cost: 30   maxlim: 27134   bits: 16/15
c ---[ 288]---> Adder-cost: 30   maxlim: 27134   bits: 16/15
c ---[ 287]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 286]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 285]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 284]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 283]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 282]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 280]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 279]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 278]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 277]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 276]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 274]---> Adder-cost: 232   maxlim: 267600   bits: 19/19
c ---[ 264]---> Adder-cost: 288   maxlim: 420400   bits: 20/19
c ---[ 260]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 258]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 256]---> Adder-cost: 238   maxlim: 210767   bits: 18/18
c ---[ 254]---> Adder-cost: 238   maxlim: 210767   bits: 18/18
c ---[ 252]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[ 250]---> Adder-cost: 184   maxlim: 165300   bits: 18/18
c ---[ 248]---> Adder-cost: 224   maxlim: 287667   bits: 19/19
c ---[ 246]---> Adder-cost: 224   maxlim: 262067   bits: 19/18
c ---[ 244]---> Adder-cost: 224   maxlim: 262067   bits: 19/18
c ---[ 242]---> Adder-cost: 208   maxlim: 210867   bits: 18/18
c ---[ 236]---> Adder-cost: 196   maxlim: 203300   bits: 18/18
c ---[ 234]---> Adder-cost: 232   maxlim: 322083   bits: 19/19
c ---[ 232]---> Adder-cost: 180   maxlim: 110883   bits: 17/17
c ---[ 224]---> Adder-cost: 228   maxlim: 229200   bits: 19/18
c ---[ 222]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 216]---> Adder-cost: 202   maxlim: 152900   bits: 18/18
c ---[ 214]---> Adder-cost: 234   maxlim: 244035   bits: 19/18
c ---[ 212]---> Adder-cost: 234   maxlim: 231235   bits: 19/18
c ---[ 210]---> Adder-cost: 278   maxlim: 283183   bits: 19/19
c ---[ 208]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 206]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 204]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 202]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 200]---> Adder-cost: 280   maxlim: 228400   bits: 19/18
c ---[ 198]---> Adder-cost: 332   maxlim: 462383   bits: 20/19
c ---[ 196]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 194]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 192]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 191]---> Adder-cost: 16   maxlim: 381   bits: 9/9
c ---[ 190]---> Adder-cost: 46   maxlim: 635   bits: 10/10
c ---[ 189]---> Adder-cost: 48   maxlim: 699   bits: 10/10
c ---[ 188]---> Adder-cost: 70   maxlim: 889   bits: 10/10
c ---[ 187]---> Adder-cost: 90   maxlim: 1272   bits: 11/11
c ---[ 186]---> Adder-cost: 88   maxlim: 952   bits: 11/10
c ---[ 185]---> Adder-cost: 16   maxlim: 381   bits: 9/9
c ---[ 184]---> Adder-cost: 46   maxlim: 635   bits: 10/10
c ---[ 183]---> Adder-cost: 48   maxlim: 699   bits: 10/10
c ---[ 182]---> Adder-cost: 70   maxlim: 761   bits: 10/10
c ---[ 181]---> Adder-cost: 88   maxlim: 1016   bits: 11/10
c ---[ 180]---> Adder-cost: 88   maxlim: 1080   bits: 11/11
c ---[ 179]---> Adder-cost: 16   maxlim: 381   bits: 9/9
c ---[ 178]---> Adder-cost: 46   maxlim: 635   bits: 10/10
c ---[ 177]---> Adder-cost: 48   maxlim: 667   bits: 10/10
c ---[ 176]---> Adder-cost: 70   maxlim: 857   bits: 10/10
c ---[ 175]---> Adder-cost: 88   maxlim: 1112   bits: 11/11
c ---[ 174]---> Adder-cost: 88   maxlim: 1048   bits: 11/11
c ---[ 173]---> Adder-cost: 16   maxlim: 381   bits: 9/9
c ---[ 172]---> Adder-cost: 46   maxlim: 507   bits: 10/9
c ---[ 171]---> Adder-cost: 48   maxlim: 667   bits: 10/10
c ---[ 170]---> Adder-cost: 68   maxlim: 697   bits: 10/10
c ---[ 169]---> Adder-cost: 86   maxlim: 1080   bits: 11/11
c ---[ 168]---> Adder-cost: 78   maxlim: 888   bits: 10/10
c ---[ 167]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 166]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 165]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 164]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 163]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 162]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 161]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 160]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 159]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 158]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 157]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 156]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 155]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 154]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 153]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 152]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 151]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 150]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 149]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 148]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 147]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 146]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 145]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 144]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 142]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 141]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 140]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 139]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 138]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 136]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 135]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 134]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 133]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 132]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 130]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 129]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 128]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 127]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 126]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 124]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 123]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 122]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 121]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 120]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 116]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 115]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 114]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[ 110]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 109]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 108]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[ 104]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 103]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 102]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  98]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  97]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  96]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  91]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  90]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  85]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  84]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  79]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  78]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  73]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  72]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  68]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  67]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  66]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  62]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  61]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  60]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  56]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  55]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  54]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  50]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  49]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  48]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  47]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  46]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  45]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  44]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  43]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  42]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  41]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  40]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  39]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  38]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  37]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  36]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  35]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  34]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  33]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  32]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  31]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  30]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  29]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  28]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  27]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  26]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  25]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  24]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  22]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  21]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  20]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  19]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  18]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  16]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  15]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  14]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  13]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  12]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  10]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[   9]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   8]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[   7]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[   6]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[   4]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[   3]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   2]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[   1]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[   0]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   74826   270067 |   24942       0        0     nan |  0.000 % |
c |       100 |   74775   269904 |   27436      92      383     4.2 | 23.181 % |
c |       250 |   74754   269838 |   30179     237     1448     6.1 | 23.200 % |
c |       476 |   74740   269791 |   33197     461     3338     7.2 | 23.212 % |
c |       813 |   74732   269765 |   36517     797     8121    10.2 | 23.219 % |
c |      1320 |   74724   269739 |   40169    1303    17352    13.3 | 23.225 % |
c |      2079 |   74709   269690 |   44186    2060    31569    15.3 | 23.237 % |
c |      3218 |   74679   269592 |   48604    3194    50324    15.8 | 23.268 % |
c |      4926 |   74672   269569 |   53465    4901    85714    17.5 | 23.275 % |
c |      7489 |   74623   269412 |   58811    7457   127242    17.1 | 23.331 % |
c |     11335 |   74607   269360 |   64693   11301   232513    20.6 | 23.349 % |
c |     17104 |   74540   269142 |   71162   17061   385436    22.6 | 23.418 % |
c |     25753 |   74467   268907 |   78278   25701   563219    21.9 | 23.499 % |
c |     38727 |   74296   268350 |   86106   38644   802935    20.8 | 23.654 % |
c |     58189 |   74272   268272 |   94717   58103  1417408    24.4 | 23.679 % |
c |     87382 |   74241   268167 |  104188   87291  2231893    25.6 | 23.704 % |
c |    131171 |   74218   268092 |  114607   36851   957821    26.0 | 23.729 % |
c |    196855 |   74171   267941 |  126068  102527  2937819    28.7 | 23.772 % |
c |    295381 |   74157   267895 |  138675   85446  2227531    26.1 | 23.785 % |
c |    443173 |   74093   267681 |  152543  107691  2862673    26.6 | 23.841 % |
#### 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.95 1.03 0.96 2/54 27088
Raw data (stat): 27088 (runsolver) R 27087 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483159485 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99997 s]
Raw data (loadavg): 0.95 1.03 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 2744 0 0 0 991 6 0 0 25 0 1 0 483159485 12890112 2667 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2667 603 41 0 3106 0
vsize: 12588
[startup+20.0011 s]
Raw data (loadavg): 0.96 1.03 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 3284 0 0 0 1989 8 0 0 25 0 1 0 483159485 15167488 3207 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3703 3207 603 41 0 3662 0
vsize: 14812
[startup+30.0009 s]
Raw data (loadavg): 0.97 1.03 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 3983 0 0 0 2987 10 0 0 25 0 1 0 483159485 17989632 3906 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4392 3906 603 41 0 4351 0
vsize: 17568
[startup+40.0014 s]
Raw data (loadavg): 0.97 1.03 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 4573 0 0 0 3985 12 0 0 25 0 1 0 483159485 20672512 4496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5047 4496 603 41 0 5006 0
vsize: 20188
[startup+50.0026 s]
Raw data (loadavg): 0.98 1.02 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 4940 0 0 0 4984 13 0 0 25 0 1 0 483159485 22134784 4863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5404 4863 603 41 0 5363 0
vsize: 21616
[startup+60.0027 s]
Raw data (loadavg): 0.98 1.02 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 5250 0 0 0 5983 15 0 0 25 0 1 0 483159485 23359488 5173 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5703 5173 603 41 0 5662 0
vsize: 22812
[startup+70.0029 s]
Raw data (loadavg): 0.98 1.02 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 5576 0 0 0 6982 15 0 0 25 0 1 0 483159485 24723456 5499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6036 5499 603 41 0 5995 0
vsize: 24144
[startup+80.003 s]
Raw data (loadavg): 0.98 1.02 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 5827 0 0 0 7982 16 0 0 25 0 1 0 483159485 25796608 5750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6298 5750 603 41 0 6257 0
vsize: 25192
[startup+90.0039 s]
Raw data (loadavg): 0.99 1.02 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6015 0 0 0 8982 16 0 0 25 0 1 0 483159485 26456064 5938 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6459 5938 603 41 0 6418 0
vsize: 25836
[startup+100.003 s]
Raw data (loadavg): 0.99 1.02 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6069 0 0 0 9982 16 0 0 25 0 1 0 483159485 26718208 5992 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6523 5992 603 41 0 6482 0
vsize: 26092
[startup+110.004 s]
Raw data (loadavg): 0.99 1.02 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6088 0 0 0 10982 16 0 0 25 0 1 0 483159485 26861568 6011 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6558 6011 603 41 0 6517 0
vsize: 26232
[startup+120.004 s]
Raw data (loadavg): 0.99 1.02 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6089 0 0 0 11982 16 0 0 25 0 1 0 483159485 26861568 6012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6558 6012 603 41 0 6517 0
vsize: 26232
[startup+130.004 s]
Raw data (loadavg): 0.99 1.02 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6094 0 0 0 12982 16 0 0 25 0 1 0 483159485 26861568 6017 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6558 6017 603 41 0 6517 0
vsize: 26232
[startup+140.005 s]
Raw data (loadavg): 0.99 1.02 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6094 0 0 0 13982 16 0 0 25 0 1 0 483159485 26861568 6017 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6558 6017 603 41 0 6517 0
vsize: 26232
[startup+150.005 s]
Raw data (loadavg): 0.99 1.01 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6094 0 0 0 14982 16 0 0 25 0 1 0 483159485 26861568 6017 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6558 6017 603 41 0 6517 0
vsize: 26232
[startup+160.004 s]
Raw data (loadavg): 0.99 1.01 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6107 0 0 0 15983 16 0 0 25 0 1 0 483159485 27025408 6030 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6598 6030 603 41 0 6557 0
vsize: 26392
[startup+170.009 s]
Raw data (loadavg): 0.99 1.01 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6113 0 0 0 16983 16 0 0 25 0 1 0 483159485 27025408 6036 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6598 6036 603 41 0 6557 0
vsize: 26392
[startup+180.008 s]
Raw data (loadavg): 0.99 1.01 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6113 0 0 0 17983 16 0 0 25 0 1 0 483159485 27025408 6036 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6598 6036 603 41 0 6557 0
vsize: 26392
[startup+190.009 s]
Raw data (loadavg): 0.99 1.01 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6281 0 0 0 18983 16 0 0 25 0 1 0 483159485 27693056 6204 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6761 6204 603 41 0 6720 0
vsize: 27044
[startup+200.009 s]
Raw data (loadavg): 0.99 1.01 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6454 0 0 0 19982 17 0 0 25 0 1 0 483159485 28389376 6377 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6931 6377 603 41 0 6890 0
vsize: 27724
[startup+210.009 s]
Raw data (loadavg): 0.99 1.01 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6635 0 0 0 20982 18 0 0 25 0 1 0 483159485 29200384 6558 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7129 6558 603 41 0 7088 0
vsize: 28516
[startup+220.009 s]
Raw data (loadavg): 0.99 1.01 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6784 0 0 0 21982 18 0 0 25 0 1 0 483159485 29736960 6707 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7260 6707 603 41 0 7219 0
vsize: 29040
[startup+230.009 s]
Raw data (loadavg): 0.99 1.01 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 6923 0 0 0 22982 18 0 0 25 0 1 0 483159485 30404608 6846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7423 6846 603 41 0 7382 0
vsize: 29692
[startup+240.01 s]
Raw data (loadavg): 0.99 1.01 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7043 0 0 0 23982 19 0 0 25 0 1 0 483159485 30797824 6966 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7519 6966 603 41 0 7478 0
vsize: 30076
[startup+250.01 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7165 0 0 0 24982 19 0 0 25 0 1 0 483159485 31326208 7088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7648 7088 603 41 0 7607 0
vsize: 30592
[startup+260.01 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7274 0 0 0 25981 19 0 0 25 0 1 0 483159485 31784960 7197 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7760 7197 603 41 0 7719 0
vsize: 31040
[startup+270.011 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7387 0 0 0 26981 20 0 0 25 0 1 0 483159485 32706560 7310 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7985 7310 603 41 0 7944 0
vsize: 31940
[startup+280.01 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7414 0 0 0 27982 20 0 0 25 0 1 0 483159485 32845824 7337 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8019 7337 603 41 0 7978 0
vsize: 32076
[startup+290.011 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7414 0 0 0 28982 20 0 0 25 0 1 0 483159485 32845824 7337 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8019 7337 603 41 0 7978 0
vsize: 32076
[startup+300.012 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7423 0 0 0 29982 20 0 0 25 0 1 0 483159485 32845824 7346 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8019 7346 603 41 0 7978 0
vsize: 32076
[startup+310.012 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7431 0 0 0 30982 20 0 0 25 0 1 0 483159485 32845824 7354 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8019 7354 603 41 0 7978 0
vsize: 32076
[startup+320.012 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7440 0 0 0 31982 20 0 0 25 0 1 0 483159485 32993280 7363 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8055 7363 603 41 0 8014 0
vsize: 32220
[startup+330.013 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7441 0 0 0 32982 20 0 0 25 0 1 0 483159485 32993280 7364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8055 7364 603 41 0 8014 0
vsize: 32220
[startup+340.013 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7464 0 0 0 33983 20 0 0 25 0 1 0 483159485 32993280 7387 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8055 7387 603 41 0 8014 0
vsize: 32220
[startup+350.014 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7475 0 0 0 34983 20 0 0 25 0 1 0 483159485 33189888 7398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7398 603 41 0 8062 0
vsize: 32412
[startup+360.013 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7476 0 0 0 35983 20 0 0 25 0 1 0 483159485 33189888 7399 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7399 603 41 0 8062 0
vsize: 32412
[startup+370.014 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7489 0 0 0 36983 20 0 0 25 0 1 0 483159485 33189888 7412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7412 603 41 0 8062 0
vsize: 32412
[startup+380.014 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7505 0 0 0 37983 20 0 0 25 0 1 0 483159485 33353728 7428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7428 603 41 0 8102 0
vsize: 32572
[startup+390.015 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7507 0 0 0 38983 20 0 0 25 0 1 0 483159485 33353728 7430 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7430 603 41 0 8102 0
vsize: 32572
[startup+400.015 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7510 0 0 0 39983 20 0 0 25 0 1 0 483159485 33353728 7433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7433 603 41 0 8102 0
vsize: 32572
[startup+410.02 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7529 0 0 0 40984 20 0 0 25 0 1 0 483159485 33353728 7452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7452 603 41 0 8102 0
vsize: 32572
[startup+420.021 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7531 0 0 0 41984 20 0 0 25 0 1 0 483159485 33353728 7454 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7454 603 41 0 8102 0
vsize: 32572
[startup+430.021 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7532 0 0 0 42984 20 0 0 25 0 1 0 483159485 33353728 7455 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7455 603 41 0 8102 0
vsize: 32572
[startup+440.022 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7596 0 0 0 43984 20 0 0 25 0 1 0 483159485 33746944 7519 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8239 7519 603 41 0 8198 0
vsize: 32956
[startup+450.022 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7600 0 0 0 44984 20 0 0 25 0 1 0 483159485 33746944 7523 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8239 7523 603 41 0 8198 0
vsize: 32956
[startup+460.021 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7649 0 0 0 45984 20 0 0 25 0 1 0 483159485 33943552 7572 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8287 7572 603 41 0 8246 0
vsize: 33148
[startup+470.022 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7655 0 0 0 46985 20 0 0 25 0 1 0 483159485 33943552 7578 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8287 7578 603 41 0 8246 0
vsize: 33148
[startup+480.022 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7659 0 0 0 47985 20 0 0 25 0 1 0 483159485 33943552 7582 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8287 7582 603 41 0 8246 0
vsize: 33148
[startup+490.022 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7667 0 0 0 48985 20 0 0 25 0 1 0 483159485 34107392 7590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7590 603 41 0 8286 0
vsize: 33308
[startup+500.023 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7667 0 0 0 49985 20 0 0 25 0 1 0 483159485 34107392 7590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7590 603 41 0 8286 0
vsize: 33308
[startup+510.022 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7668 0 0 0 50985 20 0 0 25 0 1 0 483159485 34107392 7591 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7591 603 41 0 8286 0
vsize: 33308
[startup+520.023 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7668 0 0 0 51985 20 0 0 25 0 1 0 483159485 34107392 7591 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7591 603 41 0 8286 0
vsize: 33308
[startup+530.023 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7669 0 0 0 52986 20 0 0 25 0 1 0 483159485 34107392 7592 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7592 603 41 0 8286 0
vsize: 33308
[startup+540.024 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7680 0 0 0 53986 20 0 0 25 0 1 0 483159485 34107392 7603 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7603 603 41 0 8286 0
vsize: 33308
[startup+550.023 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7680 0 0 0 54986 20 0 0 25 0 1 0 483159485 34107392 7603 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7603 603 41 0 8286 0
vsize: 33308
[startup+560.024 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7688 0 0 0 55986 20 0 0 25 0 1 0 483159485 34107392 7611 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7611 603 41 0 8286 0
vsize: 33308
[startup+570.024 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7690 0 0 0 56986 20 0 0 25 0 1 0 483159485 34107392 7613 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7613 603 41 0 8286 0
vsize: 33308
[startup+580.025 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7721 0 0 0 57986 20 0 0 25 0 1 0 483159485 34242560 7644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8360 7644 603 41 0 8319 0
vsize: 33440
[startup+590.025 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7785 0 0 0 58986 20 0 0 25 0 1 0 483159485 34512896 7708 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8426 7708 603 41 0 8385 0
vsize: 33704
[startup+600.026 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7854 0 0 0 59986 21 0 0 25 0 1 0 483159485 34811904 7777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8499 7777 603 41 0 8458 0
vsize: 33996
[startup+610.025 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7922 0 0 0 60986 21 0 0 25 0 1 0 483159485 35078144 7845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8564 7845 603 41 0 8523 0
vsize: 34256
[startup+620.025 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7936 0 0 0 61986 21 0 0 25 0 1 0 483159485 35078144 7859 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8564 7859 603 41 0 8523 0
vsize: 34256
[startup+630.025 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7943 0 0 0 62986 21 0 0 25 0 1 0 483159485 35213312 7866 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7866 603 41 0 8556 0
vsize: 34388
[startup+640.026 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7957 0 0 0 63986 21 0 0 25 0 1 0 483159485 35213312 7880 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7880 603 41 0 8556 0
vsize: 34388
[startup+650.026 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7960 0 0 0 64987 21 0 0 25 0 1 0 483159485 35213312 7883 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7883 603 41 0 8556 0
vsize: 34388
[startup+660.026 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7976 0 0 0 65987 22 0 0 25 0 1 0 483159485 35213312 7899 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7899 603 41 0 8556 0
vsize: 34388
[startup+670.026 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7992 0 0 0 66987 22 0 0 25 0 1 0 483159485 35409920 7915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7915 603 41 0 8604 0
vsize: 34580
[startup+680.033 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7994 0 0 0 67988 22 0 0 25 0 1 0 483159485 35409920 7917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7917 603 41 0 8604 0
vsize: 34580
[startup+690.034 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7995 0 0 0 68988 22 0 0 25 0 1 0 483159485 35409920 7918 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7918 603 41 0 8604 0
vsize: 34580
[startup+700.034 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7996 0 0 0 69988 22 0 0 25 0 1 0 483159485 35409920 7919 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7919 603 41 0 8604 0
vsize: 34580
[startup+710.034 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 7996 0 0 0 70988 22 0 0 25 0 1 0 483159485 35409920 7919 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7919 603 41 0 8604 0
vsize: 34580
[startup+720.035 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8001 0 0 0 71988 22 0 0 25 0 1 0 483159485 35409920 7924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7924 603 41 0 8604 0
vsize: 34580
[startup+730.034 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8002 0 0 0 72988 22 0 0 25 0 1 0 483159485 35409920 7925 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7925 603 41 0 8604 0
vsize: 34580
[startup+740.034 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8004 0 0 0 73989 22 0 0 25 0 1 0 483159485 35409920 7927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7927 603 41 0 8604 0
vsize: 34580
[startup+750.035 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8004 0 0 0 74989 22 0 0 25 0 1 0 483159485 35409920 7927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7927 603 41 0 8604 0
vsize: 34580
[startup+760.035 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8005 0 0 0 75989 22 0 0 25 0 1 0 483159485 35409920 7928 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7928 603 41 0 8604 0
vsize: 34580
[startup+770.035 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8030 0 0 0 76989 22 0 0 25 0 1 0 483159485 35606528 7953 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7953 603 41 0 8652 0
vsize: 34772
[startup+780.036 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8037 0 0 0 77989 22 0 0 25 0 1 0 483159485 35606528 7960 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7960 603 41 0 8652 0
vsize: 34772
[startup+790.036 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8041 0 0 0 78989 22 0 0 25 0 1 0 483159485 35606528 7964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7964 603 41 0 8652 0
vsize: 34772
[startup+800.036 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8043 0 0 0 79989 22 0 0 25 0 1 0 483159485 35606528 7966 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7966 603 41 0 8652 0
vsize: 34772
[startup+810.036 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8045 0 0 0 80989 22 0 0 25 0 1 0 483159485 35606528 7968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7968 603 41 0 8652 0
vsize: 34772
[startup+820.037 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8048 0 0 0 81990 22 0 0 25 0 1 0 483159485 35606528 7971 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7971 603 41 0 8652 0
vsize: 34772
[startup+830.037 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8051 0 0 0 82990 22 0 0 25 0 1 0 483159485 35606528 7974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7974 603 41 0 8652 0
vsize: 34772
[startup+840.038 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8051 0 0 0 83990 22 0 0 25 0 1 0 483159485 35606528 7974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7974 603 41 0 8652 0
vsize: 34772
[startup+850.037 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8051 0 0 0 84990 22 0 0 25 0 1 0 483159485 35606528 7974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7974 603 41 0 8652 0
vsize: 34772
[startup+860.037 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8061 0 0 0 85990 22 0 0 25 0 1 0 483159485 35606528 7984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7984 603 41 0 8652 0
vsize: 34772
[startup+870.038 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8108 0 0 0 86991 22 0 0 25 0 1 0 483159485 35835904 8031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8749 8031 603 41 0 8708 0
vsize: 34996
[startup+880.038 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8142 0 0 0 87991 22 0 0 25 0 1 0 483159485 36032512 8065 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8797 8065 603 41 0 8756 0
vsize: 35188
[startup+890.039 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8181 0 0 0 88991 22 0 0 25 0 1 0 483159485 36229120 8104 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8845 8104 603 41 0 8804 0
vsize: 35380
[startup+900.039 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8215 0 0 0 89991 22 0 0 25 0 1 0 483159485 36425728 8138 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8893 8138 603 41 0 8852 0
vsize: 35572
[startup+910.039 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8216 0 0 0 90991 22 0 0 25 0 1 0 483159485 36425728 8139 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8893 8139 603 41 0 8852 0
vsize: 35572
[startup+920.039 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8217 0 0 0 91991 22 0 0 25 0 1 0 483159485 36425728 8140 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8893 8140 603 41 0 8852 0
vsize: 35572
[startup+930.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8254 0 0 0 92991 23 0 0 25 0 1 0 483159485 36622336 8177 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8941 8177 603 41 0 8900 0
vsize: 35764
[startup+940.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8267 0 0 0 93991 23 0 0 25 0 1 0 483159485 36622336 8190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8941 8190 603 41 0 8900 0
vsize: 35764
[startup+950.041 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8267 0 0 0 94991 23 0 0 25 0 1 0 483159485 36622336 8190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8941 8190 603 41 0 8900 0
vsize: 35764
[startup+960.041 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8268 0 0 0 95991 23 0 0 25 0 1 0 483159485 36622336 8191 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8941 8191 603 41 0 8900 0
vsize: 35764
[startup+970.042 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8306 0 0 0 96992 23 0 0 25 0 1 0 483159485 36884480 8229 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8229 603 41 0 8964 0
vsize: 36020
[startup+980.042 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8314 0 0 0 97992 23 0 0 25 0 1 0 483159485 36884480 8237 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8237 603 41 0 8964 0
vsize: 36020
[startup+990.043 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8315 0 0 0 98992 23 0 0 25 0 1 0 483159485 36884480 8238 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8238 603 41 0 8964 0
vsize: 36020
[startup+1000.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8328 0 0 0 99992 23 0 0 25 0 1 0 483159485 36884480 8251 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8251 603 41 0 8964 0
vsize: 36020
[startup+1010.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8328 0 0 0 100992 23 0 0 25 0 1 0 483159485 36884480 8251 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8251 603 41 0 8964 0
vsize: 36020
[startup+1020.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8329 0 0 0 101992 23 0 0 25 0 1 0 483159485 36884480 8252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8252 603 41 0 8964 0
vsize: 36020
[startup+1030.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8330 0 0 0 102993 23 0 0 25 0 1 0 483159485 36884480 8253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8253 603 41 0 8964 0
vsize: 36020
[startup+1040.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8488 0 0 0 103992 23 0 0 25 0 1 0 483159485 37683200 8411 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9200 8411 603 41 0 9159 0
vsize: 36800
[startup+1050.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8670 0 0 0 104992 23 0 0 25 0 1 0 483159485 38359040 8593 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8593 603 41 0 9324 0
vsize: 37460
[startup+1060.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8670 0 0 0 105992 23 0 0 25 0 1 0 483159485 38359040 8593 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8593 603 41 0 9324 0
vsize: 37460
[startup+1070.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8670 0 0 0 106993 23 0 0 25 0 1 0 483159485 38359040 8593 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8593 603 41 0 9324 0
vsize: 37460
[startup+1080.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8670 0 0 0 107993 23 0 0 25 0 1 0 483159485 38359040 8593 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8593 603 41 0 9324 0
vsize: 37460
[startup+1090.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8670 0 0 0 108993 23 0 0 25 0 1 0 483159485 38359040 8593 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8593 603 41 0 9324 0
vsize: 37460
[startup+1100.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8671 0 0 0 109993 23 0 0 25 0 1 0 483159485 38359040 8594 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8594 603 41 0 9324 0
vsize: 37460
[startup+1110.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8671 0 0 0 110994 23 0 0 25 0 1 0 483159485 38359040 8594 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8594 603 41 0 9324 0
vsize: 37460
[startup+1120.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8671 0 0 0 111994 23 0 0 25 0 1 0 483159485 38359040 8594 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8594 603 41 0 9324 0
vsize: 37460
[startup+1130.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8671 0 0 0 112994 23 0 0 25 0 1 0 483159485 38359040 8594 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8594 603 41 0 9324 0
vsize: 37460
[startup+1140.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8671 0 0 0 113994 23 0 0 25 0 1 0 483159485 38359040 8594 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8594 603 41 0 9324 0
vsize: 37460
[startup+1150.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8677 0 0 0 114994 24 0 0 25 0 1 0 483159485 38359040 8600 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8600 603 41 0 9324 0
vsize: 37460
[startup+1160.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8684 0 0 0 115994 24 0 0 25 0 1 0 483159485 38522880 8607 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 8607 603 41 0 9364 0
vsize: 37620
[startup+1170.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8691 0 0 0 116995 24 0 0 25 0 1 0 483159485 38522880 8614 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 8614 603 41 0 9364 0
vsize: 37620
[startup+1180.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8701 0 0 0 117995 24 0 0 25 0 1 0 483159485 38522880 8624 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 8624 603 41 0 9364 0
vsize: 37620
[startup+1190.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8706 0 0 0 118995 24 0 0 25 0 1 0 483159485 38522880 8629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 8629 603 41 0 9364 0
vsize: 37620
[startup+1200.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 27088
Raw data (stat): 27088 (minisat+) R 27087 29151 29150 0 -1 0 8706 0 0 0 119995 24 0 0 25 0 1 0 483159485 38522880 8629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 8629 603 41 0 9364 0
vsize: 37620
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 1.00 0.96 1/54 27088
Raw data (stat): 27088 (minisat+) Z 27087 29151 29150 0 -1 12 8708 0 0 0 119995 25 0 0 25 0 1 0 483159485 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.22
CPU user time (s): 1199.96
CPU system time (s): 0.25896
CPU usage (%): 100.012
Max. virtual memory (Kb): 37620
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####