%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SCT069-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:37:28 PM UTC 2026
% Result : Unsatisfiable 10.98s 5.69s
% Output : Refutation 10.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 17
% Syntax : Number of formulae : 69 ( 12 unt; 4 def)
% Number of atoms : 206 ( 14 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 247 ( 110 ~; 133 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 5 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-4 aty)
% Number of variables : 36 ( 0 sgn 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f738,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_a_H____,v_b_H____,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) ).
fof(f739,axiom,
! [X0] :
( c_in(c_Pair(v_a_H____,v_b_H____,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_CHAINED_0) ).
fof(f740,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(f741,axiom,
c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_02) ).
fof(f743,axiom,
v_a____ != v_b____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_04) ).
fof(f744,axiom,
! [X2,X3,X0,X1] :
( ~ 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(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X3,v_sko__CHAINED__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__CHAINED__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/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_3) ).
fof(f745,axiom,
! [X2,X3,X0,X1] :
( 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(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),hAPP(X2,v_sko__CHAINED__1(X3,X2,X1,X0)),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),hAPP(X3,v_sko__CHAINED__1(X3,X2,X1,X0)),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)))
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_2) ).
fof(f746,plain,
! [X2,X3,X0,X1] :
( ~ 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__CHAINED__1(X3,X2,X1,X0)),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),hAPP(X3,v_sko__CHAINED__1(X3,X2,X1,X0)),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)))
| X0 = X1 ),
inference(reorient_equations,[],[f745]) ).
fof(f747,axiom,
! [X2,X3,X0,X1] :
( ~ 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(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X3,v_sko__CHAINED__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__CHAINED__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/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_1_05) ).
fof(f748,axiom,
! [X2,X3,X0,X1] :
( 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(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),hAPP(X2,v_sko__CHAINED__1(X3,X2,X1,X0)),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),hAPP(X3,v_sko__CHAINED__1(X3,X2,X1,X0)),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)))
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_06) ).
fof(f749,plain,
! [X2,X3,X0,X1] :
( ~ 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__CHAINED__1(X3,X2,X1,X0)),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),hAPP(X3,v_sko__CHAINED__1(X3,X2,X1,X0)),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)))
| X0 = X1 ),
inference(reorient_equations,[],[f748]) ).
fof(f750,axiom,
v_b____ = v_a_H____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_1_07) ).
fof(f751,axiom,
v_a____ = v_b_H____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_08) ).
fof(f752,negated_conjecture,
( ~ c_in(c_Pair(v_a_H____,v_b_H____,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_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f753,negated_conjecture,
( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,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(f863,plain,
! [X0] :
( c_in(c_Pair(v_b_H____,v_a_H____,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_a_H____,v_b_H____,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(definition_unfolding,[],[f738,f751,f750]) ).
fof(f864,plain,
! [X0] :
( ~ c_in(c_Pair(v_b_H____,v_a_H____,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_a_H____,v_b_H____,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(definition_unfolding,[],[f739,f751,f750]) ).
fof(f865,plain,
v_a_H____ != v_b_H____,
inference(definition_unfolding,[],[f743,f751,f750]) ).
fof(f866,plain,
( ~ c_in(c_Pair(v_a_H____,v_b_H____,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_H____,v_a_H____,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)) ),
inference(definition_unfolding,[],[f752,f751,f750]) ).
fof(f867,plain,
( c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,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)) ),
inference(definition_unfolding,[],[f753,f751,f750]) ).
fof(f871,definition,
( spl0_1
<=> c_in(c_Pair(v_a_H____,v_b_H____,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)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f873,plain,
( c_in(c_Pair(v_a_H____,v_b_H____,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))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f871]) ).
fof(f875,definition,
( spl0_2
<=> c_in(c_Pair(v_b_H____,v_a_H____,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)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f877,plain,
( c_in(c_Pair(v_b_H____,v_a_H____,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))
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f875]) ).
fof(f878,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f867,f875,f871]) ).
fof(f922,plain,
( ! [X0] :
( c_in(c_Pair(v_a_H____,v_b_H____,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_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(X0,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(X0,v_P____,v_a_H____,v_b_H____)),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_a_H____ = v_b_H____ )
| ~ spl0_2 ),
inference(resolution,[],[f747,f877]) ).
fof(f923,plain,
( ! [X0] :
( ~ 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_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(X0,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(X0,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,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)) )
| ~ spl0_2 ),
inference(global_subsumption,[],[f922,f741,f865]) ).
fof(f924,plain,
( c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,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))
| ~ spl0_2 ),
inference(resolution,[],[f923,f740]) ).
fof(f939,plain,
( c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ spl0_2 ),
inference(global_subsumption,[],[f924,f877,f866]) ).
fof(f941,definition,
( spl0_6
<=> c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f943,plain,
( c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f941]) ).
fof(f945,definition,
( spl0_7
<=> c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f946,plain,
( ~ c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| spl0_7 ),
inference(avatar_component_clause,[],[f945]) ).
fof(f947,plain,
( c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f945]) ).
fof(f948,plain,
( spl0_6
| spl0_7
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f939,f875,f945,f941]) ).
fof(f973,plain,
( ! [X0] :
( c_in(c_Pair(v_b_H____,v_a_H____,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_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(v_P_H____,X0,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,X0,v_a_H____,v_b_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(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)))
| v_a_H____ = v_b_H____ )
| ~ spl0_1 ),
inference(resolution,[],[f873,f746]) ).
fof(f976,plain,
( ! [X0] :
( ~ c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(v_P_H____,X0,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b_H____,v_a_H____,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_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,X0,v_a_H____,v_b_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))) )
| ~ spl0_1 ),
inference(global_subsumption,[],[f973,f740,f865]) ).
fof(f979,plain,
( c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),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(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ spl0_1 ),
inference(resolution,[],[f976,f863]) ).
fof(f980,plain,
( c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_F(v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),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)))
| ~ spl0_1 ),
inference(duplicate_literal_removal,[],[f979]) ).
fof(f981,plain,
( ~ c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ spl0_1 ),
inference(global_subsumption,[],[f980,f873,f741,f866]) ).
fof(f982,plain,
( ~ spl0_6
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f981,f871,f941]) ).
fof(f1003,plain,
( ! [X0] :
( c_in(c_Pair(v_a_H____,v_b_H____,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_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(X0,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(X0,v_P____,v_a_H____,v_b_H____)),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_a_H____ = v_b_H____ )
| ~ spl0_2 ),
inference(resolution,[],[f877,f744]) ).
fof(f1004,plain,
( ! [X0] :
( ~ c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(X0,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(X0,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,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))) )
| ~ spl0_2 ),
inference(global_subsumption,[],[f1003,f741,f865]) ).
fof(f1008,plain,
( c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ spl0_7 ),
inference(resolution,[],[f947,f864]) ).
fof(f1009,plain,
( spl0_6
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f1008,f945,f941]) ).
fof(f1010,plain,
( ~ c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,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)))
| ~ spl0_2
| ~ spl0_6 ),
inference(resolution,[],[f943,f1004]) ).
fof(f1011,plain,
( ~ c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ spl0_2
| ~ spl0_6 ),
inference(global_subsumption,[],[f1010,f877,f740,f866]) ).
fof(f1012,plain,
( ~ spl0_7
| ~ spl0_2
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f1011,f941,f875,f945]) ).
fof(f1015,plain,
( ~ c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| spl0_7 ),
inference(resolution,[],[f946,f863]) ).
fof(f1016,plain,
( ~ spl0_6
| spl0_7 ),
inference(avatar_split_clause,[],[f1015,f945,f941]) ).
fof(f1017,plain,
( ! [X0] :
( c_in(c_Pair(v_b_H____,v_a_H____,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_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(v_P_H____,X0,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,X0,v_a_H____,v_b_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(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)))
| v_a_H____ = v_b_H____ )
| ~ spl0_1 ),
inference(resolution,[],[f873,f749]) ).
fof(f1024,plain,
( ! [X0] :
( ~ 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_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X0,v_sko__CHAINED__1(v_P_H____,X0,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,X0,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b_H____,v_a_H____,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)) )
| ~ spl0_1 ),
inference(global_subsumption,[],[f1017,f740,f865]) ).
fof(f1033,plain,
( c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(v_b_H____,v_a_H____,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))
| ~ spl0_1 ),
inference(resolution,[],[f1024,f741]) ).
fof(f1034,plain,
( c_in(c_Pair(v_b_H____,v_a_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ spl0_1 ),
inference(global_subsumption,[],[f1033,f873,f981,f866]) ).
fof(f1044,plain,
( spl0_7
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1034,f871,f945]) ).
cnf(s24,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f878]) ).
cnf(s598,plain,
( ~ spl0_2
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f948]) ).
cnf(s626,plain,
( ~ spl0_1
| ~ spl0_6 ),
inference(sat_conversion,[],[f982]) ).
cnf(s646,plain,
( spl0_6
| ~ spl0_7 ),
inference(sat_conversion,[],[f1009]) ).
cnf(s650,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_7 ),
inference(sat_conversion,[],[f1012]) ).
cnf(s653,plain,
( ~ spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f1016]) ).
cnf(s677,plain,
( ~ spl0_1
| spl0_7 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s678,plain,
( spl0_6
| ~ spl0_2 ),
inference(rat,[],[s598,s646]) ).
cnf(s679,plain,
~ spl0_2,
inference(rat,[],[s650,s653,s678]) ).
cnf(s680,plain,
spl0_1,
inference(rat,[],[s24,s679]) ).
cnf(s681,plain,
spl0_7,
inference(rat,[],[s677,s680]) ).
cnf(s682,plain,
~ spl0_6,
inference(rat,[],[s626,s680]) ).
cnf(s683,plain,
$false,
inference(rat,[],[s646,s681,s682]) ).
fof(f1045,plain,
$false,
inference(avatar_sat_refutation,[],[s683]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT069-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 23:36:46 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.56/1.78 % (1288912)Will run a generic schedule for satisfiability detection.
% 7.56/1.78 % (1288920)dis+10_1_sil=32000:sp=arity:random_seed=501805195:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.56/1.78 % (1288918)% WARNING: option uhcvi not known.
% 7.56/1.78 % (1288917)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3410724267_2999 on theBenchmark for (2999ds/0Mi)
% 7.56/1.78 % (1288918)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2552318344:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.56/1.78 % (1288919)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1259764235:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.56/1.78 % (1288921)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3254844149:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.56/1.78 % (1288923)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=987761265:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.56/1.78 % (1288922)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2761576876:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.56/1.78 % (1288920)Instruction limit reached!
% 7.56/1.78 % (1288920)------------------------------
% 7.56/1.78 % (1288920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.56/1.78 % (1288920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.78 % (1288920)CaDiCaL version: 2.1.3
% 7.56/1.78 % (1288920)Termination reason: Instruction limit
% 7.56/1.78 % (1288920)Termination phase: Saturation
% 7.56/1.78 % (1288920)Time elapsed: 0.038 s
% 7.56/1.78 % (1288920)Peak memory usage: 13 MB
% 7.56/1.78 % (1288920)Instructions burned: 105 (million)
% 7.56/1.78 % (1288931)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2840555321:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.56/1.78 % (1288921)Instruction limit reached!
% 7.56/1.78 % (1288921)------------------------------
% 7.56/1.78 % (1288921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.56/1.78 % (1288921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.78 % (1288921)CaDiCaL version: 2.1.3
% 7.56/1.78 % (1288921)Termination reason: Instruction limit
% 7.56/1.78 % (1288921)Termination phase: Saturation
% 7.56/1.78 % (1288921)Time elapsed: 0.071 s
% 7.56/1.78 % (1288921)Peak memory usage: 13 MB
% 7.56/1.78 % (1288921)Instructions burned: 117 (million)
% 7.56/1.78 % (1288922)Instruction limit reached!
% 7.56/1.78 % (1288922)------------------------------
% 7.56/1.78 % (1288922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.56/1.78 % (1288922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.78 % (1288922)CaDiCaL version: 2.1.3
% 7.56/1.78 % (1288922)Termination reason: Instruction limit
% 7.56/1.78 % (1288922)Termination phase: Saturation
% 7.56/1.78 % (1288922)Time elapsed: 0.086 s
% 7.56/1.78 % (1288922)Peak memory usage: 13 MB
% 7.56/1.78 % (1288922)Instructions burned: 134 (million)
% 7.56/1.78 % (1288933)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1321568194:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.56/1.78 % (1288923)Instruction limit reached!
% 7.56/1.78 % (1288923)------------------------------
% 7.56/1.78 % (1288923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.56/1.78 % (1288923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.78 % (1288923)CaDiCaL version: 2.1.3
% 7.56/1.78 % (1288923)Termination reason: Instruction limit
% 7.56/1.78 % (1288923)Termination phase: Saturation
% 7.56/1.78 % (1288923)Time elapsed: 0.095 s
% 7.56/1.78 % (1288923)Peak memory usage: 13 MB
% 7.56/1.78 % (1288923)Instructions burned: 160 (million)
% 7.56/1.78 % (1288934)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1625391456:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.56/1.78 % (1288936)ott-21_1_sil=16000:fs=off:random_seed=2015677588:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.56/1.78 % TRYING [1]
% 7.56/1.78 % TRYING [2]
% 7.56/1.78 % (1288933)Instruction limit reached!
% 7.56/1.78 % (1288933)------------------------------
% 7.56/1.78 % (1288933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.56/1.78 % (1288933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.73/4.22 % (1288933)CaDiCaL version: 2.1.3
% 26.73/4.22 % (1288933)Termination reason: Instruction limit
% 26.73/4.22 % (1288933)Termination phase: Saturation
% 26.73/4.22 % (1288933)Time elapsed: 0.074 s
% 26.73/4.22 % (1288933)Peak memory usage: 13 MB
% 26.73/4.22 % (1288933)Instructions burned: 131 (million)
% 26.73/4.22 % TRYING [1]
% 26.73/4.22 % (1288939)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2083164076:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 26.73/4.22 % TRYING [2]
% 26.73/4.22 % (1288936)Instruction limit reached!
% 26.73/4.22 % (1288936)------------------------------
% 26.73/4.22 % (1288936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.73/4.22 % (1288936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.73/4.22 % (1288936)CaDiCaL version: 2.1.3
% 26.73/4.22 % (1288936)Termination reason: Instruction limit
% 26.73/4.22 % (1288936)Termination phase: Saturation
% 26.73/4.22 % (1288936)Time elapsed: 0.092 s
% 26.73/4.22 % (1288936)Peak memory usage: 13 MB
% 26.73/4.22 % (1288936)Instructions burned: 181 (million)
% 26.73/4.22 % (1288931)Instruction limit reached!
% 26.73/4.22 % (1288931)------------------------------
% 26.73/4.22 % (1288931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.73/4.22 % (1288931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.73/4.22 % (1288931)CaDiCaL version: 2.1.3
% 26.73/4.22 % (1288931)Termination reason: Instruction limit
% 26.73/4.22 % (1288931)Termination phase: Finite model building constraint generation
% 26.73/4.22 % (1288931)Time elapsed: 0.180 s
% 26.73/4.22 % (1288931)Peak memory usage: 40 MB
% 26.73/4.22 % (1288931)Instructions burned: 714 (million)
% 26.73/4.22 % (1288941)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4145572726:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 26.73/4.22 % (1288942)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3195201930:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 26.73/4.22 % TRYING [3]
% 26.73/4.22 % TRYING [1]
% 26.73/4.22 % TRYING [2]
% 26.73/4.22 % (1288939)Instruction limit reached!
% 26.73/4.22 % (1288939)------------------------------
% 26.73/4.22 % (1288939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.73/4.22 % (1288939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.73/4.22 % (1288939)CaDiCaL version: 2.1.3
% 26.73/4.22 % (1288939)Termination reason: Instruction limit
% 26.73/4.22 % (1288939)Termination phase: Saturation
% 26.73/4.22 % (1288939)Time elapsed: 0.311 s
% 26.73/4.22 % (1288939)Peak memory usage: 14 MB
% 26.73/4.22 % (1288939)Instructions burned: 477 (million)
% 26.73/4.22 % (1288945)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4215393520:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 26.73/4.22 % (1288934)Instruction limit reached!
% 26.73/4.22 % (1288934)------------------------------
% 26.73/4.22 % (1288934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.73/4.22 % (1288934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.73/4.22 % (1288934)CaDiCaL version: 2.1.3
% 26.73/4.22 % (1288934)Termination reason: Instruction limit
% 26.73/4.22 % (1288934)Termination phase: Saturation
% 26.73/4.22 % (1288934)Time elapsed: 0.425 s
% 26.73/4.22 % (1288934)Peak memory usage: 17 MB
% 26.73/4.22 % (1288934)Instructions burned: 684 (million)
% 26.73/4.22 % (1288947)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1843701822:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 26.73/4.22 % (1288942)Instruction limit reached!
% 26.73/4.22 % (1288942)------------------------------
% 26.73/4.22 % (1288942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.73/4.22 % (1288942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.73/4.22 % (1288942)CaDiCaL version: 2.1.3
% 26.73/4.22 % (1288942)Termination reason: Instruction limit
% 26.73/4.22 % (1288942)Termination phase: Saturation
% 26.73/4.22 % (1288942)Time elapsed: 0.395 s
% 26.73/4.22 % (1288942)Peak memory usage: 22 MB
% 26.73/4.22 % (1288942)Instructions burned: 1180 (million)
% 26.73/4.22 % (1288941)Instruction limit reached!
% 26.73/4.22 % (1288941)------------------------------
% 26.73/4.22 % (1288941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.73/4.22 % (1288941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.73/4.22 % (1288941)CaDiCaL version: 2.1.3
% 26.73/4.22 % (1288941)Termination reason: Instruction limit
% 10.98/5.69 % (1288941)Termination phase: Finite model building SAT solving
% 10.98/5.69 % (1288941)Time elapsed: 0.406 s
% 10.98/5.69 % (1288941)Peak memory usage: 37 MB
% 10.98/5.69 % (1288941)Instructions burned: 866 (million)
% 10.98/5.69 % (1288949)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3208112735:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 10.98/5.69 % (1288950)fmb+10_1_sil=64000:random_seed=3285213962:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 10.98/5.69 % (1288945)Cannot represent all propositional literals internally
% 10.98/5.69 % (1288945)Refutation not found, incomplete strategy
% 10.98/5.69 % (1288945)------------------------------
% 10.98/5.69 % (1288945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288945)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288945)Termination reason: Refutation not found, incomplete strategy
% 10.98/5.69 % (1288945)Time elapsed: 0.179 s
% 10.98/5.69 % (1288945)Peak memory usage: 17 MB
% 10.98/5.69 % (1288945)Instructions burned: 359 (million)
% 10.98/5.69 % (1288945)------------------------------
% 10.98/5.69 % (1288945)------------------------------
% 10.98/5.69 % (1288953)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=111929320:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 10.98/5.69 % TRYING [1]
% 10.98/5.69 % TRYING [2]
% 10.98/5.69 % (1288953)Cannot represent all propositional literals internally
% 10.98/5.69 % (1288953)Refutation not found, incomplete strategy
% 10.98/5.69 % (1288953)------------------------------
% 10.98/5.69 % (1288953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288953)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288953)Termination reason: Refutation not found, incomplete strategy
% 10.98/5.69 % (1288953)Time elapsed: 0.178 s
% 10.98/5.69 % (1288953)Peak memory usage: 17 MB
% 10.98/5.69 % (1288953)Instructions burned: 359 (million)
% 10.98/5.69 % (1288953)------------------------------
% 10.98/5.69 % (1288953)------------------------------
% 10.98/5.69 % (1288949)Instruction limit reached!
% 10.98/5.69 % (1288949)------------------------------
% 10.98/5.69 % (1288949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288949)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288949)Termination reason: Instruction limit
% 10.98/5.69 % (1288949)Termination phase: Saturation
% 10.98/5.69 % (1288949)Time elapsed: 0.275 s
% 10.98/5.69 % (1288949)Peak memory usage: 19 MB
% 10.98/5.69 % (1288949)Instructions burned: 882 (million)
% 10.98/5.69 % (1288955)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3737563457:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 10.98/5.69 % (1288957)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=956548444:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 10.98/5.69 % (1288947)Instruction limit reached!
% 10.98/5.69 % (1288947)------------------------------
% 10.98/5.69 % (1288947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288947)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288947)Termination reason: Instruction limit
% 10.98/5.69 % (1288947)Termination phase: Saturation
% 10.98/5.69 % (1288947)Time elapsed: 0.453 s
% 10.98/5.69 % (1288947)Peak memory usage: 18 MB
% 10.98/5.69 % (1288947)Instructions burned: 693 (million)
% 10.98/5.69 % (1288959)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=24813467:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 10.98/5.69 % TRYING [8]
% 10.98/5.69 % (1288955)Instruction limit reached!
% 10.98/5.69 % (1288955)------------------------------
% 10.98/5.69 % (1288955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288955)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288955)Termination reason: Instruction limit
% 10.98/5.69 % (1288955)Termination phase: Finite model building constraint generation
% 10.98/5.69 % (1288955)Time elapsed: 0.369 s
% 10.98/5.69 % (1288955)Peak memory usage: 54 MB
% 10.98/5.69 % (1288955)Instructions burned: 923 (million)
% 10.98/5.69 % (1288961)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1499865384:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 10.98/5.69 % (1288961)Cannot represent all propositional literals internally
% 10.98/5.69 % (1288961)Refutation not found, incomplete strategy
% 10.98/5.69 % (1288961)------------------------------
% 10.98/5.69 % (1288961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288961)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288961)Termination reason: Refutation not found, incomplete strategy
% 10.98/5.69 % (1288961)Time elapsed: 0.186 s
% 10.98/5.69 % (1288961)Peak memory usage: 17 MB
% 10.98/5.69 % (1288961)Instructions burned: 371 (million)
% 10.98/5.69 % (1288961)------------------------------
% 10.98/5.69 % (1288961)------------------------------
% 10.98/5.69 % (1288963)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=417824998:fmbsr=2.30978:i=2174_2984 on theBenchmark for (2984ds/2174Mi)
% 10.98/5.69 % TRYING [4]
% 10.98/5.69 % TRYING [3]
% 10.98/5.69 % (1288959)Instruction limit reached!
% 10.98/5.69 % (1288959)------------------------------
% 10.98/5.69 % (1288959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288959)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288959)Termination reason: Instruction limit
% 10.98/5.69 % (1288959)Termination phase: Saturation
% 10.98/5.69 % (1288959)Time elapsed: 0.740 s
% 10.98/5.69 % (1288959)Peak memory usage: 26 MB
% 10.98/5.69 % (1288959)Instructions burned: 1472 (million)
% 10.98/5.69 % (1288965)ott-2_1_sil=16000:newcnf=on:random_seed=4201784855:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2981 on theBenchmark for (2981ds/869Mi)
% 10.98/5.69 % (1288965)Instruction limit reached!
% 10.98/5.69 % (1288965)------------------------------
% 10.98/5.69 % (1288965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288965)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288965)Termination reason: Instruction limit
% 10.98/5.69 % (1288965)Termination phase: Saturation
% 10.98/5.69 % (1288965)Time elapsed: 0.522 s
% 10.98/5.69 % (1288965)Peak memory usage: 20 MB
% 10.98/5.69 % (1288965)Instructions burned: 870 (million)
% 10.98/5.69 % (1288967)ott+10_1_sil=32000:tgt=ground:random_seed=3559121063:i=5114:av=off_2976 on theBenchmark for (2976ds/5114Mi)
% 10.98/5.69 % (1288963)Cannot represent all propositional literals internally
% 10.98/5.69 % (1288963)Refutation not found, incomplete strategy
% 10.98/5.69 % (1288963)------------------------------
% 10.98/5.69 % (1288963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288963)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288963)Termination reason: Refutation not found, incomplete strategy
% 10.98/5.69 % (1288963)Time elapsed: 0.926 s
% 10.98/5.69 % (1288963)Peak memory usage: 30 MB
% 10.98/5.69 % (1288963)Instructions burned: 1885 (million)
% 10.98/5.69 % (1288963)------------------------------
% 10.98/5.69 % (1288963)------------------------------
% 10.98/5.69 % (1288969)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=510439668:i=54282_2974 on theBenchmark for (2974ds/54282Mi)
% 10.98/5.69 % (1288957)Instruction limit reached!
% 10.98/5.69 % (1288957)------------------------------
% 10.98/5.69 % (1288957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288957)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288957)Termination reason: Instruction limit
% 10.98/5.69 % (1288957)Termination phase: Saturation
% 10.98/5.69 % (1288957)Time elapsed: 1.648 s
% 10.98/5.69 % (1288957)Peak memory usage: 44 MB
% 10.98/5.69 % (1288957)Instructions burned: 5133 (million)
% 10.98/5.69 % (1288971)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4023559864:i=3512:aac=none_2973 on theBenchmark for (2973ds/3512Mi)
% 10.98/5.69 % TRYING [1]
% 10.98/5.69 % TRYING [2]
% 10.98/5.69 % TRYING [3]
% 10.98/5.69 % (1288971)Instruction limit reached!
% 10.98/5.69 % (1288971)------------------------------
% 10.98/5.69 % (1288971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288971)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288971)Termination reason: Instruction limit
% 10.98/5.69 % (1288971)Termination phase: Saturation
% 10.98/5.69 % (1288971)Time elapsed: 1.165 s
% 10.98/5.69 % (1288971)Peak memory usage: 34 MB
% 10.98/5.69 % (1288971)Instructions burned: 3514 (million)
% 10.98/5.69 % (1288973)dis+21_1_sil=32000:sas=cadical:random_seed=3460222945:i=3773:amm=off_2961 on theBenchmark for (2961ds/3773Mi)
% 10.98/5.69 % TRYING [4]
% 10.98/5.69 % (1288973)Instruction limit reached!
% 10.98/5.69 % (1288973)------------------------------
% 10.98/5.69 % (1288973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288973)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288973)Termination reason: Instruction limit
% 10.98/5.69 % (1288973)Termination phase: Saturation
% 10.98/5.69 % (1288973)Time elapsed: 1.279 s
% 10.98/5.69 % (1288973)Peak memory usage: 40 MB
% 10.98/5.69 % (1288973)Instructions burned: 3773 (million)
% 10.98/5.69 % (1288975)ott+11_1_sil=16000:gs=on:random_seed=3116123106:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2948 on theBenchmark for (2948ds/2251Mi)
% 10.98/5.69 % (1288975) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1288912-1288975"...
% 10.98/5.69 % (1288975)...printing done.
% 10.98/5.69 % (1288975)Refutation found. Thanks to Tanya!
% 10.98/5.69 % SZS status Unsatisfiable for theBenchmark
% 10.98/5.69 % SZS output start Proof for theBenchmark
% See solution above
% 10.98/5.69 % (1288975)------------------------------
% 10.98/5.69 % (1288975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.98/5.69 % (1288975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/5.69 % (1288975)CaDiCaL version: 2.1.3
% 10.98/5.69 % (1288975)Termination reason: Refutation
% 10.98/5.69 % (1288975)Time elapsed: 0.060 s
% 10.98/5.69 % (1288975)Peak memory usage: 14 MB
% 10.98/5.69 % (1288975)Instructions burned: 136 (million)
% 10.98/5.69 % (1288912)Success in time 5.282 s
% 10.98/5.69 % Vampire exiting
%------------------------------------------------------------------------------