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 32472

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-05-27 10:09:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23855 boxname=wulflinc28 idbench=1499 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f88781e3d6e9a5487d13eaa213c27b55  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-markshare1_1.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-markshare1_1.opb
IDLAUNCH: 23855
/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:        877012 kB
Buffers:         18192 kB
Cached:         118788 kB
SwapCached:        788 kB
Active:          17748 kB
Inactive:       121520 kB
HighTotal:      131008 kB
HighFree:         9352 kB
LowTotal:       903652 kB
LowFree:        867660 kB
SwapTotal:     2097640 kB
SwapFree:      2096168 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5448 kB
Slab:            12772 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 10:30:19 (client local time) WITH STATUS 152 IN 1229.9 SECONDS
stats: 23855 7 1229.9 152
#### 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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 % |
c |     20826 | 1038812  3011411 |  613438   20825  2917518   140.1 |  0.018 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 19361 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.93 0.98 0.91 2/54 19357
Raw data (stat): 19357 (runsolver) R 19356 24821 24820 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 855337364 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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+9.9999 s]
Raw data (loadavg): 0.94 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+19.9997 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0004 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+49.9997 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+59.9994 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+69.9991 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0038 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.01 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.01 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.01 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.011 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.011 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.014 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.015 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.014 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.014 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 19361
Raw data (stat): 19357 (minisat+_script) S 19356 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855337364 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.9
CPU user time (s): 1228.85
CPU system time (s): 1.05684
CPU usage (%): 100.015
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####