%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO678-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 : n029.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.88s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SYO678-1 : TPTP v9.2.1. Released v7.3.0.
% 0.11/0.14 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.35 % Computer : n029.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Thu May 7 13:56:15 EDT 2026
% 0.15/0.35 % CPUTime :
% 0.15/0.35 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.88/0.67 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67 Execution lmodel_grow ended with status: unsatisfiable
% 0.88/0.67 Used heuristic: lmodel_grow
% 0.88/0.67
% 0.88/0.67 Input Clauses:
% 0.88/0.67
% 0.88/0.67 Predicates: 'E' iLEQ 'LE'
% 0.88/0.67 Fol Constants: '0' z
% 0.88/0.67 Fol Functions: f suc s
% 0.88/0.67 Problem Properties:
% 0.88/0.67 This is a full first-order problem without equality.
% 0.88/0.67
% 0.88/0.67 After reduction: Problem Properties:
% 0.88/0.67 This is a full first-order problem without equality.
% 0.88/0.67
% 0.88/0.67
% 0.88/0.67 Reduced Input Clauses:
% 0.88/0.67 67:9:2:[28.5,1.0]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x1)) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 69:10:2:[45.10,2.1,36.8,68.3]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x1)),'E'(f(x1),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.88/0.67 70:5:1:[49.2,6.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.88/0.67 72:8:2:[10.7,7.1,24.5,71.5]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 73:9:2:[60.6,8.1]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1)))
% 0.88/0.67 75:5:1:[34.4,9.3,61.2,74.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))) -> iLEQ(suc(x0),suc(x0))
% 0.88/0.67 76:8:2:[24.5,10.3]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(x0)))
% 0.88/0.67 77:8:2:[24.6,12.4]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67 80:9:2:[17.9,13.1,72.9,78.6,77.7,79.7]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67 81:8:2:[28.6,14.5]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67 82:10:2:[64.8,15.1]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67 84:11:2:[48.9,16.1,73.9,83.9]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(x1))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(f(x1),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))) ->
% 0.88/0.67 86:9:2:[76.8,17.4,77.7,85.5]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67 88:5:1:[49.2,19.0,70.4,87.4]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0))
% 0.88/0.67 90:10:2:[45.9,21.0,57.7,89.9]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67 92:8:2:[36.7,22.0,27.5,91.8]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(suc(x1))))) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 94:5:1:[33.4,26.0,43.2,93.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)))) -> iLEQ(suc(x0),suc(x0))
% 0.88/0.67 96:10:2:[64.8,29.1,73.9,95.7]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.88/0.67 98:5:1:[65.4,30.0,47.2,97.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))))) -> iLEQ(suc(x0),suc(x0))
% 0.88/0.67 100:4:1:[43.2,33.2,86.8,99.5]: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.88/0.67 101:5:1:[61.2,34.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)))),iLEQ(suc(x0),suc(x0))
% 0.88/0.67 102:8:2:[60.6,35.1]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67 103:8:2:[27.5,36.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(x0)))
% 0.88/0.67 105:11:2:[40.9,38.0,67.9,104.11]:TopTop: 'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x1)) ->
% 0.88/0.67 107:8:2:[24.6,39.4,77.8,106.7]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1)))
% 0.88/0.67 109:8:2:[81.8,40.1,28.6,108.7]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(x1)))
% 0.88/0.67 113:9:2:[100.4,41.1,72.9,110.6,107.9,111.7,80.11,112.10]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) ->
% 0.88/0.67 116:9:2:[48.9,42.1,82.9,114.7,102.7,115.8]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(x1))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67 117:11:2:[109.9,44.0]:TopTop: 'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.88/0.67 118:10:2:[103.8,45.2]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x1)),'E'(f(x1),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67 120:8:2:[64.7,48.6,60.5,119.7]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(x1))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(x1))) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 121:8:2:[28.5,50.0]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(x0)))
% 0.88/0.67 123:8:2:[57.8,52.1,27.6,122.3]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1)))
% 0.88/0.67 124:2:1:[46.0,53.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 0.88/0.67 127:9:2:[76.8,54.4,107.9,125.5,86.10,126.8]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.88/0.67 128:8:2:[27.6,57.2]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67 130:10:2:[81.7,58.0,67.9,129.9]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x1)) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67 134:9:2:[69.11,59.0,90.11,131.2,92.9,132.4,123.9,133.11]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))) ->
% 0.88/0.67 135:8:2:[60.5,64.5]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(x0)))
% 0.88/0.67 136:5:1:[47.2,65.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)))),iLEQ(suc(x0),suc(x0))
% 0.88/0.67 138:9:2:[81.7,66.0,121.8,137.7]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 0.88/0.67
% 0.88/0.67 Most General Atoms: iLEQ(suc(x1),suc(x0)) 'E'('0',f(x1)) 'E'(s(s('0')),f(x1)) 'E'(f(x1),f(suc(x1))) 'LE'(f(x0),s('0')) 'LE'(f(x0),s(s('0'))) 'LE'(f(x0),s(s(s('0')))) 'E'(f(x0),f(suc(suc(x0)))) 'E'(s('0'),f(x1)) 'E'(s(s(s('0'))),f(x1)) 'LE'(f(x0),'0') 'LE'(f(x0),s(s(s(s('0')))))
% 0.88/0.67
% 0.88/0.67 === Starting SPASS-SCL-FOL A Little Less Naive, considering 75 atoms initially, heuristics mode: lmodel_grow ===
% 0.88/0.67
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 92
% 0.88/0.67 === Backtracking. Learning clause 139:3:1:[43.4,24.5]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 100
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 108
% 0.88/0.67 === Backtracking. Learning clause 140:2:1:[11.1,46.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'LE'(f(x0),s(s(s('0'))))
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 119
% 0.88/0.67 === Backtracking. Learning clause 142:4:1:[124.0,141.2,20.2,75.1,46.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> 'LE'(f(suc(x0)),s(s(s('0')))),iLEQ(suc(x0),suc(x0))
% 0.88/0.67 === Conflict found: 84:11:2:[48.9,16.1,73.9,83.9]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(x1))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(f(x1),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))) -> {x0 -> suc(suc(z)), x1 -> suc(suc(z))}
% 0.88/0.67 === Backtracking. Learning clause 144:4:1:[124.0,143.1,84.7,82.9,20.2,142.4,46.1]:Top: 'E'(f(x0),f(suc(x0))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> 'LE'(f(suc(x0)),s(s(s('0'))))
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 140
% 0.88/0.67 === Conflict found: 84:11:2:[48.9,16.1,73.9,83.9]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(x1))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(f(x1),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))) -> {x0 -> suc(suc(suc(z))), x1 -> suc(suc(suc(z)))}
% 0.88/0.67 === Backtracking. Learning clause 145:1:1:[84.7,116.9,75.5,140.1,20.2,46.1,31.2,46.1,124.1]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 0.88/0.67 === Conflict found: 98:5:1:[65.4,30.0,47.2,97.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))))) -> iLEQ(suc(x0),suc(x0)) {x0 -> '0'}
% 0.88/0.67 === Backtracking. Learning clause 149:2:1:[145.0,146.1,145.0,147.2,145.0,148.3,98.5,134.3,5.2,37.2,23.2]:Top: 'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'LE'(f(x0),s(s('0')))
% 0.88/0.67 === Conflict found: 134:9:2:[69.11,59.0,90.11,131.2,92.9,132.4,123.9,133.11]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> z, x1 -> z}
% 0.88/0.67 === Backtracking. Learning clause 150:9:1:[134.6,23.2,37.2,5.2,3.1,43.1]:Top: iLEQ(suc(x0),suc(x0)),'E'(s(s('0')),f(x0)),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))),'E'(s('0'),f(suc(suc(x0)))) -> 'LE'(f(x0),s('0')),'E'(f(suc(x0)),f(suc(suc(x0)))),iLEQ(suc(suc(x0)),suc(suc(x0)))
% 0.88/0.67 === Clause set with instances from active satisfied. Growing active. New size: 154
% 0.88/0.67 === Backtracking. Learning clause 151:11:1:[37.1,145.1,136.1,5.2,23.2,56.1,150.6]:Top: iLEQ(suc(x0),suc(x0)),'E'(s(s('0')),f(x0)),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(suc(suc(x0))),suc(suc(suc(x0)))),'LE'(f(suc(suc(x0))),s('0')),'LE'(f(x0),s('0')),'E'(f(suc(x0)),f(suc(suc(x0)))),iLEQ(suc(suc(x0)),suc(suc(x0)))
% 0.88/0.67 === Backtracking. Learning clause 152:12:1:[3.2,43.1,5.3,56.2,37.3,136.1,98.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'LE'(f(x0),s('0')),'E'(f(suc(x0)),f(suc(suc(x0)))),iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(suc(suc(x0))),s('0')),'E'(f(suc(suc(x0))),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(suc(suc(x0))),suc(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 0.88/0.67 === Backtracking. Learning clause 153:12:1:[3.1,23.3,43.1,56.2,5.3,152.3]:Top: 'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'LE'(f(x0),s('0')),'E'(f(suc(x0)),f(suc(suc(x0)))),iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(suc(suc(x0))),s('0')),'E'(f(suc(suc(x0))),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(suc(suc(x0))),suc(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 0.88/0.67 === Backtracking. Learning clause 154:11:1:[3.2,43.1,37.3,56.2,23.3,153.5,145.1,151.1,63.1]:Top: 'E'(s(s('0')),f(x0)),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(suc(suc(x0))),suc(suc(suc(x0)))),'LE'(f(suc(suc(x0))),s('0')),'E'(f(suc(x0)),f(suc(suc(x0)))),iLEQ(suc(suc(x0)),suc(suc(x0))),'E'('0',f(x0)),'LE'(f(x0),'0')
% 0.88/0.67 === Backtracking. Learning clause 157:3:1:[145.0,155.0,145.0,156.1,37.2,136.1,145.1,5.2,23.2]:Top: -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s(s('0')))
% 0.88/0.67 === Backtracking. Learning clause 158:2:1:[4.2,149.1]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 0.88/0.67 === Backtracking. Learning clause 159:1:1:[4.1,145.1,149.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 0.88/0.67 === Conflict found: 94:5:1:[33.4,26.0,43.2,93.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)))) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(z)}
% 0.88/0.67 === Backtracking. Learning clause 160:6:1:[94.1,62.2,3.2]:Top: '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'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s('0'))
% 0.88/0.67 === Conflict found: 138:9:2:[81.7,66.0,121.8,137.7]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))) {x0 -> z, x1 -> z}
% 0.88/0.67 === Backtracking. Learning clause 161:9:1:[138.8,105.2,51.2,32.2,25.3,3.3,94.1]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'LE'(f(x0),'0'),iLEQ(suc(suc(x0)),suc(suc(x0)))
% 0.88/0.67 === Conflict found: 138:9:2:[81.7,66.0,121.8,137.7]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))) {x0 -> z, x1 -> z}
% 0.88/0.67 === Backtracking. Learning clause 162:8:1:[138.8,105.2,51.2,62.3,32.2,56.3,161.7,55.2,160.6]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),'0'),iLEQ(suc(suc(x0)),suc(suc(x0)))
% 0.88/0.67 === Conflict found: 105:11:2:[40.9,38.0,67.9,104.11]:TopTop: 'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x1)) -> {x0 -> z, x1 -> z}
% 0.88/0.67 === Backtracking. Learning clause 163:8:1:[105.2,138.8,55.2,62.3,51.2,32.2,25.3,3.3,113.3,162.8]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0)),'E'('0',f(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),'0')
% 0.88/0.67 === Conflict found: 105:11:2:[40.9,38.0,67.9,104.11]:TopTop: 'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x1)) -> {x0 -> z, x1 -> z}
% 0.88/0.67 === Backtracking. Learning clause 164:7:1:[105.2,138.8,55.2,3.3,32.2,51.2,62.3,56.3,163.1,63.2]:Top: iLEQ(suc(x0),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(x0),s('0')) -> 'LE'(f(x0),'0')
% 0.88/0.67 === Conflict found: 113:9:2:[100.4,41.1,72.9,110.6,107.9,111.7,80.11,112.10]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> {x0 -> suc(z), x1 -> suc(z)}
% 0.88/0.67 === Backtracking. Learning clause 165:5:1:[113.9,94.5,3.2]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(suc(suc(x0))),s('0'))
% 0.88/0.67 === Conflict found: 113:9:2:[100.4,41.1,72.9,110.6,107.9,111.7,80.11,112.10]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> {x0 -> suc(z), x1 -> suc(z)}
% 0.88/0.67 === Backtracking. Learning clause 166:6:1:[113.9,160.5,62.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(suc(x0)),s('0'))
% 0.88/0.67 === Backtracking. Learning clause 170:5:1:[159.0,167.0,159.0,168.5,159.0,169.6,56.2,113.5,164.6]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),'0')
% 0.88/0.67 === Backtracking. Learning clause 171:2:1:[56.1,159.1]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 0.88/0.67 === Backtracking. Learning clause 172:2:1:[3.1,159.1]:Top: -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.88/0.67 === Conflict found: 105:11:2:[40.9,38.0,67.9,104.11]:TopTop: 'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x1)) -> {x0 -> z, x1 -> z}
% 0.88/0.67 === Backtracking. Learning clause 173:7:1:[105.7,63.2]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s('0')) -> 'LE'(f(x0),'0')
% 0.88/0.67 === Conflict found: 138:9:2:[81.7,66.0,121.8,137.7]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))) {x0 -> z, x1 -> z}
% 0.88/0.67 === Backtracking. Learning clause 174:3:0:[138.5,63.2,173.5,55.2,25.3,51.2,62.3,159.1,32.2,171.2,172.2,170.1,18.1]:: iLEQ(suc(z),suc(z)),'E'(s('0'),f(suc(suc(z)))),'E'(s('0'),f(suc(z))) ->
% 0.88/0.67 === Conflict found: 113:9:2:[100.4,41.1,72.9,110.6,107.9,111.7,80.11,112.10]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> {x0 -> suc(z), x1 -> suc(z)}
% 0.88/0.67 === Backtracking. Learning clause 175:4:1:[113.9,94.5,172.1]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) -> 'LE'(f(suc(suc(x0))),s('0'))
% 0.88/0.67 === Conflict found: 175:4:1:[113.9,94.5,172.1]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) -> 'LE'(f(suc(suc(x0))),s('0')) {x0 -> suc(z)}
% 0.88/0.67 === Backtracking. Learning clause 176:4:1:[175.3,172.1]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(suc(suc(x0))),s('0')),'LE'(f(suc(x0)),s('0'))
% 0.88/0.67 === Backtracking. Learning clause 177:2:0:[63.3,18.1]:: 'LE'(f(z),s('0')) -> 'E'('0',f(z))
% 0.88/0.67 === Backtracking. Learning clause 178:2:0:[51.3,18.1]:: 'LE'(f(suc(z)),s('0')) -> 'E'('0',f(suc(z)))
% 0.88/0.67 === Conflict found: 166:6:1:[113.9,160.5,62.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(suc(x0)),s('0')) {x0 -> suc(z)}
% 0.88/0.67 === Backtracking. Learning clause 179:3:1:[166.5,159.1,159.1,172.1]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(suc(x0)),s('0'))
% 0.88/0.67 === Backtracking. Learning clause 180:2:1:[25.1,159.1]:Top: -> 'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 0.88/0.67 === Conflict found: 113:9:2:[100.4,41.1,72.9,110.6,107.9,111.7,80.11,112.10]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> {x0 -> suc(z), x1 -> suc(z)}
% 0.88/0.67 === Backtracking. Learning clause 181:4:0:[113.9,94.5,180.1,178.1]:: 'E'(s('0'),f(suc(suc(z)))),'E'(s('0'),f(suc(z))),'E'(s('0'),f(suc(suc(suc(z))))) -> 'E'('0',f(suc(z)))
% 0.88/0.67 === Conflict found: 88:5:1:[49.2,19.0,70.4,87.4]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 0.88/0.67 === Backtracking. Learning clause 182:6:0:[88.5,174.1,177.2]:: 'E'('0',f(suc(suc(suc(z))))),'E'('0',f(suc(suc(z)))),'E'('0',f(suc(z))),'E'(s('0'),f(suc(suc(z)))),'E'(s('0'),f(suc(z))),'LE'(f(z),s('0')) ->
% 0.88/0.67 === Conflict found: 94:5:1:[33.4,26.0,43.2,93.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)))) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 0.88/0.67 === Backtracking. Learning clause 183:4:0:[94.3,171.1,174.1,182.6,55.2,32.2,18.1,181.4,179.3]:: 'LE'(f(suc(suc(z))),s('0')),'E'(s('0'),f(suc(z))),'E'(s('0'),f(suc(suc(suc(z))))),'E'(s('0'),f(suc(suc(z)))) ->
% 0.88/0.67 === Conflict found: 180:2:1:[25.1,159.1]:Top: -> 'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0')) {x0 -> suc(z)}
% 0.88/0.67 === Backtracking. Learning clause 184:2:0:[180.2,178.1]:: -> 'E'(s('0'),f(suc(suc(suc(suc(z)))))),'E'('0',f(suc(z)))
% 0.88/0.67 === Backtracking. Learning clause 185:2:0:[62.1,159.1,178.1]:: -> 'E'(s('0'),f(suc(suc(suc(z))))),'E'('0',f(suc(z)))
% 0.88/0.67 === Conflict found: 88:5:1:[49.2,19.0,70.4,87.4]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 0.88/0.67 === Backtracking. Learning clause 186:2:0:[88.2,55.2,177.2,32.2,174.1,18.1,180.2,171.2,185.2,183.3,179.3]:: 'E'(s('0'),f(suc(suc(z)))),'E'(s('0'),f(suc(z))) ->
% 0.88/0.67 === Conflict found: 171:2:1:[56.1,159.1]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0')) {x0 -> suc(z)}
% 0.88/0.67 === Backtracking. Learning clause 187:2:0:[171.1,186.2,178.1]:: 'E'(s('0'),f(suc(suc(z)))) -> 'E'('0',f(suc(z)))
% 0.88/0.67 === Backtracking. Learning clause 188:2:1:[62.1,159.1]:Top: -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 0.88/0.67 === Conflict found: 105:11:2:[40.9,38.0,67.9,104.11]:TopTop: 'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x1)) -> {x0 -> z, x1 -> z}
% 0.88/0.67 === Backtracking. Learning clause 189:5:1:[105.2,138.8,88.5,55.2,188.2]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(suc(x0))))))
% 0.88/0.67 === Backtracking. Learning clause 190:3:1:[24.1,172.1,171.1]:Top: iLEQ(suc(x0),suc(x0)) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),s('0'))
% 0.88/0.67 === Backtracking. Learning clause 191:3:1:[61.4,60.2]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 0.88/0.67 === Conflict found: 113:9:2:[100.4,41.1,72.9,110.6,107.9,111.7,80.11,112.10]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> {x0 -> '0', x1 -> '0'}
% 0.88/0.67 === Backtracking. Learning clause 192:2:1:[113.2,188.1,180.1,171.1,172.1]:Top: iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0'))
% 0.88/0.67 === Conflict found: 94:5:1:[33.4,26.0,43.2,93.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)))) -> iLEQ(suc(x0),suc(x0)) {x0 -> '0'}
% 0.88/0.67 === Backtracking. Learning clause 193:1:1:[94.5,192.1,180.1,188.1,172.1,171.1]:Top: -> 'LE'(f(x0),s('0'))
% 0.88/0.67 === Conflict found: 189:5:1:[105.2,138.8,88.5,55.2,188.2]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) {x0 -> z}
% 0.88/0.67 === Backtracking. Learning clause 197:1:0:[184.1,194.0,193.0,195.1,172.1,196.2,189.3,177.2,32.2,18.1]:: -> 'E'(s('0'),f(suc(suc(suc(suc(z))))))
% 0.88/0.67 === Conflict found: 138:9:2:[81.7,66.0,121.8,137.7]:TopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))) {x0 -> z, x1 -> z}
% 0.88/0.67
% 0.88/0.67 SZS status Unsatisfiable
% 0.88/0.67
% 0.88/0.67 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.88/0.67
% 0.88/0.67 SPASS-SCL-FOL Statistics:
% 0.88/0.67 Number of learned clauses: 46
% 0.88/0.67 Number of propagations: 650
% 0.88/0.67 Number of decisions: 453
% 0.88/0.67 Number of resolutions: 180
% 0.88/0.67 Number of condensations: 0
% 0.88/0.67 Number of sub resolutions: 85
% 0.88/0.67 Number of input literals (deduplicated): 38
% 0.88/0.67 Number of grows: 6
% 0.88/0.67 Number of considered ground atoms: 154
% 0.88/0.67
% 0.88/0.67 Needed: 0:00:00.15
% 0.88/0.67
%------------------------------------------------------------------------------