%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT062-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:36:50 PM UTC 2026
% Result : Unsatisfiable 8.35s 2.22s
% Output : Refutation 9.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 21
% Syntax : Number of formulae : 177 ( 32 unt; 10 def)
% Number of atoms : 944 ( 295 equ)
% Maximal formula atoms : 10 ( 5 avg)
% Number of connectives : 1131 ( 364 ~; 765 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 8 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 3 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 17 con; 0-6 aty)
% Number of variables : 298 ( 0 sgn 298 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f542,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X4 = X0
| X3 = X1
| X0 = X1
| X3 = X4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_2_0) ).
fof(f543,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(reorient_equations,[],[f542]) ).
fof(f545,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X4 = X0
| X3 = X1
| X0 = X1
| X3 = X4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_2_2) ).
fof(f546,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(reorient_equations,[],[f545]) ).
fof(f747,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(c_Fun_Ocomp(X0,X1,X2,X3,X4),X5) = hAPP(X0,hAPP(X1,X5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_o__apply_0) ).
fof(f751,axiom,
c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f754,axiom,
v_b____ != v_c____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_03) ).
fof(f755,axiom,
v_a____ != v_b____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_04) ).
fof(f756,axiom,
c_in(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_05) ).
fof(f757,axiom,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_1) ).
fof(f758,axiom,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_06) ).
fof(f759,negated_conjecture,
( ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f760,negated_conjecture,
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f846,definition,
sF0 = c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f847,plain,
c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(reorient_equations,[],[f846]) ).
fof(f848,definition,
sF1 = v_F(v_P_H____),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f849,plain,
v_F(v_P_H____) = sF1,
inference(reorient_equations,[],[f848]) ).
fof(f850,definition,
sF2 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f851,plain,
tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF2,
inference(reorient_equations,[],[f850]) ).
fof(f852,definition,
sF3 = c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f853,plain,
c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF3,
inference(reorient_equations,[],[f852]) ).
fof(f854,definition,
sF4 = c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f855,plain,
c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF4,
inference(reorient_equations,[],[f854]) ).
fof(f856,definition,
sF5 = tc_fun(sF2,tc_bool),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f857,plain,
tc_fun(sF2,tc_bool) = sF5,
inference(reorient_equations,[],[f856]) ).
fof(f858,definition,
sF6 = c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f859,plain,
c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi) = sF6,
inference(reorient_equations,[],[f858]) ).
fof(f860,definition,
sF7 = v_F(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f861,plain,
v_F(sF6) = sF7,
inference(reorient_equations,[],[f860]) ).
fof(f862,plain,
( ~ c_in(sF0,sF1,sF2)
| ~ c_in(sF3,sF7,sF2) ),
inference(definition_folding,[],[f759,f851,f861,f859,f857,f851,f857,f851,f855,f853,f851,f849,f847]) ).
fof(f863,plain,
( c_in(sF3,sF7,sF2)
| c_in(sF0,sF1,sF2) ),
inference(definition_folding,[],[f760,f851,f849,f847,f851,f861,f859,f857,f851,f857,f851,f855,f853]) ).
fof(f867,definition,
( spl8_1
<=> c_in(sF0,sF1,sF2) ),
introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition]) ).
fof(f868,plain,
( ~ c_in(sF0,sF1,sF2)
| spl8_1 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f869,plain,
( c_in(sF0,sF1,sF2)
| ~ spl8_1 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f871,definition,
( spl8_2
<=> c_in(sF3,sF7,sF2) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
fof(f872,plain,
( ~ c_in(sF3,sF7,sF2)
| spl8_2 ),
inference(avatar_component_clause,[],[f871]) ).
fof(f873,plain,
( c_in(sF3,sF7,sF2)
| ~ spl8_2 ),
inference(avatar_component_clause,[],[f871]) ).
fof(f874,plain,
( spl8_1
| spl8_2 ),
inference(avatar_split_clause,[],[f863,f871,f867]) ).
fof(f875,plain,
( ~ spl8_2
| ~ spl8_1 ),
inference(avatar_split_clause,[],[f862,f867,f871]) ).
fof(f937,plain,
c_in(c_Fun_Ocomp(sF4,v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
inference(superposition,[],[f756,f855]) ).
fof(f938,plain,
c_in(c_Fun_Ocomp(sF4,v_P____,tc_fun(sF2,tc_bool),tc_fun(sF2,tc_bool),tc_Arrow__Order__Mirabelle_Oindi),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool))),
inference(forward_demodulation,[],[f937,f851]) ).
fof(f939,plain,
c_in(c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5)),
inference(forward_demodulation,[],[f938,f857]) ).
fof(f940,plain,
c_in(sF6,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5)),
inference(forward_demodulation,[],[f939,f859]) ).
fof(f981,plain,
! [X0] : hAPP(sF4,hAPP(v_P____,X0)) = hAPP(sF6,X0),
inference(superposition,[],[f747,f859]) ).
fof(f983,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(superposition,[],[f757,f747]) ).
fof(f984,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0)),sF2)
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f983,f851]) ).
fof(f986,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF4,hAPP(v_P____,X0)),sF2)
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f984,f855]) ).
fof(f988,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF6,X0),sF2)
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f986,f981]) ).
fof(f990,plain,
! [X0] :
( c_in(sF3,hAPP(sF6,X0),sF2)
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f988,f853]) ).
fof(f992,plain,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2)
| c_in(sF3,hAPP(sF6,X0),sF2) ),
inference(forward_demodulation,[],[f990,f851]) ).
fof(f994,plain,
! [X0] :
( ~ c_in(sF0,hAPP(v_P_H____,X0),sF2)
| c_in(sF3,hAPP(sF6,X0),sF2) ),
inference(forward_demodulation,[],[f992,f847]) ).
fof(f998,plain,
c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool))),
inference(superposition,[],[f751,f851]) ).
fof(f999,plain,
c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5)),
inference(forward_demodulation,[],[f998,f857]) ).
fof(f1255,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| v_a____ = v_b____
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(resolution,[],[f546,f757]) ).
fof(f1257,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3
| v_b____ = v_c____ ),
inference(superposition,[],[f546,f847]) ).
fof(f1262,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f1257,f754]) ).
fof(f1264,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| v_a____ = v_b____
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_subsumption_resolution,[],[f1255,f756]) ).
fof(f1267,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1262,f851]) ).
fof(f1269,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_subsumption_resolution,[],[f1264,f755]) ).
fof(f1271,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1267,f851]) ).
fof(f1273,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(sF2,tc_bool),tc_fun(sF2,tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1269,f851]) ).
fof(f1275,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1271,f851]) ).
fof(f1277,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi)),sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1273,f857]) ).
fof(f1279,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF2)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1275,f851]) ).
fof(f1281,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi)),sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1277,f855]) ).
fof(f1283,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF2)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1279,f851]) ).
fof(f1285,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(sF6),sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1281,f859]) ).
fof(f1287,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF2)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1283,f857]) ).
fof(f1289,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF7,sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1285,f861]) ).
fof(f1291,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF2)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1287,f851]) ).
fof(f1293,plain,
! [X2,X0,X1] :
( ~ c_in(sF3,sF7,sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1289,f853]) ).
fof(f1294,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF2)
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1291,f857]) ).
fof(f1296,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1293,f873]) ).
fof(f1297,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(sF2,tc_bool),tc_fun(sF2,tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),sF2)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1296,f851]) ).
fof(f1298,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),sF2)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1297,f857]) ).
fof(f1299,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),sF2)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1298,f855]) ).
fof(f1300,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(sF6,X2,v_b____,X0,v_a____,X1)),sF2)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1299,f859]) ).
fof(f1301,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(sF6,X2,v_b____,X0,v_a____,X1)),sF2)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1300,f851]) ).
fof(f1302,plain,
( ! [X2,X0,X1] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(sF6,X2,v_b____,X0,v_a____,X1)),sF2)
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1301,f851]) ).
fof(f1303,plain,
( ! [X2,X0,X1] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(sF6,X2,v_b____,X0,v_a____,X1)),sF2)
| v_a____ = X0
| v_b____ = X1
| X0 = X1
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1302,f857]) ).
fof(f1304,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(sF2,tc_bool),tc_fun(sF2,tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),sF2)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(sF6,X2,v_b____,X0,v_a____,X1)),sF2)
| v_a____ = X0
| v_b____ = X1
| X0 = X1 )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1303,f851]) ).
fof(f1305,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),sF2)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(sF6,X2,v_b____,X0,v_a____,X1)),sF2)
| v_a____ = X0
| v_b____ = X1
| X0 = X1 )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1304,f857]) ).
fof(f1306,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X2,v_b____,X0,v_a____,X1)),sF2)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(sF6,X2,v_b____,X0,v_a____,X1)),sF2)
| v_a____ = X0
| v_b____ = X1
| X0 = X1 )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1305,f855]) ).
fof(f1307,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(sF6,X2,v_b____,X0,v_a____,X1)),sF2)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(sF6,X2,v_b____,X0,v_a____,X1)),sF2)
| v_a____ = X0
| v_b____ = X1
| X0 = X1 )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1306,f859]) ).
fof(f1308,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(sF6,X2,v_b____,X0,v_a____,X1)),sF2)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,X2,v_b____,X0,v_a____,X1)),sF2)
| v_a____ = X0
| v_b____ = X1
| X0 = X1 )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1307,f847]) ).
fof(f1311,plain,
( ! [X0] :
( ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| v_a____ = v_b____
| v_b____ = v_c____
| v_b____ = v_c____ )
| ~ spl8_2 ),
inference(superposition,[],[f1308,f847]) ).
fof(f1313,plain,
( ! [X0] :
( ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| v_a____ = v_b____
| v_b____ = v_c____ )
| ~ spl8_2 ),
inference(duplicate_literal_removal,[],[f1311]) ).
fof(f1316,plain,
( ! [X0] :
( ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| v_b____ = v_c____ )
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1313,f755]) ).
fof(f1318,plain,
( ! [X0] :
( ~ c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2) )
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1316,f754]) ).
fof(f1320,plain,
! [X0,X1] :
( ~ c_in(sF3,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF3,v_F(X0),sF2)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF2)
| v_b____ = v_c____
| v_a____ = v_b____
| v_a____ = v_b____ ),
inference(superposition,[],[f1294,f853]) ).
fof(f1324,plain,
! [X0,X1] :
( ~ c_in(sF3,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF3,v_F(X0),sF2)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF2)
| v_b____ = v_c____
| v_a____ = v_b____ ),
inference(duplicate_literal_removal,[],[f1320]) ).
fof(f1326,plain,
! [X0,X1] :
( ~ c_in(sF3,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF3,v_F(X0),sF2)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF2)
| v_a____ = v_b____ ),
inference(forward_subsumption_resolution,[],[f1324,f754]) ).
fof(f1327,plain,
! [X0,X1] :
( ~ c_in(sF3,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF3,v_F(X0),sF2)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF2) ),
inference(forward_subsumption_resolution,[],[f1326,f755]) ).
fof(f1429,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| v_a____ = v_b____
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(resolution,[],[f543,f758]) ).
fof(f1433,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| v_a____ = v_b____
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(resolution,[],[f543,f758]) ).
fof(f1458,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| v_a____ = v_b____
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_subsumption_resolution,[],[f1433,f756]) ).
fof(f1461,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| v_a____ = v_b____
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_subsumption_resolution,[],[f1429,f756]) ).
fof(f1472,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_subsumption_resolution,[],[f1458,f755]) ).
fof(f1475,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_subsumption_resolution,[],[f1461,f755]) ).
fof(f1484,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(sF2,tc_bool),tc_fun(sF2,tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1472,f851]) ).
fof(f1487,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(sF2,tc_bool),tc_fun(sF2,tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1475,f851]) ).
fof(f1496,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1484,f857]) ).
fof(f1499,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1487,f857]) ).
fof(f1508,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1496,f855]) ).
fof(f1511,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1499,f855]) ).
fof(f1519,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1508,f859]) ).
fof(f1522,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1511,f859]) ).
fof(f1530,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1519,f851]) ).
fof(f1532,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(sF2,tc_bool),tc_fun(sF2,tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1522,f851]) ).
fof(f1540,plain,
! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(sF2,tc_bool),tc_fun(sF2,tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),sF2)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1530,f851]) ).
fof(f1542,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi)),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1532,f857]) ).
fof(f1548,plain,
! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi)),sF2)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1540,f857]) ).
fof(f1550,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi)),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1542,f855]) ).
fof(f1552,plain,
! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi)),sF2)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1548,f855]) ).
fof(f1554,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(sF6),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1550,f859]) ).
fof(f1556,plain,
! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(sF6),sF2)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1552,f859]) ).
fof(f1557,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF7,sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1554,f861]) ).
fof(f1558,plain,
! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF7,sF2)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1556,f861]) ).
fof(f1559,plain,
! [X2,X0,X1] :
( ~ c_in(sF3,sF7,sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1557,f853]) ).
fof(f1560,plain,
! [X2,X0,X1] :
( c_in(sF3,sF7,sF2)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1558,f853]) ).
fof(f1561,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1559,f873]) ).
fof(f1562,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1561,f851]) ).
fof(f1563,plain,
( ! [X2,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1562,f851]) ).
fof(f1564,plain,
( ! [X2,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| v_a____ = X1
| v_b____ = X2
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1563,f857]) ).
fof(f1565,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(sF2,tc_bool),tc_fun(sF2,tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| v_a____ = X1
| v_b____ = X2
| X1 = X2 )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1564,f851]) ).
fof(f1566,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| v_a____ = X1
| v_b____ = X2
| X1 = X2 )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1565,f857]) ).
fof(f1567,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X0,v_b____,X1,v_a____,X2)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| v_a____ = X1
| v_b____ = X2
| X1 = X2 )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1566,f855]) ).
fof(f1568,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| v_a____ = X1
| v_b____ = X2
| X1 = X2 )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1567,f859]) ).
fof(f1569,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,X0,v_b____,X1,v_a____,X2)),sF2)
| v_a____ = X1
| v_b____ = X2
| X1 = X2 )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1568,f847]) ).
fof(f1588,plain,
( ! [X0] :
( c_in(sF0,hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| v_a____ = v_b____
| v_b____ = v_c____
| v_b____ = v_c____ )
| ~ spl8_2 ),
inference(superposition,[],[f1569,f847]) ).
fof(f1590,plain,
( ! [X0] :
( c_in(sF0,hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| v_a____ = v_b____
| v_b____ = v_c____ )
| ~ spl8_2 ),
inference(duplicate_literal_removal,[],[f1588]) ).
fof(f1597,plain,
( ! [X0] :
( c_in(sF0,hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| v_b____ = v_c____ )
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1590,f755]) ).
fof(f1599,plain,
( ! [X0] :
( c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| c_in(sF0,hAPP(X0,v_sko__local__X2__1(sF6,X0,v_b____,v_b____,v_a____,v_c____)),sF2)
| c_in(sF0,v_F(X0),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5)) )
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1597,f754]) ).
fof(f1608,plain,
( c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,v_P_H____,v_b____,v_b____,v_a____,v_c____)),sF2)
| c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ spl8_2 ),
inference(factoring,[],[f1599]) ).
fof(f1611,plain,
( c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,v_P_H____,v_b____,v_b____,v_a____,v_c____)),sF2)
| c_in(sF0,v_F(v_P_H____),sF2)
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1608,f999]) ).
fof(f1612,plain,
( c_in(sF0,sF1,sF2)
| c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,v_P_H____,v_b____,v_b____,v_a____,v_c____)),sF2)
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1611,f849]) ).
fof(f1613,plain,
( c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,v_P_H____,v_b____,v_b____,v_a____,v_c____)),sF2)
| spl8_1
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1612,f868]) ).
fof(f1614,plain,
( ~ c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,v_P_H____,v_b____,v_b____,v_a____,v_c____)),sF2)
| spl8_1
| ~ spl8_2 ),
inference(resolution,[],[f1613,f1318]) ).
fof(f1616,plain,
( c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(sF6,v_P_H____,v_b____,v_b____,v_a____,v_c____)),sF2)
| spl8_1
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1614,f999]) ).
fof(f1617,plain,
( c_in(sF0,v_F(v_P_H____),sF2)
| spl8_1
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1616,f1613]) ).
fof(f1618,plain,
( c_in(sF0,sF1,sF2)
| spl8_1
| ~ spl8_2 ),
inference(forward_demodulation,[],[f1617,f849]) ).
fof(f1619,plain,
( $false
| spl8_1
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1618,f868]) ).
fof(f1620,plain,
( spl8_1
| ~ spl8_2 ),
inference(avatar_contradiction_clause,[],[f1619]) ).
fof(f1621,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f1560,f872]) ).
fof(f1623,plain,
( ! [X2,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| spl8_2 ),
inference(forward_demodulation,[],[f1621,f851]) ).
fof(f1625,plain,
( ! [X2,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| v_b____ = X2
| v_a____ = X1
| X1 = X2
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| spl8_2 ),
inference(forward_demodulation,[],[f1623,f857]) ).
fof(f1627,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(sF2,tc_bool),tc_fun(sF2,tc_bool),tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| v_b____ = X2
| v_a____ = X1
| X1 = X2 )
| spl8_2 ),
inference(forward_demodulation,[],[f1625,f851]) ).
fof(f1629,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| v_b____ = X2
| v_a____ = X1
| X1 = X2 )
| spl8_2 ),
inference(forward_demodulation,[],[f1627,f857]) ).
fof(f1631,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,c_Fun_Ocomp(sF4,v_P____,sF5,sF5,tc_Arrow__Order__Mirabelle_Oindi),X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| v_b____ = X2
| v_a____ = X1
| X1 = X2 )
| spl8_2 ),
inference(forward_demodulation,[],[f1629,f855]) ).
fof(f1632,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| v_b____ = X2
| v_a____ = X1
| X1 = X2 )
| spl8_2 ),
inference(forward_demodulation,[],[f1631,f859]) ).
fof(f1633,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(X0,sF6,X1,v_b____,X2,v_a____)),sF2)
| v_b____ = X2
| v_a____ = X1
| X1 = X2 )
| spl8_2 ),
inference(forward_demodulation,[],[f1632,f847]) ).
fof(f1650,plain,
( ! [X0] :
( c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(X0,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| v_b____ = v_c____
| v_a____ = v_b____
| v_b____ = v_c____ )
| spl8_2 ),
inference(superposition,[],[f1633,f847]) ).
fof(f1652,plain,
( ! [X0] :
( c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(X0,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| v_b____ = v_c____
| v_a____ = v_b____ )
| spl8_2 ),
inference(duplicate_literal_removal,[],[f1650]) ).
fof(f1657,plain,
( ! [X0] :
( c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(X0,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| v_a____ = v_b____ )
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f1652,f754]) ).
fof(f1659,plain,
( ! [X0] :
( c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(X0,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| c_in(sF0,hAPP(X0,v_sko__local__X2__1(X0,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5)) )
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f1657,f755]) ).
fof(f1661,plain,
( c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(v_P_H____,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| spl8_2 ),
inference(factoring,[],[f1659]) ).
fof(f1663,plain,
( c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(v_P_H____,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f1661,f999]) ).
fof(f1664,plain,
( ~ c_in(sF0,sF1,sF2)
| c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(v_P_H____,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| spl8_2 ),
inference(forward_demodulation,[],[f1663,f849]) ).
fof(f1665,plain,
( c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(v_P_H____,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f1664,f869]) ).
fof(f1666,plain,
( c_in(sF3,hAPP(sF6,v_sko__local__X2__1(v_P_H____,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ spl8_1
| spl8_2 ),
inference(resolution,[],[f1665,f994]) ).
fof(f1668,plain,
( ~ c_in(sF6,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| c_in(sF3,v_F(sF6),sF2)
| ~ c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(v_P_H____,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ spl8_1
| spl8_2 ),
inference(resolution,[],[f1666,f1327]) ).
fof(f1671,plain,
( c_in(sF3,v_F(sF6),sF2)
| ~ c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF5))
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(v_P_H____,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f1668,f940]) ).
fof(f1673,plain,
( c_in(sF3,v_F(sF6),sF2)
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__local__X2__1(v_P_H____,sF6,v_b____,v_b____,v_c____,v_a____)),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f1671,f999]) ).
fof(f1675,plain,
( c_in(sF3,v_F(sF6),sF2)
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f1673,f1665]) ).
fof(f1677,plain,
( c_in(sF3,sF7,sF2)
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_demodulation,[],[f1675,f861]) ).
fof(f1678,plain,
( ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f1677,f872]) ).
fof(f1679,plain,
( ~ c_in(sF0,sF1,sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_demodulation,[],[f1678,f849]) ).
fof(f1680,plain,
( $false
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f1679,f869]) ).
fof(f1681,plain,
( ~ spl8_1
| spl8_2 ),
inference(avatar_contradiction_clause,[],[f1680]) ).
cnf(s1,plain,
( spl8_1
| spl8_2 ),
inference(sat_conversion,[],[f874]) ).
cnf(s2,plain,
( ~ spl8_1
| ~ spl8_2 ),
inference(sat_conversion,[],[f875]) ).
cnf(s7,plain,
( spl8_1
| ~ spl8_2 ),
inference(sat_conversion,[],[f1620]) ).
cnf(s8,plain,
( ~ spl8_1
| spl8_2 ),
inference(sat_conversion,[],[f1681]) ).
cnf(s9,plain,
spl8_1,
inference(rat,[],[s1,s7]) ).
cnf(s10,plain,
spl8_2,
inference(rat,[],[s8,s9]) ).
cnf(s11,plain,
$false,
inference(rat,[],[s2,s10,s9]) ).
fof(f1682,plain,
$false,
inference(avatar_sat_refutation,[],[s11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT062-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.39 % Computer : n019.cluster.edu
% 0.09/0.39 % Model : x86_64 x86_64
% 0.09/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.39 % Memory : 8046.5625MB
% 0.09/0.39 % OS : Linux 6.8.0-71-generic
% 0.09/0.39 % CPULimit : 300
% 0.09/0.39 % WCLimit : 300
% 0.09/0.39 % DateTime : Sun Sep 27 23:36:04 UTC 2026
% 0.09/0.39 % CPUTime :
% 0.09/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.42 Running first-order theorem proving
% 0.09/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.35/2.22 % (3531782)Input is clausal, will run a generic CNF schedule.
% 8.35/2.22 % (3531790)lrs+10_1_sil=8000:sp=occurrence:random_seed=2213322165:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.35/2.22 % (3531787)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4048365896:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.35/2.22 % (3531788)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4294524760:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.35/2.22 % (3531790)Instruction limit reached!
% 8.35/2.22 % (3531790)------------------------------
% 8.35/2.22 % (3531790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531790)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531790)Termination reason: Instruction limit
% 8.35/2.22 % (3531790)Termination phase: Saturation
% 8.35/2.22 % (3531790)Time elapsed: 0.038 s
% 8.35/2.22 % (3531790)Peak memory usage: 89 MB
% 8.35/2.22 % (3531790)Instructions burned: 110 (million)
% 8.35/2.22 % (3531789)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=473433541:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.35/2.22 % (3531792)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1239721135:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.35/2.22 % (3531791)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=485976967:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.35/2.22 % (3531793)dis-21_1_sil=8000:lcm=predicate:random_seed=2595560847:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 8.35/2.22 % (3531793)Instruction limit reached!
% 8.35/2.22 % (3531793)------------------------------
% 8.35/2.22 % (3531793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531793)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531793)Termination reason: Instruction limit
% 8.35/2.22 % (3531793)Termination phase: Saturation
% 8.35/2.22 % (3531793)Time elapsed: 0.066 s
% 8.35/2.22 % (3531793)Peak memory usage: 89 MB
% 8.35/2.22 % (3531793)Instructions burned: 118 (million)
% 8.35/2.22 % (3531798)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=4253996686:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 8.35/2.22 % (3531791)Instruction limit reached!
% 8.35/2.22 % (3531791)------------------------------
% 8.35/2.22 % (3531791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531791)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531791)Termination reason: Instruction limit
% 8.35/2.22 % (3531791)Termination phase: Saturation
% 8.35/2.22 % (3531791)Time elapsed: 0.076 s
% 8.35/2.22 % (3531791)Peak memory usage: 89 MB
% 8.35/2.22 % (3531791)Instructions burned: 114 (million)
% 8.35/2.22 % (3531798)Refutation not found, incomplete strategy
% 8.35/2.22 % (3531798)------------------------------
% 8.35/2.22 % (3531798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531798)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531798)Termination reason: Refutation not found, incomplete strategy
% 8.35/2.22 % (3531798)Time elapsed: 0.004 s
% 8.35/2.22 % (3531798)Peak memory usage: 89 MB
% 8.35/2.22 % (3531798)Instructions burned: 12 (million)
% 8.35/2.22 % (3531792)Instruction limit reached!
% 8.35/2.22 % (3531792)------------------------------
% 8.35/2.22 % (3531792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531792)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531792)Termination reason: Instruction limit
% 8.35/2.22 % (3531792)Termination phase: Saturation
% 8.35/2.22 % (3531792)Time elapsed: 0.119 s
% 8.35/2.22 % (3531792)Peak memory usage: 90 MB
% 8.35/2.22 % (3531792)Instructions burned: 181 (million)
% 8.35/2.22 % (3531802)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1561816865:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 8.35/2.22 % (3531804)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=485759545:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 8.35/2.22 % (3531798)------------------------------
% 8.35/2.22 % (3531798)------------------------------
% 8.35/2.22 % (3531805)lrs+10_64_to=lpo:sil=8000:random_seed=1109418181:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 8.35/2.22 % (3531805)Instruction limit reached!
% 8.35/2.22 % (3531805)------------------------------
% 8.35/2.22 % (3531805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531805)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531805)Termination reason: Instruction limit
% 8.35/2.22 % (3531805)Termination phase: Saturation
% 8.35/2.22 % (3531805)Time elapsed: 0.042 s
% 8.35/2.22 % (3531805)Peak memory usage: 90 MB
% 8.35/2.22 % (3531805)Instructions burned: 126 (million)
% 8.35/2.22 % (3531802)Instruction limit reached!
% 8.35/2.22 % (3531802)------------------------------
% 8.35/2.22 % (3531802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531802)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531802)Termination reason: Instruction limit
% 8.35/2.22 % (3531802)Termination phase: Saturation
% 8.35/2.22 % (3531802)Time elapsed: 0.102 s
% 8.35/2.22 % (3531802)Peak memory usage: 91 MB
% 8.35/2.22 % (3531802)Instructions burned: 191 (million)
% 8.35/2.22 % (3531804)Instruction limit reached!
% 8.35/2.22 % (3531804)------------------------------
% 8.35/2.22 % (3531804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531804)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531804)Termination reason: Instruction limit
% 8.35/2.22 % (3531804)Termination phase: Saturation
% 8.35/2.22 % (3531804)Time elapsed: 0.123 s
% 8.35/2.22 % (3531804)Peak memory usage: 90 MB
% 8.35/2.22 % (3531804)Instructions burned: 219 (million)
% 8.35/2.22 % (3531808)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1728654927:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 8.35/2.22 % (3531810)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3683014318:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 8.35/2.22 % (3531811)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3632482396:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 8.35/2.22 % (3531812)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2776865157:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 8.35/2.22 % (3531808)Instruction limit reached!
% 8.35/2.22 % (3531808)------------------------------
% 8.35/2.22 % (3531808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531808)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531808)Termination reason: Instruction limit
% 8.35/2.22 % (3531808)Termination phase: Saturation
% 8.35/2.22 % (3531808)Time elapsed: 0.130 s
% 8.35/2.22 % (3531808)Peak memory usage: 91 MB
% 8.35/2.22 % (3531808)Instructions burned: 194 (million)
% 8.35/2.22 % (3531810)Instruction limit reached!
% 8.35/2.22 % (3531810)------------------------------
% 8.35/2.22 % (3531810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531810)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531810)Termination reason: Instruction limit
% 8.35/2.22 % (3531810)Termination phase: Saturation
% 8.35/2.22 % (3531810)Time elapsed: 0.101 s
% 8.35/2.22 % (3531810)Peak memory usage: 91 MB
% 8.35/2.22 % (3531810)Instructions burned: 157 (million)
% 8.35/2.22 % (3531812)Instruction limit reached!
% 8.35/2.22 % (3531812)------------------------------
% 8.35/2.22 % (3531812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531812)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531812)Termination reason: Instruction limit
% 8.35/2.22 % (3531812)Termination phase: Saturation
% 8.35/2.22 % (3531812)Time elapsed: 0.062 s
% 8.35/2.22 % (3531812)Peak memory usage: 90 MB
% 8.35/2.22 % (3531812)Instructions burned: 106 (million)
% 8.35/2.22 % (3531817)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1306263107:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 8.35/2.22 % (3531818)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3101473397:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 8.35/2.22 % (3531819)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3011076285:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 8.35/2.22 % (3531817)Instruction limit reached!
% 8.35/2.22 % (3531817)------------------------------
% 8.35/2.22 % (3531817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531817)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531817)Termination reason: Instruction limit
% 8.35/2.22 % (3531817)Termination phase: Saturation
% 8.35/2.22 % (3531817)Time elapsed: 0.065 s
% 8.35/2.22 % (3531817)Peak memory usage: 90 MB
% 8.35/2.22 % (3531817)Instructions burned: 107 (million)
% 8.35/2.22 % (3531818)Instruction limit reached!
% 8.35/2.22 % (3531818)------------------------------
% 8.35/2.22 % (3531818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531818)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531818)Termination reason: Instruction limit
% 8.35/2.22 % (3531818)Termination phase: Saturation
% 8.35/2.22 % (3531818)Time elapsed: 0.147 s
% 8.35/2.22 % (3531818)Peak memory usage: 90 MB
% 8.35/2.22 % (3531818)Instructions burned: 242 (million)
% 8.35/2.22 % (3531823)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2475816148:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 8.35/2.22 % (3531823)Instruction limit reached!
% 8.35/2.22 % (3531823)------------------------------
% 8.35/2.22 % (3531823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531823)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531823)Termination reason: Instruction limit
% 8.35/2.22 % (3531823)Termination phase: Saturation
% 8.35/2.22 % (3531823)Time elapsed: 0.072 s
% 8.35/2.22 % (3531823)Peak memory usage: 90 MB
% 8.35/2.22 % (3531823)Instructions burned: 134 (million)
% 8.35/2.22 % (3531787)First to succeed.
% 8.35/2.22 % (3531787)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3531782"
% 8.35/2.22 % (3531824)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=448346381:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 8.35/2.22 % (3531826)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3039271877:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 8.35/2.22 % (3531826)Instruction limit reached!
% 8.35/2.22 % (3531826)------------------------------
% 8.35/2.22 % (3531826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.22 % (3531826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.22 % (3531826)CaDiCaL version: 2.1.3
% 8.35/2.22 % (3531826)Termination reason: Instruction limit
% 8.35/2.22 % (3531826)Termination phase: Saturation
% 8.35/2.22 % (3531826)Time elapsed: 0.131 s
% 8.35/2.22 % (3531826)Peak memory usage: 91 MB
% 8.35/2.22 % (3531826)Instructions burned: 191 (million)
% 8.35/2.22 % (3531787)Refutation found. Thanks to Tanya!
% 8.35/2.22 % SZS status Unsatisfiable for theBenchmark
% 8.35/2.22 % SZS output start Proof for theBenchmark
% See solution above
% 9.92/2.32 % (3531787)------------------------------
% 9.92/2.32 % (3531787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.92/2.32 % (3531787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.92/2.32 % (3531787)CaDiCaL version: 2.1.3
% 9.92/2.32 % (3531787)Termination reason: Refutation
% 9.92/2.32 % (3531787)Time elapsed: 0.936 s
% 9.92/2.32 % (3531787)Peak memory usage: 139 MB
% 9.92/2.32 % (3531787)Instructions burned: 1478 (million)
% 9.92/2.32 % (3531787)------------------------------
% 9.92/2.32 % (3531787)------------------------------
% 9.92/2.32 % (3531782)Success in time 1.359 s
% 9.92/2.32 % Vampire exiting
%------------------------------------------------------------------------------