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-4.opb
MD5SUM	e3892e1941a878802a8ccbbd36201a02
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-27
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	27842
Number of constraints which are clauses	27842
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 5028

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-13 21:31:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2894 boxname=wulflinc9 idbench=322 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  e3892e1941a878802a8ccbbd36201a02  /oldhome/oroussel/tmp/wulflinc9/normalized-frb35-17-4.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc9/normalized-frb35-17-4.opb
IDLAUNCH: 2894
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        912400 kB
Buffers:         34044 kB
Cached:          68208 kB
SwapCached:        564 kB
Active:          50804 kB
Inactive:        54896 kB
HighTotal:      131008 kB
HighFree:        58856 kB
LowTotal:       903652 kB
LowFree:        853544 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11008 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:51:21 (client local time) WITH STATUS 10 IN 1200.11 SECONDS
stats: 2894 7 1200.11 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27842 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 |   27842    55684 |    9280       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -26[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 |   56133   122130 |   18711       0        0     nan |  0.000 % |
c |       100 |   55674   121173 |   20582      85      517     6.1 |  1.318 % |
c |       250 |   55337   120462 |   22640     201     1671     8.3 |  2.285 % |
c |       475 |   53886   117283 |   24904     355     3653    10.3 |  6.749 % |
c |       813 |   52308   113815 |   27394     620     7389    11.9 | 11.632 % |
c |      1319 |   49554   107621 |   30134     953    11439    12.0 | 20.509 % |
c |      2078 |   46551   100685 |   33147    1523    18456    12.1 | 30.615 % |
c |      3217 |   42835    92193 |   36462    2389    34261    14.3 | 42.639 % |
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 |      3273 |   42557    91588 |   14185    2416    34615    14.3 | 42.639 % |
c |      3373 |   42214    90786 |   15603    2489    35595    14.3 | 45.030 % |
c |      3523 |   41934    90117 |   17163    2594    37012    14.3 | 45.977 % |
c |      3748 |   41522    89143 |   18880    2783    39915    14.3 | 47.372 % |
c |      4086 |   40623    87001 |   20768    2975    42882    14.4 | 50.494 % |
c |      4593 |   39615    84625 |   22845    3304    51715    15.7 | 53.972 % |
c |      5353 |   38103    81054 |   25129    3854    65467    17.0 | 59.168 % |
c |      6492 |   37040    78558 |   27642    4854    94566    19.5 | 62.852 % |
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 |      7236 |   36536    77417 |   12178    5459   115634    21.2 | 62.852 % |
c |      7336 |   36373    77022 |   13395    5525   117833    21.3 | 65.194 % |
c |      7486 |   36245    76711 |   14735    5659   121848    21.5 | 65.636 % |
c |      7712 |   35618    75194 |   16208    5758   121613    21.1 | 67.804 % |
c |      8049 |   35083    73909 |   17829    5937   129670    21.8 | 69.674 % |
c |      8555 |   35082    73906 |   19612    6440   149607    23.2 | 69.679 % |
c |      9314 |   34665    72910 |   21574    7108   172599    24.3 | 71.138 % |
c |     10454 |   34563    72672 |   23731    8226   223484    27.2 | 71.487 % |
c |     12162 |   34403    72291 |   26104    9826   305581    31.1 | 72.052 % |
c |     14725 |   33512    70136 |   28715   11797   413482    35.0 | 75.269 % |
c |     18569 |   32730    68273 |   31586   14907   673193    45.2 | 78.002 % |
c |     24336 |   32584    67918 |   34745   20503  1088479    53.1 | 78.521 % |
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 |     25008 |   32376    67375 |   10792   20807  1127008    54.2 | 78.521 % |
c |     25109 |   32333    67266 |   11871   20854  1131597    54.3 | 79.396 % |
c |     25259 |   32266    67098 |   13058   20933  1134331    54.2 | 79.653 % |
c |     25484 |   32266    67098 |   14364   21158  1153914    54.5 | 79.653 % |
c |     25824 |   32266    67098 |   15800   21498  1181497    55.0 | 79.653 % |
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 |     26069 |   32269    67111 |   10756   20959  1109301    52.9 | 79.653 % |
c |     26169 |   32220    66999 |   11831   21035  1113907    53.0 | 79.898 % |
c |     26319 |   32220    66999 |   13014   21185  1119388    52.8 | 79.898 % |
c |     26544 |   32174    66891 |   14316   21380  1132489    53.0 | 80.051 % |
c |     26881 |   32174    66891 |   15747   21717  1150097    53.0 | 80.051 % |
c |     27388 |   32126    66770 |   17322   22203  1170894    52.7 | 80.215 % |
c |     28148 |   32036    66557 |   19054   22829  1208152    52.9 | 80.527 % |
c |     29287 |   32036    66557 |   20960   23968  1254726    52.4 | 80.527 % |
c |     30995 |   32008    66487 |   23056   25554  1358136    53.1 | 80.634 % |
c |     33557 |   32008    66487 |   25362   28116  1511958    53.8 | 80.634 % |
c |     37401 |   32008    66487 |   27898   31960  1790963    56.0 | 80.634 % |
c |     43167 |   31963    66380 |   30688   37641  2179278    57.9 | 80.788 % |
c |     51816 |   31942    66327 |   33756   46095  2740539    59.5 | 80.865 % |
c |     64790 |   31936    66313 |   37132   23972  1287927    53.7 | 80.885 % |
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 |     83994 |   31772    65908 |   10590   43119  2704132    62.7 | 80.885 % |
c |     84094 |   31769    65901 |   11649   16788   764343    45.5 | 81.544 % |
c |     84245 |   31761    65883 |   12813   16934   773077    45.7 | 81.569 % |
c |     84470 |   31761    65883 |   14095   17159   787038    45.9 | 81.569 % |
c |     84807 |   31629    65553 |   15504   17469   799984    45.8 | 82.070 % |
c |     85314 |   31616    65520 |   17055   17970   827588    46.1 | 82.121 % |
c |     86073 |   31535    65323 |   18760   18695   873445    46.7 | 82.407 % |
c |     87212 |   31529    65309 |   20636   19831   940958    47.4 | 82.428 % |
c |     88920 |   31523    65295 |   22700   21535  1039370    48.3 | 82.448 % |
c |     91482 |   31523    65295 |   24970   24097  1198465    49.7 | 82.448 % |
c |     95326 |   31486    65206 |   27467   27922  1432420    51.3 | 82.581 % |
c |    101092 |   31447    65117 |   30214   33656  1817647    54.0 | 82.708 % |
c |    109742 |   31438    65094 |   33235   42294  2206478    52.2 | 82.744 % |
c |    122717 |   31429    65073 |   36559   23198   776943    33.5 | 82.775 % |
c |    142179 |   31427    65069 |   40215   42658  1545047    36.2 | 82.780 % |
c |    171371 |   31424    65062 |   44237   32274  1209176    37.5 | 82.790 % |
c |    215161 |   31396    64996 |   48660   32992  1383853    41.9 | 82.887 % |
c |    280846 |   31348    64880 |   53526   51753  1853976    35.8 | 83.061 % |
c |    379372 |   31268    64690 |   58879   48632  1483738    30.5 | 83.337 % |
c ==============================================================================
c [1mFound solution: -34[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 |    387520 |   31254    64622 |   10418   56778  1800142    31.7 | 83.337 % |
c |    387621 |   31254    64622 |   11459   21874   574796    26.3 | 83.395 % |
c |    387771 |   31254    64622 |   12605   22024   579120    26.3 | 83.395 % |
c |    387996 |   31254    64622 |   13866   22249   585284    26.3 | 83.395 % |
c |    388334 |   31254    64622 |   15252   22587   595104    26.3 | 83.395 % |
c |    388840 |   31254    64622 |   16778   23093   611433    26.5 | 83.395 % |
c |    389599 |   31254    64622 |   18456   23852   651357    27.3 | 83.395 % |
c |    390738 |   31254    64622 |   20301   24991   708484    28.3 | 83.395 % |
c |    392446 |   31254    64622 |   22331   26699   784774    29.4 | 83.395 % |
c |    395008 |   31254    64622 |   24565   29261   882101    30.1 | 83.395 % |
c |    398852 |   31254    64622 |   27021   33105  1025751    31.0 | 83.395 % |
c |    404619 |   31237    64583 |   29723   38861  1224818    31.5 | 83.451 % |
c |    413269 |   31193    64477 |   32696   19145   554379    29.0 | 83.609 % |
c |    426243 |   31188    64466 |   35965   32115  1008537    31.4 | 83.625 % |
c |    445704 |   31188    64466 |   39562   51576  1732486    33.6 | 83.624 % |
c |    474896 |   31175    64437 |   43518   43794  1320198    30.1 | 83.665 % |
c |    518685 |   31066    64153 |   47870   45690  1182298    25.9 | 84.089 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:23198     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    565168 |   49180   106489 |   16393   38187  1077494    28.2 | 84.089 % |
c |    565268 |   49180   106489 |   18032   15309   289280    18.9 | 55.800 % |
c |    565418 |   49180   106489 |   19835   15459   294371    19.0 | 55.800 % |
c |    565643 |   49180   106489 |   21819   15684   302669    19.3 | 55.800 % |
c |    565980 |   49180   106489 |   24000   16021   312388    19.5 | 55.800 % |
c |    566490 |   49180   106489 |   26401   16531   329375    19.9 | 55.800 % |
c |    567250 |   49180   106489 |   29041   17291   353999    20.5 | 55.800 % |
c |    568389 |   49180   106489 |   31945   18430   386682    21.0 | 55.800 % |
c |    570097 |   49180   106489 |   35139   20138   435618    21.6 | 55.800 % |
c |    572659 |   49180   106489 |   38653   22700   507140    22.3 | 55.800 % |
c |    576504 |   49139   106407 |   42519   26544   621579    23.4 | 55.877 % |
c |    582270 |   49139   106407 |   46771   32310   777211    24.1 | 55.877 % |
c |    590919 |   49102   106333 |   51448   40958  1110939    27.1 | 55.940 % |
#### 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/54 633
Raw data (stat): 633 (runsolver) R 632 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420988062 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.0009 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 2243 0 0 0 992 6 0 0 25 0 1 0 420988062 11313152 2214 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2762 2214 603 41 0 2721 0
vsize: 11048
[startup+20.0022 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 2387 0 0 0 1992 7 0 0 25 0 1 0 420988062 11960320 2358 4294967295 134512640 134672761 3221224640 3221223696 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2920 2358 603 41 0 2879 0
vsize: 11680
[startup+30.0034 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 2902 0 0 0 2990 8 0 0 25 0 1 0 420988062 14032896 2873 4294967295 134512640 134672761 3221224640 3221223812 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3426 2873 603 41 0 3385 0
vsize: 13704
[startup+40.0032 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 3453 0 0 0 3987 11 0 0 25 0 1 0 420988062 16453632 3424 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4017 3424 603 41 0 3976 0
vsize: 16068
[startup+50.0035 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 3770 0 0 0 4986 13 0 0 25 0 1 0 420988062 17653760 3741 4294967295 134512640 134672761 3221224640 3221223776 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4310 3741 603 41 0 4269 0
vsize: 17240
[startup+60.0038 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 4226 0 0 0 5984 15 0 0 25 0 1 0 420988062 19521536 4197 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4766 4197 603 41 0 4725 0
vsize: 19064
[startup+70.0045 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 4660 0 0 0 6982 16 0 0 25 0 1 0 420988062 21385216 4631 4294967295 134512640 134672761 3221224640 3221223888 134562672 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5221 4631 603 41 0 5180 0
vsize: 20884
[startup+80.0058 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5045 0 0 0 7981 18 0 0 25 0 1 0 420988062 22990848 5016 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5613 5016 603 41 0 5572 0
vsize: 22452
[startup+90.0061 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5357 0 0 0 8980 19 0 0 25 0 1 0 420988062 24182784 5328 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5904 5328 603 41 0 5863 0
vsize: 23616
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5650 0 0 0 9979 20 0 0 25 0 1 0 420988062 25391104 5621 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6199 5621 603 41 0 6158 0
vsize: 24796
[startup+110.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5812 0 0 0 10978 21 0 0 25 0 1 0 420988062 26050560 5783 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6360 5783 603 41 0 6319 0
vsize: 25440
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5812 0 0 0 11977 21 0 0 25 0 1 0 420988062 26050560 5783 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6360 5783 603 41 0 6319 0
vsize: 25440
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5812 0 0 0 12977 22 0 0 25 0 1 0 420988062 26050560 5783 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6360 5783 603 41 0 6319 0
vsize: 25440
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5812 0 0 0 13977 22 0 0 25 0 1 0 420988062 26050560 5783 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6360 5783 603 41 0 6319 0
vsize: 25440
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5812 0 0 0 14976 22 0 0 25 0 1 0 420988062 26050560 5783 4294967295 134512640 134672761 3221224640 3221223824 134558941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6360 5783 603 41 0 6319 0
vsize: 25440
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 15976 22 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223824 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 16975 23 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 17975 23 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 18974 24 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 19974 24 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 20973 25 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 21973 25 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 22973 25 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 23972 26 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 24972 26 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 25972 26 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5832 0 0 0 26972 26 0 0 25 0 1 0 420988062 26210304 5803 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5803 603 41 0 6358 0
vsize: 25596
[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5834 0 0 0 27972 26 0 0 25 0 1 0 420988062 26210304 5805 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5805 603 41 0 6358 0
vsize: 25596
[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5838 0 0 0 28972 27 0 0 25 0 1 0 420988062 26210304 5809 4294967295 134512640 134672761 3221224640 3221223744 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5809 603 41 0 6358 0
vsize: 25596
[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5838 0 0 0 29971 27 0 0 25 0 1 0 420988062 26210304 5809 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5809 603 41 0 6358 0
vsize: 25596
[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5838 0 0 0 30971 27 0 0 25 0 1 0 420988062 26210304 5809 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5809 603 41 0 6358 0
vsize: 25596
[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5838 0 0 0 31971 27 0 0 25 0 1 0 420988062 26210304 5809 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5809 603 41 0 6358 0
vsize: 25596
[startup+330.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5838 0 0 0 32970 28 0 0 25 0 1 0 420988062 26210304 5809 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5809 603 41 0 6358 0
vsize: 25596
[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5838 0 0 0 33970 28 0 0 25 0 1 0 420988062 26210304 5809 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5809 603 41 0 6358 0
vsize: 25596
[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5838 0 0 0 34970 28 0 0 25 0 1 0 420988062 26210304 5809 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5809 603 41 0 6358 0
vsize: 25596
[startup+360.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5838 0 0 0 35970 28 0 0 25 0 1 0 420988062 26210304 5809 4294967295 134512640 134672761 3221224640 3221223824 134558880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5809 603 41 0 6358 0
vsize: 25596
[startup+370.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5838 0 0 0 36969 29 0 0 25 0 1 0 420988062 26210304 5809 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5809 603 41 0 6358 0
vsize: 25596
[startup+380.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5841 0 0 0 37969 29 0 0 25 0 1 0 420988062 26210304 5812 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5812 603 41 0 6358 0
vsize: 25596
[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5842 0 0 0 38968 30 0 0 25 0 1 0 420988062 26210304 5813 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5813 603 41 0 6358 0
vsize: 25596
[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5842 0 0 0 39968 30 0 0 25 0 1 0 420988062 26210304 5813 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5813 603 41 0 6358 0
vsize: 25596
[startup+410.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5842 0 0 0 40968 30 0 0 25 0 1 0 420988062 26210304 5813 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5813 603 41 0 6358 0
vsize: 25596
[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5842 0 0 0 41967 31 0 0 25 0 1 0 420988062 26210304 5813 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5813 603 41 0 6358 0
vsize: 25596
[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5842 0 0 0 42967 31 0 0 25 0 1 0 420988062 26210304 5813 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5813 603 41 0 6358 0
vsize: 25596
[startup+440.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5842 0 0 0 43967 31 0 0 25 0 1 0 420988062 26210304 5813 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5813 603 41 0 6358 0
vsize: 25596
[startup+450.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5842 0 0 0 44966 32 0 0 25 0 1 0 420988062 26210304 5813 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5813 603 41 0 6358 0
vsize: 25596
[startup+460.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5842 0 0 0 45966 32 0 0 25 0 1 0 420988062 26210304 5813 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5813 603 41 0 6358 0
vsize: 25596
[startup+470.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 5898 0 0 0 46966 32 0 0 25 0 1 0 420988062 26472448 5869 4294967295 134512640 134672761 3221224640 3221223744 134560390 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6463 5869 603 41 0 6422 0
vsize: 25852
[startup+480.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6072 0 0 0 47965 33 0 0 25 0 1 0 420988062 27398144 6043 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6689 6043 603 41 0 6648 0
vsize: 26756
[startup+490.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6072 0 0 0 48965 33 0 0 25 0 1 0 420988062 27398144 6043 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6689 6043 603 41 0 6648 0
vsize: 26756
[startup+500.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6072 0 0 0 49964 33 0 0 25 0 1 0 420988062 27398144 6043 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6689 6043 603 41 0 6648 0
vsize: 26756
[startup+510.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6082 0 0 0 50964 34 0 0 25 0 1 0 420988062 27549696 6053 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6726 6053 603 41 0 6685 0
vsize: 26904
[startup+520.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6097 0 0 0 51964 34 0 0 25 0 1 0 420988062 27549696 6068 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6726 6068 603 41 0 6685 0
vsize: 26904
[startup+530.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6107 0 0 0 52964 34 0 0 25 0 1 0 420988062 27549696 6078 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6726 6078 603 41 0 6685 0
vsize: 26904
[startup+540.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6109 0 0 0 53963 34 0 0 25 0 1 0 420988062 27549696 6080 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6726 6080 603 41 0 6685 0
vsize: 26904
[startup+550.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6126 0 0 0 54963 34 0 0 25 0 1 0 420988062 27746304 6097 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6774 6097 603 41 0 6733 0
vsize: 27096
[startup+560.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6139 0 0 0 55962 35 0 0 25 0 1 0 420988062 27746304 6110 4294967295 134512640 134672761 3221224640 3221223824 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6774 6110 603 41 0 6733 0
vsize: 27096
[startup+570.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6140 0 0 0 56962 35 0 0 25 0 1 0 420988062 27746304 6111 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6774 6111 603 41 0 6733 0
vsize: 27096
[startup+580.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6140 0 0 0 57962 35 0 0 25 0 1 0 420988062 27746304 6111 4294967295 134512640 134672761 3221224640 3221223744 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6774 6111 603 41 0 6733 0
vsize: 27096
[startup+590.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6146 0 0 0 58963 35 0 0 25 0 1 0 420988062 27746304 6117 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6774 6117 603 41 0 6733 0
vsize: 27096
[startup+600.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6150 0 0 0 59963 35 0 0 25 0 1 0 420988062 27746304 6121 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6774 6121 603 41 0 6733 0
vsize: 27096
[startup+610.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6152 0 0 0 60963 35 0 0 25 0 1 0 420988062 27746304 6123 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6774 6123 603 41 0 6733 0
vsize: 27096
[startup+620.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6152 0 0 0 61963 35 0 0 25 0 1 0 420988062 27746304 6123 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6774 6123 603 41 0 6733 0
vsize: 27096
[startup+630.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6152 0 0 0 62963 35 0 0 25 0 1 0 420988062 27746304 6123 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6774 6123 603 41 0 6733 0
vsize: 27096
[startup+640.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6152 0 0 0 63964 35 0 0 25 0 1 0 420988062 27746304 6123 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6774 6123 603 41 0 6733 0
vsize: 27096
[startup+650.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6158 0 0 0 64964 35 0 0 25 0 1 0 420988062 27746304 6129 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6774 6129 603 41 0 6733 0
vsize: 27096
[startup+660.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6170 0 0 0 65964 35 0 0 25 0 1 0 420988062 27938816 6141 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6141 603 41 0 6780 0
vsize: 27284
[startup+670.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6182 0 0 0 66964 35 0 0 25 0 1 0 420988062 27938816 6153 4294967295 134512640 134672761 3221224640 3221223824 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6153 603 41 0 6780 0
vsize: 27284
[startup+680.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6183 0 0 0 67964 35 0 0 25 0 1 0 420988062 27938816 6154 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6154 603 41 0 6780 0
vsize: 27284
[startup+690.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6183 0 0 0 68965 35 0 0 25 0 1 0 420988062 27938816 6154 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6154 603 41 0 6780 0
vsize: 27284
[startup+700.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6184 0 0 0 69965 35 0 0 25 0 1 0 420988062 27938816 6155 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6155 603 41 0 6780 0
vsize: 27284
[startup+710.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6186 0 0 0 70965 35 0 0 25 0 1 0 420988062 27938816 6157 4294967295 134512640 134672761 3221224640 3221223808 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6157 603 41 0 6780 0
vsize: 27284
[startup+720.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6187 0 0 0 71965 35 0 0 25 0 1 0 420988062 27938816 6158 4294967295 134512640 134672761 3221224640 3221223744 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6158 603 41 0 6780 0
vsize: 27284
[startup+730.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6187 0 0 0 72965 35 0 0 25 0 1 0 420988062 27938816 6158 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6158 603 41 0 6780 0
vsize: 27284
[startup+740.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6187 0 0 0 73966 35 0 0 25 0 1 0 420988062 27938816 6158 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6158 603 41 0 6780 0
vsize: 27284
[startup+750.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6187 0 0 0 74966 35 0 0 25 0 1 0 420988062 27938816 6158 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6158 603 41 0 6780 0
vsize: 27284
[startup+760.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6187 0 0 0 75966 35 0 0 25 0 1 0 420988062 27938816 6158 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6158 603 41 0 6780 0
vsize: 27284
[startup+770.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6187 0 0 0 76966 35 0 0 25 0 1 0 420988062 27938816 6158 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6158 603 41 0 6780 0
vsize: 27284
[startup+780.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6187 0 0 0 77966 35 0 0 25 0 1 0 420988062 27938816 6158 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6158 603 41 0 6780 0
vsize: 27284
[startup+790.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6197 0 0 0 78966 35 0 0 25 0 1 0 420988062 27938816 6168 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6168 603 41 0 6780 0
vsize: 27284
[startup+800.043 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 79966 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223788 1074754724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+810.044 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 80966 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+820.044 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 81966 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+830.045 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 82966 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+840.045 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 83967 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223744 134555093 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+850.045 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 84967 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+860.046 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 85967 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+870.045 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 86967 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+880.045 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 87967 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+890.045 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 88968 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+900.045 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 89968 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+910.045 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 90968 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+920.045 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 91968 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+930.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6199 0 0 0 92968 35 0 0 25 0 1 0 420988062 27938816 6170 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6821 6170 603 41 0 6780 0
vsize: 27284
[startup+940.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6209 0 0 0 93968 35 0 0 25 0 1 0 420988062 28135424 6180 4294967295 134512640 134672761 3221224640 3221223808 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6180 603 41 0 6828 0
vsize: 27476
[startup+950.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6210 0 0 0 94969 35 0 0 25 0 1 0 420988062 28135424 6181 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6181 603 41 0 6828 0
vsize: 27476
[startup+960.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6210 0 0 0 95969 35 0 0 25 0 1 0 420988062 28135424 6181 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6181 603 41 0 6828 0
vsize: 27476
[startup+970.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6210 0 0 0 96969 35 0 0 25 0 1 0 420988062 28135424 6181 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6181 603 41 0 6828 0
vsize: 27476
[startup+980.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6210 0 0 0 97969 35 0 0 25 0 1 0 420988062 28135424 6181 4294967295 134512640 134672761 3221224640 3221223780 134542703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6181 603 41 0 6828 0
vsize: 27476
[startup+990.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6210 0 0 0 98969 35 0 0 25 0 1 0 420988062 28135424 6181 4294967295 134512640 134672761 3221224640 3221223784 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6181 603 41 0 6828 0
vsize: 27476
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6210 0 0 0 99970 35 0 0 25 0 1 0 420988062 28135424 6181 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6181 603 41 0 6828 0
vsize: 27476
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6210 0 0 0 100970 35 0 0 25 0 1 0 420988062 28135424 6181 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6181 603 41 0 6828 0
vsize: 27476
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6223 0 0 0 101970 35 0 0 25 0 1 0 420988062 28135424 6194 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6194 603 41 0 6828 0
vsize: 27476
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6226 0 0 0 102970 35 0 0 25 0 1 0 420988062 28135424 6197 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6197 603 41 0 6828 0
vsize: 27476
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6226 0 0 0 103970 35 0 0 25 0 1 0 420988062 28135424 6197 4294967295 134512640 134672761 3221224640 3221223808 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6197 603 41 0 6828 0
vsize: 27476
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6226 0 0 0 104970 35 0 0 25 0 1 0 420988062 28135424 6197 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6197 603 41 0 6828 0
vsize: 27476
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6226 0 0 0 105971 35 0 0 25 0 1 0 420988062 28135424 6197 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6197 603 41 0 6828 0
vsize: 27476
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6226 0 0 0 106971 35 0 0 25 0 1 0 420988062 28135424 6197 4294967295 134512640 134672761 3221224640 3221223812 134559060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6197 603 41 0 6828 0
vsize: 27476
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6226 0 0 0 107971 35 0 0 25 0 1 0 420988062 28135424 6197 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6197 603 41 0 6828 0
vsize: 27476
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6226 0 0 0 108971 35 0 0 25 0 1 0 420988062 28135424 6197 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6197 603 41 0 6828 0
vsize: 27476
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6820 0 0 0 109970 37 0 0 25 0 1 0 420988062 31432704 6791 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6791 603 41 0 7633 0
vsize: 30696
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6821 0 0 0 110970 37 0 0 25 0 1 0 420988062 31432704 6792 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6792 603 41 0 7633 0
vsize: 30696
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6821 0 0 0 111970 37 0 0 25 0 1 0 420988062 31432704 6792 4294967295 134512640 134672761 3221224640 3221223824 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6792 603 41 0 7633 0
vsize: 30696
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6821 0 0 0 112970 37 0 0 25 0 1 0 420988062 31432704 6792 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6792 603 41 0 7633 0
vsize: 30696
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6821 0 0 0 113971 37 0 0 25 0 1 0 420988062 31432704 6792 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6792 603 41 0 7633 0
vsize: 30696
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6821 0 0 0 114971 37 0 0 25 0 1 0 420988062 31432704 6792 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6792 603 41 0 7633 0
vsize: 30696
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6821 0 0 0 115971 37 0 0 25 0 1 0 420988062 31432704 6792 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6792 603 41 0 7633 0
vsize: 30696
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6821 0 0 0 116971 37 0 0 25 0 1 0 420988062 31432704 6792 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6792 603 41 0 7633 0
vsize: 30696
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6821 0 0 0 117971 37 0 0 25 0 1 0 420988062 31432704 6792 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6792 603 41 0 7633 0
vsize: 30696
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6821 0 0 0 118971 37 0 0 25 0 1 0 420988062 31432704 6792 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6792 603 41 0 7633 0
vsize: 30696
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 633
Raw data (stat): 633 (minisat+) R 632 30854 30853 0 -1 0 6821 0 0 0 119972 37 0 0 25 0 1 0 420988062 31432704 6792 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6792 603 41 0 7633 0
vsize: 30696
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 633
Raw data (stat): 633 (minisat+) Z 632 30854 30853 0 -1 12 6824 0 0 0 119972 38 0 0 25 0 1 0 420988062 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.07
CPU time (s): 1200.11
CPU user time (s): 1199.72
CPU system time (s): 0.386941
CPU usage (%): 100.004
Max. virtual memory (Kb): 30696
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####