%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT006-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 : n011.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:43 PM UTC 2026
% Result : Unsatisfiable 59.25s 9.28s
% Output : Refutation 60.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 39
% Syntax : Number of formulae : 260 ( 94 unt; 15 def)
% Number of atoms : 483 ( 131 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 422 ( 199 ~; 211 |; 0 &)
% ( 12 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 16 ( 14 usr; 13 prp; 0-4 aty)
% Number of functors : 23 ( 23 usr; 7 con; 0-5 aty)
% Number of variables : 451 ( 0 sgn 451 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f87,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(c_COMBB(X0,X1,X2,X3,X4),X5) = hAPP(X0,hAPP(X1,X5)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBB__def_0) ).
fof(f183,axiom,
! [X0,X1] : c_Collect(c_COMBB(c_Not,X0,tc_bool,tc_bool,X1),X1) = hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),c_Collect(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__neg__eq_0) ).
fof(f245,axiom,
! [X2,X0,X1] : c_Lattices_Oupper__semilattice__class_Osup(X0,c_HOL_Ominus__class_Ominus(X1,X0,tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__Diff__cancel_0) ).
fof(f246,plain,
! [X2,X0,X1] : c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(X0,c_HOL_Ominus__class_Ominus(X1,X0,tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)),
inference(reorient_equations,[],[f245]) ).
fof(f294,axiom,
! [X2,X0,X1] : c_Set_Oinsert(X0,X1,X2) = c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X0),X2),X1,tc_fun(X2,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__def_0) ).
fof(f334,axiom,
! [X2,X3,X0,X1] : c_Set_Ovimage(X0,X1,X2,X3) = c_Collect(hAPP(c_COMBC(c_COMBB(c_in(X3),X0,X3,tc_fun(tc_fun(X3,tc_bool),tc_bool),X2),X2,tc_fun(X3,tc_bool),tc_bool),X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_vimage__def_0) ).
fof(f335,axiom,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1) = c_Collect(c_COMBB(c_Not,hAPP(c_COMBC(c_in(X0),X0,tc_fun(X0,tc_bool),tc_bool),X1),tc_bool,tc_bool,X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Compl__eq_0) ).
fof(f344,axiom,
! [X0,X1] : c_Collect(X0,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__def_0) ).
fof(f378,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(hAPP(c_COMBC(X0,X1,X2,X3),X4),X5) = hAPP(hAPP(X0,X5),X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBC__def_0) ).
fof(f379,axiom,
! [X2,X3,X0,X1] : hAPP(c_COMBK(X0,X1,X2),X3) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBK__def_0) ).
fof(f389,axiom,
! [X2,X0,X1] : c_Fun_Oinj__on(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_inj__on__empty_0) ).
fof(f420,axiom,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),hAPP(X1,X2)),c_Set_Oimage(X1,c_HOL_Ominus__class_Ominus(X3,c_Set_Oinsert(X2,c_Orderings_Obot__class_Obot(tc_fun(X4,tc_bool)),X4),tc_fun(X4,tc_bool)),X4,X0)))
| ~ c_Fun_Oinj__on(X1,c_Set_Oinsert(X2,X3,X4),X4,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f427,axiom,
! [X2,X0,X1] :
( c_HOL_Ominus__class_Ominus(c_Set_Oinsert(X0,X1,X2),c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2),tc_fun(X2,tc_bool)) = X1
| hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Diff__insert__absorb_0) ).
fof(f429,axiom,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_double__complement_0) ).
fof(f536,axiom,
! [X2,X3,X0,X1] :
( c_Set_Ovimage(c_COMBK(X0,X1,X2),X3,X2,X1) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))
| hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_vimage__const_1) ).
fof(f537,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = c_Set_Ovimage(c_COMBK(X0,X1,X2),X3,X2,X1)
| hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
inference(reorient_equations,[],[f536]) ).
fof(f550,axiom,
! [X2,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0)
| ~ hBOOL(hAPP(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__Collect__eq_0) ).
fof(f565,axiom,
! [X2,X0,X1] :
( c_Set_Oinsert(X0,c_HOL_Ominus__class_Ominus(X1,c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2),tc_fun(X2,tc_bool)),X2) = X1
| ~ hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__Diff_0) ).
fof(f571,axiom,
! [X0,X1] : c_Collect(hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1),X0) = c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_singleton__conv_0) ).
fof(f572,plain,
! [X0,X1] : c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0) = c_Collect(hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1),X0),
inference(reorient_equations,[],[f571]) ).
fof(f586,axiom,
! [X0,X1] : c_Collect(hAPP(c_fequal(X0),X1),X0) = c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_singleton__conv2_0) ).
fof(f587,plain,
! [X0,X1] : c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0) = c_Collect(hAPP(c_fequal(X0),X1),X0),
inference(reorient_equations,[],[f586]) ).
fof(f596,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_HOL_Ominus__class_Ominus(X3,X2,tc_fun(X0,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f604,axiom,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_in(X0),X1),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X2)))
| hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ComplI_0) ).
fof(f605,axiom,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X2)))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f695,axiom,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_in(X0),X1),X2))
| ~ hBOOL(hAPP(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f696,axiom,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X0))
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mem__def_0) ).
fof(f698,negated_conjecture,
! [X0] : ~ hBOOL(hAPP(hAPP(c_in(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),X0),c_Arrow__Order__Mirabelle_OLin)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f799,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),hAPP(X1,X2)),c_Set_Oimage(X1,c_HOL_Ominus__class_Ominus(X3,c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X4),X4,X4,tc_bool),X2),X4),c_Orderings_Obot__class_Obot(tc_fun(X4,tc_bool)),tc_fun(X4,tc_bool)),tc_fun(X4,tc_bool)),X4,X0)))
| ~ c_Fun_Oinj__on(X1,c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X4),X4,X4,tc_bool),X2),X4),X3,tc_fun(X4,tc_bool)),X4,X0) ),
inference(definition_unfolding,[],[f420,f294,f294]) ).
fof(f801,plain,
! [X2,X0,X1] :
( c_HOL_Ominus__class_Ominus(c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X0),X2),X1,tc_fun(X2,tc_bool)),c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X0),X2),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)) = X1
| hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
inference(definition_unfolding,[],[f427,f294,f294]) ).
fof(f817,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = c_Collect(hAPP(c_COMBC(c_COMBB(c_in(X1),c_COMBK(X0,X1,X2),X1,tc_fun(tc_fun(X1,tc_bool),tc_bool),X2),X2,tc_fun(X1,tc_bool),tc_bool),X3),X2)
| hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
inference(definition_unfolding,[],[f537,f334]) ).
fof(f827,plain,
! [X2,X0,X1] :
( c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X0),X2),c_HOL_Ominus__class_Ominus(X1,c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X0),X2),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)) = X1
| ~ hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
inference(definition_unfolding,[],[f565,f294,f294]) ).
fof(f829,plain,
! [X0,X1] : c_Collect(hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1),X0) = c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1),X0),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),tc_fun(X0,tc_bool)),
inference(definition_unfolding,[],[f572,f294]) ).
fof(f835,plain,
! [X0,X1] : c_Collect(hAPP(c_fequal(X0),X1),X0) = c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1),X0),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),tc_fun(X0,tc_bool)),
inference(definition_unfolding,[],[f587,f294]) ).
fof(f847,definition,
sF0 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f848,plain,
tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(reorient_equations,[],[f847]) ).
fof(f849,definition,
sF1 = tc_fun(sF0,tc_bool),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f850,plain,
tc_fun(sF0,tc_bool) = sF1,
inference(reorient_equations,[],[f849]) ).
fof(f851,definition,
sF2 = c_in(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f852,plain,
c_in(sF1) = sF2,
inference(reorient_equations,[],[f851]) ).
fof(f853,plain,
! [X0] : ~ hBOOL(hAPP(hAPP(sF2,X0),c_Arrow__Order__Mirabelle_OLin)),
inference(definition_folding,[],[f698,f852,f850,f848]) ).
fof(f856,plain,
! [X0,X1] : c_Collect(hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1),X0) = c_Collect(hAPP(c_fequal(X0),X1),X0),
inference(forward_demodulation,[],[f829,f835]) ).
fof(f858,plain,
! [X2,X0,X1] :
( c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X0),X2),c_HOL_Ominus__class_Ominus(X1,c_Collect(hAPP(c_fequal(X2),X0),X2),tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)) = X1
| ~ hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
inference(forward_demodulation,[],[f827,f835]) ).
fof(f872,plain,
! [X2,X0,X1] :
( c_HOL_Ominus__class_Ominus(c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X0),X2),X1,tc_fun(X2,tc_bool)),c_Collect(hAPP(c_fequal(X2),X0),X2),tc_fun(X2,tc_bool)) = X1
| hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
inference(forward_demodulation,[],[f801,f835]) ).
fof(f873,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),hAPP(X1,X2)),c_Set_Oimage(X1,c_HOL_Ominus__class_Ominus(X3,c_Collect(hAPP(c_fequal(X4),X2),X4),tc_fun(X4,tc_bool)),X4,X0)))
| ~ c_Fun_Oinj__on(X1,c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X4),X4,X4,tc_bool),X2),X4),X3,tc_fun(X4,tc_bool)),X4,X0) ),
inference(forward_demodulation,[],[f799,f835]) ).
fof(f892,plain,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1) = c_COMBB(c_Not,hAPP(c_COMBC(c_in(X0),X0,tc_fun(X0,tc_bool),tc_bool),X1),tc_bool,tc_bool,X0),
inference(forward_demodulation,[],[f335,f344]) ).
fof(f921,plain,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X0) = c_Collect(c_COMBB(c_Not,X0,tc_bool,tc_bool,X1),X1),
inference(forward_demodulation,[],[f183,f344]) ).
fof(f938,plain,
! [X0,X1] : c_Collect(hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1),X0) = hAPP(c_fequal(X0),X1),
inference(forward_demodulation,[],[f856,f344]) ).
fof(f940,plain,
! [X2,X0,X1] :
( c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X0),X2),c_HOL_Ominus__class_Ominus(X1,hAPP(c_fequal(X2),X0),tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)) = X1
| ~ hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
inference(forward_demodulation,[],[f858,f344]) ).
fof(f952,plain,
! [X2,X0,X1] :
( c_HOL_Ominus__class_Ominus(c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X0),X2),X1,tc_fun(X2,tc_bool)),hAPP(c_fequal(X2),X0),tc_fun(X2,tc_bool)) = X1
| hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
inference(forward_demodulation,[],[f872,f344]) ).
fof(f953,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),hAPP(X1,X2)),c_Set_Oimage(X1,c_HOL_Ominus__class_Ominus(X3,hAPP(c_fequal(X4),X2),tc_fun(X4,tc_bool)),X4,X0)))
| ~ c_Fun_Oinj__on(X1,c_Lattices_Oupper__semilattice__class_Osup(c_Collect(hAPP(c_COMBC(c_fequal(X4),X4,X4,tc_bool),X2),X4),X3,tc_fun(X4,tc_bool)),X4,X0) ),
inference(forward_demodulation,[],[f873,f344]) ).
fof(f990,plain,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X0) = c_COMBB(c_Not,X0,tc_bool,tc_bool,X1),
inference(forward_demodulation,[],[f921,f344]) ).
fof(f993,plain,
! [X0,X1] : hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1) = hAPP(c_fequal(X0),X1),
inference(forward_demodulation,[],[f938,f344]) ).
fof(f994,plain,
! [X2,X0,X1] :
( c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X0),c_HOL_Ominus__class_Ominus(X1,hAPP(c_fequal(X2),X0),tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)) = X1
| ~ hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
inference(forward_demodulation,[],[f940,f344]) ).
fof(f1004,plain,
! [X2,X0,X1] :
( c_HOL_Ominus__class_Ominus(c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_COMBC(c_fequal(X2),X2,X2,tc_bool),X0),X1,tc_fun(X2,tc_bool)),hAPP(c_fequal(X2),X0),tc_fun(X2,tc_bool)) = X1
| hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
inference(forward_demodulation,[],[f952,f344]) ).
fof(f1005,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_Fun_Oinj__on(X1,c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_COMBC(c_fequal(X4),X4,X4,tc_bool),X2),X3,tc_fun(X4,tc_bool)),X4,X0)
| ~ hBOOL(hAPP(hAPP(c_in(X0),hAPP(X1,X2)),c_Set_Oimage(X1,c_HOL_Ominus__class_Ominus(X3,hAPP(c_fequal(X4),X2),tc_fun(X4,tc_bool)),X4,X0))) ),
inference(forward_demodulation,[],[f953,f344]) ).
fof(f1027,plain,
! [X2,X0,X1] :
( c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_fequal(X2),X0),c_HOL_Ominus__class_Ominus(X1,hAPP(c_fequal(X2),X0),tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)) = X1
| ~ hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
inference(forward_demodulation,[],[f994,f993]) ).
fof(f1036,plain,
! [X2,X0,X1] :
( c_HOL_Ominus__class_Ominus(c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_fequal(X2),X0),X1,tc_fun(X2,tc_bool)),hAPP(c_fequal(X2),X0),tc_fun(X2,tc_bool)) = X1
| hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
inference(forward_demodulation,[],[f1004,f993]) ).
fof(f1037,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_Fun_Oinj__on(X1,c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_fequal(X4),X2),X3,tc_fun(X4,tc_bool)),X4,X0)
| ~ hBOOL(hAPP(hAPP(c_in(X0),hAPP(X1,X2)),c_Set_Oimage(X1,c_HOL_Ominus__class_Ominus(X3,hAPP(c_fequal(X4),X2),tc_fun(X4,tc_bool)),X4,X0))) ),
inference(forward_demodulation,[],[f1005,f993]) ).
fof(f1055,plain,
! [X2,X0,X1] :
( c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_fequal(X2),X0),X1,tc_fun(X2,tc_bool)) = X1
| ~ hBOOL(hAPP(hAPP(c_in(X2),X0),X1)) ),
inference(forward_demodulation,[],[f1027,f246]) ).
fof(f1094,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(sF2,X0),X1))
| ~ hBOOL(hAPP(X1,X0)) ),
inference(superposition,[],[f695,f852]) ).
fof(f1095,plain,
! [X0] : ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0)),
inference(unit_resulting_resolution,[],[f1094,f853]) ).
fof(f1108,plain,
! [X0,X1] :
( c_Collect(X0,sF0) != c_Orderings_Obot__class_Obot(sF1)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(superposition,[],[f550,f850]) ).
fof(f1110,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X0,X1))
| c_Orderings_Obot__class_Obot(sF1) != X0 ),
inference(forward_demodulation,[],[f1108,f344]) ).
fof(f1123,plain,
! [X2,X0,X1] : hAPP(c_Not,hAPP(X1,X2)) = hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1),X2),
inference(superposition,[],[f87,f990]) ).
fof(f1124,plain,
! [X0,X1] : hAPP(c_Not,hAPP(X0,X1)) = hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),X1),
inference(superposition,[],[f1123,f850]) ).
fof(f1146,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(sF2,X0),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF1,tc_bool)),X1)))
| ~ hBOOL(hAPP(hAPP(sF2,X0),X1)) ),
inference(superposition,[],[f605,f852]) ).
fof(f1148,plain,
! [X2,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Collect(hAPP(c_COMBC(c_COMBB(sF2,c_COMBK(X1,sF1,X0),sF1,tc_fun(tc_fun(sF1,tc_bool),tc_bool),X0),X0,tc_fun(sF1,tc_bool),tc_bool),X2),X0)
| hBOOL(hAPP(hAPP(sF2,X1),X2)) ),
inference(superposition,[],[f817,f852]) ).
fof(f1159,plain,
! [X2,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = hAPP(c_COMBC(c_COMBB(sF2,c_COMBK(X1,sF1,X0),sF1,tc_fun(tc_fun(sF1,tc_bool),tc_bool),X0),X0,tc_fun(sF1,tc_bool),tc_bool),X2)
| hBOOL(hAPP(hAPP(sF2,X1),X2)) ),
inference(forward_demodulation,[],[f1148,f344]) ).
fof(f1163,plain,
! [X2,X3,X0,X1] :
( hAPP(hAPP(c_COMBB(sF2,c_COMBK(X1,sF1,X0),sF1,tc_fun(tc_fun(sF1,tc_bool),tc_bool),X0),X3),X2) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X3)
| hBOOL(hAPP(hAPP(sF2,X1),X2)) ),
inference(superposition,[],[f378,f1159]) ).
fof(f1165,plain,
! [X2,X3,X0,X1] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X3) = hAPP(hAPP(sF2,hAPP(c_COMBK(X1,sF1,X0),X3)),X2)
| hBOOL(hAPP(hAPP(sF2,X1),X2)) ),
inference(forward_demodulation,[],[f1163,f87]) ).
fof(f1166,plain,
! [X2,X3,X0,X1] :
( hAPP(hAPP(sF2,X1),X2) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X3)
| hBOOL(hAPP(hAPP(sF2,X1),X2)) ),
inference(forward_demodulation,[],[f1165,f379]) ).
fof(f1169,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(sF2,X0),X1))
| hBOOL(hAPP(X1,X0)) ),
inference(superposition,[],[f696,f852]) ).
fof(f1172,plain,
! [X0] : ~ hBOOL(hAPP(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin),hAPP(sF2,X0))),
inference(unit_resulting_resolution,[],[f1169,f853]) ).
fof(f1181,plain,
! [X0] : ~ hBOOL(hAPP(hAPP(sF2,hAPP(sF2,X0)),hAPP(sF2,c_Arrow__Order__Mirabelle_OLin))),
inference(unit_resulting_resolution,[],[f1169,f1172]) ).
fof(f1225,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(sF2,X0),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF1,tc_bool)),X1)))
| hBOOL(hAPP(hAPP(sF2,X0),X1)) ),
inference(superposition,[],[f604,f852]) ).
fof(f1227,plain,
! [X0] : hBOOL(hAPP(hAPP(sF2,X0),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF1,tc_bool)),c_Arrow__Order__Mirabelle_OLin))),
inference(unit_resulting_resolution,[],[f1225,f853]) ).
fof(f1237,plain,
! [X0] : hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF1,tc_bool)),c_Arrow__Order__Mirabelle_OLin),X0)),
inference(unit_resulting_resolution,[],[f1169,f1227]) ).
fof(f1244,plain,
! [X0] : hAPP(sF2,X0) != c_Orderings_Obot__class_Obot(sF1),
inference(unit_resulting_resolution,[],[f1110,f1227]) ).
fof(f1246,plain,
! [X0] : hBOOL(hAPP(hAPP(sF2,hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF1,tc_bool)),c_Arrow__Order__Mirabelle_OLin)),hAPP(sF2,X0))),
inference(unit_resulting_resolution,[],[f1094,f1227]) ).
fof(f1251,plain,
! [X0] : hBOOL(hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X0))),
inference(forward_demodulation,[],[f1237,f1123]) ).
fof(f1260,plain,
! [X0,X1] : hBOOL(hAPP(hAPP(c_in(X0),hAPP(c_Arrow__Order__Mirabelle_OLin,X1)),c_Not)),
inference(unit_resulting_resolution,[],[f695,f1251]) ).
fof(f1335,plain,
! [X0,X1] : hBOOL(hAPP(hAPP(sF2,c_Not),hAPP(c_in(X0),hAPP(c_Arrow__Order__Mirabelle_OLin,X1)))),
inference(unit_resulting_resolution,[],[f1094,f1260]) ).
fof(f1361,plain,
! [X0] : hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0) = c_COMBB(c_Not,hAPP(c_COMBC(c_in(sF0),sF0,sF1,tc_bool),X0),tc_bool,tc_bool,sF0),
inference(superposition,[],[f892,f850]) ).
fof(f1365,plain,
! [X2,X0,X1] : hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1),X2) = hAPP(c_Not,hAPP(hAPP(c_COMBC(c_in(X0),X0,tc_fun(X0,tc_bool),tc_bool),X1),X2)),
inference(superposition,[],[f87,f892]) ).
fof(f1366,plain,
! [X2,X0,X1] : hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1),X2) = hAPP(c_Not,hAPP(hAPP(c_in(X0),X2),X1)),
inference(forward_demodulation,[],[f1365,f378]) ).
fof(f1368,plain,
! [X0] : hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0) = hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF0,tc_bool)),hAPP(c_COMBC(c_in(sF0),sF0,sF1,tc_bool),X0)),
inference(forward_demodulation,[],[f1361,f990]) ).
fof(f1370,plain,
! [X2,X0,X1] : hAPP(c_Not,hAPP(X1,X2)) = hAPP(c_Not,hAPP(hAPP(c_in(X0),X2),X1)),
inference(forward_demodulation,[],[f1366,f1123]) ).
fof(f1372,plain,
! [X0] : hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0) = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),hAPP(c_COMBC(c_in(sF0),sF0,sF1,tc_bool),X0)),
inference(forward_demodulation,[],[f1368,f850]) ).
fof(f1374,plain,
! [X0,X1] : hAPP(c_Not,hAPP(X0,X1)) = hAPP(c_Not,hAPP(hAPP(sF2,X1),X0)),
inference(superposition,[],[f1370,f852]) ).
fof(f1449,plain,
! [X0] : hAPP(c_HOL_Ouminus__class_Ouminus(sF1),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0)) = X0,
inference(superposition,[],[f429,f850]) ).
fof(f1454,plain,
! [X2,X0,X1] : hAPP(X0,X2) = hAPP(c_Not,hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X0),X2)),
inference(superposition,[],[f1123,f429]) ).
fof(f1463,plain,
! [X2,X0] : hAPP(X0,X2) = hAPP(c_Not,hAPP(c_Not,hAPP(X0,X2))),
inference(forward_demodulation,[],[f1454,f1123]) ).
fof(f2106,plain,
! [X0] : hAPP(c_COMBC(c_in(sF0),sF0,sF1,tc_bool),X0) = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0)),
inference(superposition,[],[f1449,f1372]) ).
fof(f2113,plain,
! [X0] : hAPP(c_COMBC(c_in(sF0),sF0,sF1,tc_bool),X0) = X0,
inference(forward_demodulation,[],[f2106,f1449]) ).
fof(f2122,plain,
! [X0,X1] : hAPP(X0,X1) = hAPP(hAPP(c_in(sF0),X1),X0),
inference(superposition,[],[f378,f2113]) ).
fof(f2137,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF0,tc_bool)),X0),X1))
| ~ hBOOL(hAPP(hAPP(c_in(sF0),X1),X0)) ),
inference(superposition,[],[f605,f2122]) ).
fof(f2143,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(c_Not,hAPP(X0,X1)))
| ~ hBOOL(hAPP(hAPP(c_in(sF0),X1),X0)) ),
inference(forward_demodulation,[],[f2137,f1123]) ).
fof(f2148,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(c_Not,hAPP(X0,X1)))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(forward_demodulation,[],[f2143,f2122]) ).
fof(f2174,plain,
! [X0] :
( ~ hBOOL(hAPP(c_Not,X0))
| ~ hBOOL(X0) ),
inference(superposition,[],[f2148,f1449]) ).
fof(f2381,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF0,tc_bool)),X0),X1))
| hBOOL(hAPP(hAPP(c_in(sF0),X1),X0)) ),
inference(superposition,[],[f604,f2122]) ).
fof(f2382,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Not,hAPP(X0,X1)))
| hBOOL(hAPP(hAPP(c_in(sF0),X1),X0)) ),
inference(forward_demodulation,[],[f2381,f1123]) ).
fof(f2383,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Not,hAPP(X0,X1)))
| hBOOL(hAPP(X0,X1)) ),
inference(forward_demodulation,[],[f2382,f2122]) ).
fof(f2413,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Not,hAPP(X0,X1)))
| hBOOL(hAPP(hAPP(sF2,X1),X0)) ),
inference(superposition,[],[f2383,f1374]) ).
fof(f2465,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(c_Not,hAPP(c_Not,hAPP(X0,X1))))
| hBOOL(hAPP(hAPP(sF2,hAPP(hAPP(c_in(X2),X1),X0)),c_Not)) ),
inference(superposition,[],[f2413,f1370]) ).
fof(f2470,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(sF2,hAPP(hAPP(c_in(X2),X1),X0)),c_Not))
| hBOOL(hAPP(X0,X1)) ),
inference(forward_demodulation,[],[f2465,f1463]) ).
fof(f2479,plain,
! [X0,X1] : hBOOL(hAPP(hAPP(sF2,hAPP(hAPP(c_in(X0),c_Arrow__Order__Mirabelle_OLin),hAPP(sF2,X1))),c_Not)),
inference(unit_resulting_resolution,[],[f2470,f853]) ).
fof(f2501,plain,
! [X0] : hBOOL(hAPP(hAPP(sF2,hAPP(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin),hAPP(sF2,X0))),c_Not)),
inference(superposition,[],[f2479,f852]) ).
fof(f2551,plain,
! [X0] : ~ hBOOL(hAPP(hAPP(sF2,hAPP(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin),hAPP(sF2,X0))),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF1,tc_bool)),c_Not))),
inference(unit_resulting_resolution,[],[f1146,f2501]) ).
fof(f2753,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(c_HOL_Ominus__class_Ominus(X0,X1,tc_fun(sF0,tc_bool)),X2))
| ~ hBOOL(hAPP(hAPP(c_in(sF0),X2),X1)) ),
inference(superposition,[],[f596,f2122]) ).
fof(f2754,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(c_HOL_Ominus__class_Ominus(X0,X1,sF1),X2))
| ~ hBOOL(hAPP(hAPP(c_in(sF0),X2),X1)) ),
inference(forward_demodulation,[],[f2753,f850]) ).
fof(f2756,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(c_HOL_Ominus__class_Ominus(X0,X1,sF1),X2))
| ~ hBOOL(hAPP(X1,X2)) ),
inference(forward_demodulation,[],[f2754,f2122]) ).
fof(f2930,plain,
! [X2,X0,X1] : hAPP(hAPP(sF2,X0),c_Arrow__Order__Mirabelle_OLin) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2),
inference(unit_resulting_resolution,[],[f1166,f853]) ).
fof(f2932,plain,
! [X2,X0,X1] :
( hAPP(hAPP(sF2,X0),X1) = hAPP(c_Orderings_Obot__class_Obot(sF1),X2)
| hBOOL(hAPP(hAPP(sF2,X0),X1)) ),
inference(superposition,[],[f1166,f850]) ).
fof(f3941,plain,
! [X0,X1] : hAPP(hAPP(sF2,X0),c_Arrow__Order__Mirabelle_OLin) = hAPP(c_Orderings_Obot__class_Obot(sF1),X1),
inference(superposition,[],[f2930,f850]) ).
fof(f3942,plain,
! [X0,X1] : hAPP(hAPP(sF2,X0),c_Arrow__Order__Mirabelle_OLin) = hAPP(hAPP(sF2,X1),c_Arrow__Order__Mirabelle_OLin),
inference(superposition,[],[f2930,f2930]) ).
fof(f3966,plain,
! [X0,X1] : hAPP(c_Not,hAPP(c_Orderings_Obot__class_Obot(sF1),X0)) = hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X1)),
inference(superposition,[],[f1374,f3941]) ).
fof(f4037,plain,
! [X0,X1] : hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X1)) = hAPP(c_Not,hAPP(hAPP(sF2,X0),c_Arrow__Order__Mirabelle_OLin)),
inference(superposition,[],[f1374,f3942]) ).
fof(f4042,plain,
! [X0,X1] : hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) = hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X1)),
inference(forward_demodulation,[],[f4037,f1374]) ).
fof(f5358,plain,
! [X0,X1] : hAPP(c_Orderings_Obot__class_Obot(sF1),X0) = hAPP(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin),hAPP(sF2,X1)),
inference(unit_resulting_resolution,[],[f2932,f1172]) ).
fof(f5451,plain,
! [X0,X1] : hAPP(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin),hAPP(sF2,X0)) = hAPP(hAPP(sF2,X1),c_Arrow__Order__Mirabelle_OLin),
inference(superposition,[],[f3941,f5358]) ).
fof(f5604,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Not,hAPP(c_Not,hAPP(X0,X1))))
| hBOOL(hAPP(hAPP(sF2,X1),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0))) ),
inference(superposition,[],[f2413,f1124]) ).
fof(f5606,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(sF2,X1),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0)))
| hBOOL(hAPP(X0,X1)) ),
inference(forward_demodulation,[],[f5604,f1463]) ).
fof(f11525,plain,
! [X0] : hBOOL(hAPP(hAPP(sF2,X0),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_Arrow__Order__Mirabelle_OLin))),
inference(unit_resulting_resolution,[],[f5606,f1095]) ).
fof(f11862,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_fequal(sF0),X0),X1,sF1),hAPP(c_fequal(sF0),X0),sF1) = X1
| hBOOL(hAPP(hAPP(c_in(sF0),X0),X1)) ),
inference(superposition,[],[f1036,f850]) ).
fof(f11868,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_fequal(sF0),X0),X1,sF1),hAPP(c_fequal(sF0),X0),sF1) = X1
| hBOOL(hAPP(X1,X0)) ),
inference(forward_demodulation,[],[f11862,f2122]) ).
fof(f11900,plain,
! [X0] : hAPP(sF2,X0) = c_HOL_Ominus__class_Ominus(c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_fequal(sF0),c_Arrow__Order__Mirabelle_OLin),hAPP(sF2,X0),sF1),hAPP(c_fequal(sF0),c_Arrow__Order__Mirabelle_OLin),sF1),
inference(unit_resulting_resolution,[],[f11868,f853]) ).
fof(f11911,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_fequal(sF0),c_Arrow__Order__Mirabelle_OLin),X1))
| ~ hBOOL(hAPP(hAPP(sF2,X0),X1)) ),
inference(superposition,[],[f2756,f11900]) ).
fof(f11915,plain,
~ hBOOL(hAPP(hAPP(c_fequal(sF0),c_Arrow__Order__Mirabelle_OLin),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_Arrow__Order__Mirabelle_OLin))),
inference(unit_resulting_resolution,[],[f11911,f11525]) ).
fof(f13353,plain,
! [X0] : hAPP(c_Not,hAPP(c_Not,X0)) = X0,
inference(superposition,[],[f1463,f1449]) ).
fof(f13369,plain,
! [X2,X0,X1] : hAPP(hAPP(c_in(X2),X1),X0) = hAPP(c_Not,hAPP(c_Not,hAPP(X0,X1))),
inference(superposition,[],[f1463,f1370]) ).
fof(f13370,plain,
! [X0,X1] : hAPP(hAPP(sF2,X1),X0) = hAPP(c_Not,hAPP(c_Not,hAPP(X0,X1))),
inference(superposition,[],[f1463,f1374]) ).
fof(f13371,plain,
! [X0,X1] : hAPP(c_Arrow__Order__Mirabelle_OLin,X1) = hAPP(c_Not,hAPP(c_Not,hAPP(c_Orderings_Obot__class_Obot(sF1),X0))),
inference(superposition,[],[f1463,f3966]) ).
fof(f13382,plain,
! [X0,X1] : hAPP(c_Orderings_Obot__class_Obot(sF1),X0) = hAPP(c_Arrow__Order__Mirabelle_OLin,X1),
inference(forward_demodulation,[],[f13371,f1463]) ).
fof(f13383,plain,
! [X0,X1] : hAPP(X0,X1) = hAPP(hAPP(sF2,X1),X0),
inference(forward_demodulation,[],[f13370,f1463]) ).
fof(f13384,plain,
! [X2,X0,X1] : hAPP(X0,X1) = hAPP(hAPP(c_in(X2),X1),X0),
inference(forward_demodulation,[],[f13369,f1463]) ).
fof(f13453,plain,
! [X2,X0,X1] :
( hAPP(c_Arrow__Order__Mirabelle_OLin,X0) = hAPP(hAPP(sF2,X1),X2)
| hBOOL(hAPP(hAPP(sF2,X1),X2)) ),
inference(superposition,[],[f2932,f13382]) ).
fof(f13504,plain,
! [X2,X0,X1] :
( hAPP(X2,X1) = hAPP(c_Arrow__Order__Mirabelle_OLin,X0)
| hBOOL(hAPP(hAPP(sF2,X1),X2)) ),
inference(forward_demodulation,[],[f13453,f13383]) ).
fof(f13512,plain,
! [X2,X0,X1] :
( hAPP(X2,X1) = hAPP(c_Arrow__Order__Mirabelle_OLin,X0)
| hBOOL(hAPP(X2,X1)) ),
inference(forward_demodulation,[],[f13504,f13383]) ).
fof(f13592,plain,
! [X0,X1] :
( hAPP(c_Arrow__Order__Mirabelle_OLin,X1) = X0
| hBOOL(X0) ),
inference(superposition,[],[f13512,f1449]) ).
fof(f14039,plain,
! [X0,X1] :
( hAPP(c_Arrow__Order__Mirabelle_OLin,X0) != c_Orderings_Obot__class_Obot(sF1)
| hBOOL(hAPP(sF2,X1)) ),
inference(superposition,[],[f1244,f13512]) ).
fof(f14073,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(sF2,hAPP(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin),hAPP(c_Arrow__Order__Mirabelle_OLin,X0))),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF1,tc_bool)),c_Not)))
| hBOOL(hAPP(sF2,X1)) ),
inference(superposition,[],[f2551,f13512]) ).
fof(f14258,definition,
( spl3_15
<=> hBOOL(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin)) ),
introduced(definition,[new_symbols(definition,[spl3_15])],[avatar_definition]) ).
fof(f14259,plain,
( ~ hBOOL(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin))
| spl3_15 ),
inference(avatar_component_clause,[],[f14258]) ).
fof(f14260,plain,
( hBOOL(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin))
| ~ spl3_15 ),
inference(avatar_component_clause,[],[f14258]) ).
fof(f14317,definition,
( spl3_27
<=> hBOOL(hAPP(sF2,c_Not)) ),
introduced(definition,[new_symbols(definition,[spl3_27])],[avatar_definition]) ).
fof(f14318,plain,
( ~ hBOOL(hAPP(sF2,c_Not))
| spl3_27 ),
inference(avatar_component_clause,[],[f14317]) ).
fof(f14319,plain,
( hBOOL(hAPP(sF2,c_Not))
| ~ spl3_27 ),
inference(avatar_component_clause,[],[f14317]) ).
fof(f14490,definition,
( spl3_64
<=> ! [X1] : hBOOL(hAPP(sF2,X1)) ),
introduced(definition,[new_symbols(definition,[spl3_64])],[avatar_definition]) ).
fof(f14491,plain,
( ! [X1] : hBOOL(hAPP(sF2,X1))
| ~ spl3_64 ),
inference(avatar_component_clause,[],[f14490]) ).
fof(f14611,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF1,tc_bool)),c_Not),hAPP(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin),hAPP(c_Arrow__Order__Mirabelle_OLin,X0))))
| hBOOL(hAPP(sF2,X1)) ),
inference(forward_demodulation,[],[f14073,f13383]) ).
fof(f14694,definition,
( spl3_105
<=> ! [X0] : hAPP(c_Arrow__Order__Mirabelle_OLin,X0) != c_Orderings_Obot__class_Obot(sF1) ),
introduced(definition,[new_symbols(definition,[spl3_105])],[avatar_definition]) ).
fof(f14695,plain,
( ! [X0] : hAPP(c_Arrow__Order__Mirabelle_OLin,X0) != c_Orderings_Obot__class_Obot(sF1)
| ~ spl3_105 ),
inference(avatar_component_clause,[],[f14694]) ).
fof(f14696,plain,
( spl3_64
| spl3_105 ),
inference(avatar_split_clause,[],[f14039,f14694,f14490]) ).
fof(f14743,definition,
( spl3_116
<=> ! [X0] : ~ hBOOL(hAPP(hAPP(c_Arrow__Order__Mirabelle_OLin,X0),c_Arrow__Order__Mirabelle_OLin)) ),
introduced(definition,[new_symbols(definition,[spl3_116])],[avatar_definition]) ).
fof(f14744,plain,
( ! [X0] : ~ hBOOL(hAPP(hAPP(c_Arrow__Order__Mirabelle_OLin,X0),c_Arrow__Order__Mirabelle_OLin))
| ~ spl3_116 ),
inference(avatar_component_clause,[],[f14743]) ).
fof(f15121,definition,
( spl3_167
<=> ! [X0,X1] : hAPP(c_Arrow__Order__Mirabelle_OLin,X1) = hAPP(hAPP(c_Arrow__Order__Mirabelle_OLin,X0),c_Arrow__Order__Mirabelle_OLin) ),
introduced(definition,[new_symbols(definition,[spl3_167])],[avatar_definition]) ).
fof(f15122,plain,
( ! [X0,X1] : hAPP(c_Arrow__Order__Mirabelle_OLin,X1) = hAPP(hAPP(c_Arrow__Order__Mirabelle_OLin,X0),c_Arrow__Order__Mirabelle_OLin)
| ~ spl3_167 ),
inference(avatar_component_clause,[],[f15121]) ).
fof(f15125,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(c_Not,hAPP(c_Not,hAPP(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin),hAPP(c_Arrow__Order__Mirabelle_OLin,X0)))))
| hBOOL(hAPP(sF2,X1)) ),
inference(forward_demodulation,[],[f14611,f1123]) ).
fof(f15343,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin),hAPP(c_Arrow__Order__Mirabelle_OLin,X0)))
| hBOOL(hAPP(sF2,X1)) ),
inference(forward_demodulation,[],[f15125,f1463]) ).
fof(f15382,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_Arrow__Order__Mirabelle_OLin,X0),c_Arrow__Order__Mirabelle_OLin))
| hBOOL(hAPP(sF2,X1)) ),
inference(forward_demodulation,[],[f15343,f13383]) ).
fof(f15392,plain,
( spl3_64
| spl3_116 ),
inference(avatar_split_clause,[],[f15382,f14743,f14490]) ).
fof(f15463,plain,
! [X2,X0,X1] :
( hAPP(X1,X2) = X0
| hBOOL(hAPP(X1,X2))
| hBOOL(X0) ),
inference(superposition,[],[f13512,f13592]) ).
fof(f15575,plain,
( ! [X0] : ~ hBOOL(hAPP(c_Not,hAPP(sF2,X0)))
| ~ spl3_64 ),
inference(unit_resulting_resolution,[],[f2174,f14491]) ).
fof(f16033,plain,
( sF2 != c_Orderings_Obot__class_Obot(sF1)
| ~ spl3_15 ),
inference(unit_resulting_resolution,[],[f1110,f14260]) ).
fof(f18182,plain,
! [X2,X0,X1] :
( hAPP(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin),X0) = hAPP(hAPP(sF2,X2),c_Arrow__Order__Mirabelle_OLin)
| hBOOL(hAPP(sF2,X1))
| hBOOL(X0) ),
inference(superposition,[],[f5451,f15463]) ).
fof(f18277,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(X0,hAPP(c_in(X1),hAPP(c_Arrow__Order__Mirabelle_OLin,X2))))
| hBOOL(hAPP(sF2,c_Not))
| hBOOL(X0) ),
inference(superposition,[],[f1335,f15463]) ).
fof(f18282,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X0,hAPP(sF2,X1)))
| hBOOL(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin))
| hBOOL(X0) ),
inference(superposition,[],[f1172,f15463]) ).
fof(f19856,definition,
( spl3_210
<=> ! [X0,X1] :
( ~ hBOOL(hAPP(X0,hAPP(sF2,X1)))
| hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_210])],[avatar_definition]) ).
fof(f19857,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(X0,hAPP(sF2,X1)))
| hBOOL(X0) )
| ~ spl3_210 ),
inference(avatar_component_clause,[],[f19856]) ).
fof(f22740,plain,
( hBOOL(c_Orderings_Obot__class_Obot(sF1))
| ~ spl3_105 ),
inference(unit_resulting_resolution,[],[f15463,f1095,f14695]) ).
fof(f28501,plain,
( ! [X0,X1] : hAPP(c_Arrow__Order__Mirabelle_OLin,X0) = hAPP(hAPP(c_Arrow__Order__Mirabelle_OLin,X1),c_Arrow__Order__Mirabelle_OLin)
| ~ spl3_116 ),
inference(unit_resulting_resolution,[],[f13512,f14744]) ).
fof(f28694,plain,
( spl3_167
| ~ spl3_116 ),
inference(avatar_split_clause,[],[f28501,f14743,f15121]) ).
fof(f29112,plain,
( ! [X0,X1] : hAPP(c_Arrow__Order__Mirabelle_OLin,X0) = hAPP(c_Not,hAPP(sF2,X1))
| ~ spl3_64 ),
inference(unit_resulting_resolution,[],[f13512,f15575]) ).
fof(f29538,plain,
( ! [X0,X1] : hAPP(sF2,X1) = hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ spl3_64 ),
inference(superposition,[],[f1463,f29112]) ).
fof(f29797,plain,
( ! [X0,X1] : hBOOL(hAPP(hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X0)),hAPP(sF2,X1)))
| ~ spl3_64 ),
inference(superposition,[],[f1246,f29538]) ).
fof(f29808,plain,
( ! [X0] : ~ hBOOL(hAPP(hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X0)),hAPP(sF2,c_Arrow__Order__Mirabelle_OLin)))
| ~ spl3_64 ),
inference(superposition,[],[f1181,f29538]) ).
fof(f29851,plain,
( $false
| ~ spl3_64 ),
inference(backward_subsumption_resolution,[],[f29808,f29797]) ).
fof(f29852,plain,
~ spl3_64,
inference(avatar_contradiction_clause,[],[f29851]) ).
fof(f30056,plain,
! [X2,X0,X1] :
( hAPP(hAPP(sF2,c_Arrow__Order__Mirabelle_OLin),X0) = hAPP(c_Arrow__Order__Mirabelle_OLin,X2)
| hBOOL(hAPP(sF2,X1))
| hBOOL(X0) ),
inference(forward_demodulation,[],[f18182,f13383]) ).
fof(f30275,plain,
! [X2,X0,X1] :
( hAPP(c_Arrow__Order__Mirabelle_OLin,X2) = hAPP(X0,c_Arrow__Order__Mirabelle_OLin)
| hBOOL(hAPP(sF2,X1))
| hBOOL(X0) ),
inference(forward_demodulation,[],[f30056,f13383]) ).
fof(f30279,definition,
( spl3_271
<=> ! [X0,X1] :
( hAPP(c_Arrow__Order__Mirabelle_OLin,X1) = hAPP(X0,c_Arrow__Order__Mirabelle_OLin)
| hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_271])],[avatar_definition]) ).
fof(f30280,plain,
( ! [X0,X1] :
( hAPP(c_Arrow__Order__Mirabelle_OLin,X1) = hAPP(X0,c_Arrow__Order__Mirabelle_OLin)
| hBOOL(X0) )
| ~ spl3_271 ),
inference(avatar_component_clause,[],[f30279]) ).
fof(f30335,plain,
( spl3_64
| spl3_271 ),
inference(avatar_split_clause,[],[f30275,f30279,f14490]) ).
fof(f30646,plain,
( ! [X2,X0,X1] :
( hAPP(X1,c_Arrow__Order__Mirabelle_OLin) = hAPP(hAPP(c_Arrow__Order__Mirabelle_OLin,X0),X1)
| hBOOL(c_in(X2)) )
| ~ spl3_271 ),
inference(superposition,[],[f13384,f30280]) ).
fof(f30860,definition,
( spl3_284
<=> ! [X0,X1] : hAPP(X1,c_Arrow__Order__Mirabelle_OLin) = hAPP(hAPP(c_Arrow__Order__Mirabelle_OLin,X0),X1) ),
introduced(definition,[new_symbols(definition,[spl3_284])],[avatar_definition]) ).
fof(f30861,plain,
( ! [X0,X1] : hAPP(X1,c_Arrow__Order__Mirabelle_OLin) = hAPP(hAPP(c_Arrow__Order__Mirabelle_OLin,X0),X1)
| ~ spl3_284 ),
inference(avatar_component_clause,[],[f30860]) ).
fof(f31061,definition,
( spl3_311
<=> ! [X2] : hBOOL(c_in(X2)) ),
introduced(definition,[new_symbols(definition,[spl3_311])],[avatar_definition]) ).
fof(f31062,plain,
( ! [X2] : hBOOL(c_in(X2))
| ~ spl3_311 ),
inference(avatar_component_clause,[],[f31061]) ).
fof(f31063,plain,
( spl3_311
| spl3_284
| ~ spl3_271 ),
inference(avatar_split_clause,[],[f30646,f30279,f30860,f31061]) ).
fof(f35015,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(c_Set_Oimage(X1,c_HOL_Ominus__class_Ominus(X3,hAPP(c_fequal(X4),X2),tc_fun(X4,tc_bool)),X4,X0),hAPP(X1,X2)))
| ~ c_Fun_Oinj__on(X1,c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_fequal(X4),X2),X3,tc_fun(X4,tc_bool)),X4,X0) ),
inference(forward_demodulation,[],[f1037,f13384]) ).
fof(f35223,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(X1,X0))
| c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_fequal(X2),X0),X1,tc_fun(X2,tc_bool)) = X1 ),
inference(forward_demodulation,[],[f1055,f13384]) ).
fof(f41731,plain,
( sF2 != c_Orderings_Obot__class_Obot(sF1)
| ~ spl3_27 ),
inference(unit_resulting_resolution,[],[f1110,f14319]) ).
fof(f41997,plain,
( ~ hBOOL(hAPP(c_Not,c_Orderings_Obot__class_Obot(sF1)))
| ~ spl3_105 ),
inference(unit_resulting_resolution,[],[f2174,f22740]) ).
fof(f42070,plain,
( ! [X0] : ~ hBOOL(hAPP(c_Not,c_in(X0)))
| ~ spl3_311 ),
inference(unit_resulting_resolution,[],[f2174,f31062]) ).
fof(f42231,plain,
( ! [X0,X1] : hAPP(c_Arrow__Order__Mirabelle_OLin,X0) = hAPP(c_Not,c_in(X1))
| ~ spl3_311 ),
inference(unit_resulting_resolution,[],[f13512,f42070]) ).
fof(f42295,plain,
( ! [X0] : hAPP(c_Arrow__Order__Mirabelle_OLin,X0) = hAPP(c_Not,sF2)
| ~ spl3_311 ),
inference(superposition,[],[f42231,f852]) ).
fof(f42409,plain,
( ! [X0] : hAPP(c_Arrow__Order__Mirabelle_OLin,X0) = hAPP(hAPP(c_Not,sF2),c_Arrow__Order__Mirabelle_OLin)
| ~ spl3_167
| ~ spl3_311 ),
inference(superposition,[],[f15122,f42295]) ).
fof(f42602,plain,
( hAPP(c_Not,sF2) = hAPP(hAPP(c_Not,sF2),c_Arrow__Order__Mirabelle_OLin)
| ~ spl3_167
| ~ spl3_311 ),
inference(superposition,[],[f42295,f42409]) ).
fof(f42879,plain,
( ! [X0] : ~ hBOOL(hAPP(c_Not,c_in(X0)))
| ~ spl3_311 ),
inference(unit_resulting_resolution,[],[f2174,f31062]) ).
fof(f42888,plain,
( ! [X0,X1] :
( hAPP(X0,X1) = hAPP(X1,c_Arrow__Order__Mirabelle_OLin)
| hBOOL(X0) )
| ~ spl3_284 ),
inference(superposition,[],[f30861,f13592]) ).
fof(f42960,plain,
( ! [X0] : hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) = hAPP(c_Not,hAPP(hAPP(c_Not,sF2),c_Arrow__Order__Mirabelle_OLin))
| ~ spl3_167
| ~ spl3_311 ),
inference(superposition,[],[f4042,f42409]) ).
fof(f43011,plain,
( ! [X0] : hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) = hAPP(c_Not,hAPP(c_Not,sF2))
| ~ spl3_167
| ~ spl3_311 ),
inference(forward_demodulation,[],[f42960,f42602]) ).
fof(f43035,plain,
( ! [X0] : sF2 = hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ spl3_167
| ~ spl3_311 ),
inference(forward_demodulation,[],[f43011,f13353]) ).
fof(f43165,plain,
( ! [X0,X1] : hAPP(c_Arrow__Order__Mirabelle_OLin,X0) = hAPP(c_Not,c_in(X1))
| ~ spl3_311 ),
inference(unit_resulting_resolution,[],[f13512,f42879]) ).
fof(f43262,plain,
( ! [X0,X1] : hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X1)) = hAPP(c_Not,hAPP(c_Not,c_in(X0)))
| ~ spl3_311 ),
inference(superposition,[],[f4042,f43165]) ).
fof(f43311,plain,
( ! [X0,X1] : c_in(X0) = hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,X1))
| ~ spl3_311 ),
inference(forward_demodulation,[],[f43262,f13353]) ).
fof(f43335,plain,
( ! [X0] : c_in(X0) = sF2
| ~ spl3_167
| ~ spl3_311 ),
inference(forward_demodulation,[],[f43311,f43035]) ).
fof(f43423,plain,
( ! [X0] :
( sF2 = hAPP(c_Not,X0)
| hBOOL(X0) )
| ~ spl3_167
| ~ spl3_311 ),
inference(superposition,[],[f43035,f13592]) ).
fof(f45256,plain,
( ! [X2,X0,X1] :
( hAPP(X1,X0) = hAPP(hAPP(X0,c_Arrow__Order__Mirabelle_OLin),X1)
| hBOOL(c_in(X2)) )
| ~ spl3_284 ),
inference(superposition,[],[f13384,f42888]) ).
fof(f45869,definition,
( spl3_416
<=> ! [X0,X1] : hAPP(X1,X0) = hAPP(hAPP(X0,c_Arrow__Order__Mirabelle_OLin),X1) ),
introduced(definition,[new_symbols(definition,[spl3_416])],[avatar_definition]) ).
fof(f45870,plain,
( ! [X0,X1] : hAPP(X1,X0) = hAPP(hAPP(X0,c_Arrow__Order__Mirabelle_OLin),X1)
| ~ spl3_416 ),
inference(avatar_component_clause,[],[f45869]) ).
fof(f45871,plain,
( spl3_311
| spl3_416
| ~ spl3_284 ),
inference(avatar_split_clause,[],[f45256,f30860,f45869,f31061]) ).
fof(f47529,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(X0,hAPP(sF2,X1)))
| hBOOL(X0) )
| spl3_15 ),
inference(forward_subsumption_resolution,[],[f18282,f14259]) ).
fof(f47641,plain,
( spl3_210
| spl3_15 ),
inference(avatar_split_clause,[],[f47529,f14258,f19856]) ).
fof(f50644,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_Arrow__Order__Mirabelle_OLin),c_fequal(sF0)))
| ~ spl3_416 ),
inference(forward_demodulation,[],[f11915,f45870]) ).
fof(f50774,definition,
( spl3_458
<=> ! [X0] : hBOOL(X0) ),
introduced(definition,[new_symbols(definition,[spl3_458])],[avatar_definition]) ).
fof(f50775,plain,
( ! [X0] : hBOOL(X0)
| ~ spl3_458 ),
inference(avatar_component_clause,[],[f50774]) ).
fof(f50812,plain,
( ~ hBOOL(hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OLin,c_fequal(sF0))))
| ~ spl3_416 ),
inference(forward_demodulation,[],[f50644,f1124]) ).
fof(f50867,plain,
( $false
| ~ spl3_416 ),
inference(forward_subsumption_resolution,[],[f50812,f1251]) ).
fof(f50868,plain,
~ spl3_416,
inference(avatar_contradiction_clause,[],[f50867]) ).
fof(f59027,plain,
( ! [X2,X0,X1] : c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_fequal(X2),X0),X1,tc_fun(X2,tc_bool)) = X1
| ~ spl3_458 ),
inference(backward_subsumption_resolution,[],[f35223,f50775]) ).
fof(f59738,plain,
( ! [X2,X3,X0,X1,X4] : ~ c_Fun_Oinj__on(X1,c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_fequal(X4),X2),X3,tc_fun(X4,tc_bool)),X4,X0)
| ~ spl3_458 ),
inference(backward_subsumption_resolution,[],[f35015,f50775]) ).
fof(f60756,plain,
( ! [X3,X0,X1,X4] : ~ c_Fun_Oinj__on(X1,X3,X4,X0)
| ~ spl3_458 ),
inference(forward_demodulation,[],[f59738,f59027]) ).
fof(f61245,plain,
( $false
| ~ spl3_458 ),
inference(backward_subsumption_resolution,[],[f389,f60756]) ).
fof(f61248,plain,
~ spl3_458,
inference(avatar_contradiction_clause,[],[f61245]) ).
fof(f65505,plain,
( sF2 = hAPP(c_Not,hAPP(c_Not,c_Orderings_Obot__class_Obot(sF1)))
| ~ spl3_105
| ~ spl3_167
| ~ spl3_311 ),
inference(unit_resulting_resolution,[],[f43423,f41997]) ).
fof(f65567,plain,
( sF2 = c_Orderings_Obot__class_Obot(sF1)
| ~ spl3_105
| ~ spl3_167
| ~ spl3_311 ),
inference(forward_demodulation,[],[f65505,f13353]) ).
fof(f65607,plain,
( $false
| ~ spl3_27
| ~ spl3_105
| ~ spl3_167
| ~ spl3_311 ),
inference(forward_subsumption_resolution,[],[f65567,f41731]) ).
fof(f65608,plain,
( ~ spl3_27
| ~ spl3_105
| ~ spl3_167
| ~ spl3_311 ),
inference(avatar_contradiction_clause,[],[f65607]) ).
fof(f65877,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(X0,hAPP(c_in(X1),hAPP(c_Arrow__Order__Mirabelle_OLin,X2))))
| hBOOL(X0) )
| spl3_27 ),
inference(forward_subsumption_resolution,[],[f18277,f14318]) ).
fof(f65983,plain,
( ! [X2,X0] :
( hBOOL(hAPP(X0,hAPP(sF2,hAPP(c_Arrow__Order__Mirabelle_OLin,X2))))
| hBOOL(X0) )
| spl3_27
| ~ spl3_167
| ~ spl3_311 ),
inference(forward_demodulation,[],[f65877,f43335]) ).
fof(f66002,plain,
( ! [X0] : hBOOL(X0)
| spl3_27
| ~ spl3_167
| ~ spl3_210
| ~ spl3_311 ),
inference(forward_subsumption_resolution,[],[f65983,f19857]) ).
fof(f66006,plain,
( spl3_458
| spl3_27
| ~ spl3_167
| ~ spl3_210
| ~ spl3_311 ),
inference(avatar_split_clause,[],[f66002,f31061,f19856,f15121,f14317,f50774]) ).
fof(f66049,plain,
( $false
| ~ spl3_15
| ~ spl3_105
| ~ spl3_167
| ~ spl3_311 ),
inference(forward_subsumption_resolution,[],[f65567,f16033]) ).
fof(f66050,plain,
( ~ spl3_15
| ~ spl3_105
| ~ spl3_167
| ~ spl3_311 ),
inference(avatar_contradiction_clause,[],[f66049]) ).
cnf(s6376,plain,
( spl3_64
| spl3_105 ),
inference(sat_conversion,[],[f14696]) ).
cnf(s6813,plain,
( spl3_64
| spl3_116 ),
inference(sat_conversion,[],[f15392]) ).
cnf(s7237,plain,
( ~ spl3_116
| spl3_167 ),
inference(sat_conversion,[],[f28694]) ).
cnf(s7495,plain,
~ spl3_64,
inference(sat_conversion,[],[f29852]) ).
cnf(s7903,plain,
( spl3_64
| spl3_271 ),
inference(sat_conversion,[],[f30335]) ).
cnf(s8109,plain,
( ~ spl3_271
| spl3_284
| spl3_311 ),
inference(sat_conversion,[],[f31063]) ).
cnf(s16274,plain,
( ~ spl3_284
| spl3_311
| spl3_416 ),
inference(sat_conversion,[],[f45871]) ).
cnf(s16785,plain,
( spl3_15
| spl3_210 ),
inference(sat_conversion,[],[f47641]) ).
cnf(s19420,plain,
~ spl3_416,
inference(sat_conversion,[],[f50868]) ).
cnf(s23089,plain,
~ spl3_458,
inference(sat_conversion,[],[f61248]) ).
cnf(s24611,plain,
( ~ spl3_27
| ~ spl3_105
| ~ spl3_167
| ~ spl3_311 ),
inference(sat_conversion,[],[f65608]) ).
cnf(s24846,plain,
( spl3_27
| ~ spl3_167
| ~ spl3_210
| ~ spl3_311
| spl3_458 ),
inference(sat_conversion,[],[f66006]) ).
cnf(s24872,plain,
( ~ spl3_15
| ~ spl3_105
| ~ spl3_167
| ~ spl3_311 ),
inference(sat_conversion,[],[f66050]) ).
cnf(s24952,plain,
( ~ spl3_284
| spl3_311 ),
inference(rat,[],[s16274,s19420]) ).
cnf(s24979,plain,
spl3_271,
inference(rat,[],[s7903,s7495]) ).
cnf(s25047,plain,
spl3_116,
inference(rat,[],[s6813,s7495]) ).
cnf(s25052,plain,
spl3_167,
inference(rat,[],[s7237,s25047]) ).
cnf(s25096,plain,
spl3_105,
inference(rat,[],[s6376,s7495]) ).
cnf(s25130,plain,
spl3_311,
inference(rat,[],[s8109,s24952,s24979]) ).
cnf(s25169,plain,
~ spl3_15,
inference(rat,[],[s24872,s25096,s25052,s25130]) ).
cnf(s25171,plain,
~ spl3_27,
inference(rat,[],[s24611,s25096,s25052,s25130]) ).
cnf(s25174,plain,
spl3_210,
inference(rat,[],[s16785,s25169]) ).
cnf(s25220,plain,
$false,
inference(rat,[],[s24846,s23089,s25130,s25052,s25174,s25171]) ).
fof(f66103,plain,
$false,
inference(avatar_sat_refutation,[],[s25220]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT006-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.40 % Computer : n011.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Sun Sep 27 23:29:00 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.44 Running first-order theorem proving
% 0.14/0.44 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
% 15.67/3.11 % (2879055)Input is clausal, will run a generic CNF schedule.
% 15.67/3.11 % (2879165)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=780243489:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 15.67/3.11 % (2879161)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=590434827:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 15.67/3.11 % (2879162)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4129856559:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 15.67/3.11 % (2879163)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1924831539:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 15.67/3.11 % (2879164)lrs+10_1_sil=8000:sp=occurrence:random_seed=398110389:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 15.67/3.11 % (2879165)Instruction limit reached!
% 15.67/3.11 % (2879165)------------------------------
% 15.67/3.11 % (2879165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.67/3.11 % (2879165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.67/3.11 % (2879165)CaDiCaL version: 2.1.3
% 15.67/3.11 % (2879165)Termination reason: Instruction limit
% 15.67/3.11 % (2879165)Termination phase: Saturation
% 15.67/3.11 % (2879165)Time elapsed: 0.042 s
% 15.67/3.11 % (2879165)Peak memory usage: 88 MB
% 15.67/3.11 % (2879165)Instructions burned: 116 (million)
% 15.67/3.11 % (2879167)dis-21_1_sil=8000:lcm=predicate:random_seed=456361542: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)
% 15.67/3.11 % (2879166)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3648817014:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 15.67/3.11 % (2879164)Instruction limit reached!
% 15.67/3.11 % (2879164)------------------------------
% 15.67/3.11 % (2879164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.67/3.11 % (2879164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.67/3.12 % (2879164)CaDiCaL version: 2.1.3
% 15.67/3.12 % (2879164)Termination reason: Instruction limit
% 15.67/3.12 % (2879164)Termination phase: Saturation
% 15.67/3.12 % (2879164)Time elapsed: 0.071 s
% 15.67/3.12 % (2879164)Peak memory usage: 89 MB
% 15.67/3.12 % (2879164)Instructions burned: 108 (million)
% 15.67/3.12 % (2879167)Instruction limit reached!
% 15.67/3.12 % (2879167)------------------------------
% 15.67/3.12 % (2879167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.67/3.12 % (2879167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.67/3.12 % (2879167)CaDiCaL version: 2.1.3
% 15.67/3.12 % (2879167)Termination reason: Instruction limit
% 15.67/3.12 % (2879167)Termination phase: Saturation
% 15.67/3.12 % (2879167)Time elapsed: 0.079 s
% 15.67/3.12 % (2879167)Peak memory usage: 89 MB
% 15.67/3.12 % (2879167)Instructions burned: 117 (million)
% 15.67/3.12 % (2879177)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=3794023777:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 15.67/3.12 % (2879177)Refutation not found, incomplete strategy
% 15.67/3.12 % (2879177)------------------------------
% 15.67/3.12 % (2879177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.67/3.12 % (2879177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.67/3.12 % (2879177)CaDiCaL version: 2.1.3
% 15.67/3.12 % (2879177)Termination reason: Refutation not found, incomplete strategy
% 15.67/3.12 % (2879177)Time elapsed: 0.003 s
% 15.67/3.12 % (2879177)Peak memory usage: 88 MB
% 15.67/3.12 % (2879177)Instructions burned: 3 (million)
% 15.67/3.12 % (2879166)Instruction limit reached!
% 15.67/3.12 % (2879166)------------------------------
% 15.67/3.12 % (2879166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.67/3.12 % (2879166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.67/3.12 % (2879166)CaDiCaL version: 2.1.3
% 15.67/3.12 % (2879166)Termination reason: Instruction limit
% 15.67/3.12 % (2879166)Termination phase: Saturation
% 15.67/3.12 % (2879166)Time elapsed: 0.160 s
% 15.67/3.12 % (2879166)Peak memory usage: 89 MB
% 15.67/3.12 % (2879166)Instructions burned: 180 (million)
% 15.67/3.12 % (2879196)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2417902252: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)
% 32.20/5.44 % (2879204)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3603090259:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 32.20/5.44 % (2879177)------------------------------
% 32.20/5.44 % (2879177)------------------------------
% 32.20/5.44 % (2879207)lrs+10_64_to=lpo:sil=8000:random_seed=1987864316:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 32.20/5.44 % (2879196)Instruction limit reached!
% 32.20/5.44 % (2879196)------------------------------
% 32.20/5.44 % (2879196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.20/5.44 % (2879196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.20/5.44 % (2879196)CaDiCaL version: 2.1.3
% 32.20/5.44 % (2879196)Termination reason: Instruction limit
% 32.20/5.44 % (2879196)Termination phase: Saturation
% 32.20/5.44 % (2879196)Time elapsed: 0.126 s
% 32.20/5.44 % (2879196)Peak memory usage: 90 MB
% 32.20/5.44 % (2879196)Instructions burned: 190 (million)
% 32.20/5.44 % (2879204)Instruction limit reached!
% 32.20/5.44 % (2879204)------------------------------
% 32.20/5.44 % (2879204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.20/5.44 % (2879204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.20/5.44 % (2879204)CaDiCaL version: 2.1.3
% 32.20/5.44 % (2879204)Termination reason: Instruction limit
% 32.20/5.44 % (2879204)Termination phase: Saturation
% 32.20/5.44 % (2879204)Time elapsed: 0.215 s
% 32.20/5.44 % (2879204)Peak memory usage: 90 MB
% 32.20/5.44 % (2879204)Instructions burned: 219 (million)
% 32.20/5.44 % (2879207)Instruction limit reached!
% 32.20/5.44 % (2879207)------------------------------
% 32.20/5.44 % (2879207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.20/5.44 % (2879207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.20/5.44 % (2879207)CaDiCaL version: 2.1.3
% 32.20/5.44 % (2879207)Termination reason: Instruction limit
% 32.20/5.44 % (2879207)Termination phase: Saturation
% 32.20/5.44 % (2879207)Time elapsed: 0.136 s
% 32.20/5.44 % (2879207)Peak memory usage: 89 MB
% 32.20/5.44 % (2879207)Instructions burned: 127 (million)
% 32.20/5.44 % (2879219)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2283951185:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 32.20/5.44 % (2879219)Instruction limit reached!
% 32.20/5.44 % (2879219)------------------------------
% 32.20/5.44 % (2879219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.20/5.44 % (2879219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.20/5.44 % (2879219)CaDiCaL version: 2.1.3
% 32.20/5.44 % (2879219)Termination reason: Instruction limit
% 32.20/5.44 % (2879219)Termination phase: Saturation
% 32.20/5.44 % (2879219)Time elapsed: 0.104 s
% 32.20/5.44 % (2879219)Peak memory usage: 90 MB
% 32.20/5.44 % (2879219)Instructions burned: 195 (million)
% 32.20/5.44 % (2879221)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=855446366:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 32.20/5.44 % (2879225)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=2648935327:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 32.20/5.44 % (2879224)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1312451385:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 32.20/5.44 % (2879225)Instruction limit reached!
% 32.20/5.44 % (2879225)------------------------------
% 32.20/5.44 % (2879225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.20/5.44 % (2879225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.20/5.44 % (2879225)CaDiCaL version: 2.1.3
% 32.20/5.44 % (2879225)Termination reason: Instruction limit
% 32.20/5.44 % (2879225)Termination phase: Saturation
% 32.20/5.44 % (2879225)Time elapsed: 0.048 s
% 32.20/5.44 % (2879225)Peak memory usage: 89 MB
% 32.20/5.44 % (2879225)Instructions burned: 108 (million)
% 32.20/5.44 % (2879221)Instruction limit reached!
% 32.20/5.44 % (2879221)------------------------------
% 32.20/5.44 % (2879221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.20/5.44 % (2879221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.36/8.45 % (2879221)CaDiCaL version: 2.1.3
% 53.36/8.45 % (2879221)Termination reason: Instruction limit
% 53.36/8.45 % (2879221)Termination phase: Saturation
% 53.36/8.45 % (2879221)Time elapsed: 0.157 s
% 53.36/8.45 % (2879221)Peak memory usage: 90 MB
% 53.36/8.45 % (2879221)Instructions burned: 157 (million)
% 53.36/8.45 % (2879228)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1745290831:i=107_2990 on theBenchmark for (2990ds/107Mi)
% 53.36/8.45 % (2879237)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1729696909:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2989 on theBenchmark for (2989ds/242Mi)
% 53.36/8.45 % (2879228)Instruction limit reached!
% 53.36/8.45 % (2879228)------------------------------
% 53.36/8.45 % (2879228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.36/8.45 % (2879228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.36/8.45 % (2879228)CaDiCaL version: 2.1.3
% 53.36/8.45 % (2879228)Termination reason: Instruction limit
% 53.36/8.45 % (2879228)Termination phase: Saturation
% 53.36/8.45 % (2879228)Time elapsed: 0.112 s
% 53.36/8.45 % (2879228)Peak memory usage: 90 MB
% 53.36/8.45 % (2879228)Instructions burned: 107 (million)
% 53.36/8.45 % (2879239)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2285629868:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 53.36/8.45 % (2879237)Instruction limit reached!
% 53.36/8.45 % (2879237)------------------------------
% 53.36/8.45 % (2879237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.36/8.45 % (2879237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.36/8.45 % (2879237)CaDiCaL version: 2.1.3
% 53.36/8.45 % (2879237)Termination reason: Instruction limit
% 53.36/8.45 % (2879237)Termination phase: Saturation
% 53.36/8.45 % (2879237)Time elapsed: 0.126 s
% 53.36/8.45 % (2879237)Peak memory usage: 89 MB
% 53.36/8.45 % (2879237)Instructions burned: 244 (million)
% 53.36/8.45 % (2879242)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1874048390:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi)
% 53.36/8.45 % (2879242)Refutation not found, incomplete strategy
% 53.36/8.45 % (2879242)------------------------------
% 53.36/8.45 % (2879242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.36/8.45 % (2879242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.36/8.45 % (2879242)CaDiCaL version: 2.1.3
% 53.36/8.45 % (2879242)Termination reason: Refutation not found, incomplete strategy
% 53.36/8.45 % (2879242)Time elapsed: 0.007 s
% 53.36/8.45 % (2879242)Peak memory usage: 88 MB
% 53.36/8.45 % (2879242)Instructions burned: 4 (million)
% 53.36/8.45 % (2879247)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3806019544:i=499:bd=all_2986 on theBenchmark for (2986ds/499Mi)
% 53.36/8.45 % (2879247)Instruction limit reached!
% 53.36/8.45 % (2879247)------------------------------
% 53.36/8.45 % (2879247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.36/8.45 % (2879247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.36/8.45 % (2879247)CaDiCaL version: 2.1.3
% 53.36/8.45 % (2879247)Termination reason: Instruction limit
% 53.36/8.45 % (2879247)Termination phase: Saturation
% 53.36/8.45 % (2879247)Time elapsed: 0.256 s
% 53.36/8.45 % (2879247)Peak memory usage: 94 MB
% 53.36/8.45 % (2879247)Instructions burned: 501 (million)
% 53.36/8.45 % (2879242)------------------------------
% 53.36/8.45 % (2879242)------------------------------
% 53.36/8.45 % (2879253)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=381181934:i=191:fgj=on:bd=all_2981 on theBenchmark for (2981ds/191Mi)
% 53.36/8.45 % (2879253)Instruction limit reached!
% 53.36/8.45 % (2879253)------------------------------
% 53.36/8.45 % (2879253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.36/8.45 % (2879253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.36/8.45 % (2879253)CaDiCaL version: 2.1.3
% 53.36/8.45 % (2879253)Termination reason: Instruction limit
% 53.36/8.45 % (2879253)Termination phase: Saturation
% 53.36/8.45 % (2879253)Time elapsed: 0.105 s
% 53.36/8.45 % (2879253)Peak memory usage: 91 MB
% 53.36/8.45 % (2879253)Instructions burned: 191 (million)
% 53.36/8.45 % (2879254)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2077054497:i=264:kws=precedence:fsr=off_2979 on theBenchmark for (2979ds/264Mi)
% 59.25/9.28 % (2879259)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3592497703:cond=on:i=156:bs=on:gtg=exists_all:er=known_2977 on theBenchmark for (2977ds/156Mi)
% 59.25/9.28 % (2879259)Instruction limit reached!
% 59.25/9.28 % (2879259)------------------------------
% 59.25/9.28 % (2879259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.25/9.28 % (2879259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.25/9.28 % (2879259)CaDiCaL version: 2.1.3
% 59.25/9.28 % (2879259)Termination reason: Instruction limit
% 59.25/9.28 % (2879259)Termination phase: Saturation
% 59.25/9.28 % (2879259)Time elapsed: 0.088 s
% 59.25/9.28 % (2879259)Peak memory usage: 90 MB
% 59.25/9.28 % (2879259)Instructions burned: 157 (million)
% 59.25/9.28 % (2879254)Instruction limit reached!
% 59.25/9.28 % (2879254)------------------------------
% 59.25/9.28 % (2879254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.25/9.28 % (2879254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.25/9.28 % (2879254)CaDiCaL version: 2.1.3
% 59.25/9.28 % (2879254)Termination reason: Instruction limit
% 59.25/9.28 % (2879254)Termination phase: Saturation
% 59.25/9.28 % (2879254)Time elapsed: 0.269 s
% 59.25/9.28 % (2879254)Peak memory usage: 92 MB
% 59.25/9.28 % (2879254)Instructions burned: 264 (million)
% 59.25/9.28 % (2879265)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1421001532:i=3256:kws=precedence:bd=preordered:av=off_2974 on theBenchmark for (2974ds/3256Mi)
% 59.25/9.28 % (2879266)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3654226270:i=537:av=off:ss=included_2974 on theBenchmark for (2974ds/537Mi)
% 59.25/9.28 % (2879266)Instruction limit reached!
% 59.25/9.28 % (2879266)------------------------------
% 59.25/9.28 % (2879266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.25/9.28 % (2879266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.25/9.28 % (2879266)CaDiCaL version: 2.1.3
% 59.25/9.28 % (2879266)Termination reason: Instruction limit
% 59.25/9.28 % (2879266)Termination phase: Saturation
% 59.25/9.28 % (2879266)Time elapsed: 0.281 s
% 59.25/9.28 % (2879266)Peak memory usage: 93 MB
% 59.25/9.28 % (2879266)Instructions burned: 539 (million)
% 59.25/9.28 % (2879271)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=932225758:i=180:bd=preordered:av=off_2969 on theBenchmark for (2969ds/180Mi)
% 59.25/9.28 % (2879271)Instruction limit reached!
% 59.25/9.28 % (2879271)------------------------------
% 59.25/9.28 % (2879271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.25/9.28 % (2879271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.25/9.28 % (2879271)CaDiCaL version: 2.1.3
% 59.25/9.28 % (2879271)Termination reason: Instruction limit
% 59.25/9.28 % (2879271)Termination phase: Saturation
% 59.25/9.28 % (2879271)Time elapsed: 0.179 s
% 59.25/9.28 % (2879271)Peak memory usage: 89 MB
% 59.25/9.28 % (2879271)Instructions burned: 180 (million)
% 59.25/9.28 % (2879275)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2026815859:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2965 on theBenchmark for (2965ds/10307Mi)
% 59.25/9.28 % (2879224)Instruction limit reached!
% 59.25/9.28 % (2879224)------------------------------
% 59.25/9.28 % (2879224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.25/9.28 % (2879224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.25/9.28 % (2879224)CaDiCaL version: 2.1.3
% 59.25/9.28 % (2879224)Termination reason: Instruction limit
% 59.25/9.28 % (2879224)Termination phase: Saturation
% 59.25/9.28 % (2879224)Time elapsed: 3.376 s
% 59.25/9.28 % (2879224)Peak memory usage: 151 MB
% 59.25/9.28 % (2879224)Instructions burned: 3394 (million)
% 59.25/9.28 % (2879265)Instruction limit reached!
% 59.25/9.28 % (2879265)------------------------------
% 59.25/9.28 % (2879265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.25/9.28 % (2879265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.25/9.28 % (2879265)CaDiCaL version: 2.1.3
% 59.25/9.28 % (2879265)Termination reason: Instruction limit
% 59.25/9.28 % (2879265)Termination phase: Saturation
% 59.25/9.28 % (2879265)Time elapsed: 1.850 s
% 59.25/9.28 % (2879265)Peak memory usage: 144 MB
% 59.25/9.28 % (2879265)Instructions burned: 3258 (million)
% 59.25/9.28 % (2879279)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=4133640969:i=412:gtgl=4:gtg=exists_all_2956 on theBenchmark for (2956ds/412Mi)
% 59.25/9.28 % (2879281)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1350110787:s2pl=no:i=8478:s2at=4:nm=6_2954 on theBenchmark for (2954ds/8478Mi)
% 59.25/9.28 % (2879279)Instruction limit reached!
% 59.25/9.28 % (2879279)------------------------------
% 59.25/9.28 % (2879279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.25/9.28 % (2879279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.25/9.28 % (2879279)CaDiCaL version: 2.1.3
% 59.25/9.28 % (2879279)Termination reason: Instruction limit
% 59.25/9.28 % (2879279)Termination phase: Saturation
% 59.25/9.28 % (2879279)Time elapsed: 0.308 s
% 59.25/9.28 % (2879279)Peak memory usage: 91 MB
% 59.25/9.28 % (2879279)Instructions burned: 412 (million)
% 59.25/9.28 % (2879287)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=300041424:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2949 on theBenchmark for (2949ds/303Mi)
% 59.25/9.28 % (2879287)Instruction limit reached!
% 59.25/9.28 % (2879287)------------------------------
% 59.25/9.28 % (2879287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.25/9.28 % (2879287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.25/9.28 % (2879287)CaDiCaL version: 2.1.3
% 59.25/9.28 % (2879287)Termination reason: Instruction limit
% 59.25/9.28 % (2879287)Termination phase: Saturation
% 59.25/9.28 % (2879287)Time elapsed: 0.278 s
% 59.25/9.28 % (2879287)Peak memory usage: 92 MB
% 59.25/9.28 % (2879287)Instructions burned: 303 (million)
% 59.25/9.28 % (2879289)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=4235321553:st=4:i=720:sd=3:fsr=off:ss=axioms_2944 on theBenchmark for (2944ds/720Mi)
% 59.25/9.28 % (2879289)Instruction limit reached!
% 59.25/9.28 % (2879289)------------------------------
% 59.25/9.28 % (2879289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.25/9.28 % (2879289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.25/9.28 % (2879289)CaDiCaL version: 2.1.3
% 59.25/9.28 % (2879289)Termination reason: Instruction limit
% 59.25/9.28 % (2879289)Termination phase: Saturation
% 59.25/9.28 % (2879289)Time elapsed: 0.646 s
% 59.25/9.28 % (2879289)Peak memory usage: 95 MB
% 59.25/9.28 % (2879289)Instructions burned: 721 (million)
% 59.25/9.28 % (2879239)Instruction limit reached!
% 59.25/9.28 % (2879239)------------------------------
% 59.25/9.28 % (2879239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.25/9.28 % (2879239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.25/9.28 % (2879239)CaDiCaL version: 2.1.3
% 59.25/9.28 % (2879239)Termination reason: Instruction limit
% 59.25/9.28 % (2879239)Termination phase: Saturation
% 59.25/9.28 % (2879239)Time elapsed: 5.065 s
% 59.25/9.28 % (2879239)Peak memory usage: 153 MB
% 59.25/9.28 % (2879239)Instructions burned: 5208 (million)
% 59.25/9.28 % (2879291)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=652568627:i=598:bs=on:bd=preordered:av=off:ss=axioms_2936 on theBenchmark for (2936ds/598Mi)
% 59.25/9.28 % (2879292)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4048005746:i=2989:sd=3:ss=axioms:sgt=60_2935 on theBenchmark for (2935ds/2989Mi)
% 59.25/9.28 % (2879291)Instruction limit reached!
% 59.25/9.28 % (2879291)------------------------------
% 59.25/9.28 % (2879291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.25/9.28 % (2879291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.25/9.28 % (2879291)CaDiCaL version: 2.1.3
% 59.25/9.28 % (2879291)Termination reason: Instruction limit
% 59.25/9.28 % (2879291)Termination phase: Saturation
% 59.25/9.28 % (2879291)Time elapsed: 0.663 s
% 59.25/9.28 % (2879291)Peak memory usage: 95 MB
% 59.25/9.28 % (2879291)Instructions burned: 598 (million)
% 59.25/9.28 % (2879295)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3798513993:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2927 on theBenchmark for (2927ds/1997Mi)
% 59.25/9.28 % (2879281)First to succeed.
% 59.25/9.28 % (2879281)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2879055"
% 59.25/9.28 % (2879281)Refutation found. Thanks to Tanya!
% 59.25/9.28 % SZS status Unsatisfiable for theBenchmark
% 59.25/9.28 % SZS output start Proof for theBenchmark
% See solution above
% 60.08/9.56 % (2879281)------------------------------
% 60.08/9.56 % (2879281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.08/9.56 % (2879281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.08/9.56 % (2879281)CaDiCaL version: 2.1.3
% 60.08/9.56 % (2879281)Termination reason: Refutation
% 60.08/9.56 % (2879281)Time elapsed: 3.287 s
% 60.08/9.56 % (2879281)Peak memory usage: 173 MB
% 60.08/9.56 % (2879281)Instructions burned: 5914 (million)
% 60.08/9.56 % (2879281)------------------------------
% 60.08/9.56 % (2879281)------------------------------
% 60.08/9.56 % (2879055)Success in time 8.409 s
% 60.08/9.56 % Vampire exiting
%------------------------------------------------------------------------------