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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-5.opb
MD5SUM	70070c820bc7d178cc8f33b42e0deead
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-28
Optimality of the best value was proved	NO
Number of terms in the objective function	595
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	595
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	595
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	595
Total number of constraints	28143
Number of constraints which are clauses	28143
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5029

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-13 21:31:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2903 boxname=wulflinc1 idbench=323 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  70070c820bc7d178cc8f33b42e0deead  /oldhome/oroussel/tmp/wulflinc1/normalized-frb35-17-5.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc1/normalized-frb35-17-5.opb
IDLAUNCH: 2903
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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	: 2
cpu MHz		: 451.053
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:        861720 kB
Buffers:         40016 kB
Cached:         108700 kB
SwapCached:          0 kB
Active:         107092 kB
Inactive:        44756 kB
HighTotal:      131008 kB
HighFree:        29596 kB
LowTotal:       903652 kB
LowFree:        832124 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           7196 kB
Slab:            15476 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:51:50 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 2903 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 28143 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   28143    56286 |    9381       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   56290   122394 |   18763       0        0     nan |  0.000 % |
c |       100 |   55818   121416 |   20639      78      529     6.8 |  1.319 % |
c |       250 |   55350   120416 |   22703     201     1432     7.1 |  2.831 % |
c |       475 |   54323   118193 |   24973     376     3383     9.0 |  5.942 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       678 |   53263   115977 |   17754     507     5021     9.9 |  5.942 % |
c |       778 |   52841   115047 |   19529     588     6229    10.6 | 11.045 % |
c |       928 |   52322   113884 |   21482     715     7585    10.6 | 12.707 % |
c |      1153 |   51428   111886 |   23630     895     9815    11.0 | 15.557 % |
c |      1490 |   49468   107434 |   25993    1105    12672    11.5 | 22.140 % |
c |      1996 |   47638   103232 |   28592    1527    18207    11.9 | 28.026 % |
c |      2756 |   44784    96705 |   31452    2088    27733    13.3 | 37.330 % |
c |      3895 |   41359    88683 |   34597    2945    40667    13.8 | 48.818 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4578 |   40279    86235 |   13426    3372    48651    14.4 | 48.818 % |
c |      4678 |   39986    85593 |   14768    3439    49906    14.5 | 53.601 % |
c |      4828 |   39929    85464 |   16245    3585    53525    14.9 | 53.786 % |
c |      5053 |   39738    84989 |   17870    3769    58890    15.6 | 54.485 % |
c |      5390 |   39304    83962 |   19657    3970    63529    16.0 | 55.987 % |
c |      5897 |   38689    82488 |   21622    4286    73190    17.1 | 58.330 % |
c |      6656 |   37185    78940 |   23784    4674    86185    18.4 | 63.301 % |
c |      7795 |   36622    77561 |   26163    5675   129966    22.9 | 65.275 % |
c |      9504 |   35725    75401 |   28779    7136   192067    26.9 | 68.457 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10440 |   35152    73982 |   11717    7917   243425    30.7 | 68.457 % |
c |     10540 |   35113    73891 |   12888    7988   246532    30.9 | 70.655 % |
c |     10690 |   35113    73891 |   14177    8138   257579    31.7 | 70.655 % |
c |     10915 |   35077    73801 |   15595    8322   262608    31.6 | 70.789 % |
c |     11252 |   34978    73564 |   17154    8601   274225    31.9 | 71.134 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11391 |   34971    73570 |   11657    8688   275965    31.8 | 71.134 % |
c |     11491 |   34902    73413 |   12822    8759   278380    31.8 | 71.445 % |
c |     11641 |   34902    73413 |   14104    8909   284047    31.9 | 71.446 % |
c |     11867 |   34896    73399 |   15515    9119   294059    32.2 | 71.466 % |
c |     12204 |   34763    73092 |   17067    9394   321190    34.2 | 71.903 % |
c |     12711 |   34609    72711 |   18773    9712   337264    34.7 | 72.472 % |
c |     13470 |   34605    72698 |   20651   10457   386838    37.0 | 72.487 % |
c |     14610 |   34380    72154 |   22716   11454   436165    38.1 | 73.293 % |
c |     16319 |   33765    70670 |   24987   12907   541843    42.0 | 75.434 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16658 |   33651    70365 |   11217   13078   538486    41.2 | 75.434 % |
c |     16758 |   33651    70365 |   12338   13178   543720    41.3 | 75.826 % |
c |     16908 |   33598    70240 |   13572   13315   549004    41.2 | 76.011 % |
c |     17133 |   33492    69992 |   14929   13474   555912    41.3 | 76.371 % |
c |     17471 |   33492    69992 |   16422   13812   572516    41.5 | 76.370 % |
c |     17978 |   33390    69747 |   18065   14288   590646    41.3 | 76.730 % |
c |     18737 |   33266    69453 |   19871   15005   645411    43.0 | 77.151 % |
c |     19876 |   33263    69446 |   21858   16138   775398    48.0 | 77.161 % |
c |     21586 |   33025    68873 |   24044   17787   883974    49.7 | 78.013 % |
c |     24149 |   33025    68873 |   26449   20350  1110021    54.5 | 78.013 % |
c |     27994 |   33025    68873 |   29094   24195  1446802    59.8 | 78.013 % |
c |     33762 |   32912    68606 |   32003   29913  1976061    66.1 | 78.408 % |
c |     42412 |   32688    68047 |   35203   38230  2602127    68.1 | 79.250 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54813 |   32709    68118 |   10903   50607  3631857    71.8 | 79.250 % |
c |     54913 |   32665    68010 |   11993   17614  1027595    58.3 | 79.420 % |
c |     55063 |   32665    68010 |   13192   17764  1033328    58.2 | 79.420 % |
c |     55288 |   32632    67926 |   14511   17973  1042889    58.0 | 79.537 % |
c |     55625 |   32632    67926 |   15963   18310  1077898    58.9 | 79.537 % |
c |     56133 |   32626    67909 |   17559   18796  1115938    59.4 | 79.563 % |
c |     56892 |   32626    67909 |   19315   19555  1163074    59.5 | 79.563 % |
c |     58031 |   32585    67812 |   21246   20688  1247141    60.3 | 79.706 % |
c |     59739 |   32585    67812 |   23371   22396  1358285    60.6 | 79.706 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61766 |   32459    67492 |   10819   24393  1480169    60.7 | 79.706 % |
c |     61866 |   32459    67492 |   11900   24493  1483862    60.6 | 80.152 % |
c |     62016 |   32422    67401 |   13090   24627  1493869    60.7 | 80.285 % |
c |     62241 |   32400    67340 |   14400   24844  1515014    61.0 | 80.372 % |
c |     62579 |   32361    67247 |   15840   25167  1534905    61.0 | 80.510 % |
c |     63085 |   32361    67247 |   17424   25673  1569859    61.1 | 80.510 % |
c |     63845 |   32361    67247 |   19166   26433  1617338    61.2 | 80.510 % |
c |     64985 |   32361    67247 |   21083   27573  1724425    62.5 | 80.510 % |
c |     66693 |   32361    67247 |   23191   29281  1823567    62.3 | 80.510 % |
c |     69255 |   32361    67247 |   25510   31843  2022398    63.5 | 80.510 % |
c |     73099 |   32266    67009 |   28061   35630  2258988    63.4 | 80.852 % |
c |     78867 |   32266    67009 |   30867   41398  2541641    61.4 | 80.852 % |
c |     87517 |   32261    66998 |   33954   17592   605784    34.4 | 80.868 % |
c |    100493 |   32145    66707 |   37350   30555  1527180    50.0 | 81.251 % |
c |    119954 |   32136    66686 |   41085   50010  2776028    55.5 | 81.282 % |
c |    149146 |   32059    66501 |   45193   39406  2390640    60.7 | 81.558 % |
c |    192935 |   32018    66406 |   49713   40611  2365930    58.3 | 81.696 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    234340 |   31964    66282 |   10654   33803  1904300    56.3 | 81.696 % |
c |    234440 |   31964    66282 |   11719   16070   660384    41.1 | 81.909 % |
c |    234590 |   31939    66229 |   12891   16216   667281    41.1 | 81.980 % |
c |    234817 |   31939    66229 |   14180   16443   680004    41.4 | 81.980 % |
c |    235155 |   31853    66019 |   15598   16755   688813    41.1 | 82.286 % |
c |    235661 |   31853    66019 |   17158   17261   714839    41.4 | 82.286 % |
c |    236420 |   31848    66006 |   18874   18019   754497    41.9 | 82.307 % |
c |    237559 |   31848    66006 |   20761   19158   827477    43.2 | 82.307 % |
c |    239268 |   31848    66006 |   22837   20867   941214    45.1 | 82.307 % |
c |    241830 |   31845    65999 |   25121   23424  1134066    48.4 | 82.317 % |
c |    245674 |   31832    65966 |   27633   27261  1379284    50.6 | 82.368 % |
c |    251442 |   31821    65939 |   30397   33025  1770495    53.6 | 82.409 % |
c |    260091 |   31723    65693 |   33436   41618  2363593    56.8 | 82.781 % |
c |    273065 |   31702    65642 |   36780   21888  1194237    54.6 | 82.858 % |
c |    292526 |   31595    65388 |   40458   41329  2455787    59.4 | 83.236 % |
c |    321718 |   31590    65375 |   44504   31574  1206245    38.2 | 83.256 % |
c |    365507 |   31587    65368 |   48954   33871  1201100    35.5 | 83.266 % |
c |    431191 |   31587    65368 |   53850   55118  1835677    33.3 | 83.266 % |
c |    529717 |   31516    65201 |   59235   54938  1748182    31.8 | 83.511 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/56 15466
Raw data (stat): 15466 (runsolver) R 15465 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 364136212 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.96 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 2296 0 0 0 994 5 0 0 25 0 1 0 364136212 11571200 2267 4294967295 134512640 134672761 3221224640 3221223792 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2825 2267 603 41 0 2784 0
vsize: 11300
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 2405 0 0 0 1993 5 0 0 25 0 1 0 364136212 12099584 2376 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2954 2376 603 41 0 2913 0
vsize: 11816
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 2883 0 0 0 2992 7 0 0 25 0 1 0 364136212 14082048 2854 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3438 2854 603 41 0 3397 0
vsize: 13752
[startup+40.0023 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 3461 0 0 0 3990 9 0 0 25 0 1 0 364136212 16478208 3432 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4023 3432 603 41 0 3982 0
vsize: 16092
[startup+50.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 4044 0 0 0 4988 11 0 0 25 0 1 0 364136212 18763776 4015 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4581 4015 603 41 0 4540 0
vsize: 18324
[startup+60.0035 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 4604 0 0 0 5986 14 0 0 25 0 1 0 364136212 21049344 4575 4294967295 134512640 134672761 3221224640 3221223776 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5139 4575 603 41 0 5098 0
vsize: 20556
[startup+70.0043 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 4992 0 0 0 6984 16 0 0 25 0 1 0 364136212 22786048 4963 4294967295 134512640 134672761 3221224640 3221223824 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5563 4963 603 41 0 5522 0
vsize: 22252
[startup+80.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 5387 0 0 0 7982 17 0 0 25 0 1 0 364136212 24387584 5358 4294967295 134512640 134672761 3221224640 3221223744 134555175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5954 5358 603 41 0 5913 0
vsize: 23816
[startup+90.0048 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 5772 0 0 0 8981 19 0 0 25 0 1 0 364136212 25866240 5743 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6315 5743 603 41 0 6274 0
vsize: 25260
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6182 0 0 0 9979 21 0 0 25 0 1 0 364136212 27615232 6153 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6742 6153 603 41 0 6701 0
vsize: 26968
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6331 0 0 0 10979 21 0 0 25 0 1 0 364136212 28147712 6302 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6302 603 41 0 6831 0
vsize: 27488
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 11979 21 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 12979 21 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 13979 21 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 14979 22 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223776 134560657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 15979 22 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 16979 22 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223744 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 17979 22 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 18979 22 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 19979 22 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 20979 23 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 21979 23 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6352 0 0 0 22979 23 0 0 25 0 1 0 364136212 28307456 6323 4294967295 134512640 134672761 3221224640 3221223808 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6323 603 41 0 6870 0
vsize: 27644
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6356 0 0 0 23979 23 0 0 25 0 1 0 364136212 28307456 6327 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6327 603 41 0 6870 0
vsize: 27644
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6359 0 0 0 24979 23 0 0 25 0 1 0 364136212 28307456 6330 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6330 603 41 0 6870 0
vsize: 27644
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15466
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6359 0 0 0 25978 24 0 0 25 0 1 0 364136212 28307456 6330 4294967295 134512640 134672761 3221224640 3221223812 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6330 603 41 0 6870 0
vsize: 27644
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6359 0 0 0 26978 24 0 0 25 0 1 0 364136212 28307456 6330 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6330 603 41 0 6870 0
vsize: 27644
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6359 0 0 0 27978 24 0 0 25 0 1 0 364136212 28307456 6330 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6330 603 41 0 6870 0
vsize: 27644
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6359 0 0 0 28978 24 0 0 25 0 1 0 364136212 28307456 6330 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6330 603 41 0 6870 0
vsize: 27644
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6359 0 0 0 29978 25 0 0 25 0 1 0 364136212 28307456 6330 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6330 603 41 0 6870 0
vsize: 27644
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6359 0 0 0 30978 25 0 0 25 0 1 0 364136212 28307456 6330 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6330 603 41 0 6870 0
vsize: 27644
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6360 0 0 0 31978 25 0 0 25 0 1 0 364136212 28307456 6331 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6331 603 41 0 6870 0
vsize: 27644
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6373 0 0 0 32978 25 0 0 25 0 1 0 364136212 28450816 6344 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6946 6344 603 41 0 6905 0
vsize: 27784
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6386 0 0 0 33978 25 0 0 25 0 1 0 364136212 28450816 6357 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6946 6357 603 41 0 6905 0
vsize: 27784
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6450 0 0 0 34977 26 0 0 25 0 1 0 364136212 28717056 6421 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7011 6421 603 41 0 6970 0
vsize: 28044
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6708 0 0 0 35976 27 0 0 25 0 1 0 364136212 29827072 6679 4294967295 134512640 134672761 3221224640 3221223296 134565768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7282 6679 603 41 0 7241 0
vsize: 29128
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6708 0 0 0 36976 27 0 0 25 0 1 0 364136212 29827072 6679 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7282 6679 603 41 0 7241 0
vsize: 29128
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6708 0 0 0 37977 27 0 0 25 0 1 0 364136212 29827072 6679 4294967295 134512640 134672761 3221224640 3221223808 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7282 6679 603 41 0 7241 0
vsize: 29128
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6708 0 0 0 38977 27 0 0 25 0 1 0 364136212 29827072 6679 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7282 6679 603 41 0 7241 0
vsize: 29128
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6715 0 0 0 39977 28 0 0 25 0 1 0 364136212 29827072 6686 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7282 6686 603 41 0 7241 0
vsize: 29128
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6715 0 0 0 40977 28 0 0 25 0 1 0 364136212 29827072 6686 4294967295 134512640 134672761 3221224640 3221223824 134558836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7282 6686 603 41 0 7241 0
vsize: 29128
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6716 0 0 0 41977 28 0 0 25 0 1 0 364136212 29827072 6687 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7282 6687 603 41 0 7241 0
vsize: 29128
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 6823 0 0 0 42977 28 0 0 25 0 1 0 364136212 30228480 6794 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7380 6794 603 41 0 7339 0
vsize: 29520
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7215 0 0 0 43975 30 0 0 25 0 1 0 364136212 31834112 7186 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7772 7186 603 41 0 7731 0
vsize: 31088
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7585 0 0 0 44974 31 0 0 25 0 1 0 364136212 33431552 7556 4294967295 134512640 134672761 3221224640 3221223808 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8162 7556 603 41 0 8121 0
vsize: 32648
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 45974 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 46974 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 47975 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223776 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 48975 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223824 134558925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 49975 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 50975 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 51975 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 52975 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 53975 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 54976 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223844 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15468
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 55976 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223840 134557915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 56976 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 57976 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 58976 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 59976 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 60977 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 61977 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 62977 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7783 0 0 0 63977 31 0 0 25 0 1 0 364136212 34488320 7754 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7754 603 41 0 8379 0
vsize: 33680
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7784 0 0 0 64977 31 0 0 25 0 1 0 364136212 34488320 7755 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7755 603 41 0 8379 0
vsize: 33680
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7784 0 0 0 65978 31 0 0 25 0 1 0 364136212 34488320 7755 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7755 603 41 0 8379 0
vsize: 33680
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7784 0 0 0 66978 31 0 0 25 0 1 0 364136212 34488320 7755 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7755 603 41 0 8379 0
vsize: 33680
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7784 0 0 0 67978 31 0 0 25 0 1 0 364136212 34488320 7755 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7755 603 41 0 8379 0
vsize: 33680
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7784 0 0 0 68978 31 0 0 25 0 1 0 364136212 34488320 7755 4294967295 134512640 134672761 3221224640 3221223744 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7755 603 41 0 8379 0
vsize: 33680
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7784 0 0 0 69978 31 0 0 25 0 1 0 364136212 34488320 7755 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7755 603 41 0 8379 0
vsize: 33680
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7784 0 0 0 70979 31 0 0 25 0 1 0 364136212 34488320 7755 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7755 603 41 0 8379 0
vsize: 33680
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7784 0 0 0 71979 31 0 0 25 0 1 0 364136212 34488320 7755 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7755 603 41 0 8379 0
vsize: 33680
[startup+730.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7784 0 0 0 72979 31 0 0 25 0 1 0 364136212 34488320 7755 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7755 603 41 0 8379 0
vsize: 33680
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7785 0 0 0 73979 31 0 0 25 0 1 0 364136212 34488320 7756 4294967295 134512640 134672761 3221224640 3221223808 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7756 603 41 0 8379 0
vsize: 33680
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7785 0 0 0 74979 31 0 0 25 0 1 0 364136212 34488320 7756 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7756 603 41 0 8379 0
vsize: 33680
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7785 0 0 0 75980 31 0 0 25 0 1 0 364136212 34488320 7756 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7756 603 41 0 8379 0
vsize: 33680
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7785 0 0 0 76980 31 0 0 25 0 1 0 364136212 34488320 7756 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7756 603 41 0 8379 0
vsize: 33680
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7785 0 0 0 77980 31 0 0 25 0 1 0 364136212 34488320 7756 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7756 603 41 0 8379 0
vsize: 33680
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7785 0 0 0 78980 31 0 0 25 0 1 0 364136212 34488320 7756 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7756 603 41 0 8379 0
vsize: 33680
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7801 0 0 0 79980 31 0 0 25 0 1 0 364136212 34639872 7772 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8457 7772 603 41 0 8416 0
vsize: 33828
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7804 0 0 0 80980 31 0 0 25 0 1 0 364136212 34639872 7775 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8457 7775 603 41 0 8416 0
vsize: 33828
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7804 0 0 0 81981 31 0 0 25 0 1 0 364136212 34639872 7775 4294967295 134512640 134672761 3221224640 3221223744 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8457 7775 603 41 0 8416 0
vsize: 33828
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7804 0 0 0 82981 31 0 0 25 0 1 0 364136212 34639872 7775 4294967295 134512640 134672761 3221224640 3221223808 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8457 7775 603 41 0 8416 0
vsize: 33828
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7804 0 0 0 83981 31 0 0 25 0 1 0 364136212 34639872 7775 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8457 7775 603 41 0 8416 0
vsize: 33828
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7804 0 0 0 84981 31 0 0 25 0 1 0 364136212 34639872 7775 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8457 7775 603 41 0 8416 0
vsize: 33828
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15470
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7804 0 0 0 85981 31 0 0 25 0 1 0 364136212 34639872 7775 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8457 7775 603 41 0 8416 0
vsize: 33828
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7804 0 0 0 86981 31 0 0 25 0 1 0 364136212 34639872 7775 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8457 7775 603 41 0 8416 0
vsize: 33828
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7804 0 0 0 87982 31 0 0 25 0 1 0 364136212 34639872 7775 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8457 7775 603 41 0 8416 0
vsize: 33828
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7804 0 0 0 88982 32 0 0 25 0 1 0 364136212 34639872 7775 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7775 603 41 0 8416 0
vsize: 33828
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7804 0 0 0 89982 32 0 0 25 0 1 0 364136212 34639872 7775 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7775 603 41 0 8416 0
vsize: 33828
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7806 0 0 0 90982 32 0 0 25 0 1 0 364136212 34639872 7777 4294967295 134512640 134672761 3221224640 3221223824 134558878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7777 603 41 0 8416 0
vsize: 33828
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 91982 32 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 92982 32 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 93982 32 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 94982 32 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 95982 32 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 96982 32 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 97982 33 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 98982 33 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 99982 33 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223776 134565078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 100982 33 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223776 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 101982 33 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 102982 33 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223744 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 103982 33 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 104982 33 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 105982 34 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 106982 34 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 107982 34 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 108982 34 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 109982 34 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223776 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 110982 34 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 111982 34 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7808 0 0 0 112982 35 0 0 25 0 1 0 364136212 34639872 7779 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7779 603 41 0 8416 0
vsize: 33828
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7809 0 0 0 113982 35 0 0 25 0 1 0 364136212 34639872 7780 4294967295 134512640 134672761 3221224640 3221223776 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7780 603 41 0 8416 0
vsize: 33828
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7812 0 0 0 114982 35 0 0 25 0 1 0 364136212 34639872 7783 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7783 603 41 0 8416 0
vsize: 33828
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15472
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7813 0 0 0 115982 35 0 0 25 0 1 0 364136212 34639872 7784 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7784 603 41 0 8416 0
vsize: 33828
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15474
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7813 0 0 0 116982 35 0 0 25 0 1 0 364136212 34639872 7784 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7784 603 41 0 8416 0
vsize: 33828
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15474
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7813 0 0 0 117982 35 0 0 25 0 1 0 364136212 34639872 7784 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7784 603 41 0 8416 0
vsize: 33828
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15474
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7813 0 0 0 118982 35 0 0 25 0 1 0 364136212 34639872 7784 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7784 603 41 0 8416 0
vsize: 33828
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15474
Raw data (stat): 15466 (minisat+) R 15465 12452 12451 0 -1 0 7813 0 0 0 119982 36 0 0 25 0 1 0 364136212 34639872 7784 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8457 7784 603 41 0 8416 0
vsize: 33828
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 15474
Raw data (stat): 15466 (minisat+) Z 15465 12452 12451 0 -1 12 7816 0 0 0 119983 37 0 0 25 0 1 0 364136212 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.06
CPU time (s): 1200.21
CPU user time (s): 1199.83
CPU system time (s): 0.374943
CPU usage (%): 100.012
Max. virtual memory (Kb): 33828
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####