%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO649-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 : n029.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:14 PM UTC 2026
% Result : Unsatisfiable 0.40s 0.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO649-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 : n029.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:56:30 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.40/0.70 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.70 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.70 Execution normal ended with status: unsatisfiable
% 0.40/0.70 Used heuristic: normal
% 0.40/0.70
% 0.40/0.70 Input Clauses:
% 0.40/0.70
% 0.40/0.70 Predicates: 'E' iLEQ 'LE'
% 0.40/0.70 Fol Constants: '0' z
% 0.40/0.70 Fol Functions: suc f s
% 0.40/0.70 Problem Properties:
% 0.40/0.70 This is a full first-order problem without equality.
% 0.40/0.70
% 0.40/0.70 After reduction: Problem Properties:
% 0.40/0.70 This is a full first-order problem without equality.
% 0.40/0.70
% 0.40/0.70
% 0.40/0.70 Reduced Input Clauses:
% 0.40/0.70 40:18:2:[3.14,1.2,24.12,39.10]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(suc(x1)))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(suc(suc(x1))))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 0.40/0.70 41:10:2:[9.8,2.4]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 0.40/0.70 44:12:2:[8.11,3.2,41.9,42.9,23.7,43.10]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(x1))))
% 0.40/0.70 46:11:2:[23.8,4.1,11.6,45.6]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 0.40/0.70 49:8:1:[35.6,5.2,20.4,47.5,22.2,48.7]:Top: 'E'('0',f(suc(suc(suc(x0))))),'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'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> iLEQ(suc(x0),suc(x0))
% 0.40/0.70 51:11:2:[29.10,8.5,41.9,50.8]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1))))
% 0.40/0.70 52:8:2:[11.5,9.6]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 0.40/0.70 54:15:2:[44.14,10.2,24.12,53.8]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 0.40/0.70 57:15:2:[13.15,12.2,17.13,55.8,54.15,56.14]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'(f(x0),f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 0.40/0.70 61:12:2:[51.11,13.2,41.9,58.9,23.7,59.11,44.13,60.12]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'(f(x1),f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.40/0.70 64:7:1:[35.6,14.2,20.4,62.5,22.2,63.6]:Top: 'E'('0',f(suc(suc(suc(x0))))),'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(suc(x0)))))),iLEQ(suc(x0),suc(x0))
% 0.40/0.70 66:11:2:[41.10,15.1,52.8,65.6]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x0)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.40/0.70 69:11:2:[29.9,17.2,52.7,67.8,11.5,68.10]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(x1)))
% 0.40/0.70 71:16:2:[51.12,19.2,29.10,70.9]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(suc(x1)))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(suc(x1))))))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.40/0.70 72:5:1:[22.2,20.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))
% 0.40/0.70 75:18:2:[61.15,21.2,71.17,73.4,69.13,74.10]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(suc(x1)))))),'E'(f(x1),f(suc(suc(suc(suc(x1)))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'(f(x0),f(suc(x0))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(suc(suc(x1))))))) ->
% 0.40/0.70 76:8:2:[11.6,23.3]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(x1))))
% 0.40/0.70 79:10:2:[29.9,24.2,52.7,77.8,11.5,78.9]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(x1)))
% 0.40/0.70 81:9:2:[76.8,25.1,11.6,80.5]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(x0))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.40/0.70 84:13:2:[41.10,27.1,52.8,82.8,66.12,83.11]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x0)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(suc(suc(x0))))))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.40/0.70 87:14:2:[51.12,28.2,29.10,85.8,46.11,86.13]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(suc(x1)))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 0.40/0.70 89:9:2:[52.7,29.7,11.5,88.8]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(x1)))
% 0.40/0.70 93:10:2:[76.8,30.1,46.12,90.6,11.6,91.7,81.10,92.10]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x0)),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(suc(suc(x0))))))) -> 'E'(f(x1),f(suc(x1)))
% 0.40/0.70 97:11:2:[51.12,31.2,89.10,94.7,66.11,95.10,81.9,96.11]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 0.40/0.70 101:16:2:[61.15,32.2,87.15,98.4,69.13,99.9,46.11,100.15]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(suc(x1)))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 0.40/0.70 102:2:1:[37.0,33.0]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 0.40/0.70 106:15:2:[44.14,34.2,87.15,103.4,79.12,104.9,46.11,105.14]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(x1))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(suc(suc(x1)))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1))))),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'(f(x1),f(suc(suc(suc(suc(x1))))))
% 0.40/0.70 109:5:1:[72.4,35.4,22.2,107.5,97.8,108.7]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.40/0.70 112:12:2:[41.10,36.1,52.8,110.7,66.12,111.10]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(suc(suc(x0)))))),iLEQ(suc(x1),suc(x0)),'E'('0',f(x0)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(suc(x0)))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(suc(suc(x0))))))
% 0.40/0.70
% 0.40/0.70 Most General Atoms: 'E'('0',f(x1)) 'E'(f(x1),f(suc(suc(suc(x1))))) 'E'(f(x0),f(suc(suc(suc(suc(x0)))))) 'E'(f(x1),f(suc(suc(x1)))) 'E'(f(x1),f(suc(x1))) iLEQ(suc(x1),suc(x0)) 'LE'(f(x0),'0') 'LE'(f(x0),s('0'))
% 0.40/0.70
% 0.40/0.70 === Starting SPASS-SCL-FOL A Little Less Naive, considering 58 atoms initially, heuristics mode: normal ===
% 0.40/0.70
% 0.40/0.70 === Conflict found: 69:11:2:[29.9,17.2,52.7,67.8,11.5,68.10]:TopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(suc(suc(x0))))))),'E'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(suc(x0)))))) -> 'E'(f(x1),f(suc(x1))) {x0 -> z, x1 -> z}
% 0.40/0.70 === Backtracking. Learning clause 114:8:1:[109.4,113.1,69.11,75.14,49.8]:Top: 'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'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'(f(x0),f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(suc(suc(x0)))))) ->
% 0.40/0.70 === Conflict found: 64:7:1:[35.6,14.2,20.4,62.5,22.2,63.6]:Top: 'E'('0',f(suc(suc(suc(x0))))),'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(suc(x0)))))),iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 0.40/0.70 === Backtracking. Learning clause 116:7:1:[109.4,115.0,64.7,106.8,114.7]:Top: 'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'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)))))) ->
% 0.40/0.70 === Conflict found: 52:8:2:[11.5,9.6]:TopTop: 'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(x1))),iLEQ(suc(x0),suc(x1)),'E'('0',f(x1)) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))) {x0 -> z, x1 -> z}
% 0.40/0.70
% 0.40/0.70 SZS status Unsatisfiable
% 0.40/0.70
% 0.40/0.70 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/0.70
% 0.40/0.70 SPASS-SCL-FOL Statistics:
% 0.40/0.70 Number of learned clauses: 2
% 0.40/0.70 Number of propagations: 35
% 0.40/0.70 Number of decisions: 10
% 0.40/0.70 Number of resolutions: 19
% 0.40/0.70 Number of condensations: 0
% 0.40/0.70 Number of sub resolutions: 76
% 0.40/0.70 Number of input literals (deduplicated): 20
% 0.40/0.70 Number of grows: 0
% 0.40/0.70 Number of considered ground atoms: 58
% 0.40/0.70
% 0.40/0.70 Needed: 0:00:00.14
% 0.40/0.70
%------------------------------------------------------------------------------