%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV116+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n009.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:12:15 PM UTC 2026
% Result : Theorem 247.81s 41.36s
% Output : Proof 247.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 137
% Number of leaves : 5
% Syntax : Number of formulae : 641 ( 30 unt; 0 def)
% Number of atoms : 2223 ( 432 equ)
% Maximal formula atoms : 42 ( 3 avg)
% Number of connectives : 1978 ( 396 ~;1459 |; 102 &)
% ( 1 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 17 con; 0-3 aty)
% Number of variables : 100 ( 0 sgn 64 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f52,conjecture,
( ( ! [I] :
( ( leq(I,minus(n6,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) )
=> a_select3(pminus_ds1_filter,G,H) = a_select3(pminus_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(pv5,minus(n999,n1))
& leq(n0,pv5) )
=> ( ! [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) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quaternion_ds1_symm_0009) ).
fof(f52_neg,negated_conjecture,
~ ( ( ! [I] :
( ( leq(I,minus(n6,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) )
=> a_select3(pminus_ds1_filter,G,H) = a_select3(pminus_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(pv5,minus(n999,n1))
& leq(n0,pv5) )
=> ( ! [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) ) ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f52_nnf,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) )
| ? [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) ) )
& ! [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(n6,n1))
| ~ leq(n0,I) )
& ! [G,H] :
( a_select3(pminus_ds1_filter,G,H) = a_select3(pminus_ds1_filter,H,G)
| ~ 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(pv5,minus(n999,n1))
& leq(n0,pv5) ),
inference(nnf_transformation,[status(thm)],[f52_neg]) ).
fof(f52_sk,plain,
! [A,B,C,D,E,F,G,H,I,J] :
( ( ( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
& leq(sk32,minus(n6,n1))
& leq(sk31,minus(n6,n1))
& leq(n0,sk32)
& leq(n0,sk31) )
| ( a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
& leq(sk30,minus(n3,n1))
& leq(sk29,minus(n3,n1))
& leq(n0,sk30)
& leq(n0,sk29) )
| ( a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27)
& leq(sk28,minus(n6,n1))
& leq(sk27,minus(n6,n1))
& leq(n0,sk28)
& leq(n0,sk27) ) )
& ( 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(n6,n1))
| ~ leq(n0,I) )
& ( a_select3(pminus_ds1_filter,G,H) = a_select3(pminus_ds1_filter,H,G)
| ~ leq(H,minus(n6,n1))
| ~ leq(G,minus(n6,n1))
| ~ leq(n0,H)
| ~ leq(n0,G) )
& ( 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) )
& ( 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_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(pv5,minus(n999,n1))
& leq(n0,pv5) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk27,sk28,sk29,sk30,sk31,sk32])],[f52_nnf]) ).
cnf(c267,plain,
( leq(n0,sk31)
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(c259,plain,
( a_select3(pminus_ds1_filter,X4,X5) = a_select3(pminus_ds1_filter,X5,X4)
| ~ leq(X5,minus(n6,n1))
| ~ leq(X4,minus(n6,n1))
| ~ leq(n0,X5)
| ~ leq(n0,X4) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p3408,plain,
( a_select3(pminus_ds1_filter,sk31,X0) = a_select3(pminus_ds1_filter,X0,sk31)
| ~ leq(X0,pred(n6))
| ~ leq(sk31,pred(n6))
| ~ leq(n0,X0)
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[c267,c259]) ).
cnf(c268,plain,
( leq(n0,sk32)
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p12037,plain,
( leq(n0,sk30)
| leq(n0,sk27)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p3408,c268]) ).
cnf(p26331,plain,
( leq(n0,sk30)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p12037]) ).
cnf(p26333,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26331]) ).
fof(f38,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pred_minus_1) ).
fof(f38_nnf,plain,
! [X] : minus(X,n1) = pred(X),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [X] : minus(X,n1) = pred(X),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c234,plain,
minus(X0,n1) = pred(X0),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(c269,plain,
( leq(sk31,minus(n6,n1))
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p3994,plain,
( leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c269]) ).
cnf(p26340,plain,
( leq(n0,sk30)
| leq(n0,sk27)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26333,p3994]) ).
cnf(p26343,plain,
( leq(n0,sk30)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26340]) ).
cnf(p26345,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26343]) ).
cnf(c270,plain,
( leq(sk32,minus(n6,n1))
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4045,plain,
( leq(sk32,pred(n6))
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c270]) ).
cnf(p26352,plain,
( leq(n0,sk30)
| leq(n0,sk27)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26345,p4045]) ).
cnf(p26355,plain,
( leq(n0,sk30)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26352]) ).
cnf(p26357,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26355]) ).
cnf(c271,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p26366,plain,
( leq(n0,sk30)
| leq(n0,sk27)
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26357,c271]) ).
cnf(p26384,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26366]) ).
cnf(p26386,plain,
( leq(n0,sk30)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26384]) ).
cnf(c263,plain,
( leq(n0,sk32)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(c262,plain,
( leq(n0,sk31)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p466,plain,
( a_select3(pminus_ds1_filter,sk31,X0) = a_select3(pminus_ds1_filter,X0,sk31)
| ~ leq(X0,minus(n6,n1))
| ~ leq(sk31,minus(n6,n1))
| ~ leq(n0,X0)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[c262,c259]) ).
cnf(p3378,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(n0,sk27)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[c263,p466]) ).
cnf(p20567,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p3378]) ).
cnf(p20569,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p20567]) ).
cnf(c264,plain,
( leq(sk31,minus(n6,n1))
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p3905,plain,
( leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c264]) ).
cnf(p20578,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p20569,p3905]) ).
cnf(p20582,plain,
( leq(n0,sk29)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p20578]) ).
cnf(p20584,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p20582]) ).
cnf(c265,plain,
( leq(sk32,minus(n6,n1))
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p3956,plain,
( leq(sk32,pred(n6))
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c265]) ).
cnf(p20592,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p20584,p3956]) ).
cnf(p20597,plain,
( leq(n0,sk29)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p20592]) ).
cnf(p20599,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p20597]) ).
cnf(c266,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p20608,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p20599,c266]) ).
cnf(p20612,plain,
( leq(n0,sk29)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p20608]) ).
cnf(p20614,plain,
( leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p20612]) ).
cnf(c258,plain,
( a_select3(r_ds1_filter,X2,X3) = a_select3(r_ds1_filter,X3,X2)
| ~ leq(X3,minus(n3,n1))
| ~ leq(X2,minus(n3,n1))
| ~ leq(n0,X3)
| ~ leq(n0,X2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p20616,plain,
( a_select3(r_ds1_filter,sk29,X0) = a_select3(r_ds1_filter,X0,sk29)
| ~ leq(X0,n2)
| ~ leq(sk29,n2)
| ~ leq(n0,X0)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p20614,c258]) ).
cnf(p26423,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| ~ leq(sk29,n2)
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26386,p20616]) ).
cnf(p26474,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| ~ leq(sk29,n2)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26423]) ).
cnf(c273,plain,
( leq(n0,sk32)
| leq(sk29,minus(n3,n1))
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4097,plain,
( leq(n0,sk32)
| leq(sk29,n2)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c273]) ).
cnf(p26475,plain,
( leq(n0,sk32)
| leq(n0,sk27)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26474,p4097]) ).
cnf(p26506,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26475]) ).
cnf(c278,plain,
( leq(n0,sk32)
| leq(sk30,minus(n3,n1))
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4099,plain,
( leq(n0,sk32)
| leq(sk30,n2)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c278]) ).
cnf(p26508,plain,
( leq(n0,sk32)
| leq(n0,sk27)
| leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26506,p4099]) ).
cnf(p26574,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26508]) ).
cnf(p26576,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26574]) ).
cnf(c283,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p26585,plain,
( leq(n0,sk32)
| leq(n0,sk27)
| leq(n0,sk32)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26576,c283]) ).
cnf(p26589,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26585]) ).
cnf(p26591,plain,
( leq(n0,sk32)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26589]) ).
cnf(p26597,plain,
( a_select3(pminus_ds1_filter,sk32,X0) = a_select3(pminus_ds1_filter,X0,sk32)
| ~ leq(X0,pred(n6))
| ~ leq(sk32,pred(n6))
| ~ leq(n0,X0)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26591,c259]) ).
cnf(c272,plain,
( leq(n0,sk31)
| leq(sk29,minus(n3,n1))
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p15255,plain,
( leq(n0,sk31)
| leq(sk29,n2)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c272]) ).
cnf(p26476,plain,
( leq(n0,sk31)
| leq(n0,sk27)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26474,p15255]) ).
cnf(p26509,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26476]) ).
cnf(c277,plain,
( leq(n0,sk31)
| leq(sk30,minus(n3,n1))
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4080,plain,
( leq(n0,sk31)
| leq(sk30,n2)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c277]) ).
cnf(p26510,plain,
( leq(n0,sk31)
| leq(n0,sk27)
| leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26509,p4080]) ).
cnf(p26636,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26510]) ).
cnf(p26638,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26636]) ).
cnf(c282,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p26650,plain,
( leq(n0,sk31)
| leq(n0,sk27)
| leq(n0,sk31)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26638,c282]) ).
cnf(p26651,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26650]) ).
cnf(p26653,plain,
( leq(n0,sk31)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26651]) ).
cnf(p26863,plain,
( leq(n0,sk27)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p26597,p26653]) ).
cnf(p27206,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p26863]) ).
cnf(c280,plain,
( leq(sk32,minus(n6,n1))
| leq(sk30,minus(n3,n1))
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4218,plain,
( leq(sk32,pred(n6))
| leq(sk30,n2)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c280]) ).
cnf(p27212,plain,
( leq(sk30,n2)
| leq(n0,sk27)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p27206,p4218]) ).
cnf(p27269,plain,
( leq(sk30,n2)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27212]) ).
cnf(c279,plain,
( leq(sk31,minus(n6,n1))
| leq(sk30,minus(n3,n1))
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4183,plain,
( leq(sk31,pred(n6))
| leq(sk30,n2)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c279]) ).
cnf(p27272,plain,
( leq(sk30,n2)
| leq(n0,sk27)
| leq(sk30,n2)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p27269,p4183]) ).
cnf(p27273,plain,
( leq(sk30,n2)
| leq(sk30,n2)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27272]) ).
cnf(p27275,plain,
( leq(sk30,n2)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27273]) ).
cnf(c281,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk30,minus(n3,n1))
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p27278,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(sk30,n2)
| leq(n0,sk27)
| leq(sk30,n2)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[p27275,c281]) ).
cnf(p27279,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(sk30,n2)
| leq(sk30,n2)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27278]) ).
cnf(p27281,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(sk30,n2)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27279]) ).
cnf(p27282,plain,
( leq(sk30,n2)
| leq(n0,sk27) ),
inference(equality_resolution,[status(thm)],[p27281]) ).
cnf(c275,plain,
( leq(sk32,minus(n6,n1))
| leq(sk29,minus(n3,n1))
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4165,plain,
( leq(sk32,pred(n6))
| leq(sk29,n2)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c275]) ).
cnf(p27211,plain,
( leq(sk29,n2)
| leq(n0,sk27)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p27206,p4165]) ).
cnf(p27213,plain,
( leq(sk29,n2)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27211]) ).
cnf(c274,plain,
( leq(sk31,minus(n6,n1))
| leq(sk29,minus(n3,n1))
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4134,plain,
( leq(sk31,pred(n6))
| leq(sk29,n2)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[c234,c274]) ).
cnf(p27218,plain,
( leq(sk29,n2)
| leq(n0,sk27)
| leq(sk29,n2)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p27213,p4134]) ).
cnf(p27220,plain,
( leq(sk29,n2)
| leq(sk29,n2)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27218]) ).
cnf(p27222,plain,
( leq(sk29,n2)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27220]) ).
cnf(c276,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk29,minus(n3,n1))
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p27227,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(sk29,n2)
| leq(n0,sk27)
| leq(sk29,n2)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[p27222,c276]) ).
cnf(p27229,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(sk29,n2)
| leq(sk29,n2)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27227]) ).
cnf(p27231,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(sk29,n2)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27229]) ).
cnf(p27232,plain,
( leq(sk29,n2)
| leq(n0,sk27) ),
inference(equality_resolution,[status(thm)],[p27231]) ).
cnf(p27247,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p27232,p26474]) ).
cnf(p27266,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27247]) ).
cnf(p27313,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p27282,p27266]) ).
cnf(p27317,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27313]) ).
cnf(c285,plain,
( leq(sk32,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p27325,plain,
( leq(sk32,pred(n6))
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p27317,c285]) ).
cnf(p27354,plain,
( leq(sk32,pred(n6))
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27325]) ).
cnf(p27382,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p27354,p27206]) ).
cnf(p27452,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27382]) ).
cnf(c284,plain,
( leq(sk31,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p27324,plain,
( leq(sk31,pred(n6))
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p27317,c284]) ).
cnf(p27327,plain,
( leq(sk31,pred(n6))
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27324]) ).
cnf(p27453,plain,
( leq(n0,sk27)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p27452,p27327]) ).
cnf(p27454,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27453]) ).
cnf(c286,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p27326,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p27317,c286]) ).
cnf(p27383,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27326]) ).
cnf(p27455,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(superposition,[status(thm)],[p27454,p27383]) ).
cnf(p27456,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p27455]) ).
cnf(p27457,plain,
leq(n0,sk27),
inference(equality_resolution,[status(thm)],[p27456]) ).
cnf(c257,plain,
( 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(esa)],[f52_sk]) ).
cnf(p27458,plain,
( a_select3(q_ds1_filter,sk27,X0) = a_select3(q_ds1_filter,X0,sk27)
| ~ leq(X0,pred(n6))
| ~ leq(sk27,pred(n6))
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[p27457,c257]) ).
cnf(c302,plain,
( leq(n0,sk31)
| leq(sk30,minus(n3,n1))
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1425,plain,
( leq(n0,sk31)
| leq(sk30,n2)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c302]) ).
cnf(c293,plain,
( leq(n0,sk32)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1343,plain,
( a_select3(pminus_ds1_filter,sk32,X0) = a_select3(pminus_ds1_filter,X0,sk32)
| ~ leq(X0,pred(n6))
| ~ leq(sk32,pred(n6))
| ~ leq(n0,X0)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[c293,c259]) ).
cnf(c292,plain,
( leq(n0,sk31)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1800,plain,
( leq(n0,sk30)
| leq(n0,sk28)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p1343,c292]) ).
cnf(p2923,plain,
( leq(n0,sk30)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1800]) ).
cnf(p2925,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2923]) ).
cnf(c295,plain,
( leq(sk32,minus(n6,n1))
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1311,plain,
( leq(sk32,pred(n6))
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c295]) ).
cnf(p2932,plain,
( leq(n0,sk30)
| leq(n0,sk28)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2925,p1311]) ).
cnf(p2934,plain,
( leq(n0,sk30)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2932]) ).
cnf(p2936,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2934]) ).
cnf(c294,plain,
( leq(sk31,minus(n6,n1))
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1377,plain,
( leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c294]) ).
cnf(p2944,plain,
( leq(n0,sk30)
| leq(n0,sk28)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2936,p1377]) ).
cnf(p2954,plain,
( leq(n0,sk30)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2944]) ).
cnf(p2956,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2954]) ).
cnf(c296,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p2963,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk30)
| leq(n0,sk28)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[p2956,c296]) ).
cnf(p2965,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk30)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2963]) ).
cnf(p2967,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2965]) ).
cnf(p2968,plain,
( leq(n0,sk30)
| leq(n0,sk28) ),
inference(equality_resolution,[status(thm)],[p2967]) ).
cnf(c288,plain,
( leq(n0,sk32)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1259,plain,
( a_select3(pminus_ds1_filter,sk32,X0) = a_select3(pminus_ds1_filter,X0,sk32)
| ~ leq(X0,pred(n6))
| ~ leq(sk32,pred(n6))
| ~ leq(n0,X0)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[c288,c259]) ).
cnf(c287,plain,
( leq(n0,sk31)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1648,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p1259,c287]) ).
cnf(p2676,plain,
( leq(n0,sk29)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1648]) ).
cnf(p2678,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2676]) ).
cnf(c290,plain,
( leq(sk32,minus(n6,n1))
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1309,plain,
( leq(sk32,pred(n6))
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c290]) ).
cnf(p2686,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2678,p1309]) ).
cnf(p2689,plain,
( leq(n0,sk29)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2686]) ).
cnf(p2691,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2689]) ).
cnf(c289,plain,
( leq(sk31,minus(n6,n1))
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1293,plain,
( leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c289]) ).
cnf(p2700,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2691,p1293]) ).
cnf(p2703,plain,
( leq(n0,sk29)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2700]) ).
cnf(p2705,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2703]) ).
cnf(c291,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p2714,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk29)
| leq(n0,sk28)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[p2705,c291]) ).
cnf(p2717,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk29)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2714]) ).
cnf(p2719,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2717]) ).
cnf(p2720,plain,
( leq(n0,sk29)
| leq(n0,sk28) ),
inference(equality_resolution,[status(thm)],[p2719]) ).
cnf(p2722,plain,
( a_select3(r_ds1_filter,sk29,X0) = a_select3(r_ds1_filter,X0,sk29)
| ~ leq(X0,n2)
| ~ leq(sk29,n2)
| ~ leq(n0,X0)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2720,c258]) ).
cnf(p3001,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| ~ leq(sk29,n2)
| leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2968,p2722]) ).
cnf(p3017,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| ~ leq(sk29,n2)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p3001]) ).
cnf(c297,plain,
( leq(n0,sk31)
| leq(sk29,minus(n3,n1))
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1313,plain,
( leq(n0,sk31)
| leq(sk29,n2)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c297]) ).
cnf(p3018,plain,
( leq(n0,sk31)
| leq(n0,sk28)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p3017,p1313]) ).
cnf(p3021,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p3018]) ).
cnf(p3485,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk28)
| leq(n0,sk31)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p1425,p3021]) ).
cnf(p4992,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk31)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p3485]) ).
cnf(p4994,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk31)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p4992]) ).
cnf(c307,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p5006,plain,
( leq(n0,sk31)
| leq(n0,sk28)
| leq(n0,sk31)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p4994,c307]) ).
cnf(p5052,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p5006]) ).
cnf(p5054,plain,
( leq(n0,sk31)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p5052]) ).
cnf(p5060,plain,
( a_select3(pminus_ds1_filter,sk31,X0) = a_select3(pminus_ds1_filter,X0,sk31)
| ~ leq(X0,pred(n6))
| ~ leq(sk31,pred(n6))
| ~ leq(n0,X0)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p5054,c259]) ).
cnf(c303,plain,
( leq(n0,sk32)
| leq(sk30,minus(n3,n1))
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4115,plain,
( leq(n0,sk32)
| leq(sk30,n2)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c303]) ).
cnf(c298,plain,
( leq(n0,sk32)
| leq(sk29,minus(n3,n1))
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1315,plain,
( leq(n0,sk32)
| leq(sk29,n2)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c298]) ).
cnf(p3019,plain,
( leq(n0,sk32)
| leq(n0,sk28)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p3017,p1315]) ).
cnf(p3022,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p3019]) ).
cnf(p4130,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk28)
| leq(n0,sk32)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p4115,p3022]) ).
cnf(p5472,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk32)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p4130]) ).
cnf(p5474,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk32)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p5472]) ).
cnf(c308,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p5483,plain,
( leq(n0,sk32)
| leq(n0,sk28)
| leq(n0,sk32)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p5474,c308]) ).
cnf(p5487,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p5483]) ).
cnf(p5489,plain,
( leq(n0,sk32)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p5487]) ).
cnf(p6393,plain,
( leq(n0,sk28)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p5060,p5489]) ).
cnf(p7722,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p6393]) ).
cnf(c304,plain,
( leq(sk31,minus(n6,n1))
| leq(sk30,minus(n3,n1))
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4237,plain,
( leq(sk31,pred(n6))
| leq(sk30,n2)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c304]) ).
cnf(p7730,plain,
( leq(sk30,n2)
| leq(n0,sk28)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7722,p4237]) ).
cnf(p7791,plain,
( leq(sk30,n2)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7730]) ).
cnf(c305,plain,
( leq(sk32,minus(n6,n1))
| leq(sk30,minus(n3,n1))
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4256,plain,
( leq(sk32,pred(n6))
| leq(sk30,n2)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c305]) ).
cnf(p7795,plain,
( leq(sk30,n2)
| leq(n0,sk28)
| leq(sk30,n2)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7791,p4256]) ).
cnf(p7889,plain,
( leq(n0,sk28)
| leq(sk30,n2)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7795]) ).
cnf(p7890,plain,
( leq(sk30,n2)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7889]) ).
cnf(c306,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk30,minus(n3,n1))
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p7893,plain,
( leq(sk30,n2)
| leq(n0,sk28)
| leq(sk30,n2)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7890,c306]) ).
cnf(p7894,plain,
( leq(sk30,n2)
| leq(sk30,n2)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7893]) ).
cnf(p7896,plain,
( leq(sk30,n2)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7894]) ).
cnf(c299,plain,
( leq(sk31,minus(n6,n1))
| leq(sk29,minus(n3,n1))
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1320,plain,
( leq(sk31,pred(n6))
| leq(sk29,n2)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c299]) ).
cnf(p7727,plain,
( leq(sk29,n2)
| leq(n0,sk28)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7722,p1320]) ).
cnf(p7731,plain,
( leq(sk29,n2)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7727]) ).
cnf(c300,plain,
( leq(sk32,minus(n6,n1))
| leq(sk29,minus(n3,n1))
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1336,plain,
( leq(sk32,pred(n6))
| leq(sk29,n2)
| leq(n0,sk28) ),
inference(superposition,[status(thm)],[c234,c300]) ).
cnf(p7736,plain,
( leq(sk29,n2)
| leq(n0,sk28)
| leq(sk29,n2)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7731,p1336]) ).
cnf(p7740,plain,
( leq(sk29,n2)
| leq(sk29,n2)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7736]) ).
cnf(p7742,plain,
( leq(sk29,n2)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7740]) ).
cnf(c301,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk29,minus(n3,n1))
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p7747,plain,
( leq(sk29,n2)
| leq(n0,sk28)
| leq(sk29,n2)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7742,c301]) ).
cnf(p7750,plain,
( leq(sk29,n2)
| leq(sk29,n2)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7747]) ).
cnf(p7752,plain,
( leq(sk29,n2)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7750]) ).
cnf(p7763,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7752,p3017]) ).
cnf(p7784,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7763]) ).
cnf(p7913,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7896,p7784]) ).
cnf(p7917,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7913]) ).
cnf(c309,plain,
( leq(sk31,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p7924,plain,
( leq(sk31,pred(n6))
| leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7917,c309]) ).
cnf(p7927,plain,
( leq(sk31,pred(n6))
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7924]) ).
cnf(p7953,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7927,p7722]) ).
cnf(p8018,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7953]) ).
cnf(c310,plain,
( leq(sk32,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p7925,plain,
( leq(sk32,pred(n6))
| leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7917,c310]) ).
cnf(p7954,plain,
( leq(sk32,pred(n6))
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7925]) ).
cnf(p8019,plain,
( leq(n0,sk28)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p8018,p7954]) ).
cnf(p8020,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p8019]) ).
cnf(c311,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p7926,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p7917,c311]) ).
cnf(p7975,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p7926]) ).
cnf(p8021,plain,
( leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p8020,p7975]) ).
cnf(p8022,plain,
leq(n0,sk28),
inference(factoring,[status(thm)],[p8021]) ).
cnf(p27787,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6))
| ~ leq(sk27,pred(n6)) ),
inference(resolution,[status(thm)],[p27458,p8022]) ).
cnf(c317,plain,
( leq(n0,sk31)
| leq(n0,sk30)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4663,plain,
( leq(n0,sk31)
| leq(n0,sk30)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c317]) ).
cnf(p27907,plain,
( leq(n0,sk31)
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p27787,p4663]) ).
cnf(c342,plain,
( leq(n0,sk31)
| leq(n0,sk30)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p522,plain,
( leq(n0,sk31)
| leq(n0,sk30)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c342]) ).
cnf(p27981,plain,
( leq(n0,sk31)
| leq(n0,sk30)
| leq(n0,sk31)
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(resolution,[status(thm)],[p27907,p522]) ).
cnf(p29802,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p27981]) ).
cnf(p29804,plain,
( leq(n0,sk31)
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p29802]) ).
cnf(c367,plain,
( leq(n0,sk31)
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p29812,plain,
( leq(n0,sk31)
| leq(n0,sk30)
| leq(n0,sk31)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p29804,c367]) ).
cnf(p29813,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p29812]) ).
cnf(p29815,plain,
( leq(n0,sk31)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p29813]) ).
cnf(p29821,plain,
( a_select3(pminus_ds1_filter,sk31,X0) = a_select3(pminus_ds1_filter,X0,sk31)
| ~ leq(X0,pred(n6))
| ~ leq(sk31,pred(n6))
| ~ leq(n0,X0)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p29815,c259]) ).
cnf(c318,plain,
( leq(n0,sk32)
| leq(n0,sk30)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1172,plain,
( leq(n0,sk32)
| leq(n0,sk30)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c318]) ).
cnf(p27904,plain,
( leq(n0,sk32)
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p27787,p1172]) ).
cnf(c343,plain,
( leq(n0,sk32)
| leq(n0,sk30)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p617,plain,
( leq(n0,sk32)
| leq(n0,sk30)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c343]) ).
cnf(p27973,plain,
( leq(n0,sk32)
| leq(n0,sk30)
| leq(n0,sk32)
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(resolution,[status(thm)],[p27904,p617]) ).
cnf(p29561,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p27973]) ).
cnf(p29563,plain,
( leq(n0,sk32)
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p29561]) ).
cnf(c368,plain,
( leq(n0,sk32)
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p29569,plain,
( leq(n0,sk32)
| leq(n0,sk30)
| leq(n0,sk32)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p29563,c368]) ).
cnf(p29572,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p29569]) ).
cnf(p29574,plain,
( leq(n0,sk32)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p29572]) ).
cnf(p30532,plain,
( leq(n0,sk30)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p29821,p29574]) ).
cnf(p30828,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p30532]) ).
cnf(c319,plain,
( leq(sk31,minus(n6,n1))
| leq(n0,sk30)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1078,plain,
( leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c319]) ).
cnf(p30832,plain,
( leq(n0,sk30)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p30828,p1078]) ).
cnf(p31035,plain,
( leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p30832]) ).
cnf(c320,plain,
( leq(sk32,minus(n6,n1))
| leq(n0,sk30)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1094,plain,
( leq(sk32,pred(n6))
| leq(n0,sk30)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c320]) ).
cnf(p31036,plain,
( leq(n0,sk30)
| leq(sk27,pred(n6))
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p31035,p1094]) ).
cnf(p33223,plain,
( leq(n0,sk30)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p31036]) ).
cnf(p33224,plain,
( leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33223]) ).
cnf(c321,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p33225,plain,
( leq(n0,sk30)
| leq(sk27,pred(n6))
| leq(sk27,pred(n6))
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p33224,c321]) ).
cnf(p33229,plain,
( leq(n0,sk30)
| leq(sk27,pred(n6))
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33225]) ).
cnf(p33230,plain,
( leq(sk27,pred(n6))
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33229]) ).
cnf(p33241,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6))
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p33230,p27787]) ).
cnf(c344,plain,
( leq(sk31,minus(n6,n1))
| leq(n0,sk30)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p611,plain,
( leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c344]) ).
cnf(p30831,plain,
( leq(n0,sk30)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p30828,p611]) ).
cnf(p31028,plain,
( leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p30831]) ).
cnf(c345,plain,
( leq(sk32,minus(n6,n1))
| leq(n0,sk30)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p609,plain,
( leq(sk32,pred(n6))
| leq(n0,sk30)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c345]) ).
cnf(p31031,plain,
( leq(n0,sk30)
| leq(sk28,pred(n6))
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p31028,p609]) ).
cnf(p33148,plain,
( leq(n0,sk30)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p31031]) ).
cnf(p33149,plain,
( leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33148]) ).
cnf(c346,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p33150,plain,
( leq(n0,sk30)
| leq(sk28,pred(n6))
| leq(sk28,pred(n6))
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p33149,c346]) ).
cnf(p33153,plain,
( leq(n0,sk30)
| leq(sk28,pred(n6))
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33150]) ).
cnf(p33154,plain,
( leq(sk28,pred(n6))
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33153]) ).
cnf(p33277,plain,
( leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p33241,p33154]) ).
cnf(p33278,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33277]) ).
cnf(c370,plain,
( leq(sk32,minus(n6,n1))
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p33284,plain,
( leq(sk32,pred(n6))
| leq(n0,sk30)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p33278,c370]) ).
cnf(p33322,plain,
( leq(sk32,pred(n6))
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33284]) ).
cnf(p29580,plain,
( a_select3(pminus_ds1_filter,sk32,X0) = a_select3(pminus_ds1_filter,X0,sk32)
| ~ leq(X0,pred(n6))
| ~ leq(sk32,pred(n6))
| ~ leq(n0,X0)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p29574,c259]) ).
cnf(p30016,plain,
( leq(n0,sk30)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p29580,p29815]) ).
cnf(p30644,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p30016]) ).
cnf(p33348,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p33322,p30644]) ).
cnf(p33455,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33348]) ).
cnf(c369,plain,
( leq(sk31,minus(n6,n1))
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p33285,plain,
( leq(sk31,pred(n6))
| leq(n0,sk30)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p33278,c369]) ).
cnf(p33354,plain,
( leq(sk31,pred(n6))
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33285]) ).
cnf(p33456,plain,
( leq(n0,sk30)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p33455,p33354]) ).
cnf(p33457,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33456]) ).
cnf(c371,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p33290,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p33278,c371]) ).
cnf(p33386,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33290]) ).
cnf(p33458,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk30)
| leq(n0,sk30) ),
inference(superposition,[status(thm)],[p33457,p33386]) ).
cnf(p33459,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p33458]) ).
cnf(p33460,plain,
leq(n0,sk30),
inference(equality_resolution,[status(thm)],[p33459]) ).
cnf(c312,plain,
( leq(n0,sk31)
| leq(n0,sk29)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4349,plain,
( leq(n0,sk31)
| leq(n0,sk29)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c312]) ).
cnf(p27905,plain,
( leq(n0,sk31)
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p27787,p4349]) ).
cnf(c337,plain,
( leq(n0,sk31)
| leq(n0,sk29)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p523,plain,
( leq(n0,sk31)
| leq(n0,sk29)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c337]) ).
cnf(p27976,plain,
( leq(n0,sk31)
| leq(n0,sk29)
| leq(n0,sk31)
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(resolution,[status(thm)],[p27905,p523]) ).
cnf(p29680,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p27976]) ).
cnf(p29682,plain,
( leq(n0,sk31)
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p29680]) ).
cnf(c362,plain,
( leq(n0,sk31)
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p29683,plain,
( leq(n0,sk31)
| leq(n0,sk29)
| leq(n0,sk31)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p29682,c362]) ).
cnf(p29693,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p29683]) ).
cnf(p29695,plain,
( leq(n0,sk31)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p29693]) ).
cnf(p29701,plain,
( a_select3(pminus_ds1_filter,sk31,X0) = a_select3(pminus_ds1_filter,X0,sk31)
| ~ leq(X0,pred(n6))
| ~ leq(sk31,pred(n6))
| ~ leq(n0,X0)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p29695,c259]) ).
cnf(c313,plain,
( leq(n0,sk32)
| leq(n0,sk29)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p4384,plain,
( leq(n0,sk32)
| leq(n0,sk29)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c313]) ).
cnf(p27906,plain,
( leq(n0,sk32)
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p27787,p4384]) ).
cnf(c338,plain,
( leq(n0,sk32)
| leq(n0,sk29)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p524,plain,
( leq(n0,sk32)
| leq(n0,sk29)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c338]) ).
cnf(p27979,plain,
( leq(n0,sk32)
| leq(n0,sk29)
| leq(n0,sk32)
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(resolution,[status(thm)],[p27906,p524]) ).
cnf(p29747,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p27979]) ).
cnf(p29749,plain,
( leq(n0,sk32)
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p29747]) ).
cnf(c363,plain,
( leq(n0,sk32)
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p29755,plain,
( leq(n0,sk32)
| leq(n0,sk29)
| leq(n0,sk32)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p29749,c363]) ).
cnf(p29758,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p29755]) ).
cnf(p29760,plain,
( leq(n0,sk32)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p29758]) ).
cnf(p30210,plain,
( leq(n0,sk29)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p29701,p29760]) ).
cnf(p30718,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6))
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p30210]) ).
cnf(c314,plain,
( leq(sk31,minus(n6,n1))
| leq(n0,sk29)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1186,plain,
( leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c314]) ).
cnf(p30726,plain,
( leq(n0,sk29)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p30718,p1186]) ).
cnf(p30960,plain,
( leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p30726]) ).
cnf(c315,plain,
( leq(sk32,minus(n6,n1))
| leq(n0,sk29)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p13653,plain,
( leq(sk32,pred(n6))
| leq(n0,sk29)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c315]) ).
cnf(p30964,plain,
( leq(n0,sk29)
| leq(sk27,pred(n6))
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p30960,p13653]) ).
cnf(p32148,plain,
( leq(n0,sk29)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p30964]) ).
cnf(p32149,plain,
( leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p32148]) ).
cnf(c316,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p32150,plain,
( leq(n0,sk29)
| leq(sk27,pred(n6))
| leq(sk27,pred(n6))
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p32149,c316]) ).
cnf(p32152,plain,
( leq(n0,sk29)
| leq(sk27,pred(n6))
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p32150]) ).
cnf(p32153,plain,
( leq(sk27,pred(n6))
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p32152]) ).
cnf(p32165,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6))
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p32153,p27787]) ).
cnf(c339,plain,
( leq(sk31,minus(n6,n1))
| leq(n0,sk29)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p520,plain,
( leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c339]) ).
cnf(p30719,plain,
( leq(n0,sk29)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p30718,p520]) ).
cnf(p30942,plain,
( leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p30719]) ).
cnf(c340,plain,
( leq(sk32,minus(n6,n1))
| leq(n0,sk29)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p521,plain,
( leq(sk32,pred(n6))
| leq(n0,sk29)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c340]) ).
cnf(p30943,plain,
( leq(n0,sk29)
| leq(sk28,pred(n6))
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p30942,p521]) ).
cnf(p31097,plain,
( leq(n0,sk29)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p30943]) ).
cnf(p31098,plain,
( leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p31097]) ).
cnf(c341,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p31099,plain,
( leq(n0,sk29)
| leq(sk28,pred(n6))
| leq(sk28,pred(n6))
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p31098,c341]) ).
cnf(p31108,plain,
( leq(n0,sk29)
| leq(sk28,pred(n6))
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p31099]) ).
cnf(p31109,plain,
( leq(sk28,pred(n6))
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p31108]) ).
cnf(p32235,plain,
( leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p32165,p31109]) ).
cnf(p32236,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p32235]) ).
cnf(c365,plain,
( leq(sk32,minus(n6,n1))
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p32240,plain,
( leq(sk32,pred(n6))
| leq(n0,sk29)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p32236,c365]) ).
cnf(p32243,plain,
( leq(sk32,pred(n6))
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p32240]) ).
cnf(p29766,plain,
( a_select3(pminus_ds1_filter,sk32,X0) = a_select3(pminus_ds1_filter,X0,sk32)
| ~ leq(X0,pred(n6))
| ~ leq(sk32,pred(n6))
| ~ leq(n0,X0)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p29760,c259]) ).
cnf(p30382,plain,
( leq(n0,sk29)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p29766,p29695]) ).
cnf(p30774,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6))
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p30382]) ).
cnf(p32269,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p32243,p30774]) ).
cnf(p32383,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p32269]) ).
cnf(c364,plain,
( leq(sk31,minus(n6,n1))
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p32241,plain,
( leq(sk31,pred(n6))
| leq(n0,sk29)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p32236,c364]) ).
cnf(p32273,plain,
( leq(sk31,pred(n6))
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p32241]) ).
cnf(p32384,plain,
( leq(n0,sk29)
| a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p32383,p32273]) ).
cnf(p32385,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p32384]) ).
cnf(c366,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p32237,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p32236,c366]) ).
cnf(p32303,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p32237]) ).
cnf(p32386,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk29)
| leq(n0,sk29) ),
inference(superposition,[status(thm)],[p32385,p32303]) ).
cnf(p32387,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p32386]) ).
cnf(p32388,plain,
leq(n0,sk29),
inference(equality_resolution,[status(thm)],[p32387]) ).
cnf(p32390,plain,
( a_select3(r_ds1_filter,sk29,X0) = a_select3(r_ds1_filter,X0,sk29)
| ~ leq(X0,n2)
| ~ leq(sk29,n2)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[p32388,c258]) ).
cnf(p33500,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2)
| ~ leq(sk29,n2) ),
inference(resolution,[status(thm)],[p33460,p32390]) ).
cnf(c322,plain,
( leq(n0,sk31)
| leq(sk29,minus(n3,n1))
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1150,plain,
( leq(n0,sk31)
| leq(sk29,n2)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c322]) ).
cnf(p27902,plain,
( leq(n0,sk31)
| leq(sk29,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p27787,p1150]) ).
cnf(c347,plain,
( leq(n0,sk31)
| leq(sk29,minus(n3,n1))
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p613,plain,
( leq(n0,sk31)
| leq(sk29,n2)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c347]) ).
cnf(p27963,plain,
( leq(n0,sk31)
| leq(sk29,n2)
| leq(n0,sk31)
| leq(sk29,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(resolution,[status(thm)],[p27902,p613]) ).
cnf(p29390,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| leq(sk29,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p27963]) ).
cnf(p29392,plain,
( leq(n0,sk31)
| leq(sk29,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p29390]) ).
cnf(c372,plain,
( leq(n0,sk31)
| leq(sk29,minus(n3,n1))
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p29398,plain,
( leq(n0,sk31)
| leq(sk29,n2)
| leq(n0,sk31)
| leq(sk29,n2) ),
inference(resolution,[status(thm)],[p29392,c372]) ).
cnf(p29401,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| leq(sk29,n2) ),
inference(factoring,[status(thm)],[p29398]) ).
cnf(p29403,plain,
( leq(n0,sk31)
| leq(sk29,n2) ),
inference(factoring,[status(thm)],[p29401]) ).
cnf(p33513,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2) ),
inference(resolution,[status(thm)],[p33500,p29403]) ).
cnf(c327,plain,
( leq(n0,sk31)
| leq(sk30,minus(n3,n1))
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1100,plain,
( leq(n0,sk31)
| leq(sk30,n2)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c327]) ).
cnf(p27898,plain,
( leq(n0,sk31)
| leq(sk30,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p27787,p1100]) ).
fof(f101,axiom,
succ(succ(succ(n0))) = n3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_3) ).
fof(f101_nnf,plain,
succ(succ(succ(n0))) = n3,
inference(nnf_transformation,[status(thm)],[f101]) ).
cnf(c435,plain,
succ(succ(succ(n0))) = n3,
inference(cnf_transformation,[status(esa)],[f101_nnf]) ).
fof(f39,axiom,
! [X] : pred(succ(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pred_succ) ).
fof(f39_nnf,plain,
! [X] : pred(succ(X)) = X,
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [X] : pred(succ(X)) = X,
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c235,plain,
pred(succ(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p537,plain,
pred(n3) = n2,
inference(superposition,[status(thm)],[c435,c235]) ).
cnf(c352,plain,
( leq(n0,sk31)
| leq(sk30,minus(n3,n1))
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p528,plain,
( leq(n0,sk31)
| leq(sk30,pred(n3))
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c352]) ).
cnf(p544,plain,
( leq(n0,sk31)
| leq(sk30,n2)
| leq(sk28,pred(n6)) ),
inference(demodulation,[status(thm)],[p537,p528]) ).
cnf(p27935,plain,
( leq(n0,sk31)
| leq(sk30,n2)
| leq(n0,sk31)
| leq(sk30,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(resolution,[status(thm)],[p27898,p544]) ).
cnf(p29285,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| leq(sk30,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p27935]) ).
cnf(p29287,plain,
( leq(n0,sk31)
| leq(sk30,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p29285]) ).
cnf(c377,plain,
( leq(n0,sk31)
| leq(sk30,minus(n3,n1))
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p29297,plain,
( leq(n0,sk31)
| leq(sk30,n2)
| leq(n0,sk31)
| leq(sk30,n2) ),
inference(resolution,[status(thm)],[p29287,c377]) ).
cnf(p29306,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| leq(sk30,n2) ),
inference(factoring,[status(thm)],[p29297]) ).
cnf(p29308,plain,
( leq(n0,sk31)
| leq(sk30,n2) ),
inference(factoring,[status(thm)],[p29306]) ).
cnf(p33516,plain,
( leq(n0,sk31)
| leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29) ),
inference(resolution,[status(thm)],[p33513,p29308]) ).
cnf(p33640,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29) ),
inference(factoring,[status(thm)],[p33516]) ).
cnf(c332,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p33648,plain,
( leq(n0,sk31)
| leq(sk27,pred(n6))
| leq(n0,sk31) ),
inference(resolution,[status(thm)],[p33640,c332]) ).
cnf(p33674,plain,
( leq(sk27,pred(n6))
| leq(n0,sk31) ),
inference(factoring,[status(thm)],[p33648]) ).
cnf(p33686,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6))
| leq(n0,sk31) ),
inference(resolution,[status(thm)],[p33674,p27787]) ).
cnf(c357,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p33646,plain,
( leq(n0,sk31)
| leq(sk28,pred(n6))
| leq(n0,sk31) ),
inference(resolution,[status(thm)],[p33640,c357]) ).
cnf(p33649,plain,
( leq(sk28,pred(n6))
| leq(n0,sk31) ),
inference(factoring,[status(thm)],[p33646]) ).
cnf(p33776,plain,
( leq(n0,sk31)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(n0,sk31) ),
inference(resolution,[status(thm)],[p33686,p33649]) ).
cnf(p33777,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(n0,sk31) ),
inference(factoring,[status(thm)],[p33776]) ).
cnf(c382,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p33780,plain,
( leq(n0,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk31) ),
inference(resolution,[status(thm)],[p33777,c382]) ).
cnf(p33782,plain,
( a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk31) ),
inference(factoring,[status(thm)],[p33780]) ).
cnf(p33783,plain,
( leq(n0,sk31)
| leq(n0,sk31) ),
inference(resolution,[status(thm)],[p33782,p33640]) ).
cnf(p33784,plain,
leq(n0,sk31),
inference(factoring,[status(thm)],[p33783]) ).
cnf(p33790,plain,
( a_select3(pminus_ds1_filter,sk31,X0) = a_select3(pminus_ds1_filter,X0,sk31)
| ~ leq(X0,pred(n6))
| ~ leq(sk31,pred(n6))
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[p33784,c259]) ).
cnf(c323,plain,
( leq(n0,sk32)
| leq(sk29,minus(n3,n1))
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1096,plain,
( leq(n0,sk32)
| leq(sk29,n2)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c323]) ).
cnf(p27896,plain,
( leq(n0,sk32)
| leq(sk29,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p27787,p1096]) ).
cnf(c348,plain,
( leq(n0,sk32)
| leq(sk29,minus(n3,n1))
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p550,plain,
( leq(n0,sk32)
| leq(sk29,n2)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c348]) ).
cnf(p27913,plain,
( leq(n0,sk32)
| leq(sk29,n2)
| leq(n0,sk32)
| leq(sk29,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(resolution,[status(thm)],[p27896,p550]) ).
cnf(p29201,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| leq(sk29,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p27913]) ).
cnf(p29203,plain,
( leq(n0,sk32)
| leq(sk29,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p29201]) ).
cnf(c373,plain,
( leq(n0,sk32)
| leq(sk29,minus(n3,n1))
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p29216,plain,
( leq(n0,sk32)
| leq(sk29,n2)
| leq(n0,sk32)
| leq(sk29,n2) ),
inference(resolution,[status(thm)],[p29203,c373]) ).
cnf(p29222,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| leq(sk29,n2) ),
inference(factoring,[status(thm)],[p29216]) ).
cnf(p29224,plain,
( leq(n0,sk32)
| leq(sk29,n2) ),
inference(factoring,[status(thm)],[p29222]) ).
cnf(p33512,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2) ),
inference(resolution,[status(thm)],[p33500,p29224]) ).
cnf(c328,plain,
( leq(n0,sk32)
| leq(sk30,minus(n3,n1))
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1104,plain,
( leq(n0,sk32)
| leq(sk30,n2)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c328]) ).
cnf(p27900,plain,
( leq(n0,sk32)
| leq(sk30,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p27787,p1104]) ).
cnf(c353,plain,
( leq(n0,sk32)
| leq(sk30,minus(n3,n1))
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p546,plain,
( leq(n0,sk32)
| leq(sk30,pred(n3))
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c353]) ).
cnf(p548,plain,
( leq(n0,sk32)
| leq(sk30,n2)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[p537,p546]) ).
cnf(p27953,plain,
( leq(n0,sk32)
| leq(sk30,n2)
| leq(n0,sk32)
| leq(sk30,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(resolution,[status(thm)],[p27900,p548]) ).
cnf(p29331,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| leq(sk30,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p27953]) ).
cnf(p29333,plain,
( leq(n0,sk32)
| leq(sk30,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27) ),
inference(factoring,[status(thm)],[p29331]) ).
cnf(c378,plain,
( leq(n0,sk32)
| leq(sk30,minus(n3,n1))
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p29338,plain,
( leq(n0,sk32)
| leq(sk30,n2)
| leq(n0,sk32)
| leq(sk30,n2) ),
inference(resolution,[status(thm)],[p29333,c378]) ).
cnf(p29346,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| leq(sk30,n2) ),
inference(factoring,[status(thm)],[p29338]) ).
cnf(p29348,plain,
( leq(n0,sk32)
| leq(sk30,n2) ),
inference(factoring,[status(thm)],[p29346]) ).
cnf(p33515,plain,
( leq(n0,sk32)
| leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29) ),
inference(resolution,[status(thm)],[p33512,p29348]) ).
cnf(p33580,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29) ),
inference(factoring,[status(thm)],[p33515]) ).
cnf(c333,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p33588,plain,
( leq(n0,sk32)
| leq(sk27,pred(n6))
| leq(n0,sk32) ),
inference(resolution,[status(thm)],[p33580,c333]) ).
cnf(p33614,plain,
( leq(sk27,pred(n6))
| leq(n0,sk32) ),
inference(factoring,[status(thm)],[p33588]) ).
cnf(p33626,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6))
| leq(n0,sk32) ),
inference(resolution,[status(thm)],[p33614,p27787]) ).
cnf(c358,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p33581,plain,
( leq(n0,sk32)
| leq(sk28,pred(n6))
| leq(n0,sk32) ),
inference(resolution,[status(thm)],[p33580,c358]) ).
cnf(p33589,plain,
( leq(sk28,pred(n6))
| leq(n0,sk32) ),
inference(factoring,[status(thm)],[p33581]) ).
cnf(p33711,plain,
( leq(n0,sk32)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(n0,sk32) ),
inference(resolution,[status(thm)],[p33626,p33589]) ).
cnf(p33713,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(n0,sk32) ),
inference(factoring,[status(thm)],[p33711]) ).
cnf(c383,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p33715,plain,
( leq(n0,sk32)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk32) ),
inference(resolution,[status(thm)],[p33713,c383]) ).
cnf(p33719,plain,
( a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(n0,sk32) ),
inference(factoring,[status(thm)],[p33715]) ).
cnf(p33720,plain,
( leq(n0,sk32)
| leq(n0,sk32) ),
inference(resolution,[status(thm)],[p33719,p33580]) ).
cnf(p33722,plain,
leq(n0,sk32),
inference(factoring,[status(thm)],[p33720]) ).
cnf(p34114,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| ~ leq(sk31,pred(n6)) ),
inference(resolution,[status(thm)],[p33790,p33722]) ).
cnf(c329,plain,
( leq(sk31,minus(n6,n1))
| leq(sk30,minus(n3,n1))
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1132,plain,
( leq(sk31,pred(n6))
| leq(sk30,n2)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c329]) ).
cnf(p34166,plain,
( leq(sk30,n2)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6)) ),
inference(resolution,[status(thm)],[p34114,p1132]) ).
cnf(c330,plain,
( leq(sk32,minus(n6,n1))
| leq(sk30,minus(n3,n1))
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1148,plain,
( leq(sk32,pred(n6))
| leq(sk30,n2)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c330]) ).
cnf(p34206,plain,
( leq(sk30,n2)
| leq(sk27,pred(n6))
| leq(sk30,n2)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(resolution,[status(thm)],[p34166,p1148]) ).
cnf(p34892,plain,
( leq(sk30,n2)
| leq(sk30,n2)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(factoring,[status(thm)],[p34206]) ).
cnf(p34894,plain,
( leq(sk30,n2)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(factoring,[status(thm)],[p34892]) ).
cnf(c331,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk30,minus(n3,n1))
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p34895,plain,
( leq(sk30,n2)
| leq(sk27,pred(n6))
| leq(sk30,n2)
| leq(sk27,pred(n6)) ),
inference(resolution,[status(thm)],[p34894,c331]) ).
cnf(p34896,plain,
( leq(sk30,n2)
| leq(sk30,n2)
| leq(sk27,pred(n6)) ),
inference(factoring,[status(thm)],[p34895]) ).
cnf(p34898,plain,
( leq(sk30,n2)
| leq(sk27,pred(n6)) ),
inference(factoring,[status(thm)],[p34896]) ).
cnf(p34910,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6))
| leq(sk30,n2) ),
inference(resolution,[status(thm)],[p34898,p27787]) ).
cnf(c354,plain,
( leq(sk31,minus(n6,n1))
| leq(sk30,minus(n3,n1))
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p498,plain,
( leq(sk31,pred(n6))
| leq(sk30,pred(n3))
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c354]) ).
cnf(p538,plain,
( leq(sk31,pred(n6))
| leq(sk30,n2)
| leq(sk28,pred(n6)) ),
inference(demodulation,[status(thm)],[p537,p498]) ).
cnf(p34163,plain,
( leq(sk30,n2)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6)) ),
inference(resolution,[status(thm)],[p34114,p538]) ).
cnf(c355,plain,
( leq(sk32,minus(n6,n1))
| leq(sk30,minus(n3,n1))
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p535,plain,
( leq(sk32,pred(n6))
| leq(sk30,pred(n3))
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c355]) ).
cnf(p545,plain,
( leq(sk32,pred(n6))
| leq(sk30,n2)
| leq(sk28,pred(n6)) ),
inference(demodulation,[status(thm)],[p537,p535]) ).
cnf(p34198,plain,
( leq(sk30,n2)
| leq(sk28,pred(n6))
| leq(sk30,n2)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(resolution,[status(thm)],[p34163,p545]) ).
cnf(p34374,plain,
( leq(sk30,n2)
| leq(sk30,n2)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(factoring,[status(thm)],[p34198]) ).
cnf(p34376,plain,
( leq(sk30,n2)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(factoring,[status(thm)],[p34374]) ).
cnf(c356,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk30,minus(n3,n1))
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p34378,plain,
( leq(sk30,n2)
| leq(sk28,pred(n6))
| leq(sk30,n2)
| leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p34376,c356]) ).
cnf(p34424,plain,
( leq(sk30,n2)
| leq(sk30,n2)
| leq(sk28,pred(n6)) ),
inference(factoring,[status(thm)],[p34378]) ).
cnf(p34426,plain,
( leq(sk30,n2)
| leq(sk28,pred(n6)) ),
inference(factoring,[status(thm)],[p34424]) ).
cnf(p35079,plain,
( leq(sk30,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(sk30,n2) ),
inference(resolution,[status(thm)],[p34910,p34426]) ).
cnf(p35080,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(sk30,n2) ),
inference(factoring,[status(thm)],[p35079]) ).
cnf(c379,plain,
( leq(sk31,minus(n6,n1))
| leq(sk30,minus(n3,n1))
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35084,plain,
( leq(sk31,pred(n6))
| leq(sk30,n2)
| leq(sk30,n2) ),
inference(resolution,[status(thm)],[p35080,c379]) ).
cnf(p35087,plain,
( leq(sk31,pred(n6))
| leq(sk30,n2) ),
inference(factoring,[status(thm)],[p35084]) ).
cnf(p35116,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(sk30,n2) ),
inference(resolution,[status(thm)],[p35087,p34114]) ).
cnf(c380,plain,
( leq(sk32,minus(n6,n1))
| leq(sk30,minus(n3,n1))
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35085,plain,
( leq(sk32,pred(n6))
| leq(sk30,n2)
| leq(sk30,n2) ),
inference(resolution,[status(thm)],[p35080,c380]) ).
cnf(p35121,plain,
( leq(sk32,pred(n6))
| leq(sk30,n2) ),
inference(factoring,[status(thm)],[p35085]) ).
cnf(p35182,plain,
( leq(sk30,n2)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk30,n2) ),
inference(resolution,[status(thm)],[p35116,p35121]) ).
cnf(p35183,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk30,n2) ),
inference(factoring,[status(thm)],[p35182]) ).
cnf(c381,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk30,minus(n3,n1))
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35083,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk30,n2)
| leq(sk30,n2) ),
inference(resolution,[status(thm)],[p35080,c381]) ).
cnf(p35155,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk30,n2) ),
inference(factoring,[status(thm)],[p35083]) ).
cnf(p35184,plain,
( leq(sk30,n2)
| leq(sk30,n2) ),
inference(resolution,[status(thm)],[p35183,p35155]) ).
cnf(p35185,plain,
leq(sk30,n2),
inference(factoring,[status(thm)],[p35184]) ).
cnf(c324,plain,
( leq(sk31,minus(n6,n1))
| leq(sk29,minus(n3,n1))
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1111,plain,
( leq(sk31,pred(n6))
| leq(sk29,n2)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c324]) ).
cnf(p34165,plain,
( leq(sk29,n2)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6)) ),
inference(resolution,[status(thm)],[p34114,p1111]) ).
cnf(c325,plain,
( leq(sk32,minus(n6,n1))
| leq(sk29,minus(n3,n1))
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1127,plain,
( leq(sk32,pred(n6))
| leq(sk29,n2)
| leq(sk27,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c325]) ).
cnf(p34204,plain,
( leq(sk29,n2)
| leq(sk27,pred(n6))
| leq(sk29,n2)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(resolution,[status(thm)],[p34165,p1127]) ).
cnf(p34583,plain,
( leq(sk29,n2)
| leq(sk29,n2)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(factoring,[status(thm)],[p34204]) ).
cnf(p34585,plain,
( leq(sk29,n2)
| leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(factoring,[status(thm)],[p34583]) ).
cnf(c326,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk29,minus(n3,n1))
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p34586,plain,
( leq(sk29,n2)
| leq(sk27,pred(n6))
| leq(sk29,n2)
| leq(sk27,pred(n6)) ),
inference(resolution,[status(thm)],[p34585,c326]) ).
cnf(p34588,plain,
( leq(sk29,n2)
| leq(sk29,n2)
| leq(sk27,pred(n6)) ),
inference(factoring,[status(thm)],[p34586]) ).
cnf(p34590,plain,
( leq(sk29,n2)
| leq(sk27,pred(n6)) ),
inference(factoring,[status(thm)],[p34588]) ).
cnf(p34602,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| ~ leq(sk28,pred(n6))
| leq(sk29,n2) ),
inference(resolution,[status(thm)],[p34590,p27787]) ).
cnf(c349,plain,
( leq(sk31,minus(n6,n1))
| leq(sk29,minus(n3,n1))
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p549,plain,
( leq(sk31,pred(n6))
| leq(sk29,n2)
| leq(sk28,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c349]) ).
cnf(p34164,plain,
( leq(sk29,n2)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6)) ),
inference(resolution,[status(thm)],[p34114,p549]) ).
fof(f6,axiom,
! [X,Y] :
( geq(X,Y)
<=> leq(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_geq) ).
fof(f6_nnf,plain,
! [X,Y] :
( ( ~ leq(Y,X)
| geq(X,Y) )
& ( leq(Y,X)
| ~ geq(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y] :
( ( ~ leq(Y,X)
| geq(X,Y) )
& ( leq(Y,X)
| ~ geq(X,Y) ) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c8,plain,
( ~ leq(X1,X0)
| geq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(c350,plain,
( leq(sk32,minus(n6,n1))
| leq(sk29,minus(n3,n1))
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p600,plain,
( leq(sk29,n2)
| leq(sk28,pred(n6))
| geq(pred(n6),sk32) ),
inference(resolution,[status(thm)],[c8,c350]) ).
cnf(c7,plain,
( leq(X1,X0)
| ~ geq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p608,plain,
( leq(sk32,pred(n6))
| leq(sk29,n2)
| leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p600,c7]) ).
cnf(p34202,plain,
( leq(sk29,n2)
| leq(sk28,pred(n6))
| leq(sk29,n2)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(resolution,[status(thm)],[p34164,p608]) ).
cnf(p34507,plain,
( leq(sk29,n2)
| leq(sk29,n2)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(factoring,[status(thm)],[p34202]) ).
cnf(p34509,plain,
( leq(sk29,n2)
| leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31) ),
inference(factoring,[status(thm)],[p34507]) ).
cnf(c351,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk29,minus(n3,n1))
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p34510,plain,
( leq(sk29,n2)
| leq(sk28,pred(n6))
| leq(sk29,n2)
| leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p34509,c351]) ).
cnf(p34512,plain,
( leq(sk29,n2)
| leq(sk29,n2)
| leq(sk28,pred(n6)) ),
inference(factoring,[status(thm)],[p34510]) ).
cnf(p34514,plain,
( leq(sk29,n2)
| leq(sk28,pred(n6)) ),
inference(factoring,[status(thm)],[p34512]) ).
cnf(p34671,plain,
( leq(sk29,n2)
| a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(sk29,n2) ),
inference(resolution,[status(thm)],[p34602,p34514]) ).
cnf(p34755,plain,
( a_select3(q_ds1_filter,sk27,sk28) = a_select3(q_ds1_filter,sk28,sk27)
| leq(sk29,n2) ),
inference(factoring,[status(thm)],[p34671]) ).
cnf(c374,plain,
( leq(sk31,minus(n6,n1))
| leq(sk29,minus(n3,n1))
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p34759,plain,
( leq(sk31,pred(n6))
| leq(sk29,n2)
| leq(sk29,n2) ),
inference(resolution,[status(thm)],[p34755,c374]) ).
cnf(p34763,plain,
( leq(sk31,pred(n6))
| leq(sk29,n2) ),
inference(factoring,[status(thm)],[p34759]) ).
cnf(p34792,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(sk29,n2) ),
inference(resolution,[status(thm)],[p34763,p34114]) ).
cnf(c375,plain,
( leq(sk32,minus(n6,n1))
| leq(sk29,minus(n3,n1))
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p34761,plain,
( leq(sk32,pred(n6))
| leq(sk29,n2)
| leq(sk29,n2) ),
inference(resolution,[status(thm)],[p34755,c375]) ).
cnf(p34800,plain,
( leq(sk32,pred(n6))
| leq(sk29,n2) ),
inference(factoring,[status(thm)],[p34761]) ).
cnf(p34867,plain,
( leq(sk29,n2)
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk29,n2) ),
inference(resolution,[status(thm)],[p34792,p34800]) ).
cnf(p34868,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk29,n2) ),
inference(factoring,[status(thm)],[p34867]) ).
cnf(c376,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk29,minus(n3,n1))
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p34760,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk29,n2)
| leq(sk29,n2) ),
inference(resolution,[status(thm)],[p34755,c376]) ).
cnf(p34837,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk29,n2) ),
inference(factoring,[status(thm)],[p34760]) ).
cnf(p34869,plain,
( leq(sk29,n2)
| leq(sk29,n2) ),
inference(resolution,[status(thm)],[p34868,p34837]) ).
cnf(p34870,plain,
leq(sk29,n2),
inference(factoring,[status(thm)],[p34869]) ).
cnf(p34886,plain,
( a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29)
| ~ leq(sk30,n2) ),
inference(resolution,[status(thm)],[p34870,p33500]) ).
cnf(p35204,plain,
a_select3(r_ds1_filter,sk29,sk30) = a_select3(r_ds1_filter,sk30,sk29),
inference(resolution,[status(thm)],[p35185,p34886]) ).
cnf(c334,plain,
( leq(sk31,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35210,plain,
( leq(sk31,pred(n6))
| leq(sk27,pred(n6)) ),
inference(resolution,[status(thm)],[p35204,c334]) ).
cnf(p35321,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(sk27,pred(n6)) ),
inference(resolution,[status(thm)],[p35210,p34114]) ).
cnf(c335,plain,
( leq(sk32,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35207,plain,
( leq(sk32,pred(n6))
| leq(sk27,pred(n6)) ),
inference(resolution,[status(thm)],[p35204,c335]) ).
cnf(p35347,plain,
( leq(sk27,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk27,pred(n6)) ),
inference(resolution,[status(thm)],[p35321,p35207]) ).
cnf(p35443,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk27,pred(n6)) ),
inference(factoring,[status(thm)],[p35347]) ).
cnf(c336,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(sk27,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35208,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk27,pred(n6)) ),
inference(resolution,[status(thm)],[p35204,c336]) ).
cnf(p35444,plain,
( leq(sk27,pred(n6))
| leq(sk27,pred(n6)) ),
inference(resolution,[status(thm)],[p35443,p35208]) ).
cnf(p35445,plain,
leq(sk27,pred(n6)),
inference(factoring,[status(thm)],[p35444]) ).
cnf(c359,plain,
( leq(sk31,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35205,plain,
( leq(sk31,pred(n6))
| leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p35204,c359]) ).
cnf(p35237,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| ~ leq(sk32,pred(n6))
| leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p35205,p34114]) ).
cnf(c360,plain,
( leq(sk32,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35206,plain,
( leq(sk32,pred(n6))
| leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p35204,c360]) ).
cnf(p35338,plain,
( leq(sk28,pred(n6))
| a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p35237,p35206]) ).
cnf(p35349,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) = a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk28,pred(n6)) ),
inference(factoring,[status(thm)],[p35338]) ).
cnf(c361,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| leq(sk28,minus(n6,n1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35209,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p35204,c361]) ).
cnf(p35351,plain,
( leq(sk28,pred(n6))
| leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p35349,p35209]) ).
cnf(p35384,plain,
leq(sk28,pred(n6)),
inference(factoring,[status(thm)],[p35351]) ).
cnf(p8023,plain,
( a_select3(q_ds1_filter,sk28,X0) = a_select3(q_ds1_filter,X0,sk28)
| ~ leq(X0,pred(n6))
| ~ leq(sk28,pred(n6))
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[p8022,c257]) ).
cnf(p27491,plain,
( a_select3(q_ds1_filter,sk28,sk27) = a_select3(q_ds1_filter,sk27,sk28)
| ~ leq(sk27,pred(n6))
| ~ leq(sk28,pred(n6)) ),
inference(resolution,[status(thm)],[p27457,p8023]) ).
cnf(p35405,plain,
( a_select3(q_ds1_filter,sk28,sk27) = a_select3(q_ds1_filter,sk27,sk28)
| ~ leq(sk27,pred(n6)) ),
inference(resolution,[status(thm)],[p35384,p27491]) ).
cnf(p35477,plain,
a_select3(q_ds1_filter,sk28,sk27) = a_select3(q_ds1_filter,sk27,sk28),
inference(resolution,[status(thm)],[p35445,p35405]) ).
cnf(p33462,plain,
( a_select3(r_ds1_filter,sk30,X0) = a_select3(r_ds1_filter,X0,sk30)
| ~ leq(X0,n2)
| ~ leq(sk30,n2)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[p33460,c258]) ).
cnf(p33840,plain,
( a_select3(r_ds1_filter,sk30,sk29) = a_select3(r_ds1_filter,sk29,sk30)
| ~ leq(sk29,n2)
| ~ leq(sk30,n2) ),
inference(resolution,[status(thm)],[p33462,p32388]) ).
cnf(p35201,plain,
( a_select3(r_ds1_filter,sk30,sk29) = a_select3(r_ds1_filter,sk29,sk30)
| ~ leq(sk29,n2) ),
inference(resolution,[status(thm)],[p35185,p33840]) ).
cnf(p35326,plain,
a_select3(r_ds1_filter,sk30,sk29) = a_select3(r_ds1_filter,sk29,sk30),
inference(resolution,[status(thm)],[p35201,p34870]) ).
cnf(c385,plain,
( leq(sk32,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35334,plain,
( leq(sk32,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk29,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(demodulation,[status(thm)],[p35326,c385]) ).
cnf(p35485,plain,
( leq(sk32,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk29,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk27,sk28) ),
inference(demodulation,[status(thm)],[p35477,p35334]) ).
cnf(p35564,plain,
( leq(sk32,pred(n6))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk29,sk30) ),
inference(equality_resolution,[status(thm)],[p35485]) ).
cnf(p35566,plain,
leq(sk32,pred(n6)),
inference(equality_resolution,[status(thm)],[p35564]) ).
cnf(p33728,plain,
( a_select3(pminus_ds1_filter,sk32,X0) = a_select3(pminus_ds1_filter,X0,sk32)
| ~ leq(X0,pred(n6))
| ~ leq(sk32,pred(n6))
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[p33722,c259]) ).
cnf(p33978,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6))
| ~ leq(sk32,pred(n6)) ),
inference(resolution,[status(thm)],[p33728,p33784]) ).
cnf(p35595,plain,
( a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32)
| ~ leq(sk31,pred(n6)) ),
inference(resolution,[status(thm)],[p35566,p33978]) ).
cnf(c384,plain,
( leq(sk31,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35333,plain,
( leq(sk31,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk29,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(demodulation,[status(thm)],[p35326,c384]) ).
cnf(p35484,plain,
( leq(sk31,minus(n6,n1))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk29,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk27,sk28) ),
inference(demodulation,[status(thm)],[p35477,p35333]) ).
cnf(p35505,plain,
( leq(sk31,pred(n6))
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk29,sk30) ),
inference(equality_resolution,[status(thm)],[p35484]) ).
cnf(p35507,plain,
leq(sk31,pred(n6)),
inference(equality_resolution,[status(thm)],[p35505]) ).
cnf(p35611,plain,
a_select3(pminus_ds1_filter,sk32,sk31) = a_select3(pminus_ds1_filter,sk31,sk32),
inference(resolution,[status(thm)],[p35595,p35507]) ).
cnf(c386,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p35335,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk29,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27) ),
inference(demodulation,[status(thm)],[p35326,c386]) ).
cnf(p35486,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk29,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk27,sk28) ),
inference(demodulation,[status(thm)],[p35477,p35335]) ).
cnf(p35620,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk29,sk30)
| a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk27,sk28) ),
inference(demodulation,[status(thm)],[p35611,p35486]) ).
cnf(p35638,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32)
| a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk29,sk30) ),
inference(equality_resolution,[status(thm)],[p35620]) ).
cnf(p35641,plain,
a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk31,sk32),
inference(equality_resolution,[status(thm)],[p35638]) ).
cnf(p35643,plain,
$false,
inference(equality_resolution,[status(thm)],[p35641]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV116+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.17/5.46 % Computer : n009.cluster.edu
% 0.17/5.46 % Model : x86_64 x86_64
% 0.17/5.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.46 % Memory : 8046.5625MB
% 0.17/5.46 % OS : Linux 6.8.0-71-generic
% 0.17/5.46 % CPULimit : 300
% 0.17/5.46 % WCLimit : 300
% 0.17/5.46 % DateTime : Thu Sep 24 18:33:05 UTC 2026
% 0.17/5.46 % CPUTime :
% 0.17/5.46 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 247.81/41.36 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 247.81/41.36 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------