%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SCT121+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 177.94s 23.27s
% Output : CNFRefutation 177.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 76
% Syntax : Number of formulae : 314 ( 85 unt; 47 def)
% Number of atoms : 721 ( 63 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 721 ( 314 ~; 295 |; 45 &)
% ( 54 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 66 ( 64 usr; 48 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 9 con; 0-4 aty)
% Number of variables : 357 ( 340 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [V_g_2,V_f_2] :
( ! [B_x] : hAPP(V_f_2,B_x) = hAPP(V_g_2,B_x)
=> V_f_2 = V_g_2 ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [V_c_2,V_b_2,V_a_2,V_r_2,T_a] :
( c_Relation_Otrans(T_a,V_r_2)
=> ( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_a_2,V_b_2),V_r_2)
=> ( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_b_2,V_c_2),V_r_2)
=> c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_a_2,V_c_2),V_r_2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [V_x_2,T_a] : hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool)),V_x_2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [V_y_2,V_x_2,T_a] :
( c_member(T_a,V_x_2,c_fequal(V_y_2))
<=> V_x_2 = V_y_2 ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [V_y_2,V_x_2,V_r_2,V_A_2,T_a] :
( c_Relation_Orefl__on(T_a,V_A_2,V_r_2)
=> ( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_x_2,V_y_2),V_r_2)
=> c_member(T_a,V_x_2,V_A_2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [V_r_2,V_a_2,T_a] : c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_a_2,V_a_2),c_Transitive__Closure_Ortrancl(T_a,V_r_2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [V_r_2,T_a] : c_Relation_Orefl__on(T_a,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool)),c_Transitive__Closure_Ortrancl(T_a,V_r_2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f202,axiom,
! [V_x_2,V_A_2,V_y_2,T_a] :
( hBOOL(hAPP(c_Set_Oinsert(T_a,V_y_2,V_A_2),V_x_2))
<=> ( hBOOL(hAPP(V_A_2,V_x_2))
| V_y_2 = V_x_2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f289,axiom,
! [V_A_2,T_a] :
( ! [B_x] : ~ c_member(T_a,B_x,V_A_2)
<=> V_A_2 = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f313,axiom,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f495,axiom,
class_Lattices_Obounded__lattice(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f509,axiom,
class_Lattices_Obounded__lattice__top(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f510,axiom,
class_Lattices_Obounded__lattice__bot(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f511,axiom,
class_Lattices_Osemilattice__sup(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f512,axiom,
class_Lattices_Osemilattice__inf(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f513,axiom,
class_Lattices_Odistrib__lattice(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f514,axiom,
class_Orderings_Opreorder(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f516,axiom,
class_Orderings_Oorder(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f518,axiom,
class_Orderings_Oord(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f519,axiom,
class_Orderings_Obot(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f520,axiom,
class_Groups_Ominus(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f523,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/sandbox/benchmark/theBenchmark.p') ).
fof(f524,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/sandbox/benchmark/theBenchmark.p') ).
fof(f525,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/sandbox/benchmark/theBenchmark.p') ).
fof(f526,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)) )
=> ( 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(v_P))
& c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) ) ),
file('/export/starexec/sandbox/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/sandbox/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(f529,plain,
! [V_g_2,V_f_2] :
( V_f_2 = V_g_2
| ? [B_x] : hAPP(V_f_2,B_x) != hAPP(V_g_2,B_x) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f530,plain,
! [V_g_2,V_f_2] :
( V_f_2 = V_g_2
| hAPP(V_f_2,sK0_skl(V_f_2,V_g_2)) != hAPP(V_g_2,sK0_skl(V_f_2,V_g_2)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B_x,sK0_skl(V_f_2,V_g_2))],[f529]) ).
fof(f531,plain,
! [X0,X1] :
( X0 = X1
| hAPP(X0,sK0_skl(X0,X1)) != hAPP(X1,sK0_skl(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f530]) ).
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_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X2,X2),X1)
| ~ c_Relation_Oirrefl(X0,X1) ),
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_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X4,X3),X2)
| ~ c_member(X0,X4,X1)
| c_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X3,X4),X2)
| ~ c_member(X0,X3,X1)
| X3 = X4
| ~ c_Relation_Ototal__on(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f541]) ).
fof(f543,plain,
! [X0,X1,X2] :
( c_member(X0,sK2_skl(X0,X1,X2),X1)
| c_Relation_Ototal__on(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f541]) ).
fof(f544,plain,
! [X0,X1,X2] :
( c_member(X0,sK3_skl(X0,X1,X2),X1)
| c_Relation_Ototal__on(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f541]) ).
fof(f545,plain,
! [X0,X1,X2] :
( c_Relation_Ototal__on(X0,X1,X2)
| sK2_skl(X0,X1,X2) != sK3_skl(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f541]) ).
fof(f556,plain,
! [V_c_2,V_b_2,V_a_2,V_r_2,T_a] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_a_2,V_c_2),V_r_2)
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_b_2,V_c_2),V_r_2)
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_a_2,V_b_2),V_r_2)
| ~ c_Relation_Otrans(T_a,V_r_2) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f557,plain,
! [V_r_2,T_a] :
( ! [V_b_2,V_a_2] :
( ! [V_c_2] :
( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_a_2,V_c_2),V_r_2)
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_b_2,V_c_2),V_r_2) )
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_a_2,V_b_2),V_r_2) )
| ~ c_Relation_Otrans(T_a,V_r_2) ),
inference(miniscoping,[status(thm)],[f556]) ).
fof(f558,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X4,X2),X1)
| c_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X4,X3),X1)
| ~ c_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X2,X3),X1)
| ~ c_Relation_Otrans(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f557]) ).
fof(f559,plain,
! [X0,X1] : hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)),X1)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f609,plain,
! [V_y_2,V_x_2,T_a] :
( ( V_x_2 != V_y_2
| c_member(T_a,V_x_2,c_fequal(V_y_2)) )
& ( V_x_2 = V_y_2
| ~ c_member(T_a,V_x_2,c_fequal(V_y_2)) ) ),
inference(NNF_transformation,[status(thm)],[f17]) ).
fof(f610,plain,
( ! [V_y_2,V_x_2] :
( V_x_2 != V_y_2
| ! [T_a] : c_member(T_a,V_x_2,c_fequal(V_y_2)) )
& ! [V_y_2,V_x_2] :
( V_x_2 = V_y_2
| ! [T_a] : ~ c_member(T_a,V_x_2,c_fequal(V_y_2)) ) ),
inference(miniscoping,[status(thm)],[f609]) ).
fof(f611,plain,
! [X0,X1,X2] :
( ~ c_member(X2,X0,c_fequal(X1))
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f610]) ).
fof(f612,plain,
! [X0,X1,X2] :
( X1 != X2
| c_member(X0,X1,c_fequal(X2)) ),
inference(cnf_transformation,[status(thm)],[f610]) ).
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(f749,plain,
! [V_y_2,V_x_2,V_r_2,V_A_2,T_a] :
( c_member(T_a,V_x_2,V_A_2)
| ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_x_2,V_y_2),V_r_2)
| ~ c_Relation_Orefl__on(T_a,V_A_2,V_r_2) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f750,plain,
! [V_r_2,V_A_2,T_a] :
( ! [V_x_2] :
( c_member(T_a,V_x_2,V_A_2)
| ! [V_y_2] : ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,V_x_2,V_y_2),V_r_2) )
| ~ c_Relation_Orefl__on(T_a,V_A_2,V_r_2) ),
inference(miniscoping,[status(thm)],[f749]) ).
fof(f751,plain,
! [X0,X1,X2,X3,X4] :
( c_member(X0,X1,X4)
| ~ c_Relation_Orefl__on(X0,X4,X3)
| ~ c_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X1,X2),X3) ),
inference(cnf_transformation,[status(thm)],[f750]) ).
fof(f848,plain,
! [X0,X1,X2] : c_member(tc_prod(X0,X0),c_Product__Type_OPair(X0,X0,X1,X1),c_Transitive__Closure_Ortrancl(X0,X2)),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f859,plain,
! [X0,X1] : c_Relation_Orefl__on(X0,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)),c_Transitive__Closure_Ortrancl(X0,X1)),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f1222,plain,
! [V_x_2,V_A_2,V_y_2,T_a] :
( ( ( ~ hBOOL(hAPP(V_A_2,V_x_2))
& V_y_2 != V_x_2 )
| hBOOL(hAPP(c_Set_Oinsert(T_a,V_y_2,V_A_2),V_x_2)) )
& ( hBOOL(hAPP(V_A_2,V_x_2))
| V_y_2 = V_x_2
| ~ hBOOL(hAPP(c_Set_Oinsert(T_a,V_y_2,V_A_2),V_x_2)) ) ),
inference(NNF_transformation,[status(thm)],[f202]) ).
fof(f1223,plain,
( ! [V_x_2,V_A_2,V_y_2] :
( ( ~ hBOOL(hAPP(V_A_2,V_x_2))
& V_y_2 != V_x_2 )
| ! [T_a] : hBOOL(hAPP(c_Set_Oinsert(T_a,V_y_2,V_A_2),V_x_2)) )
& ! [V_x_2,V_A_2,V_y_2] :
( hBOOL(hAPP(V_A_2,V_x_2))
| V_y_2 = V_x_2
| ! [T_a] : ~ hBOOL(hAPP(c_Set_Oinsert(T_a,V_y_2,V_A_2),V_x_2)) ) ),
inference(miniscoping,[status(thm)],[f1222]) ).
fof(f1225,plain,
! [X0,X1,X2,X3] :
( X1 != X3
| hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X3)) ),
inference(cnf_transformation,[status(thm)],[f1223]) ).
fof(f1454,plain,
! [V_A_2,T_a] :
( ( V_A_2 != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))
| ! [B_x] : ~ c_member(T_a,B_x,V_A_2) )
& ( V_A_2 = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))
| ? [B_x] : c_member(T_a,B_x,V_A_2) ) ),
inference(NNF_transformation,[status(thm)],[f289]) ).
fof(f1455,plain,
( ! [V_A_2,T_a] :
( V_A_2 != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))
| ! [B_x] : ~ c_member(T_a,B_x,V_A_2) )
& ! [V_A_2,T_a] :
( V_A_2 = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))
| ? [B_x] : c_member(T_a,B_x,V_A_2) ) ),
inference(miniscoping,[status(thm)],[f1454]) ).
fof(f1456,plain,
( ! [V_A_2,T_a] :
( V_A_2 != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))
| ! [B_x] : ~ c_member(T_a,B_x,V_A_2) )
& ! [V_A_2,T_a] :
( V_A_2 = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))
| c_member(T_a,sK72_skl(T_a,V_A_2),V_A_2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72_skl]),skolemize(B_x,sK72_skl(T_a,V_A_2))],[f1455]) ).
fof(f1458,plain,
! [X0,X1,X2] :
( X2 != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))
| ~ c_member(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1456]) ).
fof(f1517,plain,
! [X0] : c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)),
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f2023,plain,
class_Lattices_Obounded__lattice(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f495]) ).
fof(f2063,plain,
class_Lattices_Obounded__lattice__top(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f509]) ).
fof(f2064,plain,
class_Lattices_Obounded__lattice__bot(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f510]) ).
fof(f2065,plain,
class_Lattices_Osemilattice__sup(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f511]) ).
fof(f2066,plain,
class_Lattices_Osemilattice__inf(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f512]) ).
fof(f2067,plain,
class_Lattices_Odistrib__lattice(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f513]) ).
fof(f2068,plain,
class_Orderings_Opreorder(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f514]) ).
fof(f2070,plain,
class_Orderings_Oorder(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f2072,plain,
class_Orderings_Oord(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f518]) ).
fof(f2073,plain,
class_Orderings_Obot(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f519]) ).
fof(f2074,plain,
class_Groups_Ominus(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f520]) ).
fof(f2077,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)],[f523]) ).
fof(f2078,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)],[f2077]) ).
fof(f2079,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,sK86_skl(B_P)))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_P,sK85_skl(B_P)))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(B_P,sK84_skl(B_P))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK84_skl,sK85_skl,sK86_skl]),skolemize(B_x,sK84_skl(B_P)),skolemize(B_x,sK85_skl(B_P)),skolemize(B_x,sK86_skl(B_P))],[f2078]) ).
fof(f2080,plain,
! [X0,X1,X2] :
( ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(X2,sK84_skl(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(X2,sK86_skl(X2)))
| X0 = X1
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(X2,sK85_skl(X2)))
| 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,X0,X1),v_F(X2))
| ~ 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,X0,X1),hAPP(X2,v_i)) ),
inference(cnf_transformation,[status(thm)],[f2079]) ).
fof(f2081,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)],[f524]) ).
fof(f2082,plain,
! [X0] : c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,X0)),
inference(cnf_transformation,[status(thm)],[f2081]) ).
fof(f2083,plain,
! [X0] : c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,X0)),
inference(cnf_transformation,[status(thm)],[f2081]) ).
fof(f2084,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)],[f2081]) ).
fof(f2085,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)],[f525]) ).
fof(f2086,plain,
( ( 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(v_P))
& c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_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(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)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f526]) ).
fof(f2087,plain,
( ( 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(v_P))
& c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_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(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)],[f2086]) ).
fof(f2088,plain,
( ( 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(v_P))
& c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) )
| ~ 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))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK88_skl))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK87_skl)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87_skl,sK88_skl,sK89_skl]),skolemize(B_x,sK87_skl),skolemize(B_x,sK88_skl),skolemize(B_x,sK89_skl)],[f2087]) ).
fof(f2089,plain,
( c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))
| ~ 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))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK88_skl))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK87_skl)) ),
inference(cnf_transformation,[status(thm)],[f2088]) ).
fof(f2090,plain,
( c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))
| ~ 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))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK88_skl))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK87_skl)) ),
inference(cnf_transformation,[status(thm)],[f2088]) ).
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(f2112,definition,
( sQ0_spl
<=> c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK87_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f2114,plain,
( sQ0_spl
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK87_skl)) ),
inference(component_clause,[status(thm)],[f2112]) ).
fof(f2115,definition,
( sQ1_spl
<=> c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK88_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f2117,plain,
( sQ1_spl
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK88_skl)) ),
inference(component_clause,[status(thm)],[f2115]) ).
fof(f2118,definition,
( sQ2_spl
<=> 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)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f2120,plain,
( sQ2_spl
| ~ 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)) ),
inference(component_clause,[status(thm)],[f2118]) ).
fof(f2121,definition,
( sQ3_spl
<=> c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f2124,plain,
( sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f2089,f2112,f2115,f2118,f2121]) ).
fof(f2125,definition,
( sQ4_spl
<=> c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f2126,plain,
( ~ sQ4_spl
| c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) ),
inference(component_clause,[status(thm)],[f2125]) ).
fof(f2128,plain,
( sQ4_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f2090,f2112,f2115,f2118,f2125]) ).
fof(f2185,plain,
! [X0,X1] : ~ c_member(X0,X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))),
inference(destructive_equality_resolution,[status(thm)],[f1458]) ).
fof(f2189,plain,
! [X0,X1,X2] : hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X1)),
inference(destructive_equality_resolution,[status(thm)],[f1225]) ).
fof(f2205,plain,
! [X0,X1] : c_member(X0,X1,c_fequal(X1)),
inference(destructive_equality_resolution,[status(thm)],[f612]) ).
fof(f2316,plain,
! [X0,X1,X2] :
( sK2_skl(X0,c_fequal(X1),X2) = X1
| c_Relation_Ototal__on(X0,c_fequal(X1),X2) ),
inference(resolution,[status(thm)],[f611,f543]) ).
fof(f2366,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2120,f2084]) ).
fof(f2367,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f2366]) ).
fof(f2368,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2117,f2083]) ).
fof(f2369,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f2368]) ).
fof(f2370,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2114,f2082]) ).
fof(f2371,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f2370]) ).
fof(f2438,plain,
! [X0,X1,X2,X3] : c_member(X0,X1,c_Set_Oinsert(X2,X1,X3)),
inference(resolution,[status(thm)],[f616,f2189]) ).
fof(f2440,plain,
! [X0,X1,X2] : c_member(X0,X1,c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool))),
inference(resolution,[status(thm)],[f616,f559]) ).
fof(f2450,plain,
! [X0,X1,X2,X3] :
( c_member(X3,X1,X2)
| ~ c_member(X0,X1,X2) ),
inference(resolution,[status(thm)],[f615,f616]) ).
fof(f2452,plain,
! [X0] : ~ c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_b),hAPP(v_P,v_i)),
inference(resolution,[status(thm)],[f2450,f2092]) ).
fof(f2459,plain,
! [X0,X1,X2,X3] :
( ~ c_Relation_Oirrefl(X1,X3)
| ~ c_member(X0,c_Product__Type_OPair(X1,X1,X2,X2),X3) ),
inference(resolution,[status(thm)],[f2450,f536]) ).
fof(f2477,plain,
! [X0,X1,X2] : ~ c_member(X0,X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool))),
inference(resolution,[status(thm)],[f2185,f2450]) ).
fof(f2622,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,X0,v_b),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,X0,v_a),v_F(v_P)) ),
inference(resolution,[status(thm)],[f558,f2085]) ).
fof(f2668,definition,
! [X0] :
( sQ17_spl
<=> ( 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,X0,v_b),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,X0,v_a),v_F(v_P)) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f2669,plain,
! [X0] :
( ~ sQ17_spl
| 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,X0,v_b),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,X0,v_a),v_F(v_P)) ),
inference(component_clause,[status(thm)],[f2668]) ).
fof(f2671,plain,
( ~ sQ3_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f2622,f2668,f2121]) ).
fof(f2687,plain,
( ~ sQ17_spl
| ~ c_Relation_Oirrefl(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,v_a),v_F(v_P)) ),
inference(resolution,[status(thm)],[f2669,f536]) ).
fof(f2696,definition,
( sQ22_spl
<=> 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)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f2699,plain,
( ~ sQ17_spl
| ~ sQ4_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f2687,f2696,f2125,f2668]) ).
fof(f3318,definition,
! [X1] :
( sQ91_spl
<=> ~ c_member(X1,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_a),v_F(v_P)) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f3319,plain,
! [X0] :
( ~ sQ91_spl
| ~ c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_a),v_F(v_P)) ),
inference(component_clause,[status(thm)],[f3318]) ).
fof(f4362,plain,
! [X0,X1,X2] :
( c_Relation_Ototal__on(X1,c_fequal(X0),X2)
| X0 = sK3_skl(X1,c_fequal(X0),X2) ),
inference(resolution,[status(thm)],[f544,f611]) ).
fof(f4915,definition,
( sQ248_spl
<=> c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK84_skl(v_P))) ),
introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition]) ).
fof(f4917,plain,
( sQ248_spl
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK84_skl(v_P))) ),
inference(component_clause,[status(thm)],[f4915]) ).
fof(f4918,definition,
( sQ249_spl
<=> 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,sK86_skl(v_P))) ),
introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition]) ).
fof(f4920,plain,
( sQ249_spl
| ~ 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,sK86_skl(v_P))) ),
inference(component_clause,[status(thm)],[f4918]) ).
fof(f4924,definition,
( sQ251_spl
<=> c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK85_skl(v_P))) ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f4926,plain,
( sQ251_spl
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK85_skl(v_P))) ),
inference(component_clause,[status(thm)],[f4924]) ).
fof(f4941,plain,
( sQ248_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4917,f2082]) ).
fof(f4942,plain,
sQ248_spl,
inference(contradiction_clause,[status(thm)],[f4941]) ).
fof(f4943,plain,
( sQ251_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4926,f2083]) ).
fof(f4944,plain,
sQ251_spl,
inference(contradiction_clause,[status(thm)],[f4943]) ).
fof(f4946,plain,
( sQ249_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4920,f2084]) ).
fof(f4947,plain,
sQ249_spl,
inference(contradiction_clause,[status(thm)],[f4946]) ).
fof(f5198,definition,
( sQ258_spl
<=> 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_a),v_F(v_P)) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f5199,plain,
( ~ sQ258_spl
| 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_a),v_F(v_P)) ),
inference(component_clause,[status(thm)],[f5198]) ).
fof(f5200,plain,
( sQ258_spl
| ~ 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_a),v_F(v_P)) ),
inference(component_clause,[status(thm)],[f5198]) ).
fof(f5681,plain,
! [X0] :
( sQ258_spl
| ~ c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_a),v_F(v_P)) ),
inference(resolution,[status(thm)],[f5200,f2450]) ).
fof(f5794,definition,
( sQ292_spl
<=> v_b = v_a ),
introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition]) ).
fof(f5795,plain,
( ~ sQ292_spl
| v_b = v_a ),
inference(component_clause,[status(thm)],[f5794]) ).
fof(f5959,plain,
( ~ sQ292_spl
| 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_a),v_F(v_P)) ),
inference(backward_demodulation,[status(thm)],[f5795,f2085]) ).
fof(f7414,plain,
! [X0,X1,X2] :
( c_Relation_Ototal__on(X0,c_fequal(X1),X2)
| sK2_skl(X0,c_fequal(X1),X2) != X1
| c_Relation_Ototal__on(X0,c_fequal(X1),X2) ),
inference(paramodulation,[status(thm)],[f4362,f545]) ).
fof(f7418,plain,
! [X0,X1,X2] :
( sK2_skl(X0,c_fequal(X1),X2) != X1
| c_Relation_Ototal__on(X0,c_fequal(X1),X2) ),
inference(duplicate_literals_removal,[status(thm)],[f7414]) ).
fof(f7419,plain,
! [X0,X1,X2] : c_Relation_Ototal__on(X0,c_fequal(X1),X2),
inference(forward_subsumption_resolution,[status(thm)],[f7418,f2316]) ).
fof(f10847,plain,
( ~ sQ292_spl
| ~ sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5959,f3319]) ).
fof(f10848,plain,
( ~ sQ292_spl
| ~ sQ91_spl ),
inference(contradiction_clause,[status(thm)],[f10847]) ).
fof(f10849,plain,
( sQ258_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f5681,f3318,f5198]) ).
fof(f12397,plain,
! [X0,X1,X2,X3] :
( ~ c_Relation_Orefl__on(X0,X2,c_Transitive__Closure_Ortrancl(X0,X3))
| c_member(X0,X1,X2) ),
inference(resolution,[status(thm)],[f848,f751]) ).
fof(f12888,definition,
( sQ577_spl
<=> 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)) ),
introduced(definition,[new_symbols(definition,[sQ577_spl])],[split_symbol_definition]) ).
fof(f12889,plain,
( ~ sQ577_spl
| 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)) ),
inference(component_clause,[status(thm)],[f12888]) ).
fof(f13842,plain,
! [X0] :
( ~ 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_a,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) ),
inference(resolution,[status(thm)],[f542,f2452]) ).
fof(f13869,definition,
! [X0] :
( sQ611_spl
<=> ( ~ 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)
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ611_spl])],[split_symbol_definition]) ).
fof(f13870,plain,
! [X0] :
( ~ sQ611_spl
| ~ 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(component_clause,[status(thm)],[f13869]) ).
fof(f13872,plain,
( sQ292_spl
| sQ577_spl
| sQ611_spl ),
inference(split_clause,[status(thm)],[f13842,f13869,f12888,f5794]) ).
fof(f13879,definition,
! [X0] :
( sQ613_spl
<=> ( ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,v_F(v_P))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition]) ).
fof(f13880,plain,
! [X0] :
( ~ sQ613_spl
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,v_F(v_P))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0) ),
inference(component_clause,[status(thm)],[f13879]) ).
fof(f13927,definition,
! [X0] :
( sQ625_spl
<=> ( ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,hAPP(v_P,v_i))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,sK11_skl(tc_Arrow__Order__Mirabelle_Oalt,v_a,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i)),X0)
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ625_spl])],[split_symbol_definition]) ).
fof(f13928,plain,
! [X0] :
( ~ sQ625_spl
| ~ 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,sK11_skl(tc_Arrow__Order__Mirabelle_Oalt,v_a,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i)),X0) ),
inference(component_clause,[status(thm)],[f13927]) ).
fof(f13935,definition,
! [X0] :
( sQ627_spl
<=> ( ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,v_F(v_P))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0)
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ627_spl])],[split_symbol_definition]) ).
fof(f13936,plain,
! [X0] :
( ~ sQ627_spl
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,v_F(v_P))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0)
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0) ),
inference(component_clause,[status(thm)],[f13935]) ).
fof(f13954,plain,
! [X0] :
( ~ sQ627_spl
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,v_F(v_P))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f13936]) ).
fof(f13955,plain,
! [X0] :
( ~ sQ613_spl
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,X0)
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,X0,v_F(v_P)) ),
inference(duplicate_literals_removal,[status(thm)],[f13880]) ).
fof(f14010,plain,
( ~ sQ611_spl
| ~ 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)],[f13870,f2084]) ).
fof(f14015,definition,
( sQ631_spl
<=> c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition]) ).
fof(f14017,plain,
( sQ631_spl
| ~ 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(component_clause,[status(thm)],[f14015]) ).
fof(f14018,definition,
( sQ632_spl
<=> c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
introduced(definition,[new_symbols(definition,[sQ632_spl])],[split_symbol_definition]) ).
fof(f14020,plain,
( sQ632_spl
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
inference(component_clause,[status(thm)],[f14018]) ).
fof(f14021,plain,
( ~ sQ611_spl
| ~ sQ632_spl
| ~ sQ631_spl ),
inference(split_clause,[status(thm)],[f14010,f14015,f14018,f13869]) ).
fof(f14022,plain,
( sQ631_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14017,f2440]) ).
fof(f14023,plain,
sQ631_spl,
inference(contradiction_clause,[status(thm)],[f14022]) ).
fof(f14024,plain,
( sQ632_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14020,f2440]) ).
fof(f14025,plain,
sQ632_spl,
inference(contradiction_clause,[status(thm)],[f14024]) ).
fof(f14188,plain,
! [X0] :
( ~ sQ627_spl
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,c_fequal(X0)) ),
inference(resolution,[status(thm)],[f13954,f7419]) ).
fof(f14190,plain,
( ~ sQ627_spl
| $false ),
inference(resolution,[status(thm)],[f14188,f2205]) ).
fof(f14192,plain,
~ sQ627_spl,
inference(contradiction_clause,[status(thm)],[f14190]) ).
fof(f14197,plain,
! [X0] :
( ~ sQ613_spl
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,c_fequal(X0)) ),
inference(resolution,[status(thm)],[f13955,f7419]) ).
fof(f14262,plain,
( ~ sQ613_spl
| $false ),
inference(resolution,[status(thm)],[f14197,f2205]) ).
fof(f14264,plain,
~ sQ613_spl,
inference(contradiction_clause,[status(thm)],[f14262]) ).
fof(f14318,definition,
( sQ643_spl
<=> c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i)) ),
introduced(definition,[new_symbols(definition,[sQ643_spl])],[split_symbol_definition]) ).
fof(f14320,plain,
( sQ643_spl
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i)) ),
inference(component_clause,[status(thm)],[f14318]) ).
fof(f15184,definition,
! [X0] :
( sQ665_spl
<=> ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,c_Set_Oinsert(tc_Arrow__Order__Mirabelle_Oalt,X0,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)))) ),
introduced(definition,[new_symbols(definition,[sQ665_spl])],[split_symbol_definition]) ).
fof(f15185,plain,
! [X0] :
( ~ sQ665_spl
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,c_Set_Oinsert(tc_Arrow__Order__Mirabelle_Oalt,X0,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)))) ),
inference(component_clause,[status(thm)],[f15184]) ).
fof(f15211,plain,
( ~ sQ665_spl
| $false ),
inference(resolution,[status(thm)],[f15185,f2438]) ).
fof(f15215,plain,
~ sQ665_spl,
inference(contradiction_clause,[status(thm)],[f15211]) ).
fof(f15272,definition,
! [X1,X2] :
( sQ667_spl
<=> c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) = X2 ),
introduced(definition,[new_symbols(definition,[sQ667_spl])],[split_symbol_definition]) ).
fof(f15273,plain,
! [X0,X1] :
( ~ sQ667_spl
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)) = X1 ),
inference(component_clause,[status(thm)],[f15272]) ).
fof(f15303,plain,
( ~ sQ667_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1517,f15273]) ).
fof(f15356,plain,
~ sQ667_spl,
inference(contradiction_clause,[status(thm)],[f15303]) ).
fof(f15619,definition,
( sQ677_spl
<=> class_Orderings_Obot(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ677_spl])],[split_symbol_definition]) ).
fof(f15621,plain,
( sQ677_spl
| ~ class_Orderings_Obot(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f15619]) ).
fof(f15627,plain,
( sQ677_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15621,f2073]) ).
fof(f15628,plain,
sQ677_spl,
inference(contradiction_clause,[status(thm)],[f15627]) ).
fof(f15665,definition,
! [X0,X1,X2] :
( sQ683_spl
<=> c_member(X0,X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool))) ),
introduced(definition,[new_symbols(definition,[sQ683_spl])],[split_symbol_definition]) ).
fof(f15666,plain,
! [X0,X1,X2] :
( ~ sQ683_spl
| c_member(X0,X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool))) ),
inference(component_clause,[status(thm)],[f15665]) ).
fof(f15683,plain,
( ~ sQ683_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15666,f2477]) ).
fof(f15684,plain,
~ sQ683_spl,
inference(contradiction_clause,[status(thm)],[f15683]) ).
fof(f16236,plain,
( sQ643_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14320,f2083]) ).
fof(f16237,plain,
sQ643_spl,
inference(contradiction_clause,[status(thm)],[f16236]) ).
fof(f16719,definition,
( sQ702_spl
<=> class_Lattices_Osemilattice__inf(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ702_spl])],[split_symbol_definition]) ).
fof(f16721,plain,
( sQ702_spl
| ~ class_Lattices_Osemilattice__inf(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f16719]) ).
fof(f16734,definition,
( sQ706_spl
<=> class_Lattices_Obounded__lattice__top(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ706_spl])],[split_symbol_definition]) ).
fof(f16736,plain,
( sQ706_spl
| ~ class_Lattices_Obounded__lattice__top(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f16734]) ).
fof(f16802,plain,
( sQ702_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16721,f2066]) ).
fof(f16803,plain,
sQ702_spl,
inference(contradiction_clause,[status(thm)],[f16802]) ).
fof(f16805,plain,
( sQ706_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16736,f2063]) ).
fof(f16806,plain,
sQ706_spl,
inference(contradiction_clause,[status(thm)],[f16805]) ).
fof(f16856,definition,
! [X1] :
( sQ722_spl
<=> ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,c_Set_Oinsert(tc_Arrow__Order__Mirabelle_Oalt,X1,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)))) ),
introduced(definition,[new_symbols(definition,[sQ722_spl])],[split_symbol_definition]) ).
fof(f16857,plain,
! [X0] :
( ~ sQ722_spl
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,c_Set_Oinsert(tc_Arrow__Order__Mirabelle_Oalt,X0,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)))) ),
inference(component_clause,[status(thm)],[f16856]) ).
fof(f16890,definition,
( sQ723_spl
<=> class_Orderings_Oorder(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ723_spl])],[split_symbol_definition]) ).
fof(f16892,plain,
( sQ723_spl
| ~ class_Orderings_Oorder(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f16890]) ).
fof(f16896,plain,
( sQ723_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16892,f2070]) ).
fof(f16897,plain,
sQ723_spl,
inference(contradiction_clause,[status(thm)],[f16896]) ).
fof(f17011,plain,
( ~ sQ722_spl
| $false ),
inference(resolution,[status(thm)],[f16857,f2438]) ).
fof(f17016,plain,
~ sQ722_spl,
inference(contradiction_clause,[status(thm)],[f17011]) ).
fof(f18327,plain,
! [X0] :
( ~ sQ625_spl
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)))
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)),hAPP(v_P,v_i)) ),
inference(resolution,[status(thm)],[f13928,f2440]) ).
fof(f18345,definition,
( sQ743_spl
<=> c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_fequal(sK11_skl(tc_Arrow__Order__Mirabelle_Oalt,v_a,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i))),hAPP(v_P,v_i)) ),
introduced(definition,[new_symbols(definition,[sQ743_spl])],[split_symbol_definition]) ).
fof(f18347,plain,
( sQ743_spl
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_fequal(sK11_skl(tc_Arrow__Order__Mirabelle_Oalt,v_a,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i))),hAPP(v_P,v_i)) ),
inference(component_clause,[status(thm)],[f18345]) ).
fof(f18357,plain,
! [X0] :
( ~ sQ625_spl
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)),hAPP(v_P,v_i)) ),
inference(forward_subsumption_resolution,[status(thm)],[f18327,f2440]) ).
fof(f18363,plain,
( sQ743_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18347,f7419]) ).
fof(f18364,plain,
sQ743_spl,
inference(contradiction_clause,[status(thm)],[f18363]) ).
fof(f18384,plain,
( ~ sQ625_spl
| $false ),
inference(resolution,[status(thm)],[f18357,f2084]) ).
fof(f18385,plain,
~ sQ625_spl,
inference(contradiction_clause,[status(thm)],[f18384]) ).
fof(f18984,definition,
( sQ751_spl
<=> class_Lattices_Obounded__lattice__bot(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ751_spl])],[split_symbol_definition]) ).
fof(f18986,plain,
( sQ751_spl
| ~ class_Lattices_Obounded__lattice__bot(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f18984]) ).
fof(f19045,plain,
( sQ751_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18986,f2064]) ).
fof(f19046,plain,
sQ751_spl,
inference(contradiction_clause,[status(thm)],[f19045]) ).
fof(f19085,definition,
( sQ765_spl
<=> class_Lattices_Odistrib__lattice(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ765_spl])],[split_symbol_definition]) ).
fof(f19087,plain,
( sQ765_spl
| ~ class_Lattices_Odistrib__lattice(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f19085]) ).
fof(f19097,definition,
( sQ768_spl
<=> class_Lattices_Osemilattice__sup(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ768_spl])],[split_symbol_definition]) ).
fof(f19099,plain,
( sQ768_spl
| ~ class_Lattices_Osemilattice__sup(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f19097]) ).
fof(f19133,plain,
( sQ765_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19087,f2067]) ).
fof(f19134,plain,
sQ765_spl,
inference(contradiction_clause,[status(thm)],[f19133]) ).
fof(f19135,plain,
( sQ768_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19099,f2065]) ).
fof(f19136,plain,
sQ768_spl,
inference(contradiction_clause,[status(thm)],[f19135]) ).
fof(f20294,definition,
( sQ781_spl
<=> class_Orderings_Opreorder(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ781_spl])],[split_symbol_definition]) ).
fof(f20296,plain,
( sQ781_spl
| ~ class_Orderings_Opreorder(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f20294]) ).
fof(f20305,plain,
( sQ781_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20296,f2068]) ).
fof(f20306,plain,
sQ781_spl,
inference(contradiction_clause,[status(thm)],[f20305]) ).
fof(f20960,definition,
( sQ801_spl
<=> c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,c_Set_Oinsert(tc_Arrow__Order__Mirabelle_Oalt,v_a,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)))) ),
introduced(definition,[new_symbols(definition,[sQ801_spl])],[split_symbol_definition]) ).
fof(f20962,plain,
( sQ801_spl
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,c_Set_Oinsert(tc_Arrow__Order__Mirabelle_Oalt,v_a,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)))) ),
inference(component_clause,[status(thm)],[f20960]) ).
fof(f20965,plain,
( sQ801_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20962,f2438]) ).
fof(f20966,plain,
sQ801_spl,
inference(contradiction_clause,[status(thm)],[f20965]) ).
fof(f21045,plain,
( ~ sQ258_spl
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) ),
inference(resolution,[status(thm)],[f5199,f2459]) ).
fof(f21046,plain,
( ~ sQ258_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21045,f2126]) ).
fof(f21047,plain,
( ~ sQ258_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f21046]) ).
fof(f21841,definition,
( sQ807_spl
<=> class_Groups_Ominus(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ807_spl])],[split_symbol_definition]) ).
fof(f21843,plain,
( sQ807_spl
| ~ class_Groups_Ominus(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f21841]) ).
fof(f21869,plain,
( sQ807_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21843,f2074]) ).
fof(f21870,plain,
sQ807_spl,
inference(contradiction_clause,[status(thm)],[f21869]) ).
fof(f22595,definition,
( sQ830_spl
<=> c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_fequal(sK5_skl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))),v_F(v_P)) ),
introduced(definition,[new_symbols(definition,[sQ830_spl])],[split_symbol_definition]) ).
fof(f22597,plain,
( sQ830_spl
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_fequal(sK5_skl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))),v_F(v_P)) ),
inference(component_clause,[status(thm)],[f22595]) ).
fof(f22629,plain,
( sQ830_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22597,f7419]) ).
fof(f22630,plain,
sQ830_spl,
inference(contradiction_clause,[status(thm)],[f22629]) ).
fof(f23604,definition,
! [X0] :
( sQ870_spl
<=> ( ~ 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,X0,v_a),c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,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,X0,v_a),c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i))) ) ),
introduced(definition,[new_symbols(definition,[sQ870_spl])],[split_symbol_definition]) ).
fof(f23605,plain,
! [X0] :
( ~ sQ870_spl
| ~ 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,X0,v_a),c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,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,X0,v_a),c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i))) ),
inference(component_clause,[status(thm)],[f23604]) ).
fof(f23614,plain,
! [X0] :
( ~ sQ870_spl
| ~ 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,X0,v_a),c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i))) ),
inference(duplicate_literals_removal,[status(thm)],[f23605]) ).
fof(f23764,plain,
( ~ sQ870_spl
| $false ),
inference(resolution,[status(thm)],[f23614,f848]) ).
fof(f23769,plain,
~ sQ870_spl,
inference(contradiction_clause,[status(thm)],[f23764]) ).
fof(f23834,definition,
! [X0,X1] :
( sQ893_spl
<=> c_Orderings_Otop__class_Otop(tc_HOL_Obool) = hAPP(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ893_spl])],[split_symbol_definition]) ).
fof(f23835,plain,
! [X0,X1] :
( ~ sQ893_spl
| hAPP(X0,X1) = c_Orderings_Otop__class_Otop(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f23834]) ).
fof(f23912,definition,
( sQ900_spl
<=> c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_fequal(sK10_skl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))),v_F(v_P)) ),
introduced(definition,[new_symbols(definition,[sQ900_spl])],[split_symbol_definition]) ).
fof(f23914,plain,
( sQ900_spl
| ~ c_Relation_Ototal__on(tc_Arrow__Order__Mirabelle_Oalt,c_fequal(sK10_skl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))),v_F(v_P)) ),
inference(component_clause,[status(thm)],[f23912]) ).
fof(f23929,plain,
( sQ900_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23914,f7419]) ).
fof(f23930,plain,
sQ900_spl,
inference(contradiction_clause,[status(thm)],[f23929]) ).
fof(f24059,plain,
! [X0,X1] :
( ~ sQ893_spl
| X1 = X0
| hAPP(X0,sK0_skl(X0,X1)) != c_Orderings_Otop__class_Otop(tc_HOL_Obool) ),
inference(backward_demodulation,[status(thm)],[f23835,f531]) ).
fof(f24212,definition,
! [X0,X1,X2,X3] :
( sQ918_spl
<=> ( ~ hBOOL(hAPP(X3,X1))
| ~ c_member(X0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ918_spl])],[split_symbol_definition]) ).
fof(f24213,plain,
! [X0,X1,X2,X3] :
( ~ sQ918_spl
| ~ hBOOL(hAPP(X3,X1))
| ~ c_member(X0,X1,X2) ),
inference(component_clause,[status(thm)],[f24212]) ).
fof(f24220,plain,
! [X0,X1] :
( ~ sQ893_spl
| X0 = X1
| c_Orderings_Otop__class_Otop(tc_HOL_Obool) != c_Orderings_Otop__class_Otop(tc_HOL_Obool) ),
inference(forward_demodulation,[status(thm)],[f23835,f24059]) ).
fof(f24221,plain,
! [X0,X1] :
( ~ sQ893_spl
| X0 = X1 ),
inference(trivial_equality_resolution,[status(thm)],[f24220]) ).
fof(f24281,plain,
( ~ sQ893_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1517,f24221]) ).
fof(f24294,plain,
~ sQ893_spl,
inference(contradiction_clause,[status(thm)],[f24281]) ).
fof(f24655,plain,
! [X0] :
( ~ sQ577_spl
| c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b,v_a),hAPP(v_P,v_i)) ),
inference(resolution,[status(thm)],[f2450,f12889]) ).
fof(f24826,plain,
! [X0,X1,X2] :
( ~ sQ918_spl
| ~ c_member(X0,X1,X2) ),
inference(resolution,[status(thm)],[f24213,f2189]) ).
fof(f24837,plain,
( ~ sQ918_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2085,f24826]) ).
fof(f24844,plain,
~ sQ918_spl,
inference(contradiction_clause,[status(thm)],[f24837]) ).
fof(f25145,definition,
( sQ924_spl
<=> class_Orderings_Oord(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ924_spl])],[split_symbol_definition]) ).
fof(f25147,plain,
( sQ924_spl
| ~ class_Orderings_Oord(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f25145]) ).
fof(f25150,plain,
( sQ924_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25147,f2072]) ).
fof(f25151,plain,
sQ924_spl,
inference(contradiction_clause,[status(thm)],[f25150]) ).
fof(f25653,definition,
( sQ926_spl
<=> c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
introduced(definition,[new_symbols(definition,[sQ926_spl])],[split_symbol_definition]) ).
fof(f25654,plain,
( ~ sQ926_spl
| c_member(tc_Arrow__Order__Mirabelle_Oalt,v_b,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
inference(component_clause,[status(thm)],[f25653]) ).
fof(f25658,plain,
( ~ sQ926_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25654,f2477]) ).
fof(f25659,plain,
~ sQ926_spl,
inference(contradiction_clause,[status(thm)],[f25658]) ).
fof(f25676,definition,
! [X0] :
( sQ927_spl
<=> c_member(X0,v_a,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
introduced(definition,[new_symbols(definition,[sQ927_spl])],[split_symbol_definition]) ).
fof(f25677,plain,
! [X0] :
( ~ sQ927_spl
| c_member(X0,v_a,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
inference(component_clause,[status(thm)],[f25676]) ).
fof(f25680,plain,
( ~ sQ927_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25677,f2477]) ).
fof(f25681,plain,
~ sQ927_spl,
inference(contradiction_clause,[status(thm)],[f25680]) ).
fof(f27076,definition,
! [X0] :
( sQ942_spl
<=> c_member(X0,v_b,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
introduced(definition,[new_symbols(definition,[sQ942_spl])],[split_symbol_definition]) ).
fof(f27077,plain,
! [X0] :
( ~ sQ942_spl
| c_member(X0,v_b,c_Orderings_Obot__class_Obot(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
inference(component_clause,[status(thm)],[f27076]) ).
fof(f27080,plain,
( ~ sQ942_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27077,f2477]) ).
fof(f27081,plain,
~ sQ942_spl,
inference(contradiction_clause,[status(thm)],[f27080]) ).
fof(f27997,definition,
( sQ954_spl
<=> class_Lattices_Obounded__lattice(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ954_spl])],[split_symbol_definition]) ).
fof(f27999,plain,
( sQ954_spl
| ~ class_Lattices_Obounded__lattice(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f27997]) ).
fof(f28001,plain,
( sQ954_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27999,f2023]) ).
fof(f28002,plain,
sQ954_spl,
inference(contradiction_clause,[status(thm)],[f28001]) ).
fof(f28244,definition,
! [X0] :
( sQ963_spl
<=> ( ~ c_Relation_Orefl__on(tc_Arrow__Order__Mirabelle_Oalt,X0,c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i)))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ963_spl])],[split_symbol_definition]) ).
fof(f28245,plain,
! [X0] :
( ~ sQ963_spl
| ~ c_Relation_Orefl__on(tc_Arrow__Order__Mirabelle_Oalt,X0,c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i)))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,v_a,X0) ),
inference(component_clause,[status(thm)],[f28244]) ).
fof(f28249,plain,
! [X0] :
( ~ sQ963_spl
| ~ c_Relation_Orefl__on(tc_Arrow__Order__Mirabelle_Oalt,X0,c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,v_i))) ),
inference(forward_subsumption_resolution,[status(thm)],[f28245,f12397]) ).
fof(f28389,plain,
( ~ sQ963_spl
| $false ),
inference(resolution,[status(thm)],[f28249,f859]) ).
fof(f28390,plain,
~ sQ963_spl,
inference(contradiction_clause,[status(thm)],[f28389]) ).
fof(f30515,plain,
( ~ sQ577_spl
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK84_skl(v_P)))
| ~ 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,sK86_skl(v_P)))
| v_b = v_a
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK85_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)) ),
inference(resolution,[status(thm)],[f2080,f24655]) ).
fof(f30522,plain,
( ~ sQ577_spl
| ~ sQ248_spl
| ~ sQ249_spl
| sQ292_spl
| ~ sQ251_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f30515,f2696,f4924,f5794,f4918,f4915,f12888]) ).
fof(f30523,plain,
$false,
inference(sat_refutation,[status(thm)],[f2124,f2128,f2367,f2369,f2371,f2671,f2699,f4942,f4944,f4947,f10848,f10849,f13872,f14021,f14023,f14025,f14192,f14264,f15215,f15356,f15628,f15684,f16237,f16803,f16806,f16897,f17016,f18364,f18385,f19046,f19134,f19136,f20306,f20966,f21047,f21870,f22630,f23769,f23930,f24294,f24844,f25151,f25659,f25681,f27081,f28002,f28390,f30522]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT121+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n009.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 21 04:32:57 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.05/0.52 % Drodi V4.1.1
% 177.94/23.27 % Refutation found
% 177.94/23.27 % SZS status Theorem for theBenchmark: Theorem is valid
% 177.94/23.27 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 122.27/24.56 % Elapsed time: 23.924107 seconds
% 122.27/24.56 % CPU time: 169.871405 seconds
% 122.27/24.56 % Total memory used: 519.173 MB
% 122.27/24.56 % Net memory used: 469.898 MB
%------------------------------------------------------------------------------