%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG349-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:19:50 AM UTC 2026
% Result : Unsatisfiable 10.16s 2.10s
% Output : Refutation 10.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 31
% Syntax : Number of formulae : 196 ( 43 unt; 17 def)
% Number of atoms : 504 ( 165 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 495 ( 187 ~; 291 |; 0 &)
% ( 17 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 20 ( 18 usr; 18 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-3 aty)
% Number of variables : 411 ( 0 sgn 411 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f141,axiom,
! [X0,X1] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f145,axiom,
! [X0,X1] : hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Un__empty__left_0) ).
fof(f157,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X3,tc_bool)),X2),X0),X1))
| hBOOL(hAPP(X2,X1))
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup1E_0) ).
fof(f183,axiom,
! [X2,X3,X0,X1] : hAPP(c_COMBK(X0,X1,X2),X3) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_COMBK__def_0) ).
fof(f240,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X2,tc_bool)),X0),X3),X1))
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf1E_0) ).
fof(f346,axiom,
hBOOL(hAPP(v_P,v_sko__local__Xex__1(v_P))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ex_0) ).
fof(f349,axiom,
! [X0,X1] : hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_top1I_0) ).
fof(f354,axiom,
hBOOL(hAPP(v_P,v_x____)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_x_0) ).
fof(f366,axiom,
! [X0,X1] : c_Collect(X0,X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Collect__def_0) ).
fof(f371,axiom,
! [X2,X0,X1] :
( hBOOL(hAPP(X2,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X2,X1)))
| hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X2,X1)))
| c_Collect(X0,X1) = c_Collect(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Collect__cong_0) ).
fof(f372,axiom,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(X2,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X2,X1)))
| c_Collect(X0,X1) = c_Collect(X2,X1)
| ~ hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X2,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Collect__cong_1) ).
fof(f386,axiom,
! [X0,X1] : hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)),c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool))),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Int__UNIV__left_0) ).
fof(f401,axiom,
hBOOL(hAPP(v_P,v_sko__local__Xassms__1__1(v_P))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_assms_I1_J_0) ).
fof(f407,negated_conjecture,
! [X0] : ~ hBOOL(hAPP(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),c_Collect(v_P,tc_RealDef_Oreal),tc_RealDef_Oreal),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f462,plain,
! [X0] : ~ hBOOL(hAPP(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),v_P,tc_RealDef_Oreal),X0)),
inference(superposition,[],[f407,f366]) ).
fof(f478,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(X0)
| c_Collect(X3,X4) = c_Collect(c_COMBK(X0,X1,X2),X4)
| ~ hBOOL(hAPP(X3,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X3,c_COMBK(X0,X1,X2),X4))) ),
inference(superposition,[],[f372,f183]) ).
fof(f483,plain,
! [X2,X3,X0,X1,X4] :
( c_COMBK(X0,X1,X2) = c_Collect(X3,X4)
| ~ hBOOL(X0)
| ~ hBOOL(hAPP(X3,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X3,c_COMBK(X0,X1,X2),X4))) ),
inference(forward_demodulation,[],[f478,f366]) ).
fof(f492,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(X3,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X3,c_COMBK(X0,X1,X2),X4)))
| ~ hBOOL(X0)
| c_COMBK(X0,X1,X2) = X3 ),
inference(forward_demodulation,[],[f483,f366]) ).
fof(f523,plain,
! [X0,X1] :
( hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),v_P,tc_RealDef_Oreal),X0,X1)))
| c_Collect(X0,X1) = c_Collect(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),v_P,tc_RealDef_Oreal),X1) ),
inference(resolution,[],[f371,f462]) ).
fof(f529,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(X0)
| hBOOL(hAPP(X3,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X3,c_COMBK(X0,X1,X2),X4)))
| c_Collect(X3,X4) = c_Collect(c_COMBK(X0,X1,X2),X4) ),
inference(superposition,[],[f371,f183]) ).
fof(f536,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(X0)
| hBOOL(hAPP(X3,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(c_COMBK(X0,X1,X2),X3,X4)))
| c_Collect(X3,X4) = c_Collect(c_COMBK(X0,X1,X2),X4) ),
inference(superposition,[],[f371,f183]) ).
fof(f542,plain,
! [X2,X3,X0,X1,X4] :
( c_COMBK(X0,X1,X2) = c_Collect(X3,X4)
| hBOOL(X0)
| hBOOL(hAPP(X3,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(c_COMBK(X0,X1,X2),X3,X4))) ),
inference(forward_demodulation,[],[f536,f366]) ).
fof(f549,plain,
! [X2,X3,X0,X1,X4] :
( c_COMBK(X0,X1,X2) = c_Collect(X3,X4)
| hBOOL(X0)
| hBOOL(hAPP(X3,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X3,c_COMBK(X0,X1,X2),X4))) ),
inference(forward_demodulation,[],[f529,f366]) ).
fof(f554,plain,
! [X0,X1] :
( c_Collect(X0,X1) = c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),v_P,tc_RealDef_Oreal)
| hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),v_P,tc_RealDef_Oreal),X0,X1))) ),
inference(forward_demodulation,[],[f523,f366]) ).
fof(f568,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(X3,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(c_COMBK(X0,X1,X2),X3,X4)))
| hBOOL(X0)
| c_COMBK(X0,X1,X2) = X3 ),
inference(forward_demodulation,[],[f542,f366]) ).
fof(f575,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(X3,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X3,c_COMBK(X0,X1,X2),X4)))
| hBOOL(X0)
| c_COMBK(X0,X1,X2) = X3 ),
inference(forward_demodulation,[],[f549,f366]) ).
fof(f580,plain,
! [X0,X1] :
( hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),v_P,tc_RealDef_Oreal),X0,X1)))
| c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),v_P,tc_RealDef_Oreal) = X0 ),
inference(forward_demodulation,[],[f554,f366]) ).
fof(f600,plain,
! [X0] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),v_P,tc_RealDef_Oreal),
inference(resolution,[],[f580,f141]) ).
fof(f620,plain,
! [X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
inference(superposition,[],[f600,f600]) ).
fof(f629,plain,
! [X2,X3,X0,X1] :
( hBOOL(X0)
| c_COMBK(X0,X1,X2) = c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)) ),
inference(resolution,[],[f568,f141]) ).
fof(f690,plain,
! [X2,X3,X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)) = c_COMBK(hAPP(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),v_P,tc_RealDef_Oreal),X0),X1,X2),
inference(resolution,[],[f629,f462]) ).
fof(f720,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),X2) = X2,
inference(superposition,[],[f145,f620]) ).
fof(f750,plain,
! [X0,X1,X4] : hAPP(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),v_P,tc_RealDef_Oreal),X1) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X4),
inference(superposition,[],[f183,f690]) ).
fof(f836,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(X0)
| c_COMBK(X0,X1,X2) = c_Orderings_Otop__class_Otop(tc_fun(X3,tc_bool)) ),
inference(resolution,[],[f492,f349]) ).
fof(f851,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(X3)
| ~ hBOOL(X0)
| c_COMBK(X0,X1,X2) = c_COMBK(X3,X4,X5) ),
inference(superposition,[],[f492,f183]) ).
fof(f869,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(X0)
| c_COMBK(X0,X1,X2) = c_COMBK(hAPP(v_P,v_sko__local__Xex__1(v_P)),X3,X4) ),
inference(resolution,[],[f851,f346]) ).
fof(f892,plain,
! [X2,X3,X0,X1] : c_COMBK(hAPP(v_P,v_sko__local__Xassms__1__1(v_P)),X0,X1) = c_COMBK(hAPP(v_P,v_sko__local__Xex__1(v_P)),X2,X3),
inference(resolution,[],[f869,f401]) ).
fof(f894,plain,
! [X2,X3,X0,X1] : c_COMBK(hAPP(v_P,v_sko__local__Xex__1(v_P)),X2,X3) = c_COMBK(hAPP(v_P,v_x____),X0,X1),
inference(resolution,[],[f869,f354]) ).
fof(f946,plain,
! [X2,X0,X1,X5] :
( ~ hBOOL(hAPP(X2,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X2,c_COMBK(hAPP(v_P,v_sko__local__Xex__1(v_P)),X0,X1),X5)))
| ~ hBOOL(hAPP(v_P,v_sko__local__Xassms__1__1(v_P)))
| c_COMBK(hAPP(v_P,v_sko__local__Xex__1(v_P)),X0,X1) = X2 ),
inference(superposition,[],[f492,f892]) ).
fof(f959,plain,
! [X2,X0,X1,X5] :
( ~ hBOOL(hAPP(X2,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X2,c_COMBK(hAPP(v_P,v_sko__local__Xex__1(v_P)),X0,X1),X5)))
| c_COMBK(hAPP(v_P,v_sko__local__Xex__1(v_P)),X0,X1) = X2 ),
inference(forward_subsumption_resolution,[],[f946,f401]) ).
fof(f1059,plain,
! [X2,X0,X1] : c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)) = c_COMBK(hAPP(v_P,v_sko__local__Xex__1(v_P)),X0,X1),
inference(resolution,[],[f959,f349]) ).
fof(f1084,plain,
! [X0,X1] : c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)) = c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),
inference(superposition,[],[f1059,f1059]) ).
fof(f1094,plain,
! [X3,X0] : hAPP(v_P,v_sko__local__Xex__1(v_P)) = hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X3),
inference(superposition,[],[f183,f1059]) ).
fof(f1114,plain,
! [X2,X0,X1] : c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)) = c_COMBK(hAPP(v_P,v_x____),X0,X1),
inference(resolution,[],[f836,f354]) ).
fof(f1138,plain,
! [X3,X0] : hAPP(v_P,v_x____) = hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X3),
inference(superposition,[],[f183,f1114]) ).
fof(f1183,plain,
! [X0,X1,X4] : hAPP(v_P,v_x____) = hAPP(c_COMBK(hAPP(v_P,v_sko__local__Xex__1(v_P)),X0,X1),X4),
inference(superposition,[],[f183,f894]) ).
fof(f1185,plain,
hAPP(v_P,v_sko__local__Xex__1(v_P)) = hAPP(v_P,v_x____),
inference(forward_demodulation,[],[f1183,f183]) ).
fof(f1312,plain,
! [X0,X1] : ~ hBOOL(hAPP(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),v_P,tc_RealDef_Oreal),X1)),
inference(superposition,[],[f462,f1084]) ).
fof(f1321,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X1,tc_bool)),c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool))),X2) = X2,
inference(superposition,[],[f386,f1084]) ).
fof(f1407,plain,
! [X2,X3,X0,X1] :
( hBOOL(X0)
| c_COMBK(X0,X1,X2) = c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(X3,tc_bool)),v_P,tc_RealDef_Oreal) ),
inference(resolution,[],[f1312,f575]) ).
fof(f1438,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( c_COMBK(X0,X1,X2) = c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(X3,tc_bool)),v_P,tc_RealDef_Oreal)
| c_Orderings_Otop__class_Otop(tc_fun(X6,tc_bool)) = c_COMBK(X0,X4,X5) ),
inference(resolution,[],[f1407,f836]) ).
fof(f1581,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( hAPP(v_P,v_x____) = hAPP(c_COMBK(X0,X1,X2),X4)
| c_COMBK(X0,X5,X6) = c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(X7,tc_bool)),v_P,tc_RealDef_Oreal) ),
inference(superposition,[],[f1138,f1438]) ).
fof(f1617,plain,
! [X0,X6,X7,X5] :
( c_COMBK(X0,X5,X6) = c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(X7,tc_bool)),v_P,tc_RealDef_Oreal)
| hAPP(v_P,v_x____) = X0 ),
inference(forward_demodulation,[],[f1581,f183]) ).
fof(f1702,plain,
! [X2,X3,X0,X1,X4,X5] :
( hAPP(c_COMBK(X0,X1,X2),X3) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X4,tc_bool)),X5)
| hAPP(v_P,v_x____) = X0 ),
inference(superposition,[],[f750,f1617]) ).
fof(f1708,plain,
! [X0,X4,X5] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X4,tc_bool)),X5) = X0
| hAPP(v_P,v_x____) = X0 ),
inference(forward_demodulation,[],[f1702,f183]) ).
fof(f1753,plain,
! [X3,X0] :
( X0 = X3
| hAPP(v_P,v_x____) = X3
| hAPP(v_P,v_x____) = X0 ),
inference(superposition,[],[f1708,f1708]) ).
fof(f1841,plain,
! [X2,X3,X0,X1] :
( hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3) = X3
| hAPP(v_P,v_x____) = hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X2,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))) ),
inference(superposition,[],[f145,f1708]) ).
fof(f1861,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3))
| c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____) ),
inference(superposition,[],[f349,f1708]) ).
fof(f1868,plain,
! [X2,X3,X0,X1] :
( hAPP(v_P,v_sko__local__Xex__1(v_P)) = hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3)
| c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____) ),
inference(superposition,[],[f1094,f1708]) ).
fof(f1883,plain,
! [X2,X3,X0,X1,X4] :
( hAPP(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool))),X4) = X4
| c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____) ),
inference(superposition,[],[f720,f1708]) ).
fof(f1912,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3))
| c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____) ),
inference(superposition,[],[f141,f1708]) ).
fof(f1923,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3),X4),X5))
| hBOOL(hAPP(X3,X5))
| c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____) ),
inference(superposition,[],[f240,f1708]) ).
fof(f1957,definition,
( spl0_1
<=> ! [X0] : hAPP(v_P,v_x____) = X0 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f1958,plain,
( ! [X0] : hAPP(v_P,v_x____) = X0
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f1957]) ).
fof(f1975,definition,
( spl0_5
<=> ! [X0,X1,X3] : ~ hBOOL(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f1976,plain,
( ! [X3,X0,X1] : ~ hBOOL(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f1975]) ).
fof(f2019,definition,
( spl0_15
<=> ! [X0,X1,X3] : hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f2020,plain,
( ! [X3,X0,X1] : hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3) = X3
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f2019]) ).
fof(f2026,definition,
( spl0_16
<=> ! [X2] : c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f2027,plain,
( ! [X2] : c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f2026]) ).
fof(f2037,definition,
( spl0_19
<=> ! [X3,X4,X0,X5,X1] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3),X4),X5))
| hBOOL(hAPP(X3,X5)) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f2038,plain,
( ! [X3,X0,X1,X4,X5] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3),X4),X5))
| hBOOL(hAPP(X3,X5)) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f2037]) ).
fof(f2039,plain,
( spl0_16
| spl0_19 ),
inference(avatar_split_clause,[],[f1923,f2037,f2026]) ).
fof(f2049,definition,
( spl0_22
<=> ! [X2] : c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f2050,plain,
( ! [X2] : c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f2049]) ).
fof(f2070,plain,
( spl0_22
| spl0_5 ),
inference(avatar_split_clause,[],[f1912,f1975,f2049]) ).
fof(f2126,definition,
( spl0_36
<=> ! [X2] : c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f2127,plain,
( ! [X2] : c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f2126]) ).
fof(f2129,definition,
( spl0_37
<=> ! [X4,X0,X1,X3] : hAPP(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool))),X4) = X4 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f2130,plain,
( ! [X3,X0,X1,X4] : hAPP(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool))),X4) = X4
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f2129]) ).
fof(f2131,plain,
( spl0_36
| spl0_37 ),
inference(avatar_split_clause,[],[f1883,f2129,f2126]) ).
fof(f2146,definition,
( spl0_41
<=> ! [X5] : hAPP(v_P,v_x____) = c_Orderings_Otop__class_Otop(tc_fun(X5,tc_bool)) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f2147,plain,
( ! [X5] : hAPP(v_P,v_x____) = c_Orderings_Otop__class_Otop(tc_fun(X5,tc_bool))
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f2146]) ).
fof(f2173,definition,
( spl0_48
<=> ! [X0,X1,X3] : hAPP(v_P,v_x____) = hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f2174,plain,
( ! [X3,X0,X1] : hAPP(v_P,v_x____) = hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f2173]) ).
fof(f2177,plain,
! [X2,X3,X0,X1] :
( hAPP(v_P,v_x____) = hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3)
| c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____) ),
inference(forward_demodulation,[],[f1868,f1185]) ).
fof(f2183,definition,
( spl0_49
<=> ! [X0,X1,X3] : hBOOL(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3)) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f2184,plain,
( ! [X3,X0,X1] : hBOOL(hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X3))
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f2183]) ).
fof(f2185,plain,
( spl0_41
| spl0_49 ),
inference(avatar_split_clause,[],[f1861,f2183,f2146]) ).
fof(f2209,definition,
( spl0_55
<=> ! [X2] : hAPP(v_P,v_x____) = hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X2,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f2210,plain,
( ! [X2] : hAPP(v_P,v_x____) = hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X2,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)))
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f2209]) ).
fof(f2211,plain,
( spl0_55
| spl0_15 ),
inference(avatar_split_clause,[],[f1841,f2019,f2209]) ).
fof(f2397,plain,
( spl0_41
| spl0_48 ),
inference(avatar_split_clause,[],[f2177,f2173,f2146]) ).
fof(f2595,plain,
! [X2,X3,X0,X1] :
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X1,tc_bool)),X0),X3) = X3
| hAPP(v_P,v_x____) = X0
| c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)) = hAPP(v_P,v_x____) ),
inference(superposition,[],[f1321,f1753]) ).
fof(f2646,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(hAPP(X0,X2),X3),X4))
| hBOOL(hAPP(X2,X4))
| hAPP(v_P,v_x____) = X0
| c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X1,tc_bool)) = hAPP(v_P,v_x____) ),
inference(superposition,[],[f240,f1753]) ).
fof(f2998,plain,
! [X2,X0,X1] :
( hAPP(hAPP(v_P,v_x____),X1) = X1
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))) = X2
| hAPP(v_P,v_x____) = X2 ),
inference(superposition,[],[f145,f1753]) ).
fof(f3040,plain,
! [X2,X3,X0,X1] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2) = hAPP(c_Lubs_OisUb(hAPP(v_P,v_x____),v_P,tc_RealDef_Oreal),X0)
| c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)) = X3
| hAPP(v_P,v_x____) = X3 ),
inference(superposition,[],[f750,f1753]) ).
fof(f3048,plain,
! [X2,X0,X1] :
( hAPP(v_P,v_sko__local__Xex__1(v_P)) = hAPP(hAPP(v_P,v_x____),X1)
| c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) = X2
| hAPP(v_P,v_x____) = X2 ),
inference(superposition,[],[f1094,f1753]) ).
fof(f3058,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(v_P,v_x____),X1),X2),X3))
| hBOOL(hAPP(X1,X3))
| hBOOL(hAPP(X2,X3))
| c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)) = X4
| hAPP(v_P,v_x____) = X4 ),
inference(superposition,[],[f157,f1753]) ).
fof(f3102,plain,
! [X2,X3,X0,X1] :
( hAPP(hAPP(hAPP(v_P,v_x____),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool))),X2) = X2
| c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)) = X3
| hAPP(v_P,v_x____) = X3 ),
inference(superposition,[],[f1321,f1753]) ).
fof(f4939,definition,
( spl0_150
<=> ! [X2,X3] : hBOOL(hAPP(X2,X3)) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f4940,plain,
( ! [X2,X3] : hBOOL(hAPP(X2,X3))
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f4939]) ).
fof(f4944,definition,
( spl0_151
<=> ! [X2,X1,X3] :
( hBOOL(hAPP(X1,X3))
| hBOOL(hAPP(X2,X3)) ) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f4945,plain,
( ! [X2,X3,X1] :
( hBOOL(hAPP(X1,X3))
| hBOOL(hAPP(X2,X3)) )
| ~ spl0_151 ),
inference(avatar_component_clause,[],[f4944]) ).
fof(f5390,plain,
( ! [X3,X1] : hAPP(v_P,v_x____) = hAPP(hAPP(hAPP(v_P,v_x____),X1),X3)
| ~ spl0_22
| ~ spl0_48 ),
inference(forward_demodulation,[],[f2174,f2050]) ).
fof(f6043,plain,
( ! [X0] : ~ hBOOL(hAPP(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(hAPP(v_P,v_x____)),c_Collect(v_P,tc_RealDef_Oreal),tc_RealDef_Oreal),X0))
| ~ spl0_1 ),
inference(superposition,[],[f407,f1958]) ).
fof(f6383,plain,
( ~ hBOOL(hAPP(v_P,v_x____))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f6043,f1958]) ).
fof(f6411,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f6383,f354]) ).
fof(f6412,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f6411]) ).
fof(f6425,definition,
( spl0_203
<=> ! [X0,X1,X3] :
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X1,tc_bool)),X0),X3) = X3
| hAPP(v_P,v_x____) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl0_203])],[avatar_definition]) ).
fof(f6426,plain,
( ! [X3,X0,X1] :
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X1,tc_bool)),X0),X3) = X3
| hAPP(v_P,v_x____) = X0 )
| ~ spl0_203 ),
inference(avatar_component_clause,[],[f6425]) ).
fof(f6430,plain,
( spl0_41
| spl0_203 ),
inference(avatar_split_clause,[],[f2595,f6425,f2146]) ).
fof(f7097,plain,
( ! [X3,X1,X4,X5] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(hAPP(v_P,v_x____),X1),X3),X4),X5))
| hBOOL(hAPP(X3,X5)) )
| ~ spl0_19
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2038,f2050]) ).
fof(f7317,plain,
( ! [X3,X4,X5] :
( ~ hBOOL(hAPP(hAPP(hAPP(v_P,v_x____),X4),X5))
| hBOOL(hAPP(X3,X5)) )
| ~ spl0_19
| ~ spl0_22
| ~ spl0_48 ),
inference(forward_demodulation,[],[f7097,f5390]) ).
fof(f7484,plain,
( ! [X3,X5] :
( ~ hBOOL(hAPP(v_P,v_x____))
| hBOOL(hAPP(X3,X5)) )
| ~ spl0_19
| ~ spl0_22
| ~ spl0_48 ),
inference(forward_demodulation,[],[f7317,f5390]) ).
fof(f7541,plain,
( ! [X3,X5] : hBOOL(hAPP(X3,X5))
| ~ spl0_19
| ~ spl0_22
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f7484,f354]) ).
fof(f7573,plain,
( spl0_150
| ~ spl0_19
| ~ spl0_22
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f7541,f2173,f2049,f2037,f4939]) ).
fof(f7835,plain,
( ! [X3,X0] :
( hAPP(hAPP(hAPP(v_P,v_x____),X0),X3) = X3
| hAPP(v_P,v_x____) = X0 )
| ~ spl0_16
| ~ spl0_203 ),
inference(forward_demodulation,[],[f6426,f2027]) ).
fof(f7906,plain,
( ! [X3,X0] :
( hAPP(v_P,v_x____) = X3
| hAPP(v_P,v_x____) = X0 )
| ~ spl0_16
| ~ spl0_22
| ~ spl0_48
| ~ spl0_203 ),
inference(forward_demodulation,[],[f7835,f5390]) ).
fof(f7940,plain,
( spl0_1
| spl0_1
| ~ spl0_16
| ~ spl0_22
| ~ spl0_48
| ~ spl0_203 ),
inference(avatar_split_clause,[],[f7906,f6425,f2173,f2049,f2026,f1957,f1957]) ).
fof(f8080,plain,
! [X2,X0,X1] :
( hAPP(v_P,v_x____) = hAPP(hAPP(v_P,v_x____),X1)
| c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) = X2
| hAPP(v_P,v_x____) = X2 ),
inference(forward_demodulation,[],[f3048,f1185]) ).
fof(f8829,plain,
( $false
| ~ spl0_5
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f2184,f1976]) ).
fof(f8830,plain,
( ~ spl0_5
| ~ spl0_49 ),
inference(avatar_contradiction_clause,[],[f8829]) ).
fof(f9075,plain,
( ! [X2,X3,X0] :
( hAPP(hAPP(hAPP(v_P,v_x____),hAPP(v_P,v_x____)),X2) = X2
| c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)) = X3
| hAPP(v_P,v_x____) = X3 )
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3102,f2147]) ).
fof(f9115,plain,
( ! [X2,X1] :
( hAPP(v_P,v_x____) = X2
| hAPP(v_P,v_x____) = hAPP(hAPP(v_P,v_x____),X1)
| hAPP(v_P,v_x____) = X2 )
| ~ spl0_41 ),
inference(forward_demodulation,[],[f8080,f2147]) ).
fof(f9116,plain,
( ! [X2,X1] :
( hAPP(v_P,v_x____) = X2
| hAPP(v_P,v_x____) = hAPP(hAPP(v_P,v_x____),X1) )
| ~ spl0_41 ),
inference(duplicate_literal_removal,[],[f9115]) ).
fof(f9198,definition,
( spl0_278
<=> ! [X1] : hAPP(v_P,v_x____) = hAPP(hAPP(v_P,v_x____),X1) ),
introduced(definition,[new_symbols(definition,[spl0_278])],[avatar_definition]) ).
fof(f9199,plain,
( ! [X1] : hAPP(v_P,v_x____) = hAPP(hAPP(v_P,v_x____),X1)
| ~ spl0_278 ),
inference(avatar_component_clause,[],[f9198]) ).
fof(f9205,plain,
( spl0_278
| spl0_1
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f9116,f2146,f1957,f9198]) ).
fof(f9367,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(hAPP(v_P,v_x____),X2),X3))
| hBOOL(hAPP(X1,X3))
| hBOOL(hAPP(X2,X3))
| c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)) = X4
| hAPP(v_P,v_x____) = X4 )
| ~ spl0_278 ),
inference(forward_demodulation,[],[f3058,f9199]) ).
fof(f9434,plain,
( ! [X2,X0,X1] :
( hAPP(v_P,v_x____) = X1
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))) = X2
| hAPP(v_P,v_x____) = X2 )
| ~ spl0_278 ),
inference(forward_demodulation,[],[f2998,f9199]) ).
fof(f9440,plain,
( ! [X2,X3,X0] :
( hAPP(hAPP(v_P,v_x____),X2) = X2
| c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)) = X3
| hAPP(v_P,v_x____) = X3 )
| ~ spl0_41
| ~ spl0_278 ),
inference(forward_demodulation,[],[f9075,f9199]) ).
fof(f9467,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(v_P,v_x____),X3))
| hBOOL(hAPP(X1,X3))
| hBOOL(hAPP(X2,X3))
| c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)) = X4
| hAPP(v_P,v_x____) = X4 )
| ~ spl0_278 ),
inference(forward_demodulation,[],[f9367,f9199]) ).
fof(f9513,plain,
( ! [X2,X3,X0] :
( hAPP(v_P,v_x____) = X2
| c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)) = X3
| hAPP(v_P,v_x____) = X3 )
| ~ spl0_41
| ~ spl0_278 ),
inference(forward_demodulation,[],[f9440,f9199]) ).
fof(f9534,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(v_P,v_x____))
| hBOOL(hAPP(X1,X3))
| hBOOL(hAPP(X2,X3))
| c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)) = X4
| hAPP(v_P,v_x____) = X4 )
| ~ spl0_278 ),
inference(forward_demodulation,[],[f9467,f9199]) ).
fof(f9551,plain,
( ! [X2,X3] :
( hAPP(v_P,v_x____) = X3
| hAPP(v_P,v_x____) = X2
| hAPP(v_P,v_x____) = X3 )
| ~ spl0_16
| ~ spl0_41
| ~ spl0_278 ),
inference(forward_demodulation,[],[f9513,f2027]) ).
fof(f9552,plain,
( ! [X2,X3] :
( hAPP(v_P,v_x____) = X3
| hAPP(v_P,v_x____) = X2 )
| ~ spl0_16
| ~ spl0_41
| ~ spl0_278 ),
inference(duplicate_literal_removal,[],[f9551]) ).
fof(f9563,plain,
( ! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(X1,X3))
| hBOOL(hAPP(X2,X3))
| c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)) = X4
| hAPP(v_P,v_x____) = X4 )
| ~ spl0_278 ),
inference(forward_subsumption_resolution,[],[f9534,f354]) ).
fof(f9569,plain,
( spl0_1
| spl0_1
| ~ spl0_16
| ~ spl0_41
| ~ spl0_278 ),
inference(avatar_split_clause,[],[f9552,f9198,f2146,f2026,f1957,f1957]) ).
fof(f9574,plain,
( ! [X2,X3,X1,X4] :
( hAPP(v_P,v_x____) = X4
| hBOOL(hAPP(X1,X3))
| hBOOL(hAPP(X2,X3))
| hAPP(v_P,v_x____) = X4 )
| ~ spl0_36
| ~ spl0_278 ),
inference(forward_demodulation,[],[f9563,f2127]) ).
fof(f9575,plain,
( ! [X2,X3,X1,X4] :
( hAPP(v_P,v_x____) = X4
| hBOOL(hAPP(X1,X3))
| hBOOL(hAPP(X2,X3)) )
| ~ spl0_36
| ~ spl0_278 ),
inference(duplicate_literal_removal,[],[f9574]) ).
fof(f9577,plain,
( spl0_151
| spl0_1
| ~ spl0_36
| ~ spl0_278 ),
inference(avatar_split_clause,[],[f9575,f9198,f2126,f1957,f4944]) ).
fof(f9605,plain,
( ! [X2,X0,X1,X4] :
( hBOOL(hAPP(X2,X4))
| hAPP(v_P,v_x____) = X0
| c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X1,tc_bool)) = hAPP(v_P,v_x____) )
| ~ spl0_151 ),
inference(forward_subsumption_resolution,[],[f2646,f4945]) ).
fof(f9639,plain,
( spl0_16
| spl0_1
| spl0_150
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f9605,f4944,f4939,f1957,f2026]) ).
fof(f9664,plain,
( ! [X3,X4] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X4) = X4
| ~ spl0_15
| ~ spl0_37 ),
inference(forward_demodulation,[],[f2130,f2020]) ).
fof(f11743,plain,
( ! [X2,X1] :
( hAPP(v_P,v_x____) = X2
| hAPP(v_P,v_x____) = X1
| hAPP(v_P,v_x____) = X2 )
| ~ spl0_55
| ~ spl0_278 ),
inference(forward_demodulation,[],[f9434,f2210]) ).
fof(f11744,plain,
( ! [X2,X1] :
( hAPP(v_P,v_x____) = X2
| hAPP(v_P,v_x____) = X1 )
| ~ spl0_55
| ~ spl0_278 ),
inference(duplicate_literal_removal,[],[f11743]) ).
fof(f11774,plain,
( spl0_1
| spl0_1
| ~ spl0_55
| ~ spl0_278 ),
inference(avatar_split_clause,[],[f11744,f9198,f2209,f1957,f1957]) ).
fof(f12237,plain,
( ! [X2,X3,X0,X1] :
( hAPP(v_P,v_x____) = X3
| hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2) = hAPP(c_Lubs_OisUb(hAPP(v_P,v_x____),v_P,tc_RealDef_Oreal),X0)
| hAPP(v_P,v_x____) = X3 )
| ~ spl0_41 ),
inference(forward_demodulation,[],[f3040,f2147]) ).
fof(f12238,plain,
( ! [X2,X3,X0,X1] :
( hAPP(v_P,v_x____) = X3
| hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2) = hAPP(c_Lubs_OisUb(hAPP(v_P,v_x____),v_P,tc_RealDef_Oreal),X0) )
| ~ spl0_41 ),
inference(duplicate_literal_removal,[],[f12237]) ).
fof(f12247,plain,
( ! [X2,X3,X0] :
( hAPP(c_Lubs_OisUb(hAPP(v_P,v_x____),v_P,tc_RealDef_Oreal),X0) = X2
| hAPP(v_P,v_x____) = X3 )
| ~ spl0_15
| ~ spl0_37
| ~ spl0_41 ),
inference(forward_demodulation,[],[f12238,f9664]) ).
fof(f12255,definition,
( spl0_426
<=> ! [X2,X0] : hAPP(c_Lubs_OisUb(hAPP(v_P,v_x____),v_P,tc_RealDef_Oreal),X0) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_426])],[avatar_definition]) ).
fof(f12256,plain,
( ! [X2,X0] : hAPP(c_Lubs_OisUb(hAPP(v_P,v_x____),v_P,tc_RealDef_Oreal),X0) = X2
| ~ spl0_426 ),
inference(avatar_component_clause,[],[f12255]) ).
fof(f12258,plain,
( spl0_1
| spl0_426
| ~ spl0_15
| ~ spl0_37
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f12247,f2146,f2129,f2019,f12255,f1957]) ).
fof(f12381,plain,
( ! [X2,X0] : hBOOL(hAPP(hAPP(c_Lubs_OisUb(hAPP(v_P,v_x____),v_P,tc_RealDef_Oreal),X0),X2))
| ~ spl0_426 ),
inference(superposition,[],[f349,f12256]) ).
fof(f12457,plain,
( ! [X2,X0] : ~ hBOOL(hAPP(hAPP(c_Lubs_OisUb(hAPP(v_P,v_x____),v_P,tc_RealDef_Oreal),X0),X2))
| ~ spl0_426 ),
inference(superposition,[],[f1312,f12256]) ).
fof(f12490,plain,
( $false
| ~ spl0_426 ),
inference(forward_subsumption_resolution,[],[f12381,f12457]) ).
fof(f12491,plain,
~ spl0_426,
inference(avatar_contradiction_clause,[],[f12490]) ).
fof(f12853,plain,
( $false
| ~ spl0_150 ),
inference(resolution,[],[f4940,f141]) ).
fof(f12895,plain,
~ spl0_150,
inference(avatar_contradiction_clause,[],[f12853]) ).
cnf(s16,plain,
( spl0_16
| spl0_19 ),
inference(sat_conversion,[],[f2039]) ).
cnf(s25,plain,
( spl0_5
| spl0_22 ),
inference(sat_conversion,[],[f2070]) ).
cnf(s35,plain,
( spl0_36
| spl0_37 ),
inference(sat_conversion,[],[f2131]) ).
cnf(s50,plain,
( spl0_41
| spl0_49 ),
inference(sat_conversion,[],[f2185]) ).
cnf(s55,plain,
( spl0_15
| spl0_55 ),
inference(sat_conversion,[],[f2211]) ).
cnf(s98,plain,
( spl0_41
| spl0_48 ),
inference(sat_conversion,[],[f2397]) ).
cnf(s748,plain,
~ spl0_1,
inference(sat_conversion,[],[f6412]) ).
cnf(s754,plain,
( spl0_41
| spl0_203 ),
inference(sat_conversion,[],[f6430]) ).
cnf(s837,plain,
( ~ spl0_19
| ~ spl0_22
| ~ spl0_48
| spl0_150 ),
inference(sat_conversion,[],[f7573]) ).
cnf(s914,plain,
( spl0_1
| spl0_1
| ~ spl0_16
| ~ spl0_22
| ~ spl0_48
| ~ spl0_203 ),
inference(sat_conversion,[],[f7940]) ).
cnf(s915,plain,
( spl0_1
| ~ spl0_16
| ~ spl0_22
| ~ spl0_48
| ~ spl0_203 ),
inference(rat,[],[s914]) ).
cnf(s1024,plain,
( ~ spl0_5
| ~ spl0_49 ),
inference(sat_conversion,[],[f8830]) ).
cnf(s1090,plain,
( spl0_1
| ~ spl0_41
| spl0_278 ),
inference(sat_conversion,[],[f9205]) ).
cnf(s1152,plain,
( spl0_1
| spl0_1
| ~ spl0_16
| ~ spl0_41
| ~ spl0_278 ),
inference(sat_conversion,[],[f9569]) ).
cnf(s1153,plain,
( spl0_1
| ~ spl0_16
| ~ spl0_41
| ~ spl0_278 ),
inference(rat,[],[s1152]) ).
cnf(s1157,plain,
( spl0_1
| ~ spl0_36
| spl0_151
| ~ spl0_278 ),
inference(sat_conversion,[],[f9577]) ).
cnf(s1169,plain,
( spl0_1
| spl0_16
| spl0_150
| ~ spl0_151 ),
inference(sat_conversion,[],[f9639]) ).
cnf(s1428,plain,
( spl0_1
| spl0_1
| ~ spl0_55
| ~ spl0_278 ),
inference(sat_conversion,[],[f11774]) ).
cnf(s1429,plain,
( spl0_1
| ~ spl0_55
| ~ spl0_278 ),
inference(rat,[],[s1428]) ).
cnf(s1493,plain,
( spl0_1
| ~ spl0_15
| ~ spl0_37
| ~ spl0_41
| spl0_426 ),
inference(sat_conversion,[],[f12258]) ).
cnf(s1497,plain,
~ spl0_426,
inference(sat_conversion,[],[f12491]) ).
cnf(s1528,plain,
~ spl0_150,
inference(sat_conversion,[],[f12895]) ).
cnf(s1539,plain,
( spl0_1
| ~ spl0_15
| ~ spl0_37
| ~ spl0_41 ),
inference(rat,[],[s1493,s1497]) ).
cnf(s1571,plain,
( spl0_1
| spl0_16
| ~ spl0_151 ),
inference(rat,[],[s1169,s1528]) ).
cnf(s1583,plain,
( ~ spl0_19
| ~ spl0_22
| ~ spl0_48 ),
inference(rat,[],[s837,s1528]) ).
cnf(s1843,plain,
( ~ spl0_41
| ~ spl0_278 ),
inference(rat,[],[s35,s1539,s1157,s55,s1571,s1429,s1153,s748]) ).
cnf(s1844,plain,
~ spl0_41,
inference(rat,[],[s1843,s1090,s748]) ).
cnf(s1848,plain,
spl0_203,
inference(rat,[],[s754,s1844]) ).
cnf(s1856,plain,
spl0_48,
inference(rat,[],[s98,s1844]) ).
cnf(s1857,plain,
spl0_49,
inference(rat,[],[s50,s1844]) ).
cnf(s1866,plain,
~ spl0_5,
inference(rat,[],[s1024,s1857]) ).
cnf(s1871,plain,
spl0_22,
inference(rat,[],[s25,s1866]) ).
cnf(s1882,plain,
~ spl0_19,
inference(rat,[],[s1583,s1856,s1871]) ).
cnf(s1884,plain,
~ spl0_16,
inference(rat,[],[s915,s1848,s1856,s748,s1871]) ).
cnf(s1898,plain,
$false,
inference(rat,[],[s16,s1882,s1884]) ).
fof(f12920,plain,
$false,
inference(avatar_sat_refutation,[],[s1898]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG349-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.16 % Computer : n013.cluster.edu
% 0.08/0.16 % Model : x86_64 x86_64
% 0.08/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.16 % Memory : 8046.5625MB
% 0.08/0.16 % OS : Linux 6.8.0-71-generic
% 0.08/0.16 % CPULimit : 300
% 0.08/0.16 % WCLimit : 300
% 0.08/0.16 % DateTime : Mon Sep 28 20:08:21 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 Running first-order theorem proving
% 0.08/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.16/2.10 % (1510335)Input is clausal, will run a generic CNF schedule.
% 10.16/2.10 % (1510344)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=195058466:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.16/2.10 % (1510340)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=2231495943:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.16/2.10 % (1510342)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1603185835:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.16/2.10 % (1510341)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=210519457:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.16/2.10 % (1510344)Instruction limit reached!
% 10.16/2.10 % (1510344)------------------------------
% 10.16/2.10 % (1510344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510344)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510344)Termination reason: Instruction limit
% 10.16/2.10 % (1510344)Termination phase: Saturation
% 10.16/2.10 % (1510344)Time elapsed: 0.041 s
% 10.16/2.10 % (1510344)Peak memory usage: 88 MB
% 10.16/2.10 % (1510344)Instructions burned: 115 (million)
% 10.16/2.10 % (1510345)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=504366653:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.16/2.10 % (1510343)lrs+10_1_sil=8000:sp=occurrence:random_seed=4197816468:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.16/2.10 % (1510346)dis-21_1_sil=8000:lcm=predicate:random_seed=906139097:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.16/2.10 % (1510346)Instruction limit reached!
% 10.16/2.10 % (1510346)------------------------------
% 10.16/2.10 % (1510346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510346)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510346)Termination reason: Instruction limit
% 10.16/2.10 % (1510346)Termination phase: Saturation
% 10.16/2.10 % (1510346)Time elapsed: 0.063 s
% 10.16/2.10 % (1510346)Peak memory usage: 88 MB
% 10.16/2.10 % (1510346)Instructions burned: 120 (million)
% 10.16/2.10 % (1510343)Instruction limit reached!
% 10.16/2.10 % (1510343)------------------------------
% 10.16/2.10 % (1510343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510343)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510343)Termination reason: Instruction limit
% 10.16/2.10 % (1510343)Termination phase: Saturation
% 10.16/2.10 % (1510343)Time elapsed: 0.068 s
% 10.16/2.10 % (1510343)Peak memory usage: 89 MB
% 10.16/2.10 % (1510343)Instructions burned: 108 (million)
% 10.16/2.10 % (1510351)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=3506618441:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.16/2.10 % (1510345)Instruction limit reached!
% 10.16/2.10 % (1510345)------------------------------
% 10.16/2.10 % (1510345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510345)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510345)Termination reason: Instruction limit
% 10.16/2.10 % (1510345)Termination phase: Saturation
% 10.16/2.10 % (1510345)Time elapsed: 0.124 s
% 10.16/2.10 % (1510345)Peak memory usage: 89 MB
% 10.16/2.10 % (1510345)Instructions burned: 180 (million)
% 10.16/2.10 % (1510351)Instruction limit reached!
% 10.16/2.10 % (1510351)------------------------------
% 10.16/2.10 % (1510351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510351)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510351)Termination reason: Instruction limit
% 10.16/2.10 % (1510351)Termination phase: Saturation
% 10.16/2.10 % (1510351)Time elapsed: 0.041 s
% 10.16/2.10 % (1510351)Peak memory usage: 88 MB
% 10.16/2.10 % (1510351)Instructions burned: 145 (million)
% 10.16/2.10 % (1510355)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=593746462:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 10.16/2.10 % (1510356)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1833961135:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.16/2.10 % (1510356)Refutation not found, incomplete strategy
% 10.16/2.10 % (1510356)------------------------------
% 10.16/2.10 % (1510356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510356)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510356)Termination reason: Refutation not found, incomplete strategy
% 10.16/2.10 % (1510356)Time elapsed: 0.012 s
% 10.16/2.10 % (1510356)Peak memory usage: 88 MB
% 10.16/2.10 % (1510356)Instructions burned: 19 (million)
% 10.16/2.10 % (1510359)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2314740985:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 10.16/2.10 % (1510358)lrs+10_64_to=lpo:sil=8000:random_seed=1585343608:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 10.16/2.10 % (1510355)Instruction limit reached!
% 10.16/2.10 % (1510355)------------------------------
% 10.16/2.10 % (1510355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510355)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510355)Termination reason: Instruction limit
% 10.16/2.10 % (1510355)Termination phase: Saturation
% 10.16/2.10 % (1510355)Time elapsed: 0.108 s
% 10.16/2.10 % (1510355)Peak memory usage: 89 MB
% 10.16/2.10 % (1510355)Instructions burned: 190 (million)
% 10.16/2.10 % (1510359)Instruction limit reached!
% 10.16/2.10 % (1510359)------------------------------
% 10.16/2.10 % (1510359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510359)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510359)Termination reason: Instruction limit
% 10.16/2.10 % (1510359)Termination phase: Saturation
% 10.16/2.10 % (1510359)Time elapsed: 0.070 s
% 10.16/2.10 % (1510359)Peak memory usage: 90 MB
% 10.16/2.10 % (1510359)Instructions burned: 195 (million)
% 10.16/2.10 % (1510358)Instruction limit reached!
% 10.16/2.10 % (1510358)------------------------------
% 10.16/2.10 % (1510358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510358)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510358)Termination reason: Instruction limit
% 10.16/2.10 % (1510358)Termination phase: Saturation
% 10.16/2.10 % (1510358)Time elapsed: 0.085 s
% 10.16/2.10 % (1510358)Peak memory usage: 90 MB
% 10.16/2.10 % (1510358)Instructions burned: 126 (million)
% 10.16/2.10 % (1510365)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4294097394:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 10.16/2.10 % (1510356)------------------------------
% 10.16/2.10 % (1510356)------------------------------
% 10.16/2.10 % (1510364)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3712542819:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 10.16/2.10 % (1510366)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=599875651:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 10.16/2.10 % (1510366)Instruction limit reached!
% 10.16/2.10 % (1510366)------------------------------
% 10.16/2.10 % (1510366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510366)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510366)Termination reason: Instruction limit
% 10.16/2.10 % (1510366)Termination phase: Saturation
% 10.16/2.10 % (1510366)Time elapsed: 0.062 s
% 10.16/2.10 % (1510366)Peak memory usage: 89 MB
% 10.16/2.10 % (1510366)Instructions burned: 107 (million)
% 10.16/2.10 % (1510364)Instruction limit reached!
% 10.16/2.10 % (1510364)------------------------------
% 10.16/2.10 % (1510364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510364)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510364)Termination reason: Instruction limit
% 10.16/2.10 % (1510364)Termination phase: Saturation
% 10.16/2.10 % (1510364)Time elapsed: 0.106 s
% 10.16/2.10 % (1510364)Peak memory usage: 90 MB
% 10.16/2.10 % (1510364)Instructions burned: 157 (million)
% 10.16/2.10 % (1510369)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2685541737:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 10.16/2.10 % (1510369)Instruction limit reached!
% 10.16/2.10 % (1510369)------------------------------
% 10.16/2.10 % (1510369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510369)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510369)Termination reason: Instruction limit
% 10.16/2.10 % (1510369)Termination phase: Saturation
% 10.16/2.10 % (1510369)Time elapsed: 0.067 s
% 10.16/2.10 % (1510369)Peak memory usage: 89 MB
% 10.16/2.10 % (1510369)Instructions burned: 108 (million)
% 10.16/2.10 % (1510371)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3677392502:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 10.16/2.10 % (1510372)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1713562992:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 10.16/2.10 % (1510374)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=969190949:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 10.16/2.10 % (1510371)Instruction limit reached!
% 10.16/2.10 % (1510371)------------------------------
% 10.16/2.10 % (1510371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510371)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510371)Termination reason: Instruction limit
% 10.16/2.10 % (1510371)Termination phase: Saturation
% 10.16/2.10 % (1510371)Time elapsed: 0.146 s
% 10.16/2.10 % (1510371)Peak memory usage: 90 MB
% 10.16/2.10 % (1510371)Instructions burned: 243 (million)
% 10.16/2.10 % (1510374)Instruction limit reached!
% 10.16/2.10 % (1510374)------------------------------
% 10.16/2.10 % (1510374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.16/2.10 % (1510374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.16/2.10 % (1510374)CaDiCaL version: 2.1.3
% 10.16/2.10 % (1510374)Termination reason: Instruction limit
% 10.16/2.10 % (1510374)Termination phase: Saturation
% 10.16/2.10 % (1510374)Time elapsed: 0.091 s
% 10.16/2.10 % (1510374)Peak memory usage: 89 MB
% 10.16/2.10 % (1510374)Instructions burned: 135 (million)
% 10.16/2.10 % (1510378)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1826108793:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 10.16/2.10 % (1510365)First to succeed.
% 10.16/2.10 % (1510365)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1510335"
% 10.16/2.10 % (1510379)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2708147733:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 10.16/2.10 % (1510340)Also succeeded, but the first one will report.
% 10.16/2.10 % (1510365)Refutation found. Thanks to Tanya!
% 10.16/2.10 % SZS status Unsatisfiable for theBenchmark
% 10.16/2.10 % SZS output start Proof for theBenchmark
% See solution above
% 10.68/2.19 % (1510365)------------------------------
% 10.68/2.19 % (1510365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.19 % (1510365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.19 % (1510365)CaDiCaL version: 2.1.3
% 10.68/2.19 % (1510365)Termination reason: Refutation
% 10.68/2.19 % (1510365)Time elapsed: 0.660 s
% 10.68/2.19 % (1510365)Peak memory usage: 138 MB
% 10.68/2.19 % (1510365)Instructions burned: 1967 (million)
% 10.68/2.19 % (1510365)------------------------------
% 10.68/2.19 % (1510365)------------------------------
% 10.68/2.19 % (1510335)Success in time 1.454 s
% 10.68/2.19 % Vampire exiting
%------------------------------------------------------------------------------