%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT021-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 : n007.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:13 PM UTC 2026
% Result : Unsatisfiable 6.77s 1.34s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT021-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.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 04:24:35 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.45 % Drodi V4.1.1
% 6.77/1.34 % Refutation found
% 6.77/1.34 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.77/1.34 % SZS output start CNFRefutation for theBenchmark
% 6.77/1.34 fof(f670,axiom,(
% 6.77/1.34 (![V_x,V_z,T_a,V_r,V_y]: (( hBOOL(c_in(c_Pair(V_x,V_z,T_a,T_a),V_r,tc_prod(T_a,T_a)))| ~ hBOOL(c_in(c_Pair(V_y,V_z,T_a,T_a),V_r,tc_prod(T_a,T_a)))| ~ hBOOL(c_in(c_Pair(V_x,V_y,T_a,T_a),V_r,tc_prod(T_a,T_a)))| ~ c_Relation_Otrans(V_r,T_a) ) ))),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f672,axiom,(
% 6.77/1.34 (![V_x,T_a,V_r]: (( ~ hBOOL(c_in(c_Pair(V_x,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)))| ~ c_Relation_Oirrefl(V_r,T_a) ) ))),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f674,axiom,(
% 6.77/1.34 (![T_a,V_x]: (hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_x)) ))),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f676,axiom,(
% 6.77/1.34 (![V_xa,V_x,T_a,V_r,V_A]: (( hBOOL(c_in(c_Pair(V_xa,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)))| hBOOL(c_in(c_Pair(V_x,V_xa,T_a,T_a),V_r,tc_prod(T_a,T_a)))| V_x = V_xa| ~ hBOOL(c_in(V_xa,V_A,T_a))| ~ hBOOL(c_in(V_x,V_A,T_a))| ~ c_Relation_Ototal__on(V_A,V_r,T_a) ) ))),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f677,axiom,(
% 6.77/1.34 (![V_x,V_S,T_a]: (( hBOOL(c_in(V_x,V_S,T_a))| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f678,axiom,(
% 6.77/1.34 (![V_S,V_x,T_a]: (( hBOOL(hAPP(V_S,V_x))| ~ hBOOL(c_in(V_x,V_S,T_a)) ) ))),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f679,negated_conjecture,(
% 6.77/1.34 (![V_x]: (c_Relation_Otrans(hAPP(v_P,V_x),tc_Arrow__Order__Mirabelle_Oalt) ))),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f680,negated_conjecture,(
% 6.77/1.34 (![V_x]: (c_Relation_Oirrefl(hAPP(v_P,V_x),tc_Arrow__Order__Mirabelle_Oalt) ))),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f681,negated_conjecture,(
% 6.77/1.34 (![V_x]: (c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,V_x),tc_Arrow__Order__Mirabelle_Oalt) ))),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f682,negated_conjecture,(
% 6.77/1.34 hBOOL(c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))) ),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f683,negated_conjecture,(
% 6.77/1.34 ~ 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))) ),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f684,negated_conjecture,(
% 6.77/1.34 ( c_Relation_Otrans(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)| ~ c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)| ~ c_Relation_Oirrefl(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)| ~ c_Relation_Otrans(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt) ) ),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f685,negated_conjecture,(
% 6.77/1.34 ( c_Relation_Oirrefl(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)| ~ c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)| ~ c_Relation_Oirrefl(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)| ~ c_Relation_Otrans(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt) ) ),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f687,negated_conjecture,(
% 6.77/1.34 (![V_a,V_b,V_P]: (( hBOOL(c_in(c_Pair(V_a,V_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(V_P),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)))| V_a = V_b| ~ c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt)| ~ c_Relation_Oirrefl(hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt)| ~ c_Relation_Otrans(hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt) ) ))),
% 6.77/1.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.77/1.34 fof(f1701,plain,(
% 6.77/1.34 ![T_a,V_r]: ((![V_x,V_y]: ((![V_z]: (hBOOL(c_in(c_Pair(V_x,V_z,T_a,T_a),V_r,tc_prod(T_a,T_a)))|~hBOOL(c_in(c_Pair(V_y,V_z,T_a,T_a),V_r,tc_prod(T_a,T_a)))))|~hBOOL(c_in(c_Pair(V_x,V_y,T_a,T_a),V_r,tc_prod(T_a,T_a)))))|~c_Relation_Otrans(V_r,T_a))),
% 6.77/1.34 inference(miniscoping,[status(thm)],[f670])).
% 6.77/1.34 fof(f1702,plain,(
% 6.77/1.34 ![X0,X1,X2,X3,X4]: (hBOOL(c_in(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2)))|~hBOOL(c_in(c_Pair(X4,X1,X2,X2),X3,tc_prod(X2,X2)))|~hBOOL(c_in(c_Pair(X0,X4,X2,X2),X3,tc_prod(X2,X2)))|~c_Relation_Otrans(X3,X2))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f1701])).
% 6.77/1.34 fof(f1705,plain,(
% 6.77/1.34 ![T_a,V_r]: ((![V_x]: ~hBOOL(c_in(c_Pair(V_x,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a))))|~c_Relation_Oirrefl(V_r,T_a))),
% 6.77/1.34 inference(miniscoping,[status(thm)],[f672])).
% 6.77/1.34 fof(f1706,plain,(
% 6.77/1.34 ![X0,X1,X2]: (~hBOOL(c_in(c_Pair(X0,X0,X1,X1),X2,tc_prod(X1,X1)))|~c_Relation_Oirrefl(X2,X1))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f1705])).
% 6.77/1.34 fof(f1708,plain,(
% 6.77/1.34 ![X0,X1]: (hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1)))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f674])).
% 6.77/1.34 fof(f1710,plain,(
% 6.77/1.34 ![T_a,V_r,V_A]: ((![V_x]: ((![V_xa]: (((hBOOL(c_in(c_Pair(V_xa,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)))|hBOOL(c_in(c_Pair(V_x,V_xa,T_a,T_a),V_r,tc_prod(T_a,T_a))))|V_x=V_xa)|~hBOOL(c_in(V_xa,V_A,T_a))))|~hBOOL(c_in(V_x,V_A,T_a))))|~c_Relation_Ototal__on(V_A,V_r,T_a))),
% 6.77/1.34 inference(miniscoping,[status(thm)],[f676])).
% 6.77/1.34 fof(f1711,plain,(
% 6.77/1.34 ![X0,X1,X2,X3,X4]: (hBOOL(c_in(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2)))|hBOOL(c_in(c_Pair(X1,X0,X2,X2),X3,tc_prod(X2,X2)))|X1=X0|~hBOOL(c_in(X0,X4,X2))|~hBOOL(c_in(X1,X4,X2))|~c_Relation_Ototal__on(X4,X3,X2))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f1710])).
% 6.77/1.34 fof(f1712,plain,(
% 6.77/1.34 ![V_x,V_S]: ((![T_a]: hBOOL(c_in(V_x,V_S,T_a)))|~hBOOL(hAPP(V_S,V_x)))),
% 6.77/1.34 inference(miniscoping,[status(thm)],[f677])).
% 6.77/1.34 fof(f1713,plain,(
% 6.77/1.34 ![X0,X1,X2]: (hBOOL(c_in(X0,X1,X2))|~hBOOL(hAPP(X1,X0)))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f1712])).
% 6.77/1.34 fof(f1714,plain,(
% 6.77/1.34 ![V_S,V_x]: (hBOOL(hAPP(V_S,V_x))|(![T_a]: ~hBOOL(c_in(V_x,V_S,T_a))))),
% 6.77/1.34 inference(miniscoping,[status(thm)],[f678])).
% 6.77/1.34 fof(f1715,plain,(
% 6.77/1.34 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|~hBOOL(c_in(X1,X0,X2)))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f1714])).
% 6.77/1.34 fof(f1716,plain,(
% 6.77/1.34 ![X0]: (c_Relation_Otrans(hAPP(v_P,X0),tc_Arrow__Order__Mirabelle_Oalt))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f679])).
% 6.77/1.34 fof(f1717,plain,(
% 6.77/1.34 ![X0]: (c_Relation_Oirrefl(hAPP(v_P,X0),tc_Arrow__Order__Mirabelle_Oalt))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f680])).
% 6.77/1.34 fof(f1718,plain,(
% 6.77/1.34 ![X0]: (c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,X0),tc_Arrow__Order__Mirabelle_Oalt))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f681])).
% 6.77/1.34 fof(f1719,plain,(
% 6.77/1.34 hBOOL(c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f682])).
% 6.77/1.34 fof(f1720,plain,(
% 6.77/1.34 ~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)))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f683])).
% 6.77/1.34 fof(f1721,plain,(
% 6.77/1.34 c_Relation_Otrans(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Oirrefl(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Otrans(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f684])).
% 6.77/1.34 fof(f1722,plain,(
% 6.77/1.34 c_Relation_Oirrefl(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Oirrefl(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Otrans(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f685])).
% 6.77/1.34 fof(f1724,plain,(
% 6.77/1.34 ![V_P]: ((((![V_a,V_b]: ((hBOOL(c_in(c_Pair(V_a,V_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(V_P),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))))|V_a=V_b))|~c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt))|~c_Relation_Oirrefl(hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt))|~c_Relation_Otrans(hAPP(V_P,v_Pa(V_P)),tc_Arrow__Order__Mirabelle_Oalt))),
% 6.77/1.34 inference(miniscoping,[status(thm)],[f687])).
% 6.77/1.34 fof(f1725,plain,(
% 6.77/1.34 ![X0,X1,X2]: (hBOOL(c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~hBOOL(c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|X0=X1|~c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(X2,v_Pa(X2)),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Oirrefl(hAPP(X2,v_Pa(X2)),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Otrans(hAPP(X2,v_Pa(X2)),tc_Arrow__Order__Mirabelle_Oalt))),
% 6.77/1.34 inference(cnf_transformation,[status(thm)],[f1724])).
% 6.77/1.34 fof(f1796,plain,(
% 6.77/1.34 c_Relation_Otrans(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Oirrefl(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Otrans(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.34 inference(forward_subsumption_resolution,[status(thm)],[f1721,f1718])).
% 6.77/1.34 fof(f1797,plain,(
% 6.77/1.34 c_Relation_Oirrefl(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Oirrefl(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Otrans(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.34 inference(forward_subsumption_resolution,[status(thm)],[f1722,f1718])).
% 6.77/1.34 fof(f1814,plain,(
% 6.77/1.34 c_Relation_Otrans(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Otrans(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.34 inference(resolution,[status(thm)],[f1796,f1717])).
% 6.77/1.34 fof(f1815,plain,(
% 6.77/1.34 c_Relation_Otrans(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.34 inference(forward_subsumption_resolution,[status(thm)],[f1814,f1716])).
% 6.77/1.34 fof(f1819,plain,(
% 6.77/1.34 c_Relation_Oirrefl(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Otrans(hAPP(v_P,v_x),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.34 inference(resolution,[status(thm)],[f1797,f1717])).
% 6.77/1.34 fof(f1820,plain,(
% 6.77/1.34 c_Relation_Oirrefl(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.34 inference(forward_subsumption_resolution,[status(thm)],[f1819,f1716])).
% 6.77/1.34 fof(f1821,plain,(
% 6.77/1.34 ![X0,X1,X2]: (hBOOL(c_in(X0,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X2)))),
% 6.77/1.34 inference(resolution,[status(thm)],[f1713,f1708])).
% 6.77/1.34 fof(f1822,plain,(
% 6.77/1.34 hBOOL(hAPP(v_F(v_P),c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 6.77/1.34 inference(resolution,[status(thm)],[f1715,f1719])).
% 6.77/1.34 fof(f1839,plain,(
% 6.77/1.34 ![X0]: (hBOOL(c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),X0)))),
% 6.77/1.34 inference(resolution,[status(thm)],[f1822,f1713])).
% 6.77/1.34 fof(f1984,plain,(
% 6.77/1.34 ![X0]: (hBOOL(c_in(c_Pair(v_a,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~hBOOL(c_in(c_Pair(v_b,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~c_Relation_Otrans(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt))),
% 6.77/1.34 inference(resolution,[status(thm)],[f1702,f1839])).
% 6.77/1.34 fof(f1990,plain,(
% 6.77/1.34 ![X0]: (hBOOL(c_in(c_Pair(v_a,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~hBOOL(c_in(c_Pair(v_b,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))))),
% 6.77/1.34 inference(forward_subsumption_resolution,[status(thm)],[f1984,f1815])).
% 6.77/1.34 fof(f1993,plain,(
% 6.77/1.34 ![X0,X1,X2]: (hBOOL(c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|hBOOL(c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|X1=X0|~hBOOL(c_in(X0,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),tc_Arrow__Order__Mirabelle_Oalt))|~hBOOL(c_in(X1,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),tc_Arrow__Order__Mirabelle_Oalt)))),
% 6.77/1.34 inference(resolution,[status(thm)],[f1711,f1718])).
% 6.77/1.34 fof(f1997,plain,(
% 6.77/1.34 ![X0,X1,X2]: (hBOOL(c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|hBOOL(c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|X1=X0|~hBOOL(c_in(X1,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),tc_Arrow__Order__Mirabelle_Oalt)))),
% 6.77/1.34 inference(forward_subsumption_resolution,[status(thm)],[f1993,f1821])).
% 6.77/1.34 fof(f2076,plain,(
% 6.77/1.34 ![X0,X1,X2]: (hBOOL(c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|hBOOL(c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|X1=X0)),
% 6.77/1.34 inference(resolution,[status(thm)],[f1997,f1821])).
% 6.77/1.34 fof(f2078,plain,(
% 6.77/1.34 hBOOL(c_in(c_Pair(v_b,v_a,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)))|v_b=v_a),
% 6.77/1.34 inference(resolution,[status(thm)],[f2076,f1720])).
% 6.77/1.34 fof(f2233,plain,(
% 6.77/1.34 v_b=v_a|hBOOL(c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|v_b=v_a|~c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Oirrefl(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Otrans(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.34 inference(resolution,[status(thm)],[f2078,f1725])).
% 6.77/1.34 fof(f2237,plain,(
% 6.77/1.34 v_b=v_a|hBOOL(c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~c_Relation_Ototal__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Oirrefl(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Otrans(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.34 inference(duplicate_literals_removal,[status(thm)],[f2233])).
% 6.77/1.34 fof(f2238,plain,(
% 6.77/1.34 v_b=v_a|hBOOL(c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~c_Relation_Oirrefl(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)|~c_Relation_Otrans(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.34 inference(forward_subsumption_resolution,[status(thm)],[f2237,f1718])).
% 6.77/1.34 fof(f2367,plain,(
% 6.77/1.34 v_b=v_a|hBOOL(c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~c_Relation_Otrans(hAPP(v_P,v_Pa(v_P)),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.36 inference(resolution,[status(thm)],[f2238,f1717])).
% 6.77/1.36 fof(f2368,plain,(
% 6.77/1.36 v_b=v_a|hBOOL(c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 6.77/1.36 inference(forward_subsumption_resolution,[status(thm)],[f2367,f1716])).
% 6.77/1.36 fof(f2369,plain,(
% 6.77/1.36 v_b=v_a|hBOOL(c_in(c_Pair(v_a,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 6.77/1.36 inference(resolution,[status(thm)],[f2368,f1990])).
% 6.77/1.36 fof(f2524,plain,(
% 6.77/1.36 v_b=v_a|~c_Relation_Oirrefl(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.36 inference(resolution,[status(thm)],[f2369,f1706])).
% 6.77/1.36 fof(f2534,plain,(
% 6.77/1.36 ![X0]: (hBOOL(c_in(c_Pair(v_b,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P),X0)))),
% 6.77/1.36 inference(backward_demodulation,[status(thm)],[f2545,f1839])).
% 6.77/1.36 fof(f2545,plain,(
% 6.77/1.36 v_b=v_a),
% 6.77/1.36 inference(forward_subsumption_resolution,[status(thm)],[f2524,f1820])).
% 6.77/1.36 fof(f2551,plain,(
% 6.77/1.36 ~c_Relation_Oirrefl(v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)),
% 6.77/1.36 inference(resolution,[status(thm)],[f2534,f1706])).
% 6.77/1.36 fof(f2554,plain,(
% 6.77/1.36 $false),
% 6.77/1.36 inference(forward_subsumption_resolution,[status(thm)],[f2551,f1820])).
% 6.77/1.36 % SZS output end CNFRefutation for theBenchmark.p
% 6.77/1.39 % Elapsed time: 1.010400 seconds
% 6.77/1.39 % CPU time: 7.154716 seconds
% 6.77/1.39 % Total memory used: 235.429 MB
% 6.77/1.39 % Net memory used: 232.506 MB
%------------------------------------------------------------------------------