%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO681-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 : n014.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:17 PM UTC 2026
% Result : Unsatisfiable 1.09s 0.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO681-1 : TPTP v9.2.1. Released v7.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.32 % Computer : n014.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Thu May 7 13:56:22 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.32 SPASS-SCL-FOL version:
% 0.20/0.41 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.09/0.70 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.09/0.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.09/0.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.09/0.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.09/0.70 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.09/0.70 Execution resolution_2 ended with status: unsatisfiable
% 1.09/0.70 Used heuristic: resolution_2
% 1.09/0.70
% 1.09/0.70 Input Clauses:
% 1.09/0.70
% 1.09/0.70 Predicates: 'LE' 'E' iLEQ
% 1.09/0.70 Fol Constants: '0' z
% 1.09/0.70 Fol Functions: f s suc
% 1.09/0.70 Problem Properties:
% 1.09/0.70 This is a full first-order problem without equality.
% 1.09/0.70
% 1.09/0.70 After reduction: Problem Properties:
% 1.09/0.70 This is a full first-order problem without equality.
% 1.09/0.70
% 1.09/0.70
% 1.09/0.70 Reduced Input Clauses:
% 1.09/0.70 55:2:1:[3.0,1.0]:Top: -> 'E'(s(s(s('0'))),f(x0)),'LE'(f(x0),s(s(s('0'))))
% 1.09/0.70 56:11:3:[15.9,2.5]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x2)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 1.09/0.70 57:11:3:[14.9,4.3]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),iLEQ(suc(x2),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 1.09/0.70 58:11:3:[15.10,5.2]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 1.09/0.70 59:11:3:[14.8,6.6]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),iLEQ(suc(x2),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 1.09/0.70 60:4:1:[46.2,8.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 1.09/0.70 61:12:3:[39.10,11.2]:TopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),'E'('0',f(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'('0',f(x2)) -> 'E'(f(x1),f(suc(x1)))
% 1.09/0.70 62:11:3:[19.9,12.8]:TopTopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 1.09/0.70 63:12:3:[39.11,13.4]:TopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(x1))),'E'('0',f(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'('0',f(x2)) -> 'E'(f(x2),f(suc(x2)))
% 1.09/0.70 64:13:3:[44.12,16.1]:TopTopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))) ->
% 1.09/0.70 65:12:3:[59.11,20.6]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),iLEQ(suc(x2),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(f(x2),f(suc(x2))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))) -> 'E'(f(x0),f(suc(x0)))
% 1.09/0.70 66:11:3:[15.8,21.4]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 1.09/0.70 67:12:3:[62.11,23.1]:TopTopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'(s(s('0')),f(x1)),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x2)) -> 'E'(f(x2),f(suc(x2)))
% 1.09/0.70 68:4:1:[29.2,24.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))
% 1.09/0.70 69:4:1:[26.2,27.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0))
% 1.09/0.70 70:11:3:[9.10,30.4]:TopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(x1))),'E'('0',f(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 1.09/0.70 71:11:3:[19.10,31.1]:TopTopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 1.09/0.70 73:11:3:[47.11,33.3,57.11,72.7]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),iLEQ(suc(x2),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))) -> 'E'(f(x2),f(suc(x2)))
% 1.09/0.70 75:11:3:[48.11,35.1,71.10,74.11]:TopTopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(x2)) -> 'E'(f(x0),f(suc(x0)))
% 1.09/0.70 76:4:1:[32.2,36.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)) -> iLEQ(suc(x0),suc(x0))
% 1.09/0.70 77:12:3:[70.10,37.2]:TopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),'E'(f(x1),f(suc(x1))),'E'('0',f(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(x2)) -> 'E'(f(x0),f(suc(x0)))
% 1.09/0.70 79:12:3:[65.12,38.3,73.12,78.9]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),iLEQ(suc(x2),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(f(x1),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))) ->
% 1.09/0.70 80:11:3:[9.9,39.8]:TopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(x1))),'E'('0',f(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x0)))),'E'('0',f(x2)) -> 'E'(f(x2),f(suc(x2))),'E'(f(x1),f(suc(x1)))
% 1.09/0.70 81:13:3:[53.12,40.2]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(x2)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x0)) ->
% 1.09/0.70 82:11:3:[9.8,41.2]:TopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),'E'('0',f(x0)),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 1.09/0.70 84:11:3:[48.10,44.9,62.10,83.11]:TopTopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(x2)) -> 'E'(f(x1),f(suc(x1)))
% 1.09/0.70 86:11:3:[59.10,45.3,57.10,85.8]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),iLEQ(suc(x2),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))) -> 'E'(f(x1),f(suc(x1)))
% 1.09/0.70 87:11:3:[14.10,47.5]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),iLEQ(suc(x2),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(suc(x1)))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))) -> 'E'(f(x2),f(suc(x2))),'E'(f(x0),f(suc(x0)))
% 1.09/0.70 88:11:3:[19.8,48.9]:TopTopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(s(s('0')),f(x2)) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 1.09/0.70 90:12:3:[63.12,49.2,61.12,89.6]:TopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'('0',f(x2)) ->
% 1.09/0.70 92:11:3:[66.11,50.2,58.10,91.5]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(x2)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x0)) -> 'E'(f(x0),f(suc(x0)))
% 1.09/0.70 94:11:3:[66.10,53.5,56.10,93.6]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x2)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x0)) -> 'E'(f(x1),f(suc(x1)))
% 1.09/0.70 96:11:3:[56.11,54.2,58.11,95.6]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(x2)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) -> 'E'(f(x2),f(suc(x2)))
% 1.09/0.70
% 1.09/0.70 Most General Atoms: 'LE'(f(x0),s(s(s('0')))) iLEQ(suc(x2),suc(x0)) 'E'(s('0'),f(x0)) 'LE'(f(x0),s(s(s(s('0'))))) 'E'(s(s(s('0'))),f(x2)) 'E'(f(x0),f(suc(x0))) 'LE'(f(x0),s(s('0'))) 'E'('0',f(x2)) 'E'(s(s('0')),f(x2)) 'LE'(f(x0),s('0')) 'LE'(f(x0),'0')
% 1.09/0.70
% 1.09/0.70 === Starting SPASS-SCL-FOL A Little Less Naive, considering 57 atoms initially, heuristics mode: resolution_2 ===
% 1.09/0.70
% 1.09/0.70 === Clause set with instances from active satisfied. Growing active. New size: 57
% 1.09/0.70 === Restarting.
% 1.09/0.70 === Backtracking. Learning clause 97:2:1:[43.1,3.1]:Top: -> 'E'(s(s(s('0'))),f(suc(x0))),'LE'(f(x0),s(s(s('0'))))
% 1.09/0.70 === Conflict found: 59:11:3:[14.8,6.6]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s(s(s('0'))),f(x1)),'E'(s(s(s('0'))),f(x0)),iLEQ(suc(x2),suc(x0)),'E'(s(s(s('0'))),f(x2)),'E'(s(s(s('0'))),f(suc(suc(x2)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(suc(x1))),'E'(s(s(s('0'))),f(suc(x2))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))) {x0 -> z, x1 -> z, x2 -> z}
% 1.09/0.70 === Backtracking. Learning clause 100:1:1:[97.0,98.0,3.0,99.1,59.10,79.8,76.4,28.2,55.1]:Top: -> 'LE'(f(x0),s(s(s('0'))))
% 1.09/0.70 === Clause set with instances from active satisfied. Growing active. New size: 57
% 1.09/0.70 === Restarting.
% 1.09/0.70 === Backtracking. Learning clause 101:2:0:[51.3,17.1]:: 'LE'(f(suc(z)),s('0')) -> 'E'('0',f(suc(z)))
% 1.09/0.70 === Backtracking. Learning clause 102:2:0:[25.3,17.1]:: 'LE'(f(suc(suc(z))),s('0')) -> 'E'('0',f(suc(suc(z))))
% 1.09/0.70 === Backtracking. Learning clause 103:2:0:[18.3,17.1]:: 'LE'(f(z),s('0')) -> 'E'('0',f(z))
% 1.09/0.70 === Clause set with instances from active satisfied. Growing active. New size: 57
% 1.09/0.70 === Restarting.
% 1.09/0.70 === Backtracking. Learning clause 104:2:1:[7.1,100.1]:Top: -> 'E'(s(s('0')),f(x0)),'LE'(f(x0),s(s('0')))
% 1.09/0.70 === Conflict found: 90:12:3:[63.12,49.2,61.12,89.6]:TopTopTop: 'E'('0',f(suc(x0))),iLEQ(suc(x0),suc(x1)),iLEQ(suc(x2),suc(x0)),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x2)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x1)))),'E'('0',f(suc(x2))),'E'('0',f(x1)),'E'('0',f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'('0',f(x2)) -> {x0 -> z, x1 -> z, x2 -> z}
% 1.09/0.70 === Backtracking. Learning clause 105:3:1:[90.11,82.10,69.4]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) ->
% 1.09/0.70 === Backtracking. Learning clause 106:3:1:[15.1,29.4]:Top: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 1.09/0.70 === Clause set with instances from active satisfied. Growing active. New size: 62
% 1.09/0.70 === Restarting.
% 1.09/0.70 === Backtracking. Learning clause 108:4:1:[100.0,107.0,42.1,104.2,106.2,42.2,34.3]:Top: -> 'LE'(f(suc(x0)),s('0')),'E'(f(x0),f(suc(x0))),'LE'(f(x0),s('0')),'E'(s(s('0')),f(suc(x0)))
% 1.09/0.70 === Conflict found: 60:4:1:[46.2,8.2]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> '0'}
% 1.09/0.70 === Backtracking. Learning clause 110:2:1:[100.0,109.0,60.2,34.2,10.2,104.1,100.1]:Top: -> iLEQ(suc(x0),suc(x0)),'LE'(f(x0),s(s('0')))
% 1.09/0.70 === Clause set with instances from active satisfied. Growing active. New size: 126
% 1.09/0.70 === Backtracking. Learning clause 111:3:1:[14.1,32.4]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(x0))) -> 'E'(f(x0),f(suc(x0)))
% 1.09/0.70 === Conflict found: 64:13:3:[44.12,16.1]:TopTopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))) -> {x0 -> '0', x1 -> '0', x2 -> '0'}
% 1.09/0.70 === Backtracking. Learning clause 114:2:1:[100.0,112.1,100.0,113.2,64.11,19.9,110.1,7.2,10.2]:Top: 'E'(s(s('0')),f(suc(x0))) -> 'LE'(f(x0),s(s('0')))
% 1.09/0.70 === Clause set with instances from active satisfied. Growing active. New size: 128
% 1.09/0.70 === Restarting.
% 1.09/0.70 === Backtracking. Learning clause 115:3:0:[52.3,101.1]:: 'LE'(f(suc(suc(suc(z)))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(suc(z))))),'E'('0',f(suc(z)))
% 1.09/0.70 === Backtracking. Learning clause 116:3:0:[42.3,101.1]:: 'LE'(f(suc(z)),s(s('0'))) -> 'E'(s('0'),f(suc(z))),'E'('0',f(suc(z)))
% 1.09/0.70 === Backtracking. Learning clause 117:3:0:[22.3,101.1]:: 'LE'(f(suc(suc(z))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(z)))),'E'('0',f(suc(z)))
% 1.09/0.70 === Backtracking. Learning clause 118:1:1:[34.1,100.1,114.1]:Top: -> 'LE'(f(x0),s(s('0')))
% 1.09/0.70 === Conflict found: 64:13:3:[44.12,16.1]:TopTopTop: 'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)),iLEQ(suc(x0),suc(x1)),'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(suc(x1)))),'E'(s(s('0')),f(suc(x2))),'E'(s(s('0')),f(suc(x1))),iLEQ(suc(x2),suc(x0)),'E'(s(s('0')),f(x1)),'E'(s(s('0')),f(suc(suc(x2)))),'E'(f(x0),f(suc(x0))),'E'(s(s('0')),f(x2)),'E'(f(x2),f(suc(x2))) -> {x0 -> '0', x1 -> '0', x2 -> '0'}
% 1.09/0.70 === Backtracking. Learning clause 119:3:1:[64.11,84.11,60.4]:Top: 'E'(s(s('0')),f(suc(suc(x0)))),'E'(s(s('0')),f(suc(x0))),'E'(s(s('0')),f(x0)) ->
% 1.09/0.70 === Conflict found: 76:4:1:[32.2,36.2]:Top: 'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))),'E'(s(s(s('0'))),f(x0)) -> iLEQ(suc(x0),suc(x0)) {x0 -> suc(suc('0'))}
% 1.09/0.70 === Backtracking. Learning clause 121:3:1:[111.2,120.1,76.4,79.1]:Top: 'E'(s(s(s('0'))),f(x0)),'E'(s(s(s('0'))),f(suc(suc(x0)))),'E'(s(s(s('0'))),f(suc(x0))) ->
% 1.09/0.70 === Clause set with instances from active satisfied. Growing active. New size: 129
% 1.09/0.70 === Restarting.
% 1.09/0.70 === Backtracking. Learning clause 122:2:1:[42.1,118.1]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0'))
% 1.09/0.70 === Backtracking. Learning clause 123:2:1:[52.1,118.1]:Top: -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0'))
% 1.09/0.70 === Backtracking. Learning clause 124:6:1:[18.1,22.3,105.3,25.2,22.3]:Top: 'LE'(f(suc(x0)),s(s('0'))),'E'('0',f(suc(x0))),'LE'(f(suc(suc(suc(x0)))),s(s('0'))) -> 'E'(s('0'),f(suc(x0))),'LE'(f(x0),'0'),'E'(s('0'),f(suc(suc(suc(x0)))))
% 1.09/0.70 === Conflict found: 81:13:3:[53.12,40.2]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(x2)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x0)) -> {x0 -> z, x1 -> z, x2 -> z}
% 1.09/0.70 === Backtracking. Learning clause 125:1:0:[81.1,68.4,106.3,122.1,123.1,18.1,105.3,25.2,22.3,124.4,118.1,101.2,17.1,118.1,123.2]:: -> 'E'(s('0'),f(suc(suc(suc(z)))))
% 1.09/0.70 === Conflict found: 81:13:3:[53.12,40.2]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(x2)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x0)) -> {x0 -> z, x1 -> z, x2 -> z}
% 1.09/0.70 === Backtracking. Learning clause 126:3:1:[81.6,106.3,68.4,122.1,123.1,18.1]:Top: 'E'(s('0'),f(suc(x0))) -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 1.09/0.70 === Conflict found: 117:3:0:[22.3,101.1]:: 'LE'(f(suc(suc(z))),s(s('0'))) -> 'E'(s('0'),f(suc(suc(z)))),'E'('0',f(suc(z))) {}
% 1.09/0.70 === Backtracking. Learning clause 128:2:0:[17.0,127.1,117.1,118.1,105.2,25.2,122.2]:: 'E'('0',f(z)) -> 'E'(s('0'),f(suc(suc(z))))
% 1.09/0.70 === Clause set with instances from active satisfied. Growing active. New size: 135
% 1.09/0.70 === Restarting.
% 1.09/0.70 === Conflict found: 126:3:1:[81.6,106.3,68.4,122.1,123.1,18.1]:Top: 'E'(s('0'),f(suc(x0))) -> 'E'('0',f(x0)),'LE'(f(x0),'0') {x0 -> suc(suc(z))}
% 1.09/0.70 === Backtracking. Learning clause 129:2:0:[126.1,125.1]:: -> 'E'('0',f(suc(suc(z)))),'LE'(f(suc(suc(z))),'0')
% 1.09/0.70 === Conflict found: 106:3:1:[15.1,29.4]:Top: 'E'(s('0'),f(x0)),'E'(s('0'),f(suc(x0))) -> 'E'(f(x0),f(suc(x0))) {x0 -> suc(suc(suc(z)))}
% 1.09/0.70 === Backtracking. Learning clause 130:2:0:[106.1,125.1]:: 'E'(s('0'),f(suc(suc(suc(suc(z)))))) -> 'E'(f(suc(suc(suc(z)))),f(suc(suc(suc(suc(z))))))
% 1.09/0.70 === Conflict found: 81:13:3:[53.12,40.2]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'(s('0'),f(suc(x2))),iLEQ(suc(x2),suc(x0)),'E'(s('0'),f(suc(x1))),'E'(s('0'),f(suc(suc(x0)))),'E'(f(x0),f(suc(x0))),'E'(f(x2),f(suc(x2))),'E'(s('0'),f(x2)),'E'(s('0'),f(x1)),'E'(s('0'),f(suc(suc(x1)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(suc(suc(x2)))),'E'(s('0'),f(x0)) -> {x0 -> z, x1 -> z, x2 -> z}
% 1.09/0.70 === Backtracking. Learning clause 131:3:1:[81.6,106.3,68.4]:Top: 'E'(s('0'),f(suc(suc(x0)))),'E'(s('0'),f(suc(x0))),'E'(s('0'),f(x0)) ->
% 1.09/0.70 === Conflict found: 103:2:0:[18.3,17.1]:: 'LE'(f(z),s('0')) -> 'E'('0',f(z)) {}
% 1.09/0.70 === Backtracking. Learning clause 132:1:0:[103.1,123.2,128.1,131.3,125.1]:: 'E'(s('0'),f(suc(suc(suc(suc(z)))))) ->
% 1.09/0.70 === Conflict found: 123:2:1:[52.1,118.1]:Top: -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0')) {x0 -> suc(suc(z))}
% 1.09/0.70 === Backtracking. Learning clause 133:2:0:[123.1,132.1,102.1,105.1,101.2]:: 'E'('0',f(z)),'LE'(f(suc(z)),s('0')) ->
% 1.09/0.70 === Conflict found: 123:2:1:[52.1,118.1]:Top: -> 'E'(s('0'),f(suc(suc(x0)))),'LE'(f(x0),s('0')) {x0 -> suc(suc(z))}
% 1.09/0.70 === Backtracking. Learning clause 134:1:0:[123.1,132.1,102.1]:: -> 'E'('0',f(suc(suc(z))))
% 1.09/0.70 === Conflict found: 122:2:1:[42.1,118.1]:Top: -> 'E'(s('0'),f(x0)),'LE'(f(x0),s('0')) {x0 -> suc(z)}
% 1.09/0.70 === Backtracking. Learning clause 136:1:0:[125.0,135.0,122.2,133.2,131.3,128.2]:: 'E'('0',f(z)) ->
% 1.09/0.70 === Backtracking. Learning clause 139:1:0:[125.0,137.0,136.0,138.2,22.1,118.1,103.1,131.3]:: 'E'(s('0'),f(suc(suc(z)))) ->
% 1.09/0.70 === Conflict found: 103:2:0:[18.3,17.1]:: 'LE'(f(z),s('0')) -> 'E'('0',f(z)) {}
% 1.09/0.70
% 1.09/0.70 SZS status Unsatisfiable
% 1.09/0.70
% 1.09/0.70 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.09/0.70
% 1.09/0.70 SPASS-SCL-FOL Statistics:
% 1.09/0.70 Number of learned clauses: 32
% 1.09/0.70 Number of propagations: 575
% 1.09/0.70 Number of decisions: 488
% 1.09/0.70 Number of resolutions: 85
% 1.09/0.70 Number of condensations: 0
% 1.09/0.70 Number of sub resolutions: 53
% 1.09/0.70 Number of input literals (deduplicated): 29
% 1.09/0.70 Number of grows: 8
% 1.09/0.70 Number of considered ground atoms: 135
% 1.09/0.70
% 1.09/0.70 Needed: 0:00:00.17
% 1.09/0.70
%------------------------------------------------------------------------------