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/routing/normalized-s4-4-3-2pb.opb
MD5SUM	55739635f7f3741bc4f78c540803ac21
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	64
Optimality of the best value was proved	NO
Number of terms in the objective function	648
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	648
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	648
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.03884
Number of variables	648
Total number of constraints	1952
Number of constraints which are clauses	1928
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	27
Trace number 5190

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-13 22:20:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3622 boxname=wulflinc18 idbench=238 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  55739635f7f3741bc4f78c540803ac21  /oldhome/oroussel/tmp/wulflinc18/normalized-s4-4-3-2pb.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc18/normalized-s4-4-3-2pb.opb /oldhome/oroussel/tmp/wulflinc18/normalized-s4-4-3-2pb.opb
IDLAUNCH: 3622
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        896296 kB
Buffers:         34232 kB
Cached:          68128 kB
SwapCached:        320 kB
Active:          51216 kB
Inactive:        54332 kB
HighTotal:      131008 kB
HighFree:        58856 kB
LowTotal:       903652 kB
LowFree:        837440 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27172 kB
Committed_AS:    63700 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:40:59 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 3622 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1952 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1950]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1924]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1906]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1880]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1862]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1840]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1814]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1808]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1794]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1768]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1746]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1736]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1734]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1708]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1690]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1664]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1662]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1636]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1619]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1593]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1560]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1534]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1532]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1522]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1516]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1498]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1460]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1450]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1436]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1410]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1388]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1378]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1341]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1319]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1313]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1307]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1305]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1279]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1261]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1235]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1186]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1176]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1164]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1154]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1144]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1095]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1093]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1057]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1035]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1029]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1023]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1009]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 984]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 962]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 952]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 915]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 893]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 887]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 881]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 871]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 861]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 811]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 809]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 776]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 750]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 748]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 738]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 736]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 710]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 692]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 666]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 664]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 638]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 620]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 594]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 592]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 566]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 548]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 522]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 520]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 494]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 476]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 450]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 417]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 391]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 389]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 379]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 346]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 320]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 318]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 308]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 260]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 250]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 240]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 238]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 236]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 210]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 192]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 114]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 104]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  98]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  96]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  94]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  68]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  50]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  22]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  21]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  20]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  19]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  18]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  17]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  16]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  15]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  14]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  13]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  12]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  11]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  10]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   9]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   8]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   7]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   6]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   5]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   4]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   3]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   2]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   1]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   0]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8948    30762 |    2982       0        0     nan |  0.000 % |
c |       100 |    8802    30258 |    3280      85      326     3.8 | 20.957 % |
c |       251 |    8677    29839 |    3608     221     1019     4.6 | 22.140 % |
c |       477 |    8376    28840 |    3969     406     2021     5.0 | 25.000 % |
c |       815 |    8089    27901 |    4365     707     3836     5.4 | 27.811 % |
c |      1321 |    7904    27284 |    4802    1190     8800     7.4 | 29.635 % |
c |      2080 |    7825    27025 |    5282    1928    22540    11.7 | 30.375 % |
c |      3220 |    7825    27025 |    5811    3068    57785    18.8 | 30.375 % |
c |      4929 |    7825    27025 |    6392    4777   125938    26.4 | 30.375 % |
c |      7493 |    7785    26891 |    7031    3778   103479    27.4 | 30.769 % |
c |     11339 |    7785    26891 |    7734    7624   198062    26.0 | 30.769 % |
c |     17105 |    7770    26838 |    8507    4929    95860    19.4 | 30.917 % |
c |     25755 |    7583    26207 |    9358    8952   191557    21.4 | 32.347 % |
c |     38729 |    7529    26027 |   10294    6782   153448    22.6 | 32.742 % |
c |     58190 |    7482    25868 |   11324    9650   182328    18.9 | 33.037 % |
c |     87382 |    7416    25654 |   12456    8561   207620    24.3 | 33.679 % |
c |    131171 |    7391    25573 |   13702   12474   288898    23.2 | 33.925 % |
c |    196855 |    7328    25362 |   15072   13005   272842    21.0 | 34.418 % |
c |    295383 |    7328    25362 |   16579    8626   188041    21.8 | 34.418 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1246   maxlim: 558   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    375786 |   15986    56291 |    5328   10973   233647    21.3 | 34.418 % |
c |    375886 |   15986    56291 |    5860    5587   118658    21.2 | 21.653 % |
c |    376038 |   15986    56291 |    6446    5739   121358    21.1 | 21.653 % |
c |    376263 |   15986    56291 |    7091    5964   126104    21.1 | 21.653 % |
c |    376601 |   15986    56291 |    7800    6302   132632    21.0 | 21.653 % |
c |    377109 |   15986    56291 |    8580    6810   144267    21.2 | 21.653 % |
c |    377869 |   15955    56182 |    9438    7565   161402    21.3 | 21.714 % |
c |    379008 |   15955    56182 |   10382    8704   191487    22.0 | 21.714 % |
c |    380716 |   15955    56182 |   11421   10412   236263    22.7 | 21.714 % |
c |    383278 |   15955    56182 |   12563    6869   149435    21.8 | 21.714 % |
c |    387123 |   15955    56182 |   13819   10714   250628    23.4 | 21.714 % |
c |    392891 |   15955    56182 |   15201    9175   196828    21.5 | 21.714 % |
c |    401541 |   15955    56182 |   16721    9747   226433    23.2 | 21.714 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 934   maxlim: 558   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    408958 |   22429    79311 |    7476   17164   470569    27.4 | 21.714 % |
c |    409060 |   22429    79311 |    8223    4393   136579    31.1 | 17.165 % |
c |    409213 |   22429    79311 |    9045    4546   139714    30.7 | 17.165 % |
c |    409440 |   22429    79311 |    9950    4773   143532    30.1 | 17.165 % |
c |    409777 |   22429    79311 |   10945    5110   150664    29.5 | 17.165 % |
c |    410285 |   22429    79311 |   12040    5618   162022    28.8 | 17.165 % |
c |    411044 |   22429    79311 |   13244    6377   180944    28.4 | 17.165 % |
c |    412183 |   22429    79311 |   14568    7516   211113    28.1 | 17.165 % |
c |    413892 |   22429    79311 |   16025    9225   249104    27.0 | 17.165 % |
c |    416455 |   22429    79311 |   17628   11788   301086    25.5 | 17.165 % |
c |    420299 |   22429    79311 |   19390   15632   391297    25.0 | 17.165 % |
c |    426065 |   22429    79311 |   21329   11314   254391    22.5 | 17.165 % |
c |    434714 |   22422    79288 |   23462   19962   460684    23.1 | 17.188 % |
c |    447694 |   22422    79288 |   25809   20817   439298    21.1 | 17.188 % |
c |    467162 |   22366    79096 |   28390   13598   479474    35.3 | 17.330 % |
c |    496356 |   22357    79065 |   31229   27454   916943    33.4 | 17.354 % |
c |    540147 |   22242    78664 |   34352   18008   337139    18.7 | 17.591 % |
c |    605831 |   22207    78535 |   37787   21791   497193    22.8 | 17.662 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1184   maxlim: 552   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    623545 |   30425   107883 |   10141   39505  1104596    28.0 | 17.662 % |
c |    623646 |   30425   107883 |   11155    7538   300927    39.9 | 13.969 % |
c |    623798 |   30425   107883 |   12270    7690   304114    39.5 | 13.969 % |
c |    624023 |   30425   107883 |   13497    7915   308046    38.9 | 13.969 % |
c |    624362 |   30425   107883 |   14847    8254   318778    38.6 | 13.969 % |
c |    624868 |   30425   107883 |   16332    8760   328380    37.5 | 13.969 % |
c |    625630 |   30425   107883 |   17965    9522   351980    37.0 | 13.969 % |
c |    626772 |   30425   107883 |   19761   10664   378254    35.5 | 13.969 % |
c |    628485 |   30377   107713 |   21738   12369   416928    33.7 | 14.043 % |
c |    631047 |   30330   107544 |   23911   14926   471866    31.6 | 14.117 % |
c |    634892 |   30330   107544 |   26303   18771   570076    30.4 | 14.117 % |
c |    640658 |   30330   107544 |   28933   24537   899298    36.7 | 14.117 % |
c |    649308 |   30330   107544 |   31826   18227   578693    31.7 | 14.117 % |
c |    662282 |   30330   107544 |   35009   31201  2122921    68.0 | 14.117 % |
c |    681743 |   30330   107544 |   38510   30372  2875722    94.7 | 14.117 % |
c |    710936 |   30321   107513 |   42361   37901  2896394    76.4 | 14.135 % |
c |    754727 |   30197   107077 |   46597   26062   594071    22.8 | 14.320 % |
c |    820411 |   30128   106828 |   51257   28285  1831606    64.8 | 14.431 % |
c |    918937 |   30096   106708 |   56383   51469  4247112    82.5 | 14.468 % |
c |   1066726 |   30071   106619 |   62021   41409  3278956    79.2 | 14.524 % |
#### 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.86 0.93 0.90 2/55 24519
Raw data (stat): 24519 (runsolver) R 24518 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479499642 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.88 0.93 0.90 2/55 24519
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 909 0 0 0 997 1 0 0 25 0 1 0 479499642 5308416 887 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1296 887 603 41 0 1255 0
vsize: 5184
[startup+20.0006 s]
Raw data (loadavg): 0.90 0.93 0.90 2/55 24519
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1061 0 0 0 1996 2 0 0 25 0 1 0 479499642 5861376 1039 4294967295 134512640 134672761 3221224560 3221223744 134558943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1431 1039 603 41 0 1390 0
vsize: 5724
[startup+30.0019 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 24519
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1175 0 0 0 2995 3 0 0 25 0 1 0 479499642 6406144 1153 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1564 1153 603 41 0 1523 0
vsize: 6256
[startup+40.0024 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 24519
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1345 0 0 0 3994 4 0 0 25 0 1 0 479499642 7077888 1323 4294967295 134512640 134672761 3221224560 3221223664 134554919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1728 1323 603 41 0 1687 0
vsize: 6912
[startup+50.0034 s]
Raw data (loadavg): 0.94 0.94 0.90 2/55 24519
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1377 0 0 0 4993 5 0 0 25 0 1 0 479499642 7217152 1355 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1762 1355 603 41 0 1721 0
vsize: 7048
[startup+60.0037 s]
Raw data (loadavg): 0.95 0.94 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1416 0 0 0 5992 6 0 0 25 0 1 0 479499642 7372800 1394 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1800 1394 603 41 0 1759 0
vsize: 7200
[startup+70.0042 s]
Raw data (loadavg): 0.95 0.94 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1480 0 0 0 6991 7 0 0 25 0 1 0 479499642 7667712 1458 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1872 1458 603 41 0 1831 0
vsize: 7488
[startup+80.0051 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1495 0 0 0 7991 7 0 0 25 0 1 0 479499642 7667712 1473 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1872 1473 603 41 0 1831 0
vsize: 7488
[startup+90.0055 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1516 0 0 0 8990 8 0 0 25 0 1 0 479499642 7815168 1494 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1908 1494 603 41 0 1867 0
vsize: 7632
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1553 0 0 0 9990 8 0 0 25 0 1 0 479499642 7962624 1531 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1944 1531 603 41 0 1903 0
vsize: 7776
[startup+110.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1588 0 0 0 10989 9 0 0 25 0 1 0 479499642 8097792 1566 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1977 1566 603 41 0 1936 0
vsize: 7908
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1695 0 0 0 11989 9 0 0 25 0 1 0 479499642 8708096 1673 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2126 1673 603 41 0 2085 0
vsize: 8504
[startup+130.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1711 0 0 0 12989 9 0 0 25 0 1 0 479499642 8708096 1689 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2126 1689 603 41 0 2085 0
vsize: 8504
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1718 0 0 0 13989 9 0 0 25 0 1 0 479499642 8708096 1696 4294967295 134512640 134672761 3221224560 3221223712 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2126 1696 603 41 0 2085 0
vsize: 8504
[startup+150.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1792 0 0 0 14989 10 0 0 25 0 1 0 479499642 9027584 1770 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2204 1770 603 41 0 2163 0
vsize: 8816
[startup+160.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 1886 0 0 0 15989 10 0 0 25 0 1 0 479499642 9424896 1864 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2301 1864 603 41 0 2260 0
vsize: 9204
[startup+170.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 2141 0 0 0 16988 11 0 0 25 0 1 0 479499642 10723328 2119 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2618 2119 603 41 0 2577 0
vsize: 10472
[startup+180.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 2191 0 0 0 17988 11 0 0 25 0 1 0 479499642 10870784 2169 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2654 2169 603 41 0 2613 0
vsize: 10616
[startup+190.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 2299 0 0 0 18988 12 0 0 25 0 1 0 479499642 11452416 2277 4294967295 134512640 134672761 3221224560 3221223664 134560180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2796 2277 603 41 0 2755 0
vsize: 11184
[startup+200.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 2412 0 0 0 19988 12 0 0 25 0 1 0 479499642 11857920 2390 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2895 2390 603 41 0 2854 0
vsize: 11580
[startup+210.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 2664 0 0 0 20986 13 0 0 25 0 1 0 479499642 12922880 2642 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3155 2642 603 41 0 3114 0
vsize: 12620
[startup+220.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 2796 0 0 0 21985 14 0 0 25 0 1 0 479499642 13488128 2774 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3293 2774 603 41 0 3252 0
vsize: 13172
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 2896 0 0 0 22985 14 0 0 25 0 1 0 479499642 13889536 2874 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3391 2874 603 41 0 3350 0
vsize: 13564
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 2909 0 0 0 23985 14 0 0 25 0 1 0 479499642 13889536 2887 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3391 2887 603 41 0 3350 0
vsize: 13564
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 2954 0 0 0 24985 14 0 0 25 0 1 0 479499642 14229504 2932 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3474 2932 603 41 0 3433 0
vsize: 13896
[startup+260.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 2990 0 0 0 25985 14 0 0 25 0 1 0 479499642 14426112 2968 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3522 2968 603 41 0 3481 0
vsize: 14088
[startup+270.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 3025 0 0 0 26985 15 0 0 25 0 1 0 479499642 14688256 3003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3586 3003 603 41 0 3545 0
vsize: 14344
[startup+280.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 3025 0 0 0 27985 15 0 0 25 0 1 0 479499642 14688256 3003 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3586 3003 603 41 0 3545 0
vsize: 14344
[startup+290.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 3048 0 0 0 28985 15 0 0 25 0 1 0 479499642 14688256 3026 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3586 3026 603 41 0 3545 0
vsize: 14344
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 3076 0 0 0 29986 15 0 0 25 0 1 0 479499642 14835712 3054 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3622 3054 603 41 0 3581 0
vsize: 14488
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 3082 0 0 0 30986 15 0 0 25 0 1 0 479499642 14999552 3060 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3662 3060 603 41 0 3621 0
vsize: 14648
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 3363 0 0 0 31985 15 0 0 25 0 1 0 479499642 16076800 3341 4294967295 134512640 134672761 3221224560 3221223560 1075350365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3925 3341 603 41 0 3884 0
vsize: 15700
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 3374 0 0 0 32985 16 0 0 25 0 1 0 479499642 16076800 3352 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3925 3352 603 41 0 3884 0
vsize: 15700
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 3375 0 0 0 33985 16 0 0 25 0 1 0 479499642 16076800 3353 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3925 3353 603 41 0 3884 0
vsize: 15700
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24521
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 3952 0 0 0 34984 17 0 0 25 0 1 0 479499642 18485248 3930 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 3930 603 41 0 4472 0
vsize: 18052
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 4602 0 0 0 35981 20 0 0 25 0 1 0 479499642 21168128 4580 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5168 4580 603 41 0 5127 0
vsize: 20672
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 4834 0 0 0 36981 21 0 0 25 0 1 0 479499642 22114304 4812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5399 4812 603 41 0 5358 0
vsize: 21596
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 4849 0 0 0 37981 21 0 0 25 0 1 0 479499642 22114304 4827 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5399 4827 603 41 0 5358 0
vsize: 21596
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 5502 0 0 0 38979 23 0 0 25 0 1 0 479499642 24797184 5480 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6054 5480 603 41 0 6013 0
vsize: 24216
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6160 0 0 0 39976 26 0 0 25 0 1 0 479499642 27488256 6138 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6711 6138 603 41 0 6670 0
vsize: 26844
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6475 0 0 0 40976 26 0 0 25 0 1 0 479499642 28827648 6453 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7038 6453 603 41 0 6997 0
vsize: 28152
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6475 0 0 0 41976 26 0 0 25 0 1 0 479499642 28827648 6453 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7038 6453 603 41 0 6997 0
vsize: 28152
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6487 0 0 0 42976 27 0 0 25 0 1 0 479499642 28827648 6465 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7038 6465 603 41 0 6997 0
vsize: 28152
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6501 0 0 0 43976 27 0 0 25 0 1 0 479499642 28979200 6479 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6479 603 41 0 7034 0
vsize: 28300
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6503 0 0 0 44976 27 0 0 25 0 1 0 479499642 28979200 6481 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6482 603 41 0 7034 0
vsize: 28300
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6505 0 0 0 45976 27 0 0 25 0 1 0 479499642 28979200 6483 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6483 603 41 0 7034 0
vsize: 28300
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6511 0 0 0 46976 27 0 0 25 0 1 0 479499642 28979200 6489 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6489 603 41 0 7034 0
vsize: 28300
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6513 0 0 0 47976 27 0 0 25 0 1 0 479499642 28979200 6491 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6491 603 41 0 7034 0
vsize: 28300
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6514 0 0 0 48976 27 0 0 25 0 1 0 479499642 28979200 6492 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6492 603 41 0 7034 0
vsize: 28300
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6516 0 0 0 49977 27 0 0 25 0 1 0 479499642 28979200 6494 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6494 603 41 0 7034 0
vsize: 28300
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6518 0 0 0 50977 27 0 0 25 0 1 0 479499642 28979200 6496 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6496 603 41 0 7034 0
vsize: 28300
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6518 0 0 0 51977 27 0 0 25 0 1 0 479499642 28979200 6496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6496 603 41 0 7034 0
vsize: 28300
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6520 0 0 0 52977 27 0 0 25 0 1 0 479499642 28979200 6498 4294967295 134512640 134672761 3221224560 3221223696 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6498 603 41 0 7034 0
vsize: 28300
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6520 0 0 0 53977 27 0 0 25 0 1 0 479499642 28979200 6498 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6498 603 41 0 7034 0
vsize: 28300
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6520 0 0 0 54977 27 0 0 25 0 1 0 479499642 28979200 6498 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6498 603 41 0 7034 0
vsize: 28300
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6520 0 0 0 55977 28 0 0 25 0 1 0 479499642 28979200 6498 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6498 603 41 0 7034 0
vsize: 28300
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6520 0 0 0 56978 28 0 0 25 0 1 0 479499642 28979200 6498 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6498 603 41 0 7034 0
vsize: 28300
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6521 0 0 0 57978 28 0 0 25 0 1 0 479499642 28979200 6499 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6499 603 41 0 7034 0
vsize: 28300
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6528 0 0 0 58978 28 0 0 25 0 1 0 479499642 28979200 6506 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6506 603 41 0 7034 0
vsize: 28300
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6528 0 0 0 59978 28 0 0 25 0 1 0 479499642 28979200 6506 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6506 603 41 0 7034 0
vsize: 28300
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6529 0 0 0 60978 28 0 0 25 0 1 0 479499642 28979200 6507 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6507 603 41 0 7034 0
vsize: 28300
[startup+620.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6529 0 0 0 61978 28 0 0 25 0 1 0 479499642 28979200 6507 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6507 603 41 0 7034 0
vsize: 28300
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6530 0 0 0 62979 28 0 0 25 0 1 0 479499642 28979200 6508 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6508 603 41 0 7034 0
vsize: 28300
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6530 0 0 0 63979 28 0 0 25 0 1 0 479499642 28979200 6508 4294967295 134512640 134672761 3221224560 3221223744 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6508 603 41 0 7034 0
vsize: 28300
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24523
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6530 0 0 0 64979 28 0 0 25 0 1 0 479499642 28979200 6508 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6508 603 41 0 7034 0
vsize: 28300
[startup+660.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6530 0 0 0 65979 28 0 0 25 0 1 0 479499642 28979200 6508 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6508 603 41 0 7034 0
vsize: 28300
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6530 0 0 0 66979 28 0 0 25 0 1 0 479499642 28979200 6508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6508 603 41 0 7034 0
vsize: 28300
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6530 0 0 0 67979 28 0 0 25 0 1 0 479499642 28979200 6508 4294967295 134512640 134672761 3221224560 3221223728 134560900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7075 6508 603 41 0 7034 0
vsize: 28300
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 6959 0 0 0 68978 29 0 0 25 0 1 0 479499642 30748672 6937 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7507 6937 603 41 0 7466 0
vsize: 30028
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7345 0 0 0 69977 31 0 0 25 0 1 0 479499642 32366592 7323 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7323 603 41 0 7861 0
vsize: 31608
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7354 0 0 0 70977 31 0 0 25 0 1 0 479499642 32366592 7332 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7332 603 41 0 7861 0
vsize: 31608
[startup+720.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7362 0 0 0 71977 31 0 0 25 0 1 0 479499642 32366592 7340 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7340 603 41 0 7861 0
vsize: 31608
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7363 0 0 0 72977 31 0 0 25 0 1 0 479499642 32366592 7341 4294967295 134512640 134672761 3221224560 3221223664 134560231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7341 603 41 0 7861 0
vsize: 31608
[startup+740.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7368 0 0 0 73978 31 0 0 25 0 1 0 479499642 32366592 7346 4294967295 134512640 134672761 3221224560 3221223744 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7346 603 41 0 7861 0
vsize: 31608
[startup+750.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7368 0 0 0 74978 31 0 0 25 0 1 0 479499642 32366592 7346 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7346 603 41 0 7861 0
vsize: 31608
[startup+760.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7368 0 0 0 75978 31 0 0 25 0 1 0 479499642 32366592 7346 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7346 603 41 0 7861 0
vsize: 31608
[startup+770.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7368 0 0 0 76978 31 0 0 25 0 1 0 479499642 32366592 7346 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7346 603 41 0 7861 0
vsize: 31608
[startup+780.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7368 0 0 0 77978 31 0 0 25 0 1 0 479499642 32366592 7346 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7346 603 41 0 7861 0
vsize: 31608
[startup+790.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7368 0 0 0 78978 32 0 0 25 0 1 0 479499642 32366592 7346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7346 603 41 0 7861 0
vsize: 31608
[startup+800.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7370 0 0 0 79979 32 0 0 25 0 1 0 479499642 32366592 7348 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7348 603 41 0 7861 0
vsize: 31608
[startup+810.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7371 0 0 0 80979 32 0 0 25 0 1 0 479499642 32366592 7349 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7349 603 41 0 7861 0
vsize: 31608
[startup+820.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7371 0 0 0 81979 32 0 0 25 0 1 0 479499642 32366592 7349 4294967295 134512640 134672761 3221224560 3221223744 134559342 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7349 603 41 0 7861 0
vsize: 31608
[startup+830.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7371 0 0 0 82979 32 0 0 25 0 1 0 479499642 32366592 7349 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7349 603 41 0 7861 0
vsize: 31608
[startup+840.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7371 0 0 0 83979 32 0 0 25 0 1 0 479499642 32366592 7349 4294967295 134512640 134672761 3221224560 3221223664 134559821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7349 603 41 0 7861 0
vsize: 31608
[startup+850.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7371 0 0 0 84979 32 0 0 25 0 1 0 479499642 32366592 7349 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7349 603 41 0 7861 0
vsize: 31608
[startup+860.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7371 0 0 0 85979 32 0 0 25 0 1 0 479499642 32366592 7349 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7349 603 41 0 7861 0
vsize: 31608
[startup+870.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7371 0 0 0 86980 32 0 0 25 0 1 0 479499642 32366592 7349 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7349 603 41 0 7861 0
vsize: 31608
[startup+880.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7371 0 0 0 87980 32 0 0 25 0 1 0 479499642 32366592 7349 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7902 7349 603 41 0 7861 0
vsize: 31608
[startup+890.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 7759 0 0 0 88978 34 0 0 25 0 1 0 479499642 33980416 7737 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8296 7737 603 41 0 8255 0
vsize: 33184
[startup+900.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8140 0 0 0 89977 35 0 0 25 0 1 0 479499642 35581952 8118 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8687 8118 603 41 0 8646 0
vsize: 34748
[startup+910.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8343 0 0 0 90976 36 0 0 25 0 1 0 479499642 36384768 8321 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8883 8321 603 41 0 8842 0
vsize: 35532
[startup+920.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8343 0 0 0 91976 36 0 0 25 0 1 0 479499642 36384768 8321 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8883 8321 603 41 0 8842 0
vsize: 35532
[startup+930.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8343 0 0 0 92976 36 0 0 25 0 1 0 479499642 36384768 8321 4294967295 134512640 134672761 3221224560 3221223664 134555333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8883 8321 603 41 0 8842 0
vsize: 35532
[startup+940.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8343 0 0 0 93977 36 0 0 25 0 1 0 479499642 36384768 8321 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8883 8321 603 41 0 8842 0
vsize: 35532
[startup+950.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24525
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8356 0 0 0 94977 37 0 0 25 0 1 0 479499642 36528128 8334 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8334 603 41 0 8877 0
vsize: 35672
[startup+960.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8381 0 0 0 95977 37 0 0 25 0 1 0 479499642 36528128 8359 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8359 603 41 0 8877 0
vsize: 35672
[startup+970.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8381 0 0 0 96977 37 0 0 25 0 1 0 479499642 36528128 8359 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8359 603 41 0 8877 0
vsize: 35672
[startup+980.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8381 0 0 0 97977 37 0 0 25 0 1 0 479499642 36528128 8359 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8359 603 41 0 8877 0
vsize: 35672
[startup+990.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8381 0 0 0 98977 37 0 0 25 0 1 0 479499642 36528128 8359 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8359 603 41 0 8877 0
vsize: 35672
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8381 0 0 0 99977 37 0 0 25 0 1 0 479499642 36528128 8359 4294967295 134512640 134672761 3221224560 3221223516 1075349796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8359 603 41 0 8877 0
vsize: 35672
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8381 0 0 0 100977 37 0 0 25 0 1 0 479499642 36528128 8359 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8359 603 41 0 8877 0
vsize: 35672
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8381 0 0 0 101977 37 0 0 25 0 1 0 479499642 36528128 8359 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8359 603 41 0 8877 0
vsize: 35672
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8381 0 0 0 102978 37 0 0 25 0 1 0 479499642 36528128 8359 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8359 603 41 0 8877 0
vsize: 35672
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8381 0 0 0 103978 37 0 0 25 0 1 0 479499642 36528128 8359 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8359 603 41 0 8877 0
vsize: 35672
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8381 0 0 0 104978 37 0 0 25 0 1 0 479499642 36528128 8359 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8359 603 41 0 8877 0
vsize: 35672
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8382 0 0 0 105978 37 0 0 25 0 1 0 479499642 36528128 8360 4294967295 134512640 134672761 3221224560 3221223724 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8360 603 41 0 8877 0
vsize: 35672
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 8801 0 0 0 106978 39 0 0 25 0 1 0 479499642 38260736 8779 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9341 8779 603 41 0 9300 0
vsize: 37364
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 9207 0 0 0 107976 41 0 0 25 0 1 0 479499642 39997440 9185 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9765 9185 603 41 0 9724 0
vsize: 39060
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 9207 0 0 0 108976 41 0 0 25 0 1 0 479499642 39997440 9185 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9765 9185 603 41 0 9724 0
vsize: 39060
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 9207 0 0 0 109976 41 0 0 25 0 1 0 479499642 39997440 9185 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9765 9185 603 41 0 9724 0
vsize: 39060
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 9207 0 0 0 110976 41 0 0 25 0 1 0 479499642 39997440 9185 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9765 9185 603 41 0 9724 0
vsize: 39060
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 9207 0 0 0 111976 41 0 0 25 0 1 0 479499642 39997440 9185 4294967295 134512640 134672761 3221224560 3221223664 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9765 9185 603 41 0 9724 0
vsize: 39060
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 9207 0 0 0 112977 41 0 0 25 0 1 0 479499642 39997440 9185 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9765 9185 603 41 0 9724 0
vsize: 39060
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 9213 0 0 0 113977 41 0 0 25 0 1 0 479499642 39997440 9191 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9765 9191 603 41 0 9724 0
vsize: 39060
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 9214 0 0 0 114977 41 0 0 25 0 1 0 479499642 39997440 9192 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9765 9192 603 41 0 9724 0
vsize: 39060
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 9214 0 0 0 115977 41 0 0 25 0 1 0 479499642 39997440 9192 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9765 9192 603 41 0 9724 0
vsize: 39060
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 9366 0 0 0 116976 42 0 0 25 0 1 0 479499642 40660992 9344 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9927 9344 603 41 0 9886 0
vsize: 39708
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 9789 0 0 0 117975 43 0 0 25 0 1 0 479499642 42414080 9767 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10355 9767 603 41 0 10314 0
vsize: 41420
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 10188 0 0 0 118974 45 0 0 25 0 1 0 479499642 44011520 10166 4294967295 134512640 134672761 3221224560 3221223664 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10745 10166 603 41 0 10704 0
vsize: 42980
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24527
Raw data (stat): 24519 (minisat+) R 24518 20024 20023 0 -1 0 10580 0 0 0 119972 46 0 0 25 0 1 0 479499642 45613056 10558 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11136 10558 603 41 0 11095 0
vsize: 44544
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 24527
Raw data (stat): 24519 (minisat+) Z 24518 20024 20023 0 -1 12 10583 0 0 0 119973 48 0 0 25 0 1 0 479499642 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.09
CPU time (s): 1200.22
CPU user time (s): 1199.73
CPU system time (s): 0.487925
CPU usage (%): 100.011
Max. virtual memory (Kb): 44544
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####