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/frb40-19-opb/normalized-frb40-19-1.opb
MD5SUM	94f501465233508e2f652cf118ddaf2d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-31
Optimality of the best value was proved	NO
Number of terms in the objective function	760
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	760
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	760
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.06
Number of variables	760
Total number of constraints	41314
Number of constraints which are clauses	41314
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 5616

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-14 00:57:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4084 boxname=wulflinc4 idbench=324 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  94f501465233508e2f652cf118ddaf2d  /oldhome/oroussel/tmp/wulflinc4/normalized-frb40-19-1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc4/normalized-frb40-19-1.opb /oldhome/oroussel/tmp/wulflinc4/normalized-frb40-19-1.opb
IDLAUNCH: 4084
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        899152 kB
Buffers:         35200 kB
Cached:          80468 kB
SwapCached:          0 kB
Active:          55440 kB
Inactive:        63104 kB
HighTotal:      131008 kB
HighFree:        46704 kB
LowTotal:       903652 kB
LowFree:        852448 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11424 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:17:48 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 4084 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41314 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 |   41314    82628 |   12394       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   41314    82628 |   16525       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.73274 s)
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:35010     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   77463   167541 |   23238       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24733          
c   -- var.elim.:  2000/24733          
c   -- var.elim.:  3000/24733          
c   -- var.elim.:  4000/24733          
c   -- var.elim.:  5000/24733          
c   -- var.elim.:  6000/24733          
c   -- var.elim.:  7000/24733          
c   -- var.elim.:  8000/24733          
c   -- var.elim.:  9000/24733          
c   -- var.elim.:  10000/24733          
c   -- var.elim.:  11000/24733          
c   -- var.elim.:  12000/24733          
c   -- var.elim.:  13000/24733          
c   -- var.elim.:  14000/24733          
c   -- var.elim.:  15000/24733          
c   -- var.elim.:  16000/24733          
c   -- var.elim.:  17000/24733          
c   -- var.elim.:  18000/24733          
c   -- var.elim.:  19000/24733          
c   -- var.elim.:  20000/24733          
c   -- var.elim.:  21000/24733          
c   -- var.elim.:  22000/24733          
c   -- var.elim.:  23000/24733          
c   -- var.elim.:  24000/24733          
c   -- var.elim.:  24733/24733          
c   -- var.elim.:  1000/12568          
c   -- var.elim.:  2000/12568          
c   -- var.elim.:  3000/12568          
c   -- var.elim.:  4000/12568          
c   -- var.elim.:  5000/12568          
c   -- var.elim.:  6000/12568          
c   -- var.elim.:  7000/12568          
c   -- var.elim.:  8000/12568          
c   -- var.elim.:  9000/12568          
c   -- var.elim.:  10000/12568          
c   -- var.elim.:  11000/12568          
c   -- var.elim.:  12000/12568          
c   -- var.elim.:  12568/12568          
c   -- var.elim.:  1000/2557          
c   -- var.elim.:  2000/2557          
c   -- var.elim.:  2557/2557          
c   -- subsuming                       
c   -- var.elim.:  1000/4972          
c   -- var.elim.:  2000/4972          
c   -- var.elim.:  3000/4972          
c   -- var.elim.:  4000/4972          
c   -- var.elim.:  4972/4972          
c   -- var.elim.:  288/288          
c |         0 |   51938   166290 |      --       0       --      -- |     --   | -25520/-1236
c |         0 |   51938   166290 |   20775       0        0     nan |  0.000 % |
c |       100 |   51938   166290 |   22852     100     8240    82.4 | 52.870 % |
c |       250 |   51938   166290 |   25137     250    25763   103.1 | 52.870 % |
c |       475 |   51938   166290 |   27651     475    68718   144.7 | 52.870 % |
c |       813 |   51938   166290 |   30416     813   108643   133.6 | 52.870 % |
c |      1319 |   51938   166290 |   33458    1319   187738   142.3 | 52.870 % |
c |      2078 |   51889   165938 |   36769    2077   296998   143.0 | 53.038 % |
c |      3217 |   51743   164858 |   40332    3199   459157   143.5 | 53.518 % |
c |      4925 |   51573   163423 |   44220    4889   795220   162.7 | 54.165 % |
c |      7489 |   51316   161245 |   48400    7392  1297101   175.5 | 55.140 % |
c ==============================================================================
c (current CPU-time: 70.8212 s)
c ==============================================================================
c [1mFound solution: -32[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 |      9322 |   56221   173965 |   16866    9204  1691311   183.8 | 55.140 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10203          
c   -- var.elim.:  2000/10203          
c   -- var.elim.:  3000/10203          
c   -- var.elim.:  4000/10203          
c   -- var.elim.:  5000/10203          
c   -- var.elim.:  6000/10203          
c   -- var.elim.:  7000/10203          
c   -- var.elim.:  8000/10203          
c   -- var.elim.:  9000/10203          
c   -- var.elim.:  10000/10203          
c   -- var.elim.:  10203/10203          
c   -- var.elim.:  1000/3571          
c   -- var.elim.:  2000/3571          
c   -- var.elim.:  3000/3571          
c   -- var.elim.:  3571/3571          
c   -- var.elim.:  204/204          
c   -- subsuming                       
c   -- var.elim.:  1000/3526          
c   -- var.elim.:  2000/3526          
c   -- var.elim.:  3000/3526          
c   -- var.elim.:  3526/3526          
c   -- var.elim.:  232/232          
c |      9322 |   51316   168102 |      --    9204       --      -- |     --   | -4887/-5367
c |      9322 |   51316   168102 |   20526    9204  1691311   183.8 | 55.140 % |
c |      9423 |   51316   168102 |   22579    9305  1705142   183.3 | 65.234 % |
c |      9573 |   51316   168102 |   24836    9455  1722259   182.2 | 65.234 % |
c |      9799 |   51143   166651 |   27228    8773  1203342   137.2 | 65.687 % |
c |     10136 |   51121   166429 |   29938    9103  1272875   139.8 | 65.756 % |
c |     10642 |   51083   166110 |   32907    9608  1424128   148.2 | 65.874 % |
c |     11401 |   50997   165297 |   36137   10355  1579311   152.5 | 66.141 % |
c |     12540 |   50973   165096 |   39732   11477  1846174   160.9 | 66.215 % |
c |     14248 |   50717   162720 |   43486   13134  2251404   171.4 | 67.011 % |
c |     16811 |   50391   159692 |   47527   15634  2958904   189.3 | 68.023 % |
c |     20656 |   49979   155941 |   51853   19414  3974422   204.7 | 69.291 % |
c |     26422 |   49496   151643 |   56487   25020  5399204   215.8 | 70.757 % |
c |     35071 |   48687   144294 |   61120   33505  7625062   227.6 | 73.217 % |
c |     48046 |   48330   141141 |   66739   46268 11786560   254.7 | 74.311 % |
c ==============================================================================
c (current CPU-time: 266.583 s)
c ==============================================================================
c [1mFound solution: -33[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 |     54791 |   50989   147624 |   15296   52971 13921936   262.8 | 74.311 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6790          
c   -- var.elim.:  2000/6790          
c   -- var.elim.:  3000/6790          
c   -- var.elim.:  4000/6790          
c   -- var.elim.:  5000/6790          
c   -- var.elim.:  6000/6790          
c   -- var.elim.:  6790/6790          
c   -- var.elim.:  1000/2245          
c   -- var.elim.:  2000/2245          
c   -- var.elim.:  2245/2245          
c   -- subsuming                       
c   -- var.elim.:  1000/1713          
c   -- var.elim.:  1713/1713          
c   -- var.elim.:  15/15          
c |     54791 |   48231   142129 |      --   52971       --      -- |     --   | -2757/-5492
c |     54791 |   48231   142129 |   19292   51299 13159489   256.5 | 74.311 % |
c |     54892 |   48231   142129 |   21221   19286  3873776   200.9 | 75.968 % |
c |     55043 |   48231   142129 |   23343   19437  3902573   200.8 | 75.968 % |
c |     55268 |   48231   142129 |   25678   19662  3949465   200.9 | 75.968 % |
c |     55608 |   48231   142129 |   28246   20002  4056874   202.8 | 75.968 % |
c |     56115 |   48193   141770 |   31046   20504  4140158   201.9 | 76.069 % |
c |     56874 |   48163   141498 |   34129   21252  4330596   203.8 | 76.158 % |
c |     58013 |   48127   141149 |   37514   22379  4610141   206.0 | 76.259 % |
c |     59721 |   48127   141149 |   41265   24087  5100704   211.8 | 76.258 % |
c |     62283 |   48125   141130 |   45390   26624  5769960   216.7 | 76.265 % |
c |     66127 |   47877   138794 |   49672   30382  6729396   221.5 | 76.981 % |
c |     71893 |   47855   138605 |   54614   36142  8293067   229.5 | 77.040 % |
c ==============================================================================
c (current CPU-time: 345.154 s)
c ==============================================================================
c [1mFound solution: -34[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 |     74604 |   48587   140586 |   14576   38849  9084033   233.8 | 77.040 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4376          
c   -- var.elim.:  2000/4376          
c   -- var.elim.:  3000/4376          
c   -- var.elim.:  4000/4376          
c   -- var.elim.:  4376/4376          
c   -- var.elim.:  941/941          
c |     74604 |   47812   137281 |      --   38849       --      -- |     --   | -762/-1295
c |     74604 |   47812   137281 |   19124   34859  6634049   190.3 | 77.040 % |
c |     74705 |   47812   137281 |   21037   17458  2069626   118.5 | 77.191 % |
c |     74855 |   47812   137281 |   23141   17608  2105056   119.6 | 77.191 % |
c |     75082 |   47812   137281 |   25455   17835  2161013   121.2 | 77.191 % |
c |     75420 |   47810   137262 |   27999   18170  2233084   122.9 | 77.197 % |
c |     75927 |   47778   136957 |   30778   18671  2359023   126.3 | 77.286 % |
c |     76686 |   47746   136674 |   33833   19426  2541029   130.8 | 77.374 % |
c |     77825 |   47726   136470 |   37201   20560  2823072   137.3 | 77.434 % |
c |     79535 |   47704   136264 |   40903   22254  3274530   147.1 | 77.493 % |
c |     82097 |   47553   134805 |   44850   24776  3932462   158.7 | 77.925 % |
c |     85941 |   47529   134586 |   49311   28601  4999432   174.8 | 77.991 % |
c |     91707 |   47493   134268 |   54201   34364  6567459   191.1 | 78.097 % |
c |    100359 |   47466   134045 |   59587   43010  9176366   213.4 | 78.174 % |
c |    113334 |   47174   131361 |   65142   55929 12884046   230.4 | 78.980 % |
c |    132795 |   46813   128173 |   71108   75202 18567706   246.9 | 79.999 % |
c ==============================================================================
c (current CPU-time: 715.231 s)
c ==============================================================================
c [1mFound solution: -35[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 |    154104 |   49862   135762 |   14958   33294  6991871   210.0 | 79.999 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5757          
c   -- var.elim.:  2000/5757          
c   -- var.elim.:  3000/5757          
c   -- var.elim.:  4000/5757          
c   -- var.elim.:  5000/5757          
c   -- var.elim.:  5757/5757          
c   -- var.elim.:  1000/1911          
c   -- var.elim.:  1911/1911          
c |    154104 |   46808   130848 |      --   33294       --      -- |     --   | -3035/-4875
c |    154104 |   46808   130848 |   18723   33294  6991871   210.0 | 79.999 % |
c |    154204 |   46808   130848 |   20595   33394  7019432   210.2 | 81.854 % |
c |    154354 |   46808   130848 |   22655   33544  7050212   210.2 | 81.854 % |
c |    154580 |   46808   130848 |   24920   33770  7105503   210.4 | 81.854 % |
c |    154918 |   46517   128476 |   27242   34097  7168065   210.2 | 82.604 % |
c |    155424 |   46517   128476 |   29966   34603  7351763   212.5 | 82.605 % |
c |    156183 |   46517   128476 |   32963   35362  7584756   214.5 | 82.604 % |
c |    157322 |   46517   128476 |   36259   36501  7868632   215.6 | 82.605 % |
c |    159030 |   46429   127756 |   39809   38175  8276801   216.8 | 82.821 % |
c |    161593 |   46287   126537 |   43656   40729  8894577   218.4 | 83.193 % |
c |    165439 |   46209   125810 |   47941   44546 10048708   225.6 | 83.382 % |
c |    171206 |   46132   125184 |   52647   50284 11849918   235.7 | 83.571 % |
c |    179856 |   46091   124879 |   57861   58905 14300166   242.8 | 83.668 % |
c |    192831 |   46060   124635 |   63604   71867 18948899   263.7 | 83.749 % |
c |    212292 |   45813   122760 |   69589   32184  6990066   217.2 | 84.327 % |
c |    241484 |   45628   121163 |   76239   61322 15018757   244.9 | 84.802 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.95 2/54 10667
Raw data (stat): 10667 (runsolver) R 10666 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422223032 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.0012 s]
Raw data (loadavg): 0.93 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 4986 0 0 0 980 18 0 0 25 0 1 0 422223032 22548480 4696 4294967295 134512640 134672761 3221224560 3221223152 134607919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5505 4696 603 41 0 5464 0
vsize: 22020
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 5010 0 0 0 1980 18 0 0 25 0 1 0 422223032 22691840 4720 4294967295 134512640 134672761 3221224560 3221222992 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5540 4720 603 41 0 5499 0
vsize: 22160
[startup+30.0029 s]
Raw data (loadavg): 0.95 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 5031 0 0 0 2980 18 0 0 25 0 1 0 422223032 22855680 4741 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5580 4741 603 41 0 5539 0
vsize: 22320
[startup+40.0028 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 5037 0 0 0 3980 19 0 0 25 0 1 0 422223032 22855680 4747 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5580 4747 603 41 0 5539 0
vsize: 22320
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 5189 0 0 0 4979 19 0 0 25 0 1 0 422223032 23912448 4899 4294967295 134512640 134672761 3221224560 3221223104 134621071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5838 4899 603 41 0 5797 0
vsize: 23352
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 5578 0 0 0 5978 21 0 0 25 0 1 0 422223032 24420352 5136 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5962 5136 603 41 0 5921 0
vsize: 23848
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 6582 0 0 0 6976 23 0 0 25 0 1 0 422223032 28512256 6140 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6961 6140 603 41 0 6920 0
vsize: 27844
[startup+80.004 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 7804 0 0 0 7958 40 0 0 25 0 1 0 422223032 32694272 6742 4294967295 134512640 134672761 3221224560 3221223008 134643483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7982 6742 603 41 0 7941 0
vsize: 31928
[startup+90.0042 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 7956 0 0 0 8958 40 0 0 25 0 1 0 422223032 32694272 6742 4294967295 134512640 134672761 3221224560 3221223040 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7982 6742 603 41 0 7941 0
vsize: 31928
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 8141 0 0 0 9958 41 0 0 25 0 1 0 422223032 33472512 6927 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8172 6927 603 41 0 8131 0
vsize: 32688
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 8944 0 0 0 10954 44 0 0 25 0 1 0 422223032 36749312 7730 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8972 7730 603 41 0 8931 0
vsize: 35888
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 9956 0 0 0 11952 46 0 0 25 0 1 0 422223032 40976384 8742 4294967295 134512640 134672761 3221224560 3221223704 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10004 8742 603 41 0 9963 0
vsize: 40016
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10667
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 10577 0 0 0 12950 49 0 0 25 0 1 0 422223032 43454464 9363 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10609 9363 603 41 0 10568 0
vsize: 42436
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.95 3/56 10681
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 11235 0 0 0 13948 50 0 0 25 0 1 0 422223032 46198784 10021 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11279 10021 603 41 0 11238 0
vsize: 45116
[startup+150.008 s]
Raw data (loadavg): 1.06 1.00 0.95 2/54 10720
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 12053 0 0 0 14945 54 0 0 25 0 1 0 422223032 49463296 10839 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12076 10839 603 41 0 12035 0
vsize: 48304
[startup+160.008 s]
Raw data (loadavg): 1.05 1.00 0.95 2/54 10720
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 12659 0 0 0 15943 56 0 0 25 0 1 0 422223032 51949568 11445 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12683 11445 603 41 0 12642 0
vsize: 50732
[startup+170.008 s]
Raw data (loadavg): 1.05 1.00 0.95 2/54 10720
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 13097 0 0 0 16942 57 0 0 25 0 1 0 422223032 53772288 11883 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13128 11883 603 41 0 13087 0
vsize: 52512
[startup+180.009 s]
Raw data (loadavg): 1.04 1.00 0.95 2/54 10720
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 14325 0 0 0 17939 60 0 0 25 0 1 0 422223032 58908672 13111 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14382 13111 603 41 0 14341 0
vsize: 57528
[startup+190.01 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 10720
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 15064 0 0 0 18938 61 0 0 25 0 1 0 422223032 61902848 13850 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15113 13850 603 41 0 15072 0
vsize: 60452
[startup+200.01 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 10720
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 15744 0 0 0 19937 63 0 0 25 0 1 0 422223032 64671744 14530 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15789 14530 603 41 0 15748 0
vsize: 63156
[startup+210.011 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 10720
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 16485 0 0 0 20933 66 0 0 25 0 1 0 422223032 67792896 15271 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16551 15271 603 41 0 16510 0
vsize: 66204
[startup+220.012 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 17101 0 0 0 21932 67 0 0 25 0 1 0 422223032 70283264 15887 4294967295 134512640 134672761 3221224560 3221223696 134614583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17159 15887 603 41 0 17118 0
vsize: 68636
[startup+230.013 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 17808 0 0 0 22930 69 0 0 25 0 1 0 422223032 73162752 16594 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17862 16594 603 41 0 17821 0
vsize: 71448
[startup+240.013 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 18558 0 0 0 23928 71 0 0 25 0 1 0 422223032 76181504 17344 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18599 17344 603 41 0 18558 0
vsize: 74396
[startup+250.013 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 19210 0 0 0 24927 72 0 0 25 0 1 0 422223032 78925824 17996 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19269 17996 603 41 0 19228 0
vsize: 77076
[startup+260.014 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 19925 0 0 0 25926 74 0 0 25 0 1 0 422223032 81813504 18711 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19974 18711 603 41 0 19933 0
vsize: 79896
[startup+270.014 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 21820 0 0 0 26914 85 0 0 25 0 1 0 422223032 84611072 19476 4294967295 134512640 134672761 3221224560 3221222848 134565588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20657 19476 603 41 0 20616 0
vsize: 82628
[startup+280.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 21896 0 0 0 27910 89 0 0 25 0 1 0 422223032 84611072 19476 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20657 19476 603 41 0 20616 0
vsize: 82628
[startup+290.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 21896 0 0 0 28911 89 0 0 25 0 1 0 422223032 84611072 19476 4294967295 134512640 134672761 3221224560 3221223600 134612504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20657 19476 603 41 0 20616 0
vsize: 82628
[startup+300.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 21896 0 0 0 29911 89 0 0 25 0 1 0 422223032 84611072 19476 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20657 19476 603 41 0 20616 0
vsize: 82628
[startup+310.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 21896 0 0 0 30911 89 0 0 25 0 1 0 422223032 84611072 19476 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20657 19476 603 41 0 20616 0
vsize: 82628
[startup+320.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 21896 0 0 0 31911 89 0 0 25 0 1 0 422223032 84611072 19476 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20657 19476 603 41 0 20616 0
vsize: 82628
[startup+330.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 21896 0 0 0 32911 89 0 0 25 0 1 0 422223032 84611072 19476 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20657 19476 603 41 0 20616 0
vsize: 82628
[startup+340.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 21896 0 0 0 33911 89 0 0 25 0 1 0 422223032 84611072 19476 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20657 19476 603 41 0 20616 0
vsize: 82628
[startup+350.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23019 0 0 0 34903 97 0 0 25 0 1 0 422223032 84848640 19548 4294967295 134512640 134672761 3221224560 3221223816 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19548 603 41 0 20674 0
vsize: 82860
[startup+360.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23019 0 0 0 35903 98 0 0 25 0 1 0 422223032 84848640 19548 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19548 603 41 0 20674 0
vsize: 82860
[startup+370.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23019 0 0 0 36903 98 0 0 25 0 1 0 422223032 84848640 19548 4294967295 134512640 134672761 3221224560 3221223408 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19548 603 41 0 20674 0
vsize: 82860
[startup+380.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23020 0 0 0 37903 98 0 0 25 0 1 0 422223032 84848640 19549 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19549 603 41 0 20674 0
vsize: 82860
[startup+390.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23020 0 0 0 38903 98 0 0 25 0 1 0 422223032 84848640 19549 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19549 603 41 0 20674 0
vsize: 82860
[startup+400.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23020 0 0 0 39904 98 0 0 25 0 1 0 422223032 84848640 19549 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19549 603 41 0 20674 0
vsize: 82860
[startup+410.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23020 0 0 0 40904 98 0 0 25 0 1 0 422223032 84848640 19549 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19549 603 41 0 20674 0
vsize: 82860
[startup+420.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23020 0 0 0 41904 98 0 0 25 0 1 0 422223032 84848640 19549 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19549 603 41 0 20674 0
vsize: 82860
[startup+430.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23020 0 0 0 42904 98 0 0 25 0 1 0 422223032 84848640 19549 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19549 603 41 0 20674 0
vsize: 82860
[startup+440.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23020 0 0 0 43904 98 0 0 25 0 1 0 422223032 84848640 19549 4294967295 134512640 134672761 3221224560 3221223696 134614721 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19549 603 41 0 20674 0
vsize: 82860
[startup+450.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23020 0 0 0 44905 98 0 0 25 0 1 0 422223032 84848640 19549 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19549 603 41 0 20674 0
vsize: 82860
[startup+460.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23020 0 0 0 45905 98 0 0 25 0 1 0 422223032 84848640 19549 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19549 603 41 0 20674 0
vsize: 82860
[startup+470.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23020 0 0 0 46905 98 0 0 25 0 1 0 422223032 84848640 19549 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19549 603 41 0 20674 0
vsize: 82860
[startup+480.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23020 0 0 0 47905 98 0 0 25 0 1 0 422223032 84848640 19549 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19549 603 41 0 20674 0
vsize: 82860
[startup+490.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23022 0 0 0 48905 98 0 0 25 0 1 0 422223032 84848640 19551 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19551 603 41 0 20674 0
vsize: 82860
[startup+500.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23024 0 0 0 49905 98 0 0 25 0 1 0 422223032 84848640 19553 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19553 603 41 0 20674 0
vsize: 82860
[startup+510.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10722
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23025 0 0 0 50905 98 0 0 25 0 1 0 422223032 84848640 19554 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20715 19554 603 41 0 20674 0
vsize: 82860
[startup+520.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23123 0 0 0 51905 98 0 0 25 0 1 0 422223032 85245952 19652 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20812 19652 603 41 0 20771 0
vsize: 83248
[startup+530.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 23781 0 0 0 52905 99 0 0 25 0 1 0 422223032 88006656 20310 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21486 20310 603 41 0 21445 0
vsize: 85944
[startup+540.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 24237 0 0 0 53904 100 0 0 25 0 1 0 422223032 89808896 20766 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21926 20766 603 41 0 21885 0
vsize: 87704
[startup+550.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 24634 0 0 0 54903 101 0 0 25 0 1 0 422223032 91521024 21163 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22344 21163 603 41 0 22303 0
vsize: 89376
[startup+560.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 25204 0 0 0 55902 102 0 0 25 0 1 0 422223032 94015488 21733 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22953 21733 603 41 0 22912 0
vsize: 91812
[startup+570.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 25847 0 0 0 56900 104 0 0 25 0 1 0 422223032 96641024 22376 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23594 22376 603 41 0 23553 0
vsize: 94376
[startup+580.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 26406 0 0 0 57899 106 0 0 25 0 1 0 422223032 98971648 22935 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24163 22935 603 41 0 24122 0
vsize: 96652
[startup+590.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 26841 0 0 0 58898 106 0 0 25 0 1 0 422223032 100806656 23370 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24611 23370 603 41 0 24570 0
vsize: 98444
[startup+600.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 27255 0 0 0 59897 107 0 0 25 0 1 0 422223032 102510592 23784 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25027 23784 603 41 0 24986 0
vsize: 100108
[startup+610.032 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 27698 0 0 0 60896 109 0 0 25 0 1 0 422223032 104206336 24227 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25441 24227 603 41 0 25400 0
vsize: 101764
[startup+620.032 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 28188 0 0 0 61896 110 0 0 25 0 1 0 422223032 106299392 24717 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25952 24717 603 41 0 25911 0
vsize: 103808
[startup+630.032 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 28744 0 0 0 62895 111 0 0 25 0 1 0 422223032 108544000 25273 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26500 25273 603 41 0 26459 0
vsize: 106000
[startup+640.033 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 29148 0 0 0 63893 113 0 0 25 0 1 0 422223032 110247936 25677 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26916 25677 603 41 0 26875 0
vsize: 107664
[startup+650.033 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 29694 0 0 0 64892 114 0 0 25 0 1 0 422223032 112484352 26223 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27462 26223 603 41 0 27421 0
vsize: 109848
[startup+660.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 30105 0 0 0 65891 115 0 0 25 0 1 0 422223032 114069504 26634 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27849 26634 603 41 0 27808 0
vsize: 111396
[startup+670.035 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 30633 0 0 0 66890 116 0 0 25 0 1 0 422223032 116277248 27162 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28388 27162 603 41 0 28347 0
vsize: 113552
[startup+680.036 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 31100 0 0 0 67889 117 0 0 25 0 1 0 422223032 118120448 27629 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28838 27629 603 41 0 28797 0
vsize: 115352
[startup+690.036 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 31449 0 0 0 68889 118 0 0 25 0 1 0 422223032 119070720 27862 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29070 27862 603 41 0 29029 0
vsize: 116280
[startup+700.035 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 31449 0 0 0 69889 118 0 0 25 0 1 0 422223032 119070720 27862 4294967295 134512640 134672761 3221224560 3221223760 134610511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29070 27862 603 41 0 29029 0
vsize: 116280
[startup+710.036 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 31449 0 0 0 70889 118 0 0 25 0 1 0 422223032 119070720 27862 4294967295 134512640 134672761 3221224560 3221223744 134615567 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29070 27862 603 41 0 29029 0
vsize: 116280
[startup+720.037 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32761 0 0 0 71877 129 0 0 25 0 1 0 422223032 119222272 27983 4294967295 134512640 134672761 3221224560 3221222860 1075346603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29107 27983 603 41 0 29066 0
vsize: 116428
[startup+730.037 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32761 0 0 0 72877 129 0 0 25 0 1 0 422223032 119222272 27983 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27983 603 41 0 29066 0
vsize: 116428
[startup+740.038 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 73877 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+750.038 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 74877 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+760.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 75877 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+770.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 76877 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+780.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 77877 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+790.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 78878 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+800.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 79878 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+810.042 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 80878 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+820.042 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 81878 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+830.043 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 82878 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+840.044 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 83879 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+850.043 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 84879 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+860.044 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 85879 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+870.044 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 86879 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+880.045 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 87879 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+890.046 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 88879 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+900.046 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 89879 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+910.047 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 90880 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+920.046 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32762 0 0 0 91880 130 0 0 25 0 1 0 422223032 119222272 27984 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27984 603 41 0 29066 0
vsize: 116428
[startup+930.047 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32763 0 0 0 92880 130 0 0 25 0 1 0 422223032 119222272 27985 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27985 603 41 0 29066 0
vsize: 116428
[startup+940.048 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32763 0 0 0 93880 130 0 0 25 0 1 0 422223032 119222272 27985 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27985 603 41 0 29066 0
vsize: 116428
[startup+950.049 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32763 0 0 0 94880 130 0 0 25 0 1 0 422223032 119222272 27985 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27985 603 41 0 29066 0
vsize: 116428
[startup+960.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32763 0 0 0 95881 130 0 0 25 0 1 0 422223032 119222272 27985 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29107 27985 603 41 0 29066 0
vsize: 116428
[startup+970.051 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 96881 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+980.052 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 97881 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+990.051 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 98881 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 99881 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 100882 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 101882 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 102882 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 103882 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 104882 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 105883 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 106883 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 107883 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 108883 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 109883 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223704 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 110884 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223728 134564499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 111884 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 112884 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1140.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 113884 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1150.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 114884 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1160.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 115885 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 116885 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 117885 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 118885 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10724
Raw data (stat): 10667 (minisat+) R 10666 5897 5896 0 -1 0 32842 0 0 0 119885 130 0 0 25 0 1 0 422223032 119201792 27980 4294967295 134512640 134672761 3221224560 3221223744 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29102 27980 603 41 0 29061 0
vsize: 116408
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 10724
Raw data (stat): 10667 (minisat+) Z 10666 5897 5896 0 -1 12 32843 0 0 0 119886 137 0 0 25 0 1 0 422223032 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.13
CPU time (s): 1200.24
CPU user time (s): 1198.86
CPU system time (s): 1.37479
CPU usage (%): 100.009
Max. virtual memory (Kb): 116428
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####