Vampire---5.0.1.UNS-Ref.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : GRP057-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM

% Computer : n005.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:26 AM UTC 2026

% Result   : Unsatisfiable 17.48s 3.54s
% Output   : Refutation 18.77s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   63
%            Number of leaves      :   16
% Syntax   : Number of formulae    :  642 ( 632 unt;  14 def)
%            Number of atoms       :  657 ( 637 equ)
%            Maximal formula atoms :    3 (   1 avg)
%            Number of connectives :   31 (  16   ~;  12   |;   0   &)
%                                         (   3 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   12 (   3 avg)
%            Maximal term depth    :   18 (   3 avg)
%            Number of predicates  :    5 (   3 usr;   4 prp; 0-2 aty)
%            Number of functors    :   20 (  20 usr;  18 con; 0-2 aty)
%            Number of variables   : 1524 (   0 sgn1524   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    ! [X2,X3,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),X3),inverse(multiply(X1,X3))))) = X2,
    file('/export/starexec/sandbox2/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/sandbox2/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(f39,plain,
    ( ~ spl11_1
    | ~ spl11_2
    | ~ spl11_3 ),
    inference(avatar_split_clause,[],[f26,f36,f32,f28]) ).

fof(f40,plain,
    multiply(inverse(a1),a1) = sF1,
    inference(forward_demodulation,[],[f7,f5]) ).

fof(f41,plain,
    multiply(inverse(b1),b1) = sF3,
    inference(forward_demodulation,[],[f11,f9]) ).

fof(f42,plain,
    multiply(inverse(b2),b2) = sF5,
    inference(forward_demodulation,[],[f15,f13]) ).

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

fof(f52,plain,
    ! [X0,X1] : b1 = multiply(b1,inverse(multiply(multiply(inverse(multiply(inverse(X0),sF3)),X1),inverse(multiply(X0,X1))))),
    inference(superposition,[],[f1,f41]) ).

fof(f58,plain,
    ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X5),multiply(inverse(inverse(X0)),X2))),X6),inverse(multiply(X5,X6))),inverse(multiply(multiply(inverse(multiply(inverse(X9),X7)),X10),inverse(multiply(X9,X10))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3)))))),X7))),X8),inverse(multiply(X4,X8)))),
    inference(superposition,[],[f43,f43]) ).

fof(f59,plain,
    ! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(X6),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(inverse(inverse(X2))),X0))),X4),inverse(multiply(X3,X4)))))),X7),inverse(multiply(X6,X7))))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X5),inverse(multiply(X1,X5)))),
    inference(superposition,[],[f43,f1]) ).

fof(f86,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3)))) = multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(a1)),X2)),a1),inverse(sF1)))),
    inference(superposition,[],[f43,f40]) ).

fof(f90,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3)))) = multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),b3),inverse(sF7)))),
    inference(superposition,[],[f43,f19]) ).

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

fof(f105,plain,
    ! [X2,X3,X0,X1,X6,X7,X4,X5] : inverse(multiply(multiply(inverse(multiply(inverse(X5),X2)),X6),inverse(multiply(X5,X6)))) = multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X4),inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(inverse(X1))),X2))),X3),inverse(multiply(X0,X3)))))),X7),inverse(multiply(X4,X7))))),
    inference(superposition,[],[f1,f43]) ).

fof(f115,plain,
    ! [X2,X1,X6,X7,X4,X5] : inverse(multiply(multiply(inverse(multiply(inverse(X5),X2)),X6),inverse(multiply(X5,X6)))) = multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),b3),inverse(sF7)))))),X7),inverse(multiply(X4,X7))))),
    inference(backward_demodulation,[],[f105,f90]) ).

fof(f140,plain,
    ! [X2,X0,X1,X6,X7,X5] : inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X5),inverse(multiply(X1,X5)))) = multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(X6),multiply(inverse(X2),inverse(multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1)))))),X7),inverse(multiply(X6,X7))))),
    inference(forward_demodulation,[],[f59,f86]) ).

fof(f141,plain,
    ! [X2,X6,X5] : inverse(multiply(multiply(inverse(multiply(inverse(X5),X2)),X6),inverse(multiply(X5,X6)))) = inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),b3),inverse(sF7))),
    inference(forward_demodulation,[],[f115,f1]) ).

fof(f172,plain,
    ! [X0,X1,X5] : inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X5),inverse(multiply(X1,X5)))) = inverse(multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1))),
    inference(forward_demodulation,[],[f140,f1]) ).

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

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

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

fof(f223,plain,
    ! [X2,X3,X0,X1,X6,X4,X5] : multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X5),inverse(multiply(multiply(inverse(multiply(inverse(X2),X0)),X3),inverse(multiply(X2,X3)))))),X6),inverse(multiply(X5,X6))))) = inverse(multiply(multiply(inverse(X0),X4),inverse(multiply(inverse(inverse(X1)),X4)))),
    inference(superposition,[],[f43,f99]) ).

fof(f224,plain,
    ! [X2,X3,X0,X1,X6,X7,X4,X5] : inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(inverse(X2)),multiply(X3,inverse(multiply(multiply(inverse(multiply(inverse(X4),X0)),X5),inverse(multiply(X4,X5)))))))),X6),inverse(multiply(X1,X6)))) = multiply(X2,inverse(multiply(multiply(inverse(X0),X7),inverse(multiply(X3,X7))))),
    inference(superposition,[],[f43,f99]) ).

fof(f236,plain,
    ! [X2,X3,X0,X7,X4,X5] : multiply(X2,inverse(multiply(multiply(inverse(X0),X7),inverse(multiply(X3,X7))))) = multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(inverse(a1)),multiply(X3,inverse(multiply(multiply(inverse(multiply(inverse(X4),X0)),X5),inverse(multiply(X4,X5))))))),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f224,f86]) ).

fof(f263,plain,
    ! [X2,X3,X0,X1,X6,X4,X5] : multiply(X5,inverse(multiply(multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X2),X0)),X3),inverse(multiply(X2,X3)))))),X6),inverse(multiply(inverse(X5),X6))))) = inverse(multiply(multiply(inverse(X0),X4),inverse(multiply(X1,X4)))),
    inference(superposition,[],[f222,f99]) ).

fof(f265,plain,
    ! [X2,X0,X1] : inverse(multiply(multiply(inverse(sF3),X0),inverse(multiply(b1,X0)))) = multiply(X1,inverse(multiply(multiply(inverse(b1),X2),inverse(multiply(inverse(X1),X2))))),
    inference(superposition,[],[f222,f41]) ).

fof(f266,plain,
    ! [X2,X0,X1] : inverse(multiply(multiply(inverse(sF5),X0),inverse(multiply(b2,X0)))) = multiply(X1,inverse(multiply(multiply(inverse(b2),X2),inverse(multiply(inverse(X1),X2))))),
    inference(superposition,[],[f222,f42]) ).

fof(f280,plain,
    ! [X2,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(inverse(b2)),X0)),b2),inverse(sF5))) = multiply(X1,inverse(multiply(multiply(inverse(X0),X2),inverse(multiply(inverse(X1),X2))))),
    inference(superposition,[],[f222,f42]) ).

fof(f283,plain,
    ! [X2,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(b3),X0)),c3),inverse(sF9))) = multiply(X1,inverse(multiply(multiply(inverse(X0),X2),inverse(multiply(inverse(X1),X2))))),
    inference(superposition,[],[f222,f23]) ).

fof(f295,plain,
    ! [X2,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(X0),b1)),X1),inverse(multiply(X0,X1)))) = multiply(X2,inverse(multiply(sF3,inverse(multiply(inverse(X2),b1))))),
    inference(superposition,[],[f222,f41]) ).

fof(f296,plain,
    ! [X2,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(X0),b2)),X1),inverse(multiply(X0,X1)))) = multiply(X2,inverse(multiply(sF5,inverse(multiply(inverse(X2),b2))))),
    inference(superposition,[],[f222,f42]) ).

fof(f303,plain,
    ! [X2,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X0,X2)))) = multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))),
    inference(superposition,[],[f222,f40]) ).

fof(f304,plain,
    ! [X2,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X0,X2)))) = multiply(b1,inverse(multiply(multiply(inverse(X1),b1),inverse(sF3)))),
    inference(superposition,[],[f222,f41]) ).

fof(f323,plain,
    ! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X3),X1)),X4),inverse(multiply(X3,X4))),inverse(multiply(multiply(inverse(multiply(inverse(X5),multiply(multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(inverse(X0),X2))))),X6))),X7),inverse(multiply(X5,X7))))) = X6,
    inference(superposition,[],[f1,f222]) ).

fof(f324,plain,
    ! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X4),X1)),X5),inverse(multiply(X4,X5))),inverse(multiply(multiply(inverse(multiply(inverse(X8),X6)),X9),inverse(multiply(X8,X9))))) = inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(inverse(X0),X2)))))),X6))),X7),inverse(multiply(X3,X7)))),
    inference(superposition,[],[f43,f222]) ).

fof(f354,plain,
    ! [X3,X0,X1,X4] : inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(inverse(X1)),X0))),X4),inverse(multiply(X3,X4)))) = multiply(X1,multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3))))),
    inference(backward_demodulation,[],[f43,f304]) ).

fof(f356,plain,
    ! [X2,X10,X0,X8,X6,X9,X7,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X5),multiply(inverse(inverse(X0)),X2))),X6),inverse(multiply(X5,X6))),inverse(multiply(multiply(inverse(multiply(inverse(X9),X7)),X10),inverse(multiply(X9,X10))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(multiply(X0,multiply(b1,inverse(multiply(multiply(inverse(X2),b1),inverse(sF3)))))),X7))),X8),inverse(multiply(X4,X8)))),
    inference(backward_demodulation,[],[f58,f304]) ).

fof(f368,plain,
    ! [X2,X0] : multiply(inverse(X0),multiply(X0,multiply(b1,inverse(multiply(multiply(inverse(X2),b1),inverse(sF3)))))) = X2,
    inference(backward_demodulation,[],[f99,f304]) ).

fof(f375,plain,
    ! [X2] : inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),b3),inverse(sF7))) = multiply(b1,inverse(multiply(multiply(inverse(X2),b1),inverse(sF3)))),
    inference(backward_demodulation,[],[f141,f304]) ).

fof(f380,plain,
    ! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1))) = multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3)))),
    inference(backward_demodulation,[],[f172,f304]) ).

fof(f384,plain,
    ! [X2,X0,X1,X5] : multiply(inverse(X1),multiply(X1,inverse(multiply(multiply(inverse(X0),X5),inverse(multiply(X2,X5)))))) = multiply(X2,multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3))))),
    inference(backward_demodulation,[],[f198,f304]) ).

fof(f385,plain,
    ! [X2,X0,X4] : multiply(inverse(inverse(X0)),X2) = multiply(inverse(X4),multiply(X4,multiply(X0,multiply(b1,inverse(multiply(multiply(inverse(X2),b1),inverse(sF3))))))),
    inference(backward_demodulation,[],[f220,f304]) ).

fof(f386,plain,
    ! [X0,X1,X4] : multiply(X1,inverse(multiply(multiply(inverse(X0),X4),inverse(multiply(inverse(X1),X4))))) = multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3)))),
    inference(backward_demodulation,[],[f222,f304]) ).

fof(f387,plain,
    ! [X0,X1,X6,X4,X5] : inverse(multiply(multiply(inverse(X0),X4),inverse(multiply(inverse(inverse(X1)),X4)))) = multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X5),multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3)))))),X6),inverse(multiply(X5,X6))))),
    inference(backward_demodulation,[],[f223,f304]) ).

fof(f393,plain,
    ! [X2,X3,X0,X7] : multiply(X2,inverse(multiply(multiply(inverse(X0),X7),inverse(multiply(X3,X7))))) = multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(inverse(a1)),multiply(X3,multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3))))))),a1),inverse(sF1)))),
    inference(backward_demodulation,[],[f236,f304]) ).

fof(f398,plain,
    ! [X2,X3,X0,X1,X6,X7,X4,X5] : inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(inverse(X0),X2)))))),X6))),X7),inverse(multiply(X3,X7)))) = multiply(multiply(multiply(inverse(multiply(inverse(X4),X1)),X5),inverse(multiply(X4,X5))),multiply(b1,inverse(multiply(multiply(inverse(X6),b1),inverse(sF3))))),
    inference(backward_demodulation,[],[f324,f304]) ).

fof(f410,plain,
    ! [X2,X0] : multiply(X0,multiply(b1,inverse(multiply(multiply(inverse(multiply(inverse(X0),X2)),b1),inverse(sF3))))) = X2,
    inference(backward_demodulation,[],[f1,f304]) ).

fof(f414,plain,
    ! [X2,X3,X0,X1,X6,X4] : multiply(multiply(multiply(inverse(multiply(inverse(X3),X1)),X4),inverse(multiply(X3,X4))),multiply(b1,inverse(multiply(multiply(inverse(multiply(multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(inverse(X0),X2))))),X6)),b1),inverse(sF3))))) = X6,
    inference(backward_demodulation,[],[f323,f304]) ).

fof(f416,plain,
    b1 = multiply(b1,multiply(b1,inverse(multiply(multiply(inverse(sF3),b1),inverse(sF3))))),
    inference(backward_demodulation,[],[f52,f304]) ).

fof(f418,plain,
    ! [X1] : multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))) = multiply(b1,inverse(multiply(multiply(inverse(X1),b1),inverse(sF3)))),
    inference(backward_demodulation,[],[f304,f303]) ).

fof(f425,plain,
    ! [X2] : multiply(X2,inverse(multiply(sF5,inverse(multiply(inverse(X2),b2))))) = multiply(a1,inverse(multiply(multiply(inverse(b2),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f296,f303]) ).

fof(f426,plain,
    ! [X2] : multiply(X2,inverse(multiply(sF3,inverse(multiply(inverse(X2),b1))))) = multiply(a1,inverse(multiply(multiply(inverse(b1),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f295,f303]) ).

fof(f445,plain,
    ! [X0,X1,X6,X4,X5] : inverse(multiply(multiply(inverse(X0),X4),inverse(multiply(X1,X4)))) = multiply(X5,inverse(multiply(multiply(inverse(multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))))),X6),inverse(multiply(inverse(X5),X6))))),
    inference(forward_demodulation,[],[f263,f303]) ).

fof(f460,plain,
    ! [X2,X0,X1,X6,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X4),X1)),X5),inverse(multiply(X4,X5))),multiply(b1,inverse(multiply(multiply(inverse(X6),b1),inverse(sF3))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(inverse(X0),X2)))))),X6)),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f398,f303]) ).

fof(f465,plain,
    ! [X0,X1,X4] : inverse(multiply(multiply(inverse(X0),X4),inverse(multiply(inverse(inverse(X1)),X4)))) = multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3))))),a1),inverse(sF1))))),
    inference(forward_demodulation,[],[f387,f303]) ).

fof(f469,plain,
    ! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(inverse(b2)),X0)),b2),inverse(sF5))) = multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3)))),
    inference(backward_demodulation,[],[f280,f386]) ).

fof(f472,plain,
    ! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(b3),X0)),c3),inverse(sF9))) = multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3)))),
    inference(backward_demodulation,[],[f283,f386]) ).

fof(f484,plain,
    ! [X3,X1,X6,X4] : multiply(multiply(multiply(inverse(multiply(inverse(X3),X1)),X4),inverse(multiply(X3,X4))),multiply(b1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(multiply(inverse(X1),b1),inverse(sF3)))),X6)),b1),inverse(sF3))))) = X6,
    inference(backward_demodulation,[],[f414,f386]) ).

fof(f488,plain,
    ! [X0] : inverse(multiply(multiply(inverse(sF3),X0),inverse(multiply(b1,X0)))) = multiply(b1,inverse(multiply(multiply(inverse(b1),b1),inverse(sF3)))),
    inference(backward_demodulation,[],[f265,f386]) ).

fof(f489,plain,
    ! [X0] : inverse(multiply(multiply(inverse(sF5),X0),inverse(multiply(b2,X0)))) = multiply(b1,inverse(multiply(multiply(inverse(b2),b1),inverse(sF3)))),
    inference(backward_demodulation,[],[f266,f386]) ).

fof(f514,plain,
    ! [X2,X3,X0,X7] : multiply(X2,inverse(multiply(multiply(inverse(X0),X7),inverse(multiply(X3,X7))))) = multiply(X2,multiply(b1,inverse(multiply(multiply(inverse(multiply(X3,multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3)))))),b1),inverse(sF3))))),
    inference(backward_demodulation,[],[f393,f380]) ).

fof(f533,plain,
    ! [X2,X10,X0,X6,X9,X7,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X5),multiply(inverse(inverse(X0)),X2))),X6),inverse(multiply(X5,X6))),inverse(multiply(multiply(inverse(multiply(inverse(X9),X7)),X10),inverse(multiply(X9,X10))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,multiply(b1,inverse(multiply(multiply(inverse(X2),b1),inverse(sF3)))))),X7)),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f356,f303]) ).

fof(f535,plain,
    ! [X0,X1] : multiply(X1,multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(X1)),X0)),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f354,f303]) ).

fof(f542,plain,
    ! [X2,X0] : multiply(inverse(X0),multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))))) = X2,
    inference(backward_demodulation,[],[f368,f418]) ).

fof(f543,plain,
    ! [X2] : inverse(multiply(multiply(inverse(multiply(inverse(a3),X2)),b3),inverse(sF7))) = multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))),
    inference(backward_demodulation,[],[f375,f418]) ).

fof(f544,plain,
    ! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1))) = multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))),
    inference(backward_demodulation,[],[f380,f418]) ).

fof(f545,plain,
    ! [X2,X0,X1,X5] : multiply(inverse(X1),multiply(X1,inverse(multiply(multiply(inverse(X0),X5),inverse(multiply(X2,X5)))))) = multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),
    inference(backward_demodulation,[],[f384,f418]) ).

fof(f546,plain,
    ! [X2,X0,X4] : multiply(inverse(inverse(X0)),X2) = multiply(inverse(X4),multiply(X4,multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1))))))),
    inference(backward_demodulation,[],[f385,f418]) ).

fof(f547,plain,
    ! [X0,X1,X4] : multiply(X1,inverse(multiply(multiply(inverse(X0),X4),inverse(multiply(inverse(X1),X4))))) = multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))),
    inference(backward_demodulation,[],[f386,f418]) ).

fof(f553,plain,
    ! [X2,X0] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X0),X2)),a1),inverse(sF1))))) = X2,
    inference(backward_demodulation,[],[f410,f418]) ).

fof(f555,plain,
    b1 = multiply(b1,multiply(a1,inverse(multiply(multiply(inverse(sF3),a1),inverse(sF1))))),
    inference(backward_demodulation,[],[f416,f418]) ).

fof(f573,plain,
    ! [X2,X0,X1,X6,X4,X5] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(inverse(X0),X2)))))),X6)),a1),inverse(sF1)))) = multiply(multiply(multiply(inverse(multiply(inverse(X4),X1)),X5),inverse(multiply(X4,X5))),multiply(a1,inverse(multiply(multiply(inverse(X6),a1),inverse(sF1))))),
    inference(forward_demodulation,[],[f460,f418]) ).

fof(f577,plain,
    ! [X0,X1,X4] : inverse(multiply(multiply(inverse(X0),X4),inverse(multiply(inverse(inverse(X1)),X4)))) = multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),a1),inverse(sF1))))),
    inference(forward_demodulation,[],[f465,f418]) ).

fof(f578,plain,
    ! [X0] : inverse(multiply(multiply(inverse(sF5),X0),inverse(multiply(b2,X0)))) = multiply(a1,inverse(multiply(multiply(inverse(b2),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f489,f418]) ).

fof(f579,plain,
    ! [X0] : inverse(multiply(multiply(inverse(sF3),X0),inverse(multiply(b1,X0)))) = multiply(a1,inverse(multiply(multiply(inverse(b1),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f488,f418]) ).

fof(f583,plain,
    ! [X3,X1,X6,X4] : multiply(multiply(multiply(inverse(multiply(inverse(X3),X1)),X4),inverse(multiply(X3,X4))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(multiply(inverse(X1),b1),inverse(sF3)))),X6)),a1),inverse(sF1))))) = X6,
    inference(forward_demodulation,[],[f484,f418]) ).

fof(f595,plain,
    ! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(b3),X0)),c3),inverse(sF9))) = multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f472,f418]) ).

fof(f598,plain,
    ! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(inverse(b2)),X0)),b2),inverse(sF5))) = multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f469,f418]) ).

fof(f611,plain,
    ! [X2,X3,X0,X7] : multiply(X2,inverse(multiply(multiply(inverse(X0),X7),inverse(multiply(X3,X7))))) = multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(multiply(X3,multiply(b1,inverse(multiply(multiply(inverse(X0),b1),inverse(sF3)))))),a1),inverse(sF1))))),
    inference(forward_demodulation,[],[f514,f418]) ).

fof(f644,plain,
    ! [X2,X10,X0,X6,X9,X7,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X5),multiply(inverse(inverse(X0)),X2))),X6),inverse(multiply(X5,X6))),inverse(multiply(multiply(inverse(multiply(inverse(X9),X7)),X10),inverse(multiply(X9,X10))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))))),X7)),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f533,f418]) ).

fof(f646,plain,
    ! [X0,X1] : multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(X1)),X0)),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f535,f418]) ).

fof(f663,plain,
    ! [X0,X1,X4] : inverse(multiply(multiply(inverse(X0),X4),inverse(multiply(X1,X4)))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))))),a1),inverse(sF1)))),
    inference(backward_demodulation,[],[f445,f547]) ).

fof(f680,plain,
    ! [X1,X6,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X4),X1)),X5),inverse(multiply(X4,X5))),multiply(a1,inverse(multiply(multiply(inverse(X6),a1),inverse(sF1))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),X6)),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f573,f547]) ).

fof(f683,plain,
    ! [X3,X1,X6,X4] : multiply(multiply(multiply(inverse(multiply(inverse(X3),X1)),X4),inverse(multiply(X3,X4))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))),X6)),a1),inverse(sF1))))) = X6,
    inference(forward_demodulation,[],[f583,f418]) ).

fof(f701,plain,
    ! [X2,X3,X0,X7] : multiply(X2,inverse(multiply(multiply(inverse(X0),X7),inverse(multiply(X3,X7))))) = multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(multiply(X3,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(forward_demodulation,[],[f611,f418]) ).

fof(f720,plain,
    ! [X2,X0,X6,X7,X5] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))))),X7)),a1),inverse(sF1)))) = multiply(multiply(multiply(inverse(multiply(inverse(X5),multiply(inverse(inverse(X0)),X2))),X6),inverse(multiply(X5,X6))),multiply(a1,inverse(multiply(multiply(inverse(X7),a1),inverse(sF1))))),
    inference(forward_demodulation,[],[f644,f303]) ).

fof(f773,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(inverse(X2)),multiply(inverse(inverse(X0)),X1)) = multiply(inverse(X3),multiply(X3,multiply(X2,multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))))),
    inference(superposition,[],[f546,f646]) ).

fof(f774,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X1)),multiply(inverse(X1),X0)) = multiply(inverse(X2),multiply(X2,X0)),
    inference(superposition,[],[f546,f553]) ).

fof(f784,plain,
    ! [X0] : multiply(inverse(X0),multiply(X0,a1)) = multiply(inverse(inverse(a1)),sF1),
    inference(superposition,[],[f774,f40]) ).

fof(f785,plain,
    ! [X0] : multiply(inverse(X0),multiply(X0,b1)) = multiply(inverse(inverse(b1)),sF3),
    inference(superposition,[],[f774,f41]) ).

fof(f791,plain,
    ! [X3,X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(X3),multiply(X3,X1)),
    inference(superposition,[],[f774,f774]) ).

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

fof(f802,plain,
    ! [X0] : multiply(inverse(inverse(X0)),multiply(inverse(X0),a2)) = multiply(inverse(sF5),sF6),
    inference(superposition,[],[f774,f17]) ).

fof(f808,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),a1),inverse(sF1))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(X0,X1))),a1),inverse(sF1)))),
    inference(superposition,[],[f646,f774]) ).

fof(f824,plain,
    ! [X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(X0,X1))),a1),inverse(sF1)))) = X1,
    inference(forward_demodulation,[],[f808,f553]) ).

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

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

fof(f864,plain,
    ! [X0] : multiply(inverse(X0),multiply(X0,c3)) = multiply(inverse(b3),sF9),
    inference(superposition,[],[f791,f23]) ).

fof(f866,plain,
    ! [X0] : multiply(inverse(sF7),sF8) = multiply(inverse(X0),multiply(X0,c3)),
    inference(superposition,[],[f791,f21]) ).

fof(f891,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X3),multiply(X3,multiply(X2,X1))) = multiply(inverse(inverse(X2)),multiply(inverse(X0),multiply(X0,X1))),
    inference(superposition,[],[f774,f791]) ).

fof(f899,plain,
    ! [X0,X1] : multiply(inverse(inverse(a1)),multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))) = X1,
    inference(superposition,[],[f542,f791]) ).

fof(f901,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(inverse(X2)),multiply(inverse(X2),multiply(X3,X1))) = multiply(inverse(inverse(X3)),multiply(inverse(X0),multiply(X0,X1))),
    inference(superposition,[],[f774,f791]) ).

fof(f908,plain,
    multiply(inverse(sF7),sF8) = multiply(inverse(b3),sF9),
    inference(superposition,[],[f864,f21]) ).

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

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

fof(f1424,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))) = multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(inverse(a1)),sF1),inverse(multiply(X2,multiply(X1,a1))))))),
    inference(superposition,[],[f545,f784]) ).

fof(f1432,plain,
    ! [X0,X1] : multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(b1),a1),inverse(sF1))))) = multiply(inverse(X0),multiply(X0,inverse(multiply(sF3,inverse(multiply(X1,b1)))))),
    inference(superposition,[],[f545,f41]) ).

fof(f1502,plain,
    ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(X2),multiply(X2,multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))))) = multiply(inverse(inverse(inverse(X3))),multiply(inverse(X5),multiply(X5,multiply(X3,inverse(multiply(multiply(inverse(X1),X4),inverse(multiply(X0,X4)))))))),
    inference(superposition,[],[f891,f545]) ).

fof(f1503,plain,
    ! [X3,X0,X1,X4,X5] : multiply(inverse(inverse(X0)),X1) = multiply(inverse(inverse(inverse(X3))),multiply(inverse(X5),multiply(X5,multiply(X3,inverse(multiply(multiply(inverse(X1),X4),inverse(multiply(X0,X4)))))))),
    inference(forward_demodulation,[],[f1502,f546]) ).

fof(f1748,plain,
    ! [X0,X1] : multiply(multiply(multiply(inverse(sF5),X0),inverse(multiply(b2,X0))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(b2),a1),inverse(sF1)))),X1)),a1),inverse(sF1))))) = X1,
    inference(superposition,[],[f553,f578]) ).

fof(f1878,plain,
    ! [X0] : multiply(a1,inverse(multiply(multiply(inverse(b2),a1),inverse(sF1)))) = multiply(multiply(multiply(inverse(sF5),X0),inverse(multiply(b2,X0))),inverse(multiply(sF5,inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(b2),a1),inverse(sF1)))),b2))))),
    inference(superposition,[],[f425,f578]) ).

fof(f1885,plain,
    ! [X0] : inverse(multiply(sF5,inverse(multiply(inverse(X0),b2)))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(a1,inverse(multiply(multiply(inverse(b2),a1),inverse(sF1)))))),a1),inverse(sF1)))),
    inference(superposition,[],[f824,f425]) ).

fof(f1916,plain,
    ! [X0,X1] : multiply(multiply(inverse(multiply(inverse(a3),X0)),b3),inverse(sF7)) = multiply(inverse(X1),multiply(X1,multiply(a1,inverse(multiply(multiply(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))),a1),inverse(sF1)))))),
    inference(superposition,[],[f542,f543]) ).

fof(f2255,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF3),X1),inverse(multiply(b1,X1))) = multiply(inverse(X0),multiply(X0,multiply(a1,inverse(multiply(multiply(multiply(a1,inverse(multiply(multiply(inverse(b1),a1),inverse(sF1)))),a1),inverse(sF1)))))),
    inference(superposition,[],[f542,f579]) ).

fof(f2262,plain,
    ! [X0,X1] : multiply(multiply(multiply(inverse(sF3),X0),inverse(multiply(b1,X0))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(b1),a1),inverse(sF1)))),X1)),a1),inverse(sF1))))) = X1,
    inference(superposition,[],[f553,f579]) ).

fof(f2291,plain,
    ! [X1] : multiply(multiply(inverse(sF3),X1),inverse(multiply(b1,X1))) = multiply(multiply(inverse(multiply(inverse(a3),b1)),b3),inverse(sF7)),
    inference(forward_demodulation,[],[f2255,f1916]) ).

fof(f2638,plain,
    multiply(a1,inverse(multiply(multiply(inverse(b1),a1),inverse(sF1)))) = multiply(b1,inverse(multiply(sF3,inverse(sF3)))),
    inference(superposition,[],[f426,f41]) ).

fof(f2653,plain,
    ! [X0] : inverse(multiply(sF3,inverse(multiply(inverse(inverse(X0)),b1)))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(b1),a1),inverse(sF1))))),a1),inverse(sF1))))),
    inference(superposition,[],[f553,f426]) ).

fof(f2668,plain,
    ! [X2] : multiply(X2,inverse(multiply(sF3,inverse(multiply(inverse(X2),b1))))) = multiply(b1,inverse(multiply(sF3,inverse(sF3)))),
    inference(backward_demodulation,[],[f426,f2638]) ).

fof(f2669,plain,
    ! [X0] : inverse(multiply(multiply(inverse(sF3),X0),inverse(multiply(b1,X0)))) = multiply(b1,inverse(multiply(sF3,inverse(sF3)))),
    inference(backward_demodulation,[],[f579,f2638]) ).

fof(f2670,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(multiply(sF3,inverse(multiply(X1,b1)))))) = multiply(X1,multiply(b1,inverse(multiply(sF3,inverse(sF3))))),
    inference(backward_demodulation,[],[f1432,f2638]) ).

fof(f2696,plain,
    ! [X0,X1] : multiply(multiply(multiply(inverse(sF3),X0),inverse(multiply(b1,X0))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X1)),a1),inverse(sF1))))) = X1,
    inference(backward_demodulation,[],[f2262,f2638]) ).

fof(f2721,plain,
    ! [X0] : inverse(multiply(sF3,inverse(multiply(inverse(inverse(X0)),b1)))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(b1,inverse(multiply(sF3,inverse(sF3))))),a1),inverse(sF1))))),
    inference(backward_demodulation,[],[f2653,f2638]) ).

fof(f2789,plain,
    ! [X0] : multiply(b1,multiply(a1,inverse(multiply(multiply(inverse(sF3),a1),inverse(sF1))))) = multiply(inverse(X0),multiply(X0,multiply(b1,inverse(multiply(sF3,inverse(sF3)))))),
    inference(superposition,[],[f545,f2669]) ).

fof(f2793,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF3),X1),inverse(multiply(b1,X1))) = multiply(inverse(X0),multiply(X0,multiply(a1,inverse(multiply(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),a1),inverse(sF1)))))),
    inference(superposition,[],[f542,f2669]) ).

fof(f2833,plain,
    ! [X0] : b1 = multiply(inverse(X0),multiply(X0,multiply(b1,inverse(multiply(sF3,inverse(sF3)))))),
    inference(forward_demodulation,[],[f2789,f555]) ).

fof(f2843,plain,
    ! [X2,X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(X2,X1))),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(X0,multiply(a1,X1)))),a1),inverse(sF1))),
    inference(superposition,[],[f544,f891]) ).

fof(f2871,plain,
    ! [X0,X1] : multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1)) = multiply(inverse(X1),multiply(X1,multiply(a1,inverse(multiply(multiply(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))),a1),inverse(sF1)))))),
    inference(superposition,[],[f542,f544]) ).

fof(f2880,plain,
    ! [X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),X1)),a1),inverse(sF1)))) = multiply(multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1)),multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),
    inference(superposition,[],[f646,f544]) ).

fof(f2913,plain,
    ! [X0] : multiply(multiply(inverse(multiply(inverse(a3),X0)),b3),inverse(sF7)) = multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1)),
    inference(backward_demodulation,[],[f1916,f2871]) ).

fof(f2921,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(X0,multiply(a1,X1)))),a1),inverse(sF1))) = X1,
    inference(forward_demodulation,[],[f2843,f824]) ).

fof(f2945,plain,
    ! [X1] : multiply(multiply(inverse(multiply(inverse(inverse(a1)),b1)),a1),inverse(sF1)) = multiply(multiply(inverse(sF3),X1),inverse(multiply(b1,X1))),
    inference(backward_demodulation,[],[f2291,f2913]) ).

fof(f3559,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(multiply(inverse(sF3),X3),inverse(multiply(b1,X3))),multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1))))) = multiply(inverse(X1),multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),a1),inverse(sF1))))),inverse(X0))))),
    inference(superposition,[],[f545,f2696]) ).

fof(f3861,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),multiply(X2,X0)))),X3),inverse(multiply(X1,X3))),multiply(a1,inverse(multiply(multiply(inverse(multiply(X0,X4)),a1),inverse(sF1))))) = X4,
    inference(superposition,[],[f683,f824]) ).

fof(f3871,plain,
    ! [X2,X3,X0,X1,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5))),multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1))))) = multiply(inverse(X1),multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(X3),a1),inverse(sF1)))),X0)),a1),inverse(sF1))))),inverse(X0))))),
    inference(superposition,[],[f545,f683]) ).

fof(f3925,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF3),X1),inverse(multiply(b1,X1))) = multiply(multiply(inverse(sF3),X0),inverse(multiply(b1,X0))),
    inference(superposition,[],[f2945,f2945]) ).

fof(f4257,plain,
    ! [X0] : inverse(multiply(sF3,inverse(multiply(X0,b1)))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(X0,multiply(b1,inverse(multiply(sF3,inverse(sF3)))))),a1),inverse(sF1)))),
    inference(superposition,[],[f824,f2670]) ).

fof(f4309,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),inverse(multiply(b2,multiply(sF5,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X0,X2)))))))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(b2),a1),inverse(sF1)))),X3)),a1),inverse(sF1))))) = X3,
    inference(superposition,[],[f1748,f545]) ).

fof(f4434,plain,
    ! [X3,X0,X1,X4] : multiply(inverse(X1),multiply(X1,inverse(multiply(multiply(X0,X3),inverse(multiply(X4,X3)))))) = multiply(X4,multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1))))),
    inference(superposition,[],[f545,f2921]) ).

fof(f4438,plain,
    ! [X3,X0,X1] : multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))) = multiply(X1,inverse(multiply(multiply(X0,X3),inverse(multiply(inverse(X1),X3))))),
    inference(superposition,[],[f547,f2921]) ).

fof(f4443,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(inverse(multiply(inverse(X1),multiply(multiply(inverse(multiply(inverse(X2),multiply(X2,multiply(a1,X0)))),a1),inverse(sF1)))),X3),inverse(multiply(X1,X3))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))),X4)),a1),inverse(sF1))))) = X4,
    inference(superposition,[],[f683,f2921]) ).

fof(f4636,plain,
    ! [X2,X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1))))),a1),inverse(sF1)))) = multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(inverse(multiply(multiply(X0,X2),inverse(multiply(inverse(inverse(inverse(X1))),X2))))),a1),inverse(sF1))))),
    inference(superposition,[],[f646,f4438]) ).

fof(f4637,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1))))),a1),inverse(sF1))) = multiply(a1,inverse(multiply(multiply(inverse(inverse(multiply(multiply(X0,X1),inverse(multiply(inverse(inverse(inverse(a1))),X1))))),a1),inverse(sF1)))),
    inference(superposition,[],[f544,f4438]) ).

fof(f4715,plain,
    ! [X0,X1] : multiply(multiply(inverse(multiply(inverse(inverse(b2)),X0)),b2),inverse(sF5)) = multiply(inverse(X1),multiply(X1,multiply(a1,inverse(multiply(multiply(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))),a1),inverse(sF1)))))),
    inference(superposition,[],[f542,f598]) ).

fof(f4765,plain,
    ! [X0] : multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1)) = multiply(multiply(inverse(multiply(inverse(inverse(b2)),X0)),b2),inverse(sF5)),
    inference(forward_demodulation,[],[f4715,f2871]) ).

fof(f4927,plain,
    ! [X0,X1] : multiply(multiply(inverse(multiply(inverse(b3),X0)),c3),inverse(sF9)) = multiply(inverse(X1),multiply(X1,multiply(a1,inverse(multiply(multiply(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))),a1),inverse(sF1)))))),
    inference(superposition,[],[f542,f595]) ).

fof(f4977,plain,
    ! [X0] : multiply(multiply(inverse(multiply(inverse(b3),X0)),c3),inverse(sF9)) = multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1)),
    inference(forward_demodulation,[],[f4927,f2871]) ).

fof(f5012,plain,
    ! [X0,X1] : multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1)) = multiply(inverse(inverse(a1)),multiply(inverse(X1),multiply(X1,inverse(multiply(multiply(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))),a1),inverse(sF1)))))),
    inference(superposition,[],[f899,f544]) ).

fof(f5013,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(multiply(inverse(X2),multiply(X2,multiply(a1,X0)))),a1),inverse(sF1)) = multiply(inverse(inverse(a1)),multiply(inverse(X1),multiply(X1,inverse(multiply(multiply(X0,a1),inverse(sF1)))))),
    inference(superposition,[],[f899,f2921]) ).

fof(f5605,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(inverse(a1)),sF1),inverse(multiply(X2,multiply(X1,a1)))))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f784]) ).

fof(f5607,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(inverse(b1)),sF3),inverse(multiply(X2,multiply(X1,b1)))))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f785]) ).

fof(f5613,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(a3),sF7),inverse(multiply(X2,multiply(X1,b3)))))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f863]) ).

fof(f5615,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(b3),sF9),inverse(multiply(X2,multiply(X1,c3)))))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f864]) ).

fof(f5616,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(a3),sF10),inverse(multiply(X2,multiply(X1,sF9)))))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f862]) ).

fof(f5653,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,a1)),inverse(multiply(inverse(inverse(a1)),sF1))))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f784]) ).

fof(f5655,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,b1)),inverse(multiply(inverse(inverse(b1)),sF3))))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f785]) ).

fof(f5661,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,b3)),inverse(multiply(inverse(a3),sF7))))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f863]) ).

fof(f5663,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,c3)),inverse(multiply(inverse(b3),sF9))))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f864]) ).

fof(f5664,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,sF9)),inverse(multiply(inverse(a3),sF10))))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f862]) ).

fof(f5665,plain,
    ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(multiply(inverse(sF3),X3),inverse(multiply(b1,X3))),multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f2696]) ).

fof(f5668,plain,
    ! [X2,X3,X0,X1,X4,X5] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(X3),a1),inverse(sF1)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5))),multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f701,f683]) ).

fof(f5715,plain,
    ! [X2,X3,X0,X1] : multiply(X2,inverse(multiply(multiply(inverse(X1),X3),inverse(multiply(inverse(inverse(X0)),X3))))) = multiply(X2,multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),a1),inverse(sF1)))))),
    inference(superposition,[],[f701,f646]) ).

fof(f5924,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,c3)),inverse(multiply(inverse(b3),sF9))))) = multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,sF9)),inverse(multiply(inverse(a3),sF10))))),
    inference(backward_demodulation,[],[f5664,f5663]) ).

fof(f5926,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,b3)),inverse(multiply(inverse(a3),sF7))))) = multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,c3)),inverse(multiply(inverse(b3),sF9))))),
    inference(backward_demodulation,[],[f5663,f5661]) ).

fof(f5932,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,b1)),inverse(multiply(inverse(inverse(b1)),sF3))))) = multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,b3)),inverse(multiply(inverse(a3),sF7))))),
    inference(backward_demodulation,[],[f5661,f5655]) ).

fof(f5934,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,a1)),inverse(multiply(inverse(inverse(a1)),sF1))))) = multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,b1)),inverse(multiply(inverse(inverse(b1)),sF3))))),
    inference(backward_demodulation,[],[f5655,f5653]) ).

fof(f5982,plain,
    ! [X2,X3,X0,X1,X4,X5] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(X3),a1),inverse(sF1)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,inverse(multiply(multiply(inverse(a3),sF10),inverse(multiply(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5))),multiply(X2,sF9)))))),
    inference(backward_demodulation,[],[f5668,f5616]) ).

fof(f5985,plain,
    ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,inverse(multiply(multiply(inverse(a3),sF10),inverse(multiply(multiply(multiply(inverse(sF3),X3),inverse(multiply(b1,X3))),multiply(X2,sF9)))))),
    inference(backward_demodulation,[],[f5665,f5616]) ).

fof(f6003,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(b3),sF9),inverse(multiply(X2,multiply(X1,c3)))))) = multiply(X0,inverse(multiply(multiply(inverse(a3),sF10),inverse(multiply(X2,multiply(X1,sF9)))))),
    inference(backward_demodulation,[],[f5616,f5615]) ).

fof(f6005,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(a3),sF7),inverse(multiply(X2,multiply(X1,b3)))))) = multiply(X0,inverse(multiply(multiply(inverse(b3),sF9),inverse(multiply(X2,multiply(X1,c3)))))),
    inference(backward_demodulation,[],[f5615,f5613]) ).

fof(f6011,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(inverse(b1)),sF3),inverse(multiply(X2,multiply(X1,b1)))))) = multiply(X0,inverse(multiply(multiply(inverse(a3),sF7),inverse(multiply(X2,multiply(X1,b3)))))),
    inference(backward_demodulation,[],[f5613,f5607]) ).

fof(f6013,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(inverse(a1)),sF1),inverse(multiply(X2,multiply(X1,a1)))))) = multiply(X0,inverse(multiply(multiply(inverse(inverse(b1)),sF3),inverse(multiply(X2,multiply(X1,b1)))))),
    inference(backward_demodulation,[],[f5607,f5605]) ).

fof(f6050,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,b3)),inverse(multiply(inverse(a3),sF7))))) = multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,sF9)),inverse(multiply(inverse(a3),sF10))))),
    inference(backward_demodulation,[],[f5924,f5926]) ).

fof(f6058,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,a1)),inverse(multiply(inverse(inverse(a1)),sF1))))) = multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,b3)),inverse(multiply(inverse(a3),sF7))))),
    inference(backward_demodulation,[],[f5932,f5934]) ).

fof(f6094,plain,
    ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,inverse(multiply(multiply(inverse(b3),sF9),inverse(multiply(multiply(multiply(inverse(sF3),X3),inverse(multiply(b1,X3))),multiply(X2,c3)))))),
    inference(backward_demodulation,[],[f5985,f6003]) ).

fof(f6097,plain,
    ! [X2,X3,X0,X1,X4,X5] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(X3),a1),inverse(sF1)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,inverse(multiply(multiply(inverse(b3),sF9),inverse(multiply(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5))),multiply(X2,c3)))))),
    inference(backward_demodulation,[],[f5982,f6003]) ).

fof(f6127,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(inverse(b1)),sF3),inverse(multiply(X2,multiply(X1,b1)))))) = multiply(X0,inverse(multiply(multiply(inverse(b3),sF9),inverse(multiply(X2,multiply(X1,c3)))))),
    inference(backward_demodulation,[],[f6005,f6011]) ).

fof(f6157,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,a1)),inverse(multiply(inverse(inverse(a1)),sF1))))) = multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X2,sF9)),inverse(multiply(inverse(a3),sF10))))),
    inference(backward_demodulation,[],[f6050,f6058]) ).

fof(f6170,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(inverse(a1)),sF1),inverse(multiply(X2,multiply(X1,a1)))))) = multiply(X0,inverse(multiply(multiply(inverse(b3),sF9),inverse(multiply(X2,multiply(X1,c3)))))),
    inference(forward_demodulation,[],[f6127,f6013]) ).

fof(f6198,plain,
    ! [X2,X3,X0,X1,X4,X5] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(X3),a1),inverse(sF1)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,inverse(multiply(multiply(inverse(inverse(a1)),sF1),inverse(multiply(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5))),multiply(X2,a1)))))),
    inference(backward_demodulation,[],[f6097,f6170]) ).

fof(f6201,plain,
    ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,inverse(multiply(multiply(inverse(inverse(a1)),sF1),inverse(multiply(multiply(multiply(inverse(sF3),X3),inverse(multiply(b1,X3))),multiply(X2,a1)))))),
    inference(backward_demodulation,[],[f6094,f6170]) ).

fof(f7478,plain,
    ! [X0,X1] : multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),a1),inverse(sF1))))) = inverse(multiply(multiply(inverse(X0),multiply(inverse(X1),a1)),inverse(multiply(inverse(inverse(a1)),sF1)))),
    inference(superposition,[],[f577,f784]) ).

fof(f7486,plain,
    ! [X0,X1] : multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),a1),inverse(sF1))))) = inverse(multiply(multiply(inverse(X0),multiply(inverse(X1),c3)),inverse(multiply(inverse(sF7),sF8)))),
    inference(superposition,[],[f577,f866]) ).

fof(f7487,plain,
    ! [X0,X1] : multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),a1),inverse(sF1))))) = inverse(multiply(multiply(inverse(X0),multiply(inverse(X1),c3)),inverse(multiply(inverse(b3),sF9)))),
    inference(superposition,[],[f577,f864]) ).

fof(f7488,plain,
    ! [X0,X1] : multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),a1),inverse(sF1))))) = inverse(multiply(multiply(inverse(X0),multiply(inverse(X1),sF9)),inverse(multiply(inverse(a3),sF10)))),
    inference(superposition,[],[f577,f862]) ).

fof(f7510,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),X1)),X2),inverse(multiply(inverse(inverse(X3)),X2)))) = multiply(X3,multiply(a1,inverse(multiply(multiply(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f577,f646]) ).

fof(f7600,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X2),multiply(X2,multiply(X3,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),a1),inverse(sF1)))))) = multiply(inverse(inverse(X3)),inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(inverse(inverse(inverse(a1))),X1))))),
    inference(superposition,[],[f891,f577]) ).

fof(f7613,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),a1),inverse(sF1))))),a1),inverse(sF1))))) = multiply(a1,inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(inverse(inverse(inverse(inverse(X2)))),X1))))),a1),inverse(sF1)))),
    inference(superposition,[],[f646,f577]) ).

fof(f7676,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),X1)),X2),inverse(multiply(inverse(inverse(X3)),X2)))) = multiply(X3,inverse(multiply(multiply(inverse(inverse(a1)),sF1),inverse(multiply(X0,multiply(X1,a1)))))),
    inference(forward_demodulation,[],[f7510,f5605]) ).

fof(f7686,plain,
    ! [X2,X3,X0,X1] : multiply(X2,inverse(multiply(multiply(inverse(X1),X3),inverse(multiply(inverse(inverse(X0)),X3))))) = multiply(X2,inverse(multiply(multiply(inverse(X1),multiply(inverse(X0),sF9)),inverse(multiply(inverse(a3),sF10))))),
    inference(backward_demodulation,[],[f5715,f7488]) ).

fof(f7728,plain,
    ! [X2,X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(inverse(inverse(inverse(inverse(X2)))),X1))))),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),multiply(inverse(X2),sF9)),inverse(multiply(inverse(a3),sF10)))),
    inference(backward_demodulation,[],[f7613,f7488]) ).

fof(f7745,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(X0),multiply(inverse(X1),c3)),inverse(multiply(inverse(b3),sF9)))) = inverse(multiply(multiply(inverse(X0),multiply(inverse(X1),sF9)),inverse(multiply(inverse(a3),sF10)))),
    inference(backward_demodulation,[],[f7488,f7487]) ).

fof(f7746,plain,
    ! [X0,X1] : multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),a1),inverse(sF1))))) = inverse(multiply(multiply(inverse(X0),multiply(inverse(X1),c3)),inverse(multiply(inverse(b3),sF9)))),
    inference(forward_demodulation,[],[f7486,f908]) ).

fof(f7844,plain,
    ! [X2,X3,X0,X1] : multiply(X2,inverse(multiply(multiply(inverse(X1),X3),inverse(multiply(inverse(inverse(X0)),X3))))) = multiply(X2,inverse(multiply(multiply(inverse(X1),multiply(inverse(X0),a1)),inverse(multiply(inverse(inverse(a1)),sF1))))),
    inference(forward_demodulation,[],[f7686,f6157]) ).

fof(f7891,plain,
    ! [X2,X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(inverse(inverse(inverse(inverse(X2)))),X1))))),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),multiply(inverse(X2),c3)),inverse(multiply(inverse(b3),sF9)))),
    inference(backward_demodulation,[],[f7728,f7745]) ).

fof(f7893,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(X0),multiply(inverse(X1),a1)),inverse(multiply(inverse(inverse(a1)),sF1)))) = inverse(multiply(multiply(inverse(X0),multiply(inverse(X1),c3)),inverse(multiply(inverse(b3),sF9)))),
    inference(forward_demodulation,[],[f7746,f7478]) ).

fof(f7968,plain,
    ! [X2,X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(inverse(inverse(inverse(inverse(X2)))),X1))))),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),multiply(inverse(X2),a1)),inverse(multiply(inverse(inverse(a1)),sF1)))),
    inference(backward_demodulation,[],[f7891,f7893]) ).

fof(f8004,plain,
    ! [X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))))),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(inverse(a1)),sF1),inverse(multiply(X1,multiply(X0,a1))))),
    inference(superposition,[],[f663,f784]) ).

fof(f8068,plain,
    ! [X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))))),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(X0),multiply(X1,c3)),inverse(multiply(inverse(sF7),sF8)))),
    inference(superposition,[],[f663,f866]) ).

fof(f8069,plain,
    ! [X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))))),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(X0),multiply(X1,c3)),inverse(multiply(inverse(b3),sF9)))),
    inference(superposition,[],[f663,f864]) ).

fof(f8070,plain,
    ! [X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))))),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(X0),multiply(X1,sF9)),inverse(multiply(inverse(a3),sF10)))),
    inference(superposition,[],[f663,f862]) ).

fof(f8112,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X0))),X2),inverse(multiply(X3,X2)))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(X3,X0)),a1),inverse(sF1)))),
    inference(superposition,[],[f663,f824]) ).

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

fof(f8184,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(inverse(X1),X3),inverse(multiply(X0,X3))) = multiply(inverse(inverse(a1)),multiply(inverse(X2),multiply(X2,inverse(multiply(multiply(multiply(a1,inverse(multiply(multiply(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))),a1),inverse(sF1)))),a1),inverse(sF1)))))),
    inference(superposition,[],[f899,f663]) ).

fof(f8231,plain,
    ! [X3,X0,X1] : multiply(multiply(inverse(X1),X3),inverse(multiply(X0,X3))) = multiply(multiply(inverse(multiply(inverse(inverse(a1)),multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))))),a1),inverse(sF1)),
    inference(forward_demodulation,[],[f8184,f5012]) ).

fof(f8263,plain,
    ! [X0] : inverse(multiply(sF5,inverse(multiply(inverse(X0),b2)))) = inverse(multiply(multiply(inverse(b2),multiply(X0,sF9)),inverse(multiply(inverse(a3),sF10)))),
    inference(backward_demodulation,[],[f1885,f8070]) ).

fof(f8266,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(X0),multiply(X1,c3)),inverse(multiply(inverse(b3),sF9)))) = inverse(multiply(multiply(inverse(X0),multiply(X1,sF9)),inverse(multiply(inverse(a3),sF10)))),
    inference(backward_demodulation,[],[f8070,f8069]) ).

fof(f8267,plain,
    ! [X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))))),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(X0),multiply(X1,c3)),inverse(multiply(inverse(b3),sF9)))),
    inference(forward_demodulation,[],[f8068,f908]) ).

fof(f8441,plain,
    ! [X0] : inverse(multiply(sF5,inverse(multiply(inverse(X0),b2)))) = inverse(multiply(multiply(inverse(b2),multiply(X0,c3)),inverse(multiply(inverse(b3),sF9)))),
    inference(backward_demodulation,[],[f8263,f8266]) ).

fof(f8442,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(X0),multiply(X1,c3)),inverse(multiply(inverse(b3),sF9)))) = inverse(multiply(multiply(inverse(inverse(a1)),sF1),inverse(multiply(inverse(X1),multiply(X0,a1))))),
    inference(forward_demodulation,[],[f8267,f8004]) ).

fof(f8607,plain,
    ! [X0] : inverse(multiply(sF5,inverse(multiply(inverse(X0),b2)))) = inverse(multiply(multiply(inverse(inverse(a1)),sF1),inverse(multiply(inverse(X0),multiply(b2,a1))))),
    inference(backward_demodulation,[],[f8441,f8442]) ).

fof(f8968,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(multiply(inverse(X1),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),a1),inverse(sF1))))),inverse(X0))) = inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(multiply(multiply(inverse(sF3),X3),inverse(multiply(b1,X3))),X2)))),
    inference(superposition,[],[f8131,f2696]) ).

fof(f8971,plain,
    ! [X2,X3,X0,X1,X4,X5] : inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(multiply(multiply(inverse(multiply(inverse(X3),X4)),X5),inverse(multiply(X3,X5))),X2)))) = inverse(multiply(multiply(inverse(X1),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(X4),a1),inverse(sF1)))),X0)),a1),inverse(sF1))))),inverse(X0))),
    inference(superposition,[],[f8131,f683]) ).

fof(f9126,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(X0),X4),inverse(multiply(X2,X4))) = multiply(inverse(inverse(a1)),multiply(inverse(X3),multiply(X3,inverse(multiply(multiply(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))),a1),inverse(sF1)))))),
    inference(superposition,[],[f899,f8131]) ).

fof(f9132,plain,
    ! [X2,X3,X0,X1] : multiply(b1,inverse(multiply(sF3,inverse(sF3)))) = multiply(multiply(multiply(inverse(X0),X3),inverse(multiply(X2,X3))),inverse(multiply(sF3,inverse(multiply(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))),b1))))),
    inference(superposition,[],[f2668,f8131]) ).

fof(f9137,plain,
    ! [X2,X0,X1,X4] : multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1))) = multiply(multiply(inverse(X0),X4),inverse(multiply(X2,X4))),
    inference(forward_demodulation,[],[f9126,f899]) ).

fof(f9371,plain,
    ! [X2,X3,X0,X4] : multiply(multiply(X0,X2),inverse(multiply(X3,X2))) = multiply(multiply(X0,X4),inverse(multiply(X3,X4))),
    inference(superposition,[],[f9137,f2921]) ).

fof(f9933,plain,
    ! [X0,X1] : multiply(multiply(X0,a1),inverse(sF1)) = multiply(multiply(X0,X1),inverse(multiply(inverse(a1),X1))),
    inference(superposition,[],[f9371,f40]) ).

fof(f9935,plain,
    ! [X0,X1] : multiply(multiply(X0,b2),inverse(sF5)) = multiply(multiply(X0,X1),inverse(multiply(inverse(b2),X1))),
    inference(superposition,[],[f9371,f42]) ).

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

fof(f9967,plain,
    ! [X0,X1] : multiply(multiply(X0,X1),inverse(multiply(b3,X1))) = multiply(multiply(X0,c3),inverse(sF9)),
    inference(superposition,[],[f9371,f23]) ).

fof(f10048,plain,
    ! [X2,X0,X1] : inverse(multiply(X1,inverse(multiply(sF3,inverse(sF3))))) = multiply(multiply(multiply(inverse(sF3),X2),inverse(multiply(b1,X2))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,X0),inverse(multiply(X1,X0)))),a1),inverse(sF1))))),
    inference(superposition,[],[f2696,f9371]) ).

fof(f10564,plain,
    ! [X0] : multiply(multiply(a3,X0),inverse(multiply(a3,X0))) = multiply(sF7,inverse(sF7)),
    inference(superposition,[],[f9966,f19]) ).

fof(f10763,plain,
    ! [X0] : multiply(sF7,inverse(sF7)) = multiply(X0,inverse(X0)),
    inference(superposition,[],[f10564,f553]) ).

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

fof(f10902,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(sF7,inverse(sF7))) = multiply(inverse(X0),multiply(X0,inverse(X1))),
    inference(superposition,[],[f791,f10763]) ).

fof(f10908,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X1)),multiply(inverse(X2),multiply(sF7,inverse(sF7)))) = multiply(inverse(inverse(X0)),multiply(inverse(X0),multiply(X1,inverse(X2)))),
    inference(superposition,[],[f901,f10763]) ).

fof(f10925,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(X1,inverse(inverse(X0)))) = multiply(inverse(inverse(X0)),multiply(sF7,inverse(sF7))),
    inference(superposition,[],[f774,f10763]) ).

fof(f10929,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X1)),multiply(inverse(inverse(X2)),multiply(sF7,inverse(sF7)))) = multiply(inverse(inverse(X0)),multiply(inverse(X0),multiply(X1,inverse(inverse(X2))))),
    inference(superposition,[],[f798,f10763]) ).

fof(f10938,plain,
    ! [X0] : multiply(a1,inverse(multiply(multiply(inverse(multiply(sF7,inverse(sF7))),a1),inverse(sF1)))) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(X0)))),a1),inverse(sF1))))),
    inference(superposition,[],[f646,f10763]) ).

fof(f10958,plain,
    ! [X0] : multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))) = multiply(X0,inverse(multiply(sF7,inverse(sF7)))),
    inference(superposition,[],[f4438,f10763]) ).

fof(f11178,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(X0,inverse(X0))) = multiply(inverse(X1),multiply(X1,inverse(X2))),
    inference(superposition,[],[f791,f10852]) ).

fof(f11197,plain,
    ! [X0,X1] : inverse(inverse(X1)) = multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(X0,inverse(X0))),a1),inverse(sF1))))),
    inference(superposition,[],[f553,f10852]) ).

fof(f11201,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(X2,inverse(inverse(X1)))) = multiply(inverse(inverse(X1)),multiply(X0,inverse(X0))),
    inference(superposition,[],[f774,f10852]) ).

fof(f11261,plain,
    ! [X0,X1] : b1 = multiply(inverse(X1),multiply(X1,multiply(b1,inverse(multiply(X0,inverse(X0)))))),
    inference(superposition,[],[f2833,f10852]) ).

fof(f11262,plain,
    ! [X0,X1] : inverse(multiply(sF3,inverse(multiply(inverse(inverse(X1)),b1)))) = multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(b1,inverse(multiply(X0,inverse(X0))))),a1),inverse(sF1))))),
    inference(superposition,[],[f2721,f10852]) ).

fof(f11546,plain,
    ! [X2,X3,X0] : multiply(inverse(X3),multiply(X3,X0)) = multiply(X0,multiply(X2,inverse(X2))),
    inference(superposition,[],[f11178,f2921]) ).

fof(f11604,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(X0,inverse(X1)))),X3),inverse(multiply(X1,X3))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(multiply(X2,inverse(X2))),a1),inverse(sF1)))),X4)),a1),inverse(sF1))))) = X4,
    inference(superposition,[],[f683,f11178]) ).

fof(f11695,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(X1,inverse(X1)))),a1),inverse(sF1))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(a1),inverse(X0))),a1),inverse(sF1)))),
    inference(superposition,[],[f544,f11178]) ).

fof(f11792,plain,
    ! [X2,X3,X0,X1] : multiply(X0,multiply(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,multiply(a1,X0)))),a1),inverse(sF1)),X2)) = multiply(X2,multiply(X3,inverse(X3))),
    inference(superposition,[],[f11546,f2921]) ).

fof(f11888,plain,
    ! [X3,X0,X1] : multiply(X0,multiply(X1,inverse(X1))) = multiply(X0,multiply(X3,inverse(X3))),
    inference(superposition,[],[f11546,f11546]) ).

fof(f12012,plain,
    ! [X0] : multiply(inverse(sF5),sF6) = multiply(a2,multiply(X0,inverse(X0))),
    inference(superposition,[],[f802,f11546]) ).

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

fof(f12428,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(X1,inverse(X1)))),X3),inverse(multiply(X0,X3))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(multiply(X2,inverse(X2))),a1),inverse(sF1)))),X4)),a1),inverse(sF1))))) = X4,
    inference(superposition,[],[f683,f11888]) ).

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

fof(f13249,plain,
    ! [X0,X1] : inverse(inverse(X0)) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(multiply(inverse(sF3),X1),inverse(multiply(b1,X1))),multiply(b1,inverse(multiply(sF3,inverse(sF3)))))),a1),inverse(sF1))))),
    inference(superposition,[],[f11197,f2669]) ).

fof(f13271,plain,
    ! [X0,X1] : inverse(inverse(X1)) = multiply(X1,multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(X0)))),a1),inverse(sF1)))))),
    inference(superposition,[],[f11197,f646]) ).

fof(f13304,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(X1,X3),inverse(multiply(X0,X3))) = multiply(multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(X2,inverse(X2))),a1),inverse(sF1))))),inverse(inverse(inverse(X0)))),
    inference(superposition,[],[f9371,f11197]) ).

fof(f13320,plain,
    ! [X2,X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))))),a1),inverse(sF1)))) = inverse(multiply(inverse(inverse(inverse(X0))),inverse(multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(multiply(X1,inverse(X1))),a1),inverse(sF1)))))))),
    inference(superposition,[],[f663,f11197]) ).

fof(f13334,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),a1),inverse(sF1))))) = inverse(multiply(multiply(inverse(X1),multiply(a1,inverse(multiply(multiply(inverse(multiply(X2,inverse(X2))),a1),inverse(sF1))))),inverse(inverse(inverse(inverse(inverse(X0))))))),
    inference(superposition,[],[f577,f11197]) ).

fof(f13336,plain,
    ! [X0] : multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(multiply(X0,inverse(X0))),a1),inverse(sF1))))),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(inverse(inverse(inverse(inverse(a1))))),a1),inverse(sF1))),
    inference(superposition,[],[f544,f11197]) ).

fof(f13353,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF3),X1),inverse(multiply(b1,X1))) = multiply(multiply(inverse(sF3),multiply(a1,inverse(multiply(multiply(inverse(multiply(X0,inverse(X0))),a1),inverse(sF1))))),inverse(inverse(inverse(b1)))),
    inference(superposition,[],[f3925,f11197]) ).

fof(f13358,plain,
    ! [X0] : multiply(a1,inverse(multiply(multiply(inverse(b2),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(sF5),multiply(a1,inverse(multiply(multiply(inverse(multiply(X0,inverse(X0))),a1),inverse(sF1))))),inverse(inverse(inverse(b2))))),
    inference(superposition,[],[f578,f11197]) ).

fof(f13361,plain,
    ! [X0,X1] : multiply(multiply(X0,b3),inverse(sF7)) = multiply(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(X1,inverse(X1))),a1),inverse(sF1))))),inverse(inverse(inverse(a3)))),
    inference(superposition,[],[f9966,f11197]) ).

fof(f13364,plain,
    ! [X0,X1] : multiply(multiply(X0,c3),inverse(sF9)) = multiply(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(X1,inverse(X1))),a1),inverse(sF1))))),inverse(inverse(inverse(b3)))),
    inference(superposition,[],[f9967,f11197]) ).

fof(f13365,plain,
    ! [X0] : multiply(multiply(X0,c3),inverse(sF9)) = multiply(inverse(inverse(X0)),inverse(inverse(inverse(b3)))),
    inference(forward_demodulation,[],[f13364,f11197]) ).

fof(f13368,plain,
    ! [X0] : multiply(multiply(X0,b3),inverse(sF7)) = multiply(inverse(inverse(X0)),inverse(inverse(inverse(a3)))),
    inference(forward_demodulation,[],[f13361,f11197]) ).

fof(f13369,plain,
    multiply(a1,inverse(multiply(multiply(inverse(b2),a1),inverse(sF1)))) = inverse(multiply(inverse(inverse(inverse(sF5))),inverse(inverse(inverse(b2))))),
    inference(forward_demodulation,[],[f13358,f11197]) ).

fof(f13374,plain,
    ! [X1] : multiply(multiply(inverse(sF3),X1),inverse(multiply(b1,X1))) = multiply(inverse(inverse(inverse(sF3))),inverse(inverse(inverse(b1)))),
    inference(forward_demodulation,[],[f13353,f11197]) ).

fof(f13387,plain,
    ! [X0,X1] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),a1),inverse(sF1))))) = inverse(multiply(inverse(inverse(inverse(X1))),inverse(inverse(inverse(inverse(inverse(X0))))))),
    inference(forward_demodulation,[],[f13334,f11197]) ).

fof(f13401,plain,
    ! [X2,X0] : multiply(a1,inverse(multiply(multiply(inverse(multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1)))))),a1),inverse(sF1)))) = inverse(multiply(inverse(inverse(inverse(X0))),inverse(inverse(inverse(X2))))),
    inference(forward_demodulation,[],[f13320,f11197]) ).

fof(f13408,plain,
    ! [X3,X0,X1] : multiply(multiply(X1,X3),inverse(multiply(X0,X3))) = multiply(inverse(inverse(X1)),inverse(inverse(inverse(X0)))),
    inference(forward_demodulation,[],[f13304,f11197]) ).

fof(f13437,plain,
    ! [X0,X1] : inverse(inverse(X0)) = multiply(X0,inverse(multiply(sF3,inverse(multiply(multiply(multiply(inverse(sF3),X1),inverse(multiply(b1,X1))),b1))))),
    inference(forward_demodulation,[],[f13249,f4257]) ).

fof(f13544,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(X0),multiply(inverse(X1),a1)),inverse(multiply(inverse(inverse(a1)),sF1)))) = inverse(multiply(inverse(inverse(inverse(X0))),inverse(inverse(inverse(inverse(inverse(X1))))))),
    inference(backward_demodulation,[],[f7478,f13387]) ).

fof(f13550,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(inverse(a1)),sF1),inverse(multiply(X1,multiply(X0,a1))))) = inverse(multiply(inverse(inverse(inverse(X0))),inverse(inverse(inverse(X1))))),
    inference(backward_demodulation,[],[f8004,f13401]) ).

fof(f13566,plain,
    ! [X2,X3,X0,X1] : multiply(X2,inverse(multiply(multiply(inverse(X1),X3),inverse(multiply(inverse(inverse(X0)),X3))))) = multiply(X2,inverse(multiply(inverse(inverse(inverse(X1))),inverse(inverse(inverse(inverse(inverse(X0)))))))),
    inference(backward_demodulation,[],[f7844,f13544]) ).

fof(f13622,plain,
    ! [X2,X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(inverse(inverse(inverse(inverse(X2)))),X1))))),a1),inverse(sF1)))) = inverse(multiply(inverse(inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))))),inverse(inverse(inverse(inverse(inverse(X2))))))),
    inference(backward_demodulation,[],[f7968,f13544]) ).

fof(f13664,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))) = multiply(inverse(X0),multiply(X0,inverse(multiply(inverse(inverse(inverse(X1))),inverse(inverse(inverse(X2))))))),
    inference(backward_demodulation,[],[f1424,f13550]) ).

fof(f13675,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),X1)),X2),inverse(multiply(inverse(inverse(X3)),X2)))) = multiply(X3,inverse(multiply(inverse(inverse(inverse(X1))),inverse(inverse(inverse(X0)))))),
    inference(backward_demodulation,[],[f7676,f13550]) ).

fof(f13754,plain,
    ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,inverse(multiply(inverse(inverse(inverse(X2))),inverse(inverse(inverse(multiply(multiply(inverse(sF3),X3),inverse(multiply(b1,X3))))))))),
    inference(backward_demodulation,[],[f6201,f13550]) ).

fof(f13763,plain,
    ! [X2,X3,X0,X1,X4,X5] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(X3),a1),inverse(sF1)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,inverse(multiply(inverse(inverse(inverse(X2))),inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5))))))))),
    inference(backward_demodulation,[],[f6198,f13550]) ).

fof(f13771,plain,
    ! [X0] : inverse(multiply(sF5,inverse(multiply(inverse(X0),b2)))) = inverse(multiply(inverse(inverse(inverse(b2))),inverse(inverse(inverse(inverse(X0)))))),
    inference(backward_demodulation,[],[f8607,f13550]) ).

fof(f13791,plain,
    ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(X3),a1),inverse(sF1)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,inverse(multiply(inverse(inverse(inverse(X2))),inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(X3),a1),inverse(sF1))))))))),
    inference(forward_demodulation,[],[f13763,f303]) ).

fof(f13797,plain,
    ! [X2,X0,X1] : multiply(X1,inverse(multiply(multiply(inverse(X2),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),a1),inverse(sF1))))),inverse(X0)))) = multiply(X1,inverse(multiply(inverse(inverse(inverse(X2))),inverse(inverse(multiply(b1,inverse(multiply(sF3,inverse(sF3))))))))),
    inference(forward_demodulation,[],[f13754,f2669]) ).

fof(f13830,plain,
    ! [X2,X3,X1,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5))),multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1))))) = multiply(inverse(X1),multiply(X1,inverse(multiply(inverse(inverse(inverse(X2))),inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(X3),a1),inverse(sF1)))))))))),
    inference(backward_demodulation,[],[f3871,f13791]) ).

fof(f13835,plain,
    ! [X2,X3,X1] : multiply(multiply(multiply(inverse(sF3),X3),inverse(multiply(b1,X3))),multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1))))) = multiply(inverse(X1),multiply(X1,inverse(multiply(inverse(inverse(inverse(X2))),inverse(inverse(multiply(b1,inverse(multiply(sF3,inverse(sF3)))))))))),
    inference(backward_demodulation,[],[f3559,f13797]) ).

fof(f13855,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(X3,multiply(X2,X1)))) = multiply(inverse(inverse(inverse(X2))),inverse(inverse(inverse(X3)))),
    inference(superposition,[],[f13408,f791]) ).

fof(f13939,plain,
    ! [X2,X0,X1] : multiply(multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X2),X0)),a1),inverse(sF1))))),inverse(X0)) = multiply(inverse(inverse(X1)),inverse(inverse(inverse(X2)))),
    inference(superposition,[],[f13408,f553]) ).

fof(f13951,plain,
    ! [X0,X1] : multiply(multiply(X0,inverse(X1)),inverse(multiply(sF7,inverse(sF7)))) = multiply(inverse(inverse(X0)),inverse(inverse(inverse(X1)))),
    inference(superposition,[],[f13408,f10763]) ).

fof(f14004,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))),X0)),a1),inverse(sF1))))),inverse(X0)) = multiply(inverse(inverse(X1)),inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X3),X2)),X4),inverse(multiply(X3,X4))))))),
    inference(superposition,[],[f13408,f683]) ).

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

fof(f14035,plain,
    ! [X0] : multiply(multiply(X0,c3),inverse(sF8)) = multiply(inverse(inverse(X0)),inverse(inverse(inverse(sF7)))),
    inference(superposition,[],[f13408,f21]) ).

fof(f14043,plain,
    ! [X0,X1] : multiply(multiply(X1,inverse(sF1)),multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))) = multiply(inverse(inverse(X1)),inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1))))),
    inference(superposition,[],[f13408,f544]) ).

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

fof(f14158,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(X2)))),a1),inverse(sF1))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(X0,X1),inverse(multiply(X2,X1)))),a1),inverse(sF1)))),
    inference(superposition,[],[f646,f13408]) ).

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

fof(f14224,plain,
    ! [X2,X1] : inverse(multiply(X1,inverse(multiply(sF3,inverse(sF3))))) = multiply(multiply(multiply(inverse(sF3),X2),inverse(multiply(b1,X2))),multiply(b1,multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(X1)))),a1),inverse(sF1)))))),
    inference(backward_demodulation,[],[f10048,f14158]) ).

fof(f14252,plain,
    ! [X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),X1)),a1),inverse(sF1)))) = multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1))),inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),X1)),a1))))),
    inference(backward_demodulation,[],[f2880,f14043]) ).

fof(f14321,plain,
    ! [X2,X0,X1] : multiply(multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))),X0)),a1),inverse(sF1))))),inverse(X0)) = multiply(inverse(inverse(X1)),inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1))))))),
    inference(forward_demodulation,[],[f14004,f303]) ).

fof(f14468,plain,
    ! [X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(X0,inverse(X1))),a1),inverse(sF1)))) = multiply(inverse(inverse(X0)),inverse(inverse(inverse(X1)))),
    inference(forward_demodulation,[],[f13951,f10958]) ).

fof(f14783,plain,
    ! [X1,X6,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X4),X1)),X5),inverse(multiply(X4,X5))),multiply(a1,inverse(multiply(multiply(inverse(X6),a1),inverse(sF1))))) = multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),X1)),a1))),inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),X6)),a1))))),
    inference(backward_demodulation,[],[f680,f14252]) ).

fof(f14795,plain,
    ! [X2,X3,X1,X4,X5] : inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(multiply(multiply(inverse(multiply(inverse(X3),X4)),X5),inverse(multiply(X3,X5))),X2)))) = inverse(multiply(inverse(inverse(inverse(X1))),inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(X4),a1),inverse(sF1)))))))),
    inference(backward_demodulation,[],[f8971,f14321]) ).

fof(f14797,plain,
    ! [X0,X1] : inverse(inverse(X1)) = multiply(X1,multiply(inverse(inverse(X0)),inverse(inverse(inverse(X0))))),
    inference(backward_demodulation,[],[f11197,f14468]) ).

fof(f14799,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(X0,inverse(X1)))),X3),inverse(multiply(X1,X3))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(inverse(inverse(X2)),inverse(inverse(inverse(X2)))),X4)),a1),inverse(sF1))))) = X4,
    inference(backward_demodulation,[],[f11604,f14468]) ).

fof(f14801,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(X1,inverse(X1)))),X3),inverse(multiply(X0,X3))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(inverse(inverse(X2)),inverse(inverse(inverse(X2)))),X4)),a1),inverse(sF1))))) = X4,
    inference(backward_demodulation,[],[f12428,f14468]) ).

fof(f14803,plain,
    ! [X0] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),inverse(inverse(inverse(X0))))),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(inverse(inverse(inverse(inverse(a1))))),a1),inverse(sF1))),
    inference(backward_demodulation,[],[f13336,f14468]) ).

fof(f14814,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(X1,inverse(X1)))),a1),inverse(sF1))) = multiply(inverse(inverse(inverse(a1))),inverse(inverse(inverse(X0)))),
    inference(backward_demodulation,[],[f11695,f14468]) ).

fof(f14820,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(X2)))),a1),inverse(sF1))))) = multiply(inverse(inverse(multiply(X0,X1))),inverse(inverse(inverse(multiply(X2,X1))))),
    inference(backward_demodulation,[],[f14158,f14468]) ).

fof(f14836,plain,
    ! [X0,X1] : inverse(multiply(inverse(inverse(inverse(X1))),inverse(inverse(inverse(inverse(inverse(X0))))))) = multiply(X0,multiply(inverse(inverse(a1)),inverse(inverse(inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))))),
    inference(backward_demodulation,[],[f13387,f14468]) ).

fof(f14841,plain,
    ! [X2,X0,X1] : multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(inverse(multiply(multiply(X0,X2),inverse(multiply(inverse(inverse(inverse(X1))),X2))))),a1),inverse(sF1))))) = multiply(inverse(inverse(a1)),inverse(inverse(inverse(multiply(multiply(X0,a1),inverse(sF1)))))),
    inference(backward_demodulation,[],[f4636,f14468]) ).

fof(f14857,plain,
    ! [X0,X1] : inverse(multiply(sF3,inverse(multiply(inverse(inverse(X1)),b1)))) = multiply(X1,multiply(inverse(inverse(b1)),inverse(inverse(inverse(multiply(X0,inverse(X0))))))),
    inference(backward_demodulation,[],[f11262,f14468]) ).

fof(f14863,plain,
    ! [X0] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(X0)))),a1),inverse(sF1))))) = multiply(inverse(inverse(sF7)),inverse(inverse(inverse(sF7)))),
    inference(backward_demodulation,[],[f10938,f14468]) ).

fof(f14888,plain,
    ! [X2,X3,X1] : multiply(inverse(X1),multiply(X1,inverse(multiply(inverse(inverse(inverse(X2))),inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(X3),a1),inverse(sF1)))))))))) = multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),X3)),a1))),inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),X2)),a1))))),
    inference(backward_demodulation,[],[f13830,f14783]) ).

fof(f14895,plain,
    ! [X2,X0,X7] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))))),X7)),a1),inverse(sF1)))) = multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),multiply(inverse(inverse(X0)),X2))),a1))),inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),X7)),a1))))),
    inference(backward_demodulation,[],[f720,f14783]) ).

fof(f14896,plain,
    ! [X2,X0,X4] : multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),multiply(inverse(X2),multiply(X2,X0)))),a1))),inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),multiply(X0,X4))),a1))))) = X4,
    inference(backward_demodulation,[],[f3861,f14783]) ).

fof(f14897,plain,
    ! [X2,X0,X4] : multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),multiply(multiply(inverse(multiply(inverse(X2),multiply(X2,multiply(a1,X0)))),a1),inverse(sF1)))),a1))),inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),multiply(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))),X4))),a1))))) = X4,
    inference(backward_demodulation,[],[f4443,f14783]) ).

fof(f14903,plain,
    ! [X0] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(X0)))),a1),inverse(sF1))))) = multiply(multiply(sF7,c3),inverse(sF8)),
    inference(forward_demodulation,[],[f14863,f14035]) ).

fof(f14917,plain,
    ! [X0] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(X0)))),a1),inverse(sF1))))) = inverse(multiply(multiply(inverse(inverse(inverse(inverse(inverse(a1))))),a1),inverse(sF1))),
    inference(forward_demodulation,[],[f14803,f646]) ).

fof(f14919,plain,
    ! [X2,X1,X4] : multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),multiply(X1,inverse(X1)))),a1))),inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),multiply(multiply(inverse(inverse(X2)),inverse(inverse(inverse(X2)))),X4))),a1))))) = X4,
    inference(forward_demodulation,[],[f14801,f14783]) ).

fof(f14921,plain,
    ! [X0] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(X0)))),a1),inverse(sF1))))) = multiply(sF8,inverse(sF8)),
    inference(forward_demodulation,[],[f14903,f21]) ).

fof(f14922,plain,
    ! [X1] : inverse(inverse(X1)) = multiply(X1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(inverse(a1))))),a1),inverse(sF1)))),
    inference(backward_demodulation,[],[f13271,f14917]) ).

fof(f14923,plain,
    ! [X0] : multiply(sF7,inverse(sF7)) = multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(X0)))),a1),inverse(sF1))))),
    inference(forward_demodulation,[],[f14921,f10763]) ).

fof(f14924,plain,
    multiply(sF7,inverse(sF7)) = inverse(multiply(multiply(inverse(inverse(inverse(inverse(inverse(a1))))),a1),inverse(sF1))),
    inference(backward_demodulation,[],[f14917,f14923]) ).

fof(f14925,plain,
    ! [X1] : inverse(inverse(X1)) = multiply(X1,multiply(sF7,inverse(sF7))),
    inference(backward_demodulation,[],[f14922,f14924]) ).

fof(f14933,plain,
    ! [X0,X1] : inverse(inverse(inverse(X1))) = multiply(inverse(X0),multiply(X0,inverse(X1))),
    inference(backward_demodulation,[],[f10902,f14925]) ).

fof(f14935,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X0)),multiply(inverse(X0),multiply(X1,inverse(X2)))) = multiply(inverse(inverse(X1)),inverse(inverse(inverse(X2)))),
    inference(backward_demodulation,[],[f10908,f14925]) ).

fof(f14938,plain,
    ! [X0,X1] : inverse(inverse(inverse(inverse(X0)))) = multiply(inverse(X1),multiply(X1,inverse(inverse(X0)))),
    inference(backward_demodulation,[],[f10925,f14925]) ).

fof(f14940,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X0)),multiply(inverse(X0),multiply(X1,inverse(inverse(X2))))) = multiply(inverse(inverse(X1)),inverse(inverse(inverse(inverse(X2))))),
    inference(backward_demodulation,[],[f10929,f14925]) ).

fof(f14966,plain,
    ! [X3,X0,X1,X4] : multiply(inverse(inverse(inverse(inverse(X0)))),inverse(inverse(inverse(inverse(inverse(X1)))))) = multiply(inverse(inverse(multiply(X0,X3))),multiply(inverse(X4),multiply(X4,inverse(multiply(X1,X3))))),
    inference(backward_demodulation,[],[f14144,f14940]) ).

fof(f14967,plain,
    ! [X0,X1] : inverse(inverse(inverse(inverse(X1)))) = multiply(inverse(inverse(X1)),multiply(X0,inverse(X0))),
    inference(backward_demodulation,[],[f11201,f14938]) ).

fof(f14973,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X3),multiply(X3,multiply(multiply(X0,X1),inverse(multiply(X2,X1))))) = multiply(inverse(inverse(inverse(inverse(X0)))),inverse(inverse(inverse(inverse(inverse(X2)))))),
    inference(backward_demodulation,[],[f14202,f14938]) ).

fof(f14979,plain,
    ! [X2,X3,X1,X4] : multiply(inverse(inverse(X2)),multiply(inverse(X2),multiply(X3,multiply(X4,inverse(X4))))) = multiply(inverse(inverse(X3)),multiply(inverse(inverse(X1)),inverse(inverse(inverse(X1))))),
    inference(backward_demodulation,[],[f12433,f14935]) ).

fof(f15009,plain,
    ! [X2,X0] : inverse(inverse(inverse(X2))) = multiply(inverse(X2),multiply(X0,inverse(X0))),
    inference(backward_demodulation,[],[f11178,f14933]) ).

fof(f15020,plain,
    ! [X2,X3,X1,X4] : multiply(multiply(multiply(inverse(inverse(inverse(inverse(X1)))),X3),inverse(multiply(X1,X3))),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(inverse(inverse(X2)),inverse(inverse(inverse(X2)))),X4)),a1),inverse(sF1))))) = X4,
    inference(backward_demodulation,[],[f14799,f14933]) ).

fof(f15037,plain,
    ! [X2,X1] : multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))) = inverse(inverse(inverse(multiply(inverse(inverse(inverse(X1))),inverse(inverse(inverse(X2))))))),
    inference(backward_demodulation,[],[f13664,f14933]) ).

fof(f15039,plain,
    ! [X2,X3] : multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),X3)),a1))),inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),X2)),a1))))) = inverse(inverse(inverse(multiply(inverse(inverse(inverse(X2))),inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(X3),a1),inverse(sF1)))))))))),
    inference(backward_demodulation,[],[f14888,f14933]) ).

fof(f15040,plain,
    ! [X2,X3] : multiply(multiply(multiply(inverse(sF3),X3),inverse(multiply(b1,X3))),multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1))))) = inverse(inverse(inverse(multiply(inverse(inverse(inverse(X2))),inverse(inverse(multiply(b1,inverse(multiply(sF3,inverse(sF3)))))))))),
    inference(backward_demodulation,[],[f13835,f14933]) ).

fof(f15042,plain,
    ! [X3,X0,X4] : multiply(X4,multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1))))) = inverse(inverse(inverse(multiply(multiply(X0,X3),inverse(multiply(X4,X3)))))),
    inference(backward_demodulation,[],[f4434,f14933]) ).

fof(f15043,plain,
    ! [X2,X0] : multiply(multiply(inverse(multiply(inverse(X2),multiply(X2,multiply(a1,X0)))),a1),inverse(sF1)) = multiply(inverse(inverse(a1)),inverse(inverse(inverse(multiply(multiply(X0,a1),inverse(sF1)))))),
    inference(backward_demodulation,[],[f5013,f14933]) ).

fof(f15048,plain,
    ! [X1] : multiply(inverse(inverse(a1)),inverse(inverse(inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))) = X1,
    inference(backward_demodulation,[],[f899,f14933]) ).

fof(f15109,plain,
    ! [X3,X0,X1] : multiply(inverse(inverse(inverse(inverse(X0)))),inverse(inverse(inverse(inverse(inverse(X1)))))) = multiply(inverse(inverse(multiply(X0,X3))),inverse(inverse(inverse(multiply(X1,X3))))),
    inference(forward_demodulation,[],[f14966,f14933]) ).

fof(f15119,plain,
    ! [X2,X4] : multiply(inverse(inverse(multiply(inverse(inverse(inverse(inverse(inverse(a1))))),a1))),inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(a1)),multiply(multiply(inverse(inverse(X2)),inverse(inverse(inverse(X2)))),X4))),a1))))) = X4,
    inference(backward_demodulation,[],[f14919,f14967]) ).

fof(f15150,plain,
    ! [X2,X3,X4] : inverse(inverse(inverse(inverse(X3)))) = multiply(inverse(inverse(X2)),multiply(inverse(X2),multiply(X3,multiply(X4,inverse(X4))))),
    inference(forward_demodulation,[],[f14979,f14967]) ).

fof(f15247,plain,
    ! [X0,X1] : multiply(X0,X1) = inverse(multiply(inverse(inverse(inverse(X1))),inverse(inverse(inverse(inverse(inverse(X0))))))),
    inference(backward_demodulation,[],[f14836,f15048]) ).

fof(f15259,plain,
    ! [X2,X0,X4] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(multiply(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))),X4)))),inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(X2,multiply(a1,X0)))),a1),inverse(sF1))),a1),inverse(sF1)))))))))) = X4,
    inference(backward_demodulation,[],[f14897,f15039]) ).

fof(f15260,plain,
    ! [X2,X0,X4] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(multiply(X0,X4)))),inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(X2,X0))),a1),inverse(sF1)))))))))) = X4,
    inference(backward_demodulation,[],[f14896,f15039]) ).

fof(f15265,plain,
    ! [X2,X0,X7] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))))),X7)),a1),inverse(sF1)))) = inverse(inverse(inverse(multiply(inverse(inverse(inverse(X7))),inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),X2)),a1),inverse(sF1)))))))))),
    inference(backward_demodulation,[],[f14895,f15039]) ).

fof(f15302,plain,
    ! [X0] : inverse(multiply(multiply(inverse(inverse(inverse(inverse(X0)))),a1),inverse(sF1))) = multiply(inverse(inverse(inverse(a1))),inverse(inverse(inverse(X0)))),
    inference(backward_demodulation,[],[f14814,f15009]) ).

fof(f15319,plain,
    ! [X3,X0,X4] : inverse(inverse(inverse(inverse(X0)))) = multiply(inverse(inverse(inverse(X3))),multiply(inverse(X4),multiply(X4,multiply(X3,X0)))),
    inference(backward_demodulation,[],[f12051,f15150]) ).

fof(f15338,plain,
    ! [X2,X3,X0,X1] : multiply(X2,inverse(multiply(multiply(inverse(X1),X3),inverse(multiply(inverse(inverse(X0)),X3))))) = multiply(X2,multiply(X0,X1)),
    inference(backward_demodulation,[],[f13566,f15247]) ).

fof(f15352,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))) = multiply(a1,inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(inverse(inverse(inverse(inverse(X2)))),X1))))),a1),inverse(sF1)))),
    inference(backward_demodulation,[],[f13622,f15247]) ).

fof(f15358,plain,
    ! [X2,X0,X7] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))))),X7)),a1),inverse(sF1)))) = inverse(inverse(inverse(multiply(inverse(inverse(inverse(X7))),inverse(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1))))))))))),
    inference(forward_demodulation,[],[f15265,f646]) ).

fof(f15363,plain,
    ! [X0,X4] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(multiply(X0,X4)))),inverse(inverse(X0)))))) = X4,
    inference(forward_demodulation,[],[f15260,f824]) ).

fof(f15364,plain,
    ! [X2,X0,X4] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(multiply(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))),X4)))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X2),multiply(X2,multiply(a1,X0)))),a1))),inverse(inverse(inverse(sF1)))))))))) = X4,
    inference(forward_demodulation,[],[f15259,f14468]) ).

fof(f15374,plain,
    ! [X2,X1] : inverse(multiply(X1,inverse(multiply(sF3,inverse(sF3))))) = multiply(multiply(multiply(inverse(sF3),X2),inverse(multiply(b1,X2))),multiply(b1,multiply(a1,multiply(inverse(inverse(inverse(a1))),inverse(inverse(inverse(X1))))))),
    inference(backward_demodulation,[],[f14224,f15302]) ).

fof(f15376,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(multiply(X0,X1))),inverse(inverse(inverse(multiply(X2,X1))))) = multiply(X0,multiply(a1,multiply(inverse(inverse(inverse(a1))),inverse(inverse(inverse(X2)))))),
    inference(backward_demodulation,[],[f14820,f15302]) ).

fof(f15403,plain,
    ! [X2,X3,X4,X5] : multiply(inverse(X3),multiply(X3,multiply(X4,multiply(inverse(X5),multiply(X5,X2))))) = multiply(inverse(inverse(X4)),inverse(inverse(inverse(inverse(X2))))),
    inference(backward_demodulation,[],[f1182,f15319]) ).

fof(f15409,plain,
    ! [X0,X1,X4] : multiply(inverse(inverse(X0)),X1) = inverse(inverse(inverse(inverse(inverse(multiply(multiply(inverse(X1),X4),inverse(multiply(X0,X4)))))))),
    inference(backward_demodulation,[],[f1503,f15319]) ).

fof(f15411,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X3),multiply(X3,multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2))))) = inverse(inverse(inverse(inverse(multiply(X0,X2))))),
    inference(backward_demodulation,[],[f1124,f15319]) ).

fof(f15440,plain,
    ! [X2,X3,X0] : multiply(inverse(X2),multiply(X2,multiply(X3,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),a1),inverse(sF1)))))) = multiply(inverse(inverse(X3)),multiply(inverse(a1),X0)),
    inference(backward_demodulation,[],[f7600,f15338]) ).

fof(f15461,plain,
    ! [X2,X0] : inverse(inverse(inverse(inverse(multiply(X0,X2))))) = multiply(inverse(inverse(inverse(inverse(X0)))),inverse(inverse(inverse(inverse(X2))))),
    inference(backward_demodulation,[],[f15411,f15403]) ).

fof(f15468,plain,
    ! [X3,X0,X1] : multiply(inverse(inverse(multiply(X0,X3))),inverse(inverse(inverse(multiply(X1,X3))))) = inverse(inverse(inverse(inverse(multiply(X0,inverse(X1)))))),
    inference(backward_demodulation,[],[f15109,f15461]) ).

fof(f15469,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X3),multiply(X3,multiply(multiply(X0,X1),inverse(multiply(X2,X1))))) = inverse(inverse(inverse(inverse(multiply(X0,inverse(X2)))))),
    inference(backward_demodulation,[],[f14973,f15461]) ).

fof(f15477,plain,
    ! [X2,X0] : multiply(X0,multiply(a1,multiply(inverse(inverse(inverse(a1))),inverse(inverse(inverse(X2)))))) = inverse(inverse(inverse(inverse(multiply(X0,inverse(X2)))))),
    inference(backward_demodulation,[],[f15376,f15468]) ).

fof(f15486,plain,
    ! [X2,X4] : inverse(inverse(inverse(inverse(multiply(inverse(inverse(inverse(inverse(inverse(a1))))),inverse(inverse(multiply(inverse(inverse(a1)),multiply(multiply(inverse(inverse(X2)),inverse(inverse(inverse(X2)))),X4))))))))) = X4,
    inference(backward_demodulation,[],[f15119,f15468]) ).

fof(f15525,plain,
    ! [X2,X1] : inverse(multiply(X1,inverse(multiply(sF3,inverse(sF3))))) = multiply(multiply(multiply(inverse(sF3),X2),inverse(multiply(b1,X2))),inverse(inverse(inverse(inverse(multiply(b1,inverse(X1))))))),
    inference(backward_demodulation,[],[f15374,f15477]) ).

fof(f15557,plain,
    ! [X2,X0] : inverse(inverse(X0)) = multiply(X0,multiply(X2,inverse(X2))),
    inference(superposition,[],[f11888,f14797]) ).

fof(f15558,plain,
    ! [X0,X1] : inverse(inverse(X0)) = multiply(inverse(X1),multiply(X1,X0)),
    inference(superposition,[],[f11546,f14797]) ).

fof(f15635,plain,
    multiply(inverse(sF5),sF6) = inverse(inverse(a2)),
    inference(superposition,[],[f12012,f14797]) ).

fof(f15742,plain,
    ! [X1] : multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(X1))),a1),inverse(sF1)))) = X1,
    inference(backward_demodulation,[],[f824,f15558]) ).

fof(f15785,plain,
    ! [X2,X3,X0] : multiply(a1,inverse(multiply(multiply(inverse(multiply(X3,X0)),a1),inverse(sF1)))) = inverse(multiply(multiply(inverse(inverse(inverse(X0))),X2),inverse(multiply(X3,X2)))),
    inference(backward_demodulation,[],[f8112,f15558]) ).

fof(f15817,plain,
    ! [X2,X3,X1] : multiply(inverse(inverse(inverse(X2))),inverse(inverse(inverse(X3)))) = multiply(inverse(inverse(X1)),inverse(multiply(X3,multiply(X2,X1)))),
    inference(backward_demodulation,[],[f13855,f15558]) ).

fof(f15862,plain,
    ! [X3,X0] : multiply(inverse(inverse(X3)),multiply(inverse(a1),X0)) = inverse(inverse(multiply(X3,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))),a1),inverse(sF1)))))),
    inference(backward_demodulation,[],[f15440,f15558]) ).

fof(f15874,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X2)),multiply(inverse(inverse(X0)),X1)) = inverse(inverse(multiply(X2,multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1)))))))),
    inference(backward_demodulation,[],[f773,f15558]) ).

fof(f15882,plain,
    ! [X2,X0] : multiply(inverse(inverse(X0)),X2) = inverse(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1))))))),
    inference(backward_demodulation,[],[f546,f15558]) ).

fof(f15908,plain,
    ! [X2,X0,X1] : inverse(inverse(multiply(multiply(X0,X1),inverse(multiply(X2,X1))))) = inverse(inverse(inverse(inverse(multiply(X0,inverse(X2)))))),
    inference(backward_demodulation,[],[f15469,f15558]) ).

fof(f15911,plain,
    ! [X2] : inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))))) = X2,
    inference(backward_demodulation,[],[f542,f15558]) ).

fof(f15912,plain,
    ! [X1] : multiply(multiply(inverse(sF3),X1),inverse(multiply(b1,X1))) = inverse(inverse(multiply(a1,inverse(multiply(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),a1),inverse(sF1)))))),
    inference(backward_demodulation,[],[f2793,f15558]) ).

fof(f15936,plain,
    ! [X2,X3,X0] : multiply(X2,multiply(X3,inverse(X3))) = multiply(X0,multiply(multiply(multiply(inverse(inverse(inverse(multiply(a1,X0)))),a1),inverse(sF1)),X2)),
    inference(backward_demodulation,[],[f11792,f15558]) ).

fof(f15941,plain,
    ! [X0] : multiply(inverse(inverse(a1)),inverse(inverse(inverse(multiply(multiply(X0,a1),inverse(sF1)))))) = multiply(multiply(inverse(inverse(inverse(multiply(a1,X0)))),a1),inverse(sF1)),
    inference(backward_demodulation,[],[f15043,f15558]) ).

fof(f15943,plain,
    ! [X0,X4] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(multiply(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))),X4)))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(a1,X0)))),a1))),inverse(inverse(inverse(sF1)))))))))) = X4,
    inference(backward_demodulation,[],[f15364,f15558]) ).

fof(f15945,plain,
    ! [X0] : b1 = inverse(inverse(multiply(b1,inverse(multiply(X0,inverse(X0)))))),
    inference(backward_demodulation,[],[f11261,f15558]) ).

fof(f16031,plain,
    ! [X2,X3,X1] : multiply(inverse(inverse(X2)),multiply(inverse(X2),multiply(X3,X1))) = multiply(inverse(inverse(X3)),inverse(inverse(X1))),
    inference(backward_demodulation,[],[f798,f15558]) ).

fof(f16038,plain,
    ! [X2,X1] : multiply(inverse(inverse(X1)),inverse(inverse(inverse(X2)))) = inverse(inverse(multiply(X1,inverse(X2)))),
    inference(backward_demodulation,[],[f14935,f15558]) ).

fof(f16184,plain,
    ! [X2,X3,X1,X4] : multiply(multiply(multiply(inverse(inverse(inverse(inverse(X1)))),X3),inverse(multiply(X1,X3))),multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(multiply(X2,inverse(X2)))),X4)),a1),inverse(sF1))))) = X4,
    inference(backward_demodulation,[],[f15020,f16038]) ).

fof(f16185,plain,
    ! [X2,X4] : inverse(inverse(inverse(inverse(multiply(inverse(inverse(inverse(inverse(inverse(a1))))),inverse(inverse(multiply(inverse(inverse(a1)),multiply(inverse(inverse(multiply(X2,inverse(X2)))),X4))))))))) = X4,
    inference(backward_demodulation,[],[f15486,f16038]) ).

fof(f16217,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),X1)),X2),inverse(multiply(inverse(inverse(X3)),X2)))) = multiply(X3,inverse(inverse(inverse(multiply(inverse(X1),inverse(X0)))))),
    inference(backward_demodulation,[],[f13675,f16038]) ).

fof(f16249,plain,
    ! [X2,X1] : multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(X1),inverse(X2))))))),
    inference(backward_demodulation,[],[f15037,f16038]) ).

fof(f16261,plain,
    ! [X3,X0,X1] : multiply(multiply(X1,X3),inverse(multiply(X0,X3))) = inverse(inverse(multiply(X1,inverse(X0)))),
    inference(backward_demodulation,[],[f13408,f16038]) ).

fof(f16269,plain,
    ! [X2,X0,X1] : multiply(multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X2),X0)),a1),inverse(sF1))))),inverse(X0)) = inverse(inverse(multiply(X1,inverse(X2)))),
    inference(backward_demodulation,[],[f13939,f16038]) ).

fof(f16275,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(inverse(X2)),inverse(inverse(inverse(multiply(X0,X3))))) = multiply(multiply(X2,inverse(multiply(X1,X3))),inverse(inverse(inverse(multiply(X0,inverse(X1)))))),
    inference(backward_demodulation,[],[f14017,f16038]) ).

fof(f16278,plain,
    ! [X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(X0,inverse(X1))),a1),inverse(sF1)))) = inverse(inverse(multiply(X0,inverse(X1)))),
    inference(backward_demodulation,[],[f14468,f16038]) ).

fof(f16289,plain,
    ! [X0] : inverse(multiply(sF5,inverse(multiply(inverse(X0),b2)))) = inverse(inverse(inverse(multiply(inverse(b2),inverse(inverse(X0)))))),
    inference(backward_demodulation,[],[f13771,f16038]) ).

fof(f16299,plain,
    ! [X2,X0] : inverse(inverse(inverse(inverse(multiply(X0,X2))))) = inverse(inverse(multiply(inverse(inverse(X0)),inverse(inverse(X2))))),
    inference(backward_demodulation,[],[f15461,f16038]) ).

fof(f16302,plain,
    ! [X0,X1] : multiply(X0,X1) = inverse(inverse(inverse(multiply(inverse(X1),inverse(inverse(inverse(X0))))))),
    inference(backward_demodulation,[],[f15247,f16038]) ).

fof(f16335,plain,
    ! [X2,X0,X1] : multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(inverse(multiply(multiply(X0,X2),inverse(multiply(inverse(inverse(inverse(X1))),X2))))),a1),inverse(sF1))))) = inverse(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))))),
    inference(backward_demodulation,[],[f14841,f16038]) ).

fof(f16345,plain,
    ! [X0,X1] : inverse(multiply(sF3,inverse(multiply(inverse(inverse(X1)),b1)))) = multiply(X1,inverse(inverse(multiply(b1,inverse(multiply(X0,inverse(X0))))))),
    inference(backward_demodulation,[],[f14857,f16038]) ).

fof(f16361,plain,
    ! [X1] : multiply(multiply(inverse(sF3),X1),inverse(multiply(b1,X1))) = inverse(inverse(multiply(inverse(sF3),inverse(b1)))),
    inference(backward_demodulation,[],[f13374,f16038]) ).

fof(f16368,plain,
    multiply(a1,inverse(multiply(multiply(inverse(b2),a1),inverse(sF1)))) = inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))),
    inference(backward_demodulation,[],[f13369,f16038]) ).

fof(f16377,plain,
    ! [X0] : multiply(multiply(X0,b3),inverse(sF7)) = inverse(inverse(multiply(X0,inverse(a3)))),
    inference(backward_demodulation,[],[f13368,f16038]) ).

fof(f16378,plain,
    ! [X0] : multiply(multiply(X0,c3),inverse(sF9)) = inverse(inverse(multiply(X0,inverse(b3)))),
    inference(backward_demodulation,[],[f13365,f16038]) ).

fof(f16388,plain,
    ! [X3,X1] : inverse(inverse(multiply(X3,X1))) = multiply(inverse(inverse(X3)),inverse(inverse(X1))),
    inference(forward_demodulation,[],[f16031,f15558]) ).

fof(f16490,plain,
    ! [X2,X3] : multiply(multiply(multiply(inverse(sF3),X3),inverse(multiply(b1,X3))),multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1))))) = inverse(inverse(inverse(multiply(inverse(inverse(inverse(X2))),b1)))),
    inference(backward_demodulation,[],[f15040,f15945]) ).

fof(f16494,plain,
    ! [X0,X4] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(multiply(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))),X4)))),inverse(inverse(inverse(inverse(multiply(multiply(inverse(inverse(inverse(multiply(a1,X0)))),a1),inverse(sF1)))))))))) = X4,
    inference(forward_demodulation,[],[f15943,f16038]) ).

fof(f16495,plain,
    ! [X0] : inverse(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))))) = multiply(multiply(inverse(inverse(inverse(multiply(a1,X0)))),a1),inverse(sF1)),
    inference(forward_demodulation,[],[f15941,f16038]) ).

fof(f16497,plain,
    ! [X2,X0] : inverse(inverse(X2)) = multiply(X0,multiply(multiply(multiply(inverse(inverse(inverse(multiply(a1,X0)))),a1),inverse(sF1)),X2)),
    inference(forward_demodulation,[],[f15936,f15557]) ).

fof(f16511,plain,
    ! [X2,X3,X1,X4,X5] : inverse(multiply(inverse(inverse(inverse(X1))),X4)) = inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(multiply(multiply(inverse(multiply(inverse(X3),X4)),X5),inverse(multiply(X3,X5))),X2)))),
    inference(backward_demodulation,[],[f14795,f15911]) ).

fof(f16524,plain,
    ! [X2,X0] : multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))) = multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X0),inverse(inverse(inverse(inverse(inverse(X2)))))))))),a1),inverse(sF1)))),
    inference(backward_demodulation,[],[f15352,f15908]) ).

fof(f16530,plain,
    ! [X0] : inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1))))),a1),inverse(sF1))) = multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(multiply(X0,inverse(inverse(inverse(inverse(a1))))))))),a1),inverse(sF1)))),
    inference(backward_demodulation,[],[f4637,f15908]) ).

fof(f16539,plain,
    ! [X0,X1] : multiply(inverse(inverse(X0)),X1) = inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X1),inverse(X0))))))))),
    inference(backward_demodulation,[],[f15409,f15908]) ).

fof(f16540,plain,
    ! [X0,X4] : multiply(X4,multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1))))) = inverse(inverse(inverse(inverse(inverse(multiply(X0,inverse(X4))))))),
    inference(backward_demodulation,[],[f15042,f15908]) ).

fof(f16556,plain,
    ! [X2,X0,X7] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF1)))))),X7)),a1),inverse(sF1)))) = inverse(inverse(inverse(multiply(inverse(inverse(inverse(X7))),multiply(inverse(inverse(X0)),X2))))),
    inference(backward_demodulation,[],[f15358,f15882]) ).

fof(f16587,plain,
    ! [X2,X3,X1] : multiply(inverse(inverse(X1)),inverse(multiply(X3,multiply(X2,X1)))) = inverse(inverse(multiply(inverse(X2),inverse(X3)))),
    inference(forward_demodulation,[],[f15817,f16038]) ).

fof(f16746,plain,
    ! [X0] : multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1)) = inverse(inverse(multiply(inverse(multiply(inverse(b3),X0)),inverse(b3)))),
    inference(backward_demodulation,[],[f4977,f16378]) ).

fof(f16771,plain,
    ! [X0] : multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1)) = inverse(inverse(multiply(inverse(multiply(inverse(a3),X0)),inverse(a3)))),
    inference(backward_demodulation,[],[f2913,f16377]) ).

fof(f16790,plain,
    ! [X0] : inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))) = multiply(multiply(multiply(inverse(sF5),X0),inverse(multiply(b2,X0))),inverse(multiply(sF5,inverse(multiply(inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))),b2))))),
    inference(backward_demodulation,[],[f1878,f16368]) ).

fof(f16800,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),inverse(multiply(b2,multiply(sF5,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X0,X2)))))))),multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))),X3)),a1),inverse(sF1))))) = X3,
    inference(backward_demodulation,[],[f4309,f16368]) ).

fof(f16837,plain,
    ! [X2,X0,X1] : inverse(multiply(multiply(inverse(X1),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),a1),inverse(sF1))))),inverse(X0))) = inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(inverse(inverse(multiply(inverse(sF3),inverse(b1)))),X2)))),
    inference(backward_demodulation,[],[f8968,f16361]) ).

fof(f16843,plain,
    ! [X0] : inverse(inverse(X0)) = multiply(X0,inverse(multiply(sF3,inverse(multiply(inverse(inverse(multiply(inverse(sF3),inverse(b1)))),b1))))),
    inference(backward_demodulation,[],[f13437,f16361]) ).

fof(f16846,plain,
    ! [X1] : inverse(multiply(X1,inverse(multiply(sF3,inverse(sF3))))) = multiply(inverse(inverse(multiply(inverse(sF3),inverse(b1)))),inverse(inverse(inverse(inverse(multiply(b1,inverse(X1))))))),
    inference(backward_demodulation,[],[f15525,f16361]) ).

fof(f16848,plain,
    inverse(inverse(multiply(inverse(sF3),inverse(b1)))) = inverse(inverse(multiply(a1,inverse(multiply(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),a1),inverse(sF1)))))),
    inference(backward_demodulation,[],[f15912,f16361]) ).

fof(f16858,plain,
    ! [X1] : multiply(X1,b1) = inverse(multiply(sF3,inverse(multiply(inverse(inverse(X1)),b1)))),
    inference(forward_demodulation,[],[f16345,f15945]) ).

fof(f16862,plain,
    ! [X0,X1] : inverse(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))))) = multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(inverse(inverse(inverse(multiply(X0,inverse(inverse(inverse(inverse(X1))))))))),a1),inverse(sF1))))),
    inference(forward_demodulation,[],[f16335,f15908]) ).

fof(f16887,plain,
    ! [X0,X4] : inverse(inverse(inverse(inverse(inverse(multiply(inverse(multiply(X0,X4)),X0)))))) = X4,
    inference(backward_demodulation,[],[f15363,f16299]) ).

fof(f16923,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(X2,inverse(multiply(X1,X3))),inverse(inverse(inverse(multiply(X0,inverse(X1)))))) = inverse(inverse(multiply(X2,inverse(multiply(X0,X3))))),
    inference(forward_demodulation,[],[f16275,f16038]) ).

fof(f16963,plain,
    ! [X0] : multiply(multiply(X0,a1),inverse(sF1)) = inverse(inverse(multiply(X0,inverse(inverse(a1))))),
    inference(backward_demodulation,[],[f9933,f16261]) ).

fof(f16965,plain,
    ! [X0] : multiply(multiply(X0,b2),inverse(sF5)) = inverse(inverse(multiply(X0,inverse(inverse(b2))))),
    inference(backward_demodulation,[],[f9935,f16261]) ).

fof(f16995,plain,
    ! [X0,X1] : multiply(multiply(inverse(multiply(inverse(inverse(a1)),multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))))),a1),inverse(sF1)) = inverse(inverse(multiply(inverse(X1),inverse(X0)))),
    inference(backward_demodulation,[],[f8231,f16261]) ).

fof(f17000,plain,
    ! [X2,X3,X0] : multiply(b1,inverse(multiply(sF3,inverse(sF3)))) = multiply(multiply(multiply(inverse(X0),X3),inverse(multiply(X2,X3))),inverse(multiply(sF3,inverse(multiply(inverse(inverse(inverse(multiply(inverse(X0),inverse(X2))))),b1))))),
    inference(backward_demodulation,[],[f9132,f16261]) ).

fof(f17047,plain,
    ! [X3,X0] : multiply(a1,inverse(multiply(multiply(inverse(multiply(X3,X0)),a1),inverse(sF1)))) = inverse(inverse(inverse(multiply(inverse(inverse(inverse(X0))),inverse(X3))))),
    inference(backward_demodulation,[],[f15785,f16261]) ).

fof(f17129,plain,
    ! [X0,X1] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(X1)),X0)),a1),inverse(sF1)))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(X0),inverse(X1))))))),
    inference(backward_demodulation,[],[f646,f16249]) ).

fof(f17133,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X2)),multiply(inverse(inverse(X0)),X1)) = inverse(inverse(multiply(X2,inverse(inverse(inverse(inverse(inverse(multiply(inverse(X1),inverse(X0)))))))))),
    inference(backward_demodulation,[],[f15874,f16249]) ).

fof(f17145,plain,
    ! [X2,X0,X1] : inverse(inverse(multiply(X1,inverse(X2)))) = multiply(inverse(inverse(inverse(inverse(inverse(multiply(inverse(multiply(inverse(X2),X0)),inverse(X1))))))),inverse(X0)),
    inference(backward_demodulation,[],[f16269,f16249]) ).

fof(f17205,plain,
    ! [X3,X0,X1] : multiply(X3,inverse(inverse(inverse(multiply(inverse(X1),inverse(X0)))))) = inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X0)),X1)),inverse(inverse(inverse(X3))))))),
    inference(forward_demodulation,[],[f16217,f16261]) ).

fof(f17228,plain,
    ! [X2,X4] : inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(inverse(inverse(a1))),multiply(inverse(inverse(a1)),multiply(inverse(inverse(multiply(X2,inverse(X2)))),X4))))))))) = X4,
    inference(forward_demodulation,[],[f16185,f16299]) ).

fof(f17229,plain,
    ! [X2,X3,X1,X4] : inverse(inverse(inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(X2,inverse(X2)))),X4)),inverse(multiply(multiply(inverse(inverse(inverse(inverse(X1)))),X3),inverse(multiply(X1,X3)))))))))) = X4,
    inference(forward_demodulation,[],[f16184,f16249]) ).

fof(f17306,plain,
    ! [X2,X3] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(X2))),b1)))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(sF3),X3),inverse(multiply(b1,X3)))))))))),
    inference(forward_demodulation,[],[f16490,f16249]) ).

fof(f17310,plain,
    ! [X0,X4] : multiply(inverse(multiply(multiply(inverse(inverse(inverse(multiply(a1,X0)))),a1),inverse(sF1))),inverse(inverse(multiply(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))),X4)))) = X4,
    inference(forward_demodulation,[],[f16494,f16302]) ).

fof(f17319,plain,
    ! [X2,X0] : inverse(inverse(X2)) = multiply(X0,multiply(inverse(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))))),X2)),
    inference(forward_demodulation,[],[f16497,f16495]) ).

fof(f17336,plain,
    ! [X3,X1,X4,X5] : inverse(multiply(inverse(inverse(inverse(X1))),X4)) = inverse(inverse(inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(X3),X4)),X5),inverse(multiply(X3,X5)))))))),
    inference(forward_demodulation,[],[f16511,f16261]) ).

fof(f17354,plain,
    ! [X0] : inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1))))),a1),inverse(sF1))) = inverse(multiply(X0,inverse(inverse(inverse(inverse(a1)))))),
    inference(forward_demodulation,[],[f16530,f15742]) ).

fof(f17360,plain,
    ! [X2,X0] : multiply(X2,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF1))))) = inverse(multiply(inverse(X0),inverse(inverse(inverse(inverse(inverse(X2))))))),
    inference(forward_demodulation,[],[f16524,f15742]) ).

fof(f17375,plain,
    ! [X2,X0,X7] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(X7))),multiply(inverse(inverse(X0)),X2))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X2),inverse(X0)))))))),X7)),a1),inverse(sF1)))),
    inference(forward_demodulation,[],[f16556,f16540]) ).

fof(f17471,plain,
    ! [X0] : multiply(multiply(inverse(multiply(inverse(inverse(b2)),X0)),b2),inverse(sF5)) = inverse(inverse(multiply(inverse(multiply(inverse(b3),X0)),inverse(b3)))),
    inference(backward_demodulation,[],[f4765,f16746]) ).

fof(f17489,plain,
    ! [X0] : inverse(inverse(multiply(inverse(multiply(inverse(b3),X0)),inverse(b3)))) = inverse(inverse(multiply(inverse(multiply(inverse(a3),X0)),inverse(a3)))),
    inference(backward_demodulation,[],[f16746,f16771]) ).

fof(f17514,plain,
    ! [X2,X3,X0,X1] : inverse(inverse(inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))),X3)),inverse(multiply(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),inverse(multiply(b2,multiply(sF5,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X0,X2))))))))))))))) = X3,
    inference(forward_demodulation,[],[f16800,f16540]) ).

fof(f17524,plain,
    ! [X0] : inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))) = multiply(multiply(multiply(inverse(sF5),X0),inverse(multiply(b2,X0))),inverse(inverse(inverse(multiply(inverse(b2),inverse(inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))))))))),
    inference(forward_demodulation,[],[f16790,f16289]) ).

fof(f17528,plain,
    ! [X1] : inverse(multiply(X1,inverse(multiply(sF3,inverse(sF3))))) = inverse(inverse(multiply(multiply(inverse(sF3),inverse(b1)),inverse(inverse(multiply(b1,inverse(X1))))))),
    inference(forward_demodulation,[],[f16846,f16388]) ).

fof(f17535,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(X1),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),a1),inverse(sF1))))),inverse(X0))) = inverse(inverse(inverse(multiply(inverse(X1),inverse(inverse(inverse(multiply(inverse(sF3),inverse(b1))))))))),
    inference(forward_demodulation,[],[f16837,f16261]) ).

fof(f17554,plain,
    ! [X0] : inverse(inverse(X0)) = multiply(X0,multiply(multiply(inverse(sF3),inverse(b1)),b1)),
    inference(backward_demodulation,[],[f16843,f16858]) ).

fof(f17561,plain,
    ! [X0,X1] : inverse(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(inverse(inverse(inverse(multiply(X0,inverse(inverse(inverse(inverse(X1))))))))),inverse(X1))))))),
    inference(forward_demodulation,[],[f16862,f16540]) ).

fof(f17643,plain,
    ! [X0,X1] : inverse(inverse(multiply(X0,inverse(X1)))) = inverse(inverse(inverse(multiply(inverse(inverse(inverse(inverse(X1)))),inverse(X0))))),
    inference(backward_demodulation,[],[f16278,f17047]) ).

fof(f17683,plain,
    ! [X2,X3,X0] : multiply(b1,inverse(multiply(sF3,inverse(sF3)))) = multiply(multiply(multiply(inverse(X0),X3),inverse(multiply(X2,X3))),multiply(inverse(multiply(inverse(X0),inverse(X2))),b1)),
    inference(forward_demodulation,[],[f17000,f16858]) ).

fof(f17688,plain,
    ! [X0,X1] : inverse(inverse(multiply(inverse(X1),inverse(X0)))) = inverse(inverse(multiply(inverse(multiply(inverse(a3),multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))))),inverse(a3)))),
    inference(forward_demodulation,[],[f16995,f16771]) ).

fof(f17741,plain,
    ! [X0,X1] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(X0))),inverse(inverse(inverse(X1))))))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(X0),inverse(X1))))))),
    inference(forward_demodulation,[],[f17129,f17047]) ).

fof(f17765,plain,
    ! [X3,X0,X1] : multiply(X3,inverse(inverse(inverse(multiply(inverse(X1),inverse(X0)))))) = multiply(X3,multiply(inverse(inverse(X0)),X1)),
    inference(forward_demodulation,[],[f17205,f16302]) ).

fof(f17777,plain,
    ! [X2,X4] : inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(inverse(multiply(X2,inverse(X2)))),X4))))))))) = X4,
    inference(forward_demodulation,[],[f17228,f15558]) ).

fof(f17778,plain,
    ! [X2,X1,X4] : inverse(inverse(inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(X2,inverse(X2)))),X4)),inverse(inverse(inverse(multiply(inverse(inverse(inverse(inverse(X1)))),inverse(X1))))))))))) = X4,
    inference(forward_demodulation,[],[f17229,f16261]) ).

fof(f17795,plain,
    ! [X2] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(X2))),b1)))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(X2),inverse(inverse(inverse(multiply(inverse(sF3),inverse(b1))))))))))),
    inference(forward_demodulation,[],[f17306,f16261]) ).

fof(f17797,plain,
    ! [X0,X4] : multiply(inverse(inverse(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1))))))),inverse(inverse(multiply(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))),X4)))) = X4,
    inference(forward_demodulation,[],[f17310,f16495]) ).

fof(f17805,plain,
    ! [X3,X1,X4] : inverse(multiply(inverse(inverse(inverse(X1))),X4)) = inverse(inverse(inverse(multiply(inverse(X1),inverse(inverse(inverse(multiply(inverse(multiply(inverse(X3),X4)),inverse(X3))))))))),
    inference(forward_demodulation,[],[f17336,f16261]) ).

fof(f17819,plain,
    ! [X3,X0] : multiply(inverse(inverse(X3)),multiply(inverse(a1),X0)) = inverse(inverse(multiply(X3,inverse(multiply(inverse(X0),inverse(inverse(inverse(inverse(a1))))))))),
    inference(backward_demodulation,[],[f15862,f17354]) ).

fof(f17825,plain,
    ! [X2,X0] : inverse(multiply(inverse(X0),inverse(inverse(inverse(inverse(inverse(X2))))))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(X0),inverse(X2))))))),
    inference(forward_demodulation,[],[f17360,f16540]) ).

fof(f17836,plain,
    ! [X2,X0,X7] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(X7))),multiply(inverse(inverse(X0)),X2))))) = inverse(inverse(inverse(multiply(inverse(inverse(inverse(X7))),inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X2),inverse(X0))))))))))))),
    inference(forward_demodulation,[],[f17375,f17047]) ).

fof(f17875,plain,
    ! [X0] : inverse(inverse(multiply(inverse(multiply(inverse(b3),X0)),inverse(b3)))) = inverse(inverse(multiply(inverse(multiply(inverse(inverse(b2)),X0)),inverse(inverse(b2))))),
    inference(forward_demodulation,[],[f17471,f16965]) ).

fof(f17911,plain,
    ! [X3,X0,X1] : inverse(inverse(inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))),X3)),inverse(multiply(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),inverse(multiply(b2,multiply(sF5,inverse(inverse(inverse(multiply(inverse(X1),inverse(X0)))))))))))))))) = X3,
    inference(forward_demodulation,[],[f17514,f16261]) ).

fof(f17919,plain,
    ! [X0] : inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))) = multiply(multiply(multiply(inverse(sF5),X0),inverse(multiply(b2,X0))),multiply(inverse(multiply(inverse(sF5),inverse(b2))),b2)),
    inference(forward_demodulation,[],[f17524,f16302]) ).

fof(f17926,plain,
    ! [X0,X1] : inverse(multiply(multiply(inverse(X1),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),a1),inverse(sF1))))),inverse(X0))) = multiply(multiply(inverse(sF3),inverse(b1)),X1),
    inference(forward_demodulation,[],[f17535,f16302]) ).

fof(f17988,plain,
    ! [X0,X1] : inverse(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))))) = inverse(inverse(inverse(inverse(multiply(X1,inverse(multiply(X0,inverse(inverse(inverse(inverse(X1))))))))))),
    inference(backward_demodulation,[],[f17561,f17643]) ).

fof(f18013,plain,
    ! [X2,X0] : multiply(b1,inverse(multiply(sF3,inverse(sF3)))) = multiply(inverse(inverse(multiply(inverse(X0),inverse(X2)))),multiply(inverse(multiply(inverse(X0),inverse(X2))),b1)),
    inference(forward_demodulation,[],[f17683,f16261]) ).

fof(f18017,plain,
    ! [X0,X1] : inverse(inverse(multiply(inverse(X1),inverse(X0)))) = inverse(inverse(multiply(inverse(multiply(inverse(a3),inverse(inverse(inverse(inverse(inverse(multiply(inverse(X1),inverse(X0))))))))),inverse(a3)))),
    inference(forward_demodulation,[],[f17688,f16540]) ).

fof(f18052,plain,
    ! [X0,X1] : multiply(X1,inverse(inverse(X0))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(X0),inverse(X1))))))),
    inference(forward_demodulation,[],[f17741,f16302]) ).

fof(f18073,plain,
    ! [X2,X1,X4] : inverse(inverse(multiply(multiply(inverse(inverse(inverse(inverse(X1)))),inverse(X1)),multiply(inverse(inverse(multiply(X2,inverse(X2)))),X4)))) = X4,
    inference(forward_demodulation,[],[f17778,f16302]) ).

fof(f18082,plain,
    ! [X2] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(X2))),b1)))) = inverse(inverse(multiply(multiply(inverse(sF3),inverse(b1)),X2))),
    inference(forward_demodulation,[],[f17795,f16302]) ).

fof(f18084,plain,
    ! [X0,X4] : inverse(inverse(multiply(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1))))),multiply(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))),X4)))) = X4,
    inference(forward_demodulation,[],[f17797,f16388]) ).

fof(f18090,plain,
    ! [X3,X1,X4] : inverse(multiply(inverse(inverse(inverse(X1))),X4)) = multiply(multiply(inverse(multiply(inverse(X3),X4)),inverse(X3)),X1),
    inference(forward_demodulation,[],[f17805,f16302]) ).

fof(f18099,plain,
    ! [X2,X0,X7] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(X7))),multiply(inverse(inverse(X0)),X2))))) = multiply(inverse(inverse(inverse(inverse(multiply(inverse(X2),inverse(X0)))))),inverse(inverse(X7))),
    inference(forward_demodulation,[],[f17836,f16302]) ).

fof(f18113,plain,
    ! [X0] : inverse(inverse(multiply(inverse(multiply(inverse(a3),X0)),inverse(a3)))) = inverse(inverse(multiply(inverse(multiply(inverse(inverse(b2)),X0)),inverse(inverse(b2))))),
    inference(forward_demodulation,[],[f17875,f17489]) ).

fof(f18127,plain,
    ! [X3,X0,X1] : inverse(inverse(inverse(inverse(inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))),X3)),inverse(multiply(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),inverse(multiply(b2,multiply(sF5,multiply(inverse(inverse(X0)),X1)))))))))))) = X3,
    inference(forward_demodulation,[],[f17911,f17765]) ).

fof(f18134,plain,
    inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))) = multiply(inverse(inverse(multiply(inverse(sF5),inverse(b2)))),multiply(inverse(multiply(inverse(sF5),inverse(b2))),b2)),
    inference(forward_demodulation,[],[f17919,f16261]) ).

fof(f18138,plain,
    ! [X0,X1] : inverse(multiply(inverse(inverse(inverse(inverse(inverse(multiply(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)),inverse(inverse(X1)))))))),inverse(X0))) = multiply(multiply(inverse(sF3),inverse(b1)),X1),
    inference(forward_demodulation,[],[f17926,f16540]) ).

fof(f18185,plain,
    inverse(inverse(b1)) = multiply(b1,inverse(multiply(sF3,inverse(sF3)))),
    inference(forward_demodulation,[],[f18013,f15558]) ).

fof(f18188,plain,
    ! [X0,X1] : inverse(inverse(multiply(inverse(X1),inverse(X0)))) = inverse(inverse(multiply(inverse(inverse(inverse(inverse(inverse(multiply(inverse(a3),inverse(multiply(inverse(X1),inverse(X0))))))))),inverse(a3)))),
    inference(forward_demodulation,[],[f18017,f17825]) ).

fof(f18209,plain,
    ! [X0,X1] : multiply(inverse(inverse(X0)),X1) = inverse(inverse(multiply(X0,inverse(inverse(X1))))),
    inference(backward_demodulation,[],[f16539,f18052]) ).

fof(f18213,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X2)),multiply(inverse(inverse(X0)),X1)) = inverse(inverse(multiply(X2,multiply(X0,inverse(inverse(X1)))))),
    inference(backward_demodulation,[],[f17133,f18052]) ).

fof(f18229,plain,
    ! [X2,X0,X1] : inverse(inverse(multiply(X1,inverse(X2)))) = multiply(multiply(X1,inverse(inverse(multiply(inverse(X2),X0)))),inverse(X0)),
    inference(backward_demodulation,[],[f17145,f18052]) ).

fof(f18264,plain,
    ! [X1] : inverse(multiply(X1,inverse(multiply(sF3,inverse(sF3))))) = inverse(inverse(inverse(multiply(inverse(inverse(inverse(inverse(inverse(multiply(b1,inverse(X1))))))),b1)))),
    inference(backward_demodulation,[],[f17528,f18082]) ).

fof(f18270,plain,
    ! [X4] : inverse(inverse(inverse(inverse(X4)))) = X4,
    inference(forward_demodulation,[],[f18084,f15558]) ).

fof(f18285,plain,
    ! [X2,X0,X7] : inverse(inverse(inverse(multiply(inverse(inverse(inverse(X7))),multiply(inverse(inverse(X0)),X2))))) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),inverse(X0)))),X7))),
    inference(forward_demodulation,[],[f18099,f16388]) ).

fof(f18303,plain,
    ! [X3,X0,X1] : multiply(multiply(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),inverse(multiply(b2,multiply(sF5,multiply(inverse(inverse(X0)),X1))))),inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))),X3)))) = X3,
    inference(forward_demodulation,[],[f18127,f18052]) ).

fof(f18310,plain,
    inverse(inverse(b2)) = inverse(inverse(inverse(multiply(inverse(sF5),inverse(b2))))),
    inference(forward_demodulation,[],[f18134,f15558]) ).

fof(f18313,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF3),inverse(b1)),X1) = inverse(multiply(multiply(inverse(X1),inverse(inverse(multiply(multiply(b1,inverse(multiply(sF3,inverse(sF3)))),X0)))),inverse(X0))),
    inference(forward_demodulation,[],[f18138,f18052]) ).

fof(f18362,plain,
    inverse(inverse(multiply(inverse(sF3),inverse(b1)))) = inverse(inverse(multiply(a1,inverse(multiply(multiply(inverse(inverse(b1)),a1),inverse(sF1)))))),
    inference(backward_demodulation,[],[f16848,f18185]) ).

fof(f18374,plain,
    ! [X0,X1] : inverse(inverse(multiply(inverse(X1),inverse(X0)))) = inverse(inverse(multiply(multiply(multiply(inverse(X1),inverse(X0)),inverse(inverse(a3))),inverse(a3)))),
    inference(forward_demodulation,[],[f18188,f18052]) ).

fof(f18406,plain,
    ! [X0] : multiply(inverse(inverse(X0)),a1) = multiply(multiply(X0,a1),inverse(sF1)),
    inference(backward_demodulation,[],[f16963,f18209]) ).

fof(f18418,plain,
    ! [X0] : inverse(inverse(multiply(inverse(multiply(inverse(a3),X0)),inverse(a3)))) = multiply(inverse(inverse(inverse(multiply(inverse(inverse(b2)),X0)))),b2),
    inference(backward_demodulation,[],[f18113,f18209]) ).

fof(f18433,plain,
    ! [X2,X1,X4] : inverse(inverse(multiply(multiply(X1,inverse(X1)),multiply(inverse(inverse(multiply(X2,inverse(X2)))),X4)))) = X4,
    inference(backward_demodulation,[],[f18073,f18270]) ).

fof(f18435,plain,
    ! [X0,X1] : inverse(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))))) = inverse(inverse(inverse(inverse(multiply(X1,inverse(multiply(X0,X1))))))),
    inference(backward_demodulation,[],[f17988,f18270]) ).

fof(f18436,plain,
    ! [X0,X1] : inverse(inverse(multiply(X0,inverse(X1)))) = inverse(inverse(inverse(multiply(X1,inverse(X0))))),
    inference(backward_demodulation,[],[f17643,f18270]) ).

fof(f18440,plain,
    ! [X2,X4] : inverse(inverse(inverse(inverse(multiply(inverse(inverse(multiply(X2,inverse(X2)))),X4))))) = X4,
    inference(backward_demodulation,[],[f17777,f18270]) ).

fof(f18445,plain,
    ! [X0,X4] : inverse(multiply(inverse(multiply(X0,X4)),X0)) = X4,
    inference(backward_demodulation,[],[f16887,f18270]) ).

fof(f18446,plain,
    ! [X0,X4] : multiply(X4,multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1))))) = inverse(multiply(X0,inverse(X4))),
    inference(backward_demodulation,[],[f16540,f18270]) ).

fof(f18447,plain,
    ! [X0,X1] : multiply(X1,inverse(inverse(X0))) = inverse(multiply(inverse(X0),inverse(X1))),
    inference(backward_demodulation,[],[f18052,f18270]) ).

fof(f18449,plain,
    ! [X1] : inverse(multiply(X1,inverse(multiply(sF3,inverse(sF3))))) = inverse(inverse(inverse(multiply(inverse(multiply(b1,inverse(X1))),b1)))),
    inference(backward_demodulation,[],[f18264,f18270]) ).

fof(f18465,plain,
    ! [X3,X0] : multiply(inverse(inverse(X3)),multiply(inverse(a1),X0)) = inverse(inverse(multiply(X3,inverse(multiply(inverse(X0),a1))))),
    inference(backward_demodulation,[],[f17819,f18270]) ).

fof(f18476,plain,
    ! [X2,X0,X7] : inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),inverse(X0)))),X7))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(X7),multiply(X0,inverse(inverse(X2))))))))),
    inference(forward_demodulation,[],[f18285,f18213]) ).

fof(f18489,plain,
    ! [X3,X0,X1] : multiply(multiply(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF1))))),inverse(multiply(b2,multiply(sF5,multiply(inverse(inverse(X0)),X1))))),inverse(inverse(multiply(inverse(inverse(b2)),X3)))) = X3,
    inference(backward_demodulation,[],[f18303,f18310]) ).

fof(f18493,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF3),inverse(b1)),X1) = inverse(multiply(multiply(inverse(X1),inverse(inverse(multiply(inverse(inverse(b1)),X0)))),inverse(X0))),
    inference(forward_demodulation,[],[f18313,f18185]) ).

fof(f18521,plain,
    inverse(b1) = inverse(inverse(multiply(inverse(sF3),inverse(b1)))),
    inference(forward_demodulation,[],[f18362,f15911]) ).

fof(f18537,plain,
    ! [X0] : multiply(multiply(inverse(multiply(inverse(inverse(a1)),X0)),a1),inverse(sF1)) = multiply(inverse(inverse(inverse(multiply(inverse(inverse(b2)),X0)))),b2),
    inference(backward_demodulation,[],[f16771,f18418]) ).

fof(f18565,plain,
    ! [X0] : multiply(multiply(inverse(inverse(inverse(multiply(a1,X0)))),a1),inverse(sF1)) = inverse(inverse(multiply(a1,inverse(multiply(inverse(inverse(X0)),a1))))),
    inference(backward_demodulation,[],[f16495,f18406]) ).

fof(f18569,plain,
    ! [X2,X0] : inverse(inverse(X2)) = multiply(X0,multiply(inverse(inverse(multiply(a1,inverse(multiply(inverse(inverse(X0)),a1))))),X2)),
    inference(backward_demodulation,[],[f17319,f18406]) ).

fof(f18607,plain,
    ! [X1] : multiply(a1,inverse(multiply(inverse(inverse(inverse(inverse(inverse(X1))))),a1))) = X1,
    inference(backward_demodulation,[],[f15742,f18406]) ).

fof(f18672,plain,
    ! [X2,X3,X1] : multiply(inverse(inverse(X1)),inverse(multiply(X3,multiply(X2,X1)))) = inverse(multiply(X3,inverse(inverse(X2)))),
    inference(backward_demodulation,[],[f16587,f18447]) ).

fof(f18678,plain,
    ! [X0,X1] : inverse(multiply(X0,inverse(inverse(X1)))) = inverse(inverse(multiply(multiply(multiply(inverse(X1),inverse(X0)),inverse(inverse(a3))),inverse(a3)))),
    inference(backward_demodulation,[],[f18374,f18447]) ).

fof(f18691,plain,
    ! [X0] : multiply(inverse(inverse(inverse(multiply(inverse(inverse(b2)),X0)))),b2) = inverse(multiply(a3,inverse(inverse(multiply(inverse(a3),X0))))),
    inference(backward_demodulation,[],[f18418,f18447]) ).

fof(f18713,plain,
    ! [X0,X4] : inverse(multiply(X0,inverse(X4))) = multiply(X4,multiply(a1,inverse(multiply(inverse(inverse(X0)),a1)))),
    inference(forward_demodulation,[],[f18446,f18406]) ).

fof(f18717,plain,
    ! [X1] : inverse(inverse(inverse(X1))) = inverse(multiply(X1,inverse(multiply(sF3,inverse(sF3))))),
    inference(backward_demodulation,[],[f18449,f18445]) ).

fof(f18721,plain,
    ! [X2,X4] : multiply(inverse(inverse(multiply(X2,inverse(X2)))),X4) = X4,
    inference(forward_demodulation,[],[f18440,f18270]) ).

fof(f18723,plain,
    ! [X2,X3,X0,X1] : inverse(inverse(multiply(X2,inverse(multiply(X0,X3))))) = multiply(multiply(X2,inverse(multiply(X1,X3))),inverse(inverse(multiply(X1,inverse(X0))))),
    inference(backward_demodulation,[],[f16923,f18436]) ).

fof(f18728,plain,
    ! [X0,X1] : inverse(inverse(multiply(a1,inverse(multiply(multiply(X0,a1),inverse(sF1)))))) = multiply(X1,inverse(multiply(X0,X1))),
    inference(forward_demodulation,[],[f18435,f18270]) ).

fof(f18735,plain,
    ! [X2,X0,X7] : inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),inverse(X0)))),X7))) = inverse(multiply(inverse(X7),multiply(X0,inverse(inverse(X2))))),
    inference(forward_demodulation,[],[f18476,f18270]) ).

fof(f18748,plain,
    ! [X3,X0,X1] : multiply(multiply(multiply(X0,multiply(a1,inverse(multiply(inverse(inverse(inverse(X1))),a1)))),inverse(multiply(b2,multiply(sF5,multiply(inverse(inverse(X0)),X1))))),inverse(inverse(multiply(inverse(inverse(b2)),X3)))) = X3,
    inference(forward_demodulation,[],[f18489,f18406]) ).

fof(f18751,plain,
    ! [X1] : inverse(inverse(inverse(multiply(inverse(X1),inverse(inverse(b1)))))) = multiply(multiply(inverse(sF3),inverse(b1)),X1),
    inference(forward_demodulation,[],[f18493,f18229]) ).

fof(f18772,plain,
    inverse(b1) = inverse(multiply(b1,inverse(inverse(sF3)))),
    inference(forward_demodulation,[],[f18521,f18447]) ).

fof(f18798,plain,
    ! [X0] : multiply(inverse(inverse(inverse(multiply(inverse(inverse(b2)),X0)))),b2) = multiply(inverse(inverse(inverse(multiply(inverse(inverse(a1)),X0)))),a1),
    inference(forward_demodulation,[],[f18537,f18406]) ).

fof(f18826,plain,
    ! [X1] : multiply(a1,inverse(multiply(inverse(X1),a1))) = X1,
    inference(forward_demodulation,[],[f18607,f18270]) ).

fof(f18850,plain,
    ! [X2,X0] : inverse(inverse(X2)) = multiply(X0,multiply(multiply(inverse(inverse(a1)),multiply(inverse(a1),inverse(X0))),X2)),
    inference(forward_demodulation,[],[f18569,f18465]) ).

fof(f18854,plain,
    ! [X0] : multiply(inverse(inverse(a1)),multiply(inverse(a1),inverse(X0))) = multiply(multiply(inverse(inverse(inverse(multiply(a1,X0)))),a1),inverse(sF1)),
    inference(forward_demodulation,[],[f18565,f18465]) ).

fof(f18937,plain,
    ! [X1,X4] : inverse(inverse(multiply(multiply(X1,inverse(X1)),X4))) = X4,
    inference(backward_demodulation,[],[f18433,f18721]) ).

fof(f18940,plain,
    ! [X0,X1] : multiply(X1,inverse(multiply(X0,X1))) = inverse(inverse(multiply(a1,inverse(multiply(inverse(inverse(X0)),a1))))),
    inference(forward_demodulation,[],[f18728,f18406]) ).

fof(f18947,plain,
    ! [X2,X0,X7] : inverse(multiply(inverse(X7),multiply(X0,inverse(inverse(X2))))) = inverse(inverse(multiply(inverse(multiply(X0,inverse(inverse(X2)))),X7))),
    inference(forward_demodulation,[],[f18735,f18447]) ).

fof(f18961,plain,
    ! [X3,X0,X1] : multiply(multiply(inverse(multiply(inverse(X1),inverse(X0))),inverse(multiply(b2,multiply(sF5,multiply(inverse(inverse(X0)),X1))))),inverse(inverse(multiply(inverse(inverse(b2)),X3)))) = X3,
    inference(forward_demodulation,[],[f18748,f18713]) ).

fof(f18964,plain,
    ! [X1] : multiply(multiply(inverse(sF3),inverse(b1)),X1) = inverse(inverse(multiply(inverse(b1),inverse(inverse(X1))))),
    inference(forward_demodulation,[],[f18751,f18436]) ).

fof(f19009,plain,
    ! [X0] : inverse(multiply(a3,inverse(inverse(multiply(inverse(a3),X0))))) = multiply(inverse(inverse(inverse(multiply(inverse(inverse(a1)),X0)))),a1),
    inference(forward_demodulation,[],[f18798,f18691]) ).

fof(f19031,plain,
    ! [X0,X4] : multiply(X4,inverse(X0)) = inverse(multiply(X0,inverse(X4))),
    inference(backward_demodulation,[],[f18713,f18826]) ).

fof(f19052,plain,
    ! [X2,X0] : inverse(inverse(X2)) = multiply(X0,multiply(inverse(inverse(inverse(X0))),X2)),
    inference(forward_demodulation,[],[f18850,f15558]) ).

fof(f19055,plain,
    ! [X0] : multiply(inverse(inverse(a1)),multiply(inverse(a1),inverse(X0))) = multiply(inverse(inverse(inverse(inverse(inverse(multiply(a1,X0)))))),a1),
    inference(forward_demodulation,[],[f18854,f18406]) ).

fof(f19111,plain,
    ! [X0,X1] : multiply(inverse(inverse(a1)),multiply(inverse(a1),inverse(X0))) = multiply(X1,inverse(multiply(X0,X1))),
    inference(forward_demodulation,[],[f18940,f18465]) ).

fof(f19128,plain,
    ! [X3,X0,X1] : multiply(multiply(multiply(X0,inverse(inverse(X1))),inverse(multiply(b2,multiply(sF5,multiply(inverse(inverse(X0)),X1))))),inverse(inverse(multiply(inverse(inverse(b2)),X3)))) = X3,
    inference(forward_demodulation,[],[f18961,f18447]) ).

fof(f19131,plain,
    ! [X1] : multiply(inverse(inverse(inverse(b1))),X1) = multiply(multiply(inverse(sF3),inverse(b1)),X1),
    inference(forward_demodulation,[],[f18964,f18209]) ).

fof(f19184,plain,
    ! [X2,X4] : multiply(inverse(multiply(X2,inverse(X2))),X4) = X4,
    inference(backward_demodulation,[],[f18721,f19031]) ).

fof(f19189,plain,
    ! [X3,X0,X1] : multiply(multiply(X1,X3),inverse(multiply(X0,X3))) = inverse(multiply(X0,inverse(X1))),
    inference(backward_demodulation,[],[f16261,f19031]) ).

fof(f19196,plain,
    ! [X2,X3,X0,X1] : inverse(inverse(multiply(X2,inverse(multiply(X0,X3))))) = multiply(multiply(X2,inverse(multiply(X1,X3))),inverse(multiply(X0,inverse(X1)))),
    inference(backward_demodulation,[],[f18723,f19031]) ).

fof(f19198,plain,
    ! [X0,X1] : multiply(inverse(inverse(X0)),X1) = inverse(multiply(inverse(X1),inverse(X0))),
    inference(backward_demodulation,[],[f18209,f19031]) ).

fof(f19199,plain,
    ! [X2,X3,X1] : multiply(inverse(X2),inverse(X3)) = multiply(inverse(inverse(X1)),inverse(multiply(X3,multiply(X2,X1)))),
    inference(backward_demodulation,[],[f18672,f19031]) ).

fof(f19202,plain,
    ! [X0,X1] : multiply(inverse(X1),inverse(X0)) = inverse(inverse(multiply(multiply(multiply(inverse(X1),inverse(X0)),inverse(inverse(a3))),inverse(a3)))),
    inference(backward_demodulation,[],[f18678,f19031]) ).

fof(f19205,plain,
    ! [X2,X0,X7] : inverse(multiply(inverse(X7),multiply(X0,inverse(inverse(X2))))) = inverse(inverse(multiply(multiply(inverse(X2),inverse(X0)),X7))),
    inference(backward_demodulation,[],[f18947,f19031]) ).

fof(f19225,plain,
    ! [X1] : inverse(inverse(inverse(X1))) = multiply(multiply(sF3,inverse(sF3)),inverse(X1)),
    inference(backward_demodulation,[],[f18717,f19031]) ).

fof(f19248,plain,
    inverse(b1) = multiply(inverse(sF3),inverse(b1)),
    inference(backward_demodulation,[],[f18772,f19031]) ).

fof(f19252,plain,
    ! [X0] : multiply(inverse(multiply(inverse(a3),X0)),inverse(a3)) = multiply(inverse(inverse(inverse(multiply(inverse(inverse(a1)),X0)))),a1),
    inference(backward_demodulation,[],[f19009,f19031]) ).

fof(f19300,plain,
    ! [X0] : multiply(inverse(multiply(a1,X0)),a1) = multiply(inverse(inverse(a1)),multiply(inverse(a1),inverse(X0))),
    inference(forward_demodulation,[],[f19055,f18270]) ).

fof(f19338,plain,
    ! [X0,X1] : inverse(inverse(inverse(X0))) = multiply(X1,inverse(multiply(X0,X1))),
    inference(forward_demodulation,[],[f19111,f15558]) ).

fof(f19352,plain,
    ! [X0] : inverse(inverse(X0)) = multiply(X0,multiply(inverse(inverse(inverse(b1))),b1)),
    inference(backward_demodulation,[],[f17554,f19131]) ).

fof(f19405,plain,
    ! [X1] : multiply(inverse(b1),X1) = multiply(inverse(inverse(inverse(b1))),X1),
    inference(backward_demodulation,[],[f19131,f19248]) ).

fof(f19434,plain,
    ! [X0,X1] : multiply(inverse(X1),inverse(X0)) = inverse(multiply(a3,inverse(multiply(multiply(inverse(X1),inverse(X0)),inverse(inverse(a3)))))),
    inference(forward_demodulation,[],[f19202,f19031]) ).

fof(f19435,plain,
    ! [X0,X1] : multiply(inverse(inverse(X0)),X1) = multiply(X0,inverse(inverse(X1))),
    inference(forward_demodulation,[],[f19198,f19031]) ).

fof(f19437,plain,
    ! [X2,X3,X0,X1] : inverse(inverse(multiply(X2,inverse(multiply(X0,X3))))) = multiply(multiply(X2,inverse(multiply(X1,X3))),multiply(X1,inverse(X0))),
    inference(forward_demodulation,[],[f19196,f19031]) ).

fof(f19444,plain,
    ! [X3,X0,X1] : multiply(multiply(X1,X3),inverse(multiply(X0,X3))) = multiply(X1,inverse(X0)),
    inference(forward_demodulation,[],[f19189,f19031]) ).

fof(f19448,plain,
    ! [X2,X4] : multiply(multiply(X2,inverse(X2)),X4) = X4,
    inference(forward_demodulation,[],[f19184,f19031]) ).

fof(f19475,plain,
    ! [X0] : inverse(inverse(inverse(X0))) = multiply(inverse(multiply(a1,X0)),a1),
    inference(forward_demodulation,[],[f19300,f15558]) ).

fof(f19561,plain,
    ! [X0] : inverse(inverse(X0)) = multiply(X0,multiply(inverse(b1),b1)),
    inference(backward_demodulation,[],[f19352,f19405]) ).

fof(f19582,plain,
    ! [X0,X1] : multiply(inverse(X1),inverse(X0)) = multiply(multiply(multiply(inverse(X1),inverse(X0)),inverse(inverse(a3))),inverse(a3)),
    inference(forward_demodulation,[],[f19434,f19031]) ).

fof(f19588,plain,
    ! [X0] : multiply(inverse(multiply(inverse(a3),X0)),inverse(a3)) = multiply(inverse(inverse(inverse(multiply(a1,inverse(inverse(X0)))))),a1),
    inference(backward_demodulation,[],[f19252,f19435]) ).

fof(f19594,plain,
    ! [X3,X0,X1] : multiply(multiply(multiply(X0,inverse(inverse(X1))),inverse(multiply(b2,multiply(sF5,multiply(inverse(inverse(X0)),X1))))),inverse(inverse(multiply(b2,inverse(inverse(X3)))))) = X3,
    inference(backward_demodulation,[],[f19128,f19435]) ).

fof(f19600,plain,
    ! [X2,X0] : inverse(inverse(X2)) = multiply(X0,multiply(inverse(X0),inverse(inverse(X2)))),
    inference(backward_demodulation,[],[f19052,f19435]) ).

fof(f19602,plain,
    ! [X3,X1,X4] : multiply(multiply(inverse(multiply(inverse(X3),X4)),inverse(X3)),X1) = inverse(multiply(inverse(X1),inverse(inverse(X4)))),
    inference(backward_demodulation,[],[f18090,f19435]) ).

fof(f19629,plain,
    ! [X2,X3,X1] : multiply(inverse(X2),inverse(X3)) = multiply(X1,inverse(inverse(inverse(multiply(X3,multiply(X2,X1)))))),
    inference(backward_demodulation,[],[f19199,f19435]) ).

fof(f19654,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(multiply(X0,X3),inverse(X2))) = multiply(multiply(X2,inverse(multiply(X1,X3))),multiply(X1,inverse(X0))),
    inference(forward_demodulation,[],[f19437,f19031]) ).

fof(f19660,plain,
    ! [X4] : inverse(inverse(X4)) = X4,
    inference(backward_demodulation,[],[f18937,f19448]) ).

fof(f19662,plain,
    ! [X1] : inverse(X1) = inverse(inverse(inverse(X1))),
    inference(backward_demodulation,[],[f19225,f19448]) ).

fof(f19744,plain,
    ! [X0] : inverse(inverse(X0)) = multiply(X0,sF3),
    inference(forward_demodulation,[],[f19561,f41]) ).

fof(f19780,plain,
    ! [X3,X1,X4] : multiply(multiply(inverse(multiply(inverse(X3),X4)),inverse(X3)),X1) = multiply(inverse(X4),inverse(inverse(X1))),
    inference(forward_demodulation,[],[f19602,f19031]) ).

fof(f19787,plain,
    ! [X3,X0,X1] : multiply(multiply(multiply(X0,inverse(inverse(X1))),inverse(multiply(b2,multiply(sF5,multiply(inverse(inverse(X0)),X1))))),inverse(multiply(inverse(X3),inverse(b2)))) = X3,
    inference(forward_demodulation,[],[f19594,f19031]) ).

fof(f19793,plain,
    ! [X0] : multiply(inverse(multiply(inverse(a3),X0)),inverse(a3)) = multiply(inverse(multiply(a1,inverse(inverse(X0)))),inverse(inverse(a1))),
    inference(forward_demodulation,[],[f19588,f19435]) ).

fof(f19799,plain,
    ! [X2,X3,X0,X1] : multiply(X2,inverse(multiply(X0,X3))) = multiply(multiply(X2,inverse(multiply(X1,X3))),multiply(X1,inverse(X0))),
    inference(forward_demodulation,[],[f19654,f19031]) ).

fof(f19804,plain,
    ! [X0,X1] : inverse(X0) = multiply(X1,inverse(multiply(X0,X1))),
    inference(backward_demodulation,[],[f19338,f19662]) ).

fof(f19805,plain,
    ! [X0] : inverse(X0) = multiply(inverse(multiply(a1,X0)),a1),
    inference(backward_demodulation,[],[f19475,f19662]) ).

fof(f19813,plain,
    ! [X2,X3,X1] : multiply(inverse(X2),inverse(X3)) = multiply(X1,inverse(multiply(X3,multiply(X2,X1)))),
    inference(backward_demodulation,[],[f19629,f19662]) ).

fof(f19833,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(X1,X0)) = X0,
    inference(backward_demodulation,[],[f15558,f19660]) ).

fof(f19837,plain,
    ! [X2,X0,X7] : inverse(inverse(multiply(multiply(inverse(X2),inverse(X0)),X7))) = inverse(multiply(inverse(X7),multiply(X0,X2))),
    inference(backward_demodulation,[],[f19205,f19660]) ).

fof(f19848,plain,
    ! [X2,X0] : multiply(X0,multiply(inverse(X0),X2)) = X2,
    inference(backward_demodulation,[],[f19600,f19660]) ).

fof(f19865,plain,
    a2 = multiply(inverse(sF5),sF6),
    inference(backward_demodulation,[],[f15635,f19660]) ).

fof(f19866,plain,
    ! [X0,X1] : multiply(inverse(X1),inverse(X0)) = multiply(multiply(multiply(inverse(X1),inverse(X0)),a3),inverse(a3)),
    inference(backward_demodulation,[],[f19582,f19660]) ).

fof(f19951,plain,
    ! [X0] : multiply(X0,sF3) = X0,
    inference(forward_demodulation,[],[f19744,f19660]) ).

fof(f19982,plain,
    ! [X3,X1,X4] : multiply(inverse(X4),X1) = multiply(multiply(inverse(multiply(inverse(X3),X4)),inverse(X3)),X1),
    inference(forward_demodulation,[],[f19780,f19660]) ).

fof(f19988,plain,
    ! [X3,X0,X1] : multiply(multiply(multiply(X0,inverse(inverse(X1))),inverse(multiply(b2,multiply(sF5,multiply(inverse(inverse(X0)),X1))))),multiply(b2,inverse(inverse(X3)))) = X3,
    inference(forward_demodulation,[],[f19787,f19031]) ).

fof(f19994,plain,
    ! [X0] : multiply(inverse(multiply(inverse(a3),X0)),inverse(a3)) = multiply(inverse(multiply(a1,inverse(inverse(X0)))),a1),
    inference(forward_demodulation,[],[f19793,f19660]) ).

fof(f20031,plain,
    ! [X2,X0,X7] : multiply(multiply(inverse(X2),inverse(X0)),X7) = inverse(multiply(inverse(X7),multiply(X0,X2))),
    inference(forward_demodulation,[],[f19837,f19660]) ).

fof(f20118,plain,
    ! [X3,X0,X1] : multiply(multiply(X0,inverse(inverse(X1))),inverse(multiply(inverse(X3),multiply(sF5,multiply(inverse(inverse(X0)),X1))))) = X3,
    inference(forward_demodulation,[],[f19988,f19799]) ).

fof(f20122,plain,
    ! [X0] : inverse(inverse(inverse(X0))) = multiply(inverse(multiply(inverse(a3),X0)),inverse(a3)),
    inference(forward_demodulation,[],[f19994,f19805]) ).

fof(f20141,plain,
    ! [X3,X1,X4] : multiply(inverse(X4),X1) = inverse(multiply(inverse(X1),multiply(X3,multiply(inverse(X3),X4)))),
    inference(backward_demodulation,[],[f19982,f20031]) ).

fof(f20146,plain,
    ! [X0,X1] : multiply(inverse(X1),inverse(X0)) = multiply(inverse(multiply(inverse(a3),multiply(X0,X1))),inverse(a3)),
    inference(backward_demodulation,[],[f19866,f20031]) ).

fof(f20202,plain,
    ! [X3,X0,X1] : multiply(multiply(X0,inverse(inverse(X1))),inverse(multiply(inverse(X3),multiply(sF5,multiply(X0,X1))))) = X3,
    inference(forward_demodulation,[],[f20118,f19660]) ).

fof(f20206,plain,
    ! [X0] : inverse(X0) = multiply(inverse(multiply(inverse(a3),X0)),inverse(a3)),
    inference(forward_demodulation,[],[f20122,f19660]) ).

fof(f20213,plain,
    ! [X1,X4] : inverse(multiply(inverse(X1),X4)) = multiply(inverse(X4),X1),
    inference(forward_demodulation,[],[f20141,f19848]) ).

fof(f20253,plain,
    ! [X3,X0,X1] : multiply(multiply(X0,X1),inverse(multiply(inverse(X3),multiply(sF5,multiply(X0,X1))))) = X3,
    inference(forward_demodulation,[],[f20202,f19660]) ).

fof(f20259,plain,
    ! [X0,X1] : inverse(multiply(X0,X1)) = multiply(inverse(X1),inverse(X0)),
    inference(backward_demodulation,[],[f20146,f20206]) ).

fof(f20293,plain,
    ! [X3] : multiply(inverse(sF5),inverse(inverse(X3))) = X3,
    inference(forward_demodulation,[],[f20253,f19813]) ).

fof(f20333,plain,
    ! [X3] : inverse(multiply(inverse(X3),sF5)) = X3,
    inference(forward_demodulation,[],[f20293,f20259]) ).

fof(f20344,plain,
    ! [X3] : multiply(inverse(sF5),X3) = X3,
    inference(forward_demodulation,[],[f20333,f20213]) ).

fof(f20348,plain,
    a2 = sF6,
    inference(backward_demodulation,[],[f19865,f20344]) ).

fof(f20350,plain,
    spl11_2,
    inference(avatar_split_clause,[],[f20348,f32]) ).

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

fof(f20385,plain,
    ! [X0,X1] : inverse(X1) = inverse(multiply(inverse(X0),multiply(X0,X1))),
    inference(forward_demodulation,[],[f20369,f20259]) ).

fof(f20391,plain,
    ! [X0,X1] : inverse(X1) = multiply(inverse(multiply(X0,X1)),X0),
    inference(forward_demodulation,[],[f20385,f20213]) ).

fof(f20399,plain,
    ! [X0] : sF3 = multiply(inverse(X0),X0),
    inference(superposition,[],[f19833,f19951]) ).

fof(f20417,plain,
    sF1 = sF3,
    inference(backward_demodulation,[],[f40,f20399]) ).

fof(f20432,plain,
    spl11_3,
    inference(avatar_split_clause,[],[f20417,f36]) ).

fof(f20587,plain,
    ! [X2,X0,X1] : multiply(X1,inverse(inverse(multiply(X2,X0)))) = multiply(multiply(X1,X2),inverse(inverse(X0))),
    inference(superposition,[],[f19444,f20391]) ).

fof(f20595,plain,
    ! [X2,X0,X1] : multiply(multiply(X1,X2),X0) = multiply(X1,inverse(inverse(multiply(X2,X0)))),
    inference(forward_demodulation,[],[f20587,f19660]) ).

fof(f20606,plain,
    ! [X2,X0,X1] : multiply(X1,multiply(X2,X0)) = multiply(multiply(X1,X2),X0),
    inference(forward_demodulation,[],[f20595,f19660]) ).

fof(f20796,plain,
    ! [X0] : multiply(sF7,X0) = multiply(a3,multiply(b3,X0)),
    inference(superposition,[],[f20606,f19]) ).

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

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

fof(f20859,plain,
    sF8 = sF10,
    inference(forward_demodulation,[],[f20855,f21]) ).

fof(f20862,plain,
    ( $false
    | spl11_1 ),
    inference(forward_subsumption_resolution,[],[f20859,f30]) ).

fof(f20863,plain,
    spl11_1,
    inference(avatar_contradiction_clause,[],[f20862]) ).

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

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

cnf(s3,plain,
    spl11_3,
    inference(sat_conversion,[],[f20432]) ).

cnf(s6,plain,
    spl11_1,
    inference(sat_conversion,[],[f20863]) ).

cnf(s7,plain,
    $false,
    inference(rat,[],[s1,s3,s2,s6]) ).

fof(f20864,plain,
    $false,
    inference(avatar_sat_refutation,[],[s7]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP057-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.39  % Computer : n005.cluster.edu
% 0.12/0.39  % Model    : x86_64 x86_64
% 0.12/0.39  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39  % Memory   : 8046.5625MB
% 0.12/0.39  % OS       : Linux 6.8.0-71-generic
% 0.12/0.39  % CPULimit : 300
% 0.12/0.39  % WCLimit  : 300
% 0.12/0.39  % DateTime : Sun Sep 27 09:17:02 UTC 2026
% 0.12/0.40  % CPUTime  : 
% 0.12/0.40  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.44  Running first-order theorem proving
% 0.12/0.44  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.22/2.95  % (3720359)Input is clausal, will run a generic CNF schedule.
% 13.22/2.95  % (3720380)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1292448175:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 13.22/2.95  % (3720385)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1783450131:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 13.22/2.95  % (3720383)lrs+10_1_sil=8000:sp=occurrence:random_seed=2698977727:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 13.22/2.95  % (3720378)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=2511953380:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 13.22/2.95  % (3720379)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=103624533:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 13.22/2.95  % (3720384)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=415465953:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 13.22/2.95  % (3720386)dis-21_1_sil=8000:lcm=predicate:random_seed=1416456453: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)
% 13.22/2.95  % (3720386)Refutation not found, incomplete strategy
% 13.22/2.95  % (3720386)------------------------------
% 13.22/2.95  % (3720386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.95  % (3720386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.95  % (3720386)CaDiCaL version: 2.1.3
% 13.22/2.95  % (3720386)Termination reason: Refutation not found, incomplete strategy
% 13.22/2.95  % (3720386)Time elapsed: 0.002 s
% 13.22/2.95  % (3720386)Peak memory usage: 88 MB
% 13.22/2.95  % (3720383)Instruction limit reached! 
% 13.22/2.95  % (3720383)------------------------------
% 13.22/2.95  % (3720383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.95  % (3720383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.95  % (3720383)CaDiCaL version: 2.1.3
% 13.22/2.95  % (3720383)Termination reason: Instruction limit
% 13.22/2.95  % (3720383)Termination phase: Saturation
% 13.22/2.95  % (3720383)Time elapsed: 0.072 s
% 13.22/2.95  % (3720383)Peak memory usage: 89 MB
% 13.22/2.95  % (3720383)Instructions burned: 107 (million)
% 13.22/2.95  % (3720385)Instruction limit reached! 
% 13.22/2.95  % (3720385)------------------------------
% 13.22/2.95  % (3720385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.95  % (3720385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.95  % (3720385)CaDiCaL version: 2.1.3
% 13.22/2.95  % (3720385)Termination reason: Instruction limit
% 13.22/2.95  % (3720385)Termination phase: Saturation
% 13.22/2.95  % (3720385)Time elapsed: 0.158 s
% 13.22/2.95  % (3720385)Peak memory usage: 89 MB
% 13.22/2.95  % (3720385)Instructions burned: 180 (million)
% 13.22/2.95  % (3720384)Instruction limit reached! 
% 13.22/2.95  % (3720384)------------------------------
% 13.22/2.95  % (3720384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.95  % (3720384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.95  % (3720384)CaDiCaL version: 2.1.3
% 13.22/2.95  % (3720384)Termination reason: Instruction limit
% 13.22/2.95  % (3720384)Termination phase: Saturation
% 13.22/2.95  % (3720384)Time elapsed: 0.112 s
% 13.22/2.95  % (3720384)Peak memory usage: 89 MB
% 13.22/2.95  % (3720384)Instructions burned: 114 (million)
% 13.22/2.95  % (3720397)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=2684410630:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 13.22/2.95  % (3720397)Refutation not found, incomplete strategy
% 13.22/2.95  % (3720397)------------------------------
% 13.22/2.95  % (3720397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.22/2.95  % (3720397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.22/2.95  % (3720397)CaDiCaL version: 2.1.3
% 13.22/2.95  % (3720397)Termination reason: Refutation not found, incomplete strategy
% 13.22/2.95  % (3720397)Time elapsed: 0.001 s
% 13.22/2.95  % (3720397)Peak memory usage: 88 MB
% 13.22/2.95  % (3720398)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1153183890:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 17.48/3.54  % (3720398)Refutation not found, incomplete strategy
% 17.48/3.54  % (3720398)------------------------------
% 17.48/3.54  % (3720398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720398)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720398)Termination reason: Refutation not found, incomplete strategy
% 17.48/3.54  % (3720398)Time elapsed: 0.002 s
% 17.48/3.54  % (3720398)Peak memory usage: 88 MB
% 17.48/3.54  % (3720400)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4227705042:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 17.48/3.54  % (3720400)Refutation not found, incomplete strategy
% 17.48/3.54  % (3720400)------------------------------
% 17.48/3.54  % (3720400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720400)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720400)Termination reason: Refutation not found, incomplete strategy
% 17.48/3.54  % (3720400)Time elapsed: 0.002 s
% 17.48/3.54  % (3720400)Peak memory usage: 88 MB
% 17.48/3.54  % (3720386)------------------------------
% 17.48/3.54  % (3720386)------------------------------
% 17.48/3.54  % (3720397)------------------------------
% 17.48/3.54  % (3720397)------------------------------
% 17.48/3.54  % (3720407)lrs+10_64_to=lpo:sil=8000:random_seed=134815139:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 17.48/3.54  % (3720408)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2812927491:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 17.48/3.54  % (3720398)------------------------------
% 17.48/3.54  % (3720398)------------------------------
% 17.48/3.54  % (3720400)------------------------------
% 17.48/3.54  % (3720400)------------------------------
% 17.48/3.54  % (3720407)Instruction limit reached! 
% 17.48/3.54  % (3720407)------------------------------
% 17.48/3.54  % (3720407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720407)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720407)Termination reason: Instruction limit
% 17.48/3.54  % (3720407)Termination phase: Saturation
% 17.48/3.54  % (3720407)Time elapsed: 0.120 s
% 17.48/3.54  % (3720407)Peak memory usage: 89 MB
% 17.48/3.54  % (3720407)Instructions burned: 126 (million)
% 17.48/3.54  % (3720408)Instruction limit reached! 
% 17.48/3.54  % (3720408)------------------------------
% 17.48/3.54  % (3720408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720408)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720408)Termination reason: Instruction limit
% 17.48/3.54  % (3720408)Termination phase: Saturation
% 17.48/3.54  % (3720408)Time elapsed: 0.156 s
% 17.48/3.54  % (3720408)Peak memory usage: 89 MB
% 17.48/3.54  % (3720408)Instructions burned: 194 (million)
% 17.48/3.54  % (3720414)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2571099782:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi)
% 17.48/3.54  % (3720415)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=379113802:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 17.48/3.54  % (3720416)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=1570807800:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 17.48/3.54  % (3720417)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=741266421:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 17.48/3.54  % (3720414)Instruction limit reached! 
% 17.48/3.54  % (3720414)------------------------------
% 17.48/3.54  % (3720414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720414)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720414)Termination reason: Instruction limit
% 17.48/3.54  % (3720414)Termination phase: Saturation
% 17.48/3.54  % (3720414)Time elapsed: 0.085 s
% 17.48/3.54  % (3720414)Peak memory usage: 90 MB
% 17.48/3.54  % (3720414)Instructions burned: 158 (million)
% 17.48/3.54  % (3720417)Refutation not found, incomplete strategy
% 17.48/3.54  % (3720417)------------------------------
% 17.48/3.54  % (3720417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720417)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720417)Termination reason: Refutation not found, incomplete strategy
% 17.48/3.54  % (3720417)Time elapsed: 0.001 s
% 17.48/3.54  % (3720417)Peak memory usage: 88 MB
% 17.48/3.54  % (3720416)Instruction limit reached! 
% 17.48/3.54  % (3720416)------------------------------
% 17.48/3.54  % (3720416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720416)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720416)Termination reason: Instruction limit
% 17.48/3.54  % (3720416)Termination phase: Saturation
% 17.48/3.54  % (3720416)Time elapsed: 0.065 s
% 17.48/3.54  % (3720416)Peak memory usage: 89 MB
% 17.48/3.54  % (3720416)Instructions burned: 107 (million)
% 17.48/3.54  % (3720422)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3510530805:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi)
% 17.48/3.54  % (3720423)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1262645807:cond=fast:i=5208:av=off_2988 on theBenchmark for (2988ds/5208Mi)
% 17.48/3.54  % (3720417)------------------------------
% 17.48/3.54  % (3720417)------------------------------
% 17.48/3.54  % (3720422)Instruction limit reached! 
% 17.48/3.54  % (3720422)------------------------------
% 17.48/3.54  % (3720422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720422)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720422)Termination reason: Instruction limit
% 17.48/3.54  % (3720422)Termination phase: Saturation
% 17.48/3.54  % (3720422)Time elapsed: 0.120 s
% 17.48/3.54  % (3720422)Peak memory usage: 90 MB
% 17.48/3.54  % (3720422)Instructions burned: 243 (million)
% 17.48/3.54  % (3720427)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2459117814:i=134:sd=2:doe=on:ss=axioms:sgt=14_2985 on theBenchmark for (2985ds/134Mi)
% 17.48/3.54  % (3720428)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2576794362:i=499:bd=all_2985 on theBenchmark for (2985ds/499Mi)
% 17.48/3.54  % (3720427)Instruction limit reached! 
% 17.48/3.54  % (3720427)------------------------------
% 17.48/3.54  % (3720427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720427)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720427)Termination reason: Instruction limit
% 17.48/3.54  % (3720427)Termination phase: Saturation
% 17.48/3.54  % (3720427)Time elapsed: 0.079 s
% 17.48/3.54  % (3720427)Peak memory usage: 89 MB
% 17.48/3.54  % (3720427)Instructions burned: 134 (million)
% 17.48/3.54  % (3720503)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3515581105:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 17.48/3.54  % (3720428)Instruction limit reached! 
% 17.48/3.54  % (3720428)------------------------------
% 17.48/3.54  % (3720428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720428)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720428)Termination reason: Instruction limit
% 17.48/3.54  % (3720428)Termination phase: Saturation
% 17.48/3.54  % (3720428)Time elapsed: 0.292 s
% 17.48/3.54  % (3720428)Peak memory usage: 94 MB
% 17.48/3.54  % (3720428)Instructions burned: 500 (million)
% 17.48/3.54  % (3720503)Instruction limit reached! 
% 17.48/3.54  % (3720503)------------------------------
% 17.48/3.54  % (3720503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720503)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720503)Termination reason: Instruction limit
% 17.48/3.54  % (3720503)Termination phase: Saturation
% 17.48/3.54  % (3720503)Time elapsed: 0.114 s
% 17.48/3.54  % (3720503)Peak memory usage: 90 MB
% 17.48/3.54  % (3720503)Instructions burned: 192 (million)
% 17.48/3.54  % (3720538)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3350180916:i=264:kws=precedence:fsr=off_2981 on theBenchmark for (2981ds/264Mi)
% 17.48/3.54  % (3720544)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=680921176:cond=on:i=156:bs=on:gtg=exists_all:er=known_2981 on theBenchmark for (2981ds/156Mi)
% 17.48/3.54  % (3720544)Instruction limit reached! 
% 17.48/3.54  % (3720544)------------------------------
% 17.48/3.54  % (3720544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720544)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720544)Termination reason: Instruction limit
% 17.48/3.54  % (3720544)Termination phase: Saturation
% 17.48/3.54  % (3720544)Time elapsed: 0.097 s
% 17.48/3.54  % (3720544)Peak memory usage: 89 MB
% 17.48/3.54  % (3720544)Instructions burned: 157 (million)
% 17.48/3.54  % (3720538)Instruction limit reached! 
% 17.48/3.54  % (3720538)------------------------------
% 17.48/3.54  % (3720538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.48/3.54  % (3720538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.48/3.54  % (3720538)CaDiCaL version: 2.1.3
% 17.48/3.54  % (3720538)Termination reason: Instruction limit
% 17.48/3.54  % (3720538)Termination phase: Saturation
% 17.48/3.54  % (3720538)Time elapsed: 0.155 s
% 17.48/3.54  % (3720538)Peak memory usage: 91 MB
% 17.48/3.54  % (3720538)Instructions burned: 264 (million)
% 17.48/3.54  % (3720589)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=2910928799:i=3256:kws=precedence:bd=preordered:av=off_2979 on theBenchmark for (2979ds/3256Mi)
% 17.48/3.54  % (3720590)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2819336502:i=537:av=off:ss=included_2978 on theBenchmark for (2978ds/537Mi)
% 17.48/3.54  % (3720380)First to succeed.
% 17.48/3.54  % (3720380)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3720359"
% 17.48/3.54  % (3720380)Refutation found. Thanks to Tanya!
% 17.48/3.54  % SZS status Unsatisfiable for theBenchmark
% 17.48/3.54  % SZS output start Proof for theBenchmark
% See solution above
% 18.77/3.74  % (3720380)------------------------------
% 18.77/3.74  % (3720380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.77/3.74  % (3720380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.77/3.74  % (3720380)CaDiCaL version: 2.1.3
% 18.77/3.74  % (3720380)Termination reason: Refutation
% 18.77/3.74  % (3720380)Time elapsed: 2.236 s
% 18.77/3.74  % (3720380)Peak memory usage: 160 MB
% 18.77/3.74  % (3720380)Instructions burned: 5733 (million)
% 18.77/3.74  % (3720380)------------------------------
% 18.77/3.74  % (3720380)------------------------------
% 18.77/3.74  % (3720359)Success in time 2.547 s
% 18.77/3.74  % Vampire exiting
%------------------------------------------------------------------------------