%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT055-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:15 PM UTC 2026
% Result : Unsatisfiable 0.27s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT055-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n020.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 04:29:18 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.27/0.54 % Drodi V4.1.1
% 0.27/0.57 % Refutation found
% 0.27/0.57 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.27/0.57 % SZS output start CNFRefutation for theBenchmark
% 0.27/0.57 fof(f632,axiom,(
% 0.27/0.57 (![V_i]: (( hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))| ~ hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ) ))),
% 0.27/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.57 fof(f633,axiom,(
% 0.27/0.57 (![V_i]: (( hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))| ~ hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ) ))),
% 0.27/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.57 fof(f634,axiom,(
% 0.27/0.57 (![V_x,V_S,T_a]: (( hBOOL(c_in(V_x,V_S,T_a))| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 0.27/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.57 fof(f635,axiom,(
% 0.27/0.57 (![V_S,V_x,T_a]: (( hBOOL(hAPP(V_S,V_x))| ~ hBOOL(c_in(V_x,V_S,T_a)) ) ))),
% 0.27/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.57 fof(f638,axiom,(
% 0.27/0.57 (![V_i]: (( hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,V_i)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))| ~ hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ) ))),
% 0.27/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.57 fof(f639,axiom,(
% 0.27/0.57 (![V_i]: (( hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))| ~ hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,V_i)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ) ))),
% 0.27/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.57 fof(f640,negated_conjecture,(
% 0.27/0.57 ( hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))| hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,v_x)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ) ),
% 0.27/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.57 fof(f641,negated_conjecture,(
% 0.27/0.57 ( ~ hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))| ~ hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,v_x)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ) ),
% 0.27/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.57 fof(f1616,plain,(
% 0.27/0.57 ![X0]: (hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))))),
% 0.27/0.57 inference(cnf_transformation,[status(thm)],[f632])).
% 0.27/0.57 fof(f1617,plain,(
% 0.27/0.57 ![X0]: (hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))))),
% 0.27/0.57 inference(cnf_transformation,[status(thm)],[f633])).
% 0.27/0.57 fof(f1618,plain,(
% 0.27/0.57 ![V_x,V_S]: ((![T_a]: hBOOL(c_in(V_x,V_S,T_a)))|~hBOOL(hAPP(V_S,V_x)))),
% 0.27/0.57 inference(miniscoping,[status(thm)],[f634])).
% 0.27/0.57 fof(f1619,plain,(
% 0.27/0.57 ![X0,X1,X2]: (hBOOL(c_in(X0,X1,X2))|~hBOOL(hAPP(X1,X0)))),
% 0.27/0.57 inference(cnf_transformation,[status(thm)],[f1618])).
% 0.27/0.57 fof(f1620,plain,(
% 0.27/0.57 ![V_S,V_x]: (hBOOL(hAPP(V_S,V_x))|(![T_a]: ~hBOOL(c_in(V_x,V_S,T_a))))),
% 0.27/0.57 inference(miniscoping,[status(thm)],[f635])).
% 0.27/0.57 fof(f1621,plain,(
% 0.27/0.57 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|~hBOOL(c_in(X1,X0,X2)))),
% 0.27/0.57 inference(cnf_transformation,[status(thm)],[f1620])).
% 0.27/0.57 fof(f1624,plain,(
% 0.27/0.57 ![X0]: (hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))))),
% 0.27/0.57 inference(cnf_transformation,[status(thm)],[f638])).
% 0.27/0.57 fof(f1625,plain,(
% 0.27/0.57 ![X0]: (hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))))),
% 0.27/0.57 inference(cnf_transformation,[status(thm)],[f639])).
% 0.27/0.57 fof(f1626,plain,(
% 0.27/0.57 hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,v_x)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 0.27/0.57 inference(cnf_transformation,[status(thm)],[f640])).
% 0.27/0.57 fof(f1627,plain,(
% 0.27/0.57 ~hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,v_x)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 0.27/0.57 inference(cnf_transformation,[status(thm)],[f641])).
% 0.27/0.57 fof(f1679,definition,(
% 0.27/0.57 sQ4_spl <=> (hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))))),
% 0.27/0.57 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.27/0.57 fof(f1680,plain,(
% 0.27/0.57 hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~sQ4_spl),
% 0.27/0.57 inference(component_clause,[status(thm)],[f1679])).
% 0.27/0.57 fof(f1682,definition,(
% 0.27/0.57 sQ5_spl <=> (hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,v_x)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))))),
% 0.27/0.57 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.27/0.57 fof(f1683,plain,(
% 0.27/0.57 hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,v_x)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~sQ5_spl),
% 0.27/0.57 inference(component_clause,[status(thm)],[f1682])).
% 0.27/0.57 fof(f1685,plain,(
% 0.27/0.57 sQ4_spl|sQ5_spl),
% 0.27/0.57 inference(split_clause,[status(thm)],[f1626,f1679,f1682])).
% 0.27/0.57 fof(f1686,plain,(
% 0.27/0.57 ~sQ4_spl|~sQ5_spl),
% 0.27/0.57 inference(split_clause,[status(thm)],[f1627,f1679,f1682])).
% 0.27/0.57 fof(f1700,plain,(
% 0.27/0.57 hBOOL(hAPP(hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,v_x)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~sQ5_spl),
% 0.27/0.57 inference(resolution,[status(thm)],[f1621,f1683])).
% 0.27/0.57 fof(f1701,plain,(
% 0.27/0.57 ![X0]: (hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,v_x)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),X0))|~sQ5_spl)),
% 0.27/0.57 inference(resolution,[status(thm)],[f1700,f1619])).
% 0.27/0.57 fof(f1710,plain,(
% 0.27/0.57 hBOOL(hAPP(v_P_H____(v_x),c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~sQ4_spl),
% 0.27/0.57 inference(resolution,[status(thm)],[f1680,f1621])).
% 0.27/0.57 fof(f1711,plain,(
% 0.27/0.57 ![X0]: (hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(v_x),X0))|~sQ4_spl)),
% 0.27/0.57 inference(resolution,[status(thm)],[f1710,f1619])).
% 0.27/0.57 fof(f1713,plain,(
% 0.27/0.57 hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~sQ4_spl),
% 0.27/0.57 inference(resolution,[status(thm)],[f1616,f1711])).
% 0.27/0.57 fof(f1714,plain,(
% 0.27/0.57 hBOOL(hAPP(hAPP(v_P____,v_x),c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~sQ4_spl),
% 0.27/0.57 inference(resolution,[status(thm)],[f1713,f1621])).
% 0.27/0.57 fof(f1721,plain,(
% 0.27/0.57 ![X0]: (hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_x),X0))|~sQ4_spl)),
% 0.27/0.57 inference(resolution,[status(thm)],[f1714,f1619])).
% 0.27/0.57 fof(f1724,plain,(
% 0.27/0.57 hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,v_x)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~sQ4_spl),
% 0.27/0.57 inference(resolution,[status(thm)],[f1624,f1721])).
% 0.27/0.57 fof(f1725,plain,(
% 0.27/0.57 sQ5_spl|~sQ4_spl),
% 0.27/0.57 inference(split_clause,[status(thm)],[f1724,f1682,f1679])).
% 0.27/0.57 fof(f1728,plain,(
% 0.27/0.57 hBOOL(c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~sQ5_spl),
% 0.27/0.57 inference(resolution,[status(thm)],[f1625,f1701])).
% 0.27/0.57 fof(f1730,plain,(
% 0.27/0.57 hBOOL(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P_H____(v_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~sQ5_spl),
% 0.27/0.57 inference(resolution,[status(thm)],[f1728,f1617])).
% 0.27/0.57 fof(f1732,plain,(
% 0.27/0.57 sQ4_spl|~sQ5_spl),
% 0.27/0.57 inference(split_clause,[status(thm)],[f1730,f1679,f1682])).
% 0.27/0.57 fof(f1733,plain,(
% 0.27/0.57 $false),
% 0.27/0.57 inference(sat_refutation,[status(thm)],[f1685,f1686,f1725,f1732])).
% 0.27/0.57 % SZS output end CNFRefutation for theBenchmark.p
% 0.27/0.64 % Elapsed time: 0.188184 seconds
% 0.27/0.64 % CPU time: 0.293516 seconds
% 0.27/0.64 % Total memory used: 44.814 MB
% 0.27/0.64 % Net memory used: 44.691 MB
%------------------------------------------------------------------------------