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-l152lav.opb
MD5SUM	9d4ce12b138a2bef65a1f401ec9d1f01
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4742
Optimality of the best value was proved	NO
Number of terms in the objective function	1989
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	382524
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	268
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	382524
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.33
Number of variables	1989
Total number of constraints	2086
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2085
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1989
Trace number 21407

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 23:44:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13492 boxname=wulflinc29 idbench=1038 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9d4ce12b138a2bef65a1f401ec9d1f01  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-l152lav.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-l152lav.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-l152lav.opb
IDLAUNCH: 13492
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        575748 kB
Buffers:         31660 kB
Cached:         400936 kB
SwapCached:       4304 kB
Active:          89484 kB
Inactive:       348888 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        575496 kB
SwapTotal:     2097892 kB
SwapFree:      2092680 kB
Dirty:              48 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            14972 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 00:04:45 (client local time) WITH STATUS 0 IN 1200.35 SECONDS
stats: 13492 7 1200.35 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 192]---> Adder-cost: 5478   maxlim: 25152   bits: 15/15
c ---[ 190]---> BDD-cost:    3
c ---[ 188]---> BDD-cost:  255
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:   83
c ---[ 182]---> BDD-cost:   93
c ---[ 180]---> BDD-cost:  149
c ---[ 178]---> BDD-cost:  235
c ---[ 176]---> BDD-cost:  339
c ---[ 174]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:  301
c ---[ 168]---> BDD-cost:  181
c ---[ 166]---> BDD-cost:   87
c ---[ 164]---> BDD-cost:   71
c ---[ 162]---> BDD-cost:   67
c ---[ 160]---> BDD-cost:   57
c ---[ 158]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:   39
c ---[ 154]---> BDD-cost:   85
c ---[ 152]---> BDD-cost:  147
c ---[ 150]---> BDD-cost:  189
c ---[ 148]---> BDD-cost:  211
c ---[ 146]---> BDD-cost:   95
c ---[ 144]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   35
c ---[ 140]---> BDD-cost:   59
c ---[ 138]---> BDD-cost:  171
c ---[ 136]---> BDD-cost:   59
c ---[ 134]---> BDD-cost:   51
c ---[ 132]---> BDD-cost:  151
c ---[ 130]---> BDD-cost:  147
c ---[ 128]---> BDD-cost:  317
c ---[ 126]---> BDD-cost:  201
c ---[ 124]---> BDD-cost:  105
c ---[ 122]---> BDD-cost:  101
c ---[ 120]---> BDD-cost:  121
c ---[ 118]---> BDD-cost:  133
c ---[ 116]---> BDD-cost:  149
c ---[ 114]---> BDD-cost:  189
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:  201
c ---[ 108]---> BDD-cost:   49
c ---[ 106]---> BDD-cost:   81
c ---[ 104]---> BDD-cost:  121
c ---[ 102]---> BDD-cost:  433
c ---[ 100]---> BDD-cost:  191
c ---[  98]---> BDD-cost:   81
c ---[  96]---> BDD-cost:   71
c ---[  94]---> BDD-cost:  103
c ---[  92]---> BDD-cost:   93
c ---[  90]---> BDD-cost:   85
c ---[  88]---> BDD-cost:  189
c ---[  86]---> BDD-cost:  231
c ---[  84]---> BDD-cost:  101
c ---[  82]---> BDD-cost:  109
c ---[  80]---> BDD-cost:  171
c ---[  78]---> BDD-cost:  183
c ---[  76]---> BDD-cost:  173
c ---[  74]---> BDD-cost:  239
c ---[  72]---> BDD-cost:   91
c ---[  70]---> BDD-cost:  271
c ---[  68]---> BDD-cost:  239
c ---[  66]---> BDD-cost:  105
c ---[  64]---> BDD-cost:  117
c ---[  62]---> BDD-cost:  221
c ---[  60]---> BDD-cost:  213
c ---[  58]---> BDD-cost:  145
c ---[  56]---> BDD-cost:  179
c ---[  54]---> BDD-cost:  213
c ---[  52]---> BDD-cost:  143
c ---[  50]---> BDD-cost:  209
c ---[  48]---> BDD-cost:   81
c ---[  46]---> BDD-cost:  205
c ---[  44]---> BDD-cost:   61
c ---[  42]---> BDD-cost:  225
c ---[  40]---> BDD-cost:  129
c ---[  38]---> BDD-cost:  253
c ---[  36]---> BDD-cost:   71
c ---[  34]---> BDD-cost:  203
c ---[  32]---> BDD-cost:   45
c ---[  30]---> BDD-cost:  133
c ---[  28]---> BDD-cost:  323
c ---[  26]---> BDD-cost:  155
c ---[  24]---> BDD-cost:   89
c ---[  22]---> BDD-cost:   93
c ---[  20]---> BDD-cost:   83
c ---[  18]---> BDD-cost:   67
c ---[  16]---> BDD-cost:  133
c ---[  14]---> BDD-cost:  247
c ---[  12]---> BDD-cost:   97
c ---[  10]---> BDD-cost:   97
c ---[   8]---> BDD-cost:  151
c ---[   6]---> BDD-cost:  181
c ---[   4]---> BDD-cost:  151
c ---[   2]---> BDD-cost:  181
c ---[   0]---> Adder-cost: 3598   maxlim: 1961   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   97126   314221 |   29137       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24129          
c   -- var.elim.:  2000/24129          
c   -- var.elim.:  3000/24129          
c   -- var.elim.:  4000/24129          
c   -- var.elim.:  5000/24129          
c   -- var.elim.:  6000/24129          
c   -- var.elim.:  7000/24129          
c   -- var.eli#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.79 0.95 0.95 2/54 9142
Raw data (stat): 9142 (runsolver) R 9141 27222 27221 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 549136289 1052672 97 4294967295 134512640 135381576 3221224432 3221219804 135024803 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+9.9997 s]
Raw data (loadavg): 0.82 0.95 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 6477 0 0 0 985 14 0 0 25 0 1 0 549136289 27369472 5576 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6682 5576 603 41 0 6641 0
vsize: 26728
[startup+20.0009 s]
Raw data (loadavg): 0.85 0.95 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 6869 0 0 0 1983 15 0 0 25 0 1 0 549136289 28954624 5968 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7069 5968 603 41 0 7028 0
vsize: 28276
[startup+30.0013 s]
Raw data (loadavg): 0.87 0.95 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 7320 0 0 0 2982 17 0 0 25 0 1 0 549136289 30822400 6419 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7525 6419 603 41 0 7484 0
vsize: 30100
[startup+40.0021 s]
Raw data (loadavg): 0.89 0.95 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 7894 0 0 0 3981 18 0 0 25 0 1 0 549136289 33189888 6993 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 6993 603 41 0 8062 0
vsize: 32412
[startup+50.0033 s]
Raw data (loadavg): 0.91 0.96 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 8546 0 0 0 4979 20 0 0 25 0 1 0 549136289 35831808 7645 4294967295 134512640 134672761 3221224544 3221223584 134603540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8748 7645 603 41 0 8707 0
vsize: 34992
[startup+60.0027 s]
Raw data (loadavg): 0.92 0.96 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 9259 0 0 0 5977 23 0 0 25 0 1 0 549136289 38703104 8358 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9449 8358 603 41 0 9408 0
vsize: 37796
[startup+70.0034 s]
Raw data (loadavg): 0.93 0.96 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 10181 0 0 0 6974 25 0 0 25 0 1 0 549136289 42516480 9280 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10380 9280 603 41 0 10339 0
vsize: 41520
[startup+80.0036 s]
Raw data (loadavg): 0.94 0.96 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 11870 0 0 0 7969 30 0 0 25 0 1 0 549136289 49479680 10969 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12080 10969 603 41 0 12039 0
vsize: 48320
[startup+90.004 s]
Raw data (loadavg): 0.95 0.96 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 12527 0 0 0 8968 32 0 0 25 0 1 0 549136289 52252672 11626 4294967295 134512640 134672761 3221224544 3221223736 134610749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12757 11626 603 41 0 12716 0
vsize: 51028
[startup+100.004 s]
Raw data (loadavg): 0.96 0.96 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 13439 0 0 0 9965 35 0 0 25 0 1 0 549136289 55947264 12538 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13659 12538 603 41 0 13618 0
vsize: 54636
[startup+110.004 s]
Raw data (loadavg): 0.96 0.96 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 14305 0 0 0 10963 37 0 0 25 0 1 0 549136289 59408384 13404 4294967295 134512640 134672761 3221224544 3221223688 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14504 13404 603 41 0 14463 0
vsize: 58016
[startup+120.004 s]
Raw data (loadavg): 0.97 0.96 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 14879 0 0 0 11961 39 0 0 25 0 1 0 549136289 61792256 13978 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15086 13978 603 41 0 15045 0
vsize: 60344
[startup+130.004 s]
Raw data (loadavg): 0.97 0.96 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 16304 0 0 0 12958 42 0 0 25 0 1 0 549136289 67579904 15403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16499 15403 603 41 0 16458 0
vsize: 65996
[startup+140.005 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 17528 0 0 0 13955 46 0 0 25 0 1 0 549136289 72577024 16627 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17719 16627 603 41 0 17678 0
vsize: 70876
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 18425 0 0 0 14952 49 0 0 25 0 1 0 549136289 76259328 17524 4294967295 134512640 134672761 3221224544 3221223680 134614518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18618 17524 603 41 0 18577 0
vsize: 74472
[startup+160.006 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 19640 0 0 0 15949 52 0 0 25 0 1 0 549136289 81272832 18739 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19842 18739 603 41 0 19801 0
vsize: 79368
[startup+170.007 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 20679 0 0 0 16947 54 0 0 25 0 1 0 549136289 85467136 19778 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20866 19778 603 41 0 20825 0
vsize: 83464
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 21895 0 0 0 17943 58 0 0 25 0 1 0 549136289 90734592 20994 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22152 20994 603 41 0 22111 0
vsize: 88608
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 23139 0 0 0 18940 61 0 0 25 0 1 0 549136289 95870976 22238 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23406 22238 603 41 0 23365 0
vsize: 93624
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 24073 0 0 0 19938 63 0 0 25 0 1 0 549136289 99573760 23172 4294967295 134512640 134672761 3221224544 3221223744 134610614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24310 23172 603 41 0 24269 0
vsize: 97240
[startup+210.008 s]
Raw data (loadavg): 1.07 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 25315 0 0 0 20934 67 0 0 25 0 1 0 549136289 104701952 24414 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25562 24414 603 41 0 25521 0
vsize: 102248
[startup+220.008 s]
Raw data (loadavg): 1.06 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 27266 0 0 0 21931 71 0 0 25 0 1 0 549136289 112689152 26365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27512 26365 603 41 0 27471 0
vsize: 110048
[startup+230.008 s]
Raw data (loadavg): 1.05 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 27810 0 0 0 22929 73 0 0 25 0 1 0 549136289 114900992 26909 4294967295 134512640 134672761 3221224544 3221223412 1074972064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28052 26909 603 41 0 28011 0
vsize: 112208
[startup+240.009 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 28945 0 0 0 23926 76 0 0 25 0 1 0 549136289 119492608 28044 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29173 28044 603 41 0 29132 0
vsize: 116692
[startup+250.01 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 30275 0 0 0 24923 80 0 0 25 0 1 0 549136289 124956672 29374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30507 29374 603 41 0 30466 0
vsize: 122028
[startup+260.01 s]
Raw data (loadavg): 1.03 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 31215 0 0 0 25919 83 0 0 25 0 1 0 549136289 128868352 30314 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31462 30314 603 41 0 31421 0
vsize: 125848
[startup+270.01 s]
Raw data (loadavg): 1.02 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 32189 0 0 0 26916 86 0 0 25 0 1 0 549136289 132829184 31288 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32429 31288 603 41 0 32388 0
vsize: 129716
[startup+280.011 s]
Raw data (loadavg): 1.02 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 33133 0 0 0 27914 89 0 0 25 0 1 0 549136289 136658944 32232 4294967295 134512640 134672761 3221224544 3221223584 134614286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33364 32232 603 41 0 33323 0
vsize: 133456
[startup+290.012 s]
Raw data (loadavg): 1.02 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 34062 0 0 0 28912 91 0 0 25 0 1 0 549136289 140468224 33161 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34294 33161 603 41 0 34253 0
vsize: 137176
[startup+300.013 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 34872 0 0 0 29910 93 0 0 25 0 1 0 549136289 143777792 33971 4294967295 134512640 134672761 3221224544 3221223728 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35102 33971 603 41 0 35061 0
vsize: 140408
[startup+310.013 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 35914 0 0 0 30907 97 0 0 25 0 1 0 549136289 147988480 35013 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36130 35013 603 41 0 36089 0
vsize: 144520
[startup+320.014 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 36940 0 0 0 31905 99 0 0 25 0 1 0 549136289 152199168 36039 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37158 36039 603 41 0 37117 0
vsize: 148632
[startup+330.013 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 37843 0 0 0 32903 100 0 0 25 0 1 0 549136289 155869184 36942 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38054 36942 603 41 0 38013 0
vsize: 152216
[startup+340.014 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 38919 0 0 0 33900 103 0 0 25 0 1 0 549136289 160362496 38018 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39151 38018 603 41 0 39110 0
vsize: 156604
[startup+350.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 39879 0 0 0 34897 107 0 0 25 0 1 0 549136289 164163584 38978 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40079 38978 603 41 0 40038 0
vsize: 160316
[startup+360.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 41106 0 0 0 35895 109 0 0 25 0 1 0 549136289 169238528 40205 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41318 40205 603 41 0 41277 0
vsize: 165272
[startup+370.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 41620 0 0 0 36894 110 0 0 25 0 1 0 549136289 171339776 40719 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41831 40719 603 41 0 41790 0
vsize: 167324
[startup+380.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 42571 0 0 0 37891 113 0 0 25 0 1 0 549136289 175243264 41670 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42784 41670 603 41 0 42743 0
vsize: 171136
[startup+390.017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 42949 0 0 0 38889 115 0 0 25 0 1 0 549136289 176840704 42048 4294967295 134512640 134672761 3221224544 3221223688 134616123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43174 42048 603 41 0 43133 0
vsize: 172696
[startup+400.017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 43546 0 0 0 39889 116 0 0 25 0 1 0 549136289 179216384 42645 4294967295 134512640 134672761 3221224544 3221223680 134614551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43754 42645 603 41 0 43713 0
vsize: 175016
[startup+410.017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 43886 0 0 0 40888 117 0 0 25 0 1 0 549136289 180555776 42985 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44081 42985 603 41 0 44040 0
vsize: 176324
[startup+420.017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 44196 0 0 0 41887 118 0 0 25 0 1 0 549136289 181862400 43295 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44400 43295 603 41 0 44359 0
vsize: 177600
[startup+430.017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 44529 0 0 0 42887 118 0 0 25 0 1 0 549136289 183169024 43628 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44719 43628 603 41 0 44678 0
vsize: 178876
[startup+440.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 45342 0 0 0 43885 120 0 0 25 0 1 0 549136289 186490880 44441 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45530 44441 603 41 0 45489 0
vsize: 182120
[startup+450.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 46368 0 0 0 44882 123 0 0 25 0 1 0 549136289 190681088 45467 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46553 45467 603 41 0 46512 0
vsize: 186212
[startup+460.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 46858 0 0 0 45881 125 0 0 25 0 1 0 549136289 192798720 45957 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47070 45957 603 41 0 47029 0
vsize: 188280
[startup+470.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 47524 0 0 0 46879 127 0 0 25 0 1 0 549136289 195956736 46623 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47841 46623 603 41 0 47800 0
vsize: 191364
[startup+480.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 48186 0 0 0 47878 128 0 0 25 0 1 0 549136289 198680576 47285 4294967295 134512640 134672761 3221224544 3221223688 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48506 47285 603 41 0 48465 0
vsize: 194024
[startup+490.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 48748 0 0 0 48876 130 0 0 25 0 1 0 549136289 200925184 47847 4294967295 134512640 134672761 3221224544 3221223704 134614557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49054 47847 603 41 0 49013 0
vsize: 196216
[startup+500.02 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 49514 0 0 0 49874 132 0 0 25 0 1 0 549136289 204087296 48613 4294967295 134512640 134672761 3221224544 3221223728 134616001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49826 48613 603 41 0 49785 0
vsize: 199304
[startup+510.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 50551 0 0 0 50871 135 0 0 25 0 1 0 549136289 208297984 49650 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50854 49650 603 41 0 50813 0
vsize: 203416
[startup+520.02 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 51184 0 0 0 51870 136 0 0 25 0 1 0 549136289 210948096 50283 4294967295 134512640 134672761 3221224544 3221223728 134615488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51501 50283 603 41 0 51460 0
vsize: 206004
[startup+530.02 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 52015 0 0 0 52868 139 0 0 25 0 1 0 549136289 214376448 51114 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52338 51114 603 41 0 52297 0
vsize: 209352
[startup+540.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 52672 0 0 0 53866 141 0 0 25 0 1 0 549136289 217006080 51771 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52980 51771 603 41 0 52939 0
vsize: 211920
[startup+550.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 53299 0 0 0 54865 142 0 0 25 0 1 0 549136289 219619328 52398 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53618 52398 603 41 0 53577 0
vsize: 214472
[startup+560.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 54033 0 0 0 55864 144 0 0 25 0 1 0 549136289 222531584 53132 4294967295 134512640 134672761 3221224544 3221223728 134615796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54329 53132 603 41 0 54288 0
vsize: 217316
[startup+570.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 55246 0 0 0 56861 146 0 0 25 0 1 0 549136289 227553280 54345 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55555 54345 603 41 0 55514 0
vsize: 222220
[startup+580.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 56283 0 0 0 57860 148 0 0 25 0 1 0 549136289 231743488 55382 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56578 55382 603 41 0 56537 0
vsize: 226312
[startup+590.023 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 57099 0 0 0 58858 150 0 0 25 0 1 0 549136289 235163648 56198 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57413 56198 603 41 0 57372 0
vsize: 229652
[startup+600.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 57709 0 0 0 59857 152 0 0 25 0 1 0 549136289 237641728 56808 4294967295 134512640 134672761 3221224544 3221223680 134614710 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58018 56808 603 41 0 57977 0
vsize: 232072
[startup+610.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 58356 0 0 0 60855 154 0 0 25 0 1 0 549136289 240283648 57455 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58663 57455 603 41 0 58622 0
vsize: 234652
[startup+620.023 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 59292 0 0 0 61852 157 0 0 25 0 1 0 549136289 244097024 58391 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59594 58391 603 41 0 59553 0
vsize: 238376
[startup+630.023 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 60067 0 0 0 62850 159 0 0 25 0 1 0 549136289 247238656 59166 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60361 59166 603 41 0 60320 0
vsize: 241444
[startup+640.023 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 60897 0 0 0 63848 161 0 0 25 0 1 0 549136289 250662912 59996 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61197 59996 603 41 0 61156 0
vsize: 244788
[startup+650.024 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 61622 0 0 0 64847 162 0 0 25 0 1 0 549136289 253558784 60721 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61904 60721 603 41 0 61863 0
vsize: 247616
[startup+660.024 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 62434 0 0 0 65846 164 0 0 25 0 1 0 549136289 256970752 61533 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62737 61533 603 41 0 62696 0
vsize: 250948
[startup+670.025 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 63314 0 0 0 66843 166 0 0 25 0 1 0 549136289 260513792 62413 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63602 62413 603 41 0 63561 0
vsize: 254408
[startup+680.025 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 64033 0 0 0 67842 168 0 0 25 0 1 0 549136289 263413760 63132 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64310 63132 603 41 0 64269 0
vsize: 257240
[startup+690.025 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 65016 0 0 0 68839 171 0 0 25 0 1 0 549136289 267472896 64115 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65301 64115 603 41 0 65260 0
vsize: 261204
[startup+700.025 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 65966 0 0 0 69837 173 0 0 25 0 1 0 549136289 271405056 65065 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66261 65065 603 41 0 66220 0
vsize: 265044
[startup+710.025 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 66770 0 0 0 70836 174 0 0 25 0 1 0 549136289 274698240 65869 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67065 65869 603 41 0 67024 0
vsize: 268260
[startup+720.026 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 67582 0 0 0 71835 176 0 0 25 0 1 0 549136289 277958656 66681 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67861 66681 603 41 0 67820 0
vsize: 271444
[startup+730.025 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 68597 0 0 0 72833 178 0 0 25 0 1 0 549136289 282075136 67696 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68866 67696 603 41 0 68825 0
vsize: 275464
[startup+740.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 69829 0 0 0 73830 181 0 0 25 0 1 0 549136289 287227904 68928 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70124 68928 603 41 0 70083 0
vsize: 280496
[startup+750.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 70934 0 0 0 74828 184 0 0 25 0 1 0 549136289 291721216 70033 4294967295 134512640 134672761 3221224544 3221223680 134614664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71221 70033 603 41 0 71180 0
vsize: 284884
[startup+760.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 72063 0 0 0 75826 186 0 0 25 0 1 0 549136289 296263680 71162 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72330 71162 603 41 0 72289 0
vsize: 289320
[startup+770.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 73153 0 0 0 76823 188 0 0 25 0 1 0 549136289 300797952 72252 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73437 72252 603 41 0 73396 0
vsize: 293748
[startup+780.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 74275 0 0 0 77821 191 0 0 25 0 1 0 549136289 305430528 73374 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74568 73374 603 41 0 74527 0
vsize: 298272
[startup+790.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 75523 0 0 0 78819 194 0 0 25 0 1 0 549136289 310517760 74622 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75810 74622 603 41 0 75769 0
vsize: 303240
[startup+800.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76783 0 0 0 79816 196 0 0 25 0 1 0 549136289 315932672 75850 4294967295 134512640 134672761 3221224544 3221223524 1075351063 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77132 75850 603 41 0 77091 0
vsize: 308528
[startup+810.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 80816 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+820.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 81816 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+830.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 82817 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+840.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 83817 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223356 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+850.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 84817 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+860.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 85817 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+870.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 86817 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223584 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+880.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 87817 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+890.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 88818 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+900.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 89818 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+910.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 9142
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 90818 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+920.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 9143
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 91818 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+930.029 s]
Raw data (loadavg): 1.07 1.00 0.96 2/54 9195
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 92818 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+940.03 s]
Raw data (loadavg): 1.06 1.00 0.96 2/54 9195
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 93819 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+950.031 s]
Raw data (loadavg): 1.05 1.00 0.96 2/54 9195
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 94819 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+960.031 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 9195
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 95819 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+970.031 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 9195
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 96819 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+980.031 s]
Raw data (loadavg): 1.03 1.00 0.96 2/54 9195
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 97819 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223680 134614516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+990.032 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 9195
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 98820 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1000.03 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 99820 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1010.03 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 100820 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1020.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 101820 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1030.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 102820 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1040.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 103821 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1050.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 104821 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1060.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 105821 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223584 134612601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 106821 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 107821 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 108821 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 109822 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223680 134614800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 110822 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 111822 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 112822 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 113822 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 114822 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 115823 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223584 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 116823 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 117823 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 118823 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 9197
Raw data (stat): 9142 (minisat+) R 9141 27222 27221 0 -1 0 76845 0 0 0 119823 196 0 0 25 0 1 0 549136289 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 9197
Raw data (stat): 9142 (minisat+) Z 9141 27222 27221 0 -1 12 76845 0 0 0 119823 210 0 0 25 0 1 0 549136289 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.18
CPU time (s): 1200.35
CPU user time (s): 1198.24
CPU system time (s): 2.10868
CPU usage (%): 100.014
Max. virtual memory (Kb): 308528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####