%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV117+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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:12:18 PM UTC 2026
% Result : Theorem 41.67s 11.43s
% Output : Proof 41.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 2
% Syntax : Number of formulae : 179 ( 23 unt; 0 def)
% Number of atoms : 552 ( 52 equ)
% Maximal formula atoms : 44 ( 3 avg)
% Number of connectives : 538 ( 165 ~; 243 |; 108 &)
% ( 0 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 46 ( 44 usr; 23 prp; 0-8 aty)
% Number of functors : 23 ( 23 usr; 19 con; 0-3 aty)
% Number of variables : 192 ( 65 sgn 51 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f52,conjecture,
( ( ! [G] :
( ( leq(G,minus(plus(n1,minus(n6,n1)),n1))
& leq(n0,G) )
=> ! [H] :
( ( leq(H,minus(n6,n1))
& leq(n0,H) )
=> a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G) ) )
& ! [E,F] :
( ( leq(F,minus(n6,n1))
& leq(E,minus(n6,n1))
& leq(n0,F)
& leq(n0,E) )
=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) )
& ! [C,D] :
( ( leq(D,minus(n3,n1))
& leq(C,minus(n3,n1))
& leq(n0,D)
& leq(n0,C) )
=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) )
& ! [A,B] :
( ( leq(B,minus(n6,n1))
& leq(A,minus(n6,n1))
& leq(n0,B)
& leq(n0,A) )
=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) )
=> ( ! [O] :
( ( leq(O,minus(n6,n1))
& leq(n0,O) )
=> ! [P] :
( ( leq(P,minus(n6,n1))
& leq(n0,P) )
=> a_select3(id_ds1_filter,O,P) = a_select3(id_ds1_filter,P,O) ) )
& ! [M,N] :
( ( leq(N,minus(n6,n1))
& leq(M,minus(n6,n1))
& leq(n0,N)
& leq(n0,M) )
=> a_select3(pminus_ds1_filter,M,N) = a_select3(pminus_ds1_filter,N,M) )
& ! [K,L] :
( ( leq(L,minus(n3,n1))
& leq(K,minus(n3,n1))
& leq(n0,L)
& leq(n0,K) )
=> a_select3(r_ds1_filter,K,L) = a_select3(r_ds1_filter,L,K) )
& ! [I,J] :
( ( leq(J,minus(n6,n1))
& leq(I,minus(n6,n1))
& leq(n0,J)
& leq(n0,I) )
=> a_select3(q_ds1_filter,I,J) = a_select3(q_ds1_filter,J,I) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quaternion_ds1_symm_0010) ).
fof(f52_neg,negated_conjecture,
~ ( ( ! [G] :
( ( leq(G,minus(plus(n1,minus(n6,n1)),n1))
& leq(n0,G) )
=> ! [H] :
( ( leq(H,minus(n6,n1))
& leq(n0,H) )
=> a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G) ) )
& ! [E,F] :
( ( leq(F,minus(n6,n1))
& leq(E,minus(n6,n1))
& leq(n0,F)
& leq(n0,E) )
=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) )
& ! [C,D] :
( ( leq(D,minus(n3,n1))
& leq(C,minus(n3,n1))
& leq(n0,D)
& leq(n0,C) )
=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) )
& ! [A,B] :
( ( leq(B,minus(n6,n1))
& leq(A,minus(n6,n1))
& leq(n0,B)
& leq(n0,A) )
=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) )
=> ( ! [O] :
( ( leq(O,minus(n6,n1))
& leq(n0,O) )
=> ! [P] :
( ( leq(P,minus(n6,n1))
& leq(n0,P) )
=> a_select3(id_ds1_filter,O,P) = a_select3(id_ds1_filter,P,O) ) )
& ! [M,N] :
( ( leq(N,minus(n6,n1))
& leq(M,minus(n6,n1))
& leq(n0,N)
& leq(n0,M) )
=> a_select3(pminus_ds1_filter,M,N) = a_select3(pminus_ds1_filter,N,M) )
& ! [K,L] :
( ( leq(L,minus(n3,n1))
& leq(K,minus(n3,n1))
& leq(n0,L)
& leq(n0,K) )
=> a_select3(r_ds1_filter,K,L) = a_select3(r_ds1_filter,L,K) )
& ! [I,J] :
( ( leq(J,minus(n6,n1))
& leq(I,minus(n6,n1))
& leq(n0,J)
& leq(n0,I) )
=> a_select3(q_ds1_filter,I,J) = a_select3(q_ds1_filter,J,I) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5) ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f52_nnf,plain,
( ( ? [O] :
( ? [P] :
( a_select3(id_ds1_filter,O,P) != a_select3(id_ds1_filter,P,O)
& leq(P,minus(n6,n1))
& leq(n0,P) )
& leq(O,minus(n6,n1))
& leq(n0,O) )
| ? [M,N] :
( a_select3(pminus_ds1_filter,M,N) != a_select3(pminus_ds1_filter,N,M)
& leq(N,minus(n6,n1))
& leq(M,minus(n6,n1))
& leq(n0,N)
& leq(n0,M) )
| ? [K,L] :
( a_select3(r_ds1_filter,K,L) != a_select3(r_ds1_filter,L,K)
& leq(L,minus(n3,n1))
& leq(K,minus(n3,n1))
& leq(n0,L)
& leq(n0,K) )
| ? [I,J] :
( a_select3(q_ds1_filter,I,J) != a_select3(q_ds1_filter,J,I)
& leq(J,minus(n6,n1))
& leq(I,minus(n6,n1))
& leq(n0,J)
& leq(n0,I) )
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5) )
& ! [G] :
( ! [H] :
( a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G)
| ~ leq(H,minus(n6,n1))
| ~ leq(n0,H) )
| ~ leq(G,minus(plus(n1,minus(n6,n1)),n1))
| ~ 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] :
( ( ( a_select3(id_ds1_filter,sk33,sk34) != a_select3(id_ds1_filter,sk34,sk33)
& leq(sk34,minus(n6,n1))
& leq(n0,sk34)
& leq(sk33,minus(n6,n1))
& leq(n0,sk33) )
| ( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
& leq(sk32,minus(n6,n1))
& leq(sk31,minus(n6,n1))
& leq(n0,sk32)
& leq(n0,sk31) )
| ( a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
& leq(sk30,minus(n3,n1))
& leq(sk29,minus(n3,n1))
& leq(n0,sk30)
& leq(n0,sk29) )
| ( a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27)
& leq(sk28,minus(n6,n1))
& leq(sk27,minus(n6,n1))
& leq(n0,sk28)
& leq(n0,sk27) )
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5) )
& ( a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G)
| ~ leq(H,minus(n6,n1))
| ~ leq(n0,H)
| ~ leq(G,minus(plus(n1,minus(n6,n1)),n1))
| ~ 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])],[f52_nnf]) ).
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])],[f52_sk]) ).
cnf(c381,plain,
( def20(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ def42(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])],[f52_sk]) ).
cnf(c384,plain,
def42(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])],[f52_sk]) ).
cnf(p443,plain,
def20(X0,X1,X2,X3,X4,X5,X6,X7),
inference(resolution,[status(thm)],[c381,c384]) ).
cnf(p6563,plain,
def15(X0,X1,X2,X3,X4,X5),
inference(resolution,[status(thm)],[c315,p443]) ).
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])],[f52_sk]) ).
cnf(p6565,plain,
def10(X0,X1,X2,X3),
inference(resolution,[status(thm)],[p6563,c300]) ).
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])],[f52_sk]) ).
cnf(p6568,plain,
def5(X0,X1),
inference(resolution,[status(thm)],[p6565,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])],[f52_sk]) ).
cnf(p6570,plain,
def4(X0,X1),
inference(resolution,[status(thm)],[p6568,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])],[f52_sk]) ).
cnf(p6574,plain,
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| def3(X0,X1) ),
inference(resolution,[status(thm)],[p6570,c267]) ).
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])],[f52_sk]) ).
cnf(p6567,plain,
def9(X0,X1),
inference(resolution,[status(thm)],[p6565,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])],[f52_sk]) ).
cnf(p6569,plain,
( a_select3(r_ds1_filter,X0,X1) = a_select3(r_ds1_filter,X1,X0)
| def8(X0,X1) ),
inference(resolution,[status(thm)],[p6567,c282]) ).
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])],[f52_sk]) ).
cnf(p6564,plain,
def14(X0,X1),
inference(resolution,[status(thm)],[p6563,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])],[f52_sk]) ).
cnf(p6566,plain,
( a_select3(pminus_ds1_filter,X0,X1) = a_select3(pminus_ds1_filter,X1,X0)
| def13(X0,X1) ),
inference(resolution,[status(thm)],[p6564,c297]) ).
cnf(c309,plain,
( a_select3(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6)
| def17(X7)
| ~ def18(X7,X6) ),
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])],[f52_sk]) ).
cnf(c316,plain,
( def19(X6,X7)
| ~ 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])],[f52_sk]) ).
cnf(p589,plain,
def19(X0,X1),
inference(resolution,[status(thm)],[c316,p443]) ).
cnf(c312,plain,
( def18(X7,X6)
| def16(X6)
| ~ 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])],[f52_sk]) ).
cnf(p590,plain,
( def18(X1,X0)
| def16(X0) ),
inference(resolution,[status(thm)],[p589,c312]) ).
cnf(p591,plain,
( def16(X1)
| a_select3(id_ds1_filter,X1,X0) = a_select3(id_ds1_filter,X0,X1)
| def17(X0) ),
inference(resolution,[status(thm)],[c309,p590]) ).
cnf(c382,plain,
( def41
| ~ def42(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])],[f52_sk]) ).
cnf(p434,plain,
def41,
inference(resolution,[status(thm)],[c382,c384]) ).
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])],[f52_sk]) ).
cnf(p435,plain,
( def40
| def36 ),
inference(resolution,[status(thm)],[p434,c378]) ).
cnf(c376,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])],[f52_sk]) ).
cnf(p437,plain,
( def39
| def36 ),
inference(resolution,[status(thm)],[p435,c376]) ).
cnf(c373,plain,
( a_select3(id_ds1_filter,sk33,sk34) != a_select3(id_ds1_filter,sk34,sk33)
| ~ 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])],[f52_sk]) ).
cnf(p440,plain,
( a_select3(id_ds1_filter,sk33,sk34) != a_select3(id_ds1_filter,sk34,sk33)
| def36 ),
inference(resolution,[status(thm)],[p437,c373]) ).
cnf(p592,plain,
( def36
| def16(sk33)
| def17(sk34) ),
inference(resolution,[status(thm)],[p591,p440]) ).
cnf(c306,plain,
( ~ leq(X7,minus(n6,n1))
| ~ leq(n0,X7)
| ~ def17(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])],[f52_sk]) ).
cnf(p598,plain,
( ~ leq(sk34,pred(n6))
| ~ leq(n0,sk34)
| def36
| def16(sk33) ),
inference(resolution,[status(thm)],[p592,c306]) ).
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])],[f52_sk]) ).
cnf(p439,plain,
( def38
| def36 ),
inference(resolution,[status(thm)],[p437,c372]) ).
cnf(c369,plain,
( leq(n0,sk34)
| ~ 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])],[f52_sk]) ).
cnf(p441,plain,
( leq(n0,sk34)
| def36 ),
inference(resolution,[status(thm)],[p439,c369]) ).
cnf(p599,plain,
( def36
| ~ leq(sk34,pred(n6))
| def36
| def16(sk33) ),
inference(resolution,[status(thm)],[p598,p441]) ).
cnf(p601,plain,
( ~ leq(sk34,pred(n6))
| def36
| def16(sk33) ),
inference(factoring,[status(thm)],[p599]) ).
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(c370,plain,
( leq(sk34,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])],[f52_sk]) ).
cnf(p442,plain,
( leq(sk34,minus(n6,n1))
| def36 ),
inference(resolution,[status(thm)],[p439,c370]) ).
cnf(p450,plain,
( leq(sk34,pred(n6))
| def36 ),
inference(superposition,[status(thm)],[c234,p442]) ).
cnf(p602,plain,
( def36
| def36
| def16(sk33) ),
inference(resolution,[status(thm)],[p601,p450]) ).
cnf(p609,plain,
( def36
| def16(sk33) ),
inference(factoring,[status(thm)],[p602]) ).
cnf(c303,plain,
( ~ leq(X6,minus(plus(n1,minus(n6,n1)),n1))
| ~ leq(n0,X6)
| ~ def16(X6) ),
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])],[f52_sk]) ).
cnf(p610,plain,
( ~ leq(sk33,pred(n6))
| ~ leq(n0,sk33)
| def36 ),
inference(resolution,[status(thm)],[p609,c303]) ).
cnf(c366,plain,
( leq(n0,sk33)
| ~ 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])],[f52_sk]) ).
cnf(c375,plain,
( def37
| ~ 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])],[f52_sk]) ).
cnf(p436,plain,
( def37
| def36 ),
inference(resolution,[status(thm)],[p435,c375]) ).
cnf(p444,plain,
( def36
| leq(n0,sk33) ),
inference(resolution,[status(thm)],[c366,p436]) ).
cnf(p611,plain,
( def36
| ~ leq(sk33,pred(n6))
| def36 ),
inference(resolution,[status(thm)],[p610,p444]) ).
cnf(p613,plain,
( ~ leq(sk33,pred(n6))
| def36 ),
inference(factoring,[status(thm)],[p611]) ).
cnf(c367,plain,
( leq(sk33,minus(n6,n1))
| ~ 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])],[f52_sk]) ).
cnf(p438,plain,
( leq(sk33,minus(n6,n1))
| def36 ),
inference(resolution,[status(thm)],[p436,c367]) ).
cnf(p449,plain,
( leq(sk33,pred(n6))
| def36 ),
inference(superposition,[status(thm)],[c234,p438]) ).
cnf(p614,plain,
( def36
| def36 ),
inference(resolution,[status(thm)],[p613,p449]) ).
cnf(p621,plain,
def36,
inference(factoring,[status(thm)],[p614]) ).
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])],[f52_sk]) ).
cnf(p622,plain,
( def35
| def31 ),
inference(resolution,[status(thm)],[p621,c363]) ).
cnf(c361,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| ~ 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])],[f52_sk]) ).
cnf(p624,plain,
( a_select3(pminus_ds1_filter,sk31,sk32) != a_select3(pminus_ds1_filter,sk32,sk31)
| def31 ),
inference(resolution,[status(thm)],[p622,c361]) ).
cnf(p6627,plain,
( def31
| def13(sk31,sk32) ),
inference(resolution,[status(thm)],[p6566,p624]) ).
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])],[f52_sk]) ).
cnf(p6630,plain,
( ~ leq(sk32,pred(n6))
| def12(sk31,sk32)
| def31 ),
inference(resolution,[status(thm)],[p6627,c294]) ).
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])],[f52_sk]) ).
cnf(p623,plain,
( def34
| def31 ),
inference(resolution,[status(thm)],[p622,c360]) ).
cnf(c358,plain,
( leq(sk32,minus(n6,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])],[f52_sk]) ).
cnf(p626,plain,
( leq(sk32,pred(n6))
| def31 ),
inference(resolution,[status(thm)],[p623,c358]) ).
cnf(p6636,plain,
( def31
| def12(sk31,sk32)
| def31 ),
inference(resolution,[status(thm)],[p6630,p626]) ).
cnf(p6640,plain,
( def12(sk31,sk32)
| def31 ),
inference(factoring,[status(thm)],[p6636]) ).
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])],[f52_sk]) ).
cnf(p6641,plain,
( ~ leq(sk31,pred(n6))
| def11(sk31,sk32)
| def31 ),
inference(resolution,[status(thm)],[p6640,c291]) ).
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])],[f52_sk]) ).
cnf(p625,plain,
( def33
| def31 ),
inference(resolution,[status(thm)],[p623,c357]) ).
cnf(c355,plain,
( leq(sk31,minus(n6,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])],[f52_sk]) ).
cnf(p628,plain,
( leq(sk31,pred(n6))
| def31 ),
inference(resolution,[status(thm)],[p625,c355]) ).
cnf(p6647,plain,
( def31
| def11(sk31,sk32)
| def31 ),
inference(resolution,[status(thm)],[p6641,p628]) ).
cnf(p6651,plain,
( def11(sk31,sk32)
| def31 ),
inference(factoring,[status(thm)],[p6647]) ).
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])],[f52_sk]) ).
cnf(p6652,plain,
( ~ leq(n0,sk32)
| ~ leq(n0,sk31)
| def31 ),
inference(resolution,[status(thm)],[p6651,c288]) ).
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])],[f52_sk]) ).
cnf(p627,plain,
( def32
| def31 ),
inference(resolution,[status(thm)],[p625,c354]) ).
cnf(c351,plain,
( leq(n0,sk31)
| ~ 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])],[f52_sk]) ).
cnf(p629,plain,
( leq(n0,sk31)
| def31 ),
inference(resolution,[status(thm)],[p627,c351]) ).
cnf(p6655,plain,
( def31
| ~ leq(n0,sk32)
| def31 ),
inference(resolution,[status(thm)],[p6652,p629]) ).
cnf(p6656,plain,
( ~ leq(n0,sk32)
| def31 ),
inference(factoring,[status(thm)],[p6655]) ).
cnf(c352,plain,
( leq(n0,sk32)
| ~ 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])],[f52_sk]) ).
cnf(p630,plain,
( leq(n0,sk32)
| def31 ),
inference(resolution,[status(thm)],[p627,c352]) ).
cnf(p6659,plain,
( def31
| def31 ),
inference(resolution,[status(thm)],[p6656,p630]) ).
cnf(p6660,plain,
def31,
inference(factoring,[status(thm)],[p6659]) ).
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])],[f52_sk]) ).
cnf(p6661,plain,
( def30
| def26 ),
inference(resolution,[status(thm)],[p6660,c348]) ).
cnf(c346,plain,
( a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| ~ 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])],[f52_sk]) ).
cnf(p6663,plain,
( a_select3(r_ds1_filter,sk29,sk30) != a_select3(r_ds1_filter,sk30,sk29)
| def26 ),
inference(resolution,[status(thm)],[p6661,c346]) ).
cnf(p6766,plain,
( def26
| def8(sk29,sk30) ),
inference(resolution,[status(thm)],[p6569,p6663]) ).
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])],[f52_sk]) ).
cnf(p6769,plain,
( ~ leq(sk30,n2)
| def7(sk29,sk30)
| def26 ),
inference(resolution,[status(thm)],[p6766,c279]) ).
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])],[f52_sk]) ).
cnf(p6662,plain,
( def29
| def26 ),
inference(resolution,[status(thm)],[p6661,c345]) ).
cnf(c343,plain,
( leq(sk30,minus(n3,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])],[f52_sk]) ).
cnf(p6664,plain,
( leq(sk30,n2)
| def26 ),
inference(resolution,[status(thm)],[p6662,c343]) ).
cnf(p6770,plain,
( def26
| def7(sk29,sk30)
| def26 ),
inference(resolution,[status(thm)],[p6769,p6664]) ).
cnf(p6771,plain,
( def7(sk29,sk30)
| def26 ),
inference(factoring,[status(thm)],[p6770]) ).
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])],[f52_sk]) ).
cnf(p6772,plain,
( ~ leq(sk29,n2)
| def6(sk29,sk30)
| def26 ),
inference(resolution,[status(thm)],[p6771,c276]) ).
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])],[f52_sk]) ).
cnf(p6665,plain,
( def28
| def26 ),
inference(resolution,[status(thm)],[p6662,c342]) ).
cnf(c340,plain,
( leq(sk29,minus(n3,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])],[f52_sk]) ).
cnf(p6667,plain,
( leq(sk29,n2)
| def26 ),
inference(resolution,[status(thm)],[p6665,c340]) ).
cnf(p6773,plain,
( def26
| def6(sk29,sk30)
| def26 ),
inference(resolution,[status(thm)],[p6772,p6667]) ).
cnf(p6774,plain,
( def6(sk29,sk30)
| def26 ),
inference(factoring,[status(thm)],[p6773]) ).
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])],[f52_sk]) ).
cnf(p6775,plain,
( ~ leq(n0,sk30)
| ~ leq(n0,sk29)
| def26 ),
inference(resolution,[status(thm)],[p6774,c273]) ).
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])],[f52_sk]) ).
cnf(p6666,plain,
( def27
| def26 ),
inference(resolution,[status(thm)],[p6665,c339]) ).
cnf(c336,plain,
( leq(n0,sk29)
| ~ 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])],[f52_sk]) ).
cnf(p6668,plain,
( leq(n0,sk29)
| def26 ),
inference(resolution,[status(thm)],[p6666,c336]) ).
cnf(p6778,plain,
( def26
| ~ leq(n0,sk30)
| def26 ),
inference(resolution,[status(thm)],[p6775,p6668]) ).
cnf(p6779,plain,
( ~ leq(n0,sk30)
| def26 ),
inference(factoring,[status(thm)],[p6778]) ).
cnf(c337,plain,
( leq(n0,sk30)
| ~ 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])],[f52_sk]) ).
cnf(p6669,plain,
( leq(n0,sk30)
| def26 ),
inference(resolution,[status(thm)],[p6666,c337]) ).
cnf(p6782,plain,
( def26
| def26 ),
inference(resolution,[status(thm)],[p6779,p6669]) ).
cnf(p6783,plain,
def26,
inference(factoring,[status(thm)],[p6782]) ).
cnf(c333,plain,
( def25
| def21
| ~ 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])],[f52_sk]) ).
cnf(p6784,plain,
( def25
| def21 ),
inference(resolution,[status(thm)],[p6783,c333]) ).
cnf(c331,plain,
( a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27)
| ~ def25 ),
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])],[f52_sk]) ).
cnf(p6786,plain,
( a_select3(q_ds1_filter,sk27,sk28) != a_select3(q_ds1_filter,sk28,sk27)
| def21 ),
inference(resolution,[status(thm)],[p6784,c331]) ).
cnf(p6863,plain,
( def21
| def3(sk27,sk28) ),
inference(resolution,[status(thm)],[p6574,p6786]) ).
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])],[f52_sk]) ).
cnf(p6866,plain,
( ~ leq(sk28,pred(n6))
| def2(sk27,sk28)
| def21 ),
inference(resolution,[status(thm)],[p6863,c264]) ).
cnf(c330,plain,
( def24
| ~ def25 ),
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])],[f52_sk]) ).
cnf(p6785,plain,
( def24
| def21 ),
inference(resolution,[status(thm)],[p6784,c330]) ).
cnf(c328,plain,
( leq(sk28,minus(n6,n1))
| ~ def24 ),
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])],[f52_sk]) ).
cnf(p6788,plain,
( leq(sk28,pred(n6))
| def21 ),
inference(resolution,[status(thm)],[p6785,c328]) ).
cnf(p6875,plain,
( def21
| def2(sk27,sk28)
| def21 ),
inference(resolution,[status(thm)],[p6866,p6788]) ).
cnf(p6876,plain,
( def2(sk27,sk28)
| def21 ),
inference(factoring,[status(thm)],[p6875]) ).
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])],[f52_sk]) ).
cnf(p6877,plain,
( ~ leq(sk27,pred(n6))
| def1(sk27,sk28)
| def21 ),
inference(resolution,[status(thm)],[p6876,c261]) ).
cnf(c327,plain,
( def23
| ~ def24 ),
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])],[f52_sk]) ).
cnf(p6787,plain,
( def23
| def21 ),
inference(resolution,[status(thm)],[p6785,c327]) ).
cnf(c325,plain,
( leq(sk27,minus(n6,n1))
| ~ def23 ),
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])],[f52_sk]) ).
cnf(p6789,plain,
( leq(sk27,pred(n6))
| def21 ),
inference(resolution,[status(thm)],[p6787,c325]) ).
cnf(p6886,plain,
( def21
| def1(sk27,sk28)
| def21 ),
inference(resolution,[status(thm)],[p6877,p6789]) ).
cnf(p6887,plain,
( def1(sk27,sk28)
| def21 ),
inference(factoring,[status(thm)],[p6886]) ).
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])],[f52_sk]) ).
cnf(p6888,plain,
( ~ leq(n0,sk28)
| ~ leq(n0,sk27)
| def21 ),
inference(resolution,[status(thm)],[p6887,c258]) ).
cnf(c324,plain,
( def22
| ~ def23 ),
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])],[f52_sk]) ).
cnf(p6790,plain,
( def22
| def21 ),
inference(resolution,[status(thm)],[p6787,c324]) ).
cnf(c321,plain,
( leq(n0,sk27)
| ~ def22 ),
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])],[f52_sk]) ).
cnf(p6791,plain,
( leq(n0,sk27)
| def21 ),
inference(resolution,[status(thm)],[p6790,c321]) ).
cnf(p6891,plain,
( def21
| ~ leq(n0,sk28)
| def21 ),
inference(resolution,[status(thm)],[p6888,p6791]) ).
cnf(p6892,plain,
( ~ leq(n0,sk28)
| def21 ),
inference(factoring,[status(thm)],[p6891]) ).
cnf(c322,plain,
( leq(n0,sk28)
| ~ def22 ),
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])],[f52_sk]) ).
cnf(p6792,plain,
( leq(n0,sk28)
| def21 ),
inference(resolution,[status(thm)],[p6790,c322]) ).
cnf(p6895,plain,
( def21
| def21 ),
inference(resolution,[status(thm)],[p6892,p6792]) ).
cnf(p6896,plain,
def21,
inference(factoring,[status(thm)],[p6895]) ).
cnf(c318,plain,
( ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| ~ def21 ),
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])],[f52_sk]) ).
cnf(p6897,plain,
( ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5) ),
inference(resolution,[status(thm)],[p6896,c318]) ).
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])],[f52_sk]) ).
cnf(p6571,plain,
def0,
inference(resolution,[status(thm)],[p6568,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])],[f52_sk]) ).
cnf(p6572,plain,
leq(n0,pv5),
inference(resolution,[status(thm)],[p6571,c255]) ).
cnf(p6900,plain,
~ leq(pv5,pred(n999)),
inference(resolution,[status(thm)],[p6897,p6572]) ).
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])],[f52_sk]) ).
cnf(p6573,plain,
leq(pv5,pred(n999)),
inference(resolution,[status(thm)],[p6571,c256]) ).
cnf(p6901,plain,
$false,
inference(resolution,[status(thm)],[p6900,p6573]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV117+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/5.38 % Computer : n009.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Thu Sep 24 18:33:19 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 41.67/11.43 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 41.67/11.43 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------