%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWX071+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n012.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:31:55 PM UTC 2026
% Result : Theorem 56.38s 15.80s
% Output : Proof 56.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 4
% Syntax : Number of formulae : 55 ( 12 unt; 0 def)
% Number of atoms : 309 ( 140 equ)
% Maximal formula atoms : 66 ( 5 avg)
% Number of connectives : 371 ( 117 ~; 134 |; 106 &)
% ( 1 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 34 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-19 aty)
% Number of functors : 26 ( 26 usr; 6 con; 0-3 aty)
% Number of variables : 401 ( 184 sgn 64 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f143,axiom,
! [Xa,Xi,Xx] :
( eval_succeeds(Xa,Xi,Xx)
=> ( interpretation_succeeds(Xi)
=> ! [Xy] :
( eval_succeeds(Xa,Xi,Xy)
=> Xx = Xy ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd36) ).
fof(f143_nnf,plain,
! [Xa,Xi,Xx] :
( ! [Xy] :
( Xx = Xy
| ~ eval_succeeds(Xa,Xi,Xy) )
| ~ interpretation_succeeds(Xi)
| ~ eval_succeeds(Xa,Xi,Xx) ),
inference(nnf_transformation,[status(thm)],[f143]) ).
fof(f143_sk,plain,
! [Xa,Xi,Xx,Xy] :
( Xx = Xy
| ~ eval_succeeds(Xa,Xi,Xy)
| ~ interpretation_succeeds(Xi)
| ~ eval_succeeds(Xa,Xi,Xx) ),
inference(skolemisation,[status(esa)],[f143_nnf]) ).
cnf(c1719,plain,
( X2 = X3
| ~ eval_succeeds(X0,X1,X3)
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f143_sk]) ).
fof(f149,conjecture,
! [Xa,Xh,Xx] :
( eval_succeeds(Xa,Xh,Xx)
=> ( interpretation_succeeds(Xh)
=> ! [Xi] :
( ( sub(Xi,Xh)
& literal_list_succeeds(Xi) )
=> ( ( Xx = qtd1
=> ? [Xj] :
( false_succeeds(Xa,Xi,Xj)
& sub(Xj,Xh) ) )
& ( Xx = qtd0
=> ? [Xj] :
( true_succeeds(Xa,Xi,Xj)
& sub(Xj,Xh) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd41) ).
fof(f149_neg,negated_conjecture,
~ ! [Xa,Xh,Xx] :
( eval_succeeds(Xa,Xh,Xx)
=> ( interpretation_succeeds(Xh)
=> ! [Xi] :
( ( sub(Xi,Xh)
& literal_list_succeeds(Xi) )
=> ( ( Xx = qtd1
=> ? [Xj] :
( false_succeeds(Xa,Xi,Xj)
& sub(Xj,Xh) ) )
& ( Xx = qtd0
=> ? [Xj] :
( true_succeeds(Xa,Xi,Xj)
& sub(Xj,Xh) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f149]) ).
fof(f149_nnf,plain,
? [Xa,Xh,Xx] :
( ? [Xi] :
( ( ( ! [Xj] :
( ~ false_succeeds(Xa,Xi,Xj)
| ~ sub(Xj,Xh) )
& Xx = qtd1 )
| ( ! [Xj] :
( ~ true_succeeds(Xa,Xi,Xj)
| ~ sub(Xj,Xh) )
& Xx = qtd0 ) )
& sub(Xi,Xh)
& literal_list_succeeds(Xi) )
& interpretation_succeeds(Xh)
& eval_succeeds(Xa,Xh,Xx) ),
inference(nnf_transformation,[status(thm)],[f149_neg]) ).
fof(f149_sk,plain,
! [Xj] :
( ( ( ( ~ false_succeeds(sk220,sk223,Xj)
| ~ sub(Xj,sk221) )
& sk222 = qtd1 )
| ( ( ~ true_succeeds(sk220,sk223,Xj)
| ~ sub(Xj,sk221) )
& sk222 = qtd0 ) )
& sub(sk223,sk221)
& literal_list_succeeds(sk223)
& interpretation_succeeds(sk221)
& eval_succeeds(sk220,sk221,sk222) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk220,sk221,sk222,sk223])],[f149_nnf]) ).
cnf(c2147,plain,
eval_succeeds(sk220,sk221,sk222),
inference(cnf_transformation,[status(esa)],[f149_sk]) ).
cnf(p22543,plain,
( sk222 = X0
| ~ eval_succeeds(sk220,sk221,X0)
| ~ interpretation_succeeds(sk221) ),
inference(resolution,[status(thm)],[c1719,c2147]) ).
cnf(c2148,plain,
interpretation_succeeds(sk221),
inference(cnf_transformation,[status(esa)],[f149_sk]) ).
cnf(p22708,plain,
( sk222 = X0
| ~ eval_succeeds(sk220,sk221,X0) ),
inference(resolution,[status(thm)],[p22543,c2148]) ).
fof(f73,axiom,
! [Xx1,Xx2,Xx3] :
( eval_succeeds(Xx1,Xx2,Xx3)
<=> ( ? [Xx19] :
( member_succeeds(p(Xx19),Xx2)
& Xx3 = qtd0
& Xx1 = p(Xx19) )
| ? [Xx18] :
( member_succeeds(neg(p(Xx18)),Xx2)
& Xx3 = qtd1
& Xx1 = p(Xx18) )
| ? [Xx17] :
( eval_succeeds(Xx17,Xx2,qtd1)
& Xx3 = qtd0
& Xx1 = neg(Xx17) )
| ? [Xx16] :
( eval_succeeds(Xx16,Xx2,qtd0)
& Xx3 = qtd1
& Xx1 = neg(Xx16) )
| ? [Xx14,Xx15] :
( eval_succeeds(Xx15,Xx2,qtd0)
& eval_succeeds(Xx14,Xx2,qtd0)
& Xx3 = qtd0
& Xx1 = and(Xx14,Xx15) )
| ? [Xx12,Xx13] :
( eval_succeeds(Xx12,Xx2,qtd1)
& Xx3 = qtd1
& Xx1 = and(Xx12,Xx13) )
| ? [Xx10,Xx11] :
( eval_succeeds(Xx11,Xx2,qtd1)
& Xx3 = qtd1
& Xx1 = and(Xx10,Xx11) )
| ? [Xx8,Xx9] :
( eval_succeeds(Xx8,Xx2,qtd0)
& Xx3 = qtd0
& Xx1 = or(Xx8,Xx9) )
| ? [Xx6,Xx7] :
( eval_succeeds(Xx7,Xx2,qtd0)
& Xx3 = qtd0
& Xx1 = or(Xx6,Xx7) )
| ? [Xx4,Xx5] :
( eval_succeeds(Xx5,Xx2,qtd1)
& eval_succeeds(Xx4,Xx2,qtd1)
& Xx3 = qtd1
& Xx1 = or(Xx4,Xx5) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id74) ).
fof(f73_nnf,plain,
! [Xx1,Xx2,Xx3] :
( ( ( ! [Xx19] :
( ~ member_succeeds(p(Xx19),Xx2)
| Xx3 != qtd0
| Xx1 != p(Xx19) )
& ! [Xx18] :
( ~ member_succeeds(neg(p(Xx18)),Xx2)
| Xx3 != qtd1
| Xx1 != p(Xx18) )
& ! [Xx17] :
( ~ eval_succeeds(Xx17,Xx2,qtd1)
| Xx3 != qtd0
| Xx1 != neg(Xx17) )
& ! [Xx16] :
( ~ eval_succeeds(Xx16,Xx2,qtd0)
| Xx3 != qtd1
| Xx1 != neg(Xx16) )
& ! [Xx14,Xx15] :
( ~ eval_succeeds(Xx15,Xx2,qtd0)
| ~ eval_succeeds(Xx14,Xx2,qtd0)
| Xx3 != qtd0
| Xx1 != and(Xx14,Xx15) )
& ! [Xx12,Xx13] :
( ~ eval_succeeds(Xx12,Xx2,qtd1)
| Xx3 != qtd1
| Xx1 != and(Xx12,Xx13) )
& ! [Xx10,Xx11] :
( ~ eval_succeeds(Xx11,Xx2,qtd1)
| Xx3 != qtd1
| Xx1 != and(Xx10,Xx11) )
& ! [Xx8,Xx9] :
( ~ eval_succeeds(Xx8,Xx2,qtd0)
| Xx3 != qtd0
| Xx1 != or(Xx8,Xx9) )
& ! [Xx6,Xx7] :
( ~ eval_succeeds(Xx7,Xx2,qtd0)
| Xx3 != qtd0
| Xx1 != or(Xx6,Xx7) )
& ! [Xx4,Xx5] :
( ~ eval_succeeds(Xx5,Xx2,qtd1)
| ~ eval_succeeds(Xx4,Xx2,qtd1)
| Xx3 != qtd1
| Xx1 != or(Xx4,Xx5) ) )
| eval_succeeds(Xx1,Xx2,Xx3) )
& ( ? [Xx19] :
( member_succeeds(p(Xx19),Xx2)
& Xx3 = qtd0
& Xx1 = p(Xx19) )
| ? [Xx18] :
( member_succeeds(neg(p(Xx18)),Xx2)
& Xx3 = qtd1
& Xx1 = p(Xx18) )
| ? [Xx17] :
( eval_succeeds(Xx17,Xx2,qtd1)
& Xx3 = qtd0
& Xx1 = neg(Xx17) )
| ? [Xx16] :
( eval_succeeds(Xx16,Xx2,qtd0)
& Xx3 = qtd1
& Xx1 = neg(Xx16) )
| ? [Xx14,Xx15] :
( eval_succeeds(Xx15,Xx2,qtd0)
& eval_succeeds(Xx14,Xx2,qtd0)
& Xx3 = qtd0
& Xx1 = and(Xx14,Xx15) )
| ? [Xx12,Xx13] :
( eval_succeeds(Xx12,Xx2,qtd1)
& Xx3 = qtd1
& Xx1 = and(Xx12,Xx13) )
| ? [Xx10,Xx11] :
( eval_succeeds(Xx11,Xx2,qtd1)
& Xx3 = qtd1
& Xx1 = and(Xx10,Xx11) )
| ? [Xx8,Xx9] :
( eval_succeeds(Xx8,Xx2,qtd0)
& Xx3 = qtd0
& Xx1 = or(Xx8,Xx9) )
| ? [Xx6,Xx7] :
( eval_succeeds(Xx7,Xx2,qtd0)
& Xx3 = qtd0
& Xx1 = or(Xx6,Xx7) )
| ? [Xx4,Xx5] :
( eval_succeeds(Xx5,Xx2,qtd1)
& eval_succeeds(Xx4,Xx2,qtd1)
& Xx3 = qtd1
& Xx1 = or(Xx4,Xx5) )
| ~ eval_succeeds(Xx1,Xx2,Xx3) ) ),
inference(nnf_transformation,[status(thm)],[f73]) ).
fof(f73_sk,plain,
! [Xx1,Xx2,Xx3,Xx4,Xx5,Xx6,Xx7,Xx8,Xx9,Xx10,Xx11,Xx12,Xx13,Xx14,Xx15,Xx16,Xx17,Xx18,Xx19] :
( ( ( ( ~ member_succeeds(p(Xx19),Xx2)
| Xx3 != qtd0
| Xx1 != p(Xx19) )
& ( ~ member_succeeds(neg(p(Xx18)),Xx2)
| Xx3 != qtd1
| Xx1 != p(Xx18) )
& ( ~ eval_succeeds(Xx17,Xx2,qtd1)
| Xx3 != qtd0
| Xx1 != neg(Xx17) )
& ( ~ eval_succeeds(Xx16,Xx2,qtd0)
| Xx3 != qtd1
| Xx1 != neg(Xx16) )
& ( ~ eval_succeeds(Xx15,Xx2,qtd0)
| ~ eval_succeeds(Xx14,Xx2,qtd0)
| Xx3 != qtd0
| Xx1 != and(Xx14,Xx15) )
& ( ~ eval_succeeds(Xx12,Xx2,qtd1)
| Xx3 != qtd1
| Xx1 != and(Xx12,Xx13) )
& ( ~ eval_succeeds(Xx11,Xx2,qtd1)
| Xx3 != qtd1
| Xx1 != and(Xx10,Xx11) )
& ( ~ eval_succeeds(Xx8,Xx2,qtd0)
| Xx3 != qtd0
| Xx1 != or(Xx8,Xx9) )
& ( ~ eval_succeeds(Xx7,Xx2,qtd0)
| Xx3 != qtd0
| Xx1 != or(Xx6,Xx7) )
& ( ~ eval_succeeds(Xx5,Xx2,qtd1)
| ~ eval_succeeds(Xx4,Xx2,qtd1)
| Xx3 != qtd1
| Xx1 != or(Xx4,Xx5) ) )
| eval_succeeds(Xx1,Xx2,Xx3) )
& ( ( member_succeeds(p(sk36(Xx1,Xx2,Xx3)),Xx2)
& Xx3 = qtd0
& Xx1 = p(sk36(Xx1,Xx2,Xx3)) )
| ( member_succeeds(neg(p(sk35(Xx1,Xx2,Xx3))),Xx2)
& Xx3 = qtd1
& Xx1 = p(sk35(Xx1,Xx2,Xx3)) )
| ( eval_succeeds(sk34(Xx1,Xx2,Xx3),Xx2,qtd1)
& Xx3 = qtd0
& Xx1 = neg(sk34(Xx1,Xx2,Xx3)) )
| ( eval_succeeds(sk33(Xx1,Xx2,Xx3),Xx2,qtd0)
& Xx3 = qtd1
& Xx1 = neg(sk33(Xx1,Xx2,Xx3)) )
| ( eval_succeeds(sk32(Xx1,Xx2,Xx3),Xx2,qtd0)
& eval_succeeds(sk31(Xx1,Xx2,Xx3),Xx2,qtd0)
& Xx3 = qtd0
& Xx1 = and(sk31(Xx1,Xx2,Xx3),sk32(Xx1,Xx2,Xx3)) )
| ( eval_succeeds(sk29(Xx1,Xx2,Xx3),Xx2,qtd1)
& Xx3 = qtd1
& Xx1 = and(sk29(Xx1,Xx2,Xx3),sk30(Xx1,Xx2,Xx3)) )
| ( eval_succeeds(sk28(Xx1,Xx2,Xx3),Xx2,qtd1)
& Xx3 = qtd1
& Xx1 = and(sk27(Xx1,Xx2,Xx3),sk28(Xx1,Xx2,Xx3)) )
| ( eval_succeeds(sk25(Xx1,Xx2,Xx3),Xx2,qtd0)
& Xx3 = qtd0
& Xx1 = or(sk25(Xx1,Xx2,Xx3),sk26(Xx1,Xx2,Xx3)) )
| ( eval_succeeds(sk24(Xx1,Xx2,Xx3),Xx2,qtd0)
& Xx3 = qtd0
& Xx1 = or(sk23(Xx1,Xx2,Xx3),sk24(Xx1,Xx2,Xx3)) )
| ( eval_succeeds(sk22(Xx1,Xx2,Xx3),Xx2,qtd1)
& eval_succeeds(sk21(Xx1,Xx2,Xx3),Xx2,qtd1)
& Xx3 = qtd1
& Xx1 = or(sk21(Xx1,Xx2,Xx3),sk22(Xx1,Xx2,Xx3)) )
| ~ eval_succeeds(Xx1,Xx2,Xx3) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk21,sk22,sk23,sk24,sk25,sk26,sk27,sk28,sk29,sk30,sk31,sk32,sk33,sk34,sk35,sk36])],[f73_nnf]) ).
cnf(c506,plain,
( def63(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| ~ eval_succeeds(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,def58,def59,def60,def61,def62,def63,def64])],[f73_sk]) ).
cnf(p16010,plain,
def63(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18),
inference(resolution,[status(thm)],[c506,c2147]) ).
cnf(c505,plain,
( def62(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| eval_succeeds(X0,X1,X2)
| ~ def63(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,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,def58,def59,def60,def61,def62,def63,def64])],[f73_sk]) ).
cnf(p16011,plain,
( def62(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| eval_succeeds(X0,X1,X2) ),
inference(resolution,[status(thm)],[p16010,c505]) ).
cnf(c502,plain,
( def59(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ def62(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,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,def58,def59,def60,def61,def62,def63,def64])],[f73_sk]) ).
cnf(p16013,plain,
( def59(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| eval_succeeds(X0,X1,X2) ),
inference(resolution,[status(thm)],[p16011,c502]) ).
cnf(c493,plain,
( def56(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ def59(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,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,def58,def59,def60,def61,def62,def63,def64])],[f73_sk]) ).
cnf(p16018,plain,
( def56(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| eval_succeeds(X0,X1,X2) ),
inference(resolution,[status(thm)],[p16013,c493]) ).
cnf(c485,plain,
( def55(X0,X16,X2,X1)
| ~ def56(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,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,def58,def59,def60,def61,def62,def63,def64])],[f73_sk]) ).
cnf(p16026,plain,
( def55(X3,X4,X5,X6)
| eval_succeeds(X0,X1,X2) ),
inference(resolution,[status(thm)],[p16018,c485]) ).
cnf(c481,plain,
( ~ eval_succeeds(X16,X1,qtd1)
| def54(X0,X16,X2)
| ~ def55(X0,X16,X2,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,def58,def59,def60,def61,def62,def63,def64])],[f73_sk]) ).
cnf(p16030,plain,
( ~ eval_succeeds(X4,X6,qtd1)
| def54(X3,X4,X5)
| eval_succeeds(X0,X1,X2) ),
inference(resolution,[status(thm)],[p16026,c481]) ).
cnf(c2151,plain,
( sk222 = qtd1
| sk222 = qtd0 ),
inference(cnf_transformation,[status(esa)],[f149_sk]) ).
cnf(p1398,plain,
( eval_succeeds(sk220,sk221,qtd1)
| sk222 = qtd0 ),
inference(superposition,[status(thm)],[c2151,c2147]) ).
cnf(p16032,plain,
( sk222 = qtd0
| def54(X3,sk220,X4)
| eval_succeeds(X0,X1,X2) ),
inference(resolution,[status(thm)],[p16030,p1398]) ).
cnf(c478,plain,
( X2 != qtd0
| X0 != neg(X16)
| ~ def54(X0,X16,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,def58,def59,def60,def61,def62,def63,def64])],[f73_sk]) ).
cnf(p16034,plain,
( X4 != qtd0
| X3 != neg(sk220)
| sk222 = qtd0
| eval_succeeds(X0,X1,X2) ),
inference(resolution,[status(thm)],[p16032,c478]) ).
cnf(p16035,plain,
( X3 != qtd0
| sk222 = qtd0
| eval_succeeds(X0,X1,X2) ),
inference(equality_resolution,[status(thm)],[p16034]) ).
cnf(p16039,plain,
( sk222 = qtd0
| eval_succeeds(X0,X1,X2) ),
inference(equality_resolution,[status(thm)],[p16035]) ).
cnf(p22712,plain,
( sk222 = qtd0
| sk222 = X0 ),
inference(resolution,[status(thm)],[p22708,p16039]) ).
cnf(p22726,plain,
sk222 = qtd0,
inference(factoring,[status(thm)],[p22712]) ).
cnf(p22727,plain,
eval_succeeds(sk220,sk221,qtd0),
inference(demodulation,[status(thm)],[p22726,c2147]) ).
cnf(c484,plain,
( def53(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ def56(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,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,def58,def59,def60,def61,def62,def63,def64])],[f73_sk]) ).
cnf(p16025,plain,
( def53(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| eval_succeeds(X0,X1,X2) ),
inference(resolution,[status(thm)],[p16018,c484]) ).
cnf(c476,plain,
( def52(X0,X15,X2,X1)
| ~ def53(X0,X3,X4,X2,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,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,def58,def59,def60,def61,def62,def63,def64])],[f73_sk]) ).
cnf(p16043,plain,
( def52(X3,X4,X5,X6)
| eval_succeeds(X0,X1,X2) ),
inference(resolution,[status(thm)],[p16025,c476]) ).
cnf(c472,plain,
( ~ eval_succeeds(X15,X1,qtd0)
| def51(X0,X15,X2)
| ~ def52(X0,X15,X2,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,def58,def59,def60,def61,def62,def63,def64])],[f73_sk]) ).
cnf(p16047,plain,
( ~ eval_succeeds(X4,X6,qtd0)
| def51(X3,X4,X5)
| eval_succeeds(X0,X1,X2) ),
inference(resolution,[status(thm)],[p16043,c472]) ).
cnf(p22891,plain,
( def51(X3,sk220,X4)
| eval_succeeds(X0,X1,X2) ),
inference(resolution,[status(thm)],[p22727,p16047]) ).
cnf(p22874,plain,
( qtd0 = X0
| ~ eval_succeeds(sk220,sk221,X0) ),
inference(demodulation,[status(thm)],[p22726,p22708]) ).
cnf(p23131,plain,
( qtd0 = X2
| def51(X0,sk220,X1) ),
inference(resolution,[status(thm)],[p22891,p22874]) ).
fof(f15,axiom,
qtd0 != qtd1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id16) ).
fof(f15_nnf,plain,
qtd0 != qtd1,
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
qtd0 != qtd1,
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
qtd0 != qtd1,
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p23134,plain,
def51(X0,sk220,X1),
inference(resolution,[status(thm)],[p23131,c15]) ).
cnf(c469,plain,
( X2 != qtd1
| X0 != neg(X15)
| ~ def51(X0,X15,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,def58,def59,def60,def61,def62,def63,def64])],[f73_sk]) ).
cnf(p23135,plain,
( X1 != qtd1
| X0 != neg(sk220) ),
inference(resolution,[status(thm)],[p23134,c469]) ).
cnf(p23136,plain,
X0 != qtd1,
inference(equality_resolution,[status(thm)],[p23135]) ).
cnf(p23138,plain,
$false,
inference(equality_resolution,[status(thm)],[p23136]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX071+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/5.35 % Computer : n012.cluster.edu
% 0.07/5.35 % Model : x86_64 x86_64
% 0.07/5.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/5.35 % Memory : 8046.5625MB
% 0.07/5.35 % OS : Linux 6.8.0-71-generic
% 0.07/5.35 % CPULimit : 300
% 0.07/5.35 % WCLimit : 300
% 0.07/5.35 % DateTime : Thu Sep 24 23:23:56 UTC 2026
% 0.07/5.35 % CPUTime :
% 0.07/5.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 56.38/15.80 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.38/15.80 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------