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/MIPLIB/miplib/normalized-mps-v2-13-7-lp4l.opb
MD5SUM	3c39e3c2b993ee2185e2a1a3e73b9723
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3684
Optimality of the best value was proved	NO
Number of terms in the objective function	1086
Biggest coefficient in the objective function	283
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	197191
Number of bits of the sum of numbers in the objective function	18
Biggest number in a constraint	283
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	197191
Number of bits of the biggest sum of numbers	18
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.3
Number of variables	1086
Total number of constraints	1171
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1170
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1086
Trace number 19178

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 18:10:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16911 boxname=wulflinc10 idbench=1301 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c39e3c2b993ee2185e2a1a3e73b9723  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-lp4l.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-lp4l.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-lp4l.opb
IDLAUNCH: 16911
/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:        529428 kB
Buffers:         22756 kB
Cached:         460996 kB
SwapCached:          0 kB
Active:         278424 kB
Inactive:       207868 kB
HighTotal:      131008 kB
HighFree:         7224 kB
LowTotal:       903652 kB
LowFree:        522204 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13464 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:30:18 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 16911 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 169 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 168]---> Adder-cost: 592   maxlim: 2471   bits: 12/12
c ---[ 166]---> BDD-cost:   41
c ---[ 164]---> BDD-cost:   67
c ---[ 162]---> BDD-cost:   99
c ---[ 160]---> BDD-cost:   79
c ---[ 158]---> BDD-cost:   45
c ---[ 156]---> BDD-cost:   69
c ---[ 154]---> BDD-cost:   55
c ---[ 152]---> BDD-cost:   37
c ---[ 150]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   77
c ---[ 146]---> BDD-cost:   79
c ---[ 144]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   75
c ---[ 140]---> BDD-cost:   77
c ---[ 138]---> BDD-cost:   41
c ---[ 136]---> BDD-cost:   75
c ---[ 134]---> BDD-cost:  107
c ---[ 132]---> BDD-cost:   91
c ---[ 130]---> BDD-cost:  127
c ---[ 128]---> BDD-cost:  123
c ---[ 126]---> BDD-cost:   89
c ---[ 124]---> BDD-cost:   57
c ---[ 122]---> BDD-cost:   89
c ---[ 120]---> BDD-cost:   71
c ---[ 118]---> BDD-cost:  103
c ---[ 116]---> BDD-cost:  117
c ---[ 114]---> BDD-cost:  125
c ---[ 112]---> BDD-cost:   91
c ---[ 110]---> BDD-cost:   59
c ---[ 108]---> BDD-cost:   89
c ---[ 106]---> BDD-cost:   71
c ---[ 104]---> BDD-cost:  129
c ---[ 102]---> BDD-cost:  113
c ---[ 100]---> BDD-cost:  123
c ---[  98]---> BDD-cost:   89
c ---[  96]---> BDD-cost:   61
c ---[  94]---> BDD-cost:   59
c ---[  92]---> BDD-cost:   33
c ---[  90]---> BDD-cost:  123
c ---[  88]---> BDD-cost:  121
c ---[  86]---> BDD-cost:   99
c ---[  84]---> BDD-cost:   45
c ---[  82]---> BDD-cost:   69
c ---[  80]---> BDD-cost:   59
c ---[  78]---> BDD-cost:   33
c ---[  76]---> BDD-cost:   73
c ---[  74]---> BDD-cost:   69
c ---[  72]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   67
c ---[  68]---> BDD-cost:   95
c ---[  66]---> BDD-cost:   85
c ---[  64]---> BDD-cost:  107
c ---[  62]---> BDD-cost:   97
c ---[  60]---> BDD-cost:   33
c ---[  58]---> BDD-cost:   79
c ---[  56]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   75
c ---[  52]---> BDD-cost:   67
c ---[  50]---> BDD-cost:   43
c ---[  48]---> BDD-cost:   75
c ---[  46]---> BDD-cost:  105
c ---[  44]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   63
c ---[  38]---> BDD-cost:   39
c ---[  36]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   63
c ---[  32]---> BDD-cost:    5
c ---[  30]---> BDD-cost:  169
c ---[  28]---> BDD-cost:  155
c ---[  26]---> BDD-cost:  115
c ---[  24]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   83
c ---[  20]---> BDD-cost:  111
c ---[  18]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  161
c ---[  14]---> BDD-cost:  151
c ---[  12]---> BDD-cost:  117
c ---[  10]---> BDD-cost:   57
c ---[   8]---> BDD-cost:   85
c ---[   6]---> BDD-cost:   71
c ---[   4]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   37
c ---[   0]---> Adder-cost: 2160   maxlim: 1059   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   35795   111743 |   10738       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10268          
c   -- var.elim.:  2000/10268          
c   -- var.elim.:  3000/10268          
c   -- var.elim.:  4000/10268          
c   -- var.elim.:  5000/10268          
c   -- var.elim.:  6000/10268          
c   -- var.elim.:  7000/10268          
c   -- var.elim.:  8000/10268          
c   -- var.elim.:  9000/10268          
c   -- var.elim.:  10000/10268          
c   -- var.elim.:  10268/10268          
c   -- var.elim.:  709/709          
c   -- subsuming                       
c   -- var.elim.:  409/409          
c   -- var.elim.:  306/306          
c   -- subsuming                       
c   -- var.elim.:  240/240          
c |         0 |   34266   105908 |      --       0       --      -- |     --   | -1427/-5127
c |         0 |   34266   105908 |   13706       0        0     nan |  0.000 % |
c |       107 |   34266   105908 |   15077     107     1746    16.3 |  2.444 % |
c |       257 |   34156   105521 |   16531     256     6964    27.2 |  2.572 % |
c ==============================================================================
c (current CPU-time: 1.41379 s)
c ==============================================================================
c [1mFound solution: 4642[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8142   maxlim: 192549   bits: 18/18
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       458 |   91044   308669 |   27313     457    30789    67.4 |  2.572 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9335          
c   -- var.elim.:  2000/9335          
c   -- var.elim.:  3000/9335          
c   -- var.elim.:  4000/9335          
c   -- var.elim.:  5000/9335          
c   -- var.elim.:  6000/9335          
c   -- var.elim.:  7000/9335          
c   -- var.elim.:  8000/9335          
c   -- var.elim.:  9000/9335          
c   -- var.elim.:  9335/9335          
c   -- var.elim.:  43/43          
c |       458 |   90926   308132 |      --     457       --      -- |     --   | -114/-507
c |       458 |   90926   308132 |   36370     457    30789    67.4 |  2.572 % |
c |       558 |   90828   307797 |   39964     556    35928    64.6 |  1.555 % |
c |       708 |   90731   307464 |   43913     705    45313    64.3 |  1.626 % |
c |       933 |   90731   307464 |   48305     930    67612    72.7 |  1.626 % |
c |      1270 |   90731   307464 |   53135    1267    96344    76.0 |  1.626 % |
c |      1780 |   90731   307464 |   58449    1777   154813    87.1 |  1.626 % |
c |      2540 |   90731   307464 |   64294    2537   284854   112.3 |  1.626 % |
c |      3680 |   90714   307394 |   70710    3674   350185    95.3 |  1.632 % |
c |      5388 |   90714   307394 |   77781    5382   781951   145.3 |  1.632 % |
c |      7951 |   90714   307394 |   85559    7945  1160627   146.1 |  1.632 % |
c ==============================================================================
c (current CPU-time: 24.6103 s)
c ==============================================================================
c [1mFound solution: 4407[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192784   bits: 18/18
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8209 |   90751   307558 |   27225    8203  1175824   143.3 |  1.632 % |
c   -- subsuming                       
c   -- var.elim.:  119/119          
c   -- var.elim.:  42/42          
c |      8209 |   90744   307434 |      --    8203       --      -- |     --   | -7/-121
c |      8209 |   90744   307434 |   36297    8061  1157632   143.6 |  1.632 % |
c |      8309 |   90744   307434 |   39927    8161  1203744   147.5 |  1.648 % |
c |      8459 |   90744   307434 |   43920    8311  1212490   145.9 |  1.648 % |
c |      8685 |   90744   307434 |   48312    8537  1261562   147.8 |  1.648 % |
c |      9023 |   90744   307434 |   53143    8875  1316530   148.3 |  1.648 % |
c |      9529 |   90723   307358 |   58444    9379  1377566   146.9 |  1.659 % |
c |     10288 |   90723   307358 |   64288   10138  1503919   148.3 |  1.659 % |
c |     11429 |   90723   307358 |   70717   11279  1812582   160.7 |  1.659 % |
c |     13140 |   90617   306946 |   77698   12981  2046836   157.7 |  1.697 % |
c |     15702 |   90617   306946 |   85468   15543  2708910   174.3 |  1.697 % |
c |     19546 |   90586   306840 |   93982   19386  3787906   195.4 |  1.719 % |
c |     25313 |   90586   306840 |  103380   25153  6032829   239.8 |  1.719 % |
c ==============================================================================
c (current CPU-time: 91.3411 s)
c ==============================================================================
c [1mFound solution: 4259[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192932   bits: 18/18
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     25427 |   90603   306944 |   27180   25267  6050055   239.4 |  1.719 % |
c   -- subsuming                       
c   -- var.elim.:  105/105          
c   -- var.elim.:  45/45          
c |     25427 |   90587   306881 |      --   25267       --      -- |     --   | -16/-59
c |     25427 |   90587   306881 |   36234   24480  5802691   237.0 |  1.719 % |
c |     25529 |   90587   306881 |   39858   24582  5809705   236.3 |  1.741 % |
c |     25679 |   90579   306848 |   43840   24729  5820871   235.4 |  1.746 % |
c |     25904 |   90544   306717 |   48205   24953  5834479   233.8 |  1.768 % |
c |     26242 |   90544   306717 |   53026   25291  5920443   234.1 |  1.768 % |
c |     26749 |   90544   306717 |   58328   25798  6051511   234.6 |  1.768 % |
c |     27510 |   90544   306717 |   64161   26559  6191958   233.1 |  1.768 % |
c |     28649 |   90544   306717 |   70577   27698  6409542   231.4 |  1.768 % |
c |     30357 |   90544   306717 |   77635   29406  6746367   229.4 |  1.768 % |
c |     32920 |   90544   306717 |   85399   31969  7533542   235.7 |  1.768 % |
c |     36764 |   90544   306717 |   93939   35813  8980261   250.8 |  1.768 % |
c |     42532 |   90530   306658 |  103317   41571 10975200   264.0 |  1.773 % |
c |     51181 |   90530   306658 |  113648   50220 14919586   297.1 |  1.773 % |
c ==============================================================================
c (current CPU-time: 229.902 s)
c ==============================================================================
c [1mFound solution: 4164[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 193027   bits: 18/18
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     53173 |   90467   306429 |   27140   52207 15544750   297.8 |  1.773 % |
c   -- subsuming                       
c   -- var.elim.:  79/79          
c   -- var.elim.:  35/35          
c |     53173 |   90429   306167 |      --   52207       --      -- |     --   | -25/-68
c |     53173 |   90429   306167 |   36171   51779 14976050   289.2 |  1.773 % |
c |     53273 |   90429   306167 |   39788   17458  4825033   276.4 |  1.834 % |
c |     53423 |   90429   306167 |   43767   17608  4871276   276.7 |  1.834 % |
c |     53648 |   90429   306167 |   48144   17833  4909115   275.3 |  1.834 % |
c |     53986 |   90429   306167 |   52958   18171  5078314   279.5 |  1.834 % |
c |     54494 |   90386   306019 |   58227   18675  5126458   274.5 |  1.862 % |
c |     55255 |   90386   306019 |   64049   19436  5336230   274.6 |  1.862 % |
c |     56394 |   90338   305843 |   70417   20566  5768784   280.5 |  1.889 % |
c |     58102 |   90338   305843 |   77459   22274  6326382   284.0 |  1.889 % |
c |     60664 |   90338   305843 |   85204   24836  7311124   294.4 |  1.889 % |
c |     64509 |   90338   305843 |   93725   28681  9543271   332.7 |  1.889 % |
c ==============================================================================
c (current CPU-time: 302.644 s)
c ==============================================================================
c [1mFound solution: 4129[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 193062   bits: 18/18
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     66998 |   90377   306009 |   27113   31170 10209084   327.5 |  1.889 % |
c   -- subsuming                       
c   -- var.elim.:  84/84          
c   -- var.elim.:  26/26          
c |     66998 |   90305   305710 |      --   31170       --      -- |     --   | -72/-295
c |     66998 |   90305   305710 |   36122   30872  9851316   319.1 |  1.889 % |
c |     67101 |   90305   305710 |   39734   30975  9865070   318.5 |  1.943 % |
c |     67251 |   90305   305710 |   43707   31125  9894465   317.9 |  1.943 % |
c |     67476 |   90305   305710 |   48078   31350  9948456   317.3 |  1.943 % |
c |     67813 |   90305   305710 |   52886   31687  9990916   315.3 |  1.943 % |
c |     68322 |   90305   305710 |   58174   32196 10170328   315.9 |  1.943 % |
c |     69082 |   90294   305673 |   63984   32955 10431470   316.5 |  1.948 % |
c |     70224 |   90294   305673 |   70382   34097 10888723   319.3 |  1.948 % |
c |     71932 |   90240   305475 |   77374   35799 11523850   321.9 |  1.970 % |
c |     74494 |   90240   305475 |   85112   38361 12253590   319.4 |  1.970 % |
c |     78339 |   90240   305475 |   93623   42206 13631017   323.0 |  1.970 % |
c |     84106 |   90240   305475 |  102986   47973 16072370   335.0 |  1.970 % |
c ==============================================================================
c (current CPU-time: 412.73 s)
c ==============================================================================
c [1mFound solution: 4117[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 193074   bits: 18/18
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     88422 |   90261   305588 |   27078   52289 17601186   336.6 |  1.970 % |
c   -- subsuming                       
c   -- var.elim.:  63/63          
c   -- var.elim.:  33/33          
c |     88422 |   90249   305587 |      --   52289       --      -- |     --   | -12/2
c |     88422 |   90249   305587 |   36099   46975 12515688   266.4 |  1.970 % |
c |     88523 |   90249   305587 |   39709   18334  4174854   227.7 |  1.987 % |
c |     88674 |   90249   305587 |   43680   18485  4226500   228.6 |  1.987 % |
c |     88903 |   90249   305587 |   48048   18714  4258130   227.5 |  1.987 % |
c |     89241 |   90249   305587 |   52853   19052  4312957   226.4 |  1.987 % |
c |     89748 |   90238   305550 |   58131   19557  4418089   225.9 |  1.992 % |
c |     90507 |   90238   305550 |   63944   20316  4554482   224.2 |  1.992 % |
c |     91648 |   90238   305550 |   70339   21457  4922920   229.4 |  1.992 % |
c |     93357 |   90238   305550 |   77373   23166  5871128   253.4 |  1.992 % |
c |     95921 |   90238   305550 |   85110   25730  7181864   279.1 |  1.992 % |
c |     99766 |   90238   305550 |   93621   29575  8991530   304.0 |  1.992 % |
c |    105532 |   90238   305550 |  102983   35341 11029930   312.1 |  1.992 % |
c |    114184 |   90238   305550 |  113282   43993 15644447   355.6 |  1.992 % |
c |    127159 |   90194   305368 |  124549   56963 22974346   403.3 |  2.003 % |
c |    146623 |   90164   305245 |  136959   76425 35743580   467.7 |  2.009 % |
c ==============================================================================
c (current CPU-time: 841.001 s)
c ==============================================================================
c [1mFound solution: 4106[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 193085   bits: 18/18
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    152279 |   90160   305219 |   27047   82079 39176070   477.3 |  2.009 % |
c   -- subsuming                       
c   -- var.elim.:  109/109          
c   -- var.elim.:  19/19          
c |    152279 |   90140   305132 |      --   82079       --      -- |     --   | -19/-82
c |    152279 |   90140   305132 |   36056   82079 39176070   477.3 |  2.009 % |
c |    152379 |   90140   305132 |   39661   21500  7654925   356.0 |  2.041 % |
c |    152529 |   90140   305132 |   43627   21650  7669233   354.2 |  2.041 % |
c |    152755 |   90140   305132 |   47990   21876  7693123   351.7 |  2.041 % |
c |    153092 |   90140   305132 |   52789   22213  7756711   349.2 |  2.041 % |
c |    153599 |   90140   305132 |   58068   22720  7852870   345.6 |  2.041 % |
c |    154358 |   90140   305132 |   63875   23479  8070411   343.7 |  2.041 % |
c |    155499 |   90140   305132 |   70262   24620  8400492   341.2 |  2.041 % |
c |    157209 |   90140   305132 |   77289   26330  8998289   341.8 |  2.041 % |
c |    159772 |   90140   305132 |   85018   28893  9927760   343.6 |  2.041 % |
c |    163618 |   90140   305132 |   93519   32739 11903840   363.6 |  2.041 % |
c |    169386 |   90140   305132 |  102871   38507 14547881   377.8 |  2.041 % |
c |    178037 |   90103   304978 |  113112   47155 18814147   399.0 |  2.046 % |
c |    191011 |   90103   304978 |  124423   60129 31001287   515.6 |  2.046 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -CO100001_bit0 -CO100002_bit0 -CO100003_bit0 -CO100004_bit0 -CO100005_bit0 -CO100006_bit0 -CO100007_bit0 -CO100008_bit0 -CO100009_bit0 -CO100010_bit0 -CO100011_bit0 -CO100012_bit0 -CO100013_bit0 CO100014_bit0 -CO100015_bit0 -CO100016_bit0 -CO100017_bit0 -CO100018_bit0 -CO100019_bit0 -CO100020_bit0 -CO100021_bit0 CO100022_bit0 -CO100023_bit0 -CO100024_bit0 -CO100025_bit0 -CO100026_bit0 CO100027_bit0 -CO100028_bit0 -CO100029_bit0 -CO100030_bit0 -CO100031_bit0 CO100032_bit0 -CO100033_bit0 -CO100034_bit0 -CO100035_bit0 -CO100036_bit0 -CO100037_bit0 -CO100038_bit0 -CO100039_bit0 -CO100040_bit0 -CO100041_bit0 -CO100042_bit0 -CO100043_bit0 -CO100044_bit0 -CO100045_bit0 -CO100046_bit0 -CO100047_bit0 -CO100048_bit0 -CO100049_bit0 -CO100050_bit0 -CO100051_bit0 -CO100052_bit0 -CO100053_bit0 -CO100054_bit0 -CO100055_bit0 -CO100056_bit0 -CO100057_bit0 -CO100058_bit0 -CO100059_bit0 -CO100060_bit0 -CO100061_bit0 -CO100062_bit0 -CO100063_bit0 -CO100064_bit0 -CO100065_bit0 CO100066_bit0 -CO100067_bit0 -CO100068_bit0 -CO100069_bit0 -CO100070_bit0 -CO100071_bit0 -CO100072_bit0 -CO100073_bit0 -CO100074_bit0 -CO100075_bit0 -CO100076_bit0 -CO100077_bit0 -CO100078_bit0 -CO100079_bit0 -CO100080_bit0 -CO100081_bit0 -CO100082_bit0 -CO100083_bit0 -CO100084_bit0 -CO100085_bit0 -CO100086_bit0 -CO100087_bit0 -CO100088_bit0 -CO100089_bit0 -CO100090_bit0 -CO100091_bit0 CO100092_bit0 -CO100093_bit0 -CO100094_bit0 -CO100095_bit0 -CO100096_bit0 -CO100097_bit0 -CO100098_bit0 -CO100099_bit0 -CO100100_bit0 -CO100101_bit0 -CO100102_bit0 -CO100103_bit0 -CO100104_bit0 -CO100105_bit0 -CO100106_bit0 -CO100107_bit0 -CO100108_bit0 -CO100109_bit0 -CO100110_bit0 -CO100111_bit0 -CO100112_bit0 -CO100113_bit0 -CO100114_bit0 -CO100115_bit0 -CO100116_bit0 -CO100117_bit0 -CO100118_bit0 -CO100119_bit0 -CO100120_bit0 -CO100121_bit0 -CO100122_bit0 -CO100123_bit0 CO100124_bit0 -CO100125_bit0 -CO100126_bit0 -CO100127_bit0 -CO100128_bit0 -CO100129_bit0 -CO100130_bit0 -CO100131_bit0 CO100132_bit0 -CO100133_bit0 -CO100134_bit0 -CO100135_bit0 -CO100136_bit0 -CO100137_bit0 -CO100138_bit0 -CO100139_bit0 -CO100140_bit0 -CO100141_bit0 -CO100142_bit0 -CO100143_bit0 -CO100144_bit0 -CO100145_bit0 -CO100146_bit0 -CO100147_bit0 -CO100148_bit0 -CO100149_bit0 -CO100150_bit0 -CO100151_bit0 -CO100152_bit0 -CO100153_bit0 -CO100154_bit0 -CO100155_bit0 -CO100156_bit0 -CO100157_bit0 -CO100158_bit0 -CO100159_bit0 -CO100160_bit0 -CO100161_bit0 -CO100162_bit0 -CO100163_bit0 -CO100164_bit0 -CO100165_bit0 CO100166_bit0 -CO100167_bit0 -CO100168_bit0 -CO100169_bit0 -CO100170_bit0 -CO100171_bit0 -CO100172_bit0 -CO100173_bit0 -CO100174_bit0 -CO100175_bit0 -CO100176_bit0 -CO100177_bit0 -CO100178_bit0 -CO100179_bit0 -CO100180_bit0 -CO100181_bit0 -CO100182_bit0 CO100183_bit0 -CO100184_bit0 -CO100185_bit0 -CO100186_bit0 -CO100187_bit0 -CO100188_bit0 -CO100189_bit0 -CO100190_bit0 -CO100191_bit0 -CO100192_bit0 -CO100193_bit0 -CO100194_bit0 -CO100195_bit0 -CO100196_bit0 -CO100197_bit0 -CO100198_bit0 -CO100199_bit0 -CO100200_bit0 -CO100201_bit0 -CO100202_bit0 -CO100203_bit0 -CO100204_bit0 -CO100205_bit0 -CO100206_bit0 -CO100207_bit0 -CO100208_bit0 -CO100209_bit0 -CO100210_bit0 -CO100211_bit0 -CO100212_bit0 -CO100213_bit0 -CO100214_bit0 -CO100215_bit0 -CO100216_bit0 -CO100217_bit0 -CO100218_bit0 -CO100219_bit0 -CO100220_bit0 -CO100221_bit0 -CO100222_bit0 -CO100223_bit0 -CO100224_bit0 -CO100225_bit0 -CO100226_bit0 -CO100227_bit0 -CO100228_bit0 -CO100229_bit0 -CO100230_bit0 -CO100231_bit0 -CO100232_bit0 -CO100233_bit0 -CO100234_bit0 -CO100235_bit0 -CO100236_bit0 -CO100237_bit0 -CO100238_bit0 -CO100239_bit0 -CO100240_bit0 -CO100241_bit0 -CO100242_bit0 -CO100243_bit0 -CO100244_bit0 -CO100245_bit0 -CO100246_bit0 -CO100247_bit0 -CO100248_bit0 -CO100249_bit0 -CO100250_bit0 -CO100251_bit0 -CO100252_bit0 -CO100253_bit0 -CO100254_bit0 -CO100255_bit0 -CO100256_bit0 -CO100257_bit0 -CO100258_bit0 -CO100259_bit0 -CO100260_bit0 -CO100261_bit0 -CO100262_bit0 -CO100263_bit0 -CO100264_bit0 -CO100265_bit0 CO100266_bit0 -CO100267_bit0 -CO100268_bit0 -CO100269_bit0 -CO100270_bit0 -CO100271_bit0 -CO100272_bit0 -CO100273_bit0 -CO100274_bit0 -CO100275_bit0 -CO100276_bit0 -CO100277_bit0 -CO100278_bit0 -CO100279_bit0 -CO100280_bit0 -CO100281_bit0 -CO100282_bit0 -CO100283_bit0 -CO100284_bit0 -CO100285_bit0 -CO100286_bit0 -CO100287_bit0 -CO100288_bit0 -CO100289_bit0 -CO100290_bit0 -CO100291_bit0 -CO100292_bit0 -CO100293_bit0 -CO100294_bit0 -CO100295_bit0 -CO100296_bit0 -CO100297_bit0 -CO100298_bit0 -CO100299_bit0 -CO100300_bit0 -CO100301_bit0 -CO100302_bit0 -CO100303_bit0 -CO100304_bit0 -CO100305_bit0 -CO100306_bit0 -CO100307_bit0 -CO100308_bit0 -CO100309_bit0 -CO100310_bit0 -CO100311_bit0 -CO100312_bit0 -CO100313_bit0 -CO100314_bit0 -CO100315_bit0 -CO100316_bit0 -CO100317_bit0 -CO100318_bit0 -CO100319_bit0 -CO100320_bit0 -CO100321_bit0 -CO100322_bit0 -CO100323_bit0 -CO100324_bit0 -CO100325_bit0 -CO100326_bit0 -CO100327_bit0 -CO100328_bit0 -CO100329_bit0 CO100330_bit0 -CO100331_bit0 -CO100332_bit0 -CO100333_bit0 -CO100334_bit0 -CO100335_bit0 -CO100336_bit0 -CO100337_bit0 -CO100338_bit0 -CO100339_bit0 -CO100340_bit0 -CO100341_bit0 -CO100342_bit0 -CO100343_bit0 -CO100344_bit0 -CO100345_bit0 -CO100346_bit0 -CO100347_bit0 -CO100348_bit0 -CO100349_bit0 -CO100350_bit0 -CO100351_bit0 -CO100352_bit0 -CO100353_bit0 -CO100354_bit0 -CO100355_bit0 -CO100356_bit0 -CO100357_bit0 -CO100358_bit0 -CO100359_bit0 -CO100360_bit0 -CO100361_bit0 -CO100362_bit0 -CO100363_bit0 -CO100364_bit0 -CO100365_bit0 -CO100366_bit0 -CO100367_bit0 -CO100368_bit0 -CO100369_bit0 -CO100370_bit0 -CO100371_bit0 -CO100372_bit0 -CO100373_bit0 -CO100374_bit0 -CO100375_bit0 -CO100376_bit0 CO100377_bit0 -CO100378_bit0 -CO100379_bit0 -CO100380_bit0 -CO100381_bit0 -CO100382_bit0 -CO100383_bit0 -CO100384_bit0 -CO100385_bit0 -CO100386_bit0 -CO100387_bit0 -CO100388_bit0 -CO100389_bit0 -CO100390_bit0 -CO100391_bit0 -CO100392_bit0 -CO100393_bit0 -CO100394_bit0 -CO100395_bit0 -CO100396_bit0 -CO100397_bit0 -CO100398_bit0 -CO100399_bit0 -CO100400_bit0 -CO100401_bit0 -CO100402_bit0 -CO100403_bit0 -CO100404_bit0 -CO100405_bit0 -CO100406_bit0 -CO100407_bit0 -CO100408_bit0 -CO100409_bit0 -CO100410_bit0 -CO100411_bit0 -CO100412_bit0 -CO100413_bit0 -CO100414_bit0 -CO100415_bit0 -CO100416_bit0 -CO100417_bit0 -CO100418_bit0 -CO100419_bit0 -CO100420_bit0 -CO100421_bit0 -CO100422_bit0 -CO100423_bit0 -CO100424_bit0 -CO100425_bit0 -CO100426_bit0 -CO100427_bit0 -CO100428_bit0 -CO100429_bit0 -CO100430_bit0 -CO100431_bit0 -CO100432_bit0 -CO100433_bit0 -CO100434_bit0 -CO100435_bit0 -CO100436_bit0 -CO100437_bit0 -CO100438_bit0 -CO100439_bit0 -CO100440_bit0 -CO100441_bit0 -CO100442_bit0 -CO100443_bit0 -CO100444_bit0 -CO100445_bit0 -CO100446_bit0 -CO100447_bit0 -CO100448_bit0 -CO100449_bit0 -CO100450_bit0 -CO100451_bit0 -CO100452_bit0 -CO100453_bit0 -CO100454_bit0 -CO100455_bit0 CO100456_bit0 -CO100457_bit0 -CO100458_bit0 -CO100459_bit0 -CO100460_bit0 -CO100461_bit0 -CO100462_bit0 -CO100463_bit0 -CO100464_bit0 -CO100465_bit0 -CO100466_bit0 -CO100467_bit0 -CO100468_bit0 -CO100469_bit0 -CO100470_bit0 -CO100471_bit0 -CO100472_bit0 -CO100473_bit0 -CO100474_bit0 -CO100475_bit0 -CO100476_bit0 -CO100477_bit0 -CO100478_bit0 -CO100479_bit0 -CO100480_bit0 -CO100481_bit0 -CO100482_bit0 -CO100483_bit0 -CO100484_bit0 -CO100485_bit0 -CO100486_bit0 -CO100487_bit0 -CO100488_bit0 -CO100489_bit0 -CO100490_bit0 -CO100491_bit0 -CO100492_bit0 -CO100493_bit0 -CO100494_bit0 -CO100495_bit0 -CO100496_bit0 CO100497_bit0 -CO100498_bit0 -CO100499_bit0 -CO100500_bit0 -CO100501_bit0 -CO100502_bit0 -CO100503_bit0 -CO100504_bit0 -CO100505_bit0 -CO100506_bit0 -CO100507_bit0 -CO100508_bit0 -CO100509_bit0 -CO100510_bit0 -CO100511_bit0 -CO100512_bit0 -CO100513_bit0 -CO100514_bit0 -CO100515_bit0 -CO100516_bit0 -CO100517_bit0 -CO100518_bit0 -CO100519_bit0 -CO100520_bit0 -CO100521_bit0 -CO100522_bit0 -CO100523_bit0 -CO100524_bit0 -CO100525_bit0 -CO100526_bit0 -CO100527_bit0 -CO100528_bit0 -CO100529_bit0 -CO100530_bit0 -CO100531_bit0 -CO100532_bit0 -CO100533_bit0 -CO100534_bit0 -CO100535_bit0 -CO100536_bit0 -CO100537_bit0 -CO100538_bit0 -CO100539_bit0 -CO100540_bit0 -CO100541_bit0 -CO100542_bit0 -CO100543_bit0 -CO100544_bit0 -CO100545_bit0 -CO100546_bit0 -CO100547_bit0 -CO100548_bit0 -CO100549_bit0 -CO100550_bit0 -CO100551_bit0 CO100552_bit0 -CO100553_bit0 -CO100554_bit0 -CO100555_bit0 -CO100556_bit0 -CO100557_bit0 -CO100558_bit0 -CO100559_bit0 -CO100560_bit0 -CO100561_bit0 -CO100562_bit0 -CO100563_bit0 CO100564_bit0 -CO100565_bit0 -CO100566_bit0 -CO100567_bit0 -CO100568_bit0 -CO100569_bit0 -CO100570_bit0 -CO100571_bit0 -CO100572_bit0 -CO100573_bit0 -CO100574_bit0 -CO100575_bit0 -CO100576_bit0 -CO100577_bit0 -CO100578_bit0 -CO100579_bit0 -CO100580_bit0 -CO100581_bit0 -CO100582_bit0 -CO100583_bit0 -CO100584_bit0 -CO100585_bit0 -CO100586_bit0 -CO100587_bit0 -CO100588_bit0 -CO100589_bit0 -CO100590_bit0 -CO100591_bit0 -CO100592_bit0 -CO100593_bit0 -CO100594_bit0 -CO100595_bit0 -CO100596_bit0 -CO100597_bit0 -CO100598_bit0 -CO100599_bit0 -CO100600_bit0 -CO100601_bit0 -CO100602_bit0 -CO100603_bit0 -CO100604_bit0 -CO100605_bit0 -CO100606_bit0 -CO100607_bit0 -CO100608_bit0 -CO100609_bit0 -CO100610_bit0 -CO100611_bit0 -CO100612_bit0 -CO100613_bit0 -CO100614_bit0 -CO100615_bit0 -CO100616_bit0 -CO100617_bit0 -CO100618_bit0 -CO100619_bit0 -CO100620_bit0 -CO100621_bit0 -CO100622_bit0 -CO100623_bit0 -CO100624_bit0 -CO100625_bit0 -CO100626_bit0 -CO100627_bit0 -CO100628_bit0 -CO100629_bit0 -CO100630_bit0 -CO100631_bit0 -CO100632_bit0 -CO100633_bit0 -CO100634_bit0 -CO100635_bit0 -CO100636_bit0 -CO100637_bit0 -CO100638_bit0 -CO100639_bit0 -CO100640_bit0 -CO100641_bit0 -CO100642_bit0 -CO100643_bit0 -CO100644_bit0 -CO100645_bit0 -CO100646_bit0 -CO100647_bit0 -CO100648_bit0 -CO100649_bit0 -CO100650_bit0 -CO100651_bit0 -CO100652_bit0 -CO100653_bit0 -CO100654_bit0 -CO100655_bit0 -CO100656_bit0 -CO100657_bit0 -CO100658_bit0 -CO100659_bit0 -CO100660_bit0 -CO100661_bit0 -CO100662_bit0 -CO100663_bit0 -CO100664_bit0 -CO100665_bit0 -CO100666_bit0 -CO100667_bit0 -CO100668_bit0 -CO100669_bit0 -CO100670_bit0 -CO100671_bit0 -CO100672_bit0 -CO100673_bit0 -CO100674_bit0 -CO100675_bit0 -CO100676_bit0 -CO100677_bit0 -CO100678_bit0 -CO100679_bit0 -CO100680_bit0 -CO100681_bit0 -CO100682_bit0 -CO100683_bit0 -CO100684_bit0 -CO100685_bit0 -CO100686_bit0 -CO100687_bit0 -CO100688_bit0 -CO100689_bit0 -CO100690_bit0 -CO100691_bit0 -CO100692_bit0 -CO100693_bit0 -CO100694_bit0 -CO100695_bit0 -CO100696_bit0 -CO100697_bit0 -CO100698_bit0 -CO100699_bit0 -CO100700_bit0 -CO100701_bit0 CO100702_bit0 -CO100703_bit0 -CO100704_bit0 -CO100705_bit0 -CO100706_bit0 -CO100707_bit0 -CO100708_bit0 -CO100709_bit0 -CO100710_bit0 -CO100711_bit0 -CO100712_bit0 -CO100713_bit0 -CO100714_bit0 -CO100715_bit0 -CO100716_bit0 -CO100717_bit0 -CO100718_bit0 -CO100719_bit0 -CO100720_bit0 -CO100721_bit0 -CO100722_bit0 -CO100723_bit0 -CO100724_bit0 -CO100725_bit0 -CO100726_bit0 -CO100727_bit0 -CO100728_bit0 -CO100729_bit0 -CO100730_bit0 -CO100731_bit0 -CO100732_bit0 -CO100733_bit0 -CO100734_bit0 -CO100735_bit0 -CO100736_bit0 -CO100737_bit0 -CO100738_bit0 -CO100739_bit0 -CO100740_bit0 -CO100741_bit0 -CO100742_bit0 -CO100743_bit0 -CO100744_bit0 -CO100745_bit0 -CO100746_bit0 -CO100747_bit0 -CO100748_bit0 -CO100749_bit0 -CO100750_bit0 -CO100751_bit0 -CO100752_bit0 -CO100753_bit0 -CO100754_bit0 -CO100755_bit0 -CO100756_bit0 -CO100757_bit0 -CO100758_bit0 -CO100759_bit0 -CO100760_bit0 -CO100761_bit0 -CO100762_bit0 -CO100763_bit0 -CO100764_bit0 -CO100765_bit0 -CO100766_bit0 -CO100767_bit0 -CO100768_bit0 -CO100769_bit0 -CO100770_bit0 -CO100771_bit0 -CO100772_bit0 -CO100773_bit0 -CO100774_bit0 -CO100775_bit0 -CO100776_bit0 -CO100777_bit0 -CO100778_bit0 -CO100779_bit0 -CO100780_bit0 CO100781_bit0 -CO100782_bit0 -CO100783_bit0 -CO100784_bit0 -CO100785_bit0 -CO100786_bit0 -CO100787_bit0 -CO100788_bit0 -CO100789_bit0 -CO100790_bit0 -CO100791_bit0 -CO100792_bit0 -CO100793_bit0 -CO100794_bit0 -CO100795_bit0 -CO100796_bit0 -CO100797_bit0 -CO100798_bit0 -CO100799_bit0 -CO100800_bit0 -CO100801_bit0 -CO100802_bit0 -CO100803_bit0 -CO100804_bit0 -CO100805_bit0 -CO100806_bit0 CO100807_bit0 -CO100808_bit0 -CO100809_bit0 -CO100810_bit0 -CO100811_bit0 -CO100812_bit0 -CO100813_bit0 -CO100814_bit0 -CO100815_bit0 -CO100816_bit0 -CO100817_bit0 -CO100818_bit0 -CO100819_bit0 -CO100820_bit0 -CO100821_bit0 -CO100822_bit0 -CO100823_bit0 -CO100824_bit0 -CO100825_bit0 -CO100826_bit0 -CO100827_bit0 -CO100828_bit0 -CO100829_bit0 -CO100830_bit0 -CO100831_bit0 -CO100832_bit0 -CO100833_bit0 -CO100834_bit0 -CO100835_bit0 CO100836_bit0 -CO100837_bit0 -CO100838_bit0 -CO100839_bit0 -CO100840_bit0 -CO100841_bit0 -CO100842_bit0 -CO100843_bit0 -CO100844_bit0 -CO100845_bit0 -CO100846_bit0 -CO100847_bit0 -CO100848_bit0 -CO100849_bit0 -CO100850_bit0 -CO100851_bit0 -CO100852_bit0 -CO100853_bit0 -CO100854_bit0 -CO100855_bit0 -CO100856_bit0 -CO100857_bit0 -CO100858_bit0 -CO100859_bit0 -CO100860_bit0 -CO100861_bit0 -CO100862_bit0 -CO100863_bit0 -CO100864_bit0 -CO100865_bit0 -CO100866_bit0 -CO100867_bit0 -CO100868_bit0 -CO100869_bit0 -CO100870_bit0 -CO100871_bit0 -CO100872_bit0 -CO100873_bit0 -CO100874_bit0 -CO100875_bit0 -CO100876_bit0 -CO100877_bit0 -CO100878_bit0 -CO100879_bit0 -CO100880_bit0 -CO100881_bit0 -CO100882_bit0 -CO100883_bit0 -CO100884_bit0 -CO100885_bit0 -CO100886_bit0 -CO100887_bit0 -CO100888_bit0 -CO100889_bit0 -CO100890_bit0 -CO100891_bit0 -CO100892_bit0 -CO100893_bit0 -CO100894_bit0 -CO100895_bit0 -CO100896_bit0 -CO100897_bit0 -CO100898_bit0 -CO100899_bit0 -CO100900_bit0 -CO100901_bit0 -CO100902_bit0 -CO100903_bit0 -CO100904_bit0 -CO100905_bit0 -CO100906_bit0 -CO100907_bit0 -CO100908_bit0 -CO100909_bit0 -CO100910_bit0 -CO100911_bit0 -CO100912_bit0 -CO100913_bit0 -CO100914_bit0 -CO100915_bit0 -CO100916_bit0 -CO100917_bit0 -CO100918_bit0 -CO100919_bit0 -CO100920_bit0 -CO100921_bit0 -CO100922_bit0 -CO100923_bit0 -CO100924_bit0 -CO100925_bit0 -CO100926_bit0 -CO100927_bit0 -CO100928_bit0 -CO100929_bit0 -CO100930_bit0 -CO100931_bit0 -CO100932_bit0 -CO100933_bit0 -CO100934_bi#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/54 3461
Raw data (stat): 3461 (runsolver) R 3460 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488919024 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0006 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 8372 0 0 0 980 18 0 0 25 0 1 0 488919024 34435072 7030 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8407 7030 603 41 0 8366 0
vsize: 33628
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 8950 0 0 0 1978 20 0 0 25 0 1 0 488919024 36810752 7608 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8987 7608 603 41 0 8946 0
vsize: 35948
[startup+30.0012 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 10157 0 0 0 2974 24 0 0 25 0 1 0 488919024 39407616 8285 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9621 8285 603 41 0 9580 0
vsize: 38484
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 10704 0 0 0 3972 25 0 0 25 0 1 0 488919024 41652224 8832 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10169 8832 603 41 0 10128 0
vsize: 40676
[startup+50.0003 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 11353 0 0 0 4970 28 0 0 25 0 1 0 488919024 44294144 9481 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10814 9481 603 41 0 10773 0
vsize: 43256
[startup+59.9999 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 12088 0 0 0 5968 30 0 0 25 0 1 0 488919024 47407104 10216 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11574 10216 603 41 0 11533 0
vsize: 46296
[startup+69.9997 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 12900 0 0 0 6965 33 0 0 25 0 1 0 488919024 50688000 11028 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12375 11028 603 41 0 12334 0
vsize: 49500
[startup+80 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 14046 0 0 0 7963 36 0 0 25 0 1 0 488919024 55427072 12174 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13532 12174 603 41 0 13491 0
vsize: 54128
[startup+89.9995 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 14802 0 0 0 8961 38 0 0 25 0 1 0 488919024 58441728 12930 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14268 12931 603 41 0 14227 0
vsize: 57072
[startup+99.9997 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 15789 0 0 0 9958 40 0 0 25 0 1 0 488919024 59322368 13151 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14483 13151 603 41 0 14442 0
vsize: 57932
[startup+110 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 16169 0 0 0 10956 42 0 0 25 0 1 0 488919024 60915712 13531 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14872 13531 603 41 0 14831 0
vsize: 59488
[startup+119.999 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 16754 0 0 0 11955 43 0 0 25 0 1 0 488919024 63295488 14116 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15453 14116 603 41 0 15412 0
vsize: 61812
[startup+129.999 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 17470 0 0 0 12953 45 0 0 25 0 1 0 488919024 66187264 14832 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16159 14832 603 41 0 16118 0
vsize: 64636
[startup+139.998 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 18363 0 0 0 13951 47 0 0 25 0 1 0 488919024 70012928 15725 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17093 15725 603 41 0 17052 0
vsize: 68372
[startup+149.998 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 19041 0 0 0 14950 48 0 0 25 0 1 0 488919024 72749056 16403 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17761 16403 603 41 0 17720 0
vsize: 71044
[startup+159.998 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 20192 0 0 0 15946 53 0 0 25 0 1 0 488919024 77500416 17554 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18921 17554 603 41 0 18880 0
vsize: 75684
[startup+169.997 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 20713 0 0 0 16944 55 0 0 25 0 1 0 488919024 79589376 18075 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19431 18075 603 41 0 19390 0
vsize: 77724
[startup+179.998 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 21571 0 0 0 17941 58 0 0 25 0 1 0 488919024 83148800 18933 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20300 18933 603 41 0 20259 0
vsize: 81200
[startup+189.998 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 22632 0 0 0 18939 61 0 0 25 0 1 0 488919024 87470080 19994 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21355 19994 603 41 0 21314 0
vsize: 85420
[startup+199.997 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 23553 0 0 0 19936 63 0 0 25 0 1 0 488919024 91283456 20915 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22286 20915 603 41 0 22245 0
vsize: 89144
[startup+209.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 24338 0 0 0 20934 65 0 0 25 0 1 0 488919024 94441472 21700 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23057 21700 603 41 0 23016 0
vsize: 92228
[startup+219.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 24981 0 0 0 21934 66 0 0 25 0 1 0 488919024 97067008 22343 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23698 22343 603 41 0 23657 0
vsize: 94792
[startup+229.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 25419 0 0 0 22933 67 0 0 25 0 1 0 488919024 98881536 22781 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24141 22781 603 41 0 24100 0
vsize: 96564
[startup+239.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26101 0 0 0 23931 69 0 0 25 0 1 0 488919024 100528128 23150 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+249.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26101 0 0 0 24931 69 0 0 25 0 1 0 488919024 100528128 23150 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+259.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26101 0 0 0 25931 69 0 0 25 0 1 0 488919024 100528128 23150 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+269.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26101 0 0 0 26930 69 0 0 25 0 1 0 488919024 100528128 23150 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+279.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26101 0 0 0 27930 69 0 0 25 0 1 0 488919024 100528128 23150 4294967295 134512640 134672761 3221224544 3221223680 134614736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+289.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26101 0 0 0 28930 69 0 0 25 0 1 0 488919024 100528128 23150 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+299.995 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26101 0 0 0 29931 69 0 0 25 0 1 0 488919024 100528128 23150 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+309.995 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26536 0 0 0 30930 70 0 0 25 0 1 0 488919024 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+319.996 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26536 0 0 0 31930 70 0 0 25 0 1 0 488919024 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+329.995 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26536 0 0 0 32930 70 0 0 25 0 1 0 488919024 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+339.995 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26536 0 0 0 33930 70 0 0 25 0 1 0 488919024 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+349.994 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26536 0 0 0 34930 70 0 0 25 0 1 0 488919024 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+359.995 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26536 0 0 0 35930 70 0 0 25 0 1 0 488919024 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+369.995 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26536 0 0 0 36930 70 0 0 25 0 1 0 488919024 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+379.995 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26536 0 0 0 37930 70 0 0 25 0 1 0 488919024 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+389.996 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 26911 0 0 0 38929 71 0 0 25 0 1 0 488919024 101249024 23374 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24719 23374 603 41 0 24678 0
vsize: 98876
[startup+399.995 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 27694 0 0 0 39927 73 0 0 25 0 1 0 488919024 104538112 24157 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25522 24157 603 41 0 25481 0
vsize: 102088
[startup+409.996 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 28317 0 0 0 40926 75 0 0 25 0 1 0 488919024 107024384 24780 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26129 24780 603 41 0 26088 0
vsize: 104516
[startup+419.995 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 41923 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+429.996 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 42923 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+439.995 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 43923 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+449.995 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 44923 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+459.996 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 45923 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+469.995 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 46923 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+479.995 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 47923 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+489.994 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 48924 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+499.994 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 49923 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+509.994 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 50923 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+519.993 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 51923 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+529.993 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 52924 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223536 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+539.993 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 53924 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+549.993 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 54924 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223584 134613768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+559.993 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 55923 78 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+569.993 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29339 0 0 0 56923 79 0 0 25 0 1 0 488919024 109318144 25339 4294967295 134512640 134672761 3221224544 3221223584 134612966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+579.994 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 29392 0 0 0 57922 79 0 0 25 0 1 0 488919024 109584384 25392 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26754 25392 603 41 0 26713 0
vsize: 107016
[startup+589.993 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 30769 0 0 0 58919 83 0 0 25 0 1 0 488919024 115220480 26769 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28130 26769 603 41 0 28089 0
vsize: 112520
[startup+599.992 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 31659 0 0 0 59916 85 0 0 25 0 1 0 488919024 118784000 27659 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29000 27659 603 41 0 28959 0
vsize: 116000
[startup+609.992 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 32670 0 0 0 60914 88 0 0 25 0 1 0 488919024 122986496 28670 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30026 28670 603 41 0 29985 0
vsize: 120104
[startup+619.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 33646 0 0 0 61911 91 0 0 25 0 1 0 488919024 126918656 29646 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30986 29646 603 41 0 30945 0
vsize: 123944
[startup+629.992 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 34475 0 0 0 62908 95 0 0 25 0 1 0 488919024 130351104 30475 4294967295 134512640 134672761 3221224544 3221223728 134615755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31824 30475 603 41 0 31783 0
vsize: 127296
[startup+639.992 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 34862 0 0 0 63907 95 0 0 25 0 1 0 488919024 131883008 30862 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32198 30862 603 41 0 32157 0
vsize: 128792
[startup+649.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 35490 0 0 0 64906 97 0 0 25 0 1 0 488919024 134504448 31490 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32838 31490 603 41 0 32797 0
vsize: 131352
[startup+659.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 36480 0 0 0 65904 99 0 0 25 0 1 0 488919024 138526720 32480 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33820 32480 603 41 0 33779 0
vsize: 135280
[startup+669.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 37495 0 0 0 66902 101 0 0 25 0 1 0 488919024 142639104 33495 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34824 33495 603 41 0 34783 0
vsize: 139296
[startup+679.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 38785 0 0 0 67899 104 0 0 25 0 1 0 488919024 147951616 34785 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36121 34785 603 41 0 36080 0
vsize: 144484
[startup+689.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 39532 0 0 0 68898 105 0 0 25 0 1 0 488919024 151072768 35532 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36883 35532 603 41 0 36842 0
vsize: 147532
[startup+699.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 40038 0 0 0 69897 106 0 0 25 0 1 0 488919024 153051136 36038 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37366 36038 603 41 0 37325 0
vsize: 149464
[startup+709.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 40785 0 0 0 70895 108 0 0 25 0 1 0 488919024 156454912 36785 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38197 36785 603 41 0 38156 0
vsize: 152788
[startup+719.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 41627 0 0 0 71894 110 0 0 25 0 1 0 488919024 159870976 37627 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39031 37629 603 41 0 38990 0
vsize: 156124
[startup+729.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 42551 0 0 0 72891 113 0 0 25 0 1 0 488919024 163635200 38551 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39950 38551 603 41 0 39909 0
vsize: 159800
[startup+739.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 43254 0 0 0 73889 115 0 0 25 0 1 0 488919024 166531072 39254 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40657 39254 603 41 0 40616 0
vsize: 162628
[startup+749.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 44050 0 0 0 74887 118 0 0 25 0 1 0 488919024 169816064 40050 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41459 40050 603 41 0 41418 0
vsize: 165836
[startup+759.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 44723 0 0 0 75885 120 0 0 25 0 1 0 488919024 172466176 40723 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42106 40723 603 41 0 42065 0
vsize: 168424
[startup+769.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 45426 0 0 0 76884 121 0 0 25 0 1 0 488919024 175448064 41426 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42834 41426 603 41 0 42793 0
vsize: 171336
[startup+779.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 46231 0 0 0 77881 124 0 0 25 0 1 0 488919024 178708480 42231 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43630 42231 603 41 0 43589 0
vsize: 174520
[startup+789.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 46993 0 0 0 78880 125 0 0 25 0 1 0 488919024 181796864 42993 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44384 42993 603 41 0 44343 0
vsize: 177536
[startup+799.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 47655 0 0 0 79878 127 0 0 25 0 1 0 488919024 184532992 43655 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45052 43655 603 41 0 45011 0
vsize: 180208
[startup+809.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 48010 0 0 0 80877 128 0 0 25 0 1 0 488919024 186007552 44010 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45412 44010 603 41 0 45371 0
vsize: 181648
[startup+819.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 48716 0 0 0 81875 130 0 0 25 0 1 0 488919024 188907520 44716 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46120 44716 603 41 0 46079 0
vsize: 184480
[startup+829.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 49564 0 0 0 82872 133 0 0 25 0 1 0 488919024 192266240 45564 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46940 45564 603 41 0 46899 0
vsize: 187760
[startup+839.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 50550 0 0 0 83871 135 0 0 25 0 1 0 488919024 196300800 46550 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47925 46550 603 41 0 47884 0
vsize: 191700
[startup+849.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 84868 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+859.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 85868 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+869.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 86868 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+879.992 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 87869 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+889.992 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 88868 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+899.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 89869 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+909.992 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 90869 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+919.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 91869 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+929.992 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 92869 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+939.992 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 93869 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+949.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 94869 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+959.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 95870 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+969.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 96870 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+979.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 97870 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+989.991 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 98869 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223584 134612471 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+999.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 99870 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1009.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 100870 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1019.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 101870 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1029.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 102870 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1039.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 103870 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615679 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1049.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 104870 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1059.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 105871 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1069.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 106871 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1079.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 107871 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1089.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 108871 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1099.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 109872 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1109.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 110872 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223680 134614710 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1119.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 111872 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1129.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 112872 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1139.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 113872 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1149.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 114873 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1159.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 115873 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1169.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 116873 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1179.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 117873 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1189.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51469 0 0 0 118873 137 0 0 25 0 1 0 488919024 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1199.99 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3461
Raw data (stat): 3461 (minisat+) R 3460 25347 25346 0 -1 0 51553 0 0 0 119873 138 0 0 25 0 1 0 488919024 198623232 47093 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48492 47093 603 41 0 48451 0
vsize: 193968
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 3461
Raw data (stat): 3461 (minisat+) Z 3460 25347 25346 0 -1 12 51554 0 0 0 119874 146 0 0 25 0 1 0 488919024 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.09
CPU time (s): 1200.21
CPU user time (s): 1198.74
CPU system time (s): 1.46778
CPU usage (%): 100.01
Max. virtual memory (Kb): 193968
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####