%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT049-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 : n016.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:49 PM UTC 2026
% Result : Unsatisfiable 5.60s 1.77s
% Output : Refutation 6.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 33
% Syntax : Number of formulae : 232 ( 67 unt; 17 def)
% Number of atoms : 951 ( 246 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 1149 ( 430 ~; 717 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 13 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-3 aty)
% Number of functors : 32 ( 32 usr; 24 con; 0-6 aty)
% Number of variables : 428 ( 0 sgn 428 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f768,axiom,
! [X2,X0,X1] :
( c_in(X0,X1,X2)
| ~ hBOOL(hAPP(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f769,axiom,
! [X2,X0,X1] :
( ~ c_in(X1,X0,X2)
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_0) ).
fof(f772,axiom,
v_b____ != v_c____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_2) ).
fof(f773,axiom,
v_a____ != v_c____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_1) ).
fof(f775,axiom,
c_in(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),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_01) ).
fof(f776,axiom,
c_in(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),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_02) ).
fof(f777,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(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),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__CHAINED__1(X2,X5,X0,X3,X1,X4)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ 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)))
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_3) ).
fof(f778,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__CHAINED__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__CHAINED__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_CHAINED_2_03) ).
fof(f779,plain,
! [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__CHAINED__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__CHAINED__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)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(reorient_equations,[],[f778]) ).
fof(f780,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(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),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__CHAINED__1(X2,X5,X0,X3,X1,X4)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ 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)))
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_1_04) ).
fof(f781,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__CHAINED__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__CHAINED__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_CHAINED_0_05) ).
fof(f782,plain,
! [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__CHAINED__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__CHAINED__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)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(reorient_equations,[],[f781]) ).
fof(f783,axiom,
! [X0] :
( c_in(c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),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(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_1_06) ).
fof(f784,axiom,
! [X0] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_07) ).
fof(f785,negated_conjecture,
( ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f786,negated_conjecture,
( c_in(c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),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(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f805,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(c_COMBC(X0,X1,X2,X3,X4),X5) = hAPP(hAPP(X0,X5),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ATP__Linkup_OCOMBC__def_0) ).
fof(f806,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(hAPP(c_COMBB(X0,X1,X2,X3),X4),X5) = hAPP(X0,hAPP(X4,X5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ATP__Linkup_OCOMBB__def_0) ).
fof(f893,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(f894,plain,
c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(reorient_equations,[],[f893]) ).
fof(f895,definition,
sF1 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f896,plain,
tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF1,
inference(reorient_equations,[],[f895]) ).
fof(f897,definition,
sF2 = tc_fun(sF1,tc_bool),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f898,plain,
tc_fun(sF1,tc_bool) = sF2,
inference(reorient_equations,[],[f897]) ).
fof(f899,definition,
sF3 = tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f900,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2) = sF3,
inference(reorient_equations,[],[f899]) ).
fof(f901,definition,
sF4 = tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f902,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3) = sF4,
inference(reorient_equations,[],[f901]) ).
fof(f903,definition,
sF5 = c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,sF4,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f904,plain,
c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,sF4,tc_Arrow__Order__Mirabelle_Oindi) = sF5,
inference(reorient_equations,[],[f903]) ).
fof(f905,definition,
sF6 = hAPP(sF5,v_P____),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f906,plain,
hAPP(sF5,v_P____) = sF6,
inference(reorient_equations,[],[f905]) ).
fof(f907,definition,
sF7 = c_COMBC(sF6,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f908,plain,
c_COMBC(sF6,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3) = sF7,
inference(reorient_equations,[],[f907]) ).
fof(f909,definition,
sF8 = c_COMBC(sF7,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f910,plain,
c_COMBC(sF7,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2) = sF8,
inference(reorient_equations,[],[f909]) ).
fof(f911,definition,
sF9 = hAPP(sF5,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f912,plain,
hAPP(sF5,sF8) = sF9,
inference(reorient_equations,[],[f911]) ).
fof(f913,definition,
sF10 = c_COMBC(sF9,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f914,plain,
c_COMBC(sF9,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3) = sF10,
inference(reorient_equations,[],[f913]) ).
fof(f915,definition,
sF11 = c_COMBC(sF10,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f916,plain,
c_COMBC(sF10,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2) = sF11,
inference(reorient_equations,[],[f915]) ).
fof(f917,definition,
sF12 = v_F(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f918,plain,
v_F(sF11) = sF12,
inference(reorient_equations,[],[f917]) ).
fof(f919,definition,
sF13 = c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f920,plain,
c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF13,
inference(reorient_equations,[],[f919]) ).
fof(f921,definition,
sF14 = v_F(sF8),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f922,plain,
v_F(sF8) = sF14,
inference(reorient_equations,[],[f921]) ).
fof(f923,plain,
( ~ c_in(sF0,sF12,sF1)
| ~ c_in(sF13,sF14,sF1) ),
inference(definition_folding,[],[f785,f896,f922,f910,f898,f896,f908,f900,f898,f896,f906,f904,f902,f900,f898,f896,f898,f896,f920,f896,f918,f916,f898,f896,f914,f900,f898,f896,f912,f910,f898,f896,f908,f900,f898,f896,f906,f904,f902,f900,f898,f896,f898,f896,f904,f902,f900,f898,f896,f898,f896,f894]) ).
fof(f924,plain,
( c_in(sF13,sF14,sF1)
| c_in(sF0,sF12,sF1) ),
inference(definition_folding,[],[f786,f896,f918,f916,f898,f896,f914,f900,f898,f896,f912,f910,f898,f896,f908,f900,f898,f896,f906,f904,f902,f900,f898,f896,f898,f896,f904,f902,f900,f898,f896,f898,f896,f894,f896,f922,f910,f898,f896,f908,f900,f898,f896,f906,f904,f902,f900,f898,f896,f898,f896,f920]) ).
fof(f939,definition,
( spl15_1
<=> c_in(sF0,sF12,sF1) ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
fof(f940,plain,
( ~ c_in(sF0,sF12,sF1)
| spl15_1 ),
inference(avatar_component_clause,[],[f939]) ).
fof(f941,plain,
( c_in(sF0,sF12,sF1)
| ~ spl15_1 ),
inference(avatar_component_clause,[],[f939]) ).
fof(f943,definition,
( spl15_2
<=> c_in(sF13,sF14,sF1) ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
fof(f944,plain,
( ~ c_in(sF13,sF14,sF1)
| spl15_2 ),
inference(avatar_component_clause,[],[f943]) ).
fof(f945,plain,
( c_in(sF13,sF14,sF1)
| ~ spl15_2 ),
inference(avatar_component_clause,[],[f943]) ).
fof(f946,plain,
( spl15_1
| spl15_2 ),
inference(avatar_split_clause,[],[f924,f943,f939]) ).
fof(f947,plain,
( ~ spl15_2
| ~ spl15_1 ),
inference(avatar_split_clause,[],[f923,f939,f943]) ).
fof(f1044,plain,
! [X0] :
( ~ c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(backward_demodulation,[],[f783,f894]) ).
fof(f1045,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(backward_demodulation,[],[f784,f894]) ).
fof(f1084,plain,
c_in(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(sF1,tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF1,tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(sF1,tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF1,tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF1,tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF1,tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF1,tc_bool))),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF1,tc_bool)),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool))),
inference(backward_demodulation,[],[f775,f896]) ).
fof(f1085,plain,
c_in(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(sF1,tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF1,tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF1,tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF1,tc_bool)),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool))),
inference(backward_demodulation,[],[f776,f896]) ).
fof(f1086,plain,
! [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),sF1)
| ~ 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(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),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__CHAINED__1(X2,X5,X0,X3,X1,X4)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ 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)))
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(backward_demodulation,[],[f777,f896]) ).
fof(f1087,plain,
! [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),sF1)
| ~ 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__CHAINED__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__CHAINED__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)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(backward_demodulation,[],[f779,f896]) ).
fof(f1088,plain,
! [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),sF1)
| ~ 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(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),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__CHAINED__1(X2,X5,X0,X3,X1,X4)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ 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)))
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(backward_demodulation,[],[f780,f896]) ).
fof(f1089,plain,
! [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),sF1)
| ~ 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__CHAINED__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__CHAINED__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)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(backward_demodulation,[],[f782,f896]) ).
fof(f1135,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),sF1)
| ~ c_in(c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1045,f896]) ).
fof(f1136,plain,
! [X0] :
( ~ c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),sF1)
| c_in(c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1044,f896]) ).
fof(f1144,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__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__CHAINED__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)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(forward_demodulation,[],[f1089,f896]) ).
fof(f1145,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),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__CHAINED__1(X2,X5,X0,X3,X1,X4)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ 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)))
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1088,f896]) ).
fof(f1146,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__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__CHAINED__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)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(forward_demodulation,[],[f1087,f896]) ).
fof(f1147,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),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__CHAINED__1(X2,X5,X0,X3,X1,X4)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ 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)))
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1086,f896]) ).
fof(f1148,plain,
c_in(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2)),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2)),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1085,f898]) ).
fof(f1149,plain,
c_in(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2)),tc_Arrow__Order__Mirabelle_Oindi),c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2)),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2)),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2)),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2)),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1084,f898]) ).
fof(f1204,plain,
! [X0] :
( ~ c_in(c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),sF1)
| c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),sF1) ),
inference(forward_demodulation,[],[f1135,f896]) ).
fof(f1205,plain,
! [X0] :
( c_in(c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),sF1)
| ~ c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),sF1) ),
inference(forward_demodulation,[],[f1136,f896]) ).
fof(f1213,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__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)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(forward_demodulation,[],[f1144,f896]) ).
fof(f1214,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__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ 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)))
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1145,f896]) ).
fof(f1215,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__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)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(forward_demodulation,[],[f1146,f896]) ).
fof(f1216,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__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ 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)))
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1147,f896]) ).
fof(f1217,plain,
c_in(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1148,f900]) ).
fof(f1218,plain,
c_in(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3),tc_Arrow__Order__Mirabelle_Oindi),c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3),tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2)),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1149,f900]) ).
fof(f1253,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),sF1)
| ~ c_in(sF13,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),sF1) ),
inference(forward_demodulation,[],[f1204,f920]) ).
fof(f1254,plain,
! [X0] :
( ~ c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),sF1)
| c_in(sF13,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),sF1) ),
inference(forward_demodulation,[],[f1205,f920]) ).
fof(f1260,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__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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(forward_demodulation,[],[f1213,f896]) ).
fof(f1261,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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)))
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1214,f896]) ).
fof(f1262,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__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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(forward_demodulation,[],[f1215,f896]) ).
fof(f1263,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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)))
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1216,f896]) ).
fof(f1264,plain,
c_in(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,sF4,tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1217,f902]) ).
fof(f1265,plain,
c_in(c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,sF4,tc_Arrow__Order__Mirabelle_Oindi),c_COMBC(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,sF4,tc_Arrow__Order__Mirabelle_Oindi),v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2)),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1218,f902]) ).
fof(f1293,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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(forward_demodulation,[],[f1260,f896]) ).
fof(f1294,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1261,f896]) ).
fof(f1295,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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(forward_demodulation,[],[f1262,f896]) ).
fof(f1296,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1263,f896]) ).
fof(f1297,plain,
c_in(c_COMBC(c_COMBC(hAPP(sF5,v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1264,f904]) ).
fof(f1298,plain,
c_in(c_COMBC(c_COMBC(hAPP(sF5,c_COMBC(c_COMBC(hAPP(sF5,v_P____),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2)),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1265,f904]) ).
fof(f1308,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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(forward_demodulation,[],[f1293,f898]) ).
fof(f1309,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(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__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1294,f898]) ).
fof(f1310,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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(forward_demodulation,[],[f1295,f898]) ).
fof(f1311,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(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__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ 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)))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1296,f898]) ).
fof(f1312,plain,
c_in(c_COMBC(c_COMBC(sF6,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1297,f906]) ).
fof(f1313,plain,
c_in(c_COMBC(c_COMBC(hAPP(sF5,c_COMBC(c_COMBC(sF6,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2)),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1298,f906]) ).
fof(f1317,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(forward_demodulation,[],[f1308,f896]) ).
fof(f1318,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(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__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1309,f896]) ).
fof(f1319,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(forward_demodulation,[],[f1310,f896]) ).
fof(f1320,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(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__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1311,f896]) ).
fof(f1321,plain,
c_in(c_COMBC(sF7,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1312,f908]) ).
fof(f1322,plain,
c_in(c_COMBC(c_COMBC(hAPP(sF5,c_COMBC(sF7,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2)),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1313,f908]) ).
fof(f1324,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__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(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__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(forward_demodulation,[],[f1317,f898]) ).
fof(f1325,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__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(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__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1318,f898]) ).
fof(f1326,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__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(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__CHAINED__1(X5,X2,X3,X0,X4,X1)),sF1)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(forward_demodulation,[],[f1319,f898]) ).
fof(f1327,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__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(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__CHAINED__1(X2,X5,X0,X3,X1,X4)),sF1)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1320,f898]) ).
fof(f1328,plain,
c_in(sF8,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1321,f910]) ).
fof(f1329,plain,
c_in(c_COMBC(c_COMBC(hAPP(sF5,sF8),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1322,f910]) ).
fof(f1331,plain,
c_in(c_COMBC(c_COMBC(sF9,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1329,f912]) ).
fof(f1333,plain,
c_in(c_COMBC(sF10,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1331,f914]) ).
fof(f1335,plain,
c_in(sF11,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1333,f916]) ).
fof(f1351,plain,
! [X2,X3,X0,X1] :
( c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X0),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| v_a____ = X3
| v_c____ = X2
| v_a____ = v_c____
| X2 = X3 ),
inference(superposition,[],[f1325,f920]) ).
fof(f1353,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__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X0),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f1351,f773]) ).
fof(f1356,plain,
! [X2,X3,X0,X1] :
( c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,X2,v_c____,X3)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X0,X1,v_b____,X2,v_c____,X3)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| v_c____ = X2
| v_b____ = X3
| X2 = X3
| v_b____ = v_c____ ),
inference(superposition,[],[f1324,f894]) ).
fof(f1360,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__CHAINED__1(X0,X1,v_b____,X2,v_c____,X3)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,X2,v_c____,X3)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f1356,f772]) ).
fof(f1361,plain,
! [X0] : hAPP(hAPP(sF6,X0),v_c____) = hAPP(sF7,X0),
inference(superposition,[],[f805,f908]) ).
fof(f1362,plain,
! [X0] : hAPP(hAPP(sF7,X0),v_b____) = hAPP(sF8,X0),
inference(superposition,[],[f805,f910]) ).
fof(f1363,plain,
! [X0] : hAPP(hAPP(sF9,X0),v_b____) = hAPP(sF10,X0),
inference(superposition,[],[f805,f914]) ).
fof(f1364,plain,
! [X0] : hAPP(hAPP(sF10,X0),v_a____) = hAPP(sF11,X0),
inference(superposition,[],[f805,f916]) ).
fof(f1382,plain,
! [X2,X3,X0,X1,X4] : hAPP(c_COMBC(hAPP(sF9,X0),X1,X2,X3,X4),v_b____) = hAPP(hAPP(sF10,X0),X1),
inference(superposition,[],[f805,f1363]) ).
fof(f1388,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,X2,v_c____,X3)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X0,X1,v_b____,X2,v_c____,X3)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| v_c____ = X2
| v_b____ = X3
| X2 = X3
| v_b____ = v_c____ ),
inference(superposition,[],[f1326,f894]) ).
fof(f1395,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__CHAINED__1(X0,X1,v_b____,X2,v_c____,X3)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,X2,v_c____,X3)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f1388,f772]) ).
fof(f1399,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X0),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| v_a____ = X3
| v_c____ = X2
| v_a____ = v_c____
| X2 = X3 ),
inference(superposition,[],[f1327,f920]) ).
fof(f1404,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__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X0),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f1399,f773]) ).
fof(f1409,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_a____,X1,X2,X3),v_b____),sF1)
| c_in(sF13,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),sF1) ),
inference(superposition,[],[f1254,f805]) ).
fof(f1414,plain,
! [X2,X3,X0,X1] :
( c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_a____,X1,X2,X3),v_b____),sF1)
| ~ c_in(sF13,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),sF1) ),
inference(superposition,[],[f1253,f805]) ).
fof(f1417,plain,
! [X0,X1] :
( c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF13,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X1),sF1)
| c_in(sF0,v_F(X0),sF1)
| v_a____ = v_c____
| v_b____ = v_c____
| v_b____ = v_c____ ),
inference(superposition,[],[f1353,f894]) ).
fof(f1422,plain,
! [X0,X1] :
( c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF13,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X1),sF1)
| c_in(sF0,v_F(X0),sF1)
| v_a____ = v_c____
| v_b____ = v_c____ ),
inference(duplicate_literal_removal,[],[f1417]) ).
fof(f1426,plain,
! [X0,X1] :
( c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF13,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X1),sF1)
| c_in(sF0,v_F(X0),sF1)
| v_b____ = v_c____ ),
inference(forward_subsumption_resolution,[],[f1422,f773]) ).
fof(f1427,plain,
! [X0,X1] :
( c_in(sF13,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X1),sF1)
| c_in(sF0,v_F(X0),sF1) ),
inference(forward_subsumption_resolution,[],[f1426,f772]) ).
fof(f1462,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X1),sF1)
| c_in(sF0,v_F(X0),sF1)
| v_a____ = v_c____
| v_b____ = v_c____
| v_b____ = v_c____ ),
inference(superposition,[],[f1404,f894]) ).
fof(f1467,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X1),sF1)
| c_in(sF0,v_F(X0),sF1)
| v_a____ = v_c____
| v_b____ = v_c____ ),
inference(duplicate_literal_removal,[],[f1462]) ).
fof(f1473,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X1),sF1)
| c_in(sF0,v_F(X0),sF1)
| v_b____ = v_c____ ),
inference(forward_subsumption_resolution,[],[f1467,f773]) ).
fof(f1474,plain,
! [X0,X1] :
( ~ c_in(sF13,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(X1),sF1)
| c_in(sF0,v_F(X0),sF1) ),
inference(forward_subsumption_resolution,[],[f1473,f772]) ).
fof(f1478,plain,
! [X0,X1] :
( ~ c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| c_in(sF13,v_F(X0),sF1)
| v_a____ = v_c____
| v_b____ = v_c____
| v_a____ = v_c____ ),
inference(superposition,[],[f1395,f920]) ).
fof(f1481,plain,
! [X0,X1] :
( ~ c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| c_in(sF13,v_F(X0),sF1)
| v_a____ = v_c____
| v_b____ = v_c____ ),
inference(duplicate_literal_removal,[],[f1478]) ).
fof(f1485,plain,
! [X0,X1] :
( ~ c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| c_in(sF13,v_F(X0),sF1)
| v_b____ = v_c____ ),
inference(forward_subsumption_resolution,[],[f1481,f773]) ).
fof(f1487,plain,
! [X0,X1] :
( ~ c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| c_in(sF13,v_F(X0),sF1) ),
inference(forward_subsumption_resolution,[],[f1485,f772]) ).
fof(f1523,plain,
! [X0,X1] :
( c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| c_in(sF13,v_F(X0),sF1)
| v_a____ = v_c____
| v_b____ = v_c____
| v_a____ = v_c____ ),
inference(superposition,[],[f1360,f920]) ).
fof(f1526,plain,
! [X0,X1] :
( c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| c_in(sF13,v_F(X0),sF1)
| v_a____ = v_c____
| v_b____ = v_c____ ),
inference(duplicate_literal_removal,[],[f1523]) ).
fof(f1532,plain,
! [X0,X1] :
( c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| c_in(sF13,v_F(X0),sF1)
| v_b____ = v_c____ ),
inference(forward_subsumption_resolution,[],[f1526,f773]) ).
fof(f1534,plain,
! [X0,X1] :
( c_in(sF13,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| c_in(sF13,v_F(X0),sF1) ),
inference(forward_subsumption_resolution,[],[f1532,f772]) ).
fof(f1546,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),sF0))
| c_in(sF13,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),sF1) ),
inference(resolution,[],[f768,f1254]) ).
fof(f1600,plain,
! [X0,X1] : hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(X0,X1)) = hAPP(hAPP(sF5,X0),X1),
inference(superposition,[],[f806,f904]) ).
fof(f1624,plain,
! [X0] : hAPP(sF9,X0) = hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(sF8,X0)),
inference(superposition,[],[f1600,f912]) ).
fof(f1625,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)) = hAPP(sF6,X0),
inference(superposition,[],[f1600,f906]) ).
fof(f1655,plain,
! [X2,X3,X0,X1] :
( c_in(sF13,hAPP(hAPP(hAPP(sF6,X0),v_c____),v_b____),sF1)
| ~ c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_a____,X1,X2,X3),v_b____),sF1) ),
inference(backward_demodulation,[],[f1409,f1625]) ).
fof(f1658,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF13,hAPP(hAPP(hAPP(sF6,X0),v_c____),v_b____),sF1)
| c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_a____,X1,X2,X3),v_b____),sF1) ),
inference(backward_demodulation,[],[f1414,f1625]) ).
fof(f1659,plain,
! [X0] :
( c_in(sF13,hAPP(hAPP(hAPP(sF6,X0),v_c____),v_b____),sF1)
| ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),sF0)) ),
inference(backward_demodulation,[],[f1546,f1625]) ).
fof(f1660,plain,
! [X0] :
( c_in(sF13,hAPP(hAPP(sF7,X0),v_b____),sF1)
| ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),sF0)) ),
inference(forward_demodulation,[],[f1659,f1361]) ).
fof(f1661,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF13,hAPP(hAPP(sF7,X0),v_b____),sF1)
| c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_a____,X1,X2,X3),v_b____),sF1) ),
inference(forward_demodulation,[],[f1658,f1361]) ).
fof(f1664,plain,
! [X2,X3,X0,X1] :
( c_in(sF13,hAPP(hAPP(sF7,X0),v_b____),sF1)
| ~ c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_a____,X1,X2,X3),v_b____),sF1) ),
inference(forward_demodulation,[],[f1655,f1361]) ).
fof(f1669,plain,
! [X0] :
( c_in(sF13,hAPP(sF8,X0),sF1)
| ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),sF0)) ),
inference(forward_demodulation,[],[f1660,f1362]) ).
fof(f1670,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF13,hAPP(sF8,X0),sF1)
| c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_a____,X1,X2,X3),v_b____),sF1) ),
inference(forward_demodulation,[],[f1661,f1362]) ).
fof(f1673,plain,
! [X2,X3,X0,X1] :
( c_in(sF13,hAPP(sF8,X0),sF1)
| ~ c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_a____,X1,X2,X3),v_b____),sF1) ),
inference(forward_demodulation,[],[f1664,f1362]) ).
fof(f1678,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(sF6,X0),v_c____),v_b____)),v_b____),v_a____),sF0))
| c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1669,f1625]) ).
fof(f1679,plain,
! [X2,X3,X0,X1] :
( c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(sF6,X0),v_c____),v_b____)),v_a____,X1,X2,X3),v_b____),sF1)
| ~ c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1670,f1625]) ).
fof(f1682,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(sF6,X0),v_c____),v_b____)),v_a____,X1,X2,X3),v_b____),sF1)
| c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1673,f1625]) ).
fof(f1687,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(sF7,X0),v_b____)),v_b____),v_a____),sF0))
| c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1678,f1361]) ).
fof(f1688,plain,
! [X2,X3,X0,X1] :
( c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(sF7,X0),v_b____)),v_a____,X1,X2,X3),v_b____),sF1)
| ~ c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1679,f1361]) ).
fof(f1691,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(sF7,X0),v_b____)),v_a____,X1,X2,X3),v_b____),sF1)
| c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1682,f1361]) ).
fof(f1696,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(sF8,X0)),v_b____),v_a____),sF0))
| c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1687,f1362]) ).
fof(f1697,plain,
! [X2,X3,X0,X1] :
( c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(sF8,X0)),v_a____,X1,X2,X3),v_b____),sF1)
| ~ c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1688,f1362]) ).
fof(f1700,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(c_COMBC(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(sF8,X0)),v_a____,X1,X2,X3),v_b____),sF1)
| c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1691,f1362]) ).
fof(f1705,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(sF9,X0),v_b____),v_a____),sF0))
| c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1696,f1624]) ).
fof(f1706,plain,
! [X2,X3,X0,X1] :
( c_in(sF0,hAPP(c_COMBC(hAPP(sF9,X0),v_a____,X1,X2,X3),v_b____),sF1)
| ~ c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1697,f1624]) ).
fof(f1708,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(c_COMBC(hAPP(sF9,X0),v_a____,X1,X2,X3),v_b____),sF1)
| c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1700,f1624]) ).
fof(f1712,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(hAPP(sF10,X0),v_a____),sF0))
| c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1705,f1363]) ).
fof(f1713,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(sF10,X0),v_a____),sF1)
| ~ c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1706,f1382]) ).
fof(f1715,plain,
! [X0] :
( ~ c_in(sF0,hAPP(hAPP(sF10,X0),v_a____),sF1)
| c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1708,f1382]) ).
fof(f1719,plain,
! [X0] :
( c_in(sF13,hAPP(sF8,X0),sF1)
| ~ hBOOL(hAPP(hAPP(sF11,X0),sF0)) ),
inference(forward_demodulation,[],[f1712,f1364]) ).
fof(f1720,plain,
! [X0] :
( c_in(sF0,hAPP(sF11,X0),sF1)
| ~ c_in(sF13,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f1713,f1364]) ).
fof(f1722,plain,
! [X0] :
( c_in(sF13,hAPP(sF8,X0),sF1)
| ~ c_in(sF0,hAPP(sF11,X0),sF1) ),
inference(forward_demodulation,[],[f1715,f1364]) ).
fof(f1727,plain,
! [X0] :
( ~ c_in(sF0,hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF8,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| c_in(sF13,v_F(sF8),sF1) ),
inference(resolution,[],[f1722,f1487]) ).
fof(f1732,plain,
! [X0] :
( ~ c_in(sF0,hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| c_in(sF13,v_F(sF8),sF1) ),
inference(forward_subsumption_resolution,[],[f1727,f1328]) ).
fof(f1736,plain,
! [X0] :
( c_in(sF13,sF14,sF1)
| ~ c_in(sF0,hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1) ),
inference(forward_demodulation,[],[f1732,f922]) ).
fof(f1739,plain,
( ! [X0] :
( ~ c_in(sF0,hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1) )
| spl15_2 ),
inference(forward_subsumption_resolution,[],[f1736,f944]) ).
fof(f1740,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF8,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(sF8),sF1)
| c_in(sF0,v_F(X0),sF1) ),
inference(resolution,[],[f1719,f1474]) ).
fof(f1741,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF8,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| c_in(sF13,v_F(sF8),sF1) ),
inference(resolution,[],[f1719,f1487]) ).
fof(f1746,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| c_in(sF13,v_F(sF8),sF1) ),
inference(forward_subsumption_resolution,[],[f1741,f1328]) ).
fof(f1747,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(sF8),sF1)
| c_in(sF0,v_F(X0),sF1) ),
inference(forward_subsumption_resolution,[],[f1740,f1328]) ).
fof(f1750,plain,
! [X0] :
( c_in(sF13,sF14,sF1)
| ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1) ),
inference(forward_demodulation,[],[f1746,f922]) ).
fof(f1751,plain,
! [X0] :
( ~ c_in(sF13,sF14,sF1)
| ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,v_F(X0),sF1) ),
inference(forward_demodulation,[],[f1747,f922]) ).
fof(f1753,plain,
( ! [X0] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF0,v_F(X0),sF1) )
| spl15_2 ),
inference(forward_subsumption_resolution,[],[f1750,f944]) ).
fof(f1800,plain,
( ~ c_in(sF11,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF0,v_F(sF11),sF1)
| ~ c_in(sF13,hAPP(sF8,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| spl15_2 ),
inference(resolution,[],[f1753,f1720]) ).
fof(f1806,plain,
( ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF0,v_F(sF11),sF1)
| ~ c_in(sF13,hAPP(sF8,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| spl15_2 ),
inference(forward_subsumption_resolution,[],[f1800,f1335]) ).
fof(f1807,plain,
( ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF0,v_F(sF11),sF1)
| spl15_2 ),
inference(forward_subsumption_resolution,[],[f1806,f1719]) ).
fof(f1808,plain,
( ~ c_in(sF0,sF12,sF1)
| ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| spl15_2 ),
inference(forward_demodulation,[],[f1807,f918]) ).
fof(f1809,plain,
( ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ spl15_1
| spl15_2 ),
inference(forward_subsumption_resolution,[],[f1808,f941]) ).
fof(f1825,plain,
! [X0] :
( ~ c_in(sF13,hAPP(sF8,X0),sF1)
| hBOOL(hAPP(hAPP(sF11,X0),sF0)) ),
inference(resolution,[],[f769,f1720]) ).
fof(f2243,plain,
! [X0] :
( hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF8,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| c_in(sF13,v_F(sF8),sF1) ),
inference(resolution,[],[f1825,f1534]) ).
fof(f2249,plain,
! [X0] :
( hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| c_in(sF13,v_F(sF8),sF1) ),
inference(forward_subsumption_resolution,[],[f2243,f1328]) ).
fof(f2255,plain,
! [X0] :
( c_in(sF13,sF14,sF1)
| hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1) ),
inference(forward_demodulation,[],[f2249,f922]) ).
fof(f2260,plain,
( ! [X0] :
( c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF0,v_F(X0),sF1) )
| spl15_2 ),
inference(forward_subsumption_resolution,[],[f2255,f944]) ).
fof(f2262,plain,
( ~ c_in(sF11,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF0,v_F(sF11),sF1)
| ~ c_in(sF11,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF0,hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF0,v_F(sF11),sF1)
| spl15_2 ),
inference(resolution,[],[f2260,f1739]) ).
fof(f2272,plain,
( ~ c_in(sF11,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF0,v_F(sF11),sF1)
| ~ c_in(sF0,hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| spl15_2 ),
inference(duplicate_literal_removal,[],[f2262]) ).
fof(f2274,plain,
( ~ c_in(sF11,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF0,v_F(sF11),sF1)
| spl15_2 ),
inference(forward_subsumption_resolution,[],[f2272,f2260]) ).
fof(f2276,plain,
( hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF0,v_F(sF11),sF1)
| spl15_2 ),
inference(forward_subsumption_resolution,[],[f2274,f1335]) ).
fof(f2278,plain,
( ~ c_in(sF0,v_F(sF11),sF1)
| ~ spl15_1
| spl15_2 ),
inference(forward_subsumption_resolution,[],[f2276,f1809]) ).
fof(f2280,plain,
( ~ c_in(sF0,sF12,sF1)
| ~ spl15_1
| spl15_2 ),
inference(forward_demodulation,[],[f2278,f918]) ).
fof(f2283,plain,
( $false
| ~ spl15_1
| spl15_2 ),
inference(forward_subsumption_resolution,[],[f2280,f941]) ).
fof(f2284,plain,
( ~ spl15_1
| spl15_2 ),
inference(avatar_contradiction_clause,[],[f2283]) ).
fof(f2290,plain,
( ! [X0] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(X0,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,v_F(X0),sF1) )
| ~ spl15_2 ),
inference(forward_subsumption_resolution,[],[f1751,f945]) ).
fof(f2309,plain,
( ~ hBOOL(hAPP(hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF0))
| ~ c_in(sF11,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,v_F(sF11),sF1)
| ~ c_in(sF13,hAPP(sF8,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ spl15_2 ),
inference(resolution,[],[f2290,f1720]) ).
fof(f2316,plain,
( ~ c_in(sF11,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,v_F(sF11),sF1)
| ~ c_in(sF13,hAPP(sF8,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ spl15_2 ),
inference(forward_subsumption_resolution,[],[f2309,f1825]) ).
fof(f2317,plain,
( c_in(sF0,v_F(sF11),sF1)
| ~ c_in(sF13,hAPP(sF8,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ spl15_2 ),
inference(forward_subsumption_resolution,[],[f2316,f1335]) ).
fof(f2318,plain,
( c_in(sF0,sF12,sF1)
| ~ c_in(sF13,hAPP(sF8,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ spl15_2 ),
inference(forward_demodulation,[],[f2317,f918]) ).
fof(f2319,plain,
( ~ c_in(sF13,hAPP(sF8,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| spl15_1
| ~ spl15_2 ),
inference(forward_subsumption_resolution,[],[f2318,f940]) ).
fof(f2320,plain,
( ~ c_in(sF8,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF11,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(sF8),sF1)
| c_in(sF0,v_F(sF11),sF1)
| spl15_1
| ~ spl15_2 ),
inference(resolution,[],[f2319,f1427]) ).
fof(f2323,plain,
( ~ c_in(sF0,hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| spl15_1
| ~ spl15_2 ),
inference(resolution,[],[f2319,f1722]) ).
fof(f2326,plain,
( c_in(sF0,hAPP(sF11,v_sko__CHAINED__1(sF11,sF8,v_b____,v_a____,v_c____,v_c____)),sF1)
| ~ c_in(sF11,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(sF8),sF1)
| c_in(sF0,v_F(sF11),sF1)
| spl15_1
| ~ spl15_2 ),
inference(forward_subsumption_resolution,[],[f2320,f1328]) ).
fof(f2328,plain,
( ~ c_in(sF11,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF13,v_F(sF8),sF1)
| c_in(sF0,v_F(sF11),sF1)
| spl15_1
| ~ spl15_2 ),
inference(forward_subsumption_resolution,[],[f2326,f2323]) ).
fof(f2330,plain,
( ~ c_in(sF13,v_F(sF8),sF1)
| c_in(sF0,v_F(sF11),sF1)
| spl15_1
| ~ spl15_2 ),
inference(forward_subsumption_resolution,[],[f2328,f1335]) ).
fof(f2332,plain,
( ~ c_in(sF13,sF14,sF1)
| c_in(sF0,v_F(sF11),sF1)
| spl15_1
| ~ spl15_2 ),
inference(forward_demodulation,[],[f2330,f922]) ).
fof(f2333,plain,
( c_in(sF0,v_F(sF11),sF1)
| spl15_1
| ~ spl15_2 ),
inference(forward_subsumption_resolution,[],[f2332,f945]) ).
fof(f2334,plain,
( c_in(sF0,sF12,sF1)
| spl15_1
| ~ spl15_2 ),
inference(forward_demodulation,[],[f2333,f918]) ).
fof(f2335,plain,
( $false
| spl15_1
| ~ spl15_2 ),
inference(forward_subsumption_resolution,[],[f2334,f940]) ).
fof(f2336,plain,
( spl15_1
| ~ spl15_2 ),
inference(avatar_contradiction_clause,[],[f2335]) ).
cnf(s1,plain,
( spl15_1
| spl15_2 ),
inference(sat_conversion,[],[f946]) ).
cnf(s2,plain,
( ~ spl15_1
| ~ spl15_2 ),
inference(sat_conversion,[],[f947]) ).
cnf(s12,plain,
( ~ spl15_1
| spl15_2 ),
inference(sat_conversion,[],[f2284]) ).
cnf(s13,plain,
( spl15_1
| ~ spl15_2 ),
inference(sat_conversion,[],[f2336]) ).
cnf(s14,plain,
spl15_1,
inference(rat,[],[s1,s13]) ).
cnf(s15,plain,
spl15_2,
inference(rat,[],[s12,s14]) ).
cnf(s16,plain,
$false,
inference(rat,[],[s2,s15,s14]) ).
fof(f2337,plain,
$false,
inference(avatar_sat_refutation,[],[s16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT049-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n016.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 23:39:18 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 5.60/1.77 % (3117463)Input is clausal, will run a generic CNF schedule.
% 5.60/1.77 % (3117470)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2617564534:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.60/1.77 % (3117469)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2066093815:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.60/1.77 % (3117472)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2882875811:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.60/1.77 % (3117471)lrs+10_1_sil=8000:sp=occurrence:random_seed=1717439698:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.60/1.77 % (3117468)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=3137894156:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.60/1.77 % (3117474)dis-21_1_sil=8000:lcm=predicate:random_seed=1793995076: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)
% 5.60/1.77 % (3117473)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3739818334:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.60/1.77 % (3117474)Instruction limit reached!
% 5.60/1.77 % (3117474)------------------------------
% 5.60/1.77 % (3117474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.77 % (3117474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.77 % (3117474)CaDiCaL version: 2.1.3
% 5.60/1.77 % (3117474)Termination reason: Instruction limit
% 5.60/1.77 % (3117474)Termination phase: Saturation
% 5.60/1.77 % (3117474)Time elapsed: 0.064 s
% 5.60/1.77 % (3117474)Peak memory usage: 89 MB
% 5.60/1.77 % (3117474)Instructions burned: 117 (million)
% 5.60/1.77 % (3117471)Instruction limit reached!
% 5.60/1.77 % (3117471)------------------------------
% 5.60/1.77 % (3117471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.77 % (3117471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.77 % (3117471)CaDiCaL version: 2.1.3
% 5.60/1.77 % (3117471)Termination reason: Instruction limit
% 5.60/1.77 % (3117471)Termination phase: Saturation
% 5.60/1.77 % (3117471)Time elapsed: 0.071 s
% 5.60/1.77 % (3117471)Peak memory usage: 89 MB
% 5.60/1.77 % (3117471)Instructions burned: 107 (million)
% 5.60/1.77 % (3117472)Instruction limit reached!
% 5.60/1.77 % (3117472)------------------------------
% 5.60/1.77 % (3117472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.77 % (3117472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.77 % (3117472)CaDiCaL version: 2.1.3
% 5.60/1.77 % (3117472)Termination reason: Instruction limit
% 5.60/1.77 % (3117472)Termination phase: Saturation
% 5.60/1.77 % (3117472)Time elapsed: 0.072 s
% 5.60/1.77 % (3117472)Peak memory usage: 88 MB
% 5.60/1.77 % (3117472)Instructions burned: 114 (million)
% 5.60/1.77 % (3117473)Instruction limit reached!
% 5.60/1.77 % (3117473)------------------------------
% 5.60/1.77 % (3117473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.77 % (3117473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.77 % (3117473)CaDiCaL version: 2.1.3
% 5.60/1.77 % (3117473)Termination reason: Instruction limit
% 5.60/1.77 % (3117473)Termination phase: Saturation
% 5.60/1.77 % (3117473)Time elapsed: 0.119 s
% 5.60/1.77 % (3117473)Peak memory usage: 90 MB
% 5.60/1.77 % (3117473)Instructions burned: 182 (million)
% 5.60/1.77 % (3117483)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=67519851: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)
% 5.60/1.77 % (3117482)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=3313341266:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.60/1.77 % (3117484)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1731427407:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.60/1.77 % (3117482)Refutation not found, incomplete strategy
% 5.60/1.77 % (3117482)------------------------------
% 5.60/1.77 % (3117482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.77 % (3117482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.77 % (3117482)CaDiCaL version: 2.1.3
% 5.60/1.77 % (3117482)Termination reason: Refutation not found, incomplete strategy
% 5.60/1.77 % (3117482)Time elapsed: 0.008 s
% 5.60/1.77 % (3117482)Peak memory usage: 88 MB
% 5.60/1.77 % (3117482)Instructions burned: 12 (million)
% 5.60/1.77 % (3117485)lrs+10_64_to=lpo:sil=8000:random_seed=1998492156:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 5.60/1.77 % (3117483)Instruction limit reached!
% 5.60/1.77 % (3117483)------------------------------
% 5.60/1.77 % (3117483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.77 % (3117483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.77 % (3117483)CaDiCaL version: 2.1.3
% 5.60/1.77 % (3117483)Termination reason: Instruction limit
% 5.60/1.77 % (3117483)Termination phase: Saturation
% 5.60/1.77 % (3117483)Time elapsed: 0.099 s
% 5.60/1.77 % (3117483)Peak memory usage: 90 MB
% 5.60/1.77 % (3117483)Instructions burned: 189 (million)
% 5.60/1.77 % (3117484)Instruction limit reached!
% 5.60/1.77 % (3117484)------------------------------
% 5.60/1.77 % (3117484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.77 % (3117484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.77 % (3117484)CaDiCaL version: 2.1.3
% 5.60/1.77 % (3117484)Termination reason: Instruction limit
% 5.60/1.77 % (3117484)Termination phase: Saturation
% 5.60/1.77 % (3117484)Time elapsed: 0.121 s
% 5.60/1.77 % (3117484)Peak memory usage: 90 MB
% 5.60/1.77 % (3117484)Instructions burned: 219 (million)
% 5.60/1.77 % (3117485)Instruction limit reached!
% 5.60/1.77 % (3117485)------------------------------
% 5.60/1.77 % (3117485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.77 % (3117485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.77 % (3117485)CaDiCaL version: 2.1.3
% 5.60/1.77 % (3117485)Termination reason: Instruction limit
% 5.60/1.77 % (3117485)Termination phase: Saturation
% 5.60/1.77 % (3117485)Time elapsed: 0.077 s
% 5.60/1.77 % (3117485)Peak memory usage: 90 MB
% 5.60/1.77 % (3117485)Instructions burned: 126 (million)
% 5.60/1.77 % (3117490)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1159632973:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.60/1.77 % (3117491)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=745925463:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.60/1.77 % (3117482)------------------------------
% 5.60/1.77 % (3117482)------------------------------
% 5.60/1.77 % (3117492)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1986899730:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 5.60/1.77 % (3117491)Instruction limit reached!
% 5.60/1.77 % (3117491)------------------------------
% 5.60/1.77 % (3117491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.77 % (3117491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.77 % (3117491)CaDiCaL version: 2.1.3
% 5.60/1.77 % (3117491)Termination reason: Instruction limit
% 5.60/1.77 % (3117491)Termination phase: Saturation
% 5.60/1.77 % (3117491)Time elapsed: 0.096 s
% 5.60/1.77 % (3117491)Peak memory usage: 91 MB
% 5.60/1.77 % (3117491)Instructions burned: 158 (million)
% 5.60/1.77 % (3117490)Instruction limit reached!
% 5.60/1.77 % (3117490)------------------------------
% 5.60/1.77 % (3117490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.77 % (3117490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.77 % (3117490)CaDiCaL version: 2.1.3
% 5.60/1.77 % (3117490)Termination reason: Instruction limit
% 5.60/1.77 % (3117490)Termination phase: Saturation
% 5.60/1.77 % (3117490)Time elapsed: 0.124 s
% 5.60/1.77 % (3117490)Peak memory usage: 90 MB
% 5.60/1.77 % (3117490)Instructions burned: 195 (million)
% 5.60/1.77 % (3117470)First to succeed.
% 5.60/1.77 % (3117470)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3117463"
% 5.60/1.77 % (3117495)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=2903633766:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 5.60/1.77 % (3117495)Instruction limit reached!
% 5.60/1.77 % (3117495)------------------------------
% 5.60/1.77 % (3117495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.77 % (3117495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.77 % (3117495)CaDiCaL version: 2.1.3
% 5.60/1.77 % (3117495)Termination reason: Instruction limit
% 5.60/1.77 % (3117495)Termination phase: Saturation
% 5.60/1.77 % (3117495)Time elapsed: 0.060 s
% 5.60/1.77 % (3117495)Peak memory usage: 89 MB
% 5.60/1.77 % (3117495)Instructions burned: 106 (million)
% 5.60/1.77 % (3117497)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2684290017:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 5.60/1.77 % (3117498)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3703303851:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 5.60/1.77 % (3117470)Refutation found. Thanks to Tanya!
% 5.60/1.77 % SZS status Unsatisfiable for theBenchmark
% 5.60/1.77 % SZS output start Proof for theBenchmark
% See solution above
% 6.85/1.96 % (3117470)------------------------------
% 6.85/1.96 % (3117470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/1.96 % (3117470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.96 % (3117470)CaDiCaL version: 2.1.3
% 6.85/1.96 % (3117470)Termination reason: Refutation
% 6.85/1.96 % (3117470)Time elapsed: 0.614 s
% 6.85/1.96 % (3117470)Peak memory usage: 141 MB
% 6.85/1.96 % (3117470)Instructions burned: 1750 (million)
% 6.85/1.96 % (3117470)------------------------------
% 6.85/1.96 % (3117470)------------------------------
% 6.85/1.96 % (3117463)Success in time 0.916 s
% 6.85/1.96 % Vampire exiting
%------------------------------------------------------------------------------