%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE122-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:23 AM UTC 2026
% Result : Unsatisfiable 117.42s 29.25s
% Output : Refutation 200.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 97
% Number of leaves : 53
% Syntax : Number of formulae : 731 ( 731 unt; 29 def)
% Number of atoms : 731 ( 730 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 44 ( 44 usr; 36 con; 0-3 aty)
% Number of variables : 429 ( 429 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_commutativity) ).
fof(f4,axiom,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(addition(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_associativity) ).
fof(f5,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_identity) ).
fof(f6,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_idempotence) ).
fof(f7,axiom,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_associativity) ).
fof(f8,negated_conjecture,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_right_identity) ).
fof(f9,negated_conjecture,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_left_identity) ).
fof(f10,axiom,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_distributivity) ).
fof(f11,axiom,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_distributivity) ).
fof(f12,axiom,
! [X0] : multiplication(X0,zero) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_annihilation) ).
fof(f13,plain,
! [X0] : zero = multiplication(X0,zero),
inference(reorient_equations,[],[f12]) ).
fof(f14,axiom,
! [X0] : multiplication(zero,X0) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_annihilation) ).
fof(f15,plain,
! [X0] : zero = multiplication(zero,X0),
inference(reorient_equations,[],[f14]) ).
fof(f19,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain1) ).
fof(f20,plain,
! [X0] : zero = multiplication(antidomain(X0),X0),
inference(reorient_equations,[],[f19]) ).
fof(f21,axiom,
! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain2) ).
fof(f22,plain,
! [X0,X1] : antidomain(multiplication(X0,antidomain(antidomain(X1)))) = addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(reorient_equations,[],[f21]) ).
fof(f23,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain3) ).
fof(f24,plain,
! [X0] : one = addition(antidomain(antidomain(X0)),antidomain(X0)),
inference(reorient_equations,[],[f23]) ).
fof(f25,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain4) ).
fof(f26,plain,
! [X0] : antidomain(antidomain(X0)) = domain(X0),
inference(reorient_equations,[],[f25]) ).
fof(f27,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain1) ).
fof(f28,plain,
! [X0] : zero = multiplication(X0,coantidomain(X0)),
inference(reorient_equations,[],[f27]) ).
fof(f29,axiom,
! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain2) ).
fof(f30,plain,
! [X0,X1] : coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)) = addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))),
inference(reorient_equations,[],[f29]) ).
fof(f31,axiom,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain3) ).
fof(f32,plain,
! [X0] : one = addition(coantidomain(coantidomain(X0)),coantidomain(X0)),
inference(reorient_equations,[],[f31]) ).
fof(f33,axiom,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain4) ).
fof(f34,plain,
! [X0] : coantidomain(coantidomain(X0)) = codomain(X0),
inference(reorient_equations,[],[f33]) ).
fof(f38,negated_conjecture,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backward_diamond) ).
fof(f41,negated_conjecture,
! [X2,X0,X1] : if_then_else(X0,X1,X2) = addition(multiplication(domain(X0),X1),multiplication(antidomain(X0),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',if_then_else_definition) ).
fof(f42,negated_conjecture,
addition(backward_diamond(sK5_goals_X1,multiplication(antidomain(sK4_goals_X2),domain(sK3_goals_X3))),domain(sK2_goals_X4)) = domain(sK2_goals_X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f43,plain,
domain(sK2_goals_X4) = addition(backward_diamond(sK5_goals_X1,multiplication(antidomain(sK4_goals_X2),domain(sK3_goals_X3))),domain(sK2_goals_X4)),
inference(reorient_equations,[],[f42]) ).
fof(f44,negated_conjecture,
addition(backward_diamond(sK1_goals_X0,multiplication(domain(sK4_goals_X2),domain(sK3_goals_X3))),domain(sK2_goals_X4)) = domain(sK2_goals_X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_1) ).
fof(f45,plain,
domain(sK2_goals_X4) = addition(backward_diamond(sK1_goals_X0,multiplication(domain(sK4_goals_X2),domain(sK3_goals_X3))),domain(sK2_goals_X4)),
inference(reorient_equations,[],[f44]) ).
fof(f46,negated_conjecture,
addition(backward_diamond(if_then_else(sK4_goals_X2,sK1_goals_X0,sK5_goals_X1),domain(sK3_goals_X3)),domain(sK2_goals_X4)) != domain(sK2_goals_X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_2) ).
fof(f47,plain,
domain(sK2_goals_X4) != addition(backward_diamond(if_then_else(sK4_goals_X2,sK1_goals_X0,sK5_goals_X1),domain(sK3_goals_X3)),domain(sK2_goals_X4)),
inference(reorient_equations,[],[f46]) ).
fof(f50,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f38,f34,f34]) ).
fof(f54,plain,
! [X2,X0,X1] : if_then_else(X0,X1,X2) = addition(multiplication(antidomain(antidomain(X0)),X1),multiplication(antidomain(X0),X2)),
inference(definition_unfolding,[],[f41,f26]) ).
fof(f55,plain,
antidomain(antidomain(sK2_goals_X4)) = addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(multiplication(antidomain(sK4_goals_X2),antidomain(antidomain(sK3_goals_X3))))),sK5_goals_X1))),antidomain(antidomain(sK2_goals_X4))),
inference(definition_unfolding,[],[f43,f26,f50,f26,f26]) ).
fof(f56,plain,
antidomain(antidomain(sK2_goals_X4)) = addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(multiplication(antidomain(antidomain(sK4_goals_X2)),antidomain(antidomain(sK3_goals_X3))))),sK1_goals_X0))),antidomain(antidomain(sK2_goals_X4))),
inference(definition_unfolding,[],[f45,f26,f50,f26,f26,f26]) ).
fof(f57,plain,
antidomain(antidomain(sK2_goals_X4)) != addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK3_goals_X3)))),addition(multiplication(antidomain(antidomain(sK4_goals_X2)),sK1_goals_X0),multiplication(antidomain(sK4_goals_X2),sK5_goals_X1))))),antidomain(antidomain(sK2_goals_X4))),
inference(definition_unfolding,[],[f47,f26,f50,f26,f54,f26]) ).
fof(f58,definition,
sF0 = antidomain(sK2_goals_X4),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f59,plain,
antidomain(sK2_goals_X4) = sF0,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF1 = antidomain(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f61,plain,
antidomain(sF0) = sF1,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF2 = antidomain(sK4_goals_X2),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f63,plain,
antidomain(sK4_goals_X2) = sF2,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF3 = antidomain(sK3_goals_X3),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f65,plain,
antidomain(sK3_goals_X3) = sF3,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF4 = antidomain(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f67,plain,
antidomain(sF3) = sF4,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF5 = multiplication(sF2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f69,plain,
multiplication(sF2,sF4) = sF5,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF6 = coantidomain(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f71,plain,
coantidomain(sF5) = sF6,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF7 = coantidomain(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f73,plain,
coantidomain(sF6) = sF7,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF8 = multiplication(sF7,sK5_goals_X1),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f75,plain,
multiplication(sF7,sK5_goals_X1) = sF8,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF9 = coantidomain(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f77,plain,
coantidomain(sF8) = sF9,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF10 = coantidomain(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f79,plain,
coantidomain(sF9) = sF10,
inference(reorient_equations,[],[f78]) ).
fof(f80,definition,
sF11 = addition(sF10,sF1),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f81,plain,
addition(sF10,sF1) = sF11,
inference(reorient_equations,[],[f80]) ).
fof(f82,plain,
sF1 = sF11,
inference(definition_folding,[],[f55,f81,f61,f59,f79,f77,f75,f73,f71,f69,f67,f65,f63,f61,f59]) ).
fof(f83,definition,
sF12 = antidomain(sF2),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f84,plain,
antidomain(sF2) = sF12,
inference(reorient_equations,[],[f83]) ).
fof(f85,definition,
sF13 = multiplication(sF12,sF4),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f86,plain,
multiplication(sF12,sF4) = sF13,
inference(reorient_equations,[],[f85]) ).
fof(f87,definition,
sF14 = coantidomain(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f88,plain,
coantidomain(sF13) = sF14,
inference(reorient_equations,[],[f87]) ).
fof(f89,definition,
sF15 = coantidomain(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f90,plain,
coantidomain(sF14) = sF15,
inference(reorient_equations,[],[f89]) ).
fof(f91,definition,
sF16 = multiplication(sF15,sK1_goals_X0),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f92,plain,
multiplication(sF15,sK1_goals_X0) = sF16,
inference(reorient_equations,[],[f91]) ).
fof(f93,definition,
sF17 = coantidomain(sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f94,plain,
coantidomain(sF16) = sF17,
inference(reorient_equations,[],[f93]) ).
fof(f95,definition,
sF18 = coantidomain(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f96,plain,
coantidomain(sF17) = sF18,
inference(reorient_equations,[],[f95]) ).
fof(f97,definition,
sF19 = addition(sF18,sF1),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f98,plain,
addition(sF18,sF1) = sF19,
inference(reorient_equations,[],[f97]) ).
fof(f99,plain,
sF1 = sF19,
inference(definition_folding,[],[f56,f98,f61,f59,f96,f94,f92,f90,f88,f86,f67,f65,f84,f63,f61,f59]) ).
fof(f100,definition,
sF20 = coantidomain(sF4),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f101,plain,
coantidomain(sF4) = sF20,
inference(reorient_equations,[],[f100]) ).
fof(f102,definition,
sF21 = coantidomain(sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f103,plain,
coantidomain(sF20) = sF21,
inference(reorient_equations,[],[f102]) ).
fof(f104,definition,
sF22 = multiplication(sF12,sK1_goals_X0),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f105,plain,
multiplication(sF12,sK1_goals_X0) = sF22,
inference(reorient_equations,[],[f104]) ).
fof(f106,definition,
sF23 = multiplication(sF2,sK5_goals_X1),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f107,plain,
multiplication(sF2,sK5_goals_X1) = sF23,
inference(reorient_equations,[],[f106]) ).
fof(f108,definition,
sF24 = addition(sF22,sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f109,plain,
addition(sF22,sF23) = sF24,
inference(reorient_equations,[],[f108]) ).
fof(f110,definition,
sF25 = multiplication(sF21,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f111,plain,
multiplication(sF21,sF24) = sF25,
inference(reorient_equations,[],[f110]) ).
fof(f112,definition,
sF26 = coantidomain(sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f113,plain,
coantidomain(sF25) = sF26,
inference(reorient_equations,[],[f112]) ).
fof(f114,definition,
sF27 = coantidomain(sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f115,plain,
coantidomain(sF26) = sF27,
inference(reorient_equations,[],[f114]) ).
fof(f116,definition,
sF28 = addition(sF27,sF1),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f117,plain,
addition(sF27,sF1) = sF28,
inference(reorient_equations,[],[f116]) ).
fof(f118,plain,
sF1 != sF28,
inference(definition_folding,[],[f57,f117,f61,f59,f115,f113,f111,f109,f107,f63,f105,f84,f63,f103,f101,f67,f65,f61,f59]) ).
fof(f119,plain,
! [X0] : one = addition(antidomain(X0),antidomain(antidomain(X0))),
inference(backward_demodulation,[],[f24,f3]) ).
fof(f120,plain,
! [X0] : one = addition(coantidomain(X0),coantidomain(coantidomain(X0))),
inference(backward_demodulation,[],[f32,f3]) ).
fof(f121,plain,
sF1 = addition(sF10,sF1),
inference(forward_demodulation,[],[f81,f82]) ).
fof(f122,plain,
sF1 = addition(sF18,sF1),
inference(forward_demodulation,[],[f98,f99]) ).
fof(f141,plain,
zero = multiplication(sF4,sF20),
inference(superposition,[],[f28,f101]) ).
fof(f143,plain,
zero = multiplication(sF6,sF7),
inference(superposition,[],[f28,f73]) ).
fof(f153,plain,
! [X0,X1] : multiplication(X0,addition(X1,coantidomain(X0))) = addition(multiplication(X0,X1),zero),
inference(superposition,[],[f10,f28]) ).
fof(f154,plain,
! [X0,X1] : multiplication(X0,addition(coantidomain(X0),X1)) = addition(zero,multiplication(X0,X1)),
inference(superposition,[],[f10,f28]) ).
fof(f158,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(X0,addition(X1,coantidomain(X0))),
inference(forward_demodulation,[],[f153,f5]) ).
fof(f160,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = addition(multiplication(X0,coantidomain(X1)),zero),
inference(superposition,[],[f11,f28]) ).
fof(f165,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = multiplication(X0,coantidomain(X1)),
inference(forward_demodulation,[],[f160,f5]) ).
fof(f204,plain,
zero = multiplication(sF12,sF2),
inference(superposition,[],[f20,f84]) ).
fof(f206,plain,
! [X0,X1] : addition(multiplication(X0,X1),zero) = multiplication(addition(X0,antidomain(X1)),X1),
inference(superposition,[],[f11,f20]) ).
fof(f207,plain,
! [X0,X1] : multiplication(addition(antidomain(X0),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(superposition,[],[f11,f20]) ).
fof(f208,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X1,X0)) = addition(multiplication(antidomain(X0),X1),zero),
inference(superposition,[],[f10,f20]) ).
fof(f209,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X0,X1)) = addition(zero,multiplication(antidomain(X0),X1)),
inference(superposition,[],[f10,f20]) ).
fof(f211,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X1,X0)) = multiplication(antidomain(X0),X1),
inference(forward_demodulation,[],[f208,f5]) ).
fof(f212,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(addition(X0,antidomain(X1)),X1),
inference(forward_demodulation,[],[f206,f5]) ).
fof(f214,plain,
! [X0] : multiplication(addition(sF2,X0),sF4) = addition(sF5,multiplication(X0,sF4)),
inference(superposition,[],[f11,f69]) ).
fof(f232,plain,
! [X0] : multiplication(sF7,addition(sK5_goals_X1,X0)) = addition(sF8,multiplication(sF7,X0)),
inference(superposition,[],[f10,f75]) ).
fof(f238,plain,
! [X0] : multiplication(addition(sF2,X0),sK5_goals_X1) = addition(sF23,multiplication(X0,sK5_goals_X1)),
inference(superposition,[],[f11,f107]) ).
fof(f246,plain,
! [X0] : multiplication(sF15,addition(X0,sK1_goals_X0)) = addition(multiplication(sF15,X0),sF16),
inference(superposition,[],[f10,f92]) ).
fof(f247,plain,
! [X0] : multiplication(sF15,addition(sK1_goals_X0,X0)) = addition(sF16,multiplication(sF15,X0)),
inference(superposition,[],[f10,f92]) ).
fof(f250,plain,
! [X0] : multiplication(sF15,addition(X0,sK1_goals_X0)) = addition(sF16,multiplication(sF15,X0)),
inference(forward_demodulation,[],[f246,f3]) ).
fof(f253,plain,
! [X0] : antidomain(multiplication(X0,antidomain(antidomain(coantidomain(X0))))) = addition(antidomain(zero),antidomain(multiplication(X0,antidomain(antidomain(coantidomain(X0)))))),
inference(superposition,[],[f22,f28]) ).
fof(f278,plain,
! [X0] : multiplication(addition(sF21,X0),sF24) = addition(sF25,multiplication(X0,sF24)),
inference(superposition,[],[f11,f111]) ).
fof(f279,plain,
! [X0] : multiplication(sF21,addition(X0,sF24)) = addition(multiplication(sF21,X0),sF25),
inference(superposition,[],[f10,f111]) ).
fof(f283,plain,
! [X0] : multiplication(sF21,addition(X0,sF24)) = addition(sF25,multiplication(sF21,X0)),
inference(forward_demodulation,[],[f279,f3]) ).
fof(f287,plain,
! [X0] : multiplication(addition(sF12,X0),sK1_goals_X0) = addition(sF22,multiplication(X0,sK1_goals_X0)),
inference(superposition,[],[f11,f105]) ).
fof(f319,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X0)) = multiplication(X1,coantidomain(X0)),
inference(superposition,[],[f165,f3]) ).
fof(f320,plain,
! [X2,X0,X1] : addition(multiplication(X0,X1),multiplication(X0,X2)) = multiplication(X0,addition(X2,X1)),
inference(superposition,[],[f10,f3]) ).
fof(f321,plain,
! [X2,X0,X1] : addition(multiplication(X0,X1),multiplication(X2,X1)) = multiplication(addition(X2,X0),X1),
inference(superposition,[],[f11,f3]) ).
fof(f357,plain,
! [X0,X1] : multiplication(X1,X0) = multiplication(addition(antidomain(X0),X1),X0),
inference(superposition,[],[f212,f3]) ).
fof(f371,plain,
! [X0,X1] : multiplication(X1,X0) = addition(zero,multiplication(X1,X0)),
inference(backward_demodulation,[],[f207,f357]) ).
fof(f373,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(X0,addition(coantidomain(X0),X1)),
inference(backward_demodulation,[],[f154,f371]) ).
fof(f374,plain,
! [X0,X1] : multiplication(antidomain(X0),X1) = multiplication(antidomain(X0),addition(X0,X1)),
inference(backward_demodulation,[],[f209,f371]) ).
fof(f377,plain,
zero = antidomain(one),
inference(superposition,[],[f20,f8]) ).
fof(f393,plain,
! [X0,X1] : multiplication(X0,addition(X1,one)) = addition(multiplication(X0,X1),X0),
inference(superposition,[],[f10,f8]) ).
fof(f394,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(superposition,[],[f10,f8]) ).
fof(f401,plain,
! [X0,X1] : multiplication(X0,addition(X1,one)) = addition(X0,multiplication(X0,X1)),
inference(forward_demodulation,[],[f393,f3]) ).
fof(f447,plain,
! [X0] : addition(zero,X0) = X0,
inference(superposition,[],[f3,f5]) ).
fof(f449,plain,
! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X1,addition(X0,X2)),
inference(superposition,[],[f4,f3]) ).
fof(f452,plain,
! [X2,X3,X0,X1] : addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)) = addition(multiplication(X0,addition(X1,X2)),X3),
inference(superposition,[],[f4,f10]) ).
fof(f464,plain,
! [X0] : addition(sF24,X0) = addition(sF22,addition(sF23,X0)),
inference(superposition,[],[f4,f109]) ).
fof(f470,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(superposition,[],[f3,f4]) ).
fof(f476,plain,
one = addition(sF2,antidomain(sF2)),
inference(superposition,[],[f119,f63]) ).
fof(f477,plain,
one = addition(sF3,antidomain(sF3)),
inference(superposition,[],[f119,f65]) ).
fof(f478,plain,
one = addition(sF0,antidomain(sF0)),
inference(superposition,[],[f119,f59]) ).
fof(f487,plain,
one = addition(sF0,sF1),
inference(forward_demodulation,[],[f478,f61]) ).
fof(f488,plain,
one = addition(sF3,sF4),
inference(forward_demodulation,[],[f477,f67]) ).
fof(f489,plain,
one = addition(sF2,sF12),
inference(forward_demodulation,[],[f476,f84]) ).
fof(f490,plain,
one = addition(sF4,sF3),
inference(forward_demodulation,[],[f488,f3]) ).
fof(f491,plain,
! [X0,X1] : multiplication(antidomain(X0),multiplication(X0,X1)) = multiplication(zero,X1),
inference(superposition,[],[f7,f20]) ).
fof(f501,plain,
! [X0] : multiplication(sF5,X0) = multiplication(sF2,multiplication(sF4,X0)),
inference(superposition,[],[f7,f69]) ).
fof(f502,plain,
! [X0] : multiplication(sF13,X0) = multiplication(sF12,multiplication(sF4,X0)),
inference(superposition,[],[f7,f86]) ).
fof(f503,plain,
! [X0] : multiplication(sF25,X0) = multiplication(sF21,multiplication(sF24,X0)),
inference(superposition,[],[f7,f111]) ).
fof(f511,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,[],[f30,f7]) ).
fof(f523,plain,
! [X0,X1] : zero = multiplication(antidomain(X0),multiplication(X0,X1)),
inference(forward_demodulation,[],[f491,f15]) ).
fof(f530,plain,
one = addition(sF6,coantidomain(sF6)),
inference(superposition,[],[f120,f71]) ).
fof(f532,plain,
one = addition(sF9,coantidomain(sF9)),
inference(superposition,[],[f120,f77]) ).
fof(f534,plain,
one = addition(sF14,coantidomain(sF14)),
inference(superposition,[],[f120,f88]) ).
fof(f542,plain,
! [X0] : multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))) = multiplication(one,coantidomain(coantidomain(coantidomain(X0)))),
inference(superposition,[],[f165,f120]) ).
fof(f543,plain,
! [X0] : coantidomain(coantidomain(coantidomain(X0))) = multiplication(coantidomain(X0),coantidomain(coantidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f542,f9]) ).
fof(f546,plain,
one = addition(sF14,sF15),
inference(forward_demodulation,[],[f534,f90]) ).
fof(f547,plain,
one = addition(sF9,sF10),
inference(forward_demodulation,[],[f532,f79]) ).
fof(f548,plain,
one = addition(sF6,sF7),
inference(forward_demodulation,[],[f530,f73]) ).
fof(f555,plain,
! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)),
inference(superposition,[],[f11,f9]) ).
fof(f559,plain,
zero = coantidomain(one),
inference(superposition,[],[f28,f9]) ).
fof(f581,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,[],[f158,f30]) ).
fof(f641,plain,
! [X0,X1] : zero = multiplication(multiplication(coantidomain(coantidomain(X0)),X1),coantidomain(multiplication(X0,X1))),
inference(forward_demodulation,[],[f581,f28]) ).
fof(f651,plain,
! [X0,X1] : zero = multiplication(coantidomain(coantidomain(X0)),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f641,f7]) ).
fof(f689,plain,
multiplication(addition(one,sF2),sK5_goals_X1) = addition(sK5_goals_X1,sF23),
inference(superposition,[],[f555,f107]) ).
fof(f691,plain,
multiplication(addition(one,sF12),sK1_goals_X0) = addition(sK1_goals_X0,sF22),
inference(superposition,[],[f555,f105]) ).
fof(f692,plain,
multiplication(addition(one,sF2),sF4) = addition(sF4,sF5),
inference(superposition,[],[f555,f69]) ).
fof(f693,plain,
multiplication(addition(one,sF12),sF4) = addition(sF4,sF13),
inference(superposition,[],[f555,f86]) ).
fof(f705,plain,
addition(sF4,sF13) = multiplication(addition(sF12,one),sF4),
inference(forward_demodulation,[],[f693,f3]) ).
fof(f706,plain,
addition(sF4,sF5) = multiplication(addition(sF2,one),sF4),
inference(forward_demodulation,[],[f692,f3]) ).
fof(f707,plain,
multiplication(addition(one,sF12),sK1_goals_X0) = addition(sF22,sK1_goals_X0),
inference(forward_demodulation,[],[f691,f3]) ).
fof(f709,plain,
multiplication(addition(one,sF2),sK5_goals_X1) = addition(sF23,sK5_goals_X1),
inference(forward_demodulation,[],[f689,f3]) ).
fof(f719,plain,
addition(sF22,sK1_goals_X0) = multiplication(addition(sF12,one),sK1_goals_X0),
inference(forward_demodulation,[],[f707,f3]) ).
fof(f721,plain,
addition(sF23,sK5_goals_X1) = multiplication(addition(sF2,one),sK5_goals_X1),
inference(forward_demodulation,[],[f709,f3]) ).
fof(f738,plain,
! [X2,X0,X1] : multiplication(antidomain(multiplication(X0,X2)),multiplication(X0,X1)) = multiplication(antidomain(multiplication(X0,X2)),multiplication(X0,addition(X1,X2))),
inference(superposition,[],[f211,f10]) ).
fof(f753,plain,
multiplication(antidomain(sF1),sF27) = multiplication(antidomain(sF1),sF28),
inference(superposition,[],[f211,f117]) ).
fof(f820,plain,
! [X0] : multiplication(antidomain(coantidomain(X0)),coantidomain(coantidomain(X0))) = multiplication(antidomain(coantidomain(X0)),one),
inference(superposition,[],[f374,f120]) ).
fof(f840,plain,
! [X0] : antidomain(coantidomain(X0)) = multiplication(antidomain(coantidomain(X0)),coantidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f820,f8]) ).
fof(f848,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f4,f6]) ).
fof(f854,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,addition(X0,X1)),
inference(superposition,[],[f848,f3]) ).
fof(f862,plain,
! [X0] : one = addition(antidomain(X0),one),
inference(superposition,[],[f848,f119]) ).
fof(f870,plain,
! [X0] : one = addition(coantidomain(X0),one),
inference(superposition,[],[f848,f120]) ).
fof(f877,plain,
! [X0,X1] : multiplication(X0,coantidomain(addition(X0,X1))) = multiplication(addition(X0,X1),coantidomain(addition(X0,X1))),
inference(superposition,[],[f165,f848]) ).
fof(f882,plain,
! [X0,X1] : zero = multiplication(X0,coantidomain(addition(X0,X1))),
inference(forward_demodulation,[],[f877,f28]) ).
fof(f885,plain,
! [X0] : one = addition(one,coantidomain(X0)),
inference(forward_demodulation,[],[f870,f3]) ).
fof(f886,plain,
! [X0] : one = addition(one,antidomain(X0)),
inference(forward_demodulation,[],[f862,f3]) ).
fof(f1112,plain,
multiplication(addition(sF2,sF7),sK5_goals_X1) = addition(sF23,sF8),
inference(superposition,[],[f238,f75]) ).
fof(f1132,plain,
multiplication(addition(sF2,sF7),sK5_goals_X1) = addition(sF8,sF23),
inference(forward_demodulation,[],[f1112,f3]) ).
fof(f1157,plain,
zero = multiplication(antidomain(sF2),sF23),
inference(superposition,[],[f523,f107]) ).
fof(f1159,plain,
zero = multiplication(antidomain(sF12),sF22),
inference(superposition,[],[f523,f105]) ).
fof(f1178,plain,
zero = multiplication(sF12,sF23),
inference(forward_demodulation,[],[f1157,f84]) ).
fof(f1206,plain,
multiplication(addition(sF12,sF15),sK1_goals_X0) = addition(sF22,sF16),
inference(superposition,[],[f287,f92]) ).
fof(f1226,plain,
multiplication(addition(sF12,sF15),sK1_goals_X0) = addition(sF16,sF22),
inference(forward_demodulation,[],[f1206,f3]) ).
fof(f1266,plain,
! [X0,X1] : multiplication(addition(X0,X1),addition(one,coantidomain(X1))) = addition(addition(X0,X1),multiplication(X0,coantidomain(X1))),
inference(superposition,[],[f394,f165]) ).
fof(f1272,plain,
multiplication(sF2,addition(one,sF4)) = addition(sF2,sF5),
inference(superposition,[],[f394,f69]) ).
fof(f1273,plain,
multiplication(sF12,addition(one,sF4)) = addition(sF12,sF13),
inference(superposition,[],[f394,f86]) ).
fof(f1308,plain,
addition(sF12,sF13) = multiplication(sF12,addition(sF4,one)),
inference(forward_demodulation,[],[f1273,f3]) ).
fof(f1309,plain,
addition(sF2,sF5) = multiplication(sF2,addition(sF4,one)),
inference(forward_demodulation,[],[f1272,f3]) ).
fof(f1311,plain,
! [X0,X1] : multiplication(addition(X0,X1),addition(one,coantidomain(X1))) = addition(X0,addition(X1,multiplication(X0,coantidomain(X1)))),
inference(forward_demodulation,[],[f1266,f4]) ).
fof(f1327,plain,
! [X0,X1] : multiplication(addition(X0,X1),one) = addition(X0,addition(X1,multiplication(X0,coantidomain(X1)))),
inference(forward_demodulation,[],[f1311,f885]) ).
fof(f1338,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X1,multiplication(X0,coantidomain(X1)))),
inference(forward_demodulation,[],[f1327,f8]) ).
fof(f1450,plain,
! [X0] : addition(one,X0) = addition(sF2,addition(sF12,X0)),
inference(superposition,[],[f4,f489]) ).
fof(f1451,plain,
multiplication(sF2,coantidomain(sF12)) = multiplication(one,coantidomain(sF12)),
inference(superposition,[],[f165,f489]) ).
fof(f1452,plain,
multiplication(antidomain(sF12),sF2) = multiplication(antidomain(sF12),one),
inference(superposition,[],[f211,f489]) ).
fof(f1454,plain,
! [X0] : addition(one,X0) = addition(sF12,addition(sF2,X0)),
inference(superposition,[],[f449,f489]) ).
fof(f1457,plain,
one = addition(sF2,one),
inference(superposition,[],[f848,f489]) ).
fof(f1458,plain,
addition(sF23,sK5_goals_X1) = multiplication(one,sK5_goals_X1),
inference(backward_demodulation,[],[f721,f1457]) ).
fof(f1459,plain,
addition(sF4,sF5) = multiplication(one,sF4),
inference(backward_demodulation,[],[f706,f1457]) ).
fof(f1461,plain,
! [X0] : addition(one,X0) = addition(sF2,addition(X0,sF12)),
inference(forward_demodulation,[],[f1454,f470]) ).
fof(f1463,plain,
antidomain(sF12) = multiplication(antidomain(sF12),sF2),
inference(forward_demodulation,[],[f1452,f8]) ).
fof(f1464,plain,
coantidomain(sF12) = multiplication(sF2,coantidomain(sF12)),
inference(forward_demodulation,[],[f1451,f9]) ).
fof(f1465,plain,
sF4 = addition(sF4,sF5),
inference(forward_demodulation,[],[f1459,f9]) ).
fof(f1466,plain,
sK5_goals_X1 = addition(sF23,sK5_goals_X1),
inference(forward_demodulation,[],[f1458,f9]) ).
fof(f1500,plain,
! [X0] : zero = multiplication(coantidomain(coantidomain(antidomain(X0))),multiplication(X0,coantidomain(zero))),
inference(superposition,[],[f651,f20]) ).
fof(f1530,plain,
! [X2,X0,X1] : multiplication(addition(coantidomain(coantidomain(X0)),X1),multiplication(X2,coantidomain(multiplication(X0,X2)))) = addition(zero,multiplication(X1,multiplication(X2,coantidomain(multiplication(X0,X2))))),
inference(superposition,[],[f11,f651]) ).
fof(f1538,plain,
! [X2,X0,X1] : multiplication(addition(coantidomain(coantidomain(X0)),X1),multiplication(X2,coantidomain(multiplication(X0,X2)))) = multiplication(X1,multiplication(X2,coantidomain(multiplication(X0,X2)))),
inference(forward_demodulation,[],[f1530,f447]) ).
fof(f1619,plain,
multiplication(sF0,coantidomain(sF1)) = multiplication(one,coantidomain(sF1)),
inference(superposition,[],[f165,f487]) ).
fof(f1620,plain,
multiplication(antidomain(sF1),sF0) = multiplication(antidomain(sF1),one),
inference(superposition,[],[f211,f487]) ).
fof(f1622,plain,
! [X0] : addition(one,X0) = addition(sF1,addition(sF0,X0)),
inference(superposition,[],[f449,f487]) ).
fof(f1627,plain,
! [X0] : addition(one,X0) = addition(sF0,addition(X0,sF1)),
inference(forward_demodulation,[],[f1622,f470]) ).
fof(f1629,plain,
antidomain(sF1) = multiplication(antidomain(sF1),sF0),
inference(forward_demodulation,[],[f1620,f8]) ).
fof(f1630,plain,
coantidomain(sF1) = multiplication(sF0,coantidomain(sF1)),
inference(forward_demodulation,[],[f1619,f9]) ).
fof(f1633,plain,
one = addition(one,sF3),
inference(superposition,[],[f886,f65]) ).
fof(f1636,plain,
one = addition(one,sF12),
inference(superposition,[],[f886,f84]) ).
fof(f1637,plain,
one = addition(one,sF4),
inference(superposition,[],[f886,f67]) ).
fof(f1648,plain,
one = addition(sF4,one),
inference(forward_demodulation,[],[f1637,f3]) ).
fof(f1649,plain,
one = addition(sF12,one),
inference(forward_demodulation,[],[f1636,f3]) ).
fof(f1652,plain,
one = addition(sF3,one),
inference(forward_demodulation,[],[f1633,f3]) ).
fof(f1655,plain,
addition(sF2,sF5) = multiplication(sF2,one),
inference(backward_demodulation,[],[f1309,f1648]) ).
fof(f1656,plain,
addition(sF12,sF13) = multiplication(sF12,one),
inference(backward_demodulation,[],[f1308,f1648]) ).
fof(f1657,plain,
addition(sF22,sK1_goals_X0) = multiplication(one,sK1_goals_X0),
inference(backward_demodulation,[],[f719,f1649]) ).
fof(f1658,plain,
addition(sF4,sF13) = multiplication(one,sF4),
inference(backward_demodulation,[],[f705,f1649]) ).
fof(f1659,plain,
sF12 = addition(sF12,sF13),
inference(forward_demodulation,[],[f1656,f8]) ).
fof(f1660,plain,
sF2 = addition(sF2,sF5),
inference(forward_demodulation,[],[f1655,f8]) ).
fof(f1661,plain,
sF4 = addition(sF4,sF13),
inference(forward_demodulation,[],[f1658,f9]) ).
fof(f1662,plain,
sK1_goals_X0 = addition(sF22,sK1_goals_X0),
inference(forward_demodulation,[],[f1657,f9]) ).
fof(f1667,plain,
! [X0] : addition(sK1_goals_X0,X0) = addition(sK1_goals_X0,addition(sF22,X0)),
inference(superposition,[],[f449,f1662]) ).
fof(f1672,plain,
! [X0] : addition(sK1_goals_X0,X0) = addition(sF22,addition(X0,sK1_goals_X0)),
inference(forward_demodulation,[],[f1667,f470]) ).
fof(f1676,plain,
one = addition(one,sF20),
inference(superposition,[],[f885,f101]) ).
fof(f1677,plain,
one = addition(one,sF6),
inference(superposition,[],[f885,f71]) ).
fof(f1678,plain,
one = addition(one,sF7),
inference(superposition,[],[f885,f73]) ).
fof(f1687,plain,
one = addition(one,sF27),
inference(superposition,[],[f885,f115]) ).
fof(f1698,plain,
one = addition(sF27,one),
inference(forward_demodulation,[],[f1687,f3]) ).
fof(f1707,plain,
one = addition(sF7,one),
inference(forward_demodulation,[],[f1678,f3]) ).
fof(f1708,plain,
one = addition(sF6,one),
inference(forward_demodulation,[],[f1677,f3]) ).
fof(f1709,plain,
one = addition(sF20,one),
inference(forward_demodulation,[],[f1676,f3]) ).
fof(f1802,plain,
multiplication(addition(sF2,sF12),sF4) = addition(sF5,sF13),
inference(superposition,[],[f214,f86]) ).
fof(f1828,plain,
multiplication(one,sF4) = addition(sF5,sF13),
inference(forward_demodulation,[],[f1802,f489]) ).
fof(f1835,plain,
sF4 = addition(sF5,sF13),
inference(forward_demodulation,[],[f1828,f9]) ).
fof(f1847,plain,
! [X0] : addition(sF4,X0) = addition(sF13,addition(sF5,X0)),
inference(superposition,[],[f449,f1835]) ).
fof(f1853,plain,
! [X0] : addition(sF4,X0) = addition(sF5,addition(X0,sF13)),
inference(forward_demodulation,[],[f1847,f470]) ).
fof(f1905,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = multiplication(X0,addition(X2,X1)),
inference(superposition,[],[f10,f320]) ).
fof(f2189,plain,
! [X0] : multiplication(X0,one) = multiplication(X0,coantidomain(coantidomain(X0))),
inference(superposition,[],[f373,f120]) ).
fof(f2265,plain,
! [X0] : multiplication(X0,coantidomain(coantidomain(X0))) = X0,
inference(forward_demodulation,[],[f2189,f8]) ).
fof(f2273,plain,
! [X0] : coantidomain(X0) = coantidomain(coantidomain(coantidomain(X0))),
inference(backward_demodulation,[],[f543,f2265]) ).
fof(f2306,plain,
sF4 = multiplication(sF4,coantidomain(sF20)),
inference(superposition,[],[f2265,f101]) ).
fof(f2307,plain,
sF5 = multiplication(sF5,coantidomain(sF6)),
inference(superposition,[],[f2265,f71]) ).
fof(f2311,plain,
sF13 = multiplication(sF13,coantidomain(sF14)),
inference(superposition,[],[f2265,f88]) ).
fof(f2313,plain,
sF16 = multiplication(sF16,coantidomain(sF17)),
inference(superposition,[],[f2265,f94]) ).
fof(f2320,plain,
one = coantidomain(coantidomain(one)),
inference(superposition,[],[f9,f2265]) ).
fof(f2379,plain,
one = coantidomain(zero),
inference(forward_demodulation,[],[f2320,f559]) ).
fof(f2382,plain,
sF16 = multiplication(sF16,sF18),
inference(forward_demodulation,[],[f2313,f96]) ).
fof(f2383,plain,
sF13 = multiplication(sF13,sF15),
inference(forward_demodulation,[],[f2311,f90]) ).
fof(f2385,plain,
sF5 = multiplication(sF5,sF7),
inference(forward_demodulation,[],[f2307,f73]) ).
fof(f2386,plain,
sF4 = multiplication(sF4,sF21),
inference(forward_demodulation,[],[f2306,f103]) ).
fof(f2428,plain,
! [X0] : zero = multiplication(coantidomain(coantidomain(antidomain(X0))),multiplication(X0,one)),
inference(backward_demodulation,[],[f1500,f2379]) ).
fof(f2455,plain,
! [X0] : zero = multiplication(coantidomain(coantidomain(antidomain(X0))),X0),
inference(forward_demodulation,[],[f2428,f8]) ).
fof(f2485,plain,
sF6 = coantidomain(coantidomain(sF6)),
inference(superposition,[],[f2273,f71]) ).
fof(f2489,plain,
sF14 = coantidomain(coantidomain(sF14)),
inference(superposition,[],[f2273,f88]) ).
fof(f2530,plain,
sF14 = coantidomain(sF15),
inference(forward_demodulation,[],[f2489,f90]) ).
fof(f2537,plain,
sF6 = coantidomain(sF7),
inference(forward_demodulation,[],[f2485,f73]) ).
fof(f3182,plain,
multiplication(sF4,coantidomain(sF3)) = multiplication(one,coantidomain(sF3)),
inference(superposition,[],[f165,f490]) ).
fof(f3184,plain,
multiplication(antidomain(sF4),sF3) = multiplication(antidomain(sF4),one),
inference(superposition,[],[f374,f490]) ).
fof(f3193,plain,
antidomain(sF4) = multiplication(antidomain(sF4),sF3),
inference(forward_demodulation,[],[f3184,f8]) ).
fof(f3195,plain,
coantidomain(sF3) = multiplication(sF4,coantidomain(sF3)),
inference(forward_demodulation,[],[f3182,f9]) ).
fof(f3571,plain,
! [X0] : multiplication(X0,sF2) = multiplication(addition(sF12,X0),sF2),
inference(superposition,[],[f357,f84]) ).
fof(f3573,plain,
! [X0] : multiplication(one,X0) = multiplication(antidomain(antidomain(X0)),X0),
inference(superposition,[],[f357,f119]) ).
fof(f3636,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f3573,f9]) ).
fof(f3666,plain,
sF0 = multiplication(antidomain(sF1),sF0),
inference(superposition,[],[f3636,f61]) ).
fof(f3667,plain,
sF2 = multiplication(antidomain(sF12),sF2),
inference(superposition,[],[f3636,f84]) ).
fof(f3668,plain,
sF3 = multiplication(antidomain(sF4),sF3),
inference(superposition,[],[f3636,f67]) ).
fof(f3670,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(antidomain(antidomain(X0)),multiplication(X0,X1)),
inference(superposition,[],[f7,f3636]) ).
fof(f3687,plain,
one = antidomain(antidomain(one)),
inference(superposition,[],[f8,f3636]) ).
fof(f3702,plain,
one = antidomain(zero),
inference(forward_demodulation,[],[f3687,f377]) ).
fof(f3714,plain,
sF3 = antidomain(sF4),
inference(backward_demodulation,[],[f3193,f3668]) ).
fof(f3715,plain,
sF2 = antidomain(sF12),
inference(backward_demodulation,[],[f1463,f3667]) ).
fof(f3716,plain,
sF0 = antidomain(sF1),
inference(backward_demodulation,[],[f1629,f3666]) ).
fof(f3724,plain,
! [X0] : antidomain(multiplication(X0,antidomain(antidomain(coantidomain(X0))))) = addition(one,antidomain(multiplication(X0,antidomain(antidomain(coantidomain(X0)))))),
inference(backward_demodulation,[],[f253,f3702]) ).
fof(f3742,plain,
zero = multiplication(sF2,sF22),
inference(backward_demodulation,[],[f1159,f3715]) ).
fof(f3749,plain,
multiplication(sF0,sF27) = multiplication(sF0,sF28),
inference(backward_demodulation,[],[f753,f3716]) ).
fof(f3760,plain,
! [X0] : one = antidomain(multiplication(X0,antidomain(antidomain(coantidomain(X0))))),
inference(forward_demodulation,[],[f3724,f886]) ).
fof(f3792,plain,
! [X0] : multiplication(sF0,X0) = multiplication(sF0,addition(sF1,X0)),
inference(superposition,[],[f374,f3716]) ).
fof(f3801,plain,
zero = multiplication(sF2,sF12),
inference(superposition,[],[f20,f3715]) ).
fof(f3806,plain,
! [X0] : multiplication(X0,sF12) = multiplication(addition(sF2,X0),sF12),
inference(superposition,[],[f357,f3715]) ).
fof(f3807,plain,
! [X0] : multiplication(sF2,X0) = multiplication(sF2,addition(sF12,X0)),
inference(superposition,[],[f374,f3715]) ).
fof(f4308,plain,
multiplication(sF2,sF12) = multiplication(sF5,sF12),
inference(superposition,[],[f3806,f1660]) ).
fof(f4320,plain,
zero = multiplication(sF5,sF12),
inference(forward_demodulation,[],[f4308,f3801]) ).
fof(f4819,plain,
multiplication(addition(one,sF5),sF7) = addition(sF7,sF5),
inference(superposition,[],[f555,f2385]) ).
fof(f4825,plain,
multiplication(addition(one,sF5),sF7) = addition(sF5,sF7),
inference(forward_demodulation,[],[f4819,f3]) ).
fof(f4838,plain,
addition(sF5,sF7) = multiplication(addition(sF5,one),sF7),
inference(forward_demodulation,[],[f4825,f3]) ).
fof(f5352,plain,
zero = multiplication(coantidomain(coantidomain(sF5)),multiplication(sF12,coantidomain(zero))),
inference(superposition,[],[f651,f4320]) ).
fof(f5357,plain,
zero = multiplication(coantidomain(coantidomain(sF5)),multiplication(sF12,one)),
inference(forward_demodulation,[],[f5352,f2379]) ).
fof(f5376,plain,
zero = multiplication(coantidomain(coantidomain(sF5)),sF12),
inference(forward_demodulation,[],[f5357,f8]) ).
fof(f5387,plain,
zero = multiplication(coantidomain(sF6),sF12),
inference(forward_demodulation,[],[f5376,f71]) ).
fof(f5394,plain,
zero = multiplication(sF7,sF12),
inference(forward_demodulation,[],[f5387,f73]) ).
fof(f5403,plain,
! [X0] : addition(multiplication(X0,sF12),zero) = multiplication(addition(X0,sF7),sF12),
inference(superposition,[],[f11,f5394]) ).
fof(f5431,plain,
! [X0] : multiplication(X0,sF12) = multiplication(addition(X0,sF7),sF12),
inference(forward_demodulation,[],[f5403,f5]) ).
fof(f5590,plain,
multiplication(one,sF12) = multiplication(sF6,sF12),
inference(superposition,[],[f5431,f548]) ).
fof(f5633,plain,
sF12 = multiplication(sF6,sF12),
inference(forward_demodulation,[],[f5590,f9]) ).
fof(f5653,plain,
multiplication(sF6,addition(one,sF12)) = addition(sF6,sF12),
inference(superposition,[],[f394,f5633]) ).
fof(f5665,plain,
multiplication(sF6,addition(one,sF12)) = addition(sF12,sF6),
inference(forward_demodulation,[],[f5653,f3]) ).
fof(f5676,plain,
addition(sF12,sF6) = multiplication(sF6,addition(sF12,one)),
inference(forward_demodulation,[],[f5665,f1905]) ).
fof(f5686,plain,
addition(sF12,sF6) = multiplication(sF6,one),
inference(forward_demodulation,[],[f5676,f1649]) ).
fof(f5689,plain,
sF6 = addition(sF12,sF6),
inference(forward_demodulation,[],[f5686,f8]) ).
fof(f5989,plain,
! [X0,X1] : multiplication(one,multiplication(X1,coantidomain(multiplication(X0,X1)))) = multiplication(coantidomain(coantidomain(coantidomain(X0))),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(superposition,[],[f1538,f120]) ).
fof(f6141,plain,
! [X0,X1] : multiplication(one,multiplication(X1,coantidomain(multiplication(X0,X1)))) = multiplication(coantidomain(X0),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f5989,f2273]) ).
fof(f6198,plain,
! [X0,X1] : multiplication(X1,coantidomain(multiplication(X0,X1))) = multiplication(coantidomain(X0),multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(forward_demodulation,[],[f6141,f9]) ).
fof(f6853,plain,
! [X0] : multiplication(addition(sF2,X0),sF22) = addition(zero,multiplication(X0,sF22)),
inference(superposition,[],[f11,f3742]) ).
fof(f6882,plain,
! [X0] : multiplication(X0,sF22) = multiplication(addition(sF2,X0),sF22),
inference(forward_demodulation,[],[f6853,f447]) ).
fof(f6908,plain,
multiplication(sF2,sF22) = multiplication(sF5,sF22),
inference(superposition,[],[f6882,f1660]) ).
fof(f6956,plain,
zero = multiplication(sF5,sF22),
inference(forward_demodulation,[],[f6908,f3742]) ).
fof(f7331,plain,
! [X0] : zero = multiplication(one,multiplication(X0,antidomain(antidomain(coantidomain(X0))))),
inference(superposition,[],[f20,f3760]) ).
fof(f7351,plain,
! [X0] : zero = multiplication(X0,antidomain(antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f7331,f9]) ).
fof(f9039,plain,
addition(sF22,sK5_goals_X1) = addition(sF24,sK5_goals_X1),
inference(superposition,[],[f464,f1466]) ).
fof(f9111,plain,
addition(one,sF6) = addition(sF2,sF6),
inference(superposition,[],[f1450,f5689]) ).
fof(f9115,plain,
multiplication(sF6,coantidomain(sF6)) = multiplication(sF12,coantidomain(sF6)),
inference(superposition,[],[f165,f5689]) ).
fof(f9130,plain,
multiplication(sF6,sF7) = multiplication(sF12,sF7),
inference(forward_demodulation,[],[f9115,f73]) ).
fof(f9132,plain,
addition(sF6,one) = addition(sF2,sF6),
inference(forward_demodulation,[],[f9111,f3]) ).
fof(f9133,plain,
zero = multiplication(sF12,sF7),
inference(forward_demodulation,[],[f9130,f143]) ).
fof(f9135,plain,
one = addition(sF2,sF6),
inference(forward_demodulation,[],[f9132,f1708]) ).
fof(f9147,plain,
! [X0] : multiplication(addition(X0,sF12),sF7) = addition(zero,multiplication(X0,sF7)),
inference(superposition,[],[f321,f9133]) ).
fof(f9148,plain,
! [X0] : addition(multiplication(X0,sF7),zero) = multiplication(addition(sF12,X0),sF7),
inference(superposition,[],[f321,f9133]) ).
fof(f9168,plain,
! [X0] : multiplication(X0,sF7) = multiplication(addition(sF12,X0),sF7),
inference(forward_demodulation,[],[f9148,f5]) ).
fof(f9169,plain,
! [X0] : multiplication(X0,sF7) = multiplication(addition(X0,sF12),sF7),
inference(forward_demodulation,[],[f9147,f447]) ).
fof(f9200,plain,
multiplication(sF12,sF7) = multiplication(sF13,sF7),
inference(superposition,[],[f9168,f1659]) ).
fof(f9255,plain,
zero = multiplication(sF13,sF7),
inference(forward_demodulation,[],[f9200,f9133]) ).
fof(f9282,plain,
multiplication(sF2,coantidomain(sF6)) = multiplication(one,coantidomain(sF6)),
inference(superposition,[],[f165,f9135]) ).
fof(f9299,plain,
coantidomain(sF6) = multiplication(sF2,coantidomain(sF6)),
inference(forward_demodulation,[],[f9282,f9]) ).
fof(f9303,plain,
sF7 = multiplication(sF2,sF7),
inference(forward_demodulation,[],[f9299,f73]) ).
fof(f9318,plain,
addition(sF2,sF7) = multiplication(sF2,addition(one,sF7)),
inference(superposition,[],[f394,f9303]) ).
fof(f9335,plain,
addition(sF2,sF7) = multiplication(sF2,addition(sF7,one)),
inference(forward_demodulation,[],[f9318,f1905]) ).
fof(f9349,plain,
addition(sF2,sF7) = multiplication(sF2,one),
inference(forward_demodulation,[],[f9335,f1707]) ).
fof(f9356,plain,
sF2 = addition(sF2,sF7),
inference(forward_demodulation,[],[f9349,f8]) ).
fof(f9357,plain,
multiplication(sF2,sK5_goals_X1) = addition(sF8,sF23),
inference(backward_demodulation,[],[f1132,f9356]) ).
fof(f9358,plain,
sF23 = addition(sF8,sF23),
inference(forward_demodulation,[],[f9357,f107]) ).
fof(f9664,plain,
multiplication(sF3,coantidomain(sF4)) = multiplication(one,coantidomain(sF4)),
inference(superposition,[],[f319,f490]) ).
fof(f9665,plain,
multiplication(sF4,coantidomain(sF4)) = multiplication(sF5,coantidomain(sF4)),
inference(superposition,[],[f319,f1465]) ).
fof(f9666,plain,
multiplication(sF4,coantidomain(sF4)) = multiplication(sF13,coantidomain(sF4)),
inference(superposition,[],[f319,f1661]) ).
fof(f9786,plain,
multiplication(sF4,sF20) = multiplication(sF13,sF20),
inference(forward_demodulation,[],[f9666,f101]) ).
fof(f9787,plain,
multiplication(sF4,sF20) = multiplication(sF5,sF20),
inference(forward_demodulation,[],[f9665,f101]) ).
fof(f9788,plain,
coantidomain(sF4) = multiplication(sF3,coantidomain(sF4)),
inference(forward_demodulation,[],[f9664,f9]) ).
fof(f9828,plain,
zero = multiplication(sF13,sF20),
inference(forward_demodulation,[],[f9786,f141]) ).
fof(f9829,plain,
zero = multiplication(sF5,sF20),
inference(forward_demodulation,[],[f9787,f141]) ).
fof(f9830,plain,
sF20 = multiplication(sF3,sF20),
inference(forward_demodulation,[],[f9788,f101]) ).
fof(f9866,plain,
multiplication(sF3,addition(one,sF20)) = addition(sF3,sF20),
inference(superposition,[],[f394,f9830]) ).
fof(f9883,plain,
addition(sF3,sF20) = multiplication(sF3,addition(sF20,one)),
inference(forward_demodulation,[],[f9866,f1905]) ).
fof(f9896,plain,
addition(sF3,sF20) = multiplication(sF3,one),
inference(forward_demodulation,[],[f9883,f1709]) ).
fof(f9901,plain,
sF3 = addition(sF3,sF20),
inference(forward_demodulation,[],[f9896,f8]) ).
fof(f9970,plain,
zero = multiplication(coantidomain(coantidomain(sF5)),multiplication(sF20,coantidomain(zero))),
inference(superposition,[],[f651,f9829]) ).
fof(f9979,plain,
zero = multiplication(coantidomain(coantidomain(sF5)),multiplication(sF20,one)),
inference(forward_demodulation,[],[f9970,f2379]) ).
fof(f10001,plain,
zero = multiplication(coantidomain(coantidomain(sF5)),sF20),
inference(forward_demodulation,[],[f9979,f8]) ).
fof(f10014,plain,
zero = multiplication(coantidomain(sF6),sF20),
inference(forward_demodulation,[],[f10001,f71]) ).
fof(f10022,plain,
zero = multiplication(sF7,sF20),
inference(forward_demodulation,[],[f10014,f73]) ).
fof(f10313,plain,
zero = multiplication(coantidomain(coantidomain(sF13)),multiplication(sF20,coantidomain(zero))),
inference(superposition,[],[f651,f9828]) ).
fof(f10322,plain,
zero = multiplication(coantidomain(coantidomain(sF13)),multiplication(sF20,one)),
inference(forward_demodulation,[],[f10313,f2379]) ).
fof(f10344,plain,
zero = multiplication(coantidomain(coantidomain(sF13)),sF20),
inference(forward_demodulation,[],[f10322,f8]) ).
fof(f10357,plain,
zero = multiplication(coantidomain(sF14),sF20),
inference(forward_demodulation,[],[f10344,f88]) ).
fof(f10365,plain,
zero = multiplication(sF15,sF20),
inference(forward_demodulation,[],[f10357,f90]) ).
fof(f10784,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,[],[f452,f11]) ).
fof(f14674,plain,
! [X0,X1] : addition(multiplication(sF13,X0),multiplication(sF12,X1)) = multiplication(sF12,addition(X1,multiplication(sF4,X0))),
inference(superposition,[],[f320,f502]) ).
fof(f17568,plain,
zero = multiplication(coantidomain(coantidomain(sF13)),multiplication(sF7,coantidomain(zero))),
inference(superposition,[],[f651,f9255]) ).
fof(f17579,plain,
zero = multiplication(coantidomain(coantidomain(sF13)),multiplication(sF7,one)),
inference(forward_demodulation,[],[f17568,f2379]) ).
fof(f17607,plain,
zero = multiplication(coantidomain(coantidomain(sF13)),sF7),
inference(forward_demodulation,[],[f17579,f8]) ).
fof(f17625,plain,
zero = multiplication(coantidomain(sF14),sF7),
inference(forward_demodulation,[],[f17607,f88]) ).
fof(f17636,plain,
zero = multiplication(sF15,sF7),
inference(forward_demodulation,[],[f17625,f90]) ).
fof(f17655,plain,
! [X0] : addition(zero,multiplication(X0,sF7)) = multiplication(addition(X0,sF15),sF7),
inference(superposition,[],[f321,f17636]) ).
fof(f17688,plain,
! [X0] : multiplication(X0,sF7) = multiplication(addition(X0,sF15),sF7),
inference(forward_demodulation,[],[f17655,f447]) ).
fof(f17839,plain,
multiplication(one,sF7) = multiplication(sF14,sF7),
inference(superposition,[],[f17688,f546]) ).
fof(f17895,plain,
sF7 = multiplication(sF14,sF7),
inference(forward_demodulation,[],[f17839,f9]) ).
fof(f17923,plain,
addition(sF14,sF7) = multiplication(sF14,addition(sF7,one)),
inference(superposition,[],[f401,f17895]) ).
fof(f17944,plain,
multiplication(sF14,one) = addition(sF14,sF7),
inference(forward_demodulation,[],[f17923,f1707]) ).
fof(f17959,plain,
multiplication(sF14,one) = addition(sF7,sF14),
inference(forward_demodulation,[],[f17944,f3]) ).
fof(f17968,plain,
sF14 = addition(sF7,sF14),
inference(forward_demodulation,[],[f17959,f8]) ).
fof(f17987,plain,
zero = multiplication(sF7,coantidomain(sF14)),
inference(superposition,[],[f882,f17968]) ).
fof(f17989,plain,
zero = multiplication(sF7,sF15),
inference(forward_demodulation,[],[f17987,f90]) ).
fof(f18015,plain,
! [X0] : multiplication(addition(X0,sF7),sF15) = addition(zero,multiplication(X0,sF15)),
inference(superposition,[],[f321,f17989]) ).
fof(f18049,plain,
! [X0] : multiplication(X0,sF15) = multiplication(addition(X0,sF7),sF15),
inference(forward_demodulation,[],[f18015,f447]) ).
fof(f18400,plain,
! [X0] : addition(multiplication(X0,sF23),zero) = multiplication(addition(sF12,X0),sF23),
inference(superposition,[],[f321,f1178]) ).
fof(f18431,plain,
! [X0] : multiplication(X0,sF23) = multiplication(addition(sF12,X0),sF23),
inference(forward_demodulation,[],[f18400,f5]) ).
fof(f18475,plain,
multiplication(sF12,sF23) = multiplication(sF13,sF23),
inference(superposition,[],[f18431,f1659]) ).
fof(f18541,plain,
zero = multiplication(sF13,sF23),
inference(forward_demodulation,[],[f18475,f1178]) ).
fof(f19060,plain,
! [X0] : addition(multiplication(sF13,X0),zero) = multiplication(sF13,addition(sF23,X0)),
inference(superposition,[],[f320,f18541]) ).
fof(f19096,plain,
! [X0] : multiplication(sF13,X0) = multiplication(sF13,addition(sF23,X0)),
inference(forward_demodulation,[],[f19060,f5]) ).
fof(f21669,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,[],[f511,f28]) ).
fof(f22282,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,[],[f21669,f13]) ).
fof(f22446,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,[],[f22282,f2379]) ).
fof(f22587,plain,
! [X0,X1] : one = coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),coantidomain(X1))),
inference(forward_demodulation,[],[f22446,f885]) ).
fof(f22823,plain,
addition(one,sF27) = addition(sF0,sF28),
inference(superposition,[],[f1627,f117]) ).
fof(f22860,plain,
addition(sF27,one) = addition(sF0,sF28),
inference(forward_demodulation,[],[f22823,f3]) ).
fof(f22876,plain,
one = addition(sF0,sF28),
inference(forward_demodulation,[],[f22860,f1698]) ).
fof(f23100,plain,
multiplication(antidomain(sF0),one) = multiplication(antidomain(sF0),sF28),
inference(superposition,[],[f374,f22876]) ).
fof(f23115,plain,
multiplication(sF1,one) = multiplication(sF1,sF28),
inference(forward_demodulation,[],[f23100,f61]) ).
fof(f23124,plain,
sF1 = multiplication(sF1,sF28),
inference(forward_demodulation,[],[f23115,f8]) ).
fof(f23125,plain,
! [X0] : multiplication(sF1,X0) = multiplication(sF1,multiplication(sF28,X0)),
inference(superposition,[],[f7,f23124]) ).
fof(f24913,plain,
! [X0] : addition(multiplication(sF5,X0),zero) = multiplication(sF5,addition(sF22,X0)),
inference(superposition,[],[f320,f6956]) ).
fof(f24915,plain,
! [X0] : addition(multiplication(X0,sF22),zero) = multiplication(addition(sF5,X0),sF22),
inference(superposition,[],[f321,f6956]) ).
fof(f24951,plain,
! [X0] : multiplication(X0,sF22) = multiplication(addition(sF5,X0),sF22),
inference(forward_demodulation,[],[f24915,f5]) ).
fof(f24953,plain,
! [X0] : multiplication(sF5,X0) = multiplication(sF5,addition(sF22,X0)),
inference(forward_demodulation,[],[f24913,f5]) ).
fof(f25007,plain,
multiplication(sF13,sF22) = multiplication(sF4,sF22),
inference(superposition,[],[f24951,f1835]) ).
fof(f25168,plain,
addition(sF4,sF12) = addition(sF5,sF12),
inference(superposition,[],[f1853,f1659]) ).
fof(f25206,plain,
addition(sF4,sF12) = addition(sF12,sF5),
inference(forward_demodulation,[],[f25168,f3]) ).
fof(f25220,plain,
multiplication(sF5,sF7) = multiplication(addition(sF4,sF12),sF7),
inference(superposition,[],[f9168,f25206]) ).
fof(f25221,plain,
addition(one,sF5) = addition(sF2,addition(sF4,sF12)),
inference(superposition,[],[f1450,f25206]) ).
fof(f25249,plain,
addition(one,sF4) = addition(one,sF5),
inference(forward_demodulation,[],[f25221,f1461]) ).
fof(f25250,plain,
multiplication(sF5,sF7) = multiplication(sF4,sF7),
inference(forward_demodulation,[],[f25220,f9169]) ).
fof(f25256,plain,
addition(one,sF4) = addition(sF5,one),
inference(forward_demodulation,[],[f25249,f3]) ).
fof(f25257,plain,
sF5 = multiplication(sF4,sF7),
inference(forward_demodulation,[],[f25250,f2385]) ).
fof(f25260,plain,
addition(sF4,one) = addition(sF5,one),
inference(forward_demodulation,[],[f25256,f3]) ).
fof(f25261,plain,
one = addition(sF5,one),
inference(forward_demodulation,[],[f25260,f1648]) ).
fof(f25264,plain,
addition(sF5,sF7) = multiplication(one,sF7),
inference(backward_demodulation,[],[f4838,f25261]) ).
fof(f25265,plain,
sF7 = addition(sF5,sF7),
inference(forward_demodulation,[],[f25264,f9]) ).
fof(f25562,plain,
multiplication(sF7,sF15) = multiplication(sF5,sF15),
inference(superposition,[],[f18049,f25265]) ).
fof(f25590,plain,
zero = multiplication(sF5,sF15),
inference(forward_demodulation,[],[f25562,f17989]) ).
fof(f26080,plain,
! [X0] : addition(multiplication(X0,sF15),zero) = multiplication(addition(sF5,X0),sF15),
inference(superposition,[],[f321,f25590]) ).
fof(f26116,plain,
! [X0] : multiplication(X0,sF15) = multiplication(addition(sF5,X0),sF15),
inference(forward_demodulation,[],[f26080,f5]) ).
fof(f26390,plain,
multiplication(sF13,sF15) = multiplication(sF4,sF15),
inference(superposition,[],[f26116,f1835]) ).
fof(f26462,plain,
sF13 = multiplication(sF4,sF15),
inference(forward_demodulation,[],[f26390,f2383]) ).
fof(f27245,plain,
addition(sK1_goals_X0,sF23) = addition(sF24,sK1_goals_X0),
inference(superposition,[],[f464,f1672]) ).
fof(f27272,plain,
addition(sF23,sK1_goals_X0) = addition(sF24,sK1_goals_X0),
inference(forward_demodulation,[],[f27245,f3]) ).
fof(f29126,plain,
! [X0] : multiplication(antidomain(multiplication(X0,sF23)),multiplication(X0,sF23)) = multiplication(antidomain(multiplication(X0,sF23)),multiplication(X0,sF8)),
inference(superposition,[],[f738,f9358]) ).
fof(f29291,plain,
! [X0] : zero = multiplication(antidomain(multiplication(X0,sF23)),multiplication(X0,sF8)),
inference(forward_demodulation,[],[f29126,f20]) ).
fof(f30540,plain,
! [X0] : multiplication(X0,coantidomain(zero)) = multiplication(coantidomain(antidomain(X0)),multiplication(X0,coantidomain(zero))),
inference(superposition,[],[f6198,f20]) ).
fof(f30571,plain,
! [X0,X1] : multiplication(multiplication(X0,X1),coantidomain(zero)) = multiplication(coantidomain(antidomain(X0)),multiplication(multiplication(X0,X1),coantidomain(zero))),
inference(superposition,[],[f6198,f523]) ).
fof(f30592,plain,
! [X0,X1] : multiplication(coantidomain(addition(X0,X1)),coantidomain(zero)) = multiplication(coantidomain(X0),multiplication(coantidomain(addition(X0,X1)),coantidomain(zero))),
inference(superposition,[],[f6198,f882]) ).
fof(f30616,plain,
multiplication(sF2,coantidomain(zero)) = multiplication(coantidomain(sF12),multiplication(sF2,coantidomain(zero))),
inference(superposition,[],[f6198,f204]) ).
fof(f30681,plain,
multiplication(sF12,coantidomain(zero)) = multiplication(coantidomain(sF2),multiplication(sF12,coantidomain(zero))),
inference(superposition,[],[f6198,f3801]) ).
fof(f30734,plain,
multiplication(sF20,coantidomain(zero)) = multiplication(coantidomain(sF7),multiplication(sF20,coantidomain(zero))),
inference(superposition,[],[f6198,f10022]) ).
fof(f30736,plain,
multiplication(sF20,coantidomain(zero)) = multiplication(coantidomain(sF15),multiplication(sF20,coantidomain(zero))),
inference(superposition,[],[f6198,f10365]) ).
fof(f30772,plain,
multiplication(sF28,coantidomain(multiplication(sF0,sF27))) = multiplication(coantidomain(sF0),multiplication(sF28,coantidomain(multiplication(sF0,sF27)))),
inference(superposition,[],[f6198,f3749]) ).
fof(f30863,plain,
multiplication(sF20,one) = multiplication(coantidomain(sF15),multiplication(sF20,one)),
inference(forward_demodulation,[],[f30736,f2379]) ).
fof(f30865,plain,
multiplication(sF20,one) = multiplication(coantidomain(sF7),multiplication(sF20,one)),
inference(forward_demodulation,[],[f30734,f2379]) ).
fof(f30894,plain,
multiplication(sF12,one) = multiplication(coantidomain(sF2),multiplication(sF12,one)),
inference(forward_demodulation,[],[f30681,f2379]) ).
fof(f30930,plain,
multiplication(sF2,one) = multiplication(coantidomain(sF12),multiplication(sF2,one)),
inference(forward_demodulation,[],[f30616,f2379]) ).
fof(f30948,plain,
! [X0,X1] : multiplication(coantidomain(addition(X0,X1)),one) = multiplication(coantidomain(X0),multiplication(coantidomain(addition(X0,X1)),one)),
inference(forward_demodulation,[],[f30592,f2379]) ).
fof(f30967,plain,
! [X0,X1] : multiplication(X0,multiplication(X1,coantidomain(zero))) = multiplication(coantidomain(antidomain(X0)),multiplication(X0,multiplication(X1,coantidomain(zero)))),
inference(forward_demodulation,[],[f30571,f7]) ).
fof(f30981,plain,
! [X0] : multiplication(X0,one) = multiplication(coantidomain(antidomain(X0)),multiplication(X0,one)),
inference(forward_demodulation,[],[f30540,f2379]) ).
fof(f31008,plain,
sF20 = multiplication(coantidomain(sF15),sF20),
inference(forward_demodulation,[],[f30863,f8]) ).
fof(f31010,plain,
sF20 = multiplication(coantidomain(sF7),sF20),
inference(forward_demodulation,[],[f30865,f8]) ).
fof(f31028,plain,
sF12 = multiplication(coantidomain(sF2),sF12),
inference(forward_demodulation,[],[f30894,f8]) ).
fof(f31049,plain,
sF2 = multiplication(coantidomain(sF12),sF2),
inference(forward_demodulation,[],[f30930,f8]) ).
fof(f31058,plain,
! [X0,X1] : coantidomain(addition(X0,X1)) = multiplication(coantidomain(X0),coantidomain(addition(X0,X1))),
inference(forward_demodulation,[],[f30948,f8]) ).
fof(f31063,plain,
! [X0,X1] : multiplication(X0,multiplication(X1,one)) = multiplication(coantidomain(antidomain(X0)),multiplication(X0,multiplication(X1,one))),
inference(forward_demodulation,[],[f30967,f2379]) ).
fof(f31068,plain,
! [X0] : multiplication(coantidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f30981,f8]) ).
fof(f31084,plain,
sF20 = multiplication(sF14,sF20),
inference(forward_demodulation,[],[f31008,f2530]) ).
fof(f31086,plain,
sF20 = multiplication(sF6,sF20),
inference(forward_demodulation,[],[f31010,f2537]) ).
fof(f31114,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(coantidomain(antidomain(X0)),multiplication(X0,X1)),
inference(forward_demodulation,[],[f31063,f8]) ).
fof(f31133,plain,
sF3 = multiplication(coantidomain(sF4),sF3),
inference(superposition,[],[f31068,f67]) ).
fof(f31239,plain,
sF3 = multiplication(sF20,sF3),
inference(forward_demodulation,[],[f31133,f101]) ).
fof(f31314,plain,
addition(sF20,sF3) = multiplication(sF20,addition(sF3,one)),
inference(superposition,[],[f401,f31239]) ).
fof(f31345,plain,
multiplication(sF20,one) = addition(sF20,sF3),
inference(forward_demodulation,[],[f31314,f1652]) ).
fof(f31365,plain,
multiplication(sF20,one) = addition(sF3,sF20),
inference(forward_demodulation,[],[f31345,f3]) ).
fof(f31377,plain,
sF3 = multiplication(sF20,one),
inference(forward_demodulation,[],[f31365,f9901]) ).
fof(f31382,plain,
sF3 = sF20,
inference(forward_demodulation,[],[f31377,f8]) ).
fof(f31386,plain,
sF21 = coantidomain(sF3),
inference(backward_demodulation,[],[f103,f31382]) ).
fof(f31770,plain,
sF3 = multiplication(sF14,sF3),
inference(backward_demodulation,[],[f31084,f31382]) ).
fof(f31771,plain,
sF3 = multiplication(sF6,sF3),
inference(backward_demodulation,[],[f31086,f31382]) ).
fof(f31840,plain,
sF21 = multiplication(sF4,sF21),
inference(backward_demodulation,[],[f3195,f31386]) ).
fof(f31906,plain,
sF4 = sF21,
inference(forward_demodulation,[],[f31840,f2386]) ).
fof(f31947,plain,
sF25 = multiplication(sF4,sF24),
inference(backward_demodulation,[],[f111,f31906]) ).
fof(f31950,plain,
! [X0] : addition(sF25,multiplication(X0,sF24)) = multiplication(addition(sF4,X0),sF24),
inference(backward_demodulation,[],[f278,f31906]) ).
fof(f31952,plain,
! [X0] : addition(sF25,multiplication(sF4,X0)) = multiplication(sF4,addition(X0,sF24)),
inference(backward_demodulation,[],[f283,f31906]) ).
fof(f31956,plain,
! [X0] : multiplication(sF25,X0) = multiplication(sF4,multiplication(sF24,X0)),
inference(backward_demodulation,[],[f503,f31906]) ).
fof(f32176,plain,
sF4 = coantidomain(sF3),
inference(backward_demodulation,[],[f31386,f31906]) ).
fof(f32458,plain,
multiplication(sF13,sF24) = multiplication(sF12,sF25),
inference(superposition,[],[f502,f31947]) ).
fof(f32459,plain,
multiplication(sF5,sF24) = multiplication(sF2,sF25),
inference(superposition,[],[f501,f31947]) ).
fof(f32844,plain,
addition(sF14,sF3) = multiplication(sF14,addition(sF3,one)),
inference(superposition,[],[f401,f31770]) ).
fof(f32876,plain,
multiplication(sF14,one) = addition(sF14,sF3),
inference(forward_demodulation,[],[f32844,f1652]) ).
fof(f32897,plain,
multiplication(sF14,one) = addition(sF3,sF14),
inference(forward_demodulation,[],[f32876,f3]) ).
fof(f32912,plain,
sF14 = addition(sF3,sF14),
inference(forward_demodulation,[],[f32897,f8]) ).
fof(f32939,plain,
addition(sF6,sF3) = multiplication(sF6,addition(sF3,one)),
inference(superposition,[],[f401,f31771]) ).
fof(f32971,plain,
multiplication(sF6,one) = addition(sF6,sF3),
inference(forward_demodulation,[],[f32939,f1652]) ).
fof(f32992,plain,
multiplication(sF6,one) = addition(sF3,sF6),
inference(forward_demodulation,[],[f32971,f3]) ).
fof(f33007,plain,
sF6 = addition(sF3,sF6),
inference(forward_demodulation,[],[f32992,f8]) ).
fof(f33651,plain,
! [X0] : multiplication(sF13,multiplication(sF24,X0)) = multiplication(sF12,multiplication(sF25,X0)),
inference(superposition,[],[f502,f31956]) ).
fof(f34547,plain,
zero = multiplication(sF3,coantidomain(sF14)),
inference(superposition,[],[f882,f32912]) ).
fof(f34550,plain,
zero = multiplication(sF3,sF15),
inference(forward_demodulation,[],[f34547,f90]) ).
fof(f34596,plain,
multiplication(sF15,coantidomain(zero)) = multiplication(coantidomain(sF3),multiplication(sF15,coantidomain(zero))),
inference(superposition,[],[f6198,f34550]) ).
fof(f34597,plain,
multiplication(sF15,one) = multiplication(coantidomain(sF3),multiplication(sF15,one)),
inference(forward_demodulation,[],[f34596,f2379]) ).
fof(f34629,plain,
sF15 = multiplication(coantidomain(sF3),sF15),
inference(forward_demodulation,[],[f34597,f8]) ).
fof(f34650,plain,
sF15 = multiplication(sF4,sF15),
inference(forward_demodulation,[],[f34629,f32176]) ).
fof(f34667,plain,
sF13 = sF15,
inference(forward_demodulation,[],[f34650,f26462]) ).
fof(f34673,plain,
sF13 = coantidomain(sF14),
inference(backward_demodulation,[],[f90,f34667]) ).
fof(f34674,plain,
sF16 = multiplication(sF13,sK1_goals_X0),
inference(backward_demodulation,[],[f92,f34667]) ).
fof(f34679,plain,
! [X0] : multiplication(sF13,addition(sK1_goals_X0,X0)) = addition(sF16,multiplication(sF13,X0)),
inference(backward_demodulation,[],[f247,f34667]) ).
fof(f34680,plain,
! [X0] : addition(sF16,multiplication(sF13,X0)) = multiplication(sF13,addition(X0,sK1_goals_X0)),
inference(backward_demodulation,[],[f250,f34667]) ).
fof(f34694,plain,
addition(sF16,sF22) = multiplication(addition(sF12,sF13),sK1_goals_X0),
inference(backward_demodulation,[],[f1226,f34667]) ).
fof(f35330,plain,
multiplication(sF12,sK1_goals_X0) = addition(sF16,sF22),
inference(forward_demodulation,[],[f34694,f1659]) ).
fof(f35357,plain,
sF22 = addition(sF16,sF22),
inference(forward_demodulation,[],[f35330,f105]) ).
fof(f35447,plain,
! [X0] : addition(sF22,X0) = addition(sF16,addition(sF22,X0)),
inference(superposition,[],[f4,f35357]) ).
fof(f35457,plain,
! [X0] : multiplication(antidomain(multiplication(X0,sF22)),multiplication(X0,sF22)) = multiplication(antidomain(multiplication(X0,sF22)),multiplication(X0,sF16)),
inference(superposition,[],[f738,f35357]) ).
fof(f35464,plain,
! [X0] : zero = multiplication(antidomain(multiplication(X0,sF22)),multiplication(X0,sF16)),
inference(forward_demodulation,[],[f35457,f20]) ).
fof(f36396,plain,
multiplication(sF13,addition(sK1_goals_X0,sF22)) = addition(sF16,multiplication(sF4,sF22)),
inference(superposition,[],[f34679,f25007]) ).
fof(f36398,plain,
multiplication(sF13,addition(sK1_goals_X0,sF24)) = addition(sF16,multiplication(sF12,sF25)),
inference(superposition,[],[f34679,f32458]) ).
fof(f36442,plain,
addition(sF16,multiplication(sF12,sF25)) = multiplication(sF13,addition(sF24,sK1_goals_X0)),
inference(forward_demodulation,[],[f36398,f1905]) ).
fof(f36444,plain,
addition(sF16,multiplication(sF4,sF22)) = multiplication(sF13,addition(sF22,sK1_goals_X0)),
inference(forward_demodulation,[],[f36396,f1905]) ).
fof(f36479,plain,
addition(sF16,multiplication(sF12,sF25)) = multiplication(sF13,addition(sF23,sK1_goals_X0)),
inference(forward_demodulation,[],[f36442,f27272]) ).
fof(f36481,plain,
multiplication(sF13,sK1_goals_X0) = addition(sF16,multiplication(sF4,sF22)),
inference(forward_demodulation,[],[f36444,f1662]) ).
fof(f36507,plain,
multiplication(sF13,sK1_goals_X0) = addition(sF16,multiplication(sF12,sF25)),
inference(forward_demodulation,[],[f36479,f19096]) ).
fof(f36509,plain,
sF16 = addition(sF16,multiplication(sF4,sF22)),
inference(forward_demodulation,[],[f36481,f34674]) ).
fof(f36521,plain,
sF16 = addition(sF16,multiplication(sF12,sF25)),
inference(forward_demodulation,[],[f36507,f34674]) ).
fof(f36786,plain,
zero = multiplication(sF3,coantidomain(sF6)),
inference(superposition,[],[f882,f33007]) ).
fof(f36789,plain,
zero = multiplication(sF3,sF7),
inference(forward_demodulation,[],[f36786,f73]) ).
fof(f36837,plain,
multiplication(sF7,coantidomain(zero)) = multiplication(coantidomain(sF3),multiplication(sF7,coantidomain(zero))),
inference(superposition,[],[f6198,f36789]) ).
fof(f36838,plain,
multiplication(sF7,one) = multiplication(coantidomain(sF3),multiplication(sF7,one)),
inference(forward_demodulation,[],[f36837,f2379]) ).
fof(f36870,plain,
sF7 = multiplication(coantidomain(sF3),sF7),
inference(forward_demodulation,[],[f36838,f8]) ).
fof(f36891,plain,
sF7 = multiplication(sF4,sF7),
inference(forward_demodulation,[],[f36870,f32176]) ).
fof(f36908,plain,
sF5 = sF7,
inference(forward_demodulation,[],[f36891,f25257]) ).
fof(f36915,plain,
sF8 = multiplication(sF5,sK5_goals_X1),
inference(backward_demodulation,[],[f75,f36908]) ).
fof(f36920,plain,
! [X0] : multiplication(sF5,addition(sK5_goals_X1,X0)) = addition(sF8,multiplication(sF5,X0)),
inference(backward_demodulation,[],[f232,f36908]) ).
fof(f38780,plain,
multiplication(sF5,addition(sK5_goals_X1,sF24)) = addition(sF8,multiplication(sF2,sF25)),
inference(superposition,[],[f36920,f32459]) ).
fof(f38824,plain,
addition(sF8,multiplication(sF2,sF25)) = multiplication(sF5,addition(sF24,sK5_goals_X1)),
inference(forward_demodulation,[],[f38780,f1905]) ).
fof(f38859,plain,
addition(sF8,multiplication(sF2,sF25)) = multiplication(sF5,addition(sF22,sK5_goals_X1)),
inference(forward_demodulation,[],[f38824,f9039]) ).
fof(f38886,plain,
multiplication(sF5,sK5_goals_X1) = addition(sF8,multiplication(sF2,sF25)),
inference(forward_demodulation,[],[f38859,f24953]) ).
fof(f38899,plain,
sF8 = addition(sF8,multiplication(sF2,sF25)),
inference(forward_demodulation,[],[f38886,f36915]) ).
fof(f40647,plain,
sF24 = addition(sF16,sF24),
inference(superposition,[],[f35447,f109]) ).
fof(f44324,plain,
zero = multiplication(antidomain(zero),multiplication(sF12,sF8)),
inference(superposition,[],[f29291,f1178]) ).
fof(f44421,plain,
zero = multiplication(one,multiplication(sF12,sF8)),
inference(forward_demodulation,[],[f44324,f3702]) ).
fof(f44447,plain,
zero = multiplication(sF12,sF8),
inference(forward_demodulation,[],[f44421,f9]) ).
fof(f44487,plain,
! [X0] : multiplication(addition(X0,sF12),sF8) = addition(zero,multiplication(X0,sF8)),
inference(superposition,[],[f321,f44447]) ).
fof(f44529,plain,
! [X0] : multiplication(X0,sF8) = multiplication(addition(X0,sF12),sF8),
inference(forward_demodulation,[],[f44487,f447]) ).
fof(f45074,plain,
sF16 = multiplication(coantidomain(antidomain(sF13)),sF16),
inference(superposition,[],[f31114,f34674]) ).
fof(f45209,plain,
sF25 = multiplication(coantidomain(antidomain(sF4)),sF25),
inference(superposition,[],[f31114,f31947]) ).
fof(f45290,plain,
sF25 = multiplication(coantidomain(sF3),sF25),
inference(forward_demodulation,[],[f45209,f3714]) ).
fof(f45337,plain,
sF25 = multiplication(sF4,sF25),
inference(forward_demodulation,[],[f45290,f32176]) ).
fof(f45362,plain,
multiplication(sF12,sF25) = multiplication(sF13,sF25),
inference(superposition,[],[f502,f45337]) ).
fof(f45534,plain,
addition(sF16,multiplication(sF12,sF25)) = multiplication(sF13,addition(sK1_goals_X0,sF25)),
inference(superposition,[],[f34679,f45362]) ).
fof(f45537,plain,
! [X0] : addition(multiplication(sF13,X0),multiplication(sF12,sF25)) = multiplication(sF13,addition(X0,sF25)),
inference(superposition,[],[f10,f45362]) ).
fof(f45586,plain,
! [X0] : multiplication(sF12,addition(sF25,multiplication(sF4,X0))) = multiplication(sF13,addition(X0,sF25)),
inference(forward_demodulation,[],[f45537,f14674]) ).
fof(f45589,plain,
addition(sF16,multiplication(sF12,sF25)) = multiplication(sF13,addition(sF25,sK1_goals_X0)),
inference(forward_demodulation,[],[f45534,f1905]) ).
fof(f45602,plain,
! [X0] : multiplication(sF12,multiplication(sF4,addition(X0,sF24))) = multiplication(sF13,addition(X0,sF25)),
inference(forward_demodulation,[],[f45586,f31952]) ).
fof(f45606,plain,
sF16 = multiplication(sF13,addition(sF25,sK1_goals_X0)),
inference(forward_demodulation,[],[f45589,f36521]) ).
fof(f45614,plain,
! [X0] : multiplication(sF13,addition(X0,sF24)) = multiplication(sF13,addition(X0,sF25)),
inference(forward_demodulation,[],[f45602,f502]) ).
fof(f45668,plain,
! [X0] : multiplication(addition(one,antidomain(coantidomain(X0))),coantidomain(coantidomain(X0))) = addition(coantidomain(coantidomain(X0)),antidomain(coantidomain(X0))),
inference(superposition,[],[f555,f840]) ).
fof(f45681,plain,
! [X0] : multiplication(one,coantidomain(coantidomain(X0))) = addition(coantidomain(coantidomain(X0)),antidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f45668,f886]) ).
fof(f45711,plain,
! [X0] : coantidomain(coantidomain(X0)) = addition(coantidomain(coantidomain(X0)),antidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f45681,f9]) ).
fof(f49572,plain,
zero = multiplication(antidomain(zero),multiplication(sF5,sF16)),
inference(superposition,[],[f35464,f6956]) ).
fof(f49670,plain,
zero = multiplication(one,multiplication(sF5,sF16)),
inference(forward_demodulation,[],[f49572,f3702]) ).
fof(f49695,plain,
zero = multiplication(sF5,sF16),
inference(forward_demodulation,[],[f49670,f9]) ).
fof(f50027,plain,
! [X0] : multiplication(addition(sF5,X0),sF16) = addition(multiplication(X0,sF16),zero),
inference(superposition,[],[f321,f49695]) ).
fof(f50068,plain,
! [X0] : multiplication(X0,sF16) = multiplication(addition(sF5,X0),sF16),
inference(forward_demodulation,[],[f50027,f5]) ).
fof(f50138,plain,
multiplication(sF13,sF16) = multiplication(sF4,sF16),
inference(superposition,[],[f50068,f1835]) ).
fof(f50747,plain,
! [X0] : addition(multiplication(sF4,sF16),multiplication(sF13,X0)) = multiplication(sF13,addition(X0,sF16)),
inference(superposition,[],[f320,f50138]) ).
fof(f50989,plain,
multiplication(one,sF8) = multiplication(sF2,sF8),
inference(superposition,[],[f44529,f489]) ).
fof(f51052,plain,
sF8 = multiplication(sF2,sF8),
inference(forward_demodulation,[],[f50989,f9]) ).
fof(f51073,plain,
! [X0] : addition(sF8,multiplication(sF2,X0)) = multiplication(sF2,addition(X0,sF8)),
inference(superposition,[],[f320,f51052]) ).
fof(f51113,plain,
sF8 = multiplication(sF2,addition(sF25,sF8)),
inference(backward_demodulation,[],[f38899,f51073]) ).
fof(f51128,plain,
sF8 = multiplication(sF2,addition(sF8,sF25)),
inference(forward_demodulation,[],[f51113,f1905]) ).
fof(f53549,plain,
! [X2,X0,X1] : addition(multiplication(X0,one),multiplication(addition(X0,X2),antidomain(X1))) = addition(multiplication(X0,one),multiplication(X2,antidomain(X1))),
inference(superposition,[],[f10784,f886]) ).
fof(f53550,plain,
! [X2,X0,X1] : addition(multiplication(X0,one),multiplication(addition(X0,X2),coantidomain(X1))) = addition(multiplication(X0,one),multiplication(X2,coantidomain(X1))),
inference(superposition,[],[f10784,f885]) ).
fof(f53568,plain,
! [X0,X1] : addition(multiplication(X0,sF0),multiplication(addition(X0,X1),sF1)) = addition(multiplication(X0,one),multiplication(X1,sF1)),
inference(superposition,[],[f10784,f487]) ).
fof(f53579,plain,
! [X0,X1] : addition(multiplication(X0,sF2),multiplication(addition(X0,X1),sF12)) = addition(multiplication(X0,one),multiplication(X1,sF12)),
inference(superposition,[],[f10784,f489]) ).
fof(f53621,plain,
! [X0,X1] : addition(multiplication(X0,sF9),multiplication(addition(X0,X1),sF10)) = addition(multiplication(X0,one),multiplication(X1,sF10)),
inference(superposition,[],[f10784,f547]) ).
fof(f53653,plain,
! [X0,X1] : addition(multiplication(X0,sF1),multiplication(X1,sF1)) = addition(multiplication(X0,sF18),multiplication(addition(X0,X1),sF1)),
inference(superposition,[],[f10784,f122]) ).
fof(f54160,plain,
! [X2,X0,X1] : addition(multiplication(coantidomain(X0),addition(X1,X2)),multiplication(coantidomain(coantidomain(X0)),X2)) = addition(multiplication(coantidomain(X0),X1),multiplication(one,X2)),
inference(superposition,[],[f10784,f120]) ).
fof(f54342,plain,
! [X2,X0,X1] : addition(multiplication(coantidomain(X0),X1),X2) = addition(multiplication(coantidomain(X0),addition(X1,X2)),multiplication(coantidomain(coantidomain(X0)),X2)),
inference(forward_demodulation,[],[f54160,f9]) ).
fof(f54799,plain,
! [X0,X1] : multiplication(addition(X0,X1),sF1) = addition(multiplication(X0,sF18),multiplication(addition(X0,X1),sF1)),
inference(forward_demodulation,[],[f53653,f11]) ).
fof(f54819,plain,
! [X0,X1] : addition(multiplication(X0,sF9),multiplication(addition(X0,X1),sF10)) = addition(X0,multiplication(X1,sF10)),
inference(forward_demodulation,[],[f53621,f8]) ).
fof(f54841,plain,
! [X0,X1] : addition(multiplication(X0,sF2),multiplication(addition(X0,X1),sF12)) = addition(X0,multiplication(X1,sF12)),
inference(forward_demodulation,[],[f53579,f8]) ).
fof(f54849,plain,
! [X0,X1] : addition(multiplication(X0,sF0),multiplication(addition(X0,X1),sF1)) = addition(X0,multiplication(X1,sF1)),
inference(forward_demodulation,[],[f53568,f8]) ).
fof(f54860,plain,
! [X2,X0,X1] : addition(X0,multiplication(addition(X0,X2),coantidomain(X1))) = addition(X0,multiplication(X2,coantidomain(X1))),
inference(forward_demodulation,[],[f53550,f8]) ).
fof(f54861,plain,
! [X2,X0,X1] : addition(X0,multiplication(addition(X0,X2),antidomain(X1))) = addition(X0,multiplication(X2,antidomain(X1))),
inference(forward_demodulation,[],[f53549,f8]) ).
fof(f54924,plain,
! [X2,X0,X1] : addition(multiplication(coantidomain(X0),X1),X2) = addition(multiplication(coantidomain(coantidomain(X0)),X2),multiplication(coantidomain(X0),addition(X1,X2))),
inference(forward_demodulation,[],[f54342,f3]) ).
fof(f55213,plain,
! [X0,X1] : addition(antidomain(X0),multiplication(antidomain(antidomain(X0)),antidomain(X1))) = addition(antidomain(X0),multiplication(one,antidomain(X1))),
inference(superposition,[],[f54861,f119]) ).
fof(f55215,plain,
! [X0,X1] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),antidomain(X1))) = addition(coantidomain(X0),multiplication(one,antidomain(X1))),
inference(superposition,[],[f54861,f120]) ).
fof(f55304,plain,
! [X0,X1] : addition(X0,multiplication(X1,sF1)) = addition(X0,multiplication(addition(X0,X1),sF1)),
inference(superposition,[],[f54861,f61]) ).
fof(f55580,plain,
! [X0,X1] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),antidomain(X1))) = addition(coantidomain(X0),antidomain(X1)),
inference(forward_demodulation,[],[f55215,f9]) ).
fof(f55581,plain,
! [X0,X1] : addition(antidomain(X0),multiplication(antidomain(antidomain(X0)),antidomain(X1))) = addition(antidomain(X0),antidomain(X1)),
inference(forward_demodulation,[],[f55213,f9]) ).
fof(f55845,plain,
! [X0,X1] : addition(antidomain(X0),multiplication(antidomain(antidomain(X0)),coantidomain(X1))) = addition(antidomain(X0),multiplication(one,coantidomain(X1))),
inference(superposition,[],[f54860,f119]) ).
fof(f55847,plain,
! [X0,X1] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),coantidomain(X1))) = addition(coantidomain(X0),multiplication(one,coantidomain(X1))),
inference(superposition,[],[f54860,f120]) ).
fof(f56227,plain,
! [X0,X1] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),coantidomain(X1))) = addition(coantidomain(X0),coantidomain(X1)),
inference(forward_demodulation,[],[f55847,f9]) ).
fof(f56228,plain,
! [X0,X1] : addition(antidomain(X0),multiplication(antidomain(antidomain(X0)),coantidomain(X1))) = addition(antidomain(X0),coantidomain(X1)),
inference(forward_demodulation,[],[f55845,f9]) ).
fof(f56475,plain,
! [X0,X1] : addition(X1,multiplication(X0,sF1)) = addition(X1,multiplication(addition(X0,X1),sF1)),
inference(superposition,[],[f55304,f3]) ).
fof(f56503,plain,
! [X0] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),sF1)) = addition(coantidomain(X0),multiplication(one,sF1)),
inference(superposition,[],[f55304,f120]) ).
fof(f56878,plain,
! [X0] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),sF1)) = addition(coantidomain(X0),sF1),
inference(forward_demodulation,[],[f56503,f9]) ).
fof(f57009,plain,
! [X0] : addition(sF1,coantidomain(X0)) = addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),sF1)),
inference(forward_demodulation,[],[f56878,f3]) ).
fof(f57428,plain,
! [X0] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),sF1)) = addition(multiplication(coantidomain(X0),sF0),multiplication(one,sF1)),
inference(superposition,[],[f54849,f120]) ).
fof(f57691,plain,
! [X0] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),sF1)) = addition(multiplication(one,sF1),multiplication(coantidomain(X0),sF0)),
inference(forward_demodulation,[],[f57428,f3]) ).
fof(f57810,plain,
! [X0] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),sF1)) = addition(sF1,multiplication(coantidomain(X0),sF0)),
inference(forward_demodulation,[],[f57691,f9]) ).
fof(f57896,plain,
! [X0] : addition(sF1,coantidomain(X0)) = addition(sF1,multiplication(coantidomain(X0),sF0)),
inference(forward_demodulation,[],[f57810,f57009]) ).
fof(f58070,plain,
addition(sF1,sF0) = addition(sF1,coantidomain(antidomain(sF0))),
inference(superposition,[],[f57896,f31068]) ).
fof(f58124,plain,
addition(sF1,sF0) = addition(sF1,coantidomain(sF1)),
inference(forward_demodulation,[],[f58070,f61]) ).
fof(f58154,plain,
addition(sF0,sF1) = addition(sF1,coantidomain(sF1)),
inference(forward_demodulation,[],[f58124,f3]) ).
fof(f58168,plain,
one = addition(sF1,coantidomain(sF1)),
inference(forward_demodulation,[],[f58154,f487]) ).
fof(f58285,plain,
multiplication(sF0,coantidomain(sF1)) = multiplication(sF0,one),
inference(superposition,[],[f3792,f58168]) ).
fof(f58295,plain,
multiplication(sF1,coantidomain(coantidomain(sF1))) = multiplication(one,coantidomain(coantidomain(sF1))),
inference(superposition,[],[f165,f58168]) ).
fof(f58339,plain,
coantidomain(coantidomain(sF1)) = multiplication(sF1,coantidomain(coantidomain(sF1))),
inference(forward_demodulation,[],[f58295,f9]) ).
fof(f58345,plain,
sF0 = multiplication(sF0,coantidomain(sF1)),
inference(forward_demodulation,[],[f58285,f8]) ).
fof(f58349,plain,
sF1 = coantidomain(coantidomain(sF1)),
inference(forward_demodulation,[],[f58339,f2265]) ).
fof(f58350,plain,
sF0 = coantidomain(sF1),
inference(backward_demodulation,[],[f1630,f58345]) ).
fof(f58438,plain,
sF1 = coantidomain(sF0),
inference(backward_demodulation,[],[f58349,f58350]) ).
fof(f58506,plain,
multiplication(sF28,coantidomain(multiplication(sF0,sF27))) = multiplication(sF1,multiplication(sF28,coantidomain(multiplication(sF0,sF27)))),
inference(backward_demodulation,[],[f30772,f58438]) ).
fof(f58570,plain,
multiplication(sF28,coantidomain(multiplication(sF0,sF27))) = multiplication(sF1,coantidomain(multiplication(sF0,sF27))),
inference(forward_demodulation,[],[f58506,f23125]) ).
fof(f59833,plain,
! [X0] : addition(antidomain(X0),multiplication(antidomain(antidomain(X0)),sF12)) = addition(multiplication(antidomain(X0),sF2),multiplication(one,sF12)),
inference(superposition,[],[f54841,f119]) ).
fof(f59840,plain,
! [X0] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),sF12)) = addition(multiplication(coantidomain(X0),sF2),multiplication(one,sF12)),
inference(superposition,[],[f54841,f120]) ).
fof(f60111,plain,
! [X0] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),sF12)) = addition(multiplication(one,sF12),multiplication(coantidomain(X0),sF2)),
inference(forward_demodulation,[],[f59840,f3]) ).
fof(f60113,plain,
! [X0] : addition(antidomain(X0),multiplication(antidomain(antidomain(X0)),sF12)) = addition(multiplication(one,sF12),multiplication(antidomain(X0),sF2)),
inference(forward_demodulation,[],[f59833,f3]) ).
fof(f60235,plain,
! [X0] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),sF12)) = addition(sF12,multiplication(coantidomain(X0),sF2)),
inference(forward_demodulation,[],[f60111,f9]) ).
fof(f60236,plain,
! [X0] : addition(antidomain(X0),multiplication(antidomain(antidomain(X0)),sF12)) = addition(sF12,multiplication(antidomain(X0),sF2)),
inference(forward_demodulation,[],[f60113,f9]) ).
fof(f76171,plain,
! [X0] : addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),sF12)) = addition(coantidomain(X0),sF12),
inference(superposition,[],[f55580,f84]) ).
fof(f76175,plain,
! [X0] : addition(coantidomain(X0),zero) = addition(coantidomain(X0),antidomain(antidomain(coantidomain(coantidomain(coantidomain(X0)))))),
inference(superposition,[],[f55580,f7351]) ).
fof(f76176,plain,
! [X0] : addition(coantidomain(antidomain(antidomain(X0))),antidomain(X0)) = addition(coantidomain(antidomain(antidomain(X0))),zero),
inference(superposition,[],[f55580,f2455]) ).
fof(f76239,plain,
! [X0] : coantidomain(antidomain(antidomain(X0))) = addition(coantidomain(antidomain(antidomain(X0))),antidomain(X0)),
inference(forward_demodulation,[],[f76176,f5]) ).
fof(f76240,plain,
! [X0] : addition(coantidomain(X0),zero) = addition(coantidomain(X0),antidomain(antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f76175,f2273]) ).
fof(f76244,plain,
! [X0] : addition(sF12,coantidomain(X0)) = addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),sF12)),
inference(forward_demodulation,[],[f76171,f3]) ).
fof(f76287,plain,
! [X0] : coantidomain(antidomain(antidomain(X0))) = addition(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(forward_demodulation,[],[f76239,f3]) ).
fof(f76288,plain,
! [X0] : coantidomain(X0) = addition(coantidomain(X0),antidomain(antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f76240,f5]) ).
fof(f76289,plain,
! [X0] : addition(sF12,coantidomain(X0)) = addition(sF12,multiplication(coantidomain(X0),sF2)),
inference(backward_demodulation,[],[f60235,f76244]) ).
fof(f76327,plain,
addition(sF12,zero) = addition(sF12,coantidomain(coantidomain(antidomain(sF2)))),
inference(superposition,[],[f76289,f2455]) ).
fof(f76393,plain,
addition(sF12,zero) = addition(sF12,coantidomain(coantidomain(sF12))),
inference(forward_demodulation,[],[f76327,f84]) ).
fof(f76431,plain,
sF12 = addition(sF12,coantidomain(coantidomain(sF12))),
inference(forward_demodulation,[],[f76393,f5]) ).
fof(f76859,plain,
! [X0,X1] : addition(X1,coantidomain(X0)) = addition(coantidomain(X0),addition(antidomain(antidomain(coantidomain(X0))),X1)),
inference(superposition,[],[f470,f76288]) ).
fof(f77683,plain,
! [X0] : addition(sF12,antidomain(X0)) = addition(sF12,multiplication(antidomain(sF12),antidomain(X0))),
inference(superposition,[],[f55581,f84]) ).
fof(f77696,plain,
! [X0] : addition(antidomain(X0),multiplication(antidomain(antidomain(X0)),sF12)) = addition(antidomain(X0),sF12),
inference(superposition,[],[f55581,f84]) ).
fof(f77775,plain,
! [X0] : addition(sF12,antidomain(X0)) = addition(antidomain(X0),multiplication(antidomain(antidomain(X0)),sF12)),
inference(forward_demodulation,[],[f77696,f3]) ).
fof(f77785,plain,
! [X0] : addition(sF12,antidomain(X0)) = addition(sF12,multiplication(sF2,antidomain(X0))),
inference(forward_demodulation,[],[f77683,f3715]) ).
fof(f77815,plain,
! [X0] : addition(sF12,antidomain(X0)) = addition(sF12,multiplication(antidomain(X0),sF2)),
inference(backward_demodulation,[],[f60236,f77775]) ).
fof(f77852,plain,
! [X0] : multiplication(sF2,multiplication(antidomain(X0),sF2)) = multiplication(sF2,addition(sF12,antidomain(X0))),
inference(superposition,[],[f3807,f77815]) ).
fof(f77909,plain,
! [X0] : multiplication(sF2,antidomain(X0)) = multiplication(sF2,multiplication(antidomain(X0),sF2)),
inference(forward_demodulation,[],[f77852,f3807]) ).
fof(f78573,plain,
addition(coantidomain(sF2),sF12) = multiplication(coantidomain(sF2),addition(sF12,one)),
inference(superposition,[],[f401,f31028]) ).
fof(f78612,plain,
addition(coantidomain(sF2),sF12) = multiplication(coantidomain(sF2),one),
inference(forward_demodulation,[],[f78573,f1649]) ).
fof(f78635,plain,
coantidomain(sF2) = addition(coantidomain(sF2),sF12),
inference(forward_demodulation,[],[f78612,f8]) ).
fof(f78650,plain,
coantidomain(sF2) = addition(sF12,coantidomain(sF2)),
inference(forward_demodulation,[],[f78635,f3]) ).
fof(f82531,plain,
multiplication(addition(sF8,sF25),coantidomain(sF8)) = multiplication(coantidomain(sF2),multiplication(addition(sF8,sF25),coantidomain(sF8))),
inference(superposition,[],[f6198,f51128]) ).
fof(f82537,plain,
multiplication(sF25,coantidomain(sF8)) = multiplication(coantidomain(sF2),multiplication(sF25,coantidomain(sF8))),
inference(forward_demodulation,[],[f82531,f319]) ).
fof(f82562,plain,
multiplication(sF25,sF9) = multiplication(coantidomain(sF2),multiplication(sF25,sF9)),
inference(forward_demodulation,[],[f82537,f77]) ).
fof(f86099,plain,
! [X0] : multiplication(addition(sF16,X0),sF1) = addition(sF16,multiplication(addition(sF16,X0),sF1)),
inference(superposition,[],[f54799,f2382]) ).
fof(f86681,plain,
! [X0] : addition(sF16,multiplication(X0,sF1)) = multiplication(addition(sF16,X0),sF1),
inference(forward_demodulation,[],[f86099,f55304]) ).
fof(f88537,plain,
addition(sF16,multiplication(multiplication(sF4,sF22),sF1)) = addition(multiplication(sF16,sF0),multiplication(sF16,sF1)),
inference(superposition,[],[f54849,f36509]) ).
fof(f88546,plain,
addition(sF16,multiplication(multiplication(sF4,sF22),sF1)) = multiplication(sF16,addition(sF0,sF1)),
inference(forward_demodulation,[],[f88537,f10]) ).
fof(f88567,plain,
multiplication(sF16,one) = addition(sF16,multiplication(multiplication(sF4,sF22),sF1)),
inference(forward_demodulation,[],[f88546,f487]) ).
fof(f88582,plain,
multiplication(sF16,one) = multiplication(addition(sF16,multiplication(sF4,sF22)),sF1),
inference(forward_demodulation,[],[f88567,f86681]) ).
fof(f88589,plain,
multiplication(sF16,one) = multiplication(sF16,sF1),
inference(forward_demodulation,[],[f88582,f36509]) ).
fof(f88593,plain,
sF16 = multiplication(sF16,sF1),
inference(forward_demodulation,[],[f88589,f8]) ).
fof(f91082,plain,
! [X0] : multiplication(addition(sF12,antidomain(X0)),sF2) = multiplication(multiplication(sF2,antidomain(X0)),sF2),
inference(superposition,[],[f3571,f77785]) ).
fof(f91148,plain,
! [X0] : multiplication(addition(sF12,antidomain(X0)),sF2) = multiplication(sF2,multiplication(antidomain(X0),sF2)),
inference(forward_demodulation,[],[f91082,f7]) ).
fof(f91175,plain,
! [X0] : multiplication(sF2,antidomain(X0)) = multiplication(addition(sF12,antidomain(X0)),sF2),
inference(forward_demodulation,[],[f91148,f77909]) ).
fof(f91182,plain,
! [X0] : multiplication(sF2,antidomain(X0)) = multiplication(antidomain(X0),sF2),
inference(forward_demodulation,[],[f91175,f3571]) ).
fof(f100718,plain,
! [X0,X1] : multiplication(coantidomain(X0),addition(one,coantidomain(addition(X0,X1)))) = addition(coantidomain(X0),coantidomain(addition(X0,X1))),
inference(superposition,[],[f394,f31058]) ).
fof(f100759,plain,
! [X0,X1] : multiplication(coantidomain(X0),one) = addition(coantidomain(X0),coantidomain(addition(X0,X1))),
inference(forward_demodulation,[],[f100718,f885]) ).
fof(f100889,plain,
! [X0,X1] : coantidomain(X0) = addition(coantidomain(X0),coantidomain(addition(X0,X1))),
inference(forward_demodulation,[],[f100759,f8]) ).
fof(f100935,plain,
! [X0,X1] : coantidomain(X1) = addition(coantidomain(X1),coantidomain(addition(X0,X1))),
inference(superposition,[],[f100889,f854]) ).
fof(f101778,plain,
! [X0] : coantidomain(antidomain(antidomain(coantidomain(X0)))) = addition(coantidomain(antidomain(antidomain(coantidomain(X0)))),coantidomain(coantidomain(X0))),
inference(superposition,[],[f100935,f76288]) ).
fof(f102248,plain,
! [X0] : coantidomain(antidomain(antidomain(coantidomain(X0)))) = addition(coantidomain(coantidomain(X0)),coantidomain(antidomain(antidomain(coantidomain(X0))))),
inference(forward_demodulation,[],[f101778,f3]) ).
fof(f108406,plain,
! [X0,X1] : addition(multiplication(coantidomain(X0),coantidomain(X1)),coantidomain(coantidomain(X1))) = addition(multiplication(coantidomain(coantidomain(X0)),coantidomain(coantidomain(X1))),multiplication(coantidomain(X0),one)),
inference(superposition,[],[f54924,f120]) ).
fof(f109063,plain,
! [X0,X1] : addition(multiplication(coantidomain(X0),coantidomain(X1)),coantidomain(coantidomain(X1))) = addition(multiplication(coantidomain(X0),one),multiplication(coantidomain(coantidomain(X0)),coantidomain(coantidomain(X1)))),
inference(forward_demodulation,[],[f108406,f3]) ).
fof(f109462,plain,
! [X0,X1] : addition(multiplication(coantidomain(X0),coantidomain(X1)),coantidomain(coantidomain(X1))) = addition(coantidomain(X0),multiplication(coantidomain(coantidomain(X0)),coantidomain(coantidomain(X1)))),
inference(forward_demodulation,[],[f109063,f8]) ).
fof(f109658,plain,
! [X0,X1] : addition(coantidomain(X0),coantidomain(coantidomain(X1))) = addition(multiplication(coantidomain(X0),coantidomain(X1)),coantidomain(coantidomain(X1))),
inference(forward_demodulation,[],[f109462,f56227]) ).
fof(f109787,plain,
! [X0,X1] : addition(coantidomain(X0),coantidomain(coantidomain(X1))) = addition(coantidomain(coantidomain(X1)),multiplication(coantidomain(X0),coantidomain(X1))),
inference(forward_demodulation,[],[f109658,f3]) ).
fof(f166823,plain,
sF2 = multiplication(antidomain(antidomain(coantidomain(sF12))),sF2),
inference(superposition,[],[f3670,f31049]) ).
fof(f167165,plain,
sF2 = multiplication(sF2,antidomain(antidomain(coantidomain(sF12)))),
inference(forward_demodulation,[],[f166823,f91182]) ).
fof(f172650,plain,
! [X0] : addition(antidomain(antidomain(coantidomain(X0))),X0) = addition(antidomain(antidomain(coantidomain(X0))),addition(X0,coantidomain(X0))),
inference(superposition,[],[f1338,f3636]) ).
fof(f173178,plain,
! [X0] : addition(antidomain(antidomain(coantidomain(X0))),X0) = addition(coantidomain(X0),addition(antidomain(antidomain(coantidomain(X0))),X0)),
inference(forward_demodulation,[],[f172650,f470]) ).
fof(f173320,plain,
! [X0] : addition(X0,coantidomain(X0)) = addition(antidomain(antidomain(coantidomain(X0))),X0),
inference(forward_demodulation,[],[f173178,f76859]) ).
fof(f173436,plain,
! [X0] : addition(X0,coantidomain(X0)) = addition(X0,antidomain(antidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f173320,f3]) ).
fof(f173809,plain,
multiplication(sF2,antidomain(antidomain(coantidomain(sF12)))) = multiplication(sF2,addition(sF12,coantidomain(sF12))),
inference(superposition,[],[f3807,f173436]) ).
fof(f173877,plain,
multiplication(sF2,coantidomain(sF12)) = multiplication(sF2,antidomain(antidomain(coantidomain(sF12)))),
inference(forward_demodulation,[],[f173809,f3807]) ).
fof(f174035,plain,
sF2 = multiplication(sF2,coantidomain(sF12)),
inference(forward_demodulation,[],[f173877,f167165]) ).
fof(f174162,plain,
sF2 = coantidomain(sF12),
inference(backward_demodulation,[],[f1464,f174035]) ).
fof(f174354,plain,
sF12 = addition(sF12,coantidomain(sF2)),
inference(backward_demodulation,[],[f76431,f174162]) ).
fof(f174557,plain,
sF12 = coantidomain(sF2),
inference(backward_demodulation,[],[f78650,f174354]) ).
fof(f174754,plain,
multiplication(sF25,sF9) = multiplication(sF12,multiplication(sF25,sF9)),
inference(backward_demodulation,[],[f82562,f174557]) ).
fof(f212626,plain,
! [X0] : addition(antidomain(X0),zero) = addition(antidomain(X0),coantidomain(antidomain(antidomain(X0)))),
inference(superposition,[],[f56228,f28]) ).
fof(f212730,plain,
! [X0] : coantidomain(antidomain(antidomain(X0))) = addition(antidomain(X0),zero),
inference(forward_demodulation,[],[f212626,f76287]) ).
fof(f212792,plain,
! [X0] : antidomain(X0) = coantidomain(antidomain(antidomain(X0))),
inference(forward_demodulation,[],[f212730,f5]) ).
fof(f212835,plain,
! [X0] : antidomain(coantidomain(X0)) = addition(coantidomain(coantidomain(X0)),antidomain(coantidomain(X0))),
inference(backward_demodulation,[],[f102248,f212792]) ).
fof(f212846,plain,
! [X0] : coantidomain(coantidomain(X0)) = antidomain(coantidomain(X0)),
inference(forward_demodulation,[],[f212835,f45711]) ).
fof(f220899,plain,
coantidomain(sF13) = antidomain(sF13),
inference(superposition,[],[f212846,f34673]) ).
fof(f220972,plain,
sF14 = antidomain(sF13),
inference(forward_demodulation,[],[f220899,f88]) ).
fof(f221435,plain,
sF16 = multiplication(coantidomain(sF14),sF16),
inference(backward_demodulation,[],[f45074,f220972]) ).
fof(f222383,plain,
sF16 = multiplication(sF13,sF16),
inference(forward_demodulation,[],[f221435,f34673]) ).
fof(f223593,plain,
sF16 = multiplication(sF4,sF16),
inference(backward_demodulation,[],[f50138,f222383]) ).
fof(f223903,plain,
! [X0] : addition(sF16,multiplication(sF13,X0)) = multiplication(sF13,addition(X0,sF16)),
inference(backward_demodulation,[],[f50747,f223593]) ).
fof(f224047,plain,
! [X0] : multiplication(sF13,addition(X0,sK1_goals_X0)) = multiplication(sF13,addition(X0,sF16)),
inference(backward_demodulation,[],[f34680,f223903]) ).
fof(f224108,plain,
sF16 = multiplication(sF13,addition(sF25,sF16)),
inference(backward_demodulation,[],[f45606,f224047]) ).
fof(f224185,plain,
sF16 = multiplication(sF13,addition(sF16,sF25)),
inference(forward_demodulation,[],[f224108,f1905]) ).
fof(f224198,plain,
sF16 = multiplication(sF13,addition(sF16,sF24)),
inference(forward_demodulation,[],[f224185,f45614]) ).
fof(f224202,plain,
sF16 = multiplication(sF13,sF24),
inference(forward_demodulation,[],[f224198,f40647]) ).
fof(f227842,plain,
multiplication(addition(sF4,sF13),sF24) = addition(sF25,sF16),
inference(superposition,[],[f31950,f224202]) ).
fof(f227845,plain,
! [X0] : multiplication(sF16,X0) = multiplication(sF13,multiplication(sF24,X0)),
inference(superposition,[],[f7,f224202]) ).
fof(f227912,plain,
! [X0] : multiplication(sF16,X0) = multiplication(sF12,multiplication(sF25,X0)),
inference(backward_demodulation,[],[f33651,f227845]) ).
fof(f227914,plain,
multiplication(addition(sF4,sF13),sF24) = addition(sF16,sF25),
inference(forward_demodulation,[],[f227842,f3]) ).
fof(f227944,plain,
multiplication(sF25,sF9) = multiplication(sF16,sF9),
inference(backward_demodulation,[],[f174754,f227912]) ).
fof(f227948,plain,
multiplication(sF4,sF24) = addition(sF16,sF25),
inference(forward_demodulation,[],[f227914,f1661]) ).
fof(f227993,plain,
sF25 = addition(sF16,sF25),
inference(forward_demodulation,[],[f227948,f31947]) ).
fof(f228058,plain,
addition(sF16,multiplication(sF25,sF10)) = addition(multiplication(sF16,sF9),multiplication(sF25,sF10)),
inference(superposition,[],[f54819,f227993]) ).
fof(f241197,plain,
! [X0] : addition(multiplication(sF16,sF9),multiplication(sF25,X0)) = multiplication(sF25,addition(X0,sF9)),
inference(superposition,[],[f320,f227944]) ).
fof(f241253,plain,
addition(sF16,multiplication(sF25,sF10)) = multiplication(sF25,addition(sF10,sF9)),
inference(backward_demodulation,[],[f228058,f241197]) ).
fof(f241273,plain,
addition(sF16,multiplication(sF25,sF10)) = multiplication(sF25,addition(sF9,sF10)),
inference(forward_demodulation,[],[f241253,f1905]) ).
fof(f241286,plain,
multiplication(sF25,one) = addition(sF16,multiplication(sF25,sF10)),
inference(forward_demodulation,[],[f241273,f547]) ).
fof(f241287,plain,
sF25 = addition(sF16,multiplication(sF25,sF10)),
inference(forward_demodulation,[],[f241286,f8]) ).
fof(f284942,plain,
addition(multiplication(sF25,sF10),multiplication(sF16,sF1)) = addition(multiplication(sF25,sF10),multiplication(sF25,sF1)),
inference(superposition,[],[f56475,f241287]) ).
fof(f284965,plain,
addition(multiplication(sF25,sF10),multiplication(sF16,sF1)) = multiplication(sF25,addition(sF10,sF1)),
inference(forward_demodulation,[],[f284942,f10]) ).
fof(f285003,plain,
multiplication(sF25,sF1) = addition(multiplication(sF25,sF10),multiplication(sF16,sF1)),
inference(forward_demodulation,[],[f284965,f121]) ).
fof(f285029,plain,
multiplication(sF25,sF1) = addition(multiplication(sF16,sF1),multiplication(sF25,sF10)),
inference(forward_demodulation,[],[f285003,f3]) ).
fof(f285044,plain,
multiplication(sF25,sF1) = addition(sF16,multiplication(sF25,sF10)),
inference(forward_demodulation,[],[f285029,f88593]) ).
fof(f285051,plain,
sF25 = multiplication(sF25,sF1),
inference(forward_demodulation,[],[f285044,f241287]) ).
fof(f302887,plain,
! [X0,X1] : multiplication(multiplication(coantidomain(coantidomain(X0)),coantidomain(X1)),coantidomain(coantidomain(X0))) = multiplication(addition(coantidomain(X0),coantidomain(X1)),coantidomain(coantidomain(X0))),
inference(superposition,[],[f319,f56227]) ).
fof(f302968,plain,
! [X0,X1] : multiplication(coantidomain(X1),coantidomain(coantidomain(X0))) = multiplication(multiplication(coantidomain(coantidomain(X0)),coantidomain(X1)),coantidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f302887,f319]) ).
fof(f303055,plain,
! [X0,X1] : multiplication(coantidomain(X1),coantidomain(coantidomain(X0))) = multiplication(coantidomain(coantidomain(X0)),multiplication(coantidomain(X1),coantidomain(coantidomain(X0)))),
inference(forward_demodulation,[],[f302968,f7]) ).
fof(f403109,plain,
! [X0,X1] : multiplication(coantidomain(X1),multiplication(coantidomain(X0),coantidomain(X1))) = multiplication(coantidomain(X1),addition(coantidomain(X0),coantidomain(coantidomain(X1)))),
inference(superposition,[],[f373,f109787]) ).
fof(f403218,plain,
! [X0,X1] : multiplication(coantidomain(X1),coantidomain(X0)) = multiplication(coantidomain(X1),multiplication(coantidomain(X0),coantidomain(X1))),
inference(forward_demodulation,[],[f403109,f158]) ).
fof(f403293,plain,
! [X0,X1] : multiplication(coantidomain(coantidomain(X0)),coantidomain(X1)) = multiplication(coantidomain(X1),coantidomain(coantidomain(X0))),
inference(backward_demodulation,[],[f303055,f403218]) ).
fof(f403356,plain,
! [X0,X1] : one = coantidomain(multiplication(coantidomain(X1),coantidomain(coantidomain(multiplication(X0,X1))))),
inference(backward_demodulation,[],[f22587,f403293]) ).
fof(f620110,plain,
one = coantidomain(multiplication(coantidomain(sF1),coantidomain(coantidomain(sF25)))),
inference(superposition,[],[f403356,f285051]) ).
fof(f621162,plain,
one = coantidomain(multiplication(coantidomain(sF1),coantidomain(sF26))),
inference(forward_demodulation,[],[f620110,f113]) ).
fof(f621627,plain,
one = coantidomain(multiplication(coantidomain(sF1),sF27)),
inference(forward_demodulation,[],[f621162,f115]) ).
fof(f621910,plain,
one = coantidomain(multiplication(sF0,sF27)),
inference(forward_demodulation,[],[f621627,f58350]) ).
fof(f622058,plain,
multiplication(sF1,one) = multiplication(sF28,one),
inference(backward_demodulation,[],[f58570,f621910]) ).
fof(f622191,plain,
sF28 = multiplication(sF1,one),
inference(forward_demodulation,[],[f622058,f8]) ).
fof(f622265,plain,
sF1 = sF28,
inference(forward_demodulation,[],[f622191,f8]) ).
fof(f622318,plain,
$false,
inference(forward_subsumption_resolution,[],[f622265,f118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE122-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 13:11:21 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 92.76/14.18 % (3512224)Detected a unit-equality problem, will run specialized UEQ schedule.
% 92.76/14.18 % (3512258)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=957036406:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 92.76/14.18 % (3512256)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=3159244599:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 92.76/14.18 % (3512257)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3552116377:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 92.76/14.18 % (3512261)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3348582588:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 92.76/14.18 % (3512262)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=370591869:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 92.76/14.18 % (3512260)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3233215629:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 92.76/14.18 % (3512259)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2032950119:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 92.76/14.18 % (3512259)Instruction limit reached!
% 92.76/14.18 % (3512259)------------------------------
% 92.76/14.18 % (3512259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.76/14.18 % (3512259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.76/14.18 % (3512259)CaDiCaL version: 2.1.3
% 92.76/14.18 % (3512259)Termination reason: Instruction limit
% 92.76/14.18 % (3512259)Termination phase: Saturation
% 92.76/14.18 % (3512259)Time elapsed: 0.138 s
% 92.76/14.18 % (3512259)Peak memory usage: 89 MB
% 92.76/14.18 % (3512259)Instructions burned: 136 (million)
% 92.76/14.18 % (3512260)Instruction limit reached!
% 92.76/14.18 % (3512260)------------------------------
% 92.76/14.18 % (3512260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.76/14.18 % (3512260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.76/14.18 % (3512260)CaDiCaL version: 2.1.3
% 92.76/14.18 % (3512260)Termination reason: Instruction limit
% 92.76/14.18 % (3512260)Termination phase: Saturation
% 92.76/14.18 % (3512260)Time elapsed: 0.187 s
% 92.76/14.18 % (3512260)Peak memory usage: 90 MB
% 92.76/14.18 % (3512260)Instructions burned: 181 (million)
% 92.76/14.18 % (3512261)Instruction limit reached!
% 92.76/14.18 % (3512261)------------------------------
% 92.76/14.18 % (3512261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.76/14.18 % (3512261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.76/14.18 % (3512261)CaDiCaL version: 2.1.3
% 92.76/14.18 % (3512261)Termination reason: Instruction limit
% 92.76/14.18 % (3512261)Termination phase: Saturation
% 92.76/14.18 % (3512261)Time elapsed: 0.288 s
% 92.76/14.18 % (3512261)Peak memory usage: 91 MB
% 92.76/14.18 % (3512261)Instructions burned: 257 (million)
% 92.76/14.18 % (3512270)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=4167936294:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2995 on theBenchmark for (2995ds/2051Mi)
% 92.76/14.18 % (3512271)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=732250297:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 92.76/14.18 % (3512272)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1574609736:i=215:ep=RSTC_2994 on theBenchmark for (2994ds/215Mi)
% 92.76/14.18 % (3512272)Instruction limit reached!
% 92.76/14.18 % (3512272)------------------------------
% 92.76/14.18 % (3512272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.76/14.18 % (3512272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.76/14.18 % (3512272)CaDiCaL version: 2.1.3
% 92.76/14.18 % (3512272)Termination reason: Instruction limit
% 92.76/14.18 % (3512272)Termination phase: Saturation
% 92.76/14.18 % (3512272)Time elapsed: 0.186 s
% 152.88/22.64 % (3512272)Peak memory usage: 93 MB
% 152.88/22.64 % (3512272)Instructions burned: 217 (million)
% 152.88/22.64 % (3512276)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=170809176:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/317Mi)
% 152.88/22.64 % (3512262)Instruction limit reached!
% 152.88/22.64 % (3512262)------------------------------
% 152.88/22.64 % (3512262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.88/22.64 % (3512262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.88/22.64 % (3512262)CaDiCaL version: 2.1.3
% 152.88/22.64 % (3512262)Termination reason: Instruction limit
% 152.88/22.64 % (3512262)Termination phase: Saturation
% 152.88/22.64 % (3512262)Time elapsed: 1.104 s
% 152.88/22.64 % (3512262)Peak memory usage: 99 MB
% 152.88/22.64 % (3512262)Instructions burned: 1187 (million)
% 152.88/22.64 % (3512278)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=1050771430:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/12125Mi)
% 152.88/22.64 % (3512276)Instruction limit reached!
% 152.88/22.64 % (3512276)------------------------------
% 152.88/22.64 % (3512276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.88/22.64 % (3512276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.88/22.64 % (3512276)CaDiCaL version: 2.1.3
% 152.88/22.64 % (3512276)Termination reason: Instruction limit
% 152.88/22.64 % (3512276)Termination phase: Saturation
% 152.88/22.64 % (3512276)Time elapsed: 0.274 s
% 152.88/22.64 % (3512276)Peak memory usage: 95 MB
% 152.88/22.64 % (3512276)Instructions burned: 317 (million)
% 152.88/22.64 % (3512280)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3006933527:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2983 on theBenchmark for (2983ds/2836Mi)
% 152.88/22.64 % (3512270)Instruction limit reached!
% 152.88/22.64 % (3512270)------------------------------
% 152.88/22.64 % (3512270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.88/22.64 % (3512270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.88/22.64 % (3512270)CaDiCaL version: 2.1.3
% 152.88/22.64 % (3512270)Termination reason: Instruction limit
% 152.88/22.64 % (3512270)Termination phase: Saturation
% 152.88/22.64 % (3512270)Time elapsed: 1.663 s
% 152.88/22.64 % (3512270)Peak memory usage: 142 MB
% 152.88/22.64 % (3512270)Instructions burned: 2051 (million)
% 152.88/22.64 % (3512434)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=580611652:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2975 on theBenchmark for (2975ds/14534Mi)
% 152.88/22.64 % (3512280)Instruction limit reached!
% 152.88/22.64 % (3512280)------------------------------
% 152.88/22.64 % (3512280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.88/22.64 % (3512280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.88/22.64 % (3512280)CaDiCaL version: 2.1.3
% 152.88/22.64 % (3512280)Termination reason: Instruction limit
% 152.88/22.64 % (3512280)Termination phase: Saturation
% 152.88/22.64 % (3512280)Time elapsed: 1.728 s
% 152.88/22.64 % (3512280)Peak memory usage: 138 MB
% 152.88/22.64 % (3512280)Instructions burned: 2837 (million)
% 152.88/22.64 % (3512436)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=4113053676:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2964 on theBenchmark for (2964ds/11832Mi)
% 152.88/22.64 % (3512271)Instruction limit reached!
% 152.88/22.64 % (3512271)------------------------------
% 152.88/22.64 % (3512271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.88/22.64 % (3512271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.88/22.64 % (3512271)CaDiCaL version: 2.1.3
% 152.88/22.64 % (3512271)Termination reason: Instruction limit
% 152.88/22.64 % (3512271)Termination phase: Saturation
% 152.88/22.64 % (3512271)Time elapsed: 3.253 s
% 152.88/22.64 % (3512271)Peak memory usage: 168 MB
% 152.88/22.64 % (3512271)Instructions burned: 4948 (million)
% 152.88/22.64 % (3512438)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=3155911297:i=2279:fgj=on:bd=all_2959 on theBenchmark for (2959ds/2279Mi)
% 152.88/22.64 % (3512438)Instruction limit reached!
% 152.88/22.64 % (3512438)------------------------------
% 117.42/29.25 % (3512438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512438)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512438)Termination reason: Instruction limit
% 117.42/29.25 % (3512438)Termination phase: Saturation
% 117.42/29.25 % (3512438)Time elapsed: 1.420 s
% 117.42/29.25 % (3512438)Peak memory usage: 138 MB
% 117.42/29.25 % (3512438)Instructions burned: 2280 (million)
% 117.42/29.25 % (3512440)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=2578405979:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2943 on theBenchmark for (2943ds/6225Mi)
% 117.42/29.25 % (3512278)Instruction limit reached!
% 117.42/29.25 % (3512278)------------------------------
% 117.42/29.25 % (3512278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512278)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512278)Termination reason: Instruction limit
% 117.42/29.25 % (3512278)Termination phase: Saturation
% 117.42/29.25 % (3512278)Time elapsed: 7.060 s
% 117.42/29.25 % (3512278)Peak memory usage: 247 MB
% 117.42/29.25 % (3512278)Instructions burned: 12125 (million)
% 117.42/29.25 % (3512442)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=1836498698:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2912 on theBenchmark for (2912ds/21755Mi)
% 117.42/29.25 % (3512440)Instruction limit reached!
% 117.42/29.25 % (3512440)------------------------------
% 117.42/29.25 % (3512440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512440)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512440)Termination reason: Instruction limit
% 117.42/29.25 % (3512440)Termination phase: Saturation
% 117.42/29.25 % (3512440)Time elapsed: 3.595 s
% 117.42/29.25 % (3512440)Peak memory usage: 169 MB
% 117.42/29.25 % (3512440)Instructions burned: 6226 (million)
% 117.42/29.25 % (3512444)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=3301579842:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2905 on theBenchmark for (2905ds/16427Mi)
% 117.42/29.25 % (3512436)Instruction limit reached!
% 117.42/29.25 % (3512436)------------------------------
% 117.42/29.25 % (3512436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512436)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512436)Termination reason: Instruction limit
% 117.42/29.25 % (3512436)Termination phase: Saturation
% 117.42/29.25 % (3512436)Time elapsed: 7.360 s
% 117.42/29.25 % (3512436)Peak memory usage: 230 MB
% 117.42/29.25 % (3512436)Instructions burned: 11833 (million)
% 117.42/29.25 % (3512446)lrs+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=221032617:i=9356:fgj=on:bd=preordered:av=off_2889 on theBenchmark for (2889ds/9356Mi)
% 117.42/29.25 % (3512434)Instruction limit reached!
% 117.42/29.25 % (3512434)------------------------------
% 117.42/29.25 % (3512434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512434)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512434)Termination reason: Instruction limit
% 117.42/29.25 % (3512434)Termination phase: Saturation
% 117.42/29.25 % (3512434)Time elapsed: 9.033 s
% 117.42/29.25 % (3512434)Peak memory usage: 246 MB
% 117.42/29.25 % (3512434)Instructions burned: 14535 (million)
% 117.42/29.25 % (3512448)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=3234629130:i=2070:kws=inv_precedence:slsql=off:bd=all_2883 on theBenchmark for (2883ds/2070Mi)
% 117.42/29.25 % (3512448)Instruction limit reached!
% 117.42/29.25 % (3512448)------------------------------
% 117.42/29.25 % (3512448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512448)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512448)Termination reason: Instruction limit
% 117.42/29.25 % (3512448)Termination phase: Saturation
% 117.42/29.25 % (3512448)Time elapsed: 1.210 s
% 117.42/29.25 % (3512448)Peak memory usage: 133 MB
% 117.42/29.25 % (3512448)Instructions burned: 2071 (million)
% 117.42/29.25 % (3512496)lrs+1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=8000:tgt=ground:npcc=on:fde=unused:sp=const_min:urr=ec_only:s2agt=32:random_seed=2767488377:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2869 on theBenchmark for (2869ds/6461Mi)
% 117.42/29.25 % (3512446)Instruction limit reached!
% 117.42/29.25 % (3512446)------------------------------
% 117.42/29.25 % (3512446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512446)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512446)Termination reason: Instruction limit
% 117.42/29.25 % (3512446)Termination phase: Saturation
% 117.42/29.25 % (3512446)Time elapsed: 6.033 s
% 117.42/29.25 % (3512446)Peak memory usage: 209 MB
% 117.42/29.25 % (3512446)Instructions burned: 9356 (million)
% 117.42/29.25 % (3512896)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=2913973700:i=2310:bd=all:ss=included_2826 on theBenchmark for (2826ds/2310Mi)
% 117.42/29.25 % (3512496)Instruction limit reached!
% 117.42/29.25 % (3512496)------------------------------
% 117.42/29.25 % (3512496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512496)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512496)Termination reason: Instruction limit
% 117.42/29.25 % (3512496)Termination phase: Saturation
% 117.42/29.25 % (3512496)Time elapsed: 4.381 s
% 117.42/29.25 % (3512496)Peak memory usage: 175 MB
% 117.42/29.25 % (3512496)Instructions burned: 6462 (million)
% 117.42/29.25 % (3512898)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=510956275:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2824 on theBenchmark for (2824ds/2616Mi)
% 117.42/29.25 % (3512896)Instruction limit reached!
% 117.42/29.25 % (3512896)------------------------------
% 117.42/29.25 % (3512896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512896)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512896)Termination reason: Instruction limit
% 117.42/29.25 % (3512896)Termination phase: Saturation
% 117.42/29.25 % (3512896)Time elapsed: 1.295 s
% 117.42/29.25 % (3512896)Peak memory usage: 106 MB
% 117.42/29.25 % (3512896)Instructions burned: 2311 (million)
% 117.42/29.25 % (3512900)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=2675300990:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2812 on theBenchmark for (2812ds/30521Mi)
% 117.42/29.25 % (3512898)Instruction limit reached!
% 117.42/29.25 % (3512898)------------------------------
% 117.42/29.25 % (3512898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512898)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512898)Termination reason: Instruction limit
% 117.42/29.25 % (3512898)Termination phase: Saturation
% 117.42/29.25 % (3512898)Time elapsed: 1.487 s
% 117.42/29.25 % (3512898)Peak memory usage: 112 MB
% 117.42/29.25 % (3512898)Instructions burned: 2617 (million)
% 117.42/29.25 % (3512902)lrs+11_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:tgt=full:npcc=on:prc=on:fde=unused:sp=reverse_frequency:spb=goal:acc=on:urr=ec_only:s2agt=32:random_seed=1946744973:i=3258:fgj=on:bd=all:ins=1_2807 on theBenchmark for (2807ds/3258Mi)
% 117.42/29.25 % (3512444)Instruction limit reached!
% 117.42/29.25 % (3512444)------------------------------
% 117.42/29.25 % (3512444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512444)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512444)Termination reason: Instruction limit
% 117.42/29.25 % (3512444)Termination phase: Saturation
% 117.42/29.25 % (3512444)Time elapsed: 10.556 s
% 117.42/29.25 % (3512444)Peak memory usage: 253 MB
% 117.42/29.25 % (3512444)Instructions burned: 16429 (million)
% 117.42/29.25 % (3512904)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=3312389658:i=5037:kws=precedence_2798 on theBenchmark for (2798ds/5037Mi)
% 117.42/29.25 % (3512902)Instruction limit reached!
% 117.42/29.25 % (3512902)------------------------------
% 117.42/29.25 % (3512902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512902)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512902)Termination reason: Instruction limit
% 117.42/29.25 % (3512902)Termination phase: Saturation
% 117.42/29.25 % (3512902)Time elapsed: 2.108 s
% 117.42/29.25 % (3512902)Peak memory usage: 153 MB
% 117.42/29.25 % (3512902)Instructions burned: 3258 (million)
% 117.42/29.25 % (3512906)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=1116237932:i=65240_2785 on theBenchmark for (2785ds/65240Mi)
% 117.42/29.25 % (3512442)Instruction limit reached!
% 117.42/29.25 % (3512442)------------------------------
% 117.42/29.25 % (3512442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512442)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512442)Termination reason: Instruction limit
% 117.42/29.25 % (3512442)Termination phase: Saturation
% 117.42/29.25 % (3512442)Time elapsed: 14.350 s
% 117.42/29.25 % (3512442)Peak memory usage: 298 MB
% 117.42/29.25 % (3512442)Instructions burned: 21757 (million)
% 117.42/29.25 % (3512904)Instruction limit reached!
% 117.42/29.25 % (3512904)------------------------------
% 117.42/29.25 % (3512904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.42/29.25 % (3512904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.42/29.25 % (3512904)CaDiCaL version: 2.1.3
% 117.42/29.25 % (3512904)Termination reason: Instruction limit
% 117.42/29.25 % (3512904)Termination phase: Saturation
% 117.42/29.25 % (3512904)Time elapsed: 3.009 s
% 117.42/29.25 % (3512904)Peak memory usage: 170 MB
% 117.42/29.25 % (3512904)Instructions burned: 5038 (million)
% 117.42/29.25 % (3512908)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=1378558485:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2767 on theBenchmark for (2767ds/16502Mi)
% 117.42/29.25 % (3512909)lrs-1011_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=32000:npcc=on:drc=off:sp=const_max:spb=goal_then_units:urr=ec_only:fd=preordered:random_seed=1275834546:i=7623:bd=preordered:er=filter_2766 on theBenchmark for (2766ds/7623Mi)
% 117.42/29.25 % (3512258)First to succeed.
% 117.42/29.25 % (3512258)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3512224"
% 117.42/29.25 % (3512258)Refutation found. Thanks to Tanya!
% 117.42/29.25 % SZS status Unsatisfiable for theBenchmark
% 117.42/29.25 % SZS output start Proof for theBenchmark
% See solution above
% 200.03/29.45 % (3512258)------------------------------
% 200.03/29.45 % (3512258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 200.03/29.45 % (3512258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.03/29.45 % (3512258)CaDiCaL version: 2.1.3
% 200.03/29.45 % (3512258)Termination reason: Refutation
% 200.03/29.45 % (3512258)Time elapsed: 27.584 s
% 200.03/29.45 % (3512258)Peak memory usage: 800 MB
% 200.03/29.45 % (3512258)Instructions burned: 75452 (million)
% 200.03/29.45 % (3512258)------------------------------
% 200.03/29.45 % (3512258)------------------------------
% 200.03/29.45 % (3512224)Success in time 28.089 s
% 200.03/29.45 % Vampire exiting
%------------------------------------------------------------------------------