%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SCT171+3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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 02:07:05 PM UTC 2026
% Result : Theorem 0.37s 0.81s
% Output : CNFRefutation 0.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 3
% Syntax : Number of formulae : 10 ( 7 unt; 0 def)
% Number of atoms : 15 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 11 ( 6 ~; 3 |; 1 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 41 ( 41 usr; 18 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f150,axiom,
hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(ord_less_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1644373103_mktop),p)),e))),hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(fequal_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_A1906441908t_bool(hAPP_f248867553t_bool(cOMBC_898791271t_bool,hAPP_f210227915t_bool(cOMBB_1769989562e_indi(arrow_230821333_above),p)),c)),e))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1495666017_mkbot),p)),e)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,axiom,
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,p)))
<=> hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(ord_less_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1644373103_mktop),p)),e))),hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(fequal_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_A1906441908t_bool(hAPP_f248867553t_bool(cOMBC_898791271t_bool,hAPP_f210227915t_bool(cOMBB_1769989562e_indi(arrow_230821333_above),p)),c)),e))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1495666017_mkbot),p)),e)))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1415,conjecture,
hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,p))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1416,negated_conjecture,
~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,p))),
inference(negated_conjecture,[status(cth)],[f1415]) ).
fof(f1711,plain,
hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(ord_less_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1644373103_mktop),p)),e))),hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(fequal_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_A1906441908t_bool(hAPP_f248867553t_bool(cOMBC_898791271t_bool,hAPP_f210227915t_bool(cOMBB_1769989562e_indi(arrow_230821333_above),p)),c)),e))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1495666017_mkbot),p)),e)))))),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f1712,plain,
( ( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(ord_less_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1644373103_mktop),p)),e))),hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(fequal_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_A1906441908t_bool(hAPP_f248867553t_bool(cOMBC_898791271t_bool,hAPP_f210227915t_bool(cOMBB_1769989562e_indi(arrow_230821333_above),p)),c)),e))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1495666017_mkbot),p)),e))))))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,p))) )
& ( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(ord_less_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1644373103_mktop),p)),e))),hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(fequal_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_A1906441908t_bool(hAPP_f248867553t_bool(cOMBC_898791271t_bool,hAPP_f210227915t_bool(cOMBB_1769989562e_indi(arrow_230821333_above),p)),c)),e))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1495666017_mkbot),p)),e))))))
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,p))) ) ),
inference(NNF_transformation,[status(thm)],[f151]) ).
fof(f1714,plain,
( ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(ord_less_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1644373103_mktop),p)),e))),hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(fequal_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_A1906441908t_bool(hAPP_f248867553t_bool(cOMBC_898791271t_bool,hAPP_f210227915t_bool(cOMBB_1769989562e_indi(arrow_230821333_above),p)),c)),e))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1495666017_mkbot),p)),e))))))
| hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,p))) ),
inference(cnf_transformation,[status(thm)],[f1712]) ).
fof(f6013,plain,
~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,p))),
inference(cnf_transformation,[status(thm)],[f1416]) ).
fof(f6525,plain,
~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(ord_less_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1644373103_mktop),p)),e))),hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(fequal_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_A1906441908t_bool(hAPP_f248867553t_bool(cOMBC_898791271t_bool,hAPP_f210227915t_bool(cOMBB_1769989562e_indi(arrow_230821333_above),p)),c)),e))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1495666017_mkbot),p)),e)))))),
inference(forward_subsumption_resolution,[status(thm)],[f1714,f6013]) ).
fof(f6526,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f1711,f6525]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT171+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.37 % Computer : n003.cluster.edu
% 0.03/0.37 % Model : x86_64 x86_64
% 0.03/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.37 % Memory : 8046.5625MB
% 0.03/0.37 % OS : Linux 6.8.0-71-generic
% 0.03/0.37 % CPULimit : 300
% 0.03/0.37 % WCLimit : 300
% 0.03/0.37 % DateTime : Mon Sep 21 04:39:32 UTC 2026
% 0.03/0.37 % CPUTime :
% 0.23/0.57 % Drodi V4.1.1
% 0.37/0.81 % Refutation found
% 0.37/0.81 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.37/0.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.37/0.86 % Elapsed time: 0.469006 seconds
% 0.37/0.86 % CPU time: 1.939841 seconds
% 0.37/0.86 % Total memory used: 281.744 MB
% 0.37/0.86 % Net memory used: 280.119 MB
%------------------------------------------------------------------------------