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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare1_1.opb
MD5SUM	f88781e3d6e9a5487d13eaa213c27b55
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4272
Optimality of the best value was proved	NO
Number of terms in the objective function	120
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	6291450
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	6291450
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	205
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	45
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	105
Trace number 14181

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-20 23:09:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19487 boxname=wulflinc15 idbench=1499 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f88781e3d6e9a5487d13eaa213c27b55  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-markshare1_1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-markshare1_1.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-markshare1_1.opb
IDLAUNCH: 19487
/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:        752476 kB
Buffers:         33584 kB
Cached:         224660 kB
SwapCached:       2060 kB
Active:          95480 kB
Inactive:       167584 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        752224 kB
SwapTotal:     2097136 kB
SwapFree:      2094988 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            13456 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:29:33 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 19487 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[  10]---> Adder-cost: 554   maxlim: 438520   bits: 20/19
c ---[   8]---> Adder-cost: 562   maxlim: 469716   bits: 20/19
c ---[   6]---> Adder-cost: 644   maxlim: 485238   bits: 20/19
c ---[   4]---> Adder-cost: 446   maxlim: 425237   bits: 20/19
c ---[   2]---> Adder-cost: 494   maxlim: 433357   bits: 20/19
c ---[   0]---> Adder-cost: 474   maxlim: 432725   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   21505    76409 |    7168       0        0     nan |  0.000 % |
c |       100 |   21505    76409 |    7884     100      408     4.1 |  7.165 % |
c ==============================================================================
c [1mFound solution: 717416[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       249 |   25530    85902 |    8510     249     3771    15.1 |  7.165 % |
c ==============================================================================
c [1mFound solution: 406206[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       260 |   25650    86212 |    8550     260     4094    15.7 |  7.165 % |
c |       360 |   25650    86212 |    9405     360     8790    24.4 |  5.248 % |
c |       513 |   25650    86212 |   10345     513    12894    25.1 |  5.248 % |
c |       738 |   25650    86212 |   11380     738    22723    30.8 |  5.248 % |
c |      1076 |   25642    86186 |   12518    1075    33764    31.4 |  5.269 % |
c |      1583 |   25634    86160 |   13769    1581    48143    30.5 |  5.289 % |
c |      2342 |   25626    86134 |   15146    2339    60987    26.1 |  5.310 % |
c |      3481 |   25618    86108 |   16661    3477    97775    28.1 |  5.331 % |
c |      5189 |   25586    86004 |   18327    5181   141874    27.4 |  5.414 % |
c ==============================================================================
c [1mFound solution: 280117[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5281 |   25623    86098 |    8541    5273   143131    27.1 |  5.414 % |
c |      5382 |   25623    86098 |    9395    5374   157291    29.3 |  5.423 % |
c |      5534 |   25623    86098 |   10334    5526   162671    29.4 |  5.423 % |
c |      5759 |   25623    86098 |   11368    5751   166551    29.0 |  5.423 % |
c |      6096 |   25623    86098 |   12504    6088   175066    28.8 |  5.423 % |
c |      6604 |   25615    86072 |   13755    6595   197646    30.0 |  5.444 % |
c |      7363 |   25615    86072 |   15130    7354   219613    29.9 |  5.444 % |
c |      8504 |   25615    86072 |   16643    8495   274670    32.3 |  5.444 % |
c |     10212 |   25607    86046 |   18308   10202   344573    33.8 |  5.465 % |
c |     12774 |   25607    86046 |   20139   12764   535779    42.0 |  5.465 % |
c |     16619 |   25554    85919 |   22153   16601   787015    47.4 |  5.734 % |
c |     22385 |   25554    85919 |   24368   22367  1078852    48.2 |  5.734 % |
c |     31034 |   25554    85919 |   26805   18499   839128    45.4 |  5.734 % |
c ==============================================================================
c [1mFound solution: 47811[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42282 |   25230    85063 |    8410   12610   418105    33.2 |  5.734 % |
c |     42382 |   25230    85063 |    9251    6405   225040    35.1 |  7.708 % |
c |     42532 |   25166    84918 |   10176    6501   223523    34.4 |  8.101 % |
c |     42757 |   25166    84918 |   11193    6726   226843    33.7 |  8.101 % |
c |     43097 |   25166    84918 |   12313    7066   233023    33.0 |  8.101 % |
c |     43604 |   25166    84918 |   13544    7573   239962    31.7 |  8.101 % |
c |     44363 |   25166    84918 |   14898    8332   256382    30.8 |  8.101 % |
c |     45505 |   25166    84918 |   16388    9474   290608    30.7 |  8.101 % |
c |     47213 |   25166    84918 |   18027   11182   344075    30.8 |  8.101 % |
c |     49775 |   25089    84736 |   19830   13735   440230    32.1 |  8.617 % |
c |     53619 |   25089    84736 |   21813   17579   580938    33.0 |  8.617 % |
c |     59386 |   25073    84684 |   23994   12120   348815    28.8 |  8.659 % |
c |     68036 |   25029    84578 |   26394   20768   668462    32.2 |  8.969 % |
c |     81011 |   25029    84578 |   29033   18798  1001764    53.3 |  8.969 % |
c |    100472 |   25029    84578 |   31936   20949  1061419    50.7 |  8.969 % |
c |    129664 |   25029    84578 |   35130   29418  1366444    46.4 |  8.969 % |
c |    173453 |   24973    84449 |   38643   26511  1177352    44.4 |  9.361 % |
c |    239138 |   24973    84449 |   42508   38353  2818632    73.5 |  9.361 % |
c |    337667 |   24973    84449 |   46758   23147  1156398    50.0 |  9.361 % |
c |    485458 |   24928    84339 |   51434   41509  1869342    45.0 |  9.713 % |
c |    707141 |   24862    84193 |   56578   41062  3331587    81.1 | 10.023 % |
#### 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.85 0.95 0.91 2/54 25366
Raw data (stat): 25366 (runsolver) R 25365 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482062002 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+9.99968 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 1683 0 0 0 994 4 0 0 25 0 1 0 482062002 8601600 1661 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2100 1661 603 41 0 2059 0
vsize: 8400
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 2344 0 0 0 1991 7 0 0 25 0 1 0 482062002 11321344 2322 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2764 2322 603 41 0 2723 0
vsize: 11056
[startup+30.0016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 2437 0 0 0 2991 7 0 0 25 0 1 0 482062002 11722752 2415 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2862 2415 603 41 0 2821 0
vsize: 11448
[startup+40.0021 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 2562 0 0 0 3991 7 0 0 25 0 1 0 482062002 12251136 2540 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2991 2540 603 41 0 2950 0
vsize: 11964
[startup+50.0035 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 2562 0 0 0 4991 7 0 0 25 0 1 0 482062002 12251136 2540 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2991 2540 603 41 0 2950 0
vsize: 11964
[startup+60.0033 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 2563 0 0 0 5989 8 0 0 25 0 1 0 482062002 12251136 2541 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2991 2541 603 41 0 2950 0
vsize: 11964
[startup+70.0036 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 2869 0 0 0 6988 9 0 0 25 0 1 0 482062002 13467648 2847 4294967295 134512640 134672761 3221224528 3221223696 134553598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3288 2847 603 41 0 3247 0
vsize: 13152
[startup+80.0047 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3000 0 0 0 7987 9 0 0 25 0 1 0 482062002 14004224 2978 4294967295 134512640 134672761 3221224528 3221223696 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3419 2978 603 41 0 3378 0
vsize: 13676
[startup+90.0055 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3008 0 0 0 8988 9 0 0 25 0 1 0 482062002 14004224 2986 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3419 2986 603 41 0 3378 0
vsize: 13676
[startup+100.005 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3066 0 0 0 9988 9 0 0 25 0 1 0 482062002 14401536 3044 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3044 603 41 0 3475 0
vsize: 14064
[startup+110.005 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3108 0 0 0 10988 10 0 0 25 0 1 0 482062002 14536704 3086 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3549 3086 603 41 0 3508 0
vsize: 14196
[startup+120.006 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3263 0 0 0 11987 10 0 0 25 0 1 0 482062002 15208448 3241 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3713 3241 603 41 0 3672 0
vsize: 14852
[startup+130.005 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3263 0 0 0 12987 10 0 0 25 0 1 0 482062002 15208448 3241 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3713 3241 603 41 0 3672 0
vsize: 14852
[startup+140.007 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3336 0 0 0 13988 10 0 0 25 0 1 0 482062002 15474688 3314 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3778 3314 603 41 0 3737 0
vsize: 15112
[startup+150.007 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3336 0 0 0 14988 10 0 0 25 0 1 0 482062002 15474688 3314 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3778 3314 603 41 0 3737 0
vsize: 15112
[startup+160.007 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3348 0 0 0 15988 10 0 0 25 0 1 0 482062002 15609856 3326 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3811 3326 603 41 0 3770 0
vsize: 15244
[startup+170.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3645 0 0 0 16988 11 0 0 25 0 1 0 482062002 16805888 3623 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4103 3624 603 41 0 4062 0
vsize: 16412
[startup+180.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3832 0 0 0 17987 12 0 0 25 0 1 0 482062002 17477632 3810 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4267 3810 603 41 0 4226 0
vsize: 17068
[startup+190.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 3832 0 0 0 18988 12 0 0 25 0 1 0 482062002 17477632 3810 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4267 3810 603 41 0 4226 0
vsize: 17068
[startup+200.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 4252 0 0 0 19987 14 0 0 25 0 1 0 482062002 19222528 4230 4294967295 134512640 134672761 3221224528 3221223528 1075350205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4693 4230 603 41 0 4652 0
vsize: 18772
[startup+210.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 4793 0 0 0 20985 16 0 0 25 0 1 0 482062002 21495808 4771 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5248 4771 603 41 0 5207 0
vsize: 20992
[startup+220.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 4805 0 0 0 21987 16 0 0 25 0 1 0 482062002 21495808 4783 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5248 4783 603 41 0 5207 0
vsize: 20992
[startup+230.039 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 4805 0 0 0 22987 16 0 0 25 0 1 0 482062002 21495808 4783 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5248 4783 603 41 0 5207 0
vsize: 20992
[startup+240.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 4805 0 0 0 23987 16 0 0 25 0 1 0 482062002 21495808 4783 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5248 4783 603 41 0 5207 0
vsize: 20992
[startup+250.055 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5097 0 0 0 24988 17 0 0 25 0 1 0 482062002 22700032 5075 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5542 5075 603 41 0 5501 0
vsize: 22168
[startup+260.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 25988 17 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223632 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+270.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 26986 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223632 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+280.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 27985 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223544 1075352593 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+290.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 28986 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+300.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 29986 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+310.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 30987 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+320.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 31987 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+330.084 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 32988 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+340.085 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 33988 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+350.086 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 34988 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+360.085 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 35988 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+370.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 36989 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+380.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 37989 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+390.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 38989 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+400.091 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 39990 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+410.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 40989 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+420.091 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5114 0 0 0 41989 18 0 0 25 0 1 0 482062002 22700032 5092 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5092 603 41 0 5501 0
vsize: 22168
[startup+430.091 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5116 0 0 0 42990 18 0 0 25 0 1 0 482062002 22700032 5094 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5094 603 41 0 5501 0
vsize: 22168
[startup+440.091 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 43990 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+450.091 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 44990 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+460.091 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 45990 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+470.091 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 46990 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+480.092 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 47991 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+490.091 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 48991 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+500.092 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 49991 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+510.092 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 50991 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+520.093 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 51991 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+530.093 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 52992 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223712 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+540.093 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 53992 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+550.094 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 54992 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+560.094 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 55992 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+570.095 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 56992 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+580.095 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 57992 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+590.094 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 58993 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+600.094 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 59993 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+610.095 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 60993 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+620.096 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 61993 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+630.096 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 62993 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+640.096 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 63994 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+650.096 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 64994 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+660.096 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 65994 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+670.097 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 66994 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+680.098 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 67994 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+690.098 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5117 0 0 0 68994 18 0 0 25 0 1 0 482062002 22700032 5095 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5542 5095 603 41 0 5501 0
vsize: 22168
[startup+700.099 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5122 0 0 0 69994 18 0 0 25 0 1 0 482062002 22700032 5100 4294967295 134512640 134672761 3221224528 3221223696 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5100 603 41 0 5501 0
vsize: 22168
[startup+710.099 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5122 0 0 0 70994 18 0 0 25 0 1 0 482062002 22700032 5100 4294967295 134512640 134672761 3221224528 3221223712 134558697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5100 603 41 0 5501 0
vsize: 22168
[startup+720.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5122 0 0 0 71994 18 0 0 25 0 1 0 482062002 22700032 5100 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5100 603 41 0 5501 0
vsize: 22168
[startup+730.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5122 0 0 0 72994 18 0 0 25 0 1 0 482062002 22700032 5100 4294967295 134512640 134672761 3221224528 3221223632 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5100 603 41 0 5501 0
vsize: 22168
[startup+740.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5122 0 0 0 73995 18 0 0 25 0 1 0 482062002 22700032 5100 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5542 5100 603 41 0 5501 0
vsize: 22168
[startup+750.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5396 0 0 0 74994 19 0 0 25 0 1 0 482062002 23904256 5374 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5836 5374 603 41 0 5795 0
vsize: 23344
[startup+760.101 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5397 0 0 0 75994 19 0 0 25 0 1 0 482062002 23904256 5375 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5836 5375 603 41 0 5795 0
vsize: 23344
[startup+770.101 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5397 0 0 0 76994 19 0 0 25 0 1 0 482062002 23904256 5375 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5836 5375 603 41 0 5795 0
vsize: 23344
[startup+780.102 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5397 0 0 0 77994 19 0 0 25 0 1 0 482062002 23904256 5375 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5836 5375 603 41 0 5795 0
vsize: 23344
[startup+790.102 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5400 0 0 0 78995 19 0 0 25 0 1 0 482062002 23904256 5378 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5836 5378 603 41 0 5795 0
vsize: 23344
[startup+800.102 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5627 0 0 0 79994 20 0 0 25 0 1 0 482062002 24846336 5605 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6066 5605 603 41 0 6025 0
vsize: 24264
[startup+810.102 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5627 0 0 0 80994 20 0 0 25 0 1 0 482062002 24846336 5605 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6066 5605 603 41 0 6025 0
vsize: 24264
[startup+820.102 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5627 0 0 0 81994 20 0 0 25 0 1 0 482062002 24846336 5605 4294967295 134512640 134672761 3221224528 3221223696 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6066 5605 603 41 0 6025 0
vsize: 24264
[startup+830.102 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5627 0 0 0 82994 20 0 0 25 0 1 0 482062002 24846336 5605 4294967295 134512640 134672761 3221224528 3221223728 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6066 5605 603 41 0 6025 0
vsize: 24264
[startup+840.102 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5632 0 0 0 83995 20 0 0 25 0 1 0 482062002 24846336 5610 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6066 5610 603 41 0 6025 0
vsize: 24264
[startup+850.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5632 0 0 0 84995 20 0 0 25 0 1 0 482062002 24846336 5610 4294967295 134512640 134672761 3221224528 3221223652 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6066 5610 603 41 0 6025 0
vsize: 24264
[startup+860.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5632 0 0 0 85995 20 0 0 25 0 1 0 482062002 24846336 5610 4294967295 134512640 134672761 3221224528 3221223696 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6066 5610 603 41 0 6025 0
vsize: 24264
[startup+870.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5632 0 0 0 86995 20 0 0 25 0 1 0 482062002 24846336 5610 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6066 5610 603 41 0 6025 0
vsize: 24264
[startup+880.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5632 0 0 0 87995 20 0 0 25 0 1 0 482062002 24846336 5610 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6066 5610 603 41 0 6025 0
vsize: 24264
[startup+890.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5632 0 0 0 88995 20 0 0 25 0 1 0 482062002 24846336 5610 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6066 5610 603 41 0 6025 0
vsize: 24264
[startup+900.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5762 0 0 0 89995 21 0 0 25 0 1 0 482062002 25382912 5740 4294967295 134512640 134672761 3221224528 3221223684 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6197 5740 603 41 0 6156 0
vsize: 24788
[startup+910.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5943 0 0 0 90995 21 0 0 25 0 1 0 482062002 26177536 5921 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6391 5921 603 41 0 6350 0
vsize: 25564
[startup+920.105 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5943 0 0 0 91995 21 0 0 25 0 1 0 482062002 26177536 5921 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6391 5921 603 41 0 6350 0
vsize: 25564
[startup+930.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5943 0 0 0 92995 21 0 0 25 0 1 0 482062002 26177536 5921 4294967295 134512640 134672761 3221224528 3221223696 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6391 5921 603 41 0 6350 0
vsize: 25564
[startup+940.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5943 0 0 0 93996 21 0 0 25 0 1 0 482062002 26177536 5921 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6391 5921 603 41 0 6350 0
vsize: 25564
[startup+950.105 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 5943 0 0 0 94996 21 0 0 25 0 1 0 482062002 26177536 5921 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6391 5921 603 41 0 6350 0
vsize: 25564
[startup+960.106 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 6169 0 0 0 95995 22 0 0 25 0 1 0 482062002 27111424 6147 4294967295 134512640 134672761 3221224528 3221223484 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6147 603 41 0 6578 0
vsize: 26476
[startup+970.106 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 6463 0 0 0 96995 23 0 0 25 0 1 0 482062002 28319744 6441 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6914 6441 603 41 0 6873 0
vsize: 27656
[startup+980.107 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 6463 0 0 0 97995 23 0 0 25 0 1 0 482062002 28319744 6441 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6914 6441 603 41 0 6873 0
vsize: 27656
[startup+990.106 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 6463 0 0 0 98995 23 0 0 25 0 1 0 482062002 28319744 6441 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6914 6441 603 41 0 6873 0
vsize: 27656
[startup+1000.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 6463 0 0 0 99995 23 0 0 25 0 1 0 482062002 28319744 6441 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6914 6441 603 41 0 6873 0
vsize: 27656
[startup+1010.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 6463 0 0 0 100995 23 0 0 25 0 1 0 482062002 28319744 6441 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6914 6441 603 41 0 6873 0
vsize: 27656
[startup+1020.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 6463 0 0 0 101995 23 0 0 25 0 1 0 482062002 28319744 6441 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6914 6441 603 41 0 6873 0
vsize: 27656
[startup+1030.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 6579 0 0 0 102995 23 0 0 25 0 1 0 482062002 28712960 6557 4294967295 134512640 134672761 3221224528 3221223712 134559609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7010 6557 603 41 0 6969 0
vsize: 28040
[startup+1040.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 7109 0 0 0 103994 24 0 0 25 0 1 0 482062002 30871552 7087 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7537 7087 603 41 0 7496 0
vsize: 30148
[startup+1050.11 s]
Raw data (loadavg): 1.00 0.99 0.92 3/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 7582 0 0 0 104993 25 0 0 25 0 1 0 482062002 32886784 7560 4294967295 134512640 134672761 3221224528 3221223680 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8029 7560 603 41 0 7988 0
vsize: 32116
[startup+1060.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 7960 0 0 0 105992 27 0 0 25 0 1 0 482062002 34365440 7938 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8390 7938 603 41 0 8349 0
vsize: 33560
[startup+1070.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 106992 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223624 134555595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1080.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 107992 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223652 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1090.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 108992 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1100.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 109993 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1110.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 110993 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1120.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 111993 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223680 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1130.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 112993 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1140.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 113993 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1150.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 114993 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1160.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 115994 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1170.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 116994 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1180.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 117994 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223632 134554877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1190.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 118994 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 25366
Raw data (stat): 25366 (minisat+) R 25365 29151 29150 0 -1 0 8008 0 0 0 119994 27 0 0 25 0 1 0 482062002 34500608 7986 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 7986 603 41 0 8382 0
vsize: 33692
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 25366
Raw data (stat): 25366 (minisat+) Z 25365 29151 29150 0 -1 12 8011 0 0 0 119994 28 0 0 25 0 1 0 482062002 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: 10
Real time (s): 1200.13
CPU time (s): 1200.24
CPU user time (s): 1199.95
CPU system time (s): 0.288956
CPU usage (%): 100.009
Max. virtual memory (Kb): 33692
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####