%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP666-4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 152.17s 36.36s
% Output : Refutation 252.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 85
% Number of leaves : 26
% Syntax : Number of formulae : 325 ( 297 unt; 14 def)
% Number of atoms : 379 ( 302 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 105 ( 51 ~; 46 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 9 ( 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 : 701 ( 0 sgn 701 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c01) ).
fof(f2,axiom,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c04) ).
fof(f5,axiom,
! [X0] : mult(X0,unit) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c05) ).
fof(f6,axiom,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',c09) ).
fof(f10,axiom,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c10) ).
fof(f11,axiom,
! [X0,X1] : mult(mult(X0,X1),i(X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c11) ).
fof(f12,negated_conjecture,
mult(mult(a,b),mult(c,a)) != mult(mult(a,mult(b,c)),a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f13,definition,
sF0 = mult(a,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f14,plain,
mult(a,b) = sF0,
inference(reorient_equations,[],[f13]) ).
fof(f15,definition,
sF1 = mult(c,a),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f16,plain,
mult(c,a) = sF1,
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF2 = mult(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f18,plain,
mult(sF0,sF1) = sF2,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF3 = mult(b,c),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f20,plain,
mult(b,c) = sF3,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF4 = mult(a,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f22,plain,
mult(a,sF3) = sF4,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF5 = mult(sF4,a),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f24,plain,
mult(sF4,a) = 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,plain,
! [X0,X1] : mult(X0,i(ld(X1,X0))) = X1,
inference(superposition,[],[f11,f1]) ).
fof(f33,plain,
! [X0,X1] : rd(X0,X1) = mult(X0,i(X1)),
inference(superposition,[],[f11,f3]) ).
fof(f34,plain,
! [X0,X1] : mult(X0,X1) = mult(X0,i(i(X1))),
inference(superposition,[],[f11,f11]) ).
fof(f35,plain,
! [X0,X1] : i(X1) = ld(mult(X0,X1),X0),
inference(superposition,[],[f2,f11]) ).
fof(f36,plain,
! [X0,X1] : mult(X0,X1) = rd(X0,i(X1)),
inference(backward_demodulation,[],[f34,f33]) ).
fof(f38,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(forward_demodulation,[],[f32,f33]) ).
fof(f40,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(f44,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(f50,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(f57,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(f61,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(f63,plain,
! [X0,X1] : ld(X0,mult(mult(X1,X0),X0)) = mult(ld(X0,mult(X1,X0)),X0),
inference(superposition,[],[f9,f2]) ).
fof(f64,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(f75,definition,
( spl6_1
<=> mult(sF4,a) = sF5 ),
introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition]) ).
fof(f77,plain,
( mult(sF4,a) = sF5
| ~ spl6_1 ),
inference(avatar_component_clause,[],[f75]) ).
fof(f78,plain,
spl6_1,
inference(avatar_split_clause,[],[f24,f75]) ).
fof(f80,definition,
( spl6_2
<=> mult(sF0,sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition]) ).
fof(f82,plain,
( mult(sF0,sF1) = sF2
| ~ spl6_2 ),
inference(avatar_component_clause,[],[f80]) ).
fof(f83,plain,
spl6_2,
inference(avatar_split_clause,[],[f18,f80]) ).
fof(f89,definition,
( spl6_3
<=> sF2 = sF5 ),
introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition]) ).
fof(f91,plain,
( sF2 != sF5
| spl6_3 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f92,plain,
~ spl6_3,
inference(avatar_split_clause,[],[f25,f89]) ).
fof(f94,definition,
( spl6_4
<=> mult(a,b) = sF0 ),
introduced(definition,[new_symbols(definition,[spl6_4])],[avatar_definition]) ).
fof(f96,plain,
( mult(a,b) = sF0
| ~ spl6_4 ),
inference(avatar_component_clause,[],[f94]) ).
fof(f97,plain,
spl6_4,
inference(avatar_split_clause,[],[f14,f94]) ).
fof(f101,definition,
( spl6_5
<=> mult(a,sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl6_5])],[avatar_definition]) ).
fof(f103,plain,
( mult(a,sF3) = sF4
| ~ spl6_5 ),
inference(avatar_component_clause,[],[f101]) ).
fof(f104,plain,
spl6_5,
inference(avatar_split_clause,[],[f22,f101]) ).
fof(f108,definition,
( spl6_6
<=> mult(b,c) = sF3 ),
introduced(definition,[new_symbols(definition,[spl6_6])],[avatar_definition]) ).
fof(f110,plain,
( mult(b,c) = sF3
| ~ spl6_6 ),
inference(avatar_component_clause,[],[f108]) ).
fof(f111,plain,
spl6_6,
inference(avatar_split_clause,[],[f20,f108]) ).
fof(f115,definition,
( spl6_7
<=> mult(c,a) = sF1 ),
introduced(definition,[new_symbols(definition,[spl6_7])],[avatar_definition]) ).
fof(f117,plain,
( mult(c,a) = sF1
| ~ spl6_7 ),
inference(avatar_component_clause,[],[f115]) ).
fof(f118,plain,
spl6_7,
inference(avatar_split_clause,[],[f16,f115]) ).
fof(f123,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(f145,plain,
! [X2,X3,X0,X1] : ld(mult(X1,X2),mult(X1,mult(X2,mult(X3,ld(X2,X0))))) = mult(ld(mult(X1,X2),mult(X1,mult(X2,X3))),ld(mult(X1,X2),mult(X1,X0))),
inference(superposition,[],[f7,f1]) ).
fof(f214,plain,
! [X0,X1] : ld(X1,mult(X0,X1)) = mult(ld(X1,X0),X1),
inference(superposition,[],[f63,f3]) ).
fof(f223,plain,
! [X0,X1] : ld(i(X0),mult(mult(X1,i(X0)),i(X0))) = mult(mult(X0,mult(X1,i(X0))),i(X0)),
inference(superposition,[],[f63,f28]) ).
fof(f225,plain,
! [X0,X1] : ld(X0,mult(X1,X0)) = rd(ld(X0,mult(mult(X1,X0),X0)),X0),
inference(superposition,[],[f4,f63]) ).
fof(f231,plain,
! [X0,X1] : ld(i(X0),mult(mult(X1,i(X0)),i(X0))) = rd(mult(X0,mult(X1,i(X0))),X0),
inference(forward_demodulation,[],[f223,f33]) ).
fof(f235,plain,
! [X0,X1] : ld(i(X0),mult(rd(X1,X0),i(X0))) = rd(mult(X0,rd(X1,X0)),X0),
inference(forward_demodulation,[],[f231,f33]) ).
fof(f237,plain,
! [X0,X1] : rd(mult(X0,rd(X1,X0)),X0) = mult(X0,mult(rd(X1,X0),i(X0))),
inference(forward_demodulation,[],[f235,f28]) ).
fof(f238,plain,
! [X0,X1] : rd(mult(X0,rd(X1,X0)),X0) = mult(X0,rd(rd(X1,X0),X0)),
inference(forward_demodulation,[],[f237,f33]) ).
fof(f239,plain,
! [X0,X1] : rd(mult(X1,X0),X1) = mult(X1,rd(X0,X1)),
inference(superposition,[],[f238,f4]) ).
fof(f252,plain,
! [X0,X1] : mult(X1,X0) = rd(mult(X1,mult(X0,X1)),X1),
inference(superposition,[],[f239,f4]) ).
fof(f274,plain,
! [X0,X1] : mult(mult(X0,X1),X0) = mult(X0,mult(X1,X0)),
inference(superposition,[],[f3,f252]) ).
fof(f287,plain,
( mult(sF4,a) = mult(a,mult(sF3,a))
| ~ spl6_5 ),
inference(superposition,[],[f274,f103]) ).
fof(f299,plain,
( sF5 = mult(a,mult(sF3,a))
| ~ spl6_1
| ~ spl6_5 ),
inference(forward_demodulation,[],[f287,f77]) ).
fof(f311,plain,
! [X0] : ld(X0,X0) = rd(ld(X0,mult(X0,X0)),X0),
inference(superposition,[],[f225,f6]) ).
fof(f326,plain,
! [X0] : rd(X0,X0) = ld(X0,X0),
inference(forward_demodulation,[],[f311,f2]) ).
fof(f395,plain,
! [X2,X0,X1] : ld(mult(X0,X1),X0) = ld(mult(X2,X1),X2),
inference(superposition,[],[f35,f35]) ).
fof(f396,plain,
! [X0,X1] : ld(X0,X1) = i(ld(X1,X0)),
inference(superposition,[],[f35,f1]) ).
fof(f397,plain,
! [X0] : ld(X0,X0) = i(unit),
inference(superposition,[],[f35,f5]) ).
fof(f401,plain,
! [X0] : i(X0) = ld(X0,unit),
inference(superposition,[],[f35,f6]) ).
fof(f413,plain,
! [X0] : rd(X0,X0) = i(unit),
inference(forward_demodulation,[],[f397,f326]) ).
fof(f438,plain,
! [X2,X0,X1] : ld(X1,X2) = mult(ld(mult(X0,X1),X0),X2),
inference(superposition,[],[f26,f35]) ).
fof(f446,plain,
! [X0,X1] : i(X0) = rd(ld(X0,X1),X1),
inference(superposition,[],[f4,f26]) ).
fof(f474,plain,
! [X0,X1] : i(mult(X1,X0)) = rd(i(X0),X1),
inference(superposition,[],[f446,f35]) ).
fof(f502,plain,
! [X0,X1] : mult(ld(X0,X1),mult(X0,ld(X0,X1))) = mult(ld(X0,mult(X1,X0)),ld(X0,X1)),
inference(superposition,[],[f274,f214]) ).
fof(f509,plain,
! [X0,X1] : mult(ld(X0,X1),mult(X0,ld(X0,X1))) = ld(X0,mult(mult(X1,rd(X1,X0)),X0)),
inference(forward_demodulation,[],[f502,f61]) ).
fof(f518,plain,
! [X0,X1] : mult(ld(X0,X1),X1) = ld(X0,mult(mult(X1,rd(X1,X0)),X0)),
inference(forward_demodulation,[],[f509,f1]) ).
fof(f574,plain,
! [X2,X0,X1] : mult(X0,ld(X1,mult(X2,X1))) = ld(X1,mult(mult(rd(mult(X1,X0),X1),X2),X1)),
inference(superposition,[],[f57,f2]) ).
fof(f584,plain,
! [X2,X0,X1] : ld(X1,mult(mult(rd(X2,X1),rd(X0,X1)),X1)) = mult(ld(X1,X2),ld(X1,X0)),
inference(superposition,[],[f57,f3]) ).
fof(f585,plain,
! [X0,X1] : ld(X0,mult(mult(rd(X1,X0),unit),X0)) = mult(ld(X0,X1),ld(X0,X0)),
inference(superposition,[],[f57,f6]) ).
fof(f607,plain,
! [X0,X1] : ld(X0,mult(mult(rd(X1,X0),unit),X0)) = mult(ld(X0,X1),rd(X0,X0)),
inference(forward_demodulation,[],[f585,f326]) ).
fof(f616,plain,
! [X0,X1] : ld(X0,mult(rd(X1,X0),X0)) = mult(ld(X0,X1),rd(X0,X0)),
inference(forward_demodulation,[],[f607,f5]) ).
fof(f622,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(X0,X1),rd(X0,X0)),
inference(forward_demodulation,[],[f616,f3]) ).
fof(f635,plain,
! [X0,X1] : mult(X0,rd(X1,X1)) = X0,
inference(superposition,[],[f622,f2]) ).
fof(f825,definition,
( spl6_8
<=> sF5 = mult(a,mult(sF3,a)) ),
introduced(definition,[new_symbols(definition,[spl6_8])],[avatar_definition]) ).
fof(f827,plain,
( sF5 = mult(a,mult(sF3,a))
| ~ spl6_8 ),
inference(avatar_component_clause,[],[f825]) ).
fof(f828,plain,
( spl6_8
| ~ spl6_1
| ~ spl6_5 ),
inference(avatar_split_clause,[],[f299,f101,f75,f825]) ).
fof(f946,plain,
! [X2,X0,X1] : rd(X2,X1) = mult(X2,ld(mult(X0,X1),X0)),
inference(superposition,[],[f33,f35]) ).
fof(f959,plain,
! [X0,X1] : mult(X0,mult(i(X1),X0)) = mult(rd(X0,X1),X0),
inference(superposition,[],[f274,f33]) ).
fof(f966,plain,
! [X0] : i(X0) = rd(unit,X0),
inference(superposition,[],[f6,f33]) ).
fof(f967,plain,
! [X0,X1] : ld(X0,i(X1)) = rd(i(X0),X1),
inference(superposition,[],[f26,f33]) ).
fof(f968,plain,
! [X0,X1] : ld(X0,i(X1)) = i(mult(X1,X0)),
inference(forward_demodulation,[],[f967,f474]) ).
fof(f975,plain,
! [X0,X1] : mult(X0,ld(X1,X0)) = mult(rd(X0,X1),X0),
inference(forward_demodulation,[],[f959,f26]) ).
fof(f1076,plain,
! [X0,X1] : mult(X0,X1) = mult(X1,ld(ld(X0,X1),X1)),
inference(superposition,[],[f975,f38]) ).
fof(f1081,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = mult(mult(X0,X1),ld(X1,mult(X0,X1))),
inference(superposition,[],[f975,f4]) ).
fof(f1141,plain,
! [X0,X1] : mult(i(X0),X1) = mult(X1,ld(mult(X0,X1),X1)),
inference(superposition,[],[f1076,f28]) ).
fof(f1172,plain,
! [X0,X1] : ld(X0,X1) = mult(X1,ld(mult(X0,X1),X1)),
inference(forward_demodulation,[],[f1141,f26]) ).
fof(f1210,plain,
! [X0,X1] : ld(mult(X0,X1),X0) = mult(X0,ld(mult(X0,mult(X1,X0)),X0)),
inference(superposition,[],[f1172,f274]) ).
fof(f1251,plain,
! [X0,X1] : ld(mult(X0,X1),X0) = rd(X0,mult(X1,X0)),
inference(forward_demodulation,[],[f1210,f946]) ).
fof(f1264,plain,
! [X2,X0,X1] : rd(X0,mult(X1,X0)) = ld(mult(X2,X1),X2),
inference(backward_demodulation,[],[f395,f1251]) ).
fof(f1266,plain,
! [X2,X0,X1] : ld(X1,X2) = mult(rd(X0,mult(X1,X0)),X2),
inference(backward_demodulation,[],[f438,f1251]) ).
fof(f1270,plain,
! [X2,X0,X1] : rd(X2,X1) = mult(X2,rd(X0,mult(X1,X0))),
inference(backward_demodulation,[],[f946,f1251]) ).
fof(f1274,plain,
! [X2,X0,X1] : rd(X0,mult(X1,X0)) = rd(X2,mult(X1,X2)),
inference(forward_demodulation,[],[f1264,f1251]) ).
fof(f1347,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,[],[f1274,f57]) ).
fof(f1350,plain,
! [X2,X0,X1] : rd(X2,X0) = rd(X1,mult(rd(X0,X2),X1)),
inference(superposition,[],[f1274,f3]) ).
fof(f1378,plain,
! [X2,X0,X1] : rd(mult(mult(X1,X2),X2),mult(X1,X2)) = mult(mult(X1,X2),rd(X0,mult(X1,X0))),
inference(superposition,[],[f239,f1274]) ).
fof(f1383,plain,
! [X2,X1] : rd(mult(X1,X2),X1) = rd(mult(mult(X1,X2),X2),mult(X1,X2)),
inference(forward_demodulation,[],[f1378,f1270]) ).
fof(f1429,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,[],[f1270,f57]) ).
fof(f1432,plain,
! [X2,X0,X1] : mult(X1,rd(X2,X0)) = rd(X1,rd(X0,X2)),
inference(superposition,[],[f1270,f3]) ).
fof(f1684,plain,
! [X2,X3,X0,X1] : mult(X3,rd(rd(X2,X1),X0)) = rd(X3,mult(X0,rd(X1,X2))),
inference(superposition,[],[f1432,f1432]) ).
fof(f1701,plain,
! [X0,X1] : i(unit) = mult(rd(X0,X1),rd(X1,X0)),
inference(superposition,[],[f413,f1432]) ).
fof(f1930,plain,
! [X1] : i(unit) = rd(X1,mult(i(unit),X1)),
inference(superposition,[],[f1350,f413]) ).
fof(f1965,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = mult(X2,ld(mult(rd(X1,X0),X2),X2)),
inference(superposition,[],[f975,f1350]) ).
fof(f1972,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = ld(rd(X1,X0),X2),
inference(forward_demodulation,[],[f1965,f1172]) ).
fof(f1993,plain,
! [X1] : i(unit) = rd(X1,ld(unit,X1)),
inference(forward_demodulation,[],[f1930,f26]) ).
fof(f2006,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,[],[f50,f1972]) ).
fof(f2019,plain,
unit = i(unit),
inference(forward_demodulation,[],[f1993,f38]) ).
fof(f2032,plain,
! [X0,X1] : unit = mult(rd(X0,X1),rd(X1,X0)),
inference(backward_demodulation,[],[f1701,f2019]) ).
fof(f2273,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,[],[f1266,f57]) ).
fof(f2459,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,[],[f123,f5]) ).
fof(f2595,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,[],[f2459,f1251]) ).
fof(f2625,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,[],[f2595,f1266]) ).
fof(f2650,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,[],[f2625,f401]) ).
fof(f2664,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,[],[f2650,f26]) ).
fof(f2673,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,[],[f2664,f1]) ).
fof(f2712,plain,
! [X2,X0,X1] : ld(X1,mult(mult(X2,rd(mult(X1,X0),X1)),X1)) = mult(ld(X1,mult(X2,X1)),X0),
inference(superposition,[],[f61,f2]) ).
fof(f3175,plain,
! [X2,X0,X1] : ld(mult(X1,X2),mult(X1,ld(X2,X0))) = ld(X2,ld(mult(X1,X2),mult(X1,X0))),
inference(superposition,[],[f2673,f1]) ).
fof(f3213,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,f2673]) ).
fof(f3394,plain,
! [X0,X1] : ld(X1,ld(mult(X1,X1),mult(X1,X0))) = ld(mult(X1,X1),X0),
inference(superposition,[],[f3175,f1]) ).
fof(f3500,plain,
! [X0,X1] : ld(mult(X1,X1),ld(X1,X0)) = ld(X1,ld(mult(X1,X1),X0)),
inference(superposition,[],[f3394,f1]) ).
fof(f3531,plain,
! [X0,X1] : ld(mult(X0,X0),mult(X0,X1)) = mult(X0,ld(mult(X0,X0),X1)),
inference(superposition,[],[f1,f3394]) ).
fof(f3655,plain,
! [X0,X1] : ld(i(X0),ld(mult(i(X0),i(X0)),X1)) = ld(mult(i(X0),i(X0)),mult(X0,X1)),
inference(superposition,[],[f3500,f28]) ).
fof(f3670,plain,
! [X0,X1] : ld(i(X0),ld(ld(X0,i(X0)),X1)) = ld(ld(X0,i(X0)),mult(X0,X1)),
inference(forward_demodulation,[],[f3655,f26]) ).
fof(f3684,plain,
! [X0,X1] : ld(i(X0),ld(i(mult(X0,X0)),X1)) = ld(i(mult(X0,X0)),mult(X0,X1)),
inference(forward_demodulation,[],[f3670,f968]) ).
fof(f3693,plain,
! [X0,X1] : ld(i(X0),ld(i(mult(X0,X0)),X1)) = mult(mult(X0,X0),mult(X0,X1)),
inference(forward_demodulation,[],[f3684,f28]) ).
fof(f3700,plain,
! [X0,X1] : mult(X0,ld(i(mult(X0,X0)),X1)) = mult(mult(X0,X0),mult(X0,X1)),
inference(forward_demodulation,[],[f3693,f28]) ).
fof(f3706,plain,
! [X0,X1] : mult(mult(X0,X0),mult(X0,X1)) = mult(X0,mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f3700,f28]) ).
fof(f3735,plain,
! [X0,X1] : mult(mult(X0,X0),rd(X0,X1)) = mult(X0,mult(mult(X0,X0),i(X1))),
inference(superposition,[],[f3706,f33]) ).
fof(f3763,plain,
! [X0,X1] : mult(X0,X1) = ld(mult(X0,X0),mult(X0,mult(mult(X0,X0),X1))),
inference(superposition,[],[f2,f3706]) ).
fof(f3800,plain,
! [X0,X1] : mult(mult(X0,X0),rd(X0,X1)) = mult(X0,rd(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f3735,f33]) ).
fof(f3916,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,f3531]) ).
fof(f3917,plain,
! [X0,X1] : ld(ld(X0,i(X0)),mult(i(X0),X1)) = ld(X0,ld(ld(X0,i(X0)),X1)),
inference(forward_demodulation,[],[f3916,f26]) ).
fof(f3956,plain,
! [X0,X1] : ld(i(mult(X0,X0)),mult(i(X0),X1)) = ld(X0,ld(i(mult(X0,X0)),X1)),
inference(forward_demodulation,[],[f3917,f968]) ).
fof(f3975,plain,
! [X0,X1] : ld(i(mult(X0,X0)),mult(i(X0),X1)) = ld(X0,mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f3956,f28]) ).
fof(f3988,plain,
! [X0,X1] : mult(mult(X0,X0),mult(i(X0),X1)) = ld(X0,mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f3975,f28]) ).
fof(f3996,plain,
! [X0,X1] : mult(mult(X0,X0),ld(X0,X1)) = ld(X0,mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f3988,f26]) ).
fof(f4040,plain,
! [X0,X1] : mult(X0,X0) = rd(ld(X0,mult(mult(X0,X0),X1)),ld(X0,X1)),
inference(superposition,[],[f4,f3996]) ).
fof(f4159,plain,
! [X0,X1] : rd(mult(X0,X0),X1) = mult(X0,rd(mult(X0,X0),mult(X1,X0))),
inference(superposition,[],[f1270,f3800]) ).
fof(f4700,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,[],[f446,f64]) ).
fof(f4713,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,[],[f4700,f396]) ).
fof(f4795,plain,
! [X3,X0,X1] : ld(ld(X0,X1),X3) = mult(ld(mult(rd(X1,X0),X0),X0),X3),
inference(backward_demodulation,[],[f2273,f4713]) ).
fof(f4796,plain,
! [X3,X0,X1] : rd(X3,ld(X0,X1)) = mult(X3,ld(mult(rd(X1,X0),X0),X0)),
inference(backward_demodulation,[],[f1429,f4713]) ).
fof(f4797,plain,
! [X3,X0,X1] : rd(X3,mult(ld(X0,X1),X3)) = ld(mult(rd(X1,X0),X0),X0),
inference(backward_demodulation,[],[f1347,f4713]) ).
fof(f4844,plain,
! [X3,X0,X1] : ld(X1,X0) = rd(X3,mult(ld(X0,X1),X3)),
inference(forward_demodulation,[],[f4797,f3]) ).
fof(f4845,plain,
! [X3,X0,X1] : rd(X3,ld(X0,X1)) = mult(X3,ld(X1,X0)),
inference(forward_demodulation,[],[f4796,f3]) ).
fof(f4846,plain,
! [X3,X0,X1] : mult(ld(X1,X0),X3) = ld(ld(X0,X1),X3),
inference(forward_demodulation,[],[f4795,f3]) ).
fof(f4944,plain,
! [X0,X1] : mult(X0,X0) = mult(ld(X0,mult(mult(X0,X0),X1)),ld(X1,X0)),
inference(backward_demodulation,[],[f4040,f4845]) ).
fof(f5658,plain,
! [X2,X3,X0,X1] : mult(X3,rd(ld(X2,X1),X0)) = rd(X3,mult(X0,ld(X1,X2))),
inference(superposition,[],[f1432,f4845]) ).
fof(f5813,plain,
! [X2,X3,X0,X1] : mult(X3,ld(X2,ld(X1,X0))) = rd(X3,mult(ld(X0,X1),X2)),
inference(superposition,[],[f4845,f4846]) ).
fof(f5983,plain,
! [X2,X0,X1] : ld(ld(X0,X1),mult(X0,X0)) = rd(X2,mult(ld(X0,ld(mult(X0,X0),X1)),X2)),
inference(superposition,[],[f4844,f3500]) ).
fof(f6042,plain,
! [X0,X1] : ld(ld(mult(X0,X0),X1),X0) = ld(ld(X0,X1),mult(X0,X0)),
inference(forward_demodulation,[],[f5983,f4844]) ).
fof(f6060,plain,
! [X0,X1] : ld(ld(mult(X0,X0),X1),X0) = mult(ld(X1,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f6042,f4846]) ).
fof(f6076,plain,
! [X0,X1] : mult(ld(X1,mult(X0,X0)),X0) = mult(ld(X1,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f6060,f4846]) ).
fof(f6331,plain,
! [X2,X0,X1] : ld(X0,mult(X1,mult(ld(X1,X0),X2))) = mult(ld(X1,X0),ld(X0,mult(X1,X2))),
inference(superposition,[],[f3213,f1]) ).
fof(f6365,plain,
! [X2,X0,X1] : mult(X2,ld(mult(X1,X2),X0)) = ld(mult(X1,X2),mult(X1,mult(X2,ld(X1,X0)))),
inference(superposition,[],[f3213,f1]) ).
fof(f6391,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,[],[f3213,f26]) ).
fof(f6476,plain,
! [X2,X0,X1] : ld(mult(i(X0),X2),mult(i(X0),mult(X2,X1))) = rd(X2,mult(ld(X1,X0),mult(i(X0),X2))),
inference(forward_demodulation,[],[f6391,f5813]) ).
fof(f6541,plain,
! [X2,X0,X1] : ld(ld(X0,X2),mult(i(X0),mult(X2,X1))) = rd(X2,mult(ld(X1,X0),ld(X0,X2))),
inference(forward_demodulation,[],[f6476,f26]) ).
fof(f6586,plain,
! [X2,X0,X1] : rd(X2,mult(ld(X1,X0),ld(X0,X2))) = mult(ld(X2,X0),mult(i(X0),mult(X2,X1))),
inference(forward_demodulation,[],[f6541,f4846]) ).
fof(f6643,plain,
! [X2,X0,X1] : rd(X2,mult(ld(X1,X0),ld(X0,X2))) = mult(ld(X2,X0),ld(X0,mult(X2,X1))),
inference(forward_demodulation,[],[f6586,f26]) ).
fof(f6679,plain,
! [X2,X0,X1] : rd(X2,mult(ld(X1,X0),ld(X0,X2))) = ld(X0,mult(X2,mult(ld(X2,X0),X1))),
inference(forward_demodulation,[],[f6643,f6331]) ).
fof(f6883,plain,
! [X2,X0,X1] : ld(X0,mult(mult(mult(X0,X1),X2),X0)) = mult(mult(X1,X0),ld(X0,mult(X2,X0))),
inference(superposition,[],[f574,f252]) ).
fof(f6971,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = ld(X1,mult(mult(mult(X1,X0),X0),X1)),
inference(backward_demodulation,[],[f1081,f6883]) ).
fof(f7252,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,[],[f40,f3]) ).
fof(f7937,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,[],[f44,f3]) ).
fof(f7944,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,[],[f44,f6]) ).
fof(f8105,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,[],[f7944,f1270]) ).
fof(f8112,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,[],[f7937,f1684]) ).
fof(f8214,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,[],[f8105,f966]) ).
fof(f8291,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,[],[f8214,f33]) ).
fof(f8342,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,[],[f8291,f3]) ).
fof(f8436,plain,
! [X0,X1] : rd(mult(X0,X0),mult(X1,X0)) = rd(rd(mult(X0,mult(X1,X0)),mult(X1,X0)),X1),
inference(superposition,[],[f8342,f274]) ).
fof(f8441,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,[],[f8342,f1]) ).
fof(f8490,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,f8342]) ).
fof(f8549,plain,
! [X0,X1] : rd(X0,X1) = rd(mult(X0,X0),mult(X1,X0)),
inference(forward_demodulation,[],[f8436,f4]) ).
fof(f8622,plain,
! [X0,X1] : mult(X0,rd(X0,X1)) = rd(mult(X0,X0),X1),
inference(backward_demodulation,[],[f4159,f8549]) ).
fof(f8668,plain,
! [X0,X1] : mult(ld(X0,X1),X1) = ld(X0,mult(rd(mult(X1,X1),X0),X0)),
inference(backward_demodulation,[],[f518,f8622]) ).
fof(f8711,plain,
! [X0,X1] : mult(ld(X0,X1),X1) = ld(X0,mult(X1,X1)),
inference(forward_demodulation,[],[f8668,f3]) ).
fof(f8792,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = ld(i(X0),mult(X1,X1)),
inference(superposition,[],[f8711,f28]) ).
fof(f8798,plain,
! [X0,X1] : ld(X1,X0) = rd(X1,ld(X0,mult(X1,X1))),
inference(superposition,[],[f4844,f8711]) ).
fof(f8883,plain,
! [X0,X1] : ld(X1,X0) = mult(X1,ld(mult(X1,X1),X0)),
inference(forward_demodulation,[],[f8798,f4845]) ).
fof(f8888,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = mult(X0,mult(X1,X1)),
inference(forward_demodulation,[],[f8792,f28]) ).
fof(f8927,plain,
! [X0,X1] : ld(X1,X0) = ld(mult(X1,X1),mult(X1,X0)),
inference(forward_demodulation,[],[f8883,f3531]) ).
fof(f8932,plain,
! [X2,X1] : rd(mult(X1,X2),X1) = rd(mult(X1,mult(X2,X2)),mult(X1,X2)),
inference(backward_demodulation,[],[f1383,f8888]) ).
fof(f8939,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = ld(X1,mult(mult(X1,mult(X0,X0)),X1)),
inference(backward_demodulation,[],[f6971,f8888]) ).
fof(f9014,plain,
! [X0,X1] : mult(X0,X1) = ld(X0,mult(mult(X0,X0),X1)),
inference(backward_demodulation,[],[f3763,f8927]) ).
fof(f9025,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = ld(X1,mult(X1,mult(mult(X0,X0),X1))),
inference(forward_demodulation,[],[f8939,f274]) ).
fof(f9055,plain,
! [X0,X1] : mult(X0,X0) = mult(mult(X0,X1),ld(X1,X0)),
inference(backward_demodulation,[],[f4944,f9014]) ).
fof(f9092,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = mult(mult(X0,X0),X1),
inference(forward_demodulation,[],[f9025,f2]) ).
fof(f9718,plain,
! [X2,X0,X1] : ld(X1,mult(mult(mult(X0,X0),rd(X2,X1)),X1)) = mult(ld(X1,mult(X0,mult(X0,X1))),ld(X1,X2)),
inference(superposition,[],[f61,f9092]) ).
fof(f9792,plain,
! [X2,X0,X1] : mult(ld(X1,mult(X0,mult(X0,X1))),ld(X1,X2)) = ld(X1,mult(mult(X0,mult(X0,rd(X2,X1))),X1)),
inference(forward_demodulation,[],[f9718,f9092]) ).
fof(f11737,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,[],[f40,f9055]) ).
fof(f11803,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,[],[f11737,f1]) ).
fof(f11862,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,[],[f11803,f4]) ).
fof(f11900,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,[],[f11862,f3]) ).
fof(f14686,plain,
! [X2,X0,X1] : mult(mult(X0,X1),ld(X1,X2)) = rd(mult(mult(mult(X0,X2),X1),ld(X1,X2)),X2),
inference(superposition,[],[f11900,f4]) ).
fof(f16967,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,f2712]) ).
fof(f19617,plain,
! [X2,X0,X1] : rd(mult(mult(rd(X0,X1),X2),X1),mult(X2,X1)) = mult(rd(X0,mult(X2,X1)),X2),
inference(superposition,[],[f8490,f3]) ).
fof(f22142,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,f584]) ).
fof(f22191,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,[],[f7252,f22142]) ).
fof(f22673,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,f19617]) ).
fof(f31436,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,[],[f14686,f1251]) ).
fof(f31447,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,[],[f31436,f1270]) ).
fof(f31543,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,[],[f31447,f1270]) ).
fof(f35764,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,[],[f16967,f8888]) ).
fof(f35861,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,[],[f19617,f16967]) ).
fof(f35970,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,[],[f35861,f3]) ).
fof(f36047,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,[],[f35764,f8932]) ).
fof(f36093,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,[],[f35970,f3]) ).
fof(f55207,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,[],[f16967,f22191]) ).
fof(f55475,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,[],[f55207,f3]) ).
fof(f55864,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,[],[f55475,f36047]) ).
fof(f56185,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,[],[f55864,f36093]) ).
fof(f56438,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,[],[f56185,f3]) ).
fof(f56603,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,[],[f56438,f2]) ).
fof(f56896,plain,
! [X0,X1] : mult(X0,mult(ld(X0,mult(X1,X1)),X1)) = mult(mult(X0,ld(X0,mult(X1,X1))),X1),
inference(superposition,[],[f56603,f8711]) ).
fof(f57050,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,[],[f33,f56603]) ).
fof(f57051,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,[],[f57050,f33]) ).
fof(f57114,plain,
! [X0,X1] : mult(mult(X1,X1),X1) = mult(X0,mult(ld(X0,mult(X1,X1)),X1)),
inference(forward_demodulation,[],[f56896,f1]) ).
fof(f57139,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,[],[f57051,f5658]) ).
fof(f57184,plain,
! [X0,X1] : mult(mult(X1,X1),X1) = mult(X0,mult(ld(X0,X1),mult(X1,X1))),
inference(forward_demodulation,[],[f57114,f6076]) ).
fof(f57198,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,[],[f57139,f33]) ).
fof(f57237,plain,
! [X0,X1] : mult(X1,mult(X1,X1)) = mult(X0,mult(ld(X0,X1),mult(X1,X1))),
inference(forward_demodulation,[],[f57184,f274]) ).
fof(f57246,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,[],[f57198,f5658]) ).
fof(f57282,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,[],[f57246,f33]) ).
fof(f57304,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,[],[f57282,f1972]) ).
fof(f57319,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,[],[f8441,f57304]) ).
fof(f57324,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,[],[f57319,f1266]) ).
fof(f57416,plain,
! [X2,X0,X1] : ld(mult(X1,ld(X1,X0)),mult(X1,mult(ld(X1,X0),mult(mult(X0,X0),ld(ld(X1,X0),X2))))) = mult(ld(mult(X1,ld(X1,X0)),mult(X0,mult(X0,X0))),ld(mult(X1,ld(X1,X0)),mult(X1,X2))),
inference(superposition,[],[f145,f57237]) ).
fof(f57704,plain,
! [X2,X0,X1] : ld(X0,mult(X1,mult(ld(X1,X0),mult(mult(X0,X0),ld(ld(X1,X0),X2))))) = mult(ld(X0,mult(X0,mult(X0,X0))),ld(X0,mult(X1,X2))),
inference(forward_demodulation,[],[f57416,f1]) ).
fof(f57891,plain,
! [X2,X0,X1] : ld(X0,mult(X1,mult(ld(X1,X0),mult(mult(X0,X0),ld(ld(X1,X0),X2))))) = ld(X0,mult(mult(X0,mult(X0,rd(mult(X1,X2),X0))),X0)),
inference(forward_demodulation,[],[f57704,f9792]) ).
fof(f58017,plain,
! [X2,X0,X1] : ld(X0,mult(X1,mult(ld(X1,X0),mult(mult(X0,X0),ld(ld(X1,X0),X2))))) = ld(X0,mult(X0,mult(mult(X0,rd(mult(X1,X2),X0)),X0))),
inference(forward_demodulation,[],[f57891,f274]) ).
fof(f58100,plain,
! [X2,X0,X1] : ld(X0,mult(X1,mult(ld(X1,X0),mult(mult(X0,X0),ld(ld(X1,X0),X2))))) = mult(mult(X0,rd(mult(X1,X2),X0)),X0),
inference(forward_demodulation,[],[f58017,f2]) ).
fof(f58164,plain,
! [X2,X0,X1] : ld(X0,mult(X1,mult(ld(X1,X0),mult(mult(X0,X0),ld(ld(X1,X0),X2))))) = mult(X0,mult(rd(mult(X1,X2),X0),X0)),
inference(forward_demodulation,[],[f58100,f274]) ).
fof(f58217,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = ld(X0,mult(X1,mult(ld(X1,X0),mult(mult(X0,X0),ld(ld(X1,X0),X2))))),
inference(forward_demodulation,[],[f58164,f3]) ).
fof(f58259,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = ld(X0,mult(X1,mult(ld(X1,X0),mult(X0,mult(X0,ld(ld(X1,X0),X2)))))),
inference(forward_demodulation,[],[f58217,f9092]) ).
fof(f58291,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = ld(X0,mult(X1,mult(ld(X1,X0),mult(X0,mult(X0,mult(ld(X0,X1),X2)))))),
inference(forward_demodulation,[],[f58259,f4846]) ).
fof(f74827,plain,
! [X2,X0,X1] : mult(ld(X0,X1),ld(mult(X0,ld(X0,X1)),mult(X2,X0))) = ld(mult(X0,ld(X0,X1)),mult(X0,ld(X0,mult(mult(rd(X1,X0),X2),X0)))),
inference(superposition,[],[f6365,f57]) ).
fof(f74879,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,[],[f6365,f26]) ).
fof(f75000,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,[],[f74879,f28]) ).
fof(f75041,plain,
! [X2,X0,X1] : mult(ld(X0,X1),ld(mult(X0,ld(X0,X1)),mult(X2,X0))) = ld(mult(X0,ld(X0,X1)),mult(mult(rd(X1,X0),X2),X0)),
inference(forward_demodulation,[],[f74827,f1]) ).
fof(f75167,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,[],[f75000,f26]) ).
fof(f75198,plain,
! [X2,X0,X1] : mult(ld(X0,X1),ld(X1,mult(X2,X0))) = ld(X1,mult(mult(rd(X1,X0),X2),X0)),
inference(forward_demodulation,[],[f75041,f1]) ).
fof(f75287,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,[],[f75167,f4846]) ).
fof(f75386,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,[],[f75287,f6331]) ).
fof(f75438,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,[],[f75386,f4846]) ).
fof(f75466,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = mult(X1,mult(ld(X1,X0),mult(X0,mult(ld(X0,X1),X2)))),
inference(backward_demodulation,[],[f58291,f75438]) ).
fof(f77114,plain,
! [X2,X0,X1] : mult(X1,mult(X0,ld(X0,mult(X2,X1)))) = mult(X0,mult(ld(X0,X1),mult(X1,ld(X0,mult(mult(rd(X0,X1),X2),X1))))),
inference(superposition,[],[f75466,f75198]) ).
fof(f77438,plain,
! [X2,X0,X1] : mult(X1,mult(X2,X1)) = mult(X0,mult(ld(X0,X1),mult(X1,ld(X0,mult(mult(rd(X0,X1),X2),X1))))),
inference(forward_demodulation,[],[f77114,f1]) ).
fof(f93888,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,[],[f2006,f2032]) ).
fof(f94451,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,[],[f93888,f6]) ).
fof(f94821,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,[],[f94451,f635]) ).
fof(f95080,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,[],[f8112,f94821]) ).
fof(f96635,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,[],[f95080,f3]) ).
fof(f96744,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,[],[f96635,f9092]) ).
fof(f96927,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,[],[f96744,f4]) ).
fof(f97913,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,[],[f96927,f4]) ).
fof(f98659,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,[],[f97913,f3]) ).
fof(f99074,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,[],[f98659,f22673]) ).
fof(f99640,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,[],[f99074,f57324]) ).
fof(f99682,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,[],[f99074,f446]) ).
fof(f100025,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,[],[f99682,f33]) ).
fof(f100060,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,[],[f99640,f1270]) ).
fof(f100293,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,[],[f100025,f4845]) ).
fof(f100319,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,[],[f100060,f4]) ).
fof(f100477,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,[],[f100293,f1]) ).
fof(f100496,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,[],[f100319,f1]) ).
fof(f100632,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,[],[f100496,f100477]) ).
fof(f102484,plain,
! [X2,X0,X1] : rd(X2,mult(ld(X0,X1),ld(X1,X2))) = rd(mult(X1,ld(ld(X0,X1),X2)),X2),
inference(superposition,[],[f100632,f1172]) ).
fof(f102844,plain,
! [X2,X0,X1] : rd(X2,mult(ld(X0,X1),ld(X1,X2))) = rd(mult(X1,mult(ld(X1,X0),X2)),X2),
inference(forward_demodulation,[],[f102484,f4846]) ).
fof(f103269,plain,
! [X2,X0,X1] : ld(X1,mult(X2,mult(ld(X2,X1),X0))) = rd(mult(X1,mult(ld(X1,X0),X2)),X2),
inference(forward_demodulation,[],[f102844,f6679]) ).
fof(f103510,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),X2)) = rd(mult(X0,mult(ld(X0,mult(X0,X2)),X1)),X1),
inference(backward_demodulation,[],[f75438,f103269]) ).
fof(f103684,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),X2)) = rd(mult(X0,mult(X2,X1)),X1),
inference(forward_demodulation,[],[f103510,f2]) ).
fof(f104552,plain,
! [X2,X0,X1] : mult(X1,mult(X2,X1)) = rd(mult(X1,mult(mult(X1,ld(X0,mult(mult(rd(X0,X1),X2),X1))),X0)),X0),
inference(backward_demodulation,[],[f77438,f103684]) ).
fof(f107713,plain,
! [X2,X0,X1] : mult(X1,ld(X0,mult(mult(rd(X0,X1),X2),X1))) = rd(mult(X0,mult(ld(X0,mult(X2,X1)),X1)),X1),
inference(superposition,[],[f103684,f75198]) ).
fof(f108055,plain,
! [X2,X0,X1] : mult(X1,ld(X0,mult(mult(rd(X0,X1),X2),X1))) = rd(rd(mult(mult(X2,X1),mult(X1,X0)),X0),X1),
inference(forward_demodulation,[],[f107713,f103684]) ).
fof(f108279,plain,
! [X2,X0,X1] : mult(X1,ld(X0,mult(mult(rd(X0,X1),X2),X1))) = rd(mult(X2,mult(X1,X0)),X0),
inference(forward_demodulation,[],[f108055,f31543]) ).
fof(f108727,plain,
! [X2,X0,X1] : mult(X1,mult(X2,X1)) = rd(mult(X1,mult(rd(mult(X2,mult(X1,X0)),X0),X0)),X0),
inference(backward_demodulation,[],[f104552,f108279]) ).
fof(f109586,plain,
! [X2,X0,X1] : mult(X1,mult(X2,X1)) = rd(mult(X1,mult(X2,mult(X1,X0))),X0),
inference(forward_demodulation,[],[f108727,f3]) ).
fof(f126704,plain,
! [X2,X0,X1] : mult(X1,mult(X2,X1)) = rd(mult(X1,mult(X2,X0)),ld(X1,X0)),
inference(superposition,[],[f109586,f1]) ).
fof(f127360,plain,
! [X2,X0,X1] : mult(X1,mult(X2,X1)) = mult(mult(X1,mult(X2,X0)),ld(X0,X1)),
inference(forward_demodulation,[],[f126704,f4845]) ).
fof(f128068,plain,
! [X2,X0,X1] : mult(X1,mult(rd(X0,X2),X1)) = mult(mult(X1,X0),ld(X2,X1)),
inference(superposition,[],[f127360,f3]) ).
fof(f129429,plain,
! [X2,X0,X1] : mult(mult(X1,X2),mult(X0,X1)) = mult(X1,mult(rd(X2,i(X0)),X1)),
inference(superposition,[],[f128068,f28]) ).
fof(f129612,plain,
! [X2,X0,X1] : mult(X1,mult(mult(X2,X0),X1)) = mult(mult(X1,X2),mult(X0,X1)),
inference(forward_demodulation,[],[f129429,f36]) ).
fof(f131832,plain,
( ! [X0] : mult(sF0,mult(X0,a)) = mult(a,mult(mult(b,X0),a))
| ~ spl6_4 ),
inference(superposition,[],[f129612,f96]) ).
fof(f160598,plain,
( mult(a,mult(sF3,a)) = mult(sF0,mult(c,a))
| ~ spl6_4
| ~ spl6_6 ),
inference(superposition,[],[f131832,f110]) ).
fof(f160756,plain,
( mult(sF0,sF1) = mult(a,mult(sF3,a))
| ~ spl6_4
| ~ spl6_6
| ~ spl6_7 ),
inference(forward_demodulation,[],[f160598,f117]) ).
fof(f160782,plain,
( mult(sF0,sF1) = sF5
| ~ spl6_4
| ~ spl6_6
| ~ spl6_7
| ~ spl6_8 ),
inference(forward_demodulation,[],[f160756,f827]) ).
fof(f160794,plain,
( sF2 = sF5
| ~ spl6_2
| ~ spl6_4
| ~ spl6_6
| ~ spl6_7
| ~ spl6_8 ),
inference(forward_demodulation,[],[f160782,f82]) ).
fof(f160801,plain,
( $false
| ~ spl6_2
| spl6_3
| ~ spl6_4
| ~ spl6_6
| ~ spl6_7
| ~ spl6_8 ),
inference(forward_subsumption_resolution,[],[f160794,f91]) ).
fof(f160802,plain,
( ~ spl6_2
| spl6_3
| ~ spl6_4
| ~ spl6_6
| ~ spl6_7
| ~ spl6_8 ),
inference(avatar_contradiction_clause,[],[f160801]) ).
cnf(s1,plain,
spl6_1,
inference(sat_conversion,[],[f78]) ).
cnf(s2,plain,
spl6_2,
inference(sat_conversion,[],[f83]) ).
cnf(s3,plain,
~ spl6_3,
inference(sat_conversion,[],[f92]) ).
cnf(s4,plain,
spl6_4,
inference(sat_conversion,[],[f97]) ).
cnf(s5,plain,
spl6_5,
inference(sat_conversion,[],[f104]) ).
cnf(s6,plain,
spl6_6,
inference(sat_conversion,[],[f111]) ).
cnf(s7,plain,
spl6_7,
inference(sat_conversion,[],[f118]) ).
cnf(s8,plain,
( ~ spl6_1
| ~ spl6_5
| spl6_8 ),
inference(sat_conversion,[],[f828]) ).
cnf(s49,plain,
( ~ spl6_2
| spl6_3
| ~ spl6_4
| ~ spl6_6
| ~ spl6_7
| ~ spl6_8 ),
inference(sat_conversion,[],[f160802]) ).
cnf(s77,plain,
~ spl6_8,
inference(rat,[],[s49,s3,s7,s6,s4,s2]) ).
cnf(s80,plain,
~ spl6_1,
inference(rat,[],[s8,s5,s77]) ).
cnf(s81,plain,
$false,
inference(rat,[],[s1,s80]) ).
fof(f160804,plain,
$false,
inference(avatar_sat_refutation,[],[s81]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP666-4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.41 % Computer : n017.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 27 10:29:04 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.47 Running first-order theorem proving
% 0.14/0.47 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 121.72/17.93 % (2346157)Detected a unit-equality problem, will run specialized UEQ schedule.
% 121.72/17.93 % (2346166)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2992896830:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_3000 on theBenchmark for (3000ds/181Mi)
% 121.72/17.93 % (2346168)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1019357389:i=1187:sd=4:av=off:ss=axioms:sgt=32_3000 on theBenchmark for (3000ds/1187Mi)
% 121.72/17.93 % (2346164)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=590966960:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_3000 on theBenchmark for (3000ds/130716Mi)
% 121.72/17.93 % (2346162)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=2614743328:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_3000 on theBenchmark for (3000ds/138329Mi)
% 121.72/17.93 % (2346165)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=893640815:i=136:bd=preordered:ins=2:av=off_3000 on theBenchmark for (3000ds/136Mi)
% 121.72/17.93 % (2346163)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=3209580349:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_3000 on theBenchmark for (3000ds/130792Mi)
% 121.72/17.93 % (2346167)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2241014931:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_3000 on theBenchmark for (3000ds/257Mi)
% 121.72/17.93 % (2346166)Instruction limit reached!
% 121.72/17.93 % (2346166)------------------------------
% 121.72/17.93 % (2346166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.72/17.93 % (2346166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.72/17.93 % (2346166)CaDiCaL version: 2.1.3
% 121.72/17.93 % (2346166)Termination reason: Instruction limit
% 121.72/17.93 % (2346166)Termination phase: Saturation
% 121.72/17.93 % (2346166)Time elapsed: 0.090 s
% 121.72/17.93 % (2346166)Peak memory usage: 89 MB
% 121.72/17.93 % (2346166)Instructions burned: 182 (million)
% 121.72/17.93 % (2346165)Instruction limit reached!
% 121.72/17.93 % (2346165)------------------------------
% 121.72/17.93 % (2346165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.72/17.93 % (2346165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.72/17.93 % (2346165)CaDiCaL version: 2.1.3
% 121.72/17.93 % (2346165)Termination reason: Instruction limit
% 121.72/17.93 % (2346165)Termination phase: Saturation
% 121.72/17.93 % (2346165)Time elapsed: 0.132 s
% 121.72/17.93 % (2346165)Peak memory usage: 89 MB
% 121.72/17.93 % (2346165)Instructions burned: 136 (million)
% 121.72/17.93 % (2346176)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1067569884:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 121.72/17.93 % (2346167)Instruction limit reached!
% 121.72/17.93 % (2346167)------------------------------
% 121.72/17.93 % (2346167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.72/17.93 % (2346167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.72/17.93 % (2346167)CaDiCaL version: 2.1.3
% 121.72/17.93 % (2346167)Termination reason: Instruction limit
% 121.72/17.93 % (2346167)Termination phase: Saturation
% 121.72/17.93 % (2346167)Time elapsed: 0.251 s
% 121.72/17.93 % (2346167)Peak memory usage: 91 MB
% 121.72/17.93 % (2346167)Instructions burned: 258 (million)
% 121.72/17.93 % (2346177)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=396013108:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 121.72/17.93 % (2346179)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3455039769:i=215:ep=RSTC_2994 on theBenchmark for (2994ds/215Mi)
% 121.72/17.93 % (2346179)Instruction limit reached!
% 121.72/17.93 % (2346179)------------------------------
% 121.72/17.93 % (2346179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.72/17.93 % (2346179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.72/17.93 % (2346179)CaDiCaL version: 2.1.3
% 121.72/17.93 % (2346179)Termination reason: Instruction limit
% 121.72/17.93 % (2346179)Termination phase: Saturation
% 121.72/17.93 % (2346179)Time elapsed: 0.202 s
% 159.32/23.23 % (2346179)Peak memory usage: 90 MB
% 159.32/23.23 % (2346179)Instructions burned: 216 (million)
% 159.32/23.23 % (2346168)Instruction limit reached!
% 159.32/23.23 % (2346168)------------------------------
% 159.32/23.23 % (2346168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.32/23.23 % (2346168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.32/23.23 % (2346168)CaDiCaL version: 2.1.3
% 159.32/23.23 % (2346168)Termination reason: Instruction limit
% 159.32/23.23 % (2346168)Termination phase: Saturation
% 159.32/23.23 % (2346168)Time elapsed: 0.994 s
% 159.32/23.23 % (2346168)Peak memory usage: 101 MB
% 159.32/23.23 % (2346168)Instructions burned: 1187 (million)
% 159.32/23.23 % (2346182)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=3306190824:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/317Mi)
% 159.32/23.23 % (2346183)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=2030454449:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2987 on theBenchmark for (2987ds/12125Mi)
% 159.32/23.23 % (2346182)Instruction limit reached!
% 159.32/23.23 % (2346182)------------------------------
% 159.32/23.23 % (2346182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.32/23.23 % (2346182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.32/23.23 % (2346182)CaDiCaL version: 2.1.3
% 159.32/23.23 % (2346182)Termination reason: Instruction limit
% 159.32/23.23 % (2346182)Termination phase: Saturation
% 159.32/23.23 % (2346182)Time elapsed: 0.280 s
% 159.32/23.23 % (2346182)Peak memory usage: 94 MB
% 159.32/23.23 % (2346182)Instructions burned: 317 (million)
% 159.32/23.23 % (2346186)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1708877405:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2983 on theBenchmark for (2983ds/2836Mi)
% 159.32/23.23 % (2346176)Instruction limit reached!
% 159.32/23.23 % (2346176)------------------------------
% 159.32/23.23 % (2346176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.32/23.23 % (2346176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.32/23.23 % (2346176)CaDiCaL version: 2.1.3
% 159.32/23.23 % (2346176)Termination reason: Instruction limit
% 159.32/23.23 % (2346176)Termination phase: Saturation
% 159.32/23.23 % (2346176)Time elapsed: 2.077 s
% 159.32/23.23 % (2346176)Peak memory usage: 140 MB
% 159.32/23.23 % (2346176)Instructions burned: 2051 (million)
% 159.32/23.23 % (2346188)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=701432068:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2974 on theBenchmark for (2974ds/14534Mi)
% 159.32/23.23 % (2346177)Instruction limit reached!
% 159.32/23.23 % (2346177)------------------------------
% 159.32/23.23 % (2346177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.32/23.23 % (2346177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.32/23.23 % (2346177)CaDiCaL version: 2.1.3
% 159.32/23.23 % (2346177)Termination reason: Instruction limit
% 159.32/23.23 % (2346177)Termination phase: Saturation
% 159.32/23.23 % (2346177)Time elapsed: 2.652 s
% 159.32/23.23 % (2346177)Peak memory usage: 166 MB
% 159.32/23.23 % (2346177)Instructions burned: 4949 (million)
% 159.32/23.23 % (2346190)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=380685974:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2966 on theBenchmark for (2966ds/11832Mi)
% 159.32/23.23 % (2346186)Instruction limit reached!
% 159.32/23.23 % (2346186)------------------------------
% 159.32/23.23 % (2346186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.32/23.23 % (2346186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.32/23.23 % (2346186)CaDiCaL version: 2.1.3
% 159.32/23.23 % (2346186)Termination reason: Instruction limit
% 159.32/23.23 % (2346186)Termination phase: Saturation
% 159.32/23.23 % (2346186)Time elapsed: 3.019 s
% 159.32/23.23 % (2346186)Peak memory usage: 131 MB
% 159.32/23.23 % (2346186)Instructions burned: 2836 (million)
% 159.32/23.23 % (2346192)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=1561096216:i=2279:fgj=on:bd=all_2950 on theBenchmark for (2950ds/2279Mi)
% 159.32/23.23 % (2346192)Instruction limit reached!
% 159.32/23.23 % (2346192)------------------------------
% 152.17/36.36 % (2346192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346192)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346192)Termination reason: Instruction limit
% 152.17/36.36 % (2346192)Termination phase: Saturation
% 152.17/36.36 % (2346192)Time elapsed: 2.267 s
% 152.17/36.36 % (2346192)Peak memory usage: 139 MB
% 152.17/36.36 % (2346192)Instructions burned: 2279 (million)
% 152.17/36.36 % (2346194)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=1847318568:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2924 on theBenchmark for (2924ds/6225Mi)
% 152.17/36.36 % (2346190)Instruction limit reached!
% 152.17/36.36 % (2346190)------------------------------
% 152.17/36.36 % (2346190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346190)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346190)Termination reason: Instruction limit
% 152.17/36.36 % (2346190)Termination phase: Saturation
% 152.17/36.36 % (2346190)Time elapsed: 6.768 s
% 152.17/36.36 % (2346190)Peak memory usage: 226 MB
% 152.17/36.36 % (2346190)Instructions burned: 11832 (million)
% 152.17/36.36 % (2346200)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=627356810:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2896 on theBenchmark for (2896ds/21755Mi)
% 152.17/36.36 % (2346194)Instruction limit reached!
% 152.17/36.36 % (2346194)------------------------------
% 152.17/36.36 % (2346194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346194)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346194)Termination reason: Instruction limit
% 152.17/36.36 % (2346194)Termination phase: Saturation
% 152.17/36.36 % (2346194)Time elapsed: 4.494 s
% 152.17/36.36 % (2346194)Peak memory usage: 143 MB
% 152.17/36.36 % (2346194)Instructions burned: 6225 (million)
% 152.17/36.36 % (2346202)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=3116363432:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2876 on theBenchmark for (2876ds/16427Mi)
% 152.17/36.36 % (2346183)Instruction limit reached!
% 152.17/36.36 % (2346183)------------------------------
% 152.17/36.36 % (2346183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346183)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346183)Termination reason: Instruction limit
% 152.17/36.36 % (2346183)Termination phase: Saturation
% 152.17/36.36 % (2346183)Time elapsed: 11.623 s
% 152.17/36.36 % (2346183)Peak memory usage: 244 MB
% 152.17/36.36 % (2346183)Instructions burned: 12126 (million)
% 152.17/36.36 % (2346352)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=3385543304:i=9356:fgj=on:bd=preordered:av=off_2867 on theBenchmark for (2867ds/9356Mi)
% 152.17/36.36 % (2346188)Instruction limit reached!
% 152.17/36.36 % (2346188)------------------------------
% 152.17/36.36 % (2346188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346188)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346188)Termination reason: Instruction limit
% 152.17/36.36 % (2346188)Termination phase: Saturation
% 152.17/36.36 % (2346188)Time elapsed: 12.899 s
% 152.17/36.36 % (2346188)Peak memory usage: 245 MB
% 152.17/36.36 % (2346188)Instructions burned: 14535 (million)
% 152.17/36.36 % (2346360)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=227105613:i=2070:kws=inv_precedence:slsql=off:bd=all_2842 on theBenchmark for (2842ds/2070Mi)
% 152.17/36.36 % (2346360)Instruction limit reached!
% 152.17/36.36 % (2346360)------------------------------
% 152.17/36.36 % (2346360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346360)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346360)Termination reason: Instruction limit
% 152.17/36.36 % (2346360)Termination phase: Saturation
% 152.17/36.36 % (2346360)Time elapsed: 1.190 s
% 152.17/36.36 % (2346360)Peak memory usage: 122 MB
% 152.17/36.36 % (2346360)Instructions burned: 2070 (million)
% 152.17/36.36 % (2346362)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=1801296619:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2828 on theBenchmark for (2828ds/6461Mi)
% 152.17/36.36 % (2346352)Instruction limit reached!
% 152.17/36.36 % (2346352)------------------------------
% 152.17/36.36 % (2346352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346352)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346352)Termination reason: Instruction limit
% 152.17/36.36 % (2346352)Termination phase: Saturation
% 152.17/36.36 % (2346352)Time elapsed: 5.781 s
% 152.17/36.36 % (2346352)Peak memory usage: 198 MB
% 152.17/36.36 % (2346352)Instructions burned: 9357 (million)
% 152.17/36.36 % (2346364)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=3666464605:i=2310:bd=all:ss=included_2808 on theBenchmark for (2808ds/2310Mi)
% 152.17/36.36 % (2346200)Instruction limit reached!
% 152.17/36.36 % (2346200)------------------------------
% 152.17/36.36 % (2346200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346200)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346200)Termination reason: Instruction limit
% 152.17/36.36 % (2346200)Termination phase: Saturation
% 152.17/36.36 % (2346200)Time elapsed: 9.639 s
% 152.17/36.36 % (2346200)Peak memory usage: 223 MB
% 152.17/36.36 % (2346200)Instructions burned: 21758 (million)
% 152.17/36.36 % (2346366)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=407321427:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2797 on theBenchmark for (2797ds/2616Mi)
% 152.17/36.36 % (2346364)Instruction limit reached!
% 152.17/36.36 % (2346364)------------------------------
% 152.17/36.36 % (2346364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346364)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346364)Termination reason: Instruction limit
% 152.17/36.36 % (2346364)Termination phase: Saturation
% 152.17/36.36 % (2346364)Time elapsed: 1.392 s
% 152.17/36.36 % (2346364)Peak memory usage: 99 MB
% 152.17/36.36 % (2346364)Instructions burned: 2311 (million)
% 152.17/36.36 % (2346368)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=3686068830:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2792 on theBenchmark for (2792ds/30521Mi)
% 152.17/36.36 % (2346362)Instruction limit reached!
% 152.17/36.36 % (2346362)------------------------------
% 152.17/36.36 % (2346362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346362)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346362)Termination reason: Instruction limit
% 152.17/36.36 % (2346362)Termination phase: Saturation
% 152.17/36.36 % (2346362)Time elapsed: 3.712 s
% 152.17/36.36 % (2346362)Peak memory usage: 179 MB
% 152.17/36.36 % (2346362)Instructions burned: 6462 (million)
% 152.17/36.36 % (2346370)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=1113672839:i=3258:fgj=on:bd=all:ins=1_2789 on theBenchmark for (2789ds/3258Mi)
% 152.17/36.36 % (2346366)Instruction limit reached!
% 152.17/36.36 % (2346366)------------------------------
% 152.17/36.36 % (2346366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346366)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346366)Termination reason: Instruction limit
% 152.17/36.36 % (2346366)Termination phase: Saturation
% 152.17/36.36 % (2346366)Time elapsed: 0.853 s
% 152.17/36.36 % (2346366)Peak memory usage: 123 MB
% 152.17/36.36 % (2346366)Instructions burned: 2616 (million)
% 152.17/36.36 % (2346372)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=961501866:i=5037:kws=precedence_2788 on theBenchmark for (2788ds/5037Mi)
% 152.17/36.36 % (2346370)Instruction limit reached!
% 152.17/36.36 % (2346370)------------------------------
% 152.17/36.36 % (2346370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346370)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346370)Termination reason: Instruction limit
% 152.17/36.36 % (2346370)Termination phase: Saturation
% 152.17/36.36 % (2346370)Time elapsed: 1.245 s
% 152.17/36.36 % (2346370)Peak memory usage: 145 MB
% 152.17/36.36 % (2346370)Instructions burned: 3260 (million)
% 152.17/36.36 % (2346374)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=3393359813:i=65240_2775 on theBenchmark for (2775ds/65240Mi)
% 152.17/36.36 % (2346202)Instruction limit reached!
% 152.17/36.36 % (2346202)------------------------------
% 152.17/36.36 % (2346202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346202)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346202)Termination reason: Instruction limit
% 152.17/36.36 % (2346202)Termination phase: Saturation
% 152.17/36.36 % (2346202)Time elapsed: 10.335 s
% 152.17/36.36 % (2346202)Peak memory usage: 247 MB
% 152.17/36.36 % (2346202)Instructions burned: 16427 (million)
% 152.17/36.36 % (2346376)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=2534413794:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2771 on theBenchmark for (2771ds/16502Mi)
% 152.17/36.36 % (2346372)Instruction limit reached!
% 152.17/36.36 % (2346372)------------------------------
% 152.17/36.36 % (2346372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346372)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346372)Termination reason: Instruction limit
% 152.17/36.36 % (2346372)Termination phase: Saturation
% 152.17/36.36 % (2346372)Time elapsed: 2.725 s
% 152.17/36.36 % (2346372)Peak memory usage: 168 MB
% 152.17/36.36 % (2346372)Instructions burned: 5038 (million)
% 152.17/36.36 % (2346378)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=2484651233:i=7623:bd=preordered:er=filter_2759 on theBenchmark for (2759ds/7623Mi)
% 152.17/36.36 % (2346378)Instruction limit reached!
% 152.17/36.36 % (2346378)------------------------------
% 152.17/36.36 % (2346378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346378)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346378)Termination reason: Instruction limit
% 152.17/36.36 % (2346378)Termination phase: Saturation
% 152.17/36.36 % (2346378)Time elapsed: 4.705 s
% 152.17/36.36 % (2346378)Peak memory usage: 180 MB
% 152.17/36.36 % (2346378)Instructions burned: 7623 (million)
% 152.17/36.36 % (2346496)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=2833068072:i=8183:kws=frequency:add=off:gsp=on_2710 on theBenchmark for (2710ds/8183Mi)
% 152.17/36.36 % (2346162)First to succeed.
% 152.17/36.36 % (2346162)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2346157"
% 152.17/36.36 % (2346376)Instruction limit reached!
% 152.17/36.36 % (2346376)------------------------------
% 152.17/36.36 % (2346376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.17/36.36 % (2346376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.17/36.36 % (2346376)CaDiCaL version: 2.1.3
% 152.17/36.36 % (2346376)Termination reason: Instruction limit
% 152.17/36.36 % (2346376)Termination phase: Saturation
% 152.17/36.36 % (2346376)Time elapsed: 12.213 s
% 152.17/36.36 % (2346376)Peak memory usage: 265 MB
% 152.17/36.36 % (2346376)Instructions burned: 16502 (million)
% 152.17/36.36 % (2346728)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:bsr=unit_only:random_seed=3927172619:i=8387_2647 on theBenchmark for (2647ds/8387Mi)
% 152.17/36.36 % (2346162)Refutation found. Thanks to Tanya!
% 152.17/36.36 % SZS status Unsatisfiable for theBenchmark
% 152.17/36.36 % SZS output start Proof for theBenchmark
% See solution above
% 252.82/36.55 % (2346162)------------------------------
% 252.82/36.55 % (2346162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.82/36.55 % (2346162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.82/36.55 % (2346162)CaDiCaL version: 2.1.3
% 252.82/36.55 % (2346162)Termination reason: Refutation
% 252.82/36.55 % (2346162)Time elapsed: 34.892 s
% 252.82/36.55 % (2346162)Peak memory usage: 412 MB
% 252.82/36.55 % (2346162)Instructions burned: 42883 (million)
% 252.82/36.55 % (2346162)------------------------------
% 252.82/36.55 % (2346162)------------------------------
% 252.82/36.55 % (2346157)Success in time 35.543 s
% 252.82/36.55 % Vampire exiting
%------------------------------------------------------------------------------