%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT056-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:36:49 PM UTC 2026
% Result : Unsatisfiable 10.28s 2.38s
% Output : Refutation 11.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 34
% Syntax : Number of formulae : 211 ( 66 unt; 20 def)
% Number of atoms : 605 ( 43 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 695 ( 301 ~; 390 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 5 prp; 0-3 aty)
% Number of functors : 34 ( 34 usr; 26 con; 0-5 aty)
% Number of variables : 137 ( 0 sgn 137 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f626,axiom,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_iff_1) ).
fof(f627,axiom,
! [X0] :
( ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_iff_0) ).
fof(f634,axiom,
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_CHAINED_0) ).
fof(f635,axiom,
c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f636,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X3,v_sko__CHAINED__1(X0,X1,X2,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X3),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X0,X1,X2,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X3,c_Arrow__Order__Mirabelle_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))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_3) ).
fof(f637,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X3,v_sko__CHAINED__1(X0,X1,X3,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),v_F(X3),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X0,X1,X3,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),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(X3,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_2) ).
fof(f638,axiom,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X3,v_sko__CHAINED__1(X0,X1,X2,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X0,X1,X2,X3)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X3),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X3,c_Arrow__Order__Mirabelle_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))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_1) ).
fof(f639,axiom,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X3,v_sko__CHAINED__1(X0,X1,X3,X2)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X0,X1,X3,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),v_F(X3),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X3,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_02) ).
fof(f640,axiom,
! [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_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_1_03) ).
fof(f641,axiom,
! [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_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_04) ).
fof(f642,negated_conjecture,
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_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_0) ).
fof(f643,negated_conjecture,
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f660,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(f661,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(f727,definition,
sF0 = c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f728,plain,
c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(reorient_equations,[],[f727]) ).
fof(f729,definition,
sF1 = v_F(v_P_H____),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f730,plain,
v_F(v_P_H____) = sF1,
inference(reorient_equations,[],[f729]) ).
fof(f731,definition,
sF2 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f732,plain,
tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF2,
inference(reorient_equations,[],[f731]) ).
fof(f733,definition,
sF3 = tc_fun(sF2,tc_bool),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f734,plain,
tc_fun(sF2,tc_bool) = sF3,
inference(reorient_equations,[],[f733]) ).
fof(f735,definition,
sF4 = tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f736,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3) = sF4,
inference(reorient_equations,[],[f735]) ).
fof(f737,definition,
sF5 = tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f738,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF4) = sF5,
inference(reorient_equations,[],[f737]) ).
fof(f739,definition,
sF6 = c_COMBB(c_Arrow__Order__Mirabelle_Obelow,v_P____,sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f740,plain,
c_COMBB(c_Arrow__Order__Mirabelle_Obelow,v_P____,sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi) = sF6,
inference(reorient_equations,[],[f739]) ).
fof(f741,definition,
sF7 = c_COMBC(sF6,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f742,plain,
c_COMBC(sF6,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4) = sF7,
inference(reorient_equations,[],[f741]) ).
fof(f743,definition,
sF8 = c_COMBC(sF7,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f744,plain,
c_COMBC(sF7,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3) = sF8,
inference(reorient_equations,[],[f743]) ).
fof(f745,definition,
sF9 = c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF8,sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f746,plain,
c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF8,sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi) = sF9,
inference(reorient_equations,[],[f745]) ).
fof(f747,definition,
sF10 = c_COMBC(sF9,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f748,plain,
c_COMBC(sF9,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4) = sF10,
inference(reorient_equations,[],[f747]) ).
fof(f749,definition,
sF11 = c_COMBC(sF10,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f750,plain,
c_COMBC(sF10,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3) = sF11,
inference(reorient_equations,[],[f749]) ).
fof(f751,definition,
sF12 = c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF11,sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f752,plain,
c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF11,sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi) = sF12,
inference(reorient_equations,[],[f751]) ).
fof(f753,definition,
sF13 = c_COMBC(sF12,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f754,plain,
c_COMBC(sF12,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4) = sF13,
inference(reorient_equations,[],[f753]) ).
fof(f755,definition,
sF14 = c_COMBC(sF13,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f756,plain,
c_COMBC(sF13,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3) = sF14,
inference(reorient_equations,[],[f755]) ).
fof(f757,definition,
sF15 = v_F(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f758,plain,
v_F(sF14) = sF15,
inference(reorient_equations,[],[f757]) ).
fof(f759,plain,
( ~ c_in(sF0,sF1,sF2)
| ~ c_in(sF0,sF15,sF2) ),
inference(definition_folding,[],[f642,f732,f758,f756,f734,f732,f754,f736,f734,f732,f752,f738,f736,f734,f732,f734,f732,f750,f734,f732,f748,f736,f734,f732,f746,f738,f736,f734,f732,f734,f732,f744,f734,f732,f742,f736,f734,f732,f740,f738,f736,f734,f732,f734,f732,f728,f732,f730,f728]) ).
fof(f760,plain,
( c_in(sF0,sF15,sF2)
| c_in(sF0,sF1,sF2) ),
inference(definition_folding,[],[f643,f732,f730,f728,f732,f758,f756,f734,f732,f754,f736,f734,f732,f752,f738,f736,f734,f732,f734,f732,f750,f734,f732,f748,f736,f734,f732,f746,f738,f736,f734,f732,f734,f732,f744,f734,f732,f742,f736,f734,f732,f740,f738,f736,f734,f732,f734,f732,f728]) ).
fof(f775,definition,
( spl16_1
<=> c_in(sF0,sF1,sF2) ),
introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition]) ).
fof(f776,plain,
( ~ c_in(sF0,sF1,sF2)
| spl16_1 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f777,plain,
( c_in(sF0,sF1,sF2)
| ~ spl16_1 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f779,definition,
( spl16_2
<=> c_in(sF0,sF15,sF2) ),
introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition]) ).
fof(f780,plain,
( ~ c_in(sF0,sF15,sF2)
| spl16_2 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f781,plain,
( c_in(sF0,sF15,sF2)
| ~ spl16_2 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f782,plain,
( spl16_1
| spl16_2 ),
inference(avatar_split_clause,[],[f760,f779,f775]) ).
fof(f783,plain,
( ~ spl16_2
| ~ spl16_1 ),
inference(avatar_split_clause,[],[f759,f775,f779]) ).
fof(f860,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(sF11,X0)) = hAPP(sF12,X0),
inference(superposition,[],[f661,f752]) ).
fof(f861,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(sF8,X0)) = hAPP(sF9,X0),
inference(superposition,[],[f661,f746]) ).
fof(f862,plain,
! [X0] : hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X0)) = hAPP(sF6,X0),
inference(superposition,[],[f661,f740]) ).
fof(f863,plain,
c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool))),
inference(superposition,[],[f635,f732]) ).
fof(f864,plain,
c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f863,f734]) ).
fof(f865,plain,
! [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(sF6,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_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(superposition,[],[f640,f862]) ).
fof(f866,plain,
! [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(sF6,X0),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f865,f732]) ).
fof(f867,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(sF6,X0),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f866,f728]) ).
fof(f868,plain,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2)
| c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(sF6,X0),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),sF2) ),
inference(forward_demodulation,[],[f867,f732]) ).
fof(f869,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(sF6,X0),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f868,f728]) ).
fof(f871,plain,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),sF2) ),
inference(superposition,[],[f626,f732]) ).
fof(f872,plain,
! [X0] :
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f871,f728]) ).
fof(f875,plain,
! [X0] : hAPP(hAPP(sF13,X0),v_c____) = hAPP(sF14,X0),
inference(superposition,[],[f660,f756]) ).
fof(f876,plain,
! [X0] : hAPP(hAPP(sF6,X0),v_c____) = hAPP(sF7,X0),
inference(superposition,[],[f660,f742]) ).
fof(f877,plain,
! [X0] : hAPP(sF8,X0) = hAPP(hAPP(sF7,X0),v_b____),
inference(superposition,[],[f660,f744]) ).
fof(f878,plain,
! [X0] : hAPP(hAPP(sF9,X0),v_b____) = hAPP(sF10,X0),
inference(superposition,[],[f660,f748]) ).
fof(f879,plain,
! [X0] : hAPP(sF13,X0) = hAPP(hAPP(sF12,X0),v_a____),
inference(superposition,[],[f660,f754]) ).
fof(f880,plain,
! [X0] : hAPP(sF11,X0) = hAPP(hAPP(sF10,X0),v_a____),
inference(superposition,[],[f660,f750]) ).
fof(f881,plain,
! [X0] :
( ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(superposition,[],[f627,f732]) ).
fof(f882,plain,
! [X0] :
( ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),sF2)
| c_in(sF0,hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f881,f728]) ).
fof(f887,plain,
! [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____),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(superposition,[],[f641,f732]) ).
fof(f888,plain,
! [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(sF6,X0),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f887,f862]) ).
fof(f891,plain,
! [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(sF7,X0),v_b____)),v_b____),v_a____)),v_a____),v_c____),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f888,f876]) ).
fof(f894,plain,
! [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(sF8,X0)),v_b____),v_a____)),v_a____),v_c____),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f891,f877]) ).
fof(f897,plain,
! [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(sF9,X0),v_b____),v_a____)),v_a____),v_c____),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f894,f861]) ).
fof(f900,plain,
! [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(sF10,X0),v_a____)),v_a____),v_c____),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f897,f878]) ).
fof(f903,plain,
! [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(sF11,X0)),v_a____),v_c____),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f900,f880]) ).
fof(f906,plain,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(hAPP(sF12,X0),v_a____),v_c____),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f903,f860]) ).
fof(f909,plain,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(hAPP(sF13,X0),v_c____),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f906,f879]) ).
fof(f912,plain,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF14,X0),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f909,f875]) ).
fof(f915,plain,
! [X0] :
( ~ c_in(sF0,hAPP(sF14,X0),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f912,f728]) ).
fof(f918,plain,
! [X0] :
( ~ c_in(sF0,hAPP(sF14,X0),sF2)
| c_in(sF0,hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f915,f728]) ).
fof(f924,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(sF0,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))) ),
inference(superposition,[],[f637,f728]) ).
fof(f931,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(sF0,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))) ),
inference(forward_demodulation,[],[f924,f732]) ).
fof(f935,plain,
! [X0,X1] :
( ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(sF0,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))) ),
inference(forward_demodulation,[],[f931,f732]) ).
fof(f938,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| c_in(sF0,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))) ),
inference(forward_demodulation,[],[f935,f732]) ).
fof(f941,plain,
! [X0,X1] :
( c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))) ),
inference(forward_demodulation,[],[f938,f732]) ).
fof(f944,plain,
! [X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))) ),
inference(forward_demodulation,[],[f941,f732]) ).
fof(f947,plain,
! [X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))) ),
inference(forward_demodulation,[],[f944,f734]) ).
fof(f950,plain,
! [X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2) ),
inference(forward_demodulation,[],[f947,f732]) ).
fof(f953,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,X1)),sF2) ),
inference(forward_demodulation,[],[f950,f734]) ).
fof(f956,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(sF0,v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(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))) ),
inference(superposition,[],[f636,f728]) ).
fof(f963,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2)
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(sF0,v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(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))) ),
inference(forward_demodulation,[],[f956,f732]) ).
fof(f967,plain,
! [X0,X1] :
( ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2)
| c_in(sF0,v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(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))) ),
inference(forward_demodulation,[],[f963,f732]) ).
fof(f970,plain,
! [X0,X1] :
( c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2)
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(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))) ),
inference(forward_demodulation,[],[f967,f732]) ).
fof(f973,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2)
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ 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))) ),
inference(forward_demodulation,[],[f970,f732]) ).
fof(f976,plain,
! [X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2)
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))) ),
inference(forward_demodulation,[],[f973,f732]) ).
fof(f979,plain,
! [X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2)
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))) ),
inference(forward_demodulation,[],[f976,f734]) ).
fof(f982,plain,
! [X0,X1] :
( ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2)
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2) ),
inference(forward_demodulation,[],[f979,f732]) ).
fof(f985,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X1,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X1,X0)),sF2) ),
inference(forward_demodulation,[],[f982,f734]) ).
fof(f988,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(sF7,X0),v_b____)),v_b____),v_a____)),v_a____),v_c____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,X0),sF2) ),
inference(superposition,[],[f869,f876]) ).
fof(f989,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(sF8,X0)),v_b____),v_a____)),v_a____),v_c____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f988,f877]) ).
fof(f990,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(sF9,X0),v_b____),v_a____)),v_a____),v_c____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f989,f861]) ).
fof(f991,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(sF10,X0),v_a____)),v_a____),v_c____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f990,f878]) ).
fof(f992,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(sF11,X0)),v_a____),v_c____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f991,f880]) ).
fof(f993,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(hAPP(sF12,X0),v_a____),v_c____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f992,f860]) ).
fof(f994,plain,
! [X0] :
( c_in(sF0,hAPP(hAPP(sF13,X0),v_c____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,X0),sF2) ),
inference(forward_demodulation,[],[f993,f879]) ).
fof(f995,plain,
! [X0] :
( ~ c_in(sF0,hAPP(v_P_H____,X0),sF2)
| c_in(sF0,hAPP(sF14,X0),sF2) ),
inference(forward_demodulation,[],[f994,f875]) ).
fof(f1164,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(resolution,[],[f638,f626]) ).
fof(f1200,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_subsumption_resolution,[],[f1164,f635]) ).
fof(f1216,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1200,f732]) ).
fof(f1515,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(resolution,[],[f639,f626]) ).
fof(f1544,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_subsumption_resolution,[],[f1515,f635]) ).
fof(f1560,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1544,f732]) ).
fof(f1896,plain,
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(sF2,tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF2,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(sF2,tc_bool))),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF2,tc_bool)),tc_fun(sF2,tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF2,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(sF2,tc_bool))),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF2,tc_bool)),tc_fun(sF2,tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF2,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(sF2,tc_bool))),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(sF2,tc_bool)),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool))),
inference(superposition,[],[f634,f732]) ).
fof(f1897,plain,
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____,sF3,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3)),tc_Arrow__Order__Mirabelle_Oindi),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3)),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3)),tc_Arrow__Order__Mirabelle_Oindi),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3)),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3)),tc_Arrow__Order__Mirabelle_Oindi),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF3)),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f1896,f734]) ).
fof(f1899,plain,
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____,sF3,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF4),tc_Arrow__Order__Mirabelle_Oindi),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF4),tc_Arrow__Order__Mirabelle_Oindi),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,sF4),tc_Arrow__Order__Mirabelle_Oindi),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f1897,f736]) ).
fof(f2536,plain,
! [X0] :
( c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1216,f728]) ).
fof(f2541,plain,
! [X0] :
( c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f1560,f728]) ).
fof(f2543,plain,
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____,sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f1899,f738]) ).
fof(f2557,plain,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2536,f732]) ).
fof(f2562,plain,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2541,f732]) ).
fof(f2564,plain,
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(sF6,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f2543,f740]) ).
fof(f2574,plain,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF1,sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2557,f730]) ).
fof(f2578,plain,
! [X0] :
( ~ c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2562,f728]) ).
fof(f2580,plain,
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(sF7,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f2564,f742]) ).
fof(f2590,plain,
! [X0] :
( ~ c_in(sF0,sF1,sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2574,f728]) ).
fof(f2594,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P_H____),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2578,f732]) ).
fof(f2596,plain,
c_in(c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF8,sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f2580,f744]) ).
fof(f2609,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF1,sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2594,f730]) ).
fof(f2610,plain,
c_in(c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(c_COMBC(sF9,v_b____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f2596,f746]) ).
fof(f2622,plain,
! [X0] :
( c_in(sF0,sF1,sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2609,f728]) ).
fof(f2623,plain,
c_in(c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,c_COMBC(sF10,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f2610,f748]) ).
fof(f2635,plain,
( ! [X0] :
( ~ c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| spl16_1 ),
inference(forward_subsumption_resolution,[],[f2622,f776]) ).
fof(f2636,plain,
c_in(c_COMBC(c_COMBC(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,sF11,sF3,sF5,tc_Arrow__Order__Mirabelle_Oindi),v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f2623,f750]) ).
fof(f2643,plain,
( ! [X0] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| ~ c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| spl16_1 ),
inference(forward_demodulation,[],[f2635,f732]) ).
fof(f2644,plain,
c_in(c_COMBC(c_COMBC(sF12,v_a____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF4),v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f2636,f752]) ).
fof(f2651,plain,
( ! [X0] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| spl16_1 ),
inference(forward_demodulation,[],[f2643,f734]) ).
fof(f2652,plain,
c_in(c_COMBC(sF13,v_c____,tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,sF3),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f2644,f754]) ).
fof(f2657,plain,
( ! [X0] :
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)) )
| spl16_1 ),
inference(forward_demodulation,[],[f2651,f732]) ).
fof(f2658,plain,
c_in(sF14,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f2652,f756]) ).
fof(f2679,plain,
( ! [X2,X3,X0,X1,X4] :
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,c_COMBC(X0,X1,X2,X3,X4),v_P_H____)),sF2)
| c_in(sF0,hAPP(hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,c_COMBC(X0,X1,X2,X3,X4),v_P_H____)),X1),sF2)
| ~ c_in(sF0,v_F(c_COMBC(X0,X1,X2,X3,X4)),sF2)
| ~ c_in(c_COMBC(X0,X1,X2,X3,X4),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)) )
| spl16_1 ),
inference(superposition,[],[f2657,f660]) ).
fof(f2762,plain,
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| c_in(sF0,hAPP(hAPP(sF13,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),v_c____),sF2)
| ~ c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF14,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| spl16_1 ),
inference(superposition,[],[f2679,f756]) ).
fof(f2788,plain,
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| c_in(sF0,hAPP(hAPP(sF13,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),v_c____),sF2)
| ~ c_in(sF0,v_F(sF14),sF2)
| spl16_1 ),
inference(forward_subsumption_resolution,[],[f2762,f2658]) ).
fof(f2790,plain,
( c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ c_in(sF0,v_F(sF14),sF2)
| spl16_1 ),
inference(forward_demodulation,[],[f2788,f875]) ).
fof(f2792,plain,
( ~ c_in(sF0,sF15,sF2)
| c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| spl16_1 ),
inference(forward_demodulation,[],[f2790,f758]) ).
fof(f2794,plain,
( c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| spl16_1
| ~ spl16_2 ),
inference(forward_subsumption_resolution,[],[f2792,f781]) ).
fof(f2796,definition,
( spl16_18
<=> c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2) ),
introduced(definition,[new_symbols(definition,[spl16_18])],[avatar_definition]) ).
fof(f2797,plain,
( ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| spl16_18 ),
inference(avatar_component_clause,[],[f2796]) ).
fof(f2798,plain,
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_18 ),
inference(avatar_component_clause,[],[f2796]) ).
fof(f2800,definition,
( spl16_19
<=> c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2) ),
introduced(definition,[new_symbols(definition,[spl16_19])],[avatar_definition]) ).
fof(f2801,plain,
( ~ c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| spl16_19 ),
inference(avatar_component_clause,[],[f2800]) ).
fof(f2802,plain,
( c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_19 ),
inference(avatar_component_clause,[],[f2800]) ).
fof(f2804,plain,
( spl16_18
| spl16_19
| spl16_1
| ~ spl16_2 ),
inference(avatar_split_clause,[],[f2794,f779,f775,f2800,f2796]) ).
fof(f2805,plain,
( c_in(sF0,hAPP(v_P_H____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_18 ),
inference(resolution,[],[f2798,f882]) ).
fof(f2808,plain,
( c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_18 ),
inference(resolution,[],[f2805,f995]) ).
fof(f2809,plain,
( ~ c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(sF14,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_18 ),
inference(resolution,[],[f2805,f953]) ).
fof(f2811,plain,
( c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(sF14,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_18 ),
inference(forward_subsumption_resolution,[],[f2809,f864]) ).
fof(f2812,plain,
( spl16_19
| ~ spl16_18 ),
inference(avatar_split_clause,[],[f2808,f2796,f2800]) ).
fof(f2813,plain,
( c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_18 ),
inference(forward_subsumption_resolution,[],[f2811,f2658]) ).
fof(f2814,plain,
( c_in(sF0,sF1,sF2)
| ~ c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_18 ),
inference(forward_demodulation,[],[f2813,f730]) ).
fof(f2815,plain,
( ~ c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| spl16_1
| ~ spl16_18 ),
inference(forward_subsumption_resolution,[],[f2814,f776]) ).
fof(f2816,plain,
( ~ c_in(sF0,sF15,sF2)
| ~ c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| spl16_1
| ~ spl16_18 ),
inference(forward_demodulation,[],[f2815,f758]) ).
fof(f2817,plain,
( ~ c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| spl16_1
| ~ spl16_2
| ~ spl16_18 ),
inference(forward_subsumption_resolution,[],[f2816,f781]) ).
fof(f2818,plain,
( ~ spl16_19
| spl16_1
| ~ spl16_2
| ~ spl16_18 ),
inference(avatar_split_clause,[],[f2817,f2796,f779,f775,f2800]) ).
fof(f2820,plain,
( ~ c_in(sF0,hAPP(v_P_H____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| spl16_18 ),
inference(resolution,[],[f2797,f872]) ).
fof(f2822,plain,
( c_in(sF0,hAPP(v_P_H____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_19 ),
inference(resolution,[],[f2802,f918]) ).
fof(f2825,plain,
( $false
| spl16_18
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f2822,f2820]) ).
fof(f2826,plain,
( spl16_18
| ~ spl16_19 ),
inference(avatar_contradiction_clause,[],[f2825]) ).
fof(f2829,plain,
( ! [X0] :
( c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl16_1 ),
inference(forward_subsumption_resolution,[],[f2590,f777]) ).
fof(f2831,plain,
( ! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl16_1 ),
inference(forward_demodulation,[],[f2829,f732]) ).
fof(f2833,plain,
( ! [X0] :
( c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl16_1 ),
inference(forward_demodulation,[],[f2831,f728]) ).
fof(f2835,plain,
( ! [X0] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl16_1 ),
inference(forward_demodulation,[],[f2833,f732]) ).
fof(f2837,plain,
( ! [X0] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl16_1 ),
inference(forward_demodulation,[],[f2835,f734]) ).
fof(f2839,plain,
( ! [X0] :
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(sF0,hAPP(X0,v_sko__CHAINED__1(v_b____,v_a____,X0,v_P_H____)),sF2)
| c_in(sF0,v_F(X0),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)) )
| ~ spl16_1 ),
inference(forward_demodulation,[],[f2837,f732]) ).
fof(f2883,plain,
( c_in(sF0,hAPP(sF14,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF14,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ spl16_1
| spl16_18 ),
inference(resolution,[],[f2839,f2797]) ).
fof(f2891,plain,
( c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF14,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ spl16_1
| spl16_18
| spl16_19 ),
inference(forward_subsumption_resolution,[],[f2883,f2801]) ).
fof(f2892,plain,
( c_in(sF0,v_F(sF14),sF2)
| ~ spl16_1
| spl16_18
| spl16_19 ),
inference(forward_subsumption_resolution,[],[f2891,f2658]) ).
fof(f2893,plain,
( c_in(sF0,sF15,sF2)
| ~ spl16_1
| spl16_18
| spl16_19 ),
inference(forward_demodulation,[],[f2892,f758]) ).
fof(f2894,plain,
( $false
| ~ spl16_1
| spl16_2
| spl16_18
| spl16_19 ),
inference(forward_subsumption_resolution,[],[f2893,f780]) ).
fof(f2895,plain,
( ~ spl16_1
| spl16_2
| spl16_18
| spl16_19 ),
inference(avatar_contradiction_clause,[],[f2894]) ).
fof(f2899,plain,
( ~ c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(sF14,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_19 ),
inference(resolution,[],[f2802,f985]) ).
fof(f2901,plain,
( ~ c_in(sF14,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f2899,f864]) ).
fof(f2902,plain,
( c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ c_in(sF0,hAPP(v_P_H____,v_sko__CHAINED__1(v_b____,v_a____,sF14,v_P_H____)),sF2)
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f2901,f2658]) ).
fof(f2903,plain,
( c_in(sF0,v_F(sF14),sF2)
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ spl16_18
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f2902,f2805]) ).
fof(f2904,plain,
( c_in(sF0,sF15,sF2)
| ~ c_in(sF0,v_F(v_P_H____),sF2)
| ~ spl16_18
| ~ spl16_19 ),
inference(forward_demodulation,[],[f2903,f758]) ).
fof(f2905,plain,
( ~ c_in(sF0,v_F(v_P_H____),sF2)
| spl16_2
| ~ spl16_18
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f2904,f780]) ).
fof(f2906,plain,
( ~ c_in(sF0,sF1,sF2)
| spl16_2
| ~ spl16_18
| ~ spl16_19 ),
inference(forward_demodulation,[],[f2905,f730]) ).
fof(f2907,plain,
( $false
| ~ spl16_1
| spl16_2
| ~ spl16_18
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f2906,f777]) ).
fof(f2908,plain,
( ~ spl16_1
| spl16_2
| ~ spl16_18
| ~ spl16_19 ),
inference(avatar_contradiction_clause,[],[f2907]) ).
cnf(s1,plain,
( spl16_1
| spl16_2 ),
inference(sat_conversion,[],[f782]) ).
cnf(s2,plain,
( ~ spl16_1
| ~ spl16_2 ),
inference(sat_conversion,[],[f783]) ).
cnf(s20,plain,
( spl16_1
| ~ spl16_2
| spl16_18
| spl16_19 ),
inference(sat_conversion,[],[f2804]) ).
cnf(s21,plain,
( ~ spl16_18
| spl16_19 ),
inference(sat_conversion,[],[f2812]) ).
cnf(s22,plain,
( spl16_1
| ~ spl16_2
| ~ spl16_18
| ~ spl16_19 ),
inference(sat_conversion,[],[f2818]) ).
cnf(s23,plain,
( spl16_18
| ~ spl16_19 ),
inference(sat_conversion,[],[f2826]) ).
cnf(s25,plain,
( ~ spl16_1
| spl16_2
| spl16_18
| spl16_19 ),
inference(sat_conversion,[],[f2895]) ).
cnf(s27,plain,
( ~ spl16_1
| spl16_2
| ~ spl16_18
| ~ spl16_19 ),
inference(sat_conversion,[],[f2908]) ).
cnf(s28,plain,
( spl16_18
| spl16_1 ),
inference(rat,[],[s20,s23,s1]) ).
cnf(s29,plain,
spl16_1,
inference(rat,[],[s22,s21,s28,s1]) ).
cnf(s30,plain,
~ spl16_2,
inference(rat,[],[s2,s29]) ).
cnf(s35,plain,
spl16_18,
inference(rat,[],[s25,s23,s29,s30]) ).
cnf(s36,plain,
spl16_19,
inference(rat,[],[s21,s35]) ).
cnf(s37,plain,
$false,
inference(rat,[],[s27,s30,s29,s36,s35]) ).
fof(f2909,plain,
$false,
inference(avatar_sat_refutation,[],[s37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT056-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n016.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 23:40:34 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.28/2.32 % (3118404)Input is clausal, will run a generic CNF schedule.
% 10.28/2.32 % (3118414)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3802529549:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.28/2.32 % (3118412)lrs+10_1_sil=8000:sp=occurrence:random_seed=119985838:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.28/2.32 % (3118413)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=359386583:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.28/2.32 % (3118409)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=3213882907:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.28/2.32 % (3118410)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1919992245:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.28/2.32 % (3118411)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1962113650:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.28/2.32 % (3118415)dis-21_1_sil=8000:lcm=predicate:random_seed=3798713076: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)
% 10.28/2.32 % (3118414)Instruction limit reached!
% 10.28/2.32 % (3118414)------------------------------
% 10.28/2.32 % (3118414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.32 % (3118414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.32 % (3118414)CaDiCaL version: 2.1.3
% 10.28/2.32 % (3118414)Termination reason: Instruction limit
% 10.28/2.32 % (3118414)Termination phase: Saturation
% 10.28/2.32 % (3118414)Time elapsed: 0.062 s
% 10.28/2.32 % (3118414)Peak memory usage: 90 MB
% 10.28/2.32 % (3118414)Instructions burned: 180 (million)
% 10.28/2.32 % (3118412)Instruction limit reached!
% 10.28/2.32 % (3118412)------------------------------
% 10.28/2.32 % (3118412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.32 % (3118412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.32 % (3118412)CaDiCaL version: 2.1.3
% 10.28/2.32 % (3118412)Termination reason: Instruction limit
% 10.28/2.32 % (3118412)Termination phase: Saturation
% 10.28/2.32 % (3118412)Time elapsed: 0.069 s
% 10.28/2.32 % (3118412)Peak memory usage: 89 MB
% 10.28/2.32 % (3118412)Instructions burned: 108 (million)
% 10.28/2.32 % (3118415)Instruction limit reached!
% 10.28/2.32 % (3118415)------------------------------
% 10.28/2.32 % (3118415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.32 % (3118415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.32 % (3118415)CaDiCaL version: 2.1.3
% 10.28/2.32 % (3118415)Termination reason: Instruction limit
% 10.28/2.32 % (3118415)Termination phase: Saturation
% 10.28/2.32 % (3118415)Time elapsed: 0.062 s
% 10.28/2.32 % (3118415)Peak memory usage: 89 MB
% 10.28/2.32 % (3118415)Instructions burned: 117 (million)
% 10.28/2.32 % (3118413)Instruction limit reached!
% 10.28/2.32 % (3118413)------------------------------
% 10.28/2.32 % (3118413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.32 % (3118413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.32 % (3118413)CaDiCaL version: 2.1.3
% 10.28/2.32 % (3118413)Termination reason: Instruction limit
% 10.28/2.32 % (3118413)Termination phase: Saturation
% 10.28/2.32 % (3118413)Time elapsed: 0.070 s
% 10.28/2.32 % (3118413)Peak memory usage: 89 MB
% 10.28/2.32 % (3118413)Instructions burned: 115 (million)
% 10.28/2.32 % (3118423)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=3693465324:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.28/2.32 % (3118423)Refutation not found, incomplete strategy
% 10.28/2.32 % (3118423)------------------------------
% 10.28/2.32 % (3118423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.32 % (3118423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.32 % (3118423)CaDiCaL version: 2.1.3
% 10.28/2.32 % (3118423)Termination reason: Refutation not found, incomplete strategy
% 10.28/2.32 % (3118423)Time elapsed: 0.004 s
% 10.28/2.32 % (3118423)Peak memory usage: 89 MB
% 10.28/2.32 % (3118423)Instructions burned: 13 (million)
% 10.28/2.32 % (3118426)lrs+10_64_to=lpo:sil=8000:random_seed=1396349827:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 10.28/2.38 % (3118425)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1542636227:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.28/2.38 % (3118424)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2434527190: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)
% 10.28/2.38 % (3118425)Refutation not found, incomplete strategy
% 10.28/2.38 % (3118425)------------------------------
% 10.28/2.38 % (3118425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.38 % (3118425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.38 % (3118425)CaDiCaL version: 2.1.3
% 10.28/2.38 % (3118425)Termination reason: Refutation not found, incomplete strategy
% 10.28/2.38 % (3118425)Time elapsed: 0.023 s
% 10.28/2.38 % (3118425)Peak memory usage: 89 MB
% 10.28/2.38 % (3118425)Instructions burned: 40 (million)
% 10.28/2.38 % (3118423)------------------------------
% 10.28/2.38 % (3118423)------------------------------
% 10.28/2.38 % (3118426)Instruction limit reached!
% 10.28/2.38 % (3118426)------------------------------
% 10.28/2.38 % (3118426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.38 % (3118426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.38 % (3118426)CaDiCaL version: 2.1.3
% 10.28/2.38 % (3118426)Termination reason: Instruction limit
% 10.28/2.38 % (3118426)Termination phase: Saturation
% 10.28/2.38 % (3118426)Time elapsed: 0.083 s
% 10.28/2.38 % (3118426)Peak memory usage: 90 MB
% 10.28/2.38 % (3118426)Instructions burned: 126 (million)
% 10.28/2.38 % (3118424)Instruction limit reached!
% 10.28/2.38 % (3118424)------------------------------
% 10.28/2.38 % (3118424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.38 % (3118424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.38 % (3118424)CaDiCaL version: 2.1.3
% 10.28/2.38 % (3118424)Termination reason: Instruction limit
% 10.28/2.38 % (3118424)Termination phase: Saturation
% 10.28/2.38 % (3118424)Time elapsed: 0.104 s
% 10.28/2.38 % (3118424)Peak memory usage: 90 MB
% 10.28/2.38 % (3118424)Instructions burned: 190 (million)
% 10.28/2.38 % (3118432)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=936326044:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 10.28/2.38 % (3118431)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1209727148:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 10.28/2.38 % (3118432)Instruction limit reached!
% 10.28/2.38 % (3118432)------------------------------
% 10.28/2.38 % (3118432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.38 % (3118432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.38 % (3118432)CaDiCaL version: 2.1.3
% 10.28/2.38 % (3118432)Termination reason: Instruction limit
% 10.28/2.38 % (3118432)Termination phase: Saturation
% 10.28/2.38 % (3118432)Time elapsed: 0.054 s
% 10.28/2.38 % (3118432)Peak memory usage: 91 MB
% 10.28/2.38 % (3118432)Instructions burned: 157 (million)
% 10.28/2.38 % (3118433)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=952647514:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 10.28/2.38 % (3118425)------------------------------
% 10.28/2.38 % (3118425)------------------------------
% 10.28/2.38 % (3118436)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=3686729335:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 10.28/2.38 % (3118431)Instruction limit reached!
% 10.28/2.38 % (3118431)------------------------------
% 10.28/2.38 % (3118431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.38 % (3118431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.38 % (3118431)CaDiCaL version: 2.1.3
% 10.28/2.38 % (3118431)Termination reason: Instruction limit
% 10.28/2.38 % (3118431)Termination phase: Saturation
% 10.28/2.38 % (3118431)Time elapsed: 0.132 s
% 10.28/2.38 % (3118431)Peak memory usage: 90 MB
% 10.28/2.38 % (3118431)Instructions burned: 195 (million)
% 10.28/2.38 % (3118436)Instruction limit reached!
% 10.28/2.38 % (3118436)------------------------------
% 10.28/2.38 % (3118436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.38 % (3118436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.38 % (3118436)CaDiCaL version: 2.1.3
% 10.28/2.38 % (3118436)Termination reason: Instruction limit
% 10.28/2.38 % (3118436)Termination phase: Saturation
% 10.28/2.38 % (3118436)Time elapsed: 0.034 s
% 10.28/2.38 % (3118436)Peak memory usage: 90 MB
% 10.28/2.38 % (3118436)Instructions burned: 107 (million)
% 10.28/2.38 % (3118438)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3493092388:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 10.28/2.38 % (3118441)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=876660145:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 10.28/2.38 % (3118438)Instruction limit reached!
% 10.28/2.38 % (3118438)------------------------------
% 10.28/2.38 % (3118438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.38 % (3118438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.38 % (3118438)CaDiCaL version: 2.1.3
% 10.28/2.38 % (3118438)Termination reason: Instruction limit
% 10.28/2.38 % (3118438)Termination phase: Saturation
% 10.28/2.38 % (3118438)Time elapsed: 0.068 s
% 10.28/2.38 % (3118438)Peak memory usage: 90 MB
% 10.28/2.38 % (3118438)Instructions burned: 108 (million)
% 10.28/2.38 % (3118440)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1230932160:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 10.28/2.38 % (3118444)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1314993318:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 10.28/2.38 % (3118440)Instruction limit reached!
% 10.28/2.38 % (3118440)------------------------------
% 10.28/2.38 % (3118440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.38 % (3118440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.38 % (3118440)CaDiCaL version: 2.1.3
% 10.28/2.38 % (3118440)Termination reason: Instruction limit
% 10.28/2.38 % (3118440)Termination phase: Saturation
% 10.28/2.38 % (3118440)Time elapsed: 0.149 s
% 10.28/2.38 % (3118440)Peak memory usage: 90 MB
% 10.28/2.38 % (3118440)Instructions burned: 243 (million)
% 10.28/2.38 % (3118444)Instruction limit reached!
% 10.28/2.38 % (3118444)------------------------------
% 10.28/2.38 % (3118444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.38 % (3118444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.38 % (3118444)CaDiCaL version: 2.1.3
% 10.28/2.38 % (3118444)Termination reason: Instruction limit
% 10.28/2.38 % (3118444)Termination phase: Saturation
% 10.28/2.38 % (3118444)Time elapsed: 0.082 s
% 10.28/2.38 % (3118444)Peak memory usage: 90 MB
% 10.28/2.38 % (3118444)Instructions burned: 135 (million)
% 10.28/2.38 % (3118448)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1433755983:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 10.28/2.38 % (3118449)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2806813006:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 10.28/2.38 % (3118409)First to succeed.
% 10.28/2.38 % (3118409)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3118404"
% 10.28/2.38 % (3118449)Instruction limit reached!
% 10.28/2.38 % (3118449)------------------------------
% 10.28/2.38 % (3118449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.38 % (3118449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.38 % (3118449)CaDiCaL version: 2.1.3
% 10.28/2.38 % (3118449)Termination reason: Instruction limit
% 10.28/2.38 % (3118449)Termination phase: Saturation
% 10.28/2.38 % (3118449)Time elapsed: 0.128 s
% 10.28/2.38 % (3118449)Peak memory usage: 91 MB
% 10.28/2.38 % (3118449)Instructions burned: 192 (million)
% 10.28/2.38 % (3118441)Also succeeded, but the first one will report.
% 10.28/2.38 % (3118452)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3695965728:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 10.28/2.38 % (3118448)Instruction limit reached!
% 10.28/2.38 % (3118448)------------------------------
% 10.28/2.38 % (3118448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.28/2.38 % (3118448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.28/2.38 % (3118448)CaDiCaL version: 2.1.3
% 10.28/2.38 % (3118448)Termination reason: Instruction limit
% 10.28/2.38 % (3118448)Termination phase: Saturation
% 10.28/2.38 % (3118448)Time elapsed: 0.333 s
% 10.28/2.38 % (3118448)Peak memory usage: 95 MB
% 10.28/2.38 % (3118448)Instructions burned: 499 (million)
% 10.28/2.38 % (3118409)Refutation found. Thanks to Tanya!
% 10.28/2.38 % SZS status Unsatisfiable for theBenchmark
% 10.28/2.38 % SZS output start Proof for theBenchmark
% See solution above
% 11.11/2.58 % (3118409)------------------------------
% 11.11/2.58 % (3118409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.11/2.58 % (3118409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.11/2.58 % (3118409)CaDiCaL version: 2.1.3
% 11.11/2.58 % (3118409)Termination reason: Refutation
% 11.11/2.58 % (3118409)Time elapsed: 1.076 s
% 11.11/2.58 % (3118409)Peak memory usage: 136 MB
% 11.11/2.58 % (3118409)Instructions burned: 1709 (million)
% 11.11/2.58 % (3118409)------------------------------
% 11.11/2.58 % (3118409)------------------------------
% 11.11/2.58 % (3118404)Success in time 1.523 s
% 11.11/2.58 % Vampire exiting
%------------------------------------------------------------------------------