%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE124+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:24 AM UTC 2026
% Result : Theorem 24.54s 4.34s
% Output : Refutation 25.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 40
% Syntax : Number of formulae : 319 ( 314 unt; 22 def)
% Number of atoms : 334 ( 333 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 22 ( 7 ~; 0 |; 13 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 29 con; 0-2 aty)
% Number of variables : 262 ( 252 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_associativity) ).
fof(f3,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_identity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_idempotence) ).
fof(f5,axiom,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_left_identity) ).
fof(f8,axiom,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_distributivity) ).
fof(f9,axiom,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_distributivity) ).
fof(f13,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain1) ).
fof(f15,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain3) ).
fof(f16,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain4) ).
fof(f17,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain1) ).
fof(f18,axiom,
! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain2) ).
fof(f19,axiom,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain3) ).
fof(f20,axiom,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain4) ).
fof(f24,axiom,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backward_diamond) ).
fof(f27,conjecture,
! [X0,X1,X2,X3,X4] :
( ( addition(domain(X2),domain(X1)) = domain(X1)
& addition(backward_diamond(X0,domain(X1)),domain(X3)) = domain(X3)
& addition(domain(X3),domain(X4)) = domain(X4) )
=> addition(backward_diamond(X0,domain(X2)),domain(X4)) = domain(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f28,negated_conjecture,
~ ! [X0,X1,X2,X3,X4] :
( ( addition(domain(X2),domain(X1)) = domain(X1)
& addition(backward_diamond(X0,domain(X1)),domain(X3)) = domain(X3)
& addition(domain(X3),domain(X4)) = domain(X4) )
=> addition(backward_diamond(X0,domain(X2)),domain(X4)) = domain(X4) ),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f29,plain,
? [X0,X1,X2,X3,X4] :
( domain(X4) != addition(backward_diamond(X0,domain(X2)),domain(X4))
& addition(domain(X2),domain(X1)) = domain(X1)
& addition(backward_diamond(X0,domain(X1)),domain(X3)) = domain(X3)
& addition(domain(X3),domain(X4)) = domain(X4) ),
inference(ennf_transformation,[],[f28]) ).
fof(f30,plain,
? [X0,X1,X2,X3,X4] :
( domain(X4) != addition(backward_diamond(X0,domain(X2)),domain(X4))
& addition(domain(X2),domain(X1)) = domain(X1)
& addition(backward_diamond(X0,domain(X1)),domain(X3)) = domain(X3)
& addition(domain(X3),domain(X4)) = domain(X4) ),
inference(flattening,[],[f29]) ).
fof(f31,plain,
( domain(sK4) != addition(backward_diamond(sK0,domain(sK2)),domain(sK4))
& domain(sK1) = addition(domain(sK2),domain(sK1))
& domain(sK3) = addition(backward_diamond(sK0,domain(sK1)),domain(sK3))
& domain(sK4) = addition(domain(sK3),domain(sK4)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4)],[f30]) ).
fof(f32,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f33,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f34,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f35,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f36,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f37,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f38,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f39,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f40,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f43,plain,
! [X0] : zero = multiplication(antidomain(X0),X0),
inference(cnf_transformation,[],[f13]) ).
fof(f45,plain,
! [X0] : one = addition(antidomain(antidomain(X0)),antidomain(X0)),
inference(cnf_transformation,[],[f15]) ).
fof(f46,plain,
! [X0] : antidomain(antidomain(X0)) = domain(X0),
inference(cnf_transformation,[],[f16]) ).
fof(f47,plain,
! [X0] : zero = multiplication(X0,coantidomain(X0)),
inference(cnf_transformation,[],[f17]) ).
fof(f48,plain,
! [X0,X1] : coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)) = addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))),
inference(cnf_transformation,[],[f18]) ).
fof(f49,plain,
! [X0] : one = addition(coantidomain(coantidomain(X0)),coantidomain(X0)),
inference(cnf_transformation,[],[f19]) ).
fof(f50,plain,
! [X0] : coantidomain(coantidomain(X0)) = codomain(X0),
inference(cnf_transformation,[],[f20]) ).
fof(f54,plain,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
inference(cnf_transformation,[],[f24]) ).
fof(f57,plain,
domain(sK4) = addition(domain(sK3),domain(sK4)),
inference(cnf_transformation,[],[f31]) ).
fof(f58,plain,
domain(sK3) = addition(backward_diamond(sK0,domain(sK1)),domain(sK3)),
inference(cnf_transformation,[],[f31]) ).
fof(f59,plain,
domain(sK1) = addition(domain(sK2),domain(sK1)),
inference(cnf_transformation,[],[f31]) ).
fof(f60,plain,
domain(sK4) != addition(backward_diamond(sK0,domain(sK2)),domain(sK4)),
inference(cnf_transformation,[],[f31]) ).
fof(f62,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f54,f50,f50]) ).
fof(f67,plain,
antidomain(antidomain(sK4)) != addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2)))),sK0))),antidomain(antidomain(sK4))),
inference(definition_unfolding,[],[f60,f46,f62,f46,f46]) ).
fof(f68,plain,
antidomain(antidomain(sK1)) = addition(antidomain(antidomain(sK2)),antidomain(antidomain(sK1))),
inference(definition_unfolding,[],[f59,f46,f46,f46]) ).
fof(f69,plain,
antidomain(antidomain(sK3)) = addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK1)))),sK0))),antidomain(antidomain(sK3))),
inference(definition_unfolding,[],[f58,f46,f62,f46,f46]) ).
fof(f70,plain,
antidomain(antidomain(sK4)) = addition(antidomain(antidomain(sK3)),antidomain(antidomain(sK4))),
inference(definition_unfolding,[],[f57,f46,f46,f46]) ).
fof(f71,definition,
sF5 = antidomain(sK4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f72,plain,
antidomain(sK4) = sF5,
inference(reorient_equations,[],[f71]) ).
fof(f73,definition,
sF6 = antidomain(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f74,plain,
antidomain(sF5) = sF6,
inference(reorient_equations,[],[f73]) ).
fof(f75,definition,
sF7 = antidomain(sK2),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f76,plain,
antidomain(sK2) = sF7,
inference(reorient_equations,[],[f75]) ).
fof(f77,definition,
sF8 = antidomain(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f78,plain,
antidomain(sF7) = sF8,
inference(reorient_equations,[],[f77]) ).
fof(f79,definition,
sF9 = coantidomain(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f80,plain,
coantidomain(sF8) = sF9,
inference(reorient_equations,[],[f79]) ).
fof(f81,definition,
sF10 = coantidomain(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f82,plain,
coantidomain(sF9) = sF10,
inference(reorient_equations,[],[f81]) ).
fof(f83,definition,
sF11 = multiplication(sF10,sK0),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f84,plain,
multiplication(sF10,sK0) = sF11,
inference(reorient_equations,[],[f83]) ).
fof(f85,definition,
sF12 = coantidomain(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f86,plain,
coantidomain(sF11) = sF12,
inference(reorient_equations,[],[f85]) ).
fof(f87,definition,
sF13 = coantidomain(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f88,plain,
coantidomain(sF12) = sF13,
inference(reorient_equations,[],[f87]) ).
fof(f89,definition,
sF14 = addition(sF13,sF6),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f90,plain,
addition(sF13,sF6) = sF14,
inference(reorient_equations,[],[f89]) ).
fof(f91,plain,
sF6 != sF14,
inference(definition_folding,[],[f67,f90,f74,f72,f88,f86,f84,f82,f80,f78,f76,f74,f72]) ).
fof(f92,definition,
sF15 = antidomain(sK1),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f93,plain,
antidomain(sK1) = sF15,
inference(reorient_equations,[],[f92]) ).
fof(f94,definition,
sF16 = antidomain(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f95,plain,
antidomain(sF15) = sF16,
inference(reorient_equations,[],[f94]) ).
fof(f96,definition,
sF17 = addition(sF8,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f97,plain,
addition(sF8,sF16) = sF17,
inference(reorient_equations,[],[f96]) ).
fof(f98,plain,
sF16 = sF17,
inference(definition_folding,[],[f68,f97,f95,f93,f78,f76,f95,f93]) ).
fof(f99,definition,
sF18 = antidomain(sK3),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f100,plain,
antidomain(sK3) = sF18,
inference(reorient_equations,[],[f99]) ).
fof(f101,definition,
sF19 = antidomain(sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f102,plain,
antidomain(sF18) = sF19,
inference(reorient_equations,[],[f101]) ).
fof(f103,definition,
sF20 = coantidomain(sF16),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f104,plain,
coantidomain(sF16) = sF20,
inference(reorient_equations,[],[f103]) ).
fof(f105,definition,
sF21 = coantidomain(sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f106,plain,
coantidomain(sF20) = sF21,
inference(reorient_equations,[],[f105]) ).
fof(f107,definition,
sF22 = multiplication(sF21,sK0),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f108,plain,
multiplication(sF21,sK0) = sF22,
inference(reorient_equations,[],[f107]) ).
fof(f109,definition,
sF23 = coantidomain(sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f110,plain,
coantidomain(sF22) = sF23,
inference(reorient_equations,[],[f109]) ).
fof(f111,definition,
sF24 = coantidomain(sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f112,plain,
coantidomain(sF23) = sF24,
inference(reorient_equations,[],[f111]) ).
fof(f113,definition,
sF25 = addition(sF24,sF19),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f114,plain,
addition(sF24,sF19) = sF25,
inference(reorient_equations,[],[f113]) ).
fof(f115,plain,
sF19 = sF25,
inference(definition_folding,[],[f69,f114,f102,f100,f112,f110,f108,f106,f104,f95,f93,f102,f100]) ).
fof(f116,definition,
sF26 = addition(sF19,sF6),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f117,plain,
addition(sF19,sF6) = sF26,
inference(reorient_equations,[],[f116]) ).
fof(f118,plain,
sF6 = sF26,
inference(definition_folding,[],[f70,f117,f74,f72,f102,f100,f74,f72]) ).
fof(f119,plain,
sF16 = addition(sF8,sF16),
inference(forward_demodulation,[],[f97,f98]) ).
fof(f120,plain,
sF19 = addition(sF24,sF19),
inference(forward_demodulation,[],[f114,f115]) ).
fof(f121,plain,
sF6 = addition(sF19,sF6),
inference(forward_demodulation,[],[f117,f118]) ).
fof(f125,plain,
sF6 = addition(sF6,sF19),
inference(superposition,[],[f121,f32]) ).
fof(f126,plain,
one = addition(coantidomain(sF20),sF20),
inference(superposition,[],[f49,f104]) ).
fof(f127,plain,
one = addition(coantidomain(sF9),sF9),
inference(superposition,[],[f49,f80]) ).
fof(f132,plain,
one = addition(sF10,sF9),
inference(forward_demodulation,[],[f127,f82]) ).
fof(f133,plain,
one = addition(sF21,sF20),
inference(forward_demodulation,[],[f126,f106]) ).
fof(f136,plain,
one = addition(coantidomain(sF12),sF12),
inference(superposition,[],[f49,f86]) ).
fof(f137,plain,
one = addition(sF13,sF12),
inference(forward_demodulation,[],[f136,f88]) ).
fof(f142,plain,
one = addition(antidomain(sF15),sF15),
inference(superposition,[],[f45,f93]) ).
fof(f143,plain,
one = addition(antidomain(sF7),sF7),
inference(superposition,[],[f45,f76]) ).
fof(f144,plain,
one = addition(antidomain(sF18),sF18),
inference(superposition,[],[f45,f100]) ).
fof(f153,plain,
! [X0] : one = addition(antidomain(X0),antidomain(antidomain(X0))),
inference(superposition,[],[f32,f45]) ).
fof(f155,plain,
one = addition(sF19,sF18),
inference(forward_demodulation,[],[f144,f102]) ).
fof(f156,plain,
one = addition(sF8,sF7),
inference(forward_demodulation,[],[f143,f78]) ).
fof(f157,plain,
one = addition(sF16,sF15),
inference(forward_demodulation,[],[f142,f95]) ).
fof(f162,plain,
! [X0,X1] : addition(one,X1) = addition(coantidomain(coantidomain(X0)),addition(coantidomain(X0),X1)),
inference(superposition,[],[f33,f49]) ).
fof(f164,plain,
! [X0] : addition(sF13,addition(sF6,X0)) = addition(sF14,X0),
inference(superposition,[],[f33,f90]) ).
fof(f165,plain,
! [X0] : addition(sF16,X0) = addition(sF8,addition(sF16,X0)),
inference(superposition,[],[f33,f119]) ).
fof(f170,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(superposition,[],[f32,f33]) ).
fof(f175,plain,
! [X0] : multiplication(addition(sF21,X0),sK0) = addition(sF22,multiplication(X0,sK0)),
inference(superposition,[],[f40,f108]) ).
fof(f177,plain,
! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)),
inference(superposition,[],[f40,f38]) ).
fof(f180,plain,
! [X0,X1] : multiplication(addition(X1,one),X0) = addition(multiplication(X1,X0),X0),
inference(superposition,[],[f40,f38]) ).
fof(f195,plain,
zero = multiplication(sF8,sF7),
inference(superposition,[],[f43,f78]) ).
fof(f198,plain,
! [X0,X1] : multiplication(addition(X0,antidomain(X1)),X1) = addition(multiplication(X0,X1),zero),
inference(superposition,[],[f40,f43]) ).
fof(f199,plain,
! [X0,X1] : multiplication(addition(antidomain(X0),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(superposition,[],[f40,f43]) ).
fof(f200,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(addition(X0,antidomain(X1)),X1),
inference(forward_demodulation,[],[f198,f34]) ).
fof(f227,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X1,X0)) = addition(multiplication(antidomain(X0),X1),zero),
inference(superposition,[],[f39,f43]) ).
fof(f232,plain,
! [X2,X3,X0,X1] : addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)) = addition(multiplication(X0,addition(X1,X2)),X3),
inference(superposition,[],[f33,f39]) ).
fof(f241,plain,
! [X0,X1] : multiplication(antidomain(X0),X1) = multiplication(antidomain(X0),addition(X1,X0)),
inference(forward_demodulation,[],[f227,f34]) ).
fof(f253,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X0,X1)) = multiplication(antidomain(X0),X1),
inference(superposition,[],[f241,f32]) ).
fof(f255,plain,
! [X2,X0,X1] : multiplication(antidomain(multiplication(X1,X2)),multiplication(X0,X2)) = multiplication(antidomain(multiplication(X1,X2)),multiplication(addition(X0,X1),X2)),
inference(superposition,[],[f241,f40]) ).
fof(f260,plain,
multiplication(antidomain(sF6),sF19) = multiplication(antidomain(sF6),sF6),
inference(superposition,[],[f241,f121]) ).
fof(f273,plain,
zero = multiplication(antidomain(sF6),sF19),
inference(forward_demodulation,[],[f260,f43]) ).
fof(f286,plain,
! [X0] : multiplication(one,X0) = multiplication(antidomain(antidomain(X0)),X0),
inference(superposition,[],[f200,f45]) ).
fof(f288,plain,
! [X0,X1] : multiplication(X1,X0) = multiplication(addition(antidomain(X0),X1),X0),
inference(superposition,[],[f200,f32]) ).
fof(f297,plain,
! [X0,X1] : multiplication(X1,X0) = addition(zero,multiplication(X1,X0)),
inference(forward_demodulation,[],[f288,f199]) ).
fof(f299,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f286,f38]) ).
fof(f320,plain,
! [X0] : addition(sF6,X0) = addition(sF6,addition(sF19,X0)),
inference(superposition,[],[f33,f125]) ).
fof(f330,plain,
zero = coantidomain(one),
inference(superposition,[],[f38,f47]) ).
fof(f331,plain,
! [X0,X1] : addition(multiplication(X0,X1),zero) = multiplication(X0,addition(X1,coantidomain(X0))),
inference(superposition,[],[f39,f47]) ).
fof(f334,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = addition(multiplication(X0,coantidomain(X1)),zero),
inference(superposition,[],[f40,f47]) ).
fof(f335,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X0)) = addition(zero,multiplication(X1,coantidomain(X0))),
inference(superposition,[],[f40,f47]) ).
fof(f337,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X0)) = multiplication(X1,coantidomain(X0)),
inference(forward_demodulation,[],[f335,f297]) ).
fof(f338,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = multiplication(X0,coantidomain(X1)),
inference(forward_demodulation,[],[f334,f34]) ).
fof(f340,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(X0,addition(X1,coantidomain(X0))),
inference(forward_demodulation,[],[f331,f34]) ).
fof(f345,plain,
! [X2,X0,X1] : multiplication(multiplication(X0,X1),coantidomain(multiplication(X0,X2))) = multiplication(multiplication(X0,addition(X1,X2)),coantidomain(multiplication(X0,X2))),
inference(superposition,[],[f338,f39]) ).
fof(f374,plain,
! [X2,X0,X1] : multiplication(multiplication(X0,X1),coantidomain(multiplication(X0,X2))) = multiplication(X0,multiplication(addition(X1,X2),coantidomain(multiplication(X0,X2)))),
inference(forward_demodulation,[],[f345,f36]) ).
fof(f378,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(addition(X1,X2),coantidomain(multiplication(X0,X2)))) = multiplication(X0,multiplication(X1,coantidomain(multiplication(X0,X2)))),
inference(forward_demodulation,[],[f374,f36]) ).
fof(f396,plain,
! [X0,X1] : multiplication(antidomain(multiplication(coantidomain(X0),X1)),multiplication(coantidomain(coantidomain(X0)),X1)) = multiplication(antidomain(multiplication(coantidomain(X0),X1)),multiplication(one,X1)),
inference(superposition,[],[f255,f49]) ).
fof(f415,plain,
! [X0,X1] : multiplication(antidomain(multiplication(coantidomain(X0),X1)),multiplication(coantidomain(coantidomain(X0)),X1)) = multiplication(antidomain(multiplication(coantidomain(X0),X1)),X1),
inference(forward_demodulation,[],[f396,f38]) ).
fof(f434,plain,
! [X0] : multiplication(X0,one) = multiplication(X0,coantidomain(coantidomain(X0))),
inference(superposition,[],[f340,f49]) ).
fof(f435,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,[],[f340,f48]) ).
fof(f453,plain,
! [X0,X1] : zero = multiplication(multiplication(coantidomain(coantidomain(X0)),X1),coantidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f435,f47]) ).
fof(f454,plain,
! [X0] : multiplication(X0,coantidomain(coantidomain(X0))) = X0,
inference(forward_demodulation,[],[f434,f37]) ).
fof(f458,plain,
! [X0,X1] : zero = multiplication(coantidomain(coantidomain(X0)),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f453,f36]) ).
fof(f474,plain,
zero = antidomain(one),
inference(superposition,[],[f43,f37]) ).
fof(f478,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(superposition,[],[f39,f37]) ).
fof(f572,plain,
! [X2,X3,X0,X1] : addition(multiplication(X0,addition(X3,X2)),multiplication(X1,X2)) = addition(multiplication(X0,X3),multiplication(addition(X0,X1),X2)),
inference(superposition,[],[f232,f40]) ).
fof(f708,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f33,f35]) ).
fof(f709,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X1,addition(X0,X1))),
inference(superposition,[],[f33,f35]) ).
fof(f728,plain,
! [X0] : one = addition(coantidomain(coantidomain(X0)),one),
inference(superposition,[],[f708,f49]) ).
fof(f741,plain,
! [X0,X1] : multiplication(X0,coantidomain(addition(X0,X1))) = multiplication(addition(X0,X1),coantidomain(addition(X0,X1))),
inference(superposition,[],[f338,f708]) ).
fof(f746,plain,
! [X0,X1] : zero = multiplication(X0,coantidomain(addition(X0,X1))),
inference(forward_demodulation,[],[f741,f47]) ).
fof(f877,plain,
sF8 = multiplication(sF8,coantidomain(sF9)),
inference(superposition,[],[f454,f80]) ).
fof(f887,plain,
one = coantidomain(coantidomain(one)),
inference(superposition,[],[f38,f454]) ).
fof(f908,plain,
one = coantidomain(zero),
inference(forward_demodulation,[],[f887,f330]) ).
fof(f913,plain,
sF8 = multiplication(sF8,sF10),
inference(forward_demodulation,[],[f877,f82]) ).
fof(f1016,plain,
! [X2,X0,X1] : addition(multiplication(X0,coantidomain(coantidomain(X1))),multiplication(addition(X0,X2),coantidomain(X1))) = addition(multiplication(X0,one),multiplication(X2,coantidomain(X1))),
inference(superposition,[],[f572,f49]) ).
fof(f1161,plain,
! [X2,X0,X1] : addition(multiplication(X0,coantidomain(coantidomain(X1))),multiplication(addition(X0,X2),coantidomain(X1))) = addition(X0,multiplication(X2,coantidomain(X1))),
inference(forward_demodulation,[],[f1016,f37]) ).
fof(f1344,plain,
! [X0,X1] : addition(X0,multiplication(X0,coantidomain(X1))) = addition(multiplication(X0,coantidomain(coantidomain(X1))),multiplication(X0,coantidomain(X1))),
inference(superposition,[],[f1161,f35]) ).
fof(f1378,plain,
! [X0,X1] : addition(X0,multiplication(X1,coantidomain(addition(X0,X1)))) = addition(multiplication(X0,coantidomain(coantidomain(addition(X0,X1)))),zero),
inference(superposition,[],[f1161,f47]) ).
fof(f1400,plain,
! [X0,X1] : multiplication(X0,coantidomain(coantidomain(addition(X0,X1)))) = addition(X0,multiplication(X1,coantidomain(addition(X0,X1)))),
inference(forward_demodulation,[],[f1378,f34]) ).
fof(f1422,plain,
! [X0,X1] : multiplication(X0,addition(coantidomain(coantidomain(X1)),coantidomain(X1))) = addition(X0,multiplication(X0,coantidomain(X1))),
inference(forward_demodulation,[],[f1344,f39]) ).
fof(f1443,plain,
! [X0,X1] : multiplication(X0,addition(coantidomain(coantidomain(X1)),coantidomain(X1))) = multiplication(X0,addition(one,coantidomain(X1))),
inference(forward_demodulation,[],[f1422,f478]) ).
fof(f1457,plain,
! [X0,X1] : multiplication(X0,one) = multiplication(X0,addition(one,coantidomain(X1))),
inference(forward_demodulation,[],[f1443,f49]) ).
fof(f1467,plain,
! [X0,X1] : multiplication(X0,addition(one,coantidomain(X1))) = X0,
inference(forward_demodulation,[],[f1457,f37]) ).
fof(f1514,plain,
! [X0] : multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)) = multiplication(antidomain(antidomain(antidomain(X0))),one),
inference(superposition,[],[f253,f45]) ).
fof(f1549,plain,
! [X0] : antidomain(antidomain(antidomain(X0))) = multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)),
inference(forward_demodulation,[],[f1514,f37]) ).
fof(f1557,plain,
! [X0] : antidomain(X0) = antidomain(antidomain(antidomain(X0))),
inference(forward_demodulation,[],[f1549,f299]) ).
fof(f1560,plain,
sF7 = antidomain(antidomain(sF7)),
inference(superposition,[],[f1557,f76]) ).
fof(f1562,plain,
sF5 = antidomain(antidomain(sF5)),
inference(superposition,[],[f1557,f72]) ).
fof(f1579,plain,
sF5 = antidomain(sF6),
inference(forward_demodulation,[],[f1562,f74]) ).
fof(f1581,plain,
sF7 = antidomain(sF8),
inference(forward_demodulation,[],[f1560,f78]) ).
fof(f1739,plain,
zero = multiplication(sF5,sF19),
inference(superposition,[],[f273,f1579]) ).
fof(f1753,plain,
! [X0,X1] : addition(multiplication(X0,X1),multiplication(addition(X0,antidomain(sF6)),sF19)) = addition(multiplication(X0,addition(X1,sF19)),zero),
inference(superposition,[],[f572,f273]) ).
fof(f1756,plain,
! [X0,X1] : multiplication(X0,addition(X1,sF19)) = addition(multiplication(X0,X1),multiplication(addition(X0,antidomain(sF6)),sF19)),
inference(forward_demodulation,[],[f1753,f34]) ).
fof(f1771,plain,
! [X0,X1] : multiplication(X0,addition(X1,sF19)) = addition(multiplication(X0,X1),multiplication(addition(X0,sF5),sF19)),
inference(forward_demodulation,[],[f1756,f1579]) ).
fof(f1814,plain,
one = multiplication(antidomain(zero),one),
inference(superposition,[],[f299,f474]) ).
fof(f1818,plain,
one = antidomain(zero),
inference(forward_demodulation,[],[f1814,f37]) ).
fof(f1943,plain,
! [X0] : addition(sF6,addition(X0,sF13)) = addition(X0,sF14),
inference(superposition,[],[f170,f90]) ).
fof(f2392,plain,
one = addition(sF19,one),
inference(superposition,[],[f708,f155]) ).
fof(f2409,plain,
one = addition(one,sF19),
inference(superposition,[],[f32,f2392]) ).
fof(f2513,plain,
! [X0] : multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))) = multiplication(one,coantidomain(coantidomain(coantidomain(X0)))),
inference(superposition,[],[f337,f49]) ).
fof(f2570,plain,
! [X0] : coantidomain(coantidomain(coantidomain(X0))) = multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f2513,f38]) ).
fof(f2588,plain,
! [X0] : coantidomain(X0) = coantidomain(coantidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f2570,f454]) ).
fof(f2607,plain,
sF20 = coantidomain(coantidomain(sF20)),
inference(superposition,[],[f2588,f104]) ).
fof(f2610,plain,
sF24 = coantidomain(coantidomain(sF24)),
inference(superposition,[],[f2588,f112]) ).
fof(f2626,plain,
sF20 = coantidomain(sF21),
inference(forward_demodulation,[],[f2607,f106]) ).
fof(f3528,plain,
! [X0,X1] : zero = multiplication(coantidomain(coantidomain(X0)),multiplication(coantidomain(addition(X0,X1)),coantidomain(zero))),
inference(superposition,[],[f458,f746]) ).
fof(f3545,plain,
! [X0,X1] : zero = multiplication(coantidomain(coantidomain(X0)),multiplication(coantidomain(addition(X0,X1)),one)),
inference(forward_demodulation,[],[f3528,f908]) ).
fof(f3579,plain,
! [X0,X1] : zero = multiplication(coantidomain(coantidomain(X0)),coantidomain(addition(X0,X1))),
inference(forward_demodulation,[],[f3545,f37]) ).
fof(f4261,plain,
! [X0,X1] : multiplication(X1,coantidomain(coantidomain(addition(X0,X1)))) = addition(X1,multiplication(X0,coantidomain(addition(X0,X1)))),
inference(superposition,[],[f1400,f32]) ).
fof(f4297,plain,
multiplication(sF8,coantidomain(coantidomain(sF16))) = addition(sF8,multiplication(sF16,coantidomain(sF16))),
inference(superposition,[],[f1400,f119]) ).
fof(f4369,plain,
addition(sF8,zero) = multiplication(sF8,coantidomain(coantidomain(sF16))),
inference(forward_demodulation,[],[f4297,f47]) ).
fof(f4404,plain,
! [X0,X1] : addition(X1,zero) = multiplication(X1,coantidomain(coantidomain(addition(X0,X1)))),
inference(forward_demodulation,[],[f4261,f746]) ).
fof(f4437,plain,
addition(sF8,zero) = multiplication(sF8,coantidomain(sF20)),
inference(forward_demodulation,[],[f4369,f104]) ).
fof(f4467,plain,
! [X0,X1] : multiplication(X1,coantidomain(coantidomain(addition(X0,X1)))) = X1,
inference(forward_demodulation,[],[f4404,f34]) ).
fof(f4487,plain,
addition(sF8,zero) = multiplication(sF8,sF21),
inference(forward_demodulation,[],[f4437,f106]) ).
fof(f4511,plain,
sF8 = multiplication(sF8,sF21),
inference(forward_demodulation,[],[f4487,f34]) ).
fof(f4715,plain,
one = addition(sF8,one),
inference(superposition,[],[f165,f157]) ).
fof(f4755,plain,
one = addition(one,sF8),
inference(superposition,[],[f32,f4715]) ).
fof(f4767,plain,
! [X0] : addition(sF8,multiplication(one,coantidomain(X0))) = addition(multiplication(sF8,coantidomain(coantidomain(X0))),multiplication(one,coantidomain(X0))),
inference(superposition,[],[f1161,f4715]) ).
fof(f4773,plain,
! [X0] : addition(sF8,coantidomain(X0)) = addition(multiplication(sF8,coantidomain(coantidomain(X0))),coantidomain(X0)),
inference(forward_demodulation,[],[f4767,f38]) ).
fof(f4834,plain,
one = addition(sF7,antidomain(sF7)),
inference(superposition,[],[f153,f1581]) ).
fof(f4883,plain,
one = addition(sF7,sF8),
inference(forward_demodulation,[],[f4834,f78]) ).
fof(f4913,plain,
! [X0,X1] : addition(multiplication(X0,one),multiplication(X1,sF8)) = addition(multiplication(X0,sF7),multiplication(addition(X0,X1),sF8)),
inference(superposition,[],[f572,f4883]) ).
fof(f4927,plain,
! [X0,X1] : addition(X0,multiplication(X1,sF8)) = addition(multiplication(X0,sF7),multiplication(addition(X0,X1),sF8)),
inference(forward_demodulation,[],[f4913,f37]) ).
fof(f5795,plain,
! [X0] : addition(multiplication(sF8,coantidomain(coantidomain(X0))),multiplication(one,coantidomain(X0))) = addition(sF8,multiplication(sF7,coantidomain(X0))),
inference(superposition,[],[f1161,f156]) ).
fof(f5804,plain,
! [X0] : addition(multiplication(sF8,coantidomain(coantidomain(X0))),coantidomain(X0)) = addition(sF8,multiplication(sF7,coantidomain(X0))),
inference(forward_demodulation,[],[f5795,f38]) ).
fof(f5819,plain,
! [X0] : addition(sF8,coantidomain(X0)) = addition(sF8,multiplication(sF7,coantidomain(X0))),
inference(forward_demodulation,[],[f5804,f4773]) ).
fof(f6017,plain,
! [X0] : addition(one,coantidomain(X0)) = addition(coantidomain(coantidomain(coantidomain(X0))),one),
inference(superposition,[],[f162,f49]) ).
fof(f6066,plain,
! [X0] : one = addition(one,coantidomain(X0)),
inference(forward_demodulation,[],[f6017,f728]) ).
fof(f6122,plain,
one = addition(sF13,one),
inference(superposition,[],[f708,f137]) ).
fof(f6155,plain,
one = addition(one,sF13),
inference(superposition,[],[f32,f6122]) ).
fof(f6889,plain,
multiplication(addition(sF8,one),sF10) = addition(sF8,sF10),
inference(superposition,[],[f180,f913]) ).
fof(f6900,plain,
multiplication(addition(sF8,one),sF21) = addition(sF8,sF21),
inference(superposition,[],[f180,f4511]) ).
fof(f6975,plain,
addition(sF8,sF21) = multiplication(one,sF21),
inference(forward_demodulation,[],[f6900,f4715]) ).
fof(f6985,plain,
addition(sF8,sF10) = multiplication(one,sF10),
inference(forward_demodulation,[],[f6889,f4715]) ).
fof(f7038,plain,
sF21 = addition(sF8,sF21),
inference(forward_demodulation,[],[f6975,f38]) ).
fof(f7048,plain,
sF10 = addition(sF8,sF10),
inference(forward_demodulation,[],[f6985,f38]) ).
fof(f7680,plain,
one = addition(sF21,one),
inference(superposition,[],[f708,f133]) ).
fof(f7713,plain,
one = addition(one,sF21),
inference(superposition,[],[f32,f7680]) ).
fof(f7795,plain,
! [X0,X1] : addition(multiplication(X0,one),multiplication(addition(X0,X1),sF19)) = addition(multiplication(X0,one),multiplication(X1,sF19)),
inference(superposition,[],[f572,f2409]) ).
fof(f7810,plain,
! [X0,X1] : addition(X0,multiplication(X1,sF19)) = addition(X0,multiplication(addition(X0,X1),sF19)),
inference(forward_demodulation,[],[f7795,f37]) ).
fof(f8065,plain,
one = addition(one,sF20),
inference(superposition,[],[f6066,f2626]) ).
fof(f9045,plain,
! [X0] : multiplication(X0,multiplication(one,coantidomain(multiplication(X0,one)))) = multiplication(X0,multiplication(sF8,coantidomain(multiplication(X0,one)))),
inference(superposition,[],[f378,f4715]) ).
fof(f9287,plain,
! [X0] : multiplication(X0,multiplication(one,coantidomain(X0))) = multiplication(X0,multiplication(sF8,coantidomain(X0))),
inference(forward_demodulation,[],[f9045,f37]) ).
fof(f9348,plain,
! [X0] : multiplication(X0,coantidomain(X0)) = multiplication(X0,multiplication(sF8,coantidomain(X0))),
inference(forward_demodulation,[],[f9287,f38]) ).
fof(f9389,plain,
! [X0] : zero = multiplication(X0,multiplication(sF8,coantidomain(X0))),
inference(forward_demodulation,[],[f9348,f47]) ).
fof(f10271,plain,
zero = multiplication(coantidomain(coantidomain(sF8)),coantidomain(sF21)),
inference(superposition,[],[f3579,f7038]) ).
fof(f10333,plain,
zero = multiplication(coantidomain(coantidomain(sF8)),sF20),
inference(forward_demodulation,[],[f10271,f2626]) ).
fof(f10408,plain,
zero = multiplication(coantidomain(sF9),sF20),
inference(forward_demodulation,[],[f10333,f80]) ).
fof(f10425,plain,
zero = multiplication(sF10,sF20),
inference(forward_demodulation,[],[f10408,f82]) ).
fof(f10433,plain,
! [X0] : addition(zero,multiplication(X0,sF20)) = multiplication(addition(sF10,X0),sF20),
inference(superposition,[],[f40,f10425]) ).
fof(f10469,plain,
! [X0] : multiplication(X0,sF20) = multiplication(addition(sF10,X0),sF20),
inference(forward_demodulation,[],[f10433,f297]) ).
fof(f12182,plain,
addition(sF8,multiplication(sF21,sF8)) = addition(multiplication(sF8,sF7),multiplication(sF21,sF8)),
inference(superposition,[],[f4927,f7038]) ).
fof(f12248,plain,
addition(sF8,multiplication(sF21,sF8)) = addition(zero,multiplication(sF21,sF8)),
inference(forward_demodulation,[],[f12182,f195]) ).
fof(f12342,plain,
multiplication(sF21,sF8) = addition(sF8,multiplication(sF21,sF8)),
inference(forward_demodulation,[],[f12248,f297]) ).
fof(f12401,plain,
multiplication(sF21,sF8) = multiplication(addition(one,sF21),sF8),
inference(forward_demodulation,[],[f12342,f177]) ).
fof(f12436,plain,
multiplication(one,sF8) = multiplication(sF21,sF8),
inference(forward_demodulation,[],[f12401,f7713]) ).
fof(f12454,plain,
sF8 = multiplication(sF21,sF8),
inference(forward_demodulation,[],[f12436,f38]) ).
fof(f12544,plain,
addition(sF21,sF8) = multiplication(sF21,addition(one,sF8)),
inference(superposition,[],[f478,f12454]) ).
fof(f12554,plain,
addition(sF21,sF8) = multiplication(sF21,one),
inference(forward_demodulation,[],[f12544,f4755]) ).
fof(f12569,plain,
sF21 = addition(sF21,sF8),
inference(forward_demodulation,[],[f12554,f37]) ).
fof(f13825,plain,
zero = multiplication(sF20,multiplication(sF8,sF21)),
inference(superposition,[],[f9389,f106]) ).
fof(f13831,plain,
zero = multiplication(coantidomain(sF8),sF8),
inference(superposition,[],[f9389,f454]) ).
fof(f13918,plain,
zero = multiplication(sF9,sF8),
inference(forward_demodulation,[],[f13831,f80]) ).
fof(f13920,plain,
zero = multiplication(sF20,sF8),
inference(forward_demodulation,[],[f13825,f4511]) ).
fof(f13963,plain,
! [X0] : multiplication(sF9,addition(X0,sF8)) = addition(multiplication(sF9,X0),zero),
inference(superposition,[],[f39,f13918]) ).
fof(f14007,plain,
! [X0] : multiplication(sF9,X0) = multiplication(sF9,addition(X0,sF8)),
inference(forward_demodulation,[],[f13963,f34]) ).
fof(f14732,plain,
multiplication(one,sF20) = multiplication(sF9,sF20),
inference(superposition,[],[f10469,f132]) ).
fof(f14781,plain,
sF20 = multiplication(sF9,sF20),
inference(forward_demodulation,[],[f14732,f38]) ).
fof(f14826,plain,
multiplication(sF9,addition(one,sF20)) = addition(sF9,sF20),
inference(superposition,[],[f478,f14781]) ).
fof(f14835,plain,
multiplication(sF9,one) = addition(sF9,sF20),
inference(forward_demodulation,[],[f14826,f8065]) ).
fof(f14845,plain,
sF9 = addition(sF9,sF20),
inference(forward_demodulation,[],[f14835,f37]) ).
fof(f14870,plain,
addition(sF9,multiplication(sF20,sF8)) = addition(multiplication(sF9,sF7),multiplication(sF9,sF8)),
inference(superposition,[],[f4927,f14845]) ).
fof(f14877,plain,
addition(sF9,multiplication(sF20,sF8)) = multiplication(sF9,addition(sF7,sF8)),
inference(forward_demodulation,[],[f14870,f39]) ).
fof(f14892,plain,
multiplication(sF9,sF7) = addition(sF9,multiplication(sF20,sF8)),
inference(forward_demodulation,[],[f14877,f14007]) ).
fof(f14902,plain,
addition(sF9,zero) = multiplication(sF9,sF7),
inference(forward_demodulation,[],[f14892,f13920]) ).
fof(f14909,plain,
sF9 = multiplication(sF9,sF7),
inference(forward_demodulation,[],[f14902,f34]) ).
fof(f15998,plain,
addition(sF6,sF13) = addition(sF6,addition(sF14,sF13)),
inference(superposition,[],[f709,f164]) ).
fof(f16041,plain,
addition(sF6,sF13) = addition(sF14,sF14),
inference(forward_demodulation,[],[f15998,f1943]) ).
fof(f16062,plain,
sF14 = addition(sF6,sF13),
inference(forward_demodulation,[],[f16041,f35]) ).
fof(f19970,plain,
! [X0,X1] : multiplication(antidomain(zero),multiplication(coantidomain(coantidomain(coantidomain(X0))),multiplication(X1,coantidomain(multiplication(X0,X1))))) = multiplication(antidomain(zero),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(superposition,[],[f415,f458]) ).
fof(f19981,plain,
! [X0,X1] : multiplication(antidomain(zero),multiplication(coantidomain(coantidomain(coantidomain(X0))),coantidomain(addition(X0,X1)))) = multiplication(antidomain(zero),coantidomain(addition(X0,X1))),
inference(superposition,[],[f415,f3579]) ).
fof(f20104,plain,
! [X0,X1] : multiplication(one,coantidomain(addition(X0,X1))) = multiplication(one,multiplication(coantidomain(coantidomain(coantidomain(X0))),coantidomain(addition(X0,X1)))),
inference(forward_demodulation,[],[f19981,f1818]) ).
fof(f20112,plain,
! [X0,X1] : multiplication(one,multiplication(X1,coantidomain(multiplication(X0,X1)))) = multiplication(one,multiplication(coantidomain(coantidomain(coantidomain(X0))),multiplication(X1,coantidomain(multiplication(X0,X1))))),
inference(forward_demodulation,[],[f19970,f1818]) ).
fof(f20136,plain,
! [X0,X1] : multiplication(one,coantidomain(addition(X0,X1))) = multiplication(coantidomain(coantidomain(coantidomain(X0))),coantidomain(addition(X0,X1))),
inference(forward_demodulation,[],[f20104,f38]) ).
fof(f20143,plain,
! [X0,X1] : multiplication(one,multiplication(X1,coantidomain(multiplication(X0,X1)))) = multiplication(coantidomain(coantidomain(coantidomain(X0))),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f20112,f38]) ).
fof(f20152,plain,
! [X0,X1] : multiplication(one,coantidomain(addition(X0,X1))) = multiplication(coantidomain(X0),coantidomain(addition(X0,X1))),
inference(forward_demodulation,[],[f20136,f2588]) ).
fof(f20158,plain,
! [X0,X1] : multiplication(one,multiplication(X1,coantidomain(multiplication(X0,X1)))) = multiplication(coantidomain(X0),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f20143,f2588]) ).
fof(f20160,plain,
! [X0,X1] : coantidomain(addition(X0,X1)) = multiplication(coantidomain(X0),coantidomain(addition(X0,X1))),
inference(forward_demodulation,[],[f20152,f38]) ).
fof(f20162,plain,
! [X0,X1] : multiplication(X1,coantidomain(multiplication(X0,X1))) = multiplication(coantidomain(X0),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f20158,f38]) ).
fof(f20338,plain,
! [X0,X1] : multiplication(coantidomain(X0),addition(one,coantidomain(addition(X0,X1)))) = addition(coantidomain(X0),coantidomain(addition(X0,X1))),
inference(superposition,[],[f478,f20160]) ).
fof(f20348,plain,
! [X0,X1] : coantidomain(X0) = addition(coantidomain(X0),coantidomain(addition(X0,X1))),
inference(forward_demodulation,[],[f20338,f1467]) ).
fof(f20455,plain,
! [X0,X1] : coantidomain(X1) = addition(coantidomain(X1),coantidomain(addition(X0,X1))),
inference(superposition,[],[f20348,f32]) ).
fof(f21588,plain,
! [X0] : multiplication(X0,coantidomain(zero)) = multiplication(coantidomain(antidomain(X0)),multiplication(X0,coantidomain(zero))),
inference(superposition,[],[f20162,f43]) ).
fof(f21866,plain,
! [X0] : multiplication(X0,one) = multiplication(coantidomain(antidomain(X0)),multiplication(X0,one)),
inference(forward_demodulation,[],[f21588,f908]) ).
fof(f21917,plain,
! [X0] : multiplication(coantidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f21866,f37]) ).
fof(f21957,plain,
sF7 = multiplication(coantidomain(sF8),sF7),
inference(superposition,[],[f21917,f78]) ).
fof(f22033,plain,
sF7 = multiplication(sF9,sF7),
inference(forward_demodulation,[],[f21957,f80]) ).
fof(f22043,plain,
sF7 = sF9,
inference(forward_demodulation,[],[f22033,f14909]) ).
fof(f22045,plain,
sF10 = coantidomain(sF7),
inference(superposition,[],[f82,f22043]) ).
fof(f30822,plain,
addition(sF8,zero) = addition(sF8,coantidomain(sF7)),
inference(superposition,[],[f5819,f47]) ).
fof(f30902,plain,
addition(sF8,zero) = addition(sF8,sF10),
inference(forward_demodulation,[],[f30822,f22045]) ).
fof(f30929,plain,
sF10 = addition(sF8,zero),
inference(forward_demodulation,[],[f30902,f7048]) ).
fof(f30944,plain,
sF8 = sF10,
inference(forward_demodulation,[],[f30929,f34]) ).
fof(f30957,plain,
sF11 = multiplication(sF8,sK0),
inference(superposition,[],[f84,f30944]) ).
fof(f31004,plain,
addition(sF22,sF11) = multiplication(addition(sF21,sF8),sK0),
inference(superposition,[],[f175,f30957]) ).
fof(f31054,plain,
multiplication(sF21,sK0) = addition(sF22,sF11),
inference(forward_demodulation,[],[f31004,f12569]) ).
fof(f31062,plain,
sF22 = addition(sF22,sF11),
inference(forward_demodulation,[],[f31054,f108]) ).
fof(f31317,plain,
coantidomain(sF11) = addition(coantidomain(sF11),coantidomain(sF22)),
inference(superposition,[],[f20455,f31062]) ).
fof(f31324,plain,
coantidomain(sF11) = addition(coantidomain(sF11),sF23),
inference(forward_demodulation,[],[f31317,f110]) ).
fof(f31344,plain,
sF12 = addition(sF12,sF23),
inference(forward_demodulation,[],[f31324,f86]) ).
fof(f31560,plain,
coantidomain(sF23) = addition(coantidomain(sF23),coantidomain(sF12)),
inference(superposition,[],[f20455,f31344]) ).
fof(f31567,plain,
coantidomain(sF23) = addition(coantidomain(sF23),sF13),
inference(forward_demodulation,[],[f31560,f88]) ).
fof(f31587,plain,
sF24 = addition(sF24,sF13),
inference(forward_demodulation,[],[f31567,f112]) ).
fof(f31694,plain,
sF13 = multiplication(sF13,coantidomain(coantidomain(sF24))),
inference(superposition,[],[f4467,f31587]) ).
fof(f31720,plain,
sF13 = multiplication(sF13,sF24),
inference(forward_demodulation,[],[f31694,f2610]) ).
fof(f31788,plain,
addition(sF13,multiplication(addition(sF13,sF5),sF19)) = multiplication(sF13,addition(sF24,sF19)),
inference(superposition,[],[f1771,f31720]) ).
fof(f31794,plain,
addition(sF13,multiplication(addition(sF13,sF5),sF19)) = multiplication(sF13,sF19),
inference(forward_demodulation,[],[f31788,f120]) ).
fof(f31804,plain,
addition(sF13,multiplication(sF5,sF19)) = multiplication(sF13,sF19),
inference(forward_demodulation,[],[f31794,f7810]) ).
fof(f31811,plain,
addition(sF13,zero) = multiplication(sF13,sF19),
inference(forward_demodulation,[],[f31804,f1739]) ).
fof(f31813,plain,
sF13 = multiplication(sF13,sF19),
inference(forward_demodulation,[],[f31811,f34]) ).
fof(f31822,plain,
addition(sF19,sF13) = multiplication(addition(one,sF13),sF19),
inference(superposition,[],[f177,f31813]) ).
fof(f31856,plain,
multiplication(one,sF19) = addition(sF19,sF13),
inference(forward_demodulation,[],[f31822,f6155]) ).
fof(f31867,plain,
sF19 = addition(sF19,sF13),
inference(forward_demodulation,[],[f31856,f38]) ).
fof(f32239,plain,
addition(sF6,sF19) = addition(sF6,sF13),
inference(superposition,[],[f320,f31867]) ).
fof(f32301,plain,
sF14 = addition(sF6,sF19),
inference(forward_demodulation,[],[f32239,f16062]) ).
fof(f32314,plain,
sF6 = sF14,
inference(forward_demodulation,[],[f32301,f125]) ).
fof(f32323,plain,
$false,
inference(forward_subsumption_resolution,[],[f32314,f91]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE124+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n018.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 13:13:23 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.41 Running first-order theorem proving
% 0.11/0.41 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
% 11.58/2.55 % (2341038)Detected formulas, will run a generic FOF schedule.
% 11.58/2.55 % (2341047)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1383163862:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.58/2.55 % (2341047)Instruction limit reached!
% 11.58/2.55 % (2341047)------------------------------
% 11.58/2.55 % (2341047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/2.55 % (2341047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/2.55 % (2341047)CaDiCaL version: 2.1.3
% 11.58/2.55 % (2341047)Termination reason: Instruction limit
% 11.58/2.55 % (2341047)Termination phase: Saturation
% 11.58/2.55 % (2341047)Time elapsed: 0.035 s
% 11.58/2.55 % (2341047)Peak memory usage: 88 MB
% 11.58/2.55 % (2341047)Instructions burned: 122 (million)
% 11.58/2.55 % (2341044)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4282181202:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.58/2.55 % (2341046)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2713139449:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.58/2.55 % (2341043)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=2530203116:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.58/2.55 % (2341049)dis-21_1_sil=8000:lcm=predicate:random_seed=2949508243:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.58/2.55 % (2341045)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2851301850:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.58/2.55 % (2341048)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=184189615:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.58/2.55 % (2341049)Refutation not found, incomplete strategy
% 11.58/2.55 % (2341049)------------------------------
% 11.58/2.55 % (2341049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/2.55 % (2341049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/2.55 % (2341049)CaDiCaL version: 2.1.3
% 11.58/2.55 % (2341049)Termination reason: Refutation not found, incomplete strategy
% 11.58/2.55 % (2341049)Time elapsed: 0.002 s
% 11.58/2.55 % (2341049)Peak memory usage: 88 MB
% 11.58/2.55 % (2341049)Instructions burned: 1 (million)
% 11.58/2.55 % (2341046)Instruction limit reached!
% 11.58/2.55 % (2341046)------------------------------
% 11.58/2.55 % (2341046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/2.55 % (2341046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/2.55 % (2341046)CaDiCaL version: 2.1.3
% 11.58/2.55 % (2341046)Termination reason: Instruction limit
% 11.58/2.55 % (2341046)Termination phase: Saturation
% 11.58/2.55 % (2341046)Time elapsed: 0.062 s
% 11.58/2.55 % (2341046)Peak memory usage: 88 MB
% 11.58/2.55 % (2341046)Instructions burned: 110 (million)
% 11.58/2.55 % (2341048)Instruction limit reached!
% 11.58/2.55 % (2341048)------------------------------
% 11.58/2.55 % (2341048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/2.55 % (2341048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/2.55 % (2341048)CaDiCaL version: 2.1.3
% 11.58/2.55 % (2341048)Termination reason: Instruction limit
% 11.58/2.55 % (2341048)Termination phase: Saturation
% 11.58/2.55 % (2341048)Time elapsed: 0.082 s
% 11.58/2.55 % (2341048)Peak memory usage: 89 MB
% 11.58/2.55 % (2341048)Instructions burned: 139 (million)
% 11.58/2.55 % (2341051)lrs+10_1_sil=8000:sp=occurrence:random_seed=1328212333:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.58/2.55 % (2341051)Instruction limit reached!
% 11.58/2.55 % (2341051)------------------------------
% 11.58/2.55 % (2341051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/2.55 % (2341051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/2.55 % (2341051)CaDiCaL version: 2.1.3
% 11.58/2.55 % (2341051)Termination reason: Instruction limit
% 11.58/2.55 % (2341051)Termination phase: Saturation
% 11.58/2.55 % (2341051)Time elapsed: 0.091 s
% 11.58/2.55 % (2341051)Peak memory usage: 92 MB
% 11.58/2.55 % (2341051)Instructions burned: 288 (million)
% 19.34/3.63 % (2341058)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1328912348:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 19.34/3.63 % (2341049)------------------------------
% 19.34/3.63 % (2341049)------------------------------
% 19.34/3.63 % (2341059)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3429193546:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 19.34/3.63 % (2341058)Instruction limit reached!
% 19.34/3.63 % (2341058)------------------------------
% 19.34/3.63 % (2341058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.63 % (2341058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.34/3.63 % (2341058)CaDiCaL version: 2.1.3
% 19.34/3.63 % (2341058)Termination reason: Instruction limit
% 19.34/3.63 % (2341058)Termination phase: Saturation
% 19.34/3.63 % (2341058)Time elapsed: 0.088 s
% 19.34/3.63 % (2341058)Peak memory usage: 89 MB
% 19.34/3.63 % (2341058)Instructions burned: 158 (million)
% 19.34/3.63 % (2341061)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2186529331:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 19.34/3.63 % (2341061)Instruction limit reached!
% 19.34/3.63 % (2341061)------------------------------
% 19.34/3.63 % (2341061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.63 % (2341061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.34/3.63 % (2341061)CaDiCaL version: 2.1.3
% 19.34/3.63 % (2341061)Termination reason: Instruction limit
% 19.34/3.63 % (2341061)Termination phase: Saturation
% 19.34/3.63 % (2341061)Time elapsed: 0.078 s
% 19.34/3.63 % (2341061)Peak memory usage: 91 MB
% 19.34/3.63 % (2341061)Instructions burned: 248 (million)
% 19.34/3.63 % (2341064)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1362758239:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.34/3.63 % (2341059)Instruction limit reached!
% 19.34/3.63 % (2341059)------------------------------
% 19.34/3.63 % (2341059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.63 % (2341059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.34/3.63 % (2341059)CaDiCaL version: 2.1.3
% 19.34/3.63 % (2341059)Termination reason: Instruction limit
% 19.34/3.63 % (2341059)Termination phase: Saturation
% 19.34/3.63 % (2341059)Time elapsed: 0.196 s
% 19.34/3.63 % (2341059)Peak memory usage: 92 MB
% 19.34/3.63 % (2341059)Instructions burned: 325 (million)
% 19.34/3.63 % (2341065)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1968229487:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 19.34/3.63 % (2341067)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2492873915:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 19.34/3.63 % (2341067)Instruction limit reached!
% 19.34/3.63 % (2341067)------------------------------
% 19.34/3.63 % (2341067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.63 % (2341067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.34/3.63 % (2341067)CaDiCaL version: 2.1.3
% 19.34/3.63 % (2341067)Termination reason: Instruction limit
% 19.34/3.63 % (2341067)Termination phase: Saturation
% 19.34/3.63 % (2341067)Time elapsed: 0.037 s
% 19.34/3.63 % (2341067)Peak memory usage: 90 MB
% 19.34/3.63 % (2341067)Instructions burned: 115 (million)
% 19.34/3.63 % (2341064)Instruction limit reached!
% 19.34/3.63 % (2341064)------------------------------
% 19.34/3.63 % (2341064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.63 % (2341064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.34/3.63 % (2341064)CaDiCaL version: 2.1.3
% 19.34/3.63 % (2341064)Termination reason: Instruction limit
% 19.34/3.63 % (2341064)Termination phase: Saturation
% 19.34/3.63 % (2341064)Time elapsed: 0.171 s
% 19.34/3.63 % (2341064)Peak memory usage: 90 MB
% 19.34/3.63 % (2341064)Instructions burned: 296 (million)
% 19.34/3.63 % (2341069)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2486182137:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 19.34/3.63 % (2341069)Refutation not found, incomplete strategy
% 19.34/3.63 % (2341069)------------------------------
% 19.34/3.63 % (2341069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.63 % (2341069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.33 % (2341069)CaDiCaL version: 2.1.3
% 24.54/4.33 % (2341069)Termination reason: Refutation not found, incomplete strategy
% 24.54/4.33 % (2341069)Time elapsed: 0.001 s
% 24.54/4.33 % (2341069)Peak memory usage: 88 MB
% 24.54/4.33 % (2341069)Instructions burned: 1 (million)
% 24.54/4.33 % (2341072)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=768806044:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 24.54/4.33 % (2341072)Instruction limit reached!
% 24.54/4.33 % (2341072)------------------------------
% 24.54/4.33 % (2341072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.33 % (2341072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.33 % (2341072)CaDiCaL version: 2.1.3
% 24.54/4.33 % (2341072)Termination reason: Instruction limit
% 24.54/4.33 % (2341072)Termination phase: Saturation
% 24.54/4.33 % (2341072)Time elapsed: 0.031 s
% 24.54/4.33 % (2341072)Peak memory usage: 88 MB
% 24.54/4.33 % (2341072)Instructions burned: 116 (million)
% 24.54/4.33 % (2341073)lrs+10_1_sil=8000:sp=occurrence:random_seed=1520888503:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 24.54/4.33 % (2341076)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2414925907:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 24.54/4.33 % (2341069)------------------------------
% 24.54/4.33 % (2341069)------------------------------
% 24.54/4.33 % (2341076)Instruction limit reached!
% 24.54/4.33 % (2341076)------------------------------
% 24.54/4.33 % (2341076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.33 % (2341076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.33 % (2341076)CaDiCaL version: 2.1.3
% 24.54/4.33 % (2341076)Termination reason: Instruction limit
% 24.54/4.33 % (2341076)Termination phase: Saturation
% 24.54/4.33 % (2341076)Time elapsed: 0.117 s
% 24.54/4.33 % (2341076)Peak memory usage: 90 MB
% 24.54/4.33 % (2341076)Instructions burned: 439 (million)
% 24.54/4.33 % (2341079)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=145314671:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 24.54/4.33 % (2341080)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2981514033:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 24.54/4.33 % (2341080)Refutation not found, incomplete strategy
% 24.54/4.33 % (2341080)------------------------------
% 24.54/4.33 % (2341080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.33 % (2341080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.33 % (2341080)CaDiCaL version: 2.1.3
% 24.54/4.33 % (2341080)Termination reason: Refutation not found, incomplete strategy
% 24.54/4.33 % (2341080)Time elapsed: 0.001 s
% 24.54/4.33 % (2341080)Peak memory usage: 88 MB
% 24.54/4.33 % (2341080)Instructions burned: 1 (million)
% 24.54/4.33 % (2341080)------------------------------
% 24.54/4.33 % (2341080)------------------------------
% 24.54/4.33 % (2341073)Instruction limit reached!
% 24.54/4.33 % (2341073)------------------------------
% 24.54/4.33 % (2341073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.33 % (2341073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.33 % (2341073)CaDiCaL version: 2.1.3
% 24.54/4.33 % (2341073)Termination reason: Instruction limit
% 24.54/4.33 % (2341073)Termination phase: Saturation
% 24.54/4.33 % (2341073)Time elapsed: 0.541 s
% 24.54/4.33 % (2341073)Peak memory usage: 98 MB
% 24.54/4.33 % (2341073)Instructions burned: 909 (million)
% 24.54/4.33 % (2341083)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2501803494:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 24.54/4.33 % (2341084)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2295981305:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 24.54/4.33 % (2341083)Instruction limit reached!
% 24.54/4.33 % (2341083)------------------------------
% 24.54/4.33 % (2341083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.33 % (2341083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.33 % (2341083)CaDiCaL version: 2.1.3
% 24.54/4.33 % (2341083)Termination reason: Instruction limit
% 24.54/4.33 % (2341083)Termination phase: Saturation
% 24.54/4.33 % (2341083)Time elapsed: 0.194 s
% 24.54/4.33 % (2341083)Peak memory usage: 96 MB
% 24.54/4.33 % (2341083)Instructions burned: 592 (million)
% 24.54/4.34 % (2341087)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1354258604:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 24.54/4.34 % (2341087)Instruction limit reached!
% 24.54/4.34 % (2341087)------------------------------
% 24.54/4.34 % (2341087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.34 % (2341087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.34 % (2341087)CaDiCaL version: 2.1.3
% 24.54/4.34 % (2341087)Termination reason: Instruction limit
% 24.54/4.34 % (2341087)Termination phase: Saturation
% 24.54/4.34 % (2341087)Time elapsed: 0.044 s
% 24.54/4.34 % (2341087)Peak memory usage: 90 MB
% 24.54/4.34 % (2341087)Instructions burned: 128 (million)
% 24.54/4.34 % (2341089)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3280021117:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 24.54/4.34 % (2341065)Instruction limit reached!
% 24.54/4.34 % (2341065)------------------------------
% 24.54/4.34 % (2341065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.34 % (2341065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.34 % (2341065)CaDiCaL version: 2.1.3
% 24.54/4.34 % (2341065)Termination reason: Instruction limit
% 24.54/4.34 % (2341065)Termination phase: Saturation
% 24.54/4.34 % (2341065)Time elapsed: 1.453 s
% 24.54/4.34 % (2341065)Peak memory usage: 144 MB
% 24.54/4.34 % (2341065)Instructions burned: 2352 (million)
% 24.54/4.34 % (2341089)Instruction limit reached!
% 24.54/4.34 % (2341089)------------------------------
% 24.54/4.34 % (2341089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.34 % (2341089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.34 % (2341089)CaDiCaL version: 2.1.3
% 24.54/4.34 % (2341089)Termination reason: Instruction limit
% 24.54/4.34 % (2341089)Termination phase: Saturation
% 24.54/4.34 % (2341089)Time elapsed: 0.073 s
% 24.54/4.34 % (2341089)Peak memory usage: 89 MB
% 24.54/4.34 % (2341089)Instructions burned: 135 (million)
% 24.54/4.34 % (2341091)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1434909249:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 24.54/4.34 % (2341091)Refutation not found, incomplete strategy
% 24.54/4.34 % (2341091)------------------------------
% 24.54/4.34 % (2341091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.34 % (2341091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.34 % (2341091)CaDiCaL version: 2.1.3
% 24.54/4.34 % (2341091)Termination reason: Refutation not found, incomplete strategy
% 24.54/4.34 % (2341091)Time elapsed: 0.001 s
% 24.54/4.34 % (2341091)Peak memory usage: 88 MB
% 24.54/4.34 % (2341092)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3950810778:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi)
% 24.54/4.34 % (2341092)Refutation not found, incomplete strategy
% 24.54/4.34 % (2341092)------------------------------
% 24.54/4.34 % (2341092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.34 % (2341092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.34 % (2341092)CaDiCaL version: 2.1.3
% 24.54/4.34 % (2341092)Termination reason: Refutation not found, incomplete strategy
% 24.54/4.34 % (2341092)Time elapsed: 0.002 s
% 24.54/4.34 % (2341092)Peak memory usage: 88 MB
% 24.54/4.34 % (2341092)Instructions burned: 1 (million)
% 24.54/4.34 % (2341091)------------------------------
% 24.54/4.34 % (2341091)------------------------------
% 24.54/4.34 % (2341092)------------------------------
% 24.54/4.34 % (2341092)------------------------------
% 24.54/4.34 % (2341095)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=476495819:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 24.54/4.34 % (2341096)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3479376413:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 24.54/4.34 % (2341096)Instruction limit reached!
% 24.54/4.34 % (2341096)------------------------------
% 24.54/4.34 % (2341096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.34 % (2341096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.34 % (2341096)CaDiCaL version: 2.1.3
% 24.54/4.34 % (2341096)Termination reason: Instruction limit
% 24.54/4.34 % (2341096)Termination phase: Saturation
% 24.54/4.34 % (2341096)Time elapsed: 0.087 s
% 24.54/4.34 % (2341096)Peak memory usage: 90 MB
% 24.54/4.34 % (2341096)Instructions burned: 151 (million)
% 24.54/4.34 % (2341099)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=337853440:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi)
% 24.54/4.34 % (2341079)Instruction limit reached!
% 24.54/4.34 % (2341079)------------------------------
% 24.54/4.34 % (2341079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.34 % (2341079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.34 % (2341079)CaDiCaL version: 2.1.3
% 24.54/4.34 % (2341079)Termination reason: Instruction limit
% 24.54/4.34 % (2341079)Termination phase: Saturation
% 24.54/4.34 % (2341079)Time elapsed: 2.022 s
% 24.54/4.34 % (2341079)Peak memory usage: 169 MB
% 24.54/4.34 % (2341079)Instructions burned: 5204 (million)
% 24.54/4.34 % (2341043)First to succeed.
% 24.54/4.34 % (2341043)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2341038"
% 24.54/4.34 % (2341101)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1201083728:i=667:av=off:fsr=off_2967 on theBenchmark for (2967ds/667Mi)
% 24.54/4.34 % (2341101)Instruction limit reached!
% 24.54/4.34 % (2341101)------------------------------
% 24.54/4.34 % (2341101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.54/4.34 % (2341101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.54/4.34 % (2341101)CaDiCaL version: 2.1.3
% 24.54/4.34 % (2341101)Termination reason: Instruction limit
% 24.54/4.34 % (2341101)Termination phase: Saturation
% 24.54/4.34 % (2341101)Time elapsed: 0.133 s
% 24.54/4.34 % (2341101)Peak memory usage: 88 MB
% 24.54/4.34 % (2341101)Instructions burned: 669 (million)
% 24.54/4.34 % (2341043)Refutation found. Thanks to Tanya!
% 24.54/4.34 % SZS status Theorem for theBenchmark
% 24.54/4.34 % SZS output start Proof for theBenchmark
% See solution above
% 25.18/4.53 % (2341043)------------------------------
% 25.18/4.53 % (2341043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.18/4.53 % (2341043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.18/4.53 % (2341043)CaDiCaL version: 2.1.3
% 25.18/4.53 % (2341043)Termination reason: Refutation
% 25.18/4.53 % (2341043)Time elapsed: 3.037 s
% 25.18/4.53 % (2341043)Peak memory usage: 171 MB
% 25.18/4.53 % (2341043)Instructions burned: 5005 (million)
% 25.18/4.53 % (2341043)------------------------------
% 25.18/4.53 % (2341043)------------------------------
% 25.18/4.53 % (2341038)Success in time 3.484 s
% 25.18/4.53 % Vampire exiting
%------------------------------------------------------------------------------