%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SCT117+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:37:33 PM UTC 2026
% Result : Theorem 2.25s 1.01s
% Output : Refutation 2.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 36
% Syntax : Number of formulae : 322 ( 17 unt; 32 def)
% Number of atoms : 1235 ( 276 equ)
% Maximal formula atoms : 53 ( 3 avg)
% Number of connectives : 1454 ( 541 ~; 675 |; 166 &)
% ( 33 <=>; 39 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 41 ( 39 usr; 33 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-4 aty)
% Number of variables : 184 ( 0 sgn 170 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [X0,X1,X2] :
( c_member(X2,X1,X0)
<=> hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_mem__def) ).
fof(f526,axiom,
v_x != v_y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f527,axiom,
( ! [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) ) )
& ! [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] :
( 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,X0),v_L) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
fof(f528,conjecture,
( ! [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)
& X0 != v_y
& X1 != v_y )
=> ! [X2] :
( ( ( X1 = v_x
& 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_x),v_L) ) )
& ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
& X2 != v_y )
=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X2),v_L) )
& ( ( X2 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) )
=> ( 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_x),v_L) ) ) ) )
& ( ( X1 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L)
& X0 != v_y )
=> ! [X2] :
( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X2),v_L)
& X2 != v_y )
=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X2),v_L) ) )
& ( ( X0 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L)
& X1 != v_y )
=> ! [X2] :
( ( X1 = v_x
=> X2 != v_y )
& ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
& X2 != v_y )
=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X2),v_L) )
& ( X2 = v_y
=> ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) ) ) ) )
& ! [X0,X1] :
( X0 != X1
=> ( ( X0 = v_x
& X1 = v_y )
| ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),v_L)
& X0 != v_y
& X1 != v_y )
| ( X1 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L)
& X0 != v_y )
| ( X0 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L)
& X1 != v_y )
| ( X1 = v_x
& X0 = v_y )
| ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L)
& X1 != v_y
& X0 != v_y )
| ( X0 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L)
& X1 != v_y )
| ( X1 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X0),v_L)
& X0 != v_y ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_2) ).
fof(f529,negated_conjecture,
~ ( ! [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)
& X0 != v_y
& X1 != v_y )
=> ! [X2] :
( ( ( X1 = v_x
& 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_x),v_L) ) )
& ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
& X2 != v_y )
=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X2),v_L) )
& ( ( X2 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) )
=> ( 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_x),v_L) ) ) ) )
& ( ( X1 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L)
& X0 != v_y )
=> ! [X2] :
( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X2),v_L)
& X2 != v_y )
=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X2),v_L) ) )
& ( ( X0 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L)
& X1 != v_y )
=> ! [X2] :
( ( X1 = v_x
=> X2 != v_y )
& ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
& X2 != v_y )
=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X2),v_L) )
& ( X2 = v_y
=> ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) ) ) ) )
& ! [X0,X1] :
( X0 != X1
=> ( ( X0 = v_x
& X1 = v_y )
| ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),v_L)
& X0 != v_y
& X1 != v_y )
| ( X1 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L)
& X0 != v_y )
| ( X0 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L)
& X1 != v_y )
| ( X1 = v_x
& X0 = v_y )
| ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L)
& X1 != v_y
& X0 != v_y )
| ( X0 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L)
& X1 != v_y )
| ( X1 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X0),v_L)
& X0 != v_y ) ) ) ),
inference(negated_conjecture,[status(cth)],[f528]) ).
fof(f533,plain,
( ! [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) ) )
& ! [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)
& ! [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,X4,X5),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,X5,X4),v_L) ) ) ),
inference(rectify,[],[f527]) ).
fof(f534,plain,
~ ( ! [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)
& X0 != v_y
& X1 != v_y )
=> ! [X2] :
( ( ( X1 = v_x
& 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_x),v_L) ) )
& ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
& X2 != v_y )
=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X2),v_L) )
& ( ( X2 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) )
=> ( 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_x),v_L) ) ) ) )
& ( ( X1 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L)
& X0 != v_y )
=> ! [X3] :
( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X3),v_L)
& v_y != X3 )
=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X3),v_L) ) )
& ( ( X0 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L)
& X1 != v_y )
=> ! [X4] :
( ( X1 = v_x
=> v_y != X4 )
& ( ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X4),v_L)
& v_y != X4 )
=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X4),v_L) )
& ( v_y = X4
=> ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) ) ) ) )
& ! [X5,X6] :
( X5 != X6
=> ( ( v_x = X5
& v_y = X6 )
| ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X6),v_L)
& v_y != X5
& v_y != X6 )
| ( v_y = X6
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,v_x),v_L)
& v_y != X5 )
| ( v_y = X5
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X6),v_L)
& v_y != X6 )
| ( v_x = X6
& v_y = X5 )
| ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X6,X5),v_L)
& v_y != X6
& v_y != X5 )
| ( v_y = X5
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X6,v_x),v_L)
& v_y != X6 )
| ( v_y = X6
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X5),v_L)
& v_y != X5 ) ) ) ),
inference(rectify,[],[f529]) ).
fof(f1021,plain,
( ! [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,X2),v_L)
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L) )
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),v_L) )
& ! [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)
& ! [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,X4,X5),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,X5,X4),v_L)
| X4 = X5 ) ),
inference(ennf_transformation,[],[f533]) ).
fof(f1022,plain,
( ! [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,X2),v_L)
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L) )
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),v_L) )
& ! [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)
& ! [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,X4,X5),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,X5,X4),v_L)
| X4 = X5 ) ),
inference(flattening,[],[f1021]) ).
fof(f1023,plain,
( ? [X0,X1] :
( ( ? [X2] :
( ( 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_x),v_L)
& X1 = v_x
& X2 = v_y )
| ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X2),v_L)
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
& X2 != v_y )
| ( 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_x),v_L)
& X2 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) ) )
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),v_L)
& X0 != v_y
& X1 != v_y )
| ( ? [X3] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,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,v_x,X3),v_L)
& v_y != X3 )
& X1 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L)
& X0 != v_y )
| ( ? [X4] :
( ( v_y = X4
& 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_x,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,X1,X4),v_L)
& v_y != X4 )
| ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L)
& v_y = X4 ) )
& X0 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L)
& X1 != v_y ) )
| ? [X5,X6] :
( ( v_x != X5
| v_y != X6 )
& ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X6),v_L)
| v_y = X5
| v_y = X6 )
& ( v_y != X6
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,v_x),v_L)
| v_y = X5 )
& ( v_y != X5
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X6),v_L)
| v_y = X6 )
& ( v_x != X6
| v_y != X5 )
& ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X6,X5),v_L)
| v_y = X6
| v_y = X5 )
& ( v_y != X5
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X6,v_x),v_L)
| v_y = X6 )
& ( v_y != X6
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X5),v_L)
| v_y = X5 )
& X5 != X6 ) ),
inference(ennf_transformation,[],[f534]) ).
fof(f1024,plain,
( ? [X0,X1] :
( ( ? [X2] :
( ( 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_x),v_L)
& X1 = v_x
& X2 = v_y )
| ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X2),v_L)
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X2),v_L)
& X2 != v_y )
| ( 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_x),v_L)
& X2 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L) ) )
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),v_L)
& X0 != v_y
& X1 != v_y )
| ( ? [X3] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,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,v_x,X3),v_L)
& v_y != X3 )
& X1 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L)
& X0 != v_y )
| ( ? [X4] :
( ( v_y = X4
& 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_x,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,X1,X4),v_L)
& v_y != X4 )
| ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L)
& v_y = X4 ) )
& X0 = v_y
& c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L)
& X1 != v_y ) )
| ? [X5,X6] :
( ( v_x != X5
| v_y != X6 )
& ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,X6),v_L)
| v_y = X5
| v_y = X6 )
& ( v_y != X6
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X5,v_x),v_L)
| v_y = X5 )
& ( v_y != X5
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X6),v_L)
| v_y = X6 )
& ( v_x != X6
| v_y != X5 )
& ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X6,X5),v_L)
| v_y = X6
| v_y = X5 )
& ( v_y != X5
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X6,v_x),v_L)
| v_y = X6 )
& ( v_y != X6
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X5),v_L)
| v_y = X5 )
& X5 != X6 ) ),
inference(flattening,[],[f1023]) ).
fof(f1050,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(X0,X1))
| c_member(X2,X1,X0) ),
inference(cnf_transformation,[],[f11]) ).
fof(f1051,plain,
! [X2,X0,X1] :
( ~ c_member(X2,X1,X0)
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[],[f11]) ).
fof(f1820,plain,
v_x != v_y,
inference(cnf_transformation,[],[f526]) ).
fof(f1821,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,X1,X2),v_L)
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),v_L)
| c_member(tc_prod(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,[],[f1022]) ).
fof(f1822,plain,
! [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)
| X4 = X5 ),
inference(cnf_transformation,[],[f1022]) ).
fof(f1823,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,[],[f1022]) ).
fof(f1824,plain,
! [X2,X0,X1] :
( ~ sP102(X2,X1,X0)
| v_y = X2 ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1825,plain,
! [X2,X0,X1] :
( ~ sP102(X2,X1,X0)
| v_x = X1 ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1826,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,v_x),v_L)
| ~ sP102(X2,X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1832,plain,
! [X0,X1] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L)
| c_member(tc_prod(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,sK99(X0,X1)),v_L)
| sP102(sK99(X0,X1),X1,X0)
| ~ sP96(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1833,plain,
! [X0,X1] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L)
| ~ c_member(tc_prod(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,sK99(X0,X1)),v_L)
| sP102(sK99(X0,X1),X1,X0)
| ~ sP96(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1834,plain,
! [X0,X1] :
( v_y = sK99(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,sK99(X0,X1)),v_L)
| sP102(sK99(X0,X1),X1,X0)
| ~ sP96(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1835,plain,
! [X0,X1] :
( v_y = sK99(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,sK99(X0,X1)),v_L)
| sP102(sK99(X0,X1),X1,X0)
| ~ sP96(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1836,plain,
! [X0,X1] :
( v_y != sK99(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,v_x),v_L)
| sP102(sK99(X0,X1),X1,X0)
| ~ sP96(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1839,plain,
! [X1,X4] :
( ~ sP101(X4,X1)
| v_x = X1 ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1840,plain,
! [X1,X4] :
( ~ sP101(X4,X1)
| v_y = X4 ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1842,plain,
! [X1,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)
| ~ sP100(X4,X1) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1843,plain,
! [X1,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,v_x,X4),v_L)
| ~ sP100(X4,X1) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1845,plain,
! [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,v_x),v_L)
| sP100(sK97(X1),X1)
| sP101(sK97(X1),X1)
| v_y != X0
| sP96(X1,X0)
| ~ sP95(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1846,plain,
! [X0,X1] :
( v_y = sK97(X1)
| sP100(sK97(X1),X1)
| sP101(sK97(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,v_x),v_L)
| sP96(X1,X0)
| ~ sP95(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1848,plain,
! [X0,X1] :
( v_y = sK97(X1)
| sP100(sK97(X1),X1)
| sP101(sK97(X1),X1)
| v_y = X1
| sP96(X1,X0)
| ~ sP95(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1850,plain,
! [X0,X1] :
( v_y = sK97(X1)
| sP100(sK97(X1),X1)
| sP101(sK97(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,sK98(X0)),v_L)
| sP96(X1,X0)
| ~ sP95(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1857,plain,
! [X0,X1] :
( v_y != X1
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK98(X0)),v_L)
| sP96(X1,X0)
| ~ sP95(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1861,plain,
! [X0,X1] :
( ~ sP95(X1,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,sK98(X0)),v_L)
| sP96(X1,X0)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1864,plain,
! [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,sK98(X0)),v_L)
| v_y = X0
| sP96(X1,X0)
| ~ sP95(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1865,plain,
! [X0,X1] :
( v_y != X1
| ~ sP96(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1866,plain,
! [X0,X1] :
( v_y != X0
| ~ sP96(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1867,plain,
! [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)
| ~ sP96(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1868,plain,
! [X0,X1] :
( ~ sP95(X1,X0)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L)
| sP96(X1,X0)
| v_y = X0 ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1869,plain,
! [X0,X1] :
( ~ sP95(X1,X0)
| v_y = X1
| sP96(X1,X0)
| v_y = X0 ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1870,plain,
! [X0,X1] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L)
| v_y != X0
| sP96(X1,X0)
| ~ sP95(X1,X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1871,plain,
! [X0,X1] :
( ~ sP95(X1,X0)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L)
| sP96(X1,X0)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1872,plain,
! [X0,X1] :
( ~ sP95(X1,X0)
| v_y = X1
| sP96(X1,X0)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1875,plain,
( v_y != sK92
| v_x != sK91
| sP95(sK94,sK93) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1876,plain,
( v_y = sK92
| v_y = sK91
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91,sK92),v_L)
| sP95(sK94,sK93) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1877,plain,
( v_y = sK91
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91,v_x),v_L)
| v_y != sK92
| sP95(sK94,sK93) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1878,plain,
( v_y = sK92
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK92),v_L)
| v_y != sK91
| sP95(sK94,sK93) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1879,plain,
( v_y != sK91
| v_x != sK92
| sP95(sK94,sK93) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1880,plain,
( v_y = sK91
| v_y = sK92
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK92,sK91),v_L)
| sP95(sK94,sK93) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1881,plain,
( v_y = sK92
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK92,v_x),v_L)
| v_y != sK91
| sP95(sK94,sK93) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1882,plain,
( v_y = sK91
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK91),v_L)
| v_y != sK92
| sP95(sK94,sK93) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f1883,plain,
( sK91 != sK92
| sP95(sK94,sK93) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f2057,plain,
! [X1] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L)
| sP96(X1,v_y)
| ~ sP95(X1,v_y) ),
inference(equality_resolution,[],[f1870]) ).
fof(f2058,plain,
! [X1] : ~ sP96(X1,v_y),
inference(equality_resolution,[],[f1866]) ).
fof(f2059,plain,
! [X0] : ~ sP96(v_y,X0),
inference(equality_resolution,[],[f1865]) ).
fof(f2061,plain,
! [X0] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK98(X0)),v_L)
| sP96(v_y,X0)
| ~ sP95(v_y,X0) ),
inference(equality_resolution,[],[f1857]) ).
fof(f2063,plain,
! [X1] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L)
| sP100(sK97(X1),X1)
| sP101(sK97(X1),X1)
| sP96(X1,v_y)
| ~ sP95(X1,v_y) ),
inference(equality_resolution,[],[f1845]) ).
fof(f2095,definition,
( spl103_3
<=> sP95(sK94,sK93) ),
introduced(definition,[new_symbols(definition,[spl103_3])],[avatar_definition]) ).
fof(f2097,plain,
( sP95(sK94,sK93)
| ~ spl103_3 ),
inference(avatar_component_clause,[],[f2095]) ).
fof(f2099,definition,
( spl103_4
<=> v_x = sK91 ),
introduced(definition,[new_symbols(definition,[spl103_4])],[avatar_definition]) ).
fof(f2103,definition,
( spl103_5
<=> v_y = sK92 ),
introduced(definition,[new_symbols(definition,[spl103_5])],[avatar_definition]) ).
fof(f2104,plain,
( v_y = sK92
| ~ spl103_5 ),
inference(avatar_component_clause,[],[f2103]) ).
fof(f2106,plain,
( spl103_3
| ~ spl103_4
| ~ spl103_5 ),
inference(avatar_split_clause,[],[f1875,f2103,f2099,f2095]) ).
fof(f2108,definition,
( spl103_6
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91,sK92),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_6])],[avatar_definition]) ).
fof(f2110,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,sK91,sK92),v_L)
| spl103_6 ),
inference(avatar_component_clause,[],[f2108]) ).
fof(f2112,definition,
( spl103_7
<=> v_y = sK91 ),
introduced(definition,[new_symbols(definition,[spl103_7])],[avatar_definition]) ).
fof(f2114,plain,
( v_y = sK91
| ~ spl103_7 ),
inference(avatar_component_clause,[],[f2112]) ).
fof(f2115,plain,
( spl103_3
| ~ spl103_6
| spl103_7
| spl103_5 ),
inference(avatar_split_clause,[],[f1876,f2103,f2112,f2108,f2095]) ).
fof(f2117,definition,
( spl103_8
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91,v_x),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_8])],[avatar_definition]) ).
fof(f2119,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,sK91,v_x),v_L)
| spl103_8 ),
inference(avatar_component_clause,[],[f2117]) ).
fof(f2120,plain,
( spl103_3
| ~ spl103_5
| ~ spl103_8
| spl103_7 ),
inference(avatar_split_clause,[],[f1877,f2112,f2117,f2103,f2095]) ).
fof(f2122,definition,
( spl103_9
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK92),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_9])],[avatar_definition]) ).
fof(f2124,plain,
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK92),v_L)
| spl103_9 ),
inference(avatar_component_clause,[],[f2122]) ).
fof(f2125,plain,
( spl103_3
| ~ spl103_7
| ~ spl103_9
| spl103_5 ),
inference(avatar_split_clause,[],[f1878,f2103,f2122,f2112,f2095]) ).
fof(f2127,definition,
( spl103_10
<=> v_x = sK92 ),
introduced(definition,[new_symbols(definition,[spl103_10])],[avatar_definition]) ).
fof(f2130,plain,
( spl103_3
| ~ spl103_10
| ~ spl103_7 ),
inference(avatar_split_clause,[],[f1879,f2112,f2127,f2095]) ).
fof(f2132,definition,
( spl103_11
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK92,sK91),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_11])],[avatar_definition]) ).
fof(f2135,plain,
( spl103_3
| ~ spl103_11
| spl103_5
| spl103_7 ),
inference(avatar_split_clause,[],[f1880,f2112,f2103,f2132,f2095]) ).
fof(f2137,definition,
( spl103_12
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK92,v_x),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_12])],[avatar_definition]) ).
fof(f2140,plain,
( spl103_3
| ~ spl103_7
| ~ spl103_12
| spl103_5 ),
inference(avatar_split_clause,[],[f1881,f2103,f2137,f2112,f2095]) ).
fof(f2142,definition,
( spl103_13
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK91),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_13])],[avatar_definition]) ).
fof(f2145,plain,
( spl103_3
| ~ spl103_5
| ~ spl103_13
| spl103_7 ),
inference(avatar_split_clause,[],[f1882,f2112,f2142,f2103,f2095]) ).
fof(f2147,definition,
( spl103_14
<=> sK91 = sK92 ),
introduced(definition,[new_symbols(definition,[spl103_14])],[avatar_definition]) ).
fof(f2149,plain,
( sK91 != sK92
| spl103_14 ),
inference(avatar_component_clause,[],[f2147]) ).
fof(f2150,plain,
( spl103_3
| ~ spl103_14 ),
inference(avatar_split_clause,[],[f1883,f2147,f2095]) ).
fof(f2172,plain,
! [X1] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X1),v_L)
| ~ sP95(X1,v_y) ),
inference(forward_subsumption_resolution,[],[f2057,f2058]) ).
fof(f2179,plain,
! [X0] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK98(X0)),v_L)
| ~ sP95(v_y,X0) ),
inference(forward_subsumption_resolution,[],[f2061,f2059]) ).
fof(f2216,plain,
! [X0,X1] :
( ~ sP95(X1,X0)
| sP100(sK97(X1),X1)
| v_y = X1
| sP96(X1,X0)
| v_y = sK97(X1) ),
inference(forward_subsumption_resolution,[],[f1848,f1840]) ).
fof(f2238,plain,
! [X1] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,v_x),v_L)
| sP101(sK97(X1),X1)
| sP100(sK97(X1),X1)
| ~ sP95(X1,v_y) ),
inference(forward_subsumption_resolution,[],[f2063,f2058]) ).
fof(f2243,plain,
! [X0,X1] :
( ~ sP96(X1,X0)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,sK99(X0,X1)),v_L)
| v_y = sK99(X0,X1) ),
inference(forward_subsumption_resolution,[],[f1834,f1824]) ).
fof(f2244,plain,
! [X0,X1] :
( ~ sP96(X1,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,sK99(X0,X1)),v_L)
| v_y = sK99(X0,X1) ),
inference(forward_subsumption_resolution,[],[f1835,f1824]) ).
fof(f2245,plain,
! [X0,X1] :
( ~ sP95(X1,X0)
| sP100(sK97(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,v_x),v_L)
| sP96(X1,X0)
| v_y = sK97(X1) ),
inference(forward_subsumption_resolution,[],[f1846,f1840]) ).
fof(f2246,plain,
! [X0,X1] :
( ~ sP95(X1,X0)
| sP100(sK97(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,sK98(X0)),v_L)
| sP96(X1,X0)
| v_y = sK97(X1) ),
inference(forward_subsumption_resolution,[],[f1850,f1840]) ).
fof(f2248,plain,
! [X0,X1] :
( ~ sP96(X1,X0)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,sK99(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,v_x),v_L) ),
inference(forward_subsumption_resolution,[],[f1832,f1826]) ).
fof(f2249,plain,
! [X0,X1] :
( ~ sP96(X1,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,sK99(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,v_x),v_L) ),
inference(forward_subsumption_resolution,[],[f1833,f1826]) ).
fof(f2254,plain,
~ sP95(v_x,v_y),
inference(resolution,[],[f1823,f2172]) ).
fof(f2316,definition,
( spl103_27
<=> v_y = sK97(sK94) ),
introduced(definition,[new_symbols(definition,[spl103_27])],[avatar_definition]) ).
fof(f2318,plain,
( v_y = sK97(sK94)
| ~ spl103_27 ),
inference(avatar_component_clause,[],[f2316]) ).
fof(f2320,definition,
( spl103_28
<=> sP96(sK94,sK93) ),
introduced(definition,[new_symbols(definition,[spl103_28])],[avatar_definition]) ).
fof(f2322,plain,
( sP96(sK94,sK93)
| ~ spl103_28 ),
inference(avatar_component_clause,[],[f2320]) ).
fof(f2328,definition,
( spl103_30
<=> sP100(sK97(sK94),sK94) ),
introduced(definition,[new_symbols(definition,[spl103_30])],[avatar_definition]) ).
fof(f2329,plain,
( ~ sP100(sK97(sK94),sK94)
| spl103_30 ),
inference(avatar_component_clause,[],[f2328]) ).
fof(f2330,plain,
( sP100(sK97(sK94),sK94)
| ~ spl103_30 ),
inference(avatar_component_clause,[],[f2328]) ).
fof(f2333,definition,
( spl103_31
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93,sK98(sK93)),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_31])],[avatar_definition]) ).
fof(f2335,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,sK93,sK98(sK93)),v_L)
| spl103_31 ),
inference(avatar_component_clause,[],[f2333]) ).
fof(f2338,definition,
( spl103_32
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93,v_x),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_32])],[avatar_definition]) ).
fof(f2339,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,sK93,v_x),v_L)
| spl103_32 ),
inference(avatar_component_clause,[],[f2338]) ).
fof(f2340,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,sK93,v_x),v_L)
| ~ spl103_32 ),
inference(avatar_component_clause,[],[f2338]) ).
fof(f2343,definition,
( spl103_33
<=> v_y = sK94 ),
introduced(definition,[new_symbols(definition,[spl103_33])],[avatar_definition]) ).
fof(f2344,plain,
( v_y != sK94
| spl103_33 ),
inference(avatar_component_clause,[],[f2343]) ).
fof(f2345,plain,
( v_y = sK94
| ~ spl103_33 ),
inference(avatar_component_clause,[],[f2343]) ).
fof(f2348,definition,
( spl103_34
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK94),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_34])],[avatar_definition]) ).
fof(f2354,definition,
( spl103_35
<=> v_y = sK93 ),
introduced(definition,[new_symbols(definition,[spl103_35])],[avatar_definition]) ).
fof(f2356,plain,
( v_y = sK93
| ~ spl103_35 ),
inference(avatar_component_clause,[],[f2354]) ).
fof(f2363,definition,
( spl103_36
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK94,v_x),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_36])],[avatar_definition]) ).
fof(f2365,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,sK94,v_x),v_L)
| ~ spl103_36 ),
inference(avatar_component_clause,[],[f2363]) ).
fof(f2367,definition,
( spl103_37
<=> sP101(sK97(sK94),sK94) ),
introduced(definition,[new_symbols(definition,[spl103_37])],[avatar_definition]) ).
fof(f2369,plain,
( sP101(sK97(sK94),sK94)
| ~ spl103_37 ),
inference(avatar_component_clause,[],[f2367]) ).
fof(f2381,definition,
( spl103_38
<=> v_y = sK99(sK93,sK94) ),
introduced(definition,[new_symbols(definition,[spl103_38])],[avatar_definition]) ).
fof(f2383,plain,
( v_y = sK99(sK93,sK94)
| ~ spl103_38 ),
inference(avatar_component_clause,[],[f2381]) ).
fof(f2385,definition,
( spl103_39
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK94,sK99(sK93,sK94)),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_39])],[avatar_definition]) ).
fof(f2387,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,sK94,sK99(sK93,sK94)),v_L)
| ~ spl103_39 ),
inference(avatar_component_clause,[],[f2385]) ).
fof(f2390,definition,
( spl103_40
<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93,sK99(sK93,sK94)),v_L) ),
introduced(definition,[new_symbols(definition,[spl103_40])],[avatar_definition]) ).
fof(f2392,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,sK93,sK99(sK93,sK94)),v_L)
| spl103_40 ),
inference(avatar_component_clause,[],[f2390]) ).
fof(f2441,plain,
! [X2,X0,X1] :
( ~ sP100(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,X2),v_L)
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),v_L) ),
inference(resolution,[],[f1821,f1842]) ).
fof(f2505,plain,
! [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)
| hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1)))
| X0 = X1 ),
inference(resolution,[],[f1051,f1822]) ).
fof(f2507,plain,
! [X0,X1] :
( hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1)))
| ~ sP96(X1,X0) ),
inference(resolution,[],[f1051,f1867]) ).
fof(f2514,plain,
! [X0] :
( ~ sP95(X0,v_y)
| hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,X0))) ),
inference(resolution,[],[f1051,f2172]) ).
fof(f2515,plain,
! [X0] :
( ~ sP95(v_y,X0)
| hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK98(X0)))) ),
inference(resolution,[],[f1051,f2179]) ).
fof(f2518,plain,
( hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK94,sK99(sK93,sK94))))
| ~ spl103_39 ),
inference(resolution,[],[f1051,f2387]) ).
fof(f2528,plain,
! [X2,X0,X1] :
( ~ sP96(X0,X1)
| c_member(X2,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L) ),
inference(resolution,[],[f2507,f1050]) ).
fof(f2532,plain,
( ! [X0] : c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK94,sK99(sK93,sK94)),v_L)
| ~ spl103_39 ),
inference(resolution,[],[f2518,f1050]) ).
fof(f2571,definition,
( spl103_53
<=> hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK94))) ),
introduced(definition,[new_symbols(definition,[spl103_53])],[avatar_definition]) ).
fof(f2572,plain,
( ~ hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK94)))
| spl103_53 ),
inference(avatar_component_clause,[],[f2571]) ).
fof(f2573,plain,
( hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK94)))
| ~ spl103_53 ),
inference(avatar_component_clause,[],[f2571]) ).
fof(f2575,plain,
( ! [X0] : c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK94),v_L)
| ~ spl103_53 ),
inference(resolution,[],[f2573,f1050]) ).
fof(f2577,plain,
( ! [X0] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,sK94),v_L)
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L) )
| ~ spl103_53 ),
inference(resolution,[],[f2575,f1821]) ).
fof(f2652,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,sK94,v_x),v_L)
| ~ spl103_53 ),
inference(resolution,[],[f2577,f1823]) ).
fof(f2656,plain,
( sP101(sK97(sK94),sK94)
| sP100(sK97(sK94),sK94)
| ~ sP95(sK94,v_y)
| ~ spl103_53 ),
inference(resolution,[],[f2652,f2238]) ).
fof(f2663,definition,
( spl103_59
<=> sP95(sK94,v_y) ),
introduced(definition,[new_symbols(definition,[spl103_59])],[avatar_definition]) ).
fof(f2664,plain,
( sP95(sK94,v_y)
| ~ spl103_59 ),
inference(avatar_component_clause,[],[f2663]) ).
fof(f2665,plain,
( ~ sP95(sK94,v_y)
| spl103_59 ),
inference(avatar_component_clause,[],[f2663]) ).
fof(f2666,plain,
( ~ spl103_59
| spl103_30
| spl103_37
| ~ spl103_53 ),
inference(avatar_split_clause,[],[f2656,f2571,f2367,f2328,f2663]) ).
fof(f2668,plain,
( ! [X0] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,sK97(sK94)),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,sK94),v_L) )
| ~ spl103_30 ),
inference(resolution,[],[f2330,f2441]) ).
fof(f2743,plain,
( ! [X0] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK94),v_L)
| ~ sP100(sK97(sK94),X0) )
| ~ spl103_30 ),
inference(resolution,[],[f2668,f1843]) ).
fof(f2772,definition,
( spl103_63
<=> ! [X0] : ~ sP100(sK97(sK94),X0) ),
introduced(definition,[new_symbols(definition,[spl103_63])],[avatar_definition]) ).
fof(f2773,plain,
( ! [X0] : ~ sP100(sK97(sK94),X0)
| ~ spl103_63 ),
inference(avatar_component_clause,[],[f2772]) ).
fof(f2774,plain,
( spl103_63
| ~ spl103_34
| ~ spl103_30 ),
inference(avatar_split_clause,[],[f2743,f2328,f2348,f2772]) ).
fof(f2777,plain,
( $false
| ~ spl103_30
| ~ spl103_63 ),
inference(resolution,[],[f2773,f2330]) ).
fof(f2778,plain,
( ~ spl103_30
| ~ spl103_63 ),
inference(avatar_contradiction_clause,[],[f2777]) ).
fof(f2796,definition,
( spl103_64
<=> v_x = sK94 ),
introduced(definition,[new_symbols(definition,[spl103_64])],[avatar_definition]) ).
fof(f2797,plain,
( v_x != sK94
| spl103_64 ),
inference(avatar_component_clause,[],[f2796]) ).
fof(f2798,plain,
( v_x = sK94
| ~ spl103_64 ),
inference(avatar_component_clause,[],[f2796]) ).
fof(f2803,plain,
( ! [X0] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,sK94),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L) )
| ~ spl103_36 ),
inference(resolution,[],[f2365,f1821]) ).
fof(f2852,plain,
( hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93,v_x)))
| ~ spl103_32 ),
inference(resolution,[],[f2340,f1051]) ).
fof(f2856,plain,
( ! [X0] : c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93,v_x),v_L)
| ~ spl103_32 ),
inference(resolution,[],[f2852,f1050]) ).
fof(f3067,plain,
( ! [X0] :
( ~ sP96(sK94,X0)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L) )
| ~ spl103_36 ),
inference(resolution,[],[f2803,f1867]) ).
fof(f3072,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,sK93,v_x),v_L)
| ~ spl103_28
| ~ spl103_36 ),
inference(resolution,[],[f3067,f2322]) ).
fof(f3257,definition,
( spl103_77
<=> sK93 = sK98(sK93) ),
introduced(definition,[new_symbols(definition,[spl103_77])],[avatar_definition]) ).
fof(f3258,plain,
( sK93 != sK98(sK93)
| spl103_77 ),
inference(avatar_component_clause,[],[f3257]) ).
fof(f3259,plain,
( sK93 = sK98(sK93)
| ~ spl103_77 ),
inference(avatar_component_clause,[],[f3257]) ).
fof(f3472,plain,
! [X0,X1] :
( ~ sP95(X1,X0)
| sK98(X0) = X0
| v_y = X0
| sP96(X1,X0)
| hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK98(X0),X0))) ),
inference(resolution,[],[f2505,f1864]) ).
fof(f4306,plain,
( v_y != sK92
| ~ spl103_7
| spl103_14 ),
inference(forward_demodulation,[],[f2149,f2114]) ).
fof(f4539,plain,
( $false
| ~ spl103_5
| ~ spl103_7
| spl103_14 ),
inference(forward_subsumption_resolution,[],[f4306,f2104]) ).
fof(f4540,plain,
( ~ spl103_5
| ~ spl103_7
| spl103_14 ),
inference(avatar_contradiction_clause,[],[f4539]) ).
fof(f4680,plain,
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK91),v_L)
| v_x = sK91
| spl103_8 ),
inference(resolution,[],[f2119,f1822]) ).
fof(f4697,plain,
( sP95(v_x,sK93)
| ~ spl103_3
| ~ spl103_64 ),
inference(forward_demodulation,[],[f2097,f2798]) ).
fof(f4724,plain,
( sP95(v_y,sK93)
| ~ spl103_3
| ~ spl103_33 ),
inference(forward_demodulation,[],[f2097,f2345]) ).
fof(f4755,plain,
( hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK98(sK93))))
| ~ spl103_3
| ~ spl103_33 ),
inference(resolution,[],[f4724,f2515]) ).
fof(f4776,plain,
( sK93 = sK98(sK93)
| v_y = sK93
| sP96(v_y,sK93)
| hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK98(sK93),sK93)))
| ~ spl103_3
| ~ spl103_33 ),
inference(resolution,[],[f4724,f3472]) ).
fof(f4777,plain,
( v_y = sK93
| sP96(v_y,sK93)
| hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK98(sK93),sK93)))
| ~ spl103_3
| ~ spl103_33
| spl103_77 ),
inference(forward_subsumption_resolution,[],[f4776,f3258]) ).
fof(f4793,plain,
( v_y = sK93
| hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK98(sK93),sK93)))
| ~ spl103_3
| ~ spl103_33
| spl103_77 ),
inference(forward_subsumption_resolution,[],[f4777,f2059]) ).
fof(f4827,definition,
( spl103_108
<=> hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK98(sK93),sK93))) ),
introduced(definition,[new_symbols(definition,[spl103_108])],[avatar_definition]) ).
fof(f4829,plain,
( hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK98(sK93),sK93)))
| ~ spl103_108 ),
inference(avatar_component_clause,[],[f4827]) ).
fof(f4830,plain,
( spl103_108
| spl103_35
| ~ spl103_3
| ~ spl103_33
| spl103_77 ),
inference(avatar_split_clause,[],[f4793,f3257,f2343,f2095,f2354,f4827]) ).
fof(f4879,plain,
( ! [X0] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,sK93),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,v_x),v_L) )
| ~ spl103_32 ),
inference(resolution,[],[f2856,f1821]) ).
fof(f4890,plain,
( ! [X0] : c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK98(sK93),sK93),v_L)
| ~ spl103_108 ),
inference(resolution,[],[f4829,f1050]) ).
fof(f4897,plain,
( ! [X0] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,sK98(sK93)),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,sK93),v_L) )
| ~ spl103_108 ),
inference(resolution,[],[f4890,f1821]) ).
fof(f4947,plain,
( ! [X0] : c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK98(sK93)),v_L)
| ~ spl103_3
| ~ spl103_33 ),
inference(resolution,[],[f4755,f1050]) ).
fof(f5031,plain,
( hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK98(sK93),sK93)))
| sK93 = sK98(sK93)
| spl103_31 ),
inference(resolution,[],[f2335,f2505]) ).
fof(f6126,plain,
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK93),v_L)
| ~ spl103_3
| ~ spl103_33
| ~ spl103_108 ),
inference(resolution,[],[f4897,f4947]) ).
fof(f6143,plain,
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,v_x),v_L)
| ~ spl103_3
| ~ spl103_32
| ~ spl103_33
| ~ spl103_108 ),
inference(resolution,[],[f6126,f4879]) ).
fof(f6149,plain,
( $false
| ~ spl103_3
| ~ spl103_32
| ~ spl103_33
| ~ spl103_108 ),
inference(forward_subsumption_resolution,[],[f6143,f1823]) ).
fof(f6150,plain,
( ~ spl103_3
| ~ spl103_32
| ~ spl103_33
| ~ spl103_108 ),
inference(avatar_contradiction_clause,[],[f6149]) ).
fof(f6155,plain,
( spl103_77
| spl103_108
| spl103_31 ),
inference(avatar_split_clause,[],[f5031,f2333,f4827,f3257]) ).
fof(f6179,plain,
( ! [X0] : c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK93),v_L)
| ~ spl103_3
| ~ spl103_33
| ~ spl103_77 ),
inference(superposition,[],[f4947,f3259]) ).
fof(f6206,plain,
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,v_x),v_L)
| ~ spl103_3
| ~ spl103_32
| ~ spl103_33
| ~ spl103_77 ),
inference(resolution,[],[f6179,f4879]) ).
fof(f6212,plain,
( $false
| ~ spl103_3
| ~ spl103_32
| ~ spl103_33
| ~ spl103_77 ),
inference(forward_subsumption_resolution,[],[f6206,f1823]) ).
fof(f6213,plain,
( ~ spl103_3
| ~ spl103_32
| ~ spl103_33
| ~ spl103_77 ),
inference(avatar_contradiction_clause,[],[f6212]) ).
fof(f6219,plain,
( spl103_4
| spl103_13
| spl103_8 ),
inference(avatar_split_clause,[],[f4680,f2117,f2142,f2099]) ).
fof(f6235,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,sK93,sK98(sK93)),v_L)
| sP96(sK94,sK93)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK94),v_L)
| ~ spl103_3 ),
inference(resolution,[],[f2097,f1861]) ).
fof(f6237,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,sK93,v_x),v_L)
| sP96(sK94,sK93)
| v_y = sK93
| ~ spl103_3 ),
inference(resolution,[],[f2097,f1868]) ).
fof(f6238,plain,
( v_y = sK94
| sP96(sK94,sK93)
| v_y = sK93
| ~ spl103_3 ),
inference(resolution,[],[f2097,f1869]) ).
fof(f6239,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,sK93,v_x),v_L)
| sP96(sK94,sK93)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK94),v_L)
| ~ spl103_3 ),
inference(resolution,[],[f2097,f1871]) ).
fof(f6240,plain,
( v_y = sK94
| sP96(sK94,sK93)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK94),v_L)
| ~ spl103_3 ),
inference(resolution,[],[f2097,f1872]) ).
fof(f6241,plain,
( sP100(sK97(sK94),sK94)
| v_y = sK94
| sP96(sK94,sK93)
| v_y = sK97(sK94)
| ~ spl103_3 ),
inference(resolution,[],[f2097,f2216]) ).
fof(f6242,plain,
( sP100(sK97(sK94),sK94)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93,v_x),v_L)
| sP96(sK94,sK93)
| v_y = sK97(sK94)
| ~ spl103_3 ),
inference(resolution,[],[f2097,f2245]) ).
fof(f6243,plain,
( sP100(sK97(sK94),sK94)
| ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93,sK98(sK93)),v_L)
| sP96(sK94,sK93)
| v_y = sK97(sK94)
| ~ spl103_3 ),
inference(resolution,[],[f2097,f2246]) ).
fof(f6301,plain,
( sP95(sK94,v_y)
| ~ spl103_3
| ~ spl103_35 ),
inference(superposition,[],[f2097,f2356]) ).
fof(f6350,plain,
( sP96(sK94,sK93)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK94),v_L)
| ~ spl103_3
| spl103_33 ),
inference(forward_subsumption_resolution,[],[f6240,f2344]) ).
fof(f6351,plain,
( spl103_34
| spl103_28
| spl103_32
| ~ spl103_3 ),
inference(avatar_split_clause,[],[f6239,f2095,f2338,f2320,f2348]) ).
fof(f6352,plain,
( sP96(sK94,sK93)
| v_y = sK93
| ~ spl103_3
| spl103_33 ),
inference(forward_subsumption_resolution,[],[f6238,f2344]) ).
fof(f6353,plain,
( spl103_35
| spl103_28
| spl103_32
| ~ spl103_3 ),
inference(avatar_split_clause,[],[f6237,f2095,f2338,f2320,f2354]) ).
fof(f6355,plain,
( spl103_34
| spl103_28
| ~ spl103_31
| ~ spl103_3 ),
inference(avatar_split_clause,[],[f6235,f2095,f2333,f2320,f2348]) ).
fof(f6361,plain,
( spl103_34
| spl103_28
| ~ spl103_3
| spl103_33 ),
inference(avatar_split_clause,[],[f6350,f2343,f2095,f2320,f2348]) ).
fof(f6362,plain,
( spl103_35
| spl103_28
| ~ spl103_3
| spl103_33 ),
inference(avatar_split_clause,[],[f6352,f2343,f2095,f2320,f2354]) ).
fof(f6383,plain,
( ! [X0] : c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93,sK94),v_L)
| ~ spl103_28 ),
inference(resolution,[],[f2322,f2528]) ).
fof(f6446,plain,
( sP101(v_y,sK94)
| ~ spl103_27
| ~ spl103_37 ),
inference(forward_demodulation,[],[f2369,f2318]) ).
fof(f6448,plain,
( v_x = sK94
| ~ spl103_27
| ~ spl103_37 ),
inference(resolution,[],[f6446,f1839]) ).
fof(f6612,plain,
( sP95(v_x,sK93)
| ~ spl103_3
| ~ spl103_27
| ~ spl103_37 ),
inference(superposition,[],[f2097,f6448]) ).
fof(f6723,plain,
( v_y != v_y
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK94,v_x),v_L)
| sP102(v_y,sK94,sK93)
| ~ sP96(sK94,sK93)
| ~ spl103_38 ),
inference(superposition,[],[f1836,f2383]) ).
fof(f6726,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,sK94,v_x),v_L)
| sP102(v_y,sK94,sK93)
| ~ sP96(sK94,sK93)
| ~ spl103_38 ),
inference(trivial_inequality_removal,[],[f6723]) ).
fof(f6728,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,sK94,v_x),v_L)
| sP102(v_y,sK94,sK93)
| ~ spl103_28
| ~ spl103_38 ),
inference(forward_subsumption_resolution,[],[f6726,f2322]) ).
fof(f6730,definition,
( spl103_145
<=> sP102(v_y,sK94,sK93) ),
introduced(definition,[new_symbols(definition,[spl103_145])],[avatar_definition]) ).
fof(f6732,plain,
( sP102(v_y,sK94,sK93)
| ~ spl103_145 ),
inference(avatar_component_clause,[],[f6730]) ).
fof(f6733,plain,
( spl103_145
| spl103_36
| ~ spl103_28
| ~ spl103_38 ),
inference(avatar_split_clause,[],[f6728,f2381,f2320,f2363,f6730]) ).
fof(f6746,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,sK92,sK91),v_L)
| sK91 = sK92
| spl103_6 ),
inference(resolution,[],[f2110,f1822]) ).
fof(f6751,plain,
( spl103_14
| spl103_11
| spl103_6 ),
inference(avatar_split_clause,[],[f6746,f2108,f2132,f2147]) ).
fof(f7255,plain,
( ~ sP96(v_x,sK93)
| spl103_32 ),
inference(resolution,[],[f2339,f1867]) ).
fof(f7316,plain,
( $false
| ~ spl103_28
| spl103_32
| ~ spl103_36 ),
inference(forward_subsumption_resolution,[],[f3072,f2339]) ).
fof(f7317,plain,
( ~ spl103_28
| spl103_32
| ~ spl103_36 ),
inference(avatar_contradiction_clause,[],[f7316]) ).
fof(f7758,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,sK92,v_x),v_L)
| v_x = sK92
| spl103_9 ),
inference(resolution,[],[f2124,f1822]) ).
fof(f10746,plain,
( ! [X0] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,sK99(sK93,sK94)),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,sK94),v_L) )
| ~ spl103_39 ),
inference(resolution,[],[f2532,f1821]) ).
fof(f13515,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,sK93,sK94),v_L)
| ~ spl103_39
| spl103_40 ),
inference(resolution,[],[f10746,f2392]) ).
fof(f13519,plain,
( $false
| ~ spl103_28
| ~ spl103_39
| spl103_40 ),
inference(forward_subsumption_resolution,[],[f13515,f6383]) ).
fof(f13520,plain,
( ~ spl103_28
| ~ spl103_39
| spl103_40 ),
inference(avatar_contradiction_clause,[],[f13519]) ).
fof(f13772,plain,
( $false
| ~ spl103_3
| ~ spl103_35
| spl103_59 ),
inference(forward_subsumption_resolution,[],[f6301,f2665]) ).
fof(f13773,plain,
( ~ spl103_3
| ~ spl103_35
| spl103_59 ),
inference(avatar_contradiction_clause,[],[f13772]) ).
fof(f13775,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,sK93,sK98(sK93)),v_L)
| sP96(sK94,sK93)
| v_y = sK97(sK94)
| ~ spl103_3
| spl103_30 ),
inference(forward_subsumption_resolution,[],[f6243,f2329]) ).
fof(f13776,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,sK93,v_x),v_L)
| sP96(sK94,sK93)
| v_y = sK97(sK94)
| ~ spl103_3
| spl103_30 ),
inference(forward_subsumption_resolution,[],[f6242,f2329]) ).
fof(f13777,plain,
( v_y = sK94
| sP96(sK94,sK93)
| v_y = sK97(sK94)
| ~ spl103_3
| spl103_30 ),
inference(forward_subsumption_resolution,[],[f6241,f2329]) ).
fof(f13784,plain,
( spl103_10
| spl103_12
| spl103_9 ),
inference(avatar_split_clause,[],[f7758,f2122,f2137,f2127]) ).
fof(f13791,plain,
( spl103_27
| spl103_28
| ~ spl103_31
| ~ spl103_3
| spl103_30 ),
inference(avatar_split_clause,[],[f13775,f2328,f2095,f2333,f2320,f2316]) ).
fof(f13792,plain,
( spl103_27
| spl103_28
| spl103_32
| ~ spl103_3
| spl103_30 ),
inference(avatar_split_clause,[],[f13776,f2328,f2095,f2338,f2320,f2316]) ).
fof(f13793,plain,
( sP96(sK94,sK93)
| v_y = sK97(sK94)
| ~ spl103_3
| spl103_30
| spl103_33 ),
inference(forward_subsumption_resolution,[],[f13777,f2344]) ).
fof(f13798,plain,
( spl103_27
| spl103_28
| ~ spl103_3
| spl103_30
| spl103_33 ),
inference(avatar_split_clause,[],[f13793,f2343,f2328,f2095,f2320,f2316]) ).
fof(f13836,plain,
( hBOOL(hAPP(v_L,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,sK94)))
| ~ spl103_59 ),
inference(resolution,[],[f2664,f2514]) ).
fof(f14311,plain,
( $false
| spl103_53
| ~ spl103_59 ),
inference(forward_subsumption_resolution,[],[f13836,f2572]) ).
fof(f14312,plain,
( spl103_53
| ~ spl103_59 ),
inference(avatar_contradiction_clause,[],[f14311]) ).
fof(f14322,plain,
( sP95(v_x,v_y)
| ~ spl103_3
| ~ spl103_27
| ~ spl103_35
| ~ spl103_37 ),
inference(forward_demodulation,[],[f6612,f2356]) ).
fof(f14334,plain,
( $false
| ~ spl103_3
| ~ spl103_27
| ~ spl103_35
| ~ spl103_37 ),
inference(forward_subsumption_resolution,[],[f14322,f2254]) ).
fof(f14335,plain,
( ~ spl103_3
| ~ spl103_27
| ~ spl103_35
| ~ spl103_37 ),
inference(avatar_contradiction_clause,[],[f14334]) ).
fof(f14387,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,sK94,sK99(sK93,sK94)),v_L)
| v_y = sK99(sK93,sK94)
| ~ spl103_28 ),
inference(resolution,[],[f2322,f2243]) ).
fof(f14388,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,sK93,sK99(sK93,sK94)),v_L)
| v_y = sK99(sK93,sK94)
| ~ spl103_28 ),
inference(resolution,[],[f2322,f2244]) ).
fof(f14389,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,sK94,sK99(sK93,sK94)),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,sK93,v_x),v_L)
| ~ spl103_28 ),
inference(resolution,[],[f2322,f2248]) ).
fof(f14390,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,sK93,sK99(sK93,sK94)),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,sK93,v_x),v_L)
| ~ spl103_28 ),
inference(resolution,[],[f2322,f2249]) ).
fof(f14395,plain,
( ~ spl103_32
| ~ spl103_40
| ~ spl103_28 ),
inference(avatar_split_clause,[],[f14390,f2320,f2390,f2338]) ).
fof(f14396,plain,
( ~ spl103_32
| spl103_39
| ~ spl103_28 ),
inference(avatar_split_clause,[],[f14389,f2320,f2385,f2338]) ).
fof(f14397,plain,
( spl103_38
| ~ spl103_40
| ~ spl103_28 ),
inference(avatar_split_clause,[],[f14388,f2320,f2390,f2381]) ).
fof(f14398,plain,
( spl103_38
| spl103_39
| ~ spl103_28 ),
inference(avatar_split_clause,[],[f14387,f2320,f2385,f2381]) ).
fof(f14580,plain,
( v_x = v_y
| sP96(v_x,sK93)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,v_x),v_L)
| ~ spl103_3
| ~ spl103_64 ),
inference(resolution,[],[f4697,f1872]) ).
fof(f14595,plain,
( sP96(v_x,sK93)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,v_x),v_L)
| ~ spl103_3
| ~ spl103_64 ),
inference(forward_subsumption_resolution,[],[f14580,f1820]) ).
fof(f14613,plain,
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_x,v_x),v_L)
| ~ spl103_3
| spl103_32
| ~ spl103_64 ),
inference(forward_subsumption_resolution,[],[f14595,f7255]) ).
fof(f14631,plain,
( $false
| ~ spl103_3
| spl103_32
| ~ spl103_64 ),
inference(forward_subsumption_resolution,[],[f14613,f1823]) ).
fof(f14632,plain,
( ~ spl103_3
| spl103_32
| ~ spl103_64 ),
inference(avatar_contradiction_clause,[],[f14631]) ).
fof(f14658,plain,
( v_x = sK94
| ~ spl103_145 ),
inference(resolution,[],[f6732,f1825]) ).
fof(f14668,plain,
( $false
| spl103_64
| ~ spl103_145 ),
inference(forward_subsumption_resolution,[],[f14658,f2797]) ).
fof(f14669,plain,
( spl103_64
| ~ spl103_145 ),
inference(avatar_contradiction_clause,[],[f14668]) ).
cnf(s2,plain,
( spl103_3
| ~ spl103_4
| ~ spl103_5 ),
inference(sat_conversion,[],[f2106]) ).
cnf(s3,plain,
( spl103_3
| spl103_5
| ~ spl103_6
| spl103_7 ),
inference(sat_conversion,[],[f2115]) ).
cnf(s4,plain,
( spl103_3
| ~ spl103_5
| spl103_7
| ~ spl103_8 ),
inference(sat_conversion,[],[f2120]) ).
cnf(s5,plain,
( spl103_3
| spl103_5
| ~ spl103_7
| ~ spl103_9 ),
inference(sat_conversion,[],[f2125]) ).
cnf(s6,plain,
( spl103_3
| ~ spl103_7
| ~ spl103_10 ),
inference(sat_conversion,[],[f2130]) ).
cnf(s7,plain,
( spl103_3
| spl103_5
| spl103_7
| ~ spl103_11 ),
inference(sat_conversion,[],[f2135]) ).
cnf(s8,plain,
( spl103_3
| spl103_5
| ~ spl103_7
| ~ spl103_12 ),
inference(sat_conversion,[],[f2140]) ).
cnf(s9,plain,
( spl103_3
| ~ spl103_5
| spl103_7
| ~ spl103_13 ),
inference(sat_conversion,[],[f2145]) ).
cnf(s10,plain,
( spl103_3
| ~ spl103_14 ),
inference(sat_conversion,[],[f2150]) ).
cnf(s57,plain,
( spl103_30
| spl103_37
| ~ spl103_53
| ~ spl103_59 ),
inference(sat_conversion,[],[f2666]) ).
cnf(s62,plain,
( ~ spl103_30
| ~ spl103_34
| spl103_63 ),
inference(sat_conversion,[],[f2774]) ).
cnf(s63,plain,
( ~ spl103_30
| ~ spl103_63 ),
inference(sat_conversion,[],[f2778]) ).
cnf(s109,plain,
( ~ spl103_5
| ~ spl103_7
| spl103_14 ),
inference(sat_conversion,[],[f4540]) ).
cnf(s125,plain,
( ~ spl103_3
| ~ spl103_33
| spl103_35
| spl103_77
| spl103_108 ),
inference(sat_conversion,[],[f4830]) ).
cnf(s146,plain,
( ~ spl103_3
| ~ spl103_32
| ~ spl103_33
| ~ spl103_108 ),
inference(sat_conversion,[],[f6150]) ).
cnf(s150,plain,
( spl103_31
| spl103_77
| spl103_108 ),
inference(sat_conversion,[],[f6155]) ).
cnf(s161,plain,
( ~ spl103_3
| ~ spl103_32
| ~ spl103_33
| ~ spl103_77 ),
inference(sat_conversion,[],[f6213]) ).
cnf(s163,plain,
( spl103_4
| spl103_8
| spl103_13 ),
inference(sat_conversion,[],[f6219]) ).
cnf(s192,plain,
( ~ spl103_3
| spl103_28
| spl103_32
| spl103_34 ),
inference(sat_conversion,[],[f6351]) ).
cnf(s193,plain,
( ~ spl103_3
| spl103_28
| spl103_32
| spl103_35 ),
inference(sat_conversion,[],[f6353]) ).
cnf(s195,plain,
( ~ spl103_3
| spl103_28
| ~ spl103_31
| spl103_34 ),
inference(sat_conversion,[],[f6355]) ).
cnf(s197,plain,
( ~ spl103_3
| spl103_28
| spl103_33
| spl103_34 ),
inference(sat_conversion,[],[f6361]) ).
cnf(s198,plain,
( ~ spl103_3
| spl103_28
| spl103_33
| spl103_35 ),
inference(sat_conversion,[],[f6362]) ).
cnf(s237,plain,
( ~ spl103_28
| spl103_36
| ~ spl103_38
| spl103_145 ),
inference(sat_conversion,[],[f6733]) ).
cnf(s239,plain,
( spl103_6
| spl103_11
| spl103_14 ),
inference(sat_conversion,[],[f6751]) ).
cnf(s259,plain,
( ~ spl103_28
| spl103_32
| ~ spl103_36 ),
inference(sat_conversion,[],[f7317]) ).
cnf(s318,plain,
( ~ spl103_28
| ~ spl103_39
| spl103_40 ),
inference(sat_conversion,[],[f13520]) ).
cnf(s410,plain,
( ~ spl103_3
| ~ spl103_35
| spl103_59 ),
inference(sat_conversion,[],[f13773]) ).
cnf(s413,plain,
( spl103_9
| spl103_10
| spl103_12 ),
inference(sat_conversion,[],[f13784]) ).
cnf(s416,plain,
( ~ spl103_3
| spl103_27
| spl103_28
| spl103_30
| ~ spl103_31 ),
inference(sat_conversion,[],[f13791]) ).
cnf(s417,plain,
( ~ spl103_3
| spl103_27
| spl103_28
| spl103_30
| spl103_32 ),
inference(sat_conversion,[],[f13792]) ).
cnf(s418,plain,
( ~ spl103_3
| spl103_27
| spl103_28
| spl103_30
| spl103_33 ),
inference(sat_conversion,[],[f13798]) ).
cnf(s440,plain,
( spl103_53
| ~ spl103_59 ),
inference(sat_conversion,[],[f14312]) ).
cnf(s447,plain,
( ~ spl103_3
| ~ spl103_27
| ~ spl103_35
| ~ spl103_37 ),
inference(sat_conversion,[],[f14335]) ).
cnf(s457,plain,
( ~ spl103_28
| ~ spl103_32
| ~ spl103_40 ),
inference(sat_conversion,[],[f14395]) ).
cnf(s458,plain,
( ~ spl103_28
| ~ spl103_32
| spl103_39 ),
inference(sat_conversion,[],[f14396]) ).
cnf(s459,plain,
( ~ spl103_28
| spl103_38
| ~ spl103_40 ),
inference(sat_conversion,[],[f14397]) ).
cnf(s460,plain,
( ~ spl103_28
| spl103_38
| spl103_39 ),
inference(sat_conversion,[],[f14398]) ).
cnf(s470,plain,
( ~ spl103_3
| spl103_32
| ~ spl103_64 ),
inference(sat_conversion,[],[f14632]) ).
cnf(s475,plain,
( spl103_64
| ~ spl103_145 ),
inference(sat_conversion,[],[f14669]) ).
cnf(s491,plain,
( ~ spl103_7
| spl103_5
| spl103_3 ),
inference(rat,[],[s413,s5,s8,s6]) ).
cnf(s492,plain,
( spl103_5
| spl103_3 ),
inference(rat,[],[s239,s3,s7,s491,s10]) ).
cnf(s493,plain,
( spl103_7
| ~ spl103_5
| spl103_3 ),
inference(rat,[],[s2,s163,s4,s9]) ).
cnf(s494,plain,
spl103_3,
inference(rat,[],[s493,s109,s492,s10]) ).
cnf(s496,plain,
( spl103_34
| spl103_28 ),
inference(rat,[],[s150,s146,s161,s197,s192,s195,s494]) ).
cnf(s497,plain,
( ~ spl103_33
| ~ spl103_32
| spl103_31 ),
inference(rat,[],[s150,s146,s161,s494]) ).
cnf(s498,plain,
( ~ spl103_30
| ~ spl103_34 ),
inference(rat,[],[s62,s63]) ).
cnf(s499,plain,
( spl103_30
| spl103_28
| spl103_27 ),
inference(rat,[],[s416,s497,s417,s418,s494]) ).
cnf(s500,plain,
( spl103_28
| spl103_27 ),
inference(rat,[],[s499,s498,s496]) ).
cnf(s501,plain,
( ~ spl103_32
| ~ spl103_28 ),
inference(rat,[],[s318,s457,s458]) ).
cnf(s502,plain,
( spl103_38
| ~ spl103_28 ),
inference(rat,[],[s318,s459,s460]) ).
cnf(s503,plain,
( spl103_36
| spl103_145
| ~ spl103_28 ),
inference(rat,[],[s502,s237]) ).
cnf(s504,plain,
~ spl103_28,
inference(rat,[],[s503,s475,s259,s470,s501,s494]) ).
cnf(s505,plain,
spl103_34,
inference(rat,[],[s496,s504]) ).
cnf(s506,plain,
spl103_27,
inference(rat,[],[s500,s504]) ).
cnf(s507,plain,
~ spl103_30,
inference(rat,[],[s498,s505]) ).
cnf(s509,plain,
( ~ spl103_32
| spl103_35 ),
inference(rat,[],[s125,s146,s161,s198,s494,s504]) ).
cnf(s510,plain,
spl103_35,
inference(rat,[],[s193,s509,s494,s504]) ).
cnf(s511,plain,
spl103_59,
inference(rat,[],[s410,s494,s510]) ).
cnf(s513,plain,
~ spl103_37,
inference(rat,[],[s447,s506,s494,s510]) ).
cnf(s514,plain,
spl103_53,
inference(rat,[],[s440,s511]) ).
cnf(s515,plain,
$false,
inference(rat,[],[s57,s513,s507,s514,s511]) ).
fof(f14670,plain,
$false,
inference(avatar_sat_refutation,[],[s515]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT117+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 % Computer : n009.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 23:44:00 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.41 Running first-order model finding
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.25/1.01 % (2530953)Will run a generic schedule for satisfiability detection.
% 2.25/1.01 % (2530962)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4082820462:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.25/1.01 % (2530959)% WARNING: option uhcvi not known.
% 2.25/1.01 % (2530958)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3058727290_2999 on theBenchmark for (2999ds/0Mi)
% 2.25/1.01 % (2530959)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=165253962:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.25/1.01 % (2530960)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2201879237:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.25/1.01 % (2530961)dis+10_1_sil=32000:sp=arity:random_seed=2046064998:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.25/1.01 % (2530963)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1682432688:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.25/1.01 % (2530964)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1154877800:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.25/1.01 % (2530962)Instruction limit reached!
% 2.25/1.01 % (2530962)------------------------------
% 2.25/1.01 % (2530962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/1.01 % (2530962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/1.01 % (2530962)CaDiCaL version: 2.1.3
% 2.25/1.01 % (2530962)Termination reason: Instruction limit
% 2.25/1.01 % (2530962)Termination phase: Saturation
% 2.25/1.01 % (2530962)Time elapsed: 0.034 s
% 2.25/1.01 % (2530962)Peak memory usage: 13 MB
% 2.25/1.01 % (2530962)Instructions burned: 119 (million)
% 2.25/1.01 % (2530972)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2807173690:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.25/1.01 % (2530961)Instruction limit reached!
% 2.25/1.01 % (2530961)------------------------------
% 2.25/1.01 % (2530961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/1.01 % (2530961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/1.01 % (2530961)CaDiCaL version: 2.1.3
% 2.25/1.01 % (2530961)Termination reason: Instruction limit
% 2.25/1.01 % (2530961)Termination phase: Saturation
% 2.25/1.01 % (2530961)Time elapsed: 0.061 s
% 2.25/1.01 % (2530961)Peak memory usage: 13 MB
% 2.25/1.01 % (2530961)Instructions burned: 103 (million)
% 2.25/1.01 % (2530963)Instruction limit reached!
% 2.25/1.01 % (2530963)------------------------------
% 2.25/1.01 % (2530963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/1.01 % (2530963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/1.01 % (2530963)CaDiCaL version: 2.1.3
% 2.25/1.01 % (2530963)Termination reason: Instruction limit
% 2.25/1.01 % (2530963)Termination phase: Saturation
% 2.25/1.01 % (2530963)Time elapsed: 0.078 s
% 2.25/1.01 % (2530963)Peak memory usage: 14 MB
% 2.25/1.01 % (2530963)Instructions burned: 131 (million)
% 2.25/1.01 % (2530974)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1571336997:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 2.25/1.01 % (2530975)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2280835367:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.25/1.01 % (2530964)Instruction limit reached!
% 2.25/1.01 % (2530964)------------------------------
% 2.25/1.01 % (2530964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/1.01 % (2530964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/1.01 % (2530964)CaDiCaL version: 2.1.3
% 2.25/1.01 % (2530964)Termination reason: Instruction limit
% 2.25/1.01 % (2530964)Termination phase: Saturation
% 2.25/1.01 % (2530964)Time elapsed: 0.100 s
% 2.25/1.01 % (2530964)Peak memory usage: 15 MB
% 2.25/1.01 % (2530964)Instructions burned: 160 (million)
% 2.25/1.01 % (2530978)ott-21_1_sil=16000:fs=off:random_seed=824131441:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.25/1.01 % TRYING [1]
% 2.25/1.01 % TRYING [2]
% 2.25/1.01 % (2530974)Instruction limit reached!
% 2.25/1.01 % (2530974)------------------------------
% 2.25/1.01 % (2530974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/1.01 % (2530974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/1.01 % (2530974)CaDiCaL version: 2.1.3
% 2.25/1.01 % (2530974)Termination reason: Instruction limit
% 2.25/1.01 % (2530974)Termination phase: Saturation
% 2.25/1.01 % (2530974)Time elapsed: 0.070 s
% 2.25/1.01 % (2530974)Peak memory usage: 13 MB
% 2.25/1.01 % (2530974)Instructions burned: 132 (million)
% 2.25/1.01 % (2530980)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1647530907:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 2.25/1.01 % TRYING [1]
% 2.25/1.01 % TRYING [2]
% 2.25/1.01 % (2530972)Instruction limit reached!
% 2.25/1.01 % (2530972)------------------------------
% 2.25/1.01 % (2530972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/1.01 % (2530972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/1.01 % (2530972)CaDiCaL version: 2.1.3
% 2.25/1.01 % (2530972)Termination reason: Instruction limit
% 2.25/1.01 % (2530972)Termination phase: Finite model building constraint generation
% 2.25/1.01 % (2530972)Time elapsed: 0.175 s
% 2.25/1.01 % (2530972)Peak memory usage: 38 MB
% 2.25/1.01 % (2530972)Instructions burned: 714 (million)
% 2.25/1.01 % (2530978)Instruction limit reached!
% 2.25/1.01 % (2530978)------------------------------
% 2.25/1.01 % (2530978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/1.01 % (2530978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/1.01 % (2530978)CaDiCaL version: 2.1.3
% 2.25/1.01 % (2530978)Termination reason: Instruction limit
% 2.25/1.01 % (2530978)Termination phase: Saturation
% 2.25/1.01 % (2530978)Time elapsed: 0.095 s
% 2.25/1.01 % (2530978)Peak memory usage: 13 MB
% 2.25/1.01 % (2530978)Instructions burned: 181 (million)
% 2.25/1.01 % (2530983)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=943320599:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 2.25/1.01 % (2530982)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=933402546:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.25/1.01 % TRYING [3]
% 2.25/1.01 % TRYING [1]
% 2.25/1.01 % TRYING [2]
% 2.25/1.01 % (2530980)Instruction limit reached!
% 2.25/1.01 % (2530980)------------------------------
% 2.25/1.01 % (2530980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/1.01 % (2530980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/1.01 % (2530980)CaDiCaL version: 2.1.3
% 2.25/1.01 % (2530980)Termination reason: Instruction limit
% 2.25/1.01 % (2530980)Termination phase: Saturation
% 2.25/1.01 % (2530980)Time elapsed: 0.313 s
% 2.25/1.01 % (2530980)Peak memory usage: 15 MB
% 2.25/1.01 % (2530980)Instructions burned: 477 (million)
% 2.25/1.01 % (2530986)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2839964983:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 2.25/1.01 % (2530975) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2530953-2530975"...
% 2.25/1.01 % (2530975)...printing done.
% 2.25/1.01 % (2530975)Refutation found. Thanks to Tanya!
% 2.25/1.01 % SZS status Theorem for theBenchmark
% 2.25/1.01 % SZS output start Proof for theBenchmark
% See solution above
% 2.25/1.02 % (2530975)------------------------------
% 2.25/1.02 % (2530975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/1.02 % (2530975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/1.02 % (2530975)CaDiCaL version: 2.1.3
% 2.25/1.02 % (2530975)Termination reason: Refutation
% 2.25/1.02 % (2530975)Time elapsed: 0.423 s
% 2.25/1.02 % (2530975)Peak memory usage: 17 MB
% 2.25/1.02 % (2530975)Instructions burned: 659 (million)
% 2.25/1.02 % (2530953)Success in time 0.588 s
% 2.25/1.02 % Vampire exiting
%------------------------------------------------------------------------------