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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-dcmulti.opb
MD5SUM	659e380dd1d6168ad99a794b3190043f
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	14235
Biggest coefficient in the objective function	714038312960
Number of bits for the biggest coefficient in the objective function	40
Sum of the numbers in the objective function	68224730472397
Number of bits of the sum of numbers in the objective function	46
Biggest number in a constraint	714038312960
Number of bits of the biggest number in a constraint	40
Biggest sum of numbers in a constraint	68224730472397
Number of bits of the biggest sum of numbers	46
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.12198
Number of variables	14265
Total number of constraints	365
Number of constraints which are clauses	27
Number of constraints which are cardinality constraints (but not clauses)	80
Number of constraints which are nor clauses,nor cardinality constraints	258
Minimum length of a constraint	1
Maximum length of a constraint	420
Trace number 30809

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-05-25 19:45:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22207 boxname=wulflinc3 idbench=1023 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  659e380dd1d6168ad99a794b3190043f  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-dcmulti.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-dcmulti.opb
IDLAUNCH: 22207
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        909416 kB
Buffers:          5464 kB
Cached:         100596 kB
SwapCached:         20 kB
Active:          40356 kB
Inactive:        68396 kB
HighTotal:      131008 kB
HighFree:        27160 kB
LowTotal:       903652 kB
LowFree:        882256 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6576 kB
Slab:            11024 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 20:05:51 (client local time) WITH STATUS 152 IN 1229.9 SECONDS
stats: 22207 7 1229.9 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 368 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): s....s.....sssssssssssssssssss....s.....ssssssssssssssssss....s.....sssssssssssssssssss
c ---[ 427]---> BDD-cost:   17
c ---[ 426]---> Sorter-cost: 1377     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> BDD-cost:   18
c ---[ 421]---> BDD-cost:   17
c ---[ 420]---> BDD-cost:   17
c ---[ 419]---> BDD-cost:   16
c ---[ 418]---> BDD-cost:   17
c ---[ 416]---> Adder-cost: 523   maxlim: 2097148   bits: 22/21
c ---[ 415]---> BDD-cost:   17
c ---[ 413]---> Adder-cost: 523   maxlim: 1703932   bits: 22/21
c ---[ 411]---> Adder-cost: 523   maxlim: 2097148   bits: 22/21
c ---[ 409]---> Adder-cost: 523   maxlim: 1703932   bits: 22/21
c ---[ 407]---> Adder-cost: 523   maxlim: 2097148   bits: 22/21
c ---[ 405]---> Adder-cost: 523   maxlim: 1703932   bits: 22/21
c ---[ 403]---> Adder-cost: 523   maxlim: 2097148   bits: 22/21
c ---[ 401]---> Adder-cost: 523   maxlim: 1703932   bits: 22/21
c ---[ 399]---> Adder-cost: 523   maxlim: 2097148   bits: 22/21
c ---[ 397]---> Adder-cost: 523   maxlim: 1703932   bits: 22/21
c ---[ 395]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> BDD-cost:   16
c ---[ 392]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> BDD-cost:   19
c ---[ 390]---> BDD-cost:    7
c ---[ 389]---> BDD-cost:   18
c ---[ 388]---> BDD-cost:    4
c ---[ 386]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> BDD-cost:   27
c ---[ 384]---> BDD-cost:    6
c ---[ 381]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> BDD-cost:   17
c ---[ 378]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> BDD-cost:   19
c ---[ 376]---> BDD-cost:    7
c ---[ 375]---> BDD-cost:   18
c ---[ 374]---> BDD-cost:    4
c ---[ 372]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> BDD-cost:   26
c ---[ 370]---> BDD-cost:    8
c ---[ 367]---> Sorter-cost: 1113     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Adder-cost: 463   maxlim: 1048573   bits: 21/20
c ---[ 363]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> BDD-cost:   18
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   17
c ---[ 359]---> BDD-cost:    3
c ---[ 357]---> Sorter-cost: 1054     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> BDD-cost:   26
c ---[ 355]---> BDD-cost:    6
c ---[ 352]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Adder-cost: 463   maxlim: 655357   bits: 21/20
c ---[ 348]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 347]---> BDD-cost:   19
c ---[ 346]---> BDD-cost:    7
c ---[ 345]---> BDD-cost:   18
c ---[ 344]---> BDD-cost:    4
c ---[ 342]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> BDD-cost:   27
c ---[ 340]---> BDD-cost:    6
c ---[ 337]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 335]---> Adder-cost: 463   maxlim: 1048573   bits: 21/20
c ---[ 333]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> BDD-cost:   19
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:   18
c ---[ 329]---> BDD-cost:    4
c ---[ 327]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> BDD-cost:   22
c ---[ 322]---> BDD-cost:   33
c ---[ 320]---> Adder-cost: 463   maxlim: 655357   bits: 21/20
c ---[ 308]---> Adder-cost: 463   maxlim: 1048573   bits: 21/20
c ---[ 296]---> Adder-cost: 463   maxlim: 655357   bits: 21/20
c ---[ 293]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost: 1551     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost: 1377     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 289]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> BDD-cost:   18
c ---[ 285]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 283]---> Adder-cost: 463   maxlim: 1048573   bits: 21/20
c ---[ 282]---> BDD-cost:   17
c ---[ 281]---> BDD-cost:   17
c ---[ 280]---> BDD-cost:   16
c ---[ 279]---> BDD-cost:   17
c ---[ 277]---> Adder-cost: 500   maxlim: 3145724   bits: 23/22
c ---[ 275]---> Adder-cost: 500   maxlim: 2752508   bits: 23/22
c ---[ 273]---> Adder-cost: 500   maxlim: 3145724   bits: 23/22
c ---[ 271]---> Adder-cost: 500   maxlim: 2752508   bits: 23/22
c ---[ 269]---> Adder-cost: 500   maxlim: 3145724   bits: 23/22
c ---[ 267]---> Adder-cost: 500   maxlim: 2752508   bits: 23/22
c ---[ 265]---> Adder-cost: 463   maxlim: 655357   bits: 21/20
c ---[ 263]---> Adder-cost: 500   maxlim: 3145724   bits: 23/22
c ---[ 261]---> Adder-cost: 500   maxlim: 2752508   bits: 23/22
c ---[ 259]---> Adder-cost: 500   maxlim: 3145724   bits: 23/22
c ---[ 257]---> Adder-cost: 500   maxlim: 2752508   bits: 23/22
c ---[ 255]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> BDD-cost:   19
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:   18
c ---[ 249]---> BDD-cost:    4
c ---[ 247]---> Adder-cost: 463   maxlim: 1048573   bits: 21/20
c ---[ 245]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> BDD-cost:   27
c ---[ 243]---> BDD-cost:    6
c ---[ 240]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 238]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 237]---> BDD-cost:   19
c ---[ 236]---> BDD-cost:    7
c ---[ 235]---> BDD-cost:   18
c ---[ 234]---> BDD-cost:    4
c ---[ 232]---> Adder-cost: 463   maxlim: 655357   bits: 21/20
c ---[ 230]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:    8
c ---[ 225]---> Sorter-cost: 1113     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 222]---> BDD-cost:   18
c ---[ 221]---> BDD-cost:    6
c ---[ 220]---> BDD-cost:   17
c ---[ 219]---> BDD-cost:    3
c ---[ 217]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost: 1054     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 214]---> BDD-cost:   26
c ---[ 213]---> BDD-cost:    6
c ---[ 210]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 208]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> BDD-cost:   19
c ---[ 206]---> BDD-cost:    7
c ---[ 205]---> BDD-cost:   18
c ---[ 204]---> BDD-cost:    4
c ---[ 202]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> BDD-cost:   27
c ---[ 198]---> BDD-cost:    6
c ---[ 195]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> BDD-cost:   19
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:   18
c ---[ 189]---> BDD-cost:    4
c ---[ 188]---> BDD-cost:   19
c ---[ 186]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   22
c ---[ 181]---> BDD-cost:   33
c ---[ 175]---> BDD-cost:    7
c ---[ 164]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    4
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> BDD-cost:   27
c ---[ 146]---> BDD-cost:    6
c ---[ 143]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> BDD-cost:   19
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   18
c ---[ 137]---> BDD-cost:    4
c ---[ 136]---> Sorter-cost: 1551     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> BDD-cost:   26
c ---[ 132]---> BDD-cost:    8
c ---[ 129]---> Sorter-cost: 1113     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> BDD-cost:   18
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:   17
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> Sorter-cost: 1377     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 1054     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> BDD-cost:   26
c ---[ 118]---> BDD-cost:    6
c ---[ 115]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> BDD-cost:   19
c ---[ 111]---> BDD-cost:    7
c ---[ 110]---> BDD-cost:   18
c ---[ 109]---> BDD-cost:    4
c ---[ 108]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> BDD-cost:   27
c ---[ 104]---> BDD-cost:    6
c ---[ 101]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> BDD-cost:   19
c ---[  97]---> BDD-cost:    7
c ---[  96]---> BDD-cost:   18
c ---[  95]---> BDD-cost:    4
c ---[  94]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> BDD-cost:   22
c ---[  87]---> BDD-cost:   33
c ---[  70]---> BDD-cost:   18
c ---[  62]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost: 1551     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:    5
c ---[  57]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1039     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  942     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1054     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  50]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost:  965     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  878     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  965     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost: 1026     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  886     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  855     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost: 1100     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:    5
c ---[  37]---> Sorter-cost: 1003     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  929     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost: 1087     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost: 1016     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost: 1087     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  929     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost: 1003     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> BDD-cost:    5
c ---[  18]---> Sorter-cost:  919     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> BDD-cost:   15
c ---[  16]---> Sorter-cost:  822     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost: 1003     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost: 1052     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  896     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  878     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  842     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost: 1100     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  929     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  822     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  852     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost: 1064     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  919     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  407659  1078157 |  135886       0        0     nan |  0.000 % |
c |       100 |  407640  1078115 |  149474      99      275     2.8 |  6.241 % |
c |       250 |  407421  1077629 |  164422     214      597     2.8 |  6.288 % |
c |       476 |  407230  1077203 |  180864     417     1295     3.1 |  6.331 % |
c |       814 |  407010  1076714 |  198950     728     2340     3.2 |  6.410 % |
c |      1320 |  406574  1075744 |  218845    1162     3846     3.3 |  6.475 % |
c |      2079 |  405501  1073358 |  240730    1770     6153     3.5 |  6.717 % |
c |      3218 |  404456  1071032 |  264803    2786     9745     3.5 |  6.951 % |
c |      4926 |  403134  1068083 |  291283    4259    14929     3.5 |  7.237 % |
c |      7488 |  401682  1064841 |  320412    6633    24359     3.7 |  7.552 % |
c |     11333 |  400157  1061429 |  352453   10286    45629     4.4 |  7.886 % |
c |     17104 |  399646  1060290 |  387698   15961   163733    10.3 |  7.996 % |
c |     25753 |  399275  1059467 |  426468   24558   453474    18.5 |  8.080 % |
c |     38730 |  398228  1057131 |  469115   37369   866938    23.2 |  8.307 % |
c |     58192 |  397042  1054454 |  516026   56692  1511359    26.7 |  8.577 % |
c |     87384 |  396904  1054146 |  567629   85866  2730385    31.8 |  8.607 % |
c |    131173 |  396253  1052687 |  624392  129572  4392719    33.9 |  8.750 % |
c |    196857 |  395205  1050318 |  686831  195116  7086771    36.3 |  8.981 % |
c |    295385 |  393580  1046653 |  755514  293406 11407186    38.9 |  9.345 % |
c |    443176 |  392147  1043423 |  831066  440985 17836572    40.4 |  9.667 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  3969 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.94 2/54 3965
Raw data (stat): 3965 (runsolver) R 3964 20224 20223 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783273549 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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+9.9999 s]
Raw data (loadavg): 0.93 0.96 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.96 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0013 s]
Raw data (loadavg): 0.96 0.96 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.96 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.96 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.96 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.004 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0039 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 3969
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4022
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4022
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4022
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4022
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4022
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4022
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4022
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4022
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4024
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4026
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 4026
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.76 s]
Raw data (loadavg): 0.99 0.97 0.94 1/53 4026
Raw data (stat): 3965 (minisat+_script) S 3964 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783273549 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.76
CPU time (s): 1229.9
CPU user time (s): 1228.71
CPU system time (s): 1.18682
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####