%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO673-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 : n025.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 26.57s 5.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO673-1 : TPTP v9.2.1. Released v7.3.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n025.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:14 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 26.57/5.81 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.57/5.81 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.57/5.81 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.57/5.81 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.57/5.81 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.57/5.81 Execution resolution_2 ended with status: unsatisfiable
% 26.57/5.81 Used heuristic: resolution_2
% 26.57/5.81
% 26.57/5.81 Input Clauses:
% 26.57/5.81
% 26.57/5.81 Predicates: 'E' iLEQ 'LE'
% 26.57/5.81 Fol Constants: '0' z
% 26.57/5.81 Fol Functions: s f suc
% 26.57/5.81 Problem Properties:
% 26.57/5.81 This is a full first-order problem without equality.
% 26.57/5.81
% 26.57/5.81 After reduction: Problem Properties:
% 26.57/5.81 This is a full first-order problem without equality.
% 26.57/5.81
% 26.57/5.81
% 26.57/5.81 Reduced Input Clauses:
% 26.57/5.81 66:15:4:[36.12,1.8]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 68:15:4:[63.13,3.8,66.13,67.12]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 69:16:4:[10.13,4.4]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x2)),'E'(s(s('0')),f(suc(x3))),iLEQ(suc(x1),suc(x3)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 70:17:4:[69.15,5.4]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x2)),'E'(f(x2),f(suc(x2))),'E'(s(s('0')),f(suc(x3))),iLEQ(suc(x1),suc(x3)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x3),f(suc(x3)))
% 26.57/5.81 71:4:1:[31.2,7.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 26.57/5.81 72:15:4:[2.11,8.10]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 26.57/5.81 73:15:4:[2.14,9.1]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 26.57/5.81 74:15:4:[52.11,10.8]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x2)),'E'(s(s('0')),f(suc(x3))),iLEQ(suc(x1),suc(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 75:17:4:[35.16,11.1]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'(f(x3),f(suc(x3))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x1),f(suc(x1)))
% 26.57/5.81 76:15:4:[52.12,12.4]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x2)),'E'(s(s('0')),f(suc(x3))),iLEQ(suc(x1),suc(x3)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 78:17:4:[28.17,13.1,75.17,77.5]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'(f(x3),f(suc(x3))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x0)) ->
% 26.57/5.81 79:4:1:[37.2,14.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0))
% 26.57/5.81 80:17:4:[68.15,15.4]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x3),f(suc(x3)))
% 26.57/5.81 81:17:4:[68.16,16.7]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(x3)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x0),f(suc(x0)))
% 26.57/5.81 82:17:4:[47.16,17.4]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(x3)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x2),f(suc(x2)))
% 26.57/5.81 83:16:4:[45.15,19.5]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(f(x1),f(suc(x1))),'E'(s(s('0')),f(x3)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 84:16:4:[72.13,20.3]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'(f(x3),f(suc(x3))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 26.57/5.81 85:16:4:[57.15,23.4]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 26.57/5.81 86:16:4:[76.14,24.4]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x2)),'E'(f(x2),f(suc(x2))),'E'(s(s('0')),f(suc(x3))),iLEQ(suc(x1),suc(x3)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 87:4:1:[32.2,25.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 26.57/5.81 88:15:4:[52.13,27.4]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x2)),'E'(s(s('0')),f(suc(x3))),iLEQ(suc(x1),suc(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 89:17:4:[84.15,28.3]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'(f(x3),f(suc(x3))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x0),f(suc(x0)))
% 26.57/5.81 90:17:4:[58.16,29.1]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x3),f(suc(x3)))
% 26.57/5.81 92:15:4:[49.15,30.1,73.14,91.4]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2)))
% 26.57/5.81 94:15:4:[45.14,33.5,76.15,93.13]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(x3)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 26.57/5.81 95:16:4:[72.14,35.3]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'(f(x3),f(suc(x3))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 26.57/5.81 97:17:4:[42.17,39.5,70.17,96.16]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(f(x3),f(suc(x3))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x0)))) ->
% 26.57/5.81 99:15:4:[72.15,40.1,73.13,98.12]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 26.57/5.81 100:16:4:[63.14,41.4]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 102:16:4:[48.15,42.5,94.15,101.11]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(f(x1),f(suc(x1))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x2),f(suc(x2)))
% 26.57/5.81 104:15:4:[65.15,44.1,73.15,103.4]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1)))
% 26.57/5.81 105:15:4:[52.14,45.11]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(x3)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2)))
% 26.57/5.81 106:15:4:[36.13,46.4]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 107:16:4:[66.15,47.7]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(x3)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 26.57/5.81 109:15:4:[105.13,48.9,74.15,108.12]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2)))
% 26.57/5.81 110:15:4:[2.12,49.3]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 26.57/5.81 111:2:1:[6.0,50.0]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 26.57/5.81 113:16:4:[59.16,51.4,100.16,112.8]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x1),f(suc(x1)))
% 26.57/5.81 116:15:4:[84.16,53.1,99.15,114.4,92.15,115.13]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x2),f(suc(x2)))
% 26.57/5.81 118:15:4:[74.14,54.4,88.13,117.9]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x2)),'E'(s(s('0')),f(suc(x3))),iLEQ(suc(x1),suc(x3)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 121:15:4:[109.16,55.5,83.15,119.10,118.16,120.14]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x3),f(suc(x3)))
% 26.57/5.81 123:16:4:[94.16,56.5,83.16,122.6]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(f(x1),f(suc(x1))),'E'(s(s('0')),f(x3)) -> 'E'(f(x0),f(suc(x0)))
% 26.57/5.81 124:15:4:[36.14,57.6]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 26.57/5.81 125:16:4:[110.14,58.3]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0)))
% 26.57/5.81 127:15:4:[63.15,59.6,124.13,126.12]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 26.57/5.81 130:16:4:[81.17,60.4,80.17,128.9,113.17,129.12]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(x3)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) ->
% 26.57/5.81 132:15:4:[66.14,61.4,106.14,131.10]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 133:15:4:[36.11,63.10]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3)))
% 26.57/5.81 134:15:4:[2.13,65.3]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(x3))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x0)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 26.57/5.81
% 26.57/5.81 Most General Atoms: 'E'(s('0'),f(x2)) 'E'('0',f(x0)) 'E'(f(x1),f(suc(x1))) 'E'(s(s('0')),f(x2)) 'LE'(f(x0),s(s(s('0')))) 'LE'(f(x0),s(s('0'))) 'LE'(f(x0),s('0')) iLEQ(suc(x3),suc(x2)) 'LE'(f(x0),'0')
% 26.57/5.81
% 26.57/5.81 === Starting SPASS-SCL-FOL A Little Less Naive, considering 67 atoms initially, heuristics mode: resolution_2 ===
% 26.57/5.81
% 26.57/5.81 === Conflict found: 97:17:4:[42.17,39.5,70.17,96.16]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(f(x3),f(suc(x3))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> '0', x1 -> '0', x2 -> '0', x3 -> '0'}
% 26.57/5.81 === Backtracking. Learning clause 135:5:1:[97.6,121.15,71.4,38.2,34.1]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 26.57/5.81 === Clause set with instances from active satisfied. Growing active. New size: 67
% 26.57/5.81 === Restarting.
% 26.57/5.81 === Conflict found: 135:5:1:[97.6,121.15,71.4,38.2,34.1]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0')) {x0 -> '0'}
% 26.57/5.81 === Backtracking. Learning clause 136:4:1:[135.3,6.1]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 26.57/5.81 === Backtracking. Learning clause 137:2:1:[38.1,6.1]:Top: -> 'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 26.57/5.81 === Conflict found: 106:15:4:[36.13,46.4]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(x3)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(x3))) {x0 -> '0', x1 -> '0', x2 -> '0', x3 -> '0'}
% 26.57/5.81 === Backtracking. Learning clause 138:4:1:[106.13,130.14,87.4,21.2,18.2,34.2]:Top: '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'))
% 26.57/5.81 === Conflict found: 130:16:4:[81.17,60.4,80.17,128.9,113.17,129.12]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(x3)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> {x0 -> s('0'), x1 -> s('0'), x2 -> s('0'), x3 -> s('0')}
% 26.57/5.81 === Backtracking. Learning clause 139:4:1:[130.14,66.13,87.4,21.2,18.2]:Top: 'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(x0),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 26.57/5.81 === Conflict found: 130:16:4:[81.17,60.4,80.17,128.9,113.17,129.12]:TopTopTopTop: 'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x0),suc(x3)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(x3)))),iLEQ(suc(x2),suc(x1)),'E'(s('0'),f(suc(x3))),iLEQ(suc(x1),suc(x0)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x3)),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)) -> {x0 -> s('0'), x1 -> s('0'), x2 -> s('0'), x3 -> s('0')}
% 26.57/5.81 === Backtracking. Learning clause 140:3:1:[130.14,106.13,87.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) ->
% 26.57/5.81 === Backtracking. Learning clause 141:5:1:[37.2,43.2,62.2]:Top: 'LE'(f(suc(x0)),s('0')),'LE'(f(x0),s('0')) -> 'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 26.57/5.81 === Clause set with instances from active satisfied. Growing active. New size: 67
% 26.57/5.81 === Restarting.
% 26.57/5.81 === Conflict found: 141:5:1:[37.2,43.2,62.2]:Top: 'LE'(f(suc(x0)),s('0')),'LE'(f(x0),s('0')) -> 'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0') {x0 -> z}
% 26.57/5.81 === Backtracking. Learning clause 142:4:0:[141.5,26.1]:: 'LE'(f(suc(z)),s('0')),'LE'(f(z),s('0')) -> 'E'(f(z),f(suc(z))),iLEQ(suc(z),suc(z))
% 26.57/5.81 === Backtracking. Learning clause 143:2:0:[62.3,26.1]:: 'LE'(f(z),s('0')) -> 'E'('0',f(z))
% 26.57/5.81 === Backtracking. Learning clause 144:2:0:[43.3,26.1]:: 'LE'(f(suc(z)),s('0')) -> 'E'('0',f(suc(z)))
% 26.57/5.81 === Backtracking. Learning clause 145:2:0:[22.3,26.1]:: 'LE'(f(suc(suc(z))),s('0')) -> 'E'('0',f(suc(suc(z))))
% 26.57/5.81 === Conflict found: 97:17:4:[42.17,39.5,70.17,96.16]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(f(x3),f(suc(x3))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> '0', x1 -> '0', x2 -> '0', x3 -> '0'}
% 26.57/5.81 === Backtracking. Learning clause 146:5:1:[97.1,111.1,137.1,18.1]:Top: 'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 26.57/5.81 === Conflict found: 139:4:1:[130.14,66.13,87.4,21.2,18.2]:Top: 'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(x0),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> z}
% 26.57/5.81 === Backtracking. Learning clause 147:3:1:[139.3,64.3,111.2,34.2,137.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'LE'(f(x0),s('0')),'E'(s(s('0')),f(suc(suc(x0))))
% 26.57/5.81 === Conflict found: 97:17:4:[42.17,39.5,70.17,96.16]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(f(x3),f(suc(x3))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> '0', x1 -> '0', x2 -> '0', x3 -> '0'}
% 26.57/5.81 === Backtracking. Learning clause 148:3:1:[97.6,121.15,71.4,147.3,137.1,111.1,18.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 26.57/5.81 === Conflict found: 97:17:4:[42.17,39.5,70.17,96.16]:TopTopTopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x2)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x3)),'E'(f(x3),f(suc(x3))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'(s(s('0')),f(suc(suc(x3)))),'E'(s(s('0')),f(suc(x3))),'E'(s(s('0')),f(suc(x2))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x3),suc(x2)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(x3)),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> z, x1 -> z, x2 -> z, x3 -> z}
% 26.57/5.81 === Backtracking. Learning clause 149:2:1:[97.6,118.14,71.4,137.1,111.1,64.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 26.57/5.81 === Backtracking. Learning clause 150:2:1:[64.1,6.1]:Top: -> 'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0')))
% 26.57/5.81 === Conflict found: 149:2:1:[97.6,118.14,71.4,137.1,111.1,64.2]:Top: 'LE'(f(suc(suc(x0))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> z}
% 26.57/5.81 === Backtracking. Learning clause 151:1:1:[149.1,6.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 26.57/5.81 === Clause set with instances from active satisfied. Growing active. New size: 67
% 26.57/5.81 === Restarting.
% 26.57/5.81 === Conflict found: 139:4:1:[130.14,66.13,87.4,21.2,18.2]:Top: 'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(x0),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> '0'}
% 26.57/5.81 === Backtracking. Learning clause 152:1:1:[139.2,151.1,34.2,151.1,151.1]:Top: -> 'LE'(f(x0),s('0'))
% 26.57/5.81 === Backtracking. Learning clause 153:3:1:[52.4,31.4]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 26.57/5.81 === Backtracking. Learning clause 154:2:1:[62.1,152.1,79.3,22.2,152.1,43.2,152.1]:Top: -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0')
% 26.57/5.81 === Conflict found: 78:17:4:[28.17,13.1,75.17,77.5]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),iLEQ(suc(x1),suc(x2)),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(x3)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),iLEQ(suc(x3),suc(x1)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'(f(x3),f(suc(x3))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x0)) -> {x0 -> z, x1 -> z, x2 -> z, x3 -> z}
% 26.57/5.81
% 26.57/5.81 SZS status Unsatisfiable
% 26.57/5.81
% 26.57/5.81 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.57/5.81
% 26.57/5.81 SPASS-SCL-FOL Statistics:
% 26.57/5.81 Number of learned clauses: 20
% 26.57/5.81 Number of propagations: 250
% 26.57/5.81 Number of decisions: 191
% 26.57/5.81 Number of resolutions: 63
% 26.57/5.81 Number of condensations: 0
% 26.57/5.81 Number of sub resolutions: 69
% 26.57/5.81 Number of input literals (deduplicated): 23
% 26.57/5.81 Number of grows: 3
% 26.57/5.81 Number of considered ground atoms: 67
% 26.57/5.81
% 26.57/5.81 Needed: 0:00:05.29
% 26.57/5.81
%------------------------------------------------------------------------------