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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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	3744
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.09
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 22210

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-22 02:25:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11919 boxname=wulflinc19 idbench=917 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c39e3c2b993ee2185e2a1a3e73b9723  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-lp4l.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-lp4l.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-lp4l.opb
IDLAUNCH: 11919
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        435624 kB
Buffers:         17684 kB
Cached:         557988 kB
SwapCached:        560 kB
Active:          33476 kB
Inactive:       544252 kB
HighTotal:      131008 kB
HighFree:         4340 kB
LowTotal:       903652 kB
LowFree:        431284 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5172 kB
Slab:            15740 kB
Committed_AS:    63808 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:45:55 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 11919 7 1200.27 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.42678 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.9322 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: 92.26 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: 231.555 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: 305.084 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: 415.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: 845.285 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_bit0#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.95 0.94 2/55 13898
Raw data (stat): 13898 (runsolver) R 13897 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550101182 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.001 s]
Raw data (loadavg): 0.87 0.95 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 8365 0 0 0 979 19 0 0 25 0 1 0 550101182 34435072 7023 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8407 7023 603 41 0 8366 0
vsize: 33628
[startup+20.002 s]
Raw data (loadavg): 0.89 0.95 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 8944 0 0 0 1978 20 0 0 25 0 1 0 550101182 36810752 7602 4294967295 134512640 134672761 3221224544 3221223680 134614822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8987 7602 603 41 0 8946 0
vsize: 35948
[startup+30.0018 s]
Raw data (loadavg): 0.90 0.95 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 10157 0 0 0 2975 24 0 0 25 0 1 0 550101182 39407616 8285 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.0025 s]
Raw data (loadavg): 0.92 0.95 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 10690 0 0 0 3973 25 0 0 25 0 1 0 550101182 41652224 8818 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10169 8818 603 41 0 10128 0
vsize: 40676
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.96 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 11280 0 0 0 4971 27 0 0 25 0 1 0 550101182 44032000 9408 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10750 9408 603 41 0 10709 0
vsize: 43000
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.96 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 12039 0 0 0 5970 29 0 0 25 0 1 0 550101182 47144960 10167 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11510 10167 603 41 0 11469 0
vsize: 46040
[startup+70.0038 s]
Raw data (loadavg): 0.95 0.96 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 12794 0 0 0 6968 31 0 0 25 0 1 0 550101182 50290688 10922 4294967295 134512640 134672761 3221224544 3221223584 134612632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12278 10922 603 41 0 12237 0
vsize: 49112
[startup+80.0039 s]
Raw data (loadavg): 0.96 0.96 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 13997 0 0 0 7966 33 0 0 25 0 1 0 550101182 55164928 12125 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13468 12125 603 41 0 13427 0
vsize: 53872
[startup+90.0047 s]
Raw data (loadavg): 0.96 0.96 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 14718 0 0 0 8965 35 0 0 25 0 1 0 550101182 58175488 12846 4294967295 134512640 134672761 3221224544 3221223584 134614335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14203 12846 603 41 0 14162 0
vsize: 56812
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 15789 0 0 0 9962 37 0 0 25 0 1 0 550101182 59322368 13151 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14483 13151 603 41 0 14442 0
vsize: 57932
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 16135 0 0 0 10962 37 0 0 25 0 1 0 550101182 60780544 13497 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14839 13497 603 41 0 14798 0
vsize: 59356
[startup+120.006 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 16636 0 0 0 11961 38 0 0 25 0 1 0 550101182 62902272 13998 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15357 13998 603 41 0 15316 0
vsize: 61428
[startup+130.006 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 17363 0 0 0 12958 40 0 0 25 0 1 0 550101182 65794048 14725 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16063 14725 603 41 0 16022 0
vsize: 64252
[startup+140.006 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 18258 0 0 0 13955 44 0 0 25 0 1 0 550101182 69611520 15620 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16995 15620 603 41 0 16954 0
vsize: 67980
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 19040 0 0 0 14955 45 0 0 25 0 1 0 550101182 72749056 16402 4294967295 134512640 134672761 3221224544 3221223688 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17761 16402 603 41 0 17720 0
vsize: 71044
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 19967 0 0 0 15952 47 0 0 25 0 1 0 550101182 76570624 17329 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18694 17329 603 41 0 18653 0
vsize: 74776
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 20634 0 0 0 16951 48 0 0 25 0 1 0 550101182 79327232 17996 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19367 17996 603 41 0 19326 0
vsize: 77468
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 21436 0 0 0 17949 51 0 0 25 0 1 0 550101182 82620416 18798 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20171 18798 603 41 0 20130 0
vsize: 80684
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 22476 0 0 0 18947 53 0 0 25 0 1 0 550101182 86818816 19838 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21196 19838 603 41 0 21155 0
vsize: 84784
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 23403 0 0 0 19945 56 0 0 25 0 1 0 550101182 90628096 20765 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22126 20765 603 41 0 22085 0
vsize: 88504
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 24238 0 0 0 20942 58 0 0 25 0 1 0 550101182 94048256 21600 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22961 21600 603 41 0 22920 0
vsize: 91844
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 24918 0 0 0 21941 60 0 0 25 0 1 0 550101182 96800768 22280 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23633 22280 603 41 0 23592 0
vsize: 94532
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13898
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 25380 0 0 0 22940 61 0 0 25 0 1 0 550101182 98758656 22742 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24111 22742 603 41 0 24070 0
vsize: 96444
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26101 0 0 0 23938 62 0 0 25 0 1 0 550101182 100528128 23150 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26101 0 0 0 24939 63 0 0 25 0 1 0 550101182 100528128 23150 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26101 0 0 0 25939 63 0 0 25 0 1 0 550101182 100528128 23150 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26101 0 0 0 26938 63 0 0 25 0 1 0 550101182 100528128 23150 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26101 0 0 0 27938 63 0 0 25 0 1 0 550101182 100528128 23150 4294967295 134512640 134672761 3221224544 3221223728 134615835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26101 0 0 0 28938 63 0 0 25 0 1 0 550101182 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+300.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26101 0 0 0 29938 63 0 0 25 0 1 0 550101182 100528128 23150 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24543 23150 603 41 0 24502 0
vsize: 98172
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26536 0 0 0 30937 64 0 0 25 0 1 0 550101182 99692544 22999 4294967295 134512640 134672761 3221224544 3221223584 134614340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26536 0 0 0 31937 64 0 0 25 0 1 0 550101182 99692544 22999 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26536 0 0 0 32937 64 0 0 25 0 1 0 550101182 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26536 0 0 0 33937 64 0 0 25 0 1 0 550101182 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26536 0 0 0 34937 64 0 0 25 0 1 0 550101182 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26536 0 0 0 35937 64 0 0 25 0 1 0 550101182 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26536 0 0 0 36937 64 0 0 25 0 1 0 550101182 99692544 22999 4294967295 134512640 134672761 3221224544 3221223536 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26536 0 0 0 37937 64 0 0 25 0 1 0 550101182 99692544 22999 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22999 603 41 0 24298 0
vsize: 97356
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 26707 0 0 0 38937 64 0 0 25 0 1 0 550101182 100470784 23170 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24529 23170 603 41 0 24488 0
vsize: 98116
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 27487 0 0 0 39935 66 0 0 25 0 1 0 550101182 103612416 23950 4294967295 134512640 134672761 3221224544 3221223584 134612644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25296 23950 603 41 0 25255 0
vsize: 101184
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 28150 0 0 0 40934 67 0 0 25 0 1 0 550101182 106369024 24613 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25969 24613 603 41 0 25928 0
vsize: 103876
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 41931 71 0 0 25 0 1 0 550101182 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 42930 71 0 0 25 0 1 0 550101182 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+440.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 43931 71 0 0 25 0 1 0 550101182 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+450.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 44931 71 0 0 25 0 1 0 550101182 109318144 25339 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 45931 71 0 0 25 0 1 0 550101182 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 46931 71 0 0 25 0 1 0 550101182 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+480.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 47931 71 0 0 25 0 1 0 550101182 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+490.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 48931 71 0 0 25 0 1 0 550101182 109318144 25339 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 49931 71 0 0 25 0 1 0 550101182 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+510.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 50932 71 0 0 25 0 1 0 550101182 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+520.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 51932 71 0 0 25 0 1 0 550101182 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13900
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 52932 71 0 0 25 0 1 0 550101182 109318144 25339 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 53932 71 0 0 25 0 1 0 550101182 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+550.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 54932 71 0 0 25 0 1 0 550101182 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+560.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 55932 71 0 0 25 0 1 0 550101182 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+570.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 56932 71 0 0 25 0 1 0 550101182 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 29339 0 0 0 57932 71 0 0 25 0 1 0 550101182 109318144 25339 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26689 25339 603 41 0 26648 0
vsize: 106756
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 30112 0 0 0 58931 73 0 0 25 0 1 0 550101182 112541696 26112 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27476 26112 603 41 0 27435 0
vsize: 109904
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 31322 0 0 0 59929 75 0 0 25 0 1 0 550101182 117456896 27322 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28676 27322 603 41 0 28635 0
vsize: 114704
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 32293 0 0 0 60928 77 0 0 25 0 1 0 550101182 121409536 28293 4294967295 134512640 134672761 3221224544 3221223744 134610630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29641 28293 603 41 0 29600 0
vsize: 118564
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 33309 0 0 0 61926 79 0 0 25 0 1 0 550101182 125603840 29309 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30665 29309 603 41 0 30624 0
vsize: 122660
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 34145 0 0 0 62924 81 0 0 25 0 1 0 550101182 129040384 30145 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31504 30145 603 41 0 31463 0
vsize: 126016
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 34690 0 0 0 63922 82 0 0 25 0 1 0 550101182 131239936 30690 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32041 30690 603 41 0 32000 0
vsize: 128164
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 35148 0 0 0 64922 83 0 0 25 0 1 0 550101182 133066752 31148 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32487 31148 603 41 0 32446 0
vsize: 129948
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 36119 0 0 0 65919 86 0 0 25 0 1 0 550101182 137089024 32119 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33469 32119 603 41 0 33428 0
vsize: 133876
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 37030 0 0 0 66917 88 0 0 25 0 1 0 550101182 140853248 33030 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34388 33030 603 41 0 34347 0
vsize: 137552
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 38253 0 0 0 67915 91 0 0 25 0 1 0 550101182 145788928 34253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35593 34253 603 41 0 35552 0
vsize: 142372
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 39245 0 0 0 68912 93 0 0 25 0 1 0 550101182 149901312 35245 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36597 35245 603 41 0 36556 0
vsize: 146388
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 39806 0 0 0 69912 94 0 0 25 0 1 0 550101182 152129536 35806 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37141 35806 603 41 0 37100 0
vsize: 148564
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 40508 0 0 0 70911 95 0 0 25 0 1 0 550101182 155017216 36508 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37846 36508 603 41 0 37805 0
vsize: 151384
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 41217 0 0 0 71909 97 0 0 25 0 1 0 550101182 158162944 37217 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38614 37217 603 41 0 38573 0
vsize: 154456
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 42237 0 0 0 72907 99 0 0 25 0 1 0 550101182 162328576 38237 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39631 38237 603 41 0 39590 0
vsize: 158524
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 42941 0 0 0 73906 100 0 0 25 0 1 0 550101182 165232640 38941 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40340 38941 603 41 0 40299 0
vsize: 161360
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 43734 0 0 0 74905 102 0 0 25 0 1 0 550101182 168501248 39734 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41138 39734 603 41 0 41097 0
vsize: 164552
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 44467 0 0 0 75903 105 0 0 25 0 1 0 550101182 171532288 40467 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41878 40468 603 41 0 41837 0
vsize: 167512
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 45092 0 0 0 76901 106 0 0 25 0 1 0 550101182 174043136 41092 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42491 41092 603 41 0 42450 0
vsize: 169964
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 45877 0 0 0 77899 109 0 0 25 0 1 0 550101182 177254400 41877 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43275 41877 603 41 0 43234 0
vsize: 173100
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 46725 0 0 0 78897 110 0 0 25 0 1 0 550101182 180748288 42725 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44128 42725 603 41 0 44087 0
vsize: 176512
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 47365 0 0 0 79896 112 0 0 25 0 1 0 550101182 183386112 43365 4294967295 134512640 134672761 3221224544 3221223776 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44772 43365 603 41 0 44731 0
vsize: 179088
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 47868 0 0 0 80895 113 0 0 25 0 1 0 550101182 185339904 43868 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45249 43868 603 41 0 45208 0
vsize: 180996
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 48404 0 0 0 81894 114 0 0 25 0 1 0 550101182 187592704 44404 4294967295 134512640 134672761 3221224544 3221223584 134613809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45799 44404 603 41 0 45758 0
vsize: 183196
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13902
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 49157 0 0 0 82892 116 0 0 25 0 1 0 550101182 190717952 45157 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46562 45157 603 41 0 46521 0
vsize: 186248
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 50224 0 0 0 83890 119 0 0 25 0 1 0 550101182 194994176 46224 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47606 46224 603 41 0 47565 0
vsize: 190424
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 84886 122 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223800 134616170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 85886 122 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223712 134615859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 86886 122 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 87887 122 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 88887 122 0 0 25 0 1 0 550101182 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+900.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 89887 122 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 90887 122 0 0 25 0 1 0 550101182 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+920.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 91887 122 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 92888 122 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 93888 122 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223584 134603527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 94889 122 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+960.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 95889 122 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 96889 122 0 0 25 0 1 0 550101182 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+980.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 97889 122 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+990.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 98890 122 0 0 25 0 1 0 550101182 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+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 99890 122 0 0 25 0 1 0 550101182 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+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 100890 122 0 0 25 0 1 0 550101182 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+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 101890 123 0 0 25 0 1 0 550101182 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+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 102890 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 103890 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 104891 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 105891 123 0 0 25 0 1 0 550101182 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+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 106891 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223584 134614340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 107891 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 108891 123 0 0 25 0 1 0 550101182 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+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 109891 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 110892 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 111892 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13904
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 112892 123 0 0 25 0 1 0 550101182 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+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13906
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 113892 123 0 0 25 0 1 0 550101182 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+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13906
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 114893 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13906
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 115893 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13906
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 116893 123 0 0 25 0 1 0 550101182 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+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13906
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 117893 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223584 134603552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13906
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 118894 123 0 0 25 0 1 0 550101182 198221824 47009 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48394 47009 603 41 0 48353 0
vsize: 193576
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 13906
Raw data (stat): 13898 (minisat+) R 13897 22929 22928 0 -1 0 51469 0 0 0 119894 123 0 0 25 0 1 0 550101182 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.94 1/55 13906
Raw data (stat): 13898 (minisat+) Z 13897 22929 22928 0 -1 12 51470 0 0 0 119894 132 0 0 25 0 1 0 550101182 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.15
CPU time (s): 1200.27
CPU user time (s): 1198.94
CPU system time (s): 1.3208
CPU usage (%): 100.01
Max. virtual memory (Kb): 193576
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####