%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SCT120+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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:06:57 PM UTC 2026
% Result : Theorem 61.32s 8.76s
% Output : CNFRefutation 61.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 11
% Syntax : Number of formulae : 81 ( 20 unt; 0 def)
% Number of atoms : 305 ( 27 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 377 ( 153 ~; 161 |; 47 &)
% ( 7 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-5 aty)
% Number of functors : 24 ( 24 usr; 6 con; 0-4 aty)
% Number of variables : 216 ( 196 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [V_x_2,T_a] : c_member(T_a,V_x_2,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [V_r_2,T_a] :
( c_Relation_Oirrefl(T_a,V_r_2)
<=> ! [B_x] : ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_x),V_r_2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [V_r_2,V_A_2,T_a] :
( c_Relation_Ototal__on(T_a,V_A_2,V_r_2)
<=> ! [B_x] :
( c_member(T_a,B_x,V_A_2)
=> ! [B_xa] :
( c_member(T_a,B_xa,V_A_2)
=> ( B_x != B_xa
=> ( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_xa,B_x),V_r_2)
| c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_xa),V_r_2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [V_r_2,T_a] :
( c_Relation_Otrans(T_a,V_r_2)
<=> ! [B_x,B_y] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_y),V_r_2)
=> ! [B_z] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_y,B_z),V_r_2)
=> c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_z),V_r_2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [V_A_2,V_x_2,T_a] :
( c_member(T_a,V_x_2,V_A_2)
<=> hBOOL(hAPP(V_A_2,V_x_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [V_y_2,V_x_2,V_R_2,T_b,T_a] :
( c_FunDef_Oin__rel(T_a,T_b,V_R_2,V_x_2,V_y_2)
<=> c_member(tc_prod(T_a,T_b),c_Product__Type_OPair(T_a,T_b,V_x_2,V_y_2),V_R_2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f523,hypothesis,
! [B_x] :
( ! [B_xa] :
( c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(B_x,B_xa))
& c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_x,B_xa))
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_x,B_xa)) )
=> ( c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),v_F(B_x))
& c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(B_x))
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(B_x)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f524,hypothesis,
! [B_P] :
( ! [B_x] :
( c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(B_P,B_x))
& c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_P,B_x))
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_P,B_x)) )
=> ! [B_a,B_b] :
( B_a != B_b
=> ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_P,v_i))
=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),v_F(B_P)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f525,hypothesis,
! [B_x] :
( c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(v_P,B_x))
& c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,B_x))
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,B_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f526,hypothesis,
c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_b),v_F(v_P)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f527,conjecture,
c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_b),hAPP(v_P,v_i)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f528,negated_conjecture,
~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_b),hAPP(v_P,v_i)),
inference(negated_conjecture,[status(cth)],[f527]) ).
fof(f532,plain,
! [X0,X1] : c_member(X0,X1,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool))),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f533,plain,
! [V_r_2,T_a] :
( ( ? [B_x] : c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_x),V_r_2)
| c_Relation_Oirrefl(T_a,V_r_2) )
& ( ! [B_x] : ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_x),V_r_2)
| ~ c_Relation_Oirrefl(T_a,V_r_2) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f534,plain,
( ! [V_r_2,T_a] :
( ? [B_x] : c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_x),V_r_2)
| c_Relation_Oirrefl(T_a,V_r_2) )
& ! [V_r_2,T_a] :
( ! [B_x] : ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_x),V_r_2)
| ~ c_Relation_Oirrefl(T_a,V_r_2) ) ),
inference(miniscoping,[status(thm)],[f533]) ).
fof(f535,plain,
( ! [V_r_2,T_a] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,sK1_skl(T_a,V_r_2),sK1_skl(T_a,V_r_2)),V_r_2)
| c_Relation_Oirrefl(T_a,V_r_2) )
& ! [V_r_2,T_a] :
( ! [B_x] : ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_x),V_r_2)
| ~ c_Relation_Oirrefl(T_a,V_r_2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B_x,sK1_skl(T_a,V_r_2))],[f534]) ).
fof(f536,plain,
! [X0,X1,X2] :
( ~ c_Relation_Oirrefl(X0,X2)
| ~ c_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X1,X1),X2) ),
inference(cnf_transformation,[status(thm)],[f535]) ).
fof(f538,plain,
! [V_r_2,V_A_2,T_a] :
( c_Relation_Ototal__on(T_a,V_A_2,V_r_2)
<=> ! [B_x] :
( ! [B_xa] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_xa,B_x),V_r_2)
| c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_xa),V_r_2)
| B_x = B_xa
| ~ c_member(T_a,B_xa,V_A_2) )
| ~ c_member(T_a,B_x,V_A_2) ) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f539,plain,
! [V_r_2,V_A_2,T_a] :
( ( ? [B_x] :
( ? [B_xa] :
( ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_xa,B_x),V_r_2)
& ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_xa),V_r_2)
& B_x != B_xa
& c_member(T_a,B_xa,V_A_2) )
& c_member(T_a,B_x,V_A_2) )
| c_Relation_Ototal__on(T_a,V_A_2,V_r_2) )
& ( ! [B_x] :
( ! [B_xa] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_xa,B_x),V_r_2)
| c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_xa),V_r_2)
| B_x = B_xa
| ~ c_member(T_a,B_xa,V_A_2) )
| ~ c_member(T_a,B_x,V_A_2) )
| ~ c_Relation_Ototal__on(T_a,V_A_2,V_r_2) ) ),
inference(NNF_transformation,[status(thm)],[f538]) ).
fof(f540,plain,
( ! [V_r_2,V_A_2,T_a] :
( ? [B_x] :
( ? [B_xa] :
( ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_xa,B_x),V_r_2)
& ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_xa),V_r_2)
& B_x != B_xa
& c_member(T_a,B_xa,V_A_2) )
& c_member(T_a,B_x,V_A_2) )
| c_Relation_Ototal__on(T_a,V_A_2,V_r_2) )
& ! [V_r_2,V_A_2,T_a] :
( ! [B_x] :
( ! [B_xa] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_xa,B_x),V_r_2)
| c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_xa),V_r_2)
| B_x = B_xa
| ~ c_member(T_a,B_xa,V_A_2) )
| ~ c_member(T_a,B_x,V_A_2) )
| ~ c_Relation_Ototal__on(T_a,V_A_2,V_r_2) ) ),
inference(miniscoping,[status(thm)],[f539]) ).
fof(f541,plain,
( ! [V_r_2,V_A_2,T_a] :
( ( ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,sK3_skl(T_a,V_A_2,V_r_2),sK2_skl(T_a,V_A_2,V_r_2)),V_r_2)
& ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,sK2_skl(T_a,V_A_2,V_r_2),sK3_skl(T_a,V_A_2,V_r_2)),V_r_2)
& sK2_skl(T_a,V_A_2,V_r_2) != sK3_skl(T_a,V_A_2,V_r_2)
& c_member(T_a,sK3_skl(T_a,V_A_2,V_r_2),V_A_2)
& c_member(T_a,sK2_skl(T_a,V_A_2,V_r_2),V_A_2) )
| c_Relation_Ototal__on(T_a,V_A_2,V_r_2) )
& ! [V_r_2,V_A_2,T_a] :
( ! [B_x] :
( ! [B_xa] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_xa,B_x),V_r_2)
| c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_xa),V_r_2)
| B_x = B_xa
| ~ c_member(T_a,B_xa,V_A_2) )
| ~ c_member(T_a,B_x,V_A_2) )
| ~ c_Relation_Ototal__on(T_a,V_A_2,V_r_2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(B_x,sK2_skl(T_a,V_A_2,V_r_2)),skolemize(B_xa,sK3_skl(T_a,V_A_2,V_r_2))],[f540]) ).
fof(f542,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_Relation_Ototal__on(X2,X3,X4)
| ~ c_member(X2,X0,X3)
| c_member(tc_prod(X2,X2),c_Product__Type_OPair(X2,X2,X0,X1),X4)
| c_member(tc_prod(X2,X2),c_Product__Type_OPair(X2,X2,X1,X0),X4)
| ~ c_member(X2,X1,X3)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f541]) ).
fof(f548,plain,
! [V_r_2,T_a] :
( c_Relation_Otrans(T_a,V_r_2)
<=> ! [B_x,B_y] :
( ! [B_z] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_z),V_r_2)
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_y,B_z),V_r_2) )
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_y),V_r_2) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f549,plain,
! [V_r_2,T_a] :
( ( ? [B_x,B_y] :
( ? [B_z] :
( ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_z),V_r_2)
& c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_y,B_z),V_r_2) )
& c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_y),V_r_2) )
| c_Relation_Otrans(T_a,V_r_2) )
& ( ! [B_x,B_y] :
( ! [B_z] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_z),V_r_2)
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_y,B_z),V_r_2) )
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_y),V_r_2) )
| ~ c_Relation_Otrans(T_a,V_r_2) ) ),
inference(NNF_transformation,[status(thm)],[f548]) ).
fof(f550,plain,
( ! [V_r_2,T_a] :
( ? [B_x,B_y] :
( ? [B_z] :
( ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_z),V_r_2)
& c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_y,B_z),V_r_2) )
& c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_y),V_r_2) )
| c_Relation_Otrans(T_a,V_r_2) )
& ! [V_r_2,T_a] :
( ! [B_x,B_y] :
( ! [B_z] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_z),V_r_2)
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_y,B_z),V_r_2) )
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_y),V_r_2) )
| ~ c_Relation_Otrans(T_a,V_r_2) ) ),
inference(miniscoping,[status(thm)],[f549]) ).
fof(f551,plain,
( ! [V_r_2,T_a] :
( ( ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,sK4_skl(T_a,V_r_2),sK6_skl(T_a,V_r_2)),V_r_2)
& c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,sK5_skl(T_a,V_r_2),sK6_skl(T_a,V_r_2)),V_r_2)
& c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,sK4_skl(T_a,V_r_2),sK5_skl(T_a,V_r_2)),V_r_2) )
| c_Relation_Otrans(T_a,V_r_2) )
& ! [V_r_2,T_a] :
( ! [B_x,B_y] :
( ! [B_z] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_z),V_r_2)
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_y,B_z),V_r_2) )
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_y),V_r_2) )
| ~ c_Relation_Otrans(T_a,V_r_2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(B_x,sK4_skl(T_a,V_r_2)),skolemize(B_y,sK5_skl(T_a,V_r_2)),skolemize(B_z,sK6_skl(T_a,V_r_2))],[f550]) ).
fof(f552,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X1,X4),X3)
| ~ c_Relation_Otrans(X0,X3)
| ~ c_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X4,X2),X3)
| c_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X1,X2),X3) ),
inference(cnf_transformation,[status(thm)],[f551]) ).
fof(f613,plain,
! [V_A_2,V_x_2,T_a] :
( ( ~ hBOOL(hAPP(V_A_2,V_x_2))
| c_member(T_a,V_x_2,V_A_2) )
& ( hBOOL(hAPP(V_A_2,V_x_2))
| ~ c_member(T_a,V_x_2,V_A_2) ) ),
inference(NNF_transformation,[status(thm)],[f18]) ).
fof(f614,plain,
( ! [V_A_2,V_x_2] :
( ~ hBOOL(hAPP(V_A_2,V_x_2))
| ! [T_a] : c_member(T_a,V_x_2,V_A_2) )
& ! [V_A_2,V_x_2] :
( hBOOL(hAPP(V_A_2,V_x_2))
| ! [T_a] : ~ c_member(T_a,V_x_2,V_A_2) ) ),
inference(miniscoping,[status(thm)],[f613]) ).
fof(f615,plain,
! [X0,X1,X2] :
( ~ c_member(X2,X1,X0)
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f614]) ).
fof(f616,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(X2,X1))
| c_member(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f614]) ).
fof(f617,plain,
! [V_y_2,V_x_2,V_R_2,T_b,T_a] :
( ( ~ c_member(tc_prod(T_a,T_b),c_Product__Type_OPair(T_a,T_b,V_x_2,V_y_2),V_R_2)
| c_FunDef_Oin__rel(T_a,T_b,V_R_2,V_x_2,V_y_2) )
& ( c_member(tc_prod(T_a,T_b),c_Product__Type_OPair(T_a,T_b,V_x_2,V_y_2),V_R_2)
| ~ c_FunDef_Oin__rel(T_a,T_b,V_R_2,V_x_2,V_y_2) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f618,plain,
( ! [V_y_2,V_x_2,V_R_2,T_b,T_a] :
( ~ c_member(tc_prod(T_a,T_b),c_Product__Type_OPair(T_a,T_b,V_x_2,V_y_2),V_R_2)
| c_FunDef_Oin__rel(T_a,T_b,V_R_2,V_x_2,V_y_2) )
& ! [V_y_2,V_x_2,V_R_2,T_b,T_a] :
( c_member(tc_prod(T_a,T_b),c_Product__Type_OPair(T_a,T_b,V_x_2,V_y_2),V_R_2)
| ~ c_FunDef_Oin__rel(T_a,T_b,V_R_2,V_x_2,V_y_2) ) ),
inference(miniscoping,[status(thm)],[f617]) ).
fof(f619,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_FunDef_Oin__rel(X0,X1,X4,X2,X3)
| c_member(tc_prod(X0,X1),c_Product__Type_OPair(X0,X1,X2,X3),X4) ),
inference(cnf_transformation,[status(thm)],[f618]) ).
fof(f620,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_member(tc_prod(X0,X1),c_Product__Type_OPair(X0,X1,X3,X4),X2)
| c_FunDef_Oin__rel(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f618]) ).
fof(f2077,plain,
! [B_x] :
( ( c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),v_F(B_x))
& c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(B_x))
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(B_x)) )
| ? [B_xa] :
( ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(B_x,B_xa))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_x,B_xa))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_x,B_xa)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f523]) ).
fof(f2078,plain,
! [B_x] :
( ( c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),v_F(B_x))
& c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(B_x))
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(B_x)) )
| ? [B_xa] : ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(B_x,B_xa))
| ? [B_xa] : ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_x,B_xa))
| ? [B_xa] : ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_x,B_xa)) ),
inference(miniscoping,[status(thm)],[f2077]) ).
fof(f2079,plain,
! [B_x] :
( ( c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),v_F(B_x))
& c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(B_x))
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(B_x)) )
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(B_x,sK86_skl(B_x)))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_x,sK85_skl(B_x)))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_x,sK84_skl(B_x))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK84_skl,sK85_skl,sK86_skl]),skolemize(B_xa,sK84_skl(B_x)),skolemize(B_xa,sK85_skl(B_x)),skolemize(B_xa,sK86_skl(B_x))],[f2078]) ).
fof(f2080,plain,
! [X0] :
( ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(X0,sK84_skl(X0)))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(X0,sK85_skl(X0)))
| c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(X0))
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(X0,sK86_skl(X0))) ),
inference(cnf_transformation,[status(thm)],[f2079]) ).
fof(f2081,plain,
! [X0] :
( c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(X0))
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(X0,sK86_skl(X0)))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(X0,sK85_skl(X0)))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(X0,sK84_skl(X0))) ),
inference(cnf_transformation,[status(thm)],[f2079]) ).
fof(f2083,plain,
! [B_P] :
( ! [B_a,B_b] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),v_F(B_P))
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_P,v_i))
| B_a = B_b )
| ? [B_x] :
( ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(B_P,B_x))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_P,B_x))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_P,B_x)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f524]) ).
fof(f2084,plain,
! [B_P] :
( ! [B_a,B_b] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),v_F(B_P))
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_P,v_i))
| B_a = B_b )
| ? [B_x] : ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(B_P,B_x))
| ? [B_x] : ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_P,B_x))
| ? [B_x] : ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_P,B_x)) ),
inference(miniscoping,[status(thm)],[f2083]) ).
fof(f2085,plain,
! [B_P] :
( ! [B_a,B_b] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),v_F(B_P))
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_P,v_i))
| B_a = B_b )
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(B_P,sK89_skl(B_P)))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_P,sK88_skl(B_P)))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_P,sK87_skl(B_P))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87_skl,sK88_skl,sK89_skl]),skolemize(B_x,sK87_skl(B_P)),skolemize(B_x,sK88_skl(B_P)),skolemize(B_x,sK89_skl(B_P))],[f2084]) ).
fof(f2086,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(X0,sK89_skl(X0)))
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_F(X0))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(X0,sK87_skl(X0)))
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),hAPP(X0,v_i))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(X0,sK88_skl(X0))) ),
inference(cnf_transformation,[status(thm)],[f2085]) ).
fof(f2087,plain,
( ! [B_x] : c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(v_P,B_x))
& ! [B_x] : c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,B_x))
& ! [B_x] : c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,B_x)) ),
inference(miniscoping,[status(thm)],[f525]) ).
fof(f2088,plain,
! [X0] : c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,X0)),
inference(cnf_transformation,[status(thm)],[f2087]) ).
fof(f2089,plain,
! [X0] : c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,X0)),
inference(cnf_transformation,[status(thm)],[f2087]) ).
fof(f2090,plain,
! [X0] : c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(v_P,X0)),
inference(cnf_transformation,[status(thm)],[f2087]) ).
fof(f2091,plain,
c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_b),v_F(v_P)),
inference(cnf_transformation,[status(thm)],[f526]) ).
fof(f2092,plain,
~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_b),hAPP(v_P,v_i)),
inference(cnf_transformation,[status(thm)],[f528]) ).
fof(f2279,plain,
( ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK84_skl(v_P)))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK85_skl(v_P)))
| c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) ),
inference(resolution,[status(thm)],[f2080,f2090]) ).
fof(f2280,plain,
( ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK84_skl(v_P)))
| c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2279,f2089]) ).
fof(f2283,plain,
! [X0,X1,X2,X3] :
( ~ c_member(X3,X1,X2)
| c_member(X0,X1,X2) ),
inference(resolution,[status(thm)],[f616,f615]) ).
fof(f2284,plain,
c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)),
inference(forward_subsumption_resolution,[status(thm)],[f2280,f2088]) ).
fof(f2286,plain,
! [X0] : c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_b),v_F(v_P)),
inference(resolution,[status(thm)],[f2283,f2091]) ).
fof(f2300,plain,
! [X0,X1,X2] : c_member(X0,X1,c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool))),
inference(resolution,[status(thm)],[f532,f2283]) ).
fof(f2579,plain,
( c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK85_skl(v_P)))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK84_skl(v_P))) ),
inference(resolution,[status(thm)],[f2081,f2090]) ).
fof(f2580,plain,
( c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK85_skl(v_P))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2579,f2088]) ).
fof(f2581,plain,
c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)),
inference(forward_subsumption_resolution,[status(thm)],[f2580,f2089]) ).
fof(f2773,plain,
! [X0,X1,X2] :
( ~ c_Relation_Oirrefl(X0,X1)
| ~ c_FunDef_Oin__rel(X0,X0,X1,X2,X2) ),
inference(resolution,[status(thm)],[f536,f619]) ).
fof(f2781,plain,
! [X0] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b,v_a),hAPP(v_P,v_i))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,hAPP(v_P,v_i))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0)
| v_a = v_b ),
inference(resolution,[status(thm)],[f542,f2092]) ).
fof(f2799,plain,
! [X0] :
( v_b = v_a
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(v_P,sK89_skl(v_P)))
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b,v_a),v_F(v_P))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK87_skl(v_P)))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK88_skl(v_P)))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,hAPP(v_P,v_i))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0)
| v_a = v_b ),
inference(resolution,[status(thm)],[f2781,f2086]) ).
fof(f2803,plain,
! [X0] :
( ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(v_P,sK89_skl(v_P)))
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b,v_a),v_F(v_P))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK87_skl(v_P)))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK88_skl(v_P)))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,hAPP(v_P,v_i))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0)
| v_a = v_b ),
inference(duplicate_literals_removal,[status(thm)],[f2799]) ).
fof(f2804,plain,
! [X0] :
( ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(v_P,sK89_skl(v_P)))
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,hAPP(v_P,v_i))
| v_b = v_a
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b,v_a),v_F(v_P))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK87_skl(v_P)))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2803,f2089]) ).
fof(f2815,plain,
! [X0] :
( ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,hAPP(v_P,v_i))
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b,v_a),v_F(v_P))
| v_b = v_a
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(v_P,sK89_skl(v_P)))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2804,f2088]) ).
fof(f2818,plain,
! [X0,X1] :
( c_member(X1,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b,v_a),v_F(v_P))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,hAPP(v_P,v_i))
| v_b = v_a
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)),hAPP(v_P,sK89_skl(v_P)))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0) ),
inference(resolution,[status(thm)],[f2815,f2283]) ).
fof(f2820,plain,
! [X0,X1] :
( ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0)
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| c_member(X1,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b,v_a),v_F(v_P))
| v_b = v_a
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,hAPP(v_P,v_i)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2818,f2090]) ).
fof(f2905,plain,
! [X0] :
( ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0)
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,hAPP(v_P,v_i))
| v_b = v_a
| c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P),v_b,v_a) ),
inference(resolution,[status(thm)],[f620,f2820]) ).
fof(f2907,plain,
c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P),v_a,v_b),
inference(resolution,[status(thm)],[f620,f2286]) ).
fof(f3714,plain,
! [X0] :
( ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b,X0),v_F(v_P))
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,X0),v_F(v_P)) ),
inference(resolution,[status(thm)],[f552,f2286]) ).
fof(f3731,plain,
! [X0] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,X0),v_F(v_P))
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b,X0),v_F(v_P)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3714,f2284]) ).
fof(f3785,plain,
! [X0] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,X0),v_F(v_P))
| ~ c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P),v_b,X0) ),
inference(resolution,[status(thm)],[f3731,f619]) ).
fof(f3794,plain,
( ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))
| ~ c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P),v_b,v_a) ),
inference(resolution,[status(thm)],[f3785,f536]) ).
fof(f3798,plain,
~ c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P),v_b,v_a),
inference(forward_subsumption_resolution,[status(thm)],[f3794,f2581]) ).
fof(f3801,plain,
! [X0] :
( v_b = v_a
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0)
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,hAPP(v_P,v_i)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2905,f3798]) ).
fof(f3856,plain,
( v_b = v_a
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
inference(resolution,[status(thm)],[f3801,f2090]) ).
fof(f3859,plain,
( ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)))
| v_a = v_b ),
inference(forward_subsumption_resolution,[status(thm)],[f3856,f2300]) ).
fof(f3866,plain,
c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P),v_a,v_a),
inference(backward_demodulation,[status(thm)],[f3871,f2907]) ).
fof(f3871,plain,
v_a = v_b,
inference(forward_subsumption_resolution,[status(thm)],[f3859,f2300]) ).
fof(f3872,plain,
~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)),
inference(resolution,[status(thm)],[f3866,f2773]) ).
fof(f3873,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f3872,f2581]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT120+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n001.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 04:38:28 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.29/0.58 % Drodi V4.1.1
% 61.32/8.76 % Refutation found
% 61.32/8.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 61.32/8.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 48.20/8.86 % Elapsed time: 8.388029 seconds
% 48.20/8.86 % CPU time: 65.052867 seconds
% 48.20/8.86 % Total memory used: 368.926 MB
% 48.20/8.86 % Net memory used: 337.062 MB
%------------------------------------------------------------------------------