Vampire---5.0.1.UNS-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : GRP054-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n007.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 10:12:15 AM UTC 2026

% Result   : Unsatisfiable 24.63s 4.30s
% Output   : Refutation 24.73s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2))) = X1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).

fof(f2,negated_conjecture,
    ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
    | multiply(multiply(inverse(b2),b2),a2) != a2
    | multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms) ).

fof(f3,plain,
    ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
    | a2 != multiply(multiply(inverse(b2),b2),a2)
    | multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
    inference(reorient_equations,[],[f2]) ).

fof(f4,definition,
    sF0 = inverse(a1),
    introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).

fof(f5,plain,
    inverse(a1) = sF0,
    inference(reorient_equations,[],[f4]) ).

fof(f6,definition,
    sF1 = multiply(sF0,a1),
    introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).

fof(f7,plain,
    multiply(sF0,a1) = sF1,
    inference(reorient_equations,[],[f6]) ).

fof(f8,definition,
    sF2 = inverse(b1),
    introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).

fof(f9,plain,
    inverse(b1) = sF2,
    inference(reorient_equations,[],[f8]) ).

fof(f10,definition,
    sF3 = multiply(sF2,b1),
    introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).

fof(f11,plain,
    multiply(sF2,b1) = sF3,
    inference(reorient_equations,[],[f10]) ).

fof(f12,definition,
    sF4 = inverse(b2),
    introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).

fof(f13,plain,
    inverse(b2) = sF4,
    inference(reorient_equations,[],[f12]) ).

fof(f14,definition,
    sF5 = multiply(sF4,b2),
    introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).

fof(f15,plain,
    multiply(sF4,b2) = sF5,
    inference(reorient_equations,[],[f14]) ).

fof(f16,definition,
    sF6 = multiply(sF5,a2),
    introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).

fof(f17,plain,
    multiply(sF5,a2) = sF6,
    inference(reorient_equations,[],[f16]) ).

fof(f18,definition,
    sF7 = multiply(a3,b3),
    introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).

fof(f19,plain,
    multiply(a3,b3) = sF7,
    inference(reorient_equations,[],[f18]) ).

fof(f20,definition,
    sF8 = multiply(sF7,c3),
    introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).

fof(f21,plain,
    multiply(sF7,c3) = sF8,
    inference(reorient_equations,[],[f20]) ).

fof(f22,definition,
    sF9 = multiply(b3,c3),
    introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).

fof(f23,plain,
    multiply(b3,c3) = sF9,
    inference(reorient_equations,[],[f22]) ).

fof(f24,definition,
    sF10 = multiply(a3,sF9),
    introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).

fof(f25,plain,
    multiply(a3,sF9) = sF10,
    inference(reorient_equations,[],[f24]) ).

fof(f26,plain,
    ( sF1 != sF3
    | a2 != sF6
    | sF8 != sF10 ),
    inference(definition_folding,[],[f3,f25,f23,f21,f19,f17,f15,f13,f11,f9,f7,f5]) ).

fof(f28,definition,
    ( spl11_1
  <=> sF8 = sF10 ),
    introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition]) ).

fof(f30,plain,
    ( sF8 != sF10
    | spl11_1 ),
    inference(avatar_component_clause,[],[f28]) ).

fof(f32,definition,
    ( spl11_2
  <=> a2 = sF6 ),
    introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition]) ).

fof(f36,definition,
    ( spl11_3
  <=> sF1 = sF3 ),
    introduced(definition,[new_symbols(definition,[spl11_3])],[avatar_definition]) ).

fof(f38,plain,
    ( sF1 != sF3
    | spl11_3 ),
    inference(avatar_component_clause,[],[f36]) ).

fof(f39,plain,
    ( ~ spl11_1
    | ~ spl11_2
    | ~ spl11_3 ),
    inference(avatar_split_clause,[],[f26,f36,f32,f28]) ).

fof(f40,plain,
    ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X2,X3)) = inverse(multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X1,X4))),
    inference(superposition,[],[f1,f1]) ).

fof(f42,plain,
    ! [X0] : inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF7)) = X0,
    inference(superposition,[],[f1,f19]) ).

fof(f44,plain,
    ! [X0] : inverse(multiply(inverse(multiply(sF4,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),sF5)) = X0,
    inference(superposition,[],[f1,f15]) ).

fof(f45,plain,
    ! [X0] : inverse(multiply(inverse(multiply(sF4,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(multiply(sF4,b2)))))))),sF5)) = X0,
    inference(forward_demodulation,[],[f44,f13]) ).

fof(f46,plain,
    ! [X0] : inverse(multiply(inverse(multiply(sF4,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),sF5)) = X0,
    inference(forward_demodulation,[],[f45,f15]) ).

fof(f49,plain,
    ! [X0,X1] : b1 = inverse(multiply(inverse(multiply(X0,inverse(multiply(sF2,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),multiply(X0,X1))),
    inference(superposition,[],[f1,f9]) ).

fof(f51,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(multiply(sF4,b2)))))))),multiply(X0,b2))) = X1,
    inference(superposition,[],[f1,f13]) ).

fof(f52,plain,
    ! [X0,X1] : b2 = inverse(multiply(inverse(multiply(X0,inverse(multiply(sF4,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),multiply(X0,X1))),
    inference(superposition,[],[f1,f13]) ).

fof(f53,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF5))))))),multiply(X0,b2))) = X1,
    inference(forward_demodulation,[],[f51,f15]) ).

fof(f55,plain,
    ! [X0,X1] : a1 = inverse(multiply(inverse(multiply(X0,inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),multiply(X0,X1))),
    inference(superposition,[],[f1,f5]) ).

fof(f57,plain,
    ! [X0] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(multiply(inverse(a1),a1)))))))),sF1)) = X0,
    inference(superposition,[],[f1,f7]) ).

fof(f58,plain,
    ! [X0] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(multiply(sF0,a1)))))))),sF1)) = X0,
    inference(forward_demodulation,[],[f57,f5]) ).

fof(f59,plain,
    ! [X0] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)) = X0,
    inference(forward_demodulation,[],[f58,f7]) ).

fof(f65,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(a1,inverse(sF1))))))),sF1)),
    inference(superposition,[],[f59,f1]) ).

fof(f66,plain,
    ! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(a1,inverse(sF1))))))),sF1)),
    inference(superposition,[],[f59,f59]) ).

fof(f72,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1),
    inference(forward_demodulation,[],[f65,f66]) ).

fof(f74,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)),
    inference(superposition,[],[f72,f59]) ).

fof(f82,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(multiply(sF4,b2)))))))),multiply(X0,b2)) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(a1,inverse(sF1))))))),sF1),
    inference(superposition,[],[f72,f13]) ).

fof(f86,plain,
    ! [X0] : multiply(inverse(multiply(b3,inverse(multiply(inverse(X0),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF9) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1),
    inference(superposition,[],[f72,f23]) ).

fof(f93,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X3),inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1))) = X3,
    inference(superposition,[],[f1,f72]) ).

fof(f97,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF5))))))),multiply(X0,b2)) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(a1,inverse(sF1))))))),sF1),
    inference(forward_demodulation,[],[f82,f15]) ).

fof(f187,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)) = X1,
    inference(superposition,[],[f1,f40]) ).

fof(f201,plain,
    ! [X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF1))))))),sF1) = X1,
    inference(forward_demodulation,[],[f187,f72]) ).

fof(f533,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X0)),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X1),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X0)) = X1,
    inference(superposition,[],[f1,f201]) ).

fof(f1808,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X0),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X2))),
    inference(superposition,[],[f1,f533]) ).

fof(f1817,plain,
    ! [X0,X1] : multiply(inverse(multiply(X1,X0)),multiply(X1,b2)) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF5))))),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X0),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),inverse(multiply(a1,inverse(sF1))))))),sF1),
    inference(superposition,[],[f97,f533]) ).

fof(f1819,plain,
    ! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF5))))),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X0),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(multiply(sF4,X0)),sF5)),
    inference(superposition,[],[f46,f533]) ).

fof(f1913,plain,
    ! [X0,X1] : multiply(inverse(multiply(X1,X0)),multiply(X1,b2)) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(multiply(inverse(multiply(sF4,X0)),sF5))),inverse(multiply(a1,inverse(sF1))))))),sF1),
    inference(forward_demodulation,[],[f1817,f1819]) ).

fof(f1967,plain,
    ! [X0,X1] : multiply(inverse(multiply(X1,X0)),multiply(X1,b2)) = multiply(inverse(multiply(sF4,X0)),sF5),
    inference(forward_demodulation,[],[f1913,f201]) ).

fof(f4383,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X2))),
    inference(superposition,[],[f1808,f1808]) ).

fof(f4477,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))) = X1,
    inference(superposition,[],[f533,f1808]) ).

fof(f5184,plain,
    ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X4,X1)),multiply(X4,X2)) = inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X3)),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X3)),
    inference(superposition,[],[f533,f4383]) ).

fof(f5192,plain,
    ! [X2,X0,X1,X4] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X4,X1)),multiply(X4,X2)),
    inference(forward_demodulation,[],[f5184,f533]) ).

fof(f5461,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,b3)),multiply(X0,X1)) = multiply(inverse(sF7),multiply(a3,X1)),
    inference(superposition,[],[f5192,f19]) ).

fof(f5462,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,sF9)),multiply(X0,X1)) = multiply(inverse(sF10),multiply(a3,X1)),
    inference(superposition,[],[f5192,f25]) ).

fof(f5466,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,b2)),multiply(X0,X1)) = multiply(inverse(sF5),multiply(sF4,X1)),
    inference(superposition,[],[f5192,f15]) ).

fof(f5477,plain,
    ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,X4)) = multiply(X0,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),X4)),
    inference(superposition,[],[f5192,f1]) ).

fof(f6244,plain,
    ! [X0] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)),multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)) = multiply(inverse(sF10),multiply(a3,sF9)),
    inference(superposition,[],[f5462,f86]) ).

fof(f6343,plain,
    ! [X0] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)),multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)) = multiply(inverse(sF10),sF10),
    inference(forward_demodulation,[],[f6244,f25]) ).

fof(f6359,plain,
    ! [X0] : multiply(X0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)) = multiply(inverse(sF10),sF10),
    inference(forward_demodulation,[],[f6343,f59]) ).

fof(f7287,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(X3,multiply(inverse(multiply(X1,inverse(multiply(inverse(X3),inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),X2)),
    inference(superposition,[],[f5477,f97]) ).

fof(f7290,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(sF5),multiply(sF4,X0))),multiply(inverse(multiply(X1,b2)),X2)) = multiply(X3,multiply(inverse(multiply(X1,inverse(multiply(inverse(X3),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(superposition,[],[f5477,f5466]) ).

fof(f7291,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(sF7),multiply(a3,X0))),multiply(inverse(multiply(X1,b3)),X2)) = multiply(X3,multiply(inverse(multiply(X1,inverse(multiply(inverse(X3),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(superposition,[],[f5477,f5461]) ).

fof(f7294,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(sF10),multiply(a3,X0))),multiply(inverse(multiply(X1,sF9)),X2)) = multiply(X3,multiply(inverse(multiply(X1,inverse(multiply(inverse(X3),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(superposition,[],[f5477,f5462]) ).

fof(f7303,plain,
    ! [X2,X3,X0,X1] : multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(X3,multiply(inverse(multiply(X1,inverse(multiply(inverse(X3),inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),X2)),
    inference(superposition,[],[f5477,f53]) ).

fof(f7306,plain,
    ! [X2,X3,X0,X1] : multiply(a1,multiply(inverse(multiply(X0,inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(X3,multiply(inverse(multiply(X0,inverse(multiply(inverse(X3),inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)),
    inference(superposition,[],[f5477,f55]) ).

fof(f7307,plain,
    ! [X2,X3,X0,X1] : multiply(b1,multiply(inverse(multiply(X0,inverse(multiply(sF2,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(X3,multiply(inverse(multiply(X0,inverse(multiply(inverse(X3),inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)),
    inference(superposition,[],[f5477,f49]) ).

fof(f7308,plain,
    ! [X2,X3,X0,X1] : multiply(b2,multiply(inverse(multiply(X0,inverse(multiply(sF4,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(X3,multiply(inverse(multiply(X0,inverse(multiply(inverse(X3),inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)),
    inference(superposition,[],[f5477,f52]) ).

fof(f7451,plain,
    ! [X2,X3,X0,X1] : multiply(X0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,X3))),
    inference(superposition,[],[f5477,f74]) ).

fof(f7594,plain,
    ! [X2,X3,X1] : multiply(inverse(sF10),sF10) = multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,X3))),
    inference(forward_demodulation,[],[f7451,f6359]) ).

fof(f7695,plain,
    ! [X2,X0,X1] : multiply(b1,multiply(inverse(multiply(X0,inverse(multiply(sF2,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(b2,multiply(inverse(multiply(X0,inverse(multiply(sF4,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)),
    inference(forward_demodulation,[],[f7307,f7308]) ).

fof(f7696,plain,
    ! [X2,X0,X1] : multiply(a1,multiply(inverse(multiply(X0,inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(b2,multiply(inverse(multiply(X0,inverse(multiply(sF4,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)),
    inference(forward_demodulation,[],[f7306,f7308]) ).

fof(f7699,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(b2,multiply(inverse(multiply(X1,inverse(multiply(sF4,inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),X2)),
    inference(forward_demodulation,[],[f7303,f7308]) ).

fof(f7707,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF10),multiply(a3,X0))),multiply(inverse(multiply(X1,sF9)),X2)) = multiply(b2,multiply(inverse(multiply(X1,inverse(multiply(sF4,inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(forward_demodulation,[],[f7294,f7308]) ).

fof(f7710,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF7),multiply(a3,X0))),multiply(inverse(multiply(X1,b3)),X2)) = multiply(b2,multiply(inverse(multiply(X1,inverse(multiply(sF4,inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(forward_demodulation,[],[f7291,f7308]) ).

fof(f7711,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),multiply(sF4,X0))),multiply(inverse(multiply(X1,b2)),X2)) = multiply(b2,multiply(inverse(multiply(X1,inverse(multiply(sF4,inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(forward_demodulation,[],[f7290,f7308]) ).

fof(f7714,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(b2,multiply(inverse(multiply(X1,inverse(multiply(sF4,inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),X2)),
    inference(forward_demodulation,[],[f7287,f7308]) ).

fof(f7821,plain,
    ! [X2,X0,X1] : multiply(a1,multiply(inverse(multiply(X0,inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(b1,multiply(inverse(multiply(X0,inverse(multiply(sF2,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)),
    inference(forward_demodulation,[],[f7696,f7695]) ).

fof(f7824,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(b1,multiply(inverse(multiply(X1,inverse(multiply(sF2,inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),X2)),
    inference(forward_demodulation,[],[f7699,f7695]) ).

fof(f7832,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF10),multiply(a3,X0))),multiply(inverse(multiply(X1,sF9)),X2)) = multiply(b1,multiply(inverse(multiply(X1,inverse(multiply(sF2,inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(forward_demodulation,[],[f7707,f7695]) ).

fof(f7835,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF7),multiply(a3,X0))),multiply(inverse(multiply(X1,b3)),X2)) = multiply(b1,multiply(inverse(multiply(X1,inverse(multiply(sF2,inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(forward_demodulation,[],[f7710,f7695]) ).

fof(f7836,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),multiply(sF4,X0))),multiply(inverse(multiply(X1,b2)),X2)) = multiply(b1,multiply(inverse(multiply(X1,inverse(multiply(sF2,inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(forward_demodulation,[],[f7711,f7695]) ).

fof(f7839,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(b1,multiply(inverse(multiply(X1,inverse(multiply(sF2,inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),X2)),
    inference(forward_demodulation,[],[f7714,f7695]) ).

fof(f7906,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(a1,multiply(inverse(multiply(X1,inverse(multiply(sF0,inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),X2)),
    inference(forward_demodulation,[],[f7824,f7821]) ).

fof(f7914,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF10),multiply(a3,X0))),multiply(inverse(multiply(X1,sF9)),X2)) = multiply(a1,multiply(inverse(multiply(X1,inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(forward_demodulation,[],[f7832,f7821]) ).

fof(f7917,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF7),multiply(a3,X0))),multiply(inverse(multiply(X1,b3)),X2)) = multiply(a1,multiply(inverse(multiply(X1,inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(forward_demodulation,[],[f7835,f7821]) ).

fof(f7918,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),multiply(sF4,X0))),multiply(inverse(multiply(X1,b2)),X2)) = multiply(a1,multiply(inverse(multiply(X1,inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),X2)),
    inference(forward_demodulation,[],[f7836,f7821]) ).

fof(f7921,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(a1,multiply(inverse(multiply(X1,inverse(multiply(sF0,inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),X2)),
    inference(forward_demodulation,[],[f7839,f7821]) ).

fof(f7978,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(a1,multiply(inverse(multiply(X1,inverse(multiply(sF0,inverse(multiply(b2,inverse(multiply(sF4,b2)))))))),X2)),
    inference(forward_demodulation,[],[f7906,f13]) ).

fof(f7987,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF7),multiply(a3,X0))),multiply(inverse(multiply(X1,b3)),X2)) = multiply(inverse(multiply(inverse(sF10),multiply(a3,X0))),multiply(inverse(multiply(X1,sF9)),X2)),
    inference(forward_demodulation,[],[f7917,f7914]) ).

fof(f7988,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),multiply(sF4,X0))),multiply(inverse(multiply(X1,b2)),X2)) = multiply(inverse(multiply(inverse(sF10),multiply(a3,X0))),multiply(inverse(multiply(X1,sF9)),X2)),
    inference(forward_demodulation,[],[f7918,f7914]) ).

fof(f7991,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(inverse(multiply(inverse(sF10),multiply(a3,b2))),multiply(inverse(multiply(X1,sF9)),X2)),
    inference(forward_demodulation,[],[f7921,f7914]) ).

fof(f8047,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(a1,multiply(inverse(multiply(X1,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF5))))))),X2)),
    inference(forward_demodulation,[],[f7978,f15]) ).

fof(f8053,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF7),multiply(a3,X0))),multiply(inverse(multiply(X1,b3)),X2)) = multiply(inverse(multiply(inverse(sF5),multiply(sF4,X0))),multiply(inverse(multiply(X1,b2)),X2)),
    inference(forward_demodulation,[],[f7988,f7987]) ).

fof(f8056,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(inverse(multiply(inverse(sF7),multiply(a3,b2))),multiply(inverse(multiply(X1,b3)),X2)),
    inference(forward_demodulation,[],[f7991,f7987]) ).

fof(f8114,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(inverse(multiply(inverse(sF5),multiply(sF4,b2))),multiply(inverse(multiply(X1,b2)),X2)),
    inference(forward_demodulation,[],[f8056,f8053]) ).

fof(f8172,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(multiply(X1,b2)),X2)),
    inference(forward_demodulation,[],[f8114,f15]) ).

fof(f8188,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(multiply(X1,b2)),X2)),
    inference(forward_demodulation,[],[f8172,f59]) ).

fof(f8198,plain,
    ! [X2,X1] : multiply(a1,multiply(inverse(multiply(X1,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF5))))))),X2)) = multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(multiply(X1,b2)),X2)),
    inference(forward_demodulation,[],[f8188,f8047]) ).

fof(f8256,plain,
    ! [X0,X1] : multiply(inverse(sF10),sF10) = multiply(inverse(multiply(X1,X0)),multiply(X1,X0)),
    inference(superposition,[],[f7594,f201]) ).

fof(f8493,plain,
    ! [X0,X1] : multiply(X0,multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X0),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X1)) = multiply(inverse(sF10),sF10),
    inference(superposition,[],[f8256,f533]) ).

fof(f8531,plain,
    ! [X0] : multiply(inverse(X0),X0) = multiply(inverse(sF10),sF10),
    inference(superposition,[],[f8256,f201]) ).

fof(f8554,plain,
    multiply(inverse(sF1),sF1) = multiply(inverse(sF10),sF10),
    inference(superposition,[],[f8256,f7]) ).

fof(f8556,plain,
    multiply(inverse(sF5),sF5) = multiply(inverse(sF10),sF10),
    inference(superposition,[],[f8256,f15]) ).

fof(f8557,plain,
    multiply(inverse(sF6),sF6) = multiply(inverse(sF10),sF10),
    inference(superposition,[],[f8256,f17]) ).

fof(f8605,plain,
    ! [X2,X3,X0,X1] : multiply(X3,multiply(inverse(multiply(X0,inverse(multiply(inverse(X3),inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(inverse(multiply(inverse(sF10),sF10)),multiply(inverse(multiply(X0,X1)),X2)),
    inference(superposition,[],[f5477,f8256]) ).

fof(f8651,plain,
    ! [X2,X0,X1] : multiply(b2,multiply(inverse(multiply(X0,inverse(multiply(sF4,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(inverse(multiply(inverse(sF10),sF10)),multiply(inverse(multiply(X0,X1)),X2)),
    inference(forward_demodulation,[],[f8605,f7308]) ).

fof(f8679,plain,
    multiply(inverse(sF5),sF5) = multiply(inverse(sF6),sF6),
    inference(forward_demodulation,[],[f8556,f8557]) ).

fof(f8681,plain,
    multiply(inverse(sF1),sF1) = multiply(inverse(sF6),sF6),
    inference(forward_demodulation,[],[f8554,f8557]) ).

fof(f8684,plain,
    ! [X0] : multiply(inverse(X0),X0) = multiply(inverse(sF6),sF6),
    inference(forward_demodulation,[],[f8531,f8557]) ).

fof(f8704,plain,
    ! [X0,X1] : multiply(X0,multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X0),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X1)) = multiply(inverse(sF6),sF6),
    inference(forward_demodulation,[],[f8493,f8557]) ).

fof(f8721,plain,
    ! [X2,X0,X1] : multiply(b2,multiply(inverse(multiply(X0,inverse(multiply(sF4,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(inverse(multiply(inverse(sF6),sF6)),multiply(inverse(multiply(X0,X1)),X2)),
    inference(forward_demodulation,[],[f8651,f8557]) ).

fof(f8743,plain,
    multiply(inverse(sF5),sF5) = multiply(inverse(sF1),sF1),
    inference(forward_demodulation,[],[f8681,f8679]) ).

fof(f8746,plain,
    ! [X0] : multiply(inverse(X0),X0) = multiply(inverse(sF5),sF5),
    inference(forward_demodulation,[],[f8684,f8679]) ).

fof(f8765,plain,
    ! [X0,X1] : multiply(inverse(sF5),sF5) = multiply(X0,multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X0),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X1)),
    inference(forward_demodulation,[],[f8704,f8679]) ).

fof(f8781,plain,
    ! [X2,X0,X1] : multiply(b2,multiply(inverse(multiply(X0,inverse(multiply(sF4,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(multiply(X0,X1)),X2)),
    inference(forward_demodulation,[],[f8721,f8679]) ).

fof(f8809,plain,
    ! [X1] : multiply(inverse(sF5),sF5) = multiply(b2,multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(sF4,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X1)),
    inference(forward_demodulation,[],[f8765,f7308]) ).

fof(f8822,plain,
    ! [X2,X0,X1] : multiply(b1,multiply(inverse(multiply(X0,inverse(multiply(sF2,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(multiply(X0,X1)),X2)),
    inference(forward_demodulation,[],[f8781,f7695]) ).

fof(f8836,plain,
    ! [X1] : multiply(inverse(sF5),sF5) = multiply(b1,multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(sF2,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X1)),
    inference(forward_demodulation,[],[f8809,f7695]) ).

fof(f8846,plain,
    ! [X2,X0,X1] : multiply(a1,multiply(inverse(multiply(X0,inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),X2)) = multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(multiply(X0,X1)),X2)),
    inference(forward_demodulation,[],[f8822,f7821]) ).

fof(f8857,plain,
    ! [X1] : multiply(inverse(sF5),sF5) = multiply(a1,multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X1)),
    inference(forward_demodulation,[],[f8836,f7821]) ).

fof(f8866,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF10),multiply(a3,X1))),multiply(inverse(multiply(X0,sF9)),X2)) = multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(multiply(X0,X1)),X2)),
    inference(forward_demodulation,[],[f8846,f7914]) ).

fof(f8875,plain,
    ! [X1] : multiply(inverse(sF5),sF5) = multiply(inverse(multiply(inverse(sF10),multiply(a3,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF1))))))),sF9)),X1)),
    inference(forward_demodulation,[],[f8857,f7914]) ).

fof(f8880,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(multiply(X0,X1)),X2)) = multiply(inverse(multiply(inverse(sF7),multiply(a3,X1))),multiply(inverse(multiply(X0,b3)),X2)),
    inference(forward_demodulation,[],[f8866,f7987]) ).

fof(f8888,plain,
    ! [X1] : multiply(inverse(sF5),sF5) = multiply(inverse(multiply(inverse(sF7),multiply(a3,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF1))))))),b3)),X1)),
    inference(forward_demodulation,[],[f8875,f7987]) ).

fof(f8892,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),multiply(sF4,X1))),multiply(inverse(multiply(X0,b2)),X2)) = multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(multiply(X0,X1)),X2)),
    inference(forward_demodulation,[],[f8880,f8053]) ).

fof(f8898,plain,
    ! [X1] : multiply(inverse(sF5),sF5) = multiply(inverse(multiply(inverse(sF5),multiply(sF4,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF1))))))),b2)),X1)),
    inference(forward_demodulation,[],[f8888,f8053]) ).

fof(f8902,plain,
    ! [X1] : multiply(inverse(sF5),sF5) = multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(a1,inverse(sF1))))))),sF1)),X1)),
    inference(forward_demodulation,[],[f8898,f8892]) ).

fof(f8906,plain,
    ! [X1] : multiply(inverse(sF5),sF5) = multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(X1),X1)),
    inference(forward_demodulation,[],[f8902,f59]) ).

fof(f8942,plain,
    multiply(sF0,a1) = multiply(inverse(sF5),sF5),
    inference(superposition,[],[f8746,f5]) ).

fof(f8943,plain,
    multiply(sF2,b1) = multiply(inverse(sF5),sF5),
    inference(superposition,[],[f8746,f9]) ).

fof(f8944,plain,
    multiply(sF4,b2) = multiply(inverse(sF5),sF5),
    inference(superposition,[],[f8746,f13]) ).

fof(f8960,plain,
    ! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
    inference(superposition,[],[f8746,f8746]) ).

fof(f9083,plain,
    ! [X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(multiply(X0,inverse(multiply(inverse(X0),X0))))),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X1,inverse(multiply(inverse(sF5),sF5)))),multiply(X1,X0)),
    inference(superposition,[],[f74,f8746]) ).

fof(f9229,plain,
    ! [X0,X1] : multiply(X0,inverse(multiply(inverse(X0),X0))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(sF5),sF5)))),multiply(X1,X0)),
    inference(forward_demodulation,[],[f9083,f201]) ).

fof(f9294,plain,
    sF5 = multiply(inverse(sF5),sF5),
    inference(forward_demodulation,[],[f8944,f15]) ).

fof(f9295,plain,
    sF3 = multiply(inverse(sF5),sF5),
    inference(forward_demodulation,[],[f8943,f11]) ).

fof(f9296,plain,
    sF1 = multiply(inverse(sF5),sF5),
    inference(forward_demodulation,[],[f8942,f7]) ).

fof(f9367,plain,
    sF3 = sF5,
    inference(forward_demodulation,[],[f9295,f9294]) ).

fof(f9368,plain,
    sF1 = sF5,
    inference(forward_demodulation,[],[f9296,f9294]) ).

fof(f9623,plain,
    ! [X0] : multiply(sF4,b2) = multiply(inverse(X0),X0),
    inference(superposition,[],[f8960,f13]) ).

fof(f9817,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X0),X0)))))))),multiply(X1,X3))) = X2,
    inference(superposition,[],[f1,f8960]) ).

fof(f9827,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))))),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X2),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))),
    inference(superposition,[],[f1808,f8960]) ).

fof(f9869,plain,
    ! [X2,X0] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))) = X2,
    inference(superposition,[],[f4477,f8960]) ).

fof(f9913,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))))),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X2),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))) = inverse(multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(X0),X0))),
    inference(superposition,[],[f1808,f8960]) ).

fof(f9941,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(multiply(X1,inverse(multiply(inverse(X1),X1))))),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X0)))),multiply(X2,X1)),
    inference(superposition,[],[f74,f8960]) ).

fof(f10030,plain,
    ! [X2,X0,X1] : multiply(X1,inverse(multiply(inverse(X1),X1))) = multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X0)))),multiply(X2,X1)),
    inference(forward_demodulation,[],[f9941,f201]) ).

fof(f10039,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(X0),X0))) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))))),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X2),inverse(multiply(sF1,inverse(multiply(inverse(sF5),sF5))))))),
    inference(forward_demodulation,[],[f9913,f8743]) ).

fof(f10098,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))))),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X2),inverse(multiply(sF1,inverse(multiply(inverse(sF5),sF5))))))),
    inference(forward_demodulation,[],[f9827,f8743]) ).

fof(f10228,plain,
    ! [X0] : sF5 = multiply(inverse(X0),X0),
    inference(forward_demodulation,[],[f9623,f15]) ).

fof(f10338,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(X0),X0))) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))))),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X2),inverse(multiply(sF1,inverse(sF5)))))),
    inference(forward_demodulation,[],[f10039,f9294]) ).

fof(f10368,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))))),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X2),inverse(multiply(sF1,inverse(sF5)))))),
    inference(forward_demodulation,[],[f10098,f9294]) ).

fof(f10526,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(X0),X0))) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))))),inverse(multiply(a1,inverse(sF5))))))),inverse(multiply(inverse(X2),inverse(multiply(sF5,inverse(sF5)))))),
    inference(forward_demodulation,[],[f10338,f9368]) ).

fof(f10546,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))))),inverse(multiply(a1,inverse(sF5))))))),inverse(multiply(inverse(X2),inverse(multiply(sF5,inverse(sF5)))))),
    inference(forward_demodulation,[],[f10368,f9368]) ).

fof(f10652,plain,
    ! [X2,X1] : inverse(multiply(inverse(multiply(inverse(X1),X2)),sF5)) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(sF5))))),inverse(multiply(a1,inverse(sF5))))))),inverse(multiply(inverse(X2),inverse(multiply(sF5,inverse(sF5)))))),
    inference(forward_demodulation,[],[f10526,f10228]) ).

fof(f10664,plain,
    ! [X2,X3,X1] : inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))) = multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(sF5))))),inverse(multiply(a1,inverse(sF5))))))),inverse(multiply(inverse(X2),inverse(multiply(sF5,inverse(sF5)))))),
    inference(forward_demodulation,[],[f10546,f10228]) ).

fof(f10738,plain,
    ! [X2,X3,X1] : inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))) = inverse(multiply(inverse(multiply(inverse(X1),X2)),sF5)),
    inference(forward_demodulation,[],[f10664,f10652]) ).

fof(f11081,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(inverse(X2),X1)),sF5),
    inference(superposition,[],[f5192,f10228]) ).

fof(f11082,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(sF5),multiply(inverse(X1),X2)),
    inference(superposition,[],[f5192,f10228]) ).

fof(f11095,plain,
    ! [X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(multiply(X0,inverse(multiply(inverse(X0),X0))))),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X1,inverse(sF5))),multiply(X1,X0)),
    inference(superposition,[],[f74,f10228]) ).

fof(f11185,plain,
    ! [X0,X1] : multiply(X0,inverse(multiply(inverse(X0),X0))) = multiply(inverse(multiply(X1,inverse(sF5))),multiply(X1,X0)),
    inference(forward_demodulation,[],[f11095,f201]) ).

fof(f11191,plain,
    ! [X2,X1] : multiply(inverse(multiply(inverse(X2),X1)),sF5) = multiply(inverse(sF5),multiply(inverse(X1),X2)),
    inference(forward_demodulation,[],[f11081,f11082]) ).

fof(f11341,plain,
    ! [X0] : multiply(X0,inverse(multiply(inverse(X0),X0))) = multiply(inverse(sF5),multiply(inverse(inverse(sF5)),X0)),
    inference(forward_demodulation,[],[f11185,f11082]) ).

fof(f11446,plain,
    ! [X0] : multiply(X0,inverse(sF5)) = multiply(inverse(sF5),multiply(inverse(inverse(sF5)),X0)),
    inference(forward_demodulation,[],[f11341,f10228]) ).

fof(f11789,plain,
    ! [X2,X3,X0,X1,X4,X5] : multiply(multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3)))) = multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),X5)))),multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,X3))),
    inference(superposition,[],[f10030,f5477]) ).

fof(f12212,plain,
    ! [X2,X3,X1,X4,X5] : multiply(multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3)))) = multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),X5)))),multiply(inverse(sF5),multiply(inverse(multiply(X1,X2)),X3))),
    inference(forward_demodulation,[],[f11789,f11082]) ).

fof(f12509,plain,
    ! [X2,X3,X1,X4] : multiply(multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3)))) = multiply(inverse(multiply(X4,inverse(sF5))),multiply(inverse(sF5),multiply(inverse(multiply(X1,X2)),X3))),
    inference(forward_demodulation,[],[f12212,f10228]) ).

fof(f12790,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(X4,inverse(sF5))),multiply(inverse(sF5),multiply(inverse(multiply(X1,X2)),X3))) = multiply(multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3),inverse(multiply(inverse(multiply(inverse(X3),X3)),sF5))),
    inference(forward_demodulation,[],[f12509,f10738]) ).

fof(f13043,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(X4,inverse(sF5))),multiply(inverse(sF5),multiply(inverse(multiply(X1,X2)),X3))) = multiply(multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3),inverse(multiply(inverse(sF5),multiply(inverse(X3),X3)))),
    inference(forward_demodulation,[],[f12790,f11191]) ).

fof(f13270,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(X4,inverse(sF5))),multiply(inverse(sF5),multiply(inverse(multiply(X1,X2)),X3))) = multiply(multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3),inverse(multiply(inverse(sF5),sF5))),
    inference(forward_demodulation,[],[f13043,f10228]) ).

fof(f13462,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(X4,inverse(sF5))),multiply(inverse(sF5),multiply(inverse(multiply(X1,X2)),X3))) = multiply(multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3),inverse(sF5)),
    inference(forward_demodulation,[],[f13270,f9294]) ).

fof(f13605,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(X4,inverse(sF5))),multiply(inverse(sF5),multiply(inverse(multiply(X1,X2)),X3))) = multiply(multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(sF5))))))),X3),inverse(sF5)),
    inference(forward_demodulation,[],[f13462,f10228]) ).

fof(f27575,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)),inverse(multiply(X0,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)))))))),
    inference(superposition,[],[f9869,f53]) ).

fof(f27646,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X1)))),multiply(X0,X2))))) = X2,
    inference(superposition,[],[f9869,f10030]) ).

fof(f27670,plain,
    ! [X0,X1] : multiply(inverse(X0),X0) = inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(inverse(multiply(inverse(X0),X0)))))),
    inference(superposition,[],[f9817,f9869]) ).

fof(f27722,plain,
    ! [X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X0,inverse(multiply(inverse(X0),X0))))),
    inference(superposition,[],[f201,f9869]) ).

fof(f27769,plain,
    ! [X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X0,inverse(sF5)))),
    inference(forward_demodulation,[],[f27722,f10228]) ).

fof(f27810,plain,
    ! [X1] : sF5 = inverse(multiply(inverse(sF5),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(inverse(sF5))))),
    inference(forward_demodulation,[],[f27670,f10228]) ).

fof(f27833,plain,
    ! [X2,X3,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(X1),X1)))),sF5)))) = X2,
    inference(forward_demodulation,[],[f27646,f10738]) ).

fof(f27904,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)),inverse(multiply(a1,multiply(inverse(multiply(X2,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)))))))),
    inference(forward_demodulation,[],[f27575,f8047]) ).

fof(f28001,plain,
    ! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(inverse(sF5)),inverse(multiply(X0,inverse(sF5)))),
    inference(forward_demodulation,[],[f27769,f10228]) ).

fof(f28042,plain,
    sF5 = inverse(multiply(inverse(sF5),multiply(inverse(inverse(sF5)),inverse(inverse(sF5))))),
    inference(forward_demodulation,[],[f27810,f10228]) ).

fof(f28060,plain,
    ! [X2,X3,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(sF5),multiply(inverse(inverse(multiply(inverse(X1),X1))),X2))))) = X2,
    inference(forward_demodulation,[],[f27833,f11191]) ).

fof(f28129,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)),inverse(multiply(inverse(multiply(inverse(sF5),sF5)),multiply(inverse(multiply(X2,b2)),multiply(X2,b2)))))))),
    inference(forward_demodulation,[],[f27904,f8198]) ).

fof(f28223,plain,
    ! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(a1,inverse(sF5))))))),sF5) = multiply(inverse(inverse(sF5)),inverse(multiply(X0,inverse(sF5)))),
    inference(forward_demodulation,[],[f28001,f9368]) ).

fof(f28258,plain,
    sF5 = inverse(multiply(inverse(inverse(sF5)),inverse(sF5))),
    inference(forward_demodulation,[],[f28042,f11446]) ).

fof(f28272,plain,
    ! [X2,X3] : inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(sF5),multiply(inverse(inverse(sF5)),X2))))) = X2,
    inference(forward_demodulation,[],[f28060,f10228]) ).

fof(f28333,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)),inverse(multiply(inverse(sF5),sF5)))))),
    inference(forward_demodulation,[],[f28129,f8906]) ).

fof(f28449,plain,
    sF5 = inverse(sF5),
    inference(forward_demodulation,[],[f28258,f10228]) ).

fof(f28460,plain,
    ! [X2,X3] : inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(X2,inverse(sF5))))) = X2,
    inference(forward_demodulation,[],[f28272,f11446]) ).

fof(f28511,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)),inverse(sF5))))),
    inference(forward_demodulation,[],[f28333,f9294]) ).

fof(f28611,plain,
    ! [X2,X3] : inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(X2,sF5)))) = X2,
    inference(forward_demodulation,[],[f28460,f28449]) ).

fof(f28649,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(X0,inverse(sF5))),multiply(inverse(sF5),multiply(inverse(multiply(X2,b2)),multiply(X2,b2))))))),
    inference(forward_demodulation,[],[f28511,f13605]) ).

fof(f28737,plain,
    ! [X2] : inverse(multiply(inverse(inverse(sF5)),inverse(multiply(X2,sF5)))) = X2,
    inference(forward_demodulation,[],[f28611,f10228]) ).

fof(f28775,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(X0,inverse(sF5))),multiply(inverse(sF5),multiply(inverse(sF5),multiply(sF4,b2))))))),
    inference(forward_demodulation,[],[f28649,f5466]) ).

fof(f28846,plain,
    ! [X2] : inverse(multiply(inverse(sF5),inverse(multiply(X2,sF5)))) = X2,
    inference(forward_demodulation,[],[f28737,f28449]) ).

fof(f28884,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(X0,inverse(sF5))),multiply(inverse(sF5),multiply(inverse(sF5),sF5)))))),
    inference(forward_demodulation,[],[f28775,f15]) ).

fof(f28943,plain,
    ! [X2] : inverse(multiply(sF5,inverse(multiply(X2,sF5)))) = X2,
    inference(forward_demodulation,[],[f28846,f28449]) ).

fof(f28981,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(X0,inverse(sF5))),multiply(inverse(sF5),sF5))))),
    inference(forward_demodulation,[],[f28884,f9294]) ).

fof(f29058,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF5))))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(X0,inverse(sF5))),sF5)))),
    inference(forward_demodulation,[],[f28981,f9294]) ).

fof(f29133,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,sF5)))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(X0,sF5)),sF5)))),
    inference(forward_demodulation,[],[f29058,f28449]) ).

fof(f29189,plain,
    ! [X2,X0] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,sF5)))))),multiply(X2,b2)) = inverse(multiply(inverse(inverse(sF5)),inverse(multiply(inverse(multiply(X0,sF5)),sF5)))),
    inference(forward_demodulation,[],[f29133,f10228]) ).

fof(f29242,plain,
    ! [X2,X0] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,sF5)))))),multiply(X2,b2)) = inverse(multiply(inverse(sF5),inverse(multiply(inverse(multiply(X0,sF5)),sF5)))),
    inference(forward_demodulation,[],[f29189,f28449]) ).

fof(f29283,plain,
    ! [X2,X0] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,sF5)))))),multiply(X2,b2)) = inverse(multiply(sF5,inverse(multiply(inverse(multiply(X0,sF5)),sF5)))),
    inference(forward_demodulation,[],[f29242,f28449]) ).

fof(f29317,plain,
    ! [X2,X0] : inverse(multiply(X0,sF5)) = multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(b2,sF5)))))),multiply(X2,b2)),
    inference(forward_demodulation,[],[f29283,f28943]) ).

fof(f29338,plain,
    ! [X0] : inverse(multiply(X0,sF5)) = multiply(inverse(multiply(sF4,inverse(multiply(inverse(X0),inverse(multiply(b2,sF5)))))),sF5),
    inference(forward_demodulation,[],[f29317,f1967]) ).

fof(f29392,plain,
    ! [X0] : inverse(multiply(inverse(multiply(sF4,inverse(multiply(inverse(X0),inverse(multiply(b2,sF5)))))),sF5)) = X0,
    inference(superposition,[],[f46,f28449]) ).

fof(f29441,plain,
    ! [X0] : inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(sF5),inverse(multiply(a1,inverse(sF1))))))),inverse(multiply(inverse(X0),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),sF5)) = X0,
    inference(superposition,[],[f533,f28449]) ).

fof(f29448,plain,
    ! [X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,sF5)))),inverse(multiply(sF5,inverse(multiply(sF5,sF5)))))) = X1,
    inference(superposition,[],[f4477,f28449]) ).

fof(f29476,plain,
    ! [X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,sF5)))),sF5)) = X1,
    inference(forward_demodulation,[],[f29448,f28943]) ).

fof(f29483,plain,
    ! [X0] : inverse(multiply(inverse(sF5),multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))),multiply(sF0,inverse(multiply(inverse(sF5),inverse(multiply(a1,inverse(sF1))))))))) = X0,
    inference(forward_demodulation,[],[f29441,f11191]) ).

fof(f29522,plain,
    ! [X0] : inverse(inverse(multiply(X0,sF5))) = X0,
    inference(forward_demodulation,[],[f29392,f29338]) ).

fof(f29534,plain,
    ! [X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(sF5),X1)),sF5))),sF5)) = X1,
    inference(forward_demodulation,[],[f29476,f10738]) ).

fof(f29541,plain,
    ! [X0] : inverse(multiply(inverse(sF5),multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(sF5,inverse(multiply(inverse(sF5),sF5))))))),multiply(sF0,inverse(multiply(inverse(sF5),inverse(multiply(a1,inverse(sF5))))))))) = X0,
    inference(forward_demodulation,[],[f29483,f9368]) ).

fof(f29587,plain,
    ! [X1] : inverse(multiply(inverse(multiply(inverse(sF5),X1)),sF5)) = X1,
    inference(forward_demodulation,[],[f29534,f29522]) ).

fof(f29592,plain,
    ! [X0] : inverse(multiply(sF5,multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(sF5,inverse(multiply(sF5,sF5))))))),multiply(sF0,inverse(multiply(sF5,inverse(multiply(a1,sF5)))))))) = X0,
    inference(forward_demodulation,[],[f29541,f28449]) ).

fof(f29634,plain,
    ! [X1] : inverse(multiply(inverse(sF5),multiply(inverse(X1),sF5))) = X1,
    inference(forward_demodulation,[],[f29587,f11191]) ).

fof(f29639,plain,
    ! [X0] : inverse(multiply(sF5,multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(sF5,inverse(multiply(sF5,sF5))))))),multiply(sF0,a1)))) = X0,
    inference(forward_demodulation,[],[f29592,f28943]) ).

fof(f29677,plain,
    ! [X1] : inverse(multiply(sF5,multiply(inverse(X1),sF5))) = X1,
    inference(forward_demodulation,[],[f29634,f28449]) ).

fof(f29680,plain,
    ! [X0] : inverse(multiply(sF5,multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(sF5,inverse(multiply(sF5,sF5))))))),sF1))) = X0,
    inference(forward_demodulation,[],[f29639,f7]) ).

fof(f29716,plain,
    ! [X0] : inverse(multiply(sF5,multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(sF5,inverse(multiply(sF5,sF5))))))),sF5))) = X0,
    inference(forward_demodulation,[],[f29680,f9368]) ).

fof(f29731,plain,
    ! [X0] : inverse(multiply(inverse(X0),inverse(multiply(sF5,inverse(multiply(sF5,sF5)))))) = X0,
    inference(forward_demodulation,[],[f29716,f29677]) ).

fof(f29742,plain,
    ! [X0] : inverse(multiply(inverse(X0),sF5)) = X0,
    inference(forward_demodulation,[],[f29731,f28943]) ).

fof(f29827,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,sF5)))))),inverse(multiply(inverse(multiply(X0,sF5)),inverse(multiply(X0,inverse(multiply(X0,sF5)))))))) = X2,
    inference(superposition,[],[f4477,f29522]) ).

fof(f29843,plain,
    ! [X0] : sF5 = multiply(X0,inverse(multiply(X0,sF5))),
    inference(superposition,[],[f10228,f29522]) ).

fof(f29859,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,sF5)))))),inverse(multiply(inverse(multiply(X0,sF5)),inverse(sF5))))) = X2,
    inference(forward_demodulation,[],[f29827,f29843]) ).

fof(f29918,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,sF5)))))),inverse(multiply(inverse(multiply(X0,sF5)),sF5)))) = X2,
    inference(forward_demodulation,[],[f29859,f28449]) ).

fof(f29973,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,sF5)))))),multiply(X0,sF5))) = X2,
    inference(forward_demodulation,[],[f29918,f29742]) ).

fof(f30021,plain,
    ! [X2,X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(X0,sF5))),X2)),sF5))),multiply(X0,sF5))) = X2,
    inference(forward_demodulation,[],[f29973,f10738]) ).

fof(f30064,plain,
    ! [X2,X0] : inverse(multiply(inverse(multiply(inverse(inverse(multiply(X0,sF5))),X2)),multiply(X0,sF5))) = X2,
    inference(forward_demodulation,[],[f30021,f29522]) ).

fof(f30100,plain,
    ! [X2,X0] : inverse(multiply(inverse(multiply(X0,X2)),multiply(X0,sF5))) = X2,
    inference(forward_demodulation,[],[f30064,f29522]) ).

fof(f30115,plain,
    ! [X2] : inverse(multiply(inverse(multiply(inverse(sF5),X2)),sF5)) = X2,
    inference(forward_demodulation,[],[f30100,f10738]) ).

fof(f30127,plain,
    ! [X2] : multiply(inverse(sF5),X2) = X2,
    inference(forward_demodulation,[],[f30115,f29742]) ).

fof(f30139,plain,
    ! [X2] : multiply(sF5,X2) = X2,
    inference(forward_demodulation,[],[f30127,f28449]) ).

fof(f30171,plain,
    a2 = sF6,
    inference(superposition,[],[f17,f30139]) ).

fof(f30183,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(sF5,inverse(multiply(inverse(X1),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),inverse(multiply(inverse(X2),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(a1,inverse(sF1))))))),sF1))) = X2,
    inference(superposition,[],[f93,f30139]) ).

fof(f30191,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X2))) = inverse(multiply(inverse(X0),multiply(sF5,X2))),
    inference(superposition,[],[f4383,f30139]) ).

fof(f30211,plain,
    ! [X0] : multiply(X0,inverse(multiply(inverse(X0),X0))) = multiply(inverse(multiply(sF5,inverse(multiply(inverse(sF5),sF5)))),X0),
    inference(superposition,[],[f9229,f30139]) ).

fof(f30234,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(inverse(sF5),sF5))))))),inverse(multiply(inverse(X2),inverse(multiply(multiply(X0,sF5),inverse(multiply(inverse(multiply(X0,sF5)),multiply(X0,sF5))))))))),multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(a1,inverse(sF1))))))),sF1))) = X2,
    inference(superposition,[],[f93,f30139]) ).

fof(f30247,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,multiply(sF5,X1))),multiply(X2,X3)) = multiply(X0,multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(X1,inverse(multiply(inverse(X1),X1))))))),X3)),
    inference(superposition,[],[f5477,f30139]) ).

fof(f30355,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,multiply(sF5,X1))),multiply(X2,X3)) = multiply(X0,multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(X1,inverse(sF5)))))),X3)),
    inference(forward_demodulation,[],[f30247,f10228]) ).

fof(f30368,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(inverse(sF5),sF5))))))),inverse(multiply(inverse(X2),inverse(multiply(multiply(X0,sF5),inverse(multiply(inverse(multiply(X0,sF5)),multiply(X0,sF5))))))))),multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(a1,inverse(sF5))))))),sF5))) = X2,
    inference(forward_demodulation,[],[f30234,f9368]) ).

fof(f30391,plain,
    ! [X0] : multiply(X0,inverse(multiply(inverse(X0),X0))) = multiply(inverse(sF5),X0),
    inference(forward_demodulation,[],[f30211,f28943]) ).

fof(f30408,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X2))) = inverse(multiply(inverse(X0),X2)),
    inference(forward_demodulation,[],[f30191,f30139]) ).

fof(f30416,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(sF5,inverse(multiply(inverse(X1),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),inverse(multiply(inverse(X2),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(a1,inverse(sF5))))))),sF5))) = X2,
    inference(forward_demodulation,[],[f30183,f9368]) ).

fof(f30428,plain,
    spl11_2,
    inference(avatar_split_clause,[],[f30171,f32]) ).

fof(f30478,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,multiply(sF5,X1))),multiply(X2,X3)) = multiply(X0,multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(X1,sF5))))),X3)),
    inference(forward_demodulation,[],[f30355,f28449]) ).

fof(f30491,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(inverse(sF5),sF5))))))),inverse(multiply(inverse(X2),inverse(multiply(multiply(X0,sF5),inverse(multiply(inverse(multiply(X0,sF5)),multiply(X0,sF5))))))))),multiply(inverse(inverse(sF5)),inverse(multiply(X1,inverse(sF5)))))) = X2,
    inference(forward_demodulation,[],[f30368,f28223]) ).

fof(f30514,plain,
    ! [X0] : multiply(X0,inverse(multiply(inverse(X0),X0))) = multiply(sF5,X0),
    inference(forward_demodulation,[],[f30391,f28449]) ).

fof(f30526,plain,
    ! [X2,X0] : inverse(multiply(inverse(multiply(inverse(X2),X0)),sF5)) = inverse(multiply(inverse(X0),X2)),
    inference(forward_demodulation,[],[f30408,f10738]) ).

fof(f30533,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(sF5,inverse(multiply(inverse(X1),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),inverse(multiply(inverse(X2),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),multiply(inverse(inverse(sF5)),inverse(multiply(X1,inverse(sF5)))))) = X2,
    inference(forward_demodulation,[],[f30416,f28223]) ).

fof(f30587,plain,
    ! [X3,X0,X1] : multiply(X0,multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(X1,sF5))))),X3)) = multiply(inverse(sF5),multiply(inverse(multiply(sF5,X1)),X3)),
    inference(forward_demodulation,[],[f30478,f11082]) ).

fof(f30600,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(sF5,sF5))))))),inverse(multiply(inverse(X2),inverse(multiply(multiply(X0,sF5),inverse(multiply(inverse(multiply(X0,sF5)),multiply(X0,sF5))))))))),multiply(inverse(sF5),inverse(multiply(X1,sF5))))) = X2,
    inference(forward_demodulation,[],[f30491,f28449]) ).

fof(f30621,plain,
    ! [X0] : multiply(X0,inverse(multiply(inverse(X0),X0))) = X0,
    inference(forward_demodulation,[],[f30514,f30139]) ).

fof(f30632,plain,
    ! [X2,X0] : multiply(inverse(X2),X0) = inverse(multiply(inverse(X0),X2)),
    inference(forward_demodulation,[],[f30526,f29742]) ).

fof(f30636,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(sF5,inverse(multiply(inverse(X1),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),inverse(multiply(inverse(X2),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),multiply(inverse(sF5),inverse(multiply(X1,sF5))))) = X2,
    inference(forward_demodulation,[],[f30533,f28449]) ).

fof(f30679,plain,
    ! [X3,X0,X1] : multiply(inverse(sF5),multiply(inverse(X1),X3)) = multiply(X0,multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(X1,sF5))))),X3)),
    inference(forward_demodulation,[],[f30587,f30139]) ).

fof(f30691,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(sF5,sF5))))))),inverse(multiply(inverse(X2),inverse(multiply(multiply(X0,sF5),inverse(multiply(inverse(multiply(X0,sF5)),multiply(X0,sF5))))))))),multiply(sF5,inverse(multiply(X1,sF5))))) = X2,
    inference(forward_demodulation,[],[f30600,f28449]) ).

fof(f30711,plain,
    ! [X0] : multiply(X0,inverse(sF5)) = X0,
    inference(forward_demodulation,[],[f30621,f10228]) ).

fof(f30715,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),inverse(multiply(X1,sF5)))),multiply(inverse(multiply(sF5,inverse(multiply(inverse(X1),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),inverse(multiply(inverse(X2),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))) = X2,
    inference(forward_demodulation,[],[f30636,f30632]) ).

fof(f30749,plain,
    ! [X3,X0,X1] : multiply(inverse(sF5),multiply(inverse(X1),X3)) = multiply(X0,multiply(inverse(multiply(inverse(inverse(multiply(X1,sF5))),X0)),X3)),
    inference(forward_demodulation,[],[f30679,f30632]) ).

fof(f30760,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(sF5,sF5))))))),inverse(multiply(inverse(X2),inverse(multiply(multiply(X0,sF5),inverse(multiply(inverse(multiply(X0,sF5)),multiply(X0,sF5))))))))) = X2,
    inference(forward_demodulation,[],[f30691,f30632]) ).

fof(f30780,plain,
    ! [X0] : multiply(X0,sF5) = X0,
    inference(forward_demodulation,[],[f30711,f28449]) ).

fof(f30782,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),inverse(multiply(X1,sF5)))),multiply(inverse(multiply(sF5,inverse(multiply(inverse(X1),inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))))),multiply(inverse(inverse(multiply(X0,inverse(multiply(inverse(X0),X0))))),X2))) = X2,
    inference(forward_demodulation,[],[f30715,f30632]) ).

fof(f30810,plain,
    ! [X3,X0,X1] : multiply(inverse(sF5),multiply(inverse(X1),X3)) = multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,sF5))),X3)),
    inference(forward_demodulation,[],[f30749,f30632]) ).

fof(f30821,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(sF5,sF5))))))),multiply(inverse(inverse(multiply(multiply(X0,sF5),inverse(multiply(inverse(multiply(X0,sF5)),multiply(X0,sF5)))))),X2))) = X2,
    inference(forward_demodulation,[],[f30760,f30632]) ).

fof(f30837,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),inverse(multiply(X1,sF5)))),multiply(inverse(multiply(sF5,inverse(multiply(inverse(X1),inverse(multiply(X0,multiply(inverse(X0),X0))))))),multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),X2))) = X2,
    inference(forward_demodulation,[],[f30782,f30632]) ).

fof(f30861,plain,
    ! [X3,X0,X1] : multiply(inverse(sF5),multiply(inverse(X1),X3)) = multiply(X0,multiply(multiply(inverse(X0),inverse(X1)),X3)),
    inference(forward_demodulation,[],[f30810,f30780]) ).

fof(f30868,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(sF5,sF5))))))),multiply(inverse(inverse(multiply(multiply(X0,sF5),inverse(multiply(inverse(multiply(inverse(sF5),sF5)),sF5))))),X2))) = X2,
    inference(forward_demodulation,[],[f30821,f10738]) ).

fof(f30884,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),inverse(multiply(X1,sF5)))),multiply(inverse(multiply(sF5,inverse(multiply(inverse(X1),inverse(multiply(X0,sF5)))))),multiply(inverse(inverse(multiply(X0,sF5))),X2))) = X2,
    inference(forward_demodulation,[],[f30837,f10228]) ).

fof(f30906,plain,
    ! [X3,X0,X1] : multiply(X0,multiply(multiply(inverse(X0),inverse(X1)),X3)) = multiply(sF5,multiply(inverse(X1),X3)),
    inference(forward_demodulation,[],[f30861,f28449]) ).

fof(f30913,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(sF5,sF5))))))),multiply(inverse(inverse(multiply(multiply(X0,sF5),multiply(inverse(sF5),sF5)))),X2))) = X2,
    inference(forward_demodulation,[],[f30868,f29742]) ).

fof(f30928,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),inverse(multiply(X1,sF5)))),multiply(inverse(multiply(sF5,inverse(multiply(inverse(X1),inverse(multiply(X0,sF5)))))),multiply(X0,X2))) = X2,
    inference(forward_demodulation,[],[f30884,f29522]) ).

fof(f30946,plain,
    ! [X3,X0,X1] : multiply(inverse(X1),X3) = multiply(X0,multiply(multiply(inverse(X0),inverse(X1)),X3)),
    inference(forward_demodulation,[],[f30906,f30139]) ).

fof(f30953,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(sF5,sF5))))))),multiply(inverse(inverse(multiply(multiply(X0,sF5),sF5))),X2))) = X2,
    inference(forward_demodulation,[],[f30913,f9294]) ).

fof(f30967,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),inverse(multiply(X1,sF5)))),multiply(inverse(inverse(multiply(inverse(X1),inverse(multiply(X0,sF5))))),multiply(X0,X2))) = X2,
    inference(forward_demodulation,[],[f30928,f30139]) ).

fof(f30987,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(sF5,sF5))))))),multiply(multiply(X0,sF5),X2))) = X2,
    inference(forward_demodulation,[],[f30953,f29522]) ).

fof(f31000,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),inverse(multiply(X1,sF5)))),multiply(inverse(multiply(inverse(inverse(multiply(X0,sF5))),X1)),multiply(X0,X2))) = X2,
    inference(forward_demodulation,[],[f30967,f30632]) ).

fof(f31015,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(sF5,sF5))))))),multiply(X0,X2))) = X2,
    inference(forward_demodulation,[],[f30987,f30780]) ).

fof(f31023,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),inverse(multiply(X1,sF5)))),multiply(multiply(inverse(X1),inverse(multiply(X0,sF5))),multiply(X0,X2))) = X2,
    inference(forward_demodulation,[],[f31000,f30632]) ).

fof(f31036,plain,
    ! [X2,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(sF5),multiply(inverse(inverse(multiply(inverse(X1),inverse(inverse(multiply(sF5,sF5)))))),X2))) = X2,
    inference(forward_demodulation,[],[f31015,f11082]) ).

fof(f31040,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF5),inverse(multiply(X1,sF5)))),multiply(multiply(inverse(X1),inverse(X0)),multiply(X0,X2))) = X2,
    inference(forward_demodulation,[],[f31023,f30780]) ).

fof(f31048,plain,
    ! [X2,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(sF5),multiply(inverse(multiply(inverse(inverse(inverse(multiply(sF5,sF5)))),X1)),X2))) = X2,
    inference(forward_demodulation,[],[f31036,f30632]) ).

fof(f31049,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(inverse(multiply(X1,sF5))),sF5),multiply(multiply(inverse(X1),inverse(X0)),multiply(X0,X2))) = X2,
    inference(forward_demodulation,[],[f31040,f30632]) ).

fof(f31052,plain,
    ! [X2,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(sF5),multiply(multiply(inverse(X1),inverse(inverse(multiply(sF5,sF5)))),X2))) = X2,
    inference(forward_demodulation,[],[f31048,f30632]) ).

fof(f31053,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(multiply(X1,sF5))),multiply(multiply(inverse(X1),inverse(X0)),multiply(X0,X2))) = X2,
    inference(forward_demodulation,[],[f31049,f30780]) ).

fof(f31055,plain,
    ! [X2,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(sF5),multiply(multiply(inverse(X1),sF5),X2))) = X2,
    inference(forward_demodulation,[],[f31052,f29522]) ).

fof(f31056,plain,
    ! [X2,X0,X1] : multiply(X1,multiply(multiply(inverse(X1),inverse(X0)),multiply(X0,X2))) = X2,
    inference(forward_demodulation,[],[f31053,f29522]) ).

fof(f31058,plain,
    ! [X2,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(inverse(sF5),multiply(inverse(X1),X2))) = X2,
    inference(forward_demodulation,[],[f31055,f30780]) ).

fof(f31059,plain,
    ! [X2,X0] : multiply(inverse(X0),multiply(X0,X2)) = X2,
    inference(forward_demodulation,[],[f31056,f30946]) ).

fof(f31061,plain,
    ! [X2,X1] : multiply(inverse(multiply(sF5,inverse(multiply(X1,sF5)))),multiply(sF5,multiply(inverse(X1),X2))) = X2,
    inference(forward_demodulation,[],[f31058,f28449]) ).

fof(f31062,plain,
    ! [X2,X1] : multiply(inverse(sF5),multiply(inverse(inverse(multiply(X1,sF5))),multiply(inverse(X1),X2))) = X2,
    inference(forward_demodulation,[],[f31061,f11082]) ).

fof(f31063,plain,
    ! [X2,X1] : multiply(inverse(sF5),multiply(X1,multiply(inverse(X1),X2))) = X2,
    inference(forward_demodulation,[],[f31062,f29522]) ).

fof(f31064,plain,
    ! [X2,X1] : multiply(sF5,multiply(X1,multiply(inverse(X1),X2))) = X2,
    inference(forward_demodulation,[],[f31063,f28449]) ).

fof(f31065,plain,
    ! [X2,X1] : multiply(X1,multiply(inverse(X1),X2)) = X2,
    inference(forward_demodulation,[],[f31064,f30139]) ).

fof(f31107,plain,
    ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3) = multiply(inverse(X4),multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,X3))),
    inference(superposition,[],[f31059,f5477]) ).

fof(f31117,plain,
    ! [X0,X1] : multiply(X1,X0) = multiply(inverse(inverse(X1)),X0),
    inference(superposition,[],[f31059,f31059]) ).

fof(f31120,plain,
    ! [X2,X0,X1] : multiply(X2,X1) = multiply(inverse(inverse(multiply(X2,X0))),multiply(inverse(sF5),multiply(inverse(X0),X1))),
    inference(superposition,[],[f31059,f11082]) ).

fof(f31199,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X0))))))))),X0),
    inference(superposition,[],[f72,f31059]) ).

fof(f31237,plain,
    ! [X2,X0,X1] : multiply(inverse(sF5),multiply(inverse(X2),multiply(X1,X0))) = multiply(inverse(multiply(inverse(X1),X2)),X0),
    inference(superposition,[],[f11082,f31059]) ).

fof(f31238,plain,
    ! [X2,X0,X1] : multiply(inverse(sF5),multiply(inverse(multiply(X1,X0)),X2)) = multiply(inverse(X0),multiply(inverse(X1),X2)),
    inference(superposition,[],[f11082,f31059]) ).

fof(f31239,plain,
    ! [X2,X0,X1] : multiply(inverse(X0),multiply(inverse(X1),X2)) = multiply(sF5,multiply(inverse(multiply(X1,X0)),X2)),
    inference(forward_demodulation,[],[f31238,f28449]) ).

fof(f31240,plain,
    ! [X2,X0,X1] : multiply(inverse(sF5),multiply(inverse(X2),multiply(X1,X0))) = multiply(multiply(inverse(X2),X1),X0),
    inference(forward_demodulation,[],[f31237,f30632]) ).

fof(f31276,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(multiply(inverse(inverse(multiply(inverse(X2),inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))))),X1),X0),
    inference(forward_demodulation,[],[f31199,f30632]) ).

fof(f31350,plain,
    ! [X2,X0,X1] : multiply(X2,X1) = multiply(inverse(inverse(multiply(X2,X0))),multiply(sF5,multiply(inverse(X0),X1))),
    inference(forward_demodulation,[],[f31120,f28449]) ).

fof(f31362,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3) = multiply(inverse(X4),multiply(inverse(sF5),multiply(inverse(multiply(X1,X2)),X3))),
    inference(forward_demodulation,[],[f31107,f11082]) ).

fof(f31401,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X1,X0)),X2) = multiply(inverse(X0),multiply(inverse(X1),X2)),
    inference(forward_demodulation,[],[f31239,f30139]) ).

fof(f31402,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(X2),X1),X0) = multiply(sF5,multiply(inverse(X2),multiply(X1,X0))),
    inference(forward_demodulation,[],[f31240,f28449]) ).

fof(f31434,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(multiply(multiply(inverse(X2),inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))),X1),X0),
    inference(forward_demodulation,[],[f31276,f31117]) ).

fof(f31504,plain,
    ! [X2,X0,X1] : multiply(X2,X1) = multiply(multiply(X2,X0),multiply(sF5,multiply(inverse(X0),X1))),
    inference(forward_demodulation,[],[f31350,f31117]) ).

fof(f31515,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3) = multiply(inverse(X4),multiply(sF5,multiply(inverse(multiply(X1,X2)),X3))),
    inference(forward_demodulation,[],[f31362,f28449]) ).

fof(f31549,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(X1,X0)) = multiply(multiply(inverse(X2),X1),X0),
    inference(forward_demodulation,[],[f31402,f30139]) ).

fof(f31579,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(multiply(multiply(inverse(X2),inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(inverse(X0),X0)),sF5))))),X1),X0),
    inference(forward_demodulation,[],[f31434,f10738]) ).

fof(f31629,plain,
    ! [X2,X0,X1] : multiply(X2,X1) = multiply(multiply(X2,X0),multiply(inverse(X0),X1)),
    inference(forward_demodulation,[],[f31504,f30139]) ).

fof(f31637,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3) = multiply(inverse(X4),multiply(inverse(multiply(X1,X2)),X3)),
    inference(forward_demodulation,[],[f31515,f30139]) ).

fof(f31690,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(multiply(inverse(X2),multiply(inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(inverse(X0),X0)),sF5)))),X1)),X0),
    inference(forward_demodulation,[],[f31579,f31549]) ).

fof(f31740,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(inverse(X4),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3) = multiply(inverse(multiply(multiply(X1,X2),X4)),X3),
    inference(forward_demodulation,[],[f31637,f31401]) ).

fof(f31789,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(X2),multiply(multiply(inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(inverse(X0),X0)),sF5)))),X1),X0)),
    inference(forward_demodulation,[],[f31690,f31549]) ).

fof(f31827,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(multiply(X1,X2),X4)),X3) = multiply(inverse(multiply(X1,multiply(inverse(inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))),X4))),X3),
    inference(forward_demodulation,[],[f31740,f30632]) ).

fof(f31872,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(X2),multiply(inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(inverse(X0),X0)),sF5)))),multiply(X1,X0))),
    inference(forward_demodulation,[],[f31789,f31549]) ).

fof(f31906,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(multiply(X1,X2),X4)),X3) = multiply(inverse(multiply(X1,multiply(multiply(X2,inverse(multiply(inverse(X2),X2))),X4))),X3),
    inference(forward_demodulation,[],[f31827,f31117]) ).

fof(f31948,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(inverse(X0),X0)),sF5))),X2)),multiply(X1,X0)),
    inference(forward_demodulation,[],[f31872,f31401]) ).

fof(f31982,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(multiply(X1,X2),X4)),X3) = multiply(inverse(multiply(X1,multiply(multiply(X2,multiply(inverse(X2),X2)),X4))),X3),
    inference(forward_demodulation,[],[f31906,f30632]) ).

fof(f32019,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(multiply(multiply(X1,X0),multiply(inverse(X0),X0)),X2)),multiply(X1,X0)),
    inference(forward_demodulation,[],[f31948,f29742]) ).

fof(f32051,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(multiply(multiply(X1,X2),X4)),X3) = multiply(inverse(multiply(X1,multiply(X2,X4))),X3),
    inference(forward_demodulation,[],[f31982,f31065]) ).

fof(f32087,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(multiply(X1,X0),X2)),multiply(X1,X0)),
    inference(forward_demodulation,[],[f32019,f31629]) ).

fof(f32136,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X1,multiply(X0,X2))),multiply(X1,X0)),
    inference(forward_demodulation,[],[f32087,f32051]) ).

fof(f32177,plain,
    ! [X2,X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(sF5),multiply(inverse(multiply(X0,X2)),X0)),
    inference(forward_demodulation,[],[f32136,f11082]) ).

fof(f32209,plain,
    ! [X2,X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(multiply(X0,X2),sF5)),X0),
    inference(forward_demodulation,[],[f32177,f31401]) ).

fof(f32231,plain,
    ! [X2,X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X0,multiply(X2,sF5))),X0),
    inference(forward_demodulation,[],[f32209,f32051]) ).

fof(f32248,plain,
    ! [X2,X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X0,X2)),X0),
    inference(forward_demodulation,[],[f32231,f30780]) ).

fof(f32256,plain,
    ! [X2,X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(a1,inverse(sF5))))))),sF5) = multiply(inverse(multiply(X0,X2)),X0),
    inference(forward_demodulation,[],[f32248,f9368]) ).

fof(f32263,plain,
    ! [X2,X0] : multiply(inverse(inverse(sF5)),inverse(multiply(X2,inverse(sF5)))) = multiply(inverse(multiply(X0,X2)),X0),
    inference(forward_demodulation,[],[f32256,f28223]) ).

fof(f32269,plain,
    ! [X2,X0] : multiply(sF5,inverse(multiply(X2,inverse(sF5)))) = multiply(inverse(multiply(X0,X2)),X0),
    inference(forward_demodulation,[],[f32263,f31117]) ).

fof(f32275,plain,
    ! [X2,X0] : inverse(multiply(X2,inverse(sF5))) = multiply(inverse(multiply(X0,X2)),X0),
    inference(forward_demodulation,[],[f32269,f30139]) ).

fof(f32281,plain,
    ! [X2,X0] : inverse(multiply(X2,sF5)) = multiply(inverse(multiply(X0,X2)),X0),
    inference(forward_demodulation,[],[f32275,f28449]) ).

fof(f32287,plain,
    ! [X2,X0] : inverse(X2) = multiply(inverse(multiply(X0,X2)),X0),
    inference(forward_demodulation,[],[f32281,f30780]) ).

fof(f32355,plain,
    ! [X0,X1] : inverse(X1) = multiply(inverse(inverse(X0)),inverse(multiply(X1,X0))),
    inference(superposition,[],[f32287,f32287]) ).

fof(f32445,plain,
    ! [X0,X1] : inverse(inverse(multiply(X0,inverse(multiply(inverse(X0),X0))))) = multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))),
    inference(superposition,[],[f32287,f9869]) ).

fof(f32534,plain,
    ! [X2,X0,X1] : multiply(inverse(sF5),multiply(inverse(X1),X2)) = multiply(inverse(inverse(X0)),multiply(inverse(multiply(X1,X0)),X2)),
    inference(superposition,[],[f11082,f32287]) ).

fof(f32598,plain,
    ! [X0] : inverse(inverse(inverse(X0))) = inverse(multiply(sF5,X0)),
    inference(superposition,[],[f29522,f32287]) ).

fof(f32609,plain,
    ! [X0] : inverse(X0) = inverse(inverse(inverse(X0))),
    inference(forward_demodulation,[],[f32598,f30139]) ).

fof(f32672,plain,
    ! [X2,X0,X1] : multiply(inverse(sF5),multiply(inverse(X1),X2)) = multiply(X0,multiply(inverse(multiply(X1,X0)),X2)),
    inference(forward_demodulation,[],[f32534,f31117]) ).

fof(f32758,plain,
    ! [X0,X1] : inverse(inverse(multiply(X0,inverse(multiply(inverse(X0),X0))))) = multiply(X0,inverse(multiply(inverse(X1),X1))),
    inference(forward_demodulation,[],[f32445,f30632]) ).

fof(f32843,plain,
    ! [X0,X1] : inverse(X1) = multiply(X0,inverse(multiply(X1,X0))),
    inference(forward_demodulation,[],[f32355,f31117]) ).

fof(f32931,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X1,sF5)),X2) = multiply(X0,multiply(inverse(multiply(X1,X0)),X2)),
    inference(forward_demodulation,[],[f32672,f31401]) ).

fof(f33017,plain,
    ! [X0,X1] : inverse(inverse(multiply(X0,inverse(multiply(inverse(X0),X0))))) = multiply(X0,multiply(inverse(X1),X1)),
    inference(forward_demodulation,[],[f32758,f30632]) ).

fof(f33180,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),X2) = multiply(X0,multiply(inverse(multiply(X1,X0)),X2)),
    inference(forward_demodulation,[],[f32931,f30780]) ).

fof(f33262,plain,
    ! [X0] : inverse(inverse(multiply(X0,inverse(multiply(inverse(X0),X0))))) = multiply(X0,sF5),
    inference(forward_demodulation,[],[f33017,f10228]) ).

fof(f33470,plain,
    ! [X0] : inverse(inverse(multiply(X0,inverse(multiply(inverse(X0),X0))))) = X0,
    inference(forward_demodulation,[],[f33262,f30780]) ).

fof(f33660,plain,
    ! [X0] : inverse(inverse(inverse(inverse(X0)))) = X0,
    inference(forward_demodulation,[],[f33470,f32843]) ).

fof(f33828,plain,
    ! [X0] : inverse(inverse(X0)) = X0,
    inference(forward_demodulation,[],[f33660,f32609]) ).

fof(f36408,plain,
    ! [X0] : multiply(sF7,X0) = inverse(inverse(multiply(a3,inverse(multiply(inverse(X0),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))),
    inference(superposition,[],[f32843,f42]) ).

fof(f36530,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X0)),multiply(X1,X2)) = multiply(inverse(sF5),multiply(inverse(inverse(multiply(X0,X1))),X2)),
    inference(superposition,[],[f11082,f32843]) ).

fof(f36644,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X0)),multiply(X1,X2)) = multiply(inverse(multiply(inverse(multiply(X0,X1)),sF5)),X2),
    inference(forward_demodulation,[],[f36530,f31401]) ).

fof(f36763,plain,
    ! [X0] : multiply(a3,inverse(multiply(inverse(X0),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))) = multiply(sF7,X0),
    inference(forward_demodulation,[],[f36408,f33828]) ).

fof(f36911,plain,
    ! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(inverse(inverse(X0)),multiply(X1,X2)),
    inference(forward_demodulation,[],[f36644,f29742]) ).

fof(f37030,plain,
    ! [X0] : multiply(sF7,X0) = multiply(a3,multiply(inverse(inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),X0)),
    inference(forward_demodulation,[],[f36763,f30632]) ).

fof(f37174,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X0,X1),X2),
    inference(forward_demodulation,[],[f36911,f31117]) ).

fof(f37292,plain,
    ! [X0] : multiply(sF7,X0) = multiply(a3,multiply(multiply(b3,inverse(multiply(inverse(b3),b3))),X0)),
    inference(forward_demodulation,[],[f37030,f31117]) ).

fof(f37520,plain,
    ! [X0] : multiply(sF7,X0) = multiply(a3,multiply(b3,multiply(inverse(multiply(inverse(b3),b3)),X0))),
    inference(forward_demodulation,[],[f37292,f37174]) ).

fof(f37708,plain,
    ! [X0] : multiply(sF7,X0) = multiply(a3,multiply(inverse(inverse(b3)),X0)),
    inference(forward_demodulation,[],[f37520,f33180]) ).

fof(f37865,plain,
    ! [X0] : multiply(sF7,X0) = multiply(a3,multiply(b3,X0)),
    inference(forward_demodulation,[],[f37708,f31117]) ).

fof(f79036,plain,
    multiply(sF7,c3) = multiply(a3,sF9),
    inference(superposition,[],[f37865,f23]) ).

fof(f79147,plain,
    multiply(sF7,c3) = sF10,
    inference(forward_demodulation,[],[f79036,f25]) ).

fof(f79193,plain,
    sF8 = sF10,
    inference(forward_demodulation,[],[f79147,f21]) ).

fof(f79231,plain,
    ( $false
    | spl11_1 ),
    inference(forward_subsumption_resolution,[],[f79193,f30]) ).

fof(f79232,plain,
    spl11_1,
    inference(avatar_contradiction_clause,[],[f79231]) ).

fof(f79504,plain,
    ( sF1 != sF5
    | spl11_3 ),
    inference(forward_demodulation,[],[f38,f9367]) ).

fof(f79505,plain,
    ( $false
    | spl11_3 ),
    inference(forward_subsumption_resolution,[],[f79504,f9368]) ).

fof(f79506,plain,
    spl11_3,
    inference(avatar_contradiction_clause,[],[f79505]) ).

cnf(s1,plain,
    ( ~ spl11_1
    | ~ spl11_2
    | ~ spl11_3 ),
    inference(sat_conversion,[],[f39]) ).

cnf(s2,plain,
    spl11_2,
    inference(sat_conversion,[],[f30428]) ).

cnf(s4,plain,
    spl11_1,
    inference(sat_conversion,[],[f79232]) ).

cnf(s5,plain,
    spl11_3,
    inference(sat_conversion,[],[f79506]) ).

cnf(s6,plain,
    $false,
    inference(rat,[],[s1,s5,s2,s4]) ).

fof(f79507,plain,
    $false,
    inference(avatar_sat_refutation,[],[s6]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : GRP054-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.35  % Computer : n007.cluster.edu
% 0.11/0.35  % Model    : x86_64 x86_64
% 0.11/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35  % Memory   : 8046.5625MB
% 0.11/0.35  % OS       : Linux 6.8.0-71-generic
% 0.11/0.35  % CPULimit : 300
% 0.11/0.35  % WCLimit  : 300
% 0.11/0.35  % DateTime : Sun Sep 27 09:15:25 UTC 2026
% 0.11/0.35  % CPUTime  : 
% 0.11/0.35  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.40  Running first-order theorem proving
% 0.14/0.40  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.71/2.51  % (1144972)Input is clausal, will run a generic CNF schedule.
% 11.71/2.51  % (1145052)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2357783848:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.71/2.51  % (1145054)lrs+10_1_sil=8000:sp=occurrence:random_seed=1583399345:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.71/2.51  % (1145051)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4172819447:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.71/2.51  % (1145055)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4223208278:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.71/2.51  % (1145049)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4002798325:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.71/2.51  % (1145057)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=352259137:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.71/2.51  % (1145058)dis-21_1_sil=8000:lcm=predicate:random_seed=482864352:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.71/2.51  % (1145058)Refutation not found, incomplete strategy
% 11.71/2.51  % (1145058)------------------------------
% 11.71/2.51  % (1145058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.71/2.51  % (1145058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.71/2.51  % (1145058)CaDiCaL version: 2.1.3
% 11.71/2.51  % (1145058)Termination reason: Refutation not found, incomplete strategy
% 11.71/2.51  % (1145058)Time elapsed: 0.001 s
% 11.71/2.51  % (1145058)Peak memory usage: 88 MB
% 11.71/2.51  % (1145054)Instruction limit reached! 
% 11.71/2.51  % (1145054)------------------------------
% 11.71/2.51  % (1145054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.71/2.51  % (1145054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.71/2.51  % (1145054)CaDiCaL version: 2.1.3
% 11.71/2.51  % (1145054)Termination reason: Instruction limit
% 11.71/2.51  % (1145054)Termination phase: Saturation
% 11.71/2.51  % (1145054)Time elapsed: 0.060 s
% 11.71/2.51  % (1145054)Peak memory usage: 89 MB
% 11.71/2.51  % (1145054)Instructions burned: 108 (million)
% 11.71/2.51  % (1145055)Instruction limit reached! 
% 11.71/2.51  % (1145055)------------------------------
% 11.71/2.51  % (1145055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.71/2.51  % (1145055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.71/2.51  % (1145055)CaDiCaL version: 2.1.3
% 11.71/2.51  % (1145055)Termination reason: Instruction limit
% 11.71/2.51  % (1145055)Termination phase: Saturation
% 11.71/2.51  % (1145055)Time elapsed: 0.067 s
% 11.71/2.51  % (1145055)Peak memory usage: 88 MB
% 11.71/2.51  % (1145055)Instructions burned: 116 (million)
% 11.71/2.51  % (1145057)Instruction limit reached! 
% 11.71/2.51  % (1145057)------------------------------
% 11.71/2.51  % (1145057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.71/2.51  % (1145057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.71/2.51  % (1145057)CaDiCaL version: 2.1.3
% 11.71/2.51  % (1145057)Termination reason: Instruction limit
% 11.71/2.51  % (1145057)Termination phase: Saturation
% 11.71/2.51  % (1145057)Time elapsed: 0.092 s
% 11.71/2.51  % (1145057)Peak memory usage: 89 MB
% 11.71/2.51  % (1145057)Instructions burned: 182 (million)
% 11.71/2.51  % (1145098)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3741192466:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.71/2.51  % (1145098)Refutation not found, incomplete strategy
% 11.71/2.51  % (1145098)------------------------------
% 11.71/2.51  % (1145098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.71/2.51  % (1145098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.71/2.51  % (1145098)CaDiCaL version: 2.1.3
% 11.71/2.51  % (1145098)Termination reason: Refutation not found, incomplete strategy
% 11.71/2.51  % (1145098)Time elapsed: 0.001 s
% 11.71/2.51  % (1145098)Peak memory usage: 88 MB
% 11.71/2.51  % (1145099)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3298928281:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 20.89/3.92  % (1145099)Refutation not found, incomplete strategy
% 20.89/3.92  % (1145099)------------------------------
% 20.89/3.92  % (1145099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.89/3.92  % (1145099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.89/3.92  % (1145099)CaDiCaL version: 2.1.3
% 20.89/3.92  % (1145099)Termination reason: Refutation not found, incomplete strategy
% 20.89/3.92  % (1145099)Time elapsed: 0.001 s
% 20.89/3.92  % (1145099)Peak memory usage: 88 MB
% 20.89/3.92  % (1145100)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2999790189:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 20.89/3.92  % (1145100)Refutation not found, incomplete strategy
% 20.89/3.92  % (1145100)------------------------------
% 20.89/3.92  % (1145100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.89/3.92  % (1145100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.89/3.92  % (1145100)CaDiCaL version: 2.1.3
% 20.89/3.92  % (1145100)Termination reason: Refutation not found, incomplete strategy
% 20.89/3.92  % (1145100)Time elapsed: 0.001 s
% 20.89/3.92  % (1145100)Peak memory usage: 88 MB
% 20.89/3.92  % (1145058)------------------------------
% 20.89/3.92  % (1145058)------------------------------
% 20.89/3.92  % (1145151)lrs+10_64_to=lpo:sil=8000:random_seed=2743391289:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 20.89/3.92  % (1145098)------------------------------
% 20.89/3.92  % (1145098)------------------------------
% 20.89/3.92  % (1145099)------------------------------
% 20.89/3.92  % (1145099)------------------------------
% 20.89/3.92  % (1145100)------------------------------
% 20.89/3.92  % (1145100)------------------------------
% 20.89/3.92  % (1145151)Instruction limit reached! 
% 20.89/3.92  % (1145151)------------------------------
% 20.89/3.92  % (1145151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.89/3.92  % (1145151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.89/3.92  % (1145151)CaDiCaL version: 2.1.3
% 20.89/3.92  % (1145151)Termination reason: Instruction limit
% 20.89/3.92  % (1145151)Termination phase: Saturation
% 20.89/3.92  % (1145151)Time elapsed: 0.066 s
% 20.89/3.92  % (1145151)Peak memory usage: 88 MB
% 20.89/3.92  % (1145151)Instructions burned: 126 (million)
% 20.89/3.92  % (1145153)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3196060330:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 20.89/3.92  % (1145154)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1007888977:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 20.89/3.92  % (1145155)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3099506115:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 20.89/3.92  % (1145156)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=389250371:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 20.89/3.92  % (1145153)Instruction limit reached! 
% 20.89/3.92  % (1145153)------------------------------
% 20.89/3.92  % (1145153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.89/3.92  % (1145153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.89/3.92  % (1145153)CaDiCaL version: 2.1.3
% 20.89/3.92  % (1145153)Termination reason: Instruction limit
% 20.89/3.92  % (1145153)Termination phase: Saturation
% 20.89/3.92  % (1145153)Time elapsed: 0.100 s
% 20.89/3.92  % (1145153)Peak memory usage: 89 MB
% 20.89/3.92  % (1145153)Instructions burned: 194 (million)
% 20.89/3.92  % (1145156)Instruction limit reached! 
% 20.89/3.92  % (1145156)------------------------------
% 20.89/3.92  % (1145156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.89/3.92  % (1145156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.89/3.92  % (1145156)CaDiCaL version: 2.1.3
% 20.89/3.92  % (1145156)Termination reason: Instruction limit
% 20.89/3.92  % (1145156)Termination phase: Saturation
% 20.89/3.92  % (1145156)Time elapsed: 0.059 s
% 20.89/3.92  % (1145156)Peak memory usage: 89 MB
% 20.89/3.92  % (1145156)Instructions burned: 108 (million)
% 20.89/3.92  % (1145154)Instruction limit reached! 
% 20.89/3.92  % (1145154)------------------------------
% 20.89/3.92  % (1145154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.30  % (1145154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.30  % (1145154)CaDiCaL version: 2.1.3
% 23.88/4.30  % (1145154)Termination reason: Instruction limit
% 23.88/4.30  % (1145154)Termination phase: Saturation
% 23.88/4.30  % (1145154)Time elapsed: 0.081 s
% 23.88/4.30  % (1145154)Peak memory usage: 90 MB
% 23.88/4.30  % (1145154)Instructions burned: 157 (million)
% 23.88/4.30  % (1145161)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=214853188:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 23.88/4.30  % (1145163)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4102299322:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 23.88/4.30  % (1145162)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3335547348:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 23.88/4.30  % (1145161)Refutation not found, incomplete strategy
% 23.88/4.30  % (1145161)------------------------------
% 23.88/4.30  % (1145161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.30  % (1145161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.30  % (1145161)CaDiCaL version: 2.1.3
% 23.88/4.30  % (1145161)Termination reason: Refutation not found, incomplete strategy
% 23.88/4.30  % (1145161)Time elapsed: 0.001 s
% 23.88/4.30  % (1145161)Peak memory usage: 87 MB
% 23.88/4.30  % (1145162)Instruction limit reached! 
% 23.88/4.30  % (1145162)------------------------------
% 23.88/4.30  % (1145162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.30  % (1145162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.30  % (1145162)CaDiCaL version: 2.1.3
% 23.88/4.30  % (1145162)Termination reason: Instruction limit
% 23.88/4.30  % (1145162)Termination phase: Saturation
% 23.88/4.30  % (1145162)Time elapsed: 0.116 s
% 23.88/4.30  % (1145162)Peak memory usage: 90 MB
% 23.88/4.30  % (1145162)Instructions burned: 243 (million)
% 23.88/4.30  % (1145161)------------------------------
% 23.88/4.30  % (1145161)------------------------------
% 23.88/4.30  % (1145167)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1289499414:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 23.88/4.30  % (1145167)Instruction limit reached! 
% 23.88/4.30  % (1145167)------------------------------
% 23.88/4.30  % (1145167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.30  % (1145167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.30  % (1145167)CaDiCaL version: 2.1.3
% 23.88/4.30  % (1145167)Termination reason: Instruction limit
% 23.88/4.30  % (1145167)Termination phase: Saturation
% 23.88/4.30  % (1145167)Time elapsed: 0.074 s
% 23.88/4.30  % (1145167)Peak memory usage: 89 MB
% 23.88/4.30  % (1145167)Instructions burned: 134 (million)
% 23.88/4.30  % (1145168)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3616237505:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 23.88/4.30  % (1145170)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4225869924:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 23.88/4.30  % (1145170)Instruction limit reached! 
% 23.88/4.30  % (1145170)------------------------------
% 23.88/4.30  % (1145170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.30  % (1145170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.30  % (1145170)CaDiCaL version: 2.1.3
% 23.88/4.30  % (1145170)Termination reason: Instruction limit
% 23.88/4.30  % (1145170)Termination phase: Saturation
% 23.88/4.30  % (1145170)Time elapsed: 0.100 s
% 23.88/4.30  % (1145170)Peak memory usage: 89 MB
% 23.88/4.30  % (1145170)Instructions burned: 191 (million)
% 23.88/4.30  % (1145168)Instruction limit reached! 
% 23.88/4.30  % (1145168)------------------------------
% 23.88/4.30  % (1145168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.30  % (1145168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.30  % (1145168)CaDiCaL version: 2.1.3
% 23.88/4.30  % (1145168)Termination reason: Instruction limit
% 23.88/4.30  % (1145168)Termination phase: Saturation
% 23.88/4.30  % (1145168)Time elapsed: 0.255 s
% 23.88/4.30  % (1145168)Peak memory usage: 93 MB
% 23.88/4.30  % (1145168)Instructions burned: 500 (million)
% 23.88/4.30  % (1145173)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1429702871:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 23.88/4.30  % (1145174)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=178377283:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 23.88/4.30  % (1145173)Instruction limit reached! 
% 23.88/4.30  % (1145173)------------------------------
% 23.88/4.30  % (1145173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.30  % (1145173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.30  % (1145173)CaDiCaL version: 2.1.3
% 23.88/4.30  % (1145173)Termination reason: Instruction limit
% 23.88/4.30  % (1145173)Termination phase: Saturation
% 23.88/4.30  % (1145173)Time elapsed: 0.148 s
% 23.88/4.30  % (1145173)Peak memory usage: 91 MB
% 23.88/4.30  % (1145173)Instructions burned: 265 (million)
% 23.88/4.30  % (1145174)Instruction limit reached! 
% 23.88/4.30  % (1145174)------------------------------
% 23.88/4.30  % (1145174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.30  % (1145174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.30  % (1145174)CaDiCaL version: 2.1.3
% 23.88/4.30  % (1145174)Termination reason: Instruction limit
% 23.88/4.30  % (1145174)Termination phase: Saturation
% 23.88/4.30  % (1145174)Time elapsed: 0.091 s
% 23.88/4.30  % (1145174)Peak memory usage: 89 MB
% 23.88/4.30  % (1145174)Instructions burned: 157 (million)
% 23.88/4.30  % (1145178)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3460410946:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 23.88/4.30  % (1145177)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2675585304:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 23.88/4.30  % (1145178)Instruction limit reached! 
% 23.88/4.30  % (1145178)------------------------------
% 23.88/4.30  % (1145178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.30  % (1145178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.30  % (1145178)CaDiCaL version: 2.1.3
% 23.88/4.30  % (1145178)Termination reason: Instruction limit
% 23.88/4.30  % (1145178)Termination phase: Saturation
% 23.88/4.30  % (1145178)Time elapsed: 0.285 s
% 23.88/4.30  % (1145178)Peak memory usage: 97 MB
% 23.88/4.30  % (1145178)Instructions burned: 538 (million)
% 23.88/4.30  % (1145181)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4198403172:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi)
% 23.88/4.30  % (1145181)Instruction limit reached! 
% 23.88/4.30  % (1145181)------------------------------
% 23.88/4.30  % (1145181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.30  % (1145181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.30  % (1145181)CaDiCaL version: 2.1.3
% 23.88/4.30  % (1145181)Termination reason: Instruction limit
% 23.88/4.30  % (1145181)Termination phase: Saturation
% 23.88/4.30  % (1145181)Time elapsed: 0.094 s
% 23.88/4.30  % (1145181)Peak memory usage: 89 MB
% 23.88/4.30  % (1145181)Instructions burned: 181 (million)
% 23.88/4.30  % (1145183)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=444991470:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi)
% 24.63/4.30  % (1145155)Instruction limit reached! 
% 24.63/4.30  % (1145155)------------------------------
% 24.63/4.30  % (1145155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.63/4.30  % (1145155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.30  % (1145155)CaDiCaL version: 2.1.3
% 24.63/4.30  % (1145155)Termination reason: Instruction limit
% 24.63/4.30  % (1145155)Termination phase: Saturation
% 24.63/4.30  % (1145155)Time elapsed: 1.936 s
% 24.63/4.30  % (1145155)Peak memory usage: 151 MB
% 24.63/4.30  % (1145155)Instructions burned: 3395 (million)
% 24.63/4.30  % (1145185)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3563287377:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi)
% 24.63/4.30  % (1145185)Instruction limit reached! 
% 24.63/4.30  % (1145185)------------------------------
% 24.63/4.30  % (1145185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.63/4.30  % (1145185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.30  % (1145185)CaDiCaL version: 2.1.3
% 24.63/4.30  % (1145185)Termination reason: Instruction limit
% 24.63/4.30  % (1145185)Termination phase: Saturation
% 24.63/4.30  % (1145185)Time elapsed: 0.212 s
% 24.63/4.30  % (1145185)Peak memory usage: 93 MB
% 24.63/4.30  % (1145185)Instructions burned: 412 (million)
% 24.63/4.30  % (1145049)First to succeed.
% 24.63/4.30  % (1145049)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1144972"
% 24.63/4.30  % (1145187)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=86970694:s2pl=no:i=8478:s2at=4:nm=6_2969 on theBenchmark for (2969ds/8478Mi)
% 24.63/4.30  % (1145049)Refutation found. Thanks to Tanya!
% 24.63/4.30  % SZS status Unsatisfiable for theBenchmark
% 24.63/4.30  % SZS output start Proof for theBenchmark
% See solution above
% 24.73/4.49  % (1145049)------------------------------
% 24.73/4.49  % (1145049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.73/4.49  % (1145049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.73/4.49  % (1145049)CaDiCaL version: 2.1.3
% 24.73/4.49  % (1145049)Termination reason: Refutation
% 24.73/4.49  % (1145049)Time elapsed: 3.003 s
% 24.73/4.49  % (1145049)Peak memory usage: 169 MB
% 24.73/4.49  % (1145049)Instructions burned: 5179 (million)
% 24.73/4.49  % (1145049)------------------------------
% 24.73/4.49  % (1145049)------------------------------
% 24.73/4.49  % (1144972)Success in time 3.405 s
% 24.73/4.49  % Vampire exiting
%------------------------------------------------------------------------------