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/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10c.opb
MD5SUM	31a8734340f0544712ef974997c104b2
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2677632
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	515723936
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	515723936
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	2100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 14814

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 01:31:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19225 boxname=wulflinc15 idbench=1479 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  31a8734340f0544712ef974997c104b2  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-ran10x10c.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-ran10x10c.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-ran10x10c.opb
IDLAUNCH: 19225
/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:        740004 kB
Buffers:         33784 kB
Cached:         236768 kB
SwapCached:       2060 kB
Active:         115604 kB
Inactive:       159804 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        739752 kB
SwapTotal:     2097136 kB
SwapFree:      2094988 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            13500 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:51:54 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 19225 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 2017     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1934     Base: 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 2017     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Adder-cost: 178   maxlim: 8182   bits: 14/13
c ---[ 108]---> Adder-cost: 178   maxlim: 8438   bits: 14/14
c ---[ 106]---> Sorter-cost: 2013     Base: 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2013     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[  99]---> BDD-cost:   10
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   10
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   12
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   10
c ---[  86]---> BDD-cost:   10
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   10
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   12
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   10
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   10
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   12
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   15
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   11
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   14
c ---[  60]---> BDD-cost:   12
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   10
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   10
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   15
c ---[  13]---> BDD-cost:   15
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   10
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   17
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:   17
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   10
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   95243   227095 |   28572       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/30379          
c   -- var.elim.:  2000/30379          
c   -- var.elim.:  3000/30379          
c   -- var.elim.:  4000/30379          
c   -- var.elim.:  5000/30379          
c   -- var.elim.:  6000/30379          
c   -- var.elim.:  7000/30379          
c   -- var.elim.:  8000/30379          
c   -- var.elim.:  9000/30379          
c   -- var.elim.:  10000/30379          
c   -- var.elim.:  11000/30379          
c   -- var.elim.:  12000/30379          
c   -- var.elim.:  13000/30379          
c   -- var.elim.:  14000/30379          
c   -- var.elim.:  15000/30379          
c   -- var.elim.:  16000/30379          
c   -- var.elim.:  17000/30379          
c   -- var.elim.:  18000/30379          
c   -- var.elim.:  19000/30379          
c   -- var.elim.:  20000/30379          
c   -- var.elim.:  21000/30379          
c   -- var.elim.:  22000/30379          
c   -- var.elim.:  23000/30379          
c   -- var.elim.:  24000/30379          
c   -- var.elim.:  25000/30379          
c   -- var.elim.:  26000/30379          
c   -- var.elim.:  27000/30379          
c   -- var.elim.:  28000/30379          
c   -- var.elim.:  29000/30379          
c   -- var.elim.:  30000/30379          
c   -- var.elim.:  30379/30379          
c   -- var.elim.:  1000/17184          
c   -- var.elim.:  2000/17184          
c   -- var.elim.:  3000/17184          
c   -- var.elim.:  4000/17184          
c   -- var.elim.:  5000/17184          
c   -- var.elim.:  6000/17184          
c   -- var.elim.:  7000/17184          
c   -- var.elim.:  8000/17184          
c   -- var.elim.:  9000/17184          
c   -- var.elim.:  10000/17184          
c   -- var.elim.:  11000/17184          
c   -- var.elim.:  12000/17184          
c   -- var.elim.:  13000/17184          
c   -- var.elim.:  14000/17184          
c   -- var.elim.:  15000/17184          
c   -- var.elim.:  16000/17184          
c   -- var.elim.:  17000/17184          
c   -- var.elim.:  17184/17184          
c   -- var.elim.:  147/147          
c   -- subsuming                       
c   -- var.elim.:  1000/2273          
c   -- var.elim.:  2000/2273          
c   -- var.elim.:  2273/2273          
c   -- var.elim.:  1000/1855          
c   -- var.elim.:  1855/1855          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  512/512          
c   -- var.elim.:  388/388          
c   -- var.elim.:  24/24          
c   -- subsuming                       
c   -- var.elim.:  170/170          
c   -- var.elim.:  176/176          
c   -- subsuming                       
c   -- var.elim.:  131/131          
c   -- var.elim.:  57/57          
c   -- var.elim.:  78/78          
c   -- var.elim.:  57/57          
c |         0 |   81978   246766 |      --       0       --      -- |     --   | -9538/29267
c |         0 |   81978   246766 |   32791       0        0     nan |  0.000 % |
c |       100 |   81978   246766 |   36070     100      597     6.0 | 11.846 % |
c |       251 |   81962   246714 |   39669     248     1336     5.4 | 11.856 % |
c |       476 |   81962   246714 |   43636     473     2637     5.6 | 11.856 % |
c |       814 |   81962   246714 |   48000     811     4575     5.6 | 11.856 % |
c |      1321 |   81962   246714 |   52800    1318     7988     6.1 | 11.856 % |
c |      2080 |   81863   246359 |   58010    2056    13174     6.4 | 11.934 % |
c |      3220 |   81863   246359 |   63811    3196    21361     6.7 | 11.934 % |
c |      4928 |   81863   246359 |   70192    4904    53866    11.0 | 11.934 % |
c |      7490 |   81839   246248 |   77188    7465    74492    10.0 | 11.955 % |
c |     11334 |   81767   245960 |   84833   11302   117077    10.4 | 12.001 % |
c ==============================================================================
c (current CPU-time: 13.8949 s)
c ==============================================================================
c [1mFound solution: 11380588[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4057   maxlim: 1601332   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13516 |  109912   346539 |   32973   13483   159413    11.8 | 12.001 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5388          
c   -- var.elim.:  2000/5388          
c   -- var.elim.:  3000/5388          
c   -- var.elim.:  4000/5388          
c   -- var.elim.:  5000/5388          
c   -- var.elim.:  5388/5388          
c   -- var.elim.:  258/258          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c   -- var.elim.:  54/54          
c   -- var.elim.:  44/44          
c |     13516 |  109744   346259 |      --   13483       --      -- |     --   | -168/-268
c |     13516 |  109744   346259 |   43897   13208   129220     9.8 | 12.001 % |
c |     13616 |  109744   346259 |   48287   13308   129769     9.8 | 10.064 % |
c |     13767 |  109744   346259 |   53116   13459   143488    10.7 | 10.064 % |
c |     13992 |  109695   346074 |   58401   13682   145346    10.6 | 10.089 % |
c |     14331 |  109695   346074 |   64241   14021   152055    10.8 | 10.089 % |
c |     14837 |  109601   345761 |   70605   14516   155372    10.7 | 10.145 % |
c |     15596 |  109601   345761 |   77665   15275   173754    11.4 | 10.145 % |
c ==============================================================================
c (current CPU-time: 18.5862 s)
c ==============================================================================
c [1mFound solution: 11363326[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1618594   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15895 |  109663   346073 |   32898   15574   176973    11.4 | 10.145 % |
c   -- subsuming                       
c   -- var.elim.:  209/209          
c   -- var.elim.:  157/157          
c   -- var.elim.:  28/28          
c   -- var.elim.:  43/43          
c   -- var.elim.:  35/35          
c   -- var.elim.:  51/51          
c   -- var.elim.:  8/8          
c   -- subsuming                       
c   -- var.elim.:  36/36          
c   -- var.elim.:  7/7          
c |     15895 |  109492   345663 |      --   15574       --      -- |     --   | -171/-402
c |     15895 |  109492   345663 |   43796   15555   174958    11.2 | 10.145 % |
c |     15996 |  109492   345663 |   48176   15656   175639    11.2 | 10.240 % |
c |     16148 |  109492   345663 |   52994   15808   181287    11.5 | 10.240 % |
c |     16374 |  109492   345663 |   58293   16034   184431    11.5 | 10.240 % |
c |     16711 |  109485   345634 |   64118   16370   187072    11.4 | 10.244 % |
c |     17217 |  109485   345634 |   70530   16876   190848    11.3 | 10.244 % |
c |     17976 |  109485   345634 |   77583   17635   200550    11.4 | 10.244 % |
c |     19115 |  109474   345597 |   85333   18771   218206    11.6 | 10.248 % |
c ==============================================================================
c (current CPU-time: 25.4311 s)
c ==============================================================================
c [1mFound solution: 6883505[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8   maxlim: 6098415   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19817 |  109494   345770 |   32848   19471   256683    13.2 | 10.248 % |
c   -- subsuming                       
c   -- var.elim.:  133/133          
c   -- var.elim.:  59/59          
c |     19817 |  109469   345690 |      --   19471       --      -- |     --   | -25/-68
c |     19817 |  109469   345690 |   43787   19459   256621    13.2 | 10.248 % |
c |     19917 |  109438   345583 |   48152   19558   257886    13.2 | 10.362 % |
c |     20068 |  109438   345583 |   52967   19709   259047    13.1 | 10.362 % |
c |     20295 |  109396   345423 |   58242   19933   260768    13.1 | 10.384 % |
c |     20632 |  109396   345423 |   64066   20270   267604    13.2 | 10.384 % |
c |     21140 |  109396   345423 |   70473   20778   282511    13.6 | 10.384 % |
c |     21899 |  109396   345423 |   77520   21537   290716    13.5 | 10.384 % |
c |     23039 |  109396   345423 |   85272   22677   328324    14.5 | 10.384 % |
c |     24747 |  109396   345423 |   93800   24385   389284    16.0 | 10.384 % |
c |     27309 |  109396   345423 |  103180   26947   585533    21.7 | 10.384 % |
c |     31153 |  109387   345390 |  113488   30790  1089041    35.4 | 10.388 % |
c |     36919 |  109354   345269 |  124799   36553  1438856    39.4 | 10.405 % |
c |     45570 |  109354   345269 |  137279   45204  2401052    53.1 | 10.405 % |
c |     58544 |  109344   345238 |  150994   58177  3615579    62.1 | 10.410 % |
c |     78005 |  108823   343364 |  165302   77586  4848855    62.5 | 10.727 % |
c ==============================================================================
c (current CPU-time: 133.97 s)
c ==============================================================================
c [1mFound solution: 6197855[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6784065   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     80929 |  108731   343038 |   32619   80486  5099321    63.4 | 10.727 % |
c   -- subsuming                       
c   -- var.elim.:  496/496          
c   -- var.elim.:  351/351          
c   -- var.elim.:  27/27          
c   -- var.elim.:  9/9          
c   -- subsuming                       
c   -- var.elim.:  72/72          
c   -- var.elim.:  49/49          
c |     80929 |  108548   342752 |      --   80486       --      -- |     --   | -183/-278
c |     80929 |  108548   342752 |   43419   76334  4178547    54.7 | 10.727 % |
c |     81029 |  108548   342752 |   47761   16303   824121    50.6 | 10.886 % |
c |     81179 |  108548   342752 |   52537   16453   824904    50.1 | 10.886 % |
c |     81404 |  108548   342752 |   57790   16678   826325    49.5 | 10.886 % |
c |     81741 |  108378   342054 |   63470   17009   828113    48.7 | 10.994 % |
c |     82247 |  108378   342054 |   69817   17515   845291    48.3 | 10.994 % |
c |     83006 |  108358   341989 |   76785   18267   864615    47.3 | 11.006 % |
c |     84146 |  108335   341909 |   84445   19406   881891    45.4 | 11.019 % |
c |     85856 |  108335   341909 |   92890   21116  1165856    55.2 | 11.019 % |
c |     88419 |  108307   341796 |  102152   23674  1257581    53.1 | 11.032 % |
c |     92263 |  108098   341020 |  112151   27514  1433450    52.1 | 11.166 % |
c |     98029 |  108081   340950 |  123347   33267  1819406    54.7 | 11.174 % |
c |    106678 |  108072   340916 |  135670   41913  2374858    56.7 | 11.179 % |
c |    119652 |  108020   340733 |  149165   54884  3609547    65.8 | 11.200 % |
c |    139115 |  107924   340373 |  163936   74340  5933946    79.8 | 11.256 % |
c |    168307 |  107914   340338 |  180313  103531 12753170   123.2 | 11.260 % |
c ==============================================================================
c (current CPU-time: 369.499 s)
c ==============================================================================
c [1mFound solution: 5968057[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7013863   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    173567 |  107932   340498 |   32379  108791 13537825   124.4 | 11.260 % |
c   -- subsuming                       
c   -- var.elim.:  494/494          
c   -- var.elim.:  326/326          
c   -- var.elim.:  13/13          
c   -- var.elim.:  12/12          
c   -- var.elim.:  38/38          
c   -- var.elim.:  29/29          
c   -- subsuming                       
c   -- var.elim.:  130/130          
c   -- var.elim.:  38/38          
c |    173567 |  107708   340148 |      --  108791       --      -- |     --   | -224/-341
c |    173567 |  107708   340148 |   43083   98704  7686754    77.9 | 11.260 % |
c |    173667 |  107681   340058 |   47379   17733  1180888    66.6 | 11.394 % |
c |    173817 |  107681   340058 |   52117   17883  1181978    66.1 | 11.394 % |
c |    174042 |  107681   340058 |   57329   18108  1183460    65.4 | 11.394 % |
c |    174379 |  107681   340058 |   63062   18445  1185601    64.3 | 11.394 % |
c |    174885 |  107681   340058 |   69368   18951  1190284    62.8 | 11.394 % |
c |    175644 |  107681   340058 |   76305   19710  1198607    60.8 | 11.394 % |
c |    176783 |  107681   340058 |   83935   20849  1229967    59.0 | 11.394 % |
c |    178491 |  107681   340058 |   92329   22557  1261966    55.9 | 11.394 % |
c ==============================================================================
c (current CPU-time: 381.179 s)
c ==============================================================================
c [1mFound solution: 5075324[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7906596   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    178807 |  107713   340261 |   32313   22873  1283679    56.1 | 11.394 % |
c   -- subsuming                       
c   -- var.elim.:  96/96          
c   -- var.elim.:  43/43          
c |    178807 |  107693   340215 |      --   22873       --      -- |     --   | -20/-37
c |    178807 |  107693   340215 |   43077   22860  1280902    56.0 | 11.394 % |
c |    178907 |  107693   340215 |   47384   22960  1281434    55.8 | 11.428 % |
c |    179058 |  107693   340215 |   52123   23111  1282319    55.5 | 11.428 % |
c |    179284 |  107693   340215 |   57335   23337  1286838    55.1 | 11.428 % |
c |    179621 |  107693   340215 |   63069   23674  1414621    59.8 | 11.428 % |
c |    180128 |  107693   340215 |   69376   24181  1435032    59.3 | 11.428 % |
c |    180888 |  107693   340215 |   76313   24941  1450726    58.2 | 11.428 % |
c |    182027 |  107438   339359 |   83746   26076  1590571    61.0 | 11.601 % |
c |    183737 |  107438   339359 |   92121   27786  1650782    59.4 | 11.601 % |
c |    186299 |  107438   339359 |  101333   30348  1787116    58.9 | 11.601 % |
c |    190143 |  107438   339359 |  111466   34192  2257963    66.0 | 11.601 % |
c |    195909 |  107438   339359 |  122613   39958  2549146    63.8 | 11.601 % |
c |    204559 |  107434   339342 |  134869   48596  3324475    68.4 | 11.605 % |
c ==============================================================================
c (current CPU-time: 479.828 s)
c ==============================================================================
c [1mFound solution: 3444952[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9536968   bits: 24/24
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    209027 |  107463   339533 |   32238   53064  5413069   102.0 | 11.605 % |
c   -- subsuming                       
c   -- var.elim.:  152/152          
c   -- var.elim.:  72/72          
c   -- var.elim.:  9/9          
c |    209027 |  107364   338994 |      --   53064       --      -- |     --   | -52/-69
c |    209027 |  107364   338994 |   42945   49142  3948940    80.4 | 11.605 % |
c |    209127 |  107232   338525 |   47182   17526  1726415    98.5 | 11.738 % |
c |    209278 |  107232   338525 |   51900   17677  1727503    97.7 | 11.738 % |
c |    209503 |  107223   338496 |   57085   17901  1728702    96.6 | 11.742 % |
c |    209843 |  107223   338496 |   62794   18241  1730559    94.9 | 11.742 % |
c |    210349 |  107223   338496 |   69073   18747  1735322    92.6 | 11.742 % |
c |    211108 |  107223   338496 |   75980   19506  1839052    94.3 | 11.742 % |
c |    212249 |  107214   338467 |   83571   20637  2158464   104.6 | 11.747 % |
c |    213957 |  107214   338467 |   91929   22345  2261963   101.2 | 11.747 % |
c |    216521 |  107124   338159 |  101037   24903  2506259   100.6 | 11.807 % |
c |    220365 |  107124   338159 |  111140   28747  3080473   107.2 | 11.807 % |
c |    226131 |  107124   338159 |  122254   34513  4632333   134.2 | 11.807 % |
c |    234780 |  107068   337970 |  134410   43134  6276431   145.5 | 11.837 % |
c |    247754 |  107068   337970 |  147851   56108 11669767   208.0 | 11.837 % |
c |    267218 |  107068   337970 |  162636   75572 12654683   167.5 | 11.837 % |
c |    296410 |  106707   336718 |  178296  104745 17346268   165.6 | 12.070 % |
c |    340199 |  106322   335399 |  195418  148423 23869628   160.8 | 12.329 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 X1_bit_7 X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 X4_bit_7 -X4_bit_6 X4_bit_5 X4_bit_4 X4_bit_3 X4_bit_2 X4_bit_1 X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 X12_bit_6 X12_bit_5 X12_bit_4 X12_bit_3 X12_bit_2 X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 X13_bit_7 -X13_bit_6 X13_bit_5 -X13_bit_4 X13_bit_3 X13_bit_2 -X13_bit_1 X13_bit0 X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 X16_bit_7 X16_bit_6 -X16_bit_5 X16_bit_4 -X16_bit_3 -X16_bit_2 X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 X35_bit_7 X35_bit_6 X35_bit_5 X35_bit_4 X35_bit_3 X35_bit_2 X35_bit_1 X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X37_bit_7 X37_bit_6 X37_bit_5 X37_bit_4 X37_bit_3 X37_bit_2 X37_bit_1 X37_bit0 X37_bit1 X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 X46_bit1 -X46_bit2 X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 X53_bit_7 X53_bit_6 -X53_bit_5 X53_bit_4 -X53_bit_3 -X53_bit_2 X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 X54_bit_7 -X54_bit_6 X54_bit_5 -X54_bit_4 X54_bit_3 X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 X61_bit_7 X61_bit_6 -X61_bit_5 X61_bit_4 -X61_bit_3 -X61_bit_2 X61_bit_1 -X61_bit0 -X61_bit1 X61_bit2 X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 -X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 X66_bit_7 -X66_bit_6 X66_bit_5 -X66_bit_4 X66_bit_3 X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 X71_bit_6 -X71_bit_5 -X71_bit_4 X71_bit_3 X71_bit_2 -X71_bit_1 X71_bit0 X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 X74_bit_6 X74_bit_5 X74_bit_4 -X74_bit_3 -X74_bit_2 X74_bit_1 X74_bit0 X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 X88_bit0 X88_bit1 -X88_bit2 X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 -X89_bit_6 -X89_bit_5 -X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 -X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 X98_bit_7 X98_bit_6 X98_bit_5 X98_bit_4 X98_bit_3 X98_bit_2 X98_bit_1 -X98_bit0 X98_bit1 -X98_bit2 X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -Y0_bit0 Y1_bit0 -Y2_bit0 -Y3_bit0 Y4_bit0 -Y5_bit0 -Y6_bit0 -Y7_bit0 -Y8_bit0 -Y9_bit0 -Y10_bit0 -Y11_bit0 Y12_bit0 Y13_bit0 -Y14_bit0 Y15_bit0 Y16_bit0 -Y17_bit0 Y18_bit0 -Y19_bit0 Y20_bit0 Y21_bit0 Y22_bit0 Y23_bit0 Y24_bit0 -Y25_bit0 -Y26_bit0 -Y27_bit0 -Y28_bit0 -Y29_bit0 -Y30_bit0 -Y31_bit0 Y32_bit0 -Y33_bit0 -Y34_bit0 Y35_bit0 -Y36_bit0 Y37_bit0 -Y38_bit0 -Y39_bit0 -Y40_bit0 -Y41_bit0 -Y42_bit0 -Y43_bit0 -Y44_bit0 -Y45_bit0 Y46_bit0 -Y47_bit0 -Y48_bit0 -Y49_bit0 -Y50_bit0 -Y51_bit0 -Y52_bit0 Y53_bit0 Y54_bit0 -Y55_bit0 -Y56_bit0 -Y57_bit0 -Y58_bit0 -Y59_bit0 -Y60_bit0 Y61_bit0 -Y62_bit0 -Y63_bit0 -Y64_bit0 -Y65_bit0 Y66_bit0 -Y67_bit0 -Y68_bit0 Y69_b#### 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.92 0.98 0.93 2/54 26760
Raw data (stat): 26760 (runsolver) R 26759 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482916192 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.001 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 5808 0 0 0 981 17 0 0 25 0 1 0 482916192 23175168 5006 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5658 5006 603 41 0 5617 0
vsize: 22632
[startup+20.0021 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 11348 0 0 0 1966 32 0 0 25 0 1 0 482916192 36106240 7521 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8815 7521 603 41 0 8774 0
vsize: 35260
[startup+30.0028 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 12930 0 0 0 2961 36 0 0 25 0 1 0 482916192 36605952 7635 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 7635 603 41 0 8896 0
vsize: 35748
[startup+40.004 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 13261 0 0 0 3960 38 0 0 25 0 1 0 482916192 37945344 7966 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9264 7966 603 41 0 9223 0
vsize: 37056
[startup+50.0047 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 13947 0 0 0 4958 40 0 0 25 0 1 0 482916192 40730624 8652 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9944 8652 603 41 0 9903 0
vsize: 39776
[startup+60.0043 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 14675 0 0 0 5956 42 0 0 25 0 1 0 482916192 43909120 9380 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10720 9380 603 41 0 10679 0
vsize: 42880
[startup+70.0057 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 15376 0 0 0 6955 43 0 0 25 0 1 0 482916192 46673920 10081 4294967295 134512640 134672761 3221224544 3221223688 134616247 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11395 10081 603 41 0 11354 0
vsize: 45580
[startup+80.0062 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 16191 0 0 0 7953 45 0 0 25 0 1 0 482916192 49991680 10896 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12205 10896 603 41 0 12164 0
vsize: 48820
[startup+90.0068 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 16709 0 0 0 8952 47 0 0 25 0 1 0 482916192 52109312 11414 4294967295 134512640 134672761 3221224544 3221223536 134565048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12722 11414 603 41 0 12681 0
vsize: 50888
[startup+100.007 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 17014 0 0 0 9951 48 0 0 25 0 1 0 482916192 53301248 11719 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13013 11719 603 41 0 12972 0
vsize: 52052
[startup+110.007 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 17526 0 0 0 10949 50 0 0 25 0 1 0 482916192 55685120 12231 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13595 12231 603 41 0 13554 0
vsize: 54380
[startup+120.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 17979 0 0 0 11948 52 0 0 25 0 1 0 482916192 57561088 12684 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14053 12684 603 41 0 14012 0
vsize: 56212
[startup+130.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 18292 0 0 0 12947 52 0 0 25 0 1 0 482916192 58761216 12997 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14346 12997 603 41 0 14305 0
vsize: 57384
[startup+140.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 20413 0 0 0 13941 58 0 0 25 0 1 0 482916192 60137472 13323 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14682 13323 603 41 0 14641 0
vsize: 58728
[startup+150.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 20413 0 0 0 14941 58 0 0 25 0 1 0 482916192 60137472 13323 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13323 603 41 0 14641 0
vsize: 58728
[startup+160.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 20413 0 0 0 15941 58 0 0 25 0 1 0 482916192 60137472 13323 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13323 603 41 0 14641 0
vsize: 58728
[startup+170.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 20413 0 0 0 16941 58 0 0 25 0 1 0 482916192 60137472 13323 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13323 603 41 0 14641 0
vsize: 58728
[startup+180.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 20413 0 0 0 17942 58 0 0 25 0 1 0 482916192 60137472 13323 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13323 603 41 0 14641 0
vsize: 58728
[startup+190.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 20413 0 0 0 18942 58 0 0 25 0 1 0 482916192 60137472 13323 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13323 603 41 0 14641 0
vsize: 58728
[startup+200.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 20413 0 0 0 19942 58 0 0 25 0 1 0 482916192 60137472 13323 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13323 603 41 0 14641 0
vsize: 58728
[startup+210.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 20414 0 0 0 20942 58 0 0 25 0 1 0 482916192 60137472 13324 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13324 603 41 0 14641 0
vsize: 58728
[startup+220.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 20414 0 0 0 21942 58 0 0 25 0 1 0 482916192 60137472 13324 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13324 603 41 0 14641 0
vsize: 58728
[startup+230.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 20414 0 0 0 22943 58 0 0 25 0 1 0 482916192 60137472 13324 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13324 603 41 0 14641 0
vsize: 58728
[startup+240.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 20662 0 0 0 23943 59 0 0 25 0 1 0 482916192 61186048 13572 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14938 13572 603 41 0 14897 0
vsize: 59752
[startup+250.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 21043 0 0 0 24942 60 0 0 25 0 1 0 482916192 62771200 13953 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15325 13953 603 41 0 15284 0
vsize: 61300
[startup+260.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 21406 0 0 0 25942 61 0 0 25 0 1 0 482916192 64221184 14316 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15679 14316 603 41 0 15638 0
vsize: 62716
[startup+270.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 23098 0 0 0 26937 66 0 0 25 0 1 0 482916192 71155712 16008 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17372 16008 603 41 0 17331 0
vsize: 69488
[startup+280.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 24946 0 0 0 27932 70 0 0 25 0 1 0 482916192 78749696 17856 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19226 17856 603 41 0 19185 0
vsize: 76904
[startup+290.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 25723 0 0 0 28931 72 0 0 25 0 1 0 482916192 81895424 18633 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19994 18633 603 41 0 19953 0
vsize: 79976
[startup+300.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 26160 0 0 0 29929 74 0 0 25 0 1 0 482916192 83615744 19070 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20414 19070 603 41 0 20373 0
vsize: 81656
[startup+310.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 26447 0 0 0 30929 74 0 0 25 0 1 0 482916192 84807680 19357 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 19357 603 41 0 20664 0
vsize: 82820
[startup+320.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 27135 0 0 0 31927 76 0 0 25 0 1 0 482916192 87674880 20045 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21405 20045 603 41 0 21364 0
vsize: 85620
[startup+330.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 27822 0 0 0 32926 78 0 0 25 0 1 0 482916192 90447872 20732 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22082 20732 603 41 0 22041 0
vsize: 88328
[startup+340.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 28022 0 0 0 33926 78 0 0 25 0 1 0 482916192 91250688 20932 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22278 20932 603 41 0 22237 0
vsize: 89112
[startup+350.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 28237 0 0 0 34925 79 0 0 25 0 1 0 482916192 92176384 21147 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22504 21147 603 41 0 22463 0
vsize: 90016
[startup+360.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 28503 0 0 0 35924 80 0 0 25 0 1 0 482916192 93245440 21413 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22765 21413 603 41 0 22724 0
vsize: 91060
[startup+370.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 29202 0 0 0 36923 82 0 0 25 0 1 0 482916192 96006144 22112 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23439 22112 603 41 0 23398 0
vsize: 93756
[startup+380.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 31095 0 0 0 37917 87 0 0 25 0 1 0 482916192 96583680 22205 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23580 22205 603 41 0 23539 0
vsize: 94320
[startup+390.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 32071 0 0 0 38913 90 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+400.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 32071 0 0 0 39914 90 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+410.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 32071 0 0 0 40914 90 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+420.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 32071 0 0 0 41914 90 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+430.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 32071 0 0 0 42914 90 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223536 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+440.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 32071 0 0 0 43915 90 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+450.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 32071 0 0 0 44915 90 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223584 134612743 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+460.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 32071 0 0 0 45915 90 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+470.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 32071 0 0 0 46915 90 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223480 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+480.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 32071 0 0 0 47915 90 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+490.048 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 48913 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+500.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 49913 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+510.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 50913 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+520.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 51913 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+530.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 52913 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+540.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 53914 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+550.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 54914 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+560.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 55914 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+570.049 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 56914 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+580.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 57914 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+590.051 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 58915 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+600.052 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 59915 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+610.052 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 60915 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+620.053 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 61915 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+630.052 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 62915 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+640.053 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 63916 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+650.054 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 64916 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+660.054 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 65916 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+670.054 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 66916 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223680 134614524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+680.055 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33073 0 0 0 67916 94 0 0 25 0 1 0 482916192 96436224 22171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23544 22171 603 41 0 23503 0
vsize: 94176
[startup+690.055 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 33114 0 0 0 68916 94 0 0 25 0 1 0 482916192 96563200 22212 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23575 22212 603 41 0 23534 0
vsize: 94300
[startup+700.056 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 34331 0 0 0 69914 96 0 0 25 0 1 0 482916192 101548032 23429 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24792 23429 603 41 0 24751 0
vsize: 99168
[startup+710.055 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 34588 0 0 0 70913 98 0 0 25 0 1 0 482916192 102617088 23686 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25053 23686 603 41 0 25012 0
vsize: 100212
[startup+720.056 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 34888 0 0 0 71912 98 0 0 25 0 1 0 482916192 103956480 23986 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25380 23986 603 41 0 25339 0
vsize: 101520
[startup+730.056 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 35219 0 0 0 72912 99 0 0 25 0 1 0 482916192 105295872 24317 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25707 24317 603 41 0 25666 0
vsize: 102828
[startup+740.057 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 35469 0 0 0 73912 99 0 0 25 0 1 0 482916192 106360832 24567 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25967 24567 603 41 0 25926 0
vsize: 103868
[startup+750.057 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 35800 0 0 0 74911 101 0 0 25 0 1 0 482916192 107675648 24898 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26288 24898 603 41 0 26247 0
vsize: 105152
[startup+760.058 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 36272 0 0 0 75909 103 0 0 25 0 1 0 482916192 109649920 25370 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26770 25370 603 41 0 26729 0
vsize: 107080
[startup+770.058 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 36738 0 0 0 76908 104 0 0 25 0 1 0 482916192 111489024 25836 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27219 25836 603 41 0 27178 0
vsize: 108876
[startup+780.058 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 37158 0 0 0 77907 105 0 0 25 0 1 0 482916192 113209344 26256 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27639 26256 603 41 0 27598 0
vsize: 110556
[startup+790.058 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 37343 0 0 0 78906 106 0 0 25 0 1 0 482916192 114008064 26441 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27834 26441 603 41 0 27793 0
vsize: 111336
[startup+800.059 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 37786 0 0 0 79906 107 0 0 25 0 1 0 482916192 115863552 26884 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28287 26884 603 41 0 28246 0
vsize: 113148
[startup+810.058 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 38193 0 0 0 80904 109 0 0 25 0 1 0 482916192 117448704 27291 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28674 27291 603 41 0 28633 0
vsize: 114696
[startup+820.06 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 38404 0 0 0 81903 110 0 0 25 0 1 0 482916192 118374400 27502 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28900 27502 603 41 0 28859 0
vsize: 115600
[startup+830.059 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 38831 0 0 0 82902 111 0 0 25 0 1 0 482916192 120094720 27929 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29320 27929 603 41 0 29279 0
vsize: 117280
[startup+840.059 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 39359 0 0 0 83900 113 0 0 25 0 1 0 482916192 122208256 28457 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29836 28457 603 41 0 29795 0
vsize: 119344
[startup+850.059 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 40154 0 0 0 84898 115 0 0 25 0 1 0 482916192 125497344 29252 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30639 29252 603 41 0 30598 0
vsize: 122556
[startup+860.06 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 40675 0 0 0 85896 117 0 0 25 0 1 0 482916192 127594496 29773 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31151 29773 603 41 0 31110 0
vsize: 124604
[startup+870.061 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 41290 0 0 0 86895 119 0 0 25 0 1 0 482916192 130101248 30388 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31763 30388 603 41 0 31722 0
vsize: 127052
[startup+880.061 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 41820 0 0 0 87893 121 0 0 25 0 1 0 482916192 132329472 30918 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32307 30918 603 41 0 32266 0
vsize: 129228
[startup+890.061 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 42313 0 0 0 88892 122 0 0 25 0 1 0 482916192 134316032 31411 4294967295 134512640 134672761 3221224544 3221223688 134616178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32792 31411 603 41 0 32751 0
vsize: 131168
[startup+900.06 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 42453 0 0 0 89891 123 0 0 25 0 1 0 482916192 134856704 31551 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32924 31551 603 41 0 32883 0
vsize: 131696
[startup+910.061 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 42616 0 0 0 90891 123 0 0 25 0 1 0 482916192 136044544 31714 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33214 31714 603 41 0 33173 0
vsize: 132856
[startup+920.061 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 43009 0 0 0 91891 124 0 0 25 0 1 0 482916192 137633792 32107 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33602 32107 603 41 0 33561 0
vsize: 134408
[startup+930.062 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 43282 0 0 0 92890 125 0 0 25 0 1 0 482916192 138694656 32380 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33861 32380 603 41 0 33820 0
vsize: 135444
[startup+940.062 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 43459 0 0 0 93890 125 0 0 25 0 1 0 482916192 139489280 32557 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34055 32557 603 41 0 34014 0
vsize: 136220
[startup+950.063 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 43635 0 0 0 94890 126 0 0 25 0 1 0 482916192 140144640 32733 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34215 32734 603 41 0 34174 0
vsize: 136860
[startup+960.063 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 43797 0 0 0 95889 126 0 0 25 0 1 0 482916192 140816384 32895 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34379 32895 603 41 0 34338 0
vsize: 137516
[startup+970.064 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 44032 0 0 0 96889 127 0 0 25 0 1 0 482916192 141742080 33130 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34605 33130 603 41 0 34564 0
vsize: 138420
[startup+980.064 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 44312 0 0 0 97888 128 0 0 25 0 1 0 482916192 142938112 33410 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34897 33410 603 41 0 34856 0
vsize: 139588
[startup+990.064 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 44723 0 0 0 98887 129 0 0 25 0 1 0 482916192 144572416 33821 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35296 33821 603 41 0 35255 0
vsize: 141184
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 45028 0 0 0 99887 130 0 0 25 0 1 0 482916192 145858560 34126 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35610 34126 603 41 0 35569 0
vsize: 142440
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 45349 0 0 0 100886 131 0 0 25 0 1 0 482916192 147181568 34447 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35933 34447 603 41 0 35892 0
vsize: 143732
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 45775 0 0 0 101884 133 0 0 25 0 1 0 482916192 148881408 34873 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36348 34873 603 41 0 36307 0
vsize: 145392
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 46034 0 0 0 102884 133 0 0 25 0 1 0 482916192 149934080 35132 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36605 35132 603 41 0 36564 0
vsize: 146420
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 46435 0 0 0 103883 134 0 0 25 0 1 0 482916192 151642112 35533 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37022 35533 603 41 0 36981 0
vsize: 148088
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 47003 0 0 0 104882 135 0 0 25 0 1 0 482916192 153866240 36101 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37565 36101 603 41 0 37524 0
vsize: 150260
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 47361 0 0 0 105881 136 0 0 25 0 1 0 482916192 155418624 36459 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37944 36459 603 41 0 37903 0
vsize: 151776
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 47910 0 0 0 106881 137 0 0 25 0 1 0 482916192 157655040 37008 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38490 37008 603 41 0 38449 0
vsize: 153960
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 48300 0 0 0 107880 138 0 0 25 0 1 0 482916192 159223808 37398 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38873 37398 603 41 0 38832 0
vsize: 155492
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 48437 0 0 0 108879 139 0 0 25 0 1 0 482916192 159752192 37535 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39002 37535 603 41 0 38961 0
vsize: 156008
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 48600 0 0 0 109879 139 0 0 25 0 1 0 482916192 160436224 37698 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39169 37698 603 41 0 39128 0
vsize: 156676
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 48731 0 0 0 110878 140 0 0 25 0 1 0 482916192 160960512 37829 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39297 37829 603 41 0 39256 0
vsize: 157188
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 48869 0 0 0 111878 141 0 0 25 0 1 0 482916192 161624064 37967 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39459 37967 603 41 0 39418 0
vsize: 157836
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 49016 0 0 0 112877 141 0 0 25 0 1 0 482916192 162152448 38114 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39588 38114 603 41 0 39547 0
vsize: 158352
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 49194 0 0 0 113877 142 0 0 25 0 1 0 482916192 162942976 38292 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39781 38292 603 41 0 39740 0
vsize: 159124
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 49904 0 0 0 114876 143 0 0 25 0 1 0 482916192 165838848 39002 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40488 39002 603 41 0 40447 0
vsize: 161952
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 52181 0 0 0 115871 148 0 0 25 0 1 0 482916192 175087616 41279 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42746 41279 603 41 0 42705 0
vsize: 170984
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 54175 0 0 0 116866 153 0 0 25 0 1 0 482916192 183226368 43273 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44733 43273 603 41 0 44692 0
vsize: 178932
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 56139 0 0 0 117862 158 0 0 25 0 1 0 482916192 191238144 45237 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46689 45237 603 41 0 46648 0
vsize: 186756
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 58014 0 0 0 118858 162 0 0 25 0 1 0 482916192 198995968 47112 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48583 47112 603 41 0 48542 0
vsize: 194332
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 26760
Raw data (stat): 26760 (minisat+) R 26759 29151 29150 0 -1 0 58222 0 0 0 119858 162 0 0 25 0 1 0 482916192 199753728 47320 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48768 47320 603 41 0 48727 0
vsize: 195072
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 26760
Raw data (stat): 26760 (minisat+) Z 26759 29151 29150 0 -1 12 58223 0 0 0 119858 171 0 0 22 0 1 0 482916192 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.2
CPU time (s): 1200.3
CPU user time (s): 1198.59
CPU system time (s): 1.71874
CPU usage (%): 100.008
Max. virtual memory (Kb): 195072
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####