%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP108-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 11.29s 2.34s
% Output : Refutation 12.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 30
% Syntax : Number of formulae : 305 ( 288 unt; 27 def)
% Number of atoms : 334 ( 302 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 : 8 ( 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 : 431 ( 0 sgn 431 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : inverse(double_divide(inverse(double_divide(X0,inverse(double_divide(X1,double_divide(X0,X2))))),X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,axiom,
! [X0,X1] : multiply(X0,X1) = inverse(double_divide(X1,X0)),
file('/export/starexec/sandbox/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/sandbox/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,
! [X2,X3,X0,X1] : inverse(double_divide(X2,inverse(double_divide(X0,double_divide(X2,double_divide(X1,X3)))))) = inverse(double_divide(inverse(double_divide(X1,X0)),X3)),
inference(superposition,[],[f1,f1]) ).
fof(f92,plain,
! [X2,X0,X1] : inverse(double_divide(inverse(double_divide(inverse(double_divide(X0,X1)),X2)),double_divide(X0,X2))) = X1,
inference(superposition,[],[f1,f70]) ).
fof(f107,plain,
! [X2,X0,X1] : inverse(double_divide(X0,double_divide(inverse(double_divide(X1,X0)),double_divide(X1,X2)))) = X2,
inference(superposition,[],[f92,f92]) ).
fof(f155,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X2,X1)),double_divide(X2,X0)) = inverse(double_divide(inverse(double_divide(X0,X3)),double_divide(X1,X3))),
inference(superposition,[],[f92,f107]) ).
fof(f204,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,X2)) = double_divide(inverse(double_divide(X3,X1)),double_divide(X3,X2)),
inference(superposition,[],[f155,f155]) ).
fof(f218,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,inverse(double_divide(X1,X2)))) = X2,
inference(superposition,[],[f92,f155]) ).
fof(f361,plain,
! [X0,X1] : double_divide(inverse(double_divide(X0,sF6)),double_divide(X0,X1)) = double_divide(inverse(sF7),double_divide(b2,X1)),
inference(superposition,[],[f204,f21]) ).
fof(f365,plain,
! [X0,X1] : double_divide(inverse(double_divide(X0,sF12)),double_divide(X0,X1)) = double_divide(inverse(sF13),double_divide(c3,X1)),
inference(superposition,[],[f204,f33]) ).
fof(f449,plain,
! [X0,X1] : double_divide(inverse(double_divide(X0,sF12)),double_divide(X0,X1)) = double_divide(sF14,double_divide(c3,X1)),
inference(forward_demodulation,[],[f365,f35]) ).
fof(f453,plain,
! [X0,X1] : double_divide(inverse(double_divide(X0,sF6)),double_divide(X0,X1)) = double_divide(sF8,double_divide(b2,X1)),
inference(forward_demodulation,[],[f361,f23]) ).
fof(f504,plain,
! [X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,X1)) = inverse(double_divide(sF8,double_divide(b2,sF6))),
inference(superposition,[],[f155,f453]) ).
fof(f529,plain,
! [X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,X1)) = inverse(double_divide(sF8,sF7)),
inference(forward_demodulation,[],[f504,f21]) ).
fof(f715,plain,
! [X0] : inverse(double_divide(sF8,sF7)) = double_divide(inverse(X0),X0),
inference(superposition,[],[f529,f218]) ).
fof(f741,plain,
! [X0] : inverse(double_divide(X0,inverse(double_divide(sF8,sF7)))) = X0,
inference(superposition,[],[f107,f529]) ).
fof(f744,plain,
double_divide(sF8,double_divide(b2,sF6)) = inverse(double_divide(sF8,sF7)),
inference(superposition,[],[f453,f529]) ).
fof(f745,plain,
inverse(double_divide(sF8,sF7)) = double_divide(sF14,double_divide(c3,sF12)),
inference(superposition,[],[f449,f529]) ).
fof(f746,plain,
! [X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,X1)) = inverse(inverse(double_divide(sF8,sF7))),
inference(superposition,[],[f155,f529]) ).
fof(f775,plain,
inverse(double_divide(sF8,sF7)) = inverse(inverse(double_divide(sF8,sF7))),
inference(forward_demodulation,[],[f746,f529]) ).
fof(f776,plain,
inverse(double_divide(sF8,sF7)) = double_divide(sF14,sF13),
inference(forward_demodulation,[],[f745,f33]) ).
fof(f777,plain,
double_divide(sF8,sF7) = inverse(double_divide(sF8,sF7)),
inference(forward_demodulation,[],[f744,f21]) ).
fof(f796,plain,
double_divide(sF8,sF7) = double_divide(sF14,sF13),
inference(forward_demodulation,[],[f777,f776]) ).
fof(f823,plain,
! [X0,X1] : double_divide(inverse(X0),X0) = double_divide(inverse(X1),X1),
inference(superposition,[],[f715,f715]) ).
fof(f861,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,inverse(X1))),double_divide(X0,X2)) = inverse(double_divide(inverse(double_divide(X2,X1)),inverse(double_divide(sF8,sF7)))),
inference(superposition,[],[f155,f715]) ).
fof(f863,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,inverse(X2))) = inverse(double_divide(inverse(inverse(double_divide(sF8,sF7))),double_divide(X1,X2))),
inference(superposition,[],[f155,f715]) ).
fof(f864,plain,
! [X2,X0,X1] : inverse(double_divide(inverse(double_divide(X0,X2)),double_divide(X1,X2))) = double_divide(inverse(double_divide(inverse(X0),X1)),inverse(double_divide(sF8,sF7))),
inference(superposition,[],[f155,f715]) ).
fof(f868,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,X2)) = double_divide(inverse(inverse(double_divide(sF8,sF7))),double_divide(inverse(X1),X2)),
inference(superposition,[],[f204,f715]) ).
fof(f870,plain,
! [X0,X1] : double_divide(inverse(double_divide(X0,inverse(X1))),double_divide(X0,inverse(inverse(double_divide(sF8,sF7))))) = X1,
inference(superposition,[],[f218,f715]) ).
fof(f886,plain,
! [X0,X1] : double_divide(inverse(double_divide(X0,inverse(X1))),double_divide(X0,inverse(double_divide(sF8,sF7)))) = X1,
inference(forward_demodulation,[],[f870,f775]) ).
fof(f888,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,X2)) = double_divide(inverse(double_divide(sF8,sF7)),double_divide(inverse(X1),X2)),
inference(forward_demodulation,[],[f868,f775]) ).
fof(f892,plain,
! [X2,X0,X1] : inverse(double_divide(inverse(double_divide(X0,X2)),double_divide(X1,X2))) = double_divide(inverse(double_divide(inverse(X0),X1)),double_divide(sF14,sF13)),
inference(forward_demodulation,[],[f864,f776]) ).
fof(f893,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,inverse(X2))) = inverse(double_divide(inverse(double_divide(sF8,sF7)),double_divide(X1,X2))),
inference(forward_demodulation,[],[f863,f775]) ).
fof(f895,plain,
! [X2,X0,X1] : inverse(double_divide(X2,X1)) = double_divide(inverse(double_divide(X0,inverse(X1))),double_divide(X0,X2)),
inference(forward_demodulation,[],[f861,f741]) ).
fof(f920,plain,
! [X0,X1] : double_divide(inverse(double_divide(X0,inverse(X1))),double_divide(X0,double_divide(sF14,sF13))) = X1,
inference(forward_demodulation,[],[f886,f776]) ).
fof(f922,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,X2)) = double_divide(double_divide(sF14,sF13),double_divide(inverse(X1),X2)),
inference(forward_demodulation,[],[f888,f776]) ).
fof(f926,plain,
! [X2,X0,X1] : inverse(double_divide(inverse(double_divide(X0,X2)),double_divide(X1,X2))) = double_divide(inverse(double_divide(inverse(X0),X1)),double_divide(sF8,sF7)),
inference(forward_demodulation,[],[f892,f796]) ).
fof(f927,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,inverse(X2))) = inverse(double_divide(double_divide(sF14,sF13),double_divide(X1,X2))),
inference(forward_demodulation,[],[f893,f776]) ).
fof(f940,plain,
! [X1] : inverse(double_divide(double_divide(sF14,sF13),X1)) = X1,
inference(forward_demodulation,[],[f920,f895]) ).
fof(f942,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,X2)) = double_divide(double_divide(sF8,sF7),double_divide(inverse(X1),X2)),
inference(forward_demodulation,[],[f922,f796]) ).
fof(f944,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,X1)),double_divide(X0,inverse(X2))) = inverse(double_divide(double_divide(sF8,sF7),double_divide(X1,X2))),
inference(forward_demodulation,[],[f927,f796]) ).
fof(f954,plain,
! [X1] : inverse(double_divide(double_divide(sF8,sF7),X1)) = X1,
inference(forward_demodulation,[],[f940,f796]) ).
fof(f955,plain,
! [X2,X1] : inverse(double_divide(double_divide(sF8,sF7),double_divide(X1,X2))) = double_divide(double_divide(sF8,sF7),double_divide(inverse(X1),inverse(X2))),
inference(forward_demodulation,[],[f944,f942]) ).
fof(f958,plain,
! [X2,X1] : double_divide(X1,X2) = double_divide(double_divide(sF8,sF7),double_divide(inverse(X1),inverse(X2))),
inference(forward_demodulation,[],[f955,f954]) ).
fof(f996,plain,
! [X0] : double_divide(inverse(X0),X0) = double_divide(sF0,a1),
inference(superposition,[],[f823,f7]) ).
fof(f997,plain,
! [X0] : double_divide(inverse(X0),X0) = double_divide(sF3,b1),
inference(superposition,[],[f823,f13]) ).
fof(f998,plain,
! [X0] : double_divide(inverse(X0),X0) = double_divide(sF6,b2),
inference(superposition,[],[f823,f19]) ).
fof(f1001,plain,
! [X0] : double_divide(sF8,sF7) = double_divide(inverse(X0),X0),
inference(superposition,[],[f823,f23]) ).
fof(f1064,plain,
! [X0,X1] : inverse(double_divide(X1,double_divide(inverse(X0),X0))) = X1,
inference(superposition,[],[f107,f823]) ).
fof(f1156,plain,
double_divide(sF8,sF7) = double_divide(sF6,b2),
inference(forward_demodulation,[],[f998,f1001]) ).
fof(f1157,plain,
double_divide(sF8,sF7) = double_divide(sF3,b1),
inference(forward_demodulation,[],[f997,f1001]) ).
fof(f1158,plain,
double_divide(sF8,sF7) = double_divide(sF0,a1),
inference(forward_demodulation,[],[f996,f1001]) ).
fof(f1222,plain,
double_divide(sF3,b1) = double_divide(sF6,b2),
inference(forward_demodulation,[],[f1157,f1156]) ).
fof(f1223,plain,
double_divide(sF0,a1) = double_divide(sF6,b2),
inference(forward_demodulation,[],[f1158,f1156]) ).
fof(f1250,plain,
double_divide(sF0,a1) = double_divide(sF3,b1),
inference(forward_demodulation,[],[f1223,f1222]) ).
fof(f1311,plain,
! [X0] : inverse(double_divide(X0,double_divide(sF0,a1))) = X0,
inference(superposition,[],[f1064,f7]) ).
fof(f1336,plain,
! [X2,X0,X1] : inverse(double_divide(inverse(double_divide(X0,X1)),double_divide(X0,X2))) = inverse(double_divide(inverse(X2),X1)),
inference(superposition,[],[f1064,f204]) ).
fof(f1358,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(X0,inverse(double_divide(double_divide(inverse(X1),X1),X2)))) = X2,
inference(superposition,[],[f218,f1064]) ).
fof(f1367,plain,
! [X0,X1] : inverse(double_divide(sF8,sF7)) = double_divide(X0,double_divide(X0,double_divide(inverse(X1),X1))),
inference(superposition,[],[f715,f1064]) ).
fof(f1368,plain,
! [X0] : inverse(double_divide(sF8,sF7)) = double_divide(X0,double_divide(X0,double_divide(sF8,sF7))),
inference(forward_demodulation,[],[f1367,f1001]) ).
fof(f1374,plain,
! [X2,X0] : double_divide(X0,double_divide(X0,inverse(double_divide(double_divide(sF8,sF7),X2)))) = X2,
inference(forward_demodulation,[],[f1358,f1001]) ).
fof(f1387,plain,
! [X2,X1] : inverse(double_divide(inverse(X2),X1)) = inverse(double_divide(double_divide(sF8,sF7),double_divide(inverse(X1),X2))),
inference(forward_demodulation,[],[f1336,f942]) ).
fof(f1413,plain,
! [X0] : inverse(double_divide(sF6,b2)) = double_divide(X0,double_divide(X0,double_divide(sF6,b2))),
inference(forward_demodulation,[],[f1368,f1156]) ).
fof(f1418,plain,
! [X2,X0] : double_divide(X0,double_divide(X0,X2)) = X2,
inference(forward_demodulation,[],[f1374,f954]) ).
fof(f1426,plain,
! [X2,X1] : inverse(double_divide(inverse(X2),X1)) = double_divide(inverse(X1),X2),
inference(forward_demodulation,[],[f1387,f954]) ).
fof(f1445,plain,
! [X0] : inverse(double_divide(sF3,b1)) = double_divide(X0,double_divide(X0,double_divide(sF3,b1))),
inference(forward_demodulation,[],[f1413,f1222]) ).
fof(f1471,plain,
double_divide(sF3,b1) = inverse(double_divide(sF3,b1)),
inference(forward_demodulation,[],[f1445,f1418]) ).
fof(f1495,plain,
double_divide(sF0,a1) = inverse(double_divide(sF0,a1)),
inference(forward_demodulation,[],[f1471,f1250]) ).
fof(f1523,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X1,X2)),X0) = double_divide(X1,inverse(double_divide(X2,X0))),
inference(superposition,[],[f1418,f218]) ).
fof(f1544,plain,
! [X2,X0,X1] : inverse(double_divide(inverse(double_divide(X0,X2)),X1)) = inverse(double_divide(X2,inverse(double_divide(X0,X1)))),
inference(superposition,[],[f70,f1418]) ).
fof(f1545,plain,
! [X2,X0,X1] : inverse(double_divide(inverse(double_divide(X1,inverse(double_divide(X2,X0)))),double_divide(X1,X0))) = X2,
inference(superposition,[],[f1,f1418]) ).
fof(f1548,plain,
! [X2,X0,X1] : double_divide(X1,X0) = inverse(double_divide(inverse(double_divide(inverse(X0),X2)),double_divide(X1,X2))),
inference(superposition,[],[f92,f1418]) ).
fof(f1557,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X1,X2)),double_divide(X1,double_divide(X3,X0))) = double_divide(inverse(double_divide(X3,X2)),X0),
inference(superposition,[],[f204,f1418]) ).
fof(f1572,plain,
! [X2,X3,X0] : double_divide(inverse(double_divide(X3,X2)),X0) = double_divide(double_divide(sF8,sF7),double_divide(inverse(X2),double_divide(X3,X0))),
inference(forward_demodulation,[],[f1557,f942]) ).
fof(f1579,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(inverse(double_divide(inverse(inverse(X0)),X1)),double_divide(sF8,sF7)),
inference(forward_demodulation,[],[f1548,f926]) ).
fof(f1582,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X1,X0)),double_divide(X1,inverse(double_divide(X2,X0)))) = X2,
inference(forward_demodulation,[],[f1545,f1426]) ).
fof(f1583,plain,
! [X2,X0,X1] : inverse(double_divide(X2,inverse(double_divide(X0,X1)))) = double_divide(inverse(X1),double_divide(X0,X2)),
inference(forward_demodulation,[],[f1544,f1426]) ).
fof(f1595,plain,
! [X2,X3,X0] : double_divide(inverse(double_divide(X3,X2)),X0) = double_divide(double_divide(sF6,b2),double_divide(inverse(X2),double_divide(X3,X0))),
inference(forward_demodulation,[],[f1572,f1156]) ).
fof(f1602,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(inverse(inverse(X0)),inverse(double_divide(X1,double_divide(sF8,sF7)))),
inference(forward_demodulation,[],[f1579,f1523]) ).
fof(f1605,plain,
! [X2,X0] : double_divide(double_divide(sF8,sF7),double_divide(inverse(X0),inverse(double_divide(X2,X0)))) = X2,
inference(forward_demodulation,[],[f1582,f942]) ).
fof(f1614,plain,
! [X2,X3,X0] : double_divide(inverse(double_divide(X3,X2)),X0) = double_divide(double_divide(sF3,b1),double_divide(inverse(X2),double_divide(X3,X0))),
inference(forward_demodulation,[],[f1595,f1222]) ).
fof(f1621,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(inverse(inverse(X0)),inverse(double_divide(X1,double_divide(sF6,b2)))),
inference(forward_demodulation,[],[f1602,f1156]) ).
fof(f1624,plain,
! [X2,X0] : double_divide(X0,double_divide(X2,X0)) = X2,
inference(forward_demodulation,[],[f1605,f958]) ).
fof(f1631,plain,
! [X2,X3,X0] : double_divide(inverse(double_divide(X3,X2)),X0) = double_divide(double_divide(sF0,a1),double_divide(inverse(X2),double_divide(X3,X0))),
inference(forward_demodulation,[],[f1614,f1250]) ).
fof(f1638,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(inverse(inverse(X0)),inverse(double_divide(X1,double_divide(sF3,b1)))),
inference(forward_demodulation,[],[f1621,f1222]) ).
fof(f1647,plain,
! [X2,X3,X0] : double_divide(X3,inverse(double_divide(X2,X0))) = double_divide(double_divide(sF0,a1),double_divide(inverse(X2),double_divide(X3,X0))),
inference(forward_demodulation,[],[f1631,f1523]) ).
fof(f1654,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(inverse(inverse(X0)),inverse(double_divide(X1,double_divide(sF0,a1)))),
inference(forward_demodulation,[],[f1638,f1250]) ).
fof(f1662,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(inverse(inverse(X0)),X1),
inference(forward_demodulation,[],[f1654,f1311]) ).
fof(f1667,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X0),X1) = double_divide(X1,double_divide(inverse(double_divide(inverse(double_divide(X2,X0)),X3)),double_divide(X2,X3))),
inference(superposition,[],[f1662,f92]) ).
fof(f1700,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X2,inverse(inverse(X1)))),double_divide(X2,X3)) = inverse(double_divide(inverse(double_divide(X3,X0)),double_divide(X0,X1))),
inference(superposition,[],[f155,f1662]) ).
fof(f1707,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X2,X0)),double_divide(X2,X3)) = double_divide(inverse(double_divide(X0,X1)),double_divide(inverse(inverse(X1)),X3)),
inference(superposition,[],[f204,f1662]) ).
fof(f1720,plain,
! [X0,X1] : inverse(double_divide(double_divide(inverse(X0),X0),X1)) = inverse(inverse(X1)),
inference(superposition,[],[f1064,f1662]) ).
fof(f1721,plain,
! [X0,X1] : double_divide(double_divide(inverse(inverse(X0)),X1),X0) = X1,
inference(superposition,[],[f1418,f1662]) ).
fof(f1736,plain,
! [X0,X1] : double_divide(double_divide(X1,X0),X0) = X1,
inference(forward_demodulation,[],[f1721,f1662]) ).
fof(f1737,plain,
! [X1] : inverse(double_divide(double_divide(sF8,sF7),X1)) = inverse(inverse(X1)),
inference(forward_demodulation,[],[f1720,f1001]) ).
fof(f1749,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X2,X0)),double_divide(X2,X3)) = double_divide(X0,inverse(double_divide(X1,double_divide(inverse(inverse(X1)),X3)))),
inference(forward_demodulation,[],[f1707,f1523]) ).
fof(f1756,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X2,inverse(inverse(X1)))),double_divide(X2,X3)) = double_divide(inverse(double_divide(X0,X1)),double_divide(X3,X0)),
inference(forward_demodulation,[],[f1700,f1426]) ).
fof(f1769,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X0),X1) = double_divide(X1,double_divide(inverse(double_divide(X2,X0)),inverse(double_divide(X3,double_divide(X2,X3))))),
inference(forward_demodulation,[],[f1667,f1523]) ).
fof(f1778,plain,
! [X1] : inverse(inverse(X1)) = X1,
inference(forward_demodulation,[],[f1737,f954]) ).
fof(f1789,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X2,X0)),double_divide(X2,X3)) = double_divide(X0,inverse(double_divide(X1,double_divide(X3,X1)))),
inference(forward_demodulation,[],[f1749,f1662]) ).
fof(f1796,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X2,inverse(inverse(X1)))),double_divide(X2,X3)) = double_divide(X0,inverse(double_divide(X1,double_divide(X3,X0)))),
inference(forward_demodulation,[],[f1756,f1523]) ).
fof(f1808,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X0),X1) = double_divide(X1,double_divide(X2,inverse(double_divide(X0,inverse(double_divide(X3,double_divide(X2,X3))))))),
inference(forward_demodulation,[],[f1769,f1523]) ).
fof(f1825,plain,
! [X2,X3,X0] : double_divide(inverse(double_divide(X2,X0)),double_divide(X2,X3)) = double_divide(X0,inverse(X3)),
inference(forward_demodulation,[],[f1789,f1624]) ).
fof(f1832,plain,
! [X3,X0,X1] : double_divide(X0,inverse(double_divide(X1,double_divide(X3,X0)))) = inverse(double_divide(X3,inverse(X1))),
inference(forward_demodulation,[],[f1796,f895]) ).
fof(f1842,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X0),X1) = double_divide(X1,double_divide(X2,double_divide(inverse(double_divide(X2,X3)),double_divide(X3,X0)))),
inference(forward_demodulation,[],[f1808,f1583]) ).
fof(f1850,plain,
! [X3,X0] : double_divide(X0,inverse(X3)) = double_divide(double_divide(sF8,sF7),double_divide(inverse(X0),X3)),
inference(forward_demodulation,[],[f1825,f942]) ).
fof(f1866,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X0),X1) = double_divide(X1,double_divide(X2,double_divide(X2,inverse(double_divide(X3,double_divide(X3,X0)))))),
inference(forward_demodulation,[],[f1842,f1523]) ).
fof(f1868,plain,
! [X3,X0] : double_divide(X0,inverse(X3)) = double_divide(double_divide(sF6,b2),double_divide(inverse(X0),X3)),
inference(forward_demodulation,[],[f1850,f1156]) ).
fof(f1877,plain,
! [X3,X0,X1] : double_divide(inverse(X0),X1) = double_divide(X1,inverse(double_divide(X3,double_divide(X3,X0)))),
inference(forward_demodulation,[],[f1866,f1418]) ).
fof(f1878,plain,
! [X3,X0] : double_divide(X0,inverse(X3)) = double_divide(double_divide(sF3,b1),double_divide(inverse(X0),X3)),
inference(forward_demodulation,[],[f1868,f1222]) ).
fof(f1886,plain,
! [X0,X1] : double_divide(X1,inverse(X0)) = double_divide(inverse(X0),X1),
inference(forward_demodulation,[],[f1877,f1418]) ).
fof(f1887,plain,
! [X3,X0] : double_divide(X0,inverse(X3)) = double_divide(double_divide(sF0,a1),double_divide(inverse(X0),X3)),
inference(forward_demodulation,[],[f1878,f1250]) ).
fof(f1913,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(X0,X1),
inference(superposition,[],[f1886,f1064]) ).
fof(f1948,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(inverse(X0),X1)),double_divide(X1,X2)) = inverse(double_divide(inverse(double_divide(X2,X3)),double_divide(inverse(X0),X3))),
inference(superposition,[],[f155,f1886]) ).
fof(f1954,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X2,inverse(X0))),double_divide(X2,X3)) = double_divide(inverse(double_divide(inverse(X0),X1)),double_divide(X1,X3)),
inference(superposition,[],[f204,f1886]) ).
fof(f1985,plain,
! [X0,X1] : double_divide(inverse(X1),X1) = double_divide(X0,inverse(X0)),
inference(superposition,[],[f823,f1886]) ).
fof(f2000,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X2,X3)),double_divide(X2,X0)) = double_divide(inverse(double_divide(inverse(X1),X3)),double_divide(X0,inverse(X1))),
inference(superposition,[],[f204,f1886]) ).
fof(f2014,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X2),X0)),double_divide(inverse(double_divide(X0,X1)),inverse(X2))) = X1,
inference(superposition,[],[f218,f1886]) ).
fof(f2023,plain,
! [X2,X0,X1] : double_divide(inverse(X2),inverse(double_divide(X0,double_divide(inverse(double_divide(X0,X1)),inverse(X2))))) = X1,
inference(forward_demodulation,[],[f2014,f1523]) ).
fof(f2035,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X2,X3)),double_divide(X2,X0)) = double_divide(inverse(X1),inverse(double_divide(X3,double_divide(X0,inverse(X1))))),
inference(forward_demodulation,[],[f2000,f1523]) ).
fof(f2049,plain,
! [X0] : double_divide(sF8,sF7) = double_divide(X0,inverse(X0)),
inference(forward_demodulation,[],[f1985,f1001]) ).
fof(f2074,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X2,inverse(X0))),double_divide(X2,X3)) = double_divide(inverse(X0),inverse(double_divide(X1,double_divide(X1,X3)))),
inference(forward_demodulation,[],[f1954,f1523]) ).
fof(f2080,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X0),X1)),double_divide(X1,X2)) = double_divide(inverse(double_divide(inverse(X2),inverse(X0))),double_divide(sF8,sF7)),
inference(forward_demodulation,[],[f1948,f926]) ).
fof(f2108,plain,
! [X0,X1] : inverse(double_divide(inverse(double_divide(X0,X1)),inverse(X0))) = X1,
inference(forward_demodulation,[],[f2023,f1832]) ).
fof(f2118,plain,
! [X2,X3,X0] : double_divide(inverse(double_divide(X2,X3)),double_divide(X2,X0)) = inverse(double_divide(X0,inverse(X3))),
inference(forward_demodulation,[],[f2035,f1832]) ).
fof(f2131,plain,
! [X0] : double_divide(sF6,b2) = double_divide(X0,inverse(X0)),
inference(forward_demodulation,[],[f2049,f1156]) ).
fof(f2149,plain,
! [X2,X3,X0] : double_divide(inverse(double_divide(X2,inverse(X0))),double_divide(X2,X3)) = double_divide(inverse(X0),inverse(X3)),
inference(forward_demodulation,[],[f2074,f1418]) ).
fof(f2155,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X0),X1)),double_divide(X1,X2)) = double_divide(inverse(X2),inverse(double_divide(inverse(X0),double_divide(sF8,sF7)))),
inference(forward_demodulation,[],[f2080,f1523]) ).
fof(f2174,plain,
! [X0,X1] : double_divide(inverse(inverse(X0)),double_divide(X0,X1)) = X1,
inference(forward_demodulation,[],[f2108,f1426]) ).
fof(f2183,plain,
! [X3,X0] : double_divide(double_divide(sF8,sF7),double_divide(inverse(X3),X0)) = inverse(double_divide(X0,inverse(X3))),
inference(forward_demodulation,[],[f2118,f942]) ).
fof(f2196,plain,
! [X0] : double_divide(sF3,b1) = double_divide(X0,inverse(X0)),
inference(forward_demodulation,[],[f2131,f1222]) ).
fof(f2211,plain,
! [X3,X0] : inverse(double_divide(X3,X0)) = double_divide(inverse(X0),inverse(X3)),
inference(forward_demodulation,[],[f2149,f895]) ).
fof(f2217,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X0),X1)),double_divide(X1,X2)) = double_divide(inverse(X2),double_divide(inverse(double_divide(sF8,sF7)),X0)),
inference(forward_demodulation,[],[f2155,f1426]) ).
fof(f2236,plain,
! [X0,X1] : double_divide(double_divide(X0,X1),X0) = X1,
inference(forward_demodulation,[],[f2174,f1662]) ).
fof(f2239,plain,
! [X3,X0] : double_divide(double_divide(sF6,b2),double_divide(inverse(X3),X0)) = inverse(double_divide(X0,inverse(X3))),
inference(forward_demodulation,[],[f2183,f1156]) ).
fof(f2250,plain,
! [X0] : double_divide(sF0,a1) = double_divide(X0,inverse(X0)),
inference(forward_demodulation,[],[f2196,f1250]) ).
fof(f2268,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(inverse(X0),X1)),double_divide(X1,X2)) = double_divide(inverse(X2),double_divide(sF8,inverse(double_divide(sF7,X0)))),
inference(forward_demodulation,[],[f2217,f1523]) ).
fof(f2289,plain,
! [X3,X0] : double_divide(double_divide(sF3,b1),double_divide(inverse(X3),X0)) = inverse(double_divide(X0,inverse(X3))),
inference(forward_demodulation,[],[f2239,f1222]) ).
fof(f2313,plain,
! [X2,X0,X1] : double_divide(inverse(X0),inverse(double_divide(X1,double_divide(X1,X2)))) = double_divide(inverse(X2),double_divide(sF8,inverse(double_divide(sF7,X0)))),
inference(forward_demodulation,[],[f2268,f1523]) ).
fof(f2324,plain,
! [X3,X0] : double_divide(double_divide(sF0,a1),double_divide(inverse(X3),X0)) = inverse(double_divide(X0,inverse(X3))),
inference(forward_demodulation,[],[f2289,f1250]) ).
fof(f2340,plain,
! [X2,X0,X1] : double_divide(inverse(X2),double_divide(sF8,inverse(double_divide(sF7,X0)))) = inverse(double_divide(double_divide(X1,double_divide(X1,X2)),X0)),
inference(forward_demodulation,[],[f2313,f2211]) ).
fof(f2345,plain,
! [X3,X0] : double_divide(X3,inverse(X0)) = inverse(double_divide(X0,inverse(X3))),
inference(forward_demodulation,[],[f2324,f1887]) ).
fof(f2355,plain,
! [X2,X0] : inverse(double_divide(X2,X0)) = double_divide(inverse(X2),double_divide(sF8,inverse(double_divide(sF7,X0)))),
inference(forward_demodulation,[],[f2340,f1418]) ).
fof(f2495,plain,
! [X2,X3,X0,X1] : inverse(double_divide(inverse(double_divide(X0,X3)),X1)) = inverse(double_divide(X2,inverse(double_divide(X3,double_divide(double_divide(X0,X1),X2))))),
inference(superposition,[],[f70,f1913]) ).
fof(f2522,plain,
sF1 = double_divide(sF0,a1),
inference(superposition,[],[f9,f1913]) ).
fof(f2524,plain,
sF7 = double_divide(sF6,b2),
inference(superposition,[],[f21,f1913]) ).
fof(f2529,plain,
double_divide(a4,b4) = sF19,
inference(superposition,[],[f45,f1913]) ).
fof(f2532,plain,
sF19 = sF21,
inference(forward_demodulation,[],[f2529,f49]) ).
fof(f2533,plain,
sF7 = double_divide(sF3,b1),
inference(forward_demodulation,[],[f2524,f1222]) ).
fof(f2558,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(double_divide(X0,X1),X2)),double_divide(X3,X2)) = inverse(double_divide(inverse(double_divide(X0,X3)),X1)),
inference(forward_demodulation,[],[f2495,f1583]) ).
fof(f2656,plain,
sF7 = double_divide(sF0,a1),
inference(forward_demodulation,[],[f2533,f1250]) ).
fof(f2675,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(double_divide(X0,X1),X2)),double_divide(X3,X2)) = double_divide(inverse(X1),double_divide(X0,X3)),
inference(forward_demodulation,[],[f2558,f1426]) ).
fof(f2754,plain,
sF1 = sF7,
inference(forward_demodulation,[],[f2656,f2522]) ).
fof(f2766,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X1),double_divide(X0,X3)) = double_divide(double_divide(X0,X1),inverse(double_divide(X2,double_divide(X3,X2)))),
inference(forward_demodulation,[],[f2675,f1523]) ).
fof(f2844,plain,
! [X3,X0,X1] : double_divide(inverse(X1),double_divide(X0,X3)) = double_divide(double_divide(X0,X1),inverse(X3)),
inference(forward_demodulation,[],[f2766,f1624]) ).
fof(f3032,plain,
! [X0,X1] : inverse(X1) = double_divide(X1,double_divide(inverse(X0),X0)),
inference(superposition,[],[f1624,f823]) ).
fof(f3071,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(X3,X2)),X0) = double_divide(inverse(double_divide(X1,X2)),double_divide(X1,double_divide(X0,X3))),
inference(superposition,[],[f204,f1624]) ).
fof(f3106,plain,
! [X2,X3,X0] : double_divide(inverse(double_divide(X3,X2)),X0) = double_divide(double_divide(sF8,sF7),double_divide(inverse(X2),double_divide(X0,X3))),
inference(forward_demodulation,[],[f3071,f942]) ).
fof(f3135,plain,
! [X1] : inverse(X1) = double_divide(X1,double_divide(sF8,sF7)),
inference(forward_demodulation,[],[f3032,f1001]) ).
fof(f3159,plain,
! [X2,X3,X0] : double_divide(inverse(double_divide(X3,X2)),X0) = double_divide(double_divide(sF6,b2),double_divide(inverse(X2),double_divide(X0,X3))),
inference(forward_demodulation,[],[f3106,f1156]) ).
fof(f3181,plain,
! [X1] : inverse(X1) = double_divide(X1,double_divide(sF6,b2)),
inference(forward_demodulation,[],[f3135,f1156]) ).
fof(f3194,plain,
! [X2,X3,X0] : double_divide(inverse(double_divide(X3,X2)),X0) = double_divide(double_divide(sF3,b1),double_divide(inverse(X2),double_divide(X0,X3))),
inference(forward_demodulation,[],[f3159,f1222]) ).
fof(f3208,plain,
! [X1] : inverse(X1) = double_divide(X1,double_divide(sF3,b1)),
inference(forward_demodulation,[],[f3181,f1222]) ).
fof(f3217,plain,
! [X2,X3,X0] : double_divide(inverse(double_divide(X3,X2)),X0) = double_divide(double_divide(sF0,a1),double_divide(inverse(X2),double_divide(X0,X3))),
inference(forward_demodulation,[],[f3194,f1250]) ).
fof(f3230,plain,
! [X1] : inverse(X1) = double_divide(X1,double_divide(sF0,a1)),
inference(forward_demodulation,[],[f3208,f1250]) ).
fof(f3237,plain,
! [X2,X3,X0] : double_divide(X0,inverse(double_divide(X2,X3))) = double_divide(inverse(double_divide(X3,X2)),X0),
inference(forward_demodulation,[],[f3217,f1647]) ).
fof(f3249,plain,
! [X1] : inverse(X1) = double_divide(X1,sF1),
inference(forward_demodulation,[],[f3230,f2522]) ).
fof(f3255,plain,
! [X2,X3,X0] : double_divide(X3,inverse(double_divide(X2,X0))) = double_divide(X0,inverse(double_divide(X2,X3))),
inference(forward_demodulation,[],[f3237,f1523]) ).
fof(f3325,plain,
! [X2,X0,X1] : double_divide(X0,inverse(double_divide(X1,X2))) = double_divide(X2,inverse(double_divide(X0,X1))),
inference(superposition,[],[f3255,f1913]) ).
fof(f3344,plain,
! [X0] : double_divide(X0,inverse(sF11)) = double_divide(a3,inverse(double_divide(b3,X0))),
inference(superposition,[],[f3255,f29]) ).
fof(f3345,plain,
! [X0] : double_divide(X0,inverse(sF15)) = double_divide(b3,inverse(double_divide(c3,X0))),
inference(superposition,[],[f3255,f37]) ).
fof(f3426,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X1,X0)),X2) = double_divide(X0,inverse(double_divide(X1,X2))),
inference(superposition,[],[f1913,f3255]) ).
fof(f3443,plain,
! [X2,X0,X1] : double_divide(X0,inverse(double_divide(X1,X2))) = double_divide(X1,inverse(double_divide(X0,X2))),
inference(forward_demodulation,[],[f3426,f1523]) ).
fof(f3520,plain,
! [X0] : double_divide(X0,sF16) = double_divide(b3,inverse(double_divide(c3,X0))),
inference(forward_demodulation,[],[f3345,f39]) ).
fof(f3521,plain,
! [X0] : double_divide(X0,sF12) = double_divide(a3,inverse(double_divide(b3,X0))),
inference(forward_demodulation,[],[f3344,f31]) ).
fof(f4188,plain,
sF7 = inverse(sF8),
inference(superposition,[],[f1778,f23]) ).
fof(f4207,plain,
sF1 = inverse(sF8),
inference(forward_demodulation,[],[f4188,f2754]) ).
fof(f4258,plain,
inverse(sF19) = sF22,
inference(superposition,[],[f51,f2532]) ).
fof(f4259,plain,
sF20 = sF22,
inference(forward_demodulation,[],[f4258,f47]) ).
fof(f4260,plain,
( $false
| spl23_1 ),
inference(forward_subsumption_resolution,[],[f4259,f56]) ).
fof(f4261,plain,
spl23_1,
inference(avatar_contradiction_clause,[],[f4260]) ).
fof(f4566,plain,
! [X0] : double_divide(X0,inverse(sF13)) = double_divide(c3,inverse(double_divide(X0,sF12))),
inference(superposition,[],[f3443,f33]) ).
fof(f4576,plain,
! [X0,X1] : double_divide(X1,double_divide(inverse(X0),X0)) = double_divide(sF8,inverse(double_divide(X1,sF7))),
inference(superposition,[],[f3443,f715]) ).
fof(f4658,plain,
! [X2,X0,X1] : double_divide(inverse(double_divide(X0,X2)),X1) = double_divide(X0,inverse(double_divide(X1,X2))),
inference(superposition,[],[f1913,f3443]) ).
fof(f4679,plain,
! [X2,X0,X1] : double_divide(X0,inverse(double_divide(X1,X2))) = double_divide(X0,inverse(double_divide(X2,X1))),
inference(forward_demodulation,[],[f4658,f1523]) ).
fof(f4751,plain,
! [X0,X1] : double_divide(X1,double_divide(inverse(X0),X0)) = double_divide(sF8,inverse(double_divide(X1,sF1))),
inference(forward_demodulation,[],[f4576,f2754]) ).
fof(f4761,plain,
! [X0] : double_divide(X0,sF14) = double_divide(c3,inverse(double_divide(X0,sF12))),
inference(forward_demodulation,[],[f4566,f35]) ).
fof(f4903,plain,
! [X0,X1] : double_divide(X1,double_divide(inverse(X0),X0)) = double_divide(sF8,inverse(inverse(X1))),
inference(forward_demodulation,[],[f4751,f3249]) ).
fof(f5022,plain,
! [X0,X1] : double_divide(sF8,X1) = double_divide(X1,double_divide(inverse(X0),X0)),
inference(forward_demodulation,[],[f4903,f1778]) ).
fof(f5107,plain,
! [X1] : double_divide(sF8,X1) = double_divide(X1,double_divide(sF8,sF7)),
inference(forward_demodulation,[],[f5022,f1001]) ).
fof(f5181,plain,
! [X1] : double_divide(sF8,X1) = double_divide(X1,double_divide(sF6,b2)),
inference(forward_demodulation,[],[f5107,f1156]) ).
fof(f5247,plain,
! [X1] : double_divide(sF8,X1) = double_divide(X1,double_divide(sF3,b1)),
inference(forward_demodulation,[],[f5181,f1222]) ).
fof(f5313,plain,
! [X1] : double_divide(sF8,X1) = double_divide(X1,double_divide(sF0,a1)),
inference(forward_demodulation,[],[f5247,f1250]) ).
fof(f5367,plain,
! [X1] : double_divide(sF8,X1) = double_divide(X1,sF1),
inference(forward_demodulation,[],[f5313,f2522]) ).
fof(f5409,plain,
! [X1] : double_divide(sF8,X1) = inverse(X1),
inference(forward_demodulation,[],[f5367,f3249]) ).
fof(f5547,plain,
! [X0] : inverse(X0) = double_divide(X0,sF8),
inference(superposition,[],[f1913,f5409]) ).
fof(f5567,plain,
inverse(sF1) = inverse(sF8),
inference(superposition,[],[f3249,f5409]) ).
fof(f5574,plain,
sF1 = inverse(sF1),
inference(forward_demodulation,[],[f5567,f4207]) ).
fof(f5623,plain,
sF1 = sF2,
inference(forward_demodulation,[],[f5574,f11]) ).
fof(f5840,plain,
! [X0] : double_divide(X0,inverse(sF4)) = double_divide(X0,inverse(double_divide(sF3,b1))),
inference(superposition,[],[f4679,f15]) ).
fof(f6057,plain,
! [X0] : double_divide(X0,inverse(sF4)) = double_divide(X0,inverse(double_divide(sF0,a1))),
inference(forward_demodulation,[],[f5840,f1250]) ).
fof(f6191,plain,
! [X0] : double_divide(X0,inverse(sF4)) = double_divide(X0,double_divide(sF0,a1)),
inference(forward_demodulation,[],[f6057,f1495]) ).
fof(f6305,plain,
! [X0] : double_divide(X0,sF1) = double_divide(X0,inverse(sF4)),
inference(forward_demodulation,[],[f6191,f2522]) ).
fof(f6393,plain,
! [X0] : double_divide(X0,sF1) = double_divide(X0,sF5),
inference(forward_demodulation,[],[f6305,f17]) ).
fof(f6465,plain,
! [X0] : inverse(X0) = double_divide(X0,sF5),
inference(forward_demodulation,[],[f6393,f3249]) ).
fof(f6790,plain,
! [X0] : sF5 = double_divide(X0,inverse(X0)),
inference(superposition,[],[f1418,f6465]) ).
fof(f6823,plain,
sF5 = double_divide(sF0,a1),
inference(forward_demodulation,[],[f6790,f2250]) ).
fof(f6860,plain,
sF1 = sF5,
inference(forward_demodulation,[],[f6823,f2522]) ).
fof(f10271,plain,
! [X0] : double_divide(X0,inverse(sF17)) = double_divide(a3,inverse(double_divide(X0,sF16))),
inference(superposition,[],[f3325,f41]) ).
fof(f10336,plain,
! [X0] : double_divide(a2,inverse(double_divide(sF8,X0))) = double_divide(X0,inverse(sF9)),
inference(superposition,[],[f3325,f25]) ).
fof(f10607,plain,
! [X0] : double_divide(a2,inverse(double_divide(sF8,X0))) = double_divide(X0,sF10),
inference(forward_demodulation,[],[f10336,f27]) ).
fof(f10660,plain,
! [X0] : double_divide(X0,sF18) = double_divide(a3,inverse(double_divide(X0,sF16))),
inference(forward_demodulation,[],[f10271,f43]) ).
fof(f10803,plain,
! [X0] : double_divide(X0,sF10) = double_divide(a2,inverse(inverse(X0))),
inference(forward_demodulation,[],[f10607,f5409]) ).
fof(f10960,plain,
! [X0] : double_divide(a2,X0) = double_divide(X0,sF10),
inference(forward_demodulation,[],[f10803,f1778]) ).
fof(f11539,plain,
! [X0] : sF10 = double_divide(double_divide(a2,X0),X0),
inference(superposition,[],[f2236,f10960]) ).
fof(f11574,plain,
a2 = sF10,
inference(forward_demodulation,[],[f11539,f1736]) ).
fof(f11643,plain,
spl23_3,
inference(avatar_split_clause,[],[f11574,f62]) ).
fof(f21252,plain,
! [X0] : double_divide(sF13,inverse(X0)) = inverse(double_divide(X0,sF14)),
inference(superposition,[],[f2345,f35]) ).
fof(f23799,plain,
! [X0] : double_divide(inverse(double_divide(c3,X0)),sF12) = double_divide(a3,inverse(double_divide(X0,sF16))),
inference(superposition,[],[f3521,f3520]) ).
fof(f23947,plain,
! [X0] : double_divide(inverse(double_divide(c3,X0)),sF12) = double_divide(X0,sF18),
inference(forward_demodulation,[],[f23799,f10660]) ).
fof(f24000,plain,
! [X0] : double_divide(X0,sF18) = double_divide(c3,inverse(double_divide(X0,sF12))),
inference(forward_demodulation,[],[f23947,f1523]) ).
fof(f24047,plain,
! [X0] : double_divide(X0,sF14) = double_divide(X0,sF18),
inference(forward_demodulation,[],[f24000,f4761]) ).
fof(f24143,plain,
! [X0,X1] : sF18 = inverse(double_divide(inverse(double_divide(inverse(double_divide(X0,sF14)),X1)),double_divide(X0,X1))),
inference(superposition,[],[f92,f24047]) ).
fof(f24261,plain,
! [X0] : sF18 = double_divide(inverse(double_divide(inverse(inverse(double_divide(X0,sF14))),X0)),double_divide(sF8,sF7)),
inference(forward_demodulation,[],[f24143,f926]) ).
fof(f24322,plain,
! [X0] : sF18 = double_divide(inverse(inverse(double_divide(X0,sF14))),inverse(double_divide(X0,double_divide(sF8,sF7)))),
inference(forward_demodulation,[],[f24261,f1523]) ).
fof(f24360,plain,
! [X0] : sF18 = double_divide(inverse(double_divide(X0,double_divide(sF8,sF7))),double_divide(X0,sF14)),
inference(forward_demodulation,[],[f24322,f1662]) ).
fof(f24387,plain,
sF18 = double_divide(double_divide(sF8,sF7),double_divide(inverse(double_divide(sF8,sF7)),sF14)),
inference(forward_demodulation,[],[f24360,f942]) ).
fof(f24409,plain,
sF18 = double_divide(double_divide(sF8,sF7),double_divide(sF8,inverse(double_divide(sF7,sF14)))),
inference(forward_demodulation,[],[f24387,f1523]) ).
fof(f24427,plain,
sF18 = double_divide(double_divide(sF8,sF7),inverse(inverse(double_divide(sF7,sF14)))),
inference(forward_demodulation,[],[f24409,f5409]) ).
fof(f24443,plain,
sF18 = double_divide(inverse(sF7),double_divide(sF8,inverse(double_divide(sF7,sF14)))),
inference(forward_demodulation,[],[f24427,f2844]) ).
fof(f24456,plain,
sF18 = inverse(double_divide(sF7,sF14)),
inference(forward_demodulation,[],[f24443,f2355]) ).
fof(f24469,plain,
sF18 = double_divide(sF13,inverse(sF7)),
inference(forward_demodulation,[],[f24456,f21252]) ).
fof(f24482,plain,
sF18 = double_divide(sF13,sF8),
inference(forward_demodulation,[],[f24469,f23]) ).
fof(f24493,plain,
inverse(sF13) = sF18,
inference(forward_demodulation,[],[f24482,f5547]) ).
fof(f24502,plain,
sF14 = sF18,
inference(forward_demodulation,[],[f24493,f35]) ).
fof(f24509,plain,
( $false
| spl23_2 ),
inference(forward_subsumption_resolution,[],[f24502,f60]) ).
fof(f24510,plain,
spl23_2,
inference(avatar_contradiction_clause,[],[f24509]) ).
fof(f24539,plain,
( sF1 != sF2
| spl23_4 ),
inference(forward_demodulation,[],[f68,f6860]) ).
fof(f24540,plain,
( $false
| spl23_4 ),
inference(forward_subsumption_resolution,[],[f24539,f5623]) ).
fof(f24541,plain,
spl23_4,
inference(avatar_contradiction_clause,[],[f24540]) ).
cnf(s1,plain,
( ~ spl23_1
| ~ spl23_2
| ~ spl23_3
| ~ spl23_4 ),
inference(sat_conversion,[],[f69]) ).
cnf(s2,plain,
spl23_1,
inference(sat_conversion,[],[f4261]) ).
cnf(s3,plain,
spl23_3,
inference(sat_conversion,[],[f11643]) ).
cnf(s15,plain,
spl23_2,
inference(sat_conversion,[],[f24510]) ).
cnf(s16,plain,
spl23_4,
inference(sat_conversion,[],[f24541]) ).
cnf(s17,plain,
$false,
inference(rat,[],[s1,s16,s3,s15,s2]) ).
fof(f24542,plain,
$false,
inference(avatar_sat_refutation,[],[s17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP108-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n003.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 09:21:11 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 Running first-order theorem proving
% 0.16/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
% 11.29/2.33 % (240658)Input is clausal, will run a generic CNF schedule.
% 11.29/2.33 % (240676)lrs+10_1_sil=8000:sp=occurrence:random_seed=1902697748:i=107:sd=3:ss=axioms:sgt=8_3000 on theBenchmark for (3000ds/107Mi)
% 11.29/2.33 % (240676)Instruction limit reached!
% 11.29/2.33 % (240676)------------------------------
% 11.29/2.33 % (240676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.33 % (240676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.33 % (240676)CaDiCaL version: 2.1.3
% 11.29/2.33 % (240676)Termination reason: Instruction limit
% 11.29/2.33 % (240676)Termination phase: Saturation
% 11.29/2.33 % (240676)Time elapsed: 0.040 s
% 11.29/2.33 % (240676)Peak memory usage: 90 MB
% 11.29/2.33 % (240676)Instructions burned: 108 (million)
% 11.29/2.33 % (240673)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=2081693935:i=140167_3000 on theBenchmark for (3000ds/140167Mi)
% 11.29/2.33 % (240678)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=358703622:s2a=on:i=180:gtg=position_3000 on theBenchmark for (3000ds/180Mi)
% 11.29/2.33 % (240675)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2488159676:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_3000 on theBenchmark for (3000ds/137899Mi)
% 11.29/2.33 % (240677)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4055651565:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_3000 on theBenchmark for (3000ds/114Mi)
% 11.29/2.33 % (240674)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=143727171:i=132376:av=off_3000 on theBenchmark for (3000ds/132376Mi)
% 11.29/2.33 % (240679)dis-21_1_sil=8000:lcm=predicate:random_seed=1895144859:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/117Mi)
% 11.29/2.33 % (240679)Refutation not found, incomplete strategy
% 11.29/2.33 % (240679)------------------------------
% 11.29/2.33 % (240679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.33 % (240679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.33 % (240679)CaDiCaL version: 2.1.3
% 11.29/2.33 % (240679)Termination reason: Refutation not found, incomplete strategy
% 11.29/2.33 % (240679)Time elapsed: 0.002 s
% 11.29/2.33 % (240679)Peak memory usage: 88 MB
% 11.29/2.33 % (240684)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=3487723645:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.29/2.33 % (240684)Refutation not found, incomplete strategy
% 11.29/2.33 % (240684)------------------------------
% 11.29/2.33 % (240684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.33 % (240684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.33 % (240684)CaDiCaL version: 2.1.3
% 11.29/2.33 % (240684)Termination reason: Refutation not found, incomplete strategy
% 11.29/2.33 % (240684)Time elapsed: 0.001 s
% 11.29/2.33 % (240684)Peak memory usage: 88 MB
% 11.29/2.33 % (240677)Instruction limit reached!
% 11.29/2.33 % (240677)------------------------------
% 11.29/2.33 % (240677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.33 % (240677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.33 % (240677)CaDiCaL version: 2.1.3
% 11.29/2.33 % (240677)Termination reason: Instruction limit
% 11.29/2.33 % (240677)Termination phase: Saturation
% 11.29/2.33 % (240677)Time elapsed: 0.114 s
% 11.29/2.33 % (240677)Peak memory usage: 90 MB
% 11.29/2.33 % (240677)Instructions burned: 114 (million)
% 11.29/2.33 % (240678)Instruction limit reached!
% 11.29/2.33 % (240678)------------------------------
% 11.29/2.33 % (240678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.33 % (240678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.33 % (240678)CaDiCaL version: 2.1.3
% 11.29/2.33 % (240678)Termination reason: Instruction limit
% 11.29/2.33 % (240678)Termination phase: Saturation
% 11.29/2.33 % (240678)Time elapsed: 0.143 s
% 11.29/2.33 % (240678)Peak memory usage: 90 MB
% 11.29/2.33 % (240678)Instructions burned: 181 (million)
% 11.29/2.33 % (240684)------------------------------
% 11.29/2.33 % (240684)------------------------------
% 11.29/2.33 % (240693)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2133521680: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)
% 11.29/2.33 % (240693)Refutation not found, incomplete strategy
% 11.29/2.33 % (240693)------------------------------
% 11.29/2.33 % (240693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.33 % (240693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.33 % (240693)CaDiCaL version: 2.1.3
% 11.29/2.33 % (240693)Termination reason: Refutation not found, incomplete strategy
% 11.29/2.33 % (240693)Time elapsed: 0.002 s
% 11.29/2.33 % (240693)Peak memory usage: 88 MB
% 11.29/2.33 % (240694)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=183353993:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 11.29/2.33 % (240694)Refutation not found, incomplete strategy
% 11.29/2.33 % (240694)------------------------------
% 11.29/2.33 % (240694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.33 % (240694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.33 % (240694)CaDiCaL version: 2.1.3
% 11.29/2.33 % (240694)Termination reason: Refutation not found, incomplete strategy
% 11.29/2.33 % (240694)Time elapsed: 0.001 s
% 11.29/2.33 % (240694)Peak memory usage: 88 MB
% 11.29/2.33 % (240679)------------------------------
% 11.29/2.33 % (240679)------------------------------
% 11.29/2.33 % (240699)lrs+10_64_to=lpo:sil=8000:random_seed=3961031446:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 11.29/2.33 % (240699)Instruction limit reached!
% 11.29/2.33 % (240699)------------------------------
% 11.29/2.33 % (240699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.33 % (240699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.33 % (240699)CaDiCaL version: 2.1.3
% 11.29/2.33 % (240699)Termination reason: Instruction limit
% 11.29/2.33 % (240699)Termination phase: Saturation
% 11.29/2.33 % (240699)Time elapsed: 0.052 s
% 11.29/2.33 % (240699)Peak memory usage: 89 MB
% 11.29/2.33 % (240699)Instructions burned: 128 (million)
% 11.29/2.33 % (240705)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=313072477:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 11.29/2.33 % (240703)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3047418160:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 11.29/2.33 % (240693)------------------------------
% 11.29/2.33 % (240693)------------------------------
% 11.29/2.33 % (240705)Instruction limit reached!
% 11.29/2.33 % (240705)------------------------------
% 11.29/2.33 % (240705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.33 % (240705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.33 % (240705)CaDiCaL version: 2.1.3
% 11.29/2.33 % (240705)Termination reason: Instruction limit
% 11.29/2.33 % (240705)Termination phase: Saturation
% 11.29/2.33 % (240705)Time elapsed: 0.083 s
% 11.29/2.33 % (240705)Peak memory usage: 92 MB
% 11.29/2.33 % (240705)Instructions burned: 158 (million)
% 11.29/2.33 % (240694)------------------------------
% 11.29/2.33 % (240694)------------------------------
% 11.29/2.33 % (240703)Instruction limit reached!
% 11.29/2.33 % (240703)------------------------------
% 11.29/2.33 % (240703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.33 % (240703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.34 % (240703)CaDiCaL version: 2.1.3
% 11.29/2.34 % (240703)Termination reason: Instruction limit
% 11.29/2.34 % (240703)Termination phase: Saturation
% 11.29/2.34 % (240703)Time elapsed: 0.200 s
% 11.29/2.34 % (240703)Peak memory usage: 89 MB
% 11.29/2.34 % (240703)Instructions burned: 194 (million)
% 11.29/2.34 % (240716)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2287022429:i=107_2990 on theBenchmark for (2990ds/107Mi)
% 11.29/2.34 % (240716)Refutation not found, incomplete strategy
% 11.29/2.34 % (240716)------------------------------
% 11.29/2.34 % (240716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.34 % (240716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.34 % (240716)CaDiCaL version: 2.1.3
% 11.29/2.34 % (240716)Termination reason: Refutation not found, incomplete strategy
% 11.29/2.34 % (240716)Time elapsed: 0.001 s
% 11.29/2.34 % (240716)Peak memory usage: 88 MB
% 11.29/2.34 % (240713)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2265518236:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 11.29/2.34 % (240715)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1488312774:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 11.29/2.34 % (240715)Instruction limit reached!
% 11.29/2.34 % (240715)------------------------------
% 11.29/2.34 % (240715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.34 % (240715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.34 % (240715)CaDiCaL version: 2.1.3
% 11.29/2.34 % (240715)Termination reason: Instruction limit
% 11.29/2.34 % (240715)Termination phase: Saturation
% 11.29/2.34 % (240715)Time elapsed: 0.104 s
% 11.29/2.34 % (240715)Peak memory usage: 90 MB
% 11.29/2.34 % (240715)Instructions burned: 106 (million)
% 11.29/2.34 % (240717)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3499929133:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2989 on theBenchmark for (2989ds/242Mi)
% 11.29/2.34 % (240716)------------------------------
% 11.29/2.34 % (240716)------------------------------
% 11.29/2.34 % (240723)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1476986283:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 11.29/2.34 % (240717)Instruction limit reached!
% 11.29/2.34 % (240717)------------------------------
% 11.29/2.34 % (240717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.29/2.34 % (240717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.29/2.34 % (240717)CaDiCaL version: 2.1.3
% 11.29/2.34 % (240717)Termination reason: Instruction limit
% 11.29/2.34 % (240717)Termination phase: Saturation
% 11.29/2.34 % (240717)Time elapsed: 0.204 s
% 11.29/2.34 % (240717)Peak memory usage: 92 MB
% 11.29/2.34 % (240717)Instructions burned: 243 (million)
% 11.29/2.34 % (240673)First to succeed.
% 11.29/2.34 % (240673)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-240658"
% 11.29/2.34 % (240726)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3282937067:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi)
% 11.29/2.34 % (240674)Also succeeded, but the first one will report.
% 11.29/2.34 % (240726)Also succeeded, but the first one will report.
% 11.29/2.34 % (240727)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3119364991:i=499:bd=all_2985 on theBenchmark for (2985ds/499Mi)
% 11.29/2.34 % (240675)Also succeeded, but the first one will report.
% 11.29/2.34 % (240673)Refutation found. Thanks to Tanya!
% 11.29/2.34 % SZS status Unsatisfiable for theBenchmark
% 11.29/2.34 % SZS output start Proof for theBenchmark
% See solution above
% 12.14/2.52 % (240673)------------------------------
% 12.14/2.52 % (240673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.52 % (240673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.52 % (240673)CaDiCaL version: 2.1.3
% 12.14/2.52 % (240673)Termination reason: Refutation
% 12.14/2.52 % (240673)Time elapsed: 1.305 s
% 12.14/2.52 % (240673)Peak memory usage: 140 MB
% 12.14/2.52 % (240673)Instructions burned: 2146 (million)
% 12.14/2.52 % (240673)------------------------------
% 12.14/2.52 % (240673)------------------------------
% 12.14/2.52 % (240658)Success in time 1.653 s
% 12.14/2.52 % Vampire exiting
%------------------------------------------------------------------------------