%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO668-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 : n013.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.39s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO668-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 : n013.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:12 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 SPASS-SCL-FOL version:
% 0.19/0.44 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 lmodel_grow ended with status: unsatisfiable
% 0.39/0.60 Used heuristic: lmodel_grow
% 0.39/0.60
% 0.39/0.60 Input Clauses:
% 0.39/0.60
% 0.39/0.60 Predicates: 'E' '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 37:8:1:[12.4,1.1,32.2,36.7]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(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(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))) ->
% 0.39/0.60 38:4:1:[10.2,5.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.39/0.60 40:7:1:[12.4,7.1,32.2,39.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))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 0.39/0.60 42:8:1:[23.4,9.0,19.2,41.8]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),'E'(f(x0),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.39/0.60 43:4:1:[32.2,12.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.39/0.60 45:5:1:[23.4,14.0,19.2,44.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.39/0.60 46:2:1:[26.0,15.0]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 0.39/0.60 49:6:1:[30.6,17.3,38.4,47.4,10.2,48.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)))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 0.39/0.60 50:4:1:[19.2,23.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.39/0.60 54:6:1:[30.6,27.3,38.4,51.5,10.2,52.7,49.8,53.8]: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(suc(suc(x0))))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) ->
% 0.39/0.60 57:6:1:[50.4,29.0,45.6,55.3,19.2,56.6]:Top: 'E'(s('0'),f(suc(x0))),'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)) -> 'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 0.39/0.60 59:5:1:[38.4,30.2,10.2,58.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.39/0.60 61:5:1:[43.4,31.0,32.2,60.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.39/0.60
% 0.39/0.60 Most General Atoms: 'E'('0',f(x0)) 'E'(f(x0),f(suc(suc(suc(suc(x0)))))) 'E'(f(x0),f(suc(suc(suc(x0))))) 'LE'(f(x0),'0') 'LE'(f(x0),s('0')) 'E'(s(s('0')),f(x0)) 'E'(f(x0),f(suc(suc(x0)))) 'E'(s('0'),f(x0)) 'E'(f(x0),f(suc(x0))) 'LE'(f(x0),s(s('0'))) 'LE'(f(x0),s(s(s('0'))))
% 0.39/0.60
% 0.39/0.60 === Starting SPASS-SCL-FOL A Little Less Naive, considering 83 atoms initially, heuristics mode: lmodel_grow ===
% 0.39/0.60
% 0.39/0.60 === Clause set with instances from active satisfied. Growing active. New size: 101
% 0.39/0.60 === Clause set with instances from active satisfied. Growing active. New size: 117
% 0.39/0.60 === Clause set with instances from active satisfied. Growing active. New size: 136
% 0.39/0.60 === Backtracking. Learning clause 63:5:1:[46.0,62.3,28.1,26.1,54.4]: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(x0)))) -> 'LE'(f(suc(suc(suc(x0)))),s(s('0')))
% 0.39/0.60 === Backtracking. Learning clause 65:6:1:[46.0,64.3,16.1,26.1,54.4,46.1,25.1]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))) -> 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.39/0.60 === Clause set with instances from active satisfied. Growing active. New size: 153
% 0.39/0.60 === Clause set with instances from active satisfied. Growing active. New size: 161
% 0.39/0.60 === Backtracking. Learning clause 67:5:1:[46.0,66.4,16.1,26.1,54.4]: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))))) -> 'LE'(f(suc(suc(x0))),s(s('0')))
% 0.39/0.60 === Backtracking. Learning clause 68:6:1:[33.2,54.4,26.1,16.2,26.1,24.1]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))) -> 'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 0.39/0.60 === Backtracking. Learning clause 69:4:1:[13.1,26.1,54.4,33.2,26.1,22.2,46.1,28.2,16.2]:Top: 'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 0.39/0.60 === Conflict found: 42:8:1:[23.4,9.0,19.2,41.8]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),'E'(f(x0),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.39/0.60 === Backtracking. Learning clause 70:7:1:[42.5,45.5,57.6,24.2,8.2,20.2,18.2,11.2,25.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(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(x0)),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.39/0.60 === Clause set with instances from active satisfied. Growing active. New size: 184
% 0.39/0.60 === Conflict found: 69:4:1:[13.1,26.1,54.4,33.2,26.1,22.2,46.1,28.2,16.2]:Top: 'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(suc(suc(suc(suc(s('0')))))))}
% 0.39/0.60 === Backtracking. Learning clause 71:1:1:[69.3,26.1,26.1,26.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 0.39/0.60 === Backtracking. Learning clause 72:4:1:[20.1,71.1,42.3,45.5,57.6,11.2,71.1,25.2,71.1,24.2,8.2,18.2]:Top: 'LE'(f(suc(suc(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('0'))
% 0.39/0.60 === Conflict found: 40:7:1:[12.4,7.1,32.2,39.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))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))) {x0 -> 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: 8
% 0.39/0.60 Number of propagations: 342
% 0.39/0.60 Number of decisions: 209
% 0.39/0.60 Number of resolutions: 66
% 0.39/0.60 Number of condensations: 0
% 0.39/0.60 Number of sub resolutions: 29
% 0.39/0.60 Number of input literals (deduplicated): 42
% 0.39/0.60 Number of grows: 6
% 0.39/0.60 Number of considered ground atoms: 184
% 0.39/0.60
% 0.39/0.60 Needed: 0:00:00.03
% 0.39/0.60
%------------------------------------------------------------------------------