%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SCT117+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n008.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 : Fri Sep 25 02:40:46 PM UTC 2026
% Result : Theorem 76.32s 11.44s
% Output : CNFRefutation 76.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 18
% Syntax : Number of formulae : 325 ( 25 unt; 6 def)
% Number of atoms : 1669 ( 723 equ)
% Maximal formula atoms : 53 ( 5 avg)
% Number of connectives : 1947 ( 603 ~;1013 |; 283 &)
% ( 2 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 2 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 10 con; 0-5 aty)
% Number of variables : 486 ( 0 sgn 456 !; 30 ?; 206 :)
% Comments :
%------------------------------------------------------------------------------
fof(f150,axiom,
! [X0,X1,X2,X3] :
( ( ~ c_member(X3,X2,X1)
=> X2 = X0 )
=> c_member(X3,X2,c_Set_Oinsert(X3,X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insertCI) ).
fof(f163,axiom,
! [X0,X1,X2,X3] : c_Set_Oinsert(X3,X2,c_Set_Oinsert(X3,X1,X0)) = c_Set_Oinsert(X3,X1,c_Set_Oinsert(X3,X2,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insert__commute) ).
fof(f190,axiom,
! [X0,X1,X2] :
( c_member(X2,X1,X0)
=> c_Set_Oinsert(X2,X1,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insert__absorb) ).
fof(f284,axiom,
! [X0,X1,X2,X3,X4] :
( c_Set_Oinsert(X4,X3,c_Set_Oinsert(X4,X2,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool)))) = c_Set_Oinsert(X4,X1,c_Set_Oinsert(X4,X0,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool))))
<=> ( ( X2 = X1
& X3 = X0 )
| ( X2 = X0
& X3 = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_doubleton__eq__iff) ).
fof(f325,axiom,
! [X0,X1] : c_Relation_OImage(X1,X1,c_Relation_OId(X1),X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Image__Id) ).
fof(f330,axiom,
! [X0,X1,X2,X3,X4,X5] :
( c_member(X5,X4,X3)
=> ( c_member(tc_prod(X5,X2),c_Product__Type_OPair(X5,X2,X4,X1),X0)
=> c_member(X2,X1,c_Relation_OImage(X5,X2,X0,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rev__ImageI) ).
fof(f353,axiom,
! [X0,X1,X2,X3,X4] :
( c_member(X4,X3,c_Relation_OImage(X2,X4,X1,c_Set_Oinsert(X2,X0,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)))))
<=> c_member(tc_prod(X2,X4),c_Product__Type_OPair(X2,X4,X0,X3),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Image__singleton__iff) ).
fof(f475,axiom,
! [X0,X1,X2,X3,X4] :
( c_member(X4,X3,c_Relation_OImage(X2,X4,X1,X0))
=> ~ ! [X5] :
( c_member(tc_prod(X2,X4),c_Product__Type_OPair(X2,X4,X5,X3),X1)
=> ~ c_member(X2,X5,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ImageE) ).
fof(f526,axiom,
v_x != v_y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f527,axiom,
( ! [X0,X1] :
( X0 != X1
=> ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L)
| 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_L) ) )
& ! [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,X0,X0),v_L)
& ! [X0,X1] :
( 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_L)
=> ! [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,X1,X2),v_L)
=> 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,X2),v_L) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
fof(f528,conjecture,
( ! [X0,X1] :
( X0 != X1
=> ( ( X0 != v_y
& 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_x,X0),v_L)
& X1 = v_y )
| ( X1 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L)
& X0 = v_y )
| ( X0 != v_y
& X1 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L) )
| ( X0 = v_y
& X1 = v_x )
| ( X1 != v_y
& 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_x,X1),v_L)
& X0 = v_y )
| ( X0 != v_y
& 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_x),v_L)
& X1 = v_y )
| ( X1 != v_y
& X0 != v_y
& 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_L) )
| ( X1 = v_y
& X0 = v_x ) ) )
& ! [X0,X1] :
( ( ( X1 != v_y
& 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_x,X1),v_L)
& X0 = v_y )
=> ! [X2] :
( ( X2 = v_y
=> ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) )
& ( ( X2 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L) )
=> 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_x,X2),v_L) )
& ( X1 = v_x
=> X2 != v_y ) ) )
& ( ( X0 != v_y
& 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_x),v_L)
& X1 = v_y )
=> ! [X2] :
( ( X2 != v_y
& 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_x,X2),v_L) )
=> 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,X2),v_L) ) )
& ( ( X1 != v_y
& X0 != v_y
& 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_L) )
=> ! [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,X1,v_x),v_L)
& X2 = v_y )
=> ( 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_x),v_L)
| X0 = v_x ) )
& ( ( X2 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L) )
=> 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,X2),v_L) )
& ( ( X2 = v_y
& X1 = v_x )
=> ( 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_x),v_L)
| X0 = v_x ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_2) ).
fof(f529,negated_conjecture,
~ ( ! [X0,X1] :
( X0 != X1
=> ( ( X0 != v_y
& 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_x,X0),v_L)
& X1 = v_y )
| ( X1 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L)
& X0 = v_y )
| ( X0 != v_y
& X1 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L) )
| ( X0 = v_y
& X1 = v_x )
| ( X1 != v_y
& 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_x,X1),v_L)
& X0 = v_y )
| ( X0 != v_y
& 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_x),v_L)
& X1 = v_y )
| ( X1 != v_y
& X0 != v_y
& 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_L) )
| ( X1 = v_y
& X0 = v_x ) ) )
& ! [X0,X1] :
( ( ( X1 != v_y
& 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_x,X1),v_L)
& X0 = v_y )
=> ! [X2] :
( ( X2 = v_y
=> ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) )
& ( ( X2 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L) )
=> 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_x,X2),v_L) )
& ( X1 = v_x
=> X2 != v_y ) ) )
& ( ( X0 != v_y
& 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_x),v_L)
& X1 = v_y )
=> ! [X2] :
( ( X2 != v_y
& 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_x,X2),v_L) )
=> 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,X2),v_L) ) )
& ( ( X1 != v_y
& X0 != v_y
& 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_L) )
=> ! [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,X1,v_x),v_L)
& X2 = v_y )
=> ( 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_x),v_L)
| X0 = v_x ) )
& ( ( X2 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L) )
=> 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,X2),v_L) )
& ( ( X2 = v_y
& X1 = v_x )
=> ( 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_x),v_L)
| X0 = v_x ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f528]) ).
fof(f530,plain,
( ! [X4,X5] :
( X4 != X5
=> ( 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,X5,X4),v_L)
| 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,X4,X5),v_L) ) )
& ! [X3] : ~ 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,X3,X3),v_L)
& ! [X0,X1] :
( 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_L)
=> ! [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,X1,X2),v_L)
=> 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,X2),v_L) ) ) ),
inference(rectify,[],[f527]) ).
fof(f531,plain,
~ ( ! [X5,X6] :
( X5 != X6
=> ( ( v_y != X5
& 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_x,X5),v_L)
& v_y = X6 )
| ( v_y != X6
& 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,X6,v_x),v_L)
& v_y = X5 )
| ( v_y != X5
& v_y != X6
& 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,X6,X5),v_L) )
| ( v_y = X5
& v_x = X6 )
| ( v_y != X6
& 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_x,X6),v_L)
& v_y = X5 )
| ( v_y != X5
& 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,X5,v_x),v_L)
& v_y = X6 )
| ( v_y != X6
& v_y != X5
& 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,X5,X6),v_L) )
| ( v_y = X6
& v_x = X5 ) ) )
& ! [X0,X1] :
( ( ( X1 != v_y
& 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_x,X1),v_L)
& X0 = v_y )
=> ! [X4] :
( ( v_y = X4
=> ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) )
& ( ( v_y != X4
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X4),v_L) )
=> 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_x,X4),v_L) )
& ( X1 = v_x
=> v_y != X4 ) ) )
& ( ( X0 != v_y
& 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_x),v_L)
& X1 = v_y )
=> ! [X3] :
( ( v_y != X3
& 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_x,X3),v_L) )
=> 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,X3),v_L) ) )
& ( ( X1 != v_y
& X0 != v_y
& 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_L) )
=> ! [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,X1,v_x),v_L)
& X2 = v_y )
=> ( 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_x),v_L)
| X0 = v_x ) )
& ( ( X2 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L) )
=> 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,X2),v_L) )
& ( ( X2 = v_y
& X1 = v_x )
=> ( 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_x),v_L)
| X0 = v_x ) ) ) ) ) ),
inference(rectify,[],[f529]) ).
fof(f537,plain,
( ! [X4,X5] :
( X4 = X5
| 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,X5,X4),v_L)
| 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,X4,X5),v_L) )
& ! [X3] : ~ 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,X3,X3),v_L)
& ! [X0,X1] :
( ~ 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_L)
| ! [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,X1,X2),v_L)
| 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,X2),v_L) ) ) ),
inference(ennf_transformation,[],[f530]) ).
fof(f538,plain,
( ! [X4,X5] :
( X4 = X5
| 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,X5,X4),v_L)
| 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,X4,X5),v_L) )
& ! [X3] : ~ 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,X3,X3),v_L)
& ! [X0,X1] :
( ~ 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_L)
| ! [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,X1,X2),v_L)
| 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,X2),v_L) ) ) ),
inference(flattening,[],[f537]) ).
fof(f539,plain,
( ? [X5,X6] :
( X5 != X6
& ( v_y = X5
| ~ 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_x,X5),v_L)
| v_y != X6 )
& ( v_y = X6
| ~ 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,X6,v_x),v_L)
| v_y != X5 )
& ( v_y = X5
| v_y = X6
| ~ 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,X6,X5),v_L) )
& ( v_y != X5
| v_x != X6 )
& ( v_y = X6
| ~ 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_x,X6),v_L)
| v_y != X5 )
& ( v_y = X5
| ~ 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,X5,v_x),v_L)
| v_y != X6 )
& ( v_y = X6
| v_y = X5
| ~ 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,X5,X6),v_L) )
& ( v_y != X6
| v_x != X5 ) )
| ? [X0,X1] :
( ( X1 != v_y
& 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_x,X1),v_L)
& X0 = v_y
& ? [X4] :
( ( v_y = X4
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) )
| ( v_y != X4
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X4),v_L)
& ~ 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_x,X4),v_L) )
| ( X1 = v_x
& v_y = X4 ) ) )
| ( X0 != v_y
& 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_x),v_L)
& X1 = v_y
& ? [X3] :
( v_y != X3
& 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_x,X3),v_L)
& ~ 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,X3),v_L) ) )
| ( X1 != v_y
& X0 != v_y
& 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_L)
& ? [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,X1,v_x),v_L)
& X2 = v_y
& ~ 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_x),v_L)
& v_x != X0 )
| ( X2 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
& ~ 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,X2),v_L) )
| ( X2 = v_y
& X1 = v_x
& ~ 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_x),v_L)
& v_x != X0 ) ) ) ) ),
inference(ennf_transformation,[],[f531]) ).
fof(f540,plain,
( ? [X5,X6] :
( X5 != X6
& ( v_y = X5
| ~ 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_x,X5),v_L)
| v_y != X6 )
& ( v_y = X6
| ~ 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,X6,v_x),v_L)
| v_y != X5 )
& ( v_y = X5
| v_y = X6
| ~ 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,X6,X5),v_L) )
& ( v_y != X5
| v_x != X6 )
& ( v_y = X6
| ~ 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_x,X6),v_L)
| v_y != X5 )
& ( v_y = X5
| ~ 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,X5,v_x),v_L)
| v_y != X6 )
& ( v_y = X6
| v_y = X5
| ~ 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,X5,X6),v_L) )
& ( v_y != X6
| v_x != X5 ) )
| ? [X0,X1] :
( ( X1 != v_y
& 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_x,X1),v_L)
& X0 = v_y
& ? [X4] :
( ( v_y = X4
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) )
| ( v_y != X4
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X4),v_L)
& ~ 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_x,X4),v_L) )
| ( X1 = v_x
& v_y = X4 ) ) )
| ( X0 != v_y
& 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_x),v_L)
& X1 = v_y
& ? [X3] :
( v_y != X3
& 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_x,X3),v_L)
& ~ 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,X3),v_L) ) )
| ( X1 != v_y
& X0 != v_y
& 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_L)
& ? [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,X1,v_x),v_L)
& X2 = v_y
& ~ 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_x),v_L)
& v_x != X0 )
| ( X2 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
& ~ 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,X2),v_L) )
| ( X2 = v_y
& X1 = v_x
& ~ 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_x),v_L)
& v_x != X0 ) ) ) ) ),
inference(flattening,[],[f539]) ).
fof(f666,plain,
! [X0,X1,X2] :
( ~ c_member(X2,X1,X0)
| c_Set_Oinsert(X2,X1,X0) = X0 ),
inference(ennf_transformation,[],[f190]) ).
fof(f672,plain,
! [X0,X1,X2,X3] :
( ( ~ c_member(X3,X2,X1)
& X0 != X2 )
| c_member(X3,X2,c_Set_Oinsert(X3,X0,X1)) ),
inference(ennf_transformation,[],[f150]) ).
fof(f675,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_member(X4,X3,c_Relation_OImage(X2,X4,X1,X0))
| ? [X5] :
( c_member(tc_prod(X2,X4),c_Product__Type_OPair(X2,X4,X5,X3),X1)
& c_member(X2,X5,X0) ) ),
inference(ennf_transformation,[],[f475]) ).
fof(f681,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_member(X5,X4,X3)
| ~ c_member(tc_prod(X5,X2),c_Product__Type_OPair(X5,X2,X4,X1),X0)
| c_member(X2,X1,c_Relation_OImage(X5,X2,X0,X3)) ),
inference(ennf_transformation,[],[f330]) ).
fof(f682,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_member(X5,X4,X3)
| ~ c_member(tc_prod(X5,X2),c_Product__Type_OPair(X5,X2,X4,X1),X0)
| c_member(X2,X1,c_Relation_OImage(X5,X2,X0,X3)) ),
inference(flattening,[],[f681]) ).
fof(f738,plain,
( ~ sP5
| ? [X5,X6] :
( X5 != X6
& ( v_y = X5
| ~ 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_x,X5),v_L)
| v_y != X6 )
& ( v_y = X6
| ~ 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,X6,v_x),v_L)
| v_y != X5 )
& ( v_y = X5
| v_y = X6
| ~ 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,X6,X5),v_L) )
& ( v_y != X5
| v_x != X6 )
& ( v_y = X6
| ~ 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_x,X6),v_L)
| v_y != X5 )
& ( v_y = X5
| ~ 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,X5,v_x),v_L)
| v_y != X6 )
& ( v_y = X6
| v_y = X5
| ~ 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,X5,X6),v_L) )
& ( v_y != X6
| v_x != X5 ) ) ),
inference(nnf_transformation,[],[f734]) ).
fof(f739,plain,
( ~ sP5
| ? [X0,X1] :
( X0 != X1
& ( v_y = 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_x,X0),v_L)
| v_y != X1 )
& ( v_y = X1
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L)
| v_y != X0 )
& ( v_y = X0
| v_y = X1
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L) )
& ( v_y != X0
| v_x != X1 )
& ( v_y = X1
| ~ 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_x,X1),v_L)
| v_y != X0 )
& ( v_y = 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,X0,v_x),v_L)
| v_y != X1 )
& ( v_y = X1
| v_y = 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,X0,X1),v_L) )
& ( v_y != X1
| v_x != X0 ) ) ),
inference(rectify,[],[f738]) ).
fof(f740,plain,
( ~ sP5
| ( sK7 != sK8
& ( v_y = sK7
| ~ 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_x,sK7),v_L)
| v_y != sK8 )
& ( v_y = sK8
| ~ 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,sK8,v_x),v_L)
| v_y != sK7 )
& ( v_y = sK7
| v_y = sK8
| ~ 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,sK8,sK7),v_L) )
& ( v_y != sK7
| v_x != sK8 )
& ( v_y = sK8
| ~ 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_x,sK8),v_L)
| v_y != sK7 )
& ( v_y = sK7
| ~ 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,sK7,v_x),v_L)
| v_y != sK8 )
& ( v_y = sK8
| v_y = sK7
| ~ 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,sK7,sK8),v_L) )
& ( v_y != sK8
| v_x != sK7 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X0,sK7),skolemize(X1,sK8)],[f739]) ).
fof(f741,plain,
! [X0,X1] :
( ~ sP4(X0,X1)
| ( X0 != v_y
& 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_x),v_L)
& X1 = v_y
& ? [X3] :
( v_y != X3
& 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_x,X3),v_L)
& ~ 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,X3),v_L) ) ) ),
inference(nnf_transformation,[],[f733]) ).
fof(f742,plain,
! [X0,X1] :
( ~ sP4(X0,X1)
| ( X0 != v_y
& 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_x),v_L)
& X1 = v_y
& ? [X2] :
( v_y != 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,v_x,X2),v_L)
& ~ 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,X2),v_L) ) ) ),
inference(rectify,[],[f741]) ).
fof(f743,plain,
! [X0,X1] :
( ~ sP4(X0,X1)
| ( X0 != v_y
& 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_x),v_L)
& X1 = v_y
& v_y != sK9(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_x,sK9(X0)),v_L)
& ~ 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,sK9(X0)),v_L) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X2,sK9(X0))],[f742]) ).
fof(f744,plain,
! [X1,X0] :
( ~ sP3(X1,X0)
| ( X1 != v_y
& 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_x,X1),v_L)
& X0 = v_y
& ? [X4] :
( ( v_y = X4
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) )
| sP0(X4,X1)
| ( X1 = v_x
& v_y = X4 ) ) ) ),
inference(nnf_transformation,[],[f732]) ).
fof(f745,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| ( v_y != 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_x,X0),v_L)
& v_y = X1
& ? [X2] :
( ( v_y = 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,v_x),v_L) )
| sP0(X2,X0)
| ( v_x = X0
& v_y = X2 ) ) ) ),
inference(rectify,[],[f744]) ).
fof(f746,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| ( v_y != 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_x,X0),v_L)
& v_y = X1
& ( ( v_y = sK10(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,X0,v_x),v_L) )
| sP0(sK10(X0),X0)
| ( v_x = X0
& v_y = sK10(X0) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X2,sK10(X0))],[f745]) ).
fof(f747,plain,
! [X0,X1,X2] :
( ~ sP2(X0,X1,X2)
| ( X2 = v_y
& X1 = v_x
& ~ 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_x),v_L)
& v_x != X0 ) ),
inference(nnf_transformation,[],[f731]) ).
fof(f748,plain,
! [X0,X2,X1] :
( ~ sP1(X0,X2,X1)
| ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L)
& X2 = v_y
& ~ 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_x),v_L)
& v_x != X0 ) ),
inference(nnf_transformation,[],[f730]) ).
fof(f749,plain,
! [X0,X1,X2] :
( ~ sP1(X0,X1,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,X2,v_x),v_L)
& v_y = X1
& ~ 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_x),v_L)
& v_x != X0 ) ),
inference(rectify,[],[f748]) ).
fof(f752,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| ( v_y != sK12
& v_y != sK11
& 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,sK11,sK12),v_L)
& ( sP1(sK11,sK13,sK12)
| ( v_y != sK13
& 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,sK12,sK13),v_L)
& ~ 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,sK11,sK13),v_L) )
| sP2(sK11,sK12,sK13) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13]),skolemize(X0,sK11),skolemize(X1,sK12),skolemize(X2,sK13)],[f735]) ).
fof(f790,plain,
! [X0,X1,X2,X3,X4] :
( ( c_Set_Oinsert(X4,X3,c_Set_Oinsert(X4,X2,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool)))) != c_Set_Oinsert(X4,X1,c_Set_Oinsert(X4,X0,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool))))
| ( X2 = X1
& X3 = X0 )
| ( X2 = X0
& X3 = X1 ) )
& ( ( ( X1 != X2
| X0 != X3 )
& ( X0 != X2
| X1 != X3 ) )
| c_Set_Oinsert(X4,X3,c_Set_Oinsert(X4,X2,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool)))) = c_Set_Oinsert(X4,X1,c_Set_Oinsert(X4,X0,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool)))) ) ),
inference(nnf_transformation,[],[f284]) ).
fof(f791,plain,
! [X0,X1,X2,X3,X4] :
( ( c_Set_Oinsert(X4,X3,c_Set_Oinsert(X4,X2,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool)))) != c_Set_Oinsert(X4,X1,c_Set_Oinsert(X4,X0,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool))))
| ( X2 = X1
& X3 = X0 )
| ( X2 = X0
& X3 = X1 ) )
& ( ( ( X1 != X2
| X0 != X3 )
& ( X0 != X2
| X1 != X3 ) )
| c_Set_Oinsert(X4,X3,c_Set_Oinsert(X4,X2,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool)))) = c_Set_Oinsert(X4,X1,c_Set_Oinsert(X4,X0,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool)))) ) ),
inference(flattening,[],[f790]) ).
fof(f811,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_member(X4,X3,c_Relation_OImage(X2,X4,X1,X0))
| ( c_member(tc_prod(X2,X4),c_Product__Type_OPair(X2,X4,sK37(X0,X1,X2,X3,X4),X3),X1)
& c_member(X2,sK37(X0,X1,X2,X3,X4),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37]),skolemize(X5,sK37(X0,X1,X2,X3,X4))],[f675]) ).
fof(f812,plain,
! [X0,X1,X2,X3,X4] :
( ( ~ c_member(X4,X3,c_Relation_OImage(X2,X4,X1,c_Set_Oinsert(X2,X0,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)))))
| c_member(tc_prod(X2,X4),c_Product__Type_OPair(X2,X4,X0,X3),X1) )
& ( ~ c_member(tc_prod(X2,X4),c_Product__Type_OPair(X2,X4,X0,X3),X1)
| c_member(X4,X3,c_Relation_OImage(X2,X4,X1,c_Set_Oinsert(X2,X0,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool))))) ) ),
inference(nnf_transformation,[],[f353]) ).
fof(f839,plain,
v_x != v_y,
inference(cnf_transformation,[],[f526]) ).
fof(f840,plain,
! [X4,X5] :
( X4 = X5
| 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,X5,X4),v_L)
| 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,X4,X5),v_L) ),
inference(cnf_transformation,[],[f538]) ).
fof(f841,plain,
! [X3] : ~ 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,X3,X3),v_L),
inference(cnf_transformation,[],[f538]) ).
fof(f842,plain,
! [X2,X0,X1] :
( ~ 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_L)
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
| 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,X2),v_L) ),
inference(cnf_transformation,[],[f538]) ).
fof(f843,plain,
( ~ sP5
| sK7 != sK8 ),
inference(cnf_transformation,[],[f740]) ).
fof(f844,plain,
( ~ sP5
| v_y = sK7
| ~ 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_x,sK7),v_L)
| v_y != sK8 ),
inference(cnf_transformation,[],[f740]) ).
fof(f845,plain,
( ~ sP5
| v_y = sK8
| ~ 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,sK8,v_x),v_L)
| v_y != sK7 ),
inference(cnf_transformation,[],[f740]) ).
fof(f846,plain,
( ~ sP5
| v_y = sK7
| v_y = sK8
| ~ 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,sK8,sK7),v_L) ),
inference(cnf_transformation,[],[f740]) ).
fof(f847,plain,
( ~ sP5
| v_y != sK7
| v_x != sK8 ),
inference(cnf_transformation,[],[f740]) ).
fof(f848,plain,
( ~ sP5
| v_y = sK8
| ~ 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_x,sK8),v_L)
| v_y != sK7 ),
inference(cnf_transformation,[],[f740]) ).
fof(f849,plain,
( ~ sP5
| v_y = sK7
| ~ 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,sK7,v_x),v_L)
| v_y != sK8 ),
inference(cnf_transformation,[],[f740]) ).
fof(f850,plain,
( ~ sP5
| v_y = sK8
| v_y = sK7
| ~ 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,sK7,sK8),v_L) ),
inference(cnf_transformation,[],[f740]) ).
fof(f851,plain,
( ~ sP5
| v_y != sK8
| v_x != sK7 ),
inference(cnf_transformation,[],[f740]) ).
fof(f853,plain,
! [X0,X1] :
( ~ sP4(X0,X1)
| 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_x),v_L) ),
inference(cnf_transformation,[],[f743]) ).
fof(f854,plain,
! [X0,X1] :
( ~ sP4(X0,X1)
| v_y = X1 ),
inference(cnf_transformation,[],[f743]) ).
fof(f856,plain,
! [X0,X1] :
( ~ sP4(X0,X1)
| 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_x,sK9(X0)),v_L) ),
inference(cnf_transformation,[],[f743]) ).
fof(f857,plain,
! [X0,X1] :
( ~ sP4(X0,X1)
| ~ 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,sK9(X0)),v_L) ),
inference(cnf_transformation,[],[f743]) ).
fof(f859,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| 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_x,X0),v_L) ),
inference(cnf_transformation,[],[f746]) ).
fof(f860,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| v_y = X1 ),
inference(cnf_transformation,[],[f746]) ).
fof(f862,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| 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_x),v_L)
| sP0(sK10(X0),X0)
| v_x = X0 ),
inference(cnf_transformation,[],[f746]) ).
fof(f865,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,X2)
| v_y = X2 ),
inference(cnf_transformation,[],[f747]) ).
fof(f866,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,X2)
| v_x = X1 ),
inference(cnf_transformation,[],[f747]) ).
fof(f867,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,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,v_x),v_L) ),
inference(cnf_transformation,[],[f747]) ).
fof(f868,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,X2)
| v_x != X0 ),
inference(cnf_transformation,[],[f747]) ).
fof(f869,plain,
! [X2,X0,X1] :
( ~ sP1(X0,X1,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,X2,v_x),v_L) ),
inference(cnf_transformation,[],[f749]) ).
fof(f870,plain,
! [X2,X0,X1] :
( ~ sP1(X0,X1,X2)
| v_y = X1 ),
inference(cnf_transformation,[],[f749]) ).
fof(f871,plain,
! [X2,X0,X1] :
( ~ sP1(X0,X1,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,v_x),v_L) ),
inference(cnf_transformation,[],[f749]) ).
fof(f872,plain,
! [X2,X0,X1] :
( ~ sP1(X0,X1,X2)
| v_x != X0 ),
inference(cnf_transformation,[],[f749]) ).
fof(f877,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| v_y != sK11 ),
inference(cnf_transformation,[],[f752]) ).
fof(f878,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| 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,sK11,sK12),v_L) ),
inference(cnf_transformation,[],[f752]) ).
fof(f879,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| v_y != sK13
| sP2(sK11,sK12,sK13) ),
inference(cnf_transformation,[],[f752]) ).
fof(f880,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| 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,sK12,sK13),v_L)
| sP2(sK11,sK12,sK13) ),
inference(cnf_transformation,[],[f752]) ).
fof(f881,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| ~ 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,sK11,sK13),v_L)
| sP2(sK11,sK12,sK13) ),
inference(cnf_transformation,[],[f752]) ).
fof(f1003,plain,
! [X0,X1] : c_Relation_OImage(X1,X1,c_Relation_OId(X1),X0) = X0,
inference(cnf_transformation,[],[f325]) ).
fof(f1054,plain,
! [X2,X3,X0,X1,X4] :
( c_Set_Oinsert(X4,X3,c_Set_Oinsert(X4,X2,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool)))) != c_Set_Oinsert(X4,X1,c_Set_Oinsert(X4,X0,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool))))
| X1 = X2
| X1 = X3 ),
inference(cnf_transformation,[],[f791]) ).
fof(f1098,plain,
! [X2,X0,X1] :
( ~ c_member(X2,X1,X0)
| c_Set_Oinsert(X2,X1,X0) = X0 ),
inference(cnf_transformation,[],[f666]) ).
fof(f1111,plain,
! [X2,X3,X0,X1] : c_Set_Oinsert(X3,X2,c_Set_Oinsert(X3,X1,X0)) = c_Set_Oinsert(X3,X1,c_Set_Oinsert(X3,X2,X0)),
inference(cnf_transformation,[],[f163]) ).
fof(f1114,plain,
! [X2,X3,X0,X1] :
( X0 != X2
| c_member(X3,X2,c_Set_Oinsert(X3,X0,X1)) ),
inference(cnf_transformation,[],[f672]) ).
fof(f1118,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_member(X4,X3,c_Relation_OImage(X2,X4,X1,X0))
| c_member(X2,sK37(X0,X1,X2,X3,X4),X0) ),
inference(cnf_transformation,[],[f811]) ).
fof(f1122,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_member(X4,X3,c_Relation_OImage(X2,X4,X1,c_Set_Oinsert(X2,X0,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)))))
| c_member(tc_prod(X2,X4),c_Product__Type_OPair(X2,X4,X0,X3),X1) ),
inference(cnf_transformation,[],[f812]) ).
fof(f1127,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_member(X5,X4,X3)
| ~ c_member(tc_prod(X5,X2),c_Product__Type_OPair(X5,X2,X4,X1),X0)
| c_member(X2,X1,c_Relation_OImage(X5,X2,X0,X3)) ),
inference(cnf_transformation,[],[f682]) ).
fof(f1271,plain,
! [X2,X1] : ~ sP2(v_x,X1,X2),
inference(equality_resolution,[],[f868]) ).
fof(f1272,plain,
! [X2,X1] : ~ sP1(v_x,X1,X2),
inference(equality_resolution,[],[f872]) ).
fof(f1310,plain,
! [X2,X3,X1] : c_member(X3,X2,c_Set_Oinsert(X3,X2,X1)),
inference(equality_resolution,[],[f1114]) ).
tcf(c_50,plain,
v_x != v_y,
inference(cnf_transformation,[],[f839]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $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,X2),v_L)
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
| ~ 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_L) ),
inference(cnf_transformation,[],[f842]) ).
tcf(c_52,plain,
! [X0: $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,X0),v_L),
inference(cnf_transformation,[],[f841]) ).
tcf(c_53,plain,
! [X0: $i,X1: $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,X1,X0),v_L)
| 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_L)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f840]) ).
tcf(c_54,plain,
( ~ sP5
| ( v_y != sK8 )
| ( v_x != sK7 ) ),
inference(cnf_transformation,[],[f851]) ).
tcf(c_55,plain,
( ( v_y = sK8 )
| ( v_y = sK7 )
| ~ sP5
| ~ 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,sK7,sK8),v_L) ),
inference(cnf_transformation,[],[f850]) ).
tcf(c_56,plain,
( ( v_y = sK7 )
| ~ sP5
| ~ 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,sK7,v_x),v_L)
| ( v_y != sK8 ) ),
inference(cnf_transformation,[],[f849]) ).
tcf(c_57,plain,
( ( v_y = sK8 )
| ~ sP5
| ~ 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_x,sK8),v_L)
| ( v_y != sK7 ) ),
inference(cnf_transformation,[],[f848]) ).
tcf(c_58,plain,
( ~ sP5
| ( v_y != sK7 )
| ( v_x != sK8 ) ),
inference(cnf_transformation,[],[f847]) ).
tcf(c_59,plain,
( ( v_y = sK8 )
| ( v_y = sK7 )
| ~ sP5
| ~ 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,sK8,sK7),v_L) ),
inference(cnf_transformation,[],[f846]) ).
tcf(c_60,plain,
( ( v_y = sK8 )
| ~ sP5
| ~ 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,sK8,v_x),v_L)
| ( v_y != sK7 ) ),
inference(cnf_transformation,[],[f845]) ).
tcf(c_61,plain,
( ( v_y = sK7 )
| ~ sP5
| ~ 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_x,sK7),v_L)
| ( v_y != sK8 ) ),
inference(cnf_transformation,[],[f844]) ).
tcf(c_62,plain,
( ~ sP5
| ( sK7 != sK8 ) ),
inference(cnf_transformation,[],[f843]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] :
( ~ sP4(X0,X1)
| ~ 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,sK9(X0)),v_L) ),
inference(cnf_transformation,[],[f857]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK9(X0)),v_L)
| ~ sP4(X0,X1) ),
inference(cnf_transformation,[],[f856]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] :
( ( X1 = v_y )
| ~ sP4(X0,X1) ),
inference(cnf_transformation,[],[f854]) ).
tcf(c_67,plain,
! [X0: $i,X1: $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_x),v_L)
| ~ sP4(X0,X1) ),
inference(cnf_transformation,[],[f853]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( sP0(sK10(X0),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,X0,v_x),v_L)
| ( X0 = v_x )
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f862]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( ( X1 = v_y )
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f860]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X0),v_L)
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f859]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i] : ~ sP2(v_x,X0,X1),
inference(cnf_transformation,[],[f1271]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sP2(X0,X1,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,v_x),v_L) ),
inference(cnf_transformation,[],[f867]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = v_x )
| ~ sP2(X0,X1,X2) ),
inference(cnf_transformation,[],[f866]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = v_y )
| ~ sP2(X0,X1,X2) ),
inference(cnf_transformation,[],[f865]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] : ~ sP1(v_x,X0,X1),
inference(cnf_transformation,[],[f1272]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sP1(X0,X1,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,v_x),v_L) ),
inference(cnf_transformation,[],[f871]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = v_y )
| ~ sP1(X0,X1,X2) ),
inference(cnf_transformation,[],[f870]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $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,X2,v_x),v_L)
| ~ sP1(X0,X1,X2) ),
inference(cnf_transformation,[],[f869]) ).
tcf(c_87,negated_conjecture,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| sP2(sK11,sK12,sK13)
| ~ 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,sK11,sK13),v_L) ),
inference(cnf_transformation,[],[f881]) ).
tcf(c_88,negated_conjecture,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| sP2(sK11,sK12,sK13)
| 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,sK12,sK13),v_L) ),
inference(cnf_transformation,[],[f880]) ).
tcf(c_89,negated_conjecture,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| sP2(sK11,sK12,sK13)
| ( v_y != sK13 ) ),
inference(cnf_transformation,[],[f879]) ).
tcf(c_90,negated_conjecture,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| 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,sK11,sK12),v_L) ),
inference(cnf_transformation,[],[f878]) ).
tcf(c_91,negated_conjecture,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| ( v_y != sK11 ) ),
inference(cnf_transformation,[],[f877]) ).
tcf(c_202,plain,
! [X0: $i,X1: $i] : c_Relation_OImage(X0,X0,c_Relation_OId(X0),X1) = X1,
inference(cnf_transformation,[],[f1003]) ).
tcf(c_251,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X2 = X3 )
| ( X1 = X3 )
| ( c_Set_Oinsert(X0,X1,c_Set_Oinsert(X0,X2,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))) != c_Set_Oinsert(X0,X3,c_Set_Oinsert(X0,X4,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))) ) ),
inference(cnf_transformation,[],[f1054]) ).
tcf(c_292,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_Set_Oinsert(X0,X1,X2) = X2 )
| ~ c_member(X0,X1,X2) ),
inference(cnf_transformation,[],[f1098]) ).
tcf(c_305,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_Set_Oinsert(X0,X1,c_Set_Oinsert(X0,X2,X3)) = c_Set_Oinsert(X0,X2,c_Set_Oinsert(X0,X1,X3)),
inference(cnf_transformation,[],[f1111]) ).
tcf(c_307,plain,
! [X0: $i,X1: $i,X2: $i] : c_member(X0,X1,c_Set_Oinsert(X0,X1,X2)),
inference(cnf_transformation,[],[f1310]) ).
tcf(c_311,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_member(X2,sK37(X4,X3,X2,X1,X0),X4)
| ~ c_member(X0,X1,c_Relation_OImage(X2,X0,X3,X4)) ),
inference(cnf_transformation,[],[f1118]) ).
tcf(c_317,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_member(tc_prod(X2,X0),c_Product__Type_OPair(X2,X0,X4,X1),X3)
| ~ c_member(X0,X1,c_Relation_OImage(X2,X0,X3,c_Set_Oinsert(X2,X4,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool))))) ),
inference(cnf_transformation,[],[f1122]) ).
tcf(c_321,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( c_member(X1,X3,c_Relation_OImage(X0,X1,X4,X5))
| ~ c_member(X0,X2,X5)
| ~ c_member(tc_prod(X0,X1),c_Product__Type_OPair(X0,X1,X2,X3),X4) ),
inference(cnf_transformation,[],[f1127]) ).
tcf(c_696,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sP2(X0,X1,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,v_x),v_L) ),
inference(prop_impl_just,[status(thm)],[c_77]) ).
tcf(c_698,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sP1(X0,X1,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,v_x),v_L) ),
inference(prop_impl_just,[status(thm)],[c_81]) ).
tcf(c_700,plain,
! [X0: $i,X1: $i] :
( ( X1 = v_y )
| ~ sP3(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_73]) ).
tcf(c_702,plain,
! [X0: $i,X1: $i] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X0),v_L)
| ~ sP3(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_74]) ).
tcf(c_710,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = v_x )
| ~ sP2(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_78]) ).
tcf(c_712,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = v_y )
| ~ sP2(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_79]) ).
tcf(c_714,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = v_y )
| ~ sP1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_82]) ).
tcf(c_718,plain,
! [X0: $i,X1: $i,X2: $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,X2,v_x),v_L)
| ~ sP1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_83]) ).
tcf(c_4196,plain,
! [X0: $i,X1: $i] :
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| ( v_y != sK13 )
| ( v_x != sK11 )
| ( X1 != sK13 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_76,c_89]) ).
tcf(c_4197,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| ( v_y != sK13 )
| ( v_x != sK11 ) ),
inference(unflattening,[status(thm)],[c_4196]) ).
tcf(c_4276,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| 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,sK12,sK13),v_L)
| ( X2 = v_y )
| ( X2 != sK13 )
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_712,c_88]) ).
tcf(c_4277,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| 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,sK12,sK13),v_L)
| ( sK13 = v_y ) ),
inference(unflattening,[status(thm)],[c_4276]) ).
tcf(c_4290,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| ( sK13 = v_y ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4277,c_714]) ).
tcf(c_4296,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| ( X2 = v_y )
| ~ 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,sK11,sK13),v_L)
| ( X2 != sK13 )
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_712,c_87]) ).
tcf(c_4297,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| ( sK13 = v_y )
| ~ 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,sK11,sK13),v_L) ),
inference(unflattening,[status(thm)],[c_4296]) ).
tcf(c_4310,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| ( sK13 = v_y )
| ~ 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,sK11,sK13),v_L) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4297,c_714]) ).
tcf(c_4336,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| 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,sK12,sK13),v_L)
| ( X1 = v_x )
| ( X2 != sK13 )
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_710,c_88]) ).
tcf(c_4337,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| 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,sK12,sK13),v_L)
| ( sK12 = v_x ) ),
inference(unflattening,[status(thm)],[c_4336]) ).
tcf(c_4356,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| ( X1 = v_x )
| ~ 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,sK11,sK13),v_L)
| ( X2 != sK13 )
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_710,c_87]) ).
tcf(c_4357,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| ( sK12 = v_x )
| ~ 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,sK11,sK13),v_L) ),
inference(unflattening,[status(thm)],[c_4356]) ).
tcf(c_4376,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| ~ 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_x),v_L)
| ( v_y != sK13 )
| ( X2 != sK13 )
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_696,c_89]) ).
tcf(c_4377,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| ~ 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,sK11,v_x),v_L)
| ( v_y != sK13 ) ),
inference(unflattening,[status(thm)],[c_4376]) ).
tcf(c_4390,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| ~ 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,sK11,v_x),v_L)
| ( v_y != sK13 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4377,c_698]) ).
tcf(c_4396,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| 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,sK12,sK13),v_L)
| ~ 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_x),v_L)
| ( X2 != sK13 )
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_696,c_88]) ).
tcf(c_4397,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| 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,sK12,sK13),v_L)
| ~ 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,sK11,v_x),v_L) ),
inference(unflattening,[status(thm)],[c_4396]) ).
tcf(c_4410,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| ~ 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,sK11,v_x),v_L) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4397,c_698]) ).
tcf(c_4416,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| ~ 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,sK11,sK13),v_L)
| ~ 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_x),v_L)
| ( X2 != sK13 )
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_696,c_87]) ).
tcf(c_4417,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| sP1(sK11,sK13,sK12)
| ~ 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,sK11,sK13),v_L)
| ~ 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,sK11,v_x),v_L) ),
inference(unflattening,[status(thm)],[c_4416]) ).
tcf(c_4430,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| ~ 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,sK11,sK13),v_L)
| ~ 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,sK11,v_x),v_L) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4417,c_698]) ).
tcf(c_4746,plain,
! [X0: $i,X1: $i] :
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| ( v_y != sK13 )
| ( v_x != sK11 )
| ( X1 != sK12 )
| ( X0 != sK13 ) ),
inference(resolution_lifted,[status(thm)],[c_80,c_4197]) ).
tcf(c_4747,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| ( v_y != sK13 )
| ( v_x != sK11 ) ),
inference(unflattening,[status(thm)],[c_4746]) ).
tcf(c_4763,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| 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,X2,v_x),v_L)
| ( v_x = sK12 )
| ~ 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,sK11,sK13),v_L)
| ( X2 != sK12 )
| ( X1 != sK13 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_718,c_4357]) ).
tcf(c_4764,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| ( v_x = sK12 )
| ~ 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,sK11,sK13),v_L) ),
inference(unflattening,[status(thm)],[c_4763]) ).
tcf(c_4783,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| 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,X2,v_x),v_L)
| ( v_x = sK12 )
| ( X2 != sK12 )
| ( X1 != sK13 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_718,c_4337]) ).
tcf(c_4784,plain,
( sP5
| sP3(sK12,sK11)
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| 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,sK12,v_x),v_L)
| ( v_x = sK12 ) ),
inference(unflattening,[status(thm)],[c_4783]) ).
tcf(c_4908,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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_x,X0),v_L)
| ( v_y != sK13 )
| ( v_x != sK11 )
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_702,c_4747]) ).
tcf(c_4909,plain,
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L)
| ( v_y != sK13 )
| ( v_x != sK11 ) ),
inference(unflattening,[status(thm)],[c_4908]) ).
tcf(c_4976,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| 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_x,X0),v_L)
| ~ 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,sK11,v_x),v_L)
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_702,c_4410]) ).
tcf(c_4977,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| 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_x,sK12),v_L)
| ~ 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,sK11,v_x),v_L) ),
inference(unflattening,[status(thm)],[c_4976]) ).
tcf(c_4993,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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_x,X0),v_L)
| ~ 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,sK11,v_x),v_L)
| ( v_y != sK13 )
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_702,c_4390]) ).
tcf(c_4994,plain,
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L)
| ~ 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,sK11,v_x),v_L)
| ( v_y != sK13 ) ),
inference(unflattening,[status(thm)],[c_4993]) ).
tcf(c_5027,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| 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_x,X0),v_L)
| ( v_y = sK13 )
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_702,c_4290]) ).
tcf(c_5028,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| 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_x,sK12),v_L)
| ( v_y = sK13 ) ),
inference(unflattening,[status(thm)],[c_5027]) ).
tcf(c_5060,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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_x,X0),v_L)
| ( v_y != sK11 )
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_702,c_91]) ).
tcf(c_5061,plain,
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L)
| ( v_y != sK11 ) ),
inference(unflattening,[status(thm)],[c_5060]) ).
tcf(c_5074,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK11,sK12),v_L)
| 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_x,X0),v_L)
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_702,c_90]) ).
tcf(c_5075,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK11,sK12),v_L)
| 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_x,sK12),v_L) ),
inference(unflattening,[status(thm)],[c_5074]) ).
tcf(c_5108,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| 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,sK12,v_x),v_L)
| ( v_x = sK12 )
| ( X1 = v_y )
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_700,c_4784]) ).
tcf(c_5109,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| 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,sK12,v_x),v_L)
| ( sK11 = v_y )
| ( v_x = sK12 ) ),
inference(unflattening,[status(thm)],[c_5108]) ).
tcf(c_5128,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| ( v_x = sK12 )
| ( X1 = v_y )
| ~ 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,sK11,sK13),v_L)
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_700,c_4764]) ).
tcf(c_5129,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| ( sK11 = v_y )
| ( v_x = sK12 )
| ~ 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,sK11,sK13),v_L) ),
inference(unflattening,[status(thm)],[c_5128]) ).
tcf(c_5148,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| ( X1 = v_y )
| ( v_y != sK13 )
| ( v_x != sK11 )
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_700,c_4747]) ).
tcf(c_5149,plain,
( sP5
| sP4(sK11,sK12)
| ( sK11 = v_y )
| ( v_y != sK13 )
| ( v_x != sK11 ) ),
inference(unflattening,[status(thm)],[c_5148]) ).
tcf(c_5199,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| ( X1 = v_y )
| ~ 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,sK11,sK13),v_L)
| ~ 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,sK11,v_x),v_L)
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_700,c_4430]) ).
tcf(c_5200,plain,
( sP5
| sP4(sK11,sK12)
| ( sK11 = v_y )
| ~ 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,sK11,sK13),v_L)
| ~ 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,sK11,v_x),v_L) ),
inference(unflattening,[status(thm)],[c_5199]) ).
tcf(c_5216,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| ( X1 = v_y )
| ~ 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,sK11,v_x),v_L)
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_700,c_4410]) ).
tcf(c_5217,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| ( sK11 = v_y )
| ~ 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,sK11,v_x),v_L) ),
inference(unflattening,[status(thm)],[c_5216]) ).
tcf(c_5233,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| ( X1 = v_y )
| ~ 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,sK11,v_x),v_L)
| ( v_y != sK13 )
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_700,c_4390]) ).
tcf(c_5234,plain,
( sP5
| sP4(sK11,sK12)
| ( sK11 = v_y )
| ~ 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,sK11,v_x),v_L)
| ( v_y != sK13 ) ),
inference(unflattening,[status(thm)],[c_5233]) ).
tcf(c_5250,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| ( v_y = sK13 )
| ( X1 = v_y )
| ~ 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,sK11,sK13),v_L)
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_700,c_4310]) ).
tcf(c_5251,plain,
( sP5
| sP4(sK11,sK12)
| ( sK11 = v_y )
| ( v_y = sK13 )
| ~ 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,sK11,sK13),v_L) ),
inference(unflattening,[status(thm)],[c_5250]) ).
tcf(c_5267,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| ( v_y = sK13 )
| ( X1 = v_y )
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_700,c_4290]) ).
tcf(c_5268,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| ( sK11 = v_y )
| ( v_y = sK13 ) ),
inference(unflattening,[status(thm)],[c_5267]) ).
tcf(c_5314,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK11,sK12),v_L)
| ( X1 = v_y )
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_700,c_90]) ).
tcf(c_5315,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK11,sK12),v_L)
| ( sK11 = v_y ) ),
inference(unflattening,[status(thm)],[c_5314]) ).
tcf(c_5603,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| sP0(sK10(X0),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,X0,v_x),v_L)
| ( X0 = v_x )
| ( v_y != sK11 )
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_71,c_91]) ).
tcf(c_5604,plain,
( sP5
| sP4(sK11,sK12)
| sP0(sK10(sK12),sK12)
| 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,sK12,v_x),v_L)
| ( sK12 = v_x )
| ( v_y != sK11 ) ),
inference(unflattening,[status(thm)],[c_5603]) ).
tcf(c_5623,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| sP0(sK10(X0),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,sK11,sK12),v_L)
| 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_x),v_L)
| ( X0 = v_x )
| ( X1 != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_71,c_90]) ).
tcf(c_5624,plain,
( sP5
| sP4(sK11,sK12)
| sP0(sK10(sK12),sK12)
| 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,sK12,v_x),v_L)
| 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,sK11,sK12),v_L)
| ( sK12 = v_x ) ),
inference(unflattening,[status(thm)],[c_5623]) ).
tcf(c_12139,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_18238,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| ( v_y = sK11 )
| ( v_x = sK12 )
| ( c_Set_Oinsert(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,sK12,sK13),v_L) = v_L ) ),
inference(superposition,[status(thm)],[c_5109,c_292]) ).
tcf(c_18483,plain,
( sP5
| sP4(sK11,sK12)
| ( v_y = sK11 )
| ( v_x = sK12 )
| ( c_Set_Oinsert(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,sK12,sK13),v_L) = v_L )
| ( c_Set_Oinsert(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,sK12,v_x),v_L) = v_L ) ),
inference(superposition,[status(thm)],[c_18238,c_292]) ).
tcf(c_19352,plain,
( sP5
| 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,sK11,v_x),v_L)
| ( v_y = sK11 )
| ( v_x = sK12 )
| ( c_Set_Oinsert(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,sK12,sK13),v_L) = v_L )
| ( c_Set_Oinsert(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,sK12,v_x),v_L) = v_L ) ),
inference(superposition,[status(thm)],[c_18483,c_67]) ).
tcf(c_19894,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| 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_x,sK12),v_L)
| ( v_y = sK11 )
| ( v_x = sK12 )
| ( c_Set_Oinsert(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,sK12,sK13),v_L) = v_L )
| ( c_Set_Oinsert(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,sK12,v_x),v_L) = v_L ) ),
inference(superposition,[status(thm)],[c_19352,c_4977]) ).
tcf(c_19928,plain,
( sP5
| sP4(sK11,sK12)
| ( v_x = sK12 )
| ( c_Set_Oinsert(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,sK12,sK13),v_L) = v_L )
| ( c_Set_Oinsert(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,sK12,v_x),v_L) = v_L )
| 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_x,sK12),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_19894,c_5061,c_18483]) ).
tcf(c_19929,plain,
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L)
| ( v_x = sK12 )
| ( c_Set_Oinsert(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,sK12,sK13),v_L) = v_L )
| ( c_Set_Oinsert(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,sK12,v_x),v_L) = v_L ) ),
inference(renaming,[status(thm)],[c_19928]) ).
tcf(c_19942,plain,
( sP5
| sP4(sK11,sK12)
| ( v_x = sK12 )
| ( c_Set_Oinsert(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,sK12,sK13),v_L) = v_L )
| ( c_Set_Oinsert(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,sK12,v_x),v_L) = v_L )
| ( c_Set_Oinsert(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_x,sK12),v_L) = v_L ) ),
inference(superposition,[status(thm)],[c_19929,c_292]) ).
tcf(c_19963,plain,
( sP5
| ( v_y = sK12 )
| ( v_x = sK12 )
| ( c_Set_Oinsert(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,sK12,sK13),v_L) = v_L )
| ( c_Set_Oinsert(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,sK12,v_x),v_L) = v_L )
| ( c_Set_Oinsert(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_x,sK12),v_L) = v_L ) ),
inference(superposition,[status(thm)],[c_19942,c_66]) ).
tcf(c_20535,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,sK7,v_x),v_L)
| 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_x,sK7),v_L)
| ( v_x = sK7 ) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_20538,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,sK8,v_x),v_L)
| 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_x,sK8),v_L)
| ( v_x = sK8 ) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_20539,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,sK8,sK7),v_L)
| 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,sK7,sK8),v_L)
| ( sK7 = sK8 ) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_22441,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_member(X0,sK37(X2,c_Relation_OId(X0),X0,X1,X0),X2)
| ~ c_member(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_202,c_311]) ).
tcf(c_22574,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_Set_Oinsert(X0,sK37(X2,c_Relation_OId(X0),X0,X1,X0),X2) = X2 )
| ~ c_member(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_22441,c_292]) ).
tcf(c_25453,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v_x = v_y )
| ( X1 = v_y )
| ( c_Set_Oinsert(X0,v_x,c_Set_Oinsert(X0,X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))) != c_Set_Oinsert(X0,v_y,c_Set_Oinsert(X0,X2,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))) ) ),
inference(instantiation,[status(thm)],[c_251]) ).
tcf(c_25492,plain,
( ( v_y = sK8 )
| ( v_y = sK7 )
| ~ sP5 ),
inference(global_subsumption_just,[status(thm)],[c_55,c_62,c_54,c_59,c_55,c_61,c_56,c_20535,c_20539]) ).
tcf(c_25494,plain,
( ( v_y = sK8 )
| ~ sP5 ),
inference(global_subsumption_just,[status(thm)],[c_25492,c_58,c_60,c_57,c_20538,c_25492]) ).
tcf(c_25500,plain,
( ~ sP5
| ( v_x != sK7 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_54,c_25494]) ).
tcf(c_25514,plain,
( ( v_y = sK12 )
| ( v_y = sK8 )
| ( v_x = sK12 )
| ( c_Set_Oinsert(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,sK12,sK13),v_L) = v_L )
| ( c_Set_Oinsert(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,sK12,v_x),v_L) = v_L )
| ( c_Set_Oinsert(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_x,sK12),v_L) = v_L ) ),
inference(superposition,[status(thm)],[c_19963,c_25494]) ).
tcf(c_28249,plain,
( ( v_y = sK7 )
| ~ sP5 ),
inference(global_subsumption_just,[status(thm)],[c_56,c_61,c_56,c_20535,c_25494,c_25500]) ).
tcf(c_32495,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,sK13),v_L)
| 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_x,sK11),v_L)
| ( v_y = sK11 )
| ( v_x = sK11 ) ),
inference(superposition,[status(thm)],[c_53,c_5217]) ).
tcf(c_36187,plain,
! [X0: $i] :
( sP5
| sP4(sK11,sK12)
| c_member(tc_Arrow__Order__Mirabelle_Oalt,sK12,c_Relation_OImage(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_L,X0))
| ( v_y = sK11 )
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,sK11,X0) ),
inference(superposition,[status(thm)],[c_5315,c_321]) ).
tcf(c_36874,plain,
( ~ sP4(sK11,sK12)
| ~ 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,sK11,sK9(sK11)),v_L) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_36875,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,sK11,v_x),v_L)
| ~ sP4(sK11,sK12) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_36877,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_x,sK9(sK11)),v_L)
| ~ sP4(sK11,sK12) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_39236,plain,
! [X0: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK12),v_L)
| ( v_y = sK11 )
| ~ c_member(tc_Arrow__Order__Mirabelle_Oalt,sK11,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(superposition,[status(thm)],[c_36187,c_317]) ).
tcf(c_40627,plain,
! [X0: $i] :
( ( v_y = v_y )
| ( v_x = v_y )
| ( c_Set_Oinsert(X0,v_x,c_Set_Oinsert(X0,v_y,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))) != c_Set_Oinsert(X0,v_y,c_Set_Oinsert(X0,v_x,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))) ) ),
inference(instantiation,[status(thm)],[c_25453]) ).
tcf(c_40628,plain,
! [X0: $i] : c_Set_Oinsert(X0,v_x,c_Set_Oinsert(X0,v_y,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))) = c_Set_Oinsert(X0,v_y,c_Set_Oinsert(X0,v_x,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_41082,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK11,sK12),v_L)
| ( v_y = sK11 ) ),
inference(superposition,[status(thm)],[c_307,c_39236]) ).
tcf(c_53731,plain,
! [X0: $i] :
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L)
| 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,sK11,X0),v_L)
| ~ 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,sK12,X0),v_L) ),
inference(superposition,[status(thm)],[c_5075,c_51]) ).
tcf(c_53732,plain,
! [X0: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK11,X0),v_L)
| ( v_y = sK11 )
| ~ 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,sK12,X0),v_L) ),
inference(superposition,[status(thm)],[c_5315,c_51]) ).
tcf(c_55799,plain,
! [X0: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK11,X0),v_L)
| 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,sK12),v_L)
| ( v_y = sK11 )
| ( X0 = sK12 ) ),
inference(superposition,[status(thm)],[c_53,c_53732]) ).
tcf(c_55802,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK11,sK13),v_L)
| 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_x,sK11),v_L)
| ( v_y = sK11 )
| ( v_x = sK11 ) ),
inference(superposition,[status(thm)],[c_32495,c_53732]) ).
tcf(c_55805,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| 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,sK11,sK13),v_L)
| ( v_y = sK11 )
| ( v_x = sK12 ) ),
inference(superposition,[status(thm)],[c_5109,c_53732]) ).
tcf(c_55807,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK11,sK13),v_L)
| ( v_y = sK13 )
| ( v_y = sK11 ) ),
inference(superposition,[status(thm)],[c_5268,c_53732]) ).
tcf(c_56035,plain,
! [X0: $i] :
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L)
| 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,sK11,X0),v_L)
| 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,sK12),v_L)
| ( X0 = sK12 ) ),
inference(superposition,[status(thm)],[c_53,c_53731]) ).
tcf(c_56042,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK11,sK13),v_L)
| 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_x,sK12),v_L)
| ( v_y = sK13 ) ),
inference(superposition,[status(thm)],[c_5028,c_53731]) ).
tcf(c_56355,plain,
( sP5
| sP4(sK11,sK12)
| ( v_y = sK13 )
| ( v_y = sK11 ) ),
inference(superposition,[status(thm)],[c_55807,c_5251]) ).
tcf(c_56372,plain,
( sP5
| sP4(sK11,sK12)
| ( v_y = sK13 )
| 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_x,sK12),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_56042,c_5061,c_56355]) ).
tcf(c_56373,plain,
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L)
| ( v_y = sK13 ) ),
inference(renaming,[status(thm)],[c_56372]) ).
tcf(c_56382,plain,
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L)
| ( v_x != sK11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4909,c_56373]) ).
tcf(c_56383,plain,
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L)
| ~ 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,sK11,v_x),v_L) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4994,c_56373]) ).
tcf(c_56465,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK13,sK12),v_L)
| ( sK12 = sK13 )
| ( v_y = sK13 )
| ( v_y = sK11 ) ),
inference(superposition,[status(thm)],[c_55799,c_5251]) ).
tcf(c_56833,plain,
( sP5
| sP4(sK11,sK12)
| 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_x,sK11),v_L)
| ( v_y = sK11 )
| ( v_x = sK11 )
| ~ 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,sK11,v_x),v_L) ),
inference(superposition,[status(thm)],[c_55802,c_5200]) ).
tcf(c_57006,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK11,sK13),v_L)
| 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,sK11,v_x),v_L)
| ( v_y = sK11 )
| ( v_x = sK12 ) ),
inference(superposition,[status(thm)],[c_55805,c_53732]) ).
tcf(c_59900,plain,
( sP5
| ( v_x = sK12 )
| ( v_y = sK11 )
| 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,sK11,v_x),v_L)
| 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,sK11,sK13),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_57006,c_36875,c_57006]) ).
tcf(c_59901,plain,
( sP5
| 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,sK11,sK13),v_L)
| 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,sK11,v_x),v_L)
| ( v_y = sK11 )
| ( v_x = sK12 ) ),
inference(renaming,[status(thm)],[c_59900]) ).
tcf(c_96172,plain,
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L)
| ( c_Set_Oinsert(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK37(v_L,c_Relation_OId(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),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,sK11,sK12),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),v_L) = v_L ) ),
inference(superposition,[status(thm)],[c_5075,c_22574]) ).
tcf(c_102395,plain,
! [X0: $i] :
( sP5
| sP4(sK11,sK12)
| 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_x,X0),v_L)
| ( c_Set_Oinsert(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK37(v_L,c_Relation_OId(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),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,sK11,sK12),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),v_L) = v_L )
| ~ 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,sK12,X0),v_L) ),
inference(superposition,[status(thm)],[c_96172,c_51]) ).
tcf(c_139157,plain,
! [X0: $i] :
( ( v_x = v_y )
| ( v_y != X0 )
| ( v_x != X0 ) ),
inference(instantiation,[status(thm)],[c_12139]) ).
tcf(c_140565,plain,
! [X0: $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,sK11,X0),v_L)
| ~ 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,sK11,v_x),v_L)
| ~ 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_x,X0),v_L) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_140698,plain,
! [X0: $i,X1: $i] :
( ( v_y = X0 )
| ( v_y != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_12139]) ).
tcf(c_143283,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,sK11,sK11),v_L)
| ~ 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,sK11,v_x),v_L)
| ~ 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_x,sK11),v_L) ),
inference(instantiation,[status(thm)],[c_140565]) ).
tcf(c_143284,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,sK11,sK11),v_L),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_143303,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,sK11,sK9(sK11)),v_L)
| ~ 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,sK11,v_x),v_L)
| ~ 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_x,sK9(sK11)),v_L) ),
inference(instantiation,[status(thm)],[c_140565]) ).
tcf(c_144368,plain,
! [X0: $i] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X0),v_L)
| ~ 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_x,sK12),v_L)
| ~ 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,sK12,X0),v_L) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_145108,plain,
! [X0: $i] :
( ( v_y = X0 )
| ( v_y != v_y )
| ( X0 != v_y ) ),
inference(instantiation,[status(thm)],[c_140698]) ).
tcf(c_150433,plain,
( ( v_y = sK11 )
| ( sK11 != v_y )
| ( v_y != v_y ) ),
inference(instantiation,[status(thm)],[c_145108]) ).
tcf(c_150537,plain,
( ( v_x = v_y )
| ( v_y != sK11 )
| ( v_x != sK11 ) ),
inference(instantiation,[status(thm)],[c_139157]) ).
tcf(c_171376,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_x,sK10(sK12)),v_L)
| ~ 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_x,sK12),v_L)
| ~ 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,sK12,sK10(sK12)),v_L) ),
inference(instantiation,[status(thm)],[c_144368]) ).
tcf(c_178971,plain,
( sP5
| sP4(sK11,sK12)
| ( v_x != sK11 ) ),
inference(global_subsumption_just,[status(thm)],[c_56382,c_50,c_5149,c_36877,c_36875,c_36874,c_40627,c_40628,c_56355,c_143303,c_150433,c_150537]) ).
tcf(c_178973,plain,
( sP5
| ( v_x != sK11 ) ),
inference(global_subsumption_just,[status(thm)],[c_178971,c_36877,c_36875,c_36874,c_143303,c_178971]) ).
tcf(c_184537,plain,
( sP5
| ~ 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,sK11,v_x),v_L)
| 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_x,sK12),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_56383,c_36877,c_36875,c_36874,c_56383,c_143303]) ).
tcf(c_184538,plain,
( sP5
| 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_x,sK12),v_L)
| ~ 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,sK11,v_x),v_L) ),
inference(renaming,[status(thm)],[c_184537]) ).
tcf(c_184565,plain,
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L)
| ( v_x = sK12 ) ),
inference(superposition,[status(thm)],[c_56035,c_184538]) ).
tcf(c_184804,plain,
( sP5
| ( v_x = sK12 )
| 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_x,sK12),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_184565,c_36877,c_36875,c_36874,c_143303,c_184565]) ).
tcf(c_184805,plain,
( sP5
| 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_x,sK12),v_L)
| ( v_x = sK12 ) ),
inference(renaming,[status(thm)],[c_184804]) ).
tcf(c_185340,plain,
( sP5
| ( v_y = sK11 )
| ( v_y = sK13 ) ),
inference(global_subsumption_just,[status(thm)],[c_56465,c_36877,c_36875,c_36874,c_56355,c_143303]) ).
tcf(c_185341,plain,
( sP5
| ( v_y = sK13 )
| ( v_y = sK11 ) ),
inference(renaming,[status(thm)],[c_185340]) ).
tcf(c_185348,plain,
( ( v_y = sK13 )
| ( v_y = sK11 )
| ( v_y = sK7 ) ),
inference(superposition,[status(thm)],[c_185341,c_28249]) ).
tcf(c_185383,plain,
( sP5
| sP4(sK11,sK12)
| ( v_y = sK11 )
| ( v_y = sK7 )
| ~ 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,sK11,v_x),v_L) ),
inference(superposition,[status(thm)],[c_185348,c_5234]) ).
tcf(c_187445,plain,
( sP5
| ~ 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,sK11,v_x),v_L)
| ( v_y = sK11 ) ),
inference(global_subsumption_just,[status(thm)],[c_185383,c_36877,c_36875,c_36874,c_56833,c_143283,c_143284,c_143303,c_178973]) ).
tcf(c_187446,plain,
( sP5
| ( v_y = sK11 )
| ~ 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,sK11,v_x),v_L) ),
inference(renaming,[status(thm)],[c_187445]) ).
tcf(c_187457,plain,
( sP5
| 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,sK11,sK13),v_L)
| ( v_y = sK11 )
| ( v_x = sK12 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_59901,c_187446]) ).
tcf(c_187523,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| ( v_y = sK11 )
| ( v_x = sK12 ) ),
inference(superposition,[status(thm)],[c_187457,c_5129]) ).
fof(f729,definition,
! [X4,X1] :
( ~ sP0(X4,X1)
| ( v_y != X4
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X4),v_L)
& ~ 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_x,X4),v_L) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f730,definition,
! [X0,X2,X1] :
( ~ sP1(X0,X2,X1)
| ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L)
& X2 = v_y
& ~ 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_x),v_L)
& v_x != X0 ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f731,definition,
! [X0,X1,X2] :
( ~ sP2(X0,X1,X2)
| ( X2 = v_y
& X1 = v_x
& ~ 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_x),v_L)
& v_x != X0 ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f732,definition,
! [X1,X0] :
( ~ sP3(X1,X0)
| ( X1 != v_y
& 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_x,X1),v_L)
& X0 = v_y
& ? [X4] :
( ( v_y = X4
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) )
| sP0(X4,X1)
| ( X1 = v_x
& v_y = X4 ) ) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f733,definition,
! [X0,X1] :
( ~ sP4(X0,X1)
| ( X0 != v_y
& 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_x),v_L)
& X1 = v_y
& ? [X3] :
( v_y != X3
& 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_x,X3),v_L)
& ~ 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,X3),v_L) ) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f734,definition,
( ~ sP5
| ? [X5,X6] :
( X5 != X6
& ( v_y = X5
| ~ 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_x,X5),v_L)
| v_y != X6 )
& ( v_y = X6
| ~ 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,X6,v_x),v_L)
| v_y != X5 )
& ( v_y = X5
| v_y = X6
| ~ 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,X6,X5),v_L) )
& ( v_y != X5
| v_x != X6 )
& ( v_y = X6
| ~ 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_x,X6),v_L)
| v_y != X5 )
& ( v_y = X5
| ~ 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,X5,v_x),v_L)
| v_y != X6 )
& ( v_y = X6
| v_y = X5
| ~ 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,X5,X6),v_L) )
& ( v_y != X6
| v_x != X5 ) ) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f735,plain,
( sP5
| ? [X0,X1] :
( sP3(X1,X0)
| sP4(X0,X1)
| ( X1 != v_y
& X0 != v_y
& 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_L)
& ? [X2] :
( sP1(X0,X2,X1)
| ( X2 != v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
& ~ 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,X2),v_L) )
| sP2(X0,X1,X2) ) ) ) ),
inference(definition_folding,[],[f540,f734,f733,f732,f731,f730,f729]) ).
fof(f750,plain,
! [X4,X1] :
( ~ sP0(X4,X1)
| ( v_y != X4
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X4),v_L)
& ~ 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_x,X4),v_L) ) ),
inference(nnf_transformation,[],[f729]) ).
fof(f751,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ( v_y != X0
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L)
& ~ 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_x,X0),v_L) ) ),
inference(rectify,[],[f750]) ).
fof(f874,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L) ),
inference(cnf_transformation,[],[f751]) ).
fof(f875,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ~ 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_x,X0),v_L) ),
inference(cnf_transformation,[],[f751]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X0,X1)
| ~ 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_x,X0),v_L) ),
inference(cnf_transformation,[],[f875]) ).
tcf(c_85,plain,
! [X0: $i,X1: $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,X1,X0),v_L)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f874]) ).
tcf(c_704,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X0,X1)
| ~ 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_x,X0),v_L) ),
inference(prop_impl_just,[status(thm)],[c_84]) ).
tcf(c_722,plain,
! [X0: $i,X1: $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,X1,X0),v_L)
| ~ sP0(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_85]) ).
tcf(c_6688,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| 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,sK11,sK12),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L)
| ( v_x = sK12 )
| ( X1 != sK12 )
| ( sK10(sK12) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_722,c_5624]) ).
tcf(c_6689,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| 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,sK11,sK12),v_L)
| 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,sK12,sK10(sK12)),v_L)
| ( v_x = sK12 ) ),
inference(unflattening,[status(thm)],[c_6688]) ).
tcf(c_6708,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L)
| ( v_x = sK12 )
| ( v_y != sK11 )
| ( X1 != sK12 )
| ( sK10(sK12) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_722,c_5604]) ).
tcf(c_6709,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| 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,sK12,sK10(sK12)),v_L)
| ( v_x = sK12 )
| ( v_y != sK11 ) ),
inference(unflattening,[status(thm)],[c_6708]) ).
tcf(c_7235,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| 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,sK11,sK12),v_L)
| ( v_x = sK12 )
| ~ 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_x,X0),v_L)
| ( X1 != sK12 )
| ( sK10(sK12) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_704,c_5624]) ).
tcf(c_7236,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| 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,sK11,sK12),v_L)
| ( v_x = sK12 )
| ~ 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_x,sK10(sK12)),v_L) ),
inference(unflattening,[status(thm)],[c_7235]) ).
tcf(c_7255,plain,
! [X0: $i,X1: $i] :
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| ( v_x = sK12 )
| ~ 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_x,X0),v_L)
| ( v_y != sK11 )
| ( X1 != sK12 )
| ( sK10(sK12) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_704,c_5604]) ).
tcf(c_7256,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| ( v_x = sK12 )
| ~ 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_x,sK10(sK12)),v_L)
| ( v_y != sK11 ) ),
inference(unflattening,[status(thm)],[c_7255]) ).
tcf(c_119085,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| 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,sK11,sK12),v_L)
| 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_x,sK10(sK12)),v_L)
| ( v_x = sK12 )
| ( c_Set_Oinsert(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK37(v_L,c_Relation_OId(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),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,sK11,sK12),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),v_L) = v_L ) ),
inference(superposition,[status(thm)],[c_6689,c_102395]) ).
tcf(c_177148,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| 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,sK11,sK12),v_L)
| ( v_x = sK12 ) ),
inference(global_subsumption_just,[status(thm)],[c_119085,c_5075,c_6689,c_7236,c_36877,c_36875,c_36874,c_143303,c_171376]) ).
tcf(c_177150,plain,
( sP5
| ( v_x = sK12 )
| 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,sK11,sK12),v_L)
| 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,sK12,v_x),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_177148,c_36877,c_36875,c_36874,c_143303,c_177148]) ).
tcf(c_177151,plain,
( sP5
| 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,sK12,v_x),v_L)
| 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,sK11,sK12),v_L)
| ( v_x = sK12 ) ),
inference(renaming,[status(thm)],[c_177150]) ).
tcf(c_177198,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK11,sK12),v_L)
| 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,sK11,v_x),v_L)
| ( v_y = sK11 )
| ( v_x = sK12 ) ),
inference(superposition,[status(thm)],[c_177151,c_53732]) ).
tcf(c_177445,plain,
( sP5
| ( v_y = sK11 )
| 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,sK11,sK12),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_177198,c_36877,c_36875,c_36874,c_41082,c_143303]) ).
tcf(c_177446,plain,
( sP5
| 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,sK11,sK12),v_L)
| ( v_y = sK11 ) ),
inference(renaming,[status(thm)],[c_177445]) ).
tcf(c_187784,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK12,v_x),v_L)
| ( v_x = sK12 ) ),
inference(global_subsumption_just,[status(thm)],[c_187523,c_6709,c_7256,c_36877,c_36875,c_36874,c_143303,c_171376,c_184805,c_187523]) ).
tcf(c_187786,plain,
( sP5
| ( v_x = sK12 )
| 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,sK12,v_x),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_187784,c_36877,c_36875,c_36874,c_143303,c_187784]) ).
tcf(c_187787,plain,
( sP5
| 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,sK12,v_x),v_L)
| ( v_x = sK12 ) ),
inference(renaming,[status(thm)],[c_187786]) ).
tcf(c_187849,plain,
( sP5
| sP4(sK11,sK12)
| 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,sK11,v_x),v_L)
| ( v_y = sK11 )
| ( v_x = sK12 ) ),
inference(superposition,[status(thm)],[c_187787,c_53732]) ).
tcf(c_188005,plain,
( sP5
| ( v_y = sK11 )
| ( v_x = sK12 ) ),
inference(global_subsumption_just,[status(thm)],[c_187849,c_36875,c_187446,c_187849]) ).
tcf(c_188013,plain,
( ( v_y = sK11 )
| ( v_y = sK7 )
| ( v_x = sK12 ) ),
inference(superposition,[status(thm)],[c_188005,c_28249]) ).
tcf(c_188014,plain,
( ( v_y = sK11 )
| ( v_y = sK8 )
| ( v_x = sK12 ) ),
inference(superposition,[status(thm)],[c_188005,c_25494]) ).
tcf(c_189640,plain,
( ( v_y = sK11 )
| ( v_x = sK12 )
| ~ sP5
| ( v_y != sK7 ) ),
inference(superposition,[status(thm)],[c_188014,c_62]) ).
tcf(c_189645,plain,
( ( v_y = sK11 )
| ( v_x = sK12 ) ),
inference(global_subsumption_just,[status(thm)],[c_189640,c_188005,c_188013,c_189640]) ).
tcf(c_189667,plain,
( sP5
| 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,sK11,v_x),v_L)
| ( v_y = sK11 ) ),
inference(superposition,[status(thm)],[c_189645,c_177446]) ).
tcf(c_190989,plain,
( sP5
| ( v_y = sK11 ) ),
inference(global_subsumption_just,[status(thm)],[c_189667,c_187446,c_189667]) ).
tcf(c_190995,plain,
( sP5
| sP4(sK11,sK12)
| 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_x,sK12),v_L) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5061,c_190989]) ).
tcf(c_191026,plain,
( sP5
| 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_x,sK12),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_190995,c_36875,c_184538,c_190995]) ).
tcf(c_191033,plain,
! [X0: $i] :
( sP5
| 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_x,X0),v_L)
| ~ 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,sK12,X0),v_L) ),
inference(superposition,[status(thm)],[c_191026,c_51]) ).
tcf(c_191863,plain,
( sP5
| 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_x,v_x),v_L)
| ( v_x = sK12 ) ),
inference(superposition,[status(thm)],[c_187787,c_191033]) ).
tcf(c_191864,plain,
( sP5
| ( v_x = sK12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_191863,c_52]) ).
tcf(c_192050,plain,
( ( v_x = sK12 )
| ( v_y = sK8 ) ),
inference(global_subsumption_just,[status(thm)],[c_25514,c_25494,c_191864]) ).
tcf(c_192051,plain,
( ( v_y = sK8 )
| ( v_x = sK12 ) ),
inference(renaming,[status(thm)],[c_192050]) ).
tcf(c_192057,plain,
( ( v_x = sK12 )
| ~ sP5
| ( v_y != sK7 ) ),
inference(superposition,[status(thm)],[c_192051,c_62]) ).
tcf(c_192061,plain,
v_x = sK12,
inference(global_subsumption_just,[status(thm)],[c_192057,c_62,c_54,c_59,c_55,c_61,c_56,c_20535,c_20539,c_191864,c_192057]) ).
tcf(c_192079,plain,
( sP5
| 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_x,v_x),v_L) ),
inference(demodulation,[status(thm)],[c_191026,c_192061]) ).
tcf(c_192090,plain,
sP5,
inference(forward_subsumption_resolution,[status(thm)],[c_192079,c_52]) ).
tcf(c_192095,plain,
v_y = sK7,
inference(backward_subsumption_resolution,[status(thm)],[c_28249,c_192090]) ).
tcf(c_192098,plain,
v_y = sK8,
inference(backward_subsumption_resolution,[status(thm)],[c_25494,c_192090]) ).
tcf(c_192099,plain,
sK7 != sK8,
inference(backward_subsumption_resolution,[status(thm)],[c_62,c_192090]) ).
tcf(c_192271,plain,
$false,
inference(ground_joinability,[status(thm)],[c_192099,c_192095,c_192098]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT117+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n008.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 08:48:24 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 76.32/11.44 % SZS status Started for theBenchmark.p
% 76.32/11.44 % SZS status Theorem for theBenchmark.p
% 76.32/11.44
% 76.32/11.44 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 76.32/11.44
% 76.32/11.44 % ------ iProver source info
% 76.32/11.44
% 76.32/11.44 % git: date: 2026-07-19 20:42:38 +0200
% 76.32/11.44 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 76.32/11.44 % git: non_committed_changes: false
% 76.32/11.44
% 76.32/11.44 % ------ Parsing...
% 76.32/11.44 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 76.32/11.44
% 76.32/11.44 % ------ Preprocessing... sup_sim: 55 sf_s rm: 5 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 6 0s sf_e pe_s pe_e %
% 76.32/11.44
% 76.32/11.44 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 76.32/11.44
% 76.32/11.44 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 76.32/11.44 % ------ Proving...
% 76.32/11.44 % ------ Problem Properties
% 76.32/11.44
% 76.32/11.44 %
% 76.32/11.44 % clauses 311
% 76.32/11.44 % conjectures 0
% 76.32/11.44 % EPR 9
% 76.32/11.44 % Horn 202
% 76.32/11.44 % unary 67
% 76.32/11.44 % binary 98
% 76.32/11.44 % lits 864
% 76.32/11.44 % lits eq 226
% 76.32/11.44 % fd_pure 0
% 76.32/11.44 % fd_pseudo 0
% 76.32/11.44 % fd_cond 1
% 76.32/11.44 % fd_pseudo_cond 30
% 76.32/11.44 % AC symbols 0
% 76.32/11.44
% 76.32/11.44 % ------ Schedule dynamic 5 is on
% 76.32/11.44
% 76.32/11.44 % ------ no conjectures: strip conj schedule
% 76.32/11.44
% 76.32/11.44 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 76.32/11.44
% 76.32/11.44
% 76.32/11.44 % ------
% 76.32/11.44 % Current options:
% 76.32/11.44 % ------
% 76.32/11.44
% 76.32/11.44
% 76.32/11.44 %
% 76.32/11.44
% 76.32/11.44 % ------ Proving...
% 76.32/11.44 %
% 76.32/11.44
% 76.32/11.44 % SZS status Theorem for theBenchmark.p
% 76.32/11.44
% 76.32/11.44 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 76.32/11.45
% 76.32/11.45
%------------------------------------------------------------------------------