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-1pb.opb
MD5SUM	9f27aad2edb50c2232eec4dba5ec2271
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	62
Optimality of the best value was proved	NO
Number of terms in the objective function	672
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	672
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	672
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.03484
Number of variables	672
Total number of constraints	2028
Number of constraints which are clauses	2004
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	28
Trace number 5188

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-13 22:20:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3621 boxname=wulflinc27 idbench=237 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9f27aad2edb50c2232eec4dba5ec2271  /oldhome/oroussel/tmp/wulflinc27/normalized-s4-4-3-1pb.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc27/normalized-s4-4-3-1pb.opb /oldhome/oroussel/tmp/wulflinc27/normalized-s4-4-3-1pb.opb
IDLAUNCH: 3621
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        873064 kB
Buffers:         33480 kB
Cached:          91200 kB
SwapCached:       3160 kB
Active:          49288 kB
Inactive:        81400 kB
HighTotal:      131008 kB
HighFree:        36316 kB
LowTotal:       903652 kB
LowFree:        836748 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25328 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:40:31 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3621 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2028 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2022]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2004]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1966]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1956]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1954]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1928]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1910]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1885]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1879]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1862]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1824]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1814]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1804]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1794]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1744]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1742]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1728]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1702]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1680]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1670]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1652]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1630]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1605]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1599]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1589]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1579]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1530]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1528]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1510]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1489]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1463]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1457]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1455]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1429]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1411]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1385]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1348]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1326]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1320]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1314]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1265]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1255]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1245]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1243]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1241]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1215]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1198]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1172]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1154]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1132]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1106]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1100]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1063]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1041]---> 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 ---[1019]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1009]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 959]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 957]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 955]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 929]---> 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 ---[ 883]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 857]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 839]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 813]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 811]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 785]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 768]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 742]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 736]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 718]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 680]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 670]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 656]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 630]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 608]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 598]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 592]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 575]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 537]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 527]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 521]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 504]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 466]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 456]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 438]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 416]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 390]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 384]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 370]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 344]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 322]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 312]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 294]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 272]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 246]---> 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 ---[ 212]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 194]---> 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 ---[ 140]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 122]---> 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: 50   maxlim: 24   bits: 5/5
c ---[  22]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  21]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  20]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  19]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  18]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  17]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  16]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  15]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  14]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  13]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  12]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  11]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  10]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   9]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   8]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   7]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   6]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   5]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   4]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   3]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   2]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   1]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   0]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9844    33982 |    3281       0        0     nan |  0.000 % |
c |       100 |    9798    33832 |    3609      92      385     4.2 | 19.504 % |
c |       252 |    9757    33697 |    3970     237     1022     4.3 | 19.814 % |
c |       477 |    9666    33390 |    4367     442     2098     4.7 | 20.523 % |
c |       814 |    9565    33053 |    4803     755     3929     5.2 | 21.188 % |
c |      1321 |    9385    32451 |    5284    1224     7417     6.1 | 22.562 % |
c |      2080 |    9299    32161 |    5812    1958    14542     7.4 | 23.138 % |
c |      3221 |    9218    31888 |    6393    3073    31529    10.3 | 23.715 % |
c |      4932 |    9076    31406 |    7033    4748    57329    12.1 | 24.734 % |
c |      7495 |    9007    31171 |    7736    7289   107471    14.7 | 25.222 % |
c |     11339 |    9007    31171 |    8510    6885   118184    17.2 | 25.222 % |
c |     17105 |    8984    31096 |    9361    7989   133398    16.7 | 25.399 % |
c |     25754 |    8847    30635 |   10297    6415   117806    18.4 | 26.418 % |
c |     38728 |    8745    30287 |   11326    8362   150177    18.0 | 27.172 % |
c |     58189 |    8669    30029 |   12459    9784   178654    18.3 | 27.660 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1338   maxlim: 600   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65163 |   17963    63206 |    5987   10180   162915    16.0 | 27.660 % |
c |     65263 |   17954    63175 |    6585    5184    75117    14.5 | 17.593 % |
c |     65413 |   17954    63175 |    7244    5334    77651    14.6 | 17.593 % |
c |     65639 |   17954    63175 |    7968    5560    81319    14.6 | 17.593 % |
c |     65977 |   17954    63175 |    8765    5898    87088    14.8 | 17.593 % |
c |     66483 |   17954    63175 |    9642    6404    98905    15.4 | 17.593 % |
c |     67242 |   17954    63175 |   10606    7163   113415    15.8 | 17.593 % |
c |     68381 |   17954    63175 |   11666    8302   137543    16.6 | 17.593 % |
c |     70090 |   17938    63123 |   12833   10008   168364    16.8 | 17.676 % |
c |     72652 |   17924    63073 |   14117   12567   223356    17.8 | 17.732 % |
c |     76497 |   17915    63042 |   15528    8987   150863    16.8 | 17.760 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 602   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81331 |   17919    63065 |    5973   13821   241734    17.5 | 17.760 % |
c |     81431 |   17919    63065 |    6570    3556    42622    12.0 | 17.806 % |
c |     81581 |   17919    63065 |    7227    3706    45910    12.4 | 17.806 % |
c |     81807 |   17919    63065 |    7950    3932    50145    12.8 | 17.806 % |
c |     82144 |   17919    63065 |    8745    4269    59269    13.9 | 17.806 % |
c |     82650 |   17919    63065 |    9619    4775    68179    14.3 | 17.806 % |
c |     83409 |   17907    63026 |   10581    5532    85275    15.4 | 17.861 % |
c |     84551 |   17898    62997 |   11639    6673   110525    16.6 | 17.917 % |
c |     86261 |   17898    62997 |   12803    8383   141065    16.8 | 17.917 % |
c |     88823 |   17898    62997 |   14084   10945   191899    17.5 | 17.917 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 604   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90589 |   17902    63019 |    5967   12711   239752    18.9 | 17.917 % |
c |     90691 |   17902    63019 |    6563    6458   109375    16.9 | 17.962 % |
c |     90841 |   17902    63019 |    7220    6608   112323    17.0 | 17.962 % |
c |     91066 |   17902    63019 |    7942    6833   116501    17.0 | 17.962 % |
c |     91403 |   17902    63019 |    8736    7170   122405    17.1 | 17.962 % |
c |     91910 |   17902    63019 |    9609    7677   130270    17.0 | 17.962 % |
c |     92670 |   17902    63019 |   10570    8437   143435    17.0 | 17.962 % |
c |     93809 |   17902    63019 |   11627    9576   163145    17.0 | 17.962 % |
c |     95518 |   17902    63019 |   12790   11285   193027    17.1 | 17.962 % |
c |     98080 |   17902    63019 |   14069    7100   106844    15.0 | 17.962 % |
c |    101924 |   17902    63019 |   15476   10944   173706    15.9 | 17.962 % |
c |    107691 |   17893    62988 |   17024    8619   139533    16.2 | 17.990 % |
c |    116340 |   17884    62957 |   18727   17265   314258    18.2 | 18.018 % |
c |    129314 |   17875    62926 |   20599   10733   262524    24.5 | 18.046 % |
c |    148777 |   17875    62926 |   22659   19531   426960    21.9 | 18.046 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 606   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    158218 |   17877    62943 |    5959   17291   721118    41.7 | 18.046 % |
c |    158319 |   17877    62943 |    6554    4424   209746    47.4 | 18.091 % |
c |    158471 |   17877    62943 |    7210    4576   212608    46.5 | 18.091 % |
c |    158697 |   17877    62943 |    7931    4802   216761    45.1 | 18.091 % |
c |    159037 |   17877    62943 |    8724    5142   223060    43.4 | 18.091 % |
c |    159543 |   17877    62943 |    9597    5648   231720    41.0 | 18.091 % |
c |    160303 |   17877    62943 |   10556    6408   244560    38.2 | 18.091 % |
c |    161445 |   17877    62943 |   11612    7550   263034    34.8 | 18.091 % |
c |    163153 |   17877    62943 |   12773    9258   294959    31.9 | 18.091 % |
c |    165715 |   17877    62943 |   14051   11820   345350    29.2 | 18.091 % |
c |    169559 |   17871    62923 |   15456    8202   128951    15.7 | 18.119 % |
c |    175325 |   17856    62870 |   17001   13966   246179    17.6 | 18.174 % |
c |    183974 |   17847    62841 |   18701   13652   297147    21.8 | 18.230 % |
c |    196948 |   17847    62841 |   20572   16744   671562    40.1 | 18.230 % |
c |    216409 |   17838    62810 |   22629   14527   658505    45.3 | 18.257 % |
c |    245601 |   17829    62779 |   24892   19144  1531431    80.0 | 18.285 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1100   maxlim: 607   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    262809 |   25426    89893 |    8475   23326   557158    23.9 | 18.285 % |
c |    262909 |   25426    89893 |    9322    5932    72031    12.1 | 14.188 % |
c |    263061 |   25426    89893 |   10254    6084    74533    12.3 | 14.188 % |
c |    263286 |   25426    89893 |   11280    6309    77830    12.3 | 14.188 % |
c |    263629 |   25426    89893 |   12408    6652    82740    12.4 | 14.188 % |
c |    264135 |   25426    89893 |   13649    7158    90154    12.6 | 14.188 % |
c |    264895 |   25426    89893 |   15013    7918    99931    12.6 | 14.188 % |
c |    266036 |   25417    89862 |   16515    9055   118482    13.1 | 14.210 % |
c |    267744 |   25417    89862 |   18166   10763   153137    14.2 | 14.210 % |
c |    270306 |   25417    89862 |   19983   13325   195462    14.7 | 14.210 % |
c |    274150 |   25417    89862 |   21981   17169   263145    15.3 | 14.210 % |
c |    279917 |   25409    89832 |   24180   22935   470605    20.5 | 14.231 % |
c |    288567 |   25409    89832 |   26598   18864   913759    48.4 | 14.231 % |
c |    301542 |   25409    89832 |   29257   17325   812586    46.9 | 14.231 % |
c |    321003 |   25409    89832 |   32183   20024  1169605    58.4 | 14.231 % |
c |    350197 |   25394    89781 |   35402   29378   617681    21.0 | 14.274 % |
c |    393986 |   25220    89170 |   38942   12229   231007    18.9 | 14.486 % |
c |    459672 |   25141    88902 |   42836   34925  1409207    40.3 | 14.763 % |
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 860   maxlim: 603   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    520693 |   31094   110156 |   10364   38441  4143399   107.8 | 14.763 % |
c |    520793 |   31094   110156 |   11400    8891   523807    58.9 | 12.619 % |
c |    520944 |   31094   110156 |   12540    9042   526390    58.2 | 12.619 % |
c |    521170 |   31094   110156 |   13794    9268   529569    57.1 | 12.619 % |
c |    521508 |   31094   110156 |   15173    9606   536145    55.8 | 12.619 % |
c |    522015 |   31094   110156 |   16691   10113   546553    54.0 | 12.619 % |
c |    522774 |   31094   110156 |   18360   10872   561774    51.7 | 12.619 % |
c |    523915 |   31085   110125 |   20196   12009   583691    48.6 | 12.637 % |
c |    525625 |   31085   110125 |   22216   13719   660213    48.1 | 12.637 % |
c |    528187 |   31085   110125 |   24437   16281   795726    48.9 | 12.637 % |
c |    532031 |   31085   110125 |   26881   20125   866588    43.1 | 12.637 % |
c |    537800 |   31085   110125 |   29569   25894   979328    37.8 | 12.637 % |
c |    546449 |   31085   110125 |   32526   18736   986894    52.7 | 12.637 % |
c |    559423 |   31070   110074 |   35779   31693  1540164    48.6 | 12.673 % |
c |    578887 |   31070   110074 |   39357   29948  2047523    68.4 | 12.673 % |
c |    608079 |   31048   110002 |   43293   34936  3116958    89.2 | 12.745 % |
c |    651868 |   31032   109948 |   47622   25690  2126980    82.8 | 12.781 % |
c |    717554 |   31032   109948 |   52384   26341  2612453    99.2 | 12.781 % |
c |    816080 |   31032   109948 |   57622   52195  5060747    97.0 | 12.781 % |
#### 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.88 0.96 0.90 2/54 21974
Raw data (stat): 21974 (runsolver) R 21973 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479502122 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.0008 s]
Raw data (loadavg): 0.90 0.96 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 904 0 0 0 996 2 0 0 25 0 1 0 479502122 5341184 882 4294967295 134512640 134672761 3221224560 3221223740 134556590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1304 882 603 41 0 1263 0
vsize: 5216
[startup+20.0013 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 994 0 0 0 1995 2 0 0 25 0 1 0 479502122 5611520 972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1370 972 603 41 0 1329 0
vsize: 5480
[startup+30.0019 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 1263 0 0 0 2993 4 0 0 25 0 1 0 479502122 6778880 1241 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1655 1241 603 41 0 1614 0
vsize: 6620
[startup+40.0015 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 1377 0 0 0 3993 4 0 0 25 0 1 0 479502122 7200768 1355 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1758 1355 603 41 0 1717 0
vsize: 7032
[startup+50.0027 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 1612 0 0 0 4993 5 0 0 25 0 1 0 479502122 8306688 1590 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2028 1590 603 41 0 1987 0
vsize: 8112
[startup+60.0025 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 1680 0 0 0 5992 5 0 0 25 0 1 0 479502122 8601600 1658 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2100 1658 603 41 0 2059 0
vsize: 8400
[startup+70.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 1961 0 0 0 6990 6 0 0 25 0 1 0 479502122 9666560 1939 4294967295 134512640 134672761 3221224560 3221223716 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2360 1939 603 41 0 2319 0
vsize: 9440
[startup+80.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 1963 0 0 0 7990 6 0 0 25 0 1 0 479502122 9666560 1941 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2360 1941 603 41 0 2319 0
vsize: 9440
[startup+90.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 2279 0 0 0 8989 8 0 0 25 0 1 0 479502122 10993664 2257 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2684 2257 603 41 0 2643 0
vsize: 10736
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 2625 0 0 0 9988 9 0 0 25 0 1 0 479502122 12460032 2603 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3042 2603 603 41 0 3001 0
vsize: 12168
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 2736 0 0 0 10988 9 0 0 25 0 1 0 479502122 12861440 2714 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3140 2714 603 41 0 3099 0
vsize: 12560
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 3398 0 0 0 11986 11 0 0 25 0 1 0 479502122 15544320 3376 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3795 3376 603 41 0 3754 0
vsize: 15180
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 3621 0 0 0 12986 12 0 0 25 0 1 0 479502122 16490496 3599 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4026 3599 603 41 0 3985 0
vsize: 16104
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4148 0 0 0 13984 14 0 0 25 0 1 0 479502122 18624512 4126 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4547 4126 603 41 0 4506 0
vsize: 18188
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4148 0 0 0 14984 14 0 0 25 0 1 0 479502122 18624512 4126 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4547 4126 603 41 0 4506 0
vsize: 18188
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4187 0 0 0 15984 14 0 0 25 0 1 0 479502122 18821120 4165 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4595 4165 603 41 0 4554 0
vsize: 18380
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4187 0 0 0 16984 14 0 0 25 0 1 0 479502122 18821120 4165 4294967295 134512640 134672761 3221224560 3221223744 134558771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4595 4165 603 41 0 4554 0
vsize: 18380
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4187 0 0 0 17985 14 0 0 25 0 1 0 479502122 18821120 4165 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4595 4165 603 41 0 4554 0
vsize: 18380
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4190 0 0 0 18985 14 0 0 25 0 1 0 479502122 18821120 4168 4294967295 134512640 134672761 3221224560 3221223748 134554700 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4595 4168 603 41 0 4554 0
vsize: 18380
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4190 0 0 0 19985 14 0 0 25 0 1 0 479502122 18821120 4168 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4595 4168 603 41 0 4554 0
vsize: 18380
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4193 0 0 0 20985 14 0 0 25 0 1 0 479502122 18821120 4171 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4595 4171 603 41 0 4554 0
vsize: 18380
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4193 0 0 0 21985 14 0 0 25 0 1 0 479502122 18821120 4171 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4595 4171 603 41 0 4554 0
vsize: 18380
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4227 0 0 0 22985 14 0 0 25 0 1 0 479502122 19083264 4205 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4205 603 41 0 4618 0
vsize: 18636
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4231 0 0 0 23985 14 0 0 25 0 1 0 479502122 19083264 4209 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4209 603 41 0 4618 0
vsize: 18636
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4232 0 0 0 24986 14 0 0 25 0 1 0 479502122 19083264 4210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4210 603 41 0 4618 0
vsize: 18636
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4234 0 0 0 25986 14 0 0 25 0 1 0 479502122 19083264 4212 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4212 603 41 0 4618 0
vsize: 18636
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4234 0 0 0 26986 14 0 0 25 0 1 0 479502122 19083264 4212 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4212 603 41 0 4618 0
vsize: 18636
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4234 0 0 0 27986 14 0 0 25 0 1 0 479502122 19083264 4212 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4212 603 41 0 4618 0
vsize: 18636
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4241 0 0 0 28986 14 0 0 25 0 1 0 479502122 19083264 4219 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4219 603 41 0 4618 0
vsize: 18636
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4242 0 0 0 29987 14 0 0 25 0 1 0 479502122 19083264 4220 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4220 603 41 0 4618 0
vsize: 18636
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4242 0 0 0 30987 14 0 0 25 0 1 0 479502122 19083264 4220 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4220 603 41 0 4618 0
vsize: 18636
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4242 0 0 0 31987 14 0 0 25 0 1 0 479502122 19083264 4220 4294967295 134512640 134672761 3221224560 3221223684 134566133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4220 603 41 0 4618 0
vsize: 18636
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4242 0 0 0 32987 14 0 0 25 0 1 0 479502122 19083264 4220 4294967295 134512640 134672761 3221224560 3221223712 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4220 603 41 0 4618 0
vsize: 18636
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4242 0 0 0 33987 14 0 0 25 0 1 0 479502122 19083264 4220 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4220 603 41 0 4618 0
vsize: 18636
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4443 0 0 0 34987 15 0 0 25 0 1 0 479502122 19881984 4421 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4854 4421 603 41 0 4813 0
vsize: 19416
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4660 0 0 0 35987 15 0 0 25 0 1 0 479502122 20811776 4638 4294967295 134512640 134672761 3221224560 3221223560 1075349811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5081 4638 603 41 0 5040 0
vsize: 20324
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 4666 0 0 0 36987 15 0 0 25 0 1 0 479502122 20811776 4644 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5081 4644 603 41 0 5040 0
vsize: 20324
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 5073 0 0 0 37986 17 0 0 25 0 1 0 479502122 22544384 5051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5504 5051 603 41 0 5463 0
vsize: 22016
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 5615 0 0 0 38985 18 0 0 25 0 1 0 479502122 24813568 5593 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6058 5593 603 41 0 6017 0
vsize: 24232
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6244 0 0 0 39983 20 0 0 25 0 1 0 479502122 27344896 6222 4294967295 134512640 134672761 3221224560 3221223664 134560483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6676 6222 603 41 0 6635 0
vsize: 26704
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6783 0 0 0 40981 22 0 0 25 0 1 0 479502122 29491200 6761 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7200 6761 603 41 0 7159 0
vsize: 28800
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6895 0 0 0 41981 22 0 0 25 0 1 0 479502122 30019584 6873 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6873 603 41 0 7288 0
vsize: 29316
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6896 0 0 0 42981 22 0 0 25 0 1 0 479502122 30019584 6874 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6874 603 41 0 7288 0
vsize: 29316
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6896 0 0 0 43981 22 0 0 25 0 1 0 479502122 30019584 6874 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6874 603 41 0 7288 0
vsize: 29316
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6897 0 0 0 44981 22 0 0 25 0 1 0 479502122 30019584 6875 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6875 603 41 0 7288 0
vsize: 29316
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 45981 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 46981 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 47981 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223664 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 48981 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 49981 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 50981 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 51981 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 52982 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 53982 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 54982 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 55982 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 56982 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 57982 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 58983 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 59983 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223744 134559613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 60983 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 61983 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 62984 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 63984 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 64984 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 65984 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 66984 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 67984 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223744 134559609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 68985 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 69985 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6929 0 0 0 70985 23 0 0 25 0 1 0 479502122 30019584 6907 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6907 603 41 0 7288 0
vsize: 29316
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 6993 0 0 0 71985 23 0 0 25 0 1 0 479502122 30281728 6971 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7393 6971 603 41 0 7352 0
vsize: 29572
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 7463 0 0 0 72983 25 0 0 25 0 1 0 479502122 32296960 7441 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7885 7441 603 41 0 7844 0
vsize: 31540
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 7629 0 0 0 73983 25 0 0 25 0 1 0 479502122 32960512 7607 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8047 7607 603 41 0 8006 0
vsize: 32188
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 7629 0 0 0 74983 25 0 0 25 0 1 0 479502122 32960512 7607 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8047 7607 603 41 0 8006 0
vsize: 32188
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 7629 0 0 0 75984 25 0 0 25 0 1 0 479502122 32960512 7607 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8047 7607 603 41 0 8006 0
vsize: 32188
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 7633 0 0 0 76984 25 0 0 25 0 1 0 479502122 32960512 7611 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8047 7611 603 41 0 8006 0
vsize: 32188
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 7634 0 0 0 77984 25 0 0 25 0 1 0 479502122 32960512 7612 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8047 7612 603 41 0 8006 0
vsize: 32188
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 7634 0 0 0 78984 25 0 0 25 0 1 0 479502122 32960512 7612 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8047 7612 603 41 0 8006 0
vsize: 32188
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 7634 0 0 0 79985 25 0 0 25 0 1 0 479502122 32960512 7612 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8047 7612 603 41 0 8006 0
vsize: 32188
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 7808 0 0 0 80984 26 0 0 25 0 1 0 479502122 33636352 7786 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8212 7786 603 41 0 8171 0
vsize: 32848
[startup+820.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8187 0 0 0 81983 27 0 0 25 0 1 0 479502122 35229696 8165 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8601 8165 603 41 0 8560 0
vsize: 34404
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8352 0 0 0 82983 27 0 0 25 0 1 0 479502122 35893248 8330 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8330 603 41 0 8722 0
vsize: 35052
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8352 0 0 0 83984 27 0 0 25 0 1 0 479502122 35893248 8330 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8330 603 41 0 8722 0
vsize: 35052
[startup+850.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8352 0 0 0 84983 27 0 0 25 0 1 0 479502122 35893248 8330 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8763 8330 603 41 0 8722 0
vsize: 35052
[startup+860.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8352 0 0 0 85983 27 0 0 25 0 1 0 479502122 35893248 8330 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8763 8330 603 41 0 8722 0
vsize: 35052
[startup+870.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8354 0 0 0 86983 28 0 0 25 0 1 0 479502122 35893248 8332 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8332 603 41 0 8722 0
vsize: 35052
[startup+880.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8354 0 0 0 87983 28 0 0 25 0 1 0 479502122 35893248 8332 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8332 603 41 0 8722 0
vsize: 35052
[startup+890.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8354 0 0 0 88983 28 0 0 25 0 1 0 479502122 35893248 8332 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8332 603 41 0 8722 0
vsize: 35052
[startup+900.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8354 0 0 0 89983 28 0 0 25 0 1 0 479502122 35893248 8332 4294967295 134512640 134672761 3221224560 3221223744 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8332 603 41 0 8722 0
vsize: 35052
[startup+910.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8354 0 0 0 90983 28 0 0 25 0 1 0 479502122 35893248 8332 4294967295 134512640 134672761 3221224560 3221223744 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8332 603 41 0 8722 0
vsize: 35052
[startup+920.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8354 0 0 0 91984 28 0 0 25 0 1 0 479502122 35893248 8332 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8332 603 41 0 8722 0
vsize: 35052
[startup+930.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8354 0 0 0 92984 28 0 0 25 0 1 0 479502122 35893248 8332 4294967295 134512640 134672761 3221224560 3221223664 134555130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8332 603 41 0 8722 0
vsize: 35052
[startup+940.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8354 0 0 0 93984 28 0 0 25 0 1 0 479502122 35893248 8332 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8332 603 41 0 8722 0
vsize: 35052
[startup+950.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8355 0 0 0 94984 28 0 0 25 0 1 0 479502122 35893248 8333 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8333 603 41 0 8722 0
vsize: 35052
[startup+960.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8355 0 0 0 95984 28 0 0 25 0 1 0 479502122 35893248 8333 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8333 603 41 0 8722 0
vsize: 35052
[startup+970.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8355 0 0 0 96984 28 0 0 25 0 1 0 479502122 35893248 8333 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8333 603 41 0 8722 0
vsize: 35052
[startup+980.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8355 0 0 0 97985 28 0 0 25 0 1 0 479502122 35893248 8333 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8333 603 41 0 8722 0
vsize: 35052
[startup+990.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8355 0 0 0 98985 28 0 0 25 0 1 0 479502122 35893248 8333 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8333 603 41 0 8722 0
vsize: 35052
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8355 0 0 0 99985 28 0 0 25 0 1 0 479502122 35893248 8333 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8333 603 41 0 8722 0
vsize: 35052
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8355 0 0 0 100985 28 0 0 25 0 1 0 479502122 35893248 8333 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8333 603 41 0 8722 0
vsize: 35052
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8355 0 0 0 101985 28 0 0 25 0 1 0 479502122 35893248 8333 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8333 603 41 0 8722 0
vsize: 35052
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8355 0 0 0 102986 28 0 0 25 0 1 0 479502122 35893248 8333 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8333 603 41 0 8722 0
vsize: 35052
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8360 0 0 0 103985 28 0 0 25 0 1 0 479502122 35893248 8338 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 8338 603 41 0 8722 0
vsize: 35052
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8420 0 0 0 104985 28 0 0 25 0 1 0 479502122 36163584 8398 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 8398 603 41 0 8788 0
vsize: 35316
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8420 0 0 0 105985 28 0 0 25 0 1 0 479502122 36163584 8398 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 8398 603 41 0 8788 0
vsize: 35316
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8420 0 0 0 106985 28 0 0 25 0 1 0 479502122 36163584 8398 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 8398 603 41 0 8788 0
vsize: 35316
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8420 0 0 0 107986 28 0 0 25 0 1 0 479502122 36163584 8398 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 8398 603 41 0 8788 0
vsize: 35316
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8420 0 0 0 108985 28 0 0 25 0 1 0 479502122 36163584 8398 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 8398 603 41 0 8788 0
vsize: 35316
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8420 0 0 0 109986 28 0 0 25 0 1 0 479502122 36163584 8398 4294967295 134512640 134672761 3221224560 3221223664 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 8398 603 41 0 8788 0
vsize: 35316
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8420 0 0 0 110986 28 0 0 25 0 1 0 479502122 36163584 8398 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 8398 603 41 0 8788 0
vsize: 35316
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8421 0 0 0 111986 28 0 0 25 0 1 0 479502122 36163584 8399 4294967295 134512640 134672761 3221224560 3221223760 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 8399 603 41 0 8788 0
vsize: 35316
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8422 0 0 0 112986 28 0 0 25 0 1 0 479502122 36163584 8400 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 8400 603 41 0 8788 0
vsize: 35316
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 8669 0 0 0 113985 29 0 0 25 0 1 0 479502122 37101568 8647 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9058 8647 603 41 0 9017 0
vsize: 36232
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 9090 0 0 0 114985 30 0 0 25 0 1 0 479502122 38834176 9068 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9481 9068 603 41 0 9440 0
vsize: 37924
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 9452 0 0 0 115984 31 0 0 25 0 1 0 479502122 40431616 9430 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9871 9430 603 41 0 9830 0
vsize: 39484
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 9808 0 0 0 116983 32 0 0 25 0 1 0 479502122 41758720 9786 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10195 9786 603 41 0 10154 0
vsize: 40780
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 10007 0 0 0 117983 32 0 0 25 0 1 0 479502122 42590208 9985 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10398 9985 603 41 0 10357 0
vsize: 41592
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 10007 0 0 0 118983 32 0 0 25 0 1 0 479502122 42590208 9985 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10398 9985 603 41 0 10357 0
vsize: 41592
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21974
Raw data (stat): 21974 (minisat+) R 21973 18865 18864 0 -1 0 10007 0 0 0 119983 32 0 0 25 0 1 0 479502122 42590208 9985 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10398 9985 603 41 0 10357 0
vsize: 41592
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 21974
Raw data (stat): 21974 (minisat+) Z 21973 18865 18864 0 -1 12 10010 0 0 0 119983 34 0 0 25 0 1 0 479502122 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.18
CPU user time (s): 1199.84
CPU system time (s): 0.347947
CPU usage (%): 100.01
Max. virtual memory (Kb): 41592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####