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-6pb.opb
MD5SUM	c12951e903009dc00793ce72594cf3ba
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	66
Optimality of the best value was proved	NO
Number of terms in the objective function	624
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	624
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	624
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.03684
Number of variables	624
Total number of constraints	1884
Number of constraints which are clauses	1860
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	26
Trace number 5191

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-13 22:22:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3626 boxname=wulflinc8 idbench=242 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c12951e903009dc00793ce72594cf3ba  /oldhome/oroussel/tmp/wulflinc8/normalized-s4-4-3-6pb.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-s4-4-3-6pb.opb /oldhome/oroussel/tmp/wulflinc8/normalized-s4-4-3-6pb.opb
IDLAUNCH: 3626
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        909508 kB
Buffers:         36720 kB
Cached:          69156 kB
SwapCached:          0 kB
Active:          72440 kB
Inactive:        36288 kB
HighTotal:      131008 kB
HighFree:        58016 kB
LowTotal:       903652 kB
LowFree:        851492 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            10868 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:41:18 (client local time) WITH STATUS 30 IN 1124.04 SECONDS
stats: 3626 0 1124.04 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1884 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1882]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1856]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1838]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1812]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1798]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1772]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1750]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1740]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1726]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1700]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1678]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1668]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1666]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1640]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1622]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1596]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1578]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1556]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1530]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1524]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1514]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1504]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1454]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1452]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1450]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1424]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1407]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1381]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1363]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1342]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1316]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1310]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1300]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1290]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1240]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1238]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1189]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1179]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1169]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1167]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1165]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1139]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1121]---> 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 ---[1067]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1049]---> 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 ---[ 983]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 961]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 951]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 933]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 911]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 885]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 879]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 877]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 851]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 833]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 807]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 789]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 767]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 741]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 735]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 733]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 707]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 689]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 663]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 657]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 639]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 601]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 591]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 585]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 567]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 529]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 519]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 483]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 461]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 455]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 449]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 397]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 387]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 381]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 379]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 373]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 355]---> 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 ---[ 298]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 289]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 239]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 237]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 188]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 178]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 168]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 117]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 107]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  97]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  95]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  46]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  36]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  26]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  22]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  21]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  20]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  19]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  18]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  17]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  16]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  15]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  14]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  13]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  12]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  11]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[  10]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[   9]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[   8]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[   7]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[   6]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[   5]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[   4]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[   3]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[   2]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[   1]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[   0]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9212    31856 |    3070       0        0     nan |  0.000 % |
c |       100 |    9184    31764 |    3377      92      302     3.3 | 19.508 % |
c |       250 |    9121    31557 |    3714     226      831     3.7 | 19.981 % |
c |       475 |    9078    31410 |    4086     434     1788     4.1 | 20.218 % |
c |       812 |    9029    31249 |    4494     756     3483     4.6 | 20.597 % |
c |      1319 |    8949    30977 |    4944    1239     7710     6.2 | 21.070 % |
c |      2078 |    8940    30946 |    5438    1994    17172     8.6 | 21.117 % |
c |      3218 |    8875    30731 |    5982    3117    33251    10.7 | 21.591 % |
c |      4926 |    8789    30444 |    6580    4787    61867    12.9 | 22.206 % |
c |      7489 |    8731    30251 |    7238    3730    64092    17.2 | 22.585 % |
c |     11333 |    8706    30166 |    7962    7563   179977    23.8 | 22.727 % |
c |     17101 |    8630    29910 |    8759    4569    71512    15.7 | 23.153 % |
c |     25750 |    8455    29318 |    9634    8417   145577    17.3 | 24.195 % |
c |     38724 |    8377    29058 |   10598    6032    90559    15.0 | 24.763 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1210   maxlim: 536   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50018 |   16734    58897 |    5578    6118    96827    15.8 | 24.763 % |
c |     50122 |   16734    58897 |    6135    3163    36491    11.5 | 16.150 % |
c |     50273 |   16734    58897 |    6749    3314    39153    11.8 | 16.150 % |
c |     50500 |   16734    58897 |    7424    3541    44653    12.6 | 16.150 % |
c |     50837 |   16711    58822 |    8166    3870    52798    13.6 | 16.271 % |
c |     51343 |   16711    58822 |    8983    4376    64792    14.8 | 16.271 % |
c |     52103 |   16649    58606 |    9881    5129    82909    16.2 | 16.421 % |
c |     53242 |   16649    58606 |   10869    6268   108062    17.2 | 16.421 % |
c |     54954 |   16649    58606 |   11956    7980   151841    19.0 | 16.421 % |
c |     57518 |   16642    58582 |   13152   10542   231265    21.9 | 16.451 % |
c |     61363 |   16626    58530 |   14467    7476   133524    17.9 | 16.541 % |
c |     67130 |   16590    58405 |   15914   13230   255604    19.3 | 16.692 % |
c |     75780 |   16408    57783 |   17506   13576   216002    15.9 | 17.293 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 890   maxlim: 526   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76155 |   22564    79769 |    7521   13951   223416    16.0 | 17.293 % |
c |     76256 |   22555    79738 |    8273    7074   104538    14.8 | 13.913 % |
c |     76407 |   22555    79738 |    9100    7225   107951    14.9 | 13.913 % |
c |     76633 |   22555    79738 |   10010    7451   111458    15.0 | 13.913 % |
c |     76971 |   22555    79738 |   11011    7789   116312    14.9 | 13.913 % |
c |     77478 |   22555    79738 |   12112    8296   128858    15.5 | 13.913 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 528   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78120 |   22561    79766 |    7520    8938   141797    15.9 | 13.913 % |
c |     78221 |   22483    79495 |    8272    4566    54890    12.0 | 14.144 % |
c |     78371 |   22483    79495 |    9099    4716    58366    12.4 | 14.144 % |
c |     78596 |   22483    79495 |   10009    4941    65309    13.2 | 14.144 % |
c |     78933 |   22483    79495 |   11010    5278    83541    15.8 | 14.144 % |
c |     79439 |   22483    79495 |   12111    5784    94735    16.4 | 14.144 % |
c |     80199 |   22483    79495 |   13322    6544   113667    17.4 | 14.144 % |
c |     81338 |   22469    79450 |   14654    7681   167312    21.8 | 14.215 % |
c |     83047 |   22462    79427 |   16119    9388   281557    30.0 | 14.238 % |
c |     85609 |   22444    79367 |   17731   11946   351026    29.4 | 14.309 % |
c |     89455 |   22375    79128 |   19504   14889   508827    34.2 | 14.499 % |
c |     95221 |   22360    79075 |   21455   10527   413123    39.2 | 14.523 % |
c |    103870 |   22349    79036 |   23600   19174  1217916    63.5 | 14.570 % |
c |    116844 |   22335    78989 |   25961   19812   946494    47.8 | 14.617 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 902   maxlim: 524   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127627 |   28535   101133 |    9511   17264  1134483    65.7 | 14.617 % |
c |    127727 |   28535   101133 |   10462    8732   544507    62.4 | 12.271 % |
c |    127879 |   28535   101133 |   11508    8884   546933    61.6 | 12.271 % |
c |    128104 |   28535   101133 |   12659    9109   550931    60.5 | 12.271 % |
c |    128442 |   28535   101133 |   13925    9447   574018    60.8 | 12.271 % |
c |    128948 |   28535   101133 |   15317    9953   597425    60.0 | 12.271 % |
c |    129707 |   28519   101073 |   16849   10708   620566    58.0 | 12.290 % |
c |    130847 |   28519   101073 |   18534   11848   735475    62.1 | 12.290 % |
c |    132556 |   28519   101073 |   20387   13557   872510    64.4 | 12.290 % |
c |    135121 |   28519   101073 |   22426   16122  1131769    70.2 | 12.290 % |
c |    138965 |   28519   101073 |   24669   19966  1346890    67.5 | 12.290 % |
c |    144732 |   28510   101042 |   27135   25730  2017044    78.4 | 12.310 % |
c |    153381 |   28510   101042 |   29849   20435  1649333    80.7 | 12.310 % |
c |    166355 |   28510   101042 |   32834   17673  1641660    92.9 | 12.310 % |
c |    185816 |   28457   100851 |   36118   18310  1855946   101.4 | 12.368 % |
c |    215008 |   28310   100341 |   39729   26219  1974542    75.3 | 12.622 % |
c |    258798 |   28295   100290 |   43702   26083  3080111   118.1 | 12.661 % |
c |    324482 |   28214   100010 |   48073   36351  4704119   129.4 | 12.817 % |
c |    423009 |   28190    99927 |   52880   48018  5830456   121.4 | 12.895 % |
c ==============================================================================
c [1mOptimal solution: 66[0m
s OPTIMUM FOUND
v v1 v2 v3 -v4 -v5 -v6 -v7 -v8 -v9 -v10 -v11 -v12 -v13 -v14 -v15 -v16 -v17 -v18 -v19 -v20 -v21 -v22 -v23 -v24 -v25 -v26 -v27 -v28 -v29 -v30 -v31 -v32 -v33 -v34 -v35 v36 -v37 -v38 -v39 -v40 -v41 -v42 -v43 -v44 -v45 -v46 -v47 v48 -v49 -v50 -v51 -v52 -v53 -v54 -v55 -v56 -v57 -v58 -v59 v60 -v61 -v62 -v63 -v64 -v65 -v66 -v67 -v68 -v69 -v70 -v71 -v72 -v73 -v74 -v75 -v76 -v77 -v78 -v79 -v80 v81 -v82 v83 -v84 -v85 -v86 -v87 v88 -v89 -v90 -v91 v92 -v93 -v94 v95 -v96 -v97 v98 v99 -v100 -v101 -v102 -v103 -v104 -v105 -v106 -v107 -v108 -v109 -v110 -v111 -v112 -v113 -v114 -v115 -v116 -v117 -v118 -v119 -v120 -v121 -v122 -v123 -v124 -v125 -v126 v127 v128 v129 -v130 -v131 -v132 -v133 -v134 -v135 -v136 v137 -v138 -v139 -v140 -v141 -v142 -v143 v144 -v145 -v146 -v147 -v148 -v149 -v150 -v151 -v152 -v153 -v154 -v155 v156 -v157 -v158 -v159 -v160 -v161 -v162 v163 -v164 -v165 -v166 v167 -v168 -v169 -v170 -v171 -v172 -v173 -v174 -v175 -v176 -v177 -v178 -v179 -v180 -v181 v182 -v183 -v184 -v185 v186 -v187 -v188 -v189 -v190 -v191 -v192 -v193 -v194 -v195 v196 v197 v198 -v199 -v200 -v201 -v202 -v203 -v204 v205 -v206 -v207 -v208 -v209 -v210 -v211 -v212 -v213 -v214 -v215 -v216 -v217 -v218 -v219 -v220 -v221 -v222 -v223 -v224 -v225 v226 v227 -v228 -v229 -v230 -v231 -v232 -v233 -v234 v235 -v236 -v237 -v238 v239 -v240 -v241 -v242 -v243 -v244 -v245 -v246 -v247 -v248 -v249 -v250 -v251 -v252 v253 -v254 -v255 -v256 v257 -v258 -v259 -v260 v261 -v262 -v263 -v264 v265 -v266 -v267 -v268 v269 -v270 -v271 -v272 v273 -v274 -v275 -v276 -v277 v278 -v279 -v280 -v281 -v282 v283 -v284 -v285 -v286 -v287 v288 -v289 -v290 -v291 -v292 -v293 -v294 -v295 -v296 -v297 v298 v299 -v300 -v301 -v302 -v303 -v304 v305 -v306 -v307 -v308 v309 -v310 -v311 -v312 -v313 -v314 -v315 -v316 -v317 -v318 v319 -v320 -v321 -v322 -v323 -v324 -v325 v326 -v327 -v328 -v329 v330 -v331 -v332 -v333 -v334 -v335 -v336 -v337 -v338 -v339 v340 -v341 -v342 -v343 -v344 -v345 -v346 -v347 -v348 v349 -v350 -v351 -v352 -v353 v354 -v355 -v356 -v357 v358 -v359 -v360 -v361 -v362 -v363 -v364 -v365 -v366 -v367 -v368 -v369 v370 -v371 -v372 -v373 -v374 -v375 -v376 -v377 -v378 -v379 -v380 v381 -v382 -v383 -v384 v385 v386 v387 -v388 -v389 -v390 -v391 -v392 -v393 -v394 -v395 -v396 -v397 -v398 -v399 -v400 -v401 -v402 -v403 -v404 -v405 -v406 -v407 -v408 -v409 -v410 -v411 -v412 -v413 -v414 -v415 -v416 -v417 -v418 -v419 -v420 -v421 -v422 -v423 -v424 -v425 -v426 -v427 v428 -v429 -v430 -v431 -v432 -v433 -v434 -v435 -v436 -v437 -v438 -v439 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 -v451 v452 -v453 -v454 -v455 -v456 -v457 -v458 -v459 -v460 -v461 -v462 -v463 v464 -v465 -v466 -v467 -v468 -v469 -v470 -v471 -v472 -v473 -v474 -v475 -v476 -v477 -v478 -v479 -v480 -v481 -v482 -v483 -v484 v485 -v486 -v487 -v488 -v489 -v490 -v491 -v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 -v502 -v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 v511 v512 -v513 -v514 -v515 -v516 -v517 -v518 -v519 -v520 -v521 -v522 -v523 -v524 -v525 -v526 -v527 -v528 -v529 -v530 -v531 v532 -v533 -v534 -v535 -v536 -v537 -v538 -v539 -v540 -v541 -v542 -v543 -v544 -v545 -v546 -v547 -v548 -v549 -v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 -v559 -v560 -v561 -v562 -v563 -v564 -v565 -v566 v567 -v568 -v569 -v570 -v571 -v572 -v573 -v574 -v575 -v576 -v577 -v578 -v579 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v590 v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 -v610 -v611 -v612 -v613 -v614 v615 -v616 -v617 -v618 -v619 -v620 -v621 -v622 -v623 -v624
c _______________________________________________________________________________
c 
c restarts              : 66
c conflicts             : 520995         (464 /sec)
c decisions             : 965631         (859 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1123.78 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.92 2/54 30092
Raw data (stat): 30092 (runsolver) R 30091 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 407731079 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.88 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 847 0 0 0 997 1 0 0 25 0 1 0 407731079 5087232 825 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1242 825 603 41 0 1201 0
vsize: 4968
[startup+20.0017 s]
Raw data (loadavg): 0.89 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 1033 0 0 0 1996 1 0 0 25 0 1 0 407731079 5877760 1011 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1435 1011 603 41 0 1394 0
vsize: 5740
[startup+30.0024 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 1276 0 0 0 2995 2 0 0 25 0 1 0 407731079 6868992 1254 4294967295 134512640 134672761 3221224560 3221219920 134526924 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1254 603 41 0 1636 0
vsize: 6708
[startup+40.0026 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 1732 0 0 0 3993 4 0 0 25 0 1 0 407731079 8855552 1710 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2162 1710 603 41 0 2121 0
vsize: 8648
[startup+50.0031 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 1979 0 0 0 4992 4 0 0 25 0 1 0 407731079 9924608 1957 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2423 1957 603 41 0 2382 0
vsize: 9692
[startup+60.0035 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 2617 0 0 0 5989 7 0 0 25 0 1 0 407731079 12468224 2595 4294967295 134512640 134672761 3221224560 3221223716 134559752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3044 2595 603 41 0 3003 0
vsize: 12176
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 2901 0 0 0 6989 7 0 0 25 0 1 0 407731079 13676544 2879 4294967295 134512640 134672761 3221224560 3221223792 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3339 2879 603 41 0 3298 0
vsize: 13356
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 2903 0 0 0 7989 7 0 0 25 0 1 0 407731079 13676544 2881 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3339 2881 603 41 0 3298 0
vsize: 13356
[startup+90.0039 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 2945 0 0 0 8990 7 0 0 25 0 1 0 407731079 13856768 2923 4294967295 134512640 134672761 3221224560 3221223664 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3383 2923 603 41 0 3342 0
vsize: 13532
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 2945 0 0 0 9990 7 0 0 25 0 1 0 407731079 13856768 2923 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3383 2923 603 41 0 3342 0
vsize: 13532
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 3441 0 0 0 10989 9 0 0 25 0 1 0 407731079 15872000 3419 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3875 3419 603 41 0 3834 0
vsize: 15500
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 3544 0 0 0 11989 9 0 0 25 0 1 0 407731079 16269312 3522 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3972 3522 603 41 0 3931 0
vsize: 15888
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 3544 0 0 0 12989 9 0 0 25 0 1 0 407731079 16269312 3522 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3972 3522 603 41 0 3931 0
vsize: 15888
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 3882 0 0 0 13987 10 0 0 25 0 1 0 407731079 17588224 3860 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4294 3860 603 41 0 4253 0
vsize: 17176
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 4367 0 0 0 14987 11 0 0 25 0 1 0 407731079 19582976 4345 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4345 603 41 0 4740 0
vsize: 19124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 4392 0 0 0 15987 11 0 0 25 0 1 0 407731079 19714048 4370 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4813 4370 603 41 0 4772 0
vsize: 19252
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 4392 0 0 0 16987 11 0 0 25 0 1 0 407731079 19714048 4370 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4813 4370 603 41 0 4772 0
vsize: 19252
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 4499 0 0 0 17987 12 0 0 25 0 1 0 407731079 20115456 4477 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4911 4477 603 41 0 4870 0
vsize: 19644
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5080 0 0 0 18986 13 0 0 25 0 1 0 407731079 22638592 5058 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5527 5058 603 41 0 5486 0
vsize: 22108
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5226 0 0 0 19986 13 0 0 25 0 1 0 407731079 23302144 5204 4294967295 134512640 134672761 3221224560 3221223744 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5689 5204 603 41 0 5648 0
vsize: 22756
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5226 0 0 0 20986 13 0 0 25 0 1 0 407731079 23302144 5204 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5689 5204 603 41 0 5648 0
vsize: 22756
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5229 0 0 0 21986 13 0 0 25 0 1 0 407731079 23302144 5207 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5689 5207 603 41 0 5648 0
vsize: 22756
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5230 0 0 0 22986 13 0 0 25 0 1 0 407731079 23285760 5208 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5685 5208 603 41 0 5644 0
vsize: 22740
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5230 0 0 0 23987 13 0 0 25 0 1 0 407731079 23285760 5208 4294967295 134512640 134672761 3221224560 3221223744 134559592 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5685 5208 603 41 0 5644 0
vsize: 22740
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5230 0 0 0 24987 13 0 0 25 0 1 0 407731079 23285760 5208 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5685 5208 603 41 0 5644 0
vsize: 22740
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5230 0 0 0 25987 13 0 0 25 0 1 0 407731079 23285760 5208 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5685 5208 603 41 0 5644 0
vsize: 22740
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5230 0 0 0 26987 13 0 0 25 0 1 0 407731079 23285760 5208 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5685 5208 603 41 0 5644 0
vsize: 22740
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5230 0 0 0 27987 13 0 0 25 0 1 0 407731079 23285760 5208 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5685 5208 603 41 0 5644 0
vsize: 22740
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5515 0 0 0 28986 14 0 0 25 0 1 0 407731079 24346624 5493 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5944 5493 603 41 0 5903 0
vsize: 23776
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5515 0 0 0 29987 14 0 0 25 0 1 0 407731079 24346624 5493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5944 5493 603 41 0 5903 0
vsize: 23776
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5515 0 0 0 30987 14 0 0 25 0 1 0 407731079 24346624 5493 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5944 5493 603 41 0 5903 0
vsize: 23776
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5525 0 0 0 31987 14 0 0 25 0 1 0 407731079 24481792 5503 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5977 5503 603 41 0 5936 0
vsize: 23908
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5528 0 0 0 32987 14 0 0 25 0 1 0 407731079 24481792 5506 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5977 5506 603 41 0 5936 0
vsize: 23908
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 5648 0 0 0 33987 15 0 0 25 0 1 0 407731079 25014272 5626 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6107 5626 603 41 0 6066 0
vsize: 24428
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6033 0 0 0 34986 16 0 0 25 0 1 0 407731079 26611712 6011 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6497 6011 603 41 0 6456 0
vsize: 25988
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6363 0 0 0 35985 17 0 0 25 0 1 0 407731079 27926528 6341 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6818 6341 603 41 0 6777 0
vsize: 27272
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6634 0 0 0 36984 18 0 0 25 0 1 0 407731079 28979200 6612 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6612 603 41 0 7034 0
vsize: 28300
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6634 0 0 0 37985 18 0 0 25 0 1 0 407731079 28979200 6612 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6612 603 41 0 7034 0
vsize: 28300
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6634 0 0 0 38985 18 0 0 25 0 1 0 407731079 28979200 6612 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6612 603 41 0 7034 0
vsize: 28300
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6634 0 0 0 39984 18 0 0 25 0 1 0 407731079 28979200 6612 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6612 603 41 0 7034 0
vsize: 28300
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6635 0 0 0 40985 18 0 0 25 0 1 0 407731079 28979200 6613 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6613 603 41 0 7034 0
vsize: 28300
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6638 0 0 0 41985 18 0 0 25 0 1 0 407731079 28979200 6616 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6616 603 41 0 7034 0
vsize: 28300
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6639 0 0 0 42985 18 0 0 25 0 1 0 407731079 28979200 6617 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6617 603 41 0 7034 0
vsize: 28300
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6639 0 0 0 43985 18 0 0 25 0 1 0 407731079 28979200 6617 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6617 603 41 0 7034 0
vsize: 28300
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6639 0 0 0 44985 18 0 0 25 0 1 0 407731079 28979200 6617 4294967295 134512640 134672761 3221224560 3221223664 134559784 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6617 603 41 0 7034 0
vsize: 28300
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6640 0 0 0 45986 18 0 0 25 0 1 0 407731079 28979200 6618 4294967295 134512640 134672761 3221224560 3221223732 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6618 603 41 0 7034 0
vsize: 28300
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6640 0 0 0 46986 18 0 0 25 0 1 0 407731079 28979200 6618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6618 603 41 0 7034 0
vsize: 28300
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6640 0 0 0 47986 18 0 0 25 0 1 0 407731079 28979200 6618 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6618 603 41 0 7034 0
vsize: 28300
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6640 0 0 0 48986 18 0 0 25 0 1 0 407731079 28979200 6618 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6618 603 41 0 7034 0
vsize: 28300
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6640 0 0 0 49987 18 0 0 25 0 1 0 407731079 28979200 6618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6618 603 41 0 7034 0
vsize: 28300
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6640 0 0 0 50987 18 0 0 25 0 1 0 407731079 28979200 6618 4294967295 134512640 134672761 3221224560 3221223664 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6618 603 41 0 7034 0
vsize: 28300
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6640 0 0 0 51987 18 0 0 25 0 1 0 407731079 28979200 6618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6618 603 41 0 7034 0
vsize: 28300
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6640 0 0 0 52987 18 0 0 25 0 1 0 407731079 28979200 6618 4294967295 134512640 134672761 3221224560 3221223724 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6618 603 41 0 7034 0
vsize: 28300
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6640 0 0 0 53987 18 0 0 25 0 1 0 407731079 28979200 6618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6618 603 41 0 7034 0
vsize: 28300
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6641 0 0 0 54988 18 0 0 25 0 1 0 407731079 28979200 6619 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6619 603 41 0 7034 0
vsize: 28300
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6641 0 0 0 55988 18 0 0 25 0 1 0 407731079 28979200 6619 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6619 603 41 0 7034 0
vsize: 28300
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6643 0 0 0 56988 18 0 0 25 0 1 0 407731079 28979200 6621 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7075 6621 603 41 0 7034 0
vsize: 28300
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6648 0 0 0 57988 18 0 0 25 0 1 0 407731079 29122560 6626 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7110 6626 603 41 0 7069 0
vsize: 28440
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 6983 0 0 0 58986 20 0 0 25 0 1 0 407731079 30449664 6961 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7434 6961 603 41 0 7393 0
vsize: 29736
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7307 0 0 0 59985 21 0 0 25 0 1 0 407731079 31764480 7285 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7755 7285 603 41 0 7714 0
vsize: 31020
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7508 0 0 0 60985 22 0 0 25 0 1 0 407731079 32550912 7486 4294967295 134512640 134672761 3221224560 3221223516 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7947 7486 603 41 0 7906 0
vsize: 31788
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7508 0 0 0 61985 22 0 0 25 0 1 0 407731079 32550912 7486 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7947 7486 603 41 0 7906 0
vsize: 31788
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7508 0 0 0 62985 22 0 0 25 0 1 0 407731079 32550912 7486 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7947 7486 603 41 0 7906 0
vsize: 31788
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7508 0 0 0 63985 22 0 0 25 0 1 0 407731079 32550912 7486 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7947 7486 603 41 0 7906 0
vsize: 31788
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7508 0 0 0 64985 22 0 0 25 0 1 0 407731079 32550912 7486 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7947 7486 603 41 0 7906 0
vsize: 31788
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7508 0 0 0 65986 22 0 0 25 0 1 0 407731079 32550912 7486 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7947 7486 603 41 0 7906 0
vsize: 31788
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7508 0 0 0 66986 22 0 0 25 0 1 0 407731079 32550912 7486 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7947 7486 603 41 0 7906 0
vsize: 31788
[startup+680.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7513 0 0 0 67986 22 0 0 25 0 1 0 407731079 32550912 7491 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7947 7491 603 41 0 7906 0
vsize: 31788
[startup+690.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7513 0 0 0 68986 22 0 0 25 0 1 0 407731079 32550912 7491 4294967295 134512640 134672761 3221224560 3221223744 134559613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7947 7491 603 41 0 7906 0
vsize: 31788
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7523 0 0 0 69986 22 0 0 25 0 1 0 407731079 32698368 7501 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7983 7501 603 41 0 7942 0
vsize: 31932
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7530 0 0 0 70987 22 0 0 25 0 1 0 407731079 32698368 7508 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7983 7508 603 41 0 7942 0
vsize: 31932
[startup+720.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7537 0 0 0 71987 22 0 0 25 0 1 0 407731079 32698368 7515 4294967295 134512640 134672761 3221224560 3221223744 134559599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7983 7515 603 41 0 7942 0
vsize: 31932
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7537 0 0 0 72987 22 0 0 25 0 1 0 407731079 32698368 7515 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7983 7515 603 41 0 7942 0
vsize: 31932
[startup+740.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7537 0 0 0 73987 22 0 0 25 0 1 0 407731079 32698368 7515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7983 7515 603 41 0 7942 0
vsize: 31932
[startup+750.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7537 0 0 0 74987 22 0 0 25 0 1 0 407731079 32698368 7515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7983 7515 603 41 0 7942 0
vsize: 31932
[startup+760.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7537 0 0 0 75987 22 0 0 25 0 1 0 407731079 32698368 7515 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7983 7515 603 41 0 7942 0
vsize: 31932
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7537 0 0 0 76988 22 0 0 25 0 1 0 407731079 32698368 7515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7983 7515 603 41 0 7942 0
vsize: 31932
[startup+780.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7537 0 0 0 77988 22 0 0 25 0 1 0 407731079 32698368 7515 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7983 7515 603 41 0 7942 0
vsize: 31932
[startup+790.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7553 0 0 0 78988 22 0 0 25 0 1 0 407731079 32829440 7531 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8015 7531 603 41 0 7974 0
vsize: 32060
[startup+800.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 7996 0 0 0 79988 23 0 0 25 0 1 0 407731079 34562048 7974 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8438 7974 603 41 0 8397 0
vsize: 33752
[startup+810.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8382 0 0 0 80986 24 0 0 25 0 1 0 407731079 36139008 8360 4294967295 134512640 134672761 3221224560 3221223556 1075351210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8823 8360 603 41 0 8782 0
vsize: 35292
[startup+820.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8383 0 0 0 81987 24 0 0 25 0 1 0 407731079 36139008 8361 4294967295 134512640 134672761 3221224560 3221223728 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8823 8361 603 41 0 8782 0
vsize: 35292
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8388 0 0 0 82988 24 0 0 25 0 1 0 407731079 36282368 8366 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8366 603 41 0 8817 0
vsize: 35432
[startup+840.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8388 0 0 0 83989 24 0 0 25 0 1 0 407731079 36282368 8366 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8366 603 41 0 8817 0
vsize: 35432
[startup+850.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8389 0 0 0 84989 24 0 0 25 0 1 0 407731079 36282368 8367 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8367 603 41 0 8817 0
vsize: 35432
[startup+860.053 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8389 0 0 0 85990 24 0 0 25 0 1 0 407731079 36282368 8367 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8367 603 41 0 8817 0
vsize: 35432
[startup+870.053 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8389 0 0 0 86990 24 0 0 25 0 1 0 407731079 36282368 8367 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8367 603 41 0 8817 0
vsize: 35432
[startup+880.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8389 0 0 0 87990 24 0 0 25 0 1 0 407731079 36282368 8367 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8367 603 41 0 8817 0
vsize: 35432
[startup+890.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8389 0 0 0 88990 24 0 0 25 0 1 0 407731079 36282368 8367 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8367 603 41 0 8817 0
vsize: 35432
[startup+900.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8405 0 0 0 89990 24 0 0 25 0 1 0 407731079 36282368 8383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8383 603 41 0 8817 0
vsize: 35432
[startup+910.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8416 0 0 0 90990 24 0 0 25 0 1 0 407731079 36282368 8394 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8394 603 41 0 8817 0
vsize: 35432
[startup+920.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8416 0 0 0 91990 24 0 0 25 0 1 0 407731079 36282368 8394 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8394 603 41 0 8817 0
vsize: 35432
[startup+930.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8416 0 0 0 92990 24 0 0 25 0 1 0 407731079 36282368 8394 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8394 603 41 0 8817 0
vsize: 35432
[startup+940.056 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8417 0 0 0 93990 24 0 0 25 0 1 0 407731079 36282368 8395 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8395 603 41 0 8817 0
vsize: 35432
[startup+950.056 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8421 0 0 0 94990 24 0 0 25 0 1 0 407731079 36282368 8399 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8399 603 41 0 8817 0
vsize: 35432
[startup+960.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8421 0 0 0 95991 24 0 0 25 0 1 0 407731079 36282368 8399 4294967295 134512640 134672761 3221224560 3221223744 134558715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8399 603 41 0 8817 0
vsize: 35432
[startup+970.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8421 0 0 0 96991 24 0 0 25 0 1 0 407731079 36282368 8399 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8399 603 41 0 8817 0
vsize: 35432
[startup+980.058 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8421 0 0 0 97991 24 0 0 25 0 1 0 407731079 36282368 8399 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8399 603 41 0 8817 0
vsize: 35432
[startup+990.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8421 0 0 0 98991 24 0 0 25 0 1 0 407731079 36282368 8399 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8399 603 41 0 8817 0
vsize: 35432
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8421 0 0 0 99992 24 0 0 25 0 1 0 407731079 36282368 8399 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8399 603 41 0 8817 0
vsize: 35432
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8421 0 0 0 100992 24 0 0 25 0 1 0 407731079 36282368 8399 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8399 603 41 0 8817 0
vsize: 35432
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8421 0 0 0 101992 24 0 0 25 0 1 0 407731079 36282368 8399 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8399 603 41 0 8817 0
vsize: 35432
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8421 0 0 0 102992 24 0 0 25 0 1 0 407731079 36282368 8399 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8399 603 41 0 8817 0
vsize: 35432
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8421 0 0 0 103992 24 0 0 25 0 1 0 407731079 36282368 8399 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8399 603 41 0 8817 0
vsize: 35432
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8425 0 0 0 104993 24 0 0 25 0 1 0 407731079 36282368 8403 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8403 603 41 0 8817 0
vsize: 35432
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8426 0 0 0 105993 24 0 0 25 0 1 0 407731079 36282368 8404 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8404 603 41 0 8817 0
vsize: 35432
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8426 0 0 0 106993 24 0 0 25 0 1 0 407731079 36282368 8404 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8404 603 41 0 8817 0
vsize: 35432
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8426 0 0 0 107993 24 0 0 25 0 1 0 407731079 36282368 8404 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8404 603 41 0 8817 0
vsize: 35432
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8426 0 0 0 108994 24 0 0 25 0 1 0 407731079 36282368 8404 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8404 603 41 0 8817 0
vsize: 35432
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8426 0 0 0 109994 24 0 0 25 0 1 0 407731079 36282368 8404 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8404 603 41 0 8817 0
vsize: 35432
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8426 0 0 0 110994 24 0 0 25 0 1 0 407731079 36282368 8404 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8404 603 41 0 8817 0
vsize: 35432
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8426 0 0 0 111994 24 0 0 25 0 1 0 407731079 36282368 8404 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8404 603 41 0 8817 0
vsize: 35432
[startup+1123.92 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 30092
Raw data (stat): 30092 (minisat+) R 30091 26667 26666 0 -1 0 8426 0 0 0 111994 24 0 0 25 0 1 0 407731079 36282368 8404 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8858 8404 603 41 0 8817 0
vsize: 0

Child status: 30
Real time (s): 1123.92
CPU time (s): 1124.04
CPU user time (s): 1123.78
CPU system time (s): 0.263959
CPU usage (%): 100.011
Max. virtual memory (Kb): 35432
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	66
#### END VERIFIER DATA ####