↑ Up

SPASS-SCL---0.1.SAT-Ass.s

View TPTP
Problem
Process solution in
SystemOnTSTP
Download .tgz
%------------------------------------------------------------------------------
% File     : SPASS-SCL---0.1
% Problem  : GRP123-7.005 : TPTP v9.2.1. Released v1.2.0.
% Transfm  : none
% Format   : tptp
% Command  : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n021.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu May  7 07:23:02 PM UTC 2026

% Result   : Satisfiable 36.74s 7.89s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : GRP123-7.005 : TPTP v9.2.1. Released v1.2.0.
% 0.11/0.13  % Command  : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34  % Computer : n021.cluster.edu
% 0.17/0.34  % Model    : x86_64 x86_64
% 0.17/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34  % Memory   : 8042.1875MB
% 0.17/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34  % CPULimit : 300
% 0.17/0.34  % WCLimit  : 300
% 0.17/0.34  % DateTime : Thu May  7 12:02:28 EDT 2026
% 0.17/0.34  % CPUTime  : 
% 0.17/0.34  SPASS-SCL-FOL version:
% 0.20/0.43  SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 36.74/7.89  Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.74/7.89  Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.74/7.89  Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.74/7.89  Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.74/7.89  Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.74/7.89  Execution resolution_3 ended with status: satisfiable
% 36.74/7.89  Used heuristic: resolution_3
% 36.74/7.89  
% 36.74/7.89   Input Clauses:
% 36.74/7.89  
% 36.74/7.89   Predicates: next greater product group_element equalish product1 product2 
% 36.74/7.89   Fol Constants: e_1 e_2 e_3 e_4 e_5 
% 36.74/7.89   Fol Functions: 
% 36.74/7.89   Problem Properties:
% 36.74/7.89   This is a Bernays Schoenfinkel problem.
% 36.74/7.89  
% 36.74/7.89   After reduction:  Problem Properties:
% 36.74/7.89   This is a Bernays Schoenfinkel problem.
% 36.74/7.89  
% 36.74/7.89  
% 36.74/7.89   Reduced Input Clauses:
% 36.74/7.89  
% 36.74/7.89   Most General Atoms: product(x0,e_1,x1) next(x0,x2) greater(x1,x2) group_element(x1) equalish(x0,x3) product1(x2,x1,x3) product2(x3,x0,x1) 
% 36.74/7.89  
% 36.74/7.89  === Starting SPASS-SCL-FOL A Little Less Naive, considering 14 atoms initially, heuristics mode: resolution_3 ===
% 36.74/7.89  
% 36.74/7.89  === Backtracking. Learning clause 52:1:1:[42.1,45.1]:Top:  -> equalish(x0,x0)
% 36.74/7.89  === Clause set with instances from active satisfied. Growing active. New size: 68
% 36.74/7.89  === Clause set with instances from active satisfied. Growing active. New size: 132
% 36.74/7.89  === Clause set with instances from active satisfied. Growing active. New size: 196
% 36.74/7.89  === Clause set with instances from active satisfied. Growing active. New size: 260
% 36.74/7.89  === Backtracking. Learning clause 53:4:5:[51.3,49.1]:TopTopTopTopTop: product1(x0,x1,x2),product1(x2,x1,x3),product2(x4,x0,x1) -> equalish(x3,x4)
% 36.74/7.89  === Clause set with instances from active satisfied. Growing active. New size: 324
% 36.74/7.89  === Backtracking. Learning clause 57:28:6:[20.0,54.1,19.0,55.6,16.0,56.7,41.6,53.2,44.1,46.7,53.3,41.4,43.2,41.7,51.2,41.3]:TopTopTopTopTopTop: group_element(x0),product1(e_1,e_5,x0),product1(x1,e_5,e_5),group_element(x2),product1(e_2,e_4,x3),group_element(x4),group_element(x5) -> product1(x0,e_5,e_1),product1(x0,e_5,e_2),product1(x0,e_5,e_3),equalish(e_4,x2),equalish(x0,x1),product2(x2,e_1,e_1),product2(x2,e_1,e_2),product2(x2,e_1,e_3),equalish(x3,x2),product1(e_1,e_4,e_1),product1(e_1,e_4,e_3),product1(e_1,e_4,e_4),equalish(x5,e_4),product1(e_1,x5,e_1),product1(e_1,x5,e_3),product1(e_1,x5,e_4),product2(e_2,x4,x5),product1(x4,x5,e_2),product1(x4,x5,e_3),product1(x4,x5,e_4),product1(x4,x5,e_5)
% 36.74/7.89  === Backtracking. Learning clause 63:38:8:[18.0,58.0,16.0,59.6,20.0,60.7,17.0,61.8,25.0,62.37,47.2,51.3,51.3,57.25,44.1,41.6,44.1,57.28,44.2,41.5,51.1,44.2,41.6,43.2,51.2]:TopTopTopTopTopTopTopTop: product1(x0,e_5,e_5),group_element(x1),product1(e_2,e_4,x2),group_element(x3),product1(x4,e_5,e_1),group_element(x5),product1(e_2,x6,e_1),product1(x7,e_5,e_1) -> equalish(e_5,x5),product2(e_2,e_1,x5),equalish(e_1,x3),product1(e_3,e_5,e_2),product1(e_3,e_5,e_3),equalish(e_4,x1),equalish(e_3,x0),product2(x1,e_1,e_1),product2(x1,e_1,e_2),product2(x1,e_1,e_3),equalish(x2,x1),product1(e_1,e_4,e_1),product1(e_1,e_4,e_3),product1(e_1,e_4,e_4),equalish(x5,e_4),product1(e_1,x5,e_1),product1(e_1,x5,e_3),product2(e_2,x3,x5),product1(x3,x5,e_3),product1(x3,x5,e_4),equalish(x4,e_3),product1(e_1,e_5,e_1),product1(e_1,e_5,e_4),product1(e_1,e_5,e_5),product2(e_4,x3,x5),product1(e_2,x5,e_2),product1(e_2,x5,e_3),product1(e_2,x5,e_5),equalish(x6,x5),product2(e_2,x7,e_5)
% 36.74/7.89  === Backtracking. Learning clause 64:10:5:[41.5,43.1,44.1,44.2]:TopTopTopTopTop: group_element(x0),group_element(x1),product1(x0,x2,e_3),product1(x3,x1,e_5),product1(x4,x1,e_4) -> product1(x0,x1,e_1),product1(x0,x1,e_2),equalish(x1,x2),equalish(x0,x3),equalish(x4,x0)
% 36.74/7.89  === Conflict found: 64:10:5:[41.5,43.1,44.1,44.2]:TopTopTopTopTop: group_element(x0),group_element(x1),product1(x0,x2,e_3),product1(x3,x1,e_5),product1(x4,x1,e_4) -> product1(x0,x1,e_1),product1(x0,x1,e_2),equalish(x1,x2),equalish(x0,x3),equalish(x4,x0) {x0 -> e_3, x1 -> e_4, x2 -> e_3, x3 -> e_1, x4 -> e_4}
% 36.74/7.89  === Backtracking. Learning clause 76:44:7:[16.0,65.2,18.0,66.3,20.0,67.4,17.0,68.10,19.0,69.11,29.0,70.14,36.0,71.16,40.0,72.19,30.0,73.21,26.0,74.39,21.0,75.50,64.6,43.1,41.7,43.1,41.4,51.1,41.3,64.5,63.5,44.1,44.1,41.5]:TopTopTopTopTopTopTop: product1(e_3,x0,e_3),product1(x1,e_4,e_4),product1(x2,e_5,e_5),group_element(x3),group_element(x4),group_element(x5),product1(x6,e_5,e_5) -> product1(e_3,e_4,e_2),equalish(e_4,x0),equalish(x1,e_3),product2(e_1,e_1,e_5),product1(e_2,e_5,e_2),equalish(e_2,x2),product2(e_2,e_1,x5),equalish(e_1,x4),product1(e_3,e_5,e_2),product1(e_3,e_5,e_3),equalish(e_4,x3),product2(x3,e_1,e_1),product2(x3,e_1,e_2),product2(x3,e_1,e_3),equalish(e_3,x3),product1(e_1,e_4,e_1),product1(e_1,e_4,e_4),equalish(x5,e_4),product1(e_1,x5,e_1),product1(e_1,x5,e_3),product2(e_2,x4,x5),product1(x4,x5,e_3),product1(x4,x5,e_4),product1(e_1,e_5,e_1),product1(e_1,e_5,e_4),product1(e_1,e_5,e_5),product2(e_4,x4,x5),product1(e_2,x5,e_2),product1(e_2,x5,e_3),product1(e_2,x5,e_5),equalish(e_5,x5),product2(e_2,e_2,e_5),equalish(e_3,x6),product1(e_2,e_4,e_1),product1(e_2,e_4,e_2),product1(e_2,e_4,e_4),product1(e_2,e_4,e_5)
% 36.74/7.89  === Conflict found: 53:4:5:[51.3,49.1]:TopTopTopTopTop: product1(x0,x1,x2),product1(x2,x1,x3),product2(x4,x0,x1) -> equalish(x3,x4) {x0 -> e_1, x1 -> e_4, x2 -> e_3, x3 -> e_5, x4 -> e_2}
% 36.74/7.89  === Backtracking. Learning clause 89:54:11:[17.0,77.1,20.0,78.3,16.0,79.6,18.0,80.7,19.0,81.8,43.0,82.17,44.1,83.18,29.0,84.26,30.0,85.27,40.0,86.29,44.1,87.54,44.0,88.55,53.2,41.7,46.6,53.3,41.5,44.1,44.2,64.7,41.5,64.4,44.1,51.2,43.1,76.41]:TopTopTopTopTopTopTopTopTopTopTop: group_element(x0),product1(x1,e_5,e_4),product1(x2,e_5,e_5),product1(x3,e_5,e_4),product1(e_3,x4,e_3),product1(x5,e_4,e_4),product1(x6,e_5,e_5),group_element(x7),group_element(x8),group_element(x9),product1(x10,e_5,e_5) -> equalish(e_5,x0),product2(x0,e_1,e_1),product2(x0,e_1,e_2),product2(x0,e_1,e_3),equalish(e_3,x0),equalish(x1,e_2),equalish(e_1,x2),equalish(x3,e_1),product2(e_2,e_2,e_4),product1(e_3,e_4,e_2),equalish(e_4,x4),equalish(x5,e_3),product2(e_1,e_1,e_5),product1(e_2,e_5,e_2),equalish(e_2,x6),product2(e_2,e_1,x9),equalish(e_1,x8),product1(e_3,e_5,e_2),product1(e_3,e_5,e_3),equalish(e_4,x7),product2(x7,e_1,e_1),product2(x7,e_1,e_2),product2(x7,e_1,e_3),equalish(e_3,x7),product1(e_1,e_4,e_1),product1(e_1,e_4,e_4),equalish(x9,e_4),product1(e_1,x9,e_1),product1(e_1,x9,e_3),product2(e_2,x8,x9),product1(x8,x9,e_3),product1(x8,x9,e_4),product1(e_1,e_5,e_1),product2(e_4,x8,x9),product1(e_2,x9,e_2),product1(e_2,x9,e_3),product1(e_2,x9,e_5),equalish(e_5,x9),product2(e_2,e_2,e_5),equalish(e_3,x10),product1(e_2,e_4,e_2),product1(e_2,e_4,e_4),product1(e_2,e_4,e_5)
% 36.74/7.89  === Backtracking. Learning clause 100:56:14:[20.0,90.1,16.0,91.2,18.0,92.3,19.0,93.4,17.0,94.11,43.0,95.25,44.1,96.26,29.0,97.27,26.0,98.28,40.0,99.30,41.6,53.2,53.2,46.7,53.3,41.7,41.4,43.1,44.1,41.5,64.4,44.2,51.2,43.1,76.41,43.2,43.2,41.7,53.2,43.2,53.2,43.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: group_element(x0),product1(e_3,x1,e_3),product1(x2,e_4,e_4),product1(x3,e_5,e_5),group_element(x4),group_element(x5),product1(x6,e_5,e_5),group_element(x7),product1(x8,x7,e_2),product2(x9,x8,x7),product1(e_3,x10,e_2),product1(x11,x7,e_2),product2(x12,x11,x7),product1(e_3,x13,e_2) -> equalish(e_4,x0),equalish(e_3,x0),product2(x0,e_1,e_1),product2(x0,e_1,e_2),product2(x0,e_1,e_3),equalish(e_5,x0),product2(e_2,e_2,e_4),equalish(e_4,x1),equalish(x2,e_3),product2(e_1,e_1,e_5),product1(e_2,e_5,e_2),equalish(e_2,x3),product2(e_2,e_1,x5),equalish(e_1,x4),product1(e_3,e_5,e_3),product1(e_1,e_4,e_1),product1(e_1,e_4,e_4),equalish(x5,e_4),product1(e_1,x5,e_1),product1(e_1,x5,e_3),product2(e_2,x4,x5),product1(x4,x5,e_3),product1(x4,x5,e_4),product1(e_1,e_5,e_1),product1(e_1,e_5,e_4),product1(e_1,e_5,e_5),product2(e_4,x4,x5),product1(e_2,x5,e_2),product1(e_2,x5,e_3),equalish(e_5,x5),product2(e_2,e_2,e_5),equalish(e_3,x6),product1(e_2,e_4,e_2),product1(e_2,e_4,e_4),equalish(x7,x5),equalish(x7,e_4),product1(e_2,x7,e_1),product1(e_2,x7,e_2),equalish(e_4,x9),equalish(x10,e_4),equalish(e_3,x12),equalish(x13,e_5)
% 36.74/7.89  === Backtracking. Learning clause 102:13:4:[17.0,101.0,41.5,53.2,53.2,41.4]:TopTopTopTop: product2(x0,x1,x2),product2(x3,x1,x2),group_element(x1),group_element(x2) -> product1(e_2,x2,e_1),product1(e_2,x2,e_2),product1(e_2,x2,e_4),equalish(e_3,x0),equalish(e_5,x3),product1(x1,x2,e_1),product1(x1,x2,e_3),product1(x1,x2,e_4),product1(x1,x2,e_5)
% 36.74/7.89  === Backtracking. Learning clause 103:4:5:[51.3,47.1]:TopTopTopTopTop: product1(x0,x1,x2),product1(x2,x1,x3),product2(x3,x0,x4) -> equalish(x1,x4)
% 36.74/7.89  === Backtracking. Learning clause 104:2:2:[42.3,29.1]:TopTop: product1(x0,x1,e_3),product1(x0,x1,e_1) -> 
% 36.74/7.89  === Backtracking. Learning clause 105:2:2:[42.3,31.1]:TopTop: product1(x0,x1,e_3),product1(x0,x1,e_4) -> 
% 36.74/7.89  === Backtracking. Learning clause 106:2:2:[42.3,32.1]:TopTop: product1(x0,x1,e_3),product1(x0,x1,e_5) -> 
% 36.74/7.89  === Backtracking. Learning clause 107:2:2:[47.3,36.1]:TopTop: product2(x0,x1,e_4),product2(x0,x1,e_5) -> 
% 36.74/7.89  === Backtracking. Learning clause 108:4:0:[51.1,41.4,48.2,44.1,45.1,27.1,17.1,21.1,19.1]:: product2(e_2,e_1,e_4) -> product1(e_2,e_4,e_1),product1(e_2,e_4,e_3),product1(e_2,e_4,e_5)
% 36.74/7.89  === Backtracking. Learning clause 109:6:1:[41.2,20.1,43.2,28.1]:Top: group_element(x0),product1(x0,e_2,e_5) -> product1(x0,e_5,e_1),product1(x0,e_5,e_2),product1(x0,e_5,e_3),product1(x0,e_5,e_4)
% 36.74/7.89  === Backtracking. Learning clause 110:8:3:[44.1,45.1,41.7,20.1,43.1,44.2]:TopTopTop: group_element(x0),product1(x0,x1,e_1),product1(x2,e_5,e_4) -> equalish(e_5,x0),product1(x0,e_5,e_2),product1(x0,e_5,e_3),equalish(e_5,x1),equalish(x2,x0)
% 36.74/7.89  === Backtracking. Learning clause 113:5:1:[16.0,111.1,37.0,112.4,44.3,21.1,110.6,29.1]:Top: product1(e_2,e_5,e_3),product1(e_1,x0,e_1),product1(e_3,e_5,e_4) -> product1(e_1,e_5,e_2),equalish(e_5,x0)
% 36.74/7.89  === Conflict found: 103:4:5:[51.3,47.1]:TopTopTopTopTop: product1(x0,x1,x2),product1(x2,x1,x3),product2(x3,x0,x4) -> equalish(x1,x4) {x0 -> e_2, x1 -> e_2, x2 -> e_2, x3 -> e_2, x4 -> e_4}
% 36.74/7.89  === Backtracking. Learning clause 115:6:1:[17.0,114.0,103.1,45.1,51.3,41.4]:Top: group_element(x0) -> equalish(e_2,x0),product1(e_2,x0,e_1),product1(e_2,x0,e_3),product1(e_2,x0,e_4),product1(e_2,x0,e_5)
% 36.74/7.89  === Backtracking. Learning clause 118:4:0:[19.0,116.1,27.0,117.3,44.3,26.1,115.3,43.1,36.1]:: product1(e_3,e_4,e_1),product1(e_2,e_5,e_3) -> product1(e_2,e_4,e_4),product1(e_2,e_4,e_5)
% 36.74/7.89  === Backtracking. Learning clause 119:3:3:[49.2,51.3,26.1]:TopTopTop: product2(e_2,x0,x1),product1(x0,x1,x2),product1(x2,x1,e_3) -> 
% 36.74/7.89  === Backtracking. Learning clause 120:3:0:[44.3,27.1,118.3,45.1]:: product1(e_3,e_4,e_1),product1(e_2,e_5,e_3) -> product1(e_2,e_4,e_5)
% 36.74/7.89  === Backtracking. Learning clause 125:8:1:[16.0,121.1,20.0,122.2,36.0,123.8,37.0,124.10,51.3,47.2,41.5,44.2,43.1,50.1,31.1,19.1,41.6,44.2,45.1,43.1,29.1,119.2]:Top: product1(e_3,e_4,e_1),product1(e_1,x0,e_1),product2(e_2,e_1,e_5),product1(e_2,e_5,e_3) -> product1(e_1,e_4,e_2),product1(e_1,e_4,e_5),product1(e_1,e_5,e_3),equalish(e_5,x0)
% 36.74/7.89  === Backtracking. Learning clause 127:10:2:[36.0,126.6,41.3,44.2,51.2,47.2,43.1,50.1,41.6,20.1,31.1,19.1]:TopTop: product1(x0,e_4,e_1),product1(e_3,e_4,x1),group_element(x1) -> product1(x1,e_4,e_2),product1(x1,e_4,e_5),equalish(x0,x1),product1(x1,e_5,e_1),product1(x1,e_5,e_2),product1(x1,e_5,e_3),product1(x1,e_5,e_5)
% 36.74/7.89  === Backtracking. Learning clause 129:3:0:[16.0,128.0,44.3,33.1,41.6,51.2,47.2,44.2,50.1,31.1,19.1,29.1,45.1]:: product1(e_3,e_4,e_1) -> product1(e_1,e_4,e_2),product1(e_1,e_4,e_5)
% 36.74/7.89  === Backtracking. Learning clause 130:2:2:[42.3,33.1]:TopTop: product1(x0,x1,e_4),product1(x0,x1,e_1) -> 
% 36.74/7.89  === Backtracking. Learning clause 131:2:2:[43.3,33.1]:TopTop: product1(x0,e_4,x1),product1(x0,e_1,x1) -> 
% 36.74/7.89  === Backtracking. Learning clause 132:12:7:[41.4,44.1,51.1,43.2,44.1,44.1]:TopTopTopTopTopTopTop: group_element(x0),group_element(x1),product1(x2,x1,e_2),product1(e_1,x1,x3),product1(x0,x4,e_4),product1(x5,x1,e_3),product1(x6,x1,e_5) -> equalish(x0,x2),product2(x3,x0,x1),equalish(x4,x1),equalish(x0,x5),equalish(x0,x6)
% 36.74/7.89  === Conflict found: 115:6:1:[17.0,114.0,103.1,45.1,51.3,41.4]:Top: group_element(x0) -> equalish(e_2,x0),product1(e_2,x0,e_1),product1(e_2,x0,e_3),product1(e_2,x0,e_4),product1(e_2,x0,e_5) {x0 -> e_5}
% 36.74/7.89  === Backtracking. Learning clause 138:16:7:[20.0,133.3,45.0,134.9,19.0,135.10,118.1,136.12,27.0,137.17,115.3,44.1,103.1,41.3,43.2,44.1,44.1,44.1,41.4,18.1,119.3,40.1,51.3,35.1,51.2,49.2,53.2,44.1,32.1,44.1,28.1,115.4,44.1]:TopTopTopTopTopTopTop: product1(e_4,x0,e_4),product1(x1,e_5,e_3),product1(x2,e_5,e_5),product2(e_2,x3,e_5),product1(x3,e_5,e_3),product1(e_3,e_4,e_1),product1(x4,e_5,e_3),product2(x5,x4,e_5),product1(x6,e_4,e_1) -> equalish(x0,e_5),equalish(e_4,x1),equalish(e_4,x2),equalish(e_1,x5),product1(e_2,e_4,e_4),product1(e_2,e_4,e_5),equalish(e_2,x6)
% 36.74/7.89  === Backtracking. Learning clause 139:8:3:[51.2,41.3]:TopTopTop: product1(x0,x1,x2),group_element(x2),group_element(x1) -> product2(e_1,x0,x1),product1(x2,x1,e_2),product1(x2,x1,e_3),product1(x2,x1,e_4),product1(x2,x1,e_5)
% 36.74/7.89  === Backtracking. Learning clause 140:11:6:[48.2,46.6,51.3,48.1,48.1]:TopTopTopTopTopTop: group_element(x0),group_element(x1),product1(x2,e_4,x3),product1(x3,e_4,x0),product2(x0,x4,e_5),product2(x0,x5,e_1) -> equalish(x2,x1),product2(x0,x1,e_2),product2(x0,x1,e_3),equalish(x1,x4),equalish(x1,x5)
% 36.74/7.89  === Clause set with instances from active satisfied. Growing active. New size: 349
% 36.74/7.89  
% 36.74/7.89  Linear Model Building succeeded.
% 36.74/7.89  SZS status Satisfiable
% 36.74/7.89  
% 36.74/7.89  Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.74/7.89  
% 36.74/7.89  SPASS-SCL-FOL Statistics:
% 36.74/7.89  Number of learned clauses: 31
% 36.74/7.89  Number of propagations: 2182
% 36.74/7.89  Number of decisions: 201
% 36.74/7.89  Number of resolutions: 178
% 36.74/7.89  Number of condensations: 5
% 36.74/7.89  Number of sub resolutions: 58
% 36.74/7.89  Number of input literals (deduplicated): 58
% 36.74/7.89  Number of grows: 6
% 36.74/7.89  Number of considered ground atoms: 349
% 36.74/7.89  
% 36.74/7.89   Needed:       0:00:07.36
% 36.74/7.89  
%------------------------------------------------------------------------------