%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV112+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.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 56.13s 7.65s
% Output : Proof 56.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 2
% Syntax : Number of formulae : 184 ( 26 unt; 0 def)
% Number of atoms : 583 ( 56 equ)
% Maximal formula atoms : 51 ( 3 avg)
% Number of connectives : 573 ( 174 ~; 249 |; 126 &)
% ( 0 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 49 ( 47 usr; 25 prp; 0-10 aty)
% Number of functors : 24 ( 24 usr; 20 con; 0-3 aty)
% Number of variables : 226 ( 80 sgn 59 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f52,conjecture,
( ( ! [I] :
( ( leq(I,minus(pv57,n1))
& leq(n0,I) )
=> ! [J] :
( ( leq(J,minus(n6,n1))
& leq(n0,J) )
=> a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I) ) )
& ! [G,H] :
( ( leq(H,minus(n6,n1))
& leq(G,pv57)
& leq(n0,H)
& leq(n0,G) )
=> a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G) )
& ! [E,F] :
( ( leq(F,minus(n6,n1))
& leq(E,minus(n6,n1))
& leq(n0,F)
& leq(n0,E) )
=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) )
& ! [C,D] :
( ( leq(D,minus(n3,n1))
& leq(C,minus(n3,n1))
& leq(n0,D)
& leq(n0,C) )
=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) )
& ! [A,B] :
( ( leq(B,minus(n6,n1))
& leq(A,minus(n6,n1))
& leq(n0,B)
& leq(n0,A) )
=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) )
& leq(pv57,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv57)
& leq(n0,pv5) )
=> ( ! [Q] :
( ( leq(Q,minus(plus(n1,pv57),n1))
& leq(n0,Q) )
=> ! [R] :
( ( leq(R,minus(n6,n1))
& leq(n0,R) )
=> a_select3(id_ds1_filter,Q,R) = a_select3(id_ds1_filter,R,Q) ) )
& ! [O,P] :
( ( leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
=> a_select3(pminus_ds1_filter,O,P) = a_select3(pminus_ds1_filter,P,O) )
& ! [M,N] :
( ( leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
=> a_select3(r_ds1_filter,M,N) = a_select3(r_ds1_filter,N,M) )
& ! [K,L] :
( ( leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
=> a_select3(q_ds1_filter,K,L) = a_select3(q_ds1_filter,L,K) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quaternion_ds1_symm_0005) ).
fof(f52_neg,negated_conjecture,
~ ( ( ! [I] :
( ( leq(I,minus(pv57,n1))
& leq(n0,I) )
=> ! [J] :
( ( leq(J,minus(n6,n1))
& leq(n0,J) )
=> a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I) ) )
& ! [G,H] :
( ( leq(H,minus(n6,n1))
& leq(G,pv57)
& leq(n0,H)
& leq(n0,G) )
=> a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G) )
& ! [E,F] :
( ( leq(F,minus(n6,n1))
& leq(E,minus(n6,n1))
& leq(n0,F)
& leq(n0,E) )
=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) )
& ! [C,D] :
( ( leq(D,minus(n3,n1))
& leq(C,minus(n3,n1))
& leq(n0,D)
& leq(n0,C) )
=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) )
& ! [A,B] :
( ( leq(B,minus(n6,n1))
& leq(A,minus(n6,n1))
& leq(n0,B)
& leq(n0,A) )
=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) )
& leq(pv57,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv57)
& leq(n0,pv5) )
=> ( ! [Q] :
( ( leq(Q,minus(plus(n1,pv57),n1))
& leq(n0,Q) )
=> ! [R] :
( ( leq(R,minus(n6,n1))
& leq(n0,R) )
=> a_select3(id_ds1_filter,Q,R) = a_select3(id_ds1_filter,R,Q) ) )
& ! [O,P] :
( ( leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
=> a_select3(pminus_ds1_filter,O,P) = a_select3(pminus_ds1_filter,P,O) )
& ! [M,N] :
( ( leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
=> a_select3(r_ds1_filter,M,N) = a_select3(r_ds1_filter,N,M) )
& ! [K,L] :
( ( leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
=> a_select3(q_ds1_filter,K,L) = a_select3(q_ds1_filter,L,K) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f52_nnf,plain,
( ( ? [Q] :
( ? [R] :
( a_select3(id_ds1_filter,Q,R) != a_select3(id_ds1_filter,R,Q)
& leq(R,minus(n6,n1))
& leq(n0,R) )
& leq(Q,minus(plus(n1,pv57),n1))
& leq(n0,Q) )
| ? [O,P] :
( a_select3(pminus_ds1_filter,O,P) != a_select3(pminus_ds1_filter,P,O)
& leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
| ? [M,N] :
( a_select3(r_ds1_filter,M,N) != a_select3(r_ds1_filter,N,M)
& leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
| ? [K,L] :
( a_select3(q_ds1_filter,K,L) != a_select3(q_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5) )
& ! [I] :
( ! [J] :
( a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I)
| ~ leq(J,minus(n6,n1))
| ~ leq(n0,J) )
| ~ leq(I,minus(pv57,n1))
| ~ leq(n0,I) )
& ! [G,H] :
( a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G)
| ~ leq(H,minus(n6,n1))
| ~ leq(G,pv57)
| ~ leq(n0,H)
| ~ leq(n0,G) )
& ! [E,F] :
( a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E)
| ~ leq(F,minus(n6,n1))
| ~ leq(E,minus(n6,n1))
| ~ leq(n0,F)
| ~ leq(n0,E) )
& ! [C,D] :
( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C)
| ~ leq(D,minus(n3,n1))
| ~ leq(C,minus(n3,n1))
| ~ leq(n0,D)
| ~ leq(n0,C) )
& ! [A,B] :
( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A)
| ~ leq(B,minus(n6,n1))
| ~ leq(A,minus(n6,n1))
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv57,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv57)
& leq(n0,pv5) ),
inference(nnf_transformation,[status(thm)],[f52_neg]) ).
fof(f52_sk,plain,
! [A,B,C,D,E,F,G,H,I,J] :
( ( ( a_select3(id_ds1_filter,sk33,sk34) != a_select3(id_ds1_filter,sk34,sk33)
& leq(sk34,minus(n6,n1))
& leq(n0,sk34)
& leq(sk33,minus(plus(n1,pv57),n1))
& leq(n0,sk33) )
| ( 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) )
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5) )
& ( a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I)
| ~ leq(J,minus(n6,n1))
| ~ leq(n0,J)
| ~ leq(I,minus(pv57,n1))
| ~ leq(n0,I) )
& ( a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G)
| ~ leq(H,minus(n6,n1))
| ~ leq(G,pv57)
| ~ 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(pv57,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv57)
& leq(n0,pv5) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk27,sk28,sk29,sk30,sk31,sk32,sk33,sk34])],[f52_nnf]) ).
cnf(c321,plain,
( def17(X0,X1,X2,X3,X4,X5)
| ~ def22(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(c402,plain,
( def27(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ def49(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(c405,plain,
def49(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p457,plain,
def27(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9),
inference(resolution,[status(thm)],[c402,c405]) ).
cnf(c336,plain,
( def22(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ def27(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p459,plain,
def22(X0,X1,X2,X3,X4,X5,X6,X7),
inference(resolution,[status(thm)],[p457,c336]) ).
cnf(p7058,plain,
def17(X0,X1,X2,X3,X4,X5),
inference(resolution,[status(thm)],[c321,p459]) ).
cnf(c306,plain,
( def12(X0,X1,X2,X3)
| ~ def17(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7060,plain,
def12(X0,X1,X2,X3),
inference(resolution,[status(thm)],[p7058,c306]) ).
cnf(c291,plain,
( def7(X0,X1)
| ~ def12(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7062,plain,
def7(X0,X1),
inference(resolution,[status(thm)],[p7060,c291]) ).
cnf(c277,plain,
( def6(X0,X1)
| ~ def7(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7064,plain,
def6(X0,X1),
inference(resolution,[status(thm)],[p7062,c277]) ).
cnf(c273,plain,
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| def5(X0,X1)
| ~ def6(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7073,plain,
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| def5(X0,X1) ),
inference(resolution,[status(thm)],[p7064,c273]) ).
cnf(c292,plain,
( def11(X2,X3)
| ~ def12(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7063,plain,
def11(X0,X1),
inference(resolution,[status(thm)],[p7060,c292]) ).
cnf(c288,plain,
( a_select3(r_ds1_filter,X2,X3) = a_select3(r_ds1_filter,X3,X2)
| def10(X2,X3)
| ~ def11(X2,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7072,plain,
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| def10(X0,X1) ),
inference(resolution,[status(thm)],[p7063,c288]) ).
cnf(c307,plain,
( def16(X4,X5)
| ~ def17(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7059,plain,
def16(X0,X1),
inference(resolution,[status(thm)],[p7058,c307]) ).
cnf(c303,plain,
( a_select3(pminus_ds1_filter,X4,X5) = a_select3(pminus_ds1_filter,X5,X4)
| def15(X4,X5)
| ~ def16(X4,X5) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7061,plain,
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| def15(X0,X1) ),
inference(resolution,[status(thm)],[p7059,c303]) ).
fof(f38,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox/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(c403,plain,
( def48
| ~ def49(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p500,plain,
def48,
inference(resolution,[status(thm)],[c403,c405]) ).
cnf(c399,plain,
( def47
| def43
| ~ def48 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p501,plain,
( def47
| def43 ),
inference(resolution,[status(thm)],[p500,c399]) ).
cnf(c396,plain,
( def44
| ~ def47 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p503,plain,
( def44
| def43 ),
inference(resolution,[status(thm)],[p501,c396]) ).
cnf(c388,plain,
( leq(sk33,minus(plus(n1,pv57),n1))
| ~ def44 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p507,plain,
( leq(sk33,minus(plus(n1,pv57),n1))
| def43 ),
inference(resolution,[status(thm)],[p503,c388]) ).
cnf(p651,plain,
( leq(sk33,pv57)
| def43 ),
inference(superposition,[status(thm)],[c234,p507]) ).
cnf(c315,plain,
( ~ leq(X7,minus(n6,n1))
| def19(X6,X7)
| ~ def20(X6,X7) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(c318,plain,
( a_select3(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6)
| def20(X6,X7)
| ~ def21(X6,X7) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(c322,plain,
( def21(X6,X7)
| ~ def22(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p557,plain,
def21(X0,X1),
inference(resolution,[status(thm)],[c322,p459]) ).
cnf(p558,plain,
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| def20(X0,X1) ),
inference(resolution,[status(thm)],[c318,p557]) ).
cnf(c397,plain,
( def46
| ~ def47 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p502,plain,
( def46
| def43 ),
inference(resolution,[status(thm)],[p501,c397]) ).
cnf(c394,plain,
( a_select3(id_ds1_filter,sk33,sk34) != a_select3(id_ds1_filter,sk34,sk33)
| ~ def46 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p505,plain,
( a_select3(id_ds1_filter,sk33,sk34) != a_select3(id_ds1_filter,sk34,sk33)
| def43 ),
inference(resolution,[status(thm)],[p502,c394]) ).
cnf(p562,plain,
( def43
| def20(sk33,sk34) ),
inference(resolution,[status(thm)],[p558,p505]) ).
cnf(p569,plain,
( def43
| ~ leq(sk34,minus(n6,n1))
| def19(sk33,sk34) ),
inference(resolution,[status(thm)],[c315,p562]) ).
cnf(c393,plain,
( def45
| ~ def46 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p504,plain,
( def45
| def43 ),
inference(resolution,[status(thm)],[p502,c393]) ).
cnf(c391,plain,
( leq(sk34,minus(n6,n1))
| ~ def45 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p509,plain,
( leq(sk34,minus(n6,n1))
| def43 ),
inference(resolution,[status(thm)],[p504,c391]) ).
cnf(p620,plain,
( def43
| def43
| def19(sk33,sk34) ),
inference(resolution,[status(thm)],[p569,p509]) ).
cnf(p632,plain,
( def43
| def19(sk33,sk34) ),
inference(factoring,[status(thm)],[p620]) ).
cnf(c312,plain,
( ~ leq(X6,pv57)
| def18(X6,X7)
| ~ def19(X6,X7) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p633,plain,
( ~ leq(sk33,pv57)
| def18(sk33,sk34)
| def43 ),
inference(resolution,[status(thm)],[p632,c312]) ).
cnf(p665,plain,
( def18(sk33,sk34)
| def43
| def43 ),
inference(resolution,[status(thm)],[p651,p633]) ).
cnf(p673,plain,
( def18(sk33,sk34)
| def43 ),
inference(factoring,[status(thm)],[p665]) ).
cnf(c309,plain,
( ~ leq(n0,X7)
| ~ leq(n0,X6)
| ~ def18(X6,X7) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p674,plain,
( ~ leq(n0,sk34)
| ~ leq(n0,sk33)
| def43 ),
inference(resolution,[status(thm)],[p673,c309]) ).
cnf(c387,plain,
( leq(n0,sk33)
| ~ def44 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p506,plain,
( leq(n0,sk33)
| def43 ),
inference(resolution,[status(thm)],[p503,c387]) ).
cnf(p680,plain,
( def43
| ~ leq(n0,sk34)
| def43 ),
inference(resolution,[status(thm)],[p674,p506]) ).
cnf(p682,plain,
( ~ leq(n0,sk34)
| def43 ),
inference(factoring,[status(thm)],[p680]) ).
cnf(c390,plain,
( leq(n0,sk34)
| ~ def45 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p508,plain,
( leq(n0,sk34)
| def43 ),
inference(resolution,[status(thm)],[p504,c390]) ).
cnf(p685,plain,
( def43
| def43 ),
inference(resolution,[status(thm)],[p682,p508]) ).
cnf(p686,plain,
def43,
inference(factoring,[status(thm)],[p685]) ).
cnf(c384,plain,
( def42
| def38
| ~ def43 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p687,plain,
( def42
| def38 ),
inference(resolution,[status(thm)],[p686,c384]) ).
cnf(c382,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| ~ def42 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p688,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| def38 ),
inference(resolution,[status(thm)],[p687,c382]) ).
cnf(p7268,plain,
( def38
| def15(sk31,sk32) ),
inference(resolution,[status(thm)],[p7061,p688]) ).
cnf(c300,plain,
( ~ leq(X5,minus(n6,n1))
| def14(X4,X5)
| ~ def15(X4,X5) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7271,plain,
( ~ leq(sk32,pred(n6))
| def14(sk31,sk32)
| def38 ),
inference(resolution,[status(thm)],[p7268,c300]) ).
cnf(c381,plain,
( def41
| ~ def42 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p689,plain,
( def41
| def38 ),
inference(resolution,[status(thm)],[p687,c381]) ).
cnf(c379,plain,
( leq(sk32,minus(n6,n1))
| ~ def41 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p691,plain,
( leq(sk32,pred(n6))
| def38 ),
inference(resolution,[status(thm)],[p689,c379]) ).
cnf(p7279,plain,
( def38
| def14(sk31,sk32)
| def38 ),
inference(resolution,[status(thm)],[p7271,p691]) ).
cnf(p7281,plain,
( def14(sk31,sk32)
| def38 ),
inference(factoring,[status(thm)],[p7279]) ).
cnf(c297,plain,
( ~ leq(X4,minus(n6,n1))
| def13(X4,X5)
| ~ def14(X4,X5) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7282,plain,
( ~ leq(sk31,pred(n6))
| def13(sk31,sk32)
| def38 ),
inference(resolution,[status(thm)],[p7281,c297]) ).
cnf(c378,plain,
( def40
| ~ def41 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p690,plain,
( def40
| def38 ),
inference(resolution,[status(thm)],[p689,c378]) ).
cnf(c376,plain,
( leq(sk31,minus(n6,n1))
| ~ def40 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p692,plain,
( leq(sk31,pred(n6))
| def38 ),
inference(resolution,[status(thm)],[p690,c376]) ).
cnf(p7290,plain,
( def38
| def13(sk31,sk32)
| def38 ),
inference(resolution,[status(thm)],[p7282,p692]) ).
cnf(p7292,plain,
( def13(sk31,sk32)
| def38 ),
inference(factoring,[status(thm)],[p7290]) ).
cnf(c294,plain,
( ~ leq(n0,X5)
| ~ leq(n0,X4)
| ~ def13(X4,X5) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7293,plain,
( ~ leq(n0,sk32)
| ~ leq(n0,sk31)
| def38 ),
inference(resolution,[status(thm)],[p7292,c294]) ).
cnf(c375,plain,
( def39
| ~ def40 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p693,plain,
( def39
| def38 ),
inference(resolution,[status(thm)],[p690,c375]) ).
cnf(c372,plain,
( leq(n0,sk31)
| ~ def39 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p695,plain,
( leq(n0,sk31)
| def38 ),
inference(resolution,[status(thm)],[p693,c372]) ).
cnf(p7296,plain,
( def38
| ~ leq(n0,sk32)
| def38 ),
inference(resolution,[status(thm)],[p7293,p695]) ).
cnf(p7297,plain,
( ~ leq(n0,sk32)
| def38 ),
inference(factoring,[status(thm)],[p7296]) ).
cnf(c373,plain,
( leq(n0,sk32)
| ~ def39 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p694,plain,
( leq(n0,sk32)
| def38 ),
inference(resolution,[status(thm)],[p693,c373]) ).
cnf(p7300,plain,
( def38
| def38 ),
inference(resolution,[status(thm)],[p7297,p694]) ).
cnf(p7301,plain,
def38,
inference(factoring,[status(thm)],[p7300]) ).
cnf(c369,plain,
( def37
| def33
| ~ def38 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7302,plain,
( def37
| def33 ),
inference(resolution,[status(thm)],[p7301,c369]) ).
cnf(c367,plain,
( a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| ~ def37 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7303,plain,
( a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| def33 ),
inference(resolution,[status(thm)],[p7302,c367]) ).
cnf(p7455,plain,
( def33
| def10(sk29,sk30) ),
inference(resolution,[status(thm)],[p7072,p7303]) ).
cnf(c285,plain,
( ~ leq(X3,minus(n3,n1))
| def9(X2,X3)
| ~ def10(X2,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7458,plain,
( ~ leq(sk30,n2)
| def9(sk29,sk30)
| def33 ),
inference(resolution,[status(thm)],[p7455,c285]) ).
cnf(c366,plain,
( def36
| ~ def37 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7304,plain,
( def36
| def33 ),
inference(resolution,[status(thm)],[p7302,c366]) ).
cnf(c364,plain,
( leq(sk30,minus(n3,n1))
| ~ def36 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7305,plain,
( leq(sk30,n2)
| def33 ),
inference(resolution,[status(thm)],[p7304,c364]) ).
cnf(p7459,plain,
( def33
| def9(sk29,sk30)
| def33 ),
inference(resolution,[status(thm)],[p7458,p7305]) ).
cnf(p7460,plain,
( def9(sk29,sk30)
| def33 ),
inference(factoring,[status(thm)],[p7459]) ).
cnf(c282,plain,
( ~ leq(X2,minus(n3,n1))
| def8(X2,X3)
| ~ def9(X2,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7461,plain,
( ~ leq(sk29,n2)
| def8(sk29,sk30)
| def33 ),
inference(resolution,[status(thm)],[p7460,c282]) ).
cnf(c363,plain,
( def35
| ~ def36 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7306,plain,
( def35
| def33 ),
inference(resolution,[status(thm)],[p7304,c363]) ).
cnf(c361,plain,
( leq(sk29,minus(n3,n1))
| ~ def35 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7308,plain,
( leq(sk29,n2)
| def33 ),
inference(resolution,[status(thm)],[p7306,c361]) ).
cnf(p7462,plain,
( def33
| def8(sk29,sk30)
| def33 ),
inference(resolution,[status(thm)],[p7461,p7308]) ).
cnf(p7463,plain,
( def8(sk29,sk30)
| def33 ),
inference(factoring,[status(thm)],[p7462]) ).
cnf(c279,plain,
( ~ leq(n0,X3)
| ~ leq(n0,X2)
| ~ def8(X2,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7464,plain,
( ~ leq(n0,sk30)
| ~ leq(n0,sk29)
| def33 ),
inference(resolution,[status(thm)],[p7463,c279]) ).
cnf(c360,plain,
( def34
| ~ def35 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7307,plain,
( def34
| def33 ),
inference(resolution,[status(thm)],[p7306,c360]) ).
cnf(c357,plain,
( leq(n0,sk29)
| ~ def34 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7309,plain,
( leq(n0,sk29)
| def33 ),
inference(resolution,[status(thm)],[p7307,c357]) ).
cnf(p7467,plain,
( def33
| ~ leq(n0,sk30)
| def33 ),
inference(resolution,[status(thm)],[p7464,p7309]) ).
cnf(p7468,plain,
( ~ leq(n0,sk30)
| def33 ),
inference(factoring,[status(thm)],[p7467]) ).
cnf(c358,plain,
( leq(n0,sk30)
| ~ def34 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7310,plain,
( leq(n0,sk30)
| def33 ),
inference(resolution,[status(thm)],[p7307,c358]) ).
cnf(p7471,plain,
( def33
| def33 ),
inference(resolution,[status(thm)],[p7468,p7310]) ).
cnf(p7472,plain,
def33,
inference(factoring,[status(thm)],[p7471]) ).
cnf(c354,plain,
( def32
| def28
| ~ def33 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7473,plain,
( def32
| def28 ),
inference(resolution,[status(thm)],[p7472,c354]) ).
cnf(c352,plain,
( a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27)
| ~ def32 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7475,plain,
( a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27)
| def28 ),
inference(resolution,[status(thm)],[p7473,c352]) ).
cnf(p7570,plain,
( def28
| def5(sk27,sk28) ),
inference(resolution,[status(thm)],[p7073,p7475]) ).
cnf(c270,plain,
( ~ leq(X1,minus(n6,n1))
| def4(X0,X1)
| ~ def5(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7573,plain,
( ~ leq(sk28,pred(n6))
| def4(sk27,sk28)
| def28 ),
inference(resolution,[status(thm)],[p7570,c270]) ).
cnf(c351,plain,
( def31
| ~ def32 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7474,plain,
( def31
| def28 ),
inference(resolution,[status(thm)],[p7473,c351]) ).
cnf(c349,plain,
( leq(sk28,minus(n6,n1))
| ~ def31 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7476,plain,
( leq(sk28,pred(n6))
| def28 ),
inference(resolution,[status(thm)],[p7474,c349]) ).
cnf(p7582,plain,
( def28
| def4(sk27,sk28)
| def28 ),
inference(resolution,[status(thm)],[p7573,p7476]) ).
cnf(p7583,plain,
( def4(sk27,sk28)
| def28 ),
inference(factoring,[status(thm)],[p7582]) ).
cnf(c267,plain,
( ~ leq(X0,minus(n6,n1))
| def3(X0,X1)
| ~ def4(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7584,plain,
( ~ leq(sk27,pred(n6))
| def3(sk27,sk28)
| def28 ),
inference(resolution,[status(thm)],[p7583,c267]) ).
cnf(c348,plain,
( def30
| ~ def31 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7477,plain,
( def30
| def28 ),
inference(resolution,[status(thm)],[p7474,c348]) ).
cnf(c346,plain,
( leq(sk27,minus(n6,n1))
| ~ def30 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7479,plain,
( leq(sk27,pred(n6))
| def28 ),
inference(resolution,[status(thm)],[p7477,c346]) ).
cnf(p7593,plain,
( def28
| def3(sk27,sk28)
| def28 ),
inference(resolution,[status(thm)],[p7584,p7479]) ).
cnf(p7594,plain,
( def3(sk27,sk28)
| def28 ),
inference(factoring,[status(thm)],[p7593]) ).
cnf(c264,plain,
( ~ leq(n0,X1)
| ~ leq(n0,X0)
| ~ def3(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7595,plain,
( ~ leq(n0,sk28)
| ~ leq(n0,sk27)
| def28 ),
inference(resolution,[status(thm)],[p7594,c264]) ).
cnf(c345,plain,
( def29
| ~ def30 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7478,plain,
( def29
| def28 ),
inference(resolution,[status(thm)],[p7477,c345]) ).
cnf(c342,plain,
( leq(n0,sk27)
| ~ def29 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7481,plain,
( leq(n0,sk27)
| def28 ),
inference(resolution,[status(thm)],[p7478,c342]) ).
cnf(p7598,plain,
( def28
| ~ leq(n0,sk28)
| def28 ),
inference(resolution,[status(thm)],[p7595,p7481]) ).
cnf(p7599,plain,
( ~ leq(n0,sk28)
| def28 ),
inference(factoring,[status(thm)],[p7598]) ).
cnf(c343,plain,
( leq(n0,sk28)
| ~ def29 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7480,plain,
( leq(n0,sk28)
| def28 ),
inference(resolution,[status(thm)],[p7478,c343]) ).
cnf(p7602,plain,
( def28
| def28 ),
inference(resolution,[status(thm)],[p7599,p7480]) ).
cnf(p7603,plain,
def28,
inference(factoring,[status(thm)],[p7602]) ).
cnf(c339,plain,
( ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| ~ def28 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7604,plain,
( ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5) ),
inference(resolution,[status(thm)],[p7603,c339]) ).
cnf(c276,plain,
( def2
| ~ def7(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7065,plain,
def2,
inference(resolution,[status(thm)],[p7062,c276]) ).
cnf(c261,plain,
( def1
| ~ def2 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7066,plain,
def1,
inference(resolution,[status(thm)],[p7065,c261]) ).
cnf(c258,plain,
( def0
| ~ def1 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7069,plain,
def0,
inference(resolution,[status(thm)],[p7066,c258]) ).
cnf(c255,plain,
( leq(n0,pv5)
| ~ def0 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7070,plain,
leq(n0,pv5),
inference(resolution,[status(thm)],[p7069,c255]) ).
cnf(p7607,plain,
~ leq(pv5,pred(n999)),
inference(resolution,[status(thm)],[p7604,p7070]) ).
cnf(c259,plain,
( leq(pv5,minus(n999,n1))
| ~ def1 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49])],[f52_sk]) ).
cnf(p7068,plain,
leq(pv5,pred(n999)),
inference(resolution,[status(thm)],[p7066,c259]) ).
cnf(p7608,plain,
$false,
inference(resolution,[status(thm)],[p7607,p7068]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV112+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n011.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 18:32:27 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 56.13/7.65 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.13/7.65 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------