%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO658-1 : TPTP v9.2.1. Released v7.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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 0.39s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.13 % Problem : SYO658-1 : TPTP v9.2.1. Released v7.3.0.
% 0.10/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n004.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:18 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.18/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.60 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.60 Execution resolution_2 ended with status: unsatisfiable
% 0.39/0.60 Used heuristic: resolution_2
% 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 36:11:2:[25.11,1.3,32.9,35.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) ->
% 0.39/0.60 38:8:2:[30.7,5.6,12.5,37.7]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(x1)))
% 0.39/0.60 39:9:2:[12.6,6.7]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0)))
% 0.39/0.60 40:10:2:[22.7,9.6]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.60 41:5:1:[33.2,10.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 42:8:2:[29.5,13.5]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 0.39/0.60 45:10:2:[15.11,14.8,38.9,43.9,39.9,44.10]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) ->
% 0.39/0.60 47:10:2:[30.8,15.8,39.9,46.9]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.60 48:10:2:[30.8,16.7]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(x0))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.60 50:5:1:[41.4,17.2,33.2,49.5]:Top: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0))
% 0.39/0.60 51:2:1:[11.0,18.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 0.39/0.60 52:8:2:[12.6,19.6]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.60 54:10:2:[40.9,20.3,22.7,53.8]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.60 55:8:2:[29.6,22.5]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.60 57:8:2:[42.7,23.2,29.5,56.7]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1)))
% 0.39/0.60 60:9:2:[48.9,24.7,38.9,58.8,52.7,59.9]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.39/0.60 62:10:2:[40.10,25.7,42.8,61.9]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.60 63:5:1:[4.2,26.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)))),iLEQ(suc(x0),suc(x0))
% 0.39/0.60 64:8:2:[12.5,30.6]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 0.39/0.60 66:8:2:[55.8,32.6,29.6,65.7]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0)))
% 0.39/0.60 68:5:1:[63.4,34.3,4.2,67.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0))
% 0.39/0.60
% 0.39/0.60 Most General Atoms: iLEQ(suc(x0),suc(x1)) 'E'('0',f(x1)) 'LE'(f(x0),s('0')) 'E'(f(x0),f(suc(x0))) 'E'(s('0'),f(x1)) 'LE'(f(x0),'0') 'E'(f(x0),f(suc(suc(x0)))) 'LE'(f(x0),s(s('0')))
% 0.39/0.60
% 0.39/0.60 === Starting SPASS-SCL-FOL A Little Less Naive, considering 64 atoms initially, heuristics mode: resolution_2 ===
% 0.39/0.60
% 0.39/0.60 === Clause set with instances from active satisfied. Growing active. New size: 64
% 0.39/0.60 === Restarting.
% 0.39/0.60 === Backtracking. Learning clause 69:2:0:[31.3,8.1]:: 'LE'(f(suc(z)),s('0')) -> 'E'('0',f(suc(z)))
% 0.39/0.60 === Backtracking. Learning clause 70:2:0:[27.3,8.1]:: 'LE'(f(z),s('0')) -> 'E'('0',f(z))
% 0.39/0.60 === Backtracking. Learning clause 71:2:0:[21.3,8.1]:: 'LE'(f(suc(suc(suc(z)))),s('0')) -> 'E'('0',f(suc(suc(suc(z)))))
% 0.39/0.60 === Backtracking. Learning clause 72:2:0:[7.3,8.1]:: 'LE'(f(suc(suc(z))),s('0')) -> 'E'('0',f(suc(suc(z))))
% 0.39/0.60 === Conflict found: 45:10:2:[15.11,14.8,38.9,43.9,39.9,44.10]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> {x0 -> z, x1 -> z}
% 0.39/0.60 === Backtracking. Learning clause 73:4:0:[45.10,60.9,68.5,51.1,28.2,3.2,70.1]:: 'E'(s('0'),f(suc(suc(suc(z))))),'LE'(f(suc(suc(z))),s(s('0'))),'LE'(f(suc(z)),s(s('0'))) -> 'E'('0',f(z))
% 0.39/0.60 === Conflict found: 60:9:2:[48.9,24.7,38.9,58.8,52.7,59.9]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(suc(x1)))) {x0 -> '0', x1 -> '0'}
% 0.39/0.60 === Backtracking. Learning clause 74:4:1:[60.9,45.10,68.5,3.2,2.2,51.1,28.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(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: 73:4:0:[45.10,60.9,68.5,51.1,28.2,3.2,70.1]:: 'E'(s('0'),f(suc(suc(suc(z))))),'LE'(f(suc(suc(z))),s(s('0'))),'LE'(f(suc(z)),s(s('0'))) -> 'E'('0',f(z)) {}
% 0.39/0.60 === Backtracking. Learning clause 75:3:0:[73.2,11.1,2.2,70.1]:: 'LE'(f(suc(z)),s(s('0'))),'LE'(f(suc(suc(suc(z)))),s(s('0'))) -> 'E'('0',f(z))
% 0.39/0.60 === Conflict found: 40:10:2:[22.7,9.6]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> z, x1 -> z}
% 0.39/0.60 === Backtracking. Learning clause 76:5:1:[40.9,36.9,66.8,50.5,31.2,28.3,21.2,51.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(x0)))))
% 0.39/0.60 === Clause set with instances from active satisfied. Growing active. New size: 66
% 0.39/0.60 === Restarting.
% 0.39/0.60 === Backtracking. Learning clause 77:3:0:[2.3,69.1]:: 'LE'(f(suc(suc(suc(suc(z))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(z)))))),'E'('0',f(suc(z)))
% 0.39/0.60 === Conflict found: 48:10:2:[30.8,16.7]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(x0))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> z, x1 -> z}
% 0.39/0.60 === Backtracking. Learning clause 78:5:1:[48.8,64.8,51.1]:Top: iLEQ(suc(x0),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 0.39/0.60 === Backtracking. Learning clause 79:2:1:[28.1,11.1]:Top: -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 0.39/0.60 === Conflict found: 74:4:1:[60.9,45.10,68.5,3.2,2.2,51.1,28.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> suc(z)}
% 0.39/0.60 === Backtracking. Learning clause 80:1:0:[74.1,11.1,11.1,69.1,11.1]:: -> 'E'('0',f(suc(z)))
% 0.39/0.60 === Backtracking. Learning clause 81:2:0:[7.1,3.3,76.1,8.1,70.2,2.3]:: 'LE'(f(suc(suc(suc(z)))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(z)))))
% 0.39/0.60 === Conflict found: 74:4:1:[60.9,45.10,68.5,3.2,2.2,51.1,28.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> z}
% 0.39/0.60 === Backtracking. Learning clause 82:2:1:[74.1,11.1,11.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.39/0.60 === Conflict found: 41:5:1:[33.2,10.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)) {x0 -> z}
% 0.39/0.60 === Backtracking. Learning clause 83:5:1:[41.5,40.5]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.60 === Clause set with instances from active satisfied. Growing active. New size: 70
% 0.39/0.60 === Restarting.
% 0.39/0.60 === Conflict found: 55:8:2:[29.6,22.5]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> z, x1 -> '0'}
% 0.39/0.60 === Backtracking. Learning clause 84:7:1:[55.1,80.1]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(z)),iLEQ(suc(z),suc(x0)),'E'('0',f(x0)),'E'('0',f(suc(x0))) -> 'E'(f(z),f(suc(z))),'E'(f(x0),f(suc(suc(x0))))
% 0.39/0.60 === Backtracking. Learning clause 85:6:1:[29.1,80.1]:Top: 'E'('0',f(z)),iLEQ(suc(z),suc(x0)),'E'('0',f(x0)),'E'('0',f(suc(x0))) -> 'E'(f(z),f(suc(z))),'E'(f(x0),f(suc(x0)))
% 0.39/0.60 === Conflict found: 76:5:1:[40.9,36.9,66.8,50.5,31.2,28.3,21.2,51.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(x0))))) {x0 -> suc(z)}
% 0.39/0.60 === Backtracking. Learning clause 86:4:0:[76.2,80.1]:: 'E'('0',f(suc(suc(suc(z))))),'LE'(f(suc(suc(suc(suc(z))))),s(s('0'))) -> 'LE'(f(suc(z)),'0'),'E'(s('0'),f(suc(suc(suc(suc(z))))))
% 0.39/0.60 === Conflict found: 50:5:1:[41.4,17.2,33.2,49.5]:Top: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 0.39/0.60 === Backtracking. Learning clause 87:4:0:[50.1,80.1]:: 'E'('0',f(suc(suc(z)))),'E'('0',f(z)),'E'('0',f(suc(suc(suc(z))))) -> iLEQ(suc(z),suc(z))
% 0.39/0.60 === Conflict found: 41:5:1:[33.2,10.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)) {x0 -> z}
% 0.39/0.60 === Backtracking. Learning clause 88:4:0:[41.2,80.1]:: 'E'('0',f(suc(suc(z)))),'E'('0',f(z)) -> 'E'(f(z),f(suc(suc(z)))),iLEQ(suc(z),suc(z))
% 0.39/0.60 === Backtracking. Learning clause 89:3:0:[33.1,80.1]:: 'E'('0',f(suc(suc(z)))) -> 'E'(f(suc(z)),f(suc(suc(z)))),iLEQ(suc(suc(z)),suc(suc(z)))
% 0.39/0.60 === Backtracking. Learning clause 90:2:0:[29.3,89.3,80.1]:: 'E'('0',f(suc(suc(z)))) -> 'E'(f(suc(z)),f(suc(suc(z))))
% 0.39/0.60 === Clause set with instances from active satisfied. Growing active. New size: 76
% 0.39/0.60 === Restarting.
% 0.39/0.60 === Conflict found: 74:4:1:[60.9,45.10,68.5,3.2,2.2,51.1,28.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> suc(suc(suc(z)))}
% 0.39/0.60 === Backtracking. Learning clause 91:1:0:[74.4,71.1,11.1,11.1,11.1]:: -> 'E'('0',f(suc(suc(suc(z)))))
% 0.39/0.60 === Conflict found: 36:11:2:[25.11,1.3,32.9,35.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> {x0 -> z, x1 -> z}
% 0.39/0.60 === Backtracking. Learning clause 96:2:0:[91.0,92.0,11.0,93.1,80.0,94.4,8.0,95.5,36.9,83.5,7.2,82.2,85.5]:: iLEQ(suc(z),suc(z)),'E'('0',f(z)) ->
% 0.39/0.60
% 0.39/0.60 SZS status Unsatisfiable
% 0.39/0.60
% 0.39/0.60 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.60
% 0.39/0.60 SPASS-SCL-FOL Statistics:
% 0.39/0.60 Number of learned clauses: 24
% 0.39/0.60 Number of propagations: 284
% 0.39/0.60 Number of decisions: 213
% 0.39/0.60 Number of resolutions: 68
% 0.39/0.60 Number of condensations: 0
% 0.39/0.60 Number of sub resolutions: 38
% 0.39/0.60 Number of input literals (deduplicated): 22
% 0.39/0.60 Number of grows: 4
% 0.39/0.60 Number of considered ground atoms: 76
% 0.39/0.60
% 0.39/0.60 Needed: 0:00:00.05
% 0.39/0.60
%------------------------------------------------------------------------------