%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO659-1 : TPTP v9.2.1. Released v7.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n022.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 0.61s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO659-1 : TPTP v9.2.1. Released v7.3.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n022.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:22 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.61/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.62 Execution lmodel_grow ended with status: unsatisfiable
% 0.61/0.62 Used heuristic: lmodel_grow
% 0.61/0.62
% 0.61/0.62 Input Clauses:
% 0.61/0.62
% 0.61/0.62 Predicates: iLEQ 'E' 'LE'
% 0.61/0.62 Fol Constants: '0' z
% 0.61/0.62 Fol Functions: suc s f
% 0.61/0.62 Problem Properties:
% 0.61/0.62 This is a full first-order problem without equality.
% 0.61/0.62
% 0.61/0.62 After reduction: Problem Properties:
% 0.61/0.62 This is a full first-order problem without equality.
% 0.61/0.62
% 0.61/0.62
% 0.61/0.62 Reduced Input Clauses:
% 0.61/0.62 55:13:2:[15.13,1.4,32.11,53.10,52.9,54.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'(f(x1),f(suc(x1))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x1),f(suc(suc(suc(x1)))))
% 0.61/0.62 56:8:2:[33.5,5.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)))
% 0.61/0.62 59:9:2:[22.10,6.6,48.8,57.8,33.6,58.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)))
% 0.61/0.62 60:5:1:[41.2,7.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.61/0.62 62:6:1:[23.4,8.3,2.2,61.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))
% 0.61/0.62 63:11:2:[13.6,9.8]: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(suc(x1))))),'E'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(x0)))
% 0.61/0.62 64:2:1:[24.0,10.0]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 0.61/0.62 66:9:2:[56.7,11.2,33.5,65.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)))
% 0.61/0.62 68:11:2:[34.9,14.7,46.7,67.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))))
% 0.61/0.62 71:12:2:[32.11,15.8,52.9,69.10,68.12,70.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(x1))))),'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(suc(x1)))))
% 0.61/0.62 75:10:2:[29.12,16.7,36.10,72.9,59.11,73.10,56.8,74.11]: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'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.61/0.62 78:13:2:[75.13,17.3,59.11,76.12,66.10,77.13]: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'(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'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.61/0.62 80:7:1:[60.4,18.2,41.2,79.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))))) -> iLEQ(suc(x0),suc(x0))
% 0.61/0.62 82:9:2:[48.8,22.6,33.6,81.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)))))
% 0.61/0.62 83:5:1:[2.2,23.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 0.61/0.62 86:9:2:[31.9,25.3,30.7,84.8,13.5,85.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(x1),f(suc(x1)))
% 0.61/0.62 89:6:1:[62.6,26.2,83.4,87.5,2.2,88.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))))) -> iLEQ(suc(x0),suc(x0))
% 0.61/0.62 91:14:2:[29.11,27.3,82.9,90.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(x1),f(suc(suc(suc(x1)))))
% 0.61/0.62 94:11:2:[68.11,28.4,34.9,92.9,86.11,93.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(suc(x0)))))),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x1)),'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x0))))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.61/0.62 97:10:2:[36.10,29.7,82.9,95.8,56.8,96.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'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 0.61/0.62 98:8:2:[13.5,30.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)))
% 0.61/0.62 100:9:2:[98.7,31.6,13.5,99.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)))
% 0.61/0.62 101:12:2:[98.8,32.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(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)))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 0.61/0.62 102:10:2:[98.8,34.7]: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(x0))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1))))
% 0.61/0.62 105:14:2:[75.13,35.3,78.15,103.8,59.11,104.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))) ->
% 0.61/0.62 107:9:2:[48.7,36.6,56.8,106.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))))
% 0.61/0.62 110:12:2:[97.11,37.3,82.9,108.10,66.10,109.11]: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'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 0.61/0.62 114:13:2:[49.15,40.5,45.13,111.11,86.11,112.12,63.11,113.13]: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'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) ->
% 0.61/0.62 116:6:1:[60.4,43.2,41.2,115.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))
% 0.61/0.62 119:10:2:[107.9,44.3,48.7,117.8,66.10,118.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(x0))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1))))
% 0.61/0.62 121:12:2:[98.8,45.9,63.11,120.10]: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'(f(x1),f(suc(suc(x1)))) -> 'E'(f(x0),f(suc(suc(x0))))
% 0.61/0.62 122:8:2:[13.6,46.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))))
% 0.61/0.62 125:9:2:[56.7,47.2,66.9,123.6,33.5,124.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'('0',f(suc(suc(suc(x0))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1)))
% 0.61/0.62 126:8:2:[33.6,48.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))))
% 0.61/0.62 129:13:2:[121.13,49.9,100.10,127.10,63.11,128.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)))))
% 0.61/0.62 133:10:2:[107.9,50.3,119.11,130.7,126.7,131.10,125.11,132.11]: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(x0))))),'E'('0',f(x1)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.61/0.62 135:9:2:[13.6,52.7,122.8,134.8]: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(x0),f(suc(x0))),'E'(f(x1),f(suc(suc(suc(x1)))))
% 0.61/0.62
% 0.61/0.62 Most General Atoms: iLEQ(suc(x0),suc(x1)) 'E'(s('0'),f(x1)) 'E'(f(x0),f(suc(x0))) 'LE'(f(x0),'0') 'LE'(f(x0),s('0')) 'E'('0',f(x1)) 'E'(f(x0),f(suc(suc(x0)))) 'E'(f(x0),f(suc(suc(suc(x0))))) 'LE'(f(x0),s(s('0')))
% 0.61/0.62
% 0.61/0.62 === Starting SPASS-SCL-FOL A Little Less Naive, considering 53 atoms initially, heuristics mode: lmodel_grow ===
% 0.61/0.62
% 0.61/0.62 === Conflict found: 114:13:2:[49.15,40.5,45.13,111.11,86.11,112.12,63.11,113.13]: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'(f(x1),f(suc(suc(suc(x1))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(x1)))) -> {x0 -> z, x1 -> z}
% 0.61/0.62 === Backtracking. Learning clause 136:6:1:[114.11,71.11,102.9,13.6,42.2,64.1]:Top: 'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.61/0.62 === Clause set with instances from active satisfied. Growing active. New size: 65
% 0.61/0.62 === Clause set with instances from active satisfied. Growing active. New size: 77
% 0.61/0.62 === Conflict found: 89:6:1:[62.6,26.2,83.4,87.5,2.2,88.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))))) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(suc(z))}
% 0.61/0.62 === Backtracking. Learning clause 140:4:1:[64.0,137.0,42.1,138.1,24.0,139.3,89.6,136.4,38.2,4.2,24.1,24.1,3.1]:Top: 'E'(s('0'),f(suc(suc(suc(suc(x0)))))) -> 'LE'(f(suc(suc(x0))),s('0')),'E'('0',f(suc(suc(suc(x0))))),'LE'(f(x0),'0')
% 0.61/0.62 === Conflict found: 89:6:1:[62.6,26.2,83.4,87.5,2.2,88.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))))) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(suc(z))}
% 0.61/0.62 === Backtracking. Learning clause 141:4:1:[89.6,136.4,12.2,24.1,38.2,24.1,4.2,42.2,64.1,51.1]:Top: 'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'E'('0',f(suc(suc(x0)))),'LE'(f(x0),'0')
% 0.61/0.62 === Conflict found: 110:12:2:[97.11,37.3,82.9,108.10,66.10,109.11]: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'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(suc(x0))))),'E'(f(x1),f(suc(suc(suc(x1))))) {x0 -> z, x1 -> z}
% 0.61/0.62 === Backtracking. Learning clause 142:6:1:[110.9,75.10,116.6]:Top: 'E'('0',f(suc(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(x0))))) -> 'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.61/0.62 === Conflict found: 105:14:2:[75.13,35.3,78.15,103.8,59.11,104.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))) -> {x0 -> z, x1 -> z}
% 0.61/0.62 === Backtracking. Learning clause 143:7:1:[105.13,59.9,75.10,80.7,142.6,20.2,38.3]:Top: 'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(x0)))))
% 0.61/0.62 === Conflict found: 62:6:1:[23.4,8.3,2.2,61.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)) {x0 -> z}
% 0.61/0.62 === Backtracking. Learning clause 144:10:1:[62.3,42.2,64.1,136.4,12.2,4.2,20.1,142.4]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))) -> 'LE'(f(x0),'0'),'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.61/0.62 === Conflict found: 136:6:1:[114.11,71.11,102.9,13.6,42.2,64.1]:Top: 'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'(s('0'),f(suc(suc(suc(x0))))),'E'(s('0'),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> z}
% 0.61/0.62 === Backtracking. Learning clause 145:6:1:[136.1,12.2,4.2]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0)),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.61/0.62 === Conflict found: 105:14:2:[75.13,35.3,78.15,103.8,59.11,104.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))) -> {x0 -> z, x1 -> z}
% 0.61/0.62 === Backtracking. Learning clause 150:7:1:[144.9,146.0,24.0,147.7,24.0,148.8,24.0,149.9,105.13,33.6,75.10,20.2,145.6]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(x0))),'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0)) -> 'LE'(f(x0),'0')
% 0.61/0.62 === Conflict found: 83:5:1:[2.2,23.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 0.61/0.62 === Backtracking. Learning clause 151:5:1:[83.3,64.1,42.2]:Top: 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(suc(x0)),s(s('0'))) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s('0'))
% 0.61/0.62 === Conflict found: 89:6:1:[62.6,26.2,83.4,87.5,2.2,88.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))))) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 0.61/0.62 === Backtracking. Learning clause 153:5:1:[145.1,152.4,89.3,42.2,64.1,4.2,12.2]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.61/0.62 === Conflict found: 80:7:1:[60.4,18.2,41.2,79.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))))) -> iLEQ(suc(x0),suc(x0)) {x0 -> z}
% 0.61/0.62 === Backtracking. Learning clause 157:5:1:[141.2,154.3,24.0,155.4,24.0,156.5,80.5,144.10,20.2,150.6,153.5,143.7,39.2,42.3,19.2,12.3,3.2,4.3]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(suc(suc(x0)))))))
% 0.61/0.62 === Backtracking. Learning clause 158:5:1:[38.2,153.1]:Top: 'LE'(f(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(suc(x0))))),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.61/0.62 === Backtracking. Learning clause 159:8:1:[51.1,64.2,97.2,19.2,12.3,3.2,4.3]:Top: iLEQ(suc(x0),suc(x0)),'E'('0',f(x0)),'LE'(f(suc(suc(suc(suc(suc(x0)))))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(x0)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x0),f(suc(suc(suc(x0))))),'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(suc(suc(x0)))))))
% 0.61/0.62 === Conflict found: 158:5:1:[38.2,153.1]:Top: 'LE'(f(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(suc(x0))))),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> suc(z)}
% 0.61/0.62 === Backtracking. Learning clause 160:9:1:[158.2,24.1,24.1,19.1,107.1,51.2,64.2,24.1,71.2,13.6]:Top: 'LE'(f(suc(suc(suc(x0)))),s(s('0'))),'E'('0',f(x0)),'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),'0'),'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.61/0.62 === Backtracking. Learning clause 162:5:1:[64.0,161.3,4.1,24.1,71.2,13.6]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x0)),'E'(s('0'),f(suc(x0))) -> 'LE'(f(x0),s('0')),'E'(f(x0),f(suc(suc(suc(x0)))))
% 0.61/0.62 === Backtracking. Learning clause 163:3:1:[4.1,24.1,51.1]:Top: -> 'E'(s('0'),f(suc(suc(suc(suc(x0)))))),'E'('0',f(suc(suc(x0)))),'LE'(f(x0),'0')
% 0.61/0.62 === Conflict found: 153:5:1:[145.1,152.4,89.3,42.2,64.1,4.2,12.2]:Top: 'E'(s('0'),f(suc(suc(suc(x0))))),'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> z}
% 0.61/0.62 === Backtracking. Learning clause 164:3:1:[153.4,24.1,24.1,38.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),s('0'))
% 0.61/0.62 === Backtracking. Learning clause 165:2:0:[3.3,21.1]:: 'LE'(f(suc(suc(suc(z)))),s('0')) -> 'E'('0',f(suc(suc(suc(z)))))
% 0.61/0.62 === Backtracking. Learning clause 166:2:0:[51.3,21.1]:: 'LE'(f(suc(suc(z))),s('0')) -> 'E'('0',f(suc(suc(z))))
% 0.61/0.62 === Conflict found: 157:5:1:[141.2,154.3,24.0,155.4,24.0,156.5,80.5,144.10,20.2,150.6,153.5,143.7,39.2,42.3,19.2,12.3,3.2,4.3]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(suc(suc(x0))))))) {x0 -> z}
% 0.61/0.62 === Backtracking. Learning clause 167:4:1:[157.1,24.1]:Top: 'LE'(f(suc(suc(x0))),s(s('0'))),'LE'(f(suc(suc(suc(suc(x0))))),s(s('0'))) -> 'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(suc(suc(x0)))))))
% 0.61/0.62 === Conflict found: 102:10:2:[98.8,34.7]: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(x0))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(suc(x1)))) {x0 -> z, x1 -> z}
% 0.61/0.62 === Backtracking. Learning clause 169:4:1:[64.0,168.0,102.5,42.2,151.4,24.1]:Top: 'E'(f(x0),f(suc(x0))),'E'(s('0'),f(suc(suc(x0)))) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 0.61/0.62 === Conflict found: 164:3:1:[153.4,24.1,24.1,38.2]:Top: 'LE'(f(suc(x0)),s(s('0'))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'LE'(f(x0),s('0')) {x0 -> z}
% 0.61/0.62 === Backtracking. Learning clause 170:1:1:[164.2,24.1,24.1]:Top: -> 'LE'(f(x0),s('0'))
% 0.61/0.62 === Conflict found: 107:9:2:[48.7,36.6,56.8,106.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}
% 0.61/0.62 === Backtracking. Learning clause 172:5:1:[170.0,171.3,107.4,20.2]:Top: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0)),'E'('0',f(suc(x0))) -> 'E'(f(x0),f(suc(suc(x0)))),'LE'(f(x0),'0')
% 0.61/0.62 === Conflict found: 60:5:1:[41.2,7.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}
% 0.61/0.62 === Backtracking. Learning clause 173:3:0:[60.3,20.2,172.2,19.2,21.1,170.1]:: 'LE'(f(z),s('0')),'E'('0',f(suc(suc(z)))) -> 'E'(f(z),f(suc(suc(z))))
% 0.61/0.62 === Backtracking. Learning clause 176:2:0:[173.2,174.1,170.0,175.3,39.1,170.1,105.6,110.11,3.2,170.1,33.6,19.2,20.2,21.1,170.1]:: 'E'('0',f(suc(suc(z)))),iLEQ(suc(z),suc(z)) ->
% 0.61/0.62
% 0.61/0.62 SZS status Unsatisfiable
% 0.61/0.62
% 0.61/0.62 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.62
% 0.61/0.62 SPASS-SCL-FOL Statistics:
% 0.61/0.62 Number of learned clauses: 25
% 0.61/0.62 Number of propagations: 246
% 0.61/0.62 Number of decisions: 104
% 0.61/0.62 Number of resolutions: 119
% 0.61/0.62 Number of condensations: 0
% 0.61/0.62 Number of sub resolutions: 99
% 0.61/0.62 Number of input literals (deduplicated): 27
% 0.61/0.62 Number of grows: 2
% 0.61/0.62 Number of considered ground atoms: 77
% 0.61/0.62
% 0.61/0.62 Needed: 0:00:00.10
% 0.61/0.62
%------------------------------------------------------------------------------