%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP109-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:36 AM UTC 2026
% Result : Unsatisfiable 5.73s 2.05s
% Output : Refutation 8.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 30
% Syntax : Number of formulae : 270 ( 253 unt; 27 def)
% Number of atoms : 299 ( 267 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 57 ( 28 ~; 25 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 32 con; 0-2 aty)
% Number of variables : 403 ( 0 sgn 403 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,inverse(double_divide(inverse(X1),double_divide(X0,X2))))),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,axiom,
! [X0,X1] : multiply(X0,X1) = inverse(double_divide(X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply) ).
fof(f3,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))
| multiply(a4,b4) != multiply(b4,a4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f4,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))
| multiply(a4,b4) != multiply(b4,a4) ),
inference(reorient_equations,[],[f3]) ).
fof(f5,plain,
( inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1)))
| a2 != inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2)))))
| inverse(double_divide(c3,inverse(double_divide(b3,a3)))) != inverse(double_divide(inverse(double_divide(c3,b3)),a3))
| inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4)) ),
inference(definition_unfolding,[],[f4,f2,f2,f2,f2,f2,f2,f2,f2,f2,f2]) ).
fof(f6,definition,
sF0 = inverse(a1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f7,plain,
inverse(a1) = sF0,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF1 = double_divide(a1,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f9,plain,
double_divide(a1,sF0) = sF1,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF2 = inverse(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f11,plain,
inverse(sF1) = sF2,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF3 = inverse(b1),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f13,plain,
inverse(b1) = sF3,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF4 = double_divide(b1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f15,plain,
double_divide(b1,sF3) = sF4,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF5 = inverse(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f17,plain,
inverse(sF4) = sF5,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF6 = inverse(b2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f19,plain,
inverse(b2) = sF6,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF7 = double_divide(b2,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f21,plain,
double_divide(b2,sF6) = sF7,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF8 = inverse(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f23,plain,
inverse(sF7) = sF8,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF9 = double_divide(a2,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f25,plain,
double_divide(a2,sF8) = sF9,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF10 = inverse(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f27,plain,
inverse(sF9) = sF10,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF11 = double_divide(b3,a3),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f29,plain,
double_divide(b3,a3) = sF11,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF12 = inverse(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f31,plain,
inverse(sF11) = sF12,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF13 = double_divide(c3,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f33,plain,
double_divide(c3,sF12) = sF13,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF14 = inverse(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f35,plain,
inverse(sF13) = sF14,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF15 = double_divide(c3,b3),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f37,plain,
double_divide(c3,b3) = sF15,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF16 = inverse(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f39,plain,
inverse(sF15) = sF16,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF17 = double_divide(sF16,a3),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f41,plain,
double_divide(sF16,a3) = sF17,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF18 = inverse(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f43,plain,
inverse(sF17) = sF18,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF19 = double_divide(b4,a4),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f45,plain,
double_divide(b4,a4) = sF19,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF20 = inverse(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f47,plain,
inverse(sF19) = sF20,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF21 = double_divide(a4,b4),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f49,plain,
double_divide(a4,b4) = sF21,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF22 = inverse(sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f51,plain,
inverse(sF21) = sF22,
inference(reorient_equations,[],[f50]) ).
fof(f52,plain,
( sF2 != sF5
| a2 != sF10
| sF14 != sF18
| sF20 != sF22 ),
inference(definition_folding,[],[f5,f51,f49,f47,f45,f43,f41,f39,f37,f35,f33,f31,f29,f27,f25,f23,f21,f19,f17,f15,f13,f11,f9,f7]) ).
fof(f54,definition,
( spl23_1
<=> sF20 = sF22 ),
introduced(definition,[new_symbols(definition,[spl23_1])],[avatar_definition]) ).
fof(f56,plain,
( sF20 != sF22
| spl23_1 ),
inference(avatar_component_clause,[],[f54]) ).
fof(f58,definition,
( spl23_2
<=> sF14 = sF18 ),
introduced(definition,[new_symbols(definition,[spl23_2])],[avatar_definition]) ).
fof(f60,plain,
( sF14 != sF18
| spl23_2 ),
inference(avatar_component_clause,[],[f58]) ).
fof(f62,definition,
( spl23_3
<=> a2 = sF10 ),
introduced(definition,[new_symbols(definition,[spl23_3])],[avatar_definition]) ).
fof(f66,definition,
( spl23_4
<=> sF2 = sF5 ),
introduced(definition,[new_symbols(definition,[spl23_4])],[avatar_definition]) ).
fof(f68,plain,
( sF2 != sF5
| spl23_4 ),
inference(avatar_component_clause,[],[f66]) ).
fof(f69,plain,
( ~ spl23_1
| ~ spl23_2
| ~ spl23_3
| ~ spl23_4 ),
inference(avatar_split_clause,[],[f52,f66,f62,f58,f54]) ).
fof(f70,plain,
double_divide(b1,inverse(b1)) = sF4,
inference(forward_demodulation,[],[f15,f13]) ).
fof(f71,plain,
double_divide(b2,inverse(b2)) = sF7,
inference(forward_demodulation,[],[f21,f19]) ).
fof(f72,plain,
inverse(double_divide(b3,a3)) = sF12,
inference(forward_demodulation,[],[f31,f29]) ).
fof(f73,plain,
inverse(double_divide(c3,b3)) = sF16,
inference(forward_demodulation,[],[f39,f37]) ).
fof(f74,plain,
inverse(double_divide(b4,a4)) = sF20,
inference(forward_demodulation,[],[f47,f45]) ).
fof(f75,plain,
inverse(double_divide(a4,b4)) = sF22,
inference(forward_demodulation,[],[f51,f49]) ).
fof(f79,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(inverse(double_divide(X1,inverse(double_divide(inverse(X0),double_divide(X1,X2))))),inverse(double_divide(inverse(X3),X0)))),X2) = X3,
inference(superposition,[],[f1,f1]) ).
fof(f80,plain,
! [X2,X3,X0,X1] : double_divide(X2,inverse(double_divide(inverse(X0),double_divide(X2,double_divide(X1,X3))))) = double_divide(inverse(double_divide(X1,inverse(X0))),X3),
inference(superposition,[],[f1,f1]) ).
fof(f159,plain,
! [X2,X0] : double_divide(inverse(X0),inverse(double_divide(inverse(X2),X0))) = X2,
inference(superposition,[],[f79,f1]) ).
fof(f196,plain,
! [X2,X0,X1] : double_divide(X2,inverse(double_divide(inverse(X0),double_divide(X2,X1)))) = double_divide(inverse(X1),inverse(X0)),
inference(superposition,[],[f159,f1]) ).
fof(f197,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X1),inverse(X0)) = double_divide(inverse(double_divide(X2,inverse(double_divide(inverse(X3),double_divide(X2,X1))))),inverse(double_divide(inverse(X0),X3))),
inference(superposition,[],[f159,f79]) ).
fof(f208,plain,
! [X2,X3] : double_divide(inverse(double_divide(inverse(X2),inverse(X3))),X2) = X3,
inference(backward_demodulation,[],[f79,f197]) ).
fof(f224,plain,
! [X3,X0,X1] : double_divide(inverse(double_divide(X1,inverse(X0))),X3) = double_divide(inverse(double_divide(X1,X3)),inverse(X0)),
inference(backward_demodulation,[],[f80,f196]) ).
fof(f288,plain,
! [X0,X1] : double_divide(inverse(X0),double_divide(inverse(inverse(X1)),inverse(X0))) = X1,
inference(superposition,[],[f208,f208]) ).
fof(f303,plain,
! [X2,X0,X1] : double_divide(inverse(X1),inverse(double_divide(inverse(X2),X0))) = double_divide(inverse(inverse(double_divide(inverse(X0),X1))),inverse(X2)),
inference(superposition,[],[f196,f159]) ).
fof(f310,plain,
! [X2,X0,X1] : double_divide(X1,inverse(X0)) = double_divide(inverse(X2),inverse(double_divide(inverse(double_divide(X1,X2)),inverse(X0)))),
inference(superposition,[],[f196,f208]) ).
fof(f311,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(inverse(X2),X0)) = double_divide(inverse(double_divide(inverse(X0),inverse(X1))),X2),
inference(superposition,[],[f208,f196]) ).
fof(f313,plain,
! [X2,X3] : double_divide(inverse(X3),double_divide(inverse(X2),X2)) = X3,
inference(backward_demodulation,[],[f208,f311]) ).
fof(f395,plain,
! [X0] : sF1 = double_divide(sF2,double_divide(inverse(X0),X0)),
inference(superposition,[],[f313,f11]) ).
fof(f400,plain,
! [X0] : sF17 = double_divide(sF18,double_divide(inverse(X0),X0)),
inference(superposition,[],[f313,f43]) ).
fof(f413,plain,
! [X0,X1] : double_divide(inverse(double_divide(inverse(X1),X1)),inverse(X0)) = X0,
inference(superposition,[],[f159,f313]) ).
fof(f499,plain,
! [X0,X1] : double_divide(inverse(X1),X1) = double_divide(inverse(inverse(X0)),inverse(X0)),
inference(superposition,[],[f159,f413]) ).
fof(f500,plain,
! [X2,X0,X1] : double_divide(inverse(X0),inverse(X2)) = double_divide(inverse(double_divide(inverse(double_divide(inverse(X1),X1)),inverse(X2))),inverse(X0)),
inference(superposition,[],[f224,f413]) ).
fof(f501,plain,
! [X2,X0,X1] : double_divide(inverse(inverse(X0)),inverse(X2)) = double_divide(inverse(double_divide(inverse(X1),X1)),inverse(double_divide(inverse(X2),X0))),
inference(superposition,[],[f196,f413]) ).
fof(f504,plain,
! [X2,X0] : double_divide(inverse(X2),X0) = double_divide(inverse(inverse(X0)),inverse(X2)),
inference(forward_demodulation,[],[f501,f413]) ).
fof(f505,plain,
! [X2,X0,X1] : double_divide(inverse(X0),inverse(X2)) = double_divide(inverse(X2),double_divide(inverse(inverse(X0)),double_divide(inverse(X1),X1))),
inference(forward_demodulation,[],[f500,f311]) ).
fof(f510,plain,
! [X0,X1] : double_divide(inverse(X0),double_divide(inverse(X0),X1)) = X1,
inference(backward_demodulation,[],[f288,f504]) ).
fof(f512,plain,
! [X0,X1] : double_divide(inverse(X0),X0) = double_divide(inverse(X1),X1),
inference(backward_demodulation,[],[f499,f504]) ).
fof(f513,plain,
! [X2,X0,X1] : double_divide(inverse(X1),inverse(double_divide(inverse(X2),X0))) = double_divide(inverse(X2),double_divide(inverse(X0),X1)),
inference(backward_demodulation,[],[f303,f504]) ).
fof(f516,plain,
! [X2,X0] : double_divide(inverse(X2),inverse(X0)) = double_divide(inverse(X0),inverse(X2)),
inference(forward_demodulation,[],[f505,f313]) ).
fof(f520,plain,
! [X2,X0,X1] : double_divide(X1,inverse(X0)) = double_divide(inverse(double_divide(X1,X2)),double_divide(inverse(inverse(X0)),X2)),
inference(backward_demodulation,[],[f310,f513]) ).
fof(f565,plain,
! [X0] : double_divide(inverse(X0),X0) = double_divide(sF2,sF1),
inference(superposition,[],[f512,f11]) ).
fof(f585,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(inverse(X1)),X2)),inverse(X1)) = double_divide(inverse(double_divide(inverse(X0),X0)),X2),
inference(superposition,[],[f224,f512]) ).
fof(f586,plain,
! [X2,X0,X1] : double_divide(inverse(X2),inverse(double_divide(X1,X2))) = double_divide(X1,inverse(double_divide(inverse(X0),X0))),
inference(superposition,[],[f196,f512]) ).
fof(f588,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X0),X0)),X2) = double_divide(inverse(X1),inverse(double_divide(inverse(inverse(X1)),X2))),
inference(forward_demodulation,[],[f585,f516]) ).
fof(f594,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X0),X0)),X2) = double_divide(inverse(inverse(X1)),double_divide(inverse(X2),X1)),
inference(forward_demodulation,[],[f588,f513]) ).
fof(f622,plain,
! [X0] : double_divide(sF10,inverse(X0)) = double_divide(inverse(X0),sF10),
inference(superposition,[],[f516,f27]) ).
fof(f641,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X1,inverse(X0))),X2) = double_divide(inverse(X0),inverse(double_divide(X1,X2))),
inference(superposition,[],[f224,f516]) ).
fof(f642,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X0),inverse(X1))),X2) = double_divide(inverse(double_divide(inverse(X1),X2)),inverse(X0)),
inference(superposition,[],[f224,f516]) ).
fof(f647,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X0),inverse(X1))),inverse(X2)) = double_divide(inverse(double_divide(inverse(X1),inverse(X2))),inverse(X0)),
inference(superposition,[],[f224,f516]) ).
fof(f649,plain,
! [X2,X0,X1] : double_divide(inverse(X0),inverse(double_divide(X1,inverse(X2)))) = double_divide(inverse(double_divide(X1,inverse(X0))),inverse(X2)),
inference(superposition,[],[f224,f516]) ).
fof(f651,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X0),inverse(X1))),inverse(X2)) = double_divide(inverse(X2),inverse(double_divide(inverse(X1),inverse(X0)))),
inference(forward_demodulation,[],[f647,f649]) ).
fof(f653,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(inverse(X2),X0)) = double_divide(inverse(double_divide(inverse(X1),X2)),inverse(X0)),
inference(forward_demodulation,[],[f642,f311]) ).
fof(f661,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(inverse(X2),X0)) = double_divide(inverse(X1),inverse(double_divide(inverse(X0),X2))),
inference(backward_demodulation,[],[f311,f641]) ).
fof(f685,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X0),inverse(X1))),inverse(X2)) = double_divide(inverse(X1),double_divide(inverse(inverse(X0)),X2)),
inference(forward_demodulation,[],[f651,f513]) ).
fof(f704,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(inverse(inverse(X0)),X2)) = double_divide(inverse(X1),inverse(double_divide(inverse(X0),inverse(X2)))),
inference(forward_demodulation,[],[f685,f641]) ).
fof(f718,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(inverse(inverse(X0)),X2)) = double_divide(inverse(X0),double_divide(inverse(inverse(X2)),X1)),
inference(forward_demodulation,[],[f704,f513]) ).
fof(f736,plain,
! [X0,X1] : inverse(X0) = double_divide(inverse(X1),double_divide(inverse(X0),inverse(X1))),
inference(superposition,[],[f510,f516]) ).
fof(f738,plain,
! [X2,X0,X1] : inverse(double_divide(inverse(X1),double_divide(inverse(X2),X0))) = double_divide(inverse(X2),double_divide(inverse(X0),inverse(X1))),
inference(superposition,[],[f510,f196]) ).
fof(f763,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X1),inverse(double_divide(inverse(double_divide(X0,X1)),inverse(X2)))) = double_divide(inverse(double_divide(X0,inverse(X2))),inverse(double_divide(inverse(X3),X3))),
inference(superposition,[],[f586,f224]) ).
fof(f767,plain,
! [X2,X0,X1] : double_divide(inverse(inverse(X0)),inverse(double_divide(inverse(X0),inverse(X1)))) = double_divide(inverse(X1),inverse(double_divide(inverse(X2),X2))),
inference(superposition,[],[f586,f516]) ).
fof(f776,plain,
! [X0] : double_divide(a2,inverse(double_divide(inverse(X0),X0))) = double_divide(inverse(sF8),inverse(sF9)),
inference(superposition,[],[f586,f25]) ).
fof(f788,plain,
! [X0,X1] : double_divide(inverse(X0),inverse(double_divide(X1,X0))) = double_divide(X1,inverse(double_divide(sF0,a1))),
inference(superposition,[],[f586,f7]) ).
fof(f811,plain,
! [X2,X0,X1] : inverse(double_divide(X0,X2)) = double_divide(inverse(X2),double_divide(X0,inverse(double_divide(inverse(X1),X1)))),
inference(superposition,[],[f510,f586]) ).
fof(f815,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X1,X3)),inverse(double_divide(inverse(X2),X2))) = double_divide(inverse(double_divide(inverse(X0),inverse(double_divide(X1,X0)))),X3),
inference(superposition,[],[f224,f586]) ).
fof(f823,plain,
! [X2,X3,X0,X1] : double_divide(inverse(inverse(double_divide(inverse(X3),X3))),inverse(X2)) = double_divide(X1,inverse(double_divide(inverse(X2),double_divide(inverse(X0),inverse(double_divide(X1,X0)))))),
inference(superposition,[],[f196,f586]) ).
fof(f828,plain,
! [X2,X3,X0,X1] : double_divide(inverse(inverse(double_divide(inverse(X3),X3))),inverse(X2)) = double_divide(X1,double_divide(inverse(X0),double_divide(inverse(inverse(double_divide(X1,X0))),inverse(X2)))),
inference(forward_demodulation,[],[f823,f738]) ).
fof(f836,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X1,X3)),inverse(double_divide(inverse(X2),X2))) = double_divide(inverse(double_divide(X1,X0)),inverse(double_divide(inverse(X0),X3))),
inference(forward_demodulation,[],[f815,f641]) ).
fof(f848,plain,
! [X0] : double_divide(a2,inverse(double_divide(inverse(X0),X0))) = double_divide(inverse(sF8),sF10),
inference(forward_demodulation,[],[f776,f27]) ).
fof(f857,plain,
! [X2,X0,X1] : double_divide(inverse(inverse(X0)),inverse(double_divide(inverse(X0),inverse(X1)))) = double_divide(inverse(X2),double_divide(inverse(X2),X1)),
inference(forward_demodulation,[],[f767,f513]) ).
fof(f861,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X1),inverse(double_divide(inverse(double_divide(X0,X1)),inverse(X2)))) = double_divide(inverse(X2),inverse(double_divide(X0,inverse(double_divide(inverse(X3),X3))))),
inference(forward_demodulation,[],[f763,f641]) ).
fof(f864,plain,
! [X2,X3,X0,X1] : double_divide(inverse(inverse(double_divide(inverse(X3),X3))),inverse(X2)) = double_divide(X1,double_divide(inverse(X0),double_divide(inverse(X2),double_divide(X1,X0)))),
inference(forward_demodulation,[],[f828,f504]) ).
fof(f872,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X1,X3)),inverse(double_divide(inverse(X2),X2))) = double_divide(inverse(X0),double_divide(inverse(X3),double_divide(X1,X0))),
inference(forward_demodulation,[],[f836,f513]) ).
fof(f884,plain,
! [X0] : double_divide(a2,inverse(double_divide(inverse(X0),X0))) = double_divide(sF10,inverse(sF8)),
inference(forward_demodulation,[],[f848,f622]) ).
fof(f892,plain,
! [X0,X1] : double_divide(inverse(inverse(X0)),inverse(double_divide(inverse(X0),inverse(X1)))) = X1,
inference(forward_demodulation,[],[f857,f510]) ).
fof(f896,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(inverse(inverse(X2)),X1)) = double_divide(inverse(X2),inverse(double_divide(X0,inverse(double_divide(inverse(X3),X3))))),
inference(forward_demodulation,[],[f861,f513]) ).
fof(f898,plain,
! [X2,X3,X0,X1] : double_divide(X1,double_divide(inverse(X0),double_divide(inverse(X2),double_divide(X1,X0)))) = double_divide(inverse(X2),double_divide(inverse(X3),X3)),
inference(forward_demodulation,[],[f864,f504]) ).
fof(f904,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X0),double_divide(inverse(X3),double_divide(X1,X0))) = double_divide(inverse(X2),double_divide(inverse(X2),double_divide(X1,X3))),
inference(forward_demodulation,[],[f872,f513]) ).
fof(f916,plain,
! [X0,X1] : double_divide(inverse(X0),double_divide(inverse(inverse(X1)),inverse(X0))) = X1,
inference(forward_demodulation,[],[f892,f513]) ).
fof(f919,plain,
! [X2,X3,X0] : double_divide(X0,inverse(X2)) = double_divide(inverse(X2),inverse(double_divide(X0,inverse(double_divide(inverse(X3),X3))))),
inference(forward_demodulation,[],[f896,f520]) ).
fof(f921,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(inverse(X0),double_divide(inverse(X2),double_divide(X1,X0)))) = X2,
inference(forward_demodulation,[],[f898,f313]) ).
fof(f923,plain,
! [X3,X0,X1] : double_divide(X1,X3) = double_divide(inverse(X0),double_divide(inverse(X3),double_divide(X1,X0))),
inference(forward_demodulation,[],[f904,f510]) ).
fof(f930,plain,
! [X1] : inverse(inverse(X1)) = X1,
inference(forward_demodulation,[],[f916,f736]) ).
fof(f934,plain,
! [X2,X1] : double_divide(X1,double_divide(X1,X2)) = X2,
inference(backward_demodulation,[],[f921,f923]) ).
fof(f940,plain,
! [X2,X0] : double_divide(inverse(X2),X0) = double_divide(X0,inverse(X2)),
inference(backward_demodulation,[],[f504,f930]) ).
fof(f942,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X0),X0)),X2) = double_divide(X1,double_divide(inverse(X2),X1)),
inference(backward_demodulation,[],[f594,f930]) ).
fof(f947,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(X0,X2)) = double_divide(inverse(X0),double_divide(inverse(inverse(X2)),X1)),
inference(backward_demodulation,[],[f718,f930]) ).
fof(f960,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(X0,X2)) = double_divide(inverse(X0),double_divide(X2,X1)),
inference(forward_demodulation,[],[f947,f930]) ).
fof(f973,plain,
sF1 = inverse(sF2),
inference(superposition,[],[f930,f11]) ).
fof(f975,plain,
sF7 = inverse(sF8),
inference(superposition,[],[f930,f23]) ).
fof(f976,plain,
sF9 = inverse(sF10),
inference(superposition,[],[f930,f27]) ).
fof(f977,plain,
sF13 = inverse(sF14),
inference(superposition,[],[f930,f35]) ).
fof(f980,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X1,X2)),X0) = double_divide(inverse(double_divide(X1,X0)),X2),
inference(superposition,[],[f224,f930]) ).
fof(f981,plain,
! [X0,X1] : inverse(X0) = double_divide(X0,double_divide(inverse(X1),X1)),
inference(superposition,[],[f313,f930]) ).
fof(f987,plain,
! [X2,X0,X1] : double_divide(inverse(X1),inverse(double_divide(X2,X1))) = double_divide(X2,inverse(double_divide(X0,inverse(X0)))),
inference(superposition,[],[f586,f930]) ).
fof(f992,plain,
! [X0,X1] : inverse(X0) = double_divide(X0,double_divide(X1,inverse(X1))),
inference(forward_demodulation,[],[f981,f940]) ).
fof(f993,plain,
! [X0] : double_divide(a2,inverse(double_divide(inverse(X0),X0))) = double_divide(sF10,sF7),
inference(backward_demodulation,[],[f884,f975]) ).
fof(f1000,plain,
! [X0] : double_divide(sF10,sF7) = double_divide(a2,inverse(double_divide(X0,inverse(X0)))),
inference(forward_demodulation,[],[f993,f940]) ).
fof(f1034,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(X0,X1),
inference(superposition,[],[f940,f930]) ).
fof(f1039,plain,
! [X0] : double_divide(X0,sF0) = double_divide(sF0,X0),
inference(superposition,[],[f940,f7]) ).
fof(f1040,plain,
! [X0] : double_divide(X0,sF2) = double_divide(sF2,X0),
inference(superposition,[],[f940,f11]) ).
fof(f1043,plain,
! [X0] : double_divide(X0,sF10) = double_divide(sF10,X0),
inference(superposition,[],[f940,f27]) ).
fof(f1055,plain,
! [X0,X1] : double_divide(inverse(X1),double_divide(X0,inverse(X1))) = X0,
inference(superposition,[],[f934,f940]) ).
fof(f1057,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,inverse(X1))),inverse(X2)) = double_divide(inverse(double_divide(inverse(X1),inverse(X2))),X0),
inference(superposition,[],[f224,f940]) ).
fof(f1058,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X1,X0)),inverse(X2)) = double_divide(X0,inverse(double_divide(X1,inverse(X2)))),
inference(superposition,[],[f224,f940]) ).
fof(f1064,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X1,X2)),inverse(X0)) = double_divide(inverse(double_divide(inverse(X0),X1)),X2),
inference(superposition,[],[f224,f940]) ).
fof(f1070,plain,
! [X0,X1] : inverse(X0) = double_divide(X1,double_divide(inverse(X0),X1)),
inference(superposition,[],[f934,f940]) ).
fof(f1071,plain,
! [X2,X0,X1] : double_divide(X1,inverse(double_divide(inverse(X2),X2))) = double_divide(inverse(inverse(X0)),inverse(double_divide(inverse(X0),X1))),
inference(superposition,[],[f586,f940]) ).
fof(f1072,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X1,inverse(X2))),inverse(X0)) = double_divide(inverse(double_divide(inverse(X0),X1)),inverse(X2)),
inference(superposition,[],[f224,f940]) ).
fof(f1074,plain,
! [X2,X0,X1] : double_divide(inverse(X0),double_divide(inverse(X1),X2)) = double_divide(inverse(double_divide(X1,inverse(X2))),inverse(X0)),
inference(forward_demodulation,[],[f1072,f653]) ).
fof(f1075,plain,
! [X2,X0,X1] : double_divide(inverse(X0),double_divide(inverse(X1),inverse(X0))) = double_divide(X1,inverse(double_divide(inverse(X2),X2))),
inference(forward_demodulation,[],[f1071,f513]) ).
fof(f1076,plain,
! [X2,X0] : inverse(X2) = double_divide(inverse(double_divide(inverse(X0),X0)),X2),
inference(backward_demodulation,[],[f942,f1070]) ).
fof(f1087,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(inverse(X2),X0)) = double_divide(X2,inverse(double_divide(inverse(X1),inverse(X0)))),
inference(backward_demodulation,[],[f653,f1058]) ).
fof(f1101,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,inverse(X1))),inverse(X2)) = double_divide(inverse(X2),inverse(double_divide(inverse(X1),X0))),
inference(forward_demodulation,[],[f1057,f641]) ).
fof(f1113,plain,
! [X2,X0,X1] : double_divide(inverse(X0),double_divide(inverse(X1),X2)) = double_divide(inverse(X2),inverse(double_divide(X1,inverse(X0)))),
inference(forward_demodulation,[],[f1074,f641]) ).
fof(f1114,plain,
! [X2,X0,X1] : double_divide(inverse(X0),double_divide(inverse(X1),inverse(X0))) = double_divide(X1,inverse(double_divide(X2,inverse(X2)))),
inference(forward_demodulation,[],[f1075,f940]) ).
fof(f1115,plain,
! [X2,X0] : inverse(X2) = double_divide(inverse(double_divide(X0,inverse(X0))),X2),
inference(forward_demodulation,[],[f1076,f940]) ).
fof(f1125,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,inverse(X1))),inverse(X2)) = double_divide(inverse(X1),double_divide(inverse(X0),X2)),
inference(forward_demodulation,[],[f1101,f513]) ).
fof(f1129,plain,
! [X2,X3,X0] : double_divide(X0,inverse(X2)) = double_divide(inverse(double_divide(inverse(X3),X3)),double_divide(inverse(X0),X2)),
inference(backward_demodulation,[],[f919,f1113]) ).
fof(f1131,plain,
! [X2,X1] : inverse(X1) = double_divide(X1,inverse(double_divide(X2,inverse(X2)))),
inference(forward_demodulation,[],[f1114,f1055]) ).
fof(f1132,plain,
! [X2,X0] : inverse(X2) = double_divide(inverse(X0),inverse(double_divide(X0,X2))),
inference(forward_demodulation,[],[f1115,f641]) ).
fof(f1136,plain,
! [X2,X0,X1] : double_divide(inverse(X1),inverse(double_divide(X0,inverse(X2)))) = double_divide(inverse(X1),double_divide(inverse(X0),X2)),
inference(forward_demodulation,[],[f1125,f641]) ).
fof(f1139,plain,
! [X2,X3,X0] : double_divide(X0,inverse(X2)) = double_divide(inverse(double_divide(X3,inverse(X3))),double_divide(inverse(X0),X2)),
inference(forward_demodulation,[],[f1129,f940]) ).
fof(f1141,plain,
! [X2,X1] : inverse(X2) = double_divide(inverse(X1),inverse(double_divide(X2,X1))),
inference(backward_demodulation,[],[f987,f1131]) ).
fof(f1143,plain,
double_divide(sF10,sF7) = inverse(a2),
inference(backward_demodulation,[],[f1000,f1131]) ).
fof(f1148,plain,
! [X2,X3,X0] : double_divide(X0,inverse(X2)) = double_divide(inverse(X3),inverse(double_divide(X3,double_divide(inverse(X0),X2)))),
inference(forward_demodulation,[],[f1139,f641]) ).
fof(f1150,plain,
inverse(a2) = double_divide(sF7,sF10),
inference(forward_demodulation,[],[f1143,f1043]) ).
fof(f1157,plain,
! [X1] : inverse(X1) = double_divide(X1,inverse(double_divide(sF0,a1))),
inference(backward_demodulation,[],[f788,f1141]) ).
fof(f1178,plain,
! [X2,X0] : inverse(double_divide(inverse(X0),X2)) = double_divide(X0,inverse(X2)),
inference(forward_demodulation,[],[f1148,f1132]) ).
fof(f1188,plain,
! [X1] : inverse(X1) = double_divide(X1,inverse(double_divide(a1,sF0))),
inference(forward_demodulation,[],[f1157,f1039]) ).
fof(f1223,plain,
! [X2,X0,X1] : inverse(double_divide(X0,X2)) = double_divide(inverse(X2),double_divide(X0,double_divide(X1,inverse(X1)))),
inference(backward_demodulation,[],[f811,f1178]) ).
fof(f1230,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(inverse(X2),X0)) = double_divide(inverse(X1),double_divide(X0,inverse(X2))),
inference(backward_demodulation,[],[f661,f1178]) ).
fof(f1232,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X1,X2)),inverse(X0)) = double_divide(double_divide(X0,inverse(X1)),X2),
inference(backward_demodulation,[],[f1064,f1178]) ).
fof(f1234,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(inverse(X2),X0)) = double_divide(X2,double_divide(X1,inverse(inverse(X0)))),
inference(backward_demodulation,[],[f1087,f1178]) ).
fof(f1275,plain,
! [X1] : inverse(X1) = double_divide(X1,inverse(sF1)),
inference(forward_demodulation,[],[f1188,f9]) ).
fof(f1319,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(inverse(X2),X0)) = double_divide(X2,double_divide(X1,X0)),
inference(forward_demodulation,[],[f1234,f930]) ).
fof(f1321,plain,
! [X2,X0,X1] : double_divide(X0,inverse(double_divide(X1,inverse(X2)))) = double_divide(double_divide(X2,inverse(X1)),X0),
inference(backward_demodulation,[],[f1058,f1232]) ).
fof(f1322,plain,
! [X3,X0,X1] : double_divide(inverse(double_divide(X1,inverse(X0))),X3) = double_divide(double_divide(X0,inverse(X1)),X3),
inference(backward_demodulation,[],[f224,f1232]) ).
fof(f1328,plain,
! [X2,X0] : double_divide(inverse(X2),inverse(X0)) = inverse(double_divide(X0,X2)),
inference(forward_demodulation,[],[f1223,f992]) ).
fof(f1354,plain,
! [X1] : inverse(X1) = double_divide(X1,sF2),
inference(forward_demodulation,[],[f1275,f11]) ).
fof(f1380,plain,
! [X2,X3] : double_divide(X2,double_divide(X3,X2)) = X3,
inference(backward_demodulation,[],[f313,f1319]) ).
fof(f1385,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X1,X2)) = double_divide(inverse(X1),inverse(double_divide(X0,inverse(X2)))),
inference(backward_demodulation,[],[f1136,f1319]) ).
fof(f1386,plain,
! [X2,X0,X1] : double_divide(inverse(X1),double_divide(X0,inverse(X2))) = double_divide(X2,double_divide(X1,X0)),
inference(backward_demodulation,[],[f1230,f1319]) ).
fof(f1392,plain,
! [X2,X0,X1] : double_divide(inverse(X0),inverse(double_divide(X1,X2))) = double_divide(double_divide(X0,inverse(X1)),X2),
inference(backward_demodulation,[],[f641,f1322]) ).
fof(f1394,plain,
! [X2,X1] : inverse(X1) = double_divide(double_divide(X2,inverse(X2)),X1),
inference(backward_demodulation,[],[f1131,f1321]) ).
fof(f1425,plain,
! [X2,X0] : double_divide(inverse(X0),inverse(X2)) = inverse(double_divide(X0,X2)),
inference(backward_demodulation,[],[f516,f1328]) ).
fof(f1440,plain,
! [X0] : inverse(X0) = double_divide(sF2,X0),
inference(backward_demodulation,[],[f1040,f1354]) ).
fof(f1447,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X1,X2)) = inverse(double_divide(double_divide(X0,inverse(X2)),X1)),
inference(forward_demodulation,[],[f1385,f1328]) ).
fof(f1453,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,inverse(X1)),X2) = inverse(double_divide(double_divide(X1,X2),X0)),
inference(forward_demodulation,[],[f1392,f1328]) ).
fof(f1500,plain,
! [X0] : sF1 = inverse(double_divide(inverse(X0),X0)),
inference(backward_demodulation,[],[f395,f1440]) ).
fof(f1501,plain,
! [X0] : inverse(sF1) = double_divide(inverse(X0),X0),
inference(backward_demodulation,[],[f565,f1440]) ).
fof(f1508,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X1,X2)) = double_divide(double_divide(X1,inverse(X0)),inverse(X2)),
inference(backward_demodulation,[],[f1447,f1453]) ).
fof(f1550,plain,
! [X0] : inverse(sF1) = double_divide(X0,inverse(X0)),
inference(forward_demodulation,[],[f1501,f940]) ).
fof(f1551,plain,
! [X0] : sF1 = double_divide(X0,inverse(X0)),
inference(forward_demodulation,[],[f1500,f1178]) ).
fof(f1579,plain,
! [X0] : sF2 = double_divide(X0,inverse(X0)),
inference(forward_demodulation,[],[f1550,f11]) ).
fof(f1583,plain,
! [X1] : inverse(X1) = double_divide(sF1,X1),
inference(backward_demodulation,[],[f1394,f1551]) ).
fof(f1584,plain,
sF1 = sF4,
inference(backward_demodulation,[],[f70,f1551]) ).
fof(f1585,plain,
sF1 = sF7,
inference(backward_demodulation,[],[f71,f1551]) ).
fof(f1609,plain,
sF1 = sF2,
inference(forward_demodulation,[],[f1579,f1551]) ).
fof(f1616,plain,
inverse(a2) = double_divide(sF1,sF10),
inference(backward_demodulation,[],[f1150,f1585]) ).
fof(f1620,plain,
inverse(sF1) = sF5,
inference(backward_demodulation,[],[f17,f1584]) ).
fof(f1653,plain,
sF1 = inverse(sF1),
inference(backward_demodulation,[],[f973,f1609]) ).
fof(f1659,plain,
inverse(sF10) = inverse(a2),
inference(forward_demodulation,[],[f1616,f1583]) ).
fof(f1676,plain,
sF1 = sF5,
inference(backward_demodulation,[],[f1620,f1653]) ).
fof(f1680,plain,
sF9 = inverse(a2),
inference(backward_demodulation,[],[f976,f1659]) ).
fof(f1710,plain,
sF10 = inverse(inverse(a2)),
inference(backward_demodulation,[],[f27,f1680]) ).
fof(f1741,plain,
a2 = sF10,
inference(forward_demodulation,[],[f1710,f930]) ).
fof(f1753,plain,
spl23_3,
inference(avatar_split_clause,[],[f1741,f62]) ).
fof(f1808,plain,
inverse(double_divide(a4,b4)) = sF20,
inference(superposition,[],[f74,f1034]) ).
fof(f1809,plain,
sF20 = sF22,
inference(backward_demodulation,[],[f75,f1808]) ).
fof(f1818,plain,
( $false
| spl23_1 ),
inference(forward_subsumption_resolution,[],[f1809,f56]) ).
fof(f1819,plain,
spl23_1,
inference(avatar_contradiction_clause,[],[f1818]) ).
fof(f1929,plain,
! [X0] : double_divide(sF12,inverse(X0)) = inverse(double_divide(double_divide(b3,a3),X0)),
inference(superposition,[],[f1425,f72]) ).
fof(f1930,plain,
! [X0] : double_divide(sF16,inverse(X0)) = inverse(double_divide(double_divide(c3,b3),X0)),
inference(superposition,[],[f1425,f73]) ).
fof(f1980,plain,
! [X0] : double_divide(sF16,inverse(X0)) = double_divide(double_divide(X0,inverse(c3)),b3),
inference(forward_demodulation,[],[f1930,f1453]) ).
fof(f1981,plain,
! [X0] : double_divide(sF12,inverse(X0)) = double_divide(double_divide(X0,inverse(b3)),a3),
inference(forward_demodulation,[],[f1929,f1453]) ).
fof(f2001,plain,
! [X0] : double_divide(sF16,inverse(X0)) = double_divide(b3,double_divide(X0,inverse(c3))),
inference(forward_demodulation,[],[f1980,f1034]) ).
fof(f2002,plain,
! [X0] : double_divide(sF12,inverse(X0)) = double_divide(a3,double_divide(X0,inverse(b3))),
inference(forward_demodulation,[],[f1981,f1034]) ).
fof(f2412,plain,
! [X2,X0,X1] : double_divide(inverse(X2),inverse(double_divide(X0,X1))) = double_divide(inverse(inverse(X1)),double_divide(X2,inverse(X0))),
inference(superposition,[],[f960,f1425]) ).
fof(f2416,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X3),double_divide(inverse(X0),double_divide(X1,X2))) = double_divide(inverse(double_divide(X2,X0)),double_divide(X3,inverse(X1))),
inference(superposition,[],[f960,f960]) ).
fof(f2448,plain,
! [X2,X0,X1] : inverse(double_divide(inverse(X0),double_divide(X1,X2))) = double_divide(X1,inverse(double_divide(X2,X0))),
inference(superposition,[],[f1178,f960]) ).
fof(f2460,plain,
! [X2,X0,X1] : double_divide(X0,inverse(double_divide(X1,X2))) = double_divide(X1,inverse(double_divide(X2,X0))),
inference(forward_demodulation,[],[f2448,f1178]) ).
fof(f2482,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X3),double_divide(inverse(X0),double_divide(X1,X2))) = double_divide(X1,double_divide(double_divide(X2,X0),X3)),
inference(forward_demodulation,[],[f2416,f1386]) ).
fof(f2486,plain,
! [X2,X0,X1] : double_divide(inverse(X2),inverse(double_divide(X0,X1))) = double_divide(X0,double_divide(inverse(X1),X2)),
inference(forward_demodulation,[],[f2412,f1386]) ).
fof(f2540,plain,
! [X2,X3,X0,X1] : double_divide(X1,double_divide(double_divide(X2,X0),X3)) = double_divide(X0,double_divide(X3,double_divide(X1,X2))),
inference(forward_demodulation,[],[f2482,f1319]) ).
fof(f2542,plain,
! [X2,X0,X1] : inverse(double_divide(double_divide(X0,X1),X2)) = double_divide(X0,double_divide(inverse(X1),X2)),
inference(forward_demodulation,[],[f2486,f1328]) ).
fof(f2572,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,inverse(X1)),X2) = double_divide(X1,double_divide(inverse(X2),X0)),
inference(backward_demodulation,[],[f1453,f2542]) ).
fof(f2595,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X1,X2)) = double_divide(X0,double_divide(inverse(inverse(X2)),X1)),
inference(backward_demodulation,[],[f1508,f2572]) ).
fof(f2608,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X1,X2)) = double_divide(X0,double_divide(X2,X1)),
inference(forward_demodulation,[],[f2595,f930]) ).
fof(f2851,plain,
! [X0] : double_divide(X0,inverse(sF13)) = double_divide(sF12,inverse(double_divide(X0,c3))),
inference(superposition,[],[f2460,f33]) ).
fof(f2884,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,X1)),X2) = double_divide(X0,inverse(double_divide(X1,X2))),
inference(superposition,[],[f1034,f2460]) ).
fof(f2939,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X1,X0)),X2) = double_divide(X1,inverse(double_divide(X2,X0))),
inference(backward_demodulation,[],[f980,f2884]) ).
fof(f2957,plain,
! [X0] : double_divide(X0,inverse(sF13)) = double_divide(a3,double_divide(double_divide(X0,c3),inverse(b3))),
inference(forward_demodulation,[],[f2851,f2002]) ).
fof(f3043,plain,
! [X0] : double_divide(X0,inverse(sF13)) = double_divide(a3,double_divide(inverse(b3),double_divide(X0,c3))),
inference(forward_demodulation,[],[f2957,f2608]) ).
fof(f3104,plain,
! [X0] : double_divide(X0,sF14) = double_divide(a3,double_divide(inverse(b3),double_divide(X0,c3))),
inference(forward_demodulation,[],[f3043,f35]) ).
fof(f3220,plain,
! [X0] : double_divide(inverse(sF17),X0) = double_divide(sF16,inverse(double_divide(X0,a3))),
inference(superposition,[],[f2939,f41]) ).
fof(f3316,plain,
! [X0] : double_divide(inverse(sF17),X0) = double_divide(b3,double_divide(double_divide(X0,a3),inverse(c3))),
inference(forward_demodulation,[],[f3220,f2001]) ).
fof(f3358,plain,
! [X0] : double_divide(inverse(sF17),X0) = double_divide(a3,double_divide(inverse(c3),double_divide(b3,X0))),
inference(forward_demodulation,[],[f3316,f2540]) ).
fof(f3387,plain,
! [X0] : double_divide(inverse(sF17),X0) = double_divide(a3,double_divide(inverse(b3),double_divide(X0,c3))),
inference(forward_demodulation,[],[f3358,f960]) ).
fof(f3407,plain,
! [X0] : double_divide(X0,sF14) = double_divide(inverse(sF17),X0),
inference(forward_demodulation,[],[f3387,f3104]) ).
fof(f3424,plain,
! [X0] : double_divide(X0,sF14) = double_divide(sF18,X0),
inference(forward_demodulation,[],[f3407,f43]) ).
fof(f3437,plain,
! [X0] : sF17 = double_divide(double_divide(inverse(X0),X0),sF14),
inference(backward_demodulation,[],[f400,f3424]) ).
fof(f3446,plain,
! [X0] : sF17 = double_divide(double_divide(X0,inverse(X0)),sF14),
inference(forward_demodulation,[],[f3437,f940]) ).
fof(f3458,plain,
! [X0] : sF17 = double_divide(X0,double_divide(inverse(sF14),X0)),
inference(forward_demodulation,[],[f3446,f2572]) ).
fof(f3464,plain,
sF17 = inverse(sF14),
inference(forward_demodulation,[],[f3458,f1380]) ).
fof(f3466,plain,
sF13 = sF17,
inference(forward_demodulation,[],[f3464,f977]) ).
fof(f3469,plain,
inverse(sF13) = sF18,
inference(backward_demodulation,[],[f43,f3466]) ).
fof(f3484,plain,
sF14 = sF18,
inference(forward_demodulation,[],[f3469,f35]) ).
fof(f3488,plain,
( $false
| spl23_2 ),
inference(forward_subsumption_resolution,[],[f3484,f60]) ).
fof(f3489,plain,
spl23_2,
inference(avatar_contradiction_clause,[],[f3488]) ).
fof(f3492,plain,
( sF1 != sF2
| spl23_4 ),
inference(forward_demodulation,[],[f68,f1676]) ).
fof(f3493,plain,
( $false
| spl23_4 ),
inference(forward_subsumption_resolution,[],[f3492,f1609]) ).
fof(f3494,plain,
spl23_4,
inference(avatar_contradiction_clause,[],[f3493]) ).
cnf(s1,plain,
( ~ spl23_1
| ~ spl23_2
| ~ spl23_3
| ~ spl23_4 ),
inference(sat_conversion,[],[f69]) ).
cnf(s2,plain,
spl23_3,
inference(sat_conversion,[],[f1753]) ).
cnf(s3,plain,
spl23_1,
inference(sat_conversion,[],[f1819]) ).
cnf(s4,plain,
spl23_2,
inference(sat_conversion,[],[f3489]) ).
cnf(s5,plain,
spl23_4,
inference(sat_conversion,[],[f3494]) ).
cnf(s6,plain,
$false,
inference(rat,[],[s1,s5,s2,s4,s3]) ).
fof(f3495,plain,
$false,
inference(avatar_sat_refutation,[],[s6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP109-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n001.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 09:25:30 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/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
% 5.73/2.05 % (3289328)Input is clausal, will run a generic CNF schedule.
% 5.73/2.05 % (3289376)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3293190443:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.73/2.05 % (3289380)dis-21_1_sil=8000:lcm=predicate:random_seed=1876017301: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)
% 5.73/2.05 % (3289380)Refutation not found, incomplete strategy
% 5.73/2.05 % (3289380)------------------------------
% 5.73/2.05 % (3289380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/2.05 % (3289380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/2.05 % (3289380)CaDiCaL version: 2.1.3
% 5.73/2.05 % (3289380)Termination reason: Refutation not found, incomplete strategy
% 5.73/2.05 % (3289380)Time elapsed: 0.002 s
% 5.73/2.05 % (3289380)Peak memory usage: 88 MB
% 5.73/2.05 % (3289375)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1598207454:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.73/2.05 % (3289378)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2007807133:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.73/2.05 % (3289374)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=2102256428:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.73/2.05 % (3289377)lrs+10_1_sil=8000:sp=occurrence:random_seed=2706973829:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.73/2.05 % (3289379)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1718995692:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.73/2.05 % (3289377)Instruction limit reached!
% 5.73/2.05 % (3289377)------------------------------
% 5.73/2.05 % (3289377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/2.05 % (3289377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/2.05 % (3289377)CaDiCaL version: 2.1.3
% 5.73/2.05 % (3289377)Termination reason: Instruction limit
% 5.73/2.05 % (3289377)Termination phase: Saturation
% 5.73/2.05 % (3289377)Time elapsed: 0.108 s
% 5.73/2.05 % (3289377)Peak memory usage: 89 MB
% 5.73/2.05 % (3289377)Instructions burned: 107 (million)
% 5.73/2.05 % (3289378)Instruction limit reached!
% 5.73/2.05 % (3289378)------------------------------
% 5.73/2.05 % (3289378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/2.05 % (3289378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/2.05 % (3289378)CaDiCaL version: 2.1.3
% 5.73/2.05 % (3289378)Termination reason: Instruction limit
% 5.73/2.05 % (3289378)Termination phase: Saturation
% 5.73/2.05 % (3289378)Time elapsed: 0.116 s
% 5.73/2.05 % (3289378)Peak memory usage: 89 MB
% 5.73/2.05 % (3289378)Instructions burned: 114 (million)
% 5.73/2.05 % (3289379)Instruction limit reached!
% 5.73/2.05 % (3289379)------------------------------
% 5.73/2.05 % (3289379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/2.05 % (3289379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/2.05 % (3289379)CaDiCaL version: 2.1.3
% 5.73/2.05 % (3289379)Termination reason: Instruction limit
% 5.73/2.05 % (3289379)Termination phase: Saturation
% 5.73/2.05 % (3289379)Time elapsed: 0.170 s
% 5.73/2.05 % (3289379)Peak memory usage: 90 MB
% 5.73/2.05 % (3289379)Instructions burned: 180 (million)
% 5.73/2.05 % (3289392)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=2694456448:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 5.73/2.05 % (3289392)Refutation not found, incomplete strategy
% 5.73/2.05 % (3289392)------------------------------
% 5.73/2.05 % (3289392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/2.05 % (3289392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/2.05 % (3289392)CaDiCaL version: 2.1.3
% 5.73/2.05 % (3289392)Termination reason: Refutation not found, incomplete strategy
% 5.73/2.05 % (3289392)Time elapsed: 0.002 s
% 5.73/2.05 % (3289392)Peak memory usage: 88 MB
% 5.73/2.05 % (3289380)------------------------------
% 5.73/2.05 % (3289380)------------------------------
% 5.73/2.05 % (3289394)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1274902942:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 5.73/2.05 % (3289393)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2318915893:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 5.73/2.05 % (3289394)Refutation not found, incomplete strategy
% 5.73/2.05 % (3289394)------------------------------
% 5.73/2.05 % (3289394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/2.05 % (3289394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/2.05 % (3289394)CaDiCaL version: 2.1.3
% 5.73/2.05 % (3289394)Termination reason: Refutation not found, incomplete strategy
% 5.73/2.05 % (3289394)Time elapsed: 0.002 s
% 5.73/2.05 % (3289394)Peak memory usage: 88 MB
% 5.73/2.05 % (3289393)Refutation not found, incomplete strategy
% 5.73/2.05 % (3289393)------------------------------
% 5.73/2.05 % (3289393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/2.05 % (3289393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/2.05 % (3289393)CaDiCaL version: 2.1.3
% 5.73/2.05 % (3289393)Termination reason: Refutation not found, incomplete strategy
% 5.73/2.05 % (3289393)Time elapsed: 0.002 s
% 5.73/2.05 % (3289393)Peak memory usage: 88 MB
% 5.73/2.05 % (3289400)lrs+10_64_to=lpo:sil=8000:random_seed=3839945172:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 5.73/2.05 % (3289392)------------------------------
% 5.73/2.05 % (3289392)------------------------------
% 5.73/2.05 % (3289376)First to succeed.
% 5.73/2.05 % (3289376)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3289328"
% 5.73/2.05 % (3289400)Instruction limit reached!
% 5.73/2.05 % (3289400)------------------------------
% 5.73/2.05 % (3289400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/2.05 % (3289400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/2.05 % (3289400)CaDiCaL version: 2.1.3
% 5.73/2.05 % (3289400)Termination reason: Instruction limit
% 5.73/2.05 % (3289400)Termination phase: Saturation
% 5.73/2.05 % (3289400)Time elapsed: 0.097 s
% 5.73/2.05 % (3289400)Peak memory usage: 89 MB
% 5.73/2.05 % (3289400)Instructions burned: 126 (million)
% 5.73/2.05 % (3289394)------------------------------
% 5.73/2.05 % (3289394)------------------------------
% 5.73/2.05 % (3289393)------------------------------
% 5.73/2.05 % (3289393)------------------------------
% 5.73/2.05 % (3289409)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3068972035:avsq=on:i=194:fgj=on:bd=preordered_2990 on theBenchmark for (2990ds/194Mi)
% 5.73/2.05 % (3289376)Refutation found. Thanks to Tanya!
% 5.73/2.05 % SZS status Unsatisfiable for theBenchmark
% 5.73/2.05 % SZS output start Proof for theBenchmark
% See solution above
% 8.69/2.26 % (3289376)------------------------------
% 8.69/2.26 % (3289376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.26 % (3289376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.26 % (3289376)CaDiCaL version: 2.1.3
% 8.69/2.26 % (3289376)Termination reason: Refutation
% 8.69/2.26 % (3289376)Time elapsed: 0.762 s
% 8.69/2.26 % (3289376)Peak memory usage: 134 MB
% 8.69/2.26 % (3289376)Instructions burned: 1415 (million)
% 8.69/2.26 % (3289376)------------------------------
% 8.69/2.26 % (3289376)------------------------------
% 8.69/2.26 % (3289328)Success in time 1.134 s
% 8.69/2.26 % Vampire exiting
%------------------------------------------------------------------------------