PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        823936 kB
Buffers:         36300 kB
Cached:         136544 kB
SwapCached:         12 kB
Active:          53768 kB
Inactive:       121920 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        823684 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            29312 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:09:34 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 4075 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17874 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 |   17874    35748 |    5362       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   17874    35748 |    7149       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.629904 s)
c ==============================================================================
c [1mFound solution: -20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16912     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   34859    75701 |   10457       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11691          
c   -- var.elim.:  2000/11691          
c   -- var.elim.:  3000/11691          
c   -- var.elim.:  4000/11691          
c   -- var.elim.:  5000/11691          
c   -- var.elim.:  6000/11691          
c   -- var.elim.:  7000/11691          
c   -- var.elim.:  8000/11691          
c   -- var.elim.:  9000/11691          
c   -- var.elim.:  10000/11691          
c   -- var.elim.:  11000/11691          
c   -- var.elim.:  11691/11691          
c   -- var.elim.:  1000/5966          
c   -- var.elim.:  2000/5966          
c   -- var.elim.:  3000/5966          
c   -- var.elim.:  4000/5966          
c   -- var.elim.:  5000/5966          
c   -- var.elim.:  5966/5966          
c   -- var.elim.:  157/157          
c   -- subsuming                       
c   -- var.elim.:  1000/2331          
c   -- var.elim.:  2000/2331          
c   -- var.elim.:  2331/2331          
c   -- var.elim.:  193/193          
c |         0 |   22950    71043 |      --       0       --      -- |     --   | -11904/-4643
c |         0 |   22950    71043 |    9180       0        0     nan |  0.000 % |
c |       101 |   22950    71043 |   10098     101    16045   158.9 | 51.449 % |
c |       251 |   22911    70793 |   11088     250    29647   118.6 | 51.752 % |
c ==============================================================================
c (current CPU-time: 11.9332 s)
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       352 |   26644    80932 |    7993     351    43671   124.4 | 51.752 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6332          
c   -- var.elim.:  2000/6332          
c   -- var.elim.:  3000/6332          
c   -- var.elim.:  4000/6332          
c   -- var.elim.:  5000/6332          
c   -- var.elim.:  6000/6332          
c   -- var.elim.:  6332/6332          
c   -- var.elim.:  1000/2682          
c   -- var.elim.:  2000/2682          
c   -- var.elim.:  2682/2682          
c   -- var.elim.:  21/21          
c   -- subsuming                       
c   -- var.elim.:  1000/2094          
c   -- var.elim.:  2000/2094          
c   -- var.elim.:  2094/2094          
c   -- var.elim.:  83/83          
c |       352 |   23033    75793 |      --     351       --      -- |     --   | -3602/-5120
c |       352 |   23033    75793 |    9213     351    43671   124.4 | 51.752 % |
c |       452 |   23033    75793 |   10134     451    51368   113.9 | 61.144 % |
c |       602 |   23033    75793 |   11147     601    68020   113.2 | 61.144 % |
c |       827 |   22906    74681 |   12195     820    90180   110.0 | 61.946 % |
c |      1164 |   22738    73390 |   13316    1139   140983   123.8 | 62.881 % |
c |      1671 |   22638    72500 |   14583    1607   181716   113.1 | 63.549 % |
c |      2430 |   22565    71896 |   15990    2352   292445   124.3 | 64.017 % |
c |      3569 |   22485    71243 |   17526    3476   475610   136.8 | 64.525 % |
c ==============================================================================
c (current CPU-time: 21.3168 s)
c ==============================================================================
c [1mFound solution: -24[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 |      4575 |   23289    72506 |    6986    4461   642081   143.9 | 64.525 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3425          
c   -- var.elim.:  2000/3425          
c   -- var.elim.:  3000/3425          
c   -- var.elim.:  3425/3425          
c   -- var.elim.:  745/745          
c |      4575 |   22324    68953 |      --    4461       --      -- |     --   | -947/-1610
c |      4575 |   22324    68953 |    8929    3750   321272    85.7 | 64.525 % |
c |      4676 |   22324    68953 |    9822    3851   341685    88.7 | 65.935 % |
c |      4826 |   22284    68591 |   10785    3997   362662    90.7 | 66.186 % |
c |      5053 |   22208    67935 |   11823    4216   401880    95.3 | 66.689 % |
c |      5390 |   22208    67935 |   13005    4553   461436   101.3 | 66.689 % |
c |      5896 |   22208    67935 |   14306    5059   542071   107.1 | 66.689 % |
c |      6655 |   22180    67701 |   15717    5811   675633   116.3 | 66.874 % |
c |      7794 |   22140    67374 |   17257    6937   862888   124.4 | 67.138 % |
c |      9502 |   22096    67048 |   18945    8627  1216091   141.0 | 67.430 % |
c |     12064 |   21956    65925 |   20708   11137  1734884   155.8 | 68.355 % |
c ==============================================================================
c (current CPU-time: 37.3733 s)
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15195 |   22780    68156 |    6833   14263  2615988   183.4 | 68.355 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3157          
c   -- var.elim.:  2000/3157          
c   -- var.elim.:  3000/3157          
c   -- var.elim.:  3157/3157          
c   -- var.elim.:  756/756          
c |     15195 |   21964    66987 |      --   14263       --      -- |     --   | -816/-1168
c |     15195 |   21964    66987 |    8785   14261  2615976   183.4 | 68.355 % |
c |     15296 |   21943    66842 |    9654    9608  1802111   187.6 | 68.884 % |
c |     15446 |   21943    66842 |   10620    9758  1830302   187.6 | 68.884 % |
c |     15671 |   21921    66637 |   11670    9976  1873775   187.8 | 69.028 % |
c |     16009 |   21921    66637 |   12837   10314  1938389   187.9 | 69.027 % |
c |     16515 |   21907    66490 |   14112   10810  2018340   186.7 | 69.120 % |
c |     17274 |   21863    66142 |   15492   11563  2182910   188.8 | 69.408 % |
c |     18414 |   21779    65467 |   16976   12681  2418975   190.8 | 69.958 % |
c |     20122 |   21674    64651 |   18584   14368  2744767   191.0 | 70.625 % |
c |     22684 |   21405    62657 |   20188   16903  3269777   193.4 | 72.275 % |
c |     26528 |   21403    62638 |   22205   20702  4228184   204.2 | 72.288 % |
c ==============================================================================
c (current CPU-time: 70.0763 s)
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     29546 |   21885    63521 |    6565   23683  4857739   205.1 | 72.288 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2608          
c   -- var.elim.:  2000/2608          
c   -- var.elim.:  2608/2608          
c   -- var.elim.:  715/715          
c |     29546 |   21271    60967 |      --   23683       --      -- |     --   | -596/-1105
c |     29546 |   21271    60967 |    8508   19941  3150266   158.0 | 72.288 % |
c |     29646 |   21271    60967 |    9359   13023  1944422   149.3 | 73.361 % |
c |     29796 |   21271    60967 |   10295   13173  1978050   150.2 | 73.361 % |
c |     30021 |   21142    59866 |   11256   13389  1992436   148.8 | 74.143 % |
c |     30358 |   21065    59308 |   12336   13693  2023181   147.8 | 74.587 % |
c |     30864 |   21065    59308 |   13570   14199  2121956   149.4 | 74.586 % |
c |     31625 |   21038    59118 |   14908   14942  2248094   150.5 | 74.743 % |
c |     32765 |   21034    59075 |   16395   16078  2456535   152.8 | 74.769 % |
c |     34473 |   21034    59075 |   18035   17786  2805786   157.8 | 74.769 % |
c |     37035 |   21004    58839 |   19810   20343  3403046   167.3 | 74.965 % |
c |     40879 |   20716    56687 |   21492   24137  4060037   168.2 | 76.725 % |
c |     46645 |   20694    56524 |   23616   17212  2371977   137.8 | 76.855 % |
c |     55294 |   20578    55618 |   25833   25800  3972259   154.0 | 77.573 % |
c |     68269 |   20474    54834 |   28272   22425  3374223   150.5 | 78.225 % |
c |     87731 |   20243    53083 |   30749   23691  3530738   149.0 | 79.685 % |
c ==============================================================================
c (current CPU-time: 257.32 s)
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    112710 |   21469    55556 |    6440   27114  4283328   158.0 | 79.685 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2795          
c   -- var.elim.:  2000/2795          
c   -- var.elim.:  2795/2795          
c   -- var.elim.:  769/769          
c   -- var.elim.:  2/2          
c |    112710 |   20137    53038 |      --   27114       --      -- |     --   | -1319/-2491
c |    112710 |   20137    53038 |    8054   17868  1390697    77.8 | 79.685 % |
c |    112810 |   20137    53038 |    8860   11677   889356    76.2 | 82.403 % |
c |    112962 |   20137    53038 |    9746   11829   915295    77.4 | 82.403 % |
c |    113187 |   20137    53038 |   10720   12054   951372    78.9 | 82.403 % |
c |    113525 |   20137    53038 |   11793   12392   994623    80.3 | 82.403 % |
c |    114031 |   20137    53038 |   12972   12898  1041901    80.8 | 82.403 % |
c |    114790 |   20137    53038 |   14269   13657  1157393    84.7 | 82.403 % |
c |    115929 |   20107    52823 |   15673   14794  1333933    90.2 | 82.568 % |
c |    117638 |   20107    52823 |   17240   16503  1648067    99.9 | 82.568 % |
c |    120200 |   20107    52823 |   18964   19065  2122634   111.3 | 82.567 % |
c |    124044 |   20105    52805 |   20858   22906  2774894   121.1 | 82.579 % |
c |    129810 |   20051    52446 |   22883   28663  3853137   134.4 | 82.885 % |
c |    138461 |   19991    51975 |   25096   23175  3401278   146.8 | 83.191 % |
c |    151435 |   19887    51201 |   27462   18893  2750461   145.6 | 83.755 % |
c |    170897 |   19811    50700 |   30092   17242  2475672   143.6 | 84.119 % |
c |    200089 |   19716    49988 |   32943   23503  3571817   152.0 | 84.648 % |
c ==============================================================================
c (current CPU-time: 483.169 s)
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    219016 |   19713    49876 |    5913   17378  2384114   137.2 | 84.648 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1303          
c   -- var.elim.:  1303/1303          
c   -- var.elim.:  110/110          
c |    219016 |   19681    49713 |      --   17378       --      -- |     --   | -21/-90
c |    219016 |   19681    49713 |    7872    8574   444657    51.9 | 84.648 % |
c |    219116 |   19681    49713 |    8659    8674   457793    52.8 | 84.958 % |
c |    219267 |   19681    49713 |    9525    8825   474637    53.8 | 84.958 % |
c |    219492 |   19681    49713 |   10478    9050   504890    55.8 | 84.958 % |
c |    219829 |   19681    49713 |   11525    9387   546121    58.2 | 84.958 % |
c |    220335 |   19681    49713 |   12678    9893   609627    61.6 | 84.958 % |
c |    221095 |   19681    49713 |   13946   10653   718168    67.4 | 84.958 % |
c |    222234 |   19681    49713 |   15341   11792   862263    73.1 | 84.958 % |
c |    223943 |   19681    49713 |   16875   13501  1098907    81.4 | 84.958 % |
c |    226505 |   19681    49713 |   18562   16063  1506153    93.8 | 84.958 % |
c |    230349 |   19681    49713 |   20418   19907  2173133   109.2 | 84.958 % |
c |    236115 |   19678    49702 |   22457   25666  2986644   116.4 | 84.969 % |
c |    244764 |   19678    49702 |   24703   19408  2505277   129.1 | 84.969 % |
c |    257738 |   19619    49266 |   27092   32328  4376237   135.4 | 85.299 % |
c |    277199 |   19583    48995 |   29746   32619  4236124   129.9 | 85.487 % |
c |    306391 |   19387    47520 |   32393   18471  1933635   104.7 | 86.523 % |
c |    350181 |   19350    47260 |   35565   36944  4476606   121.2 | 86.712 % |
c |    415865 |   19315    47020 |   39050   21559  2069871    96.0 | 86.912 % |
c ==============================================================================
c (current CPU-time: 958.652 s)
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    449429 |   19348    46978 |    5804   24434  2561696   104.8 | 86.912 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1139          
c   -- var.elim.:  1139/1139          
c   -- var.elim.:  252/252          
c |    449429 |   19284    46844 |      --   24434       --      -- |     --   | -61/-127
c |    449429 |   19284    46844 |    7713   22234  2172208    97.7 | 86.912 % |
c |    449529 |   19284    46844 |    8484   14923  1464019    98.1 | 87.224 % |
c |    449679 |   19284    46844 |    9333   15073  1477501    98.0 | 87.224 % |
c |    449904 |   19284    46844 |   10266   15298  1501792    98.2 | 87.224 % |
c |    450241 |   19284    46844 |   11293   15635  1540743    98.5 | 87.223 % |
c |    450749 |   19284    46844 |   12422   16143  1593960    98.7 | 87.224 % |
c |    451508 |   19284    46844 |   13665   16902  1687445    99.8 | 87.224 % |
c |    452649 |   19284    46844 |   15031   18043  1822851   101.0 | 87.223 % |
c |    454357 |   19284    46844 |   16534   19751  2035198   103.0 | 87.224 % |
c |    456920 |   19284    46844 |   18188   22314  2358713   105.7 | 87.224 % |
c |    460764 |   19284    46844 |   20007   15026  1470627    97.9 | 87.224 % |
c |    466530 |   19284    46844 |   22007   20792  2099528   101.0 | 87.224 % |
c |    475180 |   19256    46630 |   24173   29390  3147821   107.1 | 87.388 % |
c |    488155 |   19230    46477 |   26554   26068  2557661    98.1 | 87.540 % |
c |    507616 |   19197    46199 |   29160   28009  2440493    87.1 | 87.716 % |
c |    536808 |   19146    45864 |   31991   16114  1266168    78.6 | 87.985 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 C346 -C345 -C344 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.93 0.91 2/54 32500
Raw data (stat): 32500 (runsolver) R 32499 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480396139 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+9.99969 s]
Raw data (loadavg): 0.87 0.93 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 2487 0 0 0 989 9 0 0 25 0 1 0 480396139 12283904 2377 4294967295 134512640 134672761 3221224560 3221223148 1075346912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2999 2377 603 41 0 2958 0
vsize: 11996
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.93 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 3370 0 0 0 1981 18 0 0 25 0 1 0 480396139 14766080 2811 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3605 2811 603 41 0 3564 0
vsize: 14420
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 4889 0 0 0 2975 24 0 0 25 0 1 0 480396139 19066880 3855 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4655 3855 603 41 0 4614 0
vsize: 18620
[startup+40.001 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 6938 0 0 0 3967 31 0 0 25 0 1 0 480396139 25247744 5413 4294967295 134512640 134672761 3221224560 3221223600 134603565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6164 5413 603 41 0 6123 0
vsize: 24656
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 6939 0 0 0 4967 31 0 0 25 0 1 0 480396139 25247744 5414 4294967295 134512640 134672761 3221224560 3221223664 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6164 5414 603 41 0 6123 0
vsize: 24656
[startup+60.002 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 8054 0 0 0 5964 35 0 0 25 0 1 0 480396139 29876224 6529 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7294 6529 603 41 0 7253 0
vsize: 29176
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 9035 0 0 0 6961 38 0 0 25 0 1 0 480396139 33972224 7510 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8294 7510 603 41 0 8253 0
vsize: 33176
[startup+80.0031 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 9865 0 0 0 7956 43 0 0 25 0 1 0 480396139 36388864 8027 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8884 8027 603 41 0 8843 0
vsize: 35536
[startup+90.0034 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 9865 0 0 0 8956 43 0 0 25 0 1 0 480396139 36388864 8027 4294967295 134512640 134672761 3221224560 3221223704 134616123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8884 8027 603 41 0 8843 0
vsize: 35536
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 9867 0 0 0 9956 43 0 0 25 0 1 0 480396139 36388864 8029 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8884 8029 603 41 0 8843 0
vsize: 35536
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 9871 0 0 0 10956 43 0 0 25 0 1 0 480396139 36388864 8033 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8884 8033 603 41 0 8843 0
vsize: 35536
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 9871 0 0 0 11956 43 0 0 25 0 1 0 480396139 36388864 8033 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8884 8033 603 41 0 8843 0
vsize: 35536
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 9871 0 0 0 12957 43 0 0 25 0 1 0 480396139 36388864 8033 4294967295 134512640 134672761 3221224560 3221223744 134615683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8884 8033 603 41 0 8843 0
vsize: 35536
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 9887 0 0 0 13957 43 0 0 25 0 1 0 480396139 36388864 8049 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8884 8049 603 41 0 8843 0
vsize: 35536
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 10001 0 0 0 14957 44 0 0 25 0 1 0 480396139 36458496 8163 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8901 8163 603 41 0 8860 0
vsize: 35604
[startup+160.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 10001 0 0 0 15957 44 0 0 25 0 1 0 480396139 36458496 8163 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8901 8163 603 41 0 8860 0
vsize: 35604
[startup+170.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 10001 0 0 0 16957 44 0 0 25 0 1 0 480396139 36458496 8163 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8901 8163 603 41 0 8860 0
vsize: 35604
[startup+180.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 10130 0 0 0 17957 44 0 0 25 0 1 0 480396139 37117952 8292 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9062 8292 603 41 0 9021 0
vsize: 36248
[startup+190.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 10528 0 0 0 18956 45 0 0 25 0 1 0 480396139 39038976 8690 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9531 8690 603 41 0 9490 0
vsize: 38124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 10528 0 0 0 19956 45 0 0 25 0 1 0 480396139 39038976 8690 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9531 8690 603 41 0 9490 0
vsize: 38124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 10528 0 0 0 20957 45 0 0 25 0 1 0 480396139 39038976 8690 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9531 8690 603 41 0 9490 0
vsize: 38124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 10528 0 0 0 21957 45 0 0 25 0 1 0 480396139 39038976 8690 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9531 8690 603 41 0 9490 0
vsize: 38124
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 10811 0 0 0 22956 46 0 0 25 0 1 0 480396139 39952384 8973 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9754 8973 603 41 0 9713 0
vsize: 39016
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 11326 0 0 0 23954 47 0 0 25 0 1 0 480396139 41877504 9450 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10224 9450 603 41 0 10183 0
vsize: 40896
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 11326 0 0 0 24955 47 0 0 25 0 1 0 480396139 41877504 9450 4294967295 134512640 134672761 3221224560 3221223552 134565146 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10224 9450 603 41 0 10183 0
vsize: 40896
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 11994 0 0 0 25951 51 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+270.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 11994 0 0 0 26951 51 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+280.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 11994 0 0 0 27951 51 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+290.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 11994 0 0 0 28951 51 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 11994 0 0 0 29951 51 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 11994 0 0 0 30951 51 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 11994 0 0 0 31951 51 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 11994 0 0 0 32951 51 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12027 0 0 0 33951 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12027 0 0 0 34951 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12027 0 0 0 35951 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12027 0 0 0 36952 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12062 0 0 0 37951 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12062 0 0 0 38952 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12062 0 0 0 39952 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12062 0 0 0 40952 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12062 0 0 0 41952 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12099 0 0 0 42952 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12099 0 0 0 43952 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12099 0 0 0 44952 52 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223600 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12099 0 0 0 45953 53 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223600 134612659 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12099 0 0 0 46953 53 0 0 25 0 1 0 480396139 41955328 9513 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9513 603 41 0 10202 0
vsize: 40972
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 12311 0 0 0 47952 53 0 0 25 0 1 0 480396139 42872832 9725 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10467 9725 603 41 0 10426 0
vsize: 41868
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13036 0 0 0 48948 57 0 0 25 0 1 0 480396139 43737088 9946 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9946 603 41 0 10637 0
vsize: 42712
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13036 0 0 0 49947 57 0 0 25 0 1 0 480396139 43737088 9946 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9946 603 41 0 10637 0
vsize: 42712
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13036 0 0 0 50948 57 0 0 25 0 1 0 480396139 43737088 9946 4294967295 134512640 134672761 3221224560 3221223600 134614202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9946 603 41 0 10637 0
vsize: 42712
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13036 0 0 0 51948 57 0 0 25 0 1 0 480396139 43737088 9946 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9946 603 41 0 10637 0
vsize: 42712
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13036 0 0 0 52948 57 0 0 25 0 1 0 480396139 43737088 9946 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9946 603 41 0 10637 0
vsize: 42712
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 53948 57 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 54948 57 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 55948 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223792 134541802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 56948 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 57949 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 58949 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 59949 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223588 134612938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 60949 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 61949 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+630.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32500
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 62952 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+640.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32553
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 63951 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+650.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32553
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 64951 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+660.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32553
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 65952 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+670.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32553
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 66952 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+680.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32553
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 67952 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+690.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32553
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 68952 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+700.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 69952 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+710.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 70953 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+720.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 71953 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+730.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 72953 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+740.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 73953 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+750.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13037 0 0 0 74953 58 0 0 25 0 1 0 480396139 43737088 9947 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9947 603 41 0 10637 0
vsize: 42712
[startup+760.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13038 0 0 0 75953 58 0 0 25 0 1 0 480396139 43737088 9948 4294967295 134512640 134672761 3221224560 3221223600 134612653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9948 603 41 0 10637 0
vsize: 42712
[startup+770.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 76954 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+780.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 77954 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 78954 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+800.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 79954 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+810.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 80954 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 81955 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+830.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 82955 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+840.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 83955 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223600 134613815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+850.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 84955 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+860.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 85955 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+870.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 86956 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+880.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 87956 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+890.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 88956 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+900.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 89956 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+910.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 90956 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+920.047 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 91957 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+930.047 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13040 0 0 0 92957 58 0 0 25 0 1 0 480396139 43737088 9950 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9950 603 41 0 10637 0
vsize: 42712
[startup+940.048 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13042 0 0 0 93957 58 0 0 25 0 1 0 480396139 43737088 9952 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9952 603 41 0 10637 0
vsize: 42712
[startup+950.048 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13043 0 0 0 94957 58 0 0 25 0 1 0 480396139 43737088 9953 4294967295 134512640 134672761 3221224560 3221223744 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9953 603 41 0 10637 0
vsize: 42712
[startup+960.048 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13474 0 0 0 95955 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223656 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+970.049 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13474 0 0 0 96955 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+980.048 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 32555
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13474 0 0 0 97955 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+990.049 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13474 0 0 0 98955 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223600 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1000.05 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13474 0 0 0 99955 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1010.05 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13474 0 0 0 100955 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1020.05 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13474 0 0 0 101955 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1030.05 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13474 0 0 0 102955 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1040.05 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13474 0 0 0 103955 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13508 0 0 0 104955 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13508 0 0 0 105956 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13508 0 0 0 106956 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13508 0 0 0 107956 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13545 0 0 0 108956 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223684 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13545 0 0 0 109956 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13545 0 0 0 110957 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13545 0 0 0 111957 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13582 0 0 0 112957 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13582 0 0 0 113957 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13582 0 0 0 114957 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13582 0 0 0 115957 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13622 0 0 0 116958 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13622 0 0 0 117958 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13622 0 0 0 118958 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 32557
Raw data (stat): 32500 (minisat+) R 32499 27222 27221 0 -1 0 13622 0 0 0 119958 61 0 0 25 0 1 0 480396139 42995712 9781 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9781 603 41 0 10456 0
vsize: 41988
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 32557
Raw data (stat): 32500 (minisat+) Z 32499 27222 27221 0 -1 12 13623 0 0 0 119958 64 0 0 25 0 1 0 480396139 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.09
CPU time (s): 1200.23
CPU user time (s): 1199.59
CPU system time (s): 0.641902
CPU usage (%): 100.012
Max. virtual memory (Kb): 42712
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####