%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO661-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 : n008.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:15 PM UTC 2026
% Result : Unsatisfiable 1.27s 0.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO661-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.17/0.34 % Computer : n008.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 13:56:29 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.27/0.71 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.27/0.71 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.27/0.71 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.27/0.71 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.27/0.71 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.27/0.71 Execution resolution_1 ended with status: unsatisfiable
% 1.27/0.71 Used heuristic: resolution_1
% 1.27/0.71
% 1.27/0.71 Input Clauses:
% 1.27/0.71
% 1.27/0.71 Predicates: 'LE' 'E' iLEQ
% 1.27/0.71 Fol Constants: z '0'
% 1.27/0.71 Fol Functions: f s suc
% 1.27/0.71 Problem Properties:
% 1.27/0.71 This is a full first-order problem without equality.
% 1.27/0.71
% 1.27/0.71 After reduction: Problem Properties:
% 1.27/0.71 This is a full first-order problem without equality.
% 1.27/0.71
% 1.27/0.71
% 1.27/0.71 Reduced Input Clauses:
% 1.27/0.71 29:11:3:[4.10,2.6]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 1.27/0.71 30:13:3:[11.12,5.7]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) ->
% 1.27/0.71 31:12:3:[12.10,11.6]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x1),f(suc(x1)))
% 1.27/0.71 32:11:3:[4.9,12.7]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 1.27/0.71 33:12:3:[19.11,13.9]:TopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x2)),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'(f(x0),f(suc(x0))) -> 'E'(f(x2),f(suc(x2)))
% 1.27/0.71 34:11:3:[4.8,14.6]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 1.27/0.71 36:11:3:[32.11,16.6,29.11,35.9]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2)))
% 1.27/0.71 37:12:3:[19.10,17.7]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x2),f(suc(x2)))
% 1.27/0.71 39:12:3:[33.12,18.8,37.12,38.11]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(f(x1),f(suc(x1))) ->
% 1.27/0.71 40:11:3:[20.8,19.9]:TopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 1.27/0.71 41:12:3:[24.11,21.7]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1)))
% 1.27/0.71 42:4:1:[15.2,22.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0))
% 1.27/0.71 43:11:3:[20.10,24.8]:TopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x2)),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 1.27/0.71 44:2:1:[6.0,25.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 1.27/0.71 45:11:3:[20.9,26.6]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 1.27/0.71 47:11:3:[34.11,27.7,29.10,46.8]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0)))
% 1.27/0.71 48:4:1:[10.2,28.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 1.27/0.71
% 1.27/0.71 Most General Atoms: 'E'(s('0'),f(x0)) 'LE'(f(x0),'0') 'E'(f(x1),f(suc(x1))) 'LE'(f(x0),s(s('0'))) 'LE'(f(x0),s('0')) 'E'('0',f(x2)) iLEQ(suc(x1),suc(x0))
% 1.27/0.71
% 1.27/0.71 === Starting SPASS-SCL-FOL A Little Less Naive, considering 13 atoms initially, heuristics mode: resolution_1 ===
% 1.27/0.71
% 1.27/0.71 === Conflict found: 39:12:3:[33.12,18.8,37.12,38.11]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(f(x1),f(suc(x1))) -> {x0 -> z, x1 -> z, x2 -> z}
% 1.27/0.71 === Backtracking. Learning clause 50:3:1:[42.3,49.3,39.12,20.9]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x0))) ->
% 1.27/0.71 === Conflict found: 44:2:1:[6.0,25.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0')) {x0 -> suc(suc(z))}
% 1.27/0.71 === Backtracking. Learning clause 51:5:1:[44.1,30.3]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(suc(suc(x0))),s('0'))
% 1.27/0.71 === Backtracking. Learning clause 52:5:1:[7.1,6.1,30.3,44.1,20.9]:Top: 'E'(s('0'),f(x0)),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(suc(x0)),s('0'))
% 1.27/0.71 === Backtracking. Learning clause 53:2:1:[7.1,6.1]:Top: -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 1.27/0.71 === Backtracking. Learning clause 55:4:1:[44.0,54.0,23.1,6.1,30.3,53.1,20.9]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0'))
% 1.27/0.71 === Conflict found: 48:4:1:[10.2,28.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 1.27/0.71 === Backtracking. Learning clause 57:3:1:[44.0,56.0,48.1,53.1,53.1]:Top: -> iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s('0')),'LE'(f(x0),s('0'))
% 1.27/0.71 === Conflict found: 44:2:1:[6.0,25.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0')) {x0 -> suc(suc(z))}
% 1.27/0.71 === Backtracking. Learning clause 58:4:1:[44.1,48.1]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(suc(suc(x0))),s('0')),iLEQ(suc(x0),suc(x0))
% 1.27/0.71 === Backtracking. Learning clause 59:3:1:[23.1,6.1,48.1,53.1,55.3,44.1]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))) -> 'LE'(f(x0),s('0'))
% 1.27/0.71 === Conflict found: 30:13:3:[11.12,5.7]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> {x0 -> z, x1 -> z, x2 -> z}
% 1.27/0.71 === Backtracking. Learning clause 62:3:1:[44.0,60.0,57.0,61.2,30.3,53.1,53.1]:Top: 'E'(f(x0),f(suc(x0))) -> 'LE'(f(suc(x0)),s('0')),'LE'(f(x0),s('0'))
% 1.27/0.71 === Backtracking. Learning clause 65:2:1:[44.0,63.0,57.0,64.1,4.1,53.1,62.1]:Top: -> 'LE'(f(suc(x0)),s('0')),'LE'(f(x0),s('0'))
% 1.27/0.71 === Backtracking. Learning clause 67:3:1:[44.0,66.0,23.1,6.1,30.3,53.1]:Top: 'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0'))
% 1.27/0.71 === Backtracking. Learning clause 69:2:1:[44.0,68.0,4.1,53.1,67.1]:Top: iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0'))
% 1.27/0.71 === Backtracking. Learning clause 70:1:1:[23.1,6.1,48.1,53.1,69.1,44.1]:Top: -> 'LE'(f(x0),s('0'))
% 1.27/0.71 === Clause set with instances from active satisfied. Growing active. New size: 16
% 1.27/0.71 === Restarting.
% 1.27/0.71 === Backtracking. Learning clause 71:2:1:[9.1,70.1]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 1.27/0.71 === Conflict found: 71:2:1:[9.1,70.1]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0') {x0 -> suc(suc(z))}
% 1.27/0.71 === Backtracking. Learning clause 72:3:1:[71.1,50.1]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))) -> 'LE'(f(suc(suc(x0))),'0')
% 1.27/0.71 === Backtracking. Learning clause 73:2:1:[8.1,70.1,50.1,71.1]:Top: 'E'('0',f(x0)) -> 'LE'(f(suc(x0)),'0')
% 1.27/0.71 === Backtracking. Learning clause 75:2:1:[71.0,74.0,3.1,70.1,50.1]:Top: 'E'('0',f(suc(x0))) -> 'LE'(f(x0),'0')
% 1.27/0.71
% 1.27/0.71 SZS status Unsatisfiable
% 1.27/0.71
% 1.27/0.71 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.27/0.71
% 1.27/0.71 SPASS-SCL-FOL Statistics:
% 1.27/0.71 Number of learned clauses: 17
% 1.27/0.71 Number of propagations: 103
% 1.27/0.71 Number of decisions: 46
% 1.27/0.71 Number of resolutions: 43
% 1.27/0.71 Number of condensations: 1
% 1.27/0.71 Number of sub resolutions: 30
% 1.27/0.71 Number of input literals (deduplicated): 17
% 1.27/0.71 Number of grows: 1
% 1.27/0.71 Number of considered ground atoms: 16
% 1.27/0.71
% 1.27/0.71 Needed: 0:00:00.20
% 1.27/0.71
%------------------------------------------------------------------------------