%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV115+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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:12:15 PM UTC 2026
% Result : Theorem 26.48s 3.88s
% Output : Proof 26.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 2
% Syntax : Number of formulae : 216 ( 25 unt; 0 def)
% Number of atoms : 677 ( 62 equ)
% Maximal formula atoms : 54 ( 3 avg)
% Number of connectives : 658 ( 197 ~; 301 |; 134 &)
% ( 0 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 52 ( 50 usr; 28 prp; 0-10 aty)
% Number of functors : 24 ( 24 usr; 21 con; 0-3 aty)
% Number of variables : 236 ( 83 sgn 63 !; 10 ?)
% 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) )
=> ( ! [S] :
( ( leq(S,minus(n6,n1))
& leq(n0,S) )
=> ! [T] :
( ( leq(T,minus(n6,n1))
& leq(n0,T) )
=> a_select3(id_ds1_filter,S,T) = a_select3(id_ds1_filter,T,S) ) )
& ! [Q,R] :
( ( leq(R,minus(n6,n1))
& leq(Q,minus(n6,n1))
& leq(n0,R)
& leq(n0,Q) )
=> a_select3(pminus_ds1_filter,Q,R) = a_select3(pminus_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/sandbox2/benchmark/theBenchmark.p',quaternion_ds1_symm_0008) ).
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) )
=> ( ! [S] :
( ( leq(S,minus(n6,n1))
& leq(n0,S) )
=> ! [T] :
( ( leq(T,minus(n6,n1))
& leq(n0,T) )
=> a_select3(id_ds1_filter,S,T) = a_select3(id_ds1_filter,T,S) ) )
& ! [Q,R] :
( ( leq(R,minus(n6,n1))
& leq(Q,minus(n6,n1))
& leq(n0,R)
& leq(n0,Q) )
=> a_select3(pminus_ds1_filter,Q,R) = a_select3(pminus_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,
( ( ? [S] :
( ? [T] :
( a_select3(id_ds1_filter,S,T) != a_select3(id_ds1_filter,T,S)
& leq(T,minus(n6,n1))
& leq(n0,T) )
& leq(S,minus(n6,n1))
& leq(n0,S) )
| ? [Q,R] :
( a_select3(pminus_ds1_filter,Q,R) != a_select3(pminus_ds1_filter,R,Q)
& leq(R,minus(n6,n1))
& leq(Q,minus(n6,n1))
& leq(n0,R)
& leq(n0,Q) )
| ? [O,P] :
( a_select3(pminus_ds1_filter,O,P) != a_select3(pminus_ds1_filter,P,O)
& leq(P,minus(n6,n1))
& leq(O,minus(n6,n1))
& leq(n0,P)
& leq(n0,O) )
| ? [M,N] :
( a_select3(r_ds1_filter,M,N) != a_select3(r_ds1_filter,N,M)
& leq(N,minus(n3,n1))
& leq(M,minus(n3,n1))
& leq(n0,N)
& leq(n0,M) )
| ? [K,L] :
( a_select3(q_ds1_filter,K,L) != a_select3(q_ds1_filter,L,K)
& leq(L,minus(n6,n1))
& leq(K,minus(n6,n1))
& leq(n0,L)
& leq(n0,K) )
| ~ leq(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(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(id_ds1_filter,sk35,sk36) != a_select3(id_ds1_filter,sk36,sk35)
& leq(sk36,minus(n6,n1))
& leq(n0,sk36)
& leq(sk35,minus(n6,n1))
& leq(n0,sk35) )
| ( a_select3(pminus_ds1_filter,sk33,sk34) != a_select3(pminus_ds1_filter,sk34,sk33)
& leq(sk34,minus(n6,n1))
& leq(sk33,minus(n6,n1))
& leq(n0,sk34)
& 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(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,sk33,sk34,sk35,sk36])],[f52_nnf]) ).
cnf(c385,plain,
( leq(sk33,minus(n6,n1))
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(c318,plain,
( ~ leq(X8,minus(n6,n1))
| ~ leq(n0,X8)
| ~ def21(X8) ),
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,def50,def51,def52])],[f52_sk]) ).
cnf(c324,plain,
( a_select3(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8)
| def22(X9)
| ~ def23(X9,X8) ),
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,def50,def51,def52])],[f52_sk]) ).
cnf(c331,plain,
( def24(X8,X9)
| ~ def25(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,def50,def51,def52])],[f52_sk]) ).
cnf(c411,plain,
( def25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ def52(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,def50,def51,def52])],[f52_sk]) ).
cnf(c414,plain,
def52(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,def50,def51,def52])],[f52_sk]) ).
cnf(p481,plain,
def25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9),
inference(resolution,[status(thm)],[c411,c414]) ).
cnf(p557,plain,
def24(X0,X1),
inference(resolution,[status(thm)],[c331,p481]) ).
cnf(c327,plain,
( def23(X9,X8)
| def21(X8)
| ~ def24(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,def50,def51,def52])],[f52_sk]) ).
cnf(p558,plain,
( def23(X1,X0)
| def21(X0) ),
inference(resolution,[status(thm)],[p557,c327]) ).
cnf(p559,plain,
( def21(X1)
| a_select3(id_ds1_filter,X1,X0) = a_select3(id_ds1_filter,X0,X1)
| def22(X0) ),
inference(resolution,[status(thm)],[c324,p558]) ).
cnf(c403,plain,
( a_select3(id_ds1_filter,sk35,sk36) != a_select3(id_ds1_filter,sk36,sk35)
| ~ def49 ),
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,def50,def51,def52])],[f52_sk]) ).
cnf(c408,plain,
( def50
| def46
| ~ def51 ),
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,def50,def51,def52])],[f52_sk]) ).
cnf(c412,plain,
( def51
| ~ def52(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,def50,def51,def52])],[f52_sk]) ).
cnf(p469,plain,
def51,
inference(resolution,[status(thm)],[c412,c414]) ).
cnf(p470,plain,
( def50
| def46 ),
inference(resolution,[status(thm)],[c408,p469]) ).
cnf(c406,plain,
( def49
| ~ def50 ),
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,def50,def51,def52])],[f52_sk]) ).
cnf(p471,plain,
( def49
| def46 ),
inference(resolution,[status(thm)],[p470,c406]) ).
cnf(p479,plain,
( def46
| a_select3(id_ds1_filter,sk35,sk36) != a_select3(id_ds1_filter,sk36,sk35) ),
inference(resolution,[status(thm)],[c403,p471]) ).
cnf(p560,plain,
( def46
| def21(sk35)
| def22(sk36) ),
inference(resolution,[status(thm)],[p559,p479]) ).
cnf(c321,plain,
( ~ leq(X9,minus(n6,n1))
| ~ leq(n0,X9)
| ~ def22(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,def50,def51,def52])],[f52_sk]) ).
cnf(p566,plain,
( ~ leq(sk36,minus(n6,n1))
| ~ leq(n0,sk36)
| def46
| def21(sk35) ),
inference(resolution,[status(thm)],[p560,c321]) ).
cnf(c399,plain,
( leq(n0,sk36)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(c402,plain,
( def48
| ~ def49 ),
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,def50,def51,def52])],[f52_sk]) ).
cnf(p472,plain,
( def48
| def46 ),
inference(resolution,[status(thm)],[p471,c402]) ).
cnf(p483,plain,
( def46
| leq(n0,sk36) ),
inference(resolution,[status(thm)],[c399,p472]) ).
cnf(p567,plain,
( def46
| ~ leq(sk36,minus(n6,n1))
| def46
| def21(sk35) ),
inference(resolution,[status(thm)],[p566,p483]) ).
cnf(p569,plain,
( ~ leq(sk36,minus(n6,n1))
| def46
| def21(sk35) ),
inference(factoring,[status(thm)],[p567]) ).
cnf(c400,plain,
( leq(sk36,minus(n6,n1))
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p480,plain,
( def46
| leq(sk36,minus(n6,n1)) ),
inference(resolution,[status(thm)],[c400,p472]) ).
cnf(p572,plain,
( def46
| def46
| def21(sk35) ),
inference(resolution,[status(thm)],[p569,p480]) ).
cnf(p575,plain,
( def46
| def21(sk35) ),
inference(factoring,[status(thm)],[p572]) ).
cnf(p596,plain,
( def46
| ~ leq(sk35,minus(n6,n1))
| ~ leq(n0,sk35) ),
inference(resolution,[status(thm)],[c318,p575]) ).
cnf(c405,plain,
( def47
| ~ def50 ),
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,def50,def51,def52])],[f52_sk]) ).
cnf(p476,plain,
( def46
| def47 ),
inference(resolution,[status(thm)],[c405,p470]) ).
cnf(c396,plain,
( leq(n0,sk35)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p478,plain,
( leq(n0,sk35)
| def46 ),
inference(resolution,[status(thm)],[p476,c396]) ).
cnf(p608,plain,
( def46
| def46
| ~ leq(sk35,minus(n6,n1)) ),
inference(resolution,[status(thm)],[p596,p478]) ).
cnf(p620,plain,
( def46
| ~ leq(sk35,minus(n6,n1)) ),
inference(factoring,[status(thm)],[p608]) ).
cnf(c397,plain,
( leq(sk35,minus(n6,n1))
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p477,plain,
( leq(sk35,minus(n6,n1))
| def46 ),
inference(resolution,[status(thm)],[p476,c397]) ).
cnf(p622,plain,
( def46
| def46 ),
inference(resolution,[status(thm)],[p620,p477]) ).
cnf(p628,plain,
def46,
inference(factoring,[status(thm)],[p622]) ).
cnf(c393,plain,
( def45
| def41
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p629,plain,
( def45
| def41 ),
inference(resolution,[status(thm)],[p628,c393]) ).
cnf(c390,plain,
( def44
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p630,plain,
( def44
| def41 ),
inference(resolution,[status(thm)],[p629,c390]) ).
cnf(c387,plain,
( def43
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p633,plain,
( def43
| def41 ),
inference(resolution,[status(thm)],[p630,c387]) ).
cnf(p791,plain,
( def41
| leq(sk33,pred(n6)) ),
inference(resolution,[status(thm)],[c385,p633]) ).
cnf(c315,plain,
( def15(X0,X1,X2,X3,X4,X5)
| ~ def20(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,def50,def51,def52])],[f52_sk]) ).
cnf(c330,plain,
( def20(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ def25(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,def50,def51,def52])],[f52_sk]) ).
cnf(p588,plain,
def20(X0,X1,X2,X3,X4,X5,X6,X7),
inference(resolution,[status(thm)],[c330,p481]) ).
cnf(p659,plain,
def15(X0,X1,X2,X3,X4,X5),
inference(resolution,[status(thm)],[c315,p588]) ).
cnf(c301,plain,
( def14(X4,X5)
| ~ def15(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,def50,def51,def52])],[f52_sk]) ).
cnf(p660,plain,
def14(X0,X1),
inference(resolution,[status(thm)],[p659,c301]) ).
cnf(c297,plain,
( a_select3(pminus_ds1_filter,X4,X5) = a_select3(pminus_ds1_filter,X5,X4)
| 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,def50,def51,def52])],[f52_sk]) ).
cnf(p662,plain,
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| def13(X0,X1) ),
inference(resolution,[status(thm)],[p660,c297]) ).
cnf(c391,plain,
( a_select3(pminus_ds1_filter,sk33,sk34) != a_select3(pminus_ds1_filter,sk34,sk33)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p631,plain,
( a_select3(pminus_ds1_filter,sk33,sk34) != a_select3(pminus_ds1_filter,sk34,sk33)
| def41 ),
inference(resolution,[status(thm)],[p629,c391]) ).
cnf(p688,plain,
( def41
| def13(sk33,sk34) ),
inference(resolution,[status(thm)],[p662,p631]) ).
cnf(c294,plain,
( ~ leq(X5,minus(n6,n1))
| def12(X4,X5)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p691,plain,
( ~ leq(sk34,pred(n6))
| def12(sk33,sk34)
| def41 ),
inference(resolution,[status(thm)],[p688,c294]) ).
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(c388,plain,
( leq(sk34,minus(n6,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,def50,def51,def52])],[f52_sk]) ).
cnf(p632,plain,
( leq(sk34,minus(n6,n1))
| def41 ),
inference(resolution,[status(thm)],[p630,c388]) ).
cnf(p680,plain,
( leq(sk34,pred(n6))
| def41 ),
inference(superposition,[status(thm)],[c234,p632]) ).
cnf(p692,plain,
( def41
| def12(sk33,sk34)
| def41 ),
inference(resolution,[status(thm)],[p691,p680]) ).
cnf(p703,plain,
( def12(sk33,sk34)
| def41 ),
inference(factoring,[status(thm)],[p692]) ).
cnf(c291,plain,
( ~ leq(X4,minus(n6,n1))
| def11(X4,X5)
| ~ def12(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,def50,def51,def52])],[f52_sk]) ).
cnf(p704,plain,
( ~ leq(sk33,pred(n6))
| def11(sk33,sk34)
| def41 ),
inference(resolution,[status(thm)],[p703,c291]) ).
cnf(c320,plain,
( def21(X8)
| leq(X8,minus(n6,n1)) ),
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,def50,def51,def52])],[f52_sk]) ).
cnf(p674,plain,
( def21(X0)
| leq(X0,pred(n6)) ),
inference(superposition,[status(thm)],[c234,c320]) ).
cnf(p705,plain,
( def21(sk33)
| def11(sk33,sk34)
| def41 ),
inference(resolution,[status(thm)],[p704,p674]) ).
cnf(c288,plain,
( ~ leq(n0,X5)
| ~ leq(n0,X4)
| ~ def11(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,def50,def51,def52])],[f52_sk]) ).
cnf(p715,plain,
( ~ leq(n0,sk34)
| ~ leq(n0,sk33)
| def21(sk33)
| def41 ),
inference(resolution,[status(thm)],[p705,c288]) ).
cnf(c384,plain,
( def42
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p634,plain,
( def42
| def41 ),
inference(resolution,[status(thm)],[p633,c384]) ).
cnf(c381,plain,
( leq(n0,sk33)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p635,plain,
( leq(n0,sk33)
| def41 ),
inference(resolution,[status(thm)],[p634,c381]) ).
cnf(p721,plain,
( def41
| ~ leq(n0,sk34)
| def21(sk33)
| def41 ),
inference(resolution,[status(thm)],[p715,p635]) ).
cnf(p722,plain,
( ~ leq(n0,sk34)
| def21(sk33)
| def41 ),
inference(factoring,[status(thm)],[p721]) ).
cnf(c382,plain,
( leq(n0,sk34)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p636,plain,
( leq(n0,sk34)
| def41 ),
inference(resolution,[status(thm)],[p634,c382]) ).
cnf(p725,plain,
( def41
| def21(sk33)
| def41 ),
inference(resolution,[status(thm)],[p722,p636]) ).
cnf(p726,plain,
( def21(sk33)
| def41 ),
inference(factoring,[status(thm)],[p725]) ).
cnf(p727,plain,
( ~ leq(sk33,pred(n6))
| ~ leq(n0,sk33)
| def41 ),
inference(resolution,[status(thm)],[p726,c318]) ).
cnf(p729,plain,
( def41
| ~ leq(sk33,pred(n6))
| def41 ),
inference(resolution,[status(thm)],[p727,p635]) ).
cnf(p730,plain,
( ~ leq(sk33,pred(n6))
| def41 ),
inference(factoring,[status(thm)],[p729]) ).
cnf(p794,plain,
( def41
| def41 ),
inference(resolution,[status(thm)],[p791,p730]) ).
cnf(p795,plain,
def41,
inference(factoring,[status(thm)],[p794]) ).
cnf(c378,plain,
( def40
| def36
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p796,plain,
( def40
| def36 ),
inference(resolution,[status(thm)],[p795,c378]) ).
cnf(c376,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p798,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| def36 ),
inference(resolution,[status(thm)],[p796,c376]) ).
cnf(p813,plain,
( def13(sk31,sk32)
| def36 ),
inference(resolution,[status(thm)],[p798,p662]) ).
cnf(p819,plain,
( ~ leq(sk32,pred(n6))
| def12(sk31,sk32)
| def36 ),
inference(resolution,[status(thm)],[p813,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,def50,def51,def52])],[f52_sk]) ).
cnf(p797,plain,
( def39
| def36 ),
inference(resolution,[status(thm)],[p796,c375]) ).
cnf(c373,plain,
( leq(sk32,minus(n6,n1))
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p799,plain,
( leq(sk32,pred(n6))
| def36 ),
inference(resolution,[status(thm)],[p797,c373]) ).
cnf(p834,plain,
( def36
| def12(sk31,sk32)
| def36 ),
inference(resolution,[status(thm)],[p819,p799]) ).
cnf(p835,plain,
( def12(sk31,sk32)
| def36 ),
inference(factoring,[status(thm)],[p834]) ).
cnf(p836,plain,
( ~ leq(sk31,pred(n6))
| def11(sk31,sk32)
| def36 ),
inference(resolution,[status(thm)],[p835,c291]) ).
cnf(c372,plain,
( def38
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p800,plain,
( def38
| def36 ),
inference(resolution,[status(thm)],[p797,c372]) ).
cnf(c370,plain,
( leq(sk31,minus(n6,n1))
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p802,plain,
( leq(sk31,pred(n6))
| def36 ),
inference(resolution,[status(thm)],[p800,c370]) ).
cnf(p861,plain,
( def36
| def11(sk31,sk32)
| def36 ),
inference(resolution,[status(thm)],[p836,p802]) ).
cnf(p863,plain,
( def11(sk31,sk32)
| def36 ),
inference(factoring,[status(thm)],[p861]) ).
cnf(p864,plain,
( ~ leq(n0,sk32)
| ~ leq(n0,sk31)
| def36 ),
inference(resolution,[status(thm)],[p863,c288]) ).
cnf(c369,plain,
( def37
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p801,plain,
( def37
| def36 ),
inference(resolution,[status(thm)],[p800,c369]) ).
cnf(c366,plain,
( leq(n0,sk31)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p804,plain,
( leq(n0,sk31)
| def36 ),
inference(resolution,[status(thm)],[p801,c366]) ).
cnf(p867,plain,
( def36
| ~ leq(n0,sk32)
| def36 ),
inference(resolution,[status(thm)],[p864,p804]) ).
cnf(p868,plain,
( ~ leq(n0,sk32)
| def36 ),
inference(factoring,[status(thm)],[p867]) ).
cnf(c367,plain,
( leq(n0,sk32)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p803,plain,
( leq(n0,sk32)
| def36 ),
inference(resolution,[status(thm)],[p801,c367]) ).
cnf(p871,plain,
( def36
| def36 ),
inference(resolution,[status(thm)],[p868,p803]) ).
cnf(p872,plain,
def36,
inference(factoring,[status(thm)],[p871]) ).
cnf(c363,plain,
( def35
| def31
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p873,plain,
( def35
| def31 ),
inference(resolution,[status(thm)],[p872,c363]) ).
cnf(c361,plain,
( a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p874,plain,
( a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| def31 ),
inference(resolution,[status(thm)],[p873,c361]) ).
cnf(c300,plain,
( def10(X0,X1,X2,X3)
| ~ def15(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,def50,def51,def52])],[f52_sk]) ).
cnf(p661,plain,
def10(X0,X1,X2,X3),
inference(resolution,[status(thm)],[p659,c300]) ).
cnf(c286,plain,
( def9(X2,X3)
| ~ def10(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,def50,def51,def52])],[f52_sk]) ).
cnf(p664,plain,
def9(X0,X1),
inference(resolution,[status(thm)],[p661,c286]) ).
cnf(c282,plain,
( a_select3(r_ds1_filter,X2,X3) = a_select3(r_ds1_filter,X3,X2)
| 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,def50,def51,def52])],[f52_sk]) ).
cnf(p668,plain,
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| def8(X0,X1) ),
inference(resolution,[status(thm)],[p664,c282]) ).
cnf(p884,plain,
( def8(sk29,sk30)
| def31 ),
inference(resolution,[status(thm)],[p874,p668]) ).
cnf(c279,plain,
( ~ leq(X3,minus(n3,n1))
| def7(X2,X3)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p887,plain,
( ~ leq(sk30,n2)
| def7(sk29,sk30)
| def31 ),
inference(resolution,[status(thm)],[p884,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,def50,def51,def52])],[f52_sk]) ).
cnf(p875,plain,
( def34
| def31 ),
inference(resolution,[status(thm)],[p873,c360]) ).
cnf(c358,plain,
( leq(sk30,minus(n3,n1))
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p877,plain,
( leq(sk30,n2)
| def31 ),
inference(resolution,[status(thm)],[p875,c358]) ).
cnf(p888,plain,
( def31
| def7(sk29,sk30)
| def31 ),
inference(resolution,[status(thm)],[p887,p877]) ).
cnf(p889,plain,
( def7(sk29,sk30)
| def31 ),
inference(factoring,[status(thm)],[p888]) ).
cnf(c276,plain,
( ~ leq(X2,minus(n3,n1))
| def6(X2,X3)
| ~ def7(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,def50,def51,def52])],[f52_sk]) ).
cnf(p890,plain,
( ~ leq(sk29,n2)
| def6(sk29,sk30)
| def31 ),
inference(resolution,[status(thm)],[p889,c276]) ).
cnf(c357,plain,
( def33
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p876,plain,
( def33
| def31 ),
inference(resolution,[status(thm)],[p875,c357]) ).
cnf(c355,plain,
( leq(sk29,minus(n3,n1))
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p879,plain,
( leq(sk29,n2)
| def31 ),
inference(resolution,[status(thm)],[p876,c355]) ).
cnf(p891,plain,
( def31
| def6(sk29,sk30)
| def31 ),
inference(resolution,[status(thm)],[p890,p879]) ).
cnf(p892,plain,
( def6(sk29,sk30)
| def31 ),
inference(factoring,[status(thm)],[p891]) ).
cnf(c273,plain,
( ~ leq(n0,X3)
| ~ leq(n0,X2)
| ~ def6(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,def50,def51,def52])],[f52_sk]) ).
cnf(p893,plain,
( ~ leq(n0,sk30)
| ~ leq(n0,sk29)
| def31 ),
inference(resolution,[status(thm)],[p892,c273]) ).
cnf(c354,plain,
( def32
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p878,plain,
( def32
| def31 ),
inference(resolution,[status(thm)],[p876,c354]) ).
cnf(c351,plain,
( leq(n0,sk29)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p880,plain,
( leq(n0,sk29)
| def31 ),
inference(resolution,[status(thm)],[p878,c351]) ).
cnf(p896,plain,
( def31
| ~ leq(n0,sk30)
| def31 ),
inference(resolution,[status(thm)],[p893,p880]) ).
cnf(p897,plain,
( ~ leq(n0,sk30)
| def31 ),
inference(factoring,[status(thm)],[p896]) ).
cnf(c352,plain,
( leq(n0,sk30)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p881,plain,
( leq(n0,sk30)
| def31 ),
inference(resolution,[status(thm)],[p878,c352]) ).
cnf(p900,plain,
( def31
| def31 ),
inference(resolution,[status(thm)],[p897,p881]) ).
cnf(p901,plain,
def31,
inference(factoring,[status(thm)],[p900]) ).
cnf(c348,plain,
( def30
| def26
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p902,plain,
( def30
| def26 ),
inference(resolution,[status(thm)],[p901,c348]) ).
cnf(c346,plain,
( a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p903,plain,
( a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27)
| def26 ),
inference(resolution,[status(thm)],[p902,c346]) ).
cnf(c285,plain,
( def5(X0,X1)
| ~ def10(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,def50,def51,def52])],[f52_sk]) ).
cnf(p663,plain,
def5(X0,X1),
inference(resolution,[status(thm)],[p661,c285]) ).
cnf(c271,plain,
( 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,def50,def51,def52])],[f52_sk]) ).
cnf(p666,plain,
def4(X0,X1),
inference(resolution,[status(thm)],[p663,c271]) ).
cnf(c267,plain,
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| 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,def50,def51,def52])],[f52_sk]) ).
cnf(p669,plain,
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| def3(X0,X1) ),
inference(resolution,[status(thm)],[p666,c267]) ).
cnf(p911,plain,
( def3(sk27,sk28)
| def26 ),
inference(resolution,[status(thm)],[p903,p669]) ).
cnf(c264,plain,
( ~ leq(X1,minus(n6,n1))
| def2(X0,X1)
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p914,plain,
( ~ leq(sk28,pred(n6))
| def2(sk27,sk28)
| def26 ),
inference(resolution,[status(thm)],[p911,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,def50,def51,def52])],[f52_sk]) ).
cnf(p904,plain,
( def29
| def26 ),
inference(resolution,[status(thm)],[p902,c345]) ).
cnf(c343,plain,
( leq(sk28,minus(n6,n1))
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p906,plain,
( leq(sk28,pred(n6))
| def26 ),
inference(resolution,[status(thm)],[p904,c343]) ).
cnf(p926,plain,
( def26
| def2(sk27,sk28)
| def26 ),
inference(resolution,[status(thm)],[p914,p906]) ).
cnf(p927,plain,
( def2(sk27,sk28)
| def26 ),
inference(factoring,[status(thm)],[p926]) ).
cnf(c261,plain,
( ~ leq(X0,minus(n6,n1))
| def1(X0,X1)
| ~ def2(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,def50,def51,def52])],[f52_sk]) ).
cnf(p928,plain,
( ~ leq(sk27,pred(n6))
| def1(sk27,sk28)
| def26 ),
inference(resolution,[status(thm)],[p927,c261]) ).
cnf(c342,plain,
( def28
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p905,plain,
( def28
| def26 ),
inference(resolution,[status(thm)],[p904,c342]) ).
cnf(c340,plain,
( leq(sk27,minus(n6,n1))
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p907,plain,
( leq(sk27,pred(n6))
| def26 ),
inference(resolution,[status(thm)],[p905,c340]) ).
cnf(p940,plain,
( def26
| def1(sk27,sk28)
| def26 ),
inference(resolution,[status(thm)],[p928,p907]) ).
cnf(p941,plain,
( def1(sk27,sk28)
| def26 ),
inference(factoring,[status(thm)],[p940]) ).
cnf(c258,plain,
( ~ leq(n0,X1)
| ~ leq(n0,X0)
| ~ def1(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,def50,def51,def52])],[f52_sk]) ).
cnf(p942,plain,
( ~ leq(n0,sk28)
| ~ leq(n0,sk27)
| def26 ),
inference(resolution,[status(thm)],[p941,c258]) ).
cnf(c339,plain,
( def27
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p908,plain,
( def27
| def26 ),
inference(resolution,[status(thm)],[p905,c339]) ).
cnf(c336,plain,
( leq(n0,sk27)
| ~ def27 ),
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,def50,def51,def52])],[f52_sk]) ).
cnf(p909,plain,
( leq(n0,sk27)
| def26 ),
inference(resolution,[status(thm)],[p908,c336]) ).
cnf(p945,plain,
( def26
| ~ leq(n0,sk28)
| def26 ),
inference(resolution,[status(thm)],[p942,p909]) ).
cnf(p946,plain,
( ~ leq(n0,sk28)
| def26 ),
inference(factoring,[status(thm)],[p945]) ).
cnf(c337,plain,
( leq(n0,sk28)
| ~ def27 ),
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,def50,def51,def52])],[f52_sk]) ).
cnf(p910,plain,
( leq(n0,sk28)
| def26 ),
inference(resolution,[status(thm)],[p908,c337]) ).
cnf(p949,plain,
( def26
| def26 ),
inference(resolution,[status(thm)],[p946,p910]) ).
cnf(p950,plain,
def26,
inference(factoring,[status(thm)],[p949]) ).
cnf(c333,plain,
( ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| ~ def26 ),
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,def50,def51,def52])],[f52_sk]) ).
cnf(p951,plain,
( ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5) ),
inference(resolution,[status(thm)],[p950,c333]) ).
cnf(c270,plain,
( def0
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p665,plain,
def0,
inference(resolution,[status(thm)],[p663,c270]) ).
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,def50,def51,def52])],[f52_sk]) ).
cnf(p667,plain,
leq(n0,pv5),
inference(resolution,[status(thm)],[p665,c255]) ).
cnf(p954,plain,
~ leq(pv5,pred(n999)),
inference(resolution,[status(thm)],[p951,p667]) ).
cnf(c256,plain,
( leq(pv5,minus(n999,n1))
| ~ 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,def50,def51,def52])],[f52_sk]) ).
cnf(p790,plain,
leq(pv5,pred(n999)),
inference(resolution,[status(thm)],[c256,p665]) ).
cnf(p955,plain,
$false,
inference(resolution,[status(thm)],[p954,p790]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV115+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 18:35:41 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 26.48/3.88 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.48/3.88 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------