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/frb35-17-opb/normalized-frb35-17-3.opb
MD5SUM	25457db86ce3cc3b7604dfa37c8096b4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-28
Optimality of the best value was proved	NO
Number of terms in the objective function	595
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	595
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	595
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.05
Number of variables	595
Total number of constraints	27931
Number of constraints which are clauses	27931
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 5613

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        893600 kB
Buffers:         34592 kB
Cached:          63476 kB
SwapCached:        192 kB
Active:          50204 kB
Inactive:        50948 kB
HighTotal:      131008 kB
HighFree:        63700 kB
LowTotal:       903652 kB
LowFree:        829900 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34420 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:10:47 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 4081 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27931 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 |   27931    55862 |    8379       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   27931    55862 |   11172       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.07584 s)
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:26814     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   56226   122317 |   16867       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/19352          
c   -- var.elim.:  2000/19352          
c   -- var.elim.:  3000/19352          
c   -- var.elim.:  4000/19352          
c   -- var.elim.:  5000/19352          
c   -- var.elim.:  6000/19352          
c   -- var.elim.:  7000/19352          
c   -- var.elim.:  8000/19352          
c   -- var.elim.:  9000/19352          
c   -- var.elim.:  10000/19352          
c   -- var.elim.:  11000/19352          
c   -- var.elim.:  12000/19352          
c   -- var.elim.:  13000/19352          
c   -- var.elim.:  14000/19352          
c   -- var.elim.:  15000/19352          
c   -- var.elim.:  16000/19352          
c   -- var.elim.:  17000/19352          
c   -- var.elim.:  18000/19352          
c   -- var.elim.:  19000/19352          
c   -- var.elim.:  19352/19352          
c   -- var.elim.:  1000/9850          
c   -- var.elim.:  2000/9850          
c   -- var.elim.:  3000/9850          
c   -- var.elim.:  4000/9850          
c   -- var.elim.:  5000/9850          
c   -- var.elim.:  6000/9850          
c   -- var.elim.:  7000/9850          
c   -- var.elim.:  8000/9850          
c   -- var.elim.:  9000/9850          
c   -- var.elim.:  9850/9850          
c   -- var.elim.:  85/85          
c   -- var.elim.:  37/37          
c   -- subsuming                       
c   -- var.elim.:  1000/3815          
c   -- var.elim.:  2000/3815          
c   -- var.elim.:  3000/3815          
c   -- var.elim.:  3815/3815          
c   -- var.elim.:  254/254          
c |         0 |   36254   121443 |      --       0       --      -- |     --   | -19972/-873
c |         0 |   36254   121443 |   14501       0        0     nan |  0.000 % |
c |       100 |   36254   121443 |   15951     100    10412   104.1 | 52.946 % |
c |       250 |   36254   121443 |   17546     250    39243   157.0 | 52.946 % |
c |       476 |   36254   121443 |   19301     476    68750   144.4 | 52.946 % |
c |       813 |   36254   121443 |   21231     813   130238   160.2 | 52.946 % |
c |      1319 |   36172   120765 |   23302    1312   223603   170.4 | 53.323 % |
c |      2078 |   36105   120203 |   25584    2066   389085   188.3 | 53.670 % |
c ==============================================================================
c (current CPU-time: 41.6297 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 |      2647 |   36171   120199 |   10851    2630   518284   197.1 | 53.670 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3353          
c   -- var.elim.:  2000/3353          
c   -- var.elim.:  3000/3353          
c   -- var.elim.:  3353/3353          
c   -- var.elim.:  215/215          
c |      2647 |   36077   119994 |      --    2630       --      -- |     --   | -84/43
c |      2647 |   36077   119994 |   14430    2409   381338   158.3 | 53.670 % |
c |      2747 |   36077   119994 |   15873    2509   394621   157.3 | 54.009 % |
c |      2898 |   36043   119665 |   17444    2657   418279   157.4 | 54.172 % |
c |      3123 |   36043   119665 |   19189    2882   454836   157.8 | 54.171 % |
c |      3460 |   36005   119362 |   21085    3215   504171   156.8 | 54.364 % |
c |      3966 |   36005   119362 |   23194    3721   578955   155.6 | 54.364 % |
c ==============================================================================
c (current CPU-time: 47.4068 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 |      4231 |   38862   127118 |   11658    3986   644141   161.6 | 54.364 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6064          
c   -- var.elim.:  2000/6064          
c   -- var.elim.:  3000/6064          
c   -- var.elim.:  4000/6064          
c   -- var.elim.:  5000/6064          
c   -- var.elim.:  6000/6064          
c   -- var.elim.:  6064/6064          
c   -- var.elim.:  1000/2070          
c   -- var.elim.:  2000/2070          
c   -- var.elim.:  2070/2070          
c   -- var.elim.:  6/6          
c |      4231 |   36095   125025 |      --    3986       --      -- |     --   | -2760/-2078
c |      4231 |   36095   125025 |   14438    3927   613985   156.3 | 54.364 % |
c |      4332 |   36095   125025 |   15881    4028   636877   158.1 | 58.204 % |
c |      4482 |   36057   124666 |   17451    4176   661794   158.5 | 58.380 % |
c |      4707 |   35986   124079 |   19158    4393   691920   157.5 | 58.675 % |
c |      5044 |   35935   123652 |   21044    4721   752101   159.3 | 58.888 % |
c |      5550 |   35935   123652 |   23149    5227   865953   165.7 | 58.888 % |
c |      6309 |   35747   122024 |   25331    5978  1029571   172.2 | 59.710 % |
c |      7449 |   35675   121542 |   27808    7099  1268492   178.7 | 59.932 % |
c ==============================================================================
c (current CPU-time: 64.0633 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 |      8418 |   35510   119557 |   10652    8018  1447040   180.5 | 59.932 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4229          
c   -- var.elim.:  2000/4229          
c   -- var.elim.:  3000/4229          
c   -- var.elim.:  4000/4229          
c   -- var.elim.:  4229/4229          
c   -- var.elim.:  208/208          
c |      8418 |   35402   118940 |      --    8018       --      -- |     --   | -98/-392
c |      8418 |   35402   118940 |   14160    8018  1447040   180.5 | 59.932 % |
c |      8519 |   35402   118940 |   15576    8119  1459994   179.8 | 61.218 % |
c |      8669 |   35402   118940 |   17134    8269  1496812   181.0 | 61.219 % |
c |      8894 |   35402   118940 |   18848    8494  1535785   180.8 | 61.219 % |
c |      9231 |   35402   118940 |   20732    8831  1595413   180.7 | 61.219 % |
c |      9738 |   35378   118735 |   22790    8533  1247109   146.2 | 61.330 % |
c |     10497 |   35322   118261 |   25030    9288  1431168   154.1 | 61.589 % |
c |     11636 |   35185   117028 |   27426   10402  1727689   166.1 | 62.217 % |
c |     13344 |   35091   116269 |   30088   12091  2173033   179.7 | 62.652 % |
c |     15906 |   34993   115464 |   33004   14631  2987302   204.2 | 63.105 % |
c ==============================================================================
c (current CPU-time: 86.8968 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 |     16911 |   35116   115405 |   10534   15625  3223828   206.3 | 63.105 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3438          
c   -- var.elim.:  2000/3438          
c   -- var.elim.:  3000/3438          
c   -- var.elim.:  3438/3438          
c   -- var.elim.:  193/193          
c |     16911 |   34954   115159 |      --   15625       --      -- |     --   | -162/-245
c |     16911 |   34954   115159 |   13981   15610  3223777   206.5 | 63.105 % |
c |     17012 |   34954   115159 |   15379   15711  3237539   206.1 | 63.476 % |
c |     17162 |   34918   114878 |   16900   15860  3268632   206.1 | 63.642 % |
c |     17388 |   34918   114878 |   18590   16086  3329218   207.0 | 63.642 % |
c |     17726 |   34918   114878 |   20449   16424  3420588   208.3 | 63.642 % |
c |     18232 |   34816   113934 |   22428   16914  3518472   208.0 | 64.112 % |
c |     18991 |   34762   113478 |   24633   17645  3719753   210.8 | 64.352 % |
c |     20130 |   34708   113031 |   27054   18767  4181507   222.8 | 64.601 % |
c |     21839 |   34614   112241 |   29679   20462  4639105   226.7 | 65.016 % |
c |     24401 |   34431   110668 |   32474   22931  5327167   232.3 | 65.827 % |
c |     28246 |   34229   108840 |   35512   26701  6226519   233.2 | 66.713 % |
c |     34014 |   34122   107894 |   38941   32432  7756031   239.1 | 67.183 % |
c |     42664 |   33667   103784 |   42264   40991 10427068   254.4 | 69.231 % |
c |     55638 |   33240   100168 |   45901   22068  4717660   213.8 | 71.177 % |
c ==============================================================================
c (current CPU-time: 256.939 s)
c ==============================================================================
c [1mFound solution: -30[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 |     59657 |   33283   100106 |    9984   26072  5849631   224.4 | 71.177 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2776          
c   -- var.elim.:  2000/2776          
c   -- var.elim.:  2776/2776          
c   -- var.elim.:  188/188          
c |     59657 |   33195    97521 |      --   26072       --      -- |     --   | -69/-431
c |     59657 |   33195    97521 |   13278   19618  2009220   102.4 | 71.177 % |
c |     59757 |   33195    97521 |   14605   19718  2025439   102.7 | 71.453 % |
c |     59907 |   33195    97521 |   16066   19868  2058581   103.6 | 71.452 % |
c |     60133 |   33175    97334 |   17662   20092  2110463   105.0 | 71.545 % |
c |     60470 |   33175    97334 |   19428   20429  2198477   107.6 | 71.545 % |
c |     60980 |   33119    96848 |   21335   20935  2305111   110.1 | 71.794 % |
c |     61739 |   33119    96848 |   23468   21694  2501274   115.3 | 71.794 % |
c |     62878 |   33113    96794 |   25811   22823  2764025   121.1 | 71.813 % |
c |     64587 |   33113    96794 |   28392   24532  3301951   134.6 | 71.813 % |
c |     67149 |   33011    95857 |   31135   27050  4054522   149.9 | 72.283 % |
c |     70993 |   32989    95656 |   34225   30883  5065175   164.0 | 72.385 % |
c |     76759 |   32952    95387 |   37606   36646  6564474   179.1 | 72.542 % |
c |     85408 |   32899    95030 |   41300   45285  9147115   202.0 | 72.773 % |
c |     98382 |   32822    94411 |   45324   25844  5352273   207.1 | 73.115 % |
c ==============================================================================
c (current CPU-time: 437.029 s)
c ==============================================================================
c [1mFound solution: -31[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 |    114329 |   35178   100052 |   10553   41767  9731100   233.0 | 73.115 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5212          
c   -- var.elim.:  2000/5212          
c   -- var.elim.:  3000/5212          
c   -- var.elim.:  4000/5212          
c   -- var.elim.:  5000/5212          
c   -- var.elim.:  5212/5212          
c   -- var.elim.:  1000/1601          
c   -- var.elim.:  1601/1601          
c |    114329 |   32797    97142 |      --   41767       --      -- |     --   | -2372/-2891
c |    114329 |   32797    97142 |   13118   41326  9519739   230.4 | 73.115 % |
c |    114429 |   32797    97142 |   14430   18729  3331976   177.9 | 79.819 % |
c |    114579 |   32797    97142 |   15873   18879  3378772   179.0 | 79.818 % |
c |    114804 |   32795    97122 |   17460   19100  3426141   179.4 | 79.825 % |
c |    115142 |   32795    97122 |   19206   19438  3511669   180.7 | 79.825 % |
c |    115648 |   32795    97122 |   21126   19944  3655457   183.3 | 79.825 % |
c |    116407 |   32795    97122 |   23239   20703  3820419   184.5 | 79.826 % |
c |    117547 |   32765    96829 |   25539   21840  4048632   185.4 | 79.930 % |
c |    119255 |   32765    96829 |   28093   23548  4492843   190.8 | 79.930 % |
c |    121817 |   32615    95417 |   30761   26080  4992382   191.4 | 80.392 % |
c |    125661 |   32430    93637 |   33646   29845  5952397   199.4 | 80.993 % |
c |    131427 |   32353    92918 |   36922   35553  7419959   208.7 | 81.258 % |
c |    140077 |   32096    90660 |   40292   44117  9658229   218.9 | 82.104 % |
c |    153051 |   31634    86548 |   43683   21596  3740030   173.2 | 83.606 % |
c |    172512 |   31389    84638 |   47679   41022  8507382   207.4 | 84.375 % |
c |    201705 |   31212    83241 |   52152   25357  5451143   215.0 | 84.990 % |
c |    245495 |   30975    81205 |   56931   19547  4179862   213.8 | 85.800 % |
c ==============================================================================
c (current CPU-time: 1098.07 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 |    295220 |   30634    78184 |    9190   69089 15712424   227.4 | 85.800 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1870          
c   -- var.elim.:  1870/1870          
c   -- var.elim.:  295/295          
c |    295220 |   30584    77758 |      --   69089       --      -- |     --   | -39/-227
c |    295220 |   30584    77758 |   12233   32867  2721270    82.8 | 85.800 % |
c |    295320 |   30584    77758 |   13456   10247   643631    62.8 | 87.302 % |
c |    295470 |   30584    77758 |   14802   10397   664877    63.9 | 87.302 % |
c |    295696 |   30584    77758 |   16282   10623   693260    65.3 | 87.302 % |
c |    296033 |   30584    77758 |   17911   10960   758492    69.2 | 87.302 % |
c |    296540 |   30584    77758 |   19702   11467   850726    74.2 | 87.302 % |
c |    297299 |   30584    77758 |   21672   12226   965416    79.0 | 87.302 % |
c |    298438 |   30584    77758 |   23839   13365  1156639    86.5 | 87.302 % |
c |    300147 |   30584    77758 |   26223   15074  1474185    97.8 | 87.302 % |
c |    302709 |   30584    77758 |   28846   17636  1995400   113.1 | 87.302 % |
c |    306554 |   30584    77758 |   31730   21481  2761242   128.5 | 87.302 % |
c |    312320 |   30584    77758 |   34903   27247  3875900   142.3 | 87.302 % |
c |    320969 |   30582    77735 |   38391   35887  5459582   152.1 | 87.309 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -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 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -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 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 C173 -C172 -C171 -C170 C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 C137 -C136 -C135 -C134 C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 C105#### 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.93 0.98 0.91 2/54 6996
Raw data (stat): 6996 (runsolver) R 6995 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480404997 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99979 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 3653 0 0 0 985 13 0 0 25 0 1 0 480404997 17596416 3631 4294967295 134512640 134672761 3221224560 3221223152 134607998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4296 3631 603 41 0 4255 0
vsize: 17184
[startup+19.9994 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 3669 0 0 0 1985 13 0 0 25 0 1 0 480404997 17739776 3647 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4331 3647 603 41 0 4290 0
vsize: 17324
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 3699 0 0 0 2985 13 0 0 25 0 1 0 480404997 17936384 3677 4294967295 134512640 134672761 3221224560 3221223008 134643532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3677 603 41 0 4338 0
vsize: 17516
[startup+39.9997 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 3911 0 0 0 3984 14 0 0 25 0 1 0 480404997 18198528 3779 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4443 3779 603 41 0 4402 0
vsize: 17772
[startup+49.9993 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 5567 0 0 0 4970 28 0 0 25 0 1 0 480404997 21127168 4571 4294967295 134512640 134672761 3221224560 3221223008 134643987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5158 4571 603 41 0 5117 0
vsize: 20632
[startup+59.9993 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 5723 0 0 0 5970 28 0 0 25 0 1 0 480404997 21782528 4727 4294967295 134512640 134672761 3221224560 3221223760 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5318 4727 603 41 0 5277 0
vsize: 21272
[startup+69.9997 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 6921 0 0 0 6963 34 0 0 25 0 1 0 480404997 23592960 5183 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5760 5183 603 41 0 5719 0
vsize: 23040
[startup+80.0003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 7630 0 0 0 7961 36 0 0 25 0 1 0 480404997 26595328 5892 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6493 5892 603 41 0 6452 0
vsize: 25972
[startup+90.0002 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 9361 0 0 0 8954 43 0 0 25 0 1 0 480404997 31649792 7153 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7727 7153 603 41 0 7686 0
vsize: 30908
[startup+99.9996 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 9913 0 0 0 9953 44 0 0 25 0 1 0 480404997 34000896 7705 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7705 603 41 0 8260 0
vsize: 33204
[startup+110 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 10848 0 0 0 10951 47 0 0 25 0 1 0 480404997 37789696 8640 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9226 8640 603 41 0 9185 0
vsize: 36904
[startup+120 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 11643 0 0 0 11949 49 0 0 25 0 1 0 480404997 41021440 9435 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10015 9435 603 41 0 9974 0
vsize: 40060
[startup+130 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 12458 0 0 0 12946 51 0 0 25 0 1 0 480404997 44441600 10250 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10850 10250 603 41 0 10809 0
vsize: 43400
[startup+140 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 13209 0 0 0 13944 54 0 0 25 0 1 0 480404997 47431680 11001 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11580 11001 603 41 0 11539 0
vsize: 46320
[startup+150 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 13836 0 0 0 14942 56 0 0 25 0 1 0 480404997 50020352 11628 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12212 11628 603 41 0 12171 0
vsize: 48848
[startup+160 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 14675 0 0 0 15941 58 0 0 25 0 1 0 480404997 53534720 12467 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13070 12467 603 41 0 13029 0
vsize: 52280
[startup+170 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 15485 0 0 0 16940 59 0 0 25 0 1 0 480404997 56922112 13277 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13897 13277 603 41 0 13856 0
vsize: 55588
[startup+180.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 16015 0 0 0 17938 60 0 0 25 0 1 0 480404997 59023360 13807 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14410 13807 603 41 0 14369 0
vsize: 57640
[startup+190 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 16651 0 0 0 18938 62 0 0 25 0 1 0 480404997 61628416 14443 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15046 14443 603 41 0 15005 0
vsize: 60184
[startup+200 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 17298 0 0 0 19936 63 0 0 25 0 1 0 480404997 64249856 15090 4294967295 134512640 134672761 3221224560 3221223744 134616011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15686 15090 603 41 0 15645 0
vsize: 62744
[startup+210 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 17939 0 0 0 20934 65 0 0 25 0 1 0 480404997 66863104 15731 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16324 15731 603 41 0 16283 0
vsize: 65296
[startup+220 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 18683 0 0 0 21933 67 0 0 25 0 1 0 480404997 69963776 16475 4294967295 134512640 134672761 3221224560 3221223372 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17081 16476 603 41 0 17040 0
vsize: 68324
[startup+230.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 19296 0 0 0 22932 68 0 0 25 0 1 0 480404997 72417280 17088 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17680 17088 603 41 0 17639 0
vsize: 70720
[startup+240.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 19625 0 0 0 23931 69 0 0 25 0 1 0 480404997 73543680 17367 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17955 17367 603 41 0 17914 0
vsize: 71820
[startup+250 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 19625 0 0 0 24931 69 0 0 25 0 1 0 480404997 73543680 17367 4294967295 134512640 134672761 3221224560 3221223600 134614225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17955 17367 603 41 0 17914 0
vsize: 71820
[startup+260 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20362 0 0 0 25925 74 0 0 25 0 1 0 480404997 73674752 17403 4294967295 134512640 134672761 3221224560 3221223008 134643518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17987 17403 603 41 0 17946 0
vsize: 71948
[startup+270 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20363 0 0 0 26925 74 0 0 25 0 1 0 480404997 73674752 17404 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17987 17404 603 41 0 17946 0
vsize: 71948
[startup+280 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20363 0 0 0 27925 74 0 0 25 0 1 0 480404997 73674752 17404 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17404 603 41 0 17946 0
vsize: 71948
[startup+290.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20363 0 0 0 28925 74 0 0 25 0 1 0 480404997 73674752 17404 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17404 603 41 0 17946 0
vsize: 71948
[startup+300.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20363 0 0 0 29925 74 0 0 25 0 1 0 480404997 73674752 17404 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17987 17404 603 41 0 17946 0
vsize: 71948
[startup+310.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20363 0 0 0 30924 75 0 0 25 0 1 0 480404997 73674752 17404 4294967295 134512640 134672761 3221224560 3221223704 134616320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17404 603 41 0 17946 0
vsize: 71948
[startup+320.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20363 0 0 0 31924 75 0 0 25 0 1 0 480404997 73674752 17404 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17404 603 41 0 17946 0
vsize: 71948
[startup+330.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20363 0 0 0 32924 75 0 0 25 0 1 0 480404997 73674752 17404 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17404 603 41 0 17946 0
vsize: 71948
[startup+340.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20363 0 0 0 33925 75 0 0 25 0 1 0 480404997 73674752 17404 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17404 603 41 0 17946 0
vsize: 71948
[startup+350.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20363 0 0 0 34925 75 0 0 25 0 1 0 480404997 73674752 17404 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17404 603 41 0 17946 0
vsize: 71948
[startup+360.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20363 0 0 0 35925 75 0 0 25 0 1 0 480404997 73674752 17404 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17404 603 41 0 17946 0
vsize: 71948
[startup+370.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20415 0 0 0 36925 75 0 0 25 0 1 0 480404997 73674752 17405 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17405 603 41 0 17946 0
vsize: 71948
[startup+380.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20415 0 0 0 37925 75 0 0 25 0 1 0 480404997 73674752 17405 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17405 603 41 0 17946 0
vsize: 71948
[startup+390.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20415 0 0 0 38926 75 0 0 25 0 1 0 480404997 73674752 17405 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17405 603 41 0 17946 0
vsize: 71948
[startup+400.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20415 0 0 0 39926 75 0 0 25 0 1 0 480404997 73674752 17405 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17405 603 41 0 17946 0
vsize: 71948
[startup+410.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20415 0 0 0 40926 75 0 0 25 0 1 0 480404997 73674752 17405 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17405 603 41 0 17946 0
vsize: 71948
[startup+420.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20415 0 0 0 41926 75 0 0 25 0 1 0 480404997 73674752 17405 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17405 603 41 0 17946 0
vsize: 71948
[startup+430.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 20415 0 0 0 42926 75 0 0 25 0 1 0 480404997 73674752 17405 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17405 603 41 0 17946 0
vsize: 71948
[startup+440.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21223 0 0 0 43918 83 0 0 25 0 1 0 480404997 73674752 17507 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17987 17507 603 41 0 17946 0
vsize: 71948
[startup+450.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21264 0 0 0 44917 83 0 0 25 0 1 0 480404997 73674752 17507 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17507 603 41 0 17946 0
vsize: 71948
[startup+460.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21264 0 0 0 45918 83 0 0 25 0 1 0 480404997 73674752 17507 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17507 603 41 0 17946 0
vsize: 71948
[startup+470.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21264 0 0 0 46918 83 0 0 25 0 1 0 480404997 73674752 17507 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17987 17507 603 41 0 17946 0
vsize: 71948
[startup+480.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21264 0 0 0 47917 83 0 0 25 0 1 0 480404997 73674752 17507 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17987 17507 603 41 0 17946 0
vsize: 71948
[startup+490.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21264 0 0 0 48916 84 0 0 25 0 1 0 480404997 73674752 17507 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17507 603 41 0 17946 0
vsize: 71948
[startup+500.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21264 0 0 0 49916 84 0 0 25 0 1 0 480404997 73674752 17507 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17507 603 41 0 17946 0
vsize: 71948
[startup+510.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21264 0 0 0 50916 84 0 0 25 0 1 0 480404997 73674752 17507 4294967295 134512640 134672761 3221224560 3221223732 134616080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17507 603 41 0 17946 0
vsize: 71948
[startup+520.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21265 0 0 0 51917 84 0 0 25 0 1 0 480404997 73674752 17508 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17508 603 41 0 17946 0
vsize: 71948
[startup+530.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21265 0 0 0 52917 84 0 0 25 0 1 0 480404997 73674752 17508 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17508 603 41 0 17946 0
vsize: 71948
[startup+540.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21265 0 0 0 53917 84 0 0 25 0 1 0 480404997 73674752 17508 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17508 603 41 0 17946 0
vsize: 71948
[startup+550.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6996
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21265 0 0 0 54917 84 0 0 25 0 1 0 480404997 73674752 17508 4294967295 134512640 134672761 3221224560 3221223744 134615617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17508 603 41 0 17946 0
vsize: 71948
[startup+560.003 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 7031
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21265 0 0 0 55917 84 0 0 25 0 1 0 480404997 73674752 17508 4294967295 134512640 134672761 3221224560 3221223600 134612587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17508 603 41 0 17946 0
vsize: 71948
[startup+570.003 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 7049
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21265 0 0 0 56917 84 0 0 25 0 1 0 480404997 73674752 17508 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17508 603 41 0 17946 0
vsize: 71948
[startup+580.004 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 7049
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21267 0 0 0 57918 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+590.003 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 7049
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 58918 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+600.003 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 7049
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 59918 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223600 134603545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+610.004 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 7049
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 60918 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+620.003 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 7049
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 61918 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+630.004 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 7049
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 62919 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+640.005 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 63919 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+650.004 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 64919 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+660.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 65919 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+670.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 66919 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+680.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 67920 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+690.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 68920 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+700.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21320 0 0 0 69920 84 0 0 25 0 1 0 480404997 73674752 17510 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17510 603 41 0 17946 0
vsize: 71948
[startup+710.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21322 0 0 0 70920 84 0 0 25 0 1 0 480404997 73674752 17512 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17987 17512 603 41 0 17946 0
vsize: 71948
[startup+720.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 21620 0 0 0 71920 84 0 0 25 0 1 0 480404997 74977280 17810 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18305 17810 603 41 0 18264 0
vsize: 73220
[startup+730.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22202 0 0 0 72918 86 0 0 25 0 1 0 480404997 77332480 18392 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18880 18392 603 41 0 18839 0
vsize: 75520
[startup+740.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22554 0 0 0 73918 87 0 0 25 0 1 0 480404997 78458880 18684 4294967295 134512640 134672761 3221224560 3221223552 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18684 603 41 0 19114 0
vsize: 76620
[startup+750.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22554 0 0 0 74918 87 0 0 25 0 1 0 480404997 78458880 18684 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18684 603 41 0 19114 0
vsize: 76620
[startup+760.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22554 0 0 0 75918 87 0 0 25 0 1 0 480404997 78458880 18684 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18684 603 41 0 19114 0
vsize: 76620
[startup+770.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22554 0 0 0 76918 87 0 0 25 0 1 0 480404997 78458880 18684 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18684 603 41 0 19114 0
vsize: 76620
[startup+780.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22554 0 0 0 77919 87 0 0 25 0 1 0 480404997 78458880 18684 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18684 603 41 0 19114 0
vsize: 76620
[startup+790.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22554 0 0 0 78919 87 0 0 25 0 1 0 480404997 78458880 18684 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18684 603 41 0 19114 0
vsize: 76620
[startup+800.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22554 0 0 0 79919 87 0 0 25 0 1 0 480404997 78458880 18684 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18684 603 41 0 19114 0
vsize: 76620
[startup+810.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22554 0 0 0 80919 87 0 0 25 0 1 0 480404997 78458880 18684 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18684 603 41 0 19114 0
vsize: 76620
[startup+820.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22555 0 0 0 81919 87 0 0 25 0 1 0 480404997 78458880 18685 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18685 603 41 0 19114 0
vsize: 76620
[startup+830.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22555 0 0 0 82919 87 0 0 25 0 1 0 480404997 78458880 18685 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18685 603 41 0 19114 0
vsize: 76620
[startup+840.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22555 0 0 0 83920 87 0 0 25 0 1 0 480404997 78458880 18685 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18685 603 41 0 19114 0
vsize: 76620
[startup+850.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22555 0 0 0 84920 87 0 0 25 0 1 0 480404997 78458880 18685 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18685 603 41 0 19114 0
vsize: 76620
[startup+860.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22555 0 0 0 85920 87 0 0 25 0 1 0 480404997 78458880 18685 4294967295 134512640 134672761 3221224560 3221223704 134616132 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18685 603 41 0 19114 0
vsize: 76620
[startup+870.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7051
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22555 0 0 0 86920 87 0 0 25 0 1 0 480404997 78458880 18685 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18685 603 41 0 19114 0
vsize: 76620
[startup+880.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 22820 0 0 0 87920 88 0 0 25 0 1 0 480404997 79646720 18950 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19445 18950 603 41 0 19404 0
vsize: 77780
[startup+890.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 23403 0 0 0 88919 89 0 0 25 0 1 0 480404997 82014208 19533 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20023 19533 603 41 0 19982 0
vsize: 80092
[startup+900.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24053 0 0 0 89917 91 0 0 25 0 1 0 480404997 84672512 20183 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20672 20183 603 41 0 20631 0
vsize: 82688
[startup+910.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24678 0 0 0 90915 92 0 0 25 0 1 0 480404997 87429120 20808 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21345 20808 603 41 0 21304 0
vsize: 85380
[startup+920.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 91915 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+930.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 92915 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+940.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 93916 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+950.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 94916 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+960.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 95916 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+970.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 96916 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+980.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 97916 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223704 134616247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+990.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 98917 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 99917 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 100917 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 101917 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 102917 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 103918 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 104918 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 105918 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 106918 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24875 0 0 0 107918 93 0 0 25 0 1 0 480404997 87941120 20940 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20940 603 41 0 21429 0
vsize: 85880
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 24876 0 0 0 108919 93 0 0 25 0 1 0 480404997 87941120 20941 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20941 603 41 0 21429 0
vsize: 85880
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 25721 0 0 0 109914 98 0 0 25 0 1 0 480404997 87941120 20943 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21470 20943 603 41 0 21429 0
vsize: 85880
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 25754 0 0 0 110913 98 0 0 25 0 1 0 480404997 87896064 20932 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21459 20932 603 41 0 21418 0
vsize: 85836
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 25754 0 0 0 111913 98 0 0 25 0 1 0 480404997 87896064 20932 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21459 20932 603 41 0 21418 0
vsize: 85836
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 25754 0 0 0 112914 98 0 0 25 0 1 0 480404997 87896064 20932 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21459 20932 603 41 0 21418 0
vsize: 85836
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 25754 0 0 0 113913 98 0 0 25 0 1 0 480404997 87896064 20932 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21459 20932 603 41 0 21418 0
vsize: 85836
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 25754 0 0 0 114914 98 0 0 25 0 1 0 480404997 87896064 20932 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21459 20932 603 41 0 21418 0
vsize: 85836
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 25754 0 0 0 115914 98 0 0 25 0 1 0 480404997 87896064 20932 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21459 20932 603 41 0 21418 0
vsize: 85836
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 25754 0 0 0 116914 98 0 0 25 0 1 0 480404997 87896064 20932 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21459 20932 603 41 0 21418 0
vsize: 85836
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 25754 0 0 0 117914 98 0 0 25 0 1 0 480404997 87896064 20932 4294967295 134512640 134672761 3221224560 3221223704 134616126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21459 20932 603 41 0 21418 0
vsize: 85836
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 25754 0 0 0 118915 98 0 0 25 0 1 0 480404997 87896064 20932 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21459 20932 603 41 0 21418 0
vsize: 85836
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7053
Raw data (stat): 6996 (minisat+) R 6995 3260 3259 0 -1 0 25754 0 0 0 119915 98 0 0 25 0 1 0 480404997 87896064 20932 4294967295 134512640 134672761 3221224560 3221223760 134610644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21459 20932 603 41 0 21418 0
vsize: 85836
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 7053
Raw data (stat): 6996 (minisat+) Z 6995 3260 3259 0 -1 12 25755 0 0 0 119915 103 0 0 25 0 1 0 480404997 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.07
CPU time (s): 1200.19
CPU user time (s): 1199.15
CPU system time (s): 1.03984
CPU usage (%): 100.01
Max. virtual memory (Kb): 85880
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####