↑ Up

Vampire---5.0.1.UNS-Ref.s

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

% Computer : n010.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 10:12:08 AM UTC 2026

% Result   : Unsatisfiable 128.70s 27.04s
% Output   : Refutation 186.25s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   93
%            Number of leaves      :    7
% Syntax   : Number of formulae    :  527 ( 527 unt;   1 def)
%            Number of atoms       :  527 ( 523 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :    2 (   2   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    5 (   4 avg)
%            Maximal term depth    :    9 (   2 avg)
%            Number of predicates  :    3 (   1 usr;   1 prp; 0-2 aty)
%            Number of functors    :    7 (   7 usr;   4 con; 0-2 aty)
%            Number of variables   : 1422 (1422   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    ! [X0] : multiply(identity,X0) = X0,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_identity) ).

fof(f2,axiom,
    ! [X0] : multiply(inverse(X0),X0) = identity,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_inverse) ).

fof(f3,plain,
    ! [X0] : identity = multiply(inverse(X0),X0),
    inference(reorient_equations,[],[f2]) ).

fof(f4,axiom,
    ! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity) ).

fof(f5,axiom,
    ! [X0,X1] : commutator(X0,X1) = multiply(inverse(X0),multiply(inverse(X1),multiply(X0,X1))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',name) ).

fof(f6,axiom,
    ! [X2,X0,X1] : commutator(commutator(X0,X1),X2) = commutator(X0,commutator(X1,X2)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_commutator) ).

fof(f7,negated_conjecture,
    multiply(a,commutator(b,c)) != multiply(commutator(b,c),a),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_center) ).

fof(f8,definition,
    ~ sP0(multiply(a,commutator(b,c))),
    introduced(definition,[new_symbols(definition,[sP0])],[inequality_splitting_name_introduction]) ).

fof(f9,plain,
    sP0(multiply(commutator(b,c),a)),
    inference(inequality_splitting,[],[f7,f8]) ).

fof(f17,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X1),X2) = multiply(inverse(multiply(X0,X1)),multiply(inverse(X2),multiply(X0,multiply(X1,X2)))),
    inference(superposition,[],[f5,f4]) ).

fof(f18,plain,
    ! [X0] : commutator(identity,X0) = multiply(inverse(identity),multiply(inverse(X0),X0)),
    inference(superposition,[],[f5,f1]) ).

fof(f20,plain,
    ! [X2,X0,X1] : multiply(inverse(X0),multiply(multiply(inverse(X1),multiply(X0,X1)),X2)) = multiply(commutator(X0,X1),X2),
    inference(superposition,[],[f4,f5]) ).

fof(f21,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),X2) = multiply(inverse(X0),multiply(inverse(X1),multiply(multiply(X0,X1),X2))),
    inference(forward_demodulation,[],[f20,f4]) ).

fof(f22,plain,
    ! [X0] : commutator(identity,X0) = multiply(inverse(identity),identity),
    inference(forward_demodulation,[],[f18,f3]) ).

fof(f23,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),X2) = multiply(inverse(X0),multiply(inverse(X1),multiply(X0,multiply(X1,X2)))),
    inference(forward_demodulation,[],[f21,f4]) ).

fof(f24,plain,
    ! [X0] : identity = commutator(identity,X0),
    inference(forward_demodulation,[],[f22,f3]) ).

fof(f25,plain,
    ! [X0] : commutator(inverse(X0),X0) = multiply(inverse(inverse(X0)),multiply(inverse(X0),identity)),
    inference(superposition,[],[f5,f3]) ).

fof(f26,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
    inference(superposition,[],[f4,f3]) ).

fof(f27,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = X1,
    inference(forward_demodulation,[],[f26,f1]) ).

fof(f28,plain,
    ! [X0] : identity = commutator(inverse(X0),X0),
    inference(backward_demodulation,[],[f25,f27]) ).

fof(f29,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
    inference(superposition,[],[f27,f4]) ).

fof(f31,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(X0,X1)) = multiply(inverse(inverse(X0)),commutator(X0,X1)),
    inference(superposition,[],[f27,f5]) ).

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

fof(f33,plain,
    ! [X0] : multiply(inverse(inverse(X0)),identity) = X0,
    inference(superposition,[],[f27,f3]) ).

fof(f35,plain,
    ! [X0] : multiply(inverse(X0),X0) = commutator(X0,X0),
    inference(superposition,[],[f5,f27]) ).

fof(f37,plain,
    ! [X0,X1] : commutator(inverse(X1),multiply(X1,X0)) = multiply(inverse(inverse(X1)),multiply(inverse(multiply(X1,X0)),X0)),
    inference(superposition,[],[f5,f27]) ).

fof(f41,plain,
    ! [X0] : identity = commutator(X0,X0),
    inference(forward_demodulation,[],[f35,f3]) ).

fof(f44,plain,
    ! [X0,X1] : commutator(inverse(X1),multiply(X1,X0)) = multiply(X1,multiply(inverse(multiply(X1,X0)),X0)),
    inference(backward_demodulation,[],[f37,f32]) ).

fof(f45,plain,
    ! [X0] : multiply(X0,identity) = X0,
    inference(backward_demodulation,[],[f33,f32]) ).

fof(f46,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(X0,X1)) = multiply(X0,commutator(X0,X1)),
    inference(forward_demodulation,[],[f31,f32]) ).

fof(f50,plain,
    ! [X0] : commutator(X0,identity) = multiply(inverse(X0),multiply(inverse(identity),X0)),
    inference(superposition,[],[f5,f45]) ).

fof(f53,plain,
    identity = inverse(identity),
    inference(superposition,[],[f3,f45]) ).

fof(f55,plain,
    ! [X0] : multiply(inverse(X0),multiply(identity,X0)) = commutator(X0,identity),
    inference(forward_demodulation,[],[f50,f53]) ).

fof(f56,plain,
    ! [X0] : commutator(X0,identity) = multiply(identity,commutator(identity,X0)),
    inference(forward_demodulation,[],[f55,f46]) ).

fof(f57,plain,
    ! [X0] : commutator(identity,X0) = commutator(X0,identity),
    inference(forward_demodulation,[],[f56,f1]) ).

fof(f58,plain,
    ! [X0] : identity = commutator(X0,identity),
    inference(forward_demodulation,[],[f57,f24]) ).

fof(f63,plain,
    ! [X0,X1] : commutator(X1,inverse(X0)) = multiply(inverse(X1),multiply(X0,multiply(X1,inverse(X0)))),
    inference(superposition,[],[f5,f32]) ).

fof(f64,plain,
    ! [X0,X1] : commutator(inverse(X0),X1) = multiply(X0,multiply(inverse(X1),multiply(inverse(X0),X1))),
    inference(superposition,[],[f5,f32]) ).

fof(f65,plain,
    ! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = X1,
    inference(superposition,[],[f27,f32]) ).

fof(f66,plain,
    ! [X0] : identity = multiply(X0,inverse(X0)),
    inference(superposition,[],[f3,f32]) ).

fof(f70,plain,
    ! [X0] : inverse(inverse(X0)) = multiply(X0,identity),
    inference(superposition,[],[f45,f32]) ).

fof(f71,plain,
    ! [X0] : inverse(inverse(X0)) = X0,
    inference(forward_demodulation,[],[f70,f45]) ).

fof(f82,plain,
    ! [X0,X1] : commutator(inverse(X0),commutator(X0,X1)) = commutator(identity,X1),
    inference(superposition,[],[f6,f28]) ).

fof(f83,plain,
    ! [X0,X1] : identity = commutator(inverse(X0),commutator(X0,X1)),
    inference(forward_demodulation,[],[f82,f24]) ).

fof(f85,plain,
    ! [X0,X1] : commutator(identity,X1) = commutator(X0,commutator(X0,X1)),
    inference(superposition,[],[f6,f41]) ).

fof(f87,plain,
    ! [X0,X1] : identity = commutator(X0,commutator(X0,X1)),
    inference(forward_demodulation,[],[f85,f24]) ).

fof(f100,plain,
    ! [X0,X1] : multiply(X0,multiply(X1,inverse(X0))) = multiply(X1,commutator(X1,inverse(X0))),
    inference(superposition,[],[f46,f71]) ).

fof(f102,plain,
    ! [X0,X1] : multiply(X1,commutator(X1,commutator(X1,X0))) = multiply(inverse(commutator(X1,X0)),multiply(inverse(X0),multiply(X1,X0))),
    inference(superposition,[],[f46,f46]) ).

fof(f106,plain,
    ! [X0,X1] : multiply(inverse(multiply(X1,X0)),X0) = multiply(inverse(X1),commutator(inverse(X1),multiply(X1,X0))),
    inference(superposition,[],[f46,f27]) ).

fof(f110,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(commutator(X0,X1),X2)) = multiply(commutator(X0,X1),commutator(X0,commutator(X1,X2))),
    inference(superposition,[],[f46,f6]) ).

fof(f114,plain,
    ! [X0,X1] : multiply(X0,X1) = multiply(inverse(inverse(X1)),multiply(X0,commutator(X0,X1))),
    inference(superposition,[],[f27,f46]) ).

fof(f126,plain,
    ! [X0,X1] : multiply(X0,X1) = multiply(X1,multiply(X0,commutator(X0,X1))),
    inference(forward_demodulation,[],[f114,f71]) ).

fof(f132,plain,
    ! [X0,X1] : multiply(X1,identity) = multiply(inverse(commutator(X1,X0)),multiply(inverse(X0),multiply(X1,X0))),
    inference(forward_demodulation,[],[f102,f87]) ).

fof(f137,plain,
    ! [X0,X1] : multiply(inverse(commutator(X1,X0)),multiply(inverse(X0),multiply(X1,X0))) = X1,
    inference(forward_demodulation,[],[f132,f45]) ).

fof(f169,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(X0,X1)) = multiply(inverse(inverse(commutator(X0,X1))),X0),
    inference(superposition,[],[f27,f137]) ).

fof(f174,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(X0,X1)) = multiply(commutator(X0,X1),X0),
    inference(forward_demodulation,[],[f169,f71]) ).

fof(f222,plain,
    ! [X0,X1] : multiply(X0,commutator(X0,X1)) = multiply(commutator(X0,X1),X0),
    inference(superposition,[],[f46,f174]) ).

fof(f232,plain,
    ! [X0,X1] : commutator(commutator(X1,X0),X1) = multiply(inverse(commutator(X1,X0)),multiply(inverse(X1),multiply(inverse(X0),multiply(X1,X0)))),
    inference(superposition,[],[f5,f174]) ).

fof(f235,plain,
    ! [X0,X1] : commutator(commutator(X1,X0),X1) = multiply(inverse(commutator(X1,X0)),commutator(X1,X0)),
    inference(forward_demodulation,[],[f232,f5]) ).

fof(f257,plain,
    ! [X0,X1] : identity = commutator(commutator(X1,X0),X1),
    inference(forward_demodulation,[],[f235,f3]) ).

fof(f268,plain,
    ! [X0,X1] : identity = commutator(X1,commutator(X0,X1)),
    inference(forward_demodulation,[],[f257,f6]) ).

fof(f307,plain,
    ! [X2,X0,X1] : multiply(multiply(X0,commutator(X0,X1)),X2) = multiply(commutator(X0,X1),multiply(X0,X2)),
    inference(superposition,[],[f4,f222]) ).

fof(f309,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(commutator(X0,X1),X2)) = multiply(commutator(X0,X1),multiply(X0,X2)),
    inference(forward_demodulation,[],[f307,f4]) ).

fof(f384,plain,
    ! [X0,X1] : multiply(X0,commutator(X1,X0)) = multiply(commutator(X1,X0),multiply(X0,identity)),
    inference(superposition,[],[f126,f268]) ).

fof(f388,plain,
    ! [X0,X1] : multiply(inverse(X0),commutator(X0,X1)) = multiply(commutator(X0,X1),multiply(inverse(X0),identity)),
    inference(superposition,[],[f126,f83]) ).

fof(f389,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),X2) = multiply(X2,multiply(commutator(X0,X1),commutator(X0,commutator(X1,X2)))),
    inference(superposition,[],[f126,f6]) ).

fof(f402,plain,
    ! [X0,X1] : commutator(X1,multiply(X0,commutator(X0,X1))) = multiply(inverse(X1),multiply(inverse(multiply(X0,commutator(X0,X1))),multiply(X0,X1))),
    inference(superposition,[],[f5,f126]) ).

fof(f403,plain,
    ! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X1,multiply(multiply(X0,commutator(X0,X1)),X2)),
    inference(superposition,[],[f4,f126]) ).

fof(f409,plain,
    ! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X1,multiply(X0,multiply(commutator(X0,X1),X2))),
    inference(forward_demodulation,[],[f403,f4]) ).

fof(f416,plain,
    ! [X0,X1] : multiply(inverse(X0),commutator(X0,X1)) = multiply(commutator(X0,X1),inverse(X0)),
    inference(forward_demodulation,[],[f388,f45]) ).

fof(f420,plain,
    ! [X0,X1] : multiply(X0,commutator(X1,X0)) = multiply(commutator(X1,X0),X0),
    inference(forward_demodulation,[],[f384,f45]) ).

fof(f422,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(X1,multiply(X0,multiply(commutator(X0,X1),X2))),
    inference(forward_demodulation,[],[f409,f4]) ).

fof(f502,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X0),multiply(X0,X2)) = multiply(multiply(X0,commutator(X1,X0)),X2),
    inference(superposition,[],[f4,f420]) ).

fof(f504,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X0),multiply(X0,X2)) = multiply(X0,multiply(commutator(X1,X0),X2)),
    inference(forward_demodulation,[],[f502,f4]) ).

fof(f556,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(commutator(X0,X1),inverse(X2))) = multiply(commutator(X0,X1),commutator(X0,commutator(X1,inverse(X2)))),
    inference(superposition,[],[f100,f6]) ).

fof(f667,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),X0) = multiply(inverse(multiply(X1,X2)),multiply(X1,X0)),
    inference(superposition,[],[f29,f65]) ).

fof(f670,plain,
    ! [X0,X1] : inverse(X1) = multiply(inverse(multiply(X0,X1)),multiply(X0,identity)),
    inference(superposition,[],[f29,f66]) ).

fof(f687,plain,
    ! [X0,X1] : commutator(X0,X1) = multiply(inverse(multiply(X1,X0)),multiply(X0,X1)),
    inference(superposition,[],[f29,f126]) ).

fof(f691,plain,
    ! [X0,X1] : multiply(X0,X1) = multiply(inverse(multiply(inverse(X0),inverse(X1))),commutator(X0,X1)),
    inference(superposition,[],[f29,f5]) ).

fof(f706,plain,
    ! [X0] : multiply(inverse(X0),X0) = commutator(X0,multiply(X0,X0)),
    inference(superposition,[],[f5,f29]) ).

fof(f718,plain,
    ! [X0] : identity = commutator(X0,multiply(X0,X0)),
    inference(forward_demodulation,[],[f706,f3]) ).

fof(f739,plain,
    ! [X0,X1] : inverse(X1) = multiply(inverse(multiply(X0,X1)),X0),
    inference(forward_demodulation,[],[f670,f45]) ).

fof(f752,plain,
    ! [X0,X1] : commutator(X1,multiply(X0,commutator(X0,X1))) = multiply(inverse(X1),multiply(inverse(commutator(X0,X1)),X1)),
    inference(backward_demodulation,[],[f402,f667]) ).

fof(f859,plain,
    ! [X0,X1] : multiply(inverse(X0),commutator(X0,X1)) = multiply(inverse(multiply(inverse(inverse(X0)),inverse(commutator(X0,X1)))),identity),
    inference(superposition,[],[f691,f83]) ).

fof(f863,plain,
    ! [X0,X1] : commutator(inverse(multiply(inverse(X0),inverse(X1))),commutator(X0,X1)) = multiply(inverse(inverse(multiply(inverse(X0),inverse(X1)))),multiply(inverse(commutator(X0,X1)),multiply(X0,X1))),
    inference(superposition,[],[f5,f691]) ).

fof(f867,plain,
    ! [X0,X1] : commutator(inverse(multiply(inverse(X0),inverse(X1))),commutator(X0,X1)) = multiply(multiply(inverse(X0),inverse(X1)),multiply(inverse(commutator(X0,X1)),multiply(X0,X1))),
    inference(forward_demodulation,[],[f863,f71]) ).

fof(f870,plain,
    ! [X0,X1] : multiply(inverse(X0),commutator(X0,X1)) = inverse(multiply(inverse(inverse(X0)),inverse(commutator(X0,X1)))),
    inference(forward_demodulation,[],[f859,f45]) ).

fof(f883,plain,
    ! [X0,X1] : commutator(inverse(multiply(inverse(X0),inverse(X1))),commutator(X0,X1)) = multiply(inverse(X0),multiply(inverse(X1),multiply(inverse(commutator(X0,X1)),multiply(X0,X1)))),
    inference(forward_demodulation,[],[f867,f4]) ).

fof(f884,plain,
    ! [X0,X1] : multiply(inverse(X0),commutator(X0,X1)) = inverse(multiply(X0,inverse(commutator(X0,X1)))),
    inference(forward_demodulation,[],[f870,f71]) ).

fof(f912,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,inverse(commutator(X0,X1))),X2) = multiply(multiply(inverse(X0),commutator(X0,X1)),multiply(inverse(X2),multiply(multiply(X0,inverse(commutator(X0,X1))),X2))),
    inference(superposition,[],[f5,f884]) ).

fof(f939,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,inverse(commutator(X0,X1))),X2) = multiply(inverse(X0),multiply(commutator(X0,X1),multiply(inverse(X2),multiply(multiply(X0,inverse(commutator(X0,X1))),X2)))),
    inference(forward_demodulation,[],[f912,f4]) ).

fof(f958,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,inverse(commutator(X0,X1))),X2) = multiply(inverse(X0),multiply(commutator(X0,X1),multiply(inverse(X2),multiply(X0,multiply(inverse(commutator(X0,X1)),X2))))),
    inference(forward_demodulation,[],[f939,f4]) ).

fof(f1032,plain,
    ! [X0,X1] : multiply(inverse(X0),X1) = inverse(multiply(inverse(X1),X0)),
    inference(superposition,[],[f739,f65]) ).

fof(f1033,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,X1)),X1) = inverse(multiply(X0,commutator(X0,X1))),
    inference(superposition,[],[f739,f126]) ).

fof(f1036,plain,
    ! [X0,X1] : inverse(commutator(X1,X0)) = multiply(inverse(multiply(inverse(X0),multiply(X1,X0))),X1),
    inference(superposition,[],[f739,f46]) ).

fof(f1041,plain,
    ! [X0,X1] : inverse(multiply(X1,X0)) = multiply(inverse(X0),inverse(X1)),
    inference(superposition,[],[f739,f27]) ).

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

fof(f1070,plain,
    ! [X0,X1] : inverse(X1) = multiply(X0,inverse(multiply(X1,X0))),
    inference(forward_demodulation,[],[f1047,f71]) ).

fof(f1078,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(inverse(X1),multiply(inverse(commutator(X0,X1)),multiply(X0,X1)))) = commutator(inverse(inverse(multiply(X1,X0))),commutator(X0,X1)),
    inference(backward_demodulation,[],[f883,f1041]) ).

fof(f1100,plain,
    ! [X0,X1] : inverse(commutator(X1,X0)) = multiply(multiply(inverse(multiply(X1,X0)),X0),X1),
    inference(backward_demodulation,[],[f1036,f1032]) ).

fof(f1125,plain,
    ! [X0,X1] : multiply(inverse(X0),multiply(inverse(X1),multiply(inverse(commutator(X0,X1)),multiply(X0,X1)))) = commutator(multiply(X1,X0),commutator(X0,X1)),
    inference(forward_demodulation,[],[f1078,f71]) ).

fof(f1136,plain,
    ! [X0,X1] : inverse(commutator(X1,X0)) = multiply(inverse(multiply(X1,X0)),multiply(X0,X1)),
    inference(forward_demodulation,[],[f1100,f4]) ).

fof(f1158,plain,
    ! [X0,X1] : commutator(X0,X1) = inverse(commutator(X1,X0)),
    inference(forward_demodulation,[],[f1136,f687]) ).

fof(f1174,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(commutator(X1,X0),X1)) = commutator(X1,multiply(X0,commutator(X0,X1))),
    inference(backward_demodulation,[],[f752,f1158]) ).

fof(f1175,plain,
    ! [X0,X1] : multiply(inverse(X0),commutator(X0,X1)) = inverse(multiply(X0,commutator(X1,X0))),
    inference(backward_demodulation,[],[f884,f1158]) ).

fof(f1186,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,commutator(X1,X0)),X2) = multiply(inverse(X0),multiply(commutator(X0,X1),multiply(inverse(X2),multiply(X0,multiply(commutator(X1,X0),X2))))),
    inference(backward_demodulation,[],[f958,f1158]) ).

fof(f1190,plain,
    ! [X0,X1] : commutator(multiply(X1,X0),commutator(X0,X1)) = multiply(inverse(X0),multiply(inverse(X1),multiply(commutator(X1,X0),multiply(X0,X1)))),
    inference(backward_demodulation,[],[f1125,f1158]) ).

fof(f1214,plain,
    ! [X0,X1] : commutator(multiply(X1,X0),commutator(X0,X1)) = multiply(inverse(X0),multiply(inverse(X1),multiply(X0,multiply(commutator(X1,X0),X1)))),
    inference(forward_demodulation,[],[f1190,f504]) ).

fof(f1219,plain,
    ! [X0,X1] : multiply(inverse(X1),multiply(X1,commutator(X1,X0))) = commutator(X1,multiply(X0,commutator(X0,X1))),
    inference(forward_demodulation,[],[f1174,f222]) ).

fof(f1228,plain,
    ! [X0,X1] : commutator(multiply(X1,X0),commutator(X0,X1)) = multiply(inverse(X0),multiply(inverse(X1),multiply(X0,multiply(X1,commutator(X1,X0))))),
    inference(forward_demodulation,[],[f1214,f222]) ).

fof(f1231,plain,
    ! [X0,X1] : commutator(X1,X0) = commutator(X1,multiply(X0,commutator(X0,X1))),
    inference(forward_demodulation,[],[f1219,f27]) ).

fof(f1237,plain,
    ! [X0,X1] : commutator(multiply(X1,X0),commutator(X0,X1)) = multiply(commutator(X0,X1),commutator(X1,X0)),
    inference(forward_demodulation,[],[f1228,f23]) ).

fof(f1262,plain,
    ! [X0,X1] : identity = multiply(multiply(inverse(X0),commutator(X0,X1)),multiply(X0,commutator(X1,X0))),
    inference(superposition,[],[f3,f1175]) ).

fof(f1265,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(X0),commutator(X0,X1)),multiply(multiply(X0,commutator(X1,X0)),X2)) = X2,
    inference(superposition,[],[f27,f1175]) ).

fof(f1284,plain,
    ! [X2,X0,X1] : multiply(inverse(X0),multiply(commutator(X0,X1),multiply(multiply(X0,commutator(X1,X0)),X2))) = X2,
    inference(forward_demodulation,[],[f1265,f4]) ).

fof(f1287,plain,
    ! [X0,X1] : identity = multiply(inverse(X0),multiply(commutator(X0,X1),multiply(X0,commutator(X1,X0)))),
    inference(forward_demodulation,[],[f1262,f4]) ).

fof(f1304,plain,
    ! [X2,X0,X1] : multiply(inverse(X0),multiply(commutator(X0,X1),multiply(X0,multiply(commutator(X1,X0),X2)))) = X2,
    inference(forward_demodulation,[],[f1284,f4]) ).

fof(f1306,plain,
    ! [X0,X1] : identity = multiply(inverse(X0),multiply(X0,multiply(commutator(X0,X1),commutator(X1,X0)))),
    inference(forward_demodulation,[],[f1287,f309]) ).

fof(f1319,plain,
    ! [X2,X0,X1] : multiply(inverse(X0),multiply(X0,multiply(commutator(X0,X1),multiply(commutator(X1,X0),X2)))) = X2,
    inference(forward_demodulation,[],[f1304,f309]) ).

fof(f1320,plain,
    ! [X0,X1] : identity = multiply(commutator(X0,X1),commutator(X1,X0)),
    inference(forward_demodulation,[],[f1306,f27]) ).

fof(f1328,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),multiply(commutator(X1,X0),X2)) = X2,
    inference(forward_demodulation,[],[f1319,f27]) ).

fof(f1329,plain,
    ! [X0,X1] : identity = commutator(multiply(X1,X0),commutator(X0,X1)),
    inference(backward_demodulation,[],[f1237,f1320]) ).

fof(f1377,plain,
    ! [X2,X0,X1] : inverse(multiply(commutator(X1,X2),X0)) = multiply(inverse(X0),commutator(X2,X1)),
    inference(superposition,[],[f739,f1328]) ).

fof(f1493,plain,
    ! [X0,X1] : commutator(X0,X1) = commutator(X0,multiply(inverse(X0),multiply(X1,X0))),
    inference(superposition,[],[f1231,f46]) ).

fof(f1538,plain,
    ! [X0] : inverse(identity) = commutator(multiply(X0,X0),X0),
    inference(superposition,[],[f1158,f718]) ).

fof(f1579,plain,
    ! [X0] : identity = commutator(multiply(X0,X0),X0),
    inference(forward_demodulation,[],[f1538,f53]) ).

fof(f1601,plain,
    ! [X0,X1] : commutator(identity,X1) = commutator(multiply(X0,X0),commutator(X0,X1)),
    inference(superposition,[],[f6,f1579]) ).

fof(f1630,plain,
    ! [X0,X1] : identity = commutator(multiply(X0,X0),commutator(X0,X1)),
    inference(forward_demodulation,[],[f1601,f24]) ).

fof(f1728,plain,
    ! [X0,X1] : multiply(X0,inverse(X1)) = inverse(multiply(X1,inverse(X0))),
    inference(superposition,[],[f1041,f71]) ).

fof(f1730,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),inverse(X2)) = inverse(multiply(X2,commutator(X1,X0))),
    inference(superposition,[],[f1041,f1158]) ).

fof(f1740,plain,
    ! [X0,X1] : multiply(inverse(X1),commutator(inverse(X1),inverse(X0))) = multiply(X0,inverse(multiply(X0,X1))),
    inference(superposition,[],[f100,f1041]) ).

fof(f1744,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X0,X1)),X2) = multiply(inverse(X1),multiply(inverse(X0),X2)),
    inference(superposition,[],[f4,f1041]) ).

fof(f1757,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),X2) = multiply(inverse(multiply(X1,X0)),multiply(X0,multiply(X1,X2))),
    inference(backward_demodulation,[],[f23,f1744]) ).

fof(f1759,plain,
    ! [X0,X1] : multiply(X0,multiply(inverse(multiply(X0,X1)),X1)) = commutator(inverse(X0),X1),
    inference(backward_demodulation,[],[f64,f1744]) ).

fof(f1760,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X1),X2) = multiply(inverse(multiply(X2,multiply(X0,X1))),multiply(X0,multiply(X1,X2))),
    inference(backward_demodulation,[],[f17,f1744]) ).

fof(f1767,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,X1)),X1) = multiply(commutator(X1,X0),inverse(X0)),
    inference(backward_demodulation,[],[f1033,f1730]) ).

fof(f1781,plain,
    ! [X0,X1] : commutator(inverse(X1),multiply(X1,X0)) = commutator(inverse(X1),X0),
    inference(backward_demodulation,[],[f44,f1759]) ).

fof(f1792,plain,
    ! [X0,X1] : multiply(inverse(multiply(X1,X0)),X0) = multiply(inverse(X1),commutator(inverse(X1),X0)),
    inference(backward_demodulation,[],[f106,f1781]) ).

fof(f1800,plain,
    ! [X0,X1] : commutator(X0,X1) = commutator(X0,multiply(inverse(X0),X1)),
    inference(superposition,[],[f1781,f71]) ).

fof(f1809,plain,
    ! [X2,X0,X1] : commutator(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = commutator(inverse(multiply(X0,X1)),X2),
    inference(superposition,[],[f1781,f4]) ).

fof(f1812,plain,
    ! [X0,X1] : commutator(inverse(inverse(X1)),multiply(X1,X0)) = commutator(inverse(inverse(X1)),X0),
    inference(superposition,[],[f1781,f27]) ).

fof(f1831,plain,
    ! [X0,X1] : inverse(commutator(inverse(X0),X1)) = commutator(multiply(X0,X1),inverse(X0)),
    inference(superposition,[],[f1158,f1781]) ).

fof(f1837,plain,
    ! [X0,X1] : commutator(X1,inverse(X0)) = commutator(multiply(X0,X1),inverse(X0)),
    inference(forward_demodulation,[],[f1831,f1158]) ).

fof(f1851,plain,
    ! [X0,X1] : commutator(X1,X0) = commutator(X1,multiply(X1,X0)),
    inference(forward_demodulation,[],[f1812,f71]) ).

fof(f1864,plain,
    ! [X0,X1] : commutator(X0,X1) = commutator(X0,multiply(X1,X0)),
    inference(backward_demodulation,[],[f1493,f1800]) ).

fof(f1900,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X1),X2) = commutator(multiply(X0,X1),multiply(X0,multiply(X1,X2))),
    inference(superposition,[],[f1851,f4]) ).

fof(f1924,plain,
    ! [X0,X1] : inverse(commutator(X0,X1)) = commutator(multiply(X0,X1),X0),
    inference(superposition,[],[f1158,f1851]) ).

fof(f1933,plain,
    ! [X0,X1] : commutator(X1,X0) = commutator(multiply(X0,X1),X0),
    inference(forward_demodulation,[],[f1924,f1158]) ).

fof(f1967,plain,
    ! [X0,X1] : commutator(multiply(inverse(X1),X0),X1) = commutator(multiply(inverse(X1),X0),X0),
    inference(superposition,[],[f1864,f65]) ).

fof(f1977,plain,
    ! [X0,X1] : commutator(multiply(X1,X0),inverse(X1)) = commutator(multiply(X1,X0),X0),
    inference(superposition,[],[f1864,f27]) ).

fof(f1997,plain,
    ! [X0,X1] : inverse(commutator(X0,X1)) = commutator(multiply(X1,X0),X0),
    inference(superposition,[],[f1158,f1864]) ).

fof(f2008,plain,
    ! [X0,X1] : commutator(X1,X0) = commutator(multiply(X1,X0),X0),
    inference(forward_demodulation,[],[f1997,f1158]) ).

fof(f2017,plain,
    ! [X0,X1] : commutator(X0,inverse(X1)) = commutator(multiply(X1,X0),X0),
    inference(forward_demodulation,[],[f1977,f1837]) ).

fof(f2029,plain,
    ! [X0,X1] : commutator(inverse(X1),X0) = commutator(multiply(inverse(X1),X0),X1),
    inference(backward_demodulation,[],[f1967,f2008]) ).

fof(f2034,plain,
    ! [X0,X1] : commutator(X1,X0) = commutator(X0,inverse(X1)),
    inference(forward_demodulation,[],[f2017,f2008]) ).

fof(f2046,plain,
    ! [X0,X1] : commutator(X0,X1) = multiply(inverse(X1),multiply(X0,multiply(X1,inverse(X0)))),
    inference(backward_demodulation,[],[f63,f2034]) ).

fof(f2047,plain,
    ! [X0,X1] : multiply(X0,multiply(X1,inverse(X0))) = multiply(X1,commutator(X0,X1)),
    inference(backward_demodulation,[],[f100,f2034]) ).

fof(f2051,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(commutator(X0,X1),inverse(X2))) = multiply(commutator(X0,X1),commutator(X0,commutator(X2,X1))),
    inference(backward_demodulation,[],[f556,f2034]) ).

fof(f2069,plain,
    ! [X0,X1] : multiply(X0,inverse(multiply(X0,X1))) = multiply(inverse(X1),commutator(X0,inverse(X1))),
    inference(backward_demodulation,[],[f1740,f2034]) ).

fof(f2083,plain,
    ! [X0,X1] : multiply(X0,inverse(multiply(X0,X1))) = multiply(inverse(X1),commutator(X1,X0)),
    inference(forward_demodulation,[],[f2069,f2034]) ).

fof(f2098,plain,
    ! [X0,X1] : commutator(X1,X0) = commutator(inverse(X0),X1),
    inference(superposition,[],[f2034,f71]) ).

fof(f2099,plain,
    ! [X2,X0,X1] : commutator(X2,commutator(X0,X1)) = commutator(commutator(X1,X0),X2),
    inference(superposition,[],[f2034,f1158]) ).

fof(f2105,plain,
    ! [X2,X0,X1] : commutator(commutator(X0,X1),X2) = commutator(X1,commutator(inverse(X0),X2)),
    inference(superposition,[],[f6,f2034]) ).

fof(f2109,plain,
    ! [X0,X1] : multiply(X1,inverse(X0)) = multiply(inverse(X0),multiply(X1,commutator(X0,X1))),
    inference(superposition,[],[f126,f2034]) ).

fof(f2110,plain,
    ! [X0,X1] : multiply(inverse(inverse(X0)),multiply(X1,inverse(X0))) = multiply(commutator(X0,X1),X1),
    inference(superposition,[],[f174,f2034]) ).

fof(f2113,plain,
    ! [X0,X1] : multiply(inverse(X1),commutator(X0,X1)) = multiply(commutator(X0,X1),inverse(X1)),
    inference(superposition,[],[f416,f2034]) ).

fof(f2122,plain,
    ! [X2,X0,X1] : commutator(X0,commutator(X1,X2)) = commutator(X1,commutator(X2,inverse(X0))),
    inference(superposition,[],[f6,f2034]) ).

fof(f2123,plain,
    ! [X2,X0,X1] : commutator(X0,commutator(X1,X2)) = commutator(X1,commutator(X0,X2)),
    inference(forward_demodulation,[],[f2122,f2034]) ).

fof(f2126,plain,
    ! [X0,X1] : multiply(X0,multiply(X1,inverse(X0))) = multiply(commutator(X0,X1),X1),
    inference(forward_demodulation,[],[f2110,f71]) ).

fof(f2128,plain,
    ! [X2,X0,X1] : commutator(X0,commutator(X1,X2)) = commutator(X1,commutator(inverse(X0),X2)),
    inference(forward_demodulation,[],[f2105,f6]) ).

fof(f2142,plain,
    ! [X0,X1] : multiply(inverse(multiply(X1,X0)),X0) = multiply(inverse(X1),commutator(X0,X1)),
    inference(backward_demodulation,[],[f1792,f2098]) ).

fof(f2148,plain,
    ! [X0,X1] : commutator(X0,X1) = commutator(multiply(inverse(X1),X0),X1),
    inference(backward_demodulation,[],[f2029,f2098]) ).

fof(f2165,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,X1)) = commutator(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))),
    inference(backward_demodulation,[],[f1809,f2098]) ).

fof(f2168,plain,
    ! [X2,X0,X1] : commutator(X0,commutator(X1,X2)) = commutator(X1,commutator(X2,X0)),
    inference(forward_demodulation,[],[f2128,f2098]) ).

fof(f2171,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,X1)) = commutator(multiply(X0,multiply(X1,X2)),multiply(X0,X1)),
    inference(forward_demodulation,[],[f2165,f2098]) ).

fof(f2216,plain,
    ! [X0,X1] : multiply(inverse(X1),X0) = multiply(X0,multiply(inverse(X1),commutator(X0,X1))),
    inference(superposition,[],[f126,f2098]) ).

fof(f2292,plain,
    ! [X2,X0,X1] : multiply(X2,commutator(X0,commutator(X1,X2))) = multiply(commutator(X0,X1),multiply(X2,inverse(commutator(X0,X1)))),
    inference(superposition,[],[f2047,f6]) ).

fof(f2342,plain,
    ! [X2,X0,X1] : multiply(X2,commutator(X0,commutator(X1,X2))) = multiply(commutator(X0,X1),multiply(X2,commutator(X1,X0))),
    inference(forward_demodulation,[],[f2292,f1158]) ).

fof(f2430,plain,
    ! [X0,X1] : multiply(inverse(multiply(multiply(X0,X1),X0)),X0) = multiply(inverse(multiply(X0,X1)),commutator(X0,X1)),
    inference(superposition,[],[f2142,f1851]) ).

fof(f2480,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,X1)),commutator(X0,X1)) = multiply(inverse(multiply(X0,multiply(X1,X0))),X0),
    inference(forward_demodulation,[],[f2430,f4]) ).

fof(f2520,plain,
    ! [X0,X1] : inverse(multiply(X1,X0)) = multiply(inverse(multiply(X0,X1)),commutator(X0,X1)),
    inference(forward_demodulation,[],[f2480,f739]) ).

fof(f2734,plain,
    ! [X0,X1] : multiply(commutator(X0,X1),inverse(multiply(commutator(X0,X1),multiply(X1,X0)))) = multiply(inverse(multiply(X1,X0)),identity),
    inference(superposition,[],[f2083,f1329]) ).

fof(f2737,plain,
    ! [X2,X0,X1] : multiply(inverse(commutator(X0,X1)),commutator(X0,commutator(X1,X2))) = multiply(X2,inverse(multiply(X2,commutator(X0,X1)))),
    inference(superposition,[],[f2083,f6]) ).

fof(f2791,plain,
    ! [X2,X0,X1] : multiply(inverse(commutator(X0,X1)),commutator(X0,commutator(X1,X2))) = multiply(X2,multiply(commutator(X1,X0),inverse(X2))),
    inference(forward_demodulation,[],[f2737,f1730]) ).

fof(f2793,plain,
    ! [X0,X1] : inverse(multiply(X1,X0)) = multiply(commutator(X0,X1),inverse(multiply(commutator(X0,X1),multiply(X1,X0)))),
    inference(forward_demodulation,[],[f2734,f45]) ).

fof(f2832,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X0),commutator(X0,commutator(X1,X2))) = multiply(X2,multiply(commutator(X1,X0),inverse(X2))),
    inference(forward_demodulation,[],[f2791,f1158]) ).

fof(f2834,plain,
    ! [X0,X1] : inverse(multiply(X1,X0)) = multiply(commutator(X0,X1),multiply(inverse(multiply(X1,X0)),commutator(X1,X0))),
    inference(forward_demodulation,[],[f2793,f1377]) ).

fof(f2866,plain,
    ! [X0,X1] : inverse(multiply(X1,X0)) = multiply(commutator(X0,X1),inverse(multiply(X0,X1))),
    inference(forward_demodulation,[],[f2834,f2520]) ).

fof(f3158,plain,
    ! [X2,X0,X1] : commutator(X2,commutator(X0,X1)) = commutator(X0,commutator(X2,multiply(X0,X1))),
    inference(superposition,[],[f2123,f1851]) ).

fof(f3166,plain,
    ! [X2,X0,X1] : commutator(X2,commutator(X0,X1)) = commutator(multiply(X1,X0),commutator(X2,X1)),
    inference(superposition,[],[f2123,f1933]) ).

fof(f3273,plain,
    ! [X2,X0,X1] : commutator(X2,commutator(X0,X1)) = commutator(X1,commutator(multiply(X1,X0),X2)),
    inference(forward_demodulation,[],[f3166,f2168]) ).

fof(f3492,plain,
    ! [X2,X0,X1] : multiply(X1,multiply(inverse(multiply(X0,X1)),X2)) = multiply(inverse(X0),X2),
    inference(superposition,[],[f4,f1070]) ).

fof(f5148,plain,
    ! [X2,X0,X1] : commutator(X2,commutator(X0,X1)) = commutator(X0,commutator(multiply(X1,X0),X2)),
    inference(superposition,[],[f2168,f1864]) ).

fof(f5687,plain,
    ! [X0,X1] : inverse(multiply(commutator(X0,X1),multiply(X0,X0))) = multiply(identity,inverse(multiply(multiply(X0,X0),commutator(X0,X1)))),
    inference(superposition,[],[f2866,f1630]) ).

fof(f5692,plain,
    ! [X0,X1] : inverse(multiply(commutator(X0,X1),multiply(X0,X0))) = inverse(multiply(multiply(X0,X0),commutator(X0,X1))),
    inference(forward_demodulation,[],[f5687,f1]) ).

fof(f5738,plain,
    ! [X0,X1] : inverse(multiply(commutator(X0,X1),multiply(X0,X0))) = multiply(commutator(X1,X0),inverse(multiply(X0,X0))),
    inference(forward_demodulation,[],[f5692,f1730]) ).

fof(f5773,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,X0)),commutator(X1,X0)) = multiply(commutator(X1,X0),inverse(multiply(X0,X0))),
    inference(forward_demodulation,[],[f5738,f1377]) ).

fof(f5875,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(X0),commutator(X1,X0)),X2) = multiply(commutator(X1,X0),multiply(inverse(X0),X2)),
    inference(superposition,[],[f4,f2113]) ).

fof(f5899,plain,
    ! [X2,X0,X1] : multiply(inverse(X0),multiply(commutator(X1,X0),X2)) = multiply(commutator(X1,X0),multiply(inverse(X0),X2)),
    inference(forward_demodulation,[],[f5875,f4]) ).

fof(f6542,plain,
    ! [X2,X0,X1] : multiply(commutator(inverse(multiply(X0,X1)),X1),X2) = multiply(inverse(inverse(X0)),multiply(inverse(multiply(X0,X1)),multiply(X1,X2))),
    inference(superposition,[],[f1757,f1070]) ).

fof(f6635,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,multiply(X1,X2)),inverse(multiply(X1,X0))) = commutator(multiply(commutator(X0,X1),X2),inverse(multiply(X1,X0))),
    inference(superposition,[],[f1933,f1757]) ).

fof(f6648,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,multiply(X1,X2)),inverse(multiply(X1,X0))) = commutator(multiply(X1,X0),multiply(commutator(X0,X1),X2)),
    inference(forward_demodulation,[],[f6635,f2034]) ).

fof(f6730,plain,
    ! [X2,X0,X1] : multiply(commutator(inverse(multiply(X0,X1)),X1),X2) = multiply(inverse(multiply(multiply(X0,X1),inverse(X0))),multiply(X1,X2)),
    inference(forward_demodulation,[],[f6542,f1744]) ).

fof(f6746,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),multiply(commutator(X0,X1),X2)) = commutator(multiply(X1,X0),multiply(X0,multiply(X1,X2))),
    inference(forward_demodulation,[],[f6648,f2034]) ).

fof(f6815,plain,
    ! [X2,X0,X1] : multiply(commutator(inverse(multiply(X0,X1)),X1),X2) = multiply(multiply(X0,inverse(multiply(X0,X1))),multiply(X1,X2)),
    inference(forward_demodulation,[],[f6730,f1728]) ).

fof(f6885,plain,
    ! [X2,X0,X1] : multiply(commutator(inverse(multiply(X0,X1)),X1),X2) = multiply(X0,multiply(inverse(multiply(X0,X1)),multiply(X1,X2))),
    inference(forward_demodulation,[],[f6815,f4]) ).

fof(f6931,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,multiply(X0,X1)),X2) = multiply(X0,multiply(inverse(multiply(X0,X1)),multiply(X1,X2))),
    inference(forward_demodulation,[],[f6885,f2098]) ).

fof(f6967,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X0),X2) = multiply(X0,multiply(inverse(multiply(X0,X1)),multiply(X1,X2))),
    inference(forward_demodulation,[],[f6931,f1864]) ).

fof(f7645,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,inverse(multiply(X1,X0))),commutator(X1,X0)) = multiply(inverse(multiply(inverse(multiply(X1,X0)),X2)),multiply(X2,inverse(multiply(X0,X1)))),
    inference(superposition,[],[f1757,f2520]) ).

fof(f7668,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,inverse(multiply(X1,X0))),commutator(X1,X0)) = multiply(multiply(inverse(X2),multiply(X1,X0)),multiply(X2,inverse(multiply(X0,X1)))),
    inference(forward_demodulation,[],[f7645,f1032]) ).

fof(f7748,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,inverse(multiply(X1,X0))),commutator(X1,X0)) = multiply(inverse(X2),multiply(multiply(X1,X0),multiply(X2,inverse(multiply(X0,X1))))),
    inference(forward_demodulation,[],[f7668,f4]) ).

fof(f7822,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,inverse(multiply(X1,X0))),commutator(X1,X0)) = multiply(inverse(X2),multiply(X1,multiply(X0,multiply(X2,inverse(multiply(X0,X1)))))),
    inference(forward_demodulation,[],[f7748,f4]) ).

fof(f7891,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(X1,multiply(X0,multiply(X2,inverse(multiply(X0,X1)))))) = multiply(commutator(multiply(X1,X0),X2),commutator(X1,X0)),
    inference(forward_demodulation,[],[f7822,f2034]) ).

fof(f8068,plain,
    ! [X2,X0,X1] : multiply(X2,inverse(multiply(X0,X1))) = inverse(multiply(X0,multiply(X1,inverse(X2)))),
    inference(superposition,[],[f1728,f4]) ).

fof(f8103,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,inverse(X1)),X2) = commutator(X2,multiply(X1,inverse(X0))),
    inference(superposition,[],[f2098,f1728]) ).

fof(f9788,plain,
    ! [X2,X0,X1] : commutator(multiply(inverse(X0),X1),X2) = commutator(X2,multiply(inverse(X1),X0)),
    inference(superposition,[],[f2098,f1032]) ).

fof(f10240,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,X0)),multiply(commutator(X1,inverse(multiply(X2,X0))),X2)) = multiply(commutator(X1,inverse(multiply(X2,X0))),inverse(X0)),
    inference(superposition,[],[f504,f739]) ).

fof(f10342,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X2,X0)),multiply(commutator(multiply(X2,X0),X1),X2)) = multiply(commutator(multiply(X2,X0),X1),inverse(X0)),
    inference(forward_demodulation,[],[f10240,f2034]) ).

fof(f11854,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,multiply(X1,X2)),inverse(multiply(X1,X0))) = multiply(inverse(multiply(commutator(X0,X1),X2)),multiply(multiply(X0,multiply(X1,X2)),inverse(multiply(X1,X0)))),
    inference(superposition,[],[f687,f1757]) ).

fof(f12028,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,multiply(X1,X2)),inverse(multiply(X1,X0))) = multiply(inverse(multiply(commutator(X0,X1),X2)),multiply(X0,multiply(multiply(X1,X2),inverse(multiply(X1,X0))))),
    inference(forward_demodulation,[],[f11854,f4]) ).

fof(f12131,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,multiply(X1,X2)),inverse(multiply(X1,X0))) = multiply(inverse(multiply(commutator(X0,X1),X2)),multiply(X0,multiply(X1,multiply(X2,inverse(multiply(X1,X0)))))),
    inference(forward_demodulation,[],[f12028,f4]) ).

fof(f12224,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,multiply(X1,X2)),inverse(multiply(X1,X0))) = multiply(multiply(inverse(X2),commutator(X1,X0)),multiply(X0,multiply(X1,multiply(X2,inverse(multiply(X1,X0)))))),
    inference(forward_demodulation,[],[f12131,f1377]) ).

fof(f12306,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,multiply(X1,X2)),inverse(multiply(X1,X0))) = multiply(inverse(X2),multiply(commutator(X1,X0),multiply(X0,multiply(X1,multiply(X2,inverse(multiply(X1,X0))))))),
    inference(forward_demodulation,[],[f12224,f4]) ).

fof(f12365,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,multiply(X1,X2)),inverse(multiply(X1,X0))) = multiply(inverse(X2),multiply(X0,multiply(commutator(X1,X0),multiply(X1,multiply(X2,inverse(multiply(X1,X0))))))),
    inference(forward_demodulation,[],[f12306,f504]) ).

fof(f12410,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,multiply(X1,X2)),inverse(multiply(X1,X0))) = multiply(inverse(X2),multiply(X0,multiply(X1,multiply(commutator(X1,X0),multiply(X2,inverse(multiply(X1,X0))))))),
    inference(forward_demodulation,[],[f12365,f309]) ).

fof(f12440,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,multiply(X1,X2)),inverse(multiply(X1,X0))) = multiply(inverse(X2),multiply(X1,multiply(X0,multiply(X2,inverse(multiply(X1,X0)))))),
    inference(forward_demodulation,[],[f12410,f422]) ).

fof(f12461,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),multiply(X0,multiply(X1,X2))) = multiply(inverse(X2),multiply(X1,multiply(X0,multiply(X2,inverse(multiply(X1,X0)))))),
    inference(forward_demodulation,[],[f12440,f2034]) ).

fof(f12476,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),multiply(commutator(X0,X1),X2)) = multiply(inverse(X2),multiply(X1,multiply(X0,multiply(X2,inverse(multiply(X1,X0)))))),
    inference(forward_demodulation,[],[f12461,f6746]) ).

fof(f15141,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,X1),multiply(X2,X0)) = commutator(multiply(inverse(X0),X1),multiply(X2,X0)),
    inference(superposition,[],[f2148,f667]) ).

fof(f15155,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,X1),inverse(multiply(X2,X0))) = multiply(inverse(multiply(inverse(X0),X1)),multiply(multiply(X2,X1),inverse(multiply(X2,X0)))),
    inference(superposition,[],[f687,f667]) ).

fof(f15161,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(multiply(X2,X1),inverse(multiply(X2,X0))),X3) = multiply(inverse(multiply(inverse(X0),X1)),multiply(multiply(X2,X1),multiply(inverse(multiply(X2,X0)),X3))),
    inference(superposition,[],[f1757,f667]) ).

fof(f15169,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(multiply(X2,X0))),commutator(multiply(X2,X1),inverse(multiply(X2,X0)))) = multiply(inverse(multiply(inverse(X0),X1)),multiply(X2,X1)),
    inference(superposition,[],[f2142,f667]) ).

fof(f15184,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(multiply(X2,X0))),commutator(multiply(X2,X1),inverse(multiply(X2,X0)))) = multiply(multiply(inverse(X1),X0),multiply(X2,X1)),
    inference(forward_demodulation,[],[f15169,f1032]) ).

fof(f15192,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(multiply(X2,X1),inverse(multiply(X2,X0))),X3) = multiply(inverse(multiply(inverse(X0),X1)),multiply(X2,multiply(X1,multiply(inverse(multiply(X2,X0)),X3)))),
    inference(forward_demodulation,[],[f15161,f4]) ).

fof(f15198,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,X1),inverse(multiply(X2,X0))) = multiply(inverse(multiply(inverse(X0),X1)),multiply(X2,multiply(X1,inverse(multiply(X2,X0))))),
    inference(forward_demodulation,[],[f15155,f4]) ).

fof(f15313,plain,
    ! [X2,X0,X1] : multiply(inverse(inverse(multiply(X2,X0))),commutator(multiply(X2,X1),inverse(multiply(X2,X0)))) = multiply(inverse(X1),multiply(X0,multiply(X2,X1))),
    inference(forward_demodulation,[],[f15184,f4]) ).

fof(f15319,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(multiply(X2,X1),inverse(multiply(X2,X0))),X3) = multiply(multiply(inverse(X1),X0),multiply(X2,multiply(X1,multiply(inverse(multiply(X2,X0)),X3)))),
    inference(forward_demodulation,[],[f15192,f1032]) ).

fof(f15323,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,X1),inverse(multiply(X2,X0))) = multiply(multiply(inverse(X1),X0),multiply(X2,multiply(X1,inverse(multiply(X2,X0))))),
    inference(forward_demodulation,[],[f15198,f1032]) ).

fof(f15412,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(X0,multiply(X2,X1))) = multiply(inverse(inverse(multiply(X2,X0))),commutator(multiply(X2,X0),multiply(X2,X1))),
    inference(forward_demodulation,[],[f15313,f2034]) ).

fof(f15416,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(multiply(X2,X1),inverse(multiply(X2,X0))),X3) = multiply(inverse(X1),multiply(X0,multiply(X2,multiply(X1,multiply(inverse(multiply(X2,X0)),X3))))),
    inference(forward_demodulation,[],[f15319,f4]) ).

fof(f15420,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,X1),inverse(multiply(X2,X0))) = multiply(inverse(X1),multiply(X0,multiply(X2,multiply(X1,inverse(multiply(X2,X0)))))),
    inference(forward_demodulation,[],[f15323,f4]) ).

fof(f15485,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(X0,multiply(X2,X1))) = multiply(multiply(X2,X0),commutator(multiply(X2,X0),multiply(X2,X1))),
    inference(forward_demodulation,[],[f15412,f71]) ).

fof(f15489,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(X0,multiply(X2,multiply(X1,multiply(inverse(multiply(X2,X0)),X3))))) = multiply(commutator(multiply(X2,X0),multiply(X2,X1)),X3),
    inference(forward_demodulation,[],[f15416,f2034]) ).

fof(f15491,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,X0),multiply(X2,X1)) = multiply(inverse(X1),multiply(X0,multiply(X2,multiply(X1,inverse(multiply(X2,X0)))))),
    inference(forward_demodulation,[],[f15420,f2034]) ).

fof(f15540,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(X0,multiply(X2,X1))) = multiply(X2,multiply(X0,commutator(multiply(X2,X0),multiply(X2,X1)))),
    inference(forward_demodulation,[],[f15485,f4]) ).

fof(f15542,plain,
    ! [X2,X0,X1] : multiply(commutator(multiply(X1,X0),X2),commutator(X1,X0)) = commutator(multiply(X0,X1),multiply(X0,X2)),
    inference(backward_demodulation,[],[f7891,f15491]) ).

fof(f15619,plain,
    ! [X2,X0,X1] : commutator(X1,multiply(X2,inverse(multiply(X1,X0)))) = commutator(multiply(X2,inverse(X0)),multiply(X2,inverse(multiply(X1,X0)))),
    inference(superposition,[],[f2171,f739]) ).

fof(f15622,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X1),multiply(X2,inverse(multiply(X1,X0)))) = commutator(multiply(X2,commutator(X0,X1)),multiply(X2,inverse(multiply(X1,X0)))),
    inference(superposition,[],[f2171,f687]) ).

fof(f15677,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,commutator(X0,X1))) = commutator(multiply(inverse(X1),multiply(multiply(X0,X1),X2)),multiply(X0,commutator(X0,X1))),
    inference(superposition,[],[f2171,f46]) ).

fof(f15806,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,commutator(X0,X1))) = commutator(multiply(inverse(X1),multiply(X0,multiply(X1,X2))),multiply(X0,commutator(X0,X1))),
    inference(forward_demodulation,[],[f15677,f4]) ).

fof(f16885,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X1),X2) = multiply(inverse(X2),multiply(X0,multiply(X1,multiply(X2,inverse(multiply(X0,X1)))))),
    inference(superposition,[],[f2046,f4]) ).

fof(f16983,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),X2) = commutator(multiply(X1,X0),multiply(commutator(X0,X1),X2)),
    inference(backward_demodulation,[],[f12476,f16885]) ).

fof(f17060,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),X2) = commutator(multiply(X1,X0),multiply(X0,multiply(X1,X2))),
    inference(backward_demodulation,[],[f6746,f16983]) ).

fof(f19074,plain,
    ! [X2,X0,X1] : commutator(multiply(inverse(X0),commutator(X1,X0)),X2) = commutator(multiply(inverse(X0),commutator(X1,X0)),multiply(X1,multiply(inverse(multiply(X0,X1)),X2))),
    inference(superposition,[],[f17060,f2142]) ).

fof(f19097,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X2),multiply(X0,commutator(X0,X1))) = commutator(multiply(X1,X2),multiply(X2,multiply(X0,X1))),
    inference(superposition,[],[f17060,f126]) ).

fof(f19149,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,inverse(multiply(X1,X0))),multiply(X1,X2)) = commutator(multiply(X0,inverse(multiply(X1,X0))),multiply(commutator(X0,X1),X2)),
    inference(superposition,[],[f17060,f1757]) ).

fof(f19246,plain,
    ! [X2,X0,X1] : commutator(inverse(X1),multiply(X1,X2)) = commutator(inverse(X1),multiply(commutator(X0,X1),X2)),
    inference(forward_demodulation,[],[f19149,f1070]) ).

fof(f19294,plain,
    ! [X2,X0,X1] : commutator(multiply(inverse(X0),commutator(X1,X0)),X2) = commutator(multiply(inverse(X0),commutator(X1,X0)),multiply(inverse(X0),X2)),
    inference(forward_demodulation,[],[f19074,f3492]) ).

fof(f19345,plain,
    ! [X2,X0,X1] : commutator(multiply(commutator(X0,X1),X2),X1) = commutator(inverse(X1),multiply(X1,X2)),
    inference(forward_demodulation,[],[f19246,f2098]) ).

fof(f19409,plain,
    ! [X2,X0,X1] : commutator(multiply(commutator(X0,X1),X2),X1) = commutator(multiply(X1,X2),X1),
    inference(forward_demodulation,[],[f19345,f2098]) ).

fof(f19449,plain,
    ! [X2,X0,X1] : commutator(X2,X1) = commutator(multiply(commutator(X0,X1),X2),X1),
    inference(forward_demodulation,[],[f19409,f1933]) ).

fof(f19570,plain,
    ! [X2,X0,X1] : commutator(inverse(X0),X2) = commutator(inverse(multiply(X0,commutator(X1,X2))),X2),
    inference(superposition,[],[f19449,f1070]) ).

fof(f19643,plain,
    ! [X2,X0,X1] : commutator(X0,inverse(X1)) = commutator(X1,multiply(commutator(X2,inverse(X1)),X0)),
    inference(superposition,[],[f2034,f19449]) ).

fof(f19659,plain,
    ! [X2,X0,X1] : commutator(X0,inverse(X1)) = commutator(X1,multiply(commutator(X1,X2),X0)),
    inference(forward_demodulation,[],[f19643,f2034]) ).

fof(f19722,plain,
    ! [X2,X0,X1] : commutator(inverse(X0),X2) = commutator(X2,multiply(X0,commutator(X1,X2))),
    inference(forward_demodulation,[],[f19570,f2098]) ).

fof(f19762,plain,
    ! [X2,X0,X1] : commutator(X1,X0) = commutator(X1,multiply(commutator(X1,X2),X0)),
    inference(forward_demodulation,[],[f19659,f2034]) ).

fof(f19814,plain,
    ! [X2,X0,X1] : commutator(X2,X0) = commutator(X2,multiply(X0,commutator(X1,X2))),
    inference(forward_demodulation,[],[f19722,f2098]) ).

fof(f20022,plain,
    ! [X2,X0,X1] : commutator(X1,inverse(X0)) = commutator(X1,inverse(multiply(X0,commutator(X1,X2)))),
    inference(superposition,[],[f19762,f1070]) ).

fof(f20139,plain,
    ! [X2,X0,X1] : commutator(X1,inverse(X0)) = commutator(multiply(X0,commutator(X1,X2)),X1),
    inference(forward_demodulation,[],[f20022,f2034]) ).

fof(f20214,plain,
    ! [X2,X0,X1] : commutator(X0,X1) = commutator(multiply(X0,commutator(X1,X2)),X1),
    inference(forward_demodulation,[],[f20139,f2034]) ).

fof(f20305,plain,
    ! [X2,X0,X1] : commutator(X2,X1) = commutator(multiply(X2,commutator(X0,X1)),X1),
    inference(superposition,[],[f20214,f2034]) ).

fof(f20715,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X1),X2) = commutator(multiply(X0,X1),multiply(X2,commutator(X0,X1))),
    inference(superposition,[],[f19814,f1851]) ).

fof(f20807,plain,
    ! [X2,X3,X0,X1] : commutator(X2,commutator(X0,X1)) = commutator(X0,commutator(X2,multiply(X1,commutator(X3,X0)))),
    inference(superposition,[],[f2123,f19814]) ).

fof(f22723,plain,
    ! [X2,X3,X0,X1] : inverse(multiply(commutator(X0,commutator(X1,X2)),X3)) = multiply(inverse(X3),commutator(X2,commutator(X0,X1))),
    inference(superposition,[],[f1377,f6]) ).

fof(f22786,plain,
    ! [X2,X3,X0,X1] : commutator(X3,multiply(commutator(X2,X1),X0)) = commutator(multiply(inverse(X0),commutator(X1,X2)),X3),
    inference(superposition,[],[f2098,f1377]) ).

fof(f22805,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(commutator(X0,X1),X0)) = commutator(multiply(inverse(X0),commutator(X1,X0)),multiply(inverse(X0),X2)),
    inference(backward_demodulation,[],[f19294,f22786]) ).

fof(f22895,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X3),commutator(X2,commutator(X0,X1))) = multiply(inverse(X3),commutator(commutator(X1,X2),X0)),
    inference(forward_demodulation,[],[f22723,f1377]) ).

fof(f22957,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(commutator(X0,X1),X0)) = commutator(multiply(inverse(X0),X2),multiply(commutator(X0,X1),X0)),
    inference(forward_demodulation,[],[f22805,f22786]) ).

fof(f23020,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X3),commutator(X1,commutator(X2,X0))) = multiply(inverse(X3),commutator(X2,commutator(X0,X1))),
    inference(forward_demodulation,[],[f22895,f6]) ).

fof(f23051,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,commutator(X0,X1))) = commutator(multiply(inverse(X0),X2),multiply(X0,commutator(X0,X1))),
    inference(forward_demodulation,[],[f22957,f222]) ).

fof(f24910,plain,
    ! [X2,X0,X1] : commutator(multiply(inverse(X1),X2),multiply(X0,commutator(X1,X0))) = commutator(multiply(inverse(X1),X2),multiply(X2,multiply(X0,inverse(X1)))),
    inference(superposition,[],[f17060,f2109]) ).

fof(f25301,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,inverse(multiply(X0,X1))),X1) = multiply(inverse(multiply(X1,multiply(X2,inverse(multiply(X0,X1))))),multiply(X2,multiply(inverse(X0),commutator(X1,X0)))),
    inference(superposition,[],[f1760,f2142]) ).

fof(f25320,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,commutator(X1,X0)),inverse(multiply(X0,X0))) = multiply(inverse(multiply(inverse(multiply(X0,X0)),multiply(X2,commutator(X1,X0)))),multiply(X2,multiply(inverse(multiply(X0,X0)),commutator(X1,X0)))),
    inference(superposition,[],[f1760,f5773]) ).

fof(f25477,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,commutator(X1,X0)),inverse(multiply(X0,X0))) = multiply(multiply(inverse(multiply(X2,commutator(X1,X0))),multiply(X0,X0)),multiply(X2,multiply(inverse(multiply(X0,X0)),commutator(X1,X0)))),
    inference(forward_demodulation,[],[f25320,f1032]) ).

fof(f25496,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,inverse(multiply(X0,X1))),X1) = multiply(multiply(multiply(X0,X1),inverse(multiply(X1,X2))),multiply(X2,multiply(inverse(X0),commutator(X1,X0)))),
    inference(forward_demodulation,[],[f25301,f8068]) ).

fof(f25661,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,commutator(X1,X0)),inverse(multiply(X0,X0))) = multiply(inverse(multiply(X2,commutator(X1,X0))),multiply(multiply(X0,X0),multiply(X2,multiply(inverse(multiply(X0,X0)),commutator(X1,X0))))),
    inference(forward_demodulation,[],[f25477,f4]) ).

fof(f25674,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,inverse(multiply(X0,X1))),X1) = multiply(multiply(X0,X1),multiply(inverse(multiply(X1,X2)),multiply(X2,multiply(inverse(X0),commutator(X1,X0))))),
    inference(forward_demodulation,[],[f25496,f4]) ).

fof(f25823,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,commutator(X1,X0)),inverse(multiply(X0,X0))) = multiply(inverse(multiply(X2,commutator(X1,X0))),multiply(X0,multiply(X0,multiply(X2,multiply(inverse(multiply(X0,X0)),commutator(X1,X0)))))),
    inference(forward_demodulation,[],[f25661,f4]) ).

fof(f25836,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,inverse(multiply(X0,X1))),X1) = multiply(X0,multiply(X1,multiply(inverse(multiply(X1,X2)),multiply(X2,multiply(inverse(X0),commutator(X1,X0)))))),
    inference(forward_demodulation,[],[f25674,f4]) ).

fof(f25955,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,commutator(X1,X0)),inverse(multiply(X0,X0))) = multiply(multiply(commutator(X0,X1),inverse(X2)),multiply(X0,multiply(X0,multiply(X2,multiply(inverse(multiply(X0,X0)),commutator(X1,X0)))))),
    inference(forward_demodulation,[],[f25823,f1730]) ).

fof(f25967,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,inverse(multiply(X0,X1))),X1) = multiply(X0,multiply(commutator(X2,X1),multiply(inverse(X0),commutator(X1,X0)))),
    inference(forward_demodulation,[],[f25836,f6967]) ).

fof(f26054,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,commutator(X1,X0)),inverse(multiply(X0,X0))) = multiply(commutator(X0,X1),multiply(inverse(X2),multiply(X0,multiply(X0,multiply(X2,multiply(inverse(multiply(X0,X0)),commutator(X1,X0))))))),
    inference(forward_demodulation,[],[f25955,f4]) ).

fof(f26065,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(commutator(X2,X1),multiply(inverse(X0),commutator(X1,X0)))) = commutator(X1,multiply(multiply(X0,X1),inverse(X2))),
    inference(forward_demodulation,[],[f25967,f8103]) ).

fof(f26122,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,commutator(X1,X0)),inverse(multiply(X0,X0))) = multiply(commutator(X0,X1),multiply(commutator(multiply(X0,X0),multiply(X0,X2)),commutator(X1,X0))),
    inference(forward_demodulation,[],[f26054,f15489]) ).

fof(f26132,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(commutator(X2,X1),multiply(inverse(X0),commutator(X1,X0)))) = commutator(X1,multiply(X0,multiply(X1,inverse(X2)))),
    inference(forward_demodulation,[],[f26065,f4]) ).

fof(f26167,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),multiply(commutator(multiply(X0,X0),multiply(X0,X2)),commutator(X1,X0))) = commutator(multiply(X0,X0),multiply(X2,commutator(X1,X0))),
    inference(forward_demodulation,[],[f26122,f2034]) ).

fof(f28399,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(commutator(multiply(X2,X1),X0),X2)),X2) = multiply(commutator(X0,commutator(X1,X2)),inverse(commutator(multiply(X2,X1),X0))),
    inference(superposition,[],[f1767,f3273]) ).

fof(f28458,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(commutator(multiply(X2,X1),X0),X2)),X2) = multiply(commutator(X0,commutator(X1,X2)),commutator(X0,multiply(X2,X1))),
    inference(forward_demodulation,[],[f28399,f1158]) ).

fof(f28584,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,commutator(X1,X2)),commutator(X0,multiply(X2,X1))) = multiply(multiply(inverse(X2),commutator(X0,multiply(X2,X1))),X2),
    inference(forward_demodulation,[],[f28458,f1377]) ).

fof(f28695,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,commutator(X1,X2)),commutator(X0,multiply(X2,X1))) = multiply(inverse(X2),multiply(commutator(X0,multiply(X2,X1)),X2)),
    inference(forward_demodulation,[],[f28584,f4]) ).

fof(f31002,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(X2,X3),commutator(X2,commutator(X3,multiply(inverse(X1),X0)))) = multiply(multiply(inverse(X0),X1),multiply(commutator(X2,X3),multiply(inverse(X1),X0))),
    inference(superposition,[],[f110,f1032]) ).

fof(f31023,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X2),commutator(X1,commutator(X2,multiply(X0,inverse(commutator(X1,X2)))))) = multiply(inverse(multiply(X0,inverse(commutator(X1,X2)))),multiply(X0,commutator(commutator(X1,X2),X0))),
    inference(superposition,[],[f110,f2047]) ).

fof(f31102,plain,
    ! [X2,X0,X1] : multiply(inverse(commutator(X0,X1)),multiply(commutator(X2,X0),commutator(X0,X1))) = multiply(commutator(X2,X0),commutator(X2,identity)),
    inference(superposition,[],[f110,f87]) ).

fof(f31164,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(commutator(multiply(X0,commutator(X1,X2)),X1),X2)) = multiply(commutator(multiply(X0,commutator(X1,X2)),X1),commutator(X0,commutator(X1,X2))),
    inference(superposition,[],[f110,f2008]) ).

fof(f31427,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(commutator(multiply(X0,commutator(X1,X2)),X1),X2)) = commutator(multiply(commutator(X1,X2),X0),multiply(commutator(X1,X2),X1)),
    inference(forward_demodulation,[],[f31164,f15542]) ).

fof(f31467,plain,
    ! [X2,X0,X1] : multiply(inverse(commutator(X0,X1)),multiply(commutator(X2,X0),commutator(X0,X1))) = multiply(commutator(X2,X0),identity),
    inference(forward_demodulation,[],[f31102,f58]) ).

fof(f31544,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X2),commutator(X1,commutator(X2,multiply(X0,inverse(commutator(X1,X2)))))) = multiply(inverse(inverse(commutator(X1,X2))),commutator(commutator(X1,X2),X0)),
    inference(forward_demodulation,[],[f31023,f667]) ).

fof(f31564,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(X2,X3),commutator(X2,commutator(X3,multiply(inverse(X1),X0)))) = multiply(inverse(X0),multiply(X1,multiply(commutator(X2,X3),multiply(inverse(X1),X0)))),
    inference(forward_demodulation,[],[f31002,f4]) ).

fof(f31672,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(commutator(multiply(X0,commutator(X1,X2)),X1),X2)) = commutator(multiply(inverse(X1),X0),multiply(commutator(X1,X2),X1)),
    inference(forward_demodulation,[],[f31427,f15141]) ).

fof(f31691,plain,
    ! [X2,X0,X1] : commutator(X2,X0) = multiply(inverse(commutator(X0,X1)),multiply(commutator(X2,X0),commutator(X0,X1))),
    inference(forward_demodulation,[],[f31467,f45]) ).

fof(f31742,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X2),commutator(X1,commutator(X2,multiply(X0,inverse(commutator(X1,X2)))))) = multiply(inverse(inverse(commutator(X1,X2))),commutator(X1,commutator(X2,X0))),
    inference(forward_demodulation,[],[f31544,f6]) ).

fof(f31846,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(commutator(multiply(X0,commutator(X1,X2)),X1),X2)) = commutator(multiply(inverse(X1),X0),multiply(X1,commutator(X1,X2))),
    inference(forward_demodulation,[],[f31672,f222]) ).

fof(f31858,plain,
    ! [X2,X0,X1] : commutator(X2,X0) = multiply(commutator(X1,X0),multiply(commutator(X2,X0),commutator(X0,X1))),
    inference(forward_demodulation,[],[f31691,f1158]) ).

fof(f31887,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X2),commutator(X1,commutator(X2,X0))) = multiply(commutator(X1,X2),commutator(X1,commutator(X2,multiply(X0,inverse(commutator(X1,X2)))))),
    inference(forward_demodulation,[],[f31742,f71]) ).

fof(f31970,plain,
    ! [X2,X0,X1] : commutator(X0,multiply(X1,commutator(X1,X2))) = multiply(inverse(X2),multiply(commutator(multiply(X0,commutator(X1,X2)),X1),X2)),
    inference(forward_demodulation,[],[f31846,f23051]) ).

fof(f32000,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X2),commutator(X1,commutator(X2,X0))) = multiply(commutator(X1,X2),commutator(X1,commutator(X2,multiply(X0,commutator(X2,X1))))),
    inference(forward_demodulation,[],[f31887,f1158]) ).

fof(f32072,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(commutator(X0,X1),X2)) = commutator(X0,multiply(X1,commutator(X1,X2))),
    inference(forward_demodulation,[],[f31970,f20214]) ).

fof(f32092,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X2),commutator(X1,commutator(X2,X0))) = multiply(commutator(X1,X2),commutator(X2,commutator(X1,X0))),
    inference(forward_demodulation,[],[f32000,f20807]) ).

fof(f32449,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),commutator(X1,X2)) = multiply(commutator(X1,X2),commutator(X0,X1)),
    inference(superposition,[],[f1328,f31858]) ).

fof(f33072,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,X1),commutator(X0,X1)) = multiply(commutator(X0,X1),commutator(X2,X1)),
    inference(superposition,[],[f32449,f2034]) ).

fof(f33163,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(X0,commutator(X1,X2)),commutator(X0,X3)) = multiply(commutator(X0,X3),commutator(X0,commutator(X1,X2))),
    inference(superposition,[],[f32449,f2099]) ).

fof(f35547,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,commutator(X1,X2)),commutator(multiply(X2,X1),X0)) = multiply(X1,multiply(commutator(multiply(X2,X1),X0),inverse(X1))),
    inference(superposition,[],[f2126,f5148]) ).

fof(f36172,plain,
    ! [X2,X3,X0,X1] : commutator(X3,multiply(inverse(X2),multiply(X1,inverse(X0)))) = commutator(multiply(multiply(X0,inverse(X1)),X2),X3),
    inference(superposition,[],[f9788,f1728]) ).

fof(f36699,plain,
    ! [X2,X3,X0,X1] : commutator(X3,multiply(inverse(X2),multiply(X1,inverse(X0)))) = commutator(multiply(X0,multiply(inverse(X1),X2)),X3),
    inference(forward_demodulation,[],[f36172,f4]) ).

fof(f37105,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,X1),commutator(X2,commutator(X0,X1))) = multiply(multiply(inverse(X1),X0),multiply(commutator(X2,X1),inverse(multiply(inverse(X1),X0)))),
    inference(superposition,[],[f2051,f2148]) ).

fof(f37469,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,X1),commutator(X2,commutator(X0,X1))) = multiply(inverse(X1),multiply(X0,multiply(commutator(X2,X1),inverse(multiply(inverse(X1),X0))))),
    inference(forward_demodulation,[],[f37105,f4]) ).

fof(f37707,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,X1),commutator(X2,commutator(X0,X1))) = multiply(inverse(X1),multiply(X0,multiply(commutator(X2,X1),multiply(inverse(X0),X1)))),
    inference(forward_demodulation,[],[f37469,f1032]) ).

fof(f38595,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X0,commutator(X1,commutator(X2,X0)))),multiply(X0,commutator(X2,X1))) = multiply(inverse(commutator(X1,X2)),commutator(multiply(X0,commutator(X2,X1)),commutator(X1,X2))),
    inference(superposition,[],[f2142,f2342]) ).

fof(f38630,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X0,commutator(X1,commutator(X2,X0)))),multiply(X0,commutator(X2,X1))) = multiply(inverse(commutator(X1,X2)),commutator(X1,commutator(X2,multiply(X0,commutator(X2,X1))))),
    inference(forward_demodulation,[],[f38595,f23020]) ).

fof(f38918,plain,
    ! [X2,X0,X1] : multiply(inverse(commutator(X1,X2)),commutator(X2,commutator(X1,X0))) = multiply(inverse(multiply(X0,commutator(X1,commutator(X2,X0)))),multiply(X0,commutator(X2,X1))),
    inference(forward_demodulation,[],[f38630,f20807]) ).

fof(f39156,plain,
    ! [X2,X0,X1] : multiply(inverse(commutator(X1,X2)),commutator(X2,commutator(X1,X0))) = multiply(inverse(commutator(X1,commutator(X2,X0))),commutator(X2,X1)),
    inference(forward_demodulation,[],[f38918,f667]) ).

fof(f39314,plain,
    ! [X2,X0,X1] : multiply(inverse(commutator(X1,X2)),commutator(X2,commutator(X1,X0))) = multiply(commutator(commutator(X2,X0),X1),commutator(X2,X1)),
    inference(forward_demodulation,[],[f39156,f1158]) ).

fof(f39426,plain,
    ! [X2,X0,X1] : multiply(inverse(commutator(X1,X2)),commutator(X2,commutator(X1,X0))) = multiply(commutator(X2,X1),commutator(commutator(X2,X0),X1)),
    inference(forward_demodulation,[],[f39314,f33072]) ).

fof(f39509,plain,
    ! [X2,X0,X1] : multiply(inverse(commutator(X1,X2)),commutator(X2,commutator(X1,X0))) = multiply(commutator(X2,X1),commutator(X2,commutator(X0,X1))),
    inference(forward_demodulation,[],[f39426,f6]) ).

fof(f39574,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,X1),commutator(X2,commutator(X1,X0))) = multiply(commutator(X2,X1),commutator(X2,commutator(X0,X1))),
    inference(forward_demodulation,[],[f39509,f1158]) ).

fof(f39701,plain,
    ! [X2,X0,X1] : multiply(commutator(multiply(X0,X0),X1),commutator(X1,identity)) = multiply(commutator(X0,X2),multiply(commutator(multiply(X0,X0),X1),inverse(commutator(X0,X2)))),
    inference(superposition,[],[f2832,f1630]) ).

fof(f39709,plain,
    ! [X2,X0,X1] : multiply(commutator(multiply(inverse(X1),X0),X2),commutator(X2,commutator(X0,X1))) = multiply(X1,multiply(commutator(multiply(inverse(X1),X0),X2),inverse(X1))),
    inference(superposition,[],[f2832,f2148]) ).

fof(f40227,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,commutator(X0,X1)),commutator(multiply(inverse(X1),X0),X2)) = multiply(X1,multiply(commutator(multiply(inverse(X1),X0),X2),inverse(X1))),
    inference(forward_demodulation,[],[f39709,f32449]) ).

fof(f40233,plain,
    ! [X2,X0,X1] : multiply(commutator(multiply(X0,X0),X1),commutator(X1,identity)) = multiply(commutator(X0,X2),multiply(commutator(multiply(X0,X0),X1),commutator(X2,X0))),
    inference(forward_demodulation,[],[f39701,f1158]) ).

fof(f40440,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,identity),commutator(multiply(X0,X0),X1)) = multiply(commutator(X0,X2),multiply(commutator(multiply(X0,X0),X1),commutator(X2,X0))),
    inference(forward_demodulation,[],[f40233,f32449]) ).

fof(f40584,plain,
    ! [X2,X0,X1] : multiply(identity,commutator(multiply(X0,X0),X1)) = multiply(commutator(X0,X2),multiply(commutator(multiply(X0,X0),X1),commutator(X2,X0))),
    inference(forward_demodulation,[],[f40440,f58]) ).

fof(f40699,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X0),X1) = multiply(commutator(X0,X2),multiply(commutator(multiply(X0,X0),X1),commutator(X2,X0))),
    inference(forward_demodulation,[],[f40584,f1]) ).

fof(f40782,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X0),multiply(X0,X2)) = commutator(multiply(X0,X0),multiply(X2,commutator(X1,X0))),
    inference(backward_demodulation,[],[f26167,f40699]) ).

fof(f41115,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(commutator(X0,multiply(X1,X2)),X1)),X1) = multiply(commutator(X0,commutator(X1,X2)),inverse(commutator(X0,multiply(X1,X2)))),
    inference(superposition,[],[f1767,f3158]) ).

fof(f41219,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,commutator(X1,X2)),commutator(multiply(X1,X2),X0)) = multiply(inverse(multiply(commutator(X0,multiply(X1,X2)),X1)),X1),
    inference(forward_demodulation,[],[f41115,f1158]) ).

fof(f41371,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,commutator(X1,X2)),commutator(multiply(X1,X2),X0)) = multiply(multiply(inverse(X1),commutator(multiply(X1,X2),X0)),X1),
    inference(forward_demodulation,[],[f41219,f1377]) ).

fof(f41500,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,commutator(X1,X2)),commutator(multiply(X1,X2),X0)) = multiply(inverse(X1),multiply(commutator(multiply(X1,X2),X0),X1)),
    inference(forward_demodulation,[],[f41371,f4]) ).

fof(f41784,plain,
    ! [X2,X0,X1] : multiply(inverse(commutator(multiply(X2,X1),X0)),X1) = multiply(X1,multiply(inverse(commutator(multiply(X2,X1),X0)),commutator(X0,commutator(X1,X2)))),
    inference(superposition,[],[f2216,f5148]) ).

fof(f41825,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(X0),X1),X2) = multiply(X1,multiply(multiply(inverse(X0),commutator(X1,X0)),X2)),
    inference(superposition,[],[f4,f2216]) ).

fof(f41954,plain,
    ! [X2,X0,X1] : multiply(multiply(inverse(X0),X1),X2) = multiply(X1,multiply(inverse(X0),multiply(commutator(X1,X0),X2))),
    inference(forward_demodulation,[],[f41825,f4]) ).

fof(f41987,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,multiply(X2,X1)),X1) = multiply(X1,multiply(commutator(X0,multiply(X2,X1)),commutator(X0,commutator(X1,X2)))),
    inference(forward_demodulation,[],[f41784,f1158]) ).

fof(f42077,plain,
    ! [X2,X0,X1] : multiply(inverse(X0),multiply(X1,X2)) = multiply(X1,multiply(inverse(X0),multiply(commutator(X1,X0),X2))),
    inference(forward_demodulation,[],[f41954,f4]) ).

fof(f42108,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,multiply(X2,X1)),X1) = multiply(X1,multiply(commutator(X0,commutator(X1,X2)),commutator(X0,multiply(X2,X1)))),
    inference(forward_demodulation,[],[f41987,f33163]) ).

fof(f47305,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,X1),multiply(X0,commutator(X0,X1))) = commutator(multiply(X2,X1),multiply(X2,multiply(X0,X1))),
    inference(superposition,[],[f1900,f126]) ).

fof(f47314,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X2),inverse(multiply(X0,X2))) = commutator(multiply(X1,X2),multiply(X1,inverse(X0))),
    inference(superposition,[],[f1900,f1070]) ).

fof(f47328,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,inverse(X1)),inverse(X0)) = commutator(multiply(X2,inverse(X1)),multiply(X2,inverse(multiply(X0,X1)))),
    inference(superposition,[],[f1900,f1041]) ).

fof(f47356,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,commutator(X1,X0)),inverse(multiply(X1,X0))) = commutator(multiply(X2,commutator(X1,X0)),multiply(X2,inverse(multiply(X0,X1)))),
    inference(superposition,[],[f1900,f2866]) ).

fof(f47358,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,commutator(X1,X0)),inverse(multiply(X0,X0))) = commutator(multiply(X2,commutator(X1,X0)),multiply(X2,multiply(inverse(multiply(X0,X0)),commutator(X1,X0)))),
    inference(superposition,[],[f1900,f5773]) ).

fof(f47598,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X0),multiply(X2,commutator(X1,X0))) = commutator(multiply(X2,commutator(X1,X0)),multiply(X2,multiply(inverse(multiply(X0,X0)),commutator(X1,X0)))),
    inference(forward_demodulation,[],[f47358,f2034]) ).

fof(f47600,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),multiply(X2,commutator(X1,X0))) = commutator(multiply(X2,commutator(X1,X0)),multiply(X2,inverse(multiply(X0,X1)))),
    inference(forward_demodulation,[],[f47356,f2034]) ).

fof(f47618,plain,
    ! [X2,X0,X1] : commutator(X0,multiply(X2,inverse(X1))) = commutator(multiply(X2,inverse(X1)),multiply(X2,inverse(multiply(X0,X1)))),
    inference(forward_demodulation,[],[f47328,f2034]) ).

fof(f47626,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X2),multiply(X1,X2)) = commutator(multiply(X1,X2),multiply(X1,inverse(X0))),
    inference(forward_demodulation,[],[f47314,f2034]) ).

fof(f47767,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X0),multiply(X0,X2)) = commutator(multiply(X2,commutator(X1,X0)),multiply(X2,multiply(inverse(multiply(X0,X0)),commutator(X1,X0)))),
    inference(forward_demodulation,[],[f47598,f40782]) ).

fof(f47768,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),X2) = commutator(multiply(X2,commutator(X1,X0)),multiply(X2,inverse(multiply(X0,X1)))),
    inference(forward_demodulation,[],[f47600,f20715]) ).

fof(f47782,plain,
    ! [X2,X0,X1] : commutator(X1,multiply(X2,inverse(X0))) = commutator(X1,multiply(X2,inverse(multiply(X1,X0)))),
    inference(backward_demodulation,[],[f15619,f47618]) ).

fof(f47872,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X1),X2) = commutator(multiply(X0,X1),multiply(X2,inverse(multiply(X1,X0)))),
    inference(backward_demodulation,[],[f15622,f47768]) ).

fof(f48051,plain,
    ! [X2,X0,X1] : commutator(X0,X2) = commutator(X0,multiply(X2,inverse(multiply(multiply(X1,X0),inverse(X1))))),
    inference(superposition,[],[f47872,f27]) ).

fof(f48463,plain,
    ! [X2,X0,X1] : commutator(X0,X2) = commutator(X0,multiply(X2,multiply(X1,inverse(multiply(X1,X0))))),
    inference(forward_demodulation,[],[f48051,f1728]) ).

fof(f49140,plain,
    ! [X2,X0,X1] : commutator(X2,inverse(multiply(X1,X0))) = commutator(X2,multiply(inverse(X0),inverse(multiply(X1,X2)))),
    inference(superposition,[],[f48463,f667]) ).

fof(f49173,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(X3,X0),commutator(X3,commutator(X0,X1))) = multiply(inverse(multiply(X1,multiply(X2,inverse(multiply(X2,X0))))),multiply(commutator(X3,X0),multiply(X1,multiply(X2,inverse(multiply(X2,X0)))))),
    inference(superposition,[],[f110,f48463]) ).

fof(f49320,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(X3,X0),commutator(X3,commutator(X0,X1))) = commutator(X3,multiply(X0,commutator(X0,multiply(X1,multiply(X2,inverse(multiply(X2,X0))))))),
    inference(forward_demodulation,[],[f49173,f32072]) ).

fof(f49349,plain,
    ! [X2,X0,X1] : commutator(X2,inverse(multiply(X1,X0))) = commutator(X2,inverse(multiply(multiply(X1,X2),X0))),
    inference(forward_demodulation,[],[f49140,f1041]) ).

fof(f49489,plain,
    ! [X3,X0,X1] : multiply(commutator(X3,X0),commutator(X3,commutator(X0,X1))) = commutator(X3,multiply(X0,commutator(X0,X1))),
    inference(forward_demodulation,[],[f49320,f48463]) ).

fof(f49508,plain,
    ! [X2,X0,X1] : commutator(X2,inverse(multiply(X1,X0))) = commutator(multiply(multiply(X1,X2),X0),X2),
    inference(forward_demodulation,[],[f49349,f2034]) ).

fof(f49611,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),X2) = multiply(X2,commutator(X0,multiply(X1,commutator(X1,X2)))),
    inference(backward_demodulation,[],[f389,f49489]) ).

fof(f49642,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X2),commutator(X2,commutator(X1,X0))) = commutator(X1,multiply(X2,commutator(X2,X0))),
    inference(backward_demodulation,[],[f32092,f49489]) ).

fof(f49647,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X1,commutator(X1,X0))) = multiply(commutator(X2,X1),commutator(X2,commutator(X0,X1))),
    inference(backward_demodulation,[],[f39574,f49489]) ).

fof(f49657,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X0),multiply(X1,multiply(commutator(X2,X3),multiply(inverse(X1),X0)))) = commutator(X2,multiply(X3,commutator(X3,multiply(inverse(X1),X0)))),
    inference(backward_demodulation,[],[f31564,f49489]) ).

fof(f49672,plain,
    ! [X2,X0,X1] : commutator(X2,inverse(multiply(X1,X0))) = commutator(multiply(X1,multiply(X2,X0)),X2),
    inference(forward_demodulation,[],[f49508,f4]) ).

fof(f49788,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X1,commutator(X1,X0))) = multiply(inverse(X1),multiply(X0,multiply(commutator(X2,X1),multiply(inverse(X0),X1)))),
    inference(backward_demodulation,[],[f37707,f49647]) ).

fof(f49894,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),X2) = commutator(multiply(X1,multiply(X2,X0)),X2),
    inference(forward_demodulation,[],[f49672,f2034]) ).

fof(f49965,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X1,commutator(X1,X0))) = commutator(X2,multiply(X1,commutator(X1,multiply(inverse(X0),X1)))),
    inference(forward_demodulation,[],[f49788,f49657]) ).

fof(f50068,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X1,commutator(X1,X0))) = commutator(X2,multiply(X1,commutator(X1,inverse(X0)))),
    inference(forward_demodulation,[],[f49965,f1864]) ).

fof(f50135,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X1,commutator(X1,X0))) = commutator(X2,multiply(X1,commutator(X0,X1))),
    inference(forward_demodulation,[],[f50068,f2034]) ).

fof(f50234,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,multiply(X1,X0)),X1) = multiply(X1,commutator(X2,multiply(multiply(X1,X0),commutator(X0,X1)))),
    inference(superposition,[],[f49611,f1933]) ).

fof(f50258,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,X1),X0) = multiply(X0,commutator(X2,multiply(inverse(X0),multiply(X1,X0)))),
    inference(superposition,[],[f49611,f46]) ).

fof(f50306,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(commutator(X0,multiply(X1,commutator(X1,X2)))),X3) = multiply(inverse(multiply(commutator(X0,X1),X2)),multiply(X2,X3)),
    inference(superposition,[],[f667,f49611]) ).

fof(f50356,plain,
    ! [X2,X0,X1] : inverse(multiply(commutator(X0,X1),inverse(X2))) = multiply(inverse(commutator(X0,multiply(X1,commutator(X1,inverse(X2))))),X2),
    inference(superposition,[],[f1032,f49611]) ).

fof(f50360,plain,
    ! [X2,X3,X0,X1] : commutator(multiply(commutator(X0,X1),inverse(X2)),X3) = commutator(X3,multiply(inverse(commutator(X0,multiply(X1,commutator(X1,inverse(X2))))),X2)),
    inference(superposition,[],[f9788,f49611]) ).

fof(f50380,plain,
    ! [X2,X3,X0,X1] : commutator(multiply(commutator(X0,X1),inverse(X2)),X3) = commutator(X3,multiply(commutator(multiply(X1,commutator(X1,inverse(X2))),X0),X2)),
    inference(forward_demodulation,[],[f50360,f1158]) ).

fof(f50384,plain,
    ! [X2,X0,X1] : inverse(multiply(commutator(X0,X1),inverse(X2))) = multiply(commutator(multiply(X1,commutator(X1,inverse(X2))),X0),X2),
    inference(forward_demodulation,[],[f50356,f1158]) ).

fof(f50423,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(commutator(X0,multiply(X1,commutator(X1,X2)))),X3) = multiply(multiply(inverse(X2),commutator(X1,X0)),multiply(X2,X3)),
    inference(forward_demodulation,[],[f50306,f1377]) ).

fof(f50485,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,multiply(X1,X0)),X1) = multiply(X1,commutator(X2,multiply(X1,multiply(X0,commutator(X0,X1))))),
    inference(forward_demodulation,[],[f50234,f4]) ).

fof(f50511,plain,
    ! [X2,X3,X0,X1] : commutator(multiply(commutator(X0,X1),inverse(X2)),X3) = commutator(X3,multiply(commutator(multiply(X1,commutator(X2,X1)),X0),X2)),
    inference(forward_demodulation,[],[f50380,f2034]) ).

fof(f50515,plain,
    ! [X2,X0,X1] : inverse(multiply(commutator(X0,X1),inverse(X2))) = multiply(commutator(multiply(X1,commutator(X2,X1)),X0),X2),
    inference(forward_demodulation,[],[f50384,f2034]) ).

fof(f50549,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(commutator(X0,multiply(X1,commutator(X1,X2)))),X3) = multiply(inverse(X2),multiply(commutator(X1,X0),multiply(X2,X3))),
    inference(forward_demodulation,[],[f50423,f4]) ).

fof(f50594,plain,
    ! [X2,X0,X1] : multiply(X1,commutator(X2,multiply(X0,X1))) = multiply(commutator(X2,multiply(X1,X0)),X1),
    inference(forward_demodulation,[],[f50485,f126]) ).

fof(f50613,plain,
    ! [X2,X0,X1] : multiply(X2,inverse(commutator(X0,X1))) = multiply(commutator(multiply(X1,commutator(X2,X1)),X0),X2),
    inference(forward_demodulation,[],[f50515,f1728]) ).

fof(f50641,plain,
    ! [X2,X3,X0,X1] : multiply(inverse(X2),multiply(commutator(X1,X0),multiply(X2,X3))) = multiply(commutator(multiply(X1,commutator(X1,X2)),X0),X3),
    inference(forward_demodulation,[],[f50549,f1158]) ).

fof(f50681,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,commutator(X1,X2)),commutator(X0,multiply(X2,X1))) = multiply(inverse(X2),multiply(X2,commutator(X0,multiply(X1,X2)))),
    inference(backward_demodulation,[],[f28695,f50594]) ).

fof(f50699,plain,
    ! [X2,X0,X1] : multiply(X2,commutator(X1,X0)) = multiply(commutator(multiply(X1,commutator(X2,X1)),X0),X2),
    inference(forward_demodulation,[],[f50613,f1158]) ).

fof(f50738,plain,
    ! [X2,X0,X1] : commutator(X0,multiply(X1,X2)) = multiply(commutator(X0,commutator(X1,X2)),commutator(X0,multiply(X2,X1))),
    inference(forward_demodulation,[],[f50681,f27]) ).

fof(f50748,plain,
    ! [X2,X3,X0,X1] : commutator(multiply(commutator(X0,X1),inverse(X2)),X3) = commutator(X3,multiply(X2,commutator(X1,X0))),
    inference(backward_demodulation,[],[f50511,f50699]) ).

fof(f50779,plain,
    ! [X2,X0,X1] : multiply(X1,commutator(X0,multiply(X1,X2))) = multiply(commutator(X0,multiply(X2,X1)),X1),
    inference(backward_demodulation,[],[f42108,f50738]) ).

fof(f50886,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(X3,multiply(X0,X1)),X2) = multiply(X2,commutator(X3,multiply(inverse(X2),multiply(X0,multiply(X1,X2))))),
    inference(superposition,[],[f50258,f4]) ).

fof(f50897,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,inverse(multiply(X2,X0))),X2) = multiply(X2,commutator(X1,multiply(inverse(X2),inverse(X0)))),
    inference(superposition,[],[f50258,f739]) ).

fof(f50898,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,inverse(multiply(X1,X0))),X0) = multiply(X0,commutator(X2,multiply(inverse(X0),multiply(commutator(X0,X1),inverse(X1))))),
    inference(superposition,[],[f50258,f1767]) ).

fof(f50984,plain,
    ! [X2,X0,X1] : multiply(inverse(X2),multiply(commutator(X0,X1),X2)) = commutator(X0,multiply(inverse(X2),multiply(X1,X2))),
    inference(superposition,[],[f27,f50258]) ).

fof(f51038,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(commutator(X0,X1),inverse(X2))) = commutator(X0,multiply(inverse(inverse(X2)),multiply(X1,inverse(X2)))),
    inference(superposition,[],[f65,f50258]) ).

fof(f51069,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(commutator(X0,X1),inverse(X2))) = commutator(multiply(X2,multiply(inverse(X1),inverse(X2))),X0),
    inference(forward_demodulation,[],[f51038,f36699]) ).

fof(f51217,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,inverse(multiply(X1,X0))),X0) = multiply(X0,commutator(multiply(X1,multiply(inverse(commutator(X0,X1)),X0)),X2)),
    inference(forward_demodulation,[],[f50898,f36699]) ).

fof(f51218,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,inverse(multiply(X2,X0))),X2) = multiply(X2,commutator(X1,inverse(multiply(X0,X2)))),
    inference(forward_demodulation,[],[f50897,f1041]) ).

fof(f51281,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(commutator(X0,X1),inverse(X2))) = commutator(multiply(X2,inverse(multiply(X2,X1))),X0),
    inference(forward_demodulation,[],[f51069,f1041]) ).

fof(f51403,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,inverse(multiply(X1,X0))),X0) = multiply(X0,commutator(multiply(X1,multiply(commutator(X1,X0),X0)),X2)),
    inference(forward_demodulation,[],[f51217,f1158]) ).

fof(f51404,plain,
    ! [X2,X0,X1] : multiply(X2,commutator(multiply(X0,X2),X1)) = multiply(commutator(X1,inverse(multiply(X2,X0))),X2),
    inference(forward_demodulation,[],[f51218,f2034]) ).

fof(f51581,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,inverse(multiply(X1,X0))),X0) = multiply(X0,commutator(multiply(X1,multiply(X0,commutator(X1,X0))),X2)),
    inference(forward_demodulation,[],[f51403,f420]) ).

fof(f51582,plain,
    ! [X2,X0,X1] : multiply(X2,commutator(multiply(X0,X2),X1)) = multiply(commutator(multiply(X2,X0),X1),X2),
    inference(forward_demodulation,[],[f51404,f2034]) ).

fof(f51755,plain,
    ! [X2,X0,X1] : multiply(commutator(multiply(X1,X0),X2),X0) = multiply(X0,commutator(multiply(X1,multiply(X0,commutator(X1,X0))),X2)),
    inference(forward_demodulation,[],[f51581,f2034]) ).

fof(f51756,plain,
    ! [X2,X0,X1] : multiply(commutator(multiply(X2,X0),X1),inverse(X0)) = multiply(inverse(multiply(X2,X0)),multiply(X2,commutator(multiply(X0,X2),X1))),
    inference(backward_demodulation,[],[f10342,f51582]) ).

fof(f51765,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,commutator(X1,X2)),commutator(multiply(X1,X2),X0)) = multiply(inverse(X1),multiply(X1,commutator(multiply(X2,X1),X0))),
    inference(backward_demodulation,[],[f41500,f51582]) ).

fof(f51769,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,commutator(X0,X1)),commutator(multiply(inverse(X1),X0),X2)) = multiply(X1,multiply(inverse(X1),commutator(multiply(X0,inverse(X1)),X2))),
    inference(backward_demodulation,[],[f40227,f51582]) ).

fof(f51908,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,inverse(X1)),X2) = multiply(commutator(X2,commutator(X0,X1)),commutator(multiply(inverse(X1),X0),X2)),
    inference(forward_demodulation,[],[f51769,f65]) ).

fof(f51909,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,X1),X0) = multiply(commutator(X0,commutator(X1,X2)),commutator(multiply(X1,X2),X0)),
    inference(forward_demodulation,[],[f51765,f27]) ).

fof(f51911,plain,
    ! [X2,X0,X1] : multiply(commutator(multiply(X2,X0),X1),inverse(X0)) = multiply(inverse(X0),commutator(multiply(X0,X2),X1)),
    inference(forward_demodulation,[],[f51756,f667]) ).

fof(f52025,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,commutator(X1,X2)),commutator(multiply(X2,X1),X0)) = multiply(X1,multiply(inverse(X1),commutator(multiply(X1,X2),X0))),
    inference(backward_demodulation,[],[f35547,f51911]) ).

fof(f52120,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X2),X0) = multiply(commutator(X0,commutator(X1,X2)),commutator(multiply(X2,X1),X0)),
    inference(forward_demodulation,[],[f52025,f65]) ).

fof(f52405,plain,
    ! [X2,X0,X1] : inverse(commutator(multiply(X0,X1),X2)) = commutator(X2,multiply(X0,multiply(X2,X1))),
    inference(superposition,[],[f1158,f49894]) ).

fof(f52538,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,X1)) = commutator(X2,multiply(X0,multiply(X2,X1))),
    inference(forward_demodulation,[],[f52405,f1158]) ).

fof(f52714,plain,
    ! [X2,X0,X1] : commutator(X1,multiply(X0,inverse(X2))) = multiply(X0,multiply(commutator(X2,X1),multiply(inverse(X0),commutator(X1,X0)))),
    inference(backward_demodulation,[],[f26132,f52538]) ).

fof(f53144,plain,
    ! [X2,X0,X1] : multiply(commutator(multiply(X1,X0),X2),commutator(X2,commutator(X0,X1))) = commutator(multiply(X1,X0),multiply(X2,commutator(X2,X1))),
    inference(superposition,[],[f49642,f1933]) ).

fof(f53145,plain,
    ! [X2,X0,X1] : multiply(commutator(multiply(X0,X1),X2),commutator(X2,commutator(X0,X1))) = commutator(multiply(X0,X1),multiply(X2,commutator(X2,X1))),
    inference(superposition,[],[f49642,f2008]) ).

fof(f53153,plain,
    ! [X2,X0,X1] : multiply(commutator(multiply(inverse(X1),X0),X2),commutator(X2,commutator(X0,X1))) = commutator(multiply(inverse(X1),X0),multiply(X2,commutator(X2,X1))),
    inference(superposition,[],[f49642,f2148]) ).

fof(f53162,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(multiply(X0,commutator(X2,X1)),X3),commutator(X3,commutator(X0,X1))) = commutator(multiply(X0,commutator(X2,X1)),multiply(X3,commutator(X3,X1))),
    inference(superposition,[],[f49642,f20305]) ).

fof(f53391,plain,
    ! [X2,X3,X0,X1] : multiply(commutator(X3,commutator(X0,X1)),commutator(multiply(X0,commutator(X2,X1)),X3)) = commutator(multiply(X0,commutator(X2,X1)),multiply(X3,commutator(X3,X1))),
    inference(forward_demodulation,[],[f53162,f32449]) ).

fof(f53399,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,commutator(X0,X1)),commutator(multiply(inverse(X1),X0),X2)) = commutator(multiply(inverse(X1),X0),multiply(X2,commutator(X2,X1))),
    inference(forward_demodulation,[],[f53153,f32449]) ).

fof(f53407,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,commutator(X0,X1)),commutator(multiply(X0,X1),X2)) = commutator(multiply(X0,X1),multiply(X2,commutator(X2,X1))),
    inference(forward_demodulation,[],[f53145,f32449]) ).

fof(f53408,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,commutator(X0,X1)),commutator(multiply(X1,X0),X2)) = commutator(multiply(X1,X0),multiply(X2,commutator(X2,X1))),
    inference(forward_demodulation,[],[f53144,f32449]) ).

fof(f53599,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,inverse(X1)),X2) = commutator(multiply(inverse(X1),X0),multiply(X2,commutator(X2,X1))),
    inference(forward_demodulation,[],[f53399,f51908]) ).

fof(f53603,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),X2) = commutator(multiply(X0,X1),multiply(X2,commutator(X2,X1))),
    inference(forward_demodulation,[],[f53407,f51909]) ).

fof(f53604,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X1),X2) = commutator(multiply(X1,X0),multiply(X2,commutator(X2,X1))),
    inference(forward_demodulation,[],[f53408,f52120]) ).

fof(f53750,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,commutator(X0,X1))) = commutator(multiply(multiply(X0,multiply(X1,X2)),inverse(X1)),X0),
    inference(backward_demodulation,[],[f15806,f53599]) ).

fof(f53755,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X2),X0) = commutator(multiply(X2,X1),multiply(X2,multiply(X0,X1))),
    inference(backward_demodulation,[],[f47305,f53603]) ).

fof(f53760,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,X1),X0) = commutator(multiply(X1,X2),multiply(X2,multiply(X0,X1))),
    inference(backward_demodulation,[],[f19097,f53604]) ).

fof(f53871,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,commutator(X0,X1))) = commutator(X0,multiply(X1,inverse(multiply(X0,multiply(X1,X2))))),
    inference(forward_demodulation,[],[f53750,f8103]) ).

fof(f53888,plain,
    ! [X2,X0,X1] : commutator(multiply(commutator(X1,X0),X2),inverse(multiply(X0,X0))) = commutator(multiply(X0,X0),multiply(X0,X2)),
    inference(backward_demodulation,[],[f47767,f53755]) ).

fof(f53901,plain,
    ! [X2,X0,X1] : commutator(multiply(X2,inverse(X1)),X0) = commutator(multiply(inverse(X1),X2),multiply(X0,commutator(X1,X0))),
    inference(backward_demodulation,[],[f24910,f53760]) ).

fof(f53993,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,commutator(X0,X1))) = commutator(X0,multiply(X1,inverse(multiply(X1,X2)))),
    inference(forward_demodulation,[],[f53871,f47782]) ).

fof(f54002,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,X0),multiply(commutator(X1,X0),X2)) = commutator(multiply(X0,X0),multiply(X0,X2)),
    inference(forward_demodulation,[],[f53888,f2034]) ).

fof(f54397,plain,
    ! [X2,X0,X1] : inverse(commutator(X0,X1)) = multiply(commutator(X0,commutator(X1,X2)),inverse(commutator(X0,multiply(X1,commutator(X1,X2))))),
    inference(superposition,[],[f1070,f49489]) ).

fof(f54476,plain,
    ! [X2,X0,X1] : inverse(commutator(X0,X1)) = multiply(commutator(X0,commutator(X1,X2)),commutator(multiply(X1,commutator(X1,X2)),X0)),
    inference(forward_demodulation,[],[f54397,f1158]) ).

fof(f54673,plain,
    ! [X2,X0,X1] : inverse(commutator(X0,X1)) = commutator(multiply(X1,commutator(X1,X2)),multiply(X0,commutator(X0,X2))),
    inference(forward_demodulation,[],[f54476,f53391]) ).

fof(f54825,plain,
    ! [X2,X0,X1] : commutator(X1,X0) = commutator(multiply(X1,commutator(X1,X2)),multiply(X0,commutator(X0,X2))),
    inference(forward_demodulation,[],[f54673,f1158]) ).

fof(f56856,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),X2) = commutator(multiply(multiply(X1,X0),commutator(X0,X1)),multiply(X2,commutator(X2,X1))),
    inference(superposition,[],[f54825,f1933]) ).

fof(f57245,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),X2) = commutator(multiply(X1,multiply(X0,commutator(X0,X1))),multiply(X2,commutator(X2,X1))),
    inference(forward_demodulation,[],[f56856,f4]) ).

fof(f57363,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),X2) = commutator(multiply(multiply(X0,commutator(X0,X1)),X1),X2),
    inference(forward_demodulation,[],[f57245,f53604]) ).

fof(f57449,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),X2) = commutator(multiply(X0,multiply(commutator(X0,X1),X1)),X2),
    inference(forward_demodulation,[],[f57363,f4]) ).

fof(f57507,plain,
    ! [X2,X0,X1] : commutator(multiply(X1,X0),X2) = commutator(multiply(X0,multiply(X1,commutator(X0,X1))),X2),
    inference(forward_demodulation,[],[f57449,f420]) ).

fof(f57545,plain,
    ! [X2,X0,X1] : multiply(X0,commutator(multiply(X0,X1),X2)) = multiply(commutator(multiply(X1,X0),X2),X0),
    inference(backward_demodulation,[],[f51755,f57507]) ).

fof(f60372,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),X2) = multiply(X2,commutator(X0,multiply(X1,commutator(X2,X1)))),
    inference(superposition,[],[f49611,f50135]) ).

fof(f60404,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(multiply(X1,commutator(X1,X2)),inverse(X0))) = multiply(multiply(X1,commutator(X1,X2)),commutator(X0,multiply(X1,commutator(X2,X1)))),
    inference(superposition,[],[f2047,f50135]) ).

fof(f60742,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(multiply(X1,commutator(X1,X2)),inverse(X0))) = multiply(X1,multiply(commutator(X1,X2),commutator(X0,multiply(X1,commutator(X2,X1))))),
    inference(forward_demodulation,[],[f60404,f4]) ).

fof(f60923,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(commutator(X1,X2),inverse(X0)))) = multiply(X1,multiply(commutator(X1,X2),commutator(X0,multiply(X1,commutator(X2,X1))))),
    inference(forward_demodulation,[],[f60742,f4]) ).

fof(f61269,plain,
    ! [X0,X1] : commutator(multiply(X0,X0),multiply(X0,inverse(multiply(X1,X0)))) = commutator(multiply(X0,X0),inverse(multiply(X0,X1))),
    inference(superposition,[],[f54002,f2866]) ).

fof(f61331,plain,
    ! [X0,X1] : commutator(multiply(X0,X0),X1) = commutator(multiply(X0,X0),multiply(X0,X1)),
    inference(superposition,[],[f19762,f54002]) ).

fof(f61580,plain,
    ! [X0,X1] : commutator(multiply(X0,X0),multiply(X0,inverse(multiply(X1,X0)))) = commutator(multiply(X0,X1),multiply(X0,X0)),
    inference(forward_demodulation,[],[f61269,f2034]) ).

fof(f61787,plain,
    ! [X0,X1] : commutator(multiply(X0,X1),multiply(X0,X0)) = commutator(multiply(multiply(X1,X0),X0),multiply(X0,X0)),
    inference(forward_demodulation,[],[f61580,f47626]) ).

fof(f61918,plain,
    ! [X0,X1] : commutator(multiply(X0,X1),multiply(X0,X0)) = commutator(multiply(X1,multiply(X0,X0)),multiply(X0,X0)),
    inference(forward_demodulation,[],[f61787,f4]) ).

fof(f62021,plain,
    ! [X0,X1] : commutator(X1,multiply(X0,X0)) = commutator(multiply(X0,X1),multiply(X0,X0)),
    inference(forward_demodulation,[],[f61918,f2008]) ).

fof(f69777,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(multiply(X0,X1),commutator(multiply(X0,X0),X1))) = commutator(X2,multiply(multiply(X0,X1),commutator(multiply(X0,X1),multiply(X0,X0)))),
    inference(superposition,[],[f50135,f61331]) ).

fof(f69789,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(multiply(X0,X1),commutator(multiply(X0,X0),X1))) = commutator(X2,multiply(X0,multiply(X1,commutator(multiply(X0,X1),multiply(X0,X0))))),
    inference(forward_demodulation,[],[f69777,f4]) ).

fof(f69956,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(multiply(X0,X1),commutator(multiply(X0,X0),X1))) = commutator(X2,multiply(inverse(X0),multiply(X1,multiply(X0,X0)))),
    inference(forward_demodulation,[],[f69789,f15540]) ).

fof(f70079,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,multiply(X1,commutator(multiply(X0,X0),X1)))) = commutator(X2,multiply(inverse(X0),multiply(X1,multiply(X0,X0)))),
    inference(forward_demodulation,[],[f69956,f4]) ).

fof(f73019,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X1,X1)),multiply(commutator(X2,multiply(X1,X0)),multiply(X1,X1))) = multiply(commutator(X2,multiply(X1,X0)),commutator(X2,commutator(X0,multiply(X1,X1)))),
    inference(superposition,[],[f110,f62021]) ).

fof(f73097,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,multiply(X1,X0)),commutator(X2,commutator(X0,multiply(X1,X1)))) = commutator(X2,multiply(multiply(X1,X0),commutator(X0,multiply(X1,X1)))),
    inference(superposition,[],[f49489,f62021]) ).

fof(f73099,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,multiply(X1,X0)),multiply(X1,X1)) = multiply(multiply(X1,X1),commutator(X2,multiply(multiply(X1,X0),commutator(X0,multiply(X1,X1))))),
    inference(superposition,[],[f49611,f62021]) ).

fof(f73106,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(multiply(X1,X0),commutator(multiply(X1,X1),multiply(X1,X0)))) = commutator(X2,multiply(multiply(X1,X0),commutator(X0,multiply(X1,X1)))),
    inference(superposition,[],[f50135,f62021]) ).

fof(f73118,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(multiply(X1,X0),commutator(multiply(X1,X1),multiply(X1,X0)))) = commutator(X2,multiply(X1,multiply(X0,commutator(X0,multiply(X1,X1))))),
    inference(forward_demodulation,[],[f73106,f4]) ).

fof(f73124,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,multiply(X1,X0)),multiply(X1,X1)) = multiply(X1,multiply(X1,commutator(X2,multiply(multiply(X1,X0),commutator(X0,multiply(X1,X1)))))),
    inference(forward_demodulation,[],[f73099,f4]) ).

fof(f73126,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,multiply(X1,X0)),commutator(X2,commutator(X0,multiply(X1,X1)))) = commutator(X2,multiply(X1,multiply(X0,commutator(X0,multiply(X1,X1))))),
    inference(forward_demodulation,[],[f73097,f4]) ).

fof(f73268,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X1,multiply(X0,commutator(multiply(X1,X1),multiply(X1,X0))))) = commutator(X2,multiply(X1,multiply(X0,commutator(X0,multiply(X1,X1))))),
    inference(forward_demodulation,[],[f73118,f4]) ).

fof(f73274,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,multiply(X1,X0)),multiply(X1,X1)) = multiply(X1,multiply(X1,commutator(X2,multiply(X1,multiply(X0,commutator(X0,multiply(X1,X1))))))),
    inference(forward_demodulation,[],[f73124,f4]) ).

fof(f73380,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X1,multiply(X0,commutator(multiply(X1,X1),X0)))) = commutator(X2,multiply(X1,multiply(X0,commutator(X0,multiply(X1,X1))))),
    inference(forward_demodulation,[],[f73268,f61331]) ).

fof(f73471,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(inverse(X1),multiply(X0,multiply(X1,X1)))) = commutator(X2,multiply(X1,multiply(X0,commutator(X0,multiply(X1,X1))))),
    inference(forward_demodulation,[],[f73380,f70079]) ).

fof(f73537,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,multiply(X1,X0)),multiply(X1,X1)) = multiply(X1,multiply(X1,commutator(X2,multiply(inverse(X1),multiply(X0,multiply(X1,X1)))))),
    inference(backward_demodulation,[],[f73274,f73471]) ).

fof(f73538,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(inverse(X1),multiply(X0,multiply(X1,X1)))) = multiply(commutator(X2,multiply(X1,X0)),commutator(X2,commutator(X0,multiply(X1,X1)))),
    inference(backward_demodulation,[],[f73126,f73471]) ).

fof(f73584,plain,
    ! [X2,X0,X1] : multiply(inverse(multiply(X1,X1)),multiply(commutator(X2,multiply(X1,X0)),multiply(X1,X1))) = commutator(X2,multiply(inverse(X1),multiply(X0,multiply(X1,X1)))),
    inference(backward_demodulation,[],[f73019,f73538]) ).

fof(f73585,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,multiply(X1,X0)),multiply(X1,X1)) = multiply(X1,multiply(commutator(X2,multiply(X0,X1)),X1)),
    inference(forward_demodulation,[],[f73537,f50886]) ).

fof(f73621,plain,
    ! [X2,X0,X1] : multiply(commutator(X2,multiply(X1,X0)),multiply(X1,X1)) = multiply(X1,multiply(X1,commutator(X2,multiply(X1,X0)))),
    inference(forward_demodulation,[],[f73585,f50779]) ).

fof(f73650,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(inverse(X1),multiply(X0,multiply(X1,X1)))) = multiply(inverse(multiply(X1,X1)),multiply(X1,multiply(X1,commutator(X2,multiply(X1,X0))))),
    inference(backward_demodulation,[],[f73584,f73621]) ).

fof(f73678,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(inverse(X1),multiply(X0,multiply(X1,X1)))) = multiply(commutator(X1,X1),commutator(X2,multiply(X1,X0))),
    inference(forward_demodulation,[],[f73650,f1757]) ).

fof(f73699,plain,
    ! [X2,X0,X1] : multiply(identity,commutator(X2,multiply(X1,X0))) = commutator(X2,multiply(inverse(X1),multiply(X0,multiply(X1,X1)))),
    inference(forward_demodulation,[],[f73678,f41]) ).

fof(f73714,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X1,X0)) = commutator(X2,multiply(inverse(X1),multiply(X0,multiply(X1,X1)))),
    inference(forward_demodulation,[],[f73699,f1]) ).

fof(f73783,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X1,inverse(multiply(X1,X0)))) = commutator(X2,multiply(inverse(X1),multiply(inverse(X0),X1))),
    inference(superposition,[],[f73714,f667]) ).

fof(f74127,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X1,inverse(multiply(X1,X0)))) = multiply(inverse(X1),multiply(commutator(X2,inverse(X0)),X1)),
    inference(forward_demodulation,[],[f73783,f50984]) ).

fof(f74280,plain,
    ! [X2,X0,X1] : multiply(inverse(X1),multiply(commutator(X0,X2),X1)) = commutator(X2,multiply(X1,inverse(multiply(X1,X0)))),
    inference(forward_demodulation,[],[f74127,f2034]) ).

fof(f124713,plain,
    ! [X2,X0,X1] : multiply(multiply(X0,commutator(X0,X1)),commutator(X0,multiply(X1,inverse(multiply(X1,X2))))) = multiply(X2,multiply(multiply(X0,commutator(X0,X1)),inverse(X2))),
    inference(superposition,[],[f2047,f53993]) ).

fof(f125228,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(X0,multiply(commutator(X0,X1),inverse(X2)))) = multiply(multiply(X0,commutator(X0,X1)),commutator(X0,multiply(X1,inverse(multiply(X1,X2))))),
    inference(forward_demodulation,[],[f124713,f4]) ).

fof(f125700,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(X0,multiply(commutator(X0,X1),inverse(X2)))) = multiply(X0,multiply(commutator(X0,X1),commutator(X0,multiply(X1,inverse(multiply(X1,X2)))))),
    inference(forward_demodulation,[],[f125228,f4]) ).

fof(f126105,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(X0,multiply(commutator(X0,X1),inverse(X2)))) = multiply(X0,multiply(commutator(X0,X1),multiply(inverse(X1),multiply(commutator(X2,X0),X1)))),
    inference(forward_demodulation,[],[f125700,f74280]) ).

fof(f126402,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(X0,multiply(commutator(X0,X1),inverse(X2)))) = multiply(X0,multiply(inverse(X1),multiply(commutator(X0,X1),multiply(commutator(X2,X0),X1)))),
    inference(forward_demodulation,[],[f126105,f5899]) ).

fof(f126614,plain,
    ! [X2,X0,X1] : multiply(X2,multiply(X0,multiply(commutator(X0,X1),inverse(X2)))) = multiply(inverse(X1),multiply(X0,multiply(commutator(X2,X0),X1))),
    inference(forward_demodulation,[],[f126402,f42077]) ).

fof(f129817,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X0),commutator(multiply(commutator(X1,X0),inverse(X1)),X2)) = multiply(commutator(multiply(X0,inverse(multiply(X0,X1))),X2),commutator(X1,X0)),
    inference(superposition,[],[f57545,f2083]) ).

fof(f130364,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X0),commutator(multiply(commutator(X1,X0),inverse(X1)),X2)) = multiply(multiply(X0,multiply(commutator(X2,X1),inverse(X0))),commutator(X1,X0)),
    inference(forward_demodulation,[],[f129817,f51281]) ).

fof(f130581,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X0),commutator(multiply(commutator(X1,X0),inverse(X1)),X2)) = multiply(X0,multiply(multiply(commutator(X2,X1),inverse(X0)),commutator(X1,X0))),
    inference(forward_demodulation,[],[f130364,f4]) ).

fof(f130728,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(commutator(X2,X1),multiply(inverse(X0),commutator(X1,X0)))) = multiply(commutator(X1,X0),commutator(multiply(commutator(X1,X0),inverse(X1)),X2)),
    inference(forward_demodulation,[],[f130581,f4]) ).

fof(f130828,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(commutator(X2,X1),multiply(inverse(X0),commutator(X1,X0)))) = multiply(commutator(X1,X0),commutator(X2,multiply(X1,commutator(X0,X1)))),
    inference(forward_demodulation,[],[f130728,f50748]) ).

fof(f130884,plain,
    ! [X2,X0,X1] : commutator(X1,multiply(X0,inverse(X2))) = multiply(commutator(X1,X0),commutator(X2,multiply(X1,commutator(X0,X1)))),
    inference(forward_demodulation,[],[f130828,f52714]) ).

fof(f130925,plain,
    ! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(commutator(X1,X2),inverse(X0)))) = multiply(X1,commutator(X1,multiply(X2,inverse(X0)))),
    inference(backward_demodulation,[],[f60923,f130884]) ).

fof(f130974,plain,
    ! [X2,X0,X1] : multiply(X0,commutator(X0,multiply(X1,inverse(X2)))) = multiply(inverse(X1),multiply(X0,multiply(commutator(X2,X0),X1))),
    inference(backward_demodulation,[],[f126614,f130925]) ).

fof(f131010,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,commutator(X1,X0)),X2) = multiply(inverse(X0),multiply(commutator(X0,X1),multiply(X0,commutator(X0,multiply(X2,inverse(X1)))))),
    inference(backward_demodulation,[],[f1186,f130974]) ).

fof(f131029,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,commutator(X1,X0)),X2) = multiply(commutator(multiply(X0,commutator(X0,X0)),X1),commutator(X0,multiply(X2,inverse(X1)))),
    inference(forward_demodulation,[],[f131010,f50641]) ).

fof(f131039,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,commutator(X1,X0)),X2) = multiply(commutator(multiply(X0,identity),X1),commutator(X0,multiply(X2,inverse(X1)))),
    inference(forward_demodulation,[],[f131029,f41]) ).

fof(f131047,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,commutator(X1,X0)),X2) = multiply(commutator(X0,X1),commutator(X0,multiply(X2,inverse(X1)))),
    inference(forward_demodulation,[],[f131039,f45]) ).

fof(f131197,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X2),commutator(X1,inverse(X0))) = commutator(multiply(X1,commutator(X2,X1)),inverse(multiply(inverse(X2),X0))),
    inference(superposition,[],[f131047,f739]) ).

fof(f131282,plain,
    ! [X2,X0,X1] : multiply(inverse(commutator(X0,multiply(X2,inverse(X1)))),commutator(X1,X0)) = inverse(commutator(multiply(X0,commutator(X1,X0)),X2)),
    inference(superposition,[],[f1377,f131047]) ).

fof(f131480,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,commutator(X1,X0))) = multiply(inverse(commutator(X0,multiply(X2,inverse(X1)))),commutator(X1,X0)),
    inference(forward_demodulation,[],[f131282,f1158]) ).

fof(f131565,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X2),commutator(X1,inverse(X0))) = commutator(multiply(inverse(X2),X0),multiply(X1,commutator(X2,X1))),
    inference(forward_demodulation,[],[f131197,f2034]) ).

fof(f131777,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,commutator(X1,X0))) = multiply(commutator(multiply(X2,inverse(X1)),X0),commutator(X1,X0)),
    inference(forward_demodulation,[],[f131480,f1158]) ).

fof(f131859,plain,
    ! [X2,X0,X1] : commutator(multiply(X0,inverse(X2)),X1) = multiply(commutator(X1,X2),commutator(X1,inverse(X0))),
    inference(forward_demodulation,[],[f131565,f53901]) ).

fof(f132043,plain,
    ! [X2,X0,X1] : commutator(X2,multiply(X0,commutator(X1,X0))) = multiply(commutator(X1,X0),commutator(multiply(X2,inverse(X1)),X0)),
    inference(forward_demodulation,[],[f131777,f33072]) ).

fof(f132127,plain,
    ! [X2,X0,X1] : multiply(commutator(X1,X2),commutator(X0,X1)) = commutator(multiply(X0,inverse(X2)),X1),
    inference(forward_demodulation,[],[f131859,f2034]) ).

fof(f132352,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),commutator(X1,X2)) = commutator(multiply(X0,inverse(X2)),X1),
    inference(backward_demodulation,[],[f32449,f132127]) ).

fof(f132677,plain,
    ! [X2,X0,X1] : commutator(X2,X0) = multiply(commutator(X1,X0),commutator(multiply(X2,inverse(X1)),X0)),
    inference(backward_demodulation,[],[f31858,f132352]) ).

fof(f133008,plain,
    ! [X2,X0,X1] : commutator(X2,X0) = commutator(X2,multiply(X0,commutator(X1,X0))),
    inference(backward_demodulation,[],[f132043,f132677]) ).

fof(f133382,plain,
    ! [X2,X0,X1] : multiply(commutator(X0,X1),X2) = multiply(X2,commutator(X0,X1)),
    inference(backward_demodulation,[],[f60372,f133008]) ).

fof(f140322,plain,
    sP0(multiply(a,commutator(b,c))),
    inference(superposition,[],[f9,f133382]) ).

fof(f140572,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f140322,f8]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP024-5 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.35  % Computer : n010.cluster.edu
% 0.10/0.35  % Model    : x86_64 x86_64
% 0.10/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35  % Memory   : 8046.5625MB
% 0.10/0.35  % OS       : Linux 6.8.0-71-generic
% 0.10/0.35  % CPULimit : 300
% 0.10/0.35  % WCLimit  : 300
% 0.10/0.35  % DateTime : Sun Sep 27 09:14:31 UTC 2026
% 0.10/0.35  % CPUTime  : 
% 0.10/0.35  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39  Running first-order theorem proving
% 0.13/0.39  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 83.73/12.61  % (677426)Detected a unit-equality problem, will run specialized UEQ schedule.
% 83.73/12.61  % (677435)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1436749693:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 83.73/12.61  % (677432)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=3968942281:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 83.73/12.61  % (677434)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1404510287:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 83.73/12.61  % (677437)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=4038013250:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 83.73/12.61  % (677431)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=1400988073:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 83.73/12.61  % (677433)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=40908530:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 83.73/12.61  % (677436)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1843501655:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 83.73/12.61  % (677435)Instruction limit reached! 
% 83.73/12.61  % (677435)------------------------------
% 83.73/12.61  % (677435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.73/12.61  % (677435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.73/12.61  % (677435)CaDiCaL version: 2.1.3
% 83.73/12.61  % (677435)Termination reason: Instruction limit
% 83.73/12.61  % (677435)Termination phase: Saturation
% 83.73/12.61  % (677435)Time elapsed: 0.054 s
% 83.73/12.61  % (677435)Peak memory usage: 90 MB
% 83.73/12.61  % (677435)Instructions burned: 182 (million)
% 83.73/12.61  % (677434)Instruction limit reached! 
% 83.73/12.61  % (677434)------------------------------
% 83.73/12.61  % (677434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.73/12.61  % (677434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.73/12.61  % (677434)CaDiCaL version: 2.1.3
% 83.73/12.61  % (677434)Termination reason: Instruction limit
% 83.73/12.61  % (677434)Termination phase: Saturation
% 83.73/12.61  % (677434)Time elapsed: 0.075 s
% 83.73/12.61  % (677434)Peak memory usage: 88 MB
% 83.73/12.61  % (677434)Instructions burned: 137 (million)
% 83.73/12.61  % (677445)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3519583348:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 83.73/12.61  % (677436)Instruction limit reached! 
% 83.73/12.61  % (677436)------------------------------
% 83.73/12.61  % (677436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.73/12.61  % (677436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.73/12.61  % (677436)CaDiCaL version: 2.1.3
% 83.73/12.61  % (677436)Termination reason: Instruction limit
% 83.73/12.61  % (677436)Termination phase: Saturation
% 83.73/12.61  % (677436)Time elapsed: 0.169 s
% 83.73/12.61  % (677436)Peak memory usage: 90 MB
% 83.73/12.61  % (677436)Instructions burned: 257 (million)
% 83.73/12.61  % (677446)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4179668914:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 83.73/12.61  % (677448)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1364916191:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 83.73/12.61  % (677448)Instruction limit reached! 
% 83.73/12.61  % (677448)------------------------------
% 83.73/12.61  % (677448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.73/12.61  % (677448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.73/12.61  % (677448)CaDiCaL version: 2.1.3
% 83.73/12.61  % (677448)Termination reason: Instruction limit
% 83.73/12.61  % (677448)Termination phase: Saturation
% 83.73/12.61  % (677448)Time elapsed: 0.113 s
% 83.73/12.61  % (677448)Peak memory usage: 90 MB
% 83.73/12.61  % (677448)Instructions burned: 216 (million)
% 127.18/18.79  % (677451)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=1024885743:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 127.18/18.79  % (677437)Instruction limit reached! 
% 127.18/18.79  % (677437)------------------------------
% 127.18/18.79  % (677437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.18/18.79  % (677437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.18/18.79  % (677437)CaDiCaL version: 2.1.3
% 127.18/18.79  % (677437)Termination reason: Instruction limit
% 127.18/18.79  % (677437)Termination phase: Saturation
% 127.18/18.79  % (677437)Time elapsed: 0.653 s
% 127.18/18.79  % (677437)Peak memory usage: 101 MB
% 127.18/18.79  % (677437)Instructions burned: 1187 (million)
% 127.18/18.79  % (677451)Instruction limit reached! 
% 127.18/18.79  % (677451)------------------------------
% 127.18/18.79  % (677451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.18/18.79  % (677451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.18/18.79  % (677451)CaDiCaL version: 2.1.3
% 127.18/18.79  % (677451)Termination reason: Instruction limit
% 127.18/18.79  % (677451)Termination phase: Saturation
% 127.18/18.79  % (677451)Time elapsed: 0.209 s
% 127.18/18.79  % (677451)Peak memory usage: 94 MB
% 127.18/18.79  % (677451)Instructions burned: 317 (million)
% 127.18/18.79  % (677453)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=1543652374:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 127.18/18.79  % (677445)Instruction limit reached! 
% 127.18/18.79  % (677445)------------------------------
% 127.18/18.79  % (677445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.18/18.79  % (677445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.18/18.79  % (677445)CaDiCaL version: 2.1.3
% 127.18/18.79  % (677445)Termination reason: Instruction limit
% 127.18/18.79  % (677445)Termination phase: Saturation
% 127.18/18.79  % (677445)Time elapsed: 0.765 s
% 127.18/18.79  % (677445)Peak memory usage: 140 MB
% 127.18/18.79  % (677445)Instructions burned: 2052 (million)
% 127.18/18.79  % (677454)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1640581954:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 127.18/18.79  % (677456)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1364557673:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 127.18/18.79  % (677454)Instruction limit reached! 
% 127.18/18.79  % (677454)------------------------------
% 127.18/18.79  % (677454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.18/18.79  % (677454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.18/18.79  % (677454)CaDiCaL version: 2.1.3
% 127.18/18.79  % (677454)Termination reason: Instruction limit
% 127.18/18.79  % (677454)Termination phase: Saturation
% 127.18/18.79  % (677454)Time elapsed: 1.729 s
% 127.18/18.79  % (677454)Peak memory usage: 127 MB
% 127.18/18.79  % (677454)Instructions burned: 2837 (million)
% 127.18/18.79  % (677459)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=371812807:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/11832Mi)
% 127.18/18.79  % (677446)Instruction limit reached! 
% 127.18/18.79  % (677446)------------------------------
% 127.18/18.79  % (677446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.18/18.79  % (677446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.18/18.79  % (677446)CaDiCaL version: 2.1.3
% 127.18/18.79  % (677446)Termination reason: Instruction limit
% 127.18/18.79  % (677446)Termination phase: Saturation
% 127.18/18.79  % (677446)Time elapsed: 2.944 s
% 127.18/18.79  % (677446)Peak memory usage: 167 MB
% 127.18/18.79  % (677446)Instructions burned: 4949 (million)
% 127.18/18.79  % (677461)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=3968183261:i=2279:fgj=on:bd=all_2966 on theBenchmark for (2966ds/2279Mi)
% 127.18/18.79  % (677461)Instruction limit reached! 
% 127.18/18.79  % (677461)------------------------------
% 127.18/18.79  % (677461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677461)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677461)Termination reason: Instruction limit
% 128.70/27.04  % (677461)Termination phase: Saturation
% 128.70/27.04  % (677461)Time elapsed: 1.252 s
% 128.70/27.04  % (677461)Peak memory usage: 133 MB
% 128.70/27.04  % (677461)Instructions burned: 2279 (million)
% 128.70/27.04  % (677463)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=3226974437:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2951 on theBenchmark for (2951ds/6225Mi)
% 128.70/27.04  % (677453)Instruction limit reached! 
% 128.70/27.04  % (677453)------------------------------
% 128.70/27.04  % (677453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677453)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677453)Termination reason: Instruction limit
% 128.70/27.04  % (677453)Termination phase: Saturation
% 128.70/27.04  % (677453)Time elapsed: 4.317 s
% 128.70/27.04  % (677453)Peak memory usage: 233 MB
% 128.70/27.04  % (677453)Instructions burned: 12126 (million)
% 128.70/27.04  % (677465)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=2003624596:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2946 on theBenchmark for (2946ds/21755Mi)
% 128.70/27.04  % (677463)Instruction limit reached! 
% 128.70/27.04  % (677463)------------------------------
% 128.70/27.04  % (677463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677463)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677463)Termination reason: Instruction limit
% 128.70/27.04  % (677463)Termination phase: Saturation
% 128.70/27.04  % (677463)Time elapsed: 3.784 s
% 128.70/27.04  % (677463)Peak memory usage: 159 MB
% 128.70/27.04  % (677463)Instructions burned: 6225 (million)
% 128.70/27.04  % (677467)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=567672625:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2912 on theBenchmark for (2912ds/16427Mi)
% 128.70/27.04  % (677456)Instruction limit reached! 
% 128.70/27.04  % (677456)------------------------------
% 128.70/27.04  % (677456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677456)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677456)Termination reason: Instruction limit
% 128.70/27.04  % (677456)Termination phase: Saturation
% 128.70/27.04  % (677456)Time elapsed: 8.696 s
% 128.70/27.04  % (677456)Peak memory usage: 256 MB
% 128.70/27.04  % (677456)Instructions burned: 14534 (million)
% 128.70/27.04  % (677469)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=3794758229:i=9356:fgj=on:bd=preordered:av=off_2900 on theBenchmark for (2900ds/9356Mi)
% 128.70/27.04  % (677459)Instruction limit reached! 
% 128.70/27.04  % (677459)------------------------------
% 128.70/27.04  % (677459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677459)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677459)Termination reason: Instruction limit
% 128.70/27.04  % (677459)Termination phase: Saturation
% 128.70/27.04  % (677459)Time elapsed: 7.394 s
% 128.70/27.04  % (677459)Peak memory usage: 234 MB
% 128.70/27.04  % (677459)Instructions burned: 11832 (million)
% 128.70/27.04  % (677471)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=1459479579:i=2070:kws=inv_precedence:slsql=off:bd=all_2895 on theBenchmark for (2895ds/2070Mi)
% 128.70/27.04  % (677471)Instruction limit reached! 
% 128.70/27.04  % (677471)------------------------------
% 128.70/27.04  % (677471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677471)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677471)Termination reason: Instruction limit
% 128.70/27.04  % (677471)Termination phase: Saturation
% 128.70/27.04  % (677471)Time elapsed: 0.994 s
% 128.70/27.04  % (677471)Peak memory usage: 111 MB
% 128.70/27.04  % (677471)Instructions burned: 2070 (million)
% 128.70/27.04  % (677473)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=265841739:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2883 on theBenchmark for (2883ds/6461Mi)
% 128.70/27.04  % (677465)Instruction limit reached! 
% 128.70/27.04  % (677465)------------------------------
% 128.70/27.04  % (677465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677465)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677465)Termination reason: Instruction limit
% 128.70/27.04  % (677465)Termination phase: Saturation
% 128.70/27.04  % (677465)Time elapsed: 6.752 s
% 128.70/27.04  % (677465)Peak memory usage: 260 MB
% 128.70/27.04  % (677465)Instructions burned: 21908 (million)
% 128.70/27.04  % (677475)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=486458211:i=2310:bd=all:ss=included_2877 on theBenchmark for (2877ds/2310Mi)
% 128.70/27.04  % (677475)Instruction limit reached! 
% 128.70/27.04  % (677475)------------------------------
% 128.70/27.04  % (677475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677475)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677475)Termination reason: Instruction limit
% 128.70/27.04  % (677475)Termination phase: Saturation
% 128.70/27.04  % (677475)Time elapsed: 0.673 s
% 128.70/27.04  % (677475)Peak memory usage: 111 MB
% 128.70/27.04  % (677475)Instructions burned: 2312 (million)
% 128.70/27.04  % (677477)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=2524570455:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2869 on theBenchmark for (2869ds/2616Mi)
% 128.70/27.04  % (677477)Instruction limit reached! 
% 128.70/27.04  % (677477)------------------------------
% 128.70/27.04  % (677477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677477)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677477)Termination reason: Instruction limit
% 128.70/27.04  % (677477)Termination phase: Saturation
% 128.70/27.04  % (677477)Time elapsed: 0.753 s
% 128.70/27.04  % (677477)Peak memory usage: 107 MB
% 128.70/27.04  % (677477)Instructions burned: 2619 (million)
% 128.70/27.04  % (677479)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=3312937588:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2861 on theBenchmark for (2861ds/30521Mi)
% 128.70/27.04  % (677473)Instruction limit reached! 
% 128.70/27.04  % (677473)------------------------------
% 128.70/27.04  % (677473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677473)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677473)Termination reason: Instruction limit
% 128.70/27.04  % (677473)Termination phase: Saturation
% 128.70/27.04  % (677473)Time elapsed: 3.916 s
% 128.70/27.04  % (677473)Peak memory usage: 169 MB
% 128.70/27.04  % (677473)Instructions burned: 6462 (million)
% 128.70/27.04  % (677469)Instruction limit reached! 
% 128.70/27.04  % (677469)------------------------------
% 128.70/27.04  % (677469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677469)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677469)Termination reason: Instruction limit
% 128.70/27.04  % (677469)Termination phase: Saturation
% 128.70/27.04  % (677469)Time elapsed: 5.598 s
% 128.70/27.04  % (677469)Peak memory usage: 202 MB
% 128.70/27.04  % (677469)Instructions burned: 9356 (million)
% 128.70/27.04  % (677481)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=1688595043:i=3258:fgj=on:bd=all:ins=1_2842 on theBenchmark for (2842ds/3258Mi)
% 128.70/27.04  % (677482)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=1418131394:i=5037:kws=precedence_2842 on theBenchmark for (2842ds/5037Mi)
% 128.70/27.04  % (677481)Instruction limit reached! 
% 128.70/27.04  % (677481)------------------------------
% 128.70/27.04  % (677481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677481)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677481)Termination reason: Instruction limit
% 128.70/27.04  % (677481)Termination phase: Saturation
% 128.70/27.04  % (677481)Time elapsed: 2.102 s
% 128.70/27.04  % (677481)Peak memory usage: 151 MB
% 128.70/27.04  % (677481)Instructions burned: 3260 (million)
% 128.70/27.04  % (677485)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=1494909412:i=65240_2820 on theBenchmark for (2820ds/65240Mi)
% 128.70/27.04  % (677482)Instruction limit reached! 
% 128.70/27.04  % (677482)------------------------------
% 128.70/27.04  % (677482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677482)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677482)Termination reason: Instruction limit
% 128.70/27.04  % (677482)Termination phase: Saturation
% 128.70/27.04  % (677482)Time elapsed: 2.841 s
% 128.70/27.04  % (677482)Peak memory usage: 166 MB
% 128.70/27.04  % (677482)Instructions burned: 5037 (million)
% 128.70/27.04  % (677487)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=2562223637:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2812 on theBenchmark for (2812ds/16502Mi)
% 128.70/27.04  % (677467)Instruction limit reached! 
% 128.70/27.04  % (677467)------------------------------
% 128.70/27.04  % (677467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677467)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677467)Termination reason: Instruction limit
% 128.70/27.04  % (677467)Termination phase: Saturation
% 128.70/27.04  % (677467)Time elapsed: 10.257 s
% 128.70/27.04  % (677467)Peak memory usage: 258 MB
% 128.70/27.04  % (677467)Instructions burned: 16427 (million)
% 128.70/27.04  % (677489)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=2719450412:i=7623:bd=preordered:er=filter_2807 on theBenchmark for (2807ds/7623Mi)
% 128.70/27.04  % (677489)Instruction limit reached! 
% 128.70/27.04  % (677489)------------------------------
% 128.70/27.04  % (677489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677489)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677489)Termination reason: Instruction limit
% 128.70/27.04  % (677489)Termination phase: Saturation
% 128.70/27.04  % (677489)Time elapsed: 4.174 s
% 128.70/27.04  % (677489)Peak memory usage: 198 MB
% 128.70/27.04  % (677489)Instructions burned: 7624 (million)
% 128.70/27.04  % (677491)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=3084891894:i=8183:kws=frequency:add=off:gsp=on_2764 on theBenchmark for (2764ds/8183Mi)
% 128.70/27.04  % (677479)Instruction limit reached! 
% 128.70/27.04  % (677479)------------------------------
% 128.70/27.04  % (677479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.70/27.04  % (677479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.70/27.04  % (677479)CaDiCaL version: 2.1.3
% 128.70/27.04  % (677479)Termination reason: Instruction limit
% 128.70/27.04  % (677479)Termination phase: Saturation
% 128.70/27.04  % (677479)Time elapsed: 10.274 s
% 128.70/27.04  % (677479)Peak memory usage: 404 MB
% 128.70/27.04  % (677479)Instructions burned: 30522 (million)
% 128.70/27.04  % (677493)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:bsr=unit_only:random_seed=3806443035:i=8387_2756 on theBenchmark for (2756ds/8387Mi)
% 128.70/27.04  % (677487)First to succeed.
% 128.70/27.04  % (677487)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-677426"
% 128.70/27.04  % (677487)Refutation found. Thanks to Tanya!
% 128.70/27.04  % SZS status Unsatisfiable for theBenchmark
% 128.70/27.04  % SZS output start Proof for theBenchmark
% See solution above
% 186.25/27.13  % (677487)------------------------------
% 186.25/27.13  % (677487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.25/27.13  % (677487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.25/27.13  % (677487)CaDiCaL version: 2.1.3
% 186.25/27.13  % (677487)Termination reason: Refutation
% 186.25/27.13  % (677487)Time elapsed: 6.971 s
% 186.25/27.13  % (677487)Peak memory usage: 208 MB
% 186.25/27.13  % (677487)Instructions burned: 11142 (million)
% 186.25/27.13  % (677487)------------------------------
% 186.25/27.13  % (677487)------------------------------
% 186.25/27.13  % (677426)Success in time 26.204 s
% 186.25/27.13  % Vampire exiting
%------------------------------------------------------------------------------