%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO655-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 : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 7 07:41:15 PM UTC 2026
% Result : Unsatisfiable 19.67s 4.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO655-1 : TPTP v9.2.1. Released v7.3.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n007.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % 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:55:39 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]
% 19.67/4.49 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.67/4.49 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.67/4.49 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.67/4.49 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.67/4.49 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.67/4.49 Execution normal ended with status: unsatisfiable
% 19.67/4.49 Used heuristic: normal
% 19.67/4.49
% 19.67/4.49 Input Clauses:
% 19.67/4.49
% 19.67/4.49 Predicates: 'E' iLEQ 'LE'
% 19.67/4.49 Fol Constants: '0' z
% 19.67/4.49 Fol Functions: suc f s
% 19.67/4.49 Problem Properties:
% 19.67/4.49 This is a full first-order problem without equality.
% 19.67/4.49
% 19.67/4.49 After reduction: Problem Properties:
% 19.67/4.49 This is a full first-order problem without equality.
% 19.67/4.49
% 19.67/4.49
% 19.67/4.49 Reduced Input Clauses:
% 19.67/4.49 40:21:5:[32.19,1.9]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 41:20:5:[3.19,2.13]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'(f(x4),f(suc(x4))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1)))
% 19.67/4.49 42:19:5:[16.17,3.12]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 19.67/4.49 43:19:5:[16.14,4.8]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(x2)),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 44:19:5:[16.18,5.14]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 45:21:5:[38.19,6.10]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(f(x4),f(suc(x4))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1)))
% 19.67/4.49 46:20:5:[44.16,7.13]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 47:21:5:[46.18,8.9]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 49:20:5:[28.20,10.14,41.19,48.18]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'(f(x4),f(suc(x4))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 19.67/4.49 50:21:5:[28.19,12.9]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'(f(x4),f(suc(x4))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 19.67/4.49 52:19:5:[42.18,13.9,43.19,51.14]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1)))
% 19.67/4.49 54:19:5:[20.18,14.9,43.18,53.14]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 55:23:5:[31.22,15.11]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(f(x4),f(suc(x4))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) ->
% 19.67/4.49 57:21:5:[27.20,17.10,40.20,56.16]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x4),f(suc(x4)))
% 19.67/4.49 58:21:5:[41.18,18.14]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(f(x4),f(suc(x4))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1)))
% 19.67/4.49 60:20:5:[28.18,19.14,46.20,59.15]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 19.67/4.49 61:19:5:[16.16,20.12]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 63:19:5:[44.17,21.8,43.17,62.16]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 64:4:1:[23.2,22.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0))
% 19.67/4.49 65:20:5:[61.16,24.13]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 67:21:5:[60.20,25.10,50.20,66.16]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'(f(x4),f(suc(x4))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x1),f(suc(x1)))
% 19.67/4.49 69:19:5:[29.17,26.9,43.16,68.14]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(x2)),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 71:20:5:[32.18,27.14,46.19,70.15]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x1),f(suc(x1))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 73:19:5:[44.19,28.13,42.17,72.16]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 19.67/4.49 74:19:5:[16.15,29.12]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(x2)),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 77:19:5:[65.19,30.10,54.18,75.15,69.19,76.16]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 80:20:5:[49.20,31.15,60.21,78.16,71.21,79.17]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x1),f(suc(x1)))
% 19.67/4.49 82:19:5:[44.18,32.13,61.17,81.16]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(f(x4),f(suc(x4)))
% 19.67/4.49 84:21:5:[49.21,33.10,50.21,83.16]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'(f(x4),f(suc(x4))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2)))
% 19.67/4.49 87:19:5:[41.20,36.10,52.20,85.15,54.20,86.16]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x3),f(suc(x3)))
% 19.67/4.49 88:2:1:[35.0,37.0]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 19.67/4.49 90:19:5:[42.16,38.13,74.19,89.14]:TopTopTopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x1)),'E'('0',f(x0)),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),iLEQ(suc(x0),suc(x4)),'E'('0',f(x1)),'E'('0',f(x3)),'E'('0',f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x3),f(suc(x3))),'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(x0)))
% 19.67/4.49 93:20:5:[58.21,39.11,87.20,91.16,77.21,92.18]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'('0',f(x4)),'E'('0',f(suc(x4))),iLEQ(suc(x2),suc(x3)) -> 'E'(f(x3),f(suc(x3)))
% 19.67/4.49
% 19.67/4.49 Most General Atoms: 'E'('0',f(x4)) iLEQ(suc(x0),suc(x4)) 'E'(f(x0),f(suc(x0))) 'LE'(f(x0),'0') 'LE'(f(x0),s('0'))
% 19.67/4.49
% 19.67/4.49 === Starting SPASS-SCL-FOL A Little Less Naive, considering 51 atoms initially, heuristics mode: normal ===
% 19.67/4.49
% 19.67/4.49 === Conflict found: 55:23:5:[31.22,15.11]:TopTopTopTopTop: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(x3))),iLEQ(suc(x3),suc(x0)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(x4)))),'E'('0',f(x2)),'E'('0',f(suc(suc(x3)))),iLEQ(suc(x1),suc(x4)),'E'('0',f(x0)),'E'('0',f(x3)),'E'('0',f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1))),'E'(f(x4),f(suc(x4))),'E'('0',f(x4)),'E'('0',f(suc(x4))),'E'(f(x3),f(suc(x3))),iLEQ(suc(x2),suc(x3)) -> {x0 -> z, x1 -> z, x2 -> z, x3 -> z, x4 -> z}
% 19.67/4.49
% 19.67/4.49 SZS status Unsatisfiable
% 19.67/4.49
% 19.67/4.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.67/4.49
% 19.67/4.49 SPASS-SCL-FOL Statistics:
% 19.67/4.49 Number of learned clauses: 0
% 19.67/4.49 Number of propagations: 21
% 19.67/4.49 Number of decisions: 0
% 19.67/4.49 Number of resolutions: 8
% 19.67/4.49 Number of condensations: 0
% 19.67/4.49 Number of sub resolutions: 54
% 19.67/4.49 Number of input literals (deduplicated): 11
% 19.67/4.49 Number of grows: 0
% 19.67/4.49 Number of considered ground atoms: 51
% 19.67/4.49
% 19.67/4.49 Needed: 0:00:03.97
% 19.67/4.49
%------------------------------------------------------------------------------