%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP002-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:12:04 AM UTC 2026
% Result : Unsatisfiable 76.63s 11.66s
% Output : Refutation 77.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 16
% Syntax : Number of formulae : 344 ( 322 unt; 0 def)
% Number of atoms : 378 ( 295 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 70 ( 36 ~; 34 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 230 ( 230 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : product(identity,X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_identity) ).
fof(f2,axiom,
! [X0] : product(X0,identity,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_identity) ).
fof(f3,axiom,
! [X0] : product(inverse(X0),X0,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_inverse) ).
fof(f4,axiom,
! [X0] : product(X0,inverse(X0),identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_inverse) ).
fof(f5,axiom,
! [X0,X1] : product(X0,X1,multiply(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',total_function1) ).
fof(f6,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| X2 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',total_function2) ).
fof(f7,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(X2,X3,X5)
| ~ product(X1,X3,X4)
| ~ product(X0,X1,X2)
| product(X0,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity1) ).
fof(f8,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(X0,X4,X5)
| ~ product(X1,X3,X4)
| ~ product(X0,X1,X2)
| product(X2,X3,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity2) ).
fof(f9,axiom,
! [X0,X1] :
( ~ product(X0,X0,X1)
| product(X0,X1,identity) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_cubed_is_identity_1) ).
fof(f10,axiom,
! [X0,X1] :
( ~ product(X0,X0,X1)
| product(X1,X0,identity) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_cubed_is_identity_2) ).
fof(f11,negated_conjecture,
product(a,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_times_b_is_c) ).
fof(f12,negated_conjecture,
product(c,inverse(a),d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_times_inverse_a_is_d) ).
fof(f13,negated_conjecture,
product(d,inverse(b),h),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_times_inverse_b_is_h) ).
fof(f14,negated_conjecture,
product(h,b,j),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_times_b_is_j) ).
fof(f15,negated_conjecture,
product(j,inverse(h),k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',j_times_inverse_h_is_k) ).
fof(f16,negated_conjecture,
~ product(k,inverse(b),identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_k_times_inverse_b_is_e) ).
fof(f21,plain,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,identity)
| ~ product(X2,X0,X3)
| product(X3,X1,X2) ),
inference(resolution,[],[f8,f2]) ).
fof(f28,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,inverse(h))
| ~ product(j,X0,X2)
| product(X2,X1,k) ),
inference(resolution,[],[f8,f15]) ).
fof(f30,plain,
! [X2,X3,X0,X1] :
( ~ product(X3,X0,identity)
| ~ product(X0,X1,X2)
| product(X3,X2,X1) ),
inference(resolution,[],[f7,f1]) ).
fof(f37,plain,
! [X2,X3,X0,X1] :
( ~ product(X0,inverse(X1),X2)
| ~ product(X3,X0,X1)
| product(X3,X2,identity) ),
inference(resolution,[],[f4,f7]) ).
fof(f48,plain,
! [X0] : product(multiply(X0,X0),X0,identity),
inference(resolution,[],[f5,f10]) ).
fof(f49,plain,
! [X0] : product(X0,multiply(X0,X0),identity),
inference(resolution,[],[f5,f9]) ).
fof(f50,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,X2)
| multiply(X0,X1) = X2 ),
inference(resolution,[],[f5,f6]) ).
fof(f52,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X3,X0,X4)
| ~ product(X0,X1,X2)
| product(X4,X1,multiply(X3,X2)) ),
inference(resolution,[],[f5,f8]) ).
fof(f56,plain,
! [X0,X1] :
( ~ product(X0,multiply(X0,X0),X1)
| identity = X1 ),
inference(resolution,[],[f49,f6]) ).
fof(f65,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,X2)
| product(X2,inverse(X1),X0) ),
inference(resolution,[],[f21,f4]) ).
fof(f68,plain,
! [X2,X0,X1] :
( ~ product(X0,inverse(X1),X2)
| product(X2,X1,X0) ),
inference(resolution,[],[f21,f3]) ).
fof(f73,plain,
! [X0] : product(identity,X0,inverse(inverse(X0))),
inference(resolution,[],[f68,f3]) ).
fof(f75,plain,
product(d,a,c),
inference(resolution,[],[f68,f12]) ).
fof(f76,plain,
product(h,b,d),
inference(resolution,[],[f68,f13]) ).
fof(f77,plain,
product(k,h,j),
inference(resolution,[],[f68,f15]) ).
fof(f107,plain,
! [X2,X0,X1] :
( ~ product(inverse(X0),X1,X2)
| product(X0,X2,X1) ),
inference(resolution,[],[f30,f4]) ).
fof(f110,plain,
! [X2,X0,X1] :
( product(inverse(X0),X2,X1)
| ~ product(X0,X1,X2) ),
inference(resolution,[],[f30,f3]) ).
fof(f114,plain,
! [X0,X1] : product(X0,multiply(inverse(X0),X1),X1),
inference(resolution,[],[f107,f5]) ).
fof(f216,plain,
! [X0] : product(identity,inverse(X0),multiply(X0,X0)),
inference(resolution,[],[f65,f48]) ).
fof(f218,plain,
product(c,inverse(b),a),
inference(resolution,[],[f65,f11]) ).
fof(f370,plain,
! [X0] : identity = multiply(X0,multiply(X0,X0)),
inference(resolution,[],[f56,f5]) ).
fof(f393,plain,
! [X0] : multiply(X0,identity) = X0,
inference(resolution,[],[f50,f2]) ).
fof(f398,plain,
! [X0] : multiply(identity,X0) = X0,
inference(resolution,[],[f50,f1]) ).
fof(f399,plain,
! [X0] : inverse(inverse(X0)) = multiply(identity,X0),
inference(resolution,[],[f50,f73]) ).
fof(f402,plain,
! [X0] : multiply(X0,X0) = multiply(identity,inverse(X0)),
inference(resolution,[],[f50,f216]) ).
fof(f404,plain,
! [X2,X0,X1] :
( ~ product(X0,X2,X1)
| multiply(inverse(X0),X1) = X2 ),
inference(resolution,[],[f50,f110]) ).
fof(f408,plain,
c = multiply(a,b),
inference(resolution,[],[f50,f11]) ).
fof(f409,plain,
d = multiply(c,inverse(a)),
inference(resolution,[],[f50,f12]) ).
fof(f410,plain,
a = multiply(c,inverse(b)),
inference(resolution,[],[f50,f218]) ).
fof(f411,plain,
h = multiply(d,inverse(b)),
inference(resolution,[],[f50,f13]) ).
fof(f413,plain,
c = multiply(d,a),
inference(resolution,[],[f50,f75]) ).
fof(f414,plain,
j = multiply(h,b),
inference(resolution,[],[f50,f14]) ).
fof(f415,plain,
d = multiply(h,b),
inference(resolution,[],[f50,f76]) ).
fof(f417,plain,
k = multiply(j,inverse(h)),
inference(resolution,[],[f50,f15]) ).
fof(f419,plain,
j = multiply(k,h),
inference(resolution,[],[f50,f77]) ).
fof(f421,plain,
d = j,
inference(forward_demodulation,[],[f414,f415]) ).
fof(f483,plain,
! [X0] : inverse(X0) = multiply(X0,X0),
inference(backward_demodulation,[],[f402,f398]) ).
fof(f495,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(backward_demodulation,[],[f399,f398]) ).
fof(f504,plain,
product(d,inverse(h),k),
inference(backward_demodulation,[],[f15,f421]) ).
fof(f506,plain,
! [X2,X0,X1] :
( ~ product(d,X0,X2)
| ~ product(X0,X1,inverse(h))
| product(X2,X1,k) ),
inference(backward_demodulation,[],[f28,f421]) ).
fof(f537,plain,
k = multiply(d,inverse(h)),
inference(backward_demodulation,[],[f417,f421]) ).
fof(f539,plain,
d = multiply(k,h),
inference(backward_demodulation,[],[f419,f421]) ).
fof(f607,plain,
k = multiply(d,multiply(h,h)),
inference(forward_demodulation,[],[f537,f483]) ).
fof(f625,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,multiply(h,h))
| ~ product(d,X0,X2)
| product(X2,X1,k) ),
inference(forward_demodulation,[],[f506,f483]) ).
fof(f626,plain,
product(d,multiply(h,h),k),
inference(forward_demodulation,[],[f504,f483]) ).
fof(f694,plain,
d = multiply(c,multiply(a,a)),
inference(superposition,[],[f409,f483]) ).
fof(f696,plain,
h = multiply(d,multiply(b,b)),
inference(superposition,[],[f411,f483]) ).
fof(f698,plain,
product(d,multiply(b,b),h),
inference(superposition,[],[f13,f483]) ).
fof(f699,plain,
~ product(k,multiply(b,b),identity),
inference(superposition,[],[f16,f483]) ).
fof(f957,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,X2)
| product(X0,multiply(X1,inverse(X2)),identity) ),
inference(resolution,[],[f37,f5]) ).
fof(f1050,plain,
! [X0] :
( ~ product(d,h,X0)
| product(X0,h,k) ),
inference(resolution,[],[f625,f5]) ).
fof(f1061,plain,
product(multiply(d,h),h,k),
inference(resolution,[],[f1050,f5]) ).
fof(f1102,plain,
a = multiply(c,multiply(b,b)),
inference(superposition,[],[f410,f483]) ).
fof(f1149,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(resolution,[],[f114,f50]) ).
fof(f1201,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),X1)) = X1,
inference(superposition,[],[f1149,f483]) ).
fof(f1229,plain,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X2)
| product(multiply(X3,X0),X1,multiply(X3,X2)) ),
inference(resolution,[],[f52,f5]) ).
fof(f1341,plain,
! [X2,X0,X1] : product(multiply(X0,X1),X2,multiply(X0,multiply(X1,X2))),
inference(resolution,[],[f1229,f5]) ).
fof(f1414,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(resolution,[],[f1341,f50]) ).
fof(f1472,plain,
product(multiply(d,b),b,h),
inference(superposition,[],[f1341,f696]) ).
fof(f1512,plain,
! [X0,X1] : multiply(X0,multiply(X0,multiply(X0,X1))) = X1,
inference(backward_demodulation,[],[f1201,f1414]) ).
fof(f1566,plain,
! [X0,X1] : multiply(inverse(X0),X1) = multiply(X0,multiply(X0,X1)),
inference(superposition,[],[f1414,f483]) ).
fof(f1574,plain,
! [X0] : multiply(a,X0) = multiply(c,multiply(inverse(b),X0)),
inference(superposition,[],[f1414,f410]) ).
fof(f1577,plain,
! [X0] : multiply(h,X0) = multiply(d,multiply(multiply(b,b),X0)),
inference(superposition,[],[f1414,f696]) ).
fof(f1578,plain,
! [X0] : multiply(d,X0) = multiply(c,multiply(multiply(a,a),X0)),
inference(superposition,[],[f1414,f694]) ).
fof(f1581,plain,
! [X0] : multiply(c,X0) = multiply(d,multiply(a,X0)),
inference(superposition,[],[f1414,f413]) ).
fof(f1582,plain,
! [X0] : multiply(c,X0) = multiply(a,multiply(b,X0)),
inference(superposition,[],[f1414,f408]) ).
fof(f1583,plain,
! [X0] : multiply(d,X0) = multiply(h,multiply(b,X0)),
inference(superposition,[],[f1414,f415]) ).
fof(f1584,plain,
! [X0] : multiply(d,X0) = multiply(k,multiply(h,X0)),
inference(superposition,[],[f1414,f539]) ).
fof(f1601,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = multiply(X0,multiply(X1,multiply(X0,X1))),
inference(superposition,[],[f483,f1414]) ).
fof(f1641,plain,
! [X0] : multiply(d,X0) = multiply(c,multiply(a,multiply(a,X0))),
inference(forward_demodulation,[],[f1578,f1414]) ).
fof(f1642,plain,
! [X0] : multiply(h,X0) = multiply(d,multiply(b,multiply(b,X0))),
inference(forward_demodulation,[],[f1577,f1414]) ).
fof(f1645,plain,
! [X0] : multiply(a,X0) = multiply(c,multiply(multiply(b,b),X0)),
inference(forward_demodulation,[],[f1574,f483]) ).
fof(f1659,plain,
! [X0] : multiply(a,X0) = multiply(c,multiply(b,multiply(b,X0))),
inference(forward_demodulation,[],[f1645,f1414]) ).
fof(f1670,plain,
multiply(d,b) = multiply(k,d),
inference(superposition,[],[f1584,f415]) ).
fof(f1689,plain,
! [X0] : multiply(k,multiply(d,X0)) = multiply(multiply(d,b),X0),
inference(superposition,[],[f1414,f1670]) ).
fof(f1696,plain,
! [X0] : multiply(k,multiply(d,X0)) = multiply(d,multiply(b,X0)),
inference(forward_demodulation,[],[f1689,f1414]) ).
fof(f1726,plain,
multiply(d,c) = multiply(c,b),
inference(superposition,[],[f1581,f408]) ).
fof(f1747,plain,
! [X0] : multiply(d,multiply(c,X0)) = multiply(multiply(c,b),X0),
inference(superposition,[],[f1414,f1726]) ).
fof(f1754,plain,
! [X0] : multiply(d,multiply(c,X0)) = multiply(c,multiply(b,X0)),
inference(forward_demodulation,[],[f1747,f1414]) ).
fof(f1831,plain,
! [X0,X1] : product(X0,multiply(X1,inverse(multiply(X0,X1))),identity),
inference(resolution,[],[f957,f5]) ).
fof(f2323,plain,
! [X0,X1] : multiply(inverse(X0),identity) = multiply(X1,inverse(multiply(X0,X1))),
inference(resolution,[],[f404,f1831]) ).
fof(f2336,plain,
b = multiply(inverse(a),c),
inference(resolution,[],[f404,f11]) ).
fof(f2337,plain,
inverse(a) = multiply(inverse(c),d),
inference(resolution,[],[f404,f12]) ).
fof(f2341,plain,
multiply(h,h) = multiply(inverse(d),k),
inference(resolution,[],[f404,f626]) ).
fof(f2342,plain,
multiply(b,b) = multiply(inverse(d),h),
inference(resolution,[],[f404,f698]) ).
fof(f2344,plain,
b = multiply(inverse(h),d),
inference(resolution,[],[f404,f76]) ).
fof(f2349,plain,
b = multiply(h,multiply(h,d)),
inference(forward_demodulation,[],[f2344,f1566]) ).
fof(f2351,plain,
multiply(b,b) = multiply(d,multiply(d,h)),
inference(forward_demodulation,[],[f2342,f1566]) ).
fof(f2352,plain,
multiply(h,h) = multiply(d,multiply(d,k)),
inference(forward_demodulation,[],[f2341,f1566]) ).
fof(f2356,plain,
inverse(a) = multiply(c,multiply(c,d)),
inference(forward_demodulation,[],[f2337,f1566]) ).
fof(f2357,plain,
b = multiply(a,multiply(a,c)),
inference(forward_demodulation,[],[f2336,f1566]) ).
fof(f2367,plain,
! [X0,X1] : inverse(X0) = multiply(X1,inverse(multiply(X0,X1))),
inference(forward_demodulation,[],[f2323,f393]) ).
fof(f2381,plain,
multiply(a,a) = multiply(c,multiply(c,d)),
inference(forward_demodulation,[],[f2356,f483]) ).
fof(f2442,plain,
! [X0] : multiply(multiply(h,h),X0) = multiply(d,multiply(multiply(d,k),X0)),
inference(superposition,[],[f1414,f2352]) ).
fof(f2443,plain,
! [X0] : multiply(multiply(h,h),X0) = multiply(d,multiply(d,multiply(k,X0))),
inference(forward_demodulation,[],[f2442,f1414]) ).
fof(f2445,plain,
! [X0] : multiply(h,multiply(h,X0)) = multiply(d,multiply(d,multiply(k,X0))),
inference(forward_demodulation,[],[f2443,f1414]) ).
fof(f2453,plain,
! [X0] : multiply(multiply(a,a),X0) = multiply(c,multiply(multiply(c,d),X0)),
inference(superposition,[],[f1414,f2381]) ).
fof(f2454,plain,
! [X0] : multiply(multiply(a,a),X0) = multiply(c,multiply(c,multiply(d,X0))),
inference(forward_demodulation,[],[f2453,f1414]) ).
fof(f2456,plain,
! [X0] : multiply(a,multiply(a,X0)) = multiply(c,multiply(c,multiply(d,X0))),
inference(forward_demodulation,[],[f2454,f1414]) ).
fof(f2458,plain,
multiply(d,multiply(h,d)) = multiply(k,b),
inference(superposition,[],[f1584,f2349]) ).
fof(f2465,plain,
! [X0] : multiply(b,X0) = multiply(h,multiply(multiply(h,d),X0)),
inference(superposition,[],[f1414,f2349]) ).
fof(f2466,plain,
! [X0] : multiply(b,X0) = multiply(h,multiply(h,multiply(d,X0))),
inference(forward_demodulation,[],[f2465,f1414]) ).
fof(f2475,plain,
! [X0] : multiply(d,multiply(multiply(h,d),X0)) = multiply(multiply(k,b),X0),
inference(superposition,[],[f1414,f2458]) ).
fof(f2476,plain,
! [X0] : multiply(d,multiply(multiply(h,d),X0)) = multiply(k,multiply(b,X0)),
inference(forward_demodulation,[],[f2475,f1414]) ).
fof(f2478,plain,
! [X0] : multiply(k,multiply(b,X0)) = multiply(d,multiply(h,multiply(d,X0))),
inference(forward_demodulation,[],[f2476,f1414]) ).
fof(f2486,plain,
! [X0] : multiply(multiply(b,b),X0) = multiply(d,multiply(multiply(d,h),X0)),
inference(superposition,[],[f1414,f2351]) ).
fof(f2487,plain,
! [X0] : multiply(multiply(b,b),X0) = multiply(d,multiply(d,multiply(h,X0))),
inference(forward_demodulation,[],[f2486,f1414]) ).
fof(f2489,plain,
! [X0] : multiply(b,multiply(b,X0)) = multiply(d,multiply(d,multiply(h,X0))),
inference(forward_demodulation,[],[f2487,f1414]) ).
fof(f3750,plain,
multiply(c,multiply(c,h)) = multiply(a,multiply(a,multiply(b,b))),
inference(superposition,[],[f2456,f696]) ).
fof(f3752,plain,
multiply(a,multiply(a,multiply(d,h))) = multiply(c,multiply(c,multiply(b,b))),
inference(superposition,[],[f2456,f2351]) ).
fof(f3754,plain,
multiply(a,multiply(a,multiply(h,h))) = multiply(c,multiply(c,k)),
inference(superposition,[],[f2456,f607]) ).
fof(f3777,plain,
multiply(c,a) = multiply(a,multiply(a,multiply(d,h))),
inference(forward_demodulation,[],[f3752,f1102]) ).
fof(f3778,plain,
multiply(c,multiply(c,h)) = multiply(a,multiply(c,b)),
inference(forward_demodulation,[],[f3750,f1582]) ).
fof(f3819,plain,
! [X0] : multiply(a,multiply(multiply(a,multiply(d,h)),X0)) = multiply(multiply(c,a),X0),
inference(superposition,[],[f1414,f3777]) ).
fof(f3822,plain,
! [X0] : multiply(a,multiply(multiply(a,multiply(d,h)),X0)) = multiply(c,multiply(a,X0)),
inference(forward_demodulation,[],[f3819,f1414]) ).
fof(f3825,plain,
! [X0] : multiply(c,multiply(a,X0)) = multiply(a,multiply(a,multiply(multiply(d,h),X0))),
inference(forward_demodulation,[],[f3822,f1414]) ).
fof(f3827,plain,
! [X0] : multiply(c,multiply(a,X0)) = multiply(a,multiply(a,multiply(d,multiply(h,X0)))),
inference(forward_demodulation,[],[f3825,f1414]) ).
fof(f3848,plain,
multiply(d,b) = multiply(c,multiply(a,c)),
inference(superposition,[],[f1581,f2357]) ).
fof(f3856,plain,
! [X0] : multiply(b,X0) = multiply(a,multiply(multiply(a,c),X0)),
inference(superposition,[],[f1414,f2357]) ).
fof(f3860,plain,
! [X0] : multiply(b,X0) = multiply(a,multiply(a,multiply(c,X0))),
inference(forward_demodulation,[],[f3856,f1414]) ).
fof(f3870,plain,
! [X0] : multiply(multiply(d,b),X0) = multiply(c,multiply(multiply(a,c),X0)),
inference(superposition,[],[f1414,f3848]) ).
fof(f3873,plain,
! [X0] : multiply(multiply(d,b),X0) = multiply(c,multiply(a,multiply(c,X0))),
inference(forward_demodulation,[],[f3870,f1414]) ).
fof(f3875,plain,
! [X0] : multiply(d,multiply(b,X0)) = multiply(c,multiply(a,multiply(c,X0))),
inference(forward_demodulation,[],[f3873,f1414]) ).
fof(f3997,plain,
multiply(c,multiply(a,multiply(h,h))) = multiply(d,multiply(c,multiply(c,k))),
inference(superposition,[],[f1581,f3754]) ).
fof(f4010,plain,
multiply(c,multiply(a,multiply(h,h))) = multiply(c,multiply(b,multiply(c,k))),
inference(forward_demodulation,[],[f3997,f1754]) ).
fof(f4053,plain,
h = multiply(inverse(multiply(d,h)),k),
inference(resolution,[],[f1061,f404]) ).
fof(f4062,plain,
h = multiply(multiply(d,h),multiply(multiply(d,h),k)),
inference(forward_demodulation,[],[f4053,f1566]) ).
fof(f4071,plain,
h = multiply(d,multiply(h,multiply(multiply(d,h),k))),
inference(forward_demodulation,[],[f4062,f1414]) ).
fof(f4076,plain,
h = multiply(d,multiply(h,multiply(d,multiply(h,k)))),
inference(forward_demodulation,[],[f4071,f1414]) ).
fof(f4079,plain,
h = multiply(k,multiply(b,multiply(h,k))),
inference(forward_demodulation,[],[f4076,f2478]) ).
fof(f4082,plain,
multiply(d,multiply(d,h)) = multiply(h,multiply(h,multiply(b,multiply(h,k)))),
inference(superposition,[],[f2445,f4079]) ).
fof(f4090,plain,
! [X0] : multiply(h,X0) = multiply(k,multiply(multiply(b,multiply(h,k)),X0)),
inference(superposition,[],[f1414,f4079]) ).
fof(f4094,plain,
! [X0] : multiply(h,X0) = multiply(k,multiply(b,multiply(multiply(h,k),X0))),
inference(forward_demodulation,[],[f4090,f1414]) ).
fof(f4096,plain,
multiply(d,multiply(d,h)) = multiply(h,multiply(d,multiply(h,k))),
inference(forward_demodulation,[],[f4082,f1583]) ).
fof(f4097,plain,
! [X0] : multiply(h,X0) = multiply(k,multiply(b,multiply(h,multiply(k,X0)))),
inference(forward_demodulation,[],[f4094,f1414]) ).
fof(f4099,plain,
multiply(b,b) = multiply(h,multiply(d,multiply(h,k))),
inference(forward_demodulation,[],[f4096,f2351]) ).
fof(f4508,plain,
multiply(d,k) = multiply(b,multiply(b,h)),
inference(superposition,[],[f2489,f607]) ).
fof(f4509,plain,
multiply(b,multiply(b,d)) = multiply(d,multiply(k,b)),
inference(superposition,[],[f2489,f2458]) ).
fof(f4547,plain,
multiply(a,h) = multiply(c,multiply(d,k)),
inference(superposition,[],[f1659,f4508]) ).
fof(f4550,plain,
multiply(d,multiply(b,h)) = multiply(h,multiply(d,k)),
inference(superposition,[],[f1583,f4508]) ).
fof(f4566,plain,
multiply(a,multiply(a,k)) = multiply(c,multiply(a,h)),
inference(superposition,[],[f2456,f4547]) ).
fof(f4685,plain,
multiply(d,multiply(d,multiply(h,k))) = multiply(k,multiply(b,b)),
inference(superposition,[],[f1584,f4099]) ).
fof(f4699,plain,
multiply(k,multiply(b,b)) = multiply(b,multiply(b,k)),
inference(forward_demodulation,[],[f4685,f2489]) ).
fof(f5345,plain,
! [X0] : multiply(d,multiply(multiply(b,h),X0)) = multiply(multiply(h,multiply(d,k)),X0),
inference(superposition,[],[f1414,f4550]) ).
fof(f5351,plain,
! [X0] : multiply(d,multiply(multiply(b,h),X0)) = multiply(h,multiply(multiply(d,k),X0)),
inference(forward_demodulation,[],[f5345,f1414]) ).
fof(f5354,plain,
! [X0] : multiply(d,multiply(multiply(b,h),X0)) = multiply(h,multiply(d,multiply(k,X0))),
inference(forward_demodulation,[],[f5351,f1414]) ).
fof(f5356,plain,
! [X0] : multiply(d,multiply(b,multiply(h,X0))) = multiply(h,multiply(d,multiply(k,X0))),
inference(forward_demodulation,[],[f5354,f1414]) ).
fof(f6129,plain,
multiply(h,multiply(h,multiply(b,b))) = multiply(d,multiply(d,multiply(b,multiply(b,k)))),
inference(superposition,[],[f2445,f4699]) ).
fof(f6132,plain,
product(k,multiply(b,b),multiply(b,multiply(b,k))),
inference(superposition,[],[f5,f4699]) ).
fof(f6139,plain,
! [X0] : multiply(k,multiply(multiply(b,b),X0)) = multiply(multiply(b,multiply(b,k)),X0),
inference(superposition,[],[f1414,f4699]) ).
fof(f6148,plain,
! [X0] : multiply(k,multiply(multiply(b,b),X0)) = multiply(b,multiply(multiply(b,k),X0)),
inference(forward_demodulation,[],[f6139,f1414]) ).
fof(f6152,plain,
multiply(d,multiply(h,k)) = multiply(h,multiply(h,multiply(b,b))),
inference(forward_demodulation,[],[f6129,f1642]) ).
fof(f6153,plain,
! [X0] : multiply(k,multiply(multiply(b,b),X0)) = multiply(b,multiply(b,multiply(k,X0))),
inference(forward_demodulation,[],[f6148,f1414]) ).
fof(f6154,plain,
multiply(d,multiply(h,k)) = multiply(h,multiply(d,b)),
inference(forward_demodulation,[],[f6152,f1583]) ).
fof(f6155,plain,
! [X0] : multiply(k,multiply(b,multiply(b,X0))) = multiply(b,multiply(b,multiply(k,X0))),
inference(forward_demodulation,[],[f6153,f1414]) ).
fof(f6181,plain,
multiply(k,multiply(b,b)) = multiply(d,multiply(b,multiply(d,h))),
inference(superposition,[],[f1696,f2351]) ).
fof(f6187,plain,
multiply(d,multiply(b,multiply(k,b))) = multiply(k,multiply(b,multiply(b,d))),
inference(superposition,[],[f1696,f4509]) ).
fof(f6190,plain,
multiply(d,multiply(b,a)) = multiply(k,c),
inference(superposition,[],[f1696,f413]) ).
fof(f6191,plain,
multiply(d,multiply(b,c)) = multiply(k,multiply(c,b)),
inference(superposition,[],[f1696,f1726]) ).
fof(f6219,plain,
multiply(d,multiply(b,multiply(k,b))) = multiply(b,multiply(b,multiply(k,d))),
inference(forward_demodulation,[],[f6187,f6155]) ).
fof(f6225,plain,
multiply(b,multiply(b,k)) = multiply(d,multiply(b,multiply(d,h))),
inference(forward_demodulation,[],[f6181,f4699]) ).
fof(f6237,plain,
multiply(d,multiply(b,multiply(k,b))) = multiply(b,multiply(b,multiply(d,b))),
inference(forward_demodulation,[],[f6219,f1670]) ).
fof(f6246,plain,
multiply(d,multiply(b,multiply(b,a))) = multiply(k,multiply(k,c)),
inference(superposition,[],[f1696,f6190]) ).
fof(f6270,plain,
multiply(k,multiply(k,c)) = multiply(h,a),
inference(forward_demodulation,[],[f6246,f1642]) ).
fof(f6351,plain,
b = multiply(inverse(multiply(d,b)),h),
inference(resolution,[],[f1472,f404]) ).
fof(f6363,plain,
b = multiply(multiply(d,b),multiply(multiply(d,b),h)),
inference(forward_demodulation,[],[f6351,f1566]) ).
fof(f6372,plain,
b = multiply(d,multiply(b,multiply(multiply(d,b),h))),
inference(forward_demodulation,[],[f6363,f1414]) ).
fof(f6377,plain,
b = multiply(d,multiply(b,multiply(d,multiply(b,h)))),
inference(forward_demodulation,[],[f6372,f1414]) ).
fof(f6379,plain,
b = multiply(d,multiply(b,multiply(h,multiply(d,k)))),
inference(forward_demodulation,[],[f6377,f4550]) ).
fof(f6381,plain,
b = multiply(h,multiply(d,multiply(k,multiply(d,k)))),
inference(forward_demodulation,[],[f6379,f5356]) ).
fof(f6383,plain,
b = multiply(h,inverse(multiply(d,k))),
inference(forward_demodulation,[],[f6381,f1601]) ).
fof(f6387,plain,
multiply(k,b) = multiply(d,inverse(multiply(d,k))),
inference(superposition,[],[f1584,f6383]) ).
fof(f6447,plain,
! [X0] : multiply(multiply(k,b),X0) = multiply(d,multiply(inverse(multiply(d,k)),X0)),
inference(superposition,[],[f1414,f6387]) ).
fof(f6456,plain,
! [X0] : multiply(multiply(k,b),X0) = multiply(d,multiply(multiply(d,k),multiply(multiply(d,k),X0))),
inference(forward_demodulation,[],[f6447,f1566]) ).
fof(f6463,plain,
! [X0] : multiply(multiply(k,b),X0) = multiply(d,multiply(d,multiply(k,multiply(multiply(d,k),X0)))),
inference(forward_demodulation,[],[f6456,f1414]) ).
fof(f6467,plain,
! [X0] : multiply(multiply(k,b),X0) = multiply(h,multiply(h,multiply(multiply(d,k),X0))),
inference(forward_demodulation,[],[f6463,f2445]) ).
fof(f6471,plain,
! [X0] : multiply(multiply(k,b),X0) = multiply(h,multiply(h,multiply(d,multiply(k,X0)))),
inference(forward_demodulation,[],[f6467,f1414]) ).
fof(f6475,plain,
! [X0] : multiply(multiply(k,b),X0) = multiply(b,multiply(k,X0)),
inference(forward_demodulation,[],[f6471,f2466]) ).
fof(f6478,plain,
! [X0] : multiply(k,multiply(b,X0)) = multiply(b,multiply(k,X0)),
inference(forward_demodulation,[],[f6475,f1414]) ).
fof(f6480,plain,
! [X0] : multiply(d,multiply(h,multiply(d,X0))) = multiply(b,multiply(k,X0)),
inference(backward_demodulation,[],[f2478,f6478]) ).
fof(f6484,plain,
! [X0] : multiply(h,X0) = multiply(b,multiply(k,multiply(h,multiply(k,X0)))),
inference(backward_demodulation,[],[f4097,f6478]) ).
fof(f6488,plain,
multiply(b,multiply(b,k)) = multiply(b,multiply(k,b)),
inference(backward_demodulation,[],[f4699,f6478]) ).
fof(f6523,plain,
multiply(d,multiply(b,multiply(b,k))) = multiply(b,multiply(b,multiply(d,b))),
inference(backward_demodulation,[],[f6237,f6488]) ).
fof(f6527,plain,
! [X0] : multiply(h,X0) = multiply(b,multiply(d,multiply(k,X0))),
inference(forward_demodulation,[],[f6484,f1584]) ).
fof(f6547,plain,
multiply(h,k) = multiply(b,multiply(b,multiply(d,b))),
inference(forward_demodulation,[],[f6523,f1642]) ).
fof(f6901,plain,
multiply(h,multiply(k,c)) = multiply(b,multiply(d,multiply(h,a))),
inference(superposition,[],[f6527,f6270]) ).
fof(f6906,plain,
multiply(h,h) = multiply(b,multiply(d,d)),
inference(superposition,[],[f6527,f539]) ).
fof(f6975,plain,
multiply(c,multiply(d,d)) = multiply(a,multiply(h,h)),
inference(superposition,[],[f1582,f6906]) ).
fof(f7247,plain,
multiply(d,multiply(h,k)) = multiply(b,multiply(k,multiply(h,h))),
inference(superposition,[],[f6480,f607]) ).
fof(f7254,plain,
multiply(b,multiply(k,a)) = multiply(d,multiply(h,c)),
inference(superposition,[],[f6480,f413]) ).
fof(f7289,plain,
multiply(d,multiply(h,k)) = multiply(b,multiply(d,h)),
inference(forward_demodulation,[],[f7247,f1584]) ).
fof(f7314,plain,
multiply(h,multiply(d,b)) = multiply(b,multiply(d,h)),
inference(backward_demodulation,[],[f6154,f7289]) ).
fof(f7402,plain,
multiply(b,multiply(k,multiply(h,c))) = multiply(d,multiply(h,multiply(b,multiply(k,a)))),
inference(superposition,[],[f6480,f7254]) ).
fof(f7428,plain,
multiply(b,multiply(k,multiply(h,c))) = multiply(d,multiply(d,multiply(k,a))),
inference(forward_demodulation,[],[f7402,f1583]) ).
fof(f7435,plain,
multiply(b,multiply(k,multiply(h,c))) = multiply(h,multiply(h,a)),
inference(forward_demodulation,[],[f7428,f2445]) ).
fof(f7437,plain,
multiply(h,multiply(h,a)) = multiply(b,multiply(d,c)),
inference(forward_demodulation,[],[f7435,f1584]) ).
fof(f7438,plain,
multiply(h,multiply(h,a)) = multiply(b,multiply(c,b)),
inference(forward_demodulation,[],[f7437,f1726]) ).
fof(f7874,plain,
multiply(a,multiply(d,b)) = multiply(c,multiply(h,k)),
inference(superposition,[],[f1659,f6547]) ).
fof(f7877,plain,
multiply(c,multiply(b,multiply(d,b))) = multiply(a,multiply(h,k)),
inference(superposition,[],[f1582,f6547]) ).
fof(f8099,plain,
! [X0] : multiply(c,multiply(multiply(a,h),X0)) = multiply(multiply(a,multiply(a,k)),X0),
inference(superposition,[],[f1414,f4566]) ).
fof(f8108,plain,
! [X0] : multiply(c,multiply(multiply(a,h),X0)) = multiply(a,multiply(multiply(a,k),X0)),
inference(forward_demodulation,[],[f8099,f1414]) ).
fof(f8111,plain,
! [X0] : multiply(c,multiply(multiply(a,h),X0)) = multiply(a,multiply(a,multiply(k,X0))),
inference(forward_demodulation,[],[f8108,f1414]) ).
fof(f8112,plain,
! [X0] : multiply(c,multiply(a,multiply(h,X0))) = multiply(a,multiply(a,multiply(k,X0))),
inference(forward_demodulation,[],[f8111,f1414]) ).
fof(f8113,plain,
multiply(c,multiply(b,multiply(c,k))) = multiply(a,multiply(a,multiply(k,h))),
inference(backward_demodulation,[],[f4010,f8112]) ).
fof(f8117,plain,
multiply(a,multiply(a,d)) = multiply(c,multiply(b,multiply(c,k))),
inference(forward_demodulation,[],[f8113,f539]) ).
fof(f8904,plain,
! [X0] : multiply(c,multiply(multiply(b,multiply(c,k)),X0)) = multiply(multiply(a,multiply(a,d)),X0),
inference(superposition,[],[f1414,f8117]) ).
fof(f8915,plain,
! [X0] : multiply(c,multiply(multiply(b,multiply(c,k)),X0)) = multiply(a,multiply(multiply(a,d),X0)),
inference(forward_demodulation,[],[f8904,f1414]) ).
fof(f8920,plain,
! [X0] : multiply(a,multiply(a,multiply(d,X0))) = multiply(c,multiply(multiply(b,multiply(c,k)),X0)),
inference(forward_demodulation,[],[f8915,f1414]) ).
fof(f8923,plain,
! [X0] : multiply(a,multiply(a,multiply(d,X0))) = multiply(c,multiply(b,multiply(multiply(c,k),X0))),
inference(forward_demodulation,[],[f8920,f1414]) ).
fof(f8924,plain,
! [X0] : multiply(a,multiply(a,multiply(d,X0))) = multiply(c,multiply(b,multiply(c,multiply(k,X0)))),
inference(forward_demodulation,[],[f8923,f1414]) ).
fof(f8961,plain,
multiply(d,multiply(h,a)) = multiply(k,multiply(b,multiply(c,b))),
inference(superposition,[],[f1584,f7438]) ).
fof(f8986,plain,
multiply(d,multiply(h,a)) = multiply(b,multiply(k,multiply(c,b))),
inference(forward_demodulation,[],[f8961,f6478]) ).
fof(f8990,plain,
multiply(d,multiply(h,a)) = multiply(b,multiply(d,multiply(b,c))),
inference(forward_demodulation,[],[f8986,f6191]) ).
fof(f9338,plain,
! [X0] : multiply(c,multiply(multiply(h,k),X0)) = multiply(multiply(a,multiply(d,b)),X0),
inference(superposition,[],[f1414,f7874]) ).
fof(f9350,plain,
! [X0] : multiply(c,multiply(multiply(h,k),X0)) = multiply(a,multiply(multiply(d,b),X0)),
inference(forward_demodulation,[],[f9338,f1414]) ).
fof(f9353,plain,
! [X0] : multiply(c,multiply(multiply(h,k),X0)) = multiply(a,multiply(d,multiply(b,X0))),
inference(forward_demodulation,[],[f9350,f1414]) ).
fof(f9354,plain,
! [X0] : multiply(c,multiply(h,multiply(k,X0))) = multiply(a,multiply(d,multiply(b,X0))),
inference(forward_demodulation,[],[f9353,f1414]) ).
fof(f9363,plain,
! [X2,X0,X1] : inverse(multiply(X0,X1)) = multiply(X2,inverse(multiply(X0,multiply(X1,X2)))),
inference(superposition,[],[f2367,f1414]) ).
fof(f9409,plain,
inverse(d) = multiply(multiply(h,c),inverse(multiply(b,multiply(k,a)))),
inference(superposition,[],[f2367,f7254]) ).
fof(f9424,plain,
inverse(d) = multiply(a,inverse(c)),
inference(superposition,[],[f2367,f413]) ).
fof(f9472,plain,
! [X0] : multiply(a,multiply(a,inverse(multiply(X0,d)))) = multiply(c,multiply(c,inverse(X0))),
inference(superposition,[],[f2456,f2367]) ).
fof(f9527,plain,
inverse(d) = multiply(a,multiply(c,c)),
inference(forward_demodulation,[],[f9424,f483]) ).
fof(f9542,plain,
inverse(d) = multiply(h,multiply(c,inverse(multiply(b,multiply(k,a))))),
inference(forward_demodulation,[],[f9409,f1414]) ).
fof(f9610,plain,
multiply(d,d) = multiply(a,multiply(c,c)),
inference(forward_demodulation,[],[f9527,f483]) ).
fof(f9625,plain,
multiply(d,d) = multiply(h,multiply(c,inverse(multiply(b,multiply(k,a))))),
inference(forward_demodulation,[],[f9542,f483]) ).
fof(f10582,plain,
! [X0] : multiply(b,inverse(multiply(X0,c))) = multiply(a,multiply(a,inverse(X0))),
inference(superposition,[],[f3860,f2367]) ).
fof(f10583,plain,
multiply(b,multiply(a,a)) = multiply(a,multiply(a,d)),
inference(superposition,[],[f3860,f694]) ).
fof(f10585,plain,
multiply(b,multiply(a,h)) = multiply(a,multiply(a,multiply(a,multiply(a,k)))),
inference(superposition,[],[f3860,f4566]) ).
fof(f10592,plain,
multiply(a,multiply(a,multiply(a,a))) = multiply(b,multiply(c,d)),
inference(superposition,[],[f3860,f2381]) ).
fof(f10593,plain,
multiply(b,multiply(c,h)) = multiply(a,multiply(a,multiply(a,multiply(c,b)))),
inference(superposition,[],[f3860,f3778]) ).
fof(f10598,plain,
multiply(a,multiply(d,d)) = multiply(b,c),
inference(superposition,[],[f3860,f9610]) ).
fof(f10644,plain,
multiply(c,b) = multiply(b,multiply(c,h)),
inference(forward_demodulation,[],[f10593,f1512]) ).
fof(f10645,plain,
a = multiply(b,multiply(c,d)),
inference(forward_demodulation,[],[f10592,f1512]) ).
fof(f10652,plain,
multiply(a,k) = multiply(b,multiply(a,h)),
inference(forward_demodulation,[],[f10585,f1512]) ).
fof(f10653,plain,
multiply(b,multiply(a,a)) = multiply(c,multiply(b,multiply(c,k))),
inference(backward_demodulation,[],[f8117,f10583]) ).
fof(f10668,plain,
! [X0] : multiply(c,multiply(c,inverse(X0))) = multiply(b,inverse(multiply(multiply(X0,d),c))),
inference(backward_demodulation,[],[f9472,f10582]) ).
fof(f10709,plain,
! [X0] : multiply(c,multiply(c,inverse(X0))) = multiply(b,inverse(multiply(X0,multiply(d,c)))),
inference(forward_demodulation,[],[f10668,f1414]) ).
fof(f10719,plain,
! [X0] : multiply(c,multiply(c,inverse(X0))) = multiply(b,inverse(multiply(X0,multiply(c,b)))),
inference(forward_demodulation,[],[f10709,f1726]) ).
fof(f10721,plain,
! [X0] : inverse(multiply(X0,c)) = multiply(c,multiply(c,inverse(X0))),
inference(forward_demodulation,[],[f10719,f9363]) ).
fof(f10729,plain,
multiply(h,a) = multiply(d,multiply(c,d)),
inference(superposition,[],[f1583,f10645]) ).
fof(f10759,plain,
multiply(h,a) = multiply(c,multiply(b,d)),
inference(forward_demodulation,[],[f10729,f1754]) ).
fof(f10775,plain,
multiply(c,d) = inverse(multiply(a,c)),
inference(superposition,[],[f10721,f409]) ).
fof(f10898,plain,
multiply(a,c) = inverse(multiply(c,d)),
inference(superposition,[],[f495,f10775]) ).
fof(f10913,plain,
! [X0] : multiply(multiply(c,d),X0) = multiply(multiply(a,c),multiply(multiply(a,c),X0)),
inference(superposition,[],[f1566,f10775]) ).
fof(f10923,plain,
! [X0] : multiply(multiply(c,d),X0) = multiply(a,multiply(c,multiply(multiply(a,c),X0))),
inference(forward_demodulation,[],[f10913,f1414]) ).
fof(f10943,plain,
! [X0] : multiply(multiply(c,d),X0) = multiply(a,multiply(c,multiply(a,multiply(c,X0)))),
inference(forward_demodulation,[],[f10923,f1414]) ).
fof(f10955,plain,
! [X0] : multiply(multiply(c,d),X0) = multiply(a,multiply(d,multiply(b,X0))),
inference(forward_demodulation,[],[f10943,f3875]) ).
fof(f10962,plain,
! [X0] : multiply(c,multiply(d,X0)) = multiply(a,multiply(d,multiply(b,X0))),
inference(forward_demodulation,[],[f10955,f1414]) ).
fof(f10963,plain,
! [X0] : multiply(c,multiply(d,X0)) = multiply(c,multiply(h,multiply(k,X0))),
inference(backward_demodulation,[],[f9354,f10962]) ).
fof(f11122,plain,
multiply(d,multiply(a,h)) = multiply(h,multiply(a,k)),
inference(superposition,[],[f1583,f10652]) ).
fof(f11133,plain,
! [X0] : multiply(multiply(a,k),X0) = multiply(b,multiply(multiply(a,h),X0)),
inference(superposition,[],[f1414,f10652]) ).
fof(f11147,plain,
! [X0] : multiply(multiply(a,k),X0) = multiply(b,multiply(a,multiply(h,X0))),
inference(forward_demodulation,[],[f11133,f1414]) ).
fof(f11150,plain,
multiply(c,h) = multiply(h,multiply(a,k)),
inference(forward_demodulation,[],[f11122,f1581]) ).
fof(f11152,plain,
! [X0] : multiply(a,multiply(k,X0)) = multiply(b,multiply(a,multiply(h,X0))),
inference(forward_demodulation,[],[f11147,f1414]) ).
fof(f11161,plain,
multiply(c,multiply(d,d)) = multiply(d,multiply(b,c)),
inference(superposition,[],[f1581,f10598]) ).
fof(f11194,plain,
multiply(a,multiply(h,h)) = multiply(d,multiply(b,c)),
inference(forward_demodulation,[],[f11161,f6975]) ).
fof(f11200,plain,
multiply(d,multiply(h,a)) = multiply(b,multiply(a,multiply(h,h))),
inference(backward_demodulation,[],[f8990,f11194]) ).
fof(f11239,plain,
multiply(d,multiply(h,a)) = multiply(a,multiply(k,h)),
inference(forward_demodulation,[],[f11200,f11152]) ).
fof(f11254,plain,
multiply(a,d) = multiply(d,multiply(h,a)),
inference(forward_demodulation,[],[f11239,f539]) ).
fof(f11269,plain,
multiply(h,multiply(k,c)) = multiply(b,multiply(a,d)),
inference(backward_demodulation,[],[f6901,f11254]) ).
fof(f11463,plain,
! [X0] : multiply(c,multiply(multiply(b,multiply(c,k)),X0)) = multiply(multiply(b,multiply(a,a)),X0),
inference(superposition,[],[f1414,f10653]) ).
fof(f11477,plain,
! [X0] : multiply(c,multiply(multiply(b,multiply(c,k)),X0)) = multiply(b,multiply(multiply(a,a),X0)),
inference(forward_demodulation,[],[f11463,f1414]) ).
fof(f11484,plain,
! [X0] : multiply(c,multiply(multiply(b,multiply(c,k)),X0)) = multiply(b,multiply(a,multiply(a,X0))),
inference(forward_demodulation,[],[f11477,f1414]) ).
fof(f11491,plain,
! [X0] : multiply(c,multiply(b,multiply(multiply(c,k),X0))) = multiply(b,multiply(a,multiply(a,X0))),
inference(forward_demodulation,[],[f11484,f1414]) ).
fof(f11495,plain,
! [X0] : multiply(c,multiply(b,multiply(c,multiply(k,X0)))) = multiply(b,multiply(a,multiply(a,X0))),
inference(forward_demodulation,[],[f11491,f1414]) ).
fof(f11496,plain,
! [X0] : multiply(a,multiply(a,multiply(d,X0))) = multiply(b,multiply(a,multiply(a,X0))),
inference(backward_demodulation,[],[f8924,f11495]) ).
fof(f11501,plain,
! [X0] : multiply(c,multiply(a,X0)) = multiply(b,multiply(a,multiply(a,multiply(h,X0)))),
inference(backward_demodulation,[],[f3827,f11496]) ).
fof(f11503,plain,
multiply(c,a) = multiply(b,multiply(a,multiply(a,h))),
inference(backward_demodulation,[],[f3777,f11496]) ).
fof(f11507,plain,
multiply(a,multiply(c,a)) = multiply(c,multiply(a,multiply(a,h))),
inference(superposition,[],[f1582,f11503]) ).
fof(f11539,plain,
multiply(d,h) = multiply(a,multiply(c,a)),
inference(forward_demodulation,[],[f11507,f1641]) ).
fof(f11574,plain,
multiply(a,multiply(d,h)) = multiply(b,a),
inference(superposition,[],[f3860,f11539]) ).
fof(f11628,plain,
multiply(d,multiply(b,a)) = multiply(c,multiply(d,h)),
inference(superposition,[],[f1581,f11574]) ).
fof(f11657,plain,
multiply(k,c) = multiply(c,multiply(d,h)),
inference(forward_demodulation,[],[f11628,f6190]) ).
fof(f11822,plain,
! [X0] : multiply(multiply(h,a),X0) = multiply(c,multiply(multiply(b,d),X0)),
inference(superposition,[],[f1414,f10759]) ).
fof(f11836,plain,
! [X0] : multiply(multiply(h,a),X0) = multiply(c,multiply(b,multiply(d,X0))),
inference(forward_demodulation,[],[f11822,f1414]) ).
fof(f11841,plain,
! [X0] : multiply(h,multiply(a,X0)) = multiply(c,multiply(b,multiply(d,X0))),
inference(forward_demodulation,[],[f11836,f1414]) ).
fof(f11846,plain,
multiply(a,multiply(h,k)) = multiply(h,multiply(a,b)),
inference(backward_demodulation,[],[f7877,f11841]) ).
fof(f11848,plain,
multiply(h,c) = multiply(a,multiply(h,k)),
inference(forward_demodulation,[],[f11846,f408]) ).
fof(f11850,plain,
multiply(d,multiply(h,c)) = multiply(c,multiply(h,k)),
inference(superposition,[],[f1581,f11848]) ).
fof(f11861,plain,
! [X0] : multiply(multiply(h,c),X0) = multiply(a,multiply(multiply(h,k),X0)),
inference(superposition,[],[f1414,f11848]) ).
fof(f11875,plain,
! [X0] : multiply(multiply(h,c),X0) = multiply(a,multiply(h,multiply(k,X0))),
inference(forward_demodulation,[],[f11861,f1414]) ).
fof(f11878,plain,
multiply(d,multiply(h,c)) = multiply(a,multiply(d,b)),
inference(forward_demodulation,[],[f11850,f7874]) ).
fof(f11880,plain,
! [X0] : multiply(h,multiply(c,X0)) = multiply(a,multiply(h,multiply(k,X0))),
inference(forward_demodulation,[],[f11875,f1414]) ).
fof(f11881,plain,
multiply(b,multiply(k,a)) = multiply(a,multiply(d,b)),
inference(forward_demodulation,[],[f11878,f7254]) ).
fof(f11886,plain,
multiply(b,multiply(k,a)) = multiply(c,multiply(h,k)),
inference(backward_demodulation,[],[f7874,f11881]) ).
fof(f11924,plain,
multiply(b,multiply(a,multiply(a,multiply(h,k)))) = multiply(a,multiply(a,multiply(b,multiply(d,h)))),
inference(superposition,[],[f11496,f7289]) ).
fof(f11968,plain,
multiply(a,multiply(c,multiply(d,h))) = multiply(b,multiply(a,multiply(a,multiply(h,k)))),
inference(forward_demodulation,[],[f11924,f1582]) ).
fof(f12003,plain,
multiply(a,multiply(c,multiply(d,h))) = multiply(c,multiply(a,k)),
inference(forward_demodulation,[],[f11968,f11501]) ).
fof(f12032,plain,
multiply(a,multiply(k,c)) = multiply(c,multiply(a,k)),
inference(forward_demodulation,[],[f12003,f11657]) ).
fof(f12207,plain,
multiply(b,multiply(a,k)) = multiply(a,multiply(a,multiply(a,multiply(k,c)))),
inference(superposition,[],[f3860,f12032]) ).
fof(f12235,plain,
multiply(k,c) = multiply(b,multiply(a,k)),
inference(forward_demodulation,[],[f12207,f1512]) ).
fof(f12244,plain,
multiply(k,multiply(k,c)) = multiply(b,multiply(k,multiply(a,k))),
inference(superposition,[],[f6478,f12235]) ).
fof(f12247,plain,
multiply(h,multiply(k,c)) = multiply(d,multiply(a,k)),
inference(superposition,[],[f1583,f12235]) ).
fof(f12275,plain,
multiply(c,k) = multiply(h,multiply(k,c)),
inference(forward_demodulation,[],[f12247,f1581]) ).
fof(f12277,plain,
multiply(h,a) = multiply(b,multiply(k,multiply(a,k))),
inference(forward_demodulation,[],[f12244,f6270]) ).
fof(f12280,plain,
multiply(c,k) = multiply(b,multiply(a,d)),
inference(backward_demodulation,[],[f11269,f12275]) ).
fof(f12289,plain,
multiply(d,multiply(a,d)) = multiply(h,multiply(c,k)),
inference(superposition,[],[f1583,f12280]) ).
fof(f12318,plain,
multiply(c,d) = multiply(h,multiply(c,k)),
inference(forward_demodulation,[],[f12289,f1581]) ).
fof(f12340,plain,
! [X0] : multiply(multiply(c,h),X0) = multiply(h,multiply(multiply(a,k),X0)),
inference(superposition,[],[f1414,f11150]) ).
fof(f12354,plain,
! [X0] : multiply(multiply(c,h),X0) = multiply(h,multiply(a,multiply(k,X0))),
inference(forward_demodulation,[],[f12340,f1414]) ).
fof(f12361,plain,
! [X0] : multiply(c,multiply(h,X0)) = multiply(h,multiply(a,multiply(k,X0))),
inference(forward_demodulation,[],[f12354,f1414]) ).
fof(f12405,plain,
! [X0] : multiply(multiply(b,multiply(k,a)),X0) = multiply(c,multiply(multiply(h,k),X0)),
inference(superposition,[],[f1414,f11886]) ).
fof(f12419,plain,
! [X0] : multiply(multiply(b,multiply(k,a)),X0) = multiply(c,multiply(h,multiply(k,X0))),
inference(forward_demodulation,[],[f12405,f1414]) ).
fof(f12426,plain,
! [X0] : multiply(c,multiply(d,X0)) = multiply(multiply(b,multiply(k,a)),X0),
inference(forward_demodulation,[],[f12419,f10963]) ).
fof(f12430,plain,
! [X0] : multiply(c,multiply(d,X0)) = multiply(b,multiply(multiply(k,a),X0)),
inference(forward_demodulation,[],[f12426,f1414]) ).
fof(f12432,plain,
! [X0] : multiply(c,multiply(d,X0)) = multiply(b,multiply(k,multiply(a,X0))),
inference(forward_demodulation,[],[f12430,f1414]) ).
fof(f12440,plain,
multiply(c,multiply(d,k)) = multiply(h,a),
inference(backward_demodulation,[],[f12277,f12432]) ).
fof(f12441,plain,
multiply(a,h) = multiply(h,a),
inference(backward_demodulation,[],[f4547,f12440]) ).
fof(f12548,plain,
multiply(c,h) = multiply(d,multiply(h,a)),
inference(superposition,[],[f1581,f12441]) ).
fof(f12558,plain,
! [X0] : multiply(a,multiply(h,X0)) = multiply(multiply(h,a),X0),
inference(superposition,[],[f1414,f12441]) ).
fof(f12572,plain,
! [X0] : multiply(a,multiply(h,X0)) = multiply(h,multiply(a,X0)),
inference(forward_demodulation,[],[f12558,f1414]) ).
fof(f12575,plain,
multiply(a,d) = multiply(c,h),
inference(forward_demodulation,[],[f12548,f11254]) ).
fof(f12588,plain,
! [X0] : multiply(h,multiply(c,X0)) = multiply(h,multiply(a,multiply(k,X0))),
inference(backward_demodulation,[],[f11880,f12572]) ).
fof(f12615,plain,
multiply(c,b) = multiply(b,multiply(a,d)),
inference(backward_demodulation,[],[f10644,f12575]) ).
fof(f12668,plain,
! [X0] : multiply(c,multiply(h,X0)) = multiply(h,multiply(c,X0)),
inference(backward_demodulation,[],[f12361,f12588]) ).
fof(f12679,plain,
multiply(c,b) = multiply(c,k),
inference(backward_demodulation,[],[f12280,f12615]) ).
fof(f12695,plain,
multiply(b,multiply(k,a)) = multiply(h,multiply(c,k)),
inference(backward_demodulation,[],[f11886,f12668]) ).
fof(f12830,plain,
multiply(c,d) = multiply(h,multiply(c,b)),
inference(backward_demodulation,[],[f12318,f12679]) ).
fof(f12849,plain,
multiply(b,multiply(k,a)) = multiply(h,multiply(c,b)),
inference(forward_demodulation,[],[f12695,f12679]) ).
fof(f12906,plain,
multiply(c,d) = multiply(b,multiply(k,a)),
inference(forward_demodulation,[],[f12849,f12830]) ).
fof(f12935,plain,
multiply(d,d) = multiply(h,multiply(c,inverse(multiply(c,d)))),
inference(backward_demodulation,[],[f9625,f12906]) ).
fof(f12998,plain,
multiply(d,d) = multiply(h,multiply(c,multiply(a,c))),
inference(forward_demodulation,[],[f12935,f10898]) ).
fof(f13011,plain,
multiply(d,d) = multiply(h,multiply(d,b)),
inference(forward_demodulation,[],[f12998,f3848]) ).
fof(f13020,plain,
multiply(d,d) = multiply(b,multiply(d,h)),
inference(backward_demodulation,[],[f7314,f13011]) ).
fof(f13082,plain,
multiply(d,multiply(d,d)) = multiply(b,multiply(b,k)),
inference(backward_demodulation,[],[f6225,f13020]) ).
fof(f13139,plain,
identity = multiply(b,multiply(b,k)),
inference(forward_demodulation,[],[f13082,f370]) ).
fof(f13351,plain,
product(k,multiply(b,b),identity),
inference(backward_demodulation,[],[f6132,f13139]) ).
fof(f13447,plain,
$false,
inference(forward_subsumption_resolution,[],[f13351,f699]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP002-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.35 % Computer : n004.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 09:12:37 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.01/2.29 % (3231131)Input is clausal, will run a generic CNF schedule.
% 10.01/2.29 % (3231138)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=361519985:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.01/2.29 % (3231142)dis-21_1_sil=8000:lcm=predicate:random_seed=1020467724:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.01/2.29 % (3231136)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=1478134930:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.01/2.29 % (3231141)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2031379703:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.01/2.29 % (3231137)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=281964827:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.01/2.29 % (3231140)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4039740045:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.01/2.29 % (3231139)lrs+10_1_sil=8000:sp=occurrence:random_seed=3829875656:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.01/2.29 % (3231142)Instruction limit reached!
% 10.01/2.29 % (3231142)------------------------------
% 10.01/2.29 % (3231142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.01/2.29 % (3231142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/2.29 % (3231142)CaDiCaL version: 2.1.3
% 10.01/2.29 % (3231142)Termination reason: Instruction limit
% 10.01/2.29 % (3231142)Termination phase: Saturation
% 10.01/2.29 % (3231142)Time elapsed: 0.065 s
% 10.01/2.29 % (3231142)Peak memory usage: 88 MB
% 10.01/2.29 % (3231142)Instructions burned: 118 (million)
% 10.01/2.29 % (3231140)Instruction limit reached!
% 10.01/2.29 % (3231140)------------------------------
% 10.01/2.29 % (3231140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.01/2.29 % (3231140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/2.29 % (3231140)CaDiCaL version: 2.1.3
% 10.01/2.29 % (3231140)Termination reason: Instruction limit
% 10.01/2.29 % (3231140)Termination phase: Saturation
% 10.01/2.29 % (3231140)Time elapsed: 0.069 s
% 10.01/2.29 % (3231140)Peak memory usage: 88 MB
% 10.01/2.29 % (3231140)Instructions burned: 115 (million)
% 10.01/2.29 % (3231139)Instruction limit reached!
% 10.01/2.29 % (3231139)------------------------------
% 10.01/2.29 % (3231139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.01/2.29 % (3231139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/2.29 % (3231139)CaDiCaL version: 2.1.3
% 10.01/2.29 % (3231139)Termination reason: Instruction limit
% 10.01/2.29 % (3231139)Termination phase: Saturation
% 10.01/2.29 % (3231139)Time elapsed: 0.071 s
% 10.01/2.29 % (3231139)Peak memory usage: 88 MB
% 10.01/2.29 % (3231139)Instructions burned: 108 (million)
% 10.01/2.29 % (3231141)Instruction limit reached!
% 10.01/2.29 % (3231141)------------------------------
% 10.01/2.29 % (3231141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.01/2.29 % (3231141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/2.29 % (3231141)CaDiCaL version: 2.1.3
% 10.01/2.29 % (3231141)Termination reason: Instruction limit
% 10.01/2.29 % (3231141)Termination phase: Saturation
% 10.01/2.29 % (3231141)Time elapsed: 0.124 s
% 10.01/2.29 % (3231141)Peak memory usage: 89 MB
% 10.01/2.29 % (3231141)Instructions burned: 180 (million)
% 10.01/2.29 % (3231151)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3476920799:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 10.01/2.29 % (3231152)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3801723335:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.01/2.29 % (3231150)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1790433771:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.01/2.29 % (3231153)lrs+10_64_to=lpo:sil=8000:random_seed=1029647071:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 10.01/2.29 % (3231150)Instruction limit reached!
% 21.05/4.02 % (3231150)------------------------------
% 21.05/4.02 % (3231150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/4.02 % (3231150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/4.02 % (3231150)CaDiCaL version: 2.1.3
% 21.05/4.02 % (3231150)Termination reason: Instruction limit
% 21.05/4.02 % (3231150)Termination phase: Saturation
% 21.05/4.02 % (3231150)Time elapsed: 0.092 s
% 21.05/4.02 % (3231150)Peak memory usage: 89 MB
% 21.05/4.02 % (3231150)Instructions burned: 144 (million)
% 21.05/4.02 % (3231151)Instruction limit reached!
% 21.05/4.02 % (3231151)------------------------------
% 21.05/4.02 % (3231151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/4.02 % (3231151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/4.02 % (3231151)CaDiCaL version: 2.1.3
% 21.05/4.02 % (3231151)Termination reason: Instruction limit
% 21.05/4.02 % (3231151)Termination phase: Saturation
% 21.05/4.02 % (3231151)Time elapsed: 0.103 s
% 21.05/4.02 % (3231151)Peak memory usage: 89 MB
% 21.05/4.02 % (3231151)Instructions burned: 190 (million)
% 21.05/4.02 % (3231152)Instruction limit reached!
% 21.05/4.02 % (3231152)------------------------------
% 21.05/4.02 % (3231152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/4.02 % (3231152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/4.02 % (3231152)CaDiCaL version: 2.1.3
% 21.05/4.02 % (3231152)Termination reason: Instruction limit
% 21.05/4.02 % (3231152)Termination phase: Saturation
% 21.05/4.02 % (3231152)Time elapsed: 0.132 s
% 21.05/4.02 % (3231152)Peak memory usage: 89 MB
% 21.05/4.02 % (3231152)Instructions burned: 219 (million)
% 21.05/4.02 % (3231153)Instruction limit reached!
% 21.05/4.02 % (3231153)------------------------------
% 21.05/4.02 % (3231153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/4.02 % (3231153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/4.02 % (3231153)CaDiCaL version: 2.1.3
% 21.05/4.02 % (3231153)Termination reason: Instruction limit
% 21.05/4.02 % (3231153)Termination phase: Saturation
% 21.05/4.02 % (3231153)Time elapsed: 0.082 s
% 21.05/4.02 % (3231153)Peak memory usage: 88 MB
% 21.05/4.02 % (3231153)Instructions burned: 127 (million)
% 21.05/4.02 % (3231158)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1422344765:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 21.05/4.02 % (3231159)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=304317674:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 21.05/4.02 % (3231161)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2198370384:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 21.05/4.02 % (3231160)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1129851975:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 21.05/4.02 % (3231161)Instruction limit reached!
% 21.05/4.02 % (3231161)------------------------------
% 21.05/4.02 % (3231161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/4.02 % (3231161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/4.02 % (3231161)CaDiCaL version: 2.1.3
% 21.05/4.02 % (3231161)Termination reason: Instruction limit
% 21.05/4.02 % (3231161)Termination phase: Saturation
% 21.05/4.02 % (3231161)Time elapsed: 0.057 s
% 21.05/4.02 % (3231161)Peak memory usage: 88 MB
% 21.05/4.02 % (3231161)Instructions burned: 106 (million)
% 21.05/4.02 % (3231158)Instruction limit reached!
% 21.05/4.02 % (3231158)------------------------------
% 21.05/4.02 % (3231158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/4.02 % (3231158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/4.02 % (3231158)CaDiCaL version: 2.1.3
% 21.05/4.02 % (3231158)Termination reason: Instruction limit
% 21.05/4.02 % (3231158)Termination phase: Saturation
% 21.05/4.02 % (3231158)Time elapsed: 0.117 s
% 21.05/4.02 % (3231158)Peak memory usage: 89 MB
% 21.05/4.02 % (3231158)Instructions burned: 194 (million)
% 21.05/4.02 % (3231159)Instruction limit reached!
% 21.05/4.02 % (3231159)------------------------------
% 21.05/4.02 % (3231159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/4.02 % (3231159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/4.02 % (3231159)CaDiCaL version: 2.1.3
% 41.96/6.75 % (3231159)Termination reason: Instruction limit
% 41.96/6.75 % (3231159)Termination phase: Saturation
% 41.96/6.75 % (3231159)Time elapsed: 0.104 s
% 41.96/6.75 % (3231159)Peak memory usage: 90 MB
% 41.96/6.75 % (3231159)Instructions burned: 158 (million)
% 41.96/6.75 % (3231166)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1643310141:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 41.96/6.75 % (3231167)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3702068952:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 41.96/6.75 % (3231168)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3841877627:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 41.96/6.75 % (3231166)Instruction limit reached!
% 41.96/6.75 % (3231166)------------------------------
% 41.96/6.75 % (3231166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.96/6.75 % (3231166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.96/6.75 % (3231166)CaDiCaL version: 2.1.3
% 41.96/6.75 % (3231166)Termination reason: Instruction limit
% 41.96/6.75 % (3231166)Termination phase: Saturation
% 41.96/6.75 % (3231166)Time elapsed: 0.073 s
% 41.96/6.75 % (3231166)Peak memory usage: 88 MB
% 41.96/6.75 % (3231166)Instructions burned: 108 (million)
% 41.96/6.75 % (3231167)Instruction limit reached!
% 41.96/6.75 % (3231167)------------------------------
% 41.96/6.75 % (3231167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.96/6.75 % (3231167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.96/6.75 % (3231167)CaDiCaL version: 2.1.3
% 41.96/6.75 % (3231167)Termination reason: Instruction limit
% 41.96/6.75 % (3231167)Termination phase: Saturation
% 41.96/6.75 % (3231167)Time elapsed: 0.151 s
% 41.96/6.75 % (3231167)Peak memory usage: 88 MB
% 41.96/6.75 % (3231167)Instructions burned: 242 (million)
% 41.96/6.75 % (3231172)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4131357140:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 41.96/6.75 % (3231172)Instruction limit reached!
% 41.96/6.75 % (3231172)------------------------------
% 41.96/6.75 % (3231172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.96/6.75 % (3231172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.96/6.75 % (3231172)CaDiCaL version: 2.1.3
% 41.96/6.75 % (3231172)Termination reason: Instruction limit
% 41.96/6.75 % (3231172)Termination phase: Saturation
% 41.96/6.75 % (3231172)Time elapsed: 0.084 s
% 41.96/6.75 % (3231172)Peak memory usage: 89 MB
% 41.96/6.75 % (3231172)Instructions burned: 134 (million)
% 41.96/6.75 % (3231173)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2213375291:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 41.96/6.75 % (3231176)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=88611467:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 41.96/6.75 % (3231176)Instruction limit reached!
% 41.96/6.75 % (3231176)------------------------------
% 41.96/6.75 % (3231176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.96/6.75 % (3231176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.96/6.75 % (3231176)CaDiCaL version: 2.1.3
% 41.96/6.75 % (3231176)Termination reason: Instruction limit
% 41.96/6.75 % (3231176)Termination phase: Saturation
% 41.96/6.75 % (3231176)Time elapsed: 0.129 s
% 41.96/6.75 % (3231176)Peak memory usage: 88 MB
% 41.96/6.75 % (3231176)Instructions burned: 192 (million)
% 41.96/6.75 % (3231173)Instruction limit reached!
% 41.96/6.75 % (3231173)------------------------------
% 41.96/6.75 % (3231173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.96/6.75 % (3231173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.96/6.75 % (3231173)CaDiCaL version: 2.1.3
% 41.96/6.75 % (3231173)Termination reason: Instruction limit
% 41.96/6.75 % (3231173)Termination phase: Saturation
% 41.96/6.75 % (3231173)Time elapsed: 0.275 s
% 41.96/6.75 % (3231173)Peak memory usage: 91 MB
% 41.96/6.75 % (3231173)Instructions burned: 500 (million)
% 41.96/6.75 % (3231178)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3620559655:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 41.96/6.75 % (3231179)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4989054:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 55.60/8.79 % (3231179)Instruction limit reached!
% 55.60/8.79 % (3231179)------------------------------
% 55.60/8.79 % (3231179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.60/8.79 % (3231179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.60/8.79 % (3231179)CaDiCaL version: 2.1.3
% 55.60/8.79 % (3231179)Termination reason: Instruction limit
% 55.60/8.79 % (3231179)Termination phase: Saturation
% 55.60/8.79 % (3231179)Time elapsed: 0.096 s
% 55.60/8.79 % (3231179)Peak memory usage: 89 MB
% 55.60/8.79 % (3231179)Instructions burned: 157 (million)
% 55.60/8.79 % (3231178)Instruction limit reached!
% 55.60/8.79 % (3231178)------------------------------
% 55.60/8.79 % (3231178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.60/8.79 % (3231178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.60/8.79 % (3231178)CaDiCaL version: 2.1.3
% 55.60/8.79 % (3231178)Termination reason: Instruction limit
% 55.60/8.79 % (3231178)Termination phase: Saturation
% 55.60/8.79 % (3231178)Time elapsed: 0.161 s
% 55.60/8.79 % (3231178)Peak memory usage: 89 MB
% 55.60/8.79 % (3231178)Instructions burned: 264 (million)
% 55.60/8.79 % (3231182)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3396833114:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 55.60/8.79 % (3231183)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2003241437:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 55.60/8.79 % (3231183)Instruction limit reached!
% 55.60/8.79 % (3231183)------------------------------
% 55.60/8.79 % (3231183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.60/8.79 % (3231183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.60/8.79 % (3231183)CaDiCaL version: 2.1.3
% 55.60/8.79 % (3231183)Termination reason: Instruction limit
% 55.60/8.79 % (3231183)Termination phase: Saturation
% 55.60/8.79 % (3231183)Time elapsed: 0.321 s
% 55.60/8.79 % (3231183)Peak memory usage: 90 MB
% 55.60/8.79 % (3231183)Instructions burned: 538 (million)
% 55.60/8.79 % (3231186)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=856197812:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi)
% 55.60/8.79 % (3231186)Instruction limit reached!
% 55.60/8.79 % (3231186)------------------------------
% 55.60/8.79 % (3231186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.60/8.79 % (3231186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.60/8.79 % (3231186)CaDiCaL version: 2.1.3
% 55.60/8.79 % (3231186)Termination reason: Instruction limit
% 55.60/8.79 % (3231186)Termination phase: Saturation
% 55.60/8.79 % (3231186)Time elapsed: 0.099 s
% 55.60/8.79 % (3231186)Peak memory usage: 89 MB
% 55.60/8.79 % (3231186)Instructions burned: 181 (million)
% 55.60/8.79 % (3231189)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2053717876:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi)
% 55.60/8.79 % (3231160)Instruction limit reached!
% 55.60/8.79 % (3231160)------------------------------
% 55.60/8.79 % (3231160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.60/8.79 % (3231160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.60/8.79 % (3231160)CaDiCaL version: 2.1.3
% 55.60/8.79 % (3231160)Termination reason: Instruction limit
% 55.60/8.79 % (3231160)Termination phase: Saturation
% 55.60/8.79 % (3231160)Time elapsed: 2.169 s
% 55.60/8.79 % (3231160)Peak memory usage: 147 MB
% 55.60/8.79 % (3231160)Instructions burned: 3395 (million)
% 55.60/8.79 % (3231191)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3240260555:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi)
% 55.60/8.79 % (3231191)Instruction limit reached!
% 55.60/8.79 % (3231191)------------------------------
% 55.60/8.79 % (3231191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.60/8.79 % (3231191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.60/8.79 % (3231191)CaDiCaL version: 2.1.3
% 55.60/8.79 % (3231191)Termination reason: Instruction limit
% 55.60/8.79 % (3231191)Termination phase: Saturation
% 76.63/11.66 % (3231191)Time elapsed: 0.268 s
% 76.63/11.66 % (3231191)Peak memory usage: 91 MB
% 76.63/11.66 % (3231191)Instructions burned: 412 (million)
% 76.63/11.66 % (3231193)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3953658593:s2pl=no:i=8478:s2at=4:nm=6_2968 on theBenchmark for (2968ds/8478Mi)
% 76.63/11.66 % (3231182)Instruction limit reached!
% 76.63/11.66 % (3231182)------------------------------
% 76.63/11.66 % (3231182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231182)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231182)Termination reason: Instruction limit
% 76.63/11.66 % (3231182)Termination phase: Saturation
% 76.63/11.66 % (3231182)Time elapsed: 1.936 s
% 76.63/11.66 % (3231182)Peak memory usage: 144 MB
% 76.63/11.66 % (3231182)Instructions burned: 3256 (million)
% 76.63/11.66 % (3231195)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3827792439:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2963 on theBenchmark for (2963ds/303Mi)
% 76.63/11.66 % (3231195)Instruction limit reached!
% 76.63/11.66 % (3231195)------------------------------
% 76.63/11.66 % (3231195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231195)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231195)Termination reason: Instruction limit
% 76.63/11.66 % (3231195)Termination phase: Saturation
% 76.63/11.66 % (3231195)Time elapsed: 0.155 s
% 76.63/11.66 % (3231195)Peak memory usage: 89 MB
% 76.63/11.66 % (3231195)Instructions burned: 305 (million)
% 76.63/11.66 % (3231168)Instruction limit reached!
% 76.63/11.66 % (3231168)------------------------------
% 76.63/11.66 % (3231168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231168)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231168)Termination reason: Instruction limit
% 76.63/11.66 % (3231168)Termination phase: Saturation
% 76.63/11.66 % (3231168)Time elapsed: 3.192 s
% 76.63/11.66 % (3231168)Peak memory usage: 155 MB
% 76.63/11.66 % (3231168)Instructions burned: 5208 (million)
% 76.63/11.66 % (3231197)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=82149092:st=4:i=720:sd=3:fsr=off:ss=axioms_2960 on theBenchmark for (2960ds/720Mi)
% 76.63/11.66 % (3231198)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=34804438:i=598:bs=on:bd=preordered:av=off:ss=axioms_2960 on theBenchmark for (2960ds/598Mi)
% 76.63/11.66 % (3231197)Instruction limit reached!
% 76.63/11.66 % (3231197)------------------------------
% 76.63/11.66 % (3231197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231197)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231197)Termination reason: Instruction limit
% 76.63/11.66 % (3231197)Termination phase: Saturation
% 76.63/11.66 % (3231197)Time elapsed: 0.359 s
% 76.63/11.66 % (3231197)Peak memory usage: 90 MB
% 76.63/11.66 % (3231197)Instructions burned: 720 (million)
% 76.63/11.66 % (3231198)Instruction limit reached!
% 76.63/11.66 % (3231198)------------------------------
% 76.63/11.66 % (3231198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231198)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231198)Termination reason: Instruction limit
% 76.63/11.66 % (3231198)Termination phase: Saturation
% 76.63/11.66 % (3231198)Time elapsed: 0.324 s
% 76.63/11.66 % (3231198)Peak memory usage: 91 MB
% 76.63/11.66 % (3231198)Instructions burned: 599 (million)
% 76.63/11.66 % (3231201)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3314738601:i=2989:sd=3:ss=axioms:sgt=60_2956 on theBenchmark for (2956ds/2989Mi)
% 76.63/11.66 % (3231202)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=585657333:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2955 on theBenchmark for (2955ds/1997Mi)
% 76.63/11.66 % (3231202)Instruction limit reached!
% 76.63/11.66 % (3231202)------------------------------
% 76.63/11.66 % (3231202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231202)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231202)Termination reason: Instruction limit
% 76.63/11.66 % (3231202)Termination phase: Saturation
% 76.63/11.66 % (3231202)Time elapsed: 1.339 s
% 76.63/11.66 % (3231202)Peak memory usage: 136 MB
% 76.63/11.66 % (3231202)Instructions burned: 1998 (million)
% 76.63/11.66 % (3231205)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=4015174815:i=2088:bd=preordered:av=off_2940 on theBenchmark for (2940ds/2088Mi)
% 76.63/11.66 % (3231201)Instruction limit reached!
% 76.63/11.66 % (3231201)------------------------------
% 76.63/11.66 % (3231201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231201)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231201)Termination reason: Instruction limit
% 76.63/11.66 % (3231201)Termination phase: Saturation
% 76.63/11.66 % (3231201)Time elapsed: 2.064 s
% 76.63/11.66 % (3231201)Peak memory usage: 142 MB
% 76.63/11.66 % (3231201)Instructions burned: 2989 (million)
% 76.63/11.66 % (3231207)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3903341312:i=1098:nicw=on_2934 on theBenchmark for (2934ds/1098Mi)
% 76.63/11.66 % (3231207)Instruction limit reached!
% 76.63/11.66 % (3231207)------------------------------
% 76.63/11.66 % (3231207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231207)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231207)Termination reason: Instruction limit
% 76.63/11.66 % (3231207)Termination phase: Saturation
% 76.63/11.66 % (3231207)Time elapsed: 0.616 s
% 76.63/11.66 % (3231207)Peak memory usage: 108 MB
% 76.63/11.66 % (3231207)Instructions burned: 1098 (million)
% 76.63/11.66 % (3231205)Instruction limit reached!
% 76.63/11.66 % (3231205)------------------------------
% 76.63/11.66 % (3231205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231205)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231205)Termination reason: Instruction limit
% 76.63/11.66 % (3231205)Termination phase: Saturation
% 76.63/11.66 % (3231205)Time elapsed: 1.367 s
% 76.63/11.66 % (3231205)Peak memory usage: 135 MB
% 76.63/11.66 % (3231205)Instructions burned: 2088 (million)
% 76.63/11.66 % (3231209)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=529760547:i=433:bd=preordered_2926 on theBenchmark for (2926ds/433Mi)
% 76.63/11.66 % (3231210)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1025655034:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2925 on theBenchmark for (2925ds/2942Mi)
% 76.63/11.66 % (3231209)Instruction limit reached!
% 76.63/11.66 % (3231209)------------------------------
% 76.63/11.66 % (3231209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231209)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231209)Termination reason: Instruction limit
% 76.63/11.66 % (3231209)Termination phase: Saturation
% 76.63/11.66 % (3231209)Time elapsed: 0.250 s
% 76.63/11.66 % (3231209)Peak memory usage: 91 MB
% 76.63/11.66 % (3231209)Instructions burned: 433 (million)
% 76.63/11.66 % (3231213)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3309014051:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2922 on theBenchmark for (2922ds/6922Mi)
% 76.63/11.66 % (3231193)Instruction limit reached!
% 76.63/11.66 % (3231193)------------------------------
% 76.63/11.66 % (3231193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231193)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231193)Termination reason: Instruction limit
% 76.63/11.66 % (3231193)Termination phase: Saturation
% 76.63/11.66 % (3231193)Time elapsed: 4.650 s
% 76.63/11.66 % (3231193)Peak memory usage: 180 MB
% 76.63/11.66 % (3231193)Instructions burned: 8479 (million)
% 76.63/11.66 % (3231215)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=773735774:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2920 on theBenchmark for (2920ds/596Mi)
% 76.63/11.66 % (3231215)Instruction limit reached!
% 76.63/11.66 % (3231215)------------------------------
% 76.63/11.66 % (3231215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231215)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231215)Termination reason: Instruction limit
% 76.63/11.66 % (3231215)Termination phase: Saturation
% 76.63/11.66 % (3231215)Time elapsed: 0.295 s
% 76.63/11.66 % (3231215)Peak memory usage: 94 MB
% 76.63/11.66 % (3231215)Instructions burned: 596 (million)
% 76.63/11.66 % (3231217)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2339985120:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2915 on theBenchmark for (2915ds/4123Mi)
% 76.63/11.66 % (3231189)Instruction limit reached!
% 76.63/11.66 % (3231189)------------------------------
% 76.63/11.66 % (3231189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231189)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231189)Termination reason: Instruction limit
% 76.63/11.66 % (3231189)Termination phase: Saturation
% 76.63/11.66 % (3231189)Time elapsed: 6.280 s
% 76.63/11.66 % (3231189)Peak memory usage: 153 MB
% 76.63/11.66 % (3231189)Instructions burned: 10308 (million)
% 76.63/11.66 % (3231219)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3395260816:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2912 on theBenchmark for (2912ds/16411Mi)
% 76.63/11.66 % (3231210)Instruction limit reached!
% 76.63/11.66 % (3231210)------------------------------
% 76.63/11.66 % (3231210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231210)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231210)Termination reason: Instruction limit
% 76.63/11.66 % (3231210)Termination phase: Saturation
% 76.63/11.66 % (3231210)Time elapsed: 1.919 s
% 76.63/11.66 % (3231210)Peak memory usage: 137 MB
% 76.63/11.66 % (3231210)Instructions burned: 2943 (million)
% 76.63/11.66 % (3231221)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2064919915:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2905 on theBenchmark for (2905ds/1670Mi)
% 76.63/11.66 % (3231219)First to succeed.
% 76.63/11.66 % (3231219)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3231131"
% 76.63/11.66 % (3231213)Also succeeded, but the first one will report.
% 76.63/11.66 % (3231221)Instruction limit reached!
% 76.63/11.66 % (3231221)------------------------------
% 76.63/11.66 % (3231221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.63/11.66 % (3231221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.63/11.66 % (3231221)CaDiCaL version: 2.1.3
% 76.63/11.66 % (3231221)Termination reason: Instruction limit
% 76.63/11.66 % (3231221)Termination phase: Saturation
% 76.63/11.66 % (3231221)Time elapsed: 1.045 s
% 76.63/11.66 % (3231221)Peak memory usage: 135 MB
% 76.63/11.66 % (3231221)Instructions burned: 1670 (million)
% 76.63/11.66 % (3231223)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=2529016054:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2893 on theBenchmark for (2893ds/1722Mi)
% 76.63/11.66 % (3231219)Refutation found. Thanks to Tanya!
% 76.63/11.66 % SZS status Unsatisfiable for theBenchmark
% 76.63/11.66 % SZS output start Proof for theBenchmark
% See solution above
% 77.18/11.76 % (3231219)------------------------------
% 77.18/11.76 % (3231219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.18/11.76 % (3231219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.18/11.76 % (3231219)CaDiCaL version: 2.1.3
% 77.18/11.76 % (3231219)Termination reason: Refutation
% 77.18/11.76 % (3231219)Time elapsed: 1.684 s
% 77.18/11.76 % (3231219)Peak memory usage: 143 MB
% 77.18/11.76 % (3231219)Instructions burned: 2639 (million)
% 77.18/11.76 % (3231219)------------------------------
% 77.18/11.76 % (3231219)------------------------------
% 77.18/11.76 % (3231131)Success in time 10.827 s
% 77.18/11.76 % Vampire exiting
%------------------------------------------------------------------------------