%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO675-1 : TPTP v9.2.1. Released v7.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:41:16 PM UTC 2026
% Result : Unsatisfiable 0.42s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO675-1 : TPTP v9.2.1. Released v7.3.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n020.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:56:21 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.42/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.62 Execution resolution_1 ended with status: unsatisfiable
% 0.42/0.62 Used heuristic: resolution_1
% 0.42/0.62
% 0.42/0.62 Input Clauses:
% 0.42/0.62
% 0.42/0.62 Predicates: 'E' 'LE'
% 0.42/0.62 Fol Constants: '0' z
% 0.42/0.62 Fol Functions: f suc s
% 0.42/0.62 Problem Properties:
% 0.42/0.62 This is a full first-order problem without equality.
% 0.42/0.62
% 0.42/0.62 After reduction: Problem Properties:
% 0.42/0.62 This is a full first-order problem without equality.
% 0.42/0.62
% 0.42/0.62
% 0.42/0.62 Reduced Input Clauses:
% 0.42/0.62 31:5:1:[9.2,1.0]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(x0)) ->
% 0.42/0.62 32:4:1:[14.2,4.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.42/0.62 33:4:1:[7.2,13.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.42/0.62 35:4:1:[33.4,17.0,7.2,34.5]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) ->
% 0.42/0.62 36:2:1:[30.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 0.42/0.62 38:4:1:[29.4,22.0,16.2,37.3]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) ->
% 0.42/0.62 40:4:1:[32.4,24.3,14.2,39.4]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))) ->
% 0.42/0.62 41:4:1:[9.2,27.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.42/0.62 42:4:1:[16.2,29.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.42/0.62
% 0.42/0.62 Most General Atoms: 'E'(f(x0),f(suc(suc(x0)))) 'E'('0',f(x0)) 'LE'(f(x0),s('0')) 'LE'(f(x0),'0') 'E'(s(s(s('0'))),f(x0)) 'LE'(f(x0),s(s('0'))) 'E'(s(s('0')),f(x0)) 'E'(f(x0),f(suc(x0))) 'LE'(f(x0),s(s(s('0')))) 'E'(s('0'),f(x0)) 'LE'(f(x0),s(s(s(s('0')))))
% 0.42/0.62
% 0.42/0.62 === Starting SPASS-SCL-FOL A Little Less Naive, considering 21 atoms initially, heuristics mode: resolution_1 ===
% 0.42/0.62
% 0.42/0.62 === Conflict found: 31:5:1:[9.2,1.0]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(x0)) -> {x0 -> '0'}
% 0.42/0.62 === Backtracking. Learning clause 43:4:1:[31.4,41.4]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) ->
% 0.42/0.62 === Conflict found: 36:2:1:[30.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> '0'}
% 0.42/0.62 === Backtracking. Learning clause 44:3:1:[36.2,8.1]:Top: -> 'E'(s(s(s('0'))),f(x0)),'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Conflict found: 36:2:1:[30.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc('0')}
% 0.42/0.62 === Backtracking. Learning clause 45:3:1:[36.2,12.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Conflict found: 36:2:1:[30.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc('0'))}
% 0.42/0.62 === Backtracking. Learning clause 46:3:1:[36.2,11.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Conflict found: 36:2:1:[30.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc('0')))}
% 0.42/0.62 === Backtracking. Learning clause 47:5:1:[36.2,5.1,40.1,46.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Backtracking. Learning clause 48:4:1:[25.1,30.1,40.1,11.1,46.1,45.1]:Top: 'E'(s(s(s('0'))),f(x0)) -> 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Backtracking. Learning clause 49:2:1:[25.1,30.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 0.42/0.62 === Conflict found: 36:2:1:[30.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc('0')))}
% 0.42/0.62 === Backtracking. Learning clause 51:4:1:[36.0,50.1,36.2,5.1,40.1,49.1]:Top: 'E'(s(s(s('0'))),f(x0)) -> 'E'(s(s('0')),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(x0)),s(s(s('0'))))
% 0.42/0.62 === Backtracking. Learning clause 52:3:1:[19.1,30.1,40.1,49.1,12.1,45.1,44.1]:Top: -> 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Conflict found: 49:2:1:[25.1,30.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc('0'))}
% 0.42/0.62 === Backtracking. Learning clause 54:3:1:[36.0,53.0,49.1,40.1,11.1,46.1,49.1]:Top: -> 'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0'))),'LE'(f(x0),s(s(s('0'))))
% 0.42/0.62 === Backtracking. Learning clause 55:2:1:[19.1,30.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0'))))
% 0.42/0.62 === Conflict found: 36:2:1:[30.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc('0')))}
% 0.42/0.62 === Backtracking. Learning clause 58:3:1:[36.0,56.0,49.0,57.1,36.2,5.1,40.1,55.1]:Top: -> 'E'(s(s('0')),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s('0'))),'LE'(f(x0),s(s(s('0'))))
% 0.42/0.62 === Backtracking. Learning clause 59:2:1:[28.1,30.1,40.1,55.1,49.1,8.1,44.1]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Clause set with instances from active satisfied. Growing active. New size: 32
% 0.42/0.62 === Restarting.
% 0.42/0.62 === Conflict found: 59:2:1:[28.1,30.1,40.1,55.1,49.1,8.1,44.1]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0'))) {x0 -> suc('0')}
% 0.42/0.62 === Backtracking. Learning clause 60:4:1:[59.2,10.1,7.2]:Top: 'E'(s(s('0')),f(x0)) -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0')),'E'(f(x0),f(suc(x0)))
% 0.42/0.62 === Conflict found: 59:2:1:[28.1,30.1,40.1,55.1,49.1,8.1,44.1]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0'))) {x0 -> suc('0')}
% 0.42/0.62 === Backtracking. Learning clause 61:3:1:[59.2,10.1]:Top: -> 'E'(s(s('0')),f(suc(x0))),'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.42/0.62 === Conflict found: 49:2:1:[25.1,30.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0')))) {x0 -> '0'}
% 0.42/0.62 === Backtracking. Learning clause 63:2:1:[36.0,62.0,49.1,14.2]:Top: -> 'LE'(f(x0),s(s(s('0')))),'E'(f(x0),f(suc(x0)))
% 0.42/0.62 === Conflict found: 59:2:1:[28.1,30.1,40.1,55.1,49.1,8.1,44.1]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0'))) {x0 -> suc(suc('0'))}
% 0.42/0.62 === Backtracking. Learning clause 64:3:1:[59.2,2.1]:Top: -> 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 0.42/0.62 === Clause set with instances from active satisfied. Growing active. New size: 34
% 0.42/0.62 === Restarting.
% 0.42/0.62 === Clause set with instances from active satisfied. Growing active. New size: 98
% 0.42/0.62 === Conflict found: 40:4:1:[32.4,24.3,14.2,39.4]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))) -> {x0 -> suc('0')}
% 0.42/0.62 === Backtracking. Learning clause 67:2:1:[36.0,65.0,36.0,66.1,40.1,55.1,55.1]:Top: -> 'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(x0),s(s(s('0'))))
% 0.42/0.62 === Clause set with instances from active satisfied. Growing active. New size: 162
% 0.42/0.62 === Backtracking. Learning clause 68:2:1:[28.1,30.1,40.1,55.1,49.1,12.1,45.1]:Top: -> 'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Backtracking. Learning clause 70:2:1:[59.0,69.0,5.1,36.2,35.4,11.2,49.2,68.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Conflict found: 55:2:1:[19.1,30.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc('0'))}
% 0.42/0.62 === Backtracking. Learning clause 72:3:1:[36.0,71.2,55.1,40.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> 'LE'(f(suc(x0)),s(s(s('0'))))
% 0.42/0.62 === Backtracking. Learning clause 76:3:1:[68.0,73.0,59.0,74.1,70.0,75.4,5.1,49.2,35.4,11.2,40.1,72.3]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))) -> 'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Clause set with instances from active satisfied. Growing active. New size: 226
% 0.42/0.62 === Backtracking. Learning clause 79:1:1:[36.0,77.0,49.0,78.1,28.1,30.1,40.1,55.1]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 0.42/0.62 === Conflict found: 33:4:1:[7.2,13.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))) {x0 -> suc(suc(z))}
% 0.42/0.62 === Backtracking. Learning clause 82:5:1:[79.0,80.0,79.0,81.1,33.3,68.1,11.2,5.2,10.1,38.2,2.2]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s('0'))
% 0.42/0.62 === Conflict found: 33:4:1:[7.2,13.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))) {x0 -> suc(suc(z))}
% 0.42/0.62 === Backtracking. Learning clause 84:4:1:[79.0,83.0,33.1,11.2,68.1,59.1,82.3]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s('0'))
% 0.42/0.62 === Backtracking. Learning clause 86:5:1:[79.0,85.0,12.3,21.1,33.1]:Top: 'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0')),'E'(f(suc(suc(x0))),f(suc(suc(suc(suc(x0))))))
% 0.42/0.62 === Backtracking. Learning clause 88:3:1:[79.0,87.0,12.3,21.1]:Top: -> 'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 0.42/0.62 === Clause set with instances from active satisfied. Growing active. New size: 290
% 0.42/0.62 === Backtracking. Learning clause 89:2:1:[11.1,79.1]:Top: -> 'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Clause set with instances from active satisfied. Growing active. New size: 354
% 0.42/0.62 === Conflict found: 35:4:1:[33.4,17.0,7.2,34.5]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> {x0 -> f(z)}
% 0.42/0.62 === Backtracking. Learning clause 92:2:1:[68.0,90.0,68.0,91.1,35.4,89.1,59.1]:Top: -> 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Conflict found: 45:3:1:[36.2,12.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0'))) {x0 -> suc(s('0'))}
% 0.42/0.62 === Backtracking. Learning clause 93:4:1:[45.2,7.2,10.1,61.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(f(suc(x0)),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.42/0.62 === Clause set with instances from active satisfied. Growing active. New size: 418
% 0.42/0.62 === Backtracking. Learning clause 94:2:1:[5.1,79.1,35.4,68.1,89.1,10.1,61.1]:Top: -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.42/0.62 === Backtracking. Learning clause 95:4:1:[16.1,26.2,94.1,23.1]:Top: 'LE'(f(x0),s(s('0'))) -> 'E'(f(x0),f(suc(x0))),'E'('0',f(x0)),'LE'(f(x0),'0')
% 0.42/0.62 === Conflict found: 35:4:1:[33.4,17.0,7.2,34.5]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> {x0 -> s(z)}
% 0.42/0.62 === Backtracking. Learning clause 97:1:1:[79.0,96.0,35.1,68.1,59.1,5.2,89.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 0.42/0.62 === Clause set with instances from active satisfied. Growing active. New size: 482
% 0.42/0.62 === Backtracking. Learning clause 98:2:1:[2.1,97.1]:Top: -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 0.42/0.62 === Conflict found: 43:4:1:[31.4,41.4]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> {x0 -> z}
% 0.42/0.62 === Backtracking. Learning clause 101:3:1:[97.0,99.0,59.1,100.1,43.3,6.2,3.2,15.2,2.3,26.3,23.2,10.3,88.3,38.3,98.1,26.2,94.1]:Top: -> 'LE'(f(x0),'0'),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'LE'(f(suc(suc(suc(suc(x0))))),s('0'))
% 0.42/0.62 === Conflict found: 38:4:1:[29.4,22.0,16.2,37.3]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) -> {x0 -> suc(z)}
% 0.42/0.62 === Backtracking. Learning clause 104:2:1:[98.0,102.1,97.0,103.2,38.2,94.1,26.2]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))) -> 'LE'(f(x0),s('0'))
% 0.42/0.62 === Backtracking. Learning clause 106:1:1:[97.0,105.0,21.2,104.1]:Top: -> 'LE'(f(x0),s('0'))
% 0.42/0.62 === Conflict found: 43:4:1:[31.4,41.4]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> {x0 -> z}
% 0.42/0.62
% 0.42/0.62 SZS status Unsatisfiable
% 0.42/0.62
% 0.42/0.62 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.62
% 0.42/0.62 SPASS-SCL-FOL Statistics:
% 0.42/0.62 Number of learned clauses: 37
% 0.42/0.62 Number of propagations: 1841
% 0.42/0.62 Number of decisions: 725
% 0.42/0.62 Number of resolutions: 120
% 0.42/0.62 Number of condensations: 0
% 0.42/0.62 Number of sub resolutions: 39
% 0.42/0.62 Number of input literals (deduplicated): 36
% 0.42/0.62 Number of grows: 9
% 0.42/0.62 Number of considered ground atoms: 482
% 0.42/0.62
% 0.42/0.62 Needed: 0:00:00.08
% 0.42/0.62
%------------------------------------------------------------------------------