%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV111+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 : Thu Sep 24 02:46:40 PM UTC 2026
% Result : Theorem 277.00s 35.34s
% Output : CNFRefutation 277.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 25
% Syntax : Number of formulae : 262 ( 67 unt; 4 def)
% Number of atoms : 1206 ( 167 equ)
% Maximal formula atoms : 62 ( 4 avg)
% Number of connectives : 1496 ( 552 ~; 689 |; 215 &)
% ( 8 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 5 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 25 con; 0-3 aty)
% Number of variables : 400 ( 380 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X,Y] :
( lt(X,Y)
<=> gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] :
( ( X != Y
& leq(X,Y) )
=> gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] :
( leq(X,pred(Y))
<=> gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y] :
( leq(X,Y)
<=> gt(succ(Y),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
succ(tptp_minus_1) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X] : plus(X,n1) = succ(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X] : plus(n1,X) = succ(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X] : plus(X,n3) = succ(succ(succ(X))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X] : plus(n3,X) = succ(succ(succ(X))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X] : plus(n4,X) = succ(succ(succ(succ(X)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [X] : plus(n5,X) = succ(succ(succ(succ(succ(X))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X] : pred(succ(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X] : succ(pred(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [X,Y] :
( leq(succ(X),succ(Y))
<=> leq(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [X,Y] :
( leq(succ(X),Y)
=> gt(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
( ( ! [I] :
( ( leq(I,minus(pv57,n1))
& leq(n0,I) )
=> ! [J] :
( ( leq(J,minus(n6,n1))
& leq(n0,J) )
=> a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I) ) )
& ! [G,H] :
( ( leq(H,minus(n6,n1))
& leq(G,minus(n6,n1))
& leq(n0,H)
& leq(n0,G) )
=> ( ( lt(G,pv57)
=> a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G) )
& ( ( G = pv57
& lt(H,plus(n1,minus(n6,n1))) )
=> a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G) ) ) )
& ! [E,F] :
( ( leq(F,minus(n6,n1))
& leq(E,minus(n6,n1))
& leq(n0,F)
& leq(n0,E) )
=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) )
& ! [C,D] :
( ( leq(D,minus(n3,n1))
& leq(C,minus(n3,n1))
& leq(n0,D)
& leq(n0,C) )
=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) )
& ! [A,B] :
( ( leq(B,minus(n6,n1))
& leq(A,minus(n6,n1))
& leq(n0,B)
& leq(n0,A) )
=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) )
& leq(pv57,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv57)
& leq(n0,pv5) )
=> ( ! [S] :
( ( leq(S,minus(pv57,n1))
& leq(n0,S) )
=> ! [T] :
( ( leq(T,minus(n6,n1))
& leq(n0,T) )
=> a_select3(id_ds1_filter,S,T) = a_select3(id_ds1_filter,T,S) ) )
& ! [Q,R] :
( ( leq(R,minus(n6,n1))
& leq(Q,pv57)
& leq(n0,R)
& leq(n0,Q) )
=> a_select3(id_ds1_filter,Q,R) = a_select3(id_ds1_filter,R,Q) )
& ! [O,P] :
( ( leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
=> a_select3(pminus_ds1_filter,O,P) = a_select3(pminus_ds1_filter,P,O) )
& ! [M,N] :
( ( leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
=> a_select3(r_ds1_filter,M,N) = a_select3(r_ds1_filter,N,M) )
& ! [K,L] :
( ( leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
=> a_select3(q_ds1_filter,K,L) = a_select3(q_ds1_filter,L,K) )
& leq(pv57,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv57)
& leq(n0,pv5) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( ! [I] :
( ( leq(I,minus(pv57,n1))
& leq(n0,I) )
=> ! [J] :
( ( leq(J,minus(n6,n1))
& leq(n0,J) )
=> a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I) ) )
& ! [G,H] :
( ( leq(H,minus(n6,n1))
& leq(G,minus(n6,n1))
& leq(n0,H)
& leq(n0,G) )
=> ( ( lt(G,pv57)
=> a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G) )
& ( ( G = pv57
& lt(H,plus(n1,minus(n6,n1))) )
=> a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G) ) ) )
& ! [E,F] :
( ( leq(F,minus(n6,n1))
& leq(E,minus(n6,n1))
& leq(n0,F)
& leq(n0,E) )
=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) )
& ! [C,D] :
( ( leq(D,minus(n3,n1))
& leq(C,minus(n3,n1))
& leq(n0,D)
& leq(n0,C) )
=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) )
& ! [A,B] :
( ( leq(B,minus(n6,n1))
& leq(A,minus(n6,n1))
& leq(n0,B)
& leq(n0,A) )
=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) )
& leq(pv57,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv57)
& leq(n0,pv5) )
=> ( ! [S] :
( ( leq(S,minus(pv57,n1))
& leq(n0,S) )
=> ! [T] :
( ( leq(T,minus(n6,n1))
& leq(n0,T) )
=> a_select3(id_ds1_filter,S,T) = a_select3(id_ds1_filter,T,S) ) )
& ! [Q,R] :
( ( leq(R,minus(n6,n1))
& leq(Q,pv57)
& leq(n0,R)
& leq(n0,Q) )
=> a_select3(id_ds1_filter,Q,R) = a_select3(id_ds1_filter,R,Q) )
& ! [O,P] :
( ( leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
=> a_select3(pminus_ds1_filter,O,P) = a_select3(pminus_ds1_filter,P,O) )
& ! [M,N] :
( ( leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
=> a_select3(r_ds1_filter,M,N) = a_select3(r_ds1_filter,N,M) )
& ! [K,L] :
( ( leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
=> a_select3(q_ds1_filter,K,L) = a_select3(q_ds1_filter,L,K) )
& leq(pv57,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv57)
& leq(n0,pv5) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f100,axiom,
succ(succ(succ(succ(succ(succ(n0)))))) = n6,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,axiom,
succ(n0) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,axiom,
succ(succ(n0)) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,axiom,
succ(succ(succ(n0))) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,plain,
! [X,Y] :
( ( ~ gt(Y,X)
| lt(X,Y) )
& ( gt(Y,X)
| ~ lt(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f114,plain,
( ! [X,Y] :
( ~ gt(Y,X)
| lt(X,Y) )
& ! [X,Y] :
( gt(Y,X)
| ~ lt(X,Y) ) ),
inference(miniscoping,[status(thm)],[f113]) ).
fof(f116,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| lt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f123,plain,
! [X,Y] :
( gt(Y,X)
| X = Y
| ~ leq(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f124,plain,
! [X0,X1] :
( gt(X1,X0)
| X0 = X1
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
! [X,Y] :
( ( ~ gt(Y,X)
| leq(X,pred(Y)) )
& ( gt(Y,X)
| ~ leq(X,pred(Y)) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f126,plain,
( ! [X,Y] :
( ~ gt(Y,X)
| leq(X,pred(Y)) )
& ! [X,Y] :
( gt(Y,X)
| ~ leq(X,pred(Y)) ) ),
inference(miniscoping,[status(thm)],[f125]) ).
fof(f128,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,pred(X1)) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f132,plain,
! [X,Y] :
( ( ~ gt(succ(Y),X)
| leq(X,Y) )
& ( gt(succ(Y),X)
| ~ leq(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f13]) ).
fof(f133,plain,
( ! [X,Y] :
( ~ gt(succ(Y),X)
| leq(X,Y) )
& ! [X,Y] :
( gt(succ(Y),X)
| ~ leq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f132]) ).
fof(f134,plain,
! [X0,X1] :
( gt(succ(X1),X0)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( ~ gt(succ(X1),X0)
| leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f216,plain,
succ(tptp_minus_1) = n0,
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f217,plain,
! [X0] : plus(X0,n1) = succ(X0),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f218,plain,
! [X0] : plus(n1,X0) = succ(X0),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f221,plain,
! [X0] : plus(X0,n3) = succ(succ(succ(X0))),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f222,plain,
! [X0] : plus(n3,X0) = succ(succ(succ(X0))),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f224,plain,
! [X0] : plus(n4,X0) = succ(succ(succ(succ(X0)))),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f226,plain,
! [X0] : plus(n5,X0) = succ(succ(succ(succ(succ(X0))))),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f227,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f228,plain,
! [X0] : pred(succ(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f229,plain,
! [X0] : succ(pred(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f230,plain,
! [X,Y] :
( ( ~ leq(X,Y)
| leq(succ(X),succ(Y)) )
& ( leq(X,Y)
| ~ leq(succ(X),succ(Y)) ) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f231,plain,
( ! [X,Y] :
( ~ leq(X,Y)
| leq(succ(X),succ(Y)) )
& ! [X,Y] :
( leq(X,Y)
| ~ leq(succ(X),succ(Y)) ) ),
inference(miniscoping,[status(thm)],[f230]) ).
fof(f233,plain,
! [X0,X1] :
( ~ leq(X0,X1)
| leq(succ(X0),succ(X1)) ),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f234,plain,
! [X,Y] :
( gt(Y,X)
| ~ leq(succ(X),Y) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f235,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(succ(X0),X1) ),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f261,plain,
( ( ? [S] :
( ? [T] :
( a_select3(id_ds1_filter,S,T) != a_select3(id_ds1_filter,T,S)
& leq(T,minus(n6,n1))
& leq(n0,T) )
& leq(S,minus(pv57,n1))
& leq(n0,S) )
| ? [Q,R] :
( a_select3(id_ds1_filter,Q,R) != a_select3(id_ds1_filter,R,Q)
& leq(R,minus(n6,n1))
& leq(Q,pv57)
& leq(n0,R)
& leq(n0,Q) )
| ? [O,P] :
( a_select3(pminus_ds1_filter,O,P) != a_select3(pminus_ds1_filter,P,O)
& leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
| ? [M,N] :
( a_select3(r_ds1_filter,M,N) != a_select3(r_ds1_filter,N,M)
& leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
| ? [K,L] :
( a_select3(q_ds1_filter,K,L) != a_select3(q_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) )
& ! [I] :
( ! [J] :
( a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I)
| ~ leq(J,minus(n6,n1))
| ~ leq(n0,J) )
| ~ leq(I,minus(pv57,n1))
| ~ leq(n0,I) )
& ! [G,H] :
( ( ( a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G)
| ~ lt(G,pv57) )
& ( a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G)
| G != pv57
| ~ lt(H,plus(n1,minus(n6,n1))) ) )
| ~ leq(H,minus(n6,n1))
| ~ leq(G,minus(n6,n1))
| ~ leq(n0,H)
| ~ leq(n0,G) )
& ! [E,F] :
( a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E)
| ~ leq(F,minus(n6,n1))
| ~ leq(E,minus(n6,n1))
| ~ leq(n0,F)
| ~ leq(n0,E) )
& ! [C,D] :
( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C)
| ~ leq(D,minus(n3,n1))
| ~ leq(C,minus(n3,n1))
| ~ leq(n0,D)
| ~ leq(n0,C) )
& ! [A,B] :
( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A)
| ~ leq(B,minus(n6,n1))
| ~ leq(A,minus(n6,n1))
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv57,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv57)
& leq(n0,pv5) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f262,definition,
! [K,L] :
( sP3_prd(L,K)
<=> ( a_select3(q_ds1_filter,K,L) != a_select3(q_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f263,definition,
! [M,N] :
( sP4_prd(N,M)
<=> ( a_select3(r_ds1_filter,M,N) != a_select3(r_ds1_filter,N,M)
& leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f264,definition,
! [O,P] :
( sP5_prd(P,O)
<=> ( a_select3(pminus_ds1_filter,O,P) != a_select3(pminus_ds1_filter,P,O)
& leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f265,definition,
! [Q,R] :
( sP6_prd(R,Q)
<=> ( a_select3(id_ds1_filter,Q,R) != a_select3(id_ds1_filter,R,Q)
& leq(R,minus(n6,n1))
& leq(Q,pv57)
& leq(n0,R)
& leq(n0,Q) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f266,plain,
( ( ? [S] :
( ? [T] :
( a_select3(id_ds1_filter,S,T) != a_select3(id_ds1_filter,T,S)
& leq(T,minus(n6,n1))
& leq(n0,T) )
& leq(S,minus(pv57,n1))
& leq(n0,S) )
| ? [Q,R] : sP6_prd(R,Q)
| ? [O,P] : sP5_prd(P,O)
| ? [M,N] : sP4_prd(N,M)
| ? [K,L] : sP3_prd(L,K)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) )
& ! [I] :
( ! [J] :
( a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I)
| ~ leq(J,minus(n6,n1))
| ~ leq(n0,J) )
| ~ leq(I,minus(pv57,n1))
| ~ leq(n0,I) )
& ! [G,H] :
( ( ( a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G)
| ~ lt(G,pv57) )
& ( a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G)
| G != pv57
| ~ lt(H,plus(n1,minus(n6,n1))) ) )
| ~ leq(H,minus(n6,n1))
| ~ leq(G,minus(n6,n1))
| ~ leq(n0,H)
| ~ leq(n0,G) )
& ! [E,F] :
( a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E)
| ~ leq(F,minus(n6,n1))
| ~ leq(E,minus(n6,n1))
| ~ leq(n0,F)
| ~ leq(n0,E) )
& ! [C,D] :
( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C)
| ~ leq(D,minus(n3,n1))
| ~ leq(C,minus(n3,n1))
| ~ leq(n0,D)
| ~ leq(n0,C) )
& ! [A,B] :
( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A)
| ~ leq(B,minus(n6,n1))
| ~ leq(A,minus(n6,n1))
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv57,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv57)
& leq(n0,pv5) ),
inference(formula_renaming,[status(thm)],[f261,f265,f264,f263,f262]) ).
fof(f267,plain,
( ( ( a_select3(id_ds1_filter,sK31_skl,sK32_skl) != a_select3(id_ds1_filter,sK32_skl,sK31_skl)
& leq(sK32_skl,minus(n6,n1))
& leq(n0,sK32_skl)
& leq(sK31_skl,minus(pv57,n1))
& leq(n0,sK31_skl) )
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) )
& ! [I] :
( ! [J] :
( a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I)
| ~ leq(J,minus(n6,n1))
| ~ leq(n0,J) )
| ~ leq(I,minus(pv57,n1))
| ~ leq(n0,I) )
& ! [G,H] :
( ( ( a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G)
| ~ lt(G,pv57) )
& ( a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G)
| G != pv57
| ~ lt(H,plus(n1,minus(n6,n1))) ) )
| ~ leq(H,minus(n6,n1))
| ~ leq(G,minus(n6,n1))
| ~ leq(n0,H)
| ~ leq(n0,G) )
& ! [E,F] :
( a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E)
| ~ leq(F,minus(n6,n1))
| ~ leq(E,minus(n6,n1))
| ~ leq(n0,F)
| ~ leq(n0,E) )
& ! [C,D] :
( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C)
| ~ leq(D,minus(n3,n1))
| ~ leq(C,minus(n3,n1))
| ~ leq(n0,D)
| ~ leq(n0,C) )
& ! [A,B] :
( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A)
| ~ leq(B,minus(n6,n1))
| ~ leq(A,minus(n6,n1))
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv57,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv57)
& leq(n0,pv5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl,sK29_skl,sK30_skl,sK31_skl,sK32_skl]),skolemize(K,sK23_skl),skolemize(L,sK24_skl),skolemize(M,sK25_skl),skolemize(N,sK26_skl),skolemize(O,sK27_skl),skolemize(P,sK28_skl),skolemize(Q,sK29_skl),skolemize(R,sK30_skl),skolemize(S,sK31_skl),skolemize(T,sK32_skl)],[f266]) ).
fof(f268,plain,
leq(n0,pv5),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f269,plain,
leq(n0,pv57),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f270,plain,
leq(pv5,minus(n999,n1)),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f271,plain,
leq(pv57,minus(n6,n1)),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f272,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f273,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,minus(n3,n1))
| ~ leq(X0,minus(n3,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f274,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f275,plain,
! [X0,X1] :
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| X0 != pv57
| ~ lt(X1,plus(n1,minus(n6,n1)))
| ~ leq(X1,minus(n6,n1))
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f277,plain,
! [X0,X1] :
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(X0,minus(pv57,n1))
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f278,plain,
( leq(n0,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f279,plain,
( leq(sK31_skl,minus(pv57,n1))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f280,plain,
( leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f281,plain,
( leq(sK32_skl,minus(n6,n1))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f282,plain,
( a_select3(id_ds1_filter,sK31_skl,sK32_skl) != a_select3(id_ds1_filter,sK32_skl,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f335,plain,
succ(succ(succ(succ(succ(succ(n0)))))) = n6,
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f336,plain,
succ(n0) = n1,
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f337,plain,
succ(succ(n0)) = n2,
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f338,plain,
succ(succ(succ(n0))) = n3,
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f367,plain,
! [K,L] :
( ( a_select3(q_ds1_filter,K,L) = a_select3(q_ds1_filter,L,K)
| ~ leq(L,minus(n6,n1))
| ~ leq(K,minus(n6,n1))
| ~ leq(n0,L)
| ~ leq(n0,K)
| sP3_prd(L,K) )
& ( ( a_select3(q_ds1_filter,K,L) != a_select3(q_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
| ~ sP3_prd(L,K) ) ),
inference(NNF_transformation,[status(thm)],[f262]) ).
fof(f368,plain,
( ! [K,L] :
( a_select3(q_ds1_filter,K,L) = a_select3(q_ds1_filter,L,K)
| ~ leq(L,minus(n6,n1))
| ~ leq(K,minus(n6,n1))
| ~ leq(n0,L)
| ~ leq(n0,K)
| sP3_prd(L,K) )
& ! [K,L] :
( ( a_select3(q_ds1_filter,K,L) != a_select3(q_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
| ~ sP3_prd(L,K) ) ),
inference(miniscoping,[status(thm)],[f367]) ).
fof(f369,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f370,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f371,plain,
! [X0,X1] :
( leq(X1,minus(n6,n1))
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f372,plain,
! [X0,X1] :
( leq(X0,minus(n6,n1))
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f373,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X1,X0) != a_select3(q_ds1_filter,X0,X1)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f375,plain,
! [M,N] :
( ( a_select3(r_ds1_filter,M,N) = a_select3(r_ds1_filter,N,M)
| ~ leq(N,minus(n3,n1))
| ~ leq(M,minus(n3,n1))
| ~ leq(n0,N)
| ~ leq(n0,M)
| sP4_prd(N,M) )
& ( ( a_select3(r_ds1_filter,M,N) != a_select3(r_ds1_filter,N,M)
& leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
| ~ sP4_prd(N,M) ) ),
inference(NNF_transformation,[status(thm)],[f263]) ).
fof(f376,plain,
( ! [M,N] :
( a_select3(r_ds1_filter,M,N) = a_select3(r_ds1_filter,N,M)
| ~ leq(N,minus(n3,n1))
| ~ leq(M,minus(n3,n1))
| ~ leq(n0,N)
| ~ leq(n0,M)
| sP4_prd(N,M) )
& ! [M,N] :
( ( a_select3(r_ds1_filter,M,N) != a_select3(r_ds1_filter,N,M)
& leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
| ~ sP4_prd(N,M) ) ),
inference(miniscoping,[status(thm)],[f375]) ).
fof(f377,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f378,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f379,plain,
! [X0,X1] :
( leq(X1,minus(n3,n1))
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f380,plain,
! [X0,X1] :
( leq(X0,minus(n3,n1))
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f381,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X1,X0) != a_select3(r_ds1_filter,X0,X1)
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f383,plain,
! [O,P] :
( ( a_select3(pminus_ds1_filter,O,P) = a_select3(pminus_ds1_filter,P,O)
| ~ leq(P,minus(n6,n1))
| ~ leq(O,minus(n6,n1))
| ~ leq(n0,P)
| ~ leq(n0,O)
| sP5_prd(P,O) )
& ( ( a_select3(pminus_ds1_filter,O,P) != a_select3(pminus_ds1_filter,P,O)
& leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
| ~ sP5_prd(P,O) ) ),
inference(NNF_transformation,[status(thm)],[f264]) ).
fof(f384,plain,
( ! [O,P] :
( a_select3(pminus_ds1_filter,O,P) = a_select3(pminus_ds1_filter,P,O)
| ~ leq(P,minus(n6,n1))
| ~ leq(O,minus(n6,n1))
| ~ leq(n0,P)
| ~ leq(n0,O)
| sP5_prd(P,O) )
& ! [O,P] :
( ( a_select3(pminus_ds1_filter,O,P) != a_select3(pminus_ds1_filter,P,O)
& leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
| ~ sP5_prd(P,O) ) ),
inference(miniscoping,[status(thm)],[f383]) ).
fof(f385,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f386,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f387,plain,
! [X0,X1] :
( leq(X1,minus(n6,n1))
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f388,plain,
! [X0,X1] :
( leq(X0,minus(n6,n1))
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f389,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X1,X0) != a_select3(pminus_ds1_filter,X0,X1)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f391,plain,
! [Q,R] :
( ( a_select3(id_ds1_filter,Q,R) = a_select3(id_ds1_filter,R,Q)
| ~ leq(R,minus(n6,n1))
| ~ leq(Q,pv57)
| ~ leq(n0,R)
| ~ leq(n0,Q)
| sP6_prd(R,Q) )
& ( ( a_select3(id_ds1_filter,Q,R) != a_select3(id_ds1_filter,R,Q)
& leq(R,minus(n6,n1))
& leq(Q,pv57)
& leq(n0,R)
& leq(n0,Q) )
| ~ sP6_prd(R,Q) ) ),
inference(NNF_transformation,[status(thm)],[f265]) ).
fof(f392,plain,
( ! [Q,R] :
( a_select3(id_ds1_filter,Q,R) = a_select3(id_ds1_filter,R,Q)
| ~ leq(R,minus(n6,n1))
| ~ leq(Q,pv57)
| ~ leq(n0,R)
| ~ leq(n0,Q)
| sP6_prd(R,Q) )
& ! [Q,R] :
( ( a_select3(id_ds1_filter,Q,R) != a_select3(id_ds1_filter,R,Q)
& leq(R,minus(n6,n1))
& leq(Q,pv57)
& leq(n0,R)
& leq(n0,Q) )
| ~ sP6_prd(R,Q) ) ),
inference(miniscoping,[status(thm)],[f391]) ).
fof(f393,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP6_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f394,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP6_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f395,plain,
! [X0,X1] :
( leq(X1,pv57)
| ~ sP6_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f396,plain,
! [X0,X1] :
( leq(X0,minus(n6,n1))
| ~ sP6_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f397,plain,
! [X0,X1] :
( a_select3(id_ds1_filter,X1,X0) != a_select3(id_ds1_filter,X0,X1)
| ~ sP6_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f409,plain,
! [X0] :
( a_select3(id_ds1_filter,pv57,X0) = a_select3(id_ds1_filter,X0,pv57)
| ~ lt(X0,plus(n1,minus(n6,n1)))
| ~ leq(X0,minus(n6,n1))
| ~ leq(pv57,minus(n6,n1))
| ~ leq(n0,X0)
| ~ leq(n0,pv57) ),
inference(destructive_equality_resolution,[status(thm)],[f275]) ).
fof(f672,plain,
! [X0] : plus(succ(X0),n3) = succ(plus(X0,n3)),
inference(paramodulation,[status(thm)],[f221,f221]) ).
fof(f676,plain,
plus(tptp_minus_1,n3) = succ(succ(n0)),
inference(paramodulation,[status(thm)],[f216,f221]) ).
fof(f680,plain,
plus(tptp_minus_1,n3) = succ(n1),
inference(forward_demodulation,[status(thm)],[f336,f676]) ).
fof(f681,plain,
! [X0] : plus(n3,X0) = plus(X0,n3),
inference(paramodulation,[status(thm)],[f221,f222]) ).
fof(f766,plain,
! [X0,X1] :
( lt(X0,succ(X1))
| ~ leq(X0,X1) ),
inference(resolution,[status(thm)],[f134,f116]) ).
fof(f796,plain,
! [X0] :
( a_select3(id_ds1_filter,pv57,X0) = a_select3(id_ds1_filter,X0,pv57)
| ~ lt(X0,succ(minus(n6,n1)))
| ~ leq(X0,minus(n6,n1))
| ~ leq(pv57,minus(n6,n1))
| ~ leq(n0,X0)
| ~ leq(n0,pv57) ),
inference(forward_demodulation,[status(thm)],[f218,f409]) ).
fof(f797,plain,
! [X0] :
( a_select3(id_ds1_filter,pv57,X0) = a_select3(id_ds1_filter,X0,pv57)
| ~ lt(X0,succ(minus(n6,n1)))
| ~ leq(X0,minus(n6,n1))
| ~ leq(pv57,minus(n6,n1))
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f796,f269]) ).
fof(f819,plain,
! [X0] : plus(n4,X0) = plus(n3,succ(X0)),
inference(forward_demodulation,[status(thm)],[f222,f224]) ).
fof(f896,plain,
plus(n3,n0) = n3,
inference(forward_demodulation,[status(thm)],[f222,f338]) ).
fof(f937,plain,
! [X0] : plus(n5,X0) = plus(n3,succ(succ(X0))),
inference(forward_demodulation,[status(thm)],[f222,f226]) ).
fof(f938,plain,
! [X0] : plus(n5,X0) = plus(n4,succ(X0)),
inference(forward_demodulation,[status(thm)],[f819,f937]) ).
fof(f1028,plain,
( leq(n0,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv57) ),
inference(forward_subsumption_resolution,[status(thm)],[f278,f268]) ).
fof(f1029,plain,
( leq(n0,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv57) ),
inference(resolution,[status(thm)],[f1028,f271]) ).
fof(f1032,plain,
( leq(n0,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,minus(n999,n1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1029,f269]) ).
fof(f1039,plain,
! [X0,X1] :
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| ~ leq(X1,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(X0,pred(pv57))
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f227,f277]) ).
fof(f1040,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,pred(n3))
| ~ leq(X0,minus(n3,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f227,f273]) ).
fof(f1043,plain,
! [X0] :
( a_select3(id_ds1_filter,pv57,X0) = a_select3(id_ds1_filter,X0,pv57)
| ~ lt(X0,succ(pred(n6)))
| ~ leq(X0,minus(n6,n1))
| ~ leq(pv57,minus(n6,n1))
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f227,f797]) ).
fof(f1044,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f227,f274]) ).
fof(f1045,plain,
! [X0,X1] :
( leq(X0,pred(n6))
| ~ sP3_prd(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f227,f372]) ).
fof(f1046,plain,
! [X0,X1] :
( leq(X1,pred(n6))
| ~ sP3_prd(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f227,f371]) ).
fof(f1048,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(backward_demodulation,[status(thm)],[f227,f272]) ).
fof(f1049,plain,
leq(pv57,pred(n6)),
inference(backward_demodulation,[status(thm)],[f227,f271]) ).
fof(f1051,plain,
leq(pv5,pred(n999)),
inference(backward_demodulation,[status(thm)],[f227,f270]) ).
fof(f1053,plain,
! [X0,X1] :
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(n0,X1)
| ~ leq(X0,pred(pv57))
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f1039]) ).
fof(f1054,plain,
! [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| ~ leq(X1,pred(n3))
| ~ leq(X0,pred(n3))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f1040]) ).
fof(f1058,plain,
! [X0] :
( a_select3(id_ds1_filter,pv57,X0) = a_select3(id_ds1_filter,X0,pv57)
| ~ lt(X0,succ(pred(n6)))
| ~ leq(X0,minus(n6,n1))
| ~ leq(pv57,pred(n6))
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f1043]) ).
fof(f1059,plain,
! [X0] :
( a_select3(id_ds1_filter,pv57,X0) = a_select3(id_ds1_filter,X0,pv57)
| ~ lt(X0,succ(pred(n6)))
| ~ leq(X0,pred(n6))
| ~ leq(pv57,pred(n6))
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f1058]) ).
fof(f1060,plain,
! [X0] :
( a_select3(id_ds1_filter,pv57,X0) = a_select3(id_ds1_filter,X0,pv57)
| ~ lt(X0,n6)
| ~ leq(X0,pred(n6))
| ~ leq(pv57,pred(n6))
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f229,f1059]) ).
fof(f1061,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f1044]) ).
fof(f1062,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,pred(n6))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f1048]) ).
fof(f1063,plain,
succ(n1) = n2,
inference(forward_demodulation,[status(thm)],[f336,f337]) ).
fof(f1070,plain,
! [X0] :
( ~ gt(n2,X0)
| leq(X0,n1) ),
inference(paramodulation,[status(thm)],[f1063,f135]) ).
fof(f1167,plain,
( leq(sK31_skl,minus(pv57,n1))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(forward_demodulation,[status(thm)],[f227,f279]) ).
fof(f1168,plain,
( leq(sK31_skl,minus(pv57,n1))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(forward_demodulation,[status(thm)],[f227,f1167]) ).
fof(f1169,plain,
( leq(sK31_skl,pred(pv57))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(forward_demodulation,[status(thm)],[f227,f1168]) ).
fof(f1170,plain,
( leq(sK31_skl,pred(pv57))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57) ),
inference(forward_subsumption_resolution,[status(thm)],[f1169,f268]) ).
fof(f1178,plain,
( leq(sK31_skl,pred(pv57))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6))
| ~ leq(n0,pv57) ),
inference(backward_subsumption_resolution,[status(thm)],[f1170,f1051]) ).
fof(f1183,plain,
( leq(sK31_skl,pred(pv57))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1178,f269]) ).
fof(f1207,plain,
( leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(forward_demodulation,[status(thm)],[f227,f280]) ).
fof(f1208,plain,
( leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(forward_demodulation,[status(thm)],[f227,f1207]) ).
fof(f1209,plain,
( leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57) ),
inference(forward_subsumption_resolution,[status(thm)],[f1208,f268]) ).
fof(f1210,plain,
( leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57) ),
inference(resolution,[status(thm)],[f1209,f1049]) ).
fof(f1212,plain,
( leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,pred(n999)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1210,f269]) ).
fof(f1214,plain,
( leq(sK32_skl,minus(n6,n1))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(forward_demodulation,[status(thm)],[f227,f281]) ).
fof(f1215,plain,
( leq(sK32_skl,minus(n6,n1))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(forward_demodulation,[status(thm)],[f227,f1214]) ).
fof(f1216,plain,
( leq(sK32_skl,pred(n6))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(forward_demodulation,[status(thm)],[f227,f1215]) ).
fof(f1217,plain,
( leq(sK32_skl,pred(n6))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57) ),
inference(forward_subsumption_resolution,[status(thm)],[f1216,f268]) ).
fof(f1218,plain,
( leq(sK32_skl,pred(n6))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57) ),
inference(resolution,[status(thm)],[f1217,f1049]) ).
fof(f1220,plain,
( leq(sK32_skl,pred(n6))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,pred(n999)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1218,f269]) ).
fof(f1366,plain,
( a_select3(id_ds1_filter,sK31_skl,sK32_skl) != a_select3(id_ds1_filter,sK32_skl,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(forward_demodulation,[status(thm)],[f227,f282]) ).
fof(f1367,plain,
( a_select3(id_ds1_filter,sK31_skl,sK32_skl) != a_select3(id_ds1_filter,sK32_skl,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57)
| ~ leq(n0,pv5) ),
inference(forward_demodulation,[status(thm)],[f227,f1366]) ).
fof(f1368,plain,
( a_select3(id_ds1_filter,sK31_skl,sK32_skl) != a_select3(id_ds1_filter,sK32_skl,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,pred(n6))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57) ),
inference(forward_subsumption_resolution,[status(thm)],[f1367,f268]) ).
fof(f1520,plain,
! [X0,X1] :
( gt(X1,pred(X0))
| ~ leq(X0,X1) ),
inference(paramodulation,[status(thm)],[f229,f235]) ).
fof(f1678,plain,
plus(n3,succ(succ(succ(n0)))) = n6,
inference(forward_demodulation,[status(thm)],[f222,f335]) ).
fof(f1679,plain,
plus(n4,succ(succ(n0))) = n6,
inference(forward_demodulation,[status(thm)],[f819,f1678]) ).
fof(f1680,plain,
plus(n5,succ(n0)) = n6,
inference(forward_demodulation,[status(thm)],[f938,f1679]) ).
fof(f1681,plain,
plus(n5,n1) = n6,
inference(forward_demodulation,[status(thm)],[f336,f1680]) ).
fof(f1683,plain,
succ(n5) = n6,
inference(forward_demodulation,[status(thm)],[f217,f1681]) ).
fof(f1709,plain,
pred(n6) = n5,
inference(paramodulation,[status(thm)],[f1683,f228]) ).
fof(f1726,plain,
( a_select3(id_ds1_filter,sK31_skl,sK32_skl) != a_select3(id_ds1_filter,sK32_skl,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,n5)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv57) ),
inference(backward_demodulation,[status(thm)],[f1709,f1368]) ).
fof(f1729,plain,
leq(pv57,n5),
inference(backward_demodulation,[status(thm)],[f1709,f1049]) ).
fof(f1751,plain,
( a_select3(id_ds1_filter,sK31_skl,sK32_skl) != a_select3(id_ds1_filter,sK32_skl,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,n5)
| ~ leq(pv5,pred(n999)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1726,f269]) ).
fof(f1828,plain,
! [X0,X1] :
( leq(X1,pred(n3))
| ~ sP4_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f379]) ).
fof(f1855,plain,
! [X0,X1] :
( leq(X0,pred(n3))
| ~ sP4_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f380]) ).
fof(f1864,plain,
! [X0,X1] :
( gt(pred(n3),X0)
| ~ sP4_prd(succ(X0),X1) ),
inference(resolution,[status(thm)],[f1855,f235]) ).
fof(f1952,plain,
! [X0,X1] :
( leq(X1,pred(n6))
| ~ sP5_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f387]) ).
fof(f1953,plain,
! [X0,X1] :
( leq(X1,n5)
| ~ sP5_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f1709,f1952]) ).
fof(f1954,plain,
! [X0,X1] :
( leq(X0,pred(n6))
| ~ sP5_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f388]) ).
fof(f1955,plain,
! [X0,X1] :
( leq(X0,n5)
| ~ sP5_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f1709,f1954]) ).
fof(f2172,plain,
! [X0,X1] :
( leq(X0,pred(n6))
| ~ sP6_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f227,f396]) ).
fof(f2173,plain,
! [X0,X1] :
( leq(X0,n5)
| ~ sP6_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f1709,f2172]) ).
fof(f2426,plain,
! [X0,X1] :
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| ~ leq(X1,n5)
| ~ leq(n0,X1)
| ~ leq(X0,pred(pv57))
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f1709,f1053]) ).
fof(f2427,plain,
! [X0,X1] :
( ~ sP6_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(n0,X1)
| ~ leq(X0,pred(pv57))
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f2426,f397]) ).
fof(f2435,plain,
! [X0,X1] :
( ~ sP6_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,pred(pv57))
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2427,f394]) ).
fof(f2654,plain,
! [X0,X1] :
( ~ sP4_prd(X1,X0)
| ~ leq(X1,pred(n3))
| ~ leq(X0,pred(n3))
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f1054,f381]) ).
fof(f2664,plain,
! [X0,X1] :
( ~ sP4_prd(X1,X0)
| ~ leq(X1,pred(n3))
| ~ leq(X0,pred(n3))
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2654,f378]) ).
fof(f2948,plain,
! [X0] :
( a_select3(id_ds1_filter,pv57,X0) = a_select3(id_ds1_filter,X0,pv57)
| ~ lt(X0,n6)
| ~ leq(X0,pred(n6))
| ~ leq(pv57,n5)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f1709,f1060]) ).
fof(f2949,plain,
! [X0] :
( a_select3(id_ds1_filter,pv57,X0) = a_select3(id_ds1_filter,X0,pv57)
| ~ lt(X0,n6)
| ~ leq(X0,n5)
| ~ leq(pv57,n5)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f1709,f2948]) ).
fof(f2950,plain,
! [X0] :
( a_select3(id_ds1_filter,pv57,X0) = a_select3(id_ds1_filter,X0,pv57)
| ~ lt(X0,n6)
| ~ leq(X0,n5)
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2949,f1729]) ).
fof(f2981,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,n5)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f1709,f1061]) ).
fof(f2982,plain,
! [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f1709,f2981]) ).
fof(f2983,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f2982,f389]) ).
fof(f2993,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2983,f386]) ).
fof(f3003,plain,
! [X0,X1] :
( leq(X0,n5)
| ~ sP3_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f1709,f1045]) ).
fof(f3155,plain,
! [X0,X1] :
( leq(X1,n5)
| ~ sP3_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f1709,f1046]) ).
fof(f3218,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(X1,pred(n6))
| ~ leq(X0,n5)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f1709,f1062]) ).
fof(f3219,plain,
! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f1709,f3218]) ).
fof(f3220,plain,
! [X0,X1] :
( ~ sP3_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f3219,f373]) ).
fof(f3230,plain,
! [X0,X1] :
( ~ sP3_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5)
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3220,f370]) ).
fof(f3240,plain,
( leq(sK31_skl,pred(pv57))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,n5) ),
inference(forward_demodulation,[status(thm)],[f1709,f1183]) ).
fof(f3241,plain,
( leq(sK31_skl,pred(pv57))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3240,f1729]) ).
fof(f3506,plain,
( a_select3(id_ds1_filter,sK31_skl,sK32_skl) != a_select3(id_ds1_filter,sK32_skl,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,n5) ),
inference(forward_subsumption_resolution,[status(thm)],[f1751,f1051]) ).
fof(f3508,plain,
( ~ leq(sK32_skl,n5)
| ~ leq(n0,sK32_skl)
| ~ leq(sK31_skl,pred(pv57))
| ~ leq(n0,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv57,n5) ),
inference(resolution,[status(thm)],[f3506,f2426]) ).
fof(f3514,plain,
( ~ leq(sK32_skl,n5)
| ~ leq(n0,sK32_skl)
| ~ leq(sK31_skl,pred(pv57))
| ~ leq(n0,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3508,f1729]) ).
fof(f3618,plain,
plus(tptp_minus_1,n3) = n2,
inference(forward_demodulation,[status(thm)],[f1063,f680]) ).
fof(f3619,plain,
n3 = plus(n0,n3),
inference(paramodulation,[status(thm)],[f896,f681]) ).
fof(f4230,plain,
! [X0,X1] :
( ~ leq(pred(X0),X1)
| leq(X0,succ(X1)) ),
inference(paramodulation,[status(thm)],[f229,f233]) ).
fof(f4233,plain,
! [X0] :
( ~ leq(X0,n1)
| leq(succ(X0),n2) ),
inference(paramodulation,[status(thm)],[f1063,f233]) ).
fof(f4426,plain,
plus(n0,n3) = succ(plus(tptp_minus_1,n3)),
inference(paramodulation,[status(thm)],[f216,f672]) ).
fof(f4441,plain,
n3 = succ(plus(tptp_minus_1,n3)),
inference(forward_demodulation,[status(thm)],[f3619,f4426]) ).
fof(f4442,plain,
n3 = succ(n2),
inference(forward_demodulation,[status(thm)],[f3618,f4441]) ).
fof(f4493,plain,
pred(n3) = n2,
inference(paramodulation,[status(thm)],[f4442,f228]) ).
fof(f4521,plain,
! [X0,X1] :
( leq(X1,n2)
| ~ sP4_prd(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f4493,f1828]) ).
fof(f4937,plain,
! [X0] :
( lt(X0,n6)
| ~ leq(X0,n5) ),
inference(paramodulation,[status(thm)],[f1683,f766]) ).
fof(f5397,plain,
( leq(n0,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,pred(n999)) ),
inference(forward_demodulation,[status(thm)],[f227,f1032]) ).
fof(f5398,plain,
( leq(n0,sK31_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5397,f1051]) ).
fof(f10521,plain,
( leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1212,f1051]) ).
fof(f11270,plain,
( leq(sK32_skl,n5)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,pred(n999)) ),
inference(forward_demodulation,[status(thm)],[f1709,f1220]) ).
fof(f11271,plain,
( leq(sK32_skl,n5)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f11270,f1051]) ).
fof(f13814,plain,
! [X0] :
( a_select3(id_ds1_filter,pv57,X0) = a_select3(id_ds1_filter,X0,pv57)
| ~ leq(X0,n5)
| ~ leq(n0,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2950,f4937]) ).
fof(f13841,plain,
! [X0] :
( ~ sP6_prd(X0,pv57)
| ~ leq(X0,n5)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[f13814,f397]) ).
fof(f13849,plain,
! [X0] :
( ~ sP6_prd(X0,pv57)
| ~ leq(X0,n5) ),
inference(forward_subsumption_resolution,[status(thm)],[f13841,f394]) ).
fof(f17145,plain,
! [X0,X1] :
( gt(n2,X0)
| ~ sP4_prd(succ(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f4493,f1864]) ).
fof(f17157,plain,
! [X0,X1] :
( gt(n2,pred(X0))
| ~ sP4_prd(X0,X1) ),
inference(paramodulation,[status(thm)],[f229,f17145]) ).
fof(f17246,plain,
! [X0] : ~ sP6_prd(X0,pv57),
inference(forward_subsumption_resolution,[status(thm)],[f13849,f2173]) ).
fof(f18807,plain,
! [X0,X1] :
( ~ sP6_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,pred(pv57)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2435,f393]) ).
fof(f18816,plain,
! [X0,X1] :
( ~ gt(pv57,X1)
| ~ sP6_prd(X0,X1)
| ~ leq(X0,n5) ),
inference(resolution,[status(thm)],[f18807,f128]) ).
fof(f18827,plain,
! [X0,X1] :
( ~ gt(pv57,X1)
| ~ sP6_prd(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f18816,f2173]) ).
fof(f20405,plain,
! [X0,X1] :
( ~ sP4_prd(X1,X0)
| ~ leq(X1,pred(n3))
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f4493,f2664]) ).
fof(f20406,plain,
! [X0,X1] :
( ~ sP4_prd(X1,X0)
| ~ leq(X1,n2)
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f4493,f20405]) ).
fof(f20415,plain,
! [X0,X1] :
( ~ sP4_prd(X1,X0)
| ~ leq(X1,n2)
| ~ leq(X0,n2) ),
inference(forward_subsumption_resolution,[status(thm)],[f20406,f377]) ).
fof(f23871,plain,
! [X0,X1] :
( ~ sP5_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5) ),
inference(forward_subsumption_resolution,[status(thm)],[f2993,f385]) ).
fof(f24724,plain,
! [X0,X1] :
( ~ sP3_prd(X1,X0)
| ~ leq(X1,n5)
| ~ leq(X0,n5) ),
inference(forward_subsumption_resolution,[status(thm)],[f3230,f369]) ).
fof(f24908,plain,
! [X0,X1] :
( leq(pred(X0),n1)
| ~ sP4_prd(X0,X1) ),
inference(resolution,[status(thm)],[f17157,f1070]) ).
fof(f25915,plain,
! [X0,X1] :
( leq(X0,n1)
| ~ sP4_prd(succ(X0),X1) ),
inference(paramodulation,[status(thm)],[f228,f24908]) ).
fof(f26279,plain,
( ~ leq(sK32_skl,n5)
| ~ leq(n0,sK32_skl)
| ~ leq(sK31_skl,pred(pv57))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP4_prd(sK26_skl,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3514,f5398]) ).
fof(f30232,plain,
! [X0,X1] :
( ~ sP4_prd(succ(X0),X1)
| ~ leq(X1,n2)
| ~ leq(X0,n1) ),
inference(resolution,[status(thm)],[f4233,f20415]) ).
fof(f30260,plain,
! [X0,X1] :
( ~ sP4_prd(succ(X1),X0)
| ~ leq(X0,n2) ),
inference(forward_subsumption_resolution,[status(thm)],[f30232,f25915]) ).
fof(f34552,plain,
! [X0,X1] : ~ sP4_prd(succ(X0),X1),
inference(forward_subsumption_resolution,[status(thm)],[f30260,f4521]) ).
fof(f34564,plain,
! [X0,X1] : ~ sP4_prd(X0,X1),
inference(paramodulation,[status(thm)],[f229,f34552]) ).
fof(f34572,plain,
( ~ leq(sK32_skl,n5)
| ~ leq(n0,sK32_skl)
| ~ leq(sK31_skl,pred(pv57))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f26279,f34564]) ).
fof(f34578,plain,
( leq(sK31_skl,pred(pv57))
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f3241,f34564]) ).
fof(f34580,plain,
( leq(sK32_skl,n5)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f11271,f34564]) ).
fof(f34581,plain,
( leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f10521,f34564]) ).
fof(f57813,plain,
! [X0,X1] :
( ~ gt(X1,pred(X0))
| leq(X0,succ(pred(X1))) ),
inference(resolution,[status(thm)],[f4230,f128]) ).
fof(f57888,plain,
! [X0,X1] :
( ~ gt(X1,pred(X0))
| leq(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f229,f57813]) ).
fof(f58208,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(succ(X0),X1) ),
inference(paramodulation,[status(thm)],[f228,f57888]) ).
fof(f59562,plain,
! [X0,X1] :
( ~ sP3_prd(succ(X0),X1)
| ~ leq(X1,n5)
| ~ gt(n5,X0) ),
inference(resolution,[status(thm)],[f58208,f24724]) ).
fof(f59564,plain,
! [X0,X1] :
( ~ sP5_prd(succ(X0),X1)
| ~ leq(X1,n5)
| ~ gt(n5,X0) ),
inference(resolution,[status(thm)],[f58208,f23871]) ).
fof(f59689,plain,
! [X0,X1] :
( ~ sP3_prd(succ(X0),X1)
| ~ gt(n5,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f59562,f3155]) ).
fof(f59690,plain,
! [X0,X1] :
( ~ sP5_prd(succ(X0),X1)
| ~ gt(n5,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f59564,f1953]) ).
fof(f60722,plain,
( ~ leq(sK32_skl,n5)
| ~ leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f34572,f34578]) ).
fof(f62929,plain,
! [X0,X1] :
( ~ sP3_prd(X0,X1)
| ~ gt(n5,pred(X0)) ),
inference(paramodulation,[status(thm)],[f229,f59689]) ).
fof(f62942,plain,
! [X0,X1] :
( ~ sP5_prd(X0,X1)
| ~ gt(n5,pred(X0)) ),
inference(paramodulation,[status(thm)],[f229,f59690]) ).
fof(f62944,plain,
( ~ leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl)
| sP3_prd(sK24_skl,sK23_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f60722,f34580]) ).
fof(f62971,plain,
! [X0,X1] :
( ~ leq(X0,n5)
| ~ sP3_prd(X0,X1) ),
inference(resolution,[status(thm)],[f62929,f1520]) ).
fof(f62988,plain,
! [X0,X1] : ~ sP3_prd(X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[f62971,f3003]) ).
fof(f63023,plain,
! [X0,X1] :
( ~ leq(X0,n5)
| ~ sP5_prd(X0,X1) ),
inference(resolution,[status(thm)],[f62942,f1520]) ).
fof(f63040,plain,
! [X0,X1] : ~ sP5_prd(X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[f63023,f1955]) ).
fof(f64530,plain,
( leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f34581,f62988]) ).
fof(f75771,plain,
( sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f64530,f75772]) ).
fof(f75772,plain,
( ~ leq(n0,sK32_skl)
| sP6_prd(sK30_skl,sK29_skl)
| sP5_prd(sK28_skl,sK27_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f62944,f62988]) ).
fof(f75774,plain,
sP6_prd(sK30_skl,sK29_skl),
inference(forward_subsumption_resolution,[status(thm)],[f75771,f63040]) ).
fof(f75778,plain,
~ gt(pv57,sK29_skl),
inference(resolution,[status(thm)],[f75774,f18827]) ).
fof(f75781,plain,
leq(sK29_skl,pv57),
inference(resolution,[status(thm)],[f75774,f395]) ).
fof(f75807,plain,
( gt(pv57,sK29_skl)
| sK29_skl = pv57 ),
inference(resolution,[status(thm)],[f75781,f124]) ).
fof(f75811,plain,
sK29_skl = pv57,
inference(forward_subsumption_resolution,[status(thm)],[f75807,f75778]) ).
fof(f75814,plain,
sP6_prd(sK30_skl,pv57),
inference(backward_demodulation,[status(thm)],[f75811,f75774]) ).
fof(f75815,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f75814,f17246]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV111+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 08:34:07 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.40 % Drodi V4.1.1
% 277.00/35.34 % Refutation found
% 277.00/35.34 % SZS status Theorem for theBenchmark: Theorem is valid
% 277.00/35.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 19.32/35.41 % Elapsed time: 35.020494 seconds
% 19.32/35.41 % CPU time: 277.618581 seconds
% 19.32/35.41 % Total memory used: 588.138 MB
% 19.32/35.41 % Net memory used: 511.532 MB
%------------------------------------------------------------------------------