%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP055-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:25 AM UTC 2026
% Result : Unsatisfiable 9.82s 2.25s
% Output : Refutation 10.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 16
% Syntax : Number of formulae : 210 ( 195 unt; 14 def)
% Number of atoms : 230 ( 204 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 41 ( 21 ~; 17 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 18 ( 3 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 18 con; 0-2 aty)
% Number of variables : 470 ( 0 sgn 470 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X0,X2))) = X1,
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(f45,plain,
! [X2,X0,X1] : multiply(inverse(X2),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))) = inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X2))),
inference(superposition,[],[f1,f1]) ).
fof(f57,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X4,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),multiply(X2,X3)))),multiply(X4,X1))) = multiply(inverse(X1),inverse(multiply(X0,multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))))),
inference(superposition,[],[f45,f1]) ).
fof(f65,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(X2,multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))))))))),multiply(X2,X1))) = multiply(inverse(X1),X0),
inference(superposition,[],[f45,f1]) ).
fof(f66,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X2))),
inference(superposition,[],[f45,f45]) ).
fof(f74,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X1,
inference(superposition,[],[f1,f45]) ).
fof(f145,plain,
! [X2,X3,X0,X1] : multiply(inverse(X2),X1) = inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(inverse(X2),X2))))))),multiply(X3,X2))),
inference(superposition,[],[f1,f66]) ).
fof(f153,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X4,X1)),multiply(X4,X2)) = inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),multiply(inverse(X5),inverse(multiply(inverse(X5),X5))))))),multiply(X3,X5))),
inference(superposition,[],[f1,f66]) ).
fof(f154,plain,
! [X2,X0,X1,X4] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X4,X1)),multiply(X4,X2)),
inference(forward_demodulation,[],[f153,f1]) ).
fof(f195,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,X4)) = multiply(X0,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),X4)),
inference(superposition,[],[f154,f1]) ).
fof(f331,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X3)),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X1,inverse(multiply(inverse(inverse(X3)),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))))))))),multiply(X4,multiply(X1,inverse(multiply(inverse(inverse(X3)),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))))) = X3,
inference(superposition,[],[f1,f195]) ).
fof(f332,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X3)),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X1,X2)) = X3,
inference(forward_demodulation,[],[f331,f145]) ).
fof(f340,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X3,inverse(multiply(inverse(inverse(X4)),multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),multiply(inverse(multiply(X5,X1)),multiply(X5,X2))))))))),multiply(X3,multiply(inverse(multiply(X5,X1)),multiply(X5,X2)))) = X4,
inference(superposition,[],[f332,f66]) ).
fof(f374,plain,
! [X2,X3,X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,X3))),
inference(superposition,[],[f195,f332]) ).
fof(f430,plain,
! [X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(X0),X0),
inference(superposition,[],[f374,f374]) ).
fof(f509,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X3),X3) = multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),multiply(inverse(multiply(X4,X1)),multiply(X4,X2))),
inference(superposition,[],[f430,f66]) ).
fof(f542,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(multiply(inverse(X2),X2)))))),X2))) = X1,
inference(superposition,[],[f1,f430]) ).
fof(f545,plain,
! [X2,X0,X1] : multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))) = inverse(multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(X0),X0))),
inference(superposition,[],[f45,f430]) ).
fof(f546,plain,
! [X2,X0,X1] : multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))))) = inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X2),X1))),
inference(superposition,[],[f45,f430]) ).
fof(f549,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3))) = inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X2),X3))),
inference(superposition,[],[f66,f430]) ).
fof(f553,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,[],[f154,f430]) ).
fof(f554,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,[],[f154,f430]) ).
fof(f567,plain,
! [X2,X0,X1] : multiply(inverse(X2),inverse(multiply(inverse(X2),X2))) = inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))),multiply(X1,X2))),
inference(superposition,[],[f1,f430]) ).
fof(f569,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))) = multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X0),X0)))))),
inference(superposition,[],[f45,f430]) ).
fof(f577,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,inverse(multiply(inverse(X4),multiply(inverse(X3),inverse(multiply(inverse(X3),X3)))))))) = multiply(X4,multiply(inverse(X0),X0)),
inference(superposition,[],[f195,f430]) ).
fof(f578,plain,
! [X0] : sF1 = multiply(inverse(X0),X0),
inference(superposition,[],[f40,f430]) ).
fof(f579,plain,
! [X0] : sF3 = multiply(inverse(X0),X0),
inference(superposition,[],[f41,f430]) ).
fof(f580,plain,
! [X0] : sF5 = multiply(inverse(X0),X0),
inference(superposition,[],[f42,f430]) ).
fof(f585,plain,
! [X2,X0,X1] : multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))) = inverse(multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(X0),X0))),
inference(superposition,[],[f45,f430]) ).
fof(f631,plain,
! [X2,X0,X1] : multiply(inverse(X1),X0) = inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),X0)),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))),multiply(X2,X1))),
inference(backward_demodulation,[],[f65,f585]) ).
fof(f645,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X4,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),multiply(X2,X3)))),multiply(X4,X1))) = multiply(inverse(X1),inverse(multiply(X0,multiply(inverse(inverse(sF5)),inverse(multiply(inverse(inverse(sF5)),inverse(sF5))))))),
inference(backward_demodulation,[],[f57,f580]) ).
fof(f647,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),multiply(inverse(X2),inverse(sF5)))) = X1,
inference(backward_demodulation,[],[f74,f580]) ).
fof(f761,plain,
sF1 = sF5,
inference(backward_demodulation,[],[f40,f580]) ).
fof(f762,plain,
sF3 = sF5,
inference(backward_demodulation,[],[f41,f580]) ).
fof(f779,plain,
sF1 = sF3,
inference(backward_demodulation,[],[f579,f578]) ).
fof(f780,plain,
! [X2,X3,X1,X4] : multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,inverse(multiply(inverse(X4),multiply(inverse(X3),inverse(multiply(inverse(X3),X3)))))))) = multiply(X4,sF1),
inference(forward_demodulation,[],[f577,f578]) ).
fof(f788,plain,
! [X2,X3,X1] : inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))) = multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(sF1))))),
inference(forward_demodulation,[],[f569,f578]) ).
fof(f790,plain,
! [X2,X1] : multiply(inverse(X2),inverse(multiply(inverse(X2),X2))) = inverse(multiply(inverse(multiply(X1,inverse(sF1))),multiply(X1,X2))),
inference(forward_demodulation,[],[f567,f578]) ).
fof(f803,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(inverse(X3),X2)),sF1),
inference(forward_demodulation,[],[f554,f578]) ).
fof(f804,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(sF1),multiply(inverse(X2),X3)),
inference(forward_demodulation,[],[f553,f578]) ).
fof(f808,plain,
! [X2,X3,X1] : inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3))) = inverse(multiply(inverse(sF1),multiply(inverse(X2),X3))),
inference(forward_demodulation,[],[f549,f578]) ).
fof(f811,plain,
! [X2,X1] : multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))))) = inverse(multiply(inverse(sF1),multiply(inverse(X2),X1))),
inference(forward_demodulation,[],[f546,f578]) ).
fof(f812,plain,
! [X2,X1] : inverse(multiply(inverse(multiply(inverse(X1),X2)),sF1)) = multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(sF1)),inverse(multiply(inverse(inverse(sF1)),inverse(sF1))))))),
inference(forward_demodulation,[],[f545,f578]) ).
fof(f815,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(sF1))))),X2))) = X1,
inference(forward_demodulation,[],[f542,f578]) ).
fof(f846,plain,
! [X2,X0,X1,X4] : sF1 = multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),multiply(inverse(multiply(X4,X1)),multiply(X4,X2))),
inference(forward_demodulation,[],[f509,f578]) ).
fof(f870,plain,
! [X2,X0,X1] : multiply(inverse(X1),X0) = inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),X0)),sF1)))),multiply(X2,X1))),
inference(forward_demodulation,[],[f631,f578]) ).
fof(f894,plain,
sF6 = multiply(sF3,a2),
inference(backward_demodulation,[],[f17,f762]) ).
fof(f1038,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),multiply(inverse(X2),inverse(sF1)))) = X1,
inference(forward_demodulation,[],[f647,f761]) ).
fof(f1040,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X4,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),multiply(X2,X3)))),multiply(X4,X1))) = multiply(inverse(X1),inverse(multiply(X0,multiply(inverse(inverse(sF5)),inverse(sF1))))),
inference(forward_demodulation,[],[f645,f578]) ).
fof(f1045,plain,
spl11_3,
inference(avatar_split_clause,[],[f779,f36]) ).
fof(f1046,plain,
! [X2,X3,X1,X4] : multiply(X4,sF1) = multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,inverse(multiply(inverse(X4),multiply(inverse(X3),inverse(sF1))))))),
inference(forward_demodulation,[],[f780,f578]) ).
fof(f1049,plain,
! [X2,X3,X1] : inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))) = multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(sF1)),inverse(sF1))))),
inference(forward_demodulation,[],[f788,f578]) ).
fof(f1051,plain,
! [X2,X1] : inverse(multiply(inverse(multiply(X1,inverse(sF1))),multiply(X1,X2))) = multiply(inverse(X2),inverse(sF1)),
inference(forward_demodulation,[],[f790,f578]) ).
fof(f1056,plain,
! [X2,X1] : multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(sF1))))) = inverse(multiply(inverse(sF1),multiply(inverse(X2),X1))),
inference(forward_demodulation,[],[f811,f578]) ).
fof(f1057,plain,
! [X2,X1] : inverse(multiply(inverse(multiply(inverse(X1),X2)),sF1)) = multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(sF1)),inverse(sF1))))),
inference(forward_demodulation,[],[f812,f578]) ).
fof(f1059,plain,
! [X2,X1] : inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(sF1))))),X2))) = X1,
inference(forward_demodulation,[],[f815,f578]) ).
fof(f1071,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X3,inverse(multiply(inverse(inverse(X4)),multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),inverse(sF1)))))),multiply(X3,multiply(inverse(multiply(X5,X1)),multiply(X5,X2)))) = X4,
inference(backward_demodulation,[],[f340,f846]) ).
fof(f1084,plain,
! [X2,X0,X1] : multiply(inverse(X1),X0) = inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(inverse(sF1)),X0)),sF1)))),multiply(X2,X1))),
inference(forward_demodulation,[],[f870,f578]) ).
fof(f1149,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X4,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),multiply(X2,X3)))),multiply(X4,X1))) = multiply(inverse(X1),inverse(multiply(X0,multiply(inverse(inverse(sF1)),inverse(sF1))))),
inference(forward_demodulation,[],[f1040,f761]) ).
fof(f1158,plain,
! [X2,X3,X1] : inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))) = multiply(inverse(X1),inverse(multiply(inverse(X2),sF1))),
inference(forward_demodulation,[],[f1049,f578]) ).
fof(f1177,plain,
! [X2,X1] : inverse(multiply(inverse(sF1),multiply(inverse(X2),X1))) = multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(sF1)),inverse(sF1))))),
inference(forward_demodulation,[],[f1056,f578]) ).
fof(f1178,plain,
! [X2,X1] : inverse(multiply(inverse(multiply(inverse(X1),X2)),sF1)) = multiply(inverse(X1),inverse(multiply(inverse(X2),sF1))),
inference(forward_demodulation,[],[f1057,f578]) ).
fof(f1232,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X4,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),multiply(X2,X3)))),multiply(X4,X1))) = multiply(inverse(X1),inverse(multiply(X0,sF1))),
inference(forward_demodulation,[],[f1149,f578]) ).
fof(f1242,plain,
! [X2,X1] : inverse(multiply(inverse(sF1),multiply(inverse(X2),X1))) = multiply(inverse(X1),inverse(multiply(inverse(X2),sF1))),
inference(forward_demodulation,[],[f1177,f578]) ).
fof(f1273,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),inverse(multiply(X0,sF1))) = inverse(multiply(inverse(multiply(X4,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(inverse(X3),inverse(sF1)))))),multiply(X2,X3)))),multiply(X4,X1))),
inference(forward_demodulation,[],[f1232,f578]) ).
fof(f1277,plain,
! [X2,X1] : inverse(multiply(inverse(multiply(inverse(X1),X2)),sF1)) = inverse(multiply(inverse(sF1),multiply(inverse(X2),X1))),
inference(backward_demodulation,[],[f1178,f1242]) ).
fof(f1293,plain,
! [X2,X0,X1] : multiply(inverse(X1),X0) = inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(sF1),multiply(inverse(X0),inverse(sF1)))))),multiply(X2,X1))),
inference(backward_demodulation,[],[f1084,f1277]) ).
fof(f1338,plain,
( sF6 = multiply(sF1,a2)
| ~ spl11_3 ),
inference(backward_demodulation,[],[f894,f37]) ).
fof(f1409,plain,
! [X0,X1] : multiply(inverse(sF1),multiply(inverse(X0),X1)) = multiply(inverse(multiply(inverse(X1),X0)),sF1),
inference(superposition,[],[f803,f578]) ).
fof(f1418,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(X2,X0)),X3)),sF1) = multiply(inverse(multiply(inverse(multiply(X2,X1)),X3)),multiply(inverse(multiply(inverse(X0),X1)),sF1)),
inference(superposition,[],[f803,f803]) ).
fof(f1430,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,multiply(X3,X0))),multiply(X2,multiply(X3,X1))) = multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),sF1)),sF1),
inference(superposition,[],[f803,f803]) ).
fof(f1472,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,multiply(X3,X0))),multiply(X2,multiply(X3,X1))) = multiply(inverse(multiply(inverse(sF1),multiply(inverse(X1),X0))),sF1),
inference(forward_demodulation,[],[f1430,f1277]) ).
fof(f1495,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(X2,X0)),X3)),sF1) = multiply(inverse(multiply(inverse(multiply(X2,X1)),X3)),multiply(inverse(sF1),multiply(inverse(X1),X0))),
inference(backward_demodulation,[],[f1418,f1409]) ).
fof(f1511,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,multiply(X3,X0))),multiply(X2,multiply(X3,X1))) = multiply(inverse(sF1),multiply(inverse(multiply(inverse(X1),X0)),sF1)),
inference(forward_demodulation,[],[f1472,f1409]) ).
fof(f1525,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(X2,X1)),X3)),multiply(inverse(sF1),multiply(inverse(X1),X0))) = multiply(inverse(sF1),multiply(inverse(X3),multiply(X2,X0))),
inference(forward_demodulation,[],[f1495,f1409]) ).
fof(f1526,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,multiply(X3,X0))),multiply(X2,multiply(X3,X1))) = multiply(inverse(sF1),multiply(inverse(sF1),multiply(inverse(X0),X1))),
inference(forward_demodulation,[],[f1511,f1409]) ).
fof(f1560,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X2,multiply(inverse(multiply(X3,X1)),multiply(X3,X0)))),multiply(X2,X4))) = multiply(inverse(X4),inverse(multiply(multiply(inverse(X0),inverse(multiply(inverse(X1),sF1))),sF1))),
inference(superposition,[],[f1158,f1158]) ).
fof(f1563,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X3,multiply(inverse(X2),X1))),multiply(X3,X4))) = multiply(inverse(X4),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),
inference(superposition,[],[f1158,f803]) ).
fof(f1575,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,X3)),multiply(X2,multiply(inverse(multiply(X4,X1)),multiply(X4,X0)))) = multiply(inverse(multiply(multiply(inverse(X0),inverse(multiply(inverse(X1),sF1))),X3)),sF1),
inference(superposition,[],[f803,f1158]) ).
fof(f1587,plain,
! [X2,X3,X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),multiply(inverse(X2),X3)) = multiply(inverse(multiply(inverse(X3),inverse(multiply(inverse(X1),sF1)))),sF1),
inference(superposition,[],[f803,f1158]) ).
fof(f1588,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))) = multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),sF1))),X3)),sF1),
inference(superposition,[],[f803,f1158]) ).
fof(f1589,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))) = multiply(inverse(sF1),multiply(inverse(X3),inverse(multiply(inverse(X1),sF1)))),
inference(forward_demodulation,[],[f1588,f1409]) ).
fof(f1590,plain,
! [X2,X3,X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),multiply(inverse(X2),X3)) = multiply(inverse(sF1),multiply(inverse(inverse(multiply(inverse(X1),sF1))),X3)),
inference(forward_demodulation,[],[f1587,f1409]) ).
fof(f1592,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,X3)),multiply(X2,multiply(inverse(multiply(X4,X1)),multiply(X4,X0)))) = multiply(inverse(multiply(inverse(multiply(inverse(sF1),multiply(inverse(X1),X0))),X3)),sF1),
inference(forward_demodulation,[],[f1575,f1242]) ).
fof(f1601,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X2,multiply(inverse(multiply(X3,X1)),multiply(X3,X0)))),multiply(X2,X4))) = multiply(inverse(X4),inverse(multiply(inverse(multiply(inverse(sF1),multiply(inverse(X1),X0))),sF1))),
inference(forward_demodulation,[],[f1560,f1242]) ).
fof(f1625,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))) = multiply(inverse(sF1),inverse(multiply(inverse(sF1),multiply(inverse(X1),X3)))),
inference(forward_demodulation,[],[f1589,f1242]) ).
fof(f1627,plain,
! [X1] : inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(inverse(X1),sF1))),inverse(sF1)))) = X1,
inference(backward_demodulation,[],[f1038,f1590]) ).
fof(f1631,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(sF1),multiply(inverse(X3),multiply(inverse(sF1),multiply(inverse(X1),X0)))) = multiply(inverse(multiply(X2,X3)),multiply(X2,multiply(inverse(multiply(X4,X1)),multiply(X4,X0)))),
inference(forward_demodulation,[],[f1592,f1409]) ).
fof(f1636,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X2,multiply(inverse(multiply(X3,X1)),multiply(X3,X0)))),multiply(X2,X4))) = inverse(multiply(inverse(sF1),multiply(inverse(multiply(inverse(sF1),multiply(inverse(X1),X0))),X4))),
inference(forward_demodulation,[],[f1601,f1242]) ).
fof(f1653,plain,
! [X0] : multiply(inverse(X0),inverse(sF1)) = inverse(multiply(inverse(sF1),multiply(inverse(inverse(sF1)),X0))),
inference(superposition,[],[f1051,f578]) ).
fof(f1655,plain,
! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(X1),sF1))),inverse(sF1)) = inverse(multiply(inverse(multiply(inverse(X2),inverse(sF1))),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))))),
inference(superposition,[],[f1051,f1158]) ).
fof(f1667,plain,
inverse(sF1) = multiply(inverse(inverse(sF1)),inverse(sF1)),
inference(superposition,[],[f1051,f578]) ).
fof(f1690,plain,
sF1 = inverse(sF1),
inference(forward_demodulation,[],[f1667,f578]) ).
fof(f1697,plain,
! [X1] : multiply(inverse(inverse(multiply(inverse(X1),sF1))),inverse(sF1)) = inverse(multiply(inverse(sF1),inverse(multiply(inverse(sF1),multiply(inverse(X1),inverse(sF1)))))),
inference(forward_demodulation,[],[f1655,f1625]) ).
fof(f1706,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(sF1,multiply(inverse(X2),X3)),
inference(backward_demodulation,[],[f804,f1690]) ).
fof(f1707,plain,
! [X2,X3,X1] : inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3))) = inverse(multiply(sF1,multiply(inverse(X2),X3))),
inference(backward_demodulation,[],[f808,f1690]) ).
fof(f1718,plain,
! [X2,X3,X1,X4] : multiply(X4,sF1) = multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,inverse(multiply(inverse(X4),multiply(inverse(X3),sF1)))))),
inference(backward_demodulation,[],[f1046,f1690]) ).
fof(f1723,plain,
! [X2,X1] : inverse(multiply(sF1,multiply(inverse(inverse(multiply(inverse(X1),multiply(inverse(X2),sF1)))),X2))) = X1,
inference(backward_demodulation,[],[f1059,f1690]) ).
fof(f1725,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X3,inverse(multiply(inverse(inverse(X4)),multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),sF1))))),multiply(X3,multiply(inverse(multiply(X5,X1)),multiply(X5,X2)))) = X4,
inference(backward_demodulation,[],[f1071,f1690]) ).
fof(f1755,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),inverse(multiply(X0,sF1))) = inverse(multiply(inverse(multiply(X4,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(inverse(X3),sF1))))),multiply(X2,X3)))),multiply(X4,X1))),
inference(backward_demodulation,[],[f1273,f1690]) ).
fof(f1758,plain,
! [X2,X0,X1] : multiply(inverse(X1),X0) = inverse(multiply(inverse(multiply(X2,inverse(multiply(sF1,multiply(inverse(X0),sF1))))),multiply(X2,X1))),
inference(backward_demodulation,[],[f1293,f1690]) ).
fof(f1773,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(X1),X0)),sF1) = multiply(sF1,multiply(inverse(X0),X1)),
inference(backward_demodulation,[],[f1409,f1690]) ).
fof(f1782,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(X2,X1)),X3)),multiply(sF1,multiply(inverse(X1),X0))) = multiply(sF1,multiply(inverse(X3),multiply(X2,X0))),
inference(backward_demodulation,[],[f1525,f1690]) ).
fof(f1783,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,multiply(X3,X0))),multiply(X2,multiply(X3,X1))) = multiply(sF1,multiply(sF1,multiply(inverse(X0),X1))),
inference(backward_demodulation,[],[f1526,f1690]) ).
fof(f1785,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))) = multiply(sF1,inverse(multiply(sF1,multiply(inverse(X1),X3)))),
inference(backward_demodulation,[],[f1625,f1690]) ).
fof(f1787,plain,
! [X1] : inverse(multiply(sF1,multiply(inverse(inverse(multiply(inverse(X1),sF1))),sF1))) = X1,
inference(backward_demodulation,[],[f1627,f1690]) ).
fof(f1789,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,X3)),multiply(X2,multiply(inverse(multiply(X4,X1)),multiply(X4,X0)))) = multiply(sF1,multiply(inverse(X3),multiply(sF1,multiply(inverse(X1),X0)))),
inference(backward_demodulation,[],[f1631,f1690]) ).
fof(f1790,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X2,multiply(inverse(multiply(X3,X1)),multiply(X3,X0)))),multiply(X2,X4))) = inverse(multiply(sF1,multiply(inverse(multiply(sF1,multiply(inverse(X1),X0))),X4))),
inference(backward_demodulation,[],[f1636,f1690]) ).
fof(f1795,plain,
! [X0] : multiply(inverse(X0),sF1) = inverse(multiply(sF1,multiply(inverse(sF1),X0))),
inference(backward_demodulation,[],[f1653,f1690]) ).
fof(f1810,plain,
! [X1] : multiply(inverse(inverse(multiply(inverse(X1),sF1))),sF1) = inverse(multiply(sF1,inverse(multiply(sF1,multiply(inverse(X1),sF1))))),
inference(forward_demodulation,[],[f1697,f1690]) ).
fof(f1814,plain,
! [X0] : multiply(inverse(X0),sF1) = inverse(multiply(sF1,multiply(sF1,X0))),
inference(forward_demodulation,[],[f1795,f1690]) ).
fof(f1840,plain,
! [X3,X0,X1] : multiply(inverse(X1),inverse(multiply(X0,sF1))) = inverse(multiply(sF1,multiply(inverse(multiply(sF1,multiply(inverse(inverse(multiply(inverse(X0),multiply(inverse(X3),sF1)))),X3))),X1))),
inference(forward_demodulation,[],[f1755,f1790]) ).
fof(f1850,plain,
! [X2,X0,X1,X4] : multiply(sF1,multiply(inverse(inverse(multiply(inverse(inverse(X4)),multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),sF1)))),multiply(sF1,multiply(inverse(X1),X2)))) = X4,
inference(forward_demodulation,[],[f1725,f1789]) ).
fof(f1852,plain,
! [X3,X4] : multiply(X4,sF1) = multiply(sF1,multiply(sF1,multiply(inverse(X3),inverse(multiply(inverse(X4),multiply(inverse(X3),sF1)))))),
inference(forward_demodulation,[],[f1718,f1783]) ).
fof(f1858,plain,
! [X2,X3,X1,X4] : inverse(multiply(inverse(multiply(X3,multiply(inverse(X2),X1))),multiply(X3,X4))) = multiply(inverse(X4),inverse(multiply(sF1,multiply(inverse(X1),X2)))),
inference(backward_demodulation,[],[f1563,f1707]) ).
fof(f1865,plain,
! [X2,X3,X1] : multiply(sF1,inverse(multiply(sF1,multiply(inverse(X1),X3)))) = multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(sF1,multiply(inverse(X1),X2)))),
inference(backward_demodulation,[],[f1785,f1707]) ).
fof(f1866,plain,
! [X0,X1] : multiply(inverse(X1),X0) = inverse(multiply(sF1,multiply(inverse(inverse(multiply(sF1,multiply(inverse(X0),sF1)))),X1))),
inference(backward_demodulation,[],[f1758,f1707]) ).
fof(f1926,plain,
! [X0,X1] : multiply(inverse(X1),inverse(multiply(X0,sF1))) = inverse(multiply(sF1,multiply(X0,X1))),
inference(forward_demodulation,[],[f1840,f1723]) ).
fof(f1931,plain,
! [X2,X0,X1,X4] : multiply(sF1,multiply(inverse(inverse(multiply(inverse(inverse(X4)),multiply(sF1,multiply(inverse(multiply(X0,X2)),multiply(X0,X1)))))),multiply(sF1,multiply(inverse(X1),X2)))) = X4,
inference(forward_demodulation,[],[f1850,f1773]) ).
fof(f1948,plain,
! [X2,X1,X4] : multiply(inverse(X4),inverse(multiply(sF1,multiply(inverse(X1),X2)))) = inverse(multiply(sF1,multiply(inverse(multiply(inverse(X2),X1)),X4))),
inference(forward_demodulation,[],[f1858,f1706]) ).
fof(f1967,plain,
! [X2,X1,X4] : multiply(sF1,multiply(inverse(inverse(multiply(inverse(inverse(X4)),multiply(sF1,multiply(sF1,multiply(inverse(X2),X1)))))),multiply(sF1,multiply(inverse(X1),X2)))) = X4,
inference(forward_demodulation,[],[f1931,f1706]) ).
fof(f1971,plain,
! [X2,X3,X1] : multiply(sF1,inverse(multiply(sF1,multiply(inverse(X1),X3)))) = inverse(multiply(sF1,multiply(inverse(multiply(inverse(X2),X1)),multiply(inverse(X2),X3)))),
inference(backward_demodulation,[],[f1865,f1948]) ).
fof(f1976,plain,
! [X3,X1] : multiply(sF1,inverse(multiply(sF1,multiply(inverse(X1),X3)))) = inverse(multiply(sF1,multiply(sF1,multiply(inverse(X1),X3)))),
inference(forward_demodulation,[],[f1971,f1706]) ).
fof(f1980,plain,
! [X3,X1] : multiply(sF1,inverse(multiply(sF1,multiply(inverse(X1),X3)))) = multiply(inverse(multiply(inverse(X1),X3)),sF1),
inference(forward_demodulation,[],[f1976,f1814]) ).
fof(f1982,plain,
! [X3,X1] : multiply(sF1,inverse(multiply(sF1,multiply(inverse(X1),X3)))) = multiply(sF1,multiply(inverse(X3),X1)),
inference(forward_demodulation,[],[f1980,f1773]) ).
fof(f1986,plain,
! [X1] : multiply(inverse(inverse(multiply(inverse(X1),sF1))),sF1) = inverse(multiply(sF1,multiply(inverse(sF1),X1))),
inference(backward_demodulation,[],[f1810,f1982]) ).
fof(f1987,plain,
! [X1] : multiply(inverse(inverse(multiply(inverse(X1),sF1))),sF1) = inverse(multiply(sF1,multiply(sF1,X1))),
inference(forward_demodulation,[],[f1986,f1690]) ).
fof(f1988,plain,
! [X1] : multiply(inverse(X1),sF1) = multiply(inverse(inverse(multiply(inverse(X1),sF1))),sF1),
inference(forward_demodulation,[],[f1987,f1814]) ).
fof(f1991,plain,
! [X1] : inverse(multiply(sF1,multiply(inverse(X1),sF1))) = X1,
inference(backward_demodulation,[],[f1787,f1988]) ).
fof(f1994,plain,
! [X0,X1] : multiply(inverse(X1),X0) = inverse(multiply(sF1,multiply(inverse(X0),X1))),
inference(backward_demodulation,[],[f1866,f1991]) ).
fof(f2005,plain,
! [X1] : multiply(inverse(sF1),X1) = X1,
inference(backward_demodulation,[],[f1991,f1994]) ).
fof(f2006,plain,
! [X2,X1] : multiply(inverse(X2),inverse(multiply(inverse(X1),multiply(inverse(X2),sF1)))) = X1,
inference(backward_demodulation,[],[f1723,f1994]) ).
fof(f2012,plain,
! [X4] : multiply(X4,sF1) = multiply(sF1,multiply(sF1,X4)),
inference(backward_demodulation,[],[f1852,f2006]) ).
fof(f2013,plain,
! [X1] : multiply(sF1,X1) = X1,
inference(forward_demodulation,[],[f2005,f1690]) ).
fof(f2022,plain,
! [X2,X1,X4] : multiply(sF1,multiply(inverse(inverse(multiply(inverse(inverse(X4)),multiply(multiply(inverse(X2),X1),sF1)))),multiply(sF1,multiply(inverse(X1),X2)))) = X4,
inference(backward_demodulation,[],[f1967,f2012]) ).
fof(f2023,plain,
! [X4] : multiply(X4,sF1) = multiply(sF1,X4),
inference(backward_demodulation,[],[f2012,f2013]) ).
fof(f2027,plain,
! [X2,X3,X1] : multiply(inverse(X2),X3) = multiply(inverse(multiply(X1,X2)),multiply(X1,X3)),
inference(backward_demodulation,[],[f1706,f2013]) ).
fof(f2029,plain,
! [X2,X3,X0,X1] : multiply(sF1,multiply(inverse(X3),multiply(X2,X0))) = multiply(inverse(multiply(inverse(multiply(X2,X1)),X3)),multiply(inverse(X1),X0)),
inference(backward_demodulation,[],[f1782,f2013]) ).
fof(f2030,plain,
! [X0,X1] : multiply(inverse(X1),X0) = inverse(multiply(inverse(X0),X1)),
inference(backward_demodulation,[],[f1994,f2013]) ).
fof(f2054,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = multiply(inverse(X1),inverse(multiply(X0,sF1))),
inference(backward_demodulation,[],[f1926,f2013]) ).
fof(f2055,plain,
( a2 = sF6
| ~ spl11_3 ),
inference(backward_demodulation,[],[f1338,f2013]) ).
fof(f2060,plain,
! [X2,X1,X4] : multiply(inverse(inverse(multiply(inverse(inverse(X4)),multiply(multiply(inverse(X2),X1),sF1)))),multiply(sF1,multiply(inverse(X1),X2))) = X4,
inference(forward_demodulation,[],[f2022,f2013]) ).
fof(f2067,plain,
( spl11_2
| ~ spl11_3 ),
inference(avatar_split_clause,[],[f2055,f36,f32]) ).
fof(f2083,plain,
! [X2,X3,X0,X1] : multiply(sF1,multiply(inverse(X3),multiply(X2,X0))) = multiply(multiply(inverse(X3),multiply(X2,X1)),multiply(inverse(X1),X0)),
inference(forward_demodulation,[],[f2029,f2030]) ).
fof(f2088,plain,
! [X4] : multiply(X4,sF1) = X4,
inference(forward_demodulation,[],[f2023,f2013]) ).
fof(f2092,plain,
! [X2,X1,X4] : multiply(inverse(inverse(multiply(inverse(inverse(X4)),multiply(multiply(inverse(X2),X1),sF1)))),multiply(inverse(X1),X2)) = X4,
inference(forward_demodulation,[],[f2060,f2013]) ).
fof(f2113,plain,
! [X2,X3,X0,X1] : multiply(inverse(X3),multiply(X2,X0)) = multiply(multiply(inverse(X3),multiply(X2,X1)),multiply(inverse(X1),X0)),
inference(forward_demodulation,[],[f2083,f2013]) ).
fof(f2116,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = multiply(inverse(X1),inverse(X0)),
inference(backward_demodulation,[],[f2054,f2088]) ).
fof(f2122,plain,
! [X2,X1,X4] : multiply(inverse(multiply(inverse(multiply(multiply(inverse(X2),X1),sF1)),inverse(X4))),multiply(inverse(X1),X2)) = X4,
inference(forward_demodulation,[],[f2092,f2030]) ).
fof(f2146,plain,
! [X2,X1,X4] : multiply(multiply(inverse(inverse(X4)),multiply(multiply(inverse(X2),X1),sF1)),multiply(inverse(X1),X2)) = X4,
inference(forward_demodulation,[],[f2122,f2030]) ).
fof(f2165,plain,
! [X2,X1,X4] : multiply(multiply(inverse(inverse(X4)),multiply(inverse(X2),X1)),multiply(inverse(X1),X2)) = X4,
inference(forward_demodulation,[],[f2146,f2088]) ).
fof(f2181,plain,
! [X2,X4] : multiply(inverse(inverse(X4)),multiply(inverse(X2),X2)) = X4,
inference(forward_demodulation,[],[f2165,f2113]) ).
fof(f2193,plain,
! [X4] : multiply(inverse(inverse(X4)),sF1) = X4,
inference(forward_demodulation,[],[f2181,f578]) ).
fof(f2203,plain,
! [X4] : inverse(inverse(X4)) = X4,
inference(forward_demodulation,[],[f2193,f2088]) ).
fof(f2239,plain,
! [X0,X1] : multiply(inverse(X1),sF1) = multiply(inverse(multiply(X0,X1)),X0),
inference(superposition,[],[f2027,f2088]) ).
fof(f2251,plain,
! [X0,X1] : inverse(X1) = multiply(inverse(multiply(X0,X1)),X0),
inference(forward_demodulation,[],[f2239,f2088]) ).
fof(f2300,plain,
! [X0,X1] : inverse(X1) = multiply(inverse(inverse(X0)),inverse(multiply(X1,X0))),
inference(superposition,[],[f2251,f2251]) ).
fof(f2317,plain,
! [X0,X1] : inverse(X1) = inverse(multiply(multiply(X1,X0),inverse(X0))),
inference(forward_demodulation,[],[f2300,f2116]) ).
fof(f2357,plain,
! [X0,X1] : multiply(X0,inverse(X1)) = inverse(multiply(X1,inverse(X0))),
inference(superposition,[],[f2116,f2203]) ).
fof(f2389,plain,
! [X0,X1] : inverse(X1) = multiply(X0,inverse(multiply(X1,X0))),
inference(backward_demodulation,[],[f2317,f2357]) ).
fof(f2421,plain,
! [X2,X0,X1] : multiply(inverse(inverse(multiply(X0,X1))),X2) = multiply(inverse(inverse(X0)),multiply(X1,X2)),
inference(superposition,[],[f2027,f2389]) ).
fof(f2426,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(inverse(inverse(multiply(X0,X1))),X2),
inference(forward_demodulation,[],[f2421,f2203]) ).
fof(f2439,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X0,X1),X2),
inference(forward_demodulation,[],[f2426,f2203]) ).
fof(f2504,plain,
! [X0] : multiply(sF7,X0) = multiply(a3,multiply(b3,X0)),
inference(superposition,[],[f2439,f19]) ).
fof(f2560,plain,
multiply(sF7,c3) = multiply(a3,sF9),
inference(superposition,[],[f2504,f23]) ).
fof(f2577,plain,
multiply(sF7,c3) = sF10,
inference(forward_demodulation,[],[f2560,f25]) ).
fof(f2581,plain,
sF8 = sF10,
inference(forward_demodulation,[],[f2577,f21]) ).
fof(f2582,plain,
( $false
| spl11_1 ),
inference(forward_subsumption_resolution,[],[f2581,f30]) ).
fof(f2583,plain,
spl11_1,
inference(avatar_contradiction_clause,[],[f2582]) ).
cnf(s1,plain,
( ~ spl11_1
| ~ spl11_2
| ~ spl11_3 ),
inference(sat_conversion,[],[f39]) ).
cnf(s2,plain,
spl11_3,
inference(sat_conversion,[],[f1045]) ).
cnf(s8,plain,
( spl11_2
| ~ spl11_3 ),
inference(sat_conversion,[],[f2067]) ).
cnf(s9,plain,
spl11_1,
inference(sat_conversion,[],[f2583]) ).
cnf(s10,plain,
spl11_2,
inference(rat,[],[s8,s2]) ).
cnf(s11,plain,
$false,
inference(rat,[],[s1,s2,s10,s9]) ).
fof(f2584,plain,
$false,
inference(avatar_sat_refutation,[],[s11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP055-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 09:17:15 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.41 Running first-order theorem proving
% 0.14/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
% 9.82/2.25 % (1761502)Input is clausal, will run a generic CNF schedule.
% 9.82/2.25 % (1761511)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2381615786:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.82/2.25 % (1761507)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=3238079814:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.82/2.25 % (1761511)Instruction limit reached!
% 9.82/2.25 % (1761511)------------------------------
% 9.82/2.25 % (1761511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761511)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761511)Termination reason: Instruction limit
% 9.82/2.25 % (1761511)Termination phase: Saturation
% 9.82/2.25 % (1761511)Time elapsed: 0.038 s
% 9.82/2.25 % (1761511)Peak memory usage: 89 MB
% 9.82/2.25 % (1761511)Instructions burned: 115 (million)
% 9.82/2.25 % (1761513)dis-21_1_sil=8000:lcm=predicate:random_seed=3212808316: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)
% 9.82/2.25 % (1761513)Refutation not found, incomplete strategy
% 9.82/2.25 % (1761513)------------------------------
% 9.82/2.25 % (1761513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761513)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761513)Termination reason: Refutation not found, incomplete strategy
% 9.82/2.25 % (1761513)Time elapsed: 0.001 s
% 9.82/2.25 % (1761513)Peak memory usage: 88 MB
% 9.82/2.25 % (1761510)lrs+10_1_sil=8000:sp=occurrence:random_seed=3201796737:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.82/2.25 % (1761509)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1036336244:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.82/2.25 % (1761508)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2103264877:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.82/2.25 % (1761512)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3698750283:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.82/2.25 % (1761510)Instruction limit reached!
% 9.82/2.25 % (1761510)------------------------------
% 9.82/2.25 % (1761510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761510)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761510)Termination reason: Instruction limit
% 9.82/2.25 % (1761510)Termination phase: Saturation
% 9.82/2.25 % (1761510)Time elapsed: 0.063 s
% 9.82/2.25 % (1761510)Peak memory usage: 89 MB
% 9.82/2.25 % (1761510)Instructions burned: 107 (million)
% 9.82/2.25 % (1761517)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=2912406543:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.82/2.25 % (1761517)Refutation not found, incomplete strategy
% 9.82/2.25 % (1761517)------------------------------
% 9.82/2.25 % (1761517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761517)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761517)Termination reason: Refutation not found, incomplete strategy
% 9.82/2.25 % (1761517)Time elapsed: 0.0000 s
% 9.82/2.25 % (1761517)Peak memory usage: 88 MB
% 9.82/2.25 % (1761512)Instruction limit reached!
% 9.82/2.25 % (1761512)------------------------------
% 9.82/2.25 % (1761512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761512)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761512)Termination reason: Instruction limit
% 9.82/2.25 % (1761512)Termination phase: Saturation
% 9.82/2.25 % (1761512)Time elapsed: 0.094 s
% 9.82/2.25 % (1761512)Peak memory usage: 89 MB
% 9.82/2.25 % (1761512)Instructions burned: 180 (million)
% 9.82/2.25 % (1761522)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1627687237: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)
% 9.82/2.25 % (1761522)Refutation not found, incomplete strategy
% 9.82/2.25 % (1761522)------------------------------
% 9.82/2.25 % (1761522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761522)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761522)Termination reason: Refutation not found, incomplete strategy
% 9.82/2.25 % (1761522)Time elapsed: 0.001 s
% 9.82/2.25 % (1761522)Peak memory usage: 88 MB
% 9.82/2.25 % (1761517)------------------------------
% 9.82/2.25 % (1761517)------------------------------
% 9.82/2.25 % (1761513)------------------------------
% 9.82/2.25 % (1761513)------------------------------
% 9.82/2.25 % (1761524)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1504420639:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 9.82/2.25 % (1761524)Refutation not found, incomplete strategy
% 9.82/2.25 % (1761524)------------------------------
% 9.82/2.25 % (1761524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761524)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761524)Termination reason: Refutation not found, incomplete strategy
% 9.82/2.25 % (1761524)Time elapsed: 0.001 s
% 9.82/2.25 % (1761524)Peak memory usage: 88 MB
% 9.82/2.25 % (1761526)lrs+10_64_to=lpo:sil=8000:random_seed=2241137838:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 9.82/2.25 % (1761526)Instruction limit reached!
% 9.82/2.25 % (1761526)------------------------------
% 9.82/2.25 % (1761526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761526)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761526)Termination reason: Instruction limit
% 9.82/2.25 % (1761526)Termination phase: Saturation
% 9.82/2.25 % (1761526)Time elapsed: 0.039 s
% 9.82/2.25 % (1761526)Peak memory usage: 89 MB
% 9.82/2.25 % (1761526)Instructions burned: 126 (million)
% 9.82/2.25 % (1761527)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1919328299:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 9.82/2.25 % (1761522)------------------------------
% 9.82/2.25 % (1761522)------------------------------
% 9.82/2.25 % (1761531)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2796703086:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 9.82/2.25 % (1761527)Instruction limit reached!
% 9.82/2.25 % (1761527)------------------------------
% 9.82/2.25 % (1761527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761527)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761527)Termination reason: Instruction limit
% 9.82/2.25 % (1761527)Termination phase: Saturation
% 9.82/2.25 % (1761527)Time elapsed: 0.113 s
% 9.82/2.25 % (1761527)Peak memory usage: 90 MB
% 9.82/2.25 % (1761527)Instructions burned: 194 (million)
% 9.82/2.25 % (1761524)------------------------------
% 9.82/2.25 % (1761524)------------------------------
% 9.82/2.25 % (1761531)Instruction limit reached!
% 9.82/2.25 % (1761531)------------------------------
% 9.82/2.25 % (1761531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761531)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761531)Termination reason: Instruction limit
% 9.82/2.25 % (1761531)Termination phase: Saturation
% 9.82/2.25 % (1761531)Time elapsed: 0.048 s
% 9.82/2.25 % (1761531)Peak memory usage: 90 MB
% 9.82/2.25 % (1761531)Instructions burned: 157 (million)
% 9.82/2.25 % (1761532)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=426619213:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 9.82/2.25 % (1761536)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=55585512:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 9.82/2.25 % (1761534)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=3404436933:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 9.82/2.25 % (1761535)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1932466243:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 9.82/2.25 % (1761535)Refutation not found, incomplete strategy
% 9.82/2.25 % (1761535)------------------------------
% 9.82/2.25 % (1761535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761535)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761535)Termination reason: Refutation not found, incomplete strategy
% 9.82/2.25 % (1761535)Time elapsed: 0.001 s
% 9.82/2.25 % (1761535)Peak memory usage: 88 MB
% 9.82/2.25 % (1761534)Instruction limit reached!
% 9.82/2.25 % (1761534)------------------------------
% 9.82/2.25 % (1761534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761534)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761534)Termination reason: Instruction limit
% 9.82/2.25 % (1761534)Termination phase: Saturation
% 9.82/2.25 % (1761534)Time elapsed: 0.062 s
% 9.82/2.25 % (1761534)Peak memory usage: 89 MB
% 9.82/2.25 % (1761534)Instructions burned: 106 (million)
% 9.82/2.25 % (1761536)Instruction limit reached!
% 9.82/2.25 % (1761536)------------------------------
% 9.82/2.25 % (1761536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761536)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761536)Termination reason: Instruction limit
% 9.82/2.25 % (1761536)Termination phase: Saturation
% 9.82/2.25 % (1761536)Time elapsed: 0.067 s
% 9.82/2.25 % (1761536)Peak memory usage: 91 MB
% 9.82/2.25 % (1761536)Instructions burned: 242 (million)
% 9.82/2.25 % (1761541)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=37648151:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 9.82/2.25 % (1761542)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2926535144:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 9.82/2.25 % (1761535)------------------------------
% 9.82/2.25 % (1761535)------------------------------
% 9.82/2.25 % (1761542)Instruction limit reached!
% 9.82/2.25 % (1761542)------------------------------
% 9.82/2.25 % (1761542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761542)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761542)Termination reason: Instruction limit
% 9.82/2.25 % (1761542)Termination phase: Saturation
% 9.82/2.25 % (1761542)Time elapsed: 0.078 s
% 9.82/2.25 % (1761542)Peak memory usage: 89 MB
% 9.82/2.25 % (1761542)Instructions burned: 134 (million)
% 9.82/2.25 % (1761509)First to succeed.
% 9.82/2.25 % (1761509)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1761502"
% 9.82/2.25 % (1761545)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3506069979:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 9.82/2.25 % (1761546)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3787707054:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 9.82/2.25 % (1761546)Instruction limit reached!
% 9.82/2.25 % (1761546)------------------------------
% 9.82/2.25 % (1761546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/2.25 % (1761546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/2.25 % (1761546)CaDiCaL version: 2.1.3
% 9.82/2.25 % (1761546)Termination reason: Instruction limit
% 9.82/2.25 % (1761546)Termination phase: Saturation
% 9.82/2.25 % (1761546)Time elapsed: 0.107 s
% 9.82/2.25 % (1761546)Peak memory usage: 90 MB
% 9.82/2.25 % (1761546)Instructions burned: 191 (million)
% 9.82/2.25 % (1761508)Also succeeded, but the first one will report.
% 9.82/2.25 % (1761509)Refutation found. Thanks to Tanya!
% 9.82/2.25 % SZS status Unsatisfiable for theBenchmark
% 9.82/2.25 % SZS output start Proof for theBenchmark
% See solution above
% 10.44/2.44 % (1761509)------------------------------
% 10.44/2.44 % (1761509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.44/2.44 % (1761509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.44/2.44 % (1761509)CaDiCaL version: 2.1.3
% 10.44/2.44 % (1761509)Termination reason: Refutation
% 10.44/2.44 % (1761509)Time elapsed: 0.983 s
% 10.44/2.44 % (1761509)Peak memory usage: 133 MB
% 10.44/2.44 % (1761509)Instructions burned: 1561 (million)
% 10.44/2.44 % (1761509)------------------------------
% 10.44/2.44 % (1761509)------------------------------
% 10.44/2.44 % (1761502)Success in time 1.396 s
% 10.44/2.44 % Vampire exiting
%------------------------------------------------------------------------------