%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE108+1 : TPTP v9.3.1. Released v4.0.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:21 AM UTC 2026
% Result : Theorem 38.51s 6.69s
% Output : Refutation 39.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 118
% Number of leaves : 24
% Syntax : Number of formulae : 416 ( 412 unt; 0 def)
% Number of atoms : 420 ( 419 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 14 ( 10 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-2 aty)
% Number of variables : 641 ( 638 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_associativity) ).
fof(f3,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_idempotence) ).
fof(f5,axiom,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',left_distributivity) ).
fof(f10,axiom,
! [X0] : multiplication(X0,zero) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_annihilation) ).
fof(f11,axiom,
! [X0] : multiplication(zero,X0) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_annihilation) ).
fof(f13,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain1) ).
fof(f14,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(f15,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain3) ).
fof(f16,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain4) ).
fof(f17,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',codomain2) ).
fof(f19,axiom,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain3) ).
fof(f20,axiom,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain4) ).
fof(f21,axiom,
! [X0] : c(X0) = antidomain(domain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement) ).
fof(f23,axiom,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',forward_diamond) ).
fof(f24,axiom,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',backward_diamond) ).
fof(f25,axiom,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',forward_box) ).
fof(f27,conjecture,
! [X0,X1,X2] :
( addition(domain(X1),forward_box(X0,domain(X2))) = forward_box(X0,domain(X2))
=> addition(backward_diamond(X0,domain(X1)),domain(X2)) = domain(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f28,negated_conjecture,
~ ! [X0,X1,X2] :
( addition(domain(X1),forward_box(X0,domain(X2))) = forward_box(X0,domain(X2))
=> addition(backward_diamond(X0,domain(X1)),domain(X2)) = domain(X2) ),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f29,plain,
? [X0,X1,X2] :
( domain(X2) != addition(backward_diamond(X0,domain(X1)),domain(X2))
& addition(domain(X1),forward_box(X0,domain(X2))) = forward_box(X0,domain(X2)) ),
inference(ennf_transformation,[],[f28]) ).
fof(f30,plain,
( domain(sK2) != addition(backward_diamond(sK0,domain(sK1)),domain(sK2))
& forward_box(sK0,domain(sK2)) = addition(domain(sK1),forward_box(sK0,domain(sK2))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f29]) ).
fof(f31,plain,
forward_box(sK0,domain(sK2)) = addition(domain(sK1),forward_box(sK0,domain(sK2))),
inference(cnf_transformation,[],[f30]) ).
fof(f32,plain,
domain(sK2) != addition(backward_diamond(sK0,domain(sK1)),domain(sK2)),
inference(cnf_transformation,[],[f30]) ).
fof(f33,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f34,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f35,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f36,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f37,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f38,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(cnf_transformation,[],[f23]) ).
fof(f40,plain,
! [X0] : c(X0) = antidomain(domain(X0)),
inference(cnf_transformation,[],[f21]) ).
fof(f41,plain,
! [X0] : antidomain(antidomain(X0)) = domain(X0),
inference(cnf_transformation,[],[f16]) ).
fof(f43,plain,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
inference(cnf_transformation,[],[f24]) ).
fof(f44,plain,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
inference(cnf_transformation,[],[f25]) ).
fof(f45,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f46,plain,
! [X0] : one = addition(antidomain(antidomain(X0)),antidomain(X0)),
inference(cnf_transformation,[],[f15]) ).
fof(f47,plain,
! [X0,X1] : antidomain(multiplication(X0,antidomain(antidomain(X1)))) = addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(cnf_transformation,[],[f14]) ).
fof(f48,plain,
! [X0] : zero = multiplication(antidomain(X0),X0),
inference(cnf_transformation,[],[f13]) ).
fof(f49,plain,
! [X0] : coantidomain(coantidomain(X0)) = codomain(X0),
inference(cnf_transformation,[],[f20]) ).
fof(f50,plain,
! [X0] : one = addition(coantidomain(coantidomain(X0)),coantidomain(X0)),
inference(cnf_transformation,[],[f19]) ).
fof(f51,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f52,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f53,plain,
! [X0] : zero = multiplication(X0,coantidomain(X0)),
inference(cnf_transformation,[],[f17]) ).
fof(f54,plain,
! [X0] : zero = multiplication(zero,X0),
inference(cnf_transformation,[],[f11]) ).
fof(f55,plain,
! [X0] : zero = multiplication(X0,zero),
inference(cnf_transformation,[],[f10]) ).
fof(f56,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f57,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(f58,plain,
! [X0] : c(X0) = antidomain(antidomain(antidomain(X0))),
inference(definition_unfolding,[],[f40,f41]) ).
fof(f59,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f43,f49,f49]) ).
fof(f62,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f38,f41,f41]) ).
fof(f63,plain,
! [X0,X1] : forward_box(X0,X1) = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(X0,antidomain(antidomain(antidomain(antidomain(antidomain(X1))))))))))),
inference(definition_unfolding,[],[f44,f58,f62,f58]) ).
fof(f64,plain,
antidomain(antidomain(sK2)) != addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK1)))),sK0))),antidomain(antidomain(sK2))),
inference(definition_unfolding,[],[f32,f41,f59,f41,f41]) ).
fof(f65,plain,
antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2))))))))))))) = addition(antidomain(antidomain(sK1)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2)))))))))))))),
inference(definition_unfolding,[],[f31,f63,f41,f41,f63,f41]) ).
fof(f66,plain,
antidomain(antidomain(sK2)) != addition(antidomain(antidomain(sK2)),coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK1)))),sK0)))),
inference(forward_demodulation,[],[f64,f37]) ).
fof(f70,plain,
! [X0] : one = addition(antidomain(X0),antidomain(antidomain(X0))),
inference(superposition,[],[f37,f46]) ).
fof(f72,plain,
zero = coantidomain(one),
inference(superposition,[],[f51,f53]) ).
fof(f73,plain,
! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)),
inference(superposition,[],[f33,f51]) ).
fof(f74,plain,
! [X0,X1] : multiplication(addition(antidomain(X0),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(superposition,[],[f33,f48]) ).
fof(f77,plain,
! [X0,X1] : multiplication(addition(X0,antidomain(X1)),X1) = addition(multiplication(X0,X1),zero),
inference(superposition,[],[f33,f48]) ).
fof(f78,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = addition(multiplication(X0,coantidomain(X1)),zero),
inference(superposition,[],[f33,f53]) ).
fof(f83,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = multiplication(X0,coantidomain(X1)),
inference(forward_demodulation,[],[f78,f56]) ).
fof(f84,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(addition(X0,antidomain(X1)),X1),
inference(forward_demodulation,[],[f77,f56]) ).
fof(f89,plain,
! [X0] : one = addition(coantidomain(X0),coantidomain(coantidomain(X0))),
inference(superposition,[],[f37,f50]) ).
fof(f90,plain,
one = addition(coantidomain(zero),zero),
inference(superposition,[],[f50,f72]) ).
fof(f92,plain,
one = coantidomain(zero),
inference(forward_demodulation,[],[f90,f56]) ).
fof(f100,plain,
! [X0,X1] : multiplication(X1,X0) = multiplication(addition(antidomain(X0),X1),X0),
inference(superposition,[],[f84,f37]) ).
fof(f102,plain,
! [X0] : multiplication(one,X0) = multiplication(antidomain(antidomain(X0)),X0),
inference(superposition,[],[f84,f46]) ).
fof(f107,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f102,f51]) ).
fof(f136,plain,
zero = antidomain(one),
inference(superposition,[],[f48,f52]) ).
fof(f145,plain,
one = addition(antidomain(zero),zero),
inference(superposition,[],[f46,f136]) ).
fof(f146,plain,
one = antidomain(zero),
inference(forward_demodulation,[],[f145,f56]) ).
fof(f152,plain,
! [X0] : addition(zero,X0) = X0,
inference(superposition,[],[f37,f56]) ).
fof(f154,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X0,X1)) = addition(zero,multiplication(antidomain(X0),X1)),
inference(superposition,[],[f34,f48]) ).
fof(f156,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(superposition,[],[f34,f52]) ).
fof(f160,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X1,X0)) = addition(multiplication(antidomain(X0),X1),zero),
inference(superposition,[],[f34,f48]) ).
fof(f163,plain,
! [X0,X1] : addition(multiplication(X0,X1),zero) = multiplication(X0,addition(X1,coantidomain(X0))),
inference(superposition,[],[f34,f53]) ).
fof(f178,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(X0,addition(X1,coantidomain(X0))),
inference(forward_demodulation,[],[f163,f56]) ).
fof(f181,plain,
! [X0,X1] : multiplication(antidomain(X0),X1) = multiplication(antidomain(X0),addition(X1,X0)),
inference(forward_demodulation,[],[f160,f56]) ).
fof(f184,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X0,X1)) = multiplication(antidomain(X0),X1),
inference(forward_demodulation,[],[f154,f152]) ).
fof(f190,plain,
! [X2,X0,X1] : multiplication(antidomain(multiplication(X1,X2)),multiplication(X0,X2)) = multiplication(antidomain(multiplication(X1,X2)),multiplication(addition(X0,X1),X2)),
inference(superposition,[],[f181,f33]) ).
fof(f191,plain,
! [X2,X0,X1] : multiplication(antidomain(multiplication(X0,X2)),multiplication(X0,X1)) = multiplication(antidomain(multiplication(X0,X2)),multiplication(X0,addition(X1,X2))),
inference(superposition,[],[f181,f34]) ).
fof(f221,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,[],[f190,f50]) ).
fof(f232,plain,
! [X0,X1] : multiplication(antidomain(multiplication(coantidomain(X0),X1)),multiplication(coantidomain(coantidomain(X0)),X1)) = multiplication(antidomain(multiplication(coantidomain(X0),X1)),X1),
inference(forward_demodulation,[],[f221,f51]) ).
fof(f248,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f36,f35]) ).
fof(f252,plain,
! [X2,X3,X0,X1] : addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)) = addition(multiplication(X0,addition(X1,X2)),X3),
inference(superposition,[],[f36,f34]) ).
fof(f265,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(superposition,[],[f37,f36]) ).
fof(f301,plain,
! [X0,X1] : addition(multiplication(X1,X0),X0) = multiplication(addition(X1,antidomain(antidomain(X0))),X0),
inference(superposition,[],[f33,f107]) ).
fof(f306,plain,
! [X0,X1] : addition(X0,multiplication(X1,X0)) = multiplication(addition(X1,antidomain(antidomain(X0))),X0),
inference(forward_demodulation,[],[f301,f37]) ).
fof(f310,plain,
! [X0,X1] : multiplication(addition(one,X1),X0) = multiplication(addition(X1,antidomain(antidomain(X0))),X0),
inference(forward_demodulation,[],[f306,f73]) ).
fof(f319,plain,
! [X0] : multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)) = multiplication(antidomain(antidomain(antidomain(X0))),one),
inference(superposition,[],[f184,f46]) ).
fof(f330,plain,
! [X0] : antidomain(antidomain(antidomain(X0))) = multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)),
inference(forward_demodulation,[],[f319,f52]) ).
fof(f335,plain,
! [X0] : antidomain(X0) = antidomain(antidomain(antidomain(X0))),
inference(forward_demodulation,[],[f330,f107]) ).
fof(f347,plain,
antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(sK2))))))))))) = addition(antidomain(antidomain(sK1)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(sK2)))))))))))),
inference(superposition,[],[f65,f335]) ).
fof(f352,plain,
! [X0,X1] : multiplication(X1,antidomain(antidomain(X0))) = multiplication(addition(X1,antidomain(X0)),antidomain(antidomain(X0))),
inference(superposition,[],[f84,f335]) ).
fof(f356,plain,
antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(sK2))))))))) = addition(antidomain(antidomain(sK1)),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(sK2)))))))))),
inference(forward_demodulation,[],[f347,f335]) ).
fof(f366,plain,
antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(sK2))))))) = addition(antidomain(antidomain(sK1)),antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(sK2)))))))),
inference(forward_demodulation,[],[f356,f335]) ).
fof(f374,plain,
antidomain(multiplication(sK0,antidomain(antidomain(antidomain(sK2))))) = addition(antidomain(antidomain(sK1)),antidomain(multiplication(sK0,antidomain(antidomain(antidomain(sK2)))))),
inference(forward_demodulation,[],[f366,f335]) ).
fof(f382,plain,
antidomain(multiplication(sK0,antidomain(sK2))) = addition(antidomain(antidomain(sK1)),antidomain(multiplication(sK0,antidomain(sK2)))),
inference(forward_demodulation,[],[f374,f335]) ).
fof(f391,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),X0) = addition(antidomain(antidomain(sK1)),addition(antidomain(multiplication(sK0,antidomain(sK2))),X0)),
inference(superposition,[],[f36,f382]) ).
fof(f393,plain,
multiplication(antidomain(antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(antidomain(sK1))) = multiplication(antidomain(antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(multiplication(sK0,antidomain(sK2)))),
inference(superposition,[],[f181,f382]) ).
fof(f396,plain,
zero = multiplication(antidomain(antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(antidomain(sK1))),
inference(forward_demodulation,[],[f393,f48]) ).
fof(f434,plain,
! [X0] : one = addition(antidomain(antidomain(X0)),one),
inference(superposition,[],[f248,f46]) ).
fof(f439,plain,
! [X0,X1] : multiplication(antidomain(addition(X0,X1)),X0) = multiplication(antidomain(addition(X0,X1)),addition(X0,X1)),
inference(superposition,[],[f181,f248]) ).
fof(f444,plain,
! [X0,X1] : zero = multiplication(antidomain(addition(X0,X1)),X0),
inference(forward_demodulation,[],[f439,f48]) ).
fof(f449,plain,
! [X0] : one = addition(one,antidomain(antidomain(X0))),
inference(forward_demodulation,[],[f434,f37]) ).
fof(f478,plain,
! [X0,X1] : multiplication(antidomain(multiplication(X0,antidomain(X1))),multiplication(X0,antidomain(antidomain(X1)))) = multiplication(antidomain(multiplication(X0,antidomain(X1))),multiplication(X0,one)),
inference(superposition,[],[f191,f46]) ).
fof(f479,plain,
! [X0,X1] : multiplication(antidomain(multiplication(X0,coantidomain(X1))),multiplication(X0,coantidomain(coantidomain(X1)))) = multiplication(antidomain(multiplication(X0,coantidomain(X1))),multiplication(X0,one)),
inference(superposition,[],[f191,f50]) ).
fof(f495,plain,
! [X0,X1] : multiplication(antidomain(multiplication(X0,coantidomain(X1))),multiplication(X0,coantidomain(coantidomain(X1)))) = multiplication(antidomain(multiplication(X0,coantidomain(X1))),X0),
inference(forward_demodulation,[],[f479,f52]) ).
fof(f496,plain,
! [X0,X1] : multiplication(antidomain(multiplication(X0,antidomain(X1))),multiplication(X0,antidomain(antidomain(X1)))) = multiplication(antidomain(multiplication(X0,antidomain(X1))),X0),
inference(forward_demodulation,[],[f478,f52]) ).
fof(f742,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,[],[f252,f33]) ).
fof(f906,plain,
! [X0,X1] : multiplication(zero,X1) = multiplication(antidomain(X0),multiplication(X0,X1)),
inference(superposition,[],[f45,f48]) ).
fof(f927,plain,
! [X2,X0,X1] : coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),X2)) = addition(coantidomain(multiplication(X0,multiplication(X1,X2))),coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),X2))),
inference(superposition,[],[f57,f45]) ).
fof(f955,plain,
! [X0,X1] : zero = multiplication(antidomain(X0),multiplication(X0,X1)),
inference(forward_demodulation,[],[f906,f54]) ).
fof(f987,plain,
! [X0,X1] : coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1))) = addition(coantidomain(multiplication(X0,zero)),coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1)))),
inference(superposition,[],[f927,f53]) ).
fof(f1051,plain,
! [X0,X1] : coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1))) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1)))),
inference(forward_demodulation,[],[f987,f55]) ).
fof(f1069,plain,
! [X0,X1] : coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1))) = addition(one,coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1)))),
inference(forward_demodulation,[],[f1051,f92]) ).
fof(f1317,plain,
! [X0] : one = addition(one,antidomain(X0)),
inference(superposition,[],[f449,f335]) ).
fof(f1402,plain,
! [X0] : multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))) = multiplication(one,coantidomain(coantidomain(coantidomain(X0)))),
inference(superposition,[],[f83,f89]) ).
fof(f1407,plain,
! [X0] : one = addition(coantidomain(X0),one),
inference(superposition,[],[f248,f89]) ).
fof(f1408,plain,
! [X0] : one = addition(one,coantidomain(X0)),
inference(forward_demodulation,[],[f1407,f37]) ).
fof(f1413,plain,
! [X0] : coantidomain(coantidomain(coantidomain(X0))) = multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f1402,f51]) ).
fof(f1433,plain,
! [X2,X0,X1] : addition(multiplication(X0,antidomain(antidomain(X1))),multiplication(addition(X0,X2),antidomain(X1))) = addition(multiplication(X0,one),multiplication(X2,antidomain(X1))),
inference(superposition,[],[f742,f46]) ).
fof(f1500,plain,
! [X2,X0,X1] : addition(multiplication(antidomain(antidomain(X0)),addition(X1,X2)),multiplication(antidomain(X0),X2)) = addition(multiplication(antidomain(antidomain(X0)),X1),multiplication(one,X2)),
inference(superposition,[],[f742,f46]) ).
fof(f1501,plain,
! [X2,X0,X1] : addition(multiplication(coantidomain(coantidomain(X0)),addition(X1,X2)),multiplication(coantidomain(X0),X2)) = addition(multiplication(coantidomain(coantidomain(X0)),X1),multiplication(one,X2)),
inference(superposition,[],[f742,f50]) ).
fof(f1560,plain,
! [X2,X0,X1] : addition(multiplication(coantidomain(coantidomain(X0)),addition(X1,X2)),multiplication(coantidomain(X0),X2)) = addition(multiplication(coantidomain(coantidomain(X0)),X1),X2),
inference(forward_demodulation,[],[f1501,f51]) ).
fof(f1561,plain,
! [X2,X0,X1] : addition(multiplication(antidomain(antidomain(X0)),X1),X2) = addition(multiplication(antidomain(antidomain(X0)),addition(X1,X2)),multiplication(antidomain(X0),X2)),
inference(forward_demodulation,[],[f1500,f51]) ).
fof(f1616,plain,
! [X2,X0,X1] : addition(multiplication(X0,antidomain(antidomain(X1))),multiplication(addition(X0,X2),antidomain(X1))) = addition(X0,multiplication(X2,antidomain(X1))),
inference(forward_demodulation,[],[f1433,f52]) ).
fof(f1639,plain,
! [X2,X0,X1] : addition(multiplication(coantidomain(coantidomain(X0)),X1),X2) = addition(multiplication(coantidomain(X0),X2),multiplication(coantidomain(coantidomain(X0)),addition(X1,X2))),
inference(forward_demodulation,[],[f1560,f37]) ).
fof(f1640,plain,
! [X2,X0,X1] : addition(multiplication(antidomain(antidomain(X0)),X1),X2) = addition(multiplication(antidomain(X0),X2),multiplication(antidomain(antidomain(X0)),addition(X1,X2))),
inference(forward_demodulation,[],[f1561,f37]) ).
fof(f1744,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),antidomain(X1))) = addition(multiplication(antidomain(antidomain(X0)),antidomain(antidomain(X1))),multiplication(one,antidomain(X1))),
inference(superposition,[],[f1616,f46]) ).
fof(f1745,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(X1))) = addition(multiplication(coantidomain(coantidomain(X0)),antidomain(antidomain(X1))),multiplication(one,antidomain(X1))),
inference(superposition,[],[f1616,f50]) ).
fof(f1779,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(X1))) = addition(multiplication(one,antidomain(X1)),multiplication(coantidomain(coantidomain(X0)),antidomain(antidomain(X1)))),
inference(forward_demodulation,[],[f1745,f37]) ).
fof(f1780,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),antidomain(X1))) = addition(multiplication(one,antidomain(X1)),multiplication(antidomain(antidomain(X0)),antidomain(antidomain(X1)))),
inference(forward_demodulation,[],[f1744,f37]) ).
fof(f1810,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(X1))) = addition(antidomain(X1),multiplication(coantidomain(coantidomain(X0)),antidomain(antidomain(X1)))),
inference(forward_demodulation,[],[f1779,f51]) ).
fof(f1811,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),antidomain(X1))) = addition(antidomain(X1),multiplication(antidomain(antidomain(X0)),antidomain(antidomain(X1)))),
inference(forward_demodulation,[],[f1780,f51]) ).
fof(f2025,plain,
! [X0] : multiplication(one,coantidomain(antidomain(antidomain(X0)))) = multiplication(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(superposition,[],[f83,f70]) ).
fof(f2044,plain,
! [X0] : coantidomain(antidomain(antidomain(X0))) = multiplication(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(forward_demodulation,[],[f2025,f51]) ).
fof(f2064,plain,
! [X0] : multiplication(antidomain(X0),addition(one,coantidomain(antidomain(antidomain(X0))))) = addition(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(superposition,[],[f156,f2044]) ).
fof(f2077,plain,
! [X0] : multiplication(antidomain(X0),one) = addition(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(forward_demodulation,[],[f2064,f1408]) ).
fof(f2083,plain,
! [X0] : antidomain(X0) = addition(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(forward_demodulation,[],[f2077,f52]) ).
fof(f2137,plain,
! [X0] : multiplication(X0,one) = multiplication(X0,coantidomain(coantidomain(X0))),
inference(superposition,[],[f178,f50]) ).
fof(f2138,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,[],[f178,f57]) ).
fof(f2152,plain,
! [X0,X1] : multiplication(addition(one,X0),addition(X1,coantidomain(X0))) = addition(addition(X1,coantidomain(X0)),multiplication(X0,X1)),
inference(superposition,[],[f73,f178]) ).
fof(f2181,plain,
! [X0,X1] : multiplication(addition(one,X0),addition(X1,coantidomain(X0))) = addition(multiplication(X0,X1),addition(X1,coantidomain(X0))),
inference(forward_demodulation,[],[f2152,f37]) ).
fof(f2191,plain,
! [X0,X1] : zero = multiplication(multiplication(coantidomain(coantidomain(X0)),X1),coantidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f2138,f53]) ).
fof(f2192,plain,
! [X0] : multiplication(X0,coantidomain(coantidomain(X0))) = X0,
inference(forward_demodulation,[],[f2137,f52]) ).
fof(f2198,plain,
! [X0,X1] : multiplication(addition(one,X0),addition(X1,coantidomain(X0))) = addition(coantidomain(X0),addition(multiplication(X0,X1),X1)),
inference(forward_demodulation,[],[f2181,f265]) ).
fof(f2202,plain,
! [X0,X1] : zero = multiplication(coantidomain(coantidomain(X0)),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f2191,f45]) ).
fof(f2204,plain,
! [X0,X1] : multiplication(addition(one,X0),addition(X1,coantidomain(X0))) = addition(coantidomain(X0),addition(X1,multiplication(X0,X1))),
inference(forward_demodulation,[],[f2198,f37]) ).
fof(f2205,plain,
! [X0,X1] : multiplication(addition(one,X0),addition(X1,coantidomain(X0))) = addition(coantidomain(X0),multiplication(addition(one,X0),X1)),
inference(forward_demodulation,[],[f2204,f73]) ).
fof(f2235,plain,
! [X0] : coantidomain(X0) = coantidomain(coantidomain(coantidomain(X0))),
inference(superposition,[],[f1413,f2192]) ).
fof(f2345,plain,
! [X0] : zero = multiplication(coantidomain(coantidomain(antidomain(X0))),multiplication(X0,coantidomain(zero))),
inference(superposition,[],[f2202,f48]) ).
fof(f2428,plain,
! [X0] : zero = multiplication(coantidomain(coantidomain(antidomain(X0))),multiplication(X0,one)),
inference(forward_demodulation,[],[f2345,f92]) ).
fof(f2451,plain,
! [X0] : zero = multiplication(coantidomain(coantidomain(antidomain(X0))),X0),
inference(forward_demodulation,[],[f2428,f52]) ).
fof(f2600,plain,
multiplication(antidomain(zero),multiplication(antidomain(antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(antidomain(antidomain(sK1))))) = multiplication(antidomain(zero),antidomain(antidomain(multiplication(sK0,antidomain(sK2))))),
inference(superposition,[],[f496,f396]) ).
fof(f2637,plain,
multiplication(one,multiplication(antidomain(antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(antidomain(antidomain(sK1))))) = multiplication(one,antidomain(antidomain(multiplication(sK0,antidomain(sK2))))),
inference(forward_demodulation,[],[f2600,f146]) ).
fof(f2650,plain,
antidomain(antidomain(multiplication(sK0,antidomain(sK2)))) = multiplication(one,multiplication(antidomain(antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(antidomain(antidomain(sK1))))),
inference(forward_demodulation,[],[f2637,f51]) ).
fof(f2657,plain,
antidomain(antidomain(multiplication(sK0,antidomain(sK2)))) = multiplication(antidomain(antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(antidomain(antidomain(sK1)))),
inference(forward_demodulation,[],[f2650,f51]) ).
fof(f2659,plain,
antidomain(antidomain(multiplication(sK0,antidomain(sK2)))) = multiplication(antidomain(antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(sK1)),
inference(forward_demodulation,[],[f2657,f335]) ).
fof(f2721,plain,
! [X0] : multiplication(antidomain(X0),X0) = addition(zero,multiplication(coantidomain(antidomain(antidomain(X0))),X0)),
inference(superposition,[],[f74,f2083]) ).
fof(f2733,plain,
! [X0] : multiplication(antidomain(X0),X0) = multiplication(coantidomain(antidomain(antidomain(X0))),X0),
inference(forward_demodulation,[],[f2721,f152]) ).
fof(f2737,plain,
! [X0] : zero = multiplication(coantidomain(antidomain(antidomain(X0))),X0),
inference(forward_demodulation,[],[f2733,f48]) ).
fof(f3241,plain,
! [X0,X1] : addition(multiplication(antidomain(antidomain(X0)),one),antidomain(X1)) = addition(multiplication(antidomain(X0),antidomain(X1)),multiplication(antidomain(antidomain(X0)),one)),
inference(superposition,[],[f1640,f1317]) ).
fof(f3243,plain,
! [X0,X1] : addition(multiplication(antidomain(antidomain(X0)),one),coantidomain(X1)) = addition(multiplication(antidomain(X0),coantidomain(X1)),multiplication(antidomain(antidomain(X0)),one)),
inference(superposition,[],[f1640,f1408]) ).
fof(f3247,plain,
! [X0,X1] : addition(multiplication(antidomain(X0),antidomain(antidomain(X1))),multiplication(antidomain(antidomain(X0)),one)) = addition(multiplication(antidomain(antidomain(X0)),antidomain(X1)),antidomain(antidomain(X1))),
inference(superposition,[],[f1640,f70]) ).
fof(f3254,plain,
! [X0,X1] : addition(multiplication(antidomain(X0),coantidomain(coantidomain(X1))),multiplication(antidomain(antidomain(X0)),one)) = addition(multiplication(antidomain(antidomain(X0)),coantidomain(X1)),coantidomain(coantidomain(X1))),
inference(superposition,[],[f1640,f89]) ).
fof(f3282,plain,
! [X0,X1] : addition(multiplication(antidomain(X0),coantidomain(coantidomain(X1))),multiplication(antidomain(antidomain(X0)),one)) = addition(coantidomain(coantidomain(X1)),multiplication(antidomain(antidomain(X0)),coantidomain(X1))),
inference(forward_demodulation,[],[f3254,f37]) ).
fof(f3289,plain,
! [X0,X1] : addition(multiplication(antidomain(X0),antidomain(antidomain(X1))),multiplication(antidomain(antidomain(X0)),one)) = addition(antidomain(antidomain(X1)),multiplication(antidomain(antidomain(X0)),antidomain(X1))),
inference(forward_demodulation,[],[f3247,f37]) ).
fof(f3293,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),coantidomain(X1)) = addition(multiplication(antidomain(X0),coantidomain(X1)),antidomain(antidomain(X0))),
inference(forward_demodulation,[],[f3243,f52]) ).
fof(f3295,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),antidomain(X1)) = addition(multiplication(antidomain(X0),antidomain(X1)),antidomain(antidomain(X0))),
inference(forward_demodulation,[],[f3241,f52]) ).
fof(f3337,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X1)),multiplication(antidomain(antidomain(X0)),coantidomain(X1))) = addition(multiplication(antidomain(antidomain(X0)),one),multiplication(antidomain(X0),coantidomain(coantidomain(X1)))),
inference(forward_demodulation,[],[f3282,f37]) ).
fof(f3343,plain,
! [X0,X1] : addition(antidomain(antidomain(X1)),multiplication(antidomain(antidomain(X0)),antidomain(X1))) = addition(multiplication(antidomain(antidomain(X0)),one),multiplication(antidomain(X0),antidomain(antidomain(X1)))),
inference(forward_demodulation,[],[f3289,f37]) ).
fof(f3347,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),coantidomain(X1))) = addition(antidomain(antidomain(X0)),coantidomain(X1)),
inference(forward_demodulation,[],[f3293,f37]) ).
fof(f3349,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),antidomain(X1))) = addition(antidomain(antidomain(X0)),antidomain(X1)),
inference(forward_demodulation,[],[f3295,f37]) ).
fof(f3372,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X1)),multiplication(antidomain(antidomain(X0)),coantidomain(X1))) = addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),coantidomain(coantidomain(X1)))),
inference(forward_demodulation,[],[f3337,f52]) ).
fof(f3376,plain,
! [X0,X1] : addition(antidomain(antidomain(X1)),multiplication(antidomain(antidomain(X0)),antidomain(X1))) = addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),antidomain(antidomain(X1)))),
inference(forward_demodulation,[],[f3343,f52]) ).
fof(f3390,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X1)),multiplication(antidomain(antidomain(X0)),coantidomain(X1))) = addition(antidomain(antidomain(X0)),coantidomain(coantidomain(X1))),
inference(forward_demodulation,[],[f3372,f3347]) ).
fof(f3393,plain,
! [X0,X1] : addition(antidomain(antidomain(X1)),multiplication(antidomain(antidomain(X0)),antidomain(X1))) = addition(antidomain(antidomain(X0)),antidomain(antidomain(X1))),
inference(forward_demodulation,[],[f3376,f3349]) ).
fof(f3458,plain,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = addition(antidomain(antidomain(coantidomain(X0))),coantidomain(coantidomain(X0))),
inference(superposition,[],[f3390,f107]) ).
fof(f3477,plain,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = addition(coantidomain(coantidomain(X0)),antidomain(antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f3458,f37]) ).
fof(f3485,plain,
! [X0] : one = addition(coantidomain(coantidomain(X0)),antidomain(antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f3477,f50]) ).
fof(f3493,plain,
! [X0,X1] : addition(antidomain(X0),multiplication(antidomain(antidomain(X1)),antidomain(antidomain(X0)))) = addition(antidomain(antidomain(X1)),antidomain(X0)),
inference(superposition,[],[f3393,f335]) ).
fof(f3512,plain,
! [X0,X1] : multiplication(antidomain(antidomain(antidomain(X1))),multiplication(antidomain(antidomain(X0)),antidomain(X1))) = multiplication(antidomain(antidomain(antidomain(X1))),addition(antidomain(antidomain(X0)),antidomain(antidomain(X1)))),
inference(superposition,[],[f184,f3393]) ).
fof(f3525,plain,
! [X0,X1] : multiplication(antidomain(antidomain(antidomain(X1))),multiplication(antidomain(antidomain(X0)),antidomain(X1))) = multiplication(antidomain(antidomain(antidomain(X1))),antidomain(antidomain(X0))),
inference(forward_demodulation,[],[f3512,f181]) ).
fof(f3537,plain,
! [X0,X1] : multiplication(antidomain(X1),antidomain(antidomain(X0))) = multiplication(antidomain(X1),multiplication(antidomain(antidomain(X0)),antidomain(X1))),
inference(forward_demodulation,[],[f3525,f335]) ).
fof(f3551,plain,
! [X0] : multiplication(coantidomain(coantidomain(X0)),antidomain(coantidomain(X0))) = multiplication(one,antidomain(coantidomain(X0))),
inference(superposition,[],[f84,f3485]) ).
fof(f3575,plain,
! [X0] : antidomain(coantidomain(X0)) = multiplication(coantidomain(coantidomain(X0)),antidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f3551,f51]) ).
fof(f3605,plain,
! [X0] : multiplication(coantidomain(coantidomain(X0)),addition(one,antidomain(coantidomain(X0)))) = addition(coantidomain(coantidomain(X0)),antidomain(coantidomain(X0))),
inference(superposition,[],[f156,f3575]) ).
fof(f3621,plain,
! [X0] : multiplication(coantidomain(coantidomain(X0)),addition(one,antidomain(coantidomain(X0)))) = addition(antidomain(coantidomain(X0)),coantidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f3605,f37]) ).
fof(f3632,plain,
! [X0] : multiplication(coantidomain(coantidomain(X0)),one) = addition(antidomain(coantidomain(X0)),coantidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f3621,f1317]) ).
fof(f3638,plain,
! [X0] : coantidomain(coantidomain(X0)) = addition(antidomain(coantidomain(X0)),coantidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f3632,f52]) ).
fof(f3644,plain,
! [X0] : multiplication(coantidomain(X0),coantidomain(coantidomain(X0))) = multiplication(coantidomain(X0),antidomain(coantidomain(X0))),
inference(superposition,[],[f178,f3638]) ).
fof(f3665,plain,
! [X0] : zero = multiplication(coantidomain(X0),antidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f3644,f53]) ).
fof(f3682,plain,
! [X0] : multiplication(antidomain(zero),coantidomain(X0)) = multiplication(antidomain(zero),multiplication(coantidomain(X0),antidomain(antidomain(coantidomain(X0))))),
inference(superposition,[],[f496,f3665]) ).
fof(f3719,plain,
! [X0] : multiplication(one,coantidomain(X0)) = multiplication(one,multiplication(coantidomain(X0),antidomain(antidomain(coantidomain(X0))))),
inference(forward_demodulation,[],[f3682,f146]) ).
fof(f3733,plain,
! [X0] : multiplication(one,coantidomain(X0)) = multiplication(coantidomain(X0),antidomain(antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f3719,f51]) ).
fof(f3742,plain,
! [X0] : coantidomain(X0) = multiplication(coantidomain(X0),antidomain(antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f3733,f51]) ).
fof(f3757,plain,
! [X0,X1] : multiplication(coantidomain(X0),X1) = multiplication(coantidomain(X0),multiplication(antidomain(antidomain(coantidomain(X0))),X1)),
inference(superposition,[],[f45,f3742]) ).
fof(f3987,plain,
! [X0] : multiplication(antidomain(zero),X0) = multiplication(antidomain(zero),multiplication(coantidomain(coantidomain(coantidomain(antidomain(X0)))),X0)),
inference(superposition,[],[f232,f2451]) ).
fof(f3990,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,[],[f232,f2202]) ).
fof(f4063,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,[],[f3990,f146]) ).
fof(f4065,plain,
! [X0] : multiplication(antidomain(zero),X0) = multiplication(antidomain(zero),multiplication(coantidomain(antidomain(X0)),X0)),
inference(forward_demodulation,[],[f3987,f2235]) ).
fof(f4079,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,[],[f4063,f51]) ).
fof(f4080,plain,
! [X0] : multiplication(one,X0) = multiplication(one,multiplication(coantidomain(antidomain(X0)),X0)),
inference(forward_demodulation,[],[f4065,f146]) ).
fof(f4088,plain,
! [X0,X1] : multiplication(one,multiplication(X1,coantidomain(multiplication(X0,X1)))) = multiplication(coantidomain(X0),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f4079,f2235]) ).
fof(f4089,plain,
! [X0] : multiplication(one,X0) = multiplication(coantidomain(antidomain(X0)),X0),
inference(forward_demodulation,[],[f4080,f51]) ).
fof(f4091,plain,
! [X0,X1] : multiplication(X1,coantidomain(multiplication(X0,X1))) = multiplication(coantidomain(X0),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f4088,f51]) ).
fof(f4092,plain,
! [X0] : multiplication(coantidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f4089,f51]) ).
fof(f4122,plain,
! [X0] : multiplication(antidomain(multiplication(coantidomain(antidomain(antidomain(antidomain(X0)))),antidomain(X0))),coantidomain(antidomain(antidomain(antidomain(X0))))) = multiplication(antidomain(multiplication(coantidomain(antidomain(antidomain(antidomain(X0)))),antidomain(X0))),antidomain(antidomain(X0))),
inference(superposition,[],[f496,f4092]) ).
fof(f4124,plain,
! [X0] : multiplication(antidomain(zero),antidomain(antidomain(X0))) = multiplication(antidomain(zero),coantidomain(antidomain(antidomain(antidomain(X0))))),
inference(forward_demodulation,[],[f4122,f2737]) ).
fof(f4142,plain,
! [X0] : multiplication(antidomain(zero),antidomain(antidomain(X0))) = multiplication(antidomain(zero),coantidomain(antidomain(X0))),
inference(forward_demodulation,[],[f4124,f335]) ).
fof(f4147,plain,
! [X0] : multiplication(one,coantidomain(antidomain(X0))) = multiplication(one,antidomain(antidomain(X0))),
inference(forward_demodulation,[],[f4142,f146]) ).
fof(f4149,plain,
! [X0] : antidomain(antidomain(X0)) = multiplication(one,coantidomain(antidomain(X0))),
inference(forward_demodulation,[],[f4147,f51]) ).
fof(f4150,plain,
! [X0] : antidomain(antidomain(X0)) = coantidomain(antidomain(X0)),
inference(forward_demodulation,[],[f4149,f51]) ).
fof(f4154,plain,
antidomain(antidomain(sK2)) != addition(antidomain(antidomain(sK2)),coantidomain(coantidomain(multiplication(coantidomain(antidomain(antidomain(antidomain(sK1)))),sK0)))),
inference(superposition,[],[f66,f4150]) ).
fof(f4203,plain,
antidomain(antidomain(sK2)) != addition(antidomain(antidomain(sK2)),coantidomain(coantidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),sK0)))),
inference(forward_demodulation,[],[f4154,f4150]) ).
fof(f4213,plain,
antidomain(antidomain(sK2)) != addition(antidomain(antidomain(sK2)),coantidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0)))),
inference(forward_demodulation,[],[f4203,f335]) ).
fof(f4775,plain,
! [X2,X3,X0,X1] : addition(X1,multiplication(addition(X2,X0),antidomain(X3))) = addition(multiplication(X1,antidomain(antidomain(X3))),multiplication(addition(X0,addition(X1,X2)),antidomain(X3))),
inference(superposition,[],[f1616,f265]) ).
fof(f5354,plain,
! [X0,X1] : multiplication(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1)),one) = multiplication(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1)),coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1)))),
inference(superposition,[],[f178,f1069]) ).
fof(f5378,plain,
! [X0,X1] : zero = multiplication(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1)),one),
inference(forward_demodulation,[],[f5354,f53]) ).
fof(f5424,plain,
! [X0,X1] : zero = multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1)),
inference(forward_demodulation,[],[f5378,f52]) ).
fof(f6185,plain,
! [X2,X0,X1] : addition(addition(antidomain(antidomain(antidomain(X1))),X0),multiplication(X2,antidomain(X1))) = addition(multiplication(X0,antidomain(antidomain(X1))),multiplication(addition(addition(antidomain(antidomain(antidomain(X1))),X0),X2),antidomain(X1))),
inference(superposition,[],[f1616,f100]) ).
fof(f6192,plain,
! [X2,X0,X1] : addition(addition(antidomain(antidomain(antidomain(X1))),X0),multiplication(X2,antidomain(X1))) = addition(multiplication(X0,antidomain(antidomain(X1))),multiplication(addition(antidomain(antidomain(antidomain(X1))),addition(X0,X2)),antidomain(X1))),
inference(forward_demodulation,[],[f6185,f36]) ).
fof(f6228,plain,
! [X2,X0,X1] : addition(addition(antidomain(antidomain(antidomain(X1))),X0),multiplication(X2,antidomain(X1))) = addition(X0,multiplication(addition(X2,antidomain(antidomain(antidomain(X1)))),antidomain(X1))),
inference(forward_demodulation,[],[f6192,f4775]) ).
fof(f6242,plain,
! [X2,X0,X1] : addition(addition(antidomain(antidomain(antidomain(X1))),X0),multiplication(X2,antidomain(X1))) = addition(X0,multiplication(addition(one,X2),antidomain(X1))),
inference(forward_demodulation,[],[f6228,f310]) ).
fof(f6247,plain,
! [X2,X0,X1] : addition(X0,multiplication(addition(one,X2),antidomain(X1))) = addition(antidomain(antidomain(antidomain(X1))),addition(X0,multiplication(X2,antidomain(X1)))),
inference(forward_demodulation,[],[f6242,f36]) ).
fof(f6249,plain,
! [X2,X0,X1] : addition(X0,multiplication(addition(one,X2),antidomain(X1))) = addition(antidomain(X1),addition(X0,multiplication(X2,antidomain(X1)))),
inference(forward_demodulation,[],[f6247,f335]) ).
fof(f6514,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,[],[f84,f47]) ).
fof(f6535,plain,
! [X0,X1] : zero = multiplication(antidomain(multiplication(X0,X1)),multiplication(X0,antidomain(antidomain(X1)))),
inference(forward_demodulation,[],[f6514,f48]) ).
fof(f6714,plain,
! [X0,X1] : zero = multiplication(antidomain(zero),multiplication(antidomain(X0),antidomain(antidomain(multiplication(X0,X1))))),
inference(superposition,[],[f6535,f955]) ).
fof(f6739,plain,
! [X0] : zero = multiplication(antidomain(zero),multiplication(X0,antidomain(antidomain(coantidomain(X0))))),
inference(superposition,[],[f6535,f53]) ).
fof(f6848,plain,
! [X0] : zero = multiplication(one,multiplication(X0,antidomain(antidomain(coantidomain(X0))))),
inference(forward_demodulation,[],[f6739,f146]) ).
fof(f6861,plain,
! [X0,X1] : zero = multiplication(one,multiplication(antidomain(X0),antidomain(antidomain(multiplication(X0,X1))))),
inference(forward_demodulation,[],[f6714,f146]) ).
fof(f6898,plain,
! [X0] : zero = multiplication(X0,antidomain(antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f6848,f51]) ).
fof(f6909,plain,
! [X0,X1] : zero = multiplication(antidomain(X0),antidomain(antidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f6861,f51]) ).
fof(f6978,plain,
! [X0] : multiplication(antidomain(antidomain(coantidomain(X0))),coantidomain(zero)) = multiplication(coantidomain(X0),multiplication(antidomain(antidomain(coantidomain(X0))),coantidomain(zero))),
inference(superposition,[],[f4091,f6898]) ).
fof(f6993,plain,
! [X0] : multiplication(antidomain(zero),multiplication(coantidomain(coantidomain(X0)),antidomain(antidomain(coantidomain(coantidomain(X0)))))) = multiplication(antidomain(zero),antidomain(antidomain(coantidomain(coantidomain(X0))))),
inference(superposition,[],[f232,f6898]) ).
fof(f6994,plain,
! [X0] : multiplication(one,multiplication(coantidomain(coantidomain(X0)),antidomain(antidomain(coantidomain(coantidomain(X0)))))) = multiplication(one,antidomain(antidomain(coantidomain(coantidomain(X0))))),
inference(forward_demodulation,[],[f6993,f146]) ).
fof(f7008,plain,
! [X0] : multiplication(coantidomain(X0),coantidomain(zero)) = multiplication(antidomain(antidomain(coantidomain(X0))),coantidomain(zero)),
inference(forward_demodulation,[],[f6978,f3757]) ).
fof(f7036,plain,
! [X0] : antidomain(antidomain(coantidomain(coantidomain(X0)))) = multiplication(one,multiplication(coantidomain(coantidomain(X0)),antidomain(antidomain(coantidomain(coantidomain(X0)))))),
inference(forward_demodulation,[],[f6994,f51]) ).
fof(f7049,plain,
! [X0] : multiplication(coantidomain(X0),one) = multiplication(antidomain(antidomain(coantidomain(X0))),one),
inference(forward_demodulation,[],[f7008,f92]) ).
fof(f7065,plain,
! [X0] : antidomain(antidomain(coantidomain(coantidomain(X0)))) = multiplication(coantidomain(coantidomain(X0)),antidomain(antidomain(coantidomain(coantidomain(X0))))),
inference(forward_demodulation,[],[f7036,f51]) ).
fof(f7075,plain,
! [X0] : multiplication(coantidomain(X0),one) = antidomain(antidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f7049,f52]) ).
fof(f7085,plain,
! [X0] : coantidomain(coantidomain(X0)) = antidomain(antidomain(coantidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f7065,f3742]) ).
fof(f7091,plain,
! [X0] : coantidomain(X0) = antidomain(antidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f7075,f52]) ).
fof(f7122,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X1)),multiplication(coantidomain(X0),coantidomain(X1))) = addition(coantidomain(X0),coantidomain(coantidomain(X1))),
inference(superposition,[],[f3390,f7091]) ).
fof(f7127,plain,
! [X0,X1] : multiplication(antidomain(X1),coantidomain(X0)) = multiplication(antidomain(X1),multiplication(coantidomain(X0),antidomain(X1))),
inference(superposition,[],[f3537,f7091]) ).
fof(f7162,plain,
! [X0] : coantidomain(coantidomain(X0)) = antidomain(coantidomain(X0)),
inference(superposition,[],[f4150,f7091]) ).
fof(f7174,plain,
! [X0,X1] : addition(antidomain(coantidomain(X1)),multiplication(coantidomain(X0),coantidomain(X1))) = addition(coantidomain(X0),antidomain(coantidomain(X1))),
inference(forward_demodulation,[],[f7122,f7162]) ).
fof(f7217,plain,
antidomain(antidomain(sK2)) != addition(antidomain(antidomain(sK2)),antidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0)))),
inference(superposition,[],[f4213,f7162]) ).
fof(f7999,plain,
! [X0,X1] : multiplication(antidomain(zero),antidomain(X0)) = multiplication(antidomain(zero),multiplication(antidomain(X0),antidomain(antidomain(antidomain(multiplication(X0,X1)))))),
inference(superposition,[],[f496,f6909]) ).
fof(f8049,plain,
! [X0,X1] : multiplication(antidomain(zero),antidomain(X0)) = multiplication(antidomain(zero),multiplication(antidomain(X0),antidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f7999,f335]) ).
fof(f8104,plain,
! [X0,X1] : multiplication(one,antidomain(X0)) = multiplication(one,multiplication(antidomain(X0),antidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f8049,f146]) ).
fof(f8142,plain,
! [X0,X1] : multiplication(one,antidomain(X0)) = multiplication(antidomain(X0),antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f8104,f51]) ).
fof(f8154,plain,
! [X0,X1] : antidomain(X0) = multiplication(antidomain(X0),antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f8142,f51]) ).
fof(f8247,plain,
! [X0,X1] : multiplication(addition(one,antidomain(X0)),antidomain(multiplication(X0,X1))) = addition(antidomain(multiplication(X0,X1)),antidomain(X0)),
inference(superposition,[],[f73,f8154]) ).
fof(f8279,plain,
! [X0,X1] : multiplication(addition(one,antidomain(X0)),antidomain(multiplication(X0,X1))) = addition(antidomain(X0),antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f8247,f37]) ).
fof(f8324,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(multiplication(X0,X1))) = multiplication(one,antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f8279,f1317]) ).
fof(f8336,plain,
! [X0,X1] : antidomain(multiplication(X0,X1)) = addition(antidomain(X0),antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f8324,f51]) ).
fof(f8516,plain,
! [X0,X1] : antidomain(multiplication(antidomain(antidomain(X0)),X1)) = addition(antidomain(X0),antidomain(multiplication(antidomain(antidomain(X0)),X1))),
inference(superposition,[],[f8336,f335]) ).
fof(f8797,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X1)),multiplication(coantidomain(X1),antidomain(coantidomain(coantidomain(X0))))) = addition(antidomain(coantidomain(coantidomain(X0))),multiplication(coantidomain(coantidomain(X1)),coantidomain(coantidomain(X0)))),
inference(superposition,[],[f1810,f7085]) ).
fof(f8823,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(X1))) = addition(antidomain(X1),addition(coantidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(X1)))),
inference(superposition,[],[f248,f1810]) ).
fof(f8838,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(X1))) = addition(coantidomain(coantidomain(X0)),multiplication(addition(one,coantidomain(X0)),antidomain(X1))),
inference(forward_demodulation,[],[f8823,f6249]) ).
fof(f8864,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X1)),multiplication(coantidomain(X1),antidomain(coantidomain(coantidomain(X0))))) = addition(coantidomain(coantidomain(X1)),antidomain(coantidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f8797,f7174]) ).
fof(f8882,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(X1))) = multiplication(addition(one,coantidomain(X0)),addition(antidomain(X1),coantidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f8838,f2205]) ).
fof(f8899,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X1)),multiplication(coantidomain(X1),antidomain(antidomain(coantidomain(X0))))) = addition(coantidomain(coantidomain(X1)),antidomain(antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f8864,f7162]) ).
fof(f8909,plain,
! [X0,X1] : addition(antidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(X1))) = multiplication(addition(one,coantidomain(X0)),addition(antidomain(X1),antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f8882,f7162]) ).
fof(f8916,plain,
! [X0,X1] : addition(coantidomain(coantidomain(X1)),multiplication(coantidomain(X1),coantidomain(X0))) = addition(coantidomain(coantidomain(X1)),coantidomain(X0)),
inference(forward_demodulation,[],[f8899,f7091]) ).
fof(f8921,plain,
! [X0,X1] : addition(antidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(X1))) = multiplication(one,addition(antidomain(X1),antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f8909,f1408]) ).
fof(f8925,plain,
! [X0,X1] : addition(antidomain(coantidomain(X1)),multiplication(coantidomain(X1),coantidomain(X0))) = addition(antidomain(coantidomain(X1)),coantidomain(X0)),
inference(forward_demodulation,[],[f8916,f7162]) ).
fof(f8930,plain,
! [X0,X1] : addition(antidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(X1))) = addition(antidomain(X1),antidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f8921,f51]) ).
fof(f8943,plain,
! [X0,X1] : addition(antidomain(coantidomain(coantidomain(multiplication(X0,X1)))),coantidomain(X1)) = addition(antidomain(coantidomain(coantidomain(multiplication(X0,X1)))),zero),
inference(superposition,[],[f8925,f5424]) ).
fof(f8974,plain,
! [X0,X1] : antidomain(coantidomain(coantidomain(multiplication(X0,X1)))) = addition(antidomain(coantidomain(coantidomain(multiplication(X0,X1)))),coantidomain(X1)),
inference(forward_demodulation,[],[f8943,f56]) ).
fof(f8985,plain,
! [X0,X1] : antidomain(coantidomain(coantidomain(multiplication(X0,X1)))) = addition(coantidomain(X1),antidomain(coantidomain(coantidomain(multiplication(X0,X1))))),
inference(forward_demodulation,[],[f8974,f37]) ).
fof(f8992,plain,
! [X0,X1] : antidomain(antidomain(coantidomain(multiplication(X0,X1)))) = addition(coantidomain(X1),antidomain(antidomain(coantidomain(multiplication(X0,X1))))),
inference(forward_demodulation,[],[f8985,f7162]) ).
fof(f8998,plain,
! [X0,X1] : coantidomain(multiplication(X0,X1)) = addition(coantidomain(X1),coantidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f8992,f7091]) ).
fof(f9042,plain,
! [X0,X1] : coantidomain(antidomain(X0)) = addition(coantidomain(antidomain(multiplication(X0,X1))),coantidomain(antidomain(X0))),
inference(superposition,[],[f8998,f8154]) ).
fof(f9110,plain,
! [X0,X1] : coantidomain(antidomain(X0)) = addition(coantidomain(antidomain(X0)),coantidomain(antidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f9042,f37]) ).
fof(f9145,plain,
! [X0,X1] : coantidomain(antidomain(X0)) = addition(coantidomain(antidomain(X0)),antidomain(antidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f9110,f4150]) ).
fof(f9171,plain,
! [X0,X1] : antidomain(antidomain(X0)) = addition(antidomain(antidomain(X0)),antidomain(antidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f9145,f4150]) ).
fof(f11063,plain,
! [X0,X1] : addition(multiplication(coantidomain(coantidomain(X0)),one),antidomain(X1)) = addition(multiplication(coantidomain(X0),antidomain(X1)),multiplication(coantidomain(coantidomain(X0)),one)),
inference(superposition,[],[f1639,f1317]) ).
fof(f11103,plain,
! [X0,X1] : addition(multiplication(coantidomain(coantidomain(antidomain(addition(X0,X1)))),X0),X1) = addition(multiplication(coantidomain(antidomain(addition(X0,X1))),X1),zero),
inference(superposition,[],[f1639,f2451]) ).
fof(f11134,plain,
! [X0,X1] : multiplication(coantidomain(antidomain(addition(X0,X1))),X1) = addition(multiplication(coantidomain(coantidomain(antidomain(addition(X0,X1)))),X0),X1),
inference(forward_demodulation,[],[f11103,f56]) ).
fof(f11174,plain,
! [X0,X1] : addition(multiplication(coantidomain(X0),antidomain(X1)),coantidomain(coantidomain(X0))) = addition(coantidomain(coantidomain(X0)),antidomain(X1)),
inference(forward_demodulation,[],[f11063,f52]) ).
fof(f11232,plain,
! [X0,X1] : multiplication(coantidomain(antidomain(addition(X0,X1))),X1) = addition(X1,multiplication(coantidomain(coantidomain(antidomain(addition(X0,X1)))),X0)),
inference(forward_demodulation,[],[f11134,f37]) ).
fof(f11267,plain,
! [X0,X1] : addition(antidomain(coantidomain(X0)),antidomain(X1)) = addition(multiplication(coantidomain(X0),antidomain(X1)),antidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f11174,f7162]) ).
fof(f11302,plain,
! [X0,X1] : multiplication(coantidomain(antidomain(addition(X0,X1))),X1) = addition(X1,multiplication(antidomain(coantidomain(antidomain(addition(X0,X1)))),X0)),
inference(forward_demodulation,[],[f11232,f7162]) ).
fof(f11331,plain,
! [X0,X1] : addition(antidomain(coantidomain(X0)),antidomain(X1)) = addition(antidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(X1))),
inference(forward_demodulation,[],[f11267,f37]) ).
fof(f11350,plain,
! [X0,X1] : multiplication(antidomain(antidomain(addition(X0,X1))),X1) = addition(X1,multiplication(antidomain(antidomain(antidomain(addition(X0,X1)))),X0)),
inference(forward_demodulation,[],[f11302,f4150]) ).
fof(f11381,plain,
! [X0,X1] : multiplication(antidomain(antidomain(addition(X0,X1))),X1) = addition(X1,multiplication(antidomain(addition(X0,X1)),X0)),
inference(forward_demodulation,[],[f11350,f335]) ).
fof(f11400,plain,
! [X0,X1] : addition(X1,zero) = multiplication(antidomain(antidomain(addition(X0,X1))),X1),
inference(forward_demodulation,[],[f11381,f444]) ).
fof(f11411,plain,
! [X0,X1] : multiplication(antidomain(antidomain(addition(X0,X1))),X1) = X1,
inference(forward_demodulation,[],[f11400,f56]) ).
fof(f12161,plain,
addition(antidomain(sK1),multiplication(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))),antidomain(antidomain(sK1)))) = addition(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))),antidomain(antidomain(multiplication(sK0,antidomain(sK2))))),
inference(superposition,[],[f1811,f2659]) ).
fof(f12191,plain,
! [X0,X1] : multiplication(multiplication(antidomain(X1),antidomain(X0)),antidomain(X1)) = multiplication(addition(antidomain(X0),multiplication(antidomain(antidomain(X1)),antidomain(antidomain(X0)))),antidomain(X1)),
inference(superposition,[],[f100,f1811]) ).
fof(f12265,plain,
! [X0,X1] : multiplication(multiplication(antidomain(X1),antidomain(X0)),antidomain(X1)) = multiplication(addition(antidomain(antidomain(X1)),antidomain(X0)),antidomain(X1)),
inference(forward_demodulation,[],[f12191,f3493]) ).
fof(f12285,plain,
one = addition(antidomain(sK1),multiplication(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))),antidomain(antidomain(sK1)))),
inference(forward_demodulation,[],[f12161,f46]) ).
fof(f12310,plain,
! [X0,X1] : multiplication(multiplication(antidomain(X1),antidomain(X0)),antidomain(X1)) = addition(zero,multiplication(antidomain(X0),antidomain(X1))),
inference(forward_demodulation,[],[f12265,f74]) ).
fof(f12322,plain,
one = addition(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))),antidomain(sK1)),
inference(forward_demodulation,[],[f12285,f3493]) ).
fof(f12334,plain,
! [X0,X1] : multiplication(antidomain(X0),antidomain(X1)) = multiplication(multiplication(antidomain(X1),antidomain(X0)),antidomain(X1)),
inference(forward_demodulation,[],[f12310,f152]) ).
fof(f12342,plain,
one = addition(antidomain(sK1),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2)))))),
inference(forward_demodulation,[],[f12322,f37]) ).
fof(f12347,plain,
! [X0,X1] : multiplication(antidomain(X0),antidomain(X1)) = multiplication(antidomain(X1),multiplication(antidomain(X0),antidomain(X1))),
inference(forward_demodulation,[],[f12334,f45]) ).
fof(f12354,plain,
one = addition(antidomain(sK1),antidomain(multiplication(sK0,antidomain(sK2)))),
inference(forward_demodulation,[],[f12342,f335]) ).
fof(f12376,plain,
! [X0] : addition(multiplication(antidomain(antidomain(X0)),antidomain(sK1)),antidomain(multiplication(sK0,antidomain(sK2)))) = addition(multiplication(antidomain(X0),antidomain(multiplication(sK0,antidomain(sK2)))),multiplication(antidomain(antidomain(X0)),one)),
inference(superposition,[],[f1640,f12354]) ).
fof(f12379,plain,
! [X0] : addition(multiplication(antidomain(antidomain(X0)),antidomain(sK1)),antidomain(multiplication(sK0,antidomain(sK2)))) = addition(multiplication(antidomain(antidomain(X0)),one),multiplication(antidomain(X0),antidomain(multiplication(sK0,antidomain(sK2))))),
inference(forward_demodulation,[],[f12376,f37]) ).
fof(f12396,plain,
! [X0] : addition(multiplication(antidomain(antidomain(X0)),antidomain(sK1)),antidomain(multiplication(sK0,antidomain(sK2)))) = addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),antidomain(multiplication(sK0,antidomain(sK2))))),
inference(forward_demodulation,[],[f12379,f52]) ).
fof(f12401,plain,
! [X0] : addition(multiplication(antidomain(antidomain(X0)),antidomain(sK1)),antidomain(multiplication(sK0,antidomain(sK2)))) = addition(antidomain(antidomain(X0)),antidomain(multiplication(sK0,antidomain(sK2)))),
inference(forward_demodulation,[],[f12396,f3349]) ).
fof(f12405,plain,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(multiplication(sK0,antidomain(sK2)))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(antidomain(antidomain(X0)),antidomain(sK1))),
inference(forward_demodulation,[],[f12401,f37]) ).
fof(f12464,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(antidomain(X0),antidomain(sK1))) = addition(antidomain(X0),antidomain(multiplication(sK0,antidomain(sK2)))),
inference(superposition,[],[f12405,f335]) ).
fof(f13124,plain,
! [X0,X1] : multiplication(coantidomain(coantidomain(X0)),antidomain(X1)) = multiplication(antidomain(X1),multiplication(coantidomain(coantidomain(X0)),antidomain(X1))),
inference(superposition,[],[f12347,f7085]) ).
fof(f13210,plain,
! [X0,X1] : multiplication(coantidomain(coantidomain(X0)),antidomain(X1)) = multiplication(antidomain(X1),coantidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f13124,f7127]) ).
fof(f13222,plain,
! [X0,X1] : multiplication(antidomain(coantidomain(X0)),antidomain(X1)) = multiplication(antidomain(X1),antidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f13210,f7162]) ).
fof(f13237,plain,
! [X0,X1] : multiplication(coantidomain(X0),antidomain(coantidomain(X1))) = multiplication(antidomain(coantidomain(X1)),coantidomain(X0)),
inference(superposition,[],[f13222,f7091]) ).
fof(f13468,plain,
! [X0,X1] : multiplication(antidomain(antidomain(antidomain(X0))),coantidomain(X1)) = multiplication(coantidomain(X1),antidomain(antidomain(antidomain(X0)))),
inference(superposition,[],[f13237,f4150]) ).
fof(f13470,plain,
! [X0,X1] : multiplication(antidomain(antidomain(coantidomain(X0))),coantidomain(X1)) = multiplication(coantidomain(X1),antidomain(antidomain(coantidomain(X0)))),
inference(superposition,[],[f13237,f7162]) ).
fof(f13636,plain,
! [X0,X1] : multiplication(coantidomain(X0),coantidomain(X1)) = multiplication(coantidomain(X1),coantidomain(X0)),
inference(forward_demodulation,[],[f13470,f7091]) ).
fof(f13637,plain,
! [X0,X1] : multiplication(coantidomain(X1),antidomain(X0)) = multiplication(antidomain(X0),coantidomain(X1)),
inference(forward_demodulation,[],[f13468,f335]) ).
fof(f13797,plain,
! [X2,X0,X1] : multiplication(multiplication(coantidomain(X0),antidomain(X1)),X2) = multiplication(antidomain(X1),multiplication(coantidomain(X0),X2)),
inference(superposition,[],[f45,f13637]) ).
fof(f13849,plain,
! [X2,X0,X1] : multiplication(coantidomain(X0),multiplication(antidomain(X1),X2)) = multiplication(antidomain(X1),multiplication(coantidomain(X0),X2)),
inference(forward_demodulation,[],[f13797,f45]) ).
fof(f14018,plain,
! [X0,X1] : multiplication(antidomain(multiplication(coantidomain(X0),coantidomain(X1))),multiplication(coantidomain(X1),coantidomain(coantidomain(X0)))) = multiplication(antidomain(multiplication(coantidomain(X0),coantidomain(X1))),coantidomain(X1)),
inference(superposition,[],[f495,f13636]) ).
fof(f14049,plain,
! [X0,X1] : antidomain(multiplication(coantidomain(X0),coantidomain(X1))) = addition(antidomain(coantidomain(X1)),antidomain(multiplication(coantidomain(X0),coantidomain(X1)))),
inference(superposition,[],[f8336,f13636]) ).
fof(f14081,plain,
! [X0,X1] : multiplication(antidomain(multiplication(coantidomain(X0),coantidomain(X1))),multiplication(coantidomain(X1),coantidomain(coantidomain(X0)))) = multiplication(coantidomain(X1),antidomain(multiplication(coantidomain(X0),coantidomain(X1)))),
inference(forward_demodulation,[],[f14018,f13637]) ).
fof(f14145,plain,
! [X0,X1] : multiplication(coantidomain(X1),antidomain(multiplication(coantidomain(X0),coantidomain(X1)))) = multiplication(coantidomain(X1),multiplication(antidomain(multiplication(coantidomain(X0),coantidomain(X1))),coantidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f14081,f13849]) ).
fof(f14171,plain,
! [X0,X1] : multiplication(coantidomain(X1),antidomain(multiplication(coantidomain(X0),coantidomain(X1)))) = multiplication(coantidomain(X1),multiplication(coantidomain(coantidomain(X0)),antidomain(multiplication(coantidomain(X0),coantidomain(X1))))),
inference(forward_demodulation,[],[f14145,f13637]) ).
fof(f14190,plain,
! [X0,X1] : multiplication(coantidomain(X1),antidomain(multiplication(coantidomain(X0),coantidomain(X1)))) = multiplication(coantidomain(X1),multiplication(antidomain(coantidomain(X0)),antidomain(multiplication(coantidomain(X0),coantidomain(X1))))),
inference(forward_demodulation,[],[f14171,f7162]) ).
fof(f14198,plain,
! [X0,X1] : multiplication(coantidomain(X1),antidomain(coantidomain(X0))) = multiplication(coantidomain(X1),antidomain(multiplication(coantidomain(X0),coantidomain(X1)))),
inference(forward_demodulation,[],[f14190,f8154]) ).
fof(f14224,plain,
! [X0,X1] : addition(antidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(coantidomain(X1)))) = addition(antidomain(coantidomain(X0)),antidomain(multiplication(coantidomain(X1),coantidomain(X0)))),
inference(superposition,[],[f11331,f14198]) ).
fof(f14296,plain,
! [X0,X1] : addition(antidomain(coantidomain(X0)),multiplication(coantidomain(X0),antidomain(coantidomain(X1)))) = antidomain(multiplication(coantidomain(X1),coantidomain(X0))),
inference(forward_demodulation,[],[f14224,f14049]) ).
fof(f14326,plain,
! [X0,X1] : addition(antidomain(coantidomain(X1)),antidomain(coantidomain(X0))) = antidomain(multiplication(coantidomain(X1),coantidomain(X0))),
inference(forward_demodulation,[],[f14296,f8930]) ).
fof(f14372,plain,
! [X0,X1] : addition(antidomain(coantidomain(X1)),antidomain(antidomain(antidomain(X0)))) = antidomain(multiplication(coantidomain(X1),antidomain(antidomain(X0)))),
inference(superposition,[],[f14326,f4150]) ).
fof(f14386,plain,
! [X0,X1] : addition(antidomain(coantidomain(X1)),antidomain(coantidomain(X0))) = antidomain(multiplication(coantidomain(X0),coantidomain(X1))),
inference(superposition,[],[f37,f14326]) ).
fof(f14413,plain,
! [X0,X1] : addition(antidomain(coantidomain(X1)),antidomain(X0)) = antidomain(multiplication(coantidomain(X1),antidomain(antidomain(X0)))),
inference(forward_demodulation,[],[f14372,f335]) ).
fof(f14441,plain,
! [X0,X1] : antidomain(multiplication(antidomain(antidomain(X0)),coantidomain(X1))) = addition(antidomain(coantidomain(X1)),antidomain(antidomain(antidomain(X0)))),
inference(superposition,[],[f14386,f4150]) ).
fof(f14485,plain,
! [X0,X1] : antidomain(multiplication(antidomain(antidomain(X0)),coantidomain(X1))) = addition(antidomain(coantidomain(X1)),antidomain(X0)),
inference(forward_demodulation,[],[f14441,f335]) ).
fof(f14514,plain,
! [X0,X1] : addition(antidomain(coantidomain(X1)),antidomain(antidomain(X0))) = antidomain(multiplication(antidomain(X0),coantidomain(X1))),
inference(superposition,[],[f14485,f335]) ).
fof(f14519,plain,
! [X0,X1] : addition(antidomain(antidomain(antidomain(X0))),antidomain(X1)) = antidomain(multiplication(antidomain(antidomain(X1)),antidomain(antidomain(X0)))),
inference(superposition,[],[f14485,f4150]) ).
fof(f14645,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(X1)) = antidomain(multiplication(antidomain(antidomain(X1)),antidomain(antidomain(X0)))),
inference(forward_demodulation,[],[f14519,f335]) ).
fof(f14914,plain,
! [X0,X1] : addition(antidomain(antidomain(antidomain(X0))),antidomain(antidomain(X1))) = antidomain(multiplication(antidomain(X1),antidomain(antidomain(X0)))),
inference(superposition,[],[f14514,f4150]) ).
fof(f14967,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(antidomain(X1))) = antidomain(multiplication(antidomain(X1),antidomain(antidomain(X0)))),
inference(forward_demodulation,[],[f14914,f335]) ).
fof(f16833,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),antidomain(X1)) = antidomain(multiplication(antidomain(antidomain(X1)),antidomain(X0))),
inference(superposition,[],[f14645,f335]) ).
fof(f17079,plain,
! [X0,X1] : addition(antidomain(antidomain(X1)),antidomain(antidomain(X0))) = antidomain(multiplication(antidomain(X0),antidomain(X1))),
inference(superposition,[],[f16833,f335]) ).
fof(f17391,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),antidomain(antidomain(X1))) = antidomain(multiplication(antidomain(X0),antidomain(X1))),
inference(superposition,[],[f37,f17079]) ).
fof(f17469,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(antidomain(X1))) = antidomain(multiplication(antidomain(antidomain(X0)),antidomain(X1))),
inference(superposition,[],[f17391,f335]) ).
fof(f17501,plain,
! [X0,X1] : antidomain(multiplication(antidomain(X1),antidomain(X0))) = antidomain(multiplication(antidomain(X0),antidomain(X1))),
inference(superposition,[],[f17079,f17391]) ).
fof(f18334,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(antidomain(antidomain(X1)))) = addition(antidomain(multiplication(antidomain(antidomain(X0)),X1)),addition(antidomain(X0),antidomain(antidomain(antidomain(X1))))),
inference(superposition,[],[f47,f17469]) ).
fof(f18462,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(antidomain(antidomain(X1)))) = addition(antidomain(antidomain(antidomain(X1))),addition(antidomain(multiplication(antidomain(antidomain(X0)),X1)),antidomain(X0))),
inference(forward_demodulation,[],[f18334,f265]) ).
fof(f18522,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(antidomain(antidomain(X1)))) = addition(antidomain(antidomain(antidomain(X1))),addition(antidomain(X0),antidomain(multiplication(antidomain(antidomain(X0)),X1)))),
inference(forward_demodulation,[],[f18462,f37]) ).
fof(f18555,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(antidomain(antidomain(X1)))) = addition(antidomain(antidomain(antidomain(X1))),antidomain(multiplication(antidomain(antidomain(X0)),X1))),
inference(forward_demodulation,[],[f18522,f8516]) ).
fof(f18571,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(X1)) = addition(antidomain(X1),antidomain(multiplication(antidomain(antidomain(X0)),X1))),
inference(forward_demodulation,[],[f18555,f335]) ).
fof(f18621,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),antidomain(X1)) = addition(antidomain(X1),antidomain(multiplication(antidomain(X0),X1))),
inference(superposition,[],[f18571,f335]) ).
fof(f18664,plain,
! [X0,X1] : multiplication(antidomain(multiplication(antidomain(antidomain(X0)),X1)),X1) = multiplication(addition(antidomain(X0),antidomain(X1)),X1),
inference(superposition,[],[f100,f18571]) ).
fof(f18693,plain,
! [X0,X1] : multiplication(antidomain(X0),X1) = multiplication(antidomain(multiplication(antidomain(antidomain(X0)),X1)),X1),
inference(forward_demodulation,[],[f18664,f84]) ).
fof(f18899,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),antidomain(multiplication(X0,X1))) = addition(antidomain(multiplication(X0,X1)),antidomain(zero)),
inference(superposition,[],[f18621,f955]) ).
fof(f19018,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),antidomain(multiplication(X0,X1))) = addition(antidomain(zero),antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f18899,f37]) ).
fof(f19078,plain,
! [X0,X1] : addition(one,antidomain(multiplication(X0,X1))) = addition(antidomain(antidomain(X0)),antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f19018,f146]) ).
fof(f19124,plain,
! [X0,X1] : one = addition(antidomain(antidomain(X0)),antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f19078,f1317]) ).
fof(f20376,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(antidomain(X0),antidomain(sK1))) = addition(antidomain(multiplication(antidomain(antidomain(X0)),antidomain(sK1))),antidomain(multiplication(sK0,antidomain(sK2)))),
inference(superposition,[],[f12464,f18693]) ).
fof(f20461,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(antidomain(X0),antidomain(sK1))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(multiplication(antidomain(antidomain(X0)),antidomain(sK1)))),
inference(forward_demodulation,[],[f20376,f37]) ).
fof(f20532,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(antidomain(X0),antidomain(sK1))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(multiplication(antidomain(sK1),antidomain(antidomain(X0))))),
inference(forward_demodulation,[],[f20461,f17501]) ).
fof(f20578,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(antidomain(X0),antidomain(sK1))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),addition(antidomain(X0),antidomain(antidomain(sK1)))),
inference(forward_demodulation,[],[f20532,f14967]) ).
fof(f20604,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(antidomain(X0),antidomain(sK1))) = addition(antidomain(antidomain(sK1)),addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(X0))),
inference(forward_demodulation,[],[f20578,f265]) ).
fof(f20616,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(antidomain(X0),antidomain(sK1))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(X0)),
inference(forward_demodulation,[],[f20604,f391]) ).
fof(f20645,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(coantidomain(X0),antidomain(sK1))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),coantidomain(X0)),
inference(superposition,[],[f20616,f7091]) ).
fof(f20698,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),coantidomain(X0)) = addition(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(antidomain(sK1),coantidomain(X0))),
inference(forward_demodulation,[],[f20645,f13637]) ).
fof(f20730,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(antidomain(X0))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(antidomain(sK1),antidomain(antidomain(X0)))),
inference(superposition,[],[f20698,f4150]) ).
fof(f23425,plain,
! [X0] : addition(antidomain(multiplication(sK0,antidomain(sK2))),zero) = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(antidomain(multiplication(sK1,X0)))),
inference(superposition,[],[f20730,f6909]) ).
fof(f23459,plain,
! [X0] : antidomain(multiplication(sK0,antidomain(sK2))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(antidomain(multiplication(sK1,X0)))),
inference(forward_demodulation,[],[f23425,f56]) ).
fof(f23503,plain,
! [X0] : antidomain(antidomain(multiplication(sK1,X0))) = multiplication(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))),antidomain(antidomain(multiplication(sK1,X0)))),
inference(superposition,[],[f11411,f23459]) ).
fof(f23504,plain,
! [X0] : antidomain(antidomain(multiplication(sK1,X0))) = multiplication(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(antidomain(multiplication(sK1,X0)))),
inference(forward_demodulation,[],[f23503,f335]) ).
fof(f23598,plain,
! [X0] : one = addition(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))),antidomain(antidomain(antidomain(multiplication(sK1,X0))))),
inference(superposition,[],[f19124,f23504]) ).
fof(f23599,plain,
! [X0] : one = antidomain(multiplication(antidomain(antidomain(multiplication(sK1,X0))),antidomain(antidomain(multiplication(sK0,antidomain(sK2)))))),
inference(forward_demodulation,[],[f23598,f17079]) ).
fof(f23632,plain,
! [X0] : one = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(antidomain(antidomain(multiplication(sK1,X0))))),
inference(forward_demodulation,[],[f23599,f14967]) ).
fof(f23654,plain,
! [X0] : one = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(multiplication(sK1,X0))),
inference(forward_demodulation,[],[f23632,f335]) ).
fof(f23827,plain,
! [X0,X1] : addition(multiplication(antidomain(antidomain(X0)),antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(multiplication(sK1,X1))) = addition(multiplication(antidomain(X0),antidomain(multiplication(sK1,X1))),multiplication(antidomain(antidomain(X0)),one)),
inference(superposition,[],[f1640,f23654]) ).
fof(f23830,plain,
! [X0,X1] : addition(multiplication(antidomain(antidomain(X0)),antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(multiplication(sK1,X1))) = addition(multiplication(antidomain(antidomain(X0)),one),multiplication(antidomain(X0),antidomain(multiplication(sK1,X1)))),
inference(forward_demodulation,[],[f23827,f37]) ).
fof(f23856,plain,
! [X0,X1] : addition(multiplication(antidomain(antidomain(X0)),antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(multiplication(sK1,X1))) = addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),antidomain(multiplication(sK1,X1)))),
inference(forward_demodulation,[],[f23830,f52]) ).
fof(f23867,plain,
! [X0,X1] : addition(multiplication(antidomain(antidomain(X0)),antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(multiplication(sK1,X1))) = addition(antidomain(antidomain(X0)),antidomain(multiplication(sK1,X1))),
inference(forward_demodulation,[],[f23856,f3349]) ).
fof(f24371,plain,
! [X0,X1] : addition(multiplication(coantidomain(X0),antidomain(multiplication(sK0,antidomain(sK2)))),antidomain(multiplication(sK1,X1))) = addition(coantidomain(X0),antidomain(multiplication(sK1,X1))),
inference(superposition,[],[f23867,f7091]) ).
fof(f24618,plain,
! [X0,X1] : addition(coantidomain(X0),antidomain(multiplication(sK1,X1))) = addition(multiplication(antidomain(multiplication(sK0,antidomain(sK2))),coantidomain(X0)),antidomain(multiplication(sK1,X1))),
inference(superposition,[],[f24371,f13637]) ).
fof(f24938,plain,
! [X0,X1] : multiplication(addition(coantidomain(X0),antidomain(multiplication(sK1,X1))),coantidomain(antidomain(multiplication(sK1,X1)))) = multiplication(multiplication(antidomain(multiplication(sK0,antidomain(sK2))),coantidomain(X0)),coantidomain(antidomain(multiplication(sK1,X1)))),
inference(superposition,[],[f83,f24618]) ).
fof(f24962,plain,
! [X0,X1] : multiplication(addition(coantidomain(X0),antidomain(multiplication(sK1,X1))),coantidomain(antidomain(multiplication(sK1,X1)))) = multiplication(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(coantidomain(X0),coantidomain(antidomain(multiplication(sK1,X1))))),
inference(forward_demodulation,[],[f24938,f45]) ).
fof(f24981,plain,
! [X0,X1] : multiplication(addition(coantidomain(X0),antidomain(multiplication(sK1,X1))),antidomain(antidomain(multiplication(sK1,X1)))) = multiplication(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(coantidomain(X0),antidomain(antidomain(multiplication(sK1,X1))))),
inference(forward_demodulation,[],[f24962,f4150]) ).
fof(f24995,plain,
! [X0,X1] : multiplication(coantidomain(X0),antidomain(antidomain(multiplication(sK1,X1)))) = multiplication(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(coantidomain(X0),antidomain(antidomain(multiplication(sK1,X1))))),
inference(forward_demodulation,[],[f24981,f352]) ).
fof(f26966,plain,
! [X0] : multiplication(coantidomain(X0),antidomain(antidomain(sK1))) = multiplication(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(coantidomain(X0),antidomain(antidomain(sK1)))),
inference(superposition,[],[f24995,f2192]) ).
fof(f27227,plain,
! [X0] : antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))) = addition(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))),antidomain(antidomain(multiplication(coantidomain(X0),antidomain(antidomain(sK1)))))),
inference(superposition,[],[f9171,f26966]) ).
fof(f27234,plain,
! [X0] : antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))) = antidomain(multiplication(antidomain(multiplication(coantidomain(X0),antidomain(antidomain(sK1)))),antidomain(antidomain(multiplication(sK0,antidomain(sK2)))))),
inference(forward_demodulation,[],[f27227,f17079]) ).
fof(f27266,plain,
! [X0] : antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(antidomain(multiplication(coantidomain(X0),antidomain(antidomain(sK1)))))),
inference(forward_demodulation,[],[f27234,f14967]) ).
fof(f27285,plain,
! [X0] : antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(addition(antidomain(coantidomain(X0)),antidomain(sK1)))),
inference(forward_demodulation,[],[f27266,f14413]) ).
fof(f27298,plain,
! [X0] : antidomain(antidomain(antidomain(multiplication(sK0,antidomain(sK2))))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(addition(antidomain(sK1),antidomain(coantidomain(X0))))),
inference(forward_demodulation,[],[f27285,f37]) ).
fof(f27306,plain,
! [X0] : antidomain(multiplication(sK0,antidomain(sK2))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(addition(antidomain(sK1),antidomain(coantidomain(X0))))),
inference(forward_demodulation,[],[f27298,f335]) ).
fof(f27322,plain,
! [X0] : antidomain(multiplication(sK0,antidomain(sK2))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(addition(antidomain(sK1),antidomain(antidomain(antidomain(X0)))))),
inference(superposition,[],[f27306,f4150]) ).
fof(f27352,plain,
! [X0] : antidomain(multiplication(sK0,antidomain(sK2))) = addition(antidomain(multiplication(sK0,antidomain(sK2))),antidomain(addition(antidomain(sK1),antidomain(X0)))),
inference(forward_demodulation,[],[f27322,f335]) ).
fof(f27405,plain,
! [X0] : multiplication(antidomain(multiplication(sK0,antidomain(sK2))),multiplication(sK0,antidomain(sK2))) = multiplication(antidomain(addition(antidomain(sK1),antidomain(X0))),multiplication(sK0,antidomain(sK2))),
inference(superposition,[],[f100,f27352]) ).
fof(f27427,plain,
! [X0] : zero = multiplication(antidomain(addition(antidomain(sK1),antidomain(X0))),multiplication(sK0,antidomain(sK2))),
inference(forward_demodulation,[],[f27405,f48]) ).
fof(f28556,plain,
! [X0] : coantidomain(multiplication(coantidomain(coantidomain(multiplication(antidomain(addition(antidomain(sK1),antidomain(X0))),sK0))),antidomain(sK2))) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(multiplication(antidomain(addition(antidomain(sK1),antidomain(X0))),sK0))),antidomain(sK2)))),
inference(superposition,[],[f927,f27427]) ).
fof(f28630,plain,
! [X0] : coantidomain(multiplication(antidomain(sK2),coantidomain(coantidomain(multiplication(antidomain(addition(antidomain(sK1),antidomain(X0))),sK0))))) = addition(coantidomain(zero),coantidomain(multiplication(antidomain(sK2),coantidomain(coantidomain(multiplication(antidomain(addition(antidomain(sK1),antidomain(X0))),sK0)))))),
inference(forward_demodulation,[],[f28556,f13637]) ).
fof(f28669,plain,
! [X0] : coantidomain(multiplication(antidomain(sK2),antidomain(coantidomain(multiplication(antidomain(addition(antidomain(sK1),antidomain(X0))),sK0))))) = addition(coantidomain(zero),coantidomain(multiplication(antidomain(sK2),antidomain(coantidomain(multiplication(antidomain(addition(antidomain(sK1),antidomain(X0))),sK0)))))),
inference(forward_demodulation,[],[f28630,f7162]) ).
fof(f28697,plain,
! [X0] : coantidomain(multiplication(antidomain(sK2),antidomain(coantidomain(multiplication(antidomain(addition(antidomain(sK1),antidomain(X0))),sK0))))) = addition(one,coantidomain(multiplication(antidomain(sK2),antidomain(coantidomain(multiplication(antidomain(addition(antidomain(sK1),antidomain(X0))),sK0)))))),
inference(forward_demodulation,[],[f28669,f92]) ).
fof(f28716,plain,
! [X0] : one = coantidomain(multiplication(antidomain(sK2),antidomain(coantidomain(multiplication(antidomain(addition(antidomain(sK1),antidomain(X0))),sK0))))),
inference(forward_demodulation,[],[f28697,f1408]) ).
fof(f28778,plain,
one = coantidomain(multiplication(antidomain(sK2),antidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0))))),
inference(superposition,[],[f28716,f35]) ).
fof(f29283,plain,
zero = multiplication(multiplication(antidomain(sK2),antidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0)))),one),
inference(superposition,[],[f53,f28778]) ).
fof(f29519,plain,
zero = multiplication(antidomain(sK2),antidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0)))),
inference(forward_demodulation,[],[f29283,f52]) ).
fof(f29729,plain,
multiplication(antidomain(zero),multiplication(antidomain(sK2),antidomain(antidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0)))))) = multiplication(antidomain(zero),antidomain(sK2)),
inference(superposition,[],[f496,f29519]) ).
fof(f29803,plain,
multiplication(one,multiplication(antidomain(sK2),antidomain(antidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0)))))) = multiplication(one,antidomain(sK2)),
inference(forward_demodulation,[],[f29729,f146]) ).
fof(f29837,plain,
antidomain(sK2) = multiplication(one,multiplication(antidomain(sK2),antidomain(antidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0)))))),
inference(forward_demodulation,[],[f29803,f51]) ).
fof(f29865,plain,
antidomain(sK2) = multiplication(antidomain(sK2),antidomain(antidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0))))),
inference(forward_demodulation,[],[f29837,f51]) ).
fof(f29886,plain,
antidomain(sK2) = multiplication(antidomain(sK2),coantidomain(multiplication(antidomain(antidomain(sK1)),sK0))),
inference(forward_demodulation,[],[f29865,f7091]) ).
fof(f29968,plain,
coantidomain(antidomain(sK2)) = addition(coantidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0))),coantidomain(antidomain(sK2))),
inference(superposition,[],[f8998,f29886]) ).
fof(f29981,plain,
coantidomain(antidomain(sK2)) = addition(coantidomain(antidomain(sK2)),coantidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0)))),
inference(forward_demodulation,[],[f29968,f37]) ).
fof(f30006,plain,
coantidomain(antidomain(sK2)) = addition(coantidomain(antidomain(sK2)),antidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0)))),
inference(forward_demodulation,[],[f29981,f7162]) ).
fof(f30023,plain,
antidomain(antidomain(sK2)) = addition(antidomain(antidomain(sK2)),antidomain(coantidomain(multiplication(antidomain(antidomain(sK1)),sK0)))),
inference(forward_demodulation,[],[f30006,f4150]) ).
fof(f30032,plain,
$false,
inference(forward_subsumption_resolution,[],[f30023,f7217]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : KLE108+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.48 % Computer : n013.cluster.edu
% 0.22/0.48 % Model : x86_64 x86_64
% 0.22/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.48 % Memory : 8046.5625MB
% 0.22/0.48 % OS : Linux 6.8.0-71-generic
% 0.22/0.48 % CPULimit : 300
% 0.22/0.48 % WCLimit : 300
% 0.22/0.48 % DateTime : Sun Sep 27 13:09:51 UTC 2026
% 0.22/0.49 % CPUTime :
% 0.22/0.49 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.27/0.55 Running first-order theorem proving
% 0.27/0.55 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
% 22.40/4.42 % (216587)Detected formulas, will run a generic FOF schedule.
% 22.40/4.42 % (216596)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1063353303:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 22.40/4.42 % (216596)Instruction limit reached!
% 22.40/4.42 % (216596)------------------------------
% 22.40/4.42 % (216596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.40/4.42 % (216596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/4.42 % (216596)CaDiCaL version: 2.1.3
% 22.40/4.42 % (216596)Termination reason: Instruction limit
% 22.40/4.42 % (216596)Termination phase: Saturation
% 22.40/4.42 % (216596)Time elapsed: 0.051 s
% 22.40/4.42 % (216596)Peak memory usage: 88 MB
% 22.40/4.42 % (216596)Instructions burned: 120 (million)
% 22.40/4.42 % (216593)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=243742929:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 22.40/4.42 % (216592)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=787854297:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 22.40/4.42 % (216595)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=478635811:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 22.40/4.42 % (216594)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=3696790356:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 22.40/4.42 % (216598)dis-21_1_sil=8000:lcm=predicate:random_seed=2856277960: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)
% 22.40/4.42 % (216597)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=790621083:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 22.40/4.42 % (216598)Refutation not found, incomplete strategy
% 22.40/4.42 % (216598)------------------------------
% 22.40/4.42 % (216598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.40/4.42 % (216598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/4.42 % (216598)CaDiCaL version: 2.1.3
% 22.40/4.42 % (216598)Termination reason: Refutation not found, incomplete strategy
% 22.40/4.42 % (216598)Time elapsed: 0.003 s
% 22.40/4.42 % (216598)Peak memory usage: 88 MB
% 22.40/4.42 % (216598)Instructions burned: 1 (million)
% 22.40/4.42 % (216595)Instruction limit reached!
% 22.40/4.42 % (216595)------------------------------
% 22.40/4.42 % (216595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.40/4.42 % (216595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/4.42 % (216595)CaDiCaL version: 2.1.3
% 22.40/4.42 % (216595)Termination reason: Instruction limit
% 22.40/4.42 % (216595)Termination phase: Saturation
% 22.40/4.42 % (216595)Time elapsed: 0.095 s
% 22.40/4.42 % (216595)Peak memory usage: 88 MB
% 22.40/4.42 % (216595)Instructions burned: 109 (million)
% 22.40/4.42 % (216597)Instruction limit reached!
% 22.40/4.42 % (216597)------------------------------
% 22.40/4.42 % (216597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.40/4.42 % (216597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/4.42 % (216597)CaDiCaL version: 2.1.3
% 22.40/4.42 % (216597)Termination reason: Instruction limit
% 22.40/4.42 % (216597)Termination phase: Saturation
% 22.40/4.42 % (216597)Time elapsed: 0.136 s
% 22.40/4.42 % (216597)Peak memory usage: 89 MB
% 22.40/4.42 % (216597)Instructions burned: 140 (million)
% 22.40/4.42 % (216602)lrs+10_1_sil=8000:sp=occurrence:random_seed=2938823916:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 22.40/4.42 % (216602)Instruction limit reached!
% 22.40/4.42 % (216602)------------------------------
% 22.40/4.42 % (216602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.40/4.42 % (216602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/4.42 % (216602)CaDiCaL version: 2.1.3
% 22.40/4.42 % (216602)Termination reason: Instruction limit
% 22.40/4.42 % (216602)Termination phase: Saturation
% 22.40/4.42 % (216602)Time elapsed: 0.144 s
% 22.40/4.42 % (216602)Peak memory usage: 92 MB
% 22.40/4.42 % (216602)Instructions burned: 286 (million)
% 22.40/4.42 % (216598)------------------------------
% 22.40/4.42 % (216598)------------------------------
% 30.99/5.69 % (216607)lrs+10_1_sil=32000:urr=on:br=off:random_seed=431339653:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 30.99/5.69 % (216617)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2855509509:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 30.99/5.69 % (216607)Instruction limit reached!
% 30.99/5.69 % (216607)------------------------------
% 30.99/5.69 % (216607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.69 % (216607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.69 % (216607)CaDiCaL version: 2.1.3
% 30.99/5.69 % (216607)Termination reason: Instruction limit
% 30.99/5.69 % (216607)Termination phase: Saturation
% 30.99/5.69 % (216607)Time elapsed: 0.163 s
% 30.99/5.69 % (216607)Peak memory usage: 89 MB
% 30.99/5.69 % (216607)Instructions burned: 157 (million)
% 30.99/5.69 % (216619)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=563223650:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 30.99/5.69 % (216619)Instruction limit reached!
% 30.99/5.69 % (216619)------------------------------
% 30.99/5.69 % (216619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.69 % (216619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.69 % (216619)CaDiCaL version: 2.1.3
% 30.99/5.69 % (216619)Termination reason: Instruction limit
% 30.99/5.69 % (216619)Termination phase: Saturation
% 30.99/5.69 % (216619)Time elapsed: 0.124 s
% 30.99/5.69 % (216619)Peak memory usage: 91 MB
% 30.99/5.69 % (216619)Instructions burned: 249 (million)
% 30.99/5.69 % (216621)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=477927752:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 30.99/5.69 % (216617)Instruction limit reached!
% 30.99/5.69 % (216617)------------------------------
% 30.99/5.69 % (216617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.69 % (216617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.69 % (216617)CaDiCaL version: 2.1.3
% 30.99/5.69 % (216617)Termination reason: Instruction limit
% 30.99/5.69 % (216617)Termination phase: Saturation
% 30.99/5.69 % (216617)Time elapsed: 0.323 s
% 30.99/5.69 % (216617)Peak memory usage: 92 MB
% 30.99/5.69 % (216617)Instructions burned: 325 (million)
% 30.99/5.69 % (216632)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=500687966:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 30.99/5.69 % (216621)Instruction limit reached!
% 30.99/5.69 % (216621)------------------------------
% 30.99/5.69 % (216621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.69 % (216621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.69 % (216621)CaDiCaL version: 2.1.3
% 30.99/5.69 % (216621)Termination reason: Instruction limit
% 30.99/5.69 % (216621)Termination phase: Saturation
% 30.99/5.69 % (216621)Time elapsed: 0.271 s
% 30.99/5.69 % (216621)Peak memory usage: 89 MB
% 30.99/5.69 % (216621)Instructions burned: 294 (million)
% 30.99/5.69 % (216634)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1172780109:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 30.99/5.69 % (216635)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1633156669:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 30.99/5.69 % (216635)Refutation not found, incomplete strategy
% 30.99/5.69 % (216635)------------------------------
% 30.99/5.69 % (216635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.69 % (216635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.69 % (216635)CaDiCaL version: 2.1.3
% 30.99/5.69 % (216635)Termination reason: Refutation not found, incomplete strategy
% 30.99/5.69 % (216635)Time elapsed: 0.001 s
% 30.99/5.69 % (216635)Peak memory usage: 88 MB
% 30.99/5.69 % (216635)Instructions burned: 1 (million)
% 30.99/5.69 % (216634)Instruction limit reached!
% 30.99/5.69 % (216634)------------------------------
% 30.99/5.69 % (216634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.69 % (216634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.69 % (216634)CaDiCaL version: 2.1.3
% 30.99/5.69 % (216634)Termination reason: Instruction limit
% 30.99/5.69 % (216634)Termination phase: Saturation
% 30.99/5.69 % (216634)Time elapsed: 0.100 s
% 38.51/6.68 % (216634)Peak memory usage: 89 MB
% 38.51/6.68 % (216634)Instructions burned: 113 (million)
% 38.51/6.68 % (216635)------------------------------
% 38.51/6.68 % (216635)------------------------------
% 38.51/6.68 % (216638)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1637116177:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 38.51/6.68 % (216640)lrs+10_1_sil=8000:sp=occurrence:random_seed=2652864894:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 38.51/6.68 % (216638)Instruction limit reached!
% 38.51/6.68 % (216638)------------------------------
% 38.51/6.68 % (216638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.51/6.68 % (216638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.51/6.68 % (216638)CaDiCaL version: 2.1.3
% 38.51/6.68 % (216638)Termination reason: Instruction limit
% 38.51/6.68 % (216638)Termination phase: Saturation
% 38.51/6.68 % (216638)Time elapsed: 0.097 s
% 38.51/6.68 % (216638)Peak memory usage: 89 MB
% 38.51/6.68 % (216638)Instructions burned: 115 (million)
% 38.51/6.68 % (216641)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=957217657:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 38.51/6.68 % (216644)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2671060765:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 38.51/6.68 % (216641)Instruction limit reached!
% 38.51/6.68 % (216641)------------------------------
% 38.51/6.68 % (216641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.51/6.68 % (216641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.51/6.68 % (216641)CaDiCaL version: 2.1.3
% 38.51/6.68 % (216641)Termination reason: Instruction limit
% 38.51/6.68 % (216641)Termination phase: Saturation
% 38.51/6.68 % (216641)Time elapsed: 0.362 s
% 38.51/6.68 % (216641)Peak memory usage: 92 MB
% 38.51/6.68 % (216641)Instructions burned: 438 (million)
% 38.51/6.68 % (216647)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1432510432:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 38.51/6.68 % (216647)Refutation not found, incomplete strategy
% 38.51/6.68 % (216647)------------------------------
% 38.51/6.68 % (216647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.51/6.68 % (216647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.51/6.68 % (216647)CaDiCaL version: 2.1.3
% 38.51/6.68 % (216647)Termination reason: Refutation not found, incomplete strategy
% 38.51/6.68 % (216647)Time elapsed: 0.003 s
% 38.51/6.68 % (216647)Peak memory usage: 88 MB
% 38.51/6.68 % (216647)Instructions burned: 1 (million)
% 38.51/6.68 % (216640)Instruction limit reached!
% 38.51/6.68 % (216640)------------------------------
% 38.51/6.68 % (216640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.51/6.68 % (216640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.51/6.68 % (216640)CaDiCaL version: 2.1.3
% 38.51/6.68 % (216640)Termination reason: Instruction limit
% 38.51/6.68 % (216640)Termination phase: Saturation
% 38.51/6.68 % (216640)Time elapsed: 0.860 s
% 38.51/6.68 % (216640)Peak memory usage: 97 MB
% 38.51/6.68 % (216640)Instructions burned: 907 (million)
% 38.51/6.68 % (216649)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1159105792:st=8:i=592:sd=3:ep=RST:ss=axioms_2974 on theBenchmark for (2974ds/592Mi)
% 38.51/6.68 % (216632)Instruction limit reached!
% 38.51/6.68 % (216632)------------------------------
% 38.51/6.68 % (216632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.51/6.68 % (216632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.51/6.68 % (216632)CaDiCaL version: 2.1.3
% 38.51/6.68 % (216632)Termination reason: Instruction limit
% 38.51/6.68 % (216632)Termination phase: Saturation
% 38.51/6.68 % (216632)Time elapsed: 1.699 s
% 38.51/6.68 % (216632)Peak memory usage: 143 MB
% 38.51/6.68 % (216632)Instructions burned: 2351 (million)
% 38.51/6.68 % (216647)------------------------------
% 38.51/6.68 % (216647)------------------------------
% 38.51/6.68 % (216651)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=703901114:st=3:i=13193:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/13193Mi)
% 38.51/6.68 % (216652)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=897835330:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/125Mi)
% 38.51/6.68 % (216652)Instruction limit reached!
% 38.51/6.68 % (216652)------------------------------
% 38.51/6.68 % (216652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.51/6.68 % (216652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.51/6.68 % (216652)CaDiCaL version: 2.1.3
% 38.51/6.68 % (216652)Termination reason: Instruction limit
% 38.51/6.68 % (216652)Termination phase: Saturation
% 38.51/6.68 % (216652)Time elapsed: 0.138 s
% 38.51/6.68 % (216652)Peak memory usage: 90 MB
% 38.51/6.68 % (216652)Instructions burned: 125 (million)
% 38.51/6.68 % (216649)Instruction limit reached!
% 38.51/6.68 % (216649)------------------------------
% 38.51/6.68 % (216649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.51/6.68 % (216649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.51/6.68 % (216649)CaDiCaL version: 2.1.3
% 38.51/6.68 % (216649)Termination reason: Instruction limit
% 38.51/6.68 % (216649)Termination phase: Saturation
% 38.51/6.68 % (216649)Time elapsed: 0.582 s
% 38.51/6.68 % (216649)Peak memory usage: 96 MB
% 38.51/6.68 % (216649)Instructions burned: 592 (million)
% 38.51/6.68 % (216655)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=256544200:i=134:gtgl=5:slsql=off:gtg=exists_sym_2966 on theBenchmark for (2966ds/134Mi)
% 38.51/6.68 % (216655)Instruction limit reached!
% 38.51/6.68 % (216655)------------------------------
% 38.51/6.68 % (216655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.51/6.68 % (216655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.51/6.68 % (216655)CaDiCaL version: 2.1.3
% 38.51/6.68 % (216655)Termination reason: Instruction limit
% 38.51/6.68 % (216655)Termination phase: Saturation
% 38.51/6.68 % (216655)Time elapsed: 0.081 s
% 38.51/6.68 % (216655)Peak memory usage: 88 MB
% 38.51/6.68 % (216655)Instructions burned: 135 (million)
% 38.51/6.68 % (216656)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3098968771:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/141Mi)
% 38.51/6.68 % (216656)Refutation not found, incomplete strategy
% 38.51/6.68 % (216656)------------------------------
% 38.51/6.69 % (216656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.51/6.69 % (216656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.51/6.69 % (216656)CaDiCaL version: 2.1.3
% 38.51/6.69 % (216656)Termination reason: Refutation not found, incomplete strategy
% 38.51/6.69 % (216656)Time elapsed: 0.002 s
% 38.51/6.69 % (216656)Peak memory usage: 88 MB
% 38.51/6.69 % (216659)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1071205422:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2963 on theBenchmark for (2963ds/431Mi)
% 38.51/6.69 % (216659)Refutation not found, incomplete strategy
% 38.51/6.69 % (216659)------------------------------
% 38.51/6.69 % (216659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.51/6.69 % (216659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.51/6.69 % (216659)CaDiCaL version: 2.1.3
% 38.51/6.69 % (216659)Termination reason: Refutation not found, incomplete strategy
% 38.51/6.69 % (216659)Time elapsed: 0.001 s
% 38.51/6.69 % (216659)Peak memory usage: 88 MB
% 38.51/6.69 % (216659)Instructions burned: 1 (million)
% 38.51/6.69 % (216656)------------------------------
% 38.51/6.69 % (216656)------------------------------
% 38.51/6.69 % (216659)------------------------------
% 38.51/6.69 % (216659)------------------------------
% 38.51/6.69 % (216661)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=2077903113:i=6060:aac=none:ins=25_2959 on theBenchmark for (2959ds/6060Mi)
% 38.51/6.69 % (216662)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=1347950428:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2958 on theBenchmark for (2958ds/150Mi)
% 38.51/6.69 % (216662)Instruction limit reached!
% 38.51/6.69 % (216662)------------------------------
% 38.51/6.69 % (216662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.51/6.69 % (216662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.51/6.69 % (216662)CaDiCaL version: 2.1.3
% 38.51/6.69 % (216662)Termination reason: Instruction limit
% 38.51/6.69 % (216662)Termination phase: Saturation
% 38.51/6.69 % (216662)Time elapsed: 0.069 s
% 38.51/6.69 % (216662)Peak memory usage: 90 MB
% 38.51/6.69 % (216662)Instructions burned: 152 (million)
% 38.51/6.69 % (216665)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3947313416:i=14155:bd=all_2955 on theBenchmark for (2955ds/14155Mi)
% 38.51/6.69 % (216593)First to succeed.
% 38.51/6.69 % (216593)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-216587"
% 38.51/6.69 % (216593)Refutation found. Thanks to Tanya!
% 38.51/6.69 % SZS status Theorem for theBenchmark
% 38.51/6.69 % SZS output start Proof for theBenchmark
% See solution above
% 39.27/7.08 % (216593)------------------------------
% 39.27/7.08 % (216593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.27/7.08 % (216593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.27/7.08 % (216593)CaDiCaL version: 2.1.3
% 39.27/7.08 % (216593)Termination reason: Refutation
% 39.27/7.08 % (216593)Time elapsed: 4.691 s
% 39.27/7.08 % (216593)Peak memory usage: 165 MB
% 39.27/7.08 % (216593)Instructions burned: 4463 (million)
% 39.27/7.08 % (216593)------------------------------
% 39.27/7.08 % (216593)------------------------------
% 39.27/7.08 % (216587)Success in time 5.441 s
% 39.27/7.08 % Vampire exiting
%------------------------------------------------------------------------------