%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP746+1 : 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 : n026.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:16:05 AM UTC 2026
% Result : Theorem 120.04s 22.87s
% Output : Refutation 120.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 19
% Syntax : Number of formulae : 313 ( 195 unt; 10 def)
% Number of atoms : 457 ( 333 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 234 ( 90 ~; 132 |; 2 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 11 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 481 ( 0 sgn 481 !; 0 ?)
% 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] : mult(X0,unit) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f05) ).
fof(f6,axiom,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f06) ).
fof(f7,axiom,
! [X0,X1,X2] : mult(mult(mult(X2,X1),X0),X1) = mult(X2,mult(mult(X1,X0),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f07) ).
fof(f8,axiom,
! [X0,X1,X2] :
( ( mult(mult(X0,X1),X2) = mult(X0,mult(X1,X2))
& mult(mult(X0,X2),X1) = mult(X0,mult(X2,X1)) )
| ( mult(mult(X0,X1),X2) = mult(mult(X0,X2),X1)
& mult(X0,mult(X1,X2)) = mult(X0,mult(X2,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f08) ).
fof(f9,conjecture,
mult(mult(a,b),c) = mult(a,mult(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f10,negated_conjecture,
mult(mult(a,b),c) != mult(a,mult(b,c)),
inference(negated_conjecture,[status(cth)],[f9]) ).
fof(f11,plain,
mult(mult(a,b),c) != mult(a,mult(b,c)),
inference(flattening,[],[f10]) ).
fof(f12,plain,
! [X0,X1] : mult(X1,ld(X1,X0)) = X0,
inference(cnf_transformation,[],[f1]) ).
fof(f13,plain,
! [X0,X1] : ld(X1,mult(X1,X0)) = X0,
inference(cnf_transformation,[],[f2]) ).
fof(f14,plain,
! [X0,X1] : mult(rd(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f3]) ).
fof(f15,plain,
! [X0,X1] : rd(mult(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f4]) ).
fof(f16,plain,
! [X0] : mult(X0,unit) = X0,
inference(cnf_transformation,[],[f5]) ).
fof(f17,plain,
! [X0] : mult(unit,X0) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f18,plain,
! [X2,X0,X1] : mult(mult(mult(X2,X1),X0),X1) = mult(X2,mult(mult(X1,X0),X1)),
inference(cnf_transformation,[],[f7]) ).
fof(f19,plain,
! [X2,X0,X1] :
( mult(mult(X0,X2),X1) = mult(X0,mult(X2,X1))
| mult(X0,mult(X1,X2)) = mult(X0,mult(X2,X1)) ),
inference(cnf_transformation,[],[f8]) ).
fof(f20,plain,
! [X2,X0,X1] :
( mult(mult(X0,X1),X2) = mult(mult(X0,X2),X1)
| mult(mult(X0,X2),X1) = mult(X0,mult(X2,X1)) ),
inference(cnf_transformation,[],[f8]) ).
fof(f23,plain,
mult(mult(a,b),c) != mult(a,mult(b,c)),
inference(cnf_transformation,[],[f11]) ).
fof(f40,plain,
! [X2,X0,X1] :
( mult(X0,mult(mult(X2,X1),X2)) = mult(mult(mult(X0,X1),X2),X2)
| mult(mult(X0,X2),X1) = mult(X0,mult(X2,X1)) ),
inference(superposition,[],[f18,f20]) ).
fof(f55,plain,
( mult(a,mult(b,c)) != mult(a,mult(b,c))
| mult(a,mult(b,c)) = mult(a,mult(c,b)) ),
inference(superposition,[],[f23,f19]) ).
fof(f62,plain,
mult(a,mult(b,c)) = mult(a,mult(c,b)),
inference(trivial_inequality_removal,[],[f55]) ).
fof(f151,plain,
! [X2,X0,X1] : mult(X1,mult(mult(ld(X1,X0),X2),ld(X1,X0))) = mult(mult(X0,X2),ld(X1,X0)),
inference(superposition,[],[f18,f12]) ).
fof(f153,plain,
! [X2,X0,X1] : mult(X0,X2) = mult(X1,mult(mult(X2,ld(mult(X1,X2),X0)),X2)),
inference(superposition,[],[f18,f12]) ).
fof(f156,plain,
! [X0] : ld(unit,X0) = X0,
inference(superposition,[],[f17,f12]) ).
fof(f166,plain,
mult(c,b) = ld(a,mult(a,mult(b,c))),
inference(superposition,[],[f13,f62]) ).
fof(f167,plain,
mult(b,c) = mult(c,b),
inference(forward_demodulation,[],[f166,f13]) ).
fof(f214,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f13,f14]) ).
fof(f215,plain,
! [X2,X0,X1] : mult(mult(X0,X2),X1) = mult(rd(X0,X1),mult(mult(X1,X2),X1)),
inference(superposition,[],[f18,f14]) ).
fof(f216,plain,
! [X2,X0,X1] :
( mult(rd(X0,X1),mult(X1,X2)) = mult(rd(X0,X1),mult(X2,X1))
| mult(X0,X2) = mult(rd(X0,X1),mult(X1,X2)) ),
inference(superposition,[],[f19,f14]) ).
fof(f222,plain,
! [X2,X0,X1] : mult(mult(X1,ld(X2,X0)),X2) = mult(rd(X1,X2),mult(X0,X2)),
inference(superposition,[],[f215,f12]) ).
fof(f240,plain,
! [X2,X0,X1] : mult(mult(X2,X1),X2) = ld(rd(X0,X2),mult(mult(X0,X1),X2)),
inference(superposition,[],[f13,f215]) ).
fof(f275,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = mult(X0,mult(mult(X1,unit),X1)),
inference(superposition,[],[f18,f16]) ).
fof(f281,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = mult(X0,mult(X1,X1)),
inference(forward_demodulation,[],[f275,f16]) ).
fof(f378,plain,
! [X2,X0,X1] : mult(mult(X1,ld(X2,X0)),X1) = ld(rd(X2,X1),mult(X0,X1)),
inference(superposition,[],[f240,f12]) ).
fof(f388,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X1) = ld(rd(rd(X0,X2),X1),mult(X0,X1)),
inference(superposition,[],[f240,f14]) ).
fof(f390,plain,
! [X0,X1] : mult(mult(X1,X0),X1) = ld(rd(unit,X1),mult(X0,X1)),
inference(superposition,[],[f240,f17]) ).
fof(f637,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X1) = ld(rd(rd(rd(X0,X1),X2),X1),X0),
inference(superposition,[],[f388,f14]) ).
fof(f652,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f15,f12]) ).
fof(f655,plain,
! [X2,X0,X1] : mult(mult(X0,X1),X2) = rd(mult(X0,mult(mult(X1,X2),X1)),X1),
inference(superposition,[],[f15,f18]) ).
fof(f664,plain,
! [X2,X0,X1] : rd(X0,X2) = rd(mult(mult(X0,X1),X2),mult(mult(X2,X1),X2)),
inference(superposition,[],[f15,f215]) ).
fof(f665,plain,
! [X0] : unit = rd(X0,X0),
inference(superposition,[],[f15,f17]) ).
fof(f676,plain,
! [X2,X0,X1] : mult(mult(X1,X2),ld(X2,X0)) = rd(mult(X1,mult(X0,X2)),X2),
inference(superposition,[],[f655,f12]) ).
fof(f943,plain,
! [X2,X0,X1] : mult(mult(X1,ld(X2,X0)),ld(ld(X2,X0),X2)) = rd(mult(X1,X0),ld(X2,X0)),
inference(superposition,[],[f676,f12]) ).
fof(f957,plain,
! [X2,X0,X1] : mult(mult(X1,X2),ld(X2,rd(X0,X2))) = rd(mult(X1,X0),X2),
inference(superposition,[],[f676,f14]) ).
fof(f959,plain,
! [X0,X1] : rd(mult(X1,X0),X0) = mult(mult(X1,X0),ld(X0,unit)),
inference(superposition,[],[f676,f17]) ).
fof(f990,plain,
! [X0,X1] : mult(mult(X1,X0),ld(X0,unit)) = X1,
inference(forward_demodulation,[],[f959,f15]) ).
fof(f1017,plain,
! [X0,X1] : rd(X0,X1) = mult(X0,ld(X1,unit)),
inference(superposition,[],[f990,f14]) ).
fof(f1043,plain,
! [X0,X1] : ld(X1,unit) = ld(mult(X0,X1),X0),
inference(superposition,[],[f13,f990]) ).
fof(f1044,plain,
! [X0,X1] : mult(X0,X1) = rd(X0,ld(X1,unit)),
inference(superposition,[],[f15,f990]) ).
fof(f1153,plain,
! [X2,X0,X1] : mult(X0,mult(mult(X1,ld(X2,unit)),X1)) = mult(rd(mult(X0,X1),X2),X1),
inference(superposition,[],[f18,f1017]) ).
fof(f1159,plain,
! [X0] : rd(unit,X0) = ld(X0,unit),
inference(superposition,[],[f17,f1017]) ).
fof(f1165,plain,
! [X2,X0,X1] : mult(rd(mult(X0,X1),X2),X1) = mult(X0,mult(rd(X1,X2),X1)),
inference(forward_demodulation,[],[f1153,f1017]) ).
fof(f1831,plain,
! [X2,X0,X1] :
( mult(X2,X1) = ld(rd(X0,X1),mult(rd(X0,X1),mult(X1,X2)))
| mult(X0,X2) = mult(rd(X0,X1),mult(X1,X2)) ),
inference(superposition,[],[f13,f216]) ).
fof(f1860,plain,
! [X2,X0,X1] :
( mult(X0,X2) = mult(rd(X0,X1),mult(X1,X2))
| mult(X2,X1) = mult(X1,X2) ),
inference(forward_demodulation,[],[f1831,f13]) ).
fof(f1918,plain,
! [X2,X0,X1] : rd(rd(X0,X1),X2) = rd(mult(X0,X2),mult(mult(X2,X1),X2)),
inference(superposition,[],[f664,f14]) ).
fof(f2098,plain,
! [X2,X0,X1] : rd(rd(X1,ld(X2,X0)),X2) = rd(mult(X1,X2),mult(X0,X2)),
inference(superposition,[],[f1918,f12]) ).
fof(f2192,plain,
! [X2,X0,X1] :
( mult(mult(X0,X1),X2) = mult(X0,mult(X1,X2))
| mult(X2,X1) = mult(X1,X2) ),
inference(superposition,[],[f1860,f15]) ).
fof(f2200,plain,
! [X2,X0,X1] :
( mult(X1,ld(X2,X0)) = mult(rd(X1,X2),X0)
| mult(ld(X2,X0),X2) = X0 ),
inference(superposition,[],[f1860,f12]) ).
fof(f2355,plain,
! [X2,X0,X1] :
( mult(X0,X1) = rd(mult(X0,mult(X1,X2)),X2)
| mult(X2,X1) = mult(X1,X2) ),
inference(superposition,[],[f15,f2192]) ).
fof(f2401,plain,
! [X2,X0,X1] :
( mult(X0,X1) = mult(mult(X0,X2),ld(X2,X1))
| mult(X2,X1) = mult(X1,X2) ),
inference(forward_demodulation,[],[f2355,f676]) ).
fof(f2469,plain,
! [X0,X1] : ld(X0,X1) = ld(ld(X1,X0),unit),
inference(superposition,[],[f1043,f12]) ).
fof(f2517,plain,
! [X2,X0,X1] :
( mult(X0,X2) = mult(mult(X0,X1),ld(X1,X2))
| mult(ld(X1,X2),X1) = X2 ),
inference(superposition,[],[f2200,f15]) ).
fof(f2972,plain,
! [X2,X0,X1] : mult(mult(X1,ld(mult(X0,X1),X2)),X1) = ld(X0,mult(X2,X1)),
inference(superposition,[],[f378,f15]) ).
fof(f3009,plain,
! [X0,X1] : mult(mult(X0,ld(X1,unit)),X0) = ld(rd(X1,X0),X0),
inference(superposition,[],[f378,f17]) ).
fof(f3029,plain,
! [X0,X1] : mult(rd(X0,X1),X0) = ld(rd(X1,X0),X0),
inference(forward_demodulation,[],[f3009,f1017]) ).
fof(f3052,plain,
! [X0,X1] : ld(X0,X1) = mult(rd(X1,mult(X0,X1)),X1),
inference(superposition,[],[f3029,f15]) ).
fof(f3275,plain,
! [X2,X3,X0,X1] : mult(mult(X3,ld(mult(X0,X2),X1)),X2) = mult(rd(X3,X2),ld(X0,mult(X1,X2))),
inference(superposition,[],[f215,f2972]) ).
fof(f3285,plain,
! [X2,X0,X1] : rd(ld(X0,mult(X1,X2)),X2) = mult(X2,ld(mult(X0,X2),X1)),
inference(superposition,[],[f15,f2972]) ).
fof(f4318,plain,
! [X2,X0,X1] :
( mult(mult(X0,X1),X2) = mult(X0,mult(mult(X2,ld(X2,X1)),X2))
| mult(ld(X2,X1),X2) = X1 ),
inference(superposition,[],[f18,f2517]) ).
fof(f4377,plain,
! [X2,X0,X1] :
( mult(mult(X0,X1),X2) = mult(X0,mult(rd(X2,X2),mult(X1,X2)))
| mult(ld(X2,X1),X2) = X1 ),
inference(forward_demodulation,[],[f4318,f222]) ).
fof(f4399,plain,
! [X2,X0,X1] :
( mult(mult(X0,X1),X2) = mult(X0,mult(unit,mult(X1,X2)))
| mult(ld(X2,X1),X2) = X1 ),
inference(forward_demodulation,[],[f4377,f665]) ).
fof(f4412,plain,
! [X2,X0,X1] :
( mult(mult(X0,X1),X2) = mult(X0,mult(X1,X2))
| mult(ld(X2,X1),X2) = X1 ),
inference(forward_demodulation,[],[f4399,f17]) ).
fof(f4527,plain,
( mult(a,mult(b,c)) != mult(a,mult(b,c))
| b = mult(ld(c,b),c) ),
inference(superposition,[],[f23,f4412]) ).
fof(f4631,plain,
b = mult(ld(c,b),c),
inference(trivial_inequality_removal,[],[f4527]) ).
fof(f4686,plain,
c = ld(ld(c,b),b),
inference(superposition,[],[f13,f4631]) ).
fof(f4687,plain,
ld(c,b) = rd(b,c),
inference(superposition,[],[f15,f4631]) ).
fof(f4719,plain,
ld(c,unit) = ld(b,ld(c,b)),
inference(superposition,[],[f1043,f4631]) ).
fof(f4883,plain,
! [X2,X0,X1] : rd(X0,ld(X1,X2)) = mult(rd(mult(X0,X1),mult(X2,X1)),X1),
inference(superposition,[],[f14,f2098]) ).
fof(f4898,plain,
! [X2,X0,X1] : rd(X0,ld(X1,X2)) = mult(X0,mult(rd(X1,mult(X2,X1)),X1)),
inference(forward_demodulation,[],[f4883,f1165]) ).
fof(f4911,plain,
! [X2,X0,X1] : rd(X0,ld(X1,X2)) = mult(X0,ld(X2,X1)),
inference(forward_demodulation,[],[f4898,f3052]) ).
fof(f4947,plain,
! [X0,X1] : unit = mult(ld(X0,X1),ld(X1,X0)),
inference(superposition,[],[f665,f4911]) ).
fof(f4968,plain,
! [X2,X3,X0,X1] : rd(mult(X0,ld(X1,X2)),mult(X3,ld(X1,X2))) = mult(rd(X0,ld(ld(X1,X2),X3)),ld(X2,X1)),
inference(superposition,[],[f2098,f4911]) ).
fof(f4971,plain,
! [X2,X3,X0,X1] : rd(mult(X0,ld(X1,X2)),mult(X3,ld(X1,X2))) = mult(mult(X0,ld(X3,ld(X1,X2))),ld(X2,X1)),
inference(forward_demodulation,[],[f4968,f4911]) ).
fof(f5143,plain,
! [X0,X1] : unit = mult(ld(mult(X1,X0),X1),X0),
inference(superposition,[],[f4947,f13]) ).
fof(f5151,plain,
unit = mult(ld(b,ld(c,b)),c),
inference(superposition,[],[f4947,f4686]) ).
fof(f5240,plain,
unit = mult(ld(c,unit),c),
inference(forward_demodulation,[],[f5151,f4719]) ).
fof(f5243,plain,
! [X0] : unit = mult(ld(X0,unit),X0),
inference(forward_demodulation,[],[f5143,f1043]) ).
fof(f5331,plain,
! [X0] : ld(ld(c,unit),mult(X0,c)) = mult(mult(c,ld(unit,X0)),c),
inference(superposition,[],[f2972,f5240]) ).
fof(f5336,plain,
! [X0] : mult(mult(c,X0),c) = ld(ld(c,unit),mult(X0,c)),
inference(forward_demodulation,[],[f5331,f156]) ).
fof(f5540,plain,
mult(mult(c,ld(c,b)),c) = ld(ld(c,unit),b),
inference(superposition,[],[f5336,f4631]) ).
fof(f5593,plain,
mult(rd(c,c),mult(b,c)) = ld(ld(c,unit),b),
inference(forward_demodulation,[],[f5540,f222]) ).
fof(f5605,plain,
mult(unit,mult(b,c)) = ld(ld(c,unit),b),
inference(forward_demodulation,[],[f5593,f665]) ).
fof(f5613,plain,
mult(b,c) = ld(ld(c,unit),b),
inference(forward_demodulation,[],[f5605,f17]) ).
fof(f8385,plain,
! [X0,X1] : mult(mult(ld(X1,X0),X1),ld(X1,X0)) = ld(rd(unit,ld(X1,X0)),X0),
inference(superposition,[],[f390,f12]) ).
fof(f8532,plain,
! [X0,X1] : mult(mult(ld(X1,X0),X1),ld(X1,X0)) = ld(mult(unit,ld(X0,X1)),X0),
inference(forward_demodulation,[],[f8385,f4911]) ).
fof(f8573,plain,
! [X0,X1] : mult(mult(ld(X1,X0),X1),ld(X1,X0)) = ld(ld(X0,X1),X0),
inference(forward_demodulation,[],[f8532,f17]) ).
fof(f10846,plain,
! [X2,X3,X0,X1] : mult(ld(X0,X1),ld(mult(X2,ld(X0,X1)),X3)) = mult(ld(X2,mult(X3,ld(X0,X1))),ld(X1,X0)),
inference(superposition,[],[f4911,f3285]) ).
fof(f15052,definition,
( spl0_75
<=> mult(a,mult(b,c)) = mult(mult(b,c),a) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f15053,plain,
( mult(a,mult(b,c)) = mult(mult(b,c),a)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f15052]) ).
fof(f15138,plain,
! [X0,X1] : mult(ld(X0,X1),X0) = mult(rd(unit,X0),mult(X1,X0)),
inference(superposition,[],[f222,f17]) ).
fof(f15323,plain,
! [X0,X1] : mult(ld(X0,X1),X0) = mult(ld(X0,unit),mult(X1,X0)),
inference(forward_demodulation,[],[f15138,f1159]) ).
fof(f15473,plain,
! [X2,X0,X1] : mult(ld(ld(X1,X0),X2),ld(X1,X0)) = mult(ld(X0,X1),mult(X2,ld(X1,X0))),
inference(superposition,[],[f15323,f2469]) ).
fof(f15619,plain,
! [X2,X0,X1] : rd(rd(X2,mult(X1,X0)),ld(X0,unit)) = rd(mult(X2,ld(X0,unit)),mult(mult(ld(X0,X1),X0),ld(X0,unit))),
inference(superposition,[],[f1918,f15323]) ).
fof(f15633,plain,
! [X2,X0,X1] : rd(rd(X2,mult(X1,X0)),ld(X0,unit)) = mult(mult(X2,ld(mult(ld(X0,X1),X0),ld(X0,unit))),ld(unit,X0)),
inference(forward_demodulation,[],[f15619,f4971]) ).
fof(f15725,plain,
! [X2,X0,X1] : rd(rd(X2,mult(X1,X0)),ld(X0,unit)) = mult(mult(X2,ld(mult(ld(X0,X1),X0),ld(X0,unit))),X0),
inference(forward_demodulation,[],[f15633,f156]) ).
fof(f15793,plain,
! [X2,X0,X1] : rd(rd(X2,mult(X1,X0)),ld(X0,unit)) = mult(rd(X2,X0),ld(ld(X0,X1),mult(ld(X0,unit),X0))),
inference(forward_demodulation,[],[f15725,f3275]) ).
fof(f15836,plain,
! [X2,X0,X1] : rd(rd(X2,mult(X1,X0)),ld(X0,unit)) = mult(rd(X2,X0),ld(ld(X0,X1),unit)),
inference(forward_demodulation,[],[f15793,f5243]) ).
fof(f15859,plain,
! [X2,X0,X1] : rd(rd(X2,X0),ld(X0,X1)) = rd(rd(X2,mult(X1,X0)),ld(X0,unit)),
inference(forward_demodulation,[],[f15836,f1017]) ).
fof(f15871,plain,
! [X2,X0,X1] : rd(rd(X2,X0),ld(X0,X1)) = mult(rd(X2,mult(X1,X0)),X0),
inference(forward_demodulation,[],[f15859,f1044]) ).
fof(f15878,plain,
! [X2,X0,X1] : mult(rd(X2,mult(X1,X0)),X0) = mult(rd(X2,X0),ld(X1,X0)),
inference(forward_demodulation,[],[f15871,f4911]) ).
fof(f16582,definition,
( spl0_81
<=> mult(a,mult(mult(b,c),a)) = mult(a,mult(a,mult(b,c))) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f16583,plain,
( mult(a,mult(mult(b,c),a)) = mult(a,mult(a,mult(b,c)))
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f16582]) ).
fof(f16613,plain,
( mult(mult(b,c),a) = ld(a,mult(a,mult(a,mult(b,c))))
| ~ spl0_81 ),
inference(superposition,[],[f13,f16583]) ).
fof(f16684,plain,
( mult(a,mult(b,c)) = mult(mult(b,c),a)
| ~ spl0_81 ),
inference(forward_demodulation,[],[f16613,f13]) ).
fof(f16706,definition,
( spl0_87
<=> mult(a,c) = mult(c,a) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f16707,plain,
( mult(a,c) = mult(c,a)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f16706]) ).
fof(f16714,definition,
( spl0_89
<=> mult(a,b) = mult(b,a) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f16715,plain,
( mult(a,b) = mult(b,a)
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f16714]) ).
fof(f16735,plain,
( spl0_75
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f16684,f16582,f15052]) ).
fof(f23954,plain,
! [X2,X0,X1] :
( mult(X1,mult(X2,X0)) = mult(mult(X1,X2),X0)
| mult(mult(X2,X0),X2) = mult(X2,mult(X2,X0)) ),
inference(superposition,[],[f2401,f13]) ).
fof(f25217,plain,
! [X2,X0,X1] :
( mult(X0,mult(X1,X0)) = mult(X0,mult(X0,X1))
| mult(X0,mult(X1,X0)) = mult(X0,mult(X0,X1))
| mult(mult(X2,X0),X1) = mult(X2,mult(X0,X1)) ),
inference(superposition,[],[f19,f23954]) ).
fof(f25218,plain,
! [X2,X0,X1] :
( mult(mult(X0,X0),X1) = mult(X0,mult(X0,X1))
| mult(mult(X0,X0),X1) = mult(X0,mult(X0,X1))
| mult(mult(X2,X0),X1) = mult(X2,mult(X0,X1)) ),
inference(superposition,[],[f20,f23954]) ).
fof(f25331,plain,
! [X2,X0,X1] :
( mult(mult(X0,X0),X1) = mult(X0,mult(X0,X1))
| mult(mult(X2,X0),X1) = mult(X2,mult(X0,X1)) ),
inference(duplicate_literal_removal,[],[f25218]) ).
fof(f25332,plain,
! [X2,X0,X1] :
( mult(X0,mult(X1,X0)) = mult(X0,mult(X0,X1))
| mult(mult(X2,X0),X1) = mult(X2,mult(X0,X1)) ),
inference(duplicate_literal_removal,[],[f25217]) ).
fof(f26418,plain,
( mult(a,mult(b,c)) = mult(mult(b,a),c)
| mult(mult(b,c),a) = mult(b,mult(c,a))
| ~ spl0_75 ),
inference(superposition,[],[f15053,f20]) ).
fof(f26524,definition,
( spl0_158
<=> mult(a,mult(b,c)) = mult(b,mult(c,a)) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f26525,plain,
( mult(a,mult(b,c)) = mult(b,mult(c,a))
| ~ spl0_158 ),
inference(avatar_component_clause,[],[f26524]) ).
fof(f26543,definition,
( spl0_161
<=> mult(a,mult(b,c)) = mult(mult(b,a),c) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f26544,plain,
( mult(a,mult(b,c)) = mult(mult(b,a),c)
| ~ spl0_161 ),
inference(avatar_component_clause,[],[f26543]) ).
fof(f26558,plain,
( mult(a,mult(b,c)) = mult(b,mult(c,a))
| mult(a,mult(b,c)) = mult(mult(b,a),c)
| ~ spl0_75 ),
inference(forward_demodulation,[],[f26418,f15053]) ).
fof(f26580,plain,
( spl0_161
| spl0_158
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f26558,f15052,f26524,f26543]) ).
fof(f27002,plain,
! [X2,X0,X1] :
( mult(X0,X2) = mult(rd(X0,X1),mult(X1,X2))
| mult(X1,mult(X1,X2)) = mult(X1,mult(X2,X1)) ),
inference(superposition,[],[f25332,f14]) ).
fof(f28851,plain,
! [X0,X1] :
( mult(X0,mult(X0,X1)) != mult(X0,mult(X0,X1))
| mult(mult(X0,X0),X1) = mult(X0,mult(X0,X1)) ),
inference(equality_factoring,[],[f25331]) ).
fof(f28852,plain,
! [X0,X1] : mult(mult(X0,X0),X1) = mult(X0,mult(X0,X1)),
inference(trivial_inequality_removal,[],[f28851]) ).
fof(f29183,plain,
! [X0,X1] : mult(mult(X0,mult(X0,X1)),X0) = mult(X0,mult(mult(X0,X1),X0)),
inference(superposition,[],[f18,f28852]) ).
fof(f29197,plain,
! [X0,X1] : rd(mult(X0,X1),X0) = mult(X0,mult(X0,ld(X0,rd(X1,X0)))),
inference(superposition,[],[f957,f28852]) ).
fof(f29225,plain,
! [X0,X1] : mult(X0,X0) = rd(mult(X0,mult(X0,X1)),X1),
inference(superposition,[],[f15,f28852]) ).
fof(f29294,plain,
! [X0,X1] : mult(X0,mult(X0,ld(X1,unit))) = rd(mult(X0,X0),X1),
inference(superposition,[],[f1017,f28852]) ).
fof(f29333,plain,
! [X0,X1] : mult(X0,rd(X0,X1)) = rd(mult(X0,X0),X1),
inference(forward_demodulation,[],[f29294,f1017]) ).
fof(f29375,plain,
! [X0,X1] : mult(X0,X0) = mult(mult(X0,X1),ld(X1,X0)),
inference(forward_demodulation,[],[f29225,f676]) ).
fof(f29397,plain,
! [X0,X1] : mult(X0,rd(X1,X0)) = rd(mult(X0,X1),X0),
inference(forward_demodulation,[],[f29197,f12]) ).
fof(f29572,plain,
! [X0,X1] : mult(X1,X1) = mult(X0,ld(ld(X1,X0),X1)),
inference(superposition,[],[f29375,f12]) ).
fof(f31686,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,rd(X1,X0)),X0),
inference(superposition,[],[f14,f29397]) ).
fof(f31696,plain,
! [X2,X0,X1] : rd(mult(X2,mult(X0,X1)),X0) = mult(mult(X2,X0),ld(X0,mult(X0,rd(X1,X0)))),
inference(superposition,[],[f957,f29397]) ).
fof(f31718,plain,
! [X2,X0,X1] : mult(mult(X2,X0),rd(X1,X0)) = rd(mult(X2,mult(X0,X1)),X0),
inference(forward_demodulation,[],[f31696,f13]) ).
fof(f32501,plain,
! [X0,X1] : mult(mult(X1,X0),X1) = mult(X1,mult(X0,X1)),
inference(superposition,[],[f29183,f12]) ).
fof(f32507,plain,
! [X2,X0,X1] : mult(mult(X2,mult(X0,X1)),X2) = mult(X2,mult(mult(X0,X1),X2)),
inference(superposition,[],[f29183,f153]) ).
fof(f33253,plain,
! [X0,X1] : mult(X0,X1) = mult(X1,mult(ld(X1,X0),X1)),
inference(superposition,[],[f32501,f12]) ).
fof(f33268,plain,
! [X0,X1] : mult(mult(ld(X0,X1),X0),ld(X0,unit)) = mult(ld(X0,unit),mult(mult(X1,X0),ld(X0,unit))),
inference(superposition,[],[f32501,f15323]) ).
fof(f33435,plain,
! [X0,X1] : ld(ld(X1,X0),X1) = mult(ld(X0,X1),mult(X0,ld(X0,X1))),
inference(superposition,[],[f8573,f32501]) ).
fof(f33499,plain,
! [X0,X1] : ld(X0,unit) = ld(mult(X0,mult(X1,X0)),mult(X0,X1)),
inference(superposition,[],[f1043,f32501]) ).
fof(f33609,plain,
! [X0,X1] : ld(ld(X1,X0),X1) = mult(ld(X0,X1),X1),
inference(forward_demodulation,[],[f33435,f12]) ).
fof(f33718,plain,
! [X0,X1] : mult(ld(X0,unit),X1) = mult(mult(ld(X0,X1),X0),ld(X0,unit)),
inference(forward_demodulation,[],[f33268,f990]) ).
fof(f33834,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(X0,unit),X1),
inference(forward_demodulation,[],[f33718,f990]) ).
fof(f34023,plain,
! [X0,X1] : ld(X1,mult(X0,X1)) = mult(ld(X1,X0),X1),
inference(superposition,[],[f13,f33253]) ).
fof(f35125,plain,
! [X0,X1] : ld(ld(X1,unit),X0) = mult(ld(ld(X1,unit),mult(X0,X1)),ld(X1,unit)),
inference(superposition,[],[f34023,f990]) ).
fof(f35153,plain,
! [X0,X1] : ld(X1,X0) = mult(ld(X1,rd(X0,X1)),X1),
inference(superposition,[],[f34023,f14]) ).
fof(f35266,plain,
! [X0,X1] : ld(ld(X1,unit),X0) = mult(ld(unit,X1),mult(mult(X0,X1),ld(X1,unit))),
inference(forward_demodulation,[],[f35125,f15473]) ).
fof(f35347,plain,
! [X0,X1] : ld(ld(X1,unit),X0) = mult(ld(unit,X1),X0),
inference(forward_demodulation,[],[f35266,f990]) ).
fof(f35390,plain,
! [X0,X1] : mult(X1,X0) = ld(ld(X1,unit),X0),
inference(forward_demodulation,[],[f35347,f156]) ).
fof(f35914,plain,
! [X0,X1] : mult(X1,X1) = mult(X0,mult(ld(X0,X1),X1)),
inference(superposition,[],[f29572,f33609]) ).
fof(f36067,plain,
! [X2,X0,X1] : ld(ld(X2,X1),X0) = mult(ld(ld(X2,X1),mult(X0,ld(X1,X2))),ld(X2,X1)),
inference(superposition,[],[f35153,f4911]) ).
fof(f36296,plain,
! [X2,X0,X1] : ld(ld(X2,X1),X0) = mult(ld(X1,X2),ld(mult(ld(X2,X1),ld(X1,X2)),X0)),
inference(forward_demodulation,[],[f36067,f10846]) ).
fof(f36354,plain,
! [X2,X0,X1] : ld(ld(X2,X1),X0) = mult(ld(X1,X2),ld(unit,X0)),
inference(forward_demodulation,[],[f36296,f4947]) ).
fof(f36389,plain,
! [X2,X0,X1] : ld(ld(X2,X1),X0) = mult(ld(X1,X2),X0),
inference(forward_demodulation,[],[f36354,f156]) ).
fof(f37613,plain,
! [X2,X0,X1] : mult(mult(X2,rd(X1,X0)),X0) = mult(rd(X2,X0),mult(X0,X1)),
inference(superposition,[],[f215,f31686]) ).
fof(f38034,plain,
! [X0,X1] : mult(X1,X1) = mult(rd(X1,X0),mult(X0,X1)),
inference(superposition,[],[f35914,f214]) ).
fof(f38040,plain,
! [X0,X1] : mult(mult(X1,X0),mult(X1,X0)) = mult(X1,mult(X0,mult(X1,X0))),
inference(superposition,[],[f35914,f13]) ).
fof(f41686,plain,
! [X0,X1] : rd(X0,X1) = rd(mult(X0,X0),mult(X1,X0)),
inference(superposition,[],[f15,f38034]) ).
fof(f41836,plain,
! [X0,X1] : rd(X0,X1) = mult(X0,rd(X0,mult(X1,X0))),
inference(forward_demodulation,[],[f41686,f29333]) ).
fof(f42331,plain,
! [X0,X1] : rd(X1,rd(X0,X1)) = mult(X1,rd(X1,X0)),
inference(superposition,[],[f41836,f14]) ).
fof(f42444,plain,
! [X0,X1] : mult(rd(X0,X1),X0) = mult(X0,mult(rd(X0,mult(X1,X0)),X0)),
inference(superposition,[],[f32501,f41836]) ).
fof(f42539,plain,
! [X0,X1] : mult(rd(X0,X1),X0) = mult(X0,mult(rd(X0,X0),ld(X1,X0))),
inference(forward_demodulation,[],[f42444,f15878]) ).
fof(f42715,plain,
! [X0,X1] : mult(rd(X0,X1),X0) = mult(X0,mult(unit,ld(X1,X0))),
inference(forward_demodulation,[],[f42539,f665]) ).
fof(f42819,plain,
! [X0,X1] : mult(X0,ld(X1,X0)) = mult(rd(X0,X1),X0),
inference(forward_demodulation,[],[f42715,f17]) ).
fof(f43101,plain,
! [X0,X1] : rd(X1,X0) = ld(mult(X0,rd(X0,X1)),X0),
inference(superposition,[],[f214,f42331]) ).
fof(f43152,plain,
! [X0,X1] : rd(X1,X0) = ld(rd(X0,X1),unit),
inference(forward_demodulation,[],[f43101,f1043]) ).
fof(f53022,plain,
! [X0,X1] : ld(X0,unit) = rd(ld(X0,X1),X1),
inference(superposition,[],[f43152,f652]) ).
fof(f53055,plain,
rd(c,b) = ld(ld(c,b),unit),
inference(superposition,[],[f43152,f4687]) ).
fof(f53068,plain,
! [X2,X0,X1] : mult(X2,rd(X0,X1)) = rd(X2,rd(X1,X0)),
inference(superposition,[],[f1017,f43152]) ).
fof(f53075,plain,
! [X2,X0,X1] : ld(rd(X0,X1),X2) = mult(rd(X1,X0),X2),
inference(superposition,[],[f35390,f43152]) ).
fof(f53145,plain,
ld(b,c) = rd(c,b),
inference(forward_demodulation,[],[f53055,f2469]) ).
fof(f53752,plain,
! [X2,X0,X1] : mult(mult(X1,ld(ld(X0,X1),X2)),X1) = ld(ld(X0,unit),mult(X2,X1)),
inference(superposition,[],[f378,f53022]) ).
fof(f53754,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X1) = ld(rd(rd(ld(X0,unit),X2),X1),ld(X0,X1)),
inference(superposition,[],[f637,f53022]) ).
fof(f53807,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X1) = mult(rd(X1,rd(ld(X0,unit),X2)),ld(X0,X1)),
inference(forward_demodulation,[],[f53754,f53075]) ).
fof(f53809,plain,
! [X2,X0,X1] : mult(mult(X1,ld(ld(X0,X1),X2)),X1) = mult(ld(unit,X0),mult(X2,X1)),
inference(forward_demodulation,[],[f53752,f36389]) ).
fof(f53863,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X1) = mult(mult(X1,rd(X2,ld(X0,unit))),ld(X0,X1)),
inference(forward_demodulation,[],[f53807,f53068]) ).
fof(f53865,plain,
! [X2,X0,X1] : mult(X0,mult(X2,X1)) = mult(mult(X1,ld(ld(X0,X1),X2)),X1),
inference(forward_demodulation,[],[f53809,f156]) ).
fof(f53897,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X1) = mult(mult(X1,mult(X2,X0)),ld(X0,X1)),
inference(forward_demodulation,[],[f53863,f1044]) ).
fof(f53899,plain,
! [X2,X0,X1] : mult(X0,mult(X2,X1)) = mult(X1,mult(ld(ld(X0,X1),X2),X1)),
inference(forward_demodulation,[],[f53865,f32501]) ).
fof(f53917,plain,
! [X2,X0,X1] : mult(X1,mult(X2,X1)) = mult(mult(X1,mult(X2,X0)),ld(X0,X1)),
inference(forward_demodulation,[],[f53897,f32501]) ).
fof(f53919,plain,
! [X2,X0,X1] : mult(X0,mult(X2,X1)) = mult(X1,mult(mult(ld(X1,X0),X2),X1)),
inference(forward_demodulation,[],[f53899,f36389]) ).
fof(f54048,plain,
! [X2,X0,X1] : mult(mult(X1,X0),ld(X2,X1)) = mult(X1,mult(rd(X0,X2),X1)),
inference(superposition,[],[f53917,f14]) ).
fof(f54082,plain,
! [X2,X0,X1] : mult(X2,mult(mult(ld(X2,X0),X1),X2)) = mult(mult(mult(X0,X1),ld(X2,X0)),ld(ld(X2,X0),X2)),
inference(superposition,[],[f53917,f151]) ).
fof(f54528,plain,
! [X2,X0,X1] : mult(X2,mult(mult(ld(X2,X0),X1),X2)) = rd(mult(mult(X0,X1),X0),ld(X2,X0)),
inference(forward_demodulation,[],[f54082,f943]) ).
fof(f54776,plain,
! [X2,X0,X1] : mult(mult(mult(X0,X1),X0),ld(X0,X2)) = mult(X2,mult(mult(ld(X2,X0),X1),X2)),
inference(forward_demodulation,[],[f54528,f4911]) ).
fof(f54941,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = mult(mult(mult(X0,X1),X0),ld(X0,X2)),
inference(forward_demodulation,[],[f54776,f53919]) ).
fof(f55051,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = mult(mult(X0,mult(X1,X0)),ld(X0,X2)),
inference(forward_demodulation,[],[f54941,f32501]) ).
fof(f55293,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X0) = mult(X1,mult(rd(X2,rd(X1,X0)),X1)),
inference(superposition,[],[f54048,f214]) ).
fof(f55298,plain,
! [X2,X0,X1] : mult(mult(X1,X2),mult(X0,X1)) = mult(X1,mult(rd(X2,ld(X0,unit)),X1)),
inference(superposition,[],[f54048,f35390]) ).
fof(f55326,plain,
! [X0] : mult(mult(b,X0),mult(b,c)) = mult(b,mult(rd(X0,ld(c,unit)),b)),
inference(superposition,[],[f54048,f5613]) ).
fof(f55645,plain,
! [X0] : mult(mult(b,X0),mult(b,c)) = mult(b,mult(mult(X0,c),b)),
inference(forward_demodulation,[],[f55326,f1044]) ).
fof(f55673,plain,
! [X2,X0,X1] : mult(mult(X1,X2),mult(X0,X1)) = mult(X1,mult(mult(X2,X0),X1)),
inference(forward_demodulation,[],[f55298,f1044]) ).
fof(f55678,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X0) = mult(X1,mult(mult(X2,rd(X0,X1)),X1)),
inference(forward_demodulation,[],[f55293,f53068]) ).
fof(f55914,plain,
! [X2,X0,X1] : mult(mult(X1,X2),X0) = mult(X1,mult(rd(X2,X1),mult(X1,X0))),
inference(forward_demodulation,[],[f55678,f37613]) ).
fof(f57534,plain,
! [X2,X0,X1] : mult(mult(X0,X2),ld(X0,X1)) = mult(X0,mult(mult(X2,ld(X0,rd(X1,X0))),X0)),
inference(superposition,[],[f55673,f35153]) ).
fof(f58088,plain,
! [X2,X0,X1] : mult(mult(X0,X2),ld(X0,X1)) = mult(X0,mult(rd(X2,X0),mult(rd(X1,X0),X0))),
inference(forward_demodulation,[],[f57534,f222]) ).
fof(f58390,plain,
! [X2,X0,X1] : mult(mult(X0,X2),ld(X0,X1)) = mult(X0,mult(rd(X2,X0),X1)),
inference(forward_demodulation,[],[f58088,f14]) ).
fof(f62201,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),X2)) = mult(mult(X0,X1),ld(X1,X2)),
inference(superposition,[],[f55051,f33253]) ).
fof(f63364,plain,
! [X2,X0,X1] : mult(mult(X1,ld(X0,X1)),X2) = mult(X1,mult(ld(X0,unit),mult(X1,X2))),
inference(superposition,[],[f55914,f53022]) ).
fof(f63548,plain,
! [X2,X0,X1] :
( mult(mult(X2,X0),X1) = mult(X2,mult(X0,X1))
| mult(X2,mult(X1,X2)) = mult(X2,mult(X2,X1)) ),
inference(superposition,[],[f55914,f27002]) ).
fof(f63549,plain,
! [X2,X0,X1] :
( mult(mult(X2,X0),X1) = mult(X2,mult(X0,X1))
| mult(X2,X1) = mult(X1,X2) ),
inference(superposition,[],[f55914,f1860]) ).
fof(f63982,plain,
! [X2,X0,X1] : mult(X1,ld(X0,mult(X1,X2))) = mult(mult(X1,ld(X0,X1)),X2),
inference(forward_demodulation,[],[f63364,f33834]) ).
fof(f64486,plain,
! [X2,X0,X1] :
( mult(rd(X0,X1),X2) = mult(X0,mult(ld(X1,unit),X2))
| mult(X0,X2) = mult(X2,X0) ),
inference(superposition,[],[f63549,f1017]) ).
fof(f64776,plain,
( mult(a,mult(b,c)) != mult(a,mult(b,c))
| mult(a,c) = mult(c,a) ),
inference(superposition,[],[f23,f63549]) ).
fof(f64929,plain,
mult(a,c) = mult(c,a),
inference(trivial_inequality_removal,[],[f64776]) ).
fof(f65004,plain,
spl0_87,
inference(avatar_split_clause,[],[f64929,f16706]) ).
fof(f65175,plain,
! [X2,X0,X1] :
( mult(rd(X0,X1),X2) = mult(X0,ld(X1,X2))
| mult(X0,X2) = mult(X2,X0) ),
inference(forward_demodulation,[],[f64486,f33834]) ).
fof(f66350,plain,
( ! [X0] : mult(a,mult(mult(X0,c),a)) = mult(mult(a,X0),mult(a,c))
| ~ spl0_87 ),
inference(superposition,[],[f55673,f16707]) ).
fof(f78520,plain,
! [X2,X0,X1] :
( ld(X0,mult(X0,X1)) = mult(rd(mult(X0,X1),mult(X0,mult(X1,X0))),mult(X0,X1))
| mult(mult(X0,X2),X1) = mult(X0,mult(X2,X1)) ),
inference(superposition,[],[f3052,f63548]) ).
fof(f78727,plain,
! [X2,X0,X1] :
( ld(X0,mult(X0,X1)) = mult(mult(X0,X1),ld(mult(X0,mult(X1,X0)),mult(X0,X1)))
| mult(mult(X0,X2),X1) = mult(X0,mult(X2,X1)) ),
inference(forward_demodulation,[],[f78520,f42819]) ).
fof(f79517,plain,
! [X2,X0,X1] :
( ld(X0,mult(X0,X1)) = mult(mult(X0,X1),ld(X0,unit))
| mult(mult(X0,X2),X1) = mult(X0,mult(X2,X1)) ),
inference(forward_demodulation,[],[f78727,f33499]) ).
fof(f80066,plain,
! [X2,X0,X1] :
( ld(X0,mult(X0,X1)) = mult(X0,mult(rd(X1,X0),unit))
| mult(mult(X0,X2),X1) = mult(X0,mult(X2,X1)) ),
inference(forward_demodulation,[],[f79517,f58390]) ).
fof(f80454,plain,
! [X2,X0,X1] :
( ld(X0,mult(X0,X1)) = mult(X0,rd(X1,X0))
| mult(mult(X0,X2),X1) = mult(X0,mult(X2,X1)) ),
inference(forward_demodulation,[],[f80066,f16]) ).
fof(f80718,plain,
! [X2,X0,X1] :
( mult(X0,rd(X1,X0)) = X1
| mult(mult(X0,X2),X1) = mult(X0,mult(X2,X1)) ),
inference(forward_demodulation,[],[f80454,f13]) ).
fof(f81912,plain,
! [X2,X0,X1] :
( rd(X0,rd(X0,X1)) = X1
| mult(X1,mult(X2,X0)) = mult(mult(X1,X2),X0) ),
inference(superposition,[],[f15,f80718]) ).
fof(f82590,plain,
! [X2,X0,X1] :
( mult(X0,rd(X1,X0)) = X1
| mult(X1,mult(X2,X0)) = mult(mult(X1,X2),X0) ),
inference(forward_demodulation,[],[f81912,f53068]) ).
fof(f91359,plain,
! [X2,X0,X1] :
( mult(mult(X1,X0),X2) = mult(X1,mult(X0,ld(X1,mult(X1,X2))))
| mult(X0,mult(X1,X2)) = mult(mult(X1,X2),X0) ),
inference(superposition,[],[f55914,f65175]) ).
fof(f91648,plain,
! [X2,X0,X1] :
( mult(mult(X1,X0),X2) = mult(X1,mult(X0,X2))
| mult(X0,mult(X1,X2)) = mult(mult(X1,X2),X0) ),
inference(forward_demodulation,[],[f91359,f13]) ).
fof(f92698,plain,
( mult(a,mult(b,c)) != mult(a,mult(b,c))
| mult(mult(a,c),b) = mult(b,mult(a,c)) ),
inference(superposition,[],[f23,f91648]) ).
fof(f93349,plain,
mult(mult(a,c),b) = mult(b,mult(a,c)),
inference(trivial_inequality_removal,[],[f92698]) ).
fof(f94686,definition,
( spl0_251
<=> mult(a,mult(b,c)) = mult(b,mult(a,c)) ),
introduced(definition,[new_symbols(definition,[spl0_251])],[avatar_definition]) ).
fof(f94687,plain,
( mult(a,mult(b,c)) = mult(b,mult(a,c))
| ~ spl0_251 ),
inference(avatar_component_clause,[],[f94686]) ).
fof(f95250,plain,
( mult(mult(a,b),c) = mult(b,mult(a,c))
| mult(mult(a,c),b) = mult(a,mult(c,b)) ),
inference(superposition,[],[f93349,f20]) ).
fof(f95258,plain,
( mult(a,mult(c,b)) = mult(b,mult(a,c))
| mult(a,b) = mult(b,a) ),
inference(superposition,[],[f93349,f63549]) ).
fof(f95262,plain,
( mult(a,mult(c,b)) = mult(b,mult(a,c))
| a = mult(b,rd(a,b)) ),
inference(superposition,[],[f93349,f82590]) ).
fof(f95270,plain,
( mult(a,mult(mult(b,c),b)) = mult(mult(b,mult(a,c)),b)
| mult(mult(a,b),c) = mult(a,mult(b,c)) ),
inference(superposition,[],[f40,f93349]) ).
fof(f95317,plain,
mult(mult(b,mult(a,c)),b) = mult(mult(a,c),mult(b,b)),
inference(superposition,[],[f281,f93349]) ).
fof(f95424,plain,
mult(b,mult(mult(a,c),b)) = mult(mult(a,c),mult(b,b)),
inference(forward_demodulation,[],[f95317,f32507]) ).
fof(f95456,plain,
mult(a,mult(mult(b,c),b)) = mult(mult(b,mult(a,c)),b),
inference(forward_subsumption_resolution,[],[f95270,f23]) ).
fof(f95461,plain,
( mult(a,mult(b,c)) = mult(b,mult(a,c))
| a = mult(b,rd(a,b)) ),
inference(forward_demodulation,[],[f95262,f62]) ).
fof(f95464,plain,
( mult(a,mult(b,c)) = mult(b,mult(a,c))
| mult(a,b) = mult(b,a) ),
inference(forward_demodulation,[],[f95258,f62]) ).
fof(f95468,plain,
( mult(a,mult(b,c)) = mult(mult(a,c),b)
| mult(mult(a,b),c) = mult(b,mult(a,c)) ),
inference(forward_demodulation,[],[f95250,f62]) ).
fof(f95472,definition,
( spl0_252
<=> mult(mult(a,c),mult(b,b)) = mult(b,mult(b,mult(a,c))) ),
introduced(definition,[new_symbols(definition,[spl0_252])],[avatar_definition]) ).
fof(f95473,plain,
( mult(mult(a,c),mult(b,b)) = mult(b,mult(b,mult(a,c)))
| ~ spl0_252 ),
inference(avatar_component_clause,[],[f95472]) ).
fof(f95500,plain,
mult(mult(a,c),mult(b,b)) = mult(b,mult(b,mult(a,c))),
inference(forward_demodulation,[],[f95424,f93349]) ).
fof(f95519,definition,
( spl0_255
<=> a = mult(b,rd(a,b)) ),
introduced(definition,[new_symbols(definition,[spl0_255])],[avatar_definition]) ).
fof(f95520,plain,
( a = mult(b,rd(a,b))
| ~ spl0_255 ),
inference(avatar_component_clause,[],[f95519]) ).
fof(f95543,plain,
mult(a,mult(mult(b,c),b)) = mult(b,mult(mult(a,c),b)),
inference(forward_demodulation,[],[f95456,f32507]) ).
fof(f95546,definition,
( spl0_260
<=> mult(mult(a,b),c) = mult(b,mult(a,c)) ),
introduced(definition,[new_symbols(definition,[spl0_260])],[avatar_definition]) ).
fof(f95547,plain,
( mult(mult(a,b),c) = mult(b,mult(a,c))
| ~ spl0_260 ),
inference(avatar_component_clause,[],[f95546]) ).
fof(f95551,plain,
( spl0_255
| spl0_251 ),
inference(avatar_split_clause,[],[f95461,f94686,f95519]) ).
fof(f95554,plain,
( spl0_89
| spl0_251 ),
inference(avatar_split_clause,[],[f95464,f94686,f16714]) ).
fof(f95557,plain,
( mult(a,mult(b,c)) = mult(b,mult(a,c))
| mult(mult(a,b),c) = mult(b,mult(a,c)) ),
inference(forward_demodulation,[],[f95468,f93349]) ).
fof(f95572,plain,
spl0_252,
inference(avatar_split_clause,[],[f95500,f95472]) ).
fof(f95583,plain,
mult(a,mult(mult(b,c),b)) = mult(b,mult(b,mult(a,c))),
inference(forward_demodulation,[],[f95543,f93349]) ).
fof(f95586,plain,
( spl0_260
| spl0_251 ),
inference(avatar_split_clause,[],[f95557,f94686,f95546]) ).
fof(f95603,plain,
mult(a,mult(b,mult(c,b))) = mult(b,mult(b,mult(a,c))),
inference(forward_demodulation,[],[f95583,f32501]) ).
fof(f95614,plain,
mult(a,mult(b,mult(b,c))) = mult(b,mult(b,mult(a,c))),
inference(forward_demodulation,[],[f95603,f167]) ).
fof(f95628,plain,
( mult(a,mult(b,mult(b,c))) = mult(mult(a,c),mult(b,b))
| ~ spl0_252 ),
inference(forward_demodulation,[],[f95473,f95614]) ).
fof(f97116,plain,
( mult(a,mult(b,c)) != mult(b,mult(a,c))
| ~ spl0_260 ),
inference(superposition,[],[f23,f95547]) ).
fof(f98237,plain,
( mult(a,a) = mult(b,mult(rd(a,b),a))
| ~ spl0_255 ),
inference(superposition,[],[f38040,f95520]) ).
fof(f98267,plain,
( mult(a,a) = mult(b,mult(a,ld(b,a)))
| ~ spl0_255 ),
inference(forward_demodulation,[],[f98237,f42819]) ).
fof(f98533,plain,
( rd(mult(a,mult(b,mult(b,c))),b) = mult(mult(mult(a,c),b),ld(b,b))
| ~ spl0_252 ),
inference(superposition,[],[f676,f95628]) ).
fof(f98728,plain,
( rd(mult(a,mult(b,mult(b,c))),b) = mult(b,mult(ld(b,mult(a,c)),b))
| ~ spl0_252 ),
inference(forward_demodulation,[],[f98533,f62201]) ).
fof(f98811,plain,
( mult(mult(a,c),b) = rd(mult(a,mult(b,mult(b,c))),b)
| ~ spl0_252 ),
inference(forward_demodulation,[],[f98728,f33253]) ).
fof(f98879,plain,
( mult(mult(a,c),b) = mult(mult(a,b),rd(mult(b,c),b))
| ~ spl0_252 ),
inference(forward_demodulation,[],[f98811,f31718]) ).
fof(f98923,plain,
( mult(mult(a,c),b) = mult(mult(a,b),mult(b,rd(c,b)))
| ~ spl0_252 ),
inference(forward_demodulation,[],[f98879,f29397]) ).
fof(f98954,plain,
( mult(mult(a,c),b) = mult(mult(a,b),mult(b,ld(b,c)))
| ~ spl0_252 ),
inference(forward_demodulation,[],[f98923,f53145]) ).
fof(f98985,plain,
( mult(mult(a,b),c) = mult(mult(a,c),b)
| ~ spl0_252 ),
inference(forward_demodulation,[],[f98954,f12]) ).
fof(f99008,plain,
( mult(mult(a,b),c) = mult(b,mult(a,c))
| ~ spl0_252 ),
inference(forward_demodulation,[],[f98985,f93349]) ).
fof(f99019,plain,
( mult(mult(a,b),c) = mult(a,mult(b,c))
| ~ spl0_251
| ~ spl0_252 ),
inference(forward_demodulation,[],[f99008,f94687]) ).
fof(f99029,plain,
( $false
| ~ spl0_251
| ~ spl0_252 ),
inference(forward_subsumption_resolution,[],[f99019,f23]) ).
fof(f99030,plain,
( ~ spl0_251
| ~ spl0_252 ),
inference(avatar_contradiction_clause,[],[f99029]) ).
fof(f106417,plain,
( mult(mult(a,a),mult(b,c)) = mult(b,mult(mult(mult(a,ld(b,a)),c),b))
| ~ spl0_255 ),
inference(superposition,[],[f55645,f98267]) ).
fof(f106625,plain,
( mult(mult(a,a),mult(b,c)) = mult(b,mult(mult(a,ld(b,mult(a,c))),b))
| ~ spl0_255 ),
inference(forward_demodulation,[],[f106417,f63982]) ).
fof(f106720,plain,
( mult(mult(a,a),mult(b,c)) = mult(b,mult(rd(a,b),mult(mult(a,c),b)))
| ~ spl0_255 ),
inference(forward_demodulation,[],[f106625,f222]) ).
fof(f106806,plain,
( mult(mult(a,a),mult(b,c)) = mult(b,mult(rd(a,b),mult(b,mult(a,c))))
| ~ spl0_255 ),
inference(forward_demodulation,[],[f106720,f93349]) ).
fof(f106867,plain,
( mult(mult(a,a),mult(b,c)) = mult(mult(b,a),mult(a,c))
| ~ spl0_255 ),
inference(forward_demodulation,[],[f106806,f55914]) ).
fof(f106910,plain,
( mult(mult(a,a),mult(b,c)) = mult(mult(a,b),mult(a,c))
| ~ spl0_89
| ~ spl0_255 ),
inference(forward_demodulation,[],[f106867,f16715]) ).
fof(f106938,plain,
( mult(a,mult(mult(b,c),a)) = mult(mult(a,a),mult(b,c))
| ~ spl0_87
| ~ spl0_89
| ~ spl0_255 ),
inference(forward_demodulation,[],[f106910,f66350]) ).
fof(f106961,plain,
( mult(a,mult(mult(b,c),a)) = mult(a,mult(a,mult(b,c)))
| ~ spl0_87
| ~ spl0_89
| ~ spl0_255 ),
inference(forward_demodulation,[],[f106938,f28852]) ).
fof(f111876,plain,
( spl0_81
| ~ spl0_87
| ~ spl0_89
| ~ spl0_255 ),
inference(avatar_split_clause,[],[f106961,f95519,f16714,f16706,f16582]) ).
fof(f111899,plain,
( mult(a,mult(b,c)) = mult(b,mult(a,c))
| ~ spl0_87
| ~ spl0_158 ),
inference(forward_demodulation,[],[f26525,f16707]) ).
fof(f111903,plain,
( $false
| ~ spl0_87
| ~ spl0_158
| ~ spl0_260 ),
inference(forward_subsumption_resolution,[],[f111899,f97116]) ).
fof(f111904,plain,
( ~ spl0_87
| ~ spl0_158
| ~ spl0_260 ),
inference(avatar_contradiction_clause,[],[f111903]) ).
fof(f111911,plain,
( mult(mult(a,b),c) = mult(a,mult(b,c))
| ~ spl0_89
| ~ spl0_161 ),
inference(forward_demodulation,[],[f26544,f16715]) ).
fof(f111916,plain,
( $false
| ~ spl0_89
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f111911,f23]) ).
fof(f111917,plain,
( ~ spl0_89
| ~ spl0_161 ),
inference(avatar_contradiction_clause,[],[f111916]) ).
cnf(s90,plain,
( spl0_75
| ~ spl0_81 ),
inference(sat_conversion,[],[f16735]) ).
cnf(s194,plain,
( ~ spl0_75
| spl0_158
| spl0_161 ),
inference(sat_conversion,[],[f26580]) ).
cnf(s223,plain,
spl0_87,
inference(sat_conversion,[],[f65004]) ).
cnf(s324,plain,
( spl0_251
| spl0_255 ),
inference(sat_conversion,[],[f95551]) ).
cnf(s327,plain,
( spl0_89
| spl0_251 ),
inference(sat_conversion,[],[f95554]) ).
cnf(s329,plain,
spl0_252,
inference(sat_conversion,[],[f95572]) ).
cnf(s330,plain,
( spl0_251
| spl0_260 ),
inference(sat_conversion,[],[f95586]) ).
cnf(s396,plain,
( ~ spl0_251
| ~ spl0_252 ),
inference(sat_conversion,[],[f99030]) ).
cnf(s509,plain,
( spl0_81
| ~ spl0_87
| ~ spl0_89
| ~ spl0_255 ),
inference(sat_conversion,[],[f111876]) ).
cnf(s511,plain,
( ~ spl0_87
| ~ spl0_158
| ~ spl0_260 ),
inference(sat_conversion,[],[f111904]) ).
cnf(s512,plain,
( ~ spl0_89
| ~ spl0_161 ),
inference(sat_conversion,[],[f111917]) ).
cnf(s514,plain,
~ spl0_251,
inference(rat,[],[s396,s329]) ).
cnf(s515,plain,
spl0_260,
inference(rat,[],[s330,s514]) ).
cnf(s520,plain,
spl0_89,
inference(rat,[],[s327,s514]) ).
cnf(s521,plain,
~ spl0_161,
inference(rat,[],[s512,s520]) ).
cnf(s526,plain,
spl0_255,
inference(rat,[],[s324,s514]) ).
cnf(s549,plain,
~ spl0_158,
inference(rat,[],[s511,s515,s223]) ).
cnf(s550,plain,
spl0_81,
inference(rat,[],[s509,s526,s520,s223]) ).
cnf(s559,plain,
~ spl0_75,
inference(rat,[],[s194,s521,s549]) ).
cnf(s571,plain,
$false,
inference(rat,[],[s90,s550,s559]) ).
fof(f111930,plain,
$false,
inference(avatar_sat_refutation,[],[s571]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP746+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/5.44 % Computer : n026.cluster.edu
% 0.15/5.44 % Model : x86_64 x86_64
% 0.15/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.44 % Memory : 8046.5625MB
% 0.15/5.44 % OS : Linux 6.8.0-71-generic
% 0.15/5.44 % CPULimit : 300
% 0.15/5.44 % WCLimit : 300
% 0.15/5.44 % DateTime : Sun Sep 27 10:44:32 UTC 2026
% 0.15/5.44 % CPUTime :
% 0.15/5.44 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/5.49 Running first-order theorem proving
% 0.15/5.49 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
% 19.78/8.83 % (2646498)Detected formulas, will run a generic FOF schedule.
% 19.78/8.83 % (2646505)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=467508718:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 19.78/8.83 % (2646507)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2754041016:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 19.78/8.83 % (2646506)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4196762873:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 19.78/8.83 % (2646503)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=292777211:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 19.78/8.83 % (2646504)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=1634977640:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 19.78/8.83 % (2646509)dis-21_1_sil=8000:lcm=predicate:random_seed=860909734: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)
% 19.78/8.83 % (2646508)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=80950630:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 19.78/8.83 % (2646509)Refutation not found, incomplete strategy
% 19.78/8.83 % (2646509)------------------------------
% 19.78/8.83 % (2646509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.78/8.83 % (2646509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.78/8.83 % (2646509)CaDiCaL version: 2.1.3
% 19.78/8.83 % (2646509)Termination reason: Refutation not found, incomplete strategy
% 19.78/8.83 % (2646509)Time elapsed: 0.002 s
% 19.78/8.83 % (2646509)Peak memory usage: 88 MB
% 19.78/8.83 % (2646509)Instructions burned: 1 (million)
% 19.78/8.83 % (2646507)Instruction limit reached!
% 19.78/8.83 % (2646507)------------------------------
% 19.78/8.83 % (2646507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.78/8.83 % (2646507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.78/8.83 % (2646507)CaDiCaL version: 2.1.3
% 19.78/8.83 % (2646507)Termination reason: Instruction limit
% 19.78/8.83 % (2646507)Termination phase: Saturation
% 19.78/8.83 % (2646507)Time elapsed: 0.093 s
% 19.78/8.83 % (2646507)Peak memory usage: 88 MB
% 19.78/8.83 % (2646507)Instructions burned: 119 (million)
% 19.78/8.83 % (2646506)Instruction limit reached!
% 19.78/8.83 % (2646506)------------------------------
% 19.78/8.83 % (2646506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.78/8.83 % (2646506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.78/8.83 % (2646506)CaDiCaL version: 2.1.3
% 19.78/8.83 % (2646506)Termination reason: Instruction limit
% 19.78/8.83 % (2646506)Termination phase: Saturation
% 19.78/8.83 % (2646506)Time elapsed: 0.094 s
% 19.78/8.83 % (2646506)Peak memory usage: 89 MB
% 19.78/8.83 % (2646506)Instructions burned: 109 (million)
% 19.78/8.83 % (2646508)Instruction limit reached!
% 19.78/8.83 % (2646508)------------------------------
% 19.78/8.83 % (2646508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.78/8.83 % (2646508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.78/8.83 % (2646508)CaDiCaL version: 2.1.3
% 19.78/8.83 % (2646508)Termination reason: Instruction limit
% 19.78/8.83 % (2646508)Termination phase: Saturation
% 19.78/8.83 % (2646508)Time elapsed: 0.129 s
% 19.78/8.83 % (2646508)Peak memory usage: 89 MB
% 19.78/8.83 % (2646508)Instructions burned: 140 (million)
% 19.78/8.83 % (2646517)lrs+10_1_sil=8000:sp=occurrence:random_seed=1796147493:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 19.78/8.83 % (2646518)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1513402563:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 19.78/8.83 % (2646519)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2080564924:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 19.78/8.83 % (2646509)------------------------------
% 19.78/8.83 % (2646509)------------------------------
% 19.78/8.83 % (2646518)Instruction limit reached!
% 19.78/8.83 % (2646518)------------------------------
% 19.78/8.83 % (2646518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/10.27 % (2646518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/10.27 % (2646518)CaDiCaL version: 2.1.3
% 30.39/10.27 % (2646518)Termination reason: Instruction limit
% 30.39/10.27 % (2646518)Termination phase: Saturation
% 30.39/10.27 % (2646518)Time elapsed: 0.142 s
% 30.39/10.27 % (2646518)Peak memory usage: 89 MB
% 30.39/10.27 % (2646518)Instructions burned: 157 (million)
% 30.39/10.27 % (2646517)Instruction limit reached!
% 30.39/10.27 % (2646517)------------------------------
% 30.39/10.27 % (2646517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/10.27 % (2646517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/10.27 % (2646517)CaDiCaL version: 2.1.3
% 30.39/10.27 % (2646517)Termination reason: Instruction limit
% 30.39/10.27 % (2646517)Termination phase: Saturation
% 30.39/10.27 % (2646517)Time elapsed: 0.237 s
% 30.39/10.27 % (2646517)Peak memory usage: 90 MB
% 30.39/10.27 % (2646517)Instructions burned: 285 (million)
% 30.39/10.27 % (2646523)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=2362188078:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 30.39/10.27 % (2646519)Instruction limit reached!
% 30.39/10.27 % (2646519)------------------------------
% 30.39/10.27 % (2646519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/10.27 % (2646519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/10.27 % (2646519)CaDiCaL version: 2.1.3
% 30.39/10.27 % (2646519)Termination reason: Instruction limit
% 30.39/10.27 % (2646519)Termination phase: Saturation
% 30.39/10.27 % (2646519)Time elapsed: 0.313 s
% 30.39/10.27 % (2646519)Peak memory usage: 91 MB
% 30.39/10.27 % (2646519)Instructions burned: 325 (million)
% 30.39/10.27 % (2646524)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3422554474:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 30.39/10.27 % (2646523)Instruction limit reached!
% 30.39/10.27 % (2646523)------------------------------
% 30.39/10.27 % (2646523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/10.27 % (2646523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/10.27 % (2646523)CaDiCaL version: 2.1.3
% 30.39/10.27 % (2646523)Termination reason: Instruction limit
% 30.39/10.27 % (2646523)Termination phase: Saturation
% 30.39/10.27 % (2646523)Time elapsed: 0.120 s
% 30.39/10.27 % (2646523)Peak memory usage: 90 MB
% 30.39/10.27 % (2646523)Instructions burned: 249 (million)
% 30.39/10.27 % (2646525)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4166907049:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 30.39/10.27 % (2646527)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4131455448:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 30.39/10.27 % (2646529)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3811503170:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 30.39/10.27 % (2646529)Refutation not found, incomplete strategy
% 30.39/10.27 % (2646529)------------------------------
% 30.39/10.27 % (2646529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/10.27 % (2646529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/10.27 % (2646529)CaDiCaL version: 2.1.3
% 30.39/10.27 % (2646529)Termination reason: Refutation not found, incomplete strategy
% 30.39/10.27 % (2646529)Time elapsed: 0.001 s
% 30.39/10.27 % (2646529)Peak memory usage: 87 MB
% 30.39/10.27 % (2646524)Instruction limit reached!
% 30.39/10.27 % (2646524)------------------------------
% 30.39/10.27 % (2646524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/10.27 % (2646524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/10.27 % (2646524)CaDiCaL version: 2.1.3
% 30.39/10.27 % (2646524)Termination reason: Instruction limit
% 30.39/10.27 % (2646524)Termination phase: Saturation
% 30.39/10.27 % (2646524)Time elapsed: 0.252 s
% 30.39/10.27 % (2646524)Peak memory usage: 89 MB
% 30.39/10.27 % (2646524)Instructions burned: 295 (million)
% 30.39/10.27 % (2646527)Instruction limit reached!
% 30.39/10.27 % (2646527)------------------------------
% 30.39/10.27 % (2646527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/10.27 % (2646527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/10.27 % (2646527)CaDiCaL version: 2.1.3
% 30.39/10.27 % (2646527)Termination reason: Instruction limit
% 61.50/14.62 % (2646527)Termination phase: Saturation
% 61.50/14.62 % (2646527)Time elapsed: 0.107 s
% 61.50/14.62 % (2646527)Peak memory usage: 89 MB
% 61.50/14.62 % (2646527)Instructions burned: 114 (million)
% 61.50/14.62 % (2646529)------------------------------
% 61.50/14.62 % (2646529)------------------------------
% 61.50/14.62 % (2646533)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=172287848:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi)
% 61.50/14.62 % (2646534)lrs+10_1_sil=8000:sp=occurrence:random_seed=3084543962:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 61.50/14.62 % (2646533)Instruction limit reached!
% 61.50/14.62 % (2646533)------------------------------
% 61.50/14.62 % (2646533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.50/14.62 % (2646533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.50/14.62 % (2646533)CaDiCaL version: 2.1.3
% 61.50/14.62 % (2646533)Termination reason: Instruction limit
% 61.50/14.62 % (2646533)Termination phase: Saturation
% 61.50/14.62 % (2646533)Time elapsed: 0.086 s
% 61.50/14.62 % (2646533)Peak memory usage: 88 MB
% 61.50/14.62 % (2646533)Instructions burned: 115 (million)
% 61.50/14.62 % (2646535)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1007816828:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 61.50/14.62 % (2646535)Instruction limit reached!
% 61.50/14.62 % (2646535)------------------------------
% 61.50/14.62 % (2646535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.50/14.62 % (2646535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.50/14.62 % (2646535)CaDiCaL version: 2.1.3
% 61.50/14.62 % (2646535)Termination reason: Instruction limit
% 61.50/14.62 % (2646535)Termination phase: Saturation
% 61.50/14.62 % (2646535)Time elapsed: 0.181 s
% 61.50/14.62 % (2646535)Peak memory usage: 90 MB
% 61.50/14.62 % (2646535)Instructions burned: 437 (million)
% 61.50/14.62 % (2646538)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3981644562:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 61.50/14.62 % (2646540)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=223176385:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2983 on theBenchmark for (2983ds/134Mi)
% 61.50/14.62 % (2646540)Refutation not found, incomplete strategy
% 61.50/14.62 % (2646540)------------------------------
% 61.50/14.62 % (2646540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.50/14.62 % (2646540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.50/14.62 % (2646540)CaDiCaL version: 2.1.3
% 61.50/14.62 % (2646540)Termination reason: Refutation not found, incomplete strategy
% 61.50/14.62 % (2646540)Time elapsed: 0.002 s
% 61.50/14.62 % (2646540)Peak memory usage: 89 MB
% 61.50/14.62 % (2646540)Instructions burned: 1 (million)
% 61.50/14.62 % (2646540)------------------------------
% 61.50/14.62 % (2646540)------------------------------
% 61.50/14.62 % (2646534)Instruction limit reached!
% 61.50/14.62 % (2646534)------------------------------
% 61.50/14.62 % (2646534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.50/14.62 % (2646534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.50/14.62 % (2646534)CaDiCaL version: 2.1.3
% 61.50/14.62 % (2646534)Termination reason: Instruction limit
% 61.50/14.62 % (2646534)Termination phase: Saturation
% 61.50/14.62 % (2646534)Time elapsed: 0.870 s
% 61.50/14.62 % (2646534)Peak memory usage: 95 MB
% 61.50/14.62 % (2646534)Instructions burned: 907 (million)
% 61.50/14.62 % (2646545)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1432108679:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 61.50/14.62 % (2646546)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=59125854:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 61.50/14.62 % (2646545)Instruction limit reached!
% 61.50/14.62 % (2646545)------------------------------
% 61.50/14.62 % (2646545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.50/14.62 % (2646545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.50/14.62 % (2646545)CaDiCaL version: 2.1.3
% 61.50/14.62 % (2646545)Termination reason: Instruction limit
% 61.50/14.62 % (2646545)Termination phase: Saturation
% 61.50/14.62 % (2646545)Time elapsed: 0.342 s
% 61.50/14.62 % (2646545)Peak memory usage: 95 MB
% 61.50/14.62 % (2646545)Instructions burned: 594 (million)
% 61.50/14.62 % (2646551)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=567544087:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/125Mi)
% 117.89/22.56 % (2646551)Instruction limit reached!
% 117.89/22.56 % (2646551)------------------------------
% 117.89/22.56 % (2646551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.89/22.56 % (2646551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.89/22.56 % (2646551)CaDiCaL version: 2.1.3
% 117.89/22.56 % (2646551)Termination reason: Instruction limit
% 117.89/22.56 % (2646551)Termination phase: Saturation
% 117.89/22.56 % (2646551)Time elapsed: 0.124 s
% 117.89/22.56 % (2646551)Peak memory usage: 90 MB
% 117.89/22.56 % (2646551)Instructions burned: 125 (million)
% 117.89/22.56 % (2646525)Instruction limit reached!
% 117.89/22.56 % (2646525)------------------------------
% 117.89/22.56 % (2646525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.89/22.56 % (2646525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.89/22.56 % (2646525)CaDiCaL version: 2.1.3
% 117.89/22.56 % (2646525)Termination reason: Instruction limit
% 117.89/22.56 % (2646525)Termination phase: Saturation
% 117.89/22.56 % (2646525)Time elapsed: 2.191 s
% 117.89/22.56 % (2646525)Peak memory usage: 143 MB
% 117.89/22.56 % (2646525)Instructions burned: 2351 (million)
% 117.89/22.56 % (2646555)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2144813397:i=134:gtgl=5:slsql=off:gtg=exists_sym_2970 on theBenchmark for (2970ds/134Mi)
% 117.89/22.56 % (2646555)Instruction limit reached!
% 117.89/22.56 % (2646555)------------------------------
% 117.89/22.56 % (2646555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.89/22.56 % (2646555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.89/22.56 % (2646555)CaDiCaL version: 2.1.3
% 117.89/22.56 % (2646555)Termination reason: Instruction limit
% 117.89/22.56 % (2646555)Termination phase: Saturation
% 117.89/22.56 % (2646555)Time elapsed: 0.130 s
% 117.89/22.56 % (2646555)Peak memory usage: 90 MB
% 117.89/22.56 % (2646555)Instructions burned: 134 (million)
% 117.89/22.56 % (2646556)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3351116437:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/141Mi)
% 117.89/22.56 % (2646556)Refutation not found, incomplete strategy
% 117.89/22.56 % (2646556)------------------------------
% 117.89/22.56 % (2646556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.89/22.56 % (2646556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.89/22.56 % (2646556)CaDiCaL version: 2.1.3
% 117.89/22.56 % (2646556)Termination reason: Refutation not found, incomplete strategy
% 117.89/22.56 % (2646556)Time elapsed: 0.002 s
% 117.89/22.56 % (2646556)Peak memory usage: 88 MB
% 117.89/22.56 % (2646558)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=881093595:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2966 on theBenchmark for (2966ds/431Mi)
% 117.89/22.56 % (2646558)Refutation not found, incomplete strategy
% 117.89/22.56 % (2646558)------------------------------
% 117.89/22.56 % (2646558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.89/22.56 % (2646558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.89/22.56 % (2646558)CaDiCaL version: 2.1.3
% 117.89/22.56 % (2646558)Termination reason: Refutation not found, incomplete strategy
% 117.89/22.56 % (2646558)Time elapsed: 0.002 s
% 117.89/22.56 % (2646558)Peak memory usage: 88 MB
% 117.89/22.56 % (2646556)------------------------------
% 117.89/22.56 % (2646556)------------------------------
% 117.89/22.56 % (2646558)------------------------------
% 117.89/22.56 % (2646558)------------------------------
% 117.89/22.56 % (2646561)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=1389608284:i=6060:aac=none:ins=25_2962 on theBenchmark for (2962ds/6060Mi)
% 117.89/22.56 % (2646562)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=1956534818:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2960 on theBenchmark for (2960ds/150Mi)
% 117.89/22.56 % (2646562)Instruction limit reached!
% 117.89/22.56 % (2646562)------------------------------
% 117.89/22.56 % (2646562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.89/22.56 % (2646562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646562)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646562)Termination reason: Instruction limit
% 120.04/22.87 % (2646562)Termination phase: Saturation
% 120.04/22.87 % (2646562)Time elapsed: 0.139 s
% 120.04/22.87 % (2646562)Peak memory usage: 90 MB
% 120.04/22.87 % (2646562)Instructions burned: 150 (million)
% 120.04/22.87 % (2646565)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=852858852:i=14155:bd=all_2957 on theBenchmark for (2957ds/14155Mi)
% 120.04/22.87 % (2646538)Instruction limit reached!
% 120.04/22.87 % (2646538)------------------------------
% 120.04/22.87 % (2646538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.04/22.87 % (2646538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646538)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646538)Termination reason: Instruction limit
% 120.04/22.87 % (2646538)Termination phase: Saturation
% 120.04/22.87 % (2646538)Time elapsed: 4.622 s
% 120.04/22.87 % (2646538)Peak memory usage: 160 MB
% 120.04/22.87 % (2646538)Instructions burned: 5202 (million)
% 120.04/22.87 % (2646569)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=94898818:i=667:av=off:fsr=off_2937 on theBenchmark for (2937ds/667Mi)
% 120.04/22.87 % (2646569)Instruction limit reached!
% 120.04/22.87 % (2646569)------------------------------
% 120.04/22.87 % (2646569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.04/22.87 % (2646569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646569)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646569)Termination reason: Instruction limit
% 120.04/22.87 % (2646569)Termination phase: Saturation
% 120.04/22.87 % (2646569)Time elapsed: 0.470 s
% 120.04/22.87 % (2646569)Peak memory usage: 89 MB
% 120.04/22.87 % (2646569)Instructions burned: 667 (million)
% 120.04/22.87 % (2646571)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=593305013:s2a=on:i=185:s2at=1.8:fdi=4_2930 on theBenchmark for (2930ds/185Mi)
% 120.04/22.87 % (2646571)Instruction limit reached!
% 120.04/22.87 % (2646571)------------------------------
% 120.04/22.87 % (2646571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.04/22.87 % (2646571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646571)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646571)Termination reason: Instruction limit
% 120.04/22.87 % (2646571)Termination phase: Saturation
% 120.04/22.87 % (2646571)Time elapsed: 0.172 s
% 120.04/22.87 % (2646571)Peak memory usage: 91 MB
% 120.04/22.87 % (2646571)Instructions burned: 186 (million)
% 120.04/22.87 % (2646573)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1114338722:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2925 on theBenchmark for (2925ds/193Mi)
% 120.04/22.87 % (2646573)Instruction limit reached!
% 120.04/22.87 % (2646573)------------------------------
% 120.04/22.87 % (2646573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.04/22.87 % (2646573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646573)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646573)Termination reason: Instruction limit
% 120.04/22.87 % (2646573)Termination phase: Saturation
% 120.04/22.87 % (2646573)Time elapsed: 0.174 s
% 120.04/22.87 % (2646573)Peak memory usage: 90 MB
% 120.04/22.87 % (2646573)Instructions burned: 194 (million)
% 120.04/22.87 % (2646575)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2164429671:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2921 on theBenchmark for (2921ds/4850Mi)
% 120.04/22.87 % (2646575)Refutation not found, incomplete strategy
% 120.04/22.87 % (2646575)------------------------------
% 120.04/22.87 % (2646575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.04/22.87 % (2646575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646575)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646575)Termination reason: Refutation not found, incomplete strategy
% 120.04/22.87 % (2646575)Time elapsed: 0.001 s
% 120.04/22.87 % (2646575)Peak memory usage: 87 MB
% 120.04/22.87 % (2646575)------------------------------
% 120.04/22.87 % (2646575)------------------------------
% 120.04/22.87 % (2646577)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1653339055:i=12111:sd=1:ss=included_2915 on theBenchmark for (2915ds/12111Mi)
% 120.04/22.87 % (2646546)Instruction limit reached!
% 120.04/22.87 % (2646546)------------------------------
% 120.04/22.87 % (2646546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.04/22.87 % (2646546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646546)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646546)Termination reason: Instruction limit
% 120.04/22.87 % (2646546)Termination phase: Saturation
% 120.04/22.87 % (2646546)Time elapsed: 7.199 s
% 120.04/22.87 % (2646546)Peak memory usage: 219 MB
% 120.04/22.87 % (2646546)Instructions burned: 13195 (million)
% 120.04/22.87 % (2646579)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3906230354:i=319:kws=precedence:fsr=off_2903 on theBenchmark for (2903ds/319Mi)
% 120.04/22.87 % (2646579)Instruction limit reached!
% 120.04/22.87 % (2646579)------------------------------
% 120.04/22.87 % (2646579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.04/22.87 % (2646579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646579)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646579)Termination reason: Instruction limit
% 120.04/22.87 % (2646579)Termination phase: Saturation
% 120.04/22.87 % (2646579)Time elapsed: 0.174 s
% 120.04/22.87 % (2646579)Peak memory usage: 93 MB
% 120.04/22.87 % (2646579)Instructions burned: 320 (million)
% 120.04/22.87 % (2646581)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2140090532:i=2064:ep=RST_2899 on theBenchmark for (2899ds/2064Mi)
% 120.04/22.87 % (2646561)Instruction limit reached!
% 120.04/22.87 % (2646561)------------------------------
% 120.04/22.87 % (2646561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.04/22.87 % (2646561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646561)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646561)Termination reason: Instruction limit
% 120.04/22.87 % (2646561)Termination phase: Saturation
% 120.04/22.87 % (2646561)Time elapsed: 6.391 s
% 120.04/22.87 % (2646561)Peak memory usage: 177 MB
% 120.04/22.87 % (2646561)Instructions burned: 6060 (million)
% 120.04/22.87 % (2646583)dis-1011_128_sil=32000:random_seed=839291848:i=3706:ep=RST:av=off_2895 on theBenchmark for (2895ds/3706Mi)
% 120.04/22.87 % (2646581)Instruction limit reached!
% 120.04/22.87 % (2646581)------------------------------
% 120.04/22.87 % (2646581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.04/22.87 % (2646581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646581)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646581)Termination reason: Instruction limit
% 120.04/22.87 % (2646581)Termination phase: Saturation
% 120.04/22.87 % (2646581)Time elapsed: 1.157 s
% 120.04/22.87 % (2646581)Peak memory usage: 106 MB
% 120.04/22.87 % (2646581)Instructions burned: 2065 (million)
% 120.04/22.87 % (2646585)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2138883688:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2886 on theBenchmark for (2886ds/757Mi)
% 120.04/22.87 % (2646585)Instruction limit reached!
% 120.04/22.87 % (2646585)------------------------------
% 120.04/22.87 % (2646585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.04/22.87 % (2646585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646585)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646585)Termination reason: Instruction limit
% 120.04/22.87 % (2646585)Termination phase: Saturation
% 120.04/22.87 % (2646585)Time elapsed: 0.336 s
% 120.04/22.87 % (2646585)Peak memory usage: 100 MB
% 120.04/22.87 % (2646585)Instructions burned: 758 (million)
% 120.04/22.87 % (2646589)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1970850296:i=13913:ss=axioms:sgt=8_2881 on theBenchmark for (2881ds/13913Mi)
% 120.04/22.87 % (2646583)Instruction limit reached!
% 120.04/22.87 % (2646583)------------------------------
% 120.04/22.87 % (2646583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.04/22.87 % (2646583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.04/22.87 % (2646583)CaDiCaL version: 2.1.3
% 120.04/22.87 % (2646583)Termination reason: Instruction limit
% 120.04/22.87 % (2646583)Termination phase: Saturation
% 120.04/22.87 % (2646583)Time elapsed: 3.668 s
% 120.04/22.87 % (2646583)Peak memory usage: 116 MB
% 120.04/22.87 % (2646583)Instructions burned: 3708 (million)
% 120.04/22.87 % (2646648)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4046891039:i=9925:aac=none_2856 on theBenchmark for (2856ds/9925Mi)
% 120.04/22.87 % (2646504)First to succeed.
% 120.04/22.87 % (2646504)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2646498"
% 120.04/22.87 % (2646504)Refutation found. Thanks to Tanya!
% 120.04/22.87 % SZS status Theorem for theBenchmark
% 120.04/22.87 % SZS output start Proof for theBenchmark
% See solution above
% 120.51/22.97 % (2646504)------------------------------
% 120.51/22.97 % (2646504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.51/22.97 % (2646504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.51/22.97 % (2646504)CaDiCaL version: 2.1.3
% 120.51/22.97 % (2646504)Termination reason: Refutation
% 120.51/22.97 % (2646504)Time elapsed: 16.380 s
% 120.51/22.97 % (2646504)Peak memory usage: 256 MB
% 120.51/22.97 % (2646504)Instructions burned: 16959 (million)
% 120.51/22.97 % (2646504)------------------------------
% 120.51/22.97 % (2646504)------------------------------
% 120.51/22.97 % (2646498)Success in time 16.896 s
% 120.51/22.97 % Vampire exiting
%------------------------------------------------------------------------------