PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-2pb.opb
MD5SUM	55739635f7f3741bc4f78c540803ac21
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	64
Optimality of the best value was proved	NO
Number of terms in the objective function	648
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	648
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	648
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03884
Number of variables	648
Total number of constraints	1952
Number of constraints which are clauses	1928
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	27
Trace number 5579

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 00:31:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3998 boxname=wulflinc15 idbench=238 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  55739635f7f3741bc4f78c540803ac21  /oldhome/oroussel/tmp/wulflinc15/normalized-s4-4-3-2pb.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc15/normalized-s4-4-3-2pb.opb /oldhome/oroussel/tmp/wulflinc15/normalized-s4-4-3-2pb.opb
IDLAUNCH: 3998
/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:        903532 kB
Buffers:         35480 kB
Cached:          74168 kB
SwapCached:       2144 kB
Active:          63388 kB
Inactive:        51248 kB
HighTotal:      131008 kB
HighFree:        52976 kB
LowTotal:       903652 kB
LowFree:        850556 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10916 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:49:48 (client local time) WITH STATUS 30 IN 1107.7 SECONDS
stats: 3998 0 1107.7 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1952 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1950]---> BDD-cost:    1
c ---[1924]---> BDD-cost:    1
c ---[1906]---> BDD-cost:    1
c ---[1880]---> BDD-cost:    1
c ---[1862]---> BDD-cost:    1
c ---[1840]---> BDD-cost:    1
c ---[1814]---> BDD-cost:    1
c ---[1808]---> BDD-cost:    1
c ---[1794]---> BDD-cost:    1
c ---[1768]---> BDD-cost:    1
c ---[1746]---> BDD-cost:    1
c ---[1736]---> BDD-cost:    1
c ---[1734]---> BDD-cost:    1
c ---[1708]---> BDD-cost:    1
c ---[1690]---> BDD-cost:    1
c ---[1664]---> BDD-cost:    1
c ---[1662]---> BDD-cost:    1
c ---[1636]---> BDD-cost:    1
c ---[1619]---> BDD-cost:    1
c ---[1593]---> BDD-cost:    1
c ---[1560]---> BDD-cost:    1
c ---[1534]---> BDD-cost:    1
c ---[1532]---> BDD-cost:    1
c ---[1522]---> BDD-cost:    1
c ---[1516]---> BDD-cost:    1
c ---[1498]---> BDD-cost:    1
c ---[1460]---> BDD-cost:    1
c ---[1450]---> BDD-cost:    1
c ---[1436]---> BDD-cost:    1
c ---[1410]---> BDD-cost:    1
c ---[1388]---> BDD-cost:    1
c ---[1378]---> BDD-cost:    1
c ---[1341]---> BDD-cost:    1
c ---[1319]---> BDD-cost:    1
c ---[1313]---> BDD-cost:    1
c ---[1307]---> BDD-cost:    1
c ---[1305]---> BDD-cost:    1
c ---[1279]---> BDD-cost:    1
c ---[1261]---> BDD-cost:    1
c ---[1235]---> BDD-cost:    1
c ---[1186]---> BDD-cost:    1
c ---[1176]---> BDD-cost:    1
c ---[1166]---> BDD-cost:    1
c ---[1164]---> BDD-cost:    1
c ---[1154]---> BDD-cost:    1
c ---[1144]---> BDD-cost:    1
c ---[1095]---> BDD-cost:    1
c ---[1093]---> BDD-cost:    1
c ---[1057]---> BDD-cost:    1
c ---[1035]---> BDD-cost:    1
c ---[1029]---> BDD-cost:    1
c ---[1023]---> BDD-cost:    1
c ---[1009]---> BDD-cost:    1
c ---[ 984]---> BDD-cost:    1
c ---[ 962]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 915]---> BDD-cost:    1
c ---[ 893]---> BDD-cost:    1
c ---[ 887]---> BDD-cost:    1
c ---[ 881]---> BDD-cost:    1
c ---[ 871]---> BDD-cost:    1
c ---[ 861]---> BDD-cost:    1
c ---[ 811]---> BDD-cost:    1
c ---[ 809]---> BDD-cost:    1
c ---[ 776]---> BDD-cost:    1
c ---[ 750]---> BDD-cost:    1
c ---[ 748]---> BDD-cost:    1
c ---[ 738]---> BDD-cost:    1
c ---[ 736]---> BDD-cost:    1
c ---[ 710]---> BDD-cost:    1
c ---[ 692]---> BDD-cost:    1
c ---[ 666]---> BDD-cost:    1
c ---[ 664]---> BDD-cost:    1
c ---[ 638]---> BDD-cost:    1
c ---[ 620]---> BDD-cost:    1
c ---[ 594]---> BDD-cost:    1
c ---[ 592]---> BDD-cost:    1
c ---[ 566]---> BDD-cost:    1
c ---[ 548]---> BDD-cost:    1
c ---[ 522]---> BDD-cost:    1
c ---[ 520]---> BDD-cost:    1
c ---[ 494]---> BDD-cost:    1
c ---[ 476]---> BDD-cost:    1
c ---[ 450]---> BDD-cost:    1
c ---[ 417]---> BDD-cost:    1
c ---[ 391]---> BDD-cost:    1
c ---[ 389]---> BDD-cost:    1
c ---[ 379]---> BDD-cost:    1
c ---[ 346]---> BDD-cost:    1
c ---[ 320]---> BDD-cost:    1
c ---[ 318]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 260]---> BDD-cost:    1
c ---[ 250]---> BDD-cost:    1
c ---[ 240]---> BDD-cost:    1
c ---[ 238]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 210]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[  98]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   95
c ---[  22]---> BDD-cost:   95
c ---[  21]---> BDD-cost:   95
c ---[  20]---> BDD-cost:   95
c ---[  19]---> BDD-cost:   95
c ---[  18]---> BDD-cost:   95
c ---[  17]---> BDD-cost:   95
c ---[  16]---> BDD-cost:   95
c ---[  15]---> BDD-cost:   95
c ---[  14]---> BDD-cost:   95
c ---[  13]---> BDD-cost:   95
c ---[  12]---> BDD-cost:   95
c ---[  11]---> BDD-cost:   95
c ---[  10]---> BDD-cost:   95
c ---[   9]---> BDD-cost:   95
c ---[   8]---> BDD-cost:   95
c ---[   7]---> BDD-cost:   95
c ---[   6]---> BDD-cost:   95
c ---[   5]---> BDD-cost:   95
c ---[   4]---> BDD-cost:   95
c ---[   3]---> BDD-cost:   95
c ---[   2]---> BDD-cost:   95
c ---[   1]---> BDD-cost:   95
c ---[   0]---> BDD-cost:   95
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    8072    23334 |    2421       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2904          
c   -- var.elim.:  2000/2904          
c   -- var.elim.:  2904/2904          
c   -- var.elim.:  336/336          
c   -- subsuming                       
c   -- var.elim.:  216/216          
c   -- var.elim.:  264/264          
c   -- subsuming                       
c |         0 |    7928    22902 |      --       0       --      -- |     --   | -144/-144
c |         0 |    7928    22902 |    3171       0        0     nan |  0.000 % |
c |       100 |    7928    22902 |    3488     100     2347    23.5 |  4.564 % |
c |       251 |    7928    22902 |    3837     251     6210    24.7 |  4.564 % |
c |       476 |    7928    22902 |    4220     476    14963    31.4 |  4.564 % |
c |       813 |    7928    22902 |    4642     813    28684    35.3 |  4.564 % |
c |      1319 |    7928    22902 |    5107    1319    51272    38.9 |  4.564 % |
c |      2079 |    7928    22902 |    5617    2079    81081    39.0 |  4.564 % |
c |      3221 |    7928    22902 |    6179    3221   123865    38.5 |  4.564 % |
c |      4930 |    7928    22902 |    6797    4930   212121    43.0 |  4.564 % |
c |      7492 |    7928    22902 |    7477    5095   237901    46.7 |  4.564 % |
c |     11336 |    7928    22902 |    8225    6201   318777    51.4 |  4.564 % |
c ==============================================================================
c (current CPU-time: 5.00324 s)
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:29320     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14293 |   41809   101977 |   12542    6158   329097    53.4 |  4.564 % |
c   -- subsuming                       
c   -- var.elim.:  1000/22861          
c   -- var.elim.:  2000/22861          
c   -- var.elim.:  3000/22861          
c   -- var.elim.:  4000/22861          
c   -- var.elim.:  5000/22861          
c   -- var.elim.:  6000/22861          
c   -- var.elim.:  7000/22861          
c   -- var.elim.:  8000/22861          
c   -- var.elim.:  9000/22861          
c   -- var.elim.:  10000/22861          
c   -- var.elim.:  11000/22861          
c   -- var.elim.:  12000/22861          
c   -- var.elim.:  13000/22861          
c   -- var.elim.:  14000/22861          
c   -- var.elim.:  15000/22861          
c   -- var.elim.:  16000/22861          
c   -- var.elim.:  17000/22861          
c   -- var.elim.:  18000/22861          
c   -- var.elim.:  19000/22861          
c   -- var.elim.:  20000/22861          
c   -- var.elim.:  21000/22861          
c   -- var.elim.:  22000/22861          
c   -- var.elim.:  22861/22861          
c   -- var.elim.:  1000/11371          
c   -- var.elim.:  2000/11371          
c   -- var.elim.:  3000/11371          
c   -- var.elim.:  4000/11371          
c   -- var.elim.:  5000/11371          
c   -- var.elim.:  6000/11371          
c   -- var.elim.:  7000/11371          
c   -- var.elim.:  8000/11371          
c   -- var.elim.:  9000/11371          
c   -- var.elim.:  10000/11371          
c   -- var.elim.:  11000/11371          
c   -- var.elim.:  11371/11371          
c   -- var.elim.:  1000/2292          
c   -- var.elim.:  2000/2292          
c   -- var.elim.:  2292/2292          
c   -- var.elim.:  1000/4129          
c   -- var.elim.:  2000/4129          
c   -- var.elim.:  3000/4129          
c   -- var.elim.:  4000/4129          
c   -- var.elim.:  4129/4129          
c   -- var.elim.:  1000/5006          
c   -- var.elim.:  2000/5006          
c   -- var.elim.:  3000/5006          
c   -- var.elim.:  4000/5006          
c   -- var.elim.:  5000/5006          
c   -- var.elim.:  5006/5006          
c   -- var.elim.:  1000/4419          
c   -- var.elim.:  2000/4419          
c   -- var.elim.:  3000/4419          
c   -- var.elim.:  4000/4419          
c   -- var.elim.:  4419/4419          
c   -- var.elim.:  392/392          
c   -- subsuming                       
c   -- var.elim.:  1000/10054          
c   -- var.elim.:  2000/10054          
c   -- var.elim.:  3000/10054          
c   -- var.elim.:  4000/10054          
c   -- var.elim.:  5000/10054          
c   -- var.elim.:  6000/10054          
c   -- var.elim.:  7000/10054          
c   -- var.elim.:  8000/10054          
c   -- var.elim.:  9000/10054          
c   -- var.elim.:  10000/10054          
c   -- var.elim.:  10054/10054          
c   -- var.elim.:  1000/5727          
c   -- var.elim.:  2000/5727          
c   -- var.elim.:  3000/5727          
c   -- var.elim.:  4000/5727          
c   -- var.elim.:  5000/5727          
c   -- var.elim.:  5727/5727          
c   -- var.elim.:  1000/6068          
c   -- var.elim.:  2000/6068          
c   -- var.elim.:  3000/6068          
c   -- var.elim.:  4000/6068          
c   -- var.elim.:  5000/6068          
c   -- var.elim.:  6000/6068          
c   -- var.elim.:  6068/6068          
c   -- var.elim.:  1000/6310          
c   -- var.elim.:  2000/6310          
c   -- var.elim.:  3000/6310          
c   -- var.elim.:  4000/6310          
c   -- var.elim.:  5000/6310          
c   -- var.elim.:  6000/6310          
c   -- var.elim.:  6310/6310          
c   -- var.elim.:  1000/5150          
c   -- var.elim.:  2000/5150          
c   -- var.elim.:  3000/5150          
c   -- var.elim.:  4000/5150          
c   -- var.elim.:  5000/5150          
c   -- var.elim.:  5150/5150          
c   -- var.elim.:  1000/2213          
c   -- var.elim.:  2000/2213          
c   -- var.elim.:  2213/2213          
c   -- subsuming                       
c   -- var.elim.:  1000/6653          
c   -- var.elim.:  2000/6653          
c   -- var.elim.:  3000/6653          
c   -- var.elim.:  4000/6653          
c   -- var.elim.:  5000/6653          
c   -- var.elim.:  6000/6653          
c   -- var.elim.:  6653/6653          
c   -- var.elim.:  1000/4906          
c   -- var.elim.:  2000/4906          
c   -- var.elim.:  3000/4906          
c   -- var.elim.:  4000/4906          
c   -- var.elim.:  4906/4906          
c   -- var.elim.:  1000/3473          
c   -- var.elim.:  2000/3473          
c   -- var.elim.:  3000/3473          
c   -- var.elim.:  3473/3473          
c   -- var.elim.:  1000/2910          
c   -- var.elim.:  2000/2910          
c   -- var.elim.:  2910/2910          
c   -- subsuming                       
c   -- var.elim.:  1000/5005          
c   -- var.elim.:  2000/5005          
c   -- var.elim.:  3000/5005          
c   -- var.elim.:  4000/5005          
c   -- var.elim.:  5000/5005          
c   -- var.elim.:  5005/5005          
c   -- var.elim.:  1000/3906          
c   -- var.elim.:  2000/3906          
c   -- var.elim.:  3000/3906          
c   -- var.elim.:  3906/3906          
c   -- var.elim.:  1000/2541          
c   -- var.elim.:  2000/2541          
c   -- var.elim.:  2541/2541          
c   -- var.elim.:  1000/3061          
c   -- var.elim.:  2000/3061          
c   -- var.elim.:  3000/3061          
c   -- var.elim.:  3061/3061          
c   -- var.elim.:  200/200          
c   -- subsuming                       
c   -- var.elim.:  1000/3771          
c   -- var.elim.:  2000/3771          
c   -- var.elim.:  3000/3771          
c   -- var.elim.:  3771/3771          
c   -- var.elim.:  1000/2960          
c   -- var.elim.:  2000/2960          
c   -- var.elim.:  2960/2960          
c |     14293 |   29129   181167 |      --    6158       --      -- |     --   | -12669/79223
c |     14293 |   29129   181167 |   11651    6158   329097    53.4 |  4.564 % |
c |     14394 |   29129   181167 |   12816    6259   331373    52.9 |  1.122 % |
c |     14544 |   29129   181167 |   14098    6409   334610    52.2 |  1.122 % |
c |     14769 |   29129   181167 |   15508    6634   342349    51.6 |  1.122 % |
c |     15106 |   29129   181167 |   17059    6971   354848    50.9 |  1.122 % |
c |     15615 |   29129   181167 |   18765    7480   373791    50.0 |  1.122 % |
c |     16377 |   29101   181063 |   20621    8195   402680    49.1 |  1.137 % |
c |     17517 |   29101   181063 |   22683    9335   439575    47.1 |  1.137 % |
c |     19225 |   29101   181063 |   24952   11043   503056    45.6 |  1.137 % |
c |     21788 |   29101   181063 |   27447   13606   627237    46.1 |  1.137 % |
c |     25632 |   29101   181063 |   30192   17450   779280    44.7 |  1.137 % |
c |     31398 |   29101   181063 |   33211   23216  1098225    47.3 |  1.137 % |
c |     40048 |   29101   181063 |   36532   31866  1692937    53.1 |  1.137 % |
c |     53024 |   29101   181063 |   40185   21101  1328219    62.9 |  1.137 % |
c |     72485 |   29101   181063 |   44204   14828   705951    47.6 |  1.137 % |
c |    101680 |   29016   171748 |   48482   44000  2201070    50.0 |  1.215 % |
c ==============================================================================
c (current CPU-time: 289.757 s)
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:17998     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    108194 |   52574   230103 |   15772   15122   819837    54.2 |  1.215 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24519          
c   -- var.elim.:  2000/24519          
c   -- var.elim.:  3000/24519          
c   -- var.elim.:  4000/24519          
c   -- var.elim.:  5000/24519          
c   -- var.elim.:  6000/24519          
c   -- var.elim.:  7000/24519          
c   -- var.elim.:  8000/24519          
c   -- var.elim.:  9000/24519          
c   -- var.elim.:  10000/24519          
c   -- var.elim.:  11000/24519          
c   -- var.elim.:  12000/24519          
c   -- var.elim.:  13000/24519          
c   -- var.elim.:  14000/24519          
c   -- var.elim.:  15000/24519          
c   -- var.elim.:  16000/24519          
c   -- var.elim.:  17000/24519          
c   -- var.elim.:  18000/24519          
c   -- var.elim.:  19000/24519          
c   -- var.elim.:  20000/24519          
c   -- var.elim.:  21000/24519          
c   -- var.elim.:  22000/24519          
c   -- var.elim.:  23000/24519          
c   -- var.elim.:  24000/24519          
c   -- var.elim.:  24519/24519          
c   -- var.elim.:  1000/13042          
c   -- var.elim.:  2000/13042          
c   -- var.elim.:  3000/13042          
c   -- var.elim.:  4000/13042          
c   -- var.elim.:  5000/13042          
c   -- var.elim.:  6000/13042          
c   -- var.elim.:  7000/13042          
c   -- var.elim.:  8000/13042          
c   -- var.elim.:  9000/13042          
c   -- var.elim.:  10000/13042          
c   -- var.elim.:  11000/13042          
c   -- var.elim.:  12000/13042          
c   -- var.elim.:  13000/13042          
c   -- var.elim.:  13042/13042          
c   -- var.elim.:  1000/8298          
c   -- var.elim.:  2000/8298          
c   -- var.elim.:  3000/8298          
c   -- var.elim.:  4000/8298          
c   -- var.elim.:  5000/8298          
c   -- var.elim.:  6000/8298          
c   -- var.elim.:  7000/8298          
c   -- var.elim.:  8000/8298          
c   -- var.elim.:  8298/8298          
c   -- var.elim.:  1000/7208          
c   -- var.elim.:  2000/7208          
c   -- var.elim.:  3000/7208          
c   -- var.elim.:  4000/7208          
c   -- var.elim.:  5000/7208          
c   -- var.elim.:  6000/7208          
c   -- var.elim.:  7000/7208          
c   -- var.elim.:  7208/7208          
c   -- var.elim.:  1000/3767          
c   -- var.elim.:  2000/3767          
c   -- var.elim.:  3000/3767          
c   -- var.elim.:  3767/3767          
c   -- var.elim.:  209/209          
c   -- var.elim.:  390/390          
c   -- subsuming                       
c   -- var.elim.:  1000/10869          
c   -- var.elim.:  2000/10869          
c   -- var.elim.:  3000/10869          
c   -- var.elim.:  4000/10869          
c   -- var.elim.:  5000/10869          
c   -- var.elim.:  6000/10869          
c   -- var.elim.:  7000/10869          
c   -- var.elim.:  8000/10869          
c   -- var.elim.:  9000/10869          
c   -- var.elim.:  10000/10869          
c   -- var.elim.:  10869/10869          
c   -- var.elim.:  1000/5068          
c   -- var.elim.:  2000/5068          
c   -- var.elim.:  3000/5068          
c   -- var.elim.:  4000/5068          
c   -- var.elim.:  5000/5068          
c   -- var.elim.:  5068/5068          
c   -- var.elim.:  1000/5976          
c   -- var.elim.:  2000/5976          
c   -- var.elim.:  3000/5976          
c   -- var.elim.:  4000/5976          
c   -- var.elim.:  5000/5976          
c   -- var.elim.:  5976/5976          
c   -- var.elim.:  1000/6683          
c   -- var.elim.:  2000/6683          
c   -- var.elim.:  3000/6683          
c   -- var.elim.:  4000/6683          
c   -- var.elim.:  5000/6683          
c   -- var.elim.:  6000/6683          
c   -- var.elim.:  6683/6683          
c   -- var.elim.:  1000/4423          
c   -- var.elim.:  2000/4423          
c   -- var.elim.:  3000/4423          
c   -- var.elim.:  4000/4423          
c   -- var.elim.:  4423/4423          
c   -- var.elim.:  1000/1046          
c   -- var.elim.:  1046/1046          
c   -- var.elim.:  772/772          
c   -- subsuming                       
c   -- var.elim.:  1000/7158          
c   -- var.elim.:  2000/7158          
c   -- var.elim.:  3000/7158          
c   -- var.elim.:  4000/7158          
c   -- var.elim.:  5000/7158          
c   -- var.elim.:  6000/7158          
c   -- var.elim.:  7000/7158          
c   -- var.elim.:  7158/7158          
c   -- var.elim.:  1000/4508          
c   -- var.elim.:  2000/4508          
c   -- var.elim.:  3000/4508          
c   -- var.elim.:  4000/4508          
c   -- var.elim.:  4508/4508          
c   -- var.elim.:  1000/2897          
c   -- var.elim.:  2000/2897          
c   -- var.elim.:  2897/2897          
c   -- var.elim.:  461/461          
c   -- subsuming                       
c   -- var.elim.:  1000/5219          
c   -- var.elim.:  2000/5219          
c   -- var.elim.:  3000/5219          
c   -- var.elim.:  4000/5219          
c   -- var.elim.:  5000/5219          
c   -- var.elim.:  5219/5219          
c   -- var.elim.:  1000/2105          
c   -- var.elim.:  2000/2105          
c   -- var.elim.:  2105/2105          
c   -- var.elim.:  1000/1134          
c   -- var.elim.:  1134/1134          
c   -- var.elim.:  1000/2450          
c   -- var.elim.:  2000/2450          
c   -- var.elim.:  2450/2450          
c   -- var.elim.:  16/16          
c |    108194 |   39268   270299 |      --   15122       --      -- |     --   | -13034/44186
c |    108194 |   39268   270299 |   15707   14779   761636    51.5 |  1.215 % |
c |    108294 |   39268   270299 |   17277   14879   764919    51.4 |  1.597 % |
c |    108446 |   39268   270299 |   19005   15031   770643    51.3 |  1.597 % |
c |    108672 |   39268   270299 |   20906   15257   783850    51.4 |  1.597 % |
c |    109011 |   39268   270299 |   22996   15596   798933    51.2 |  1.597 % |
c |    109519 |   39268   270299 |   25296   16104   827308    51.4 |  1.597 % |
c |    110279 |   39268   270299 |   27826   16864   857471    50.8 |  1.597 % |
c |    111419 |   39268   270299 |   30608   18004   927817    51.5 |  1.597 % |
c |    113130 |   39268   270299 |   33669   19715   997908    50.6 |  1.597 % |
c |    115692 |   39268   270299 |   37036   22277  1119626    50.3 |  1.597 % |
c |    119538 |   39227   270042 |   40697   26105  1325398    50.8 |  1.608 % |
c |    125305 |   39227   270042 |   44767   31872  1617002    50.7 |  1.608 % |
c |    133954 |   39227   270042 |   49244   40521  2193724    54.1 |  1.608 % |
c |    146928 |   39227   270042 |   54168   18889  1039632    55.0 |  1.608 % |
c |    166392 |   39024   268286 |   59277   38346  1992716    52.0 |  2.026 % |
c |    195584 |   38894   264965 |   64987   21890  1013283    46.3 |  2.227 % |
c |    239376 |   38839   259702 |   71385   16011   715380    44.7 |  2.238 % |
c |    305060 |   37128   194229 |   75064   26254  1372144    52.3 |  4.590 % |
c ==============================================================================
c (current CPU-time: 877.515 s)
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:20188     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    356884 |   61521   251148 |   18456   21065   905187    43.0 |  4.590 % |
c   -- subsuming                       
c   -- var.elim.:  1000/29129          
c   -- var.elim.:  2000/29129          
c   -- var.elim.:  3000/29129          
c   -- var.elim.:  4000/29129          
c   -- var.elim.:  5000/29129          
c   -- var.elim.:  6000/29129          
c   -- var.elim.:  7000/29129          
c   -- var.elim.:  8000/29129          
c   -- var.elim.:  9000/29129          
c   -- var.elim.:  10000/29129          
c   -- var.elim.:  11000/29129          
c   -- var.elim.:  12000/29129          
c   -- var.elim.:  13000/29129          
c   -- var.elim.:  14000/29129          
c   -- var.elim.:  15000/29129          
c   -- var.elim.:  16000/29129          
c   -- var.elim.:  17000/29129          
c   -- var.elim.:  18000/29129          
c   -- var.elim.:  19000/29129          
c   -- var.elim.:  20000/29129          
c   -- var.elim.:  21000/29129          
c   -- var.elim.:  22000/29129          
c   -- var.elim.:  23000/29129          
c   -- var.elim.:  24000/29129          
c   -- var.elim.:  25000/29129          
c   -- var.elim.:  26000/29129          
c   -- var.elim.:  27000/29129          
c   -- var.elim.:  28000/29129          
c   -- var.elim.:  29000/29129          
c   -- var.elim.:  29129/29129          
c   -- var.elim.:  1000/17291          
c   -- var.elim.:  2000/17291          
c   -- var.elim.:  3000/17291          
c   -- var.elim.:  4000/17291          
c   -- var.elim.:  5000/17291          
c   -- var.elim.:  6000/17291          
c   -- var.elim.:  7000/17291          
c   -- var.elim.:  8000/17291          
c   -- var.elim.:  9000/17291          
c   -- var.elim.:  10000/17291          
c   -- var.elim.:  11000/17291          
c   -- var.elim.:  12000/17291          
c   -- var.elim.:  13000/17291          
c   -- var.elim.:  14000/17291          
c   -- var.elim.:  15000/17291          
c   -- var.elim.:  16000/17291          
c   -- var.elim.:  17000/17291          
c   -- var.elim.:  17291/17291          
c   -- var.elim.:  1000/12052          
c   -- var.elim.:  2000/12052          
c   -- var.elim.:  3000/12052          
c   -- var.elim.:  4000/12052          
c   -- var.elim.:  5000/12052          
c   -- var.elim.:  6000/12052          
c   -- var.elim.:  7000/12052          
c   -- var.elim.:  8000/12052          
c   -- var.elim.:  9000/12052          
c   -- var.elim.:  10000/12052          
c   -- var.elim.:  11000/12052          
c   -- var.elim.:  12000/12052          
c   -- var.elim.:  12052/12052          
c   -- var.elim.:  1000/10816          
c   -- var.elim.:  2000/10816          
c   -- var.elim.:  3000/10816          
c   -- var.elim.:  4000/10816          
c   -- var.elim.:  5000/10816          
c   -- var.elim.:  6000/10816          
c   -- var.elim.:  7000/10816          
c   -- var.elim.:  8000/10816          
c   -- var.elim.:  9000/10816          
c   -- var.elim.:  10000/10816          
c   -- var.elim.:  10816/10816          
c   -- var.elim.:  1000/4992          
c   -- var.elim.:  2000/4992          
c   -- var.elim.:  3000/4992          
c   -- var.elim.:  4000/4992          
c   -- var.elim.:  4992/4992          
c   -- var.elim.:  1000/1542          
c   -- var.elim.:  1542/1542          
c   -- var.elim.:  1000/1518          
c   -- var.elim.:  1518/1518          
c   -- subsuming                       
c   -- var.elim.:  1000/13044          
c   -- var.elim.:  2000/13044          
c   -- var.elim.:  3000/13044          
c   -- var.elim.:  4000/13044          
c   -- var.elim.:  5000/13044          
c   -- var.elim.:  6000/13044          
c   -- var.elim.:  7000/13044          
c   -- var.elim.:  8000/13044          
c   -- var.elim.:  9000/13044          
c   -- var.elim.:  10000/13044          
c   -- var.elim.:  11000/13044          
c   -- var.elim.:  12000/13044          
c   -- var.elim.:  13000/13044          
c   -- var.elim.:  13044/13044          
c   -- var.elim.:  1000/7839          
c   -- var.elim.:  2000/7839          
c   -- var.elim.:  3000/7839          
c   -- var.elim.:  4000/7839          
c   -- var.elim.:  5000/7839          
c   -- var.elim.:  6000/7839          
c   -- var.elim.:  7000/7839          
c   -- var.elim.:  7839/7839          
c   -- var.elim.:  1000/5641          
c   -- var.elim.:  2000/5641          
c   -- var.elim.:  3000/5641          
c   -- var.elim.:  4000/5641          
c   -- var.elim.:  5000/5641          
c   -- var.elim.:  5641/5641          
c   -- var.elim.:  1000/4603          
c   -- var.elim.:  2000/4603          
c   -- var.elim.:  3000/4603          
c   -- var.elim.:  4000/4603          
c   -- var.elim.:  4603/4603          
c   -- var.elim.:  1000/3126          
c   -- var.elim.:  2000/3126          
c   -- var.elim.:  3000/3126          
c   -- var.elim.:  3126/3126          
c   -- var.elim.:  1000/2077          
c   -- var.elim.:  2000/2077          
c   -- var.elim.:  2077/2077          
c   -- subsuming                       
c   -- var.elim.:  1000/8342          
c   -- var.elim.:  2000/8342          
c   -- var.elim.:  3000/8342          
c   -- var.elim.:  4000/8342          
c   -- var.elim.:  5000/8342          
c   -- var.elim.:  6000/8342          
c   -- var.elim.:  7000/8342          
c   -- var.elim.:  8000/8342          
c   -- var.elim.:  8342/8342          
c   -- var.elim.:  1000/4966          
c   -- var.elim.:  2000/4966          
c   -- var.elim.:  3000/4966          
c   -- var.elim.:  4000/4966          
c   -- var.elim.:  4966/4966          
c   -- var.elim.:  1000/4259          
c   -- var.elim.:  2000/4259          
c   -- var.elim.:  3000/4259          
c   -- var.elim.:  4000/4259          
c   -- var.elim.:  4259/4259          
c   -- var.elim.:  1000/2509          
c   -- var.elim.:  2000/2509          
c   -- var.elim.:  2509/2509          
c   -- subsuming                       
c   -- var.elim.:  1000/6404          
c   -- var.elim.:  2000/6404          
c   -- var.elim.:  3000/6404          
c   -- var.elim.:  4000/6404          
c   -- var.elim.:  5000/6404          
c   -- var.elim.:  6000/6404          
c   -- var.elim.:  6404/6404          
c   -- var.elim.:  810/810          
c |    356884 |   46747   295853 |      --   21065       --      -- |     --   | -14612/45127
c |    356884 |   46747   295853 |   18698   16161   601252    37.2 |  4.590 % |
c |    356984 |   46747   295853 |   20568   16261   608736    37.4 |  5.984 % |
c |    357134 |   46665   295263 |   22585   16404   617823    37.7 |  6.135 % |
c |    357359 |   46622   294853 |   24821   16628   631961    38.0 |  6.231 % |
c |    357696 |   46622   294853 |   27303   16965   650929    38.4 |  6.231 % |
c |    358202 |   46622   294853 |   30034   17471   676008    38.7 |  6.231 % |
c |    358965 |   46622   294853 |   33037   18234   711776    39.0 |  6.231 % |
c |    360106 |   46618   294800 |   36338   19363   786627    40.6 |  6.240 % |
c |    361814 |   46560   294411 |   39922   21070   898131    42.6 |  6.364 % |
c |    364378 |   46090   281503 |   43471   23629  1059651    44.8 |  6.922 % |
c |    368225 |   45897   280093 |   47617   27437  1356867    49.5 |  7.310 % |
c ==============================================================================
c (current CPU-time: 1075.93 s)
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    373650 |   51748   240152 |   15524   32653  1669548    51.1 |  7.310 % |
c   -- subsuming                       
c   -- var.elim.:  1000/21713          
c   -- var.elim.:  2000/21713          
c   -- var.elim.:  3000/21713          
c   -- var.elim.:  4000/21713          
c   -- var.elim.:  5000/21713          
c   -- var.elim.:  6000/21713          
c   -- var.elim.:  7000/21713          
c   -- var.elim.:  8000/21713          
c   -- var.elim.:  9000/21713          
c   -- var.elim.:  10000/21713          
c   -- var.elim.:  11000/21713          
c   -- var.elim.:  12000/21713          
c   -- var.elim.:  13000/21713          
c   -- var.elim.:  14000/21713          
c   -- var.elim.:  15000/21713          
c   -- var.elim.:  16000/21713          
c   -- var.elim.:  17000/21713          
c   -- var.elim.:  18000/21713          
c   -- var.elim.:  19000/21713          
c   -- var.elim.:  20000/21713          
c   -- var.elim.:  21000/21713          
c   -- var.elim.:  21713/21713          
c   -- var.elim.:  1000/12335          
c   -- var.elim.:  2000/12335          
c   -- var.elim.:  3000/12335          
c   -- var.elim.:  4000/12335          
c   -- var.elim.:  5000/12335          
c   -- var.elim.:  6000/12335          
c   -- var.elim.:  7000/12335          
c   -- var.elim.:  8000/12335          
c   -- var.elim.:  9000/12335          
c   -- var.elim.:  10000/12335          
c   -- var.elim.:  11000/12335          
c   -- var.elim.:  12000/12335          
c   -- var.elim.:  12335/12335          
c   -- var.elim.:  1000/8771          
c   -- var.elim.:  2000/8771          
c   -- var.elim.:  3000/8771          
c   -- var.elim.:  4000/8771          
c   -- var.elim.:  5000/8771          
c   -- var.elim.:  6000/8771          
c   -- var.elim.:  7000/8771          
c   -- var.elim.:  8000/8771          
c   -- var.elim.:  8771/8771          
c   -- var.elim.:  1000/7854          
c   -- var.elim.:  2000/7854          
c   -- var.elim.:  3000/7854          
c   -- var.elim.:  4000/7854          
c   -- var.elim.:  5000/7854          
c   -- var.elim.:  6000/7854          
c   -- var.elim.:  7000/7854          
c   -- var.elim.:  7854/7854          
c   -- var.elim.:  1000/4519          
c   -- var.elim.:  2000/4519          
c   -- var.elim.:  3000/4519          
c   -- var.elim.:  4000/4519          
c   -- var.elim.:  4519/4519          
c   -- var.elim.:  1000/2869          
c   -- var.elim.:  2000/2869          
c   -- var.elim.:  2869/2869          
c   -- var.elim.:  1000/1449          
c   -- var.elim.:  1449/1449          
c   -- var.elim.:  511/511          
c   -- var.elim.:  2/2          
c   -- subsuming                       
c   -- var.elim.:  1000/4441          
c   -- var.elim.:  2000/4441          
c   -- var.elim.:  3000/4441          
c   -- var.elim.:  4000/4441          
c   -- var.elim.:  4441/4441          
c   -- var.elim.:  30/30          
c |    373650 |   40308   224044 |      --   32653       --      -- |     --   | -11431/-16010
c |    373650 |   40308   224044 |   16123   29576  1399893    47.3 |  7.310 % |
c |    373750 |   40308   224044 |   17735   15270   700816    45.9 | 12.393 % |
c |    373900 |   39458   205984 |   19097   15416   707831    45.9 | 13.263 % |
c |    374126 |   38826   201016 |   20670   15601   711264    45.6 | 14.333 % |
c ==============================================================================
c [1mOptimal solution: 64[0m
s OPTIMUM FOUND
v -v1 v2 v3 v4 -v5 -v6 -v7 -v8 -v9 -v10 -v11 -v12 -v13 v14 -v15 -v16 v17 -v18 -v19 -v20 v21 -v22 -v23 -v24 -v25 -v26 -v27 -v28 -v29 -v30 -v31 -v32 -v33 v34 -v35 -v36 -v37 -v38 -v39 -v40 -v41 -v42 -v43 -v44 v45 -v46 -v47 -v48 -v49 -v50 -v51 -v52 -v53 -v54 v55 -v56 -v57 -v58 v59 -v60 -v61 -v62 -v63 -v64 -v65 -v66 -v67 -v68 -v69 v70 -v71 -v72 -v73 -v74 -v75 -v76 -v77 -v78 v79 -v80 -v81 -v82 v83 -v84 v85 -v86 -v87 -v88 v89 -v90 -v91 -v92 -v93 v94 -v95 -v96 -v97 -v98 -v99 -v100 -v101 -v102 -v103 -v104 -v105 v106 -v107 -v108 -v109 -v110 -v111 -v112 -v113 v114 -v115 -v116 -v117 v118 -v119 -v120 -v121 -v122 -v123 -v124 -v125 -v126 -v127 -v128 -v129 -v130 -v131 -v132 -v133 -v134 -v135 -v136 -v137 -v138 -v139 -v140 -v141 -v142 v143 -v144 -v145 -v146 -v147 -v148 -v149 -v150 -v151 -v152 -v153 -v154 v155 v156 -v157 -v158 -v159 -v160 -v161 -v162 -v163 -v164 -v165 -v166 -v167 v168 -v169 -v170 -v171 -v172 -v173 -v174 -v175 -v176 -v177 -v178 -v179 v180 -v181 -v182 -v183 v184 -v185 -v186 -v187 v188 -v189 -v190 -v191 v192 -v193 v194 v195 -v196 -v197 -v198 -v199 -v200 -v201 -v202 -v203 -v204 -v205 v206 -v207 -v208 -v209 v210 -v211 -v212 -v213 -v214 -v215 -v216 -v217 -v218 -v219 -v220 -v221 -v222 -v223 -v224 -v225 -v226 -v227 v228 -v229 -v230 -v231 -v232 -v233 -v234 -v235 -v236 -v237 -v238 -v239 -v240 -v241 -v242 -v243 -v244 -v245 -v246 v247 v248 -v249 -v250 -v251 -v252 -v253 -v254 -v255 -v256 -v257 -v258 v259 -v260 -v261 -v262 -v263 -v264 -v265 -v266 -v267 -v268 -v269 -v270 -v271 v272 v273 -v274 -v275 -v276 -v277 -v278 -v279 -v280 -v281 -v282 -v283 v284 -v285 -v286 -v287 -v288 -v289 -v290 -v291 -v292 -v293 -v294 -v295 -v296 -v297 -v298 -v299 -v300 -v301 -v302 -v303 -v304 -v305 v306 -v307 -v308 -v309 -v310 -v311 -v312 -v313 -v314 -v315 -v316 -v317 -v318 -v319 -v320 -v321 -v322 -v323 -v324 -v325 -v326 -v327 -v328 -v329 -v330 v331 -v332 -v333 -v334 v335 -v336 -v337 -v338 -v339 -v340 -v341 -v342 -v343 v344 -v345 -v346 -v347 -v348 -v349 -v350 -v351 -v352 -v353 -v354 -v355 -v356 -v357 -v358 v359 -v360 v361 v362 -v363 -v364 -v365 v366 -v367 -v368 -v369 -v370 -v371 -v372 -v373 -v374 v375 -v376 -v377 -v378 -v379 -v380 -v381 -v382 -v383 -v384 -v385 -v386 -v387 v388 v389 -v390 -v391 -v392 -v393 -v394 -v395 -v396 -v397 -v398 -v399 -v400 -v401 -v402 v403 -v404 -v405 -v406 -v407 -v408 -v409 -v410 -v411 -v412 -v413 -v414 -v415 -v416 -v417 -v418 -v419 -v420 -v421 -v422 -v423 v424 -v425 -v426 -v427 -v428 -v429 -v430 -v431 -v432 -v433 -v434 v435 -v436 -v437 -v438 -v439 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 -v451 -v452 -v453 -v454 -v455 -v456 -v457 -v458 -v459 -v460 -v461 -v462 -v463 -v464 -v465 -v466 -v467 -v468 v469 -v470 -v471 -v472 v473 -v474 -v475 -v476 v477 -v478 -v479 -v480 v481 -v482 -v483 -v484 -v485 -v486 -v487 -v488 -v489 -v490 -v491 -v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 -v502 -v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 -v511 -v512 v513 -v514 -v515 -v516 -v517 -v518 -v519 -v520 -v521 -v522 -v523 -v524 -v525 -v526 -v527 v528 -v529 -v530 -v531 -v532 -v533 -v534 -v535 -v536 v537 -v538 -v539 -v540 -v541 -v542 -v543 -v544 -v545 -v546 -v547 v548 -v549 -v550 -v551 -v552 -v553 -v554 -v555 -v556 v557 -v558 -v559 -v560 -v561 -v562 -v563 -v564 -v565 -v566 -v567 -v568 -v569 -v570 -v571 -v572 -v573 -v574 -v575 -v576 -v577 -v578 -v579 -v580 -v581 -v582 -v583 -v584 -v585 v586 -v587 -v588 -v589 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 v605 -v606 -v607 -v608 -v609 -v610 -v611 -v612 -v613 -v614 -v615 -v616 -v617 -v618 -v619 -v620 -v621 -v622 -v623 -v624 -v625 -v626 -v627 -v628 -v629 -v630 -v631 -v632 -v633 -v634 -v635 -v636 -v637 -v638 -v639 v640 -v641 -v642 -v643 -v644 -v645 -v646 -v647 -v648
c _______________________________________________________________________________
c 
c restarts              : 60
c conflicts             : 374350         (338 /sec)
c decisions             : 607562         (549 /sec)
c propagations          : 83110024       (75118 /sec)
c inspects              : 1169889725     (1057391 /sec)
c CPU time              : 1106.39 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.76 0.91 0.89 2/54 3098
Raw data (stat): 3098 (runsolver) R 3097 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422065367 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.0008 s]
Raw data (loadavg): 0.80 0.91 0.89 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4280 0 0 0 982 15 0 0 25 0 1 0 422065367 19472384 4117 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4754 4117 603 41 0 4713 0
vsize: 19016
[startup+20.0012 s]
Raw data (loadavg): 0.83 0.91 0.89 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4354 0 0 0 1981 17 0 0 25 0 1 0 422065367 19742720 4191 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4820 4191 603 41 0 4779 0
vsize: 19280
[startup+30.0018 s]
Raw data (loadavg): 0.85 0.92 0.89 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4389 0 0 0 2980 18 0 0 25 0 1 0 422065367 19877888 4226 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4853 4226 603 41 0 4812 0
vsize: 19412
[startup+40.0013 s]
Raw data (loadavg): 0.87 0.92 0.89 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4530 0 0 0 3979 18 0 0 25 0 1 0 422065367 20402176 4345 4294967295 134512640 134672761 3221224560 3221222784 134621194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4981 4345 603 41 0 4940 0
vsize: 19924
[startup+50.0014 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4530 0 0 0 4979 18 0 0 25 0 1 0 422065367 20402176 4345 4294967295 134512640 134672761 3221224560 3221222960 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4981 4345 603 41 0 4940 0
vsize: 19924
[startup+60.0022 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4534 0 0 0 5978 20 0 0 25 0 1 0 422065367 19922944 4258 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4864 4258 603 41 0 4823 0
vsize: 19456
[startup+70.0019 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4534 0 0 0 6975 22 0 0 25 0 1 0 422065367 19922944 4258 4294967295 134512640 134672761 3221224560 3221223008 134644008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4864 4258 603 41 0 4823 0
vsize: 19456
[startup+80.0032 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4537 0 0 0 7973 24 0 0 25 0 1 0 422065367 20025344 4261 4294967295 134512640 134672761 3221224560 3221223040 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4889 4261 603 41 0 4848 0
vsize: 19556
[startup+90.004 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4667 0 0 0 8973 24 0 0 25 0 1 0 422065367 20410368 4362 4294967295 134512640 134672761 3221224560 3221222892 1075350346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4983 4362 603 41 0 4942 0
vsize: 19932
[startup+100.003 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4667 0 0 0 9971 26 0 0 25 0 1 0 422065367 20025344 4280 4294967295 134512640 134672761 3221224560 3221223008 134643624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4889 4280 603 41 0 4848 0
vsize: 19556
[startup+110.005 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4667 0 0 0 10970 26 0 0 25 0 1 0 422065367 20025344 4280 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4889 4280 603 41 0 4848 0
vsize: 19556
[startup+120.005 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4667 0 0 0 11969 26 0 0 25 0 1 0 422065367 20025344 4280 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4889 4280 603 41 0 4848 0
vsize: 19556
[startup+130.006 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4750 0 0 0 12969 27 0 0 25 0 1 0 422065367 20631552 4363 4294967295 134512640 134672761 3221224560 3221223024 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5037 4363 603 41 0 4996 0
vsize: 20148
[startup+140.006 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4750 0 0 0 13969 27 0 0 25 0 1 0 422065367 20631552 4363 4294967295 134512640 134672761 3221224560 3221223104 134621164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5037 4363 603 41 0 4996 0
vsize: 20148
[startup+150.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4750 0 0 0 14968 28 0 0 25 0 1 0 422065367 20025344 4281 4294967295 134512640 134672761 3221224560 3221223008 134643499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4889 4281 603 41 0 4848 0
vsize: 19556
[startup+160.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4750 0 0 0 15967 29 0 0 25 0 1 0 422065367 20025344 4281 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4889 4281 603 41 0 4848 0
vsize: 19556
[startup+170.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4827 0 0 0 16967 29 0 0 25 0 1 0 422065367 20414464 4358 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4984 4358 603 41 0 4943 0
vsize: 19936
[startup+180.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 4827 0 0 0 17967 29 0 0 25 0 1 0 422065367 20025344 4283 4294967295 134512640 134672761 3221224560 3221223008 134643651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4889 4283 603 41 0 4848 0
vsize: 19556
[startup+190.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 5440 0 0 0 18966 31 0 0 25 0 1 0 422065367 22597632 4896 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5517 4896 603 41 0 5476 0
vsize: 22068
[startup+200.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 6249 0 0 0 19963 33 0 0 25 0 1 0 422065367 25899008 5705 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6323 5705 603 41 0 6282 0
vsize: 25292
[startup+210.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 6755 0 0 0 20962 35 0 0 25 0 1 0 422065367 28196864 6211 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6884 6211 603 41 0 6843 0
vsize: 27536
[startup+220.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 6755 0 0 0 21962 35 0 0 25 0 1 0 422065367 28196864 6211 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6884 6211 603 41 0 6843 0
vsize: 27536
[startup+230.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 6815 0 0 0 22962 35 0 0 25 0 1 0 422065367 28459008 6271 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6948 6271 603 41 0 6907 0
vsize: 27792
[startup+240.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 7184 0 0 0 23960 37 0 0 25 0 1 0 422065367 30072832 6640 4294967295 134512640 134672761 3221224560 3221223600 134612797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7342 6640 603 41 0 7301 0
vsize: 29368
[startup+250.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 7416 0 0 0 24960 37 0 0 25 0 1 0 422065367 30724096 6832 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7501 6832 603 41 0 7460 0
vsize: 30004
[startup+260.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 7416 0 0 0 25960 37 0 0 25 0 1 0 422065367 30724096 6832 4294967295 134512640 134672761 3221224560 3221223744 134615622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7501 6832 603 41 0 7460 0
vsize: 30004
[startup+270.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 7446 0 0 0 26960 38 0 0 25 0 1 0 422065367 30920704 6862 4294967295 134512640 134672761 3221224560 3221223496 1075350051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7549 6862 603 41 0 7508 0
vsize: 30196
[startup+280.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 7490 0 0 0 27961 38 0 0 25 0 1 0 422065367 31117312 6906 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7597 6906 603 41 0 7556 0
vsize: 30388
[startup+290.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 7688 0 0 0 28960 38 0 0 25 0 1 0 422065367 31936512 7087 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7797 7087 603 41 0 7756 0
vsize: 31188
[startup+300.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9174 0 0 0 29948 50 0 0 25 0 1 0 422065367 36315136 7804 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7804 603 41 0 8825 0
vsize: 35464
[startup+310.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9174 0 0 0 30947 51 0 0 25 0 1 0 422065367 36315136 7804 4294967295 134512640 134672761 3221224560 3221223008 134643948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7804 603 41 0 8825 0
vsize: 35464
[startup+320.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9174 0 0 0 31946 52 0 0 25 0 1 0 422065367 36315136 7804 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7804 603 41 0 8825 0
vsize: 35464
[startup+330.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9174 0 0 0 32945 53 0 0 25 0 1 0 422065367 36315136 7804 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7804 603 41 0 8825 0
vsize: 35464
[startup+340.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9282 0 0 0 33945 53 0 0 25 0 1 0 422065367 36782080 7912 4294967295 134512640 134672761 3221224560 3221223024 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8980 7912 603 41 0 8939 0
vsize: 35920
[startup+350.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9282 0 0 0 34944 55 0 0 25 0 1 0 422065367 36315136 7811 4294967295 134512640 134672761 3221224560 3221223008 134643468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7811 603 41 0 8825 0
vsize: 35464
[startup+360.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9282 0 0 0 35943 55 0 0 25 0 1 0 422065367 36315136 7811 4294967295 134512640 134672761 3221224560 3221223008 134643539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7811 603 41 0 8825 0
vsize: 35464
[startup+370.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9283 0 0 0 36942 57 0 0 25 0 1 0 422065367 36315136 7812 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7812 603 41 0 8825 0
vsize: 35464
[startup+380.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9283 0 0 0 37942 57 0 0 25 0 1 0 422065367 36315136 7812 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7812 603 41 0 8825 0
vsize: 35464
[startup+390.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9387 0 0 0 38942 57 0 0 25 0 1 0 422065367 36978688 7916 4294967295 134512640 134672761 3221224560 3221223052 134642774 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9028 7916 603 41 0 8987 0
vsize: 36112
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9387 0 0 0 39941 58 0 0 25 0 1 0 422065367 36315136 7812 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7812 603 41 0 8825 0
vsize: 35464
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9387 0 0 0 40941 58 0 0 25 0 1 0 422065367 36315136 7812 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7812 603 41 0 8825 0
vsize: 35464
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9387 0 0 0 41941 58 0 0 25 0 1 0 422065367 36315136 7812 4294967295 134512640 134672761 3221224560 3221223008 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7812 603 41 0 8825 0
vsize: 35464
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9491 0 0 0 42941 58 0 0 25 0 1 0 422065367 36315136 7812 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7812 603 41 0 8825 0
vsize: 35464
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9491 0 0 0 43941 58 0 0 25 0 1 0 422065367 36315136 7812 4294967295 134512640 134672761 3221224560 3221223072 134638304 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7812 603 41 0 8825 0
vsize: 35464
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9491 0 0 0 44942 58 0 0 25 0 1 0 422065367 36315136 7812 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7812 603 41 0 8825 0
vsize: 35464
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9491 0 0 0 45942 58 0 0 25 0 1 0 422065367 36315136 7812 4294967295 134512640 134672761 3221224560 3221223600 134612827 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8866 7812 603 41 0 8825 0
vsize: 35464
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 9947 0 0 0 46940 60 0 0 25 0 1 0 422065367 38289408 8268 4294967295 134512640 134672761 3221224560 3221223744 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9348 8268 603 41 0 9307 0
vsize: 37392
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 10577 0 0 0 47938 62 0 0 25 0 1 0 422065367 40828928 8898 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9968 8898 603 41 0 9927 0
vsize: 39872
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 10861 0 0 0 48938 63 0 0 25 0 1 0 422065367 41758720 9133 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10195 9133 603 41 0 10154 0
vsize: 40780
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 10862 0 0 0 49938 63 0 0 25 0 1 0 422065367 41758720 9134 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10195 9134 603 41 0 10154 0
vsize: 40780
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 10862 0 0 0 50938 63 0 0 25 0 1 0 422065367 41758720 9134 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10195 9134 603 41 0 10154 0
vsize: 40780
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 10862 0 0 0 51938 63 0 0 25 0 1 0 422065367 41758720 9134 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10195 9134 603 41 0 10154 0
vsize: 40780
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11128 0 0 0 52938 64 0 0 25 0 1 0 422065367 42844160 9400 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10460 9400 603 41 0 10419 0
vsize: 41840
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11447 0 0 0 53937 64 0 0 25 0 1 0 422065367 43868160 9660 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10710 9660 603 41 0 10669 0
vsize: 42840
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11447 0 0 0 54937 64 0 0 25 0 1 0 422065367 43868160 9660 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10710 9660 603 41 0 10669 0
vsize: 42840
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11447 0 0 0 55938 64 0 0 25 0 1 0 422065367 43868160 9660 4294967295 134512640 134672761 3221224560 3221223744 134616039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10710 9660 603 41 0 10669 0
vsize: 42840
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11449 0 0 0 56938 64 0 0 25 0 1 0 422065367 43868160 9662 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10710 9662 603 41 0 10669 0
vsize: 42840
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11449 0 0 0 57938 64 0 0 25 0 1 0 422065367 43868160 9662 4294967295 134512640 134672761 3221224560 3221223432 1075352757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10710 9662 603 41 0 10669 0
vsize: 42840
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11449 0 0 0 58938 64 0 0 25 0 1 0 422065367 43868160 9662 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10710 9662 603 41 0 10669 0
vsize: 42840
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11464 0 0 0 59938 64 0 0 25 0 1 0 422065367 44064768 9677 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10758 9677 603 41 0 10717 0
vsize: 43032
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11517 0 0 0 60938 64 0 0 25 0 1 0 422065367 44195840 9730 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10790 9730 603 41 0 10749 0
vsize: 43160
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11873 0 0 0 61938 65 0 0 25 0 1 0 422065367 46157824 10086 4294967295 134512640 134672761 3221224560 3221223616 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11269 10086 603 41 0 11228 0
vsize: 45076
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11878 0 0 0 62938 65 0 0 25 0 1 0 422065367 45633536 10026 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11141 10026 603 41 0 11100 0
vsize: 44564
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11879 0 0 0 63938 65 0 0 25 0 1 0 422065367 45633536 10027 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11141 10027 603 41 0 11100 0
vsize: 44564
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11879 0 0 0 64938 65 0 0 25 0 1 0 422065367 45633536 10027 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11141 10027 603 41 0 11100 0
vsize: 44564
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11879 0 0 0 65938 65 0 0 25 0 1 0 422065367 45633536 10027 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11141 10027 603 41 0 11100 0
vsize: 44564
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11881 0 0 0 66939 65 0 0 25 0 1 0 422065367 45633536 10029 4294967295 134512640 134672761 3221224560 3221223744 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11141 10029 603 41 0 11100 0
vsize: 44564
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11881 0 0 0 67939 65 0 0 25 0 1 0 422065367 45633536 10029 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11141 10029 603 41 0 11100 0
vsize: 44564
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11919 0 0 0 68939 65 0 0 25 0 1 0 422065367 45895680 10067 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11205 10067 603 41 0 11164 0
vsize: 44820
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 11941 0 0 0 69939 65 0 0 25 0 1 0 422065367 46157824 10089 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11269 10089 603 41 0 11228 0
vsize: 45076
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12137 0 0 0 70938 66 0 0 25 0 1 0 422065367 46833664 10285 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11434 10285 603 41 0 11393 0
vsize: 45736
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12466 0 0 0 71938 67 0 0 25 0 1 0 422065367 48300032 10614 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11792 10614 603 41 0 11751 0
vsize: 47168
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12685 0 0 0 72937 68 0 0 25 0 1 0 422065367 48619520 10730 4294967295 134512640 134672761 3221224560 3221223744 134616005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11870 10730 603 41 0 11829 0
vsize: 47480
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12685 0 0 0 73937 68 0 0 25 0 1 0 422065367 48619520 10730 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11870 10730 603 41 0 11829 0
vsize: 47480
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12685 0 0 0 74938 68 0 0 25 0 1 0 422065367 48619520 10730 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11870 10730 603 41 0 11829 0
vsize: 47480
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12685 0 0 0 75938 68 0 0 25 0 1 0 422065367 48619520 10730 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11870 10730 603 41 0 11829 0
vsize: 47480
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12685 0 0 0 76938 68 0 0 25 0 1 0 422065367 48619520 10730 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11870 10730 603 41 0 11829 0
vsize: 47480
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12685 0 0 0 77938 68 0 0 25 0 1 0 422065367 48619520 10730 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11870 10730 603 41 0 11829 0
vsize: 47480
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12689 0 0 0 78938 68 0 0 25 0 1 0 422065367 48619520 10734 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11870 10734 603 41 0 11829 0
vsize: 47480
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12689 0 0 0 79938 68 0 0 25 0 1 0 422065367 48619520 10734 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11870 10734 603 41 0 11829 0
vsize: 47480
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12695 0 0 0 80939 68 0 0 25 0 1 0 422065367 48783360 10740 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11910 10740 603 41 0 11869 0
vsize: 47640
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12695 0 0 0 81939 68 0 0 25 0 1 0 422065367 48783360 10740 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11910 10740 603 41 0 11869 0
vsize: 47640
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12695 0 0 0 82939 68 0 0 25 0 1 0 422065367 48783360 10740 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11910 10740 603 41 0 11869 0
vsize: 47640
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12723 0 0 0 83939 68 0 0 25 0 1 0 422065367 48930816 10768 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11946 10768 603 41 0 11905 0
vsize: 47784
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12723 0 0 0 84939 68 0 0 25 0 1 0 422065367 48930816 10768 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11946 10768 603 41 0 11905 0
vsize: 47784
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12821 0 0 0 85939 68 0 0 25 0 1 0 422065367 49328128 10866 4294967295 134512640 134672761 3221224560 3221223744 134615779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12043 10866 603 41 0 12002 0
vsize: 48172
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 12985 0 0 0 86938 69 0 0 25 0 1 0 422065367 49983488 11030 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11030 603 41 0 12162 0
vsize: 48812
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15075 0 0 0 87927 81 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221222912 134605448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15075 0 0 0 88917 91 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15075 0 0 0 89915 92 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221223008 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15075 0 0 0 90913 94 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221222944 134631846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15075 0 0 0 91911 95 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221223008 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15075 0 0 0 92911 95 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15136 0 0 0 93911 96 0 0 25 0 1 0 422065367 53755904 11987 4294967295 134512640 134672761 3221224560 3221223052 134642716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13124 11987 603 41 0 13083 0
vsize: 52496
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15136 0 0 0 94911 96 0 0 25 0 1 0 422065367 53755904 11987 4294967295 134512640 134672761 3221224560 3221223104 134621186 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13124 11987 603 41 0 13083 0
vsize: 52496
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15136 0 0 0 95908 98 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+970.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15136 0 0 0 96906 100 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221223008 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+980.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15136 0 0 0 97905 101 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221223008 134643545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15197 0 0 0 98905 101 0 0 25 0 1 0 422065367 53809152 11987 4294967295 134512640 134672761 3221224560 3221222892 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13137 11987 603 41 0 13096 0
vsize: 52548
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15197 0 0 0 99905 101 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221221456 134645947 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15197 0 0 0 100903 103 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15197 0 0 0 101902 104 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221223008 134643636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15258 0 0 0 102903 104 0 0 25 0 1 0 422065367 53407744 11926 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11926 603 41 0 12998 0
vsize: 52156
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15261 0 0 0 103903 104 0 0 25 0 1 0 422065367 53407744 11929 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11929 603 41 0 12998 0
vsize: 52156
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15261 0 0 0 104903 104 0 0 25 0 1 0 422065367 53407744 11929 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11929 603 41 0 12998 0
vsize: 52156
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15261 0 0 0 105903 104 0 0 25 0 1 0 422065367 53407744 11929 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11929 603 41 0 12998 0
vsize: 52156
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 15261 0 0 0 106903 104 0 0 25 0 1 0 422065367 53407744 11929 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13039 11929 603 41 0 12998 0
vsize: 52156
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 17415 0 0 0 107889 119 0 0 25 0 1 0 422065367 58826752 12078 4294967295 134512640 134672761 3221224560 3221223008 134643777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 12078 603 41 0 14321 0
vsize: 57448
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 17415 0 0 0 108886 121 0 0 25 0 1 0 422065367 58826752 12078 4294967295 134512640 134672761 3221224560 3221223008 134643777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14362 12078 603 41 0 14321 0
vsize: 57448
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 17415 0 0 0 109885 123 0 0 25 0 1 0 422065367 58826752 12078 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14362 12078 603 41 0 14321 0
vsize: 57448
[startup+1107.65 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 3098
Raw data (stat): 3098 (minisat+) R 3097 29151 29150 0 -1 0 17415 0 0 0 109885 123 0 0 25 0 1 0 422065367 58826752 12078 4294967295 134512640 134672761 3221224560 3221223008 134644014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14362 12078 603 41 0 14321 0
vsize: 0

Child status: 30
Real time (s): 1107.65
CPU time (s): 1107.7
CPU user time (s): 1106.42
CPU system time (s): 1.2838
CPU usage (%): 100.005
Max. virtual memory (Kb): 57448
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	64
#### END VERIFIER DATA ####