%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWX040+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:32:36 PM UTC 2026
% Result : Theorem 68.28s 17.75s
% Output : CNFRefutation 68.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 12
% Syntax : Number of formulae : 282 ( 80 unt; 1 def)
% Number of atoms : 785 ( 386 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 762 ( 271 ~; 396 |; 76 &)
% ( 2 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-2 aty)
% Number of variables : 360 ( 0 sgn 312 !; 48 ?; 167 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : '0' != s(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id1) ).
fof(f2,axiom,
! [X0,X1] :
( s(X0) = s(X1)
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id2) ).
fof(f24,axiom,
! [X0,X1] :
( '@<_succeeds'(X0,X1)
<=> ( ? [X4] :
( X1 = s(X4)
& X0 = '0' )
| ? [X2,X3] :
( '@<_succeeds'(X2,X3)
& X1 = s(X3)
& X0 = s(X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id24) ).
fof(f27,axiom,
! [X0] :
( nat_succeeds(X0)
<=> ( X0 = '0'
| ? [X1] :
( nat_succeeds(X1)
& X0 = s(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id27) ).
fof(f73,axiom,
! [X0,X1] :
( '@<_succeeds'(X0,X1)
=> nat_succeeds(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(less:types)') ).
fof(f74,axiom,
! [X0,X1] :
( '@<_succeeds'(X0,X1)
=> ? [X2] : X1 = s(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(less:successor)') ).
fof(f75,axiom,
( ! [X0,X1] :
( ( ? [X5] :
( X1 = s(X5)
& X0 = '0' )
| ? [X2,X3] :
( ! [X4] :
( '@<_succeeds'(X3,s(X4))
=> '@<_succeeds'(X2,X4) )
& '@<_succeeds'(X2,X3)
& X1 = s(X3)
& X0 = s(X2) ) )
=> ! [X4] :
( '@<_succeeds'(X1,s(X4))
=> '@<_succeeds'(X0,X4) ) )
=> ! [X0,X1] :
( '@<_succeeds'(X0,X1)
=> ! [X4] :
( '@<_succeeds'(X1,s(X4))
=> '@<_succeeds'(X0,X4) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',induction) ).
fof(f76,conjecture,
! [X0,X1,X2] :
( ( '@<_succeeds'(X1,s(X2))
& '@<_succeeds'(X0,X1) )
=> '@<_succeeds'(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(less:transitive:successor)') ).
fof(f77,negated_conjecture,
~ ! [X0,X1,X2] :
( ( '@<_succeeds'(X1,s(X2))
& '@<_succeeds'(X0,X1) )
=> '@<_succeeds'(X0,X2) ),
inference(negated_conjecture,[status(cth)],[f76]) ).
fof(f78,plain,
( ! [X0,X1] :
( ( ? [X5] :
( X1 = s(X5)
& X0 = '0' )
| ? [X2,X3] :
( ! [X4] :
( '@<_succeeds'(X3,s(X4))
=> '@<_succeeds'(X2,X4) )
& '@<_succeeds'(X2,X3)
& X1 = s(X3)
& X0 = s(X2) ) )
=> ! [X6] :
( '@<_succeeds'(X1,s(X6))
=> '@<_succeeds'(X0,X6) ) )
=> ! [X7,X8] :
( '@<_succeeds'(X7,X8)
=> ! [X9] :
( '@<_succeeds'(X8,s(X9))
=> '@<_succeeds'(X7,X9) ) ) ),
inference(rectify,[],[f75]) ).
fof(f79,plain,
? [X0,X1,X2] :
( '@<_succeeds'(X1,s(X2))
& '@<_succeeds'(X0,X1)
& ~ '@<_succeeds'(X0,X2) ),
inference(ennf_transformation,[],[f77]) ).
fof(f80,plain,
? [X0,X1,X2] :
( '@<_succeeds'(X1,s(X2))
& '@<_succeeds'(X0,X1)
& ~ '@<_succeeds'(X0,X2) ),
inference(flattening,[],[f79]) ).
fof(f81,plain,
! [X0,X1] :
( s(X0) != s(X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f2]) ).
fof(f82,plain,
( ? [X0,X1] :
( ( ? [X5] :
( X1 = s(X5)
& X0 = '0' )
| ? [X2,X3] :
( ! [X4] :
( ~ '@<_succeeds'(X3,s(X4))
| '@<_succeeds'(X2,X4) )
& '@<_succeeds'(X2,X3)
& X1 = s(X3)
& X0 = s(X2) ) )
& ? [X6] :
( '@<_succeeds'(X1,s(X6))
& ~ '@<_succeeds'(X0,X6) ) )
| ! [X7,X8] :
( ~ '@<_succeeds'(X7,X8)
| ! [X9] :
( ~ '@<_succeeds'(X8,s(X9))
| '@<_succeeds'(X7,X9) ) ) ),
inference(ennf_transformation,[],[f78]) ).
fof(f83,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| ? [X2] : X1 = s(X2) ),
inference(ennf_transformation,[],[f74]) ).
fof(f84,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| nat_succeeds(X0) ),
inference(ennf_transformation,[],[f73]) ).
fof(f87,plain,
( '@<_succeeds'(sK2,s(sK3))
& '@<_succeeds'(sK1,sK2)
& ~ '@<_succeeds'(sK1,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3)],[f80]) ).
fof(f88,plain,
! [X0] :
( ( ~ nat_succeeds(X0)
| X0 = '0'
| ? [X1] :
( nat_succeeds(X1)
& X0 = s(X1) ) )
& ( ( '0' != X0
& ! [X1] :
( ~ nat_succeeds(X1)
| s(X1) != X0 ) )
| nat_succeeds(X0) ) ),
inference(nnf_transformation,[],[f27]) ).
fof(f89,plain,
! [X0] :
( ( ~ nat_succeeds(X0)
| X0 = '0'
| ? [X1] :
( nat_succeeds(X1)
& X0 = s(X1) ) )
& ( ( '0' != X0
& ! [X1] :
( ~ nat_succeeds(X1)
| s(X1) != X0 ) )
| nat_succeeds(X0) ) ),
inference(flattening,[],[f88]) ).
fof(f90,plain,
! [X0] :
( ( ~ nat_succeeds(X0)
| X0 = '0'
| ? [X2] :
( nat_succeeds(X2)
& s(X2) = X0 ) )
& ( ( '0' != X0
& ! [X1] :
( ~ nat_succeeds(X1)
| s(X1) != X0 ) )
| nat_succeeds(X0) ) ),
inference(rectify,[],[f89]) ).
fof(f91,plain,
! [X0] :
( ( ~ nat_succeeds(X0)
| X0 = '0'
| ( nat_succeeds(sK4(X0))
& s(sK4(X0)) = X0 ) )
& ( ( '0' != X0
& ! [X1] :
( ~ nat_succeeds(X1)
| s(X1) != X0 ) )
| nat_succeeds(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0))],[f90]) ).
fof(f94,plain,
( ? [X3,X4] :
( sP0(X3,X4)
& ? [X5] :
( '@<_succeeds'(X4,s(X5))
& ~ '@<_succeeds'(X3,X5) ) )
| ! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| ! [X2] :
( ~ '@<_succeeds'(X1,s(X2))
| '@<_succeeds'(X0,X2) ) ) ),
inference(rectify,[],[f86]) ).
fof(f95,plain,
( ( sP0(sK8,sK9)
& '@<_succeeds'(sK9,s(sK10))
& ~ '@<_succeeds'(sK8,sK10) )
| ! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| ! [X2] :
( ~ '@<_succeeds'(X1,s(X2))
| '@<_succeeds'(X0,X2) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X3,sK8),skolemize(X4,sK9),skolemize(X5,sK10)],[f94]) ).
fof(f96,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| s(sK11(X1)) = X1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11(X1))],[f83]) ).
fof(f97,plain,
! [X0,X1] :
( ( ~ '@<_succeeds'(X0,X1)
| ? [X4] :
( X1 = s(X4)
& X0 = '0' )
| ? [X2,X3] :
( '@<_succeeds'(X2,X3)
& X1 = s(X3)
& X0 = s(X2) ) )
& ( ( ! [X4] :
( s(X4) != X1
| '0' != X0 )
& ! [X2,X3] :
( ~ '@<_succeeds'(X2,X3)
| s(X3) != X1
| s(X2) != X0 ) )
| '@<_succeeds'(X0,X1) ) ),
inference(nnf_transformation,[],[f24]) ).
fof(f98,plain,
! [X0,X1] :
( ( ~ '@<_succeeds'(X0,X1)
| ? [X4] :
( X1 = s(X4)
& X0 = '0' )
| ? [X2,X3] :
( '@<_succeeds'(X2,X3)
& X1 = s(X3)
& X0 = s(X2) ) )
& ( ( ! [X4] :
( s(X4) != X1
| '0' != X0 )
& ! [X2,X3] :
( ~ '@<_succeeds'(X2,X3)
| s(X3) != X1
| s(X2) != X0 ) )
| '@<_succeeds'(X0,X1) ) ),
inference(flattening,[],[f97]) ).
fof(f99,plain,
! [X0,X1] :
( ( ~ '@<_succeeds'(X0,X1)
| ? [X7] :
( s(X7) = X1
& X0 = '0' )
| ? [X5,X6] :
( '@<_succeeds'(X5,X6)
& s(X6) = X1
& s(X5) = X0 ) )
& ( ( ! [X4] :
( s(X4) != X1
| '0' != X0 )
& ! [X2,X3] :
( ~ '@<_succeeds'(X2,X3)
| s(X3) != X1
| s(X2) != X0 ) )
| '@<_succeeds'(X0,X1) ) ),
inference(rectify,[],[f98]) ).
fof(f100,plain,
! [X0,X1] :
( ( ~ '@<_succeeds'(X0,X1)
| ( s(sK14(X0,X1)) = X1
& X0 = '0' )
| ( '@<_succeeds'(sK12(X0,X1),sK13(X0,X1))
& s(sK13(X0,X1)) = X1
& s(sK12(X0,X1)) = X0 ) )
& ( ( ! [X4] :
( s(X4) != X1
| '0' != X0 )
& ! [X2,X3] :
( ~ '@<_succeeds'(X2,X3)
| s(X3) != X1
| s(X2) != X0 ) )
| '@<_succeeds'(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14]),skolemize(X5,sK12(X0,X1)),skolemize(X6,sK13(X0,X1)),skolemize(X7,sK14(X0,X1))],[f99]) ).
fof(f101,plain,
'@<_succeeds'(sK2,s(sK3)),
inference(cnf_transformation,[],[f87]) ).
fof(f102,plain,
'@<_succeeds'(sK1,sK2),
inference(cnf_transformation,[],[f87]) ).
fof(f103,plain,
~ '@<_succeeds'(sK1,sK3),
inference(cnf_transformation,[],[f87]) ).
fof(f105,plain,
! [X0] :
( ~ nat_succeeds(X0)
| '0' = X0
| s(sK4(X0)) = X0 ),
inference(cnf_transformation,[],[f91]) ).
fof(f107,plain,
! [X0,X1] :
( ~ nat_succeeds(X1)
| s(X1) != X0
| nat_succeeds(X0) ),
inference(cnf_transformation,[],[f91]) ).
fof(f108,plain,
! [X0,X1] :
( s(X0) != s(X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f81]) ).
fof(f109,plain,
! [X0] : '0' != s(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f118,plain,
! [X2,X0,X1] :
( sP0(sK8,sK9)
| ~ '@<_succeeds'(X0,X1)
| ~ '@<_succeeds'(X1,s(X2))
| '@<_succeeds'(X0,X2) ),
inference(cnf_transformation,[],[f95]) ).
fof(f119,plain,
! [X2,X0,X1] :
( '@<_succeeds'(sK9,s(sK10))
| ~ '@<_succeeds'(X0,X1)
| ~ '@<_succeeds'(X1,s(X2))
| '@<_succeeds'(X0,X2) ),
inference(cnf_transformation,[],[f95]) ).
fof(f120,plain,
! [X2,X0,X1] :
( ~ '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'(X0,X1)
| ~ '@<_succeeds'(X1,s(X2))
| '@<_succeeds'(X0,X2) ),
inference(cnf_transformation,[],[f95]) ).
fof(f121,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| s(sK11(X1)) = X1 ),
inference(cnf_transformation,[],[f96]) ).
fof(f122,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| nat_succeeds(X0) ),
inference(cnf_transformation,[],[f84]) ).
fof(f124,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| '0' = X0
| '@<_succeeds'(sK12(X0,X1),sK13(X0,X1)) ),
inference(cnf_transformation,[],[f100]) ).
fof(f126,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| '0' = X0
| s(sK13(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f100]) ).
fof(f127,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| s(sK14(X0,X1)) = X1
| s(sK12(X0,X1)) = X0 ),
inference(cnf_transformation,[],[f100]) ).
fof(f128,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| '0' = X0
| s(sK12(X0,X1)) = X0 ),
inference(cnf_transformation,[],[f100]) ).
fof(f129,plain,
! [X0,X1,X4] :
( s(X4) != X1
| '0' != X0
| '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f130,plain,
! [X2,X3,X0,X1] :
( ~ '@<_succeeds'(X2,X3)
| s(X3) != X1
| s(X2) != X0
| '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f131,plain,
! [X1] :
( ~ nat_succeeds(X1)
| nat_succeeds(s(X1)) ),
inference(equality_resolution,[],[f107]) ).
fof(f133,plain,
! [X2,X3,X1] :
( ~ '@<_succeeds'(X2,X3)
| s(X3) != X1
| '@<_succeeds'(s(X2),X1) ),
inference(equality_resolution,[],[f130]) ).
fof(f134,plain,
! [X2,X3] :
( ~ '@<_succeeds'(X2,X3)
| '@<_succeeds'(s(X2),s(X3)) ),
inference(equality_resolution,[],[f133]) ).
fof(f135,plain,
! [X1,X4] :
( s(X4) != X1
| '@<_succeeds'('0',X1) ),
inference(equality_resolution,[],[f129]) ).
fof(f136,plain,
! [X4] : '@<_succeeds'('0',s(X4)),
inference(equality_resolution,[],[f135]) ).
tcf(c_49,negated_conjecture,
~ '@<_succeeds'(sK1,sK3),
inference(cnf_transformation,[],[f103]) ).
tcf(c_50,negated_conjecture,
'@<_succeeds'(sK1,sK2),
inference(cnf_transformation,[],[f102]) ).
tcf(c_51,negated_conjecture,
'@<_succeeds'(sK2,s(sK3)),
inference(cnf_transformation,[],[f101]) ).
tcf(c_52,plain,
! [X0: $i] :
( nat_succeeds(s(X0))
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_54,plain,
! [X0: $i] :
( ( X0 = '0' )
| ( s(sK4(X0)) = X0 )
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( s(X0) != s(X1) ) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_57,plain,
! [X0: $i] : s(X0) != '0',
inference(cnf_transformation,[],[f109]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( '@<_succeeds'(X2,X1)
| ~ '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'(X2,X0)
| ~ '@<_succeeds'(X0,s(X1)) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] :
( '@<_succeeds'(X2,X1)
| '@<_succeeds'(sK9,s(sK10))
| ~ '@<_succeeds'(X2,X0)
| ~ '@<_succeeds'(X0,s(X1)) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(sK8,sK9)
| '@<_succeeds'(X2,X1)
| ~ '@<_succeeds'(X2,X0)
| ~ '@<_succeeds'(X0,s(X1)) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i] :
( ( s(sK11(X1)) = X1 )
| ~ '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i] :
( nat_succeeds(X0)
| ~ '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( '@<_succeeds'(s(X0),s(X1))
| ~ '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_72,plain,
! [X0: $i] : '@<_succeeds'('0',s(X0)),
inference(cnf_transformation,[],[f136]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( ( X0 = '0' )
| ( s(sK12(X0,X1)) = X0 )
| ~ '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( ( s(sK14(X0,X1)) = X1 )
| ( s(sK12(X0,X1)) = X0 )
| ~ '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] :
( ( X0 = '0' )
| ( s(sK13(X0,X1)) = X1 )
| ~ '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i] :
( '@<_succeeds'(sK12(X0,X1),sK13(X0,X1))
| ( X0 = '0' )
| ~ '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_955,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_957,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_958,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( '@<_succeeds'(X0,X2)
| ~ '@<_succeeds'(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_968,plain,
'0' = '0',
inference(instantiation,[status(thm)],[c_955]) ).
tcf(c_1528,plain,
nat_succeeds(sK1),
inference(superposition,[status(thm)],[c_50,c_70]) ).
tcf(c_1529,plain,
nat_succeeds(sK2),
inference(superposition,[status(thm)],[c_51,c_70]) ).
tcf(c_1540,plain,
! [X0: $i,X1: $i] :
( nat_succeeds(s(X0))
| ~ '@<_succeeds'(X0,X1) ),
inference(superposition,[status(thm)],[c_71,c_70]) ).
tcf(c_1554,plain,
s(sK11(sK2)) = sK2,
inference(superposition,[status(thm)],[c_50,c_69]) ).
tcf(c_1557,plain,
! [X0: $i] : s(sK11(s(X0))) = s(X0),
inference(superposition,[status(thm)],[c_72,c_69]) ).
tcf(c_1576,plain,
( ( sK1 = '0' )
| ( s(sK4(sK1)) = sK1 ) ),
inference(superposition,[status(thm)],[c_1528,c_54]) ).
tcf(c_1579,plain,
( ( sK2 = '0' )
| ( s(sK4(sK2)) = sK2 ) ),
inference(superposition,[status(thm)],[c_1529,c_54]) ).
tcf(c_1590,plain,
sK2 != '0',
inference(superposition,[status(thm)],[c_1554,c_57]) ).
tcf(c_1639,plain,
s(sK4(sK2)) = sK2,
inference(global_subsumption_just,[status(thm)],[c_1579,c_1579,c_1590]) ).
tcf(c_1647,plain,
! [X0: $i] :
( ( sK4(sK2) = X0 )
| ( s(X0) != sK2 ) ),
inference(superposition,[status(thm)],[c_1639,c_56]) ).
tcf(c_1681,plain,
( ( sK1 = '0' )
| ( s(sK12(sK1,sK2)) = sK1 ) ),
inference(superposition,[status(thm)],[c_50,c_73]) ).
tcf(c_1682,plain,
( ( sK2 = '0' )
| ( s(sK12(sK2,s(sK3))) = sK2 ) ),
inference(superposition,[status(thm)],[c_51,c_73]) ).
tcf(c_1688,plain,
s(sK12(sK2,s(sK3))) = sK2,
inference(forward_subsumption_resolution,[status(thm)],[c_1682,c_1590]) ).
tcf(c_1699,plain,
( ( sK1 = '0' )
| ( s(sK13(sK1,sK2)) = sK2 ) ),
inference(superposition,[status(thm)],[c_50,c_75]) ).
tcf(c_1700,plain,
( ( sK2 = '0' )
| ( s(sK13(sK2,s(sK3))) = s(sK3) ) ),
inference(superposition,[status(thm)],[c_51,c_75]) ).
tcf(c_1706,plain,
s(sK13(sK2,s(sK3))) = s(sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_1700,c_1590]) ).
tcf(c_1744,plain,
! [X0: $i,X1: $i,X2: $i] :
( '@<_succeeds'(X0,X2)
| ~ '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'(X1,X2)
| ~ '@<_succeeds'(X0,s(X1)) ),
inference(superposition,[status(thm)],[c_71,c_66]) ).
tcf(c_1778,plain,
! [X0: $i,X1: $i] :
( nat_succeeds(s(sK12(X0,X1)))
| ( X0 = '0' )
| ~ '@<_succeeds'(X0,X1) ),
inference(superposition,[status(thm)],[c_77,c_1540]) ).
tcf(c_1810,plain,
! [X0: $i] :
( ( sK1 = '0' )
| ( sK12(sK1,sK2) = X0 )
| ( s(X0) != sK1 ) ),
inference(superposition,[status(thm)],[c_1681,c_56]) ).
tcf(c_1844,plain,
! [X0: $i] :
( ( sK1 = '0' )
| ( sK13(sK1,sK2) = X0 )
| ( s(X0) != sK2 ) ),
inference(superposition,[status(thm)],[c_1699,c_56]) ).
tcf(c_1985,plain,
! [X0: $i] :
( '@<_succeeds'(X0,sK3)
| '@<_succeeds'(sK9,s(sK10))
| ~ '@<_succeeds'(X0,sK2) ),
inference(superposition,[status(thm)],[c_51,c_67]) ).
tcf(c_2060,plain,
( ( s(sK14(sK1,sK2)) = sK2 )
| ( s(sK12(sK1,sK2)) = sK1 ) ),
inference(superposition,[status(thm)],[c_50,c_74]) ).
tcf(c_2063,plain,
! [X0: $i] :
( ( s(sK14('0',s(X0))) = s(X0) )
| ( s(sK12('0',s(X0))) = '0' ) ),
inference(superposition,[status(thm)],[c_72,c_74]) ).
tcf(c_2070,plain,
! [X0: $i] : s(sK14('0',s(X0))) = s(X0),
inference(forward_subsumption_resolution,[status(thm)],[c_2063,c_57]) ).
tcf(c_2081,plain,
! [X0: $i,X1: $i] :
( ( s(X0) = '0' )
| ( '0' != X1 )
| ( s(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_957]) ).
tcf(c_2232,plain,
! [X0: $i,X1: $i] :
( ( sK11(s(X0)) = X1 )
| ( s(X0) != s(X1) ) ),
inference(superposition,[status(thm)],[c_1557,c_56]) ).
tcf(c_2333,plain,
! [X0: $i,X1: $i] :
( ( X0 = sK1 )
| ( sK1 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_957]) ).
tcf(c_2334,plain,
( ( '0' = sK1 )
| ( '0' != '0' )
| ( sK1 != '0' ) ),
inference(instantiation,[status(thm)],[c_2333]) ).
tcf(c_2345,plain,
( '@<_succeeds'(sK1,sK3)
| '@<_succeeds'(sK9,s(sK10)) ),
inference(superposition,[status(thm)],[c_50,c_1985]) ).
tcf(c_2349,plain,
'@<_succeeds'(sK9,s(sK10)),
inference(forward_subsumption_resolution,[status(thm)],[c_2345,c_49]) ).
tcf(c_2355,plain,
( ( '0' = sK9 )
| ( s(sK13(sK9,s(sK10))) = s(sK10) ) ),
inference(superposition,[status(thm)],[c_2349,c_75]) ).
tcf(c_2356,plain,
( ( '0' = sK9 )
| ( s(sK12(sK9,s(sK10))) = sK9 ) ),
inference(superposition,[status(thm)],[c_2349,c_73]) ).
tcf(c_2495,plain,
! [X0: $i,X1: $i,X2: $i] :
( '@<_succeeds'(s(X0),X2)
| ~ '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'(X1,X2)
| ~ '@<_succeeds'(X0,X1) ),
inference(superposition,[status(thm)],[c_71,c_1744]) ).
tcf(c_2622,plain,
( ( s(sK7(sK8,sK9)) = '0' )
| ( '0' != sK9 )
| ( s(sK7(sK8,sK9)) != sK9 ) ),
inference(instantiation,[status(thm)],[c_2081]) ).
tcf(c_3407,plain,
( ( sK1 = '0' )
| ( sK12(sK1,sK2) = sK4(sK1) ) ),
inference(superposition,[status(thm)],[c_1576,c_1810]) ).
tcf(c_3507,plain,
! [X0: $i] :
( ( s(X0) = '0' )
| ( '0' != sK1 )
| ( s(X0) != sK1 ) ),
inference(instantiation,[status(thm)],[c_2081]) ).
tcf(c_3552,plain,
( ( sK1 = '0' )
| ( sK13(sK1,sK2) = sK4(sK2) ) ),
inference(superposition,[status(thm)],[c_1639,c_1844]) ).
tcf(c_5245,plain,
sK12(sK2,s(sK3)) = sK4(sK2),
inference(superposition,[status(thm)],[c_1688,c_1647]) ).
tcf(c_5348,plain,
( '@<_succeeds'(sK4(sK2),sK13(sK2,s(sK3)))
| ( sK2 = '0' )
| ~ '@<_succeeds'(sK2,s(sK3)) ),
inference(superposition,[status(thm)],[c_5245,c_77]) ).
tcf(c_5349,plain,
'@<_succeeds'(sK4(sK2),sK13(sK2,s(sK3))),
inference(forward_subsumption_resolution,[status(thm)],[c_5348,c_1590,c_51]) ).
tcf(c_5359,plain,
s(sK11(sK13(sK2,s(sK3)))) = sK13(sK2,s(sK3)),
inference(superposition,[status(thm)],[c_5349,c_69]) ).
tcf(c_8630,plain,
sK10 = sK10,
inference(instantiation,[status(thm)],[c_955]) ).
tcf(c_8708,plain,
( '@<_succeeds'(sK4(sK1),sK13(sK1,sK2))
| ( sK1 = '0' )
| ~ '@<_succeeds'(sK1,sK2) ),
inference(superposition,[status(thm)],[c_3407,c_77]) ).
tcf(c_8747,plain,
( '@<_succeeds'(sK4(sK1),sK13(sK1,sK2))
| ( sK1 = '0' ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8708,c_50]) ).
tcf(c_10018,plain,
( '@<_succeeds'(sK4(sK1),sK4(sK2))
| ( sK1 = '0' ) ),
inference(superposition,[status(thm)],[c_3552,c_8747]) ).
tcf(c_15736,plain,
! [X0: $i] : s(sK11(s(X0))) = s(X0),
inference(superposition,[status(thm)],[c_72,c_69]) ).
tcf(c_15792,plain,
! [X0: $i,X1: $i] :
( ( sK11(s(X0)) = X1 )
| ( s(X0) != s(X1) ) ),
inference(superposition,[status(thm)],[c_15736,c_56]) ).
tcf(c_16174,plain,
! [X0: $i,X1: $i,X2: $i] :
( '@<_succeeds'(X2,sK11(s(X1)))
| ~ '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'(X2,X0)
| ~ '@<_succeeds'(X0,s(X1)) ),
inference(superposition,[status(thm)],[c_15736,c_66]) ).
tcf(c_17459,plain,
! [X0: $i] :
( '@<_succeeds'(X0,sK11(s(sK3)))
| ~ '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'(X0,sK2) ),
inference(superposition,[status(thm)],[c_51,c_16174]) ).
tcf(c_19582,plain,
! [X0: $i] :
( ( s(sK11(sK11(s(sK3)))) = sK11(s(sK3)) )
| ~ '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'(X0,sK2) ),
inference(superposition,[status(thm)],[c_17459,c_69]) ).
tcf(c_19682,plain,
! [X0: $i] :
( ( sK1 = '0' )
| ( sK11(s(sK12(sK1,sK2))) = X0 )
| ( s(X0) != sK1 ) ),
inference(superposition,[status(thm)],[c_1681,c_2232]) ).
tcf(c_19781,plain,
! [X0: $i] : sK11(s(X0)) = X0,
inference(equality_resolution,[status(thm)],[c_2232]) ).
tcf(c_20682,plain,
sK13(sK2,s(sK3)) = sK11(s(sK3)),
inference(superposition,[status(thm)],[c_1706,c_19781]) ).
tcf(c_20686,plain,
! [X0: $i] : sK14('0',s(X0)) = sK11(s(X0)),
inference(superposition,[status(thm)],[c_2070,c_19781]) ).
tcf(c_20692,plain,
( ( '0' = sK9 )
| ( sK13(sK9,s(sK10)) = sK11(s(sK10)) ) ),
inference(superposition,[status(thm)],[c_2355,c_19781]) ).
tcf(c_20693,plain,
( ( '0' = sK9 )
| ( sK12(sK9,s(sK10)) = sK11(sK9) ) ),
inference(superposition,[status(thm)],[c_2356,c_19781]) ).
tcf(c_20720,plain,
! [X0: $i] : sK14('0',s(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_20686,c_19781]) ).
tcf(c_20773,plain,
s(sK11(sK11(s(sK3)))) = sK11(s(sK3)),
inference(demodulation,[status(thm)],[c_5359,c_20682]) ).
tcf(c_20774,plain,
'@<_succeeds'(sK4(sK2),sK11(s(sK3))),
inference(demodulation,[status(thm)],[c_5349,c_20682]) ).
tcf(c_20911,plain,
'@<_succeeds'(sK4(sK2),sK3),
inference(demodulation,[status(thm)],[c_20774,c_19781]) ).
tcf(c_21079,plain,
! [X0: $i] :
( ( s(X0) != sK1 )
| ( sK11(s(sK12(sK1,sK2))) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_19682,c_57,c_968,c_2334,c_3507,c_19682]) ).
tcf(c_21080,plain,
! [X0: $i] :
( ( sK11(s(sK12(sK1,sK2))) = X0 )
| ( s(X0) != sK1 ) ),
inference(renaming,[status(thm)],[c_21079]) ).
tcf(c_21082,plain,
! [X0: $i] :
( ( sK12(sK1,sK2) = X0 )
| ( s(X0) != sK1 ) ),
inference(demodulation,[status(thm)],[c_21080,c_19781]) ).
tcf(c_21098,plain,
( ( sK12(sK1,sK2) = sK14(sK1,sK2) )
| ( s(sK12(sK1,sK2)) = sK1 )
| ( sK1 != sK2 ) ),
inference(superposition,[status(thm)],[c_2060,c_21082]) ).
tcf(c_32805,plain,
s(sK7(sK8,sK9)) != '0',
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_40778,plain,
! [X0: $i,X1: $i] :
( '@<_succeeds'(sK1,sK3)
| ~ '@<_succeeds'(X0,X1)
| ( sK3 != X1 )
| ( sK1 != X0 ) ),
inference(instantiation,[status(thm)],[c_958]) ).
tcf(c_40779,plain,
! [X0: $i,X1: $i] :
( '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'(X0,X1)
| ( sK10 != X1 )
| ( sK8 != X0 ) ),
inference(instantiation,[status(thm)],[c_958]) ).
tcf(c_45741,plain,
! [X0: $i] : sK11(s(X0)) = X0,
inference(equality_resolution,[status(thm)],[c_15792]) ).
tcf(c_52379,plain,
! [X0: $i] :
( '@<_succeeds'(sK1,sK3)
| ~ '@<_succeeds'(X0,sK3)
| ( sK3 != sK3 )
| ( sK1 != X0 ) ),
inference(instantiation,[status(thm)],[c_40778]) ).
tcf(c_52380,plain,
sK3 = sK3,
inference(instantiation,[status(thm)],[c_955]) ).
tcf(c_52381,plain,
( '@<_succeeds'(sK1,sK3)
| ~ '@<_succeeds'('0',sK3)
| ( sK3 != sK3 )
| ( sK1 != '0' ) ),
inference(instantiation,[status(thm)],[c_52379]) ).
tcf(c_55958,plain,
s(sK11(sK11(s(sK3)))) = sK11(s(sK3)),
inference(global_subsumption_just,[status(thm)],[c_19582,c_20773]) ).
tcf(c_55960,plain,
s(sK11(sK3)) = sK3,
inference(demodulation,[status(thm)],[c_55958,c_45741]) ).
tcf(c_55977,plain,
'@<_succeeds'('0',sK3),
inference(superposition,[status(thm)],[c_55960,c_72]) ).
tcf(c_66868,plain,
s(sK12(sK1,sK2)) = sK1,
inference(global_subsumption_just,[status(thm)],[c_21098,c_49,c_1681,c_52381,c_52380,c_55977]) ).
tcf(c_66920,plain,
sK1 != '0',
inference(superposition,[status(thm)],[c_66868,c_57]) ).
tcf(c_67066,plain,
'@<_succeeds'(sK4(sK1),sK4(sK2)),
inference(backward_subsumption_resolution,[status(thm)],[c_10018,c_66920]) ).
tcf(c_67088,plain,
s(sK4(sK1)) = sK1,
inference(backward_subsumption_resolution,[status(thm)],[c_1576,c_66920]) ).
tcf(c_68098,plain,
! [X0: $i] :
( '@<_succeeds'(s(sK4(sK1)),X0)
| ~ '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'(sK4(sK2),X0) ),
inference(superposition,[status(thm)],[c_67066,c_2495]) ).
tcf(c_68118,plain,
! [X0: $i] :
( '@<_succeeds'(sK1,X0)
| ~ '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'(sK4(sK2),X0) ),
inference(light_normalisation,[status(thm)],[c_68098,c_67088]) ).
tcf(c_83721,plain,
( nat_succeeds(s(sK11(sK9)))
| ( '0' = sK9 )
| ~ '@<_succeeds'(sK9,s(sK10)) ),
inference(superposition,[status(thm)],[c_20693,c_1778]) ).
tcf(c_83729,plain,
( nat_succeeds(s(sK11(sK9)))
| ( '0' = sK9 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_83721,c_2349]) ).
tcf(c_104588,plain,
( '@<_succeeds'(sK1,sK3)
| ~ '@<_succeeds'(sK8,sK10) ),
inference(superposition,[status(thm)],[c_20911,c_68118]) ).
tcf(c_104590,plain,
~ '@<_succeeds'(sK8,sK10),
inference(forward_subsumption_resolution,[status(thm)],[c_104588,c_49]) ).
tcf(c_104847,plain,
( ( '0' = sK9 )
| ( sK13(sK9,s(sK10)) = sK10 ) ),
inference(demodulation,[status(thm)],[c_20692,c_19781]) ).
tcf(c_104855,plain,
( '@<_succeeds'(sK12(sK9,s(sK10)),sK10)
| ( '0' = sK9 )
| ~ '@<_succeeds'(sK9,s(sK10)) ),
inference(superposition,[status(thm)],[c_104847,c_77]) ).
tcf(c_104867,plain,
( '@<_succeeds'(sK12(sK9,s(sK10)),sK10)
| ( '0' = sK9 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_104855,c_2349]) ).
tcf(c_104890,plain,
( ( '0' = sK9 )
| ( s(sK11(sK10)) = sK10 ) ),
inference(superposition,[status(thm)],[c_104867,c_69]) ).
tcf(c_105023,plain,
( '@<_succeeds'('0',sK10)
| ( '0' = sK9 ) ),
inference(superposition,[status(thm)],[c_104890,c_72]) ).
tcf(c_123958,plain,
! [X0: $i] :
( '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'(X0,sK10)
| ( sK10 != sK10 )
| ( sK8 != X0 ) ),
inference(instantiation,[status(thm)],[c_40779]) ).
tcf(c_123959,plain,
( '@<_succeeds'(sK8,sK10)
| ~ '@<_succeeds'('0',sK10)
| ( sK10 != sK10 )
| ( sK8 != '0' ) ),
inference(instantiation,[status(thm)],[c_123958]) ).
tcf(c_129800,plain,
! [X0: $i] : s(sK11(s(X0))) = s(X0),
inference(superposition,[status(thm)],[c_72,c_69]) ).
tcf(c_130004,plain,
'@<_succeeds'(sK9,s(sK10)),
inference(global_subsumption_just,[status(thm)],[c_67,c_2349]) ).
tcf(c_130006,plain,
( ( '0' = sK9 )
| ( s(sK13(sK9,s(sK10))) = s(sK10) ) ),
inference(superposition,[status(thm)],[c_130004,c_75]) ).
tcf(c_130007,plain,
( ( '0' = sK9 )
| ( s(sK12(sK9,s(sK10))) = sK9 ) ),
inference(superposition,[status(thm)],[c_130004,c_73]) ).
tcf(c_130011,plain,
nat_succeeds(sK9),
inference(superposition,[status(thm)],[c_130004,c_70]) ).
tcf(c_130050,plain,
( ( '0' = sK9 )
| ( s(sK4(sK9)) = sK9 ) ),
inference(superposition,[status(thm)],[c_130011,c_54]) ).
tcf(c_130486,plain,
! [X0: $i,X1: $i] :
( ( sK11(s(X0)) = X1 )
| ( s(X0) != s(X1) ) ),
inference(superposition,[status(thm)],[c_129800,c_56]) ).
tcf(c_146289,plain,
! [X0: $i] : sK11(s(X0)) = X0,
inference(equality_resolution,[status(thm)],[c_130486]) ).
fof(f85,definition,
! [X0,X1] :
( ~ sP0(X0,X1)
| ? [X5] :
( X1 = s(X5)
& X0 = '0' )
| ? [X2,X3] :
( ! [X4] :
( ~ '@<_succeeds'(X3,s(X4))
| '@<_succeeds'(X2,X4) )
& '@<_succeeds'(X2,X3)
& X1 = s(X3)
& X0 = s(X2) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f86,plain,
( ? [X0,X1] :
( sP0(X0,X1)
& ? [X6] :
( '@<_succeeds'(X1,s(X6))
& ~ '@<_succeeds'(X0,X6) ) )
| ! [X7,X8] :
( ~ '@<_succeeds'(X7,X8)
| ! [X9] :
( ~ '@<_succeeds'(X8,s(X9))
| '@<_succeeds'(X7,X9) ) ) ),
inference(definition_folding,[],[f82,f85]) ).
fof(f92,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ? [X5] :
( X1 = s(X5)
& X0 = '0' )
| ? [X2,X3] :
( ! [X4] :
( ~ '@<_succeeds'(X3,s(X4))
| '@<_succeeds'(X2,X4) )
& '@<_succeeds'(X2,X3)
& X1 = s(X3)
& X0 = s(X2) ) ),
inference(nnf_transformation,[],[f85]) ).
fof(f93,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ( s(sK7(X0,X1)) = X1
& X0 = '0' )
| ( ! [X4] :
( ~ '@<_succeeds'(sK6(X0,X1),s(X4))
| '@<_succeeds'(sK5(X0,X1),X4) )
& '@<_succeeds'(sK5(X0,X1),sK6(X0,X1))
& s(sK6(X0,X1)) = X1
& s(sK5(X0,X1)) = X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7]),skolemize(X2,sK5(X0,X1)),skolemize(X3,sK6(X0,X1)),skolemize(X5,sK7(X0,X1))],[f92]) ).
fof(f110,plain,
! [X0,X1,X4] :
( ~ sP0(X0,X1)
| s(sK7(X0,X1)) = X1
| ~ '@<_succeeds'(sK6(X0,X1),s(X4))
| '@<_succeeds'(sK5(X0,X1),X4) ),
inference(cnf_transformation,[],[f93]) ).
fof(f111,plain,
! [X0,X1,X4] :
( ~ sP0(X0,X1)
| '0' = X0
| ~ '@<_succeeds'(sK6(X0,X1),s(X4))
| '@<_succeeds'(sK5(X0,X1),X4) ),
inference(cnf_transformation,[],[f93]) ).
fof(f113,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| '0' = X0
| '@<_succeeds'(sK5(X0,X1),sK6(X0,X1)) ),
inference(cnf_transformation,[],[f93]) ).
fof(f115,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| '0' = X0
| s(sK6(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f93]) ).
fof(f116,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| s(sK7(X0,X1)) = X1
| s(sK5(X0,X1)) = X0 ),
inference(cnf_transformation,[],[f93]) ).
fof(f117,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| '0' = X0
| s(sK5(X0,X1)) = X0 ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( ( X0 = '0' )
| ( s(sK5(X0,X1)) = X0 )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( ( s(sK7(X0,X1)) = X1 )
| ( s(sK5(X0,X1)) = X0 )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( ( X0 = '0' )
| ( s(sK6(X0,X1)) = X1 )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( '@<_succeeds'(sK5(X0,X1),sK6(X0,X1))
| ( X0 = '0' )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] :
( '@<_succeeds'(sK5(X0,X1),X2)
| ( X0 = '0' )
| ~ sP0(X0,X1)
| ~ '@<_succeeds'(sK6(X0,X1),s(X2)) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( '@<_succeeds'(sK5(X0,X1),X2)
| ( s(sK7(X0,X1)) = X1 )
| ~ sP0(X0,X1)
| ~ '@<_succeeds'(sK6(X0,X1),s(X2)) ),
inference(cnf_transformation,[],[f110]) ).
tcf(c_406,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( '@<_succeeds'(X5,X4)
| '@<_succeeds'(sK5(X0,X1),X2)
| ( s(sK7(X0,X1)) = X1 )
| ~ '@<_succeeds'(X5,X3)
| ~ '@<_succeeds'(X3,s(X4))
| ~ '@<_succeeds'(sK6(X0,X1),s(X2))
| ( X1 != sK9 )
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_65,c_68]) ).
tcf(c_407,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( '@<_succeeds'(X3,X2)
| '@<_succeeds'(sK5(sK8,sK9),X0)
| ( s(sK7(sK8,sK9)) = sK9 )
| ~ '@<_succeeds'(X3,X1)
| ~ '@<_succeeds'(X1,s(X2))
| ~ '@<_succeeds'(sK6(sK8,sK9),s(X0)) ),
inference(unflattening,[status(thm)],[c_406]) ).
tcf(c_426,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( '@<_succeeds'(X5,X4)
| '@<_succeeds'(sK5(X0,X1),X2)
| ( X0 = '0' )
| ~ '@<_succeeds'(X5,X3)
| ~ '@<_succeeds'(X3,s(X4))
| ~ '@<_succeeds'(sK6(X0,X1),s(X2))
| ( X1 != sK9 )
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_68]) ).
tcf(c_427,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( '@<_succeeds'(X3,X2)
| '@<_succeeds'(sK5(sK8,sK9),X0)
| ( sK8 = '0' )
| ~ '@<_succeeds'(X3,X1)
| ~ '@<_succeeds'(X1,s(X2))
| ~ '@<_succeeds'(sK6(sK8,sK9),s(X0)) ),
inference(unflattening,[status(thm)],[c_426]) ).
tcf(c_463,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( '@<_succeeds'(X4,X3)
| '@<_succeeds'(sK5(X0,X1),sK6(X0,X1))
| ( X0 = '0' )
| ~ '@<_succeeds'(X4,X2)
| ~ '@<_succeeds'(X2,s(X3))
| ( X1 != sK9 )
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_68]) ).
tcf(c_464,plain,
! [X0: $i,X1: $i,X2: $i] :
( '@<_succeeds'(X2,X1)
| '@<_succeeds'(sK5(sK8,sK9),sK6(sK8,sK9))
| ( sK8 = '0' )
| ~ '@<_succeeds'(X2,X0)
| ~ '@<_succeeds'(X0,s(X1)) ),
inference(unflattening,[status(thm)],[c_463]) ).
tcf(c_497,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( '@<_succeeds'(X4,X3)
| ( X0 = '0' )
| ( s(sK6(X0,X1)) = X1 )
| ~ '@<_succeeds'(X4,X2)
| ~ '@<_succeeds'(X2,s(X3))
| ( X1 != sK9 )
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_68]) ).
tcf(c_498,plain,
! [X0: $i,X1: $i,X2: $i] :
( '@<_succeeds'(X2,X1)
| ( sK8 = '0' )
| ( s(sK6(sK8,sK9)) = sK9 )
| ~ '@<_succeeds'(X2,X0)
| ~ '@<_succeeds'(X0,s(X1)) ),
inference(unflattening,[status(thm)],[c_497]) ).
tcf(c_514,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( '@<_succeeds'(X4,X3)
| ( s(sK7(X0,X1)) = X1 )
| ( s(sK5(X0,X1)) = X0 )
| ~ '@<_succeeds'(X4,X2)
| ~ '@<_succeeds'(X2,s(X3))
| ( X1 != sK9 )
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_68]) ).
tcf(c_515,plain,
! [X0: $i,X1: $i,X2: $i] :
( '@<_succeeds'(X2,X1)
| ( s(sK7(sK8,sK9)) = sK9 )
| ( s(sK5(sK8,sK9)) = sK8 )
| ~ '@<_succeeds'(X2,X0)
| ~ '@<_succeeds'(X0,s(X1)) ),
inference(unflattening,[status(thm)],[c_514]) ).
tcf(c_531,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( '@<_succeeds'(X4,X3)
| ( X0 = '0' )
| ( s(sK5(X0,X1)) = X0 )
| ~ '@<_succeeds'(X4,X2)
| ~ '@<_succeeds'(X2,s(X3))
| ( X1 != sK9 )
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_68]) ).
tcf(c_532,plain,
! [X0: $i,X1: $i,X2: $i] :
( '@<_succeeds'(X2,X1)
| ( sK8 = '0' )
| ( s(sK5(sK8,sK9)) = sK8 )
| ~ '@<_succeeds'(X2,X0)
| ~ '@<_succeeds'(X0,s(X1)) ),
inference(unflattening,[status(thm)],[c_531]) ).
tcf(c_945,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iPr_def_10
| ~ '@<_succeeds'(X1,s(X2))
| '@<_succeeds'(X0,X2)
| ~ '@<_succeeds'(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_532]) ).
tcf(c_946,plain,
( iPr_def_10
| ( sK8 = '0' )
| ( s(sK5(sK8,sK9)) = sK8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_532]) ).
tcf(c_947,plain,
( iPr_def_10
| ( s(sK7(sK8,sK9)) = sK9 )
| ( s(sK5(sK8,sK9)) = sK8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_515]) ).
tcf(c_948,plain,
( iPr_def_10
| ( sK8 = '0' )
| ( s(sK6(sK8,sK9)) = sK9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_498]) ).
tcf(c_950,plain,
( iPr_def_10
| '@<_succeeds'(sK5(sK8,sK9),sK6(sK8,sK9))
| ( sK8 = '0' ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_464]) ).
tcf(c_952,plain,
! [X0: $i] :
( ~ iPr_def_11
| '@<_succeeds'(sK5(sK8,sK9),X0)
| ~ '@<_succeeds'(sK6(sK8,sK9),s(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_427]) ).
tcf(c_953,plain,
( iPr_def_11
| iPr_def_10
| ( sK8 = '0' ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_427]) ).
tcf(c_954,plain,
( iPr_def_11
| iPr_def_10
| ( s(sK7(sK8,sK9)) = sK9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_407]) ).
tcf(c_4773,plain,
! [X0: $i] :
( '@<_succeeds'(sK1,X0)
| ~ iPr_def_10
| ~ '@<_succeeds'(sK1,sK2)
| ~ '@<_succeeds'(sK2,s(X0)) ),
inference(instantiation,[status(thm)],[c_945]) ).
tcf(c_5617,plain,
( '@<_succeeds'(sK1,sK3)
| ~ iPr_def_10
| ~ '@<_succeeds'(sK1,sK2)
| ~ '@<_succeeds'(sK2,s(sK3)) ),
inference(instantiation,[status(thm)],[c_4773]) ).
tcf(c_10733,plain,
( iPr_def_11
| ( s(sK7(sK8,sK9)) = sK9 ) ),
inference(global_subsumption_just,[status(thm)],[c_954,c_50,c_51,c_49,c_954,c_5617]) ).
tcf(c_15703,plain,
( iPr_def_11
| ( sK8 = '0' ) ),
inference(global_subsumption_just,[status(thm)],[c_953,c_50,c_51,c_49,c_953,c_5617]) ).
tcf(c_54122,plain,
( ( s(sK5(sK8,sK9)) = sK8 )
| ( sK8 = '0' ) ),
inference(global_subsumption_just,[status(thm)],[c_946,c_50,c_51,c_49,c_946,c_5617]) ).
tcf(c_54123,plain,
( ( sK8 = '0' )
| ( s(sK5(sK8,sK9)) = sK8 ) ),
inference(renaming,[status(thm)],[c_54122]) ).
tcf(c_54150,plain,
( ( '0' = sK8 )
| ( sK5(sK8,sK9) = sK11(sK8) ) ),
inference(superposition,[status(thm)],[c_54123,c_19781]) ).
tcf(c_54163,plain,
( nat_succeeds(sK8)
| ( '0' = sK8 )
| ~ nat_succeeds(sK5(sK8,sK9)) ),
inference(superposition,[status(thm)],[c_54123,c_52]) ).
tcf(c_54164,plain,
( '@<_succeeds'('0',sK8)
| ( '0' = sK8 ) ),
inference(superposition,[status(thm)],[c_54123,c_72]) ).
tcf(c_54352,plain,
( ( '0' = sK8 )
| ( s(sK11(sK8)) = sK8 ) ),
inference(superposition,[status(thm)],[c_54164,c_69]) ).
tcf(c_54515,plain,
! [X0: $i] :
( '@<_succeeds'(sK8,s(X0))
| ( '0' = sK8 )
| ~ '@<_succeeds'(sK11(sK8),X0) ),
inference(superposition,[status(thm)],[c_54352,c_71]) ).
tcf(c_55106,plain,
( ( s(sK6(sK8,sK9)) = sK9 )
| ( sK8 = '0' ) ),
inference(global_subsumption_just,[status(thm)],[c_948,c_50,c_51,c_49,c_948,c_5617]) ).
tcf(c_55107,plain,
( ( sK8 = '0' )
| ( s(sK6(sK8,sK9)) = sK9 ) ),
inference(renaming,[status(thm)],[c_55106]) ).
tcf(c_55131,plain,
( ( '0' = sK8 )
| ( sK6(sK8,sK9) = sK14('0',sK9) ) ),
inference(superposition,[status(thm)],[c_55107,c_20720]) ).
tcf(c_55133,plain,
( ( '0' = sK8 )
| ( sK6(sK8,sK9) = sK11(sK9) ) ),
inference(superposition,[status(thm)],[c_55107,c_19781]) ).
tcf(c_55145,plain,
( ( '0' = sK8 )
| ( '0' != sK9 ) ),
inference(superposition,[status(thm)],[c_55107,c_57]) ).
tcf(c_55147,plain,
( '@<_succeeds'('0',sK9)
| ( '0' = sK8 ) ),
inference(superposition,[status(thm)],[c_55107,c_72]) ).
tcf(c_55565,plain,
( ( '0' = sK8 )
| ( s(sK14('0',sK9)) = sK9 )
| ( s(sK12('0',sK9)) = '0' ) ),
inference(superposition,[status(thm)],[c_55147,c_74]) ).
tcf(c_55569,plain,
( ( '0' = sK8 )
| ( s(sK11(sK9)) = sK9 ) ),
inference(superposition,[status(thm)],[c_55147,c_69]) ).
tcf(c_55581,plain,
( ( '0' = sK8 )
| ( s(sK14('0',sK9)) = sK9 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_55565,c_57]) ).
tcf(c_57267,plain,
( ( sK8 = '0' )
| '@<_succeeds'(sK5(sK8,sK9),sK6(sK8,sK9)) ),
inference(global_subsumption_just,[status(thm)],[c_950,c_50,c_51,c_49,c_950,c_5617]) ).
tcf(c_57268,plain,
( '@<_succeeds'(sK5(sK8,sK9),sK6(sK8,sK9))
| ( sK8 = '0' ) ),
inference(renaming,[status(thm)],[c_57267]) ).
tcf(c_57273,plain,
( '@<_succeeds'(sK11(sK8),sK6(sK8,sK9))
| ( '0' = sK8 ) ),
inference(superposition,[status(thm)],[c_54150,c_57268]) ).
tcf(c_57295,plain,
( nat_succeeds(sK5(sK8,sK9))
| ( '0' = sK8 ) ),
inference(superposition,[status(thm)],[c_57268,c_70]) ).
tcf(c_57577,plain,
( nat_succeeds(sK8)
| ( '0' = sK8 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_54163,c_57295]) ).
tcf(c_59570,plain,
( '@<_succeeds'(sK11(sK8),sK11(sK9))
| ( '0' = sK8 ) ),
inference(superposition,[status(thm)],[c_55133,c_57273]) ).
tcf(c_60045,plain,
( '@<_succeeds'(sK8,s(sK11(sK9)))
| ( '0' = sK8 ) ),
inference(superposition,[status(thm)],[c_59570,c_54515]) ).
tcf(c_61446,plain,
( ( '0' = sK8 )
| ( s(sK13(sK8,s(sK11(sK9)))) = s(sK11(sK9)) ) ),
inference(superposition,[status(thm)],[c_60045,c_75]) ).
tcf(c_94310,plain,
( ( '0' = sK8 )
| ( s(sK6(sK8,sK9)) = sK9 ) ),
inference(superposition,[status(thm)],[c_55131,c_55581]) ).
tcf(c_103000,plain,
( nat_succeeds(s(sK11(sK9)))
| ( '0' = sK8 )
| ~ nat_succeeds(sK13(sK8,s(sK11(sK9)))) ),
inference(superposition,[status(thm)],[c_61446,c_52]) ).
tcf(c_106269,plain,
( nat_succeeds(s(sK11(sK9)))
| ( '0' = sK8 ) ),
inference(global_subsumption_just,[status(thm)],[c_103000,c_55145,c_83729]) ).
tcf(c_106281,plain,
( ( '0' = sK8 )
| ( s(sK11(sK9)) = '0' )
| ( s(sK4(s(sK11(sK9)))) = s(sK11(sK9)) ) ),
inference(superposition,[status(thm)],[c_106269,c_54]) ).
tcf(c_106286,plain,
( ( '0' = sK8 )
| ( s(sK4(s(sK11(sK9)))) = s(sK11(sK9)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_106281,c_57]) ).
tcf(c_106295,plain,
( ( '0' = sK8 )
| ( s(sK4(sK9)) = sK9 ) ),
inference(superposition,[status(thm)],[c_55569,c_106286]) ).
tcf(c_125804,plain,
iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_954,c_2622,c_8630,c_10733,c_15703,c_32805,c_104590,c_105023,c_123959]) ).
tcf(c_129767,plain,
s(sK5(sK8,sK9)) = sK8,
inference(global_subsumption_just,[status(thm)],[c_946,c_50,c_51,c_49,c_946,c_947,c_2622,c_5617,c_8630,c_32805,c_104590,c_105023,c_123959]) ).
tcf(c_129770,plain,
'0' != sK8,
inference(superposition,[status(thm)],[c_129767,c_57]) ).
tcf(c_129773,plain,
'@<_succeeds'('0',sK8),
inference(superposition,[status(thm)],[c_129767,c_72]) ).
tcf(c_129850,plain,
s(sK11(sK8)) = sK8,
inference(superposition,[status(thm)],[c_129773,c_69]) ).
tcf(c_130061,plain,
( nat_succeeds(sK8)
| ~ nat_succeeds(sK11(sK8)) ),
inference(superposition,[status(thm)],[c_129850,c_52]) ).
tcf(c_130065,plain,
! [X0: $i] :
( ( sK11(sK8) = X0 )
| ( s(X0) != sK8 ) ),
inference(superposition,[status(thm)],[c_129850,c_56]) ).
tcf(c_130285,plain,
nat_succeeds(sK8),
inference(global_subsumption_just,[status(thm)],[c_130061,c_57577,c_129770]) ).
tcf(c_130287,plain,
( ( '0' = sK8 )
| ( s(sK4(sK8)) = sK8 ) ),
inference(superposition,[status(thm)],[c_130285,c_54]) ).
tcf(c_130288,plain,
s(sK4(sK8)) = sK8,
inference(forward_subsumption_resolution,[status(thm)],[c_130287,c_129770]) ).
tcf(c_132029,plain,
s(sK4(sK9)) = sK9,
inference(global_subsumption_just,[status(thm)],[c_130050,c_106295,c_129770]) ).
tcf(c_132037,plain,
'0' != sK9,
inference(superposition,[status(thm)],[c_132029,c_57]) ).
tcf(c_132042,plain,
! [X0: $i] :
( ( sK4(sK9) = X0 )
| ( s(X0) != sK9 ) ),
inference(superposition,[status(thm)],[c_132029,c_56]) ).
tcf(c_134200,plain,
sK5(sK8,sK9) = sK11(sK8),
inference(superposition,[status(thm)],[c_129767,c_130065]) ).
tcf(c_134241,plain,
sK4(sK8) = sK11(sK8),
inference(superposition,[status(thm)],[c_130288,c_130065]) ).
tcf(c_134635,plain,
sK5(sK8,sK9) = sK4(sK8),
inference(light_normalisation,[status(thm)],[c_134200,c_134241]) ).
tcf(c_139332,plain,
s(sK12(sK9,s(sK10))) = sK9,
inference(global_subsumption_just,[status(thm)],[c_130007,c_2356,c_55145,c_129770]) ).
tcf(c_139342,plain,
sK12(sK9,s(sK10)) = sK4(sK9),
inference(superposition,[status(thm)],[c_139332,c_132042]) ).
tcf(c_139410,plain,
( '@<_succeeds'(sK4(sK9),sK13(sK9,s(sK10)))
| ( '0' = sK9 )
| ~ '@<_succeeds'(sK9,s(sK10)) ),
inference(superposition,[status(thm)],[c_139342,c_77]) ).
tcf(c_139412,plain,
'@<_succeeds'(sK4(sK9),sK13(sK9,s(sK10))),
inference(forward_subsumption_resolution,[status(thm)],[c_139410,c_132037,c_130004]) ).
tcf(c_139425,plain,
s(sK11(sK13(sK9,s(sK10)))) = sK13(sK9,s(sK10)),
inference(superposition,[status(thm)],[c_139412,c_69]) ).
tcf(c_142560,plain,
'@<_succeeds'('0',sK13(sK9,s(sK10))),
inference(superposition,[status(thm)],[c_139425,c_72]) ).
tcf(c_143048,plain,
s(sK13(sK9,s(sK10))) = s(sK10),
inference(global_subsumption_just,[status(thm)],[c_130006,c_2355,c_55145,c_129770]) ).
tcf(c_147470,plain,
sK13(sK9,s(sK10)) = sK11(s(sK10)),
inference(superposition,[status(thm)],[c_143048,c_146289]) ).
tcf(c_147599,plain,
'@<_succeeds'('0',sK11(s(sK10))),
inference(demodulation,[status(thm)],[c_142560,c_147470]) ).
tcf(c_147601,plain,
'@<_succeeds'(sK4(sK9),sK11(s(sK10))),
inference(demodulation,[status(thm)],[c_139412,c_147470]) ).
tcf(c_147614,plain,
'@<_succeeds'('0',sK10),
inference(demodulation,[status(thm)],[c_147599,c_146289]) ).
tcf(c_147623,plain,
s(sK11(sK10)) = sK10,
inference(superposition,[status(thm)],[c_147614,c_69]) ).
tcf(c_147976,plain,
! [X0: $i] :
( '@<_succeeds'(s(X0),sK10)
| ~ '@<_succeeds'(X0,sK11(sK10)) ),
inference(superposition,[status(thm)],[c_147623,c_71]) ).
tcf(c_148166,plain,
'@<_succeeds'(sK4(sK9),sK10),
inference(demodulation,[status(thm)],[c_147601,c_146289]) ).
tcf(c_160425,plain,
s(sK6(sK8,sK9)) = sK9,
inference(global_subsumption_just,[status(thm)],[c_948,c_94310,c_129770]) ).
tcf(c_160448,plain,
sK6(sK8,sK9) = sK4(sK9),
inference(superposition,[status(thm)],[c_160425,c_132042]) ).
tcf(c_193863,plain,
! [X0: $i] :
( ~ '@<_succeeds'(sK6(sK8,sK9),s(X0))
| '@<_succeeds'(sK5(sK8,sK9),X0) ),
inference(global_subsumption_just,[status(thm)],[c_952,c_952,c_125804]) ).
tcf(c_193864,plain,
! [X0: $i] :
( '@<_succeeds'(sK5(sK8,sK9),X0)
| ~ '@<_succeeds'(sK6(sK8,sK9),s(X0)) ),
inference(renaming,[status(thm)],[c_193863]) ).
tcf(c_193866,plain,
! [X0: $i] :
( '@<_succeeds'(sK4(sK8),X0)
| ~ '@<_succeeds'(sK4(sK9),s(X0)) ),
inference(light_normalisation,[status(thm)],[c_193864,c_134635,c_160448]) ).
tcf(c_193894,plain,
( '@<_succeeds'(sK4(sK8),sK11(sK10))
| ~ '@<_succeeds'(sK4(sK9),sK10) ),
inference(superposition,[status(thm)],[c_147623,c_193866]) ).
tcf(c_193970,plain,
'@<_succeeds'(sK4(sK8),sK11(sK10)),
inference(forward_subsumption_resolution,[status(thm)],[c_193894,c_148166]) ).
tcf(c_194535,plain,
'@<_succeeds'(s(sK4(sK8)),sK10),
inference(superposition,[status(thm)],[c_193970,c_147976]) ).
tcf(c_194536,plain,
'@<_succeeds'(sK8,sK10),
inference(light_normalisation,[status(thm)],[c_194535,c_130288]) ).
tcf(c_194537,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_194536,c_104590]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX040+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.16/0.41 % Computer : n006.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Thu Sep 24 23:21:11 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.16/0.47 Running first-order theorem proving
% 0.16/0.47 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.49
% 0.16/0.49 % ======== iProver multi-core TPTP/SMT =========
% 0.16/0.49
% 0.16/0.49 % Detected problem language: tptp
% 0.23/0.51 % Proving...
% 68.28/17.75 % SZS status Started for theBenchmark.p
% 68.28/17.75 % SZS status Theorem for theBenchmark.p
% 68.28/17.75
% 68.28/17.75 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 68.28/17.75
% 68.28/17.75 % ------ iProver source info
% 68.28/17.75
% 68.28/17.75 % git: date: 2026-07-19 20:42:38 +0200
% 68.28/17.75 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 68.28/17.75 % git: non_committed_changes: false
% 68.28/17.75
% 68.28/17.75 % ------ Parsing...
% 68.28/17.75 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 68.28/17.75
% 68.28/17.75 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 68.28/17.75
% 68.28/17.75 % ------ Preprocessing... gs_s sp: 10 0s gs_e snvd_s sp: 0 0s snvd_e %
% 68.28/17.75
% 68.28/17.75 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 68.28/17.75 % ------ Proving...
% 68.28/17.75 % ------ Problem Properties
% 68.28/17.75
% 68.28/17.75 %
% 68.28/17.75 % clauses 31
% 68.28/17.75 % conjectures 3
% 68.28/17.75 % EPR 5
% 68.28/17.75 % Horn 14
% 68.28/17.75 % unary 6
% 68.28/17.75 % binary 5
% 68.28/17.75 % lits 79
% 68.28/17.75 % lits eq 29
% 68.28/17.75 % fd_pure 0
% 68.28/17.75 % fd_pseudo 0
% 68.28/17.75 % fd_cond 2
% 68.28/17.75 % fd_pseudo_cond 1
% 68.28/17.75 % AC symbols 0
% 68.28/17.75
% 68.28/17.75 % ------ Schedule dynamic 5 is on
% 68.28/17.75
% 68.28/17.75 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 68.28/17.75
% 68.28/17.75
% 68.28/17.75 % ------
% 68.28/17.75 % Current options:
% 68.28/17.75 % ------
% 68.28/17.75
% 68.28/17.75
% 68.28/17.75 %
% 68.28/17.75
% 68.28/17.75 % ------ Proving...
% 68.28/17.75 % Proof_search_loop: time out after: 4454 full_loop iterations
% 68.28/17.75
% 68.28/17.75 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 68.28/17.75
% 68.28/17.75
% 68.28/17.75 % ------
% 68.28/17.75 % Current options:
% 68.28/17.75 % ------
% 68.28/17.75
% 68.28/17.75
% 68.28/17.75 %
% 68.28/17.75
% 68.28/17.75 % ------ Proving...
% 68.28/17.75 %
% 68.28/17.75
% 68.28/17.75 % SZS status Theorem for theBenchmark.p
% 68.28/17.75
% 68.28/17.75 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 68.28/17.76
% 68.28/17.76
%------------------------------------------------------------------------------