%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO676-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 : n026.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.82s 0.68s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SYO676-1 : TPTP v9.2.1. Released v7.3.0.
% 0.12/0.14 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n026.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.35 % DateTime : Thu May 7 13:56:24 EDT 2026
% 0.15/0.35 % CPUTime :
% 0.15/0.35 SPASS-SCL-FOL version:
% 0.19/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.82/0.68 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.68 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.68 Execution resolution_1 ended with status: unsatisfiable
% 0.82/0.68 Used heuristic: resolution_1
% 0.82/0.68
% 0.82/0.68 Input Clauses:
% 0.82/0.68
% 0.82/0.68 Predicates: 'E' 'LE'
% 0.82/0.68 Fol Constants: '0' z
% 0.82/0.68 Fol Functions: f suc s
% 0.82/0.68 Problem Properties:
% 0.82/0.68 This is a full first-order problem without equality.
% 0.82/0.68
% 0.82/0.68 After reduction: Problem Properties:
% 0.82/0.68 This is a full first-order problem without equality.
% 0.82/0.68
% 0.82/0.68
% 0.82/0.68 Reduced Input Clauses:
% 0.82/0.68 48:5:1:[40.4,1.0,17.2,47.3]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.82/0.68 49:4:1:[9.2,2.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.82/0.68 52:6:1:[12.6,5.0,37.4,50.4,46.2,51.5]:Top: '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'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 0.82/0.68 55:7:1:[22.8,8.0,9.2,53.2,49.4,54.8]:Top: 'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)) ->
% 0.82/0.68 57:5:1:[37.4,12.3,46.2,56.4]:Top: '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'(s(s(s('0'))),f(suc(x0))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.82/0.68 59:8:1:[35.4,13.0,41.2,58.9]:Top: 'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) ->
% 0.82/0.68 61:5:1:[9.2,14.0,49.4,60.4]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.82/0.68 62:2:1:[7.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 65:6:1:[9.2,22.0,61.6,63.4,49.4,64.6]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 0.82/0.68 67:7:1:[35.4,23.0,41.2,66.7]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 0.82/0.68 69:5:1:[35.4,25.0,41.2,68.5]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.82/0.68 72:6:1:[40.4,30.0,17.2,70.4,48.6,71.6]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 0.82/0.68 76:6:1:[40.4,32.1,17.2,73.5,72.8,74.7,48.6,75.8]:Top: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) ->
% 0.82/0.68 80:6:1:[57.6,33.0,37.4,77.5,46.2,78.6,52.8,79.7]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) ->
% 0.82/0.68 81:4:1:[41.2,35.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.82/0.68 82:4:1:[46.2,37.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.82/0.68 83:4:1:[17.2,40.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.82/0.68
% 0.82/0.68 Most General Atoms: 'E'(s('0'),f(x0)) 'E'(f(x0),f(suc(suc(suc(x0))))) 'E'('0',f(x0)) 'E'(f(x0),f(suc(suc(x0)))) 'LE'(f(x0),s(s(s('0')))) 'LE'(f(x0),s('0')) 'E'(s(s(s('0'))),f(x0)) 'E'(f(x0),f(suc(suc(suc(suc(x0)))))) 'LE'(f(x0),'0') 'LE'(f(x0),s(s(s(s('0'))))) 'E'(f(x0),f(suc(x0))) 'E'(s(s('0')),f(x0)) 'LE'(f(x0),s(s('0')))
% 0.82/0.68
% 0.82/0.68 === Starting SPASS-SCL-FOL A Little Less Naive, considering 24 atoms initially, heuristics mode: resolution_1 ===
% 0.82/0.68
% 0.82/0.68 === Conflict found: 62:2:1:[7.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> '0'}
% 0.82/0.68 === Backtracking. Learning clause 84:3:1:[62.2,44.1]:Top: -> 'E'(s(s(s('0'))),f(x0)),'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Conflict found: 62:2:1:[7.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc('0')}
% 0.82/0.68 === Backtracking. Learning clause 85:3:1:[62.2,29.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Conflict found: 62:2:1:[7.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc('0'))}
% 0.82/0.68 === Backtracking. Learning clause 86:3:1:[62.2,45.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Conflict found: 62:2:1:[7.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc('0')))}
% 0.82/0.68 === Backtracking. Learning clause 87:3:1:[62.2,38.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Conflict found: 62:2:1:[7.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc(suc('0'))))}
% 0.82/0.68 === Backtracking. Learning clause 88:3:1:[62.2,26.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Conflict found: 62:2:1:[7.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc(suc(suc('0')))))}
% 0.82/0.68 === Backtracking. Learning clause 89:7:1:[62.2,15.1,80.2,88.1]:Top: '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'(s(s(s('0'))),f(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(x0),s(s('0')))
% 0.82/0.68 === Backtracking. Learning clause 90:6:1:[42.1,7.1,80.2,26.1,88.1,87.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(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(x0),s(s('0')))
% 0.82/0.68 === Backtracking. Learning clause 91:2:1:[42.1,7.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Conflict found: 62:2:1:[7.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc(suc(suc('0')))))}
% 0.82/0.68 === Backtracking. Learning clause 93:6:1:[62.0,92.0,62.2,15.1,80.2,91.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0'))))
% 0.82/0.68 === Backtracking. Learning clause 94:5:1:[36.1,7.1,80.2,91.1,38.1,87.1,86.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Conflict found: 91:2:1:[42.1,7.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc(suc('0'))))}
% 0.82/0.68 === Backtracking. Learning clause 96:5:1:[62.0,95.1,91.1,80.2,26.1,88.1,91.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(x0))),s(s(s('0'))))
% 0.82/0.68 === Backtracking. Learning clause 97:2:1:[36.1,7.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Conflict found: 62:2:1:[7.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc(suc(suc('0')))))}
% 0.82/0.68 === Backtracking. Learning clause 99:6:1:[62.0,98.2,62.2,15.1,80.2,97.1]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(x0))),s(s(s('0'))))
% 0.82/0.68 === Backtracking. Learning clause 101:4:1:[62.0,100.0,11.1,7.1,80.2,97.1,97.1,45.1,97.1,29.1,85.1]:Top: -> 'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0')))),'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Conflict found: 80:6:1:[57.6,33.0,37.4,77.5,46.2,78.6,52.8,79.7]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) -> {x0 -> '0'}
% 0.82/0.68 === Backtracking. Learning clause 104:4:1:[62.0,102.0,62.0,103.1,80.2,97.1,91.1,38.1,97.1,97.1]:Top: -> 'E'(s(s('0')),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Conflict found: 91:2:1:[42.1,7.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc(suc('0'))))}
% 0.82/0.68 === Backtracking. Learning clause 106:5:1:[62.0,105.2,91.1,80.2,26.1,88.1,97.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> 'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(x0)),s(s(s('0'))))
% 0.82/0.68 === Backtracking. Learning clause 107:2:1:[11.1,7.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Conflict found: 62:2:1:[7.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc(suc(suc('0')))))}
% 0.82/0.68 === Backtracking. Learning clause 109:6:1:[62.0,108.3,62.2,15.1,80.2,107.1]:Top: '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'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(x0)),s(s(s('0'))))
% 0.82/0.68 === Backtracking. Learning clause 110:3:1:[3.1,7.1,80.2,107.1,107.1,97.1,29.1,85.1,44.1,84.1]:Top: -> 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Conflict found: 80:6:1:[57.6,33.0,37.4,77.5,46.2,78.6,52.8,79.7]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) -> {x0 -> '0'}
% 0.82/0.68 === Backtracking. Learning clause 112:3:1:[62.0,111.0,80.2,107.1,97.1,107.1,45.1,97.1,91.1]:Top: -> 'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0'))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Conflict found: 80:6:1:[57.6,33.0,37.4,77.5,46.2,78.6,52.8,79.7]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) -> {x0 -> '0'}
% 0.82/0.68 === Backtracking. Learning clause 115:3:1:[62.0,113.0,91.0,114.1,80.2,97.1,91.1,38.1,107.1,97.1]:Top: -> 'E'(s(s('0')),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s('0'))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Conflict found: 91:2:1:[42.1,7.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc(suc('0'))))}
% 0.82/0.68 === Backtracking. Learning clause 119:3:1:[62.0,116.0,97.0,117.1,91.0,118.2,91.1,80.2,26.1,88.1,107.1]:Top: -> 'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s('0'))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Backtracking. Learning clause 120:2:1:[3.1,7.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Conflict found: 62:2:1:[7.0,20.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0')))) {x0 -> suc(suc(suc(suc(suc('0')))))}
% 0.82/0.68 === Backtracking. Learning clause 125:3:1:[107.0,121.0,62.0,122.1,97.0,123.2,91.0,124.3,62.2,15.1,80.2,120.1]:Top: -> 'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(x0),s(s('0'))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Backtracking. Learning clause 126:2:1:[27.1,7.1,80.2,120.1,107.1,97.1,91.1,44.1,84.1]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Clause set with instances from active satisfied. Growing active. New size: 46
% 0.82/0.68 === Restarting.
% 0.82/0.68 === Conflict found: 126:2:1:[27.1,7.1,80.2,120.1,107.1,97.1,91.1,44.1,84.1]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0'))) {x0 -> '0'}
% 0.82/0.68 === Backtracking. Learning clause 127:3:1:[126.2,43.1]:Top: -> 'E'(s(s('0')),f(x0)),'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 0.82/0.68 === Conflict found: 126:2:1:[27.1,7.1,80.2,120.1,107.1,97.1,91.1,44.1,84.1]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0'))) {x0 -> suc(suc(suc('0')))}
% 0.82/0.68 === Backtracking. Learning clause 128:3:1:[126.2,24.1]:Top: -> 'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 0.82/0.68 === Clause set with instances from active satisfied. Growing active. New size: 51
% 0.82/0.68 === Restarting.
% 0.82/0.68 === Backtracking. Learning clause 130:2:1:[62.0,129.0,46.2,91.1]:Top: -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Conflict found: 82:4:1:[46.2,37.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 -> suc(suc('0'))}
% 0.82/0.68 === Backtracking. Learning clause 133:2:1:[91.0,131.0,62.0,132.1,82.1,97.1]:Top: -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Clause set with instances from active satisfied. Growing active. New size: 115
% 0.82/0.68 === Conflict found: 80:6:1:[57.6,33.0,37.4,77.5,46.2,78.6,52.8,79.7]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) -> {x0 -> suc(suc(suc('0')))}
% 0.82/0.68 === Backtracking. Learning clause 135:4:1:[62.0,134.0,80.1,120.1,120.1,120.1,107.1,29.1,97.1]:Top: -> 'LE'(f(suc(x0)),s(s(s('0')))),'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Conflict found: 80:6:1:[57.6,33.0,37.4,77.5,46.2,78.6,52.8,79.7]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) -> {x0 -> suc(suc('0'))}
% 0.82/0.68 === Backtracking. Learning clause 137:3:1:[62.0,136.0,80.2,107.1,120.1,29.1,91.1,107.1,97.1]:Top: -> 'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Conflict found: 80:6:1:[57.6,33.0,37.4,77.5,46.2,78.6,52.8,79.7]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) -> {x0 -> suc(suc('0'))}
% 0.82/0.68 === Backtracking. Learning clause 142:2:1:[107.0,138.0,62.0,139.1,62.0,140.2,91.0,141.3,80.6,120.1,107.1]:Top: -> 'LE'(f(x0),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0'))))
% 0.82/0.68 === Backtracking. Learning clause 143:4:1:[29.3,43.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))) -> 'E'(s(s('0')),f(suc(x0))),'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 0.82/0.68 === Clause set with instances from active satisfied. Growing active. New size: 179
% 0.82/0.68 === Backtracking. Learning clause 145:1:1:[62.0,144.0,27.1,7.1,80.2,120.1,91.1,107.1,97.1]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 0.82/0.68 === Clause set with instances from active satisfied. Growing active. New size: 243
% 0.82/0.68 === Backtracking. Learning clause 146:3:1:[44.3,31.1,145.1]:Top: -> 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 0.82/0.68 === Conflict found: 69:5:1:[35.4,25.0,41.2,68.5]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> suc(suc(z))}
% 0.82/0.68 === Backtracking. Learning clause 150:4:1:[146.0,147.0,145.0,148.2,145.0,149.3,69.2,45.2,29.2,31.1]:Top: 'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))) -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(suc(suc(x0))))))),'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 0.82/0.68 === Conflict found: 69:5:1:[35.4,25.0,41.2,68.5]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> suc(suc(z))}
% 0.82/0.68 === Backtracking. Learning clause 153:9:1:[145.0,151.1,145.0,152.2,69.1,29.2,45.2,4.1,6.1,9.2,19.2,150.4,48.3,43.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),'0'),'E'(f(suc(suc(x0))),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(suc(suc(suc(suc(x0))))),s('0'))
% 0.82/0.68 === Conflict found: 48:5:1:[40.4,1.0,17.2,47.3]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> suc(suc(z))}
% 0.82/0.68 === Backtracking. Learning clause 154:6:1:[48.3,150.3,39.2]:Top: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))) -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(x0),s('0'))
% 0.82/0.68 === Backtracking. Learning clause 155:4:1:[9.1,19.2,6.2]:Top: 'LE'(f(x0),s('0')),'LE'(f(suc(x0)),s('0')) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),'0')
% 0.82/0.68 === Clause set with instances from active satisfied. Growing active. New size: 307
% 0.82/0.68 === Conflict found: 48:5:1:[40.4,1.0,17.2,47.3]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> suc(suc(suc(suc('0'))))}
% 0.82/0.68 === Backtracking. Learning clause 157:5:1:[145.0,156.2,48.1,146.2,4.2,29.3]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'LE'(f(suc(x0)),s('0')),'E'(s(s('0')),f(suc(suc(suc(x0)))))
% 0.82/0.68 === Conflict found: 83:4:1:[17.2,40.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)))) {x0 -> f('0')}
% 0.82/0.68 === Backtracking. Learning clause 158:5:1:[83.2,4.2,43.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(x0),s(s('0'))) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 0.82/0.68 === Conflict found: 69:5:1:[35.4,25.0,41.2,68.5]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> z}
% 0.82/0.68 === Backtracking. Learning clause 160:7:1:[145.0,159.2,69.3,127.1,143.2,48.3]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))) -> 'LE'(f(x0),s('0')),'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.82/0.68 === Conflict found: 59:8:1:[35.4,13.0,41.2,58.9]:Top: 'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> {x0 -> z}
% 0.82/0.68 === Backtracking. Learning clause 162:8:1:[145.0,161.6,59.7,127.1,143.2]:Top: 'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 0.82/0.68 === Clause set with instances from active satisfied. Growing active. New size: 371
% 0.82/0.68 === Backtracking. Learning clause 163:2:1:[29.1,145.1]:Top: -> 'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Backtracking. Learning clause 164:3:1:[43.1,163.2]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0')),'E'(s(s('0')),f(suc(x0)))
% 0.82/0.68 === Clause set with instances from active satisfied. Growing active. New size: 435
% 0.82/0.68 === Clause set with instances from active satisfied. Growing active. New size: 499
% 0.82/0.68 === Clause set with instances from active satisfied. Growing active. New size: 563
% 0.82/0.68 === Backtracking. Learning clause 165:2:1:[15.1,145.1]:Top: -> 'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Backtracking. Learning clause 166:4:1:[17.2,24.2,31.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 0.82/0.68 === Conflict found: 76:6:1:[40.4,32.1,17.2,73.5,72.8,74.7,48.6,75.8]:Top: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) -> {x0 -> s('0')}
% 0.82/0.68 === Backtracking. Learning clause 167:7:1:[76.5,43.2,39.2,4.2,18.2,24.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(suc(suc(x0)))))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.82/0.68 === Clause set with instances from active satisfied. Growing active. New size: 627
% 0.82/0.68 === Backtracking. Learning clause 168:2:1:[45.1,145.1]:Top: -> 'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Conflict found: 67:7:1:[35.4,23.0,41.2,66.7]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))) {x0 -> z}
% 0.82/0.68 === Backtracking. Learning clause 169:2:1:[67.7,162.3,26.2,145.1,69.5,38.2,145.1,165.1,168.1,43.1,127.1,164.3]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 0.82/0.68 === Conflict found: 67:7:1:[35.4,23.0,41.2,66.7]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))) {x0 -> s(z)}
% 0.82/0.68 === Backtracking. Learning clause 170:1:1:[67.7,59.4,26.2,145.1,69.5,38.2,168.1,145.1,163.1,126.1,165.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 0.82/0.68 === Backtracking. Learning clause 171:2:1:[24.1,170.1]:Top: -> 'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 0.82/0.68 === Backtracking. Learning clause 172:1:1:[31.1,170.1,76.6,4.2,170.1,18.2,170.1,39.2,170.1,169.1,171.1]:Top: -> 'LE'(f(x0),s('0'))
% 0.82/0.68 === Conflict found: 61:5:1:[9.2,14.0,49.4,60.4]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> z}
% 0.82/0.68 === Backtracking. Learning clause 173:5:0:[61.2,28.2,16.2,19.2,21.1]:: 'E'('0',f(suc(z))),'LE'(f(suc(suc(z))),s('0')),'LE'(f(suc(suc(suc(z)))),s('0')),'LE'(f(z),s('0')) -> 'E'(f(z),f(suc(suc(suc(z)))))
% 0.82/0.68 === Backtracking. Learning clause 174:3:0:[6.3,21.1,173.1,172.1,172.1]:: 'LE'(f(suc(z)),s('0')),'LE'(f(z),s('0')) -> 'E'(f(z),f(suc(suc(suc(z)))))
% 0.82/0.68 === Conflict found: 55:7:1:[22.8,8.0,9.2,53.2,49.4,54.8]:Top: 'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> {x0 -> z}
% 0.82/0.68
% 0.82/0.68 SZS status Unsatisfiable
% 0.82/0.68
% 0.82/0.68 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.68
% 0.82/0.68 SPASS-SCL-FOL Statistics:
% 0.82/0.68 Number of learned clauses: 55
% 0.82/0.68 Number of propagations: 2799
% 0.82/0.68 Number of decisions: 1103
% 0.82/0.68 Number of resolutions: 206
% 0.82/0.68 Number of condensations: 0
% 0.82/0.68 Number of sub resolutions: 73
% 0.82/0.68 Number of input literals (deduplicated): 54
% 0.82/0.68 Number of grows: 11
% 0.82/0.68 Number of considered ground atoms: 627
% 0.82/0.68
% 0.82/0.68 Needed: 0:00:00.13
% 0.82/0.68
%------------------------------------------------------------------------------