%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV038+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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:11:56 PM UTC 2026
% Result : Theorem 25.56s 4.17s
% Output : Proof 25.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 142
% Number of leaves : 2
% Syntax : Number of formulae : 319 ( 57 unt; 0 def)
% Number of atoms : 965 ( 165 equ)
% Maximal formula atoms : 59 ( 3 avg)
% Number of connectives : 939 ( 293 ~; 472 |; 144 &)
% ( 0 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 41 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 63 ( 61 usr; 44 prp; 0-5 aty)
% Number of functors : 28 ( 28 usr; 25 con; 0-3 aty)
% Number of variables : 136 ( 54 sgn 30 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f52,conjecture,
( ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [E] :
( ( leq(E,minus(n3,n1))
& leq(n0,E) )
=> a_select2(s_try7_init,E) = init )
& ! [D] :
( ( leq(D,n2)
& leq(n0,D) )
=> a_select2(s_center7_init,D) = init )
& ! [C] :
( ( leq(C,n3)
& leq(n0,C) )
=> a_select2(s_values7_init,C) = init )
& ! [A] :
( ( leq(A,n2)
& leq(n0,A) )
=> ! [B] :
( ( leq(B,n3)
& leq(n0,B) )
=> a_select3(simplex7_init,B,A) = init ) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init )
=> ( ( n0 = pv1413
=> true )
& ( n0 != pv1413
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [J] :
( ( leq(J,minus(n3,n1))
& leq(n0,J) )
=> a_select2(s_try7_init,J) = init )
& ! [I] :
( ( leq(I,n2)
& leq(n0,I) )
=> a_select2(s_center7_init,I) = init )
& ! [H] :
( ( leq(H,n3)
& leq(n0,H) )
=> a_select2(s_values7_init,H) = init )
& ! [F] :
( ( leq(F,n2)
& leq(n0,F) )
=> ! [G] :
( ( leq(G,n3)
& leq(n0,G) )
=> a_select3(simplex7_init,G,F) = init ) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init
& init = init ) )
& init = init ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gauss_init_0065) ).
fof(f52_neg,negated_conjecture,
~ ( ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [E] :
( ( leq(E,minus(n3,n1))
& leq(n0,E) )
=> a_select2(s_try7_init,E) = init )
& ! [D] :
( ( leq(D,n2)
& leq(n0,D) )
=> a_select2(s_center7_init,D) = init )
& ! [C] :
( ( leq(C,n3)
& leq(n0,C) )
=> a_select2(s_values7_init,C) = init )
& ! [A] :
( ( leq(A,n2)
& leq(n0,A) )
=> ! [B] :
( ( leq(B,n3)
& leq(n0,B) )
=> a_select3(simplex7_init,B,A) = init ) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init )
=> ( ( n0 = pv1413
=> true )
& ( n0 != pv1413
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [J] :
( ( leq(J,minus(n3,n1))
& leq(n0,J) )
=> a_select2(s_try7_init,J) = init )
& ! [I] :
( ( leq(I,n2)
& leq(n0,I) )
=> a_select2(s_center7_init,I) = init )
& ! [H] :
( ( leq(H,n3)
& leq(n0,H) )
=> a_select2(s_values7_init,H) = init )
& ! [F] :
( ( leq(F,n2)
& leq(n0,F) )
=> ! [G] :
( ( leq(G,n3)
& leq(n0,G) )
=> a_select3(simplex7_init,G,F) = init ) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init
& init = init ) )
& init = init ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f52_nnf,plain,
( ( ( ~ true
& n0 = pv1413 )
| ( ( ( ( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init )
& gt(loopcounter,n1) )
| ? [J] :
( a_select2(s_try7_init,J) != init
& leq(J,minus(n3,n1))
& leq(n0,J) )
| ? [I] :
( a_select2(s_center7_init,I) != init
& leq(I,n2)
& leq(n0,I) )
| ? [H] :
( a_select2(s_values7_init,H) != init
& leq(H,n3)
& leq(n0,H) )
| ? [F] :
( ? [G] :
( a_select3(simplex7_init,G,F) != init
& leq(G,n3)
& leq(n0,G) )
& leq(F,n2)
& leq(n0,F) )
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_sworst7_init != init
| s_best7_init != init
| init != init )
& n0 != pv1413 )
| init != init )
& ( ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init )
| ~ gt(loopcounter,n1) )
& ! [E] :
( a_select2(s_try7_init,E) = init
| ~ leq(E,minus(n3,n1))
| ~ leq(n0,E) )
& ! [D] :
( a_select2(s_center7_init,D) = init
| ~ leq(D,n2)
| ~ leq(n0,D) )
& ! [C] :
( a_select2(s_values7_init,C) = init
| ~ leq(C,n3)
| ~ leq(n0,C) )
& ! [A] :
( ! [B] :
( a_select3(simplex7_init,B,A) = init
| ~ leq(B,n3)
| ~ leq(n0,B) )
| ~ leq(A,n2)
| ~ leq(n0,A) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init ),
inference(nnf_transformation,[status(thm)],[f52_neg]) ).
fof(f52_sk,plain,
! [A,B,C,D,E] :
( ( ( ~ true
& n0 = pv1413 )
| ( ( ( ( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init )
& gt(loopcounter,n1) )
| ( a_select2(s_try7_init,sk31) != init
& leq(sk31,minus(n3,n1))
& leq(n0,sk31) )
| ( a_select2(s_center7_init,sk30) != init
& leq(sk30,n2)
& leq(n0,sk30) )
| ( a_select2(s_values7_init,sk29) != init
& leq(sk29,n3)
& leq(n0,sk29) )
| ( a_select3(simplex7_init,sk28,sk27) != init
& leq(sk28,n3)
& leq(n0,sk28)
& leq(sk27,n2)
& leq(n0,sk27) )
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| s_worst7_init != init
| s_sworst7_init != init
| s_best7_init != init
| init != init )
& n0 != pv1413 )
| init != init )
& ( ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init )
| ~ gt(loopcounter,n1) )
& ( a_select2(s_try7_init,E) = init
| ~ leq(E,minus(n3,n1))
| ~ leq(n0,E) )
& ( a_select2(s_center7_init,D) = init
| ~ leq(D,n2)
| ~ leq(n0,D) )
& ( a_select2(s_values7_init,C) = init
| ~ leq(C,n3)
| ~ leq(n0,C) )
& ( a_select3(simplex7_init,B,A) = init
| ~ leq(B,n3)
| ~ leq(n0,B)
| ~ leq(A,n2)
| ~ leq(n0,A) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk27,sk28,sk29,sk30,sk31])],[f52_nnf]) ).
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,def55,def56,def57])],[f52_sk]) ).
cnf(c312,plain,
( ~ leq(X4,minus(n3,n1))
| ~ leq(n0,X4)
| ~ def19(X4) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(c309,plain,
( def15(X0,X1,X2)
| ~ def18(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,def55,def56,def57])],[f52_sk]) ).
cnf(c426,plain,
( def25(X0,X1,X2,X3,X4)
| ~ def57(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(c429,plain,
def57(X0,X1,X2,X3,X4),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p497,plain,
def25(X0,X1,X2,X3,X4),
inference(resolution,[status(thm)],[c426,c429]) ).
cnf(c330,plain,
( def21(X0,X1,X2,X3,X4)
| ~ def25(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p499,plain,
def21(X0,X1,X2,X3,X4),
inference(resolution,[status(thm)],[p497,c330]) ).
cnf(c318,plain,
( def18(X0,X1,X2,X3)
| ~ def21(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p544,plain,
def18(X0,X1,X2,X3),
inference(resolution,[status(thm)],[p499,c318]) ).
cnf(p592,plain,
def15(X0,X1,X2),
inference(resolution,[status(thm)],[c309,p544]) ).
cnf(c300,plain,
( def12(X0,X1)
| ~ def15(X0,X1,X2) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p593,plain,
def12(X0,X1),
inference(resolution,[status(thm)],[p592,c300]) ).
cnf(c291,plain,
( def7
| ~ def12(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,def55,def56,def57])],[f52_sk]) ).
cnf(p596,plain,
def7,
inference(resolution,[status(thm)],[p593,c291]) ).
cnf(c276,plain,
( def6
| ~ def7 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p598,plain,
def6,
inference(resolution,[status(thm)],[p596,c276]) ).
cnf(c273,plain,
( def5
| ~ def6 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p599,plain,
def5,
inference(resolution,[status(thm)],[p598,c273]) ).
cnf(c270,plain,
( def4
| ~ def5 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p601,plain,
def4,
inference(resolution,[status(thm)],[p599,c270]) ).
cnf(c267,plain,
( def3
| ~ def4 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p603,plain,
def3,
inference(resolution,[status(thm)],[p601,c267]) ).
cnf(c264,plain,
( def2
| ~ def3 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p605,plain,
def2,
inference(resolution,[status(thm)],[p603,c264]) ).
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,def55,def56,def57])],[f52_sk]) ).
cnf(p607,plain,
def1,
inference(resolution,[status(thm)],[p605,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,def55,def56,def57])],[f52_sk]) ).
cnf(p611,plain,
def0,
inference(resolution,[status(thm)],[p607,c258]) ).
cnf(c255,plain,
( s_best7_init = init
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p612,plain,
s_best7_init = init,
inference(resolution,[status(thm)],[p611,c255]) ).
cnf(c259,plain,
( s_worst7_init = init
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p609,plain,
s_worst7_init = init,
inference(resolution,[status(thm)],[p607,c259]) ).
cnf(p624,plain,
init = s_best7_init,
inference(superposition,[status(thm)],[p612,p609]) ).
cnf(c315,plain,
( a_select2(s_try7_init,X4) = init
| def19(X4)
| ~ def20(X4) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p627,plain,
( a_select2(s_try7_init,X0) = s_best7_init
| def19(X0)
| ~ def20(X0) ),
inference(demodulation,[status(thm)],[p624,c315]) ).
cnf(c319,plain,
( def20(X4)
| ~ def21(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p543,plain,
def20(X0),
inference(resolution,[status(thm)],[p499,c319]) ).
cnf(p654,plain,
( a_select2(s_try7_init,X0) = s_best7_init
| def19(X0) ),
inference(resolution,[status(thm)],[p627,p543]) ).
cnf(c331,plain,
( def24
| ~ def25(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p498,plain,
def24,
inference(resolution,[status(thm)],[p497,c331]) ).
cnf(c327,plain,
( def23
| ~ gt(loopcounter,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,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p500,plain,
( def23
| ~ gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p498,c327]) ).
cnf(c417,plain,
( def53
| init != init
| ~ def54 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p469,plain,
( def53
| ~ def54 ),
inference(equality_resolution,[status(thm)],[c417]) ).
cnf(c423,plain,
( def55
| def54
| ~ def56 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(c427,plain,
( def56
| ~ def57(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p464,plain,
def56,
inference(resolution,[status(thm)],[c427,c429]) ).
cnf(p465,plain,
( def55
| def54 ),
inference(resolution,[status(thm)],[c423,p464]) ).
cnf(c421,plain,
( ~ true
| ~ def55 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p466,plain,
( ~ true
| def54 ),
inference(resolution,[status(thm)],[p465,c421]) ).
fof(f50,axiom,
true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ttrue) ).
fof(f50_nnf,plain,
true,
inference(nnf_transformation,[status(thm)],[f50]) ).
cnf(c253,plain,
true,
inference(cnf_transformation,[status(esa)],[f50_nnf]) ).
cnf(p468,plain,
def54,
inference(resolution,[status(thm)],[p466,c253]) ).
cnf(p501,plain,
def53,
inference(resolution,[status(thm)],[p469,p468]) ).
cnf(c415,plain,
( def52
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p503,plain,
def52,
inference(resolution,[status(thm)],[p501,c415]) ).
cnf(c411,plain,
( def51
| def48
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p504,plain,
( def51
| def48 ),
inference(resolution,[status(thm)],[p503,c411]) ).
cnf(c408,plain,
( gt(loopcounter,n1)
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p506,plain,
( gt(loopcounter,n1)
| def48 ),
inference(resolution,[status(thm)],[p504,c408]) ).
cnf(p537,plain,
( def48
| def23 ),
inference(resolution,[status(thm)],[p500,p506]) ).
cnf(c399,plain,
( def47
| def45
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p538,plain,
( def47
| def45
| def23 ),
inference(resolution,[status(thm)],[p537,c399]) ).
cnf(c397,plain,
( a_select2(s_try7_init,sk31) != init
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p567,plain,
( a_select2(s_try7_init,sk31) != init
| def45
| def23 ),
inference(resolution,[status(thm)],[p538,c397]) ).
cnf(p622,plain,
( a_select2(s_try7_init,sk31) != s_best7_init
| def45
| def23 ),
inference(superposition,[status(thm)],[p612,p567]) ).
cnf(p655,plain,
( def45
| def23
| def19(sk31) ),
inference(resolution,[status(thm)],[p654,p622]) ).
cnf(p663,plain,
( def45
| def23
| ~ leq(sk31,minus(n3,n1))
| ~ leq(n0,sk31) ),
inference(resolution,[status(thm)],[c312,p655]) ).
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,def55,def56,def57])],[f52_sk]) ).
cnf(p566,plain,
( def46
| def45
| def23 ),
inference(resolution,[status(thm)],[p538,c396]) ).
cnf(c393,plain,
( leq(n0,sk31)
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p570,plain,
( leq(n0,sk31)
| def45
| def23 ),
inference(resolution,[status(thm)],[p566,c393]) ).
cnf(p668,plain,
( def45
| def23
| def45
| def23
| ~ leq(sk31,minus(n3,n1)) ),
inference(resolution,[status(thm)],[p663,p570]) ).
cnf(p698,plain,
( def45
| def45
| def23
| ~ leq(sk31,minus(n3,n1)) ),
inference(factoring,[status(thm)],[p668]) ).
cnf(p700,plain,
( def45
| def23
| ~ leq(sk31,minus(n3,n1)) ),
inference(factoring,[status(thm)],[p698]) ).
cnf(c394,plain,
( leq(sk31,minus(n3,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,def55,def56,def57])],[f52_sk]) ).
cnf(p571,plain,
( leq(sk31,minus(n3,n1))
| def45
| def23 ),
inference(resolution,[status(thm)],[p566,c394]) ).
cnf(p701,plain,
( def45
| def23
| def45
| def23 ),
inference(resolution,[status(thm)],[p700,p571]) ).
cnf(p702,plain,
( def45
| def45
| def23 ),
inference(factoring,[status(thm)],[p701]) ).
cnf(p704,plain,
( def45
| def23 ),
inference(factoring,[status(thm)],[p702]) ).
cnf(c390,plain,
( def44
| def42
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p705,plain,
( def44
| def42
| def23 ),
inference(resolution,[status(thm)],[p704,c390]) ).
cnf(c388,plain,
( a_select2(s_center7_init,sk30) != init
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p637,plain,
( a_select2(s_center7_init,sk30) != s_best7_init
| ~ def44 ),
inference(demodulation,[status(thm)],[p624,c388]) ).
cnf(p707,plain,
( a_select2(s_center7_init,sk30) != s_best7_init
| def42
| def23 ),
inference(resolution,[status(thm)],[p705,p637]) ).
cnf(c310,plain,
( def17(X3)
| ~ def18(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,def55,def56,def57])],[f52_sk]) ).
cnf(p545,plain,
def17(X0),
inference(resolution,[status(thm)],[p544,c310]) ).
cnf(c306,plain,
( a_select2(s_center7_init,X3) = init
| def16(X3)
| ~ def17(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,def55,def56,def57])],[f52_sk]) ).
cnf(p546,plain,
( a_select2(s_center7_init,X0) = init
| def16(X0) ),
inference(resolution,[status(thm)],[p545,c306]) ).
cnf(p621,plain,
( a_select2(s_center7_init,X0) = s_best7_init
| def16(X0) ),
inference(superposition,[status(thm)],[p612,p546]) ).
cnf(p710,plain,
( def16(sk30)
| def42
| def23 ),
inference(resolution,[status(thm)],[p707,p621]) ).
cnf(c303,plain,
( ~ leq(X3,n2)
| ~ leq(n0,X3)
| ~ def16(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,def55,def56,def57])],[f52_sk]) ).
cnf(p711,plain,
( ~ leq(sk30,n2)
| ~ leq(n0,sk30)
| def42
| def23 ),
inference(resolution,[status(thm)],[p710,c303]) ).
cnf(c387,plain,
( def43
| ~ def44 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p706,plain,
( def43
| def42
| def23 ),
inference(resolution,[status(thm)],[p705,c387]) ).
cnf(c384,plain,
( leq(n0,sk30)
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p708,plain,
( leq(n0,sk30)
| def42
| def23 ),
inference(resolution,[status(thm)],[p706,c384]) ).
cnf(p716,plain,
( def42
| def23
| ~ leq(sk30,n2)
| def42
| def23 ),
inference(resolution,[status(thm)],[p711,p708]) ).
cnf(p738,plain,
( def42
| ~ leq(sk30,n2)
| def42
| def23 ),
inference(factoring,[status(thm)],[p716]) ).
cnf(p740,plain,
( ~ leq(sk30,n2)
| def42
| def23 ),
inference(factoring,[status(thm)],[p738]) ).
cnf(c385,plain,
( leq(sk30,n2)
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p709,plain,
( leq(sk30,n2)
| def42
| def23 ),
inference(resolution,[status(thm)],[p706,c385]) ).
cnf(p741,plain,
( def42
| def23
| def42
| def23 ),
inference(resolution,[status(thm)],[p740,p709]) ).
cnf(p742,plain,
( def42
| def42
| def23 ),
inference(factoring,[status(thm)],[p741]) ).
cnf(p744,plain,
( def42
| def23 ),
inference(factoring,[status(thm)],[p742]) ).
cnf(c381,plain,
( def41
| def39
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p745,plain,
( def41
| def39
| def23 ),
inference(resolution,[status(thm)],[p744,c381]) ).
cnf(c379,plain,
( a_select2(s_values7_init,sk29) != init
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p635,plain,
( a_select2(s_values7_init,sk29) != s_best7_init
| ~ def41 ),
inference(demodulation,[status(thm)],[p624,c379]) ).
cnf(p747,plain,
( a_select2(s_values7_init,sk29) != s_best7_init
| def39
| def23 ),
inference(resolution,[status(thm)],[p745,p635]) ).
cnf(c297,plain,
( a_select2(s_values7_init,X2) = init
| def13(X2)
| ~ def14(X2) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p626,plain,
( a_select2(s_values7_init,X0) = s_best7_init
| def13(X0)
| ~ def14(X0) ),
inference(demodulation,[status(thm)],[p624,c297]) ).
cnf(c301,plain,
( def14(X2)
| ~ def15(X0,X1,X2) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p594,plain,
def14(X0),
inference(resolution,[status(thm)],[p592,c301]) ).
cnf(p653,plain,
( a_select2(s_values7_init,X0) = s_best7_init
| def13(X0) ),
inference(resolution,[status(thm)],[p626,p594]) ).
cnf(p750,plain,
( def13(sk29)
| def39
| def23 ),
inference(resolution,[status(thm)],[p747,p653]) ).
cnf(c294,plain,
( ~ leq(X2,n3)
| ~ leq(n0,X2)
| ~ def13(X2) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p751,plain,
( ~ leq(sk29,n3)
| ~ leq(n0,sk29)
| def39
| def23 ),
inference(resolution,[status(thm)],[p750,c294]) ).
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,def55,def56,def57])],[f52_sk]) ).
cnf(p746,plain,
( def40
| def39
| def23 ),
inference(resolution,[status(thm)],[p745,c378]) ).
cnf(c375,plain,
( leq(n0,sk29)
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p749,plain,
( leq(n0,sk29)
| def39
| def23 ),
inference(resolution,[status(thm)],[p746,c375]) ).
cnf(p756,plain,
( def39
| def23
| ~ leq(sk29,n3)
| def39
| def23 ),
inference(resolution,[status(thm)],[p751,p749]) ).
cnf(p775,plain,
( def39
| ~ leq(sk29,n3)
| def39
| def23 ),
inference(factoring,[status(thm)],[p756]) ).
cnf(p777,plain,
( ~ leq(sk29,n3)
| def39
| def23 ),
inference(factoring,[status(thm)],[p775]) ).
cnf(c376,plain,
( leq(sk29,n3)
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p748,plain,
( leq(sk29,n3)
| def39
| def23 ),
inference(resolution,[status(thm)],[p746,c376]) ).
cnf(p778,plain,
( def39
| def23
| def39
| def23 ),
inference(resolution,[status(thm)],[p777,p748]) ).
cnf(p779,plain,
( def39
| def39
| def23 ),
inference(factoring,[status(thm)],[p778]) ).
cnf(p781,plain,
( def39
| def23 ),
inference(factoring,[status(thm)],[p779]) ).
cnf(c372,plain,
( def38
| def34
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p782,plain,
( def38
| def34
| def23 ),
inference(resolution,[status(thm)],[p781,c372]) ).
cnf(c370,plain,
( def37
| ~ def38 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p783,plain,
( def37
| def34
| def23 ),
inference(resolution,[status(thm)],[p782,c370]) ).
cnf(p799,plain,
( def34
| def23
| def36 ),
inference(resolution,[status(thm)],[c366,p783]) ).
cnf(c363,plain,
( leq(n0,sk28)
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p801,plain,
( leq(n0,sk28)
| def34
| def23 ),
inference(resolution,[status(thm)],[p799,c363]) ).
cnf(c367,plain,
( a_select3(simplex7_init,sk28,sk27) != init
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p633,plain,
( a_select3(simplex7_init,sk28,sk27) != s_best7_init
| ~ def37 ),
inference(demodulation,[status(thm)],[p624,c367]) ).
cnf(p785,plain,
( a_select3(simplex7_init,sk28,sk27) != s_best7_init
| def34
| def23 ),
inference(resolution,[status(thm)],[p783,p633]) ).
cnf(c285,plain,
( a_select3(simplex7_init,X1,X0) = init
| def9(X1)
| ~ def10(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p625,plain,
( a_select3(simplex7_init,X0,X1) = s_best7_init
| def9(X0)
| ~ def10(X0,X1) ),
inference(demodulation,[status(thm)],[p624,c285]) ).
cnf(c292,plain,
( def11(X0,X1)
| ~ def12(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,def55,def56,def57])],[f52_sk]) ).
cnf(p595,plain,
def11(X0,X1),
inference(resolution,[status(thm)],[p593,c292]) ).
cnf(c288,plain,
( def10(X1,X0)
| def8(X0)
| ~ def11(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,def55,def56,def57])],[f52_sk]) ).
cnf(p615,plain,
( def10(X1,X0)
| def8(X0) ),
inference(resolution,[status(thm)],[p595,c288]) ).
cnf(p664,plain,
( def8(X1)
| a_select3(simplex7_init,X0,X1) = s_best7_init
| def9(X0) ),
inference(resolution,[status(thm)],[p625,p615]) ).
cnf(p787,plain,
( def8(sk27)
| def9(sk28)
| def34
| def23 ),
inference(resolution,[status(thm)],[p785,p664]) ).
cnf(c282,plain,
( ~ leq(X1,n3)
| ~ leq(n0,X1)
| ~ def9(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,def55,def56,def57])],[f52_sk]) ).
cnf(p788,plain,
( ~ leq(sk28,n3)
| ~ leq(n0,sk28)
| def8(sk27)
| def34
| def23 ),
inference(resolution,[status(thm)],[p787,c282]) ).
cnf(p805,plain,
( ~ leq(sk28,n3)
| def8(sk27)
| def34
| def23
| def34
| def23 ),
inference(resolution,[status(thm)],[p801,p788]) ).
cnf(p817,plain,
( ~ leq(sk28,n3)
| def8(sk27)
| def34
| def34
| def23 ),
inference(factoring,[status(thm)],[p805]) ).
cnf(p819,plain,
( ~ leq(sk28,n3)
| def8(sk27)
| def34
| def23 ),
inference(factoring,[status(thm)],[p817]) ).
cnf(c364,plain,
( leq(sk28,n3)
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p800,plain,
( leq(sk28,n3)
| def34
| def23 ),
inference(resolution,[status(thm)],[p799,c364]) ).
cnf(p820,plain,
( def34
| def23
| def8(sk27)
| def34
| def23 ),
inference(resolution,[status(thm)],[p819,p800]) ).
cnf(p821,plain,
( def34
| def8(sk27)
| def34
| def23 ),
inference(factoring,[status(thm)],[p820]) ).
cnf(p823,plain,
( def8(sk27)
| def34
| def23 ),
inference(factoring,[status(thm)],[p821]) ).
cnf(c279,plain,
( ~ leq(X0,n2)
| ~ leq(n0,X0)
| ~ def8(X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p824,plain,
( ~ leq(sk27,n2)
| ~ leq(n0,sk27)
| def34
| def23 ),
inference(resolution,[status(thm)],[p823,c279]) ).
cnf(c369,plain,
( def35
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p784,plain,
( def35
| def34
| def23 ),
inference(resolution,[status(thm)],[p782,c369]) ).
cnf(c360,plain,
( leq(n0,sk27)
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p786,plain,
( leq(n0,sk27)
| def34
| def23 ),
inference(resolution,[status(thm)],[p784,c360]) ).
cnf(p829,plain,
( def34
| def23
| ~ leq(sk27,n2)
| def34
| def23 ),
inference(resolution,[status(thm)],[p824,p786]) ).
cnf(p850,plain,
( def34
| ~ leq(sk27,n2)
| def34
| def23 ),
inference(factoring,[status(thm)],[p829]) ).
cnf(p852,plain,
( ~ leq(sk27,n2)
| def34
| def23 ),
inference(factoring,[status(thm)],[p850]) ).
cnf(c361,plain,
( leq(sk27,n2)
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p798,plain,
( def34
| def23
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[c361,p784]) ).
cnf(p853,plain,
( def34
| def23
| def34
| def23 ),
inference(resolution,[status(thm)],[p852,p798]) ).
cnf(p854,plain,
( def34
| def34
| def23 ),
inference(factoring,[status(thm)],[p853]) ).
cnf(p856,plain,
( def34
| def23 ),
inference(factoring,[status(thm)],[p854]) ).
cnf(c357,plain,
( ~ leq(s_worst7,n3)
| def33
| ~ def34 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p857,plain,
( ~ leq(s_worst7,n3)
| def33
| def23 ),
inference(resolution,[status(thm)],[p856,c357]) ).
cnf(c277,plain,
( leq(s_worst7,n3)
| ~ def7 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p597,plain,
leq(s_worst7,n3),
inference(resolution,[status(thm)],[p596,c277]) ).
cnf(p860,plain,
( def33
| def23 ),
inference(resolution,[status(thm)],[p857,p597]) ).
cnf(c354,plain,
( ~ leq(s_sworst7,n3)
| def32
| ~ def33 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p861,plain,
( ~ leq(s_sworst7,n3)
| def32
| def23 ),
inference(resolution,[status(thm)],[p860,c354]) ).
cnf(c274,plain,
( leq(s_sworst7,n3)
| ~ def6 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p600,plain,
leq(s_sworst7,n3),
inference(resolution,[status(thm)],[p598,c274]) ).
cnf(p864,plain,
( def32
| def23 ),
inference(resolution,[status(thm)],[p861,p600]) ).
cnf(c351,plain,
( ~ leq(s_best7,n3)
| 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,def55,def56,def57])],[f52_sk]) ).
cnf(p865,plain,
( ~ leq(s_best7,n3)
| def31
| def23 ),
inference(resolution,[status(thm)],[p864,c351]) ).
cnf(c271,plain,
( leq(s_best7,n3)
| ~ def5 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p602,plain,
leq(s_best7,n3),
inference(resolution,[status(thm)],[p599,c271]) ).
cnf(p868,plain,
( def31
| def23 ),
inference(resolution,[status(thm)],[p865,p602]) ).
cnf(c348,plain,
( ~ leq(n0,s_worst7)
| 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,def55,def56,def57])],[f52_sk]) ).
cnf(p869,plain,
( ~ leq(n0,s_worst7)
| def30
| def23 ),
inference(resolution,[status(thm)],[p868,c348]) ).
cnf(c268,plain,
( leq(n0,s_worst7)
| ~ def4 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p604,plain,
leq(n0,s_worst7),
inference(resolution,[status(thm)],[p601,c268]) ).
cnf(p874,plain,
( def30
| def23 ),
inference(resolution,[status(thm)],[p869,p604]) ).
cnf(c345,plain,
( ~ leq(n0,s_sworst7)
| 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,def55,def56,def57])],[f52_sk]) ).
cnf(p875,plain,
( ~ leq(n0,s_sworst7)
| def29
| def23 ),
inference(resolution,[status(thm)],[p874,c345]) ).
cnf(c265,plain,
( leq(n0,s_sworst7)
| ~ def3 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,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,def55,def56,def57])],[f52_sk]) ).
cnf(p606,plain,
leq(n0,s_sworst7),
inference(resolution,[status(thm)],[p603,c265]) ).
cnf(p880,plain,
( def29
| def23 ),
inference(resolution,[status(thm)],[p875,p606]) ).
cnf(c342,plain,
( ~ leq(n0,s_best7)
| def28
| ~ def29 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p881,plain,
( ~ leq(n0,s_best7)
| def28
| def23 ),
inference(resolution,[status(thm)],[p880,c342]) ).
cnf(c262,plain,
( leq(n0,s_best7)
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p608,plain,
leq(n0,s_best7),
inference(resolution,[status(thm)],[p605,c262]) ).
cnf(p886,plain,
( def28
| def23 ),
inference(resolution,[status(thm)],[p881,p608]) ).
cnf(c339,plain,
( s_worst7_init != init
| def27
| ~ def28 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p610,plain,
( init != init
| def27
| ~ def28 ),
inference(demodulation,[status(thm)],[p609,c339]) ).
cnf(p645,plain,
( s_best7_init != s_best7_init
| def27
| ~ def28 ),
inference(demodulation,[status(thm)],[p624,p610]) ).
cnf(p649,plain,
( def27
| ~ def28 ),
inference(equality_resolution,[status(thm)],[p645]) ).
cnf(p887,plain,
( def27
| def23 ),
inference(resolution,[status(thm)],[p886,p649]) ).
cnf(c256,plain,
( s_sworst7_init = init
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p613,plain,
s_sworst7_init = init,
inference(resolution,[status(thm)],[p611,c256]) ).
cnf(c336,plain,
( s_sworst7_init != init
| def26
| ~ def27 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p614,plain,
( init != init
| def26
| ~ def27 ),
inference(demodulation,[status(thm)],[p613,c336]) ).
cnf(p647,plain,
( s_best7_init != s_best7_init
| def26
| ~ def27 ),
inference(demodulation,[status(thm)],[p624,p614]) ).
cnf(p650,plain,
( def26
| ~ def27 ),
inference(equality_resolution,[status(thm)],[p647]) ).
cnf(p888,plain,
( def26
| def23 ),
inference(resolution,[status(thm)],[p887,p650]) ).
cnf(c333,plain,
( s_best7_init != init
| init != init
| ~ def26 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p494,plain,
( s_best7_init != init
| ~ def26 ),
inference(equality_resolution,[status(thm)],[c333]) ).
cnf(p643,plain,
( s_best7_init != s_best7_init
| ~ def26 ),
inference(demodulation,[status(thm)],[p624,p494]) ).
cnf(p648,plain,
~ def26,
inference(equality_resolution,[status(thm)],[p643]) ).
cnf(p889,plain,
def23,
inference(resolution,[status(thm)],[p888,p648]) ).
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,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p890,plain,
def22,
inference(resolution,[status(thm)],[p889,c324]) ).
cnf(c322,plain,
( pvar1401_init = init
| ~ 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,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p629,plain,
( pvar1401_init = s_best7_init
| ~ def22 ),
inference(demodulation,[status(thm)],[p624,c322]) ).
cnf(p896,plain,
pvar1401_init = s_best7_init,
inference(resolution,[status(thm)],[p890,p629]) ).
cnf(c321,plain,
( pvar1400_init = init
| ~ 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,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p628,plain,
( pvar1400_init = s_best7_init
| ~ def22 ),
inference(demodulation,[status(thm)],[p624,c321]) ).
cnf(p894,plain,
pvar1400_init = s_best7_init,
inference(resolution,[status(thm)],[p890,p628]) ).
cnf(c402,plain,
( pvar1401_init != init
| pvar1400_init != init
| ~ 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,def55,def56,def57])],[f52_sk]) ).
cnf(p641,plain,
( pvar1401_init != s_best7_init
| pvar1400_init != s_best7_init
| ~ def49 ),
inference(demodulation,[status(thm)],[p624,c402]) ).
cnf(p895,plain,
( pvar1401_init != s_best7_init
| s_best7_init != s_best7_init
| ~ def49 ),
inference(demodulation,[status(thm)],[p894,p641]) ).
cnf(p897,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_best7_init
| ~ def49 ),
inference(demodulation,[status(thm)],[p896,p895]) ).
cnf(p900,plain,
( s_best7_init != s_best7_init
| ~ def49 ),
inference(factoring,[status(thm)],[p897]) ).
cnf(p901,plain,
~ def49,
inference(equality_resolution,[status(thm)],[p900]) ).
cnf(c325,plain,
( pvar1402_init = init
| ~ 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,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p631,plain,
( pvar1402_init = s_best7_init
| ~ def23 ),
inference(demodulation,[status(thm)],[p624,c325]) ).
cnf(p891,plain,
pvar1402_init = s_best7_init,
inference(resolution,[status(thm)],[p889,p631]) ).
cnf(c409,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,def55,def56,def57])],[f52_sk]) ).
cnf(p505,plain,
( def50
| def48 ),
inference(resolution,[status(thm)],[p504,c409]) ).
cnf(c405,plain,
( pvar1402_init != init
| def49
| ~ def50 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57])],[f52_sk]) ).
cnf(p507,plain,
( pvar1402_init != init
| def49
| def48 ),
inference(resolution,[status(thm)],[p505,c405]) ).
cnf(p620,plain,
( pvar1402_init != s_best7_init
| def49
| def48 ),
inference(superposition,[status(thm)],[p612,p507]) ).
cnf(p892,plain,
( s_best7_init != s_best7_init
| def49
| def48 ),
inference(demodulation,[status(thm)],[p891,p620]) ).
cnf(p898,plain,
( def49
| def48 ),
inference(equality_resolution,[status(thm)],[p892]) ).
cnf(p902,plain,
def48,
inference(resolution,[status(thm)],[p901,p898]) ).
cnf(p903,plain,
( def47
| def45 ),
inference(resolution,[status(thm)],[p902,c399]) ).
cnf(p639,plain,
( a_select2(s_try7_init,sk31) != s_best7_init
| ~ def47 ),
inference(demodulation,[status(thm)],[p624,c397]) ).
cnf(p905,plain,
( a_select2(s_try7_init,sk31) != s_best7_init
| def45 ),
inference(resolution,[status(thm)],[p903,p639]) ).
cnf(p908,plain,
( def19(sk31)
| def45 ),
inference(resolution,[status(thm)],[p905,p654]) ).
cnf(p909,plain,
( ~ leq(sk31,minus(n3,n1))
| ~ leq(n0,sk31)
| def45 ),
inference(resolution,[status(thm)],[p908,c312]) ).
cnf(p904,plain,
( def46
| def45 ),
inference(resolution,[status(thm)],[p903,c396]) ).
cnf(p906,plain,
( leq(n0,sk31)
| def45 ),
inference(resolution,[status(thm)],[p904,c393]) ).
cnf(p914,plain,
( def45
| ~ leq(sk31,minus(n3,n1))
| def45 ),
inference(resolution,[status(thm)],[p909,p906]) ).
cnf(p915,plain,
( ~ leq(sk31,minus(n3,n1))
| def45 ),
inference(factoring,[status(thm)],[p914]) ).
cnf(p907,plain,
( leq(sk31,minus(n3,n1))
| def45 ),
inference(resolution,[status(thm)],[p904,c394]) ).
cnf(p916,plain,
( def45
| def45 ),
inference(resolution,[status(thm)],[p915,p907]) ).
cnf(p917,plain,
def45,
inference(factoring,[status(thm)],[p916]) ).
cnf(p918,plain,
( def44
| def42 ),
inference(resolution,[status(thm)],[p917,c390]) ).
cnf(p920,plain,
( a_select2(s_center7_init,sk30) != s_best7_init
| def42 ),
inference(resolution,[status(thm)],[p918,p637]) ).
cnf(p923,plain,
( def16(sk30)
| def42 ),
inference(resolution,[status(thm)],[p920,p621]) ).
cnf(p924,plain,
( ~ leq(sk30,n2)
| ~ leq(n0,sk30)
| def42 ),
inference(resolution,[status(thm)],[p923,c303]) ).
cnf(p919,plain,
( def43
| def42 ),
inference(resolution,[status(thm)],[p918,c387]) ).
cnf(p921,plain,
( leq(n0,sk30)
| def42 ),
inference(resolution,[status(thm)],[p919,c384]) ).
cnf(p929,plain,
( def42
| ~ leq(sk30,n2)
| def42 ),
inference(resolution,[status(thm)],[p924,p921]) ).
cnf(p930,plain,
( ~ leq(sk30,n2)
| def42 ),
inference(factoring,[status(thm)],[p929]) ).
cnf(p922,plain,
( leq(sk30,n2)
| def42 ),
inference(resolution,[status(thm)],[p919,c385]) ).
cnf(p932,plain,
( def42
| def42 ),
inference(resolution,[status(thm)],[p930,p922]) ).
cnf(p933,plain,
def42,
inference(factoring,[status(thm)],[p932]) ).
cnf(p934,plain,
( def41
| def39 ),
inference(resolution,[status(thm)],[p933,c381]) ).
cnf(p936,plain,
( a_select2(s_values7_init,sk29) != s_best7_init
| def39 ),
inference(resolution,[status(thm)],[p934,p635]) ).
cnf(p939,plain,
( def13(sk29)
| def39 ),
inference(resolution,[status(thm)],[p936,p653]) ).
cnf(p940,plain,
( ~ leq(sk29,n3)
| ~ leq(n0,sk29)
| def39 ),
inference(resolution,[status(thm)],[p939,c294]) ).
cnf(p935,plain,
( def40
| def39 ),
inference(resolution,[status(thm)],[p934,c378]) ).
cnf(p938,plain,
( leq(n0,sk29)
| def39 ),
inference(resolution,[status(thm)],[p935,c375]) ).
cnf(p945,plain,
( def39
| ~ leq(sk29,n3)
| def39 ),
inference(resolution,[status(thm)],[p940,p938]) ).
cnf(p946,plain,
( ~ leq(sk29,n3)
| def39 ),
inference(factoring,[status(thm)],[p945]) ).
cnf(p937,plain,
( leq(sk29,n3)
| def39 ),
inference(resolution,[status(thm)],[p935,c376]) ).
cnf(p948,plain,
( def39
| def39 ),
inference(resolution,[status(thm)],[p946,p937]) ).
cnf(p949,plain,
def39,
inference(factoring,[status(thm)],[p948]) ).
cnf(p950,plain,
( def38
| def34 ),
inference(resolution,[status(thm)],[p949,c372]) ).
cnf(p951,plain,
( def37
| def34 ),
inference(resolution,[status(thm)],[p950,c370]) ).
cnf(p953,plain,
( a_select3(simplex7_init,sk28,sk27) != s_best7_init
| def34 ),
inference(resolution,[status(thm)],[p951,p633]) ).
cnf(p959,plain,
( def8(sk27)
| def9(sk28)
| def34 ),
inference(resolution,[status(thm)],[p953,p664]) ).
cnf(p960,plain,
( ~ leq(sk28,n3)
| ~ leq(n0,sk28)
| def8(sk27)
| def34 ),
inference(resolution,[status(thm)],[p959,c282]) ).
cnf(p954,plain,
( def36
| def34 ),
inference(resolution,[status(thm)],[p951,c366]) ).
cnf(p958,plain,
( leq(n0,sk28)
| def34 ),
inference(resolution,[status(thm)],[p954,c363]) ).
cnf(p966,plain,
( def34
| ~ leq(sk28,n3)
| def8(sk27)
| def34 ),
inference(resolution,[status(thm)],[p960,p958]) ).
cnf(p967,plain,
( ~ leq(sk28,n3)
| def8(sk27)
| def34 ),
inference(factoring,[status(thm)],[p966]) ).
cnf(p957,plain,
( leq(sk28,n3)
| def34 ),
inference(resolution,[status(thm)],[p954,c364]) ).
cnf(p969,plain,
( def34
| def8(sk27)
| def34 ),
inference(resolution,[status(thm)],[p967,p957]) ).
cnf(p970,plain,
( def8(sk27)
| def34 ),
inference(factoring,[status(thm)],[p969]) ).
cnf(p971,plain,
( ~ leq(sk27,n2)
| ~ leq(n0,sk27)
| def34 ),
inference(resolution,[status(thm)],[p970,c279]) ).
cnf(p952,plain,
( def35
| def34 ),
inference(resolution,[status(thm)],[p950,c369]) ).
cnf(p955,plain,
( leq(n0,sk27)
| def34 ),
inference(resolution,[status(thm)],[p952,c360]) ).
cnf(p976,plain,
( def34
| ~ leq(sk27,n2)
| def34 ),
inference(resolution,[status(thm)],[p971,p955]) ).
cnf(p977,plain,
( ~ leq(sk27,n2)
| def34 ),
inference(factoring,[status(thm)],[p976]) ).
cnf(p956,plain,
( leq(sk27,n2)
| def34 ),
inference(resolution,[status(thm)],[p952,c361]) ).
cnf(p979,plain,
( def34
| def34 ),
inference(resolution,[status(thm)],[p977,p956]) ).
cnf(p980,plain,
def34,
inference(factoring,[status(thm)],[p979]) ).
cnf(p981,plain,
( ~ leq(s_worst7,n3)
| def33 ),
inference(resolution,[status(thm)],[p980,c357]) ).
cnf(p984,plain,
def33,
inference(resolution,[status(thm)],[p981,p597]) ).
cnf(p985,plain,
( ~ leq(s_sworst7,n3)
| def32 ),
inference(resolution,[status(thm)],[p984,c354]) ).
cnf(p988,plain,
def32,
inference(resolution,[status(thm)],[p985,p600]) ).
cnf(p989,plain,
( ~ leq(s_best7,n3)
| def31 ),
inference(resolution,[status(thm)],[p988,c351]) ).
cnf(p992,plain,
def31,
inference(resolution,[status(thm)],[p989,p602]) ).
cnf(p993,plain,
( ~ leq(n0,s_worst7)
| def30 ),
inference(resolution,[status(thm)],[p992,c348]) ).
cnf(p998,plain,
def30,
inference(resolution,[status(thm)],[p993,p604]) ).
cnf(p999,plain,
( ~ leq(n0,s_sworst7)
| def29 ),
inference(resolution,[status(thm)],[p998,c345]) ).
cnf(p1004,plain,
def29,
inference(resolution,[status(thm)],[p999,p606]) ).
cnf(p1005,plain,
( ~ leq(n0,s_best7)
| def28 ),
inference(resolution,[status(thm)],[p1004,c342]) ).
cnf(p1010,plain,
def28,
inference(resolution,[status(thm)],[p1005,p608]) ).
cnf(p1011,plain,
def27,
inference(resolution,[status(thm)],[p1010,p649]) ).
cnf(p1012,plain,
def26,
inference(resolution,[status(thm)],[p1011,p650]) ).
cnf(p1013,plain,
$false,
inference(resolution,[status(thm)],[p1012,p648]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV038+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 18:24:24 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 25.56/4.17 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 25.56/4.17 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------