%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT047-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 : n017.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:48 PM UTC 2026
% Result : Unsatisfiable 7.25s 2.14s
% Output : Refutation 11.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 28
% Syntax : Number of formulae : 179 ( 48 unt; 14 def)
% Number of atoms : 842 ( 236 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 1016 ( 353 ~; 661 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 7 avg)
% Maximal term depth : 10 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 3 prp; 0-3 aty)
% Number of functors : 29 ( 29 usr; 21 con; 0-6 aty)
% Number of variables : 338 ( 0 sgn 338 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f790,axiom,
v_a____ != v_c____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_1) ).
fof(f791,axiom,
v_a____ != v_b____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f792,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_01) ).
fof(f793,axiom,
c_in(v_P____,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(f794,axiom,
! [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)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(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(f795,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(f796,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)),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(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(reorient_equations,[],[f795]) ).
fof(f797,axiom,
! [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)),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(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(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(f798,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(f799,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)),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),v_F(X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(reorient_equations,[],[f798]) ).
fof(f800,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_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_1_06) ).
fof(f801,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_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_07) ).
fof(f802,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_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f803,negated_conjecture,
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),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_1) ).
fof(f822,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(f823,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(f917,definition,
sF0 = c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f918,plain,
c_Pair(v_a____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(reorient_equations,[],[f917]) ).
fof(f919,definition,
sF1 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f920,plain,
tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF1,
inference(reorient_equations,[],[f919]) ).
fof(f921,definition,
sF2 = tc_fun(sF1,tc_bool),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f922,plain,
tc_fun(sF1,tc_bool) = sF2,
inference(reorient_equations,[],[f921]) ).
fof(f923,definition,
sF3 = tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f924,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2) = sF3,
inference(reorient_equations,[],[f923]) ).
fof(f925,definition,
sF4 = tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f926,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3) = sF4,
inference(reorient_equations,[],[f925]) ).
fof(f927,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(f928,plain,
c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF2,sF4,tc_Arrow__Order__Mirabelle_Oindi) = sF5,
inference(reorient_equations,[],[f927]) ).
fof(f929,definition,
sF6 = hAPP(sF5,v_P____),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f930,plain,
hAPP(sF5,v_P____) = sF6,
inference(reorient_equations,[],[f929]) ).
fof(f931,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(f932,plain,
c_COMBC(sF6,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3) = sF7,
inference(reorient_equations,[],[f931]) ).
fof(f933,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(f934,plain,
c_COMBC(sF7,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2) = sF8,
inference(reorient_equations,[],[f933]) ).
fof(f935,definition,
sF9 = v_F(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f936,plain,
v_F(sF8) = sF9,
inference(reorient_equations,[],[f935]) ).
fof(f937,definition,
sF10 = c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f938,plain,
c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF10,
inference(reorient_equations,[],[f937]) ).
fof(f939,definition,
sF11 = v_F(v_P____),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f940,plain,
v_F(v_P____) = sF11,
inference(reorient_equations,[],[f939]) ).
fof(f941,plain,
( ~ c_in(sF0,sF9,sF1)
| ~ c_in(sF10,sF11,sF1) ),
inference(definition_folding,[],[f802,f920,f940,f938,f920,f936,f934,f922,f920,f932,f924,f922,f920,f930,f928,f926,f924,f922,f920,f922,f920,f918]) ).
fof(f942,plain,
( c_in(sF10,sF11,sF1)
| c_in(sF0,sF9,sF1) ),
inference(definition_folding,[],[f803,f920,f936,f934,f922,f920,f932,f924,f922,f920,f930,f928,f926,f924,f922,f920,f922,f920,f918,f920,f940,f938]) ).
fof(f957,definition,
( spl12_1
<=> c_in(sF0,sF9,sF1) ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f958,plain,
( ~ c_in(sF0,sF9,sF1)
| spl12_1 ),
inference(avatar_component_clause,[],[f957]) ).
fof(f959,plain,
( c_in(sF0,sF9,sF1)
| ~ spl12_1 ),
inference(avatar_component_clause,[],[f957]) ).
fof(f961,definition,
( spl12_2
<=> c_in(sF10,sF11,sF1) ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f962,plain,
( ~ c_in(sF10,sF11,sF1)
| spl12_2 ),
inference(avatar_component_clause,[],[f961]) ).
fof(f963,plain,
( c_in(sF10,sF11,sF1)
| ~ spl12_2 ),
inference(avatar_component_clause,[],[f961]) ).
fof(f964,plain,
( spl12_1
| spl12_2 ),
inference(avatar_split_clause,[],[f942,f961,f957]) ).
fof(f965,plain,
( ~ spl12_2
| ~ spl12_1 ),
inference(avatar_split_clause,[],[f941,f957,f961]) ).
fof(f1034,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(superposition,[],[f792,f920]) ).
fof(f1035,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,[],[f1034,f922]) ).
fof(f1036,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,[],[f1035,f924]) ).
fof(f1037,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,[],[f1036,f926]) ).
fof(f1038,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,[],[f1037,f928]) ).
fof(f1039,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,[],[f1038,f930]) ).
fof(f1040,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,[],[f1039,f932]) ).
fof(f1041,plain,
c_in(sF8,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1040,f934]) ).
fof(f1043,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(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),sF1) ),
inference(superposition,[],[f801,f920]) ).
fof(f1044,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),sF1)
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),sF1) ),
inference(forward_demodulation,[],[f1043,f918]) ).
fof(f1046,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),sF1)
| ~ c_in(sF10,hAPP(v_P____,X0),sF1) ),
inference(forward_demodulation,[],[f1044,f938]) ).
fof(f1051,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(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),sF1) ),
inference(superposition,[],[f800,f920]) ).
fof(f1052,plain,
! [X0] :
( ~ c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),sF1)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),sF1) ),
inference(forward_demodulation,[],[f1051,f918]) ).
fof(f1054,plain,
! [X0] :
( ~ c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____),sF1)
| c_in(sF10,hAPP(v_P____,X0),sF1) ),
inference(forward_demodulation,[],[f1052,f938]) ).
fof(f1058,plain,
! [X0] : hAPP(hAPP(sF7,X0),v_b____) = hAPP(sF8,X0),
inference(superposition,[],[f822,f934]) ).
fof(f1059,plain,
! [X0] : hAPP(sF7,X0) = hAPP(hAPP(sF6,X0),v_c____),
inference(superposition,[],[f822,f932]) ).
fof(f1061,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| v_a____ = v_c____
| X2 = X3 ),
inference(superposition,[],[f794,f918]) ).
fof(f1066,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f1061,f790]) ).
fof(f1070,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1066,f920]) ).
fof(f1073,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,v_F(X0),sF1)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(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____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1070,f920]) ).
fof(f1076,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| ~ 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____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1073,f920]) ).
fof(f1079,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(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| ~ c_in(sF0,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,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1076,f920]) ).
fof(f1082,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| ~ 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(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| ~ c_in(sF0,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,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1079,f920]) ).
fof(f1085,plain,
! [X2,X3,X0,X1] :
( ~ 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(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| ~ c_in(sF0,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,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1082,f922]) ).
fof(f1088,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| ~ 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(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1085,f920]) ).
fof(f1090,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(X1,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),v_F(X1),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1088,f922]) ).
fof(f1100,plain,
! [X0,X1] :
( ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),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(sF10,v_F(X0),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1)
| v_a____ = v_b____
| v_a____ = v_c____
| v_a____ = v_b____ ),
inference(superposition,[],[f1090,f938]) ).
fof(f1104,plain,
! [X0,X1] :
( ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),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(sF10,v_F(X0),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1)
| v_a____ = v_b____
| v_a____ = v_c____ ),
inference(duplicate_literal_removal,[],[f1100]) ).
fof(f1106,plain,
! [X0,X1] :
( ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),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(sF10,v_F(X0),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1)
| v_a____ = v_c____ ),
inference(forward_subsumption_resolution,[],[f1104,f791]) ).
fof(f1107,plain,
! [X0,X1] :
( ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),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(sF10,v_F(X0),sF1)
| ~ c_in(sF0,v_F(X1),sF1)
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1) ),
inference(forward_subsumption_resolution,[],[f1106,f790]) ).
fof(f1108,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF10,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X3
| X2 = X3
| v_a____ = v_b____ ),
inference(superposition,[],[f796,f938]) ).
fof(f1115,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF10,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X3
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f1108,f791]) ).
fof(f1119,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),sF1)
| ~ c_in(sF10,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1115,f920]) ).
fof(f1122,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF10,v_F(X0),sF1)
| ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),sF1)
| ~ 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_a____,X2,v_b____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1119,f920]) ).
fof(f1125,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_a____,X2,v_b____,X3)),sF1)
| ~ c_in(sF10,v_F(X0),sF1)
| ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1122,f920]) ).
fof(f1128,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| ~ 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_a____,X2,v_b____,X3)),sF1)
| ~ c_in(sF10,v_F(X0),sF1)
| ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1125,f920]) ).
fof(f1131,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| ~ 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_a____,X2,v_b____,X3)),sF1)
| ~ c_in(sF10,v_F(X0),sF1)
| ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1128,f920]) ).
fof(f1134,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,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),v_F(X1),sF1)
| ~ 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_a____,X2,v_b____,X3)),sF1)
| ~ c_in(sF10,v_F(X0),sF1)
| ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = X2
| v_a____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1131,f922]) ).
fof(f1137,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| ~ c_in(X1,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),v_F(X1),sF1)
| ~ 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_a____,X2,v_b____,X3)),sF1)
| ~ c_in(sF10,v_F(X0),sF1)
| ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),sF1)
| v_b____ = X2
| v_a____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1134,f920]) ).
fof(f1139,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_a____,X2,v_b____,X3)),sF1)
| ~ c_in(X1,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),v_F(X1),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF10,v_F(X0),sF1)
| ~ c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,X2,v_b____,X3)),sF1)
| v_b____ = X2
| v_a____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f1137,f922]) ).
fof(f1141,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_a____,v_a____,v_b____,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)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF10,v_F(X1),sF1)
| ~ c_in(sF10,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_a____,v_a____,v_b____,v_c____)),sF1)
| v_a____ = v_b____
| v_a____ = v_c____
| v_a____ = v_c____ ),
inference(superposition,[],[f1139,f918]) ).
fof(f1143,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_a____,v_a____,v_b____,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)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF10,v_F(X1),sF1)
| ~ c_in(sF10,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_a____,v_a____,v_b____,v_c____)),sF1)
| v_a____ = v_b____
| v_a____ = v_c____ ),
inference(duplicate_literal_removal,[],[f1141]) ).
fof(f1145,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_a____,v_a____,v_b____,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)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF10,v_F(X1),sF1)
| ~ c_in(sF10,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_a____,v_a____,v_b____,v_c____)),sF1)
| v_a____ = v_c____ ),
inference(forward_subsumption_resolution,[],[f1143,f791]) ).
fof(f1147,plain,
! [X0,X1] :
( ~ c_in(sF10,hAPP(X1,v_sko__CHAINED__1(X1,X0,v_a____,v_a____,v_b____,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)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF10,v_F(X1),sF1)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,v_a____,v_a____,v_b____,v_c____)),sF1) ),
inference(forward_subsumption_resolution,[],[f1145,f790]) ).
fof(f1165,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(X0,X2,X3,X4,X5)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_COMBC(X0,X2,X3,X4,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(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(superposition,[],[f799,f822]) ).
fof(f1171,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF1)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(X0,X2,X3,X4,X5)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_COMBC(X0,X2,X3,X4,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(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(forward_demodulation,[],[f1165,f920]) ).
fof(f1179,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF1)
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF1)
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(X0,X2,X3,X4,X5)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_COMBC(X0,X2,X3,X4,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(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(forward_demodulation,[],[f1171,f920]) ).
fof(f1186,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF1)
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF1)
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(X0,X2,X3,X4,X5)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_COMBC(X0,X2,X3,X4,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(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(forward_demodulation,[],[f1179,f920]) ).
fof(f1192,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(X0,X2,X3,X4,X5)),sF1)
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF1)
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF1)
| ~ c_in(c_COMBC(X0,X2,X3,X4,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(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(forward_demodulation,[],[f1186,f920]) ).
fof(f1198,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ c_in(c_COMBC(X0,X2,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(X0,X2,X3,X4,X5)),sF1)
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF1)
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(forward_demodulation,[],[f1192,f920]) ).
fof(f1204,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ c_in(c_COMBC(X0,X2,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(X0,X2,X3,X4,X5)),sF1)
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF1)
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(forward_demodulation,[],[f1198,f922]) ).
fof(f1210,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| ~ c_in(c_COMBC(X0,X2,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(X0,X2,X3,X4,X5)),sF1)
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF1)
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF1)
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(forward_demodulation,[],[f1204,f920]) ).
fof(f1216,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF1)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF1)
| c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_COMBC(X0,X2,X3,X4,X5)),sF1)
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| ~ c_in(c_COMBC(X0,X2,X3,X4,X5),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))
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(forward_demodulation,[],[f1210,f922]) ).
fof(f1285,plain,
! [X2,X3,X0,X1,X4] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X2,sF8,X0,X3,X1,X4)),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(sF7,v_sko__CHAINED__1(X2,sF8,X0,X3,X1,X4)),v_b____),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(sF8),sF1)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF1)
| ~ c_in(sF8,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(superposition,[],[f1216,f934]) ).
fof(f1293,plain,
! [X2,X3,X0,X1,X4] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X2,sF8,X0,X3,X1,X4)),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(sF7,v_sko__CHAINED__1(X2,sF8,X0,X3,X1,X4)),v_b____),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(sF8),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,sF2))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f1285,f1041]) ).
fof(f1296,plain,
! [X2,X3,X0,X1,X4] :
( c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF8,v_sko__CHAINED__1(X2,sF8,X0,X3,X1,X4)),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X2,sF8,X0,X3,X1,X4)),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(sF8),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,sF2))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1293,f1058]) ).
fof(f1298,plain,
! [X2,X3,X0,X1,X4] :
( c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF8,v_sko__CHAINED__1(X2,sF8,X0,X3,X1,X4)),sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X2,sF8,X0,X3,X1,X4)),sF1)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF9,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,sF2))
| X1 = X3
| X0 = X4
| X3 = X4
| X0 = X1 ),
inference(forward_demodulation,[],[f1296,f936]) ).
fof(f1306,plain,
! [X2,X0,X1] :
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(X0,sF8,X1,v_a____,X2,v_c____)),sF1)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(X0,sF8,X1,v_a____,X2,v_c____)),sF1)
| c_in(sF0,sF9,sF1)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| v_a____ = X2
| v_c____ = X1
| v_a____ = v_c____
| X1 = X2 ),
inference(superposition,[],[f1298,f918]) ).
fof(f1317,plain,
( ! [X2,X0,X1] :
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(X0,sF8,X1,v_a____,X2,v_c____)),sF1)
| c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(X0,sF8,X1,v_a____,X2,v_c____)),sF1)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| v_a____ = X2
| v_c____ = X1
| v_a____ = v_c____
| X1 = X2 )
| spl12_1 ),
inference(forward_subsumption_resolution,[],[f1306,f958]) ).
fof(f1322,plain,
( ! [X2,X0,X1] :
( c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(X0,sF8,X1,v_a____,X2,v_c____)),sF1)
| c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(X0,sF8,X1,v_a____,X2,v_c____)),sF1)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| v_a____ = X2
| v_c____ = X1
| X1 = X2 )
| spl12_1 ),
inference(forward_subsumption_resolution,[],[f1317,f790]) ).
fof(f1338,plain,
( ! [X0] :
( c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(X0,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ c_in(sF10,v_F(X0),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| v_a____ = v_b____
| v_a____ = v_c____
| v_a____ = v_b____ )
| spl12_1 ),
inference(superposition,[],[f1322,f938]) ).
fof(f1342,plain,
( ! [X0] :
( c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(X0,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ c_in(sF10,v_F(X0),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| v_a____ = v_b____
| v_a____ = v_c____ )
| spl12_1 ),
inference(duplicate_literal_removal,[],[f1338]) ).
fof(f1346,plain,
( ! [X0] :
( c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(X0,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ c_in(sF10,v_F(X0),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| v_a____ = v_c____ )
| spl12_1 ),
inference(forward_subsumption_resolution,[],[f1342,f791]) ).
fof(f1347,plain,
( ! [X0] :
( c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(X0,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ c_in(sF10,v_F(X0),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)) )
| spl12_1 ),
inference(forward_subsumption_resolution,[],[f1346,f790]) ).
fof(f1373,plain,
! [X2,X3,X0,X1] :
( c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| v_a____ = v_c____
| X2 = X3 ),
inference(superposition,[],[f797,f918]) ).
fof(f1389,plain,
! [X2,X3,X0,X1] :
( c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f1373,f790]) ).
fof(f1397,plain,
! [X2,X3,X0,X1] :
( c_in(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| 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____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1389,f920]) ).
fof(f1403,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(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1397,f920]) ).
fof(f1409,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF0,v_F(X0),sF1)
| 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(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1403,f920]) ).
fof(f1415,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| 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(sF0,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,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1409,f920]) ).
fof(f1421,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| 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(sF0,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,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1415,f920]) ).
fof(f1427,plain,
! [X2,X3,X0,X1] :
( ~ 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),v_F(X1),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| 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(sF0,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,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1421,f922]) ).
fof(f1433,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool)))
| ~ 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),v_F(X1),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| 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(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1427,f920]) ).
fof(f1437,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(sF0,hAPP(X0,v_sko__CHAINED__1(X1,X0,X2,v_a____,X3,v_c____)),sF1)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF1)
| ~ c_in(sF0,v_F(X0),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))
| v_a____ = X3
| v_c____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f1433,f922]) ).
fof(f1441,plain,
! [X0,X1] :
( c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF10,v_F(X0),sF1)
| ~ c_in(sF0,v_F(X1),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))
| v_a____ = v_b____
| v_a____ = v_c____
| v_a____ = v_b____ ),
inference(superposition,[],[f1437,f938]) ).
fof(f1446,plain,
! [X0,X1] :
( c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF10,v_F(X0),sF1)
| ~ c_in(sF0,v_F(X1),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))
| v_a____ = v_b____
| v_a____ = v_c____ ),
inference(duplicate_literal_removal,[],[f1441]) ).
fof(f1450,plain,
! [X0,X1] :
( c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF10,v_F(X0),sF1)
| ~ c_in(sF0,v_F(X1),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))
| v_a____ = v_c____ ),
inference(forward_subsumption_resolution,[],[f1446,f791]) ).
fof(f1451,plain,
! [X0,X1] :
( c_in(sF10,hAPP(X0,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(X1,v_sko__CHAINED__1(X0,X1,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF10,v_F(X0),sF1)
| ~ c_in(sF0,v_F(X1),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)) ),
inference(forward_subsumption_resolution,[],[f1450,f790]) ).
fof(f1505,plain,
c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF1,tc_bool))),
inference(superposition,[],[f793,f920]) ).
fof(f1506,plain,
c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)),
inference(forward_demodulation,[],[f1505,f922]) ).
fof(f2470,plain,
! [X0,X1] : hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(X0,X1)) = hAPP(hAPP(sF5,X0),X1),
inference(superposition,[],[f823,f928]) ).
fof(f2615,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)) = hAPP(sF6,X0),
inference(superposition,[],[f2470,f930]) ).
fof(f2760,plain,
! [X0] :
( ~ c_in(sF0,hAPP(hAPP(hAPP(sF6,X0),v_c____),v_b____),sF1)
| c_in(sF10,hAPP(v_P____,X0),sF1) ),
inference(superposition,[],[f1054,f2615]) ).
fof(f2762,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(sF6,X0),v_c____),v_b____),sF1)
| ~ c_in(sF10,hAPP(v_P____,X0),sF1) ),
inference(superposition,[],[f1046,f2615]) ).
fof(f2765,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(sF7,X0),v_b____),sF1)
| ~ c_in(sF10,hAPP(v_P____,X0),sF1) ),
inference(forward_demodulation,[],[f2762,f1059]) ).
fof(f2767,plain,
! [X0] :
( ~ c_in(sF0,hAPP(hAPP(sF7,X0),v_b____),sF1)
| c_in(sF10,hAPP(v_P____,X0),sF1) ),
inference(forward_demodulation,[],[f2760,f1059]) ).
fof(f2769,plain,
! [X0] :
( ~ c_in(sF10,hAPP(v_P____,X0),sF1)
| c_in(sF0,hAPP(sF8,X0),sF1) ),
inference(forward_demodulation,[],[f2765,f1058]) ).
fof(f2771,plain,
! [X0] :
( ~ c_in(sF0,hAPP(sF8,X0),sF1)
| c_in(sF10,hAPP(v_P____,X0),sF1) ),
inference(forward_demodulation,[],[f2767,f1058]) ).
fof(f2780,plain,
! [X0] :
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,X0,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_P____,X0,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF10,v_F(v_P____),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)) ),
inference(resolution,[],[f2769,f1451]) ).
fof(f2784,plain,
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ c_in(sF10,v_F(v_P____),sF1)
| ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| spl12_1 ),
inference(resolution,[],[f2769,f1347]) ).
fof(f2793,plain,
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ c_in(sF10,v_F(v_P____),sF1)
| ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| spl12_1 ),
inference(duplicate_literal_removal,[],[f2784]) ).
fof(f2801,plain,
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ c_in(sF10,v_F(v_P____),sF1)
| spl12_1 ),
inference(forward_subsumption_resolution,[],[f2793,f1506]) ).
fof(f2805,plain,
! [X0] :
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,X0,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_P____,X0,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF10,v_F(v_P____),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)) ),
inference(forward_subsumption_resolution,[],[f2780,f1506]) ).
fof(f2813,plain,
( ~ c_in(sF10,sF11,sF1)
| c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| spl12_1 ),
inference(forward_demodulation,[],[f2801,f940]) ).
fof(f2817,plain,
! [X0] :
( c_in(sF10,sF11,sF1)
| c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,X0,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_P____,X0,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)) ),
inference(forward_demodulation,[],[f2805,f940]) ).
fof(f2821,plain,
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| spl12_1
| ~ spl12_2 ),
inference(forward_subsumption_resolution,[],[f2813,f963]) ).
fof(f2841,plain,
( c_in(sF10,hAPP(v_P____,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| spl12_1
| ~ spl12_2 ),
inference(resolution,[],[f2771,f2821]) ).
fof(f2858,plain,
( ~ c_in(sF8,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF0,v_F(sF8),sF1)
| ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF10,v_F(v_P____),sF1)
| ~ c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| spl12_1
| ~ spl12_2 ),
inference(resolution,[],[f2841,f1147]) ).
fof(f2859,plain,
( c_in(sF0,v_F(sF8),sF1)
| ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(sF10,v_F(v_P____),sF1)
| ~ c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| spl12_1
| ~ spl12_2 ),
inference(forward_subsumption_resolution,[],[f2858,f1041]) ).
fof(f2861,plain,
( c_in(sF0,v_F(sF8),sF1)
| ~ c_in(sF10,v_F(v_P____),sF1)
| ~ c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| spl12_1
| ~ spl12_2 ),
inference(forward_subsumption_resolution,[],[f2859,f1506]) ).
fof(f2863,plain,
( c_in(sF0,v_F(sF8),sF1)
| ~ c_in(sF10,v_F(v_P____),sF1)
| spl12_1
| ~ spl12_2 ),
inference(forward_subsumption_resolution,[],[f2861,f2821]) ).
fof(f2865,plain,
( c_in(sF0,sF9,sF1)
| ~ c_in(sF10,v_F(v_P____),sF1)
| spl12_1
| ~ spl12_2 ),
inference(forward_demodulation,[],[f2863,f936]) ).
fof(f2867,plain,
( ~ c_in(sF10,v_F(v_P____),sF1)
| spl12_1
| ~ spl12_2 ),
inference(forward_subsumption_resolution,[],[f2865,f958]) ).
fof(f2868,plain,
( ~ c_in(sF10,sF11,sF1)
| spl12_1
| ~ spl12_2 ),
inference(forward_demodulation,[],[f2867,f940]) ).
fof(f2869,plain,
( $false
| spl12_1
| ~ spl12_2 ),
inference(forward_subsumption_resolution,[],[f2868,f963]) ).
fof(f2870,plain,
( spl12_1
| ~ spl12_2 ),
inference(avatar_contradiction_clause,[],[f2869]) ).
fof(f2876,plain,
( ! [X0] :
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,X0,v_a____,v_a____,v_b____,v_c____)),sF1)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_P____,X0,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ c_in(sF0,v_F(X0),sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2)) )
| spl12_2 ),
inference(forward_subsumption_resolution,[],[f2817,f962]) ).
fof(f2947,plain,
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ c_in(sF0,v_F(sF8),sF1)
| ~ c_in(sF8,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| spl12_2 ),
inference(factoring,[],[f2876]) ).
fof(f2951,plain,
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ c_in(sF0,v_F(sF8),sF1)
| spl12_2 ),
inference(forward_subsumption_resolution,[],[f2947,f1041]) ).
fof(f2952,plain,
( ~ c_in(sF0,sF9,sF1)
| c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| spl12_2 ),
inference(forward_demodulation,[],[f2951,f936]) ).
fof(f2953,plain,
( c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ spl12_1
| spl12_2 ),
inference(forward_subsumption_resolution,[],[f2952,f959]) ).
fof(f2954,plain,
( c_in(sF10,hAPP(v_P____,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ spl12_1
| spl12_2 ),
inference(resolution,[],[f2953,f2771]) ).
fof(f2956,plain,
( ~ c_in(sF8,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF10,v_F(v_P____),sF1)
| ~ c_in(sF0,v_F(sF8),sF1)
| ~ c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ spl12_1
| spl12_2 ),
inference(resolution,[],[f2954,f1107]) ).
fof(f2959,plain,
( ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF2))
| c_in(sF10,v_F(v_P____),sF1)
| ~ c_in(sF0,v_F(sF8),sF1)
| ~ c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ spl12_1
| spl12_2 ),
inference(forward_subsumption_resolution,[],[f2956,f1041]) ).
fof(f2961,plain,
( c_in(sF10,v_F(v_P____),sF1)
| ~ c_in(sF0,v_F(sF8),sF1)
| ~ c_in(sF0,hAPP(sF8,v_sko__CHAINED__1(v_P____,sF8,v_a____,v_a____,v_b____,v_c____)),sF1)
| ~ spl12_1
| spl12_2 ),
inference(forward_subsumption_resolution,[],[f2959,f1506]) ).
fof(f2963,plain,
( c_in(sF10,v_F(v_P____),sF1)
| ~ c_in(sF0,v_F(sF8),sF1)
| ~ spl12_1
| spl12_2 ),
inference(forward_subsumption_resolution,[],[f2961,f2953]) ).
fof(f2965,plain,
( c_in(sF10,sF11,sF1)
| ~ c_in(sF0,v_F(sF8),sF1)
| ~ spl12_1
| spl12_2 ),
inference(forward_demodulation,[],[f2963,f940]) ).
fof(f2966,plain,
( ~ c_in(sF0,v_F(sF8),sF1)
| ~ spl12_1
| spl12_2 ),
inference(forward_subsumption_resolution,[],[f2965,f962]) ).
fof(f2967,plain,
( ~ c_in(sF0,sF9,sF1)
| ~ spl12_1
| spl12_2 ),
inference(forward_demodulation,[],[f2966,f936]) ).
fof(f2968,plain,
( $false
| ~ spl12_1
| spl12_2 ),
inference(forward_subsumption_resolution,[],[f2967,f959]) ).
fof(f2969,plain,
( ~ spl12_1
| spl12_2 ),
inference(avatar_contradiction_clause,[],[f2968]) ).
cnf(s1,plain,
( spl12_1
| spl12_2 ),
inference(sat_conversion,[],[f964]) ).
cnf(s2,plain,
( ~ spl12_1
| ~ spl12_2 ),
inference(sat_conversion,[],[f965]) ).
cnf(s4,plain,
( spl12_1
| ~ spl12_2 ),
inference(sat_conversion,[],[f2870]) ).
cnf(s7,plain,
( ~ spl12_1
| spl12_2 ),
inference(sat_conversion,[],[f2969]) ).
cnf(s8,plain,
spl12_1,
inference(rat,[],[s1,s4]) ).
cnf(s9,plain,
spl12_2,
inference(rat,[],[s7,s8]) ).
cnf(s10,plain,
$false,
inference(rat,[],[s2,s9,s8]) ).
fof(f2970,plain,
$false,
inference(avatar_sat_refutation,[],[s10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT047-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n017.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 23:30:06 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 Running first-order theorem proving
% 0.15/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.68/2.06 % (3068412)Input is clausal, will run a generic CNF schedule.
% 9.68/2.06 % (3068422)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4271177783:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.68/2.06 % (3068420)lrs+10_1_sil=8000:sp=occurrence:random_seed=2878717445:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.68/2.06 % (3068419)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2246110650:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.68/2.06 % (3068418)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3401916452:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.68/2.06 % (3068417)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=2450561051:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.68/2.06 % (3068421)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3455904380:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.68/2.06 % (3068423)dis-21_1_sil=8000:lcm=predicate:random_seed=873476503: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)
% 9.68/2.06 % (3068423)Instruction limit reached!
% 9.68/2.06 % (3068423)------------------------------
% 9.68/2.06 % (3068423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.06 % (3068423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.06 % (3068423)CaDiCaL version: 2.1.3
% 9.68/2.06 % (3068423)Termination reason: Instruction limit
% 9.68/2.06 % (3068423)Termination phase: Saturation
% 9.68/2.06 % (3068423)Time elapsed: 0.064 s
% 9.68/2.06 % (3068423)Peak memory usage: 89 MB
% 9.68/2.06 % (3068423)Instructions burned: 117 (million)
% 9.68/2.06 % (3068420)Instruction limit reached!
% 9.68/2.06 % (3068420)------------------------------
% 9.68/2.06 % (3068420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.06 % (3068420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.06 % (3068420)CaDiCaL version: 2.1.3
% 9.68/2.06 % (3068420)Termination reason: Instruction limit
% 9.68/2.06 % (3068420)Termination phase: Saturation
% 9.68/2.06 % (3068420)Time elapsed: 0.070 s
% 9.68/2.06 % (3068420)Peak memory usage: 89 MB
% 9.68/2.06 % (3068420)Instructions burned: 108 (million)
% 9.68/2.06 % (3068421)Instruction limit reached!
% 9.68/2.06 % (3068421)------------------------------
% 9.68/2.06 % (3068421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.06 % (3068421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.06 % (3068421)CaDiCaL version: 2.1.3
% 9.68/2.06 % (3068421)Termination reason: Instruction limit
% 9.68/2.06 % (3068421)Termination phase: Saturation
% 9.68/2.06 % (3068421)Time elapsed: 0.077 s
% 9.68/2.06 % (3068421)Peak memory usage: 89 MB
% 9.68/2.06 % (3068421)Instructions burned: 115 (million)
% 9.68/2.06 % (3068422)Instruction limit reached!
% 9.68/2.06 % (3068422)------------------------------
% 9.68/2.06 % (3068422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.06 % (3068422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.06 % (3068422)CaDiCaL version: 2.1.3
% 9.68/2.06 % (3068422)Termination reason: Instruction limit
% 9.68/2.06 % (3068422)Termination phase: Saturation
% 9.68/2.06 % (3068422)Time elapsed: 0.107 s
% 9.68/2.06 % (3068422)Peak memory usage: 90 MB
% 9.68/2.06 % (3068422)Instructions burned: 181 (million)
% 9.68/2.06 % (3068431)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=3112731031:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.68/2.06 % (3068432)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2397644969: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)
% 9.68/2.06 % (3068431)Refutation not found, incomplete strategy
% 9.68/2.06 % (3068431)------------------------------
% 9.68/2.06 % (3068431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.06 % (3068431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.06 % (3068431)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068431)Termination reason: Refutation not found, incomplete strategy
% 7.25/2.14 % (3068431)Time elapsed: 0.007 s
% 7.25/2.14 % (3068431)Peak memory usage: 89 MB
% 7.25/2.14 % (3068431)Instructions burned: 10 (million)
% 7.25/2.14 % (3068433)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1411707147:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 7.25/2.14 % (3068434)lrs+10_64_to=lpo:sil=8000:random_seed=3031616492:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 7.25/2.14 % (3068434)Instruction limit reached!
% 7.25/2.14 % (3068434)------------------------------
% 7.25/2.14 % (3068434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.25/2.14 % (3068434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.25/2.14 % (3068434)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068434)Termination reason: Instruction limit
% 7.25/2.14 % (3068434)Termination phase: Saturation
% 7.25/2.14 % (3068434)Time elapsed: 0.048 s
% 7.25/2.14 % (3068434)Peak memory usage: 90 MB
% 7.25/2.14 % (3068434)Instructions burned: 127 (million)
% 7.25/2.14 % (3068432)Instruction limit reached!
% 7.25/2.14 % (3068432)------------------------------
% 7.25/2.14 % (3068432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.25/2.14 % (3068432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.25/2.14 % (3068432)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068432)Termination reason: Instruction limit
% 7.25/2.14 % (3068432)Termination phase: Saturation
% 7.25/2.14 % (3068432)Time elapsed: 0.103 s
% 7.25/2.14 % (3068432)Peak memory usage: 90 MB
% 7.25/2.14 % (3068432)Instructions burned: 190 (million)
% 7.25/2.14 % (3068433)Instruction limit reached!
% 7.25/2.14 % (3068433)------------------------------
% 7.25/2.14 % (3068433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.25/2.14 % (3068433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.25/2.14 % (3068433)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068433)Termination reason: Instruction limit
% 7.25/2.14 % (3068433)Termination phase: Saturation
% 7.25/2.14 % (3068433)Time elapsed: 0.118 s
% 7.25/2.14 % (3068433)Peak memory usage: 90 MB
% 7.25/2.14 % (3068433)Instructions burned: 219 (million)
% 7.25/2.14 % (3068439)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2073128210:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 7.25/2.14 % (3068439)Instruction limit reached!
% 7.25/2.14 % (3068439)------------------------------
% 7.25/2.14 % (3068439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.25/2.14 % (3068439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.25/2.14 % (3068439)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068439)Termination reason: Instruction limit
% 7.25/2.14 % (3068439)Termination phase: Saturation
% 7.25/2.14 % (3068439)Time elapsed: 0.069 s
% 7.25/2.14 % (3068439)Peak memory usage: 90 MB
% 7.25/2.14 % (3068439)Instructions burned: 196 (million)
% 7.25/2.14 % (3068440)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1017438961:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 7.25/2.14 % (3068431)------------------------------
% 7.25/2.14 % (3068431)------------------------------
% 7.25/2.14 % (3068441)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=454772703:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 7.25/2.14 % (3068443)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=3951969667:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 7.25/2.14 % (3068440)Instruction limit reached!
% 7.25/2.14 % (3068440)------------------------------
% 7.25/2.14 % (3068440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.25/2.14 % (3068440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.25/2.14 % (3068440)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068440)Termination reason: Instruction limit
% 7.25/2.14 % (3068440)Termination phase: Saturation
% 7.25/2.14 % (3068440)Time elapsed: 0.098 s
% 7.25/2.14 % (3068440)Peak memory usage: 91 MB
% 7.25/2.14 % (3068440)Instructions burned: 158 (million)
% 7.25/2.14 % (3068443)Instruction limit reached!
% 7.25/2.14 % (3068443)------------------------------
% 7.25/2.14 % (3068443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.25/2.14 % (3068443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.25/2.14 % (3068443)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068443)Termination reason: Instruction limit
% 7.25/2.14 % (3068443)Termination phase: Saturation
% 7.25/2.14 % (3068443)Time elapsed: 0.034 s
% 7.25/2.14 % (3068443)Peak memory usage: 89 MB
% 7.25/2.14 % (3068443)Instructions burned: 106 (million)
% 7.25/2.14 % (3068445)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3217882583:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 7.25/2.14 % (3068449)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1081052880:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 7.25/2.14 % (3068445)Instruction limit reached!
% 7.25/2.14 % (3068445)------------------------------
% 7.25/2.14 % (3068445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.25/2.14 % (3068445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.25/2.14 % (3068445)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068445)Termination reason: Instruction limit
% 7.25/2.14 % (3068445)Termination phase: Saturation
% 7.25/2.14 % (3068445)Time elapsed: 0.070 s
% 7.25/2.14 % (3068445)Peak memory usage: 90 MB
% 7.25/2.14 % (3068445)Instructions burned: 108 (million)
% 7.25/2.14 % (3068448)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1584831692:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 7.25/2.14 % (3068453)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2402443942:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 7.25/2.14 % (3068448)Instruction limit reached!
% 7.25/2.14 % (3068448)------------------------------
% 7.25/2.14 % (3068448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.25/2.14 % (3068448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.25/2.14 % (3068448)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068448)Termination reason: Instruction limit
% 7.25/2.14 % (3068448)Termination phase: Saturation
% 7.25/2.14 % (3068448)Time elapsed: 0.144 s
% 7.25/2.14 % (3068448)Peak memory usage: 90 MB
% 7.25/2.14 % (3068448)Instructions burned: 242 (million)
% 7.25/2.14 % (3068453)Instruction limit reached!
% 7.25/2.14 % (3068453)------------------------------
% 7.25/2.14 % (3068453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.25/2.14 % (3068453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.25/2.14 % (3068453)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068453)Termination reason: Instruction limit
% 7.25/2.14 % (3068453)Termination phase: Saturation
% 7.25/2.14 % (3068453)Time elapsed: 0.090 s
% 7.25/2.14 % (3068453)Peak memory usage: 90 MB
% 7.25/2.14 % (3068453)Instructions burned: 135 (million)
% 7.25/2.14 % (3068455)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1778422822:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 7.25/2.14 % (3068456)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2508156009:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 7.25/2.14 % (3068417)First to succeed.
% 7.25/2.14 % (3068417)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3068412"
% 7.25/2.14 % (3068456)Instruction limit reached!
% 7.25/2.14 % (3068456)------------------------------
% 7.25/2.14 % (3068456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.25/2.14 % (3068456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.25/2.14 % (3068456)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068456)Termination reason: Instruction limit
% 7.25/2.14 % (3068456)Termination phase: Saturation
% 7.25/2.14 % (3068456)Time elapsed: 0.126 s
% 7.25/2.14 % (3068456)Peak memory usage: 91 MB
% 7.25/2.14 % (3068456)Instructions burned: 191 (million)
% 7.25/2.14 % (3068455)Instruction limit reached!
% 7.25/2.14 % (3068455)------------------------------
% 7.25/2.14 % (3068455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.25/2.14 % (3068455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.25/2.14 % (3068455)CaDiCaL version: 2.1.3
% 7.25/2.14 % (3068455)Termination reason: Instruction limit
% 7.25/2.14 % (3068455)Termination phase: Saturation
% 7.25/2.14 % (3068455)Time elapsed: 0.330 s
% 7.25/2.14 % (3068455)Peak memory usage: 95 MB
% 7.25/2.14 % (3068455)Instructions burned: 501 (million)
% 7.25/2.14 % (3068459)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3525497565:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 7.25/2.14 % (3068419)Also succeeded, but the first one will report.
% 7.25/2.14 % (3068417)Refutation found. Thanks to Tanya!
% 7.25/2.14 % SZS status Unsatisfiable for theBenchmark
% 7.25/2.14 % SZS output start Proof for theBenchmark
% See solution above
% 11.05/2.37 % (3068417)------------------------------
% 11.05/2.37 % (3068417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.37 % (3068417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.37 % (3068417)CaDiCaL version: 2.1.3
% 11.05/2.37 % (3068417)Termination reason: Refutation
% 11.05/2.37 % (3068417)Time elapsed: 1.113 s
% 11.05/2.37 % (3068417)Peak memory usage: 137 MB
% 11.05/2.37 % (3068417)Instructions burned: 1775 (million)
% 11.05/2.37 % (3068417)------------------------------
% 11.05/2.37 % (3068417)------------------------------
% 11.05/2.37 % (3068412)Success in time 1.521 s
% 11.05/2.37 % Vampire exiting
%------------------------------------------------------------------------------