%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SCT122+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:28:31 AM UTC 2026
% Result : Theorem 258.51s 59.45s
% Output : CNFRefutation 258.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 19
% Syntax : Number of formulae : 94 ( 36 unt; 0 def)
% Number of atoms : 238 ( 37 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 246 ( 102 ~; 107 |; 17 &)
% ( 4 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 8 con; 0-4 aty)
% Number of variables : 148 ( 8 sgn 69 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_UNIV__I,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('theBenchmark.p',fact_UNIV__I) ).
fof(fact_irrefl__def,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('theBenchmark.p',fact_irrefl__def) ).
fof(fact_total__on__def,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('theBenchmark.p',fact_total__on__def) ).
fof(fact_mem__def,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('theBenchmark.p',fact_mem__def) ).
fof(fact_antisymD,axiom,
! [V_b_2,V_a_2,V_r_2,T_a] :
( c_Relation_Oantisym(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_a_2),V_r_2)
=> V_a_2 = V_b_2 ) ) ),
file('theBenchmark.p',fact_antisymD) ).
fof(fact_reflcl__trancl,axiom,
! [V_r_2,T_a] : c_Lattices_Osemilattice__sup__class_Osup(tc_fun(tc_prod(T_a,T_a),tc_HOL_Obool),c_Transitive__Closure_Otrancl(T_a,V_r_2),c_Relation_OId(T_a)) = c_Transitive__Closure_Ortrancl(T_a,V_r_2),
file('theBenchmark.p',fact_reflcl__trancl) ).
fof(fact_trancl__id,axiom,
! [V_r_2,T_a] :
( c_Relation_Otrans(T_a,V_r_2)
=> c_Transitive__Closure_Otrancl(T_a,V_r_2) = V_r_2 ),
file('theBenchmark.p',fact_trancl__id) ).
fof(fact_acyclic__def,axiom,
! [V_r_2,T_a] :
( c_Wellfounded_Oacyclic(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),c_Transitive__Closure_Otrancl(T_a,V_r_2)) ),
file('theBenchmark.p',fact_acyclic__def) ).
fof(fact_acyclic__impl__antisym__rtrancl,axiom,
! [V_r_2,T_a] :
( c_Wellfounded_Oacyclic(T_a,V_r_2)
=> c_Relation_Oantisym(T_a,c_Transitive__Closure_Ortrancl(T_a,V_r_2)) ),
file('theBenchmark.p',fact_acyclic__impl__antisym__rtrancl) ).
fof(fact_irrefl__trancl__rD,axiom,
! [V_y_2,V_x_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),c_Transitive__Closure_Otrancl(T_a,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)
=> V_x_2 != V_y_2 ) ),
file('theBenchmark.p',fact_irrefl__trancl__rD) ).
fof(fact_Id__on__empty,axiom,
! [T_a] : c_Relation_OId__on(T_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))) = c_Orderings_Obot__class_Obot(tc_fun(tc_prod(T_a,T_a),tc_HOL_Obool)),
file('theBenchmark.p',fact_Id__on__empty) ).
fof(fact_Un__upper1,axiom,
! [V_B_2,V_A_2,T_a] : c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,tc_HOL_Obool),V_A_2,c_Lattices_Osemilattice__sup__class_Osup(tc_fun(T_a,tc_HOL_Obool),V_A_2,V_B_2)),
file('theBenchmark.p',fact_Un__upper1) ).
fof(fact_antisym__subset,axiom,
! [V_s_2,V_r_2,T_a] :
( c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(T_a,T_a),tc_HOL_Obool),V_r_2,V_s_2)
=> ( c_Relation_Oantisym(T_a,V_s_2)
=> c_Relation_Oantisym(T_a,V_r_2) ) ),
file('theBenchmark.p',fact_antisym__subset) ).
fof(fact_rtrancl__empty,axiom,
! [T_a] : c_Transitive__Closure_Ortrancl(T_a,c_Orderings_Obot__class_Obot(tc_fun(tc_prod(T_a,T_a),tc_HOL_Obool))) = c_Relation_OId(T_a),
file('theBenchmark.p',fact_rtrancl__empty) ).
fof(conj_0,axiom,
! [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('theBenchmark.p',conj_0) ).
fof(conj_2,axiom,
( ! [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('theBenchmark.p',conj_2) ).
fof(conj_3,axiom,
( ! [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)) )
=> ! [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(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,B_a,B_b),v_F(v_P)) ) ) ),
file('theBenchmark.p',conj_3) ).
fof(conj_4,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('theBenchmark.p',conj_4) ).
fof(conj_4_neg,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(assume_negation,[status(cth)],[conj_4]) ).
cnf(c_805,plain,
c_member(A,B,c_Orderings_Otop__class_Otop(tc_fun(A,tc_HOL_Obool))),
inference(clausify,[status(thm)],[fact_UNIV__I]) ).
cnf(c_806,plain,
( ~ c_member(tc_prod(A,A),c_Product__Type_OPair(A,A,C,C),B)
| ~ c_Relation_Oirrefl(A,B) ),
inference(clausify,[status(thm)],[fact_irrefl__def]) ).
cnf(c_808,plain,
( c_member(tc_prod(A,A),c_Product__Type_OPair(A,A,E,D),C)
| c_member(tc_prod(A,A),c_Product__Type_OPair(A,A,D,E),C)
| E = D
| ~ c_member(A,E,B)
| ~ c_member(A,D,B)
| ~ c_Relation_Ototal__on(A,B,C) ),
inference(clausify,[status(thm)],[fact_total__on__def]) ).
cnf(c_827,plain,
( hBOOL(hAPP(C,B))
| ~ c_member(A,B,C) ),
inference(clausify,[status(thm)],[fact_mem__def]) ).
cnf(c_828,plain,
( ~ hBOOL(hAPP(C,B))
| c_member(A,B,C) ),
inference(clausify,[status(thm)],[fact_mem__def]) ).
cnf(c_915,plain,
( D = C
| ~ c_member(tc_prod(A,A),c_Product__Type_OPair(A,A,D,C),B)
| ~ c_member(tc_prod(A,A),c_Product__Type_OPair(A,A,C,D),B)
| ~ c_Relation_Oantisym(A,B) ),
inference(clausify,[status(thm)],[fact_antisymD]) ).
cnf(c_954,plain,
c_Lattices_Osemilattice__sup__class_Osup(tc_fun(tc_prod(A,A),tc_HOL_Obool),c_Transitive__Closure_Otrancl(A,B),c_Relation_OId(A)) = c_Transitive__Closure_Ortrancl(A,B),
inference(clausify,[status(thm)],[fact_reflcl__trancl]) ).
cnf(c_964,plain,
( c_Transitive__Closure_Otrancl(A,B) = B
| ~ c_Relation_Otrans(A,B) ),
inference(clausify,[status(thm)],[fact_trancl__id]) ).
fof(nnf_129,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),c_Transitive__Closure_Otrancl(T_a,V_r_2))
| c_Wellfounded_Oacyclic(T_a,V_r_2) )
& ( ! [X0] : ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,X0,X0),c_Transitive__Closure_Otrancl(T_a,V_r_2))
| ~ c_Wellfounded_Oacyclic(T_a,V_r_2) ) ),
inference(fof_nnf,[status(thm)],[fact_acyclic__def]) ).
fof(sk_fact_acyclic__def_sk,plain,
! [V_r_2,T_a] :
( ( c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,sK0(V_r_2,T_a),sK0(V_r_2,T_a)),c_Transitive__Closure_Otrancl(T_a,V_r_2))
| c_Wellfounded_Oacyclic(T_a,V_r_2) )
& ( ! [X0] : ~ c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,X0,X0),c_Transitive__Closure_Otrancl(T_a,V_r_2))
| ~ c_Wellfounded_Oacyclic(T_a,V_r_2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(B_x,sK0(V_r_2,T_a))],[nnf_129]) ).
fof(sk_fact_acyclic__def,plain,
( ! [VAR_0,VAR_1] :
( c_member(tc_prod(VAR_0,VAR_0),c_Product__Type_OPair(VAR_0,VAR_0,sK0(VAR_1,VAR_0),sK0(VAR_1,VAR_0)),c_Transitive__Closure_Otrancl(VAR_0,VAR_1))
| c_Wellfounded_Oacyclic(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ c_member(tc_prod(VAR_0,VAR_0),c_Product__Type_OPair(VAR_0,VAR_0,VAR_2,VAR_2),c_Transitive__Closure_Otrancl(VAR_0,VAR_1))
| ~ c_Wellfounded_Oacyclic(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_fact_acyclic__def_sk]) ).
cnf(c_999,plain,
( ~ c_member(tc_prod(A,A),c_Product__Type_OPair(A,A,C,C),c_Transitive__Closure_Otrancl(A,B))
| ~ c_Wellfounded_Oacyclic(A,B) ),
inference(split_conjunct,[status(thm)],[sk_fact_acyclic__def]) ).
cnf(c_1000,plain,
( c_member(tc_prod(A,A),c_Product__Type_OPair(A,A,sK0(B,A),sK0(B,A)),c_Transitive__Closure_Otrancl(A,B))
| c_Wellfounded_Oacyclic(A,B) ),
inference(split_conjunct,[status(thm)],[sk_fact_acyclic__def]) ).
cnf(c_1004,plain,
( c_Relation_Oantisym(A,c_Transitive__Closure_Ortrancl(A,B))
| ~ c_Wellfounded_Oacyclic(A,B) ),
inference(clausify,[status(thm)],[fact_acyclic__impl__antisym__rtrancl]) ).
fof(nnf_136,plain,
! [V_y_2,V_x_2,V_r_2,T_a] :
( V_y_2 != V_x_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)
| ? [B_x] : c_member(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,B_x,B_x),c_Transitive__Closure_Otrancl(T_a,V_r_2)) ),
inference(fof_nnf,[status(thm)],[fact_irrefl__trancl__rD]) ).
fof(sk_fact_irrefl__trancl__rD,plain,
! [V_y_2,V_x_2,V_r_2,T_a] :
( V_y_2 != V_x_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(tc_prod(T_a,T_a),c_Product__Type_OPair(T_a,T_a,sK1(V_y_2,V_x_2,V_r_2,T_a),sK1(V_y_2,V_x_2,V_r_2,T_a)),c_Transitive__Closure_Otrancl(T_a,V_r_2)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(B_x,sK1(V_y_2,V_x_2,V_r_2,T_a))],[nnf_136]) ).
cnf(c_1011,plain,
( B != C
| ~ c_member(tc_prod(A,A),c_Product__Type_OPair(A,A,C,B),D)
| c_member(tc_prod(A,A),c_Product__Type_OPair(A,A,sK1(B,C,D,A),sK1(B,C,D,A)),c_Transitive__Closure_Otrancl(A,D)) ),
inference(split_conjunct,[status(thm)],[sk_fact_irrefl__trancl__rD]) ).
cnf(c_1092,plain,
c_Orderings_Obot__class_Obot(tc_fun(tc_prod(A,A),tc_HOL_Obool)) = c_Relation_OId__on(A,c_Orderings_Obot__class_Obot(tc_fun(A,tc_HOL_Obool))),
inference(clausify,[status(thm)],[fact_Id__on__empty]) ).
cnf(c_1102,plain,
c_Orderings_Oord__class_Oless__eq(tc_fun(A,tc_HOL_Obool),B,c_Lattices_Osemilattice__sup__class_Osup(tc_fun(A,tc_HOL_Obool),B,C)),
inference(clausify,[status(thm)],[fact_Un__upper1]) ).
cnf(c_1144,plain,
( c_Relation_Oantisym(A,B)
| ~ c_Relation_Oantisym(A,C)
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(A,A),tc_HOL_Obool),B,C) ),
inference(clausify,[status(thm)],[fact_antisym__subset]) ).
cnf(c_1170,plain,
c_Relation_OId(A) = c_Transitive__Closure_Ortrancl(A,c_Orderings_Obot__class_Obot(tc_fun(tc_prod(A,A),tc_HOL_Obool))),
inference(clausify,[status(thm)],[fact_rtrancl__empty]) ).
cnf(c_1171,plain,
c_Relation_OId(A) = c_Transitive__Closure_Ortrancl(A,c_Relation_OId__on(A,c_Orderings_Obot__class_Obot(tc_fun(A,tc_HOL_Obool)))),
inference(paramod,[status(thm)],[c_1092,c_1170]) ).
cnf(c_1280,plain,
c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,A)),
inference(clausify,[status(thm)],[conj_0]) ).
cnf(c_1281,plain,
c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,A)),
inference(clausify,[status(thm)],[conj_0]) ).
cnf(c_1282,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)),hAPP(v_P,A)),
inference(clausify,[status(thm)],[conj_0]) ).
fof(conj_1,axiom,
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('theBenchmark.p',conj_1) ).
cnf(c_1283,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(clausify,[status(thm)],[conj_1]) ).
fof(nnf_337,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(fof_nnf,[status(thm)],[conj_2]) ).
fof(sk_conj_2_sk,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,sK2))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(B_x,sK2)],[nnf_337]) ).
fof(sk_conj_2,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_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,sK2))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2)) )
& ( 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,sK2))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2)) )
& ( 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,sK2))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2)) ) ),
inference(cnf_transformation,[status(thm)],[sk_conj_2_sk]) ).
cnf(c_1284,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,sK2))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2)) ),
inference(split_conjunct,[status(thm)],[sk_conj_2]) ).
cnf(c_52716,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,sK2))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2)) ),
inference(resolve,[status(thm)],[c_1280,c_1284]) ).
cnf(c_52717,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,sK2)) ),
inference(resolve,[status(thm)],[c_1281,c_52716]) ).
cnf(c_1285,plain,
c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)),
inference(resolve,[status(thm)],[c_1282,c_52717]) ).
cnf(c_1286,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,sK2))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2)) ),
inference(split_conjunct,[status(thm)],[sk_conj_2]) ).
cnf(c_52718,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,sK2))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK2)) ),
inference(resolve,[status(thm)],[c_1280,c_1286]) ).
cnf(c_52719,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,sK2)) ),
inference(resolve,[status(thm)],[c_1281,c_52718]) ).
cnf(c_1287,plain,
c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)),
inference(resolve,[status(thm)],[c_1282,c_52719]) ).
fof(nnf_338,plain,
( ! [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(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,B_a,B_b),hAPP(v_P,v_i))
| B_b = B_a )
| ? [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(fof_nnf,[status(thm)],[conj_3]) ).
fof(sk_conj_3_sk,plain,
( ! [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(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,B_a,B_b),hAPP(v_P,v_i))
| B_b = B_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,sK3))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK3))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK3)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(B_x,sK3)],[nnf_338]) ).
fof(sk_conj_3,plain,
! [VAR_0,VAR_1] :
( 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,VAR_1,VAR_0),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,VAR_1,VAR_0),hAPP(v_P,v_i))
| VAR_0 = VAR_1
| ~ 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,sK3))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK3))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK3)) ),
inference(cnf_transformation,[status(thm)],[sk_conj_3_sk]) ).
cnf(c_1290,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,B,A),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,B,A),hAPP(v_P,v_i))
| A = 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(v_P,sK3))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK3))
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK3)) ),
inference(split_conjunct,[status(thm)],[sk_conj_3]) ).
cnf(c_52720,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,B,A),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,B,A),hAPP(v_P,v_i))
| A = 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(v_P,sK3))
| ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P,sK3)) ),
inference(resolve,[status(thm)],[c_1280,c_1290]) ).
cnf(c_52721,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,B,A),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,B,A),hAPP(v_P,v_i))
| A = 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(v_P,sK3)) ),
inference(resolve,[status(thm)],[c_1281,c_52720]) ).
cnf(c_1291,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,B,A),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,B,A),hAPP(v_P,v_i))
| A = B ),
inference(resolve,[status(thm)],[c_1282,c_52721]) ).
cnf(c_1292,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(clausify,[status(thm)],[conj_4_neg]) ).
cnf(c_1315,plain,
c_Lattices_Osemilattice__sup__class_Osup(tc_fun(tc_prod(A,A),tc_HOL_Obool),c_Transitive__Closure_Otrancl(A,B),c_Transitive__Closure_Ortrancl(A,c_Relation_OId__on(A,c_Orderings_Obot__class_Obot(tc_fun(A,tc_HOL_Obool))))) = c_Transitive__Closure_Ortrancl(A,B),
inference(paramod,[status(thm)],[c_1171,c_954]) ).
cnf(c_52722,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,B,A),hAPP(v_P,C))
| 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,A,B),hAPP(v_P,C))
| B = A
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,B,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool)))
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,A,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
inference(resolve,[status(thm)],[c_808,c_1282]) ).
cnf(c_52723,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,A,B),hAPP(v_P,C))
| 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),hAPP(v_P,C))
| A = B
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,A,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_HOL_Obool))) ),
inference(resolve,[status(thm)],[c_805,c_52722]) ).
cnf(c_1688,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,A,B),hAPP(v_P,C))
| 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),hAPP(v_P,C))
| A = B ),
inference(resolve,[status(thm)],[c_805,c_52723]) ).
cnf(c_3445,plain,
hBOOL(hAPP(v_F(v_P),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_b))),
inference(resolve,[status(thm)],[c_827,c_1283]) ).
cnf(c_3702,plain,
c_member(A,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a,v_b),v_F(v_P)),
inference(resolve,[status(thm)],[c_3445,c_828]) ).
cnf(c_10627,plain,
( v_b = v_a
| ~ 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_Oantisym(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) ),
inference(resolve,[status(thm)],[c_915,c_3702]) ).
cnf(c_17317,plain,
c_Transitive__Closure_Otrancl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) = v_F(v_P),
inference(resolve,[status(thm)],[c_964,c_1285]) ).
cnf(c_20929,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,A,A),v_F(v_P))
| ~ c_Wellfounded_Oacyclic(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) ),
inference(paramod,[status(thm)],[c_17317,c_999]) ).
cnf(c_20962,plain,
( ~ c_Relation_Oirrefl(A,c_Transitive__Closure_Otrancl(A,B))
| c_Wellfounded_Oacyclic(A,B) ),
inference(resolve,[status(thm)],[c_1000,c_806]) ).
cnf(c_52724,plain,
( ~ c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))
| c_Wellfounded_Oacyclic(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) ),
inference(paramod,[status(thm)],[c_17317,c_20962]) ).
cnf(c_20975,plain,
c_Wellfounded_Oacyclic(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)),
inference(resolve,[status(thm)],[c_1287,c_52724]) ).
cnf(c_20979,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,A,A),v_F(v_P)),
inference(resolve,[status(thm)],[c_20975,c_20929]) ).
cnf(c_21319,plain,
c_Relation_Oantisym(tc_Arrow__Order__Mirabelle_Oalt,c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))),
inference(resolve,[status(thm)],[c_1004,c_20975]) ).
cnf(c_52725,plain,
( v_b != v_a
| 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,sK1(v_b,v_a,v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt),sK1(v_b,v_a,v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)),c_Transitive__Closure_Otrancl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))) ),
inference(resolve,[status(thm)],[c_1011,c_3702]) ).
cnf(c_52726,plain,
( v_b != v_a
| 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,sK1(v_b,v_a,v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt),sK1(v_b,v_a,v_F(v_P),tc_Arrow__Order__Mirabelle_Oalt)),v_F(v_P)) ),
inference(paramod,[status(thm)],[c_17317,c_52725]) ).
cnf(c_21681,plain,
v_b != v_a,
inference(resolve,[status(thm)],[c_20979,c_52726]) ).
cnf(c_21694,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_b,v_a),v_F(v_P))
| ~ c_Relation_Oantisym(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)) ),
inference(resolve,[status(thm)],[c_21681,c_10627]) ).
cnf(c_37049,plain,
c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(A,A),tc_HOL_Obool),c_Transitive__Closure_Otrancl(A,B),c_Transitive__Closure_Ortrancl(A,B)),
inference(paramod,[status(thm)],[c_1315,c_1102]) ).
cnf(c_37066,plain,
( c_Relation_Oantisym(A,c_Transitive__Closure_Otrancl(A,B))
| ~ c_Relation_Oantisym(A,c_Transitive__Closure_Ortrancl(A,B)) ),
inference(resolve,[status(thm)],[c_37049,c_1144]) ).
cnf(c_52727,plain,
c_Relation_Oantisym(tc_Arrow__Order__Mirabelle_Oalt,c_Transitive__Closure_Otrancl(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))),
inference(resolve,[status(thm)],[c_37066,c_21319]) ).
cnf(c_37076,plain,
c_Relation_Oantisym(tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P)),
inference(paramod,[status(thm)],[c_17317,c_52727]) ).
cnf(c_37079,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_b,v_a),v_F(v_P)),
inference(resolve,[status(thm)],[c_37076,c_21694]) ).
cnf(c_52728,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_b,v_a),hAPP(v_P,v_i))
| v_b = v_a ),
inference(resolve,[status(thm)],[c_1688,c_1292]) ).
cnf(c_52691,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_b,v_a),hAPP(v_P,v_i)),
inference(resolve,[status(thm)],[c_21681,c_52728]) ).
cnf(c_52729,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_b,v_a),v_F(v_P))
| v_a = v_b ),
inference(resolve,[status(thm)],[c_52691,c_1291]) ).
cnf(c_52730,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_b,v_a),v_F(v_P))
| v_b = v_a ),
inference(copy,[status(thm)],[c_52729]) ).
cnf(c_52731,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_b,v_a),v_F(v_P)),
inference(resolve,[status(thm)],[c_21681,c_52730]) ).
cnf(c_52715,plain,
$false,
inference(resolve,[status(thm)],[c_37079,c_52731]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT122+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 06:28:10 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 3000721 was started by sandbox on n007,
% 0.08/0.37 % Sat Sep 26 06:28:10 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.43
% 0.08/0.43 % From the command line: assign(max_seconds, 300).
% 0.08/0.43
% 0.08/0.43 % SInE: 339 to sos, 187 to usable, of 526 axioms (tolerance 2.00, depth 0 fixpoint).
% 258.51/59.45
% 258.51/59.45 % given #500 (F,wt=19): 5338 c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(A,tc_HOL_Obool),c_fequal(B),c_Wellfounded_Oacc(C,c_Relation_OId__on(C,c_Orderings_Obot__class_Obot(tc_fun(C,tc_HOL_Obool))))) != c_Orderings_Obot__class_Obot(tc_fun(A,tc_HOL_Obool)). [resolve(4291,b,4836,a),xx(b)].
% 258.51/59.45
% 258.51/59.45 % given #1000 (W,wt=13): 9464 c_member(A,c_Arrow__Order__Mirabelle_Omktop(c_Arrow__Order__Mirabelle_Omkbot(c1,B),C),c_Lattices_Osemilattice__sup__class_Osup(tc_fun(D,tc_HOL_Obool),c_Arrow__Order__Mirabelle_OLin,E)). [resolve(6753,a,828,b)].
% 258.51/59.45
% 258.51/59.45 % given #1500 (F,wt=18): 17325 c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(tc_prod(A,A),tc_HOL_Obool),c_Orderings_Otop__class_Otop(tc_fun(B,tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin) != c_Relation_OId__on(A,c_Orderings_Obot__class_Obot(tc_fun(A,tc_HOL_Obool))). [back_rewrite(16852),rewrite([17308(7)])].
% 258.51/59.45
% 258.51/59.45 % given #2000 (T,wt=11): 21776 c_member(A,c_Arrow__Order__Mirabelle_Omktop(c1,B),c_Set_Oinsert(A,C,c_Transitive__Closure_Otrancl(D,c_Arrow__Order__Mirabelle_OLin))). [resolve(1012,a,16472,a)].
% 258.51/59.45
% 258.51/59.45 % given #2500 (F,wt=12): 28688 c_Relation_OId__on(tc_prod(A,A),c_Relation_OId__on(A,c_Orderings_Obot__class_Obot(tc_fun(A,tc_HOL_Obool)))) != c_Arrow__Order__Mirabelle_OLin. [para(1092(a,1),28219(a,1,2))].
% 258.51/59.45
% 258.51/59.45 % given #3000 (T,wt=11): 32492 c_Arrow__Order__Mirabelle_Omktop(f64(c_Arrow__Order__Mirabelle_OLin,A),B) != C | c_member(D,C,c_Arrow__Order__Mirabelle_OLin). [resolve(32462,a,826,b),flip(a)].
% 258.51/59.45
% 258.51/59.45 % given #3500 (F,wt=16): 29678 c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(A,tc_HOL_Obool),c_Arrow__Order__Mirabelle_OLin,c_Wellfounded_Oacc(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_HOL_Obool)))) != c_Orderings_Obot__class_Obot(tc_fun(D,tc_HOL_Obool)). [para(29209(a,1),27686(a,2))].
% 258.51/59.45
% 258.51/59.45 % given #4000 (T,wt=13): 31827 c_Relation_Otrans(A,c_Relation_ODomain(B,C,c_Wellfounded_Oacc(D,c_Relation_OId__on(E,c_Orderings_Obot__class_Obot(tc_fun(F,tc_HOL_Obool)))))). [para(29916(a,1),31808(a,2,3,2))].
% 258.51/59.45
% 258.51/59.45 % given #4500 (A,wt=47): 1441 c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(tc_prod(A,A),tc_HOL_Obool),B,C) != c_Relation_OId__on(A,c_Orderings_Obot__class_Obot(tc_fun(A,tc_HOL_Obool))) | -c_member(tc_prod(A,A),D,B) | c_Product__Type_OPair(A,A,f75(E,F,C,V6,V7,A),F) != D | c_Recdef_Ocut(A,V7,E,C,F) = c_Recdef_Ocut(A,V7,V6,C,F). [resolve(1232,c,587,b),rewrite([1092(8)])].
% 258.51/59.45
% 258.51/59.45 % given #5000 (T,wt=12): 46357 c_member(A,v_b,c_Transitive__Closure_Ortrancl(B,c_Transitive__Closure_Ortrancl(C,c_Relation_ORange(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_F(v_P))))). [resolve(46351,a,828,b)].
% 258.51/59.45
% 258.51/59.45 % given #5500 (W,wt=14): 17285 c_Transitive__Closure_Otrancl(A,B) = B | hBOOL(hAPP(c_Relation_ODomain(A,A,B),f9(B,A))). [resolve(964,a,5438,a)].
% 258.51/59.45
% 258.51/59.45 % given #6000 (F,wt=17): 51328 c_Orderings_Obot__class_Obot(tc_fun(A,tc_HOL_Obool)) != c_Transitive__Closure_Otrancl(B,c_Lattices_Osemilattice__sup__class_Osup(tc_fun(C,tc_HOL_Obool),D,c_Transitive__Closure_Otrancl(E,c_Transitive__Closure_Ortrancl(F,c_Arrow__Order__Mirabelle_OLin)))). [para(23921(a,1),37355(a,2,2,3))].
% 258.51/59.45
% 258.51/59.45 % SZS status Theorem for theBenchmark
% 258.51/59.45
% 258.51/59.45 % Proof 1 at 28.76 (+ 3.56) seconds.
% 258.51/59.45 % Length of proof is 65.
% 258.51/59.45 % Level of proof is 9.
% 258.51/59.45 % Maximum clause weight is 319.000.
% 258.51/59.45 % Given clauses 6309.
% 258.51/59.45
% 258.51/59.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------