%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM736+4 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 : Thu Sep 24 01:41:33 PM UTC 2026
% Result : Theorem 240.27s 30.83s
% Output : CNFRefutation 240.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 9
% Syntax : Number of formulae : 52 ( 11 unt; 0 def)
% Number of atoms : 154 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 167 ( 65 ~; 59 |; 27 &)
% ( 9 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 11 con; 0-2 aty)
% Number of variables : 101 ( 98 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f31,axiom,
! [X,Xa] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,X),Xa))
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,Xa))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,Xa)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [X,Xa] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,X),Xa))
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,Xa))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,Xa)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [X,Xa] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,X),Xa))
<=> pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(Xa),X))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [X,Xa] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,X),Xa))
<=> pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(X),Xa))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,axiom,
! [X,Xa] :
( pp(aa_fun171081125l_bool(scratc1668550563all_of(X),Xa))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc1458855606_is_of(X2,X)
=> pp(aa_TPTP_ind_bool(Xa,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f398,axiom,
! [X0] :
( ! [X13] :
( gg_TPTP_ind(X13)
=> ( ! [X22] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc695511610bnd_in,X22),X13))
=> pp(aa_TPTP_ind_bool(X0,X22)) )
=> pp(aa_TPTP_ind_bool(X0,X13)) ) )
=> ! [X14] : pp(aa_TPTP_ind_bool(X0,X14)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f539,axiom,
! [Uu] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,Uu))
<=> pp(aa_fun171081125l_bool(scratc1668550563all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,Uu))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f581,axiom,
! [Uu,Uua] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,Uu),Uua))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,Uu),Uua))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,Uua),Uu)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f841,conjecture,
pp(aa_fun171081125l_bool(scratc1668550563all_of(aTP_Lamm_a),aTP_Lamm_ab)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f842,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1668550563all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(negated_conjecture,[status(cth)],[f841]) ).
fof(f873,plain,
! [X,Xa] :
( ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,Xa))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,Xa)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X))))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,X),Xa)) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,Xa))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,Xa)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,X),Xa)) ) ),
inference(NNF_transformation,[status(thm)],[f31]) ).
fof(f874,plain,
( ! [X,Xa] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,Xa))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,Xa)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X))))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,X),Xa)) )
& ! [X,Xa] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,Xa))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,Xa)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,X),Xa)) ) ),
inference(miniscoping,[status(thm)],[f873]) ).
fof(f876,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X0)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X1))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X1)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X0)))) ),
inference(cnf_transformation,[status(thm)],[f874]) ).
fof(f877,plain,
! [X,Xa] :
( ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,Xa))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,Xa)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X))))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,X),Xa)) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,Xa))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,Xa)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,X),Xa)) ) ),
inference(NNF_transformation,[status(thm)],[f32]) ).
fof(f878,plain,
( ! [X,Xa] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,Xa))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,Xa)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X))))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,X),Xa)) )
& ! [X,Xa] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,Xa))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,Xa)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,X),Xa)) ) ),
inference(miniscoping,[status(thm)],[f877]) ).
fof(f879,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X0)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X1))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X1)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X0)))) ),
inference(cnf_transformation,[status(thm)],[f878]) ).
fof(f964,plain,
! [X,Xa] :
( ( ~ pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(Xa),X)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,X),Xa)) )
& ( pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(Xa),X)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,X),Xa)) ) ),
inference(NNF_transformation,[status(thm)],[f77]) ).
fof(f965,plain,
( ! [X,Xa] :
( ~ pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(Xa),X)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,X),Xa)) )
& ! [X,Xa] :
( pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(Xa),X)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,X),Xa)) ) ),
inference(miniscoping,[status(thm)],[f964]) ).
fof(f967,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,X1),X0))
| ~ pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(X0),X1))) ),
inference(cnf_transformation,[status(thm)],[f965]) ).
fof(f968,plain,
! [X,Xa] :
( ( ~ pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(X),Xa)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,X),Xa)) )
& ( pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(X),Xa)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,X),Xa)) ) ),
inference(NNF_transformation,[status(thm)],[f78]) ).
fof(f969,plain,
( ! [X,Xa] :
( ~ pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(X),Xa)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,X),Xa)) )
& ! [X,Xa] :
( pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(X),Xa)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,X),Xa)) ) ),
inference(miniscoping,[status(thm)],[f968]) ).
fof(f970,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1523036013n_some,aa_TPT43085870d_bool(scratc1590329917ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f969]) ).
fof(f1288,plain,
! [X,Xa] :
( pp(aa_fun171081125l_bool(scratc1668550563all_of(X),Xa))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(Xa,X2))
| ~ scratc1458855606_is_of(X2,X)
| ~ gg_TPTP_ind(X2) ) ),
inference(pre_NNF_transformation,[status(thm)],[f196]) ).
fof(f1289,plain,
! [X,Xa] :
( ( ? [X2] :
( ~ pp(aa_TPTP_ind_bool(Xa,X2))
& scratc1458855606_is_of(X2,X)
& gg_TPTP_ind(X2) )
| pp(aa_fun171081125l_bool(scratc1668550563all_of(X),Xa)) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(Xa,X2))
| ~ scratc1458855606_is_of(X2,X)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1668550563all_of(X),Xa)) ) ),
inference(NNF_transformation,[status(thm)],[f1288]) ).
fof(f1290,plain,
( ! [X,Xa] :
( ? [X2] :
( ~ pp(aa_TPTP_ind_bool(Xa,X2))
& scratc1458855606_is_of(X2,X)
& gg_TPTP_ind(X2) )
| pp(aa_fun171081125l_bool(scratc1668550563all_of(X),Xa)) )
& ! [X,Xa] :
( ! [X2] :
( pp(aa_TPTP_ind_bool(Xa,X2))
| ~ scratc1458855606_is_of(X2,X)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1668550563all_of(X),Xa)) ) ),
inference(miniscoping,[status(thm)],[f1289]) ).
fof(f1291,plain,
( ! [X,Xa] :
( ( ~ pp(aa_TPTP_ind_bool(Xa,sK12_skl(Xa,X)))
& scratc1458855606_is_of(sK12_skl(Xa,X),X)
& gg_TPTP_ind(sK12_skl(Xa,X)) )
| pp(aa_fun171081125l_bool(scratc1668550563all_of(X),Xa)) )
& ! [X,Xa] :
( ! [X2] :
( pp(aa_TPTP_ind_bool(Xa,X2))
| ~ scratc1458855606_is_of(X2,X)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1668550563all_of(X),Xa)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(X2,sK12_skl(Xa,X))],[f1290]) ).
fof(f1295,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1668550563all_of(X1),X0))
| ~ pp(aa_TPTP_ind_bool(X0,sK12_skl(X0,X1))) ),
inference(cnf_transformation,[status(thm)],[f1291]) ).
fof(f1591,plain,
! [X0] :
( ! [X14] : pp(aa_TPTP_ind_bool(X0,X14))
| ? [X13] :
( ~ pp(aa_TPTP_ind_bool(X0,X13))
& ! [X22] :
( pp(aa_TPTP_ind_bool(X0,X22))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc695511610bnd_in,X22),X13)) )
& gg_TPTP_ind(X13) ) ),
inference(pre_NNF_transformation,[status(thm)],[f398]) ).
fof(f1592,plain,
! [X0] :
( ! [X14] : pp(aa_TPTP_ind_bool(X0,X14))
| ( ~ pp(aa_TPTP_ind_bool(X0,sK20_skl(X0)))
& ! [X22] :
( pp(aa_TPTP_ind_bool(X0,X22))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc695511610bnd_in,X22),sK20_skl(X0))) )
& gg_TPTP_ind(sK20_skl(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(X13,sK20_skl(X0))],[f1591]) ).
fof(f1595,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(X0,sK20_skl(X0)))
| pp(aa_TPTP_ind_bool(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f1592]) ).
fof(f2161,plain,
! [Uu] :
( ( ~ pp(aa_fun171081125l_bool(scratc1668550563all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,Uu)))
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,Uu)) )
& ( pp(aa_fun171081125l_bool(scratc1668550563all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,Uu)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,Uu)) ) ),
inference(NNF_transformation,[status(thm)],[f539]) ).
fof(f2162,plain,
( ! [Uu] :
( ~ pp(aa_fun171081125l_bool(scratc1668550563all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,Uu)))
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,Uu)) )
& ! [Uu] :
( pp(aa_fun171081125l_bool(scratc1668550563all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,Uu)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,Uu)) ) ),
inference(miniscoping,[status(thm)],[f2161]) ).
fof(f2164,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ pp(aa_fun171081125l_bool(scratc1668550563all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) ),
inference(cnf_transformation,[status(thm)],[f2162]) ).
fof(f2356,plain,
! [Uu,Uua] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,Uu),Uua))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,Uua),Uu))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,Uu),Uua)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f581]) ).
fof(f2357,plain,
! [Uu,Uua] :
( ( ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,Uua),Uu))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,Uu),Uua)) )
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,Uu),Uua)) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,Uua),Uu))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,Uu),Uua))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,Uu),Uua)) ) ),
inference(NNF_transformation,[status(thm)],[f2356]) ).
fof(f2358,plain,
( ! [Uu,Uua] :
( ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,Uua),Uu))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,Uu),Uua)) )
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,Uu),Uua)) )
& ! [Uu,Uua] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,Uua),Uu))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,Uu),Uua))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,Uu),Uua)) ) ),
inference(miniscoping,[status(thm)],[f2357]) ).
fof(f2360,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f2358]) ).
fof(f2361,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,X1),X0))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f2358]) ).
fof(f3526,plain,
~ pp(aa_fun171081125l_bool(scratc1668550563all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(cnf_transformation,[status(thm)],[f842]) ).
fof(f3742,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,X0),X1)) ),
inference(resolution,[status(thm)],[f970,f967]) ).
fof(f4258,plain,
! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),sK12_skl(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),aTP_Lamm_a)))
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(resolution,[status(thm)],[f1295,f2164]) ).
fof(f4259,plain,
~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12_skl(aTP_Lamm_ab,aTP_Lamm_a))),
inference(resolution,[status(thm)],[f1295,f3526]) ).
fof(f6734,plain,
~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK20_skl(aTP_Lamm_ab))),
inference(resolution,[status(thm)],[f1595,f4259]) ).
fof(f6753,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),sK20_skl(aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))) ),
inference(resolution,[status(thm)],[f1595,f4258]) ).
fof(f13034,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc550632248_lessf,sK20_skl(aa_TPT43085870d_bool(aTP_Lamm_aa,X0))),X0)) ),
inference(resolution,[status(thm)],[f2361,f6753]) ).
fof(f13066,plain,
! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,sK20_skl(aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,X0))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,X0)),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,sK20_skl(aa_TPT43085870d_bool(aTP_Lamm_aa,X0))))))
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(resolution,[status(thm)],[f13034,f876]) ).
fof(f13278,plain,
~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1575674740nd_iii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,sK20_skl(aa_TPT43085870d_bool(aTP_Lamm_aa,sK20_skl(aTP_Lamm_ab))))),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,sK20_skl(aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,sK20_skl(aTP_Lamm_ab))),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,sK20_skl(aa_TPT43085870d_bool(aTP_Lamm_aa,sK20_skl(aTP_Lamm_ab))))))),
inference(resolution,[status(thm)],[f13066,f6734]) ).
fof(f14467,plain,
~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc125826166_29_ii,aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,sK20_skl(aTP_Lamm_ab))),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,sK20_skl(aa_TPT43085870d_bool(aTP_Lamm_aa,sK20_skl(aTP_Lamm_ab)))))),aa_TPTP_ind_TPTP_ind(scratc128556792d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1617769457nd_num,sK20_skl(aa_TPT43085870d_bool(aTP_Lamm_aa,sK20_skl(aTP_Lamm_ab))))),aa_TPTP_ind_TPTP_ind(scratc1534104824nd_den,sK20_skl(aTP_Lamm_ab))))),
inference(resolution,[status(thm)],[f3742,f13278]) ).
fof(f14988,plain,
~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc896954044_moref,sK20_skl(aTP_Lamm_ab)),sK20_skl(aa_TPT43085870d_bool(aTP_Lamm_aa,sK20_skl(aTP_Lamm_ab))))),
inference(resolution,[status(thm)],[f14467,f879]) ).
fof(f15023,plain,
pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,sK20_skl(aTP_Lamm_ab)),sK20_skl(aa_TPT43085870d_bool(aTP_Lamm_aa,sK20_skl(aTP_Lamm_ab))))),
inference(resolution,[status(thm)],[f14988,f2360]) ).
fof(f15080,plain,
pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK20_skl(aTP_Lamm_ab))),
inference(resolution,[status(thm)],[f15023,f6753]) ).
fof(f15083,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f15080,f6734]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM736+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 03:00:08 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.43 % Drodi V4.1.1
% 240.27/30.83 % Refutation found
% 240.27/30.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 240.27/30.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 68.33/30.99 % Elapsed time: 30.603936 seconds
% 68.33/30.99 % CPU time: 242.018227 seconds
% 68.33/30.99 % Total memory used: 1.111 GB
% 68.33/30.99 % Net memory used: 1.037 GB
%------------------------------------------------------------------------------