PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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	1176.34
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 15700

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-21 05:31:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16900 boxname=wulflinc27 idbench=1300 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00855a9538cee8df79108d56ee6867b4  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-l152lav.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-l152lav.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-l152lav.opb
IDLAUNCH: 16900
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        812096 kB
Buffers:         25304 kB
Cached:         168912 kB
SwapCached:        604 kB
Active:          31724 kB
Inactive:       164628 kB
HighTotal:      131008 kB
HighFree:        15260 kB
LowTotal:       903652 kB
LowFree:        796836 kB
SwapTotal:     2097892 kB
SwapFree:      2096484 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5236 kB
Slab:            20736 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:51:10 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 16900 7 1200.28 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.97 0.93 2/54 12549
Raw data (stat): 12549 (runsolver) R 12548 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542574111 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 4361 0 0 0 989 9 0 0 25 0 1 0 542574111 19894272 3997 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4857 3997 603 41 0 4816 0
vsize: 19428
[startup+20.001 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 4566 0 0 0 1987 10 0 0 25 0 1 0 542574111 20840448 4202 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5088 4202 603 41 0 5047 0
vsize: 20352
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 4674 0 0 0 2987 10 0 0 25 0 1 0 542574111 21295104 4310 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5199 4310 603 41 0 5158 0
vsize: 20796
[startup+40.001 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 4827 0 0 0 3986 11 0 0 25 0 1 0 542574111 21835776 4463 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5331 4463 603 41 0 5290 0
vsize: 21324
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 4995 0 0 0 4986 11 0 0 25 0 1 0 542574111 22495232 4631 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.0016 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 5258 0 0 0 5985 13 0 0 25 0 1 0 542574111 23597056 4894 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5761 4894 603 41 0 5720 0
vsize: 23044
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 5586 0 0 0 6983 14 0 0 25 0 1 0 542574111 24944640 5222 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6090 5222 603 41 0 6049 0
vsize: 24360
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 6021 0 0 0 7982 16 0 0 25 0 1 0 542574111 26701824 5657 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6519 5657 603 41 0 6478 0
vsize: 26076
[startup+90.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 6599 0 0 0 8980 18 0 0 25 0 1 0 542574111 29122560 6235 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7110 6235 603 41 0 7069 0
vsize: 28440
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 7108 0 0 0 9979 20 0 0 25 0 1 0 542574111 31141888 6744 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7603 6744 603 41 0 7562 0
vsize: 30412
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 7438 0 0 0 10978 21 0 0 25 0 1 0 542574111 32612352 7074 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7962 7074 603 41 0 7921 0
vsize: 31848
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 7794 0 0 0 11976 22 0 0 25 0 1 0 542574111 34074624 7430 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 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.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 8166 0 0 0 12974 23 0 0 25 0 1 0 542574111 35676160 7802 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8710 7802 603 41 0 8669 0
vsize: 34840
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 8569 0 0 0 13973 24 0 0 25 0 1 0 542574111 37281792 8205 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9102 8205 603 41 0 9061 0
vsize: 36408
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 8933 0 0 0 14972 25 0 0 25 0 1 0 542574111 38764544 8569 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9464 8569 603 41 0 9423 0
vsize: 37856
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 9064 0 0 0 15972 26 0 0 25 0 1 0 542574111 39301120 8700 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9595 8700 603 41 0 9554 0
vsize: 38380
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 9305 0 0 0 16971 27 0 0 25 0 1 0 542574111 40226816 8941 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9821 8941 603 41 0 9780 0
vsize: 39284
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 9627 0 0 0 17970 28 0 0 25 0 1 0 542574111 41574400 9263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9263 603 41 0 10109 0
vsize: 40600
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 9862 0 0 0 18969 29 0 0 25 0 1 0 542574111 42512384 9498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10379 9498 603 41 0 10338 0
vsize: 41516
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 10351 0 0 0 19968 30 0 0 25 0 1 0 542574111 44539904 9987 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10874 9987 603 41 0 10833 0
vsize: 43496
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 10875 0 0 0 20967 32 0 0 25 0 1 0 542574111 46690304 10511 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11399 10511 603 41 0 11358 0
vsize: 45596
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 11387 0 0 0 21966 33 0 0 25 0 1 0 542574111 48705536 11023 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11891 11023 603 41 0 11850 0
vsize: 47564
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 11832 0 0 0 22965 34 0 0 25 0 1 0 542574111 50589696 11468 4294967295 134512640 134672761 3221224544 3221223728 134558925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12351 11468 603 41 0 12310 0
vsize: 49404
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 12266 0 0 0 23964 35 0 0 25 0 1 0 542574111 52600832 11902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12842 11902 603 41 0 12801 0
vsize: 51368
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 12515 0 0 0 24964 36 0 0 25 0 1 0 542574111 53534720 12151 4294967295 134512640 134672761 3221224544 3221223648 134559796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13070 12151 603 41 0 13029 0
vsize: 52280
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 12784 0 0 0 25963 37 0 0 25 0 1 0 542574111 54730752 12420 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13362 12420 603 41 0 13321 0
vsize: 53448
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 13087 0 0 0 26962 38 0 0 25 0 1 0 542574111 55922688 12723 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13653 12723 603 41 0 13612 0
vsize: 54612
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 13852 0 0 0 27960 40 0 0 25 0 1 0 542574111 59031552 13488 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14412 13488 603 41 0 14371 0
vsize: 57648
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 14605 0 0 0 28959 41 0 0 25 0 1 0 542574111 62136320 14241 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15170 14241 603 41 0 15129 0
vsize: 60680
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 15288 0 0 0 29957 43 0 0 25 0 1 0 542574111 64983040 14924 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15865 14924 603 41 0 15824 0
vsize: 63460
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 15822 0 0 0 30955 45 0 0 25 0 1 0 542574111 67149824 15458 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16394 15458 603 41 0 16353 0
vsize: 65576
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 16298 0 0 0 31954 47 0 0 25 0 1 0 542574111 69033984 15934 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16854 15934 603 41 0 16813 0
vsize: 67416
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 16814 0 0 0 32952 48 0 0 25 0 1 0 542574111 71204864 16450 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17384 16450 603 41 0 17343 0
vsize: 69536
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 17371 0 0 0 33950 51 0 0 25 0 1 0 542574111 73502720 17007 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17945 17009 603 41 0 17904 0
vsize: 71780
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 17921 0 0 0 34948 53 0 0 25 0 1 0 542574111 75661312 17557 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18472 17557 603 41 0 18431 0
vsize: 73888
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 18427 0 0 0 35947 54 0 0 25 0 1 0 542574111 77824000 18063 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19000 18063 603 41 0 18959 0
vsize: 76000
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 18956 0 0 0 36947 55 0 0 25 0 1 0 542574111 79982592 18592 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19527 18592 603 41 0 19486 0
vsize: 78108
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 19454 0 0 0 37945 56 0 0 25 0 1 0 542574111 82022400 19090 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20025 19090 603 41 0 19984 0
vsize: 80100
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 19956 0 0 0 38944 58 0 0 25 0 1 0 542574111 84054016 19592 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20521 19592 603 41 0 20480 0
vsize: 82084
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 20473 0 0 0 39943 59 0 0 25 0 1 0 542574111 86208512 20109 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21047 20109 603 41 0 21006 0
vsize: 84188
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 20993 0 0 0 40942 60 0 0 25 0 1 0 542574111 88227840 20629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21540 20629 603 41 0 21499 0
vsize: 86160
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 21577 0 0 0 41939 63 0 0 25 0 1 0 542574111 90648576 21213 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22131 21213 603 41 0 22090 0
vsize: 88524
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 22202 0 0 0 42937 65 0 0 25 0 1 0 542574111 93200384 21838 4294967295 134512640 134672761 3221224544 3221223648 134560125 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22754 21838 603 41 0 22713 0
vsize: 91016
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 22803 0 0 0 43935 67 0 0 25 0 1 0 542574111 95723520 22439 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23370 22439 603 41 0 23329 0
vsize: 93480
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 23403 0 0 0 44934 69 0 0 25 0 1 0 542574111 98136064 23039 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23959 23039 603 41 0 23918 0
vsize: 95836
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 23995 0 0 0 45933 70 0 0 25 0 1 0 542574111 100540416 23631 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24546 23631 603 41 0 24505 0
vsize: 98184
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 24528 0 0 0 46932 72 0 0 25 0 1 0 542574111 102707200 24164 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25075 24164 603 41 0 25034 0
vsize: 100300
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 25042 0 0 0 47930 73 0 0 25 0 1 0 542574111 104857600 24678 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25600 24678 603 41 0 25559 0
vsize: 102400
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 25538 0 0 0 48928 75 0 0 25 0 1 0 542574111 106872832 25174 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26092 25174 603 41 0 26051 0
vsize: 104368
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 26092 0 0 0 49927 77 0 0 25 0 1 0 542574111 109158400 25728 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26650 25728 603 41 0 26609 0
vsize: 106600
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 26605 0 0 0 50926 78 0 0 25 0 1 0 542574111 111321088 26241 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27178 26241 603 41 0 27137 0
vsize: 108712
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 27124 0 0 0 51926 79 0 0 25 0 1 0 542574111 113360896 26760 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27676 26760 603 41 0 27635 0
vsize: 110704
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 27628 0 0 0 52924 80 0 0 25 0 1 0 542574111 115515392 27264 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28202 27264 603 41 0 28161 0
vsize: 112808
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 28110 0 0 0 53923 82 0 0 25 0 1 0 542574111 117403648 27746 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28663 27746 603 41 0 28622 0
vsize: 114652
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 28585 0 0 0 54921 84 0 0 25 0 1 0 542574111 119451648 28221 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29163 28221 603 41 0 29122 0
vsize: 116652
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 29060 0 0 0 55920 85 0 0 25 0 1 0 542574111 121344000 28696 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29625 28696 603 41 0 29584 0
vsize: 118500
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 29516 0 0 0 56919 86 0 0 25 0 1 0 542574111 123240448 29152 4294967295 134512640 134672761 3221224544 3221223728 134559625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30088 29152 603 41 0 30047 0
vsize: 120352
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 30027 0 0 0 57918 88 0 0 25 0 1 0 542574111 125296640 29663 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30590 29663 603 41 0 30549 0
vsize: 122360
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 30509 0 0 0 58917 89 0 0 25 0 1 0 542574111 127328256 30145 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31086 30145 603 41 0 31045 0
vsize: 124344
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 31079 0 0 0 59915 91 0 0 25 0 1 0 542574111 129650688 30715 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31653 30715 603 41 0 31612 0
vsize: 126612
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 31645 0 0 0 60913 93 0 0 25 0 1 0 542574111 132075520 31281 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32245 31281 603 41 0 32204 0
vsize: 128980
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 32076 0 0 0 61912 94 0 0 25 0 1 0 542574111 133820416 31712 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32671 31712 603 41 0 32630 0
vsize: 130684
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 32492 0 0 0 62911 95 0 0 25 0 1 0 542574111 135561216 32128 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33096 32128 603 41 0 33055 0
vsize: 132384
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 32831 0 0 0 63910 96 0 0 25 0 1 0 542574111 136912896 32467 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33426 32467 603 41 0 33385 0
vsize: 133704
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 33250 0 0 0 64910 97 0 0 25 0 1 0 542574111 138653696 32886 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33851 32886 603 41 0 33810 0
vsize: 135404
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 33700 0 0 0 65909 98 0 0 25 0 1 0 542574111 140394496 33336 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34276 33336 603 41 0 34235 0
vsize: 137104
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 34092 0 0 0 66907 100 0 0 25 0 1 0 542574111 142000128 33728 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34668 33728 603 41 0 34627 0
vsize: 138672
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 34492 0 0 0 67906 101 0 0 25 0 1 0 542574111 143618048 34128 4294967295 134512640 134672761 3221224544 3221223648 134559943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35063 34128 603 41 0 35022 0
vsize: 140252
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 34930 0 0 0 68905 102 0 0 25 0 1 0 542574111 145494016 34566 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35521 34566 603 41 0 35480 0
vsize: 142084
[startup+700.02 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 35383 0 0 0 69903 104 0 0 25 0 1 0 542574111 147243008 35019 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35948 35019 603 41 0 35907 0
vsize: 143792
[startup+710.02 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 35727 0 0 0 70902 106 0 0 25 0 1 0 542574111 148717568 35363 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36308 35363 603 41 0 36267 0
vsize: 145232
[startup+720.021 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 36046 0 0 0 71901 107 0 0 25 0 1 0 542574111 149934080 35682 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36605 35682 603 41 0 36564 0
vsize: 146420
[startup+730.021 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 36312 0 0 0 72901 107 0 0 25 0 1 0 542574111 151015424 35948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36869 35948 603 41 0 36828 0
vsize: 147476
[startup+740.021 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 36572 0 0 0 73899 109 0 0 25 0 1 0 542574111 152596480 36208 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37255 36208 603 41 0 37214 0
vsize: 149020
[startup+750.022 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 36844 0 0 0 74898 110 0 0 25 0 1 0 542574111 153812992 36480 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37552 36480 603 41 0 37511 0
vsize: 150208
[startup+760.022 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 37288 0 0 0 75897 111 0 0 25 0 1 0 542574111 155545600 36924 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37975 36924 603 41 0 37934 0
vsize: 151900
[startup+770.023 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 37759 0 0 0 76896 112 0 0 25 0 1 0 542574111 157560832 37395 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38467 37395 603 41 0 38426 0
vsize: 153868
[startup+780.023 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 38542 0 0 0 77895 113 0 0 25 0 1 0 542574111 160661504 38178 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39224 38178 603 41 0 39183 0
vsize: 156896
[startup+790.023 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 39197 0 0 0 78894 115 0 0 25 0 1 0 542574111 163360768 38833 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39883 38833 603 41 0 39842 0
vsize: 159532
[startup+800.023 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 39857 0 0 0 79892 116 0 0 25 0 1 0 542574111 166064128 39493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40543 39493 603 41 0 40502 0
vsize: 162172
[startup+810.024 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 40460 0 0 0 80890 118 0 0 25 0 1 0 542574111 168493056 40096 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41136 40096 603 41 0 41095 0
vsize: 164544
[startup+820.024 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 41124 0 0 0 81889 120 0 0 25 0 1 0 542574111 171208704 40760 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41799 40760 603 41 0 41758 0
vsize: 167196
[startup+830.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 41766 0 0 0 82887 121 0 0 25 0 1 0 542574111 173924352 41402 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42462 41402 603 41 0 42421 0
vsize: 169848
[startup+840.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 42374 0 0 0 83886 123 0 0 25 0 1 0 542574111 176361472 42010 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43057 42010 603 41 0 43016 0
vsize: 172228
[startup+850.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 42958 0 0 0 84885 125 0 0 25 0 1 0 542574111 178823168 42594 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43658 42594 603 41 0 43617 0
vsize: 174632
[startup+860.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 43562 0 0 0 85883 126 0 0 25 0 1 0 542574111 181264384 43198 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44254 43198 603 41 0 44213 0
vsize: 177016
[startup+870.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 43992 0 0 0 86882 128 0 0 25 0 1 0 542574111 183009280 43628 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44680 43628 603 41 0 44639 0
vsize: 178720
[startup+880.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 44483 0 0 0 87881 129 0 0 25 0 1 0 542574111 185028608 44119 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45173 44119 603 41 0 45132 0
vsize: 180692
[startup+890.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 44953 0 0 0 88880 130 0 0 25 0 1 0 542574111 186916864 44589 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45634 44589 603 41 0 45593 0
vsize: 182536
[startup+900.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 45391 0 0 0 89878 132 0 0 25 0 1 0 542574111 188669952 45027 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46062 45027 603 41 0 46021 0
vsize: 184248
[startup+910.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 45853 0 0 0 90878 133 0 0 25 0 1 0 542574111 190545920 45489 4294967295 134512640 134672761 3221224544 3221223704 134559749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46520 45489 603 41 0 46479 0
vsize: 186080
[startup+920.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 46376 0 0 0 91876 134 0 0 25 0 1 0 542574111 192692224 46012 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47044 46012 603 41 0 47003 0
vsize: 188176
[startup+930.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 46940 0 0 0 92876 135 0 0 25 0 1 0 542574111 194965504 46576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47599 46576 603 41 0 47558 0
vsize: 190396
[startup+940.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 47404 0 0 0 93874 137 0 0 25 0 1 0 542574111 196972544 47040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48089 47040 603 41 0 48048 0
vsize: 192356
[startup+950.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 47809 0 0 0 94873 138 0 0 25 0 1 0 542574111 198590464 47445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48484 47445 603 41 0 48443 0
vsize: 193936
[startup+960.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 48219 0 0 0 95871 140 0 0 25 0 1 0 542574111 200187904 47855 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48874 47855 603 41 0 48833 0
vsize: 195496
[startup+970.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 48733 0 0 0 96870 142 0 0 25 0 1 0 542574111 202334208 48369 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49398 48369 603 41 0 49357 0
vsize: 197592
[startup+980.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 49186 0 0 0 97869 143 0 0 25 0 1 0 542574111 204222464 48822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49859 48822 603 41 0 49818 0
vsize: 199436
[startup+990.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 49451 0 0 0 98868 144 0 0 25 0 1 0 542574111 205303808 49087 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50123 49087 603 41 0 50082 0
vsize: 200492
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 49461 0 0 0 99868 144 0 0 25 0 1 0 542574111 205303808 49097 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50123 49097 603 41 0 50082 0
vsize: 200492
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 49821 0 0 0 100867 145 0 0 25 0 1 0 542574111 206786560 49457 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50485 49457 603 41 0 50444 0
vsize: 201940
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 50013 0 0 0 101867 145 0 0 25 0 1 0 542574111 207597568 49649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50683 49649 603 41 0 50642 0
vsize: 202732
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 50563 0 0 0 102866 147 0 0 25 0 1 0 542574111 209743872 50199 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51207 50199 603 41 0 51166 0
vsize: 204828
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 50861 0 0 0 103865 148 0 0 25 0 1 0 542574111 211075072 50497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51532 50497 603 41 0 51491 0
vsize: 206128
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 51308 0 0 0 104864 150 0 0 25 0 1 0 542574111 212832256 50944 4294967295 134512640 134672761 3221224544 3221223648 134559995 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51961 50944 603 41 0 51920 0
vsize: 207844
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 51800 0 0 0 105863 151 0 0 25 0 1 0 542574111 214835200 51436 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52450 51436 603 41 0 52409 0
vsize: 209800
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 51931 0 0 0 106862 151 0 0 25 0 1 0 542574111 215367680 51567 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52580 51567 603 41 0 52539 0
vsize: 210320
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 52315 0 0 0 107862 152 0 0 25 0 1 0 542574111 216989696 51951 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52976 51951 603 41 0 52935 0
vsize: 211904
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 52724 0 0 0 108861 153 0 0 25 0 1 0 542574111 218603520 52360 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53370 52360 603 41 0 53329 0
vsize: 213480
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 53179 0 0 0 109859 155 0 0 25 0 1 0 542574111 220450816 52815 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53821 52815 603 41 0 53780 0
vsize: 215284
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 53304 0 0 0 110859 155 0 0 25 0 1 0 542574111 220991488 52940 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53953 52940 603 41 0 53912 0
vsize: 215812
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 53333 0 0 0 111860 155 0 0 25 0 1 0 542574111 221126656 52969 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53986 52969 603 41 0 53945 0
vsize: 215944
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 53479 0 0 0 112859 156 0 0 25 0 1 0 542574111 221663232 53115 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54117 53115 603 41 0 54076 0
vsize: 216468
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 53927 0 0 0 113858 157 0 0 25 0 1 0 542574111 223522816 53563 4294967295 134512640 134672761 3221224544 3221223648 134559784 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54571 53563 603 41 0 54530 0
vsize: 218284
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 54375 0 0 0 114856 159 0 0 25 0 1 0 542574111 225427456 54011 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55036 54011 603 41 0 54995 0
vsize: 220144
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 54711 0 0 0 115854 161 0 0 25 0 1 0 542574111 226750464 54347 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55359 54347 603 41 0 55318 0
vsize: 221436
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 55036 0 0 0 116854 162 0 0 25 0 1 0 542574111 228065280 54672 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55680 54672 603 41 0 55639 0
vsize: 222720
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 55383 0 0 0 117853 163 0 0 25 0 1 0 542574111 229539840 55019 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56040 55019 603 41 0 55999 0
vsize: 224160
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 55740 0 0 0 118853 164 0 0 25 0 1 0 542574111 230961152 55376 4294967295 134512640 134672761 3221224544 3221223728 134558923 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56387 55376 603 41 0 56346 0
vsize: 225548
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 12549
Raw data (stat): 12549 (minisat+) R 12548 18865 18864 0 -1 0 56069 0 0 0 119852 164 0 0 25 0 1 0 542574111 232275968 55705 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56708 55705 603 41 0 56667 0
vsize: 226832
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 12549
Raw data (stat): 12549 (minisat+) Z 12548 18865 18864 0 -1 12 56071 0 0 0 119852 175 0 0 25 0 1 0 542574111 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.14
CPU time (s): 1200.28
CPU user time (s): 1198.53
CPU system time (s): 1.75173
CPU usage (%): 100.011
Max. virtual memory (Kb): 226832
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####