%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO670-1 : TPTP v9.2.1. Released v7.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/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:16 PM UTC 2026
% Result : Unsatisfiable 2.32s 1.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO670-1 : TPTP v9.2.1. Released v7.3.0.
% 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.32 % Computer : n027.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Thu May 7 13:56:35 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.21/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 2.32/1.00 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.32/1.00 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.32/1.00 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.32/1.00 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.32/1.00 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.32/1.00 Execution resolution_2 ended with status: unsatisfiable
% 2.32/1.00 Used heuristic: resolution_2
% 2.32/1.00
% 2.32/1.00 Input Clauses:
% 2.32/1.00
% 2.32/1.00 Predicates: 'E' iLEQ 'LE'
% 2.32/1.00 Fol Constants: '0' z
% 2.32/1.00 Fol Functions: s f suc
% 2.32/1.00 Problem Properties:
% 2.32/1.00 This is a full first-order problem without equality.
% 2.32/1.00
% 2.32/1.00 After reduction: Problem Properties:
% 2.32/1.00 This is a full first-order problem without equality.
% 2.32/1.00
% 2.32/1.00
% 2.32/1.00 Reduced Input Clauses:
% 2.32/1.00 78:11:2:[33.6,1.2]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(suc(x1)))))),'E'(s(s('0')),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(x0)))
% 2.32/1.00 79:8:2:[36.6,3.4]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 2.32/1.00 81:9:2:[40.7,4.3,33.5,80.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1)))
% 2.32/1.00 83:11:2:[69.10,7.3,77.8,82.6]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 2.32/1.00 84:8:2:[33.6,8.1]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 2.32/1.00 86:7:1:[21.4,10.1,28.2,85.6]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0))
% 2.32/1.00 88:14:2:[81.10,11.2,78.11,87.11]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(suc(x1)))))),'E'(s(s('0')),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 2.32/1.00 90:9:2:[79.8,12.3,36.6,89.5]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 2.32/1.00 91:5:1:[26.2,14.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))
% 2.32/1.00 93:15:2:[46.13,15.0,22.11,92.14]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) ->
% 2.32/1.00 94:8:2:[53.6,17.6]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0))))
% 2.32/1.00 96:10:2:[77.7,19.0,36.5,95.8]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x1),f(suc(x1)))
% 2.32/1.00 97:8:2:[53.5,20.5]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(x0)))
% 2.32/1.00 98:5:1:[28.2,21.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))
% 2.32/1.00 101:9:2:[79.8,22.3,90.10,99.6,36.6,100.7]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(x0)))
% 2.32/1.00 103:9:2:[97.7,23.2,53.5,102.7]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0)))
% 2.32/1.00 105:11:2:[81.10,24.1,84.7,104.8]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1))))
% 2.32/1.00 107:15:2:[71.13,25.5,42.11,106.12]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0))))) ->
% 2.32/1.00 110:9:2:[97.7,27.3,53.5,108.8,103.9,109.10]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x1),f(suc(x1)))
% 2.32/1.00 111:15:2:[60.11,29.1]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 2.32/1.00 113:13:2:[81.10,30.1,105.12,112.3]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 2.32/1.00 114:12:2:[40.8,32.1]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 2.32/1.00 115:2:1:[45.0,34.0]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 2.32/1.00 117:6:1:[91.4,35.0,26.2,116.4]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 2.32/1.00 119:9:2:[94.7,37.6,97.8,118.8]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 2.32/1.00 122:13:2:[71.13,39.4,42.11,120.11,103.10,121.14]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(f(x0),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 2.32/1.00 123:8:2:[33.5,40.4]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 2.32/1.00 125:12:2:[123.8,41.2,114.12,124.5]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(suc(x1)))))),'E'(s(s('0')),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(x0))))
% 2.32/1.00 127:10:2:[94.8,42.4,53.6,126.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(f(x0),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(x1)))
% 2.32/1.00 129:11:2:[119.10,43.4,97.8,128.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 2.32/1.00 132:10:2:[119.9,44.3,94.7,130.8,103.10,131.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0))))
% 2.32/1.00 136:10:2:[69.10,46.3,83.12,133.7,77.8,134.8,101.11,135.10]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0))))
% 2.32/1.00 138:13:2:[83.11,48.0,90.9,137.10]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(f(x1),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 2.32/1.00 141:6:1:[57.6,50.3,52.4,139.4,6.2,140.6]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> iLEQ(suc(x0),suc(x0))
% 2.32/1.00 142:5:1:[6.2,52.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))
% 2.32/1.00 145:11:2:[69.9,54.0,96.11,143.8,79.7,144.10]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x1),f(suc(suc(x1))))
% 2.32/1.00 147:6:1:[142.4,57.2,6.2,146.4]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 2.32/1.00 149:9:2:[33.6,58.1,84.8,148.3]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 2.32/1.00 151:6:1:[98.4,59.0,28.2,150.5]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 2.32/1.00 154:9:2:[81.9,60.3,123.7,152.5,33.5,153.8]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x1),f(suc(x1)))
% 2.32/1.00 156:9:2:[77.7,61.0,36.5,155.6]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1)))
% 2.32/1.00 159:13:2:[129.11,62.5,70.9,157.11,110.11,158.13]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(f(x0),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 2.32/1.00 162:10:2:[69.9,63.0,156.10,160.6,79.7,161.8]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1))))
% 2.32/1.00 166:12:2:[83.11,66.0,145.13,163.5,96.11,164.9,90.9,165.12]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 2.32/1.00 169:6:1:[91.4,67.0,117.6,167.3,26.2,168.6]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 2.32/1.00 172:11:2:[154.11,68.1,105.11,170.4,84.7,171.10]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x1),f(suc(suc(x1))))
% 2.32/1.00 174:9:2:[77.8,69.5,79.7,173.6]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 2.32/1.00 176:9:2:[94.8,70.4,53.6,175.8]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 2.32/1.00 179:11:2:[119.10,71.4,127.11,177.9,97.8,178.12]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)),'E'(f(x0),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(suc(x1))))
% 2.32/1.00 181:9:2:[123.8,72.1,84.7,180.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 2.32/1.00 185:10:2:[119.9,73.4,94.7,182.9,110.11,183.11,132.11,184.12]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x1),f(suc(suc(x1))))
% 2.32/1.00 189:12:2:[136.13,74.0,162.12,186.4,156.10,187.9,101.11,188.12]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 2.32/1.00 193:11:2:[129.11,75.4,132.12,190.5,176.9,191.10,103.10,192.12]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x1))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 2.32/1.00 196:14:2:[154.11,76.2,88.15,194.5,172.13,195.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(suc(x1)))))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) ->
% 2.32/1.00 197:8:2:[36.5,77.4]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 2.32/1.00
% 2.32/1.00 Most General Atoms: 'E'(s(s('0')),f(x1)) 'LE'(f(x0),'0') 'E'(s('0'),f(x0)) 'E'(f(x0),f(suc(suc(suc(x0))))) 'E'(f(x1),f(suc(x1))) 'LE'(f(x0),s('0')) 'E'(f(x0),f(suc(suc(x0)))) 'LE'(f(x0),s(s('0'))) 'E'('0',f(x1)) iLEQ(suc(x1),suc(x0)) 'LE'(f(x0),s(s(s('0'))))
% 2.32/1.00
% 2.32/1.00 === Starting SPASS-SCL-FOL A Little Less Naive, considering 73 atoms initially, heuristics mode: resolution_2 ===
% 2.32/1.00
% 2.32/1.00 === Clause set with instances from active satisfied. Growing active. New size: 73
% 2.32/1.00 === Restarting.
% 2.32/1.00 === Backtracking. Learning clause 198:2:1:[18.1,45.1]:Top: -> 'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 2.32/1.00 === Conflict found: 181:9:2:[123.8,72.1,84.7,180.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> z, x1 -> z}
% 2.32/1.00 === Backtracking. Learning clause 200:3:1:[198.0,199.1,181.3,142.5,115.1]:Top: 'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s(s('0')))
% 2.32/1.00 === Clause set with instances from active satisfied. Growing active. New size: 73
% 2.32/1.00 === Restarting.
% 2.32/1.00 === Backtracking. Learning clause 201:2:0:[56.3,65.1]:: 'LE'(f(z),s('0')) -> 'E'('0',f(z))
% 2.32/1.00 === Backtracking. Learning clause 202:2:0:[51.3,65.1]:: 'LE'(f(suc(z)),s('0')) -> 'E'('0',f(suc(z)))
% 2.32/1.00 === Backtracking. Learning clause 203:2:0:[31.3,65.1]:: 'LE'(f(suc(suc(suc(z)))),s('0')) -> 'E'('0',f(suc(suc(suc(z)))))
% 2.32/1.00 === Backtracking. Learning clause 204:2:0:[13.3,65.1]:: 'LE'(f(suc(suc(z))),s('0')) -> 'E'('0',f(suc(suc(z))))
% 2.32/1.00 === Backtracking. Learning clause 205:2:0:[2.3,65.1]:: 'LE'(f(suc(suc(suc(suc(z))))),s('0')) -> 'E'('0',f(suc(suc(suc(suc(z))))))
% 2.32/1.00 === Conflict found: 181:9:2:[123.8,72.1,84.7,180.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> '0', x1 -> '0'}
% 2.32/1.00 === Backtracking. Learning clause 206:4:1:[181.3,142.5]: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))))
% 2.32/1.00 === Conflict found: 196:14:2:[154.11,76.2,88.15,194.5,172.13,195.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(suc(x1)))))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> {x0 -> '0', x1 -> '0'}
% 2.32/1.00 === Backtracking. Learning clause 211:5:1:[200.1,207.2,198.0,208.3,115.0,209.6,45.0,210.7,196.2,64.2,113.12,38.2]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))),iLEQ(suc(x0),suc(x0)),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))) -> 'LE'(f(x0),s(s('0')))
% 2.32/1.00 === Clause set with instances from active satisfied. Growing active. New size: 73
% 2.32/1.01 === Restarting.
% 2.32/1.01 === Backtracking. Learning clause 212:3:1:[16.1,115.2]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0')),'E'(s(s('0')),f(x0))
% 2.32/1.01 === Clause set with instances from active satisfied. Growing active. New size: 80
% 2.32/1.01 === Restarting.
% 2.32/1.01 === Conflict found: 149:9:2:[33.6,58.1,84.8,148.3]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x1))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(x1))))) {x0 -> suc(suc('0')), x1 -> '0'}
% 2.32/1.01 === Backtracking. Learning clause 214:6:1:[115.0,213.1,149.1,198.1]:Top: iLEQ(suc(suc(suc(x0))),suc(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(x0)) -> 'E'(f(suc(suc(x0))),f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(suc(x0))))),'LE'(f(suc(x0)),s(s('0')))
% 2.32/1.01 === Conflict found: 147:6:1:[142.4,57.2,6.2,146.4]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0)) {x0 -> suc(suc('0'))}
% 2.32/1.01 === Backtracking. Learning clause 215:6:1:[147.1,198.1]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'E'(f(suc(x0)),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(x0),s(s('0')))
% 2.32/1.01 === Conflict found: 141:6:1:[57.6,50.3,52.4,139.4,6.2,140.6]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(suc('0'))}
% 2.32/1.01 === Backtracking. Learning clause 216:6:1:[141.1,198.1,38.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(suc(suc(x0))))))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))) -> iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(x0),s(s('0')))
% 2.32/1.01 === Conflict found: 142:5:1:[6.2,52.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)) {x0 -> '0'}
% 2.32/1.01 === Backtracking. Learning clause 218:4:1:[115.0,217.0,142.1,198.1]:Top: 'E'(s(s('0')),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s(s('0')))
% 2.32/1.01 === Backtracking. Learning clause 219:4:1:[6.1,198.1]:Top: 'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(suc(x0)),f(suc(suc(x0)))),iLEQ(suc(suc(x0)),suc(suc(x0))),'LE'(f(x0),s(s('0')))
% 2.32/1.01 === Conflict found: 200:3:1:[198.0,199.1,181.3,142.5,115.1]:Top: 'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s(s('0'))) {x0 -> '0'}
% 2.32/1.01 === Backtracking. Learning clause 220:3:1:[200.1,198.1]:Top: -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s(s('0'))),'LE'(f(suc(x0)),s(s('0')))
% 2.32/1.01 === Clause set with instances from active satisfied. Growing active. New size: 144
% 2.32/1.01 === Backtracking. Learning clause 221:7:1:[64.1,45.1,47.1,169.3]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)) -> 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(x0)))))))),'LE'(f(x0),s('0')),iLEQ(suc(x0),suc(x0))
% 2.32/1.01 === Clause set with instances from active satisfied. Growing active. New size: 145
% 2.32/1.01 === Restarting.
% 2.32/1.01 === Backtracking. Learning clause 222:3:0:[47.3,201.1]:: 'LE'(f(suc(suc(z))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(z)))),'E'('0',f(z))
% 2.32/1.01 === Backtracking. Learning clause 223:3:0:[5.3,201.1]:: 'LE'(f(suc(suc(suc(suc(z))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(z)))))),'E'('0',f(z))
% 2.32/1.01 === Backtracking. Learning clause 224:3:1:[26.4,36.5]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 2.32/1.01 === Conflict found: 224:3:1:[26.4,36.5]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0))) {x0 -> s('0')}
% 2.32/1.01 === Backtracking. Learning clause 225:4:1:[224.2,212.1,9.2]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x0)),'LE'(f(x0),s('0'))
% 2.32/1.01 === Clause set with instances from active satisfied. Growing active. New size: 150
% 2.32/1.01 === Restarting.
% 2.32/1.01 === Conflict found: 225:4:1:[224.2,212.1,9.2]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x0)),'LE'(f(x0),s('0')) {x0 -> suc(z)}
% 2.32/1.01 === Backtracking. Learning clause 226:4:0:[225.4,202.1]:: 'LE'(f(suc(suc(z))),s(s('0'))) -> 'E'(f(suc(z)),f(suc(suc(z)))),'E'(s(s('0')),f(suc(z))),'E'('0',f(suc(z)))
% 2.32/1.01 === Backtracking. Learning clause 227:3:0:[9.3,202.1]:: 'LE'(f(suc(suc(z))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(z)))),'E'('0',f(suc(z)))
% 2.32/1.01 === Backtracking. Learning clause 230:3:0:[227.1,228.1,202.0,229.3,33.3,6.4,226.3,198.1,16.1,224.2]:: 'LE'(f(suc(suc(z))),s(s('0'))) -> 'E'('0',f(suc(z))),'E'(f(suc(z)),f(suc(suc(z))))
% 2.32/1.01 === Clause set with instances from active satisfied. Growing active. New size: 157
% 2.32/1.01 === Restarting.
% 2.32/1.01 === Backtracking. Learning clause 231:3:0:[47.3,203.1]:: 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(z))))))),'E'('0',f(suc(suc(suc(z)))))
% 2.32/1.01 === Backtracking. Learning clause 232:3:0:[55.3,203.1]:: 'LE'(f(suc(suc(suc(suc(suc(suc(z))))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(z)))))))),'E'('0',f(suc(suc(suc(z)))))
% 2.32/1.01 === Backtracking. Learning clause 233:3:0:[16.3,203.1]:: 'LE'(f(suc(suc(suc(z)))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(z))))),'E'('0',f(suc(suc(suc(z)))))
% 2.32/1.01 === Conflict found: 196:14:2:[154.11,76.2,88.15,194.5,172.13,195.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(suc(x1)))))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> {x0 -> z, x1 -> z}
% 2.32/1.01 === Backtracking. Learning clause 234:7:1:[196.5,113.12,206.4,53.6,141.6]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) ->
% 2.32/1.01 === Conflict found: 196:14:2:[154.11,76.2,88.15,194.5,172.13,195.6]:TopTop: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(suc(x1)))))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(x1))))),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(x1))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x1)) -> {x0 -> z, x1 -> z}
% 2.32/1.01 === Backtracking. Learning clause 235:5:1:[196.5,113.12,206.4,33.6,141.6]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) ->
% 2.32/1.01 === Backtracking. Learning clause 236:9:1:[16.2,36.2,18.3,212.1,235.2]:Top: iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s(s(s('0')))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> 'LE'(f(x0),s('0')),'E'(f(x0),f(suc(x0))),'LE'(f(suc(x0)),s('0'))
% 2.32/1.01 === Clause set with instances from active satisfied. Growing active. New size: 161
% 2.32/1.01 === Restarting.
% 2.32/1.01 === Conflict found: 225:4:1:[224.2,212.1,9.2]:Top: 'LE'(f(suc(x0)),s(s('0'))) -> 'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x0)),'LE'(f(x0),s('0')) {x0 -> suc(suc(z))}
% 2.32/1.01 === Backtracking. Learning clause 237:4:0:[225.4,204.1]:: 'LE'(f(suc(suc(suc(z)))),s(s('0'))) -> 'E'(f(suc(suc(z))),f(suc(suc(suc(z))))),'E'(s(s('0')),f(suc(suc(z)))),'E'('0',f(suc(suc(z))))
% 2.32/1.01 === Conflict found: 212:3:1:[16.1,115.2]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0')),'E'(s(s('0')),f(x0)) {x0 -> suc(suc(z))}
% 2.32/1.01 === Backtracking. Learning clause 238:3:0:[212.2,204.1]:: -> 'E'(s('0'),f(suc(suc(z)))),'E'(s(s('0')),f(suc(suc(z)))),'E'('0',f(suc(suc(z))))
% 2.32/1.01 === Backtracking. Learning clause 240:5:1:[115.1,239.0,28.1,56.2,51.2,9.3,212.2]:Top: -> 'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0'),'E'(s('0'),f(suc(x0))),'E'(s(s('0')),f(suc(x0)))
% 2.32/1.01 === Conflict found: 235:5:1:[196.5,113.12,206.4,33.6,141.6]:Top: 'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> {x0 -> '0'}
% 2.32/1.01 === Backtracking. Learning clause 241:5:1:[235.2,18.2,115.1,38.2,64.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s(s('0')))),'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 2.32/1.01 === Clause set with instances from active satisfied. Growing active. New size: 225
% 2.32/1.01 === Backtracking. Learning clause 242:2:1:[64.1,45.1]:Top: -> 'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s(s('0')))
% 2.32/1.01 === Backtracking. Learning clause 243:2:1:[38.1,45.1,235.4,198.1,115.1,242.1]:Top: 'E'(s(s('0')),f(suc(suc(x0)))) -> 'LE'(f(x0),s(s('0')))
% 2.32/1.01 === Backtracking. Learning clause 244:1:1:[49.1,45.1,243.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 2.32/1.01 === Backtracking. Learning clause 245:2:1:[16.1,244.1]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 2.32/1.01 === Backtracking. Learning clause 246:3:1:[53.5,28.4]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 2.32/1.01 === Conflict found: 93:15:2:[46.13,15.0,22.11,92.14]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x1)) -> {x0 -> suc(suc(z)), x1 -> suc(suc(z))}
% 2.32/1.01 === Backtracking. Learning clause 247:2:1:[93.8,138.12,136.10,224.3,169.6,5.2,244.1,55.2,244.1,47.2,244.1,245.1]:Top: 'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),s('0'))
% 2.32/1.01 === Backtracking. Learning clause 248:2:1:[47.1,244.1]:Top: -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 2.32/1.01 === Backtracking. Learning clause 249:2:1:[47.2,247.1,244.1]:Top: -> 'LE'(f(x0),s('0')),'LE'(f(suc(x0)),s('0'))
% 2.32/1.01 === Backtracking. Learning clause 250:1:1:[9.2,247.1,244.1]:Top: -> 'LE'(f(x0),s('0'))
% 2.32/1.01 === Backtracking. Learning clause 251:5:0:[28.1,223.3,202.2]:: 'LE'(f(suc(suc(suc(suc(z))))),s(s('0'))),'LE'(f(suc(z)),s('0')) -> 'E'(f(z),f(suc(z))),iLEQ(suc(z),suc(z)),'E'(s('0'),f(suc(suc(suc(suc(z))))))
% 2.32/1.01 === Backtracking. Learning clause 252:4:0:[53.2,223.3,202.2,251.4]:: 'LE'(f(suc(suc(suc(suc(z))))),s(s('0'))),'LE'(f(suc(z)),s('0')) -> 'E'(f(z),f(suc(z))),'E'(s('0'),f(suc(suc(suc(suc(z))))))
% 2.32/1.01 === Backtracking. Learning clause 253:5:0:[2.1,250.1,86.1,151.5,203.2,204.2,65.1]:: 'E'('0',f(z)),'E'('0',f(suc(z))),'LE'(f(suc(suc(suc(z)))),s('0')),'LE'(f(suc(suc(z))),s('0')) -> iLEQ(suc(z),suc(z))
% 2.32/1.01 === Conflict found: 107:15:2:[71.13,25.5,42.11,106.12]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0))))) -> {x0 -> z, x1 -> z}
% 2.32/1.01 === Backtracking. Learning clause 254:4:0:[107.6,119.8,2.2,250.1,193.10,203.2,204.2,65.1,253.5,223.3,202.2,252.3,250.1]:: 'LE'(f(suc(suc(suc(z)))),s('0')),'LE'(f(suc(suc(z))),s('0')),'LE'(f(suc(suc(suc(suc(z))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(z))))))
% 2.32/1.01 === Backtracking. Learning clause 255:1:0:[56.1,250.1,65.1,246.1,202.2,250.1]:: -> 'E'(f(z),f(suc(z)))
% 2.32/1.01 === Conflict found: 253:5:0:[2.1,250.1,86.1,151.5,203.2,204.2,65.1]:: 'E'('0',f(z)),'E'('0',f(suc(z))),'LE'(f(suc(suc(suc(z)))),s('0')),'LE'(f(suc(suc(z))),s('0')) -> iLEQ(suc(z),suc(z)) {}
% 2.32/1.01 === Backtracking. Learning clause 256:3:0:[253.3,250.1,250.1]:: 'E'('0',f(z)),'E'('0',f(suc(z))) -> iLEQ(suc(z),suc(z))
% 2.32/1.01 === Backtracking. Learning clause 257:1:0:[56.1,250.1,65.1,256.1,202.2,250.1]:: -> iLEQ(suc(z),suc(z))
% 2.32/1.01 === Conflict found: 107:15:2:[71.13,25.5,42.11,106.12]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0))))) -> {x0 -> z, x1 -> z}
% 2.32/1.01 === Backtracking. Learning clause 259:1:0:[257.0,258.1,107.6,119.8,2.2,250.1,193.10,31.2,13.2,250.1,250.1,65.1,255.1,202.2,250.1]:: 'E'('0',f(z)) ->
% 2.32/1.01
% 2.32/1.01 SZS status Unsatisfiable
% 2.32/1.01
% 2.32/1.01 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.32/1.01
% 2.32/1.01 SPASS-SCL-FOL Statistics:
% 2.32/1.01 Number of learned clauses: 51
% 2.32/1.01 Number of propagations: 1060
% 2.32/1.01 Number of decisions: 832
% 2.32/1.01 Number of resolutions: 136
% 2.32/1.01 Number of condensations: 0
% 2.32/1.01 Number of sub resolutions: 131
% 2.32/1.01 Number of input literals (deduplicated): 37
% 2.32/1.01 Number of grows: 10
% 2.32/1.01 Number of considered ground atoms: 225
% 2.32/1.01
% 2.32/1.01 Needed: 0:00:00.49
% 2.32/1.01
%------------------------------------------------------------------------------