%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE110-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.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:22 AM UTC 2026
% Result : Unsatisfiable 9.44s 2.17s
% Output : Refutation 9.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 41
% Syntax : Number of formulae : 249 ( 249 unt; 19 def)
% Number of atoms : 249 ( 248 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 20 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 23 con; 0-2 aty)
% Number of variables : 142 ( 142 !; 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(f21,axiom,
! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain2) ).
fof(f22,plain,
! [X0,X1] : antidomain(multiplication(X0,antidomain(antidomain(X1)))) = addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(reorient_equations,[],[f21]) ).
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(f40,negated_conjecture,
! [X0,X1] : backward_box(X0,X1) = c(backward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',backward_box) ).
fof(f41,negated_conjecture,
addition(domain(sK2_goals_X0),backward_box(sK1_goals_X1,forward_diamond(sK1_goals_X1,domain(sK2_goals_X0)))) != backward_box(sK1_goals_X1,forward_diamond(sK1_goals_X1,domain(sK2_goals_X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f42,plain,
backward_box(sK1_goals_X1,forward_diamond(sK1_goals_X1,domain(sK2_goals_X0))) != addition(domain(sK2_goals_X0),backward_box(sK1_goals_X1,forward_diamond(sK1_goals_X1,domain(sK2_goals_X0)))),
inference(reorient_equations,[],[f41]) ).
fof(f44,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f37,f26,f26]) ).
fof(f45,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f38,f34,f34]) ).
fof(f46,plain,
! [X0] : c(X0) = antidomain(antidomain(antidomain(X0))),
inference(definition_unfolding,[],[f35,f26]) ).
fof(f48,plain,
! [X0,X1] : backward_box(X0,X1) = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X0)))))),
inference(definition_unfolding,[],[f40,f46,f45,f46]) ).
fof(f49,plain,
antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))) != addition(antidomain(antidomain(sK2_goals_X0)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1))))))),
inference(definition_unfolding,[],[f42,f48,f44,f26,f26,f48,f44,f26]) ).
fof(f50,definition,
sF0 = antidomain(sK2_goals_X0),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f51,plain,
antidomain(sK2_goals_X0) = sF0,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF1 = antidomain(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f53,plain,
antidomain(sF0) = sF1,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF2 = antidomain(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f55,plain,
antidomain(sF1) = sF2,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF3 = antidomain(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f57,plain,
antidomain(sF2) = sF3,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF4 = multiplication(sK1_goals_X1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f59,plain,
multiplication(sK1_goals_X1,sF3) = sF4,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF5 = antidomain(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f61,plain,
antidomain(sF4) = sF5,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF6 = antidomain(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f63,plain,
antidomain(sF5) = sF6,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF7 = antidomain(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f65,plain,
antidomain(sF6) = sF7,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF8 = antidomain(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f67,plain,
antidomain(sF7) = sF8,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF9 = antidomain(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f69,plain,
antidomain(sF8) = sF9,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF10 = coantidomain(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f71,plain,
coantidomain(sF9) = sF10,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF11 = coantidomain(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f73,plain,
coantidomain(sF10) = sF11,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF12 = multiplication(sF11,sK1_goals_X1),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f75,plain,
multiplication(sF11,sK1_goals_X1) = sF12,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF13 = coantidomain(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f77,plain,
coantidomain(sF12) = sF13,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF14 = coantidomain(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f79,plain,
coantidomain(sF13) = sF14,
inference(reorient_equations,[],[f78]) ).
fof(f80,definition,
sF15 = antidomain(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f81,plain,
antidomain(sF14) = sF15,
inference(reorient_equations,[],[f80]) ).
fof(f82,definition,
sF16 = antidomain(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f83,plain,
antidomain(sF15) = sF16,
inference(reorient_equations,[],[f82]) ).
fof(f84,definition,
sF17 = antidomain(sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f85,plain,
antidomain(sF16) = sF17,
inference(reorient_equations,[],[f84]) ).
fof(f86,definition,
sF18 = addition(sF1,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f87,plain,
addition(sF1,sF17) = sF18,
inference(reorient_equations,[],[f86]) ).
fof(f88,plain,
sF17 != sF18,
inference(definition_folding,[],[f49,f87,f85,f83,f81,f79,f77,f75,f73,f71,f69,f67,f65,f63,f61,f59,f57,f55,f53,f51,f53,f51,f85,f83,f81,f79,f77,f75,f73,f71,f69,f67,f65,f63,f61,f59,f57,f55,f53,f51]) ).
fof(f89,plain,
! [X0] : one = addition(antidomain(X0),antidomain(antidomain(X0))),
inference(backward_demodulation,[],[f24,f3]) ).
fof(f90,plain,
! [X0] : one = addition(coantidomain(X0),coantidomain(coantidomain(X0))),
inference(backward_demodulation,[],[f32,f3]) ).
fof(f109,plain,
! [X0,X1] : multiplication(X0,addition(coantidomain(X0),X1)) = addition(zero,multiplication(X0,X1)),
inference(superposition,[],[f10,f28]) ).
fof(f112,plain,
! [X0,X1] : multiplication(X0,addition(X1,coantidomain(X0))) = addition(multiplication(X0,X1),zero),
inference(superposition,[],[f10,f28]) ).
fof(f117,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(X0,addition(X1,coantidomain(X0))),
inference(forward_demodulation,[],[f112,f5]) ).
fof(f161,plain,
zero = multiplication(sF5,sF4),
inference(superposition,[],[f20,f61]) ).
fof(f162,plain,
zero = multiplication(sF6,sF5),
inference(superposition,[],[f20,f63]) ).
fof(f163,plain,
zero = multiplication(sF7,sF6),
inference(superposition,[],[f20,f65]) ).
fof(f170,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X1,X0)) = addition(multiplication(antidomain(X0),X1),zero),
inference(superposition,[],[f10,f20]) ).
fof(f171,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X0,X1)) = addition(zero,multiplication(antidomain(X0),X1)),
inference(superposition,[],[f10,f20]) ).
fof(f175,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X1,X0)) = multiplication(antidomain(X0),X1),
inference(forward_demodulation,[],[f170,f5]) ).
fof(f179,plain,
! [X0] : addition(zero,X0) = X0,
inference(superposition,[],[f3,f5]) ).
fof(f180,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(X0,addition(coantidomain(X0),X1)),
inference(backward_demodulation,[],[f109,f179]) ).
fof(f181,plain,
! [X0,X1] : multiplication(antidomain(X0),X1) = multiplication(antidomain(X0),addition(X0,X1)),
inference(backward_demodulation,[],[f171,f179]) ).
fof(f210,plain,
one = addition(sF13,coantidomain(sF13)),
inference(superposition,[],[f90,f77]) ).
fof(f214,plain,
one = addition(sF13,sF14),
inference(forward_demodulation,[],[f210,f79]) ).
fof(f220,plain,
one = addition(sF5,antidomain(sF5)),
inference(superposition,[],[f89,f61]) ).
fof(f225,plain,
one = addition(sF15,antidomain(sF15)),
inference(superposition,[],[f89,f81]) ).
fof(f226,plain,
one = addition(sF16,antidomain(sF16)),
inference(superposition,[],[f89,f83]) ).
fof(f230,plain,
one = addition(sF16,sF17),
inference(forward_demodulation,[],[f226,f85]) ).
fof(f231,plain,
one = addition(sF15,sF16),
inference(forward_demodulation,[],[f225,f83]) ).
fof(f235,plain,
one = addition(sF5,sF6),
inference(forward_demodulation,[],[f220,f63]) ).
fof(f241,plain,
zero = antidomain(one),
inference(superposition,[],[f20,f8]) ).
fof(f248,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(superposition,[],[f10,f8]) ).
fof(f267,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X0)) = addition(zero,multiplication(X1,coantidomain(X0))),
inference(superposition,[],[f11,f28]) ).
fof(f269,plain,
! [X0,X1] : multiplication(addition(antidomain(X0),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(superposition,[],[f11,f20]) ).
fof(f273,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = addition(multiplication(X0,coantidomain(X1)),zero),
inference(superposition,[],[f11,f28]) ).
fof(f275,plain,
! [X0,X1] : addition(multiplication(X0,X1),zero) = multiplication(addition(X0,antidomain(X1)),X1),
inference(superposition,[],[f11,f20]) ).
fof(f291,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(addition(X0,antidomain(X1)),X1),
inference(forward_demodulation,[],[f275,f5]) ).
fof(f293,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = multiplication(X0,coantidomain(X1)),
inference(forward_demodulation,[],[f273,f5]) ).
fof(f294,plain,
! [X0,X1] : multiplication(addition(antidomain(X0),X1),X0) = multiplication(X1,X0),
inference(forward_demodulation,[],[f269,f179]) ).
fof(f296,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X0)) = multiplication(X1,coantidomain(X0)),
inference(forward_demodulation,[],[f267,f179]) ).
fof(f311,plain,
! [X0,X1] : multiplication(antidomain(multiplication(X0,X1)),multiplication(X0,antidomain(antidomain(X1)))) = multiplication(antidomain(multiplication(X0,antidomain(antidomain(X1)))),multiplication(X0,antidomain(antidomain(X1)))),
inference(superposition,[],[f291,f22]) ).
fof(f329,plain,
! [X0,X1] : zero = multiplication(antidomain(multiplication(X0,X1)),multiplication(X0,antidomain(antidomain(X1)))),
inference(forward_demodulation,[],[f311,f20]) ).
fof(f342,plain,
! [X0] : multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))) = multiplication(one,coantidomain(coantidomain(coantidomain(X0)))),
inference(superposition,[],[f293,f90]) ).
fof(f357,plain,
! [X0] : coantidomain(coantidomain(coantidomain(X0))) = multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f342,f9]) ).
fof(f389,plain,
! [X0] : addition(sF1,addition(sF17,X0)) = addition(sF18,X0),
inference(superposition,[],[f4,f87]) ).
fof(f396,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(superposition,[],[f3,f4]) ).
fof(f401,plain,
! [X0] : addition(one,X0) = addition(sF16,addition(sF17,X0)),
inference(superposition,[],[f4,f230]) ).
fof(f419,plain,
! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)),
inference(superposition,[],[f11,f9]) ).
fof(f425,plain,
zero = coantidomain(one),
inference(superposition,[],[f28,f9]) ).
fof(f453,plain,
! [X0] : multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)) = multiplication(antidomain(antidomain(antidomain(X0))),one),
inference(superposition,[],[f175,f89]) ).
fof(f474,plain,
! [X0] : antidomain(antidomain(antidomain(X0))) = multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)),
inference(forward_demodulation,[],[f453,f8]) ).
fof(f481,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f4,f6]) ).
fof(f495,plain,
! [X0] : multiplication(sF12,X0) = multiplication(sF11,multiplication(sK1_goals_X1,X0)),
inference(superposition,[],[f7,f75]) ).
fof(f572,plain,
! [X0] : multiplication(one,X0) = multiplication(antidomain(antidomain(X0)),X0),
inference(superposition,[],[f294,f89]) ).
fof(f598,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f572,f9]) ).
fof(f602,plain,
! [X0] : antidomain(X0) = antidomain(antidomain(antidomain(X0))),
inference(backward_demodulation,[],[f474,f598]) ).
fof(f614,plain,
sF1 = antidomain(antidomain(sF1)),
inference(superposition,[],[f602,f53]) ).
fof(f617,plain,
sF5 = antidomain(antidomain(sF5)),
inference(superposition,[],[f602,f61]) ).
fof(f619,plain,
sF7 = antidomain(antidomain(sF7)),
inference(superposition,[],[f602,f65]) ).
fof(f622,plain,
sF15 = antidomain(antidomain(sF15)),
inference(superposition,[],[f602,f81]) ).
fof(f640,plain,
sF15 = antidomain(sF16),
inference(forward_demodulation,[],[f622,f83]) ).
fof(f642,plain,
sF7 = antidomain(sF8),
inference(forward_demodulation,[],[f619,f67]) ).
fof(f644,plain,
sF5 = antidomain(sF6),
inference(forward_demodulation,[],[f617,f63]) ).
fof(f647,plain,
sF1 = antidomain(sF2),
inference(forward_demodulation,[],[f614,f55]) ).
fof(f655,plain,
sF15 = sF17,
inference(backward_demodulation,[],[f85,f640]) ).
fof(f659,plain,
sF7 = sF9,
inference(backward_demodulation,[],[f69,f642]) ).
fof(f661,plain,
sF5 = sF7,
inference(backward_demodulation,[],[f65,f644]) ).
fof(f666,plain,
sF1 = sF3,
inference(backward_demodulation,[],[f57,f647]) ).
fof(f670,plain,
sF18 = addition(sF1,sF15),
inference(backward_demodulation,[],[f87,f655]) ).
fof(f671,plain,
sF15 != sF18,
inference(backward_demodulation,[],[f88,f655]) ).
fof(f679,plain,
! [X0] : addition(sF18,X0) = addition(sF1,addition(sF15,X0)),
inference(backward_demodulation,[],[f389,f655]) ).
fof(f680,plain,
! [X0] : addition(one,X0) = addition(sF16,addition(sF15,X0)),
inference(backward_demodulation,[],[f401,f655]) ).
fof(f694,plain,
sF10 = coantidomain(sF7),
inference(backward_demodulation,[],[f71,f659]) ).
fof(f722,plain,
zero = multiplication(sF5,sF6),
inference(backward_demodulation,[],[f163,f661]) ).
fof(f733,plain,
sF4 = multiplication(sK1_goals_X1,sF1),
inference(backward_demodulation,[],[f59,f666]) ).
fof(f757,plain,
! [X0] : addition(one,X0) = addition(sF15,addition(X0,sF16)),
inference(forward_demodulation,[],[f680,f396]) ).
fof(f779,plain,
sF10 = coantidomain(sF5),
inference(forward_demodulation,[],[f694,f661]) ).
fof(f1049,plain,
! [X0] : multiplication(X0,one) = multiplication(X0,coantidomain(coantidomain(X0))),
inference(superposition,[],[f180,f90]) ).
fof(f1090,plain,
! [X0] : multiplication(X0,coantidomain(coantidomain(X0))) = X0,
inference(forward_demodulation,[],[f1049,f8]) ).
fof(f1094,plain,
! [X0] : coantidomain(X0) = coantidomain(coantidomain(coantidomain(X0))),
inference(backward_demodulation,[],[f357,f1090]) ).
fof(f1103,plain,
sF5 = multiplication(sF5,coantidomain(sF10)),
inference(superposition,[],[f1090,f779]) ).
fof(f1109,plain,
one = coantidomain(coantidomain(one)),
inference(superposition,[],[f9,f1090]) ).
fof(f1134,plain,
one = coantidomain(zero),
inference(forward_demodulation,[],[f1109,f425]) ).
fof(f1137,plain,
sF5 = multiplication(sF5,sF11),
inference(forward_demodulation,[],[f1103,f73]) ).
fof(f1178,plain,
sF13 = coantidomain(coantidomain(sF13)),
inference(superposition,[],[f1094,f77]) ).
fof(f1196,plain,
sF13 = coantidomain(sF14),
inference(forward_demodulation,[],[f1178,f79]) ).
fof(f1393,plain,
one = antidomain(antidomain(one)),
inference(superposition,[],[f8,f598]) ).
fof(f1397,plain,
one = antidomain(zero),
inference(forward_demodulation,[],[f1393,f241]) ).
fof(f2004,plain,
! [X0] : one = addition(antidomain(X0),one),
inference(superposition,[],[f481,f89]) ).
fof(f2008,plain,
! [X0] : one = addition(coantidomain(X0),one),
inference(superposition,[],[f481,f90]) ).
fof(f2009,plain,
sF18 = addition(sF1,sF18),
inference(superposition,[],[f481,f670]) ).
fof(f2035,plain,
! [X0] : one = addition(one,coantidomain(X0)),
inference(forward_demodulation,[],[f2008,f3]) ).
fof(f2036,plain,
! [X0] : one = addition(one,antidomain(X0)),
inference(forward_demodulation,[],[f2004,f3]) ).
fof(f2065,plain,
one = addition(one,sF1),
inference(superposition,[],[f2036,f53]) ).
fof(f2069,plain,
one = addition(one,sF16),
inference(superposition,[],[f2036,f83]) ).
fof(f2077,plain,
one = addition(sF16,one),
inference(forward_demodulation,[],[f2069,f3]) ).
fof(f2081,plain,
one = addition(sF1,one),
inference(forward_demodulation,[],[f2065,f3]) ).
fof(f2099,plain,
one = addition(one,sF11),
inference(superposition,[],[f2035,f73]) ).
fof(f2102,plain,
one = addition(one,sF14),
inference(superposition,[],[f2035,f79]) ).
fof(f2110,plain,
one = addition(sF14,one),
inference(forward_demodulation,[],[f2102,f3]) ).
fof(f2113,plain,
one = addition(sF11,one),
inference(forward_demodulation,[],[f2099,f3]) ).
fof(f2179,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,[],[f117,f30]) ).
fof(f2229,plain,
! [X0,X1] : zero = multiplication(multiplication(coantidomain(coantidomain(X0)),X1),coantidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f2179,f28]) ).
fof(f2242,plain,
! [X0,X1] : zero = multiplication(coantidomain(coantidomain(X0)),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f2229,f7]) ).
fof(f2291,plain,
zero = multiplication(coantidomain(coantidomain(sF5)),multiplication(sF6,coantidomain(zero))),
inference(superposition,[],[f2242,f722]) ).
fof(f2336,plain,
zero = multiplication(coantidomain(coantidomain(sF5)),multiplication(sF6,one)),
inference(forward_demodulation,[],[f2291,f1134]) ).
fof(f2369,plain,
zero = multiplication(coantidomain(coantidomain(sF5)),sF6),
inference(forward_demodulation,[],[f2336,f8]) ).
fof(f2382,plain,
zero = multiplication(coantidomain(sF10),sF6),
inference(forward_demodulation,[],[f2369,f779]) ).
fof(f2389,plain,
zero = multiplication(sF11,sF6),
inference(forward_demodulation,[],[f2382,f73]) ).
fof(f2396,plain,
! [X0] : addition(multiplication(sF11,X0),zero) = multiplication(sF11,addition(X0,sF6)),
inference(superposition,[],[f10,f2389]) ).
fof(f2413,plain,
! [X0] : multiplication(sF11,X0) = multiplication(sF11,addition(X0,sF6)),
inference(forward_demodulation,[],[f2396,f5]) ).
fof(f2743,plain,
multiplication(antidomain(sF14),sF13) = multiplication(antidomain(sF14),one),
inference(superposition,[],[f175,f214]) ).
fof(f2753,plain,
antidomain(sF14) = multiplication(antidomain(sF14),sF13),
inference(forward_demodulation,[],[f2743,f8]) ).
fof(f2756,plain,
sF15 = multiplication(sF15,sF13),
inference(forward_demodulation,[],[f2753,f81]) ).
fof(f2778,plain,
multiplication(sF11,one) = multiplication(sF11,sF5),
inference(superposition,[],[f2413,f235]) ).
fof(f2792,plain,
sF11 = multiplication(sF11,sF5),
inference(forward_demodulation,[],[f2778,f8]) ).
fof(f2928,plain,
addition(sF1,one) = addition(sF18,sF16),
inference(superposition,[],[f679,f231]) ).
fof(f2942,plain,
addition(sF1,one) = addition(sF16,sF18),
inference(forward_demodulation,[],[f2928,f3]) ).
fof(f2945,plain,
one = addition(sF16,sF18),
inference(forward_demodulation,[],[f2942,f2081]) ).
fof(f2949,plain,
multiplication(antidomain(sF16),one) = multiplication(antidomain(sF16),sF18),
inference(superposition,[],[f181,f2945]) ).
fof(f2957,plain,
multiplication(sF15,one) = multiplication(sF15,sF18),
inference(forward_demodulation,[],[f2949,f640]) ).
fof(f2959,plain,
sF15 = multiplication(sF15,sF18),
inference(forward_demodulation,[],[f2957,f8]) ).
fof(f2962,plain,
! [X0] : addition(multiplication(sF15,X0),sF15) = multiplication(sF15,addition(X0,sF18)),
inference(superposition,[],[f10,f2959]) ).
fof(f2977,plain,
! [X0] : addition(sF15,multiplication(sF15,X0)) = multiplication(sF15,addition(X0,sF18)),
inference(forward_demodulation,[],[f2962,f3]) ).
fof(f2979,plain,
! [X0] : multiplication(sF15,addition(one,X0)) = multiplication(sF15,addition(X0,sF18)),
inference(forward_demodulation,[],[f2977,f248]) ).
fof(f3283,plain,
multiplication(addition(one,sF11),sF5) = addition(sF5,sF11),
inference(superposition,[],[f419,f2792]) ).
fof(f3349,plain,
addition(sF5,sF11) = multiplication(addition(sF11,one),sF5),
inference(forward_demodulation,[],[f3283,f3]) ).
fof(f3409,plain,
addition(sF5,sF11) = multiplication(one,sF5),
inference(forward_demodulation,[],[f3349,f2113]) ).
fof(f3447,plain,
sF5 = addition(sF5,sF11),
inference(forward_demodulation,[],[f3409,f9]) ).
fof(f3479,plain,
multiplication(antidomain(sF5),sF5) = multiplication(antidomain(sF5),sF11),
inference(superposition,[],[f181,f3447]) ).
fof(f3486,plain,
multiplication(sF6,sF5) = multiplication(sF6,sF11),
inference(forward_demodulation,[],[f3479,f63]) ).
fof(f3489,plain,
zero = multiplication(sF6,sF11),
inference(forward_demodulation,[],[f3486,f162]) ).
fof(f3493,plain,
! [X0] : multiplication(addition(X0,sF6),sF11) = addition(multiplication(X0,sF11),zero),
inference(superposition,[],[f11,f3489]) ).
fof(f3512,plain,
! [X0] : multiplication(X0,sF11) = multiplication(addition(X0,sF6),sF11),
inference(forward_demodulation,[],[f3493,f5]) ).
fof(f3636,plain,
! [X0] : zero = multiplication(antidomain(zero),multiplication(X0,antidomain(antidomain(coantidomain(X0))))),
inference(superposition,[],[f329,f28]) ).
fof(f3765,plain,
! [X0] : zero = multiplication(one,multiplication(X0,antidomain(antidomain(coantidomain(X0))))),
inference(forward_demodulation,[],[f3636,f1397]) ).
fof(f3791,plain,
! [X0] : zero = multiplication(X0,antidomain(antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f3765,f9]) ).
fof(f5054,plain,
zero = multiplication(sF13,antidomain(antidomain(sF14))),
inference(superposition,[],[f3791,f79]) ).
fof(f5127,plain,
zero = multiplication(sF13,antidomain(sF15)),
inference(forward_demodulation,[],[f5054,f81]) ).
fof(f5160,plain,
zero = multiplication(sF13,sF16),
inference(forward_demodulation,[],[f5127,f83]) ).
fof(f5178,plain,
! [X0] : addition(zero,multiplication(X0,sF16)) = multiplication(addition(sF13,X0),sF16),
inference(superposition,[],[f11,f5160]) ).
fof(f5204,plain,
! [X0] : multiplication(X0,sF16) = multiplication(addition(sF13,X0),sF16),
inference(forward_demodulation,[],[f5178,f179]) ).
fof(f5234,plain,
multiplication(one,sF16) = multiplication(sF14,sF16),
inference(superposition,[],[f5204,f214]) ).
fof(f5283,plain,
sF16 = multiplication(sF14,sF16),
inference(forward_demodulation,[],[f5234,f9]) ).
fof(f5314,plain,
addition(sF14,sF16) = multiplication(sF14,addition(one,sF16)),
inference(superposition,[],[f248,f5283]) ).
fof(f5334,plain,
addition(sF14,sF16) = multiplication(sF14,addition(sF16,one)),
inference(forward_demodulation,[],[f5314,f3]) ).
fof(f5345,plain,
multiplication(sF14,one) = addition(sF14,sF16),
inference(forward_demodulation,[],[f5334,f2077]) ).
fof(f5353,plain,
sF14 = addition(sF14,sF16),
inference(forward_demodulation,[],[f5345,f8]) ).
fof(f5361,plain,
addition(one,sF14) = addition(sF15,sF14),
inference(superposition,[],[f757,f5353]) ).
fof(f5373,plain,
addition(one,sF14) = addition(sF14,sF15),
inference(forward_demodulation,[],[f5361,f3]) ).
fof(f5376,plain,
addition(sF14,one) = addition(sF14,sF15),
inference(forward_demodulation,[],[f5373,f3]) ).
fof(f5377,plain,
one = addition(sF14,sF15),
inference(forward_demodulation,[],[f5376,f2110]) ).
fof(f5556,plain,
multiplication(one,coantidomain(sF14)) = multiplication(sF15,coantidomain(sF14)),
inference(superposition,[],[f296,f5377]) ).
fof(f5567,plain,
multiplication(sF15,sF13) = multiplication(one,sF13),
inference(forward_demodulation,[],[f5556,f1196]) ).
fof(f5571,plain,
sF13 = multiplication(sF15,sF13),
inference(forward_demodulation,[],[f5567,f9]) ).
fof(f5574,plain,
sF13 = sF15,
inference(backward_demodulation,[],[f2756,f5571]) ).
fof(f5591,plain,
sF18 = addition(sF1,sF13),
inference(backward_demodulation,[],[f670,f5574]) ).
fof(f5592,plain,
sF13 != sF18,
inference(backward_demodulation,[],[f671,f5574]) ).
fof(f5650,plain,
sF13 = multiplication(sF13,sF18),
inference(backward_demodulation,[],[f2959,f5574]) ).
fof(f5660,plain,
! [X0] : multiplication(sF13,addition(one,X0)) = multiplication(sF13,addition(X0,sF18)),
inference(backward_demodulation,[],[f2979,f5574]) ).
fof(f6784,plain,
multiplication(sF5,sF11) = multiplication(one,sF11),
inference(superposition,[],[f3512,f235]) ).
fof(f6816,plain,
sF11 = multiplication(sF5,sF11),
inference(forward_demodulation,[],[f6784,f9]) ).
fof(f6820,plain,
sF5 = sF11,
inference(forward_demodulation,[],[f6816,f1137]) ).
fof(f6832,plain,
! [X0] : multiplication(sF12,X0) = multiplication(sF5,multiplication(sK1_goals_X1,X0)),
inference(backward_demodulation,[],[f495,f6820]) ).
fof(f7344,plain,
multiplication(sF5,sF4) = multiplication(sF12,sF1),
inference(superposition,[],[f6832,f733]) ).
fof(f7398,plain,
zero = multiplication(sF12,sF1),
inference(forward_demodulation,[],[f7344,f161]) ).
fof(f7434,plain,
zero = multiplication(coantidomain(coantidomain(sF12)),multiplication(sF1,coantidomain(zero))),
inference(superposition,[],[f2242,f7398]) ).
fof(f7435,plain,
zero = multiplication(coantidomain(coantidomain(sF12)),multiplication(sF1,one)),
inference(forward_demodulation,[],[f7434,f1134]) ).
fof(f7452,plain,
zero = multiplication(coantidomain(coantidomain(sF12)),sF1),
inference(forward_demodulation,[],[f7435,f8]) ).
fof(f7465,plain,
zero = multiplication(coantidomain(sF13),sF1),
inference(forward_demodulation,[],[f7452,f77]) ).
fof(f7478,plain,
zero = multiplication(sF14,sF1),
inference(forward_demodulation,[],[f7465,f79]) ).
fof(f7510,plain,
! [X0] : addition(multiplication(X0,sF1),zero) = multiplication(addition(X0,sF14),sF1),
inference(superposition,[],[f11,f7478]) ).
fof(f7538,plain,
! [X0] : multiplication(X0,sF1) = multiplication(addition(X0,sF14),sF1),
inference(forward_demodulation,[],[f7510,f5]) ).
fof(f7963,plain,
multiplication(one,sF1) = multiplication(sF13,sF1),
inference(superposition,[],[f7538,f214]) ).
fof(f8006,plain,
sF1 = multiplication(sF13,sF1),
inference(forward_demodulation,[],[f7963,f9]) ).
fof(f8029,plain,
addition(sF13,sF1) = multiplication(sF13,addition(one,sF1)),
inference(superposition,[],[f248,f8006]) ).
fof(f8049,plain,
addition(sF13,sF1) = multiplication(sF13,addition(sF1,sF18)),
inference(forward_demodulation,[],[f8029,f5660]) ).
fof(f8062,plain,
multiplication(sF13,sF18) = addition(sF13,sF1),
inference(forward_demodulation,[],[f8049,f2009]) ).
fof(f8087,plain,
addition(sF1,sF13) = multiplication(sF13,sF18),
inference(forward_demodulation,[],[f8062,f3]) ).
fof(f8101,plain,
sF13 = addition(sF1,sF13),
inference(forward_demodulation,[],[f8087,f5650]) ).
fof(f8108,plain,
sF13 = sF18,
inference(backward_demodulation,[],[f5591,f8101]) ).
fof(f8113,plain,
$false,
inference(forward_subsumption_resolution,[],[f8108,f5592]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE110-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n013.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 13:10:06 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 9.44/2.16 % (217220)Detected a unit-equality problem, will run specialized UEQ schedule.
% 9.44/2.16 % (217228)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2524593451:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 9.44/2.16 % (217231)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1051817692:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 9.44/2.16 % (217225)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=2912819266:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 9.44/2.16 % (217229)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1721781740:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 9.44/2.16 % (217226)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=2151948898:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 9.44/2.16 % (217227)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1195395673:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 9.44/2.16 % (217230)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3394177628:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 9.44/2.16 % (217228)Instruction limit reached!
% 9.44/2.16 % (217228)------------------------------
% 9.44/2.16 % (217228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.16 % (217228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.16 % (217228)CaDiCaL version: 2.1.3
% 9.44/2.16 % (217228)Termination reason: Instruction limit
% 9.44/2.16 % (217228)Termination phase: Saturation
% 9.44/2.16 % (217228)Time elapsed: 0.046 s
% 9.44/2.16 % (217228)Peak memory usage: 89 MB
% 9.44/2.16 % (217228)Instructions burned: 136 (million)
% 9.44/2.16 % (217229)Instruction limit reached!
% 9.44/2.16 % (217229)------------------------------
% 9.44/2.16 % (217229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.16 % (217229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.16 % (217229)CaDiCaL version: 2.1.3
% 9.44/2.16 % (217229)Termination reason: Instruction limit
% 9.44/2.16 % (217229)Termination phase: Saturation
% 9.44/2.16 % (217229)Time elapsed: 0.106 s
% 9.44/2.16 % (217229)Peak memory usage: 90 MB
% 9.44/2.16 % (217229)Instructions burned: 181 (million)
% 9.44/2.16 % (217239)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2844867025:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 9.44/2.16 % (217230)Instruction limit reached!
% 9.44/2.16 % (217230)------------------------------
% 9.44/2.16 % (217230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.16 % (217230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.16 % (217230)CaDiCaL version: 2.1.3
% 9.44/2.16 % (217230)Termination reason: Instruction limit
% 9.44/2.16 % (217230)Termination phase: Saturation
% 9.44/2.16 % (217230)Time elapsed: 0.169 s
% 9.44/2.16 % (217230)Peak memory usage: 91 MB
% 9.44/2.16 % (217230)Instructions burned: 258 (million)
% 9.44/2.16 % (217240)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2958312884:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 9.44/2.16 % (217242)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1896408252:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 9.44/2.16 % (217242)Instruction limit reached!
% 9.44/2.16 % (217242)------------------------------
% 9.44/2.16 % (217242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.16 % (217242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.16 % (217242)CaDiCaL version: 2.1.3
% 9.44/2.16 % (217242)Termination reason: Instruction limit
% 9.44/2.16 % (217242)Termination phase: Saturation
% 9.44/2.16 % (217242)Time elapsed: 0.107 s
% 9.44/2.16 % (217242)Peak memory usage: 90 MB
% 9.44/2.16 % (217242)Instructions burned: 216 (million)
% 9.44/2.16 % (217245)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=3600847064:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 9.44/2.16 % (217231)Instruction limit reached!
% 9.44/2.16 % (217231)------------------------------
% 9.44/2.16 % (217231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.16 % (217231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.16 % (217231)CaDiCaL version: 2.1.3
% 9.44/2.16 % (217231)Termination reason: Instruction limit
% 9.44/2.16 % (217231)Termination phase: Saturation
% 9.44/2.16 % (217231)Time elapsed: 0.645 s
% 9.44/2.16 % (217231)Peak memory usage: 102 MB
% 9.44/2.16 % (217231)Instructions burned: 1187 (million)
% 9.44/2.16 % (217245)Instruction limit reached!
% 9.44/2.16 % (217245)------------------------------
% 9.44/2.16 % (217245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.44/2.16 % (217245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.44/2.17 % (217245)CaDiCaL version: 2.1.3
% 9.44/2.17 % (217245)Termination reason: Instruction limit
% 9.44/2.17 % (217245)Termination phase: Saturation
% 9.44/2.17 % (217245)Time elapsed: 0.186 s
% 9.44/2.17 % (217245)Peak memory usage: 94 MB
% 9.44/2.17 % (217245)Instructions burned: 319 (million)
% 9.44/2.17 % (217247)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=1147125480:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 9.44/2.17 % (217248)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=541917255:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 9.44/2.17 % (217227)First to succeed.
% 9.44/2.17 % (217227)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-217220"
% 9.44/2.17 % (217227)Refutation found. Thanks to Tanya!
% 9.44/2.17 % SZS status Unsatisfiable for theBenchmark
% 9.44/2.17 % SZS output start Proof for theBenchmark
% See solution above
% 9.82/2.36 % (217227)------------------------------
% 9.82/2.36 % (217227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.36 % (217227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.36 % (217227)CaDiCaL version: 2.1.3
% 9.82/2.36 % (217227)Termination reason: Refutation
% 9.82/2.36 % (217227)Time elapsed: 0.973 s
% 9.82/2.36 % (217227)Peak memory usage: 141 MB
% 9.82/2.36 % (217227)Instructions burned: 2140 (million)
% 9.82/2.36 % (217227)------------------------------
% 9.82/2.36 % (217227)------------------------------
% 9.82/2.36 % (217220)Success in time 1.307 s
% 9.82/2.36 % Vampire exiting
%------------------------------------------------------------------------------