%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT063-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:36:50 PM UTC 2026
% Result : Unsatisfiable 9.64s 2.22s
% Output : Refutation 9.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 24
% Syntax : Number of formulae : 171 ( 35 unt; 12 def)
% Number of atoms : 603 ( 43 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 744 ( 312 ~; 428 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 5 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 17 con; 0-5 aty)
% Number of variables : 197 ( 0 sgn 197 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f551,axiom,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X3,v_sko__local__X3__1(X2,X3,X0,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,X3,X0,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X1,X0,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)))
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_3_1) ).
fof(f554,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X3,v_sko__local__X3__1(X2,X3,X0,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X1,X0,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__local__X3__1(X2,X3,X0,X1)),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)))
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_3_3) ).
fof(f593,axiom,
c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_A_I4_J_0) ).
fof(f708,axiom,
c_in(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cP_0) ).
fof(f735,axiom,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| 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/sandbox/benchmark/theBenchmark.p',cls_iff_1) ).
fof(f736,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_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_iff_0) ).
fof(f739,axiom,
v_a____ != v_b____,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_A_I1_J_0) ).
fof(f740,plain,
v_b____ != v_a____,
inference(reorient_equations,[],[f739]) ).
fof(f747,axiom,
! [X2,X3,X0,X1,X4] :
( ~ c_in(c_Pair(X1,X0,X3,X2),hAPP(c_Relation_Oconverse(X2,X3),X4),tc_prod(X3,X2))
| c_in(c_Pair(X0,X1,X2,X3),X4,tc_prod(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_converseD_0) ).
fof(f749,axiom,
! [X2,X0,X1] : hAPP(c_Relation_Oconverse(X0,X1),hAPP(c_Relation_Oconverse(X1,X0),X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_converse__converse_0) ).
fof(f751,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(c_Fun_Ocomp(X0,X1,X2,X3,X4),X5) = hAPP(X0,hAPP(X1,X5)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_o__apply_0) ).
fof(f754,negated_conjecture,
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f755,negated_conjecture,
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f841,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(f842,plain,
c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(reorient_equations,[],[f841]) ).
fof(f843,definition,
sF1 = c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f844,plain,
c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF1,
inference(reorient_equations,[],[f843]) ).
fof(f845,definition,
sF2 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f846,plain,
tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF2,
inference(reorient_equations,[],[f845]) ).
fof(f847,definition,
sF3 = tc_fun(sF2,tc_bool),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f848,plain,
tc_fun(sF2,tc_bool) = sF3,
inference(reorient_equations,[],[f847]) ).
fof(f849,definition,
sF4 = c_Fun_Ocomp(sF1,v_P____,sF3,sF3,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f850,plain,
c_Fun_Ocomp(sF1,v_P____,sF3,sF3,tc_Arrow__Order__Mirabelle_Oindi) = sF4,
inference(reorient_equations,[],[f849]) ).
fof(f851,definition,
sF5 = v_F(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f852,plain,
v_F(sF4) = sF5,
inference(reorient_equations,[],[f851]) ).
fof(f853,definition,
sF6 = c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f854,plain,
c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF6,
inference(reorient_equations,[],[f853]) ).
fof(f855,definition,
sF7 = v_F(v_P____),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f856,plain,
v_F(v_P____) = sF7,
inference(reorient_equations,[],[f855]) ).
fof(f857,plain,
( ~ c_in(sF0,sF5,sF2)
| ~ c_in(sF6,sF7,sF2) ),
inference(definition_folding,[],[f754,f846,f856,f854,f846,f852,f850,f848,f846,f848,f846,f844,f842]) ).
fof(f858,plain,
( c_in(sF6,sF7,sF2)
| c_in(sF0,sF5,sF2) ),
inference(definition_folding,[],[f755,f846,f852,f850,f848,f846,f848,f846,f844,f842,f846,f856,f854]) ).
fof(f862,definition,
( spl8_1
<=> c_in(sF0,sF5,sF2) ),
introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition]) ).
fof(f863,plain,
( ~ c_in(sF0,sF5,sF2)
| spl8_1 ),
inference(avatar_component_clause,[],[f862]) ).
fof(f864,plain,
( c_in(sF0,sF5,sF2)
| ~ spl8_1 ),
inference(avatar_component_clause,[],[f862]) ).
fof(f866,definition,
( spl8_2
<=> c_in(sF6,sF7,sF2) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
fof(f867,plain,
( ~ c_in(sF6,sF7,sF2)
| spl8_2 ),
inference(avatar_component_clause,[],[f866]) ).
fof(f868,plain,
( c_in(sF6,sF7,sF2)
| ~ spl8_2 ),
inference(avatar_component_clause,[],[f866]) ).
fof(f869,plain,
( spl8_1
| spl8_2 ),
inference(avatar_split_clause,[],[f858,f866,f862]) ).
fof(f870,plain,
( ~ spl8_2
| ~ spl8_1 ),
inference(avatar_split_clause,[],[f857,f862,f866]) ).
fof(f949,plain,
c_in(c_Fun_Ocomp(sF1,v_P____,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_Arrow__Order__Mirabelle_Oindi),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
inference(superposition,[],[f708,f844]) ).
fof(f950,plain,
c_in(c_Fun_Ocomp(sF1,v_P____,tc_fun(sF2,tc_bool),tc_fun(sF2,tc_bool),tc_Arrow__Order__Mirabelle_Oindi),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool))),
inference(forward_demodulation,[],[f949,f846]) ).
fof(f951,plain,
c_in(c_Fun_Ocomp(sF1,v_P____,sF3,sF3,tc_Arrow__Order__Mirabelle_Oindi),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f950,f848]) ).
fof(f952,plain,
c_in(sF4,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f951,f850]) ).
fof(f957,plain,
! [X0] : hAPP(sF1,hAPP(v_P____,X0)) = hAPP(sF4,X0),
inference(superposition,[],[f751,f850]) ).
fof(f960,plain,
c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool))),
inference(superposition,[],[f593,f846]) ).
fof(f961,plain,
c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)),
inference(forward_demodulation,[],[f960,f848]) ).
fof(f962,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = v_a____ ),
inference(superposition,[],[f554,f842]) ).
fof(f963,plain,
! [X0,X1] :
( ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF6,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(X1),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(X1,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = v_a____ ),
inference(superposition,[],[f554,f854]) ).
fof(f968,plain,
! [X0,X1] :
( ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF6,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(X1),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(X1,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),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_subsumption_resolution,[],[f963,f740]) ).
fof(f969,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(sF0,v_F(X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),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_subsumption_resolution,[],[f962,f740]) ).
fof(f972,plain,
! [X0,X1] :
( ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| ~ c_in(sF6,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(X1),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(X1,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),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,[],[f968,f846]) ).
fof(f973,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),sF2)
| ~ c_in(sF0,v_F(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),v_F(X1),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(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),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,[],[f969,f846]) ).
fof(f975,plain,
! [X0,X1] :
( ~ c_in(sF6,v_F(X0),sF2)
| ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),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,[],[f972,f846]) ).
fof(f976,plain,
! [X0,X1] :
( ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),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,[],[f973,f846]) ).
fof(f978,plain,
! [X0,X1] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF2)
| ~ c_in(sF6,v_F(X0),sF2)
| ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),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,[],[f975,f846]) ).
fof(f979,plain,
! [X0,X1] :
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),sF2)
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),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,[],[f976,f846]) ).
fof(f981,plain,
! [X0,X1] :
( c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF6,v_F(X0),sF2)
| ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),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,[],[f978,f842]) ).
fof(f982,plain,
! [X0,X1] :
( c_in(sF6,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),sF2)
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),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,[],[f979,f854]) ).
fof(f984,plain,
! [X0,X1] :
( ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF6,v_F(X0),sF2)
| ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ 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,[],[f981,f846]) ).
fof(f985,plain,
! [X0,X1] :
( ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),sF2)
| c_in(sF6,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),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,[],[f982,f846]) ).
fof(f987,plain,
! [X0,X1] :
( ~ c_in(sF0,hAPP(X1,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF6,v_F(X0),sF2)
| ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ 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,[],[f984,f842]) ).
fof(f988,plain,
! [X0,X1] :
( ~ c_in(sF6,hAPP(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),sF2)
| c_in(sF6,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),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,[],[f985,f854]) ).
fof(f990,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__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF6,v_F(X0),sF2)
| ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),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,[],[f987,f846]) ).
fof(f991,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(sF6,hAPP(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),sF2)
| c_in(sF6,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),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,[],[f988,f846]) ).
fof(f992,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__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF6,v_F(X0),sF2)
| ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),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,[],[f990,f848]) ).
fof(f993,plain,
! [X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(sF6,hAPP(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),sF2)
| c_in(sF6,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),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,[],[f991,f848]) ).
fof(f994,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__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF6,v_F(X0),sF2)
| ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),sF2) ),
inference(forward_demodulation,[],[f992,f846]) ).
fof(f995,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(sF6,hAPP(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),sF2)
| c_in(sF6,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),sF2) ),
inference(forward_demodulation,[],[f993,f846]) ).
fof(f996,plain,
! [X0,X1] :
( ~ c_in(sF6,hAPP(X0,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(sF0,hAPP(X1,v_sko__local__X3__1(X1,X0,v_b____,v_a____)),sF2)
| c_in(sF0,v_F(X1),sF2)
| ~ c_in(sF6,v_F(X0),sF2)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)) ),
inference(forward_demodulation,[],[f994,f848]) ).
fof(f997,plain,
! [X0,X1] :
( ~ c_in(sF6,hAPP(X1,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),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(sF6,v_F(X1),sF2)
| ~ c_in(sF0,v_F(X0),sF2)
| ~ c_in(sF0,hAPP(X0,v_sko__local__X3__1(X1,X0,v_a____,v_b____)),sF2) ),
inference(forward_demodulation,[],[f995,f848]) ).
fof(f1056,plain,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),sF2) ),
inference(superposition,[],[f735,f846]) ).
fof(f1057,plain,
! [X0] :
( ~ c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),sF2)
| c_in(sF6,hAPP(v_P____,X0),sF2) ),
inference(forward_demodulation,[],[f1056,f854]) ).
fof(f2321,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| 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____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| v_b____ = v_a____
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(resolution,[],[f551,f736]) ).
fof(f2328,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,hAPP(X1,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7))),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(X0,X1,X3,X4,X5)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X6,X7,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_Fun_Ocomp(X0,X1,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(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)))
| X6 = X7 ),
inference(superposition,[],[f551,f751]) ).
fof(f2342,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,hAPP(X1,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7))),sF2)
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(X0,X1,X3,X4,X5)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X6,X7,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_Fun_Ocomp(X0,X1,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(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)))
| X6 = X7 ),
inference(forward_demodulation,[],[f2328,f846]) ).
fof(f2347,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| 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)))
| v_b____ = v_a____
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_subsumption_resolution,[],[f2321,f593]) ).
fof(f2354,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7)),sF2)
| c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,hAPP(X1,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7))),sF2)
| ~ c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(X0,X1,X3,X4,X5)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X6,X7,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_Fun_Ocomp(X0,X1,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(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)))
| X6 = X7 ),
inference(forward_demodulation,[],[f2342,f846]) ).
fof(f2359,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| 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_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_subsumption_resolution,[],[f2347,f740]) ).
fof(f2364,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(X0,X1,X3,X4,X5)),sF2)
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7)),sF2)
| c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,hAPP(X1,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7))),sF2)
| c_in(c_Pair(X6,X7,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_Fun_Ocomp(X0,X1,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(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)))
| X6 = X7 ),
inference(forward_demodulation,[],[f2354,f846]) ).
fof(f2369,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),sF2)
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_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_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2359,f846]) ).
fof(f2374,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(X0,X1,X3,X4,X5)),sF2)
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7)),sF2)
| c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,hAPP(X1,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7))),sF2)
| ~ c_in(c_Fun_Ocomp(X0,X1,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| ~ c_in(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)))
| X6 = X7 ),
inference(forward_demodulation,[],[f2364,f846]) ).
fof(f2379,plain,
! [X0] :
( c_in(sF0,hAPP(X0,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),sF2)
| ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_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_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2369,f842]) ).
fof(f2384,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_in(c_Fun_Ocomp(X0,X1,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(X0,X1,X3,X4,X5)),sF2)
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7)),sF2)
| c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,hAPP(X1,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7))),sF2)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X6 = X7 ),
inference(forward_demodulation,[],[f2374,f846]) ).
fof(f2389,plain,
! [X0] :
( ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),sF2)
| c_in(sF0,hAPP(X0,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),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_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2379,f846]) ).
fof(f2393,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_in(c_Fun_Ocomp(X0,X1,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(X0,X1,X3,X4,X5)),sF2)
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7)),sF2)
| c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,hAPP(X1,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7))),sF2)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| X6 = X7 ),
inference(forward_demodulation,[],[f2384,f848]) ).
fof(f2398,plain,
! [X0] :
( ~ c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF7,sF2)
| c_in(sF0,hAPP(X0,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),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_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2389,f856]) ).
fof(f2402,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF2,tc_bool)))
| ~ c_in(c_Fun_Ocomp(X0,X1,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(X0,X1,X3,X4,X5)),sF2)
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7)),sF2)
| c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,hAPP(X1,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7))),sF2)
| X6 = X7 ),
inference(forward_demodulation,[],[f2393,f846]) ).
fof(f2407,plain,
! [X0] :
( ~ c_in(sF6,sF7,sF2)
| c_in(sF0,hAPP(X0,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),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_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f2398,f854]) ).
fof(f2411,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,hAPP(X1,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7))),sF2)
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,c_Fun_Ocomp(X0,X1,X3,X4,X5),X6,X7)),sF2)
| c_in(c_Pair(X6,X7,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X7,X6,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(c_Fun_Ocomp(X0,X1,X3,X4,X5)),sF2)
| ~ c_in(c_Fun_Ocomp(X0,X1,X3,X4,X5),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| X6 = X7 ),
inference(forward_demodulation,[],[f2402,f848]) ).
fof(f2416,plain,
( ! [X0] :
( c_in(sF0,hAPP(X0,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),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_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f2407,f868]) ).
fof(f2423,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__local__X3__1(X0,v_P____,v_b____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f2416,f846]) ).
fof(f2429,plain,
( ! [X0] :
( c_in(sF0,v_F(X0),sF2)
| c_in(sF0,hAPP(X0,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f2423,f842]) ).
fof(f2434,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__local__X3__1(X0,v_P____,v_b____,v_a____)),sF2)
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f2429,f846]) ).
fof(f2435,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__local__X3__1(X0,v_P____,v_b____,v_a____)),sF2)
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f2434,f848]) ).
fof(f2436,plain,
( ! [X0] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),sF2)
| c_in(sF0,hAPP(X0,v_sko__local__X3__1(X0,v_P____,v_b____,v_a____)),sF2)
| c_in(sF0,v_F(X0),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)) )
| ~ spl8_2 ),
inference(forward_demodulation,[],[f2435,f846]) ).
fof(f2510,plain,
( ! [X2,X3,X0,X1,X4] :
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(c_Fun_Ocomp(X0,X1,X2,X3,X4),v_P____,v_b____,v_a____)),sF2)
| c_in(sF0,hAPP(X0,hAPP(X1,v_sko__local__X3__1(c_Fun_Ocomp(X0,X1,X2,X3,X4),v_P____,v_b____,v_a____))),sF2)
| c_in(sF0,v_F(c_Fun_Ocomp(X0,X1,X2,X3,X4)),sF2)
| ~ c_in(c_Fun_Ocomp(X0,X1,X2,X3,X4),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)) )
| ~ spl8_2 ),
inference(superposition,[],[f2436,f751]) ).
fof(f2575,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,sF4,X0,X1)),sF2)
| c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF1,hAPP(v_P____,v_sko__local__X3__1(X2,sF4,X0,X1))),sF2)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(sF4),sF2)
| ~ c_in(sF4,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| X0 = X1 ),
inference(superposition,[],[f2411,f850]) ).
fof(f2580,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,sF4,X0,X1)),sF2)
| c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF1,hAPP(v_P____,v_sko__local__X3__1(X2,sF4,X0,X1))),sF2)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(sF4),sF2)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f2575,f952]) ).
fof(f2588,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF4,v_sko__local__X3__1(X2,sF4,X0,X1)),sF2)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,sF4,X0,X1)),sF2)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(sF4),sF2)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| X0 = X1 ),
inference(forward_demodulation,[],[f2580,f957]) ).
fof(f2594,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF4,v_sko__local__X3__1(X2,sF4,X0,X1)),sF2)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__local__X3__1(X2,sF4,X0,X1)),sF2)
| ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF5,sF2)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(X2),sF2)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| X0 = X1 ),
inference(forward_demodulation,[],[f2588,f852]) ).
fof(f2608,plain,
! [X0] :
( c_in(sF6,hAPP(X0,v_sko__local__X3__1(X0,sF4,v_a____,v_b____)),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF4,v_sko__local__X3__1(X0,sF4,v_a____,v_b____)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF5,sF2)
| c_in(sF6,v_F(X0),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| v_b____ = v_a____ ),
inference(superposition,[],[f2594,f854]) ).
fof(f2614,plain,
! [X0] :
( c_in(sF6,hAPP(X0,v_sko__local__X3__1(X0,sF4,v_a____,v_b____)),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(sF4,v_sko__local__X3__1(X0,sF4,v_a____,v_b____)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF5,sF2)
| c_in(sF6,v_F(X0),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)) ),
inference(forward_subsumption_resolution,[],[f2608,f740]) ).
fof(f2616,plain,
! [X0] :
( c_in(sF0,hAPP(sF4,v_sko__local__X3__1(X0,sF4,v_a____,v_b____)),sF2)
| c_in(sF6,hAPP(X0,v_sko__local__X3__1(X0,sF4,v_a____,v_b____)),sF2)
| ~ c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF5,sF2)
| c_in(sF6,v_F(X0),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)) ),
inference(forward_demodulation,[],[f2614,f842]) ).
fof(f3046,plain,
! [X0] : hAPP(sF1,hAPP(sF1,X0)) = X0,
inference(superposition,[],[f749,f844]) ).
fof(f3058,plain,
! [X0] : hAPP(v_P____,X0) = hAPP(sF1,hAPP(sF4,X0)),
inference(superposition,[],[f3046,f957]) ).
fof(f5382,plain,
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| c_in(sF0,hAPP(sF1,hAPP(v_P____,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____))),sF2)
| c_in(sF0,v_F(sF4),sF2)
| ~ c_in(sF4,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ spl8_2 ),
inference(superposition,[],[f2510,f850]) ).
fof(f5397,plain,
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| c_in(sF0,hAPP(sF1,hAPP(v_P____,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____))),sF2)
| c_in(sF0,v_F(sF4),sF2)
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f5382,f952]) ).
fof(f5401,plain,
( c_in(sF0,hAPP(sF4,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| c_in(sF0,v_F(sF4),sF2)
| ~ spl8_2 ),
inference(forward_demodulation,[],[f5397,f957]) ).
fof(f5403,plain,
( c_in(sF0,sF5,sF2)
| c_in(sF0,hAPP(sF4,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| ~ spl8_2 ),
inference(forward_demodulation,[],[f5401,f852]) ).
fof(f5405,plain,
( c_in(sF0,hAPP(sF4,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| spl8_1
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f5403,f863]) ).
fof(f5407,definition,
( spl8_12
<=> c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2) ),
introduced(definition,[new_symbols(definition,[spl8_12])],[avatar_definition]) ).
fof(f5409,plain,
( c_in(c_Pair(v_b____,v_c____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| ~ spl8_12 ),
inference(avatar_component_clause,[],[f5407]) ).
fof(f5411,definition,
( spl8_13
<=> c_in(sF0,hAPP(sF4,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2) ),
introduced(definition,[new_symbols(definition,[spl8_13])],[avatar_definition]) ).
fof(f5412,plain,
( ~ c_in(sF0,hAPP(sF4,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| spl8_13 ),
inference(avatar_component_clause,[],[f5411]) ).
fof(f5413,plain,
( c_in(sF0,hAPP(sF4,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| ~ spl8_13 ),
inference(avatar_component_clause,[],[f5411]) ).
fof(f5415,plain,
( spl8_12
| spl8_13
| spl8_1
| ~ spl8_2 ),
inference(avatar_split_clause,[],[f5405,f866,f862,f5411,f5407]) ).
fof(f5428,plain,
! [X0] :
( ~ c_in(sF0,sF5,sF2)
| c_in(sF0,hAPP(sF4,v_sko__local__X3__1(X0,sF4,v_a____,v_b____)),sF2)
| c_in(sF6,hAPP(X0,v_sko__local__X3__1(X0,sF4,v_a____,v_b____)),sF2)
| c_in(sF6,v_F(X0),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)) ),
inference(forward_demodulation,[],[f2616,f842]) ).
fof(f5464,plain,
( ! [X0] :
( c_in(sF6,hAPP(X0,v_sko__local__X3__1(X0,sF4,v_a____,v_b____)),sF2)
| c_in(sF0,hAPP(sF4,v_sko__local__X3__1(X0,sF4,v_a____,v_b____)),sF2)
| c_in(sF6,v_F(X0),sF2)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3)) )
| ~ spl8_1 ),
inference(forward_subsumption_resolution,[],[f5428,f864]) ).
fof(f6322,plain,
! [X0] :
( ~ c_in(sF0,hAPP(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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),X0,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(superposition,[],[f747,f842]) ).
fof(f6323,plain,
! [X0] :
( ~ c_in(sF6,hAPP(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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),X0,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(superposition,[],[f747,f854]) ).
fof(f6329,plain,
! [X0] :
( ~ c_in(sF6,hAPP(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f6323,f846]) ).
fof(f6330,plain,
! [X0] :
( ~ c_in(sF0,hAPP(c_Relation_Oconverse(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f6322,f846]) ).
fof(f6342,plain,
! [X0] :
( ~ c_in(sF6,hAPP(sF1,X0),sF2)
| c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f6329,f844]) ).
fof(f6343,plain,
! [X0] :
( ~ c_in(sF0,hAPP(sF1,X0),sF2)
| c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f6330,f844]) ).
fof(f6354,plain,
! [X0] :
( c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0,sF2)
| ~ c_in(sF6,hAPP(sF1,X0),sF2) ),
inference(forward_demodulation,[],[f6342,f846]) ).
fof(f6355,plain,
! [X0] :
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0,sF2)
| ~ c_in(sF0,hAPP(sF1,X0),sF2) ),
inference(forward_demodulation,[],[f6343,f846]) ).
fof(f6366,plain,
! [X0] :
( ~ c_in(sF6,hAPP(sF1,X0),sF2)
| c_in(sF0,X0,sF2) ),
inference(forward_demodulation,[],[f6354,f842]) ).
fof(f6367,plain,
! [X0] :
( ~ c_in(sF0,hAPP(sF1,X0),sF2)
| c_in(sF6,X0,sF2) ),
inference(forward_demodulation,[],[f6355,f854]) ).
fof(f6519,plain,
! [X0] :
( ~ c_in(sF6,hAPP(v_P____,X0),sF2)
| c_in(sF0,hAPP(sF4,X0),sF2) ),
inference(superposition,[],[f6366,f3058]) ).
fof(f6529,plain,
! [X0] :
( ~ c_in(sF0,hAPP(sF4,X0),sF2)
| c_in(sF6,hAPP(v_P____,X0),sF2) ),
inference(superposition,[],[f6367,f957]) ).
fof(f7802,plain,
( c_in(sF0,hAPP(sF4,v_sko__local__X3__1(v_P____,sF4,v_a____,v_b____)),sF2)
| c_in(sF0,hAPP(sF4,v_sko__local__X3__1(v_P____,sF4,v_a____,v_b____)),sF2)
| c_in(sF6,v_F(v_P____),sF2)
| ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ spl8_1 ),
inference(resolution,[],[f6519,f5464]) ).
fof(f7807,plain,
( c_in(sF0,hAPP(sF4,v_sko__local__X3__1(v_P____,sF4,v_a____,v_b____)),sF2)
| c_in(sF6,v_F(v_P____),sF2)
| ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ spl8_1 ),
inference(duplicate_literal_removal,[],[f7802]) ).
fof(f7811,plain,
( c_in(sF0,hAPP(sF4,v_sko__local__X3__1(v_P____,sF4,v_a____,v_b____)),sF2)
| c_in(sF6,v_F(v_P____),sF2)
| ~ spl8_1 ),
inference(forward_subsumption_resolution,[],[f7807,f961]) ).
fof(f7825,plain,
( c_in(sF6,sF7,sF2)
| c_in(sF0,hAPP(sF4,v_sko__local__X3__1(v_P____,sF4,v_a____,v_b____)),sF2)
| ~ spl8_1 ),
inference(forward_demodulation,[],[f7811,f856]) ).
fof(f7837,plain,
( c_in(sF0,hAPP(sF4,v_sko__local__X3__1(v_P____,sF4,v_a____,v_b____)),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f7825,f867]) ).
fof(f7843,plain,
( c_in(sF6,hAPP(v_P____,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| ~ spl8_13 ),
inference(resolution,[],[f5413,f6529]) ).
fof(f7844,plain,
( c_in(sF6,hAPP(v_P____,v_sko__local__X3__1(v_P____,sF4,v_a____,v_b____)),sF2)
| ~ spl8_1
| spl8_2 ),
inference(resolution,[],[f7837,f6529]) ).
fof(f7847,plain,
( ~ c_in(sF4,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(sF6,v_F(v_P____),sF2)
| ~ c_in(sF0,v_F(sF4),sF2)
| ~ c_in(sF0,hAPP(sF4,v_sko__local__X3__1(v_P____,sF4,v_a____,v_b____)),sF2)
| ~ spl8_1
| spl8_2 ),
inference(resolution,[],[f7844,f997]) ).
fof(f7849,plain,
( ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| c_in(sF6,v_F(v_P____),sF2)
| ~ c_in(sF0,v_F(sF4),sF2)
| ~ c_in(sF0,hAPP(sF4,v_sko__local__X3__1(v_P____,sF4,v_a____,v_b____)),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f7847,f952]) ).
fof(f7852,plain,
( c_in(sF6,v_F(v_P____),sF2)
| ~ c_in(sF0,v_F(sF4),sF2)
| ~ c_in(sF0,hAPP(sF4,v_sko__local__X3__1(v_P____,sF4,v_a____,v_b____)),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f7849,f961]) ).
fof(f7855,plain,
( c_in(sF6,v_F(v_P____),sF2)
| ~ c_in(sF0,v_F(sF4),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f7852,f7837]) ).
fof(f7858,plain,
( c_in(sF6,sF7,sF2)
| ~ c_in(sF0,v_F(sF4),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_demodulation,[],[f7855,f856]) ).
fof(f7862,plain,
( ~ c_in(sF0,v_F(sF4),sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f7858,f867]) ).
fof(f7863,plain,
( ~ c_in(sF0,sF5,sF2)
| ~ spl8_1
| spl8_2 ),
inference(forward_demodulation,[],[f7862,f852]) ).
fof(f7864,plain,
( $false
| ~ spl8_1
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f7863,f864]) ).
fof(f7865,plain,
( ~ spl8_1
| spl8_2 ),
inference(avatar_contradiction_clause,[],[f7864]) ).
fof(f8188,plain,
( ~ c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ c_in(sF0,hAPP(sF4,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| c_in(sF0,v_F(sF4),sF2)
| ~ c_in(sF6,v_F(v_P____),sF2)
| ~ c_in(sF4,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ spl8_13 ),
inference(resolution,[],[f7843,f996]) ).
fof(f8190,plain,
( ~ c_in(sF0,hAPP(sF4,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| c_in(sF0,v_F(sF4),sF2)
| ~ c_in(sF6,v_F(v_P____),sF2)
| ~ c_in(sF4,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ spl8_13 ),
inference(forward_subsumption_resolution,[],[f8188,f961]) ).
fof(f8192,plain,
( c_in(sF0,v_F(sF4),sF2)
| ~ c_in(sF6,v_F(v_P____),sF2)
| ~ c_in(sF4,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF3))
| ~ spl8_13 ),
inference(forward_subsumption_resolution,[],[f8190,f5413]) ).
fof(f8194,plain,
( c_in(sF0,v_F(sF4),sF2)
| ~ c_in(sF6,v_F(v_P____),sF2)
| ~ spl8_13 ),
inference(forward_subsumption_resolution,[],[f8192,f952]) ).
fof(f8196,plain,
( c_in(sF0,sF5,sF2)
| ~ c_in(sF6,v_F(v_P____),sF2)
| ~ spl8_13 ),
inference(forward_demodulation,[],[f8194,f852]) ).
fof(f8198,plain,
( ~ c_in(sF6,v_F(v_P____),sF2)
| spl8_1
| ~ spl8_13 ),
inference(forward_subsumption_resolution,[],[f8196,f863]) ).
fof(f8199,plain,
( ~ c_in(sF6,sF7,sF2)
| spl8_1
| ~ spl8_13 ),
inference(forward_demodulation,[],[f8198,f856]) ).
fof(f8200,plain,
( $false
| spl8_1
| ~ spl8_2
| ~ spl8_13 ),
inference(forward_subsumption_resolution,[],[f8199,f868]) ).
fof(f8201,plain,
( spl8_1
| ~ spl8_2
| ~ spl8_13 ),
inference(avatar_contradiction_clause,[],[f8200]) ).
fof(f8202,plain,
( c_in(sF6,hAPP(v_P____,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| ~ spl8_12 ),
inference(resolution,[],[f5409,f1057]) ).
fof(f8206,plain,
( c_in(sF0,hAPP(sF4,v_sko__local__X3__1(sF4,v_P____,v_b____,v_a____)),sF2)
| ~ spl8_12 ),
inference(resolution,[],[f8202,f6519]) ).
fof(f8207,plain,
( $false
| ~ spl8_12
| spl8_13 ),
inference(forward_subsumption_resolution,[],[f8206,f5412]) ).
fof(f8208,plain,
( ~ spl8_12
| spl8_13 ),
inference(avatar_contradiction_clause,[],[f8207]) ).
cnf(s1,plain,
( spl8_1
| spl8_2 ),
inference(sat_conversion,[],[f869]) ).
cnf(s2,plain,
( ~ spl8_1
| ~ spl8_2 ),
inference(sat_conversion,[],[f870]) ).
cnf(s9,plain,
( spl8_1
| ~ spl8_2
| spl8_12
| spl8_13 ),
inference(sat_conversion,[],[f5415]) ).
cnf(s39,plain,
( ~ spl8_1
| spl8_2 ),
inference(sat_conversion,[],[f7865]) ).
cnf(s48,plain,
( spl8_1
| ~ spl8_2
| ~ spl8_13 ),
inference(sat_conversion,[],[f8201]) ).
cnf(s49,plain,
( ~ spl8_12
| spl8_13 ),
inference(sat_conversion,[],[f8208]) ).
cnf(s50,plain,
( ~ spl8_2
| spl8_13
| spl8_1 ),
inference(rat,[],[s49,s9]) ).
cnf(s51,plain,
( ~ spl8_2
| spl8_1 ),
inference(rat,[],[s50,s48]) ).
cnf(s52,plain,
spl8_1,
inference(rat,[],[s51,s1]) ).
cnf(s53,plain,
spl8_2,
inference(rat,[],[s39,s52]) ).
cnf(s55,plain,
$false,
inference(rat,[],[s2,s53,s52]) ).
fof(f8209,plain,
$false,
inference(avatar_sat_refutation,[],[s55]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT063-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n009.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 23:36:00 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.64/2.22 % (2528212)Input is clausal, will run a generic CNF schedule.
% 9.64/2.22 % (2528217)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=3034430298:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.64/2.22 % (2528219)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=35631711:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.64/2.22 % (2528220)lrs+10_1_sil=8000:sp=occurrence:random_seed=2375420717:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.64/2.22 % (2528218)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3861733656:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.64/2.22 % (2528221)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3783160771:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.64/2.22 % (2528223)dis-21_1_sil=8000:lcm=predicate:random_seed=680835821:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 9.64/2.22 % (2528222)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3661736077:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.64/2.22 % (2528220)Instruction limit reached!
% 9.64/2.22 % (2528220)------------------------------
% 9.64/2.22 % (2528220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528220)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528220)Termination reason: Instruction limit
% 9.64/2.22 % (2528220)Termination phase: Saturation
% 9.64/2.22 % (2528220)Time elapsed: 0.072 s
% 9.64/2.22 % (2528220)Peak memory usage: 89 MB
% 9.64/2.22 % (2528220)Instructions burned: 108 (million)
% 9.64/2.22 % (2528223)Instruction limit reached!
% 9.64/2.22 % (2528223)------------------------------
% 9.64/2.22 % (2528223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528223)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528223)Termination reason: Instruction limit
% 9.64/2.22 % (2528223)Termination phase: Saturation
% 9.64/2.22 % (2528223)Time elapsed: 0.066 s
% 9.64/2.22 % (2528223)Peak memory usage: 89 MB
% 9.64/2.22 % (2528223)Instructions burned: 118 (million)
% 9.64/2.22 % (2528221)Instruction limit reached!
% 9.64/2.22 % (2528221)------------------------------
% 9.64/2.22 % (2528221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528221)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528221)Termination reason: Instruction limit
% 9.64/2.22 % (2528221)Termination phase: Saturation
% 9.64/2.22 % (2528221)Time elapsed: 0.076 s
% 9.64/2.22 % (2528221)Peak memory usage: 89 MB
% 9.64/2.22 % (2528221)Instructions burned: 115 (million)
% 9.64/2.22 % (2528222)Instruction limit reached!
% 9.64/2.22 % (2528222)------------------------------
% 9.64/2.22 % (2528222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528222)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528222)Termination reason: Instruction limit
% 9.64/2.22 % (2528222)Termination phase: Saturation
% 9.64/2.22 % (2528222)Time elapsed: 0.122 s
% 9.64/2.22 % (2528222)Peak memory usage: 89 MB
% 9.64/2.22 % (2528222)Instructions burned: 180 (million)
% 9.64/2.22 % (2528231)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=2681726970:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.64/2.22 % (2528233)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3417242766:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 9.64/2.22 % (2528232)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3300351296:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 9.64/2.22 % (2528231)Refutation not found, incomplete strategy
% 9.64/2.22 % (2528231)------------------------------
% 9.64/2.22 % (2528231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528231)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528231)Termination reason: Refutation not found, incomplete strategy
% 9.64/2.22 % (2528231)Time elapsed: 0.008 s
% 9.64/2.22 % (2528231)Peak memory usage: 88 MB
% 9.64/2.22 % (2528231)Instructions burned: 12 (million)
% 9.64/2.22 % (2528234)lrs+10_64_to=lpo:sil=8000:random_seed=3430029836:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 9.64/2.22 % (2528232)Instruction limit reached!
% 9.64/2.22 % (2528232)------------------------------
% 9.64/2.22 % (2528232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528232)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528232)Termination reason: Instruction limit
% 9.64/2.22 % (2528232)Termination phase: Saturation
% 9.64/2.22 % (2528232)Time elapsed: 0.103 s
% 9.64/2.22 % (2528232)Peak memory usage: 90 MB
% 9.64/2.22 % (2528232)Instructions burned: 189 (million)
% 9.64/2.22 % (2528233)Instruction limit reached!
% 9.64/2.22 % (2528233)------------------------------
% 9.64/2.22 % (2528233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528233)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528233)Termination reason: Instruction limit
% 9.64/2.22 % (2528233)Termination phase: Saturation
% 9.64/2.22 % (2528233)Time elapsed: 0.125 s
% 9.64/2.22 % (2528233)Peak memory usage: 89 MB
% 9.64/2.22 % (2528233)Instructions burned: 219 (million)
% 9.64/2.22 % (2528234)Instruction limit reached!
% 9.64/2.22 % (2528234)------------------------------
% 9.64/2.22 % (2528234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528234)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528234)Termination reason: Instruction limit
% 9.64/2.22 % (2528234)Termination phase: Saturation
% 9.64/2.22 % (2528234)Time elapsed: 0.079 s
% 9.64/2.22 % (2528234)Peak memory usage: 90 MB
% 9.64/2.22 % (2528234)Instructions burned: 127 (million)
% 9.64/2.22 % (2528231)------------------------------
% 9.64/2.22 % (2528231)------------------------------
% 9.64/2.22 % (2528239)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3323596807:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 9.64/2.22 % (2528240)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=86941066:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 9.64/2.22 % (2528241)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=190572498:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 9.64/2.22 % (2528240)Instruction limit reached!
% 9.64/2.22 % (2528240)------------------------------
% 9.64/2.22 % (2528240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528240)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528240)Termination reason: Instruction limit
% 9.64/2.22 % (2528240)Termination phase: Saturation
% 9.64/2.22 % (2528240)Time elapsed: 0.102 s
% 9.64/2.22 % (2528240)Peak memory usage: 91 MB
% 9.64/2.22 % (2528240)Instructions burned: 158 (million)
% 9.64/2.22 % (2528239)Instruction limit reached!
% 9.64/2.22 % (2528239)------------------------------
% 9.64/2.22 % (2528239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528239)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528239)Termination reason: Instruction limit
% 9.64/2.22 % (2528239)Termination phase: Saturation
% 9.64/2.22 % (2528239)Time elapsed: 0.134 s
% 9.64/2.22 % (2528239)Peak memory usage: 90 MB
% 9.64/2.22 % (2528239)Instructions burned: 194 (million)
% 9.64/2.22 % (2528243)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=4270349710:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 9.64/2.22 % (2528243)Instruction limit reached!
% 9.64/2.22 % (2528243)------------------------------
% 9.64/2.22 % (2528243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528243)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528243)Termination reason: Instruction limit
% 9.64/2.22 % (2528243)Termination phase: Saturation
% 9.64/2.22 % (2528243)Time elapsed: 0.061 s
% 9.64/2.22 % (2528243)Peak memory usage: 89 MB
% 9.64/2.22 % (2528243)Instructions burned: 107 (million)
% 9.64/2.22 % (2528246)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=540803681:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 9.64/2.22 % (2528247)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2979830940:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 9.64/2.22 % (2528246)Instruction limit reached!
% 9.64/2.22 % (2528246)------------------------------
% 9.64/2.22 % (2528246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528246)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528246)Termination reason: Instruction limit
% 9.64/2.22 % (2528246)Termination phase: Saturation
% 9.64/2.22 % (2528246)Time elapsed: 0.069 s
% 9.64/2.22 % (2528246)Peak memory usage: 90 MB
% 9.64/2.22 % (2528246)Instructions burned: 108 (million)
% 9.64/2.22 % (2528249)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2248701741:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 9.64/2.22 % (2528247)Instruction limit reached!
% 9.64/2.22 % (2528247)------------------------------
% 9.64/2.22 % (2528247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528247)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528247)Termination reason: Instruction limit
% 9.64/2.22 % (2528247)Termination phase: Saturation
% 9.64/2.22 % (2528247)Time elapsed: 0.148 s
% 9.64/2.22 % (2528247)Peak memory usage: 90 MB
% 9.64/2.22 % (2528247)Instructions burned: 242 (million)
% 9.64/2.22 % (2528252)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1775251677:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 9.64/2.22 % (2528217)First to succeed.
% 9.64/2.22 % (2528217)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2528212"
% 9.64/2.22 % (2528254)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2853492960:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 9.64/2.22 % (2528252)Instruction limit reached!
% 9.64/2.22 % (2528252)------------------------------
% 9.64/2.22 % (2528252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.64/2.22 % (2528252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.64/2.22 % (2528252)CaDiCaL version: 2.1.3
% 9.64/2.22 % (2528252)Termination reason: Instruction limit
% 9.64/2.22 % (2528252)Termination phase: Saturation
% 9.64/2.22 % (2528252)Time elapsed: 0.086 s
% 9.64/2.22 % (2528252)Peak memory usage: 89 MB
% 9.64/2.22 % (2528252)Instructions burned: 135 (million)
% 9.64/2.22 % (2528217)Refutation found. Thanks to Tanya!
% 9.64/2.22 % SZS status Unsatisfiable for theBenchmark
% 9.64/2.22 % SZS output start Proof for theBenchmark
% See solution above
% 9.98/2.32 % (2528217)------------------------------
% 9.98/2.32 % (2528217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.98/2.32 % (2528217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.98/2.32 % (2528217)CaDiCaL version: 2.1.3
% 9.98/2.32 % (2528217)Termination reason: Refutation
% 9.98/2.32 % (2528217)Time elapsed: 1.043 s
% 9.98/2.32 % (2528217)Peak memory usage: 142 MB
% 9.98/2.32 % (2528217)Instructions burned: 2850 (million)
% 9.98/2.32 % (2528217)------------------------------
% 9.98/2.32 % (2528217)------------------------------
% 9.98/2.32 % (2528212)Success in time 1.366 s
% 9.98/2.32 % Vampire exiting
%------------------------------------------------------------------------------