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-ran10x12.opb
MD5SUM	ddd1f838c1e3a248aad1987162b1d40d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	656964
Optimality of the best value was proved	NO
Number of terms in the objective function	2520
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	666682247
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	666682247
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.04
Number of variables	2520
Total number of constraints	142
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	142
Minimum length of a constraint	21
Maximum length of a constraint	240
Trace number 14807

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 01:31:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19232 boxname=wulflinc3 idbench=1480 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  ddd1f838c1e3a248aad1987162b1d40d  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-ran10x12.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-ran10x12.opb
IDLAUNCH: 19232
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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		: 451.190
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:        303336 kB
Buffers:         34404 kB
Cached:         673476 kB
SwapCached:          0 kB
Active:         200808 kB
Inactive:       509820 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        303084 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6840 kB
Slab:            15004 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:51:17 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 19232 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 164 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 162]---> Adder-cost: 222   maxlim: 13044   bits: 14/14
c ---[ 160]---> Adder-cost: 230   maxlim: 20340   bits: 15/15
c ---[ 158]---> Adder-cost: 230   maxlim: 19188   bits: 15/15
c ---[ 156]---> Adder-cost: 230   maxlim: 20852   bits: 15/15
c ---[ 154]---> Adder-cost: 222   maxlim: 13812   bits: 14/14
c ---[ 152]---> Adder-cost: 222   maxlim: 13556   bits: 14/14
c ---[ 150]---> Adder-cost: 230   maxlim: 19444   bits: 15/15
c ---[ 148]---> Adder-cost: 214   maxlim: 9076   bits: 14/14
c ---[ 146]---> Adder-cost: 214   maxlim: 9076   bits: 14/14
c ---[ 144]---> Adder-cost: 222   maxlim: 13300   bits: 14/14
c ---[ 142]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 140]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Adder-cost: 196   maxlim: 16758   bits: 15/15
c ---[ 132]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 119]---> BDD-cost:   10
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   13
c ---[ 114]---> BDD-cost:   10
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   13
c ---[ 111]---> BDD-cost:   10
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   10
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   11
c ---[ 103]---> BDD-cost:   13
c ---[ 102]---> BDD-cost:   13
c ---[ 101]---> BDD-cost:   10
c ---[ 100]---> BDD-cost:   10
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:   13
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   15
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   17
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   10
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:   17
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   10
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   13
c ---[  70]---> BDD-cost:   16
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   14
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   10
c ---[  60]---> BDD-cost:   17
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   10
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   12
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   10
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   10
c ---[  35]---> BDD-cost:   10
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   10
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   15
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   10
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   10
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   10
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   71854   188428 |   23951       0        0     nan |  0.000 % |
c |       100 |   71772   188245 |   26346      89      483     5.4 |  9.032 % |
c |       250 |   71292   187145 |   28980     231     1112     4.8 |  9.655 % |
c |       475 |   71276   187093 |   31878     454     2215     4.9 |  9.667 % |
c |       813 |   70929   186305 |   35066     770     3716     4.8 | 10.075 % |
c |      1319 |   70929   186305 |   38573    1276     5968     4.7 | 10.075 % |
c |      2078 |   70905   186237 |   42430    2030     9447     4.7 | 10.096 % |
c |      3218 |   70582   185459 |   46673    3157    14875     4.7 | 10.467 % |
c |      4926 |   69741   183406 |   51341    4815    24261     5.0 | 11.489 % |
c |      7489 |   69312   182361 |   56475    7343    37294     5.1 | 11.994 % |
c |     11333 |   67979   179228 |   62122   11074    58131     5.2 | 13.681 % |
c ==============================================================================
c [1mFound solution: 2950330[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4798   maxlim: 969933   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12019 |  101372   298643 |   33790   11740    62732     5.3 | 13.681 % |
c |     12123 |  101372   298643 |   37169   11843    63303     5.3 | 11.519 % |
c |     12273 |  101354   298595 |   40885   11991    63970     5.3 | 11.529 % |
c |     12498 |  101354   298595 |   44974   12216    65070     5.3 | 11.529 % |
c |     12836 |  101354   298595 |   49471   12554    66909     5.3 | 11.529 % |
c |     13344 |  101354   298595 |   54419   13062    70190     5.4 | 11.529 % |
c |     14106 |  101211   298233 |   59861   13816    74433     5.4 | 11.666 % |
c |     15245 |  101183   298163 |   65847   14952    82206     5.5 | 11.690 % |
c |     16953 |  100955   297597 |   72431   16641    94324     5.7 | 11.939 % |
c ==============================================================================
c [1mFound solution: 2802740[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1117523   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19039 |  100956   297694 |   33652   18719   117106     6.3 | 11.939 % |
c |     19139 |  100956   297694 |   37017   18819   117642     6.3 | 11.986 % |
c |     19289 |  100901   297552 |   40718   18950   118739     6.3 | 12.042 % |
c |     19515 |  100901   297552 |   44790   19176   120894     6.3 | 12.042 % |
c |     19852 |  100892   297523 |   49269   19512   123644     6.3 | 12.049 % |
c |     20358 |  100884   297497 |   54196   20017   127585     6.4 | 12.053 % |
c |     21117 |  100855   297402 |   59616   20772   133416     6.4 | 12.074 % |
c |     22256 |  100772   297187 |   65578   21903   141784     6.5 | 12.165 % |
c |     23964 |  100686   296943 |   72136   23604   178358     7.6 | 12.242 % |
c |     26526 |  100686   296943 |   79349   26166   454561    17.4 | 12.242 % |
c ==============================================================================
c [1mFound solution: 2698613[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1221650   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28013 |  100583   296801 |   33527   27634   489957    17.7 | 12.242 % |
c |     28113 |  100583   296801 |   36879   27734   490588    17.7 | 12.381 % |
c |     28263 |  100583   296801 |   40567   27884   491780    17.6 | 12.381 % |
c |     28488 |  100583   296801 |   44624   28109   495046    17.6 | 12.381 % |
c |     28825 |  100583   296801 |   49086   28446   497849    17.5 | 12.381 % |
c |     29332 |  100564   296756 |   53995   28951   536007    18.5 | 12.406 % |
c ==============================================================================
c [1mFound solution: 2585248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1335015   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29494 |  100563   296875 |   33521   29112   538417    18.5 | 12.406 % |
c |     29594 |  100531   296804 |   36873   29209   539003    18.5 | 12.488 % |
c |     29744 |  100258   296174 |   40560   29291   539674    18.4 | 12.796 % |
c |     29969 |  100112   295837 |   44616   29515   542606    18.4 | 12.974 % |
c |     30306 |  100112   295837 |   49078   29852   566780    19.0 | 12.974 % |
c |     30812 |  100036   295655 |   53985   30352   571159    18.8 | 13.044 % |
c |     31571 |  100027   295624 |   59384   31109   579760    18.6 | 13.047 % |
c |     32710 |   99680   294794 |   65322   32222   596929    18.5 | 13.432 % |
c |     34419 |   99680   294794 |   71855   33931   787069    23.2 | 13.432 % |
c ==============================================================================
c [1mFound solution: 2443672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1476591   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35364 |   99607   294718 |   33202   34864   807217    23.2 | 13.432 % |
c |     35464 |   99591   294683 |   36522   34960   807928    23.1 | 13.556 % |
c |     35615 |   99591   294683 |   40174   35111   809396    23.1 | 13.556 % |
c |     35841 |   99591   294683 |   44191   35337   811724    23.0 | 13.556 % |
c |     36178 |   99521   294521 |   48611   35662   819237    23.0 | 13.632 % |
c ==============================================================================
c [1mFound solution: 2165210[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1755053   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36647 |   99542   294703 |   33180   36131   829323    23.0 | 13.632 % |
c |     36747 |   99440   294473 |   36498   36221   829993    22.9 | 13.769 % |
c |     36897 |   99440   294473 |   40147   36371   833862    22.9 | 13.769 % |
c |     37122 |   99440   294473 |   44162   36596   837156    22.9 | 13.769 % |
c |     37459 |   99440   294473 |   48578   36933   843815    22.8 | 13.769 % |
c |     37965 |   99386   294332 |   53436   37432   854608    22.8 | 13.811 % |
c |     38726 |   99386   294332 |   58780   38193   896115    23.5 | 13.811 % |
c |     39865 |   99386   294332 |   64658   39332  1011513    25.7 | 13.811 % |
c |     41574 |   99386   294332 |   71124   41041  1057780    25.8 | 13.811 % |
c |     44138 |   99386   294332 |   78236   43605  1391279    31.9 | 13.811 % |
c ==============================================================================
c [1mFound solution: 1277552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2642711   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45814 |   99350   293826 |   33116   45272  1454878    32.1 | 13.811 % |
c |     45914 |   99334   293789 |   36427   20561   707515    34.4 | 13.851 % |
c |     46065 |   99313   293740 |   40070   20711   708554    34.2 | 13.872 % |
c |     46291 |   99313   293740 |   44077   20937   709806    33.9 | 13.872 % |
c |     46628 |   99313   293740 |   48485   21274   712617    33.5 | 13.872 % |
c |     47136 |   99313   293740 |   53333   21782   718896    33.0 | 13.872 % |
c |     47895 |   99299   293708 |   58667   22539   743656    33.0 | 13.886 % |
c |     49035 |   99299   293708 |   64533   23679   808196    34.1 | 13.886 % |
c |     50744 |   99189   293451 |   70987   25365   833733    32.9 | 13.998 % |
c |     53306 |   99178   293426 |   78085   27926   960091    34.4 | 14.009 % |
c |     57150 |   99154   293371 |   85894   31769  1101818    34.7 | 14.033 % |
c |     62916 |   99067   293155 |   94483   37525  1251382    33.3 | 14.120 % |
c |     71566 |   99010   293022 |  103932   46168  1559284    33.8 | 14.190 % |
c |     84540 |   98894   292754 |  114325   59139  2427787    41.1 | 14.330 % |
c |    104002 |   98880   292723 |  125757   78598  3347089    42.6 | 14.344 % |
c |    133197 |   98880   292723 |  138333  107793  6808231    63.2 | 14.344 % |
c |    176986 |   98485   291804 |  152167   27387   873164    31.9 | 14.790 % |
c |    242670 |   98447   291705 |  167383   93066  6833293    73.4 | 14.832 % |
c |    341196 |   98154   291024 |  184122   28531  1620958    56.8 | 15.143 % |
c ==============================================================================
c [1mFound solution: 1084717[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2835546   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    441705 |   97687   290039 |   32562  128961  7360631    57.1 | 15.143 % |
c |    441805 |   97687   290039 |   35818   23728   802967    33.8 | 15.693 % |
c |    441955 |   97640   289931 |   39400   23874   803609    33.7 | 15.753 % |
c |    442180 |   97640   289931 |   43340   24099   809907    33.6 | 15.753 % |
c |    442517 |   97640   289931 |   47674   24436   819386    33.5 | 15.753 % |
c |    443025 |   97640   289931 |   52441   24944   825160    33.1 | 15.753 % |
c |    443784 |   97640   289931 |   57685   25703   905240    35.2 | 15.753 % |
c |    444925 |   97640   289931 |   63454   26844   928234    34.6 | 15.753 % |
c |    446633 |   97640   289931 |   69799   28552  1071065    37.5 | 15.753 % |
c |    449196 |   97640   289931 |   76779   31115  1200456    38.6 | 15.753 % |
c |    453041 |   97640   289931 |   84457   34960  1387575    39.7 | 15.753 % |
c |    458807 |   97632   289912 |   92903   40725  1545545    38.0 | 15.763 % |
c |    467460 |   97568   289764 |  102193   49372  2122274    43.0 | 15.836 % |
c |    480434 |   97495   289591 |  112412   62341  4299541    69.0 | 15.920 % |
c |    499895 |   97467   289527 |  123654   81800  5459223    66.7 | 15.952 % |
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 X100_bit_7 X100_bit_6 X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 -X101_bit_6 -X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 -X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 X104_bit_6 X104_bit_5 -X104_bit_4 -X104_bit_3 X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 X105_bit_6 -X105_bit_5 -X105_bit_4 -X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X106_bit_7 -X106_bit_6 -X106_bit_5 -X106_bit_4 -X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 -X107_bit_6 -X107_bit_5 -X107_bit_4 -X107_bit_3 -X107_bit_2 X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 -X108_bit_6 -X108_bit_5 -X108_bit_4 -X108_bit_3 -X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 X109_bit_7 X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X111_bit_7 -X111_bit_6 -X111_bit_5 -X111_bit_4 -X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 X112_bit_7 -X112_bit_6 -X112_bit_5 -X112_bit_4 X112_bit_3 -X112_bit_2 -X112_bit_1 -X112_bit0 X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 -X115_bit_6 -X115_bit_5 -X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 -X116_bit_7 -X116_bit_6 -X116_bit_5 X116_bit_4 -X116_bit_3 X116_bit_2 X116_bit_1 -X116_bit0 -X116_bit1 X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 -X117_bit_6 -X117_bit_5 -X117_bit_#### 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.91 0.95 0.94 2/54 3101
Raw data (stat): 3101 (runsolver) R 3100 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482911576 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.93 0.95 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 2446 0 0 0 993 5 0 0 25 0 1 0 482911576 12079104 2366 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2366 603 41 0 2908 0
vsize: 11796
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 5451 0 0 0 1985 12 0 0 25 0 1 0 482911576 22687744 4793 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5539 4793 603 41 0 5498 0
vsize: 22156
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 5612 0 0 0 2985 12 0 0 25 0 1 0 482911576 23277568 4946 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5683 4946 603 41 0 5642 0
vsize: 22732
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 6072 0 0 0 3982 14 0 0 25 0 1 0 482911576 25055232 5395 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6117 5395 603 41 0 6076 0
vsize: 24468
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 6284 0 0 0 4982 15 0 0 25 0 1 0 482911576 26005504 5601 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6349 5601 603 41 0 6308 0
vsize: 25396
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 6542 0 0 0 5981 15 0 0 25 0 1 0 482911576 26939392 5841 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 5841 603 41 0 6536 0
vsize: 26308
[startup+70.0019 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 7165 0 0 0 6979 17 0 0 25 0 1 0 482911576 29487104 6464 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7199 6464 603 41 0 7158 0
vsize: 28796
[startup+80.0023 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 7248 0 0 0 7979 18 0 0 25 0 1 0 482911576 29798400 6538 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7275 6538 603 41 0 7234 0
vsize: 29100
[startup+90.0026 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 7248 0 0 0 8979 18 0 0 25 0 1 0 482911576 29798400 6538 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7275 6538 603 41 0 7234 0
vsize: 29100
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 7248 0 0 0 9979 18 0 0 25 0 1 0 482911576 29798400 6538 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7275 6538 603 41 0 7234 0
vsize: 29100
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 7448 0 0 0 10979 18 0 0 25 0 1 0 482911576 30605312 6738 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7472 6738 603 41 0 7431 0
vsize: 29888
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 7760 0 0 0 11978 20 0 0 25 0 1 0 482911576 31821824 7050 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7769 7050 603 41 0 7728 0
vsize: 31076
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 8159 0 0 0 12977 20 0 0 25 0 1 0 482911576 33443840 7449 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8165 7449 603 41 0 8124 0
vsize: 32660
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 8510 0 0 0 13977 21 0 0 25 0 1 0 482911576 34926592 7800 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8527 7800 603 41 0 8486 0
vsize: 34108
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 8899 0 0 0 14976 22 0 0 25 0 1 0 482911576 36679680 8189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8955 8189 603 41 0 8914 0
vsize: 35820
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 9339 0 0 0 15975 23 0 0 25 0 1 0 482911576 38551552 8629 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9412 8629 603 41 0 9371 0
vsize: 37648
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 9709 0 0 0 16974 25 0 0 25 0 1 0 482911576 40050688 8999 4294967295 134512640 134672761 3221224624 3221223776 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9778 8999 603 41 0 9737 0
vsize: 39112
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 10370 0 0 0 17972 27 0 0 25 0 1 0 482911576 42721280 9660 4294967295 134512640 134672761 3221224624 3221223728 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10430 9661 603 41 0 10389 0
vsize: 41720
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 10991 0 0 0 18970 29 0 0 25 0 1 0 482911576 45252608 10281 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11048 10281 603 41 0 11007 0
vsize: 44192
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 11580 0 0 0 19969 30 0 0 25 0 1 0 482911576 47652864 10870 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11634 10870 603 41 0 11593 0
vsize: 46536
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 12163 0 0 0 20968 31 0 0 25 0 1 0 482911576 50065408 11453 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11453 603 41 0 12182 0
vsize: 48892
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 12596 0 0 0 21967 32 0 0 25 0 1 0 482911576 51810304 11886 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12649 11886 603 41 0 12608 0
vsize: 50596
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 12919 0 0 0 22966 34 0 0 25 0 1 0 482911576 53022720 12209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12945 12209 603 41 0 12904 0
vsize: 51780
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 13244 0 0 0 23965 35 0 0 25 0 1 0 482911576 54358016 12534 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13271 12534 603 41 0 13230 0
vsize: 53084
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 13756 0 0 0 24963 37 0 0 25 0 1 0 482911576 56508416 13046 4294967295 134512640 134672761 3221224624 3221223808 134558360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13796 13046 603 41 0 13755 0
vsize: 55184
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 14110 0 0 0 25962 37 0 0 25 0 1 0 482911576 57864192 13400 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14127 13400 603 41 0 14086 0
vsize: 56508
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 14437 0 0 0 26962 38 0 0 25 0 1 0 482911576 59224064 13727 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14459 13727 603 41 0 14418 0
vsize: 57836
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 14826 0 0 0 27961 39 0 0 25 0 1 0 482911576 60829696 14116 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14851 14116 603 41 0 14810 0
vsize: 59404
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 15139 0 0 0 28960 40 0 0 25 0 1 0 482911576 62558208 14429 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15273 14429 603 41 0 15232 0
vsize: 61092
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 15454 0 0 0 29959 41 0 0 25 0 1 0 482911576 63909888 14744 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15603 14744 603 41 0 15562 0
vsize: 62412
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 15664 0 0 0 30959 42 0 0 25 0 1 0 482911576 64716800 14954 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15800 14954 603 41 0 15759 0
vsize: 63200
[startup+320.018 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 15941 0 0 0 31960 42 0 0 25 0 1 0 482911576 65925120 15231 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16095 15231 603 41 0 16054 0
vsize: 64380
[startup+330.018 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16305 0 0 0 32959 44 0 0 25 0 1 0 482911576 67399680 15595 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16455 15595 603 41 0 16414 0
vsize: 65820
[startup+340.018 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 33959 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+350.018 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 34959 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+360.017 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 35959 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+370.017 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 36959 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+380.018 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 37959 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+390.018 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 38959 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+400.018 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 39960 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+410.018 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 40960 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+420.018 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 41960 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+430.018 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 42960 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+440.019 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 43960 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+450.019 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 44961 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+460.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 45961 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+470.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 46961 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+480.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 47960 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+490.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 48960 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+500.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 49961 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+510.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 50961 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223760 134560637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+520.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 51961 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+530.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 52961 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+540.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 53961 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+550.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16374 0 0 0 54962 44 0 0 25 0 1 0 482911576 67670016 15664 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16521 15664 603 41 0 16480 0
vsize: 66084
[startup+560.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16433 0 0 0 55961 44 0 0 25 0 1 0 482911576 67801088 15723 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16553 15723 603 41 0 16512 0
vsize: 66212
[startup+570.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16720 0 0 0 56961 45 0 0 25 0 1 0 482911576 69009408 16010 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16848 16010 603 41 0 16807 0
vsize: 67392
[startup+580.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 16969 0 0 0 57960 46 0 0 25 0 1 0 482911576 70086656 16259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17111 16259 603 41 0 17070 0
vsize: 68444
[startup+590.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 17201 0 0 0 58959 47 0 0 25 0 1 0 482911576 71028736 16491 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17341 16491 603 41 0 17300 0
vsize: 69364
[startup+600.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 17442 0 0 0 59958 48 0 0 25 0 1 0 482911576 71970816 16732 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17571 16732 603 41 0 17530 0
vsize: 70284
[startup+610.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 17699 0 0 0 60958 49 0 0 25 0 1 0 482911576 73043968 16989 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17833 16989 603 41 0 17792 0
vsize: 71332
[startup+620.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 17976 0 0 0 61957 50 0 0 25 0 1 0 482911576 74248192 17266 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18127 17266 603 41 0 18086 0
vsize: 72508
[startup+630.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 18206 0 0 0 62957 50 0 0 25 0 1 0 482911576 75063296 17496 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18326 17496 603 41 0 18285 0
vsize: 73304
[startup+640.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 18518 0 0 0 63956 51 0 0 25 0 1 0 482911576 76406784 17808 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18654 17808 603 41 0 18613 0
vsize: 74616
[startup+650.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 18745 0 0 0 64955 52 0 0 25 0 1 0 482911576 77340672 18035 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18882 18035 603 41 0 18841 0
vsize: 75528
[startup+660.021 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 18886 0 0 0 65954 53 0 0 25 0 1 0 482911576 77873152 18176 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19012 18176 603 41 0 18971 0
vsize: 76048
[startup+670.022 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 19114 0 0 0 66954 54 0 0 25 0 1 0 482911576 78815232 18404 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19242 18404 603 41 0 19201 0
vsize: 76968
[startup+680.031 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 19406 0 0 0 67954 55 0 0 25 0 1 0 482911576 80019456 18696 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19536 18696 603 41 0 19495 0
vsize: 78144
[startup+690.031 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 19742 0 0 0 68953 56 0 0 25 0 1 0 482911576 81362944 19032 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19864 19032 603 41 0 19823 0
vsize: 79456
[startup+700.031 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 20053 0 0 0 69952 57 0 0 25 0 1 0 482911576 82710528 19343 4294967295 134512640 134672761 3221224624 3221223728 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20193 19343 603 41 0 20152 0
vsize: 80772
[startup+710.031 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 20269 0 0 0 70952 57 0 0 25 0 1 0 482911576 83509248 19559 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20388 19559 603 41 0 20347 0
vsize: 81552
[startup+720.032 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 20427 0 0 0 71952 58 0 0 25 0 1 0 482911576 84180992 19717 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20552 19717 603 41 0 20511 0
vsize: 82208
[startup+730.032 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 20591 0 0 0 72951 58 0 0 25 0 1 0 482911576 84856832 19881 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20717 19881 603 41 0 20676 0
vsize: 82868
[startup+740.032 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 20795 0 0 0 73950 59 0 0 25 0 1 0 482911576 85651456 20085 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20911 20085 603 41 0 20870 0
vsize: 83644
[startup+750.033 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21068 0 0 0 74950 60 0 0 25 0 1 0 482911576 86732800 20358 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21175 20358 603 41 0 21134 0
vsize: 84700
[startup+760.032 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21375 0 0 0 75949 61 0 0 25 0 1 0 482911576 87941120 20665 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20665 603 41 0 21429 0
vsize: 85880
[startup+770.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21657 0 0 0 76949 62 0 0 25 0 1 0 482911576 89149440 20947 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21765 20947 603 41 0 21724 0
vsize: 87060
[startup+780.033 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 77948 62 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+790.033 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 78948 62 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+800.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 79948 62 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+810.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 80947 63 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+820.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 81947 63 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+830.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 82947 63 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+840.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 83948 63 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+850.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 84948 63 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+860.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 85948 63 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+870.035 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 86948 63 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+880.035 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 87948 63 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+890.035 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 88948 63 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+900.034 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21827 0 0 0 89949 63 0 0 25 0 1 0 482911576 89817088 21117 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21117 603 41 0 21887 0
vsize: 87712
[startup+910.041 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21828 0 0 0 90949 63 0 0 25 0 1 0 482911576 89817088 21118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21118 603 41 0 21887 0
vsize: 87712
[startup+920.042 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21828 0 0 0 91950 63 0 0 25 0 1 0 482911576 89817088 21118 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21118 603 41 0 21887 0
vsize: 87712
[startup+930.041 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21828 0 0 0 92950 63 0 0 25 0 1 0 482911576 89817088 21118 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21118 603 41 0 21887 0
vsize: 87712
[startup+940.042 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21828 0 0 0 93950 63 0 0 25 0 1 0 482911576 89817088 21118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21118 603 41 0 21887 0
vsize: 87712
[startup+950.042 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21828 0 0 0 94950 63 0 0 25 0 1 0 482911576 89817088 21118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21118 603 41 0 21887 0
vsize: 87712
[startup+960.041 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21828 0 0 0 95950 63 0 0 25 0 1 0 482911576 89817088 21118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21118 603 41 0 21887 0
vsize: 87712
[startup+970.041 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21828 0 0 0 96950 63 0 0 25 0 1 0 482911576 89817088 21118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21118 603 41 0 21887 0
vsize: 87712
[startup+980.042 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21828 0 0 0 97951 63 0 0 25 0 1 0 482911576 89817088 21118 4294967295 134512640 134672761 3221224624 3221223748 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21118 603 41 0 21887 0
vsize: 87712
[startup+990.042 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21828 0 0 0 98951 63 0 0 25 0 1 0 482911576 89817088 21118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21118 603 41 0 21887 0
vsize: 87712
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21830 0 0 0 99951 63 0 0 25 0 1 0 482911576 89817088 21120 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21120 603 41 0 21887 0
vsize: 87712
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21833 0 0 0 100951 63 0 0 25 0 1 0 482911576 89817088 21123 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21123 603 41 0 21887 0
vsize: 87712
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21834 0 0 0 101951 63 0 0 25 0 1 0 482911576 89817088 21124 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21124 603 41 0 21887 0
vsize: 87712
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21834 0 0 0 102951 63 0 0 25 0 1 0 482911576 89817088 21124 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21124 603 41 0 21887 0
vsize: 87712
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 103951 63 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 104949 63 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 105949 63 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 106949 63 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 107949 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 108950 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 109950 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 110950 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 111950 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 112950 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 113951 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 114951 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 115951 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 116951 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 117951 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 118951 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 3101
Raw data (stat): 3101 (minisat+) R 3100 10720 10719 0 -1 0 21835 0 0 0 119951 64 0 0 25 0 1 0 482911576 89817088 21125 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21928 21125 603 41 0 21887 0
vsize: 87712
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.94 1/54 3101
Raw data (stat): 3101 (minisat+) Z 3100 10720 10719 0 -1 12 21838 0 0 0 119952 68 0 0 25 0 1 0 482911576 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.21
CPU user time (s): 1199.52
CPU system time (s): 0.684895
CPU usage (%): 100.009
Max. virtual memory (Kb): 87712
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####