Vampire---5.0.1.UNS-Ref.s

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

% Computer : n008.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:14:30 AM UTC 2026

% Result   : Unsatisfiable 195.19s 39.54s
% Output   : Refutation 274.67s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

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

fof(f2,negated_conjecture,
    multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_3) ).

fof(f3,definition,
    sF0 = multiply(a3,b3),
    introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).

fof(f4,plain,
    multiply(a3,b3) = sF0,
    inference(reorient_equations,[],[f3]) ).

fof(f5,definition,
    sF1 = multiply(sF0,c3),
    introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).

fof(f6,plain,
    multiply(sF0,c3) = sF1,
    inference(reorient_equations,[],[f5]) ).

fof(f7,definition,
    sF2 = multiply(b3,c3),
    introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).

fof(f8,plain,
    multiply(b3,c3) = sF2,
    inference(reorient_equations,[],[f7]) ).

fof(f9,definition,
    sF3 = multiply(a3,sF2),
    introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).

fof(f10,plain,
    multiply(a3,sF2) = sF3,
    inference(reorient_equations,[],[f9]) ).

fof(f11,plain,
    sF1 != sF3,
    inference(definition_folding,[],[f2,f10,f8,f6,f4]) ).

fof(f16,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF1),multiply(c3,sF0))),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(X2,inverse(X3)),inverse(X1))))))),X3) = X2,
    inference(superposition,[],[f1,f6]) ).

fof(f19,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF2,a3)),sF3)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(X2,inverse(X3)),inverse(X1))))))),X3) = X2,
    inference(superposition,[],[f1,f10]) ).

fof(f23,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X2,inverse(X3)),inverse(b3))))))),X3) = X2,
    inference(superposition,[],[f1,f4]) ).

fof(f26,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(sF1),multiply(sF0,inverse(multiply(multiply(X2,inverse(X3)),inverse(c3))))))),X3) = X2,
    inference(superposition,[],[f1,f6]) ).

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

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

fof(f31,plain,
    ! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(X1)),inverse(b3))))))),X1) = X0,
    inference(superposition,[],[f23,f4]) ).

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

fof(f551,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF1),multiply(c3,sF0))),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(X2,inverse(X1))))))),X3),inverse(X3)) = X2,
    inference(superposition,[],[f472,f6]) ).

fof(f609,plain,
    ! [X2,X3,X10,X0,X1,X4,X5] : multiply(X4,inverse(inverse(X5))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(X4,inverse(X3))))))),X5),X10),inverse(X10)),
    inference(superposition,[],[f472,f27]) ).

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

fof(f617,plain,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X9,X10)),multiply(X10,X9))),multiply(inverse(multiply(X11,X12)),multiply(X11,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X8)),multiply(X7,inverse(multiply(X0,inverse(X8))))))),inverse(X12))))))),X4) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(inverse(X4)))),multiply(X3,inverse(X0))))),
    inference(superposition,[],[f27,f472]) ).

fof(f830,plain,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X9,X10)),multiply(X10,X9))),multiply(inverse(multiply(X11,X7)),multiply(X11,inverse(X0))))),X8) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF2,a3)),sF3)),multiply(inverse(multiply(X5,X6)),multiply(X5,inverse(multiply(multiply(X0,inverse(inverse(X7))),inverse(X6))))))),inverse(inverse(X8))),inverse(X4))))))),
    inference(superposition,[],[f27,f19]) ).

fof(f864,plain,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(sF1),multiply(sF0,inverse(multiply(multiply(X0,inverse(X1)),inverse(c3))))))))),X0)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,X5)),multiply(X5,X4))),multiply(inverse(multiply(X6,X7)),multiply(X6,inverse(multiply(multiply(X8,inverse(inverse(multiply(multiply(X9,inverse(X10)),inverse(X11))))),inverse(X7))))))),X11)),X8))),X10) = X9,
    inference(superposition,[],[f28,f26]) ).

fof(f953,plain,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] : inverse(multiply(inverse(multiply(inverse(multiply(X8,X9)),multiply(X9,X8))),multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(X0,inverse(X11))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,X6)),multiply(X5,inverse(multiply(multiply(X7,inverse(inverse(X0))),inverse(X6))))))),inverse(X12))),X7))),X12),
    inference(superposition,[],[f28,f472]) ).

fof(f1184,plain,
    ! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(sF2,a3)),sF3)),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(X0,inverse(inverse(X5))),inverse(X4))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF1),multiply(c3,sF0))),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,inverse(X2))))))),X5),
    inference(superposition,[],[f16,f19]) ).

fof(f1746,plain,
    ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X0,inverse(X4))))))),X5) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X5),
    inference(superposition,[],[f31,f472]) ).

fof(f1749,plain,
    ! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(X0,inverse(inverse(X5))),inverse(X4))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X5),
    inference(superposition,[],[f31,f1]) ).

fof(f1755,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X1),
    inference(superposition,[],[f31,f31]) ).

fof(f1762,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(sF2,a3)),sF3)),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(multiply(X0,inverse(inverse(X3))),inverse(X2))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X3),
    inference(superposition,[],[f31,f19]) ).

fof(f1806,plain,
    ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X0,inverse(X4))))))),X5) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(inverse(X5))),inverse(b3))))))),
    inference(superposition,[],[f1,f31]) ).

fof(f1825,plain,
    ! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(inverse(X4))),inverse(b3))))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(X0))))),X5),inverse(X5)),
    inference(superposition,[],[f472,f31]) ).

fof(f1843,plain,
    ! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X0,inverse(X4))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X6,X7)),multiply(X7,X6))),multiply(inverse(multiply(X8,X9)),multiply(X8,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(inverse(inverse(X5)))),inverse(b3))))))),inverse(X9))))))),X5),
    inference(superposition,[],[f27,f31]) ).

fof(f2064,plain,
    ! [X2,X3,X10,X0,X11,X1,X8,X9] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(sF1),multiply(sF0,inverse(multiply(multiply(X0,inverse(X1)),inverse(c3))))))))),X0)),multiply(inverse(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(X8,inverse(inverse(multiply(multiply(X9,inverse(X10)),inverse(X11))))),inverse(inverse(X11))),inverse(b3)))))))),X8))),X10) = X9,
    inference(backward_demodulation,[],[f864,f1806]) ).

fof(f2158,plain,
    ! [X2,X10,X0,X11,X1,X8,X9,X7,X12] : inverse(multiply(inverse(multiply(inverse(multiply(X8,X9)),multiply(X9,X8))),multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(X0,inverse(X11))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(X7,inverse(inverse(X0))),inverse(inverse(inverse(X12)))),inverse(b3)))))))),X7))),X12),
    inference(backward_demodulation,[],[f953,f1806]) ).

fof(f2257,plain,
    ! [X10,X4,X5] : multiply(X4,inverse(inverse(X5))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X4,inverse(inverse(X5))),inverse(b3))))))),X10),inverse(X10)),
    inference(backward_demodulation,[],[f609,f1806]) ).

fof(f2390,plain,
    ! [X2,X3,X10,X0,X11,X1,X9,X4,X12] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(inverse(X4)))),multiply(X3,inverse(X0))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X9,X10)),multiply(X10,X9))),multiply(inverse(multiply(X11,X12)),multiply(X11,inverse(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(inverse(inverse(X12)))),inverse(b3)))))))))))),X4),
    inference(backward_demodulation,[],[f617,f1806]) ).

fof(f2416,plain,
    ! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X0,inverse(X4))))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(inverse(inverse(X5)))),inverse(b3))))))),inverse(inverse(X5))),inverse(b3))))))),
    inference(backward_demodulation,[],[f1843,f1806]) ).

fof(f2437,plain,
    ! [X2,X3,X10,X0,X11,X1,X8,X9,X7,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X9,X10)),multiply(X10,X9))),multiply(inverse(multiply(X11,X7)),multiply(X11,inverse(X0))))),X8) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X7),inverse(inverse(X8))),inverse(X4))))))),
    inference(backward_demodulation,[],[f830,f1762]) ).

fof(f2439,plain,
    ! [X2,X0,X1,X5] : multiply(inverse(multiply(inverse(multiply(inverse(sF1),multiply(c3,sF0))),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,inverse(X2))))))),X5) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X5),
    inference(backward_demodulation,[],[f1184,f1762]) ).

fof(f2662,plain,
    ! [X2,X3,X0,X1,X4,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(X0))))),X5),inverse(X5)) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X4),
    inference(backward_demodulation,[],[f1825,f1755]) ).

fof(f3173,plain,
    ! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X0,inverse(X4))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(inverse(inverse(X5)))),inverse(b3))))))),inverse(b3))))))),X5),
    inference(forward_demodulation,[],[f2416,f1755]) ).

fof(f3199,plain,
    ! [X2,X3,X10,X0,X11,X1,X9,X4,X12] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(inverse(X4)))),multiply(X3,inverse(X0))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X9,X10)),multiply(X10,X9))),multiply(inverse(multiply(X11,X12)),multiply(X11,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(X12))))))),X4),
    inference(forward_demodulation,[],[f2390,f1755]) ).

fof(f3302,plain,
    ! [X10,X4,X5] : multiply(X4,inverse(inverse(X5))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X4,inverse(b3))))))),X5),X10),inverse(X10)),
    inference(forward_demodulation,[],[f2257,f1755]) ).

fof(f3397,plain,
    ! [X2,X10,X0,X11,X1,X8,X9,X7,X12] : inverse(multiply(inverse(multiply(inverse(multiply(X8,X9)),multiply(X9,X8))),multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(X0,inverse(X11))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X7,inverse(inverse(X0))),inverse(b3))))))),inverse(X12))),X7))),X12),
    inference(forward_demodulation,[],[f2158,f1755]) ).

fof(f3491,plain,
    ! [X2,X3,X10,X0,X11,X1,X8,X9] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(sF1),multiply(sF0,inverse(multiply(multiply(X0,inverse(X1)),inverse(c3))))))))),X0)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X8,inverse(inverse(multiply(multiply(X9,inverse(X10)),inverse(X11))))),inverse(b3))))))),X11)),X8))),X10) = X9,
    inference(forward_demodulation,[],[f2064,f1755]) ).

fof(f3544,plain,
    ! [X2,X3] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))),X3),inverse(X3)) = X2,
    inference(backward_demodulation,[],[f551,f2439]) ).

fof(f3562,plain,
    ! [X10,X0,X11,X8,X9,X7] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X9,X10)),multiply(X10,X9))),multiply(inverse(multiply(X11,X7)),multiply(X11,inverse(X0))))),X8) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X7),inverse(b3))))))),X8),
    inference(forward_demodulation,[],[f2437,f1749]) ).

fof(f3956,plain,
    ! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X0,inverse(X4))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(X5)),inverse(b3))))))),X5),
    inference(forward_demodulation,[],[f3173,f1755]) ).

fof(f3967,plain,
    ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(inverse(X4)))),multiply(X3,inverse(X0))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(b3))))))),X4),
    inference(forward_demodulation,[],[f3199,f1746]) ).

fof(f4077,plain,
    ! [X2,X10,X0,X11,X1,X8,X9,X7,X12] : inverse(multiply(inverse(multiply(inverse(multiply(X8,X9)),multiply(X9,X8))),multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(X0,inverse(X11))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X7,inverse(b3))))))),X0),inverse(X12))),X7))),X12),
    inference(forward_demodulation,[],[f3397,f1755]) ).

fof(f4159,plain,
    ! [X2,X3,X10,X0,X11,X1,X8,X9] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(sF1),multiply(sF0,inverse(multiply(multiply(X0,inverse(X1)),inverse(c3))))))))),X0)),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X8,inverse(b3))))))),multiply(multiply(X9,inverse(X10)),inverse(X11))),X11)),X8))),X10) = X9,
    inference(forward_demodulation,[],[f3491,f1755]) ).

fof(f4309,plain,
    ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X0,inverse(X4))))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),
    inference(forward_demodulation,[],[f3956,f31]) ).

fof(f4576,plain,
    ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(X0))))),X4) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),
    inference(backward_demodulation,[],[f616,f4309]) ).

fof(f4601,plain,
    ! [X2,X0,X1,X7,X12] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X7,inverse(b3))))))),X0),inverse(X12))),X7))),X12),
    inference(backward_demodulation,[],[f4077,f4309]) ).

fof(f4717,plain,
    ! [X2,X0,X1] : multiply(multiply(X0,inverse(X1)),inverse(inverse(X1))) = multiply(multiply(X0,X2),inverse(X2)),
    inference(superposition,[],[f3302,f31]) ).

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

fof(f4762,plain,
    ! [X0] : multiply(multiply(a3,X0),inverse(X0)) = multiply(sF0,inverse(b3)),
    inference(superposition,[],[f4725,f4]) ).

fof(f4763,plain,
    ! [X0] : multiply(multiply(a3,X0),inverse(X0)) = multiply(sF3,inverse(sF2)),
    inference(superposition,[],[f4725,f10]) ).

fof(f4764,plain,
    ! [X0] : multiply(multiply(b3,X0),inverse(X0)) = multiply(sF2,inverse(c3)),
    inference(superposition,[],[f4725,f8]) ).

fof(f4765,plain,
    ! [X0] : multiply(multiply(sF0,X0),inverse(X0)) = multiply(sF1,inverse(c3)),
    inference(superposition,[],[f4725,f6]) ).

fof(f4784,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(multiply(X0,X2),X3),inverse(X3)) = multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2))),
    inference(superposition,[],[f4717,f4725]) ).

fof(f4786,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(multiply(X0,X2),inverse(X3)),inverse(inverse(X3))) = multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2))),
    inference(superposition,[],[f4717,f4725]) ).

fof(f4787,plain,
    multiply(sF0,inverse(b3)) = multiply(sF3,inverse(sF2)),
    inference(backward_demodulation,[],[f4763,f4762]) ).

fof(f4802,plain,
    ! [X0,X1] : multiply(multiply(multiply(a3,X0),X1),inverse(X1)) = multiply(multiply(sF0,inverse(b3)),inverse(inverse(X0))),
    inference(superposition,[],[f4725,f4762]) ).

fof(f4822,plain,
    ! [X0] : multiply(multiply(sF3,X0),inverse(X0)) = multiply(multiply(sF0,inverse(b3)),inverse(inverse(sF2))),
    inference(superposition,[],[f4725,f4787]) ).

fof(f5995,plain,
    ! [X2,X0,X1,X4] : multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2))) = multiply(multiply(multiply(X0,X4),inverse(X4)),inverse(inverse(X2))),
    inference(superposition,[],[f4784,f4784]) ).

fof(f7135,plain,
    ! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(sF1),multiply(sF0,inverse(multiply(multiply(X5,inverse(X2)),inverse(c3))))))))),X5)),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X6,inverse(b3))))))),multiply(multiply(X0,X1),inverse(X1))),inverse(X7))),X6))),X7) = X0,
    inference(superposition,[],[f4159,f4725]) ).

fof(f8428,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(sF3),multiply(a3,inverse(multiply(X2,inverse(sF2))))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))),
    inference(superposition,[],[f4309,f10]) ).

fof(f8429,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(sF2),multiply(b3,inverse(multiply(X2,inverse(c3))))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))),
    inference(superposition,[],[f4309,f8]) ).

fof(f8430,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(sF1),multiply(sF0,inverse(multiply(X2,inverse(c3))))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))),
    inference(superposition,[],[f4309,f6]) ).

fof(f8444,plain,
    ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(X0))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(inverse(X4))),inverse(b3))))))),inverse(b3))))))),
    inference(superposition,[],[f4309,f31]) ).

fof(f8468,plain,
    ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(X0))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X4),inverse(b3))))))),
    inference(forward_demodulation,[],[f8444,f1755]) ).

fof(f8496,plain,
    ! [X2,X0,X1,X6,X7,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X5,inverse(X2)),inverse(b3))))))))),X5)),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X6,inverse(b3))))))),multiply(multiply(X0,X1),inverse(X1))),inverse(X7))),X6))),X7) = X0,
    inference(backward_demodulation,[],[f7135,f8430]) ).

fof(f9485,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))),X1),inverse(b3))))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(X2))))),X3),
    inference(superposition,[],[f3562,f8]) ).

fof(f9503,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))),b3),inverse(b3))))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(sF0),multiply(a3,inverse(X2))))),X3),
    inference(superposition,[],[f3562,f4]) ).

fof(f9524,plain,
    ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X3,inverse(b3))))))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(X3)))),inverse(b3)))))),inverse(b3))))))),X4) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),X0)),X4),
    inference(superposition,[],[f3562,f31]) ).

fof(f9598,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(sF0),multiply(a3,inverse(X2))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(X2))))),X3),
    inference(forward_demodulation,[],[f9503,f3544]) ).

fof(f9654,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(sF0),multiply(a3,inverse(X0))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(X0))))),inverse(X1)),inverse(b3))))))),X1),
    inference(superposition,[],[f31,f9598]) ).

fof(f9684,plain,
    ! [X2,X3,X0] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(X0))))) = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(sF0),multiply(a3,inverse(X0))))),
    inference(forward_demodulation,[],[f9654,f31]) ).

fof(f9871,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X3,inverse(b3))))))),inverse(b3))))))),X2) = inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X2)),inverse(X3))))),
    inference(superposition,[],[f3967,f4762]) ).

fof(f9872,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X3,inverse(b3))))))),inverse(b3))))))),X2) = inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(sF2,inverse(c3))),multiply(multiply(b3,inverse(X2)),inverse(X3))))),
    inference(superposition,[],[f3967,f4764]) ).

fof(f9873,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X3,inverse(b3))))))),inverse(b3))))))),X2) = inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(sF1,inverse(c3))),multiply(multiply(sF0,inverse(X2)),inverse(X3))))),
    inference(superposition,[],[f3967,f4765]) ).

fof(f10282,plain,
    ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X1,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(X2)),inverse(b3))))))))),X0)),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X3,inverse(b3))))))),X1),inverse(X4))),X3))),X4),
    inference(superposition,[],[f4601,f31]) ).

fof(f10313,plain,
    ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X1),inverse(X1))),X0))),X2),
    inference(superposition,[],[f4601,f4725]) ).

fof(f10349,plain,
    ! [X2,X3,X0,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(X0),X0))),X2),
    inference(forward_demodulation,[],[f10313,f3544]) ).

fof(f10359,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(b3))))))) = X0,
    inference(backward_demodulation,[],[f8496,f10282]) ).

fof(f13270,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))),b3) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(sF0),multiply(a3,inverse(X2))))),X3),inverse(X3)),
    inference(superposition,[],[f2662,f4]) ).

fof(f13275,plain,
    ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X7,inverse(b3))))))),multiply(inverse(multiply(X5,X6)),multiply(X5,inverse(multiply(X0,inverse(X6)))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),inverse(X7))))),X8),inverse(X8)),
    inference(superposition,[],[f2662,f4309]) ).

fof(f13360,plain,
    ! [X2,X3] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))),b3) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(X2))))),X3),inverse(X3)),
    inference(forward_demodulation,[],[f13270,f9684]) ).

fof(f18002,plain,
    ! [X2,X3,X0,X1,X6,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X5,inverse(b3))))))),multiply(inverse(sF2),multiply(b3,inverse(multiply(X0,inverse(c3)))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),inverse(X5))))),X6),inverse(X6)),
    inference(superposition,[],[f2662,f8429]) ).

fof(f18041,plain,
    ! [X0,X6,X7,X5] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X7,inverse(b3))))))),multiply(inverse(multiply(X5,X6)),multiply(X5,inverse(multiply(X0,inverse(X6)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X7,inverse(b3))))))),multiply(inverse(sF2),multiply(b3,inverse(multiply(X0,inverse(c3)))))),
    inference(backward_demodulation,[],[f13275,f18002]) ).

fof(f18227,plain,
    ! [X0] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF3),multiply(a3,inverse(multiply(X0,inverse(sF2))))))),
    inference(superposition,[],[f8428,f4]) ).

fof(f18282,plain,
    ! [X2,X3,X0,X1,X6,X4,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),inverse(X5))))),X6),inverse(X6)) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X5,inverse(b3))))))),multiply(inverse(sF3),multiply(a3,inverse(multiply(X0,inverse(sF2)))))),
    inference(superposition,[],[f2662,f8428]) ).

fof(f18320,plain,
    ! [X0,X5] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X5,inverse(b3))))))),multiply(inverse(sF2),multiply(b3,inverse(multiply(X0,inverse(c3)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X5,inverse(b3))))))),multiply(inverse(sF3),multiply(a3,inverse(multiply(X0,inverse(sF2)))))),
    inference(forward_demodulation,[],[f18282,f18002]) ).

fof(f18817,plain,
    ! [X2,X0,X1] : multiply(X0,inverse(inverse(b3))) = multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(X0))))),X1),inverse(X1)),X2),inverse(X2)),
    inference(superposition,[],[f3302,f13360]) ).

fof(f20593,plain,
    ! [X2,X3,X0,X1,X6,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(X0,X5),inverse(X5)),inverse(b3)))))),inverse(b3))))))),X4) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))),X6),inverse(X6)),
    inference(superposition,[],[f2662,f10359]) ).

fof(f24749,plain,
    ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X3,inverse(b3))))))),multiply(inverse(sF3),multiply(a3,inverse(multiply(X0,inverse(sF2)))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(X3))))),X4),inverse(X4)),
    inference(superposition,[],[f2662,f18227]) ).

fof(f24800,plain,
    ! [X3,X0] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X3,inverse(b3))))))),multiply(inverse(sF3),multiply(a3,inverse(multiply(X0,inverse(sF2)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X3,inverse(b3))))))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3)))))),
    inference(forward_demodulation,[],[f24749,f2662]) ).

fof(f24816,plain,
    ! [X0,X5] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X5,inverse(b3))))))),multiply(inverse(sF2),multiply(b3,inverse(multiply(X0,inverse(c3)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X5,inverse(b3))))))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3)))))),
    inference(backward_demodulation,[],[f18320,f24800]) ).

fof(f24843,plain,
    ! [X0,X6,X7,X5] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X7,inverse(b3))))))),multiply(inverse(multiply(X5,X6)),multiply(X5,inverse(multiply(X0,inverse(X6)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X7,inverse(b3))))))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3)))))),
    inference(backward_demodulation,[],[f18041,f24816]) ).

fof(f24864,plain,
    ! [X2,X3,X0,X4] : multiply(X0,multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(X4,inverse(X3)))))) = multiply(X0,multiply(inverse(sF0),multiply(a3,inverse(multiply(X4,inverse(b3)))))),
    inference(superposition,[],[f24843,f10359]) ).

fof(f34040,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(X1)),inverse(b3))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,X1),inverse(X0))))),X2),
    inference(superposition,[],[f9485,f4762]) ).

fof(f34100,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X1),inverse(b3))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X0),X1)),multiply(sF1,inverse(c3))))),X2),
    inference(superposition,[],[f9485,f4765]) ).

fof(f34101,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X1),inverse(b3))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF3,X0),X1)),multiply(multiply(sF0,inverse(b3)),inverse(inverse(sF2)))))),X2),
    inference(superposition,[],[f9485,f4822]) ).

fof(f34898,plain,
    ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),X0)),X4) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF3,X3),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(X3)))),inverse(b3))))))),multiply(multiply(sF0,inverse(b3)),inverse(inverse(sF2)))))),X4),
    inference(backward_demodulation,[],[f9524,f34101]) ).

fof(f34945,plain,
    ! [X10,X0,X11,X8,X9,X7] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X9,X10)),multiply(X10,X9))),multiply(inverse(multiply(X11,X7)),multiply(X11,inverse(X0))))),X8) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X0),X7)),multiply(sF1,inverse(c3))))),X8),
    inference(backward_demodulation,[],[f3562,f34100]) ).

fof(f34952,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X0),X1)),multiply(sF1,inverse(c3))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF3,X0),X1)),multiply(multiply(sF0,inverse(b3)),inverse(inverse(sF2)))))),X2),
    inference(backward_demodulation,[],[f34101,f34100]) ).

fof(f35012,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,X1),inverse(X0))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X0),inverse(X1))),multiply(sF1,inverse(c3))))),X2),
    inference(forward_demodulation,[],[f34040,f34100]) ).

fof(f35358,plain,
    ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),X0)),X4) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X3),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(X3)))),inverse(b3))))))),multiply(sF1,inverse(c3))))),X4),
    inference(backward_demodulation,[],[f34898,f34952]) ).

fof(f35833,plain,
    ! [X0,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X0),inverse(X4))),multiply(sF1,inverse(c3))))),X4),
    inference(backward_demodulation,[],[f4576,f34945]) ).

fof(f36769,plain,
    ! [X0,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,X4),inverse(X0))))),X4),
    inference(forward_demodulation,[],[f35833,f35012]) ).

fof(f37053,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(X2))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X2),X1)),multiply(sF1,inverse(c3))))),X3),
    inference(superposition,[],[f34945,f4]) ).

fof(f37055,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(X2))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X2),X1)),multiply(sF1,inverse(c3))))),X3),
    inference(superposition,[],[f34945,f8]) ).

fof(f37329,plain,
    ! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,X1)),multiply(X5,inverse(X0))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X0),X1)),multiply(sF1,inverse(c3))))),X2),inverse(X2)),inverse(b3))))))),
    inference(superposition,[],[f10359,f34945]) ).

fof(f37336,plain,
    ! [X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,X1)),multiply(X5,inverse(X0))))) = inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X0),X1)),multiply(sF1,inverse(c3))))),
    inference(forward_demodulation,[],[f37329,f10359]) ).

fof(f37591,plain,
    ! [X0,X4] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(b3))))))),X4) = inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X0),inverse(inverse(X4)))),multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f3967,f37336]) ).

fof(f37730,plain,
    ! [X0,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X4),inverse(b3))))))) = inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X0),X4)),multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f8468,f37336]) ).

fof(f38240,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f9871,f37591]) ).

fof(f38241,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(sF2,inverse(c3))),multiply(multiply(b3,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f9872,f37591]) ).

fof(f38242,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(sF1,inverse(c3))),multiply(multiply(sF0,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f9873,f37591]) ).

fof(f41226,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X1),inverse(X0))),multiply(sF1,inverse(c3))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,X0),inverse(X1))))),X2),
    inference(superposition,[],[f37055,f4762]) ).

fof(f41284,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X0),X1)),multiply(sF1,inverse(c3))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(multiply(sF0,X0),X1)),multiply(sF1,inverse(c3))))),X2),
    inference(superposition,[],[f37055,f4765]) ).

fof(f41291,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X1),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(X1)))),inverse(b3))))))),multiply(sF1,inverse(c3))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),X0)),X2),
    inference(superposition,[],[f37055,f31]) ).

fof(f41687,plain,
    ! [X2,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),X0)),X4) = multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),X0)),X4),
    inference(backward_demodulation,[],[f35358,f41291]) ).

fof(f42116,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,X1),inverse(X0))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(multiply(sF0,X0),inverse(X1))),multiply(sF1,inverse(c3))))),X2),
    inference(backward_demodulation,[],[f35012,f41284]) ).

fof(f42612,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,X0),inverse(X1))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(multiply(sF0,X1),inverse(X0))),multiply(sF1,inverse(c3))))),X2),
    inference(forward_demodulation,[],[f41226,f41284]) ).

fof(f42762,plain,
    ! [X2,X0] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(X0),X0))),X2),
    inference(backward_demodulation,[],[f10349,f41687]) ).

fof(f42769,plain,
    ! [X3,X0,X6,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(X0,X5),inverse(X5)),inverse(b3)))))),inverse(b3))))))),X4) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))),X6),inverse(X6)),
    inference(backward_demodulation,[],[f20593,f41687]) ).

fof(f42887,plain,
    ! [X0,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(multiply(sF0,X0),inverse(X4))),multiply(sF1,inverse(c3))))),X4),
    inference(backward_demodulation,[],[f36769,f42116]) ).

fof(f43444,plain,
    ! [X0,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,X4),inverse(X0))))),X4),
    inference(forward_demodulation,[],[f42887,f42612]) ).

fof(f43599,plain,
    ! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),X0)),X1) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),X1),
    inference(superposition,[],[f41687,f4]) ).

fof(f43660,plain,
    ! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),X0)),X1) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),X0)),X1),
    inference(superposition,[],[f41687,f8]) ).

fof(f43767,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),X0)) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),X0)),X1),inverse(X1)),inverse(b3))))))),
    inference(superposition,[],[f10359,f41687]) ).

fof(f43776,plain,
    ! [X2,X3,X0] : inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),X0)) = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),X0)),
    inference(forward_demodulation,[],[f43767,f10359]) ).

fof(f44281,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(X2))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(multiply(sF0,X2),X1)),multiply(sF1,inverse(c3))))),X3),
    inference(backward_demodulation,[],[f37053,f43660]) ).

fof(f45349,plain,
    ! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),X1) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),X0)),X1),
    inference(backward_demodulation,[],[f43660,f43599]) ).

fof(f45417,plain,
    ! [X2,X0] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X2,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(X0),X0))),X2),
    inference(backward_demodulation,[],[f42762,f43599]) ).

fof(f45419,plain,
    ! [X3,X0,X6,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(X0,X5),inverse(X5)),inverse(b3)))))),inverse(b3))))))),X4) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))),X6),inverse(X6)),
    inference(backward_demodulation,[],[f42769,f43599]) ).

fof(f45436,plain,
    ! [X0,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,X4),inverse(X0))))),X4),
    inference(backward_demodulation,[],[f43444,f43599]) ).

fof(f46375,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))) = inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X2)),inverse(X3))))),
    inference(backward_demodulation,[],[f38240,f43776]) ).

fof(f46378,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))) = inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF1,inverse(c3))),multiply(multiply(sF0,inverse(X2)),inverse(X3))))),
    inference(backward_demodulation,[],[f38242,f43776]) ).

fof(f46380,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))) = inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF2,inverse(c3))),multiply(multiply(b3,inverse(X2)),inverse(X3))))),
    inference(backward_demodulation,[],[f38241,f43776]) ).

fof(f46639,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(X2))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(sF0,X2),X1)),multiply(sF1,inverse(c3))))),X3),
    inference(forward_demodulation,[],[f44281,f43599]) ).

fof(f48193,plain,
    ! [X0,X4] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(b3))))))),X4) = inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF2,inverse(c3))),multiply(multiply(b3,inverse(X4)),inverse(X0))))),
    inference(backward_demodulation,[],[f37591,f46380]) ).

fof(f48514,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF1,inverse(c3))),multiply(multiply(sF0,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF2,inverse(c3))),multiply(multiply(b3,inverse(X2)),inverse(X3))))),
    inference(forward_demodulation,[],[f46378,f46380]) ).

fof(f48521,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF2,inverse(c3))),multiply(multiply(b3,inverse(X2)),inverse(X3))))),
    inference(backward_demodulation,[],[f46380,f46375]) ).

fof(f49444,plain,
    ! [X0,X4] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(b3))))))),X4) = inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X4)),inverse(X0))))),
    inference(backward_demodulation,[],[f48193,f48521]) ).

fof(f49652,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF1,inverse(c3))),multiply(multiply(sF0,inverse(X2)),inverse(X3))))),
    inference(backward_demodulation,[],[f48514,f48521]) ).

fof(f50177,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),X0)) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),X1),inverse(X1)),inverse(b3))))))),
    inference(superposition,[],[f10359,f45349]) ).

fof(f50184,plain,
    ! [X0] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)) = inverse(multiply(inverse(multiply(inverse(multiply(c3,b3)),sF2)),X0)),
    inference(forward_demodulation,[],[f50177,f10359]) ).

fof(f50484,plain,
    ! [X0,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),X4),inverse(b3))))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(sF0,X0),X4)),multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f37730,f50184]) ).

fof(f50532,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f46375,f50184]) ).

fof(f50645,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF2,inverse(c3))),multiply(multiply(b3,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f48521,f50532]) ).

fof(f50669,plain,
    ! [X0,X4] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(b3))))))),X4) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(sF0,X0),inverse(inverse(X4)))),multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f49444,f50532]) ).

fof(f50861,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),multiply(inverse(multiply(sF1,inverse(c3))),multiply(multiply(sF0,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f49652,f50532]) ).

fof(f52120,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),X0)) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),X1),inverse(X1)),inverse(b3))))))),
    inference(superposition,[],[f10359,f43599]) ).

fof(f52127,plain,
    ! [X0] : inverse(multiply(inverse(multiply(inverse(sF2),multiply(c3,b3))),X0)) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),
    inference(forward_demodulation,[],[f52120,f10359]) ).

fof(f52223,plain,
    ! [X2,X3,X0] : inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),X0)) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),
    inference(backward_demodulation,[],[f43776,f52127]) ).

fof(f52232,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f50532,f52127]) ).

fof(f52233,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF2,inverse(c3))),multiply(multiply(b3,inverse(X2)),inverse(X3))))),
    inference(backward_demodulation,[],[f50645,f52127]) ).

fof(f52234,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(sF0,X3),inverse(inverse(X2)))),multiply(sF1,inverse(c3))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF1,inverse(c3))),multiply(multiply(sF0,inverse(X2)),inverse(X3))))),
    inference(backward_demodulation,[],[f50861,f52127]) ).

fof(f52386,plain,
    ! [X0,X4] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(b3))))))),X4) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF1,inverse(c3))),multiply(multiply(sF0,inverse(X4)),inverse(X0))))),
    inference(backward_demodulation,[],[f50669,f52234]) ).

fof(f52706,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF2,inverse(c3))),multiply(multiply(b3,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF1,inverse(c3))),multiply(multiply(sF0,inverse(X2)),inverse(X3))))),
    inference(backward_demodulation,[],[f52234,f52233]) ).

fof(f52707,plain,
    ! [X2,X3] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X2)),inverse(X3))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF2,inverse(c3))),multiply(multiply(b3,inverse(X2)),inverse(X3))))),
    inference(backward_demodulation,[],[f52233,f52232]) ).

fof(f52970,plain,
    ! [X0,X4] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(b3))))))),X4) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF2,inverse(c3))),multiply(multiply(b3,inverse(X4)),inverse(X0))))),
    inference(backward_demodulation,[],[f52386,f52706]) ).

fof(f53530,plain,
    ! [X0,X4] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(b3))))))),X4) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X4)),inverse(X0))))),
    inference(forward_demodulation,[],[f52970,f52707]) ).

fof(f56463,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(b3))))))),X2),inverse(X2)),
    inference(superposition,[],[f3544,f52223]) ).

fof(f56518,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))) = inverse(multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f56463,f3544]) ).

fof(f65719,plain,
    ! [X2,X0,X1,X4] : multiply(multiply(multiply(X1,X4),inverse(X4)),inverse(X0)) = multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(X0)),
    inference(superposition,[],[f5995,f10359]) ).

fof(f66450,plain,
    ! [X2,X0,X1,X4] : multiply(multiply(multiply(X1,X2),inverse(X2)),X0) = multiply(multiply(multiply(X1,X4),inverse(X4)),X0),
    inference(superposition,[],[f65719,f10359]) ).

fof(f72214,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X0,X1)),multiply(X1,X0)),inverse(inverse(b3))) = multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(inverse(sF0),multiply(b3,a3))))))),X2),inverse(X2)),X3),inverse(X3)),
    inference(superposition,[],[f18817,f56518]) ).

fof(f72813,plain,
    ! [X0,X1] : multiply(multiply(inverse(multiply(X0,X1)),multiply(X1,X0)),inverse(inverse(b3))) = multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(inverse(b3))),
    inference(forward_demodulation,[],[f72214,f18817]) ).

fof(f89501,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))))),inverse(X1)),inverse(b3))))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,X1),inverse(X0))))),
    inference(superposition,[],[f10359,f45436]) ).

fof(f89526,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,X1),inverse(X0))))) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(sF0,X0),inverse(X1))),multiply(sF1,inverse(c3))))),
    inference(forward_demodulation,[],[f89501,f50484]) ).

fof(f93211,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(X1,X0)) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(inverse(b3))),inverse(b3))))))),inverse(b3)),
    inference(superposition,[],[f31,f72813]) ).

fof(f93254,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(X1,X0)) = multiply(inverse(sF0),multiply(b3,a3)),
    inference(forward_demodulation,[],[f93211,f31]) ).

fof(f93445,plain,
    ! [X2,X0,X1] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(multiply(inverse(X2),multiply(X0,X2))),multiply(multiply(X0,X1),inverse(X1))),
    inference(superposition,[],[f93254,f4725]) ).

fof(f93493,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(multiply(b3,a3)),sF0),
    inference(superposition,[],[f93254,f4]) ).

fof(f93505,plain,
    ! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(sF0,X0),inverse(X0))),multiply(sF1,inverse(c3))))),X1) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X1),
    inference(superposition,[],[f46639,f93254]) ).

fof(f93526,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(multiply(X0,X1)),X2),inverse(X2)) = multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(X1,X0))),
    inference(superposition,[],[f4725,f93254]) ).

fof(f93535,plain,
    ! [X0,X1] : inverse(multiply(X0,X1)) = inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(X1,X0))),inverse(b3))))))),
    inference(superposition,[],[f10359,f93254]) ).

fof(f93549,plain,
    ! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,X0),inverse(X0))))),X1) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X1),
    inference(forward_demodulation,[],[f93505,f89526]) ).

fof(f93837,plain,
    ! [X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(sF0,inverse(b3))))),X1) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X1),
    inference(forward_demodulation,[],[f93549,f4762]) ).

fof(f93866,plain,
    ! [X1] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X1,inverse(b3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X1),
    inference(forward_demodulation,[],[f93837,f45417]) ).

fof(f93868,plain,
    ! [X10,X4,X5] : multiply(X4,inverse(inverse(X5))) = multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X4),X5),X10),inverse(X10)),
    inference(backward_demodulation,[],[f3302,f93866]) ).

fof(f93869,plain,
    ! [X2,X3] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X2),X3),inverse(X3)) = X2,
    inference(backward_demodulation,[],[f3544,f93866]) ).

fof(f93878,plain,
    ! [X2,X3] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(X2))))),X3),inverse(X3)) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X2),b3),
    inference(backward_demodulation,[],[f13360,f93866]) ).

fof(f94153,plain,
    ! [X0,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X4)),inverse(X0))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X0),inverse(b3))))))),X4),
    inference(backward_demodulation,[],[f53530,f93866]) ).

fof(f95443,plain,
    ! [X3,X0,X6,X4,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))),X6),inverse(X6)) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(X0,X5),inverse(X5)),inverse(b3))))))),X4),
    inference(backward_demodulation,[],[f45419,f93866]) ).

fof(f95455,plain,
    ! [X0,X1] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(X0,inverse(X1))),X1) = X0,
    inference(backward_demodulation,[],[f31,f93866]) ).

fof(f95478,plain,
    ! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(multiply(X0,X1),inverse(X1))) = X0,
    inference(backward_demodulation,[],[f10359,f93866]) ).

fof(f95484,plain,
    ! [X0,X1] : inverse(multiply(X0,X1)) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(X1,X0)))),
    inference(backward_demodulation,[],[f93535,f93866]) ).

fof(f96424,plain,
    ! [X0,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X4)),inverse(X0))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X0)),X4),
    inference(forward_demodulation,[],[f94153,f93866]) ).

fof(f97283,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(sF0),multiply(b3,a3))),
    inference(superposition,[],[f95455,f93254]) ).

fof(f97582,plain,
    ! [X0,X1] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(inverse(sF0),multiply(b3,a3)))),inverse(inverse(X0))) = multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),X1),inverse(X1)),
    inference(superposition,[],[f93868,f93254]) ).

fof(f97667,plain,
    ! [X2,X0,X1] : multiply(X2,inverse(inverse(inverse(X2)))) = multiply(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X0),inverse(X0)),X1),inverse(X1)),
    inference(superposition,[],[f93868,f66450]) ).

fof(f97938,plain,
    ! [X2,X0] : multiply(X2,inverse(inverse(inverse(X2)))) = multiply(X0,inverse(inverse(inverse(X0)))),
    inference(forward_demodulation,[],[f97667,f93868]) ).

fof(f98271,plain,
    ! [X0,X1] : multiply(multiply(sF0,inverse(b3)),inverse(inverse(inverse(inverse(inverse(a3)))))) = multiply(multiply(multiply(X0,inverse(inverse(inverse(X0)))),X1),inverse(X1)),
    inference(superposition,[],[f4802,f97938]) ).

fof(f98272,plain,
    ! [X0] : multiply(sF0,inverse(b3)) = multiply(multiply(X0,inverse(inverse(inverse(X0)))),inverse(inverse(inverse(inverse(a3))))),
    inference(superposition,[],[f4762,f97938]) ).

fof(f98741,plain,
    ! [X0] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),inverse(X0)) = multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(inverse(sF0),multiply(b3,a3)))),
    inference(superposition,[],[f93869,f93254]) ).

fof(f98769,plain,
    ! [X0,X1] : inverse(inverse(inverse(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))))))) = multiply(multiply(multiply(X0,inverse(inverse(inverse(X0)))),X1),inverse(X1)),
    inference(superposition,[],[f93869,f97938]) ).

fof(f98772,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,inverse(X2))))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3)))))),X3),inverse(X3)),
    inference(superposition,[],[f93869,f24864]) ).

fof(f99055,plain,
    ! [X2,X0,X1] : multiply(inverse(sF0),multiply(a3,inverse(multiply(X0,inverse(b3))))) = multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,inverse(X2))))),
    inference(forward_demodulation,[],[f98772,f93869]) ).

fof(f99058,plain,
    inverse(inverse(inverse(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))))))) = multiply(multiply(sF0,inverse(b3)),inverse(inverse(inverse(inverse(inverse(a3)))))),
    inference(forward_demodulation,[],[f98769,f98271]) ).

fof(f100098,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(X0,inverse(multiply(multiply(X0,X1),inverse(X1))))),
    inference(superposition,[],[f95478,f95478]) ).

fof(f100150,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X1),inverse(X1)) = multiply(X0,inverse(multiply(multiply(X0,X2),inverse(X2)))),
    inference(superposition,[],[f4725,f95478]) ).

fof(f100155,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X1),inverse(X2)),inverse(inverse(X2))) = multiply(multiply(X0,inverse(multiply(multiply(X0,X3),inverse(X3)))),inverse(inverse(X1))),
    inference(superposition,[],[f4786,f95478]) ).

fof(f100167,plain,
    ! [X3,X0,X1] : multiply(multiply(X0,inverse(multiply(multiply(X0,X3),inverse(X3)))),inverse(inverse(X1))) = X1,
    inference(forward_demodulation,[],[f100155,f93869]) ).

fof(f100336,plain,
    ! [X1] : multiply(multiply(a3,inverse(multiply(sF0,inverse(b3)))),inverse(inverse(X1))) = X1,
    inference(superposition,[],[f100167,f4762]) ).

fof(f100338,plain,
    ! [X1] : multiply(multiply(sF0,inverse(multiply(sF1,inverse(c3)))),inverse(inverse(X1))) = X1,
    inference(superposition,[],[f100167,f4765]) ).

fof(f100407,plain,
    ! [X2,X0,X1] : multiply(multiply(X0,X2),inverse(X2)) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X1),inverse(X1))),inverse(inverse(inverse(inverse(X0))))),
    inference(superposition,[],[f93868,f100167]) ).

fof(f100493,plain,
    ! [X0] : multiply(X0,inverse(inverse(inverse(X0)))) = inverse(multiply(a3,inverse(multiply(sF0,inverse(b3))))),
    inference(superposition,[],[f97938,f100336]) ).

fof(f100500,plain,
    ! [X0] : multiply(a3,inverse(multiply(sF0,inverse(b3)))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X0),inverse(X0)),
    inference(superposition,[],[f95455,f100336]) ).

fof(f100518,plain,
    ! [X2,X0,X1] : multiply(multiply(X0,inverse(inverse(inverse(X0)))),X2) = multiply(multiply(multiply(multiply(a3,inverse(multiply(sF0,inverse(b3)))),X1),inverse(X1)),X2),
    inference(superposition,[],[f66450,f100336]) ).

fof(f100524,plain,
    ! [X2,X0] : multiply(multiply(X0,inverse(inverse(inverse(X0)))),X2) = multiply(multiply(multiply(sF0,inverse(b3)),inverse(inverse(inverse(multiply(sF0,inverse(b3)))))),X2),
    inference(forward_demodulation,[],[f100518,f4802]) ).

fof(f100540,plain,
    ! [X2,X0] : multiply(multiply(X0,X2),inverse(X2)) = multiply(inverse(multiply(a3,inverse(multiply(sF0,inverse(b3))))),inverse(inverse(inverse(inverse(X0))))),
    inference(backward_demodulation,[],[f100407,f100500]) ).

fof(f100541,plain,
    ! [X2,X0] : multiply(a3,inverse(multiply(sF0,inverse(b3)))) = multiply(X0,inverse(multiply(multiply(X0,X2),inverse(X2)))),
    inference(backward_demodulation,[],[f100150,f100500]) ).

fof(f100569,plain,
    ! [X2,X0] : multiply(multiply(X0,inverse(inverse(inverse(X0)))),X2) = multiply(inverse(multiply(a3,inverse(multiply(sF0,inverse(b3))))),X2),
    inference(forward_demodulation,[],[f100524,f100493]) ).

fof(f100603,plain,
    inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(a3,inverse(multiply(sF0,inverse(b3))))),
    inference(backward_demodulation,[],[f100098,f100541]) ).

fof(f100702,plain,
    multiply(a3,inverse(multiply(sF0,inverse(b3)))) = multiply(b3,inverse(multiply(sF2,inverse(c3)))),
    inference(superposition,[],[f100541,f4764]) ).

fof(f100703,plain,
    multiply(a3,inverse(multiply(sF0,inverse(b3)))) = multiply(sF0,inverse(multiply(sF1,inverse(c3)))),
    inference(superposition,[],[f100541,f4765]) ).

fof(f100759,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(multiply(a3,inverse(multiply(sF0,inverse(b3)))),X1),X2),inverse(X2)) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X0),inverse(X0))),inverse(inverse(X1))),
    inference(superposition,[],[f93868,f100541]) ).

fof(f100784,plain,
    ! [X2,X1] : multiply(multiply(multiply(multiply(a3,inverse(multiply(sF0,inverse(b3)))),X1),X2),inverse(X2)) = multiply(inverse(multiply(a3,inverse(multiply(sF0,inverse(b3))))),inverse(inverse(X1))),
    inference(forward_demodulation,[],[f100759,f100500]) ).

fof(f100837,plain,
    ! [X0] : multiply(X0,inverse(inverse(inverse(X0)))) = inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f100493,f100703]) ).

fof(f100839,plain,
    ! [X0] : multiply(sF0,inverse(multiply(sF1,inverse(c3)))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X0),inverse(X0)),
    inference(backward_demodulation,[],[f100500,f100703]) ).

fof(f100845,plain,
    ! [X2,X0] : multiply(multiply(X0,X2),inverse(X2)) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(X0))))),
    inference(backward_demodulation,[],[f100540,f100703]) ).

fof(f100846,plain,
    ! [X2,X0] : multiply(sF0,inverse(multiply(sF1,inverse(c3)))) = multiply(X0,inverse(multiply(multiply(X0,X2),inverse(X2)))),
    inference(backward_demodulation,[],[f100541,f100703]) ).

fof(f100856,plain,
    ! [X2,X0] : multiply(multiply(X0,inverse(inverse(inverse(X0)))),X2) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),X2),
    inference(backward_demodulation,[],[f100569,f100703]) ).

fof(f100873,plain,
    inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(sF0,inverse(multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f100603,f100703]) ).

fof(f100885,plain,
    multiply(b3,inverse(multiply(sF2,inverse(c3)))) = multiply(sF0,inverse(multiply(sF1,inverse(c3)))),
    inference(forward_demodulation,[],[f100702,f100703]) ).

fof(f100971,plain,
    ! [X2,X1] : multiply(multiply(multiply(multiply(sF0,inverse(multiply(sF1,inverse(c3)))),X1),X2),inverse(X2)) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(X1))),
    inference(forward_demodulation,[],[f100784,f100703]) ).

fof(f101280,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(X0,X1),inverse(X1)),X2) = multiply(multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(X0))))),X2),
    inference(superposition,[],[f66450,f100837]) ).

fof(f101281,plain,
    ! [X0] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3)))))),multiply(inverse(inverse(inverse(X0))),X0)),
    inference(superposition,[],[f93254,f100837]) ).

fof(f101305,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(X0,X2),inverse(X2)),inverse(inverse(X1))) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(multiply(X0,X1)))))),
    inference(superposition,[],[f4784,f100837]) ).

fof(f101306,plain,
    ! [X0,X1] : multiply(X0,inverse(inverse(X1))) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X0),X1)))))),
    inference(superposition,[],[f93868,f100837]) ).

fof(f101311,plain,
    ! [X0,X1] : multiply(inverse(inverse(inverse(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))))))),inverse(inverse(X0))) = multiply(multiply(multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),X0),X1),inverse(X1)),
    inference(superposition,[],[f93868,f100837]) ).

fof(f101364,plain,
    ! [X0,X1] : multiply(multiply(multiply(sF0,inverse(b3)),inverse(inverse(inverse(inverse(inverse(a3)))))),inverse(inverse(X0))) = multiply(multiply(multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),X0),X1),inverse(X1)),
    inference(forward_demodulation,[],[f101311,f99058]) ).

fof(f101506,plain,
    ! [X0,X1] : multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,X1),inverse(b3))))) = multiply(inverse(multiply(X0,X1)),multiply(sF0,inverse(multiply(sF1,inverse(c3))))),
    inference(superposition,[],[f99055,f100846]) ).

fof(f101615,plain,
    inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))) = multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))),inverse(b3))))),
    inference(backward_demodulation,[],[f100873,f101506]) ).

fof(f102015,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2))),inverse(inverse(X3))) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(multiply(multiply(X0,X2),X3)))))),
    inference(superposition,[],[f100845,f4784]) ).

fof(f102043,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(X1,X0))) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(inverse(multiply(X0,X1))))))),
    inference(superposition,[],[f100845,f93254]) ).

fof(f102090,plain,
    multiply(sF0,inverse(b3)) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(a3))))),
    inference(superposition,[],[f4762,f100845]) ).

fof(f102940,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(X0),multiply(X1,X0))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(multiply(X1,X2),inverse(X2))))),
    inference(superposition,[],[f95478,f93445]) ).

fof(f102942,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(multiply(X1,X2),inverse(X2)))) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(inverse(multiply(inverse(X0),multiply(X1,X0)))))))),
    inference(superposition,[],[f100845,f93445]) ).

fof(f102944,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(multiply(X1,X2),inverse(X2)))) = multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(multiply(X1,X0),inverse(X0)))),
    inference(forward_demodulation,[],[f102942,f102043]) ).

fof(f102945,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(X0),multiply(X1,X0))) = inverse(multiply(inverse(X2),multiply(X1,X2))),
    inference(forward_demodulation,[],[f102940,f95484]) ).

fof(f103083,plain,
    ! [X0,X1] : inverse(multiply(inverse(X0),multiply(X1,X0))) = inverse(multiply(inverse(inverse(inverse(inverse(X1)))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))))),
    inference(superposition,[],[f102945,f100837]) ).

fof(f103259,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(X1,X2)) = multiply(multiply(sF0,inverse(multiply(sF1,inverse(c3)))),inverse(inverse(multiply(inverse(X0),multiply(X1,X0))))),
    inference(superposition,[],[f100338,f102945]) ).

fof(f103265,plain,
    ! [X2,X0,X1] : multiply(inverse(X0),multiply(X1,X0)) = multiply(inverse(X2),multiply(X1,X2)),
    inference(forward_demodulation,[],[f103259,f100338]) ).

fof(f103410,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(X1,X0)) = multiply(inverse(inverse(inverse(inverse(X1)))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3)))))),
    inference(superposition,[],[f103265,f100837]) ).

fof(f103412,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(X2,X1)) = multiply(inverse(inverse(inverse(inverse(X2)))),multiply(X0,inverse(inverse(inverse(X0))))),
    inference(superposition,[],[f103265,f97938]) ).

fof(f103415,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(multiply(X0,X2),X1)) = multiply(inverse(inverse(X2)),multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(X0)))))),
    inference(superposition,[],[f103265,f100845]) ).

fof(f103417,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X2),multiply(multiply(X0,X3),X2)) = multiply(inverse(inverse(X3)),multiply(multiply(X0,X1),inverse(X1))),
    inference(superposition,[],[f103265,f4725]) ).

fof(f103441,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(multiply(a3,X1),X0)) = multiply(inverse(inverse(X1)),multiply(sF0,inverse(b3))),
    inference(superposition,[],[f103265,f4762]) ).

fof(f103445,plain,
    ! [X0,X1] : multiply(inverse(inverse(inverse(X0))),X0) = multiply(inverse(X1),multiply(multiply(sF0,inverse(multiply(sF1,inverse(c3)))),X1)),
    inference(superposition,[],[f103265,f100338]) ).

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

fof(f103457,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X1)) = multiply(inverse(multiply(multiply(X0,X2),inverse(X2))),X0),
    inference(superposition,[],[f103265,f95478]) ).

fof(f103459,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(inverse(inverse(inverse(X0))))),multiply(multiply(X0,X1),inverse(X1))) = multiply(inverse(X2),multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),X2)),
    inference(superposition,[],[f103265,f100845]) ).

fof(f103470,plain,
    ! [X0] : multiply(inverse(sF2),sF3) = multiply(inverse(X0),multiply(a3,X0)),
    inference(superposition,[],[f103265,f10]) ).

fof(f103471,plain,
    ! [X0] : multiply(inverse(X0),multiply(b3,X0)) = multiply(inverse(c3),sF2),
    inference(superposition,[],[f103265,f8]) ).

fof(f103472,plain,
    ! [X0] : multiply(inverse(X0),multiply(sF0,X0)) = multiply(inverse(c3),sF1),
    inference(superposition,[],[f103265,f6]) ).

fof(f103473,plain,
    ! [X0] : multiply(inverse(X0),multiply(sF3,X0)) = multiply(inverse(inverse(sF2)),multiply(sF0,inverse(b3))),
    inference(superposition,[],[f103265,f4787]) ).

fof(f103522,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X2)),inverse(multiply(X1,multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))))))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(inverse(X0),multiply(X1,X0))),X2),
    inference(superposition,[],[f96424,f103265]) ).

fof(f103523,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(inverse(X0),multiply(X1,X0)),X2),inverse(X2)) = multiply(X1,multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),
    inference(superposition,[],[f93869,f103265]) ).

fof(f103533,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(inverse(X0),multiply(X1,X0)),inverse(multiply(X1,X2))) = multiply(multiply(inverse(X2),X3),inverse(X3)),
    inference(superposition,[],[f4725,f103265]) ).

fof(f103553,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(X0),multiply(X1,X0)),inverse(multiply(X1,X2))) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(inverse(X2)))))),
    inference(superposition,[],[f100845,f103265]) ).

fof(f103612,plain,
    ! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(inverse(X0)))))) = multiply(multiply(inverse(c3),sF2),inverse(multiply(b3,X0))),
    inference(superposition,[],[f100845,f103471]) ).

fof(f103617,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(inverse(X1),X0)) = multiply(inverse(multiply(b3,X1)),multiply(inverse(c3),sF2)),
    inference(superposition,[],[f103265,f103471]) ).

fof(f103619,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(X1,X0))) = multiply(multiply(inverse(c3),sF2),inverse(multiply(b3,multiply(X0,X1)))),
    inference(backward_demodulation,[],[f102043,f103612]) ).

fof(f103620,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(X0),multiply(X1,X0)),inverse(multiply(X1,X2))) = multiply(multiply(inverse(c3),sF2),inverse(multiply(b3,X2))),
    inference(backward_demodulation,[],[f103553,f103612]) ).

fof(f103651,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(multiply(X1,X0),inverse(X0)))) = multiply(multiply(inverse(c3),sF2),inverse(multiply(b3,multiply(inverse(X2),multiply(X1,X2))))),
    inference(backward_demodulation,[],[f102944,f103619]) ).

fof(f103653,plain,
    ! [X0] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),inverse(X0)) = multiply(multiply(inverse(c3),sF2),inverse(multiply(b3,multiply(multiply(b3,a3),inverse(sF0))))),
    inference(backward_demodulation,[],[f98741,f103619]) ).

fof(f103654,plain,
    ! [X0,X1] : multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),X1),inverse(X1)) = multiply(multiply(multiply(inverse(c3),sF2),inverse(multiply(b3,multiply(multiply(b3,a3),inverse(sF0))))),inverse(inverse(X0))),
    inference(backward_demodulation,[],[f97582,f103619]) ).

fof(f103682,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(c3),sF2),inverse(multiply(b3,multiply(inverse(X2),multiply(X1,X2))))) = multiply(multiply(inverse(c3),sF2),inverse(multiply(b3,multiply(inverse(X0),multiply(X1,X0))))),
    inference(forward_demodulation,[],[f103651,f103619]) ).

fof(f103760,plain,
    ! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(inverse(X0)))))) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,X0))),
    inference(superposition,[],[f100845,f103470]) ).

fof(f103766,plain,
    ! [X0] : multiply(multiply(inverse(c3),sF2),inverse(multiply(b3,X0))) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,X0))),
    inference(backward_demodulation,[],[f103612,f103760]) ).

fof(f103777,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(X0),multiply(X1,X0)),inverse(multiply(X1,X2))) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,X2))),
    inference(backward_demodulation,[],[f103620,f103766]) ).

fof(f103779,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(X1,X0))) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(X0,X1)))),
    inference(backward_demodulation,[],[f103619,f103766]) ).

fof(f103781,plain,
    ! [X0] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),inverse(X0)) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(multiply(b3,a3),inverse(sF0))))),
    inference(backward_demodulation,[],[f103653,f103766]) ).

fof(f103782,plain,
    ! [X0,X1] : multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),X1),inverse(X1)) = multiply(multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(multiply(b3,a3),inverse(sF0))))),inverse(inverse(X0))),
    inference(backward_demodulation,[],[f103654,f103766]) ).

fof(f103789,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(c3),sF2),inverse(multiply(b3,multiply(inverse(X0),multiply(X1,X0))))) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(inverse(X2),multiply(X1,X2))))),
    inference(backward_demodulation,[],[f103682,f103766]) ).

fof(f103800,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(inverse(X2),multiply(X1,X2))))) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(inverse(X0),multiply(X1,X0))))),
    inference(forward_demodulation,[],[f103789,f103766]) ).

fof(f103828,plain,
    ! [X0,X1] : multiply(multiply(inverse(X0),X1),inverse(X1)) = multiply(multiply(inverse(c3),sF1),inverse(multiply(sF0,X0))),
    inference(superposition,[],[f4725,f103472]) ).

fof(f103851,plain,
    ! [X0,X1] : inverse(multiply(inverse(X0),multiply(inverse(X1),X0))) = inverse(multiply(inverse(multiply(sF0,X1)),multiply(inverse(c3),sF1))),
    inference(superposition,[],[f102945,f103472]) ).

fof(f103934,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(X1),X2),inverse(X2)) = multiply(multiply(inverse(inverse(inverse(X0))),X0),inverse(multiply(multiply(sF0,inverse(multiply(sF1,inverse(c3)))),X1))),
    inference(superposition,[],[f103533,f100338]) ).

fof(f103951,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(inverse(X2),X3),inverse(X3)) = multiply(multiply(inverse(inverse(inverse(inverse(inverse(X0))))),multiply(multiply(X0,X1),inverse(X1))),inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),X2))),
    inference(superposition,[],[f103533,f100845]) ).

fof(f104030,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(inverse(inverse(inverse(inverse(inverse(X0))))),X3),inverse(X3)) = multiply(multiply(inverse(X2),multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),X2)),inverse(multiply(multiply(X0,X1),inverse(X1)))),
    inference(superposition,[],[f103533,f100845]) ).

fof(f104031,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF0),X1),inverse(X1)) = multiply(multiply(inverse(X0),multiply(inverse(multiply(b3,a3)),X0)),inverse(multiply(inverse(sF0),multiply(b3,a3)))),
    inference(superposition,[],[f103533,f93493]) ).

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

fof(f104490,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),X0) = multiply(inverse(inverse(multiply(X0,inverse(X1)))),multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X2),inverse(X2))),
    inference(superposition,[],[f103417,f95455]) ).

fof(f104492,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X1)),multiply(multiply(X0,X2),inverse(X2))) = multiply(inverse(inverse(inverse(inverse(multiply(X0,X1))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3)))))),
    inference(superposition,[],[f103417,f100837]) ).

fof(f104631,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(X1,X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),inverse(inverse(X3))) = multiply(multiply(multiply(multiply(inverse(inverse(X0)),multiply(multiply(X1,X2),inverse(X2))),X3),X4),inverse(X4)),
    inference(superposition,[],[f93868,f103417]) ).

fof(f104736,plain,
    ! [X0,X1] : multiply(inverse(X1),X0) = multiply(inverse(inverse(multiply(X0,inverse(X1)))),multiply(sF0,inverse(multiply(sF1,inverse(c3))))),
    inference(forward_demodulation,[],[f104490,f100839]) ).

fof(f105391,plain,
    ! [X0,X1] : multiply(inverse(inverse(inverse(X1))),X1) = multiply(inverse(inverse(multiply(X0,inverse(inverse(inverse(X0)))))),multiply(sF0,inverse(multiply(sF1,inverse(c3))))),
    inference(superposition,[],[f104736,f97938]) ).

fof(f105392,plain,
    ! [X0,X1] : multiply(inverse(multiply(multiply(X0,X1),inverse(X1))),X0) = multiply(inverse(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3)))))),multiply(sF0,inverse(multiply(sF1,inverse(c3))))),
    inference(superposition,[],[f104736,f100846]) ).

fof(f105473,plain,
    ! [X0,X1] : multiply(multiply(inverse(X0),X1),inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3)))))) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(inverse(inverse(multiply(X1,inverse(X0))))))))),
    inference(superposition,[],[f100845,f104736]) ).

fof(f105484,plain,
    ! [X0,X1] : multiply(multiply(inverse(X0),X1),inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3)))))) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,inverse(multiply(X1,inverse(X0)))))),
    inference(forward_demodulation,[],[f105473,f103760]) ).

fof(f105547,plain,
    ! [X0,X1] : multiply(inverse(multiply(multiply(X0,X1),inverse(X1))),X0) = multiply(inverse(multiply(sF1,inverse(c3))),sF0),
    inference(forward_demodulation,[],[f105392,f104736]) ).

fof(f105548,plain,
    ! [X0,X1] : multiply(inverse(inverse(inverse(X1))),X1) = multiply(inverse(inverse(inverse(X0))),X0),
    inference(forward_demodulation,[],[f105391,f104736]) ).

fof(f105558,plain,
    ! [X1] : multiply(inverse(multiply(sF1,inverse(c3))),sF0) = multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X1)),
    inference(backward_demodulation,[],[f103457,f105547]) ).

fof(f105637,plain,
    ! [X0,X1] : inverse(inverse(inverse(inverse(X1)))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(inverse(inverse(inverse(X0))),X0)),X1),
    inference(superposition,[],[f95455,f105548]) ).

fof(f105665,plain,
    ! [X0,X1] : multiply(multiply(inverse(inverse(inverse(X0))),X0),inverse(X1)) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(inverse(inverse(inverse(X1)))))))),
    inference(superposition,[],[f100845,f105548]) ).

fof(f105675,plain,
    ! [X0,X1] : multiply(multiply(inverse(inverse(inverse(X0))),X0),inverse(X1)) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,inverse(inverse(X1))))),
    inference(forward_demodulation,[],[f105665,f103760]) ).

fof(f106244,plain,
    ! [X0,X1] : multiply(inverse(multiply(b3,X0)),multiply(inverse(c3),sF2)) = multiply(inverse(inverse(inverse(inverse(inverse(X0))))),multiply(X1,inverse(inverse(inverse(X1))))),
    inference(superposition,[],[f103412,f103471]) ).

fof(f106245,plain,
    ! [X0,X1] : multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)) = multiply(inverse(inverse(inverse(inverse(inverse(X0))))),multiply(X1,inverse(inverse(inverse(X1))))),
    inference(superposition,[],[f103412,f103472]) ).

fof(f106248,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(inverse(sF0),multiply(b3,a3))) = multiply(inverse(inverse(inverse(inverse(inverse(multiply(X1,X0)))))),multiply(X2,inverse(inverse(inverse(X2))))),
    inference(superposition,[],[f103412,f93254]) ).

fof(f106254,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(inverse(inverse(inverse(X0))))),multiply(multiply(X0,X1),inverse(X1))) = multiply(inverse(inverse(inverse(inverse(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))))))),multiply(X2,inverse(inverse(inverse(X2))))),
    inference(superposition,[],[f103412,f100845]) ).

fof(f106448,plain,
    ! [X0,X1] : multiply(inverse(inverse(inverse(inverse(inverse(X0))))),multiply(multiply(X0,X1),inverse(X1))) = multiply(inverse(multiply(inverse(multiply(sF1,inverse(c3))),sF0)),multiply(inverse(sF0),multiply(b3,a3))),
    inference(backward_demodulation,[],[f106254,f106248]) ).

fof(f106459,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(inverse(sF0),multiply(b3,a3))) = multiply(inverse(multiply(sF0,multiply(X1,X0))),multiply(inverse(c3),sF1)),
    inference(backward_demodulation,[],[f106248,f106245]) ).

fof(f106460,plain,
    ! [X0] : multiply(inverse(multiply(b3,X0)),multiply(inverse(c3),sF2)) = multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)),
    inference(forward_demodulation,[],[f106244,f106245]) ).

fof(f107870,plain,
    ! [X0,X1] : multiply(multiply(a3,X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))) = multiply(multiply(multiply(inverse(inverse(X0)),multiply(sF0,inverse(b3))),X1),inverse(X1)),
    inference(superposition,[],[f93869,f103441]) ).

fof(f108273,plain,
    ! [X0,X1] : multiply(inverse(inverse(inverse(inverse(inverse(X0))))),multiply(multiply(X0,X1),inverse(X1))) = multiply(inverse(inverse(inverse(inverse(inverse(a3))))),multiply(sF0,inverse(b3))),
    inference(superposition,[],[f103417,f98272]) ).

fof(f108307,plain,
    ! [X0,X1] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(multiply(inverse(X0),multiply(multiply(X1,inverse(inverse(inverse(X1)))),X0))),multiply(multiply(sF0,inverse(b3)),inverse(inverse(inverse(inverse(inverse(a3))))))),
    inference(superposition,[],[f93445,f98272]) ).

fof(f108342,plain,
    multiply(inverse(multiply(inverse(multiply(sF1,inverse(c3))),sF0)),multiply(inverse(sF0),multiply(b3,a3))) = multiply(inverse(inverse(inverse(inverse(inverse(a3))))),multiply(sF0,inverse(b3))),
    inference(backward_demodulation,[],[f106448,f108273]) ).

fof(f108343,plain,
    ! [X2,X3] : multiply(multiply(inverse(X2),X3),inverse(X3)) = multiply(multiply(inverse(inverse(inverse(inverse(inverse(a3))))),multiply(sF0,inverse(b3))),inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),X2))),
    inference(backward_demodulation,[],[f103951,f108273]) ).

fof(f108344,plain,
    ! [X2] : multiply(inverse(X2),multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),X2)) = multiply(inverse(inverse(inverse(inverse(inverse(a3))))),multiply(sF0,inverse(b3))),
    inference(backward_demodulation,[],[f103459,f108273]) ).

fof(f108373,plain,
    ! [X3,X0,X1] : multiply(multiply(inverse(inverse(inverse(inverse(inverse(X0))))),X3),inverse(X3)) = multiply(multiply(inverse(inverse(inverse(inverse(inverse(a3))))),multiply(sF0,inverse(b3))),inverse(multiply(multiply(X0,X1),inverse(X1)))),
    inference(backward_demodulation,[],[f104030,f108344]) ).

fof(f108577,plain,
    ! [X0,X1] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(multiply(a3,X0),inverse(X0))),b3) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(sF0,inverse(multiply(sF1,inverse(c3))))))),X1),inverse(X1)),
    inference(superposition,[],[f93878,f100846]) ).

fof(f108749,plain,
    ! [X1] : multiply(a3,b3) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(sF0,inverse(multiply(sF1,inverse(c3))))))),X1),inverse(X1)),
    inference(forward_demodulation,[],[f108577,f95478]) ).

fof(f108768,plain,
    ! [X1] : sF0 = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(sF0,inverse(multiply(sF1,inverse(c3))))))),X1),inverse(X1)),
    inference(forward_demodulation,[],[f108749,f4]) ).

fof(f108780,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(multiply(X0,inverse(inverse(inverse(X0)))),X1)) = multiply(inverse(multiply(b3,multiply(sF0,inverse(multiply(sF1,inverse(c3)))))),multiply(inverse(c3),sF2)),
    inference(superposition,[],[f103617,f100837]) ).

fof(f108801,plain,
    ! [X0,X1] : multiply(inverse(multiply(multiply(X0,X1),inverse(X1))),X0) = multiply(inverse(multiply(b3,multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))))),multiply(inverse(c3),sF2)),
    inference(superposition,[],[f103617,f95478]) ).

fof(f108818,plain,
    ! [X0] : multiply(inverse(multiply(b3,X0)),multiply(inverse(c3),sF2)) = multiply(inverse(inverse(inverse(inverse(inverse(X0))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3)))))),
    inference(superposition,[],[f103617,f100837]) ).

fof(f108847,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X1)),inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))))))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(inverse(multiply(b3,X0)),multiply(inverse(c3),sF2))),X1),
    inference(superposition,[],[f96424,f103617]) ).

fof(f108848,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))) = multiply(multiply(multiply(inverse(multiply(b3,X0)),multiply(inverse(c3),sF2)),X1),inverse(X1)),
    inference(superposition,[],[f93869,f103617]) ).

fof(f108886,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(inverse(inverse(inverse(X1))))),multiply(X2,inverse(inverse(inverse(X2))))) = multiply(inverse(multiply(inverse(X0),X1)),multiply(inverse(multiply(b3,X0)),multiply(inverse(c3),sF2))),
    inference(superposition,[],[f103412,f103617]) ).

fof(f108891,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(inverse(X0),X2)),X3),inverse(X3)) = multiply(multiply(inverse(X1),multiply(inverse(X2),X1)),inverse(multiply(inverse(multiply(b3,X0)),multiply(inverse(c3),sF2)))),
    inference(superposition,[],[f103533,f103617]) ).

fof(f108950,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(inverse(X0),X2)),X3),inverse(X3)) = multiply(multiply(inverse(X1),multiply(inverse(X2),X1)),inverse(multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)))),
    inference(forward_demodulation,[],[f108891,f106460]) ).

fof(f108955,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(inverse(inverse(inverse(X1))))),multiply(X2,inverse(inverse(inverse(X2))))) = multiply(inverse(multiply(inverse(X0),X1)),multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1))),
    inference(forward_demodulation,[],[f108886,f106460]) ).

fof(f108992,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))) = multiply(multiply(multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)),X1),inverse(X1)),
    inference(forward_demodulation,[],[f108848,f106460]) ).

fof(f108993,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X1)),inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))))))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1))),X1),
    inference(forward_demodulation,[],[f108847,f106460]) ).

fof(f109013,plain,
    ! [X0] : multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)) = multiply(inverse(inverse(inverse(inverse(inverse(X0))))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3)))))),
    inference(forward_demodulation,[],[f108818,f106460]) ).

fof(f109030,plain,
    ! [X0,X1] : multiply(inverse(multiply(multiply(X0,X1),inverse(X1))),X0) = multiply(inverse(multiply(sF0,multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))))),multiply(inverse(c3),sF1)),
    inference(forward_demodulation,[],[f108801,f106460]) ).

fof(f109050,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(multiply(X0,inverse(inverse(inverse(X0)))),X1)) = multiply(inverse(multiply(sF0,multiply(sF0,inverse(multiply(sF1,inverse(c3)))))),multiply(inverse(c3),sF1)),
    inference(forward_demodulation,[],[f108780,f106460]) ).

fof(f109055,plain,
    ! [X0,X1] : multiply(inverse(multiply(sF0,X1)),multiply(inverse(c3),sF1)) = multiply(inverse(multiply(inverse(X0),X1)),multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1))),
    inference(forward_demodulation,[],[f108955,f106245]) ).

fof(f109097,plain,
    ! [X0,X1] : multiply(inverse(multiply(multiply(X0,X1),inverse(X1))),X0) = multiply(inverse(multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(inverse(sF0),multiply(b3,a3))))),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f109030,f106459]) ).

fof(f109105,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(multiply(X0,inverse(inverse(inverse(X0)))),X1)) = multiply(inverse(multiply(inverse(multiply(sF1,inverse(c3))),sF0)),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f109050,f106459]) ).

fof(f109116,plain,
    ! [X0,X1] : multiply(inverse(multiply(multiply(X0,X1),inverse(X1))),X0) = multiply(inverse(multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(multiply(b3,a3),inverse(sF0)))))),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f109097,f103779]) ).

fof(f109121,plain,
    multiply(inverse(multiply(sF1,inverse(c3))),sF0) = multiply(inverse(multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(multiply(b3,a3),inverse(sF0)))))),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f109116,f105547]) ).

fof(f109304,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X1))),X2),inverse(X2)) = multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(multiply(inverse(c3),sF1),inverse(multiply(sF0,X0))))),
    inference(superposition,[],[f93526,f103828]) ).

fof(f109526,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X4),inverse(X4)),inverse(inverse(inverse(multiply(X1,X0))))) = multiply(multiply(multiply(multiply(inverse(multiply(X0,X1)),X2),inverse(X2)),X3),inverse(X3)),
    inference(superposition,[],[f4784,f93526]) ).

fof(f109761,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X1))),X2),inverse(X2)) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1))))),
    inference(forward_demodulation,[],[f109304,f103779]) ).

fof(f110430,plain,
    ! [X0] : multiply(inverse(inverse(sF2)),multiply(sF0,inverse(b3))) = multiply(multiply(X0,inverse(inverse(inverse(X0)))),multiply(sF3,multiply(sF0,inverse(multiply(sF1,inverse(c3)))))),
    inference(superposition,[],[f103473,f100837]) ).

fof(f111365,plain,
    multiply(inverse(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3)))))),multiply(sF0,inverse(multiply(sF1,inverse(c3))))) = multiply(inverse(multiply(sF2,inverse(c3))),b3),
    inference(superposition,[],[f104736,f100885]) ).

fof(f111384,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(multiply(inverse(multiply(sF2,inverse(c3))),b3)),multiply(sF0,inverse(multiply(sF1,inverse(c3))))),
    inference(superposition,[],[f93254,f100885]) ).

fof(f111423,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(sF2,inverse(c3))),b3),inverse(b3))))),
    inference(forward_demodulation,[],[f111384,f101506]) ).

fof(f111441,plain,
    multiply(inverse(multiply(sF1,inverse(c3))),sF0) = multiply(inverse(multiply(sF2,inverse(c3))),b3),
    inference(forward_demodulation,[],[f111365,f104736]) ).

fof(f111463,plain,
    ! [X0,X1] : multiply(inverse(multiply(multiply(X0,X1),inverse(X1))),X0) = multiply(inverse(multiply(sF2,inverse(c3))),b3),
    inference(backward_demodulation,[],[f105547,f111441]) ).

fof(f111466,plain,
    ! [X1] : multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X1)) = multiply(inverse(multiply(sF2,inverse(c3))),b3),
    inference(backward_demodulation,[],[f105558,f111441]) ).

fof(f111476,plain,
    multiply(inverse(inverse(inverse(inverse(inverse(a3))))),multiply(sF0,inverse(b3))) = multiply(inverse(multiply(inverse(multiply(sF2,inverse(c3))),b3)),multiply(inverse(sF0),multiply(b3,a3))),
    inference(backward_demodulation,[],[f108342,f111441]) ).

fof(f111477,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(multiply(X0,inverse(inverse(inverse(X0)))),X1)) = multiply(inverse(multiply(inverse(multiply(sF2,inverse(c3))),b3)),multiply(inverse(sF0),multiply(b3,a3))),
    inference(backward_demodulation,[],[f109105,f111441]) ).

fof(f111478,plain,
    multiply(inverse(multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(multiply(b3,a3),inverse(sF0)))))),multiply(inverse(sF0),multiply(b3,a3))) = multiply(inverse(multiply(sF2,inverse(c3))),b3),
    inference(backward_demodulation,[],[f109121,f111441]) ).

fof(f111662,plain,
    multiply(inverse(multiply(sF2,inverse(c3))),b3) = multiply(inverse(multiply(sF0,inverse(b3))),a3),
    inference(superposition,[],[f111463,f4762]) ).

fof(f111689,plain,
    ! [X0,X1] : multiply(inverse(X0),inverse(multiply(multiply(inverse(X0),X1),inverse(X1)))) = multiply(inverse(inverse(multiply(inverse(multiply(sF2,inverse(c3))),b3))),multiply(sF0,inverse(multiply(sF1,inverse(c3))))),
    inference(superposition,[],[f104736,f111463]) ).

fof(f111748,plain,
    multiply(sF0,inverse(multiply(sF1,inverse(c3)))) = multiply(inverse(inverse(multiply(inverse(multiply(sF2,inverse(c3))),b3))),multiply(sF0,inverse(multiply(sF1,inverse(c3))))),
    inference(forward_demodulation,[],[f111689,f100846]) ).

fof(f111759,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(sF0,inverse(b3))),a3),inverse(b3))))),
    inference(backward_demodulation,[],[f111423,f111662]) ).

fof(f111766,plain,
    ! [X1] : multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),X1)) = multiply(inverse(multiply(sF0,inverse(b3))),a3),
    inference(backward_demodulation,[],[f111466,f111662]) ).

fof(f111774,plain,
    multiply(inverse(inverse(inverse(inverse(inverse(a3))))),multiply(sF0,inverse(b3))) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),multiply(inverse(sF0),multiply(b3,a3))),
    inference(backward_demodulation,[],[f111476,f111662]) ).

fof(f111775,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(multiply(X0,inverse(inverse(inverse(X0)))),X1)) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),multiply(inverse(sF0),multiply(b3,a3))),
    inference(backward_demodulation,[],[f111477,f111662]) ).

fof(f111776,plain,
    multiply(inverse(multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(multiply(b3,a3),inverse(sF0)))))),multiply(inverse(sF0),multiply(b3,a3))) = multiply(inverse(multiply(sF0,inverse(b3))),a3),
    inference(backward_demodulation,[],[f111478,f111662]) ).

fof(f111973,plain,
    multiply(sF0,inverse(multiply(sF1,inverse(c3)))) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3))),multiply(sF0,inverse(multiply(sF1,inverse(c3))))),
    inference(forward_demodulation,[],[f111748,f111662]) ).

fof(f112646,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X0),multiply(inverse(inverse(multiply(multiply(X1,X2),inverse(X2)))),X0)) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),multiply(inverse(X3),multiply(X1,X3))),
    inference(superposition,[],[f103452,f100846]) ).

fof(f112687,plain,
    ! [X2,X3,X0,X1,X4] : multiply(inverse(X3),multiply(inverse(inverse(multiply(X1,X0))),X3)) = multiply(inverse(multiply(multiply(inverse(multiply(X0,X1)),X2),inverse(X2))),multiply(inverse(X4),multiply(multiply(inverse(sF0),multiply(b3,a3)),X4))),
    inference(superposition,[],[f103452,f93526]) ).

fof(f112983,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X1)),inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))))))))) = multiply(multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),X1),
    inference(superposition,[],[f96424,f103452]) ).

fof(f112985,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X1)) = multiply(multiply(multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),X2),inverse(X2)),
    inference(superposition,[],[f93869,f103452]) ).

fof(f112986,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(inverse(X1),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X1)),inverse(inverse(X2))) = multiply(multiply(multiply(multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),X2),X3),inverse(X3)),
    inference(superposition,[],[f93868,f103452]) ).

fof(f113087,plain,
    ! [X0,X1] : multiply(multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),X1) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(inverse(multiply(sF0,multiply(inverse(sF0),multiply(b3,a3)))),multiply(inverse(c3),sF1))),X1),
    inference(forward_demodulation,[],[f112983,f108993]) ).

fof(f113302,plain,
    ! [X0,X1] : multiply(multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),X1) = multiply(multiply(inverse(multiply(sF0,multiply(inverse(sF0),multiply(b3,a3)))),multiply(inverse(c3),sF1)),X1),
    inference(forward_demodulation,[],[f113087,f109055]) ).

fof(f113380,plain,
    ! [X0,X1] : multiply(multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),X1) = multiply(multiply(inverse(multiply(multiply(b3,a3),inverse(sF0))),multiply(inverse(sF0),multiply(b3,a3))),X1),
    inference(forward_demodulation,[],[f113302,f106459]) ).

fof(f113391,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF0),multiply(b3,a3)),X1) = multiply(multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0)),X1),
    inference(forward_demodulation,[],[f113380,f93254]) ).

fof(f113395,plain,
    ! [X2,X1] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X2),inverse(X2)) = multiply(inverse(X1),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X1)),
    inference(backward_demodulation,[],[f112985,f113391]) ).

fof(f113396,plain,
    ! [X2,X3,X1] : multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X2),X3),inverse(X3)) = multiply(multiply(inverse(X1),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X1)),inverse(inverse(X2))),
    inference(backward_demodulation,[],[f112986,f113391]) ).

fof(f113397,plain,
    ! [X2,X3] : multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X2),X3),inverse(X3)) = multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(inverse(X2))),
    inference(forward_demodulation,[],[f113396,f113391]) ).

fof(f113399,plain,
    ! [X0] : multiply(multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(multiply(b3,a3),inverse(sF0))))),inverse(inverse(X0))) = multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(inverse(X0))),
    inference(backward_demodulation,[],[f103782,f113397]) ).

fof(f113496,plain,
    ! [X0] : multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(multiply(b3,a3),inverse(sF0))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3)))),multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(inverse(X0))),inverse(inverse(inverse(X0))))),
    inference(superposition,[],[f95478,f113399]) ).

fof(f113528,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(multiply(b3,a3),inverse(sF0))))),
    inference(forward_demodulation,[],[f113496,f95478]) ).

fof(f113582,plain,
    ! [X0] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),inverse(X0)),
    inference(backward_demodulation,[],[f103781,f113528]) ).

fof(f113592,plain,
    multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))) = multiply(inverse(multiply(sF0,inverse(b3))),a3),
    inference(backward_demodulation,[],[f111776,f113528]) ).

fof(f113648,plain,
    ! [X2,X3] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),X2),X3),inverse(X3)) = X2,
    inference(backward_demodulation,[],[f93869,f113592]) ).

fof(f114043,plain,
    ! [X3,X0,X6,X4,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))),X6),inverse(X6)) = multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(X0,X5),inverse(X5)),inverse(b3))))))),X4),
    inference(backward_demodulation,[],[f95443,f113592]) ).

fof(f114316,plain,
    ! [X0,X4] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X4)),inverse(X0))))) = multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),X0)),X4),
    inference(backward_demodulation,[],[f96424,f113592]) ).

fof(f114549,plain,
    multiply(multiply(sF0,inverse(b3)),inverse(inverse(inverse(inverse(inverse(a3)))))) = inverse(inverse(inverse(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3))))),
    inference(backward_demodulation,[],[f99058,f113592]) ).

fof(f114605,plain,
    ! [X0] : multiply(sF0,inverse(multiply(sF1,inverse(c3)))) = multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),X0),inverse(X0)),
    inference(backward_demodulation,[],[f100839,f113592]) ).

fof(f114632,plain,
    ! [X0,X1] : multiply(X0,inverse(inverse(X1))) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),X0),X1)))))),
    inference(backward_demodulation,[],[f101306,f113592]) ).

fof(f114642,plain,
    multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(multiply(sF0,inverse(b3))),a3),inverse(b3))))) = inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),
    inference(backward_demodulation,[],[f101615,f113592]) ).

fof(f114661,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(sF0,inverse(b3))),multiply(multiply(a3,inverse(X2)),inverse(multiply(X1,multiply(inverse(multiply(sF0,inverse(b3))),a3))))))) = multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),multiply(inverse(X0),multiply(X1,X0))),X2),
    inference(backward_demodulation,[],[f103522,f113592]) ).

fof(f114662,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(inverse(X0),multiply(X1,X0)),X2),inverse(X2)) = multiply(X1,multiply(inverse(multiply(sF0,inverse(b3))),a3)),
    inference(backward_demodulation,[],[f103523,f113592]) ).

fof(f114690,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(multiply(inverse(inverse(X0)),multiply(multiply(X1,X2),inverse(X2))),X3),X4),inverse(X4)) = multiply(multiply(multiply(X1,X0),multiply(inverse(multiply(sF0,inverse(b3))),a3)),inverse(inverse(X3))),
    inference(backward_demodulation,[],[f104631,f113592]) ).

fof(f114715,plain,
    ! [X0,X1] : inverse(inverse(inverse(inverse(X1)))) = multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),multiply(inverse(inverse(inverse(X0))),X0)),X1),
    inference(backward_demodulation,[],[f105637,f113592]) ).

fof(f114739,plain,
    ! [X0,X1] : multiply(multiply(multiply(inverse(inverse(X0)),multiply(sF0,inverse(b3))),X1),inverse(X1)) = multiply(multiply(a3,X0),multiply(inverse(multiply(sF0,inverse(b3))),a3)),
    inference(backward_demodulation,[],[f107870,f113592]) ).

fof(f114774,plain,
    ! [X0,X1] : multiply(multiply(multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)),X1),inverse(X1)) = multiply(inverse(X0),multiply(inverse(multiply(sF0,inverse(b3))),a3)),
    inference(backward_demodulation,[],[f108992,f113592]) ).

fof(f114832,plain,
    ! [X1] : multiply(inverse(multiply(sF0,inverse(b3))),a3) = multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),X1)),
    inference(backward_demodulation,[],[f111766,f113592]) ).

fof(f114876,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(multiply(multiply(inverse(multiply(X0,X1)),X2),inverse(X2)),X3),inverse(X3)) = multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(inverse(inverse(multiply(X1,X0))))),
    inference(backward_demodulation,[],[f109526,f113582]) ).

fof(f114882,plain,
    ! [X1] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(X1),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X1)),
    inference(backward_demodulation,[],[f113395,f113582]) ).

fof(f115054,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),
    inference(forward_demodulation,[],[f114642,f111759]) ).

fof(f115299,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),multiply(inverse(X0),multiply(X1,X0))),X2) = multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),multiply(X1,multiply(inverse(multiply(sF0,inverse(b3))),a3)))),X2),
    inference(backward_demodulation,[],[f114661,f114316]) ).

fof(f115588,plain,
    multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(sF0),multiply(b3,a3))) = multiply(inverse(inverse(inverse(inverse(inverse(a3))))),multiply(sF0,inverse(b3))),
    inference(backward_demodulation,[],[f111774,f115054]) ).

fof(f115589,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(sF0),multiply(b3,a3))) = multiply(inverse(X1),multiply(multiply(X0,inverse(inverse(inverse(X0)))),X1)),
    inference(backward_demodulation,[],[f111775,f115054]) ).

fof(f115593,plain,
    multiply(sF0,inverse(multiply(sF1,inverse(c3)))) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(sF0,inverse(multiply(sF1,inverse(c3))))),
    inference(backward_demodulation,[],[f111973,f115054]) ).

fof(f115596,plain,
    ! [X2,X3] : multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X2),X3),inverse(X3)) = X2,
    inference(backward_demodulation,[],[f113648,f115054]) ).

fof(f115874,plain,
    ! [X3,X0,X6,X4,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))),X6),inverse(X6)) = multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(multiply(X0,X5),inverse(X5)),inverse(b3))))))),X4),
    inference(backward_demodulation,[],[f114043,f115054]) ).

fof(f116254,plain,
    inverse(inverse(inverse(multiply(inverse(sF0),multiply(b3,a3))))) = multiply(multiply(sF0,inverse(b3)),inverse(inverse(inverse(inverse(inverse(a3)))))),
    inference(backward_demodulation,[],[f114549,f115054]) ).

fof(f116300,plain,
    ! [X0] : multiply(sF0,inverse(multiply(sF1,inverse(c3)))) = multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),inverse(X0)),
    inference(backward_demodulation,[],[f114605,f115054]) ).

fof(f116326,plain,
    ! [X0,X1] : multiply(X0,inverse(inverse(X1))) = multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),inverse(inverse(inverse(inverse(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),X1)))))),
    inference(backward_demodulation,[],[f114632,f115054]) ).

fof(f116361,plain,
    ! [X0,X1] : inverse(inverse(inverse(inverse(X1)))) = multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(inverse(inverse(X0))),X0)),X1),
    inference(backward_demodulation,[],[f114715,f115054]) ).

fof(f116447,plain,
    ! [X1] : multiply(inverse(multiply(sF0,inverse(b3))),a3) = multiply(inverse(X1),multiply(multiply(inverse(sF0),multiply(b3,a3)),X1)),
    inference(backward_demodulation,[],[f114832,f115054]) ).

fof(f116538,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),multiply(inverse(X0),multiply(X1,X0))),X2) = multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(b3))),a3)),multiply(inverse(inverse(inverse(inverse(X1)))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))))),X2),
    inference(forward_demodulation,[],[f115299,f103410]) ).

fof(f116990,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X3),multiply(inverse(inverse(multiply(X1,X0))),X3)) = multiply(inverse(multiply(multiply(inverse(multiply(X0,X1)),X2),inverse(X2))),multiply(inverse(multiply(sF0,inverse(b3))),a3)),
    inference(backward_demodulation,[],[f112687,f116447]) ).

fof(f116999,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(sF0,inverse(multiply(sF1,inverse(c3)))),
    inference(forward_demodulation,[],[f116300,f113582]) ).

fof(f117005,plain,
    ! [X0,X1] : multiply(multiply(multiply(inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))),X0),X1),inverse(X1)) = multiply(inverse(inverse(inverse(multiply(inverse(sF0),multiply(b3,a3))))),inverse(inverse(X0))),
    inference(backward_demodulation,[],[f101364,f116254]) ).

fof(f117015,plain,
    ! [X0,X1] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(multiply(inverse(X0),multiply(multiply(X1,inverse(inverse(inverse(X1)))),X0))),inverse(inverse(inverse(multiply(inverse(sF0),multiply(b3,a3)))))),
    inference(backward_demodulation,[],[f108307,f116254]) ).

fof(f117464,plain,
    ! [X2] : multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(inverse(X2))) = X2,
    inference(backward_demodulation,[],[f113397,f115596]) ).

fof(f117465,plain,
    multiply(sF0,inverse(multiply(sF1,inverse(c3)))) = multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(b3))))),
    inference(forward_demodulation,[],[f115593,f101506]) ).

fof(f117467,plain,
    ! [X0,X1] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(X1),multiply(multiply(X0,inverse(inverse(inverse(X0)))),X1)),
    inference(forward_demodulation,[],[f115589,f97283]) ).

fof(f117468,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(inverse(inverse(inverse(inverse(a3))))),multiply(sF0,inverse(b3))),
    inference(forward_demodulation,[],[f115588,f97283]) ).

fof(f117509,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(X0),multiply(X1,X0))),X2) = multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(inverse(inverse(inverse(X1)))),inverse(multiply(sF0,inverse(multiply(sF1,inverse(c3))))))),X2),
    inference(forward_demodulation,[],[f116538,f115054]) ).

fof(f117862,plain,
    ! [X2,X0] : multiply(multiply(X0,X2),inverse(X2)) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(inverse(inverse(X0))))),
    inference(backward_demodulation,[],[f100845,f116999]) ).

fof(f117864,plain,
    ! [X2,X0] : multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X2) = multiply(multiply(X0,inverse(inverse(inverse(X0)))),X2),
    inference(backward_demodulation,[],[f100856,f116999]) ).

fof(f117889,plain,
    ! [X2,X1] : multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X1),X2),inverse(X2)) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(X1))),
    inference(backward_demodulation,[],[f100971,f116999]) ).

fof(f117893,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(X0,X1),inverse(X1)),X2) = multiply(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(inverse(inverse(X0))))),X2),
    inference(backward_demodulation,[],[f101280,f116999]) ).

fof(f117894,plain,
    ! [X0] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(inverse(multiply(inverse(sF0),multiply(b3,a3)))),multiply(inverse(inverse(inverse(X0))),X0)),
    inference(backward_demodulation,[],[f101281,f116999]) ).

fof(f117900,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(X0,X2),inverse(X2)),inverse(inverse(X1))) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(inverse(inverse(multiply(X0,X1)))))),
    inference(backward_demodulation,[],[f101305,f116999]) ).

fof(f117911,plain,
    ! [X0,X1] : multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(X0,X1),inverse(b3))))) = multiply(inverse(multiply(X0,X1)),multiply(inverse(sF0),multiply(b3,a3))),
    inference(backward_demodulation,[],[f101506,f116999]) ).

fof(f117914,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2))),inverse(inverse(X3))) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(inverse(inverse(multiply(multiply(X0,X2),X3)))))),
    inference(backward_demodulation,[],[f102015,f116999]) ).

fof(f117926,plain,
    multiply(sF0,inverse(b3)) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(inverse(inverse(a3))))),
    inference(backward_demodulation,[],[f102090,f116999]) ).

fof(f117946,plain,
    ! [X0,X1] : inverse(multiply(inverse(X0),multiply(X1,X0))) = inverse(multiply(inverse(inverse(inverse(inverse(X1)))),inverse(multiply(inverse(sF0),multiply(b3,a3))))),
    inference(backward_demodulation,[],[f103083,f116999]) ).

fof(f117953,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(multiply(X0,X2),X1)) = multiply(inverse(inverse(X2)),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(inverse(inverse(X0)))))),
    inference(backward_demodulation,[],[f103415,f116999]) ).

fof(f117954,plain,
    ! [X0,X1] : multiply(inverse(inverse(inverse(X0))),X0) = multiply(inverse(X1),multiply(multiply(inverse(sF0),multiply(b3,a3)),X1)),
    inference(backward_demodulation,[],[f103445,f116999]) ).

fof(f117958,plain,
    ! [X0] : multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,X0))) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(inverse(inverse(inverse(X0)))))),
    inference(backward_demodulation,[],[f103760,f116999]) ).

fof(f117966,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(X1),X2),inverse(X2)) = multiply(multiply(inverse(inverse(inverse(X0))),X0),inverse(multiply(multiply(inverse(sF0),multiply(b3,a3)),X1))),
    inference(backward_demodulation,[],[f103934,f116999]) ).

fof(f117976,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X1)),multiply(multiply(X0,X2),inverse(X2))) = multiply(inverse(inverse(inverse(inverse(multiply(X0,X1))))),inverse(multiply(inverse(sF0),multiply(b3,a3)))),
    inference(backward_demodulation,[],[f104492,f116999]) ).

fof(f117995,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,inverse(multiply(X1,inverse(X0)))))) = multiply(multiply(inverse(X0),X1),inverse(multiply(inverse(sF0),multiply(b3,a3)))),
    inference(backward_demodulation,[],[f105484,f116999]) ).

fof(f118014,plain,
    ! [X2,X3] : multiply(multiply(inverse(X2),X3),inverse(X3)) = multiply(multiply(inverse(inverse(inverse(inverse(inverse(a3))))),multiply(sF0,inverse(b3))),inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X2))),
    inference(backward_demodulation,[],[f108343,f116999]) ).

fof(f118016,plain,
    ! [X1] : sF0 = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(inverse(sF0),multiply(b3,a3))))),X1),inverse(X1)),
    inference(backward_demodulation,[],[f108768,f116999]) ).

fof(f118017,plain,
    ! [X0] : multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)) = multiply(inverse(inverse(inverse(inverse(inverse(X0))))),inverse(multiply(inverse(sF0),multiply(b3,a3)))),
    inference(backward_demodulation,[],[f109013,f116999]) ).

fof(f118024,plain,
    ! [X0] : multiply(inverse(inverse(sF2)),multiply(sF0,inverse(b3))) = multiply(multiply(X0,inverse(inverse(inverse(X0)))),multiply(sF3,multiply(inverse(sF0),multiply(b3,a3)))),
    inference(backward_demodulation,[],[f110430,f116999]) ).

fof(f118036,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X0),multiply(inverse(inverse(multiply(multiply(X1,X2),inverse(X2)))),X0)) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(X3),multiply(X1,X3))),
    inference(backward_demodulation,[],[f112646,f116999]) ).

fof(f118049,plain,
    ! [X0,X1] : multiply(X0,inverse(inverse(X1))) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(inverse(inverse(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),X1)))))),
    inference(backward_demodulation,[],[f116326,f116999]) ).

fof(f118077,plain,
    ! [X0,X1] : multiply(inverse(inverse(inverse(multiply(inverse(sF0),multiply(b3,a3))))),inverse(inverse(X0))) = multiply(multiply(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X0),X1),inverse(X1)),
    inference(forward_demodulation,[],[f117005,f116999]) ).

fof(f118321,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(X1,X0)) = multiply(multiply(multiply(multiply(inverse(multiply(X0,X1)),X2),inverse(X2)),X3),inverse(X3)),
    inference(backward_demodulation,[],[f114876,f117464]) ).

fof(f118328,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(sF0),multiply(a3,inverse(multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(b3))))),
    inference(forward_demodulation,[],[f117465,f116999]) ).

fof(f118337,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(inverse(multiply(inverse(sF0),multiply(b3,a3)))))),
    inference(backward_demodulation,[],[f117015,f117467]) ).

fof(f118342,plain,
    ! [X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(multiply(X0,X1),inverse(X1)))) = multiply(multiply(inverse(inverse(inverse(inverse(inverse(X0))))),X3),inverse(X3)),
    inference(backward_demodulation,[],[f108373,f117468]) ).

fof(f118367,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(X0),multiply(X1,X0))),X2) = multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(inverse(inverse(inverse(X1)))),inverse(multiply(inverse(sF0),multiply(b3,a3))))),X2),
    inference(forward_demodulation,[],[f117509,f116999]) ).

fof(f118558,plain,
    sF0 = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(inverse(multiply(sF0,sF0)),multiply(inverse(c3),sF1))))),
    inference(forward_demodulation,[],[f118016,f109761]) ).

fof(f118560,plain,
    ! [X2,X3] : multiply(multiply(inverse(X2),X3),inverse(X3)) = multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),X2))),
    inference(forward_demodulation,[],[f118014,f117468]) ).

fof(f118917,plain,
    ! [X3,X0,X6,X4,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))),X6),inverse(X6)) = multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(multiply(X0,X5),inverse(X5))),multiply(inverse(sF0),multiply(b3,a3))))),X4),
    inference(backward_demodulation,[],[f115874,f117911]) ).

fof(f119092,plain,
    ! [X1] : multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(X1))) = X1,
    inference(forward_demodulation,[],[f117889,f115596]) ).

fof(f119230,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f118328,f117911]) ).

fof(f119233,plain,
    ! [X3,X0,X1] : multiply(multiply(inverse(inverse(inverse(inverse(inverse(X0))))),X3),inverse(X3)) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(inverse(X1),multiply(X0,X1))))),
    inference(forward_demodulation,[],[f118342,f103779]) ).

fof(f119314,plain,
    ! [X2,X3] : multiply(multiply(inverse(X2),X3),inverse(X3)) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(X2,inverse(multiply(inverse(sF0),multiply(b3,a3))))))),
    inference(forward_demodulation,[],[f118560,f103779]) ).

fof(f119354,plain,
    ! [X3,X0,X6,X4,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))),X6),inverse(X6)) = multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(inverse(inverse(inverse(inverse(multiply(multiply(X0,X5),inverse(X5))))))),inverse(multiply(inverse(sF0),multiply(b3,a3))))),X4),
    inference(forward_demodulation,[],[f118917,f118367]) ).

fof(f119535,plain,
    ! [X2,X0] : inverse(inverse(X0)) = multiply(multiply(X0,X2),inverse(X2)),
    inference(backward_demodulation,[],[f117862,f119092]) ).

fof(f119538,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(X0,X1),inverse(X1)),X2) = multiply(inverse(inverse(X0)),X2),
    inference(backward_demodulation,[],[f117893,f119092]) ).

fof(f119548,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(multiply(X0,X2),X1)) = multiply(inverse(inverse(X2)),inverse(inverse(X0))),
    inference(backward_demodulation,[],[f117953,f119092]) ).

fof(f119561,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(X0,X2),inverse(X2)),inverse(inverse(X1))) = inverse(inverse(multiply(X0,X1))),
    inference(backward_demodulation,[],[f117900,f119092]) ).

fof(f119568,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2))),inverse(inverse(X3))) = inverse(inverse(multiply(multiply(X0,X2),X3))),
    inference(backward_demodulation,[],[f117914,f119092]) ).

fof(f119572,plain,
    ! [X0,X1] : multiply(X0,inverse(inverse(X1))) = inverse(inverse(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),X1))),
    inference(backward_demodulation,[],[f118049,f119092]) ).

fof(f119581,plain,
    ! [X0] : inverse(inverse(inverse(X0))) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,X0))),
    inference(backward_demodulation,[],[f117958,f119092]) ).

fof(f119582,plain,
    multiply(sF0,inverse(b3)) = inverse(inverse(a3)),
    inference(backward_demodulation,[],[f117926,f119092]) ).

fof(f119586,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = inverse(multiply(inverse(sF0),multiply(b3,a3))),
    inference(backward_demodulation,[],[f118337,f119092]) ).

fof(f119702,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(multiply(sF0,inverse(b3))),a3),
    inference(backward_demodulation,[],[f113592,f119230]) ).

fof(f119808,plain,
    ! [X3,X0,X6,X4,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))),X6),inverse(X6)) = multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(multiply(sF0,multiply(multiply(X0,X5),inverse(X5)))),multiply(inverse(c3),sF1))),X4),
    inference(forward_demodulation,[],[f119354,f118017]) ).

fof(f119995,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF0),X1),inverse(X1)) = multiply(multiply(inverse(X0),multiply(inverse(multiply(b3,a3)),X0)),multiply(inverse(sF0),multiply(b3,a3))),
    inference(backward_demodulation,[],[f104031,f119586]) ).

fof(f120013,plain,
    ! [X1] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(X1),multiply(multiply(inverse(sF0),multiply(b3,a3)),X1)),
    inference(backward_demodulation,[],[f114882,f119586]) ).

fof(f120327,plain,
    ! [X2,X0] : multiply(multiply(inverse(sF0),multiply(b3,a3)),X2) = multiply(multiply(X0,inverse(inverse(inverse(X0)))),X2),
    inference(backward_demodulation,[],[f117864,f119586]) ).

fof(f120328,plain,
    ! [X0] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(inverse(inverse(X0))),X0)),
    inference(backward_demodulation,[],[f117894,f119586]) ).

fof(f120337,plain,
    ! [X0,X1] : inverse(multiply(inverse(X0),multiply(X1,X0))) = inverse(multiply(inverse(inverse(inverse(inverse(X1)))),multiply(inverse(sF0),multiply(b3,a3)))),
    inference(backward_demodulation,[],[f117946,f119586]) ).

fof(f120342,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(X1)),multiply(multiply(X0,X2),inverse(X2))) = multiply(inverse(inverse(inverse(inverse(multiply(X0,X1))))),multiply(inverse(sF0),multiply(b3,a3))),
    inference(backward_demodulation,[],[f117976,f119586]) ).

fof(f120358,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,inverse(multiply(X1,inverse(X0)))))) = multiply(multiply(inverse(X0),X1),multiply(inverse(sF0),multiply(b3,a3))),
    inference(backward_demodulation,[],[f117995,f119586]) ).

fof(f120374,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X0),multiply(inverse(inverse(multiply(multiply(X1,X2),inverse(X2)))),X0)) = multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(X3),multiply(X1,X3))),
    inference(backward_demodulation,[],[f118036,f119586]) ).

fof(f120393,plain,
    ! [X0,X1] : multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),X1),inverse(X1)) = multiply(inverse(inverse(multiply(inverse(sF0),multiply(b3,a3)))),inverse(inverse(X0))),
    inference(backward_demodulation,[],[f118077,f119586]) ).

fof(f120543,plain,
    ! [X2,X3] : multiply(multiply(inverse(X2),X3),inverse(X3)) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(X2,multiply(inverse(sF0),multiply(b3,a3)))))),
    inference(backward_demodulation,[],[f119314,f119586]) ).

fof(f121005,plain,
    ! [X2,X0,X1] : multiply(multiply(multiply(inverse(X0),multiply(X1,X0)),X2),inverse(X2)) = multiply(X1,multiply(inverse(inverse(inverse(a3))),a3)),
    inference(backward_demodulation,[],[f114662,f119582]) ).

fof(f121014,plain,
    ! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(multiply(inverse(inverse(X0)),multiply(multiply(X1,X2),inverse(X2))),X3),X4),inverse(X4)) = multiply(multiply(multiply(X1,X0),multiply(inverse(inverse(inverse(a3))),a3)),inverse(inverse(X3))),
    inference(backward_demodulation,[],[f114690,f119582]) ).

fof(f121019,plain,
    ! [X0,X1] : multiply(multiply(multiply(inverse(inverse(X0)),inverse(inverse(a3))),X1),inverse(X1)) = multiply(multiply(a3,X0),multiply(inverse(inverse(inverse(a3))),a3)),
    inference(backward_demodulation,[],[f114739,f119582]) ).

fof(f121022,plain,
    ! [X0,X1] : multiply(multiply(multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)),X1),inverse(X1)) = multiply(inverse(X0),multiply(inverse(inverse(inverse(a3))),a3)),
    inference(backward_demodulation,[],[f114774,f119582]) ).

fof(f121077,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X3),multiply(inverse(inverse(multiply(X1,X0))),X3)) = multiply(inverse(multiply(multiply(inverse(multiply(X0,X1)),X2),inverse(X2))),multiply(inverse(inverse(inverse(a3))),a3)),
    inference(backward_demodulation,[],[f116990,f119582]) ).

fof(f121086,plain,
    ! [X0] : multiply(multiply(X0,inverse(inverse(inverse(X0)))),multiply(sF3,multiply(inverse(sF0),multiply(b3,a3)))) = multiply(inverse(inverse(sF2)),inverse(inverse(a3))),
    inference(backward_demodulation,[],[f118024,f119582]) ).

fof(f121142,plain,
    ! [X2,X0,X1] : inverse(inverse(inverse(X2))) = multiply(multiply(inverse(X0),multiply(X1,X0)),inverse(multiply(X1,X2))),
    inference(backward_demodulation,[],[f103777,f119581]) ).

fof(f121182,plain,
    ! [X0,X1] : multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(multiply(X1,X0))) = inverse(inverse(inverse(multiply(X0,X1)))),
    inference(backward_demodulation,[],[f103779,f119581]) ).

fof(f121205,plain,
    ! [X2,X0,X1] : inverse(inverse(inverse(multiply(inverse(X2),multiply(X1,X2))))) = multiply(multiply(inverse(sF2),sF3),inverse(multiply(a3,multiply(inverse(X0),multiply(X1,X0))))),
    inference(backward_demodulation,[],[f103800,f119581]) ).

fof(f121210,plain,
    ! [X3,X0,X1] : multiply(multiply(inverse(inverse(inverse(inverse(inverse(X0))))),X3),inverse(X3)) = inverse(inverse(inverse(multiply(inverse(X1),multiply(X0,X1))))),
    inference(backward_demodulation,[],[f119233,f119581]) ).

fof(f121224,plain,
    sF0 = inverse(inverse(inverse(multiply(inverse(multiply(sF0,sF0)),multiply(inverse(c3),sF1))))),
    inference(backward_demodulation,[],[f118558,f119581]) ).

fof(f121232,plain,
    ! [X0,X1] : inverse(inverse(inverse(inverse(inverse(X1))))) = multiply(multiply(inverse(inverse(inverse(X0))),X0),inverse(X1)),
    inference(backward_demodulation,[],[f105675,f119581]) ).

fof(f121348,plain,
    ! [X2,X3,X0,X4,X5] : multiply(inverse(inverse(inverse(inverse(X4)))),multiply(multiply(multiply(multiply(X0,X2),inverse(X4)),X5),inverse(X5))) = multiply(inverse(X3),multiply(inverse(inverse(multiply(X0,X2))),X3)),
    inference(backward_demodulation,[],[f104397,f119561]) ).

fof(f121362,plain,
    ! [X2,X3,X0] : inverse(inverse(multiply(multiply(X0,X2),X3))) = multiply(inverse(inverse(multiply(X0,X2))),inverse(inverse(X3))),
    inference(backward_demodulation,[],[f119568,f119561]) ).

fof(f121529,plain,
    ! [X0] : multiply(inverse(inverse(inverse(X0))),X0) = multiply(inverse(inverse(multiply(b3,a3))),inverse(inverse(inverse(sF0)))),
    inference(backward_demodulation,[],[f117954,f119548]) ).

fof(f121572,plain,
    ! [X3,X0,X1] : inverse(multiply(X1,X0)) = multiply(multiply(inverse(inverse(inverse(multiply(X0,X1)))),X3),inverse(X3)),
    inference(backward_demodulation,[],[f118321,f119538]) ).

fof(f121582,plain,
    ! [X0,X1] : inverse(inverse(multiply(X0,X1))) = multiply(inverse(inverse(X0)),inverse(inverse(X1))),
    inference(backward_demodulation,[],[f119561,f119538]) ).

fof(f121666,plain,
    ! [X0,X1] : inverse(inverse(inverse(X1))) = multiply(multiply(inverse(inverse(inverse(X0))),X0),inverse(multiply(multiply(inverse(sF0),multiply(b3,a3)),X1))),
    inference(backward_demodulation,[],[f117966,f119535]) ).

fof(f121721,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(X1),multiply(inverse(X2),X1)),inverse(multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)))) = inverse(inverse(inverse(multiply(inverse(X0),X2)))),
    inference(backward_demodulation,[],[f108950,f119535]) ).

fof(f121844,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(inverse(inverse(a3))),a3),
    inference(forward_demodulation,[],[f119702,f119582]) ).

fof(f121941,plain,
    ! [X3,X0,X6,X4,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))),X6),inverse(X6)) = multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(multiply(inverse(X5),multiply(X0,X5))),multiply(inverse(sF0),multiply(b3,a3)))),X4),
    inference(forward_demodulation,[],[f119808,f106459]) ).

fof(f122099,plain,
    ! [X2,X3] : multiply(multiply(inverse(X2),X3),inverse(X3)) = inverse(inverse(inverse(multiply(X2,multiply(inverse(sF0),multiply(b3,a3)))))),
    inference(forward_demodulation,[],[f120543,f119581]) ).

fof(f122212,plain,
    ! [X0,X1] : multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),X1),inverse(X1)) = multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(X0))),
    inference(forward_demodulation,[],[f120393,f119586]) ).

fof(f122219,plain,
    ! [X3,X0,X1] : multiply(inverse(X0),multiply(inverse(inverse(inverse(inverse(X1)))),X0)) = multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(X3),multiply(X1,X3))),
    inference(forward_demodulation,[],[f120374,f119535]) ).

fof(f122232,plain,
    ! [X0,X1] : inverse(inverse(inverse(inverse(multiply(X1,inverse(X0)))))) = multiply(multiply(inverse(X0),X1),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f120358,f119581]) ).

fof(f122243,plain,
    ! [X0,X1] : multiply(inverse(inverse(X1)),inverse(inverse(X0))) = multiply(inverse(inverse(inverse(inverse(multiply(X0,X1))))),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f120342,f119535]) ).

fof(f122254,plain,
    ! [X0] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(inverse(inverse(X0))),X0)),
    inference(forward_demodulation,[],[f120328,f119586]) ).

fof(f122520,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(inverse(multiply(b3,a3))),inverse(inverse(inverse(sF0)))),
    inference(forward_demodulation,[],[f120013,f119548]) ).

fof(f122525,plain,
    ! [X0] : inverse(inverse(inverse(sF0))) = multiply(multiply(inverse(X0),multiply(inverse(multiply(b3,a3)),X0)),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f119995,f119535]) ).

fof(f122716,plain,
    ! [X3,X0,X1] : multiply(inverse(X3),multiply(inverse(inverse(multiply(X1,X0))),X3)) = multiply(inverse(inverse(inverse(inverse(multiply(X0,X1))))),multiply(inverse(inverse(inverse(a3))),a3)),
    inference(forward_demodulation,[],[f121077,f119535]) ).

fof(f122760,plain,
    ! [X0] : multiply(inverse(X0),multiply(inverse(inverse(inverse(a3))),a3)) = inverse(inverse(multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)))),
    inference(forward_demodulation,[],[f121022,f119535]) ).

fof(f122763,plain,
    ! [X0] : multiply(multiply(a3,X0),multiply(inverse(inverse(inverse(a3))),a3)) = inverse(inverse(multiply(inverse(inverse(X0)),inverse(inverse(a3))))),
    inference(forward_demodulation,[],[f121019,f119535]) ).

fof(f122768,plain,
    ! [X2,X3,X0,X1] : multiply(multiply(multiply(X1,X0),multiply(inverse(inverse(inverse(a3))),a3)),inverse(inverse(X3))) = inverse(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(X1,X2),inverse(X2))),X3))),
    inference(forward_demodulation,[],[f121014,f119535]) ).

fof(f122777,plain,
    ! [X0,X1] : inverse(inverse(multiply(inverse(X0),multiply(X1,X0)))) = multiply(X1,multiply(inverse(inverse(inverse(a3))),a3)),
    inference(forward_demodulation,[],[f121005,f119535]) ).

fof(f122926,plain,
    ! [X0,X1] : inverse(inverse(inverse(inverse(inverse(inverse(inverse(X0))))))) = inverse(inverse(inverse(multiply(inverse(X1),multiply(X0,X1))))),
    inference(forward_demodulation,[],[f121210,f119535]) ).

fof(f122930,plain,
    ! [X2,X0,X1] : inverse(inverse(inverse(multiply(inverse(X0),multiply(X1,X0))))) = inverse(inverse(inverse(multiply(inverse(X2),multiply(X1,X2))))),
    inference(forward_demodulation,[],[f121205,f119581]) ).

fof(f123146,plain,
    ! [X2,X3,X0,X4] : multiply(inverse(X3),multiply(inverse(inverse(multiply(X0,X2))),X3)) = multiply(inverse(inverse(inverse(inverse(X4)))),inverse(inverse(multiply(multiply(X0,X2),inverse(X4))))),
    inference(forward_demodulation,[],[f121348,f119535]) ).

fof(f123254,plain,
    ! [X0] : multiply(inverse(inverse(inverse(X0))),X0) = inverse(inverse(multiply(multiply(b3,a3),inverse(sF0)))),
    inference(forward_demodulation,[],[f121529,f121362]) ).

fof(f123299,plain,
    ! [X0] : inverse(inverse(multiply(sF2,a3))) = multiply(multiply(X0,inverse(inverse(inverse(X0)))),multiply(sF3,multiply(inverse(sF0),multiply(b3,a3)))),
    inference(backward_demodulation,[],[f121086,f121582]) ).

fof(f123306,plain,
    ! [X0,X1] : inverse(multiply(X1,X0)) = inverse(inverse(inverse(inverse(inverse(multiply(X0,X1)))))),
    inference(forward_demodulation,[],[f121572,f119535]) ).

fof(f123378,plain,
    ! [X1] : inverse(inverse(inverse(X1))) = inverse(inverse(inverse(inverse(inverse(multiply(multiply(inverse(sF0),multiply(b3,a3)),X1)))))),
    inference(forward_demodulation,[],[f121666,f121232]) ).

fof(f123566,plain,
    ! [X3,X0,X4,X5] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(multiply(inverse(X5),multiply(X0,X5))),multiply(inverse(sF0),multiply(b3,a3)))),X4) = inverse(inverse(inverse(multiply(inverse(multiply(inverse(sF0),multiply(b3,a3))),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))))),
    inference(forward_demodulation,[],[f121941,f119535]) ).

fof(f123710,plain,
    ! [X2] : inverse(inverse(inverse(X2))) = inverse(inverse(inverse(multiply(X2,multiply(inverse(sF0),multiply(b3,a3)))))),
    inference(forward_demodulation,[],[f122099,f119535]) ).

fof(f123788,plain,
    ! [X0,X1] : multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),X1),inverse(X1)) = multiply(multiply(inverse(sF0),multiply(b3,a3)),inverse(inverse(X0))),
    inference(forward_demodulation,[],[f122212,f119586]) ).

fof(f123820,plain,
    ! [X0,X1] : inverse(inverse(multiply(X1,X0))) = multiply(inverse(inverse(inverse(inverse(multiply(X0,X1))))),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f122243,f121582]) ).

fof(f123824,plain,
    ! [X1] : inverse(inverse(inverse(inverse(X1)))) = multiply(multiply(inverse(sF0),multiply(b3,a3)),X1),
    inference(backward_demodulation,[],[f116361,f122254]) ).

fof(f123994,plain,
    multiply(inverse(sF0),multiply(b3,a3)) = inverse(inverse(multiply(multiply(b3,a3),inverse(sF0)))),
    inference(forward_demodulation,[],[f122520,f121582]) ).

fof(f123999,plain,
    ! [X0] : inverse(inverse(inverse(sF0))) = inverse(inverse(inverse(inverse(multiply(multiply(inverse(multiply(b3,a3)),X0),inverse(X0)))))),
    inference(forward_demodulation,[],[f122525,f122232]) ).

fof(f124147,plain,
    ! [X3,X0,X1] : multiply(inverse(X3),multiply(inverse(inverse(multiply(X1,X0))),X3)) = multiply(inverse(inverse(inverse(inverse(multiply(X0,X1))))),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f122716,f121844]) ).

fof(f124188,plain,
    ! [X0] : multiply(inverse(X0),multiply(inverse(sF0),multiply(b3,a3))) = inverse(inverse(multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)))),
    inference(forward_demodulation,[],[f122760,f121844]) ).

fof(f124191,plain,
    ! [X0] : multiply(multiply(a3,X0),multiply(inverse(inverse(inverse(a3))),a3)) = inverse(inverse(inverse(inverse(multiply(X0,a3))))),
    inference(forward_demodulation,[],[f122763,f121582]) ).

fof(f124196,plain,
    ! [X3,X0,X1] : multiply(multiply(multiply(X1,X0),multiply(inverse(inverse(inverse(a3))),a3)),inverse(inverse(X3))) = inverse(inverse(multiply(multiply(inverse(inverse(X0)),inverse(inverse(X1))),X3))),
    inference(forward_demodulation,[],[f122768,f119535]) ).

fof(f124205,plain,
    ! [X0,X1] : multiply(X1,multiply(inverse(sF0),multiply(b3,a3))) = inverse(inverse(multiply(inverse(X0),multiply(X1,X0)))),
    inference(forward_demodulation,[],[f122777,f121844]) ).

fof(f124300,plain,
    ! [X0,X1] : inverse(inverse(inverse(multiply(inverse(X0),multiply(X1,X0))))) = inverse(inverse(inverse(inverse(inverse(inverse(inverse(X1))))))),
    inference(forward_demodulation,[],[f122930,f122926]) ).

fof(f124409,plain,
    ! [X2,X3,X0,X4] : multiply(inverse(X3),multiply(inverse(inverse(multiply(X0,X2))),X3)) = inverse(inverse(multiply(inverse(inverse(X4)),multiply(multiply(X0,X2),inverse(X4))))),
    inference(forward_demodulation,[],[f123146,f121582]) ).

fof(f124592,plain,
    ! [X1] : inverse(inverse(inverse(X1))) = inverse(multiply(X1,multiply(inverse(sF0),multiply(b3,a3)))),
    inference(forward_demodulation,[],[f123378,f123306]) ).

fof(f124704,plain,
    ! [X3,X0,X4,X5] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(multiply(inverse(X5),multiply(X0,X5))),multiply(inverse(sF0),multiply(b3,a3)))),X4) = inverse(inverse(inverse(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(multiply(X3,X4)),multiply(X3,X0)))))),
    inference(forward_demodulation,[],[f123566,f119586]) ).

fof(f124888,plain,
    ! [X0,X1] : multiply(multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0),X1),inverse(X1)) = X0,
    inference(forward_demodulation,[],[f123788,f117464]) ).

fof(f124936,plain,
    ! [X0,X1] : multiply(X0,inverse(inverse(X1))) = inverse(inverse(multiply(inverse(inverse(inverse(inverse(X0)))),X1))),
    inference(backward_demodulation,[],[f119572,f123824]) ).

fof(f124976,plain,
    ! [X2,X0] : inverse(inverse(inverse(inverse(X2)))) = multiply(multiply(X0,inverse(inverse(inverse(X0)))),X2),
    inference(backward_demodulation,[],[f120327,f123824]) ).

fof(f125215,plain,
    ! [X3,X0,X1] : inverse(inverse(inverse(inverse(multiply(inverse(X3),multiply(X1,X3)))))) = multiply(inverse(X0),multiply(inverse(inverse(inverse(inverse(X1)))),X0)),
    inference(backward_demodulation,[],[f122219,f123824]) ).

fof(f125294,plain,
    ! [X0,X1] : inverse(inverse(inverse(multiply(X0,X1)))) = inverse(inverse(inverse(inverse(inverse(multiply(X1,X0)))))),
    inference(backward_demodulation,[],[f121182,f123824]) ).

fof(f125295,plain,
    ! [X2] : inverse(inverse(inverse(inverse(inverse(inverse(X2)))))) = X2,
    inference(backward_demodulation,[],[f117464,f123824]) ).

fof(f125464,plain,
    ! [X0] : multiply(inverse(sF0),multiply(b3,a3)) = multiply(inverse(inverse(inverse(X0))),X0),
    inference(backward_demodulation,[],[f123254,f123994]) ).

fof(f125470,plain,
    inverse(inverse(inverse(sF0))) = inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(b3,a3)))))))),
    inference(forward_demodulation,[],[f123999,f119535]) ).

fof(f125591,plain,
    ! [X3,X0,X1] : inverse(inverse(multiply(X1,X0))) = multiply(inverse(X3),multiply(inverse(inverse(multiply(X1,X0))),X3)),
    inference(forward_demodulation,[],[f124147,f123820]) ).

fof(f125630,plain,
    sF0 = inverse(multiply(inverse(sF0),multiply(inverse(sF0),multiply(b3,a3)))),
    inference(backward_demodulation,[],[f121224,f124188]) ).

fof(f125633,plain,
    ! [X0] : multiply(multiply(a3,X0),multiply(inverse(sF0),multiply(b3,a3))) = inverse(inverse(inverse(inverse(multiply(X0,a3))))),
    inference(forward_demodulation,[],[f124191,f121844]) ).

fof(f125634,plain,
    ! [X3,X0,X1] : multiply(multiply(multiply(X1,X0),multiply(inverse(inverse(inverse(a3))),a3)),inverse(inverse(X3))) = inverse(inverse(multiply(inverse(inverse(multiply(X0,X1))),X3))),
    inference(forward_demodulation,[],[f124196,f121582]) ).

fof(f125703,plain,
    ! [X1] : inverse(multiply(X1,multiply(inverse(sF0),multiply(b3,a3)))) = inverse(inverse(inverse(inverse(inverse(inverse(inverse(X1))))))),
    inference(forward_demodulation,[],[f124300,f124205]) ).

fof(f125755,plain,
    ! [X2,X3,X0] : multiply(inverse(X3),multiply(inverse(inverse(multiply(X0,X2))),X3)) = multiply(multiply(X0,X2),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f124409,f124205]) ).

fof(f125889,plain,
    ! [X2] : inverse(inverse(inverse(X2))) = inverse(inverse(inverse(inverse(inverse(X2))))),
    inference(backward_demodulation,[],[f123710,f124592]) ).

fof(f125897,plain,
    ! [X0,X1] : inverse(multiply(inverse(X0),multiply(X1,X0))) = inverse(inverse(inverse(inverse(inverse(inverse(inverse(X1))))))),
    inference(backward_demodulation,[],[f120337,f124592]) ).

fof(f126007,plain,
    ! [X3,X0,X4,X5] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(multiply(inverse(X5),multiply(X0,X5))),multiply(inverse(sF0),multiply(b3,a3)))),X4) = inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,X0))))))))),
    inference(forward_demodulation,[],[f124704,f123824]) ).

fof(f126179,plain,
    ! [X0] : inverse(inverse(multiply(multiply(inverse(sF0),multiply(b3,a3)),X0))) = X0,
    inference(forward_demodulation,[],[f124888,f119535]) ).

fof(f126202,plain,
    ! [X0,X1] : inverse(multiply(X0,X1)) = inverse(inverse(inverse(multiply(X0,X1)))),
    inference(forward_demodulation,[],[f125294,f123306]) ).

fof(f126257,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(inverse(inverse(inverse(inverse(X1)))),X0)) = inverse(inverse(multiply(X1,multiply(inverse(sF0),multiply(b3,a3))))),
    inference(forward_demodulation,[],[f125215,f124205]) ).

fof(f126455,plain,
    inverse(inverse(multiply(sF2,a3))) = inverse(inverse(inverse(inverse(multiply(sF3,multiply(inverse(sF0),multiply(b3,a3))))))),
    inference(backward_demodulation,[],[f123299,f124976]) ).

fof(f126715,plain,
    inverse(multiply(b3,a3)) = inverse(inverse(inverse(sF0))),
    inference(forward_demodulation,[],[f125470,f125295]) ).

fof(f126827,plain,
    sF0 = inverse(inverse(inverse(inverse(sF0)))),
    inference(forward_demodulation,[],[f125630,f124592]) ).

fof(f126829,plain,
    ! [X3,X0,X1] : inverse(inverse(multiply(inverse(inverse(multiply(X0,X1))),X3))) = multiply(multiply(multiply(X1,X0),multiply(inverse(sF0),multiply(b3,a3))),inverse(inverse(X3))),
    inference(forward_demodulation,[],[f125634,f125464]) ).

fof(f126881,plain,
    ! [X1] : inverse(X1) = inverse(multiply(X1,multiply(inverse(sF0),multiply(b3,a3)))),
    inference(forward_demodulation,[],[f125703,f125295]) ).

fof(f126904,plain,
    ! [X2,X0] : inverse(inverse(multiply(X0,X2))) = multiply(multiply(X0,X2),multiply(inverse(sF0),multiply(b3,a3))),
    inference(forward_demodulation,[],[f125755,f125591]) ).

fof(f127011,plain,
    ! [X0,X1] : inverse(X1) = inverse(multiply(inverse(X0),multiply(X1,X0))),
    inference(forward_demodulation,[],[f125897,f125295]) ).

fof(f127024,plain,
    ! [X2] : inverse(inverse(inverse(inverse(X2)))) = X2,
    inference(backward_demodulation,[],[f125295,f125889]) ).

fof(f127129,plain,
    ! [X3,X0,X4,X5] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(multiply(inverse(X5),multiply(X0,X5))),multiply(inverse(sF0),multiply(b3,a3)))),X4) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,X0))))))),
    inference(forward_demodulation,[],[f126007,f125889]) ).

fof(f127293,plain,
    ! [X0] : inverse(inverse(inverse(inverse(inverse(inverse(X0)))))) = X0,
    inference(forward_demodulation,[],[f126179,f123824]) ).

fof(f127331,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(X0),X2)) = multiply(multiply(inverse(X1),multiply(inverse(X2),X1)),inverse(multiply(inverse(multiply(sF0,X0)),multiply(inverse(c3),sF1)))),
    inference(backward_demodulation,[],[f121721,f126202]) ).

fof(f127332,plain,
    ! [X0,X1] : inverse(inverse(multiply(X1,inverse(X0)))) = multiply(multiply(inverse(X0),X1),multiply(inverse(sF0),multiply(b3,a3))),
    inference(backward_demodulation,[],[f122232,f126202]) ).

fof(f127375,plain,
    ! [X0] : multiply(multiply(a3,X0),multiply(inverse(sF0),multiply(b3,a3))) = inverse(inverse(multiply(X0,a3))),
    inference(backward_demodulation,[],[f125633,f126202]) ).

fof(f127417,plain,
    ! [X0,X1] : inverse(inverse(inverse(inverse(X1)))) = multiply(inverse(X0),multiply(inverse(inverse(inverse(inverse(X1)))),X0)),
    inference(forward_demodulation,[],[f126257,f124592]) ).

fof(f127594,plain,
    inverse(inverse(multiply(sF2,a3))) = inverse(inverse(multiply(sF3,multiply(inverse(sF0),multiply(b3,a3))))),
    inference(forward_demodulation,[],[f126455,f126202]) ).

fof(f127929,plain,
    sF0 = inverse(inverse(multiply(b3,a3))),
    inference(forward_demodulation,[],[f126827,f126715]) ).

fof(f127968,plain,
    ! [X1] : inverse(X1) = inverse(inverse(inverse(X1))),
    inference(backward_demodulation,[],[f124592,f126881]) ).

fof(f127986,plain,
    ! [X3,X0,X1] : inverse(inverse(multiply(inverse(inverse(multiply(X0,X1))),X3))) = multiply(inverse(inverse(multiply(X1,X0))),inverse(inverse(X3))),
    inference(backward_demodulation,[],[f126829,f126904]) ).

fof(f128102,plain,
    ! [X1] : inverse(inverse(X1)) = inverse(multiply(inverse(multiply(sF0,X1)),multiply(inverse(c3),sF1))),
    inference(backward_demodulation,[],[f103851,f127011]) ).

fof(f128121,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(X2,X1)) = multiply(X2,multiply(X0,inverse(inverse(inverse(X0))))),
    inference(backward_demodulation,[],[f103412,f127024]) ).

fof(f128144,plain,
    ! [X1] : multiply(multiply(inverse(sF0),multiply(b3,a3)),X1) = X1,
    inference(backward_demodulation,[],[f123824,f127024]) ).

fof(f128161,plain,
    ! [X0,X1] : multiply(X0,inverse(inverse(X1))) = inverse(inverse(multiply(X0,X1))),
    inference(backward_demodulation,[],[f124936,f127024]) ).

fof(f128301,plain,
    ! [X3,X0,X4,X5] : multiply(multiply(multiply(inverse(sF0),multiply(b3,a3)),multiply(inverse(multiply(inverse(X5),multiply(X0,X5))),multiply(inverse(sF0),multiply(b3,a3)))),X4) = inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,X0))),
    inference(forward_demodulation,[],[f127129,f127024]) ).

fof(f128462,plain,
    ! [X0] : inverse(inverse(X0)) = X0,
    inference(forward_demodulation,[],[f127293,f127024]) ).

fof(f128486,plain,
    ! [X0] : inverse(inverse(multiply(a3,X0))) = inverse(inverse(multiply(X0,a3))),
    inference(forward_demodulation,[],[f127375,f126904]) ).

fof(f128500,plain,
    ! [X0,X1] : inverse(inverse(multiply(inverse(X0),X1))) = inverse(inverse(multiply(X1,inverse(X0)))),
    inference(forward_demodulation,[],[f127332,f126904]) ).

fof(f128545,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(X1,X0)) = X1,
    inference(forward_demodulation,[],[f127417,f127024]) ).

fof(f128763,plain,
    inverse(inverse(multiply(sF2,a3))) = inverse(inverse(sF3)),
    inference(forward_demodulation,[],[f127594,f126881]) ).

fof(f129095,plain,
    ! [X2,X0,X1] : inverse(X2) = multiply(multiply(inverse(X0),multiply(X1,X0)),inverse(multiply(X1,X2))),
    inference(backward_demodulation,[],[f121142,f127968]) ).

fof(f129164,plain,
    ! [X3,X0,X1] : inverse(inverse(multiply(multiply(X1,X0),X3))) = inverse(inverse(multiply(inverse(inverse(multiply(X0,X1))),X3))),
    inference(forward_demodulation,[],[f127986,f121582]) ).

fof(f129249,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(X0),X2)) = multiply(multiply(inverse(X1),multiply(inverse(X2),X1)),inverse(inverse(X0))),
    inference(backward_demodulation,[],[f127331,f128102]) ).

fof(f129370,plain,
    sF0 = multiply(b3,inverse(inverse(a3))),
    inference(backward_demodulation,[],[f127929,f128161]) ).

fof(f129426,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(X2,X1)) = multiply(X2,multiply(X0,inverse(X0))),
    inference(forward_demodulation,[],[f128121,f127968]) ).

fof(f129522,plain,
    ! [X3,X0,X4,X5] : inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,X0))) = multiply(multiply(inverse(multiply(inverse(X5),multiply(X0,X5))),multiply(inverse(sF0),multiply(b3,a3))),X4),
    inference(forward_demodulation,[],[f128301,f128144]) ).

fof(f129725,plain,
    ! [X0] : multiply(X0,a3) = inverse(inverse(multiply(a3,X0))),
    inference(forward_demodulation,[],[f128486,f128462]) ).

fof(f129739,plain,
    ! [X0,X1] : multiply(X1,inverse(X0)) = inverse(inverse(multiply(inverse(X0),X1))),
    inference(forward_demodulation,[],[f128500,f128462]) ).

fof(f130021,plain,
    sF3 = inverse(inverse(multiply(sF2,a3))),
    inference(forward_demodulation,[],[f128763,f128462]) ).

fof(f130391,plain,
    ! [X2,X1] : inverse(X2) = multiply(X1,inverse(multiply(X1,X2))),
    inference(forward_demodulation,[],[f129095,f128545]) ).

fof(f130406,plain,
    ! [X3,X0,X1] : inverse(inverse(multiply(multiply(X1,X0),X3))) = multiply(inverse(inverse(multiply(X0,X1))),X3),
    inference(forward_demodulation,[],[f129164,f128462]) ).

fof(f130483,plain,
    ! [X2,X0,X1] : inverse(multiply(inverse(X0),X2)) = multiply(multiply(inverse(X1),multiply(inverse(X2),X1)),X0),
    inference(forward_demodulation,[],[f129249,f128462]) ).

fof(f130579,plain,
    sF0 = multiply(b3,a3),
    inference(forward_demodulation,[],[f129370,f128462]) ).

fof(f130646,plain,
    ! [X2,X0] : multiply(X2,multiply(X0,inverse(X0))) = X2,
    inference(forward_demodulation,[],[f129426,f128545]) ).

fof(f130740,plain,
    ! [X3,X0,X4] : inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,X0))) = multiply(multiply(inverse(X0),multiply(inverse(sF0),multiply(b3,a3))),X4),
    inference(forward_demodulation,[],[f129522,f128545]) ).

fof(f130941,plain,
    ! [X0] : multiply(a3,X0) = multiply(X0,a3),
    inference(forward_demodulation,[],[f129725,f128462]) ).

fof(f130953,plain,
    ! [X0,X1] : multiply(X1,inverse(X0)) = multiply(inverse(X0),X1),
    inference(forward_demodulation,[],[f129739,f128462]) ).

fof(f131230,plain,
    sF3 = multiply(sF2,a3),
    inference(forward_demodulation,[],[f130021,f128462]) ).

fof(f131571,plain,
    ! [X3,X0,X1] : multiply(multiply(X0,X1),X3) = inverse(inverse(multiply(multiply(X1,X0),X3))),
    inference(forward_demodulation,[],[f130406,f128462]) ).

fof(f131638,plain,
    ! [X2,X0] : inverse(multiply(inverse(X0),X2)) = multiply(inverse(X2),X0),
    inference(forward_demodulation,[],[f130483,f128545]) ).

fof(f131881,plain,
    ! [X3,X0,X4] : inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,X0))) = multiply(multiply(inverse(X0),multiply(inverse(sF0),sF0)),X4),
    inference(forward_demodulation,[],[f130740,f130579]) ).

fof(f132638,plain,
    ! [X3,X0,X1] : multiply(multiply(X0,X1),X3) = multiply(multiply(X1,X0),X3),
    inference(forward_demodulation,[],[f131571,f128462]) ).

fof(f132909,plain,
    ! [X3,X0,X4] : inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,X0))) = multiply(multiply(inverse(X0),multiply(sF0,inverse(sF0))),X4),
    inference(forward_demodulation,[],[f131881,f130953]) ).

fof(f133826,plain,
    ! [X3,X0,X4] : multiply(inverse(X0),X4) = inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,X0))),
    inference(forward_demodulation,[],[f132909,f130646]) ).

fof(f134660,plain,
    ! [X3,X0,X4] : multiply(inverse(X0),X4) = multiply(inverse(multiply(X3,X0)),multiply(X3,X4)),
    inference(forward_demodulation,[],[f133826,f131638]) ).

fof(f144079,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(multiply(X1,X0))),X2) = multiply(inverse(inverse(X0)),multiply(X1,X2)),
    inference(superposition,[],[f134660,f130391]) ).

fof(f144130,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(inverse(inverse(multiply(X1,X0))),X2),
    inference(forward_demodulation,[],[f144079,f128462]) ).

fof(f144142,plain,
    ! [X2,X0,X1] : multiply(multiply(X1,X0),X2) = multiply(X0,multiply(X1,X2)),
    inference(forward_demodulation,[],[f144130,f128462]) ).

fof(f144352,plain,
    ! [X3,X0,X1] : multiply(multiply(X1,X0),X3) = multiply(X1,multiply(X0,X3)),
    inference(backward_demodulation,[],[f132638,f144142]) ).

fof(f147057,plain,
    ! [X0] : multiply(sF0,X0) = multiply(a3,multiply(b3,X0)),
    inference(superposition,[],[f144352,f4]) ).

fof(f148087,plain,
    multiply(sF0,c3) = multiply(a3,sF2),
    inference(superposition,[],[f147057,f8]) ).

fof(f148133,plain,
    multiply(sF0,c3) = multiply(sF2,a3),
    inference(forward_demodulation,[],[f148087,f130941]) ).

fof(f148144,plain,
    multiply(sF0,c3) = sF3,
    inference(forward_demodulation,[],[f148133,f131230]) ).

fof(f148151,plain,
    sF1 = sF3,
    inference(forward_demodulation,[],[f148144,f6]) ).

fof(f148154,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f148151,f11]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP507-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39  % Computer : n008.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 10:06:54 UTC 2026
% 0.12/0.39  % CPUTime  : 
% 0.12/0.39  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.43  Running first-order theorem proving
% 0.12/0.43  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 85.02/12.86  % (999016)Detected a unit-equality problem, will run specialized UEQ schedule.
% 85.02/12.86  % (999077)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2438474282:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 85.02/12.86  % (999069)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1495497305:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 85.02/12.86  % (999068)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=483871574:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 85.02/12.86  % (999071)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1116045193:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 85.02/12.86  % (999072)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2437974553:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 85.02/12.86  % (999076)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=696233006:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 85.02/12.86  % (999074)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1898892461:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 85.02/12.86  % (999072)Instruction limit reached! 
% 85.02/12.86  % (999072)------------------------------
% 85.02/12.86  % (999072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.02/12.86  % (999072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.02/12.86  % (999072)CaDiCaL version: 2.1.3
% 85.02/12.86  % (999072)Termination reason: Instruction limit
% 85.02/12.86  % (999072)Termination phase: Saturation
% 85.02/12.86  % (999072)Time elapsed: 0.072 s
% 85.02/12.86  % (999072)Peak memory usage: 88 MB
% 85.02/12.86  % (999072)Instructions burned: 138 (million)
% 85.02/12.86  % (999074)Instruction limit reached! 
% 85.02/12.86  % (999074)------------------------------
% 85.02/12.86  % (999074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.02/12.86  % (999074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.02/12.86  % (999074)CaDiCaL version: 2.1.3
% 85.02/12.86  % (999074)Termination reason: Instruction limit
% 85.02/12.86  % (999074)Termination phase: Saturation
% 85.02/12.86  % (999074)Time elapsed: 0.086 s
% 85.02/12.86  % (999074)Peak memory usage: 88 MB
% 85.02/12.86  % (999074)Instructions burned: 182 (million)
% 85.02/12.86  % (999076)Instruction limit reached! 
% 85.02/12.86  % (999076)------------------------------
% 85.02/12.86  % (999076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.02/12.86  % (999076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.02/12.86  % (999076)CaDiCaL version: 2.1.3
% 85.02/12.86  % (999076)Termination reason: Instruction limit
% 85.02/12.86  % (999076)Termination phase: Saturation
% 85.02/12.86  % (999076)Time elapsed: 0.136 s
% 85.02/12.86  % (999076)Peak memory usage: 90 MB
% 85.02/12.86  % (999076)Instructions burned: 259 (million)
% 85.02/12.86  % (999125)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1183794438:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 85.02/12.86  % (999126)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1855565156:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 85.02/12.86  % (999127)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=842578598:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 85.02/12.86  % (999077)Instruction limit reached! 
% 85.02/12.86  % (999077)------------------------------
% 85.02/12.86  % (999077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.02/12.86  % (999077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.02/12.86  % (999077)CaDiCaL version: 2.1.3
% 85.02/12.86  % (999077)Termination reason: Instruction limit
% 85.02/12.86  % (999077)Termination phase: Saturation
% 85.02/12.86  % (999077)Time elapsed: 0.314 s
% 85.02/12.86  % (999077)Peak memory usage: 95 MB
% 85.02/12.86  % (999077)Instructions burned: 1189 (million)
% 115.12/17.10  % (999127)Instruction limit reached! 
% 115.12/17.10  % (999127)------------------------------
% 115.12/17.10  % (999127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.12/17.10  % (999127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.12/17.10  % (999127)CaDiCaL version: 2.1.3
% 115.12/17.10  % (999127)Termination reason: Instruction limit
% 115.12/17.10  % (999127)Termination phase: Saturation
% 115.12/17.10  % (999127)Time elapsed: 0.126 s
% 115.12/17.10  % (999127)Peak memory usage: 89 MB
% 115.12/17.10  % (999127)Instructions burned: 215 (million)
% 115.12/17.10  % (999131)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=1412091960:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2995 on theBenchmark for (2995ds/317Mi)
% 115.12/17.10  % (999131)Instruction limit reached! 
% 115.12/17.10  % (999131)------------------------------
% 115.12/17.10  % (999131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.12/17.10  % (999131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.12/17.10  % (999131)CaDiCaL version: 2.1.3
% 115.12/17.10  % (999131)Termination reason: Instruction limit
% 115.12/17.10  % (999131)Termination phase: Saturation
% 115.12/17.10  % (999131)Time elapsed: 0.094 s
% 115.12/17.10  % (999131)Peak memory usage: 92 MB
% 115.12/17.10  % (999131)Instructions burned: 319 (million)
% 115.12/17.10  % (999133)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=2038167597:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/12125Mi)
% 115.12/17.10  % (999134)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3245919805:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2993 on theBenchmark for (2993ds/2836Mi)
% 115.12/17.10  % (999125)Instruction limit reached! 
% 115.12/17.10  % (999125)------------------------------
% 115.12/17.10  % (999125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.12/17.10  % (999125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.12/17.10  % (999125)CaDiCaL version: 2.1.3
% 115.12/17.10  % (999125)Termination reason: Instruction limit
% 115.12/17.10  % (999125)Termination phase: Saturation
% 115.12/17.10  % (999125)Time elapsed: 1.203 s
% 115.12/17.10  % (999125)Peak memory usage: 139 MB
% 115.12/17.10  % (999125)Instructions burned: 2052 (million)
% 115.12/17.10  % (999134)Instruction limit reached! 
% 115.12/17.10  % (999134)------------------------------
% 115.12/17.10  % (999134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.12/17.10  % (999134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.12/17.10  % (999134)CaDiCaL version: 2.1.3
% 115.12/17.10  % (999134)Termination reason: Instruction limit
% 115.12/17.10  % (999134)Termination phase: Saturation
% 115.12/17.10  % (999134)Time elapsed: 0.828 s
% 115.12/17.10  % (999134)Peak memory usage: 111 MB
% 115.12/17.10  % (999134)Instructions burned: 2839 (million)
% 115.12/17.10  % (999137)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2368355670:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2983 on theBenchmark for (2983ds/14534Mi)
% 115.12/17.10  % (999138)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=969740643:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2983 on theBenchmark for (2983ds/11832Mi)
% 115.12/17.11  % (999126)Instruction limit reached! 
% 115.12/17.11  % (999126)------------------------------
% 115.12/17.11  % (999126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.12/17.11  % (999126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.12/17.11  % (999126)CaDiCaL version: 2.1.3
% 115.12/17.11  % (999126)Termination reason: Instruction limit
% 115.12/17.11  % (999126)Termination phase: Saturation
% 115.12/17.11  % (999126)Time elapsed: 2.705 s
% 115.12/17.11  % (999126)Peak memory usage: 167 MB
% 115.12/17.11  % (999126)Instructions burned: 4950 (million)
% 115.12/17.11  % (999141)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=3106387842:i=2279:fgj=on:bd=all_2968 on theBenchmark for (2968ds/2279Mi)
% 115.12/17.11  % (999141)Instruction limit reached! 
% 115.12/17.11  % (999141)------------------------------
% 115.12/17.11  % (999141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.68/32.62  % (999141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.68/32.62  % (999141)CaDiCaL version: 2.1.3
% 225.68/32.62  % (999141)Termination reason: Instruction limit
% 225.68/32.62  % (999141)Termination phase: Saturation
% 225.68/32.62  % (999141)Time elapsed: 1.319 s
% 225.68/32.62  % (999141)Peak memory usage: 140 MB
% 225.68/32.62  % (999141)Instructions burned: 2279 (million)
% 225.68/32.62  % (999143)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=2943507795:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2953 on theBenchmark for (2953ds/6225Mi)
% 225.68/32.62  % (999138)Instruction limit reached! 
% 225.68/32.62  % (999138)------------------------------
% 225.68/32.62  % (999138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.68/32.62  % (999138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.68/32.62  % (999138)CaDiCaL version: 2.1.3
% 225.68/32.62  % (999138)Termination reason: Instruction limit
% 225.68/32.62  % (999138)Termination phase: Saturation
% 225.68/32.62  % (999138)Time elapsed: 3.721 s
% 225.68/32.62  % (999138)Peak memory usage: 206 MB
% 225.68/32.62  % (999138)Instructions burned: 11835 (million)
% 225.68/32.62  % (999160)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=1711919655:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2945 on theBenchmark for (2945ds/21755Mi)
% 225.68/32.62  % (999133)Instruction limit reached! 
% 225.68/32.62  % (999133)------------------------------
% 225.68/32.62  % (999133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.68/32.62  % (999133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.68/32.62  % (999133)CaDiCaL version: 2.1.3
% 225.68/32.62  % (999133)Termination reason: Instruction limit
% 225.68/32.62  % (999133)Termination phase: Saturation
% 225.68/32.62  % (999133)Time elapsed: 7.235 s
% 225.68/32.62  % (999133)Peak memory usage: 239 MB
% 225.68/32.62  % (999133)Instructions burned: 12125 (million)
% 225.68/32.62  % (999320)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=684119327:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2920 on theBenchmark for (2920ds/16427Mi)
% 225.68/32.62  % (999143)Instruction limit reached! 
% 225.68/32.62  % (999143)------------------------------
% 225.68/32.62  % (999143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.68/32.62  % (999143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.68/32.62  % (999143)CaDiCaL version: 2.1.3
% 225.68/32.62  % (999143)Termination reason: Instruction limit
% 225.68/32.62  % (999143)Termination phase: Saturation
% 225.68/32.62  % (999143)Time elapsed: 4.203 s
% 225.68/32.62  % (999143)Peak memory usage: 174 MB
% 225.68/32.62  % (999143)Instructions burned: 6226 (million)
% 225.68/32.62  % (999369)lrs+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=3771508444:i=9356:fgj=on:bd=preordered:av=off_2909 on theBenchmark for (2909ds/9356Mi)
% 225.68/32.62  % (999137)Instruction limit reached! 
% 225.68/32.62  % (999137)------------------------------
% 225.68/32.62  % (999137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.68/32.62  % (999137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.68/32.62  % (999137)CaDiCaL version: 2.1.3
% 225.68/32.62  % (999137)Termination reason: Instruction limit
% 225.68/32.62  % (999137)Termination phase: Saturation
% 225.68/32.62  % (999137)Time elapsed: 8.909 s
% 225.68/32.62  % (999137)Peak memory usage: 239 MB
% 225.68/32.62  % (999137)Instructions burned: 14535 (million)
% 225.68/32.62  % (999371)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=2649028532:i=2070:kws=inv_precedence:slsql=off:bd=all_2893 on theBenchmark for (2893ds/2070Mi)
% 225.68/32.62  % (999371)Instruction limit reached! 
% 225.68/32.62  % (999371)------------------------------
% 225.68/32.62  % (999371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.68/32.62  % (999371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.68/32.62  % (999371)CaDiCaL version: 2.1.3
% 225.68/32.62  % (999371)Termination reason: Instruction limit
% 225.68/32.62  % (999371)Termination phase: Saturation
% 225.68/32.62  % (999371)Time elapsed: 1.0000 s
% 225.68/32.62  % (999371)Peak memory usage: 115 MB
% 225.68/32.62  % (999371)Instructions burned: 2071 (million)
% 225.68/32.62  % (999373)lrs+1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=8000:tgt=ground:npcc=on:fde=unused:sp=const_min:urr=ec_only:s2agt=32:random_seed=364651176:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2881 on theBenchmark for (2881ds/6461Mi)
% 195.19/39.54  % (999160)Instruction limit reached! 
% 195.19/39.54  % (999160)------------------------------
% 195.19/39.54  % (999160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999160)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999160)Termination reason: Instruction limit
% 195.19/39.54  % (999160)Termination phase: Saturation
% 195.19/39.54  % (999160)Time elapsed: 7.507 s
% 195.19/39.54  % (999160)Peak memory usage: 186 MB
% 195.19/39.54  % (999160)Instructions burned: 21755 (million)
% 195.19/39.54  % (999506)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=2828398433:i=2310:bd=all:ss=included_2868 on theBenchmark for (2868ds/2310Mi)
% 195.19/39.54  % (999506)Instruction limit reached! 
% 195.19/39.54  % (999506)------------------------------
% 195.19/39.54  % (999506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999506)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999506)Termination reason: Instruction limit
% 195.19/39.54  % (999506)Termination phase: Saturation
% 195.19/39.54  % (999506)Time elapsed: 0.609 s
% 195.19/39.54  % (999506)Peak memory usage: 102 MB
% 195.19/39.54  % (999506)Instructions burned: 2313 (million)
% 195.19/39.54  % (999610)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=324169879:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2861 on theBenchmark for (2861ds/2616Mi)
% 195.19/39.54  % (999369)Instruction limit reached! 
% 195.19/39.54  % (999369)------------------------------
% 195.19/39.54  % (999369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999369)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999369)Termination reason: Instruction limit
% 195.19/39.54  % (999369)Termination phase: Saturation
% 195.19/39.54  % (999369)Time elapsed: 5.229 s
% 195.19/39.54  % (999369)Peak memory usage: 196 MB
% 195.19/39.54  % (999369)Instructions burned: 9357 (million)
% 195.19/39.54  % (999625)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=3828934835:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2855 on theBenchmark for (2855ds/30521Mi)
% 195.19/39.54  % (999610)Instruction limit reached! 
% 195.19/39.54  % (999610)------------------------------
% 195.19/39.54  % (999610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999610)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999610)Termination reason: Instruction limit
% 195.19/39.54  % (999610)Termination phase: Saturation
% 195.19/39.54  % (999610)Time elapsed: 1.126 s
% 195.19/39.54  % (999610)Peak memory usage: 115 MB
% 195.19/39.54  % (999610)Instructions burned: 2617 (million)
% 195.19/39.54  % (999642)lrs+11_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:tgt=full:npcc=on:prc=on:fde=unused:sp=reverse_frequency:spb=goal:acc=on:urr=ec_only:s2agt=32:random_seed=2547408465:i=3258:fgj=on:bd=all:ins=1_2848 on theBenchmark for (2848ds/3258Mi)
% 195.19/39.54  % (999373)Instruction limit reached! 
% 195.19/39.54  % (999373)------------------------------
% 195.19/39.54  % (999373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999373)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999373)Termination reason: Instruction limit
% 195.19/39.54  % (999373)Termination phase: Saturation
% 195.19/39.54  % (999373)Time elapsed: 3.735 s
% 195.19/39.54  % (999373)Peak memory usage: 181 MB
% 195.19/39.54  % (999373)Instructions burned: 6462 (million)
% 195.19/39.54  % (999797)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=962556740:i=5037:kws=precedence_2842 on theBenchmark for (2842ds/5037Mi)
% 195.19/39.54  % (999642)Instruction limit reached! 
% 195.19/39.54  % (999642)------------------------------
% 195.19/39.54  % (999642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999642)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999642)Termination reason: Instruction limit
% 195.19/39.54  % (999642)Termination phase: Saturation
% 195.19/39.54  % (999642)Time elapsed: 0.989 s
% 195.19/39.54  % (999642)Peak memory usage: 150 MB
% 195.19/39.54  % (999642)Instructions burned: 3261 (million)
% 195.19/39.54  % (999799)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=410936242:i=65240_2837 on theBenchmark for (2837ds/65240Mi)
% 195.19/39.54  % (999320)Instruction limit reached! 
% 195.19/39.54  % (999320)------------------------------
% 195.19/39.54  % (999320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999320)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999320)Termination reason: Instruction limit
% 195.19/39.54  % (999320)Termination phase: Saturation
% 195.19/39.54  % (999320)Time elapsed: 9.489 s
% 195.19/39.54  % (999320)Peak memory usage: 245 MB
% 195.19/39.54  % (999320)Instructions burned: 16427 (million)
% 195.19/39.54  % (999801)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=1488973194:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2823 on theBenchmark for (2823ds/16502Mi)
% 195.19/39.54  % (999797)Instruction limit reached! 
% 195.19/39.54  % (999797)------------------------------
% 195.19/39.54  % (999797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999797)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999797)Termination reason: Instruction limit
% 195.19/39.54  % (999797)Termination phase: Saturation
% 195.19/39.54  % (999797)Time elapsed: 2.713 s
% 195.19/39.54  % (999797)Peak memory usage: 167 MB
% 195.19/39.54  % (999797)Instructions burned: 5037 (million)
% 195.19/39.54  % (999803)lrs-1011_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=32000:npcc=on:drc=off:sp=const_max:spb=goal_then_units:urr=ec_only:fd=preordered:random_seed=3795929817:i=7623:bd=preordered:er=filter_2813 on theBenchmark for (2813ds/7623Mi)
% 195.19/39.54  % (999803)Instruction limit reached! 
% 195.19/39.54  % (999803)------------------------------
% 195.19/39.54  % (999803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999803)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999803)Termination reason: Instruction limit
% 195.19/39.54  % (999803)Termination phase: Saturation
% 195.19/39.54  % (999803)Time elapsed: 4.289 s
% 195.19/39.54  % (999803)Peak memory usage: 183 MB
% 195.19/39.54  % (999803)Instructions burned: 7624 (million)
% 195.19/39.54  % (999805)dis+1010_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:tgt=full:npcc=on:sp=const_min:spb=non_intro:lcm=predicate:acc=on:urr=ec_only:rp=on:gs=on:random_seed=4118486555:i=8183:kws=frequency:add=off:gsp=on_2769 on theBenchmark for (2769ds/8183Mi)
% 195.19/39.54  % (999801)Instruction limit reached! 
% 195.19/39.54  % (999801)------------------------------
% 195.19/39.54  % (999801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999801)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999801)Termination reason: Instruction limit
% 195.19/39.54  % (999801)Termination phase: Saturation
% 195.19/39.54  % (999801)Time elapsed: 9.131 s
% 195.19/39.54  % (999801)Peak memory usage: 255 MB
% 195.19/39.54  % (999801)Instructions burned: 16503 (million)
% 195.19/39.54  % (999805)Instruction limit reached! 
% 195.19/39.54  % (999805)------------------------------
% 195.19/39.54  % (999805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999805)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999805)Termination reason: Instruction limit
% 195.19/39.54  % (999805)Termination phase: Saturation
% 195.19/39.54  % (999805)Time elapsed: 3.743 s
% 195.19/39.54  % (999805)Peak memory usage: 176 MB
% 195.19/39.54  % (999805)Instructions burned: 8183 (million)
% 195.19/39.54  % (999807)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:bsr=unit_only:random_seed=1488802419:i=8387_2730 on theBenchmark for (2730ds/8387Mi)
% 195.19/39.54  % (999808)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=453703986:i=53964:kws=inv_arity_squared:fgj=on:bd=preordered_2729 on theBenchmark for (2729ds/53964Mi)
% 195.19/39.54  % (999807)Instruction limit reached! 
% 195.19/39.54  % (999807)------------------------------
% 195.19/39.54  % (999807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999807)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999807)Termination reason: Instruction limit
% 195.19/39.54  % (999807)Termination phase: Saturation
% 195.19/39.54  % (999807)Time elapsed: 4.610 s
% 195.19/39.54  % (999807)Peak memory usage: 203 MB
% 195.19/39.54  % (999807)Instructions burned: 8389 (million)
% 195.19/39.54  % (1000230)lrs-1011_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:sp=reverse_frequency:spb=goal:lsd=20:urr=on:flr=on:random_seed=3017311246:i=10575:s2at=5:gtg=position_2682 on theBenchmark for (2682ds/10575Mi)
% 195.19/39.54  % (999625)Instruction limit reached! 
% 195.19/39.54  % (999625)------------------------------
% 195.19/39.54  % (999625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999625)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999625)Termination reason: Instruction limit
% 195.19/39.54  % (999625)Termination phase: Saturation
% 195.19/39.54  % (999625)Time elapsed: 17.713 s
% 195.19/39.54  % (999625)Peak memory usage: 300 MB
% 195.19/39.54  % (999625)Instructions burned: 30522 (million)
% 195.19/39.54  % (1000232)ott-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=ground:npcc=on:lsd=50:urr=ec_only:random_seed=997567743:i=12036:s2at=3:gtgl=2:kws=frequency:add=off:fgj=on:bd=preordered:ins=2:gtg=exists_sym_2675 on theBenchmark for (2675ds/12036Mi)
% 195.19/39.54  % (999799)Instruction limit reached! 
% 195.19/39.54  % (999799)------------------------------
% 195.19/39.54  % (999799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (999799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (999799)CaDiCaL version: 2.1.3
% 195.19/39.54  % (999799)Termination reason: Instruction limit
% 195.19/39.54  % (999799)Termination phase: Saturation
% 195.19/39.54  % (999799)Time elapsed: 19.630 s
% 195.19/39.54  % (999799)Peak memory usage: 711 MB
% 195.19/39.54  % (999799)Instructions burned: 65244 (million)
% 195.19/39.54  % (1000234)lrs+1011_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=96051654:i=16065:fgj=on:bd=preordered:av=off_2639 on theBenchmark for (2639ds/16065Mi)
% 195.19/39.54  % (1000230)Instruction limit reached! 
% 195.19/39.54  % (1000230)------------------------------
% 195.19/39.54  % (1000230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.19/39.54  % (1000230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.19/39.54  % (1000230)CaDiCaL version: 2.1.3
% 195.19/39.54  % (1000230)Termination reason: Instruction limit
% 195.19/39.54  % (1000230)Termination phase: Saturation
% 195.19/39.54  % (1000230)Time elapsed: 5.596 s
% 195.19/39.54  % (1000230)Peak memory usage: 220 MB
% 195.19/39.54  % (1000230)Instructions burned: 10576 (million)
% 195.19/39.54  % (1000236)dis-1011_1_to=kbo:ncem=casc2026/models/loop4.pt:sil=64000:tgt=ground:npcc=on:sp=arity:spb=non_intro:random_seed=3984203350:st=8.34:cond=on:i=28442:gtgl=3:sd=8:gtg=all:ss=included_2624 on theBenchmark for (2624ds/28442Mi)
% 195.19/39.54  % (999071)First to succeed.
% 195.19/39.54  % (999071)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-999016"
% 195.19/39.54  % (999071)Refutation found. Thanks to Tanya!
% 195.19/39.54  % SZS status Unsatisfiable for theBenchmark
% 195.19/39.54  % SZS output start Proof for theBenchmark
% See solution above
% 274.67/39.74  % (999071)------------------------------
% 274.67/39.74  % (999071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.67/39.74  % (999071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.67/39.74  % (999071)CaDiCaL version: 2.1.3
% 274.67/39.74  % (999071)Termination reason: Refutation
% 274.67/39.74  % (999071)Time elapsed: 38.114 s
% 274.67/39.74  % (999071)Peak memory usage: 359 MB
% 274.67/39.74  % (999071)Instructions burned: 61500 (million)
% 274.67/39.74  % (999071)------------------------------
% 274.67/39.74  % (999071)------------------------------
% 274.67/39.74  % (999016)Success in time 38.67 s
% 274.67/39.74  % Vampire exiting
%------------------------------------------------------------------------------