%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SCT171+3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 : Sun Sep 27 08:27:55 AM UTC 2026
% Result : Theorem 31.39s 7.08s
% Output : CNFRefutation 31.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 3
% Syntax : Number of formulae : 9 ( 7 unt; 0 def)
% Number of atoms : 11 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 6 ( 4 ~; 1 |; 0 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 3 ( 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 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_13__096c_A_060_092_060_094bsub_062F_A_I_Fi_O_Aif_Ah_Ai_A_060_An_Athen_Amkto,axiom,
hBOOL('hAPP$uf592646513l$ubool'('hAPP$uP229966473l$ubool'('member1441201108le$ualt','hAPP$uA702847159le$ualt'('hAPP$uA1505516597le$ualt'('produc1400112471le$ualt',c),d)),'hAPP$uf412050202t$ubool'(f,'hAPP$uf1740414619t$ubool'('cOMBS$u1064524443t$ubool'('hAPP$uf1842612975t$ubool'('cOMBS$u131695599t$ubool'('hAPP$uf586238575t$ubool'('cOMBB$u2107911302e$uindi'('if$ufun2098446489t$ubool'),'hAPP$un821919323i$ubool'('hAPP$uf446868133i$ubool'('cOMBC$u1996607964t$ubool','hAPP$uf224734595t$ubool'('cOMBB$u1883918730e$uindi'('ord$uless$unat'),h)),n))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uf721938099t$ubool'('cOMBB$u2032668066e$uindi'('arrow$u1644373103$umktop'),p)),e))),'hAPP$uf1740414619t$ubool'('cOMBS$u1064524443t$ubool'('hAPP$uf1842612975t$ubool'('cOMBS$u131695599t$ubool'('hAPP$uf586238575t$ubool'('cOMBB$u2107911302e$uindi'('if$ufun2098446489t$ubool'),'hAPP$un821919323i$ubool'('hAPP$uf446868133i$ubool'('cOMBC$u1996607964t$ubool','hAPP$uf224734595t$ubool'('cOMBB$u1883918730e$uindi'('fequal$unat'),h)),n))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uA1906441908t$ubool'('hAPP$uf248867553t$ubool'('cOMBC$u898791271t$ubool','hAPP$uf210227915t$ubool'('cOMBB$u1769989562e$uindi'('arrow$u230821333$uabove'),p)),c)),e))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uf721938099t$ubool'('cOMBB$u2032668066e$uindi'('arrow$u1495666017$umkbot'),p)),e)))))) ).
fof(fact_14_PW,axiom,
( hBOOL('hAPP$uf592646513l$ubool'('hAPP$uP229966473l$ubool'('member1441201108le$ualt','hAPP$uA702847159le$ualt'('hAPP$uA1505516597le$ualt'('produc1400112471le$ualt',c),d)),'hAPP$uf412050202t$ubool'(f,p)))
<=> hBOOL('hAPP$uf592646513l$ubool'('hAPP$uP229966473l$ubool'('member1441201108le$ualt','hAPP$uA702847159le$ualt'('hAPP$uA1505516597le$ualt'('produc1400112471le$ualt',c),d)),'hAPP$uf412050202t$ubool'(f,'hAPP$uf1740414619t$ubool'('cOMBS$u1064524443t$ubool'('hAPP$uf1842612975t$ubool'('cOMBS$u131695599t$ubool'('hAPP$uf586238575t$ubool'('cOMBB$u2107911302e$uindi'('if$ufun2098446489t$ubool'),'hAPP$un821919323i$ubool'('hAPP$uf446868133i$ubool'('cOMBC$u1996607964t$ubool','hAPP$uf224734595t$ubool'('cOMBB$u1883918730e$uindi'('ord$uless$unat'),h)),n))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uf721938099t$ubool'('cOMBB$u2032668066e$uindi'('arrow$u1644373103$umktop'),p)),e))),'hAPP$uf1740414619t$ubool'('cOMBS$u1064524443t$ubool'('hAPP$uf1842612975t$ubool'('cOMBS$u131695599t$ubool'('hAPP$uf586238575t$ubool'('cOMBB$u2107911302e$uindi'('if$ufun2098446489t$ubool'),'hAPP$un821919323i$ubool'('hAPP$uf446868133i$ubool'('cOMBC$u1996607964t$ubool','hAPP$uf224734595t$ubool'('cOMBB$u1883918730e$uindi'('fequal$unat'),h)),n))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uA1906441908t$ubool'('hAPP$uf248867553t$ubool'('cOMBC$u898791271t$ubool','hAPP$uf210227915t$ubool'('cOMBB$u1769989562e$uindi'('arrow$u230821333$uabove'),p)),c)),e))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uf721938099t$ubool'('cOMBB$u2032668066e$uindi'('arrow$u1495666017$umkbot'),p)),e)))))) ) ).
fof(conj_0,conjecture,
hBOOL('hAPP$uf592646513l$ubool'('hAPP$uP229966473l$ubool'('member1441201108le$ualt','hAPP$uA702847159le$ualt'('hAPP$uA1505516597le$ualt'('produc1400112471le$ualt',c),d)),'hAPP$uf412050202t$ubool'(f,p))) ).
fof(negated_conjecture,negated_conjecture,
~ hBOOL('hAPP$uf592646513l$ubool'('hAPP$uP229966473l$ubool'('member1441201108le$ualt','hAPP$uA702847159le$ualt'('hAPP$uA1505516597le$ualt'('produc1400112471le$ualt',c),d)),'hAPP$uf412050202t$ubool'(f,p))),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c203,plain,
hBOOL('hAPP$uf592646513l$ubool'('hAPP$uP229966473l$ubool'('member1441201108le$ualt','hAPP$uA702847159le$ualt'('hAPP$uA1505516597le$ualt'('produc1400112471le$ualt',c),d)),'hAPP$uf412050202t$ubool'(f,'hAPP$uf1740414619t$ubool'('cOMBS$u1064524443t$ubool'('hAPP$uf1842612975t$ubool'('cOMBS$u131695599t$ubool'('hAPP$uf586238575t$ubool'('cOMBB$u2107911302e$uindi'('if$ufun2098446489t$ubool'),'hAPP$un821919323i$ubool'('hAPP$uf446868133i$ubool'('cOMBC$u1996607964t$ubool','hAPP$uf224734595t$ubool'('cOMBB$u1883918730e$uindi'('ord$uless$unat'),h)),n))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uf721938099t$ubool'('cOMBB$u2032668066e$uindi'('arrow$u1644373103$umktop'),p)),e))),'hAPP$uf1740414619t$ubool'('cOMBS$u1064524443t$ubool'('hAPP$uf1842612975t$ubool'('cOMBS$u131695599t$ubool'('hAPP$uf586238575t$ubool'('cOMBB$u2107911302e$uindi'('if$ufun2098446489t$ubool'),'hAPP$un821919323i$ubool'('hAPP$uf446868133i$ubool'('cOMBC$u1996607964t$ubool','hAPP$uf224734595t$ubool'('cOMBB$u1883918730e$uindi'('fequal$unat'),h)),n))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uA1906441908t$ubool'('hAPP$uf248867553t$ubool'('cOMBC$u898791271t$ubool','hAPP$uf210227915t$ubool'('cOMBB$u1769989562e$uindi'('arrow$u230821333$uabove'),p)),c)),e))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uf721938099t$ubool'('cOMBB$u2032668066e$uindi'('arrow$u1495666017$umkbot'),p)),e)))))),
inference(clausification,[status(esa)],[fact_13__096c_A_060_092_060_094bsub_062F_A_I_Fi_O_Aif_Ah_Ai_A_060_An_Athen_Amkto]) ).
cnf(c205,plain,
( ~ hBOOL('hAPP$uf592646513l$ubool'('hAPP$uP229966473l$ubool'('member1441201108le$ualt','hAPP$uA702847159le$ualt'('hAPP$uA1505516597le$ualt'('produc1400112471le$ualt',c),d)),'hAPP$uf412050202t$ubool'(f,'hAPP$uf1740414619t$ubool'('cOMBS$u1064524443t$ubool'('hAPP$uf1842612975t$ubool'('cOMBS$u131695599t$ubool'('hAPP$uf586238575t$ubool'('cOMBB$u2107911302e$uindi'('if$ufun2098446489t$ubool'),'hAPP$un821919323i$ubool'('hAPP$uf446868133i$ubool'('cOMBC$u1996607964t$ubool','hAPP$uf224734595t$ubool'('cOMBB$u1883918730e$uindi'('ord$uless$unat'),h)),n))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uf721938099t$ubool'('cOMBB$u2032668066e$uindi'('arrow$u1644373103$umktop'),p)),e))),'hAPP$uf1740414619t$ubool'('cOMBS$u1064524443t$ubool'('hAPP$uf1842612975t$ubool'('cOMBS$u131695599t$ubool'('hAPP$uf586238575t$ubool'('cOMBB$u2107911302e$uindi'('if$ufun2098446489t$ubool'),'hAPP$un821919323i$ubool'('hAPP$uf446868133i$ubool'('cOMBC$u1996607964t$ubool','hAPP$uf224734595t$ubool'('cOMBB$u1883918730e$uindi'('fequal$unat'),h)),n))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uA1906441908t$ubool'('hAPP$uf248867553t$ubool'('cOMBC$u898791271t$ubool','hAPP$uf210227915t$ubool'('cOMBB$u1769989562e$uindi'('arrow$u230821333$uabove'),p)),c)),e))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uf721938099t$ubool'('cOMBB$u2032668066e$uindi'('arrow$u1495666017$umkbot'),p)),e))))))
| hBOOL('hAPP$uf592646513l$ubool'('hAPP$uP229966473l$ubool'('member1441201108le$ualt','hAPP$uA702847159le$ualt'('hAPP$uA1505516597le$ualt'('produc1400112471le$ualt',c),d)),'hAPP$uf412050202t$ubool'(f,p))) ),
inference(clausification,[status(esa)],[fact_14_PW]) ).
cnf(c2397,plain,
~ hBOOL('hAPP$uf592646513l$ubool'('hAPP$uP229966473l$ubool'('member1441201108le$ualt','hAPP$uA702847159le$ualt'('hAPP$uA1505516597le$ualt'('produc1400112471le$ualt',c),d)),'hAPP$uf412050202t$ubool'(f,p))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
~ hBOOL('hAPP$uf592646513l$ubool'('hAPP$uP229966473l$ubool'('member1441201108le$ualt','hAPP$uA702847159le$ualt'('hAPP$uA1505516597le$ualt'('produc1400112471le$ualt',c),d)),'hAPP$uf412050202t$ubool'(f,'hAPP$uf1740414619t$ubool'('cOMBS$u1064524443t$ubool'('hAPP$uf1842612975t$ubool'('cOMBS$u131695599t$ubool'('hAPP$uf586238575t$ubool'('cOMBB$u2107911302e$uindi'('if$ufun2098446489t$ubool'),'hAPP$un821919323i$ubool'('hAPP$uf446868133i$ubool'('cOMBC$u1996607964t$ubool','hAPP$uf224734595t$ubool'('cOMBB$u1883918730e$uindi'('ord$uless$unat'),h)),n))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uf721938099t$ubool'('cOMBB$u2032668066e$uindi'('arrow$u1644373103$umktop'),p)),e))),'hAPP$uf1740414619t$ubool'('cOMBS$u1064524443t$ubool'('hAPP$uf1842612975t$ubool'('cOMBS$u131695599t$ubool'('hAPP$uf586238575t$ubool'('cOMBB$u2107911302e$uindi'('if$ufun2098446489t$ubool'),'hAPP$un821919323i$ubool'('hAPP$uf446868133i$ubool'('cOMBC$u1996607964t$ubool','hAPP$uf224734595t$ubool'('cOMBB$u1883918730e$uindi'('fequal$unat'),h)),n))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uA1906441908t$ubool'('hAPP$uf248867553t$ubool'('cOMBC$u898791271t$ubool','hAPP$uf210227915t$ubool'('cOMBB$u1769989562e$uindi'('arrow$u230821333$uabove'),p)),c)),e))),'hAPP$uA1805174428t$ubool'('hAPP$uf1808153265t$ubool'('cOMBC$u1353880399t$ubool','hAPP$uf721938099t$ubool'('cOMBB$u2032668066e$uindi'('arrow$u1495666017$umkbot'),p)),e)))))),
inference(resolution,[status(thm)],[c2397,c205]) ).
cnf(d1,plain,
$false,
inference(resolution,[status(thm)],[c203,d0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT171+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n006.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.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 06:38:11 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 31.39/7.08 % SZS status Theorem for theBenchmark.p
% 31.39/7.08 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------