%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE104+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 : n003.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:20 AM UTC 2026
% Result : Theorem 19.63s 3.67s
% Output : Refutation 20.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 24
% Syntax : Number of formulae : 246 ( 242 unt; 0 def)
% Number of atoms : 250 ( 249 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 15 ( 11 ~; 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 : 16 ( 16 usr; 5 con; 0-2 aty)
% Number of variables : 374 ( 371 !; 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(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(f26,axiom,
! [X0,X1] : backward_box(X0,X1) = c(backward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',backward_box) ).
fof(f27,conjecture,
! [X0,X1,X2] :
( addition(domain(X1),backward_box(X0,domain(X2))) = one
=> addition(forward_box(X0,domain(X1)),domain(X2)) = one ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f28,negated_conjecture,
~ ! [X0,X1,X2] :
( addition(domain(X1),backward_box(X0,domain(X2))) = one
=> addition(forward_box(X0,domain(X1)),domain(X2)) = one ),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f29,plain,
? [X0,X1,X2] :
( one != addition(forward_box(X0,domain(X1)),domain(X2))
& addition(domain(X1),backward_box(X0,domain(X2))) = one ),
inference(ennf_transformation,[],[f28]) ).
fof(f30,plain,
( one != addition(forward_box(sK0,domain(sK1)),domain(sK2))
& one = addition(domain(sK1),backward_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,
one = addition(domain(sK1),backward_box(sK0,domain(sK2))),
inference(cnf_transformation,[],[f30]) ).
fof(f32,plain,
one != addition(forward_box(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] : one = addition(coantidomain(coantidomain(X0)),coantidomain(X0)),
inference(cnf_transformation,[],[f19]) ).
fof(f39,plain,
! [X0] : one = addition(antidomain(antidomain(X0)),antidomain(X0)),
inference(cnf_transformation,[],[f15]) ).
fof(f40,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f41,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f42,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(cnf_transformation,[],[f23]) ).
fof(f44,plain,
! [X0] : c(X0) = antidomain(domain(X0)),
inference(cnf_transformation,[],[f21]) ).
fof(f45,plain,
! [X0] : antidomain(antidomain(X0)) = domain(X0),
inference(cnf_transformation,[],[f16]) ).
fof(f46,plain,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
inference(cnf_transformation,[],[f25]) ).
fof(f47,plain,
! [X0,X1] : backward_box(X0,X1) = c(backward_diamond(X0,c(X1))),
inference(cnf_transformation,[],[f26]) ).
fof(f48,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f49,plain,
! [X0] : coantidomain(coantidomain(X0)) = codomain(X0),
inference(cnf_transformation,[],[f20]) ).
fof(f50,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(f51,plain,
! [X0] : zero = multiplication(X0,coantidomain(X0)),
inference(cnf_transformation,[],[f17]) ).
fof(f52,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(f53,plain,
! [X0] : zero = multiplication(antidomain(X0),X0),
inference(cnf_transformation,[],[f13]) ).
fof(f54,plain,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
inference(cnf_transformation,[],[f24]) ).
fof(f55,plain,
! [X0] : zero = multiplication(zero,X0),
inference(cnf_transformation,[],[f11]) ).
fof(f57,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f58,plain,
! [X0] : c(X0) = antidomain(antidomain(antidomain(X0))),
inference(definition_unfolding,[],[f44,f45]) ).
fof(f59,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f54,f49,f49]) ).
fof(f60,plain,
! [X0,X1] : backward_box(X0,X1) = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X0)))))),
inference(definition_unfolding,[],[f47,f58,f59,f58]) ).
fof(f62,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f42,f45,f45]) ).
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,[],[f46,f58,f62,f58]) ).
fof(f64,plain,
one != addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))))))),antidomain(antidomain(sK2))),
inference(definition_unfolding,[],[f32,f63,f45,f45]) ).
fof(f65,plain,
one = addition(antidomain(antidomain(sK1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2))))))),sK0))))))),
inference(definition_unfolding,[],[f31,f45,f60,f45]) ).
fof(f66,plain,
one != addition(antidomain(antidomain(sK2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1)))))))))))))),
inference(forward_demodulation,[],[f64,f37]) ).
fof(f73,plain,
! [X0] : one = addition(antidomain(X0),antidomain(antidomain(X0))),
inference(superposition,[],[f39,f37]) ).
fof(f74,plain,
! [X0] : one = addition(coantidomain(X0),coantidomain(coantidomain(X0))),
inference(superposition,[],[f38,f37]) ).
fof(f76,plain,
zero = antidomain(one),
inference(superposition,[],[f41,f53]) ).
fof(f78,plain,
one = addition(antidomain(zero),zero),
inference(superposition,[],[f39,f76]) ).
fof(f79,plain,
one = antidomain(zero),
inference(forward_demodulation,[],[f78,f57]) ).
fof(f80,plain,
! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)),
inference(superposition,[],[f33,f40]) ).
fof(f82,plain,
! [X0,X1] : multiplication(addition(antidomain(X0),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(superposition,[],[f33,f53]) ).
fof(f85,plain,
! [X0,X1] : multiplication(addition(X0,antidomain(X1)),X1) = addition(multiplication(X0,X1),zero),
inference(superposition,[],[f33,f53]) ).
fof(f90,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(addition(X0,antidomain(X1)),X1),
inference(forward_demodulation,[],[f85,f57]) ).
fof(f97,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = addition(multiplication(X0,coantidomain(X1)),zero),
inference(superposition,[],[f33,f51]) ).
fof(f99,plain,
zero = coantidomain(one),
inference(superposition,[],[f40,f51]) ).
fof(f100,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = multiplication(X0,coantidomain(X1)),
inference(forward_demodulation,[],[f97,f57]) ).
fof(f102,plain,
one = addition(coantidomain(zero),zero),
inference(superposition,[],[f38,f99]) ).
fof(f103,plain,
one = coantidomain(zero),
inference(forward_demodulation,[],[f102,f57]) ).
fof(f106,plain,
! [X0,X1] : multiplication(X1,X0) = multiplication(addition(antidomain(X0),X1),X0),
inference(superposition,[],[f90,f37]) ).
fof(f108,plain,
! [X0] : multiplication(one,X0) = multiplication(antidomain(antidomain(X0)),X0),
inference(superposition,[],[f90,f39]) ).
fof(f117,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f108,f40]) ).
fof(f127,plain,
! [X0] : addition(zero,X0) = X0,
inference(superposition,[],[f37,f57]) ).
fof(f146,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(superposition,[],[f34,f41]) ).
fof(f151,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X0,X1)) = addition(zero,multiplication(antidomain(X0),X1)),
inference(superposition,[],[f34,f53]) ).
fof(f153,plain,
! [X0,X1] : addition(multiplication(X0,X1),zero) = multiplication(X0,addition(X1,coantidomain(X0))),
inference(superposition,[],[f34,f51]) ).
fof(f157,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X1,X0)) = addition(multiplication(antidomain(X0),X1),zero),
inference(superposition,[],[f34,f53]) ).
fof(f170,plain,
! [X0,X1] : multiplication(antidomain(X0),X1) = multiplication(antidomain(X0),addition(X1,X0)),
inference(forward_demodulation,[],[f157,f57]) ).
fof(f174,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(X0,addition(X1,coantidomain(X0))),
inference(forward_demodulation,[],[f153,f57]) ).
fof(f176,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X0,X1)) = multiplication(antidomain(X0),X1),
inference(forward_demodulation,[],[f151,f127]) ).
fof(f183,plain,
! [X2,X0,X1] : multiplication(antidomain(multiplication(X1,X2)),multiplication(X0,X2)) = multiplication(antidomain(multiplication(X1,X2)),multiplication(addition(X0,X1),X2)),
inference(superposition,[],[f170,f33]) ).
fof(f184,plain,
! [X2,X0,X1] : multiplication(antidomain(multiplication(X0,X2)),multiplication(X0,X1)) = multiplication(antidomain(multiplication(X0,X2)),multiplication(X0,addition(X1,X2))),
inference(superposition,[],[f170,f34]) ).
fof(f213,plain,
! [X0,X1] : multiplication(antidomain(multiplication(antidomain(X0),X1)),multiplication(antidomain(antidomain(X0)),X1)) = multiplication(antidomain(multiplication(antidomain(X0),X1)),multiplication(one,X1)),
inference(superposition,[],[f183,f39]) ).
fof(f214,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,[],[f183,f38]) ).
fof(f225,plain,
! [X0,X1] : multiplication(antidomain(multiplication(coantidomain(X0),X1)),multiplication(coantidomain(coantidomain(X0)),X1)) = multiplication(antidomain(multiplication(coantidomain(X0),X1)),X1),
inference(forward_demodulation,[],[f214,f40]) ).
fof(f226,plain,
! [X0,X1] : multiplication(antidomain(multiplication(antidomain(X0),X1)),multiplication(antidomain(antidomain(X0)),X1)) = multiplication(antidomain(multiplication(antidomain(X0),X1)),X1),
inference(forward_demodulation,[],[f213,f40]) ).
fof(f241,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f36,f35]) ).
fof(f245,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(f258,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(superposition,[],[f37,f36]) ).
fof(f349,plain,
! [X0] : multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)) = multiplication(antidomain(antidomain(antidomain(X0))),one),
inference(superposition,[],[f176,f39]) ).
fof(f362,plain,
! [X0] : antidomain(antidomain(antidomain(X0))) = multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)),
inference(forward_demodulation,[],[f349,f41]) ).
fof(f368,plain,
! [X0] : antidomain(X0) = antidomain(antidomain(antidomain(X0))),
inference(forward_demodulation,[],[f362,f117]) ).
fof(f381,plain,
one != addition(antidomain(antidomain(sK2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(sK1)))))))))))),
inference(superposition,[],[f66,f368]) ).
fof(f382,plain,
one = addition(antidomain(antidomain(sK1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sK2))))),sK0))))))),
inference(superposition,[],[f65,f368]) ).
fof(f391,plain,
one = addition(antidomain(antidomain(sK1)),antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sK2))))),sK0))))),
inference(forward_demodulation,[],[f382,f368]) ).
fof(f392,plain,
one != addition(antidomain(antidomain(sK2)),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(sK1)))))))))),
inference(forward_demodulation,[],[f381,f368]) ).
fof(f404,plain,
one = addition(antidomain(antidomain(sK1)),antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0))))),
inference(forward_demodulation,[],[f391,f368]) ).
fof(f405,plain,
one != addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(sK1)))))))),
inference(forward_demodulation,[],[f392,f368]) ).
fof(f416,plain,
one != addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(antidomain(antidomain(sK1)))))),
inference(forward_demodulation,[],[f405,f368]) ).
fof(f424,plain,
one != addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))),
inference(forward_demodulation,[],[f416,f368]) ).
fof(f437,plain,
! [X0] : multiplication(antidomain(X0),coantidomain(antidomain(antidomain(X0)))) = multiplication(one,coantidomain(antidomain(antidomain(X0)))),
inference(superposition,[],[f100,f73]) ).
fof(f440,plain,
! [X0,X1] : multiplication(antidomain(multiplication(antidomain(antidomain(X0)),X1)),multiplication(antidomain(X0),X1)) = multiplication(antidomain(multiplication(antidomain(antidomain(X0)),X1)),multiplication(one,X1)),
inference(superposition,[],[f183,f73]) ).
fof(f441,plain,
! [X0,X1] : multiplication(antidomain(multiplication(antidomain(antidomain(X0)),X1)),multiplication(antidomain(X0),X1)) = multiplication(antidomain(multiplication(antidomain(antidomain(X0)),X1)),X1),
inference(forward_demodulation,[],[f440,f40]) ).
fof(f444,plain,
! [X0] : coantidomain(antidomain(antidomain(X0))) = multiplication(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(forward_demodulation,[],[f437,f40]) ).
fof(f454,plain,
! [X0] : multiplication(X0,one) = multiplication(X0,coantidomain(coantidomain(X0))),
inference(superposition,[],[f174,f38]) ).
fof(f474,plain,
! [X0] : multiplication(X0,coantidomain(coantidomain(X0))) = X0,
inference(forward_demodulation,[],[f454,f41]) ).
fof(f497,plain,
! [X0] : one = addition(antidomain(X0),one),
inference(superposition,[],[f241,f73]) ).
fof(f512,plain,
! [X0] : one = addition(one,antidomain(X0)),
inference(forward_demodulation,[],[f497,f37]) ).
fof(f759,plain,
! [X0,X1] : multiplication(zero,X1) = multiplication(antidomain(X0),multiplication(X0,X1)),
inference(superposition,[],[f48,f53]) ).
fof(f788,plain,
! [X0,X1] : zero = multiplication(antidomain(X0),multiplication(X0,X1)),
inference(forward_demodulation,[],[f759,f55]) ).
fof(f904,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,[],[f245,f33]) ).
fof(f1079,plain,
! [X0,X1] : multiplication(antidomain(multiplication(X0,antidomain(X1))),multiplication(X0,one)) = multiplication(antidomain(multiplication(X0,antidomain(X1))),multiplication(X0,antidomain(antidomain(X1)))),
inference(superposition,[],[f184,f39]) ).
fof(f1081,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,[],[f184,f38]) ).
fof(f1115,plain,
! [X0,X1] : multiplication(antidomain(multiplication(X0,coantidomain(X1))),multiplication(X0,coantidomain(coantidomain(X1)))) = multiplication(antidomain(multiplication(X0,coantidomain(X1))),X0),
inference(forward_demodulation,[],[f1081,f41]) ).
fof(f1117,plain,
! [X0,X1] : multiplication(antidomain(multiplication(X0,antidomain(X1))),multiplication(X0,antidomain(antidomain(X1)))) = multiplication(antidomain(multiplication(X0,antidomain(X1))),X0),
inference(forward_demodulation,[],[f1079,f41]) ).
fof(f1234,plain,
! [X2,X0,X1] : addition(multiplication(X0,one),multiplication(X2,antidomain(X1))) = addition(multiplication(X0,antidomain(antidomain(X1))),multiplication(addition(X0,X2),antidomain(X1))),
inference(superposition,[],[f904,f39]) ).
fof(f1236,plain,
! [X2,X0,X1] : addition(multiplication(X0,coantidomain(coantidomain(X1))),multiplication(addition(X0,X2),coantidomain(X1))) = addition(multiplication(X0,one),multiplication(X2,coantidomain(X1))),
inference(superposition,[],[f904,f38]) ).
fof(f1299,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,[],[f904,f39]) ).
fof(f1358,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,[],[f1299,f40]) ).
fof(f1409,plain,
! [X2,X0,X1] : addition(multiplication(X0,coantidomain(coantidomain(X1))),multiplication(addition(X0,X2),coantidomain(X1))) = addition(X0,multiplication(X2,coantidomain(X1))),
inference(forward_demodulation,[],[f1236,f41]) ).
fof(f1411,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,[],[f1234,f41]) ).
fof(f1434,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,[],[f1358,f37]) ).
fof(f1515,plain,
! [X0,X1] : addition(X0,multiplication(X0,coantidomain(X1))) = addition(multiplication(X0,coantidomain(coantidomain(X1))),multiplication(X0,coantidomain(X1))),
inference(superposition,[],[f1409,f35]) ).
fof(f1585,plain,
! [X0,X1] : addition(X0,multiplication(X0,coantidomain(X1))) = addition(multiplication(X0,coantidomain(X1)),multiplication(X0,coantidomain(coantidomain(X1)))),
inference(forward_demodulation,[],[f1515,f37]) ).
fof(f1615,plain,
! [X0,X1] : addition(X0,multiplication(X0,coantidomain(X1))) = multiplication(X0,addition(coantidomain(X1),coantidomain(coantidomain(X1)))),
inference(forward_demodulation,[],[f1585,f34]) ).
fof(f1633,plain,
! [X0,X1] : multiplication(X0,one) = addition(X0,multiplication(X0,coantidomain(X1))),
inference(forward_demodulation,[],[f1615,f74]) ).
fof(f1646,plain,
! [X0,X1] : multiplication(X0,one) = multiplication(X0,addition(one,coantidomain(X1))),
inference(forward_demodulation,[],[f1633,f146]) ).
fof(f1656,plain,
! [X0,X1] : multiplication(X0,addition(one,coantidomain(X1))) = X0,
inference(forward_demodulation,[],[f1646,f41]) ).
fof(f1685,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,[],[f1411,f39]) ).
fof(f1721,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,[],[f1685,f37]) ).
fof(f1752,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,[],[f1721,f40]) ).
fof(f1839,plain,
! [X0,X1] : addition(multiplication(antidomain(antidomain(X0)),one),antidomain(X1)) = addition(multiplication(antidomain(X0),antidomain(X1)),multiplication(antidomain(antidomain(X0)),one)),
inference(superposition,[],[f1434,f512]) ).
fof(f1842,plain,
! [X0,X1] : addition(multiplication(antidomain(antidomain(X0)),antidomain(X1)),antidomain(antidomain(X1))) = addition(multiplication(antidomain(X0),antidomain(antidomain(X1))),multiplication(antidomain(antidomain(X0)),one)),
inference(superposition,[],[f1434,f73]) ).
fof(f1872,plain,
! [X0,X1] : addition(multiplication(antidomain(antidomain(X0)),antidomain(X1)),antidomain(antidomain(X1))) = addition(multiplication(antidomain(antidomain(X0)),one),multiplication(antidomain(X0),antidomain(antidomain(X1)))),
inference(forward_demodulation,[],[f1842,f37]) ).
fof(f1875,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),antidomain(X1)) = addition(multiplication(antidomain(X0),antidomain(X1)),antidomain(antidomain(X0))),
inference(forward_demodulation,[],[f1839,f41]) ).
fof(f1905,plain,
! [X0,X1] : addition(multiplication(antidomain(antidomain(X0)),antidomain(X1)),antidomain(antidomain(X1))) = addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),antidomain(antidomain(X1)))),
inference(forward_demodulation,[],[f1872,f41]) ).
fof(f1908,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),antidomain(X1))) = addition(antidomain(antidomain(X0)),antidomain(X1)),
inference(forward_demodulation,[],[f1875,f37]) ).
fof(f1924,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),multiplication(antidomain(X0),antidomain(antidomain(X1)))) = addition(antidomain(antidomain(X1)),multiplication(antidomain(antidomain(X0)),antidomain(X1))),
inference(forward_demodulation,[],[f1905,f37]) ).
fof(f1934,plain,
! [X0,X1] : addition(antidomain(antidomain(X1)),multiplication(antidomain(antidomain(X0)),antidomain(X1))) = addition(antidomain(antidomain(X0)),antidomain(antidomain(X1))),
inference(forward_demodulation,[],[f1924,f1908]) ).
fof(f1948,plain,
! [X0,X1] : addition(antidomain(X0),multiplication(antidomain(antidomain(X1)),antidomain(antidomain(X0)))) = addition(antidomain(antidomain(X1)),antidomain(X0)),
inference(superposition,[],[f1934,f368]) ).
fof(f1952,plain,
! [X0,X1] : addition(antidomain(antidomain(X1)),multiplication(antidomain(X0),antidomain(X1))) = addition(antidomain(X0),antidomain(antidomain(X1))),
inference(superposition,[],[f1934,f368]) ).
fof(f1965,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,[],[f176,f1934]) ).
fof(f1978,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,[],[f1965,f170]) ).
fof(f1989,plain,
! [X0,X1] : multiplication(antidomain(X1),antidomain(antidomain(X0))) = multiplication(antidomain(X1),multiplication(antidomain(antidomain(X0)),antidomain(X1))),
inference(forward_demodulation,[],[f1978,f368]) ).
fof(f2095,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,[],[f174,f50]) ).
fof(f2113,plain,
! [X0,X1] : zero = multiplication(multiplication(coantidomain(coantidomain(X0)),X1),coantidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f2095,f51]) ).
fof(f2132,plain,
! [X0,X1] : zero = multiplication(coantidomain(coantidomain(X0)),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f2113,f48]) ).
fof(f2147,plain,
! [X0] : multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))) = multiplication(one,coantidomain(coantidomain(coantidomain(X0)))),
inference(superposition,[],[f100,f74]) ).
fof(f2168,plain,
! [X0] : coantidomain(coantidomain(coantidomain(X0))) = multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f2147,f40]) ).
fof(f2176,plain,
! [X0] : coantidomain(X0) = coantidomain(coantidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f2168,f474]) ).
fof(f2546,plain,
multiplication(antidomain(antidomain(sK1)),coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0)))) = multiplication(one,coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0)))),
inference(superposition,[],[f90,f404]) ).
fof(f2573,plain,
coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0))) = multiplication(antidomain(antidomain(sK1)),coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK2))),sK0)))),
inference(forward_demodulation,[],[f2546,f40]) ).
fof(f2727,plain,
! [X0] : multiplication(antidomain(X0),addition(one,coantidomain(antidomain(antidomain(X0))))) = addition(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(superposition,[],[f146,f444]) ).
fof(f2738,plain,
! [X0] : antidomain(X0) = addition(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(forward_demodulation,[],[f2727,f1656]) ).
fof(f2789,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,[],[f90,f52]) ).
fof(f2810,plain,
! [X0,X1] : zero = multiplication(antidomain(multiplication(X0,X1)),multiplication(X0,antidomain(antidomain(X1)))),
inference(forward_demodulation,[],[f2789,f53]) ).
fof(f2889,plain,
! [X0,X1] : zero = multiplication(antidomain(zero),multiplication(antidomain(X0),antidomain(antidomain(multiplication(X0,X1))))),
inference(superposition,[],[f2810,f788]) ).
fof(f2960,plain,
! [X0,X1] : zero = multiplication(one,multiplication(antidomain(X0),antidomain(antidomain(multiplication(X0,X1))))),
inference(forward_demodulation,[],[f2889,f79]) ).
fof(f2983,plain,
! [X0,X1] : zero = multiplication(antidomain(X0),antidomain(antidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f2960,f40]) ).
fof(f3192,plain,
! [X0,X1] : multiplication(antidomain(zero),antidomain(X0)) = multiplication(antidomain(zero),multiplication(antidomain(X0),antidomain(antidomain(antidomain(multiplication(X0,X1)))))),
inference(superposition,[],[f1117,f2983]) ).
fof(f3197,plain,
! [X2,X0,X1] : multiplication(zero,X2) = multiplication(antidomain(X0),multiplication(antidomain(antidomain(multiplication(X0,X1))),X2)),
inference(superposition,[],[f48,f2983]) ).
fof(f3223,plain,
! [X2,X0,X1] : zero = multiplication(antidomain(X0),multiplication(antidomain(antidomain(multiplication(X0,X1))),X2)),
inference(forward_demodulation,[],[f3197,f55]) ).
fof(f3228,plain,
! [X0,X1] : multiplication(antidomain(zero),antidomain(X0)) = multiplication(antidomain(zero),multiplication(antidomain(X0),antidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f3192,f368]) ).
fof(f3258,plain,
! [X0,X1] : multiplication(one,antidomain(X0)) = multiplication(one,multiplication(antidomain(X0),antidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f3228,f79]) ).
fof(f3275,plain,
! [X0,X1] : multiplication(one,antidomain(X0)) = multiplication(antidomain(X0),antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f3258,f40]) ).
fof(f3278,plain,
! [X0,X1] : antidomain(X0) = multiplication(antidomain(X0),antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f3275,f40]) ).
fof(f3326,plain,
! [X0,X1] : multiplication(addition(one,antidomain(X0)),antidomain(multiplication(X0,X1))) = addition(antidomain(multiplication(X0,X1)),antidomain(X0)),
inference(superposition,[],[f80,f3278]) ).
fof(f3343,plain,
! [X0,X1] : multiplication(addition(one,antidomain(X0)),antidomain(multiplication(X0,X1))) = addition(antidomain(X0),antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f3326,f37]) ).
fof(f3363,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(multiplication(X0,X1))) = multiplication(one,antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f3343,f512]) ).
fof(f3366,plain,
! [X0,X1] : antidomain(multiplication(X0,X1)) = addition(antidomain(X0),antidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f3363,f40]) ).
fof(f3368,plain,
! [X0,X1] : antidomain(multiplication(antidomain(antidomain(X0)),X1)) = addition(antidomain(X0),antidomain(multiplication(antidomain(antidomain(X0)),X1))),
inference(superposition,[],[f3366,f368]) ).
fof(f3470,plain,
! [X0] : zero = multiplication(coantidomain(coantidomain(antidomain(X0))),multiplication(X0,coantidomain(zero))),
inference(superposition,[],[f2132,f53]) ).
fof(f3550,plain,
! [X0] : zero = multiplication(coantidomain(coantidomain(antidomain(X0))),multiplication(X0,one)),
inference(forward_demodulation,[],[f3470,f103]) ).
fof(f3579,plain,
! [X0] : zero = multiplication(coantidomain(coantidomain(antidomain(X0))),X0),
inference(forward_demodulation,[],[f3550,f41]) ).
fof(f4353,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,[],[f106,f1752]) ).
fof(f4419,plain,
! [X0,X1] : multiplication(multiplication(antidomain(X1),antidomain(X0)),antidomain(X1)) = multiplication(addition(antidomain(antidomain(X1)),antidomain(X0)),antidomain(X1)),
inference(forward_demodulation,[],[f4353,f1948]) ).
fof(f4451,plain,
! [X0,X1] : multiplication(multiplication(antidomain(X1),antidomain(X0)),antidomain(X1)) = addition(zero,multiplication(antidomain(X0),antidomain(X1))),
inference(forward_demodulation,[],[f4419,f82]) ).
fof(f4471,plain,
! [X0,X1] : multiplication(antidomain(X0),antidomain(X1)) = multiplication(multiplication(antidomain(X1),antidomain(X0)),antidomain(X1)),
inference(forward_demodulation,[],[f4451,f127]) ).
fof(f4481,plain,
! [X0,X1] : multiplication(antidomain(X0),antidomain(X1)) = multiplication(antidomain(X1),multiplication(antidomain(X0),antidomain(X1))),
inference(forward_demodulation,[],[f4471,f48]) ).
fof(f5421,plain,
! [X0] : multiplication(antidomain(X0),X0) = multiplication(coantidomain(antidomain(antidomain(X0))),X0),
inference(superposition,[],[f106,f2738]) ).
fof(f5444,plain,
! [X0] : zero = multiplication(coantidomain(antidomain(antidomain(X0))),X0),
inference(forward_demodulation,[],[f5421,f53]) ).
fof(f5515,plain,
! [X0,X1] : multiplication(antidomain(antidomain(X0)),antidomain(X1)) = multiplication(antidomain(X1),antidomain(antidomain(X0))),
inference(superposition,[],[f1989,f4481]) ).
fof(f5541,plain,
! [X0,X1] : antidomain(multiplication(antidomain(X0),antidomain(X1))) = addition(antidomain(antidomain(X1)),antidomain(multiplication(antidomain(X0),antidomain(X1)))),
inference(superposition,[],[f3366,f4481]) ).
fof(f5572,plain,
! [X0,X1] : multiplication(antidomain(X1),antidomain(X0)) = multiplication(antidomain(X0),antidomain(X1)),
inference(superposition,[],[f5515,f368]) ).
fof(f5640,plain,
! [X2,X0,X1] : multiplication(multiplication(antidomain(antidomain(X0)),antidomain(X1)),X2) = multiplication(antidomain(X1),multiplication(antidomain(antidomain(X0)),X2)),
inference(superposition,[],[f48,f5515]) ).
fof(f5667,plain,
! [X2,X0,X1] : multiplication(antidomain(antidomain(X0)),multiplication(antidomain(X1),X2)) = multiplication(antidomain(X1),multiplication(antidomain(antidomain(X0)),X2)),
inference(forward_demodulation,[],[f5640,f48]) ).
fof(f5796,plain,
! [X2,X0,X1] : multiplication(antidomain(X1),multiplication(antidomain(X0),X2)) = multiplication(multiplication(antidomain(X0),antidomain(X1)),X2),
inference(superposition,[],[f48,f5572]) ).
fof(f5823,plain,
! [X2,X0,X1] : multiplication(antidomain(X1),multiplication(antidomain(X0),X2)) = multiplication(antidomain(X0),multiplication(antidomain(X1),X2)),
inference(forward_demodulation,[],[f5796,f48]) ).
fof(f6124,plain,
! [X0,X1] : multiplication(antidomain(multiplication(antidomain(antidomain(multiplication(antidomain(X0),X1))),multiplication(antidomain(antidomain(X0)),X1))),multiplication(antidomain(antidomain(X0)),X1)) = multiplication(antidomain(multiplication(antidomain(antidomain(multiplication(antidomain(X0),X1))),multiplication(antidomain(antidomain(X0)),X1))),multiplication(antidomain(multiplication(antidomain(X0),X1)),X1)),
inference(superposition,[],[f441,f226]) ).
fof(f6194,plain,
! [X0,X1] : multiplication(antidomain(multiplication(antidomain(antidomain(multiplication(antidomain(X0),X1))),multiplication(antidomain(antidomain(X0)),X1))),multiplication(antidomain(antidomain(X0)),X1)) = multiplication(antidomain(multiplication(antidomain(X0),X1)),multiplication(antidomain(multiplication(antidomain(antidomain(multiplication(antidomain(X0),X1))),multiplication(antidomain(antidomain(X0)),X1))),X1)),
inference(forward_demodulation,[],[f6124,f5823]) ).
fof(f6254,plain,
! [X0,X1] : multiplication(antidomain(multiplication(antidomain(antidomain(X0)),multiplication(antidomain(antidomain(multiplication(antidomain(X0),X1))),X1))),multiplication(antidomain(antidomain(X0)),X1)) = multiplication(antidomain(multiplication(antidomain(X0),X1)),multiplication(antidomain(multiplication(antidomain(antidomain(X0)),multiplication(antidomain(antidomain(multiplication(antidomain(X0),X1))),X1))),X1)),
inference(forward_demodulation,[],[f6194,f5667]) ).
fof(f6297,plain,
! [X0,X1] : multiplication(antidomain(zero),multiplication(antidomain(antidomain(X0)),X1)) = multiplication(antidomain(multiplication(antidomain(X0),X1)),multiplication(antidomain(zero),X1)),
inference(forward_demodulation,[],[f6254,f3223]) ).
fof(f6323,plain,
! [X0,X1] : multiplication(antidomain(zero),multiplication(antidomain(antidomain(X0)),X1)) = multiplication(antidomain(zero),multiplication(antidomain(multiplication(antidomain(X0),X1)),X1)),
inference(forward_demodulation,[],[f6297,f5823]) ).
fof(f6336,plain,
! [X0,X1] : multiplication(one,multiplication(antidomain(antidomain(X0)),X1)) = multiplication(one,multiplication(antidomain(multiplication(antidomain(X0),X1)),X1)),
inference(forward_demodulation,[],[f6323,f79]) ).
fof(f6342,plain,
! [X0,X1] : multiplication(antidomain(multiplication(antidomain(X0),X1)),X1) = multiplication(one,multiplication(antidomain(antidomain(X0)),X1)),
inference(forward_demodulation,[],[f6336,f40]) ).
fof(f6344,plain,
! [X0,X1] : multiplication(antidomain(antidomain(X0)),X1) = multiplication(antidomain(multiplication(antidomain(X0),X1)),X1),
inference(forward_demodulation,[],[f6342,f40]) ).
fof(f6392,plain,
! [X0,X1] : addition(antidomain(antidomain(X1)),multiplication(antidomain(antidomain(X0)),antidomain(X1))) = addition(antidomain(multiplication(antidomain(X0),antidomain(X1))),antidomain(antidomain(X1))),
inference(superposition,[],[f1952,f6344]) ).
fof(f6459,plain,
! [X0,X1] : addition(antidomain(antidomain(X1)),multiplication(antidomain(antidomain(X0)),antidomain(X1))) = addition(antidomain(antidomain(X1)),antidomain(multiplication(antidomain(X0),antidomain(X1)))),
inference(forward_demodulation,[],[f6392,f37]) ).
fof(f6500,plain,
! [X0,X1] : addition(antidomain(antidomain(X1)),multiplication(antidomain(antidomain(X0)),antidomain(X1))) = antidomain(multiplication(antidomain(X0),antidomain(X1))),
inference(forward_demodulation,[],[f6459,f5541]) ).
fof(f6526,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),antidomain(antidomain(X1))) = antidomain(multiplication(antidomain(X0),antidomain(X1))),
inference(forward_demodulation,[],[f6500,f1952]) ).
fof(f6543,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(antidomain(X1))) = antidomain(multiplication(antidomain(antidomain(X0)),antidomain(X1))),
inference(superposition,[],[f6526,f368]) ).
fof(f6728,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,[],[f52,f6543]) ).
fof(f6825,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,[],[f6728,f258]) ).
fof(f6858,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,[],[f6825,f37]) ).
fof(f6877,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(antidomain(antidomain(X1)))) = addition(antidomain(antidomain(antidomain(X1))),antidomain(multiplication(antidomain(antidomain(X0)),X1))),
inference(forward_demodulation,[],[f6858,f3368]) ).
fof(f6888,plain,
! [X0,X1] : addition(antidomain(X0),antidomain(X1)) = addition(antidomain(X1),antidomain(multiplication(antidomain(antidomain(X0)),X1))),
inference(forward_demodulation,[],[f6877,f368]) ).
fof(f7105,plain,
! [X0,X1] : addition(antidomain(antidomain(X0)),antidomain(X1)) = addition(antidomain(X1),antidomain(multiplication(antidomain(X0),X1))),
inference(superposition,[],[f6888,f368]) ).
fof(f7406,plain,
! [X0] : multiplication(antidomain(zero),X0) = multiplication(antidomain(zero),multiplication(coantidomain(coantidomain(coantidomain(antidomain(X0)))),X0)),
inference(superposition,[],[f225,f3579]) ).
fof(f7501,plain,
! [X0] : multiplication(antidomain(zero),X0) = multiplication(antidomain(zero),multiplication(coantidomain(antidomain(X0)),X0)),
inference(forward_demodulation,[],[f7406,f2176]) ).
fof(f7525,plain,
! [X0] : multiplication(one,X0) = multiplication(one,multiplication(coantidomain(antidomain(X0)),X0)),
inference(forward_demodulation,[],[f7501,f79]) ).
fof(f7537,plain,
! [X0] : multiplication(one,X0) = multiplication(coantidomain(antidomain(X0)),X0),
inference(forward_demodulation,[],[f7525,f40]) ).
fof(f7542,plain,
! [X0] : multiplication(coantidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f7537,f40]) ).
fof(f7584,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,[],[f1117,f7542]) ).
fof(f7591,plain,
! [X0] : multiplication(antidomain(multiplication(coantidomain(antidomain(antidomain(antidomain(X0)))),antidomain(X0))),coantidomain(antidomain(antidomain(antidomain(X0))))) = multiplication(antidomain(antidomain(X0)),antidomain(multiplication(coantidomain(antidomain(antidomain(antidomain(X0)))),antidomain(X0)))),
inference(forward_demodulation,[],[f7584,f5515]) ).
fof(f7618,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),antidomain(zero)) = multiplication(antidomain(zero),coantidomain(antidomain(antidomain(antidomain(X0))))),
inference(forward_demodulation,[],[f7591,f5444]) ).
fof(f7628,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),antidomain(zero)) = multiplication(antidomain(zero),coantidomain(antidomain(X0))),
inference(forward_demodulation,[],[f7618,f368]) ).
fof(f7631,plain,
! [X0] : multiplication(one,coantidomain(antidomain(X0))) = multiplication(antidomain(antidomain(X0)),one),
inference(forward_demodulation,[],[f7628,f79]) ).
fof(f7632,plain,
! [X0] : antidomain(antidomain(X0)) = multiplication(one,coantidomain(antidomain(X0))),
inference(forward_demodulation,[],[f7631,f41]) ).
fof(f7633,plain,
! [X0] : antidomain(antidomain(X0)) = coantidomain(antidomain(X0)),
inference(forward_demodulation,[],[f7632,f40]) ).
fof(f7647,plain,
coantidomain(coantidomain(multiplication(coantidomain(antidomain(antidomain(sK2))),sK0))) = multiplication(antidomain(antidomain(sK1)),coantidomain(coantidomain(multiplication(coantidomain(antidomain(antidomain(sK2))),sK0)))),
inference(superposition,[],[f2573,f7633]) ).
fof(f7687,plain,
coantidomain(coantidomain(multiplication(antidomain(antidomain(antidomain(sK2))),sK0))) = multiplication(antidomain(antidomain(sK1)),coantidomain(coantidomain(multiplication(antidomain(antidomain(antidomain(sK2))),sK0)))),
inference(forward_demodulation,[],[f7647,f7633]) ).
fof(f7702,plain,
coantidomain(coantidomain(multiplication(antidomain(sK2),sK0))) = multiplication(antidomain(antidomain(sK1)),coantidomain(coantidomain(multiplication(antidomain(sK2),sK0)))),
inference(forward_demodulation,[],[f7687,f368]) ).
fof(f7826,plain,
zero = multiplication(antidomain(antidomain(antidomain(sK1))),coantidomain(coantidomain(multiplication(antidomain(sK2),sK0)))),
inference(superposition,[],[f788,f7702]) ).
fof(f7846,plain,
zero = multiplication(antidomain(sK1),coantidomain(coantidomain(multiplication(antidomain(sK2),sK0)))),
inference(forward_demodulation,[],[f7826,f368]) ).
fof(f7890,plain,
multiplication(antidomain(zero),multiplication(antidomain(sK1),coantidomain(coantidomain(coantidomain(multiplication(antidomain(sK2),sK0)))))) = multiplication(antidomain(zero),antidomain(sK1)),
inference(superposition,[],[f1115,f7846]) ).
fof(f7940,plain,
multiplication(one,antidomain(sK1)) = multiplication(one,multiplication(antidomain(sK1),coantidomain(coantidomain(coantidomain(multiplication(antidomain(sK2),sK0)))))),
inference(forward_demodulation,[],[f7890,f79]) ).
fof(f7961,plain,
multiplication(one,antidomain(sK1)) = multiplication(antidomain(sK1),coantidomain(coantidomain(coantidomain(multiplication(antidomain(sK2),sK0))))),
inference(forward_demodulation,[],[f7940,f40]) ).
fof(f7976,plain,
multiplication(one,antidomain(sK1)) = multiplication(antidomain(sK1),coantidomain(multiplication(antidomain(sK2),sK0))),
inference(forward_demodulation,[],[f7961,f2176]) ).
fof(f7984,plain,
antidomain(sK1) = multiplication(antidomain(sK1),coantidomain(multiplication(antidomain(sK2),sK0))),
inference(forward_demodulation,[],[f7976,f40]) ).
fof(f8004,plain,
addition(coantidomain(multiplication(antidomain(sK2),sK0)),antidomain(sK1)) = multiplication(addition(one,antidomain(sK1)),coantidomain(multiplication(antidomain(sK2),sK0))),
inference(superposition,[],[f80,f7984]) ).
fof(f8029,plain,
addition(coantidomain(multiplication(antidomain(sK2),sK0)),antidomain(sK1)) = multiplication(one,coantidomain(multiplication(antidomain(sK2),sK0))),
inference(forward_demodulation,[],[f8004,f512]) ).
fof(f8039,plain,
coantidomain(multiplication(antidomain(sK2),sK0)) = addition(coantidomain(multiplication(antidomain(sK2),sK0)),antidomain(sK1)),
inference(forward_demodulation,[],[f8029,f40]) ).
fof(f8044,plain,
coantidomain(multiplication(antidomain(sK2),sK0)) = addition(antidomain(sK1),coantidomain(multiplication(antidomain(sK2),sK0))),
inference(forward_demodulation,[],[f8039,f37]) ).
fof(f8052,plain,
multiplication(multiplication(antidomain(sK2),sK0),antidomain(sK1)) = multiplication(multiplication(antidomain(sK2),sK0),coantidomain(multiplication(antidomain(sK2),sK0))),
inference(superposition,[],[f174,f8044]) ).
fof(f8074,plain,
zero = multiplication(multiplication(antidomain(sK2),sK0),antidomain(sK1)),
inference(forward_demodulation,[],[f8052,f51]) ).
fof(f8078,plain,
zero = multiplication(antidomain(sK2),multiplication(sK0,antidomain(sK1))),
inference(forward_demodulation,[],[f8074,f48]) ).
fof(f8082,plain,
addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))) = addition(antidomain(multiplication(sK0,antidomain(sK1))),antidomain(zero)),
inference(superposition,[],[f7105,f8078]) ).
fof(f8140,plain,
addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))) = addition(antidomain(zero),antidomain(multiplication(sK0,antidomain(sK1)))),
inference(forward_demodulation,[],[f8082,f37]) ).
fof(f8161,plain,
addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))) = addition(one,antidomain(multiplication(sK0,antidomain(sK1)))),
inference(forward_demodulation,[],[f8140,f79]) ).
fof(f8175,plain,
one = addition(antidomain(antidomain(sK2)),antidomain(multiplication(sK0,antidomain(sK1)))),
inference(forward_demodulation,[],[f8161,f512]) ).
fof(f8182,plain,
$false,
inference(forward_subsumption_resolution,[],[f8175,f424]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : KLE104+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.43 % Computer : n003.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Sun Sep 27 13:12:11 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.49 Running first-order theorem proving
% 0.22/0.49 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
% 19.63/3.67 % (520064)Detected formulas, will run a generic FOF schedule.
% 19.63/3.67 % (520071)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=2557887586:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 19.63/3.67 % (520077)dis-21_1_sil=8000:lcm=predicate:random_seed=3046753036: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)
% 19.63/3.67 % (520077)Refutation not found, incomplete strategy
% 19.63/3.67 % (520077)------------------------------
% 19.63/3.67 % (520077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520077)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520077)Termination reason: Refutation not found, incomplete strategy
% 19.63/3.67 % (520077)Time elapsed: 0.002 s
% 19.63/3.67 % (520077)Peak memory usage: 88 MB
% 19.63/3.67 % (520077)Instructions burned: 1 (million)
% 19.63/3.67 % (520076)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1978493268:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 19.63/3.67 % (520073)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=1383199579:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 19.63/3.67 % (520074)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=895800837:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 19.63/3.67 % (520075)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2750947368:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 19.63/3.67 % (520072)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=335004930:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 19.63/3.67 % (520074)Instruction limit reached!
% 19.63/3.67 % (520074)------------------------------
% 19.63/3.67 % (520074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520074)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520074)Termination reason: Instruction limit
% 19.63/3.67 % (520074)Termination phase: Saturation
% 19.63/3.67 % (520074)Time elapsed: 0.104 s
% 19.63/3.67 % (520074)Peak memory usage: 89 MB
% 19.63/3.67 % (520074)Instructions burned: 109 (million)
% 19.63/3.67 % (520075)Instruction limit reached!
% 19.63/3.67 % (520075)------------------------------
% 19.63/3.67 % (520075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520075)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520075)Termination reason: Instruction limit
% 19.63/3.67 % (520075)Termination phase: Saturation
% 19.63/3.67 % (520075)Time elapsed: 0.112 s
% 19.63/3.67 % (520075)Peak memory usage: 89 MB
% 19.63/3.67 % (520075)Instructions burned: 119 (million)
% 19.63/3.67 % (520076)Instruction limit reached!
% 19.63/3.67 % (520076)------------------------------
% 19.63/3.67 % (520076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520076)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520076)Termination reason: Instruction limit
% 19.63/3.67 % (520076)Termination phase: Saturation
% 19.63/3.67 % (520076)Time elapsed: 0.133 s
% 19.63/3.67 % (520076)Peak memory usage: 90 MB
% 19.63/3.67 % (520076)Instructions burned: 139 (million)
% 19.63/3.67 % (520077)------------------------------
% 19.63/3.67 % (520077)------------------------------
% 19.63/3.67 % (520088)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=3982794352:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 19.63/3.67 % (520086)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3349502603:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 19.63/3.67 % (520085)lrs+10_1_sil=8000:sp=occurrence:random_seed=4098921321:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 19.63/3.67 % (520087)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2369788012:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 19.63/3.67 % (520088)Instruction limit reached!
% 19.63/3.67 % (520088)------------------------------
% 19.63/3.67 % (520088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520088)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520088)Termination reason: Instruction limit
% 19.63/3.67 % (520088)Termination phase: Saturation
% 19.63/3.67 % (520088)Time elapsed: 0.134 s
% 19.63/3.67 % (520088)Peak memory usage: 92 MB
% 19.63/3.67 % (520088)Instructions burned: 250 (million)
% 19.63/3.67 % (520086)Instruction limit reached!
% 19.63/3.67 % (520086)------------------------------
% 19.63/3.67 % (520086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520086)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520086)Termination reason: Instruction limit
% 19.63/3.67 % (520086)Termination phase: Saturation
% 19.63/3.67 % (520086)Time elapsed: 0.149 s
% 19.63/3.67 % (520086)Peak memory usage: 90 MB
% 19.63/3.67 % (520086)Instructions burned: 157 (million)
% 19.63/3.67 % (520085)Instruction limit reached!
% 19.63/3.67 % (520085)------------------------------
% 19.63/3.67 % (520085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520085)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520085)Termination reason: Instruction limit
% 19.63/3.67 % (520085)Termination phase: Saturation
% 19.63/3.67 % (520085)Time elapsed: 0.275 s
% 19.63/3.67 % (520085)Peak memory usage: 92 MB
% 19.63/3.67 % (520085)Instructions burned: 286 (million)
% 19.63/3.67 % (520093)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3551037606:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 19.63/3.67 % (520087)Instruction limit reached!
% 19.63/3.67 % (520087)------------------------------
% 19.63/3.67 % (520087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520087)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520087)Termination reason: Instruction limit
% 19.63/3.67 % (520087)Termination phase: Saturation
% 19.63/3.67 % (520087)Time elapsed: 0.319 s
% 19.63/3.67 % (520087)Peak memory usage: 92 MB
% 19.63/3.67 % (520087)Instructions burned: 325 (million)
% 19.63/3.67 % (520094)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=580788446:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 19.63/3.67 % (520093)Instruction limit reached!
% 19.63/3.67 % (520093)------------------------------
% 19.63/3.67 % (520093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520093)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520093)Termination reason: Instruction limit
% 19.63/3.67 % (520093)Termination phase: Saturation
% 19.63/3.67 % (520093)Time elapsed: 0.154 s
% 19.63/3.67 % (520093)Peak memory usage: 90 MB
% 19.63/3.67 % (520093)Instructions burned: 296 (million)
% 19.63/3.67 % (520095)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4235253040:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 19.63/3.67 % (520097)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=497148596:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 19.63/3.67 % (520095)Instruction limit reached!
% 19.63/3.67 % (520095)------------------------------
% 19.63/3.67 % (520095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520095)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520095)Termination reason: Instruction limit
% 19.63/3.67 % (520095)Termination phase: Saturation
% 19.63/3.67 % (520095)Time elapsed: 0.109 s
% 19.63/3.67 % (520095)Peak memory usage: 90 MB
% 19.63/3.67 % (520095)Instructions burned: 113 (million)
% 19.63/3.67 % (520097)Refutation not found, incomplete strategy
% 19.63/3.67 % (520097)------------------------------
% 19.63/3.67 % (520097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520097)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520097)Termination reason: Refutation not found, incomplete strategy
% 19.63/3.67 % (520097)Time elapsed: 0.002 s
% 19.63/3.67 % (520097)Peak memory usage: 88 MB
% 19.63/3.67 % (520097)Instructions burned: 1 (million)
% 19.63/3.67 % (520099)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3650774886:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 19.63/3.67 % (520099)Instruction limit reached!
% 19.63/3.67 % (520099)------------------------------
% 19.63/3.67 % (520099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520099)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520099)Termination reason: Instruction limit
% 19.63/3.67 % (520099)Termination phase: Saturation
% 19.63/3.67 % (520099)Time elapsed: 0.101 s
% 19.63/3.67 % (520099)Peak memory usage: 88 MB
% 19.63/3.67 % (520099)Instructions burned: 115 (million)
% 19.63/3.67 % (520102)lrs+10_1_sil=8000:sp=occurrence:random_seed=2981203672:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 19.63/3.67 % (520097)------------------------------
% 19.63/3.67 % (520097)------------------------------
% 19.63/3.67 % (520104)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1843236828:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 19.63/3.67 % (520106)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3256843378:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 19.63/3.67 % (520104)Instruction limit reached!
% 19.63/3.67 % (520104)------------------------------
% 19.63/3.67 % (520104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520104)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520104)Termination reason: Instruction limit
% 19.63/3.67 % (520104)Termination phase: Saturation
% 19.63/3.67 % (520104)Time elapsed: 0.377 s
% 19.63/3.67 % (520104)Peak memory usage: 90 MB
% 19.63/3.67 % (520104)Instructions burned: 438 (million)
% 19.63/3.67 % (520102)Instruction limit reached!
% 19.63/3.67 % (520102)------------------------------
% 19.63/3.67 % (520102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520102)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520102)Termination reason: Instruction limit
% 19.63/3.67 % (520102)Termination phase: Saturation
% 19.63/3.67 % (520102)Time elapsed: 0.816 s
% 19.63/3.67 % (520102)Peak memory usage: 96 MB
% 19.63/3.67 % (520102)Instructions burned: 907 (million)
% 19.63/3.67 % (520072)First to succeed.
% 19.63/3.67 % (520072)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-520064"
% 19.63/3.67 % (520109)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1307086046:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 19.63/3.67 % (520109)Refutation not found, incomplete strategy
% 19.63/3.67 % (520109)------------------------------
% 19.63/3.67 % (520109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.63/3.67 % (520109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.63/3.67 % (520109)CaDiCaL version: 2.1.3
% 19.63/3.67 % (520109)Termination reason: Refutation not found, incomplete strategy
% 19.63/3.67 % (520109)Time elapsed: 0.003 s
% 19.63/3.67 % (520109)Peak memory usage: 89 MB
% 19.63/3.67 % (520109)Instructions burned: 1 (million)
% 19.63/3.67 % (520110)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=382294587:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 19.63/3.67 % (520109)------------------------------
% 19.63/3.67 % (520109)------------------------------
% 19.63/3.67 % (520072)Refutation found. Thanks to Tanya!
% 19.63/3.67 % SZS status Theorem for theBenchmark
% 19.63/3.67 % SZS output start Proof for theBenchmark
% See solution above
% 20.56/3.88 % (520072)------------------------------
% 20.56/3.88 % (520072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.56/3.88 % (520072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.56/3.88 % (520072)CaDiCaL version: 2.1.3
% 20.56/3.88 % (520072)Termination reason: Refutation
% 20.56/3.88 % (520072)Time elapsed: 2.159 s
% 20.56/3.88 % (520072)Peak memory usage: 140 MB
% 20.56/3.88 % (520072)Instructions burned: 2039 (million)
% 20.56/3.88 % (520072)------------------------------
% 20.56/3.88 % (520072)------------------------------
% 20.56/3.88 % (520064)Success in time 2.845 s
% 20.56/3.88 % Vampire exiting
%------------------------------------------------------------------------------