%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL150-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:51:21 AM UTC 2026
% Result : Unsatisfiable 152.18s 26.11s
% Output : Refutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 17
% Syntax : Number of formulae : 299 ( 299 unt; 10 def)
% Number of atoms : 299 ( 298 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 14 con; 0-2 aty)
% Number of variables : 462 ( 462 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : implies(truth,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_1) ).
fof(f2,axiom,
! [X2,X0,X1] : implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))) = truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_2) ).
fof(f3,plain,
! [X2,X0,X1] : truth = implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X0,X1] : implies(implies(X0,X1),X1) = implies(implies(X1,X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_3) ).
fof(f5,axiom,
! [X0,X1] : implies(implies(not(X0),not(X1)),implies(X1,X0)) = truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_4) ).
fof(f6,plain,
! [X0,X1] : truth = implies(implies(not(X0),not(X1)),implies(X1,X0)),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X0,X1] : big_V(X0,X1) = implies(implies(X0,X1),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_V_definition) ).
fof(f8,plain,
! [X0,X1] : implies(implies(X0,X1),X1) = big_V(X0,X1),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X0,X1] : big_hat(X0,X1) = not(big_V(not(X0),not(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_hat_definition) ).
fof(f14,negated_conjecture,
implies(big_hat(x,y),z) != big_V(implies(x,z),implies(y,z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_wajsberg_theorem) ).
fof(f15,plain,
! [X0,X1] : big_hat(X0,X1) = not(implies(implies(not(X0),not(X1)),not(X1))),
inference(definition_unfolding,[],[f9,f8]) ).
fof(f16,plain,
implies(not(implies(implies(not(x),not(y)),not(y))),z) != implies(implies(implies(x,z),implies(y,z)),implies(y,z)),
inference(definition_unfolding,[],[f14,f15,f8]) ).
fof(f17,definition,
sF0 = not(x),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f18,plain,
not(x) = sF0,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF1 = not(y),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f20,plain,
not(y) = sF1,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF2 = implies(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f22,plain,
implies(sF0,sF1) = sF2,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF3 = implies(sF2,sF1),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f24,plain,
implies(sF2,sF1) = sF3,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF4 = not(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f26,plain,
not(sF3) = sF4,
inference(reorient_equations,[],[f25]) ).
fof(f27,definition,
sF5 = implies(sF4,z),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f28,plain,
implies(sF4,z) = sF5,
inference(reorient_equations,[],[f27]) ).
fof(f29,definition,
sF6 = implies(x,z),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f30,plain,
implies(x,z) = sF6,
inference(reorient_equations,[],[f29]) ).
fof(f31,definition,
sF7 = implies(y,z),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f32,plain,
implies(y,z) = sF7,
inference(reorient_equations,[],[f31]) ).
fof(f33,definition,
sF8 = implies(sF6,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f34,plain,
implies(sF6,sF7) = sF8,
inference(reorient_equations,[],[f33]) ).
fof(f35,definition,
sF9 = implies(sF8,sF7),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f36,plain,
implies(sF8,sF7) = sF9,
inference(reorient_equations,[],[f35]) ).
fof(f37,plain,
sF5 != sF9,
inference(definition_folding,[],[f16,f36,f32,f34,f32,f30,f28,f26,f24,f20,f22,f20,f18]) ).
fof(f41,plain,
! [X2,X3,X0,X1] : truth = implies(truth,implies(implies(implies(implies(X1,X2),implies(X0,X2)),X3),implies(implies(X0,X1),X3))),
inference(superposition,[],[f3,f3]) ).
fof(f43,plain,
! [X2,X0,X1] : truth = implies(implies(X0,implies(not(X1),not(X2))),implies(truth,implies(X0,implies(X2,X1)))),
inference(superposition,[],[f3,f6]) ).
fof(f48,plain,
! [X0,X1] : truth = implies(implies(truth,X1),implies(implies(X1,X0),X0)),
inference(superposition,[],[f3,f1]) ).
fof(f52,plain,
! [X0,X1] : truth = implies(X1,implies(implies(X1,X0),X0)),
inference(forward_demodulation,[],[f48,f1]) ).
fof(f54,plain,
! [X2,X0,X1] : truth = implies(implies(X0,implies(not(X1),not(X2))),implies(X0,implies(X2,X1))),
inference(forward_demodulation,[],[f43,f1]) ).
fof(f56,plain,
! [X2,X3,X0,X1] : truth = implies(implies(implies(implies(X1,X2),implies(X0,X2)),X3),implies(implies(X0,X1),X3)),
inference(forward_demodulation,[],[f41,f1]) ).
fof(f70,plain,
! [X2,X0,X1] : implies(implies(implies(implies(X0,X1),implies(X2,X1)),implies(X2,X0)),implies(X2,X0)) = implies(truth,implies(implies(X0,X1),implies(X2,X1))),
inference(superposition,[],[f4,f3]) ).
fof(f72,plain,
implies(implies(z,x),x) = implies(sF6,z),
inference(superposition,[],[f4,f30]) ).
fof(f81,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X2,X1)) = implies(implies(implies(implies(X0,X1),implies(X2,X1)),implies(X2,X0)),implies(X2,X0)),
inference(forward_demodulation,[],[f70,f1]) ).
fof(f103,plain,
implies(sF8,sF7) = implies(implies(sF7,sF6),sF6),
inference(superposition,[],[f4,f34]) ).
fof(f108,plain,
sF9 = implies(implies(sF7,sF6),sF6),
inference(forward_demodulation,[],[f103,f36]) ).
fof(f111,plain,
implies(sF2,sF1) = implies(implies(sF1,sF0),sF0),
inference(superposition,[],[f4,f22]) ).
fof(f116,plain,
sF3 = implies(implies(sF1,sF0),sF0),
inference(forward_demodulation,[],[f111,f24]) ).
fof(f125,plain,
! [X2,X0,X1] : implies(truth,implies(X2,implies(X1,X0))) = implies(implies(implies(truth,implies(X2,implies(X1,X0))),implies(X2,implies(not(X0),not(X1)))),implies(X2,implies(not(X0),not(X1)))),
inference(superposition,[],[f81,f6]) ).
fof(f129,plain,
! [X2,X0,X1] : implies(implies(implies(X0,X1),X1),implies(X2,X0)) = implies(implies(implies(implies(implies(X0,X1),X1),implies(X2,X0)),implies(X2,implies(X1,X0))),implies(X2,implies(X1,X0))),
inference(superposition,[],[f81,f4]) ).
fof(f154,plain,
! [X0,X1] : implies(implies(X0,X1),implies(truth,X1)) = implies(implies(implies(implies(X0,X1),implies(truth,X1)),X0),X0),
inference(superposition,[],[f81,f1]) ).
fof(f159,plain,
! [X2,X0,X1] : implies(implies(X0,X2),implies(implies(X1,X0),X2)) = implies(implies(implies(implies(X0,X2),implies(implies(X1,X0),X2)),implies(implies(X0,X1),X1)),implies(implies(X0,X1),X1)),
inference(superposition,[],[f81,f4]) ).
fof(f173,plain,
! [X0,X1] : implies(implies(X0,X1),X1) = implies(implies(implies(implies(X0,X1),X1),X0),X0),
inference(forward_demodulation,[],[f154,f1]) ).
fof(f178,plain,
! [X2,X0,X1] : implies(X2,implies(X1,X0)) = implies(implies(implies(X2,implies(X1,X0)),implies(X2,implies(not(X0),not(X1)))),implies(X2,implies(not(X0),not(X1)))),
inference(forward_demodulation,[],[f125,f1]) ).
fof(f182,plain,
! [X0,X1] : implies(truth,implies(X1,X0)) = implies(implies(implies(truth,implies(X1,X0)),implies(not(X0),not(X1))),implies(not(X0),not(X1))),
inference(superposition,[],[f173,f6]) ).
fof(f210,plain,
! [X0,X1] : implies(X1,X0) = implies(implies(implies(X1,X0),implies(not(X0),not(X1))),implies(not(X0),not(X1))),
inference(forward_demodulation,[],[f182,f1]) ).
fof(f281,plain,
! [X0,X1] : truth = implies(X1,implies(implies(X0,X1),X1)),
inference(superposition,[],[f52,f4]) ).
fof(f285,plain,
! [X2,X0,X1] : truth = implies(truth,implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2))),
inference(superposition,[],[f3,f52]) ).
fof(f296,plain,
! [X0] : truth = implies(implies(truth,X0),X0),
inference(superposition,[],[f1,f52]) ).
fof(f300,plain,
! [X0] : truth = implies(X0,X0),
inference(forward_demodulation,[],[f296,f1]) ).
fof(f306,plain,
! [X2,X0,X1] : truth = implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2)),
inference(forward_demodulation,[],[f285,f1]) ).
fof(f366,plain,
! [X2,X0,X1] : truth = implies(implies(implies(implies(X0,X1),X1),X2),implies(X1,X2)),
inference(superposition,[],[f306,f4]) ).
fof(f396,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),X1) = implies(truth,implies(X0,X1)),
inference(superposition,[],[f173,f306]) ).
fof(f415,plain,
! [X0,X1] : implies(X0,X1) = implies(implies(implies(X0,X1),X1),X1),
inference(forward_demodulation,[],[f396,f1]) ).
fof(f456,plain,
sF8 = implies(implies(sF8,sF7),sF7),
inference(superposition,[],[f415,f34]) ).
fof(f459,plain,
! [X0,X1] : implies(X1,X0) = implies(implies(implies(X0,X1),X1),X0),
inference(superposition,[],[f415,f4]) ).
fof(f479,plain,
sF8 = implies(sF9,sF7),
inference(forward_demodulation,[],[f456,f36]) ).
fof(f660,plain,
! [X2,X0,X1] : truth = implies(truth,implies(implies(X2,implies(X0,X1)),implies(X0,implies(X2,X1)))),
inference(superposition,[],[f56,f306]) ).
fof(f753,plain,
! [X2,X0,X1] : truth = implies(implies(X2,implies(X0,X1)),implies(X0,implies(X2,X1))),
inference(forward_demodulation,[],[f660,f1]) ).
fof(f902,plain,
! [X2,X0,X1] : implies(truth,implies(X1,implies(X0,X2))) = implies(implies(implies(truth,implies(X1,implies(X0,X2))),implies(X0,implies(X1,X2))),implies(X0,implies(X1,X2))),
inference(superposition,[],[f173,f753]) ).
fof(f911,plain,
! [X2,X0,X1] : implies(X1,implies(X0,X2)) = implies(implies(implies(X1,implies(X0,X2)),implies(X0,implies(X1,X2))),implies(X0,implies(X1,X2))),
inference(forward_demodulation,[],[f902,f1]) ).
fof(f951,plain,
! [X2,X0,X1] : implies(X1,implies(X0,X2)) = implies(truth,implies(X0,implies(X1,X2))),
inference(forward_demodulation,[],[f911,f753]) ).
fof(f961,plain,
! [X2,X0,X1] : implies(X0,implies(X1,X2)) = implies(X1,implies(X0,X2)),
inference(forward_demodulation,[],[f951,f1]) ).
fof(f1011,plain,
! [X0,X1] : implies(X1,truth) = implies(X0,implies(X1,X0)),
inference(superposition,[],[f961,f300]) ).
fof(f1015,plain,
! [X2,X0,X1] : implies(X2,implies(implies(X0,X1),X1)) = implies(implies(X1,X0),implies(X2,X0)),
inference(superposition,[],[f961,f4]) ).
fof(f1016,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = implies(implies(implies(X0,X1),X1),implies(X2,X1)),
inference(superposition,[],[f961,f415]) ).
fof(f1026,plain,
! [X0] : implies(X0,sF6) = implies(x,implies(X0,z)),
inference(superposition,[],[f961,f30]) ).
fof(f1027,plain,
! [X0] : implies(X0,sF7) = implies(y,implies(X0,z)),
inference(superposition,[],[f961,f32]) ).
fof(f1031,plain,
! [X0] : implies(X0,sF5) = implies(sF4,implies(X0,z)),
inference(superposition,[],[f961,f28]) ).
fof(f1032,plain,
! [X0] : implies(X0,sF8) = implies(sF6,implies(X0,sF7)),
inference(superposition,[],[f961,f34]) ).
fof(f1033,plain,
! [X0] : implies(sF8,implies(X0,sF7)) = implies(X0,sF9),
inference(superposition,[],[f961,f36]) ).
fof(f1159,plain,
implies(z,sF6) = implies(x,truth),
inference(superposition,[],[f1026,f300]) ).
fof(f1211,plain,
implies(z,sF7) = implies(y,truth),
inference(superposition,[],[f1027,f300]) ).
fof(f1270,plain,
! [X0,X1] : implies(X0,implies(implies(X0,X1),X1)) = implies(implies(X1,X0),truth),
inference(superposition,[],[f1011,f4]) ).
fof(f1289,plain,
implies(sF7,sF8) = implies(sF6,truth),
inference(superposition,[],[f1011,f34]) ).
fof(f1307,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),X1) = implies(implies(X0,truth),implies(X0,X1)),
inference(superposition,[],[f4,f1011]) ).
fof(f1334,plain,
! [X0,X1] : implies(X0,X1) = implies(implies(X0,truth),implies(X0,X1)),
inference(forward_demodulation,[],[f1307,f415]) ).
fof(f1348,plain,
! [X0,X1] : truth = implies(implies(X1,X0),truth),
inference(forward_demodulation,[],[f1270,f52]) ).
fof(f1357,plain,
implies(sF1,sF0) = implies(sF3,sF0),
inference(superposition,[],[f415,f116]) ).
fof(f1431,plain,
! [X0] : truth = implies(X0,truth),
inference(superposition,[],[f415,f1348]) ).
fof(f1455,plain,
! [X2,X0,X1] : implies(X2,truth) = implies(implies(X0,X1),implies(X2,truth)),
inference(superposition,[],[f961,f1348]) ).
fof(f1855,plain,
sF6 = implies(implies(x,truth),sF6),
inference(superposition,[],[f1334,f30]) ).
fof(f1857,plain,
sF7 = implies(implies(y,truth),sF7),
inference(superposition,[],[f1334,f32]) ).
fof(f1964,plain,
sF7 = implies(implies(z,sF7),sF7),
inference(forward_demodulation,[],[f1857,f1211]) ).
fof(f1966,plain,
sF6 = implies(implies(z,sF6),sF6),
inference(forward_demodulation,[],[f1855,f1159]) ).
fof(f2092,plain,
! [X2,X3,X0,X1] : implies(X0,implies(implies(implies(X1,implies(X2,X3)),implies(X2,implies(X1,X3))),implies(X2,implies(X1,X3)))) = implies(truth,implies(X0,implies(X1,implies(X2,X3)))),
inference(superposition,[],[f1015,f753]) ).
fof(f2158,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X2,X1)) = implies(implies(X1,X0),implies(X2,X0)),
inference(superposition,[],[f961,f1015]) ).
fof(f2307,plain,
! [X2,X3,X0,X1] : implies(X0,implies(X1,implies(X2,X3))) = implies(X0,implies(implies(implies(X1,implies(X2,X3)),implies(X2,implies(X1,X3))),implies(X2,implies(X1,X3)))),
inference(forward_demodulation,[],[f2092,f1]) ).
fof(f2347,plain,
! [X2,X3,X0,X1] : implies(X0,implies(X1,implies(X2,X3))) = implies(X0,implies(truth,implies(X2,implies(X1,X3)))),
inference(forward_demodulation,[],[f2307,f753]) ).
fof(f2361,plain,
! [X2,X3,X0,X1] : implies(X0,implies(X1,implies(X2,X3))) = implies(X0,implies(X2,implies(X1,X3))),
inference(forward_demodulation,[],[f2347,f1]) ).
fof(f5219,plain,
implies(sF7,sF8) = implies(implies(sF9,sF7),sF8),
inference(superposition,[],[f459,f36]) ).
fof(f5298,plain,
! [X2,X0,X1] : implies(implies(X2,X1),implies(X0,X1)) = implies(implies(implies(X1,X0),X0),implies(implies(X1,X2),X2)),
inference(superposition,[],[f1015,f459]) ).
fof(f5364,plain,
implies(sF7,sF8) = implies(sF8,sF8),
inference(forward_demodulation,[],[f5219,f479]) ).
fof(f5409,plain,
truth = implies(sF7,sF8),
inference(forward_demodulation,[],[f5364,f300]) ).
fof(f6524,plain,
truth = implies(z,sF7),
inference(superposition,[],[f52,f1964]) ).
fof(f6643,plain,
implies(sF6,truth) = implies(z,sF8),
inference(superposition,[],[f1032,f6524]) ).
fof(f6724,plain,
implies(sF7,sF8) = implies(z,sF8),
inference(forward_demodulation,[],[f6643,f1289]) ).
fof(f6735,plain,
truth = implies(z,sF8),
inference(forward_demodulation,[],[f6724,f5409]) ).
fof(f8351,plain,
! [X0,X1] : implies(not(X1),implies(X1,X0)) = implies(implies(implies(not(X1),implies(X1,X0)),implies(not(X0),truth)),implies(not(X0),truth)),
inference(superposition,[],[f178,f1011]) ).
fof(f8484,plain,
! [X0,X1] : implies(not(X0),truth) = implies(not(X1),implies(X1,X0)),
inference(forward_demodulation,[],[f8351,f1455]) ).
fof(f8537,plain,
! [X0,X1] : truth = implies(not(X1),implies(X1,X0)),
inference(forward_demodulation,[],[f8484,f1431]) ).
fof(f8630,plain,
! [X0,X1] : truth = implies(truth,implies(not(not(X0)),implies(X1,X0))),
inference(superposition,[],[f54,f8537]) ).
fof(f8742,plain,
! [X0,X1] : truth = implies(not(not(X0)),implies(X1,X0)),
inference(forward_demodulation,[],[f8630,f1]) ).
fof(f9276,plain,
! [X0] : truth = implies(not(not(X0)),X0),
inference(superposition,[],[f8742,f1]) ).
fof(f9349,plain,
! [X0,X1] : truth = implies(truth,implies(not(not(not(X0))),implies(X0,X1))),
inference(superposition,[],[f54,f8742]) ).
fof(f9361,plain,
! [X0,X1] : truth = implies(implies(X0,X1),implies(not(not(X0)),X1)),
inference(superposition,[],[f1015,f8742]) ).
fof(f9461,plain,
! [X0,X1] : truth = implies(not(not(not(X0))),implies(X0,X1)),
inference(forward_demodulation,[],[f9349,f1]) ).
fof(f9496,plain,
! [X0] : truth = implies(truth,implies(X0,not(not(X0)))),
inference(superposition,[],[f6,f9276]) ).
fof(f9520,plain,
! [X0,X1] : implies(implies(X0,X1),implies(truth,X1)) = implies(implies(implies(implies(X0,X1),implies(truth,X1)),implies(implies(X0,not(not(X0))),not(not(X0)))),implies(implies(X0,not(not(X0))),not(not(X0)))),
inference(superposition,[],[f159,f9276]) ).
fof(f9601,plain,
! [X0,X1] : implies(implies(X0,X1),X1) = implies(implies(implies(implies(X0,X1),X1),implies(implies(X0,not(not(X0))),not(not(X0)))),implies(implies(X0,not(not(X0))),not(not(X0)))),
inference(forward_demodulation,[],[f9520,f1]) ).
fof(f9620,plain,
! [X0] : truth = implies(X0,not(not(X0))),
inference(forward_demodulation,[],[f9496,f1]) ).
fof(f9627,plain,
! [X0,X1] : implies(implies(X0,X1),X1) = implies(implies(implies(not(not(X0)),X0),implies(X1,X0)),implies(implies(X0,not(not(X0))),not(not(X0)))),
inference(forward_demodulation,[],[f9601,f5298]) ).
fof(f9634,plain,
! [X0,X1] : implies(implies(X0,X1),X1) = implies(implies(implies(not(not(X0)),X0),implies(X1,X0)),implies(truth,not(not(X0)))),
inference(forward_demodulation,[],[f9627,f9620]) ).
fof(f9637,plain,
! [X0,X1] : implies(implies(X0,X1),X1) = implies(implies(implies(not(not(X0)),X0),implies(X1,X0)),not(not(X0))),
inference(forward_demodulation,[],[f9634,f1]) ).
fof(f9638,plain,
! [X0,X1] : implies(implies(X0,X1),X1) = implies(implies(truth,implies(X1,X0)),not(not(X0))),
inference(forward_demodulation,[],[f9637,f9276]) ).
fof(f9639,plain,
! [X0,X1] : implies(implies(X0,X1),X1) = implies(implies(X1,X0),not(not(X0))),
inference(forward_demodulation,[],[f9638,f1]) ).
fof(f9668,plain,
! [X0] : implies(truth,not(not(X0))) = implies(implies(implies(truth,not(not(X0))),X0),X0),
inference(superposition,[],[f173,f9620]) ).
fof(f9688,plain,
! [X0,X1] : implies(X0,implies(implies(not(not(X1)),X1),X1)) = implies(truth,implies(X0,not(not(X1)))),
inference(superposition,[],[f1015,f9620]) ).
fof(f9723,plain,
! [X0,X1] : implies(X0,not(not(X1))) = implies(X0,implies(implies(not(not(X1)),X1),X1)),
inference(forward_demodulation,[],[f9688,f1]) ).
fof(f9738,plain,
! [X0] : not(not(X0)) = implies(implies(not(not(X0)),X0),X0),
inference(forward_demodulation,[],[f9668,f1]) ).
fof(f9765,plain,
! [X0,X1] : implies(X0,implies(truth,X1)) = implies(X0,not(not(X1))),
inference(forward_demodulation,[],[f9723,f9276]) ).
fof(f9768,plain,
! [X0] : implies(truth,X0) = not(not(X0)),
inference(forward_demodulation,[],[f9738,f9276]) ).
fof(f9784,plain,
! [X0,X1] : implies(X0,X1) = implies(X0,not(not(X1))),
inference(forward_demodulation,[],[f9765,f1]) ).
fof(f9786,plain,
! [X0] : not(not(X0)) = X0,
inference(forward_demodulation,[],[f9768,f1]) ).
fof(f9800,plain,
x = not(sF0),
inference(superposition,[],[f9786,f18]) ).
fof(f9801,plain,
y = not(sF1),
inference(superposition,[],[f9786,f20]) ).
fof(f9802,plain,
sF3 = not(sF4),
inference(superposition,[],[f9786,f26]) ).
fof(f9807,plain,
! [X0,X1] : truth = implies(implies(not(X1),X0),implies(not(X0),X1)),
inference(superposition,[],[f6,f9786]) ).
fof(f10863,plain,
! [X0,X1] : truth = implies(truth,implies(not(implies(X0,X1)),X0)),
inference(superposition,[],[f9807,f8537]) ).
fof(f10864,plain,
! [X0,X1] : truth = implies(truth,implies(not(implies(X1,X0)),not(X0))),
inference(superposition,[],[f9807,f8742]) ).
fof(f10981,plain,
! [X2,X0,X1] : implies(implies(implies(not(X2),X1),implies(not(X1),X2)),implies(X0,implies(not(X1),X2))) = implies(X0,implies(truth,implies(not(X2),X1))),
inference(superposition,[],[f1015,f9807]) ).
fof(f10996,plain,
! [X2,X0,X1] : implies(X0,implies(not(X2),X1)) = implies(implies(implies(not(X2),X1),implies(not(X1),X2)),implies(X0,implies(not(X1),X2))),
inference(forward_demodulation,[],[f10981,f1]) ).
fof(f11056,plain,
! [X0,X1] : truth = implies(not(implies(X1,X0)),not(X0)),
inference(forward_demodulation,[],[f10864,f1]) ).
fof(f11057,plain,
! [X0,X1] : truth = implies(not(implies(X0,X1)),X0),
inference(forward_demodulation,[],[f10863,f1]) ).
fof(f11061,plain,
! [X2,X0,X1] : implies(X0,implies(not(X2),X1)) = implies(truth,implies(X0,implies(not(X1),X2))),
inference(forward_demodulation,[],[f10996,f9807]) ).
fof(f11081,plain,
! [X2,X0,X1] : implies(X0,implies(not(X2),X1)) = implies(X0,implies(not(X1),X2)),
inference(forward_demodulation,[],[f11061,f1]) ).
fof(f11226,plain,
! [X2,X0,X1] : implies(X2,truth) = implies(not(implies(X0,X1)),implies(X2,X0)),
inference(superposition,[],[f961,f11057]) ).
fof(f11244,plain,
! [X2,X0,X1] : truth = implies(X0,implies(not(implies(implies(X0,X1),X2)),X1)),
inference(superposition,[],[f961,f11057]) ).
fof(f11254,plain,
! [X0] : implies(x,truth) = implies(not(implies(z,X0)),sF6),
inference(superposition,[],[f1026,f11057]) ).
fof(f11261,plain,
! [X0] : implies(z,sF6) = implies(not(implies(z,X0)),sF6),
inference(forward_demodulation,[],[f11254,f1159]) ).
fof(f11277,plain,
! [X2,X0,X1] : truth = implies(not(implies(X0,X1)),implies(X2,X0)),
inference(forward_demodulation,[],[f11226,f1431]) ).
fof(f11396,plain,
truth = implies(not(sF3),not(sF0)),
inference(superposition,[],[f11056,f116]) ).
fof(f11556,plain,
truth = implies(not(sF3),x),
inference(forward_demodulation,[],[f11396,f9800]) ).
fof(f11581,plain,
truth = implies(sF4,x),
inference(forward_demodulation,[],[f11556,f26]) ).
fof(f12253,plain,
! [X0] : truth = implies(not(implies(z,X0)),sF6),
inference(superposition,[],[f11277,f30]) ).
fof(f12428,plain,
truth = implies(z,sF6),
inference(forward_demodulation,[],[f12253,f11261]) ).
fof(f20522,plain,
! [X2,X0,X1] : implies(X1,implies(X0,X2)) = implies(X1,implies(not(X2),not(X0))),
inference(superposition,[],[f11081,f9786]) ).
fof(f20783,plain,
! [X2,X0,X1] : implies(X0,implies(not(X1),X2)) = implies(not(X2),implies(X0,X1)),
inference(superposition,[],[f961,f11081]) ).
fof(f20860,plain,
! [X0,X1] : implies(not(X1),X0) = implies(truth,implies(not(X0),X1)),
inference(superposition,[],[f1,f11081]) ).
fof(f20863,plain,
! [X0,X1] : implies(X0,X1) = implies(implies(implies(X0,X1),implies(not(not(X0)),X1)),implies(not(X1),not(X0))),
inference(superposition,[],[f210,f11081]) ).
fof(f20962,plain,
! [X0,X1] : implies(X0,X1) = implies(truth,implies(not(X1),not(X0))),
inference(forward_demodulation,[],[f20863,f9361]) ).
fof(f20963,plain,
! [X0,X1] : implies(not(X0),X1) = implies(not(X1),X0),
inference(forward_demodulation,[],[f20860,f1]) ).
fof(f21070,plain,
! [X0,X1] : implies(X0,X1) = implies(not(X1),not(X0)),
inference(forward_demodulation,[],[f20962,f1]) ).
fof(f21107,plain,
! [X0,X1] : implies(X0,not(X1)) = implies(X1,not(X0)),
inference(superposition,[],[f21070,f9786]) ).
fof(f21115,plain,
! [X0] : implies(x,X0) = implies(not(X0),sF0),
inference(superposition,[],[f21070,f18]) ).
fof(f21116,plain,
! [X0] : implies(y,X0) = implies(not(X0),sF1),
inference(superposition,[],[f21070,f20]) ).
fof(f21120,plain,
! [X0] : implies(sF4,X0) = implies(not(X0),sF3),
inference(superposition,[],[f21070,f9802]) ).
fof(f21159,plain,
! [X0,X1] : implies(implies(not(X0),not(X1)),not(X1)) = implies(implies(X0,X1),not(X0)),
inference(superposition,[],[f4,f21070]) ).
fof(f21194,plain,
! [X0,X1] : implies(not(X0),not(X1)) = implies(implies(implies(X0,X1),not(X0)),not(X1)),
inference(superposition,[],[f459,f21070]) ).
fof(f21199,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = implies(not(X1),implies(X2,not(X0))),
inference(superposition,[],[f961,f21070]) ).
fof(f21202,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X2,not(X0))) = implies(X2,implies(implies(not(X0),not(X1)),not(X1))),
inference(superposition,[],[f1015,f21070]) ).
fof(f21230,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X2,not(X0))) = implies(X2,implies(implies(X1,X0),not(X1))),
inference(forward_demodulation,[],[f21202,f21070]) ).
fof(f21234,plain,
! [X0,X1] : implies(X1,X0) = implies(implies(implies(X0,X1),not(X0)),not(X1)),
inference(forward_demodulation,[],[f21194,f21070]) ).
fof(f21249,plain,
! [X0,X1] : implies(implies(X0,X1),not(X0)) = implies(implies(X1,X0),not(X1)),
inference(forward_demodulation,[],[f21159,f21070]) ).
fof(f21548,plain,
! [X2,X0,X1] : implies(not(implies(X0,X1)),X2) = implies(X0,implies(not(X2),X1)),
inference(superposition,[],[f961,f20963]) ).
fof(f21964,plain,
! [X0] : not(X0) = implies(X0,not(truth)),
inference(superposition,[],[f1,f21107]) ).
fof(f22439,plain,
! [X2,X0,X1] : implies(not(X0),implies(X1,X2)) = implies(not(X2),implies(X1,X0)),
inference(superposition,[],[f961,f20783]) ).
fof(f23528,plain,
! [X0] : implies(not(X0),sF3) = implies(not(sF1),implies(sF2,X0)),
inference(superposition,[],[f22439,f24]) ).
fof(f23916,plain,
! [X0] : implies(not(X0),sF3) = implies(y,implies(sF2,X0)),
inference(forward_demodulation,[],[f23528,f9801]) ).
fof(f24215,plain,
! [X0] : implies(sF4,X0) = implies(y,implies(sF2,X0)),
inference(forward_demodulation,[],[f23916,f21120]) ).
fof(f24526,plain,
implies(sF4,z) = implies(sF2,sF7),
inference(superposition,[],[f1027,f24215]) ).
fof(f24654,plain,
sF5 = implies(sF2,sF7),
inference(forward_demodulation,[],[f24526,f28]) ).
fof(f24849,plain,
implies(sF0,sF1) = implies(y,x),
inference(superposition,[],[f21116,f18]) ).
fof(f24981,plain,
sF2 = implies(y,x),
inference(forward_demodulation,[],[f24849,f22]) ).
fof(f25043,plain,
! [X0] : implies(X0,sF2) = implies(y,implies(X0,x)),
inference(superposition,[],[f961,f24981]) ).
fof(f25059,plain,
truth = implies(not(sF2),not(x)),
inference(superposition,[],[f11056,f24981]) ).
fof(f25075,plain,
truth = implies(x,sF2),
inference(forward_demodulation,[],[f25059,f21070]) ).
fof(f25130,plain,
implies(sF3,sF0) = implies(x,sF4),
inference(superposition,[],[f21115,f9802]) ).
fof(f25254,plain,
implies(sF1,sF0) = implies(x,sF4),
inference(forward_demodulation,[],[f25130,f1357]) ).
fof(f25893,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),not(implies(X1,X0))) = implies(implies(not(not(X0)),implies(X1,X0)),not(not(not(X0)))),
inference(superposition,[],[f21249,f9639]) ).
fof(f25918,plain,
! [X0,X1] : implies(truth,not(not(not(not(X0))))) = implies(implies(implies(X0,X1),not(not(not(X0)))),not(implies(X0,X1))),
inference(superposition,[],[f21249,f9461]) ).
fof(f26119,plain,
! [X2,X0,X1] : implies(not(X2),implies(implies(X0,X1),not(X0))) = implies(not(not(X1)),implies(implies(X1,X0),X2)),
inference(superposition,[],[f22439,f21249]) ).
fof(f26120,plain,
! [X2,X0,X1] : implies(X1,implies(implies(X1,X0),X2)) = implies(not(X2),implies(implies(X0,X1),not(X0))),
inference(forward_demodulation,[],[f26119,f9786]) ).
fof(f26222,plain,
! [X0,X1] : implies(truth,not(not(not(not(X0))))) = implies(implies(implies(X0,X1),not(X0)),not(implies(X0,X1))),
inference(forward_demodulation,[],[f25918,f9784]) ).
fof(f26246,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),not(implies(X1,X0))) = implies(implies(not(not(X0)),implies(X1,X0)),not(X0)),
inference(forward_demodulation,[],[f25893,f9784]) ).
fof(f26364,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X0,X2)) = implies(X1,implies(implies(X1,X0),X2)),
inference(forward_demodulation,[],[f26120,f21199]) ).
fof(f26437,plain,
! [X0,X1] : not(not(not(not(X0)))) = implies(implies(implies(X0,X1),not(X0)),not(implies(X0,X1))),
inference(forward_demodulation,[],[f26222,f1]) ).
fof(f26452,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),not(implies(X1,X0))) = implies(truth,not(X0)),
inference(forward_demodulation,[],[f26246,f8742]) ).
fof(f26584,plain,
! [X0,X1] : not(not(X0)) = implies(implies(implies(X0,X1),not(X0)),not(implies(X0,X1))),
inference(forward_demodulation,[],[f26437,f9786]) ).
fof(f26597,plain,
! [X0,X1] : not(X0) = implies(implies(implies(X0,X1),X1),not(implies(X1,X0))),
inference(forward_demodulation,[],[f26452,f1]) ).
fof(f26679,plain,
! [X0,X1] : implies(implies(implies(X0,X1),not(X0)),not(implies(X0,X1))) = X0,
inference(forward_demodulation,[],[f26584,f9786]) ).
fof(f27128,plain,
! [X0] : implies(X0,implies(implies(X0,x),z)) = implies(implies(x,X0),sF6),
inference(superposition,[],[f26364,f30]) ).
fof(f27224,plain,
! [X2,X0,X1] : implies(implies(implies(X0,X1),X1),implies(implies(X0,X1),X2)) = implies(implies(X1,implies(implies(X0,X1),X1)),implies(X1,X2)),
inference(superposition,[],[f26364,f415]) ).
fof(f27278,plain,
! [X0,X1] : implies(implies(X1,X0),implies(X0,X1)) = implies(implies(X0,implies(X1,X0)),implies(X0,X1)),
inference(superposition,[],[f26364,f459]) ).
fof(f27394,plain,
! [X2,X0,X1] : implies(X0,implies(implies(X0,X1),X2)) = implies(X1,implies(implies(X1,X0),X2)),
inference(superposition,[],[f961,f26364]) ).
fof(f27720,plain,
! [X0,X1] : implies(implies(X1,truth),implies(X0,X1)) = implies(implies(X1,X0),implies(X0,X1)),
inference(forward_demodulation,[],[f27278,f1011]) ).
fof(f27762,plain,
! [X2,X0,X1] : implies(truth,implies(X1,X2)) = implies(implies(implies(X0,X1),X1),implies(implies(X0,X1),X2)),
inference(forward_demodulation,[],[f27224,f281]) ).
fof(f28017,plain,
! [X0,X1] : implies(truth,implies(X0,X1)) = implies(implies(X1,X0),implies(X0,X1)),
inference(forward_demodulation,[],[f27720,f1431]) ).
fof(f28051,plain,
! [X2,X0,X1] : implies(X1,X2) = implies(implies(implies(X0,X1),X1),implies(implies(X0,X1),X2)),
inference(forward_demodulation,[],[f27762,f1]) ).
fof(f28185,plain,
! [X0,X1] : implies(X0,X1) = implies(implies(X1,X0),implies(X0,X1)),
inference(forward_demodulation,[],[f28017,f1]) ).
fof(f28705,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = implies(implies(X1,X0),implies(X2,implies(X0,X1))),
inference(superposition,[],[f961,f28185]) ).
fof(f29830,plain,
! [X0,X1] : not(not(X1)) = implies(implies(implies(not(X1),implies(X1,X0)),implies(X1,X0)),not(implies(implies(X0,X1),not(X0)))),
inference(superposition,[],[f26597,f21249]) ).
fof(f30145,plain,
! [X0,X1] : not(not(X1)) = implies(implies(truth,implies(X1,X0)),not(implies(implies(X0,X1),not(X0)))),
inference(forward_demodulation,[],[f29830,f8537]) ).
fof(f30426,plain,
! [X0,X1] : not(not(X1)) = implies(implies(X1,X0),not(implies(implies(X0,X1),not(X0)))),
inference(forward_demodulation,[],[f30145,f1]) ).
fof(f30590,plain,
! [X0,X1] : implies(implies(X1,X0),not(implies(implies(X0,X1),not(X0)))) = X1,
inference(forward_demodulation,[],[f30426,f9786]) ).
fof(f30914,plain,
! [X2,X0,X1] : implies(implies(implies(not(implies(X0,X1)),X2),X2),X0) = implies(implies(implies(implies(implies(not(implies(X0,X1)),X2),X2),X0),implies(implies(implies(X0,X1),not(X0)),implies(X2,not(implies(X0,X1))))),implies(implies(implies(X0,X1),not(X0)),implies(X2,not(implies(X0,X1))))),
inference(superposition,[],[f129,f26679]) ).
fof(f30947,plain,
! [X2,X3,X0,X1] : implies(X1,implies(implies(implies(X0,X2),not(X0)),implies(X3,not(implies(X0,X2))))) = implies(X1,implies(X3,X0)),
inference(superposition,[],[f2361,f26679]) ).
fof(f30968,plain,
! [X0,X1] : not(implies(implies(X0,X1),not(X0))) = implies(implies(X0,not(implies(X0,X1))),not(implies(not(implies(X0,X1)),implies(implies(X0,X1),not(X0))))),
inference(superposition,[],[f26597,f26679]) ).
fof(f30977,plain,
! [X0,X1] : not(implies(implies(X0,X1),not(X0))) = implies(implies(X0,not(implies(X0,X1))),not(implies(X0,implies(not(implies(implies(X0,X1),not(X0))),X1)))),
inference(forward_demodulation,[],[f30968,f21548]) ).
fof(f31009,plain,
! [X2,X0,X1] : implies(implies(implies(not(implies(X0,X1)),X2),X2),X0) = implies(implies(implies(implies(implies(not(implies(X0,X1)),X2),X2),X0),implies(implies(implies(X0,X1),not(X0)),implies(X2,not(implies(X0,X1))))),implies(X2,X0)),
inference(forward_demodulation,[],[f30914,f30947]) ).
fof(f31139,plain,
! [X0,X1] : not(implies(implies(X0,X1),not(X0))) = implies(implies(X0,not(implies(X0,X1))),not(truth)),
inference(forward_demodulation,[],[f30977,f11244]) ).
fof(f31157,plain,
! [X2,X0,X1] : implies(implies(implies(not(implies(X0,X1)),X2),X2),X0) = implies(implies(implies(implies(implies(not(implies(X0,X1)),X2),X2),X0),implies(X2,X0)),implies(X2,X0)),
inference(forward_demodulation,[],[f31009,f30947]) ).
fof(f31265,plain,
! [X0,X1] : not(implies(implies(X0,X1),not(X0))) = not(implies(X0,not(implies(X0,X1)))),
inference(forward_demodulation,[],[f31139,f21964]) ).
fof(f31279,plain,
! [X2,X0,X1] : implies(truth,implies(X2,X0)) = implies(implies(implies(not(implies(X0,X1)),X2),X2),X0),
inference(forward_demodulation,[],[f31157,f366]) ).
fof(f31317,plain,
! [X2,X0,X1] : implies(truth,implies(X2,X0)) = implies(implies(implies(X0,implies(not(X2),X1)),X2),X0),
inference(forward_demodulation,[],[f31279,f21548]) ).
fof(f31326,plain,
! [X2,X0,X1] : implies(X2,X0) = implies(implies(implies(X0,implies(not(X2),X1)),X2),X0),
inference(forward_demodulation,[],[f31317,f1]) ).
fof(f34919,plain,
! [X0] : implies(X0,truth) = implies(x,implies(X0,sF2)),
inference(superposition,[],[f961,f25075]) ).
fof(f34984,plain,
! [X0] : truth = implies(x,implies(X0,sF2)),
inference(forward_demodulation,[],[f34919,f1431]) ).
fof(f39813,plain,
implies(implies(z,x),sF2) = implies(y,implies(sF6,z)),
inference(superposition,[],[f25043,f72]) ).
fof(f40009,plain,
implies(sF6,sF7) = implies(implies(z,x),sF2),
inference(forward_demodulation,[],[f39813,f1027]) ).
fof(f40043,plain,
sF8 = implies(implies(z,x),sF2),
inference(forward_demodulation,[],[f40009,f34]) ).
fof(f40774,plain,
implies(implies(x,sF4),sF6) = implies(implies(sF4,x),sF5),
inference(superposition,[],[f1031,f27128]) ).
fof(f40779,plain,
implies(truth,sF5) = implies(implies(x,sF4),sF6),
inference(forward_demodulation,[],[f40774,f11581]) ).
fof(f40870,plain,
implies(truth,sF5) = implies(implies(sF1,sF0),sF6),
inference(forward_demodulation,[],[f40779,f25254]) ).
fof(f40935,plain,
sF5 = implies(implies(sF1,sF0),sF6),
inference(forward_demodulation,[],[f40870,f1]) ).
fof(f47859,plain,
! [X0] : implies(implies(implies(sF6,X0),X0),sF5) = implies(implies(implies(implies(implies(sF6,X0),X0),sF5),implies(implies(sF1,sF0),implies(X0,sF6))),implies(implies(sF1,sF0),implies(X0,sF6))),
inference(superposition,[],[f129,f40935]) ).
fof(f47884,plain,
! [X0] : implies(X0,sF5) = implies(implies(sF1,sF0),implies(X0,sF6)),
inference(superposition,[],[f961,f40935]) ).
fof(f47888,plain,
! [X0] : implies(implies(sF1,sF0),implies(X0,sF6)) = implies(implies(implies(X0,sF6),sF6),sF5),
inference(superposition,[],[f1016,f40935]) ).
fof(f47892,plain,
! [X0,X1] : implies(X0,implies(X1,sF5)) = implies(X0,implies(implies(sF1,sF0),implies(X1,sF6))),
inference(superposition,[],[f2361,f40935]) ).
fof(f47953,plain,
! [X0] : implies(implies(implies(sF6,X0),X0),sF5) = implies(implies(implies(implies(implies(sF6,X0),X0),sF5),implies(implies(sF1,sF0),implies(X0,sF6))),implies(X0,sF5)),
inference(forward_demodulation,[],[f47859,f47892]) ).
fof(f47974,plain,
! [X0] : implies(implies(implies(sF6,X0),X0),sF5) = implies(implies(implies(implies(implies(sF6,X0),X0),sF5),implies(X0,sF5)),implies(X0,sF5)),
inference(forward_demodulation,[],[f47953,f47892]) ).
fof(f47988,plain,
! [X0] : implies(truth,implies(X0,sF5)) = implies(implies(implies(sF6,X0),X0),sF5),
inference(forward_demodulation,[],[f47974,f366]) ).
fof(f47993,plain,
! [X0] : implies(X0,sF5) = implies(implies(implies(sF6,X0),X0),sF5),
inference(forward_demodulation,[],[f47988,f1]) ).
fof(f53165,plain,
! [X2,X0,X1] : implies(X0,implies(not(X1),X2)) = implies(implies(implies(X0,implies(not(X1),X2)),X1),X1),
inference(superposition,[],[f415,f21548]) ).
fof(f55354,plain,
! [X2,X0,X1] : implies(X2,implies(implies(not(X0),implies(implies(X1,X0),not(X1))),not(not(X0)))) = implies(implies(X0,X1),implies(X2,not(implies(implies(X1,X0),not(X1))))),
inference(superposition,[],[f21230,f21234]) ).
fof(f55409,plain,
! [X2,X0,X1] : implies(X2,implies(implies(not(X0),implies(implies(X1,X0),not(X1))),not(not(X0)))) = implies(implies(X0,X1),implies(X2,not(implies(X1,not(implies(X1,X0)))))),
inference(forward_demodulation,[],[f55354,f31265]) ).
fof(f55693,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X2,not(implies(X1,not(implies(X1,X0)))))) = implies(X2,implies(implies(not(X0),implies(implies(X1,X0),not(X1))),X0)),
inference(forward_demodulation,[],[f55409,f9784]) ).
fof(f55848,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X2,not(implies(X1,not(implies(X1,X0)))))) = implies(X2,implies(implies(implies(X1,X0),implies(X1,X0)),X0)),
inference(forward_demodulation,[],[f55693,f21199]) ).
fof(f55938,plain,
! [X2,X0,X1] : implies(X2,implies(truth,X0)) = implies(implies(X0,X1),implies(X2,not(implies(X1,not(implies(X1,X0)))))),
inference(forward_demodulation,[],[f55848,f300]) ).
fof(f55981,plain,
! [X2,X0,X1] : implies(X2,X0) = implies(implies(X0,X1),implies(X2,not(implies(X1,not(implies(X1,X0)))))),
inference(forward_demodulation,[],[f55938,f1]) ).
fof(f64208,plain,
! [X2,X0,X1] : implies(X0,X1) = implies(implies(implies(implies(X1,implies(not(X0),X2)),X0),X0),implies(X0,X1)),
inference(superposition,[],[f28051,f31326]) ).
fof(f64425,plain,
! [X2,X0,X1] : implies(X0,X1) = implies(implies(X1,implies(not(X0),X2)),implies(X0,X1)),
inference(forward_demodulation,[],[f64208,f53165]) ).
fof(f64716,plain,
! [X2,X0,X1] : implies(X1,X2) = implies(implies(X2,implies(X0,X1)),implies(X1,X2)),
inference(superposition,[],[f64425,f21070]) ).
fof(f65110,plain,
! [X2,X0,X1] : implies(X0,X1) = implies(X0,implies(implies(X1,implies(not(X0),X2)),X1)),
inference(superposition,[],[f961,f64425]) ).
fof(f76684,plain,
! [X2,X0,X1] : implies(X2,X1) = implies(implies(X0,implies(X1,X2)),implies(X2,X1)),
inference(superposition,[],[f64716,f961]) ).
fof(f78479,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = implies(implies(X1,X0),implies(implies(implies(X1,X0),X2),implies(X0,X1))),
inference(superposition,[],[f27394,f76684]) ).
fof(f78707,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = implies(implies(implies(X1,X0),X2),implies(X0,X1)),
inference(forward_demodulation,[],[f78479,f28705]) ).
fof(f113321,plain,
implies(sF8,sF5) = implies(sF2,sF9),
inference(superposition,[],[f1033,f24654]) ).
fof(f116073,plain,
! [X2,X0,X1] : implies(X0,implies(X2,X1)) = implies(X0,implies(implies(not(X0),implies(implies(X1,X2),not(X1))),implies(X2,X1))),
inference(superposition,[],[f65110,f21230]) ).
fof(f116580,plain,
! [X2,X0,X1] : implies(X0,implies(X2,X1)) = implies(X0,implies(implies(implies(X1,X2),implies(X1,X0)),implies(X2,X1))),
inference(forward_demodulation,[],[f116073,f21199]) ).
fof(f116722,plain,
! [X2,X0,X1] : implies(X0,implies(X2,X1)) = implies(X0,implies(implies(X1,X0),implies(X2,X1))),
inference(forward_demodulation,[],[f116580,f78707]) ).
fof(f133530,plain,
! [X2,X0,X1] : implies(implies(implies(not(implies(implies(X1,X0),not(X1))),X2),X2),X0) = implies(implies(implies(implies(implies(not(implies(implies(X1,X0),not(X1))),X2),X2),X0),implies(implies(X0,X1),implies(X2,not(implies(implies(X1,X0),not(X1)))))),implies(implies(X0,X1),implies(X2,not(implies(implies(X1,X0),not(X1)))))),
inference(superposition,[],[f129,f30590]) ).
fof(f133633,plain,
! [X2,X0,X1] : implies(X1,X0) = implies(X1,implies(implies(not(implies(implies(X2,X0),not(X2))),X1),X0)),
inference(superposition,[],[f116722,f30590]) ).
fof(f133634,plain,
! [X2,X0,X1] : implies(X1,X0) = implies(X1,implies(implies(implies(X2,X0),implies(not(X1),not(X2))),X0)),
inference(forward_demodulation,[],[f133633,f21548]) ).
fof(f133722,plain,
! [X2,X0,X1] : implies(implies(implies(not(implies(X1,not(implies(X1,X0)))),X2),X2),X0) = implies(implies(implies(implies(implies(not(implies(X1,not(implies(X1,X0)))),X2),X2),X0),implies(implies(X0,X1),implies(X2,not(implies(X1,not(implies(X1,X0))))))),implies(implies(X0,X1),implies(X2,not(implies(X1,not(implies(X1,X0))))))),
inference(forward_demodulation,[],[f133530,f31265]) ).
fof(f134415,plain,
! [X2,X0,X1] : implies(X1,X0) = implies(X1,implies(implies(implies(X2,X0),implies(X2,X1)),X0)),
inference(forward_demodulation,[],[f133634,f20522]) ).
fof(f134481,plain,
! [X2,X0,X1] : implies(implies(implies(not(implies(X1,not(implies(X1,X0)))),X2),X2),X0) = implies(implies(implies(implies(implies(not(implies(X1,not(implies(X1,X0)))),X2),X2),X0),implies(X2,X0)),implies(X2,X0)),
inference(forward_demodulation,[],[f133722,f55981]) ).
fof(f134977,plain,
! [X2,X0,X1] : implies(truth,implies(X2,X0)) = implies(implies(implies(not(implies(X1,not(implies(X1,X0)))),X2),X2),X0),
inference(forward_demodulation,[],[f134481,f366]) ).
fof(f135327,plain,
! [X2,X0,X1] : implies(truth,implies(X2,X0)) = implies(implies(implies(X1,implies(not(X2),not(implies(X1,X0)))),X2),X0),
inference(forward_demodulation,[],[f134977,f21548]) ).
fof(f135544,plain,
! [X2,X0,X1] : implies(truth,implies(X2,X0)) = implies(implies(implies(X1,implies(implies(X1,X0),X2)),X2),X0),
inference(forward_demodulation,[],[f135327,f20522]) ).
fof(f135667,plain,
! [X2,X0,X1] : implies(X2,X0) = implies(implies(implies(X1,implies(implies(X1,X0),X2)),X2),X0),
inference(forward_demodulation,[],[f135544,f1]) ).
fof(f135991,plain,
! [X0] : implies(X0,z) = implies(implies(implies(y,implies(sF7,X0)),X0),z),
inference(superposition,[],[f135667,f32]) ).
fof(f140134,plain,
implies(implies(x,implies(y,implies(sF7,x))),sF6) = implies(implies(y,implies(sF7,x)),implies(x,z)),
inference(superposition,[],[f27128,f135991]) ).
fof(f140387,plain,
implies(implies(x,implies(y,implies(sF7,x))),sF6) = implies(implies(y,implies(sF7,x)),sF6),
inference(forward_demodulation,[],[f140134,f30]) ).
fof(f140479,plain,
implies(implies(x,implies(sF7,sF2)),sF6) = implies(implies(sF7,sF2),sF6),
inference(forward_demodulation,[],[f140387,f25043]) ).
fof(f140536,plain,
implies(truth,sF6) = implies(implies(sF7,sF2),sF6),
inference(forward_demodulation,[],[f140479,f34984]) ).
fof(f140562,plain,
sF6 = implies(implies(sF7,sF2),sF6),
inference(forward_demodulation,[],[f140536,f1]) ).
fof(f141125,plain,
implies(sF6,sF2) = implies(implies(implies(sF7,sF6),sF6),sF2),
inference(superposition,[],[f135667,f140562]) ).
fof(f141331,plain,
implies(sF6,sF2) = implies(sF9,sF2),
inference(forward_demodulation,[],[f141125,f108]) ).
fof(f142987,plain,
! [X0] : implies(X0,sF8) = implies(X0,implies(implies(truth,implies(z,X0)),sF8)),
inference(superposition,[],[f134415,f6735]) ).
fof(f144086,plain,
! [X0] : implies(X0,sF8) = implies(X0,implies(implies(z,X0),sF8)),
inference(forward_demodulation,[],[f142987,f1]) ).
fof(f174361,plain,
implies(sF2,implies(x,z)) = implies(sF8,implies(x,z)),
inference(superposition,[],[f78707,f40043]) ).
fof(f174380,plain,
implies(sF6,implies(sF0,sF1)) = implies(sF5,implies(sF0,sF1)),
inference(superposition,[],[f78707,f40935]) ).
fof(f175574,plain,
implies(sF5,sF2) = implies(sF6,sF2),
inference(forward_demodulation,[],[f174380,f22]) ).
fof(f175593,plain,
implies(sF8,sF6) = implies(sF2,sF6),
inference(forward_demodulation,[],[f174361,f30]) ).
fof(f176854,plain,
sF5 = implies(implies(sF6,sF2),not(implies(implies(sF2,sF5),not(sF2)))),
inference(superposition,[],[f30590,f175574]) ).
fof(f176902,plain,
sF5 = implies(implies(sF6,sF2),not(implies(sF2,not(implies(sF2,sF5))))),
inference(forward_demodulation,[],[f176854,f31265]) ).
fof(f299119,plain,
! [X0] : implies(implies(sF6,sF8),implies(X0,sF8)) = implies(implies(sF2,sF6),implies(X0,sF6)),
inference(superposition,[],[f2158,f175593]) ).
fof(f324179,plain,
implies(implies(implies(z,sF6),sF8),sF5) = implies(implies(implies(sF6,sF8),implies(implies(z,sF6),sF8)),sF5),
inference(superposition,[],[f47993,f144086]) ).
fof(f324205,plain,
implies(implies(implies(z,sF6),sF8),sF5) = implies(implies(implies(sF2,sF6),implies(implies(z,sF6),sF6)),sF5),
inference(forward_demodulation,[],[f324179,f299119]) ).
fof(f324398,plain,
implies(implies(implies(z,sF6),sF8),sF5) = implies(implies(implies(sF2,sF6),sF6),sF5),
inference(forward_demodulation,[],[f324205,f1966]) ).
fof(f324501,plain,
implies(implies(implies(z,sF6),sF8),sF5) = implies(implies(sF1,sF0),implies(sF2,sF6)),
inference(forward_demodulation,[],[f324398,f47888]) ).
fof(f324534,plain,
implies(sF2,sF5) = implies(implies(implies(z,sF6),sF8),sF5),
inference(forward_demodulation,[],[f324501,f47884]) ).
fof(f324555,plain,
implies(sF2,sF5) = implies(implies(truth,sF8),sF5),
inference(forward_demodulation,[],[f324534,f12428]) ).
fof(f324560,plain,
implies(sF2,sF5) = implies(sF8,sF5),
inference(forward_demodulation,[],[f324555,f1]) ).
fof(f324561,plain,
implies(sF2,sF5) = implies(sF2,sF9),
inference(forward_demodulation,[],[f324560,f113321]) ).
fof(f324703,plain,
sF9 = implies(implies(sF9,sF2),not(implies(implies(sF2,sF5),not(sF2)))),
inference(superposition,[],[f30590,f324561]) ).
fof(f324801,plain,
sF9 = implies(implies(sF9,sF2),not(implies(sF2,not(implies(sF2,sF5))))),
inference(forward_demodulation,[],[f324703,f31265]) ).
fof(f324884,plain,
sF9 = implies(implies(sF6,sF2),not(implies(sF2,not(implies(sF2,sF5))))),
inference(forward_demodulation,[],[f324801,f141331]) ).
fof(f324930,plain,
sF5 = sF9,
inference(forward_demodulation,[],[f324884,f176902]) ).
fof(f324960,plain,
$false,
inference(forward_subsumption_resolution,[],[f324930,f37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL150-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 % Computer : n006.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sun Sep 27 15:22:55 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.48 Running first-order theorem proving
% 0.15/0.48 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.47/3.79 % (3092155)Input is clausal, will run a generic CNF schedule.
% 18.47/3.79 % (3092165)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3786978472:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.47/3.79 % (3092164)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2993825853:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.47/3.79 % (3092164)Instruction limit reached!
% 18.47/3.79 % (3092164)------------------------------
% 18.47/3.79 % (3092164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/3.79 % (3092164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/3.79 % (3092164)CaDiCaL version: 2.1.3
% 18.47/3.79 % (3092164)Termination reason: Instruction limit
% 18.47/3.79 % (3092164)Termination phase: Saturation
% 18.47/3.79 % (3092164)Time elapsed: 0.077 s
% 18.47/3.79 % (3092164)Peak memory usage: 89 MB
% 18.47/3.79 % (3092164)Instructions burned: 114 (million)
% 18.47/3.79 % (3092165)Instruction limit reached!
% 18.47/3.79 % (3092165)------------------------------
% 18.47/3.79 % (3092165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/3.79 % (3092165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/3.79 % (3092165)CaDiCaL version: 2.1.3
% 18.47/3.79 % (3092165)Termination reason: Instruction limit
% 18.47/3.79 % (3092165)Termination phase: Saturation
% 18.47/3.79 % (3092165)Time elapsed: 0.092 s
% 18.47/3.79 % (3092165)Peak memory usage: 89 MB
% 18.47/3.79 % (3092165)Instructions burned: 180 (million)
% 18.47/3.79 % (3092162)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1798074338:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.47/3.79 % (3092166)dis-21_1_sil=8000:lcm=predicate:random_seed=1072053143: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)
% 18.47/3.79 % (3092163)lrs+10_1_sil=8000:sp=occurrence:random_seed=271171232:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.47/3.79 % (3092160)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=1397230585:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.47/3.79 % (3092161)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3423687424:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.47/3.79 % (3092166)Refutation not found, incomplete strategy
% 18.47/3.79 % (3092166)------------------------------
% 18.47/3.79 % (3092166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/3.79 % (3092166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/3.79 % (3092166)CaDiCaL version: 2.1.3
% 18.47/3.79 % (3092166)Termination reason: Refutation not found, incomplete strategy
% 18.47/3.79 % (3092166)Time elapsed: 0.002 s
% 18.47/3.79 % (3092166)Peak memory usage: 88 MB
% 18.47/3.79 % (3092163)Instruction limit reached!
% 18.47/3.79 % (3092163)------------------------------
% 18.47/3.79 % (3092163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/3.79 % (3092163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/3.79 % (3092163)CaDiCaL version: 2.1.3
% 18.47/3.79 % (3092163)Termination reason: Instruction limit
% 18.47/3.79 % (3092163)Termination phase: Saturation
% 18.47/3.79 % (3092163)Time elapsed: 0.108 s
% 18.47/3.79 % (3092163)Peak memory usage: 89 MB
% 18.47/3.79 % (3092163)Instructions burned: 107 (million)
% 18.47/3.79 % (3092169)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=289109163:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 18.47/3.79 % (3092169)Refutation not found, incomplete strategy
% 18.47/3.79 % (3092169)------------------------------
% 18.47/3.79 % (3092169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/3.79 % (3092169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/3.79 % (3092169)CaDiCaL version: 2.1.3
% 18.47/3.79 % (3092169)Termination reason: Refutation not found, incomplete strategy
% 18.47/3.79 % (3092169)Time elapsed: 0.002 s
% 18.47/3.79 % (3092169)Peak memory usage: 88 MB
% 18.47/3.79 % (3092169)Instructions burned: 1 (million)
% 18.47/3.79 % (3092170)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=139954520: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)
% 38.07/6.47 % (3092170)Refutation not found, incomplete strategy
% 38.07/6.47 % (3092170)------------------------------
% 38.07/6.47 % (3092170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.07/6.47 % (3092170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.07/6.47 % (3092170)CaDiCaL version: 2.1.3
% 38.07/6.47 % (3092170)Termination reason: Refutation not found, incomplete strategy
% 38.07/6.47 % (3092170)Time elapsed: 0.002 s
% 38.07/6.47 % (3092170)Peak memory usage: 88 MB
% 38.07/6.47 % (3092170)Instructions burned: 1 (million)
% 38.07/6.47 % (3092166)------------------------------
% 38.07/6.47 % (3092166)------------------------------
% 38.07/6.47 % (3092176)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=190837232:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 38.07/6.47 % (3092169)------------------------------
% 38.07/6.47 % (3092169)------------------------------
% 38.07/6.47 % (3092170)------------------------------
% 38.07/6.47 % (3092170)------------------------------
% 38.07/6.47 % (3092176)Instruction limit reached!
% 38.07/6.47 % (3092176)------------------------------
% 38.07/6.47 % (3092176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.07/6.47 % (3092176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.07/6.47 % (3092176)CaDiCaL version: 2.1.3
% 38.07/6.47 % (3092176)Termination reason: Instruction limit
% 38.07/6.47 % (3092176)Termination phase: Saturation
% 38.07/6.47 % (3092176)Time elapsed: 0.235 s
% 38.07/6.47 % (3092176)Peak memory usage: 91 MB
% 38.07/6.47 % (3092176)Instructions burned: 219 (million)
% 38.07/6.47 % (3092179)lrs+10_64_to=lpo:sil=8000:random_seed=1911435681:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 38.07/6.47 % (3092181)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1214409980:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 38.07/6.47 % (3092179)Instruction limit reached!
% 38.07/6.47 % (3092179)------------------------------
% 38.07/6.47 % (3092179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.07/6.47 % (3092179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.07/6.47 % (3092179)CaDiCaL version: 2.1.3
% 38.07/6.47 % (3092179)Termination reason: Instruction limit
% 38.07/6.47 % (3092179)Termination phase: Saturation
% 38.07/6.47 % (3092179)Time elapsed: 0.133 s
% 38.07/6.47 % (3092179)Peak memory usage: 89 MB
% 38.07/6.47 % (3092179)Instructions burned: 126 (million)
% 38.07/6.47 % (3092182)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2194227359:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 38.07/6.47 % (3092181)Instruction limit reached!
% 38.07/6.47 % (3092181)------------------------------
% 38.07/6.47 % (3092181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.07/6.47 % (3092181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.07/6.47 % (3092181)CaDiCaL version: 2.1.3
% 38.07/6.47 % (3092181)Termination reason: Instruction limit
% 38.07/6.47 % (3092181)Termination phase: Saturation
% 38.07/6.47 % (3092181)Time elapsed: 0.112 s
% 38.07/6.47 % (3092181)Peak memory usage: 90 MB
% 38.07/6.47 % (3092181)Instructions burned: 194 (million)
% 38.07/6.47 % (3092183)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=507643695:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 38.07/6.47 % (3092182)Instruction limit reached!
% 38.07/6.47 % (3092182)------------------------------
% 38.07/6.47 % (3092182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.07/6.47 % (3092182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.07/6.47 % (3092182)CaDiCaL version: 2.1.3
% 38.07/6.47 % (3092182)Termination reason: Instruction limit
% 38.07/6.47 % (3092182)Termination phase: Saturation
% 38.07/6.47 % (3092182)Time elapsed: 0.152 s
% 38.07/6.47 % (3092182)Peak memory usage: 91 MB
% 38.07/6.47 % (3092182)Instructions burned: 158 (million)
% 38.07/6.47 % (3092186)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=2396605213:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 38.07/6.47 % (3092188)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=895662603:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 61.97/9.81 % (3092188)Refutation not found, incomplete strategy
% 61.97/9.81 % (3092188)------------------------------
% 61.97/9.81 % (3092188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.97/9.81 % (3092188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.97/9.81 % (3092188)CaDiCaL version: 2.1.3
% 61.97/9.81 % (3092188)Termination reason: Refutation not found, incomplete strategy
% 61.97/9.81 % (3092188)Time elapsed: 0.002 s
% 61.97/9.81 % (3092188)Peak memory usage: 88 MB
% 61.97/9.81 % (3092186)Instruction limit reached!
% 61.97/9.81 % (3092186)------------------------------
% 61.97/9.81 % (3092186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.97/9.81 % (3092186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.97/9.81 % (3092186)CaDiCaL version: 2.1.3
% 61.97/9.81 % (3092186)Termination reason: Instruction limit
% 61.97/9.81 % (3092186)Termination phase: Saturation
% 61.97/9.81 % (3092186)Time elapsed: 0.108 s
% 61.97/9.81 % (3092186)Peak memory usage: 88 MB
% 61.97/9.81 % (3092186)Instructions burned: 107 (million)
% 61.97/9.81 % (3092190)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2511375785:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 61.97/9.81 % (3092190)Instruction limit reached!
% 61.97/9.81 % (3092190)------------------------------
% 61.97/9.81 % (3092190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.97/9.81 % (3092190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.97/9.81 % (3092190)CaDiCaL version: 2.1.3
% 61.97/9.81 % (3092190)Termination reason: Instruction limit
% 61.97/9.81 % (3092190)Termination phase: Saturation
% 61.97/9.81 % (3092190)Time elapsed: 0.224 s
% 61.97/9.81 % (3092190)Peak memory usage: 90 MB
% 61.97/9.81 % (3092190)Instructions burned: 242 (million)
% 61.97/9.81 % (3092188)------------------------------
% 61.97/9.81 % (3092188)------------------------------
% 61.97/9.81 % (3092193)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2715427722:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 61.97/9.81 % (3092195)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2941961243:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 61.97/9.81 % (3092197)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=155561558:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi)
% 61.97/9.81 % (3092195)Instruction limit reached!
% 61.97/9.81 % (3092195)------------------------------
% 61.97/9.81 % (3092195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.97/9.81 % (3092195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.97/9.81 % (3092195)CaDiCaL version: 2.1.3
% 61.97/9.81 % (3092195)Termination reason: Instruction limit
% 61.97/9.81 % (3092195)Termination phase: Saturation
% 61.97/9.81 % (3092195)Time elapsed: 0.133 s
% 61.97/9.81 % (3092195)Peak memory usage: 89 MB
% 61.97/9.81 % (3092195)Instructions burned: 135 (million)
% 61.97/9.81 % (3092200)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1358976536:i=191:fgj=on:bd=all_2978 on theBenchmark for (2978ds/191Mi)
% 61.97/9.81 % (3092197)Instruction limit reached!
% 61.97/9.81 % (3092197)------------------------------
% 61.97/9.81 % (3092197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.97/9.81 % (3092197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.97/9.81 % (3092197)CaDiCaL version: 2.1.3
% 61.97/9.81 % (3092197)Termination reason: Instruction limit
% 61.97/9.81 % (3092197)Termination phase: Saturation
% 61.97/9.81 % (3092197)Time elapsed: 0.477 s
% 61.97/9.81 % (3092197)Peak memory usage: 94 MB
% 61.97/9.81 % (3092197)Instructions burned: 499 (million)
% 61.97/9.81 % (3092200)Instruction limit reached!
% 61.97/9.81 % (3092200)------------------------------
% 61.97/9.81 % (3092200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.97/9.81 % (3092200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.97/9.81 % (3092200)CaDiCaL version: 2.1.3
% 61.97/9.81 % (3092200)Termination reason: Instruction limit
% 61.97/9.81 % (3092200)Termination phase: Saturation
% 61.97/9.81 % (3092200)Time elapsed: 0.213 s
% 61.97/9.81 % (3092200)Peak memory usage: 92 MB
% 61.97/9.81 % (3092200)Instructions burned: 191 (million)
% 96.33/14.67 % (3092202)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3570143889:i=264:kws=precedence:fsr=off_2974 on theBenchmark for (2974ds/264Mi)
% 96.33/14.67 % (3092203)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=983742913:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi)
% 96.33/14.67 % (3092202)Instruction limit reached!
% 96.33/14.67 % (3092202)------------------------------
% 96.33/14.67 % (3092202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.33/14.67 % (3092202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.33/14.67 % (3092202)CaDiCaL version: 2.1.3
% 96.33/14.67 % (3092202)Termination reason: Instruction limit
% 96.33/14.67 % (3092202)Termination phase: Saturation
% 96.33/14.67 % (3092202)Time elapsed: 0.270 s
% 96.33/14.67 % (3092202)Peak memory usage: 93 MB
% 96.33/14.67 % (3092202)Instructions burned: 264 (million)
% 96.33/14.67 % (3092203)Instruction limit reached!
% 96.33/14.67 % (3092203)------------------------------
% 96.33/14.67 % (3092203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.33/14.67 % (3092203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.33/14.67 % (3092203)CaDiCaL version: 2.1.3
% 96.33/14.67 % (3092203)Termination reason: Instruction limit
% 96.33/14.67 % (3092203)Termination phase: Saturation
% 96.33/14.67 % (3092203)Time elapsed: 0.161 s
% 96.33/14.67 % (3092203)Peak memory usage: 89 MB
% 96.33/14.67 % (3092203)Instructions burned: 157 (million)
% 96.33/14.67 % (3092206)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=3987556340:i=3256:kws=precedence:bd=preordered:av=off_2968 on theBenchmark for (2968ds/3256Mi)
% 96.33/14.67 % (3092207)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2657735274:i=537:av=off:ss=included_2968 on theBenchmark for (2968ds/537Mi)
% 96.33/14.67 % (3092207)Instruction limit reached!
% 96.33/14.67 % (3092207)------------------------------
% 96.33/14.67 % (3092207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.33/14.67 % (3092207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.33/14.67 % (3092207)CaDiCaL version: 2.1.3
% 96.33/14.67 % (3092207)Termination reason: Instruction limit
% 96.33/14.67 % (3092207)Termination phase: Saturation
% 96.33/14.67 % (3092207)Time elapsed: 0.502 s
% 96.33/14.67 % (3092207)Peak memory usage: 92 MB
% 96.33/14.67 % (3092207)Instructions burned: 538 (million)
% 96.33/14.67 % (3092210)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1958643748:i=180:bd=preordered:av=off_2960 on theBenchmark for (2960ds/180Mi)
% 96.33/14.67 % (3092210)Instruction limit reached!
% 96.33/14.67 % (3092210)------------------------------
% 96.33/14.67 % (3092210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.33/14.67 % (3092210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.33/14.67 % (3092210)CaDiCaL version: 2.1.3
% 96.33/14.67 % (3092210)Termination reason: Instruction limit
% 96.33/14.67 % (3092210)Termination phase: Saturation
% 96.33/14.67 % (3092210)Time elapsed: 0.182 s
% 96.33/14.67 % (3092210)Peak memory usage: 89 MB
% 96.33/14.67 % (3092210)Instructions burned: 181 (million)
% 96.33/14.67 % (3092183)Instruction limit reached!
% 96.33/14.67 % (3092183)------------------------------
% 96.33/14.67 % (3092183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.33/14.67 % (3092183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.33/14.67 % (3092183)CaDiCaL version: 2.1.3
% 96.33/14.67 % (3092183)Termination reason: Instruction limit
% 96.33/14.67 % (3092183)Termination phase: Saturation
% 96.33/14.67 % (3092183)Time elapsed: 3.426 s
% 96.33/14.67 % (3092183)Peak memory usage: 151 MB
% 96.33/14.67 % (3092183)Instructions burned: 3394 (million)
% 96.33/14.67 % (3092212)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=2088721908:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2955 on theBenchmark for (2955ds/10307Mi)
% 96.33/14.67 % (3092213)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=620552256:i=412:gtgl=4:gtg=exists_all_2953 on theBenchmark for (2953ds/412Mi)
% 96.33/14.67 % (3092213)Instruction limit reached!
% 96.33/14.67 % (3092213)------------------------------
% 96.33/14.67 % (3092213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.70/17.74 % (3092213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.70/17.74 % (3092213)CaDiCaL version: 2.1.3
% 117.70/17.74 % (3092213)Termination reason: Instruction limit
% 117.70/17.74 % (3092213)Termination phase: Saturation
% 117.70/17.74 % (3092213)Time elapsed: 0.420 s
% 117.70/17.74 % (3092213)Peak memory usage: 96 MB
% 117.70/17.74 % (3092213)Instructions burned: 412 (million)
% 117.70/17.74 % (3092216)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=473550133:s2pl=no:i=8478:s2at=4:nm=6_2946 on theBenchmark for (2946ds/8478Mi)
% 117.70/17.74 % (3092206)Instruction limit reached!
% 117.70/17.74 % (3092206)------------------------------
% 117.70/17.74 % (3092206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.70/17.74 % (3092206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.70/17.74 % (3092206)CaDiCaL version: 2.1.3
% 117.70/17.74 % (3092206)Termination reason: Instruction limit
% 117.70/17.74 % (3092206)Termination phase: Saturation
% 117.70/17.74 % (3092206)Time elapsed: 3.353 s
% 117.70/17.74 % (3092206)Peak memory usage: 149 MB
% 117.70/17.74 % (3092206)Instructions burned: 3256 (million)
% 117.70/17.74 % (3092193)Instruction limit reached!
% 117.70/17.74 % (3092193)------------------------------
% 117.70/17.74 % (3092193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.70/17.74 % (3092193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.70/17.74 % (3092193)CaDiCaL version: 2.1.3
% 117.70/17.74 % (3092193)Termination reason: Instruction limit
% 117.70/17.74 % (3092193)Termination phase: Saturation
% 117.70/17.74 % (3092193)Time elapsed: 5.204 s
% 117.70/17.74 % (3092193)Peak memory usage: 169 MB
% 117.70/17.74 % (3092193)Instructions burned: 5208 (million)
% 117.70/17.74 % (3092218)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=4192669485:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2932 on theBenchmark for (2932ds/303Mi)
% 117.70/17.74 % (3092218)Refutation not found, incomplete strategy
% 117.70/17.74 % (3092218)------------------------------
% 117.70/17.74 % (3092218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.70/17.74 % (3092218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.70/17.74 % (3092218)CaDiCaL version: 2.1.3
% 117.70/17.74 % (3092218)Termination reason: Refutation not found, incomplete strategy
% 117.70/17.74 % (3092218)Time elapsed: 0.002 s
% 117.70/17.74 % (3092218)Peak memory usage: 88 MB
% 117.70/17.74 % (3092219)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1514189465:st=4:i=720:sd=3:fsr=off:ss=axioms_2929 on theBenchmark for (2929ds/720Mi)
% 117.70/17.74 % (3092219)Refutation not found, incomplete strategy
% 117.70/17.74 % (3092219)------------------------------
% 117.70/17.74 % (3092219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.70/17.74 % (3092219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.70/17.74 % (3092219)CaDiCaL version: 2.1.3
% 117.70/17.74 % (3092219)Termination reason: Refutation not found, incomplete strategy
% 117.70/17.74 % (3092219)Time elapsed: 0.002 s
% 117.70/17.74 % (3092219)Peak memory usage: 88 MB
% 117.70/17.74 % (3092218)------------------------------
% 117.70/17.74 % (3092218)------------------------------
% 117.70/17.74 % (3092219)------------------------------
% 117.70/17.74 % (3092219)------------------------------
% 117.70/17.74 % (3092222)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=4045477152:i=598:bs=on:bd=preordered:av=off:ss=axioms_2924 on theBenchmark for (2924ds/598Mi)
% 117.70/17.74 % (3092223)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2913398155:i=2989:sd=3:ss=axioms:sgt=60_2922 on theBenchmark for (2922ds/2989Mi)
% 117.70/17.74 % (3092222)Instruction limit reached!
% 117.70/17.74 % (3092222)------------------------------
% 117.70/17.74 % (3092222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.70/17.74 % (3092222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.70/17.74 % (3092222)CaDiCaL version: 2.1.3
% 117.70/17.74 % (3092222)Termination reason: Instruction limit
% 117.70/17.74 % (3092222)Termination phase: Saturation
% 117.70/17.74 % (3092222)Time elapsed: 0.573 s
% 117.70/17.74 % (3092222)Peak memory usage: 94 MB
% 117.70/17.74 % (3092222)Instructions burned: 598 (million)
% 117.70/17.74 % (3092226)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=163658212:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2915 on theBenchmark for (2915ds/1997Mi)
% 152.26/22.51 % (3092226)Instruction limit reached!
% 152.26/22.51 % (3092226)------------------------------
% 152.26/22.51 % (3092226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.26/22.51 % (3092226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.26/22.51 % (3092226)CaDiCaL version: 2.1.3
% 152.26/22.51 % (3092226)Termination reason: Instruction limit
% 152.26/22.51 % (3092226)Termination phase: Saturation
% 152.26/22.51 % (3092226)Time elapsed: 1.981 s
% 152.26/22.51 % (3092226)Peak memory usage: 140 MB
% 152.26/22.51 % (3092226)Instructions burned: 1997 (million)
% 152.26/22.51 % (3092223)Instruction limit reached!
% 152.26/22.51 % (3092223)------------------------------
% 152.26/22.51 % (3092223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.26/22.51 % (3092223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.26/22.51 % (3092223)CaDiCaL version: 2.1.3
% 152.26/22.51 % (3092223)Termination reason: Instruction limit
% 152.26/22.51 % (3092223)Termination phase: Saturation
% 152.26/22.51 % (3092223)Time elapsed: 2.944 s
% 152.26/22.51 % (3092223)Peak memory usage: 148 MB
% 152.26/22.51 % (3092223)Instructions burned: 2990 (million)
% 152.26/22.51 % (3092232)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=3271460949:i=2088:bd=preordered:av=off_2892 on theBenchmark for (2892ds/2088Mi)
% 152.26/22.51 % (3092233)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1670732280:i=1098:nicw=on_2890 on theBenchmark for (2890ds/1098Mi)
% 152.26/22.51 % (3092233)Instruction limit reached!
% 152.26/22.51 % (3092233)------------------------------
% 152.26/22.51 % (3092233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.26/22.51 % (3092233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.26/22.51 % (3092233)CaDiCaL version: 2.1.3
% 152.26/22.51 % (3092233)Termination reason: Instruction limit
% 152.26/22.51 % (3092233)Termination phase: Saturation
% 152.26/22.51 % (3092233)Time elapsed: 0.957 s
% 152.26/22.51 % (3092233)Peak memory usage: 101 MB
% 152.26/22.51 % (3092233)Instructions burned: 1099 (million)
% 152.26/22.51 % (3092258)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2393054367:i=433:bd=preordered_2877 on theBenchmark for (2877ds/433Mi)
% 152.26/22.51 % (3092258)Refutation not found, incomplete strategy
% 152.26/22.51 % (3092258)------------------------------
% 152.26/22.51 % (3092258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.26/22.51 % (3092258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.26/22.51 % (3092258)CaDiCaL version: 2.1.3
% 152.26/22.51 % (3092258)Termination reason: Refutation not found, incomplete strategy
% 152.26/22.51 % (3092258)Time elapsed: 0.002 s
% 152.26/22.51 % (3092258)Peak memory usage: 88 MB
% 152.26/22.51 % (3092258)Instructions burned: 1 (million)
% 152.26/22.51 % (3092258)------------------------------
% 152.26/22.51 % (3092258)------------------------------
% 152.26/22.51 % (3092232)Instruction limit reached!
% 152.26/22.51 % (3092232)------------------------------
% 152.26/22.51 % (3092232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.26/22.51 % (3092232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.26/22.51 % (3092232)CaDiCaL version: 2.1.3
% 152.26/22.51 % (3092232)Termination reason: Instruction limit
% 152.26/22.51 % (3092232)Termination phase: Saturation
% 152.26/22.51 % (3092232)Time elapsed: 1.661 s
% 152.26/22.51 % (3092232)Peak memory usage: 139 MB
% 152.26/22.51 % (3092232)Instructions burned: 2089 (million)
% 152.26/22.51 % (3092348)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=82595893:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2873 on theBenchmark for (2873ds/2942Mi)
% 152.26/22.51 % (3092349)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=589987778:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2873 on theBenchmark for (2873ds/6922Mi)
% 152.26/22.51 % (3092216)Instruction limit reached!
% 152.26/22.51 % (3092216)------------------------------
% 152.26/22.51 % (3092216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.83/25.42 % (3092216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.83/25.42 % (3092216)CaDiCaL version: 2.1.3
% 172.83/25.42 % (3092216)Termination reason: Instruction limit
% 172.83/25.42 % (3092216)Termination phase: Saturation
% 172.83/25.42 % (3092216)Time elapsed: 7.883 s
% 172.83/25.42 % (3092216)Peak memory usage: 202 MB
% 172.83/25.42 % (3092216)Instructions burned: 8478 (million)
% 172.83/25.42 % (3092399)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3052116478:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2864 on theBenchmark for (2864ds/596Mi)
% 172.83/25.42 % (3092399)Refutation not found, incomplete strategy
% 172.83/25.42 % (3092399)------------------------------
% 172.83/25.42 % (3092399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.83/25.42 % (3092399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.83/25.42 % (3092399)CaDiCaL version: 2.1.3
% 172.83/25.42 % (3092399)Termination reason: Refutation not found, incomplete strategy
% 172.83/25.42 % (3092399)Time elapsed: 0.002 s
% 172.83/25.42 % (3092399)Peak memory usage: 88 MB
% 172.83/25.42 % (3092399)Instructions burned: 1 (million)
% 172.83/25.42 % (3092399)------------------------------
% 172.83/25.42 % (3092399)------------------------------
% 172.83/25.42 % (3092401)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2572432564:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2860 on theBenchmark for (2860ds/4123Mi)
% 172.83/25.42 % (3092212)Instruction limit reached!
% 172.83/25.42 % (3092212)------------------------------
% 172.83/25.42 % (3092212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.83/25.42 % (3092212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.83/25.42 % (3092212)CaDiCaL version: 2.1.3
% 172.83/25.42 % (3092212)Termination reason: Instruction limit
% 172.83/25.42 % (3092212)Termination phase: Saturation
% 172.83/25.42 % (3092212)Time elapsed: 9.518 s
% 172.83/25.42 % (3092212)Peak memory usage: 201 MB
% 172.83/25.42 % (3092212)Instructions burned: 10308 (million)
% 172.83/25.42 % (3092404)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=929722875:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2856 on theBenchmark for (2856ds/16411Mi)
% 172.83/25.42 % (3092348)Instruction limit reached!
% 172.83/25.42 % (3092348)------------------------------
% 172.83/25.42 % (3092348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.83/25.42 % (3092348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.83/25.42 % (3092348)CaDiCaL version: 2.1.3
% 172.83/25.42 % (3092348)Termination reason: Instruction limit
% 172.83/25.42 % (3092348)Termination phase: Saturation
% 172.83/25.42 % (3092348)Time elapsed: 1.882 s
% 172.83/25.42 % (3092348)Peak memory usage: 148 MB
% 172.83/25.42 % (3092348)Instructions burned: 2943 (million)
% 172.83/25.42 % (3092406)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1081890843:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2852 on theBenchmark for (2852ds/1670Mi)
% 172.83/25.42 % (3092406)Instruction limit reached!
% 172.83/25.42 % (3092406)------------------------------
% 172.83/25.42 % (3092406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.83/25.42 % (3092406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.83/25.42 % (3092406)CaDiCaL version: 2.1.3
% 172.83/25.42 % (3092406)Termination reason: Instruction limit
% 172.83/25.42 % (3092406)Termination phase: Saturation
% 172.83/25.42 % (3092406)Time elapsed: 1.052 s
% 172.83/25.42 % (3092406)Peak memory usage: 136 MB
% 172.83/25.42 % (3092406)Instructions burned: 1671 (million)
% 172.83/25.42 % (3092408)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=829128248:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2840 on theBenchmark for (2840ds/1722Mi)
% 172.83/25.42 % (3092401)Instruction limit reached!
% 172.83/25.42 % (3092401)------------------------------
% 172.83/25.42 % (3092401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.83/25.42 % (3092401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.83/25.42 % (3092401)CaDiCaL version: 2.1.3
% 172.83/25.42 % (3092401)Termination reason: Instruction limit
% 172.83/25.42 % (3092401)Termination phase: Saturation
% 152.18/26.11 % (3092401)Time elapsed: 2.477 s
% 152.18/26.11 % (3092401)Peak memory usage: 156 MB
% 152.18/26.11 % (3092401)Instructions burned: 4124 (million)
% 152.18/26.11 % (3092410)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=108982688:cts=off:cond=on:i=9530:bs=on:fsd=on_2833 on theBenchmark for (2833ds/9530Mi)
% 152.18/26.11 % (3092349)Instruction limit reached!
% 152.18/26.11 % (3092349)------------------------------
% 152.18/26.11 % (3092349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092349)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092349)Termination reason: Instruction limit
% 152.18/26.11 % (3092349)Termination phase: Saturation
% 152.18/26.11 % (3092349)Time elapsed: 4.223 s
% 152.18/26.11 % (3092349)Peak memory usage: 168 MB
% 152.18/26.11 % (3092349)Instructions burned: 6924 (million)
% 152.18/26.11 % (3092408)Instruction limit reached!
% 152.18/26.11 % (3092408)------------------------------
% 152.18/26.11 % (3092408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092408)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092408)Termination reason: Instruction limit
% 152.18/26.11 % (3092408)Termination phase: Saturation
% 152.18/26.11 % (3092408)Time elapsed: 1.100 s
% 152.18/26.11 % (3092408)Peak memory usage: 133 MB
% 152.18/26.11 % (3092408)Instructions burned: 1723 (million)
% 152.18/26.11 % (3092412)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1665709844:st=2:i=4495:sd=10:ss=included_2829 on theBenchmark for (2829ds/4495Mi)
% 152.18/26.11 % (3092413)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=2925794871:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2827 on theBenchmark for (2827ds/4920Mi)
% 152.18/26.11 % (3092412)Instruction limit reached!
% 152.18/26.11 % (3092412)------------------------------
% 152.18/26.11 % (3092412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092412)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092412)Termination reason: Instruction limit
% 152.18/26.11 % (3092412)Termination phase: Saturation
% 152.18/26.11 % (3092412)Time elapsed: 2.727 s
% 152.18/26.11 % (3092412)Peak memory usage: 161 MB
% 152.18/26.11 % (3092412)Instructions burned: 4495 (million)
% 152.18/26.11 % (3092416)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=740210679:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2800 on theBenchmark for (2800ds/2083Mi)
% 152.18/26.11 % (3092413)Instruction limit reached!
% 152.18/26.11 % (3092413)------------------------------
% 152.18/26.11 % (3092413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092413)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092413)Termination reason: Instruction limit
% 152.18/26.11 % (3092413)Termination phase: Saturation
% 152.18/26.11 % (3092413)Time elapsed: 2.886 s
% 152.18/26.11 % (3092413)Peak memory usage: 160 MB
% 152.18/26.11 % (3092413)Instructions burned: 4921 (million)
% 152.18/26.11 % (3092418)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=3031276128:i=4629:av=off:gsp=on_2797 on theBenchmark for (2797ds/4629Mi)
% 152.18/26.11 % (3092418)Refutation not found, incomplete strategy
% 152.18/26.11 % (3092418)------------------------------
% 152.18/26.11 % (3092418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092418)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092418)Termination reason: Refutation not found, incomplete strategy
% 152.18/26.11 % (3092418)Time elapsed: 0.575 s
% 152.18/26.11 % (3092418)Peak memory usage: 127 MB
% 152.18/26.11 % (3092418)Instructions burned: 866 (million)
% 152.18/26.11 % (3092418)------------------------------
% 152.18/26.11 % (3092418)------------------------------
% 152.18/26.11 % (3092416)Instruction limit reached!
% 152.18/26.11 % (3092416)------------------------------
% 152.18/26.11 % (3092416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092416)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092416)Termination reason: Instruction limit
% 152.18/26.11 % (3092416)Termination phase: Saturation
% 152.18/26.11 % (3092416)Time elapsed: 1.265 s
% 152.18/26.11 % (3092416)Peak memory usage: 140 MB
% 152.18/26.11 % (3092416)Instructions burned: 2084 (million)
% 152.18/26.11 % (3092420)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=150829638:i=1258:av=off_2787 on theBenchmark for (2787ds/1258Mi)
% 152.18/26.11 % (3092421)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2859761003:i=7343:av=off:ss=included_2785 on theBenchmark for (2785ds/7343Mi)
% 152.18/26.11 % (3092420)Instruction limit reached!
% 152.18/26.11 % (3092420)------------------------------
% 152.18/26.11 % (3092420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092420)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092420)Termination reason: Instruction limit
% 152.18/26.11 % (3092420)Termination phase: Saturation
% 152.18/26.11 % (3092420)Time elapsed: 0.678 s
% 152.18/26.11 % (3092420)Peak memory usage: 108 MB
% 152.18/26.11 % (3092420)Instructions burned: 1259 (million)
% 152.18/26.11 % (3092424)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=124734167:i=1325:sd=2:ss=axioms:sgt=16_2778 on theBenchmark for (2778ds/1325Mi)
% 152.18/26.11 % (3092410)Instruction limit reached!
% 152.18/26.11 % (3092410)------------------------------
% 152.18/26.11 % (3092410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092410)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092410)Termination reason: Instruction limit
% 152.18/26.11 % (3092410)Termination phase: Saturation
% 152.18/26.11 % (3092410)Time elapsed: 5.747 s
% 152.18/26.11 % (3092410)Peak memory usage: 176 MB
% 152.18/26.11 % (3092410)Instructions burned: 9531 (million)
% 152.18/26.11 % (3092426)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=2961684142:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2774 on theBenchmark for (2774ds/2646Mi)
% 152.18/26.11 % (3092424)Instruction limit reached!
% 152.18/26.11 % (3092424)------------------------------
% 152.18/26.11 % (3092424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092424)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092424)Termination reason: Instruction limit
% 152.18/26.11 % (3092424)Termination phase: Saturation
% 152.18/26.11 % (3092424)Time elapsed: 0.883 s
% 152.18/26.11 % (3092424)Peak memory usage: 99 MB
% 152.18/26.11 % (3092424)Instructions burned: 1325 (million)
% 152.18/26.11 % (3092428)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1429756200:i=1489:sd=2:ep=R:ss=axioms_2768 on theBenchmark for (2768ds/1489Mi)
% 152.18/26.11 % (3092428)Refutation not found, incomplete strategy
% 152.18/26.11 % (3092428)------------------------------
% 152.18/26.11 % (3092428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092428)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092428)Termination reason: Refutation not found, incomplete strategy
% 152.18/26.11 % (3092428)Time elapsed: 0.578 s
% 152.18/26.11 % (3092428)Peak memory usage: 127 MB
% 152.18/26.11 % (3092428)Instructions burned: 857 (million)
% 152.18/26.11 % (3092428)------------------------------
% 152.18/26.11 % (3092428)------------------------------
% 152.18/26.11 % (3092426)Instruction limit reached!
% 152.18/26.11 % (3092426)------------------------------
% 152.18/26.11 % (3092426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092426)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092426)Termination reason: Instruction limit
% 152.18/26.11 % (3092426)Termination phase: Saturation
% 152.18/26.11 % (3092426)Time elapsed: 1.560 s
% 152.18/26.11 % (3092426)Peak memory usage: 148 MB
% 152.18/26.11 % (3092426)Instructions burned: 2647 (million)
% 152.18/26.11 % (3092430)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=3432858966:i=1503_2758 on theBenchmark for (2758ds/1503Mi)
% 152.18/26.11 % (3092431)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=995575025:i=13942:kws=frequency_2757 on theBenchmark for (2757ds/13942Mi)
% 152.18/26.11 % (3092160)First to succeed.
% 152.18/26.11 % (3092160)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3092155"
% 152.18/26.11 % (3092430)Refutation not found, incomplete strategy
% 152.18/26.11 % (3092430)------------------------------
% 152.18/26.11 % (3092430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.18/26.11 % (3092430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.18/26.11 % (3092430)CaDiCaL version: 2.1.3
% 152.18/26.11 % (3092430)Termination reason: Refutation not found, incomplete strategy
% 152.18/26.11 % (3092430)Time elapsed: 0.574 s
% 152.18/26.11 % (3092430)Peak memory usage: 127 MB
% 152.18/26.11 % (3092430)Instructions burned: 852 (million)
% 152.18/26.11 % (3092160)Refutation found. Thanks to Tanya!
% 152.18/26.11 % SZS status Unsatisfiable for theBenchmark
% 152.18/26.11 % SZS output start Proof for theBenchmark
% See solution above
% 0.23/26.31 % (3092160)------------------------------
% 0.23/26.31 % (3092160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.23/26.31 % (3092160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/26.31 % (3092160)CaDiCaL version: 2.1.3
% 0.23/26.31 % (3092160)Termination reason: Refutation
% 0.23/26.31 % (3092160)Time elapsed: 24.392 s
% 0.23/26.31 % (3092160)Peak memory usage: 418 MB
% 0.23/26.31 % (3092160)Instructions burned: 31458 (million)
% 0.23/26.31 % (3092160)------------------------------
% 0.23/26.31 % (3092160)------------------------------
% 0.23/26.31 % (3092155)Success in time 25.006 s
% 0.23/26.31 % Vampire exiting
%------------------------------------------------------------------------------