%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP666-3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:15:31 AM UTC 2026
% Result : Unsatisfiable 124.92s 38.10s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 86
% Number of leaves : 26
% Syntax : Number of formulae : 337 ( 309 unt; 14 def)
% Number of atoms : 388 ( 314 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 99 ( 48 ~; 43 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 9 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 743 ( 0 sgn 743 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c01) ).
fof(f2,axiom,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c04) ).
fof(f5,axiom,
! [X0] : mult(X0,unit) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c05) ).
fof(f6,axiom,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c06) ).
fof(f7,axiom,
! [X2,X3,X0,X1] : ld(mult(X0,X1),mult(X0,mult(X1,mult(X2,X3)))) = mult(ld(mult(X0,X1),mult(X0,mult(X1,X2))),ld(mult(X0,X1),mult(X0,mult(X1,X3)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c07) ).
fof(f8,axiom,
! [X2,X3,X0,X1] : rd(mult(mult(mult(X0,X1),X2),X3),mult(X2,X3)) = mult(rd(mult(mult(X0,X2),X3),mult(X2,X3)),rd(mult(mult(X1,X2),X3),mult(X2,X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c08) ).
fof(f9,axiom,
! [X2,X0,X1] : ld(X0,mult(mult(X1,X2),X0)) = mult(ld(X0,mult(X1,X0)),ld(X0,mult(X2,X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c09) ).
fof(f10,axiom,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c10) ).
fof(f11,axiom,
! [X0,X1] : mult(mult(X0,X1),i(X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c11) ).
fof(f12,negated_conjecture,
mult(a,mult(b,mult(c,b))) != mult(mult(mult(a,b),c),b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f13,definition,
sF0 = mult(c,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f14,plain,
mult(c,b) = sF0,
inference(reorient_equations,[],[f13]) ).
fof(f15,definition,
sF1 = mult(b,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f16,plain,
mult(b,sF0) = sF1,
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF2 = mult(a,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f18,plain,
mult(a,sF1) = sF2,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF3 = mult(a,b),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f20,plain,
mult(a,b) = sF3,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF4 = mult(sF3,c),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f22,plain,
mult(sF3,c) = sF4,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF5 = mult(sF4,b),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f24,plain,
mult(sF4,b) = sF5,
inference(reorient_equations,[],[f23]) ).
fof(f25,plain,
sF2 != sF5,
inference(definition_folding,[],[f12,f24,f22,f20,f18,f16,f14]) ).
fof(f26,plain,
! [X0,X1] : ld(X1,X0) = mult(i(X1),X0),
inference(superposition,[],[f10,f1]) ).
fof(f28,plain,
! [X0,X1] : mult(X1,X0) = ld(i(X1),X0),
inference(superposition,[],[f2,f10]) ).
fof(f32,definition,
( spl6_1
<=> mult(a,sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition]) ).
fof(f34,plain,
( mult(a,sF1) = sF2
| ~ spl6_1 ),
inference(avatar_component_clause,[],[f32]) ).
fof(f35,plain,
spl6_1,
inference(avatar_split_clause,[],[f18,f32]) ).
fof(f37,plain,
! [X0,X1] : mult(X0,i(ld(X1,X0))) = X1,
inference(superposition,[],[f11,f1]) ).
fof(f38,plain,
! [X0,X1] : rd(X0,X1) = mult(X0,i(X1)),
inference(superposition,[],[f11,f3]) ).
fof(f39,plain,
! [X0,X1] : mult(X0,X1) = mult(X0,i(i(X1))),
inference(superposition,[],[f11,f11]) ).
fof(f40,plain,
! [X0,X1] : i(X1) = ld(mult(X0,X1),X0),
inference(superposition,[],[f2,f11]) ).
fof(f41,plain,
! [X0,X1] : mult(X0,X1) = rd(X0,i(X1)),
inference(backward_demodulation,[],[f39,f38]) ).
fof(f43,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(forward_demodulation,[],[f37,f38]) ).
fof(f46,plain,
! [X2,X3,X0,X1] : rd(mult(mult(mult(rd(X0,X1),X2),X1),X3),mult(X1,X3)) = mult(rd(mult(X0,X3),mult(X1,X3)),rd(mult(mult(X2,X1),X3),mult(X1,X3))),
inference(superposition,[],[f8,f3]) ).
fof(f51,plain,
! [X2,X3,X0,X1] : rd(mult(mult(mult(X1,rd(X0,X2)),X2),X3),mult(X2,X3)) = mult(rd(mult(mult(X1,X2),X3),mult(X2,X3)),rd(mult(X0,X3),mult(X2,X3))),
inference(superposition,[],[f8,f3]) ).
fof(f59,plain,
! [X2,X3,X0,X1] : rd(mult(mult(X1,X2),X3),mult(X2,X3)) = ld(rd(mult(mult(X0,X2),X3),mult(X2,X3)),rd(mult(mult(mult(X0,X1),X2),X3),mult(X2,X3))),
inference(superposition,[],[f2,f8]) ).
fof(f69,plain,
! [X2,X0,X1] : ld(X1,mult(mult(rd(X0,X1),X2),X1)) = mult(ld(X1,X0),ld(X1,mult(X2,X1))),
inference(superposition,[],[f9,f3]) ).
fof(f74,plain,
! [X2,X0,X1] : ld(X1,mult(mult(X2,rd(X0,X1)),X1)) = mult(ld(X1,mult(X2,X1)),ld(X1,X0)),
inference(superposition,[],[f9,f3]) ).
fof(f76,plain,
! [X0,X1] : ld(X0,mult(mult(X1,X0),X0)) = mult(ld(X0,mult(X1,X0)),X0),
inference(superposition,[],[f9,f2]) ).
fof(f77,plain,
! [X2,X0,X1] : ld(X0,mult(X2,X0)) = ld(ld(X0,mult(X1,X0)),ld(X0,mult(mult(X1,X2),X0))),
inference(superposition,[],[f2,f9]) ).
fof(f90,definition,
( spl6_2
<=> mult(sF4,b) = sF5 ),
introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition]) ).
fof(f92,plain,
( mult(sF4,b) = sF5
| ~ spl6_2 ),
inference(avatar_component_clause,[],[f90]) ).
fof(f93,plain,
spl6_2,
inference(avatar_split_clause,[],[f24,f90]) ).
fof(f100,definition,
( spl6_3
<=> sF2 = sF5 ),
introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition]) ).
fof(f102,plain,
( sF2 != sF5
| spl6_3 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f103,plain,
~ spl6_3,
inference(avatar_split_clause,[],[f25,f100]) ).
fof(f105,definition,
( spl6_4
<=> mult(a,b) = sF3 ),
introduced(definition,[new_symbols(definition,[spl6_4])],[avatar_definition]) ).
fof(f107,plain,
( mult(a,b) = sF3
| ~ spl6_4 ),
inference(avatar_component_clause,[],[f105]) ).
fof(f108,plain,
spl6_4,
inference(avatar_split_clause,[],[f20,f105]) ).
fof(f112,definition,
( spl6_5
<=> mult(c,b) = sF0 ),
introduced(definition,[new_symbols(definition,[spl6_5])],[avatar_definition]) ).
fof(f114,plain,
( mult(c,b) = sF0
| ~ spl6_5 ),
inference(avatar_component_clause,[],[f112]) ).
fof(f115,plain,
spl6_5,
inference(avatar_split_clause,[],[f14,f112]) ).
fof(f119,definition,
( spl6_6
<=> mult(b,sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl6_6])],[avatar_definition]) ).
fof(f121,plain,
( mult(b,sF0) = sF1
| ~ spl6_6 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f122,plain,
spl6_6,
inference(avatar_split_clause,[],[f16,f119]) ).
fof(f125,plain,
! [X2,X3,X0,X1] : ld(mult(X1,X2),mult(X1,mult(X2,mult(ld(X2,X0),X3)))) = mult(ld(mult(X1,X2),mult(X1,X0)),ld(mult(X1,X2),mult(X1,mult(X2,X3)))),
inference(superposition,[],[f7,f1]) ).
fof(f203,definition,
( spl6_7
<=> mult(sF3,c) = sF4 ),
introduced(definition,[new_symbols(definition,[spl6_7])],[avatar_definition]) ).
fof(f205,plain,
( mult(sF3,c) = sF4
| ~ spl6_7 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f206,plain,
spl6_7,
inference(avatar_split_clause,[],[f22,f203]) ).
fof(f218,plain,
! [X0,X1] : ld(X1,mult(X0,X1)) = mult(ld(X1,X0),X1),
inference(superposition,[],[f76,f3]) ).
fof(f227,plain,
! [X0,X1] : ld(i(X0),mult(mult(X1,i(X0)),i(X0))) = mult(mult(X0,mult(X1,i(X0))),i(X0)),
inference(superposition,[],[f76,f28]) ).
fof(f229,plain,
! [X0,X1] : ld(X0,mult(X1,X0)) = rd(ld(X0,mult(mult(X1,X0),X0)),X0),
inference(superposition,[],[f4,f76]) ).
fof(f235,plain,
! [X0,X1] : ld(i(X0),mult(mult(X1,i(X0)),i(X0))) = rd(mult(X0,mult(X1,i(X0))),X0),
inference(forward_demodulation,[],[f227,f38]) ).
fof(f239,plain,
! [X0,X1] : ld(i(X0),mult(rd(X1,X0),i(X0))) = rd(mult(X0,rd(X1,X0)),X0),
inference(forward_demodulation,[],[f235,f38]) ).
fof(f241,plain,
! [X0,X1] : rd(mult(X0,rd(X1,X0)),X0) = mult(X0,mult(rd(X1,X0),i(X0))),
inference(forward_demodulation,[],[f239,f28]) ).
fof(f242,plain,
! [X0,X1] : rd(mult(X0,rd(X1,X0)),X0) = mult(X0,rd(rd(X1,X0),X0)),
inference(forward_demodulation,[],[f241,f38]) ).
fof(f243,plain,
! [X0,X1] : rd(mult(X1,X0),X1) = mult(X1,rd(X0,X1)),
inference(superposition,[],[f242,f4]) ).
fof(f256,plain,
! [X0,X1] : mult(X1,X0) = rd(mult(X1,mult(X0,X1)),X1),
inference(superposition,[],[f243,f4]) ).
fof(f278,plain,
! [X0,X1] : mult(mult(X0,X1),X0) = mult(X0,mult(X1,X0)),
inference(superposition,[],[f3,f256]) ).
fof(f315,plain,
! [X0] : ld(X0,X0) = rd(ld(X0,mult(X0,X0)),X0),
inference(superposition,[],[f229,f6]) ).
fof(f330,plain,
! [X0] : rd(X0,X0) = ld(X0,X0),
inference(forward_demodulation,[],[f315,f2]) ).
fof(f398,plain,
! [X2,X0,X1] : ld(mult(X0,X1),X0) = ld(mult(X2,X1),X2),
inference(superposition,[],[f40,f40]) ).
fof(f399,plain,
! [X0,X1] : ld(X0,X1) = i(ld(X1,X0)),
inference(superposition,[],[f40,f1]) ).
fof(f400,plain,
! [X0] : ld(X0,X0) = i(unit),
inference(superposition,[],[f40,f5]) ).
fof(f404,plain,
! [X0] : i(X0) = ld(X0,unit),
inference(superposition,[],[f40,f6]) ).
fof(f416,plain,
! [X0] : rd(X0,X0) = i(unit),
inference(forward_demodulation,[],[f400,f330]) ).
fof(f450,plain,
! [X0,X1] : mult(ld(X0,X1),mult(X0,ld(X0,X1))) = mult(ld(X0,mult(X1,X0)),ld(X0,X1)),
inference(superposition,[],[f278,f218]) ).
fof(f457,plain,
! [X0,X1] : mult(ld(X0,X1),mult(X0,ld(X0,X1))) = ld(X0,mult(mult(X1,rd(X1,X0)),X0)),
inference(forward_demodulation,[],[f450,f74]) ).
fof(f467,plain,
! [X0,X1] : mult(ld(X0,X1),X1) = ld(X0,mult(mult(X1,rd(X1,X0)),X0)),
inference(forward_demodulation,[],[f457,f1]) ).
fof(f473,plain,
! [X2,X0,X1] : ld(X1,X2) = mult(ld(mult(X0,X1),X0),X2),
inference(superposition,[],[f26,f40]) ).
fof(f481,plain,
! [X0,X1] : i(X0) = rd(ld(X0,X1),X1),
inference(superposition,[],[f4,f26]) ).
fof(f509,plain,
! [X0,X1] : i(mult(X1,X0)) = rd(i(X0),X1),
inference(superposition,[],[f481,f40]) ).
fof(f581,plain,
! [X2,X0,X1] : mult(X0,ld(X1,mult(X2,X1))) = ld(X1,mult(mult(rd(mult(X1,X0),X1),X2),X1)),
inference(superposition,[],[f69,f2]) ).
fof(f591,plain,
! [X2,X0,X1] : ld(X1,mult(mult(rd(X2,X1),rd(X0,X1)),X1)) = mult(ld(X1,X2),ld(X1,X0)),
inference(superposition,[],[f69,f3]) ).
fof(f592,plain,
! [X0,X1] : ld(X0,mult(mult(rd(X1,X0),unit),X0)) = mult(ld(X0,X1),ld(X0,X0)),
inference(superposition,[],[f69,f6]) ).
fof(f614,plain,
! [X0,X1] : ld(X0,mult(mult(rd(X1,X0),unit),X0)) = mult(ld(X0,X1),rd(X0,X0)),
inference(forward_demodulation,[],[f592,f330]) ).
fof(f623,plain,
! [X0,X1] : ld(X0,mult(rd(X1,X0),X0)) = mult(ld(X0,X1),rd(X0,X0)),
inference(forward_demodulation,[],[f614,f5]) ).
fof(f629,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(X0,X1),rd(X0,X0)),
inference(forward_demodulation,[],[f623,f3]) ).
fof(f642,plain,
! [X0,X1] : mult(X0,rd(X1,X1)) = X0,
inference(superposition,[],[f629,f2]) ).
fof(f934,plain,
! [X2,X0,X1] : rd(X2,X1) = mult(X2,ld(mult(X0,X1),X0)),
inference(superposition,[],[f38,f40]) ).
fof(f947,plain,
! [X0,X1] : mult(X0,mult(i(X1),X0)) = mult(rd(X0,X1),X0),
inference(superposition,[],[f278,f38]) ).
fof(f954,plain,
! [X0] : i(X0) = rd(unit,X0),
inference(superposition,[],[f6,f38]) ).
fof(f955,plain,
! [X0,X1] : ld(X0,i(X1)) = rd(i(X0),X1),
inference(superposition,[],[f26,f38]) ).
fof(f956,plain,
! [X0,X1] : ld(X0,i(X1)) = i(mult(X1,X0)),
inference(forward_demodulation,[],[f955,f509]) ).
fof(f963,plain,
! [X0,X1] : mult(X0,ld(X1,X0)) = mult(rd(X0,X1),X0),
inference(forward_demodulation,[],[f947,f26]) ).
fof(f1064,plain,
! [X0,X1] : mult(X0,X1) = mult(X1,ld(ld(X0,X1),X1)),
inference(superposition,[],[f963,f43]) ).
fof(f1069,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = mult(mult(X0,X1),ld(X1,mult(X0,X1))),
inference(superposition,[],[f963,f4]) ).
fof(f1129,plain,
! [X0,X1] : mult(i(X0),X1) = mult(X1,ld(mult(X0,X1),X1)),
inference(superposition,[],[f1064,f28]) ).
fof(f1160,plain,
! [X0,X1] : ld(X0,X1) = mult(X1,ld(mult(X0,X1),X1)),
inference(forward_demodulation,[],[f1129,f26]) ).
fof(f1198,plain,
! [X0,X1] : ld(mult(X0,X1),X0) = mult(X0,ld(mult(X0,mult(X1,X0)),X0)),
inference(superposition,[],[f1160,f278]) ).
fof(f1237,plain,
! [X0,X1] : ld(mult(X0,X1),X0) = rd(X0,mult(X1,X0)),
inference(forward_demodulation,[],[f1198,f934]) ).
fof(f1250,plain,
! [X2,X0,X1] : rd(X0,mult(X1,X0)) = ld(mult(X2,X1),X2),
inference(backward_demodulation,[],[f398,f1237]) ).
fof(f1252,plain,
! [X2,X0,X1] : ld(X1,X2) = mult(rd(X0,mult(X1,X0)),X2),
inference(backward_demodulation,[],[f473,f1237]) ).
fof(f1256,plain,
! [X2,X0,X1] : rd(X2,X1) = mult(X2,rd(X0,mult(X1,X0))),
inference(backward_demodulation,[],[f934,f1237]) ).
fof(f1260,plain,
! [X2,X0,X1] : rd(X0,mult(X1,X0)) = rd(X2,mult(X1,X2)),
inference(forward_demodulation,[],[f1250,f1237]) ).
fof(f1332,plain,
! [X2,X3,X0,X1] : rd(X3,mult(ld(X0,X1),X3)) = rd(ld(X0,mult(X2,X0)),ld(X0,mult(mult(rd(X1,X0),X2),X0))),
inference(superposition,[],[f1260,f69]) ).
fof(f1335,plain,
! [X2,X0,X1] : rd(X2,X0) = rd(X1,mult(rd(X0,X2),X1)),
inference(superposition,[],[f1260,f3]) ).
fof(f1362,plain,
! [X2,X0,X1] : rd(mult(mult(X1,X2),X2),mult(X1,X2)) = mult(mult(X1,X2),rd(X0,mult(X1,X0))),
inference(superposition,[],[f243,f1260]) ).
fof(f1367,plain,
! [X2,X1] : rd(mult(X1,X2),X1) = rd(mult(mult(X1,X2),X2),mult(X1,X2)),
inference(forward_demodulation,[],[f1362,f1256]) ).
fof(f1413,plain,
! [X2,X3,X0,X1] : rd(X3,ld(X0,X1)) = mult(X3,rd(ld(X0,mult(X2,X0)),ld(X0,mult(mult(rd(X1,X0),X2),X0)))),
inference(superposition,[],[f1256,f69]) ).
fof(f1416,plain,
! [X2,X0,X1] : mult(X1,rd(X2,X0)) = rd(X1,rd(X0,X2)),
inference(superposition,[],[f1256,f3]) ).
fof(f1661,plain,
! [X2,X3,X0,X1] : mult(X3,rd(rd(X2,X1),X0)) = rd(X3,mult(X0,rd(X1,X2))),
inference(superposition,[],[f1416,f1416]) ).
fof(f1678,plain,
! [X0,X1] : i(unit) = mult(rd(X0,X1),rd(X1,X0)),
inference(superposition,[],[f416,f1416]) ).
fof(f1691,plain,
! [X2,X0,X1] : mult(i(X0),rd(X1,X2)) = i(mult(rd(X2,X1),X0)),
inference(superposition,[],[f509,f1416]) ).
fof(f1692,plain,
! [X2,X0,X1] : ld(X0,rd(X1,X2)) = i(mult(rd(X2,X1),X0)),
inference(forward_demodulation,[],[f1691,f26]) ).
fof(f1856,plain,
! [X1] : i(unit) = rd(X1,mult(i(unit),X1)),
inference(superposition,[],[f1335,f416]) ).
fof(f1891,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = mult(X2,ld(mult(rd(X1,X0),X2),X2)),
inference(superposition,[],[f963,f1335]) ).
fof(f1898,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = ld(rd(X1,X0),X2),
inference(forward_demodulation,[],[f1891,f1160]) ).
fof(f1918,plain,
! [X1] : i(unit) = rd(X1,ld(unit,X1)),
inference(forward_demodulation,[],[f1856,f26]) ).
fof(f1931,plain,
! [X2,X3,X0,X1] : rd(mult(mult(X1,X2),X3),mult(X2,X3)) = mult(rd(mult(X2,X3),mult(mult(X0,X2),X3)),rd(mult(mult(mult(X0,X1),X2),X3),mult(X2,X3))),
inference(backward_demodulation,[],[f59,f1898]) ).
fof(f1944,plain,
unit = i(unit),
inference(forward_demodulation,[],[f1918,f43]) ).
fof(f1957,plain,
! [X0,X1] : unit = mult(rd(X0,X1),rd(X1,X0)),
inference(backward_demodulation,[],[f1678,f1944]) ).
fof(f2258,plain,
! [X2,X3,X0,X1] : ld(ld(X0,X1),X3) = mult(rd(ld(X0,mult(X2,X0)),ld(X0,mult(mult(rd(X1,X0),X2),X0))),X3),
inference(superposition,[],[f1252,f69]) ).
fof(f2443,plain,
! [X2,X0,X1] : ld(mult(X0,X1),mult(X0,mult(X1,mult(ld(X1,unit),X2)))) = mult(ld(mult(X0,X1),X0),ld(mult(X0,X1),mult(X0,mult(X1,X2)))),
inference(superposition,[],[f125,f5]) ).
fof(f2574,plain,
! [X2,X0,X1] : ld(mult(X0,X1),mult(X0,mult(X1,mult(ld(X1,unit),X2)))) = mult(rd(X0,mult(X1,X0)),ld(mult(X0,X1),mult(X0,mult(X1,X2)))),
inference(forward_demodulation,[],[f2443,f1237]) ).
fof(f2603,plain,
! [X2,X0,X1] : ld(mult(X0,X1),mult(X0,mult(X1,mult(ld(X1,unit),X2)))) = ld(X1,ld(mult(X0,X1),mult(X0,mult(X1,X2)))),
inference(forward_demodulation,[],[f2574,f1252]) ).
fof(f2628,plain,
! [X2,X0,X1] : ld(X1,ld(mult(X0,X1),mult(X0,mult(X1,X2)))) = ld(mult(X0,X1),mult(X0,mult(X1,mult(i(X1),X2)))),
inference(forward_demodulation,[],[f2603,f404]) ).
fof(f2642,plain,
! [X2,X0,X1] : ld(mult(X0,X1),mult(X0,mult(X1,ld(X1,X2)))) = ld(X1,ld(mult(X0,X1),mult(X0,mult(X1,X2)))),
inference(forward_demodulation,[],[f2628,f26]) ).
fof(f2651,plain,
! [X2,X0,X1] : ld(mult(X0,X1),mult(X0,X2)) = ld(X1,ld(mult(X0,X1),mult(X0,mult(X1,X2)))),
inference(forward_demodulation,[],[f2642,f1]) ).
fof(f2689,plain,
! [X2,X0,X1] : ld(X1,mult(mult(X2,rd(mult(X1,X0),X1)),X1)) = mult(ld(X1,mult(X2,X1)),X0),
inference(superposition,[],[f74,f2]) ).
fof(f3150,plain,
! [X2,X0,X1] : ld(mult(X1,X2),mult(X1,ld(X2,X0))) = ld(X2,ld(mult(X1,X2),mult(X1,X0))),
inference(superposition,[],[f2651,f1]) ).
fof(f3186,plain,
! [X2,X0,X1] : ld(mult(X0,X1),mult(X0,mult(X1,X2))) = mult(X1,ld(mult(X0,X1),mult(X0,X2))),
inference(superposition,[],[f1,f2651]) ).
fof(f3364,plain,
! [X0,X1] : ld(X1,ld(mult(X1,X1),mult(X1,X0))) = ld(mult(X1,X1),X0),
inference(superposition,[],[f3150,f1]) ).
fof(f3469,plain,
! [X0,X1] : ld(mult(X1,X1),ld(X1,X0)) = ld(X1,ld(mult(X1,X1),X0)),
inference(superposition,[],[f3364,f1]) ).
fof(f3499,plain,
! [X0,X1] : ld(mult(X0,X0),mult(X0,X1)) = mult(X0,ld(mult(X0,X0),X1)),
inference(superposition,[],[f1,f3364]) ).
fof(f3623,plain,
! [X0,X1] : ld(i(X0),ld(mult(i(X0),i(X0)),X1)) = ld(mult(i(X0),i(X0)),mult(X0,X1)),
inference(superposition,[],[f3469,f28]) ).
fof(f3638,plain,
! [X0,X1] : ld(i(X0),ld(ld(X0,i(X0)),X1)) = ld(ld(X0,i(X0)),mult(X0,X1)),
inference(forward_demodulation,[],[f3623,f26]) ).
fof(f3652,plain,
! [X0,X1] : ld(i(X0),ld(i(mult(X0,X0)),X1)) = ld(i(mult(X0,X0)),mult(X0,X1)),
inference(forward_demodulation,[],[f3638,f956]) ).
fof(f3661,plain,
! [X0,X1] : ld(i(X0),ld(i(mult(X0,X0)),X1)) = mult(mult(X0,X0),mult(X0,X1)),
inference(forward_demodulation,[],[f3652,f28]) ).
fof(f3668,plain,
! [X0,X1] : mult(X0,ld(i(mult(X0,X0)),X1)) = mult(mult(X0,X0),mult(X0,X1)),
inference(forward_demodulation,[],[f3661,f28]) ).
fof(f3674,plain,
! [X0,X1] : mult(mult(X0,X0),mult(X0,X1)) = mult(X0,mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f3668,f28]) ).
fof(f3703,plain,
! [X0,X1] : mult(mult(X0,X0),rd(X0,X1)) = mult(X0,mult(mult(X0,X0),i(X1))),
inference(superposition,[],[f3674,f38]) ).
fof(f3730,plain,
! [X0,X1] : mult(X0,X1) = ld(mult(X0,X0),mult(X0,mult(mult(X0,X0),X1))),
inference(superposition,[],[f2,f3674]) ).
fof(f3767,plain,
! [X0,X1] : mult(mult(X0,X0),rd(X0,X1)) = mult(X0,rd(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f3703,f38]) ).
fof(f3883,plain,
! [X0,X1] : ld(mult(i(X0),i(X0)),mult(i(X0),X1)) = ld(X0,ld(mult(i(X0),i(X0)),X1)),
inference(superposition,[],[f26,f3499]) ).
fof(f3884,plain,
! [X0,X1] : ld(ld(X0,i(X0)),mult(i(X0),X1)) = ld(X0,ld(ld(X0,i(X0)),X1)),
inference(forward_demodulation,[],[f3883,f26]) ).
fof(f3923,plain,
! [X0,X1] : ld(i(mult(X0,X0)),mult(i(X0),X1)) = ld(X0,ld(i(mult(X0,X0)),X1)),
inference(forward_demodulation,[],[f3884,f956]) ).
fof(f3942,plain,
! [X0,X1] : ld(i(mult(X0,X0)),mult(i(X0),X1)) = ld(X0,mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f3923,f28]) ).
fof(f3955,plain,
! [X0,X1] : mult(mult(X0,X0),mult(i(X0),X1)) = ld(X0,mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f3942,f28]) ).
fof(f3963,plain,
! [X0,X1] : mult(mult(X0,X0),ld(X0,X1)) = ld(X0,mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f3955,f26]) ).
fof(f4007,plain,
! [X0,X1] : mult(X0,X0) = rd(ld(X0,mult(mult(X0,X0),X1)),ld(X0,X1)),
inference(superposition,[],[f4,f3963]) ).
fof(f4127,plain,
! [X0,X1] : rd(mult(X0,X0),X1) = mult(X0,rd(mult(X0,X0),mult(X1,X0))),
inference(superposition,[],[f1256,f3767]) ).
fof(f4577,plain,
! [X2,X0,X1] : ld(X0,mult(X1,mult(ld(X1,X0),X2))) = mult(ld(X1,X0),ld(X0,mult(X1,X2))),
inference(superposition,[],[f3186,f1]) ).
fof(f4609,plain,
! [X2,X0,X1] : ld(mult(X1,X2),mult(X1,mult(X2,ld(X1,X0)))) = mult(X2,ld(mult(X1,X2),X0)),
inference(superposition,[],[f3186,f1]) ).
fof(f4634,plain,
! [X2,X0,X1] : ld(mult(i(X0),X2),mult(i(X0),mult(X2,X1))) = mult(X2,ld(mult(i(X0),X2),ld(X0,X1))),
inference(superposition,[],[f3186,f26]) ).
fof(f4705,plain,
! [X2,X0,X1] : ld(ld(X0,X2),mult(i(X0),mult(X2,X1))) = mult(X2,ld(ld(X0,X2),ld(X0,X1))),
inference(forward_demodulation,[],[f4634,f26]) ).
fof(f4734,plain,
! [X2,X0,X1] : mult(X2,ld(ld(X0,X2),ld(X0,X1))) = ld(ld(X0,X2),ld(X0,mult(X2,X1))),
inference(forward_demodulation,[],[f4705,f26]) ).
fof(f4887,plain,
! [X2,X0,X1] : i(ld(X0,mult(X2,X0))) = rd(ld(X0,mult(X1,X0)),ld(X0,mult(mult(X2,X1),X0))),
inference(superposition,[],[f481,f77]) ).
fof(f4900,plain,
! [X2,X0,X1] : ld(mult(X2,X0),X0) = rd(ld(X0,mult(X1,X0)),ld(X0,mult(mult(X2,X1),X0))),
inference(forward_demodulation,[],[f4887,f399]) ).
fof(f4981,plain,
! [X3,X0,X1] : ld(ld(X0,X1),X3) = mult(ld(mult(rd(X1,X0),X0),X0),X3),
inference(backward_demodulation,[],[f2258,f4900]) ).
fof(f4982,plain,
! [X3,X0,X1] : rd(X3,ld(X0,X1)) = mult(X3,ld(mult(rd(X1,X0),X0),X0)),
inference(backward_demodulation,[],[f1413,f4900]) ).
fof(f4983,plain,
! [X3,X0,X1] : rd(X3,mult(ld(X0,X1),X3)) = ld(mult(rd(X1,X0),X0),X0),
inference(backward_demodulation,[],[f1332,f4900]) ).
fof(f5030,plain,
! [X3,X0,X1] : ld(X1,X0) = rd(X3,mult(ld(X0,X1),X3)),
inference(forward_demodulation,[],[f4983,f3]) ).
fof(f5031,plain,
! [X3,X0,X1] : rd(X3,ld(X0,X1)) = mult(X3,ld(X1,X0)),
inference(forward_demodulation,[],[f4982,f3]) ).
fof(f5032,plain,
! [X3,X0,X1] : mult(ld(X1,X0),X3) = ld(ld(X0,X1),X3),
inference(forward_demodulation,[],[f4981,f3]) ).
fof(f5136,plain,
! [X0,X1] : mult(X0,X0) = mult(ld(X0,mult(mult(X0,X0),X1)),ld(X1,X0)),
inference(backward_demodulation,[],[f4007,f5031]) ).
fof(f5256,plain,
! [X2,X0,X1] : ld(ld(X0,X2),ld(X0,mult(X2,X1))) = mult(X2,mult(ld(X2,X0),ld(X0,X1))),
inference(backward_demodulation,[],[f4734,f5032]) ).
fof(f5505,plain,
! [X2,X0,X1] : mult(X2,mult(ld(X2,X0),ld(X0,X1))) = mult(ld(X2,X0),ld(X0,mult(X2,X1))),
inference(forward_demodulation,[],[f5256,f5032]) ).
fof(f5653,plain,
! [X2,X0,X1] : mult(X2,mult(ld(X2,X0),ld(X0,X1))) = ld(X0,mult(X2,mult(ld(X2,X0),X1))),
inference(forward_demodulation,[],[f5505,f4577]) ).
fof(f5960,plain,
! [X2,X3,X0,X1] : mult(X3,rd(ld(X2,X1),X0)) = rd(X3,mult(X0,ld(X1,X2))),
inference(superposition,[],[f1416,f5031]) ).
fof(f6841,plain,
! [X2,X0,X1] : ld(X0,mult(mult(mult(X0,X1),X2),X0)) = mult(mult(X1,X0),ld(X0,mult(X2,X0))),
inference(superposition,[],[f581,f256]) ).
fof(f6929,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = ld(X1,mult(mult(mult(X1,X0),X0),X1)),
inference(backward_demodulation,[],[f1069,f6841]) ).
fof(f7209,plain,
! [X2,X3,X0,X1] : rd(mult(mult(mult(rd(X1,X2),rd(X0,X2)),X2),X3),mult(X2,X3)) = mult(rd(mult(X1,X3),mult(X2,X3)),rd(mult(X0,X3),mult(X2,X3))),
inference(superposition,[],[f46,f3]) ).
fof(f7867,plain,
! [X2,X0,X1] : rd(mult(mult(mult(X0,rd(X2,X0)),X0),ld(X0,X1)),mult(X0,ld(X0,X1))) = mult(rd(ld(X0,mult(mult(X0,X0),X1)),mult(X0,ld(X0,X1))),rd(mult(X2,ld(X0,X1)),mult(X0,ld(X0,X1)))),
inference(superposition,[],[f51,f3963]) ).
fof(f7898,plain,
! [X2,X3,X0,X1] : rd(mult(mult(mult(X1,rd(rd(X0,X2),X3)),X3),X2),mult(X3,X2)) = mult(rd(mult(mult(X1,X3),X2),mult(X3,X2)),rd(X0,mult(X3,X2))),
inference(superposition,[],[f51,f3]) ).
fof(f7905,plain,
! [X2,X0,X1] : rd(mult(mult(mult(X1,rd(unit,X2)),X2),X0),mult(X2,X0)) = mult(rd(mult(mult(X1,X2),X0),mult(X2,X0)),rd(X0,mult(X2,X0))),
inference(superposition,[],[f51,f6]) ).
fof(f8064,plain,
! [X2,X0,X1] : rd(mult(mult(mult(X1,rd(unit,X2)),X2),X0),mult(X2,X0)) = rd(rd(mult(mult(X1,X2),X0),mult(X2,X0)),X2),
inference(forward_demodulation,[],[f7905,f1256]) ).
fof(f8071,plain,
! [X2,X3,X0,X1] : mult(rd(mult(mult(X1,X3),X2),mult(X3,X2)),rd(X0,mult(X3,X2))) = rd(mult(mult(rd(X1,mult(X3,rd(X2,X0))),X3),X2),mult(X3,X2)),
inference(forward_demodulation,[],[f7898,f1661]) ).
fof(f8093,plain,
! [X2,X0,X1] : rd(mult(mult(mult(X0,rd(X2,X0)),X0),ld(X0,X1)),X1) = mult(rd(ld(X0,mult(mult(X0,X0),X1)),X1),rd(mult(X2,ld(X0,X1)),X1)),
inference(forward_demodulation,[],[f7867,f1]) ).
fof(f8173,plain,
! [X2,X0,X1] : rd(rd(mult(mult(X1,X2),X0),mult(X2,X0)),X2) = rd(mult(mult(mult(X1,i(X2)),X2),X0),mult(X2,X0)),
inference(forward_demodulation,[],[f8064,f954]) ).
fof(f8194,plain,
! [X2,X0,X1] : mult(rd(ld(X0,mult(mult(X0,X0),X1)),X1),rd(mult(X2,ld(X0,X1)),X1)) = rd(mult(mult(X0,mult(rd(X2,X0),X0)),ld(X0,X1)),X1),
inference(forward_demodulation,[],[f8093,f278]) ).
fof(f8250,plain,
! [X2,X0,X1] : rd(rd(mult(mult(X1,X2),X0),mult(X2,X0)),X2) = rd(mult(mult(rd(X1,X2),X2),X0),mult(X2,X0)),
inference(forward_demodulation,[],[f8173,f38]) ).
fof(f8262,plain,
! [X2,X0,X1] : mult(rd(ld(X0,mult(mult(X0,X0),X1)),X1),rd(mult(X2,ld(X0,X1)),X1)) = rd(mult(mult(X0,X2),ld(X0,X1)),X1),
inference(forward_demodulation,[],[f8194,f3]) ).
fof(f8301,plain,
! [X2,X0,X1] : rd(rd(mult(mult(X1,X2),X0),mult(X2,X0)),X2) = rd(mult(X1,X0),mult(X2,X0)),
inference(forward_demodulation,[],[f8250,f3]) ).
fof(f8394,plain,
! [X0,X1] : rd(mult(X0,X0),mult(X1,X0)) = rd(rd(mult(X0,mult(X1,X0)),mult(X1,X0)),X1),
inference(superposition,[],[f8301,f278]) ).
fof(f8399,plain,
! [X2,X0,X1] : rd(mult(X1,ld(mult(X1,X2),X0)),mult(X2,ld(mult(X1,X2),X0))) = rd(rd(X0,mult(X2,ld(mult(X1,X2),X0))),X2),
inference(superposition,[],[f8301,f1]) ).
fof(f8447,plain,
! [X2,X0,X1] : rd(mult(mult(X0,X2),X1),mult(X2,X1)) = mult(rd(mult(X0,X1),mult(X2,X1)),X2),
inference(superposition,[],[f3,f8301]) ).
fof(f8506,plain,
! [X0,X1] : rd(X0,X1) = rd(mult(X0,X0),mult(X1,X0)),
inference(forward_demodulation,[],[f8394,f4]) ).
fof(f8578,plain,
! [X0,X1] : mult(X0,rd(X0,X1)) = rd(mult(X0,X0),X1),
inference(backward_demodulation,[],[f4127,f8506]) ).
fof(f8624,plain,
! [X0,X1] : mult(ld(X0,X1),X1) = ld(X0,mult(rd(mult(X1,X1),X0),X0)),
inference(backward_demodulation,[],[f467,f8578]) ).
fof(f8667,plain,
! [X0,X1] : mult(ld(X0,X1),X1) = ld(X0,mult(X1,X1)),
inference(forward_demodulation,[],[f8624,f3]) ).
fof(f8754,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = ld(i(X0),mult(X1,X1)),
inference(superposition,[],[f8667,f28]) ).
fof(f8760,plain,
! [X0,X1] : ld(X1,X0) = rd(X1,ld(X0,mult(X1,X1))),
inference(superposition,[],[f5030,f8667]) ).
fof(f8845,plain,
! [X0,X1] : ld(X1,X0) = mult(X1,ld(mult(X1,X1),X0)),
inference(forward_demodulation,[],[f8760,f5031]) ).
fof(f8850,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = mult(X0,mult(X1,X1)),
inference(forward_demodulation,[],[f8754,f28]) ).
fof(f8889,plain,
! [X0,X1] : ld(X1,X0) = ld(mult(X1,X1),mult(X1,X0)),
inference(forward_demodulation,[],[f8845,f3499]) ).
fof(f8894,plain,
! [X2,X1] : rd(mult(X1,X2),X1) = rd(mult(X1,mult(X2,X2)),mult(X1,X2)),
inference(backward_demodulation,[],[f1367,f8850]) ).
fof(f8901,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = ld(X1,mult(mult(X1,mult(X0,X0)),X1)),
inference(backward_demodulation,[],[f6929,f8850]) ).
fof(f8973,plain,
! [X0,X1] : mult(X0,X1) = ld(X0,mult(mult(X0,X0),X1)),
inference(backward_demodulation,[],[f3730,f8889]) ).
fof(f8984,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = ld(X1,mult(X1,mult(mult(X0,X0),X1))),
inference(forward_demodulation,[],[f8901,f278]) ).
fof(f9014,plain,
! [X0,X1] : mult(X0,X0) = mult(mult(X0,X1),ld(X1,X0)),
inference(backward_demodulation,[],[f5136,f8973]) ).
fof(f9024,plain,
! [X2,X0,X1] : rd(mult(mult(X0,X2),ld(X0,X1)),X1) = mult(rd(mult(X0,X1),X1),rd(mult(X2,ld(X0,X1)),X1)),
inference(backward_demodulation,[],[f8262,f8973]) ).
fof(f9051,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = mult(mult(X0,X0),X1),
inference(forward_demodulation,[],[f8984,f2]) ).
fof(f9065,plain,
! [X2,X0,X1] : rd(mult(mult(X0,X2),ld(X0,X1)),X1) = mult(X0,rd(mult(X2,ld(X0,X1)),X1)),
inference(forward_demodulation,[],[f9024,f4]) ).
fof(f9663,plain,
! [X2,X0,X1] : rd(mult(mult(mult(X0,rd(X2,X0)),X0),X1),mult(X0,X1)) = mult(rd(mult(X0,mult(X0,X1)),mult(X0,X1)),rd(mult(X2,X1),mult(X0,X1))),
inference(superposition,[],[f51,f9051]) ).
fof(f9755,plain,
! [X2,X0,X1] : rd(mult(mult(mult(X0,rd(X2,X0)),X0),X1),mult(X0,X1)) = mult(X0,rd(mult(X2,X1),mult(X0,X1))),
inference(forward_demodulation,[],[f9663,f4]) ).
fof(f9796,plain,
! [X2,X0,X1] : mult(X0,rd(mult(X2,X1),mult(X0,X1))) = rd(mult(mult(X0,mult(rd(X2,X0),X0)),X1),mult(X0,X1)),
inference(forward_demodulation,[],[f9755,f278]) ).
fof(f9816,plain,
! [X2,X0,X1] : mult(X0,rd(mult(X2,X1),mult(X0,X1))) = rd(mult(mult(X0,X2),X1),mult(X0,X1)),
inference(forward_demodulation,[],[f9796,f3]) ).
fof(f11698,plain,
! [X2,X0,X1] : rd(mult(mult(mult(rd(X1,X2),X0),X2),ld(X2,X0)),mult(X2,ld(X2,X0))) = mult(rd(mult(X1,ld(X2,X0)),mult(X2,ld(X2,X0))),rd(mult(X0,X0),mult(X2,ld(X2,X0)))),
inference(superposition,[],[f46,f9014]) ).
fof(f11764,plain,
! [X2,X0,X1] : rd(mult(mult(mult(rd(X1,X2),X0),X2),ld(X2,X0)),X0) = mult(rd(mult(X1,ld(X2,X0)),X0),rd(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f11698,f1]) ).
fof(f11822,plain,
! [X2,X0,X1] : rd(mult(mult(mult(rd(X1,X2),X0),X2),ld(X2,X0)),X0) = mult(rd(mult(X1,ld(X2,X0)),X0),X0),
inference(forward_demodulation,[],[f11764,f4]) ).
fof(f11860,plain,
! [X2,X0,X1] : mult(X1,ld(X2,X0)) = rd(mult(mult(mult(rd(X1,X2),X0),X2),ld(X2,X0)),X0),
inference(forward_demodulation,[],[f11822,f3]) ).
fof(f14696,plain,
! [X2,X0,X1] : mult(mult(X0,X1),ld(X1,X2)) = rd(mult(mult(mult(X0,X2),X1),ld(X1,X2)),X2),
inference(superposition,[],[f11860,f4]) ).
fof(f16949,plain,
! [X2,X0,X1] : mult(X0,mult(ld(X0,mult(X1,X0)),X2)) = mult(mult(X1,rd(mult(X0,X2),X0)),X0),
inference(superposition,[],[f1,f2689]) ).
fof(f19744,plain,
! [X2,X0,X1] : rd(mult(mult(rd(X0,X1),X2),X1),mult(X2,X1)) = mult(rd(X0,mult(X2,X1)),X2),
inference(superposition,[],[f8447,f3]) ).
fof(f22222,plain,
! [X2,X0,X1] : mult(mult(rd(X1,X0),rd(X2,X0)),X0) = mult(X0,mult(ld(X0,X1),ld(X0,X2))),
inference(superposition,[],[f1,f591]) ).
fof(f22271,plain,
! [X2,X3,X0,X1] : mult(rd(mult(X1,X3),mult(X2,X3)),rd(mult(X0,X3),mult(X2,X3))) = rd(mult(mult(X2,mult(ld(X2,X1),ld(X2,X0))),X3),mult(X2,X3)),
inference(backward_demodulation,[],[f7209,f22222]) ).
fof(f23484,plain,
! [X2,X0,X1] : rd(mult(mult(X1,mult(rd(X0,X2),X1)),X2),mult(X1,X2)) = mult(X1,mult(rd(X0,mult(X1,X2)),X1)),
inference(superposition,[],[f9816,f19744]) ).
fof(f23491,plain,
! [X2,X0,X1] : mult(mult(rd(X0,X2),X1),X2) = mult(mult(rd(X0,mult(X1,X2)),X1),mult(X1,X2)),
inference(superposition,[],[f3,f19744]) ).
fof(f31229,plain,
! [X2,X0,X1] : rd(X0,mult(rd(mult(X1,ld(X0,X2)),X2),X0)) = ld(rd(mult(mult(X0,X1),ld(X0,X2)),X2),X0),
inference(superposition,[],[f1237,f9065]) ).
fof(f31313,plain,
! [X2,X0,X1] : mult(mult(X2,mult(X0,X1)),rd(X0,mult(X1,X0))) = rd(mult(mult(mult(X2,X0),mult(X0,X1)),rd(X0,mult(X1,X0))),X0),
inference(superposition,[],[f14696,f1237]) ).
fof(f31324,plain,
! [X2,X0,X1] : mult(mult(X2,mult(X0,X1)),rd(X0,mult(X1,X0))) = rd(rd(mult(mult(X2,X0),mult(X0,X1)),X1),X0),
inference(forward_demodulation,[],[f31313,f1256]) ).
fof(f31406,plain,
! [X2,X0,X1] : rd(X0,mult(rd(mult(X1,ld(X0,X2)),X2),X0)) = mult(rd(X2,mult(mult(X0,X1),ld(X0,X2))),X0),
inference(forward_demodulation,[],[f31229,f1898]) ).
fof(f31420,plain,
! [X2,X0,X1] : rd(mult(X2,mult(X0,X1)),X1) = rd(rd(mult(mult(X2,X0),mult(X0,X1)),X1),X0),
inference(forward_demodulation,[],[f31324,f1256]) ).
fof(f31476,plain,
! [X2,X0,X1] : rd(X2,mult(X1,ld(X0,X2))) = mult(rd(X2,mult(mult(X0,X1),ld(X0,X2))),X0),
inference(forward_demodulation,[],[f31406,f1335]) ).
fof(f35443,plain,
! [X2,X0,X1] : mult(mult(X2,rd(mult(X0,mult(X1,X1)),mult(X0,X1))),mult(X0,X1)) = mult(mult(X0,X1),mult(ld(mult(X0,X1),mult(X2,mult(X0,X1))),X1)),
inference(superposition,[],[f16949,f8850]) ).
fof(f35538,plain,
! [X2,X0,X1] : mult(rd(X1,mult(rd(mult(X0,X2),X0),X0)),rd(mult(X0,X2),X0)) = rd(mult(X0,mult(ld(X0,mult(rd(X1,X0),X0)),X2)),mult(rd(mult(X0,X2),X0),X0)),
inference(superposition,[],[f19744,f16949]) ).
fof(f35647,plain,
! [X2,X0,X1] : mult(rd(X1,mult(X0,X2)),rd(mult(X0,X2),X0)) = rd(mult(X0,mult(ld(X0,mult(rd(X1,X0),X0)),X2)),mult(X0,X2)),
inference(forward_demodulation,[],[f35538,f3]) ).
fof(f35724,plain,
! [X2,X0,X1] : mult(mult(X2,rd(mult(X0,X1),X0)),mult(X0,X1)) = mult(mult(X0,X1),mult(ld(mult(X0,X1),mult(X2,mult(X0,X1))),X1)),
inference(forward_demodulation,[],[f35443,f8894]) ).
fof(f35770,plain,
! [X2,X0,X1] : mult(rd(X1,mult(X0,X2)),rd(mult(X0,X2),X0)) = rd(mult(X0,mult(ld(X0,X1),X2)),mult(X0,X2)),
inference(forward_demodulation,[],[f35647,f3]) ).
fof(f46247,plain,
! [X2,X0,X1] : mult(X1,ld(mult(i(X0),X1),X2)) = ld(mult(i(X0),X1),ld(X0,mult(X1,ld(i(X0),X2)))),
inference(superposition,[],[f4609,f26]) ).
fof(f46324,plain,
! [X2,X0,X1] : mult(X1,ld(mult(i(X0),X1),X2)) = ld(mult(i(X0),X1),ld(X0,mult(X1,mult(X0,X2)))),
inference(forward_demodulation,[],[f46247,f28]) ).
fof(f46449,plain,
! [X2,X0,X1] : mult(X1,ld(ld(X0,X1),X2)) = ld(ld(X0,X1),ld(X0,mult(X1,mult(X0,X2)))),
inference(forward_demodulation,[],[f46324,f26]) ).
fof(f46540,plain,
! [X2,X0,X1] : mult(X1,ld(ld(X0,X1),X2)) = mult(ld(X1,X0),ld(X0,mult(X1,mult(X0,X2)))),
inference(forward_demodulation,[],[f46449,f5032]) ).
fof(f46616,plain,
! [X2,X0,X1] : mult(X1,ld(ld(X0,X1),X2)) = ld(X0,mult(X1,mult(ld(X1,X0),mult(X0,X2)))),
inference(forward_demodulation,[],[f46540,f4577]) ).
fof(f46651,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),X2)) = ld(X0,mult(X1,mult(ld(X1,X0),mult(X0,X2)))),
inference(forward_demodulation,[],[f46616,f5032]) ).
fof(f57835,plain,
! [X2,X0,X1] : mult(mult(X0,X2),mult(ld(mult(X0,X2),mult(rd(mult(X1,X2),mult(X0,X2)),mult(X0,X2))),X2)) = mult(rd(mult(mult(X0,mult(ld(X0,X1),ld(X0,mult(X0,X2)))),X2),mult(X0,X2)),mult(X0,X2)),
inference(superposition,[],[f16949,f22271]) ).
fof(f58107,plain,
! [X2,X0,X1] : mult(mult(X0,mult(ld(X0,X1),ld(X0,mult(X0,X2)))),X2) = mult(mult(X0,X2),mult(ld(mult(X0,X2),mult(rd(mult(X1,X2),mult(X0,X2)),mult(X0,X2))),X2)),
inference(forward_demodulation,[],[f57835,f3]) ).
fof(f58505,plain,
! [X2,X0,X1] : mult(mult(X0,mult(ld(X0,X1),ld(X0,mult(X0,X2)))),X2) = mult(mult(rd(mult(X1,X2),mult(X0,X2)),rd(mult(X0,X2),X0)),mult(X0,X2)),
inference(forward_demodulation,[],[f58107,f35724]) ).
fof(f58835,plain,
! [X2,X0,X1] : mult(mult(X0,mult(ld(X0,X1),ld(X0,mult(X0,X2)))),X2) = mult(rd(mult(X0,mult(ld(X0,mult(X1,X2)),X2)),mult(X0,X2)),mult(X0,X2)),
inference(forward_demodulation,[],[f58505,f35770]) ).
fof(f59094,plain,
! [X2,X0,X1] : mult(X0,mult(ld(X0,mult(X1,X2)),X2)) = mult(mult(X0,mult(ld(X0,X1),ld(X0,mult(X0,X2)))),X2),
inference(forward_demodulation,[],[f58835,f3]) ).
fof(f59264,plain,
! [X2,X0,X1] : mult(X0,mult(ld(X0,mult(X1,X2)),X2)) = mult(mult(X0,mult(ld(X0,X1),X2)),X2),
inference(forward_demodulation,[],[f59094,f2]) ).
fof(f59737,plain,
! [X2,X0,X1] : mult(X0,mult(ld(X0,mult(X1,i(X2))),i(X2))) = rd(mult(X0,mult(ld(X0,X1),i(X2))),X2),
inference(superposition,[],[f38,f59264]) ).
fof(f59738,plain,
! [X2,X0,X1] : mult(X0,mult(ld(X0,mult(X1,i(X2))),i(X2))) = rd(mult(X0,rd(ld(X0,X1),X2)),X2),
inference(forward_demodulation,[],[f59737,f38]) ).
fof(f59826,plain,
! [X2,X0,X1] : rd(rd(X0,mult(X2,ld(X1,X0))),X2) = mult(X0,mult(ld(X0,mult(X1,i(X2))),i(X2))),
inference(forward_demodulation,[],[f59738,f5960]) ).
fof(f59885,plain,
! [X2,X0,X1] : rd(rd(X0,mult(X2,ld(X1,X0))),X2) = mult(X0,rd(ld(X0,mult(X1,i(X2))),X2)),
inference(forward_demodulation,[],[f59826,f38]) ).
fof(f59933,plain,
! [X2,X0,X1] : rd(rd(X0,mult(X2,ld(X1,X0))),X2) = rd(X0,mult(X2,ld(mult(X1,i(X2)),X0))),
inference(forward_demodulation,[],[f59885,f5960]) ).
fof(f59969,plain,
! [X2,X0,X1] : rd(rd(X0,mult(X2,ld(X1,X0))),X2) = rd(X0,mult(X2,ld(rd(X1,X2),X0))),
inference(forward_demodulation,[],[f59933,f38]) ).
fof(f59991,plain,
! [X2,X0,X1] : rd(rd(X0,mult(X2,ld(X1,X0))),X2) = rd(X0,mult(X2,mult(rd(X2,X1),X0))),
inference(forward_demodulation,[],[f59969,f1898]) ).
fof(f60006,plain,
! [X2,X0,X1] : rd(mult(X1,ld(mult(X1,X2),X0)),mult(X2,ld(mult(X1,X2),X0))) = rd(X0,mult(X2,mult(rd(X2,mult(X1,X2)),X0))),
inference(backward_demodulation,[],[f8399,f59991]) ).
fof(f60011,plain,
! [X2,X0,X1] : rd(X0,mult(X2,ld(X1,X0))) = rd(mult(X1,ld(mult(X1,X2),X0)),mult(X2,ld(mult(X1,X2),X0))),
inference(forward_demodulation,[],[f60006,f1252]) ).
fof(f94948,plain,
! [X2,X3,X0,X1] : rd(mult(mult(rd(X0,X1),X2),X3),mult(X2,X3)) = mult(rd(mult(X2,X3),mult(mult(rd(X1,X0),X2),X3)),rd(mult(mult(unit,X2),X3),mult(X2,X3))),
inference(superposition,[],[f1931,f1957]) ).
fof(f95509,plain,
! [X2,X3,X0,X1] : rd(mult(mult(rd(X0,X1),X2),X3),mult(X2,X3)) = mult(rd(mult(X2,X3),mult(mult(rd(X1,X0),X2),X3)),rd(mult(X2,X3),mult(X2,X3))),
inference(forward_demodulation,[],[f94948,f6]) ).
fof(f95884,plain,
! [X2,X3,X0,X1] : rd(mult(mult(rd(X0,X1),X2),X3),mult(X2,X3)) = rd(mult(X2,X3),mult(mult(rd(X1,X0),X2),X3)),
inference(forward_demodulation,[],[f95509,f642]) ).
fof(f96148,plain,
! [X2,X3,X0,X1] : mult(rd(mult(mult(X1,X3),X2),mult(X3,X2)),rd(X0,mult(X3,X2))) = rd(mult(X3,X2),mult(mult(rd(mult(X3,rd(X2,X0)),X1),X3),X2)),
inference(backward_demodulation,[],[f8071,f95884]) ).
fof(f97696,plain,
! [X2,X0,X1] : mult(rd(mult(mult(X0,X0),X1),mult(X0,X1)),rd(X2,mult(X0,X1))) = rd(mult(X0,X1),mult(mult(X0,rd(X1,X2)),X1)),
inference(superposition,[],[f96148,f3]) ).
fof(f97805,plain,
! [X2,X0,X1] : rd(mult(X0,X1),mult(mult(X0,rd(X1,X2)),X1)) = mult(rd(mult(X0,mult(X0,X1)),mult(X0,X1)),rd(X2,mult(X0,X1))),
inference(forward_demodulation,[],[f97696,f9051]) ).
fof(f97992,plain,
! [X2,X0,X1] : mult(X0,rd(X2,mult(X0,X1))) = rd(mult(X0,X1),mult(mult(X0,rd(X1,X2)),X1)),
inference(forward_demodulation,[],[f97805,f4]) ).
fof(f98984,plain,
! [X2,X0,X1] : mult(X1,rd(X2,mult(X1,mult(X0,X2)))) = rd(mult(X1,mult(X0,X2)),mult(mult(X1,X0),mult(X0,X2))),
inference(superposition,[],[f97992,f4]) ).
fof(f99735,plain,
! [X2,X0,X1] : mult(rd(X0,mult(X1,X2)),rd(X2,X0)) = rd(X0,mult(mult(rd(X0,mult(X1,X2)),X1),mult(X1,X2))),
inference(superposition,[],[f98984,f3]) ).
fof(f99853,plain,
! [X2,X0,X1] : mult(X1,rd(ld(X2,X0),mult(X1,X0))) = rd(mult(X1,X0),mult(mult(X1,X2),X0)),
inference(superposition,[],[f98984,f1]) ).
fof(f100101,plain,
! [X2,X0,X1] : rd(mult(X1,X0),mult(mult(X1,X2),X0)) = rd(X1,mult(mult(X1,X0),ld(X0,X2))),
inference(forward_demodulation,[],[f99853,f5960]) ).
fof(f100148,plain,
! [X2,X0,X1] : mult(rd(X0,mult(X1,X2)),rd(X2,X0)) = rd(X0,mult(mult(rd(X0,X2),X1),X2)),
inference(forward_demodulation,[],[f99735,f23491]) ).
fof(f100710,plain,
! [X2,X0,X1] : rd(mult(X2,ld(mult(X2,X1),X0)),mult(mult(rd(mult(X2,ld(mult(X2,X1),X0)),ld(mult(X2,X1),X0)),X1),ld(mult(X2,X1),X0))) = mult(rd(X0,mult(X1,ld(X2,X0))),rd(ld(mult(X2,X1),X0),mult(X2,ld(mult(X2,X1),X0)))),
inference(superposition,[],[f100148,f60011]) ).
fof(f100752,plain,
! [X2,X0,X1] : rd(X1,mult(mult(rd(X1,ld(X0,X1)),X2),ld(X0,X1))) = mult(rd(X1,mult(X2,ld(X0,X1))),i(X0)),
inference(superposition,[],[f100148,f481]) ).
fof(f101095,plain,
! [X2,X0,X1] : rd(X1,mult(mult(rd(X1,ld(X0,X1)),X2),ld(X0,X1))) = rd(rd(X1,mult(X2,ld(X0,X1))),X0),
inference(forward_demodulation,[],[f100752,f38]) ).
fof(f101130,plain,
! [X2,X0,X1] : rd(mult(X2,ld(mult(X2,X1),X0)),mult(mult(rd(mult(X2,ld(mult(X2,X1),X0)),ld(mult(X2,X1),X0)),X1),ld(mult(X2,X1),X0))) = rd(rd(X0,mult(X1,ld(X2,X0))),X2),
inference(forward_demodulation,[],[f100710,f1256]) ).
fof(f101363,plain,
! [X2,X0,X1] : rd(rd(X1,mult(X2,ld(X0,X1))),X0) = rd(X1,mult(mult(mult(X1,ld(X1,X0)),X2),ld(X0,X1))),
inference(forward_demodulation,[],[f101095,f5031]) ).
fof(f101389,plain,
! [X2,X0,X1] : rd(rd(X0,mult(X1,ld(X2,X0))),X2) = rd(mult(X2,ld(mult(X2,X1),X0)),mult(mult(X2,X1),ld(mult(X2,X1),X0))),
inference(forward_demodulation,[],[f101130,f4]) ).
fof(f101546,plain,
! [X2,X0,X1] : rd(X1,mult(mult(X0,X2),ld(X0,X1))) = rd(rd(X1,mult(X2,ld(X0,X1))),X0),
inference(forward_demodulation,[],[f101363,f1]) ).
fof(f101565,plain,
! [X2,X0,X1] : rd(rd(X0,mult(X1,ld(X2,X0))),X2) = rd(mult(X2,ld(mult(X2,X1),X0)),X0),
inference(forward_demodulation,[],[f101389,f1]) ).
fof(f101701,plain,
! [X2,X0,X1] : rd(X0,mult(mult(X2,X1),ld(X2,X0))) = rd(mult(X2,ld(mult(X2,X1),X0)),X0),
inference(forward_demodulation,[],[f101565,f101546]) ).
fof(f102765,plain,
! [X2,X0,X1] : rd(X0,mult(mult(X1,X2),ld(X1,X0))) = rd(X1,mult(X0,ld(ld(X1,X0),X2))),
inference(superposition,[],[f100101,f1]) ).
fof(f103187,plain,
! [X2,X0,X1] : rd(X0,mult(mult(X1,X2),ld(X1,X0))) = rd(X1,mult(X0,mult(ld(X0,X1),X2))),
inference(forward_demodulation,[],[f102765,f5032]) ).
fof(f103565,plain,
! [X2,X0,X1] : rd(mult(X2,ld(X0,X1)),X1) = rd(X1,mult(X0,ld(X2,X1))),
inference(superposition,[],[f101701,f1]) ).
fof(f104107,plain,
! [X2,X0,X1] : mult(mult(X0,X1),ld(X1,X2)) = rd(X2,mult(X1,ld(mult(mult(X0,X2),X1),X2))),
inference(backward_demodulation,[],[f14696,f103565]) ).
fof(f105000,plain,
! [X2,X0,X1] : rd(mult(X2,mult(X0,X1)),X1) = rd(X1,mult(i(X0),ld(X2,X1))),
inference(superposition,[],[f103565,f28]) ).
fof(f105127,plain,
! [X2,X0,X1] : mult(mult(X2,ld(X1,i(X0))),X0) = rd(i(X0),mult(X1,ld(X2,i(X0)))),
inference(superposition,[],[f41,f103565]) ).
fof(f105128,plain,
! [X2,X0,X1] : mult(mult(X2,ld(X1,i(X0))),X0) = i(mult(mult(X1,ld(X2,i(X0))),X0)),
inference(forward_demodulation,[],[f105127,f509]) ).
fof(f105225,plain,
! [X2,X0,X1] : rd(mult(X2,mult(X0,X1)),X1) = rd(X1,ld(X0,ld(X2,X1))),
inference(forward_demodulation,[],[f105000,f26]) ).
fof(f105276,plain,
! [X2,X0,X1] : mult(mult(X2,ld(X1,i(X0))),X0) = i(mult(mult(X1,i(mult(X0,X2))),X0)),
inference(forward_demodulation,[],[f105128,f956]) ).
fof(f105380,plain,
! [X2,X0,X1] : rd(mult(X2,mult(X0,X1)),X1) = mult(X1,ld(ld(X2,X1),X0)),
inference(forward_demodulation,[],[f105225,f5031]) ).
fof(f105412,plain,
! [X2,X0,X1] : mult(mult(X2,ld(X1,i(X0))),X0) = i(mult(rd(X1,mult(X0,X2)),X0)),
inference(forward_demodulation,[],[f105276,f38]) ).
fof(f105485,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X2),X0)) = rd(mult(X2,mult(X0,X1)),X1),
inference(forward_demodulation,[],[f105380,f5032]) ).
fof(f105516,plain,
! [X2,X0,X1] : mult(mult(X2,ld(X1,i(X0))),X0) = ld(X0,rd(mult(X0,X2),X1)),
inference(forward_demodulation,[],[f105412,f1692]) ).
fof(f105589,plain,
! [X2,X0,X1] : mult(X2,mult(ld(X2,X0),ld(X0,X1))) = ld(X0,rd(mult(X0,mult(X1,X2)),X2)),
inference(backward_demodulation,[],[f5653,f105485]) ).
fof(f105639,plain,
! [X2,X0,X1] : rd(mult(X0,mult(X2,X1)),X1) = ld(X0,mult(X1,mult(ld(X1,X0),mult(X0,X2)))),
inference(backward_demodulation,[],[f46651,f105485]) ).
fof(f105852,plain,
! [X2,X0,X1] : rd(X0,mult(mult(X1,X2),ld(X1,X0))) = rd(X1,rd(mult(X1,mult(X2,X0)),X0)),
inference(backward_demodulation,[],[f103187,f105485]) ).
fof(f106989,plain,
! [X2,X0,X1] : mult(mult(X2,i(mult(X0,X1))),X0) = ld(X0,rd(mult(X0,X2),X1)),
inference(forward_demodulation,[],[f105516,f956]) ).
fof(f108180,plain,
! [X2,X0,X1] : rd(X0,mult(mult(X1,X2),ld(X1,X0))) = mult(X1,rd(X0,mult(X1,mult(X2,X0)))),
inference(forward_demodulation,[],[f105852,f1416]) ).
fof(f108353,plain,
! [X2,X0,X1] : rd(mult(X0,mult(X2,X1)),X1) = ld(X0,rd(mult(X0,mult(mult(X0,X2),X1)),X1)),
inference(forward_demodulation,[],[f105639,f105485]) ).
fof(f108389,plain,
! [X2,X0,X1] : rd(mult(X0,mult(ld(X0,X1),X2)),X2) = ld(X0,rd(mult(X0,mult(X1,X2)),X2)),
inference(forward_demodulation,[],[f105589,f105485]) ).
fof(f108421,plain,
! [X2,X0,X1] : mult(rd(X2,mult(X0,X1)),X0) = ld(X0,rd(mult(X0,X2),X1)),
inference(forward_demodulation,[],[f106989,f38]) ).
fof(f109010,plain,
! [X2,X0,X1] : rd(X2,mult(X1,ld(X0,X2))) = mult(mult(X0,rd(X2,mult(X0,mult(X1,X2)))),X0),
inference(backward_demodulation,[],[f31476,f108180]) ).
fof(f109225,plain,
! [X2,X0,X1] : ld(X0,rd(mult(X0,mult(X1,X2)),X2)) = rd(rd(mult(X1,mult(X2,X0)),X0),X2),
inference(forward_demodulation,[],[f108389,f105485]) ).
fof(f109258,plain,
! [X2,X0,X1] : rd(mult(X0,mult(X2,X1)),X1) = mult(rd(mult(mult(X0,X2),X1),mult(X0,X1)),X0),
inference(backward_demodulation,[],[f108353,f108421]) ).
fof(f109527,plain,
! [X2,X0,X1] : rd(X2,mult(X1,ld(X0,X2))) = mult(X0,mult(rd(X2,mult(X0,mult(X1,X2))),X0)),
inference(forward_demodulation,[],[f109010,f278]) ).
fof(f109626,plain,
! [X2,X0,X1] : mult(rd(mult(X1,X2),mult(X0,X2)),X0) = rd(rd(mult(X1,mult(X2,X0)),X0),X2),
inference(forward_demodulation,[],[f109225,f108421]) ).
fof(f109643,plain,
! [X2,X0,X1] : rd(mult(X0,mult(X2,X1)),X1) = rd(mult(mult(mult(X0,X2),X0),X1),mult(X0,X1)),
inference(forward_demodulation,[],[f109258,f8447]) ).
fof(f109836,plain,
! [X2,X0,X1] : rd(mult(mult(X1,X0),X2),mult(X0,X2)) = rd(rd(mult(X1,mult(X2,X0)),X0),X2),
inference(forward_demodulation,[],[f109626,f8447]) ).
fof(f109852,plain,
! [X2,X0,X1] : rd(mult(X0,mult(X2,X1)),X1) = rd(mult(mult(X0,mult(X2,X0)),X1),mult(X0,X1)),
inference(forward_demodulation,[],[f109643,f278]) ).
fof(f109942,plain,
! [X2,X0,X1] : rd(mult(X2,mult(X0,X1)),X1) = rd(mult(mult(mult(X2,X0),X1),X0),mult(X1,X0)),
inference(backward_demodulation,[],[f31420,f109836]) ).
fof(f109956,plain,
! [X2,X0,X1] : mult(X1,mult(rd(X0,mult(X1,X2)),X1)) = rd(mult(X1,mult(rd(X0,X2),X2)),X2),
inference(backward_demodulation,[],[f23484,f109852]) ).
fof(f110006,plain,
! [X2,X0,X1] : rd(mult(X1,X0),X2) = mult(X1,mult(rd(X0,mult(X1,X2)),X1)),
inference(forward_demodulation,[],[f109956,f3]) ).
fof(f110039,plain,
! [X2,X0,X1] : rd(mult(X0,X2),mult(X1,X2)) = rd(X2,mult(X1,ld(X0,X2))),
inference(backward_demodulation,[],[f109527,f110006]) ).
fof(f110325,plain,
! [X2,X0,X1] : mult(mult(X0,X1),ld(X1,X2)) = rd(mult(mult(mult(X0,X2),X1),X2),mult(X1,X2)),
inference(backward_demodulation,[],[f104107,f110039]) ).
fof(f110810,plain,
! [X2,X0,X1] : mult(mult(X0,X1),ld(X1,X2)) = rd(mult(X0,mult(X2,X1)),X1),
inference(forward_demodulation,[],[f110325,f109942]) ).
fof(f113553,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X0) = rd(mult(X1,mult(mult(X2,X0),X2)),X2),
inference(superposition,[],[f110810,f2]) ).
fof(f113846,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X0) = rd(mult(X1,mult(X2,mult(X0,X2))),X2),
inference(forward_demodulation,[],[f113553,f278]) ).
fof(f158536,plain,
( ! [X0] : mult(mult(X0,b),c) = rd(mult(X0,mult(b,sF0)),b)
| ~ spl6_5 ),
inference(superposition,[],[f113846,f114]) ).
fof(f158713,plain,
( ! [X0] : mult(mult(X0,b),c) = rd(mult(X0,sF1),b)
| ~ spl6_5
| ~ spl6_6 ),
inference(forward_demodulation,[],[f158536,f121]) ).
fof(f160886,plain,
( mult(mult(a,b),c) = rd(sF2,b)
| ~ spl6_1
| ~ spl6_5
| ~ spl6_6 ),
inference(superposition,[],[f158713,f34]) ).
fof(f160939,plain,
( mult(sF3,c) = rd(sF2,b)
| ~ spl6_1
| ~ spl6_4
| ~ spl6_5
| ~ spl6_6 ),
inference(forward_demodulation,[],[f160886,f107]) ).
fof(f160955,plain,
( sF4 = rd(sF2,b)
| ~ spl6_1
| ~ spl6_4
| ~ spl6_5
| ~ spl6_6
| ~ spl6_7 ),
inference(forward_demodulation,[],[f160939,f205]) ).
fof(f160965,definition,
( spl6_51
<=> sF4 = rd(sF2,b) ),
introduced(definition,[new_symbols(definition,[spl6_51])],[avatar_definition]) ).
fof(f160967,plain,
( sF4 = rd(sF2,b)
| ~ spl6_51 ),
inference(avatar_component_clause,[],[f160965]) ).
fof(f160968,plain,
( spl6_51
| ~ spl6_1
| ~ spl6_4
| ~ spl6_5
| ~ spl6_6
| ~ spl6_7 ),
inference(avatar_split_clause,[],[f160955,f203,f119,f112,f105,f32,f160965]) ).
fof(f160969,plain,
( sF2 = mult(sF4,b)
| ~ spl6_51 ),
inference(superposition,[],[f3,f160967]) ).
fof(f161003,plain,
( sF2 = sF5
| ~ spl6_2
| ~ spl6_51 ),
inference(forward_demodulation,[],[f160969,f92]) ).
fof(f161004,plain,
( $false
| ~ spl6_2
| spl6_3
| ~ spl6_51 ),
inference(forward_subsumption_resolution,[],[f161003,f102]) ).
fof(f161005,plain,
( ~ spl6_2
| spl6_3
| ~ spl6_51 ),
inference(avatar_contradiction_clause,[],[f161004]) ).
cnf(s1,plain,
spl6_1,
inference(sat_conversion,[],[f35]) ).
cnf(s2,plain,
spl6_2,
inference(sat_conversion,[],[f93]) ).
cnf(s3,plain,
~ spl6_3,
inference(sat_conversion,[],[f103]) ).
cnf(s4,plain,
spl6_4,
inference(sat_conversion,[],[f108]) ).
cnf(s5,plain,
spl6_5,
inference(sat_conversion,[],[f115]) ).
cnf(s6,plain,
spl6_6,
inference(sat_conversion,[],[f122]) ).
cnf(s7,plain,
spl6_7,
inference(sat_conversion,[],[f206]) ).
cnf(s51,plain,
( ~ spl6_1
| ~ spl6_4
| ~ spl6_5
| ~ spl6_6
| ~ spl6_7
| spl6_51 ),
inference(sat_conversion,[],[f160968]) ).
cnf(s52,plain,
( ~ spl6_2
| spl6_3
| ~ spl6_51 ),
inference(sat_conversion,[],[f161005]) ).
cnf(s89,plain,
~ spl6_51,
inference(rat,[],[s52,s3,s2]) ).
cnf(s93,plain,
~ spl6_1,
inference(rat,[],[s51,s4,s7,s6,s5,s89]) ).
cnf(s94,plain,
$false,
inference(rat,[],[s1,s93]) ).
fof(f161006,plain,
$false,
inference(avatar_sat_refutation,[],[s94]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP666-3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.39 % Computer : n005.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Sun Sep 27 10:33:32 UTC 2026
% 0.14/0.39 % CPUTime :
% 0.14/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.17/0.43 Running first-order theorem proving
% 0.17/0.43 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
% 83.51/12.45 % (3794756)Detected a unit-equality problem, will run specialized UEQ schedule.
% 83.51/12.45 % (3794780)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2895569420:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 83.51/12.45 % (3794781)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1448077644:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 83.51/12.45 % (3794783)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1849147566:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 83.51/12.45 % (3794778)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1263442514:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 83.51/12.45 % (3794777)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=1972466842:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 83.51/12.45 % (3794782)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=732255339:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 83.51/12.45 % (3794784)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1745528626:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 83.51/12.45 % (3794781)Instruction limit reached!
% 83.51/12.45 % (3794781)------------------------------
% 83.51/12.45 % (3794781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.51/12.45 % (3794781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/12.45 % (3794781)CaDiCaL version: 2.1.3
% 83.51/12.45 % (3794781)Termination reason: Instruction limit
% 83.51/12.45 % (3794781)Termination phase: Saturation
% 83.51/12.45 % (3794781)Time elapsed: 0.088 s
% 83.51/12.45 % (3794781)Peak memory usage: 89 MB
% 83.51/12.45 % (3794781)Instructions burned: 151 (million)
% 83.51/12.45 % (3794782)Instruction limit reached!
% 83.51/12.45 % (3794782)------------------------------
% 83.51/12.45 % (3794782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.51/12.45 % (3794782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/12.45 % (3794782)CaDiCaL version: 2.1.3
% 83.51/12.45 % (3794782)Termination reason: Instruction limit
% 83.51/12.45 % (3794782)Termination phase: Saturation
% 83.51/12.45 % (3794782)Time elapsed: 0.119 s
% 83.51/12.45 % (3794782)Peak memory usage: 89 MB
% 83.51/12.45 % (3794782)Instructions burned: 181 (million)
% 83.51/12.45 % (3794783)Instruction limit reached!
% 83.51/12.45 % (3794783)------------------------------
% 83.51/12.45 % (3794783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.51/12.45 % (3794783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/12.45 % (3794783)CaDiCaL version: 2.1.3
% 83.51/12.45 % (3794783)Termination reason: Instruction limit
% 83.51/12.45 % (3794783)Termination phase: Saturation
% 83.51/12.45 % (3794783)Time elapsed: 0.170 s
% 83.51/12.45 % (3794783)Peak memory usage: 90 MB
% 83.51/12.45 % (3794783)Instructions burned: 258 (million)
% 83.51/12.45 % (3794866)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3739958127:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 83.51/12.45 % (3794871)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4051801643:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 83.51/12.45 % (3794878)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2152939545:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 83.51/12.45 % (3794878)Instruction limit reached!
% 83.51/12.45 % (3794878)------------------------------
% 83.51/12.45 % (3794878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.51/12.45 % (3794878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/12.45 % (3794878)CaDiCaL version: 2.1.3
% 83.51/12.45 % (3794878)Termination reason: Instruction limit
% 83.51/12.45 % (3794878)Termination phase: Saturation
% 83.51/12.45 % (3794878)Time elapsed: 0.120 s
% 129.01/18.80 % (3794878)Peak memory usage: 90 MB
% 129.01/18.80 % (3794878)Instructions burned: 215 (million)
% 129.01/18.80 % (3794902)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=2318914447:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 129.01/18.80 % (3794784)Instruction limit reached!
% 129.01/18.80 % (3794784)------------------------------
% 129.01/18.80 % (3794784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.01/18.80 % (3794784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.01/18.80 % (3794784)CaDiCaL version: 2.1.3
% 129.01/18.80 % (3794784)Termination reason: Instruction limit
% 129.01/18.80 % (3794784)Termination phase: Saturation
% 129.01/18.80 % (3794784)Time elapsed: 0.670 s
% 129.01/18.80 % (3794784)Peak memory usage: 101 MB
% 129.01/18.80 % (3794784)Instructions burned: 1189 (million)
% 129.01/18.80 % (3794902)Instruction limit reached!
% 129.01/18.80 % (3794902)------------------------------
% 129.01/18.80 % (3794902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.01/18.80 % (3794902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.01/18.80 % (3794902)CaDiCaL version: 2.1.3
% 129.01/18.80 % (3794902)Termination reason: Instruction limit
% 129.01/18.80 % (3794902)Termination phase: Saturation
% 129.01/18.80 % (3794902)Time elapsed: 0.183 s
% 129.01/18.80 % (3794902)Peak memory usage: 93 MB
% 129.01/18.80 % (3794902)Instructions burned: 319 (million)
% 129.01/18.80 % (3794932)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=3310991627:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 129.01/18.80 % (3794866)Instruction limit reached!
% 129.01/18.80 % (3794866)------------------------------
% 129.01/18.80 % (3794866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.01/18.80 % (3794866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.01/18.80 % (3794866)CaDiCaL version: 2.1.3
% 129.01/18.80 % (3794866)Termination reason: Instruction limit
% 129.01/18.80 % (3794866)Termination phase: Saturation
% 129.01/18.80 % (3794866)Time elapsed: 0.702 s
% 129.01/18.80 % (3794866)Peak memory usage: 140 MB
% 129.01/18.80 % (3794866)Instructions burned: 2051 (million)
% 129.01/18.80 % (3794981)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2539118784:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2989 on theBenchmark for (2989ds/2836Mi)
% 129.01/18.80 % (3795004)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1229120718:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 129.01/18.80 % (3794981)Instruction limit reached!
% 129.01/18.80 % (3794981)------------------------------
% 129.01/18.80 % (3794981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.01/18.80 % (3794981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.01/18.80 % (3794981)CaDiCaL version: 2.1.3
% 129.01/18.80 % (3794981)Termination reason: Instruction limit
% 129.01/18.80 % (3794981)Termination phase: Saturation
% 129.01/18.80 % (3794981)Time elapsed: 1.736 s
% 129.01/18.80 % (3794981)Peak memory usage: 134 MB
% 129.01/18.80 % (3794981)Instructions burned: 2837 (million)
% 129.01/18.80 % (3795065)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2218977556:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/11832Mi)
% 129.01/18.80 % (3794871)Instruction limit reached!
% 129.01/18.80 % (3794871)------------------------------
% 129.01/18.80 % (3794871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.01/18.80 % (3794871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.01/18.80 % (3794871)CaDiCaL version: 2.1.3
% 129.01/18.80 % (3794871)Termination reason: Instruction limit
% 129.01/18.80 % (3794871)Termination phase: Saturation
% 129.01/18.80 % (3794871)Time elapsed: 2.998 s
% 129.01/18.80 % (3794871)Peak memory usage: 167 MB
% 129.01/18.80 % (3794871)Instructions burned: 4949 (million)
% 129.01/18.80 % (3795067)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=4193238090:i=2279:fgj=on:bd=all_2965 on theBenchmark for (2965ds/2279Mi)
% 129.01/18.80 % (3795067)Instruction limit reached!
% 129.01/18.80 % (3795067)------------------------------
% 124.92/38.10 % (3795067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795067)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795067)Termination reason: Instruction limit
% 124.92/38.10 % (3795067)Termination phase: Saturation
% 124.92/38.10 % (3795067)Time elapsed: 1.380 s
% 124.92/38.10 % (3795067)Peak memory usage: 139 MB
% 124.92/38.10 % (3795067)Instructions burned: 2279 (million)
% 124.92/38.10 % (3795069)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=3210326112:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2950 on theBenchmark for (2950ds/6225Mi)
% 124.92/38.10 % (3794932)Instruction limit reached!
% 124.92/38.10 % (3794932)------------------------------
% 124.92/38.10 % (3794932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3794932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3794932)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3794932)Termination reason: Instruction limit
% 124.92/38.10 % (3794932)Termination phase: Saturation
% 124.92/38.10 % (3794932)Time elapsed: 4.164 s
% 124.92/38.10 % (3794932)Peak memory usage: 244 MB
% 124.92/38.10 % (3794932)Instructions burned: 12128 (million)
% 124.92/38.10 % (3795071)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=706898314:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2948 on theBenchmark for (2948ds/21755Mi)
% 124.92/38.10 % (3795069)Instruction limit reached!
% 124.92/38.10 % (3795069)------------------------------
% 124.92/38.10 % (3795069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795069)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795069)Termination reason: Instruction limit
% 124.92/38.10 % (3795069)Termination phase: Saturation
% 124.92/38.10 % (3795069)Time elapsed: 2.702 s
% 124.92/38.10 % (3795069)Peak memory usage: 143 MB
% 124.92/38.10 % (3795069)Instructions burned: 6226 (million)
% 124.92/38.10 % (3795073)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=1810459837:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2921 on theBenchmark for (2921ds/16427Mi)
% 124.92/38.10 % (3795004)Instruction limit reached!
% 124.92/38.10 % (3795004)------------------------------
% 124.92/38.10 % (3795004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795004)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795004)Termination reason: Instruction limit
% 124.92/38.10 % (3795004)Termination phase: Saturation
% 124.92/38.10 % (3795004)Time elapsed: 8.733 s
% 124.92/38.10 % (3795004)Peak memory usage: 245 MB
% 124.92/38.10 % (3795004)Instructions burned: 14534 (million)
% 124.92/38.10 % (3795075)lrs+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=1838747445:i=9356:fgj=on:bd=preordered:av=off_2900 on theBenchmark for (2900ds/9356Mi)
% 124.92/38.10 % (3795065)Instruction limit reached!
% 124.92/38.10 % (3795065)------------------------------
% 124.92/38.10 % (3795065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795065)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795065)Termination reason: Instruction limit
% 124.92/38.10 % (3795065)Termination phase: Saturation
% 124.92/38.10 % (3795065)Time elapsed: 7.381 s
% 124.92/38.10 % (3795065)Peak memory usage: 227 MB
% 124.92/38.10 % (3795065)Instructions burned: 11833 (million)
% 124.92/38.10 % (3795077)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=365181772:i=2070:kws=inv_precedence:slsql=off:bd=all_2895 on theBenchmark for (2895ds/2070Mi)
% 124.92/38.10 % (3795077)Instruction limit reached!
% 124.92/38.10 % (3795077)------------------------------
% 124.92/38.10 % (3795077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795077)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795077)Termination reason: Instruction limit
% 124.92/38.10 % (3795077)Termination phase: Saturation
% 124.92/38.10 % (3795077)Time elapsed: 1.172 s
% 124.92/38.10 % (3795077)Peak memory usage: 122 MB
% 124.92/38.10 % (3795077)Instructions burned: 2071 (million)
% 124.92/38.10 % (3795079)lrs+1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=8000:tgt=ground:npcc=on:fde=unused:sp=const_min:urr=ec_only:s2agt=32:random_seed=1340112825:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2881 on theBenchmark for (2881ds/6461Mi)
% 124.92/38.10 % (3795071)Instruction limit reached!
% 124.92/38.10 % (3795071)------------------------------
% 124.92/38.10 % (3795071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795071)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795071)Termination reason: Instruction limit
% 124.92/38.10 % (3795071)Termination phase: Saturation
% 124.92/38.10 % (3795071)Time elapsed: 8.601 s
% 124.92/38.10 % (3795071)Peak memory usage: 226 MB
% 124.92/38.10 % (3795071)Instructions burned: 21756 (million)
% 124.92/38.10 % (3795213)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=2925532340:i=2310:bd=all:ss=included_2860 on theBenchmark for (2860ds/2310Mi)
% 124.92/38.10 % (3795213)Instruction limit reached!
% 124.92/38.10 % (3795213)------------------------------
% 124.92/38.10 % (3795213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795213)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795213)Termination reason: Instruction limit
% 124.92/38.10 % (3795213)Termination phase: Saturation
% 124.92/38.10 % (3795213)Time elapsed: 0.753 s
% 124.92/38.10 % (3795213)Peak memory usage: 99 MB
% 124.92/38.10 % (3795213)Instructions burned: 2310 (million)
% 124.92/38.10 % (3795326)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=3257124541:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2851 on theBenchmark for (2851ds/2616Mi)
% 124.92/38.10 % (3795079)Instruction limit reached!
% 124.92/38.10 % (3795079)------------------------------
% 124.92/38.10 % (3795079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795079)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795079)Termination reason: Instruction limit
% 124.92/38.10 % (3795079)Termination phase: Saturation
% 124.92/38.10 % (3795079)Time elapsed: 4.313 s
% 124.92/38.10 % (3795079)Peak memory usage: 177 MB
% 124.92/38.10 % (3795079)Instructions burned: 6462 (million)
% 124.92/38.10 % (3795326)Instruction limit reached!
% 124.92/38.10 % (3795326)------------------------------
% 124.92/38.10 % (3795326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795326)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795326)Termination reason: Instruction limit
% 124.92/38.10 % (3795326)Termination phase: Saturation
% 124.92/38.10 % (3795326)Time elapsed: 1.268 s
% 124.92/38.10 % (3795326)Peak memory usage: 123 MB
% 124.92/38.10 % (3795326)Instructions burned: 2617 (million)
% 124.92/38.10 % (3795366)lrs+11_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:tgt=full:npcc=on:prc=on:fde=unused:sp=reverse_frequency:spb=goal:acc=on:urr=ec_only:s2agt=32:random_seed=3260187233:i=3258:fgj=on:bd=all:ins=1_2836 on theBenchmark for (2836ds/3258Mi)
% 124.92/38.10 % (3795075)Instruction limit reached!
% 124.92/38.10 % (3795075)------------------------------
% 124.92/38.10 % (3795075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795075)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795075)Termination reason: Instruction limit
% 124.92/38.10 % (3795075)Termination phase: Saturation
% 124.92/38.10 % (3795075)Time elapsed: 6.400 s
% 124.92/38.10 % (3795075)Peak memory usage: 195 MB
% 124.92/38.10 % (3795075)Instructions burned: 9356 (million)
% 124.92/38.10 % (3795365)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=2416541608:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2836 on theBenchmark for (2836ds/30521Mi)
% 124.92/38.10 % (3795372)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=2972970826:i=5037:kws=precedence_2834 on theBenchmark for (2834ds/5037Mi)
% 124.92/38.10 % (3795366)Instruction limit reached!
% 124.92/38.10 % (3795366)------------------------------
% 124.92/38.10 % (3795366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795366)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795366)Termination reason: Instruction limit
% 124.92/38.10 % (3795366)Termination phase: Saturation
% 124.92/38.10 % (3795366)Time elapsed: 1.644 s
% 124.92/38.10 % (3795366)Peak memory usage: 145 MB
% 124.92/38.10 % (3795366)Instructions burned: 3264 (million)
% 124.92/38.10 % (3795381)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=3577377488:i=65240_2818 on theBenchmark for (2818ds/65240Mi)
% 124.92/38.10 % (3795073)Instruction limit reached!
% 124.92/38.10 % (3795073)------------------------------
% 124.92/38.10 % (3795073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795073)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795073)Termination reason: Instruction limit
% 124.92/38.10 % (3795073)Termination phase: Saturation
% 124.92/38.10 % (3795073)Time elapsed: 12.581 s
% 124.92/38.10 % (3795073)Peak memory usage: 245 MB
% 124.92/38.10 % (3795073)Instructions burned: 16427 (million)
% 124.92/38.10 % (3795389)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=4287206431:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2793 on theBenchmark for (2793ds/16502Mi)
% 124.92/38.10 % (3795372)Instruction limit reached!
% 124.92/38.10 % (3795372)------------------------------
% 124.92/38.10 % (3795372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795372)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795372)Termination reason: Instruction limit
% 124.92/38.10 % (3795372)Termination phase: Saturation
% 124.92/38.10 % (3795372)Time elapsed: 5.052 s
% 124.92/38.10 % (3795372)Peak memory usage: 168 MB
% 124.92/38.10 % (3795372)Instructions burned: 5037 (million)
% 124.92/38.10 % (3795395)lrs-1011_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=32000:npcc=on:drc=off:sp=const_max:spb=goal_then_units:urr=ec_only:fd=preordered:random_seed=857893742:i=7623:bd=preordered:er=filter_2781 on theBenchmark for (2781ds/7623Mi)
% 124.92/38.10 % (3795395)Instruction limit reached!
% 124.92/38.10 % (3795395)------------------------------
% 124.92/38.10 % (3795395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.92/38.10 % (3795395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.92/38.10 % (3795395)CaDiCaL version: 2.1.3
% 124.92/38.10 % (3795395)Termination reason: Instruction limit
% 124.92/38.10 % (3795395)Termination phase: Saturation
% 124.92/38.10 % (3795395)Time elapsed: 7.906 s
% 124.92/38.10 % (3795395)Peak memory usage: 179 MB
% 124.92/38.10 % (3795395)Instructions burned: 7623 (million)
% 124.92/38.10 % (3795409)dis+1010_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:tgt=full:npcc=on:sp=const_min:spb=non_intro:lcm=predicate:acc=on:urr=ec_only:rp=on:gs=on:random_seed=925756177:i=8183:kws=frequency:add=off:gsp=on_2699 on theBenchmark for (2699ds/8183Mi)
% 124.92/38.10 % (3794777)First to succeed.
% 124.92/38.10 % (3794777)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3794756"
% 124.92/38.10 % (3794777)Refutation found. Thanks to Tanya!
% 124.92/38.10 % SZS status Unsatisfiable for theBenchmark
% 124.92/38.10 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/38.40 % (3794777)------------------------------
% 0.19/38.40 % (3794777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/38.40 % (3794777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/38.40 % (3794777)CaDiCaL version: 2.1.3
% 0.19/38.40 % (3794777)Termination reason: Refutation
% 0.19/38.40 % (3794777)Time elapsed: 36.649 s
% 0.19/38.40 % (3794777)Peak memory usage: 410 MB
% 0.19/38.40 % (3794777)Instructions burned: 42564 (million)
% 0.19/38.40 % (3794777)------------------------------
% 0.19/38.40 % (3794777)------------------------------
% 0.19/38.40 % (3794756)Success in time 37.452 s
% 0.19/38.40 % Vampire exiting
%------------------------------------------------------------------------------