%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SCT171+3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n013.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 02:40:58 PM UTC 2026
% Result : Theorem 2.46s 1.09s
% Output : CNFRefutation 2.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 3
% Syntax : Number of formulae : 13 ( 9 unt; 0 def)
% Number of atoms : 19 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 14 ( 8 ~; 4 |; 1 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 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 sgn 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/sandbox/benchmark/theBenchmark.p',fact_13__096c_A_060_092_060_094bsub_062F_A_I_Fi_O_Aif_Ah_Ai_A_060_An_Athen_Amkto) ).
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/sandbox/benchmark/theBenchmark.p',fact_14_PW) ).
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/sandbox/benchmark/theBenchmark.p',conj_0) ).
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(f1417,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(flattening,[],[f1416]) ).
fof(f2091,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)))
| 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,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,[],[f151]) ).
fof(f2355,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,[],[f1417]) ).
fof(f2420,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,[],[f2091]) ).
fof(f2421,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,[],[f150]) ).
tcf(c_54,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(cnf_transformation,[],[f2355]) ).
tcf(c_118,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)))
| ~ 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,[],[f2420]) ).
tcf(c_120,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,[],[f2421]) ).
tcf(c_1140,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_118,c_120,c_54]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT171+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n013.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 08:59:37 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 2.46/1.09 % SZS status Started for theBenchmark.p
% 2.46/1.09 % SZS status Theorem for theBenchmark.p
% 2.46/1.09
% 2.46/1.09 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.46/1.09
% 2.46/1.09 % ------ iProver source info
% 2.46/1.09
% 2.46/1.09 % git: date: 2026-07-19 20:42:38 +0200
% 2.46/1.09 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.46/1.09 % git: non_committed_changes: false
% 2.46/1.09
% 2.46/1.09 % ------ Parsing...
% 2.46/1.09 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.46/1.09
% 2.46/1.09 % ------ Preprocessing...%
% 2.46/1.09
% 2.46/1.09 % SZS status Theorem for theBenchmark.p
% 2.46/1.09
% 2.46/1.09 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.46/1.09
% 2.46/1.09
%------------------------------------------------------------------------------