%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO648-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 : n028.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:14 PM UTC 2026
% Result : Unsatisfiable 0.39s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO648-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.15/0.34 % Computer : n028.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 13:56:31 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.60 Execution normal ended with status: unsatisfiable
% 0.39/0.60 Used heuristic: normal
% 0.39/0.60
% 0.39/0.60 Input Clauses:
% 0.39/0.60
% 0.39/0.60 Predicates: 'E' iLEQ 'LE'
% 0.39/0.60 Fol Constants: '0' z
% 0.39/0.60 Fol Functions: suc f s
% 0.39/0.60 Problem Properties:
% 0.39/0.60 This is a full first-order problem without equality.
% 0.39/0.60
% 0.39/0.60 After reduction: Problem Properties:
% 0.39/0.60 This is a full first-order problem without equality.
% 0.39/0.60
% 0.39/0.60
% 0.39/0.60 Reduced Input Clauses:
% 0.39/0.60 28:8:2:[14.5,1.6]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 0.39/0.60 29:10:2:[28.8,4.4]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.60 31:13:2:[25.12,5.2,13.10,30.7]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 0.39/0.60 33:6:1:[18.4,6.4,3.2,32.5]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 0.39/0.60 35:14:2:[22.13,7.2,31.13,34.4]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 0.39/0.60 38:6:1:[33.6,9.2,18.4,36.5,3.2,37.6]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(suc(x0)))))) -> iLEQ(suc(x0),suc(x0))
% 0.39/0.60 40:9:2:[23.8,11.1,14.6,39.5]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.39/0.60 43:9:2:[13.9,12.2,28.7,41.8,14.5,42.9]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(x1)))
% 0.39/0.60 45:9:2:[28.7,13.7,14.5,44.8]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1)))
% 0.39/0.60 48:9:2:[23.8,16.1,14.6,46.6,40.10,47.9]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1)))
% 0.39/0.60 51:11:2:[29.10,17.1,28.8,49.7,48.11,50.11]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.60 52:5:1:[3.2,18.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 0.39/0.60 55:10:2:[29.10,20.1,28.8,53.6,40.9,54.9]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.39/0.60 58:11:2:[25.11,22.2,43.11,56.6,29.9,57.9]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.60 59:8:2:[14.6,23.3]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.60 63:13:2:[58.13,24.2,43.11,60.9,51.13,61.12,48.11,62.14]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(suc(x1)))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))) ->
% 0.39/0.60 66:10:2:[45.10,25.5,29.9,64.8,59.7,65.9]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.60 67:2:1:[8.0,26.0]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 0.39/0.60 71:12:2:[66.12,27.2,45.10,68.8,51.13,69.11,48.11,70.13]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(suc(x1)))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.39/0.60
% 0.39/0.60 Most General Atoms: 'E'('0',f(x1)) 'LE'(f(x0),'0') 'E'(f(x0),f(suc(x0))) 'E'(f(x1),f(suc(suc(x1)))) 'E'(f(x1),f(suc(suc(suc(x1))))) 'LE'(f(x0),s('0')) iLEQ(suc(x1),suc(x0))
% 0.39/0.60
% 0.39/0.60 === Starting SPASS-SCL-FOL A Little Less Naive, considering 49 atoms initially, heuristics mode: normal ===
% 0.39/0.60
% 0.39/0.60 === Conflict found: 35:14:2:[22.13,7.2,31.13,34.4]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(suc(suc(x1))))) {x0 -> z, x1 -> z}
% 0.39/0.60
% 0.39/0.60 SZS status Unsatisfiable
% 0.39/0.60
% 0.39/0.60 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.60
% 0.39/0.60 SPASS-SCL-FOL Statistics:
% 0.39/0.60 Number of learned clauses: 0
% 0.39/0.60 Number of propagations: 25
% 0.39/0.60 Number of decisions: 0
% 0.39/0.60 Number of resolutions: 14
% 0.39/0.60 Number of condensations: 0
% 0.39/0.60 Number of sub resolutions: 44
% 0.39/0.60 Number of input literals (deduplicated): 17
% 0.39/0.60 Number of grows: 0
% 0.39/0.60 Number of considered ground atoms: 49
% 0.39/0.60
% 0.39/0.60 Needed: 0:00:00.03
% 0.39/0.60
%------------------------------------------------------------------------------