%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO662-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 : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 7 07:41:15 PM UTC 2026
% Result : Unsatisfiable 19.66s 4.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYO662-1 : TPTP v9.2.1. Released v7.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n027.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Thu May 7 13:56:35 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.19/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 19.66/4.41 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.66/4.41 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.66/4.41 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.66/4.41 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.66/4.41 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.66/4.41 Execution resolution_1 ended with status: unsatisfiable
% 19.66/4.41 Used heuristic: resolution_1
% 19.66/4.41
% 19.66/4.41 Input Clauses:
% 19.66/4.41
% 19.66/4.41 Predicates: 'LE' 'E' iLEQ
% 19.66/4.41 Fol Constants: '0' z
% 19.66/4.41 Fol Functions: f s suc
% 19.66/4.41 Problem Properties:
% 19.66/4.41 This is a full first-order problem without equality.
% 19.66/4.41
% 19.66/4.41 After reduction: Problem Properties:
% 19.66/4.41 This is a full first-order problem without equality.
% 19.66/4.41
% 19.66/4.41
% 19.66/4.41 Reduced Input Clauses:
% 19.66/4.41 71:2:1:[60.0,1.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 19.66/4.41 73:17:3:[32.17,2.3,37.15,72.15]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 75:16:3:[5.15,3.6,68.13,74.13]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 76:12:3:[40.9,4.7]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 19.66/4.41 77:16:3:[62.14,5.7]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 78:13:3:[23.9,6.6]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 19.66/4.41 79:14:3:[76.12,7.6]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 80:14:3:[34.11,10.7]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 19.66/4.41 82:12:3:[19.12,11.1,23.10,81.10]:TopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x2)),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 19.66/4.41 84:14:3:[39.14,12.2,82.13,83.8]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0))))
% 19.66/4.41 85:14:3:[34.12,13.9]:TopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x2)),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'(f(x0),f(suc(x0))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 87:12:3:[76.11,14.5,40.9,86.9]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 19.66/4.41 89:18:3:[31.18,15.6,58.16,88.17]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) ->
% 19.66/4.41 91:5:1:[28.4,17.2,36.2,90.5]:Top: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0))
% 19.66/4.41 92:5:1:[16.2,18.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 19.66/4.41 93:12:3:[23.10,19.8]:TopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x2)),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 95:16:3:[77.16,20.7,62.14,94.8]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0))))
% 19.66/4.41 97:18:3:[73.18,21.3,48.16,96.19]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x0)) ->
% 19.66/4.41 99:12:3:[66.12,22.6,40.10,98.7]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 19.66/4.41 101:15:3:[57.14,24.2,82.12,100.15]:TopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x2)),'E'('0',f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x2),f(suc(x2)))
% 19.66/4.41 103:12:3:[33.10,25.6,40.8,102.7]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 19.66/4.41 105:14:3:[93.11,26.7,78.13,104.12]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 19.66/4.41 106:5:1:[36.2,28.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))
% 19.66/4.41 108:14:3:[62.13,29.6,87.12,107.8]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x1),f(suc(x1)))
% 19.66/4.41 111:13:3:[79.14,30.6,76.12,109.7,99.13,110.11]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(suc(x0))))
% 19.66/4.41 114:16:3:[56.17,31.7,95.16,112.8,111.14,113.11]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0))))
% 19.66/4.41 116:16:3:[85.13,32.8,105.14,115.15]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 19.66/4.41 117:12:3:[40.8,33.6]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 19.66/4.41 118:12:3:[23.8,34.9]:TopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 19.66/4.41 120:14:3:[118.11,37.7,80.13,119.8]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 19.66/4.41 122:5:1:[92.4,38.3,16.2,121.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0))
% 19.66/4.41 123:14:3:[93.11,39.7]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(x2))))
% 19.66/4.41 127:13:3:[45.14,41.6,108.14,124.7,87.12,125.9,103.12,126.13]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x1),f(suc(x1)))
% 19.66/4.41 129:12:3:[118.10,43.2,23.8,128.11]:TopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 19.66/4.41 130:12:3:[23.9,44.6]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 19.66/4.41 133:13:3:[62.12,45.6,76.10,131.7,103.12,132.11]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 19.66/4.41 136:13:3:[80.12,46.3,129.12,134.8,130.10,135.13]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 19.66/4.41 138:17:3:[116.16,47.3,105.14,137.17]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x2),f(suc(suc(x2))))
% 19.66/4.41 141:14:3:[105.15,48.2,82.13,139.8,84.15,140.9]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1)))
% 19.66/4.41 143:15:3:[85.13,50.8,80.14,142.11]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(x2))))
% 19.66/4.41 146:14:3:[120.14,51.3,129.12,144.8,136.14,145.9]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x2),f(suc(x2)))
% 19.66/4.41 149:14:3:[111.15,52.5,87.13,147.8,99.13,148.13]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x1),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2)))
% 19.66/4.41 152:16:3:[56.16,53.6,75.16,150.8,127.16,151.9]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 154:16:3:[143.16,54.3,80.14,153.13]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 19.66/4.41 157:13:3:[68.14,55.7,117.12,155.8,99.12,156.10]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0)))
% 19.66/4.41 160:15:3:[77.14,56.7,133.15,158.8,79.12,159.9]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 163:13:3:[85.14,57.2,118.12,161.11,82.12,162.13]:TopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x2)),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 19.66/4.41 167:13:3:[67.15,58.7,157.14,164.8,103.13,165.9,99.12,166.11]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0)))
% 19.66/4.41 170:16:3:[154.16,61.3,101.16,168.10,136.15,169.14]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0))))
% 19.66/4.41 172:13:3:[76.10,62.6,117.11,171.9]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 19.66/4.41 176:15:3:[95.17,63.6,75.17,173.8,108.15,174.9,157.15,175.15]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2))))
% 19.66/4.41 179:13:3:[85.12,65.2,129.13,177.10,93.10,178.13]:TopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x2),suc(x1)),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x2)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 180:12:3:[40.10,66.6]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 183:13:3:[68.12,67.7,103.13,181.8,180.10,182.9]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x2))))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 185:13:3:[117.12,68.7,180.10,184.8]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 188:13:3:[79.13,69.5,87.13,186.7,180.11,187.11]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(suc(x1))))
% 19.66/4.41 191:15:3:[143.14,70.3,179.14,189.9,136.15,190.12]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x0)),'E'(f(x1),f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(x2))))
% 19.66/4.41
% 19.66/4.41 Most General Atoms: 'LE'(f(x0),s('0')) 'E'('0',f(x0)) 'E'(s('0'),f(x2)) 'E'(f(x2),f(suc(x2))) 'E'(f(x2),f(suc(suc(x2)))) 'LE'(f(x0),'0') iLEQ(suc(x2),suc(x1)) 'LE'(f(x0),s(s('0')))
% 19.66/4.41
% 19.66/4.41 === Starting SPASS-SCL-FOL A Little Less Naive, considering 18 atoms initially, heuristics mode: resolution_1 ===
% 19.66/4.41
% 19.66/4.41 === Conflict found: 97:18:3:[73.18,21.3,48.16,96.19]:TopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(x2))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x0)) -> {x0 -> '0', x1 -> '0', x2 -> '0'}
% 19.66/4.41 === Backtracking. Learning clause 193:5:1:[91.4,192.4,97.4,143.13]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(x0))) ->
% 19.66/4.41 === Conflict found: 71:2:1:[60.0,1.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0')) {x0 -> suc(suc(suc('0')))}
% 19.66/4.41 === Backtracking. Learning clause 194:7:1:[71.1,89.11]:Top: 'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(suc(suc(suc(x0)))),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 195:8:1:[59.1,60.1,89.11,71.1,143.13]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x0)),'E'(f(x0),f(suc(x0))) -> 'LE'(f(suc(suc(x0))),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 197:6:1:[71.0,196.0,27.1,60.1,89.11]:Top: 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(suc(x0)),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 199:6:1:[71.0,198.0,27.1,60.1,197.3,143.13,23.9]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0')),'LE'(f(suc(x0)),s('0'))
% 19.66/4.41 === Conflict found: 77:16:3:[62.14,5.7]:TopTopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x2),suc(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x2),f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> '0', x1 -> '0', x2 -> '0'}
% 19.66/4.41 === Backtracking. Learning clause 200:6:1:[77.3,71.1]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(suc(suc(x0))),s('0'))
% 19.66/4.41 === Conflict found: 197:6:1:[71.0,196.0,27.1,60.1,89.11]:Top: 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(suc(x0)),s('0')) {x0 -> '0'}
% 19.66/4.41 === Backtracking. Learning clause 202:5:1:[71.0,201.0,197.3,71.1,200.5]:Top: 'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(suc(x0)),s('0')),'LE'(f(suc(suc(x0))),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 204:5:1:[71.0,203.1,27.1,60.1,77.3]:Top: 'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0')),'E'(f(x0),f(suc(suc(x0))))
% 19.66/4.41 === Backtracking. Learning clause 206:5:1:[71.0,205.0,27.1,60.1,197.3,204.5,71.1,23.9]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0')),'LE'(f(suc(x0)),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 209:5:1:[204.4,207.1,71.0,208.4,42.1,60.1,89.11]:Top: 'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 210:4:1:[27.1,60.1,209.3]:Top: 'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 211:4:1:[59.1,60.1,210.1,23.9]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0'))
% 19.66/4.41 === Conflict found: 71:2:1:[60.0,1.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0')) {x0 -> suc(suc(suc('0')))}
% 19.66/4.41 === Backtracking. Learning clause 212:5:1:[71.1,122.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> 'LE'(f(suc(suc(suc(x0)))),s('0')),iLEQ(suc(x0),suc(x0))
% 19.66/4.41 === Backtracking. Learning clause 213:4:1:[59.1,60.1,122.4,71.1]:Top: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(suc(suc(x0))),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 215:4:1:[71.0,214.2,27.1,60.1,122.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)) -> 'LE'(f(suc(x0)),s('0')),iLEQ(suc(x0),suc(x0))
% 19.66/4.41 === Backtracking. Learning clause 217:3:1:[71.0,216.0,27.1,60.1,215.1]:Top: -> 'LE'(f(x0),s('0')),'LE'(f(suc(x0)),s('0')),iLEQ(suc(x0),suc(x0))
% 19.66/4.41 === Backtracking. Learning clause 219:4:1:[71.0,218.1,42.1,60.1,122.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),s('0')),iLEQ(suc(x0),suc(x0))
% 19.66/4.41 === Backtracking. Learning clause 220:3:1:[27.1,60.1,219.1]:Top: 'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),s('0')),iLEQ(suc(x0),suc(x0))
% 19.66/4.41 === Backtracking. Learning clause 221:3:1:[59.1,60.1,220.1,211.3]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))) -> 'LE'(f(x0),s('0'))
% 19.66/4.41 === Conflict found: 210:4:1:[27.1,60.1,209.3]:Top: 'E'(s('0'),f(suc(x0))),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0')) {x0 -> '0'}
% 19.66/4.41 === Backtracking. Learning clause 223:3:1:[217.2,222.1,210.1,71.1]:Top: 'E'(f(x0),f(suc(x0))) -> 'LE'(f(x0),s('0')),'LE'(f(suc(x0)),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 226:2:1:[71.0,224.0,217.2,225.1,40.1,71.1,223.1]:Top: -> 'LE'(f(x0),s('0')),'LE'(f(suc(x0)),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 227:3:1:[59.1,60.1,210.1]:Top: 'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 229:2:1:[71.0,228.0,59.1,60.1,40.1,227.1]:Top: iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),s('0'))
% 19.66/4.41 === Backtracking. Learning clause 230:1:1:[59.1,60.1,220.1,229.1]:Top: -> 'LE'(f(x0),s('0'))
% 19.66/4.41 === Clause set with instances from active satisfied. Growing active. New size: 23
% 19.66/4.41 === Restarting.
% 19.66/4.41 === Backtracking. Learning clause 231:2:1:[8.1,230.1]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 19.66/4.41 === Backtracking. Learning clause 232:2:1:[9.1,230.1]:Top: -> 'E'('0',f(suc(x0))),'LE'(f(x0),'0')
% 19.66/4.41 === Conflict found: 231:2:1:[8.1,230.1]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0') {x0 -> suc(suc(suc('0')))}
% 19.66/4.41 === Backtracking. Learning clause 233:5:1:[231.1,91.4]:Top: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)) -> 'LE'(f(suc(suc(suc(x0)))),'0'),iLEQ(suc(x0),suc(x0))
% 19.66/4.41 === Backtracking. Learning clause 236:3:1:[232.0,234.0,231.0,235.2,35.1,230.1,91.4]:Top: 'E'('0',f(suc(suc(x0)))) -> 'LE'(f(x0),'0'),iLEQ(suc(x0),suc(x0))
% 19.66/4.41 === Backtracking. Learning clause 237:2:1:[64.1,230.1,236.1]:Top: -> 'LE'(f(x0),'0'),iLEQ(suc(x0),suc(x0))
% 19.66/4.41 === Conflict found: 231:2:1:[8.1,230.1]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0') {x0 -> suc(suc(suc('0')))}
% 19.66/4.41 === Backtracking. Learning clause 238:5:1:[231.1,193.1]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(x0))) -> 'LE'(f(suc(suc(suc(x0)))),'0')
% 19.66/4.41 === Backtracking. Learning clause 242:2:1:[231.0,239.1,232.0,240.2,236.2,241.3,35.1,230.1,193.1,23.9]:Top: 'E'('0',f(suc(suc(x0)))) -> 'LE'(f(x0),'0')
% 19.66/4.41 === Backtracking. Learning clause 243:1:1:[64.1,230.1,242.1]:Top: -> 'LE'(f(x0),'0')
% 19.66/4.41 === Clause set with instances from active satisfied. Growing active. New size: 24
% 19.66/4.41 === Restarting.
% 19.66/4.41 === Conflict found: 243:1:1:[64.1,230.1,242.1]:Top: -> 'LE'(f(x0),'0') {x0 -> z}
% 19.66/4.41
% 19.66/4.41 SZS status Unsatisfiable
% 19.66/4.41
% 19.66/4.41 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.66/4.41
% 19.66/4.41 SPASS-SCL-FOL Statistics:
% 19.66/4.41 Number of learned clauses: 32
% 19.66/4.41 Number of propagations: 205
% 19.66/4.41 Number of decisions: 92
% 19.66/4.41 Number of resolutions: 69
% 19.66/4.41 Number of condensations: 1
% 19.66/4.41 Number of sub resolutions: 141
% 19.66/4.41 Number of input literals (deduplicated): 22
% 19.66/4.41 Number of grows: 2
% 19.66/4.41 Number of considered ground atoms: 24
% 19.66/4.41
% 19.66/4.41 Needed: 0:00:03.88
% 19.66/4.41
%------------------------------------------------------------------------------