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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-5.opb
MD5SUM	00a81d808a7a59d6e11f17e19e68d826
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
Optimality of the best value was proved	NO
Number of terms in the objective function	450
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04884
Number of variables	450
Total number of constraints	17794
Number of constraints which are clauses	17794
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5611

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-14 00:50:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4078 boxname=wulflinc9 idbench=318 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00a81d808a7a59d6e11f17e19e68d826  /oldhome/oroussel/tmp/wulflinc9/normalized-frb30-15-5.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc9/normalized-frb30-15-5.opb /oldhome/oroussel/tmp/wulflinc9/normalized-frb30-15-5.opb
IDLAUNCH: 4078
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        896788 kB
Buffers:         35828 kB
Cached:          81792 kB
SwapCached:        564 kB
Active:          53456 kB
Inactive:        67572 kB
HighTotal:      131008 kB
HighFree:        45332 kB
LowTotal:       903652 kB
LowFree:        851456 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11272 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:10:21 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 4078 7 1200.15 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17794 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   17794    35588 |    5338       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   17794    35588 |    7117       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.610907 s)
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16912     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   34807    75603 |   10442       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11709          
c   -- var.elim.:  2000/11709          
c   -- var.elim.:  3000/11709          
c   -- var.elim.:  4000/11709          
c   -- var.elim.:  5000/11709          
c   -- var.elim.:  6000/11709          
c   -- var.elim.:  7000/11709          
c   -- var.elim.:  8000/11709          
c   -- var.elim.:  9000/11709          
c   -- var.elim.:  10000/11709          
c   -- var.elim.:  11000/11709          
c   -- var.elim.:  11709/11709          
c   -- var.elim.:  1000/5970          
c   -- var.elim.:  2000/5970          
c   -- var.elim.:  3000/5970          
c   -- var.elim.:  4000/5970          
c   -- var.elim.:  5000/5970          
c   -- var.elim.:  5970/5970          
c   -- var.elim.:  118/118          
c   -- subsuming                       
c   -- var.elim.:  1000/2296          
c   -- var.elim.:  2000/2296          
c   -- var.elim.:  2296/2296          
c   -- var.elim.:  212/212          
c |         0 |   22812    70611 |      --       0       --      -- |     --   | -11990/-4977
c |         0 |   22812    70611 |    9124       0        0     nan |  0.000 % |
c |       100 |   22812    70611 |   10037     100    12214   122.1 | 52.004 % |
c |       251 |   22812    70611 |   11041     251    27947   111.3 | 52.003 % |
c |       476 |   22812    70611 |   12145     476    62672   131.7 | 52.003 % |
c |       813 |   22812    70611 |   13359     813   118547   145.8 | 52.003 % |
c ==============================================================================
c (current CPU-time: 11.9572 s)
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       942 |   26027    79209 |    7808     942   136759   145.2 | 52.003 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5250          
c   -- var.elim.:  2000/5250          
c   -- var.elim.:  3000/5250          
c   -- var.elim.:  4000/5250          
c   -- var.elim.:  5000/5250          
c   -- var.elim.:  5250/5250          
c   -- var.elim.:  1000/2169          
c   -- var.elim.:  2000/2169          
c   -- var.elim.:  2169/2169          
c   -- var.elim.:  24/24          
c |       942 |   22919    75650 |      --     942       --      -- |     --   | -3099/-3540
c |       942 |   22919    75650 |    9167     942   136759   145.2 | 52.003 % |
c |      1042 |   22919    75650 |   10084    1042   145431   139.6 | 61.380 % |
c |      1192 |   22919    75650 |   11092    1192   161580   135.6 | 61.380 % |
c |      1418 |   22890    75439 |   12186    1413   181535   128.5 | 61.554 % |
c |      1755 |   22874    75299 |   13395    1745   235630   135.0 | 61.661 % |
c |      2261 |   22852    75084 |   14721    2249   308454   137.2 | 61.808 % |
c |      3020 |   22632    73150 |   16037    2972   382157   128.6 | 63.062 % |
c |      4159 |   22377    70989 |   17442    4070   539962   132.7 | 64.758 % |
c ==============================================================================
c (current CPU-time: 19.2501 s)
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5073 |   23165    72707 |    6949    4966   699418   140.8 | 64.758 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3402          
c   -- var.elim.:  2000/3402          
c   -- var.elim.:  3000/3402          
c   -- var.elim.:  3402/3402          
c   -- var.elim.:  850/850          
c |      5073 |   22307    71028 |      --    4966       --      -- |     --   | -858/-1678
c |      5073 |   22307    71028 |    8922    4875   669556   137.3 | 64.758 % |
c |      5173 |   22283    70846 |    9804    4973   679661   136.7 | 65.887 % |
c |      5323 |   22259    70668 |   10773    5105   695330   136.2 | 66.032 % |
c |      5548 |   22257    70649 |   11849    5325   729919   137.1 | 66.046 % |
c |      5885 |   22257    70649 |   13034    5662   781946   138.1 | 66.045 % |
c |      6392 |   22237    70467 |   14325    6163   887455   144.0 | 66.164 % |
c |      7151 |   22215    70271 |   15742    6917  1021340   147.7 | 66.310 % |
c |      8290 |   22139    69599 |   17257    8042  1264542   157.2 | 66.813 % |
c |      9999 |   22028    68682 |   18887    9720  1574147   161.9 | 67.526 % |
c |     12561 |   21881    67463 |   20637   12258  2006746   163.7 | 68.480 % |
c |     16406 |   21683    65803 |   22496   16007  2793622   174.5 | 69.749 % |
c |     22172 |   21324    62940 |   24335   21635  3922197   181.3 | 71.998 % |
c |     30821 |   21196    61842 |   26608   30173  5785378   191.7 | 72.805 % |
c ==============================================================================
c (current CPU-time: 79.136 s)
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     32377 |   21615    62208 |    6484   31685  6164063   194.5 | 72.805 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2546          
c   -- var.elim.:  2000/2546          
c   -- var.elim.:  2546/2546          
c   -- var.elim.:  1000/1096          
c   -- var.elim.:  1096/1096          
c |     32377 |   21010    59483 |      --   31685       --      -- |     --   | -584/-1213
c |     32377 |   21010    59483 |    8404   31685  6164063   194.5 | 72.805 % |
c |     32477 |   21010    59483 |    9244   13195  1644600   124.6 | 74.345 % |
c |     32627 |   21010    59483 |   10168   13345  1672956   125.4 | 74.345 % |
c |     32852 |   21010    59483 |   11185   13570  1716268   126.5 | 74.345 % |
c |     33192 |   21010    59483 |   12304   13910  1788518   128.6 | 74.345 % |
c |     33699 |   21010    59483 |   13534   14417  1870358   129.7 | 74.345 % |
c |     34458 |   21010    59483 |   14888   15176  2018343   133.0 | 74.345 % |
c |     35598 |   20905    58692 |   16295   16310  2208651   135.4 | 74.961 % |
c |     37306 |   20841    58203 |   17869   18000  2554774   141.9 | 75.368 % |
c |     39868 |   20731    57381 |   19553   20517  3053577   148.8 | 76.062 % |
c |     43712 |   20705    57201 |   21481   24344  3775638   155.1 | 76.233 % |
c |     49479 |   20637    56729 |   23551   18125  2659772   146.7 | 76.652 % |
c |     58130 |   20124    52973 |   25263   26648  4192767   157.3 | 79.772 % |
c ==============================================================================
c (current CPU-time: 139.829 s)
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     61031 |   21305    55342 |    6391   29536  4717318   159.7 | 79.772 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2746          
c   -- var.elim.:  2000/2746          
c   -- var.elim.:  2746/2746          
c   -- var.elim.:  766/766          
c   -- var.elim.:  24/24          
c |     61031 |   20025    52890 |      --   29536       --      -- |     --   | -1270/-2431
c |     61031 |   20025    52890 |    8010   29477  4716976   160.0 | 79.772 % |
c |     61131 |   20025    52890 |    8811   10838  1280415   118.1 | 82.410 % |
c |     61281 |   20025    52890 |    9692   10988  1306172   118.9 | 82.410 % |
c |     61507 |   20025    52890 |   10661   11214  1335168   119.1 | 82.410 % |
c |     61845 |   20025    52890 |   11727   11552  1382940   119.7 | 82.410 % |
c |     62352 |   20025    52890 |   12900   12059  1459723   121.0 | 82.410 % |
c |     63111 |   20025    52890 |   14190   12818  1566657   122.2 | 82.410 % |
c |     64250 |   20025    52890 |   15609   13957  1777112   127.3 | 82.410 % |
c |     65958 |   20025    52890 |   17170   15665  2059915   131.5 | 82.410 % |
c |     68520 |   20010    52767 |   18873   18226  2460731   135.0 | 82.493 % |
c |     72364 |   19990    52588 |   20739   22048  3118372   141.4 | 82.599 % |
c |     78130 |   19964    52380 |   22783   27748  4138095   149.1 | 82.753 % |
c |     86779 |   19948    52236 |   25042   21620  2998630   138.7 | 82.847 % |
c |     99753 |   19865    51570 |   27431   17905  2365048   132.1 | 83.296 % |
c ==============================================================================
c (current CPU-time: 233.748 s)
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    108411 |   19883    51620 |    5964   26560  3944426   148.5 | 83.296 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1003          
c   -- var.elim.:  1003/1003          
c   -- var.elim.:  192/192          
c |    108411 |   19845    51387 |      --   26560       --      -- |     --   | -23/-75
c |    108411 |   19845    51387 |    7938   14968   903728    60.4 | 83.296 % |
c |    108511 |   19845    51387 |    8731   15068   917831    60.9 | 83.438 % |
c |    108661 |   19845    51387 |    9604   15218   938847    61.7 | 83.438 % |
c |    108886 |   19845    51387 |   10565   15443   970618    62.9 | 83.438 % |
c |    109224 |   19845    51387 |   11622   15781  1027459    65.1 | 83.438 % |
c |    109730 |   19845    51387 |   12784   16287  1108636    68.1 | 83.438 % |
c |    110489 |   19817    51145 |   14042   17040  1226717    72.0 | 83.604 % |
c |    111628 |   19817    51145 |   15447   18179  1397999    76.9 | 83.604 % |
c |    113337 |   19817    51145 |   16991   19888  1671431    84.0 | 83.603 % |
c |    115899 |   19793    50933 |   18668   22434  2124508    94.7 | 83.722 % |
c |    119745 |   19775    50798 |   20516   26275  2745356   104.5 | 83.828 % |
c |    125511 |   19739    50507 |   22527   20633  2486612   120.5 | 84.029 % |
c |    134160 |   19651    49870 |   24669   29273  3768599   128.7 | 84.526 % |
c |    147134 |   19553    49122 |   27000   26253  3256167   124.0 | 85.081 % |
c |    166595 |   19464    48512 |   29565   26650  3182250   119.4 | 85.578 % |
c |    195787 |   19346    47731 |   32325   34583  4210357   121.7 | 86.240 % |
c |    239576 |   19301    47432 |   35475   32386  3417296   105.5 | 86.488 % |
c ==============================================================================
c (current CPU-time: 562.297 s)
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    261588 |   19258    46708 |    5777   28384  2898760   102.1 | 86.488 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1144          
c   -- var.elim.:  1144/1144          
c   -- var.elim.:  270/270          
c |    261588 |   19193    46631 |      --   28384       --      -- |     --   | -65/-76
c |    261588 |   19193    46631 |    7677   16328  1083950    66.4 | 86.488 % |
c |    261688 |   19193    46631 |    8444   10306   679880    66.0 | 87.348 % |
c |    261838 |   19193    46631 |    9289   10456   693036    66.3 | 87.349 % |
c |    262063 |   19193    46631 |   10218   10681   717611    67.2 | 87.349 % |
c |    262400 |   19193    46631 |   11240   11018   755190    68.5 | 87.349 % |
c |    262907 |   19170    46491 |   12349   11523   809124    70.2 | 87.455 % |
c |    263667 |   19161    46449 |   13577   12282   885908    72.1 | 87.490 % |
c |    264807 |   19161    46449 |   14935   13422  1012562    75.4 | 87.490 % |
c |    266515 |   19139    46307 |   16410   15116  1153906    76.3 | 87.607 % |
c |    269077 |   19139    46307 |   18051   17678  1410326    79.8 | 87.608 % |
c |    272921 |   19119    46141 |   19835   21518  1795886    83.5 | 87.725 % |
c |    278688 |   19119    46141 |   21819   27285  2396733    87.8 | 87.725 % |
c |    287337 |   19099    45987 |   23976   22141  1764666    79.7 | 87.819 % |
c |    300312 |   19073    45810 |   26338   19225  1443089    75.1 | 87.973 % |
c |    319776 |   19009    45378 |   28874   20759  1506416    72.6 | 88.314 % |
c ==============================================================================
c (current CPU-time: 685.745 s)
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:13768     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    335448 |   31121    73750 |    9336   32019  2470035    77.1 | 88.314 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9224          
c   -- var.elim.:  2000/9224          
c   -- var.elim.:  3000/9224          
c   -- var.elim.:  4000/9224          
c   -- var.elim.:  5000/9224          
c   -- var.elim.:  6000/9224          
c   -- var.elim.:  7000/9224          
c   -- var.elim.:  8000/9224          
c   -- var.elim.:  9000/9224          
c   -- var.elim.:  9224/9224          
c   -- var.elim.:  1000/4419          
c   -- var.elim.:  2000/4419          
c   -- var.elim.:  3000/4419          
c   -- var.elim.:  4000/4419          
c   -- var.elim.:  4419/4419          
c   -- var.elim.:  1000/1268          
c   -- var.elim.:  1268/1268          
c   -- var.elim.:  70/70          
c   -- subsuming                       
c   -- var.elim.:  1000/1805          
c   -- var.elim.:  1805/1805          
c   -- var.elim.:  180/180          
c |    335448 |   22432    69873 |      --   32019       --      -- |     --   | -8653/-3800
c |    335448 |   22432    69873 |    8972   23087  1488312    64.5 | 88.314 % |
c |    335548 |   22432    69873 |    9870   11983   695880    58.1 | 79.843 % |
c |    335700 |   22432    69873 |   10857   12135   703741    58.0 | 79.843 % |
c |    335925 |   22432    69873 |   11942   12360   725841    58.7 | 79.842 % |
c |    336262 |   22432    69873 |   13137   12697   756482    59.6 | 79.843 % |
c |    336769 |   22432    69873 |   14450   13204   809133    61.3 | 79.842 % |
c |    337530 |   22432    69873 |   15895   13965   882660    63.2 | 79.843 % |
c |    338670 |   22432    69873 |   17485   15105   984165    65.2 | 79.843 % |
c |    340378 |   22432    69873 |   19233   16813  1129298    67.2 | 79.843 % |
c |    342942 |   22407    69714 |   21133   19376  1354449    69.9 | 79.918 % |
c |    346786 |   22407    69714 |   23247   23220  1679739    72.3 | 79.918 % |
c |    352552 |   22387    69585 |   25549   28979  2163505    74.7 | 79.979 % |
c |    361202 |   22366    69477 |   28077   17746  1155724    65.1 | 80.047 % |
c |    374178 |   22275    69281 |   30759   28546  1967765    68.9 | 80.055 % |
c |    393640 |   22186    69087 |   33700   14894   816051    54.8 | 80.062 % |
c |    422832 |   22080    68801 |   36893#### 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.81 0.88 0.88 2/54 2451
Raw data (stat): 2451 (runsolver) R 2450 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422182261 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.84 0.88 0.88 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 2488 0 0 0 988 10 0 0 25 0 1 0 422182261 12300288 2380 4294967295 134512640 134672761 3221224560 3221222408 134566735 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3003 2380 603 41 0 2962 0
vsize: 12012
[startup+20.0016 s]
Raw data (loadavg): 0.87 0.89 0.88 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 4048 0 0 0 1978 20 0 0 25 0 1 0 422182261 16883712 3379 4294967295 134512640 134672761 3221224560 3221223104 134621044 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4122 3379 603 41 0 4081 0
vsize: 16488
[startup+30.0014 s]
Raw data (loadavg): 0.89 0.89 0.88 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 5122 0 0 0 2975 23 0 0 25 0 1 0 422182261 21114880 4419 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5155 4419 603 41 0 5114 0
vsize: 20620
[startup+40.0022 s]
Raw data (loadavg): 0.90 0.89 0.89 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 6223 0 0 0 3972 26 0 0 25 0 1 0 422182261 25669632 5520 4294967295 134512640 134672761 3221224560 3221223744 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6267 5520 603 41 0 6226 0
vsize: 25068
[startup+50.0029 s]
Raw data (loadavg): 0.92 0.89 0.89 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 7136 0 0 0 4969 29 0 0 25 0 1 0 422182261 29356032 6433 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7167 6433 603 41 0 7126 0
vsize: 28668
[startup+60.0037 s]
Raw data (loadavg): 0.93 0.90 0.89 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 7951 0 0 0 5966 32 0 0 25 0 1 0 422182261 32649216 7248 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7971 7248 603 41 0 7930 0
vsize: 31884
[startup+70.0049 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 8959 0 0 0 6962 36 0 0 25 0 1 0 422182261 36724736 8256 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8966 8256 603 41 0 8925 0
vsize: 35864
[startup+80.0053 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10434 0 0 0 7957 41 0 0 25 0 1 0 422182261 40484864 9180 4294967295 134512640 134672761 3221224560 3221223052 134642749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9884 9180 603 41 0 9843 0
vsize: 39536
[startup+90.006 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10435 0 0 0 8957 42 0 0 25 0 1 0 422182261 40312832 9147 4294967295 134512640 134672761 3221224560 3221223600 134614254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9842 9147 603 41 0 9801 0
vsize: 39368
[startup+100.006 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10435 0 0 0 9956 42 0 0 25 0 1 0 422182261 40312832 9147 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9842 9147 603 41 0 9801 0
vsize: 39368
[startup+110.007 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10435 0 0 0 10956 42 0 0 25 0 1 0 422182261 40312832 9147 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9842 9147 603 41 0 9801 0
vsize: 39368
[startup+120.006 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10435 0 0 0 11956 42 0 0 25 0 1 0 422182261 40312832 9147 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9842 9147 603 41 0 9801 0
vsize: 39368
[startup+130.007 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10435 0 0 0 12955 43 0 0 25 0 1 0 422182261 40312832 9147 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9842 9147 603 41 0 9801 0
vsize: 39368
[startup+140.007 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10435 0 0 0 13955 43 0 0 25 0 1 0 422182261 40312832 9147 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9842 9147 603 41 0 9801 0
vsize: 39368
[startup+150.008 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10952 0 0 0 14951 48 0 0 25 0 1 0 422182261 40067072 9113 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9113 603 41 0 9741 0
vsize: 39128
[startup+160.008 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10952 0 0 0 15951 48 0 0 25 0 1 0 422182261 40067072 9113 4294967295 134512640 134672761 3221224560 3221223760 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9113 603 41 0 9741 0
vsize: 39128
[startup+170.008 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10952 0 0 0 16951 48 0 0 25 0 1 0 422182261 40067072 9113 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9113 603 41 0 9741 0
vsize: 39128
[startup+180.008 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10952 0 0 0 17950 48 0 0 25 0 1 0 422182261 40067072 9113 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9113 603 41 0 9741 0
vsize: 39128
[startup+190.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10952 0 0 0 18950 48 0 0 25 0 1 0 422182261 40067072 9113 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9113 603 41 0 9741 0
vsize: 39128
[startup+200.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10952 0 0 0 19950 49 0 0 25 0 1 0 422182261 40067072 9113 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9113 603 41 0 9741 0
vsize: 39128
[startup+210.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10953 0 0 0 20949 49 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+220.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10953 0 0 0 21949 49 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223600 134613756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+230.01 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 10953 0 0 0 22949 50 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+240.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11477 0 0 0 23944 54 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+250.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11477 0 0 0 24944 54 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+260.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11477 0 0 0 25944 55 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223656 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+270.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11477 0 0 0 26943 55 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+280.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11477 0 0 0 27943 55 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+290.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11477 0 0 0 28944 55 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+300.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11477 0 0 0 29944 55 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223744 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+310.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11477 0 0 0 30944 55 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+320.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11477 0 0 0 31944 55 0 0 25 0 1 0 422182261 40067072 9114 4294967295 134512640 134672761 3221224560 3221223744 134615560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9782 9114 603 41 0 9741 0
vsize: 39128
[startup+330.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11511 0 0 0 32944 55 0 0 25 0 1 0 422182261 40329216 9148 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9148 603 41 0 9805 0
vsize: 39384
[startup+340.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11547 0 0 0 33944 55 0 0 25 0 1 0 422182261 40329216 9149 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9149 603 41 0 9805 0
vsize: 39384
[startup+350.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11547 0 0 0 34944 55 0 0 25 0 1 0 422182261 40329216 9149 4294967295 134512640 134672761 3221224560 3221223600 134614171 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9149 603 41 0 9805 0
vsize: 39384
[startup+360.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11547 0 0 0 35945 55 0 0 25 0 1 0 422182261 40329216 9149 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9149 603 41 0 9805 0
vsize: 39384
[startup+370.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11547 0 0 0 36945 55 0 0 25 0 1 0 422182261 40329216 9149 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9149 603 41 0 9805 0
vsize: 39384
[startup+380.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11586 0 0 0 37945 55 0 0 25 0 1 0 422182261 40329216 9151 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9151 603 41 0 9805 0
vsize: 39384
[startup+390.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11586 0 0 0 38945 55 0 0 25 0 1 0 422182261 40329216 9151 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9151 603 41 0 9805 0
vsize: 39384
[startup+400.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11586 0 0 0 39945 55 0 0 25 0 1 0 422182261 40329216 9151 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9151 603 41 0 9805 0
vsize: 39384
[startup+410.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11586 0 0 0 40945 55 0 0 25 0 1 0 422182261 40329216 9151 4294967295 134512640 134672761 3221224560 3221223600 134612587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9151 603 41 0 9805 0
vsize: 39384
[startup+420.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11586 0 0 0 41946 55 0 0 25 0 1 0 422182261 40329216 9151 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9151 603 41 0 9805 0
vsize: 39384
[startup+430.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11588 0 0 0 42946 55 0 0 25 0 1 0 422182261 40329216 9153 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9153 603 41 0 9805 0
vsize: 39384
[startup+440.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11629 0 0 0 43946 55 0 0 25 0 1 0 422182261 40329216 9154 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9154 603 41 0 9805 0
vsize: 39384
[startup+450.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11629 0 0 0 44946 55 0 0 25 0 1 0 422182261 40329216 9154 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9154 603 41 0 9805 0
vsize: 39384
[startup+460.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11629 0 0 0 45946 55 0 0 25 0 1 0 422182261 40329216 9154 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9154 603 41 0 9805 0
vsize: 39384
[startup+470.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11629 0 0 0 46946 55 0 0 25 0 1 0 422182261 40329216 9154 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9154 603 41 0 9805 0
vsize: 39384
[startup+480.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11629 0 0 0 47947 55 0 0 25 0 1 0 422182261 40329216 9154 4294967295 134512640 134672761 3221224560 3221223744 134615796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9154 603 41 0 9805 0
vsize: 39384
[startup+490.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11669 0 0 0 48947 55 0 0 25 0 1 0 422182261 40329216 9154 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9154 603 41 0 9805 0
vsize: 39384
[startup+500.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11669 0 0 0 49947 55 0 0 25 0 1 0 422182261 40329216 9154 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9154 603 41 0 9805 0
vsize: 39384
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11669 0 0 0 50947 55 0 0 25 0 1 0 422182261 40329216 9154 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9154 603 41 0 9805 0
vsize: 39384
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11669 0 0 0 51947 55 0 0 25 0 1 0 422182261 40329216 9154 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9154 603 41 0 9805 0
vsize: 39384
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11669 0 0 0 52947 55 0 0 25 0 1 0 422182261 40329216 9154 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9154 603 41 0 9805 0
vsize: 39384
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11671 0 0 0 53947 55 0 0 25 0 1 0 422182261 40329216 9156 4294967295 134512640 134672761 3221224560 3221223744 134615755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9156 603 41 0 9805 0
vsize: 39384
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11713 0 0 0 54948 55 0 0 25 0 1 0 422182261 40329216 9156 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9156 603 41 0 9805 0
vsize: 39384
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 11713 0 0 0 55948 55 0 0 25 0 1 0 422182261 40329216 9156 4294967295 134512640 134672761 3221224560 3221223552 134565036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9156 603 41 0 9805 0
vsize: 39384
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12139 0 0 0 56944 59 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223600 134603510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2451
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12139 0 0 0 57945 59 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 2494
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12139 0 0 0 58932 71 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2504
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12139 0 0 0 59932 71 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2504
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12139 0 0 0 60932 71 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2504
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12139 0 0 0 61932 71 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2504
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12139 0 0 0 62933 71 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223744 134615996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2504
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12139 0 0 0 63933 71 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2504
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12139 0 0 0 64933 71 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12173 0 0 0 65933 71 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12173 0 0 0 66933 71 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223600 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12173 0 0 0 67933 71 0 0 25 0 1 0 422182261 40329216 9158 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9846 9158 603 41 0 9805 0
vsize: 39384
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12821 0 0 0 68927 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221222816 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12821 0 0 0 69926 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12821 0 0 0 70926 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223600 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+720.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12821 0 0 0 71927 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12821 0 0 0 72927 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12858 0 0 0 73927 78 0 0 25 0 1 0 422182261 40931328 9415 4294967295 134512640 134672761 3221224560 3221223184 134645493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9993 9415 603 41 0 9952 0
vsize: 39972
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12858 0 0 0 74927 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12858 0 0 0 75927 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12858 0 0 0 76928 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12858 0 0 0 77928 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+790.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12858 0 0 0 78928 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12900 0 0 0 79928 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+810.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12900 0 0 0 80928 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12900 0 0 0 81928 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12900 0 0 0 82928 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12900 0 0 0 83929 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223372 1075349950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12900 0 0 0 84929 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223704 134616320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12900 0 0 0 85929 78 0 0 25 0 1 0 422182261 40669184 9378 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9378 603 41 0 9888 0
vsize: 39716
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12902 0 0 0 86929 78 0 0 25 0 1 0 422182261 40669184 9380 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9929 9380 603 41 0 9888 0
vsize: 39716
[startup+880.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12952 0 0 0 87929 78 0 0 25 0 1 0 422182261 40931328 9430 4294967295 134512640 134672761 3221224560 3221223540 1075351222 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9993 9430 603 41 0 9952 0
vsize: 39972
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12952 0 0 0 88929 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+900.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2506
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12952 0 0 0 89929 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12952 0 0 0 90929 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+920.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12952 0 0 0 91929 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223800 134564646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12952 0 0 0 92929 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223600 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12952 0 0 0 93929 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12952 0 0 0 94930 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+960.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12952 0 0 0 95930 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+970.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12999 0 0 0 96930 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223600 134603565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12999 0 0 0 97930 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12999 0 0 0 98930 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12999 0 0 0 99930 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12999 0 0 0 100930 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12999 0 0 0 101931 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12999 0 0 0 102931 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12999 0 0 0 103931 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12999 0 0 0 104931 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 12999 0 0 0 105931 78 0 0 25 0 1 0 422182261 40669184 9383 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9383 603 41 0 9888 0
vsize: 39716
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13002 0 0 0 106932 78 0 0 25 0 1 0 422182261 40669184 9386 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9386 603 41 0 9888 0
vsize: 39716
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13054 0 0 0 107932 78 0 0 25 0 1 0 422182261 40669184 9387 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9387 603 41 0 9888 0
vsize: 39716
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13054 0 0 0 108932 78 0 0 25 0 1 0 422182261 40669184 9387 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9387 603 41 0 9888 0
vsize: 39716
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13054 0 0 0 109932 78 0 0 25 0 1 0 422182261 40669184 9387 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9387 603 41 0 9888 0
vsize: 39716
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13054 0 0 0 110932 78 0 0 25 0 1 0 422182261 40669184 9387 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9387 603 41 0 9888 0
vsize: 39716
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13054 0 0 0 111932 78 0 0 25 0 1 0 422182261 40669184 9387 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9387 603 41 0 9888 0
vsize: 39716
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13054 0 0 0 112932 78 0 0 25 0 1 0 422182261 40669184 9387 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9387 603 41 0 9888 0
vsize: 39716
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13054 0 0 0 113933 78 0 0 25 0 1 0 422182261 40669184 9387 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9387 603 41 0 9888 0
vsize: 39716
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13054 0 0 0 114933 78 0 0 25 0 1 0 422182261 40669184 9387 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9387 603 41 0 9888 0
vsize: 39716
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13054 0 0 0 115933 78 0 0 25 0 1 0 422182261 40669184 9387 4294967295 134512640 134672761 3221224560 3221223744 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9387 603 41 0 9888 0
vsize: 39716
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13054 0 0 0 116933 78 0 0 25 0 1 0 422182261 40669184 9387 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9387 603 41 0 9888 0
vsize: 39716
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13054 0 0 0 117933 78 0 0 25 0 1 0 422182261 40669184 9387 4294967295 134512640 134672761 3221224560 3221223744 134616014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9387 603 41 0 9888 0
vsize: 39716
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13109 0 0 0 118933 79 0 0 25 0 1 0 422182261 40931328 9442 4294967295 134512640 134672761 3221224560 3221222480 134645591 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9993 9442 603 41 0 9952 0
vsize: 39972
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2508
Raw data (stat): 2451 (minisat+) R 2450 30854 30853 0 -1 0 13109 0 0 0 119933 79 0 0 25 0 1 0 422182261 40669184 9389 4294967295 134512640 134672761 3221224560 3221223760 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9929 9389 603 41 0 9888 0
vsize: 39716
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 2508
Raw data (stat): 2451 (minisat+) Z 2450 30854 30853 0 -1 12 13110 0 0 0 119933 81 0 0 25 0 1 0 422182261 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.04
CPU time (s): 1200.15
CPU user time (s): 1199.34
CPU system time (s): 0.814876
CPU usage (%): 100.01
Max. virtual memory (Kb): 39972
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####