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/miplib/normalized-mps-v2-20-10-l152lav.opb
MD5SUM	00855a9538cee8df79108d56ee6867b4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5046
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.28
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 22277

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        622372 kB
Buffers:         28148 kB
Cached:         362760 kB
SwapCached:        432 kB
Active:          59348 kB
Inactive:       333744 kB
HighTotal:      131008 kB
HighFree:        44800 kB
LowTotal:       903652 kB
LowFree:        577572 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5364 kB
Slab:            13640 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:54:33 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 11908 7 1200.3 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  123819   394251 |   41273       0        0     nan |  0.000 % |
c |       100 |  123689   393805 |   45400      82     1033    12.6 |  0.582 % |
c |       250 |  123611   393519 |   49940     223    12255    55.0 |  0.635 % |
c |       476 |  123592   393454 |   54934     446    25868    58.0 |  0.651 % |
c |       813 |  123592   393454 |   60427     783    31769    40.6 |  0.651 % |
c |      1319 |  122327   388987 |   66470    1056    36336    34.4 |  1.522 % |
c |      2078 |  122067   388081 |   73117    1773    50521    28.5 |  1.722 % |
c |      3217 |  122033   387971 |   80429    2908   115105    39.6 |  1.750 % |
c |      4925 |  121872   387428 |   88472    4589   198107    43.2 |  1.864 % |
c |      7487 |  121369   385669 |   97319    7065   281333    39.8 |  2.222 % |
c |     11331 |  121046   384558 |  107051   10860   383375    35.3 |  2.446 % |
c |     17097 |  120433   382447 |  117756   16530   595557    36.0 |  2.816 % |
c |     25746 |  120172   381574 |  129532   25104  1198644    47.7 |  2.979 % |
c |     38722 |  120096   381316 |  142485   38063  3051886    80.2 |  3.020 % |
c |     58183 |  119808   380306 |  156734   57411  5055291    88.1 |  3.158 % |
c |     87381 |  119754   380120 |  172407   86599 15798491   182.4 |  3.183 % |
c |    131170 |  119668   379828 |  189648  130372 30883892   236.9 |  3.228 % |
#### 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.91 2/54 23099
Raw data (stat): 23099 (runsolver) R 23098 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491933320 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 4361 0 0 0 986 12 0 0 25 0 1 0 491933320 19894272 3997 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4857 3997 603 41 0 4816 0
vsize: 19428
[startup+20.0014 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 4566 0 0 0 1986 12 0 0 25 0 1 0 491933320 20840448 4202 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5088 4202 603 41 0 5047 0
vsize: 20352
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 4675 0 0 0 2985 13 0 0 25 0 1 0 491933320 21295104 4311 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5199 4311 603 41 0 5158 0
vsize: 20796
[startup+40.0018 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 4828 0 0 0 3984 14 0 0 25 0 1 0 491933320 21835776 4464 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5331 4464 603 41 0 5290 0
vsize: 21324
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 4995 0 0 0 4983 15 0 0 25 0 1 0 491933320 22495232 4631 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5492 4631 603 41 0 5451 0
vsize: 21968
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 5260 0 0 0 5982 16 0 0 25 0 1 0 491933320 23732224 4896 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5794 4896 603 41 0 5753 0
vsize: 23176
[startup+70.0032 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 5589 0 0 0 6981 18 0 0 25 0 1 0 491933320 24944640 5225 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6090 5225 603 41 0 6049 0
vsize: 24360
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 6028 0 0 0 7980 20 0 0 25 0 1 0 491933320 26836992 5664 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6552 5664 603 41 0 6511 0
vsize: 26208
[startup+90.0044 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 6606 0 0 0 8977 22 0 0 25 0 1 0 491933320 29122560 6242 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7110 6242 603 41 0 7069 0
vsize: 28440
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 7111 0 0 0 9976 24 0 0 25 0 1 0 491933320 31141888 6747 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7603 6747 603 41 0 7562 0
vsize: 30412
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 7440 0 0 0 10975 25 0 0 25 0 1 0 491933320 32743424 7076 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7994 7076 603 41 0 7953 0
vsize: 31976
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 7794 0 0 0 11973 27 0 0 25 0 1 0 491933320 34074624 7430 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7430 603 41 0 8278 0
vsize: 33276
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 8158 0 0 0 12972 28 0 0 25 0 1 0 491933320 35545088 7794 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8678 7794 603 41 0 8637 0
vsize: 34712
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 8562 0 0 0 13970 30 0 0 25 0 1 0 491933320 37281792 8198 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9102 8198 603 41 0 9061 0
vsize: 36408
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 8931 0 0 0 14968 32 0 0 25 0 1 0 491933320 38764544 8567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9464 8567 603 41 0 9423 0
vsize: 37856
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 9060 0 0 0 15968 32 0 0 25 0 1 0 491933320 39301120 8696 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9595 8696 603 41 0 9554 0
vsize: 38380
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 9298 0 0 0 16967 33 0 0 25 0 1 0 491933320 40226816 8934 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9821 8934 603 41 0 9780 0
vsize: 39284
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 9620 0 0 0 17966 35 0 0 25 0 1 0 491933320 41574400 9256 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9256 603 41 0 10109 0
vsize: 40600
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 9851 0 0 0 18965 36 0 0 25 0 1 0 491933320 42512384 9487 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10379 9487 603 41 0 10338 0
vsize: 41516
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 10334 0 0 0 19963 37 0 0 25 0 1 0 491933320 44404736 9970 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10841 9970 603 41 0 10800 0
vsize: 43364
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 10857 0 0 0 20961 40 0 0 25 0 1 0 491933320 46555136 10493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11366 10493 603 41 0 11325 0
vsize: 45464
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 11365 0 0 0 21959 42 0 0 25 0 1 0 491933320 48705536 11001 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11891 11001 603 41 0 11850 0
vsize: 47564
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 11797 0 0 0 22958 44 0 0 25 0 1 0 491933320 50454528 11433 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12318 11433 603 41 0 12277 0
vsize: 49272
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 12261 0 0 0 23957 45 0 0 25 0 1 0 491933320 52600832 11897 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12842 11897 603 41 0 12801 0
vsize: 51368
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 12498 0 0 0 24956 46 0 0 25 0 1 0 491933320 53534720 12134 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13070 12134 603 41 0 13029 0
vsize: 52280
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 12772 0 0 0 25955 47 0 0 25 0 1 0 491933320 54595584 12408 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13329 12408 603 41 0 13288 0
vsize: 53316
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 13049 0 0 0 26954 48 0 0 25 0 1 0 491933320 55787520 12685 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13620 12685 603 41 0 13579 0
vsize: 54480
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 13813 0 0 0 27951 51 0 0 25 0 1 0 491933320 58896384 13449 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14379 13449 603 41 0 14338 0
vsize: 57516
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 14562 0 0 0 28949 53 0 0 25 0 1 0 491933320 62001152 14198 4294967295 134512640 134672761 3221224544 3221223728 134559532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15137 14198 603 41 0 15096 0
vsize: 60548
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 15254 0 0 0 29947 55 0 0 25 0 1 0 491933320 64716800 14890 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15800 14890 603 41 0 15759 0
vsize: 63200
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 15803 0 0 0 30946 56 0 0 25 0 1 0 491933320 67014656 15439 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16361 15439 603 41 0 16320 0
vsize: 65444
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 16275 0 0 0 31945 58 0 0 25 0 1 0 491933320 68907008 15911 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16823 15911 603 41 0 16782 0
vsize: 67292
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 16787 0 0 0 32943 60 0 0 25 0 1 0 491933320 71065600 16423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17350 16423 603 41 0 17309 0
vsize: 69400
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 17344 0 0 0 33942 61 0 0 25 0 1 0 491933320 73367552 16980 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17912 16980 603 41 0 17871 0
vsize: 71648
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 17893 0 0 0 34941 62 0 0 25 0 1 0 491933320 75661312 17529 4294967295 134512640 134672761 3221224544 3221223728 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18472 17529 603 41 0 18431 0
vsize: 73888
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 18398 0 0 0 35939 64 0 0 25 0 1 0 491933320 77692928 18034 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18968 18034 603 41 0 18927 0
vsize: 75872
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 18930 0 0 0 36938 66 0 0 25 0 1 0 491933320 79847424 18566 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19494 18566 603 41 0 19453 0
vsize: 77976
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 19431 0 0 0 37937 67 0 0 25 0 1 0 491933320 81887232 19067 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19992 19067 603 41 0 19951 0
vsize: 79968
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 19936 0 0 0 38936 68 0 0 25 0 1 0 491933320 83918848 19572 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20488 19572 603 41 0 20447 0
vsize: 81952
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 20465 0 0 0 39935 69 0 0 25 0 1 0 491933320 86073344 20101 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21014 20101 603 41 0 20973 0
vsize: 84056
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 20989 0 0 0 40933 70 0 0 25 0 1 0 491933320 88227840 20625 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21540 20625 603 41 0 21499 0
vsize: 86160
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 21578 0 0 0 41932 72 0 0 25 0 1 0 491933320 90648576 21214 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22131 21214 603 41 0 22090 0
vsize: 88524
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 22212 0 0 0 42930 74 0 0 25 0 1 0 491933320 93327360 21848 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22785 21848 603 41 0 22744 0
vsize: 91140
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 22814 0 0 0 43929 76 0 0 25 0 1 0 491933320 95723520 22450 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23370 22450 603 41 0 23329 0
vsize: 93480
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 23423 0 0 0 44927 77 0 0 25 0 1 0 491933320 98271232 23059 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23992 23059 603 41 0 23951 0
vsize: 95968
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 24018 0 0 0 45926 79 0 0 25 0 1 0 491933320 100675584 23654 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24579 23654 603 41 0 24538 0
vsize: 98316
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 24559 0 0 0 46924 81 0 0 25 0 1 0 491933320 102842368 24195 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25108 24195 603 41 0 25067 0
vsize: 100432
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 25079 0 0 0 47923 82 0 0 25 0 1 0 491933320 104992768 24715 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25633 24715 603 41 0 25592 0
vsize: 102532
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 25579 0 0 0 48921 84 0 0 25 0 1 0 491933320 107008000 25215 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26125 25215 603 41 0 26084 0
vsize: 104500
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 26141 0 0 0 49920 85 0 0 25 0 1 0 491933320 109297664 25777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26684 25777 603 41 0 26643 0
vsize: 106736
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 26666 0 0 0 50920 86 0 0 25 0 1 0 491933320 111460352 26302 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27212 26302 603 41 0 27171 0
vsize: 108848
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 27186 0 0 0 51919 88 0 0 25 0 1 0 491933320 113627136 26822 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27741 26822 603 41 0 27700 0
vsize: 110964
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 27688 0 0 0 52917 89 0 0 25 0 1 0 491933320 115650560 27324 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28235 27324 603 41 0 28194 0
vsize: 112940
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 28167 0 0 0 53917 90 0 0 25 0 1 0 491933320 117669888 27803 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28728 27803 603 41 0 28687 0
vsize: 114912
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 28649 0 0 0 54916 91 0 0 25 0 1 0 491933320 119721984 28285 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29229 28285 603 41 0 29188 0
vsize: 116916
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 29126 0 0 0 55915 92 0 0 25 0 1 0 491933320 121610240 28762 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29690 28762 603 41 0 29649 0
vsize: 118760
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 29599 0 0 0 56914 93 0 0 25 0 1 0 491933320 123641856 29235 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30186 29235 603 41 0 30145 0
vsize: 120744
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 30104 0 0 0 57913 94 0 0 25 0 1 0 491933320 125702144 29740 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30689 29740 603 41 0 30648 0
vsize: 122756
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 30613 0 0 0 58912 95 0 0 25 0 1 0 491933320 127754240 30249 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31190 30249 603 41 0 31149 0
vsize: 124760
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 31202 0 0 0 59911 97 0 0 25 0 1 0 491933320 130191360 30838 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31785 30838 603 41 0 31744 0
vsize: 127140
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 31769 0 0 0 60910 98 0 0 25 0 1 0 491933320 132476928 31405 4294967295 134512640 134672761 3221224544 3221223648 134560136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32343 31405 603 41 0 32302 0
vsize: 129372
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 32189 0 0 0 61909 99 0 0 25 0 1 0 491933320 134225920 31825 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32770 31825 603 41 0 32729 0
vsize: 131080
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 32602 0 0 0 62907 101 0 0 25 0 1 0 491933320 135966720 32238 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33195 32238 603 41 0 33154 0
vsize: 132780
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 32932 0 0 0 63906 102 0 0 25 0 1 0 491933320 137314304 32568 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33524 32568 603 41 0 33483 0
vsize: 134096
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 33391 0 0 0 64906 103 0 0 25 0 1 0 491933320 139190272 33027 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33982 33027 603 41 0 33941 0
vsize: 135928
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 33796 0 0 0 65904 104 0 0 25 0 1 0 491933320 140795904 33432 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34374 33432 603 41 0 34333 0
vsize: 137496
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 34193 0 0 0 66904 105 0 0 25 0 1 0 491933320 142405632 33829 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34767 33829 603 41 0 34726 0
vsize: 139068
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 34626 0 0 0 67903 106 0 0 25 0 1 0 491933320 144154624 34262 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35194 34262 603 41 0 35153 0
vsize: 140776
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 35065 0 0 0 68902 107 0 0 25 0 1 0 491933320 146034688 34701 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35653 34701 603 41 0 35612 0
vsize: 142612
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 35515 0 0 0 69901 109 0 0 25 0 1 0 491933320 147783680 35151 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36080 35151 603 41 0 36039 0
vsize: 144320
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 35833 0 0 0 70900 109 0 0 25 0 1 0 491933320 149123072 35469 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36407 35469 603 41 0 36366 0
vsize: 145628
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 36124 0 0 0 71900 110 0 0 25 0 1 0 491933320 150339584 35760 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36704 35760 603 41 0 36663 0
vsize: 146816
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 36419 0 0 0 72899 111 0 0 25 0 1 0 491933320 151539712 36055 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36997 36055 603 41 0 36956 0
vsize: 147988
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 36634 0 0 0 73898 112 0 0 25 0 1 0 491933320 152866816 36270 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37321 36270 603 41 0 37280 0
vsize: 149284
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 36981 0 0 0 74897 113 0 0 25 0 1 0 491933320 154349568 36617 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37683 36617 603 41 0 37642 0
vsize: 150732
[startup+760.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 37485 0 0 0 75897 114 0 0 25 0 1 0 491933320 156352512 37121 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38172 37121 603 41 0 38131 0
vsize: 152688
[startup+770.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 38044 0 0 0 76896 115 0 0 25 0 1 0 491933320 158642176 37680 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38731 37680 603 41 0 38690 0
vsize: 154924
[startup+780.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 38768 0 0 0 77894 116 0 0 25 0 1 0 491933320 161603584 38404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39454 38404 603 41 0 39413 0
vsize: 157816
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 39446 0 0 0 78893 118 0 0 25 0 1 0 491933320 164433920 39082 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40145 39082 603 41 0 40104 0
vsize: 160580
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 40110 0 0 0 79892 119 0 0 25 0 1 0 491933320 167145472 39746 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40807 39746 603 41 0 40766 0
vsize: 163228
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 40744 0 0 0 80890 121 0 0 25 0 1 0 491933320 169709568 40380 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41433 40380 603 41 0 41392 0
vsize: 165732
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 41404 0 0 0 81889 122 0 0 25 0 1 0 491933320 172429312 41040 4294967295 134512640 134672761 3221224544 3221223648 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42097 41040 603 41 0 42056 0
vsize: 168388
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 42043 0 0 0 82888 124 0 0 25 0 1 0 491933320 175005696 41679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42726 41679 603 41 0 42685 0
vsize: 170904
[startup+840.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 42640 0 0 0 83887 125 0 0 25 0 1 0 491933320 177446912 42276 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43322 42276 603 41 0 43281 0
vsize: 173288
[startup+850.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 43266 0 0 0 84886 126 0 0 25 0 1 0 491933320 180043776 42902 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43956 42902 603 41 0 43915 0
vsize: 175824
[startup+860.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 43783 0 0 0 85885 127 0 0 25 0 1 0 491933320 182075392 43419 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44452 43419 603 41 0 44411 0
vsize: 177808
[startup+870.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 44205 0 0 0 86884 129 0 0 25 0 1 0 491933320 183812096 43841 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44876 43841 603 41 0 44835 0
vsize: 179504
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 44759 0 0 0 87883 130 0 0 25 0 1 0 491933320 186105856 44395 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45436 44395 603 41 0 45395 0
vsize: 181744
[startup+890.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 45172 0 0 0 88882 131 0 0 25 0 1 0 491933320 187858944 44808 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45864 44808 603 41 0 45823 0
vsize: 183456
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 45658 0 0 0 89880 133 0 0 25 0 1 0 491933320 189734912 45294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46322 45294 603 41 0 46281 0
vsize: 185288
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 46103 0 0 0 90880 133 0 0 25 0 1 0 491933320 191619072 45739 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46782 45739 603 41 0 46741 0
vsize: 187128
[startup+920.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 46692 0 0 0 91880 134 0 0 25 0 1 0 491933320 194027520 46328 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47370 46328 603 41 0 47329 0
vsize: 189480
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 47201 0 0 0 92878 135 0 0 25 0 1 0 491933320 196034560 46837 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47860 46837 603 41 0 47819 0
vsize: 191440
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 47639 0 0 0 93878 136 0 0 25 0 1 0 491933320 197914624 47275 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48319 47275 603 41 0 48278 0
vsize: 193276
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 48037 0 0 0 94878 136 0 0 25 0 1 0 491933320 199524352 47673 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48712 47673 603 41 0 48671 0
vsize: 194848
[startup+960.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 48486 0 0 0 95877 137 0 0 25 0 1 0 491933320 201392128 48122 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49168 48122 603 41 0 49127 0
vsize: 196672
[startup+970.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 48989 0 0 0 96876 138 0 0 25 0 1 0 491933320 203399168 48625 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49658 48625 603 41 0 49617 0
vsize: 198632
[startup+980.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 49333 0 0 0 97875 139 0 0 25 0 1 0 491933320 204763136 48969 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49991 48969 603 41 0 49950 0
vsize: 199964
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 49461 0 0 0 98875 140 0 0 25 0 1 0 491933320 205303808 49097 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50123 49097 603 41 0 50082 0
vsize: 200492
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 49702 0 0 0 99875 140 0 0 25 0 1 0 491933320 206237696 49338 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50351 49338 603 41 0 50310 0
vsize: 201404
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 49860 0 0 0 100875 140 0 0 25 0 1 0 491933320 206921728 49496 4294967295 134512640 134672761 3221224544 3221223648 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50518 49496 603 41 0 50477 0
vsize: 202072
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 50450 0 0 0 101873 142 0 0 25 0 1 0 491933320 209350656 50086 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51111 50086 603 41 0 51070 0
vsize: 204444
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 50727 0 0 0 102873 142 0 0 25 0 1 0 491933320 210411520 50363 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51370 50363 603 41 0 51329 0
vsize: 205480
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 51117 0 0 0 103873 143 0 0 25 0 1 0 491933320 212013056 50753 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51761 50753 603 41 0 51720 0
vsize: 207044
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 51707 0 0 0 104872 144 0 0 25 0 1 0 491933320 214429696 51343 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52351 51343 603 41 0 52310 0
vsize: 209404
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 51908 0 0 0 105872 145 0 0 25 0 1 0 491933320 215236608 51544 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52548 51544 603 41 0 52507 0
vsize: 210192
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 52209 0 0 0 106871 145 0 0 25 0 1 0 491933320 216584192 51845 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52877 51845 603 41 0 52836 0
vsize: 211508
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 52589 0 0 0 107870 147 0 0 25 0 1 0 491933320 218066944 52225 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53239 52225 603 41 0 53198 0
vsize: 212956
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 53084 0 0 0 108869 148 0 0 25 0 1 0 491933320 220045312 52720 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53722 52720 603 41 0 53681 0
vsize: 214888
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 53276 0 0 0 109868 148 0 0 25 0 1 0 491933320 220856320 52912 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53920 52912 603 41 0 53879 0
vsize: 215680
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 53329 0 0 0 110869 148 0 0 25 0 1 0 491933320 221126656 52965 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53986 52965 603 41 0 53945 0
vsize: 215944
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 53386 0 0 0 111869 148 0 0 25 0 1 0 491933320 221261824 53022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54019 53022 603 41 0 53978 0
vsize: 216076
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 53827 0 0 0 112868 149 0 0 25 0 1 0 491933320 223129600 53463 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54475 53463 603 41 0 54434 0
vsize: 217900
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 54270 0 0 0 113868 150 0 0 25 0 1 0 491933320 224989184 53906 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54929 53906 603 41 0 54888 0
vsize: 219716
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 54655 0 0 0 114867 151 0 0 25 0 1 0 491933320 226480128 54291 4294967295 134512640 134672761 3221224544 3221223648 134560322 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55293 54291 603 41 0 55252 0
vsize: 221172
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 54969 0 0 0 115866 151 0 0 25 0 1 0 491933320 227807232 54605 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55617 54605 603 41 0 55576 0
vsize: 222468
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 55305 0 0 0 116866 152 0 0 25 0 1 0 491933320 229134336 54941 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55941 54941 603 41 0 55900 0
vsize: 223764
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 55671 0 0 0 117865 153 0 0 25 0 1 0 491933320 230707200 55307 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56325 55307 603 41 0 56284 0
vsize: 225300
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 56014 0 0 0 118865 154 0 0 25 0 1 0 491933320 232140800 55650 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56675 55650 603 41 0 56634 0
vsize: 226700
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23099
Raw data (stat): 23099 (minisat+) R 23098 29151 29150 0 -1 0 56344 0 0 0 119864 154 0 0 25 0 1 0 491933320 233439232 55980 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56992 55980 603 41 0 56951 0
vsize: 227968
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 23099
Raw data (stat): 23099 (minisat+) Z 23098 29151 29150 0 -1 12 56346 0 0 0 119864 164 0 0 25 0 1 0 491933320 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.14
CPU time (s): 1200.3
CPU user time (s): 1198.65
CPU system time (s): 1.64875
CPU usage (%): 100.013
Max. virtual memory (Kb): 227968
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####