%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO634-1 : TPTP v9.2.1. Released v7.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:13 PM UTC 2026
% Result : Unsatisfiable 0.41s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO634-1 : TPTP v9.2.1. Released v7.1.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 : n006.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:54:47 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.41/0.56 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/0.56 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/0.56 Execution normal ended with status: unsatisfiable
% 0.41/0.56 Used heuristic: normal
% 0.41/0.56
% 0.41/0.56 Input Clauses:
% 0.41/0.56
% 0.41/0.56 Predicates: 'E' 'LEQ'
% 0.41/0.56 Fol Constants: '0'
% 0.41/0.56 Fol Functions: f s 'AP'
% 0.41/0.56 Problem Properties:
% 0.41/0.56 This is a full first-order problem without equality.
% 0.41/0.56
% 0.41/0.56 After reduction: Problem Properties:
% 0.41/0.56 This is a full first-order problem without equality.
% 0.41/0.56
% 0.41/0.56
% 0.41/0.56 Reduced Input Clauses:
% 0.41/0.56 25:1:1:[9.0,1.0,3.0,24.1]:Top: -> 'E'(f(x0),s(s(s(s(s(s(s(s('0')))))))))
% 0.41/0.56 28:8:8:[25.2,2.0,3.0,26.3,9.0,27.8]:TopTopTopTopTopTopTopTop: 'E'(f(x0),s(s(s(s(s('0')))))),'E'(f(x1),s('0')),'E'(f(x2),s(s(s(s('0'))))),'E'(f(x3),s(s('0'))),'E'(f(x4),s(s(s(s(s(s(s('0')))))))),'E'(f(x5),s(s(s('0')))),'E'(f(x6),s(s(s(s(s(s('0'))))))) -> 'LEQ'('AP'('0',x7),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x7))
% 0.41/0.56 31:6:6:[25.2,4.0,3.0,29.2,9.0,30.6]:TopTopTopTopTopTop: 'E'(f(x0),s(s(s(s(s('0')))))),'E'(f(x1),s(s(s(s('0'))))),'E'(f(x2),s(s(s(s(s(s(s('0')))))))),'E'(f(x3),s(s(s('0')))),'E'(f(x4),s(s(s(s(s(s('0'))))))) -> 'LEQ'('AP'(s(s('0')),x5),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x5))
% 0.41/0.56 33:1:2:[9.0,5.0,3.0,32.1]:TopTop: -> 'LEQ'('AP'(s(s(s(s(s(s(s(s('0')))))))),x0),x1)
% 0.41/0.56 36:2:2:[9.0,6.0,3.0,34.1,25.2,35.2]:TopTop: 'E'(f(x0),s(s(s(s(s(s(s('0')))))))) -> 'E'(f(x1),s(s(s(s(s(s('0')))))))
% 0.41/0.56 40:4:4:[25.2,7.0,3.0,37.2,9.0,38.5,36.4,39.6]:TopTopTopTop: 'E'(f(x0),s(s(s(s(s('0')))))),'E'(f(x1),s(s(s(s('0'))))),'E'(f(x2),s(s(s(s(s(s(s('0')))))))) -> 'LEQ'('AP'(s(s(s('0'))),x3),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x3))
% 0.41/0.56 44:3:3:[25.2,8.0,3.0,41.2,9.0,42.4,36.4,43.5]:TopTopTop: 'E'(f(x0),s(s(s(s(s('0')))))),'E'(f(x1),s(s(s(s(s(s(s('0')))))))) -> 'LEQ'('AP'(s(s(s(s('0')))),x2),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x2))
% 0.41/0.56 48:6:6:[25.2,10.0,3.0,45.2,9.0,46.7,36.4,47.8]:TopTopTopTopTopTop: 'E'(f(x0),s(s(s(s(s('0')))))),'E'(f(x1),s(s(s(s('0'))))),'E'(f(x2),s(s('0'))),'E'(f(x3),s(s(s(s(s(s(s('0')))))))),'E'(f(x4),s(s(s('0')))) -> 'LEQ'('AP'(s('0'),x5),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x5))
% 0.41/0.56 52:6:6:[25.2,11.0,3.0,49.2,9.0,50.7,36.4,51.8]:TopTopTopTopTopTop: 'E'(f(x0),s(s(s(s(s('0')))))),'E'(f(x1),s(s(s(s('0'))))),'E'(f(x2),s(s('0'))),'E'(f(x3),s(s(s(s(s(s(s('0')))))))),'E'(f(x4),s(s(s('0')))) -> 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x5)),s('0'))
% 0.41/0.56 56:3:3:[25.2,12.0,3.0,53.2,9.0,54.4,36.4,55.5]:TopTopTop: 'E'(f(x0),s(s(s(s(s('0')))))),'E'(f(x1),s(s(s(s(s(s(s('0')))))))) -> 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x2)),s(s(s(s('0')))))
% 0.41/0.56 59:1:1:[9.0,14.0,3.0,57.1,25.2,58.2]:Top: -> 'E'(f(x0),s(s(s(s(s(s(s('0'))))))))
% 0.41/0.56 63:4:4:[25.2,15.0,3.0,60.2,59.3,61.4,9.0,62.5]:TopTopTopTop: 'E'(f(x0),s(s(s(s(s('0')))))),'E'(f(x1),s(s(s(s('0'))))),'E'(f(x2),s(s(s(s(s(s('0'))))))) -> 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x3)),s(s(s('0'))))
% 0.41/0.56 67:1:2:[9.0,16.0,3.0,64.1,25.2,65.2,59.3,66.3]:TopTop: -> 'LEQ'('AP'(s(s(s(s(s(s('0')))))),x0),x1)
% 0.41/0.56 71:7:7:[25.2,17.0,3.0,68.3,59.3,69.6,9.0,70.8]:TopTopTopTopTopTopTop: 'E'(f(x0),s(s(s(s(s('0')))))),'E'(f(x1),s('0')),'E'(f(x2),s(s(s(s('0'))))),'E'(f(x3),s(s('0'))),'E'(f(x4),s(s(s('0')))),'E'(f(x5),s(s(s(s(s(s('0'))))))),'E'(f(x6),'0') ->
% 0.41/0.56 74:1:2:[9.0,18.0,3.0,72.1,25.2,73.2]:TopTop: -> 'LEQ'('AP'(s(s(s(s(s(s(s('0'))))))),x0),x1)
% 0.41/0.56 78:5:5:[25.2,19.0,3.0,75.2,59.3,76.4,9.0,77.6]:TopTopTopTopTop: 'E'(f(x0),s(s(s(s(s('0')))))),'E'(f(x1),s(s(s(s('0'))))),'E'(f(x2),s(s(s('0')))),'E'(f(x3),s(s(s(s(s(s('0'))))))) -> 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x4)),s(s('0')))
% 0.41/0.56 82:2:2:[25.2,20.0,3.0,79.1,59.3,80.2,9.0,81.3]:TopTop: 'E'(f(x0),s(s(s(s(s(s('0'))))))) -> 'E'(f(x1),s(s(s(s(s('0'))))))
% 0.41/0.56 86:2:3:[25.2,21.0,3.0,83.1,59.3,84.2,9.0,85.3]:TopTopTop: 'E'(f(x0),s(s(s(s(s(s('0'))))))) -> 'LEQ'('AP'(s(s(s(s(s('0'))))),x1),x2)
% 0.41/0.56 91:6:6:[25.2,22.0,82.5,87.1,3.0,88.3,59.3,89.6,9.0,90.8]:TopTopTopTopTopTop: 'E'(f(x0),s('0')),'E'(f(x1),s(s(s(s('0'))))),'E'(f(x2),s(s('0'))),'E'(f(x3),s(s(s('0')))),'E'(f(x4),s(s(s(s(s(s('0'))))))) -> 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x5)),'0')
% 0.41/0.56
% 0.41/0.56 Most General Atoms: 'E'(f(x0),s(s(s(s(s(s(s(s('0'))))))))) 'LEQ'('AP'('0',x7),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x7)) 'E'(f(x0),s(s(s(s(s(s(s(s(s(s('0'))))))))))) 'E'(f(x1),s(s(s(s('0'))))) 'LEQ'('AP'(s(s('0')),x5),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x5)) 'LEQ'('AP'(s(s(s(s(s(s(s(s('0')))))))),x0),x1) 'LEQ'('AP'(s(s(s('0'))),x3),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x3)) 'LEQ'('AP'(s(s(s(s('0')))),x2),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x2)) 'E'(f(x0),s(s(s(s(s(s(s(s(s('0')))))))))) 'E'(f(x2),s(s('0'))) 'E'(f(x3),s(s(s(s(s(s(s('0')))))))) 'LEQ'('AP'(s('0'),x5),'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),x5)) 'LEQ'('AP'(s(s(s(s(s(s(s(s(s('0'))))))))),x0),x1) 'LEQ'('AP'(s(s(s(s(s(s('0')))))),x0),x1) 'E'(f(x6),'0') 'LEQ'('AP'(s(s(s(s(s(s(s('0'))))))),x0),x1) 'E'(f(x2),s(s(s('0')))) 'E'(f(x0),s(s(s(s(s(s('0'))))))) 'E'(f(x1),s(s(s(s(s('0')))))) 'LEQ'('AP'(s(s(s(s(s('0'))))),x1),x2) 'E'(f(x0),s('0')) 'LEQ'('AP'(s(s(s(s(s(s(s(s(s(s('0')))))))))),x0),x1)
% 0.41/0.56
% 0.41/0.56 === Starting SPASS-SCL-FOL A Little Less Naive, considering 54 atoms initially, heuristics mode: normal ===
% 0.41/0.56
% 0.41/0.56 === Conflict found: 71:7:7:[25.2,17.0,3.0,68.3,59.3,69.6,9.0,70.8]:TopTopTopTopTopTopTop: 'E'(f(x0),s(s(s(s(s('0')))))),'E'(f(x1),s('0')),'E'(f(x2),s(s(s(s('0'))))),'E'(f(x3),s(s('0'))),'E'(f(x4),s(s(s('0')))),'E'(f(x5),s(s(s(s(s(s('0'))))))),'E'(f(x6),'0') -> {x0 -> f('0'), x1 -> 'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),'0'), x2 -> 'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),'0'), x3 -> 'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),f('0')), x4 -> 'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),'0'), x5 -> '0', x6 -> 'AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),f('0'))}
% 0.41/0.56
% 0.41/0.56 SZS status Unsatisfiable
% 0.41/0.56
% 0.41/0.56 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/0.56
% 0.41/0.56 SPASS-SCL-FOL Statistics:
% 0.41/0.56 Number of learned clauses: 0
% 0.41/0.56 Number of propagations: 39
% 0.41/0.56 Number of decisions: 0
% 0.41/0.56 Number of resolutions: 13
% 0.41/0.56 Number of condensations: 0
% 0.41/0.56 Number of sub resolutions: 68
% 0.41/0.56 Number of input literals (deduplicated): 27
% 0.41/0.56 Number of grows: 0
% 0.41/0.56 Number of considered ground atoms: 54
% 0.41/0.56
% 0.41/0.56 Needed: 0:00:00.03
% 0.41/0.56
%------------------------------------------------------------------------------