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-3pb.opb
MD5SUM	c267b57d74142f6538ad16680277f9bf
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	648
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	648
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	648
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02984
Number of variables	648
Total number of constraints	1954
Number of constraints which are clauses	1930
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	27
Trace number 5192

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-13 22:21:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3623 boxname=wulflinc10 idbench=239 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c267b57d74142f6538ad16680277f9bf  /oldhome/oroussel/tmp/wulflinc10/normalized-s4-4-3-3pb.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc10/normalized-s4-4-3-3pb.opb /oldhome/oroussel/tmp/wulflinc10/normalized-s4-4-3-3pb.opb
IDLAUNCH: 3623
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        887872 kB
Buffers:         34408 kB
Cached:          92860 kB
SwapCached:        164 kB
Active:          51020 kB
Inactive:        79288 kB
HighTotal:      131008 kB
HighFree:        34496 kB
LowTotal:       903652 kB
LowFree:        853376 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10824 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:41:38 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3623 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1954 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1944]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1934]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1885]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1883]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1869]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1843]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1821]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1811]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1778]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1752]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1750]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1740]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1726]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1700]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1678]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1668]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1654]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1628]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1606]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1596]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1594]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1568]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1550]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1525]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1507]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1485]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1459]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1453]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1435]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1413]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1387]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1381]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1333]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1323]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1313]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1311]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1258]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1248]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1242]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1240]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1203]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1181]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1175]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1169]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1167]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1141]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1123]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1097]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1060]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1038]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1032]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1026]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1024]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 998]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 980]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 954]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 952]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 926]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 908]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 882]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 868]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 842]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 820]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 810]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 792]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 771]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 745]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 739]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 722]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 700]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 674]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 668]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 658]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 648]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 598]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 596]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 586]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 576]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 526]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 524]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 487]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 465]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 459]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 453]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 400]---> 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 ---[ 382]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 372]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 362]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 312]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 310]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 304]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 286]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 248]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 238]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 236]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 210]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 192]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 129]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 107]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 101]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  95]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  62]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  36]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  34]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  22]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  21]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  20]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  19]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  18]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  17]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  16]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  15]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  14]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  13]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  12]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  11]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[  10]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   9]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   8]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   7]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   6]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   5]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   4]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   3]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   2]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   1]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ---[   0]---> Adder-cost: 46   maxlim: 23   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8950    30768 |    2983       0        0     nan |  0.000 % |
c |       100 |    8875    30503 |    3281      93      362     3.9 | 20.266 % |
c |       250 |    8657    29769 |    3609     215      961     4.5 | 22.337 % |
c |       475 |    8454    29094 |    3970     410     2281     5.6 | 24.359 % |
c |       812 |    8330    28674 |    4367     731     4939     6.8 | 25.690 % |
c |      1321 |    8183    28193 |    4804    1219    10289     8.4 | 26.972 % |
c |      2082 |    8093    27897 |    5284    1970    21052    10.7 | 27.860 % |
c |      3221 |    7909    27295 |    5813    3084    39629    12.8 | 29.586 % |
c |      4930 |    7850    27104 |    6394    4785    79353    16.6 | 30.178 % |
c |      7493 |    7760    26808 |    7033    3764    93349    24.8 | 31.065 % |
c |     11339 |    7745    26755 |    7737    7607   255530    33.6 | 31.213 % |
c |     17108 |    7745    26755 |    8510    4909   101559    20.7 | 31.213 % |
c |     25757 |    7745    26755 |    9361    8888   249903    28.1 | 31.213 % |
c |     38731 |    7720    26674 |   10298    6621   148456    22.4 | 31.460 % |
c |     58195 |    7720    26674 |   11327    9368   271351    29.0 | 31.460 % |
c |     87387 |    7681    26547 |   12460    8423   142688    16.9 | 31.805 % |
c |    131176 |    7622    26354 |   13706   12543   294859    23.5 | 32.347 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1290   maxlim: 578   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    139193 |   16561    58268 |    5520   13297   294993    22.2 | 32.347 % |
c |    139294 |   16561    58268 |    6072    3426    46835    13.7 | 20.054 % |
c |    139444 |   16561    58268 |    6679    3576    50128    14.0 | 20.054 % |
c |    139669 |   16561    58268 |    7347    3801    54671    14.4 | 20.054 % |
c |    140006 |   16561    58268 |    8081    4138    61071    14.8 | 20.054 % |
c |    140512 |   16561    58268 |    8890    4644    71303    15.4 | 20.054 % |
c |    141272 |   16561    58268 |    9779    5404    87943    16.3 | 20.054 % |
c |    142411 |   16552    58239 |   10756    6542   110227    16.8 | 20.114 % |
c |    144119 |   16552    58239 |   11832    8250   140486    17.0 | 20.114 % |
c |    146684 |   16552    58239 |   13015   10815   189541    17.5 | 20.114 % |
c |    150529 |   16552    58239 |   14317    7742   127050    16.4 | 20.114 % |
c |    156295 |   16523    58141 |   15749   13504   249658    18.5 | 20.265 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 582   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    164887 |   16528    58171 |    5509   13866   289716    20.9 | 20.265 % |
c |    164988 |   16528    58171 |    6059    3568    79388    22.2 | 20.337 % |
c |    165139 |   16528    58171 |    6665    3719    81679    22.0 | 20.337 % |
c |    165364 |   16528    58171 |    7332    3944    86038    21.8 | 20.337 % |
c |    165701 |   16528    58171 |    8065    4281    92568    21.6 | 20.337 % |
c |    166207 |   16528    58171 |    8872    4787   101543    21.2 | 20.337 % |
c |    166970 |   16528    58171 |    9759    5550   118044    21.3 | 20.337 % |
c |    168112 |   16528    58171 |   10735    6692   140346    21.0 | 20.337 % |
c |    169821 |   16528    58171 |   11809    8401   180364    21.5 | 20.337 % |
c |    172383 |   16528    58171 |   12989   10963   237713    21.7 | 20.337 % |
c |    176227 |   16528    58171 |   14288    7943   150570    19.0 | 20.337 % |
c |    181993 |   16528    58171 |   15717   13709   268979    19.6 | 20.337 % |
c |    190643 |   16519    58140 |   17289   14122   265346    18.8 | 20.367 % |
c |    203617 |   16519    58140 |   19018    9090   146606    16.1 | 20.367 % |
c |    223079 |   16519    58140 |   20920   18681   332859    17.8 | 20.367 % |
c |    252271 |   16519    58140 |   23012   15398   243018    15.8 | 20.367 % |
c |    296062 |   16519    58140 |   25313   22756  1478040    65.0 | 20.367 % |
c |    361746 |   16519    58140 |   27845   23247   689454    29.7 | 20.367 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 584   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    376572 |   16525    58171 |    5508   23544  1166998    49.6 | 20.367 % |
c |    376672 |   16525    58171 |    6058    5986   294018    49.1 | 20.415 % |
c |    376822 |   16525    58171 |    6664    6136   295096    48.1 | 20.415 % |
c |    377048 |   16525    58171 |    7331    6362   298383    46.9 | 20.415 % |
c |    377385 |   16525    58171 |    8064    6699   302466    45.2 | 20.415 % |
c |    377892 |   16525    58171 |    8870    7206   312375    43.3 | 20.415 % |
c |    378652 |   16525    58171 |    9757    7966   331593    41.6 | 20.415 % |
c |    379791 |   16525    58171 |   10733    9105   363845    40.0 | 20.415 % |
c |    381500 |   16525    58171 |   11806   10814   411056    38.0 | 20.415 % |
c |    384063 |   16525    58171 |   12987    7093   156966    22.1 | 20.415 % |
c |    387907 |   16525    58171 |   14286   10937   256061    23.4 | 20.415 % |
c |    393674 |   16525    58171 |   15714    9189   179805    19.6 | 20.415 % |
c |    402324 |   16525    58171 |   17286    9546   212916    22.3 | 20.415 % |
c |    415298 |   16525    58171 |   19015   13490   342290    25.4 | 20.415 % |
c |    434761 |   16525    58171 |   20916   13117   291167    22.2 | 20.415 % |
c |    463957 |   16525    58171 |   23008   20650   470459    22.8 | 20.415 % |
c |    507750 |   16525    58171 |   25309   15835  1010833    63.8 | 20.415 % |
c |    573434 |   16525    58171 |   27840   15283   904171    59.2 | 20.415 % |
c |    671962 |   16507    58109 |   30624   24422  1933828    79.2 | 20.475 % |
c |    819751 |   16507    58109 |   33686   25591  1445985    56.5 | 20.475 % |
c |   1041434 |   16498    58078 |   37055   17947  1492936    83.2 | 20.505 % |
#### 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.84 0.94 0.90 2/54 28902
Raw data (stat): 28902 (runsolver) R 28901 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421296781 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 955 0 0 0 995 3 0 0 25 0 1 0 421296781 5455872 933 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1332 933 603 41 0 1291 0
vsize: 5328
[startup+20.0003 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 1108 0 0 0 1995 3 0 0 25 0 1 0 421296781 6135808 1086 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1498 1086 603 41 0 1457 0
vsize: 5992
[startup+30.0008 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 1174 0 0 0 2995 3 0 0 25 0 1 0 421296781 6414336 1152 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1566 1152 603 41 0 1525 0
vsize: 6264
[startup+40.0001 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 1239 0 0 0 3994 4 0 0 25 0 1 0 421296781 6721536 1217 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1641 1217 603 41 0 1600 0
vsize: 6564
[startup+50.001 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 1365 0 0 0 4994 5 0 0 25 0 1 0 421296781 7131136 1343 4294967295 134512640 134672761 3221224560 3221223744 134559553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1741 1343 603 41 0 1700 0
vsize: 6964
[startup+60.0003 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 1543 0 0 0 5993 5 0 0 25 0 1 0 421296781 8126464 1521 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1984 1521 603 41 0 1943 0
vsize: 7936
[startup+69.9998 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 1582 0 0 0 6993 5 0 0 25 0 1 0 421296781 8273920 1560 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2020 1560 603 41 0 1979 0
vsize: 8080
[startup+80.0008 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 1678 0 0 0 7994 5 0 0 25 0 1 0 421296781 8695808 1656 4294967295 134512640 134672761 3221224560 3221223684 134566095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1656 603 41 0 2082 0
vsize: 8492
[startup+90 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 1713 0 0 0 8994 5 0 0 25 0 1 0 421296781 8843264 1691 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2159 1691 603 41 0 2118 0
vsize: 8636
[startup+99.9995 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 1786 0 0 0 9993 6 0 0 25 0 1 0 421296781 9121792 1764 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2227 1764 603 41 0 2186 0
vsize: 8908
[startup+109.999 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 1819 0 0 0 10994 6 0 0 25 0 1 0 421296781 9269248 1797 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1797 603 41 0 2222 0
vsize: 9052
[startup+119.999 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 2066 0 0 0 11993 7 0 0 25 0 1 0 421296781 10240000 2044 4294967295 134512640 134672761 3221224560 3221223620 1075346629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2500 2044 603 41 0 2459 0
vsize: 10000
[startup+129.998 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 2654 0 0 0 12991 8 0 0 25 0 1 0 421296781 12656640 2632 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3090 2632 603 41 0 3049 0
vsize: 12360
[startup+139.998 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3190 0 0 0 13990 10 0 0 25 0 1 0 421296781 14917632 3168 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3168 603 41 0 3601 0
vsize: 14568
[startup+149.998 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3350 0 0 0 14990 10 0 0 25 0 1 0 421296781 15593472 3328 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3328 603 41 0 3766 0
vsize: 15228
[startup+159.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3351 0 0 0 15990 10 0 0 25 0 1 0 421296781 15593472 3329 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3329 603 41 0 3766 0
vsize: 15228
[startup+169.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3353 0 0 0 16990 10 0 0 25 0 1 0 421296781 15593472 3331 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3331 603 41 0 3766 0
vsize: 15228
[startup+179.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3358 0 0 0 17990 10 0 0 25 0 1 0 421296781 15593472 3336 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3336 603 41 0 3766 0
vsize: 15228
[startup+189.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3358 0 0 0 18990 10 0 0 25 0 1 0 421296781 15593472 3336 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3336 603 41 0 3766 0
vsize: 15228
[startup+199.997 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3360 0 0 0 19990 10 0 0 25 0 1 0 421296781 15593472 3338 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3338 603 41 0 3766 0
vsize: 15228
[startup+209.997 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3362 0 0 0 20991 10 0 0 25 0 1 0 421296781 15593472 3340 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3340 603 41 0 3766 0
vsize: 15228
[startup+219.996 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3363 0 0 0 21990 10 0 0 25 0 1 0 421296781 15593472 3341 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3341 603 41 0 3766 0
vsize: 15228
[startup+229.996 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3363 0 0 0 22991 10 0 0 25 0 1 0 421296781 15593472 3341 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3341 603 41 0 3766 0
vsize: 15228
[startup+239.995 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3363 0 0 0 23991 10 0 0 25 0 1 0 421296781 15593472 3341 4294967295 134512640 134672761 3221224560 3221223744 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3341 603 41 0 3766 0
vsize: 15228
[startup+249.996 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3363 0 0 0 24991 10 0 0 25 0 1 0 421296781 15593472 3341 4294967295 134512640 134672761 3221224560 3221223744 134559553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3341 603 41 0 3766 0
vsize: 15228
[startup+259.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3364 0 0 0 25991 10 0 0 25 0 1 0 421296781 15593472 3342 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3342 603 41 0 3766 0
vsize: 15228
[startup+269.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3365 0 0 0 26991 10 0 0 25 0 1 0 421296781 15593472 3343 4294967295 134512640 134672761 3221224560 3221223744 134558332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3343 603 41 0 3766 0
vsize: 15228
[startup+279.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3365 0 0 0 27992 10 0 0 25 0 1 0 421296781 15593472 3343 4294967295 134512640 134672761 3221224560 3221223664 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3807 3343 603 41 0 3766 0
vsize: 15228
[startup+289.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3554 0 0 0 28991 11 0 0 25 0 1 0 421296781 16400384 3532 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4004 3532 603 41 0 3963 0
vsize: 16016
[startup+299.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3797 0 0 0 29991 11 0 0 25 0 1 0 421296781 17342464 3775 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4234 3775 603 41 0 4193 0
vsize: 16936
[startup+309.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3797 0 0 0 30991 11 0 0 25 0 1 0 421296781 17342464 3775 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4234 3775 603 41 0 4193 0
vsize: 16936
[startup+319.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3798 0 0 0 31991 11 0 0 25 0 1 0 421296781 17342464 3776 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4234 3776 603 41 0 4193 0
vsize: 16936
[startup+329.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3798 0 0 0 32992 11 0 0 25 0 1 0 421296781 17342464 3776 4294967295 134512640 134672761 3221224560 3221223728 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4234 3776 603 41 0 4193 0
vsize: 16936
[startup+339.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3798 0 0 0 33992 11 0 0 25 0 1 0 421296781 17342464 3776 4294967295 134512640 134672761 3221224560 3221223576 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4234 3776 603 41 0 4193 0
vsize: 16936
[startup+349.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3814 0 0 0 34992 12 0 0 25 0 1 0 421296781 17342464 3792 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4234 3792 603 41 0 4193 0
vsize: 16936
[startup+359.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3981 0 0 0 35990 13 0 0 25 0 1 0 421296781 18145280 3959 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4430 3959 603 41 0 4389 0
vsize: 17720
[startup+369.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3981 0 0 0 36989 13 0 0 25 0 1 0 421296781 18145280 3959 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4430 3959 603 41 0 4389 0
vsize: 17720
[startup+379.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3981 0 0 0 37989 13 0 0 25 0 1 0 421296781 18145280 3959 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4430 3959 603 41 0 4389 0
vsize: 17720
[startup+389.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3982 0 0 0 38989 13 0 0 25 0 1 0 421296781 18145280 3960 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4430 3960 603 41 0 4389 0
vsize: 17720
[startup+399.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 3982 0 0 0 39989 13 0 0 25 0 1 0 421296781 18145280 3960 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4430 3960 603 41 0 4389 0
vsize: 17720
[startup+409.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4149 0 0 0 40989 14 0 0 25 0 1 0 421296781 18808832 4127 4294967295 134512640 134672761 3221224560 3221223664 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4592 4127 603 41 0 4551 0
vsize: 18368
[startup+419.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4774 0 0 0 41987 16 0 0 25 0 1 0 421296781 21344256 4752 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5211 4752 603 41 0 5170 0
vsize: 20844
[startup+429.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4867 0 0 0 42986 16 0 0 25 0 1 0 421296781 21749760 4845 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5310 4845 603 41 0 5269 0
vsize: 21240
[startup+439.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4869 0 0 0 43986 16 0 0 25 0 1 0 421296781 21749760 4847 4294967295 134512640 134672761 3221224560 3221223744 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5310 4847 603 41 0 5269 0
vsize: 21240
[startup+449.995 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4902 0 0 0 44987 16 0 0 25 0 1 0 421296781 22011904 4880 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4880 603 41 0 5333 0
vsize: 21496
[startup+459.995 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4902 0 0 0 45987 16 0 0 25 0 1 0 421296781 22011904 4880 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4880 603 41 0 5333 0
vsize: 21496
[startup+469.995 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4902 0 0 0 46987 16 0 0 25 0 1 0 421296781 22011904 4880 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4880 603 41 0 5333 0
vsize: 21496
[startup+479.995 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4902 0 0 0 47987 16 0 0 25 0 1 0 421296781 22011904 4880 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4880 603 41 0 5333 0
vsize: 21496
[startup+489.995 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4902 0 0 0 48987 16 0 0 25 0 1 0 421296781 22011904 4880 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4880 603 41 0 5333 0
vsize: 21496
[startup+499.996 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4902 0 0 0 49988 16 0 0 25 0 1 0 421296781 22011904 4880 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4880 603 41 0 5333 0
vsize: 21496
[startup+509.996 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4902 0 0 0 50988 16 0 0 25 0 1 0 421296781 22011904 4880 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4880 603 41 0 5333 0
vsize: 21496
[startup+519.995 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4902 0 0 0 51988 16 0 0 25 0 1 0 421296781 22011904 4880 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4880 603 41 0 5333 0
vsize: 21496
[startup+529.995 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4902 0 0 0 52988 16 0 0 25 0 1 0 421296781 22011904 4880 4294967295 134512640 134672761 3221224560 3221223792 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4880 603 41 0 5333 0
vsize: 21496
[startup+539.995 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4902 0 0 0 53988 16 0 0 25 0 1 0 421296781 22011904 4880 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4880 603 41 0 5333 0
vsize: 21496
[startup+549.996 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4902 0 0 0 54989 16 0 0 25 0 1 0 421296781 22011904 4880 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4880 603 41 0 5333 0
vsize: 21496
[startup+559.996 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 4904 0 0 0 55989 16 0 0 25 0 1 0 421296781 22011904 4882 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5374 4882 603 41 0 5333 0
vsize: 21496
[startup+569.995 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5007 0 0 0 56988 17 0 0 25 0 1 0 421296781 22417408 4985 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5473 4985 603 41 0 5432 0
vsize: 21892
[startup+579.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5007 0 0 0 57989 17 0 0 25 0 1 0 421296781 22417408 4985 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5473 4985 603 41 0 5432 0
vsize: 21892
[startup+589.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5007 0 0 0 58989 17 0 0 25 0 1 0 421296781 22417408 4985 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5473 4985 603 41 0 5432 0
vsize: 21892
[startup+599.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5124 0 0 0 59989 17 0 0 25 0 1 0 421296781 22962176 5102 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5606 5102 603 41 0 5565 0
vsize: 22424
[startup+609.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5125 0 0 0 60989 17 0 0 25 0 1 0 421296781 22962176 5103 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5606 5103 603 41 0 5565 0
vsize: 22424
[startup+619.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5127 0 0 0 61989 17 0 0 25 0 1 0 421296781 22962176 5105 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5606 5105 603 41 0 5565 0
vsize: 22424
[startup+629.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5127 0 0 0 62989 17 0 0 25 0 1 0 421296781 22962176 5105 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5606 5105 603 41 0 5565 0
vsize: 22424
[startup+639.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5128 0 0 0 63989 17 0 0 25 0 1 0 421296781 22962176 5106 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5606 5106 603 41 0 5565 0
vsize: 22424
[startup+649.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5128 0 0 0 64989 17 0 0 25 0 1 0 421296781 22962176 5106 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5606 5106 603 41 0 5565 0
vsize: 22424
[startup+659.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5128 0 0 0 65989 17 0 0 25 0 1 0 421296781 22962176 5106 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5606 5106 603 41 0 5565 0
vsize: 22424
[startup+669.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5129 0 0 0 66990 17 0 0 25 0 1 0 421296781 22962176 5107 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5606 5107 603 41 0 5565 0
vsize: 22424
[startup+679.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5137 0 0 0 67990 17 0 0 25 0 1 0 421296781 22962176 5115 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5606 5115 603 41 0 5565 0
vsize: 22424
[startup+689.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5158 0 0 0 68990 17 0 0 25 0 1 0 421296781 23101440 5136 4294967295 134512640 134672761 3221224560 3221223664 134554673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5640 5136 603 41 0 5599 0
vsize: 22560
[startup+699.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5158 0 0 0 69990 17 0 0 25 0 1 0 421296781 23101440 5136 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5640 5136 603 41 0 5599 0
vsize: 22560
[startup+709.997 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5158 0 0 0 70990 17 0 0 25 0 1 0 421296781 23101440 5136 4294967295 134512640 134672761 3221224560 3221223664 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5640 5136 603 41 0 5599 0
vsize: 22560
[startup+719.997 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5158 0 0 0 71990 17 0 0 25 0 1 0 421296781 23101440 5136 4294967295 134512640 134672761 3221224560 3221223664 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5640 5136 603 41 0 5599 0
vsize: 22560
[startup+729.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5158 0 0 0 72991 17 0 0 25 0 1 0 421296781 23101440 5136 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5640 5136 603 41 0 5599 0
vsize: 22560
[startup+739.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5243 0 0 0 73991 17 0 0 25 0 1 0 421296781 23502848 5221 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5738 5221 603 41 0 5697 0
vsize: 22952
[startup+749.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5274 0 0 0 74991 17 0 0 25 0 1 0 421296781 23633920 5252 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5770 5252 603 41 0 5729 0
vsize: 23080
[startup+759.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5710 0 0 0 75990 19 0 0 25 0 1 0 421296781 25362432 5688 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6192 5688 603 41 0 6151 0
vsize: 24768
[startup+769.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5739 0 0 0 76990 19 0 0 25 0 1 0 421296781 25493504 5717 4294967295 134512640 134672761 3221224560 3221223664 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6224 5717 603 41 0 6183 0
vsize: 24896
[startup+779.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5744 0 0 0 77990 19 0 0 25 0 1 0 421296781 25493504 5722 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6224 5722 603 41 0 6183 0
vsize: 24896
[startup+789.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5986 0 0 0 78989 19 0 0 25 0 1 0 421296781 26562560 5964 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6485 5964 603 41 0 6444 0
vsize: 25940
[startup+799.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 5986 0 0 0 79990 19 0 0 25 0 1 0 421296781 26562560 5964 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6485 5964 603 41 0 6444 0
vsize: 25940
[startup+809.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6450 0 0 0 80988 21 0 0 25 0 1 0 421296781 28446720 6428 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6945 6428 603 41 0 6904 0
vsize: 27780
[startup+819.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6506 0 0 0 81988 21 0 0 25 0 1 0 421296781 28581888 6484 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6484 603 41 0 6937 0
vsize: 27912
[startup+829.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6506 0 0 0 82988 21 0 0 25 0 1 0 421296781 28581888 6484 4294967295 134512640 134672761 3221224560 3221223664 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6484 603 41 0 6937 0
vsize: 27912
[startup+839.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6506 0 0 0 83989 21 0 0 25 0 1 0 421296781 28581888 6484 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6484 603 41 0 6937 0
vsize: 27912
[startup+849.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6506 0 0 0 84989 21 0 0 25 0 1 0 421296781 28581888 6484 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6484 603 41 0 6937 0
vsize: 27912
[startup+859.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6507 0 0 0 85989 21 0 0 25 0 1 0 421296781 28581888 6485 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6485 603 41 0 6937 0
vsize: 27912
[startup+869.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6507 0 0 0 86989 21 0 0 25 0 1 0 421296781 28581888 6485 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6485 603 41 0 6937 0
vsize: 27912
[startup+879.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6507 0 0 0 87989 21 0 0 25 0 1 0 421296781 28581888 6485 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6485 603 41 0 6937 0
vsize: 27912
[startup+890.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6507 0 0 0 88991 21 0 0 25 0 1 0 421296781 28581888 6485 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6485 603 41 0 6937 0
vsize: 27912
[startup+900.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6507 0 0 0 89991 21 0 0 25 0 1 0 421296781 28581888 6485 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6485 603 41 0 6937 0
vsize: 27912
[startup+910.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6507 0 0 0 90991 21 0 0 25 0 1 0 421296781 28581888 6485 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6485 603 41 0 6937 0
vsize: 27912
[startup+920.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6508 0 0 0 91991 21 0 0 25 0 1 0 421296781 28581888 6486 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6486 603 41 0 6937 0
vsize: 27912
[startup+930.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6508 0 0 0 92991 21 0 0 25 0 1 0 421296781 28581888 6486 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6486 603 41 0 6937 0
vsize: 27912
[startup+940.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6509 0 0 0 93992 21 0 0 25 0 1 0 421296781 28581888 6487 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6487 603 41 0 6937 0
vsize: 27912
[startup+950.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6510 0 0 0 94992 21 0 0 25 0 1 0 421296781 28581888 6488 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6488 603 41 0 6937 0
vsize: 27912
[startup+960.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6510 0 0 0 95992 21 0 0 25 0 1 0 421296781 28581888 6488 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6488 603 41 0 6937 0
vsize: 27912
[startup+970.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6512 0 0 0 96992 21 0 0 25 0 1 0 421296781 28581888 6490 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6490 603 41 0 6937 0
vsize: 27912
[startup+980.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6512 0 0 0 97992 21 0 0 25 0 1 0 421296781 28581888 6490 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6490 603 41 0 6937 0
vsize: 27912
[startup+990.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6512 0 0 0 98992 21 0 0 25 0 1 0 421296781 28581888 6490 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6490 603 41 0 6937 0
vsize: 27912
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6513 0 0 0 99992 21 0 0 25 0 1 0 421296781 28581888 6491 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6491 603 41 0 6937 0
vsize: 27912
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6514 0 0 0 100993 21 0 0 25 0 1 0 421296781 28581888 6492 4294967295 134512640 134672761 3221224560 3221223664 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6492 603 41 0 6937 0
vsize: 27912
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6514 0 0 0 101993 21 0 0 25 0 1 0 421296781 28581888 6492 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6492 603 41 0 6937 0
vsize: 27912
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6514 0 0 0 102993 21 0 0 25 0 1 0 421296781 28581888 6492 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6492 603 41 0 6937 0
vsize: 27912
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6514 0 0 0 103993 21 0 0 25 0 1 0 421296781 28581888 6492 4294967295 134512640 134672761 3221224560 3221223664 134560316 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6492 603 41 0 6937 0
vsize: 27912
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6514 0 0 0 104993 21 0 0 25 0 1 0 421296781 28581888 6492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6978 6492 603 41 0 6937 0
vsize: 27912
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 6695 0 0 0 105993 22 0 0 25 0 1 0 421296781 29380608 6673 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7173 6673 603 41 0 7132 0
vsize: 28692
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 7260 0 0 0 106992 24 0 0 25 0 1 0 421296781 31670272 7238 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7732 7238 603 41 0 7691 0
vsize: 30928
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 7773 0 0 0 107990 25 0 0 25 0 1 0 421296781 33824768 7751 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8258 7751 603 41 0 8217 0
vsize: 33032
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8195 0 0 0 108989 27 0 0 25 0 1 0 421296781 35565568 8173 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8683 8173 603 41 0 8642 0
vsize: 34732
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8195 0 0 0 109989 27 0 0 25 0 1 0 421296781 35565568 8173 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8683 8173 603 41 0 8642 0
vsize: 34732
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8195 0 0 0 110989 27 0 0 25 0 1 0 421296781 35565568 8173 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8683 8173 603 41 0 8642 0
vsize: 34732
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8195 0 0 0 111989 27 0 0 25 0 1 0 421296781 35565568 8173 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8683 8173 603 41 0 8642 0
vsize: 34732
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8195 0 0 0 112990 27 0 0 25 0 1 0 421296781 35565568 8173 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8683 8173 603 41 0 8642 0
vsize: 34732
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8195 0 0 0 113990 27 0 0 25 0 1 0 421296781 35565568 8173 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8683 8173 603 41 0 8642 0
vsize: 34732
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8195 0 0 0 114990 27 0 0 25 0 1 0 421296781 35565568 8173 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8683 8173 603 41 0 8642 0
vsize: 34732
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8196 0 0 0 115991 27 0 0 25 0 1 0 421296781 35565568 8174 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8683 8174 603 41 0 8642 0
vsize: 34732
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8197 0 0 0 116991 27 0 0 25 0 1 0 421296781 35565568 8175 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8683 8175 603 41 0 8642 0
vsize: 34732
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8236 0 0 0 117991 27 0 0 25 0 1 0 421296781 35700736 8214 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8716 8214 603 41 0 8675 0
vsize: 34864
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8244 0 0 0 118991 27 0 0 25 0 1 0 421296781 35700736 8222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8716 8222 603 41 0 8675 0
vsize: 34864
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28902
Raw data (stat): 28902 (minisat+) R 28901 25347 25346 0 -1 0 8244 0 0 0 119991 27 0 0 25 0 1 0 421296781 35700736 8222 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8716 8222 603 41 0 8675 0
vsize: 34864
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 28902
Raw data (stat): 28902 (minisat+) Z 28901 25347 25346 0 -1 12 8247 0 0 0 119991 29 0 0 25 0 1 0 421296781 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.03
CPU time (s): 1200.21
CPU user time (s): 1199.92
CPU system time (s): 0.291955
CPU usage (%): 100.015
Max. virtual memory (Kb): 34864
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####