PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.5:100.opb
MD5SUM	dd81121db7c1c4b8597dd9571c707a87
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3
Optimality of the best value was proved	NO
Number of terms in the objective function	372
Biggest coefficient in the objective function	220
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	983
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	220
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	983
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	372
Total number of constraints	792
Number of constraints which are clauses	345
Number of constraints which are cardinality constraints (but not clauses)	447
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	18
Trace number 5287

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-13 23:17:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3750 boxname=wulflinc28 idbench=366 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  dd81121db7c1c4b8597dd9571c707a87  /oldhome/oroussel/tmp/wulflinc28/normalized-10:10:4.5:0.5:100.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc28/normalized-10:10:4.5:0.5:100.opb /oldhome/oroussel/tmp/wulflinc28/normalized-10:10:4.5:0.5:100.opb
IDLAUNCH: 3750
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        896700 kB
Buffers:         34476 kB
Cached:          67792 kB
SwapCached:          4 kB
Active:          51128 kB
Inactive:        54048 kB
HighTotal:      131008 kB
HighFree:        59500 kB
LowTotal:       903652 kB
LowFree:        837200 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27320 kB
Committed_AS:    63512 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:37:12 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 3750 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 420 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................
c ---[  85]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  82]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  73]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  72]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  71]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  70]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  69]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  68]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  67]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  66]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  65]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  64]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  63]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  62]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  61]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  60]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  59]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  58]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  57]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  56]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  54]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  53]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  52]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  51]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  49]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  48]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  47]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  46]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  45]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  44]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  43]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  42]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  41]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[  40]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  39]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  38]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  37]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  36]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  35]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  34]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  33]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  32]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  31]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  30]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  29]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  28]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  27]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  25]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  23]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  22]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  21]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  20]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  19]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  18]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  16]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  15]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  14]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  13]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  11]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  10]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[   7]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   3]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6041    20862 |    2013       0        0     nan |  0.000 % |
c |       100 |    6041    20862 |    2214     100      506     5.1 |  9.164 % |
c ==============================================================================
c [1mFound solution: 76[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 870   maxlim: 467   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       147 |   12095    42473 |    4031     147      719     4.9 |  9.164 % |
c |       247 |   12095    42473 |    4434     247     2821    11.4 |  5.997 % |
c |       397 |   12095    42473 |    4877     397     3528     8.9 |  5.997 % |
c ==============================================================================
c [1mFound solution: 71[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 472   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       530 |   12109    42540 |    4036     530     4283     8.1 |  5.997 % |
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 488   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       584 |   12117    42583 |    4039     584     4558     7.8 |  5.997 % |
c ==============================================================================
c [1mFound solution: 54[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 489   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       601 |   12118    42593 |    4039     601     4704     7.8 |  5.997 % |
c |       701 |   12118    42593 |    4442     701     5258     7.5 |  6.226 % |
c |       851 |   12118    42593 |    4887     851     6009     7.1 |  6.226 % |
c |      1076 |   12118    42593 |    5375    1076     9095     8.5 |  6.226 % |
c |      1414 |   12118    42593 |    5913    1414    17273    12.2 |  6.226 % |
c |      1921 |   12118    42593 |    6504    1921    34697    18.1 |  6.226 % |
c |      2680 |   12118    42593 |    7155    2680    58201    21.7 |  6.226 % |
c ==============================================================================
c [1mFound solution: 46[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 497   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3256 |   12120    42610 |    4040    3256    69807    21.4 |  6.226 % |
c |      3356 |   12120    42610 |    4444    3356    70677    21.1 |  6.305 % |
c |      3507 |   12120    42610 |    4888    3507    73247    20.9 |  6.305 % |
c |      3733 |   12120    42610 |    5377    3733    79879    21.4 |  6.305 % |
c |      4071 |   12120    42610 |    5914    4071    91012    22.4 |  6.305 % |
c ==============================================================================
c [1mFound solution: 42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 501   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4281 |   12125    42637 |    4041    4281    99149    23.2 |  6.305 % |
c |      4382 |   12125    42637 |    4445    2242    43378    19.3 |  6.381 % |
c |      4532 |   12125    42637 |    4889    2392    44468    18.6 |  6.381 % |
c |      4757 |   12125    42637 |    5378    2617    54821    20.9 |  6.381 % |
c |      5094 |   12125    42637 |    5916    2954    60845    20.6 |  6.381 % |
c |      5600 |   12125    42637 |    6508    3460    84826    24.5 |  6.381 % |
c |      6359 |   12125    42637 |    7158    4219   111742    26.5 |  6.381 % |
c |      7498 |   12125    42637 |    7874    5358   154857    28.9 |  6.381 % |
c ==============================================================================
c [1mFound solution: 39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 504   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7786 |   12128    42656 |    4042    5646   160428    28.4 |  6.381 % |
c ==============================================================================
c [1mFound solution: 38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 505   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7868 |   12130    42668 |    4043    2905    68514    23.6 |  6.381 % |
c |      7968 |   12130    42668 |    4447    3005    70384    23.4 |  6.494 % |
c |      8118 |   12130    42668 |    4892    3155    73671    23.4 |  6.494 % |
c |      8344 |   12130    42668 |    5381    3381    78855    23.3 |  6.494 % |
c |      8682 |   12130    42668 |    5919    3719    86312    23.2 |  6.494 % |
c |      9188 |   12130    42668 |    6511    4225   111409    26.4 |  6.494 % |
c |      9947 |   12130    42668 |    7162    4984   141457    28.4 |  6.494 % |
c |     11086 |   12130    42668 |    7878    6123   191892    31.3 |  6.494 % |
c |     12796 |   12130    42668 |    8666    7833   242398    30.9 |  6.494 % |
c |     15358 |   12130    42668 |    9533    5446   180542    33.2 |  6.494 % |
c |     19204 |   12130    42668 |   10486    9292   437150    47.0 |  6.494 % |
c |     24970 |   12130    42668 |   11535    9306   572735    61.5 |  6.494 % |
c |     33619 |   12130    42668 |   12688    6060   332558    54.9 |  6.494 % |
c |     46594 |   12130    42668 |   13957   12283   973231    79.2 |  6.494 % |
c |     66055 |   12130    42668 |   15353    8927   700151    78.4 |  6.494 % |
c |     95247 |   12130    42668 |   16888   13049  1178396    90.3 |  6.494 % |
c |    139036 |   12130    42668 |   18577   12597  1055509    83.8 |  6.494 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 512   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    155989 |   12102    42507 |    4034   19664  1570600    79.9 |  6.494 % |
c |    156089 |   12102    42507 |    4437    2558   121700    47.6 |  6.697 % |
c |    156239 |   12102    42507 |    4881    2708   122499    45.2 |  6.697 % |
c |    156464 |   12102    42507 |    5369    2933   126217    43.0 |  6.697 % |
c |    156801 |   12102    42507 |    5906    3270   133194    40.7 |  6.697 % |
c |    157309 |   12102    42507 |    6496    3778   139819    37.0 |  6.697 % |
c |    158070 |   12102    42507 |    7146    4539   175552    38.7 |  6.697 % |
c |    159210 |   12102    42507 |    7861    5679   216474    38.1 |  6.697 % |
c |    160918 |   12102    42507 |    8647    7387   301285    40.8 |  6.697 % |
c |    163483 |   12102    42507 |    9511    9952   471632    47.4 |  6.697 % |
c |    167327 |   12102    42507 |   10463    8820   515414    58.4 |  6.697 % |
c |    173094 |   12102    42507 |   11509    8807   647238    73.5 |  6.697 % |
c |    181744 |   12102    42507 |   12660   10999   720905    65.5 |  6.697 % |
c |    194718 |   12102    42507 |   13926   10490   717006    68.4 |  6.697 % |
c |    214182 |   12102    42507 |   15319    7921   481162    60.7 |  6.697 % |
c |    243374 |   12102    42507 |   16851   13006  1098047    84.4 |  6.697 % |
c |    287163 |   12102    42507 |   18536   11727   936272    79.8 |  6.697 % |
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 513   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    319165 |   12104    42517 |    4034   13974  1463581   104.7 |  6.697 % |
c |    319265 |   12104    42517 |    4437    3594   245776    68.4 |  6.734 % |
c |    319416 |   12104    42517 |    4881    3745   246711    65.9 |  6.734 % |
c |    319641 |   12104    42517 |    5369    3970   248556    62.6 |  6.734 % |
c |    319978 |   12104    42517 |    5906    4307   251419    58.4 |  6.734 % |
c |    320484 |   12104    42517 |    6496    4813   265087    55.1 |  6.734 % |
c |    321243 |   12104    42517 |    7146    5572   292087    52.4 |  6.734 % |
c |    322383 |   12104    42517 |    7861    6712   339110    50.5 |  6.734 % |
c |    324091 |   12104    42517 |    8647    8420   421125    50.0 |  6.734 % |
c |    326653 |   12104    42517 |    9511    5758   246754    42.9 |  6.734 % |
c |    330499 |   12104    42517 |   10463    9604   489190    50.9 |  6.734 % |
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 514   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    333970 |   12109    42542 |    4036    7710   427098    55.4 |  6.734 % |
c |    334070 |   12109    42542 |    4439    3955   176149    44.5 |  6.773 % |
c |    334221 |   12109    42542 |    4883    4106   180766    44.0 |  6.773 % |
c |    334446 |   12109    42542 |    5371    4331   185769    42.9 |  6.773 % |
c |    334784 |   12109    42542 |    5909    4669   196569    42.1 |  6.773 % |
c |    335290 |   12109    42542 |    6500    5175   211983    41.0 |  6.773 % |
c |    336050 |   12109    42542 |    7150    5935   237740    40.1 |  6.773 % |
c |    337189 |   12109    42542 |    7865    7074   275330    38.9 |  6.773 % |
c |    338897 |   12109    42542 |    8651    4458   162908    36.5 |  6.773 % |
c |    341463 |   12109    42542 |    9516    7024   345829    49.2 |  6.773 % |
c |    345309 |   12109    42542 |   10468    5908   245278    41.5 |  6.773 % |
c |    351076 |   12109    42542 |   11515    6174   334248    54.1 |  6.773 % |
c |    359725 |   12109    42542 |   12666    8779   509978    58.1 |  6.773 % |
c |    372701 |   12109    42542 |   13933    8027   598136    74.5 |  6.773 % |
c |    392163 |   12109    42542 |   15326   12352  1400320   113.4 |  6.773 % |
c |    421357 |   12109    42542 |   16859   16500  1436646    87.1 |  6.773 % |
c |    465146 |   12109    42542 |   18545   15894  1226816    77.2 |  6.773 % |
c |    530830 |   12109    42542 |   20399   13974  1258432    90.1 |  6.773 % |
c |    629360 |   12109    42542 |   22439   16889  1573138    93.1 |  6.773 % |
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 516   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    636091 |   12111    42558 |    4037   23620  2075601    87.9 |  6.773 % |
c |    636191 |   12111    42558 |    4440    3053   188398    61.7 |  6.850 % |
c |    636341 |   12111    42558 |    4884    3203   192909    60.2 |  6.850 % |
c |    636566 |   12111    42558 |    5373    3428   194662    56.8 |  6.850 % |
c |    636905 |   12111    42558 |    5910    3767   206647    54.9 |  6.850 % |
c |    637411 |   12111    42558 |    6501    4273   219600    51.4 |  6.851 % |
c |    638170 |   12111    42558 |    7151    5032   261328    51.9 |  6.850 % |
c |    639309 |   12111    42558 |    7866    6171   311388    50.5 |  6.850 % |
c |    641017 |   12111    42558 |    8653    7879   410801    52.1 |  6.850 % |
c |    643579 |   12111    42558 |    9519    5578   224839    40.3 |  6.850 % |
c |    647425 |   12111    42558 |   10470    9424   425139    45.1 |  6.850 % |
c |    653191 |   12111    42558 |   11518    9613   541449    56.3 |  6.850 % |
c |    661841 |   12111    42558 |   12669   12101   804529    66.5 |  6.850 % |
c |    674815 |   12111    42558 |   13936   11348   971116    85.6 |  6.850 % |
c |    694277 |   12111    42558 |   15330    8632   869501   100.7 |  6.850 % |
c |    723469 |   12111    42558 |   16863   14038   901871    64.2 |  6.850 % |
c |    767261 |   12111    42558 |   18549   13806  1101548    79.8 |  6.850 % |
c |    832947 |   12111    42558 |   20404   12053   974821    80.9 |  6.850 % |
c |    931477 |   12111    42558 |   22445   15353  1166239    76.0 |  6.850 % |
c |   1079266 |   12111    42558 |   24689   12409  1103773    88.9 |  6.850 % |
#### 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.94 2/54 15217
Raw data (stat): 15217 (runsolver) R 15216 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479848963 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+9.99987 s]
Raw data (loadavg): 0.87 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 1250 0 0 0 995 3 0 0 25 0 1 0 479848963 6737920 1228 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1645 1228 603 41 0 1604 0
vsize: 6580
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 1469 0 0 0 1994 4 0 0 25 0 1 0 479848963 7680000 1447 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1875 1447 603 41 0 1834 0
vsize: 7500
[startup+30.0008 s]
Raw data (loadavg): 0.91 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 1959 0 0 0 2992 5 0 0 25 0 1 0 479848963 9560064 1937 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2334 1937 603 41 0 2293 0
vsize: 9336
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 1959 0 0 0 3991 6 0 0 25 0 1 0 479848963 9560064 1937 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2334 1937 603 41 0 2293 0
vsize: 9336
[startup+50.0008 s]
Raw data (loadavg): 0.93 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2351 0 0 0 4990 7 0 0 25 0 1 0 479848963 11255808 2329 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2748 2329 603 41 0 2707 0
vsize: 10992
[startup+60.0005 s]
Raw data (loadavg): 0.94 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2573 0 0 0 5990 7 0 0 25 0 1 0 479848963 12210176 2551 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2981 2551 603 41 0 2940 0
vsize: 11924
[startup+70.0009 s]
Raw data (loadavg): 0.95 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2573 0 0 0 6990 7 0 0 25 0 1 0 479848963 12210176 2551 4294967295 134512640 134672761 3221224544 3221223728 134559604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2981 2551 603 41 0 2940 0
vsize: 11924
[startup+80.0009 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2574 0 0 0 7990 7 0 0 25 0 1 0 479848963 12210176 2552 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2981 2552 603 41 0 2940 0
vsize: 11924
[startup+90.0015 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2574 0 0 0 8991 7 0 0 25 0 1 0 479848963 12210176 2552 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2981 2552 603 41 0 2940 0
vsize: 11924
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2922 0 0 0 9990 8 0 0 25 0 1 0 479848963 13684736 2900 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3341 2900 603 41 0 3300 0
vsize: 13364
[startup+110.001 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2955 0 0 0 10990 8 0 0 25 0 1 0 479848963 13819904 2933 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2933 603 41 0 3333 0
vsize: 13496
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2955 0 0 0 11990 8 0 0 25 0 1 0 479848963 13819904 2933 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2933 603 41 0 3333 0
vsize: 13496
[startup+130.001 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 12990 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223728 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+140.001 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 13990 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 14991 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223712 134561086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 15991 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 16991 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 17991 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223808 134562284 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 18991 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 19991 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 20991 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 21991 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 22991 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 2957 0 0 0 23992 8 0 0 25 0 1 0 479848963 13819904 2935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2935 603 41 0 3333 0
vsize: 13496
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3033 0 0 0 24992 8 0 0 25 0 1 0 479848963 14086144 3011 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3439 3011 603 41 0 3398 0
vsize: 13756
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3152 0 0 0 25992 9 0 0 25 0 1 0 479848963 14630912 3130 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3572 3130 603 41 0 3531 0
vsize: 14288
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3155 0 0 0 26992 9 0 0 25 0 1 0 479848963 14630912 3133 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3572 3133 603 41 0 3531 0
vsize: 14288
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3404 0 0 0 27992 9 0 0 25 0 1 0 479848963 15581184 3382 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3804 3382 603 41 0 3763 0
vsize: 15216
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3506 0 0 0 28992 9 0 0 25 0 1 0 479848963 15982592 3484 4294967295 134512640 134672761 3221224544 3221223696 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3902 3484 603 41 0 3861 0
vsize: 15608
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 29991 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223648 134560260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+310 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 30991 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 31992 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+330 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 32992 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 33992 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+350 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 34992 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 35992 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223728 134558920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 36992 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+380 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 37992 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 38992 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 39992 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+410 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 40993 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+420 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 41993 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 42993 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+440 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 43993 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+450 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 44993 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+460 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3690 0 0 0 45993 10 0 0 25 0 1 0 479848963 16785408 3668 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4098 3668 603 41 0 4057 0
vsize: 16392
[startup+470 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3732 0 0 0 46993 10 0 0 25 0 1 0 479848963 16920576 3710 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4131 3710 603 41 0 4090 0
vsize: 16524
[startup+480 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3732 0 0 0 47994 10 0 0 25 0 1 0 479848963 16920576 3710 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4131 3710 603 41 0 4090 0
vsize: 16524
[startup+490.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3732 0 0 0 48994 10 0 0 25 0 1 0 479848963 16920576 3710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4131 3710 603 41 0 4090 0
vsize: 16524
[startup+500.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3749 0 0 0 49994 10 0 0 25 0 1 0 479848963 17076224 3727 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4169 3727 603 41 0 4128 0
vsize: 16676
[startup+510.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3750 0 0 0 50994 10 0 0 25 0 1 0 479848963 17076224 3728 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4169 3728 603 41 0 4128 0
vsize: 16676
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3750 0 0 0 51994 10 0 0 25 0 1 0 479848963 17076224 3728 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4169 3728 603 41 0 4128 0
vsize: 16676
[startup+530.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3752 0 0 0 52994 10 0 0 25 0 1 0 479848963 17076224 3730 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4169 3730 603 41 0 4128 0
vsize: 16676
[startup+540.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3752 0 0 0 53995 10 0 0 25 0 1 0 479848963 17076224 3730 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4169 3730 603 41 0 4128 0
vsize: 16676
[startup+550.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3820 0 0 0 54995 10 0 0 25 0 1 0 479848963 17346560 3798 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4235 3798 603 41 0 4194 0
vsize: 16940
[startup+560.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3831 0 0 0 55995 10 0 0 25 0 1 0 479848963 17346560 3809 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4235 3809 603 41 0 4194 0
vsize: 16940
[startup+570.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3841 0 0 0 56995 10 0 0 25 0 1 0 479848963 17510400 3819 4294967295 134512640 134672761 3221224544 3221223648 134559805 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4275 3819 603 41 0 4234 0
vsize: 17100
[startup+580.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3891 0 0 0 57995 10 0 0 25 0 1 0 479848963 17645568 3869 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4308 3869 603 41 0 4267 0
vsize: 17232
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3898 0 0 0 58995 10 0 0 25 0 1 0 479848963 17645568 3876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4308 3876 603 41 0 4267 0
vsize: 17232
[startup+600.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3986 0 0 0 59995 11 0 0 25 0 1 0 479848963 18059264 3964 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4409 3964 603 41 0 4368 0
vsize: 17636
[startup+610.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3990 0 0 0 60995 11 0 0 25 0 1 0 479848963 18059264 3968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4409 3968 603 41 0 4368 0
vsize: 17636
[startup+620.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 3990 0 0 0 61995 11 0 0 25 0 1 0 479848963 18059264 3968 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4409 3968 603 41 0 4368 0
vsize: 17636
[startup+630.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4012 0 0 0 62995 11 0 0 25 0 1 0 479848963 18190336 3990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4441 3990 603 41 0 4400 0
vsize: 17764
[startup+640.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 63994 11 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 64995 11 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+660.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 65995 11 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+670.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 66995 11 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+680.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 67995 11 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+690.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 68995 11 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+700.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 69995 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+710.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 70995 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+720.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 71995 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+730.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 72995 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+740.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 73995 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+750.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 74996 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+760.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 75996 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+770.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 76996 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 77997 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 78997 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 79997 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.94 3/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 80997 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 81998 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 82998 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 83998 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4128 0 0 0 84998 12 0 0 25 0 1 0 479848963 18595840 4106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4540 4106 603 41 0 4499 0
vsize: 18160
[startup+860.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4227 0 0 0 85998 12 0 0 25 0 1 0 479848963 19001344 4205 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4639 4205 603 41 0 4598 0
vsize: 18556
[startup+870.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4241 0 0 0 86998 12 0 0 25 0 1 0 479848963 19148800 4219 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4675 4219 603 41 0 4634 0
vsize: 18700
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4241 0 0 0 87998 12 0 0 25 0 1 0 479848963 19148800 4219 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4675 4219 603 41 0 4634 0
vsize: 18700
[startup+890.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4241 0 0 0 88998 12 0 0 25 0 1 0 479848963 19148800 4219 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4675 4219 603 41 0 4634 0
vsize: 18700
[startup+900.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4241 0 0 0 89998 12 0 0 25 0 1 0 479848963 19148800 4219 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4675 4219 603 41 0 4634 0
vsize: 18700
[startup+910.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4325 0 0 0 90999 12 0 0 25 0 1 0 479848963 19550208 4303 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4303 603 41 0 4732 0
vsize: 19092
[startup+920.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4325 0 0 0 91999 12 0 0 25 0 1 0 479848963 19550208 4303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4303 603 41 0 4732 0
vsize: 19092
[startup+930.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4337 0 0 0 92999 12 0 0 25 0 1 0 479848963 19550208 4315 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4315 603 41 0 4732 0
vsize: 19092
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4429 0 0 0 93999 12 0 0 25 0 1 0 479848963 19955712 4407 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4872 4407 603 41 0 4831 0
vsize: 19488
[startup+950.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4429 0 0 0 94999 12 0 0 25 0 1 0 479848963 19955712 4407 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4872 4407 603 41 0 4831 0
vsize: 19488
[startup+960.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4429 0 0 0 95999 12 0 0 25 0 1 0 479848963 19955712 4407 4294967295 134512640 134672761 3221224544 3221223728 134559351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4872 4407 603 41 0 4831 0
vsize: 19488
[startup+970.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4429 0 0 0 96999 12 0 0 25 0 1 0 479848963 19955712 4407 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4872 4407 603 41 0 4831 0
vsize: 19488
[startup+980.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4429 0 0 0 98000 12 0 0 25 0 1 0 479848963 19955712 4407 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4872 4407 603 41 0 4831 0
vsize: 19488
[startup+990.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4653 0 0 0 98999 13 0 0 25 0 1 0 479848963 20885504 4631 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4631 603 41 0 5058 0
vsize: 20396
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4653 0 0 0 99999 13 0 0 25 0 1 0 479848963 20885504 4631 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5099 4631 603 41 0 5058 0
vsize: 20396
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4693 0 0 0 101000 13 0 0 25 0 1 0 479848963 21020672 4671 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5132 4671 603 41 0 5091 0
vsize: 20528
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4695 0 0 0 102000 13 0 0 25 0 1 0 479848963 21020672 4673 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5132 4673 603 41 0 5091 0
vsize: 20528
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4880 0 0 0 102999 14 0 0 25 0 1 0 479848963 21827584 4858 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5329 4858 603 41 0 5288 0
vsize: 21316
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4883 0 0 0 103999 14 0 0 25 0 1 0 479848963 21827584 4861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5329 4861 603 41 0 5288 0
vsize: 21316
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4883 0 0 0 104999 14 0 0 25 0 1 0 479848963 21827584 4861 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5329 4861 603 41 0 5288 0
vsize: 21316
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4884 0 0 0 106000 14 0 0 25 0 1 0 479848963 21827584 4862 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5329 4862 603 41 0 5288 0
vsize: 21316
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4889 0 0 0 107000 14 0 0 25 0 1 0 479848963 21827584 4867 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5329 4867 603 41 0 5288 0
vsize: 21316
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4890 0 0 0 108000 14 0 0 25 0 1 0 479848963 21827584 4868 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5329 4868 603 41 0 5288 0
vsize: 21316
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4935 0 0 0 109000 14 0 0 25 0 1 0 479848963 21962752 4913 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5362 4913 603 41 0 5321 0
vsize: 21448
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4941 0 0 0 110000 14 0 0 25 0 1 0 479848963 22106112 4919 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5397 4919 603 41 0 5356 0
vsize: 21588
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4973 0 0 0 111000 14 0 0 25 0 1 0 479848963 22241280 4951 4294967295 134512640 134672761 3221224544 3221223616 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5430 4951 603 41 0 5389 0
vsize: 21720
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4976 0 0 0 112000 14 0 0 25 0 1 0 479848963 22241280 4954 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5430 4954 603 41 0 5389 0
vsize: 21720
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4976 0 0 0 113000 14 0 0 25 0 1 0 479848963 22241280 4954 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5430 4954 603 41 0 5389 0
vsize: 21720
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4976 0 0 0 114001 14 0 0 25 0 1 0 479848963 22241280 4954 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5430 4954 603 41 0 5389 0
vsize: 21720
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4976 0 0 0 115001 14 0 0 25 0 1 0 479848963 22241280 4954 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5430 4954 603 41 0 5389 0
vsize: 21720
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4976 0 0 0 116001 14 0 0 25 0 1 0 479848963 22241280 4954 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5430 4954 603 41 0 5389 0
vsize: 21720
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4976 0 0 0 117001 14 0 0 25 0 1 0 479848963 22241280 4954 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5430 4954 603 41 0 5389 0
vsize: 21720
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4976 0 0 0 118001 15 0 0 25 0 1 0 479848963 22241280 4954 4294967295 134512640 134672761 3221224544 3221223728 134559609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5430 4954 603 41 0 5389 0
vsize: 21720
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4977 0 0 0 119000 15 0 0 25 0 1 0 479848963 22241280 4955 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5430 4955 603 41 0 5389 0
vsize: 21720
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 15217
Raw data (stat): 15217 (minisat+) R 15216 10614 10613 0 -1 0 4978 0 0 0 120001 15 0 0 25 0 1 0 479848963 22241280 4956 4294967295 134512640 134672761 3221224544 3221223648 134554919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5430 4956 603 41 0 5389 0
vsize: 21720
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.94 1/54 15217
Raw data (stat): 15217 (minisat+) Z 15216 10614 10613 0 -1 12 4981 0 0 0 120001 16 0 0 25 0 1 0 479848963 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.03
CPU time (s): 1200.17
CPU user time (s): 1200.01
CPU system time (s): 0.162975
CPU usage (%): 100.012
Max. virtual memory (Kb): 21720
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####