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-1.opb
MD5SUM	16a8eb66aae2bcfd534a482dd0a3948e
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	27856
Number of constraints which are clauses	27856
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 6363

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-14 04:35:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4831 boxname=wulflinc7 idbench=319 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  16a8eb66aae2bcfd534a482dd0a3948e  /oldhome/oroussel/tmp/wulflinc7/normalized-frb35-17-1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc7/normalized-frb35-17-1.opb /oldhome/oroussel/tmp/wulflinc7/normalized-frb35-17-1.opb
IDLAUNCH: 4831
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        853784 kB
Buffers:         38176 kB
Cached:         122916 kB
SwapCached:          0 kB
Active:          73836 kB
Inactive:        90164 kB
HighTotal:      131008 kB
HighFree:         4284 kB
LowTotal:       903652 kB
LowFree:        849500 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11404 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:55:14 (client local time) WITH STATUS 10 IN 1200.13 SECONDS
stats: 4831 7 1200.13 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27856 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 |   27856    55712 |    9285       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -25[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 |   84761   188924 |   28253       0        0     nan |  0.000 % |
c |       100 |   84761   188924 |   31078     100      926     9.3 |  0.006 % |
c |       250 |   83634   186349 |   34186     221     1413     6.4 |  1.710 % |
c |       475 |   80933   180134 |   37604     355     2207     6.2 |  6.040 % |
c |       813 |   77409   172060 |   41365     588     3785     6.4 | 11.559 % |
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 |       882 |   76572   170159 |   25524     646     4060     6.3 | 11.559 % |
c |       982 |   76248   169418 |   28076     742     4907     6.6 | 13.294 % |
c |      1132 |   75475   167645 |   30884     876     5884     6.7 | 14.513 % |
c |      1357 |   73323   162694 |   33972    1053     7524     7.1 | 18.119 % |
c |      1694 |   69083   152875 |   37369    1223    10212     8.3 | 25.384 % |
c |      2200 |   64548   142369 |   41106    1552    13210     8.5 | 32.597 % |
c |      2959 |   56360   123262 |   45217    1947    17611     9.0 | 46.490 % |
c |      4098 |   49200   106477 |   49739    2692    28019    10.4 | 58.967 % |
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 |      4161 |   49289   106739 |   16429    2744    28691    10.5 | 58.967 % |
c |      4262 |   48935   105921 |   18071    2789    29429    10.6 | 59.635 % |
c |      4412 |   48112   103990 |   19879    2876    29925    10.4 | 61.106 % |
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 |      4461 |   47968   103651 |   15989    2912    30201    10.4 | 61.106 % |
c |      4561 |   47684   102981 |   17587    2967    31426    10.6 | 61.861 % |
c |      4711 |   46346    99868 |   19346    3046    32263    10.6 | 64.186 % |
c |      4936 |   45722    98411 |   21281    3162    35929    11.4 | 65.281 % |
c |      5273 |   43815    93936 |   23409    3346    37840    11.3 | 68.630 % |
c |      5779 |   43112    92271 |   25750    3784    48755    12.9 | 69.849 % |
c |      6539 |   41802    89200 |   28325    4347    59496    13.7 | 72.153 % |
c |      7678 |   40239    85515 |   31158    5142    78057    15.2 | 74.992 % |
c |      9387 |   38157    80627 |   34273    6289   115049    18.3 | 78.757 % |
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 |      9858 |   37798    79788 |   12599    6531   119747    18.3 | 78.757 % |
c |      9958 |   37726    79617 |   13858    6604   121765    18.4 | 79.634 % |
c |     10108 |   37643    79425 |   15244    6724   126513    18.8 | 79.773 % |
c |     10333 |   37643    79425 |   16769    6949   134036    19.3 | 79.773 % |
c |     10670 |   36907    77684 |   18446    6904   136475    19.8 | 81.093 % |
c |     11176 |   36835    77516 |   20290    7393   153999    20.8 | 81.211 % |
c |     11935 |   35953    75441 |   22319    7624   166763    21.9 | 82.778 % |
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 |     12588 |   35739    74894 |   11913    8170   207554    25.4 | 82.778 % |
c |     12688 |   35739    74894 |   13104    8270   208584    25.2 | 83.170 % |
c |     12838 |   35739    74894 |   14414    8420   218670    26.0 | 83.170 % |
c |     13063 |   35707    74819 |   15856    8610   225982    26.2 | 83.226 % |
c |     13401 |   35618    74611 |   17441    8885   237778    26.8 | 83.386 % |
c |     13908 |   35560    74475 |   19186    9358   264892    28.3 | 83.488 % |
c |     14667 |   35560    74475 |   21104   10117   308099    30.5 | 83.488 % |
c |     15806 |   35560    74475 |   23215   11256   362675    32.2 | 83.488 % |
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 |     16630 |   35623    74634 |   11874   12080   410133    34.0 | 83.488 % |
c |     16731 |   35623    74634 |   13061   12181   413895    34.0 | 83.461 % |
c |     16881 |   35399    74102 |   14367   12096   411608    34.0 | 83.870 % |
c |     17108 |   35399    74102 |   15804   12323   420199    34.1 | 83.870 % |
c |     17445 |   35224    73688 |   17384   12478   434634    34.8 | 84.203 % |
c |     17951 |   35224    73688 |   19123   12984   457545    35.2 | 84.203 % |
c |     18710 |   35206    73646 |   21035   13681   487715    35.6 | 84.233 % |
c |     19850 |   35206    73646 |   23139   14821   580299    39.2 | 84.233 % |
c |     21558 |   35043    73263 |   25452   16275   660769    40.6 | 84.540 % |
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 |     23421 |   34951    73040 |   11650   18057   748344    41.4 | 84.540 % |
c |     23521 |   34951    73040 |   12815   18157   752443    41.4 | 84.695 % |
c |     23671 |   34951    73040 |   14096   18307   760640    41.5 | 84.695 % |
c |     23896 |   34951    73040 |   15506   18532   772530    41.7 | 84.695 % |
c |     24233 |   34951    73040 |   17056   18869   786845    41.7 | 84.695 % |
c |     24739 |   34879    72868 |   18762   19340   808939    41.8 | 84.833 % |
c |     25499 |   34821    72731 |   20638   19978   845346    42.3 | 84.941 % |
c |     26638 |   34821    72731 |   22702   21117   905157    42.9 | 84.941 % |
c |     28346 |   34789    72655 |   24972   22751   987687    43.4 | 85.002 % |
c |     30908 |   34645    72317 |   27470   24983  1142123    45.7 | 85.242 % |
c |     34752 |   34645    72317 |   30217   28827  1311031    45.5 | 85.242 % |
c |     40519 |   34637    72298 |   33238   34588  1629004    47.1 | 85.258 % |
c |     49168 |   34637    72298 |   36562   43237  2269074    52.5 | 85.258 % |
c |     62142 |   34573    72148 |   40218   20265   742174    36.6 | 85.370 % |
c |     81603 |   34535    72058 |   44240   39681  1558930    39.3 | 85.442 % |
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 |    101139 |   34529    72044 |   11509   58501  2189828    37.4 | 85.442 % |
c |    101240 |   34529    72044 |   12659   17731   491164    27.7 | 85.487 % |
c |    101390 |   34529    72044 |   13925   17881   495473    27.7 | 85.487 % |
c |    101615 |   34529    72044 |   15318   18106   500510    27.6 | 85.487 % |
c |    101953 |   34529    72044 |   16850   18444   514504    27.9 | 85.487 % |
c |    102459 |   34529    72044 |   18535   18950   534744    28.2 | 85.487 % |
c |    103218 |   34425    71802 |   20388   19640   572395    29.1 | 85.671 % |
c |    104357 |   34425    71802 |   22427   20779   628325    30.2 | 85.671 % |
c |    106065 |   34425    71802 |   24670   22487   709934    31.6 | 85.671 % |
c |    108628 |   34346    71617 |   27137   25036   811728    32.4 | 85.808 % |
c |    112472 |   34328    71575 |   29851   28874   987130    34.2 | 85.839 % |
c |    118238 |   34322    71561 |   32836   34639  1283641    37.1 | 85.849 % |
c |    126888 |   34322    71561 |   36120   43289  1643232    38.0 | 85.849 % |
c |    139862 |   34251    71389 |   39732   19773   584205    29.5 | 85.982 % |
c |    159324 |   34251    71389 |   43705   39235  1210050    30.8 | 85.982 % |
c |    188516 |   34245    71375 |   48075   27450   799838    29.1 | 85.992 % |
c |    232305 |   34231    71342 |   52883   23024  1220731    53.0 | 86.018 % |
c |    297989 |   34209    71290 |   58171   36017  2069080    57.4 | 86.059 % |
c |    396515 |   34090    71010 |   63989   24664   626640    25.4 | 86.278 % |
c |    544304 |   33918    70562 |   70387   50468  1465252    29.0 | 86.610 % |
#### 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.91 0.93 0.90 2/54 29522
Raw data (stat): 29522 (runsolver) R 29521 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423536077 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0002 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 2412 0 0 0 992 6 0 0 25 0 1 0 423536077 12300288 2383 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3003 2383 603 41 0 2962 0
vsize: 12012
[startup+19.9998 s]
Raw data (loadavg): 0.93 0.93 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 2426 0 0 0 1991 7 0 0 25 0 1 0 423536077 12300288 2397 4294967295 134512640 134672761 3221224560 3221223776 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3003 2397 603 41 0 2962 0
vsize: 12012
[startup+30.0009 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 2860 0 0 0 2990 8 0 0 25 0 1 0 423536077 14049280 2831 4294967295 134512640 134672761 3221224560 3221223744 134559467 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3430 2831 603 41 0 3389 0
vsize: 13720
[startup+40.0011 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 3354 0 0 0 3988 10 0 0 25 0 1 0 423536077 16236544 3325 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3964 3325 603 41 0 3923 0
vsize: 15856
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 3763 0 0 0 4986 12 0 0 25 0 1 0 423536077 17846272 3734 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4357 3734 603 41 0 4316 0
vsize: 17428
[startup+60.0018 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 4154 0 0 0 5984 14 0 0 25 0 1 0 423536077 19578880 4125 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4780 4125 603 41 0 4739 0
vsize: 19120
[startup+70.0019 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 4583 0 0 0 6982 15 0 0 25 0 1 0 423536077 21315584 4554 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5204 4554 603 41 0 5163 0
vsize: 20816
[startup+80.0026 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 4998 0 0 0 7981 17 0 0 25 0 1 0 423536077 23064576 4969 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5631 4969 603 41 0 5590 0
vsize: 22524
[startup+90.0027 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5278 0 0 0 8979 18 0 0 25 0 1 0 423536077 24133632 5249 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5892 5249 603 41 0 5851 0
vsize: 23568
[startup+100.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5533 0 0 0 9978 19 0 0 25 0 1 0 423536077 25194496 5504 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6151 5504 603 41 0 6110 0
vsize: 24604
[startup+110.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5581 0 0 0 10978 20 0 0 25 0 1 0 423536077 25325568 5552 4294967295 134512640 134672761 3221224560 3221223664 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6183 5552 603 41 0 6142 0
vsize: 24732
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5581 0 0 0 11977 20 0 0 25 0 1 0 423536077 25325568 5552 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6183 5552 603 41 0 6142 0
vsize: 24732
[startup+130.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5581 0 0 0 12977 20 0 0 25 0 1 0 423536077 25325568 5552 4294967295 134512640 134672761 3221224560 3221223664 134555333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6183 5552 603 41 0 6142 0
vsize: 24732
[startup+140.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5581 0 0 0 13976 22 0 0 25 0 1 0 423536077 25325568 5552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6183 5552 603 41 0 6142 0
vsize: 24732
[startup+150.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5581 0 0 0 14976 22 0 0 25 0 1 0 423536077 25325568 5552 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6183 5552 603 41 0 6142 0
vsize: 24732
[startup+160.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5581 0 0 0 15976 22 0 0 25 0 1 0 423536077 25325568 5552 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6183 5552 603 41 0 6142 0
vsize: 24732
[startup+170.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5587 0 0 0 16975 22 0 0 25 0 1 0 423536077 25468928 5558 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6218 5558 603 41 0 6177 0
vsize: 24872
[startup+180.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5600 0 0 0 17975 22 0 0 25 0 1 0 423536077 25468928 5571 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6218 5571 603 41 0 6177 0
vsize: 24872
[startup+190.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5609 0 0 0 18974 23 0 0 25 0 1 0 423536077 25468928 5580 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6218 5580 603 41 0 6177 0
vsize: 24872
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5609 0 0 0 19974 23 0 0 25 0 1 0 423536077 25468928 5580 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6218 5580 603 41 0 6177 0
vsize: 24872
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5614 0 0 0 20974 23 0 0 25 0 1 0 423536077 25616384 5585 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5585 603 41 0 6213 0
vsize: 25016
[startup+220.006 s]
Raw data (loadavg): 1.07 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5614 0 0 0 21974 23 0 0 25 0 1 0 423536077 25616384 5585 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5585 603 41 0 6213 0
vsize: 25016
[startup+230.007 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5615 0 0 0 22973 24 0 0 25 0 1 0 423536077 25616384 5586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5586 603 41 0 6213 0
vsize: 25016
[startup+240.007 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5615 0 0 0 23973 24 0 0 25 0 1 0 423536077 25616384 5586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5586 603 41 0 6213 0
vsize: 25016
[startup+250.007 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5615 0 0 0 24973 24 0 0 25 0 1 0 423536077 25616384 5586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5586 603 41 0 6213 0
vsize: 25016
[startup+260.008 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5615 0 0 0 25973 24 0 0 25 0 1 0 423536077 25616384 5586 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5586 603 41 0 6213 0
vsize: 25016
[startup+270.008 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5615 0 0 0 26972 24 0 0 25 0 1 0 423536077 25616384 5586 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5586 603 41 0 6213 0
vsize: 25016
[startup+280.008 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5615 0 0 0 27972 25 0 0 25 0 1 0 423536077 25616384 5586 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5586 603 41 0 6213 0
vsize: 25016
[startup+290.009 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5615 0 0 0 28972 25 0 0 25 0 1 0 423536077 25616384 5586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5586 603 41 0 6213 0
vsize: 25016
[startup+300.01 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5615 0 0 0 29971 25 0 0 25 0 1 0 423536077 25616384 5586 4294967295 134512640 134672761 3221224560 3221223744 134559176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5586 603 41 0 6213 0
vsize: 25016
[startup+310.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5615 0 0 0 30971 25 0 0 25 0 1 0 423536077 25616384 5586 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5586 603 41 0 6213 0
vsize: 25016
[startup+320.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5615 0 0 0 31971 26 0 0 25 0 1 0 423536077 25616384 5586 4294967295 134512640 134672761 3221224560 3221223696 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5586 603 41 0 6213 0
vsize: 25016
[startup+330.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5618 0 0 0 32971 26 0 0 25 0 1 0 423536077 25616384 5589 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5589 603 41 0 6213 0
vsize: 25016
[startup+340.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5618 0 0 0 33970 27 0 0 25 0 1 0 423536077 25616384 5589 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5589 603 41 0 6213 0
vsize: 25016
[startup+350.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5618 0 0 0 34969 27 0 0 25 0 1 0 423536077 25616384 5589 4294967295 134512640 134672761 3221224560 3221223664 134560134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5589 603 41 0 6213 0
vsize: 25016
[startup+360.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5618 0 0 0 35969 27 0 0 25 0 1 0 423536077 25616384 5589 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5589 603 41 0 6213 0
vsize: 25016
[startup+370.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5618 0 0 0 36969 28 0 0 25 0 1 0 423536077 25616384 5589 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5589 603 41 0 6213 0
vsize: 25016
[startup+380.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5619 0 0 0 37969 28 0 0 25 0 1 0 423536077 25616384 5590 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6254 5590 603 41 0 6213 0
vsize: 25016
[startup+390.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5657 0 0 0 38968 28 0 0 25 0 1 0 423536077 25747456 5628 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6286 5628 603 41 0 6245 0
vsize: 25144
[startup+400.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 5929 0 0 0 39967 30 0 0 25 0 1 0 423536077 26812416 5900 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6546 5900 603 41 0 6505 0
vsize: 26184
[startup+410.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 6246 0 0 0 40966 31 0 0 25 0 1 0 423536077 28151808 6217 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6873 6217 603 41 0 6832 0
vsize: 27492
[startup+420.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 6496 0 0 0 41965 32 0 0 25 0 1 0 423536077 29343744 6467 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7164 6467 603 41 0 7123 0
vsize: 28656
[startup+430.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 6503 0 0 0 42965 32 0 0 25 0 1 0 423536077 29503488 6474 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7203 6474 603 41 0 7162 0
vsize: 28812
[startup+440.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 6507 0 0 0 43965 32 0 0 25 0 1 0 423536077 29503488 6478 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7203 6478 603 41 0 7162 0
vsize: 28812
[startup+450.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 6513 0 0 0 44965 32 0 0 25 0 1 0 423536077 29503488 6484 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7203 6484 603 41 0 7162 0
vsize: 28812
[startup+460.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 6513 0 0 0 45966 32 0 0 25 0 1 0 423536077 29503488 6484 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7203 6484 603 41 0 7162 0
vsize: 28812
[startup+470.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 6513 0 0 0 46966 32 0 0 25 0 1 0 423536077 29503488 6484 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7203 6484 603 41 0 7162 0
vsize: 28812
[startup+480.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 6518 0 0 0 47966 32 0 0 25 0 1 0 423536077 29503488 6489 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7203 6489 603 41 0 7162 0
vsize: 28812
[startup+490.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 6527 0 0 0 48966 32 0 0 25 0 1 0 423536077 29503488 6498 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7203 6498 603 41 0 7162 0
vsize: 28812
[startup+500.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 6764 0 0 0 49966 32 0 0 25 0 1 0 423536077 30576640 6735 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7465 6735 603 41 0 7424 0
vsize: 29860
[startup+510.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7012 0 0 0 50965 33 0 0 25 0 1 0 423536077 31514624 6983 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7694 6983 603 41 0 7653 0
vsize: 30776
[startup+520.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7257 0 0 0 51965 34 0 0 25 0 1 0 423536077 32591872 7228 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7957 7228 603 41 0 7916 0
vsize: 31828
[startup+530.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7484 0 0 0 52965 34 0 0 25 0 1 0 423536077 33529856 7455 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8186 7455 603 41 0 8145 0
vsize: 32744
[startup+540.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7569 0 0 0 53965 34 0 0 25 0 1 0 423536077 33792000 7540 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7540 603 41 0 8209 0
vsize: 33000
[startup+550.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7569 0 0 0 54965 34 0 0 25 0 1 0 423536077 33792000 7540 4294967295 134512640 134672761 3221224560 3221223560 1075349905 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7540 603 41 0 8209 0
vsize: 33000
[startup+560.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7569 0 0 0 55965 34 0 0 25 0 1 0 423536077 33792000 7540 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7540 603 41 0 8209 0
vsize: 33000
[startup+570.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7569 0 0 0 56964 35 0 0 25 0 1 0 423536077 33792000 7540 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8250 7540 603 41 0 8209 0
vsize: 33000
[startup+580.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7569 0 0 0 57964 35 0 0 25 0 1 0 423536077 33792000 7540 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7540 603 41 0 8209 0
vsize: 33000
[startup+590.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7569 0 0 0 58964 35 0 0 25 0 1 0 423536077 33792000 7540 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7540 603 41 0 8209 0
vsize: 33000
[startup+600.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7569 0 0 0 59964 35 0 0 25 0 1 0 423536077 33792000 7540 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7540 603 41 0 8209 0
vsize: 33000
[startup+610.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7569 0 0 0 60965 35 0 0 25 0 1 0 423536077 33792000 7540 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7540 603 41 0 8209 0
vsize: 33000
[startup+620.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7569 0 0 0 61965 35 0 0 25 0 1 0 423536077 33792000 7540 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7540 603 41 0 8209 0
vsize: 33000
[startup+630.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7569 0 0 0 62965 35 0 0 25 0 1 0 423536077 33792000 7540 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7540 603 41 0 8209 0
vsize: 33000
[startup+640.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7576 0 0 0 63965 35 0 0 25 0 1 0 423536077 33792000 7547 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7547 603 41 0 8209 0
vsize: 33000
[startup+650.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7586 0 0 0 64965 35 0 0 25 0 1 0 423536077 33935360 7557 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7557 603 41 0 8244 0
vsize: 33140
[startup+660.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7586 0 0 0 65965 35 0 0 25 0 1 0 423536077 33935360 7557 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7557 603 41 0 8244 0
vsize: 33140
[startup+670.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7586 0 0 0 66966 35 0 0 25 0 1 0 423536077 33935360 7557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7557 603 41 0 8244 0
vsize: 33140
[startup+680.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7586 0 0 0 67966 35 0 0 25 0 1 0 423536077 33935360 7557 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7557 603 41 0 8244 0
vsize: 33140
[startup+690.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7586 0 0 0 68966 35 0 0 25 0 1 0 423536077 33935360 7557 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7557 603 41 0 8244 0
vsize: 33140
[startup+700.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7602 0 0 0 69966 35 0 0 25 0 1 0 423536077 33935360 7573 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7573 603 41 0 8244 0
vsize: 33140
[startup+710.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7605 0 0 0 70967 35 0 0 25 0 1 0 423536077 33935360 7576 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7576 603 41 0 8244 0
vsize: 33140
[startup+720.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7607 0 0 0 71967 35 0 0 25 0 1 0 423536077 33935360 7578 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7578 603 41 0 8244 0
vsize: 33140
[startup+730.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7608 0 0 0 72967 35 0 0 25 0 1 0 423536077 33935360 7579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7579 603 41 0 8244 0
vsize: 33140
[startup+740.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7608 0 0 0 73967 35 0 0 25 0 1 0 423536077 33935360 7579 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7579 603 41 0 8244 0
vsize: 33140
[startup+750.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7608 0 0 0 74967 35 0 0 25 0 1 0 423536077 33935360 7579 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7579 603 41 0 8244 0
vsize: 33140
[startup+760.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7619 0 0 0 75968 35 0 0 25 0 1 0 423536077 34131968 7590 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7590 603 41 0 8292 0
vsize: 33332
[startup+770.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7619 0 0 0 76968 35 0 0 25 0 1 0 423536077 34131968 7590 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8333 7590 603 41 0 8292 0
vsize: 33332
[startup+780.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7619 0 0 0 77967 35 0 0 25 0 1 0 423536077 34131968 7590 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7590 603 41 0 8292 0
vsize: 33332
[startup+790.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7628 0 0 0 78967 35 0 0 25 0 1 0 423536077 34131968 7599 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7599 603 41 0 8292 0
vsize: 33332
[startup+800.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7628 0 0 0 79967 35 0 0 25 0 1 0 423536077 34131968 7599 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7599 603 41 0 8292 0
vsize: 33332
[startup+810.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7628 0 0 0 80967 35 0 0 25 0 1 0 423536077 34131968 7599 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7599 603 41 0 8292 0
vsize: 33332
[startup+820.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7628 0 0 0 81968 35 0 0 25 0 1 0 423536077 34131968 7599 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7599 603 41 0 8292 0
vsize: 33332
[startup+830.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7628 0 0 0 82968 35 0 0 25 0 1 0 423536077 34131968 7599 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7599 603 41 0 8292 0
vsize: 33332
[startup+840.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7628 0 0 0 83968 35 0 0 25 0 1 0 423536077 34131968 7599 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7599 603 41 0 8292 0
vsize: 33332
[startup+850.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7628 0 0 0 84968 35 0 0 25 0 1 0 423536077 34131968 7599 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7599 603 41 0 8292 0
vsize: 33332
[startup+860.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7628 0 0 0 85968 35 0 0 25 0 1 0 423536077 34131968 7599 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7599 603 41 0 8292 0
vsize: 33332
[startup+870.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7628 0 0 0 86969 35 0 0 25 0 1 0 423536077 34131968 7599 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7599 603 41 0 8292 0
vsize: 33332
[startup+880.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7641 0 0 0 87969 35 0 0 25 0 1 0 423536077 34131968 7612 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7612 603 41 0 8292 0
vsize: 33332
[startup+890.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7644 0 0 0 88969 35 0 0 25 0 1 0 423536077 34131968 7615 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7615 603 41 0 8292 0
vsize: 33332
[startup+900.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7644 0 0 0 89969 35 0 0 25 0 1 0 423536077 34131968 7615 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7615 603 41 0 8292 0
vsize: 33332
[startup+910.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7644 0 0 0 90969 35 0 0 25 0 1 0 423536077 34131968 7615 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7615 603 41 0 8292 0
vsize: 33332
[startup+920.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7644 0 0 0 91970 35 0 0 25 0 1 0 423536077 34131968 7615 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7615 603 41 0 8292 0
vsize: 33332
[startup+930.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7654 0 0 0 92970 35 0 0 25 0 1 0 423536077 34328576 7625 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7625 603 41 0 8340 0
vsize: 33524
[startup+940.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7655 0 0 0 93970 35 0 0 25 0 1 0 423536077 34328576 7626 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7626 603 41 0 8340 0
vsize: 33524
[startup+950.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7655 0 0 0 94970 35 0 0 25 0 1 0 423536077 34328576 7626 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7626 603 41 0 8340 0
vsize: 33524
[startup+960.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7655 0 0 0 95970 35 0 0 25 0 1 0 423536077 34328576 7626 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7626 603 41 0 8340 0
vsize: 33524
[startup+970.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7655 0 0 0 96971 35 0 0 25 0 1 0 423536077 34328576 7626 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7626 603 41 0 8340 0
vsize: 33524
[startup+980.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7667 0 0 0 97971 35 0 0 25 0 1 0 423536077 34328576 7638 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7638 603 41 0 8340 0
vsize: 33524
[startup+990.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7667 0 0 0 98971 35 0 0 25 0 1 0 423536077 34328576 7638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7638 603 41 0 8340 0
vsize: 33524
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7682 0 0 0 99971 35 0 0 25 0 1 0 423536077 34328576 7653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7653 603 41 0 8340 0
vsize: 33524
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7684 0 0 0 100971 35 0 0 25 0 1 0 423536077 34328576 7655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7655 603 41 0 8340 0
vsize: 33524
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7684 0 0 0 101972 35 0 0 25 0 1 0 423536077 34328576 7655 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7655 603 41 0 8340 0
vsize: 33524
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7684 0 0 0 102972 35 0 0 25 0 1 0 423536077 34328576 7655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7655 603 41 0 8340 0
vsize: 33524
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7684 0 0 0 103972 35 0 0 25 0 1 0 423536077 34328576 7655 4294967295 134512640 134672761 3221224560 3221223696 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7655 603 41 0 8340 0
vsize: 33524
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7684 0 0 0 104972 35 0 0 25 0 1 0 423536077 34328576 7655 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7655 603 41 0 8340 0
vsize: 33524
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7696 0 0 0 105973 35 0 0 25 0 1 0 423536077 34525184 7667 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7667 603 41 0 8388 0
vsize: 33716
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7699 0 0 0 106973 35 0 0 25 0 1 0 423536077 34525184 7670 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7670 603 41 0 8388 0
vsize: 33716
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7700 0 0 0 107972 35 0 0 25 0 1 0 423536077 34525184 7671 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7671 603 41 0 8388 0
vsize: 33716
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7700 0 0 0 108972 35 0 0 25 0 1 0 423536077 34525184 7671 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7671 603 41 0 8388 0
vsize: 33716
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7712 0 0 0 109972 36 0 0 25 0 1 0 423536077 34525184 7683 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7683 603 41 0 8388 0
vsize: 33716
[startup+1110.03 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7712 0 0 0 110973 36 0 0 25 0 1 0 423536077 34525184 7683 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7683 603 41 0 8388 0
vsize: 33716
[startup+1120.03 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7712 0 0 0 111973 36 0 0 25 0 1 0 423536077 34525184 7683 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7683 603 41 0 8388 0
vsize: 33716
[startup+1130.03 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7730 0 0 0 112973 36 0 0 25 0 1 0 423536077 34721792 7701 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8477 7701 603 41 0 8436 0
vsize: 33908
[startup+1140.03 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7733 0 0 0 113973 36 0 0 25 0 1 0 423536077 34721792 7704 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8477 7704 603 41 0 8436 0
vsize: 33908
[startup+1150.03 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7736 0 0 0 114973 36 0 0 25 0 1 0 423536077 34721792 7707 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8477 7707 603 41 0 8436 0
vsize: 33908
[startup+1160.03 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7737 0 0 0 115974 36 0 0 25 0 1 0 423536077 34721792 7708 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8477 7708 603 41 0 8436 0
vsize: 33908
[startup+1170.03 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7737 0 0 0 116974 36 0 0 25 0 1 0 423536077 34721792 7708 4294967295 134512640 134672761 3221224560 3221223696 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8477 7708 603 41 0 8436 0
vsize: 33908
[startup+1180.03 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7737 0 0 0 117974 36 0 0 25 0 1 0 423536077 34721792 7708 4294967295 134512640 134672761 3221224560 3221223744 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8477 7708 603 41 0 8436 0
vsize: 33908
[startup+1190.03 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7737 0 0 0 118974 36 0 0 25 0 1 0 423536077 34721792 7708 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8477 7708 603 41 0 8436 0
vsize: 33908
[startup+1200.03 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 29522
Raw data (stat): 29522 (minisat+) R 29521 22932 22931 0 -1 0 7737 0 0 0 119974 36 0 0 25 0 1 0 423536077 34721792 7708 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8477 7708 603 41 0 8436 0
vsize: 33908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.02 0.99 0.92 1/54 29522
Raw data (stat): 29522 (minisat+) Z 29521 22932 22931 0 -1 12 7740 0 0 0 119974 37 0 0 25 0 1 0 423536077 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.05
CPU time (s): 1200.13
CPU user time (s): 1199.75
CPU system time (s): 0.376942
CPU usage (%): 100.007
Max. virtual memory (Kb): 33908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####