%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP655+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 : n013.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:27 AM UTC 2026
% Result : Theorem 67.64s 16.38s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 80
% Number of leaves : 11
% Syntax : Number of formulae : 306 ( 294 unt; 5 def)
% Number of atoms : 318 ( 303 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 26 ( 14 ~; 8 |; 2 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 525 ( 0 sgn 523 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X1,ld(X1,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f01) ).
fof(f2,axiom,
! [X0,X1] : ld(X1,mult(X1,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X1,X0),X0) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X1,X0),X0) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f04) ).
fof(f5,axiom,
! [X0,X1,X2] : mult(X2,mult(X1,mult(X0,X1))) = mult(mult(mult(X2,X1),X0),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f05) ).
fof(f6,conjecture,
! [X0,X1] :
( mult(X0,ld(X1,X1)) = X0
& mult(ld(X1,X1),X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f7,negated_conjecture,
~ ! [X0,X1] :
( mult(X0,ld(X1,X1)) = X0
& mult(ld(X1,X1),X0) = X0 ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
? [X0,X1] :
( mult(X0,ld(X1,X1)) != X0
| mult(ld(X1,X1),X0) != X0 ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
( sK0 != mult(sK0,ld(sK1,sK1))
| sK0 != mult(ld(sK1,sK1),sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f8]) ).
fof(f10,plain,
! [X0,X1] : mult(X1,ld(X1,X0)) = X0,
inference(cnf_transformation,[],[f1]) ).
fof(f11,plain,
! [X0,X1] : ld(X1,mult(X1,X0)) = X0,
inference(cnf_transformation,[],[f2]) ).
fof(f12,plain,
! [X0,X1] : mult(rd(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f3]) ).
fof(f13,plain,
! [X0,X1] : rd(mult(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f4]) ).
fof(f14,plain,
! [X2,X0,X1] : mult(X2,mult(X1,mult(X0,X1))) = mult(mult(mult(X2,X1),X0),X1),
inference(cnf_transformation,[],[f5]) ).
fof(f15,plain,
( sK0 != mult(sK0,ld(sK1,sK1))
| sK0 != mult(ld(sK1,sK1),sK0) ),
inference(cnf_transformation,[],[f9]) ).
fof(f16,definition,
sF2 = ld(sK1,sK1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f17,plain,
ld(sK1,sK1) = sF2,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF3 = mult(sK0,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f19,plain,
mult(sK0,sF2) = sF3,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF4 = mult(sF2,sK0),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f21,plain,
mult(sF2,sK0) = sF4,
inference(reorient_equations,[],[f20]) ).
fof(f22,plain,
( sK0 != sF3
| sK0 != sF4 ),
inference(definition_folding,[],[f15,f21,f17,f19,f17]) ).
fof(f24,definition,
( spl5_1
<=> sK0 = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
fof(f26,plain,
( sK0 != sF4
| spl5_1 ),
inference(avatar_component_clause,[],[f24]) ).
fof(f28,definition,
( spl5_2
<=> sK0 = sF3 ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
fof(f31,plain,
( ~ spl5_1
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f22,f28,f24]) ).
fof(f32,plain,
sK1 = mult(sK1,sF2),
inference(superposition,[],[f10,f17]) ).
fof(f35,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),mult(X2,ld(X1,X0)))) = mult(mult(X0,X2),ld(X1,X0)),
inference(superposition,[],[f14,f10]) ).
fof(f42,plain,
! [X2,X0,X1] : mult(rd(X0,X1),mult(X1,mult(X2,X1))) = mult(mult(X0,X2),X1),
inference(superposition,[],[f14,f12]) ).
fof(f43,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f11,f12]) ).
fof(f44,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f13,f10]) ).
fof(f45,plain,
! [X2,X0,X1] : mult(mult(X0,X1),X2) = rd(mult(X0,mult(X1,mult(X2,X1))),X1),
inference(superposition,[],[f13,f14]) ).
fof(f46,plain,
sK0 = rd(sF3,sF2),
inference(superposition,[],[f13,f19]) ).
fof(f51,plain,
! [X2,X0,X1] : mult(mult(X1,ld(X2,X0)),X2) = rd(mult(X1,mult(ld(X2,X0),X0)),ld(X2,X0)),
inference(superposition,[],[f45,f10]) ).
fof(f53,plain,
! [X2,X0,X1] : mult(mult(X1,X2),rd(X0,X2)) = rd(mult(X1,mult(X2,X0)),X2),
inference(superposition,[],[f45,f12]) ).
fof(f57,plain,
! [X2,X0,X1] : rd(X0,X1) = mult(mult(rd(X0,mult(X1,mult(X2,X1))),X1),X2),
inference(superposition,[],[f45,f12]) ).
fof(f67,plain,
! [X2,X0,X1] : rd(mult(rd(X0,X1),mult(X1,X2)),X1) = mult(X0,rd(X2,X1)),
inference(superposition,[],[f53,f12]) ).
fof(f89,plain,
! [X0,X1] : mult(mult(X0,X1),ld(X1,X0)) = mult(X1,mult(ld(X1,X0),X0)),
inference(superposition,[],[f35,f10]) ).
fof(f97,plain,
! [X2,X0,X1] : mult(ld(X2,X0),mult(X1,ld(X2,X0))) = ld(X2,mult(mult(X0,X1),ld(X2,X0))),
inference(superposition,[],[f11,f35]) ).
fof(f100,plain,
! [X0,X1] : mult(ld(X1,X0),mult(ld(ld(X1,X0),X1),X1)) = mult(X0,ld(ld(X1,X0),X1)),
inference(superposition,[],[f89,f10]) ).
fof(f129,plain,
! [X0] : mult(sF2,mult(X0,sF2)) = ld(sK1,mult(mult(sK1,X0),sF2)),
inference(superposition,[],[f97,f17]) ).
fof(f132,plain,
! [X2,X0,X1] : mult(X0,mult(X2,X0)) = ld(rd(X1,X0),mult(mult(X1,X2),X0)),
inference(superposition,[],[f97,f43]) ).
fof(f146,plain,
! [X2,X0,X1] : ld(rd(X2,X1),mult(X0,X1)) = mult(X1,mult(ld(X2,X0),X1)),
inference(superposition,[],[f132,f10]) ).
fof(f173,plain,
! [X2,X0,X1] : mult(X1,mult(ld(mult(X0,X1),X2),X1)) = ld(X0,mult(X2,X1)),
inference(superposition,[],[f146,f13]) ).
fof(f207,plain,
! [X0] : ld(sK0,mult(X0,sF2)) = mult(sF2,mult(ld(sF3,X0),sF2)),
inference(superposition,[],[f173,f19]) ).
fof(f213,plain,
! [X2,X0,X1] : mult(ld(mult(X0,X2),X1),X2) = ld(X2,ld(X0,mult(X1,X2))),
inference(superposition,[],[f11,f173]) ).
fof(f254,plain,
! [X2,X0,X1] : mult(mult(X1,rd(X0,X2)),X2) = mult(rd(X1,X2),mult(X2,X0)),
inference(superposition,[],[f42,f12]) ).
fof(f276,plain,
ld(sK1,mult(sK1,sF2)) = mult(sF2,mult(sF2,sF2)),
inference(superposition,[],[f129,f32]) ).
fof(f288,plain,
sF2 = mult(sF2,mult(sF2,sF2)),
inference(forward_demodulation,[],[f276,f11]) ).
fof(f291,plain,
! [X0] : mult(mult(X0,sF2),sF2) = rd(mult(X0,sF2),sF2),
inference(superposition,[],[f45,f288]) ).
fof(f292,plain,
mult(sF2,sF2) = ld(sF2,sF2),
inference(superposition,[],[f11,f288]) ).
fof(f304,plain,
! [X0] : mult(mult(X0,sF2),sF2) = X0,
inference(forward_demodulation,[],[f291,f13]) ).
fof(f316,plain,
! [X0] : mult(X0,sF2) = rd(X0,sF2),
inference(superposition,[],[f13,f304]) ).
fof(f320,plain,
! [X0,X1] : rd(mult(mult(X0,sF2),mult(sF2,X1)),sF2) = mult(X0,rd(X1,sF2)),
inference(superposition,[],[f53,f304]) ).
fof(f344,plain,
! [X0,X1] : rd(mult(X0,mult(sF2,X1)),sF2) = mult(rd(X0,sF2),rd(X1,sF2)),
inference(superposition,[],[f53,f316]) ).
fof(f348,plain,
! [X0,X1] : mult(sF2,mult(ld(X1,X0),sF2)) = ld(rd(X1,sF2),rd(X0,sF2)),
inference(superposition,[],[f146,f316]) ).
fof(f357,plain,
! [X0] : rd(rd(X0,sF2),sF2) = X0,
inference(superposition,[],[f12,f316]) ).
fof(f358,plain,
sF3 = rd(sK0,sF2),
inference(superposition,[],[f19,f316]) ).
fof(f368,plain,
! [X0,X1] : ld(rd(X1,sF2),rd(X0,sF2)) = mult(sF2,rd(ld(X1,X0),sF2)),
inference(forward_demodulation,[],[f348,f316]) ).
fof(f503,plain,
! [X2,X0,X1] : mult(X1,rd(ld(X2,X0),X2)) = rd(mult(rd(X1,X2),X0),X2),
inference(superposition,[],[f67,f10]) ).
fof(f601,plain,
! [X2,X0,X1] : rd(ld(X1,X2),X1) = ld(X0,rd(mult(rd(X0,X1),X2),X1)),
inference(superposition,[],[f11,f503]) ).
fof(f620,plain,
! [X2,X3,X0,X1] : mult(X0,mult(X1,mult(rd(ld(X2,X3),X2),X1))) = mult(rd(mult(rd(mult(X0,X1),X2),X3),X2),X1),
inference(superposition,[],[f14,f503]) ).
fof(f718,plain,
! [X2,X0,X1] : ld(X2,ld(X1,X0)) = mult(ld(mult(X1,X2),rd(X0,X2)),X2),
inference(superposition,[],[f213,f12]) ).
fof(f724,plain,
! [X0,X1] : mult(ld(mult(X1,X0),X1),X0) = ld(X0,X0),
inference(superposition,[],[f213,f11]) ).
fof(f777,plain,
! [X0,X1] : ld(X1,X1) = mult(ld(X0,rd(X0,X1)),X1),
inference(superposition,[],[f724,f12]) ).
fof(f790,plain,
! [X0,X1] : ld(mult(X1,X0),X1) = rd(ld(X0,X0),X0),
inference(superposition,[],[f13,f724]) ).
fof(f860,plain,
! [X0,X1] : ld(X0,rd(X0,X1)) = rd(ld(X1,X1),X1),
inference(superposition,[],[f790,f12]) ).
fof(f874,plain,
! [X2,X0,X1] : mult(rd(ld(X0,X0),X0),mult(X2,rd(ld(X0,X0),X0))) = ld(mult(X1,X0),mult(mult(X1,X2),rd(ld(X0,X0),X0))),
inference(superposition,[],[f97,f790]) ).
fof(f878,plain,
! [X2,X0,X1] : rd(mult(rd(X2,X1),X1),X1) = mult(X2,ld(mult(X0,X1),X0)),
inference(superposition,[],[f503,f790]) ).
fof(f887,plain,
! [X2,X0,X1] : rd(X2,X1) = mult(X2,ld(mult(X0,X1),X0)),
inference(forward_demodulation,[],[f878,f13]) ).
fof(f890,plain,
! [X2,X0,X1] : mult(rd(ld(X0,X0),X0),mult(X2,rd(ld(X0,X0),X0))) = ld(mult(X1,X0),rd(mult(rd(mult(X1,X2),X0),X0),X0)),
inference(forward_demodulation,[],[f874,f503]) ).
fof(f905,plain,
! [X2,X0,X1] : mult(rd(ld(X0,X0),X0),mult(X2,rd(ld(X0,X0),X0))) = ld(mult(X1,X0),rd(mult(X1,X2),X0)),
inference(forward_demodulation,[],[f890,f13]) ).
fof(f918,plain,
! [X2,X0,X1] : ld(mult(X1,X0),rd(mult(X1,X2),X0)) = mult(rd(ld(X0,X0),X0),rd(mult(rd(X2,X0),X0),X0)),
inference(forward_demodulation,[],[f905,f503]) ).
fof(f921,plain,
! [X2,X0,X1] : ld(mult(X1,X0),rd(mult(X1,X2),X0)) = mult(rd(ld(X0,X0),X0),rd(X2,X0)),
inference(forward_demodulation,[],[f918,f13]) ).
fof(f927,plain,
! [X2,X0,X1] : mult(X1,ld(X0,X2)) = rd(X1,ld(X2,X0)),
inference(superposition,[],[f887,f10]) ).
fof(f928,plain,
! [X2,X3,X0,X1] : rd(X2,ld(mult(X3,X1),X3)) = mult(X2,ld(rd(X0,X1),X0)),
inference(superposition,[],[f887,f887]) ).
fof(f940,plain,
! [X2,X0,X1] : rd(X1,X2) = mult(X1,ld(X0,rd(X0,X2))),
inference(superposition,[],[f887,f12]) ).
fof(f945,plain,
! [X0] : rd(X0,mult(sF2,sF2)) = mult(X0,ld(sF2,sF2)),
inference(superposition,[],[f887,f288]) ).
fof(f955,plain,
! [X2,X0,X1] : rd(rd(X0,X1),ld(mult(X2,X1),X2)) = X0,
inference(superposition,[],[f13,f887]) ).
fof(f980,plain,
! [X0,X1] : mult(sF2,mult(ld(mult(X1,X0),X1),sF2)) = ld(sK1,mult(rd(sK1,X0),sF2)),
inference(superposition,[],[f129,f887]) ).
fof(f981,plain,
! [X0,X1] : mult(sF2,mult(ld(mult(X1,X0),X1),sF2)) = ld(sK1,rd(rd(sK1,X0),sF2)),
inference(forward_demodulation,[],[f980,f316]) ).
fof(f1000,plain,
! [X0] : mult(X0,mult(sF2,sF2)) = rd(X0,mult(sF2,sF2)),
inference(forward_demodulation,[],[f945,f292]) ).
fof(f1010,plain,
! [X2,X3,X1] : mult(X2,X1) = rd(X2,ld(mult(X3,X1),X3)),
inference(forward_demodulation,[],[f928,f43]) ).
fof(f1011,plain,
! [X0,X1] : ld(sK1,rd(rd(sK1,X0),sF2)) = mult(sF2,rd(ld(mult(X1,X0),X1),sF2)),
inference(forward_demodulation,[],[f981,f316]) ).
fof(f1023,plain,
! [X0] : mult(X0,rd(sF2,sF2)) = rd(X0,rd(sF2,sF2)),
inference(forward_demodulation,[],[f1000,f316]) ).
fof(f1035,plain,
! [X2,X3,X0,X1] : mult(X3,mult(ld(X0,X1),mult(X2,ld(X0,X1)))) = rd(X3,ld(mult(mult(X1,X2),ld(X0,X1)),X0)),
inference(superposition,[],[f927,f97]) ).
fof(f1038,plain,
! [X2,X0,X1] : mult(X1,X0) = rd(X1,ld(X2,rd(X2,X0))),
inference(superposition,[],[f927,f43]) ).
fof(f1039,plain,
! [X2,X3,X0,X1] : mult(X2,mult(X0,mult(X1,X0))) = rd(X2,ld(mult(mult(X3,X1),X0),rd(X3,X0))),
inference(superposition,[],[f927,f132]) ).
fof(f1040,plain,
! [X2,X3,X0,X1] : mult(X3,mult(X0,mult(ld(X1,X2),X0))) = rd(X3,ld(mult(X2,X0),rd(X1,X0))),
inference(superposition,[],[f927,f146]) ).
fof(f1076,plain,
! [X0,X1] : mult(X1,mult(ld(X1,X0),X0)) = rd(mult(X0,X1),ld(X0,X1)),
inference(superposition,[],[f89,f927]) ).
fof(f1078,plain,
! [X2,X3,X0,X1] : mult(X0,mult(ld(X1,X2),mult(X3,ld(X1,X2)))) = rd(mult(mult(X0,ld(X1,X2)),X3),ld(X2,X1)),
inference(superposition,[],[f14,f927]) ).
fof(f1085,plain,
! [X2,X3,X0,X1] : mult(X0,mult(ld(X1,X2),mult(X3,ld(X1,X2)))) = rd(mult(rd(X0,ld(X2,X1)),X3),ld(X2,X1)),
inference(forward_demodulation,[],[f1078,f927]) ).
fof(f1110,plain,
! [X2,X3,X0,X1] : mult(X3,mult(ld(X0,X1),mult(X2,ld(X0,X1)))) = rd(X3,ld(rd(mult(X1,X2),ld(X1,X0)),X0)),
inference(forward_demodulation,[],[f1035,f927]) ).
fof(f1112,plain,
! [X2,X3,X0,X1] : rd(mult(rd(X0,ld(X2,X1)),X3),ld(X2,X1)) = mult(X0,mult(ld(X1,X2),rd(X3,ld(X2,X1)))),
inference(forward_demodulation,[],[f1085,f927]) ).
fof(f1127,plain,
! [X2,X3,X0,X1] : rd(X3,ld(rd(mult(X1,X2),ld(X1,X0)),X0)) = mult(X3,mult(ld(X0,X1),rd(X2,ld(X1,X0)))),
inference(forward_demodulation,[],[f1110,f927]) ).
fof(f1132,plain,
! [X2,X3,X0,X1] : rd(X3,ld(rd(mult(X1,X2),ld(X1,X0)),X0)) = rd(mult(rd(X3,ld(X1,X0)),X2),ld(X1,X0)),
inference(forward_demodulation,[],[f1127,f1112]) ).
fof(f1154,plain,
! [X2,X0,X1] : mult(rd(ld(X0,X0),X0),mult(X2,rd(ld(X0,X0),X0))) = ld(X1,mult(mult(rd(X1,X0),X2),rd(ld(X0,X0),X0))),
inference(superposition,[],[f97,f860]) ).
fof(f1172,plain,
! [X2,X0,X1] : mult(rd(ld(X0,X0),X0),mult(X2,rd(ld(X0,X0),X0))) = ld(X1,rd(mult(rd(mult(rd(X1,X0),X2),X0),X0),X0)),
inference(forward_demodulation,[],[f1154,f503]) ).
fof(f1189,plain,
! [X2,X0,X1] : mult(rd(ld(X0,X0),X0),mult(X2,rd(ld(X0,X0),X0))) = ld(X1,rd(mult(rd(X1,X0),X2),X0)),
inference(forward_demodulation,[],[f1172,f13]) ).
fof(f1202,plain,
! [X2,X0] : mult(rd(ld(X0,X0),X0),mult(X2,rd(ld(X0,X0),X0))) = rd(ld(X0,X2),X0),
inference(forward_demodulation,[],[f1189,f601]) ).
fof(f1206,plain,
! [X2,X0] : mult(rd(ld(X0,X0),X0),rd(mult(rd(X2,X0),X0),X0)) = rd(ld(X0,X2),X0),
inference(forward_demodulation,[],[f1202,f503]) ).
fof(f1209,plain,
! [X2,X0] : mult(rd(ld(X0,X0),X0),rd(X2,X0)) = rd(ld(X0,X2),X0),
inference(forward_demodulation,[],[f1206,f13]) ).
fof(f1315,plain,
! [X2,X3,X0,X1] : mult(ld(X3,rd(X3,X1)),mult(ld(X2,X0),ld(X3,rd(X3,X1)))) = ld(rd(X2,ld(X3,rd(X3,X1))),rd(X0,X1)),
inference(superposition,[],[f146,f940]) ).
fof(f1327,plain,
! [X2,X0,X1] : ld(X0,rd(mult(rd(X0,X1),X2),X1)) = mult(ld(X0,rd(X0,X1)),mult(X2,ld(X0,rd(X0,X1)))),
inference(superposition,[],[f97,f940]) ).
fof(f1338,plain,
! [X2,X0,X1] : ld(X0,rd(mult(rd(X0,X1),X2),X1)) = mult(ld(X0,rd(X0,X1)),rd(X2,X1)),
inference(forward_demodulation,[],[f1327,f940]) ).
fof(f1349,plain,
! [X2,X3,X0,X1] : mult(ld(X3,rd(X3,X1)),mult(ld(X2,X0),ld(X3,rd(X3,X1)))) = ld(mult(X2,X1),rd(X0,X1)),
inference(forward_demodulation,[],[f1315,f1038]) ).
fof(f1378,plain,
! [X2,X0,X1] : rd(ld(X1,X2),X1) = mult(ld(X0,rd(X0,X1)),rd(X2,X1)),
inference(forward_demodulation,[],[f1338,f601]) ).
fof(f1386,plain,
! [X2,X3,X0,X1] : ld(mult(X2,X1),rd(X0,X1)) = mult(ld(X3,rd(X3,X1)),rd(ld(X2,X0),X1)),
inference(forward_demodulation,[],[f1349,f940]) ).
fof(f1401,plain,
! [X2,X0,X1] : ld(mult(X2,X1),rd(X0,X1)) = rd(ld(X1,ld(X2,X0)),X1),
inference(forward_demodulation,[],[f1386,f1378]) ).
fof(f1442,plain,
! [X2,X0,X1] : mult(X1,rd(X0,ld(X2,rd(X2,X0)))) = rd(mult(rd(X1,ld(X2,rd(X2,X0))),ld(X0,X0)),ld(X2,rd(X2,X0))),
inference(superposition,[],[f67,f777]) ).
fof(f1476,plain,
! [X2,X0,X1] : mult(X1,rd(X0,ld(X2,rd(X2,X0)))) = rd(X1,ld(rd(mult(X2,ld(X0,X0)),ld(X2,rd(X2,X0))),rd(X2,X0))),
inference(forward_demodulation,[],[f1442,f1132]) ).
fof(f1502,plain,
! [X2,X0,X1] : mult(X1,rd(X0,ld(X2,rd(X2,X0)))) = rd(X1,ld(mult(mult(X2,ld(X0,X0)),X0),rd(X2,X0))),
inference(forward_demodulation,[],[f1476,f1038]) ).
fof(f1519,plain,
! [X2,X0,X1] : mult(X1,rd(X0,ld(X2,rd(X2,X0)))) = mult(X1,mult(X0,mult(ld(X0,X0),X0))),
inference(forward_demodulation,[],[f1502,f1039]) ).
fof(f1531,plain,
! [X2,X0,X1] : mult(X1,rd(X0,ld(X2,rd(X2,X0)))) = rd(X1,ld(mult(X0,X0),rd(X0,X0))),
inference(forward_demodulation,[],[f1519,f1040]) ).
fof(f1534,plain,
! [X2,X0,X1] : mult(X1,rd(X0,ld(X2,rd(X2,X0)))) = rd(X1,rd(ld(X0,ld(X0,X0)),X0)),
inference(forward_demodulation,[],[f1531,f1401]) ).
fof(f1535,plain,
! [X0,X1] : rd(X1,rd(ld(X0,ld(X0,X0)),X0)) = mult(X1,mult(X0,X0)),
inference(forward_demodulation,[],[f1534,f1038]) ).
fof(f1772,plain,
! [X0] : rd(ld(sF2,X0),sF2) = mult(rd(mult(sF2,sF2),sF2),rd(X0,sF2)),
inference(superposition,[],[f1209,f292]) ).
fof(f1778,plain,
! [X0,X1] : mult(rd(ld(X1,X1),X1),X0) = rd(ld(X1,mult(X0,X1)),X1),
inference(superposition,[],[f1209,f13]) ).
fof(f1787,plain,
rd(ld(sF2,sF3),sF2) = mult(rd(ld(sF2,sF2),sF2),sK0),
inference(superposition,[],[f1209,f46]) ).
fof(f1794,plain,
! [X0,X1] : rd(ld(X0,X0),X0) = rd(rd(ld(X0,X1),X0),rd(X1,X0)),
inference(superposition,[],[f13,f1209]) ).
fof(f1820,plain,
rd(ld(sF2,sF3),sF2) = mult(rd(mult(sF2,sF2),sF2),sK0),
inference(forward_demodulation,[],[f1787,f292]) ).
fof(f1830,plain,
! [X0] : rd(ld(sF2,X0),sF2) = rd(mult(mult(sF2,sF2),mult(sF2,X0)),sF2),
inference(forward_demodulation,[],[f1772,f344]) ).
fof(f1838,plain,
mult(sF2,sK0) = rd(ld(sF2,sF3),sF2),
inference(forward_demodulation,[],[f1820,f13]) ).
fof(f1844,plain,
! [X0] : mult(sF2,rd(X0,sF2)) = rd(ld(sF2,X0),sF2),
inference(forward_demodulation,[],[f1830,f320]) ).
fof(f1849,plain,
sF4 = rd(ld(sF2,sF3),sF2),
inference(forward_demodulation,[],[f1838,f21]) ).
fof(f1858,plain,
ld(sF2,sF3) = mult(sF4,sF2),
inference(superposition,[],[f12,f1849]) ).
fof(f1861,plain,
! [X0] : rd(mult(X0,mult(sF2,ld(sF2,sF3))),sF2) = mult(mult(X0,sF2),sF4),
inference(superposition,[],[f53,f1849]) ).
fof(f1877,plain,
! [X0] : mult(rd(X0,sF2),sF4) = rd(mult(X0,mult(sF2,ld(sF2,sF3))),sF2),
inference(forward_demodulation,[],[f1861,f316]) ).
fof(f1879,plain,
ld(sF2,sF3) = rd(sF4,sF2),
inference(forward_demodulation,[],[f1858,f316]) ).
fof(f1887,plain,
! [X0] : mult(rd(X0,sF2),sF4) = rd(mult(X0,sF3),sF2),
inference(forward_demodulation,[],[f1877,f10]) ).
fof(f1909,plain,
! [X0] : mult(X0,rd(sF4,sF2)) = rd(X0,ld(sF3,sF2)),
inference(superposition,[],[f927,f1879]) ).
fof(f2893,plain,
! [X0] : rd(ld(sF2,mult(X0,sF2)),sF2) = mult(rd(mult(sF2,sF2),sF2),X0),
inference(superposition,[],[f1778,f292]) ).
fof(f2913,plain,
! [X0] : ld(X0,X0) = rd(ld(X0,mult(X0,X0)),X0),
inference(superposition,[],[f12,f1778]) ).
fof(f2920,plain,
! [X2,X0,X1] : mult(mult(X2,X1),rd(ld(X0,X0),X0)) = rd(mult(X2,mult(X1,rd(ld(X0,mult(X1,X0)),X0))),X1),
inference(superposition,[],[f45,f1778]) ).
fof(f2968,plain,
! [X2,X0,X1] : mult(mult(X2,X1),rd(ld(X0,X0),X0)) = rd(mult(X2,rd(mult(rd(X1,X0),mult(X1,X0)),X0)),X1),
inference(forward_demodulation,[],[f2920,f503]) ).
fof(f2972,plain,
! [X0] : ld(X0,X0) = rd(X0,X0),
inference(forward_demodulation,[],[f2913,f11]) ).
fof(f2979,plain,
! [X0] : mult(sF2,X0) = rd(ld(sF2,mult(X0,sF2)),sF2),
inference(forward_demodulation,[],[f2893,f13]) ).
fof(f2991,plain,
! [X2,X0,X1] : rd(mult(X2,rd(mult(rd(X1,X0),mult(X1,X0)),X0)),X1) = rd(mult(rd(mult(X2,X1),X0),X0),X0),
inference(forward_demodulation,[],[f2968,f503]) ).
fof(f2998,plain,
! [X0] : mult(sF2,X0) = rd(ld(sF2,rd(X0,sF2)),sF2),
inference(forward_demodulation,[],[f2979,f316]) ).
fof(f3008,plain,
! [X2,X0,X1] : rd(mult(X2,X1),X0) = rd(mult(X2,rd(mult(rd(X1,X0),mult(X1,X0)),X0)),X1),
inference(forward_demodulation,[],[f2991,f13]) ).
fof(f3053,plain,
! [X0,X1] : ld(X1,rd(X1,X0)) = rd(rd(X0,X0),X0),
inference(superposition,[],[f860,f2972]) ).
fof(f3054,plain,
! [X0,X1] : ld(mult(X1,X0),X1) = rd(rd(X0,X0),X0),
inference(superposition,[],[f790,f2972]) ).
fof(f3057,plain,
! [X0] : rd(X0,rd(X0,X0)) = X0,
inference(superposition,[],[f44,f2972]) ).
fof(f3058,plain,
! [X0,X1] : mult(mult(X1,rd(X0,X0)),X0) = rd(mult(X1,mult(rd(X0,X0),X0)),rd(X0,X0)),
inference(superposition,[],[f51,f2972]) ).
fof(f3062,plain,
! [X0] : mult(rd(X0,X0),mult(ld(rd(X0,X0),X0),X0)) = mult(X0,ld(rd(X0,X0),X0)),
inference(superposition,[],[f100,f2972]) ).
fof(f3063,plain,
! [X0,X1] : rd(mult(rd(X1,X0),X0),X0) = mult(X1,rd(rd(X0,X0),X0)),
inference(superposition,[],[f503,f2972]) ).
fof(f3065,plain,
! [X0,X1] : mult(X1,rd(X0,X0)) = rd(X1,rd(X0,X0)),
inference(superposition,[],[f927,f2972]) ).
fof(f3070,plain,
sF2 = rd(sK1,sK1),
inference(superposition,[],[f17,f2972]) ).
fof(f3074,plain,
! [X0,X1] : rd(X1,X0) = mult(X1,rd(rd(X0,X0),X0)),
inference(forward_demodulation,[],[f3063,f13]) ).
fof(f3075,plain,
! [X0] : mult(rd(X0,X0),mult(ld(rd(X0,X0),X0),X0)) = rd(X0,ld(X0,rd(X0,X0))),
inference(forward_demodulation,[],[f3062,f927]) ).
fof(f3078,plain,
! [X0,X1] : mult(mult(X1,rd(X0,X0)),X0) = rd(mult(X1,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f3058,f12]) ).
fof(f3082,plain,
! [X0] : mult(X0,X0) = mult(rd(X0,X0),mult(ld(rd(X0,X0),X0),X0)),
inference(forward_demodulation,[],[f3075,f1038]) ).
fof(f3085,plain,
! [X0,X1] : mult(rd(X1,X0),mult(X0,X0)) = rd(mult(X1,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f3078,f254]) ).
fof(f3087,plain,
! [X0] : mult(X0,X0) = rd(mult(X0,rd(X0,X0)),ld(X0,rd(X0,X0))),
inference(forward_demodulation,[],[f3082,f1076]) ).
fof(f3088,plain,
! [X0] : mult(X0,X0) = mult(mult(X0,rd(X0,X0)),X0),
inference(forward_demodulation,[],[f3087,f1038]) ).
fof(f3089,plain,
! [X0] : mult(X0,X0) = mult(rd(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f3088,f254]) ).
fof(f3090,plain,
! [X0] : mult(X0,X0) = rd(mult(X0,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f3089,f3085]) ).
fof(f3201,plain,
! [X0,X1] : rd(rd(X0,X1),rd(rd(X1,X1),X1)) = X0,
inference(superposition,[],[f13,f3074]) ).
fof(f3231,plain,
! [X0] : rd(rd(ld(X0,X0),X0),X0) = rd(ld(X0,rd(X0,X0)),X0),
inference(superposition,[],[f1209,f3074]) ).
fof(f3236,plain,
! [X0] : rd(ld(X0,rd(X0,X0)),X0) = rd(rd(rd(X0,X0),X0),X0),
inference(forward_demodulation,[],[f3231,f2972]) ).
fof(f4827,plain,
! [X0] : rd(X0,X0) = ld(mult(X0,X0),mult(X0,X0)),
inference(superposition,[],[f43,f3090]) ).
fof(f4853,plain,
! [X0] : rd(X0,X0) = rd(mult(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f4827,f2972]) ).
fof(f4919,plain,
! [X0] : rd(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)) = rd(rd(ld(X0,ld(X0,X0)),X0),rd(ld(X0,ld(X0,X0)),X0)),
inference(superposition,[],[f4853,f1209]) ).
fof(f4926,plain,
! [X0,X1] : rd(X1,mult(X0,X0)) = mult(X1,rd(rd(X0,X0),mult(X0,X0))),
inference(superposition,[],[f3074,f4853]) ).
fof(f4944,plain,
! [X0] : ld(mult(X0,X0),rd(X0,X0)) = rd(rd(X0,X0),mult(X0,X0)),
inference(superposition,[],[f3053,f4853]) ).
fof(f4945,plain,
! [X0] : rd(ld(X0,ld(X0,X0)),X0) = rd(rd(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f4944,f1401]) ).
fof(f4958,plain,
! [X0] : rd(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)) = mult(rd(ld(X0,ld(X0,X0)),X0),mult(X0,X0)),
inference(forward_demodulation,[],[f4919,f1535]) ).
fof(f4964,plain,
! [X0] : rd(ld(X0,rd(X0,X0)),X0) = rd(rd(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f4945,f2972]) ).
fof(f4975,plain,
! [X0] : rd(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)) = rd(mult(ld(X0,ld(X0,X0)),X0),rd(X0,X0)),
inference(forward_demodulation,[],[f4958,f3085]) ).
fof(f4979,plain,
! [X0] : rd(rd(rd(X0,X0),X0),X0) = rd(rd(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f4964,f3236]) ).
fof(f4989,plain,
! [X0] : rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),X0)) = rd(mult(ld(X0,rd(X0,X0)),X0),rd(X0,X0)),
inference(forward_demodulation,[],[f4975,f2972]) ).
fof(f5001,plain,
! [X0] : rd(ld(X0,X0),rd(X0,X0)) = rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),X0)),
inference(forward_demodulation,[],[f4989,f777]) ).
fof(f5005,plain,
! [X0] : rd(X0,X0) = rd(ld(X0,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f5001,f3201]) ).
fof(f5008,plain,
! [X0] : rd(X0,X0) = rd(rd(X0,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f5005,f2972]) ).
fof(f5217,plain,
! [X2,X0,X1] : ld(X1,ld(rd(X0,X1),X2)) = mult(ld(X0,rd(X2,X1)),X1),
inference(superposition,[],[f718,f12]) ).
fof(f7072,plain,
! [X2,X0,X1] : mult(X0,X2) = mult(rd(rd(X0,rd(X1,X2)),X2),mult(X2,X1)),
inference(superposition,[],[f254,f12]) ).
fof(f7632,plain,
sF2 = rd(sF2,sF2),
inference(superposition,[],[f5008,f3070]) ).
fof(f11208,plain,
! [X0] : ld(sF2,ld(sF2,X0)) = mult(ld(sF2,rd(X0,sF2)),sF2),
inference(superposition,[],[f5217,f7632]) ).
fof(f11275,plain,
! [X0] : rd(ld(sF2,rd(X0,sF2)),sF2) = ld(sF2,ld(sF2,X0)),
inference(forward_demodulation,[],[f11208,f316]) ).
fof(f11327,plain,
! [X0] : mult(sF2,X0) = ld(sF2,ld(sF2,X0)),
inference(forward_demodulation,[],[f11275,f2998]) ).
fof(f11383,plain,
! [X0] : ld(sF2,X0) = mult(sF2,mult(sF2,X0)),
inference(superposition,[],[f10,f11327]) ).
fof(f12669,plain,
! [X2,X0,X1] : rd(mult(X0,X1),mult(X1,X2)) = rd(rd(X0,rd(X2,X1)),X1),
inference(superposition,[],[f13,f7072]) ).
fof(f13092,plain,
! [X0,X1] : mult(X0,mult(X1,X1)) = rd(mult(mult(X0,X1),X1),rd(X1,X1)),
inference(superposition,[],[f3085,f13]) ).
fof(f13111,plain,
! [X0,X1] : mult(ld(mult(X0,X1),X0),mult(X1,X1)) = rd(mult(rd(X1,X1),X1),rd(X1,X1)),
inference(superposition,[],[f3085,f3054]) ).
fof(f13211,plain,
! [X0,X1] : rd(X1,rd(X1,X1)) = mult(ld(mult(X0,X1),X0),mult(X1,X1)),
inference(forward_demodulation,[],[f13111,f12]) ).
fof(f13274,plain,
! [X0,X1] : mult(ld(mult(X0,X1),X0),mult(X1,X1)) = X1,
inference(forward_demodulation,[],[f13211,f3057]) ).
fof(f13533,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = mult(mult(X0,mult(X1,X1)),rd(X1,X1)),
inference(superposition,[],[f12,f13092]) ).
fof(f13578,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = rd(mult(X0,mult(X1,X1)),rd(X1,X1)),
inference(forward_demodulation,[],[f13533,f3065]) ).
fof(f13871,plain,
! [X0,X1] : rd(rd(X0,X0),X0) = mult(ld(mult(X1,rd(rd(X0,X0),X0)),X1),rd(rd(rd(X0,X0),X0),X0)),
inference(superposition,[],[f13274,f3074]) ).
fof(f13880,plain,
! [X0,X1] : ld(mult(X1,X0),X1) = rd(X0,mult(X0,X0)),
inference(superposition,[],[f13,f13274]) ).
fof(f13934,plain,
! [X0,X1] : rd(rd(X0,X0),X0) = mult(ld(mult(X1,rd(rd(X0,X0),X0)),X1),rd(rd(X0,X0),mult(X0,X0))),
inference(forward_demodulation,[],[f13871,f4979]) ).
fof(f14002,plain,
! [X0,X1] : rd(rd(X0,X0),X0) = rd(ld(mult(X1,rd(rd(X0,X0),X0)),X1),mult(X0,X0)),
inference(forward_demodulation,[],[f13934,f4926]) ).
fof(f14050,plain,
! [X0,X1] : rd(rd(X0,X0),X0) = rd(ld(rd(X1,X0),X1),mult(X0,X0)),
inference(forward_demodulation,[],[f14002,f3074]) ).
fof(f14077,plain,
! [X0] : rd(rd(X0,X0),X0) = rd(X0,mult(X0,X0)),
inference(forward_demodulation,[],[f14050,f43]) ).
fof(f14173,plain,
! [X0,X1] : rd(X1,X0) = mult(X1,rd(X0,mult(X0,X0))),
inference(superposition,[],[f887,f13880]) ).
fof(f14565,plain,
! [X0,X1] : mult(mult(X0,mult(X1,X1)),X1) = mult(rd(mult(mult(X0,X1),X1),X1),mult(X1,X1)),
inference(superposition,[],[f7072,f13578]) ).
fof(f14612,plain,
! [X0,X1] : mult(mult(X0,mult(X1,X1)),X1) = rd(mult(mult(mult(X0,X1),X1),X1),rd(X1,X1)),
inference(forward_demodulation,[],[f14565,f3085]) ).
fof(f14662,plain,
! [X0,X1] : mult(mult(X0,X1),mult(X1,X1)) = mult(mult(X0,mult(X1,X1)),X1),
inference(forward_demodulation,[],[f14612,f13092]) ).
fof(f16139,plain,
! [X0] : ld(sK1,mult(rd(sK1,X0),sF2)) = mult(sF2,mult(rd(X0,mult(X0,X0)),sF2)),
inference(superposition,[],[f129,f14173]) ).
fof(f16140,plain,
! [X0] : mult(sF2,rd(sF2,X0)) = ld(sF2,rd(X0,mult(X0,X0))),
inference(superposition,[],[f11383,f14173]) ).
fof(f16141,plain,
! [X0] : ld(sK1,mult(rd(sK1,X0),sF2)) = mult(sF2,rd(rd(X0,mult(X0,X0)),sF2)),
inference(forward_demodulation,[],[f16139,f316]) ).
fof(f16227,plain,
! [X0] : ld(sK1,mult(rd(sK1,X0),sF2)) = rd(ld(sF2,rd(X0,mult(X0,X0))),sF2),
inference(forward_demodulation,[],[f16141,f1844]) ).
fof(f16295,plain,
! [X0] : ld(sK1,mult(rd(sK1,X0),sF2)) = rd(mult(sF2,rd(sF2,X0)),sF2),
inference(forward_demodulation,[],[f16227,f16140]) ).
fof(f16337,plain,
! [X0] : ld(sK1,rd(rd(sK1,X0),sF2)) = rd(mult(sF2,rd(sF2,X0)),sF2),
inference(forward_demodulation,[],[f16295,f316]) ).
fof(f17740,plain,
! [X0] : rd(rd(X0,sF4),sF2) = rd(mult(X0,sF2),mult(sF2,ld(sF2,sF3))),
inference(superposition,[],[f12669,f1849]) ).
fof(f17774,plain,
! [X0] : rd(rd(X0,sF3),sF2) = rd(mult(X0,sF2),mult(sF2,sK0)),
inference(superposition,[],[f12669,f358]) ).
fof(f17908,plain,
! [X0] : rd(rd(X0,sF3),sF2) = rd(mult(X0,sF2),sF4),
inference(forward_demodulation,[],[f17774,f21]) ).
fof(f17938,plain,
! [X0] : rd(rd(X0,sF4),sF2) = rd(mult(X0,sF2),sF3),
inference(forward_demodulation,[],[f17740,f10]) ).
fof(f17981,plain,
! [X0] : rd(rd(X0,sF3),sF2) = rd(rd(X0,sF2),sF4),
inference(forward_demodulation,[],[f17908,f316]) ).
fof(f17997,plain,
! [X0] : rd(rd(X0,sF4),sF2) = rd(rd(X0,sF2),sF3),
inference(forward_demodulation,[],[f17938,f316]) ).
fof(f18049,plain,
! [X0,X1] : rd(ld(X1,X1),X1) = rd(rd(X0,X1),rd(mult(X1,X0),X1)),
inference(superposition,[],[f1794,f11]) ).
fof(f18174,plain,
! [X0,X1] : rd(rd(ld(X0,X0),X0),X0) = rd(mult(rd(ld(X0,X1),X0),X0),mult(X0,X1)),
inference(superposition,[],[f12669,f1794]) ).
fof(f18225,plain,
! [X0,X1] : rd(rd(ld(X0,X0),X0),X0) = rd(ld(X0,X1),mult(X0,X1)),
inference(forward_demodulation,[],[f18174,f12]) ).
fof(f18346,plain,
! [X0,X1] : rd(rd(X1,X1),X1) = rd(rd(X0,X1),rd(mult(X1,X0),X1)),
inference(forward_demodulation,[],[f18049,f2972]) ).
fof(f18362,plain,
! [X0,X1] : rd(rd(rd(X0,X0),X0),X0) = rd(ld(X0,X1),mult(X0,X1)),
inference(forward_demodulation,[],[f18225,f2972]) ).
fof(f18477,plain,
! [X0,X1] : rd(X1,mult(X1,X1)) = rd(rd(X0,X1),rd(mult(X1,X0),X1)),
inference(forward_demodulation,[],[f18346,f14077]) ).
fof(f18487,plain,
! [X0,X1] : rd(rd(X0,X0),mult(X0,X0)) = rd(ld(X0,X1),mult(X0,X1)),
inference(forward_demodulation,[],[f18362,f4979]) ).
fof(f18720,plain,
! [X0] : rd(X0,sF2) = rd(rd(mult(X0,sF3),sF2),sF4),
inference(superposition,[],[f17981,f13]) ).
fof(f18842,plain,
! [X0] : ld(sF4,sF4) = mult(ld(rd(mult(X0,sF3),sF2),rd(X0,sF2)),sF4),
inference(superposition,[],[f777,f18720]) ).
fof(f18874,plain,
! [X0] : ld(sF4,sF4) = mult(mult(sF2,rd(ld(mult(X0,sF3),X0),sF2)),sF4),
inference(forward_demodulation,[],[f18842,f368]) ).
fof(f18896,plain,
ld(sF4,sF4) = mult(ld(sK1,rd(rd(sK1,sF3),sF2)),sF4),
inference(forward_demodulation,[],[f18874,f1011]) ).
fof(f18914,plain,
ld(sF4,sF4) = mult(rd(mult(sF2,rd(sF2,sF3)),sF2),sF4),
inference(forward_demodulation,[],[f18896,f16337]) ).
fof(f18925,plain,
ld(sF4,sF4) = rd(mult(mult(sF2,rd(sF2,sF3)),sF3),sF2),
inference(forward_demodulation,[],[f18914,f1887]) ).
fof(f18928,plain,
ld(sF4,sF4) = rd(mult(rd(sF2,sF3),mult(sF3,sF2)),sF2),
inference(forward_demodulation,[],[f18925,f254]) ).
fof(f18929,plain,
ld(sF4,sF4) = rd(mult(rd(sF2,sF3),rd(sF3,sF2)),sF2),
inference(forward_demodulation,[],[f18928,f316]) ).
fof(f18930,plain,
ld(sF4,sF4) = rd(mult(rd(sF2,sF3),sK0),sF2),
inference(forward_demodulation,[],[f18929,f46]) ).
fof(f18931,plain,
rd(sF4,sF4) = rd(mult(rd(sF2,sF3),sK0),sF2),
inference(forward_demodulation,[],[f18930,f2972]) ).
fof(f20721,plain,
ld(sK0,mult(sF3,sF2)) = mult(sF2,mult(rd(sF3,sF3),sF2)),
inference(superposition,[],[f207,f2972]) ).
fof(f20832,plain,
ld(sK0,mult(sF3,sF2)) = mult(sF2,rd(rd(sF3,sF3),sF2)),
inference(forward_demodulation,[],[f20721,f316]) ).
fof(f20889,plain,
ld(sK0,mult(sF3,sF2)) = rd(ld(sF2,rd(sF3,sF3)),sF2),
inference(forward_demodulation,[],[f20832,f1844]) ).
fof(f20928,plain,
rd(ld(sF2,rd(sF3,sF3)),sF2) = ld(sK0,rd(sF3,sF2)),
inference(forward_demodulation,[],[f20889,f316]) ).
fof(f20957,plain,
ld(sK0,sK0) = rd(ld(sF2,rd(sF3,sF3)),sF2),
inference(forward_demodulation,[],[f20928,f46]) ).
fof(f20974,plain,
rd(sK0,sK0) = rd(ld(sF2,rd(sF3,sF3)),sF2),
inference(forward_demodulation,[],[f20957,f2972]) ).
fof(f21008,plain,
! [X0] : rd(mult(X0,mult(sF2,ld(sF2,rd(sF3,sF3)))),sF2) = mult(mult(X0,sF2),rd(sK0,sK0)),
inference(superposition,[],[f53,f20974]) ).
fof(f21054,plain,
! [X0] : rd(mult(X0,mult(sF2,ld(sF2,rd(sF3,sF3)))),sF2) = rd(mult(X0,sF2),rd(sK0,sK0)),
inference(forward_demodulation,[],[f21008,f3065]) ).
fof(f21076,plain,
! [X0] : rd(mult(X0,mult(sF2,ld(sF2,rd(sF3,sF3)))),sF2) = rd(rd(X0,sF2),rd(sK0,sK0)),
inference(forward_demodulation,[],[f21054,f316]) ).
fof(f21091,plain,
! [X0] : rd(mult(X0,rd(sF3,sF3)),sF2) = rd(rd(X0,sF2),rd(sK0,sK0)),
inference(forward_demodulation,[],[f21076,f10]) ).
fof(f21103,plain,
! [X0] : rd(rd(X0,rd(sF3,sF3)),sF2) = rd(rd(X0,sF2),rd(sK0,sK0)),
inference(forward_demodulation,[],[f21091,f3065]) ).
fof(f27829,plain,
! [X0,X1] : rd(X1,mult(X1,X1)) = rd(X0,rd(mult(X1,mult(X0,X1)),X1)),
inference(superposition,[],[f18477,f13]) ).
fof(f28534,plain,
! [X2,X0,X1] : mult(X1,rd(mult(X0,mult(X2,X0)),X0)) = rd(X1,ld(X2,rd(X0,mult(X0,X0)))),
inference(superposition,[],[f1038,f27829]) ).
fof(f32260,plain,
! [X2,X3,X0,X1] : mult(mult(rd(ld(X0,X0),X0),rd(X1,X0)),mult(X3,mult(rd(ld(X0,X0),X0),rd(X1,X0)))) = ld(mult(X2,X0),mult(mult(rd(mult(X2,X1),X0),X3),mult(rd(ld(X0,X0),X0),rd(X1,X0)))),
inference(superposition,[],[f97,f921]) ).
fof(f32439,plain,
! [X2,X3,X0,X1] : mult(rd(ld(X0,X1),X0),mult(X3,rd(ld(X0,X1),X0))) = ld(mult(X2,X0),mult(mult(rd(mult(X2,X1),X0),X3),rd(ld(X0,X1),X0))),
inference(forward_demodulation,[],[f32260,f1209]) ).
fof(f32777,plain,
! [X2,X3,X0,X1] : mult(rd(ld(X0,X1),X0),mult(X3,rd(ld(X0,X1),X0))) = ld(mult(X2,X0),rd(mult(rd(mult(rd(mult(X2,X1),X0),X3),X0),X1),X0)),
inference(forward_demodulation,[],[f32439,f503]) ).
fof(f33077,plain,
! [X2,X3,X0,X1] : mult(rd(ld(X0,X1),X0),mult(X3,rd(ld(X0,X1),X0))) = rd(ld(X0,ld(X2,mult(rd(mult(rd(mult(X2,X1),X0),X3),X0),X1))),X0),
inference(forward_demodulation,[],[f32777,f1401]) ).
fof(f33281,plain,
! [X2,X3,X0,X1] : mult(rd(ld(X0,X1),X0),mult(X3,rd(ld(X0,X1),X0))) = rd(ld(X0,ld(X2,mult(X2,mult(X1,mult(rd(ld(X0,X3),X0),X1))))),X0),
inference(forward_demodulation,[],[f33077,f620]) ).
fof(f33426,plain,
! [X3,X0,X1] : mult(rd(ld(X0,X1),X0),mult(X3,rd(ld(X0,X1),X0))) = rd(ld(X0,mult(X1,mult(rd(ld(X0,X3),X0),X1))),X0),
inference(forward_demodulation,[],[f33281,f11]) ).
fof(f33535,plain,
! [X3,X0,X1] : mult(rd(ld(X0,X1),X0),rd(mult(rd(X3,X0),X1),X0)) = rd(ld(X0,mult(X1,mult(rd(ld(X0,X3),X0),X1))),X0),
inference(forward_demodulation,[],[f33426,f503]) ).
fof(f39836,plain,
! [X2,X0,X1] : mult(X2,mult(X0,X0)) = mult(rd(rd(X2,rd(ld(X0,X1),mult(X0,X1))),mult(X0,X0)),mult(mult(X0,X0),rd(X0,X0))),
inference(superposition,[],[f7072,f18487]) ).
fof(f39911,plain,
! [X2,X0,X1] : mult(X2,mult(X0,X0)) = mult(rd(rd(X2,rd(ld(X0,X1),mult(X0,X1))),mult(X0,X0)),rd(mult(X0,mult(X0,X0)),X0)),
inference(forward_demodulation,[],[f39836,f53]) ).
fof(f40050,plain,
! [X2,X0,X1] : mult(X2,mult(X0,X0)) = rd(rd(rd(X2,rd(ld(X0,X1),mult(X0,X1))),mult(X0,X0)),ld(X0,rd(X0,mult(X0,X0)))),
inference(forward_demodulation,[],[f39911,f28534]) ).
fof(f40151,plain,
! [X2,X0,X1] : mult(X2,mult(X0,X0)) = mult(rd(rd(X2,rd(ld(X0,X1),mult(X0,X1))),mult(X0,X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f40050,f1038]) ).
fof(f40231,plain,
! [X2,X0,X1] : mult(X2,mult(X0,X0)) = rd(X2,rd(ld(X0,X1),mult(X0,X1))),
inference(forward_demodulation,[],[f40151,f12]) ).
fof(f41098,plain,
! [X2,X0,X1] : mult(X1,mult(rd(X2,X0),rd(X2,X0))) = rd(X1,rd(X0,mult(rd(X2,X0),X2))),
inference(superposition,[],[f40231,f43]) ).
fof(f41169,plain,
! [X2,X0,X1] : mult(X1,mult(rd(X0,X2),rd(X0,X2))) = rd(X1,rd(ld(rd(X0,X2),X2),X0)),
inference(superposition,[],[f40231,f12]) ).
fof(f41470,plain,
! [X2,X0,X1] : rd(X1,rd(X0,mult(rd(X2,X0),X2))) = rd(X1,rd(ld(rd(X2,X0),X0),X2)),
inference(forward_demodulation,[],[f41098,f41169]) ).
fof(f59235,plain,
mult(rd(sF2,sF3),sK0) = rd(rd(sF4,sF4),sF2),
inference(superposition,[],[f357,f18931]) ).
fof(f59317,plain,
rd(rd(sF4,sF2),sF3) = mult(rd(sF2,sF3),sK0),
inference(forward_demodulation,[],[f59235,f17997]) ).
fof(f61500,plain,
! [X2,X3,X0,X1] : rd(X0,rd(ld(X1,X2),X1)) = mult(rd(mult(rd(rd(X0,mult(rd(ld(X1,X2),X1),mult(X3,rd(ld(X1,X2),X1)))),X1),X2),X1),X3),
inference(superposition,[],[f57,f503]) ).
fof(f61540,plain,
! [X2,X0,X1] : mult(rd(X0,mult(X1,mult(X2,X1))),X1) = rd(rd(X0,X1),X2),
inference(superposition,[],[f13,f57]) ).
fof(f61710,plain,
! [X2,X3,X0,X1] : rd(X0,rd(ld(X1,X2),X1)) = mult(rd(mult(rd(rd(X0,mult(rd(ld(X1,X2),X1),rd(mult(rd(X3,X1),X2),X1))),X1),X2),X1),X3),
inference(forward_demodulation,[],[f61500,f503]) ).
fof(f61867,plain,
! [X2,X3,X0,X1] : rd(X0,rd(ld(X1,X2),X1)) = mult(rd(mult(rd(rd(X0,rd(ld(X1,mult(X2,mult(rd(ld(X1,X3),X1),X2))),X1)),X1),X2),X1),X3),
inference(forward_demodulation,[],[f61710,f33535]) ).
fof(f61978,plain,
! [X2,X3,X0,X1] : rd(X0,rd(ld(X1,X2),X1)) = mult(rd(mult(rd(mult(X0,X1),mult(X1,ld(X1,mult(X2,mult(rd(ld(X1,X3),X1),X2))))),X2),X1),X3),
inference(forward_demodulation,[],[f61867,f12669]) ).
fof(f62050,plain,
! [X2,X3,X0,X1] : rd(X0,rd(ld(X1,X2),X1)) = mult(rd(mult(rd(mult(X0,X1),mult(X2,mult(rd(ld(X1,X3),X1),X2))),X2),X1),X3),
inference(forward_demodulation,[],[f61978,f10]) ).
fof(f62104,plain,
! [X2,X3,X0,X1] : rd(X0,rd(ld(X1,X2),X1)) = mult(rd(rd(rd(mult(X0,X1),X2),rd(ld(X1,X3),X1)),X1),X3),
inference(forward_demodulation,[],[f62050,f61540]) ).
fof(f62146,plain,
! [X2,X3,X0,X1] : rd(X0,rd(ld(X1,X2),X1)) = mult(rd(mult(rd(mult(X0,X1),X2),X1),mult(X1,ld(X1,X3))),X3),
inference(forward_demodulation,[],[f62104,f12669]) ).
fof(f62171,plain,
! [X2,X3,X0,X1] : rd(X0,rd(ld(X1,X2),X1)) = mult(rd(mult(rd(mult(X0,X1),X2),X1),X3),X3),
inference(forward_demodulation,[],[f62146,f10]) ).
fof(f62183,plain,
! [X2,X0,X1] : rd(X0,rd(ld(X1,X2),X1)) = mult(rd(mult(X0,X1),X2),X1),
inference(forward_demodulation,[],[f62171,f12]) ).
fof(f62459,plain,
! [X0,X1] : rd(rd(mult(X0,sF2),X1),sF2) = rd(X0,rd(ld(sF2,X1),sF2)),
inference(superposition,[],[f316,f62183]) ).
fof(f62466,plain,
! [X0,X1] : rd(rd(rd(X0,sF2),X1),sF2) = rd(X0,rd(ld(sF2,X1),sF2)),
inference(forward_demodulation,[],[f62459,f316]) ).
fof(f66226,plain,
! [X0] : rd(mult(X0,mult(rd(sF2,sF3),sK0)),sF2) = rd(mult(X0,rd(mult(rd(sF4,sF4),mult(mult(rd(sF2,sF3),sK0),sF2)),sF2)),mult(rd(sF2,sF3),sK0)),
inference(superposition,[],[f3008,f18931]) ).
fof(f66759,plain,
! [X0] : rd(mult(X0,rd(rd(sF4,sF2),sF3)),sF2) = rd(mult(X0,rd(mult(rd(sF4,sF4),mult(rd(rd(sF4,sF2),sF3),sF2)),sF2)),rd(rd(sF4,sF2),sF3)),
inference(forward_demodulation,[],[f66226,f59317]) ).
fof(f66992,plain,
! [X0] : rd(mult(X0,rd(rd(sF4,sF2),sF3)),sF2) = rd(mult(X0,rd(mult(rd(sF4,sF4),rd(rd(rd(sF4,sF2),sF3),sF2)),sF2)),rd(rd(sF4,sF2),sF3)),
inference(forward_demodulation,[],[f66759,f316]) ).
fof(f67183,plain,
! [X0] : rd(mult(X0,rd(rd(sF4,sF2),sF3)),sF2) = rd(mult(X0,rd(mult(rd(sF4,sF4),rd(sF4,rd(ld(sF2,sF3),sF2))),sF2)),rd(rd(sF4,sF2),sF3)),
inference(forward_demodulation,[],[f66992,f62466]) ).
fof(f67318,plain,
! [X0] : rd(mult(X0,rd(rd(sF4,sF2),sF3)),sF2) = rd(mult(X0,rd(mult(rd(sF4,sF4),rd(sF4,sF4)),sF2)),rd(rd(sF4,sF2),sF3)),
inference(forward_demodulation,[],[f67183,f1849]) ).
fof(f67416,plain,
! [X0] : rd(mult(X0,rd(rd(sF4,sF2),sF3)),sF2) = rd(mult(X0,rd(rd(rd(sF4,sF4),rd(sF4,sF4)),sF2)),rd(rd(sF4,sF2),sF3)),
inference(forward_demodulation,[],[f67318,f3065]) ).
fof(f67477,plain,
! [X0] : rd(mult(X0,rd(rd(sF4,sF2),sF3)),sF2) = rd(mult(X0,rd(rd(sF4,sF4),sF2)),rd(rd(sF4,sF2),sF3)),
inference(forward_demodulation,[],[f67416,f5008]) ).
fof(f67518,plain,
! [X0] : rd(mult(X0,rd(rd(sF4,sF2),sF3)),sF2) = rd(mult(X0,rd(rd(sF4,sF2),sF3)),rd(rd(sF4,sF2),sF3)),
inference(forward_demodulation,[],[f67477,f17997]) ).
fof(f67537,plain,
! [X0] : rd(mult(X0,rd(rd(sF4,sF2),sF3)),sF2) = X0,
inference(forward_demodulation,[],[f67518,f13]) ).
fof(f89647,plain,
! [X0] : mult(X0,mult(rd(rd(sF4,sF2),sF3),rd(rd(sF4,sF2),sF3))) = rd(mult(mult(X0,rd(rd(sF4,sF2),sF3)),mult(rd(rd(sF4,sF2),sF3),rd(rd(sF4,sF2),sF3))),sF2),
inference(superposition,[],[f67537,f14662]) ).
fof(f89677,plain,
! [X0] : sF2 = ld(X0,mult(X0,rd(rd(sF4,sF2),sF3))),
inference(superposition,[],[f43,f67537]) ).
fof(f89764,plain,
sF2 = rd(rd(sF4,sF2),sF3),
inference(forward_demodulation,[],[f89677,f11]) ).
fof(f89784,plain,
! [X0] : mult(X0,mult(rd(rd(sF4,sF2),sF3),rd(rd(sF4,sF2),sF3))) = rd(rd(mult(X0,rd(rd(sF4,sF2),sF3)),rd(ld(rd(rd(sF4,sF2),sF3),sF3),rd(sF4,sF2))),sF2),
inference(forward_demodulation,[],[f89647,f41169]) ).
fof(f89846,plain,
! [X0] : mult(X0,mult(rd(rd(sF4,sF2),sF3),rd(rd(sF4,sF2),sF3))) = rd(rd(mult(X0,rd(rd(sF4,sF2),sF3)),rd(sF3,mult(rd(rd(sF4,sF2),sF3),rd(sF4,sF2)))),sF2),
inference(forward_demodulation,[],[f89784,f41470]) ).
fof(f89886,plain,
! [X0] : mult(X0,mult(rd(rd(sF4,sF2),sF3),rd(rd(sF4,sF2),sF3))) = rd(rd(mult(X0,rd(rd(sF4,sF2),sF3)),rd(sF3,rd(rd(rd(sF4,sF2),sF3),ld(sF3,sF2)))),sF2),
inference(forward_demodulation,[],[f89846,f1909]) ).
fof(f89906,plain,
! [X0] : mult(X0,mult(sF2,sF2)) = rd(rd(mult(X0,sF2),rd(sF3,rd(sF2,ld(sF3,sF2)))),sF2),
inference(forward_demodulation,[],[f89886,f89764]) ).
fof(f89921,plain,
! [X0] : mult(X0,mult(sF2,sF2)) = rd(rd(mult(X0,sF2),rd(sF3,sF3)),sF2),
inference(forward_demodulation,[],[f89906,f44]) ).
fof(f89932,plain,
! [X0] : mult(X0,mult(sF2,sF2)) = rd(rd(mult(X0,sF2),sF2),rd(sK0,sK0)),
inference(forward_demodulation,[],[f89921,f21103]) ).
fof(f89941,plain,
! [X0] : mult(X0,mult(sF2,sF2)) = rd(X0,rd(sK0,sK0)),
inference(forward_demodulation,[],[f89932,f13]) ).
fof(f89950,plain,
! [X0] : mult(X0,rd(sF2,sF2)) = rd(X0,rd(sK0,sK0)),
inference(forward_demodulation,[],[f89941,f316]) ).
fof(f89956,plain,
! [X0] : rd(X0,rd(sF2,sF2)) = rd(X0,rd(sK0,sK0)),
inference(forward_demodulation,[],[f89950,f1023]) ).
fof(f89962,plain,
! [X0] : rd(X0,sF2) = rd(X0,rd(sK0,sK0)),
inference(forward_demodulation,[],[f89956,f7632]) ).
fof(f89997,plain,
sK0 = rd(sK0,sF2),
inference(superposition,[],[f3057,f89962]) ).
fof(f90057,plain,
! [X0] : ld(rd(X0,sF2),X0) = rd(sK0,sK0),
inference(superposition,[],[f43,f89962]) ).
fof(f90190,plain,
sF2 = rd(sK0,sK0),
inference(forward_demodulation,[],[f90057,f43]) ).
fof(f90247,plain,
sK0 = sF3,
inference(forward_demodulation,[],[f89997,f358]) ).
fof(f90385,plain,
spl5_2,
inference(avatar_split_clause,[],[f90247,f28]) ).
fof(f90802,plain,
! [X0] : sK0 = rd(sF2,ld(mult(X0,sK0),X0)),
inference(superposition,[],[f955,f90190]) ).
fof(f90852,plain,
sK0 = mult(sF2,sK0),
inference(forward_demodulation,[],[f90802,f1010]) ).
fof(f90892,plain,
sK0 = sF4,
inference(forward_demodulation,[],[f90852,f21]) ).
fof(f90916,plain,
( $false
| spl5_1 ),
inference(forward_subsumption_resolution,[],[f90892,f26]) ).
fof(f90917,plain,
spl5_1,
inference(avatar_contradiction_clause,[],[f90916]) ).
cnf(s1,plain,
( ~ spl5_1
| ~ spl5_2 ),
inference(sat_conversion,[],[f31]) ).
cnf(s2,plain,
spl5_2,
inference(sat_conversion,[],[f90385]) ).
cnf(s5,plain,
spl5_1,
inference(sat_conversion,[],[f90917]) ).
cnf(s6,plain,
$false,
inference(rat,[],[s1,s2,s5]) ).
fof(f90944,plain,
$false,
inference(avatar_sat_refutation,[],[s6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP655+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/6.25 % Computer : n013.cluster.edu
% 0.14/6.25 % Model : x86_64 x86_64
% 0.14/6.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/6.25 % Memory : 8046.5625MB
% 0.14/6.25 % OS : Linux 6.8.0-71-generic
% 0.14/6.25 % CPULimit : 300
% 0.14/6.25 % WCLimit : 300
% 0.14/6.25 % DateTime : Sun Sep 27 10:31:49 UTC 2026
% 0.14/6.25 % CPUTime :
% 0.14/6.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.18/6.30 Running first-order theorem proving
% 0.18/6.30 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
% 20.18/9.86 % (20129)Detected formulas, will run a generic FOF schedule.
% 20.18/9.86 % (20136)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1135173792:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 20.18/9.86 % (20140)dis-21_1_sil=8000:lcm=predicate:random_seed=2080401686:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 20.18/9.86 % (20140)Refutation not found, incomplete strategy
% 20.18/9.86 % (20140)------------------------------
% 20.18/9.86 % (20140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.18/9.86 % (20140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.18/9.86 % (20140)CaDiCaL version: 2.1.3
% 20.18/9.86 % (20140)Termination reason: Refutation not found, incomplete strategy
% 20.18/9.86 % (20140)Time elapsed: 0.002 s
% 20.18/9.86 % (20140)Peak memory usage: 88 MB
% 20.18/9.86 % (20135)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3669287795:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 20.18/9.86 % (20134)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=456931977:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 20.18/9.86 % (20137)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2071743709:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 20.18/9.86 % (20138)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1448972678:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 20.18/9.86 % (20139)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=33080268:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 20.18/9.86 % (20137)Refutation not found, incomplete strategy
% 20.18/9.86 % (20137)------------------------------
% 20.18/9.86 % (20137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.18/9.86 % (20137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.18/9.86 % (20137)CaDiCaL version: 2.1.3
% 20.18/9.86 % (20137)Termination reason: Refutation not found, incomplete strategy
% 20.18/9.86 % (20137)Time elapsed: 0.002 s
% 20.18/9.86 % (20137)Peak memory usage: 88 MB
% 20.18/9.86 % (20138)Instruction limit reached!
% 20.18/9.86 % (20138)------------------------------
% 20.18/9.86 % (20138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.18/9.86 % (20138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.18/9.86 % (20138)CaDiCaL version: 2.1.3
% 20.18/9.86 % (20138)Termination reason: Instruction limit
% 20.18/9.86 % (20138)Termination phase: Saturation
% 20.18/9.86 % (20138)Time elapsed: 0.113 s
% 20.18/9.86 % (20138)Peak memory usage: 89 MB
% 20.18/9.86 % (20138)Instructions burned: 119 (million)
% 20.18/9.86 % (20139)Instruction limit reached!
% 20.18/9.86 % (20139)------------------------------
% 20.18/9.86 % (20139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.18/9.86 % (20139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.18/9.86 % (20139)CaDiCaL version: 2.1.3
% 20.18/9.86 % (20139)Termination reason: Instruction limit
% 20.18/9.86 % (20139)Termination phase: Saturation
% 20.18/9.86 % (20139)Time elapsed: 0.135 s
% 20.18/9.86 % (20139)Peak memory usage: 89 MB
% 20.18/9.86 % (20139)Instructions burned: 140 (million)
% 20.18/9.86 % (20140)------------------------------
% 20.18/9.86 % (20140)------------------------------
% 20.18/9.86 % (20148)lrs+10_1_sil=8000:sp=occurrence:random_seed=971948161:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 20.18/9.86 % (20137)------------------------------
% 20.18/9.86 % (20137)------------------------------
% 20.18/9.86 % (20149)lrs+10_1_sil=32000:urr=on:br=off:random_seed=398472425:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 20.18/9.86 % (20136)Refutation not found, incomplete strategy
% 20.18/9.86 % (20136)------------------------------
% 20.18/9.86 % (20136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.18/9.86 % (20136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.18/9.86 % (20136)CaDiCaL version: 2.1.3
% 20.18/9.86 % (20136)Termination reason: Refutation not found, incomplete strategy
% 20.18/9.86 % (20136)Time elapsed: 0.529 s
% 30.21/11.06 % (20136)Peak memory usage: 128 MB
% 30.21/11.06 % (20136)Instructions burned: 883 (million)
% 30.21/11.06 % (20150)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3047517784:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 30.21/11.06 % (20149)Instruction limit reached!
% 30.21/11.06 % (20149)------------------------------
% 30.21/11.06 % (20149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/11.06 % (20149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/11.06 % (20149)CaDiCaL version: 2.1.3
% 30.21/11.06 % (20149)Termination reason: Instruction limit
% 30.21/11.06 % (20149)Termination phase: Saturation
% 30.21/11.06 % (20149)Time elapsed: 0.162 s
% 30.21/11.06 % (20149)Peak memory usage: 90 MB
% 30.21/11.06 % (20149)Instructions burned: 157 (million)
% 30.21/11.06 % (20148)Instruction limit reached!
% 30.21/11.06 % (20148)------------------------------
% 30.21/11.06 % (20148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/11.06 % (20148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/11.06 % (20148)CaDiCaL version: 2.1.3
% 30.21/11.06 % (20148)Termination reason: Instruction limit
% 30.21/11.06 % (20148)Termination phase: Saturation
% 30.21/11.06 % (20148)Time elapsed: 0.289 s
% 30.21/11.06 % (20148)Peak memory usage: 92 MB
% 30.21/11.06 % (20148)Instructions burned: 286 (million)
% 30.21/11.06 % (20136)------------------------------
% 30.21/11.06 % (20136)------------------------------
% 30.21/11.06 % (20152)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1511161000:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 30.21/11.06 % (20156)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1908666593:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 30.21/11.06 % (20156)Refutation not found, incomplete strategy
% 30.21/11.06 % (20156)------------------------------
% 30.21/11.06 % (20156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/11.06 % (20156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/11.06 % (20156)CaDiCaL version: 2.1.3
% 30.21/11.06 % (20156)Termination reason: Refutation not found, incomplete strategy
% 30.21/11.06 % (20156)Time elapsed: 0.002 s
% 30.21/11.06 % (20156)Peak memory usage: 88 MB
% 30.21/11.06 % (20150)Instruction limit reached!
% 30.21/11.06 % (20150)------------------------------
% 30.21/11.06 % (20150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/11.06 % (20150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/11.06 % (20150)CaDiCaL version: 2.1.3
% 30.21/11.06 % (20150)Termination reason: Instruction limit
% 30.21/11.06 % (20150)Termination phase: Saturation
% 30.21/11.06 % (20150)Time elapsed: 0.308 s
% 30.21/11.06 % (20150)Peak memory usage: 93 MB
% 30.21/11.06 % (20150)Instructions burned: 326 (million)
% 30.21/11.06 % (20159)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=485834772:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 30.21/11.06 % (20159)Refutation not found, incomplete strategy
% 30.21/11.06 % (20159)------------------------------
% 30.21/11.06 % (20159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/11.06 % (20159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/11.06 % (20159)CaDiCaL version: 2.1.3
% 30.21/11.06 % (20159)Termination reason: Refutation not found, incomplete strategy
% 30.21/11.06 % (20159)Time elapsed: 0.002 s
% 30.21/11.06 % (20159)Peak memory usage: 88 MB
% 30.21/11.06 % (20157)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2380300968:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 30.21/11.06 % (20152)Instruction limit reached!
% 30.21/11.06 % (20152)------------------------------
% 30.21/11.06 % (20152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/11.06 % (20152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/11.06 % (20152)CaDiCaL version: 2.1.3
% 30.21/11.06 % (20152)Termination reason: Instruction limit
% 30.21/11.06 % (20152)Termination phase: Saturation
% 30.21/11.06 % (20152)Time elapsed: 0.247 s
% 30.21/11.06 % (20152)Peak memory usage: 92 MB
% 30.21/11.06 % (20152)Instructions burned: 249 (million)
% 30.21/11.06 % (20162)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2661897656:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 30.21/11.06 % (20162)Refutation not found, incomplete strategy
% 50.21/14.04 % (20162)------------------------------
% 50.21/14.04 % (20162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.21/14.04 % (20162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.21/14.04 % (20162)CaDiCaL version: 2.1.3
% 50.21/14.04 % (20162)Termination reason: Refutation not found, incomplete strategy
% 50.21/14.04 % (20162)Time elapsed: 0.001 s
% 50.21/14.04 % (20162)Peak memory usage: 87 MB
% 50.21/14.04 % (20165)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3407265170:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 50.21/14.04 % (20165)Refutation not found, incomplete strategy
% 50.21/14.04 % (20165)------------------------------
% 50.21/14.04 % (20165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.21/14.04 % (20165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.21/14.04 % (20165)CaDiCaL version: 2.1.3
% 50.21/14.04 % (20165)Termination reason: Refutation not found, incomplete strategy
% 50.21/14.04 % (20165)Time elapsed: 0.002 s
% 50.21/14.04 % (20165)Peak memory usage: 88 MB
% 50.21/14.04 % (20156)------------------------------
% 50.21/14.04 % (20156)------------------------------
% 50.21/14.04 % (20159)------------------------------
% 50.21/14.04 % (20159)------------------------------
% 50.21/14.04 % (20168)lrs+10_1_sil=8000:sp=occurrence:random_seed=549503922:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 50.21/14.04 % (20162)------------------------------
% 50.21/14.04 % (20162)------------------------------
% 50.21/14.04 % (20169)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2985615236:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 50.21/14.04 % (20169)Refutation not found, incomplete strategy
% 50.21/14.04 % (20169)------------------------------
% 50.21/14.04 % (20169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.21/14.04 % (20169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.21/14.04 % (20169)CaDiCaL version: 2.1.3
% 50.21/14.04 % (20169)Termination reason: Refutation not found, incomplete strategy
% 50.21/14.04 % (20169)Time elapsed: 0.002 s
% 50.21/14.04 % (20169)Peak memory usage: 88 MB
% 50.21/14.04 % (20165)------------------------------
% 50.21/14.04 % (20165)------------------------------
% 50.21/14.04 % (20171)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=305500841:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 50.21/14.04 % (20173)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2429262253:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2981 on theBenchmark for (2981ds/134Mi)
% 50.21/14.04 % (20173)Refutation not found, incomplete strategy
% 50.21/14.04 % (20173)------------------------------
% 50.21/14.04 % (20173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.21/14.04 % (20173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.21/14.04 % (20173)CaDiCaL version: 2.1.3
% 50.21/14.04 % (20173)Termination reason: Refutation not found, incomplete strategy
% 50.21/14.04 % (20173)Time elapsed: 0.002 s
% 50.21/14.04 % (20173)Peak memory usage: 88 MB
% 50.21/14.04 % (20169)------------------------------
% 50.21/14.04 % (20169)------------------------------
% 50.21/14.04 % (20177)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2533695101:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 50.21/14.04 % (20173)------------------------------
% 50.21/14.04 % (20173)------------------------------
% 50.21/14.04 % (20168)Instruction limit reached!
% 50.21/14.04 % (20168)------------------------------
% 50.21/14.04 % (20168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.21/14.04 % (20168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.21/14.04 % (20168)CaDiCaL version: 2.1.3
% 50.21/14.04 % (20168)Termination reason: Instruction limit
% 50.21/14.04 % (20168)Termination phase: Saturation
% 50.21/14.04 % (20168)Time elapsed: 0.909 s
% 50.21/14.04 % (20168)Peak memory usage: 100 MB
% 50.21/14.04 % (20168)Instructions burned: 907 (million)
% 50.21/14.04 % (20180)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1588534178:st=3:i=13193:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/13193Mi)
% 50.21/14.04 % (20181)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2263076957:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/125Mi)
% 67.64/16.38 % (20177)Instruction limit reached!
% 67.64/16.38 % (20177)------------------------------
% 67.64/16.38 % (20177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20177)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20177)Termination reason: Instruction limit
% 67.64/16.38 % (20177)Termination phase: Saturation
% 67.64/16.38 % (20177)Time elapsed: 0.560 s
% 67.64/16.38 % (20177)Peak memory usage: 93 MB
% 67.64/16.38 % (20177)Instructions burned: 593 (million)
% 67.64/16.38 % (20181)Instruction limit reached!
% 67.64/16.38 % (20181)------------------------------
% 67.64/16.38 % (20181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20181)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20181)Termination reason: Instruction limit
% 67.64/16.38 % (20181)Termination phase: Saturation
% 67.64/16.38 % (20181)Time elapsed: 0.132 s
% 67.64/16.38 % (20181)Peak memory usage: 90 MB
% 67.64/16.38 % (20181)Instructions burned: 126 (million)
% 67.64/16.38 % (20184)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4251594963:i=134:gtgl=5:slsql=off:gtg=exists_sym_2968 on theBenchmark for (2968ds/134Mi)
% 67.64/16.38 % (20185)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3823932054:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/141Mi)
% 67.64/16.38 % (20185)Refutation not found, incomplete strategy
% 67.64/16.38 % (20185)------------------------------
% 67.64/16.38 % (20185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20185)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20185)Termination reason: Refutation not found, incomplete strategy
% 67.64/16.38 % (20185)Time elapsed: 0.002 s
% 67.64/16.38 % (20185)Peak memory usage: 88 MB
% 67.64/16.38 % (20184)Instruction limit reached!
% 67.64/16.38 % (20184)------------------------------
% 67.64/16.38 % (20184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20184)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20184)Termination reason: Instruction limit
% 67.64/16.38 % (20184)Termination phase: Saturation
% 67.64/16.38 % (20184)Time elapsed: 0.136 s
% 67.64/16.38 % (20184)Peak memory usage: 90 MB
% 67.64/16.38 % (20184)Instructions burned: 134 (million)
% 67.64/16.38 % (20157)Instruction limit reached!
% 67.64/16.38 % (20157)------------------------------
% 67.64/16.38 % (20157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20157)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20157)Termination reason: Instruction limit
% 67.64/16.38 % (20157)Termination phase: Saturation
% 67.64/16.38 % (20157)Time elapsed: 2.482 s
% 67.64/16.38 % (20157)Peak memory usage: 143 MB
% 67.64/16.38 % (20157)Instructions burned: 2350 (million)
% 67.64/16.38 % (20188)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=539963005:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2964 on theBenchmark for (2964ds/431Mi)
% 67.64/16.38 % (20188)Refutation not found, incomplete strategy
% 67.64/16.38 % (20188)------------------------------
% 67.64/16.38 % (20188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20188)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20188)Termination reason: Refutation not found, incomplete strategy
% 67.64/16.38 % (20188)Time elapsed: 0.002 s
% 67.64/16.38 % (20188)Peak memory usage: 88 MB
% 67.64/16.38 % (20185)------------------------------
% 67.64/16.38 % (20185)------------------------------
% 67.64/16.38 % (20189)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1160645521:i=6060:aac=none:ins=25_2963 on theBenchmark for (2963ds/6060Mi)
% 67.64/16.38 % (20191)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1264505583:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2961 on theBenchmark for (2961ds/150Mi)
% 67.64/16.38 % (20188)------------------------------
% 67.64/16.38 % (20188)------------------------------
% 67.64/16.38 % (20191)Instruction limit reached!
% 67.64/16.38 % (20191)------------------------------
% 67.64/16.38 % (20191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20191)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20191)Termination reason: Instruction limit
% 67.64/16.38 % (20191)Termination phase: Saturation
% 67.64/16.38 % (20191)Time elapsed: 0.154 s
% 67.64/16.38 % (20191)Peak memory usage: 91 MB
% 67.64/16.38 % (20191)Instructions burned: 150 (million)
% 67.64/16.38 % (20194)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3402689407:i=14155:bd=all_2957 on theBenchmark for (2957ds/14155Mi)
% 67.64/16.38 % (20195)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2949718602:i=667:av=off:fsr=off_2957 on theBenchmark for (2957ds/667Mi)
% 67.64/16.38 % (20195)Refutation not found, incomplete strategy
% 67.64/16.38 % (20195)------------------------------
% 67.64/16.38 % (20195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20195)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20195)Termination reason: Refutation not found, incomplete strategy
% 67.64/16.38 % (20195)Time elapsed: 0.002 s
% 67.64/16.38 % (20195)Peak memory usage: 88 MB
% 67.64/16.38 % (20195)------------------------------
% 67.64/16.38 % (20195)------------------------------
% 67.64/16.38 % (20200)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=242480421:s2a=on:i=185:s2at=1.8:fdi=4_2950 on theBenchmark for (2950ds/185Mi)
% 67.64/16.38 % (20200)Instruction limit reached!
% 67.64/16.38 % (20200)------------------------------
% 67.64/16.38 % (20200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20200)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20200)Termination reason: Instruction limit
% 67.64/16.38 % (20200)Termination phase: Saturation
% 67.64/16.38 % (20200)Time elapsed: 0.190 s
% 67.64/16.38 % (20200)Peak memory usage: 91 MB
% 67.64/16.38 % (20200)Instructions burned: 185 (million)
% 67.64/16.38 % (20202)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2625692641:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2945 on theBenchmark for (2945ds/193Mi)
% 67.64/16.38 % (20202)Instruction limit reached!
% 67.64/16.38 % (20202)------------------------------
% 67.64/16.38 % (20202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20202)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20202)Termination reason: Instruction limit
% 67.64/16.38 % (20202)Termination phase: Saturation
% 67.64/16.38 % (20202)Time elapsed: 0.191 s
% 67.64/16.38 % (20202)Peak memory usage: 92 MB
% 67.64/16.38 % (20202)Instructions burned: 194 (million)
% 67.64/16.38 % (20206)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=244250601:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2940 on theBenchmark for (2940ds/4850Mi)
% 67.64/16.38 % (20206)Refutation not found, incomplete strategy
% 67.64/16.38 % (20206)------------------------------
% 67.64/16.38 % (20206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20206)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20206)Termination reason: Refutation not found, incomplete strategy
% 67.64/16.38 % (20206)Time elapsed: 0.001 s
% 67.64/16.38 % (20206)Peak memory usage: 87 MB
% 67.64/16.38 % (20206)------------------------------
% 67.64/16.38 % (20206)------------------------------
% 67.64/16.38 % (20208)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4080395221:i=12111:sd=1:ss=included_2933 on theBenchmark for (2933ds/12111Mi)
% 67.64/16.38 % (20171)Instruction limit reached!
% 67.64/16.38 % (20171)------------------------------
% 67.64/16.38 % (20171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20171)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20171)Termination reason: Instruction limit
% 67.64/16.38 % (20171)Termination phase: Saturation
% 67.64/16.38 % (20171)Time elapsed: 5.077 s
% 67.64/16.38 % (20171)Peak memory usage: 168 MB
% 67.64/16.38 % (20171)Instructions burned: 5202 (million)
% 67.64/16.38 % (20212)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3462471225:i=319:kws=precedence:fsr=off_2927 on theBenchmark for (2927ds/319Mi)
% 67.64/16.38 % (20212)Instruction limit reached!
% 67.64/16.38 % (20212)------------------------------
% 67.64/16.38 % (20212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.64/16.38 % (20212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.64/16.38 % (20212)CaDiCaL version: 2.1.3
% 67.64/16.38 % (20212)Termination reason: Instruction limit
% 67.64/16.38 % (20212)Termination phase: Saturation
% 67.64/16.38 % (20212)Time elapsed: 0.312 s
% 67.64/16.38 % (20212)Peak memory usage: 94 MB
% 67.64/16.38 % (20212)Instructions burned: 319 (million)
% 67.64/16.38 % (20215)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2274563144:i=2064:ep=RST_2921 on theBenchmark for (2921ds/2064Mi)
% 67.64/16.38 % (20134)First to succeed.
% 67.64/16.38 % (20134)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-20129"
% 67.64/16.38 % (20134)Refutation found. Thanks to Tanya!
% 67.64/16.38 % SZS status Theorem for theBenchmark
% 67.64/16.38 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/16.61 % (20134)------------------------------
% 0.21/16.61 % (20134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.21/16.61 % (20134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/16.61 % (20134)CaDiCaL version: 2.1.3
% 0.21/16.61 % (20134)Termination reason: Refutation
% 0.21/16.61 % (20134)Time elapsed: 8.793 s
% 0.21/16.61 % (20134)Peak memory usage: 201 MB
% 0.21/16.61 % (20134)Instructions burned: 8331 (million)
% 0.21/16.61 % (20134)------------------------------
% 0.21/16.61 % (20134)------------------------------
% 0.21/16.61 % (20129)Success in time 9.528 s
% 0.21/16.61 % Vampire exiting
%------------------------------------------------------------------------------