%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO663-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 : n009.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 8.29s 2.19s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO663-1 : TPTP v9.2.1. Released v7.3.0.
% 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.33 % Computer : n009.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:56:11 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 8.29/2.19 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.29/2.19 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.29/2.19 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.29/2.19 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.29/2.19 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.29/2.19 Execution resolution_2 ended with status: unsatisfiable
% 8.29/2.19 Used heuristic: resolution_2
% 8.29/2.19
% 8.29/2.19 Input Clauses:
% 8.29/2.19
% 8.29/2.19 Predicates: 'E' iLEQ 'LE'
% 8.29/2.19 Fol Constants: '0' z
% 8.29/2.19 Fol Functions: suc f s
% 8.29/2.19 Problem Properties:
% 8.29/2.19 This is a full first-order problem without equality.
% 8.29/2.19
% 8.29/2.19 After reduction: Problem Properties:
% 8.29/2.19 This is a full first-order problem without equality.
% 8.29/2.19
% 8.29/2.19
% 8.29/2.19 Reduced Input Clauses:
% 8.29/2.19 45:16:4:[12.14,1.8]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3)))
% 8.29/2.19 46:15:4:[19.14,2.3]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(x0)),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 8.29/2.19 47:18:4:[5.17,4.7]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x2)))) ->
% 8.29/2.19 48:17:4:[43.16,5.7]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3))),'E'(s('0'),f(suc(x1))) -> 'E'(f(x2),f(suc(x2)))
% 8.29/2.19 49:4:1:[33.2,6.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 8.29/2.19 51:15:4:[12.15,9.3,46.15,50.12]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 8.29/2.19 53:15:4:[44.15,10.4,46.14,52.8]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2)))
% 8.29/2.19 54:15:4:[19.13,12.10]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(x3))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(x3)))
% 8.29/2.19 56:16:4:[28.15,13.9,45.15,55.15]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x3),f(suc(x3)))
% 8.29/2.19 57:17:4:[43.15,14.7]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x2)))) -> 'E'(f(x1),f(suc(x1)))
% 8.29/2.19 59:15:4:[21.15,16.4,46.13,58.13]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 8.29/2.19 62:15:4:[45.16,17.4,51.16,60.9,53.16,61.14]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x0),f(suc(x0)))
% 8.29/2.19 63:16:4:[22.14,18.6]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x2)))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0)))
% 8.29/2.19 64:15:4:[25.12,20.6]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x2)))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 8.29/2.19 65:15:4:[19.11,21.11]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(x3))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 8.29/2.19 66:15:4:[25.14,22.6]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 8.29/2.19 67:16:4:[65.13,23.8]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(x3))),'E'('0',f(x3)),'E'(f(x0),f(suc(x0))),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 8.29/2.19 70:15:4:[28.16,24.4,59.16,68.13,51.15,69.15]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1)))
% 8.29/2.19 72:15:4:[65.14,28.11,54.13,71.13]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(x3))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x3),f(suc(x3)))
% 8.29/2.19 73:15:4:[25.11,29.11]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 8.29/2.19 74:2:1:[11.0,30.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 8.29/2.19 77:16:4:[56.17,31.5,70.17,75.10,62.17,76.17]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) ->
% 8.29/2.19 79:15:4:[73.15,32.7,66.13,78.13]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 8.29/2.19 80:4:1:[8.2,34.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0))
% 8.29/2.19 83:15:4:[67.16,35.5,59.15,81.9,53.15,82.15]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x2),f(suc(x2)))
% 8.29/2.19 84:15:4:[25.13,36.11]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 8.29/2.19 86:15:4:[84.15,37.6,66.15,85.13]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x2),f(suc(x2)))
% 8.29/2.19 88:16:4:[86.16,38.6,63.16,87.14]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x2)))) -> 'E'(f(x3),f(suc(x3)))
% 8.29/2.19 90:15:4:[84.14,39.6,64.14,89.12]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x2)))) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1)))
% 8.29/2.19 92:15:4:[73.13,40.7,64.13,91.12]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x2)))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 8.29/2.19 94:16:4:[79.15,41.7,92.16,93.8]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(x0)),'E'(f(x3),f(suc(x3))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x2)))) -> 'E'(f(x0),f(suc(x0)))
% 8.29/2.19 96:15:4:[73.14,43.12,84.13,95.13]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x1))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 8.29/2.19 97:15:4:[19.12,44.7]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(x3))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 8.29/2.19
% 8.29/2.19 Most General Atoms: 'E'('0',f(x3)) 'E'(f(x1),f(suc(x1))) 'LE'(f(x0),s('0')) 'LE'(f(x0),'0') iLEQ(suc(x3),suc(x2)) 'E'(s('0'),f(x0)) 'LE'(f(x0),s(s('0')))
% 8.29/2.19
% 8.29/2.19 === Starting SPASS-SCL-FOL A Little Less Naive, considering 49 atoms initially, heuristics mode: resolution_2 ===
% 8.29/2.19
% 8.29/2.19 === Conflict found: 77:16:4:[56.17,31.5,70.17,75.10,62.17,76.17]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> {x0 -> '0', x1 -> '0', x2 -> '0', x3 -> '0'}
% 8.29/2.19 === Backtracking. Learning clause 98:4:1:[77.14,54.13,80.4,15.2,3.2]:Top: 'E'('0',f(x0)),'LE'(f(suc(suc(x0))),s('0')),'LE'(f(suc(x0)),s('0')) -> 'LE'(f(suc(x0)),'0')
% 8.29/2.19 === Backtracking. Learning clause 99:6:1:[15.2,77.1,42.3,3.2,7.3,47.4,25.12]:Top: 'E'('0',f(suc(suc(x0)))),'LE'(f(suc(suc(x0))),s(s('0'))),iLEQ(suc(x0),suc(x0)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),'0')
% 8.29/2.19 === Conflict found: 80:4:1:[8.2,34.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 8.29/2.19 === Backtracking. Learning clause 100:5:1:[80.3,3.2,15.2,42.3,7.3,49.1,99.3]:Top: 'E'('0',f(suc(suc(x0)))),'LE'(f(suc(suc(x0))),s(s('0'))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),'0')
% 8.29/2.19 === Conflict found: 47:18:4:[5.17,4.7]:TopTopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(x2)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x3)))),'E'(s('0'),f(x1)),'E'(s('0'),f(x3)),iLEQ(suc(x2),suc(x0)),'E'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(x3))),'E'(s('0'),f(suc(x2))),'E'(s('0'),f(suc(suc(x1)))),iLEQ(suc(x3),suc(x2)),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(f(x0),f(suc(x0))),'E'(f(x3),f(suc(x3))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x2)))) -> {x0 -> z, x1 -> z, x2 -> z, x3 -> z}
% 8.29/2.19 === Backtracking. Learning clause 101:3:1:[47.8,96.14,49.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) ->
% 8.29/2.19 === Backtracking. Learning clause 102:4:1:[27.1,74.2,100.1,101.1]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(x0),'0')
% 8.29/2.19 === Clause set with instances from active satisfied. Growing active. New size: 49
% 8.29/2.19 === Restarting.
% 8.29/2.19 === Conflict found: 99:6:1:[15.2,77.1,42.3,3.2,7.3,47.4,25.12]:Top: 'E'('0',f(suc(suc(x0)))),'LE'(f(suc(suc(x0))),s(s('0'))),iLEQ(suc(x0),suc(x0)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),'0') {x0 -> '0'}
% 8.29/2.19 === Backtracking. Learning clause 103:5:1:[99.2,11.1]:Top: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),'0')
% 8.29/2.19 === Conflict found: 100:5:1:[80.3,3.2,15.2,42.3,7.3,49.1,99.3]:Top: 'E'('0',f(suc(suc(x0)))),'LE'(f(suc(suc(x0))),s(s('0'))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),'0') {x0 -> '0'}
% 8.29/2.19 === Backtracking. Learning clause 104:4:1:[100.2,11.1]:Top: 'E'('0',f(suc(suc(x0)))),'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),'0')
% 8.29/2.19 === Conflict found: 102:4:1:[27.1,74.2,100.1,101.1]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(x0),'0') {x0 -> '0'}
% 8.29/2.19 === Backtracking. Learning clause 105:3:1:[102.1,11.1]:Top: 'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'LE'(f(x0),'0')
% 8.29/2.19 === Backtracking. Learning clause 106:2:1:[42.1,11.1]:Top: -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),s('0'))
% 8.29/2.19 === Conflict found: 77:16:4:[56.17,31.5,70.17,75.10,62.17,76.17]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> {x0 -> z, x1 -> z, x2 -> z, x3 -> z}
% 8.29/2.19 === Backtracking. Learning clause 108:3:0:[74.1,107.2,77.14,46.13,15.2,3.2,27.2,26.1,7.3,11.1]:: iLEQ(suc(z),suc(z)),'LE'(f(suc(z)),s('0')) -> 'E'(s('0'),f(suc(suc(z))))
% 8.29/2.19 === Backtracking. Learning clause 109:1:0:[27.1,74.2,80.1,3.2,7.3,11.1,15.2,26.1,108.1,106.2]:: -> 'E'(s('0'),f(suc(suc(z))))
% 8.29/2.19 === Conflict found: 77:16:4:[56.17,31.5,70.17,75.10,62.17,76.17]:TopTopTopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x2),suc(x3)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),'E'('0',f(suc(x3))),'E'(f(x2),f(suc(x2))),'E'('0',f(x3)),iLEQ(suc(x1),suc(x2)) -> {x0 -> z, x1 -> z, x2 -> z, x3 -> z}
% 8.29/2.19 === Backtracking. Learning clause 111:3:1:[80.3,110.3,77.14,46.13]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) ->
% 8.29/2.19 === Conflict found: 101:3:1:[47.8,96.14,49.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> {x0 -> suc('0')}
% 8.29/2.19 === Backtracking. Learning clause 112:2:1:[101.2,106.1,7.2,74.1]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 8.29/2.19 === Backtracking. Learning clause 113:1:1:[7.1,11.1,101.1,74.1,106.1]:Top: -> 'LE'(f(x0),s('0'))
% 8.29/2.19 === Backtracking. Learning clause 114:2:0:[27.1,113.1,111.1,3.2,26.1]:: 'E'('0',f(suc(z))),'LE'(f(z),s('0')) ->
% 8.29/2.19
% 8.29/2.19 SZS status Unsatisfiable
% 8.29/2.19
% 8.29/2.19 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.29/2.19
% 8.29/2.19 SPASS-SCL-FOL Statistics:
% 8.29/2.19 Number of learned clauses: 15
% 8.29/2.19 Number of propagations: 152
% 8.29/2.19 Number of decisions: 67
% 8.29/2.19 Number of resolutions: 57
% 8.29/2.19 Number of condensations: 1
% 8.29/2.19 Number of sub resolutions: 55
% 8.29/2.19 Number of input literals (deduplicated): 17
% 8.29/2.19 Number of grows: 1
% 8.29/2.19 Number of considered ground atoms: 49
% 8.29/2.19
% 8.29/2.19 Needed: 0:00:01.63
% 8.29/2.19
%------------------------------------------------------------------------------