%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP049-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:14 AM UTC 2026
% Result : Unsatisfiable 6.69s 1.98s
% Output : Refutation 8.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 16
% Syntax : Number of formulae : 253 ( 178 unt; 14 def)
% Number of atoms : 334 ( 246 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 163 ( 82 ~; 78 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 18 con; 0-2 aty)
% Number of variables : 469 ( 0 sgn 469 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),inverse(multiply(X1,multiply(inverse(X1),X1)))))) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f3,plain,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| a2 != multiply(multiply(inverse(b2),b2),a2)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
inference(reorient_equations,[],[f2]) ).
fof(f4,definition,
sF0 = inverse(a1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f5,plain,
inverse(a1) = sF0,
inference(reorient_equations,[],[f4]) ).
fof(f6,definition,
sF1 = multiply(sF0,a1),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f7,plain,
multiply(sF0,a1) = sF1,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF2 = inverse(b1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f9,plain,
inverse(b1) = sF2,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF3 = multiply(sF2,b1),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f11,plain,
multiply(sF2,b1) = sF3,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF4 = inverse(b2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f13,plain,
inverse(b2) = sF4,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF5 = multiply(sF4,b2),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f15,plain,
multiply(sF4,b2) = sF5,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF6 = multiply(sF5,a2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f17,plain,
multiply(sF5,a2) = sF6,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF7 = multiply(a3,b3),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f19,plain,
multiply(a3,b3) = sF7,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF8 = multiply(sF7,c3),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f21,plain,
multiply(sF7,c3) = sF8,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF9 = multiply(b3,c3),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f23,plain,
multiply(b3,c3) = sF9,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF10 = multiply(a3,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f25,plain,
multiply(a3,sF9) = sF10,
inference(reorient_equations,[],[f24]) ).
fof(f26,plain,
( sF1 != sF3
| a2 != sF6
| sF8 != sF10 ),
inference(definition_folding,[],[f3,f25,f23,f21,f19,f17,f15,f13,f11,f9,f7,f5]) ).
fof(f28,definition,
( spl11_1
<=> sF8 = sF10 ),
introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition]) ).
fof(f30,plain,
( sF8 != sF10
| spl11_1 ),
inference(avatar_component_clause,[],[f28]) ).
fof(f32,definition,
( spl11_2
<=> a2 = sF6 ),
introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition]) ).
fof(f36,definition,
( spl11_3
<=> sF1 = sF3 ),
introduced(definition,[new_symbols(definition,[spl11_3])],[avatar_definition]) ).
fof(f37,plain,
( sF1 = sF3
| ~ spl11_3 ),
inference(avatar_component_clause,[],[f36]) ).
fof(f39,plain,
( ~ spl11_1
| ~ spl11_2
| ~ spl11_3 ),
inference(avatar_split_clause,[],[f26,f36,f32,f28]) ).
fof(f40,plain,
multiply(inverse(a1),a1) = sF1,
inference(forward_demodulation,[],[f7,f5]) ).
fof(f41,plain,
multiply(inverse(b1),b1) = sF3,
inference(forward_demodulation,[],[f11,f9]) ).
fof(f42,plain,
multiply(inverse(b2),b2) = sF5,
inference(forward_demodulation,[],[f15,f13]) ).
fof(f44,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),X0)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,multiply(inverse(X2),X2)))))),
inference(superposition,[],[f1,f1]) ).
fof(f51,plain,
! [X0] : multiply(inverse(a1),inverse(multiply(inverse(multiply(inverse(sF1),X0)),inverse(multiply(a1,sF1))))) = X0,
inference(superposition,[],[f1,f40]) ).
fof(f58,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF1),X0)),X1)),inverse(multiply(X0,multiply(inverse(X0),X0))))) = multiply(inverse(a1),inverse(multiply(inverse(X1),inverse(multiply(a1,sF1))))),
inference(superposition,[],[f44,f40]) ).
fof(f62,plain,
! [X0,X1] : multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,multiply(inverse(b3),b3)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF7),X0)),X1)),inverse(multiply(X0,multiply(inverse(X0),X0))))),
inference(superposition,[],[f44,f19]) ).
fof(f74,plain,
! [X2,X0,X1] : multiply(X0,inverse(multiply(inverse(X2),inverse(multiply(X1,multiply(inverse(X1),X1)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),a1)),X2)),inverse(multiply(a1,sF1)))),
inference(superposition,[],[f44,f40]) ).
fof(f76,plain,
! [X2,X0,X1] : multiply(X0,inverse(multiply(inverse(X2),inverse(multiply(X1,multiply(inverse(X1),X1)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),b2)),X2)),inverse(multiply(b2,sF5)))),
inference(superposition,[],[f44,f42]) ).
fof(f84,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,X2)),multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2))))))) = X1,
inference(superposition,[],[f1,f44]) ).
fof(f88,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(X0,X1)),X3))),inverse(multiply(X2,multiply(inverse(X2),X2))))) = X3,
inference(superposition,[],[f1,f44]) ).
fof(f151,plain,
! [X0,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X4)),multiply(X0,X5))),inverse(multiply(X4,multiply(inverse(X4),X4))))) = X5,
inference(superposition,[],[f88,f88]) ).
fof(f166,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(X3,X4)),X2)),multiply(inverse(multiply(X3,X4)),X0)) = multiply(inverse(multiply(X1,X2)),multiply(X1,X0)),
inference(superposition,[],[f84,f88]) ).
fof(f170,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),multiply(inverse(multiply(X1,X2)),X0))),inverse(multiply(inverse(multiply(X0,X4)),inverse(multiply(inverse(multiply(X3,multiply(inverse(X3),X3))),multiply(inverse(inverse(multiply(X3,multiply(inverse(X3),X3)))),inverse(multiply(X3,multiply(inverse(X3),X3))))))))) = X4,
inference(superposition,[],[f1,f88]) ).
fof(f177,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),multiply(inverse(multiply(X1,X2)),X0))),inverse(multiply(X3,multiply(inverse(X3),X3))))),b2)),multiply(X0,X4))),inverse(multiply(b2,sF5)))) = X4,
inference(forward_demodulation,[],[f170,f76]) ).
fof(f183,plain,
! [X0,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),multiply(X0,X4))),inverse(multiply(b2,sF5)))) = X4,
inference(forward_demodulation,[],[f177,f151]) ).
fof(f191,plain,
! [X0] : inverse(multiply(inverse(multiply(inverse(sF5),multiply(inverse(b2),X0))),inverse(multiply(b2,sF5)))) = X0,
inference(superposition,[],[f151,f42]) ).
fof(f199,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X0)),inverse(multiply(X2,multiply(inverse(X2),X2))))) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X3)),X0)),inverse(multiply(X3,multiply(inverse(X3),X3))))),
inference(superposition,[],[f151,f1]) ).
fof(f212,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,a1)),multiply(X0,X1))),inverse(multiply(a1,sF1)))) = X1,
inference(superposition,[],[f151,f40]) ).
fof(f219,plain,
! [X2,X0,X1] : inverse(multiply(X2,multiply(inverse(X2),X2))) = multiply(inverse(multiply(X1,X2)),inverse(multiply(X0,inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),multiply(X1,X0))))))),
inference(superposition,[],[f1,f151]) ).
fof(f221,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(multiply(X3,X2)),multiply(X3,X0)),
inference(superposition,[],[f84,f151]) ).
fof(f283,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X3,inverse(multiply(X4,multiply(inverse(X4),X4))))),multiply(X3,X5)) = multiply(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X2)),X4)),X1)),X5)),
inference(superposition,[],[f221,f44]) ).
fof(f284,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,X3)) = multiply(X0,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X0))),X3)),
inference(superposition,[],[f221,f151]) ).
fof(f285,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),X0)),inverse(multiply(X4,multiply(inverse(X4),X4))))))) = multiply(inverse(multiply(X3,X2)),X0),
inference(superposition,[],[f221,f1]) ).
fof(f500,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(inverse(X1),X1))))),multiply(X0,X2)) = multiply(a1,multiply(inverse(multiply(inverse(multiply(inverse(a1),X1)),sF1)),X2)),
inference(superposition,[],[f284,f40]) ).
fof(f577,plain,
! [X2,X0,X1,X4,X5] : multiply(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X2)),X4)),X1)),X5)) = multiply(a1,multiply(inverse(multiply(inverse(multiply(inverse(a1),X4)),sF1)),X5)),
inference(backward_demodulation,[],[f283,f500]) ).
fof(f667,plain,
! [X0,X1] : inverse(multiply(X0,inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))) = multiply(X1,inverse(multiply(inverse(inverse(multiply(b2,sF5))),inverse(multiply(b2,multiply(inverse(b2),b2)))))),
inference(superposition,[],[f44,f183]) ).
fof(f689,plain,
! [X0,X1] : inverse(multiply(X0,inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))) = multiply(X1,inverse(multiply(inverse(inverse(multiply(b2,sF5))),inverse(multiply(b2,sF5))))),
inference(forward_demodulation,[],[f667,f42]) ).
fof(f706,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X0)),inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X0)),inverse(multiply(X2,multiply(inverse(X2),X2)))))),inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X0)),inverse(multiply(X2,multiply(inverse(X2),X2)))))))) = multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(multiply(X1,X3),multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))),
inference(superposition,[],[f219,f1]) ).
fof(f724,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X3,multiply(inverse(X3),X3))),multiply(inverse(inverse(multiply(X3,multiply(inverse(X3),X3)))),inverse(multiply(X3,multiply(inverse(X3),X3)))))) = multiply(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2)))))),inverse(multiply(X4,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X2)),X3)),X1)),X4),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X2)),X3)),X1)),X4)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X2)),X3)),X1)),X4))))))),
inference(superposition,[],[f219,f44]) ).
fof(f749,plain,
! [X0] : inverse(multiply(X0,multiply(inverse(X0),X0))) = multiply(inverse(multiply(sF7,X0)),inverse(multiply(c3,inverse(multiply(sF8,multiply(inverse(sF8),sF8)))))),
inference(superposition,[],[f219,f21]) ).
fof(f788,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),inverse(multiply(X0,multiply(inverse(X0),X0))))) = multiply(X1,inverse(multiply(inverse(inverse(multiply(X3,inverse(multiply(multiply(inverse(multiply(X1,X2)),X3),multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),multiply(inverse(multiply(X1,X2)),X3))))))),inverse(multiply(X2,multiply(inverse(X2),X2)))))),
inference(superposition,[],[f44,f219]) ).
fof(f790,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,inverse(X2)))),inverse(multiply(X0,multiply(inverse(X0),X0)))) = X2,
inference(superposition,[],[f84,f219]) ).
fof(f800,plain,
! [X2,X0,X1] : inverse(multiply(X2,inverse(multiply(multiply(X1,X2),multiply(inverse(multiply(X1,X2)),multiply(X1,X2)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X0)),b2)),inverse(multiply(X0,multiply(inverse(X0),X0))))),inverse(multiply(b2,sF5)))),
inference(superposition,[],[f183,f219]) ).
fof(f814,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),inverse(multiply(X0,multiply(inverse(X0),X0))))) = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),inverse(multiply(inverse(inverse(multiply(b2,sF5))),inverse(multiply(b2,sF5)))))),inverse(multiply(X2,multiply(inverse(X2),X2)))))),
inference(forward_demodulation,[],[f788,f689]) ).
fof(f827,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X3,multiply(inverse(X3),X3))),multiply(inverse(inverse(multiply(X3,multiply(inverse(X3),X3)))),inverse(multiply(X3,multiply(inverse(X3),X3)))))) = multiply(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X2)),X3)),X1)),inverse(multiply(inverse(inverse(multiply(b2,sF5))),inverse(multiply(b2,sF5)))))),
inference(forward_demodulation,[],[f724,f689]) ).
fof(f839,plain,
! [X2,X3,X0,X1] : multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(multiply(X1,X3),multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))) = multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X0)),inverse(multiply(X2,multiply(inverse(X2),X2))))))),inverse(multiply(c3,inverse(multiply(sF8,multiply(inverse(sF8),sF8)))))),
inference(forward_demodulation,[],[f706,f749]) ).
fof(f842,plain,
! [X0] : inverse(multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),inverse(multiply(X0,multiply(inverse(X0),X0))))) = inverse(multiply(inverse(inverse(multiply(b2,sF5))),inverse(multiply(b2,sF5)))),
inference(forward_demodulation,[],[f814,f1]) ).
fof(f844,plain,
! [X3] : inverse(multiply(inverse(multiply(X3,multiply(inverse(X3),X3))),multiply(inverse(inverse(multiply(X3,multiply(inverse(X3),X3)))),inverse(multiply(X3,multiply(inverse(X3),X3)))))) = multiply(a1,multiply(inverse(multiply(inverse(multiply(inverse(a1),X3)),sF1)),inverse(multiply(inverse(inverse(multiply(b2,sF5))),inverse(multiply(b2,sF5)))))),
inference(forward_demodulation,[],[f827,f577]) ).
fof(f901,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,inverse(X4)))),multiply(inverse(multiply(X0,X1)),inverse(multiply(X2,inverse(multiply(multiply(X0,X2),multiply(inverse(multiply(X0,X2)),multiply(X0,X2)))))))) = X4,
inference(superposition,[],[f790,f219]) ).
fof(f909,plain,
! [X2,X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),
inference(superposition,[],[f284,f790]) ).
fof(f937,plain,
! [X2,X0] : multiply(inverse(X0),X0) = multiply(a1,multiply(inverse(multiply(inverse(multiply(inverse(a1),X2)),sF1)),inverse(multiply(X2,multiply(inverse(X2),X2))))),
inference(forward_demodulation,[],[f909,f500]) ).
fof(f1014,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),inverse(multiply(X2,multiply(inverse(X2),X2))))) = inverse(multiply(inverse(multiply(inverse(X0),X3)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X4)),X0)),inverse(multiply(X4,multiply(inverse(X4),X4))))),multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(X1,X4)),X0)),inverse(multiply(X4,multiply(inverse(X4),X4)))))),inverse(multiply(inverse(multiply(inverse(multiply(X1,X4)),X0)),inverse(multiply(X4,multiply(inverse(X4),X4)))))))))),
inference(superposition,[],[f199,f1]) ).
fof(f1027,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(b2),X0)),X1)),inverse(multiply(X0,multiply(inverse(X0),X0))))) = inverse(multiply(inverse(multiply(inverse(sF5),X1)),inverse(multiply(b2,sF5)))),
inference(superposition,[],[f199,f42]) ).
fof(f1045,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),inverse(multiply(X0,multiply(inverse(X0),X0))))) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),inverse(multiply(X3,inverse(multiply(multiply(X1,X3),multiply(inverse(multiply(X1,X3)),multiply(X1,X3)))))))),inverse(multiply(X2,multiply(inverse(X2),X2))))),
inference(superposition,[],[f199,f219]) ).
fof(f1051,plain,
! [X2,X3,X0,X1] : inverse(multiply(X0,inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),inverse(multiply(X2,multiply(inverse(X2),X2))))),inverse(multiply(X3,multiply(inverse(X3),X3))))),
inference(superposition,[],[f199,f151]) ).
fof(f1067,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),inverse(multiply(X1,multiply(inverse(X1),X1))))) = inverse(multiply(inverse(multiply(inverse(multiply(X0,a1)),X2)),inverse(multiply(a1,sF1)))),
inference(superposition,[],[f199,f40]) ).
fof(f1068,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),inverse(multiply(X1,multiply(inverse(X1),X1))))) = inverse(multiply(inverse(multiply(inverse(multiply(X0,b1)),X2)),inverse(multiply(b1,sF3)))),
inference(superposition,[],[f199,f41]) ).
fof(f1198,plain,
! [X1] : multiply(inverse(a1),inverse(multiply(inverse(X1),inverse(multiply(a1,sF1))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF1),b1)),X1)),inverse(multiply(b1,sF3)))),
inference(backward_demodulation,[],[f58,f1068]) ).
fof(f1202,plain,
! [X1] : multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,multiply(inverse(b3),b3)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF7),b1)),X1)),inverse(multiply(b1,sF3)))),
inference(backward_demodulation,[],[f62,f1068]) ).
fof(f1212,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X3,X2)),X0) = multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X3,b1)),X0)),inverse(multiply(b1,sF3)))))),
inference(backward_demodulation,[],[f285,f1068]) ).
fof(f1220,plain,
! [X3,X0,X1] : multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(multiply(X1,X3),multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))) = multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,b1)),X0)),inverse(multiply(b1,sF3)))))),inverse(multiply(c3,inverse(multiply(sF8,multiply(inverse(sF8),sF8)))))),
inference(backward_demodulation,[],[f839,f1068]) ).
fof(f1278,plain,
! [X2,X1] : inverse(multiply(X2,inverse(multiply(multiply(X1,X2),multiply(inverse(multiply(X1,X2)),multiply(X1,X2)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,b1)),b2)),inverse(multiply(b1,sF3)))),inverse(multiply(b2,sF5)))),
inference(backward_demodulation,[],[f800,f1068]) ).
fof(f1287,plain,
! [X2,X0] : inverse(multiply(inverse(multiply(inverse(multiply(X0,a1)),X2)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(multiply(inverse(multiply(X0,b1)),X2)),inverse(multiply(b1,sF3)))),
inference(backward_demodulation,[],[f1068,f1067]) ).
fof(f1303,plain,
! [X2,X0,X1] : inverse(multiply(X0,inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),a1)),inverse(multiply(X2,multiply(inverse(X2),X2))))),inverse(multiply(a1,sF1)))),
inference(forward_demodulation,[],[f1051,f1067]) ).
fof(f1309,plain,
! [X3,X0,X1] : inverse(multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),inverse(multiply(X0,multiply(inverse(X0),X0))))) = inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),inverse(multiply(X3,inverse(multiply(multiply(X1,X3),multiply(inverse(multiply(X1,X3)),multiply(X1,X3)))))))),inverse(multiply(a1,sF1)))),
inference(forward_demodulation,[],[f1045,f1067]) ).
fof(f1327,plain,
! [X1] : inverse(multiply(inverse(multiply(inverse(sF5),X1)),inverse(multiply(b2,sF5)))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(b2),a1)),X1)),inverse(multiply(a1,sF1)))),
inference(forward_demodulation,[],[f1027,f1067]) ).
fof(f1340,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),inverse(multiply(X2,multiply(inverse(X2),X2))))) = inverse(multiply(inverse(multiply(inverse(X0),X3)),multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,X4)),X0)),inverse(multiply(X4,multiply(inverse(X4),X4))))))),inverse(multiply(c3,inverse(multiply(sF8,multiply(inverse(sF8),sF8)))))))),
inference(forward_demodulation,[],[f1014,f749]) ).
fof(f1418,plain,
! [X2,X1] : inverse(multiply(X2,inverse(multiply(multiply(X1,X2),multiply(inverse(multiply(X1,X2)),multiply(X1,X2)))))) = multiply(X1,inverse(multiply(inverse(inverse(multiply(b1,sF3))),inverse(multiply(b1,multiply(inverse(b1),b1)))))),
inference(forward_demodulation,[],[f1278,f76]) ).
fof(f1487,plain,
! [X1] : multiply(inverse(a1),inverse(multiply(inverse(X1),inverse(multiply(a1,sF1))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF1),a1)),X1)),inverse(multiply(a1,sF1)))),
inference(backward_demodulation,[],[f1198,f1287]) ).
fof(f1491,plain,
! [X1] : multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,multiply(inverse(b3),b3)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF7),a1)),X1)),inverse(multiply(a1,sF1)))),
inference(backward_demodulation,[],[f1202,f1287]) ).
fof(f1497,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X3,X2)),X0) = multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X3,a1)),X0)),inverse(multiply(a1,sF1)))))),
inference(backward_demodulation,[],[f1212,f1287]) ).
fof(f1502,plain,
! [X3,X0,X1] : multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(multiply(X1,X3),multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))) = multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))))),inverse(multiply(c3,inverse(multiply(sF8,multiply(inverse(sF8),sF8)))))),
inference(backward_demodulation,[],[f1220,f1287]) ).
fof(f1562,plain,
! [X0,X1] : inverse(multiply(X0,inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),a1)),inverse(multiply(a1,sF1)))),inverse(multiply(a1,sF1)))),
inference(forward_demodulation,[],[f1303,f1067]) ).
fof(f1568,plain,
! [X0] : inverse(multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),inverse(multiply(X0,multiply(inverse(X0),X0))))) = inverse(multiply(inverse(inverse(multiply(a1,multiply(inverse(a1),a1)))),inverse(multiply(a1,sF1)))),
inference(forward_demodulation,[],[f1309,f219]) ).
fof(f1595,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),inverse(multiply(X2,multiply(inverse(X2),X2))))) = inverse(multiply(inverse(multiply(inverse(X0),X3)),multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))))),inverse(multiply(c3,inverse(multiply(sF8,multiply(inverse(sF8),sF8)))))))),
inference(forward_demodulation,[],[f1340,f1067]) ).
fof(f1633,plain,
! [X2,X1] : inverse(multiply(X2,inverse(multiply(multiply(X1,X2),multiply(inverse(multiply(X1,X2)),multiply(X1,X2)))))) = multiply(X1,inverse(multiply(inverse(inverse(multiply(b1,sF3))),inverse(multiply(b1,sF3))))),
inference(forward_demodulation,[],[f1418,f41]) ).
fof(f1702,plain,
! [X0,X1] : inverse(multiply(X0,inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))) = multiply(X1,inverse(multiply(inverse(inverse(multiply(a1,sF1))),inverse(multiply(a1,multiply(inverse(a1),a1)))))),
inference(forward_demodulation,[],[f1562,f74]) ).
fof(f1705,plain,
! [X0] : inverse(multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),inverse(multiply(X0,multiply(inverse(X0),X0))))) = inverse(multiply(inverse(inverse(multiply(a1,sF1))),inverse(multiply(a1,sF1)))),
inference(forward_demodulation,[],[f1568,f40]) ).
fof(f1713,plain,
! [X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X3)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(multiply(inverse(X0),X3)),multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))))),inverse(multiply(c3,inverse(multiply(sF8,multiply(inverse(sF8),sF8)))))))),
inference(forward_demodulation,[],[f1595,f1067]) ).
fof(f1765,plain,
! [X0,X1] : inverse(multiply(X0,inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))) = multiply(X1,inverse(multiply(inverse(inverse(multiply(a1,sF1))),inverse(multiply(a1,sF1))))),
inference(forward_demodulation,[],[f1702,f40]) ).
fof(f1768,plain,
inverse(multiply(inverse(inverse(multiply(b2,sF5))),inverse(multiply(b2,sF5)))) = inverse(multiply(inverse(inverse(multiply(a1,sF1))),inverse(multiply(a1,sF1)))),
inference(backward_demodulation,[],[f842,f1705]) ).
fof(f1795,plain,
! [X3] : inverse(multiply(inverse(multiply(X3,multiply(inverse(X3),X3))),multiply(inverse(inverse(multiply(X3,multiply(inverse(X3),X3)))),inverse(multiply(X3,multiply(inverse(X3),X3)))))) = multiply(a1,multiply(inverse(multiply(inverse(multiply(inverse(a1),X3)),sF1)),inverse(multiply(inverse(inverse(multiply(a1,sF1))),inverse(multiply(a1,sF1)))))),
inference(backward_demodulation,[],[f844,f1768]) ).
fof(f1953,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),inverse(multiply(X1,multiply(inverse(X1),X1)))) = multiply(inverse(multiply(inverse(multiply(X0,a1)),X2)),inverse(multiply(a1,sF1))),
inference(superposition,[],[f790,f1497]) ).
fof(f1998,plain,
! [X0] : multiply(inverse(X0),X0) = multiply(a1,multiply(inverse(multiply(inverse(multiply(inverse(a1),a1)),sF1)),inverse(multiply(a1,sF1)))),
inference(backward_demodulation,[],[f937,f1953]) ).
fof(f2046,plain,
! [X0] : multiply(inverse(X0),X0) = multiply(a1,multiply(inverse(multiply(inverse(sF1),sF1)),inverse(multiply(a1,sF1)))),
inference(forward_demodulation,[],[f1998,f40]) ).
fof(f2066,plain,
! [X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(X0),X0),
inference(superposition,[],[f2046,f2046]) ).
fof(f2068,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,X0)),inverse(multiply(X2,inverse(multiply(multiply(X1,X2),multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))) = inverse(multiply(X0,multiply(a1,multiply(inverse(multiply(inverse(sF1),sF1)),inverse(multiply(a1,sF1)))))),
inference(superposition,[],[f219,f2046]) ).
fof(f2080,plain,
! [X2,X3,X1] : multiply(X2,multiply(inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X2))),inverse(multiply(X1,multiply(inverse(X1),X1))))) = multiply(a1,multiply(inverse(multiply(inverse(sF1),sF1)),inverse(multiply(a1,sF1)))),
inference(superposition,[],[f284,f2046]) ).
fof(f2122,plain,
! [X2,X3] : multiply(X2,multiply(inverse(multiply(inverse(multiply(X3,a1)),multiply(X3,X2))),inverse(multiply(a1,sF1)))) = multiply(a1,multiply(inverse(multiply(inverse(sF1),sF1)),inverse(multiply(a1,sF1)))),
inference(forward_demodulation,[],[f2080,f1953]) ).
fof(f2137,plain,
! [X3,X1,X4] : multiply(inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,inverse(X4)))),inverse(multiply(X1,multiply(a1,multiply(inverse(multiply(inverse(sF1),sF1)),inverse(multiply(a1,sF1))))))) = X4,
inference(backward_demodulation,[],[f901,f2068]) ).
fof(f2255,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X2),X3)),
inference(superposition,[],[f221,f2066]) ).
fof(f2256,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(inverse(X3),X2)),multiply(inverse(X0),X0)),
inference(superposition,[],[f221,f2066]) ).
fof(f2258,plain,
! [X2,X3,X0,X1,X4] : multiply(X3,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),X1)) = multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(inverse(X0),X0)),
inference(superposition,[],[f284,f2066]) ).
fof(f2260,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,X3)) = multiply(X4,multiply(inverse(multiply(inverse(multiply(inverse(X4),X2)),multiply(inverse(X0),X0))),X3)),
inference(superposition,[],[f284,f2066]) ).
fof(f2269,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(X4,multiply(inverse(multiply(inverse(multiply(X5,X2)),multiply(X5,X4))),X3)) = multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X0),X0))))),multiply(X1,X3)),
inference(superposition,[],[f284,f2066]) ).
fof(f2272,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X4,X3)),multiply(X4,multiply(X1,X2))) = multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),multiply(inverse(X0),X0)),
inference(superposition,[],[f166,f2066]) ).
fof(f2276,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,X3)) = multiply(X2,multiply(inverse(multiply(inverse(X0),X0)),X3)),
inference(superposition,[],[f284,f2066]) ).
fof(f2281,plain,
! [X2,X3,X0,X4] : multiply(inverse(X0),X0) = multiply(X3,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),inverse(multiply(X2,multiply(inverse(X2),X2))))),
inference(superposition,[],[f284,f2066]) ).
fof(f2284,plain,
! [X2,X0,X1] : inverse(multiply(X2,multiply(inverse(X2),X2))) = multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(inverse(X0),X0)))),
inference(superposition,[],[f84,f2066]) ).
fof(f2285,plain,
! [X0] : sF1 = multiply(inverse(X0),X0),
inference(superposition,[],[f40,f2066]) ).
fof(f2286,plain,
! [X0] : sF3 = multiply(inverse(X0),X0),
inference(superposition,[],[f41,f2066]) ).
fof(f2287,plain,
! [X0] : sF5 = multiply(inverse(X0),X0),
inference(superposition,[],[f42,f2066]) ).
fof(f2293,plain,
! [X2,X0,X1] : inverse(multiply(X1,multiply(inverse(X0),X0))) = multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X2,inverse(multiply(multiply(inverse(X1),X2),multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(X1),X2))))))),
inference(superposition,[],[f219,f2066]) ).
fof(f2310,plain,
! [X0,X1] : inverse(multiply(X1,multiply(inverse(X0),X0))) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),inverse(multiply(inverse(inverse(multiply(b1,sF3))),inverse(multiply(b1,sF3)))))),
inference(forward_demodulation,[],[f2293,f1633]) ).
fof(f2361,plain,
! [X0] : multiply(inverse(multiply(sF7,X0)),inverse(multiply(c3,inverse(multiply(sF8,multiply(inverse(sF8),sF8)))))) = inverse(multiply(X0,sF5)),
inference(backward_demodulation,[],[f749,f2287]) ).
fof(f2415,plain,
! [X3] : multiply(a1,multiply(inverse(multiply(inverse(multiply(inverse(a1),X3)),sF1)),inverse(multiply(inverse(inverse(multiply(a1,sF1))),inverse(multiply(a1,sF1)))))) = inverse(multiply(inverse(multiply(X3,sF5)),multiply(inverse(inverse(multiply(X3,sF5))),inverse(multiply(X3,sF5))))),
inference(backward_demodulation,[],[f1795,f2287]) ).
fof(f2512,plain,
! [X3,X0,X1] : multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))))),inverse(multiply(c3,inverse(multiply(sF8,multiply(inverse(sF8),sF8)))))) = multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(multiply(X1,X3),sF5))))),
inference(backward_demodulation,[],[f1502,f2287]) ).
fof(f2516,plain,
! [X0,X1] : multiply(X1,inverse(multiply(inverse(inverse(multiply(a1,sF1))),inverse(multiply(a1,sF1))))) = inverse(multiply(X0,inverse(multiply(multiply(X1,X0),sF5)))),
inference(backward_demodulation,[],[f1765,f2287]) ).
fof(f2553,plain,
sF1 = sF5,
inference(backward_demodulation,[],[f40,f2287]) ).
fof(f2554,plain,
sF3 = sF5,
inference(backward_demodulation,[],[f41,f2287]) ).
fof(f2559,plain,
! [X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF7),a1)),X1)),inverse(multiply(a1,sF1)))) = multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,sF5))))),
inference(backward_demodulation,[],[f1491,f2287]) ).
fof(f2580,plain,
! [X2,X3] : multiply(X2,multiply(inverse(multiply(inverse(multiply(X3,a1)),multiply(X3,X2))),inverse(multiply(a1,sF1)))) = multiply(a1,multiply(inverse(sF5),inverse(multiply(a1,sF1)))),
inference(backward_demodulation,[],[f2122,f2287]) ).
fof(f2583,plain,
! [X3,X1,X4] : multiply(inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,inverse(X4)))),inverse(multiply(X1,multiply(a1,multiply(inverse(sF5),inverse(multiply(a1,sF1))))))) = X4,
inference(backward_demodulation,[],[f2137,f2287]) ).
fof(f2593,plain,
! [X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X3)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(multiply(inverse(X0),X3)),multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))))),inverse(multiply(c3,inverse(multiply(sF8,sF5))))))),
inference(backward_demodulation,[],[f1713,f2287]) ).
fof(f2602,plain,
sF1 = sF3,
inference(backward_demodulation,[],[f2286,f2285]) ).
fof(f2603,plain,
! [X2,X1] : inverse(multiply(X2,multiply(inverse(X2),X2))) = multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(sF1))),
inference(forward_demodulation,[],[f2284,f2285]) ).
fof(f2606,plain,
! [X2,X3,X0,X4] : multiply(inverse(X0),X0) = multiply(X3,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),inverse(multiply(X2,sF1)))),
inference(forward_demodulation,[],[f2281,f2285]) ).
fof(f2611,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,X3)) = multiply(X2,multiply(inverse(sF1),X3)),
inference(forward_demodulation,[],[f2276,f2285]) ).
fof(f2615,plain,
! [X2,X3,X1,X4] : multiply(inverse(multiply(X4,X3)),multiply(X4,multiply(X1,X2))) = multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),sF1),
inference(forward_demodulation,[],[f2272,f2285]) ).
fof(f2618,plain,
! [X2,X3,X1,X4,X5] : multiply(X4,multiply(inverse(multiply(inverse(multiply(X5,X2)),multiply(X5,X4))),X3)) = multiply(inverse(multiply(X1,inverse(multiply(X2,sF1)))),multiply(X1,X3)),
inference(forward_demodulation,[],[f2269,f2285]) ).
fof(f2627,plain,
! [X2,X3,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,X3)) = multiply(X4,multiply(inverse(multiply(inverse(multiply(inverse(X4),X2)),sF1)),X3)),
inference(forward_demodulation,[],[f2260,f2285]) ).
fof(f2629,plain,
! [X2,X3,X1,X4] : multiply(X3,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),X1)) = multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2))))),sF1),
inference(forward_demodulation,[],[f2258,f2285]) ).
fof(f2631,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(inverse(X3),X2)),sF1),
inference(forward_demodulation,[],[f2256,f2285]) ).
fof(f2632,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(sF1),multiply(inverse(X2),X3)),
inference(forward_demodulation,[],[f2255,f2285]) ).
fof(f2688,plain,
! [X0,X1] : inverse(multiply(X1,multiply(inverse(X0),X0))) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),inverse(sF1))),
inference(forward_demodulation,[],[f2310,f2285]) ).
fof(f2692,plain,
sF6 = multiply(sF3,a2),
inference(backward_demodulation,[],[f17,f2554]) ).
fof(f2696,plain,
! [X0] : inverse(multiply(inverse(multiply(inverse(sF3),multiply(inverse(b2),X0))),inverse(multiply(b2,sF3)))) = X0,
inference(backward_demodulation,[],[f191,f2554]) ).
fof(f2709,plain,
! [X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(b2),a1)),X1)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(multiply(inverse(sF3),X1)),inverse(multiply(b2,sF3)))),
inference(backward_demodulation,[],[f1327,f2554]) ).
fof(f2721,plain,
! [X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF7),a1)),X1)),inverse(multiply(a1,sF1)))) = multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,sF3))))),
inference(backward_demodulation,[],[f2559,f2554]) ).
fof(f2741,plain,
! [X2,X3] : multiply(X2,multiply(inverse(multiply(inverse(multiply(X3,a1)),multiply(X3,X2))),inverse(multiply(a1,sF1)))) = multiply(a1,multiply(inverse(sF3),inverse(multiply(a1,sF1)))),
inference(backward_demodulation,[],[f2580,f2554]) ).
fof(f2744,plain,
! [X3,X1,X4] : multiply(inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,inverse(X4)))),inverse(multiply(X1,multiply(a1,multiply(inverse(sF3),inverse(multiply(a1,sF1))))))) = X4,
inference(backward_demodulation,[],[f2583,f2554]) ).
fof(f2753,plain,
! [X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X3)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(multiply(inverse(X0),X3)),multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))))),inverse(multiply(c3,inverse(multiply(sF8,sF3))))))),
inference(backward_demodulation,[],[f2593,f2554]) ).
fof(f2797,plain,
! [X0,X1] : multiply(X1,inverse(multiply(inverse(inverse(multiply(a1,sF1))),inverse(multiply(a1,sF1))))) = inverse(multiply(X0,inverse(multiply(multiply(X1,X0),sF1)))),
inference(forward_demodulation,[],[f2516,f2553]) ).
fof(f2801,plain,
! [X3,X0,X1] : multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))))),inverse(multiply(c3,inverse(multiply(sF8,multiply(inverse(sF8),sF8)))))) = multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(multiply(X1,X3),sF1))))),
inference(forward_demodulation,[],[f2512,f2553]) ).
fof(f2898,plain,
! [X3] : multiply(a1,multiply(inverse(multiply(inverse(multiply(inverse(a1),X3)),sF1)),inverse(multiply(inverse(inverse(multiply(a1,sF1))),inverse(multiply(a1,sF1)))))) = inverse(multiply(inverse(multiply(X3,sF5)),sF1)),
inference(forward_demodulation,[],[f2415,f2285]) ).
fof(f2952,plain,
! [X0] : multiply(inverse(multiply(sF7,X0)),inverse(multiply(c3,inverse(multiply(sF8,multiply(inverse(sF8),sF8)))))) = inverse(multiply(X0,sF1)),
inference(forward_demodulation,[],[f2361,f2553]) ).
fof(f3004,plain,
spl11_3,
inference(avatar_split_clause,[],[f2602,f36]) ).
fof(f3005,plain,
! [X2,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(sF1))) = inverse(multiply(X2,sF1)),
inference(forward_demodulation,[],[f2603,f2285]) ).
fof(f3007,plain,
! [X2,X3,X4] : sF1 = multiply(X3,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),inverse(multiply(X2,sF1)))),
inference(forward_demodulation,[],[f2606,f2285]) ).
fof(f3009,plain,
! [X2,X3,X1] : multiply(X2,multiply(inverse(sF1),X3)) = multiply(inverse(multiply(X1,inverse(multiply(X2,sF1)))),multiply(X1,X3)),
inference(forward_demodulation,[],[f2611,f2285]) ).
fof(f3016,plain,
! [X2,X3,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(X2,sF1)))),multiply(X1,X3)) = multiply(X4,multiply(inverse(multiply(inverse(multiply(inverse(X4),X2)),sF1)),X3)),
inference(forward_demodulation,[],[f2627,f2285]) ).
fof(f3017,plain,
! [X2,X3,X1,X4] : multiply(X3,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),X1)) = multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,sF1)))),sF1),
inference(forward_demodulation,[],[f2629,f2285]) ).
fof(f3040,plain,
! [X1] : inverse(multiply(X1,sF1)) = multiply(inverse(sF1),multiply(inverse(X1),inverse(sF1))),
inference(forward_demodulation,[],[f2688,f2285]) ).
fof(f3066,plain,
! [X0,X1] : multiply(X1,inverse(sF1)) = inverse(multiply(X0,inverse(multiply(multiply(X1,X0),sF1)))),
inference(forward_demodulation,[],[f2797,f2285]) ).
fof(f3074,plain,
! [X3,X0,X1] : multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(multiply(X1,X3),sF1))))) = multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))))),inverse(multiply(c3,inverse(multiply(sF8,sF1))))),
inference(forward_demodulation,[],[f2801,f2285]) ).
fof(f3139,plain,
! [X3] : multiply(a1,multiply(inverse(multiply(inverse(multiply(inverse(a1),X3)),sF1)),inverse(multiply(inverse(inverse(multiply(a1,sF1))),inverse(multiply(a1,sF1)))))) = inverse(multiply(inverse(multiply(X3,sF1)),sF1)),
inference(forward_demodulation,[],[f2898,f2553]) ).
fof(f3182,plain,
! [X0] : inverse(multiply(X0,sF1)) = multiply(inverse(multiply(sF7,X0)),inverse(multiply(c3,inverse(multiply(sF8,sF1))))),
inference(forward_demodulation,[],[f2952,f2285]) ).
fof(f3216,plain,
sF1 = multiply(a1,multiply(inverse(sF3),inverse(multiply(a1,sF1)))),
inference(backward_demodulation,[],[f2741,f3007]) ).
fof(f3221,plain,
! [X2,X3,X4,X5] : multiply(X4,multiply(inverse(multiply(inverse(multiply(X5,X2)),multiply(X5,X4))),X3)) = multiply(X2,multiply(inverse(sF1),X3)),
inference(backward_demodulation,[],[f2618,f3009]) ).
fof(f3223,plain,
! [X2,X3,X4] : multiply(X2,multiply(inverse(sF1),X3)) = multiply(X4,multiply(inverse(multiply(inverse(multiply(inverse(X4),X2)),sF1)),X3)),
inference(forward_demodulation,[],[f3016,f3009]) ).
fof(f3248,plain,
! [X0,X1] : multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))))),inverse(multiply(c3,inverse(multiply(sF8,sF1))))) = multiply(inverse(X0),multiply(X1,inverse(sF1))),
inference(forward_demodulation,[],[f3074,f3066]) ).
fof(f3286,plain,
! [X3] : inverse(multiply(inverse(multiply(X3,sF1)),sF1)) = multiply(a1,multiply(inverse(multiply(inverse(multiply(inverse(a1),X3)),sF1)),inverse(sF1))),
inference(forward_demodulation,[],[f3139,f2285]) ).
fof(f3341,plain,
! [X3,X1,X4] : multiply(inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,inverse(X4)))),inverse(multiply(X1,sF1))) = X4,
inference(backward_demodulation,[],[f2744,f3216]) ).
fof(f3354,plain,
! [X2,X1] : multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,sF1)))),sF1) = multiply(X2,multiply(inverse(sF1),X1)),
inference(backward_demodulation,[],[f3017,f3221]) ).
fof(f3442,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X1,inverse(sF1))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))),sF1)),
inference(forward_demodulation,[],[f3248,f3182]) ).
fof(f3469,plain,
! [X3] : inverse(multiply(inverse(multiply(X3,sF1)),sF1)) = multiply(X3,multiply(inverse(sF1),inverse(sF1))),
inference(forward_demodulation,[],[f3286,f3223]) ).
fof(f3518,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X1,inverse(sF1))) = inverse(multiply(a1,multiply(inverse(sF1),multiply(inverse(multiply(X1,a1)),X0)))),
inference(forward_demodulation,[],[f3442,f3354]) ).
fof(f3564,plain,
( sF6 = multiply(sF1,a2)
| ~ spl11_3 ),
inference(backward_demodulation,[],[f2692,f37]) ).
fof(f3566,plain,
( ! [X0] : inverse(multiply(inverse(multiply(inverse(sF1),multiply(inverse(b2),X0))),inverse(multiply(b2,sF1)))) = X0
| ~ spl11_3 ),
inference(backward_demodulation,[],[f2696,f37]) ).
fof(f3573,plain,
( ! [X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(b2),a1)),X1)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(multiply(inverse(sF1),X1)),inverse(multiply(b2,sF1))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f2709,f37]) ).
fof(f3584,plain,
( ! [X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF7),a1)),X1)),inverse(multiply(a1,sF1)))) = multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,sF1)))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f2721,f37]) ).
fof(f3598,plain,
( ! [X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X3)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(multiply(inverse(X0),X3)),multiply(inverse(multiply(sF7,inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))))),inverse(multiply(c3,inverse(multiply(sF8,sF1)))))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f2753,f37]) ).
fof(f3626,plain,
( ! [X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X3)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(multiply(inverse(X0),X3)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X0)),inverse(multiply(a1,sF1)))),sF1))))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f3598,f3182]) ).
fof(f3634,plain,
( ! [X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X3)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(multiply(inverse(X0),X3)),inverse(multiply(a1,multiply(inverse(sF1),multiply(inverse(multiply(X1,a1)),X0))))))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f3626,f3354]) ).
fof(f3640,plain,
( ! [X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X3)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(multiply(inverse(X0),X3)),multiply(inverse(X0),multiply(X1,inverse(sF1)))))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f3634,f3518]) ).
fof(f3642,plain,
( ! [X3,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X3)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(sF1))),X3)),sF1))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f3640,f2615]) ).
fof(f3698,plain,
! [X1] : multiply(inverse(sF1),inverse(multiply(inverse(X1),sF1))) = X1,
inference(superposition,[],[f3341,f2285]) ).
fof(f3729,plain,
! [X0,X1] : multiply(inverse(sF1),multiply(inverse(X0),X1)) = multiply(inverse(multiply(inverse(X1),X0)),sF1),
inference(superposition,[],[f2631,f2285]) ).
fof(f3878,plain,
( ! [X3,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,a1)),X3)),inverse(multiply(a1,sF1)))) = inverse(multiply(inverse(sF1),multiply(inverse(X3),multiply(X1,inverse(sF1)))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f3642,f3729]) ).
fof(f3949,plain,
( ! [X1] : inverse(multiply(inverse(multiply(inverse(sF1),X1)),inverse(multiply(b2,sF1)))) = inverse(multiply(inverse(sF1),multiply(inverse(X1),multiply(inverse(b2),inverse(sF1)))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f3573,f3878]) ).
fof(f3950,plain,
( ! [X1] : multiply(inverse(a1),inverse(multiply(inverse(X1),inverse(multiply(a1,sF1))))) = inverse(multiply(inverse(sF1),multiply(inverse(X1),multiply(inverse(sF1),inverse(sF1)))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f1487,f3878]) ).
fof(f3952,plain,
( ! [X1] : multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,sF1))))) = inverse(multiply(inverse(sF1),multiply(inverse(X1),multiply(inverse(sF7),inverse(sF1)))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f3584,f3878]) ).
fof(f3985,plain,
( ! [X0,X1] : inverse(multiply(inverse(sF1),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(sF1))))) = X1
| ~ spl11_3 ),
inference(backward_demodulation,[],[f212,f3878]) ).
fof(f4013,plain,
( ! [X1] : inverse(multiply(inverse(sF1),inverse(multiply(X1,sF1)))) = X1
| ~ spl11_3 ),
inference(forward_demodulation,[],[f3985,f3005]) ).
fof(f4016,plain,
( ! [X1] : multiply(inverse(a1),inverse(multiply(inverse(X1),inverse(multiply(a1,sF1))))) = inverse(multiply(inverse(sF1),inverse(multiply(inverse(multiply(inverse(X1),sF1)),sF1))))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f3950,f3469]) ).
fof(f4021,plain,
( ! [X1] : multiply(inverse(a1),inverse(multiply(inverse(X1),inverse(multiply(a1,sF1))))) = inverse(multiply(inverse(X1),sF1))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4016,f4013]) ).
fof(f4026,plain,
( ! [X0] : inverse(multiply(inverse(multiply(inverse(sF1),X0)),sF1)) = X0
| ~ spl11_3 ),
inference(backward_demodulation,[],[f51,f4021]) ).
fof(f4027,plain,
( ! [X0] : inverse(multiply(inverse(sF1),multiply(inverse(X0),sF1))) = X0
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4026,f3729]) ).
fof(f4050,plain,
( ! [X0] : multiply(inverse(sF1),inverse(multiply(X0,sF1))) = inverse(multiply(inverse(sF1),multiply(X0,sF1)))
| ~ spl11_3 ),
inference(superposition,[],[f4027,f4013]) ).
fof(f4051,plain,
( ! [X0] : multiply(inverse(sF1),multiply(inverse(X0),sF1)) = inverse(multiply(inverse(sF1),multiply(X0,sF1)))
| ~ spl11_3 ),
inference(superposition,[],[f4027,f4027]) ).
fof(f4052,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X1) = inverse(multiply(inverse(sF1),multiply(inverse(multiply(X0,X1)),multiply(X0,X2))))
| ~ spl11_3 ),
inference(superposition,[],[f4027,f2631]) ).
fof(f4053,plain,
( sF1 = inverse(multiply(inverse(sF1),sF1))
| ~ spl11_3 ),
inference(superposition,[],[f4027,f2285]) ).
fof(f4060,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(X0,X2)),sF1) = multiply(inverse(multiply(X1,X2)),multiply(X1,multiply(inverse(sF1),multiply(inverse(X0),sF1))))
| ~ spl11_3 ),
inference(superposition,[],[f2631,f4027]) ).
fof(f4064,plain,
( sF1 = inverse(sF1)
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4053,f2285]) ).
fof(f4065,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(X0,X2)),sF1) = multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(inverse(sF1),multiply(X0,sF1)))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f4060,f4051]) ).
fof(f4074,plain,
( ! [X1] : inverse(multiply(inverse(sF1),multiply(inverse(X1),sF1))) = X1
| ~ spl11_3 ),
inference(backward_demodulation,[],[f3698,f4050]) ).
fof(f4086,plain,
( ! [X2,X3,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(sF1,multiply(inverse(X2),X3))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f2632,f4064]) ).
fof(f4090,plain,
( ! [X1] : inverse(multiply(X1,sF1)) = multiply(sF1,multiply(inverse(X1),sF1))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f3040,f4064]) ).
fof(f4152,plain,
( ! [X0] : inverse(multiply(inverse(multiply(sF1,multiply(inverse(b2),X0))),inverse(multiply(b2,sF1)))) = X0
| ~ spl11_3 ),
inference(backward_demodulation,[],[f3566,f4064]) ).
fof(f4181,plain,
( ! [X1] : inverse(multiply(inverse(multiply(sF1,X1)),inverse(multiply(b2,sF1)))) = inverse(multiply(sF1,multiply(inverse(X1),multiply(inverse(b2),sF1))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f3949,f4064]) ).
fof(f4183,plain,
( ! [X1] : multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,sF1))))) = inverse(multiply(sF1,multiply(inverse(X1),multiply(inverse(sF7),sF1))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f3952,f4064]) ).
fof(f4219,plain,
( ! [X0] : inverse(multiply(sF1,multiply(X0,sF1))) = multiply(sF1,multiply(inverse(X0),sF1))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f4051,f4064]) ).
fof(f4220,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X1) = inverse(multiply(sF1,multiply(inverse(multiply(X0,X1)),multiply(X0,X2))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f4052,f4064]) ).
fof(f4225,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(X0,X2)),sF1) = multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(sF1,multiply(X0,sF1)))))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4065,f4064]) ).
fof(f4233,plain,
( ! [X1] : inverse(multiply(sF1,multiply(inverse(X1),sF1))) = X1
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4074,f4064]) ).
fof(f4259,plain,
( ! [X0] : inverse(multiply(sF1,multiply(inverse(multiply(inverse(b2),X0)),multiply(inverse(b2),sF1)))) = X0
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4152,f4181]) ).
fof(f4275,plain,
( ! [X0] : inverse(multiply(X0,sF1)) = inverse(multiply(sF1,multiply(X0,sF1)))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f4219,f4090]) ).
fof(f4305,plain,
( ! [X2,X1] : multiply(inverse(X2),X1) = inverse(multiply(sF1,multiply(sF1,multiply(inverse(X1),X2))))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f4220,f4086]) ).
fof(f4344,plain,
( ! [X2,X0] : multiply(inverse(multiply(X0,X2)),sF1) = multiply(sF1,multiply(inverse(X2),inverse(multiply(sF1,multiply(X0,sF1)))))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4225,f4086]) ).
fof(f4348,plain,
( ! [X1] : inverse(inverse(multiply(X1,sF1))) = X1
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4233,f4090]) ).
fof(f4353,plain,
( ! [X0] : inverse(multiply(sF1,multiply(sF1,multiply(inverse(X0),sF1)))) = X0
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4259,f4086]) ).
fof(f4394,plain,
( ! [X2,X0] : multiply(inverse(multiply(X0,X2)),sF1) = multiply(sF1,multiply(inverse(X2),inverse(multiply(X0,sF1))))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4344,f4275]) ).
fof(f4405,plain,
( ! [X0] : multiply(inverse(sF1),X0) = X0
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4353,f4305]) ).
fof(f4425,plain,
( ! [X0] : multiply(sF1,X0) = X0
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4405,f4064]) ).
fof(f4482,plain,
( ! [X2,X1] : multiply(inverse(X2),X1) = inverse(multiply(sF1,multiply(inverse(X1),X2)))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f4305,f4425]) ).
fof(f4501,plain,
( ! [X1] : multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,sF1))))) = inverse(multiply(inverse(X1),multiply(inverse(sF7),sF1)))
| ~ spl11_3 ),
inference(backward_demodulation,[],[f4183,f4425]) ).
fof(f4512,plain,
( ! [X2,X0] : multiply(inverse(X2),inverse(multiply(X0,sF1))) = multiply(inverse(multiply(X0,X2)),sF1)
| ~ spl11_3 ),
inference(backward_demodulation,[],[f4394,f4425]) ).
fof(f4519,plain,
( ! [X1] : inverse(multiply(X1,sF1)) = multiply(inverse(X1),sF1)
| ~ spl11_3 ),
inference(backward_demodulation,[],[f4090,f4425]) ).
fof(f4534,plain,
( a2 = sF6
| ~ spl11_3 ),
inference(backward_demodulation,[],[f3564,f4425]) ).
fof(f4548,plain,
( spl11_2
| ~ spl11_3 ),
inference(avatar_split_clause,[],[f4534,f36,f32]) ).
fof(f4564,plain,
( ! [X2,X0] : inverse(multiply(multiply(X0,X2),sF1)) = multiply(inverse(X2),inverse(multiply(X0,sF1)))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4512,f4519]) ).
fof(f4573,plain,
( ! [X1] : multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,sF1))))) = inverse(multiply(inverse(X1),inverse(multiply(sF7,sF1))))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4501,f4519]) ).
fof(f4586,plain,
( ! [X2,X1] : inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1)
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4482,f4425]) ).
fof(f4654,plain,
( ! [X1] : multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,sF1))))) = inverse(inverse(multiply(multiply(sF7,X1),sF1)))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4573,f4564]) ).
fof(f4729,plain,
( ! [X1] : multiply(sF7,X1) = multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,sF1)))))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4654,f4348]) ).
fof(f4789,plain,
( ! [X1] : multiply(sF7,X1) = multiply(a3,multiply(inverse(inverse(multiply(b3,sF1))),X1))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4729,f4586]) ).
fof(f4838,plain,
( ! [X1] : multiply(sF7,X1) = multiply(a3,multiply(b3,X1))
| ~ spl11_3 ),
inference(forward_demodulation,[],[f4789,f4348]) ).
fof(f5456,plain,
( multiply(sF7,c3) = multiply(a3,sF9)
| ~ spl11_3 ),
inference(superposition,[],[f4838,f23]) ).
fof(f5473,plain,
( multiply(sF7,c3) = sF10
| ~ spl11_3 ),
inference(forward_demodulation,[],[f5456,f25]) ).
fof(f5477,plain,
( sF8 = sF10
| ~ spl11_3 ),
inference(forward_demodulation,[],[f5473,f21]) ).
fof(f5479,plain,
( $false
| spl11_1
| ~ spl11_3 ),
inference(forward_subsumption_resolution,[],[f5477,f30]) ).
fof(f5480,plain,
( spl11_1
| ~ spl11_3 ),
inference(avatar_contradiction_clause,[],[f5479]) ).
cnf(s1,plain,
( ~ spl11_1
| ~ spl11_2
| ~ spl11_3 ),
inference(sat_conversion,[],[f39]) ).
cnf(s2,plain,
spl11_3,
inference(sat_conversion,[],[f3004]) ).
cnf(s8,plain,
( spl11_2
| ~ spl11_3 ),
inference(sat_conversion,[],[f4548]) ).
cnf(s9,plain,
( spl11_1
| ~ spl11_3 ),
inference(sat_conversion,[],[f5480]) ).
cnf(s10,plain,
spl11_1,
inference(rat,[],[s9,s2]) ).
cnf(s11,plain,
spl11_2,
inference(rat,[],[s8,s2]) ).
cnf(s12,plain,
$false,
inference(rat,[],[s1,s2,s11,s10]) ).
fof(f5481,plain,
$false,
inference(avatar_sat_refutation,[],[s12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP049-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n009.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 09:17:00 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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
% 6.69/1.98 % (1761065)Input is clausal, will run a generic CNF schedule.
% 6.69/1.98 % (1761072)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3990824060:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.69/1.98 % (1761075)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1885250751:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.69/1.98 % (1761073)lrs+10_1_sil=8000:sp=occurrence:random_seed=3614588789:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.69/1.98 % (1761074)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2355646690:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.69/1.98 % (1761071)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2369768170:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.69/1.98 % (1761070)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1636914506:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.69/1.98 % (1761076)dis-21_1_sil=8000:lcm=predicate:random_seed=2794493307:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 6.69/1.98 % (1761076)Refutation not found, incomplete strategy
% 6.69/1.98 % (1761076)------------------------------
% 6.69/1.98 % (1761076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761076)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761076)Termination reason: Refutation not found, incomplete strategy
% 6.69/1.98 % (1761076)Time elapsed: 0.001 s
% 6.69/1.98 % (1761076)Peak memory usage: 88 MB
% 6.69/1.98 % (1761073)Instruction limit reached!
% 6.69/1.98 % (1761073)------------------------------
% 6.69/1.98 % (1761073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761073)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761073)Termination reason: Instruction limit
% 6.69/1.98 % (1761073)Termination phase: Saturation
% 6.69/1.98 % (1761073)Time elapsed: 0.064 s
% 6.69/1.98 % (1761073)Peak memory usage: 89 MB
% 6.69/1.98 % (1761073)Instructions burned: 107 (million)
% 6.69/1.98 % (1761074)Instruction limit reached!
% 6.69/1.98 % (1761074)------------------------------
% 6.69/1.98 % (1761074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761074)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761074)Termination reason: Instruction limit
% 6.69/1.98 % (1761074)Termination phase: Saturation
% 6.69/1.98 % (1761074)Time elapsed: 0.071 s
% 6.69/1.98 % (1761074)Peak memory usage: 89 MB
% 6.69/1.98 % (1761074)Instructions burned: 115 (million)
% 6.69/1.98 % (1761075)Instruction limit reached!
% 6.69/1.98 % (1761075)------------------------------
% 6.69/1.98 % (1761075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761075)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761075)Termination reason: Instruction limit
% 6.69/1.98 % (1761075)Termination phase: Saturation
% 6.69/1.98 % (1761075)Time elapsed: 0.100 s
% 6.69/1.98 % (1761075)Peak memory usage: 89 MB
% 6.69/1.98 % (1761075)Instructions burned: 181 (million)
% 6.69/1.98 % (1761085)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3596547262:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 6.69/1.98 % (1761085)Refutation not found, incomplete strategy
% 6.69/1.98 % (1761085)------------------------------
% 6.69/1.98 % (1761085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761085)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761085)Termination reason: Refutation not found, incomplete strategy
% 6.69/1.98 % (1761085)Time elapsed: 0.001 s
% 6.69/1.98 % (1761085)Peak memory usage: 88 MB
% 6.69/1.98 % (1761084)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3726903851:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 6.69/1.98 % (1761084)Refutation not found, incomplete strategy
% 6.69/1.98 % (1761084)------------------------------
% 6.69/1.98 % (1761084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761084)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761084)Termination reason: Refutation not found, incomplete strategy
% 6.69/1.98 % (1761084)Time elapsed: 0.001 s
% 6.69/1.98 % (1761084)Peak memory usage: 88 MB
% 6.69/1.98 % (1761086)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=251099478:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 6.69/1.98 % (1761086)Refutation not found, incomplete strategy
% 6.69/1.98 % (1761086)------------------------------
% 6.69/1.98 % (1761086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761086)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761086)Termination reason: Refutation not found, incomplete strategy
% 6.69/1.98 % (1761086)Time elapsed: 0.001 s
% 6.69/1.98 % (1761086)Peak memory usage: 88 MB
% 6.69/1.98 % (1761076)------------------------------
% 6.69/1.98 % (1761076)------------------------------
% 6.69/1.98 % (1761090)lrs+10_64_to=lpo:sil=8000:random_seed=812037453:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 6.69/1.98 % (1761084)------------------------------
% 6.69/1.98 % (1761084)------------------------------
% 6.69/1.98 % (1761085)------------------------------
% 6.69/1.98 % (1761085)------------------------------
% 6.69/1.98 % (1761090)Instruction limit reached!
% 6.69/1.98 % (1761090)------------------------------
% 6.69/1.98 % (1761090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761090)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761090)Termination reason: Instruction limit
% 6.69/1.98 % (1761090)Termination phase: Saturation
% 6.69/1.98 % (1761090)Time elapsed: 0.075 s
% 6.69/1.98 % (1761090)Peak memory usage: 89 MB
% 6.69/1.98 % (1761090)Instructions burned: 127 (million)
% 6.69/1.98 % (1761086)------------------------------
% 6.69/1.98 % (1761086)------------------------------
% 6.69/1.98 % (1761093)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=201027328:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 6.69/1.98 % (1761092)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3079537978:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 6.69/1.98 % (1761094)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1118443233:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 6.69/1.98 % (1761095)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=202154069:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 6.69/1.98 % (1761093)Instruction limit reached!
% 6.69/1.98 % (1761093)------------------------------
% 6.69/1.98 % (1761093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761093)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761093)Termination reason: Instruction limit
% 6.69/1.98 % (1761093)Termination phase: Saturation
% 6.69/1.98 % (1761093)Time elapsed: 0.090 s
% 6.69/1.98 % (1761093)Peak memory usage: 90 MB
% 6.69/1.98 % (1761093)Instructions burned: 158 (million)
% 6.69/1.98 % (1761092)Instruction limit reached!
% 6.69/1.98 % (1761092)------------------------------
% 6.69/1.98 % (1761092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761092)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761092)Termination reason: Instruction limit
% 6.69/1.98 % (1761092)Termination phase: Saturation
% 6.69/1.98 % (1761092)Time elapsed: 0.114 s
% 6.69/1.98 % (1761092)Peak memory usage: 90 MB
% 6.69/1.98 % (1761092)Instructions burned: 195 (million)
% 6.69/1.98 % (1761095)Instruction limit reached!
% 6.69/1.98 % (1761095)------------------------------
% 6.69/1.98 % (1761095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761095)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761095)Termination reason: Instruction limit
% 6.69/1.98 % (1761095)Termination phase: Saturation
% 6.69/1.98 % (1761095)Time elapsed: 0.060 s
% 6.69/1.98 % (1761095)Peak memory usage: 90 MB
% 6.69/1.98 % (1761095)Instructions burned: 106 (million)
% 6.69/1.98 % (1761100)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3701560760:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 6.69/1.98 % (1761100)Refutation not found, incomplete strategy
% 6.69/1.98 % (1761100)------------------------------
% 6.69/1.98 % (1761100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761100)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761100)Termination reason: Refutation not found, incomplete strategy
% 6.69/1.98 % (1761100)Time elapsed: 0.001 s
% 6.69/1.98 % (1761100)Peak memory usage: 88 MB
% 6.69/1.98 % (1761101)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2356685139:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 6.69/1.98 % (1761102)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4240082698:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 6.69/1.98 % (1761072)First to succeed.
% 6.69/1.98 % (1761072)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1761065"
% 6.69/1.98 % (1761101)Instruction limit reached!
% 6.69/1.98 % (1761101)------------------------------
% 6.69/1.98 % (1761101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.98 % (1761101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.98 % (1761101)CaDiCaL version: 2.1.3
% 6.69/1.98 % (1761101)Termination reason: Instruction limit
% 6.69/1.98 % (1761101)Termination phase: Saturation
% 6.69/1.98 % (1761101)Time elapsed: 0.131 s
% 6.69/1.98 % (1761101)Peak memory usage: 90 MB
% 6.69/1.98 % (1761101)Instructions burned: 242 (million)
% 6.69/1.98 % (1761072)Refutation found. Thanks to Tanya!
% 6.69/1.98 % SZS status Unsatisfiable for theBenchmark
% 6.69/1.98 % SZS output start Proof for theBenchmark
% See solution above
% 8.58/2.17 % (1761072)------------------------------
% 8.58/2.17 % (1761072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.58/2.17 % (1761072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.58/2.17 % (1761072)CaDiCaL version: 2.1.3
% 8.58/2.17 % (1761072)Termination reason: Refutation
% 8.58/2.17 % (1761072)Time elapsed: 0.867 s
% 8.58/2.17 % (1761072)Peak memory usage: 140 MB
% 8.58/2.17 % (1761072)Instructions burned: 2495 (million)
% 8.58/2.17 % (1761072)------------------------------
% 8.58/2.17 % (1761072)------------------------------
% 8.58/2.17 % (1761065)Success in time 1.13 s
% 8.58/2.17 % Vampire exiting
%------------------------------------------------------------------------------