%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE108-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:40:21 AM UTC 2026
% Result : Unsatisfiable 13.39s 2.79s
% Output : Refutation 14.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 44
% Syntax : Number of formulae : 265 ( 265 unt; 22 def)
% Number of atoms : 265 ( 264 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 27 con; 0-2 aty)
% Number of variables : 151 ( 151 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_commutativity) ).
fof(f4,axiom,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(addition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_associativity) ).
fof(f5,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity) ).
fof(f6,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_idempotence) ).
fof(f7,axiom,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_associativity) ).
fof(f8,negated_conjecture,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_right_identity) ).
fof(f9,negated_conjecture,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_left_identity) ).
fof(f10,axiom,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_distributivity) ).
fof(f11,axiom,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_distributivity) ).
fof(f19,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain1) ).
fof(f20,plain,
! [X0] : zero = multiplication(antidomain(X0),X0),
inference(reorient_equations,[],[f19]) ).
fof(f23,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain3) ).
fof(f24,plain,
! [X0] : one = addition(antidomain(antidomain(X0)),antidomain(X0)),
inference(reorient_equations,[],[f23]) ).
fof(f25,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain4) ).
fof(f26,plain,
! [X0] : antidomain(antidomain(X0)) = domain(X0),
inference(reorient_equations,[],[f25]) ).
fof(f27,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain1) ).
fof(f28,plain,
! [X0] : zero = multiplication(X0,coantidomain(X0)),
inference(reorient_equations,[],[f27]) ).
fof(f29,axiom,
! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain2) ).
fof(f30,plain,
! [X0,X1] : coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)) = addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))),
inference(reorient_equations,[],[f29]) ).
fof(f31,axiom,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain3) ).
fof(f32,plain,
! [X0] : one = addition(coantidomain(coantidomain(X0)),coantidomain(X0)),
inference(reorient_equations,[],[f31]) ).
fof(f33,axiom,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain4) ).
fof(f34,plain,
! [X0] : coantidomain(coantidomain(X0)) = codomain(X0),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
! [X0] : c(X0) = antidomain(domain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement) ).
fof(f37,negated_conjecture,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',forward_diamond) ).
fof(f38,negated_conjecture,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',backward_diamond) ).
fof(f39,negated_conjecture,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',forward_box) ).
fof(f41,negated_conjecture,
addition(domain(sK2_goals_X1),forward_box(sK3_goals_X0,domain(sK1_goals_X2))) = forward_box(sK3_goals_X0,domain(sK1_goals_X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f42,plain,
forward_box(sK3_goals_X0,domain(sK1_goals_X2)) = addition(domain(sK2_goals_X1),forward_box(sK3_goals_X0,domain(sK1_goals_X2))),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
addition(backward_diamond(sK3_goals_X0,domain(sK2_goals_X1)),domain(sK1_goals_X2)) != domain(sK1_goals_X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_1) ).
fof(f44,plain,
domain(sK1_goals_X2) != addition(backward_diamond(sK3_goals_X0,domain(sK2_goals_X1)),domain(sK1_goals_X2)),
inference(reorient_equations,[],[f43]) ).
fof(f46,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f37,f26,f26]) ).
fof(f47,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f38,f34,f34]) ).
fof(f48,plain,
! [X0] : c(X0) = antidomain(antidomain(antidomain(X0))),
inference(definition_unfolding,[],[f35,f26]) ).
fof(f49,plain,
! [X0,X1] : forward_box(X0,X1) = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(X0,antidomain(antidomain(antidomain(antidomain(antidomain(X1))))))))))),
inference(definition_unfolding,[],[f39,f48,f46,f48]) ).
fof(f51,plain,
antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))))))))) = addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))))))))))))),
inference(definition_unfolding,[],[f42,f49,f26,f26,f49,f26]) ).
fof(f52,plain,
antidomain(antidomain(sK1_goals_X2)) != addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0))),antidomain(antidomain(sK1_goals_X2))),
inference(definition_unfolding,[],[f44,f26,f47,f26,f26]) ).
fof(f53,definition,
sF0 = antidomain(sK1_goals_X2),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f54,plain,
antidomain(sK1_goals_X2) = sF0,
inference(reorient_equations,[],[f53]) ).
fof(f55,definition,
sF1 = antidomain(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f56,plain,
antidomain(sF0) = sF1,
inference(reorient_equations,[],[f55]) ).
fof(f57,definition,
sF2 = antidomain(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f58,plain,
antidomain(sF1) = sF2,
inference(reorient_equations,[],[f57]) ).
fof(f59,definition,
sF3 = antidomain(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f60,plain,
antidomain(sF2) = sF3,
inference(reorient_equations,[],[f59]) ).
fof(f61,definition,
sF4 = antidomain(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f62,plain,
antidomain(sF3) = sF4,
inference(reorient_equations,[],[f61]) ).
fof(f63,definition,
sF5 = antidomain(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f64,plain,
antidomain(sF4) = sF5,
inference(reorient_equations,[],[f63]) ).
fof(f65,definition,
sF6 = antidomain(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f66,plain,
antidomain(sF5) = sF6,
inference(reorient_equations,[],[f65]) ).
fof(f67,definition,
sF7 = multiplication(sK3_goals_X0,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f68,plain,
multiplication(sK3_goals_X0,sF6) = sF7,
inference(reorient_equations,[],[f67]) ).
fof(f69,definition,
sF8 = antidomain(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f70,plain,
antidomain(sF7) = sF8,
inference(reorient_equations,[],[f69]) ).
fof(f71,definition,
sF9 = antidomain(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f72,plain,
antidomain(sF8) = sF9,
inference(reorient_equations,[],[f71]) ).
fof(f73,definition,
sF10 = antidomain(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f74,plain,
antidomain(sF9) = sF10,
inference(reorient_equations,[],[f73]) ).
fof(f75,definition,
sF11 = antidomain(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f76,plain,
antidomain(sF10) = sF11,
inference(reorient_equations,[],[f75]) ).
fof(f77,definition,
sF12 = antidomain(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f78,plain,
antidomain(sF11) = sF12,
inference(reorient_equations,[],[f77]) ).
fof(f79,definition,
sF13 = antidomain(sK2_goals_X1),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f80,plain,
antidomain(sK2_goals_X1) = sF13,
inference(reorient_equations,[],[f79]) ).
fof(f81,definition,
sF14 = antidomain(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f82,plain,
antidomain(sF13) = sF14,
inference(reorient_equations,[],[f81]) ).
fof(f83,definition,
sF15 = addition(sF14,sF12),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f84,plain,
addition(sF14,sF12) = sF15,
inference(reorient_equations,[],[f83]) ).
fof(f85,plain,
sF12 = sF15,
inference(definition_folding,[],[f51,f84,f78,f76,f74,f72,f70,f68,f66,f64,f62,f60,f58,f56,f54,f82,f80,f78,f76,f74,f72,f70,f68,f66,f64,f62,f60,f58,f56,f54]) ).
fof(f86,definition,
sF16 = coantidomain(sF14),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f87,plain,
coantidomain(sF14) = sF16,
inference(reorient_equations,[],[f86]) ).
fof(f88,definition,
sF17 = coantidomain(sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f89,plain,
coantidomain(sF16) = sF17,
inference(reorient_equations,[],[f88]) ).
fof(f90,definition,
sF18 = multiplication(sF17,sK3_goals_X0),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f91,plain,
multiplication(sF17,sK3_goals_X0) = sF18,
inference(reorient_equations,[],[f90]) ).
fof(f92,definition,
sF19 = coantidomain(sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f93,plain,
coantidomain(sF18) = sF19,
inference(reorient_equations,[],[f92]) ).
fof(f94,definition,
sF20 = coantidomain(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f95,plain,
coantidomain(sF19) = sF20,
inference(reorient_equations,[],[f94]) ).
fof(f96,definition,
sF21 = addition(sF20,sF1),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f97,plain,
addition(sF20,sF1) = sF21,
inference(reorient_equations,[],[f96]) ).
fof(f98,plain,
sF1 != sF21,
inference(definition_folding,[],[f52,f97,f56,f54,f95,f93,f91,f89,f87,f82,f80,f56,f54]) ).
fof(f99,plain,
! [X0] : one = addition(antidomain(X0),antidomain(antidomain(X0))),
inference(backward_demodulation,[],[f24,f3]) ).
fof(f100,plain,
! [X0] : one = addition(coantidomain(X0),coantidomain(coantidomain(X0))),
inference(backward_demodulation,[],[f32,f3]) ).
fof(f101,plain,
sF12 = addition(sF14,sF12),
inference(forward_demodulation,[],[f84,f85]) ).
fof(f128,plain,
! [X0,X1] : multiplication(X0,addition(X1,coantidomain(X0))) = addition(multiplication(X0,X1),zero),
inference(superposition,[],[f10,f28]) ).
fof(f129,plain,
! [X0,X1] : multiplication(X0,addition(coantidomain(X0),X1)) = addition(zero,multiplication(X0,X1)),
inference(superposition,[],[f10,f28]) ).
fof(f133,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(X0,addition(X1,coantidomain(X0))),
inference(forward_demodulation,[],[f128,f5]) ).
fof(f141,plain,
! [X2,X0,X1] : addition(multiplication(X0,X1),multiplication(X0,X2)) = multiplication(X0,addition(X2,X1)),
inference(superposition,[],[f10,f3]) ).
fof(f182,plain,
zero = multiplication(sF8,sF7),
inference(superposition,[],[f20,f70]) ).
fof(f189,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X1,X0)) = addition(multiplication(antidomain(X0),X1),zero),
inference(superposition,[],[f10,f20]) ).
fof(f194,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X1,X0)) = multiplication(antidomain(X0),X1),
inference(forward_demodulation,[],[f189,f5]) ).
fof(f198,plain,
! [X0] : addition(zero,X0) = X0,
inference(superposition,[],[f3,f5]) ).
fof(f199,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(X0,addition(coantidomain(X0),X1)),
inference(backward_demodulation,[],[f129,f198]) ).
fof(f228,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X0)) = addition(zero,multiplication(X1,coantidomain(X0))),
inference(superposition,[],[f11,f28]) ).
fof(f229,plain,
! [X0,X1] : multiplication(addition(antidomain(X0),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(superposition,[],[f11,f20]) ).
fof(f233,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = addition(multiplication(X0,coantidomain(X1)),zero),
inference(superposition,[],[f11,f28]) ).
fof(f236,plain,
! [X0] : multiplication(addition(X0,sK3_goals_X0),sF6) = addition(multiplication(X0,sF6),sF7),
inference(superposition,[],[f11,f68]) ).
fof(f248,plain,
! [X0] : addition(sF7,multiplication(X0,sF6)) = multiplication(addition(X0,sK3_goals_X0),sF6),
inference(forward_demodulation,[],[f236,f3]) ).
fof(f251,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = multiplication(X0,coantidomain(X1)),
inference(forward_demodulation,[],[f233,f5]) ).
fof(f252,plain,
! [X0,X1] : multiplication(addition(antidomain(X0),X1),X0) = multiplication(X1,X0),
inference(forward_demodulation,[],[f229,f198]) ).
fof(f253,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X0)) = multiplication(X1,coantidomain(X0)),
inference(forward_demodulation,[],[f228,f198]) ).
fof(f328,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(superposition,[],[f10,f8]) ).
fof(f354,plain,
one = addition(sF13,antidomain(sF13)),
inference(superposition,[],[f99,f80]) ).
fof(f355,plain,
one = addition(sF0,antidomain(sF0)),
inference(superposition,[],[f99,f54]) ).
fof(f383,plain,
one = addition(sF0,sF1),
inference(forward_demodulation,[],[f355,f56]) ).
fof(f384,plain,
one = addition(sF13,sF14),
inference(forward_demodulation,[],[f354,f82]) ).
fof(f386,plain,
one = addition(sF14,sF13),
inference(forward_demodulation,[],[f384,f3]) ).
fof(f391,plain,
! [X0] : multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))) = multiplication(one,coantidomain(coantidomain(coantidomain(X0)))),
inference(superposition,[],[f251,f100]) ).
fof(f394,plain,
! [X0] : coantidomain(coantidomain(coantidomain(X0))) = multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f391,f9]) ).
fof(f398,plain,
! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X1,addition(X0,X2)),
inference(superposition,[],[f4,f3]) ).
fof(f417,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(superposition,[],[f3,f4]) ).
fof(f433,plain,
! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)),
inference(superposition,[],[f11,f9]) ).
fof(f439,plain,
zero = coantidomain(one),
inference(superposition,[],[f28,f9]) ).
fof(f467,plain,
! [X2,X0,X1] : multiplication(antidomain(multiplication(X1,X2)),multiplication(X0,X2)) = multiplication(antidomain(multiplication(X1,X2)),multiplication(addition(X0,X1),X2)),
inference(superposition,[],[f194,f11]) ).
fof(f469,plain,
! [X0] : multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)) = multiplication(antidomain(antidomain(antidomain(X0))),one),
inference(superposition,[],[f194,f99]) ).
fof(f491,plain,
! [X0] : antidomain(antidomain(antidomain(X0))) = multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)),
inference(forward_demodulation,[],[f469,f8]) ).
fof(f498,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f4,f6]) ).
fof(f550,plain,
! [X0] : multiplication(sF18,X0) = multiplication(sF17,multiplication(sK3_goals_X0,X0)),
inference(superposition,[],[f7,f91]) ).
fof(f624,plain,
! [X0] : one = addition(antidomain(X0),one),
inference(superposition,[],[f498,f99]) ).
fof(f628,plain,
! [X0] : one = addition(coantidomain(X0),one),
inference(superposition,[],[f498,f100]) ).
fof(f642,plain,
! [X0] : one = addition(one,coantidomain(X0)),
inference(forward_demodulation,[],[f628,f3]) ).
fof(f643,plain,
! [X0] : one = addition(one,antidomain(X0)),
inference(forward_demodulation,[],[f624,f3]) ).
fof(f648,plain,
! [X0] : addition(one,X0) = addition(sF0,addition(sF1,X0)),
inference(superposition,[],[f4,f383]) ).
fof(f703,plain,
multiplication(addition(one,sF17),sK3_goals_X0) = addition(sK3_goals_X0,sF18),
inference(superposition,[],[f433,f91]) ).
fof(f722,plain,
multiplication(addition(one,sF17),sK3_goals_X0) = addition(sF18,sK3_goals_X0),
inference(forward_demodulation,[],[f703,f3]) ).
fof(f736,plain,
addition(sF18,sK3_goals_X0) = multiplication(addition(sF17,one),sK3_goals_X0),
inference(forward_demodulation,[],[f722,f3]) ).
fof(f808,plain,
! [X0] : multiplication(X0,sF0) = multiplication(addition(sF1,X0),sF0),
inference(superposition,[],[f252,f56]) ).
fof(f811,plain,
! [X0] : multiplication(X0,sF3) = multiplication(addition(sF4,X0),sF3),
inference(superposition,[],[f252,f62]) ).
fof(f820,plain,
! [X0] : multiplication(one,X0) = multiplication(antidomain(antidomain(X0)),X0),
inference(superposition,[],[f252,f99]) ).
fof(f852,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f820,f9]) ).
fof(f858,plain,
! [X0] : antidomain(X0) = antidomain(antidomain(antidomain(X0))),
inference(backward_demodulation,[],[f491,f852]) ).
fof(f877,plain,
sF0 = antidomain(antidomain(sF0)),
inference(superposition,[],[f858,f54]) ).
fof(f878,plain,
sF1 = antidomain(antidomain(sF1)),
inference(superposition,[],[f858,f56]) ).
fof(f879,plain,
sF2 = antidomain(antidomain(sF2)),
inference(superposition,[],[f858,f58]) ).
fof(f881,plain,
sF4 = antidomain(antidomain(sF4)),
inference(superposition,[],[f858,f62]) ).
fof(f884,plain,
sF8 = antidomain(antidomain(sF8)),
inference(superposition,[],[f858,f70]) ).
fof(f886,plain,
sF10 = antidomain(antidomain(sF10)),
inference(superposition,[],[f858,f74]) ).
fof(f905,plain,
sF10 = antidomain(sF11),
inference(forward_demodulation,[],[f886,f76]) ).
fof(f907,plain,
sF8 = antidomain(sF9),
inference(forward_demodulation,[],[f884,f72]) ).
fof(f910,plain,
sF4 = antidomain(sF5),
inference(forward_demodulation,[],[f881,f64]) ).
fof(f912,plain,
sF2 = antidomain(sF3),
inference(forward_demodulation,[],[f879,f60]) ).
fof(f913,plain,
sF1 = antidomain(sF2),
inference(forward_demodulation,[],[f878,f58]) ).
fof(f914,plain,
sF0 = antidomain(sF1),
inference(forward_demodulation,[],[f877,f56]) ).
fof(f920,plain,
sF10 = sF12,
inference(backward_demodulation,[],[f78,f905]) ).
fof(f922,plain,
sF8 = sF10,
inference(backward_demodulation,[],[f74,f907]) ).
fof(f927,plain,
sF4 = sF6,
inference(backward_demodulation,[],[f66,f910]) ).
fof(f929,plain,
sF2 = sF4,
inference(backward_demodulation,[],[f62,f912]) ).
fof(f930,plain,
sF1 = sF3,
inference(forward_demodulation,[],[f913,f60]) ).
fof(f931,plain,
sF0 = sF2,
inference(backward_demodulation,[],[f58,f914]) ).
fof(f938,plain,
sF10 = addition(sF14,sF10),
inference(backward_demodulation,[],[f101,f920]) ).
fof(f973,plain,
sF7 = multiplication(sK3_goals_X0,sF4),
inference(backward_demodulation,[],[f68,f927]) ).
fof(f981,plain,
! [X0] : addition(sF7,multiplication(X0,sF4)) = multiplication(addition(X0,sK3_goals_X0),sF4),
inference(backward_demodulation,[],[f248,f927]) ).
fof(f1007,plain,
! [X0] : multiplication(X0,sF3) = multiplication(addition(sF2,X0),sF3),
inference(backward_demodulation,[],[f811,f929]) ).
fof(f1011,plain,
sF21 = addition(sF20,sF3),
inference(backward_demodulation,[],[f97,f930]) ).
fof(f1012,plain,
sF3 != sF21,
inference(backward_demodulation,[],[f98,f930]) ).
fof(f1023,plain,
one = addition(sF0,sF3),
inference(backward_demodulation,[],[f383,f930]) ).
fof(f1037,plain,
! [X0] : addition(one,X0) = addition(sF0,addition(sF3,X0)),
inference(backward_demodulation,[],[f648,f930]) ).
fof(f1048,plain,
! [X0] : multiplication(X0,sF0) = multiplication(addition(sF3,X0),sF0),
inference(backward_demodulation,[],[f808,f930]) ).
fof(f1076,plain,
sF0 = sF4,
inference(backward_demodulation,[],[f929,f931]) ).
fof(f1089,plain,
sF8 = addition(sF14,sF8),
inference(forward_demodulation,[],[f938,f922]) ).
fof(f1110,plain,
! [X0] : multiplication(X0,sF3) = multiplication(addition(sF0,X0),sF3),
inference(forward_demodulation,[],[f1007,f931]) ).
fof(f1132,plain,
sF21 = addition(sF3,sF20),
inference(forward_demodulation,[],[f1011,f3]) ).
fof(f1134,plain,
sF7 = multiplication(sK3_goals_X0,sF0),
inference(backward_demodulation,[],[f973,f1076]) ).
fof(f1139,plain,
! [X0] : addition(sF7,multiplication(X0,sF0)) = multiplication(addition(X0,sK3_goals_X0),sF0),
inference(backward_demodulation,[],[f981,f1076]) ).
fof(f1559,plain,
one = addition(one,sF16),
inference(superposition,[],[f642,f87]) ).
fof(f1560,plain,
one = addition(one,sF17),
inference(superposition,[],[f642,f89]) ).
fof(f1562,plain,
one = addition(one,sF20),
inference(superposition,[],[f642,f95]) ).
fof(f1573,plain,
one = addition(sF20,one),
inference(forward_demodulation,[],[f1562,f3]) ).
fof(f1575,plain,
one = addition(sF17,one),
inference(forward_demodulation,[],[f1560,f3]) ).
fof(f1576,plain,
one = addition(sF16,one),
inference(forward_demodulation,[],[f1559,f3]) ).
fof(f1579,plain,
addition(sF18,sK3_goals_X0) = multiplication(one,sK3_goals_X0),
inference(backward_demodulation,[],[f736,f1575]) ).
fof(f1580,plain,
sK3_goals_X0 = addition(sF18,sK3_goals_X0),
inference(forward_demodulation,[],[f1579,f9]) ).
fof(f1593,plain,
one = addition(one,sF13),
inference(superposition,[],[f643,f80]) ).
fof(f1596,plain,
one = addition(one,sF8),
inference(superposition,[],[f643,f70]) ).
fof(f1611,plain,
one = addition(sF8,one),
inference(forward_demodulation,[],[f1596,f3]) ).
fof(f1614,plain,
one = addition(sF13,one),
inference(forward_demodulation,[],[f1593,f3]) ).
fof(f1718,plain,
! [X0] : multiplication(X0,one) = multiplication(X0,coantidomain(coantidomain(X0))),
inference(superposition,[],[f199,f100]) ).
fof(f1766,plain,
! [X0] : multiplication(X0,coantidomain(coantidomain(X0))) = X0,
inference(forward_demodulation,[],[f1718,f8]) ).
fof(f1771,plain,
! [X0] : coantidomain(X0) = coantidomain(coantidomain(coantidomain(X0))),
inference(backward_demodulation,[],[f394,f1766]) ).
fof(f1780,plain,
sF14 = multiplication(sF14,coantidomain(sF16)),
inference(superposition,[],[f1766,f87]) ).
fof(f1786,plain,
one = coantidomain(coantidomain(one)),
inference(superposition,[],[f9,f1766]) ).
fof(f1816,plain,
one = coantidomain(zero),
inference(forward_demodulation,[],[f1786,f439]) ).
fof(f1819,plain,
sF14 = multiplication(sF14,sF17),
inference(forward_demodulation,[],[f1780,f89]) ).
fof(f2026,plain,
! [X0,X1] : multiplication(multiplication(coantidomain(coantidomain(X0)),X1),coantidomain(multiplication(X0,X1))) = multiplication(multiplication(coantidomain(coantidomain(X0)),X1),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))),
inference(superposition,[],[f133,f30]) ).
fof(f2073,plain,
! [X0,X1] : zero = multiplication(multiplication(coantidomain(coantidomain(X0)),X1),coantidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f2026,f28]) ).
fof(f2084,plain,
! [X0,X1] : zero = multiplication(coantidomain(coantidomain(X0)),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f2073,f7]) ).
fof(f2131,plain,
! [X2,X0,X1] : multiplication(addition(coantidomain(coantidomain(X0)),X1),multiplication(X2,coantidomain(multiplication(X0,X2)))) = addition(zero,multiplication(X1,multiplication(X2,coantidomain(multiplication(X0,X2))))),
inference(superposition,[],[f11,f2084]) ).
fof(f2137,plain,
! [X2,X0,X1] : multiplication(X1,multiplication(X2,coantidomain(multiplication(X0,X2)))) = multiplication(addition(coantidomain(coantidomain(X0)),X1),multiplication(X2,coantidomain(multiplication(X0,X2)))),
inference(forward_demodulation,[],[f2131,f198]) ).
fof(f2260,plain,
sF7 = multiplication(antidomain(sF8),sF7),
inference(superposition,[],[f852,f70]) ).
fof(f2295,plain,
sF7 = multiplication(sF9,sF7),
inference(forward_demodulation,[],[f2260,f72]) ).
fof(f2772,plain,
! [X0] : multiplication(addition(sF9,X0),sF7) = addition(sF7,multiplication(X0,sF7)),
inference(superposition,[],[f11,f2295]) ).
fof(f2782,plain,
! [X0] : multiplication(addition(sF9,X0),sF7) = multiplication(addition(one,X0),sF7),
inference(forward_demodulation,[],[f2772,f433]) ).
fof(f3115,plain,
! [X0] : addition(one,X0) = addition(sF14,addition(sF13,X0)),
inference(superposition,[],[f4,f386]) ).
fof(f3119,plain,
multiplication(sF14,coantidomain(sF13)) = multiplication(one,coantidomain(sF13)),
inference(superposition,[],[f251,f386]) ).
fof(f3120,plain,
multiplication(sF13,coantidomain(sF14)) = multiplication(one,coantidomain(sF14)),
inference(superposition,[],[f253,f386]) ).
fof(f3127,plain,
coantidomain(sF14) = multiplication(sF13,coantidomain(sF14)),
inference(forward_demodulation,[],[f3120,f9]) ).
fof(f3128,plain,
coantidomain(sF13) = multiplication(sF14,coantidomain(sF13)),
inference(forward_demodulation,[],[f3119,f9]) ).
fof(f3131,plain,
sF16 = multiplication(sF13,sF16),
inference(forward_demodulation,[],[f3127,f87]) ).
fof(f3631,plain,
multiplication(sF13,addition(one,sF16)) = addition(sF13,sF16),
inference(superposition,[],[f328,f3131]) ).
fof(f3692,plain,
addition(sF13,sF16) = multiplication(sF13,addition(sF16,one)),
inference(forward_demodulation,[],[f3631,f3]) ).
fof(f3740,plain,
addition(sF13,sF16) = multiplication(sF13,one),
inference(forward_demodulation,[],[f3692,f1576]) ).
fof(f3776,plain,
sF13 = addition(sF13,sF16),
inference(forward_demodulation,[],[f3740,f8]) ).
fof(f4085,plain,
! [X0] : addition(sF8,X0) = addition(sF8,addition(sF14,X0)),
inference(superposition,[],[f398,f1089]) ).
fof(f4148,plain,
! [X0] : addition(sF8,X0) = addition(sF14,addition(X0,sF8)),
inference(forward_demodulation,[],[f4085,f417]) ).
fof(f5544,plain,
multiplication(sF20,sF0) = multiplication(sF21,sF0),
inference(superposition,[],[f1048,f1132]) ).
fof(f5732,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = multiplication(X0,addition(X2,X1)),
inference(superposition,[],[f10,f141]) ).
fof(f5983,plain,
addition(one,sF20) = addition(sF0,sF21),
inference(superposition,[],[f1037,f1132]) ).
fof(f6027,plain,
addition(sF20,one) = addition(sF0,sF21),
inference(forward_demodulation,[],[f5983,f3]) ).
fof(f6034,plain,
one = addition(sF0,sF21),
inference(forward_demodulation,[],[f6027,f1573]) ).
fof(f6038,plain,
multiplication(one,sF3) = multiplication(sF21,sF3),
inference(superposition,[],[f1110,f6034]) ).
fof(f6064,plain,
sF3 = multiplication(sF21,sF3),
inference(forward_demodulation,[],[f6038,f9]) ).
fof(f6856,plain,
addition(one,sF8) = addition(sF8,sF13),
inference(superposition,[],[f4148,f3115]) ).
fof(f6879,plain,
addition(sF8,one) = addition(sF8,sF13),
inference(forward_demodulation,[],[f6856,f3]) ).
fof(f6891,plain,
one = addition(sF8,sF13),
inference(forward_demodulation,[],[f6879,f1611]) ).
fof(f6905,plain,
multiplication(one,coantidomain(sF13)) = multiplication(sF8,coantidomain(sF13)),
inference(superposition,[],[f251,f6891]) ).
fof(f6920,plain,
coantidomain(sF13) = multiplication(sF8,coantidomain(sF13)),
inference(forward_demodulation,[],[f6905,f9]) ).
fof(f7305,plain,
multiplication(sF18,sF0) = multiplication(sF17,sF7),
inference(superposition,[],[f550,f1134]) ).
fof(f7383,plain,
multiplication(addition(sF18,sK3_goals_X0),sF0) = addition(sF7,multiplication(sF17,sF7)),
inference(superposition,[],[f1139,f7305]) ).
fof(f7405,plain,
zero = multiplication(coantidomain(coantidomain(sF18)),multiplication(sF0,coantidomain(multiplication(sF17,sF7)))),
inference(superposition,[],[f2084,f7305]) ).
fof(f7406,plain,
zero = multiplication(coantidomain(sF19),multiplication(sF0,coantidomain(multiplication(sF17,sF7)))),
inference(forward_demodulation,[],[f7405,f93]) ).
fof(f7421,plain,
multiplication(addition(sF18,sK3_goals_X0),sF0) = multiplication(addition(one,sF17),sF7),
inference(forward_demodulation,[],[f7383,f433]) ).
fof(f7422,plain,
zero = multiplication(sF20,multiplication(sF0,coantidomain(multiplication(sF17,sF7)))),
inference(forward_demodulation,[],[f7406,f95]) ).
fof(f7435,plain,
multiplication(addition(sF18,sK3_goals_X0),sF0) = multiplication(addition(sF9,sF17),sF7),
inference(forward_demodulation,[],[f7421,f2782]) ).
fof(f7444,plain,
multiplication(sK3_goals_X0,sF0) = multiplication(addition(sF9,sF17),sF7),
inference(forward_demodulation,[],[f7435,f1580]) ).
fof(f7448,plain,
sF7 = multiplication(addition(sF9,sF17),sF7),
inference(forward_demodulation,[],[f7444,f1134]) ).
fof(f7509,plain,
! [X0,X1] : multiplication(one,multiplication(X1,coantidomain(multiplication(X0,X1)))) = multiplication(coantidomain(coantidomain(coantidomain(X0))),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(superposition,[],[f2137,f100]) ).
fof(f7690,plain,
! [X0,X1] : multiplication(one,multiplication(X1,coantidomain(multiplication(X0,X1)))) = multiplication(coantidomain(X0),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f7509,f1771]) ).
fof(f7748,plain,
! [X0,X1] : multiplication(X1,coantidomain(multiplication(X0,X1))) = multiplication(coantidomain(X0),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f7690,f9]) ).
fof(f7810,plain,
! [X0] : multiplication(X0,coantidomain(zero)) = multiplication(coantidomain(antidomain(X0)),multiplication(X0,coantidomain(zero))),
inference(superposition,[],[f7748,f20]) ).
fof(f7937,plain,
! [X0] : multiplication(X0,one) = multiplication(coantidomain(antidomain(X0)),multiplication(X0,one)),
inference(forward_demodulation,[],[f7810,f1816]) ).
fof(f7974,plain,
! [X0] : multiplication(coantidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f7937,f8]) ).
fof(f8003,plain,
sF13 = multiplication(coantidomain(sF14),sF13),
inference(superposition,[],[f7974,f82]) ).
fof(f8069,plain,
sF13 = multiplication(sF16,sF13),
inference(forward_demodulation,[],[f8003,f87]) ).
fof(f8117,plain,
addition(sF16,sF13) = multiplication(sF16,addition(one,sF13)),
inference(superposition,[],[f328,f8069]) ).
fof(f8135,plain,
addition(sF16,sF13) = multiplication(sF16,addition(sF13,one)),
inference(forward_demodulation,[],[f8117,f5732]) ).
fof(f8148,plain,
multiplication(sF16,one) = addition(sF16,sF13),
inference(forward_demodulation,[],[f8135,f1614]) ).
fof(f8157,plain,
multiplication(sF16,one) = addition(sF13,sF16),
inference(forward_demodulation,[],[f8148,f3]) ).
fof(f8161,plain,
sF13 = multiplication(sF16,one),
inference(forward_demodulation,[],[f8157,f3776]) ).
fof(f8163,plain,
sF13 = sF16,
inference(forward_demodulation,[],[f8161,f8]) ).
fof(f8165,plain,
sF17 = coantidomain(sF13),
inference(backward_demodulation,[],[f89,f8163]) ).
fof(f8327,plain,
sF17 = multiplication(sF14,sF17),
inference(backward_demodulation,[],[f3128,f8165]) ).
fof(f8329,plain,
sF17 = multiplication(sF8,sF17),
inference(backward_demodulation,[],[f6920,f8165]) ).
fof(f8356,plain,
sF14 = sF17,
inference(forward_demodulation,[],[f8327,f1819]) ).
fof(f8462,plain,
zero = multiplication(sF20,multiplication(sF0,coantidomain(multiplication(sF14,sF7)))),
inference(backward_demodulation,[],[f7422,f8356]) ).
fof(f8465,plain,
sF7 = multiplication(addition(sF9,sF14),sF7),
inference(backward_demodulation,[],[f7448,f8356]) ).
fof(f8547,plain,
sF14 = multiplication(sF8,sF14),
inference(backward_demodulation,[],[f8329,f8356]) ).
fof(f8572,plain,
sF7 = multiplication(addition(sF14,sF9),sF7),
inference(forward_demodulation,[],[f8465,f3]) ).
fof(f8706,plain,
! [X0] : multiplication(sF14,X0) = multiplication(sF8,multiplication(sF14,X0)),
inference(superposition,[],[f7,f8547]) ).
fof(f9090,plain,
multiplication(antidomain(multiplication(sF9,sF7)),multiplication(sF14,sF7)) = multiplication(antidomain(multiplication(sF9,sF7)),sF7),
inference(superposition,[],[f467,f8572]) ).
fof(f9091,plain,
multiplication(antidomain(sF7),sF7) = multiplication(antidomain(sF7),multiplication(sF14,sF7)),
inference(forward_demodulation,[],[f9090,f2295]) ).
fof(f9108,plain,
multiplication(sF8,sF7) = multiplication(sF8,multiplication(sF14,sF7)),
inference(forward_demodulation,[],[f9091,f70]) ).
fof(f9118,plain,
multiplication(sF8,sF7) = multiplication(sF14,sF7),
inference(forward_demodulation,[],[f9108,f8706]) ).
fof(f9123,plain,
zero = multiplication(sF14,sF7),
inference(forward_demodulation,[],[f9118,f182]) ).
fof(f9134,plain,
zero = multiplication(sF20,multiplication(sF0,coantidomain(zero))),
inference(backward_demodulation,[],[f8462,f9123]) ).
fof(f9143,plain,
zero = multiplication(sF20,multiplication(sF0,one)),
inference(forward_demodulation,[],[f9134,f1816]) ).
fof(f9152,plain,
zero = multiplication(sF20,sF0),
inference(forward_demodulation,[],[f9143,f8]) ).
fof(f9160,plain,
zero = multiplication(sF21,sF0),
inference(backward_demodulation,[],[f5544,f9152]) ).
fof(f9920,plain,
! [X0] : multiplication(sF21,addition(sF0,X0)) = addition(multiplication(sF21,X0),zero),
inference(superposition,[],[f141,f9160]) ).
fof(f9946,plain,
! [X0] : multiplication(sF21,X0) = multiplication(sF21,addition(sF0,X0)),
inference(forward_demodulation,[],[f9920,f5]) ).
fof(f10129,plain,
multiplication(sF21,one) = multiplication(sF21,sF3),
inference(superposition,[],[f9946,f1023]) ).
fof(f10176,plain,
sF3 = multiplication(sF21,one),
inference(forward_demodulation,[],[f10129,f6064]) ).
fof(f10182,plain,
sF3 = sF21,
inference(forward_demodulation,[],[f10176,f8]) ).
fof(f10185,plain,
$false,
inference(forward_subsumption_resolution,[],[f10182,f1012]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE108-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n007.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 13:08:40 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.39/2.79 % (1403842)Detected a unit-equality problem, will run specialized UEQ schedule.
% 13.39/2.79 % (1403852)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=4146605640:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 13.39/2.79 % (1403851)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1532003705:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 13.39/2.79 % (1403850)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3660191850:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 13.39/2.79 % (1403848)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3154903727:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 13.39/2.79 % (1403847)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=95718914:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 13.39/2.79 % (1403849)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=417637961:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 13.39/2.79 % (1403853)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2589806317:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 13.39/2.79 % (1403852)Instruction limit reached!
% 13.39/2.79 % (1403852)------------------------------
% 13.39/2.79 % (1403852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.79 % (1403852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.79 % (1403852)CaDiCaL version: 2.1.3
% 13.39/2.79 % (1403852)Termination reason: Instruction limit
% 13.39/2.79 % (1403852)Termination phase: Saturation
% 13.39/2.79 % (1403852)Time elapsed: 0.093 s
% 13.39/2.79 % (1403852)Peak memory usage: 91 MB
% 13.39/2.79 % (1403852)Instructions burned: 260 (million)
% 13.39/2.79 % (1403850)Instruction limit reached!
% 13.39/2.79 % (1403850)------------------------------
% 13.39/2.79 % (1403850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.79 % (1403850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.79 % (1403850)CaDiCaL version: 2.1.3
% 13.39/2.79 % (1403850)Termination reason: Instruction limit
% 13.39/2.79 % (1403850)Termination phase: Saturation
% 13.39/2.79 % (1403850)Time elapsed: 0.084 s
% 13.39/2.79 % (1403850)Peak memory usage: 89 MB
% 13.39/2.79 % (1403850)Instructions burned: 137 (million)
% 13.39/2.79 % (1403851)Instruction limit reached!
% 13.39/2.79 % (1403851)------------------------------
% 13.39/2.79 % (1403851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.79 % (1403851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.79 % (1403851)CaDiCaL version: 2.1.3
% 13.39/2.79 % (1403851)Termination reason: Instruction limit
% 13.39/2.79 % (1403851)Termination phase: Saturation
% 13.39/2.79 % (1403851)Time elapsed: 0.105 s
% 13.39/2.79 % (1403851)Peak memory usage: 90 MB
% 13.39/2.79 % (1403851)Instructions burned: 183 (million)
% 13.39/2.79 % (1403861)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1299161003:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 13.39/2.79 % (1403862)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=437729086:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 13.39/2.79 % (1403863)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1348352047:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 13.39/2.79 % (1403863)Instruction limit reached!
% 13.39/2.79 % (1403863)------------------------------
% 13.39/2.79 % (1403863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.79 % (1403863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.79 % (1403863)CaDiCaL version: 2.1.3
% 13.39/2.79 % (1403863)Termination reason: Instruction limit
% 13.39/2.79 % (1403863)Termination phase: Saturation
% 13.39/2.79 % (1403863)Time elapsed: 0.114 s
% 13.39/2.79 % (1403863)Peak memory usage: 93 MB
% 13.39/2.79 % (1403863)Instructions burned: 217 (million)
% 13.39/2.79 % (1403867)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=2964774882:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2995 on theBenchmark for (2995ds/317Mi)
% 13.39/2.79 % (1403853)Instruction limit reached!
% 13.39/2.79 % (1403853)------------------------------
% 13.39/2.79 % (1403853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.79 % (1403853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.79 % (1403853)CaDiCaL version: 2.1.3
% 13.39/2.79 % (1403853)Termination reason: Instruction limit
% 13.39/2.79 % (1403853)Termination phase: Saturation
% 13.39/2.79 % (1403853)Time elapsed: 0.640 s
% 13.39/2.79 % (1403853)Peak memory usage: 101 MB
% 13.39/2.79 % (1403853)Instructions burned: 1187 (million)
% 13.39/2.79 % (1403867)Instruction limit reached!
% 13.39/2.79 % (1403867)------------------------------
% 13.39/2.79 % (1403867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.79 % (1403867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.79 % (1403867)CaDiCaL version: 2.1.3
% 13.39/2.79 % (1403867)Termination reason: Instruction limit
% 13.39/2.79 % (1403867)Termination phase: Saturation
% 13.39/2.79 % (1403867)Time elapsed: 0.184 s
% 13.39/2.79 % (1403867)Peak memory usage: 94 MB
% 13.39/2.79 % (1403867)Instructions burned: 318 (million)
% 13.39/2.79 % (1403869)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=4009008893:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 13.39/2.79 % (1403870)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3765774843:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 13.39/2.79 % (1403861)Instruction limit reached!
% 13.39/2.79 % (1403861)------------------------------
% 13.39/2.79 % (1403861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.79 % (1403861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.79 % (1403861)CaDiCaL version: 2.1.3
% 13.39/2.79 % (1403861)Termination reason: Instruction limit
% 13.39/2.79 % (1403861)Termination phase: Saturation
% 13.39/2.79 % (1403861)Time elapsed: 0.751 s
% 13.39/2.79 % (1403861)Peak memory usage: 143 MB
% 13.39/2.79 % (1403861)Instructions burned: 2053 (million)
% 13.39/2.79 % (1403873)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1021850086:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 13.39/2.79 % (1403849)First to succeed.
% 13.39/2.79 % (1403849)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1403842"
% 13.39/2.79 % (1403849)Refutation found. Thanks to Tanya!
% 13.39/2.79 % SZS status Unsatisfiable for theBenchmark
% 13.39/2.79 % SZS output start Proof for theBenchmark
% See solution above
% 14.21/2.98 % (1403849)------------------------------
% 14.21/2.98 % (1403849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.21/2.98 % (1403849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.21/2.98 % (1403849)CaDiCaL version: 2.1.3
% 14.21/2.98 % (1403849)Termination reason: Refutation
% 14.21/2.98 % (1403849)Time elapsed: 1.521 s
% 14.21/2.98 % (1403849)Peak memory usage: 144 MB
% 14.21/2.98 % (1403849)Instructions burned: 2415 (million)
% 14.21/2.98 % (1403849)------------------------------
% 14.21/2.98 % (1403849)------------------------------
% 14.21/2.98 % (1403842)Success in time 1.923 s
% 14.21/2.98 % Vampire exiting
%------------------------------------------------------------------------------