%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP419-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:13:57 AM UTC 2026
% Result : Unsatisfiable 16.98s 3.29s
% Output : Refutation 17.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 55
% Number of leaves : 5
% Syntax : Number of formulae : 171 ( 171 unt; 3 def)
% Number of atoms : 171 ( 170 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 20 ( 4 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 298 ( 298 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_2) ).
fof(f3,plain,
a2 != multiply(multiply(inverse(b2),b2),a2),
inference(reorient_equations,[],[f2]) ).
fof(f4,definition,
sF0 = inverse(b2),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f5,plain,
inverse(b2) = sF0,
inference(reorient_equations,[],[f4]) ).
fof(f6,definition,
sF1 = multiply(sF0,b2),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f7,plain,
multiply(sF0,b2) = sF1,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF2 = multiply(sF1,a2),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f9,plain,
multiply(sF1,a2) = sF2,
inference(reorient_equations,[],[f8]) ).
fof(f10,plain,
a2 != sF2,
inference(definition_folding,[],[f3,f9,f7,f5]) ).
fof(f13,plain,
! [X0] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),sF1)) = X0,
inference(superposition,[],[f1,f7]) ).
fof(f14,plain,
! [X0] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(multiply(sF0,b2)))))))),sF1)) = X0,
inference(forward_demodulation,[],[f13,f5]) ).
fof(f15,plain,
! [X0] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1))))))),sF1)) = X0,
inference(forward_demodulation,[],[f14,f7]) ).
fof(f16,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(superposition,[],[f15,f1]) ).
fof(f17,plain,
! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1))))))),sF1) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(superposition,[],[f15,f15]) ).
fof(f24,plain,
! [X0] : inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))) = X0,
inference(backward_demodulation,[],[f15,f17]) ).
fof(f29,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(superposition,[],[f16,f24]) ).
fof(f30,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(b2,inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(X0,inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),multiply(X0,X1)),
inference(superposition,[],[f16,f5]) ).
fof(f32,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(multiply(sF0,b2)))))))),multiply(X0,b2)),
inference(superposition,[],[f16,f5]) ).
fof(f37,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),multiply(X0,b2)),
inference(forward_demodulation,[],[f32,f7]) ).
fof(f39,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)) = inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(b2,inverse(sF1))))))),sF1))),
inference(forward_demodulation,[],[f29,f17]) ).
fof(f41,plain,
! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)),
inference(forward_demodulation,[],[f39,f24]) ).
fof(f43,plain,
inverse(multiply(inverse(multiply(sF0,inverse(multiply(b2,inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1),
inference(backward_demodulation,[],[f30,f41]) ).
fof(f44,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),multiply(X1,b2)),
inference(superposition,[],[f37,f24]) ).
fof(f48,plain,
! [X0,X1] : inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1),inverse(multiply(b2,inverse(sF1))))))),sF1))) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),multiply(X1,b2)),
inference(forward_demodulation,[],[f44,f17]) ).
fof(f49,plain,
! [X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),multiply(X1,b2)),
inference(forward_demodulation,[],[f48,f24]) ).
fof(f51,plain,
! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(multiply(X0,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))))))))),multiply(X2,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),
inference(superposition,[],[f41,f24]) ).
fof(f64,plain,
! [X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))),
inference(superposition,[],[f41,f17]) ).
fof(f67,plain,
b2 = inverse(multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(superposition,[],[f24,f43]) ).
fof(f85,plain,
! [X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X0)),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),
inference(superposition,[],[f64,f17]) ).
fof(f95,plain,
! [X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X0)),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X0),
inference(forward_demodulation,[],[f85,f24]) ).
fof(f113,plain,
! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X2,X1)),
inference(superposition,[],[f41,f95]) ).
fof(f117,plain,
! [X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),sF1) = multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X1,b2)),
inference(superposition,[],[f49,f95]) ).
fof(f127,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X2,X1)) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))),inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(forward_demodulation,[],[f113,f17]) ).
fof(f135,plain,
! [X0,X1] : multiply(inverse(multiply(sF0,inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))))),sF1) = multiply(inverse(multiply(X1,inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))))),multiply(X1,b2)),
inference(superposition,[],[f117,f17]) ).
fof(f148,plain,
! [X0,X1] : multiply(inverse(multiply(sF0,X0)),sF1) = multiply(inverse(multiply(X1,X0)),multiply(X1,b2)),
inference(forward_demodulation,[],[f135,f24]) ).
fof(f336,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(inverse(X0),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))),inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(X1,inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))))),multiply(X1,X2)),
inference(superposition,[],[f127,f17]) ).
fof(f342,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))),inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X2)),
inference(superposition,[],[f127,f64]) ).
fof(f398,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(inverse(X0),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))),inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(X1,X0)),multiply(X1,X2)),
inference(forward_demodulation,[],[f336,f24]) ).
fof(f429,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X3,X1)),multiply(X3,X2)),
inference(superposition,[],[f398,f398]) ).
fof(f432,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(inverse(multiply(X2,b2)),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))),inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(inverse(multiply(sF0,X0)),sF1)),multiply(inverse(multiply(X2,X0)),X1)),
inference(superposition,[],[f398,f148]) ).
fof(f436,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(inverse(multiply(X2,X3)),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))),inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),multiply(inverse(multiply(X2,inverse(multiply(X0,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),X1)),
inference(superposition,[],[f398,f41]) ).
fof(f451,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(inverse(X3),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))),inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3)),multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(superposition,[],[f398,f41]) ).
fof(f626,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X2)),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X3)),
inference(superposition,[],[f429,f95]) ).
fof(f627,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X1,X3)) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X3)),
inference(superposition,[],[f429,f64]) ).
fof(f631,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,sF1)),multiply(X1,X2)) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))),multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1))))))),X2)),
inference(superposition,[],[f429,f17]) ).
fof(f638,plain,
! [X0,X1] : multiply(inverse(multiply(X0,b2)),multiply(X0,X1)) = multiply(inverse(sF1),multiply(sF0,X1)),
inference(superposition,[],[f429,f7]) ).
fof(f723,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,sF1)),multiply(X1,X2)) = multiply(X0,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1))))))),X2)),
inference(forward_demodulation,[],[f631,f24]) ).
fof(f769,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(inverse(multiply(X2,X0)),inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))),inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(inverse(sF1),multiply(sF0,X0))),multiply(inverse(multiply(X2,b2)),X1)),
inference(superposition,[],[f398,f638]) ).
fof(f780,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),multiply(inverse(multiply(X2,inverse(multiply(X0,inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),X1)) = multiply(inverse(multiply(inverse(sF1),multiply(sF0,X3))),multiply(inverse(multiply(X2,b2)),X1)),
inference(backward_demodulation,[],[f436,f769]) ).
fof(f781,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(sF0,X0)),sF1)),multiply(inverse(multiply(X2,X0)),X1)) = multiply(inverse(multiply(inverse(sF1),multiply(sF0,b2))),multiply(inverse(multiply(X2,b2)),X1)),
inference(backward_demodulation,[],[f432,f769]) ).
fof(f793,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(sF0,X0)),sF1)),multiply(inverse(multiply(X2,X0)),X1)) = multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(X2,b2)),X1)),
inference(forward_demodulation,[],[f781,f7]) ).
fof(f796,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(multiply(inverse(sF1),multiply(sF0,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X2)),inverse(multiply(b2,inverse(sF1))))))),b2)),X3)),
inference(backward_demodulation,[],[f626,f780]) ).
fof(f797,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X1,X3)) = multiply(inverse(multiply(inverse(sF1),multiply(sF0,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),b2)),X3)),
inference(backward_demodulation,[],[f627,f780]) ).
fof(f798,plain,
! [X2,X1] : inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X1,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1))))))),inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(inverse(sF1),multiply(sF0,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),b2)),X2)),
inference(backward_demodulation,[],[f342,f780]) ).
fof(f837,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),X3)),multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(multiply(inverse(sF1),multiply(sF0,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X3)),inverse(multiply(b2,inverse(sF1))))))),b2)),multiply(X1,X2))),
inference(backward_demodulation,[],[f451,f798]) ).
fof(f945,plain,
! [X0,X1] : multiply(b2,multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),X0)) = multiply(X1,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),X0)),
inference(superposition,[],[f723,f67]) ).
fof(f958,plain,
! [X0,X1] : multiply(X1,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))),inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))),
inference(superposition,[],[f723,f17]) ).
fof(f976,plain,
! [X0,X1] : multiply(X0,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))) = multiply(inverse(multiply(X1,sF1)),multiply(X1,sF1)),
inference(superposition,[],[f723,f17]) ).
fof(f981,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,sF1)),multiply(X2,multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(multiply(sF0,inverse(multiply(inverse(X3),inverse(multiply(b2,inverse(sF1)))))))),inverse(multiply(b2,inverse(sF1))))))),X1))) = multiply(X3,multiply(inverse(multiply(X0,sF1)),multiply(X0,X1))),
inference(superposition,[],[f723,f723]) ).
fof(f1024,plain,
! [X0,X1] : multiply(X1,multiply(inverse(multiply(sF0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1))))))),sF1)) = multiply(X0,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))),
inference(forward_demodulation,[],[f958,f24]) ).
fof(f1055,plain,
! [X0] : multiply(X0,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))) = multiply(b2,multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(forward_demodulation,[],[f1024,f945]) ).
fof(f1081,plain,
! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(multiply(b2,multiply(inverse(multiply(sF0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),sF1))))))))),multiply(X2,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),
inference(backward_demodulation,[],[f51,f1055]) ).
fof(f1272,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(X1,b2)),X2)) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))),multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1))))))),X2)),
inference(superposition,[],[f793,f17]) ).
fof(f1275,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(X0,b2)),X1)) = multiply(b2,multiply(inverse(multiply(X0,inverse(multiply(sF0,inverse(multiply(b2,inverse(sF1))))))),X1)),
inference(superposition,[],[f793,f67]) ).
fof(f1428,plain,
! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(sF0,b2)),sF1))))))))),multiply(X2,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),
inference(backward_demodulation,[],[f1081,f1275]) ).
fof(f1440,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(X1,b2)),X2)) = multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1))))))),X2)),
inference(forward_demodulation,[],[f1272,f24]) ).
fof(f1474,plain,
! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(sF1),sF1))))))))),multiply(X2,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),
inference(forward_demodulation,[],[f1428,f7]) ).
fof(f1542,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,X3)),multiply(X2,multiply(inverse(multiply(X0,inverse(multiply(inverse(X4),inverse(multiply(b2,inverse(sF1))))))),X1))) = multiply(inverse(multiply(X4,X3)),multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(X0,b2)),X1))),
inference(superposition,[],[f429,f1440]) ).
fof(f1565,plain,
! [X3,X0,X1] : multiply(X3,multiply(inverse(multiply(X0,sF1)),multiply(X0,X1))) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X3),inverse(multiply(b2,inverse(sF1))))))),sF1)),multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(sF0,b2)),X1))),
inference(backward_demodulation,[],[f981,f1542]) ).
fof(f1592,plain,
! [X3,X0,X1] : multiply(X3,multiply(inverse(multiply(X0,sF1)),multiply(X0,X1))) = multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X3),inverse(multiply(b2,inverse(sF1))))))),sF1)),multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(sF1),X1))),
inference(forward_demodulation,[],[f1565,f7]) ).
fof(f1603,plain,
! [X3,X0,X1] : multiply(X3,multiply(inverse(multiply(X0,sF1)),multiply(X0,X1))) = multiply(inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X3,inverse(multiply(b2,inverse(sF1))))))),sF1))),multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(sF1),X1))),
inference(forward_demodulation,[],[f1592,f17]) ).
fof(f1604,plain,
! [X3,X0,X1] : multiply(X3,multiply(inverse(multiply(X0,sF1)),multiply(X0,X1))) = multiply(X3,multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(sF1),X1))),
inference(forward_demodulation,[],[f1603,f24]) ).
fof(f1606,plain,
! [X2,X0,X1] : multiply(X1,multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(sF1),X2))) = multiply(X1,multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X2))),
inference(superposition,[],[f1604,f95]) ).
fof(f1654,plain,
! [X2,X3,X0,X1] : multiply(X0,multiply(inverse(multiply(X1,sF1)),multiply(X1,X2))) = multiply(X0,multiply(inverse(multiply(X3,sF1)),multiply(X3,X2))),
inference(superposition,[],[f1604,f1604]) ).
fof(f1764,plain,
! [X2,X1] : multiply(X1,multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(sF1),X2))) = multiply(X1,multiply(inverse(multiply(inverse(sF1),multiply(sF0,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1))))))),b2)),X2))),
inference(forward_demodulation,[],[f1606,f780]) ).
fof(f1837,plain,
! [X2,X3,X0,X1] : multiply(X1,multiply(inverse(multiply(X2,sF1)),multiply(X2,X3))) = multiply(X1,multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),X3))),
inference(superposition,[],[f1654,f95]) ).
fof(f1853,plain,
! [X2,X3,X0,X1] : multiply(X1,multiply(inverse(multiply(X2,sF1)),multiply(X2,X3))) = multiply(X1,multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X3)),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(X0,inverse(multiply(sF1,inverse(multiply(inverse(sF1),sF1)))))))),sF1)),multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1))),
inference(superposition,[],[f1654,f95]) ).
fof(f1992,plain,
! [X2,X3,X1] : multiply(X1,multiply(inverse(multiply(X2,sF1)),multiply(X2,X3))) = multiply(X1,multiply(inverse(multiply(inverse(sF1),multiply(sF0,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1))))))),b2)),multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X3)),inverse(multiply(b2,inverse(sF1))))))),sF1)))),
inference(forward_demodulation,[],[f1853,f837]) ).
fof(f2002,plain,
! [X2,X3,X1] : multiply(X1,multiply(inverse(multiply(X2,sF1)),multiply(X2,X3))) = multiply(X1,multiply(inverse(multiply(inverse(sF1),multiply(sF0,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1))))))),b2)),X3))),
inference(forward_demodulation,[],[f1837,f780]) ).
fof(f2047,plain,
! [X2,X3,X1] : multiply(X1,multiply(inverse(multiply(X2,sF1)),multiply(X2,X3))) = multiply(X1,multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(sF1),multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(X3)),inverse(multiply(b2,inverse(sF1))))))),sF1)))),
inference(forward_demodulation,[],[f1992,f1764]) ).
fof(f2070,plain,
! [X2,X3,X1] : multiply(X1,multiply(inverse(multiply(X2,sF1)),multiply(X2,X3))) = multiply(X1,multiply(inverse(multiply(inverse(X3),sF1)),multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(sF0,b2)),sF1)))),
inference(forward_demodulation,[],[f2047,f1542]) ).
fof(f2077,plain,
! [X2,X3,X1] : multiply(X1,multiply(inverse(multiply(X2,sF1)),multiply(X2,X3))) = multiply(X1,multiply(inverse(multiply(inverse(X3),sF1)),multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(sF1),sF1)))),
inference(forward_demodulation,[],[f2070,f7]) ).
fof(f3831,plain,
! [X0,X1] : multiply(inverse(multiply(X1,sF1)),multiply(X1,sF1)) = multiply(inverse(X0),inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),
inference(superposition,[],[f976,f17]) ).
fof(f3833,plain,
! [X0] : multiply(sF0,b2) = multiply(inverse(multiply(X0,sF1)),multiply(X0,sF1)),
inference(superposition,[],[f976,f67]) ).
fof(f3856,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X3,inverse(multiply(b2,inverse(sF1))))))),sF1)))) = multiply(inverse(multiply(X3,X2)),multiply(inverse(multiply(X0,sF1)),multiply(X0,sF1))),
inference(superposition,[],[f429,f976]) ).
fof(f3857,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X1,X3)) = multiply(inverse(multiply(inverse(multiply(X0,sF1)),multiply(X0,sF1))),multiply(X2,X3)),
inference(superposition,[],[f429,f976]) ).
fof(f3879,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(X1,b2)),inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),inverse(multiply(b2,inverse(sF1))))))),sF1)))) = multiply(X2,multiply(inverse(multiply(X0,sF1)),multiply(X0,sF1))),
inference(superposition,[],[f1440,f976]) ).
fof(f3942,plain,
! [X2,X0,X1] : multiply(X2,multiply(inverse(multiply(X0,sF1)),multiply(X0,sF1))) = multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(X1,b2)),inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1)))))),inverse(multiply(b2,inverse(sF1))))))),sF1))))),
inference(forward_demodulation,[],[f3879,f17]) ).
fof(f3964,plain,
! [X0] : sF1 = multiply(inverse(multiply(X0,sF1)),multiply(X0,sF1)),
inference(forward_demodulation,[],[f3833,f7]) ).
fof(f3966,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,sF1)),multiply(X1,sF1)),
inference(forward_demodulation,[],[f3831,f24]) ).
fof(f3975,plain,
! [X2,X0,X1] : multiply(X2,multiply(inverse(multiply(X0,sF1)),multiply(X0,sF1))) = multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(multiply(X1,b2)),multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1)))))))),
inference(forward_demodulation,[],[f3942,f24]) ).
fof(f3996,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X3,inverse(multiply(b2,inverse(sF1))))))),sF1)))) = multiply(inverse(multiply(X3,X2)),sF1),
inference(backward_demodulation,[],[f3856,f3964]) ).
fof(f3997,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1))))))),sF1)))),multiply(X1,X3)) = multiply(inverse(sF1),multiply(X2,X3)),
inference(backward_demodulation,[],[f3857,f3964]) ).
fof(f4019,plain,
! [X2,X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(sF1))))))),multiply(X2,inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)))),
inference(backward_demodulation,[],[f1474,f3964]) ).
fof(f4022,plain,
! [X2,X3,X1] : multiply(X1,multiply(inverse(multiply(X2,sF1)),multiply(X2,X3))) = multiply(X1,multiply(inverse(multiply(inverse(X3),sF1)),sF1)),
inference(backward_demodulation,[],[f2077,f3964]) ).
fof(f4035,plain,
! [X0] : sF1 = multiply(inverse(X0),X0),
inference(forward_demodulation,[],[f3966,f3964]) ).
fof(f4038,plain,
! [X2,X0] : multiply(X2,multiply(inverse(multiply(X0,sF1)),multiply(X0,sF1))) = multiply(inverse(multiply(inverse(sF1),sF1)),multiply(inverse(sF1),multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1)))))))),
inference(forward_demodulation,[],[f3975,f638]) ).
fof(f4134,plain,
! [X3,X1] : multiply(X1,multiply(inverse(multiply(inverse(sF1),multiply(sF0,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(sF1)),inverse(multiply(b2,inverse(sF1))))))),b2)),X3))) = multiply(X1,multiply(inverse(multiply(inverse(X3),sF1)),sF1)),
inference(backward_demodulation,[],[f2002,f4022]) ).
fof(f4184,plain,
! [X2,X3] : multiply(inverse(multiply(inverse(sF1),multiply(sF0,sF1))),multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1))))))),b2)),X3)) = multiply(inverse(sF1),multiply(X2,X3)),
inference(backward_demodulation,[],[f797,f3997]) ).
fof(f4206,plain,
! [X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(sF1))))))),sF1),
inference(backward_demodulation,[],[f4019,f3996]) ).
fof(f4512,plain,
! [X2,X0] : multiply(X2,multiply(inverse(multiply(X0,sF1)),multiply(X0,sF1))) = multiply(inverse(sF1),multiply(inverse(sF1),multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1)))))))),
inference(forward_demodulation,[],[f4038,f4035]) ).
fof(f4629,plain,
! [X3,X1] : multiply(X1,multiply(inverse(multiply(inverse(X3),sF1)),sF1)) = multiply(X1,multiply(inverse(sF1),multiply(inverse(sF1),X3))),
inference(backward_demodulation,[],[f4134,f4184]) ).
fof(f4636,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X3)) = multiply(inverse(sF1),multiply(inverse(X2),X3)),
inference(backward_demodulation,[],[f796,f4184]) ).
fof(f4832,plain,
! [X2] : multiply(inverse(sF1),multiply(inverse(sF1),multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1)))))))) = multiply(X2,multiply(inverse(multiply(inverse(sF1),sF1)),sF1)),
inference(forward_demodulation,[],[f4512,f4022]) ).
fof(f5122,plain,
! [X2] : multiply(inverse(sF1),multiply(inverse(sF1),multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1)))))))) = multiply(X2,multiply(inverse(sF1),multiply(inverse(sF1),sF1))),
inference(forward_demodulation,[],[f4832,f4629]) ).
fof(f5338,plain,
! [X2] : multiply(X2,multiply(inverse(sF1),sF1)) = multiply(inverse(sF1),multiply(inverse(sF1),multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1)))))))),
inference(forward_demodulation,[],[f5122,f4035]) ).
fof(f5431,plain,
! [X2] : multiply(X2,sF1) = multiply(inverse(sF1),multiply(inverse(sF1),multiply(sF0,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1)))))))),
inference(forward_demodulation,[],[f5338,f4035]) ).
fof(f5571,plain,
! [X0,X1] : multiply(inverse(sF1),multiply(inverse(X1),X0)) = multiply(inverse(multiply(inverse(X0),X1)),sF1),
inference(superposition,[],[f4636,f4035]) ).
fof(f6004,plain,
! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(sF1)))),inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X0,inverse(sF1))),sF1),
inference(superposition,[],[f4206,f4035]) ).
fof(f6027,plain,
! [X0] : multiply(inverse(multiply(X0,inverse(sF1))),sF1) = inverse(multiply(inverse(multiply(sF0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(sF1))),inverse(multiply(b2,inverse(sF1))))))),sF1)),
inference(forward_demodulation,[],[f6004,f17]) ).
fof(f6032,plain,
! [X0] : multiply(inverse(multiply(X0,inverse(sF1))),sF1) = inverse(inverse(multiply(inverse(multiply(sF0,inverse(multiply(multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(sF1)),inverse(multiply(b2,inverse(sF1))))))),sF1))),
inference(forward_demodulation,[],[f6027,f17]) ).
fof(f6035,plain,
! [X0] : multiply(inverse(multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1)),inverse(sF1)) = multiply(inverse(multiply(X0,inverse(sF1))),sF1),
inference(forward_demodulation,[],[f6032,f24]) ).
fof(f6039,plain,
! [X0,X1] : multiply(inverse(multiply(sF0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(inverse(multiply(X0,inverse(sF1))),sF1)))))),sF1),
inference(backward_demodulation,[],[f4206,f6035]) ).
fof(f6040,plain,
! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(multiply(inverse(inverse(sF1)),inverse(multiply(X0,inverse(multiply(inverse(sF1),sF1)))))),sF1),
inference(superposition,[],[f6039,f4035]) ).
fof(f6063,plain,
! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(multiply(inverse(sF1),sF1))))),inverse(sF1))),
inference(forward_demodulation,[],[f6040,f5571]) ).
fof(f6065,plain,
! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1))))))),sF1) = multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),inverse(sF1))),
inference(forward_demodulation,[],[f6063,f4035]) ).
fof(f6066,plain,
! [X0] : multiply(inverse(multiply(sF0,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1))))))),sF1) = inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),inverse(sF1)))),
inference(backward_demodulation,[],[f17,f6065]) ).
fof(f6067,plain,
! [X0] : inverse(inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),inverse(sF1))))) = X0,
inference(backward_demodulation,[],[f24,f6065]) ).
fof(f6112,plain,
! [X0] : multiply(inverse(multiply(X0,inverse(sF1))),sF1) = multiply(inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),inverse(sF1)))),inverse(sF1)),
inference(backward_demodulation,[],[f6035,f6065]) ).
fof(f6191,plain,
! [X0] : inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),inverse(sF1)))) = multiply(inverse(sF1),multiply(inverse(inverse(multiply(inverse(X0),inverse(sF1)))),inverse(sF1))),
inference(forward_demodulation,[],[f6066,f6065]) ).
fof(f6228,plain,
! [X0] : multiply(inverse(sF1),multiply(inverse(sF1),multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1)))))))) = multiply(inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),inverse(sF1)))),sF1),
inference(superposition,[],[f5431,f6067]) ).
fof(f6230,plain,
! [X0] : multiply(inverse(sF1),multiply(inverse(sF1),multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1)))))))) = multiply(inverse(sF1),multiply(inverse(multiply(inverse(inverse(multiply(X0,inverse(sF1)))),inverse(sF1))),sF1)),
inference(forward_demodulation,[],[f6228,f5571]) ).
fof(f6232,plain,
! [X0] : multiply(inverse(sF1),multiply(inverse(sF1),multiply(sF0,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1)))))))) = multiply(inverse(sF1),multiply(inverse(sF1),multiply(inverse(inverse(sF1)),inverse(multiply(X0,inverse(sF1)))))),
inference(forward_demodulation,[],[f6230,f5571]) ).
fof(f6234,plain,
! [X2] : multiply(X2,sF1) = multiply(inverse(sF1),multiply(inverse(sF1),multiply(inverse(inverse(sF1)),inverse(multiply(inverse(X2),inverse(sF1)))))),
inference(backward_demodulation,[],[f5431,f6232]) ).
fof(f6442,plain,
multiply(inverse(sF1),sF1) = multiply(inverse(multiply(inverse(sF1),multiply(inverse(inverse(sF1)),inverse(sF1)))),inverse(sF1)),
inference(superposition,[],[f6112,f4035]) ).
fof(f6443,plain,
! [X0] : multiply(inverse(multiply(inverse(X0),inverse(sF1))),sF1) = multiply(inverse(inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),inverse(sF1))))),inverse(sF1)),
inference(superposition,[],[f6112,f6191]) ).
fof(f6454,plain,
! [X0] : inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),inverse(sF1)))) = inverse(inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(sF1))),sF1))),inverse(sF1))))),
inference(superposition,[],[f6067,f6112]) ).
fof(f6485,plain,
! [X0] : multiply(X0,inverse(sF1)) = multiply(inverse(multiply(inverse(X0),inverse(sF1))),sF1),
inference(forward_demodulation,[],[f6443,f6067]) ).
fof(f6486,plain,
multiply(inverse(sF1),sF1) = multiply(inverse(multiply(inverse(sF1),sF1)),inverse(sF1)),
inference(forward_demodulation,[],[f6442,f4035]) ).
fof(f6493,plain,
! [X0] : multiply(X0,inverse(sF1)) = multiply(inverse(sF1),multiply(inverse(inverse(sF1)),X0)),
inference(forward_demodulation,[],[f6485,f5571]) ).
fof(f6494,plain,
sF1 = multiply(inverse(sF1),inverse(sF1)),
inference(forward_demodulation,[],[f6486,f4035]) ).
fof(f6507,plain,
! [X2] : multiply(X2,sF1) = multiply(inverse(sF1),multiply(inverse(multiply(inverse(X2),inverse(sF1))),inverse(sF1))),
inference(backward_demodulation,[],[f6234,f6493]) ).
fof(f6552,plain,
multiply(inverse(sF1),multiply(inverse(inverse(sF1)),inverse(sF1))) = inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(sF1,inverse(sF1)))),inverse(sF1)))),
inference(superposition,[],[f6191,f6494]) ).
fof(f6553,plain,
multiply(inverse(sF1),sF1) = multiply(inverse(sF1),multiply(inverse(inverse(sF1)),sF1)),
inference(superposition,[],[f5571,f6494]) ).
fof(f6557,plain,
inverse(sF1) = inverse(inverse(multiply(inverse(sF1),multiply(inverse(inverse(sF1)),inverse(sF1))))),
inference(superposition,[],[f6067,f6494]) ).
fof(f6560,plain,
! [X0] : multiply(inverse(sF1),multiply(inverse(X0),inverse(sF1))) = multiply(inverse(multiply(inverse(sF1),X0)),sF1),
inference(superposition,[],[f4636,f6494]) ).
fof(f6561,plain,
! [X0] : multiply(inverse(sF1),multiply(inverse(sF1),X0)) = multiply(inverse(sF1),multiply(inverse(inverse(sF1)),X0)),
inference(superposition,[],[f4636,f6494]) ).
fof(f6562,plain,
! [X0] : multiply(X0,inverse(sF1)) = multiply(inverse(sF1),multiply(inverse(sF1),X0)),
inference(forward_demodulation,[],[f6561,f6493]) ).
fof(f6563,plain,
! [X0] : multiply(inverse(sF1),multiply(inverse(X0),sF1)) = multiply(inverse(sF1),multiply(inverse(X0),inverse(sF1))),
inference(forward_demodulation,[],[f6560,f5571]) ).
fof(f6566,plain,
inverse(sF1) = inverse(inverse(multiply(inverse(sF1),inverse(sF1)))),
inference(forward_demodulation,[],[f6557,f6493]) ).
fof(f6570,plain,
multiply(inverse(sF1),sF1) = multiply(sF1,inverse(sF1)),
inference(forward_demodulation,[],[f6553,f6493]) ).
fof(f6571,plain,
multiply(inverse(sF1),inverse(sF1)) = inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(sF1,inverse(sF1)))),inverse(sF1)))),
inference(forward_demodulation,[],[f6552,f6493]) ).
fof(f6607,plain,
! [X0] : inverse(inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),sF1)))) = X0,
inference(backward_demodulation,[],[f6067,f6563]) ).
fof(f6646,plain,
! [X0] : multiply(inverse(sF1),multiply(inverse(inverse(multiply(inverse(X0),inverse(sF1)))),inverse(sF1))) = inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),sF1))),
inference(backward_demodulation,[],[f6191,f6563]) ).
fof(f6651,plain,
! [X0] : inverse(inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(sF1))),sF1))),inverse(sF1))))) = inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),sF1))),
inference(backward_demodulation,[],[f6454,f6563]) ).
fof(f6683,plain,
! [X2] : multiply(X2,sF1) = multiply(inverse(sF1),multiply(inverse(multiply(inverse(X2),inverse(sF1))),sF1)),
inference(backward_demodulation,[],[f6507,f6563]) ).
fof(f6687,plain,
inverse(sF1) = inverse(inverse(sF1)),
inference(forward_demodulation,[],[f6566,f6494]) ).
fof(f6691,plain,
sF1 = multiply(sF1,inverse(sF1)),
inference(forward_demodulation,[],[f6570,f4035]) ).
fof(f6692,plain,
multiply(inverse(sF1),inverse(sF1)) = inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(sF1,inverse(sF1)))),sF1))),
inference(forward_demodulation,[],[f6571,f6563]) ).
fof(f6716,plain,
! [X2] : multiply(X2,sF1) = multiply(inverse(sF1),multiply(inverse(sF1),multiply(inverse(inverse(sF1)),X2))),
inference(forward_demodulation,[],[f6683,f5571]) ).
fof(f6733,plain,
! [X0] : inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),sF1))) = inverse(inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(sF1))),sF1))),sF1)))),
inference(forward_demodulation,[],[f6651,f6563]) ).
fof(f6735,plain,
! [X0] : inverse(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,inverse(sF1)))),sF1))) = multiply(inverse(sF1),multiply(inverse(inverse(multiply(inverse(X0),inverse(sF1)))),sF1)),
inference(forward_demodulation,[],[f6646,f6563]) ).
fof(f6771,plain,
multiply(inverse(sF1),inverse(sF1)) = inverse(multiply(inverse(sF1),multiply(inverse(inverse(sF1)),sF1))),
inference(forward_demodulation,[],[f6692,f6691]) ).
fof(f6786,plain,
! [X2] : multiply(X2,sF1) = multiply(multiply(inverse(inverse(sF1)),X2),inverse(sF1)),
inference(forward_demodulation,[],[f6716,f6562]) ).
fof(f6804,plain,
inverse(multiply(inverse(sF1),multiply(inverse(sF1),sF1))) = multiply(inverse(sF1),inverse(sF1)),
inference(forward_demodulation,[],[f6771,f6687]) ).
fof(f6816,plain,
! [X2] : multiply(X2,sF1) = multiply(multiply(inverse(sF1),X2),inverse(sF1)),
inference(forward_demodulation,[],[f6786,f6687]) ).
fof(f6821,plain,
sF1 = inverse(multiply(inverse(sF1),multiply(inverse(sF1),sF1))),
inference(forward_demodulation,[],[f6804,f6494]) ).
fof(f6833,plain,
sF1 = inverse(multiply(sF1,inverse(sF1))),
inference(forward_demodulation,[],[f6821,f6562]) ).
fof(f6838,plain,
sF1 = inverse(sF1),
inference(forward_demodulation,[],[f6833,f6691]) ).
fof(f6940,plain,
! [X0] : inverse(inverse(multiply(sF1,multiply(inverse(inverse(multiply(X0,sF1))),sF1)))) = X0,
inference(backward_demodulation,[],[f6607,f6838]) ).
fof(f6998,plain,
! [X0] : inverse(multiply(sF1,multiply(inverse(inverse(multiply(X0,sF1))),sF1))) = inverse(inverse(multiply(sF1,multiply(inverse(inverse(multiply(inverse(multiply(X0,sF1)),sF1))),sF1)))),
inference(backward_demodulation,[],[f6733,f6838]) ).
fof(f7000,plain,
! [X0] : multiply(sF1,multiply(inverse(inverse(multiply(inverse(X0),sF1))),sF1)) = inverse(multiply(sF1,multiply(inverse(inverse(multiply(X0,sF1))),sF1))),
inference(backward_demodulation,[],[f6735,f6838]) ).
fof(f7049,plain,
! [X2] : multiply(X2,sF1) = multiply(multiply(sF1,X2),sF1),
inference(backward_demodulation,[],[f6816,f6838]) ).
fof(f7071,plain,
! [X0] : inverse(multiply(sF1,multiply(inverse(inverse(multiply(X0,sF1))),sF1))) = inverse(inverse(inverse(multiply(sF1,multiply(inverse(inverse(multiply(multiply(X0,sF1),sF1))),sF1))))),
inference(forward_demodulation,[],[f6998,f7000]) ).
fof(f7187,plain,
! [X0] : inverse(multiply(X0,sF1)) = inverse(multiply(sF1,multiply(inverse(inverse(multiply(X0,sF1))),sF1))),
inference(forward_demodulation,[],[f7071,f6940]) ).
fof(f7232,plain,
! [X0] : inverse(inverse(multiply(X0,sF1))) = X0,
inference(backward_demodulation,[],[f6940,f7187]) ).
fof(f7492,plain,
! [X0] : multiply(sF1,X0) = inverse(inverse(multiply(X0,sF1))),
inference(superposition,[],[f7232,f7049]) ).
fof(f7494,plain,
! [X0] : multiply(sF1,X0) = X0,
inference(forward_demodulation,[],[f7492,f7232]) ).
fof(f7617,plain,
a2 = sF2,
inference(backward_demodulation,[],[f9,f7494]) ).
fof(f7622,plain,
$false,
inference(forward_subsumption_resolution,[],[f7617,f10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP419-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n026.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 10:06:41 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.98/3.29 % (2592797)Detected a unit-equality problem, will run specialized UEQ schedule.
% 16.98/3.29 % (2592805)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1890186887:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 16.98/3.29 % (2592802)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=2698856853:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 16.98/3.29 % (2592808)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=373963213:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 16.98/3.29 % (2592804)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1405341819:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 16.98/3.29 % (2592803)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1290524668:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 16.98/3.29 % (2592806)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1692816693:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 16.98/3.29 % (2592807)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=128709870:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 16.98/3.29 % (2592805)Instruction limit reached!
% 16.98/3.29 % (2592805)------------------------------
% 16.98/3.29 % (2592805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/3.29 % (2592805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/3.29 % (2592805)CaDiCaL version: 2.1.3
% 16.98/3.29 % (2592805)Termination reason: Instruction limit
% 16.98/3.29 % (2592805)Termination phase: Saturation
% 16.98/3.29 % (2592805)Time elapsed: 0.039 s
% 16.98/3.29 % (2592805)Peak memory usage: 89 MB
% 16.98/3.29 % (2592805)Instructions burned: 137 (million)
% 16.98/3.29 % (2592806)Instruction limit reached!
% 16.98/3.29 % (2592806)------------------------------
% 16.98/3.29 % (2592806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/3.29 % (2592806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/3.29 % (2592806)CaDiCaL version: 2.1.3
% 16.98/3.29 % (2592806)Termination reason: Instruction limit
% 16.98/3.29 % (2592806)Termination phase: Saturation
% 16.98/3.29 % (2592806)Time elapsed: 0.095 s
% 16.98/3.29 % (2592806)Peak memory usage: 89 MB
% 16.98/3.29 % (2592806)Instructions burned: 182 (million)
% 16.98/3.29 % (2592816)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3849331182:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 16.98/3.29 % (2592807)Instruction limit reached!
% 16.98/3.29 % (2592807)------------------------------
% 16.98/3.29 % (2592807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/3.29 % (2592807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/3.29 % (2592807)CaDiCaL version: 2.1.3
% 16.98/3.29 % (2592807)Termination reason: Instruction limit
% 16.98/3.29 % (2592807)Termination phase: Saturation
% 16.98/3.29 % (2592807)Time elapsed: 0.136 s
% 16.98/3.29 % (2592807)Peak memory usage: 90 MB
% 16.98/3.29 % (2592807)Instructions burned: 259 (million)
% 16.98/3.29 % (2592817)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3767069305:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 16.98/3.29 % (2592819)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1859002558:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 16.98/3.29 % (2592819)Instruction limit reached!
% 16.98/3.29 % (2592819)------------------------------
% 16.98/3.29 % (2592819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/3.29 % (2592819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/3.29 % (2592819)CaDiCaL version: 2.1.3
% 16.98/3.29 % (2592819)Termination reason: Instruction limit
% 16.98/3.29 % (2592819)Termination phase: Saturation
% 16.98/3.29 % (2592819)Time elapsed: 0.129 s
% 16.98/3.29 % (2592819)Peak memory usage: 89 MB
% 16.98/3.29 % (2592819)Instructions burned: 216 (million)
% 16.98/3.29 % (2592822)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=2685173619:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 16.98/3.29 % (2592808)Instruction limit reached!
% 16.98/3.29 % (2592808)------------------------------
% 16.98/3.29 % (2592808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/3.29 % (2592808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/3.29 % (2592808)CaDiCaL version: 2.1.3
% 16.98/3.29 % (2592808)Termination reason: Instruction limit
% 16.98/3.29 % (2592808)Termination phase: Saturation
% 16.98/3.29 % (2592808)Time elapsed: 0.580 s
% 16.98/3.29 % (2592808)Peak memory usage: 93 MB
% 16.98/3.29 % (2592808)Instructions burned: 1187 (million)
% 16.98/3.29 % (2592822)Instruction limit reached!
% 16.98/3.29 % (2592822)------------------------------
% 16.98/3.29 % (2592822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/3.29 % (2592822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/3.29 % (2592822)CaDiCaL version: 2.1.3
% 16.98/3.29 % (2592822)Termination reason: Instruction limit
% 16.98/3.29 % (2592822)Termination phase: Saturation
% 16.98/3.29 % (2592822)Time elapsed: 0.160 s
% 16.98/3.29 % (2592822)Peak memory usage: 91 MB
% 16.98/3.29 % (2592822)Instructions burned: 318 (million)
% 16.98/3.29 % (2592824)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=3739554833:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 16.98/3.29 % (2592816)Instruction limit reached!
% 16.98/3.29 % (2592816)------------------------------
% 16.98/3.29 % (2592816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/3.29 % (2592816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/3.29 % (2592816)CaDiCaL version: 2.1.3
% 16.98/3.29 % (2592816)Termination reason: Instruction limit
% 16.98/3.29 % (2592816)Termination phase: Saturation
% 16.98/3.29 % (2592816)Time elapsed: 0.672 s
% 16.98/3.29 % (2592816)Peak memory usage: 139 MB
% 16.98/3.29 % (2592816)Instructions burned: 2054 (million)
% 16.98/3.29 % (2592825)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=848463160:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 16.98/3.29 % (2592827)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1907901169:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2990 on theBenchmark for (2990ds/14534Mi)
% 16.98/3.29 % (2592817)Instruction limit reached!
% 16.98/3.29 % (2592817)------------------------------
% 16.98/3.29 % (2592817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.98/3.29 % (2592817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.98/3.29 % (2592817)CaDiCaL version: 2.1.3
% 16.98/3.29 % (2592817)Termination reason: Instruction limit
% 16.98/3.29 % (2592817)Termination phase: Saturation
% 16.98/3.29 % (2592817)Time elapsed: 1.716 s
% 16.98/3.29 % (2592817)Peak memory usage: 165 MB
% 16.98/3.29 % (2592817)Instructions burned: 4949 (million)
% 16.98/3.29 % (2592804)First to succeed.
% 16.98/3.29 % (2592804)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2592797"
% 16.98/3.29 % (2592830)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1435776134:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2979 on theBenchmark for (2979ds/11832Mi)
% 16.98/3.29 % (2592824)Also succeeded, but the first one will report.
% 16.98/3.29 % (2592804)Refutation found. Thanks to Tanya!
% 16.98/3.29 % SZS status Unsatisfiable for theBenchmark
% 16.98/3.29 % SZS output start Proof for theBenchmark
% See solution above
% 17.77/3.49 % (2592804)------------------------------
% 17.77/3.49 % (2592804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.77/3.49 % (2592804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.77/3.49 % (2592804)CaDiCaL version: 2.1.3
% 17.77/3.49 % (2592804)Termination reason: Refutation
% 17.77/3.49 % (2592804)Time elapsed: 2.024 s
% 17.77/3.49 % (2592804)Peak memory usage: 143 MB
% 17.77/3.49 % (2592804)Instructions burned: 3366 (million)
% 17.77/3.49 % (2592804)------------------------------
% 17.77/3.49 % (2592804)------------------------------
% 17.77/3.49 % (2592797)Success in time 2.435 s
% 17.77/3.49 % Vampire exiting
%------------------------------------------------------------------------------