PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 00:52:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19486 boxname=wulflinc28 idbench=1499 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f88781e3d6e9a5487d13eaa213c27b55  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-markshare1_1.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-markshare1_1.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-markshare1_1.opb
IDLAUNCH: 19486
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        432760 kB
Buffers:         33976 kB
Cached:         534476 kB
SwapCached:        164 kB
Active:         276436 kB
Inactive:       294476 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        432508 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6088 kB
Slab:            25344 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 01:12:07 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 19486 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[  10]---> BDD-cost:75459
c ---[   8]---> BDD-cost:72163
c ---[   6]---> BDD-cost:75517
c ---[   4]---> BDD-cost:34784
c ---[   2]---> BDD-cost:54075
c ---[   0]---> BDD-cost:51809
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1034848  3002025 |  344949       0        0     nan |  0.000 % |
c |       100 | 1034848  3002025 |  379443     100    12853   128.5 |  0.006 % |
c ==============================================================================
c [1mFound solution: 751001[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       103 | 1038541  3010654 |  346180     103    12951   125.7 |  0.006 % |
c ==============================================================================
c [1mFound solution: 745673[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       186 | 1038567  3010767 |  346189     186    15313    82.3 |  0.006 % |
c |       287 | 1038567  3010767 |  380807     287    53907   187.8 |  0.007 % |
c |       437 | 1038567  3010767 |  418888     437    64914   148.5 |  0.007 % |
c ==============================================================================
c [1mFound solution: 702847[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       451 | 1038586  3010821 |  346195     451    65310   144.8 |  0.007 % |
c |       552 | 1038586  3010821 |  380814     552    70766   128.2 |  0.007 % |
c |       702 | 1038586  3010821 |  418895     702    78066   111.2 |  0.007 % |
c ==============================================================================
c [1mFound solution: 702091[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       827 | 1038603  3010862 |  346201     827    84307   101.9 |  0.007 % |
c |       928 | 1038603  3010862 |  380821     928    88870    95.8 |  0.007 % |
c |      1078 | 1038603  3010862 |  418903    1078   105260    97.6 |  0.007 % |
c ==============================================================================
c [1mFound solution: 701945[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1276 | 1038617  3010899 |  346205    1276   114089    89.4 |  0.007 % |
c |      1378 | 1038617  3010899 |  380825    1378   192833   139.9 |  0.008 % |
c |      1528 | 1038617  3010899 |  418908    1528   200991   131.5 |  0.008 % |
c |      1753 | 1038617  3010899 |  460798    1753   212581   121.3 |  0.008 % |
c ==============================================================================
c [1mFound solution: 701908[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1876 | 1038651  3010987 |  346217    1876   218937   116.7 |  0.008 % |
c |      1978 | 1038651  3010987 |  380838    1978   232402   117.5 |  0.008 % |
c |      2128 | 1038651  3010987 |  418922    2128   241211   113.4 |  0.008 % |
c |      2353 | 1038651  3010987 |  460814    2353   253387   107.7 |  0.008 % |
c ==============================================================================
c [1mFound solution: 695987[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2628 | 1038666  3011026 |  346222    2628   266325   101.3 |  0.008 % |
c |      2728 | 1038666  3011026 |  380844    2728   402601   147.6 |  0.008 % |
c |      2880 | 1038666  3011026 |  418928    2880   423602   147.1 |  0.008 % |
c |      3105 | 1038666  3011026 |  460821    3105   435615   140.3 |  0.008 % |
c |      3444 | 1038666  3011026 |  506903    3444   451420   131.1 |  0.008 % |
c |      3950 | 1038666  3011026 |  557593    3950   477904   121.0 |  0.008 % |
c |      4711 | 1038666  3011026 |  613353    4711   642378   136.4 |  0.008 % |
c ==============================================================================
c [1mFound solution: 692033[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4986 | 1038684  3011070 |  346228    4986   658724   132.1 |  0.008 % |
c |      5086 | 1038684  3011070 |  380850    5086   664639   130.7 |  0.009 % |
c |      5236 | 1038684  3011070 |  418935    5236   671657   128.3 |  0.009 % |
c |      5462 | 1038684  3011070 |  460829    5462   685296   125.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 691909[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5613 | 1038703  3011116 |  346234    5613   693471   123.5 |  0.009 % |
c |      5713 | 1038703  3011116 |  380857    5713   785010   137.4 |  0.009 % |
c |      5865 | 1038703  3011116 |  418943    5865   791510   135.0 |  0.009 % |
c |      6090 | 1038703  3011116 |  460837    6090  1304054   214.1 |  0.009 % |
c |      6429 | 1038703  3011116 |  506921    6429  1399189   217.6 |  0.009 % |
c |      6935 | 1038703  3011116 |  557613    6935  1628471   234.8 |  0.009 % |
c ==============================================================================
c [1mFound solution: 688482[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7023 | 1038723  3011163 |  346241    7023  1632430   232.4 |  0.009 % |
c ==============================================================================
c [1mFound solution: 683776[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7057 | 1038741  3011207 |  346247    7057  1634867   231.7 |  0.009 % |
c |      7157 | 1038741  3011207 |  380871    7157  1640282   229.2 |  0.009 % |
c |      7307 | 1038741  3011207 |  418958    7307  1649677   225.8 |  0.009 % |
c |      7533 | 1038741  3011207 |  460854    7533  1660838   220.5 |  0.009 % |
c |      7873 | 1038741  3011207 |  506940    7873  1678428   213.2 |  0.009 % |
c |      8379 | 1038741  3011207 |  557634    8379  1709092   204.0 |  0.009 % |
c |      9138 | 1038741  3011207 |  613397    9138  1746778   191.2 |  0.009 % |
c ==============================================================================
c [1mFound solution: 681919[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9275 | 1038755  3011243 |  346251    9275  1752757   189.0 |  0.009 % |
c |      9377 | 1038755  3011243 |  380876    9377  1807482   192.8 |  0.010 % |
c |      9527 | 1038755  3011243 |  418963    9527  1816257   190.6 |  0.010 % |
c |      9752 | 1038755  3011243 |  460860    9752  1839487   188.6 |  0.010 % |
c |     10089 | 1038755  3011243 |  506946   10089  1853654   183.7 |  0.010 % |
c |     10595 | 1038755  3011243 |  557640   10595  1929881   182.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 681733[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10781 | 1038768  3011275 |  346256   10781  1936965   179.7 |  0.010 % |
c |     10884 | 1038768  3011275 |  380881   10884  2058947   189.2 |  0.010 % |
c ==============================================================================
c [1mFound solution: 677080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10906 | 1038787  3011321 |  346262   10906  2060382   188.9 |  0.010 % |
c |     11006 | 1038787  3011321 |  380888   11006  2065394   187.7 |  0.010 % |
c |     11156 | 1038787  3011321 |  418977   11156  2073808   185.9 |  0.010 % |
c |     11383 | 1038787  3011321 |  460874   11383  2095873   184.1 |  0.010 % |
c ==============================================================================
c [1mFound solution: 652289[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11484 | 1038807  3011372 |  346269   11484  2100932   182.9 |  0.010 % |
c |     11586 | 1038807  3011372 |  380895   11586  2107249   181.9 |  0.011 % |
c |     11737 | 1038807  3011372 |  418985   11737  2116318   180.3 |  0.011 % |
c |     11965 | 1038807  3011372 |  460884   11965  2127617   177.8 |  0.011 % |
c |     12302 | 1038807  3011372 |  506972   12302  2145408   174.4 |  0.011 % |
c |     12812 | 1038807  3011372 |  557669   12812  2172932   169.6 |  0.011 % |
c |     13571 | 1038807  3011372 |  613436   13571  2216930   163.4 |  0.011 % |
c ==============================================================================
c [1mFound solution: 540468[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13947 | 1038819  3011406 |  346273   13947  2235137   160.3 |  0.011 % |
c |     14048 | 1038819  3011406 |  380900   14048  2279828   162.3 |  0.011 % |
c |     14199 | 1038819  3011406 |  418990   14199  2289976   161.3 |  0.011 % |
c |     14425 | 1038819  3011406 |  460889   14425  2303417   159.7 |  0.011 % |
c |     14763 | 1038819  3011406 |  506978   14763  2321219   157.2 |  0.011 % |
c |     15270 | 1038819  3011406 |  557676   15270  2339491   153.2 |  0.011 % |
c |     16029 | 1038819  3011406 |  613443   16029  2441734   152.3 |  0.011 % |
c ==============================================================================
c [1mFound solution: 504535[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16694 | 1038839  3011457 |  346279   16694  2477770   148.4 |  0.011 % |
c |     16794 | 1038839  3011457 |  380906   16794  2481379   147.8 |  0.011 % |
c |     16945 | 1038839  3011457 |  418997   16945  2489945   146.9 |  0.011 % |
c |     17172 | 1038791  3011361 |  460897   17171  2508995   146.1 |  0.017 % |
c |     17510 | 1038791  3011361 |  506987   17509  2526924   144.3 |  0.017 % |
c |     18018 | 1038791  3011361 |  557685   18017  2552123   141.7 |  0.017 % |
c ==============================================================================
c [1mFound solution: 504326[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18739 | 1038812  3011411 |  346270   18738  2585840   138.0 |  0.017 % |
c |     18843 | 1038812  3011411 |  380897   18842  2790992   148.1 |  0.018 % |
c |     18995 | 1038812  3011411 |  418986   18994  2830922   149.0 |  0.018 % |
c |     19221 | 1038812  3011411 |  460885   19220  2845252   148.0 |  0.018 % |
c |     19559 | 1038812  3011411 |  506973   19558  2862220   146.3 |  0.018 % |
c |     20067 | 1038812  3011411 |  557671   20066  2886912   143.9 |  0.018 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.93 2/54 13048
Raw data (stat): 13048 (runsolver) R 13047 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540907084 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 33507 0 0 0 923 76 0 0 25 0 1 0 540907084 141996032 30604 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34667 30604 603 41 0 34626 0
vsize: 138668
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34448 0 0 0 1919 78 0 0 25 0 1 0 540907084 146518016 31545 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35771 31545 603 41 0 35730 0
vsize: 143084
[startup+30.0009 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34630 0 0 0 2918 79 0 0 25 0 1 0 540907084 147292160 31695 4294967295 134512640 134672761 3221224528 3221223664 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35960 31695 603 41 0 35919 0
vsize: 143840
[startup+40.001 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34649 0 0 0 3918 79 0 0 25 0 1 0 540907084 147292160 31714 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35960 31714 603 41 0 35919 0
vsize: 143840
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34687 0 0 0 4918 80 0 0 25 0 1 0 540907084 147427328 31752 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35993 31752 603 41 0 35952 0
vsize: 143972
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34726 0 0 0 5918 80 0 0 25 0 1 0 540907084 148086784 31791 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36154 31791 603 41 0 36113 0
vsize: 144616
[startup+70.003 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34743 0 0 0 6918 80 0 0 25 0 1 0 540907084 148086784 31808 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36154 31808 603 41 0 36113 0
vsize: 144616
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34821 0 0 0 7917 81 0 0 25 0 1 0 540907084 148353024 31886 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36219 31886 603 41 0 36178 0
vsize: 144876
[startup+90.0029 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34834 0 0 0 8917 81 0 0 25 0 1 0 540907084 148484096 31899 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36251 31899 603 41 0 36210 0
vsize: 145004
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34847 0 0 0 9917 82 0 0 25 0 1 0 540907084 148484096 31912 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36251 31912 603 41 0 36210 0
vsize: 145004
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34860 0 0 0 10916 82 0 0 25 0 1 0 540907084 148611072 31925 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36282 31925 603 41 0 36241 0
vsize: 145128
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34882 0 0 0 11916 83 0 0 25 0 1 0 540907084 148611072 31947 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36282 31947 603 41 0 36241 0
vsize: 145128
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34895 0 0 0 12916 83 0 0 25 0 1 0 540907084 148746240 31960 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36315 31960 603 41 0 36274 0
vsize: 145260
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 34909 0 0 0 13915 84 0 0 25 0 1 0 540907084 148746240 31974 4294967295 134512640 134672761 3221224528 3221223696 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36315 31974 603 41 0 36274 0
vsize: 145260
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35025 0 0 0 14914 84 0 0 25 0 1 0 540907084 149270528 32090 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36443 32090 603 41 0 36402 0
vsize: 145772
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35069 0 0 0 15914 85 0 0 25 0 1 0 540907084 149413888 32134 4294967295 134512640 134672761 3221224528 3221223664 134560694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36478 32134 603 41 0 36437 0
vsize: 145912
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35078 0 0 0 16914 85 0 0 25 0 1 0 540907084 149413888 32143 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36478 32143 603 41 0 36437 0
vsize: 145912
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35085 0 0 0 17914 85 0 0 25 0 1 0 540907084 149413888 32150 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36478 32150 603 41 0 36437 0
vsize: 145912
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35095 0 0 0 18914 86 0 0 25 0 1 0 540907084 149544960 32160 4294967295 134512640 134672761 3221224528 3221223664 134560694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36510 32160 603 41 0 36469 0
vsize: 146040
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35105 0 0 0 19914 86 0 0 25 0 1 0 540907084 149544960 32170 4294967295 134512640 134672761 3221224528 3221223712 134558658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36510 32170 603 41 0 36469 0
vsize: 146040
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35118 0 0 0 20914 86 0 0 25 0 1 0 540907084 149544960 32183 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36510 32183 603 41 0 36469 0
vsize: 146040
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35140 0 0 0 21914 86 0 0 25 0 1 0 540907084 149680128 32205 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36543 32205 603 41 0 36502 0
vsize: 146172
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35175 0 0 0 22914 86 0 0 25 0 1 0 540907084 149823488 32240 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36578 32240 603 41 0 36537 0
vsize: 146312
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35204 0 0 0 23914 86 0 0 25 0 1 0 540907084 149954560 32269 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36610 32269 603 41 0 36569 0
vsize: 146440
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35236 0 0 0 24914 86 0 0 25 0 1 0 540907084 150089728 32301 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36643 32301 603 41 0 36602 0
vsize: 146572
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35281 0 0 0 25914 86 0 0 25 0 1 0 540907084 150224896 32346 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36676 32346 603 41 0 36635 0
vsize: 146704
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35298 0 0 0 26914 86 0 0 25 0 1 0 540907084 150364160 32363 4294967295 134512640 134672761 3221224528 3221223664 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36710 32363 603 41 0 36669 0
vsize: 146840
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35305 0 0 0 27914 86 0 0 25 0 1 0 540907084 150364160 32370 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36710 32370 603 41 0 36669 0
vsize: 146840
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35320 0 0 0 28914 87 0 0 25 0 1 0 540907084 150495232 32385 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36742 32385 603 41 0 36701 0
vsize: 146968
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35334 0 0 0 29914 87 0 0 25 0 1 0 540907084 150495232 32399 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36742 32399 603 41 0 36701 0
vsize: 146968
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35345 0 0 0 30915 87 0 0 25 0 1 0 540907084 150495232 32410 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36742 32410 603 41 0 36701 0
vsize: 146968
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35362 0 0 0 31915 87 0 0 25 0 1 0 540907084 150630400 32427 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36775 32427 603 41 0 36734 0
vsize: 147100
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35453 0 0 0 32915 87 0 0 25 0 1 0 540907084 151019520 32518 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36870 32518 603 41 0 36829 0
vsize: 147480
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35571 0 0 0 33915 87 0 0 25 0 1 0 540907084 151412736 32636 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36966 32636 603 41 0 36925 0
vsize: 147864
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35781 0 0 0 34914 87 0 0 25 0 1 0 540907084 152260608 32846 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37173 32846 603 41 0 37132 0
vsize: 148692
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35971 0 0 0 35914 88 0 0 25 0 1 0 540907084 153116672 33036 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37382 33036 603 41 0 37341 0
vsize: 149528
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 35990 0 0 0 36914 88 0 0 25 0 1 0 540907084 153255936 33055 4294967295 134512640 134672761 3221224528 3221223632 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37416 33055 603 41 0 37375 0
vsize: 149664
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36013 0 0 0 37914 88 0 0 25 0 1 0 540907084 153255936 33078 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37416 33078 603 41 0 37375 0
vsize: 149664
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36059 0 0 0 38914 88 0 0 25 0 1 0 540907084 153530368 33124 4294967295 134512640 134672761 3221224528 3221223676 1074733095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37483 33124 603 41 0 37442 0
vsize: 149932
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36159 0 0 0 39915 88 0 0 25 0 1 0 540907084 153804800 33224 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37550 33224 603 41 0 37509 0
vsize: 150200
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36263 0 0 0 40915 88 0 0 25 0 1 0 540907084 154341376 33328 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37681 33328 603 41 0 37640 0
vsize: 150724
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36298 0 0 0 41915 88 0 0 25 0 1 0 540907084 154476544 33363 4294967295 134512640 134672761 3221224528 3221223680 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37714 33363 603 41 0 37673 0
vsize: 150856
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36310 0 0 0 42915 88 0 0 25 0 1 0 540907084 154476544 33375 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37714 33375 603 41 0 37673 0
vsize: 150856
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36318 0 0 0 43915 88 0 0 25 0 1 0 540907084 154476544 33383 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37714 33383 603 41 0 37673 0
vsize: 150856
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36329 0 0 0 44915 88 0 0 25 0 1 0 540907084 154611712 33394 4294967295 134512640 134672761 3221224528 3221223696 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37747 33394 603 41 0 37706 0
vsize: 150988
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36340 0 0 0 45916 88 0 0 25 0 1 0 540907084 154611712 33405 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37747 33405 603 41 0 37706 0
vsize: 150988
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 13048
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36352 0 0 0 46916 89 0 0 25 0 1 0 540907084 154611712 33417 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37747 33417 603 41 0 37706 0
vsize: 150988
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.93 3/55 13049
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36362 0 0 0 47916 89 0 0 25 0 1 0 540907084 154742784 33427 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37779 33427 603 41 0 37738 0
vsize: 151116
[startup+490.01 s]
Raw data (loadavg): 1.14 1.00 0.94 2/54 13101
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36380 0 0 0 48914 90 0 0 25 0 1 0 540907084 154742784 33445 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37779 33445 603 41 0 37738 0
vsize: 151116
[startup+500.011 s]
Raw data (loadavg): 1.12 1.00 0.94 2/54 13101
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36384 0 0 0 49914 90 0 0 25 0 1 0 540907084 154873856 33449 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37811 33449 603 41 0 37770 0
vsize: 151244
[startup+510.012 s]
Raw data (loadavg): 1.10 1.00 0.94 2/54 13101
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36391 0 0 0 50914 90 0 0 25 0 1 0 540907084 154873856 33456 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37811 33456 603 41 0 37770 0
vsize: 151244
[startup+520.011 s]
Raw data (loadavg): 1.08 1.00 0.94 2/54 13101
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36401 0 0 0 51914 90 0 0 25 0 1 0 540907084 154873856 33466 4294967295 134512640 134672761 3221224528 3221223696 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37811 33466 603 41 0 37770 0
vsize: 151244
[startup+530.011 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 13101
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36409 0 0 0 52915 90 0 0 25 0 1 0 540907084 154873856 33474 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37811 33474 603 41 0 37770 0
vsize: 151244
[startup+540.011 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 13101
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36417 0 0 0 53915 90 0 0 25 0 1 0 540907084 155004928 33482 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37843 33482 603 41 0 37802 0
vsize: 151372
[startup+550.01 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36425 0 0 0 54915 90 0 0 25 0 1 0 540907084 155004928 33490 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37843 33490 603 41 0 37802 0
vsize: 151372
[startup+560.011 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36443 0 0 0 55915 90 0 0 25 0 1 0 540907084 155004928 33508 4294967295 134512640 134672761 3221224528 3221223684 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37843 33508 603 41 0 37802 0
vsize: 151372
[startup+570.012 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36494 0 0 0 56915 90 0 0 25 0 1 0 540907084 155267072 33559 4294967295 134512640 134672761 3221224528 3221223632 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37907 33559 603 41 0 37866 0
vsize: 151628
[startup+580.012 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36516 0 0 0 57915 90 0 0 25 0 1 0 540907084 155398144 33581 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37939 33581 603 41 0 37898 0
vsize: 151756
[startup+590.012 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36532 0 0 0 58915 90 0 0 25 0 1 0 540907084 155398144 33597 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37939 33597 603 41 0 37898 0
vsize: 151756
[startup+600.012 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36552 0 0 0 59915 90 0 0 25 0 1 0 540907084 155533312 33617 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37972 33617 603 41 0 37931 0
vsize: 151888
[startup+610.013 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36595 0 0 0 60915 90 0 0 25 0 1 0 540907084 155668480 33660 4294967295 134512640 134672761 3221224528 3221223632 134559969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38005 33660 603 41 0 37964 0
vsize: 152020
[startup+620.012 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36624 0 0 0 61915 90 0 0 25 0 1 0 540907084 155803648 33689 4294967295 134512640 134672761 3221224528 3221223696 134561388 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38038 33689 603 41 0 37997 0
vsize: 152152
[startup+630.012 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36682 0 0 0 62915 91 0 0 25 0 1 0 540907084 156082176 33747 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38106 33747 603 41 0 38065 0
vsize: 152424
[startup+640.013 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36755 0 0 0 63915 91 0 0 25 0 1 0 540907084 156348416 33820 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38171 33820 603 41 0 38130 0
vsize: 152684
[startup+650.012 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36778 0 0 0 64915 91 0 0 25 0 1 0 540907084 156348416 33843 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38171 33843 603 41 0 38130 0
vsize: 152684
[startup+660.012 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36800 0 0 0 65915 91 0 0 25 0 1 0 540907084 156483584 33865 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38204 33865 603 41 0 38163 0
vsize: 152816
[startup+670.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36810 0 0 0 66916 91 0 0 25 0 1 0 540907084 156483584 33875 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38204 33875 603 41 0 38163 0
vsize: 152816
[startup+680.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36822 0 0 0 67916 91 0 0 25 0 1 0 540907084 156483584 33887 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38204 33887 603 41 0 38163 0
vsize: 152816
[startup+690.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36831 0 0 0 68916 91 0 0 25 0 1 0 540907084 156618752 33896 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38237 33896 603 41 0 38196 0
vsize: 152948
[startup+700.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36843 0 0 0 69917 91 0 0 25 0 1 0 540907084 156618752 33908 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38237 33908 603 41 0 38196 0
vsize: 152948
[startup+710.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36852 0 0 0 70918 91 0 0 25 0 1 0 540907084 156618752 33917 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38237 33917 603 41 0 38196 0
vsize: 152948
[startup+720.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36861 0 0 0 71918 91 0 0 25 0 1 0 540907084 156749824 33926 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38269 33926 603 41 0 38228 0
vsize: 153076
[startup+730.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36870 0 0 0 72918 91 0 0 25 0 1 0 540907084 156749824 33935 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38269 33935 603 41 0 38228 0
vsize: 153076
[startup+740.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36878 0 0 0 73919 91 0 0 25 0 1 0 540907084 156749824 33943 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38269 33943 603 41 0 38228 0
vsize: 153076
[startup+750.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36885 0 0 0 74919 91 0 0 25 0 1 0 540907084 156749824 33950 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38269 33950 603 41 0 38228 0
vsize: 153076
[startup+760.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36893 0 0 0 75919 91 0 0 25 0 1 0 540907084 156880896 33958 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38301 33958 603 41 0 38260 0
vsize: 153204
[startup+770.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36905 0 0 0 76919 91 0 0 25 0 1 0 540907084 156880896 33970 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38301 33970 603 41 0 38260 0
vsize: 153204
[startup+780.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36917 0 0 0 77919 91 0 0 25 0 1 0 540907084 156880896 33982 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38301 33982 603 41 0 38260 0
vsize: 153204
[startup+790.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36927 0 0 0 78920 91 0 0 25 0 1 0 540907084 157016064 33992 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38334 33992 603 41 0 38293 0
vsize: 153336
[startup+800.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36940 0 0 0 79920 91 0 0 25 0 1 0 540907084 157016064 34005 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38334 34005 603 41 0 38293 0
vsize: 153336
[startup+810.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36955 0 0 0 80921 91 0 0 25 0 1 0 540907084 157155328 34020 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38368 34020 603 41 0 38327 0
vsize: 153472
[startup+820.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 36963 0 0 0 81921 91 0 0 25 0 1 0 540907084 157155328 34028 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38368 34028 603 41 0 38327 0
vsize: 153472
[startup+830.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37016 0 0 0 82921 91 0 0 25 0 1 0 540907084 157274112 34081 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38397 34081 603 41 0 38356 0
vsize: 153588
[startup+840.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37027 0 0 0 83921 91 0 0 25 0 1 0 540907084 157405184 34092 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38429 34092 603 41 0 38388 0
vsize: 153716
[startup+850.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13103
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37045 0 0 0 84921 91 0 0 25 0 1 0 540907084 157405184 34110 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38429 34110 603 41 0 38388 0
vsize: 153716
[startup+860.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37051 0 0 0 85922 91 0 0 25 0 1 0 540907084 157536256 34116 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38461 34116 603 41 0 38420 0
vsize: 153844
[startup+870.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37061 0 0 0 86922 91 0 0 25 0 1 0 540907084 157536256 34126 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38461 34126 603 41 0 38420 0
vsize: 153844
[startup+880.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37070 0 0 0 87922 91 0 0 25 0 1 0 540907084 157536256 34135 4294967295 134512640 134672761 3221224528 3221223672 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38461 34135 603 41 0 38420 0
vsize: 153844
[startup+890.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37090 0 0 0 88922 91 0 0 25 0 1 0 540907084 157671424 34155 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38494 34155 603 41 0 38453 0
vsize: 153976
[startup+900.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37127 0 0 0 89923 91 0 0 25 0 1 0 540907084 157806592 34192 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38527 34192 603 41 0 38486 0
vsize: 154108
[startup+910.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37175 0 0 0 90923 92 0 0 25 0 1 0 540907084 157941760 34240 4294967295 134512640 134672761 3221224528 3221223696 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38560 34240 603 41 0 38519 0
vsize: 154240
[startup+920.048 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37194 0 0 0 91923 92 0 0 25 0 1 0 540907084 158076928 34259 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38593 34259 603 41 0 38552 0
vsize: 154372
[startup+930.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37203 0 0 0 92923 92 0 0 25 0 1 0 540907084 158076928 34268 4294967295 134512640 134672761 3221224528 3221223632 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38593 34268 603 41 0 38552 0
vsize: 154372
[startup+940.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37225 0 0 0 93923 92 0 0 25 0 1 0 540907084 158298112 34290 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38647 34290 603 41 0 38606 0
vsize: 154588
[startup+950.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37225 0 0 0 94923 92 0 0 25 0 1 0 540907084 158298112 34290 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38647 34290 603 41 0 38606 0
vsize: 154588
[startup+960.048 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37225 0 0 0 95924 92 0 0 25 0 1 0 540907084 158298112 34290 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38647 34290 603 41 0 38606 0
vsize: 154588
[startup+970.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37228 0 0 0 96924 92 0 0 25 0 1 0 540907084 158298112 34293 4294967295 134512640 134672761 3221224528 3221223792 134562359 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38647 34293 603 41 0 38606 0
vsize: 154588
[startup+980.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37239 0 0 0 97924 92 0 0 25 0 1 0 540907084 158298112 34304 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38647 34304 603 41 0 38606 0
vsize: 154588
[startup+990.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37253 0 0 0 98924 92 0 0 25 0 1 0 540907084 158298112 34318 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38647 34318 603 41 0 38606 0
vsize: 154588
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37264 0 0 0 99924 92 0 0 25 0 1 0 540907084 158433280 34329 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38680 34329 603 41 0 38639 0
vsize: 154720
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37273 0 0 0 100924 92 0 0 25 0 1 0 540907084 158433280 34338 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38680 34338 603 41 0 38639 0
vsize: 154720
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37281 0 0 0 101925 92 0 0 25 0 1 0 540907084 158433280 34346 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38680 34346 603 41 0 38639 0
vsize: 154720
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37290 0 0 0 102925 92 0 0 25 0 1 0 540907084 158433280 34355 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38680 34355 603 41 0 38639 0
vsize: 154720
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37301 0 0 0 103925 92 0 0 25 0 1 0 540907084 158564352 34366 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38712 34366 603 41 0 38671 0
vsize: 154848
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37311 0 0 0 104925 92 0 0 25 0 1 0 540907084 158564352 34376 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38712 34376 603 41 0 38671 0
vsize: 154848
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37320 0 0 0 105925 92 0 0 25 0 1 0 540907084 158564352 34385 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38712 34385 603 41 0 38671 0
vsize: 154848
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37325 0 0 0 106925 92 0 0 25 0 1 0 540907084 158564352 34390 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38712 34390 603 41 0 38671 0
vsize: 154848
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37333 0 0 0 107925 92 0 0 25 0 1 0 540907084 158695424 34398 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38744 34398 603 41 0 38703 0
vsize: 154976
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37338 0 0 0 108926 92 0 0 25 0 1 0 540907084 158695424 34403 4294967295 134512640 134672761 3221224528 3221223632 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38744 34403 603 41 0 38703 0
vsize: 154976
[startup+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37349 0 0 0 109926 92 0 0 25 0 1 0 540907084 158695424 34414 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38744 34414 603 41 0 38703 0
vsize: 154976
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37504 0 0 0 110925 93 0 0 25 0 1 0 540907084 159387648 34569 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38913 34569 603 41 0 38872 0
vsize: 155652
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37597 0 0 0 111925 93 0 0 25 0 1 0 540907084 159805440 34662 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39015 34662 603 41 0 38974 0
vsize: 156060
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37609 0 0 0 112925 93 0 0 25 0 1 0 540907084 159805440 34674 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39015 34674 603 41 0 38974 0
vsize: 156060
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37617 0 0 0 113925 93 0 0 25 0 1 0 540907084 159805440 34682 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39015 34682 603 41 0 38974 0
vsize: 156060
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37630 0 0 0 114925 93 0 0 25 0 1 0 540907084 159932416 34695 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39046 34695 603 41 0 39005 0
vsize: 156184
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37635 0 0 0 115926 93 0 0 25 0 1 0 540907084 159932416 34700 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39046 34700 603 41 0 39005 0
vsize: 156184
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37647 0 0 0 116926 93 0 0 25 0 1 0 540907084 159932416 34712 4294967295 134512640 134672761 3221224528 3221223696 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39046 34712 603 41 0 39005 0
vsize: 156184
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37656 0 0 0 117926 93 0 0 25 0 1 0 540907084 159932416 34721 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39046 34721 603 41 0 39005 0
vsize: 156184
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37666 0 0 0 118926 93 0 0 25 0 1 0 540907084 160063488 34731 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39078 34731 603 41 0 39037 0
vsize: 156312
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13105
Raw data (stat): 13048 (minisat+) R 13047 10614 10613 0 -1 0 37675 0 0 0 119926 93 0 0 25 0 1 0 540907084 160063488 34740 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39078 34740 603 41 0 39037 0
vsize: 156312
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 13105
Raw data (stat): 13048 (minisat+) Z 13047 10614 10613 0 -1 12 37678 0 0 0 119926 100 0 0 25 0 1 0 540907084 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.12
CPU time (s): 1200.27
CPU user time (s): 1199.27
CPU system time (s): 1.00585
CPU usage (%): 100.013
Max. virtual memory (Kb): 156312
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####