%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT051-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 : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:36:49 PM UTC 2026
% Result : Unsatisfiable 14.18s 2.68s
% Output : Refutation 14.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 46
% Syntax : Number of formulae : 247 ( 97 unt; 32 def)
% Number of atoms : 1010 ( 315 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 1188 ( 425 ~; 759 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 15 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 5 prp; 0-3 aty)
% Number of functors : 45 ( 45 usr; 28 con; 0-6 aty)
% Number of variables : 420 ( 0 sgn 420 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f623,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__local__X2__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),hAPP(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(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__local__X2__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_2_3) ).
fof(f624,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(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),hAPP(v_F,X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X4 = X0
| X3 = X1
| X0 = X1
| X3 = X4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_2_2) ).
fof(f625,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(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,[],[f624]) ).
fof(f626,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__local__X2__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__local__X2__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),hAPP(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(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_2_1) ).
fof(f627,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(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),hAPP(v_F,X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X4 = X0
| X3 = X1
| X0 = X1
| X3 = X4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_2_0) ).
fof(f628,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(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(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,[],[f627]) ).
fof(f645,negated_conjecture,
c_in(c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,v_P____,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_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_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_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f646,negated_conjecture,
c_in(c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,v_P____,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_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_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_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_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_a____,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_c____,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_conjecture_1) ).
fof(f647,negated_conjecture,
v_a____ != v_b____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f649,negated_conjecture,
v_b____ != v_c____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f650,negated_conjecture,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f651,negated_conjecture,
! [X0] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f652,negated_conjecture,
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,v_P____,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_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_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_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_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_a____,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_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,v_P____,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_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_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_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f653,negated_conjecture,
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,v_P____,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_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_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_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,v_P____,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_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_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_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_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_a____,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_c____,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_8) ).
fof(f668,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(f669,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(c_COMBB(X0,X1,X2,X3,X4),X5) = hAPP(X0,hAPP(X1,X5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ATP__Linkup_OCOMBB__def_0) ).
fof(f747,definition,
sF0 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f748,plain,
tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(reorient_equations,[],[f747]) ).
fof(f749,definition,
sF1 = tc_fun(sF0,tc_bool),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f750,plain,
tc_fun(sF0,tc_bool) = sF1,
inference(reorient_equations,[],[f749]) ).
fof(f751,definition,
sF2 = tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f752,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF1) = sF2,
inference(reorient_equations,[],[f751]) ).
fof(f753,definition,
sF3 = tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f754,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF2) = sF3,
inference(reorient_equations,[],[f753]) ).
fof(f755,definition,
sF4 = c_COMBB(c_Arrow__Order__Mirabelle_Obelow,v_P____,sF1,sF3,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f756,plain,
c_COMBB(c_Arrow__Order__Mirabelle_Obelow,v_P____,sF1,sF3,tc_Arrow__Order__Mirabelle_Oindi) = sF4,
inference(reorient_equations,[],[f755]) ).
fof(f757,definition,
sF5 = c_COMBC(sF4,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f758,plain,
c_COMBC(sF4,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2) = sF5,
inference(reorient_equations,[],[f757]) ).
fof(f759,definition,
sF6 = c_COMBC(sF5,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF1),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f760,plain,
c_COMBC(sF5,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF1) = sF6,
inference(reorient_equations,[],[f759]) ).
fof(f761,definition,
sF7 = c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF6,sF1,sF3,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f762,plain,
c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF6,sF1,sF3,tc_Arrow__Order__Mirabelle_Oindi) = sF7,
inference(reorient_equations,[],[f761]) ).
fof(f763,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(f764,plain,
c_COMBC(sF7,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2) = sF8,
inference(reorient_equations,[],[f763]) ).
fof(f765,definition,
sF9 = c_COMBC(sF8,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF1),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f766,plain,
c_COMBC(sF8,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF1) = sF9,
inference(reorient_equations,[],[f765]) ).
fof(f767,definition,
sF10 = tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f768,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1) = sF10,
inference(reorient_equations,[],[f767]) ).
fof(f769,plain,
c_in(sF9,c_Arrow__Order__Mirabelle_OProf,sF10),
inference(definition_folding,[],[f645,f768,f750,f748,f766,f750,f748,f764,f752,f750,f748,f762,f754,f752,f750,f748,f750,f748,f760,f750,f748,f758,f752,f750,f748,f756,f754,f752,f750,f748,f750,f748]) ).
fof(f770,definition,
sF11 = c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF9,sF1,sF3,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f771,plain,
c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF9,sF1,sF3,tc_Arrow__Order__Mirabelle_Oindi) = sF11,
inference(reorient_equations,[],[f770]) ).
fof(f772,definition,
sF12 = c_COMBC(sF11,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f773,plain,
c_COMBC(sF11,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF2) = sF12,
inference(reorient_equations,[],[f772]) ).
fof(f774,definition,
sF13 = c_COMBC(sF12,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF1),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f775,plain,
c_COMBC(sF12,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF1) = sF13,
inference(reorient_equations,[],[f774]) ).
fof(f776,plain,
c_in(sF13,c_Arrow__Order__Mirabelle_OProf,sF10),
inference(definition_folding,[],[f646,f768,f750,f748,f775,f750,f748,f773,f752,f750,f748,f771,f754,f752,f750,f748,f750,f748,f766,f750,f748,f764,f752,f750,f748,f762,f754,f752,f750,f748,f750,f748,f760,f750,f748,f758,f752,f750,f748,f756,f754,f752,f750,f748,f750,f748]) ).
fof(f777,definition,
sF14 = c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f778,plain,
c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF14,
inference(reorient_equations,[],[f777]) ).
fof(f779,definition,
! [X0] : sF15(X0) = hAPP(v_P____,X0),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f780,plain,
! [X0] : hAPP(v_P____,X0) = sF15(X0),
inference(reorient_equations,[],[f779]) ).
fof(f781,definition,
! [X0] : sF16(X0) = hAPP(c_Arrow__Order__Mirabelle_Obelow,sF15(X0)),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f782,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,sF15(X0)) = sF16(X0),
inference(reorient_equations,[],[f781]) ).
fof(f783,definition,
! [X0] : sF17(X0) = hAPP(sF16(X0),v_c____),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f784,plain,
! [X0] : hAPP(sF16(X0),v_c____) = sF17(X0),
inference(reorient_equations,[],[f783]) ).
fof(f785,definition,
! [X0] : sF18(X0) = hAPP(sF17(X0),v_b____),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f786,plain,
! [X0] : hAPP(sF17(X0),v_b____) = sF18(X0),
inference(reorient_equations,[],[f785]) ).
fof(f787,definition,
! [X0] : sF19(X0) = hAPP(c_Arrow__Order__Mirabelle_Obelow,sF18(X0)),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f788,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,sF18(X0)) = sF19(X0),
inference(reorient_equations,[],[f787]) ).
fof(f789,definition,
! [X0] : sF20(X0) = hAPP(sF19(X0),v_b____),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f790,plain,
! [X0] : hAPP(sF19(X0),v_b____) = sF20(X0),
inference(reorient_equations,[],[f789]) ).
fof(f791,definition,
! [X0] : sF21(X0) = hAPP(sF20(X0),v_a____),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f792,plain,
! [X0] : hAPP(sF20(X0),v_a____) = sF21(X0),
inference(reorient_equations,[],[f791]) ).
fof(f793,definition,
! [X0] : sF22(X0) = hAPP(c_Arrow__Order__Mirabelle_Obelow,sF21(X0)),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f794,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,sF21(X0)) = sF22(X0),
inference(reorient_equations,[],[f793]) ).
fof(f795,definition,
! [X0] : sF23(X0) = hAPP(sF22(X0),v_a____),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f796,plain,
! [X0] : hAPP(sF22(X0),v_a____) = sF23(X0),
inference(reorient_equations,[],[f795]) ).
fof(f797,definition,
! [X0] : sF24(X0) = hAPP(sF23(X0),v_c____),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f798,plain,
! [X0] : hAPP(sF23(X0),v_c____) = sF24(X0),
inference(reorient_equations,[],[f797]) ).
fof(f799,definition,
sF25 = c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f800,plain,
c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF25,
inference(reorient_equations,[],[f799]) ).
fof(f801,plain,
! [X0] :
( ~ c_in(sF25,sF21(X0),sF0)
| c_in(sF14,sF24(X0),sF0) ),
inference(definition_folding,[],[f650,f748,f792,f790,f788,f786,f784,f782,f780,f800,f748,f798,f796,f794,f792,f790,f788,f786,f784,f782,f780,f778]) ).
fof(f802,plain,
! [X0] :
( ~ c_in(sF14,sF24(X0),sF0)
| c_in(sF25,sF21(X0),sF0) ),
inference(definition_folding,[],[f651,f748,f798,f796,f794,f792,f790,f788,f786,f784,f782,f780,f778,f748,f792,f790,f788,f786,f784,f782,f780,f800]) ).
fof(f803,definition,
sF26 = hAPP(v_F,sF13),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f804,plain,
hAPP(v_F,sF13) = sF26,
inference(reorient_equations,[],[f803]) ).
fof(f805,definition,
sF27 = hAPP(v_F,sF9),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f806,plain,
hAPP(v_F,sF9) = sF27,
inference(reorient_equations,[],[f805]) ).
fof(f807,plain,
( ~ c_in(sF14,sF26,sF0)
| ~ c_in(sF25,sF27,sF0) ),
inference(definition_folding,[],[f652,f748,f806,f766,f750,f748,f764,f752,f750,f748,f762,f754,f752,f750,f748,f750,f748,f760,f750,f748,f758,f752,f750,f748,f756,f754,f752,f750,f748,f750,f748,f800,f748,f804,f775,f750,f748,f773,f752,f750,f748,f771,f754,f752,f750,f748,f750,f748,f766,f750,f748,f764,f752,f750,f748,f762,f754,f752,f750,f748,f750,f748,f760,f750,f748,f758,f752,f750,f748,f756,f754,f752,f750,f748,f750,f748,f778]) ).
fof(f808,plain,
( c_in(sF25,sF27,sF0)
| c_in(sF14,sF26,sF0) ),
inference(definition_folding,[],[f653,f748,f804,f775,f750,f748,f773,f752,f750,f748,f771,f754,f752,f750,f748,f750,f748,f766,f750,f748,f764,f752,f750,f748,f762,f754,f752,f750,f748,f750,f748,f760,f750,f748,f758,f752,f750,f748,f756,f754,f752,f750,f748,f750,f748,f778,f748,f806,f766,f750,f748,f764,f752,f750,f748,f762,f754,f752,f750,f748,f750,f748,f760,f750,f748,f758,f752,f750,f748,f756,f754,f752,f750,f748,f750,f748,f800]) ).
fof(f823,definition,
( spl28_1
<=> c_in(sF14,sF26,sF0) ),
introduced(definition,[new_symbols(definition,[spl28_1])],[avatar_definition]) ).
fof(f824,plain,
( ~ c_in(sF14,sF26,sF0)
| spl28_1 ),
inference(avatar_component_clause,[],[f823]) ).
fof(f825,plain,
( c_in(sF14,sF26,sF0)
| ~ spl28_1 ),
inference(avatar_component_clause,[],[f823]) ).
fof(f827,definition,
( spl28_2
<=> c_in(sF25,sF27,sF0) ),
introduced(definition,[new_symbols(definition,[spl28_2])],[avatar_definition]) ).
fof(f828,plain,
( ~ c_in(sF25,sF27,sF0)
| spl28_2 ),
inference(avatar_component_clause,[],[f827]) ).
fof(f829,plain,
( c_in(sF25,sF27,sF0)
| ~ spl28_2 ),
inference(avatar_component_clause,[],[f827]) ).
fof(f830,plain,
( spl28_1
| spl28_2 ),
inference(avatar_split_clause,[],[f808,f827,f823]) ).
fof(f831,plain,
( ~ spl28_2
| ~ spl28_1 ),
inference(avatar_split_clause,[],[f807,f823,f827]) ).
fof(f885,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(sF9,X0)) = hAPP(sF11,X0),
inference(superposition,[],[f669,f771]) ).
fof(f886,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(sF6,X0)) = hAPP(sF7,X0),
inference(superposition,[],[f669,f762]) ).
fof(f887,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)) = hAPP(sF4,X0),
inference(superposition,[],[f669,f756]) ).
fof(f888,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,sF15(X0)) = hAPP(sF4,X0),
inference(forward_demodulation,[],[f887,f780]) ).
fof(f889,plain,
! [X0] : sF16(X0) = hAPP(sF4,X0),
inference(forward_demodulation,[],[f888,f782]) ).
fof(f890,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF25,hAPP(v_F,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3
| v_b____ = v_c____ ),
inference(superposition,[],[f625,f800]) ).
fof(f901,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF25,hAPP(v_F,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f890,f649]) ).
fof(f907,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f901,f748]) ).
fof(f913,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f907,f748]) ).
fof(f919,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f913,f748]) ).
fof(f924,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f919,f748]) ).
fof(f929,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF0,tc_bool)))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f924,f748]) ).
fof(f934,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f929,f750]) ).
fof(f939,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f934,f768]) ).
fof(f944,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF0,tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f939,f748]) ).
fof(f949,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f944,f750]) ).
fof(f967,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f949,f768]) ).
fof(f969,plain,
! [X0,X1] :
( ~ c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(sF25,hAPP(v_F,X1),sF0)
| ~ c_in(sF25,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| v_b____ = v_c____
| v_a____ = v_b____
| v_a____ = v_b____ ),
inference(superposition,[],[f967,f778]) ).
fof(f973,plain,
! [X0,X1] :
( ~ c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(sF25,hAPP(v_F,X1),sF0)
| ~ c_in(sF25,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| v_b____ = v_c____
| v_a____ = v_b____ ),
inference(duplicate_literal_removal,[],[f969]) ).
fof(f975,plain,
! [X0,X1] :
( ~ c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(sF25,hAPP(v_F,X1),sF0)
| ~ c_in(sF25,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| v_a____ = v_b____ ),
inference(forward_subsumption_resolution,[],[f973,f649]) ).
fof(f977,plain,
! [X0,X1] :
( ~ c_in(sF25,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(sF25,hAPP(v_F,X1),sF0)
| ~ c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0) ),
inference(forward_subsumption_resolution,[],[f975,f647]) ).
fof(f1090,plain,
! [X0] : hAPP(sF9,X0) = hAPP(hAPP(sF8,X0),v_a____),
inference(superposition,[],[f668,f766]) ).
fof(f1091,plain,
! [X0] : hAPP(hAPP(sF12,X0),v_c____) = hAPP(sF13,X0),
inference(superposition,[],[f668,f775]) ).
fof(f1102,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__local__X2__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(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(X0,X2,X3,X4,X5)),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(v_F,X1),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__local__X2__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_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,[],[f623,f668]) ).
fof(f1104,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__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(X0,X2,X3,X4,X5)),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(v_F,X1),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__local__X2__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_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,[],[f1102,f748]) ).
fof(f1106,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(v_F,c_COMBC(X0,X2,X3,X4,X5)),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF0)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),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__local__X2__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_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,[],[f1104,f748]) ).
fof(f1108,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(v_F,X1),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(X0,X2,X3,X4,X5)),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF0)
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__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_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,[],[f1106,f748]) ).
fof(f1110,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__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF0)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(X0,X2,X3,X4,X5)),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF0)
| ~ 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,[],[f1108,f748]) ).
fof(f1112,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(sF0,tc_bool)))
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF0)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(X0,X2,X3,X4,X5)),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF0)
| ~ 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,[],[f1110,f748]) ).
fof(f1114,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,sF1))
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF0)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(X0,X2,X3,X4,X5)),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF0)
| ~ 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,[],[f1112,f750]) ).
fof(f1116,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,sF10)
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF0)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(X0,X2,X3,X4,X5)),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF0)
| ~ 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,[],[f1114,f768]) ).
fof(f1118,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(sF0,tc_bool)))
| ~ c_in(c_COMBC(X0,X2,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF0)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(X0,X2,X3,X4,X5)),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF0)
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(forward_demodulation,[],[f1116,f748]) ).
fof(f1120,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,sF1))
| ~ c_in(c_COMBC(X0,X2,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF0)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(X0,X2,X3,X4,X5)),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(X0,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF0)
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(forward_demodulation,[],[f1118,f750]) ).
fof(f1122,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__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),X2),sF0)
| ~ c_in(c_COMBC(X0,X2,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,c_COMBC(X0,X2,X3,X4,X5),X6,X7,X8,X9)),sF0)
| c_in(c_Pair(X6,X8,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(c_Pair(X7,X9,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,c_COMBC(X0,X2,X3,X4,X5)),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| X7 = X8
| X6 = X9
| X7 = X9
| X6 = X8 ),
inference(forward_demodulation,[],[f1120,f768]) ).
fof(f1367,plain,
! [X0] : hAPP(hAPP(sF4,X0),v_c____) = hAPP(sF5,X0),
inference(superposition,[],[f668,f758]) ).
fof(f1368,plain,
! [X0] : hAPP(sF16(X0),v_c____) = hAPP(sF5,X0),
inference(forward_demodulation,[],[f1367,f889]) ).
fof(f1370,plain,
! [X0] : sF17(X0) = hAPP(sF5,X0),
inference(forward_demodulation,[],[f1368,f784]) ).
fof(f1437,plain,
! [X0] : hAPP(sF6,X0) = hAPP(hAPP(sF5,X0),v_b____),
inference(superposition,[],[f668,f760]) ).
fof(f1438,plain,
! [X0] : hAPP(sF17(X0),v_b____) = hAPP(sF6,X0),
inference(forward_demodulation,[],[f1437,f1370]) ).
fof(f1440,plain,
! [X0] : sF18(X0) = hAPP(sF6,X0),
inference(forward_demodulation,[],[f1438,f786]) ).
fof(f1450,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,sF18(X0)) = hAPP(sF7,X0),
inference(superposition,[],[f886,f1440]) ).
fof(f1483,plain,
! [X0] : sF19(X0) = hAPP(sF7,X0),
inference(forward_demodulation,[],[f1450,f788]) ).
fof(f1672,plain,
! [X0] : hAPP(sF8,X0) = hAPP(hAPP(sF7,X0),v_b____),
inference(superposition,[],[f668,f764]) ).
fof(f1673,plain,
! [X0] : hAPP(sF19(X0),v_b____) = hAPP(sF8,X0),
inference(forward_demodulation,[],[f1672,f1483]) ).
fof(f1675,plain,
! [X0] : sF20(X0) = hAPP(sF8,X0),
inference(forward_demodulation,[],[f1673,f790]) ).
fof(f1742,plain,
! [X0] : hAPP(sF12,X0) = hAPP(hAPP(sF11,X0),v_a____),
inference(superposition,[],[f668,f773]) ).
fof(f1958,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(sF12,v_sko__local__X2__1(X2,sF13,X3,X0,X4,X1)),v_c____),sF0)
| ~ c_in(sF13,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X2,sF13,X3,X0,X4,X1)),sF0)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X2),sF0)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,sF13),sF0)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,sF10)
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(superposition,[],[f1122,f775]) ).
fof(f1974,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(sF12,v_sko__local__X2__1(X2,sF13,X3,X0,X4,X1)),v_c____),sF0)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X2,sF13,X3,X0,X4,X1)),sF0)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X2),sF0)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,sF13),sF0)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,sF10)
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(forward_subsumption_resolution,[],[f1958,f776]) ).
fof(f1978,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF13,v_sko__local__X2__1(X2,sF13,X3,X0,X4,X1)),sF0)
| ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X2,sF13,X3,X0,X4,X1)),sF0)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X2),sF0)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,sF13),sF0)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,sF10)
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(forward_demodulation,[],[f1974,f1091]) ).
fof(f1980,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X2__1(X2,sF13,X3,X0,X4,X1)),sF0)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF13,v_sko__local__X2__1(X2,sF13,X3,X0,X4,X1)),sF0)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF26,sF0)
| c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X2),sF0)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,sF10)
| X0 = X4
| X1 = X3
| X0 = X1
| X3 = X4 ),
inference(forward_demodulation,[],[f1978,f804]) ).
fof(f1982,plain,
! [X2,X0,X1] :
( ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,sF13,v_b____,X1,v_c____,X2)),sF0)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF13,v_sko__local__X2__1(X0,sF13,v_b____,X1,v_c____,X2)),sF0)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF26,sF0)
| c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_c____ = X1
| v_b____ = X2
| X1 = X2
| v_b____ = v_c____ ),
inference(superposition,[],[f1980,f800]) ).
fof(f1993,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF13,v_sko__local__X2__1(X0,sF13,v_b____,X1,v_c____,X2)),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,sF13,v_b____,X1,v_c____,X2)),sF0)
| ~ c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF26,sF0)
| c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_c____ = X1
| v_b____ = X2
| X1 = X2 ),
inference(forward_subsumption_resolution,[],[f1982,f649]) ).
fof(f2007,plain,
! [X0] :
( ~ c_in(sF14,hAPP(sF13,v_sko__local__X2__1(X0,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF14,sF26,sF0)
| c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_b____ = v_c____
| v_a____ = v_b____
| v_a____ = v_b____ ),
inference(superposition,[],[f1993,f778]) ).
fof(f2008,plain,
! [X0] :
( ~ c_in(sF14,hAPP(sF13,v_sko__local__X2__1(X0,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF14,sF26,sF0)
| c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_b____ = v_c____
| v_a____ = v_b____ ),
inference(duplicate_literal_removal,[],[f2007]) ).
fof(f2010,plain,
( ! [X0] :
( ~ c_in(sF14,hAPP(sF13,v_sko__local__X2__1(X0,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_b____ = v_c____
| v_a____ = v_b____ )
| ~ spl28_1 ),
inference(forward_subsumption_resolution,[],[f2008,f825]) ).
fof(f2011,plain,
( ! [X0] :
( ~ c_in(sF14,hAPP(sF13,v_sko__local__X2__1(X0,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_a____ = v_b____ )
| ~ spl28_1 ),
inference(forward_subsumption_resolution,[],[f2010,f649]) ).
fof(f2012,plain,
( ! [X0] :
( ~ c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF14,hAPP(sF13,v_sko__local__X2__1(X0,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10) )
| ~ spl28_1 ),
inference(forward_subsumption_resolution,[],[f2011,f647]) ).
fof(f2334,plain,
! [X2,X3,X0,X1] :
( c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF14,hAPP(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(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_b____ = X3
| v_a____ = X2
| v_a____ = v_b____
| X2 = X3 ),
inference(superposition,[],[f626,f778]) ).
fof(f2378,plain,
! [X2,X3,X0,X1] :
( c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF14,hAPP(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(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_b____ = X3
| v_a____ = X2
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f2334,f647]) ).
fof(f2400,plain,
! [X2,X3,X0,X1] :
( c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF14,hAPP(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(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_b____ = X3
| v_a____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f2378,f748]) ).
fof(f2422,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| ~ c_in(sF14,hAPP(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(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_b____ = X3
| v_a____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f2400,f748]) ).
fof(f2444,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF14,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(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_b____ = X3
| v_a____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f2422,f748]) ).
fof(f2464,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF14,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| ~ 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_b____ = X3
| v_a____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f2444,f748]) ).
fof(f2484,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF0,tc_bool)))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF14,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| ~ 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_b____ = X3
| v_a____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f2464,f748]) ).
fof(f2504,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF14,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| ~ 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_b____ = X3
| v_a____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f2484,f750]) ).
fof(f2518,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF14,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| ~ 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_b____ = X3
| v_a____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f2504,f768]) ).
fof(f2532,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF0,tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF14,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| v_b____ = X3
| v_a____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f2518,f748]) ).
fof(f2546,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF14,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| v_b____ = X3
| v_a____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f2532,f750]) ).
fof(f2550,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,X2,v_b____,X3,v_a____)),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_b____ = X3
| v_a____ = X2
| X2 = X3 ),
inference(forward_demodulation,[],[f2546,f768]) ).
fof(f2659,plain,
! [X0,X1] :
( c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF14,hAPP(v_F,X1),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_b____ = v_c____
| v_a____ = v_b____
| v_b____ = v_c____ ),
inference(superposition,[],[f2550,f800]) ).
fof(f2672,plain,
! [X0,X1] :
( c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF14,hAPP(v_F,X1),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_b____ = v_c____
| v_a____ = v_b____ ),
inference(duplicate_literal_removal,[],[f2659]) ).
fof(f2695,plain,
! [X0,X1] :
( c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF14,hAPP(v_F,X1),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_a____ = v_b____ ),
inference(forward_subsumption_resolution,[],[f2672,f649]) ).
fof(f2706,plain,
! [X0,X1] :
( c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(sF14,hAPP(v_F,X1),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10) ),
inference(forward_subsumption_resolution,[],[f2695,f647]) ).
fof(f3013,plain,
! [X2,X3,X0,X1] :
( c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF25,hAPP(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(v_F,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3
| v_b____ = v_c____ ),
inference(superposition,[],[f628,f800]) ).
fof(f3059,plain,
! [X2,X3,X0,X1] :
( c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF25,hAPP(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(v_F,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_subsumption_resolution,[],[f3013,f649]) ).
fof(f3081,plain,
! [X2,X3,X0,X1] :
( c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF25,hAPP(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(v_F,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f3059,f748]) ).
fof(f3103,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(sF25,hAPP(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(v_F,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f3081,f748]) ).
fof(f3125,plain,
! [X2,X3,X0,X1] :
( ~ c_in(sF25,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f3103,f748]) ).
fof(f3145,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f3125,f748]) ).
fof(f3165,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF0,tc_bool)))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f3145,f748]) ).
fof(f3185,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1))
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f3165,f750]) ).
fof(f3199,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f3185,f768]) ).
fof(f3213,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF0,tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f3199,f748]) ).
fof(f3227,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f3213,f750]) ).
fof(f3231,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(sF25,hAPP(X0,v_sko__local__X2__1(X0,X1,v_b____,X2,v_c____,X3)),sF0)
| c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X1),sF0)
| ~ c_in(sF25,hAPP(v_F,X0),sF0)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_c____ = X2
| v_b____ = X3
| X2 = X3 ),
inference(forward_demodulation,[],[f3227,f768]) ).
fof(f3255,plain,
! [X0,X1] :
( c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(v_F,X1),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_b____ = v_c____
| v_a____ = v_b____
| v_a____ = v_b____ ),
inference(superposition,[],[f3231,f778]) ).
fof(f3266,plain,
! [X0,X1] :
( c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(v_F,X1),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_b____ = v_c____
| v_a____ = v_b____ ),
inference(duplicate_literal_removal,[],[f3255]) ).
fof(f3290,plain,
! [X0,X1] :
( c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(v_F,X1),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10)
| v_a____ = v_b____ ),
inference(forward_subsumption_resolution,[],[f3266,f649]) ).
fof(f3303,plain,
! [X0,X1] :
( c_in(sF25,hAPP(X1,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(X1,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(v_F,X1),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF10) ),
inference(forward_subsumption_resolution,[],[f3290,f647]) ).
fof(f5089,plain,
! [X0] : hAPP(sF20(X0),v_a____) = hAPP(sF9,X0),
inference(superposition,[],[f1090,f1675]) ).
fof(f5094,plain,
! [X0] : sF21(X0) = hAPP(sF9,X0),
inference(forward_demodulation,[],[f5089,f792]) ).
fof(f5095,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,sF21(X0)) = hAPP(sF11,X0),
inference(superposition,[],[f885,f5094]) ).
fof(f5121,plain,
! [X0] :
( c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(v_F,sF9),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(sF9,c_Arrow__Order__Mirabelle_OProf,sF10) ),
inference(superposition,[],[f3303,f5094]) ).
fof(f5122,plain,
! [X0] :
( c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(v_F,sF9),sF0)
| ~ c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(sF9,c_Arrow__Order__Mirabelle_OProf,sF10) ),
inference(superposition,[],[f2706,f5094]) ).
fof(f5124,plain,
! [X0] :
( ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(sF9,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ c_in(sF25,hAPP(v_F,sF9),sF0)
| ~ c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0) ),
inference(superposition,[],[f977,f5094]) ).
fof(f5134,plain,
( ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF14,hAPP(sF13,v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(v_F,sF9),sF0)
| ~ c_in(sF9,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ spl28_1 ),
inference(superposition,[],[f2012,f5094]) ).
fof(f5282,plain,
( ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF14,hAPP(sF13,v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(v_F,sF9),sF0)
| ~ spl28_1 ),
inference(forward_subsumption_resolution,[],[f5134,f769]) ).
fof(f5292,plain,
! [X0] :
( ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(v_F,sF9),sF0)
| ~ c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0) ),
inference(forward_subsumption_resolution,[],[f5124,f769]) ).
fof(f5294,plain,
! [X0] :
( c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,hAPP(v_F,sF9),sF0)
| ~ c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10) ),
inference(forward_subsumption_resolution,[],[f5122,f769]) ).
fof(f5295,plain,
! [X0] :
( c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,hAPP(v_F,sF9),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10) ),
inference(forward_subsumption_resolution,[],[f5121,f769]) ).
fof(f5310,plain,
! [X0] : sF22(X0) = hAPP(sF11,X0),
inference(forward_demodulation,[],[f5095,f794]) ).
fof(f5376,plain,
( c_in(sF25,sF27,sF0)
| ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF14,hAPP(sF13,v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ spl28_1 ),
inference(forward_demodulation,[],[f5282,f806]) ).
fof(f5386,plain,
! [X0] :
( ~ c_in(sF25,sF27,sF0)
| ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0) ),
inference(forward_demodulation,[],[f5292,f806]) ).
fof(f5415,plain,
( ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF14,hAPP(sF13,v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ spl28_1
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f5376,f828]) ).
fof(f5446,definition,
( spl28_50
<=> c_in(sF14,hAPP(sF13,v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0) ),
introduced(definition,[new_symbols(definition,[spl28_50])],[avatar_definition]) ).
fof(f5447,plain,
( c_in(sF14,hAPP(sF13,v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ spl28_50 ),
inference(avatar_component_clause,[],[f5446]) ).
fof(f5448,plain,
( ~ c_in(sF14,hAPP(sF13,v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| spl28_50 ),
inference(avatar_component_clause,[],[f5446]) ).
fof(f5450,definition,
( spl28_51
<=> c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0) ),
introduced(definition,[new_symbols(definition,[spl28_51])],[avatar_definition]) ).
fof(f5451,plain,
( c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ spl28_51 ),
inference(avatar_component_clause,[],[f5450]) ).
fof(f5452,plain,
( ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| spl28_51 ),
inference(avatar_component_clause,[],[f5450]) ).
fof(f5453,plain,
( ~ spl28_50
| ~ spl28_51
| ~ spl28_1
| spl28_2 ),
inference(avatar_split_clause,[],[f5415,f827,f823,f5450,f5446]) ).
fof(f5521,plain,
! [X0] : hAPP(sF22(X0),v_a____) = hAPP(sF12,X0),
inference(superposition,[],[f1742,f5310]) ).
fof(f5972,plain,
! [X0] : sF23(X0) = hAPP(sF12,X0),
inference(forward_demodulation,[],[f5521,f796]) ).
fof(f6111,plain,
! [X0] : hAPP(sF23(X0),v_c____) = hAPP(sF13,X0),
inference(superposition,[],[f1091,f5972]) ).
fof(f6562,plain,
! [X0] : sF24(X0) = hAPP(sF13,X0),
inference(forward_demodulation,[],[f6111,f798]) ).
fof(f7302,plain,
! [X0] :
( c_in(sF25,sF27,sF0)
| c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10) ),
inference(forward_demodulation,[],[f5294,f806]) ).
fof(f7303,plain,
! [X0] :
( ~ c_in(sF25,sF27,sF0)
| c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10) ),
inference(forward_demodulation,[],[f5295,f806]) ).
fof(f7311,plain,
( ! [X0] :
( ~ c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0) )
| ~ spl28_2 ),
inference(forward_subsumption_resolution,[],[f5386,f829]) ).
fof(f7359,plain,
( ! [X0] :
( c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10) )
| ~ spl28_2 ),
inference(forward_subsumption_resolution,[],[f7303,f829]) ).
fof(f7558,plain,
( ~ c_in(sF14,sF24(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF13,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(sF14,hAPP(v_F,sF13),sF0)
| ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ spl28_2 ),
inference(superposition,[],[f7311,f6562]) ).
fof(f7744,plain,
( c_in(sF14,sF24(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(v_F,sF13),sF0)
| ~ c_in(sF13,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ spl28_2 ),
inference(superposition,[],[f7359,f6562]) ).
fof(f7746,plain,
( c_in(sF14,sF24(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(v_F,sF13),sF0)
| ~ c_in(sF13,c_Arrow__Order__Mirabelle_OProf,sF10)
| ~ spl28_2 ),
inference(forward_subsumption_resolution,[],[f7744,f801]) ).
fof(f7748,plain,
( c_in(sF14,sF24(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF14,hAPP(v_F,sF13),sF0)
| ~ spl28_2 ),
inference(forward_subsumption_resolution,[],[f7746,f776]) ).
fof(f7750,plain,
( c_in(sF14,sF26,sF0)
| c_in(sF14,sF24(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ spl28_2 ),
inference(forward_demodulation,[],[f7748,f804]) ).
fof(f7752,plain,
( c_in(sF14,sF24(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| spl28_1
| ~ spl28_2 ),
inference(forward_subsumption_resolution,[],[f7750,f824]) ).
fof(f7755,plain,
( c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| spl28_1
| ~ spl28_2 ),
inference(resolution,[],[f7752,f802]) ).
fof(f7756,plain,
( $false
| spl28_1
| ~ spl28_2
| spl28_51 ),
inference(forward_subsumption_resolution,[],[f7755,f5452]) ).
fof(f7757,plain,
( spl28_1
| ~ spl28_2
| spl28_51 ),
inference(avatar_contradiction_clause,[],[f7756]) ).
fof(f7758,plain,
( ~ c_in(sF13,c_Arrow__Order__Mirabelle_OProf,sF10)
| c_in(sF14,hAPP(v_F,sF13),sF0)
| ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ spl28_2 ),
inference(forward_subsumption_resolution,[],[f7558,f801]) ).
fof(f7759,plain,
( c_in(sF14,hAPP(v_F,sF13),sF0)
| ~ c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ spl28_2 ),
inference(forward_subsumption_resolution,[],[f7758,f776]) ).
fof(f7760,plain,
( c_in(sF14,hAPP(v_F,sF13),sF0)
| ~ spl28_2
| ~ spl28_51 ),
inference(forward_subsumption_resolution,[],[f7759,f5451]) ).
fof(f7761,plain,
( c_in(sF14,sF26,sF0)
| ~ spl28_2
| ~ spl28_51 ),
inference(forward_demodulation,[],[f7760,f804]) ).
fof(f7762,plain,
( $false
| spl28_1
| ~ spl28_2
| ~ spl28_51 ),
inference(forward_subsumption_resolution,[],[f7761,f824]) ).
fof(f7763,plain,
( spl28_1
| ~ spl28_2
| ~ spl28_51 ),
inference(avatar_contradiction_clause,[],[f7762]) ).
fof(f7764,plain,
( ~ c_in(sF14,sF24(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| spl28_50 ),
inference(forward_demodulation,[],[f5448,f6562]) ).
fof(f7773,plain,
( ! [X0] :
( c_in(sF14,hAPP(X0,v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,sF21(v_sko__local__X2__1(sF9,X0,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF14,hAPP(v_F,X0),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,sF10) )
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f7302,f828]) ).
fof(f8278,plain,
( c_in(sF14,sF24(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF14,hAPP(v_F,sF13),sF0)
| ~ c_in(sF13,c_Arrow__Order__Mirabelle_OProf,sF10)
| spl28_2 ),
inference(superposition,[],[f7773,f6562]) ).
fof(f8280,plain,
( c_in(sF14,sF24(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ c_in(sF14,hAPP(v_F,sF13),sF0)
| ~ c_in(sF13,c_Arrow__Order__Mirabelle_OProf,sF10)
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f8278,f801]) ).
fof(f8281,plain,
( ~ c_in(sF14,hAPP(v_F,sF13),sF0)
| ~ c_in(sF13,c_Arrow__Order__Mirabelle_OProf,sF10)
| spl28_2
| spl28_50 ),
inference(forward_subsumption_resolution,[],[f8280,f7764]) ).
fof(f8282,plain,
( ~ c_in(sF14,hAPP(v_F,sF13),sF0)
| spl28_2
| spl28_50 ),
inference(forward_subsumption_resolution,[],[f8281,f776]) ).
fof(f8283,plain,
( ~ c_in(sF14,sF26,sF0)
| spl28_2
| spl28_50 ),
inference(forward_demodulation,[],[f8282,f804]) ).
fof(f8284,plain,
( $false
| ~ spl28_1
| spl28_2
| spl28_50 ),
inference(forward_subsumption_resolution,[],[f8283,f825]) ).
fof(f8285,plain,
( ~ spl28_1
| spl28_2
| spl28_50 ),
inference(avatar_contradiction_clause,[],[f8284]) ).
fof(f8286,plain,
( c_in(sF14,sF24(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ spl28_50 ),
inference(forward_demodulation,[],[f5447,f6562]) ).
fof(f8288,plain,
( c_in(sF25,sF21(v_sko__local__X2__1(sF9,sF13,v_b____,v_b____,v_c____,v_a____)),sF0)
| ~ spl28_50 ),
inference(resolution,[],[f8286,f802]) ).
fof(f8289,plain,
( $false
| ~ spl28_50
| spl28_51 ),
inference(forward_subsumption_resolution,[],[f8288,f5452]) ).
fof(f8290,plain,
( ~ spl28_50
| spl28_51 ),
inference(avatar_contradiction_clause,[],[f8289]) ).
cnf(s1,plain,
( spl28_1
| spl28_2 ),
inference(sat_conversion,[],[f830]) ).
cnf(s2,plain,
( ~ spl28_1
| ~ spl28_2 ),
inference(sat_conversion,[],[f831]) ).
cnf(s41,plain,
( ~ spl28_1
| spl28_2
| ~ spl28_50
| ~ spl28_51 ),
inference(sat_conversion,[],[f5453]) ).
cnf(s247,plain,
( spl28_1
| ~ spl28_2
| spl28_51 ),
inference(sat_conversion,[],[f7757]) ).
cnf(s248,plain,
( spl28_1
| ~ spl28_2
| ~ spl28_51 ),
inference(sat_conversion,[],[f7763]) ).
cnf(s253,plain,
( ~ spl28_1
| spl28_2
| spl28_50 ),
inference(sat_conversion,[],[f8285]) ).
cnf(s254,plain,
( ~ spl28_50
| spl28_51 ),
inference(sat_conversion,[],[f8290]) ).
cnf(s255,plain,
( ~ spl28_2
| spl28_1 ),
inference(rat,[],[s247,s248]) ).
cnf(s256,plain,
spl28_1,
inference(rat,[],[s255,s1]) ).
cnf(s257,plain,
~ spl28_2,
inference(rat,[],[s2,s256]) ).
cnf(s258,plain,
spl28_50,
inference(rat,[],[s253,s256,s257]) ).
cnf(s260,plain,
spl28_51,
inference(rat,[],[s254,s258]) ).
cnf(s261,plain,
$false,
inference(rat,[],[s41,s257,s256,s260,s258]) ).
fof(f8291,plain,
$false,
inference(avatar_sat_refutation,[],[s261]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT051-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.37 % Computer : n013.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 23:33:37 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.13/1.90 % (667635)Input is clausal, will run a generic CNF schedule.
% 7.13/1.90 % (667643)lrs+10_1_sil=8000:sp=occurrence:random_seed=3946251511:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.13/1.90 % (667640)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=3756707834:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.13/1.90 % (667645)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1024874658:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.13/1.90 % (667641)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3120513381:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.13/1.90 % (667642)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2946120206:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.13/1.90 % (667646)dis-21_1_sil=8000:lcm=predicate:random_seed=135983263: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)
% 7.13/1.90 % (667644)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=484973106:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.13/1.90 % (667643)Instruction limit reached!
% 7.13/1.90 % (667643)------------------------------
% 7.13/1.90 % (667643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.90 % (667643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.90 % (667643)CaDiCaL version: 2.1.3
% 7.13/1.90 % (667643)Termination reason: Instruction limit
% 7.13/1.90 % (667643)Termination phase: Saturation
% 7.13/1.90 % (667643)Time elapsed: 0.063 s
% 7.13/1.90 % (667643)Peak memory usage: 89 MB
% 7.13/1.90 % (667643)Instructions burned: 108 (million)
% 7.13/1.90 % (667646)Instruction limit reached!
% 7.13/1.90 % (667646)------------------------------
% 7.13/1.90 % (667646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.90 % (667646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.90 % (667646)CaDiCaL version: 2.1.3
% 7.13/1.90 % (667646)Termination reason: Instruction limit
% 7.13/1.90 % (667646)Termination phase: Saturation
% 7.13/1.90 % (667646)Time elapsed: 0.064 s
% 7.13/1.90 % (667646)Peak memory usage: 89 MB
% 7.13/1.90 % (667646)Instructions burned: 118 (million)
% 7.13/1.90 % (667644)Instruction limit reached!
% 7.13/1.90 % (667644)------------------------------
% 7.13/1.90 % (667644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.90 % (667644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.90 % (667644)CaDiCaL version: 2.1.3
% 7.13/1.90 % (667644)Termination reason: Instruction limit
% 7.13/1.90 % (667644)Termination phase: Saturation
% 7.13/1.90 % (667644)Time elapsed: 0.072 s
% 7.13/1.90 % (667644)Peak memory usage: 89 MB
% 7.13/1.90 % (667644)Instructions burned: 114 (million)
% 7.13/1.90 % (667645)Instruction limit reached!
% 7.13/1.90 % (667645)------------------------------
% 7.13/1.90 % (667645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.90 % (667645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.90 % (667645)CaDiCaL version: 2.1.3
% 7.13/1.90 % (667645)Termination reason: Instruction limit
% 7.13/1.90 % (667645)Termination phase: Saturation
% 7.13/1.90 % (667645)Time elapsed: 0.114 s
% 7.13/1.90 % (667645)Peak memory usage: 90 MB
% 7.13/1.90 % (667645)Instructions burned: 180 (million)
% 7.13/1.90 % (667654)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=1112801962:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 7.13/1.90 % (667655)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1223979653: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)
% 7.13/1.90 % (667654)Refutation not found, incomplete strategy
% 7.13/1.90 % (667654)------------------------------
% 7.13/1.90 % (667654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.90 % (667654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.90 % (667654)CaDiCaL version: 2.1.3
% 7.13/1.90 % (667654)Termination reason: Refutation not found, incomplete strategy
% 14.18/2.67 % (667654)Time elapsed: 0.011 s
% 14.18/2.67 % (667654)Peak memory usage: 89 MB
% 14.18/2.67 % (667654)Instructions burned: 19 (million)
% 14.18/2.67 % (667656)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1488433830:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 14.18/2.67 % (667657)lrs+10_64_to=lpo:sil=8000:random_seed=2011449932:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 14.18/2.67 % (667655)Instruction limit reached!
% 14.18/2.67 % (667655)------------------------------
% 14.18/2.67 % (667655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.67 % (667655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.67 % (667655)CaDiCaL version: 2.1.3
% 14.18/2.67 % (667655)Termination reason: Instruction limit
% 14.18/2.67 % (667655)Termination phase: Saturation
% 14.18/2.67 % (667655)Time elapsed: 0.099 s
% 14.18/2.67 % (667655)Peak memory usage: 90 MB
% 14.18/2.67 % (667655)Instructions burned: 189 (million)
% 14.18/2.67 % (667657)Instruction limit reached!
% 14.18/2.67 % (667657)------------------------------
% 14.18/2.67 % (667657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667657)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667657)Termination reason: Instruction limit
% 14.18/2.68 % (667657)Termination phase: Saturation
% 14.18/2.68 % (667657)Time elapsed: 0.043 s
% 14.18/2.68 % (667657)Peak memory usage: 90 MB
% 14.18/2.68 % (667657)Instructions burned: 127 (million)
% 14.18/2.68 % (667656)Instruction limit reached!
% 14.18/2.68 % (667656)------------------------------
% 14.18/2.68 % (667656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667656)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667656)Termination reason: Instruction limit
% 14.18/2.68 % (667656)Termination phase: Saturation
% 14.18/2.68 % (667656)Time elapsed: 0.118 s
% 14.18/2.68 % (667656)Peak memory usage: 90 MB
% 14.18/2.68 % (667656)Instructions burned: 221 (million)
% 14.18/2.68 % (667663)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2050913996:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 14.18/2.68 % (667662)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2623922963:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 14.18/2.68 % (667654)------------------------------
% 14.18/2.68 % (667654)------------------------------
% 14.18/2.68 % (667663)Instruction limit reached!
% 14.18/2.68 % (667663)------------------------------
% 14.18/2.68 % (667663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667663)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667663)Termination reason: Instruction limit
% 14.18/2.68 % (667663)Termination phase: Saturation
% 14.18/2.68 % (667663)Time elapsed: 0.054 s
% 14.18/2.68 % (667663)Peak memory usage: 91 MB
% 14.18/2.68 % (667663)Instructions burned: 160 (million)
% 14.18/2.68 % (667664)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4153169666:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 14.18/2.68 % (667667)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=3351468981:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 14.18/2.68 % (667667)Instruction limit reached!
% 14.18/2.68 % (667667)------------------------------
% 14.18/2.68 % (667667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667667)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667667)Termination reason: Instruction limit
% 14.18/2.68 % (667667)Termination phase: Saturation
% 14.18/2.68 % (667667)Time elapsed: 0.030 s
% 14.18/2.68 % (667667)Peak memory usage: 90 MB
% 14.18/2.68 % (667667)Instructions burned: 107 (million)
% 14.18/2.68 % (667662)Instruction limit reached!
% 14.18/2.68 % (667662)------------------------------
% 14.18/2.68 % (667662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667662)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667662)Termination reason: Instruction limit
% 14.18/2.68 % (667662)Termination phase: Saturation
% 14.18/2.68 % (667662)Time elapsed: 0.124 s
% 14.18/2.68 % (667662)Peak memory usage: 90 MB
% 14.18/2.68 % (667662)Instructions burned: 194 (million)
% 14.18/2.68 % (667668)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3509909282:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 14.18/2.68 % (667671)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3715404885:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 14.18/2.68 % (667668)Instruction limit reached!
% 14.18/2.68 % (667668)------------------------------
% 14.18/2.68 % (667668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667668)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667668)Termination reason: Instruction limit
% 14.18/2.68 % (667668)Termination phase: Saturation
% 14.18/2.68 % (667668)Time elapsed: 0.067 s
% 14.18/2.68 % (667668)Peak memory usage: 90 MB
% 14.18/2.68 % (667668)Instructions burned: 108 (million)
% 14.18/2.68 % (667672)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1439710824:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 14.18/2.68 % (667671)Instruction limit reached!
% 14.18/2.68 % (667671)------------------------------
% 14.18/2.68 % (667671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667671)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667671)Termination reason: Instruction limit
% 14.18/2.68 % (667671)Termination phase: Saturation
% 14.18/2.68 % (667671)Time elapsed: 0.076 s
% 14.18/2.68 % (667671)Peak memory usage: 90 MB
% 14.18/2.68 % (667671)Instructions burned: 242 (million)
% 14.18/2.68 % (667675)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3939557034:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 14.18/2.68 % (667677)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3951314908:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 14.18/2.68 % (667675)Instruction limit reached!
% 14.18/2.68 % (667675)------------------------------
% 14.18/2.68 % (667675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667675)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667675)Termination reason: Instruction limit
% 14.18/2.68 % (667675)Termination phase: Saturation
% 14.18/2.68 % (667675)Time elapsed: 0.083 s
% 14.18/2.68 % (667675)Peak memory usage: 90 MB
% 14.18/2.68 % (667675)Instructions burned: 135 (million)
% 14.18/2.68 % (667677)Instruction limit reached!
% 14.18/2.68 % (667677)------------------------------
% 14.18/2.68 % (667677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667677)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667677)Termination reason: Instruction limit
% 14.18/2.68 % (667677)Termination phase: Saturation
% 14.18/2.68 % (667677)Time elapsed: 0.166 s
% 14.18/2.68 % (667677)Peak memory usage: 95 MB
% 14.18/2.68 % (667677)Instructions burned: 500 (million)
% 14.18/2.68 % (667680)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=971665587:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 14.18/2.68 % (667681)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3278326143:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 14.18/2.68 % (667680)Instruction limit reached!
% 14.18/2.68 % (667680)------------------------------
% 14.18/2.68 % (667680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667680)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667680)Termination reason: Instruction limit
% 14.18/2.68 % (667680)Termination phase: Saturation
% 14.18/2.68 % (667680)Time elapsed: 0.122 s
% 14.18/2.68 % (667680)Peak memory usage: 91 MB
% 14.18/2.68 % (667680)Instructions burned: 191 (million)
% 14.18/2.68 % (667681)Instruction limit reached!
% 14.18/2.68 % (667681)------------------------------
% 14.18/2.68 % (667681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667681)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667681)Termination reason: Instruction limit
% 14.18/2.68 % (667681)Termination phase: Saturation
% 14.18/2.68 % (667681)Time elapsed: 0.083 s
% 14.18/2.68 % (667681)Peak memory usage: 91 MB
% 14.18/2.68 % (667681)Instructions burned: 267 (million)
% 14.18/2.68 % (667685)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2298370147:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi)
% 14.18/2.68 % (667684)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2953469379:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 14.18/2.68 % (667684)Instruction limit reached!
% 14.18/2.68 % (667684)------------------------------
% 14.18/2.68 % (667684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667684)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667684)Termination reason: Instruction limit
% 14.18/2.68 % (667684)Termination phase: Saturation
% 14.18/2.68 % (667684)Time elapsed: 0.096 s
% 14.18/2.68 % (667684)Peak memory usage: 90 MB
% 14.18/2.68 % (667684)Instructions burned: 156 (million)
% 14.18/2.68 % (667688)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=638347043:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi)
% 14.18/2.68 % (667640)First to succeed.
% 14.18/2.68 % (667640)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-667635"
% 14.18/2.68 % (667688)Instruction limit reached!
% 14.18/2.68 % (667688)------------------------------
% 14.18/2.68 % (667688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/2.68 % (667688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/2.68 % (667688)CaDiCaL version: 2.1.3
% 14.18/2.68 % (667688)Termination reason: Instruction limit
% 14.18/2.68 % (667688)Termination phase: Saturation
% 14.18/2.68 % (667688)Time elapsed: 0.319 s
% 14.18/2.68 % (667688)Peak memory usage: 91 MB
% 14.18/2.68 % (667688)Instructions burned: 538 (million)
% 14.18/2.68 % (667640)Refutation found. Thanks to Tanya!
% 14.18/2.68 % SZS status Unsatisfiable for theBenchmark
% 14.18/2.68 % SZS output start Proof for theBenchmark
% See solution above
% 14.89/2.87 % (667640)------------------------------
% 14.89/2.87 % (667640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.89/2.87 % (667640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.89/2.87 % (667640)CaDiCaL version: 2.1.3
% 14.89/2.87 % (667640)Termination reason: Refutation
% 14.89/2.87 % (667640)Time elapsed: 1.653 s
% 14.89/2.87 % (667640)Peak memory usage: 142 MB
% 14.89/2.87 % (667640)Instructions burned: 2696 (million)
% 14.89/2.87 % (667640)------------------------------
% 14.89/2.87 % (667640)------------------------------
% 14.89/2.87 % (667635)Success in time 2.07 s
% 14.89/2.87 % Vampire exiting
%------------------------------------------------------------------------------