PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-14 04:39:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4835 boxname=wulflinc31 idbench=323 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  70070c820bc7d178cc8f33b42e0deead  /oldhome/oroussel/tmp/wulflinc31/normalized-frb35-17-5.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc31/normalized-frb35-17-5.opb /oldhome/oroussel/tmp/wulflinc31/normalized-frb35-17-5.opb
IDLAUNCH: 4835
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        886924 kB
Buffers:         36380 kB
Cached:          72504 kB
SwapCached:        392 kB
Active:          54040 kB
Inactive:        58056 kB
HighTotal:      131008 kB
HighFree:        54824 kB
LowTotal:       903652 kB
LowFree:        832100 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            30132 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:59:25 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 4835 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 28143 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   28143    56286 |    9381       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   84748   188800 |   28249       0        0     nan |  0.000 % |
c |       100 |   84624   188521 |   31073      96      432     4.5 |  0.177 % |
c |       254 |   83390   185712 |   34181     230     1363     5.9 |  2.032 % |
c |       479 |   81071   180414 |   37599     401     2950     7.4 |  5.621 % |
c |       816 |   78150   173694 |   41359     672     4804     7.1 | 10.342 % |
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       908 |   77762   172942 |   25920     755     5333     7.1 | 10.342 % |
c |      1008 |   76198   169362 |   28512     828     6299     7.6 | 13.838 % |
c |      1158 |   74950   166475 |   31363     947     7232     7.6 | 15.932 % |
c ==============================================================================
c [1mFound solution: -24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1166 |   74911   166381 |   24970     955     7288     7.6 | 15.932 % |
c |      1266 |   73647   163469 |   27467    1027     8055     7.8 | 18.029 % |
c |      1416 |   72177   160076 |   30213    1139     8986     7.9 | 20.970 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1635 |   70164   155409 |   23388    1285     9911     7.7 | 20.970 % |
c |      1735 |   69071   152889 |   25726    1363    10823     7.9 | 25.684 % |
c |      1885 |   68023   150463 |   28299    1486    13545     9.1 | 27.408 % |
c |      2110 |   64685   142729 |   31129    1602    16022    10.0 | 32.936 % |
c |      2447 |   61596   135541 |   34242    1799    17922    10.0 | 38.128 % |
c |      2953 |   57693   126365 |   37666    2158    23279    10.8 | 44.612 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3306 |   55839   122085 |   18613    2362    25814    10.9 | 44.612 % |
c |      3406 |   54488   118911 |   20474    2357    26158    11.1 | 50.568 % |
c |      3556 |   53735   117145 |   22521    2479    27525    11.1 | 52.063 % |
c |      3782 |   53053   115551 |   24773    2658    28929    10.9 | 53.081 % |
c |      4119 |   50977   110716 |   27251    2861    30434    10.6 | 56.699 % |
c |      4625 |   49032   106169 |   29976    3192    34378    10.8 | 60.111 % |
c |      5384 |   46429   100083 |   32974    3706    44639    12.0 | 64.649 % |
c |      6525 |   43415    92953 |   36271    4460    57911    13.0 | 69.957 % |
c |      8234 |   41425    88281 |   39898    5771   110823    19.2 | 73.508 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10722 |   39860    84554 |   13286    7566   158098    20.9 | 73.508 % |
c |     10822 |   39675    84120 |   14614    7606   158812    20.9 | 76.630 % |
c |     10973 |   39495    83691 |   16076    7643   161838    21.2 | 76.944 % |
c |     11198 |   39447    83577 |   17683    7810   172408    22.1 | 77.036 % |
c |     11535 |   39095    82746 |   19452    7908   173835    22.0 | 77.668 % |
c |     12041 |   38754    81935 |   21397    8167   205796    25.2 | 78.305 % |
c |     12800 |   37569    79149 |   23536    8465   228498    27.0 | 80.443 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13651 |   37374    78699 |   12458    9195   277934    30.2 | 80.443 % |
c |     13753 |   37374    78699 |   13703    9297   280111    30.1 | 80.870 % |
c |     13903 |   37160    78199 |   15074    9258   281896    30.4 | 81.255 % |
c |     14128 |   37160    78199 |   16581    9483   298554    31.5 | 81.255 % |
c |     14465 |   37160    78199 |   18239    9820   310124    31.6 | 81.255 % |
c |     14971 |   36561    76799 |   20063   10017   321371    32.1 | 82.312 % |
c |     15731 |   36561    76799 |   22070   10777   361875    33.6 | 82.312 % |
c |     16870 |   35970    75418 |   24277   11815   415944    35.2 | 83.369 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18001 |   35939    75321 |   11979   12708   474326    37.3 | 83.369 % |
c |     18101 |   35919    75274 |   13176   12801   475124    37.1 | 83.443 % |
c |     18251 |   35919    75274 |   14494   12951   482995    37.3 | 83.443 % |
c |     18476 |   35919    75274 |   15944   13176   501084    38.0 | 83.443 % |
c |     18814 |   35919    75274 |   17538   13514   516653    38.2 | 83.443 % |
c |     19320 |   35915    75265 |   19292   14019   546644    39.0 | 83.448 % |
c |     20081 |   35915    75265 |   21221   14780   604609    40.9 | 83.448 % |
c |     21220 |   35851    75115 |   23343   15813   669897    42.4 | 83.566 % |
c |     22929 |   35841    75091 |   25678   17518   789160    45.0 | 83.586 % |
c |     25491 |   35825    75054 |   28245   20078   979848    48.8 | 83.612 % |
c |     29335 |   35825    75054 |   31070   23922  1430972    59.8 | 83.612 % |
c |     35101 |   35825    75054 |   34177   29688  1877159    63.2 | 83.612 % |
c |     43751 |   35825    75054 |   37595   38338  2465402    64.3 | 83.612 % |
c |     56726 |   35825    75054 |   41354   51313  3290818    64.1 | 83.612 % |
c |     76187 |   35819    75040 |   45490   28480  2114446    74.2 | 83.622 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94239 |   35784    74967 |   11928   46502  3559087    76.5 | 83.622 % |
c |     94339 |   35784    74967 |   13120   15445   929262    60.2 | 83.769 % |
c |     94490 |   35784    74967 |   14432   15596   936226    60.0 | 83.769 % |
c |     94715 |   35784    74967 |   15876   15821   947356    59.9 | 83.769 % |
c |     95054 |   35784    74967 |   17463   16160   963384    59.6 | 83.768 % |
c |     95560 |   35784    74967 |   19210   16666   995213    59.7 | 83.769 % |
c |     96319 |   35784    74967 |   21131   17425  1039793    59.7 | 83.769 % |
c |     97460 |   35784    74967 |   23244   18566  1130509    60.9 | 83.768 % |
c |     99168 |   35766    74925 |   25568   20263  1260001    62.2 | 83.799 % |
c |    101730 |   35470    74235 |   28125   22790  1406948    61.7 | 84.305 % |
c |    105575 |   35470    74235 |   30938   26635  1672008    62.8 | 84.305 % |
c |    111341 |   35470    74235 |   34031   32401  1892123    58.4 | 84.305 % |
c |    119990 |   35464    74221 |   37435   41049  2607512    63.5 | 84.315 % |
c |    132965 |   35464    74221 |   41178   54024  3690497    68.3 | 84.315 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    138080 |   35371    73970 |   11790   59134  4033036    68.2 | 84.315 % |
c |    138180 |   35371    73970 |   12969   17157   956412    55.7 | 84.455 % |
c |    138330 |   35371    73970 |   14265   17307   964684    55.7 | 84.455 % |
c |    138556 |   35371    73970 |   15692   17533   978963    55.8 | 84.455 % |
c |    138893 |   35371    73970 |   17261   17870  1002097    56.1 | 84.455 % |
c |    139400 |   35365    73956 |   18987   18370  1034378    56.3 | 84.465 % |
c |    140159 |   35365    73956 |   20886   19129  1082219    56.6 | 84.465 % |
c |    141300 |   35172    73504 |   22975   20256  1158377    57.2 | 84.812 % |
c |    143008 |   35172    73504 |   25272   21964  1304359    59.4 | 84.812 % |
c |    145570 |   35172    73504 |   27800   24526  1468083    59.9 | 84.812 % |
c |    149414 |   35172    73504 |   30580   28370  1785813    62.9 | 84.812 % |
c |    155182 |   35172    73504 |   33638   34138  2125445    62.3 | 84.812 % |
c |    163831 |   35172    73504 |   37002   42787  2721954    63.6 | 84.812 % |
c |    176805 |   35172    73504 |   40702   17336   617344    35.6 | 84.812 % |
c |    196266 |   35162    73481 |   44772   36790  1508532    41.0 | 84.828 % |
c |    225458 |   35162    73481 |   49249   22610   964663    42.7 | 84.828 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    245961 |   34974    73031 |   11658   42987  2195159    51.1 | 84.828 % |
c |    246061 |   34974    73031 |   12823   17665   678213    38.4 | 85.215 % |
c |    246211 |   34974    73031 |   14106   17815   683166    38.3 | 85.215 % |
c |    246436 |   34974    73031 |   15516   18040   696179    38.6 | 85.215 % |
c |    246774 |   34968    73017 |   17068   18351   711063    38.7 | 85.225 % |
c |    247280 |   34940    72949 |   18775   18847   733517    38.9 | 85.287 % |
c |    248040 |   34940    72949 |   20652   19607   775148    39.5 | 85.287 % |
c |    249179 |   34940    72949 |   22718   20746   838247    40.4 | 85.287 % |
c |    250887 |   34814    72658 |   24989   22412   946326    42.2 | 85.496 % |
c |    253449 |   34814    72658 |   27488   24974  1089645    43.6 | 85.496 % |
c |    257294 |   34808    72644 |   30237   28817  1336073    46.4 | 85.506 % |
c |    263060 |   34808    72644 |   33261   34583  1626529    47.0 | 85.506 % |
c |    271711 |   34808    72644 |   36587   43234  2031152    47.0 | 85.506 % |
c |    284685 |   34808    72644 |   40246   20013   584102    29.2 | 85.506 % |
c |    304147 |   34796    72616 |   44271   39470  1417064    35.9 | 85.526 % |
c |    333339 |   34790    72602 |   48698   25628   797603    31.1 | 85.537 % |
c |    377128 |   34723    72436 |   53568   23138   555975    24.0 | 85.674 % |
c |    442813 |   34685    72346 |   58925   36288  1511640    41.7 | 85.746 % |
c |    541340 |   34544    72012 |   64817   22531   589911    26.2 | 86.016 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.92 2/54 31328
Raw data (stat): 31328 (runsolver) R 31327 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481765257 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 2416 0 0 0 991 7 0 0 25 0 1 0 481765257 12247040 2387 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2387 603 41 0 2949 0
vsize: 11960
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 2418 0 0 0 1990 7 0 0 25 0 1 0 481765257 12247040 2389 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2389 603 41 0 2949 0
vsize: 11960
[startup+30.0027 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 2739 0 0 0 2989 8 0 0 25 0 1 0 481765257 13578240 2710 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3315 2710 603 41 0 3274 0
vsize: 13260
[startup+40.0027 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 3327 0 0 0 3986 10 0 0 25 0 1 0 481765257 16093184 3298 4294967295 134512640 134672761 3221224560 3221223744 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3929 3298 603 41 0 3888 0
vsize: 15716
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 4032 0 0 0 4985 12 0 0 25 0 1 0 481765257 18894848 4003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4613 4003 603 41 0 4572 0
vsize: 18452
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 4474 0 0 0 5983 13 0 0 25 0 1 0 481765257 20766720 4445 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5070 4445 603 41 0 5029 0
vsize: 20280
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 4907 0 0 0 6980 16 0 0 25 0 1 0 481765257 22614016 4878 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5521 4878 603 41 0 5480 0
vsize: 22084
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 5309 0 0 0 7978 17 0 0 25 0 1 0 481765257 24215552 5280 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5912 5280 603 41 0 5871 0
vsize: 23648
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 5603 0 0 0 8978 18 0 0 25 0 1 0 481765257 25407488 5574 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6203 5574 603 41 0 6162 0
vsize: 24812
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 5922 0 0 0 9977 18 0 0 25 0 1 0 481765257 26730496 5893 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6526 5893 603 41 0 6485 0
vsize: 26104
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6319 0 0 0 10976 20 0 0 25 0 1 0 481765257 28336128 6290 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6918 6290 603 41 0 6877 0
vsize: 27672
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6646 0 0 0 11976 21 0 0 25 0 1 0 481765257 29667328 6617 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7243 6617 603 41 0 7202 0
vsize: 28972
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6773 0 0 0 12975 21 0 0 25 0 1 0 481765257 30208000 6744 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6744 603 41 0 7334 0
vsize: 29500
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6773 0 0 0 13975 21 0 0 25 0 1 0 481765257 30208000 6744 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6744 603 41 0 7334 0
vsize: 29500
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6773 0 0 0 14975 21 0 0 25 0 1 0 481765257 30208000 6744 4294967295 134512640 134672761 3221224560 3221223744 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6744 603 41 0 7334 0
vsize: 29500
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6773 0 0 0 15975 21 0 0 25 0 1 0 481765257 30208000 6744 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6744 603 41 0 7334 0
vsize: 29500
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6773 0 0 0 16976 21 0 0 25 0 1 0 481765257 30208000 6744 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6744 603 41 0 7334 0
vsize: 29500
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6773 0 0 0 17976 21 0 0 25 0 1 0 481765257 30208000 6744 4294967295 134512640 134672761 3221224560 3221223664 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6744 603 41 0 7334 0
vsize: 29500
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6775 0 0 0 18976 21 0 0 25 0 1 0 481765257 30208000 6746 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6746 603 41 0 7334 0
vsize: 29500
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6775 0 0 0 19976 21 0 0 25 0 1 0 481765257 30208000 6746 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6746 603 41 0 7334 0
vsize: 29500
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6775 0 0 0 20976 21 0 0 25 0 1 0 481765257 30208000 6746 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6746 603 41 0 7334 0
vsize: 29500
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6775 0 0 0 21976 21 0 0 25 0 1 0 481765257 30208000 6746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6746 603 41 0 7334 0
vsize: 29500
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6775 0 0 0 22977 21 0 0 25 0 1 0 481765257 30208000 6746 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6746 603 41 0 7334 0
vsize: 29500
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6775 0 0 0 23977 21 0 0 25 0 1 0 481765257 30208000 6746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6746 603 41 0 7334 0
vsize: 29500
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6775 0 0 0 24977 21 0 0 25 0 1 0 481765257 30208000 6746 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6746 603 41 0 7334 0
vsize: 29500
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 6932 0 0 0 25977 22 0 0 25 0 1 0 481765257 30871552 6903 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7537 6903 603 41 0 7496 0
vsize: 30148
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 26976 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 27977 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 28977 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 29977 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 30977 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 31977 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 32978 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 33978 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223744 134559379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+350.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 34979 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223712 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 35979 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 36979 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 37979 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+390.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 38979 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 39979 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+410.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7070 0 0 0 40980 22 0 0 25 0 1 0 481765257 31424512 7041 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7041 603 41 0 7631 0
vsize: 30688
[startup+420.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 41980 22 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+430.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 42980 22 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+440.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 43980 22 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+450.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 44980 22 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+460.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 45980 22 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+470.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 46980 22 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+480.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 47981 22 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 48981 22 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+500.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 49981 22 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+510.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 50981 22 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+520.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 51981 23 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+530.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 52981 23 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+540.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 53982 23 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+550.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 54982 23 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 55982 23 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 56982 23 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223664 134559922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+580.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 57982 23 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+590.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7072 0 0 0 58983 23 0 0 25 0 1 0 481765257 31424512 7043 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7043 603 41 0 7631 0
vsize: 30688
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7073 0 0 0 59983 23 0 0 25 0 1 0 481765257 31424512 7044 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7044 603 41 0 7631 0
vsize: 30688
[startup+610.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7073 0 0 0 60983 23 0 0 25 0 1 0 481765257 31424512 7044 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7044 603 41 0 7631 0
vsize: 30688
[startup+620.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7073 0 0 0 61983 23 0 0 25 0 1 0 481765257 31424512 7044 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7044 603 41 0 7631 0
vsize: 30688
[startup+630.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7076 0 0 0 62984 23 0 0 25 0 1 0 481765257 31424512 7047 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7047 603 41 0 7631 0
vsize: 30688
[startup+640.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7077 0 0 0 63984 23 0 0 25 0 1 0 481765257 31424512 7048 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7048 603 41 0 7631 0
vsize: 30688
[startup+650.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7078 0 0 0 64984 23 0 0 25 0 1 0 481765257 31424512 7049 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7672 7049 603 41 0 7631 0
vsize: 30688
[startup+660.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7090 0 0 0 65984 23 0 0 25 0 1 0 481765257 31600640 7061 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7715 7061 603 41 0 7674 0
vsize: 30860
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7103 0 0 0 66984 23 0 0 25 0 1 0 481765257 31600640 7074 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7715 7074 603 41 0 7674 0
vsize: 30860
[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7103 0 0 0 67984 23 0 0 25 0 1 0 481765257 31600640 7074 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7715 7074 603 41 0 7674 0
vsize: 30860
[startup+690.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7123 0 0 0 68985 23 0 0 25 0 1 0 481765257 32026624 7094 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7094 603 41 0 7778 0
vsize: 31276
[startup+700.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7124 0 0 0 69985 23 0 0 25 0 1 0 481765257 32026624 7095 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7095 603 41 0 7778 0
vsize: 31276
[startup+710.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7124 0 0 0 70985 23 0 0 25 0 1 0 481765257 32026624 7095 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7095 603 41 0 7778 0
vsize: 31276
[startup+720.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7124 0 0 0 71985 23 0 0 25 0 1 0 481765257 32026624 7095 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7095 603 41 0 7778 0
vsize: 31276
[startup+730.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7129 0 0 0 72985 23 0 0 25 0 1 0 481765257 32026624 7100 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7100 603 41 0 7778 0
vsize: 31276
[startup+740.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7135 0 0 0 73985 23 0 0 25 0 1 0 481765257 32026624 7106 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7106 603 41 0 7778 0
vsize: 31276
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7135 0 0 0 74985 23 0 0 25 0 1 0 481765257 32026624 7106 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7106 603 41 0 7778 0
vsize: 31276
[startup+760.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7135 0 0 0 75986 23 0 0 25 0 1 0 481765257 32026624 7106 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7106 603 41 0 7778 0
vsize: 31276
[startup+770.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7158 0 0 0 76985 23 0 0 25 0 1 0 481765257 32219136 7129 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7129 603 41 0 7825 0
vsize: 31464
[startup+780.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7160 0 0 0 77986 23 0 0 25 0 1 0 481765257 32219136 7131 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7131 603 41 0 7825 0
vsize: 31464
[startup+790.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7163 0 0 0 78986 23 0 0 25 0 1 0 481765257 32219136 7134 4294967295 134512640 134672761 3221224560 3221223696 134565140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7134 603 41 0 7825 0
vsize: 31464
[startup+800.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7163 0 0 0 79986 23 0 0 25 0 1 0 481765257 32219136 7134 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7134 603 41 0 7825 0
vsize: 31464
[startup+810.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7163 0 0 0 80986 23 0 0 25 0 1 0 481765257 32219136 7134 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7134 603 41 0 7825 0
vsize: 31464
[startup+820.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7163 0 0 0 81986 23 0 0 25 0 1 0 481765257 32219136 7134 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7134 603 41 0 7825 0
vsize: 31464
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7163 0 0 0 82986 23 0 0 25 0 1 0 481765257 32219136 7134 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7134 603 41 0 7825 0
vsize: 31464
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7163 0 0 0 83986 23 0 0 25 0 1 0 481765257 32219136 7134 4294967295 134512640 134672761 3221224560 3221223664 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7134 603 41 0 7825 0
vsize: 31464
[startup+850.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7169 0 0 0 84987 23 0 0 25 0 1 0 481765257 32219136 7140 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7140 603 41 0 7825 0
vsize: 31464
[startup+860.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7177 0 0 0 85987 23 0 0 25 0 1 0 481765257 32219136 7148 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7148 603 41 0 7825 0
vsize: 31464
[startup+870.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7177 0 0 0 86987 23 0 0 25 0 1 0 481765257 32219136 7148 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7148 603 41 0 7825 0
vsize: 31464
[startup+880.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7177 0 0 0 87987 23 0 0 25 0 1 0 481765257 32219136 7148 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7148 603 41 0 7825 0
vsize: 31464
[startup+890.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7179 0 0 0 88987 23 0 0 25 0 1 0 481765257 32219136 7150 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7150 603 41 0 7825 0
vsize: 31464
[startup+900.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7186 0 0 0 89987 23 0 0 25 0 1 0 481765257 32219136 7157 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7866 7157 603 41 0 7825 0
vsize: 31464
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7200 0 0 0 90987 23 0 0 25 0 1 0 481765257 32382976 7171 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7171 603 41 0 7865 0
vsize: 31624
[startup+920.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7201 0 0 0 91988 23 0 0 25 0 1 0 481765257 32382976 7172 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7172 603 41 0 7865 0
vsize: 31624
[startup+930.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7201 0 0 0 92988 23 0 0 25 0 1 0 481765257 32382976 7172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7172 603 41 0 7865 0
vsize: 31624
[startup+940.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7201 0 0 0 93988 23 0 0 25 0 1 0 481765257 32382976 7172 4294967295 134512640 134672761 3221224560 3221223744 134559356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7172 603 41 0 7865 0
vsize: 31624
[startup+950.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7201 0 0 0 94988 23 0 0 25 0 1 0 481765257 32382976 7172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7172 603 41 0 7865 0
vsize: 31624
[startup+960.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7207 0 0 0 95988 23 0 0 25 0 1 0 481765257 32382976 7178 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7178 603 41 0 7865 0
vsize: 31624
[startup+970.04 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7207 0 0 0 96988 23 0 0 25 0 1 0 481765257 32382976 7178 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7178 603 41 0 7865 0
vsize: 31624
[startup+980.041 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7207 0 0 0 97989 23 0 0 25 0 1 0 481765257 32382976 7178 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7178 603 41 0 7865 0
vsize: 31624
[startup+990.041 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7207 0 0 0 98989 23 0 0 25 0 1 0 481765257 32382976 7178 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7178 603 41 0 7865 0
vsize: 31624
[startup+1000.04 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7207 0 0 0 99989 23 0 0 25 0 1 0 481765257 32382976 7178 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7178 603 41 0 7865 0
vsize: 31624
[startup+1010.04 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7213 0 0 0 100989 23 0 0 25 0 1 0 481765257 32382976 7184 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7184 603 41 0 7865 0
vsize: 31624
[startup+1020.04 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7221 0 0 0 101989 23 0 0 25 0 1 0 481765257 32382976 7192 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7906 7192 603 41 0 7865 0
vsize: 31624
[startup+1030.04 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7221 0 0 0 102989 23 0 0 25 0 1 0 481765257 32382976 7192 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7192 603 41 0 7865 0
vsize: 31624
[startup+1040.04 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7222 0 0 0 103989 23 0 0 25 0 1 0 481765257 32382976 7193 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7906 7193 603 41 0 7865 0
vsize: 31624
[startup+1050.04 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7233 0 0 0 104989 24 0 0 25 0 1 0 481765257 32546816 7204 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7946 7204 603 41 0 7905 0
vsize: 31784
[startup+1060.04 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7234 0 0 0 105989 24 0 0 25 0 1 0 481765257 32546816 7205 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7946 7205 603 41 0 7905 0
vsize: 31784
[startup+1070.04 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7242 0 0 0 106990 24 0 0 25 0 1 0 481765257 32546816 7213 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7946 7213 603 41 0 7905 0
vsize: 31784
[startup+1080.04 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7242 0 0 0 107990 24 0 0 25 0 1 0 481765257 32546816 7213 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7946 7213 603 41 0 7905 0
vsize: 31784
[startup+1090.04 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7260 0 0 0 108990 24 0 0 25 0 1 0 481765257 32546816 7231 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7946 7231 603 41 0 7905 0
vsize: 31784
[startup+1100.04 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7286 0 0 0 109990 24 0 0 25 0 1 0 481765257 32694272 7257 4294967295 134512640 134672761 3221224560 3221223728 134561086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7982 7257 603 41 0 7941 0
vsize: 31928
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7287 0 0 0 110991 24 0 0 25 0 1 0 481765257 32694272 7258 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7982 7258 603 41 0 7941 0
vsize: 31928
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7288 0 0 0 111991 24 0 0 25 0 1 0 481765257 32694272 7259 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7982 7259 603 41 0 7941 0
vsize: 31928
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7300 0 0 0 112991 24 0 0 25 0 1 0 481765257 32890880 7271 4294967295 134512640 134672761 3221224560 3221223744 134558374 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8030 7271 603 41 0 7989 0
vsize: 32120
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7310 0 0 0 113991 24 0 0 25 0 1 0 481765257 32890880 7281 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8030 7281 603 41 0 7989 0
vsize: 32120
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7312 0 0 0 114991 24 0 0 25 0 1 0 481765257 32890880 7283 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8030 7283 603 41 0 7989 0
vsize: 32120
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7312 0 0 0 115991 24 0 0 25 0 1 0 481765257 32890880 7283 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8030 7283 603 41 0 7989 0
vsize: 32120
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7312 0 0 0 116992 24 0 0 25 0 1 0 481765257 32890880 7283 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8030 7283 603 41 0 7989 0
vsize: 32120
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7312 0 0 0 117992 24 0 0 25 0 1 0 481765257 32890880 7283 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8030 7283 603 41 0 7989 0
vsize: 32120
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7312 0 0 0 118992 24 0 0 25 0 1 0 481765257 32890880 7283 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8030 7283 603 41 0 7989 0
vsize: 32120
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 31328
Raw data (stat): 31328 (minisat+) R 31327 23176 23175 0 -1 0 7317 0 0 0 119992 24 0 0 25 0 1 0 481765257 32890880 7288 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8030 7288 603 41 0 7989 0
vsize: 32120
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 31328
Raw data (stat): 31328 (minisat+) Z 31327 23176 23175 0 -1 12 7320 0 0 0 119992 25 0 0 25 0 1 0 481765257 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.19
CPU user time (s): 1199.93
CPU system time (s): 0.25796
CPU usage (%): 100.01
Max. virtual memory (Kb): 32120
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####