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/submitted/manquinho/primes-dimacs-cnf/normalized-ii32d1.opb
MD5SUM	151e246868267296e134c3c76a3cb289
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	285
Optimality of the best value was proved	NO
Number of terms in the objective function	664
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	664
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	664
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	1.02484
Number of variables	664
Total number of constraints	3035
Number of constraints which are clauses	3035
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	32
Trace number 6252

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        878156 kB
Buffers:         36488 kB
Cached:          97820 kB
SwapCached:       2644 kB
Active:          54556 kB
Inactive:        85304 kB
HighTotal:      131008 kB
HighFree:        29260 kB
LowTotal:       903652 kB
LowFree:        848896 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11096 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:18:23 (client local time) WITH STATUS 10 IN 1200.46 SECONDS
stats: 4667 7 1200.46 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3035 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 |    3035     9828 |    1011       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 319[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30182     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        22 |   75753   179887 |   25251      22      879    40.0 |  0.000 % |
c |       122 |   75691   179749 |   27776     119     6630    55.7 |  0.125 % |
c |       274 |   72917   173408 |   30553     191     9598    50.3 |  3.407 % |
c ==============================================================================
c [1mFound solution: 313[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 |       315 |   73175   174061 |   24391     232    11582    49.9 |  3.407 % |
c |       416 |   73088   173864 |   26830     332    17940    54.0 |  3.498 % |
c |       569 |   73027   173726 |   29513     484    29310    60.6 |  3.567 % |
c |       794 |   69767   166270 |   32464     640    31164    48.7 |  7.481 % |
c |      1131 |   69345   165298 |   35710     956    52304    54.7 |  8.013 % |
c ==============================================================================
c [1mFound solution: 312[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 |      1456 |   68570   163517 |   22856    1275    80411    63.1 |  8.013 % |
c |      1556 |   66326   158344 |   25141    1340    80701    60.2 | 11.809 % |
c |      1706 |   61327   146852 |   27655    1410    80893    57.4 | 18.107 % |
c |      1933 |   55021   132320 |   30421    1470    85310    58.0 | 26.079 % |
c |      2270 |   54573   131285 |   33463    1803   107472    59.6 | 26.491 % |
c |      2776 |   45731   110838 |   36809    1987   115637    58.2 | 37.868 % |
c |      3537 |   42623   103658 |   40490    2689   161146    59.9 | 41.786 % |
c |      4676 |   42283   102873 |   44539    3816   275687    72.2 | 42.209 % |
c ==============================================================================
c [1mFound solution: 311[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 |      4999 |   42341   103023 |   14113    4139   300450    72.6 | 42.209 % |
c |      5099 |   40038    97687 |   15524    4181   301133    72.0 | 45.138 % |
c |      5249 |   39509    96456 |   17076    4323   310941    71.9 | 45.831 % |
c ==============================================================================
c [1mFound solution: 302[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 |      5380 |   39519    96512 |   13173    4431   316806    71.5 | 45.831 % |
c |      5481 |   39519    96512 |   14490    4532   327396    72.2 | 46.001 % |
c |      5632 |   39413    96270 |   15939    4682   345016    73.7 | 46.126 % |
c |      5860 |   39291    95984 |   17533    4909   362995    73.9 | 46.291 % |
c |      6198 |   39291    95984 |   19286    5247   393396    75.0 | 46.291 % |
c |      6704 |   39291    95984 |   21215    5753   440679    76.6 | 46.291 % |
c |      7465 |   39291    95984 |   23336    6514   512843    78.7 | 46.291 % |
c |      8604 |   39168    95698 |   25670    7651   625064    81.7 | 46.456 % |
c |     10313 |   39168    95698 |   28237    9360   786014    84.0 | 46.456 % |
c |     12875 |   36668    89885 |   31061   11820   962644    81.4 | 49.711 % |
c |     16720 |   35792    87851 |   34167   15639  1439761    92.1 | 50.856 % |
c ==============================================================================
c [1mFound solution: 301[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 |     17812 |   35720    87700 |   11906   16723  1509812    90.3 | 50.856 % |
c |     17912 |   35599    87421 |   13096   16822  1520491    90.4 | 51.170 % |
c |     18065 |   35599    87421 |   14406   16975  1526352    89.9 | 51.170 % |
c |     18292 |   35599    87421 |   15846   17202  1540357    89.5 | 51.170 % |
c |     18629 |   35599    87421 |   17431   17539  1561129    89.0 | 51.170 % |
c |     19135 |   35599    87421 |   19174   18045  1585817    87.9 | 51.170 % |
c |     19897 |   35599    87421 |   21092   18807  1638473    87.1 | 51.170 % |
c |     21037 |   35599    87421 |   23201   19947  1725179    86.5 | 51.170 % |
c |     22745 |   35599    87421 |   25521   21655  1851099    85.5 | 51.170 % |
c |     25308 |   34990    86014 |   28073   24204  2051815    84.8 | 51.945 % |
c |     29154 |   28456    70851 |   30881   27765  2297283    82.7 | 60.454 % |
c ==============================================================================
c [1mFound solution: 300[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 |     30359 |   28405    70720 |    9468   28906  2407410    83.3 | 60.454 % |
c |     30459 |   28405    70720 |   10414   13774   892666    64.8 | 60.506 % |
c |     30609 |   28405    70720 |   11456   13924   896511    64.4 | 60.506 % |
c |     30835 |   28405    70720 |   12601   14150   905364    64.0 | 60.506 % |
c |     31172 |   28405    70720 |   13862   14487   932968    64.4 | 60.506 % |
c |     31678 |   28405    70720 |   15248   14993   967091    64.5 | 60.506 % |
c ==============================================================================
c [1mFound solution: 299[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 |     32108 |   28459    70858 |    9486   15423   993277    64.4 | 60.506 % |
c |     32208 |   28459    70858 |   10434   15523   997601    64.3 | 60.474 % |
c |     32358 |   28459    70858 |   11478   15673  1008569    64.4 | 60.474 % |
c |     32586 |   28459    70858 |   12625   15901  1020329    64.2 | 60.474 % |
c ==============================================================================
c [1mFound solution: 298[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 |     32713 |   28402    70702 |    9467   15913  1016183    63.9 | 60.474 % |
c |     32813 |   27800    69310 |   10413   15998  1017375    63.6 | 61.295 % |
c |     32963 |   27600    68847 |   11455   16146  1021221    63.2 | 61.552 % |
c |     33192 |   27600    68847 |   12600   16375  1040376    63.5 | 61.552 % |
c |     33530 |   27470    68543 |   13860   16712  1073281    64.2 | 61.728 % |
c |     34040 |   27340    68237 |   15246   17219  1100828    63.9 | 61.901 % |
c |     34801 |   27340    68237 |   16771   17980  1147505    63.8 | 61.901 % |
c |     35942 |   27214    67941 |   18448   19116  1223470    64.0 | 62.073 % |
c |     37651 |   26588    66485 |   20293   20806  1347229    64.8 | 62.892 % |
c |     40215 |   26452    66167 |   22322   23366  1502043    64.3 | 63.068 % |
c ==============================================================================
c [1mFound solution: 297[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 |     40756 |   26509    66312 |    8836   23907  1551823    64.9 | 63.068 % |
c |     40856 |   26509    66312 |    9719   24007  1555919    64.8 | 63.050 % |
c |     41011 |   26509    66312 |   10691   24162  1565706    64.8 | 63.050 % |
c |     41240 |   26509    66312 |   11760   24391  1585142    65.0 | 63.050 % |
c |     41577 |   26509    66312 |   12936   24728  1611834    65.2 | 63.050 % |
c |     42083 |   26509    66312 |   14230   25234  1662536    65.9 | 63.050 % |
c |     42842 |   26509    66312 |   15653   25993  1735671    66.8 | 63.050 % |
c |     43983 |   26509    66312 |   17218   27134  1835526    67.6 | 63.050 % |
c |     45693 |   26509    66312 |   18940   28844  1925648    66.8 | 63.050 % |
c |     48255 |   26411    66078 |   20834   31402  2120053    67.5 | 63.198 % |
c ==============================================================================
c [1mFound solution: 296[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 |     49960 |   26373    65971 |    8791   32920  2252359    68.4 | 63.198 % |
c ==============================================================================
c [1mFound solution: 295[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 |     49976 |   26319    65855 |    8773   15628   945164    60.5 | 63.198 % |
c |     50079 |   26319    65855 |    9650   15731   955142    60.7 | 63.355 % |
c |     50230 |   26319    65855 |   10615   15882   965893    60.8 | 63.355 % |
c |     50456 |   26319    65855 |   11676   16108   987736    61.3 | 63.355 % |
c |     50795 |   26319    65855 |   12844   16447  1006886    61.2 | 63.355 % |
c |     51302 |   26319    65855 |   14129   16954  1037991    61.2 | 63.355 % |
c |     52063 |   26319    65855 |   15541   17715  1105830    62.4 | 63.355 % |
c |     53202 |   24975    62722 |   17096   18809  1163538    61.9 | 65.080 % |
c |     54911 |   24975    62722 |   18805   20518  1301907    63.5 | 65.080 % |
c |     57473 |   24975    62722 |   20686   23080  1497755    64.9 | 65.080 % |
c |     61319 |   24371    61319 |   22754   26890  1676729    62.4 | 65.873 % |
c ==============================================================================
c [1mFound solution: 294[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 |     61412 |   24321    61185 |    8107   26910  1672856    62.2 | 65.873 % |
c |     61512 |   24058    60579 |    8917   13546   667815    49.3 | 66.248 % |
c |     61663 |   24058    60579 |    9809   13697   670777    49.0 | 66.248 % |
c |     61888 |   24058    60579 |   10790   13922   676545    48.6 | 66.248 % |
c |     62227 |   24058    60579 |   11869   14261   696837    48.9 | 66.248 % |
c |     62733 |   24058    60579 |   13056   14767   729539    49.4 | 66.248 % |
c |     63492 |   24058    60579 |   14362   15526   784039    50.5 | 66.248 % |
c |     64631 |   24058    60579 |   15798   16665   858325    51.5 | 66.248 % |
c |     66340 |   24058    60579 |   17378   18374   990848    53.9 | 66.248 % |
c |     68904 |   24058    60579 |   19115   20938  1139906    54.4 | 66.248 % |
c |     72748 |   23849    60096 |   21027   24425  1430855    58.6 | 66.504 % |
c |     78515 |   23849    60096 |   23130   30192  2002514    66.3 | 66.504 % |
c ==============================================================================
c [1mFound solution: 293[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 |     79810 |   23906    60241 |    7968   31487  2112178    67.1 | 66.504 % |
c |     79912 |   23906    60241 |    8764   15846  1067796    67.4 | 66.479 % |
c |     80062 |   23906    60241 |    9641   15996  1083060    67.7 | 66.479 % |
c |     80287 |   23906    60241 |   10605   16221  1090562    67.2 | 66.479 % |
c |     80627 |   23906    60241 |   11665   16561  1118473    67.5 | 66.479 % |
c |     81133 |   23906    60241 |   12832   17067  1157139    67.8 | 66.479 % |
c |     81893 |   23906    60241 |   14115   17827  1190290    66.8 | 66.479 % |
c |     83032 |   23906    60241 |   15527   18966  1225306    64.6 | 66.479 % |
c |     84740 |   23906    60241 |   17080   20674  1323175    64.0 | 66.479 % |
c |     87302 |   23906    60241 |   18788   23236  1414517    60.9 | 66.479 % |
c ==============================================================================
c [1mFound solution: 292[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 |     88488 |   23856    60108 |    7952   24420  1474440    60.4 | 66.479 % |
c |     88589 |   23856    60108 |    8747   24521  1482277    60.4 | 66.529 % |
c |     88740 |   23856    60108 |    9621   24672  1489562    60.4 | 66.529 % |
c |     88970 |   23856    60108 |   10584   24902  1504730    60.4 | 66.529 % |
c |     89307 |   23856    60108 |   11642   25239  1529286    60.6 | 66.529 % |
c |     89814 |   23856    60108 |   12806   25746  1567599    60.9 | 66.529 % |
c |     90574 |   23856    60108 |   14087   26506  1624471    61.3 | 66.529 % |
c |     91713 |   23856    60108 |   15496   27645  1718708    62.2 | 66.529 % |
c |     93422 |   23856    60108 |   17045   29354  1836776    62.6 | 66.529 % |
c |     95986 |   23856    60108 |   18750   31918  2061179    64.6 | 66.529 % |
c ==============================================================================
c [1mFound solution: 285[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 |     99165 |   24019    60505 |    8006   35097  2186627    62.3 | 66.529 % |
c |     99265 |   24019    60505 |    8806   17469   845969    48.4 | 66.441 % |
c |     99415 |   24019    60505 |    9687   17619   850999    48.3 | 66.441 % |
c |     99641 |   24019    60505 |   10655   17845   860294    48.2 | 66.441 % |
c |     99979 |   24019    60505 |   11721   18183   876691    48.2 | 66.441 % |
c |    100487 |   24019    60505 |   12893   18691   900179    48.2 | 66.441 % |
c |    101246 |   24019    60505 |   14183   19450   951534    48.9 | 66.441 % |
c |    102388 |   24019    60505 |   15601   20592  1013605    49.2 | 66.441 % |
c |    104098 |   24019    60505 |   17161   22302  1099806    49.3 | 66.441 % |
c |    106664 |   24019    60505 |   18877   24868  1239898    49.9 | 66.441 % |
c |    110511 |   24019    60505 |   20765   28715  1467986    51.1 | 66.441 % |
c |    116277 |   24019    60505 |   22842   34481  1828751    53.0 | 66.441 % |
c |    124926 |   24019    60505 |   25126   20677  1007911    48.7 | 66.441 % |
c |    137901 |   24019    60505 |   27638   33652  1505273    44.7 | 66.441 % |
c |    157362 |   24019    60505 |   30402   27702  1253382    45.2 | 66.441 % |
c |    186555 |   24019    60505 |   33443   31439  1360351    43.3 | 66.441 % |
c |    230344 |   23393    59036 |   36787   44516  3496333    78.5 | 67.353 % |
#### 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.90 2/54 2882
Raw data (stat): 2882 (runsolver) R 2881 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423310083 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 2882
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 2592 0 0 0 992 6 0 0 25 0 1 0 423310083 12656640 2517 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3090 2517 603 41 0 3049 0
vsize: 12360
[startup+20.002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 2882
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 2864 0 0 0 1990 8 0 0 25 0 1 0 423310083 13832192 2789 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3377 2789 603 41 0 3336 0
vsize: 13508
[startup+30.0033 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2882
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 3297 0 0 0 2989 9 0 0 25 0 1 0 423310083 15585280 3222 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3805 3222 603 41 0 3764 0
vsize: 15220
[startup+40.0029 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2882
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 3598 0 0 0 3988 10 0 0 25 0 1 0 423310083 16797696 3523 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4101 3523 603 41 0 4060 0
vsize: 16404
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2882
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 3990 0 0 0 4987 11 0 0 25 0 1 0 423310083 18391040 3915 4294967295 134512640 134672761 3221224576 3221223680 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3915 603 41 0 4449 0
vsize: 17960
[startup+60.0035 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2882
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 4267 0 0 0 5987 12 0 0 25 0 1 0 423310083 19587072 4192 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4782 4192 603 41 0 4741 0
vsize: 19128
[startup+70.0044 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2882
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 4496 0 0 0 6986 13 0 0 25 0 1 0 423310083 20533248 4421 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5013 4421 603 41 0 4972 0
vsize: 20052
[startup+80.0108 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2882
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 4730 0 0 0 7986 14 0 0 25 0 1 0 423310083 21458944 4655 4294967295 134512640 134672761 3221224576 3221223680 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5239 4655 603 41 0 5198 0
vsize: 20956
[startup+90.0109 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2882
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 4916 0 0 0 8985 15 0 0 25 0 1 0 423310083 22265856 4841 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5436 4841 603 41 0 5395 0
vsize: 21744
[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2882
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5106 0 0 0 9985 15 0 0 25 0 1 0 423310083 23056384 5031 4294967295 134512640 134672761 3221224576 3221223712 134560598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5629 5031 603 41 0 5588 0
vsize: 22516
[startup+110.012 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 2935
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5181 0 0 0 10985 16 0 0 25 0 1 0 423310083 23322624 5106 4294967295 134512640 134672761 3221224576 3221223712 134560560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5694 5106 603 41 0 5653 0
vsize: 22776
[startup+120.013 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 2935
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5311 0 0 0 11984 16 0 0 25 0 1 0 423310083 23846912 5236 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5822 5236 603 41 0 5781 0
vsize: 23288
[startup+130.013 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 2935
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5311 0 0 0 12985 16 0 0 25 0 1 0 423310083 23846912 5236 4294967295 134512640 134672761 3221224576 3221223680 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5822 5236 603 41 0 5781 0
vsize: 23288
[startup+140.014 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 2935
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5311 0 0 0 13985 16 0 0 25 0 1 0 423310083 23846912 5236 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5822 5236 603 41 0 5781 0
vsize: 23288
[startup+150.015 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 2935
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5311 0 0 0 14986 16 0 0 25 0 1 0 423310083 23846912 5236 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5822 5236 603 41 0 5781 0
vsize: 23288
[startup+160.015 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 2935
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5311 0 0 0 15986 16 0 0 25 0 1 0 423310083 23846912 5236 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5822 5236 603 41 0 5781 0
vsize: 23288
[startup+170.015 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 2935
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5312 0 0 0 16986 16 0 0 25 0 1 0 423310083 23846912 5237 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5822 5237 603 41 0 5781 0
vsize: 23288
[startup+180.015 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 17986 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223532 1075350371 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+190.016 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 18987 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223680 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+200.016 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 19987 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223760 134559356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+210.017 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 20988 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+220.018 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 21988 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+230.018 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 22988 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+240.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 23989 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+250.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 24989 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+260.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 25989 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+270.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 26989 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223680 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+280.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 27990 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+290.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 28990 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+300.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 29990 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+310.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 30991 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+320.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 31991 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+330.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 32991 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+340.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5346 0 0 0 33992 17 0 0 25 0 1 0 423310083 24109056 5271 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5271 603 41 0 5845 0
vsize: 23544
[startup+350.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5351 0 0 0 34992 17 0 0 25 0 1 0 423310083 24109056 5276 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5276 603 41 0 5845 0
vsize: 23544
[startup+360.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5351 0 0 0 35993 17 0 0 25 0 1 0 423310083 24109056 5276 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5276 603 41 0 5845 0
vsize: 23544
[startup+370.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5351 0 0 0 36993 17 0 0 25 0 1 0 423310083 24109056 5276 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5276 603 41 0 5845 0
vsize: 23544
[startup+380.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5351 0 0 0 37993 17 0 0 25 0 1 0 423310083 24109056 5276 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5276 603 41 0 5845 0
vsize: 23544
[startup+390.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5351 0 0 0 38994 17 0 0 25 0 1 0 423310083 24109056 5276 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5276 603 41 0 5845 0
vsize: 23544
[startup+400.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5351 0 0 0 39994 17 0 0 25 0 1 0 423310083 24109056 5276 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5276 603 41 0 5845 0
vsize: 23544
[startup+410.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2937
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5351 0 0 0 40994 17 0 0 25 0 1 0 423310083 24109056 5276 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5276 603 41 0 5845 0
vsize: 23544
[startup+420.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5354 0 0 0 41995 17 0 0 25 0 1 0 423310083 24109056 5279 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5279 603 41 0 5845 0
vsize: 23544
[startup+430.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5386 0 0 0 42995 17 0 0 25 0 1 0 423310083 24244224 5311 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5311 603 41 0 5878 0
vsize: 23676
[startup+440.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5391 0 0 0 43995 17 0 0 25 0 1 0 423310083 24244224 5316 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5316 603 41 0 5878 0
vsize: 23676
[startup+450.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5422 0 0 0 44995 17 0 0 25 0 1 0 423310083 24379392 5347 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5952 5347 603 41 0 5911 0
vsize: 23808
[startup+460.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5436 0 0 0 45996 18 0 0 25 0 1 0 423310083 24543232 5361 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5992 5361 603 41 0 5951 0
vsize: 23968
[startup+470.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5447 0 0 0 46996 18 0 0 25 0 1 0 423310083 24543232 5372 4294967295 134512640 134672761 3221224576 3221223760 134559613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5992 5372 603 41 0 5951 0
vsize: 23968
[startup+480.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5449 0 0 0 47996 18 0 0 25 0 1 0 423310083 24543232 5374 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5992 5374 603 41 0 5951 0
vsize: 23968
[startup+490.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5458 0 0 0 48997 18 0 0 25 0 1 0 423310083 24543232 5383 4294967295 134512640 134672761 3221224576 3221223712 134560720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5992 5383 603 41 0 5951 0
vsize: 23968
[startup+500.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5471 0 0 0 49997 18 0 0 25 0 1 0 423310083 24707072 5396 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6032 5396 603 41 0 5991 0
vsize: 24128
[startup+510.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5478 0 0 0 50998 18 0 0 25 0 1 0 423310083 24707072 5403 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6032 5403 603 41 0 5991 0
vsize: 24128
[startup+520.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5491 0 0 0 51998 18 0 0 25 0 1 0 423310083 24707072 5416 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6032 5416 603 41 0 5991 0
vsize: 24128
[startup+530.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5513 0 0 0 52998 18 0 0 25 0 1 0 423310083 24842240 5438 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6065 5438 603 41 0 6024 0
vsize: 24260
[startup+540.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5519 0 0 0 53998 18 0 0 25 0 1 0 423310083 24842240 5444 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6065 5444 603 41 0 6024 0
vsize: 24260
[startup+550.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5519 0 0 0 54999 18 0 0 25 0 1 0 423310083 24842240 5444 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6065 5444 603 41 0 6024 0
vsize: 24260
[startup+560.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5530 0 0 0 55999 18 0 0 25 0 1 0 423310083 24981504 5455 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6099 5455 603 41 0 6058 0
vsize: 24396
[startup+570.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5553 0 0 0 57000 18 0 0 25 0 1 0 423310083 24981504 5478 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6099 5478 603 41 0 6058 0
vsize: 24396
[startup+580.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5556 0 0 0 58000 18 0 0 25 0 1 0 423310083 25128960 5481 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6135 5481 603 41 0 6094 0
vsize: 24540
[startup+590.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5560 0 0 0 59000 18 0 0 25 0 1 0 423310083 25128960 5485 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6135 5485 603 41 0 6094 0
vsize: 24540
[startup+600.033 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5572 0 0 0 60001 18 0 0 25 0 1 0 423310083 25128960 5497 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6135 5497 603 41 0 6094 0
vsize: 24540
[startup+610.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5573 0 0 0 61001 18 0 0 25 0 1 0 423310083 25128960 5498 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6135 5498 603 41 0 6094 0
vsize: 24540
[startup+620.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5691 0 0 0 62001 18 0 0 25 0 1 0 423310083 25665536 5616 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6266 5616 603 41 0 6225 0
vsize: 25064
[startup+630.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5820 0 0 0 63001 19 0 0 25 0 1 0 423310083 26263552 5745 4294967295 134512640 134672761 3221224576 3221223664 134565768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6412 5745 603 41 0 6371 0
vsize: 25648
[startup+640.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5820 0 0 0 64001 19 0 0 25 0 1 0 423310083 26263552 5745 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6412 5745 603 41 0 6371 0
vsize: 25648
[startup+650.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5831 0 0 0 65002 19 0 0 25 0 1 0 423310083 26263552 5756 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6412 5756 603 41 0 6371 0
vsize: 25648
[startup+660.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5834 0 0 0 66002 19 0 0 25 0 1 0 423310083 26398720 5759 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6445 5759 603 41 0 6404 0
vsize: 25780
[startup+670.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5834 0 0 0 67003 19 0 0 25 0 1 0 423310083 26398720 5759 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6445 5759 603 41 0 6404 0
vsize: 25780
[startup+680.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5834 0 0 0 68003 19 0 0 25 0 1 0 423310083 26398720 5759 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6445 5759 603 41 0 6404 0
vsize: 25780
[startup+690.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5849 0 0 0 69003 19 0 0 25 0 1 0 423310083 26398720 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6445 5774 603 41 0 6404 0
vsize: 25780
[startup+700.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5873 0 0 0 70004 19 0 0 25 0 1 0 423310083 26546176 5798 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5798 603 41 0 6440 0
vsize: 25924
[startup+710.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5873 0 0 0 71004 19 0 0 25 0 1 0 423310083 26546176 5798 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5798 603 41 0 6440 0
vsize: 25924
[startup+720.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5873 0 0 0 72004 19 0 0 25 0 1 0 423310083 26546176 5798 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5798 603 41 0 6440 0
vsize: 25924
[startup+730.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5873 0 0 0 73005 19 0 0 25 0 1 0 423310083 26546176 5798 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5798 603 41 0 6440 0
vsize: 25924
[startup+740.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5873 0 0 0 74005 19 0 0 25 0 1 0 423310083 26546176 5798 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5798 603 41 0 6440 0
vsize: 25924
[startup+750.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5873 0 0 0 75006 19 0 0 25 0 1 0 423310083 26546176 5798 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5798 603 41 0 6440 0
vsize: 25924
[startup+760.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5873 0 0 0 76006 19 0 0 25 0 1 0 423310083 26546176 5798 4294967295 134512640 134672761 3221224576 3221223680 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5798 603 41 0 6440 0
vsize: 25924
[startup+770.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 5910 0 0 0 77006 19 0 0 25 0 1 0 423310083 26681344 5835 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6514 5835 603 41 0 6473 0
vsize: 26056
[startup+780.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 6110 0 0 0 78006 20 0 0 25 0 1 0 423310083 27598848 6035 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6738 6035 603 41 0 6697 0
vsize: 26952
[startup+790.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 6284 0 0 0 79005 21 0 0 25 0 1 0 423310083 28262400 6209 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6900 6209 603 41 0 6859 0
vsize: 27600
[startup+800.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 6475 0 0 0 80005 21 0 0 25 0 1 0 423310083 29061120 6400 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7095 6400 603 41 0 7054 0
vsize: 28380
[startup+810.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 6658 0 0 0 81004 22 0 0 25 0 1 0 423310083 29851648 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7288 6583 603 41 0 7247 0
vsize: 29152
[startup+820.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 6821 0 0 0 82004 23 0 0 25 0 1 0 423310083 30519296 6746 4294967295 134512640 134672761 3221224576 3221223760 134558632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7451 6746 603 41 0 7410 0
vsize: 29804
[startup+830.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 6969 0 0 0 83004 23 0 0 25 0 1 0 423310083 31043584 6894 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7579 6894 603 41 0 7538 0
vsize: 30316
[startup+840.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7117 0 0 0 84004 23 0 0 25 0 1 0 423310083 31715328 7042 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7743 7042 603 41 0 7702 0
vsize: 30972
[startup+850.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7265 0 0 0 85004 24 0 0 25 0 1 0 423310083 32247808 7190 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7873 7190 603 41 0 7832 0
vsize: 31492
[startup+860.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7419 0 0 0 86004 25 0 0 25 0 1 0 423310083 32919552 7344 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8037 7344 603 41 0 7996 0
vsize: 32148
[startup+870.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7542 0 0 0 87003 26 0 0 25 0 1 0 423310083 33452032 7467 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8167 7467 603 41 0 8126 0
vsize: 32668
[startup+880.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7674 0 0 0 88003 26 0 0 25 0 1 0 423310083 33980416 7599 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8296 7599 603 41 0 8255 0
vsize: 33184
[startup+890.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7801 0 0 0 89003 26 0 0 25 0 1 0 423310083 34516992 7726 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7726 603 41 0 8386 0
vsize: 33708
[startup+900.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7869 0 0 0 90003 26 0 0 25 0 1 0 423310083 34779136 7794 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8491 7794 603 41 0 8450 0
vsize: 33964
[startup+910.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7875 0 0 0 91004 26 0 0 25 0 1 0 423310083 34779136 7800 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8491 7800 603 41 0 8450 0
vsize: 33964
[startup+920.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7875 0 0 0 92004 26 0 0 25 0 1 0 423310083 34779136 7800 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8491 7800 603 41 0 8450 0
vsize: 33964
[startup+930.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7875 0 0 0 93005 26 0 0 25 0 1 0 423310083 34779136 7800 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8491 7800 603 41 0 8450 0
vsize: 33964
[startup+940.052 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7889 0 0 0 94005 26 0 0 25 0 1 0 423310083 34918400 7814 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8525 7814 603 41 0 8484 0
vsize: 34100
[startup+950.052 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7889 0 0 0 95005 26 0 0 25 0 1 0 423310083 34918400 7814 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8525 7814 603 41 0 8484 0
vsize: 34100
[startup+960.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7892 0 0 0 96006 26 0 0 25 0 1 0 423310083 34918400 7817 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8525 7817 603 41 0 8484 0
vsize: 34100
[startup+970.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7902 0 0 0 97006 27 0 0 25 0 1 0 423310083 34918400 7827 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8525 7827 603 41 0 8484 0
vsize: 34100
[startup+980.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7906 0 0 0 98006 27 0 0 25 0 1 0 423310083 34918400 7831 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8525 7831 603 41 0 8484 0
vsize: 34100
[startup+990.054 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7928 0 0 0 99007 27 0 0 25 0 1 0 423310083 35065856 7853 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8561 7853 603 41 0 8520 0
vsize: 34244
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7945 0 0 0 100007 27 0 0 25 0 1 0 423310083 35213312 7870 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7870 603 41 0 8556 0
vsize: 34388
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7947 0 0 0 101007 27 0 0 25 0 1 0 423310083 35213312 7872 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7872 603 41 0 8556 0
vsize: 34388
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7951 0 0 0 102008 27 0 0 25 0 1 0 423310083 35213312 7876 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7876 603 41 0 8556 0
vsize: 34388
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7952 0 0 0 103008 27 0 0 25 0 1 0 423310083 35213312 7877 4294967295 134512640 134672761 3221224576 3221223712 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7877 603 41 0 8556 0
vsize: 34388
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7961 0 0 0 104008 27 0 0 25 0 1 0 423310083 35213312 7886 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7886 603 41 0 8556 0
vsize: 34388
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7970 0 0 0 105009 27 0 0 25 0 1 0 423310083 35360768 7895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8633 7895 603 41 0 8592 0
vsize: 34532
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7972 0 0 0 106009 27 0 0 25 0 1 0 423310083 35360768 7897 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8633 7897 603 41 0 8592 0
vsize: 34532
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 7978 0 0 0 107009 27 0 0 25 0 1 0 423310083 35360768 7903 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8633 7903 603 41 0 8592 0
vsize: 34532
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8016 0 0 0 108010 27 0 0 25 0 1 0 423310083 35524608 7941 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7941 603 41 0 8632 0
vsize: 34692
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8017 0 0 0 109010 27 0 0 25 0 1 0 423310083 35524608 7942 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7942 603 41 0 8632 0
vsize: 34692
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8017 0 0 0 110010 27 0 0 25 0 1 0 423310083 35524608 7942 4294967295 134512640 134672761 3221224576 3221223532 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7942 603 41 0 8632 0
vsize: 34692
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8017 0 0 0 111011 27 0 0 25 0 1 0 423310083 35524608 7942 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7942 603 41 0 8632 0
vsize: 34692
[startup+1120.06 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8017 0 0 0 112011 27 0 0 25 0 1 0 423310083 35524608 7942 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7942 603 41 0 8632 0
vsize: 34692
[startup+1130.09 s]
Raw data (loadavg): 1.14 1.01 0.93 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8017 0 0 0 113014 27 0 0 25 0 1 0 423310083 35524608 7942 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7942 603 41 0 8632 0
vsize: 34692
[startup+1140.08 s]
Raw data (loadavg): 1.12 1.01 0.93 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8017 0 0 0 114014 27 0 0 25 0 1 0 423310083 35524608 7942 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7942 603 41 0 8632 0
vsize: 34692
[startup+1150.08 s]
Raw data (loadavg): 1.10 1.01 0.93 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8017 0 0 0 115015 27 0 0 25 0 1 0 423310083 35524608 7942 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7942 603 41 0 8632 0
vsize: 34692
[startup+1160.08 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8017 0 0 0 116015 27 0 0 25 0 1 0 423310083 35524608 7942 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7942 603 41 0 8632 0
vsize: 34692
[startup+1170.08 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8017 0 0 0 117015 27 0 0 25 0 1 0 423310083 35524608 7942 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7942 603 41 0 8632 0
vsize: 34692
[startup+1180.08 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8017 0 0 0 118016 27 0 0 25 0 1 0 423310083 35524608 7942 4294967295 134512640 134672761 3221224576 3221223744 134561278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7942 603 41 0 8632 0
vsize: 34692
[startup+1190.08 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8022 0 0 0 119016 27 0 0 25 0 1 0 423310083 35524608 7947 4294967295 134512640 134672761 3221224576 3221223488 1075352446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8673 7947 603 41 0 8632 0
vsize: 34692
[startup+1200.08 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 2939
Raw data (stat): 2882 (minisat+) R 2881 29653 29652 0 -1 0 8031 0 0 0 120016 27 0 0 25 0 1 0 423310083 35688448 7956 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8713 7956 603 41 0 8672 0
vsize: 34852
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.04 1.01 0.93 1/54 2939
Raw data (stat): 2882 (minisat+) Z 2881 29653 29652 0 -1 12 8034 0 0 0 120017 28 0 0 25 0 1 0 423310083 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.1
CPU time (s): 1200.46
CPU user time (s): 1200.17
CPU system time (s): 0.289955
CPU usage (%): 100.03
Max. virtual memory (Kb): 34852
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####