%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO679-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 : n028.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:17 PM UTC 2026
% Result : Unsatisfiable 3.15s 1.19s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYO679-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.14/0.32 % Computer : n028.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Thu May 7 13:56:16 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.33 SPASS-SCL-FOL version:
% 0.18/0.41 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 3.15/1.19 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.15/1.19 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.15/1.19 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.15/1.19 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.15/1.19 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.15/1.19 Execution normal ended with status: unsatisfiable
% 3.15/1.19 Used heuristic: normal
% 3.15/1.19
% 3.15/1.19 Input Clauses:
% 3.15/1.19
% 3.15/1.19 Predicates: 'E' iLEQ 'LE'
% 3.15/1.19 Fol Constants: '0' z
% 3.15/1.19 Fol Functions: s f suc
% 3.15/1.19 Problem Properties:
% 3.15/1.19 This is a full first-order problem without equality.
% 3.15/1.19
% 3.15/1.19 After reduction: Problem Properties:
% 3.15/1.19 This is a full first-order problem without equality.
% 3.15/1.19
% 3.15/1.19
% 3.15/1.19 Reduced Input Clauses:
% 3.15/1.19 103:8:2:[53.6,1.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))))
% 3.15/1.19 105:11:2:[33.9,2.0,103.7,104.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(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0))))
% 3.15/1.19 107:14:2:[11.14,6.0,12.10,106.8]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x0)),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 3.15/1.19 109:7:1:[60.4,8.0,44.2,108.7]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0))
% 3.15/1.19 111:14:2:[52.11,9.0,24.9,110.13]:TopTop: 'E'(s(s('0')),f(x0)),'E'(f(x0),f(suc(suc(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(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'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)))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 113:13:2:[19.11,11.1,23.9,112.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'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 115:9:2:[92.7,12.1,16.5,114.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(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0)))
% 3.15/1.19 116:13:2:[71.11,13.1]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(x1))))),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'(f(x1),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x1)))))) -> 'E'(f(x0),f(suc(suc(x0))))
% 3.15/1.19 119:6:1:[36.6,14.0,59.4,117.4,32.2,118.5]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) -> iLEQ(suc(x0),suc(x0))
% 3.15/1.19 120:10:2:[92.8,17.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'(f(x1),f(suc(x1))),'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))))
% 3.15/1.19 121:2:1:[21.0,18.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 3.15/1.19 123:11:2:[92.8,19.4,120.10,122.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'(f(x1),f(suc(x1))),'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)))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 126:14:2:[31.13,22.0,68.11,124.14,111.15,125.15]:TopTop: 'E'(s(s('0')),f(x0)),'E'(f(x0),f(suc(suc(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(suc(suc(suc(x1)))))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'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)))) ->
% 3.15/1.19 127:10:2:[16.6,23.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(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 129:9:2:[103.8,24.1,53.6,128.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))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 131:10:2:[76.10,25.1,41.6,130.2]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(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)))
% 3.15/1.19 133:10:2:[49.7,27.0,53.5,132.10]: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(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'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)))
% 3.15/1.19 134:13:2:[86.11,29.1]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'(f(x0),f(suc(suc(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))))
% 3.15/1.19 136:12:2:[33.10,31.1,49.8,135.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(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'(f(x0),f(suc(suc(suc(x0))))),'E'(s(s('0')),f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1))))
% 3.15/1.19 138:9:2:[49.8,33.2,103.7,137.7]: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(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 3.15/1.19 139:5:1:[83.2,34.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))
% 3.15/1.19 141:10:2:[127.10,35.0,16.6,140.6]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(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'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(x1)))
% 3.15/1.19 143:6:1:[59.4,36.3,32.2,142.4]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 3.15/1.19 145:12:2:[120.9,37.1,98.7,144.8]: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(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 3.15/1.19 147:14:2:[71.11,38.1,116.13,146.14]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(x1))))),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'(f(x1),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x1)))))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 149:7:1:[82.4,39.0,30.2,148.4]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))) -> iLEQ(suc(x0),suc(x0))
% 3.15/1.19 151:11:2:[120.9,40.1,115.10,150.6]: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'(f(x1),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0))))
% 3.15/1.19 153:14:2:[86.11,42.1,134.13,152.12]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'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'(f(x0),f(suc(suc(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(suc(x1)))))
% 3.15/1.19 154:11:2:[3.5,45.0]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x1)))))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x1)))),'E'(f(x1),f(suc(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)))
% 3.15/1.19 155:12:2:[97.9,46.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)))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 156:10:2:[55.7,48.0]: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'(f(x0),f(suc(x0))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 3.15/1.19 157:8:2:[53.5,49.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)))
% 3.15/1.19 160:11:2:[123.12,51.0,92.8,158.6,141.11,159.7]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(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'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x1),f(suc(suc(x1))))
% 3.15/1.19 163:10:2:[138.10,52.1,157.8,161.3,129.9,162.9]: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(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 164:8:2:[3.5,54.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)))
% 3.15/1.19 165:8:2:[3.6,55.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))))
% 3.15/1.19 166:12:2:[87.10,56.1]: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'(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(suc(x1))))),'E'(f(x0),f(suc(suc(x0))))
% 3.15/1.19 168:13:2:[97.9,57.0,155.11,167.10]: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(x0),f(suc(x0))),'E'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 170:9:2:[3.5,58.0,164.7,169.7]: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'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0)))
% 3.15/1.19 171:5:1:[32.2,59.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))
% 3.15/1.19 173:4:1:[44.2,60.2,138.3,172.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))))
% 3.15/1.19 175:12:2:[165.7,61.0,156.9,174.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x1)))))),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'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)) -> 'E'(f(x0),f(suc(suc(x0))))
% 3.15/1.19 179:13:2:[78.15,62.0,160.13,176.2,141.11,177.10,145.13,178.14]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) ->
% 3.15/1.19 181:13:2:[87.10,63.1,166.12,180.12]: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'(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(suc(x1))))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 184:13:2:[97.9,64.0,175.13,182.3,154.11,183.13]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x1)))))),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'(f(x1),f(suc(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)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 187:13:2:[181.14,66.1,87.10,185.2,131.11,186.11]: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(suc(suc(suc(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(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(suc(x1)))))
% 3.15/1.19 189:7:1:[83.2,67.0,139.4,188.6]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0))
% 3.15/1.19 192:9:2:[103.8,68.1,53.6,190.3,129.10,191.9]: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(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)))
% 3.15/1.19 193:8:2:[41.6,69.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))))
% 3.15/1.19 196:9:2:[87.9,71.1,90.7,194.7,41.5,195.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(x1))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x1)))))) -> 'E'(f(x0),f(suc(x0)))
% 3.15/1.19 199:10:2:[165.7,73.0,156.9,197.8,170.10,198.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'('0',f(x1)) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0))))
% 3.15/1.19 201:6:1:[82.4,74.0,30.2,200.3]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 3.15/1.19 203:9:2:[41.6,76.1,193.8,202.8]: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(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 206:11:2:[138.9,77.0,133.11,204.3,103.7,205.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(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'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))))
% 3.15/1.19 209:13:2:[123.11,78.1,127.9,207.8,113.13,208.11]: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(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 212:9:2:[92.7,81.1,16.5,210.6,115.9,211.8]: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(suc(suc(suc(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)))
% 3.15/1.19 213:5:1:[30.2,82.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))
% 3.15/1.19 215:6:1:[173.4,84.0,44.2,214.5]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(x0)),'E'(s(s('0')),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 3.15/1.19 219:13:2:[147.15,85.1,196.11,216.2,187.15,217.3,131.11,218.12]: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(suc(suc(suc(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(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'(s(s(s('0'))),f(suc(suc(suc(suc(x1)))))),'E'(f(x0),f(suc(suc(x0)))) ->
% 3.15/1.19 221:10:2:[165.8,86.2,3.6,220.9]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(f(x0),f(suc(suc(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)))
% 3.15/1.19 223:9:2:[90.7,87.6,41.5,222.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(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0)))
% 3.15/1.19 226:12:2:[163.11,89.0,105.12,224.2,129.9,225.11]: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(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)))) -> 'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 227:8:2:[41.5,90.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)))
% 3.15/1.19 231:12:2:[136.13,91.0,105.12,228.2,192.11,229.12,226.14,230.13]: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(suc(suc(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)))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 3.15/1.19 232:8:2:[16.5,92.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)))
% 3.15/1.19 236:13:2:[221.11,94.1,175.13,233.4,184.15,234.7,154.11,235.15]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x1)))))),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'(f(x1),f(suc(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)) ->
% 3.15/1.19 238:6:1:[83.2,95.0,139.4,237.4]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 3.15/1.19 241:11:2:[102.12,96.1,227.8,239.2,131.11,240.9]:TopTop: 'E'(s(s(s('0'))),f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'(s(s(s('0'))),f(suc(suc(suc(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))))
% 3.15/1.19 243:9:2:[165.8,97.1,3.6,242.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))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 244:8:2:[16.6,98.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))))
% 3.15/1.19 246:9:2:[157.7,99.0,53.5,245.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(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0)))
% 3.15/1.19 248:9:2:[227.8,101.1,193.7,247.6]: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(x0)))),'E'(s(s(s('0'))),f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 3.15/1.19 251:10:2:[227.8,102.1,203.9,249.7,248.10,250.10]: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(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19
% 3.15/1.19 Most General Atoms: iLEQ(suc(x1),suc(x0)) 'E'(s(s('0')),f(x1)) 'E'(f(x0),f(suc(x0))) 'E'('0',f(x1)) 'LE'(f(x0),s('0')) 'LE'(f(x0),'0') 'E'(f(x1),f(suc(suc(x1)))) 'E'(s('0'),f(x1)) 'LE'(f(x0),s(s(s('0')))) 'LE'(f(x0),s(s('0'))) 'E'(f(x0),f(suc(suc(suc(x0))))) 'E'(s(s(s('0'))),f(x1)) 'LE'(f(x0),s(s(s(s('0')))))
% 3.15/1.19
% 3.15/1.19 === Starting SPASS-SCL-FOL A Little Less Naive, considering 93 atoms initially, heuristics mode: normal ===
% 3.15/1.19
% 3.15/1.19 === Conflict found: 189:7:1:[83.2,67.0,139.4,188.6]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 3.15/1.19 === Backtracking. Learning clause 252:7:1:[189.7,236.4]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(x0)) ->
% 3.15/1.19 === Clause set with instances from active satisfied. Growing active. New size: 157
% 3.15/1.19 === Clause set with instances from active satisfied. Growing active. New size: 221
% 3.15/1.19 === Backtracking. Learning clause 253:3:1:[72.1,21.1,20.1]:Top: -> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0')))
% 3.15/1.19 === Conflict found: 251:10:2:[227.8,102.1,203.9,249.7,248.10,250.10]: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(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> s('0'), x1 -> s('0')}
% 3.15/1.19 === Backtracking. Learning clause 254:6:1:[251.9,219.8,119.6]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 3.15/1.19 === Clause set with instances from active satisfied. Growing active. New size: 285
% 3.15/1.19 === Backtracking. Learning clause 255:3:1:[20.1,121.2]:Top: -> 'E'(s(s('0')),f(suc(suc(x0)))),'LE'(f(x0),s(s('0'))),'E'(s(s(s('0'))),f(suc(suc(x0))))
% 3.15/1.19 === Conflict found: 171:5:1:[32.2,59.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)) {x0 -> s('0')}
% 3.15/1.19 === Backtracking. Learning clause 256:5:1:[171.3,121.1,75.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s(s(s('0'))))) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s(s(s('0'))))
% 3.15/1.19 === Conflict found: 196:9:2:[87.9,71.1,90.7,194.7,41.5,195.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(x1))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x1)))))) -> 'E'(f(x0),f(suc(x0))) {x0 -> f('0'), x1 -> f('0')}
% 3.15/1.19 === Backtracking. Learning clause 257:6:1:[196.2,32.4,121.1,75.2]:Top: '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(suc(suc(suc(x0)))))),'LE'(f(suc(x0)),s(s(s(s('0'))))) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 3.15/1.19 === Clause set with instances from active satisfied. Growing active. New size: 349
% 3.15/1.19 === Backtracking. Learning clause 258:2:1:[75.1,21.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 3.15/1.19 === Conflict found: 248:9:2:[227.8,101.1,193.7,247.6]: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(x0)))),'E'(s(s(s('0'))),f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))) {x0 -> s('0'), x1 -> s('0')}
% 3.15/1.19 === Backtracking. Learning clause 259:4:1:[248.8,219.8,119.6,72.2,47.2,93.2,121.1,258.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s('0'))))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s(s('0'))))
% 3.15/1.19 === Backtracking. Learning clause 262:4:1:[121.0,260.1,258.0,261.2,72.1,21.1,119.3]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) -> 'LE'(f(x0),s(s(s('0')))),iLEQ(suc(x0),suc(x0))
% 3.15/1.19 === Backtracking. Learning clause 265:4:1:[121.0,263.0,258.0,264.1,72.1,21.1,248.5,262.4]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s(s(s('0'))))
% 3.15/1.19 === Backtracking. Learning clause 268:3:1:[258.0,266.0,121.0,267.1,72.1,21.1,171.1]:Top: -> 'LE'(f(x0),s(s(s('0')))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 3.15/1.19 === Backtracking. Learning clause 271:2:1:[121.0,269.0,258.0,270.1,72.1,21.1,248.5,268.3]:Top: -> 'LE'(f(x0),s(s(s('0')))),'E'(f(x0),f(suc(suc(x0))))
% 3.15/1.19 === Backtracking. Learning clause 274:4:1:[121.0,272.1,258.0,273.3,47.1,21.1,119.5]:Top: 'E'(s(s(s('0'))),f(suc(suc(suc(x0))))),'E'(s(s(s('0'))),f(suc(suc(x0)))) -> 'LE'(f(x0),s(s(s('0')))),iLEQ(suc(x0),suc(x0))
% 3.15/1.19 === Conflict found: 259:4:1:[248.8,219.8,119.6,72.2,47.2,93.2,121.1,258.1]:Top: 'LE'(f(suc(suc(x0))),s(s(s(s('0'))))),'LE'(f(suc(suc(suc(suc(x0))))),s(s(s(s('0'))))),'LE'(f(suc(suc(suc(x0)))),s(s(s(s('0'))))) -> 'LE'(f(x0),s(s(s('0')))) {x0 -> s('0')}
% 3.15/1.19 === Backtracking. Learning clause 275:1:1:[259.3,21.1,21.1,21.1]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 3.15/1.19 === Backtracking. Learning clause 276:6:1:[10.2,16.1,43.1,3.1]:Top: 'LE'(f(suc(x0)),s(s('0'))),'E'(s('0'),f(x0)),iLEQ(suc(x0),suc(x0)),'E'('0',f(x0)) -> 'LE'(f(x0),'0'),'E'(f(x0),f(suc(x0)))
% 3.15/1.19 === Backtracking. Learning clause 278:5:1:[275.0,277.1,44.2,28.2,7.2,10.1,30.1]:Top: 'LE'(f(suc(x0)),s(s(s('0')))),'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),s('0')),'E'(f(x0),f(suc(x0))),iLEQ(suc(x0),suc(x0))
% 3.15/1.19 === Conflict found: 201:6:1:[82.4,74.0,30.2,200.3]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0)) {x0 -> '0'}
% 3.15/1.19 === Backtracking. Learning clause 279:7:1:[201.5,149.5,88.2]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x0)))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s('0'))
% 3.15/1.19 === Backtracking. Learning clause 280:3:1:[44.4,53.3]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 3.15/1.19 === Conflict found: 280:3:1:[44.4,53.3]:Top: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> 'E'(f(x0),f(suc(x0))) {x0 -> s(z)}
% 3.15/1.19 === Backtracking. Learning clause 282:3:1:[275.0,281.1,280.1,28.2,7.2]:Top: 'LE'(f(suc(x0)),s(s(s('0')))) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 3.15/1.19 === Backtracking. Learning clause 283:5:1:[16.3,10.2,65.2]:Top: iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),s('0'))
% 3.15/1.19 === Clause set with instances from active satisfied. Growing active. New size: 413
% 3.15/1.19 === Backtracking. Learning clause 284:9:1:[10.1,255.2,149.6]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(suc(suc(x0))))) -> 'LE'(f(suc(suc(x0))),s('0')),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(s(s(s('0'))),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x0),suc(x0))
% 3.15/1.19 === Backtracking. Learning clause 285:6:1:[50.1,275.1,109.2,215.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))))) -> 'LE'(f(x0),s(s('0'))),iLEQ(suc(x0),suc(x0))
% 3.15/1.19 === Conflict found: 126:14:2:[31.13,22.0,68.11,124.14,111.15,125.15]:TopTop: 'E'(s(s('0')),f(x0)),'E'(f(x0),f(suc(suc(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(suc(suc(suc(x1)))))),'E'(s(s('0')),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'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 -> s(z), x1 -> s(z)}
% 3.15/1.19 === Backtracking. Learning clause 287:4:1:[275.0,286.3,126.2,173.4,50.2,275.1,226.11,285.6,15.2,20.2,282.2,28.2,7.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0')))
% 3.15/1.19 === Backtracking. Learning clause 288:2:1:[28.1,275.1]:Top: -> 'E'(s(s('0')),f(suc(x0))),'LE'(f(x0),s(s('0')))
% 3.15/1.19 === Conflict found: 287:4:1:[275.0,286.3,126.2,173.4,50.2,275.1,226.11,285.6,15.2,20.2,282.2,28.2,7.2]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s(s('0')))),'LE'(f(suc(suc(x0))),s(s(s('0')))),'LE'(f(suc(x0)),s(s(s('0')))) -> 'LE'(f(x0),s(s('0'))) {x0 -> s(z)}
% 3.15/1.19 === Backtracking. Learning clause 289:1:1:[287.2,275.1,275.1,275.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 3.15/1.19 === Conflict found: 179:13:2:[78.15,62.0,160.13,176.2,141.11,177.10,145.13,178.14]:TopTop: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> {x0 -> '0', x1 -> '0'}
% 3.15/1.19 === Backtracking. Learning clause 292:7:1:[289.0,290.0,289.0,291.1,179.8,283.4,149.7]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))) -> 'LE'(f(x0),s('0'))
% 3.15/1.19 === Conflict found: 209:13:2:[123.11,78.1,127.9,207.8,113.13,208.11]: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(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0))))) {x0 -> '0', x1 -> '0'}
% 3.15/1.19 === Backtracking. Learning clause 295:4:1:[289.0,293.3,289.0,294.4,209.10,123.10,283.4,201.6,292.5,65.2,4.2,88.2,10.2,79.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 3.15/1.19 === Backtracking. Learning clause 296:4:1:[3.2,83.4,43.2]:Top: 'E'('0',f(x0)),'LE'(f(suc(x0)),s('0')) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),'0')
% 3.15/1.19 === Backtracking. Learning clause 297:3:1:[3.2,83.4]:Top: 'E'('0',f(x0)),'E'('0',f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 3.15/1.19 === Clause set with instances from active satisfied. Growing active. New size: 477
% 3.15/1.19 === Conflict found: 295:4:1:[289.0,293.3,289.0,294.4,209.10,123.10,283.4,201.6,292.5,65.2,4.2,88.2,10.2,79.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> suc(z)}
% 3.15/1.19 === Backtracking. Learning clause 298:5:1:[295.2,289.1,296.2]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(x0))),'LE'(f(x0),'0')
% 3.15/1.19 === Conflict found: 236:13:2:[221.11,94.1,175.13,233.4,184.15,234.7,154.11,235.15]:TopTop: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x1)))))),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'(f(x1),f(suc(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}
% 3.15/1.19 === Backtracking. Learning clause 301:7:1:[297.2,299.4,289.0,300.6,236.8,168.12,100.2,26.2,10.3,65.3]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(x0)))))
% 3.15/1.19 === Clause set with instances from active satisfied. Growing active. New size: 541
% 3.15/1.19 === Conflict found: 295:4:1:[289.0,293.3,289.0,294.4,209.10,123.10,283.4,201.6,292.5,65.2,4.2,88.2,10.2,79.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> suc(suc(suc(z)))}
% 3.15/1.19 === Backtracking. Learning clause 302:3:1:[295.2,289.1]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 3.15/1.19 === Conflict found: 302:3:1:[295.2,289.1]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> suc(suc(suc(z)))}
% 3.15/1.19 === Backtracking. Learning clause 303:1:1:[302.1,289.1,289.1]:Top: -> 'LE'(f(x0),s('0'))
% 3.15/1.19 === Backtracking. Learning clause 304:3:0:[5.2,3.3,303.1,70.1]:: iLEQ(suc(z),suc(z)),'E'('0',f(suc(z))) -> 'E'(f(z),f(suc(z)))
% 3.15/1.19 === Backtracking. Learning clause 305:4:0:[80.1,303.1,236.1,168.12,156.9,26.2,100.2,5.2,70.1,303.1,304.3]:: 'LE'(f(suc(suc(suc(z)))),s('0')),'LE'(f(suc(suc(z))),s('0')),iLEQ(suc(z),suc(z)),'E'('0',f(suc(z))) ->
% 3.15/1.19 === Backtracking. Learning clause 306:3:0:[80.1,303.1,189.1,238.5,100.2,26.2,5.2,303.1,70.1,305.3]:: 'LE'(f(suc(suc(suc(z)))),s('0')),'LE'(f(suc(suc(z))),s('0')),'E'('0',f(suc(z))) ->
% 3.15/1.19
% 3.15/1.19 SZS status Unsatisfiable
% 3.15/1.19
% 3.15/1.19 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.15/1.19
% 3.15/1.19 SPASS-SCL-FOL Statistics:
% 3.15/1.19 Number of learned clauses: 36
% 3.15/1.19 Number of propagations: 1816
% 3.15/1.19 Number of decisions: 959
% 3.15/1.19 Number of resolutions: 118
% 3.15/1.19 Number of condensations: 0
% 3.15/1.19 Number of sub resolutions: 168
% 3.15/1.19 Number of input literals (deduplicated): 47
% 3.15/1.19 Number of grows: 7
% 3.15/1.19 Number of considered ground atoms: 541
% 3.15/1.19
% 3.15/1.19 Needed: 0:00:00.66
% 3.15/1.19
%------------------------------------------------------------------------------