%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL911+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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 11:56:59 AM UTC 2026
% Result : Satisfiable 19.22s 3.89s
% Output : Saturation 21.84s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u234,axiom,
is_a_theorem(X1) ).
cnf(u420,axiom,
is_a_theorem(necessarily(X0)) ).
cnf(u562,negated_conjecture,
is_a_theorem(necessarily(implies(X1,X1))) ).
cnf(u404,axiom,
( is_a_theorem(necessarily(implies(necessarily(X0),necessarily(X1))))
| ~ is_a_theorem(necessarily(necessarily(implies(X0,X1)))) ) ).
cnf(u339,axiom,
( is_a_theorem(implies(implies(not(X0),X0),X1))
| ~ is_a_theorem(not(X0)) ) ).
cnf(u367,negated_conjecture,
( ~ is_a_theorem(implies(implies(implies(X0,X1),X2),and(X0,not(X1))))
| is_a_theorem(equiv(implies(implies(X0,X1),X2),and(X0,not(X1)))) ) ).
cnf(u634,negated_conjecture,
( ~ is_a_theorem(implies(not(X0),not(not(X0))))
| is_a_theorem(not(not(X0))) ) ).
cnf(u578,negated_conjecture,
and(necessarily(implies(X0,X0)),X1) = X1 ).
cnf(u647,negated_conjecture,
is_a_theorem(not(not(implies(X0,X0)))) ).
cnf(u659,negated_conjecture,
is_a_theorem(equiv(not(not(X0)),X0)) ).
cnf(u593,negated_conjecture,
and(implies(X0,implies(X1,X1)),X2) = X2 ).
cnf(u198,negated_conjecture,
is_a_theorem(sF3(X0,X1)) ).
cnf(u153,axiom,
implies_1 ).
cnf(u213,axiom,
implies(implies(X0,X1),implies(implies(X1,X0),equiv(X0,X1))) = sF3(X0,X1) ).
cnf(u276,axiom,
is_a_theorem(implies(implies(not(X2),implies(X0,X1)),implies(and(X0,not(X1)),X2))) ).
cnf(u172,axiom,
necessitation ).
cnf(u624,negated_conjecture,
is_a_theorem(implies(implies(not(X0),not(not(X0))),not(not(X0)))) ).
cnf(u395,axiom,
( is_a_theorem(necessarily(implies(X0,X1)))
| ~ is_a_theorem(necessarily(X1)) ) ).
cnf(u216,negated_conjecture,
is_a_theorem(implies(equiv(X0,X1),implies(X1,X0))) ).
cnf(u638,negated_conjecture,
is_a_theorem(implies(not(not(X0)),implies(implies(X0,not(X0)),equiv(not(X0),X0)))) ).
cnf(u239,axiom,
is_a_theorem(implies(X0,implies(not(X0),X1))) ).
cnf(u192,axiom,
is_a_theorem(implies(necessarily(X0),X0)) ).
cnf(u314,negated_conjecture,
( is_a_theorem(implies(implies(X1,X0),equiv(X0,X1)))
| ~ is_a_theorem(implies(X0,X1)) ) ).
cnf(u202,axiom,
is_a_theorem(implies(X1,or(X0,X1))) ).
cnf(u242,axiom,
( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ) ).
cnf(u397,axiom,
( is_a_theorem(necessarily(implies(not(X0),X1)))
| ~ is_a_theorem(necessarily(X0)) ) ).
cnf(u478,negated_conjecture,
( ~ is_a_theorem(X0)
| and(X0,X1) = X1 ) ).
cnf(u490,negated_conjecture,
( ~ is_a_theorem(X0)
| and(implies(not(X0),X1),X2) = X2 ) ).
cnf(u493,negated_conjecture,
and(implies(X0,implies(X1,and(X0,X1))),X2) = X2 ).
cnf(u157,axiom,
and_2 ).
cnf(u640,negated_conjecture,
( is_a_theorem(implies(not(not(X0)),equiv(X0,not(X0))))
| ~ is_a_theorem(implies(X0,not(X0))) ) ).
cnf(u400,negated_conjecture,
( is_a_theorem(necessarily(implies(implies(X0,X1),equiv(X1,X0))))
| ~ is_a_theorem(necessarily(implies(X1,X0))) ) ).
cnf(u201,axiom,
is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2)))) ).
cnf(u148,axiom,
op_or ).
cnf(u160,axiom,
or_2 ).
cnf(u628,negated_conjecture,
( is_a_theorem(not(not(X0)))
| ~ is_a_theorem(X0) ) ).
cnf(u220,axiom,
( ~ is_a_theorem(and(X0,X1))
| is_a_theorem(X1) ) ).
cnf(u396,axiom,
( is_a_theorem(necessarily(implies(X0,and(X1,X0))))
| ~ is_a_theorem(necessarily(X1)) ) ).
cnf(u183,axiom,
implies(implies(X1,X0),equiv(X0,X1)) = sF2(X1,X0) ).
cnf(u626,negated_conjecture,
is_a_theorem(implies(equiv(X0,not(X0)),not(not(X0)))) ).
cnf(u227,axiom,
( is_a_theorem(implies(not(X0),X1))
| ~ is_a_theorem(X0) ) ).
cnf(u224,axiom,
( is_a_theorem(implies(X1,and(X0,X1)))
| ~ is_a_theorem(X0) ) ).
cnf(u496,negated_conjecture,
and(implies(implies(not(X0),not(X1)),implies(X1,X0)),X2) = X2 ).
cnf(u350,axiom,
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(necessarily(X1))
| ~ is_a_theorem(necessarily(X0)) ) ).
cnf(u513,negated_conjecture,
( ~ is_a_theorem(X1)
| and(and(X0,X1),X2) = X2
| ~ is_a_theorem(X0) ) ).
cnf(u246,axiom,
is_a_theorem(implies(and(X0,not(X1)),implies(implies(X0,X1),X2))) ).
cnf(u365,negated_conjecture,
( ~ is_a_theorem(implies(implies(X0,X1),equiv(X1,X0)))
| is_a_theorem(equiv(implies(X0,X1),equiv(X1,X0))) ) ).
cnf(u174,axiom,
axiom_M ).
cnf(u469,axiom,
( ~ is_a_theorem(and(X0,X1))
| is_a_theorem(necessarily(X0)) ) ).
cnf(u481,axiom,
( ~ is_a_theorem(and(X1,X0))
| is_a_theorem(necessarily(X0)) ) ).
cnf(u406,negated_conjecture,
( ~ is_a_theorem(necessarily(implies(X1,X0)))
| is_a_theorem(necessarily(equiv(X0,X1)))
| ~ is_a_theorem(implies(X0,X1)) ) ).
cnf(u205,axiom,
is_a_theorem(implies(and(X0,X1),X1)) ).
cnf(u637,negated_conjecture,
equiv(X0,not(X0)) = and(implies(X0,not(X0)),not(not(X0))) ).
cnf(u642,negated_conjecture,
( ~ is_a_theorem(necessarily(not(not(X0))))
| ~ is_a_theorem(necessarily(not(X0)))
| is_a_theorem(necessarily(X0)) ) ).
cnf(u196,axiom,
implies(X0,X1) = not(and(X0,not(X1))) ).
cnf(u208,axiom,
is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))) ).
cnf(u335,axiom,
is_a_theorem(implies(and(X2,implies(X0,X1)),implies(implies(X2,and(X0,not(X1))),X3))) ).
cnf(u495,negated_conjecture,
and(implies(implies(X0,implies(X0,X1)),implies(X0,X1)),X2) = X2 ).
cnf(u159,axiom,
or_1 ).
cnf(u171,axiom,
op_possibly ).
cnf(u639,negated_conjecture,
is_a_theorem(implies(implies(X0,not(X0)),implies(not(not(X0)),equiv(X0,not(X0))))) ).
cnf(u203,axiom,
is_a_theorem(implies(X0,or(X0,X1))) ).
cnf(u500,negated_conjecture,
and(implies(and(X0,not(X1)),implies(implies(X0,X1),X2)),X3) = X3 ).
cnf(u573,axiom,
( is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(necessarily(X0)) ) ).
cnf(u162,axiom,
equivalence_1 ).
cnf(u190,axiom,
possibly(X0) = not(necessarily(not(X0))) ).
cnf(u309,negated_conjecture,
is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X0),equiv(X0,X1)))) ).
cnf(u398,axiom,
( ~ is_a_theorem(necessarily(implies(X0,implies(X0,X1))))
| is_a_theorem(necessarily(implies(X0,X1))) ) ).
cnf(u177,axiom,
implies(equiv(X0,X1),implies(X0,X1)) = sF0(X0,X1) ).
cnf(u613,negated_conjecture,
not(implies(X0,X1)) = implies(implies(X0,X1),and(X0,not(X1))) ).
cnf(u488,negated_conjecture,
( ~ is_a_theorem(X1)
| and(implies(X0,X1),X2) = X2 ) ).
cnf(u627,negated_conjecture,
is_a_theorem(implies(equiv(not(X0),X0),not(not(X0)))) ).
cnf(u207,axiom,
is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) ).
cnf(u621,negated_conjecture,
is_a_theorem(implies(necessarily(not(not(X0))),implies(necessarily(not(X0)),necessarily(X0)))) ).
cnf(u210,axiom,
is_a_theorem(implies(implies(not(X1),not(X0)),implies(X0,X1))) ).
cnf(u585,axiom,
( ~ is_a_theorem(necessarily(not(X0)))
| is_a_theorem(implies(X0,X1)) ) ).
cnf(u401,negated_conjecture,
( ~ is_a_theorem(necessarily(equiv(X1,X0)))
| is_a_theorem(necessarily(implies(X0,X1))) ) ).
cnf(u360,negated_conjecture,
( ~ is_a_theorem(implies(implies(X0,and(X1,X0)),X1))
| is_a_theorem(equiv(implies(X0,and(X1,X0)),X1)) ) ).
cnf(u355,negated_conjecture,
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(equiv(X0,X1))
| ~ is_a_theorem(X0) ) ).
cnf(u383,negated_conjecture,
is_a_theorem(equiv(equiv(X0,X0),implies(X0,X0))) ).
cnf(u492,negated_conjecture,
and(implies(X0,implies(X1,X0)),X2) = X2 ).
cnf(u487,negated_conjecture,
( ~ is_a_theorem(not(X0))
| and(implies(X0,X1),X2) = X2 ) ).
cnf(u151,axiom,
modus_ponens ).
cnf(u594,negated_conjecture,
( is_a_theorem(equiv(implies(X0,X0),X1))
| ~ is_a_theorem(not(not(X1))) ) ).
cnf(u195,negated_conjecture,
equiv(X0,X1) = sF4(X0,X1) ).
cnf(u663,negated_conjecture,
( ~ is_a_theorem(necessarily(X0))
| and(necessarily(implies(not(X0),X1)),X2) = X2 ) ).
cnf(u154,axiom,
implies_2 ).
cnf(u214,axiom,
is_a_theorem(implies(not(necessarily(not(X0))),necessarily(not(necessarily(not(X0)))))) ).
cnf(u449,negated_conjecture,
implies(not(X0),X0) = not(not(X0)) ).
cnf(u304,axiom,
( is_a_theorem(implies(X2,and(X0,not(X1))))
| ~ is_a_theorem(not(implies(X0,X1))) ) ).
cnf(u188,axiom,
and(implies(X0,X1),implies(X1,X0)) = sF4(X0,X1) ).
cnf(u512,negated_conjecture,
( ~ is_a_theorem(X0)
| and(equiv(and(X0,X1),X1),X2) = X2 ) ).
cnf(u352,negated_conjecture,
( ~ is_a_theorem(implies(X0,and(X0,X1)))
| is_a_theorem(equiv(X0,and(X0,X1))) ) ).
cnf(u408,axiom,
( is_a_theorem(necessarily(and(X0,X0)))
| ~ is_a_theorem(necessarily(X0)) ) ).
cnf(u359,negated_conjecture,
( ~ is_a_theorem(implies(implies(X0,X1),X1))
| is_a_theorem(equiv(implies(X0,X1),X1)) ) ).
cnf(u644,negated_conjecture,
( is_a_theorem(necessarily(not(not(X0))))
| ~ is_a_theorem(necessarily(X0)) ) ).
cnf(u535,negated_conjecture,
is_a_theorem(implies(X0,implies(X1,X1))) ).
cnf(u651,axiom,
( is_a_theorem(implies(and(X0,not(X1)),X2))
| ~ is_a_theorem(necessarily(implies(X0,X1))) ) ).
cnf(u158,axiom,
and_3 ).
cnf(u377,negated_conjecture,
is_a_theorem(equiv(necessarily(not(necessarily(not(X0)))),not(necessarily(not(X0))))) ).
cnf(u494,negated_conjecture,
and(implies(X0,implies(not(X0),X1)),X2) = X2 ).
cnf(u657,negated_conjecture,
and(implies(X0,not(not(X0))),X1) = X1 ).
cnf(u509,negated_conjecture,
( ~ is_a_theorem(necessarily(implies(X0,X1)))
| and(implies(necessarily(X0),necessarily(X1)),X2) = X2 ) ).
cnf(u173,axiom,
axiom_K ).
cnf(u217,negated_conjecture,
is_a_theorem(implies(equiv(X0,X1),implies(X0,X1))) ).
cnf(u164,axiom,
equivalence_3 ).
cnf(u340,axiom,
( ~ is_a_theorem(and(X2,implies(X0,X1)))
| is_a_theorem(implies(implies(X2,and(X0,not(X1))),X3)) ) ).
cnf(u275,axiom,
is_a_theorem(implies(implies(implies(X0,X1),not(X2)),implies(X2,and(X0,not(X1))))) ).
cnf(u303,axiom,
( ~ is_a_theorem(not(not(X0)))
| is_a_theorem(implies(X1,X0)) ) ).
cnf(u384,negated_conjecture,
is_a_theorem(equiv(implies(X0,X1),implies(X0,implies(X0,X1)))) ).
cnf(u412,axiom,
( ~ is_a_theorem(necessarily(implies(X1,X0)))
| ~ is_a_theorem(necessarily(necessarily(X1)))
| is_a_theorem(necessarily(necessarily(X0))) ) ).
cnf(u347,axiom,
( is_a_theorem(implies(implies(implies(X0,X1),and(X0,not(X1))),X2))
| ~ is_a_theorem(implies(X0,X1)) ) ).
cnf(u407,axiom,
( is_a_theorem(necessarily(and(X0,X1)))
| ~ is_a_theorem(necessarily(X1))
| ~ is_a_theorem(X0) ) ).
cnf(u586,negated_conjecture,
( ~ is_a_theorem(necessarily(X0))
| and(implies(X1,X0),X2) = X2 ) ).
cnf(u306,negated_conjecture,
equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ).
cnf(u646,negated_conjecture,
( ~ is_a_theorem(necessarily(X0))
| is_a_theorem(not(not(X0))) ) ).
cnf(u366,negated_conjecture,
( ~ is_a_theorem(implies(implies(X0,X1),equiv(X0,X1)))
| is_a_theorem(equiv(implies(X0,X1),equiv(X0,X1))) ) ).
cnf(u529,negated_conjecture,
( ~ is_a_theorem(equiv(X0,X1))
| is_a_theorem(necessarily(implies(X1,X0))) ) ).
cnf(u381,negated_conjecture,
( is_a_theorem(equiv(and(X0,X1),X1))
| ~ is_a_theorem(X0) ) ).
cnf(u206,axiom,
is_a_theorem(implies(and(X0,X1),X0)) ).
cnf(u485,negated_conjecture,
and(implies(and(X0,X1),X0),X2) = X2 ).
cnf(u149,axiom,
op_implies_and ).
cnf(u193,axiom,
is_a_theorem(implies(necessarily(implies(X0,X1)),implies(necessarily(X0),necessarily(X1)))) ).
cnf(u221,negated_conjecture,
( ~ is_a_theorem(equiv(X0,X1))
| is_a_theorem(implies(X1,X0)) ) ).
cnf(u284,axiom,
( is_a_theorem(and(X0,X0))
| ~ is_a_theorem(X0) ) ).
cnf(u152,axiom,
modus_tollens ).
cnf(u212,axiom,
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ) ).
cnf(u388,axiom,
( ~ is_a_theorem(necessarily(and(X0,X1)))
| is_a_theorem(necessarily(X0)) ) ).
cnf(u323,negated_conjecture,
is_a_theorem(equiv(X0,X0)) ).
cnf(u351,negated_conjecture,
( ~ is_a_theorem(implies(X0,necessarily(X0)))
| is_a_theorem(equiv(X0,necessarily(X0))) ) ).
cnf(u574,negated_conjecture,
( ~ is_a_theorem(necessarily(X0))
| and(necessarily(implies(X1,X0)),X2) = X2 ) ).
cnf(u175,axiom,
axiom_5 ).
cnf(u618,negated_conjecture,
is_a_theorem(implies(not(not(not(X0))),implies(X0,not(X0)))) ).
cnf(u219,axiom,
( ~ is_a_theorem(and(X0,X1))
| is_a_theorem(X0) ) ).
cnf(u690,negated_conjecture,
X0 = X1 ).
cnf(u497,negated_conjecture,
and(implies(implies(X0,X1),implies(implies(X1,X0),equiv(X0,X1))),X2) = X2 ).
cnf(u354,negated_conjecture,
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(equiv(X0,X1))
| ~ is_a_theorem(not(X1)) ) ).
cnf(u297,axiom,
( ~ is_a_theorem(implies(implies(X0,X1),not(X2)))
| is_a_theorem(implies(X2,and(X0,not(X1)))) ) ).
cnf(u357,negated_conjecture,
( ~ is_a_theorem(implies(X0,not(X1)))
| is_a_theorem(equiv(X0,not(X1)))
| ~ is_a_theorem(X1) ) ).
cnf(u486,negated_conjecture,
and(implies(X0,X0),X1) = X1 ).
cnf(u403,axiom,
( ~ is_a_theorem(necessarily(and(X0,not(X1))))
| is_a_theorem(necessarily(implies(implies(X0,X1),X2))) ) ).
cnf(u272,axiom,
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(X0,X1)) ) ).
cnf(u156,axiom,
and_1 ).
cnf(u332,axiom,
( ~ is_a_theorem(necessarily(implies(X0,X1)))
| ~ is_a_theorem(necessarily(X0))
| is_a_theorem(necessarily(X1)) ) ).
cnf(u636,negated_conjecture,
equiv(not(X0),X0) = and(not(not(X0)),implies(X0,not(X0))) ).
cnf(u504,negated_conjecture,
( ~ is_a_theorem(X1)
| and(implies(X0,and(X1,X0)),X2) = X2 ) ).
cnf(u327,axiom,
is_a_theorem(implies(not(necessarily(implies(X0,X1))),necessarily(not(necessarily(implies(X0,X1)))))) ).
cnf(u499,negated_conjecture,
and(implies(equiv(X0,X1),implies(X0,X1)),X2) = X2 ).
cnf(u163,axiom,
equivalence_2 ).
cnf(u515,negated_conjecture,
( ~ is_a_theorem(X0)
| and(necessarily(X0),X1) = X1 ) ).
cnf(u223,axiom,
( is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(X0) ) ).
cnf(u298,axiom,
( ~ is_a_theorem(implies(not(X2),implies(X0,X1)))
| is_a_theorem(implies(and(X0,not(X1)),X2)) ) ).
cnf(u580,negated_conjecture,
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(equiv(X0,X1))
| ~ is_a_theorem(necessarily(X0)) ) ).
cnf(u358,negated_conjecture,
( ~ is_a_theorem(implies(X0,and(X1,X0)))
| is_a_theorem(equiv(X0,and(X1,X0))) ) ).
cnf(u681,negated_conjecture,
and(not(not(X0)),X1) = X1 ).
cnf(u405,negated_conjecture,
( ~ is_a_theorem(necessarily(implies(X0,X0)))
| is_a_theorem(necessarily(equiv(X0,X0))) ) ).
cnf(u364,negated_conjecture,
( ~ is_a_theorem(implies(implies(implies(X0,X1),equiv(X1,X0)),implies(X1,X0)))
| is_a_theorem(equiv(implies(implies(X0,X1),equiv(X1,X0)),implies(X1,X0))) ) ).
cnf(u376,negated_conjecture,
( ~ is_a_theorem(implies(necessarily(X0),necessarily(X1)))
| is_a_theorem(equiv(necessarily(X0),necessarily(X1)))
| ~ is_a_theorem(necessarily(implies(X1,X0))) ) ).
cnf(u552,negated_conjecture,
not(not(X0)) = implies(implies(X1,X1),X0) ).
cnf(u204,axiom,
is_a_theorem(implies(X0,implies(X1,and(X0,X1)))) ).
cnf(u656,negated_conjecture,
is_a_theorem(implies(not(not(X0)),X0)) ).
cnf(u508,negated_conjecture,
and(implies(not(necessarily(not(X0))),necessarily(not(necessarily(not(X0))))),X1) = X1 ).
cnf(u503,negated_conjecture,
( ~ is_a_theorem(implies(X1,X0))
| and(implies(implies(X0,X1),equiv(X1,X0)),X2) = X2 ) ).
cnf(u211,negated_conjecture,
( ~ is_a_theorem(equiv(X0,X1))
| X0 = X1 ) ).
cnf(u274,axiom,
( ~ is_a_theorem(implies(not(X0),not(X1)))
| is_a_theorem(implies(X1,X0)) ) ).
cnf(u277,axiom,
is_a_theorem(implies(X0,X0)) ).
cnf(u474,negated_conjecture,
( ~ is_a_theorem(equiv(X0,X1))
| is_a_theorem(necessarily(implies(X0,X1))) ) ).
cnf(u245,axiom,
implies(X2,and(X0,not(X1))) = not(and(X2,implies(X0,X1))) ).
cnf(u308,axiom,
( is_a_theorem(implies(necessarily(X0),necessarily(X1)))
| ~ is_a_theorem(necessarily(implies(X0,X1))) ) ).
cnf(u380,negated_conjecture,
is_a_theorem(equiv(and(X0,X0),X0)) ).
cnf(u315,negated_conjecture,
( ~ is_a_theorem(implies(X1,X0))
| is_a_theorem(equiv(X0,X1))
| ~ is_a_theorem(implies(X0,X1)) ) ).
cnf(u248,axiom,
( ~ is_a_theorem(and(X0,not(X1)))
| is_a_theorem(implies(implies(X0,X1),X2)) ) ).
cnf(u484,negated_conjecture,
and(implies(necessarily(X0),X0),X1) = X1 ).
cnf(u491,negated_conjecture,
and(implies(and(X0,X1),X1),X2) = X2 ).
cnf(u155,axiom,
implies_3 ).
cnf(u623,negated_conjecture,
is_a_theorem(implies(X0,not(not(X0)))) ).
cnf(u215,axiom,
or(X0,X1) = implies(not(X0),X1) ).
cnf(u658,negated_conjecture,
is_a_theorem(implies(and(X0,not(X1)),not(implies(X0,X1)))) ).
cnf(u278,axiom,
is_a_theorem(implies(X0,and(X0,X0))) ).
cnf(u322,negated_conjecture,
is_a_theorem(implies(implies(X0,X0),equiv(X0,X0))) ).
cnf(u218,axiom,
( ~ is_a_theorem(necessarily(X0))
| is_a_theorem(X0) ) ).
cnf(u394,axiom,
( ~ is_a_theorem(necessarily(and(X1,X0)))
| is_a_theorem(necessarily(X0)) ) ).
cnf(u454,negated_conjecture,
implies(X0,X0) = equiv(X0,X0) ).
cnf(u161,axiom,
or_3 ).
cnf(u296,axiom,
( is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(not(X0)) ) ).
cnf(u180,axiom,
implies(equiv(X0,X1),implies(X1,X0)) = sF1(X0,X1) ).
cnf(u356,negated_conjecture,
( ~ is_a_theorem(implies(X0,implies(not(X1),X1)))
| is_a_theorem(equiv(X0,implies(not(X1),X1)))
| ~ is_a_theorem(not(X1)) ) ).
cnf(u368,negated_conjecture,
( ~ is_a_theorem(implies(implies(necessarily(X0),necessarily(X1)),necessarily(implies(X0,X1))))
| is_a_theorem(equiv(implies(necessarily(X0),necessarily(X1)),necessarily(implies(X0,X1)))) ) ).
cnf(u399,axiom,
( ~ is_a_theorem(necessarily(implies(not(X1),not(X0))))
| is_a_theorem(necessarily(implies(X0,X1))) ) ).
cnf(u428,negated_conjecture,
and(X0,X0) = X0 ).
cnf(u363,negated_conjecture,
( ~ is_a_theorem(implies(implies(X0,X1),implies(not(X1),not(X0))))
| is_a_theorem(equiv(implies(X0,X1),implies(not(X1),not(X0)))) ) ).
cnf(u338,axiom,
( is_a_theorem(implies(implies(X0,X1),X2))
| ~ is_a_theorem(not(X1))
| ~ is_a_theorem(X0) ) ).
cnf(u402,negated_conjecture,
( ~ is_a_theorem(necessarily(equiv(X0,X1)))
| is_a_theorem(necessarily(implies(X0,X1))) ) ).
cnf(u662,axiom,
( is_a_theorem(implies(not(X0),X1))
| ~ is_a_theorem(necessarily(X0)) ) ).
cnf(u382,negated_conjecture,
( is_a_theorem(equiv(equiv(X0,X1),implies(X1,X0)))
| ~ is_a_theorem(implies(X0,X1)) ) ).
cnf(u150,axiom,
op_equiv ).
cnf(u194,axiom,
( is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X0) ) ).
cnf(u222,negated_conjecture,
( ~ is_a_theorem(equiv(X0,X1))
| is_a_theorem(implies(X0,X1)) ) ).
cnf(u501,negated_conjecture,
and(implies(necessarily(implies(X0,X1)),implies(necessarily(X0),necessarily(X1))),X2) = X2 ).
cnf(u165,axiom,
substitution_of_equivalents ).
cnf(u209,axiom,
is_a_theorem(implies(X0,implies(X1,X0))) ).
cnf(u498,negated_conjecture,
and(implies(equiv(X0,X1),implies(X1,X0)),X2) = X2 ).
cnf(u361,negated_conjecture,
( ~ is_a_theorem(implies(implies(not(X0),X1),X0))
| is_a_theorem(equiv(implies(not(X0),X1),X0)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL911+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n001.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 17:11:46 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 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
% 3.79/1.48 % (3807653)Detected formulas, will run a generic FOF schedule.
% 3.79/1.48 % (3807753)dis-21_1_sil=8000:lcm=predicate:random_seed=3574979710:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.79/1.48 % (3807753)Refutation not found, incomplete strategy
% 3.79/1.48 % (3807753)------------------------------
% 3.79/1.48 % (3807753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.48 % (3807753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.48 % (3807753)CaDiCaL version: 2.1.3
% 3.79/1.48 % (3807753)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.48 % (3807753)Time elapsed: 0.0000 s
% 3.79/1.48 % (3807753)Peak memory usage: 86 MB
% 3.79/1.48 % (3807749)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3253171466:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.79/1.48 % (3807748)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=351869380:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.79/1.48 % (3807750)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3110845964:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.79/1.48 % (3807747)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=1142497023:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.79/1.48 % (3807751)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=575070183:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.79/1.48 % (3807750)Refutation not found, incomplete strategy
% 3.79/1.48 % (3807750)------------------------------
% 3.79/1.48 % (3807750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.48 % (3807750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.48 % (3807750)CaDiCaL version: 2.1.3
% 3.79/1.48 % (3807750)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.48 % (3807750)Time elapsed: 0.004 s
% 3.79/1.48 % (3807750)Peak memory usage: 86 MB
% 3.79/1.48 % (3807751)Refutation not found, incomplete strategy
% 3.79/1.48 % (3807751)------------------------------
% 3.79/1.48 % (3807751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.48 % (3807751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.48 % (3807751)CaDiCaL version: 2.1.3
% 3.79/1.48 % (3807751)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.48 % (3807751)Time elapsed: 0.003 s
% 3.79/1.48 % (3807751)Peak memory usage: 86 MB
% 3.79/1.48 % (3807752)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1179270208:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.79/1.48 % (3807752)Refutation not found, incomplete strategy
% 3.79/1.48 % (3807752)------------------------------
% 3.79/1.48 % (3807752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.48 % (3807752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.48 % (3807752)CaDiCaL version: 2.1.3
% 3.79/1.48 % (3807752)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.48 % (3807752)Time elapsed: 0.042 s
% 3.79/1.48 % (3807752)Peak memory usage: 90 MB
% 3.79/1.48 % (3807752)Instructions burned: 66 (million)
% 3.79/1.48 % (3807753)------------------------------
% 3.79/1.48 % (3807753)------------------------------
% 3.79/1.48 % (3807751)------------------------------
% 3.79/1.48 % (3807751)------------------------------
% 3.79/1.48 % (3807774)lrs+10_1_sil=8000:sp=occurrence:random_seed=2100327880:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 3.79/1.48 % (3807774)Refutation not found, incomplete strategy
% 3.79/1.48 % (3807774)------------------------------
% 3.79/1.48 % (3807774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.48 % (3807774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.48 % (3807774)CaDiCaL version: 2.1.3
% 3.79/1.48 % (3807774)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.48 % (3807774)Time elapsed: 0.0000 s
% 3.79/1.48 % (3807774)Peak memory usage: 86 MB
% 3.79/1.48 % (3807750)------------------------------
% 7.40/2.10 % (3807750)------------------------------
% 7.40/2.10 % (3807752)------------------------------
% 7.40/2.10 % (3807752)------------------------------
% 7.40/2.10 [W927 17:11:47.014243441 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014281211 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014319628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014331608 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014356595 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014367698 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014392615 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014403722 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014428689 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014439776 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014465646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014476709 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.40/2.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.40/2.10 [W927 17:11:47.014543660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.50/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.50/2.80 [W927 17:11:47.014572683 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.50/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.50/2.80 [W927 17:11:47.014610837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.50/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.50/2.80 [W927 17:11:47.014634957 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.50/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.71/2.80 [W927 17:11:47.014661054 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.71/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.71/2.80 [W927 17:11:47.014671271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.71/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.71/2.80 [W927 17:11:47.014695627 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.71/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.71/2.80 [W927 17:11:47.014706171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.71/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.71/2.80 [W927 17:11:47.014730738 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.71/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.71/2.80 [W927 17:11:47.014740808 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.71/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.71/2.80 [W927 17:11:47.014764875 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.71/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.71/2.80 [W927 17:11:47.014775361 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.71/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.71/2.80 % (3807775)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3125451592:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 12.71/2.80 % (3807775)Refutation not found, incomplete strategy
% 12.71/2.80 % (3807775)------------------------------
% 12.71/2.80 % (3807775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.71/2.80 % (3807775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.71/2.80 % (3807775)CaDiCaL version: 2.1.3
% 12.71/2.80 % (3807775)Termination reason: Refutation not found, incomplete strategy
% 12.90/2.92 % (3807775)Time elapsed: 0.001 s
% 12.90/2.92 % (3807775)Peak memory usage: 87 MB
% 12.90/2.92 % (3807774)------------------------------
% 12.90/2.92 % (3807774)------------------------------
% 12.90/2.92 % (3807777)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1932679254:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 12.90/2.92 % (3807777)Refutation not found, incomplete strategy
% 12.90/2.92 % (3807777)------------------------------
% 12.90/2.92 % (3807777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.90/2.92 % (3807777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.90/2.92 % (3807777)CaDiCaL version: 2.1.3
% 12.90/2.92 % (3807777)Termination reason: Refutation not found, incomplete strategy
% 12.90/2.92 % (3807777)Time elapsed: 0.001 s
% 12.90/2.92 % (3807777)Peak memory usage: 86 MB
% 12.90/2.92 % (3807778)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2241491776:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 12.90/2.92 % (3807748)Refutation not found, incomplete strategy
% 12.90/2.92 % (3807748)------------------------------
% 12.90/2.92 % (3807748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.90/2.92 % (3807748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.90/2.92 % (3807748)CaDiCaL version: 2.1.3
% 12.90/2.92 % (3807748)Termination reason: Refutation not found, incomplete strategy
% 12.90/2.92 % (3807748)Time elapsed: 0.548 s
% 12.90/2.92 % (3807748)Peak memory usage: 123 MB
% 12.90/2.92 % (3807748)Instructions burned: 822 (million)
% 12.90/2.92 % (3807749)Refutation not found, incomplete strategy
% 12.90/2.92 % (3807749)------------------------------
% 12.90/2.92 % (3807749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.90/2.92 % (3807749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.90/2.92 % (3807749)CaDiCaL version: 2.1.3
% 12.90/2.92 % (3807749)Termination reason: Refutation not found, incomplete strategy
% 12.90/2.92 % (3807749)Time elapsed: 0.576 s
% 12.90/2.92 % (3807749)Peak memory usage: 124 MB
% 12.90/2.92 % (3807749)Instructions burned: 826 (million)
% 12.90/2.92 % (3807780)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2628800413:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 12.90/2.92 % (3807780)Refutation not found, incomplete strategy
% 12.90/2.92 % (3807780)------------------------------
% 12.90/2.92 % (3807780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.90/2.92 % (3807780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.90/2.92 % (3807780)CaDiCaL version: 2.1.3
% 12.90/2.92 % (3807780)Termination reason: Refutation not found, incomplete strategy
% 12.90/2.92 % (3807780)Time elapsed: 0.001 s
% 12.90/2.92 % (3807780)Peak memory usage: 86 MB
% 12.90/2.92 % (3807778)Instruction limit reached!
% 12.90/2.92 % (3807778)------------------------------
% 12.90/2.92 % (3807778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.90/2.92 % (3807778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.90/2.92 % (3807778)CaDiCaL version: 2.1.3
% 12.90/2.92 % (3807778)Termination reason: Instruction limit
% 12.90/2.92 % (3807778)Termination phase: Saturation
% 12.90/2.92 % (3807778)Time elapsed: 0.222 s
% 12.90/2.92 % (3807778)Peak memory usage: 93 MB
% 12.90/2.92 % (3807778)Instructions burned: 248 (million)
% 12.90/2.92 % (3807775)------------------------------
% 12.90/2.92 % (3807775)------------------------------
% 12.90/2.92 % (3807777)------------------------------
% 12.90/2.92 % (3807777)------------------------------
% 12.90/2.92 % (3807780)------------------------------
% 12.90/2.92 % (3807780)------------------------------
% 12.90/2.92 % (3807748)------------------------------
% 12.90/2.92 % (3807748)------------------------------
% 12.90/2.92 % (3807749)------------------------------
% 12.90/2.92 % (3807749)------------------------------
% 12.90/2.92 % (3807796)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=400670705:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 12.90/2.92 % (3807800)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1585602997:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 12.90/2.92 % (3807800)Refutation not found, incomplete strategy
% 12.90/2.92 % (3807800)------------------------------
% 12.90/2.92 % (3807800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.90/2.92 % (3807800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.85/3.51 % (3807800)CaDiCaL version: 2.1.3
% 17.85/3.51 % (3807800)Termination reason: Refutation not found, incomplete strategy
% 17.85/3.51 % (3807800)Time elapsed: 0.001 s
% 17.85/3.51 % (3807800)Peak memory usage: 87 MB
% 17.85/3.51 % (3807803)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2486300939:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 17.85/3.51 % (3807803)Refutation not found, incomplete strategy
% 17.85/3.51 % (3807803)------------------------------
% 17.85/3.51 % (3807803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.85/3.51 % (3807803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.85/3.51 % (3807803)CaDiCaL version: 2.1.3
% 17.85/3.51 % (3807803)Termination reason: Refutation not found, incomplete strategy
% 17.85/3.51 % (3807803)Time elapsed: 0.001 s
% 17.85/3.51 % (3807803)Peak memory usage: 87 MB
% 17.85/3.51 % (3807802)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2463328906:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 17.85/3.51 % (3807802)Refutation not found, incomplete strategy
% 17.85/3.51 % (3807802)------------------------------
% 17.85/3.51 % (3807802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.85/3.51 % (3807802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.85/3.51 % (3807802)CaDiCaL version: 2.1.3
% 17.85/3.51 % (3807802)Termination reason: Refutation not found, incomplete strategy
% 17.85/3.51 % (3807802)Time elapsed: 0.002 s
% 17.85/3.51 % (3807802)Peak memory usage: 88 MB
% 17.85/3.51 % (3807802)Instructions burned: 1 (million)
% 17.85/3.51 % (3807805)lrs+10_1_sil=8000:sp=occurrence:random_seed=3989392918:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 17.85/3.51 % (3807805)Refutation not found, incomplete strategy
% 17.85/3.51 % (3807805)------------------------------
% 17.85/3.51 % (3807805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.85/3.51 % (3807805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.85/3.51 % (3807805)CaDiCaL version: 2.1.3
% 17.85/3.51 % (3807805)Termination reason: Refutation not found, incomplete strategy
% 17.85/3.51 % (3807805)Time elapsed: 0.001 s
% 17.85/3.51 % (3807805)Peak memory usage: 86 MB
% 17.85/3.51 % (3807807)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4097066111:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 17.85/3.51 % (3807807)Refutation not found, incomplete strategy
% 17.85/3.51 % (3807807)------------------------------
% 17.85/3.51 % (3807807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.85/3.51 % (3807807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.85/3.51 % (3807807)CaDiCaL version: 2.1.3
% 17.85/3.51 % (3807807)Termination reason: Refutation not found, incomplete strategy
% 17.85/3.51 % (3807807)Time elapsed: 0.001 s
% 17.85/3.51 % (3807807)Peak memory usage: 86 MB
% 17.85/3.51 % (3807803)------------------------------
% 17.85/3.51 % (3807803)------------------------------
% 17.85/3.51 % (3807800)------------------------------
% 17.85/3.51 % (3807800)------------------------------
% 17.85/3.51 % (3807802)------------------------------
% 17.85/3.51 % (3807802)------------------------------
% 17.85/3.51 % (3807819)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4125480199:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 17.85/3.51 % (3807807)------------------------------
% 17.85/3.51 % (3807807)------------------------------
% 17.85/3.51 % (3807805)------------------------------
% 17.85/3.51 % (3807805)------------------------------
% 17.85/3.51 % (3807823)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2120246138:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2983 on theBenchmark for (2983ds/134Mi)
% 17.85/3.51 % (3807823)Refutation not found, incomplete strategy
% 17.85/3.51 % (3807823)------------------------------
% 17.85/3.51 % (3807823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.85/3.51 % (3807823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.85/3.51 % (3807823)CaDiCaL version: 2.1.3
% 17.85/3.51 % (3807823)Termination reason: Refutation not found, incomplete strategy
% 17.85/3.51 % (3807823)Time elapsed: 0.001 s
% 17.85/3.51 % (3807823)Peak memory usage: 87 MB
% 17.85/3.51 % (3807825)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=647943237:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 19.22/3.80 % (3807825)Refutation not found, incomplete strategy
% 19.22/3.80 % (3807825)------------------------------
% 19.22/3.80 % (3807825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.80 % (3807825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.80 % (3807825)CaDiCaL version: 2.1.3
% 19.22/3.80 % (3807825)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.80 % (3807825)Time elapsed: 0.001 s
% 19.22/3.80 % (3807825)Peak memory usage: 86 MB
% 19.22/3.80 [W927 17:11:49.506609529 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.80 [W927 17:11:49.506647838 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.80 [W927 17:11:49.506683054 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.80 [W927 17:11:49.506695534 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.80 [W927 17:11:49.506721549 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.80 [W927 17:11:49.506732502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.80 [W927 17:11:49.506757006 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.80 [W927 17:11:49.506768885 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.80 [W927 17:11:49.506792922 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.80 [W927 17:11:49.506804161 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.80 [W927 17:11:49.506828577 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.80 [W927 17:11:49.506852067 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.88 % (3807828)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2576811461:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 19.22/3.88 % (3807829)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3526990716:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 19.22/3.88 % (3807829)Refutation not found, incomplete strategy
% 19.22/3.88 % (3807829)------------------------------
% 19.22/3.88 % (3807829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.88 % (3807829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.88 % (3807829)CaDiCaL version: 2.1.3
% 19.22/3.88 % (3807829)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.88 % (3807829)Time elapsed: 0.002 s
% 19.22/3.88 % (3807829)Peak memory usage: 87 MB
% 19.22/3.88 % (3807829)Instructions burned: 1 (million)
% 19.22/3.88 % (3807823)------------------------------
% 19.22/3.88 % (3807823)------------------------------
% 19.22/3.88 % (3807819)Refutation not found, incomplete strategy
% 19.22/3.88 % (3807819)------------------------------
% 19.22/3.88 % (3807819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.88 % (3807819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.88 % (3807819)CaDiCaL version: 2.1.3
% 19.22/3.88 % (3807819)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.88 % (3807819)Time elapsed: 0.494 s
% 19.22/3.88 % (3807819)Peak memory usage: 125 MB
% 19.22/3.88 % (3807819)Instructions burned: 828 (million)
% 19.22/3.88 % (3807825)------------------------------
% 19.22/3.88 % (3807825)------------------------------
% 19.22/3.88 % (3807819)------------------------------
% 19.22/3.88 % (3807819)------------------------------
% 19.22/3.88 % (3807829)------------------------------
% 19.22/3.88 % (3807829)------------------------------
% 19.22/3.88 % (3807840)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2384173806:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 19.22/3.89 % (3807840)First to succeed.
% 19.22/3.89 % (3807840)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3807653"
% 19.22/3.89 % (3807843)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3810224810:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 19.22/3.89 % (3807843)Refutation not found, incomplete strategy
% 19.22/3.89 % (3807843)------------------------------
% 19.22/3.89 % (3807843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.89 % (3807843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.89 % (3807843)CaDiCaL version: 2.1.3
% 19.22/3.89 % (3807843)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.89 % (3807843)Time elapsed: 0.001 s
% 19.22/3.89 % (3807843)Peak memory usage: 86 MB
% 19.22/3.89 [W927 17:11:50.093909728 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 [W927 17:11:50.093961289 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 [W927 17:11:50.094043322 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 [W927 17:11:50.094080416 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 [W927 17:11:50.094130123 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 [W927 17:11:50.094148537 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 [W927 17:11:50.094193264 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 [W927 17:11:50.094219650 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 [W927 17:11:50.094264091 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 [W927 17:11:50.094281284 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 [W927 17:11:50.094324148 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 [W927 17:11:50.094341115 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.22/3.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.22/3.89 % (3807849)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3368724510:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi)
% 19.22/3.89 % (3807849)Refutation not found, incomplete strategy
% 19.22/3.89 % (3807849)------------------------------
% 19.22/3.89 % (3807849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.89 % (3807849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.89 % (3807849)CaDiCaL version: 2.1.3
% 19.22/3.89 % (3807849)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.89 % (3807849)Time elapsed: 0.001 s
% 19.22/3.89 % (3807849)Peak memory usage: 86 MB
% 19.22/3.89 % (3807850)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1932766097:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 19.22/3.89 % (3807828)Refutation not found, incomplete strategy
% 19.22/3.89 % (3807828)------------------------------
% 19.22/3.89 % (3807828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.22/3.89 % (3807828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.22/3.89 % (3807828)CaDiCaL version: 2.1.3
% 19.22/3.89 % (3807828)Termination reason: Refutation not found, incomplete strategy
% 19.22/3.89 % (3807828)Time elapsed: 0.849 s
% 19.22/3.89 % (3807828)Peak memory usage: 125 MB
% 19.22/3.89 % (3807828)Instructions burned: 823 (million)
% 19.22/3.89 % (3807849)------------------------------
% 19.22/3.89 % (3807849)------------------------------
% 19.22/3.89 % (3807843)------------------------------
% 19.22/3.89 % (3807843)------------------------------
% 19.22/3.89 % SZS status Satisfiable for theBenchmark
% 19.22/3.89 % SZS output start Saturation.
% See solution above
% 21.84/4.16 % SZS output start Definitions and Model Updates.
% 21.84/4.16 for all inputs,
% 21.84/4.16 define op_and := $false
% 21.84/4.16 for all inputs,
% 21.84/4.16 define op_implies_or := $false
% 21.84/4.16 for all inputs,
% 21.84/4.16 define op_necessarily := $false
% 21.84/4.16 for all inputs,
% 21.84/4.16 define op_strict_implies := $false
% 21.84/4.16 for all inputs,
% 21.84/4.16 define op_strict_equiv := $false
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : ((is_a_theorem(X0) & is_a_theorem(implies(X0,X1))) => is_a_theorem(X1)) is true, set modus_ponens to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : (is_a_theorem(equiv(X0,X1)) => X0 = X1) is true, set substitution_of_equivalents to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(implies(not(X1),not(X0)),implies(X0,X1))) is true, set modus_tollens to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))) is true, set implies_1 to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))) is true, set implies_2 to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) is true, set implies_3 to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0)) is true, set and_1 to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X1)) is true, set and_2 to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,and(X0,X1)))) is true, set and_3 to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(X0,or(X0,X1))) is true, set or_1 to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(X1,or(X0,X1))) is true, set or_2 to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2)))) is true, set or_3 to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(equiv(X0,X1),implies(X0,X1))) is true, set equivalence_1 to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(equiv(X0,X1),implies(X1,X0))) is true, set equivalence_2 to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X0),equiv(X0,X1)))) is true, set equivalence_3 to true
% 21.84/4.16 for all inputs,
% 21.84/4.16 define kn1 := ! [X0] : is_a_theorem(implies(X0,and(X0,X0)))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define kn2 := ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define kn3 := ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0)))))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define cn1 := ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define cn2 := ! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1)))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define cn3 := ! [X0] : is_a_theorem(implies(implies(not(X0),X0),X0))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define r1 := ! [X0] : is_a_theorem(implies(or(X0,X0),X0))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define r2 := ! [X0,X1] : is_a_theorem(implies(X1,or(X0,X1)))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define r3 := ! [X0,X1] : is_a_theorem(implies(or(X0,X1),or(X1,X0)))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define r4 := ! [X0,X1,X2] : is_a_theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2))))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define r5 := ! [X0,X1,X2] : is_a_theorem(implies(implies(X1,X2),implies(or(X0,X1),or(X0,X2))))
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0] : (is_a_theorem(X0) => is_a_theorem(necessarily(X0))) is true, set necessitation to true
% 21.84/4.16 for all inputs,
% 21.84/4.16 define modus_ponens_strict_implies := ! [X0,X1] : ((is_a_theorem(X0) & is_a_theorem(strict_implies(X0,X1))) => is_a_theorem(X1))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define adjunction := ! [X0,X1] : ((is_a_theorem(X0) & is_a_theorem(X1)) => is_a_theorem(and(X0,X1)))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define substitution_strict_equiv := ! [X0,X1] : (is_a_theorem(strict_equiv(X0,X1)) => X0 = X1)
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0,X1] : is_a_theorem(implies(necessarily(implies(X0,X1)),implies(necessarily(X0),necessarily(X1)))) is true, set axiom_K to true
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0] : is_a_theorem(implies(necessarily(X0),X0)) is true, set axiom_M to true
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_4 := ! [X0] : is_a_theorem(implies(necessarily(X0),necessarily(necessarily(X0))))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_B := ! [X0] : is_a_theorem(implies(X0,necessarily(possibly(X0))))
% 21.84/4.16 for all groundings,
% 21.84/4.16 whenever ! [X0] : is_a_theorem(implies(possibly(X0),necessarily(possibly(X0)))) is true, set axiom_5 to true
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_s1 := ! [X0,X1,X2] : is_a_theorem(implies(and(necessarily(implies(X0,X1)),necessarily(implies(X1,X2))),necessarily(implies(X0,X2))))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_s2 := ! [X0,X1] : is_a_theorem(strict_implies(possibly(and(X0,X1)),and(possibly(X0),possibly(X1))))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_s3 := ! [X0,X1] : is_a_theorem(strict_implies(strict_implies(X0,X1),strict_implies(not(possibly(X1)),not(possibly(X0)))))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_s4 := ! [X0] : is_a_theorem(strict_implies(necessarily(X0),necessarily(necessarily(X0))))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_m1 := ! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),and(X1,X0)))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_m2 := ! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),X0))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_m3 := ! [X0,X1,X2] : is_a_theorem(strict_implies(and(and(X0,X1),X2),and(X0,and(X1,X2))))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_m4 := ! [X0] : is_a_theorem(strict_implies(X0,and(X0,X0)))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_m5 := ! [X0,X1,X2] : is_a_theorem(strict_implies(and(strict_implies(X0,X1),strict_implies(X1,X2)),strict_implies(X0,X2)))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_m6 := ! [X0] : is_a_theorem(strict_implies(X0,possibly(X0)))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_m7 := ! [X0,X1] : is_a_theorem(strict_implies(possibly(and(X0,X1)),X0))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_m8 := ! [X0,X1] : is_a_theorem(strict_implies(strict_implies(X0,X1),strict_implies(possibly(X0),possibly(X1))))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_m9 := ! [X0] : is_a_theorem(strict_implies(possibly(possibly(X0)),possibly(X0)))
% 21.84/4.16 for all inputs,
% 21.84/4.16 define axiom_m10 := ! [X0] : is_a_theorem(strict_implies(possibly(X0),necessarily(possibly(X0))))
% 21.84/4.16 % SZS output end Definitions and Model Updates.
% 21.84/4.16 % (3807840)------------------------------
% 21.84/4.16 % (3807840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.84/4.16 % (3807840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.84/4.16 % (3807840)CaDiCaL version: 2.1.3
% 21.84/4.16 % (3807840)Termination reason: Satisfiable
% 21.84/4.16 % (3807840)Time elapsed: 0.103 s
% 21.84/4.16 % (3807840)Peak memory usage: 90 MB
% 21.84/4.16 % (3807840)Instructions burned: 107 (million)
% 21.84/4.16 % (3807840)------------------------------
% 21.84/4.16 % (3807840)------------------------------
% 21.84/4.16 % (3807653)Success in time 3.005 s
% 21.84/4.16 % Vampire exiting
%------------------------------------------------------------------------------