%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO660-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 : n011.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 1.42s 0.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO660-1 : TPTP v9.2.1. Released v7.3.0.
% 0.13/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n011.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 13:56:03 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.35 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83 Execution resolution_2 ended with status: unsatisfiable
% 1.42/0.83 Used heuristic: resolution_2
% 1.42/0.83
% 1.42/0.83 Input Clauses:
% 1.42/0.83
% 1.42/0.83 Predicates: 'LE' 'E' iLEQ
% 1.42/0.83 Fol Constants: '0' z
% 1.42/0.83 Fol Functions: suc f s
% 1.42/0.83 Problem Properties:
% 1.42/0.83 This is a full first-order problem without equality.
% 1.42/0.83
% 1.42/0.83 After reduction: Problem Properties:
% 1.42/0.83 This is a full first-order problem without equality.
% 1.42/0.83
% 1.42/0.83
% 1.42/0.83 Reduced Input Clauses:
% 1.42/0.83 75:10:2:[67.6,2.7]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 1.42/0.83 78:18:2:[51.17,7.7,48.15,76.14,56.13,77.16]:TopTop: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(suc(suc(suc(x1))))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(x1))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) ->
% 1.42/0.83 81:15:2:[55.13,8.5,30.11,79.11,75.9,80.13]:TopTop: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(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(x1)),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 1.42/0.83 84:10:2:[32.10,9.6,46.8,82.8,53.6,83.9]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 86:14:2:[68.9,10.3,46.7,85.12]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1))))
% 1.42/0.83 89:11:2:[15.9,11.4,62.7,87.9,67.5,88.10]:TopTop: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),iLEQ(suc(x0),suc(x1)),'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(suc(x0)))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(x1)))
% 1.42/0.83 91:8:1:[41.4,12.2,70.2,90.7]:Top: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x0),suc(x0))
% 1.42/0.83 93:11:2:[69.9,13.7,60.7,92.9]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1))))
% 1.42/0.83 95:12:2:[45.7,14.2,53.5,94.11]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1)))
% 1.42/0.83 97:9:2:[62.7,15.6,67.5,96.7]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1)))
% 1.42/0.83 100:15:2:[19.11,16.3,86.15,98.13,95.13,99.15]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 1.42/0.83 102:16:2:[27.15,17.3,25.13,101.14]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(suc(x1))))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 1.42/0.83 105:12:2:[19.12,18.7,68.10,103.9,84.11,104.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 107:11:2:[68.10,19.7,45.8,106.9]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 1.42/0.83 112:15:2:[105.13,20.3,100.17,108.12,86.15,109.15,84.11,110.16,95.13,111.17]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 113:14:2:[62.8,21.9]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 115:11:2:[67.6,22.8,75.10,114.9]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 118:17:2:[51.17,23.6,48.15,116.13,56.13,117.15]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(suc(suc(suc(x1))))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(x1))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 1.42/0.83 122:10:2:[32.10,25.7,84.12,119.9,46.8,120.10,53.6,121.11]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(suc(x1))))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0)))
% 1.42/0.83 125:10:2:[97.9,26.3,62.7,123.8,67.5,124.9]:TopTop: iLEQ(suc(x0),suc(x1)),'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(suc(x0)))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1)))
% 1.42/0.83 129:12:2:[107.12,27.8,105.14,126.10,68.10,127.11,122.13,128.12]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(suc(x1))))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0))))
% 1.42/0.83 131:11:2:[62.8,30.8,75.9,130.9]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 1.42/0.83 133:15:2:[107.11,31.3,32.9,132.12]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 1.42/0.83 135:9:2:[46.8,32.6,53.6,134.7]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 1.42/0.83 137:13:2:[107.11,33.3,135.9,136.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 1.42/0.83 140:14:2:[105.13,34.3,137.14,138.8,84.11,139.12]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 143:16:2:[105.13,36.3,140.15,141.8,84.11,142.14]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 145:13:2:[68.9,37.3,46.7,144.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(x1))))
% 1.42/0.83 149:13:2:[55.13,38.4,131.11,146.10,125.12,147.11,75.9,148.12]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(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(x1)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 1.42/0.83 152:7:1:[65.6,39.2,71.4,150.5,6.2,151.6]: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(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x0),suc(x0))
% 1.42/0.83 153:5:1:[70.2,41.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))
% 1.42/0.83 155:6:1:[153.4,43.2,70.2,154.5]:Top: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 1.42/0.83 158:14:2:[113.13,44.9,97.10,156.10,115.11,157.11]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 159:8:2:[53.5,45.5]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 1.42/0.83 160:8:2:[53.6,46.5]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 1.42/0.83 162:11:2:[68.9,47.3,160.7,161.8]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1))))
% 1.42/0.83 165:13:2:[113.14,48.8,62.8,163.11,131.12,164.13]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(suc(suc(suc(x1))))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0))))
% 1.42/0.83 168:18:2:[129.15,49.3,102.17,166.11,122.13,167.18]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(suc(x1))))))),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) ->
% 1.42/0.83 170:11:2:[159.7,50.2,53.5,169.9]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1)))
% 1.42/0.83 173:15:2:[158.16,51.8,165.15,171.11,97.10,172.12]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(suc(suc(suc(x1))))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 1.42/0.83 175:9:2:[159.7,52.2,53.5,174.7]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1)))
% 1.42/0.83 179:7:1:[153.4,54.2,91.8,176.6,155.6,177.7,70.2,178.9]:Top: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0))
% 1.42/0.83 182:12:2:[131.11,55.8,97.10,180.9,75.9,181.10]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 1.42/0.83 185:11:2:[115.12,56.7,67.6,183.10,75.10,184.11]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(suc(suc(suc(x1))))))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0)))
% 1.42/0.83 189:16:2:[129.15,58.3,102.17,186.9,143.18,187.14,122.13,188.16]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(suc(x1))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 1.42/0.83 190:8:2:[67.6,60.6]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 1.42/0.83 191:2:1:[73.0,61.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 1.42/0.83 192:8:2:[67.5,62.6]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 1.42/0.83 196:12:2:[93.11,63.5,69.9,193.10,89.13,194.11,190.7,195.12]:TopTop: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(suc(x1))))
% 1.42/0.83 201:14:2:[158.15,64.5,113.13,197.11,125.12,198.12,115.11,199.13,149.16,200.14]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(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(x1)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 203:6:1:[71.4,65.3,6.2,202.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))))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0))
% 1.42/0.83 207:11:2:[93.11,66.4,69.9,204.9,125.12,205.10,190.7,206.11]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(x1))))
% 1.42/0.83 209:9:2:[160.7,68.6,159.8,208.7]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 1.42/0.83 211:9:2:[192.8,69.7,190.7,210.8]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 1.42/0.83 213:4:1:[6.2,71.2,211.0,212.5]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(x0))))
% 1.42/0.83 219:14:2:[158.15,72.6,113.13,214.12,89.13,215.13,115.11,216.14,201.17,217.16,213.4,218.18]:TopTop: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(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(x1)),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 223:7:1:[203.6,74.3,213.4,220.6,6.2,221.7,152.8,222.8]:Top: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),'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(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0))
% 1.42/0.83
% 1.42/0.83 Most General Atoms: 'LE'(f(x0),s('0')) iLEQ(suc(x0),suc(x1)) 'E'(s('0'),f(x1)) 'LE'(f(x0),'0') 'E'(f(x1),f(suc(x1))) 'E'(f(x0),f(suc(suc(suc(suc(x0)))))) 'E'('0',f(x1)) 'E'(f(x0),f(suc(suc(suc(x0))))) 'E'(f(x0),f(suc(suc(x0)))) 'LE'(f(x0),s(s('0')))
% 1.42/0.83
% 1.42/0.83 === Starting SPASS-SCL-FOL A Little Less Naive, considering 63 atoms initially, heuristics mode: resolution_2 ===
% 1.42/0.83
% 1.42/0.83 === Conflict found: 182:12:2:[131.11,55.8,97.10,180.9,75.9,181.10]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1))))) {x0 -> '0', x1 -> '0'}
% 1.42/0.83 === Backtracking. Learning clause 224:6:1:[182.1,203.6,40.2,191.1,29.2]:Top: 'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 1.42/0.83 === Conflict found: 137:13:2:[107.11,33.3,135.9,136.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1))))) {x0 -> '0', x1 -> '0'}
% 1.42/0.83 === Backtracking. Learning clause 225:9:1:[137.10,53.6,155.6,4.2,224.6]:Top: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(f(x0),f(suc(suc(suc(x0)))))
% 1.42/0.83 === Conflict found: 223:7:1:[203.6,74.3,213.4,220.6,6.2,221.7,152.8,222.8]:Top: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),'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(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0)) {x0 -> '0'}
% 1.42/0.83 === Backtracking. Learning clause 228:6:1:[191.0,226.1,73.0,227.5,223.1,57.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s('0'))
% 1.42/0.83 === Conflict found: 78:18:2:[51.17,7.7,48.15,76.14,56.13,77.16]:TopTop: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(suc(suc(suc(x1))))))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(f(x1),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x1),f(suc(x1))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> {x0 -> '0', x1 -> '0'}
% 1.42/0.83 === Backtracking. Learning clause 233:5:1:[224.4,229.0,73.0,230.3,73.0,231.6,73.0,232.7,78.14,67.6,57.2,228.5,29.2,191.1,40.2]:Top: 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> 'LE'(f(x0),s('0'))
% 1.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 63
% 1.42/0.83 === Restarting.
% 1.42/0.83 === Backtracking. Learning clause 234:2:0:[59.3,3.1]:: 'LE'(f(suc(suc(suc(suc(suc(z)))))),s('0')) -> 'E'('0',f(suc(suc(suc(suc(suc(z)))))))
% 1.42/0.83 === Backtracking. Learning clause 235:2:0:[42.3,3.1]:: 'LE'(f(suc(suc(suc(suc(z))))),s('0')) -> 'E'('0',f(suc(suc(suc(suc(z))))))
% 1.42/0.83 === Backtracking. Learning clause 236:2:0:[28.3,3.1]:: 'LE'(f(suc(suc(suc(z)))),s('0')) -> 'E'('0',f(suc(suc(suc(z)))))
% 1.42/0.83 === Backtracking. Learning clause 237:2:0:[24.3,3.1]:: 'LE'(f(suc(z)),s('0')) -> 'E'('0',f(suc(z)))
% 1.42/0.83 === Backtracking. Learning clause 238:2:0:[5.3,3.1]:: 'LE'(f(suc(suc(z))),s('0')) -> 'E'('0',f(suc(suc(z))))
% 1.42/0.83 === Backtracking. Learning clause 239:2:0:[4.3,3.1]:: 'LE'(f(z),s('0')) -> 'E'('0',f(z))
% 1.42/0.83 === Conflict found: 223:7:1:[203.6,74.3,213.4,220.6,6.2,221.7,152.8,222.8]:Top: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),'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(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0)) {x0 -> '0'}
% 1.42/0.83 === Backtracking. Learning clause 240:7:1:[223.5,35.2,1.2,191.1,40.2,29.2,57.2]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(suc(suc(suc(x0)))))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s('0'))
% 1.42/0.83 === Conflict found: 201:14:2:[158.15,64.5,113.13,197.11,125.12,198.12,115.11,199.13,149.16,200.14]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(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(x1)),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(suc(x1)))))) {x0 -> z, x1 -> z}
% 1.42/0.83 === Backtracking. Learning clause 241:13:2:[201.12,213.4]:TopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 69
% 1.42/0.83 === Restarting.
% 1.42/0.83 === Conflict found: 240:7:1:[223.5,35.2,1.2,191.1,40.2,29.2,57.2]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(suc(suc(suc(x0)))))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s('0')) {x0 -> suc('0')}
% 1.42/0.83 === Backtracking. Learning clause 242:6:1:[240.1,73.1]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(suc(suc(suc(x0)))))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s('0'))
% 1.42/0.83 === Conflict found: 224:6:1:[182.1,203.6,40.2,191.1,29.2]:Top: 'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0')) {x0 -> suc(suc(suc('0')))}
% 1.42/0.83 === Backtracking. Learning clause 243:5:1:[224.3,73.1]:Top: 'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'LE'(f(x0),s('0'))
% 1.42/0.83 === Backtracking. Learning clause 244:2:1:[1.1,73.1]:Top: -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 1.42/0.83 === Conflict found: 219:14:2:[158.15,72.6,113.13,214.12,89.13,215.13,115.11,216.14,201.17,217.16,213.4,218.18]:TopTop: 'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))),iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(suc(suc(suc(x1)))))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(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(x1)),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(suc(suc(suc(x1)))))) {x0 -> z, x1 -> z}
% 1.42/0.83 === Backtracking. Learning clause 245:8:0:[219.14,233.1,29.2,243.4,244.1,35.2,40.2,242.5,57.2,239.1]:: 'E'(s('0'),f(z)),'E'(f(z),f(suc(suc(z)))),'LE'(f(suc(suc(suc(suc(z))))),s(s('0'))),'LE'(f(suc(z)),s(s('0'))),'LE'(f(suc(suc(z))),s(s('0'))),'LE'(f(suc(suc(suc(z)))),s(s('0'))),'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s('0'))) -> 'E'('0',f(z))
% 1.42/0.83 === Conflict found: 233:5:1:[224.4,229.0,73.0,230.3,73.0,231.6,73.0,232.7,78.14,67.6,57.2,228.5,29.2,191.1,40.2]:Top: 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> 'LE'(f(x0),s('0')) {x0 -> z}
% 1.42/0.83 === Backtracking. Learning clause 252:2:1:[191.0,246.1,73.0,247.2,73.0,248.3,73.0,249.4,73.0,250.5,73.0,251.6,233.1,241.12,35.2,242.5,244.1,29.2,40.2]:Top: 'E'(f(x0),f(suc(suc(x0)))) -> 'LE'(f(x0),s('0'))
% 1.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 83
% 1.42/0.83 === Restarting.
% 1.42/0.83 === Conflict found: 242:6:1:[240.1,73.1]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'LE'(f(suc(suc(suc(suc(suc(x0)))))),s(s('0'))) -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s('0')) {x0 -> suc(suc(suc(suc(suc(z)))))}
% 1.42/0.83 === Backtracking. Learning clause 253:6:0:[242.6,234.1]:: 'LE'(f(suc(suc(suc(suc(suc(suc(z))))))),s(s('0'))),'LE'(f(suc(suc(suc(suc(suc(suc(suc(z)))))))),s(s('0'))),'LE'(f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))),s(s('0'))),'LE'(f(suc(suc(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))),s(s('0'))) -> iLEQ(suc(suc(suc(suc(suc(suc(z)))))),suc(suc(suc(suc(suc(suc(z))))))),'E'('0',f(suc(suc(suc(suc(suc(z)))))))
% 1.42/0.83 === Backtracking. Learning clause 254:3:0:[40.3,234.1]:: 'LE'(f(suc(suc(suc(suc(suc(suc(suc(z)))))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(z))))))))),'E'('0',f(suc(suc(suc(suc(suc(z)))))))
% 1.42/0.83 === Backtracking. Learning clause 255:3:0:[35.3,234.1]:: 'LE'(f(suc(suc(suc(suc(suc(suc(suc(suc(suc(z)))))))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))),'E'('0',f(suc(suc(suc(suc(suc(z)))))))
% 1.42/0.83 === Backtracking. Learning clause 256:3:0:[29.3,234.1]:: 'LE'(f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(suc(z)))))))))),'E'('0',f(suc(suc(suc(suc(suc(z)))))))
% 1.42/0.83 === Backtracking. Learning clause 257:2:0:[1.3,234.1,73.1]:: -> 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(z)))))))),'E'('0',f(suc(suc(suc(suc(suc(z)))))))
% 1.42/0.83 === Backtracking. Learning clause 258:2:1:[35.1,73.1]:Top: -> 'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),s('0'))
% 1.42/0.83 === Backtracking. Learning clause 259:6:1:[42.1,191.2,91.4,155.5,28.2,244.2,24.2,29.3,5.2,40.3]:Top: 'E'('0',f(x0)),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(suc(x0))))))
% 1.42/0.83 === Conflict found: 213:4:1:[6.2,71.2,211.0,212.5]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))) {x0 -> suc(suc(suc(suc(suc(z)))))}
% 1.42/0.83 === Backtracking. Learning clause 260:1:0:[213.4,252.1,40.2,73.1,191.1,257.1,234.1]:: -> 'E'('0',f(suc(suc(suc(suc(suc(z)))))))
% 1.42/0.83 === Conflict found: 140:14:2:[105.13,34.3,137.14,138.8,84.11,139.12]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(suc(x1)))))) {x0 -> z, x1 -> z}
% 1.42/0.83 === Backtracking. Learning clause 261:14:2:[140.11,53.6]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'('0',f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))),iLEQ(suc(x1),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 1.42/0.83 === Conflict found: 189:16:2:[129.15,58.3,102.17,186.9,143.18,187.14,122.13,188.16]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(suc(x1))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))) {x0 -> z, x1 -> z}
% 1.42/0.83 === Backtracking. Learning clause 262:4:1:[189.14,53.6,261.13,209.8,5.2,40.3,24.2,29.3,259.4,73.1,4.2,28.2,244.2,42.2,191.2,258.2]:Top: 'E'('0',f(suc(suc(suc(suc(suc(x0))))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(suc(x0))))))
% 1.42/0.83 === Conflict found: 213:4:1:[6.2,71.2,211.0,212.5]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))) {x0 -> z}
% 1.42/0.83 === Backtracking. Learning clause 263:2:1:[213.3,191.1,244.1,252.1]:Top: 'E'(s('0'),f(suc(suc(x0)))) -> 'LE'(f(x0),s('0'))
% 1.42/0.83 === Backtracking. Learning clause 264:1:1:[40.1,73.1,263.1]:Top: -> 'LE'(f(x0),s('0'))
% 1.42/0.83 === Conflict found: 137:13:2:[107.11,33.3,135.9,136.10]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1))))) {x0 -> z, x1 -> z}
% 1.42/0.83 === Backtracking. Learning clause 265:2:0:[137.10,53.6,209.8,155.6,239.2,238.2,264.1,237.2,264.1,236.2,264.1]:: 'LE'(f(z),s('0')) -> 'E'(f(z),f(suc(suc(suc(z)))))
% 1.42/0.83 === Conflict found: 153:5:1:[70.2,41.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)) {x0 -> z}
% 1.42/0.83 === Backtracking. Learning clause 266:4:1:[153.5,209.5]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x0))) -> 'E'(f(x0),f(suc(suc(x0))))
% 1.42/0.83 === Conflict found: 153:5:1:[70.2,41.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)) {x0 -> z}
% 1.42/0.83 === Backtracking. Learning clause 267:5:0:[153.3,239.2]:: 'E'('0',f(suc(suc(z)))),'E'('0',f(suc(z))),'LE'(f(z),s('0')) -> 'E'(f(z),f(suc(suc(z)))),iLEQ(suc(z),suc(z))
% 1.42/0.83 === Conflict found: 209:9:2:[160.7,68.6,159.8,208.7]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> z, x1 -> z}
% 1.42/0.83 === Backtracking. Learning clause 268:4:0:[209.4,239.2,267.5]:: 'E'('0',f(suc(suc(z)))),'E'('0',f(suc(z))),'LE'(f(z),s('0')) -> 'E'(f(z),f(suc(suc(z))))
% 1.42/0.83 === Conflict found: 179:7:1:[153.4,54.2,91.8,176.6,155.6,177.7,70.2,178.9]:Top: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x0))))) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 1.42/0.83 === Backtracking. Learning clause 269:5:0:[179.4,260.1,235.2,264.1]:: 'E'('0',f(suc(z))),'E'('0',f(suc(suc(z)))),'E'('0',f(z)),'E'('0',f(suc(suc(suc(z))))) -> iLEQ(suc(z),suc(z))
% 1.42/0.83 === Conflict found: 168:18:2:[129.15,49.3,102.17,166.11,122.13,167.18]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(suc(suc(suc(suc(x1))))))),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(x1)))),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> {x0 -> z, x1 -> z}
% 1.42/0.83
% 1.42/0.83 SZS status Unsatisfiable
% 1.42/0.83
% 1.42/0.83 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83
% 1.42/0.83 SPASS-SCL-FOL Statistics:
% 1.42/0.83 Number of learned clauses: 34
% 1.42/0.83 Number of propagations: 365
% 1.42/0.83 Number of decisions: 192
% 1.42/0.83 Number of resolutions: 122
% 1.42/0.83 Number of condensations: 0
% 1.42/0.83 Number of sub resolutions: 161
% 1.42/0.83 Number of input literals (deduplicated): 32
% 1.42/0.83 Number of grows: 3
% 1.42/0.83 Number of considered ground atoms: 83
% 1.42/0.83
% 1.42/0.83 Needed: 0:00:00.29
% 1.42/0.83
%------------------------------------------------------------------------------