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-2.opb
MD5SUM	409f1cf0658f035df65cb61f3e4f598e
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	27847
Number of constraints which are clauses	27847
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 5612

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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:      1034724 kB
MemFree:        707748 kB
Buffers:         34940 kB
Cached:         180292 kB
SwapCached:       1212 kB
Active:         146768 kB
Inactive:       148824 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        707492 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2316 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25660 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:10:41 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 4080 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27847 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 |   27847    55694 |    8354       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   27847    55694 |   11138       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.09783 s)
c ==============================================================================
c [1mFound solution: -24[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 |   56117   122092 |   16835       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/19331          
c   -- var.elim.:  2000/19331          
c   -- var.elim.:  3000/19331          
c   -- var.elim.:  4000/19331          
c   -- var.elim.:  5000/19331          
c   -- var.elim.:  6000/19331          
c   -- var.elim.:  7000/19331          
c   -- var.elim.:  8000/19331          
c   -- var.elim.:  9000/19331          
c   -- var.elim.:  10000/19331          
c   -- var.elim.:  11000/19331          
c   -- var.elim.:  12000/19331          
c   -- var.elim.:  13000/19331          
c   -- var.elim.:  14000/19331          
c   -- var.elim.:  15000/19331          
c   -- var.elim.:  16000/19331          
c   -- var.elim.:  17000/19331          
c   -- var.elim.:  18000/19331          
c   -- var.elim.:  19000/19331          
c   -- var.elim.:  19331/19331          
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/3869          
c   -- var.elim.:  2000/3869          
c   -- var.elim.:  3000/3869          
c   -- var.elim.:  3869/3869          
c   -- var.elim.:  368/368          
c |         0 |   36235   121913 |      --       0       --      -- |     --   | -19877/-164
c |         0 |   36235   121913 |   14494       0        0     nan |  0.000 % |
c |       100 |   36235   121913 |   15943     100     7380    73.8 | 52.610 % |
c |       250 |   36235   121913 |   17537     250    24858    99.4 | 52.609 % |
c |       476 |   36217   121759 |   19281     475    54042   113.8 | 52.701 % |
c ==============================================================================
c (current CPU-time: 39.393 s)
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       794 |   39198   130032 |   11759     793   109586   138.2 | 52.701 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6121          
c   -- var.elim.:  2000/6121          
c   -- var.elim.:  3000/6121          
c   -- var.elim.:  4000/6121          
c   -- var.elim.:  5000/6121          
c   -- var.elim.:  6000/6121          
c   -- var.elim.:  6121/6121          
c   -- var.elim.:  1000/2330          
c   -- var.elim.:  2000/2330          
c   -- var.elim.:  2330/2330          
c |       794 |   36268   129241 |      --     793       --      -- |     --   | -2930/-790
c |       794 |   36268   129241 |   14507     793   109586   138.2 | 52.701 % |
c |       896 |   36268   129241 |   15957     895   124196   138.8 | 57.572 % |
c |      1046 |   36268   129241 |   17553    1045   147458   141.1 | 57.572 % |
c ==============================================================================
c (current CPU-time: 47.8647 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 |      1238 |   40360   140506 |   12107    1237   177620   143.6 | 57.572 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7154          
c   -- var.elim.:  2000/7154          
c   -- var.elim.:  3000/7154          
c   -- var.elim.:  4000/7154          
c   -- var.elim.:  5000/7154          
c   -- var.elim.:  6000/7154          
c   -- var.elim.:  7000/7154          
c   -- var.elim.:  7154/7154          
c   -- var.elim.:  1000/3077          
c   -- var.elim.:  2000/3077          
c   -- var.elim.:  3000/3077          
c   -- var.elim.:  3077/3077          
c   -- var.elim.:  4/4          
c |      1238 |   36365   137393 |      --    1237       --      -- |     --   | -3989/-3100
c |      1238 |   36365   137393 |   14546    1237   177620   143.6 | 57.572 % |
c |      1338 |   36365   137393 |   16000    1337   201478   150.7 | 58.405 % |
c |      1488 |   36365   137393 |   17600    1487   215733   145.1 | 58.405 % |
c |      1713 |   36331   137039 |   19342    1708   242983   142.3 | 58.530 % |
c |      2050 |   36331   137039 |   21276    2045   285103   139.4 | 58.529 % |
c |      2556 |   36301   136723 |   23385    2547   366271   143.8 | 58.663 % |
c |      3316 |   36208   135828 |   25657    3304   485100   146.8 | 59.045 % |
c |      4455 |   36064   134395 |   28111    4429   747700   168.8 | 59.640 % |
c ==============================================================================
c (current CPU-time: 68.6286 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 |      5508 |   36964   135284 |   11089    5455   951126   174.4 | 59.640 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5404          
c   -- var.elim.:  2000/5404          
c   -- var.elim.:  3000/5404          
c   -- var.elim.:  4000/5404          
c   -- var.elim.:  5000/5404          
c   -- var.elim.:  5404/5404          
c   -- var.elim.:  1000/1040          
c   -- var.elim.:  1040/1040          
c   -- var.elim.:  2/2          
c |      5508 |   35803   130124 |      --    5455       --      -- |     --   | -1141/-3749
c |      5508 |   35803   130124 |   14321    4805   506080   105.3 | 59.640 % |
c |      5609 |   35765   129783 |   15736    4904   523461   106.7 | 60.951 % |
c |      5759 |   35711   129357 |   17284    5041   544500   108.0 | 61.137 % |
c |      5984 |   35711   129357 |   19012    5266   585074   111.1 | 61.137 % |
c |      6321 |   35711   129357 |   20913    5603   673444   120.2 | 61.137 % |
c |      6828 |   35643   128764 |   22961    6105   778996   127.6 | 61.438 % |
c |      7587 |   35593   128242 |   25222    6851   947237   138.3 | 61.659 % |
c |      8726 |   35387   126387 |   27583    7955  1252575   157.5 | 62.571 % |
c ==============================================================================
c (current CPU-time: 84.0622 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 |      9128 |   36457   128779 |   10937    8338  1326901   159.1 | 62.571 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5118          
c   -- var.elim.:  2000/5118          
c   -- var.elim.:  3000/5118          
c   -- var.elim.:  4000/5118          
c   -- var.elim.:  5000/5118          
c   -- var.elim.:  5118/5118          
c   -- var.elim.:  1000/1049          
c   -- var.elim.:  1049/1049          
c |      9128 |   35313   126704 |      --    8338       --      -- |     --   | -1144/-2074
c |      9128 |   35313   126704 |   14125    8338  1326901   159.1 | 62.571 % |
c |      9228 |   35289   126463 |   15527    8437  1347624   159.7 | 63.383 % |
c |      9378 |   35203   125635 |   17038    8529  1353604   158.7 | 63.761 % |
c |      9604 |   35203   125635 |   18742    8755  1388335   158.6 | 63.761 % |
c |      9941 |   35203   125635 |   20616    9092  1443829   158.8 | 63.761 % |
c |     10447 |   35203   125635 |   22677    9598  1556268   162.1 | 63.761 % |
c |     11206 |   35079   124486 |   24857   10316  1728682   167.6 | 64.306 % |
c |     12345 |   35007   123721 |   27287   11440  2006539   175.4 | 64.622 % |
c |     14053 |   34945   123025 |   29963   13113  2438571   186.0 | 64.886 % |
c |     16615 |   34615   119966 |   32648   15550  2924835   188.1 | 66.318 % |
c |     20459 |   34460   118517 |   35752   19348  3837785   198.4 | 66.968 % |
c |     26225 |   34094   114797 |   38909   25002  5305831   212.2 | 68.541 % |
c |     34874 |   33633   106887 |   42221   33464  7925738   236.8 | 70.466 % |
c ==============================================================================
c (current CPU-time: 183.911 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 |     38763 |   34235   106878 |   10270   37296  9163997   245.7 | 70.466 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4076          
c   -- var.elim.:  2000/4076          
c   -- var.elim.:  3000/4076          
c   -- var.elim.:  4000/4076          
c   -- var.elim.:  4076/4076          
c   -- var.elim.:  1000/1910          
c   -- var.elim.:  1910/1910          
c   -- var.elim.:  1000/1059          
c   -- var.elim.:  1059/1059          
c |     38763 |   33308    99097 |      --   37296       --      -- |     --   | -897/-3012
c |     38763 |   33308    99097 |   13323   27231  3344817   122.8 | 70.466 % |
c |     38863 |   33306    99077 |   14654   11908  1031719    86.6 | 72.307 % |
c |     39013 |   33306    99077 |   16120   12058  1058540    87.8 | 72.307 % |
c |     39238 |   33306    99077 |   17732   12283  1106448    90.1 | 72.307 % |
c |     39575 |   33306    99077 |   19505   12620  1210413    95.9 | 72.307 % |
c |     40081 |   33306    99077 |   21455   13126  1350205   102.9 | 72.307 % |
c |     40841 |   33264    98763 |   23571   13876  1487989   107.2 | 72.480 % |
c |     41980 |   33234    98522 |   25905   15006  1750061   116.6 | 72.602 % |
c |     43689 |   33234    98522 |   28496   16715  2137835   127.9 | 72.602 % |
c |     46252 |   33234    98522 |   31345   19278  2889509   149.9 | 72.602 % |
c |     50096 |   33197    98175 |   34441   23112  3963958   171.5 | 72.749 % |
c |     55863 |   32981    96218 |   37639   28847  5405803   187.4 | 73.660 % |
c |     64512 |   32729    94099 |   41087   37364  7521912   201.3 | 74.692 % |
c |     77489 |   32366    91043 |   44694   50150 10645711   212.3 | 76.202 % |
c |     96950 |   31825    86736 |   48342   33498  6552759   195.6 | 78.413 % |
c |    126142 |   31237    82423 |   52193   24202  3605631   149.0 | 80.850 % |
c ==============================================================================
c (current CPU-time: 507.527 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 |    136961 |   32974    86613 |    9892   34997  6322247   180.7 | 80.850 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3918          
c   -- var.elim.:  2000/3918          
c   -- var.elim.:  3000/3918          
c   -- var.elim.:  3918/3918          
c   -- var.elim.:  1000/1132          
c   -- var.elim.:  1132/1132          
c   -- var.elim.:  4/4          
c |    136961 |   31229    84045 |      --   34997       --      -- |     --   | -1737/-2551
c |    136961 |   31229    84045 |   12491   28192  3976532   141.1 | 80.850 % |
c |    137062 |   31229    84045 |   13740   14916  2147303   144.0 | 85.364 % |
c |    137212 |   31229    84045 |   15114   15066  2177522   144.5 | 85.364 % |
c |    137437 |   31229    84045 |   16626   15291  2214756   144.8 | 85.364 % |
c |    137774 |   31229    84045 |   18288   15628  2285887   146.3 | 85.364 % |
c |    138281 |   31229    84045 |   20117   16135  2394456   148.4 | 85.364 % |
c |    139041 |   31229    84045 |   22129   16895  2545891   150.7 | 85.364 % |
c |    140180 |   31229    84045 |   24342   18034  2773515   153.8 | 85.364 % |
c |    141889 |   31229    84045 |   26776   19743  3157122   159.9 | 85.364 % |
c |    144451 |   31194    83763 |   29421   22297  3752147   168.3 | 85.477 % |
c |    148296 |   31194    83763 |   32363   26142  4561475   174.5 | 85.477 % |
c |    154062 |   31107    83143 |   35500   31902  6012226   188.5 | 85.752 % |
c |    162711 |   31084    82957 |   39021   40543  8025727   198.0 | 85.825 % |
c |    175686 |   30879    81241 |   42641   19150  2911522   152.0 | 86.500 % |
c |    195149 |   30746    80130 |   46703   38531  7468689   193.8 | 86.935 % |
c |    224341 |   30702    79745 |   51299   25196  4714823   187.1 | 87.069 % |
c |    268132 |   30467    77819 |   55998   19604  4016306   204.9 | 87.844 % |
c |    333816 |   30240    75930 |   61138   32254  6508990   201.8 | 88.593 % |
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 -C#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.77 0.92 0.89 2/53 13796
Raw data (stat): 13796 (runsolver) R 13795 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480400963 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0016 s]
Raw data (loadavg): 0.81 0.92 0.89 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 3648 0 0 0 984 13 0 0 25 0 1 0 480400963 17813504 3626 4294967295 134512640 134672761 3221224560 3221222592 134566560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4349 3626 603 41 0 4308 0
vsize: 17396
[startup+20.003 s]
Raw data (loadavg): 0.84 0.93 0.90 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 3667 0 0 0 1983 14 0 0 25 0 1 0 480400963 17956864 3645 4294967295 134512640 134672761 3221224560 3221222992 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3645 603 41 0 4343 0
vsize: 17536
[startup+30.0037 s]
Raw data (loadavg): 0.86 0.93 0.90 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 3698 0 0 0 2983 14 0 0 25 0 1 0 480400963 18153472 3676 4294967295 134512640 134672761 3221224560 3221223008 134643948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4432 3676 603 41 0 4391 0
vsize: 17728
[startup+40.0045 s]
Raw data (loadavg): 0.88 0.93 0.90 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 4607 0 0 0 3980 17 0 0 25 0 1 0 480400963 19542016 4092 4294967295 134512640 134672761 3221224560 3221223104 134621086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4771 4092 603 41 0 4730 0
vsize: 19084
[startup+50.0051 s]
Raw data (loadavg): 0.90 0.93 0.90 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 5368 0 0 0 4952 33 0 0 25 0 1 0 480400963 19582976 4125 4294967295 134512640 134672761 3221224560 3221222960 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4781 4125 603 41 0 4740 0
vsize: 19124
[startup+60.0061 s]
Raw data (loadavg): 0.91 0.93 0.90 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 5368 0 0 0 5944 42 0 0 25 0 1 0 480400963 18714624 4015 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4569 4015 603 41 0 4528 0
vsize: 18276
[startup+70.0068 s]
Raw data (loadavg): 0.93 0.94 0.90 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 6957 0 0 0 6936 49 0 0 25 0 1 0 480400963 23461888 5140 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5728 5140 603 41 0 5687 0
vsize: 22912
[startup+80.0077 s]
Raw data (loadavg): 0.94 0.94 0.90 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 6957 0 0 0 7934 51 0 0 25 0 1 0 480400963 23461888 5140 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5728 5140 603 41 0 5687 0
vsize: 22912
[startup+90.0086 s]
Raw data (loadavg): 0.95 0.94 0.90 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 7947 0 0 0 8925 60 0 0 25 0 1 0 480400963 25444352 5676 4294967295 134512640 134672761 3221224560 3221223008 134643987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6212 5676 603 41 0 6171 0
vsize: 24848
[startup+100.009 s]
Raw data (loadavg): 0.95 0.94 0.90 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 8147 0 0 0 9924 61 0 0 25 0 1 0 480400963 26230784 5876 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6404 5876 603 41 0 6363 0
vsize: 25616
[startup+110.01 s]
Raw data (loadavg): 0.96 0.94 0.90 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 8965 0 0 0 10922 63 0 0 25 0 1 0 480400963 29515776 6694 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7206 6694 603 41 0 7165 0
vsize: 28824
[startup+120.011 s]
Raw data (loadavg): 0.97 0.94 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 9930 0 0 0 11921 65 0 0 25 0 1 0 480400963 33615872 7659 4294967295 134512640 134672761 3221224560 3221223704 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8207 7659 603 41 0 8166 0
vsize: 32828
[startup+130.011 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 10774 0 0 0 12920 66 0 0 25 0 1 0 480400963 37003264 8503 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9034 8503 603 41 0 8993 0
vsize: 36136
[startup+140.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 11653 0 0 0 13918 68 0 0 25 0 1 0 480400963 40644608 9382 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9923 9382 603 41 0 9882 0
vsize: 39692
[startup+150.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 12726 0 0 0 14916 70 0 0 25 0 1 0 480400963 44949504 10455 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10974 10455 603 41 0 10933 0
vsize: 43896
[startup+160.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 13520 0 0 0 15913 73 0 0 25 0 1 0 480400963 48209920 11249 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11770 11249 603 41 0 11729 0
vsize: 47080
[startup+170.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 14228 0 0 0 16912 75 0 0 25 0 1 0 480400963 51200000 11957 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12500 11957 603 41 0 12459 0
vsize: 50000
[startup+180.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 15147 0 0 0 17909 78 0 0 25 0 1 0 480400963 55042048 12876 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13438 12876 603 41 0 13397 0
vsize: 53752
[startup+190.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 18898 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14422 13864 603 41 0 14381 0
vsize: 57688
[startup+200.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 19898 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14422 13864 603 41 0 14381 0
vsize: 57688
[startup+210.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 20898 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14422 13864 603 41 0 14381 0
vsize: 57688
[startup+220.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 21898 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14422 13864 603 41 0 14381 0
vsize: 57688
[startup+230.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 22899 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14422 13864 603 41 0 14381 0
vsize: 57688
[startup+240.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 23899 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14422 13864 603 41 0 14381 0
vsize: 57688
[startup+250.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 24899 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14422 13864 603 41 0 14381 0
vsize: 57688
[startup+260.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 25899 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14422 13864 603 41 0 14381 0
vsize: 57688
[startup+270.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16639 0 0 0 26899 89 0 0 25 0 1 0 480400963 59072512 13866 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14422 13866 603 41 0 14381 0
vsize: 57688
[startup+280.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16642 0 0 0 27900 89 0 0 25 0 1 0 480400963 59072512 13869 4294967295 134512640 134672761 3221224560 3221223336 1075351081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14422 13869 603 41 0 14381 0
vsize: 57688
[startup+290.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16644 0 0 0 28900 89 0 0 25 0 1 0 480400963 59072512 13871 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14422 13871 603 41 0 14381 0
vsize: 57688
[startup+300.04 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16814 0 0 0 29901 89 0 0 25 0 1 0 480400963 59723776 14041 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14581 14041 603 41 0 14540 0
vsize: 58324
[startup+310.041 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 17402 0 0 0 30900 91 0 0 25 0 1 0 480400963 62074880 14629 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15155 14629 603 41 0 15114 0
vsize: 60620
[startup+320.042 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 17973 0 0 0 31899 92 0 0 25 0 1 0 480400963 64446464 15200 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15734 15200 603 41 0 15693 0
vsize: 62936
[startup+330.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 18391 0 0 0 32898 93 0 0 25 0 1 0 480400963 66150400 15618 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16150 15618 603 41 0 16109 0
vsize: 64600
[startup+340.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19096 0 0 0 33897 95 0 0 25 0 1 0 480400963 68947968 16323 4294967295 134512640 134672761 3221224560 3221223008 134645372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16833 16323 603 41 0 16792 0
vsize: 67332
[startup+350.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 34897 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+360.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 35897 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+370.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 36897 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223600 134612829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+380.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 37898 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+390.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 38898 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+400.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 39898 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223600 134614207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+410.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 40898 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+420.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 41899 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+430.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 42899 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+440.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 43899 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+450.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 44899 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+460.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 45900 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223704 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16865 16336 603 41 0 16824 0
vsize: 67460
[startup+470.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19246 0 0 0 46899 95 0 0 25 0 1 0 480400963 69607424 16450 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16994 16450 603 41 0 16953 0
vsize: 67976
[startup+480.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19306 0 0 0 47900 95 0 0 25 0 1 0 480400963 69672960 16485 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17010 16485 603 41 0 16969 0
vsize: 68040
[startup+490.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19306 0 0 0 48900 95 0 0 25 0 1 0 480400963 69672960 16485 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17010 16485 603 41 0 16969 0
vsize: 68040
[startup+500.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19306 0 0 0 49900 95 0 0 25 0 1 0 480400963 69672960 16485 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17010 16485 603 41 0 16969 0
vsize: 68040
[startup+510.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20390 0 0 0 50890 106 0 0 25 0 1 0 480400963 73072640 16799 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17840 16799 603 41 0 17799 0
vsize: 71360
[startup+520.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 51889 106 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+530.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 52889 106 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+540.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 53890 106 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+550.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 54890 106 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+560.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13796
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 55890 106 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+570.064 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 13839
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 56889 107 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+580.064 s]
Raw data (loadavg): 1.06 0.99 0.91 2/53 13849
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 57889 107 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+590.065 s]
Raw data (loadavg): 1.05 0.99 0.91 2/53 13849
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 58888 107 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223704 134616111 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+600.066 s]
Raw data (loadavg): 1.04 0.99 0.91 2/53 13849
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 59888 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+610.066 s]
Raw data (loadavg): 1.03 0.99 0.91 2/53 13849
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 60888 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+620.067 s]
Raw data (loadavg): 1.03 0.99 0.91 2/53 13849
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 61888 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+630.068 s]
Raw data (loadavg): 1.02 0.99 0.91 2/53 13849
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 62888 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223656 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+640.068 s]
Raw data (loadavg): 1.02 0.99 0.91 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 63888 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+650.069 s]
Raw data (loadavg): 1.02 0.99 0.91 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 64889 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+660.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 65889 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+670.072 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 66889 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+680.072 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 67890 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+690.072 s]
Raw data (loadavg): 1.09 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 68890 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+700.073 s]
Raw data (loadavg): 1.07 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 69890 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+710.074 s]
Raw data (loadavg): 1.06 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 70890 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+720.075 s]
Raw data (loadavg): 1.05 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 71890 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+730.076 s]
Raw data (loadavg): 1.04 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 72891 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+740.076 s]
Raw data (loadavg): 1.04 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 73891 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17840 16803 603 41 0 17799 0
vsize: 71360
[startup+750.077 s]
Raw data (loadavg): 1.03 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20731 0 0 0 74890 108 0 0 25 0 1 0 480400963 74518528 17140 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18193 17140 603 41 0 18152 0
vsize: 72772
[startup+760.078 s]
Raw data (loadavg): 1.02 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21156 0 0 0 75890 109 0 0 25 0 1 0 480400963 76226560 17565 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18610 17565 603 41 0 18569 0
vsize: 74440
[startup+770.079 s]
Raw data (loadavg): 1.02 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 76889 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+780.08 s]
Raw data (loadavg): 1.02 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 77890 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+790.081 s]
Raw data (loadavg): 1.01 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 78890 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+800.082 s]
Raw data (loadavg): 1.01 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 79890 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+810.083 s]
Raw data (loadavg): 1.01 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 80890 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+820.083 s]
Raw data (loadavg): 1.01 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 81891 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+830.084 s]
Raw data (loadavg): 1.01 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 82891 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+840.084 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 83891 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+850.086 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 84891 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+860.086 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 85892 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+870.087 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 86892 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+880.088 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 87892 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+890.088 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 88892 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 18015 603 41 0 19008 0
vsize: 76196
[startup+900.089 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 22063 0 0 0 89891 111 0 0 25 0 1 0 480400963 79724544 18412 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19464 18412 603 41 0 19423 0
vsize: 77856
[startup+910.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 22735 0 0 0 90890 113 0 0 25 0 1 0 480400963 82481152 19084 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20137 19084 603 41 0 20096 0
vsize: 80548
[startup+920.091 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23371 0 0 0 91889 114 0 0 25 0 1 0 480400963 85114880 19720 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20780 19720 603 41 0 20739 0
vsize: 83120
[startup+930.092 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13851
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 92888 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+940.093 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 93888 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+950.093 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 94888 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+960.099 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 95889 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+970.101 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 96889 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+980.101 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 97890 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+990.101 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 98890 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 99890 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+1010.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 100890 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 101891 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 102891 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 103891 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+1050.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 104891 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+1060.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 105892 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+1070.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 106892 116 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223600 134614280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+1080.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 107892 116 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21189 20098 603 41 0 21148 0
vsize: 84756
[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24260 0 0 0 108891 117 0 0 25 0 1 0 480400963 88621056 20544 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21636 20544 603 41 0 21595 0
vsize: 86544
[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24634 0 0 0 109889 118 0 0 25 0 1 0 480400963 90202112 20918 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22022 20918 603 41 0 21981 0
vsize: 88088
[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 110889 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 21087 603 41 0 22136 0
vsize: 88708
[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 111889 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 21087 603 41 0 22136 0
vsize: 88708
[startup+1130.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 112890 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223664 134603768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 21087 603 41 0 22136 0
vsize: 88708
[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 113890 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 21087 603 41 0 22136 0
vsize: 88708
[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 114890 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 21087 603 41 0 22136 0
vsize: 88708
[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 115890 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 21087 603 41 0 22136 0
vsize: 88708
[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 116891 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 21087 603 41 0 22136 0
vsize: 88708
[startup+1180.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 117891 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 21087 603 41 0 22136 0
vsize: 88708
[startup+1190.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24873 0 0 0 118891 119 0 0 25 0 1 0 480400963 90836992 21088 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 21088 603 41 0 22136 0
vsize: 88708
[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.92 2/53 13853
Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24873 0 0 0 119891 119 0 0 25 0 1 0 480400963 90836992 21088 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 21088 603 41 0 22136 0
vsize: 88708
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 13853
Raw data (stat): 13796 (minisat+) Z 13795 7987 7986 0 -1 12 24874 0 0 0 119892 125 0 0 25 0 1 0 480400963 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.19
CPU time (s): 1200.18
CPU user time (s): 1198.92
CPU system time (s): 1.25681
CPU usage (%): 99.9992
Max. virtual memory (Kb): 88708
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####