%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SCT115+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n018.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 188.96s 29.29s
% Output : CNFRefutation 188.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 8
% Syntax : Number of formulae : 188 ( 11 unt; 5 def)
% Number of atoms : 1026 ( 413 equ)
% Maximal formula atoms : 47 ( 5 avg)
% Number of connectives : 1261 ( 466 ~; 514 |; 246 &)
% ( 0 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 4 ( 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 : 16 ( 16 usr; 9 con; 0-4 aty)
% Number of variables : 271 ( 0 sgn 241 !; 30 ?; 125 :)
% Comments :
%------------------------------------------------------------------------------
fof(f173,axiom,
! [X0,X1,X2,X3] :
( ( ~ c_member(X3,X2,X1)
=> c_Groups_Ominus__class_Ominus(tc_fun(X3,tc_HOL_Obool),c_Set_Oinsert(X3,X2,X0),X1) = c_Set_Oinsert(X3,X2,c_Groups_Ominus__class_Ominus(tc_fun(X3,tc_HOL_Obool),X0,X1)) )
& ( c_member(X3,X2,X1)
=> c_Groups_Ominus__class_Ominus(tc_fun(X3,tc_HOL_Obool),c_Set_Oinsert(X3,X2,X0),X1) = c_Groups_Ominus__class_Ominus(tc_fun(X3,tc_HOL_Obool),X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_insert__Diff__if) ).
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/sandbox/benchmark/theBenchmark.p',conj_1) ).
fof(f528,conjecture,
( ! [X0,X1] :
( X0 != X1
=> ( ( X0 != 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,v_y,X0),v_L)
& X1 = v_x )
| ( 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,X1,v_y),v_L)
& X0 = v_x )
| ( X0 != v_x
& 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,X1,X0),v_L) )
| ( X0 = v_y
& X1 = v_x )
| ( 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,v_y,X1),v_L)
& X0 = v_x )
| ( X0 != 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_y),v_L)
& X1 = v_x )
| ( X1 != v_x
& X0 != 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,X1),v_L) )
| ( X1 = v_y
& X0 = v_x ) ) )
& ! [X0,X1] :
( ( ( 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,v_y,X1),v_L)
& X0 = v_x )
=> ! [X2] :
( ( X2 = 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,X1,v_y),v_L) )
& ( ( X2 != 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,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_y,X2),v_L)
| X2 = v_y ) ) ) )
& ( ( X0 != 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_y),v_L)
& X1 = v_x )
=> ! [X2] :
( ( X2 != 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,v_y,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_x
& X0 != 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,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_y),v_L)
& X2 = 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_y),v_L) )
& ( ( X2 != 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,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/sandbox/benchmark/theBenchmark.p',conj_2) ).
fof(f529,negated_conjecture,
~ ( ! [X0,X1] :
( X0 != X1
=> ( ( X0 != 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,v_y,X0),v_L)
& X1 = v_x )
| ( 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,X1,v_y),v_L)
& X0 = v_x )
| ( X0 != v_x
& 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,X1,X0),v_L) )
| ( X0 = v_y
& X1 = v_x )
| ( 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,v_y,X1),v_L)
& X0 = v_x )
| ( X0 != 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_y),v_L)
& X1 = v_x )
| ( X1 != v_x
& X0 != 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,X1),v_L) )
| ( X1 = v_y
& X0 = v_x ) ) )
& ! [X0,X1] :
( ( ( 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,v_y,X1),v_L)
& X0 = v_x )
=> ! [X2] :
( ( X2 = 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,X1,v_y),v_L) )
& ( ( X2 != 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,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_y,X2),v_L)
| X2 = v_y ) ) ) )
& ( ( X0 != 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_y),v_L)
& X1 = v_x )
=> ! [X2] :
( ( X2 != 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,v_y,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_x
& X0 != 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,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_y),v_L)
& X2 = 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_y),v_L) )
& ( ( X2 != 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,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(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_x != 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_y,X5),v_L)
& v_x = X6 )
| ( v_x != 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_y),v_L)
& v_x = X5 )
| ( v_x != X5
& v_x != 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_x != 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_y,X6),v_L)
& v_x = X5 )
| ( v_x != 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_y),v_L)
& v_x = X6 )
| ( v_x != X6
& v_x != 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_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,v_y,X1),v_L)
& X0 = v_x )
=> ! [X4] :
( ( v_x = 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_y),v_L) )
& ( ( v_x != 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_y,X4),v_L)
| v_y = X4 ) ) ) )
& ( ( X0 != 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_y),v_L)
& X1 = v_x )
=> ! [X3] :
( ( v_x != 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_y,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_x
& X0 != 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,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_y),v_L)
& X2 = 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_y),v_L) )
& ( ( X2 != 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,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,[],[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_x = 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_y,X5),v_L)
| v_x != X6 )
& ( v_x = 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_y),v_L)
| v_x != X5 )
& ( v_x = X5
| v_x = 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_x = 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_y,X6),v_L)
| v_x != X5 )
& ( v_x = 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_y),v_L)
| v_x != X6 )
& ( v_x = X6
| v_x = 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_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,v_y,X1),v_L)
& X0 = v_x
& ? [X4] :
( ( v_x = 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_y),v_L) )
| ( v_x != 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_y,X4),v_L)
& v_y != X4 ) ) )
| ( X0 != 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_y),v_L)
& X1 = v_x
& ? [X3] :
( v_x != 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_y,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_x
& X0 != 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,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_y),v_L)
& X2 = 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_y),v_L) )
| ( X2 != 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,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,[],[f531]) ).
fof(f540,plain,
( ? [X5,X6] :
( X5 != X6
& ( v_x = 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_y,X5),v_L)
| v_x != X6 )
& ( v_x = 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_y),v_L)
| v_x != X5 )
& ( v_x = X5
| v_x = 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_x = 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_y,X6),v_L)
| v_x != X5 )
& ( v_x = 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_y),v_L)
| v_x != X6 )
& ( v_x = X6
| v_x = 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_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,v_y,X1),v_L)
& X0 = v_x
& ? [X4] :
( ( v_x = 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_y),v_L) )
| ( v_x != 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_y,X4),v_L)
& v_y != X4 ) ) )
| ( X0 != 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_y),v_L)
& X1 = v_x
& ? [X3] :
( v_x != 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_y,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_x
& X0 != 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,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_y),v_L)
& X2 = 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_y),v_L) )
| ( X2 != 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,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,[],[f539]) ).
fof(f671,plain,
! [X0,X1,X2,X3] :
( ( c_member(X3,X2,X1)
| c_Groups_Ominus__class_Ominus(tc_fun(X3,tc_HOL_Obool),c_Set_Oinsert(X3,X2,X0),X1) = c_Set_Oinsert(X3,X2,c_Groups_Ominus__class_Ominus(tc_fun(X3,tc_HOL_Obool),X0,X1)) )
& ( ~ c_member(X3,X2,X1)
| c_Groups_Ominus__class_Ominus(tc_fun(X3,tc_HOL_Obool),c_Set_Oinsert(X3,X2,X0),X1) = c_Groups_Ominus__class_Ominus(tc_fun(X3,tc_HOL_Obool),X0,X1) ) ),
inference(ennf_transformation,[],[f173]) ).
fof(f737,plain,
( ~ sP4
| ? [X5,X6] :
( X5 != X6
& ( v_x = 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_y,X5),v_L)
| v_x != X6 )
& ( v_x = 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_y),v_L)
| v_x != X5 )
& ( v_x = X5
| v_x = 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_x = 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_y,X6),v_L)
| v_x != X5 )
& ( v_x = 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_y),v_L)
| v_x != X6 )
& ( v_x = X6
| v_x = 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,[],[f733]) ).
fof(f738,plain,
( ~ sP4
| ? [X0,X1] :
( X0 != X1
& ( v_x = 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_y,X0),v_L)
| v_x != X1 )
& ( v_x = 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_y),v_L)
| v_x != X0 )
& ( v_x = X0
| v_x = 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_x = 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_y,X1),v_L)
| v_x != X0 )
& ( v_x = 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_y),v_L)
| v_x != X1 )
& ( v_x = X1
| v_x = 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,[],[f737]) ).
fof(f739,plain,
( ~ sP4
| ( sK6 != sK7
& ( v_x = sK6
| ~ c_member(tc_prod(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_y,sK6),v_L)
| v_x != sK7 )
& ( v_x = 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_y),v_L)
| v_x != sK6 )
& ( v_x = sK6
| v_x = 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,sK6),v_L) )
& ( v_y != sK6
| v_x != sK7 )
& ( v_x = 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_y,sK7),v_L)
| v_x != sK6 )
& ( v_x = sK6
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK6,v_y),v_L)
| v_x != sK7 )
& ( v_x = sK7
| v_x = sK6
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK6,sK7),v_L) )
& ( v_y != sK7
| v_x != sK6 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X0,sK6),skolemize(X1,sK7)],[f738]) ).
fof(f740,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| ( X1 != v_x
& X0 != 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,X1),v_L)
& ? [X2] :
( sP1(X0,X2,X1)
| ( X2 != 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,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(nnf_transformation,[],[f732]) ).
fof(f741,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| ( X1 != v_x
& X0 != 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,X1),v_L)
& ( sP1(X0,sK8(X0,X1),X1)
| ( v_x != sK8(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,sK8(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,X0,sK8(X0,X1)),v_L) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X2,sK8(X0,X1))],[f740]) ).
fof(f742,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| ( X0 != 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_y),v_L)
& X1 = v_x
& ? [X3] :
( v_x != 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_y,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,[],[f731]) ).
fof(f743,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| ( X0 != 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_y),v_L)
& X1 = v_x
& ? [X2] :
( v_x != 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_y,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,[],[f742]) ).
fof(f744,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| ( X0 != 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_y),v_L)
& X1 = v_x
& v_x != 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_y,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))],[f743]) ).
fof(f745,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_y),v_L)
& X2 = 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_y),v_L) ) ),
inference(nnf_transformation,[],[f730]) ).
fof(f746,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_y),v_L)
& v_x = 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_y),v_L) ) ),
inference(rectify,[],[f745]) ).
fof(f750,plain,
( sP4
| ( 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_y,sK12),v_L)
& v_x = sK11
& sP0(sK12) )
| sP2(sK11,sK12)
| sP3(sK11,sK12) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X0,sK11),skolemize(X1,sK12)],[f734]) ).
fof(f838,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(f839,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(f840,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(f841,plain,
( ~ sP4
| sK6 != sK7 ),
inference(cnf_transformation,[],[f739]) ).
fof(f842,plain,
( ~ sP4
| v_x = sK6
| ~ c_member(tc_prod(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_y,sK6),v_L)
| v_x != sK7 ),
inference(cnf_transformation,[],[f739]) ).
fof(f843,plain,
( ~ sP4
| v_x = 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_y),v_L)
| v_x != sK6 ),
inference(cnf_transformation,[],[f739]) ).
fof(f844,plain,
( ~ sP4
| v_x = sK6
| v_x = 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,sK6),v_L) ),
inference(cnf_transformation,[],[f739]) ).
fof(f845,plain,
( ~ sP4
| v_y != sK6
| v_x != sK7 ),
inference(cnf_transformation,[],[f739]) ).
fof(f846,plain,
( ~ sP4
| v_x = 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_y,sK7),v_L)
| v_x != sK6 ),
inference(cnf_transformation,[],[f739]) ).
fof(f847,plain,
( ~ sP4
| v_x = sK6
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK6,v_y),v_L)
| v_x != sK7 ),
inference(cnf_transformation,[],[f739]) ).
fof(f848,plain,
( ~ sP4
| v_x = sK7
| v_x = sK6
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK6,sK7),v_L) ),
inference(cnf_transformation,[],[f739]) ).
fof(f849,plain,
( ~ sP4
| v_y != sK7
| v_x != sK6 ),
inference(cnf_transformation,[],[f739]) ).
fof(f852,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,X1),v_L) ),
inference(cnf_transformation,[],[f741]) ).
fof(f854,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| sP1(X0,sK8(X0,X1),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,sK8(X0,X1)),v_L) ),
inference(cnf_transformation,[],[f741]) ).
fof(f855,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| sP1(X0,sK8(X0,X1),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,sK8(X0,X1)),v_L) ),
inference(cnf_transformation,[],[f741]) ).
fof(f856,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| v_x != X0 ),
inference(cnf_transformation,[],[f744]) ).
fof(f857,plain,
! [X0,X1] :
( ~ sP2(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_y),v_L) ),
inference(cnf_transformation,[],[f744]) ).
fof(f858,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| v_x = X1 ),
inference(cnf_transformation,[],[f744]) ).
fof(f860,plain,
! [X0,X1] :
( ~ sP2(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_y,sK9(X0)),v_L) ),
inference(cnf_transformation,[],[f744]) ).
fof(f861,plain,
! [X0,X1] :
( ~ sP2(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,[],[f744]) ).
fof(f862,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_y),v_L) ),
inference(cnf_transformation,[],[f746]) ).
fof(f864,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_y),v_L) ),
inference(cnf_transformation,[],[f746]) ).
fof(f873,plain,
( sP4
| v_x != sK12
| sP2(sK11,sK12)
| sP3(sK11,sK12) ),
inference(cnf_transformation,[],[f750]) ).
fof(f874,plain,
( sP4
| c_member(tc_prod(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_y,sK12),v_L)
| sP2(sK11,sK12)
| sP3(sK11,sK12) ),
inference(cnf_transformation,[],[f750]) ).
fof(f875,plain,
( sP4
| v_x = sK11
| sP2(sK11,sK12)
| sP3(sK11,sK12) ),
inference(cnf_transformation,[],[f750]) ).
fof(f876,plain,
( sP4
| sP0(sK12)
| sP2(sK11,sK12)
| sP3(sK11,sK12) ),
inference(cnf_transformation,[],[f750]) ).
fof(f1103,plain,
! [X2,X3,X0,X1] :
( ~ c_member(X3,X2,X1)
| c_Groups_Ominus__class_Ominus(tc_fun(X3,tc_HOL_Obool),c_Set_Oinsert(X3,X2,X0),X1) = c_Groups_Ominus__class_Ominus(tc_fun(X3,tc_HOL_Obool),X0,X1) ),
inference(cnf_transformation,[],[f671]) ).
fof(f1230,plain,
! [X1] : ~ sP2(v_x,X1),
inference(equality_resolution,[],[f856]) ).
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,X2,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,X2,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) ),
inference(cnf_transformation,[],[f840]) ).
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,[],[f839]) ).
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,[],[f838]) ).
tcf(c_54,plain,
( ~ sP4
| ( v_y != sK7 )
| ( v_x != sK6 ) ),
inference(cnf_transformation,[],[f849]) ).
tcf(c_55,plain,
( ( v_x = sK7 )
| ( v_x = sK6 )
| ~ sP4
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK6,sK7),v_L) ),
inference(cnf_transformation,[],[f848]) ).
tcf(c_56,plain,
( ( v_x = sK6 )
| ~ sP4
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK6,v_y),v_L)
| ( v_x != sK7 ) ),
inference(cnf_transformation,[],[f847]) ).
tcf(c_57,plain,
( ( v_x = sK7 )
| ~ sP4
| ~ c_member(tc_prod(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_y,sK7),v_L)
| ( v_x != sK6 ) ),
inference(cnf_transformation,[],[f846]) ).
tcf(c_58,plain,
( ~ sP4
| ( v_y != sK6 )
| ( v_x != sK7 ) ),
inference(cnf_transformation,[],[f845]) ).
tcf(c_59,plain,
( ( v_x = sK7 )
| ( v_x = sK6 )
| ~ sP4
| ~ c_member(tc_prod(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,sK6),v_L) ),
inference(cnf_transformation,[],[f844]) ).
tcf(c_60,plain,
( ( v_x = sK7 )
| ~ sP4
| ~ c_member(tc_prod(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_y),v_L)
| ( v_x != sK6 ) ),
inference(cnf_transformation,[],[f843]) ).
tcf(c_61,plain,
( ( v_x = sK6 )
| ~ sP4
| ~ c_member(tc_prod(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_y,sK6),v_L)
| ( v_x != sK7 ) ),
inference(cnf_transformation,[],[f842]) ).
tcf(c_62,plain,
( ~ sP4
| ( sK6 != sK7 ) ),
inference(cnf_transformation,[],[f841]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] :
( sP1(X0,sK8(X0,X1),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,sK8(X0,X1)),v_L) ),
inference(cnf_transformation,[],[f855]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( sP1(X0,sK8(X0,X1),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,sK8(X0,X1)),v_L)
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f854]) ).
tcf(c_66,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,X1),v_L)
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f852]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i] :
( ~ sP2(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,[],[f861]) ).
tcf(c_70,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_y,sK9(X0)),v_L)
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f860]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( ( X1 = v_x )
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f858]) ).
tcf(c_73,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_y),v_L)
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f857]) ).
tcf(c_74,plain,
! [X0: $i] : ~ sP2(v_x,X0),
inference(cnf_transformation,[],[f1230]) ).
tcf(c_75,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_y),v_L) ),
inference(cnf_transformation,[],[f864]) ).
tcf(c_77,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_y),v_L)
| ~ sP1(X0,X1,X2) ),
inference(cnf_transformation,[],[f862]) ).
tcf(c_85,negated_conjecture,
( sP4
| sP0(sK12)
| sP2(sK11,sK12)
| sP3(sK11,sK12) ),
inference(cnf_transformation,[],[f876]) ).
tcf(c_86,negated_conjecture,
( sP4
| sP2(sK11,sK12)
| sP3(sK11,sK12)
| ( v_x = sK11 ) ),
inference(cnf_transformation,[],[f875]) ).
tcf(c_87,negated_conjecture,
( sP4
| sP2(sK11,sK12)
| sP3(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_y,sK12),v_L) ),
inference(cnf_transformation,[],[f874]) ).
tcf(c_88,negated_conjecture,
( sP4
| sP2(sK11,sK12)
| sP3(sK11,sK12)
| ( v_x != sK12 ) ),
inference(cnf_transformation,[],[f873]) ).
tcf(c_297,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( c_Groups_Ominus__class_Ominus(tc_fun(X0,tc_HOL_Obool),c_Set_Oinsert(X0,X1,X3),X2) = c_Groups_Ominus__class_Ominus(tc_fun(X0,tc_HOL_Obool),X3,X2) )
| ~ c_member(X0,X1,X2) ),
inference(cnf_transformation,[],[f1103]) ).
tcf(c_676,plain,
! [X0: $i,X1: $i] :
( ~ sP2(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(prop_impl_just,[status(thm)],[c_69]) ).
tcf(c_680,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_y,sK9(X0)),v_L)
| ~ sP2(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_70]) ).
tcf(c_684,plain,
! [X0: $i,X1: $i] :
( ( X1 = v_x )
| ~ sP2(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_72]) ).
tcf(c_686,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_y),v_L)
| ~ sP2(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_73]) ).
tcf(c_690,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_y),v_L) ),
inference(prop_impl_just,[status(thm)],[c_75]) ).
tcf(c_698,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_y),v_L)
| ~ sP1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_77]) ).
tcf(c_3922,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $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,X4,v_y),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,sK8(X0,X1)),v_L)
| ~ sP3(X0,X1)
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK8(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_698]) ).
tcf(c_3923,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,v_y),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,sK8(X0,X1)),v_L)
| ~ sP3(X0,X1) ),
inference(unflattening,[status(thm)],[c_3922]) ).
tcf(c_3946,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $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,sK8(X0,X1)),v_L)
| ~ 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,X3,v_y),v_L)
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK8(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_690]) ).
tcf(c_3947,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,sK8(X0,X1)),v_L)
| ~ 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_y),v_L) ),
inference(unflattening,[status(thm)],[c_3946]) ).
tcf(c_3958,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $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,X4,v_y),v_L)
| ~ 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,sK8(X0,X1)),v_L)
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK8(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_698]) ).
tcf(c_3959,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,v_y),v_L)
| ~ 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,sK8(X0,X1)),v_L) ),
inference(unflattening,[status(thm)],[c_3958]) ).
tcf(c_3982,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ 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,X3,v_y),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,sK8(X0,X1)),v_L)
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK8(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_690]) ).
tcf(c_3983,plain,
! [X0: $i,X1: $i] :
( ~ 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_y),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,sK8(X0,X1)),v_L) ),
inference(unflattening,[status(thm)],[c_3982]) ).
tcf(c_4469,plain,
! [X0: $i,X1: $i] :
( sP4
| sP3(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,v_y),v_L)
| ( v_x = sK11 )
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_686,c_86]) ).
tcf(c_4470,plain,
( sP4
| sP3(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_y),v_L)
| ( v_x = sK11 ) ),
inference(unflattening,[status(thm)],[c_4469]) ).
tcf(c_4616,plain,
! [X0: $i,X1: $i] :
( sP4
| sP3(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_y,sK12),v_L)
| ( X1 = v_x )
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_684,c_87]) ).
tcf(c_4617,plain,
( sP4
| sP3(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_y,sK12),v_L)
| ( sK12 = v_x ) ),
inference(unflattening,[status(thm)],[c_4616]) ).
tcf(c_4952,plain,
! [X0: $i,X1: $i] :
( sP4
| sP3(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_y,sK9(X0)),v_L)
| ( v_x = sK11 )
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_680,c_86]) ).
tcf(c_4953,plain,
( sP4
| sP3(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_y,sK9(sK11)),v_L)
| ( v_x = sK11 ) ),
inference(unflattening,[status(thm)],[c_4952]) ).
tcf(c_5113,plain,
! [X0: $i,X1: $i] :
( sP4
| sP3(sK11,sK12)
| ( 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,X0,sK9(X0)),v_L)
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_676,c_86]) ).
tcf(c_5114,plain,
( sP4
| sP3(sK11,sK12)
| ( 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,sK9(sK11)),v_L) ),
inference(unflattening,[status(thm)],[c_5113]) ).
tcf(c_5246,plain,
! [X0: $i] :
( sP4
| sP3(sK11,sK12)
| ( v_x != sK12 )
| ( v_x != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_74,c_88]) ).
tcf(c_5247,plain,
( sP4
| sP3(sK11,sK12)
| ( v_x != sK12 )
| ( v_x != sK11 ) ),
inference(unflattening,[status(thm)],[c_5246]) ).
tcf(c_5260,plain,
! [X0: $i] :
( sP4
| sP3(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_y,sK12),v_L)
| ( v_x != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_74,c_87]) ).
tcf(c_5261,plain,
( sP4
| sP3(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_y,sK12),v_L)
| ( v_x != sK11 ) ),
inference(unflattening,[status(thm)],[c_5260]) ).
tcf(c_18236,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,sK6),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,sK6,sK7),v_L)
| ( sK6 = sK7 ) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_22051,plain,
( ( v_x = sK7 )
| ( v_x = sK6 )
| ~ sP4 ),
inference(global_subsumption_just,[status(thm)],[c_55,c_62,c_59,c_55,c_18236]) ).
tcf(c_24115,plain,
( ( v_x = sK6 )
| ~ sP4
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK6,v_y),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_56,c_56,c_22051]) ).
tcf(c_24283,plain,
( ( v_x = sK7 )
| ~ sP4
| ~ c_member(tc_prod(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_y,sK7),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_57,c_57,c_22051]) ).
tcf(c_24295,plain,
( ( v_x = sK7 )
| ~ sP4
| ~ c_member(tc_prod(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_y),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_60,c_60,c_22051]) ).
tcf(c_24307,plain,
( ( v_x = sK6 )
| ~ sP4
| ~ c_member(tc_prod(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_y,sK6),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_61,c_62,c_59,c_55,c_61,c_18236]) ).
tcf(c_30232,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,sK6,v_y),v_L)
| ( v_y = sK6 )
| ( v_x = sK6 )
| ~ sP4 ),
inference(superposition,[status(thm)],[c_53,c_24307]) ).
tcf(c_33008,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_y),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_y,sK7),v_L)
| ( v_y = sK7 ) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_36741,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,v_y),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_y),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) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_47780,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_y),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,v_y),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(instantiation,[status(thm)],[c_51]) ).
tcf(c_47782,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_y,v_y),v_L),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_56974,plain,
( ( v_x = sK7 )
| ~ sP4 ),
inference(global_subsumption_just,[status(thm)],[c_55,c_54,c_22051,c_24283,c_24295,c_33008]) ).
tcf(c_56980,plain,
( ~ sP4
| ( v_y != sK6 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_58,c_56974]) ).
tcf(c_59495,plain,
! [X0: $i] :
( sP4
| sP3(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,sK9(sK11)),v_L)
| ( 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,X0,v_y),v_L) ),
inference(superposition,[status(thm)],[c_4953,c_51]) ).
tcf(c_62935,plain,
( sP4
| sP3(sK11,sK12)
| ( 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_y),v_L) ),
inference(superposition,[status(thm)],[c_59495,c_5114]) ).
tcf(c_63127,plain,
( sP4
| sP3(sK11,sK12)
| ( v_x = sK11 ) ),
inference(global_subsumption_just,[status(thm)],[c_62935,c_4470,c_62935]) ).
tcf(c_63142,plain,
( sP4
| sP3(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_y,sK12),v_L) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5261,c_63127]) ).
tcf(c_63143,plain,
( sP4
| sP3(sK11,sK12)
| ( v_x != sK12 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5247,c_63127]) ).
tcf(c_65428,plain,
( ( v_x = sK6 )
| ~ sP4 ),
inference(global_subsumption_just,[status(thm)],[c_56,c_24115,c_30232,c_56980]) ).
tcf(c_67651,plain,
! [X0: $i,X1: $i] :
( ~ 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,X1,sK8(X0,X1)),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_64,c_66,c_3923,c_3947,c_47780]) ).
tcf(c_67652,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,sK8(X0,X1)),v_L)
| ~ sP3(X0,X1) ),
inference(renaming,[status(thm)],[c_67651]) ).
tcf(c_72114,plain,
! [X0: $i] :
( sP4
| sP3(sK11,sK12)
| ( v_x = sK11 )
| ( c_Groups_Ominus__class_Ominus(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),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,sK11,v_y),X0),v_L) = c_Groups_Ominus__class_Ominus(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),X0,v_L) ) ),
inference(superposition,[status(thm)],[c_4470,c_297]) ).
tcf(c_77325,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_y,v_y),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_y),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_y,sK12),v_L) ),
inference(instantiation,[status(thm)],[c_36741]) ).
tcf(c_77521,plain,
( sP4
| sP3(sK11,sK12)
| ( v_x = sK11 ) ),
inference(global_subsumption_just,[status(thm)],[c_72114,c_63127]) ).
tcf(c_77638,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,sK8(X0,X1)),v_L)
| ~ sP3(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_63,c_66,c_3959,c_3983,c_47780]) ).
tcf(c_77639,plain,
! [X0: $i,X1: $i] :
( ~ 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,sK8(X0,X1)),v_L) ),
inference(renaming,[status(thm)],[c_77638]) ).
tcf(c_108985,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_y,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_y,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_114697,plain,
( sP4
| sP3(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_y,sK12),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_4617,c_63142]) ).
tcf(c_117878,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_y,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_y,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_108985]) ).
tcf(c_164118,plain,
! [X0: $i] :
( sP4
| sP3(sK11,sK12)
| ( c_Groups_Ominus__class_Ominus(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),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_y,sK12),X0),v_L) = c_Groups_Ominus__class_Ominus(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),X0,v_L) ) ),
inference(superposition,[status(thm)],[c_114697,c_297]) ).
tcf(c_249698,plain,
( ( v_x = sK7 )
| ~ sP4 ),
inference(global_subsumption_just,[status(thm)],[c_55,c_54,c_22051,c_24283,c_24295,c_33008]) ).
tcf(c_249704,plain,
( ( v_x = sK6 )
| ~ sP4 ),
inference(global_subsumption_just,[status(thm)],[c_56,c_65428]) ).
tcf(c_249729,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,sK8(X0,X1)),v_L)
| ~ sP3(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_63,c_77639]) ).
tcf(c_249730,plain,
! [X0: $i,X1: $i] :
( ~ 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,sK8(X0,X1)),v_L) ),
inference(renaming,[status(thm)],[c_249729]) ).
tcf(c_249740,plain,
! [X0: $i,X1: $i] :
( ~ 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,X1,sK8(X0,X1)),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_64,c_67652]) ).
tcf(c_249741,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,sK8(X0,X1)),v_L)
| ~ sP3(X0,X1) ),
inference(renaming,[status(thm)],[c_249740]) ).
tcf(c_249746,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,sK8(X2,X1)),v_L)
| ~ sP3(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,X0,X1),v_L) ),
inference(superposition,[status(thm)],[c_249741,c_51]) ).
tcf(c_266691,plain,
! [X0: $i,X1: $i] :
( ~ 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,X1),v_L) ),
inference(superposition,[status(thm)],[c_249746,c_249730]) ).
tcf(c_266923,plain,
! [X0: $i,X1: $i] : ~ sP3(X0,X1),
inference(global_subsumption_just,[status(thm)],[c_266691,c_66,c_266691]) ).
fof(f729,definition,
! [X1] :
( ~ sP0(X1)
| ? [X4] :
( ( v_x = 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_y),v_L) )
| ( v_x != 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_y,X4),v_L)
& v_y != X4 ) ) ),
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_y),v_L)
& X2 = 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_y),v_L) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f731,definition,
! [X0,X1] :
( ~ sP2(X0,X1)
| ( X0 != 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_y),v_L)
& X1 = v_x
& ? [X3] :
( v_x != 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_y,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,[sP2])],[predicate_definition_introduction]) ).
fof(f732,definition,
! [X0,X1] :
( ~ sP3(X0,X1)
| ( X1 != v_x
& X0 != 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,X1),v_L)
& ? [X2] :
( sP1(X0,X2,X1)
| ( X2 != 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,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) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f733,definition,
( ~ sP4
| ? [X5,X6] :
( X5 != X6
& ( v_x = 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_y,X5),v_L)
| v_x != X6 )
& ( v_x = 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_y),v_L)
| v_x != X5 )
& ( v_x = X5
| v_x = 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_x = 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_y,X6),v_L)
| v_x != X5 )
& ( v_x = 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_y),v_L)
| v_x != X6 )
& ( v_x = X6
| v_x = 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,[sP4])],[predicate_definition_introduction]) ).
fof(f734,plain,
( sP4
| ? [X0,X1] :
( ( 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,v_y,X1),v_L)
& X0 = v_x
& sP0(X1) )
| sP2(X0,X1)
| sP3(X0,X1) ) ),
inference(definition_folding,[],[f540,f733,f732,f731,f730,f729]) ).
fof(f747,plain,
! [X1] :
( ~ sP0(X1)
| ? [X4] :
( ( v_x = 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_y),v_L) )
| ( v_x != 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_y,X4),v_L)
& v_y != X4 ) ) ),
inference(nnf_transformation,[],[f729]) ).
fof(f748,plain,
! [X0] :
( ~ sP0(X0)
| ? [X1] :
( ( v_x = 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_y),v_L) )
| ( v_x != 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,v_y,X1),v_L)
& v_y != X1 ) ) ),
inference(rectify,[],[f747]) ).
fof(f749,plain,
! [X0] :
( ~ sP0(X0)
| ( v_x = 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_y),v_L) )
| ( v_x != 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,sK10(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_y,sK10(X0)),v_L)
& v_y != sK10(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X1,sK10(X0))],[f748]) ).
fof(f866,plain,
! [X0] :
( ~ sP0(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_y),v_L)
| v_x != sK10(X0) ),
inference(cnf_transformation,[],[f749]) ).
fof(f867,plain,
! [X0] :
( ~ sP0(X0)
| v_x = 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,sK10(X0)),v_L) ),
inference(cnf_transformation,[],[f749]) ).
fof(f869,plain,
! [X0] :
( ~ sP0(X0)
| v_x = 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,v_y,sK10(X0)),v_L) ),
inference(cnf_transformation,[],[f749]) ).
tcf(c_81,plain,
! [X0: $i] :
( ( sK10(X0) = v_x )
| ~ sP0(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_y,sK10(X0)),v_L) ),
inference(cnf_transformation,[],[f869]) ).
tcf(c_83,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,sK10(X0)),v_L)
| ( sK10(X0) = v_x )
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f867]) ).
tcf(c_84,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,v_y),v_L)
| ~ sP0(X0)
| ( sK10(X0) != v_x ) ),
inference(cnf_transformation,[],[f866]) ).
tcf(c_4018,plain,
! [X0: $i] :
( sP4
| sP2(sK11,sK12)
| sP3(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,v_y),v_L)
| ( X0 != sK12 )
| ( sK10(X0) != v_x ) ),
inference(resolution_lifted,[status(thm)],[c_84,c_85]) ).
tcf(c_4019,plain,
( sP4
| sP2(sK11,sK12)
| sP3(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_y),v_L)
| ( sK10(sK12) != v_x ) ),
inference(unflattening,[status(thm)],[c_4018]) ).
tcf(c_4035,plain,
! [X0: $i] :
( sP4
| sP2(sK11,sK12)
| sP3(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,sK10(X0)),v_L)
| ( sK10(X0) = v_x )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_83,c_85]) ).
tcf(c_4036,plain,
( sP4
| sP2(sK11,sK12)
| sP3(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,sK10(sK12)),v_L)
| ( sK10(sK12) = v_x ) ),
inference(unflattening,[status(thm)],[c_4035]) ).
tcf(c_4069,plain,
! [X0: $i] :
( sP4
| sP2(sK11,sK12)
| sP3(sK11,sK12)
| ( sK10(X0) = 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,v_y,sK10(X0)),v_L)
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_81,c_85]) ).
tcf(c_4070,plain,
( sP4
| sP2(sK11,sK12)
| sP3(sK11,sK12)
| ( sK10(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,v_y,sK10(sK12)),v_L) ),
inference(unflattening,[status(thm)],[c_4069]) ).
tcf(c_4534,plain,
! [X0: $i,X1: $i] :
( sP4
| sP3(sK11,sK12)
| ( X1 = v_x )
| ( sK10(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,v_y,sK10(sK12)),v_L)
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_684,c_4070]) ).
tcf(c_4535,plain,
( sP4
| sP3(sK11,sK12)
| ( sK12 = v_x )
| ( sK10(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,v_y,sK10(sK12)),v_L) ),
inference(unflattening,[status(thm)],[c_4534]) ).
tcf(c_4568,plain,
! [X0: $i,X1: $i] :
( sP4
| sP3(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,sK10(sK12)),v_L)
| ( X1 = v_x )
| ( sK10(sK12) = v_x )
| ( X1 != sK12 )
| ( X0 != sK11 ) ),
inference(resolution_lifted,[status(thm)],[c_684,c_4036]) ).
tcf(c_4569,plain,
( sP4
| sP3(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,sK10(sK12)),v_L)
| ( sK12 = v_x )
| ( sK10(sK12) = v_x ) ),
inference(unflattening,[status(thm)],[c_4568]) ).
tcf(c_5178,plain,
! [X0: $i] :
( sP4
| sP3(sK11,sK12)
| ( sK10(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,v_y,sK10(sK12)),v_L)
| ( v_x != sK11 )
| ( X0 != sK12 ) ),
inference(resolution_lifted,[status(thm)],[c_74,c_4070]) ).
tcf(c_5179,plain,
( sP4
| sP3(sK11,sK12)
| ( sK10(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,v_y,sK10(sK12)),v_L)
| ( v_x != sK11 ) ),
inference(unflattening,[status(thm)],[c_5178]) ).
tcf(c_5229,plain,
! [X0: $i] :
( sP4
| sP3(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_y),v_L)
| ( v_x != sK11 )
| ( X0 != sK12 )
| ( sK10(sK12) != v_x ) ),
inference(resolution_lifted,[status(thm)],[c_74,c_4019]) ).
tcf(c_5230,plain,
( sP4
| sP3(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_y),v_L)
| ( v_x != sK11 )
| ( sK10(sK12) != v_x ) ),
inference(unflattening,[status(thm)],[c_5229]) ).
tcf(c_63136,plain,
( sP4
| sP3(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_y),v_L)
| ( sK10(sK12) != v_x ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5230,c_63127]) ).
tcf(c_63139,plain,
( sP4
| sP3(sK11,sK12)
| ( sK10(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,v_y,sK10(sK12)),v_L) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5179,c_63127]) ).
tcf(c_77530,plain,
( sP4
| sP3(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_y),v_L)
| ( sK10(sK12) != v_x ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5230,c_77521]) ).
tcf(c_78167,plain,
( sP4
| sP3(sK11,sK12)
| ( sK10(sK12) != v_x ) ),
inference(global_subsumption_just,[status(thm)],[c_77530,c_47782,c_63142,c_63136,c_77325]) ).
tcf(c_78177,plain,
( sP4
| sP3(sK11,sK12)
| ( 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_y,sK10(sK12)),v_L) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4535,c_78167]) ).
tcf(c_78178,plain,
( sP4
| sP3(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,sK10(sK12)),v_L)
| ( v_x = sK12 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4569,c_78167]) ).
tcf(c_78275,plain,
( sP4
| sP3(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,sK10(sK12)),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_78178,c_63143,c_78178]) ).
tcf(c_78298,plain,
( sP4
| sP3(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_y,sK10(sK12)),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_78177,c_63139,c_78167]) ).
tcf(c_106525,plain,
( sP4
| sP3(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_y,sK10(sK12)),v_L) ),
inference(global_subsumption_just,[status(thm)],[c_4535,c_78298]) ).
tcf(c_118474,plain,
( sP4
| sP3(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,sK10(sK12),v_y),v_L)
| ( sK10(sK12) = v_y ) ),
inference(superposition,[status(thm)],[c_53,c_106525]) ).
tcf(c_118552,plain,
( sP4
| sP3(sK11,sK12) ),
inference(global_subsumption_just,[status(thm)],[c_118474,c_63142,c_78275,c_78298,c_117878]) ).
tcf(c_167666,plain,
( sP4
| sP3(sK11,sK12) ),
inference(global_subsumption_just,[status(thm)],[c_164118,c_118552]) ).
tcf(c_266925,plain,
sP4,
inference(backward_subsumption_resolution,[status(thm)],[c_167666,c_266923]) ).
tcf(c_266927,plain,
v_x = sK6,
inference(backward_subsumption_resolution,[status(thm)],[c_249704,c_266925]) ).
tcf(c_266929,plain,
v_x = sK7,
inference(backward_subsumption_resolution,[status(thm)],[c_249698,c_266925]) ).
tcf(c_266930,plain,
sK6 != sK7,
inference(backward_subsumption_resolution,[status(thm)],[c_62,c_266925]) ).
tcf(c_267341,plain,
$false,
inference(ground_joinability,[status(thm)],[c_266930,c_266927,c_266929]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT115+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.18/0.45 % Computer : n018.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Thu Sep 24 08:49:18 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.24/0.52 Running first-order theorem proving
% 0.24/0.52 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.24/0.53
% 0.24/0.53 % ======== iProver multi-core TPTP/SMT =========
% 0.24/0.53
% 0.24/0.54 % Detected problem language: tptp
% 0.24/0.55 % Proving...
% 188.96/29.29 % SZS status Started for theBenchmark.p
% 188.96/29.29 % SZS status Theorem for theBenchmark.p
% 188.96/29.29
% 188.96/29.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 188.96/29.29
% 188.96/29.29 % ------ iProver source info
% 188.96/29.29
% 188.96/29.29 % git: date: 2026-07-19 20:42:38 +0200
% 188.96/29.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 188.96/29.29 % git: non_committed_changes: false
% 188.96/29.29
% 188.96/29.29 % ------ Parsing...
% 188.96/29.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 188.96/29.29
% 188.96/29.29 % ------ Preprocessing... sup_sim: 9 sf_s rm: 5 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 4 0s sf_e pe_s pe_e %
% 188.96/29.29
% 188.96/29.29 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 188.96/29.29
% 188.96/29.29 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 188.96/29.29 % ------ Proving...
% 188.96/29.29 % ------ Problem Properties
% 188.96/29.29
% 188.96/29.29 %
% 188.96/29.29 % clauses 318
% 188.96/29.29 % conjectures 0
% 188.96/29.29 % EPR 10
% 188.96/29.29 % Horn 208
% 188.96/29.29 % unary 70
% 188.96/29.29 % binary 98
% 188.96/29.29 % lits 834
% 188.96/29.29 % lits eq 209
% 188.96/29.29 % fd_pure 0
% 188.96/29.29 % fd_pseudo 0
% 188.96/29.29 % fd_cond 1
% 188.96/29.29 % fd_pseudo_cond 30
% 188.96/29.29 % AC symbols 0
% 188.96/29.29
% 188.96/29.29 % ------ Schedule dynamic 5 is on
% 188.96/29.29
% 188.96/29.29 % ------ no conjectures: strip conj schedule
% 188.96/29.29
% 188.96/29.29 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 188.96/29.29
% 188.96/29.29
% 188.96/29.29 % ------
% 188.96/29.29 % Current options:
% 188.96/29.29 % ------
% 188.96/29.29
% 188.96/29.29
% 188.96/29.29 %
% 188.96/29.29
% 188.96/29.29 % ------ Proving...
% 188.96/29.29 % Proof_search_loop: time out after: 3598 full_loop iterations
% 188.96/29.29
% 188.96/29.29 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" stripped conjectures Time Limit: 15.
% 188.96/29.29
% 188.96/29.29
% 188.96/29.29 % ------
% 188.96/29.29 % Current options:
% 188.96/29.29 % ------
% 188.96/29.29
% 188.96/29.29
% 188.96/29.29 %
% 188.96/29.29
% 188.96/29.29 % ------ Proving...
% 188.96/29.29 % Proof_search_loop: time out after: 5811 full_loop iterations
% 188.96/29.29
% 188.96/29.29 % ------ Option_1: Negative Selections stripped conjectures Time Limit: 35.
% 188.96/29.29
% 188.96/29.29
% 188.96/29.29 % ------
% 188.96/29.29 % Current options:
% 188.96/29.29 % ------
% 188.96/29.29
% 188.96/29.29
% 188.96/29.29 %
% 188.96/29.29
% 188.96/29.29 % ------ Proving...
% 188.96/29.29 %
% 188.96/29.29
% 188.96/29.29 % SZS status Theorem for theBenchmark.p
% 188.96/29.29
% 188.96/29.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 188.96/29.29
% 188.96/29.29
%------------------------------------------------------------------------------