%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP026-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:12:09 AM UTC 2026
% Result : Satisfiable 60.05s 9.44s
% Output : Saturation 61.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u88,negated_conjecture,
~ product(g2,isomorphism6(d1),isomorphism6(d2),isomorphism6(d3)) ).
cnf(u107,negated_conjecture,
product(g2,isomorphism1(d1),isomorphism1(d2),isomorphism1(d3)) ).
cnf(u117,negated_conjecture,
c != d1 ).
cnf(u121,negated_conjecture,
b != d1 ).
cnf(u126,negated_conjecture,
a = d1 ).
cnf(u136,negated_conjecture,
c = d3 ).
cnf(u139,negated_conjecture,
b != d3 ).
cnf(u143,negated_conjecture,
a != d3 ).
cnf(u154,negated_conjecture,
c = d2 ).
cnf(u846,hypothesis,
g = multiply(g2,h,h) ).
cnf(u849,hypothesis,
f != multiply(g2,h,h) ).
cnf(u880,hypothesis,
h != multiply(g2,g,h) ).
cnf(u884,hypothesis,
g != multiply(g2,g,h) ).
cnf(u889,hypothesis,
f = multiply(g2,g,h) ).
cnf(u925,hypothesis,
g != multiply(g2,h,g) ).
cnf(u930,hypothesis,
f = multiply(g2,h,g) ).
cnf(u974,hypothesis,
h != inverse(g2,h) ).
cnf(u979,hypothesis,
g = inverse(g2,h) ).
cnf(u982,hypothesis,
f != inverse(g2,h) ).
cnf(u1010,hypothesis,
h = inverse(g2,g) ).
cnf(u1013,hypothesis,
g != inverse(g2,g) ).
cnf(u1017,hypothesis,
f != inverse(g2,g) ).
cnf(u1190,hypothesis,
c = inverse(g1,b) ).
cnf(u1193,hypothesis,
b != inverse(g1,b) ).
cnf(u1197,hypothesis,
a != inverse(g1,b) ).
cnf(u1291,hypothesis,
h = multiply(g2,g,g) ).
cnf(u1294,hypothesis,
g != multiply(g2,g,g) ).
cnf(u1298,hypothesis,
f != multiply(g2,g,g) ).
cnf(u1395,hypothesis,
h = multiply(g2,h,f) ).
cnf(u1398,hypothesis,
g != multiply(g2,h,f) ).
cnf(u1441,hypothesis,
h = multiply(g2,f,h) ).
cnf(u1444,hypothesis,
g != multiply(g2,f,h) ).
cnf(u1486,hypothesis,
h != multiply(g2,g,f) ).
cnf(u1491,hypothesis,
g = multiply(g2,g,f) ).
cnf(u1494,hypothesis,
f != multiply(g2,g,f) ).
cnf(u1535,hypothesis,
g = multiply(g2,f,g) ).
cnf(u1538,hypothesis,
f != multiply(g2,f,g) ).
cnf(u1606,hypothesis,
f = multiply(g2,f,f) ).
cnf(u2039,hypothesis,
c != multiply(g1,b,c) ).
cnf(u2043,hypothesis,
b != multiply(g1,b,c) ).
cnf(u2048,hypothesis,
a = multiply(g1,b,c) ).
cnf(u2604,hypothesis,
c = multiply(g1,b,b) ).
cnf(u2607,hypothesis,
b != multiply(g1,b,b) ).
cnf(u2611,hypothesis,
a != multiply(g1,b,b) ).
cnf(u3406,hypothesis,
c != inverse(g1,c) ).
cnf(u3411,hypothesis,
b = inverse(g1,c) ).
cnf(u3702,hypothesis,
c != multiply(g1,c,c) ).
cnf(u3707,hypothesis,
b = multiply(g1,c,c) ).
cnf(u3710,hypothesis,
a != multiply(g1,c,c) ).
cnf(u2734,axiom,
( ~ product(X1,X0,inverse(X1,X0),X2)
| product(X1,identity_for(X1),X2,identity_for(X1)) ) ).
cnf(u63,hypothesis,
g = isomorphism4(a) ).
cnf(u2945,hypothesis,
( ~ product(g2,h,g,X0)
| product(g2,f,X0,f) ) ).
cnf(u4996,hypothesis,
( ~ product(g1,b,a,X0)
| product(g1,X0,c,a) ) ).
cnf(u755,hypothesis,
( ~ product(g2,inverse(g2,X0),X0,X1)
| product(g2,f,X1,f) ) ).
cnf(u5006,hypothesis,
( ~ product(g1,a,c,X0)
| product(g1,b,X0,a) ) ).
cnf(u744,axiom,
( ~ product(X0,inverse(X0,X1),X1,X2)
| product(X0,identity_for(X0),X2,identity_for(X0)) ) ).
cnf(u4058,hypothesis,
( ~ product(g1,X0,b,a)
| c = X0 ) ).
cnf(u3591,hypothesis,
product(g2,g,g,h) ).
cnf(u588,axiom,
( ~ product(X0,X1,X2,X3)
| product(X0,X3,inverse(X0,X2),X1) ) ).
cnf(u4550,hypothesis,
( ~ product(g2,X0,inverse(g2,X0),X1)
| product(g2,f,X1,f) ) ).
cnf(u3300,hypothesis,
( ~ product(g1,X0,X1,c)
| product(g1,X2,X1,a)
| ~ product(g1,b,X0,X2) ) ).
cnf(u785,hypothesis,
( ~ product(g2,X0,f,X1)
| product(g2,X1,inverse(g2,X0),f) ) ).
cnf(u1268,hypothesis,
product(g1,c,b,a) ).
cnf(u5146,hypothesis,
( ~ product(g2,f,h,X0)
| product(g2,g,X0,f) ) ).
cnf(u4053,hypothesis,
( ~ product(g1,c,b,X0)
| product(g1,X0,a,a) ) ).
cnf(u4311,hypothesis,
( ~ product(g1,inverse(g1,X0),X0,X1)
| product(g1,X1,a,a) ) ).
cnf(u67,hypothesis,
f = isomorphism4(c) ).
cnf(u5125,hypothesis,
( ~ product(g2,g,h,X0)
| product(g2,g,X0,g) ) ).
cnf(u1694,hypothesis,
( ~ product(g2,X2,X0,h)
| ~ product(g2,X0,g,X1)
| product(g2,X2,X1,f) ) ).
cnf(u1693,hypothesis,
( ~ product(g2,X0,X1,g)
| product(g2,X2,X1,f)
| ~ product(g2,h,X0,X2) ) ).
cnf(u45,hypothesis,
f = isomorphism1(a) ).
cnf(u707,hypothesis,
b = multiply(g1,a,b) ).
cnf(u679,hypothesis,
c = multiply(g1,c,a) ).
cnf(u1690,hypothesis,
( ~ product(g2,X0,g,f)
| h = X0 ) ).
cnf(u5115,hypothesis,
( ~ product(g2,h,g,X0)
| product(g2,X0,g,g) ) ).
cnf(u252,hypothesis,
( ~ group_member(X0,g1)
| group_member(multiply(g1,X0,a),g1) ) ).
cnf(u3369,negated_conjecture,
~ product(g2,h,g,g) ).
cnf(u4979,hypothesis,
( ~ product(g1,a,b,X0)
| product(g1,b,X0,c) ) ).
cnf(u49,hypothesis,
h = isomorphism1(c) ).
cnf(u4107,hypothesis,
( ~ product(g2,X3,X0,inverse(g2,X1))
| ~ product(g2,X0,X1,X2)
| product(g2,X3,X2,f) ) ).
cnf(u4660,hypothesis,
( ~ product(g1,X3,X1,inverse(g1,X0))
| ~ product(g1,X1,X0,X2)
| product(g1,X3,X2,a) ) ).
cnf(u2264,hypothesis,
( ~ product(g2,h,X0,X1)
| product(g2,g,X1,X0) ) ).
cnf(f_right_identity,hypothesis,
product(g2,X0,f,X0) ).
cnf(u232,hypothesis,
( ~ group_member(X0,g2)
| group_member(multiply(g2,X0,f),g2) ) ).
cnf(u3051,hypothesis,
( ~ product(g2,X2,X0,h)
| ~ product(g2,X0,h,X1)
| product(g2,X2,X1,g) ) ).
cnf(u73,hypothesis,
f = isomorphism5(c) ).
cnf(f_member_of_group2,hypothesis,
group_member(f,g2) ).
cnf(u783,hypothesis,
( ~ product(g1,X0,a,X1)
| product(g1,X1,inverse(g1,X0),a) ) ).
cnf(u226,axiom,
( ~ group_member(X0,X1)
| product(X1,X0,identity_for(X1),multiply(X1,X0,identity_for(X1))) ) ).
cnf(u4013,hypothesis,
( ~ product(g1,X0,c,X1)
| product(g1,X1,b,X0) ) ).
cnf(u39,hypothesis,
f = identity_for(g2) ).
cnf(u1832,hypothesis,
product(g2,g,h,f) ).
cnf(u69,hypothesis,
h = isomorphism5(a) ).
cnf(g_member_of_group2,hypothesis,
group_member(g,g2) ).
cnf(u2090,hypothesis,
product(g1,b,c,a) ).
cnf(u184,hypothesis,
( ~ product(g2,X0,X1,X0)
| f = X1 ) ).
cnf(u3596,hypothesis,
( ~ product(g2,g,X0,h)
| g = X0 ) ).
cnf(f_not_g,hypothesis,
f != g ).
cnf(u3558,hypothesis,
product(g1,c,c,b) ).
cnf(u178,hypothesis,
( ~ product(g1,a,X0,X3)
| ~ product(g1,X0,X1,X2)
| product(g1,X3,X1,X2) ) ).
cnf(b_member_of_group1,hypothesis,
group_member(b,g1) ).
cnf(u177,hypothesis,
( ~ product(g2,X0,X1,f)
| ~ product(g2,X2,X0,X3)
| product(g2,X3,X1,X2) ) ).
cnf(u180,axiom,
( ~ product(X0,identity_for(X0),X1,X4)
| ~ product(X0,X1,X2,X3)
| product(X0,X4,X2,X3) ) ).
cnf(a_not_b,hypothesis,
a != b ).
cnf(u4970,hypothesis,
( ~ product(g1,a,c,X0)
| product(g1,c,X0,b) ) ).
cnf(u3522,hypothesis,
( ~ product(g1,c,X0,X1)
| product(g1,b,X1,X0) ) ).
cnf(total_function1_2,axiom,
( ~ group_member(X2,X1)
| ~ group_member(X0,X1)
| group_member(multiply(X1,X0,X2),X1) ) ).
cnf(u323,hypothesis,
( ~ product(g2,X0,f,X1)
| product(g2,X1,f,X0) ) ).
cnf(left_identity,axiom,
product(X0,identity_for(X0),X1,X1) ).
cnf(identity_in_group,axiom,
group_member(identity_for(X0),X0) ).
cnf(u4986,hypothesis,
( ~ product(g1,b,c,X0)
| product(g1,X0,c,c) ) ).
cnf(u4035,hypothesis,
( ~ product(g1,c,b,X0)
| a = X0 ) ).
cnf(u3939,hypothesis,
( ~ product(g1,X0,X1,c)
| product(g1,X2,X1,b)
| ~ product(g1,c,X0,X2) ) ).
cnf(u562,axiom,
identity_for(X0) = inverse(X0,identity_for(X0)) ).
cnf(u2917,hypothesis,
( ~ product(g2,h,g,X0)
| product(g2,X0,f,f) ) ).
cnf(u4885,hypothesis,
( ~ product(g1,c,c,X0)
| product(g1,X0,c,a) ) ).
cnf(u253,hypothesis,
( ~ group_member(X0,g1)
| product(g1,X0,a,multiply(g1,X0,a)) ) ).
cnf(u2944,hypothesis,
( ~ product(g2,g,h,X0)
| product(g2,X0,f,f) ) ).
cnf(u3297,hypothesis,
( ~ product(g1,X0,c,a)
| b = X0 ) ).
cnf(u5162,hypothesis,
( ~ product(g2,g,g,X0)
| product(g2,g,X0,f) ) ).
cnf(u3523,hypothesis,
( ~ product(g1,X0,b,X1)
| product(g1,X1,c,X0) ) ).
cnf(u1374,hypothesis,
( ~ product(g1,X0,inverse(g1,X1),a)
| X0 = X1 ) ).
cnf(u4611,hypothesis,
( ~ product(g1,X0,X1,X0)
| product(g1,a,X1,a) ) ).
cnf(u5154,hypothesis,
( ~ product(g2,h,f,X0)
| product(g2,X0,g,f) ) ).
cnf(u2283,hypothesis,
( ~ product(g2,X0,g,X1)
| product(g2,X1,h,X0) ) ).
cnf(u4960,hypothesis,
( ~ product(g1,c,a,X0)
| product(g1,X0,c,b) ) ).
cnf(u2285,hypothesis,
( ~ product(g2,X0,h,X1)
| product(g2,X1,g,X0) ) ).
cnf(u1835,hypothesis,
( ~ product(g2,g,h,X0)
| f = X0 ) ).
cnf(u5164,hypothesis,
( ~ product(g2,f,g,X0)
| product(g2,h,X0,f) ) ).
cnf(u563,hypothesis,
( ~ product(g2,X0,X1,f)
| inverse(g2,X1) = X0 ) ).
cnf(u4033,hypothesis,
( ~ product(g1,X0,X2,b)
| ~ product(g1,c,X0,X1)
| product(g1,X1,X2,a) ) ).
cnf(u202,hypothesis,
( ~ group_member(X0,g2)
| product(g2,X0,g,multiply(g2,X0,g)) ) ).
cnf(u784,hypothesis,
( ~ product(g2,X0,inverse(g2,X0),X1)
| product(g2,X1,f,f) ) ).
cnf(u171,hypothesis,
( ~ product(g2,X0,f,X1)
| ~ product(g2,X2,X0,X3)
| product(g2,X2,X1,X3) ) ).
cnf(u201,hypothesis,
( ~ group_member(X0,g2)
| product(g2,X0,f,multiply(g2,X0,f)) ) ).
cnf(u174,axiom,
( ~ product(X0,X4,X1,identity_for(X0))
| ~ product(X0,X1,X2,X3)
| product(X0,X4,X3,X2) ) ).
cnf(u587,axiom,
inverse(X0,inverse(X0,X1)) = X1 ).
cnf(u552,hypothesis,
product(g1,inverse(g1,X0),X0,a) ).
cnf(u173,hypothesis,
( ~ product(g1,X0,a,X1)
| ~ product(g1,X2,X0,X3)
| product(g1,X2,X1,X3) ) ).
cnf(u195,hypothesis,
( ~ product(g2,X0,X1,X1)
| f = X0 ) ).
cnf(inverse_in_group,axiom,
( ~ group_member(X0,X1)
| group_member(inverse(X1,X0),X1) ) ).
cnf(u197,hypothesis,
( ~ product(g1,X0,X1,X1)
| a = X0 ) ).
cnf(u4132,hypothesis,
( ~ product(g2,X0,X1,X0)
| product(g2,f,X1,f) ) ).
cnf(u5153,hypothesis,
( ~ product(g2,h,h,X0)
| product(g2,X0,h,f) ) ).
cnf(u4574,hypothesis,
( ~ product(g1,X0,inverse(g1,X0),X1)
| a = X1 ) ).
cnf(u4176,hypothesis,
( ~ product(g2,X0,X1,inverse(g2,X2))
| ~ product(g2,X2,X0,X3)
| product(g2,X3,X1,f) ) ).
cnf(u496,hypothesis,
( ~ group_member(X0,g1)
| group_member(multiply(g1,X0,b),g1) ) ).
cnf(u592,axiom,
( ~ product(X0,X1,X2,identity_for(X0))
| inverse(X0,X1) = X2 ) ).
cnf(u3937,hypothesis,
( ~ product(g1,c,c,X0)
| b = X0 ) ).
cnf(u4106,hypothesis,
( ~ product(g2,inverse(g2,X0),X0,X1)
| f = X1 ) ).
cnf(u451,hypothesis,
( ~ group_member(X0,g1)
| product(g1,X0,c,multiply(g1,X0,c)) ) ).
cnf(u3047,hypothesis,
( ~ product(g2,X0,h,g)
| h = X0 ) ).
cnf(u290,axiom,
( ~ product(X0,identity_for(X0),X1,X2)
| product(X0,identity_for(X0),X2,X1) ) ).
cnf(u4135,hypothesis,
( ~ product(g2,X0,X1,X1)
| product(g2,X0,f,f) ) ).
cnf(u3049,hypothesis,
( ~ product(g2,h,X0,g)
| h = X0 ) ).
cnf(u5094,hypothesis,
( ~ product(g2,h,g,X0)
| product(g2,h,X0,h) ) ).
cnf(u57,hypothesis,
g = isomorphism3(a) ).
cnf(u3045,hypothesis,
product(g2,h,h,g) ).
cnf(u51,hypothesis,
f = isomorphism2(a) ).
cnf(u4034,hypothesis,
( ~ product(g1,c,X0,a)
| b = X0 ) ).
cnf(u53,hypothesis,
h = isomorphism2(b) ).
cnf(u3539,hypothesis,
product(g1,b,b,c) ).
cnf(a_left_identity,hypothesis,
product(g1,a,X0,X0) ).
cnf(u47,hypothesis,
g = isomorphism1(b) ).
cnf(u3540,hypothesis,
( ~ product(g1,X0,b,c)
| b = X0 ) ).
cnf(u3595,hypothesis,
( ~ product(g2,X0,X1,g)
| ~ product(g2,g,X0,X2)
| product(g2,X2,X1,h) ) ).
cnf(u3299,hypothesis,
( ~ product(g1,b,X0,a)
| c = X0 ) ).
cnf(u1692,hypothesis,
( ~ product(g2,h,X0,f)
| g = X0 ) ).
cnf(u75,hypothesis,
h = isomorphism6(a) ).
cnf(u3301,hypothesis,
( ~ product(g1,X2,X0,b)
| ~ product(g1,X0,c,X1)
| product(g1,X2,X1,a) ) ).
cnf(u4886,hypothesis,
( ~ product(g1,c,a,X0)
| product(g1,X0,b,a) ) ).
cnf(u789,axiom,
( ~ product(X0,X1,X2,X1)
| product(X0,identity_for(X0),X2,identity_for(X0)) ) ).
cnf(u4027,hypothesis,
( ~ product(g1,c,b,X0)
| product(g1,a,X0,a) ) ).
cnf(u3938,hypothesis,
( ~ product(g1,c,X0,b)
| c = X0 ) ).
cnf(u5104,hypothesis,
( ~ product(g2,g,h,X0)
| product(g2,X0,h,h) ) ).
cnf(u3298,hypothesis,
( ~ product(g1,b,c,X0)
| a = X0 ) ).
cnf(u5136,hypothesis,
( ~ product(g2,g,f,X0)
| product(g2,X0,h,f) ) ).
cnf(u4961,hypothesis,
( ~ product(g1,c,c,X0)
| product(g1,X0,a,b) ) ).
cnf(u769,hypothesis,
( ~ product(g2,X0,f,X1)
| product(g2,X0,inverse(g2,X1),f) ) ).
cnf(u680,hypothesis,
b = multiply(g1,b,a) ).
cnf(u4301,hypothesis,
( ~ product(g1,X0,inverse(g1,X0),X1)
| product(g1,a,X1,a) ) ).
cnf(u1373,hypothesis,
( ~ product(g2,X0,inverse(g2,X1),f)
| X0 = X1 ) ).
cnf(u4995,hypothesis,
( ~ product(g1,b,b,X0)
| product(g1,X0,b,a) ) ).
cnf(u678,hypothesis,
a = multiply(g1,a,a) ).
cnf(u3048,hypothesis,
( ~ product(g2,h,h,X0)
| g = X0 ) ).
cnf(u1838,hypothesis,
( ~ product(g2,X2,X0,g)
| ~ product(g2,X0,h,X1)
| product(g2,X2,X1,f) ) ).
cnf(u4988,hypothesis,
( ~ product(g1,b,b,X0)
| product(g1,X0,a,c) ) ).
cnf(u234,hypothesis,
( ~ group_member(X0,g2)
| group_member(multiply(g2,X0,h),g2) ) ).
cnf(u4647,hypothesis,
( ~ product(g1,inverse(g1,X0),X1,X3)
| ~ product(g1,X1,X2,X0)
| product(g1,X3,X2,a) ) ).
cnf(u233,hypothesis,
( ~ group_member(X0,g2)
| group_member(multiply(g2,X0,g),g2) ) ).
cnf(u1834,hypothesis,
( ~ product(g2,X0,h,f)
| g = X0 ) ).
cnf(u77,hypothesis,
f = isomorphism6(b) ).
cnf(u4032,hypothesis,
( ~ product(g1,X0,X1,c)
| product(g1,X0,X2,a)
| ~ product(g1,X1,b,X2) ) ).
cnf(u33,hypothesis,
( ~ group_member(X0,g1)
| a = X0
| b = X0
| c = X0 ) ).
cnf(u71,hypothesis,
g = isomorphism5(b) ).
cnf(u186,hypothesis,
( ~ product(g1,X0,X1,X0)
| a = X1 ) ).
cnf(h_member_of_group2,hypothesis,
group_member(h,g2) ).
cnf(u185,hypothesis,
( ~ product(g1,a,X0,X1)
| X0 = X1 ) ).
cnf(u30,hypothesis,
f != h ).
cnf(u4959,hypothesis,
( ~ product(g1,c,b,X0)
| product(g1,X0,b,b) ) ).
cnf(u188,axiom,
( ~ product(X0,X1,X2,X1)
| identity_for(X0) = X2 ) ).
cnf(u4978,hypothesis,
( ~ product(g1,b,b,X0)
| product(g1,a,X0,c) ) ).
cnf(u179,hypothesis,
( ~ product(g1,X0,X1,a)
| ~ product(g1,X2,X0,X3)
| product(g1,X3,X1,X2) ) ).
cnf(u16,axiom,
( ~ product(X0,X4,X2,X3)
| ~ product(X0,X1,X2,X3)
| X1 = X4 ) ).
cnf(u23,hypothesis,
a != c ).
cnf(u752,hypothesis,
( ~ product(g1,a,X0,X1)
| product(g1,inverse(g1,X0),X1,a) ) ).
cnf(u181,axiom,
( ~ product(X0,X1,X2,identity_for(X0))
| ~ product(X0,X3,X1,X4)
| product(X0,X4,X2,X3) ) ).
cnf(u10,axiom,
( ~ product(X0,X1,X2,X4)
| ~ product(X0,X1,X2,X3)
| X3 = X4 ) ).
cnf(u203,hypothesis,
( ~ group_member(X0,g2)
| product(g2,X0,h,multiply(g2,X0,h)) ) ).
cnf(u175,axiom,
( ~ product(X0,X1,identity_for(X0),X2)
| ~ product(X0,X3,X1,X4)
| product(X0,X3,X2,X4) ) ).
cnf(right_identity,axiom,
product(X0,X1,identity_for(X0),X1) ).
cnf(associativity2,axiom,
( ~ product(X0,X1,X5,X6)
| ~ product(X0,X2,X4,X5)
| ~ product(X0,X1,X2,X3)
| product(X0,X3,X4,X6) ) ).
cnf(u3542,hypothesis,
( ~ product(g1,b,X0,c)
| b = X0 ) ).
cnf(u4175,hypothesis,
( ~ product(g2,X0,inverse(g2,X1),X2)
| ~ product(g2,X3,X0,X1)
| product(g2,X3,X2,f) ) ).
cnf(left_inverse,axiom,
product(X0,inverse(X0,X1),X1,identity_for(X0)) ).
cnf(u3936,hypothesis,
( ~ product(g1,X0,c,b)
| c = X0 ) ).
cnf(right_inverse,axiom,
product(X0,X1,inverse(X0,X1),identity_for(X0)) ).
cnf(u4830,axiom,
identity_for(X0) = multiply(X0,identity_for(X0),identity_for(X0)) ).
cnf(u569,hypothesis,
f = inverse(g2,f) ).
cnf(u798,hypothesis,
( ~ product(g1,a,X0,X1)
| product(g1,inverse(g1,X1),X0,a) ) ).
cnf(u594,axiom,
( ~ product(X0,X1,inverse(X0,X2),X3)
| ~ product(X0,X4,X1,X2)
| product(X0,X4,X3,identity_for(X0)) ) ).
cnf(u758,axiom,
( ~ product(X0,X1,identity_for(X0),X2)
| product(X0,X1,inverse(X0,X2),identity_for(X0)) ) ).
cnf(u318,axiom,
( ~ product(X0,X1,identity_for(X0),X2)
| product(X0,X2,identity_for(X0),X1) ) ).
cnf(u593,axiom,
( ~ product(X0,X1,X2,inverse(X0,X3))
| ~ product(X0,X3,X1,X4)
| product(X0,X4,X2,identity_for(X0)) ) ).
cnf(u1837,hypothesis,
( ~ product(g2,X0,X1,h)
| product(g2,X2,X1,f)
| ~ product(g2,g,X0,X2) ) ).
cnf(u745,axiom,
( ~ product(X0,identity_for(X0),X1,X2)
| product(X0,inverse(X0,X1),X2,identity_for(X0)) ) ).
cnf(u590,axiom,
( ~ product(X0,X1,inverse(X0,X2),identity_for(X0))
| X1 = X2 ) ).
cnf(u589,axiom,
( ~ product(X0,inverse(X0,X1),X2,X3)
| product(X0,X1,X3,X2) ) ).
cnf(u546,axiom,
( ~ product(X0,inverse(X0,X3),X1,X4)
| ~ product(X0,X1,X2,X3)
| product(X0,X4,X2,identity_for(X0)) ) ).
cnf(u545,axiom,
( ~ product(X0,inverse(X0,X1),X2,identity_for(X0))
| X1 = X2 ) ).
cnf(u4046,hypothesis,
( ~ product(g1,b,X0,X1)
| product(g1,c,X1,X0) ) ).
cnf(u774,axiom,
( ~ product(X0,X1,identity_for(X0),X2)
| product(X0,X2,inverse(X0,X1),identity_for(X0)) ) ).
cnf(u4968,hypothesis,
( ~ product(g1,b,c,X0)
| product(g1,b,X0,b) ) ).
cnf(u4576,hypothesis,
( ~ product(g1,X0,X1,inverse(g1,X2))
| ~ product(g1,X2,X0,X3)
| product(g1,X3,X1,a) ) ).
cnf(u542,axiom,
( ~ product(X0,X1,X2,X3)
| product(X0,inverse(X0,X1),X3,X2) ) ).
cnf(u3543,hypothesis,
( ~ product(g1,X0,X1,b)
| product(g1,X2,X1,c)
| ~ product(g1,b,X0,X2) ) ).
cnf(u541,axiom,
( ~ product(X0,X1,inverse(X0,X2),X3)
| product(X0,X3,X2,X1) ) ).
cnf(u760,axiom,
( ~ product(X0,X1,X2,X2)
| product(X0,X1,identity_for(X0),identity_for(X0)) ) ).
cnf(u4977,hypothesis,
( ~ product(g1,c,b,X0)
| product(g1,c,X0,c) ) ).
cnf(u1358,hypothesis,
( ~ product(g1,inverse(g1,X0),X1,a)
| X0 = X1 ) ).
cnf(u5116,hypothesis,
( ~ product(g2,h,f,X0)
| product(g2,X0,h,g) ) ).
cnf(u5144,hypothesis,
( ~ product(g2,h,h,X0)
| product(g2,h,X0,f) ) ).
cnf(u4054,hypothesis,
( ~ product(g1,b,c,X0)
| product(g1,a,X0,a) ) ).
cnf(u788,axiom,
( ~ product(X0,identity_for(X0),X1,X2)
| product(X0,inverse(X0,X2),X1,identity_for(X0)) ) ).
cnf(u5126,hypothesis,
( ~ product(g2,h,h,X0)
| product(g2,f,X0,g) ) ).
cnf(u4026,hypothesis,
( ~ product(g1,b,c,X0)
| product(g1,X0,a,a) ) ).
cnf(u591,axiom,
( ~ product(X0,X1,inverse(X0,X1),X2)
| identity_for(X0) = X2 ) ).
cnf(u192,hypothesis,
( ~ product(g1,X0,a,X1)
| X0 = X1 ) ).
cnf(u199,axiom,
( ~ product(X0,X1,X2,X2)
| identity_for(X0) = X1 ) ).
cnf(u547,axiom,
( ~ product(X0,X4,X1,inverse(X0,X2))
| ~ product(X0,X1,X2,X3)
| product(X0,X4,X3,identity_for(X0)) ) ).
cnf(u59,hypothesis,
f = isomorphism3(b) ).
cnf(u5135,hypothesis,
( ~ product(g2,g,g,X0)
| product(g2,X0,g,f) ) ).
cnf(u768,hypothesis,
( ~ product(g1,X0,a,X1)
| product(g1,X0,inverse(g1,X1),a) ) ).
cnf(u5106,hypothesis,
( ~ product(g2,g,g,X0)
| product(g2,X0,f,h) ) ).
cnf(u543,axiom,
( ~ product(X0,X1,X2,identity_for(X0))
| inverse(X0,X2) = X1 ) ).
cnf(u3597,hypothesis,
( ~ product(g2,X0,g,h)
| g = X0 ) ).
cnf(u4539,hypothesis,
( ~ product(g2,inverse(g2,X0),X0,X1)
| product(g2,X1,f,f) ) ).
cnf(u2754,axiom,
( ~ product(X1,inverse(X1,X0),X0,X2)
| product(X1,X2,identity_for(X1),identity_for(X1)) ) ).
cnf(u3594,hypothesis,
( ~ product(g2,X2,X0,g)
| ~ product(g2,X0,g,X1)
| product(g2,X2,X1,h) ) ).
cnf(u61,hypothesis,
h = isomorphism3(c) ).
cnf(u3940,hypothesis,
( ~ product(g1,X2,X0,c)
| ~ product(g1,X0,c,X1)
| product(g1,X2,X1,b) ) ).
cnf(u55,hypothesis,
g = isomorphism2(c) ).
cnf(f_left_identity,hypothesis,
product(g2,f,X0,X0) ).
cnf(a_right_identity,hypothesis,
product(g1,X0,a,X0) ).
cnf(u4108,hypothesis,
( ~ product(g2,inverse(g2,X2),X0,X3)
| ~ product(g2,X0,X1,X2)
| product(g2,X3,X1,f) ) ).
cnf(u79,hypothesis,
g = isomorphism6(c) ).
cnf(u5004,hypothesis,
( ~ product(g1,c,c,X0)
| product(g1,c,X0,a) ) ).
cnf(u35,hypothesis,
( ~ group_member(X0,g2)
| f = X0
| g = X0
| h = X0 ) ).
cnf(u65,hypothesis,
h = isomorphism4(b) ).
cnf(u3544,hypothesis,
( ~ product(g1,X2,X0,b)
| ~ product(g1,X0,b,X1)
| product(g1,X2,X1,c) ) ).
cnf(u1691,hypothesis,
( ~ product(g2,h,g,X0)
| f = X0 ) ).
cnf(u37,hypothesis,
a = identity_for(g1) ).
cnf(u4575,hypothesis,
( ~ product(g1,X0,inverse(g1,X1),X2)
| ~ product(g1,X3,X0,X1)
| product(g1,X3,X2,a) ) ).
cnf(two_groups,hypothesis,
g1 != g2 ).
cnf(b_not_c,hypothesis,
b != c ).
cnf(g_not_h,hypothesis,
g != h ).
cnf(u5096,hypothesis,
( ~ product(g2,f,g,X0)
| product(g2,g,X0,h) ) ).
cnf(u5105,hypothesis,
( ~ product(g2,g,f,X0)
| product(g2,X0,g,h) ) ).
cnf(a_member_of_group1,hypothesis,
group_member(a,g1) ).
cnf(u4969,hypothesis,
( ~ product(g1,c,c,X0)
| product(g1,a,X0,b) ) ).
cnf(u2918,hypothesis,
( ~ product(g2,g,h,X0)
| product(g2,f,X0,f) ) ).
cnf(u622,hypothesis,
( ~ product(g2,X0,X1,f)
| inverse(g2,X0) = X1 ) ).
cnf(u1836,hypothesis,
( ~ product(g2,g,X0,f)
| h = X0 ) ).
cnf(u4078,hypothesis,
a = multiply(g1,c,b) ).
cnf(u602,hypothesis,
product(g1,X0,inverse(g1,X0),a) ).
cnf(u293,hypothesis,
( ~ product(g1,a,X0,X1)
| product(g1,a,X1,X0) ) ).
cnf(u5117,hypothesis,
( ~ product(g2,h,h,X0)
| product(g2,X0,f,g) ) ).
cnf(u601,hypothesis,
product(g2,X0,inverse(g2,X0),f) ).
cnf(u708,hypothesis,
c = multiply(g1,a,c) ).
cnf(u5127,hypothesis,
( ~ product(g2,f,h,X0)
| product(g2,h,X0,g) ) ).
cnf(u2266,hypothesis,
( ~ product(g2,g,X0,X1)
| product(g2,h,X1,X0) ) ).
cnf(u4604,hypothesis,
( ~ product(g1,X0,X1,X1)
| product(g1,X0,a,a) ) ).
cnf(u1357,hypothesis,
( ~ product(g2,inverse(g2,X0),X1,f)
| X0 = X1 ) ).
cnf(u4636,hypothesis,
( ~ product(g1,inverse(g1,X0),X0,X1)
| a = X1 ) ).
cnf(u235,axiom,
( ~ group_member(X0,X1)
| group_member(multiply(X1,X0,identity_for(X1)),X1) ) ).
cnf(u3541,hypothesis,
( ~ product(g1,b,b,X0)
| c = X0 ) ).
cnf(u623,hypothesis,
( ~ product(g1,X0,X1,a)
| inverse(g1,X0) = X1 ) ).
cnf(u450,hypothesis,
( ~ group_member(X0,g1)
| group_member(multiply(g1,X0,c),g1) ) ).
cnf(u775,axiom,
( ~ product(X0,X1,inverse(X0,X1),X2)
| product(X0,X2,identity_for(X0),identity_for(X0)) ) ).
cnf(u187,axiom,
( ~ product(X0,identity_for(X0),X1,X2)
| X1 = X2 ) ).
cnf(u1688,hypothesis,
product(g2,h,g,f) ).
cnf(u190,hypothesis,
( ~ product(g2,X0,f,X1)
| X0 = X1 ) ).
cnf(u497,hypothesis,
( ~ group_member(X0,g1)
| product(g1,X0,b,multiply(g1,X0,b)) ) ).
cnf(u176,hypothesis,
( ~ product(g2,f,X0,X3)
| ~ product(g2,X0,X1,X2)
| product(g2,X3,X1,X2) ) ).
cnf(u295,hypothesis,
( ~ product(g2,f,X0,X1)
| product(g2,f,X1,X0) ) ).
cnf(u183,hypothesis,
( ~ product(g2,f,X0,X1)
| X0 = X1 ) ).
cnf(c_member_of_group1,hypothesis,
group_member(c,g1) ).
cnf(u170,hypothesis,
( ~ product(g2,X3,X0,f)
| ~ product(g2,X0,X1,X2)
| product(g2,X3,X2,X1) ) ).
cnf(associativity1,axiom,
( ~ product(X0,X3,X4,X6)
| ~ product(X0,X2,X4,X5)
| ~ product(X0,X1,X2,X3)
| product(X0,X1,X5,X6) ) ).
cnf(u564,hypothesis,
( ~ product(g1,X0,X1,a)
| inverse(g1,X1) = X0 ) ).
cnf(u14,axiom,
( ~ product(X0,X1,X4,X3)
| ~ product(X0,X1,X2,X3)
| X2 = X4 ) ).
cnf(u172,hypothesis,
( ~ product(g1,X3,X0,a)
| ~ product(g1,X0,X1,X2)
| product(g1,X3,X2,X1) ) ).
cnf(u194,axiom,
( ~ product(X0,X1,identity_for(X0),X2)
| X1 = X2 ) ).
cnf(u321,hypothesis,
( ~ product(g1,X0,a,X1)
| product(g1,X1,a,X0) ) ).
cnf(u4879,hypothesis,
( ~ product(g1,a,b,X0)
| product(g1,c,X0,a) ) ).
cnf(u5095,hypothesis,
( ~ product(g2,g,g,X0)
| product(g2,f,X0,h) ) ).
cnf(total_function1_1,axiom,
( ~ group_member(X2,X1)
| ~ group_member(X0,X1)
| product(X1,X0,X2,multiply(X1,X0,X2)) ) ).
cnf(u544,axiom,
( ~ product(X0,inverse(X0,X1),X1,X2)
| identity_for(X0) = X2 ) ).
cnf(u3050,hypothesis,
( ~ product(g2,X0,X1,h)
| product(g2,X2,X1,g)
| ~ product(g2,h,X0,X2) ) ).
cnf(u551,hypothesis,
product(g2,inverse(g2,X0),X0,f) ).
cnf(u4158,hypothesis,
( ~ product(g2,X0,inverse(g2,X0),X1)
| f = X1 ) ).
cnf(u754,hypothesis,
( ~ product(g2,f,X0,X1)
| product(g2,inverse(g2,X0),X1,f) ) ).
cnf(u4987,hypothesis,
( ~ product(g1,b,a,X0)
| product(g1,X0,b,c) ) ).
cnf(u3593,hypothesis,
( ~ product(g2,g,g,X0)
| h = X0 ) ).
cnf(u753,hypothesis,
( ~ product(g1,inverse(g1,X0),X0,X1)
| product(g1,a,X1,a) ) ).
cnf(u799,hypothesis,
( ~ product(g2,f,X0,X1)
| product(g2,inverse(g2,X1),X0,f) ) ).
cnf(u553,hypothesis,
a = inverse(g1,a) ).
cnf(u782,hypothesis,
( ~ product(g1,X0,inverse(g1,X0),X1)
| product(g1,X1,a,a) ) ).
cnf(u4877,hypothesis,
( ~ product(g1,b,b,X0)
| product(g1,b,X0,a) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP026-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n005.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 09:14:32 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 9.68/2.26 % (3712604)Input is clausal, will run a generic CNF schedule.
% 9.68/2.26 % (3712614)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=817264904:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.68/2.26 % (3712610)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1945523050:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.68/2.26 % (3712613)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1431346297:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.68/2.26 % (3712611)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=695029538:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.68/2.26 % (3712609)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=1639905039:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.68/2.26 % (3712615)dis-21_1_sil=8000:lcm=predicate:random_seed=2439520529: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)
% 9.68/2.26 % (3712612)lrs+10_1_sil=8000:sp=occurrence:random_seed=331238316:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.68/2.26 % (3712614)Instruction limit reached!
% 9.68/2.26 % (3712614)------------------------------
% 9.68/2.26 % (3712614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.26 % (3712614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.26 % (3712614)CaDiCaL version: 2.1.3
% 9.68/2.26 % (3712614)Termination reason: Instruction limit
% 9.68/2.26 % (3712614)Termination phase: Saturation
% 9.68/2.26 % (3712614)Time elapsed: 0.063 s
% 9.68/2.26 % (3712614)Peak memory usage: 89 MB
% 9.68/2.26 % (3712614)Instructions burned: 182 (million)
% 9.68/2.26 % (3712615)Instruction limit reached!
% 9.68/2.26 % (3712615)------------------------------
% 9.68/2.26 % (3712615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.26 % (3712615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.26 % (3712615)CaDiCaL version: 2.1.3
% 9.68/2.26 % (3712615)Termination reason: Instruction limit
% 9.68/2.26 % (3712615)Termination phase: Saturation
% 9.68/2.26 % (3712615)Time elapsed: 0.063 s
% 9.68/2.26 % (3712615)Peak memory usage: 88 MB
% 9.68/2.26 % (3712615)Instructions burned: 117 (million)
% 9.68/2.26 % (3712613)Instruction limit reached!
% 9.68/2.26 % (3712613)------------------------------
% 9.68/2.26 % (3712613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.26 % (3712613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.26 % (3712613)CaDiCaL version: 2.1.3
% 9.68/2.26 % (3712613)Termination reason: Instruction limit
% 9.68/2.26 % (3712613)Termination phase: Saturation
% 9.68/2.26 % (3712613)Time elapsed: 0.069 s
% 9.68/2.26 % (3712613)Peak memory usage: 88 MB
% 9.68/2.26 % (3712613)Instructions burned: 117 (million)
% 9.68/2.26 % (3712612)Instruction limit reached!
% 9.68/2.26 % (3712612)------------------------------
% 9.68/2.26 % (3712612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.26 % (3712612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.26 % (3712612)CaDiCaL version: 2.1.3
% 9.68/2.26 % (3712612)Termination reason: Instruction limit
% 9.68/2.26 % (3712612)Termination phase: Saturation
% 9.68/2.26 % (3712612)Time elapsed: 0.068 s
% 9.68/2.26 % (3712612)Peak memory usage: 88 MB
% 9.68/2.26 % (3712612)Instructions burned: 108 (million)
% 9.68/2.26 % (3712623)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=1385006309:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.68/2.26 % (3712623)Instruction limit reached!
% 9.68/2.26 % (3712623)------------------------------
% 9.68/2.26 % (3712623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.26 % (3712623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.26 % (3712623)CaDiCaL version: 2.1.3
% 9.68/2.26 % (3712623)Termination reason: Instruction limit
% 9.68/2.26 % (3712623)Termination phase: Saturation
% 9.68/2.26 % (3712623)Time elapsed: 0.054 s
% 9.68/2.26 % (3712623)Peak memory usage: 89 MB
% 9.68/2.26 % (3712623)Instructions burned: 146 (million)
% 9.68/2.26 % (3712625)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1283557966:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 19.07/3.66 % (3712626)lrs+10_64_to=lpo:sil=8000:random_seed=64887340:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 19.07/3.66 % (3712624)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4097577337: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)
% 19.07/3.66 % (3712626)Instruction limit reached!
% 19.07/3.66 % (3712626)------------------------------
% 19.07/3.66 % (3712626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.07/3.66 % (3712626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.07/3.66 % (3712626)CaDiCaL version: 2.1.3
% 19.07/3.66 % (3712626)Termination reason: Instruction limit
% 19.07/3.66 % (3712626)Termination phase: Saturation
% 19.07/3.66 % (3712626)Time elapsed: 0.081 s
% 19.07/3.66 % (3712626)Peak memory usage: 88 MB
% 19.07/3.66 % (3712626)Instructions burned: 126 (million)
% 19.07/3.66 % (3712624)Instruction limit reached!
% 19.07/3.66 % (3712624)------------------------------
% 19.07/3.66 % (3712624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.07/3.66 % (3712624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.07/3.66 % (3712624)CaDiCaL version: 2.1.3
% 19.07/3.66 % (3712624)Termination reason: Instruction limit
% 19.07/3.66 % (3712624)Termination phase: Saturation
% 19.07/3.66 % (3712624)Time elapsed: 0.095 s
% 19.07/3.66 % (3712624)Peak memory usage: 89 MB
% 19.07/3.66 % (3712624)Instructions burned: 189 (million)
% 19.07/3.66 % (3712628)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1563702642:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 19.07/3.66 % (3712625)Instruction limit reached!
% 19.07/3.66 % (3712625)------------------------------
% 19.07/3.66 % (3712625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.07/3.66 % (3712625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.07/3.66 % (3712625)CaDiCaL version: 2.1.3
% 19.07/3.66 % (3712625)Termination reason: Instruction limit
% 19.07/3.66 % (3712625)Termination phase: Saturation
% 19.07/3.66 % (3712625)Time elapsed: 0.121 s
% 19.07/3.66 % (3712625)Peak memory usage: 88 MB
% 19.07/3.66 % (3712625)Instructions burned: 219 (million)
% 19.07/3.66 % (3712628)Instruction limit reached!
% 19.07/3.66 % (3712628)------------------------------
% 19.07/3.66 % (3712628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.07/3.66 % (3712628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.07/3.66 % (3712628)CaDiCaL version: 2.1.3
% 19.07/3.66 % (3712628)Termination reason: Instruction limit
% 19.07/3.66 % (3712628)Termination phase: Saturation
% 19.07/3.66 % (3712628)Time elapsed: 0.070 s
% 19.07/3.66 % (3712628)Peak memory usage: 89 MB
% 19.07/3.66 % (3712628)Instructions burned: 196 (million)
% 19.07/3.66 % (3712632)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=916409612:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 19.07/3.66 % (3712633)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2607598310:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 19.07/3.66 % (3712635)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=472461992:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 19.07/3.66 % (3712636)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1570106596:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 19.07/3.66 % (3712635)Instruction limit reached!
% 19.07/3.66 % (3712635)------------------------------
% 19.07/3.66 % (3712635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.07/3.66 % (3712635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.07/3.66 % (3712635)CaDiCaL version: 2.1.3
% 19.07/3.66 % (3712635)Termination reason: Instruction limit
% 19.07/3.66 % (3712635)Termination phase: Saturation
% 19.07/3.66 % (3712635)Time elapsed: 0.054 s
% 19.07/3.66 % (3712635)Peak memory usage: 89 MB
% 19.07/3.66 % (3712635)Instructions burned: 106 (million)
% 19.07/3.66 % (3712632)Instruction limit reached!
% 19.07/3.66 % (3712632)------------------------------
% 19.07/3.66 % (3712632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.17/6.27 % (3712632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.17/6.27 % (3712632)CaDiCaL version: 2.1.3
% 38.17/6.27 % (3712632)Termination reason: Instruction limit
% 38.17/6.27 % (3712632)Termination phase: Saturation
% 38.17/6.27 % (3712632)Time elapsed: 0.108 s
% 38.17/6.27 % (3712632)Peak memory usage: 90 MB
% 38.17/6.27 % (3712632)Instructions burned: 158 (million)
% 38.17/6.27 % (3712636)Instruction limit reached!
% 38.17/6.27 % (3712636)------------------------------
% 38.17/6.27 % (3712636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.17/6.27 % (3712636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.17/6.27 % (3712636)CaDiCaL version: 2.1.3
% 38.17/6.27 % (3712636)Termination reason: Instruction limit
% 38.17/6.27 % (3712636)Termination phase: Saturation
% 38.17/6.27 % (3712636)Time elapsed: 0.037 s
% 38.17/6.27 % (3712636)Peak memory usage: 89 MB
% 38.17/6.27 % (3712636)Instructions burned: 110 (million)
% 38.17/6.27 % (3712643)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=151767596:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 38.17/6.27 % (3712642)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3961167228:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 38.17/6.27 % (3712641)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2439225781:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 38.17/6.27 % (3712643)Instruction limit reached!
% 38.17/6.27 % (3712643)------------------------------
% 38.17/6.27 % (3712643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.17/6.27 % (3712643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.17/6.27 % (3712643)CaDiCaL version: 2.1.3
% 38.17/6.27 % (3712643)Termination reason: Instruction limit
% 38.17/6.27 % (3712643)Termination phase: Saturation
% 38.17/6.27 % (3712643)Time elapsed: 0.049 s
% 38.17/6.27 % (3712643)Peak memory usage: 89 MB
% 38.17/6.27 % (3712643)Instructions burned: 137 (million)
% 38.17/6.27 % (3712647)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=199779197:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 38.17/6.27 % (3712641)Instruction limit reached!
% 38.17/6.27 % (3712641)------------------------------
% 38.17/6.27 % (3712641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.17/6.27 % (3712641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.17/6.27 % (3712641)CaDiCaL version: 2.1.3
% 38.17/6.27 % (3712641)Termination reason: Instruction limit
% 38.17/6.27 % (3712641)Termination phase: Saturation
% 38.17/6.27 % (3712641)Time elapsed: 0.144 s
% 38.17/6.27 % (3712641)Peak memory usage: 88 MB
% 38.17/6.27 % (3712641)Instructions burned: 242 (million)
% 38.17/6.27 % (3712647)Instruction limit reached!
% 38.17/6.27 % (3712647)------------------------------
% 38.17/6.27 % (3712647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.17/6.27 % (3712647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.17/6.27 % (3712647)CaDiCaL version: 2.1.3
% 38.17/6.27 % (3712647)Termination reason: Instruction limit
% 38.17/6.27 % (3712647)Termination phase: Saturation
% 38.17/6.27 % (3712647)Time elapsed: 0.139 s
% 38.17/6.27 % (3712647)Peak memory usage: 91 MB
% 38.17/6.27 % (3712647)Instructions burned: 501 (million)
% 38.17/6.27 % (3712649)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2286817964:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 38.17/6.27 % (3712650)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=466710336:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 38.17/6.27 % (3712649)Instruction limit reached!
% 38.17/6.27 % (3712649)------------------------------
% 38.17/6.27 % (3712649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.17/6.27 % (3712649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.17/6.27 % (3712649)CaDiCaL version: 2.1.3
% 38.17/6.27 % (3712649)Termination reason: Instruction limit
% 38.17/6.27 % (3712649)Termination phase: Saturation
% 38.17/6.27 % (3712649)Time elapsed: 0.116 s
% 38.17/6.27 % (3712649)Peak memory usage: 89 MB
% 38.17/6.27 % (3712649)Instructions burned: 192 (million)
% 38.17/6.27 % (3712650)Instruction limit reached!
% 38.17/6.27 % (3712650)------------------------------
% 46.54/7.56 % (3712650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.54/7.56 % (3712650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.54/7.56 % (3712650)CaDiCaL version: 2.1.3
% 46.54/7.56 % (3712650)Termination reason: Instruction limit
% 46.54/7.56 % (3712650)Termination phase: Saturation
% 46.54/7.56 % (3712650)Time elapsed: 0.088 s
% 46.54/7.56 % (3712650)Peak memory usage: 90 MB
% 46.54/7.56 % (3712650)Instructions burned: 266 (million)
% 46.54/7.56 % (3712653)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3548644729:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 46.54/7.56 % (3712654)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=3845441507:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi)
% 46.54/7.56 % (3712653)Instruction limit reached!
% 46.54/7.56 % (3712653)------------------------------
% 46.54/7.56 % (3712653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.54/7.56 % (3712653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.54/7.56 % (3712653)CaDiCaL version: 2.1.3
% 46.54/7.56 % (3712653)Termination reason: Instruction limit
% 46.54/7.56 % (3712653)Termination phase: Saturation
% 46.54/7.56 % (3712653)Time elapsed: 0.094 s
% 46.54/7.56 % (3712653)Peak memory usage: 89 MB
% 46.54/7.56 % (3712653)Instructions burned: 156 (million)
% 46.54/7.56 % (3712657)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2455742187:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi)
% 46.54/7.56 % (3712657)Instruction limit reached!
% 46.54/7.56 % (3712657)------------------------------
% 46.54/7.56 % (3712657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.54/7.56 % (3712657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.54/7.56 % (3712657)CaDiCaL version: 2.1.3
% 46.54/7.56 % (3712657)Termination reason: Instruction limit
% 46.54/7.56 % (3712657)Termination phase: Saturation
% 46.54/7.56 % (3712657)Time elapsed: 0.220 s
% 46.54/7.56 % (3712657)Peak memory usage: 89 MB
% 46.54/7.56 % (3712657)Instructions burned: 538 (million)
% 46.54/7.56 % (3712659)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=782406364:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi)
% 46.54/7.56 % (3712659)Instruction limit reached!
% 46.54/7.56 % (3712659)------------------------------
% 46.54/7.56 % (3712659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.54/7.56 % (3712659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.54/7.56 % (3712659)CaDiCaL version: 2.1.3
% 46.54/7.56 % (3712659)Termination reason: Instruction limit
% 46.54/7.56 % (3712659)Termination phase: Saturation
% 46.54/7.56 % (3712659)Time elapsed: 0.084 s
% 46.54/7.56 % (3712659)Peak memory usage: 89 MB
% 46.54/7.56 % (3712659)Instructions burned: 181 (million)
% 46.54/7.56 % (3712661)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=3043900834:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi)
% 46.54/7.56 % (3712654)Instruction limit reached!
% 46.54/7.56 % (3712654)------------------------------
% 46.54/7.56 % (3712654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.54/7.56 % (3712654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.54/7.56 % (3712654)CaDiCaL version: 2.1.3
% 46.54/7.56 % (3712654)Termination reason: Instruction limit
% 46.54/7.56 % (3712654)Termination phase: Saturation
% 46.54/7.56 % (3712654)Time elapsed: 1.032 s
% 46.54/7.56 % (3712654)Peak memory usage: 148 MB
% 46.54/7.56 % (3712654)Instructions burned: 3258 (million)
% 46.54/7.56 % (3712663)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=2125598557:i=412:gtgl=4:gtg=exists_all_2974 on theBenchmark for (2974ds/412Mi)
% 46.54/7.56 % (3712663)Instruction limit reached!
% 46.54/7.56 % (3712663)------------------------------
% 46.54/7.56 % (3712663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.54/7.56 % (3712663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.54/7.56 % (3712663)CaDiCaL version: 2.1.3
% 46.54/7.56 % (3712663)Termination reason: Instruction limit
% 46.54/7.56 % (3712663)Termination phase: Saturation
% 60.05/9.43 % (3712663)Time elapsed: 0.122 s
% 60.05/9.43 % (3712663)Peak memory usage: 91 MB
% 60.05/9.43 % (3712663)Instructions burned: 413 (million)
% 60.05/9.43 % (3712633)Instruction limit reached!
% 60.05/9.43 % (3712633)------------------------------
% 60.05/9.43 % (3712633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712633)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712633)Termination reason: Instruction limit
% 60.05/9.43 % (3712633)Termination phase: Saturation
% 60.05/9.43 % (3712633)Time elapsed: 2.200 s
% 60.05/9.43 % (3712633)Peak memory usage: 146 MB
% 60.05/9.43 % (3712633)Instructions burned: 3395 (million)
% 60.05/9.43 % (3712665)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=43574831:s2pl=no:i=8478:s2at=4:nm=6_2972 on theBenchmark for (2972ds/8478Mi)
% 60.05/9.43 % (3712666)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=728517372:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2971 on theBenchmark for (2971ds/303Mi)
% 60.05/9.43 % (3712666)Instruction limit reached!
% 60.05/9.43 % (3712666)------------------------------
% 60.05/9.43 % (3712666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712666)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712666)Termination reason: Instruction limit
% 60.05/9.43 % (3712666)Termination phase: Saturation
% 60.05/9.43 % (3712666)Time elapsed: 0.163 s
% 60.05/9.43 % (3712666)Peak memory usage: 90 MB
% 60.05/9.43 % (3712666)Instructions burned: 304 (million)
% 60.05/9.43 % (3712669)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3976261108:st=4:i=720:sd=3:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/720Mi)
% 60.05/9.43 % (3712669)Instruction limit reached!
% 60.05/9.43 % (3712669)------------------------------
% 60.05/9.43 % (3712669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712669)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712669)Termination reason: Instruction limit
% 60.05/9.43 % (3712669)Termination phase: Saturation
% 60.05/9.43 % (3712669)Time elapsed: 0.362 s
% 60.05/9.43 % (3712669)Peak memory usage: 91 MB
% 60.05/9.43 % (3712669)Instructions burned: 720 (million)
% 60.05/9.43 % (3712671)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=353854979:i=598:bs=on:bd=preordered:av=off:ss=axioms_2962 on theBenchmark for (2962ds/598Mi)
% 60.05/9.43 % (3712671)Instruction limit reached!
% 60.05/9.43 % (3712671)------------------------------
% 60.05/9.43 % (3712671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712671)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712671)Termination reason: Instruction limit
% 60.05/9.43 % (3712671)Termination phase: Saturation
% 60.05/9.43 % (3712671)Time elapsed: 0.318 s
% 60.05/9.43 % (3712671)Peak memory usage: 89 MB
% 60.05/9.43 % (3712671)Instructions burned: 598 (million)
% 60.05/9.43 % (3712642)Instruction limit reached!
% 60.05/9.43 % (3712642)------------------------------
% 60.05/9.43 % (3712642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712642)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712642)Termination reason: Instruction limit
% 60.05/9.43 % (3712642)Termination phase: Saturation
% 60.05/9.43 % (3712642)Time elapsed: 3.305 s
% 60.05/9.43 % (3712642)Peak memory usage: 148 MB
% 60.05/9.43 % (3712642)Instructions burned: 5209 (million)
% 60.05/9.43 % (3712673)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1106072181:i=2989:sd=3:ss=axioms:sgt=60_2957 on theBenchmark for (2957ds/2989Mi)
% 60.05/9.43 % (3712674)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=762053963:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2957 on theBenchmark for (2957ds/1997Mi)
% 60.05/9.43 % (3712665)Instruction limit reached!
% 60.05/9.43 % (3712665)------------------------------
% 60.05/9.43 % (3712665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712665)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712665)Termination reason: Instruction limit
% 60.05/9.43 % (3712665)Termination phase: Saturation
% 60.05/9.43 % (3712665)Time elapsed: 2.469 s
% 60.05/9.43 % (3712665)Peak memory usage: 199 MB
% 60.05/9.43 % (3712665)Instructions burned: 8480 (million)
% 60.05/9.43 % (3712677)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=643725686:i=2088:bd=preordered:av=off_2945 on theBenchmark for (2945ds/2088Mi)
% 60.05/9.43 % (3712674)Instruction limit reached!
% 60.05/9.43 % (3712674)------------------------------
% 60.05/9.43 % (3712674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712674)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712674)Termination reason: Instruction limit
% 60.05/9.43 % (3712674)Termination phase: Saturation
% 60.05/9.43 % (3712674)Time elapsed: 1.319 s
% 60.05/9.43 % (3712674)Peak memory usage: 136 MB
% 60.05/9.43 % (3712674)Instructions burned: 1999 (million)
% 60.05/9.43 % (3712679)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1384394641:i=1098:nicw=on_2942 on theBenchmark for (2942ds/1098Mi)
% 60.05/9.43 % (3712673)Instruction limit reached!
% 60.05/9.43 % (3712673)------------------------------
% 60.05/9.43 % (3712673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712673)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712673)Termination reason: Instruction limit
% 60.05/9.43 % (3712673)Termination phase: Saturation
% 60.05/9.43 % (3712673)Time elapsed: 1.915 s
% 60.05/9.43 % (3712673)Peak memory usage: 142 MB
% 60.05/9.43 % (3712673)Instructions burned: 2990 (million)
% 60.05/9.43 % (3712677)Instruction limit reached!
% 60.05/9.43 % (3712677)------------------------------
% 60.05/9.43 % (3712677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712677)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712677)Termination reason: Instruction limit
% 60.05/9.43 % (3712677)Termination phase: Saturation
% 60.05/9.43 % (3712677)Time elapsed: 0.741 s
% 60.05/9.43 % (3712677)Peak memory usage: 136 MB
% 60.05/9.43 % (3712677)Instructions burned: 2088 (million)
% 60.05/9.43 % (3712682)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2701846041:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2936 on theBenchmark for (2936ds/2942Mi)
% 60.05/9.43 % (3712679)Instruction limit reached!
% 60.05/9.43 % (3712679)------------------------------
% 60.05/9.43 % (3712679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712679)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712679)Termination reason: Instruction limit
% 60.05/9.43 % (3712679)Termination phase: Saturation
% 60.05/9.43 % (3712679)Time elapsed: 0.564 s
% 60.05/9.43 % (3712679)Peak memory usage: 106 MB
% 60.05/9.43 % (3712679)Instructions burned: 1098 (million)
% 60.05/9.43 % (3712681)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=813473698:i=433:bd=preordered_2937 on theBenchmark for (2937ds/433Mi)
% 60.05/9.43 % (3712685)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=584163485:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2935 on theBenchmark for (2935ds/6922Mi)
% 60.05/9.43 % (3712681)Instruction limit reached!
% 60.05/9.43 % (3712681)------------------------------
% 60.05/9.43 % (3712681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712681)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712681)Termination reason: Instruction limit
% 60.05/9.43 % (3712681)Termination phase: Saturation
% 60.05/9.43 % (3712681)Time elapsed: 0.268 s
% 60.05/9.43 % (3712681)Peak memory usage: 91 MB
% 60.05/9.43 % (3712681)Instructions burned: 434 (million)
% 60.05/9.43 % (3712687)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=1940929785:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2933 on theBenchmark for (2933ds/596Mi)
% 60.05/9.43 % (3712687)Instruction limit reached!
% 60.05/9.43 % (3712687)------------------------------
% 60.05/9.43 % (3712687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.43 % (3712687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.43 % (3712687)CaDiCaL version: 2.1.3
% 60.05/9.43 % (3712687)Termination reason: Instruction limit
% 60.05/9.43 % (3712687)Termination phase: Saturation
% 60.05/9.43 % (3712687)Time elapsed: 0.284 s
% 60.05/9.43 % (3712687)Peak memory usage: 96 MB
% 60.05/9.43 % (3712687)Instructions burned: 596 (million)
% 60.05/9.43 % (3712689)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=90710134:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2928 on theBenchmark for (2928ds/4123Mi)
% 60.05/9.43 % (3712661)Instruction limit reached!
% 60.05/9.44 % (3712661)------------------------------
% 60.05/9.44 % (3712661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.44 % (3712661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.44 % (3712661)CaDiCaL version: 2.1.3
% 60.05/9.44 % (3712661)Termination reason: Instruction limit
% 60.05/9.44 % (3712661)Termination phase: Saturation
% 60.05/9.44 % (3712661)Time elapsed: 5.344 s
% 60.05/9.44 % (3712661)Peak memory usage: 155 MB
% 60.05/9.44 % (3712661)Instructions burned: 10310 (million)
% 60.05/9.44 % (3712691)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1467252733:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2922 on theBenchmark for (2922ds/16411Mi)
% 60.05/9.44 % (3712682)Instruction limit reached!
% 60.05/9.44 % (3712682)------------------------------
% 60.05/9.44 % (3712682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.44 % (3712682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.44 % (3712682)CaDiCaL version: 2.1.3
% 60.05/9.44 % (3712682)Termination reason: Instruction limit
% 60.05/9.44 % (3712682)Termination phase: Saturation
% 60.05/9.44 % (3712682)Time elapsed: 1.663 s
% 60.05/9.44 % (3712682)Peak memory usage: 142 MB
% 60.05/9.44 % (3712682)Instructions burned: 2943 (million)
% 60.05/9.44 % (3712693)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=678995191:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2919 on theBenchmark for (2919ds/1670Mi)
% 60.05/9.44 % (3712691)First to succeed.
% 60.05/9.44 % (3712691)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3712604"
% 60.05/9.44 % SZS status Satisfiable for theBenchmark
% 60.05/9.44 % SZS output start Saturation.
% See solution above
% 61.19/9.64 % SZS output start Definitions and Model Updates.
% 61.19/9.64 % SZS output end Definitions and Model Updates.
% 61.19/9.64 % (3712691)------------------------------
% 61.19/9.64 % (3712691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.19/9.64 % (3712691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.19/9.64 % (3712691)CaDiCaL version: 2.1.3
% 61.19/9.64 % (3712691)Termination reason: Satisfiable
% 61.19/9.64 % (3712691)Time elapsed: 0.492 s
% 61.19/9.64 % (3712691)Peak memory usage: 131 MB
% 61.19/9.64 % (3712691)Instructions burned: 1324 (million)
% 61.19/9.64 % (3712691)------------------------------
% 61.19/9.64 % (3712691)------------------------------
% 61.19/9.64 % (3712604)Success in time 8.568 s
% 61.19/9.64 % Vampire exiting
%------------------------------------------------------------------------------