%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV109+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 7.80s 4.00s
% Output : Proof 7.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 2
% Syntax : Number of formulae : 216 ( 28 unt; 0 def)
% Number of atoms : 676 ( 62 equ)
% Maximal formula atoms : 56 ( 3 avg)
% Number of connectives : 655 ( 195 ~; 292 |; 142 &)
% ( 0 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 54 ( 52 usr; 30 prp; 0-10 aty)
% Number of functors : 24 ( 24 usr; 21 con; 0-3 aty)
% Number of variables : 236 ( 85 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(pv47,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv47)
& 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/sandbox/benchmark/theBenchmark.p',quaternion_ds1_symm_0002) ).
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(pv47,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv47)
& 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(pv47,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv47)
& 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(pv47,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv47)
& leq(n0,pv5) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk27,sk28,sk29,sk30,sk31,sk32,sk33,sk34,sk35,sk36])],[f52_nnf]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(c417,plain,
( def27(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ def54(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,def53,def54])],[f52_sk]) ).
cnf(c420,plain,
def54(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,def53,def54])],[f52_sk]) ).
cnf(p582,plain,
def27(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9),
inference(resolution,[status(thm)],[c417,c420]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p584,plain,
def22(X0,X1,X2,X3,X4,X5,X6,X7),
inference(resolution,[status(thm)],[p582,c336]) ).
cnf(p633,plain,
def17(X0,X1,X2,X3,X4,X5),
inference(resolution,[status(thm)],[c321,p584]) ).
cnf(p682,plain,
def12(X0,X1,X2,X3),
inference(resolution,[status(thm)],[c306,p633]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p683,plain,
def7(X0,X1),
inference(resolution,[status(thm)],[p682,c291]) ).
cnf(p843,plain,
def6(X0,X1),
inference(resolution,[status(thm)],[c277,p683]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p844,plain,
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| def5(X0,X1) ),
inference(resolution,[status(thm)],[p843,c273]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p684,plain,
def11(X0,X1),
inference(resolution,[status(thm)],[p682,c292]) ).
cnf(p777,plain,
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| def10(X0,X1) ),
inference(resolution,[status(thm)],[c288,p684]) ).
cnf(c312,plain,
( ~ leq(X6,minus(n6,n1))
| 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,def50,def51,def52,def53,def54])],[f52_sk]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(c318,plain,
( a_select3(pminus_ds1_filter,X6,X7) = a_select3(pminus_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,def50,def51,def52,def53,def54])],[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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p628,plain,
def21(X0,X1),
inference(resolution,[status(thm)],[c322,p584]) ).
cnf(p634,plain,
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| def20(X0,X1) ),
inference(resolution,[status(thm)],[c318,p628]) ).
cnf(c337,plain,
( def26(X8,X9)
| ~ 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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p583,plain,
def26(X0,X1),
inference(resolution,[status(thm)],[p582,c337]) ).
cnf(c333,plain,
( def25(X9,X8)
| def23(X8)
| ~ def26(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,def53,def54])],[f52_sk]) ).
cnf(p585,plain,
( def25(X1,X0)
| def23(X0) ),
inference(resolution,[status(thm)],[p583,c333]) ).
cnf(c330,plain,
( a_select3(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8)
| def24(X9)
| ~ def25(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,def53,def54])],[f52_sk]) ).
cnf(p586,plain,
( a_select3(id_ds1_filter,X0,X1) = a_select3(id_ds1_filter,X1,X0)
| def24(X1)
| def23(X0) ),
inference(resolution,[status(thm)],[p585,c330]) ).
cnf(c418,plain,
( def53
| ~ def54(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,def53,def54])],[f52_sk]) ).
cnf(p497,plain,
def53,
inference(resolution,[status(thm)],[c418,c420]) ).
cnf(c414,plain,
( def52
| def48
| ~ def53 ),
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,def53,def54])],[f52_sk]) ).
cnf(p498,plain,
( def52
| def48 ),
inference(resolution,[status(thm)],[p497,c414]) ).
cnf(c412,plain,
( def51
| ~ def52 ),
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,def53,def54])],[f52_sk]) ).
cnf(p516,plain,
( def51
| def48 ),
inference(resolution,[status(thm)],[p498,c412]) ).
cnf(c409,plain,
( a_select3(id_ds1_filter,sk35,sk36) != a_select3(id_ds1_filter,sk36,sk35)
| ~ 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,def53,def54])],[f52_sk]) ).
cnf(p519,plain,
( a_select3(id_ds1_filter,sk35,sk36) != a_select3(id_ds1_filter,sk36,sk35)
| def48 ),
inference(resolution,[status(thm)],[p516,c409]) ).
cnf(p589,plain,
( def48
| def24(sk36)
| def23(sk35) ),
inference(resolution,[status(thm)],[p586,p519]) ).
cnf(c327,plain,
( ~ leq(X9,minus(n6,n1))
| ~ leq(n0,X9)
| ~ def24(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,def53,def54])],[f52_sk]) ).
cnf(p592,plain,
( ~ leq(sk36,minus(n6,n1))
| ~ leq(n0,sk36)
| def48
| def23(sk35) ),
inference(resolution,[status(thm)],[p589,c327]) ).
cnf(c408,plain,
( def50
| ~ 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,def53,def54])],[f52_sk]) ).
cnf(p518,plain,
( def50
| def48 ),
inference(resolution,[status(thm)],[p516,c408]) ).
cnf(c405,plain,
( leq(n0,sk36)
| ~ 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,def53,def54])],[f52_sk]) ).
cnf(p523,plain,
( leq(n0,sk36)
| def48 ),
inference(resolution,[status(thm)],[p518,c405]) ).
cnf(p595,plain,
( def48
| ~ leq(sk36,minus(n6,n1))
| def48
| def23(sk35) ),
inference(resolution,[status(thm)],[p592,p523]) ).
cnf(p596,plain,
( ~ leq(sk36,minus(n6,n1))
| def48
| def23(sk35) ),
inference(factoring,[status(thm)],[p595]) ).
cnf(c406,plain,
( leq(sk36,minus(n6,n1))
| ~ 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,def53,def54])],[f52_sk]) ).
cnf(p522,plain,
( leq(sk36,minus(n6,n1))
| def48 ),
inference(resolution,[status(thm)],[p518,c406]) ).
cnf(p599,plain,
( def48
| def48
| def23(sk35) ),
inference(resolution,[status(thm)],[p596,p522]) ).
cnf(p600,plain,
( def48
| def23(sk35) ),
inference(factoring,[status(thm)],[p599]) ).
cnf(c324,plain,
( ~ leq(X8,minus(n6,n1))
| ~ leq(n0,X8)
| ~ def23(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,def53,def54])],[f52_sk]) ).
cnf(p601,plain,
( ~ leq(sk35,minus(n6,n1))
| ~ leq(n0,sk35)
| def48 ),
inference(resolution,[status(thm)],[p600,c324]) ).
cnf(c411,plain,
( def49
| ~ def52 ),
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,def53,def54])],[f52_sk]) ).
cnf(p517,plain,
( def49
| def48 ),
inference(resolution,[status(thm)],[p498,c411]) ).
cnf(c402,plain,
( leq(n0,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,def53,def54])],[f52_sk]) ).
cnf(p520,plain,
( leq(n0,sk35)
| def48 ),
inference(resolution,[status(thm)],[p517,c402]) ).
cnf(p603,plain,
( def48
| ~ leq(sk35,minus(n6,n1))
| def48 ),
inference(resolution,[status(thm)],[p601,p520]) ).
cnf(p604,plain,
( ~ leq(sk35,minus(n6,n1))
| def48 ),
inference(factoring,[status(thm)],[p603]) ).
cnf(c403,plain,
( leq(sk35,minus(n6,n1))
| ~ 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,def53,def54])],[f52_sk]) ).
cnf(p521,plain,
( leq(sk35,minus(n6,n1))
| def48 ),
inference(resolution,[status(thm)],[p517,c403]) ).
cnf(p607,plain,
( def48
| def48 ),
inference(resolution,[status(thm)],[p604,p521]) ).
cnf(p608,plain,
def48,
inference(factoring,[status(thm)],[p607]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p609,plain,
( def47
| def43 ),
inference(resolution,[status(thm)],[p608,c399]) ).
cnf(c397,plain,
( a_select3(pminus_ds1_filter,sk33,sk34) != a_select3(pminus_ds1_filter,sk34,sk33)
| ~ 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,def53,def54])],[f52_sk]) ).
cnf(p611,plain,
( a_select3(pminus_ds1_filter,sk33,sk34) != a_select3(pminus_ds1_filter,sk34,sk33)
| def43 ),
inference(resolution,[status(thm)],[p609,c397]) ).
cnf(p635,plain,
( def43
| def20(sk33,sk34) ),
inference(resolution,[status(thm)],[p634,p611]) ).
cnf(p639,plain,
( def43
| ~ leq(sk34,minus(n6,n1))
| def19(sk33,sk34) ),
inference(resolution,[status(thm)],[c315,p635]) ).
cnf(c396,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p610,plain,
( def46
| def43 ),
inference(resolution,[status(thm)],[p609,c396]) ).
cnf(c394,plain,
( leq(sk34,minus(n6,n1))
| ~ 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,def53,def54])],[f52_sk]) ).
cnf(p612,plain,
( leq(sk34,minus(n6,n1))
| def43 ),
inference(resolution,[status(thm)],[p610,c394]) ).
cnf(p649,plain,
( def43
| def43
| def19(sk33,sk34) ),
inference(resolution,[status(thm)],[p639,p612]) ).
cnf(p659,plain,
( def43
| def19(sk33,sk34) ),
inference(factoring,[status(thm)],[p649]) ).
cnf(p692,plain,
( def43
| ~ leq(sk33,minus(n6,n1))
| def18(sk33,sk34) ),
inference(resolution,[status(thm)],[c312,p659]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p613,plain,
( def45
| def43 ),
inference(resolution,[status(thm)],[p610,c393]) ).
cnf(c391,plain,
( leq(sk33,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p614,plain,
( leq(sk33,minus(n6,n1))
| def43 ),
inference(resolution,[status(thm)],[p613,c391]) ).
cnf(p697,plain,
( def43
| def43
| def18(sk33,sk34) ),
inference(resolution,[status(thm)],[p692,p614]) ).
cnf(p707,plain,
( def43
| def18(sk33,sk34) ),
inference(factoring,[status(thm)],[p697]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p708,plain,
( ~ leq(n0,sk34)
| ~ leq(n0,sk33)
| def43 ),
inference(resolution,[status(thm)],[p707,c309]) ).
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,def53,def54])],[f52_sk]) ).
cnf(p615,plain,
( def44
| def43 ),
inference(resolution,[status(thm)],[p613,c390]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p616,plain,
( leq(n0,sk33)
| def43 ),
inference(resolution,[status(thm)],[p615,c387]) ).
cnf(p711,plain,
( def43
| ~ leq(n0,sk34)
| def43 ),
inference(resolution,[status(thm)],[p708,p616]) ).
cnf(p712,plain,
( ~ leq(n0,sk34)
| def43 ),
inference(factoring,[status(thm)],[p711]) ).
cnf(c388,plain,
( leq(n0,sk34)
| ~ 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,def53,def54])],[f52_sk]) ).
cnf(p617,plain,
( leq(n0,sk34)
| def43 ),
inference(resolution,[status(thm)],[p615,c388]) ).
cnf(p715,plain,
( def43
| def43 ),
inference(resolution,[status(thm)],[p712,p617]) ).
cnf(p716,plain,
def43,
inference(factoring,[status(thm)],[p715]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p717,plain,
( def42
| def38 ),
inference(resolution,[status(thm)],[p716,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p718,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| def38 ),
inference(resolution,[status(thm)],[p717,c382]) ).
cnf(p726,plain,
( def20(sk31,sk32)
| def38 ),
inference(resolution,[status(thm)],[p718,p634]) ).
cnf(p729,plain,
( ~ leq(sk32,minus(n6,n1))
| def19(sk31,sk32)
| def38 ),
inference(resolution,[status(thm)],[p726,c315]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p719,plain,
( def41
| def38 ),
inference(resolution,[status(thm)],[p717,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p721,plain,
( leq(sk32,minus(n6,n1))
| def38 ),
inference(resolution,[status(thm)],[p719,c379]) ).
cnf(p742,plain,
( def38
| def19(sk31,sk32)
| def38 ),
inference(resolution,[status(thm)],[p729,p721]) ).
cnf(p743,plain,
( def19(sk31,sk32)
| def38 ),
inference(factoring,[status(thm)],[p742]) ).
cnf(p744,plain,
( ~ leq(sk31,minus(n6,n1))
| def18(sk31,sk32)
| def38 ),
inference(resolution,[status(thm)],[p743,c312]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p720,plain,
( def40
| def38 ),
inference(resolution,[status(thm)],[p719,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p722,plain,
( leq(sk31,minus(n6,n1))
| def38 ),
inference(resolution,[status(thm)],[p720,c376]) ).
cnf(p757,plain,
( def38
| def18(sk31,sk32)
| def38 ),
inference(resolution,[status(thm)],[p744,p722]) ).
cnf(p758,plain,
( def18(sk31,sk32)
| def38 ),
inference(factoring,[status(thm)],[p757]) ).
cnf(p759,plain,
( ~ leq(n0,sk32)
| ~ leq(n0,sk31)
| def38 ),
inference(resolution,[status(thm)],[p758,c309]) ).
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,def53,def54])],[f52_sk]) ).
cnf(p723,plain,
( def39
| def38 ),
inference(resolution,[status(thm)],[p720,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p725,plain,
( leq(n0,sk31)
| def38 ),
inference(resolution,[status(thm)],[p723,c372]) ).
cnf(p762,plain,
( def38
| ~ leq(n0,sk32)
| def38 ),
inference(resolution,[status(thm)],[p759,p725]) ).
cnf(p763,plain,
( ~ leq(n0,sk32)
| def38 ),
inference(factoring,[status(thm)],[p762]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p724,plain,
( leq(n0,sk32)
| def38 ),
inference(resolution,[status(thm)],[p723,c373]) ).
cnf(p766,plain,
( def38
| def38 ),
inference(resolution,[status(thm)],[p763,p724]) ).
cnf(p767,plain,
def38,
inference(factoring,[status(thm)],[p766]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p768,plain,
( def37
| def33 ),
inference(resolution,[status(thm)],[p767,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p770,plain,
( a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| def33 ),
inference(resolution,[status(thm)],[p768,c367]) ).
cnf(p778,plain,
( def33
| def10(sk29,sk30) ),
inference(resolution,[status(thm)],[p777,p770]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p781,plain,
( ~ leq(sk30,minus(n3,n1))
| def9(sk29,sk30)
| def33 ),
inference(resolution,[status(thm)],[p778,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p769,plain,
( def36
| def33 ),
inference(resolution,[status(thm)],[p768,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p772,plain,
( leq(sk30,minus(n3,n1))
| def33 ),
inference(resolution,[status(thm)],[p769,c364]) ).
cnf(p783,plain,
( def33
| def9(sk29,sk30)
| def33 ),
inference(resolution,[status(thm)],[p781,p772]) ).
cnf(p784,plain,
( def9(sk29,sk30)
| def33 ),
inference(factoring,[status(thm)],[p783]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p785,plain,
( ~ leq(sk29,minus(n3,n1))
| def8(sk29,sk30)
| def33 ),
inference(resolution,[status(thm)],[p784,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p771,plain,
( def35
| def33 ),
inference(resolution,[status(thm)],[p769,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p773,plain,
( leq(sk29,minus(n3,n1))
| def33 ),
inference(resolution,[status(thm)],[p771,c361]) ).
cnf(p787,plain,
( def33
| def8(sk29,sk30)
| def33 ),
inference(resolution,[status(thm)],[p785,p773]) ).
cnf(p788,plain,
( def8(sk29,sk30)
| def33 ),
inference(factoring,[status(thm)],[p787]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p789,plain,
( ~ leq(n0,sk30)
| ~ leq(n0,sk29)
| def33 ),
inference(resolution,[status(thm)],[p788,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,def53,def54])],[f52_sk]) ).
cnf(p774,plain,
( def34
| def33 ),
inference(resolution,[status(thm)],[p771,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p775,plain,
( leq(n0,sk29)
| def33 ),
inference(resolution,[status(thm)],[p774,c357]) ).
cnf(p792,plain,
( def33
| ~ leq(n0,sk30)
| def33 ),
inference(resolution,[status(thm)],[p789,p775]) ).
cnf(p793,plain,
( ~ leq(n0,sk30)
| def33 ),
inference(factoring,[status(thm)],[p792]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p776,plain,
( leq(n0,sk30)
| def33 ),
inference(resolution,[status(thm)],[p774,c358]) ).
cnf(p796,plain,
( def33
| def33 ),
inference(resolution,[status(thm)],[p793,p776]) ).
cnf(p797,plain,
def33,
inference(factoring,[status(thm)],[p796]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p798,plain,
( def32
| def28 ),
inference(resolution,[status(thm)],[p797,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p800,plain,
( a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27)
| def28 ),
inference(resolution,[status(thm)],[p798,c352]) ).
cnf(p872,plain,
( def28
| def5(sk27,sk28) ),
inference(resolution,[status(thm)],[p844,p800]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p875,plain,
( ~ leq(sk28,pred(n6))
| def4(sk27,sk28)
| def28 ),
inference(resolution,[status(thm)],[p872,c270]) ).
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(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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p799,plain,
( def31
| def28 ),
inference(resolution,[status(thm)],[p798,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p801,plain,
( leq(sk28,minus(n6,n1))
| def28 ),
inference(resolution,[status(thm)],[p799,c349]) ).
cnf(p831,plain,
( leq(sk28,pred(n6))
| def28 ),
inference(superposition,[status(thm)],[c234,p801]) ).
cnf(p876,plain,
( def28
| def4(sk27,sk28)
| def28 ),
inference(resolution,[status(thm)],[p875,p831]) ).
cnf(p888,plain,
( def4(sk27,sk28)
| def28 ),
inference(factoring,[status(thm)],[p876]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p889,plain,
( ~ leq(sk27,pred(n6))
| def3(sk27,sk28)
| def28 ),
inference(resolution,[status(thm)],[p888,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p802,plain,
( def30
| def28 ),
inference(resolution,[status(thm)],[p799,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p804,plain,
( leq(sk27,minus(n6,n1))
| def28 ),
inference(resolution,[status(thm)],[p802,c346]) ).
cnf(p832,plain,
( leq(sk27,pred(n6))
| def28 ),
inference(superposition,[status(thm)],[c234,p804]) ).
cnf(p890,plain,
( def28
| def3(sk27,sk28)
| def28 ),
inference(resolution,[status(thm)],[p889,p832]) ).
cnf(p902,plain,
( def3(sk27,sk28)
| def28 ),
inference(factoring,[status(thm)],[p890]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p903,plain,
( ~ leq(n0,sk28)
| ~ leq(n0,sk27)
| def28 ),
inference(resolution,[status(thm)],[p902,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,def53,def54])],[f52_sk]) ).
cnf(p803,plain,
( def29
| def28 ),
inference(resolution,[status(thm)],[p802,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p806,plain,
( leq(n0,sk27)
| def28 ),
inference(resolution,[status(thm)],[p803,c342]) ).
cnf(p906,plain,
( def28
| ~ leq(n0,sk28)
| def28 ),
inference(resolution,[status(thm)],[p903,p806]) ).
cnf(p907,plain,
( ~ leq(n0,sk28)
| def28 ),
inference(factoring,[status(thm)],[p906]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p805,plain,
( leq(n0,sk28)
| def28 ),
inference(resolution,[status(thm)],[p803,c343]) ).
cnf(p910,plain,
( def28
| def28 ),
inference(resolution,[status(thm)],[p907,p805]) ).
cnf(p911,plain,
def28,
inference(factoring,[status(thm)],[p910]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p912,plain,
( ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5) ),
inference(resolution,[status(thm)],[p911,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p685,plain,
def2,
inference(resolution,[status(thm)],[p683,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p686,plain,
def1,
inference(resolution,[status(thm)],[p685,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p689,plain,
def0,
inference(resolution,[status(thm)],[p686,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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p690,plain,
leq(n0,pv5),
inference(resolution,[status(thm)],[p689,c255]) ).
cnf(p915,plain,
~ leq(pv5,pred(n999)),
inference(resolution,[status(thm)],[p912,p690]) ).
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,def50,def51,def52,def53,def54])],[f52_sk]) ).
cnf(p688,plain,
leq(pv5,minus(n999,n1)),
inference(resolution,[status(thm)],[p686,c259]) ).
cnf(p830,plain,
leq(pv5,pred(n999)),
inference(superposition,[status(thm)],[c234,p688]) ).
cnf(p916,plain,
$false,
inference(resolution,[status(thm)],[p915,p830]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV109+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n011.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 18:32:12 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.80/4.00 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.80/4.00 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------