%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL151-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:51:21 AM UTC 2026
% Result : Unsatisfiable 167.54s 28.47s
% Output : Refutation 195.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 77
% Number of leaves : 25
% Syntax : Number of formulae : 434 ( 418 unt; 18 def)
% Number of atoms : 451 ( 422 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 36 ( 19 ~; 15 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 20 con; 0-2 aty)
% Number of variables : 364 ( 0 sgn 364 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : implies(truth,X0) = X0,
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',wajsberg_3) ).
fof(f5,axiom,
! [X0,X1] : implies(implies(not(X0),not(X1)),implies(X1,X0)) = truth,
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',big_hat_definition) ).
fof(f14,negated_conjecture,
big_V(big_hat(x,y),z) != big_hat(big_V(x,z),big_V(y,z)),
file('/export/starexec/sandbox/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(implies(not(implies(implies(not(x),not(y)),not(y))),z),z) != not(implies(implies(not(implies(implies(x,z),z)),not(implies(implies(y,z),z))),not(implies(implies(y,z),z)))),
inference(definition_unfolding,[],[f14,f8,f15,f15,f8,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(sF5,z),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f30,plain,
implies(sF5,z) = sF6,
inference(reorient_equations,[],[f29]) ).
fof(f31,definition,
sF7 = implies(x,z),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f32,plain,
implies(x,z) = sF7,
inference(reorient_equations,[],[f31]) ).
fof(f33,definition,
sF8 = implies(sF7,z),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f34,plain,
implies(sF7,z) = sF8,
inference(reorient_equations,[],[f33]) ).
fof(f35,definition,
sF9 = not(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f36,plain,
not(sF8) = sF9,
inference(reorient_equations,[],[f35]) ).
fof(f37,definition,
sF10 = implies(y,z),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f38,plain,
implies(y,z) = sF10,
inference(reorient_equations,[],[f37]) ).
fof(f39,definition,
sF11 = implies(sF10,z),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f40,plain,
implies(sF10,z) = sF11,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF12 = not(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f42,plain,
not(sF11) = sF12,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF13 = implies(sF9,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f44,plain,
implies(sF9,sF12) = sF13,
inference(reorient_equations,[],[f43]) ).
fof(f45,definition,
sF14 = implies(sF13,sF12),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f46,plain,
implies(sF13,sF12) = sF14,
inference(reorient_equations,[],[f45]) ).
fof(f47,definition,
sF15 = not(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f48,plain,
not(sF14) = sF15,
inference(reorient_equations,[],[f47]) ).
fof(f49,plain,
sF6 != sF15,
inference(definition_folding,[],[f16,f48,f46,f42,f40,f38,f44,f42,f40,f38,f36,f34,f32,f30,f28,f26,f24,f20,f22,f20,f18]) ).
fof(f52,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(f53,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(f61,plain,
! [X2,X0,X1] : truth = implies(implies(X0,implies(not(X1),not(X2))),implies(X0,implies(X2,X1))),
inference(forward_demodulation,[],[f53,f1]) ).
fof(f62,plain,
! [X2,X3,X0,X1] : truth = implies(implies(implies(implies(X1,X2),implies(X0,X2)),X3),implies(implies(X0,X1),X3)),
inference(forward_demodulation,[],[f52,f1]) ).
fof(f66,plain,
! [X0,X1] : truth = implies(X0,implies(implies(X0,X1),implies(truth,X1))),
inference(superposition,[],[f3,f1]) ).
fof(f67,plain,
! [X0] : truth = implies(implies(not(X0),not(truth)),X0),
inference(superposition,[],[f6,f1]) ).
fof(f68,plain,
! [X0,X1] : truth = implies(X0,implies(implies(X0,X1),X1)),
inference(forward_demodulation,[],[f66,f1]) ).
fof(f107,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(f108,plain,
implies(sF7,z) = implies(implies(z,x),x),
inference(superposition,[],[f4,f32]) ).
fof(f109,plain,
implies(sF10,z) = implies(implies(z,y),y),
inference(superposition,[],[f4,f38]) ).
fof(f117,plain,
! [X0,X1] : truth = implies(implies(not(X0),not(implies(X1,X0))),implies(implies(X0,X1),X1)),
inference(superposition,[],[f6,f4]) ).
fof(f118,plain,
sF11 = implies(implies(z,y),y),
inference(forward_demodulation,[],[f109,f40]) ).
fof(f119,plain,
sF8 = implies(implies(z,x),x),
inference(forward_demodulation,[],[f108,f34]) ).
fof(f120,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,[],[f107,f1]) ).
fof(f133,plain,
implies(sF2,sF1) = implies(implies(sF1,sF0),sF0),
inference(superposition,[],[f4,f22]) ).
fof(f138,plain,
sF3 = implies(implies(sF1,sF0),sF0),
inference(forward_demodulation,[],[f133,f24]) ).
fof(f147,plain,
implies(sF13,sF12) = implies(implies(sF12,sF9),sF9),
inference(superposition,[],[f4,f44]) ).
fof(f152,plain,
sF14 = implies(implies(sF12,sF9),sF9),
inference(forward_demodulation,[],[f147,f46]) ).
fof(f163,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,[],[f120,f4]) ).
fof(f194,plain,
! [X0,X1] : implies(implies(X0,X1),implies(truth,X1)) = implies(implies(implies(implies(X0,X1),implies(truth,X1)),X0),X0),
inference(superposition,[],[f120,f1]) ).
fof(f216,plain,
! [X0,X1] : implies(implies(X0,X1),X1) = implies(implies(implies(implies(X0,X1),X1),X0),X0),
inference(forward_demodulation,[],[f194,f1]) ).
fof(f290,plain,
truth = implies(x,implies(sF7,z)),
inference(superposition,[],[f68,f32]) ).
fof(f291,plain,
truth = implies(y,implies(sF10,z)),
inference(superposition,[],[f68,f38]) ).
fof(f292,plain,
truth = implies(sF0,implies(sF2,sF1)),
inference(superposition,[],[f68,f22]) ).
fof(f302,plain,
! [X0,X1] : truth = implies(X1,implies(implies(X0,X1),X1)),
inference(superposition,[],[f68,f4]) ).
fof(f304,plain,
truth = implies(z,sF8),
inference(superposition,[],[f68,f119]) ).
fof(f307,plain,
! [X2,X0,X1] : truth = implies(truth,implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2))),
inference(superposition,[],[f3,f68]) ).
fof(f317,plain,
! [X0] : truth = implies(implies(truth,X0),X0),
inference(superposition,[],[f1,f68]) ).
fof(f321,plain,
! [X0] : truth = implies(X0,X0),
inference(forward_demodulation,[],[f317,f1]) ).
fof(f327,plain,
! [X2,X0,X1] : truth = implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2)),
inference(forward_demodulation,[],[f307,f1]) ).
fof(f331,plain,
truth = implies(sF0,sF3),
inference(forward_demodulation,[],[f292,f24]) ).
fof(f332,plain,
truth = implies(y,sF11),
inference(forward_demodulation,[],[f291,f40]) ).
fof(f333,plain,
truth = implies(x,sF8),
inference(forward_demodulation,[],[f290,f34]) ).
fof(f531,plain,
! [X2,X0,X1] : truth = implies(implies(implies(implies(X0,X1),X1),X2),implies(X1,X2)),
inference(superposition,[],[f327,f4]) ).
fof(f569,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),X1) = implies(truth,implies(X0,X1)),
inference(superposition,[],[f216,f327]) ).
fof(f571,plain,
! [X2,X0,X1] : truth = implies(truth,implies(implies(X2,implies(X0,X1)),implies(X0,implies(X2,X1)))),
inference(superposition,[],[f62,f327]) ).
fof(f591,plain,
! [X2,X0,X1] : truth = implies(implies(X2,implies(X0,X1)),implies(X0,implies(X2,X1))),
inference(forward_demodulation,[],[f571,f1]) ).
fof(f592,plain,
! [X0,X1] : implies(X0,X1) = implies(implies(implies(X0,X1),X1),X1),
inference(forward_demodulation,[],[f569,f1]) ).
fof(f634,plain,
sF7 = implies(implies(sF7,z),z),
inference(superposition,[],[f592,f32]) ).
fof(f635,plain,
sF10 = implies(implies(sF10,z),z),
inference(superposition,[],[f592,f38]) ).
fof(f636,plain,
sF2 = implies(implies(sF2,sF1),sF1),
inference(superposition,[],[f592,f22]) ).
fof(f638,plain,
sF5 = implies(implies(sF5,z),z),
inference(superposition,[],[f592,f28]) ).
fof(f641,plain,
sF13 = implies(implies(sF13,sF12),sF12),
inference(superposition,[],[f592,f44]) ).
fof(f646,plain,
implies(z,x) = implies(sF8,x),
inference(superposition,[],[f592,f119]) ).
fof(f647,plain,
implies(z,y) = implies(sF11,y),
inference(superposition,[],[f592,f118]) ).
fof(f661,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X2,X1)) = implies(implies(implies(implies(X0,X1),implies(X2,X1)),implies(X2,implies(implies(X0,X1),X1))),implies(X2,implies(implies(X0,X1),X1))),
inference(superposition,[],[f120,f592]) ).
fof(f667,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X2,X1)) = implies(truth,implies(X2,implies(implies(X0,X1),X1))),
inference(forward_demodulation,[],[f661,f591]) ).
fof(f669,plain,
sF13 = implies(sF14,sF12),
inference(forward_demodulation,[],[f641,f46]) ).
fof(f670,plain,
sF5 = implies(sF6,z),
inference(forward_demodulation,[],[f638,f30]) ).
fof(f671,plain,
sF2 = implies(sF3,sF1),
inference(forward_demodulation,[],[f636,f24]) ).
fof(f672,plain,
sF10 = implies(sF11,z),
inference(forward_demodulation,[],[f635,f40]) ).
fof(f673,plain,
sF7 = implies(sF8,z),
inference(forward_demodulation,[],[f634,f34]) ).
fof(f681,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X2,X1)) = implies(X2,implies(implies(X0,X1),X1)),
inference(forward_demodulation,[],[f667,f1]) ).
fof(f684,plain,
! [X0,X1] : implies(X1,implies(implies(X0,X1),X1)) = implies(implies(X0,X1),truth),
inference(superposition,[],[f681,f321]) ).
fof(f699,plain,
! [X0] : implies(implies(X0,z),sF10) = implies(y,implies(implies(X0,z),z)),
inference(superposition,[],[f681,f38]) ).
fof(f716,plain,
! [X0,X1] : implies(X0,implies(X1,X0)) = implies(X1,implies(X0,X0)),
inference(superposition,[],[f681,f1]) ).
fof(f729,plain,
! [X0] : implies(sF7,implies(X0,z)) = implies(X0,implies(sF7,z)),
inference(superposition,[],[f681,f32]) ).
fof(f730,plain,
! [X0] : implies(sF10,implies(X0,z)) = implies(X0,implies(sF10,z)),
inference(superposition,[],[f681,f38]) ).
fof(f731,plain,
! [X0] : implies(sF2,implies(X0,sF1)) = implies(X0,implies(sF2,sF1)),
inference(superposition,[],[f681,f22]) ).
fof(f733,plain,
! [X0] : implies(sF5,implies(X0,z)) = implies(X0,implies(sF5,z)),
inference(superposition,[],[f681,f28]) ).
fof(f734,plain,
! [X0] : implies(sF6,implies(X0,z)) = implies(X0,implies(sF6,z)),
inference(superposition,[],[f681,f30]) ).
fof(f737,plain,
! [X0] : implies(sF11,implies(X0,z)) = implies(X0,implies(sF11,z)),
inference(superposition,[],[f681,f40]) ).
fof(f738,plain,
! [X0] : implies(sF14,implies(X0,sF12)) = implies(X0,implies(sF14,sF12)),
inference(superposition,[],[f681,f46]) ).
fof(f741,plain,
! [X2,X0,X1] : implies(X2,implies(implies(X0,X1),X1)) = implies(implies(X1,X0),implies(X2,X0)),
inference(superposition,[],[f681,f4]) ).
fof(f744,plain,
! [X0] : implies(X0,sF8) = implies(implies(z,x),implies(X0,x)),
inference(superposition,[],[f681,f119]) ).
fof(f830,plain,
! [X0] : implies(X0,sF8) = implies(implies(sF8,x),implies(X0,x)),
inference(forward_demodulation,[],[f744,f646]) ).
fof(f832,plain,
! [X0] : implies(X0,sF13) = implies(sF14,implies(X0,sF12)),
inference(forward_demodulation,[],[f738,f669]) ).
fof(f833,plain,
! [X0] : implies(X0,sF10) = implies(sF11,implies(X0,z)),
inference(forward_demodulation,[],[f737,f672]) ).
fof(f836,plain,
! [X0] : implies(X0,sF5) = implies(sF6,implies(X0,z)),
inference(forward_demodulation,[],[f734,f670]) ).
fof(f837,plain,
! [X0] : implies(sF5,implies(X0,z)) = implies(X0,sF6),
inference(forward_demodulation,[],[f733,f30]) ).
fof(f839,plain,
! [X0] : implies(X0,sF3) = implies(sF2,implies(X0,sF1)),
inference(forward_demodulation,[],[f731,f24]) ).
fof(f840,plain,
! [X0] : implies(sF10,implies(X0,z)) = implies(X0,sF11),
inference(forward_demodulation,[],[f730,f40]) ).
fof(f841,plain,
! [X0] : implies(sF7,implies(X0,z)) = implies(X0,sF8),
inference(forward_demodulation,[],[f729,f34]) ).
fof(f849,plain,
! [X0,X1] : implies(X1,truth) = implies(X0,implies(X1,X0)),
inference(forward_demodulation,[],[f716,f321]) ).
fof(f855,plain,
! [X0,X1] : truth = implies(implies(X0,X1),truth),
inference(forward_demodulation,[],[f684,f302]) ).
fof(f998,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,[],[f216,f591]) ).
fof(f1008,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,[],[f998,f1]) ).
fof(f1057,plain,
! [X2,X0,X1] : implies(X1,implies(X0,X2)) = implies(truth,implies(X0,implies(X1,X2))),
inference(forward_demodulation,[],[f1008,f591]) ).
fof(f1065,plain,
! [X2,X0,X1] : implies(X0,implies(X1,X2)) = implies(X1,implies(X0,X2)),
inference(forward_demodulation,[],[f1057,f1]) ).
fof(f1131,plain,
! [X0] : implies(X0,sF7) = implies(x,implies(X0,z)),
inference(superposition,[],[f1065,f32]) ).
fof(f1132,plain,
! [X0] : implies(X0,sF10) = implies(y,implies(X0,z)),
inference(superposition,[],[f1065,f38]) ).
fof(f1135,plain,
! [X0] : implies(X0,sF5) = implies(sF4,implies(X0,z)),
inference(superposition,[],[f1065,f28]) ).
fof(f1139,plain,
! [X0] : implies(X0,sF13) = implies(sF9,implies(X0,sF12)),
inference(superposition,[],[f1065,f44]) ).
fof(f1240,plain,
! [X2,X0,X1] : implies(X0,implies(implies(X1,implies(X0,X2)),X2)) = implies(implies(implies(X0,X2),X1),X1),
inference(superposition,[],[f4,f1065]) ).
fof(f1326,plain,
implies(sF10,sF7) = implies(x,sF11),
inference(superposition,[],[f1131,f40]) ).
fof(f1448,plain,
implies(sF4,sF8) = implies(sF7,sF5),
inference(superposition,[],[f841,f28]) ).
fof(f1450,plain,
implies(sF7,sF5) = implies(sF6,sF8),
inference(superposition,[],[f841,f670]) ).
fof(f1453,plain,
implies(sF7,sF10) = implies(sF11,sF8),
inference(superposition,[],[f841,f672]) ).
fof(f1510,plain,
implies(sF10,sF7) = implies(sF8,sF11),
inference(superposition,[],[f840,f673]) ).
fof(f1556,plain,
! [X0,X1] : implies(X0,truth) = implies(implies(implies(X0,X1),X1),truth),
inference(superposition,[],[f849,f68]) ).
fof(f1605,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),X1) = implies(implies(X0,truth),implies(X0,X1)),
inference(superposition,[],[f4,f849]) ).
fof(f1632,plain,
! [X0,X1] : implies(X0,X1) = implies(implies(X0,truth),implies(X0,X1)),
inference(forward_demodulation,[],[f1605,f592]) ).
fof(f1656,plain,
! [X0] : truth = implies(X0,truth),
inference(forward_demodulation,[],[f1556,f855]) ).
fof(f1896,plain,
implies(sF12,sF13) = implies(sF14,truth),
inference(superposition,[],[f849,f669]) ).
fof(f1901,plain,
truth = implies(sF12,sF13),
inference(forward_demodulation,[],[f1896,f1656]) ).
fof(f1936,plain,
implies(sF1,sF2) = implies(sF3,truth),
inference(superposition,[],[f849,f671]) ).
fof(f1941,plain,
truth = implies(sF1,sF2),
inference(forward_demodulation,[],[f1936,f1656]) ).
fof(f2417,plain,
! [X0,X1] : truth = implies(implies(not(X0),truth),implies(not(X1),implies(X1,X0))),
inference(superposition,[],[f61,f849]) ).
fof(f2595,plain,
! [X0,X1] : truth = implies(truth,implies(not(X1),implies(X1,X0))),
inference(forward_demodulation,[],[f2417,f1656]) ).
fof(f2605,plain,
! [X0,X1] : truth = implies(not(X1),implies(X1,X0)),
inference(forward_demodulation,[],[f2595,f1]) ).
fof(f2670,plain,
! [X0,X1] : truth = implies(X0,implies(not(X0),X1)),
inference(superposition,[],[f1065,f2605]) ).
fof(f2674,plain,
! [X0,X1] : truth = implies(truth,implies(not(not(X0)),implies(X1,X0))),
inference(superposition,[],[f61,f2605]) ).
fof(f2725,plain,
! [X0,X1] : truth = implies(not(not(X0)),implies(X1,X0)),
inference(forward_demodulation,[],[f2674,f1]) ).
fof(f2759,plain,
! [X0] : truth = implies(not(not(X0)),X0),
inference(superposition,[],[f2725,f1]) ).
fof(f2883,plain,
! [X0] : truth = implies(truth,implies(X0,not(not(X0)))),
inference(superposition,[],[f6,f2759]) ).
fof(f2955,plain,
! [X0] : truth = implies(X0,not(not(X0))),
inference(forward_demodulation,[],[f2883,f1]) ).
fof(f3089,plain,
! [X0] : implies(truth,not(not(X0))) = implies(implies(implies(truth,not(not(X0))),X0),X0),
inference(superposition,[],[f216,f2955]) ).
fof(f3122,plain,
! [X0] : not(not(X0)) = implies(implies(not(not(X0)),X0),X0),
inference(forward_demodulation,[],[f3089,f1]) ).
fof(f3137,plain,
! [X0] : implies(truth,X0) = not(not(X0)),
inference(forward_demodulation,[],[f3122,f2759]) ).
fof(f3144,plain,
! [X0] : not(not(X0)) = X0,
inference(forward_demodulation,[],[f3137,f1]) ).
fof(f3150,plain,
x = not(sF0),
inference(superposition,[],[f3144,f18]) ).
fof(f3151,plain,
y = not(sF1),
inference(superposition,[],[f3144,f20]) ).
fof(f3152,plain,
sF3 = not(sF4),
inference(superposition,[],[f3144,f26]) ).
fof(f3153,plain,
sF8 = not(sF9),
inference(superposition,[],[f3144,f36]) ).
fof(f3154,plain,
sF11 = not(sF12),
inference(superposition,[],[f3144,f42]) ).
fof(f3159,plain,
! [X0,X1] : truth = implies(implies(X0,not(X1)),implies(X1,not(X0))),
inference(superposition,[],[f6,f3144]) ).
fof(f3204,plain,
! [X2,X0,X1] : truth = implies(implies(X0,X1),implies(truth,implies(X0,implies(not(X1),X2)))),
inference(superposition,[],[f3,f2670]) ).
fof(f3274,plain,
! [X2,X0,X1] : truth = implies(implies(X0,X1),implies(X0,implies(not(X1),X2))),
inference(forward_demodulation,[],[f3204,f1]) ).
fof(f3306,plain,
implies(sF1,sF0) = implies(sF3,sF0),
inference(superposition,[],[f592,f138]) ).
fof(f6245,plain,
! [X0,X1] : implies(truth,implies(X1,X0)) = implies(implies(implies(truth,implies(X1,X0)),implies(X1,implies(not(X0),not(truth)))),implies(X1,implies(not(X0),not(truth)))),
inference(superposition,[],[f120,f67]) ).
fof(f6316,plain,
! [X0,X1] : implies(X1,X0) = implies(implies(implies(X1,X0),implies(X1,implies(not(X0),not(truth)))),implies(X1,implies(not(X0),not(truth)))),
inference(forward_demodulation,[],[f6245,f1]) ).
fof(f6347,plain,
! [X0,X1] : implies(X1,X0) = implies(truth,implies(X1,implies(not(X0),not(truth)))),
inference(forward_demodulation,[],[f6316,f3274]) ).
fof(f6371,plain,
! [X0,X1] : implies(X1,X0) = implies(X1,implies(not(X0),not(truth))),
inference(forward_demodulation,[],[f6347,f1]) ).
fof(f6381,plain,
! [X0,X1] : implies(X1,not(X0)) = implies(X1,implies(X0,not(truth))),
inference(superposition,[],[f6371,f3144]) ).
fof(f6458,plain,
! [X0] : implies(truth,X0) = implies(not(X0),not(truth)),
inference(superposition,[],[f1,f6371]) ).
fof(f6520,plain,
! [X0] : implies(not(X0),not(truth)) = X0,
inference(forward_demodulation,[],[f6458,f1]) ).
fof(f6585,plain,
! [X0] : not(X0) = implies(X0,not(truth)),
inference(superposition,[],[f6520,f3144]) ).
fof(f6614,plain,
! [X0,X1] : implies(X0,implies(X1,not(truth))) = implies(implies(implies(X0,implies(X1,not(truth))),implies(X1,not(X0))),implies(X1,not(X0))),
inference(superposition,[],[f120,f6520]) ).
fof(f6650,plain,
! [X0,X1] : implies(X0,not(X1)) = implies(implies(implies(X0,not(X1)),implies(X1,not(X0))),implies(X1,not(X0))),
inference(forward_demodulation,[],[f6614,f6381]) ).
fof(f6669,plain,
! [X0,X1] : implies(X0,not(X1)) = implies(truth,implies(X1,not(X0))),
inference(forward_demodulation,[],[f6650,f3159]) ).
fof(f6679,plain,
! [X0,X1] : implies(X0,not(X1)) = implies(X1,not(X0)),
inference(forward_demodulation,[],[f6669,f1]) ).
fof(f6706,plain,
! [X0,X1] : implies(X1,X0) = implies(not(X0),not(X1)),
inference(superposition,[],[f6679,f3144]) ).
fof(f6708,plain,
! [X0] : implies(X0,sF1) = implies(y,not(X0)),
inference(superposition,[],[f6679,f20]) ).
fof(f6709,plain,
! [X0] : implies(X0,x) = implies(sF0,not(X0)),
inference(superposition,[],[f6679,f3150]) ).
fof(f6710,plain,
! [X0] : implies(X0,y) = implies(sF1,not(X0)),
inference(superposition,[],[f6679,f3151]) ).
fof(f6711,plain,
! [X0] : implies(X0,sF4) = implies(sF3,not(X0)),
inference(superposition,[],[f6679,f26]) ).
fof(f6713,plain,
! [X0] : implies(X0,sF12) = implies(sF11,not(X0)),
inference(superposition,[],[f6679,f42]) ).
fof(f6714,plain,
! [X0] : implies(X0,sF11) = implies(sF12,not(X0)),
inference(superposition,[],[f6679,f3154]) ).
fof(f6715,plain,
! [X0] : implies(X0,sF15) = implies(sF14,not(X0)),
inference(superposition,[],[f6679,f48]) ).
fof(f6829,plain,
! [X2,X0,X1] : implies(X1,implies(X2,not(X0))) = implies(X2,implies(X0,not(X1))),
inference(superposition,[],[f1065,f6679]) ).
fof(f6903,plain,
! [X0] : implies(X0,sF3) = implies(sF4,not(X0)),
inference(superposition,[],[f6706,f26]) ).
fof(f6904,plain,
! [X0] : implies(X0,sF8) = implies(sF9,not(X0)),
inference(superposition,[],[f6706,f36]) ).
fof(f6908,plain,
! [X0,X1] : implies(not(X0),X1) = implies(not(X1),X0),
inference(superposition,[],[f6706,f3144]) ).
fof(f6909,plain,
! [X0] : implies(x,X0) = implies(not(X0),sF0),
inference(superposition,[],[f6706,f18]) ).
fof(f6910,plain,
! [X0] : implies(y,X0) = implies(not(X0),sF1),
inference(superposition,[],[f6706,f20]) ).
fof(f6911,plain,
! [X0] : implies(sF0,X0) = implies(not(X0),x),
inference(superposition,[],[f6706,f3150]) ).
fof(f6912,plain,
! [X0] : implies(sF1,X0) = implies(not(X0),y),
inference(superposition,[],[f6706,f3151]) ).
fof(f6916,plain,
! [X0] : implies(sF12,X0) = implies(not(X0),sF11),
inference(superposition,[],[f6706,f3154]) ).
fof(f6940,plain,
! [X0,X1] : implies(implies(not(X0),not(X1)),not(X1)) = implies(implies(X0,X1),not(X0)),
inference(superposition,[],[f4,f6706]) ).
fof(f6968,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = implies(not(X1),implies(X2,not(X0))),
inference(superposition,[],[f1065,f6706]) ).
fof(f6983,plain,
! [X0,X1] : implies(implies(X0,X1),not(X0)) = implies(implies(X1,X0),not(X1)),
inference(forward_demodulation,[],[f6940,f6706]) ).
fof(f7013,plain,
! [X0] : implies(sF9,X0) = implies(not(X0),sF8),
inference(superposition,[],[f6908,f36]) ).
fof(f7136,plain,
! [X2,X0,X1] : implies(X2,implies(not(X0),X1)) = implies(not(X1),implies(X2,X0)),
inference(superposition,[],[f1065,f6908]) ).
fof(f7218,plain,
implies(sF0,sF1) = implies(y,x),
inference(superposition,[],[f6910,f18]) ).
fof(f7288,plain,
sF2 = implies(y,x),
inference(forward_demodulation,[],[f7218,f22]) ).
fof(f7651,plain,
implies(sF3,sF1) = implies(y,sF4),
inference(superposition,[],[f6910,f3152]) ).
fof(f7652,plain,
sF2 = implies(y,sF4),
inference(forward_demodulation,[],[f7651,f671]) ).
fof(f7853,plain,
implies(sF1,sF0) = implies(x,y),
inference(superposition,[],[f6909,f20]) ).
fof(f7857,plain,
implies(x,sF8) = implies(sF9,sF0),
inference(superposition,[],[f6909,f36]) ).
fof(f7859,plain,
implies(x,sF11) = implies(sF12,sF0),
inference(superposition,[],[f6909,f42]) ).
fof(f7918,plain,
implies(sF10,sF7) = implies(sF12,sF0),
inference(forward_demodulation,[],[f7859,f1326]) ).
fof(f7919,plain,
truth = implies(sF9,sF0),
inference(forward_demodulation,[],[f7857,f333]) ).
fof(f7922,plain,
implies(sF8,sF11) = implies(sF12,sF0),
inference(forward_demodulation,[],[f7918,f1510]) ).
fof(f9586,plain,
implies(sF14,sF1) = implies(y,sF15),
inference(superposition,[],[f6708,f48]) ).
fof(f10355,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),not(implies(X1,X0))) = implies(implies(X0,implies(X1,X0)),not(X0)),
inference(superposition,[],[f6983,f4]) ).
fof(f10372,plain,
! [X0,X1] : implies(implies(not(X1),implies(X1,X0)),not(not(X1))) = implies(implies(implies(X0,X1),not(X0)),not(implies(X1,X0))),
inference(superposition,[],[f6983,f6983]) ).
fof(f10374,plain,
implies(sF11,not(implies(z,y))) = implies(implies(y,implies(z,y)),not(y)),
inference(superposition,[],[f6983,f118]) ).
fof(f10375,plain,
implies(sF3,not(implies(sF1,sF0))) = implies(implies(sF0,implies(sF1,sF0)),not(sF0)),
inference(superposition,[],[f6983,f138]) ).
fof(f10392,plain,
implies(sF3,not(sF2)) = implies(implies(sF1,sF2),not(sF1)),
inference(superposition,[],[f6983,f24]) ).
fof(f10403,plain,
implies(sF14,not(sF13)) = implies(implies(sF12,sF13),not(sF12)),
inference(superposition,[],[f6983,f46]) ).
fof(f10474,plain,
! [X0,X1] : implies(implies(X0,X1),not(X0)) = implies(X1,not(implies(X1,X0))),
inference(superposition,[],[f6679,f6983]) ).
fof(f10538,plain,
implies(sF14,not(sF13)) = implies(implies(sF12,sF13),sF11),
inference(forward_demodulation,[],[f10403,f3154]) ).
fof(f10549,plain,
implies(sF3,not(sF2)) = implies(implies(sF1,sF2),y),
inference(forward_demodulation,[],[f10392,f3151]) ).
fof(f10566,plain,
implies(sF3,not(implies(sF1,sF0))) = implies(implies(sF0,implies(sF1,sF0)),x),
inference(forward_demodulation,[],[f10375,f3150]) ).
fof(f10567,plain,
implies(sF11,not(implies(z,y))) = implies(implies(y,implies(z,y)),sF1),
inference(forward_demodulation,[],[f10374,f20]) ).
fof(f10569,plain,
! [X0,X1] : implies(implies(implies(X0,X1),not(X0)),not(implies(X1,X0))) = implies(implies(not(X1),implies(X1,X0)),X1),
inference(forward_demodulation,[],[f10372,f3144]) ).
fof(f10584,plain,
! [X0,X1] : implies(implies(implies(X0,X1),X1),not(implies(X1,X0))) = implies(implies(X1,truth),not(X0)),
inference(forward_demodulation,[],[f10355,f849]) ).
fof(f10674,plain,
implies(truth,sF11) = implies(sF14,not(sF13)),
inference(forward_demodulation,[],[f10538,f1901]) ).
fof(f10685,plain,
implies(sF3,not(sF2)) = implies(truth,y),
inference(forward_demodulation,[],[f10549,f1941]) ).
fof(f10700,plain,
implies(sF3,not(implies(sF1,sF0))) = implies(implies(sF1,truth),x),
inference(forward_demodulation,[],[f10566,f849]) ).
fof(f10701,plain,
implies(sF11,not(implies(z,y))) = implies(implies(z,truth),sF1),
inference(forward_demodulation,[],[f10567,f849]) ).
fof(f10703,plain,
! [X0,X1] : implies(truth,X1) = implies(implies(implies(X0,X1),not(X0)),not(implies(X1,X0))),
inference(forward_demodulation,[],[f10569,f2605]) ).
fof(f10716,plain,
! [X0,X1] : implies(truth,not(X0)) = implies(implies(implies(X0,X1),X1),not(implies(X1,X0))),
inference(forward_demodulation,[],[f10584,f1656]) ).
fof(f10786,plain,
implies(truth,sF11) = implies(sF13,sF15),
inference(forward_demodulation,[],[f10674,f6715]) ).
fof(f10792,plain,
y = implies(sF3,not(sF2)),
inference(forward_demodulation,[],[f10685,f1]) ).
fof(f10799,plain,
implies(sF3,not(implies(sF1,sF0))) = implies(truth,x),
inference(forward_demodulation,[],[f10700,f1656]) ).
fof(f10800,plain,
implies(truth,sF1) = implies(sF11,not(implies(z,y))),
inference(forward_demodulation,[],[f10701,f1656]) ).
fof(f10802,plain,
! [X0,X1] : implies(implies(implies(X0,X1),not(X0)),not(implies(X1,X0))) = X1,
inference(forward_demodulation,[],[f10703,f1]) ).
fof(f10814,plain,
! [X0,X1] : not(X0) = implies(implies(implies(X0,X1),X1),not(implies(X1,X0))),
inference(forward_demodulation,[],[f10716,f1]) ).
fof(f10858,plain,
sF11 = implies(sF13,sF15),
inference(forward_demodulation,[],[f10786,f1]) ).
fof(f10863,plain,
y = implies(sF2,sF4),
inference(forward_demodulation,[],[f10792,f6711]) ).
fof(f10867,plain,
x = implies(sF3,not(implies(sF1,sF0))),
inference(forward_demodulation,[],[f10799,f1]) ).
fof(f10868,plain,
implies(truth,sF1) = implies(implies(z,y),sF12),
inference(forward_demodulation,[],[f10800,f6713]) ).
fof(f10892,plain,
x = implies(implies(sF1,sF0),sF4),
inference(forward_demodulation,[],[f10867,f6711]) ).
fof(f10893,plain,
implies(truth,sF1) = implies(implies(sF11,y),sF12),
inference(forward_demodulation,[],[f10868,f647]) ).
fof(f10902,plain,
sF1 = implies(implies(sF11,y),sF12),
inference(forward_demodulation,[],[f10893,f1]) ).
fof(f10940,plain,
truth = implies(not(not(sF4)),y),
inference(superposition,[],[f2725,f10863]) ).
fof(f10941,plain,
truth = implies(sF1,not(sF4)),
inference(forward_demodulation,[],[f10940,f6912]) ).
fof(f10962,plain,
truth = implies(sF4,y),
inference(forward_demodulation,[],[f10941,f6710]) ).
fof(f11070,plain,
not(sF9) = implies(implies(truth,sF0),not(implies(sF0,sF9))),
inference(superposition,[],[f10814,f7919]) ).
fof(f11177,plain,
not(z) = implies(implies(implies(z,y),y),not(sF10)),
inference(superposition,[],[f10814,f38]) ).
fof(f11338,plain,
not(z) = implies(sF11,not(sF10)),
inference(forward_demodulation,[],[f11177,f118]) ).
fof(f11426,plain,
not(sF9) = implies(sF0,not(implies(sF0,sF9))),
inference(forward_demodulation,[],[f11070,f1]) ).
fof(f11544,plain,
not(z) = implies(sF10,sF12),
inference(forward_demodulation,[],[f11338,f6713]) ).
fof(f11605,plain,
not(sF9) = implies(implies(sF0,sF9),x),
inference(forward_demodulation,[],[f11426,f6709]) ).
fof(f11722,plain,
sF8 = implies(implies(sF0,sF9),x),
inference(forward_demodulation,[],[f11605,f3153]) ).
fof(f11786,plain,
implies(sF10,sF13) = implies(sF9,not(z)),
inference(superposition,[],[f1139,f11544]) ).
fof(f11854,plain,
implies(z,sF8) = implies(sF10,sF13),
inference(forward_demodulation,[],[f11786,f6904]) ).
fof(f11874,plain,
truth = implies(sF10,sF13),
inference(forward_demodulation,[],[f11854,f304]) ).
fof(f13484,plain,
truth = implies(not(not(sF15)),sF11),
inference(superposition,[],[f2725,f10858]) ).
fof(f13491,plain,
truth = implies(sF12,not(sF15)),
inference(forward_demodulation,[],[f13484,f6916]) ).
fof(f13509,plain,
truth = implies(sF15,sF11),
inference(forward_demodulation,[],[f13491,f6714]) ).
fof(f14544,plain,
implies(z,x) = implies(implies(implies(x,implies(z,x)),not(x)),not(sF8)),
inference(superposition,[],[f10802,f119]) ).
fof(f14545,plain,
implies(z,y) = implies(implies(implies(y,implies(z,y)),not(y)),not(sF11)),
inference(superposition,[],[f10802,f118]) ).
fof(f14607,plain,
sF13 = implies(implies(implies(sF12,sF13),not(sF12)),not(sF14)),
inference(superposition,[],[f10802,f46]) ).
fof(f14710,plain,
sF13 = implies(implies(implies(sF12,sF13),not(sF12)),sF15),
inference(forward_demodulation,[],[f14607,f48]) ).
fof(f14766,plain,
implies(z,y) = implies(implies(implies(y,implies(z,y)),not(y)),sF12),
inference(forward_demodulation,[],[f14545,f42]) ).
fof(f14767,plain,
implies(z,x) = implies(implies(implies(x,implies(z,x)),not(x)),sF9),
inference(forward_demodulation,[],[f14544,f36]) ).
fof(f14950,plain,
sF13 = implies(implies(implies(sF12,sF13),sF11),sF15),
inference(forward_demodulation,[],[f14710,f3154]) ).
fof(f15003,plain,
implies(z,y) = implies(implies(implies(y,implies(z,y)),sF1),sF12),
inference(forward_demodulation,[],[f14766,f20]) ).
fof(f15004,plain,
implies(z,x) = implies(implies(implies(x,implies(z,x)),sF0),sF9),
inference(forward_demodulation,[],[f14767,f18]) ).
fof(f15147,plain,
sF13 = implies(implies(truth,sF11),sF15),
inference(forward_demodulation,[],[f14950,f1901]) ).
fof(f15195,plain,
implies(z,y) = implies(implies(implies(z,truth),sF1),sF12),
inference(forward_demodulation,[],[f15003,f849]) ).
fof(f15196,plain,
implies(z,x) = implies(implies(implies(z,truth),sF0),sF9),
inference(forward_demodulation,[],[f15004,f849]) ).
fof(f15305,plain,
sF13 = implies(sF11,sF15),
inference(forward_demodulation,[],[f15147,f1]) ).
fof(f15348,plain,
implies(z,y) = implies(implies(truth,sF1),sF12),
inference(forward_demodulation,[],[f15195,f1656]) ).
fof(f15349,plain,
implies(z,x) = implies(implies(truth,sF0),sF9),
inference(forward_demodulation,[],[f15196,f1656]) ).
fof(f15429,plain,
implies(z,y) = implies(sF1,sF12),
inference(forward_demodulation,[],[f15348,f1]) ).
fof(f15430,plain,
implies(z,x) = implies(sF0,sF9),
inference(forward_demodulation,[],[f15349,f1]) ).
fof(f15452,plain,
implies(sF11,y) = implies(sF1,sF12),
inference(forward_demodulation,[],[f15429,f647]) ).
fof(f15453,plain,
implies(sF8,x) = implies(sF0,sF9),
inference(forward_demodulation,[],[f15430,f646]) ).
fof(f22466,plain,
! [X2,X0,X1] : implies(not(X2),implies(X0,not(implies(X0,X1)))) = implies(implies(X1,X0),implies(not(not(X1)),X2)),
inference(superposition,[],[f7136,f10474]) ).
fof(f22468,plain,
! [X2,X0,X1] : implies(not(X2),implies(implies(X0,X1),not(X0))) = implies(implies(X1,X0),implies(not(not(X1)),X2)),
inference(superposition,[],[f7136,f6983]) ).
fof(f22469,plain,
! [X2,X0,X1] : implies(not(X2),not(X0)) = implies(implies(implies(X0,X1),X1),implies(not(not(implies(X1,X0))),X2)),
inference(superposition,[],[f7136,f10814]) ).
fof(f22943,plain,
! [X2,X0,X1] : implies(not(X2),not(X0)) = implies(implies(implies(X0,X1),X1),implies(implies(X1,X0),X2)),
inference(forward_demodulation,[],[f22469,f3144]) ).
fof(f22944,plain,
! [X2,X0,X1] : implies(implies(X1,X0),implies(X1,X2)) = implies(not(X2),implies(implies(X0,X1),not(X0))),
inference(forward_demodulation,[],[f22468,f3144]) ).
fof(f22946,plain,
! [X2,X0,X1] : implies(implies(X1,X0),implies(X1,X2)) = implies(not(X2),implies(X0,not(implies(X0,X1)))),
inference(forward_demodulation,[],[f22466,f3144]) ).
fof(f23119,plain,
! [X2,X0,X1] : implies(X0,X2) = implies(implies(implies(X0,X1),X1),implies(implies(X1,X0),X2)),
inference(forward_demodulation,[],[f22943,f6706]) ).
fof(f23120,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X0,X2)) = implies(implies(X1,X0),implies(X1,X2)),
inference(forward_demodulation,[],[f22944,f6968]) ).
fof(f23122,plain,
! [X2,X0,X1] : implies(implies(X1,X0),implies(X1,X2)) = implies(X0,implies(implies(X0,X1),X2)),
inference(forward_demodulation,[],[f22946,f6968]) ).
fof(f23314,plain,
! [X0] : implies(truth,implies(sF15,X0)) = implies(sF11,implies(implies(sF11,sF15),X0)),
inference(superposition,[],[f23122,f13509]) ).
fof(f23395,plain,
! [X0] : implies(X0,implies(implies(X0,x),z)) = implies(implies(x,X0),sF7),
inference(superposition,[],[f23122,f32]) ).
fof(f23402,plain,
! [X0] : implies(X0,implies(implies(X0,y),z)) = implies(implies(y,X0),sF10),
inference(superposition,[],[f23122,f38]) ).
fof(f23444,plain,
! [X0] : implies(X0,implies(implies(X0,sF11),z)) = implies(implies(sF11,X0),sF10),
inference(superposition,[],[f23122,f672]) ).
fof(f23496,plain,
! [X2,X0,X1] : implies(implies(X0,implies(X1,X0)),implies(X0,X2)) = implies(implies(X1,X0),implies(implies(implies(X0,X1),X1),X2)),
inference(superposition,[],[f23122,f4]) ).
fof(f23893,plain,
! [X2,X0,X1] : implies(implies(X1,X0),implies(implies(implies(X0,X1),X1),X2)) = implies(implies(X1,truth),implies(X0,X2)),
inference(forward_demodulation,[],[f23496,f849]) ).
fof(f23972,plain,
! [X0] : implies(truth,implies(sF15,X0)) = implies(sF11,implies(sF13,X0)),
inference(forward_demodulation,[],[f23314,f15305]) ).
fof(f24124,plain,
! [X2,X0,X1] : implies(truth,implies(X0,X2)) = implies(implies(X1,X0),implies(implies(implies(X0,X1),X1),X2)),
inference(forward_demodulation,[],[f23893,f1656]) ).
fof(f24155,plain,
! [X0] : implies(sF15,X0) = implies(sF11,implies(sF13,X0)),
inference(forward_demodulation,[],[f23972,f1]) ).
fof(f24258,plain,
! [X2,X0,X1] : implies(X0,X2) = implies(implies(X1,X0),implies(implies(implies(X0,X1),X1),X2)),
inference(forward_demodulation,[],[f24124,f1]) ).
fof(f27431,plain,
! [X0] : implies(implies(x,X0),sF7) = implies(implies(X0,x),implies(X0,z)),
inference(superposition,[],[f23120,f32]) ).
fof(f27438,plain,
! [X0] : implies(implies(y,X0),sF10) = implies(implies(X0,y),implies(X0,z)),
inference(superposition,[],[f23120,f38]) ).
fof(f31160,plain,
! [X0,X1] : implies(X0,X1) = implies(implies(implies(X0,X1),implies(implies(X1,X0),implies(X0,X1))),implies(implies(X1,X0),implies(X0,X1))),
inference(superposition,[],[f120,f23119]) ).
fof(f31303,plain,
! [X0,X1] : implies(X0,X1) = implies(implies(implies(X1,X0),truth),implies(implies(X1,X0),implies(X0,X1))),
inference(forward_demodulation,[],[f31160,f849]) ).
fof(f31655,plain,
! [X0,X1] : implies(X0,X1) = implies(implies(X1,X0),implies(X0,X1)),
inference(forward_demodulation,[],[f31303,f1632]) ).
fof(f32350,plain,
! [X0,X1] : implies(X0,X1) = implies(X0,implies(implies(X1,X0),X1)),
inference(superposition,[],[f1065,f31655]) ).
fof(f33024,plain,
! [X2,X0,X1] : implies(implies(implies(X1,X0),X0),implies(implies(X0,X1),X2)) = implies(X1,implies(implies(X2,implies(X0,X1)),X2)),
inference(superposition,[],[f23119,f32350]) ).
fof(f33092,plain,
! [X2,X0,X1] : implies(X1,X2) = implies(X1,implies(implies(X2,implies(X0,X1)),X2)),
inference(forward_demodulation,[],[f33024,f23119]) ).
fof(f34826,plain,
! [X2,X0,X1] : implies(X2,X1) = implies(X2,implies(implies(X0,implies(X1,X2)),X1)),
inference(superposition,[],[f33092,f1065]) ).
fof(f37676,plain,
implies(sF11,x) = implies(sF0,sF12),
inference(superposition,[],[f6911,f3154]) ).
fof(f47147,plain,
implies(sF4,sF8) = implies(sF9,sF3),
inference(superposition,[],[f7013,f26]) ).
fof(f47151,plain,
implies(sF9,sF12) = implies(sF11,sF8),
inference(superposition,[],[f7013,f3154]) ).
fof(f47319,plain,
implies(sF9,sF12) = implies(sF7,sF10),
inference(forward_demodulation,[],[f47151,f1453]) ).
fof(f47352,plain,
sF13 = implies(sF7,sF10),
inference(forward_demodulation,[],[f47319,f44]) ).
fof(f58598,plain,
! [X0,X1] : implies(X1,implies(X0,sF12)) = implies(sF11,implies(X1,not(X0))),
inference(superposition,[],[f1065,f6713]) ).
fof(f58775,plain,
implies(sF14,sF3) = implies(sF4,sF15),
inference(superposition,[],[f6903,f48]) ).
fof(f59358,plain,
! [X2,X0,X1] : implies(not(X0),not(X1)) = implies(not(X0),implies(implies(X2,implies(X0,X1)),not(X1))),
inference(superposition,[],[f34826,f6706]) ).
fof(f59955,plain,
! [X2,X0,X1] : implies(not(X0),not(X1)) = implies(implies(X2,implies(X0,X1)),implies(X1,X0)),
inference(forward_demodulation,[],[f59358,f6968]) ).
fof(f60111,plain,
! [X2,X0,X1] : implies(X1,X0) = implies(implies(X2,implies(X0,X1)),implies(X1,X0)),
inference(forward_demodulation,[],[f59955,f6706]) ).
fof(f60911,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = implies(implies(implies(X1,X0),X2),implies(implies(X1,X0),implies(X0,X1))),
inference(superposition,[],[f23122,f60111]) ).
fof(f61098,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = implies(implies(implies(X1,X0),X2),implies(X0,X1)),
inference(forward_demodulation,[],[f60911,f31655]) ).
fof(f66603,plain,
! [X0] : implies(implies(implies(x,X0),X0),sF8) = implies(implies(implies(implies(implies(x,X0),X0),sF8),implies(implies(z,x),implies(X0,x))),implies(implies(z,x),implies(X0,x))),
inference(superposition,[],[f163,f119]) ).
fof(f67889,plain,
! [X0] : implies(implies(implies(x,X0),X0),sF8) = implies(implies(implies(implies(implies(x,X0),X0),sF8),implies(implies(sF8,x),implies(X0,x))),implies(implies(sF8,x),implies(X0,x))),
inference(forward_demodulation,[],[f66603,f646]) ).
fof(f68669,plain,
! [X0] : implies(implies(implies(x,X0),X0),sF8) = implies(implies(implies(implies(implies(x,X0),X0),sF8),implies(X0,sF8)),implies(X0,sF8)),
inference(forward_demodulation,[],[f67889,f830]) ).
fof(f69281,plain,
! [X0] : implies(truth,implies(X0,sF8)) = implies(implies(implies(x,X0),X0),sF8),
inference(forward_demodulation,[],[f68669,f531]) ).
fof(f69565,plain,
! [X0] : implies(X0,sF8) = implies(implies(implies(x,X0),X0),sF8),
inference(forward_demodulation,[],[f69281,f1]) ).
fof(f72301,plain,
implies(sF10,sF13) = implies(sF14,not(z)),
inference(superposition,[],[f832,f11544]) ).
fof(f72510,plain,
implies(sF10,sF13) = implies(z,sF15),
inference(forward_demodulation,[],[f72301,f6715]) ).
fof(f72556,plain,
truth = implies(z,sF15),
inference(forward_demodulation,[],[f72510,f11874]) ).
fof(f72604,plain,
implies(truth,sF15) = implies(implies(implies(truth,sF15),z),z),
inference(superposition,[],[f216,f72556]) ).
fof(f72710,plain,
sF15 = implies(implies(sF15,z),z),
inference(forward_demodulation,[],[f72604,f1]) ).
fof(f72808,plain,
implies(sF11,sF15) = implies(implies(sF15,z),sF10),
inference(superposition,[],[f833,f72710]) ).
fof(f72814,plain,
implies(y,sF15) = implies(implies(sF15,z),sF10),
inference(superposition,[],[f1132,f72710]) ).
fof(f72815,plain,
implies(sF4,sF15) = implies(implies(sF15,z),sF5),
inference(superposition,[],[f1135,f72710]) ).
fof(f72971,plain,
implies(sF14,sF1) = implies(implies(sF15,z),sF10),
inference(forward_demodulation,[],[f72814,f9586]) ).
fof(f72974,plain,
sF13 = implies(implies(sF15,z),sF10),
inference(forward_demodulation,[],[f72808,f15305]) ).
fof(f73046,plain,
sF13 = implies(sF14,sF1),
inference(forward_demodulation,[],[f72974,f72971]) ).
fof(f73107,plain,
implies(sF14,sF3) = implies(sF2,sF13),
inference(superposition,[],[f839,f73046]) ).
fof(f73255,plain,
implies(sF4,sF15) = implies(sF2,sF13),
inference(forward_demodulation,[],[f73107,f58775]) ).
fof(f74719,definition,
( spl16_48
<=> truth = implies(sF2,sF13) ),
introduced(definition,[new_symbols(definition,[spl16_48])],[avatar_definition]) ).
fof(f74720,plain,
( truth = implies(sF2,sF13)
| ~ spl16_48 ),
inference(avatar_component_clause,[],[f74719]) ).
fof(f74721,plain,
( truth != implies(sF2,sF13)
| spl16_48 ),
inference(avatar_component_clause,[],[f74719]) ).
fof(f78918,plain,
implies(implies(sF15,z),sF5) = implies(sF6,sF15),
inference(superposition,[],[f836,f72710]) ).
fof(f79170,plain,
implies(sF4,sF15) = implies(sF6,sF15),
inference(forward_demodulation,[],[f78918,f72815]) ).
fof(f79193,plain,
implies(sF2,sF13) = implies(sF6,sF15),
inference(forward_demodulation,[],[f79170,f73255]) ).
fof(f79439,plain,
! [X0,X1] : implies(X1,implies(X0,sF4)) = implies(sF3,implies(X1,not(X0))),
inference(superposition,[],[f1065,f6711]) ).
fof(f89101,plain,
! [X2,X0,X1] : implies(X0,implies(implies(X1,X2),not(X1))) = implies(X2,implies(implies(X2,X1),not(X0))),
inference(superposition,[],[f23122,f6829]) ).
fof(f108204,plain,
implies(implies(x,y),sF7) = implies(implies(y,x),sF10),
inference(superposition,[],[f1131,f23402]) ).
fof(f108221,plain,
implies(implies(y,sF4),sF10) = implies(implies(sF4,y),sF5),
inference(superposition,[],[f1135,f23402]) ).
fof(f108259,plain,
implies(truth,sF5) = implies(implies(y,sF4),sF10),
inference(forward_demodulation,[],[f108221,f10962]) ).
fof(f108271,plain,
implies(sF2,sF10) = implies(implies(x,y),sF7),
inference(forward_demodulation,[],[f108204,f7288]) ).
fof(f108400,plain,
implies(truth,sF5) = implies(sF2,sF10),
inference(forward_demodulation,[],[f108259,f7652]) ).
fof(f108410,plain,
implies(sF2,sF10) = implies(implies(sF1,sF0),sF7),
inference(forward_demodulation,[],[f108271,f7853]) ).
fof(f108501,plain,
sF5 = implies(sF2,sF10),
inference(forward_demodulation,[],[f108400,f1]) ).
fof(f108899,definition,
( spl16_86
<=> truth = implies(sF4,sF8) ),
introduced(definition,[new_symbols(definition,[spl16_86])],[avatar_definition]) ).
fof(f108900,plain,
( truth = implies(sF4,sF8)
| ~ spl16_86 ),
inference(avatar_component_clause,[],[f108899]) ).
fof(f108901,plain,
( truth != implies(sF4,sF8)
| spl16_86 ),
inference(avatar_component_clause,[],[f108899]) ).
fof(f110972,plain,
implies(implies(sF11,x),sF10) = implies(implies(x,sF11),sF7),
inference(superposition,[],[f833,f23395]) ).
fof(f110981,plain,
implies(implies(sF10,sF7),sF7) = implies(implies(sF11,x),sF10),
inference(forward_demodulation,[],[f110972,f1326]) ).
fof(f111125,plain,
implies(implies(sF10,sF7),sF7) = implies(implies(sF0,sF12),sF10),
inference(forward_demodulation,[],[f110981,f37676]) ).
fof(f111228,plain,
implies(implies(sF8,sF11),sF7) = implies(implies(sF0,sF12),sF10),
inference(forward_demodulation,[],[f111125,f1510]) ).
fof(f111295,plain,
implies(implies(sF12,sF0),sF7) = implies(implies(sF0,sF12),sF10),
inference(forward_demodulation,[],[f111228,f7922]) ).
fof(f112622,plain,
! [X0] : implies(X0,implies(truth,not(y))) = implies(sF11,implies(implies(sF11,y),not(X0))),
inference(superposition,[],[f89101,f332]) ).
fof(f112632,plain,
! [X0] : implies(X0,implies(truth,not(sF0))) = implies(sF3,implies(implies(sF3,sF0),not(X0))),
inference(superposition,[],[f89101,f331]) ).
fof(f114359,plain,
! [X0] : implies(X0,implies(truth,not(sF0))) = implies(implies(sF3,sF0),implies(X0,sF4)),
inference(forward_demodulation,[],[f112632,f79439]) ).
fof(f114369,plain,
! [X0] : implies(X0,implies(truth,not(y))) = implies(implies(sF11,y),implies(X0,sF12)),
inference(forward_demodulation,[],[f112622,f58598]) ).
fof(f114959,plain,
! [X0] : implies(X0,implies(truth,not(sF0))) = implies(implies(sF1,sF0),implies(X0,sF4)),
inference(forward_demodulation,[],[f114359,f3306]) ).
fof(f114968,plain,
! [X0] : implies(X0,implies(truth,not(y))) = implies(implies(sF1,sF12),implies(X0,sF12)),
inference(forward_demodulation,[],[f114369,f15452]) ).
fof(f115379,plain,
! [X0] : implies(X0,not(sF0)) = implies(implies(sF1,sF0),implies(X0,sF4)),
inference(forward_demodulation,[],[f114959,f1]) ).
fof(f115386,plain,
! [X0] : implies(X0,not(y)) = implies(implies(sF1,sF12),implies(X0,sF12)),
inference(forward_demodulation,[],[f114968,f1]) ).
fof(f115605,plain,
! [X0] : implies(X0,x) = implies(implies(sF1,sF0),implies(X0,sF4)),
inference(forward_demodulation,[],[f115379,f3150]) ).
fof(f115609,plain,
! [X0] : implies(X0,sF1) = implies(implies(sF1,sF12),implies(X0,sF12)),
inference(forward_demodulation,[],[f115386,f20]) ).
fof(f118220,plain,
! [X0] : implies(implies(implies(sF4,X0),X0),x) = implies(implies(implies(implies(implies(sF4,X0),X0),x),implies(implies(sF1,sF0),implies(X0,sF4))),implies(implies(sF1,sF0),implies(X0,sF4))),
inference(superposition,[],[f163,f10892]) ).
fof(f118388,plain,
! [X0] : implies(implies(implies(sF4,X0),X0),x) = implies(implies(implies(implies(implies(sF4,X0),X0),x),implies(X0,x)),implies(X0,x)),
inference(forward_demodulation,[],[f118220,f115605]) ).
fof(f118464,plain,
! [X0] : implies(truth,implies(X0,x)) = implies(implies(implies(sF4,X0),X0),x),
inference(forward_demodulation,[],[f118388,f531]) ).
fof(f118503,plain,
! [X0] : implies(X0,x) = implies(implies(implies(sF4,X0),X0),x),
inference(forward_demodulation,[],[f118464,f1]) ).
fof(f118536,plain,
implies(z,x) = implies(implies(sF5,z),x),
inference(superposition,[],[f118503,f28]) ).
fof(f118903,plain,
implies(z,x) = implies(sF6,x),
inference(forward_demodulation,[],[f118536,f30]) ).
fof(f118976,plain,
implies(sF8,x) = implies(sF6,x),
inference(forward_demodulation,[],[f118903,f646]) ).
fof(f119021,plain,
implies(sF0,sF9) = implies(sF6,x),
inference(forward_demodulation,[],[f118976,f15453]) ).
fof(f119084,plain,
truth = implies(implies(not(sF6),not(implies(x,sF6))),implies(implies(sF0,sF9),x)),
inference(superposition,[],[f117,f119021]) ).
fof(f119257,plain,
truth = implies(implies(not(sF6),not(implies(x,sF6))),sF8),
inference(forward_demodulation,[],[f119084,f11722]) ).
fof(f119315,plain,
truth = implies(implies(implies(x,sF6),sF6),sF8),
inference(forward_demodulation,[],[f119257,f6706]) ).
fof(f119339,plain,
truth = implies(sF6,sF8),
inference(forward_demodulation,[],[f119315,f69565]) ).
fof(f119346,plain,
truth = implies(sF7,sF5),
inference(forward_demodulation,[],[f119339,f1450]) ).
fof(f119350,plain,
truth = implies(sF4,sF8),
inference(forward_demodulation,[],[f119346,f1448]) ).
fof(f119352,plain,
( $false
| spl16_86 ),
inference(forward_subsumption_resolution,[],[f119350,f108901]) ).
fof(f119353,plain,
spl16_86,
inference(avatar_contradiction_clause,[],[f119352]) ).
fof(f119994,plain,
! [X0] : implies(implies(implies(sF12,X0),X0),sF1) = implies(implies(implies(implies(implies(sF12,X0),X0),sF1),implies(implies(sF11,y),implies(X0,sF12))),implies(implies(sF11,y),implies(X0,sF12))),
inference(superposition,[],[f163,f10902]) ).
fof(f120183,plain,
! [X0] : implies(implies(implies(sF12,X0),X0),sF1) = implies(implies(implies(implies(implies(sF12,X0),X0),sF1),implies(implies(sF1,sF12),implies(X0,sF12))),implies(implies(sF1,sF12),implies(X0,sF12))),
inference(forward_demodulation,[],[f119994,f15452]) ).
fof(f120268,plain,
! [X0] : implies(implies(implies(sF12,X0),X0),sF1) = implies(implies(implies(implies(implies(sF12,X0),X0),sF1),implies(X0,sF1)),implies(X0,sF1)),
inference(forward_demodulation,[],[f120183,f115609]) ).
fof(f120336,plain,
! [X0] : implies(truth,implies(X0,sF1)) = implies(implies(implies(sF12,X0),X0),sF1),
inference(forward_demodulation,[],[f120268,f531]) ).
fof(f120371,plain,
! [X0] : implies(X0,sF1) = implies(implies(implies(sF12,X0),X0),sF1),
inference(forward_demodulation,[],[f120336,f1]) ).
fof(f120504,plain,
! [X0] : implies(sF2,implies(X0,sF1)) = implies(implies(implies(sF12,X0),X0),sF3),
inference(superposition,[],[f839,f120371]) ).
fof(f120674,plain,
! [X0] : implies(X0,sF3) = implies(implies(implies(sF12,X0),X0),sF3),
inference(forward_demodulation,[],[f120504,f839]) ).
fof(f120951,plain,
implies(sF9,sF3) = implies(sF14,sF3),
inference(superposition,[],[f120674,f152]) ).
fof(f121225,plain,
implies(sF9,sF3) = implies(sF4,sF15),
inference(forward_demodulation,[],[f120951,f58775]) ).
fof(f121307,plain,
implies(sF9,sF3) = implies(sF2,sF13),
inference(forward_demodulation,[],[f121225,f73255]) ).
fof(f121352,plain,
implies(sF4,sF8) = implies(sF2,sF13),
inference(forward_demodulation,[],[f121307,f47147]) ).
fof(f121385,plain,
( truth = implies(sF2,sF13)
| ~ spl16_86 ),
inference(forward_demodulation,[],[f121352,f108900]) ).
fof(f121401,plain,
( $false
| spl16_48
| ~ spl16_86 ),
inference(forward_subsumption_resolution,[],[f121385,f74721]) ).
fof(f121402,plain,
( spl16_48
| ~ spl16_86 ),
inference(avatar_contradiction_clause,[],[f121401]) ).
fof(f173695,plain,
! [X0] : implies(implies(implies(X0,z),sF10),sF10) = implies(X0,implies(implies(X0,sF11),z)),
inference(superposition,[],[f1240,f840]) ).
fof(f175526,plain,
! [X0] : implies(implies(implies(X0,z),sF10),sF10) = implies(implies(sF11,X0),sF10),
inference(forward_demodulation,[],[f173695,f23444]) ).
fof(f204721,plain,
! [X0] : implies(X0,implies(sF13,sF10)) = implies(implies(sF10,sF7),implies(X0,sF7)),
inference(superposition,[],[f741,f47352]) ).
fof(f207278,plain,
! [X0] : implies(X0,implies(sF13,sF10)) = implies(implies(sF8,sF11),implies(X0,sF7)),
inference(forward_demodulation,[],[f204721,f1510]) ).
fof(f207718,plain,
! [X0] : implies(X0,implies(sF13,sF10)) = implies(implies(sF12,sF0),implies(X0,sF7)),
inference(forward_demodulation,[],[f207278,f7922]) ).
fof(f347705,plain,
! [X2,X0,X1] : implies(implies(X0,X1),implies(X0,X2)) = implies(implies(implies(implies(X0,X2),X2),X1),implies(X0,X2)),
inference(superposition,[],[f61098,f24258]) ).
fof(f452345,plain,
implies(sF13,sF10) = implies(sF15,z),
inference(superposition,[],[f833,f24155]) ).
fof(f452949,plain,
implies(sF15,sF6) = implies(sF5,implies(sF13,sF10)),
inference(superposition,[],[f837,f452345]) ).
fof(f462672,plain,
! [X0] : implies(implies(y,implies(implies(X0,z),z)),sF10) = implies(implies(implies(implies(X0,z),z),y),implies(X0,z)),
inference(superposition,[],[f27438,f592]) ).
fof(f463243,plain,
! [X0] : implies(implies(X0,y),implies(X0,z)) = implies(implies(y,implies(implies(X0,z),z)),sF10),
inference(forward_demodulation,[],[f462672,f347705]) ).
fof(f463395,plain,
! [X0] : implies(implies(implies(X0,z),sF10),sF10) = implies(implies(X0,y),implies(X0,z)),
inference(forward_demodulation,[],[f463243,f699]) ).
fof(f463501,plain,
! [X0] : implies(implies(implies(X0,z),sF10),sF10) = implies(implies(y,X0),sF10),
inference(forward_demodulation,[],[f463395,f27438]) ).
fof(f463552,plain,
! [X0] : implies(implies(y,X0),sF10) = implies(implies(sF11,X0),sF10),
inference(forward_demodulation,[],[f463501,f175526]) ).
fof(f464547,plain,
implies(implies(x,y),sF7) = implies(implies(y,x),sF10),
inference(superposition,[],[f27431,f38]) ).
fof(f465080,plain,
implies(implies(x,y),sF7) = implies(implies(sF11,x),sF10),
inference(forward_demodulation,[],[f464547,f463552]) ).
fof(f465239,plain,
implies(implies(x,y),sF7) = implies(implies(sF0,sF12),sF10),
inference(forward_demodulation,[],[f465080,f37676]) ).
fof(f465346,plain,
implies(implies(sF12,sF0),sF7) = implies(implies(x,y),sF7),
inference(forward_demodulation,[],[f465239,f111295]) ).
fof(f465405,plain,
implies(implies(sF12,sF0),sF7) = implies(implies(sF1,sF0),sF7),
inference(forward_demodulation,[],[f465346,f7853]) ).
fof(f465437,plain,
implies(implies(sF12,sF0),sF7) = implies(sF2,sF10),
inference(forward_demodulation,[],[f465405,f108410]) ).
fof(f465451,plain,
sF5 = implies(implies(sF12,sF0),sF7),
inference(forward_demodulation,[],[f465437,f108501]) ).
fof(f465500,plain,
truth = implies(implies(sF12,sF0),implies(sF5,sF7)),
inference(superposition,[],[f68,f465451]) ).
fof(f465842,plain,
truth = implies(sF5,implies(sF13,sF10)),
inference(forward_demodulation,[],[f465500,f207718]) ).
fof(f465957,plain,
truth = implies(sF15,sF6),
inference(forward_demodulation,[],[f465842,f452949]) ).
fof(f466149,plain,
sF6 = implies(implies(truth,not(sF15)),not(implies(sF6,sF15))),
inference(superposition,[],[f10802,f465957]) ).
fof(f466369,plain,
sF6 = implies(implies(truth,not(sF15)),not(implies(sF2,sF13))),
inference(forward_demodulation,[],[f466149,f79193]) ).
fof(f466526,plain,
( sF6 = implies(implies(truth,not(sF15)),not(truth))
| ~ spl16_48 ),
inference(forward_demodulation,[],[f466369,f74720]) ).
fof(f466627,plain,
( sF6 = not(implies(truth,not(sF15)))
| ~ spl16_48 ),
inference(forward_demodulation,[],[f466526,f6585]) ).
fof(f466697,plain,
( sF6 = not(not(sF15))
| ~ spl16_48 ),
inference(forward_demodulation,[],[f466627,f1]) ).
fof(f466730,plain,
( sF6 = sF15
| ~ spl16_48 ),
inference(forward_demodulation,[],[f466697,f3144]) ).
fof(f466751,plain,
( $false
| ~ spl16_48 ),
inference(forward_subsumption_resolution,[],[f466730,f49]) ).
fof(f466752,plain,
~ spl16_48,
inference(avatar_contradiction_clause,[],[f466751]) ).
cnf(s58,plain,
spl16_86,
inference(sat_conversion,[],[f119353]) ).
cnf(s61,plain,
( spl16_48
| ~ spl16_86 ),
inference(sat_conversion,[],[f121402]) ).
cnf(s95,plain,
~ spl16_48,
inference(sat_conversion,[],[f466752]) ).
cnf(s96,plain,
~ spl16_86,
inference(rat,[],[s61,s95]) ).
cnf(s97,plain,
$false,
inference(rat,[],[s58,s96]) ).
fof(f466760,plain,
$false,
inference(avatar_sat_refutation,[],[s97]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL151-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n011.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 15:24:00 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.85/2.29 % (2547209)Input is clausal, will run a generic CNF schedule.
% 9.85/2.29 % (2547218)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3826253349:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.85/2.29 % (2547216)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3005988610:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.85/2.29 % (2547215)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2992630727:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.85/2.29 % (2547217)lrs+10_1_sil=8000:sp=occurrence:random_seed=2805614154:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.85/2.29 % (2547214)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=815513823:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.85/2.29 % (2547218)Instruction limit reached!
% 9.85/2.29 % (2547218)------------------------------
% 9.85/2.29 % (2547218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.85/2.29 % (2547218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/2.29 % (2547218)CaDiCaL version: 2.1.3
% 9.85/2.29 % (2547218)Termination reason: Instruction limit
% 9.85/2.29 % (2547218)Termination phase: Saturation
% 9.85/2.29 % (2547218)Time elapsed: 0.040 s
% 9.85/2.29 % (2547218)Peak memory usage: 89 MB
% 9.85/2.29 % (2547218)Instructions burned: 117 (million)
% 9.85/2.29 % (2547219)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3687494266:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.85/2.29 % (2547220)dis-21_1_sil=8000:lcm=predicate:random_seed=2031086970: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)
% 9.85/2.29 % (2547220)Refutation not found, incomplete strategy
% 9.85/2.29 % (2547220)------------------------------
% 9.85/2.29 % (2547220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.85/2.29 % (2547220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/2.29 % (2547220)CaDiCaL version: 2.1.3
% 9.85/2.29 % (2547220)Termination reason: Refutation not found, incomplete strategy
% 9.85/2.29 % (2547220)Time elapsed: 0.001 s
% 9.85/2.29 % (2547220)Peak memory usage: 88 MB
% 9.85/2.29 % (2547220)Instructions burned: 1 (million)
% 9.85/2.29 % (2547219)Instruction limit reached!
% 9.85/2.29 % (2547219)------------------------------
% 9.85/2.29 % (2547219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.85/2.29 % (2547219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/2.29 % (2547219)CaDiCaL version: 2.1.3
% 9.85/2.29 % (2547219)Termination reason: Instruction limit
% 9.85/2.29 % (2547219)Termination phase: Saturation
% 9.85/2.29 % (2547219)Time elapsed: 0.057 s
% 9.85/2.29 % (2547219)Peak memory usage: 90 MB
% 9.85/2.29 % (2547219)Instructions burned: 181 (million)
% 9.85/2.29 % (2547217)Instruction limit reached!
% 9.85/2.29 % (2547217)------------------------------
% 9.85/2.29 % (2547217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.85/2.29 % (2547217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/2.29 % (2547217)CaDiCaL version: 2.1.3
% 9.85/2.29 % (2547217)Termination reason: Instruction limit
% 9.85/2.29 % (2547217)Termination phase: Saturation
% 9.85/2.29 % (2547217)Time elapsed: 0.064 s
% 9.85/2.29 % (2547217)Peak memory usage: 89 MB
% 9.85/2.29 % (2547217)Instructions burned: 107 (million)
% 9.85/2.29 % (2547228)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=4050039396:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.85/2.29 % (2547228)Refutation not found, incomplete strategy
% 9.85/2.29 % (2547228)------------------------------
% 9.85/2.29 % (2547228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.85/2.29 % (2547228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/2.29 % (2547228)CaDiCaL version: 2.1.3
% 9.85/2.29 % (2547228)Termination reason: Refutation not found, incomplete strategy
% 9.85/2.29 % (2547228)Time elapsed: 0.001 s
% 9.85/2.29 % (2547228)Peak memory usage: 88 MB
% 9.85/2.29 % (2547229)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=959996003: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)
% 18.79/3.56 % (2547229)Refutation not found, incomplete strategy
% 18.79/3.56 % (2547229)------------------------------
% 18.79/3.56 % (2547229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.79/3.56 % (2547229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.79/3.56 % (2547229)CaDiCaL version: 2.1.3
% 18.79/3.56 % (2547229)Termination reason: Refutation not found, incomplete strategy
% 18.79/3.56 % (2547229)Time elapsed: 0.001 s
% 18.79/3.56 % (2547229)Peak memory usage: 88 MB
% 18.79/3.56 % (2547229)Instructions burned: 1 (million)
% 18.79/3.56 % (2547230)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=193285473:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 18.79/3.56 % (2547220)------------------------------
% 18.79/3.56 % (2547220)------------------------------
% 18.79/3.56 % (2547229)------------------------------
% 18.79/3.56 % (2547229)------------------------------
% 18.79/3.56 % (2547230)Instruction limit reached!
% 18.79/3.56 % (2547230)------------------------------
% 18.79/3.56 % (2547230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.79/3.56 % (2547230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.79/3.56 % (2547230)CaDiCaL version: 2.1.3
% 18.79/3.56 % (2547230)Termination reason: Instruction limit
% 18.79/3.56 % (2547230)Termination phase: Saturation
% 18.79/3.56 % (2547230)Time elapsed: 0.135 s
% 18.79/3.56 % (2547230)Peak memory usage: 90 MB
% 18.79/3.56 % (2547230)Instructions burned: 220 (million)
% 18.79/3.56 % (2547228)------------------------------
% 18.79/3.56 % (2547228)------------------------------
% 18.79/3.56 % (2547234)lrs+10_64_to=lpo:sil=8000:random_seed=142473822:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 18.79/3.56 % (2547235)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=692383027:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 18.79/3.56 % (2547236)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3753072135:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 18.79/3.56 % (2547235)Instruction limit reached!
% 18.79/3.56 % (2547235)------------------------------
% 18.79/3.56 % (2547235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.79/3.56 % (2547235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.79/3.56 % (2547235)CaDiCaL version: 2.1.3
% 18.79/3.56 % (2547235)Termination reason: Instruction limit
% 18.79/3.56 % (2547235)Termination phase: Saturation
% 18.79/3.56 % (2547235)Time elapsed: 0.066 s
% 18.79/3.56 % (2547235)Peak memory usage: 90 MB
% 18.79/3.56 % (2547235)Instructions burned: 196 (million)
% 18.79/3.56 % (2547234)Instruction limit reached!
% 18.79/3.56 % (2547234)------------------------------
% 18.79/3.56 % (2547234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.79/3.56 % (2547234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.79/3.56 % (2547234)CaDiCaL version: 2.1.3
% 18.79/3.56 % (2547234)Termination reason: Instruction limit
% 18.79/3.56 % (2547234)Termination phase: Saturation
% 18.79/3.56 % (2547234)Time elapsed: 0.080 s
% 18.79/3.56 % (2547234)Peak memory usage: 89 MB
% 18.79/3.56 % (2547234)Instructions burned: 127 (million)
% 18.79/3.56 % (2547238)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2823350094:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 18.79/3.56 % (2547236)Instruction limit reached!
% 18.79/3.56 % (2547236)------------------------------
% 18.79/3.56 % (2547236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.79/3.56 % (2547236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.79/3.56 % (2547236)CaDiCaL version: 2.1.3
% 18.79/3.56 % (2547236)Termination reason: Instruction limit
% 18.79/3.56 % (2547236)Termination phase: Saturation
% 18.79/3.56 % (2547236)Time elapsed: 0.102 s
% 18.79/3.56 % (2547236)Peak memory usage: 92 MB
% 18.79/3.56 % (2547236)Instructions burned: 158 (million)
% 18.79/3.56 % (2547241)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=2727187831:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 18.79/3.56 % (2547242)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3602376707:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 27.84/4.81 % (2547242)Refutation not found, incomplete strategy
% 27.84/4.81 % (2547242)------------------------------
% 27.84/4.81 % (2547242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/4.81 % (2547242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/4.81 % (2547242)CaDiCaL version: 2.1.3
% 27.84/4.81 % (2547242)Termination reason: Refutation not found, incomplete strategy
% 27.84/4.81 % (2547242)Time elapsed: 0.001 s
% 27.84/4.81 % (2547242)Peak memory usage: 88 MB
% 27.84/4.81 % (2547242)Instructions burned: 1 (million)
% 27.84/4.81 % (2547241)Instruction limit reached!
% 27.84/4.81 % (2547241)------------------------------
% 27.84/4.81 % (2547241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/4.81 % (2547241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/4.81 % (2547241)CaDiCaL version: 2.1.3
% 27.84/4.81 % (2547241)Termination reason: Instruction limit
% 27.84/4.81 % (2547241)Termination phase: Saturation
% 27.84/4.81 % (2547241)Time elapsed: 0.036 s
% 27.84/4.81 % (2547241)Peak memory usage: 88 MB
% 27.84/4.81 % (2547241)Instructions burned: 108 (million)
% 27.84/4.81 % (2547244)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1973181325:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 27.84/4.81 % (2547247)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3172020462:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 27.84/4.81 % (2547242)------------------------------
% 27.84/4.81 % (2547242)------------------------------
% 27.84/4.81 % (2547244)Instruction limit reached!
% 27.84/4.81 % (2547244)------------------------------
% 27.84/4.81 % (2547244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/4.81 % (2547244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/4.81 % (2547244)CaDiCaL version: 2.1.3
% 27.84/4.81 % (2547244)Termination reason: Instruction limit
% 27.84/4.81 % (2547244)Termination phase: Saturation
% 27.84/4.81 % (2547244)Time elapsed: 0.136 s
% 27.84/4.81 % (2547244)Peak memory usage: 90 MB
% 27.84/4.81 % (2547244)Instructions burned: 242 (million)
% 27.84/4.81 % (2547251)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1522911123:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 27.84/4.81 % (2547250)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3168087172:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 27.84/4.81 % (2547250)Instruction limit reached!
% 27.84/4.81 % (2547250)------------------------------
% 27.84/4.81 % (2547250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/4.81 % (2547250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/4.81 % (2547250)CaDiCaL version: 2.1.3
% 27.84/4.81 % (2547250)Termination reason: Instruction limit
% 27.84/4.81 % (2547250)Termination phase: Saturation
% 27.84/4.81 % (2547250)Time elapsed: 0.078 s
% 27.84/4.81 % (2547250)Peak memory usage: 89 MB
% 27.84/4.81 % (2547250)Instructions burned: 134 (million)
% 27.84/4.81 % (2547254)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4149292779:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 27.84/4.81 % (2547251)Instruction limit reached!
% 27.84/4.81 % (2547251)------------------------------
% 27.84/4.81 % (2547251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/4.81 % (2547251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/4.81 % (2547251)CaDiCaL version: 2.1.3
% 27.84/4.81 % (2547251)Termination reason: Instruction limit
% 27.84/4.81 % (2547251)Termination phase: Saturation
% 27.84/4.81 % (2547251)Time elapsed: 0.304 s
% 27.84/4.81 % (2547251)Peak memory usage: 93 MB
% 27.84/4.81 % (2547251)Instructions burned: 499 (million)
% 27.84/4.81 % (2547254)Instruction limit reached!
% 27.84/4.81 % (2547254)------------------------------
% 27.84/4.81 % (2547254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/4.81 % (2547254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/4.81 % (2547254)CaDiCaL version: 2.1.3
% 27.84/4.81 % (2547254)Termination reason: Instruction limit
% 27.84/4.81 % (2547254)Termination phase: Saturation
% 27.84/4.81 % (2547254)Time elapsed: 0.124 s
% 27.84/4.81 % (2547254)Peak memory usage: 92 MB
% 47.55/7.55 % (2547254)Instructions burned: 192 (million)
% 47.55/7.55 % (2547256)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3493008055:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 47.55/7.55 % (2547257)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2712021224:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 47.55/7.55 % (2547257)Instruction limit reached!
% 47.55/7.55 % (2547257)------------------------------
% 47.55/7.55 % (2547257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.55/7.55 % (2547257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.55/7.55 % (2547257)CaDiCaL version: 2.1.3
% 47.55/7.55 % (2547257)Termination reason: Instruction limit
% 47.55/7.55 % (2547257)Termination phase: Saturation
% 47.55/7.55 % (2547257)Time elapsed: 0.094 s
% 47.55/7.55 % (2547257)Peak memory usage: 89 MB
% 47.55/7.55 % (2547257)Instructions burned: 156 (million)
% 47.55/7.55 % (2547256)Instruction limit reached!
% 47.55/7.55 % (2547256)------------------------------
% 47.55/7.55 % (2547256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.55/7.55 % (2547256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.55/7.55 % (2547256)CaDiCaL version: 2.1.3
% 47.55/7.55 % (2547256)Termination reason: Instruction limit
% 47.55/7.55 % (2547256)Termination phase: Saturation
% 47.55/7.55 % (2547256)Time elapsed: 0.170 s
% 47.55/7.55 % (2547256)Peak memory usage: 93 MB
% 47.55/7.55 % (2547256)Instructions burned: 264 (million)
% 47.55/7.55 % (2547260)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=2683180656:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 47.55/7.55 % (2547261)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2258414679:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 47.55/7.55 % (2547261)Instruction limit reached!
% 47.55/7.55 % (2547261)------------------------------
% 47.55/7.55 % (2547261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.55/7.55 % (2547261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.55/7.55 % (2547261)CaDiCaL version: 2.1.3
% 47.55/7.55 % (2547261)Termination reason: Instruction limit
% 47.55/7.55 % (2547261)Termination phase: Saturation
% 47.55/7.55 % (2547261)Time elapsed: 0.286 s
% 47.55/7.55 % (2547261)Peak memory usage: 95 MB
% 47.55/7.55 % (2547261)Instructions burned: 539 (million)
% 47.55/7.55 % (2547264)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2278422471:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi)
% 47.55/7.55 % (2547264)Instruction limit reached!
% 47.55/7.55 % (2547264)------------------------------
% 47.55/7.55 % (2547264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.55/7.55 % (2547264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.55/7.55 % (2547264)CaDiCaL version: 2.1.3
% 47.55/7.55 % (2547264)Termination reason: Instruction limit
% 47.55/7.55 % (2547264)Termination phase: Saturation
% 47.55/7.55 % (2547264)Time elapsed: 0.100 s
% 47.55/7.55 % (2547264)Peak memory usage: 89 MB
% 47.55/7.55 % (2547264)Instructions burned: 181 (million)
% 47.55/7.55 % (2547247)Instruction limit reached!
% 47.55/7.55 % (2547247)------------------------------
% 47.55/7.55 % (2547247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.55/7.55 % (2547247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.55/7.55 % (2547247)CaDiCaL version: 2.1.3
% 47.55/7.55 % (2547247)Termination reason: Instruction limit
% 47.55/7.55 % (2547247)Termination phase: Saturation
% 47.55/7.55 % (2547247)Time elapsed: 1.619 s
% 47.55/7.55 % (2547247)Peak memory usage: 171 MB
% 47.55/7.55 % (2547247)Instructions burned: 5208 (million)
% 47.55/7.55 % (2547266)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=174541031:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2976 on theBenchmark for (2976ds/10307Mi)
% 47.55/7.55 % (2547267)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=2644560869:i=412:gtgl=4:gtg=exists_all_2974 on theBenchmark for (2974ds/412Mi)
% 47.55/7.55 % (2547267)Instruction limit reached!
% 47.55/7.55 % (2547267)------------------------------
% 47.55/7.55 % (2547267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.50/10.11 % (2547267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.50/10.11 % (2547267)CaDiCaL version: 2.1.3
% 65.50/10.11 % (2547267)Termination reason: Instruction limit
% 65.50/10.11 % (2547267)Termination phase: Saturation
% 65.50/10.11 % (2547267)Time elapsed: 0.127 s
% 65.50/10.11 % (2547267)Peak memory usage: 97 MB
% 65.50/10.11 % (2547267)Instructions burned: 413 (million)
% 65.50/10.11 % (2547238)Instruction limit reached!
% 65.50/10.11 % (2547238)------------------------------
% 65.50/10.11 % (2547238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.50/10.11 % (2547238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.50/10.11 % (2547238)CaDiCaL version: 2.1.3
% 65.50/10.11 % (2547238)Termination reason: Instruction limit
% 65.50/10.11 % (2547238)Termination phase: Saturation
% 65.50/10.11 % (2547238)Time elapsed: 2.067 s
% 65.50/10.11 % (2547238)Peak memory usage: 151 MB
% 65.50/10.11 % (2547238)Instructions burned: 3394 (million)
% 65.50/10.11 % (2547270)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=988610541:s2pl=no:i=8478:s2at=4:nm=6_2972 on theBenchmark for (2972ds/8478Mi)
% 65.50/10.11 % (2547271)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=72957947:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2972 on theBenchmark for (2972ds/303Mi)
% 65.50/10.11 % (2547271)Refutation not found, incomplete strategy
% 65.50/10.11 % (2547271)------------------------------
% 65.50/10.11 % (2547271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.50/10.11 % (2547271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.50/10.11 % (2547271)CaDiCaL version: 2.1.3
% 65.50/10.11 % (2547271)Termination reason: Refutation not found, incomplete strategy
% 65.50/10.11 % (2547271)Time elapsed: 0.001 s
% 65.50/10.11 % (2547271)Peak memory usage: 88 MB
% 65.50/10.11 % (2547271)------------------------------
% 65.50/10.11 % (2547271)------------------------------
% 65.50/10.11 % (2547274)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2693966899:st=4:i=720:sd=3:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/720Mi)
% 65.50/10.11 % (2547274)Refutation not found, incomplete strategy
% 65.50/10.11 % (2547274)------------------------------
% 65.50/10.11 % (2547274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.50/10.11 % (2547274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.50/10.11 % (2547274)CaDiCaL version: 2.1.3
% 65.50/10.11 % (2547274)Termination reason: Refutation not found, incomplete strategy
% 65.50/10.11 % (2547274)Time elapsed: 0.001 s
% 65.50/10.11 % (2547274)Peak memory usage: 88 MB
% 65.50/10.11 % (2547274)Instructions burned: 1 (million)
% 65.50/10.11 % (2547274)------------------------------
% 65.50/10.11 % (2547274)------------------------------
% 65.50/10.11 % (2547276)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2335222306:i=598:bs=on:bd=preordered:av=off:ss=axioms_2965 on theBenchmark for (2965ds/598Mi)
% 65.50/10.11 % (2547260)Instruction limit reached!
% 65.50/10.11 % (2547260)------------------------------
% 65.50/10.11 % (2547260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.50/10.11 % (2547260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.50/10.11 % (2547260)CaDiCaL version: 2.1.3
% 65.50/10.11 % (2547260)Termination reason: Instruction limit
% 65.50/10.11 % (2547260)Termination phase: Saturation
% 65.50/10.11 % (2547260)Time elapsed: 2.022 s
% 65.50/10.11 % (2547260)Peak memory usage: 148 MB
% 65.50/10.11 % (2547260)Instructions burned: 3256 (million)
% 65.50/10.11 % (2547278)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2865751003:i=2989:sd=3:ss=axioms:sgt=60_2961 on theBenchmark for (2961ds/2989Mi)
% 65.50/10.11 % (2547276)Instruction limit reached!
% 65.50/10.11 % (2547276)------------------------------
% 65.50/10.11 % (2547276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.50/10.11 % (2547276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.50/10.11 % (2547276)CaDiCaL version: 2.1.3
% 65.50/10.11 % (2547276)Termination reason: Instruction limit
% 65.50/10.11 % (2547276)Termination phase: Saturation
% 65.50/10.11 % (2547276)Time elapsed: 0.335 s
% 65.50/10.11 % (2547276)Peak memory usage: 95 MB
% 95.33/14.31 % (2547276)Instructions burned: 600 (million)
% 95.33/14.31 % (2547280)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=954700051:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2960 on theBenchmark for (2960ds/1997Mi)
% 95.33/14.31 % (2547280)Instruction limit reached!
% 95.33/14.31 % (2547280)------------------------------
% 95.33/14.31 % (2547280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.33/14.31 % (2547280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.33/14.31 % (2547280)CaDiCaL version: 2.1.3
% 95.33/14.31 % (2547280)Termination reason: Instruction limit
% 95.33/14.31 % (2547280)Termination phase: Saturation
% 95.33/14.31 % (2547280)Time elapsed: 1.191 s
% 95.33/14.31 % (2547280)Peak memory usage: 140 MB
% 95.33/14.31 % (2547280)Instructions burned: 1998 (million)
% 95.33/14.31 % (2547282)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=774355090:i=2088:bd=preordered:av=off_2947 on theBenchmark for (2947ds/2088Mi)
% 95.33/14.31 % (2547270)Instruction limit reached!
% 95.33/14.31 % (2547270)------------------------------
% 95.33/14.31 % (2547270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.33/14.31 % (2547270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.33/14.31 % (2547270)CaDiCaL version: 2.1.3
% 95.33/14.31 % (2547270)Termination reason: Instruction limit
% 95.33/14.31 % (2547270)Termination phase: Saturation
% 95.33/14.31 % (2547270)Time elapsed: 2.833 s
% 95.33/14.31 % (2547270)Peak memory usage: 205 MB
% 95.33/14.31 % (2547270)Instructions burned: 8480 (million)
% 95.33/14.31 % (2547278)Instruction limit reached!
% 95.33/14.31 % (2547278)------------------------------
% 95.33/14.31 % (2547278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.33/14.31 % (2547278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.33/14.31 % (2547278)CaDiCaL version: 2.1.3
% 95.33/14.31 % (2547278)Termination reason: Instruction limit
% 95.33/14.31 % (2547278)Termination phase: Saturation
% 95.33/14.31 % (2547278)Time elapsed: 1.701 s
% 95.33/14.31 % (2547278)Peak memory usage: 149 MB
% 95.33/14.31 % (2547278)Instructions burned: 2991 (million)
% 95.33/14.31 % (2547284)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=970447301:i=1098:nicw=on_2943 on theBenchmark for (2943ds/1098Mi)
% 95.33/14.31 % (2547285)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1764170566:i=433:bd=preordered_2943 on theBenchmark for (2943ds/433Mi)
% 95.33/14.31 % (2547285)Refutation not found, incomplete strategy
% 95.33/14.31 % (2547285)------------------------------
% 95.33/14.31 % (2547285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.33/14.31 % (2547285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.33/14.31 % (2547285)CaDiCaL version: 2.1.3
% 95.33/14.31 % (2547285)Termination reason: Refutation not found, incomplete strategy
% 95.33/14.31 % (2547285)Time elapsed: 0.002 s
% 95.33/14.31 % (2547285)Peak memory usage: 88 MB
% 95.33/14.31 % (2547285)Instructions burned: 1 (million)
% 95.33/14.31 % (2547285)------------------------------
% 95.33/14.31 % (2547285)------------------------------
% 95.33/14.31 % (2547284)Instruction limit reached!
% 95.33/14.31 % (2547284)------------------------------
% 95.33/14.31 % (2547284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.33/14.31 % (2547284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.33/14.31 % (2547284)CaDiCaL version: 2.1.3
% 95.33/14.31 % (2547284)Termination reason: Instruction limit
% 95.33/14.31 % (2547284)Termination phase: Saturation
% 95.33/14.31 % (2547284)Time elapsed: 0.376 s
% 95.33/14.31 % (2547284)Peak memory usage: 101 MB
% 95.33/14.31 % (2547284)Instructions burned: 1100 (million)
% 95.33/14.31 % (2547288)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=796137010:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2939 on theBenchmark for (2939ds/2942Mi)
% 95.33/14.31 % (2547289)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=149209590:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2938 on theBenchmark for (2938ds/6922Mi)
% 95.33/14.31 % (2547282)Instruction limit reached!
% 110.37/16.41 % (2547282)------------------------------
% 110.37/16.41 % (2547282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.37/16.41 % (2547282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.37/16.41 % (2547282)CaDiCaL version: 2.1.3
% 110.37/16.41 % (2547282)Termination reason: Instruction limit
% 110.37/16.41 % (2547282)Termination phase: Saturation
% 110.37/16.41 % (2547282)Time elapsed: 1.289 s
% 110.37/16.41 % (2547282)Peak memory usage: 139 MB
% 110.37/16.41 % (2547282)Instructions burned: 2088 (million)
% 110.37/16.41 % (2547292)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=3629627308:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2932 on theBenchmark for (2932ds/596Mi)
% 110.37/16.41 % (2547292)Refutation not found, incomplete strategy
% 110.37/16.41 % (2547292)------------------------------
% 110.37/16.41 % (2547292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.37/16.41 % (2547292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.37/16.41 % (2547292)CaDiCaL version: 2.1.3
% 110.37/16.41 % (2547292)Termination reason: Refutation not found, incomplete strategy
% 110.37/16.41 % (2547292)Time elapsed: 0.002 s
% 110.37/16.41 % (2547292)Peak memory usage: 88 MB
% 110.37/16.41 % (2547292)Instructions burned: 1 (million)
% 110.37/16.41 % (2547292)------------------------------
% 110.37/16.41 % (2547292)------------------------------
% 110.37/16.41 % (2547294)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=1780994448:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2929 on theBenchmark for (2929ds/4123Mi)
% 110.37/16.41 % (2547288)Instruction limit reached!
% 110.37/16.41 % (2547288)------------------------------
% 110.37/16.41 % (2547288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.37/16.41 % (2547288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.37/16.41 % (2547288)CaDiCaL version: 2.1.3
% 110.37/16.41 % (2547288)Termination reason: Instruction limit
% 110.37/16.41 % (2547288)Termination phase: Saturation
% 110.37/16.41 % (2547288)Time elapsed: 1.854 s
% 110.37/16.41 % (2547288)Peak memory usage: 149 MB
% 110.37/16.41 % (2547288)Instructions burned: 2944 (million)
% 110.37/16.41 % (2547296)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3812692261:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2919 on theBenchmark for (2919ds/16411Mi)
% 110.37/16.41 % (2547289)Instruction limit reached!
% 110.37/16.41 % (2547289)------------------------------
% 110.37/16.41 % (2547289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.37/16.41 % (2547289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.37/16.41 % (2547289)CaDiCaL version: 2.1.3
% 110.37/16.41 % (2547289)Termination reason: Instruction limit
% 110.37/16.41 % (2547289)Termination phase: Saturation
% 110.37/16.41 % (2547289)Time elapsed: 2.290 s
% 110.37/16.41 % (2547289)Peak memory usage: 168 MB
% 110.37/16.41 % (2547289)Instructions burned: 6923 (million)
% 110.37/16.41 % (2547298)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=737875869:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2914 on theBenchmark for (2914ds/1670Mi)
% 110.37/16.41 % (2547266)Instruction limit reached!
% 110.37/16.41 % (2547266)------------------------------
% 110.37/16.41 % (2547266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.37/16.41 % (2547266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.37/16.41 % (2547266)CaDiCaL version: 2.1.3
% 110.37/16.41 % (2547266)Termination reason: Instruction limit
% 110.37/16.41 % (2547266)Termination phase: Saturation
% 110.37/16.41 % (2547266)Time elapsed: 6.525 s
% 110.37/16.41 % (2547266)Peak memory usage: 202 MB
% 110.37/16.41 % (2547266)Instructions burned: 10308 (million)
% 110.37/16.41 % (2547300)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=679871599:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2909 on theBenchmark for (2909ds/1722Mi)
% 110.37/16.41 % (2547298)Instruction limit reached!
% 110.37/16.41 % (2547298)------------------------------
% 110.37/16.41 % (2547298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.37/16.41 % (2547298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.37/16.41 % (2547298)CaDiCaL version: 2.1.3
% 143.25/21.04 % (2547298)Termination reason: Instruction limit
% 143.25/21.04 % (2547298)Termination phase: Saturation
% 143.25/21.04 % (2547298)Time elapsed: 0.653 s
% 143.25/21.04 % (2547298)Peak memory usage: 136 MB
% 143.25/21.04 % (2547298)Instructions burned: 1673 (million)
% 143.25/21.04 % (2547302)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=279965608:cts=off:cond=on:i=9530:bs=on:fsd=on_2907 on theBenchmark for (2907ds/9530Mi)
% 143.25/21.04 % (2547294)Instruction limit reached!
% 143.25/21.04 % (2547294)------------------------------
% 143.25/21.04 % (2547294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.25/21.04 % (2547294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.25/21.04 % (2547294)CaDiCaL version: 2.1.3
% 143.25/21.04 % (2547294)Termination reason: Instruction limit
% 143.25/21.04 % (2547294)Termination phase: Saturation
% 143.25/21.04 % (2547294)Time elapsed: 2.482 s
% 143.25/21.04 % (2547294)Peak memory usage: 154 MB
% 143.25/21.04 % (2547294)Instructions burned: 4124 (million)
% 143.25/21.04 % (2547304)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=115790377:st=2:i=4495:sd=10:ss=included_2902 on theBenchmark for (2902ds/4495Mi)
% 143.25/21.04 % (2547300)Instruction limit reached!
% 143.25/21.04 % (2547300)------------------------------
% 143.25/21.04 % (2547300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.25/21.04 % (2547300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.25/21.04 % (2547300)CaDiCaL version: 2.1.3
% 143.25/21.04 % (2547300)Termination reason: Instruction limit
% 143.25/21.04 % (2547300)Termination phase: Saturation
% 143.25/21.04 % (2547300)Time elapsed: 1.304 s
% 143.25/21.04 % (2547300)Peak memory usage: 133 MB
% 143.25/21.04 % (2547300)Instructions burned: 1723 (million)
% 143.25/21.04 % (2547306)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=71143871:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2895 on theBenchmark for (2895ds/4920Mi)
% 143.25/21.04 % (2547304)Instruction limit reached!
% 143.25/21.04 % (2547304)------------------------------
% 143.25/21.04 % (2547304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.25/21.04 % (2547304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.25/21.04 % (2547304)CaDiCaL version: 2.1.3
% 143.25/21.04 % (2547304)Termination reason: Instruction limit
% 143.25/21.04 % (2547304)Termination phase: Saturation
% 143.25/21.04 % (2547304)Time elapsed: 2.696 s
% 143.25/21.04 % (2547304)Peak memory usage: 162 MB
% 143.25/21.04 % (2547304)Instructions burned: 4495 (million)
% 143.25/21.04 % (2547302)Instruction limit reached!
% 143.25/21.04 % (2547302)------------------------------
% 143.25/21.04 % (2547302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.25/21.04 % (2547302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.25/21.04 % (2547302)CaDiCaL version: 2.1.3
% 143.25/21.04 % (2547302)Termination reason: Instruction limit
% 143.25/21.04 % (2547302)Termination phase: Saturation
% 143.25/21.04 % (2547302)Time elapsed: 3.296 s
% 143.25/21.04 % (2547302)Peak memory usage: 190 MB
% 143.25/21.04 % (2547302)Instructions burned: 9532 (million)
% 143.25/21.04 % (2547309)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=2798110653:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2874 on theBenchmark for (2874ds/2083Mi)
% 143.25/21.04 % (2547346)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=518361778:i=4629:av=off:gsp=on_2873 on theBenchmark for (2873ds/4629Mi)
% 143.25/21.04 % (2547346)Refutation not found, incomplete strategy
% 143.25/21.04 % (2547346)------------------------------
% 143.25/21.04 % (2547346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.25/21.04 % (2547346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.25/21.04 % (2547346)CaDiCaL version: 2.1.3
% 143.25/21.04 % (2547346)Termination reason: Refutation not found, incomplete strategy
% 143.25/21.04 % (2547346)Time elapsed: 0.443 s
% 143.25/21.04 % (2547346)Peak memory usage: 127 MB
% 143.25/21.04 % (2547346)Instructions burned: 869 (million)
% 143.25/21.04 % (2547346)------------------------------
% 143.25/21.04 % (2547346)------------------------------
% 143.25/21.04 % (2547471)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2599643738:i=1258:av=off_2866 on theBenchmark for (2866ds/1258Mi)
% 155.00/22.89 % (2547306)Instruction limit reached!
% 155.00/22.89 % (2547306)------------------------------
% 155.00/22.89 % (2547306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.00/22.89 % (2547306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.00/22.89 % (2547306)CaDiCaL version: 2.1.3
% 155.00/22.89 % (2547306)Termination reason: Instruction limit
% 155.00/22.89 % (2547306)Termination phase: Saturation
% 155.00/22.89 % (2547306)Time elapsed: 2.852 s
% 155.00/22.89 % (2547306)Peak memory usage: 160 MB
% 155.00/22.89 % (2547306)Instructions burned: 4921 (million)
% 155.00/22.89 % (2547516)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1094221037:i=7343:av=off:ss=included_2865 on theBenchmark for (2865ds/7343Mi)
% 155.00/22.89 % (2547471)Instruction limit reached!
% 155.00/22.89 % (2547471)------------------------------
% 155.00/22.89 % (2547471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.00/22.89 % (2547471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.00/22.89 % (2547471)CaDiCaL version: 2.1.3
% 155.00/22.89 % (2547471)Termination reason: Instruction limit
% 155.00/22.89 % (2547471)Termination phase: Saturation
% 155.00/22.89 % (2547471)Time elapsed: 0.361 s
% 155.00/22.89 % (2547471)Peak memory usage: 110 MB
% 155.00/22.89 % (2547471)Instructions burned: 1261 (million)
% 155.00/22.89 % (2547549)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1990378881:i=1325:sd=2:ss=axioms:sgt=16_2861 on theBenchmark for (2861ds/1325Mi)
% 155.00/22.89 % (2547309)Instruction limit reached!
% 155.00/22.89 % (2547309)------------------------------
% 155.00/22.89 % (2547309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.00/22.89 % (2547309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.00/22.89 % (2547309)CaDiCaL version: 2.1.3
% 155.00/22.89 % (2547309)Termination reason: Instruction limit
% 155.00/22.89 % (2547309)Termination phase: Saturation
% 155.00/22.89 % (2547309)Time elapsed: 1.281 s
% 155.00/22.89 % (2547309)Peak memory usage: 140 MB
% 155.00/22.89 % (2547309)Instructions burned: 2083 (million)
% 155.00/22.89 % (2547564)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=8789474:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2860 on theBenchmark for (2860ds/2646Mi)
% 155.00/22.89 % (2547549)Instruction limit reached!
% 155.00/22.89 % (2547549)------------------------------
% 155.00/22.89 % (2547549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.00/22.89 % (2547549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.00/22.89 % (2547549)CaDiCaL version: 2.1.3
% 155.00/22.89 % (2547549)Termination reason: Instruction limit
% 155.00/22.89 % (2547549)Termination phase: Saturation
% 155.00/22.89 % (2547549)Time elapsed: 0.424 s
% 155.00/22.89 % (2547549)Peak memory usage: 103 MB
% 155.00/22.89 % (2547549)Instructions burned: 1326 (million)
% 155.00/22.89 % (2547566)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1367197405:i=1489:sd=2:ep=R:ss=axioms_2856 on theBenchmark for (2856ds/1489Mi)
% 155.00/22.89 % (2547566)Refutation not found, incomplete strategy
% 155.00/22.89 % (2547566)------------------------------
% 155.00/22.89 % (2547566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.00/22.89 % (2547566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.00/22.89 % (2547566)CaDiCaL version: 2.1.3
% 155.00/22.89 % (2547566)Termination reason: Refutation not found, incomplete strategy
% 155.00/22.89 % (2547566)Time elapsed: 0.425 s
% 155.00/22.89 % (2547566)Peak memory usage: 127 MB
% 155.00/22.89 % (2547566)Instructions burned: 858 (million)
% 155.00/22.89 % (2547566)------------------------------
% 155.00/22.89 % (2547566)------------------------------
% 155.00/22.89 % (2547588)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=347446438:i=1503_2848 on theBenchmark for (2848ds/1503Mi)
% 155.00/22.89 % (2547588)Refutation not found, incomplete strategy
% 155.00/22.89 % (2547588)------------------------------
% 155.00/22.89 % (2547588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.00/22.89 % (2547588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.32/25.78 % (2547588)CaDiCaL version: 2.1.3
% 176.32/25.78 % (2547588)Termination reason: Refutation not found, incomplete strategy
% 176.32/25.78 % (2547588)Time elapsed: 0.368 s
% 176.32/25.78 % (2547588)Peak memory usage: 127 MB
% 176.32/25.78 % (2547588)Instructions burned: 856 (million)
% 176.32/25.78 % (2547588)------------------------------
% 176.32/25.78 % (2547588)------------------------------
% 176.32/25.78 % (2547600)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2323928269:i=13942:kws=frequency_2841 on theBenchmark for (2841ds/13942Mi)
% 176.32/25.78 % (2547564)Instruction limit reached!
% 176.32/25.78 % (2547564)------------------------------
% 176.32/25.78 % (2547564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.32/25.78 % (2547564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.32/25.78 % (2547564)CaDiCaL version: 2.1.3
% 176.32/25.78 % (2547564)Termination reason: Instruction limit
% 176.32/25.78 % (2547564)Termination phase: Saturation
% 176.32/25.78 % (2547564)Time elapsed: 2.374 s
% 176.32/25.78 % (2547564)Peak memory usage: 147 MB
% 176.32/25.78 % (2547564)Instructions burned: 2646 (million)
% 176.32/25.78 % (2547611)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=640540797:i=3604:fsr=off:er=filter_2835 on theBenchmark for (2835ds/3604Mi)
% 176.32/25.78 % (2547611)Instruction limit reached!
% 176.32/25.78 % (2547611)------------------------------
% 176.32/25.78 % (2547611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.32/25.78 % (2547611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.32/25.78 % (2547611)CaDiCaL version: 2.1.3
% 176.32/25.78 % (2547611)Termination reason: Instruction limit
% 176.32/25.78 % (2547611)Termination phase: Saturation
% 176.32/25.78 % (2547611)Time elapsed: 2.484 s
% 176.32/25.78 % (2547611)Peak memory usage: 151 MB
% 176.32/25.78 % (2547611)Instructions burned: 3605 (million)
% 176.32/25.78 % (2547516)Instruction limit reached!
% 176.32/25.78 % (2547516)------------------------------
% 176.32/25.78 % (2547516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.32/25.78 % (2547516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.32/25.78 % (2547516)CaDiCaL version: 2.1.3
% 176.32/25.78 % (2547516)Termination reason: Instruction limit
% 176.32/25.78 % (2547516)Termination phase: Saturation
% 176.32/25.78 % (2547516)Time elapsed: 5.605 s
% 176.32/25.78 % (2547516)Peak memory usage: 193 MB
% 176.32/25.78 % (2547516)Instructions burned: 7344 (million)
% 176.32/25.78 % (2547773)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2920630460:i=1876:sd=1:ss=included:sgt=32_2807 on theBenchmark for (2807ds/1876Mi)
% 176.32/25.78 % (2547774)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2892153779:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2807 on theBenchmark for (2807ds/1932Mi)
% 176.32/25.78 % (2547296)Instruction limit reached!
% 176.32/25.78 % (2547296)------------------------------
% 176.32/25.78 % (2547296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.32/25.78 % (2547296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.32/25.78 % (2547296)CaDiCaL version: 2.1.3
% 176.32/25.78 % (2547296)Termination reason: Instruction limit
% 176.32/25.78 % (2547296)Termination phase: Saturation
% 176.32/25.78 % (2547296)Time elapsed: 11.555 s
% 176.32/25.78 % (2547296)Peak memory usage: 240 MB
% 176.32/25.78 % (2547296)Instructions burned: 16411 (million)
% 176.32/25.78 % (2547777)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=2690431579:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2802 on theBenchmark for (2802ds/1980Mi)
% 176.32/25.78 % (2547774)Refutation not found, incomplete strategy
% 176.32/25.78 % (2547774)------------------------------
% 176.32/25.78 % (2547774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.32/25.78 % (2547774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.32/25.78 % (2547774)CaDiCaL version: 2.1.3
% 176.32/25.78 % (2547774)Termination reason: Refutation not found, incomplete strategy
% 176.32/25.78 % (2547774)Time elapsed: 0.576 s
% 176.32/25.78 % (2547774)Peak memory usage: 127 MB
% 176.32/25.78 % (2547774)Instructions burned: 870 (million)
% 176.32/25.78 % (2547774)------------------------------
% 176.32/25.78 % (2547774)------------------------------
% 167.54/28.46 % (2547779)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=3081680504:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2797 on theBenchmark for (2797ds/3902Mi)
% 167.54/28.46 % (2547773)Instruction limit reached!
% 167.54/28.46 % (2547773)------------------------------
% 167.54/28.46 % (2547773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.46 % (2547773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.46 % (2547773)CaDiCaL version: 2.1.3
% 167.54/28.46 % (2547773)Termination reason: Instruction limit
% 167.54/28.46 % (2547773)Termination phase: Saturation
% 167.54/28.46 % (2547773)Time elapsed: 1.148 s
% 167.54/28.46 % (2547773)Peak memory usage: 138 MB
% 167.54/28.46 % (2547773)Instructions burned: 1877 (million)
% 167.54/28.46 % (2547781)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2323787743:avsq=on:i=3916:aac=none:amm=off_2795 on theBenchmark for (2795ds/3916Mi)
% 167.54/28.46 % (2547779)Refutation not found, incomplete strategy
% 167.54/28.46 % (2547779)------------------------------
% 167.54/28.46 % (2547779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.46 % (2547779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.46 % (2547779)CaDiCaL version: 2.1.3
% 167.54/28.46 % (2547779)Termination reason: Refutation not found, incomplete strategy
% 167.54/28.46 % (2547779)Time elapsed: 0.574 s
% 167.54/28.46 % (2547779)Peak memory usage: 128 MB
% 167.54/28.46 % (2547779)Instructions burned: 869 (million)
% 167.54/28.46 % (2547777)Instruction limit reached!
% 167.54/28.46 % (2547777)------------------------------
% 167.54/28.46 % (2547777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.46 % (2547777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.46 % (2547777)CaDiCaL version: 2.1.3
% 167.54/28.46 % (2547777)Termination reason: Instruction limit
% 167.54/28.46 % (2547777)Termination phase: Saturation
% 167.54/28.46 % (2547777)Time elapsed: 1.198 s
% 167.54/28.46 % (2547777)Peak memory usage: 138 MB
% 167.54/28.46 % (2547777)Instructions burned: 1980 (million)
% 167.54/28.46 % (2547779)------------------------------
% 167.54/28.46 % (2547779)------------------------------
% 167.54/28.46 % (2547600)Instruction limit reached!
% 167.54/28.46 % (2547600)------------------------------
% 167.54/28.46 % (2547600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.46 % (2547600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.46 % (2547600)CaDiCaL version: 2.1.3
% 167.54/28.46 % (2547600)Termination reason: Instruction limit
% 167.54/28.46 % (2547600)Termination phase: Saturation
% 167.54/28.46 % (2547600)Time elapsed: 5.214 s
% 167.54/28.46 % (2547600)Peak memory usage: 256 MB
% 167.54/28.46 % (2547600)Instructions burned: 13943 (million)
% 167.54/28.46 % (2547783)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=4261050605:cond=on:i=3940:av=off:er=known_2789 on theBenchmark for (2789ds/3940Mi)
% 167.54/28.46 % (2547785)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=1111885335:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2788 on theBenchmark for (2788ds/2087Mi)
% 167.54/28.46 % (2547784)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=226278988:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2788 on theBenchmark for (2788ds/3980Mi)
% 167.54/28.46 % (2547785)Instruction limit reached!
% 167.54/28.46 % (2547785)------------------------------
% 167.54/28.46 % (2547785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.46 % (2547785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.46 % (2547785)CaDiCaL version: 2.1.3
% 167.54/28.46 % (2547785)Termination reason: Instruction limit
% 167.54/28.46 % (2547785)Termination phase: Saturation
% 167.54/28.46 % (2547785)Time elapsed: 0.667 s
% 167.54/28.46 % (2547785)Peak memory usage: 143 MB
% 167.54/28.46 % (2547785)Instructions burned: 2090 (million)
% 167.54/28.46 % (2547789)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1056528921:cts=off:cond=on:i=4272:bs=on:fsd=on_2780 on theBenchmark for (2780ds/4272Mi)
% 167.54/28.46 % (2547781)Instruction limit reached!
% 167.54/28.46 % (2547781)------------------------------
% 167.54/28.46 % (2547781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.46 % (2547781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.46 % (2547781)CaDiCaL version: 2.1.3
% 167.54/28.46 % (2547781)Termination reason: Instruction limit
% 167.54/28.46 % (2547781)Termination phase: Saturation
% 167.54/28.46 % (2547781)Time elapsed: 2.304 s
% 167.54/28.46 % (2547781)Peak memory usage: 135 MB
% 167.54/28.46 % (2547781)Instructions burned: 3918 (million)
% 167.54/28.46 % (2547791)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2115464068:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2770 on theBenchmark for (2770ds/2197Mi)
% 167.54/28.46 % (2547783)Instruction limit reached!
% 167.54/28.46 % (2547783)------------------------------
% 167.54/28.46 % (2547783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.46 % (2547783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.46 % (2547783)CaDiCaL version: 2.1.3
% 167.54/28.46 % (2547783)Termination reason: Instruction limit
% 167.54/28.46 % (2547783)Termination phase: Saturation
% 167.54/28.46 % (2547783)Time elapsed: 2.235 s
% 167.54/28.46 % (2547783)Peak memory usage: 158 MB
% 167.54/28.46 % (2547783)Instructions burned: 3940 (million)
% 167.54/28.46 % (2547789)Instruction limit reached!
% 167.54/28.46 % (2547789)------------------------------
% 167.54/28.46 % (2547789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.46 % (2547789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.46 % (2547789)CaDiCaL version: 2.1.3
% 167.54/28.46 % (2547789)Termination reason: Instruction limit
% 167.54/28.46 % (2547789)Termination phase: Saturation
% 167.54/28.46 % (2547789)Time elapsed: 1.418 s
% 167.54/28.46 % (2547789)Peak memory usage: 159 MB
% 167.54/28.46 % (2547789)Instructions burned: 4273 (million)
% 167.54/28.46 % (2547793)dis+21_1_sil=8000:spb=goal_then_units:random_seed=1008743909:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2765 on theBenchmark for (2765ds/6508Mi)
% 167.54/28.46 % (2547794)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3359075641:i=2330:fgj=on:av=off:fsr=off_2765 on theBenchmark for (2765ds/2330Mi)
% 167.54/28.46 % (2547784)Instruction limit reached!
% 167.54/28.46 % (2547784)------------------------------
% 167.54/28.46 % (2547784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.46 % (2547784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.46 % (2547784)CaDiCaL version: 2.1.3
% 167.54/28.46 % (2547784)Termination reason: Instruction limit
% 167.54/28.46 % (2547784)Termination phase: Saturation
% 167.54/28.46 % (2547784)Time elapsed: 2.433 s
% 167.54/28.46 % (2547784)Peak memory usage: 157 MB
% 167.54/28.46 % (2547784)Instructions burned: 3980 (million)
% 167.54/28.46 % (2547797)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2593127524:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2762 on theBenchmark for (2762ds/7592Mi)
% 167.54/28.46 % (2547791)Instruction limit reached!
% 167.54/28.46 % (2547791)------------------------------
% 167.54/28.46 % (2547791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.46 % (2547791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.47 % (2547791)CaDiCaL version: 2.1.3
% 167.54/28.47 % (2547791)Termination reason: Instruction limit
% 167.54/28.47 % (2547791)Termination phase: Saturation
% 167.54/28.47 % (2547791)Time elapsed: 0.952 s
% 167.54/28.47 % (2547791)Peak memory usage: 138 MB
% 167.54/28.47 % (2547791)Instructions burned: 2200 (million)
% 167.54/28.47 % (2547799)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=3013655248:i=2693:kws=precedence:ins=1:av=off_2759 on theBenchmark for (2759ds/2693Mi)
% 167.54/28.47 % (2547794)Instruction limit reached!
% 167.54/28.47 % (2547794)------------------------------
% 167.54/28.47 % (2547794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.47 % (2547794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.47 % (2547794)CaDiCaL version: 2.1.3
% 167.54/28.47 % (2547794)Termination reason: Instruction limit
% 167.54/28.47 % (2547794)Termination phase: Saturation
% 167.54/28.47 % (2547794)Time elapsed: 1.344 s
% 167.54/28.47 % (2547794)Peak memory usage: 141 MB
% 167.54/28.47 % (2547794)Instructions burned: 2331 (million)
% 167.54/28.47 % (2547799)Instruction limit reached!
% 167.54/28.47 % (2547799)------------------------------
% 167.54/28.47 % (2547799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.47 % (2547799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.47 % (2547799)CaDiCaL version: 2.1.3
% 167.54/28.47 % (2547799)Termination reason: Instruction limit
% 167.54/28.47 % (2547799)Termination phase: Saturation
% 167.54/28.47 % (2547799)Time elapsed: 0.915 s
% 167.54/28.47 % (2547799)Peak memory usage: 149 MB
% 167.54/28.47 % (2547799)Instructions burned: 2696 (million)
% 167.54/28.47 % (2547801)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=3288018794:i=28651:sd=4:ss=included:sgt=64_2750 on theBenchmark for (2750ds/28651Mi)
% 167.54/28.47 % (2547802)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=158937340:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2749 on theBenchmark for (2749ds/2700Mi)
% 167.54/28.47 % (2547802)Instruction limit reached!
% 167.54/28.47 % (2547802)------------------------------
% 167.54/28.47 % (2547802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.47 % (2547802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.47 % (2547802)CaDiCaL version: 2.1.3
% 167.54/28.47 % (2547802)Termination reason: Instruction limit
% 167.54/28.47 % (2547802)Termination phase: Saturation
% 167.54/28.47 % (2547802)Time elapsed: 0.914 s
% 167.54/28.47 % (2547802)Peak memory usage: 144 MB
% 167.54/28.47 % (2547802)Instructions burned: 2704 (million)
% 167.54/28.47 % (2547805)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=1454181100:i=3196:nm=4_2739 on theBenchmark for (2739ds/3196Mi)
% 167.54/28.47 % (2547805)Refutation not found, incomplete strategy
% 167.54/28.47 % (2547805)------------------------------
% 167.54/28.47 % (2547805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.47 % (2547805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.47 % (2547805)CaDiCaL version: 2.1.3
% 167.54/28.47 % (2547805)Termination reason: Refutation not found, incomplete strategy
% 167.54/28.47 % (2547805)Time elapsed: 0.342 s
% 167.54/28.47 % (2547805)Peak memory usage: 128 MB
% 167.54/28.47 % (2547805)Instructions burned: 907 (million)
% 167.54/28.47 % (2547805)------------------------------
% 167.54/28.47 % (2547805)------------------------------
% 167.54/28.47 % (2547807)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=1367115283:cts=off:i=3254:av=off_2733 on theBenchmark for (2733ds/3254Mi)
% 167.54/28.47 % (2547793)Instruction limit reached!
% 167.54/28.47 % (2547793)------------------------------
% 167.54/28.47 % (2547793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 167.54/28.47 % (2547793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 167.54/28.47 % (2547793)CaDiCaL version: 2.1.3
% 167.54/28.47 % (2547793)Termination reason: Instruction limit
% 167.54/28.47 % (2547793)Termination phase: Saturation
% 167.54/28.47 % (2547793)Time elapsed: 3.503 s
% 167.54/28.47 % (2547793)Peak memory usage: 148 MB
% 167.54/28.47 % (2547793)Instructions burned: 6509 (million)
% 167.54/28.47 % (2547809)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=2881772167:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2728 on theBenchmark for (2728ds/3264Mi)
% 167.54/28.47 % (2547214)First to succeed.
% 167.54/28.47 % (2547214)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2547209"
% 167.54/28.47 % (2547214)Refutation found. Thanks to Tanya!
% 167.54/28.47 % SZS status Unsatisfiable for theBenchmark
% 167.54/28.47 % SZS output start Proof for theBenchmark
% See solution above
% 195.88/28.67 % (2547214)------------------------------
% 195.88/28.67 % (2547214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.88/28.67 % (2547214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.88/28.67 % (2547214)CaDiCaL version: 2.1.3
% 195.88/28.67 % (2547214)Termination reason: Refutation
% 195.88/28.67 % (2547214)Time elapsed: 27.119 s
% 195.88/28.67 % (2547214)Peak memory usage: 491 MB
% 195.88/28.67 % (2547214)Instructions burned: 41517 (million)
% 195.88/28.67 % (2547214)------------------------------
% 195.88/28.67 % (2547214)------------------------------
% 195.88/28.67 % (2547209)Success in time 27.623 s
% 195.88/28.67 % Vampire exiting
%------------------------------------------------------------------------------