%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO684-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 : n002.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:17 PM UTC 2026
% Result : Unsatisfiable 0.73s 0.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO684-1 : TPTP v9.2.1. Released v7.3.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n002.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:56:17 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.73/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.73/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.73/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.73/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.73/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.73/0.63 Execution resolution_2 ended with status: unsatisfiable
% 0.73/0.63 Used heuristic: resolution_2
% 0.73/0.63
% 0.73/0.63 Input Clauses:
% 0.73/0.63
% 0.73/0.63 Predicates: 'E' 'LE'
% 0.73/0.63 Fol Constants: '0' z
% 0.73/0.63 Fol Functions: s suc f
% 0.73/0.63 Problem Properties:
% 0.73/0.63 This is a full first-order problem without equality.
% 0.73/0.63
% 0.73/0.63 After reduction: Problem Properties:
% 0.73/0.63 This is a full first-order problem without equality.
% 0.73/0.63
% 0.73/0.63
% 0.73/0.63 Reduced Input Clauses:
% 0.73/0.63 49:6:1:[18.4,1.2,28.2,48.4]:Top: '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)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(x0)) ->
% 0.73/0.63 51:5:1:[23.4,7.0,45.2,50.5]:Top: 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.73/0.63 52:7:1:[22.2,9.0]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) ->
% 0.73/0.63 54:5:1:[19.4,12.2,36.2,53.4]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.73/0.63 55:4:1:[22.2,15.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.73/0.63 56:4:1:[28.2,18.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.73/0.63 57:4:1:[36.2,19.2]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.73/0.63 58:4:1:[2.2,20.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.73/0.63 59:4:1:[45.2,23.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.73/0.63 61:5:1:[22.2,25.0,55.4,60.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.73/0.63 64:5:1:[59.4,26.0,51.6,62.5,45.2,63.7]:Top: 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'E'(s(s(s('0'))),f(suc(suc(x0)))) ->
% 0.73/0.63 66:6:1:[2.2,27.5,58.4,65.7]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(suc(suc(x0))))) ->
% 0.73/0.63 69:5:1:[54.6,33.0,57.4,67.3,36.2,68.5]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(x0)))))),'E'(s(s(s(s('0')))),f(x0)) ->
% 0.73/0.63 70:2:1:[35.0,34.0]:Top: -> 'E'(s(s(s(s('0')))),f(x0)),'LE'(f(x0),s(s(s(s('0')))))
% 0.73/0.63 72:5:1:[2.2,46.4,58.4,71.5]:Top: 'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.73/0.63 74:5:1:[56.4,47.1,28.2,73.3]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.73/0.63
% 0.73/0.63 Most General Atoms: 'E'(f(x0),f(suc(suc(suc(x0))))) 'E'(s(s('0')),f(x0)) 'E'('0',f(x0)) 'E'(f(x0),f(suc(x0))) 'LE'(f(x0),s(s(s('0')))) 'LE'(f(x0),s(s(s(s('0'))))) 'LE'(f(x0),s(s('0'))) 'E'(s(s(s('0'))),f(x0)) 'E'(f(x0),f(suc(suc(x0)))) 'E'(s('0'),f(x0)) 'E'(s(s(s(s('0')))),f(x0)) 'LE'(f(x0),'0') 'LE'(f(x0),s('0')) 'LE'(f(x0),s(s(s(s(s('0'))))))
% 0.73/0.63
% 0.73/0.63 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: resolution_2 ===
% 0.73/0.63
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 65
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Backtracking. Learning clause 75:2:0:[43.3,11.1]:: 'LE'(f(z),s('0')) -> 'E'('0',f(z))
% 0.73/0.63 === Backtracking. Learning clause 76:2:0:[40.3,11.1]:: 'LE'(f(suc(z)),s('0')) -> 'E'('0',f(suc(z)))
% 0.73/0.63 === Backtracking. Learning clause 77:2:0:[38.3,11.1]:: 'LE'(f(suc(suc(z))),s('0')) -> 'E'('0',f(suc(suc(z))))
% 0.73/0.63 === Backtracking. Learning clause 78:2:0:[17.3,11.1]:: 'LE'(f(suc(suc(suc(suc(z))))),s('0')) -> 'E'('0',f(suc(suc(suc(suc(z))))))
% 0.73/0.63 === Backtracking. Learning clause 79:2:0:[13.3,11.1]:: 'LE'(f(suc(suc(suc(z)))),s('0')) -> 'E'('0',f(suc(suc(suc(z)))))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 65
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Backtracking. Learning clause 80:2:1:[24.1,35.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(x0))),'LE'(f(x0),s(s(s(s('0')))))
% 0.73/0.63 === Conflict found: 59:4:1:[45.2,23.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))) {x0 -> '0'}
% 0.73/0.63 === Backtracking. Learning clause 81:5:1:[59.3,6.2,3.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(x0),s(s(s(s('0'))))),'LE'(f(suc(x0)),s(s(s(s('0'))))) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 68
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Conflict found: 81:5:1:[59.3,6.2,3.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(x0),s(s(s(s('0'))))),'LE'(f(suc(x0)),s(s(s(s('0'))))) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc(suc('0'))))}
% 0.73/0.63 === Backtracking. Learning clause 82:5:1:[81.2,70.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s(s(s('0'))))) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0')))),'E'(s(s(s(s('0')))),f(x0))
% 0.73/0.63 === Backtracking. Learning clause 83:3:1:[32.1,70.2]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s(s('0')))),'E'(s(s(s(s('0')))),f(suc(suc(suc(x0)))))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 78
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Backtracking. Learning clause 84:3:0:[42.3,75.1]:: 'LE'(f(suc(z)),s(s('0'))) -> 'E'(s('0'),f(suc(z))),'E'('0',f(z))
% 0.73/0.63 === Backtracking. Learning clause 85:3:0:[41.3,75.1]:: 'LE'(f(suc(suc(suc(z)))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(z))))),'E'('0',f(z))
% 0.73/0.63 === Backtracking. Learning clause 86:3:0:[39.3,75.1]:: 'LE'(f(suc(suc(suc(suc(z))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(z)))))),'E'('0',f(z))
% 0.73/0.63 === Backtracking. Learning clause 87:3:0:[37.3,75.1]:: 'LE'(f(suc(suc(z))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(z)))),'E'('0',f(z))
% 0.73/0.63 === Backtracking. Learning clause 88:3:0:[30.3,75.1]:: 'LE'(f(z),s(s('0'))) -> 'E'(s('0'),f(z)),'E'('0',f(z))
% 0.73/0.63 === Conflict found: 69:5:1:[54.6,33.0,57.4,67.3,36.2,68.5]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(x0)))))),'E'(s(s(s(s('0')))),f(x0)) -> {x0 -> '0'}
% 0.73/0.63 === Backtracking. Learning clause 89:5:1:[69.5,70.1,44.2,80.1,4.2,10.2,6.1]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))) -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 142
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 144
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Backtracking. Learning clause 90:3:0:[39.3,76.1]:: 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(z))))))),'E'('0',f(suc(z)))
% 0.73/0.63 === Backtracking. Learning clause 91:3:0:[30.3,76.1]:: 'LE'(f(suc(z)),s(s('0'))) -> 'E'(s('0'),f(suc(z))),'E'('0',f(suc(z)))
% 0.73/0.63 === Backtracking. Learning clause 92:5:1:[16.1,80.2,64.5,83.1,3.2,10.3]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s('0')))),'E'(s(s(s(s('0')))),f(suc(suc(suc(x0)))))
% 0.73/0.63 === Conflict found: 52:7:1:[22.2,9.0]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> {x0 -> '0'}
% 0.73/0.63 === Backtracking. Learning clause 93:9:1:[52.6,30.2,42.2,43.1]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))) -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 146
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Backtracking. Learning clause 94:3:0:[39.3,77.1]:: 'LE'(f(suc(suc(suc(suc(suc(suc(z))))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(z)))))))),'E'('0',f(suc(suc(z))))
% 0.73/0.63 === Backtracking. Learning clause 95:3:0:[41.3,77.1]:: 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(z))))))),'E'('0',f(suc(suc(z))))
% 0.73/0.63 === Backtracking. Learning clause 96:3:0:[37.3,77.1]:: 'LE'(f(suc(suc(suc(suc(z))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(z)))))),'E'('0',f(suc(suc(z))))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 150
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Backtracking. Learning clause 97:3:0:[39.3,78.1]:: 'LE'(f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(suc(z)))))))))),'E'('0',f(suc(suc(suc(suc(z))))))
% 0.73/0.63 === Backtracking. Learning clause 98:3:0:[41.3,78.1]:: 'LE'(f(suc(suc(suc(suc(suc(suc(suc(z)))))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(z))))))))),'E'('0',f(suc(suc(suc(suc(z))))))
% 0.73/0.63 === Backtracking. Learning clause 99:3:0:[37.3,78.1]:: 'LE'(f(suc(suc(suc(suc(suc(suc(z))))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(z)))))))),'E'('0',f(suc(suc(suc(suc(z))))))
% 0.73/0.63 === Backtracking. Learning clause 100:3:0:[42.3,78.1]:: 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(z))))))),'E'('0',f(suc(suc(suc(suc(z))))))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 150
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Backtracking. Learning clause 101:3:0:[39.3,79.1]:: 'LE'(f(suc(suc(suc(suc(suc(suc(suc(z)))))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(z))))))))),'E'('0',f(suc(suc(suc(z)))))
% 0.73/0.63 === Backtracking. Learning clause 102:3:0:[41.3,79.1]:: 'LE'(f(suc(suc(suc(suc(suc(suc(z))))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(z)))))))),'E'('0',f(suc(suc(suc(z)))))
% 0.73/0.63 === Backtracking. Learning clause 103:3:0:[37.3,79.1]:: 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(z))))))),'E'('0',f(suc(suc(suc(z)))))
% 0.73/0.63 === Backtracking. Learning clause 104:3:0:[30.3,79.1]:: 'LE'(f(suc(suc(suc(z)))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(z))))),'E'('0',f(suc(suc(suc(z)))))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 214
% 0.73/0.63 === Conflict found: 57:4:1:[36.2,19.2]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))) {x0 -> suc(suc(suc(suc('0'))))}
% 0.73/0.63 === Backtracking. Learning clause 105:4:1:[57.2,70.1,70.1]:Top: 'E'(s(s(s(s('0')))),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0')))))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 215
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Backtracking. Learning clause 106:4:1:[44.3,3.1]:Top: 'LE'(f(suc(suc(suc(suc(suc(x0)))))),s(s(s(s(s('0')))))) -> 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Conflict found: 80:2:1:[24.1,35.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(x0))),'LE'(f(x0),s(s(s(s('0'))))) {x0 -> suc('0')}
% 0.73/0.63 === Backtracking. Learning clause 107:3:1:[80.2,3.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Backtracking. Learning clause 108:2:1:[44.1,35.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s(s(s('0')))))
% 0.73/0.63 === Backtracking. Learning clause 109:2:1:[10.1,35.1,69.2,4.2,35.1,70.1,107.1,108.1,3.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Conflict found: 64:5:1:[59.4,26.0,51.6,62.5,45.2,63.7]:Top: 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> {x0 -> suc(suc('0'))}
% 0.73/0.63 === Backtracking. Learning clause 110:5:1:[64.4,32.2,16.2,109.1]:Top: 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s('0'))))) -> 'LE'(f(suc(x0)),s(s(s('0'))))
% 0.73/0.63 === Conflict found: 69:5:1:[54.6,33.0,57.4,67.3,36.2,68.5]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(x0)))))),'E'(s(s(s(s('0')))),f(x0)) -> {x0 -> z}
% 0.73/0.63 === Backtracking. Learning clause 111:3:1:[69.4,108.1,70.1,4.2,80.1,10.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s(s('0')))))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 215
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Backtracking. Learning clause 112:2:1:[4.1,35.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s(s(s('0')))))
% 0.73/0.63 === Conflict found: 64:5:1:[59.4,26.0,51.6,62.5,45.2,63.7]:Top: 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> {x0 -> '0'}
% 0.73/0.63 === Backtracking. Learning clause 117:3:1:[112.1,113.0,4.2,114.1,35.0,115.2,80.1,116.3,64.3,6.2,16.2,83.1,106.3,8.2]:Top: -> 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Conflict found: 52:7:1:[22.2,9.0]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> {x0 -> '0'}
% 0.73/0.63 === Backtracking. Learning clause 118:7:1:[52.7,37.2,61.5,42.2,30.2]:Top: 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(suc(suc(x0))),s('0'))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 216
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Conflict found: 105:4:1:[57.2,70.1,70.1]:Top: 'E'(s(s(s(s('0')))),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s(s(s('0'))))),'LE'(f(suc(suc(x0))),s(s(s(s('0'))))) {x0 -> suc(suc(suc('0')))}
% 0.73/0.63 === Backtracking. Learning clause 119:4:1:[105.1,112.1]:Top: -> 'E'(f(suc(suc(suc(x0)))),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))),'LE'(f(suc(suc(suc(suc(suc(x0)))))),s(s(s(s('0'))))),'LE'(f(x0),s(s(s(s('0')))))
% 0.73/0.63 === Conflict found: 57:4:1:[36.2,19.2]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))) {x0 -> suc(suc(suc('0')))}
% 0.73/0.63 === Backtracking. Learning clause 121:3:1:[70.0,120.0,57.3,112.1,80.1]:Top: -> 'E'(f(suc(suc(suc(x0)))),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(x0),s(s(s(s('0'))))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0')))))
% 0.73/0.63 === Conflict found: 57:4:1:[36.2,19.2]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))) {x0 -> suc('0')}
% 0.73/0.63 === Backtracking. Learning clause 123:3:1:[80.0,122.1,57.1,112.1]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(x0)))) -> 'E'(f(suc(x0)),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s(s(s('0')))))
% 0.73/0.63 === Backtracking. Learning clause 125:2:1:[108.0,124.0,36.1,112.1]:Top: -> 'E'(f(suc(suc(suc(x0)))),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s(s(s('0')))))
% 0.73/0.63 === Conflict found: 111:3:1:[69.4,108.1,70.1,4.2,80.1,10.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s(s('0'))))) {x0 -> '0'}
% 0.73/0.63 === Backtracking. Learning clause 126:1:1:[111.2,35.1,35.1]:Top: -> 'LE'(f(x0),s(s(s(s('0')))))
% 0.73/0.63 === Conflict found: 92:5:1:[16.1,80.2,64.5,83.1,3.2,10.3]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s(s('0')))))) -> 'LE'(f(x0),s(s(s('0')))),'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))) {x0 -> '0'}
% 0.73/0.63 === Backtracking. Learning clause 127:6:1:[92.1,89.4,8.2]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))) -> 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 216
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Conflict found: 127:6:1:[92.1,89.4,8.2]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(x0))),s(s(s(s(s('0')))))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))) -> 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s(s('0')))) {x0 -> '0'}
% 0.73/0.63 === Backtracking. Learning clause 128:2:1:[127.4,126.1,35.1,35.1,35.1]:Top: -> 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Backtracking. Learning clause 129:2:1:[8.1,126.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Backtracking. Learning clause 130:5:1:[28.1,14.2,21.2,30.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))) -> 'E'(f(suc(suc(suc(x0)))),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 0.73/0.63 === Backtracking. Learning clause 131:4:1:[28.1,14.2,21.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))) -> 'E'(f(suc(suc(suc(x0)))),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s('0')))
% 0.73/0.63 === Backtracking. Learning clause 132:4:1:[39.1,31.3,22.2,41.2,5.3]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))) -> 'E'(f(suc(suc(suc(x0)))),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s('0')),'E'(s(s('0')),f(suc(suc(suc(suc(x0))))))
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 280
% 0.73/0.63 === Backtracking. Learning clause 134:5:1:[5.2,133.1,42.1,31.3,22.2,30.2,43.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))) -> 'E'(s(s('0')),f(suc(x0))),'E'(f(x0),f(suc(x0))),'E'('0',f(x0)),'LE'(f(x0),'0')
% 0.73/0.63 === Conflict found: 74:5:1:[56.4,47.1,28.2,73.3]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> z}
% 0.73/0.63 === Backtracking. Learning clause 135:5:1:[74.5,49.5]:Top: '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)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(x0)) ->
% 0.73/0.63 === Clause set with instances from active satisfied. Growing active. New size: 280
% 0.73/0.63 === Restarting.
% 0.73/0.63 === Conflict found: 69:5:1:[54.6,33.0,57.4,67.3,36.2,68.5]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(suc(x0))))),'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(x0)))))),'E'(s(s(s(s('0')))),f(x0)) -> {x0 -> '0'}
% 0.73/0.63 === Backtracking. Learning clause 136:5:1:[69.1,128.1]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(x0)))),'E'(s(s(s(s('0')))),f(suc(x0))),'E'(s(s(s(s('0')))),f(suc(suc(suc(suc(x0)))))),'E'(s(s(s(s('0')))),f(x0)) -> 'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Backtracking. Learning clause 137:3:1:[36.2,128.1]:Top: 'E'(s(s(s(s('0')))),f(suc(suc(x0)))) -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Backtracking. Learning clause 138:1:1:[32.1,126.1,64.2,16.2,126.1,109.1,6.2,126.1,129.1]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 0.73/0.63 === Backtracking. Learning clause 139:2:1:[21.1,138.1]:Top: -> 'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s('0')))
% 0.73/0.63 === Conflict found: 135:5:1:[74.5,49.5]:Top: '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)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(x0)) -> {x0 -> '0'}
% 0.73/0.63 === Backtracking. Learning clause 141:1:1:[138.0,140.0,135.3,29.2,5.2,138.1,31.2,138.1,14.2,138.1,139.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 0.73/0.63 === Conflict found: 52:7:1:[22.2,9.0]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> {x0 -> '0'}
% 0.73/0.63 === Backtracking. Learning clause 145:1:1:[141.0,142.0,141.0,143.1,141.0,144.2,52.5,55.4,61.5,37.2,141.1,42.2,141.1,30.2,41.2,39.2]:Top: -> 'LE'(f(x0),s('0'))
% 0.73/0.63 === Conflict found: 66:6:1:[2.2,27.5,58.4,65.7]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(suc(suc(x0))))) -> {x0 -> z}
% 0.73/0.63
% 0.73/0.63 SZS status Unsatisfiable
% 0.73/0.63
% 0.73/0.63 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.73/0.63
% 0.73/0.63 SPASS-SCL-FOL Statistics:
% 0.73/0.63 Number of learned clauses: 59
% 0.73/0.63 Number of propagations: 1477
% 0.73/0.63 Number of decisions: 1438
% 0.73/0.63 Number of resolutions: 140
% 0.73/0.63 Number of condensations: 0
% 0.73/0.63 Number of sub resolutions: 39
% 0.73/0.63 Number of input literals (deduplicated): 55
% 0.73/0.63 Number of grows: 16
% 0.73/0.63 Number of considered ground atoms: 280
% 0.73/0.63
% 0.73/0.63 Needed: 0:00:00.11
% 0.73/0.63
%------------------------------------------------------------------------------