%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO667-1 : TPTP v9.2.1. Released v7.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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.40s 0.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SYO667-1 : TPTP v9.2.1. Released v7.3.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.35 % Computer : n017.cluster.edu
% 0.16/0.35 % Model : x86_64 x86_64
% 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.35 % Memory : 8042.1875MB
% 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.35 % CPULimit : 300
% 0.16/0.35 % WCLimit : 300
% 0.16/0.35 % DateTime : Thu May 7 13:54:58 EDT 2026
% 0.16/0.35 % CPUTime :
% 0.16/0.35 SPASS-SCL-FOL version:
% 0.21/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.40/0.61 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.61 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.61 Execution normal ended with status: unsatisfiable
% 0.40/0.61 Used heuristic: normal
% 0.40/0.61
% 0.40/0.61 Input Clauses:
% 0.40/0.61
% 0.40/0.61 Predicates: 'E' 'LE'
% 0.40/0.61 Fol Constants: '0' z
% 0.40/0.61 Fol Functions: s suc f
% 0.40/0.61 Problem Properties:
% 0.40/0.61 This is a full first-order problem without equality.
% 0.40/0.61
% 0.40/0.61 After reduction: Problem Properties:
% 0.40/0.61 This is a full first-order problem without equality.
% 0.40/0.61
% 0.40/0.61
% 0.40/0.61 Reduced Input Clauses:
% 0.40/0.61 30:4:1:[12.2,1.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.40/0.61 31:4:1:[24.2,2.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.40/0.61 33:6:1:[31.4,5.0,24.2,32.6]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) ->
% 0.40/0.61 34:4:1:[16.2,6.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.40/0.61 36:5:1:[30.4,7.2,12.2,35.4]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.40/0.61 37:2:1:[21.0,13.0]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 0.40/0.61 40:5:1:[36.6,14.3,30.4,38.4,12.2,39.6]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) ->
% 0.40/0.61 42:6:1:[34.4,15.1,16.2,41.6]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(suc(x0))))) ->
% 0.40/0.61 44:5:1:[31.4,20.0,24.2,43.4]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.40/0.61 46:5:1:[34.4,25.0,16.2,45.5]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.40/0.61
% 0.40/0.61 Most General Atoms: 'E'(s(s('0')),f(x0)) 'E'(f(x0),f(suc(suc(x0)))) 'E'(s('0'),f(x0)) 'LE'(f(x0),s(s('0'))) 'LE'(f(x0),s('0')) 'E'(f(x0),f(suc(suc(suc(x0))))) 'E'('0',f(x0)) 'LE'(f(x0),'0') 'E'(f(x0),f(suc(x0))) 'LE'(f(x0),s(s(s('0'))))
% 0.40/0.61
% 0.40/0.61 === Starting SPASS-SCL-FOL A Little Less Naive, considering 69 atoms initially, heuristics mode: normal ===
% 0.40/0.61
% 0.40/0.61 === Conflict found: 40:5:1:[36.6,14.3,30.4,38.4,12.2,39.6]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> '0'}
% 0.40/0.61 === Backtracking. Learning clause 47:5:1:[40.5,28.2,37.1,3.2,18.2]:Top: 'E'(s(s('0')),f(suc(suc(suc(x0))))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 0.40/0.61 === Backtracking. Learning clause 48:7:1:[19.2,47.1,29.1,10.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'E'(s('0'),f(x0)),'E'('0',f(x0)),'LE'(f(x0),'0')
% 0.40/0.61 === Conflict found: 40:5:1:[36.6,14.3,30.4,38.4,12.2,39.6]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> z}
% 0.40/0.61 === Backtracking. Learning clause 49:5:1:[40.5,18.2,19.2,37.1]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))) -> 'LE'(f(suc(x0)),s(s('0')))
% 0.40/0.61 === Clause set with instances from active satisfied. Growing active. New size: 133
% 0.40/0.61 === Backtracking. Learning clause 51:4:1:[37.0,50.1,19.1,21.1,40.3]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> 'LE'(f(suc(x0)),s(s('0')))
% 0.40/0.61 === Conflict found: 49:5:1:[40.5,18.2,19.2,37.1]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))) -> 'LE'(f(suc(x0)),s(s('0'))) {x0 -> s('0')}
% 0.40/0.61 === Backtracking. Learning clause 52:5:1:[49.2,28.2]:Top: 'E'(s(s('0')),f(x0)),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(suc(x0)),s(s('0')))
% 0.40/0.61 === Clause set with instances from active satisfied. Growing active. New size: 197
% 0.40/0.61 === Conflict found: 47:5:1:[40.5,28.2,37.1,3.2,18.2]:Top: 'E'(s(s('0')),f(suc(suc(suc(x0))))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(z))}
% 0.40/0.61 === Backtracking. Learning clause 53:4:1:[47.3,21.1,19.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 0.40/0.61 === Conflict found: 47:5:1:[40.5,28.2,37.1,3.2,18.2]:Top: 'E'(s(s('0')),f(suc(suc(suc(x0))))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(z))}
% 0.40/0.61 === Backtracking. Learning clause 54:3:1:[47.2,21.1,19.2,21.1]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 0.40/0.61 === Conflict found: 33:6:1:[31.4,5.0,24.2,32.6]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) -> {x0 -> z}
% 0.40/0.61 === Backtracking. Learning clause 55:10:1:[33.2,4.2,44.5,11.2,22.2,26.2,48.5,10.1]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 0.40/0.61 === Conflict found: 44:5:1:[31.4,20.0,24.2,43.4]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> z}
% 0.40/0.61 === Backtracking. Learning clause 56:6:1:[44.5,33.3,22.2,4.2,26.2,29.2,11.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.40/0.61 === Conflict found: 46:5:1:[34.4,25.0,16.2,45.5]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))) -> 'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> z}
% 0.40/0.61 === Backtracking. Learning clause 57:5:1:[46.1,8.2,9.2,17.2,22.3,29.3,26.3]:Top: 'E'('0',f(x0)),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(x0)))))
% 0.40/0.61 === Clause set with instances from active satisfied. Growing active. New size: 261
% 0.40/0.61 === Conflict found: 54:3:1:[47.2,21.1,19.2,21.1]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(suc(suc('0'))))}
% 0.40/0.61 === Backtracking. Learning clause 58:3:1:[54.1,21.1,22.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.40/0.61 === Backtracking. Learning clause 59:4:1:[24.2,22.2,29.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s('0'))) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.40/0.61 === Conflict found: 33:6:1:[31.4,5.0,24.2,32.6]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) -> {x0 -> '0'}
% 0.40/0.61 === Backtracking. Learning clause 60:6:1:[33.3,44.5,29.2]:Top: 'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(suc(x0)),s('0'))
% 0.40/0.61 === Clause set with instances from active satisfied. Growing active. New size: 325
% 0.40/0.61 === Conflict found: 58:3:1:[54.1,21.1,22.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0')) {x0 -> suc(suc(suc(f('0'))))}
% 0.40/0.61 === Backtracking. Learning clause 61:2:1:[58.1,21.1]:Top: -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.40/0.61 === Conflict found: 34:4:1:[16.2,6.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))) {x0 -> suc(s('0'))}
% 0.40/0.61 === Backtracking. Learning clause 62:6:1:[34.1,8.2,17.2,26.3,9.2,58.3,29.3,24.1]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> 'E'(f(suc(x0)),f(suc(suc(suc(x0))))),'LE'(f(x0),'0'),'E'(f(suc(suc(suc(x0)))),f(suc(suc(suc(suc(x0))))))
% 0.40/0.61 === Clause set with instances from active satisfied. Growing active. New size: 389
% 0.40/0.61 === Conflict found: 54:3:1:[47.2,21.1,19.2,21.1]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(suc(suc(f('0')))))}
% 0.40/0.61 === Backtracking. Learning clause 63:2:1:[54.1,21.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 0.40/0.61 === Conflict found: 63:2:1:[54.1,21.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(z))}
% 0.40/0.61 === Backtracking. Learning clause 64:1:1:[63.1,21.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 0.40/0.61 === Backtracking. Learning clause 68:2:1:[64.0,65.0,64.0,66.1,64.0,67.2,11.1,64.1,44.3,29.2,26.2,22.2]:Top: -> 'E'(f(x0),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 0.40/0.61 === Backtracking. Learning clause 71:2:0:[68.1,69.0,64.0,70.1,10.2,57.1,23.1]:: -> 'E'(f(z),f(suc(suc(suc(z))))),'E'(s('0'),f(suc(suc(suc(z)))))
% 0.40/0.61 === Clause set with instances from active satisfied. Growing active. New size: 453
% 0.40/0.61 === Backtracking. Learning clause 72:6:1:[27.2,42.1,29.3,46.5,8.2,22.3]:Top: 'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(suc(x0))))))
% 0.40/0.61 === Conflict found: 56:6:1:[44.5,33.3,22.2,4.2,26.2,29.2,11.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> suc(suc(suc(f('0'))))}
% 0.40/0.61 === Backtracking. Learning clause 74:2:1:[64.0,73.1,56.5,64.1,64.1,64.1]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.40/0.61 === Conflict found: 74:2:1:[64.0,73.1,56.5,64.1,64.1,64.1]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> s(z)}
% 0.40/0.61 === Backtracking. Learning clause 75:1:1:[74.1,64.1]:Top: -> 'LE'(f(x0),s('0'))
% 0.40/0.61 === Backtracking. Learning clause 76:2:0:[27.1,75.1,42.1,17.2,75.1,8.2,9.2,75.1,75.1,10.2,23.1,71.1]:: 'LE'(f(z),s('0')) -> 'E'(s('0'),f(suc(suc(suc(z)))))
% 0.40/0.61
% 0.40/0.61 SZS status Unsatisfiable
% 0.40/0.61
% 0.40/0.61 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.61
% 0.40/0.61 SPASS-SCL-FOL Statistics:
% 0.40/0.61 Number of learned clauses: 23
% 0.40/0.61 Number of propagations: 1606
% 0.40/0.61 Number of decisions: 614
% 0.40/0.61 Number of resolutions: 92
% 0.40/0.61 Number of condensations: 0
% 0.40/0.61 Number of sub resolutions: 24
% 0.40/0.61 Number of input literals (deduplicated): 35
% 0.40/0.61 Number of grows: 6
% 0.40/0.61 Number of considered ground atoms: 453
% 0.40/0.61
% 0.40/0.61 Needed: 0:00:00.05
% 0.40/0.61
%------------------------------------------------------------------------------