%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV953-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 : n018.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 01:19:51 PM UTC 2026
% Result : Satisfiable 22.74s 3.91s
% Output : Saturation 24.96s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_ty_Osimps_I9_J_0,axiom,
c_Type_Oty_OClass(X0) != c_Type_Oty_OVoid ).
cnf(cls_is__refT__def_1,axiom,
c_Type_Ois__refT(c_Type_Oty_ONT) ).
cnf(u191,axiom,
( ~ c_TypeRel_Owiden(X1,X2,X0,X3)
| c_Type_Oty_ONT = X2
| c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(v_sko__TypeRel__Xwiden__Xcases__3(X0),X1,X2,X3)) = X2
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u65,axiom,
c_Type_Oty_ONT != c_Type_Oty_OVoid ).
cnf(u379,axiom,
( X0 != X1
| c_Type_Osko__Type__Xty__Xexhaust__1__1(X0) = c_Type_Osko__Type__Xty__Xnchotomy__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u435,axiom,
( X0 != X3
| c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X1,X0,X2) = c_Type_Osko__Type__Xty__Xnchotomy__1__1(X3)
| c_Type_Oty_ONT = X3
| c_Type_Oty_OInteger = X3
| c_Type_Oty_OBoolean = X3
| c_Type_Oty_OVoid = X3
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u434,axiom,
( X0 != X3
| c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X1,X0,X2) = c_Type_Osko__Type__Xty__Xexhaust__1__1(X3)
| c_Type_Oty_ONT = X3
| c_Type_Oty_OInteger = X3
| c_Type_Oty_OBoolean = X3
| c_Type_Oty_OVoid = X3
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u562,axiom,
c_Type_Osko__Type__Xis__refT__def__1__1(c_Type_Oty_OClass(X0)) = X0 ).
cnf(u606,axiom,
( X0 != X3
| c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X3) = c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X1,X0,X2)
| c_Type_Oty_ONT = X3
| c_Type_Oty_OInteger = X3
| c_Type_Oty_OBoolean = X3
| c_Type_Oty_OVoid = X3
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u264,axiom,
( v_sko__TypeRel__Xwiden__Xcases__3(X0) = c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(cls_is__type__simps_5,axiom,
( c_Decl_Ois__type(X0,c_Type_Oty_OClass(X1),X2)
| ~ c_Decl_Ois__class(X0,X1,X2) ) ).
cnf(u71,axiom,
( c_TypeRel_Owiden(X0,X1,c_Type_Oty_OClass(X2),X3)
| ~ c_TypeRel_Owiden(X0,X1,c_Type_Oty_ONT,X3) ) ).
cnf(u112,axiom,
( c_Type_Oty_OClass(X1) != X0
| c_Type_Osko__Type__Xis__refT__def__1__1(X0) = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(cls_is__type__simps_2,axiom,
c_Decl_Ois__type(X0,c_Type_Oty_OInteger,X1) ).
cnf(u73,axiom,
( c_Decl_Ois__class(X1,c_Type_Osko__Type__Xty__Xexhaust__1__1(X0),X2)
| ~ c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(cls_is__type__simps_0,axiom,
c_Decl_Ois__type(X0,c_Type_Oty_OVoid,X1) ).
cnf(u83,axiom,
( c_Decl_Ois__class(X1,c_Type_Osko__Type__XrefTE__1__1(X0),X2)
| ~ c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u12,axiom,
( ~ c_Type_Ois__refT(X0)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OClass(c_Type_Osko__Type__Xis__refT__def__1__1(X0)) = X0 ) ).
cnf(u22,axiom,
( c_Type_Ois__refT(X0)
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u68,negated_conjecture,
c_Type_Oty_OVoid != v_T____ ).
cnf(cls_ty_Osimps_I13_J_0,axiom,
c_Type_Oty_ONT != c_Type_Oty_OBoolean ).
cnf(u343,axiom,
c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(X0,X1,c_Type_Oty_OClass(X0),X2) = X0 ).
cnf(u596,axiom,
( X0 != X1
| v_sko__TypeRel__Xwiden__Xcases__3(X0) = v_sko__TypeRel__Xwiden__Xcases__3(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u31,axiom,
( c_Type_Oty_OClass(c_Type_Osko__Type__Xty__Xnchotomy__1__1(X0)) = X0
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u551,axiom,
( X0 != X1
| v_sko__TypeRel__Xwiden__Xcases__3(X0) = c_Type_Osko__Type__Xis__refT__def__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u605,axiom,
( X0 != X1
| c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u526,axiom,
c_Type_Osko__Type__XrefTE__1__1(c_Type_Oty_OClass(X0)) = X0 ).
cnf(cls_is__refT__def_2,axiom,
c_Type_Ois__refT(c_Type_Oty_OClass(X0)) ).
cnf(u356,axiom,
( c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u384,axiom,
c_Type_Osko__Type__Xty__Xnchotomy__1__1(c_Type_Oty_OClass(X0)) = X0 ).
cnf(cls_ty_Osimps_I17_J_0,axiom,
c_Type_Oty_ONT != c_Type_Oty_OInteger ).
cnf(u147,axiom,
( ~ c_Decl_Ois__class(X1,c_Type_Osko__Type__Xty__Xexhaust__1__1(X0),X2)
| c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u76,axiom,
( c_TypeRel_Owiden(X1,c_Type_Oty_ONT,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u42,axiom,
( c_Type_Oty_OClass(X1) != c_Type_Oty_OClass(X0)
| X0 = X1 ) ).
cnf(u193,axiom,
( c_Decl_Ois__class(X1,v_sko__TypeRel__Xwiden__Xcases__3(X0),X2)
| ~ c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u60,axiom,
c_Type_Oty_OBoolean != c_Type_Oty_OVoid ).
cnf(u88,axiom,
( c_Type_Oty_OClass(X1) != X0
| c_Type_Osko__Type__XrefTE__1__1(X0) = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u397,axiom,
( X0 != X1
| v_sko__TypeRel__Xwiden__Xcases__3(X0) = c_Type_Osko__Type__Xty__Xexhaust__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u177,axiom,
( ~ c_TypeRel_Owiden(X0,X1,c_Type_Oty_ONT,t_a)
| c_Type_Oty_OClass(X2) = X1
| c_Type_Oty_ONT = X1
| c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__1(X0,X1,c_Type_Oty_OClass(X2))) = X1 ) ).
cnf(u407,axiom,
c_Type_Osko__Type__Xty__Xexhaust__1__1(c_Type_Oty_OClass(X0)) = X0 ).
cnf(u265,axiom,
( c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = c_Type_Osko__Type__XrefTE__1__1(X0)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u194,axiom,
( ~ c_Decl_Ois__class(X1,v_sko__TypeRel__Xwiden__Xcases__3(X0),X2)
| c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u374,axiom,
( X0 != X1
| v_sko__TypeRel__Xwiden__Xcases__3(X0) = c_Type_Osko__Type__Xty__Xnchotomy__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u402,axiom,
( X0 != X1
| c_Type_Osko__Type__Xty__Xexhaust__1__1(X0) = c_Type_Osko__Type__Xty__Xexhaust__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u400,axiom,
( X0 != X1
| c_Type_Osko__Type__Xis__refT__def__1__1(X0) = c_Type_Osko__Type__Xty__Xexhaust__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u94,axiom,
( c_Type_Oty_OClass(X1) != X0
| c_Type_Osko__Type__Xty__Xnchotomy__1__1(X0) = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u250,axiom,
c_TypeRel_Osko__TypeRel__XClass__widen__1__1(c_Type_Oty_OClass(X0)) = X0 ).
cnf(cls_widen__Class_2,axiom,
c_TypeRel_Owiden(X0,c_Type_Oty_ONT,c_Type_Oty_OClass(X1),X2) ).
cnf(u229,axiom,
( c_Type_Oty_OClass(X1) != X0
| c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(cls_is__type__simps_1,axiom,
c_Decl_Ois__type(X0,c_Type_Oty_OBoolean,X1) ).
cnf(u124,axiom,
( ~ c_TypeRel_Owiden(X1,X2,X0,X3)
| c_Type_Oty_ONT = X2
| c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_Type_Osko__Type__XrefTE__1__1(X0),X1,X2,X3)) = X2
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u6,axiom,
( ~ c_TypeRel_Owiden(X1,c_Type_Oty_OClass(X2),X0,X3)
| c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0)) = X0 ) ).
cnf(u51,axiom,
( c_Type_Oty_OClass(c_Type_Osko__Type__Xty__Xexhaust__1__1(X0)) = X0
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u8,axiom,
( ~ c_TypeRel_Owiden(X2,X0,c_Type_Oty_OClass(X1),X3)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(X1,X2,X0,X3)) = X0 ) ).
cnf(cls_widen__trans_0,axiom,
( ~ c_TypeRel_Owiden(X0,X4,X2,X3)
| c_TypeRel_Owiden(X0,X1,X2,X3)
| ~ c_TypeRel_Owiden(X0,X1,X4,X3) ) ).
cnf(u580,axiom,
( X0 != X1
| v_sko__TypeRel__Xwiden__Xcases__3(X0) = c_Type_Osko__Type__XrefTE__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u301,axiom,
v_sko__TypeRel__Xwiden__Xcases__3(c_Type_Oty_OClass(X0)) = X0 ).
cnf(u598,axiom,
( X0 != X3
| c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X1,X0,X2) = v_sko__TypeRel__Xwiden__Xcases__3(X3)
| c_Type_Oty_ONT = X3
| c_Type_Oty_OInteger = X3
| c_Type_Oty_OBoolean = X3
| c_Type_Oty_OVoid = X3
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u428,axiom,
( c_Type_Oty_OClass(X1) != X0
| c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X2,X0,X3) = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u707,axiom,
( X0 != X3
| c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X1,X0,X2) = c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X3),X4,X3,X5)
| c_Type_Oty_ONT = X3
| c_Type_Oty_OInteger = X3
| c_Type_Oty_OBoolean = X3
| c_Type_Oty_OVoid = X3
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u266,axiom,
( c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = c_Type_Osko__Type__Xis__refT__def__1__1(X0)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u322,axiom,
( c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X1,X0,X2)) = X0
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u4,axiom,
( ~ c_TypeRel_Owiden(X1,X2,X0,t_a)
| c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__2(X1,X2,X0)) = X0
| X0 = X2
| c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__3(X0)) = X0 ) ).
cnf(cls_ty_Osimps_I20_J_0,axiom,
c_Type_Oty_ONT != c_Type_Oty_OClass(X0) ).
cnf(u14,axiom,
( ~ c_TypeRel_Owiden(X1,X0,X2,t_a)
| c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__1(X1,X0,X2)) = X0
| X0 = X2
| c_Type_Oty_ONT = X0 ) ).
cnf(u103,axiom,
( c_Type_Oty_OClass(c_Type_Osko__Type__Xis__refT__def__1__1(X0)) = X0
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u16,axiom,
( ~ c_TypeRel_Owiden(X2,X0,X1,t_a)
| c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__2(X2,X0,X1)) = X1
| X0 = X1
| c_Type_Oty_ONT = X0 ) ).
cnf(cls_is__type__simps_4,axiom,
( ~ c_Decl_Ois__type(X0,c_Type_Oty_OClass(X1),X2)
| c_Decl_Ois__class(X0,X1,X2) ) ).
cnf(u226,axiom,
( ~ c_Decl_Ois__class(X1,c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X2)
| c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u44,axiom,
c_Type_Oty_OInteger != c_Type_Oty_OBoolean ).
cnf(u72,axiom,
( ~ c_TypeRel_Owiden(X0,X3,X1,X2)
| c_TypeRel_Owiden(X0,X3,c_Type_Oty_OClass(X4),X2)
| ~ c_TypeRel_Owiden(X0,X1,c_Type_Oty_ONT,X2) ) ).
cnf(cls_widen__refl_0,axiom,
c_TypeRel_Owiden(X0,X1,X1,X2) ).
cnf(u375,axiom,
( X0 != X1
| c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = c_Type_Osko__Type__Xty__Xnchotomy__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u553,axiom,
( X0 != X3
| c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X1,X0,X2) = c_Type_Osko__Type__Xis__refT__def__1__1(X3)
| c_Type_Oty_ONT = X3
| c_Type_Oty_OBoolean = X3
| c_Type_Oty_OVoid = X3
| c_Type_Oty_OInteger = X3
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u597,axiom,
( X0 != X1
| c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = v_sko__TypeRel__Xwiden__Xcases__3(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u377,axiom,
( X0 != X1
| c_Type_Osko__Type__Xis__refT__def__1__1(X0) = c_Type_Osko__Type__Xty__Xnchotomy__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u555,axiom,
( X0 != X1
| c_Type_Osko__Type__Xis__refT__def__1__1(X0) = c_Type_Osko__Type__Xis__refT__def__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u78,axiom,
( c_Type_Oty_OClass(X1) != X0
| c_Type_Osko__Type__Xty__Xexhaust__1__1(X0) = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u123,axiom,
( ~ c_TypeRel_Owiden(X2,X0,c_Type_Oty_ONT,X3)
| c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(X1,X2,X0,X3)) = X0
| c_Type_Oty_ONT = X0 ) ).
cnf(u267,axiom,
( c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = c_Type_Osko__Type__Xty__Xnchotomy__1__1(X0)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u74,axiom,
( ~ c_TypeRel_Owiden(X1,X2,c_Type_Oty_ONT,X3)
| c_TypeRel_Owiden(X1,X2,X0,X3)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u399,axiom,
( X0 != X1
| c_Type_Osko__Type__XrefTE__1__1(X0) = c_Type_Osko__Type__Xty__Xexhaust__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u223,axiom,
( ~ c_TypeRel_Owiden(X1,X2,X0,X3)
| c_Type_Oty_ONT = X2
| c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X1,X2,X3)) = X2
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(cls_is__type__simps_3,axiom,
c_Decl_Ois__type(X0,c_Type_Oty_ONT,X1) ).
cnf(u225,axiom,
( c_Decl_Ois__class(X1,c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X2)
| ~ c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u146,axiom,
( ~ c_Decl_Ois__class(X1,c_Type_Osko__Type__Xty__Xnchotomy__1__1(X0),X2)
| c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u79,axiom,
( c_Type_Oty_OClass(c_Type_Osko__Type__XrefTE__1__1(X0)) = X0
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u2,axiom,
( ~ c_TypeRel_Owiden(X2,X1,X0,t_a)
| c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__1(X2,X1,X0)) = X1
| X0 = X1
| c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__3(X0)) = X0 ) ).
cnf(u63,axiom,
c_Type_Oty_OInteger != c_Type_Oty_OVoid ).
cnf(u582,axiom,
( X0 != X3
| c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0),X1,X0,X2) = c_Type_Osko__Type__XrefTE__1__1(X3)
| c_Type_Oty_ONT = X3
| c_Type_Oty_OBoolean = X3
| c_Type_Oty_OVoid = X3
| c_Type_Oty_OInteger = X3
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u554,axiom,
( X0 != X1
| c_Type_Osko__Type__XrefTE__1__1(X0) = c_Type_Osko__Type__Xis__refT__def__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u378,axiom,
( X0 != X1
| c_Type_Osko__Type__Xty__Xnchotomy__1__1(X0) = c_Type_Osko__Type__Xty__Xnchotomy__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u268,axiom,
( c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = c_Type_Osko__Type__Xty__Xexhaust__1__1(X0)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u187,axiom,
( c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__3(X1)) = X1
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1 ) ).
cnf(u144,axiom,
( ~ c_Decl_Ois__class(X1,c_Type_Osko__Type__XrefTE__1__1(X0),X2)
| c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u109,axiom,
( c_Decl_Ois__class(X1,c_Type_Osko__Type__Xis__refT__def__1__1(X0),X2)
| ~ c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u126,axiom,
( ~ c_TypeRel_Owiden(X1,X2,X0,X3)
| c_Type_Oty_ONT = X2
| c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_Type_Osko__Type__Xty__Xnchotomy__1__1(X0),X1,X2,X3)) = X2
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u89,axiom,
( c_Decl_Ois__class(X1,c_Type_Osko__Type__Xty__Xnchotomy__1__1(X0),X2)
| ~ c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u10,axiom,
( ~ c_Type_Ois__refT(X0)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OClass(c_Type_Osko__Type__XrefTE__1__1(X0)) = X0 ) ).
cnf(u99,axiom,
( ~ c_TypeRel_Owiden(X1,X0,X2,X3)
| c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X2)) = X2
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u145,axiom,
( ~ c_Decl_Ois__class(X1,c_Type_Osko__Type__Xis__refT__def__1__1(X0),X2)
| c_Decl_Ois__type(X1,X0,X2)
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u127,axiom,
( ~ c_TypeRel_Owiden(X1,X2,X0,X3)
| c_Type_Oty_ONT = X2
| c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_Type_Osko__Type__Xty__Xexhaust__1__1(X0),X1,X2,X3)) = X2
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u376,axiom,
( X0 != X1
| c_Type_Osko__Type__XrefTE__1__1(X0) = c_Type_Osko__Type__Xty__Xnchotomy__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u581,axiom,
( X0 != X1
| c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = c_Type_Osko__Type__XrefTE__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u583,axiom,
( X0 != X1
| c_Type_Osko__Type__XrefTE__1__1(X0) = c_Type_Osko__Type__XrefTE__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(u208,axiom,
( c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0)) = X0
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u141,axiom,
( ~ c_TypeRel_Owiden(X0,X1,c_Type_Oty_ONT,t_a)
| c_Type_Oty_OClass(X2) = X1
| c_Type_Oty_ONT = X1
| c_Type_Oty_OClass(X2) = c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__2(X0,X1,c_Type_Oty_OClass(X2))) ) ).
cnf(u398,axiom,
( X0 != X1
| c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = c_Type_Osko__Type__Xty__Xexhaust__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u125,axiom,
( ~ c_TypeRel_Owiden(X1,X2,X0,X3)
| c_Type_Oty_ONT = X2
| c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(c_Type_Osko__Type__Xis__refT__def__1__1(X0),X1,X2,X3)) = X2
| c_Type_Oty_ONT = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0
| c_Type_Oty_OInteger = X0 ) ).
cnf(cls_ty_Osimps_I15_J_0,axiom,
c_Type_Oty_OClass(X0) != c_Type_Oty_OBoolean ).
cnf(u197,axiom,
( c_Type_Oty_OClass(X1) != X0
| v_sko__TypeRel__Xwiden__Xcases__3(X0) = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u552,axiom,
( X0 != X1
| c_TypeRel_Osko__TypeRel__XClass__widen__1__1(X0) = c_Type_Osko__Type__Xis__refT__def__1__1(X1)
| c_Type_Oty_ONT = X1
| c_Type_Oty_OBoolean = X1
| c_Type_Oty_OVoid = X1
| c_Type_Oty_OInteger = X1
| c_Type_Oty_ONT = X0
| c_Type_Oty_OInteger = X0
| c_Type_Oty_OBoolean = X0
| c_Type_Oty_OVoid = X0 ) ).
cnf(u48,axiom,
c_Type_Oty_OClass(X0) != c_Type_Oty_OInteger ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV953-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.12/0.17 % Computer : n018.cluster.edu
% 0.12/0.17 % Model : x86_64 x86_64
% 0.12/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.17 % Memory : 8046.5625MB
% 0.12/0.17 % OS : Linux 6.8.0-71-generic
% 0.12/0.17 % CPULimit : 300
% 0.12/0.17 % WCLimit : 300
% 0.12/0.17 % DateTime : Mon Sep 28 13:03:40 UTC 2026
% 0.12/0.18 % CPUTime :
% 0.12/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.21 Running first-order theorem proving
% 0.12/0.21 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
% 13.19/2.32 % (3367348)Input is clausal, will run a generic CNF schedule.
% 13.19/2.32 % (3367359)dis-21_1_sil=8000:lcm=predicate:random_seed=3580316406: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)
% 13.19/2.32 % (3367359)Instruction limit reached!
% 13.19/2.32 % (3367359)------------------------------
% 13.19/2.32 % (3367359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.19/2.32 % (3367359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.19/2.32 % (3367359)CaDiCaL version: 2.1.3
% 13.19/2.32 % (3367359)Termination reason: Instruction limit
% 13.19/2.32 % (3367359)Termination phase: Saturation
% 13.19/2.32 % (3367359)Time elapsed: 0.030 s
% 13.19/2.32 % (3367359)Peak memory usage: 88 MB
% 13.19/2.32 % (3367359)Instructions burned: 122 (million)
% 13.19/2.32 % (3367358)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3678278206:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 13.19/2.32 % (3367353)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=3253308421:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 13.19/2.32 % (3367355)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3791317365:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 13.19/2.32 % (3367357)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1136204221:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 13.19/2.32 % (3367354)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1781281274:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 13.19/2.32 % (3367356)lrs+10_1_sil=8000:sp=occurrence:random_seed=1779954486:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 13.19/2.32 % (3367356)Refutation not found, incomplete strategy
% 13.19/2.32 % (3367356)------------------------------
% 13.19/2.32 % (3367356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.19/2.32 % (3367356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.19/2.32 % (3367356)CaDiCaL version: 2.1.3
% 13.19/2.32 % (3367356)Termination reason: Refutation not found, incomplete strategy
% 13.19/2.32 % (3367356)Time elapsed: 0.001 s
% 13.19/2.32 % (3367356)Peak memory usage: 87 MB
% 13.19/2.32 % (3367357)Refutation not found, incomplete strategy
% 13.19/2.32 % (3367357)------------------------------
% 13.19/2.32 % (3367357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.19/2.32 % (3367357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.19/2.32 % (3367357)CaDiCaL version: 2.1.3
% 13.19/2.32 % (3367357)Termination reason: Refutation not found, incomplete strategy
% 13.19/2.32 % (3367357)Time elapsed: 0.001 s
% 13.19/2.32 % (3367357)Peak memory usage: 87 MB
% 13.19/2.32 % (3367358)Instruction limit reached!
% 13.19/2.32 % (3367358)------------------------------
% 13.19/2.32 % (3367358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.19/2.32 % (3367358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.19/2.32 % (3367358)CaDiCaL version: 2.1.3
% 13.19/2.32 % (3367358)Termination reason: Instruction limit
% 13.19/2.32 % (3367358)Termination phase: Saturation
% 13.19/2.32 % (3367358)Time elapsed: 0.089 s
% 13.19/2.32 % (3367358)Peak memory usage: 88 MB
% 13.19/2.32 % (3367358)Instructions burned: 181 (million)
% 13.19/2.32 % (3367375)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=3014140873:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 13.19/2.32 % (3367375)Refutation not found, incomplete strategy
% 13.19/2.32 % (3367375)------------------------------
% 13.19/2.32 % (3367375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.19/2.32 % (3367375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.19/2.32 % (3367375)CaDiCaL version: 2.1.3
% 13.19/2.32 % (3367375)Termination reason: Refutation not found, incomplete strategy
% 13.19/2.32 % (3367375)Time elapsed: 0.001 s
% 13.19/2.32 % (3367375)Peak memory usage: 88 MB
% 13.19/2.32 % (3367375)Instructions burned: 1 (million)
% 13.19/2.32 % (3367357)------------------------------
% 13.19/2.32 % (3367357)------------------------------
% 13.19/2.32 % (3367356)------------------------------
% 19.75/3.24 % (3367356)------------------------------
% 19.75/3.24 % (3367416)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=855308484: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)
% 19.75/3.24 % (3367375)------------------------------
% 19.75/3.24 % (3367375)------------------------------
% 19.75/3.24 % (3367416)Instruction limit reached!
% 19.75/3.24 % (3367416)------------------------------
% 19.75/3.24 % (3367416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.75/3.24 % (3367416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.75/3.24 % (3367416)CaDiCaL version: 2.1.3
% 19.75/3.24 % (3367416)Termination reason: Instruction limit
% 19.75/3.24 % (3367416)Termination phase: Saturation
% 19.75/3.24 % (3367416)Time elapsed: 0.089 s
% 19.75/3.24 % (3367416)Peak memory usage: 88 MB
% 19.75/3.24 % (3367416)Instructions burned: 190 (million)
% 19.75/3.24 % (3367468)lrs+10_64_to=lpo:sil=8000:random_seed=1448629791:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 19.75/3.24 % (3367467)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4270042179:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 19.75/3.24 % (3367467)Refutation not found, incomplete strategy
% 19.75/3.24 % (3367467)------------------------------
% 19.75/3.24 % (3367467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.75/3.24 % (3367467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.75/3.24 % (3367467)CaDiCaL version: 2.1.3
% 19.75/3.24 % (3367467)Termination reason: Refutation not found, incomplete strategy
% 19.75/3.24 % (3367467)Time elapsed: 0.001 s
% 19.75/3.24 % (3367467)Peak memory usage: 87 MB
% 19.75/3.24 % (3367476)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1579147547:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 19.75/3.24 % (3367468)Instruction limit reached!
% 19.75/3.24 % (3367468)------------------------------
% 19.75/3.24 % (3367468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.75/3.24 % (3367468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.75/3.24 % (3367468)CaDiCaL version: 2.1.3
% 19.75/3.24 % (3367468)Termination reason: Instruction limit
% 19.75/3.24 % (3367468)Termination phase: Saturation
% 19.75/3.24 % (3367468)Time elapsed: 0.062 s
% 19.75/3.24 % (3367468)Peak memory usage: 87 MB
% 19.75/3.24 % (3367468)Instructions burned: 128 (million)
% 19.75/3.24 % (3367476)Instruction limit reached!
% 19.75/3.24 % (3367476)------------------------------
% 19.75/3.24 % (3367476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.75/3.24 % (3367476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.75/3.24 % (3367476)CaDiCaL version: 2.1.3
% 19.75/3.24 % (3367476)Termination reason: Instruction limit
% 19.75/3.24 % (3367476)Termination phase: Saturation
% 19.75/3.24 % (3367476)Time elapsed: 0.053 s
% 19.75/3.24 % (3367476)Peak memory usage: 88 MB
% 19.75/3.24 % (3367476)Instructions burned: 194 (million)
% 19.75/3.24 % (3367486)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1269744617:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 19.75/3.24 % (3367508)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1379394231:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 19.75/3.24 % (3367509)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=3764734423:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 19.75/3.24 % (3367486)Instruction limit reached!
% 19.75/3.24 % (3367486)------------------------------
% 19.75/3.24 % (3367486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.75/3.24 % (3367486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.75/3.24 % (3367486)CaDiCaL version: 2.1.3
% 19.75/3.24 % (3367486)Termination reason: Instruction limit
% 19.75/3.24 % (3367486)Termination phase: Saturation
% 19.75/3.24 % (3367486)Time elapsed: 0.088 s
% 19.75/3.24 % (3367486)Peak memory usage: 89 MB
% 19.75/3.24 % (3367486)Instructions burned: 158 (million)
% 19.75/3.24 % (3367467)------------------------------
% 19.75/3.24 % (3367467)------------------------------
% 19.75/3.24 % (3367509)Instruction limit reached!
% 19.75/3.24 % (3367509)------------------------------
% 19.75/3.24 % (3367509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367509)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367509)Termination reason: Instruction limit
% 22.74/3.91 % (3367509)Termination phase: Saturation
% 22.74/3.91 % (3367509)Time elapsed: 0.053 s
% 22.74/3.91 % (3367509)Peak memory usage: 88 MB
% 22.74/3.91 % (3367509)Instructions burned: 106 (million)
% 22.74/3.91 % (3367513)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1195078967:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 22.74/3.91 % (3367513)Refutation not found, incomplete strategy
% 22.74/3.91 % (3367513)------------------------------
% 22.74/3.91 % (3367513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367513)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367513)Termination reason: Refutation not found, incomplete strategy
% 22.74/3.91 % (3367513)Time elapsed: 0.001 s
% 22.74/3.91 % (3367513)Peak memory usage: 87 MB
% 22.74/3.91 % (3367514)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=634569428:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 22.74/3.91 % (3367515)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4143109327:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 22.74/3.91 % (3367514)Instruction limit reached!
% 22.74/3.91 % (3367514)------------------------------
% 22.74/3.91 % (3367514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367514)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367514)Termination reason: Instruction limit
% 22.74/3.91 % (3367514)Termination phase: Saturation
% 22.74/3.91 % (3367514)Time elapsed: 0.082 s
% 22.74/3.91 % (3367514)Peak memory usage: 87 MB
% 22.74/3.91 % (3367514)Instructions burned: 243 (million)
% 22.74/3.91 % (3367513)------------------------------
% 22.74/3.91 % (3367513)------------------------------
% 22.74/3.91 % (3367519)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3297746208:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 22.74/3.91 % (3367519)Refutation not found, incomplete strategy
% 22.74/3.91 % (3367519)------------------------------
% 22.74/3.91 % (3367519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367519)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367519)Termination reason: Refutation not found, incomplete strategy
% 22.74/3.91 % (3367519)Time elapsed: 0.009 s
% 22.74/3.91 % (3367519)Peak memory usage: 88 MB
% 22.74/3.91 % (3367519)Instructions burned: 16 (million)
% 22.74/3.91 % (3367521)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2628875500:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 22.74/3.91 % (3367519)------------------------------
% 22.74/3.91 % (3367519)------------------------------
% 22.74/3.91 % (3367540)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=773936167:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 22.74/3.91 % (3367521)Instruction limit reached!
% 22.74/3.91 % (3367521)------------------------------
% 22.74/3.91 % (3367521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367521)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367521)Termination reason: Instruction limit
% 22.74/3.91 % (3367521)Termination phase: Saturation
% 22.74/3.91 % (3367521)Time elapsed: 0.362 s
% 22.74/3.91 % (3367521)Peak memory usage: 90 MB
% 22.74/3.91 % (3367521)Instructions burned: 499 (million)
% 22.74/3.91 % (3367508)Instruction limit reached!
% 22.74/3.91 % (3367508)------------------------------
% 22.74/3.91 % (3367508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367508)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367508)Termination reason: Instruction limit
% 22.74/3.91 % (3367508)Termination phase: Saturation
% 22.74/3.91 % (3367508)Time elapsed: 1.146 s
% 22.74/3.91 % (3367508)Peak memory usage: 137 MB
% 22.74/3.91 % (3367508)Instructions burned: 3396 (million)
% 22.74/3.91 % (3367540)Instruction limit reached!
% 22.74/3.91 % (3367540)------------------------------
% 22.74/3.91 % (3367540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367540)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367540)Termination reason: Instruction limit
% 22.74/3.91 % (3367540)Termination phase: Saturation
% 22.74/3.91 % (3367540)Time elapsed: 0.091 s
% 22.74/3.91 % (3367540)Peak memory usage: 89 MB
% 22.74/3.91 % (3367540)Instructions burned: 192 (million)
% 22.74/3.91 % (3367543)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=330133310:i=264:kws=precedence:fsr=off_2981 on theBenchmark for (2981ds/264Mi)
% 22.74/3.91 % (3367544)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1409779834:cond=on:i=156:bs=on:gtg=exists_all:er=known_2980 on theBenchmark for (2980ds/156Mi)
% 22.74/3.91 % (3367545)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=1621728027:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 22.74/3.91 % (3367543)Instruction limit reached!
% 22.74/3.91 % (3367543)------------------------------
% 22.74/3.91 % (3367543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367543)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367543)Termination reason: Instruction limit
% 22.74/3.91 % (3367543)Termination phase: Saturation
% 22.74/3.91 % (3367543)Time elapsed: 0.129 s
% 22.74/3.91 % (3367543)Peak memory usage: 90 MB
% 22.74/3.91 % (3367543)Instructions burned: 265 (million)
% 22.74/3.91 % (3367544)Instruction limit reached!
% 22.74/3.91 % (3367544)------------------------------
% 22.74/3.91 % (3367544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367544)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367544)Termination reason: Instruction limit
% 22.74/3.91 % (3367544)Termination phase: Saturation
% 22.74/3.91 % (3367544)Time elapsed: 0.078 s
% 22.74/3.91 % (3367544)Peak memory usage: 88 MB
% 22.74/3.91 % (3367544)Instructions burned: 156 (million)
% 22.74/3.91 % (3367550)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3569123137:i=537:av=off:ss=included_2978 on theBenchmark for (2978ds/537Mi)
% 22.74/3.91 % (3367551)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3778440286:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi)
% 22.74/3.91 % (3367551)Instruction limit reached!
% 22.74/3.91 % (3367551)------------------------------
% 22.74/3.91 % (3367551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367551)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367551)Termination reason: Instruction limit
% 22.74/3.91 % (3367551)Termination phase: Saturation
% 22.74/3.91 % (3367551)Time elapsed: 0.097 s
% 22.74/3.91 % (3367551)Peak memory usage: 88 MB
% 22.74/3.91 % (3367551)Instructions burned: 181 (million)
% 22.74/3.91 % (3367627)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=1219541597:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2976 on theBenchmark for (2976ds/10307Mi)
% 22.74/3.91 % (3367550)Instruction limit reached!
% 22.74/3.91 % (3367550)------------------------------
% 22.74/3.91 % (3367550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367550)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367550)Termination reason: Instruction limit
% 22.74/3.91 % (3367550)Termination phase: Saturation
% 22.74/3.91 % (3367550)Time elapsed: 0.272 s
% 22.74/3.91 % (3367550)Peak memory usage: 89 MB
% 22.74/3.91 % (3367550)Instructions burned: 538 (million)
% 22.74/3.91 % (3367661)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=1077135721:i=412:gtgl=4:gtg=exists_all_2974 on theBenchmark for (2974ds/412Mi)
% 22.74/3.91 % (3367661)Instruction limit reached!
% 22.74/3.91 % (3367661)------------------------------
% 22.74/3.91 % (3367661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367661)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367661)Termination reason: Instruction limit
% 22.74/3.91 % (3367661)Termination phase: Saturation
% 22.74/3.91 % (3367661)Time elapsed: 0.142 s
% 22.74/3.91 % (3367661)Peak memory usage: 88 MB
% 22.74/3.91 % (3367661)Instructions burned: 414 (million)
% 22.74/3.91 % (3367710)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=3396961510:s2pl=no:i=8478:s2at=4:nm=6_2971 on theBenchmark for (2971ds/8478Mi)
% 22.74/3.91 % (3367515)Instruction limit reached!
% 22.74/3.91 % (3367515)------------------------------
% 22.74/3.91 % (3367515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367515)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367515)Termination reason: Instruction limit
% 22.74/3.91 % (3367515)Termination phase: Saturation
% 22.74/3.91 % (3367515)Time elapsed: 2.014 s
% 22.74/3.91 % (3367515)Peak memory usage: 138 MB
% 22.74/3.91 % (3367515)Instructions burned: 5208 (million)
% 22.74/3.91 % (3367712)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=961856227:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2969 on theBenchmark for (2969ds/303Mi)
% 22.74/3.91 % (3367627)First to succeed.
% 22.74/3.91 % (3367712)Instruction limit reached!
% 22.74/3.91 % (3367712)------------------------------
% 22.74/3.91 % (3367712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.74/3.91 % (3367712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.74/3.91 % (3367712)CaDiCaL version: 2.1.3
% 22.74/3.91 % (3367712)Termination reason: Instruction limit
% 22.74/3.91 % (3367712)Termination phase: Saturation
% 22.74/3.91 % (3367712)Time elapsed: 0.082 s
% 22.74/3.91 % (3367712)Peak memory usage: 90 MB
% 22.74/3.91 % (3367712)Instructions burned: 305 (million)
% 22.74/3.91 % (3367627)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3367348"
% 22.74/3.91 % (3367714)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=335476864:st=4:i=720:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/720Mi)
% 22.74/3.91 % SZS status Satisfiable for theBenchmark
% 22.74/3.91 % SZS output start Saturation.
% See solution above
% 24.96/4.12 % SZS output start Definitions and Model Updates.
% 24.96/4.12 for all inputs,
% 24.96/4.12 define c_WellTypeRT_OWTrt(X0,X1,X2,X3,X4) := $true
% 24.96/4.12 % SZS output end Definitions and Model Updates.
% 24.96/4.12 % (3367627)------------------------------
% 24.96/4.12 % (3367627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.12 % (3367627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.12 % (3367627)CaDiCaL version: 2.1.3
% 24.96/4.12 % (3367627)Termination reason: Satisfiable
% 24.96/4.12 % (3367627)Time elapsed: 0.689 s
% 24.96/4.12 % (3367627)Peak memory usage: 129 MB
% 24.96/4.12 % (3367627)Instructions burned: 1053 (million)
% 24.96/4.12 % (3367627)------------------------------
% 24.96/4.12 % (3367627)------------------------------
% 24.96/4.12 % (3367348)Success in time 3.483 s
% 24.96/4.12 % Vampire exiting
%------------------------------------------------------------------------------