%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP002-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:16:19 AM UTC 2026
% Result : Unsatisfiable 151.28s 25.69s
% Output : Refutation 151.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 18
% Syntax : Number of formulae : 317 ( 317 unt; 0 def)
% Number of atoms : 317 ( 316 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 9 con; 0-4 aty)
% Number of variables : 370 ( 370 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq2(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f2,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom_001) ).
fof(f3,axiom,
! [X0] : product(identity,X0,X0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_identity) ).
fof(f4,axiom,
! [X0] : product(X0,identity,X0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_identity) ).
fof(f5,plain,
! [X0] : true = product(X0,identity,X0),
inference(reorient_equations,[],[f4]) ).
fof(f6,axiom,
! [X0] : product(inverse(X0),X0,identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_inverse) ).
fof(f7,plain,
! [X0] : true = product(inverse(X0),X0,identity),
inference(reorient_equations,[],[f6]) ).
fof(f8,axiom,
! [X0] : product(X0,inverse(X0),identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_inverse) ).
fof(f9,plain,
! [X0] : true = product(X0,inverse(X0),identity),
inference(reorient_equations,[],[f8]) ).
fof(f10,axiom,
! [X0,X1] : product(X0,X1,multiply(X0,X1)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',total_function1) ).
fof(f11,plain,
! [X0,X1] : true = product(X0,X1,multiply(X0,X1)),
inference(reorient_equations,[],[f10]) ).
fof(f12,axiom,
! [X2,X3,X0,X1] : ifeq2(product(X0,X1,X2),true,ifeq2(product(X0,X1,X3),true,X3,X2),X2) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',total_function2) ).
fof(f13,axiom,
! [X2,X3,X0,X1,X4,X5] : ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(product(X5,X3,X0),true,product(X5,X4,X2),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity1) ).
fof(f14,plain,
! [X2,X3,X0,X1,X4,X5] : true = ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(product(X5,X3,X0),true,product(X5,X4,X2),true),true),true),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X2,X3,X0,X1,X4,X5] : ifeq(product(X0,X1,X2),true,ifeq(product(X3,X2,X4),true,ifeq(product(X3,X0,X5),true,product(X5,X1,X4),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity2) ).
fof(f16,plain,
! [X2,X3,X0,X1,X4,X5] : true = ifeq(product(X0,X1,X2),true,ifeq(product(X3,X2,X4),true,ifeq(product(X3,X0,X5),true,product(X5,X1,X4),true),true),true),
inference(reorient_equations,[],[f15]) ).
fof(f17,axiom,
! [X0,X1] : ifeq(product(X0,X0,X1),true,product(X0,X1,identity),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_cubed_is_identity_1) ).
fof(f18,plain,
! [X0,X1] : true = ifeq(product(X0,X0,X1),true,product(X0,X1,identity),true),
inference(reorient_equations,[],[f17]) ).
fof(f19,axiom,
! [X0,X1] : ifeq(product(X0,X0,X1),true,product(X1,X0,identity),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_cubed_is_identity_2) ).
fof(f20,plain,
! [X0,X1] : true = ifeq(product(X0,X0,X1),true,product(X1,X0,identity),true),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
product(a,b,c) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_times_b_is_c) ).
fof(f22,plain,
true = product(a,b,c),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
product(c,inverse(a),d) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_times_inverse_a_is_d) ).
fof(f24,plain,
true = product(c,inverse(a),d),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
product(d,inverse(b),h) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_times_inverse_b_is_h) ).
fof(f26,plain,
true = product(d,inverse(b),h),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
product(h,b,j) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_times_b_is_j) ).
fof(f28,plain,
true = product(h,b,j),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
product(j,inverse(h),k) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',j_times_inverse_h_is_k) ).
fof(f30,plain,
true = product(j,inverse(h),k),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
product(k,inverse(b),identity) != true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_k_times_inverse_b_is_e) ).
fof(f32,plain,
true != product(k,inverse(b),identity),
inference(reorient_equations,[],[f31]) ).
fof(f34,plain,
! [X0] : true = ifeq(true,true,product(X0,multiply(X0,X0),identity),true),
inference(superposition,[],[f18,f11]) ).
fof(f41,plain,
! [X0] : true = ifeq(true,true,product(multiply(X0,X0),X0,identity),true),
inference(superposition,[],[f20,f11]) ).
fof(f47,plain,
! [X0,X1] : ifeq2(true,true,ifeq2(product(identity,X0,X1),true,X1,X0),X0) = X0,
inference(superposition,[],[f12,f3]) ).
fof(f49,plain,
! [X2,X0,X1] : multiply(X0,X1) = ifeq2(true,true,ifeq2(product(X0,X1,X2),true,X2,multiply(X0,X1)),multiply(X0,X1)),
inference(superposition,[],[f12,f11]) ).
fof(f50,plain,
! [X0,X1] : ifeq2(true,true,ifeq2(product(X0,identity,X1),true,X1,X0),X0) = X0,
inference(superposition,[],[f12,f5]) ).
fof(f57,plain,
! [X0,X1] : ifeq2(product(identity,X0,X1),true,ifeq2(true,true,X0,X1),X1) = X1,
inference(superposition,[],[f12,f3]) ).
fof(f59,plain,
! [X2,X0,X1] : ifeq2(product(X0,X1,X2),true,ifeq2(true,true,multiply(X0,X1),X2),X2) = X2,
inference(superposition,[],[f12,f11]) ).
fof(f60,plain,
! [X0,X1] : ifeq2(product(X0,identity,X1),true,ifeq2(true,true,X0,X1),X1) = X1,
inference(superposition,[],[f12,f5]) ).
fof(f65,plain,
! [X0] : ifeq2(product(a,b,X0),true,ifeq2(true,true,c,X0),X0) = X0,
inference(superposition,[],[f12,f22]) ).
fof(f68,plain,
! [X0] : ifeq2(product(a,b,X0),true,c,X0) = X0,
inference(forward_demodulation,[],[f65,f1]) ).
fof(f73,plain,
! [X0,X1] : ifeq2(product(X0,identity,X1),true,X0,X1) = X1,
inference(forward_demodulation,[],[f60,f1]) ).
fof(f74,plain,
! [X2,X0,X1] : ifeq2(product(X0,X1,X2),true,multiply(X0,X1),X2) = X2,
inference(forward_demodulation,[],[f59,f1]) ).
fof(f76,plain,
! [X0,X1] : ifeq2(product(identity,X0,X1),true,X0,X1) = X1,
inference(forward_demodulation,[],[f57,f1]) ).
fof(f93,plain,
! [X2,X3,X0,X1,X4] : true = ifeq(product(X0,X1,X2),true,ifeq(true,true,ifeq(product(X4,X3,X0),true,product(X4,multiply(X3,X1),X2),true),true),true),
inference(superposition,[],[f14,f11]) ).
fof(f96,plain,
! [X2,X0,X1] : true = ifeq(product(X0,inverse(a),X1),true,ifeq(true,true,ifeq(product(X2,c,X0),true,product(X2,d,X1),true),true),true),
inference(superposition,[],[f14,f24]) ).
fof(f97,plain,
! [X2,X0,X1] : true = ifeq(product(X0,inverse(b),X1),true,ifeq(true,true,ifeq(product(X2,d,X0),true,product(X2,h,X1),true),true),true),
inference(superposition,[],[f14,f26]) ).
fof(f98,plain,
! [X2,X0,X1] : true = ifeq(product(X0,inverse(h),X1),true,ifeq(true,true,ifeq(product(X2,j,X0),true,product(X2,k,X1),true),true),true),
inference(superposition,[],[f14,f30]) ).
fof(f99,plain,
! [X2,X0,X1] : true = ifeq(product(X0,b,X1),true,ifeq(true,true,ifeq(product(X2,a,X0),true,product(X2,c,X1),true),true),true),
inference(superposition,[],[f14,f22]) ).
fof(f100,plain,
! [X2,X0,X1] : true = ifeq(product(X0,b,X1),true,ifeq(true,true,ifeq(product(X2,h,X0),true,product(X2,j,X1),true),true),true),
inference(superposition,[],[f14,f28]) ).
fof(f102,plain,
! [X2,X3,X0,X1] : true = ifeq(product(identity,X0,X1),true,ifeq(product(X2,X0,X3),true,ifeq(true,true,product(inverse(X2),X3,X1),true),true),true),
inference(superposition,[],[f14,f7]) ).
fof(f103,plain,
! [X2,X3,X0,X1,X4] : true = ifeq(product(multiply(X0,X1),X2,X3),true,ifeq(product(X1,X2,X4),true,ifeq(true,true,product(X0,X4,X3),true),true),true),
inference(superposition,[],[f14,f11]) ).
fof(f105,plain,
! [X2,X3,X0,X1] : true = ifeq(product(identity,X0,X1),true,ifeq(product(inverse(X2),X0,X3),true,ifeq(true,true,product(X2,X3,X1),true),true),true),
inference(superposition,[],[f14,f9]) ).
fof(f107,plain,
! [X2,X0,X1] : true = ifeq(product(h,X0,X1),true,ifeq(product(inverse(b),X0,X2),true,ifeq(true,true,product(d,X2,X1),true),true),true),
inference(superposition,[],[f14,f26]) ).
fof(f109,plain,
! [X2,X0,X1] : true = ifeq(product(c,X0,X1),true,ifeq(product(b,X0,X2),true,ifeq(true,true,product(a,X2,X1),true),true),true),
inference(superposition,[],[f14,f22]) ).
fof(f124,plain,
! [X2,X0,X1] : true = ifeq(product(c,X0,X1),true,ifeq(product(b,X0,X2),true,product(a,X2,X1),true),true),
inference(forward_demodulation,[],[f109,f2]) ).
fof(f126,plain,
! [X2,X0,X1] : true = ifeq(product(h,X0,X1),true,ifeq(product(inverse(b),X0,X2),true,product(d,X2,X1),true),true),
inference(forward_demodulation,[],[f107,f2]) ).
fof(f128,plain,
! [X2,X3,X0,X1] : true = ifeq(product(identity,X0,X1),true,ifeq(product(inverse(X2),X0,X3),true,product(X2,X3,X1),true),true),
inference(forward_demodulation,[],[f105,f2]) ).
fof(f130,plain,
! [X2,X3,X0,X1,X4] : true = ifeq(product(multiply(X0,X1),X2,X3),true,ifeq(product(X1,X2,X4),true,product(X0,X4,X3),true),true),
inference(forward_demodulation,[],[f103,f2]) ).
fof(f131,plain,
! [X2,X3,X0,X1] : true = ifeq(product(identity,X0,X1),true,ifeq(product(X2,X0,X3),true,product(inverse(X2),X3,X1),true),true),
inference(forward_demodulation,[],[f102,f2]) ).
fof(f133,plain,
! [X2,X0,X1] : true = ifeq(product(X0,b,X1),true,ifeq(product(X2,h,X0),true,product(X2,j,X1),true),true),
inference(forward_demodulation,[],[f100,f2]) ).
fof(f134,plain,
! [X2,X0,X1] : true = ifeq(product(X0,b,X1),true,ifeq(product(X2,a,X0),true,product(X2,c,X1),true),true),
inference(forward_demodulation,[],[f99,f2]) ).
fof(f135,plain,
! [X2,X0,X1] : true = ifeq(product(X0,inverse(h),X1),true,ifeq(product(X2,j,X0),true,product(X2,k,X1),true),true),
inference(forward_demodulation,[],[f98,f2]) ).
fof(f136,plain,
! [X2,X0,X1] : true = ifeq(product(X0,inverse(b),X1),true,ifeq(product(X2,d,X0),true,product(X2,h,X1),true),true),
inference(forward_demodulation,[],[f97,f2]) ).
fof(f137,plain,
! [X2,X0,X1] : true = ifeq(product(X0,inverse(a),X1),true,ifeq(product(X2,c,X0),true,product(X2,d,X1),true),true),
inference(forward_demodulation,[],[f96,f2]) ).
fof(f140,plain,
! [X2,X3,X0,X1,X4] : true = ifeq(product(X0,X1,X2),true,ifeq(product(X4,X3,X0),true,product(X4,multiply(X3,X1),X2),true),true),
inference(forward_demodulation,[],[f93,f2]) ).
fof(f157,plain,
! [X2,X3,X0,X1] : true = ifeq(product(X0,X1,identity),true,ifeq(true,true,ifeq(product(X2,X0,X3),true,product(X3,X1,X2),true),true),true),
inference(superposition,[],[f16,f5]) ).
fof(f166,plain,
! [X2,X3,X0,X1,X4] : true = ifeq(product(X0,X1,X2),true,ifeq(product(X3,X2,X4),true,ifeq(true,true,product(multiply(X3,X0),X1,X4),true),true),true),
inference(superposition,[],[f16,f11]) ).
fof(f169,plain,
! [X2,X0,X1] : true = ifeq(product(inverse(a),X0,X1),true,ifeq(product(c,X1,X2),true,ifeq(true,true,product(d,X0,X2),true),true),true),
inference(superposition,[],[f16,f24]) ).
fof(f172,plain,
! [X2,X0,X1] : true = ifeq(product(b,X0,X1),true,ifeq(product(a,X1,X2),true,ifeq(true,true,product(c,X0,X2),true),true),true),
inference(superposition,[],[f16,f22]) ).
fof(f187,plain,
! [X2,X0,X1] : true = ifeq(product(b,X0,X1),true,ifeq(product(a,X1,X2),true,product(c,X0,X2),true),true),
inference(forward_demodulation,[],[f172,f2]) ).
fof(f190,plain,
! [X2,X0,X1] : true = ifeq(product(inverse(a),X0,X1),true,ifeq(product(c,X1,X2),true,product(d,X0,X2),true),true),
inference(forward_demodulation,[],[f169,f2]) ).
fof(f193,plain,
! [X2,X3,X0,X1,X4] : true = ifeq(product(X0,X1,X2),true,ifeq(product(X3,X2,X4),true,product(multiply(X3,X0),X1,X4),true),true),
inference(forward_demodulation,[],[f166,f2]) ).
fof(f202,plain,
! [X2,X3,X0,X1] : true = ifeq(product(X0,X1,identity),true,ifeq(product(X2,X0,X3),true,product(X3,X1,X2),true),true),
inference(forward_demodulation,[],[f157,f2]) ).
fof(f207,plain,
multiply(a,b) = ifeq2(true,true,c,multiply(a,b)),
inference(superposition,[],[f68,f11]) ).
fof(f209,plain,
c = multiply(a,b),
inference(forward_demodulation,[],[f207,f1]) ).
fof(f283,plain,
! [X0,X1] : true = ifeq(product(c,X0,X1),true,ifeq(true,true,product(a,multiply(b,X0),X1),true),true),
inference(superposition,[],[f124,f11]) ).
fof(f292,plain,
! [X0,X1] : true = ifeq(product(c,X0,X1),true,product(a,multiply(b,X0),X1),true),
inference(forward_demodulation,[],[f283,f2]) ).
fof(f295,plain,
! [X0] : true = ifeq(true,true,ifeq(product(X0,h,identity),true,product(X0,j,b),true),true),
inference(superposition,[],[f133,f3]) ).
fof(f299,plain,
! [X0] : true = ifeq(product(identity,b,X0),true,ifeq(true,true,product(inverse(h),j,X0),true),true),
inference(superposition,[],[f133,f7]) ).
fof(f309,plain,
! [X0] : true = ifeq(product(identity,b,X0),true,product(inverse(h),j,X0),true),
inference(forward_demodulation,[],[f299,f2]) ).
fof(f318,plain,
! [X0] : true = ifeq(true,true,ifeq(product(X0,a,identity),true,product(X0,c,b),true),true),
inference(superposition,[],[f134,f3]) ).
fof(f322,plain,
! [X0] : true = ifeq(product(identity,b,X0),true,ifeq(true,true,product(inverse(a),c,X0),true),true),
inference(superposition,[],[f134,f7]) ).
fof(f323,plain,
! [X0,X1] : true = ifeq(product(multiply(X0,a),b,X1),true,ifeq(true,true,product(X0,c,X1),true),true),
inference(superposition,[],[f134,f11]) ).
fof(f331,plain,
! [X0,X1] : true = ifeq(product(multiply(X0,a),b,X1),true,product(X0,c,X1),true),
inference(forward_demodulation,[],[f323,f2]) ).
fof(f332,plain,
! [X0] : true = ifeq(product(identity,b,X0),true,product(inverse(a),c,X0),true),
inference(forward_demodulation,[],[f322,f2]) ).
fof(f353,plain,
! [X0] : true = ifeq(product(b,X0,identity),true,ifeq(true,true,product(c,X0,a),true),true),
inference(superposition,[],[f187,f5]) ).
fof(f362,plain,
! [X0] : true = ifeq(product(b,X0,identity),true,product(c,X0,a),true),
inference(forward_demodulation,[],[f353,f2]) ).
fof(f418,plain,
! [X0] : true = ifeq(product(h,b,X0),true,ifeq(true,true,product(d,identity,X0),true),true),
inference(superposition,[],[f126,f7]) ).
fof(f429,plain,
! [X0] : true = ifeq(product(h,b,X0),true,product(d,identity,X0),true),
inference(forward_demodulation,[],[f418,f2]) ).
fof(f454,plain,
! [X0,X1] : true = ifeq(product(multiply(X0,j),inverse(h),X1),true,ifeq(true,true,product(X0,k,X1),true),true),
inference(superposition,[],[f135,f11]) ).
fof(f462,plain,
! [X0,X1] : true = ifeq(product(multiply(X0,j),inverse(h),X1),true,product(X0,k,X1),true),
inference(forward_demodulation,[],[f454,f2]) ).
fof(f472,plain,
! [X0,X1] : true = ifeq(product(multiply(X0,d),inverse(b),X1),true,ifeq(true,true,product(X0,h,X1),true),true),
inference(superposition,[],[f136,f11]) ).
fof(f480,plain,
! [X0,X1] : true = ifeq(product(multiply(X0,d),inverse(b),X1),true,product(X0,h,X1),true),
inference(forward_demodulation,[],[f472,f2]) ).
fof(f490,plain,
! [X0,X1] : true = ifeq(product(multiply(X0,c),inverse(a),X1),true,ifeq(true,true,product(X0,d,X1),true),true),
inference(superposition,[],[f137,f11]) ).
fof(f498,plain,
! [X0,X1] : true = ifeq(product(multiply(X0,c),inverse(a),X1),true,product(X0,d,X1),true),
inference(forward_demodulation,[],[f490,f2]) ).
fof(f536,plain,
! [X0,X1] : true = ifeq(product(inverse(a),X0,X1),true,ifeq(true,true,product(d,X0,multiply(c,X1)),true),true),
inference(superposition,[],[f190,f11]) ).
fof(f537,plain,
! [X0] : true = ifeq(product(inverse(a),X0,identity),true,ifeq(true,true,product(d,X0,c),true),true),
inference(superposition,[],[f190,f5]) ).
fof(f546,plain,
! [X0] : true = ifeq(product(inverse(a),X0,identity),true,product(d,X0,c),true),
inference(forward_demodulation,[],[f537,f2]) ).
fof(f547,plain,
! [X0,X1] : true = ifeq(product(inverse(a),X0,X1),true,product(d,X0,multiply(c,X1)),true),
inference(forward_demodulation,[],[f536,f2]) ).
fof(f990,plain,
! [X0] : multiply(identity,X0) = ifeq2(true,true,X0,multiply(identity,X0)),
inference(superposition,[],[f76,f11]) ).
fof(f994,plain,
! [X0] : multiply(identity,X0) = X0,
inference(forward_demodulation,[],[f990,f1]) ).
fof(f1007,plain,
! [X0] : true = product(X0,multiply(X0,X0),identity),
inference(superposition,[],[f34,f2]) ).
fof(f1014,plain,
! [X0] : true = product(multiply(X0,X0),X0,identity),
inference(superposition,[],[f41,f2]) ).
fof(f1043,plain,
! [X0,X1] : ifeq2(product(identity,X0,X1),true,X1,X0) = X0,
inference(superposition,[],[f47,f1]) ).
fof(f1056,plain,
! [X0,X1] : ifeq2(product(X0,identity,X1),true,X1,X0) = X0,
inference(superposition,[],[f50,f1]) ).
fof(f1151,plain,
! [X2,X0,X1] : multiply(X0,X1) = ifeq2(product(X0,X1,X2),true,X2,multiply(X0,X1)),
inference(superposition,[],[f49,f1]) ).
fof(f1406,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(product(X1,X0,X2),true,product(X2,inverse(X0),X1),true),true),
inference(superposition,[],[f202,f9]) ).
fof(f1408,plain,
! [X0,X1] : true = ifeq(product(X0,X1,identity),true,ifeq(true,true,product(identity,X1,inverse(X0)),true),true),
inference(superposition,[],[f202,f7]) ).
fof(f1409,plain,
! [X2,X0,X1] : true = ifeq(product(X0,X1,identity),true,ifeq(true,true,product(multiply(X2,X0),X1,X2),true),true),
inference(superposition,[],[f202,f11]) ).
fof(f1442,plain,
! [X2,X0,X1] : true = ifeq(product(X0,X1,identity),true,product(multiply(X2,X0),X1,X2),true),
inference(forward_demodulation,[],[f1409,f2]) ).
fof(f1443,plain,
! [X0,X1] : true = ifeq(product(X0,X1,identity),true,product(identity,X1,inverse(X0)),true),
inference(forward_demodulation,[],[f1408,f2]) ).
fof(f1486,plain,
! [X2,X0,X1] : true = ifeq(product(identity,X0,X1),true,ifeq(true,true,product(X2,multiply(inverse(X2),X0),X1),true),true),
inference(superposition,[],[f128,f11]) ).
fof(f1501,plain,
! [X2,X0,X1] : true = ifeq(product(identity,X0,X1),true,product(X2,multiply(inverse(X2),X0),X1),true),
inference(forward_demodulation,[],[f1486,f2]) ).
fof(f1505,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(product(X1,X0,X2),true,product(inverse(X1),X2,X0),true),true),
inference(superposition,[],[f131,f3]) ).
fof(f1510,plain,
! [X0,X1] : true = ifeq(product(identity,X0,X1),true,ifeq(true,true,product(inverse(inverse(X0)),identity,X1),true),true),
inference(superposition,[],[f131,f7]) ).
fof(f1511,plain,
! [X2,X0,X1] : true = ifeq(product(identity,X0,X1),true,ifeq(true,true,product(inverse(X2),multiply(X2,X0),X1),true),true),
inference(superposition,[],[f131,f11]) ).
fof(f1531,plain,
! [X2,X0,X1] : true = ifeq(product(identity,X0,X1),true,product(inverse(X2),multiply(X2,X0),X1),true),
inference(forward_demodulation,[],[f1511,f2]) ).
fof(f1532,plain,
! [X0,X1] : true = ifeq(product(identity,X0,X1),true,product(inverse(inverse(X0)),identity,X1),true),
inference(forward_demodulation,[],[f1510,f2]) ).
fof(f1729,plain,
! [X2,X3,X0,X1] : true = ifeq(product(multiply(X0,X1),X2,X3),true,ifeq(true,true,product(X0,multiply(X1,X2),X3),true),true),
inference(superposition,[],[f130,f11]) ).
fof(f1757,plain,
! [X2,X3,X0,X1] : true = ifeq(product(multiply(X0,X1),X2,X3),true,product(X0,multiply(X1,X2),X3),true),
inference(forward_demodulation,[],[f1729,f2]) ).
fof(f1760,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(product(X1,X2,identity),true,product(X1,multiply(X2,X0),X0),true),true),
inference(superposition,[],[f140,f3]) ).
fof(f1814,plain,
! [X2,X3,X0,X1] : true = ifeq(product(X0,X1,X2),true,ifeq(true,true,product(multiply(X3,X0),X1,multiply(X3,X2)),true),true),
inference(superposition,[],[f193,f11]) ).
fof(f1838,plain,
! [X2,X3,X0,X1] : true = ifeq(product(X0,X1,X2),true,product(multiply(X3,X0),X1,multiply(X3,X2)),true),
inference(forward_demodulation,[],[f1814,f2]) ).
fof(f3148,plain,
true = ifeq(true,true,product(c,inverse(b),a),true),
inference(superposition,[],[f362,f9]) ).
fof(f3240,plain,
true = ifeq(true,true,product(d,identity,j),true),
inference(superposition,[],[f429,f28]) ).
fof(f3264,plain,
true = product(d,identity,j),
inference(superposition,[],[f3240,f2]) ).
fof(f3280,plain,
true = ifeq(true,true,product(inverse(h),j,b),true),
inference(superposition,[],[f309,f3]) ).
fof(f3292,plain,
j = ifeq2(true,true,d,j),
inference(superposition,[],[f73,f3264]) ).
fof(f3444,plain,
d = j,
inference(forward_demodulation,[],[f3292,f1]) ).
fof(f3448,plain,
true = ifeq(true,true,product(inverse(a),c,b),true),
inference(superposition,[],[f332,f3]) ).
fof(f3778,plain,
true = ifeq(true,true,product(d,a,c),true),
inference(superposition,[],[f546,f7]) ).
fof(f3971,plain,
true = product(d,a,c),
inference(superposition,[],[f3778,f2]) ).
fof(f4001,plain,
multiply(d,a) = ifeq2(true,true,ifeq2(true,true,c,multiply(d,a)),multiply(d,a)),
inference(superposition,[],[f49,f3971]) ).
fof(f4103,plain,
multiply(d,a) = ifeq2(true,true,c,multiply(d,a)),
inference(forward_demodulation,[],[f4001,f1]) ).
fof(f4121,plain,
c = multiply(d,a),
inference(forward_demodulation,[],[f4103,f1]) ).
fof(f4402,plain,
! [X0] : true = ifeq(true,true,product(a,multiply(b,X0),multiply(c,X0)),true),
inference(superposition,[],[f292,f11]) ).
fof(f4419,plain,
! [X0] : true = ifeq(true,true,product(X0,c,multiply(multiply(X0,a),b)),true),
inference(superposition,[],[f331,f11]) ).
fof(f4743,plain,
! [X0,X1] : true = ifeq(product(multiply(X0,d),inverse(h),X1),true,product(X0,k,X1),true),
inference(forward_demodulation,[],[f462,f3444]) ).
fof(f4744,plain,
! [X0] : true = ifeq(true,true,product(X0,h,multiply(multiply(X0,d),inverse(b))),true),
inference(superposition,[],[f480,f11]) ).
fof(f4755,plain,
! [X0] : true = ifeq(true,true,product(X0,d,multiply(multiply(X0,c),inverse(a))),true),
inference(superposition,[],[f498,f11]) ).
fof(f4901,plain,
! [X0] : true = ifeq(true,true,product(X0,k,multiply(multiply(X0,d),inverse(h))),true),
inference(superposition,[],[f4743,f11]) ).
fof(f5012,plain,
! [X0] : true = ifeq(true,true,ifeq(product(X0,h,identity),true,product(X0,d,b),true),true),
inference(forward_demodulation,[],[f295,f3444]) ).
fof(f5646,plain,
true = product(c,inverse(b),a),
inference(superposition,[],[f3148,f2]) ).
fof(f5833,plain,
true = ifeq(true,true,product(inverse(h),d,b),true),
inference(forward_demodulation,[],[f3280,f3444]) ).
fof(f5843,plain,
true = product(inverse(a),c,b),
inference(superposition,[],[f3448,f2]) ).
fof(f5857,plain,
true = ifeq(true,true,product(d,c,multiply(c,b)),true),
inference(superposition,[],[f547,f5843]) ).
fof(f7245,plain,
true = product(inverse(h),d,b),
inference(superposition,[],[f5833,f2]) ).
fof(f7284,plain,
multiply(inverse(h),d) = ifeq2(true,true,ifeq2(true,true,b,multiply(inverse(h),d)),multiply(inverse(h),d)),
inference(superposition,[],[f49,f7245]) ).
fof(f7386,plain,
multiply(inverse(h),d) = ifeq2(true,true,b,multiply(inverse(h),d)),
inference(forward_demodulation,[],[f7284,f1]) ).
fof(f7408,plain,
b = multiply(inverse(h),d),
inference(forward_demodulation,[],[f7386,f1]) ).
fof(f13887,plain,
true = ifeq(true,true,product(c,multiply(b,b),a),true),
inference(superposition,[],[f362,f1007]) ).
fof(f13912,plain,
true = ifeq(true,true,product(a,multiply(b,multiply(c,c)),identity),true),
inference(superposition,[],[f292,f1007]) ).
fof(f14384,plain,
true = ifeq(true,true,ifeq(true,true,product(multiply(a,a),c,b),true),true),
inference(superposition,[],[f318,f1014]) ).
fof(f14460,plain,
true = ifeq(true,true,ifeq(true,true,product(multiply(h,h),d,b),true),true),
inference(superposition,[],[f5012,f1014]) ).
fof(f14505,plain,
true = ifeq(true,true,product(multiply(h,h),d,b),true),
inference(forward_demodulation,[],[f14460,f2]) ).
fof(f14555,plain,
true = ifeq(true,true,product(multiply(a,a),c,b),true),
inference(forward_demodulation,[],[f14384,f2]) ).
fof(f17150,plain,
! [X0] : true = ifeq(true,true,product(identity,multiply(X0,X0),inverse(X0)),true),
inference(superposition,[],[f1443,f1007]) ).
fof(f17417,plain,
! [X0,X1] : true = ifeq(true,true,product(multiply(X1,inverse(X0)),X0,X1),true),
inference(superposition,[],[f1442,f7]) ).
fof(f17420,plain,
! [X0,X1] : true = ifeq(true,true,product(multiply(X1,X0),inverse(X0),X1),true),
inference(superposition,[],[f1442,f9]) ).
fof(f17421,plain,
! [X0,X1] : true = ifeq(true,true,product(multiply(X1,X0),multiply(X0,X0),X1),true),
inference(superposition,[],[f1442,f1007]) ).
fof(f17590,plain,
! [X0,X1] : true = ifeq(true,true,product(X1,multiply(inverse(X1),X0),X0),true),
inference(superposition,[],[f1501,f3]) ).
fof(f17640,plain,
! [X0,X1] : true = ifeq(true,true,product(inverse(X1),multiply(X1,X0),X0),true),
inference(superposition,[],[f1531,f3]) ).
fof(f18280,plain,
! [X2,X0,X1] : true = ifeq(true,true,product(X0,multiply(X1,X2),multiply(multiply(X0,X1),X2)),true),
inference(superposition,[],[f1757,f11]) ).
fof(f18329,plain,
! [X2,X0,X1] : true = ifeq(true,true,product(multiply(X2,X0),X1,multiply(X2,multiply(X0,X1))),true),
inference(superposition,[],[f1838,f11]) ).
fof(f18700,plain,
true = ifeq(true,true,ifeq(true,true,product(b,inverse(c),inverse(a)),true),true),
inference(superposition,[],[f1406,f5843]) ).
fof(f18701,plain,
true = ifeq(true,true,ifeq(true,true,product(b,inverse(d),inverse(h)),true),true),
inference(superposition,[],[f1406,f7245]) ).
fof(f18728,plain,
true = ifeq(true,true,product(b,inverse(d),inverse(h)),true),
inference(forward_demodulation,[],[f18701,f2]) ).
fof(f18729,plain,
true = ifeq(true,true,product(b,inverse(c),inverse(a)),true),
inference(forward_demodulation,[],[f18700,f2]) ).
fof(f18840,plain,
true = ifeq(true,true,ifeq(true,true,product(inverse(c),a,inverse(b)),true),true),
inference(superposition,[],[f1505,f5646]) ).
fof(f18882,plain,
true = ifeq(true,true,product(inverse(c),a,inverse(b)),true),
inference(forward_demodulation,[],[f18840,f2]) ).
fof(f21240,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(true,true,product(X0,multiply(multiply(X0,X0),X1),X1),true),true),
inference(superposition,[],[f1760,f1007]) ).
fof(f21276,plain,
! [X0,X1] : true = ifeq(true,true,product(X0,multiply(multiply(X0,X0),X1),X1),true),
inference(forward_demodulation,[],[f21240,f2]) ).
fof(f25262,plain,
true = product(c,multiply(b,b),a),
inference(superposition,[],[f13887,f2]) ).
fof(f25374,plain,
true = ifeq(true,true,ifeq(true,true,product(inverse(c),a,multiply(b,b)),true),true),
inference(superposition,[],[f1505,f25262]) ).
fof(f25421,plain,
true = ifeq(true,true,product(inverse(c),a,multiply(b,b)),true),
inference(forward_demodulation,[],[f25374,f2]) ).
fof(f25596,plain,
true = product(multiply(h,h),d,b),
inference(superposition,[],[f14505,f2]) ).
fof(f25598,plain,
true = product(multiply(a,a),c,b),
inference(superposition,[],[f14555,f2]) ).
fof(f26087,plain,
true = ifeq(true,true,ifeq(true,true,product(b,inverse(d),multiply(h,h)),true),true),
inference(superposition,[],[f1406,f25596]) ).
fof(f26143,plain,
true = ifeq(true,true,product(b,inverse(d),multiply(h,h)),true),
inference(forward_demodulation,[],[f26087,f2]) ).
fof(f26441,plain,
true = ifeq(true,true,ifeq(true,true,product(b,inverse(c),multiply(a,a)),true),true),
inference(superposition,[],[f1406,f25598]) ).
fof(f26497,plain,
true = ifeq(true,true,product(b,inverse(c),multiply(a,a)),true),
inference(forward_demodulation,[],[f26441,f2]) ).
fof(f29196,plain,
true = product(d,c,multiply(c,b)),
inference(superposition,[],[f5857,f2]) ).
fof(f29307,plain,
multiply(d,c) = ifeq2(true,true,multiply(c,b),multiply(d,c)),
inference(superposition,[],[f1151,f29196]) ).
fof(f29368,plain,
multiply(c,b) = multiply(d,c),
inference(forward_demodulation,[],[f29307,f1]) ).
fof(f31536,plain,
! [X0] : true = product(a,multiply(b,X0),multiply(c,X0)),
inference(superposition,[],[f4402,f2]) ).
fof(f31550,plain,
! [X0] : true = product(X0,c,multiply(multiply(X0,a),b)),
inference(superposition,[],[f4419,f2]) ).
fof(f31660,plain,
! [X0] : multiply(a,multiply(b,X0)) = ifeq2(true,true,multiply(c,X0),multiply(a,multiply(b,X0))),
inference(superposition,[],[f1151,f31536]) ).
fof(f31721,plain,
! [X0] : multiply(c,X0) = multiply(a,multiply(b,X0)),
inference(forward_demodulation,[],[f31660,f1]) ).
fof(f31970,plain,
true = ifeq(true,true,product(inverse(inverse(c)),identity,multiply(multiply(identity,a),b)),true),
inference(superposition,[],[f1532,f31550]) ).
fof(f32069,plain,
! [X0] : multiply(multiply(X0,a),b) = ifeq2(true,true,multiply(X0,c),multiply(multiply(X0,a),b)),
inference(superposition,[],[f74,f31550]) ).
fof(f32275,plain,
! [X0] : multiply(X0,c) = multiply(multiply(X0,a),b),
inference(forward_demodulation,[],[f32069,f1]) ).
fof(f32359,plain,
true = ifeq(true,true,product(inverse(inverse(c)),identity,multiply(a,b)),true),
inference(forward_demodulation,[],[f31970,f994]) ).
fof(f32462,plain,
true = ifeq(true,true,product(inverse(inverse(c)),identity,c),true),
inference(forward_demodulation,[],[f32359,f209]) ).
fof(f40331,plain,
true = product(b,inverse(d),inverse(h)),
inference(superposition,[],[f18728,f2]) ).
fof(f40464,plain,
multiply(b,inverse(d)) = ifeq2(true,true,inverse(h),multiply(b,inverse(d))),
inference(superposition,[],[f1151,f40331]) ).
fof(f40525,plain,
inverse(h) = multiply(b,inverse(d)),
inference(forward_demodulation,[],[f40464,f1]) ).
fof(f41368,plain,
true = product(b,inverse(c),inverse(a)),
inference(superposition,[],[f18729,f2]) ).
fof(f41488,plain,
multiply(b,inverse(c)) = ifeq2(true,true,inverse(a),multiply(b,inverse(c))),
inference(superposition,[],[f1151,f41368]) ).
fof(f41549,plain,
inverse(a) = multiply(b,inverse(c)),
inference(forward_demodulation,[],[f41488,f1]) ).
fof(f43338,plain,
true = product(inverse(c),a,inverse(b)),
inference(superposition,[],[f18882,f2]) ).
fof(f43451,plain,
multiply(inverse(c),a) = ifeq2(true,true,inverse(b),multiply(inverse(c),a)),
inference(superposition,[],[f1151,f43338]) ).
fof(f43512,plain,
inverse(b) = multiply(inverse(c),a),
inference(forward_demodulation,[],[f43451,f1]) ).
fof(f45557,plain,
true = product(a,multiply(b,multiply(c,c)),identity),
inference(superposition,[],[f13912,f2]) ).
fof(f46714,plain,
multiply(a,multiply(b,multiply(c,c))) = ifeq2(true,true,ifeq2(true,true,identity,multiply(a,multiply(b,multiply(c,c)))),multiply(a,multiply(b,multiply(c,c)))),
inference(superposition,[],[f49,f45557]) ).
fof(f46904,plain,
multiply(c,multiply(c,c)) = ifeq2(true,true,ifeq2(true,true,identity,multiply(c,multiply(c,c))),multiply(c,multiply(c,c))),
inference(forward_demodulation,[],[f46714,f31721]) ).
fof(f46979,plain,
multiply(c,multiply(c,c)) = ifeq2(true,true,identity,multiply(c,multiply(c,c))),
inference(forward_demodulation,[],[f46904,f1]) ).
fof(f46993,plain,
identity = multiply(c,multiply(c,c)),
inference(forward_demodulation,[],[f46979,f1]) ).
fof(f47717,plain,
! [X0] : true = product(X0,h,multiply(multiply(X0,d),inverse(b))),
inference(superposition,[],[f4744,f2]) ).
fof(f48233,plain,
! [X0] : true = product(X0,d,multiply(multiply(X0,c),inverse(a))),
inference(superposition,[],[f4755,f2]) ).
fof(f49080,plain,
! [X0] : true = product(X0,k,multiply(multiply(X0,d),inverse(h))),
inference(superposition,[],[f4901,f2]) ).
fof(f49382,plain,
! [X0] : multiply(multiply(X0,d),inverse(b)) = ifeq2(true,true,multiply(X0,h),multiply(multiply(X0,d),inverse(b))),
inference(superposition,[],[f74,f47717]) ).
fof(f49588,plain,
! [X0] : multiply(X0,h) = multiply(multiply(X0,d),inverse(b)),
inference(forward_demodulation,[],[f49382,f1]) ).
fof(f52052,plain,
! [X0] : multiply(multiply(X0,c),inverse(a)) = ifeq2(true,true,multiply(X0,d),multiply(multiply(X0,c),inverse(a))),
inference(superposition,[],[f74,f48233]) ).
fof(f52258,plain,
! [X0] : multiply(X0,d) = multiply(multiply(X0,c),inverse(a)),
inference(forward_demodulation,[],[f52052,f1]) ).
fof(f54977,plain,
! [X0] : multiply(multiply(X0,d),inverse(h)) = ifeq2(true,true,multiply(X0,k),multiply(multiply(X0,d),inverse(h))),
inference(superposition,[],[f74,f49080]) ).
fof(f55183,plain,
! [X0] : multiply(X0,k) = multiply(multiply(X0,d),inverse(h)),
inference(forward_demodulation,[],[f54977,f1]) ).
fof(f69290,plain,
true = product(inverse(inverse(c)),identity,c),
inference(superposition,[],[f32462,f2]) ).
fof(f69319,plain,
inverse(inverse(c)) = ifeq2(true,true,c,inverse(inverse(c))),
inference(superposition,[],[f1056,f69290]) ).
fof(f69611,plain,
c = inverse(inverse(c)),
inference(forward_demodulation,[],[f69319,f1]) ).
fof(f75706,plain,
! [X0] : true = product(identity,multiply(X0,X0),inverse(X0)),
inference(superposition,[],[f17150,f2]) ).
fof(f75824,plain,
! [X0,X1] : true = product(multiply(X0,inverse(X1)),X1,X0),
inference(superposition,[],[f17417,f2]) ).
fof(f76086,plain,
! [X0,X1] : true = product(X0,multiply(inverse(X0),X1),X1),
inference(superposition,[],[f17590,f2]) ).
fof(f76239,plain,
! [X0,X1] : true = product(inverse(X0),multiply(X0,X1),X1),
inference(superposition,[],[f17640,f2]) ).
fof(f77126,plain,
! [X0,X1] : true = product(multiply(X0,X1),multiply(X1,X1),X0),
inference(superposition,[],[f17421,f2]) ).
fof(f77224,plain,
! [X0,X1] : true = product(X0,multiply(multiply(X0,X0),X1),X1),
inference(superposition,[],[f21276,f2]) ).
fof(f93751,plain,
! [X2,X0,X1] : true = product(X0,multiply(X1,X2),multiply(multiply(X0,X1),X2)),
inference(superposition,[],[f18280,f2]) ).
fof(f94268,plain,
! [X2,X0,X1] : true = product(multiply(X0,X1),X2,multiply(X0,multiply(X1,X2))),
inference(superposition,[],[f18329,f2]) ).
fof(f121490,plain,
true = product(inverse(c),a,multiply(b,b)),
inference(superposition,[],[f25421,f2]) ).
fof(f121608,plain,
multiply(inverse(c),a) = ifeq2(true,true,multiply(b,b),multiply(inverse(c),a)),
inference(superposition,[],[f1151,f121490]) ).
fof(f121721,plain,
multiply(inverse(c),a) = multiply(b,b),
inference(forward_demodulation,[],[f121608,f1]) ).
fof(f121822,plain,
inverse(b) = multiply(b,b),
inference(forward_demodulation,[],[f121721,f43512]) ).
fof(f121921,plain,
multiply(c,b) = multiply(a,inverse(b)),
inference(superposition,[],[f31721,f121822]) ).
fof(f125929,plain,
true = product(b,inverse(d),multiply(h,h)),
inference(superposition,[],[f26143,f2]) ).
fof(f126054,plain,
multiply(b,inverse(d)) = ifeq2(true,true,multiply(h,h),multiply(b,inverse(d))),
inference(superposition,[],[f1151,f125929]) ).
fof(f126172,plain,
multiply(b,inverse(d)) = multiply(h,h),
inference(forward_demodulation,[],[f126054,f1]) ).
fof(f126284,plain,
inverse(h) = multiply(h,h),
inference(forward_demodulation,[],[f126172,f40525]) ).
fof(f126550,plain,
true = ifeq(true,true,product(inverse(h),inverse(h),h),true),
inference(superposition,[],[f17420,f126284]) ).
fof(f129094,plain,
true = product(inverse(h),inverse(h),h),
inference(superposition,[],[f126550,f2]) ).
fof(f129232,plain,
multiply(inverse(h),inverse(h)) = ifeq2(true,true,h,multiply(inverse(h),inverse(h))),
inference(superposition,[],[f1151,f129094]) ).
fof(f129346,plain,
h = multiply(inverse(h),inverse(h)),
inference(forward_demodulation,[],[f129232,f1]) ).
fof(f131907,plain,
true = product(b,inverse(c),multiply(a,a)),
inference(superposition,[],[f26497,f2]) ).
fof(f132040,plain,
multiply(b,inverse(c)) = ifeq2(true,true,multiply(a,a),multiply(b,inverse(c))),
inference(superposition,[],[f1151,f131907]) ).
fof(f132158,plain,
multiply(b,inverse(c)) = multiply(a,a),
inference(forward_demodulation,[],[f132040,f1]) ).
fof(f132270,plain,
inverse(a) = multiply(a,a),
inference(forward_demodulation,[],[f132158,f41549]) ).
fof(f132512,plain,
true = ifeq(true,true,product(inverse(a),inverse(a),a),true),
inference(superposition,[],[f17420,f132270]) ).
fof(f133949,plain,
true = product(inverse(a),inverse(a),a),
inference(superposition,[],[f132512,f2]) ).
fof(f134081,plain,
multiply(inverse(a),inverse(a)) = ifeq2(true,true,a,multiply(inverse(a),inverse(a))),
inference(superposition,[],[f1151,f133949]) ).
fof(f134195,plain,
a = multiply(inverse(a),inverse(a)),
inference(forward_demodulation,[],[f134081,f1]) ).
fof(f145879,plain,
true = product(identity,multiply(inverse(c),inverse(c)),c),
inference(superposition,[],[f75706,f69611]) ).
fof(f151576,plain,
multiply(inverse(c),inverse(c)) = ifeq2(true,true,c,multiply(inverse(c),inverse(c))),
inference(superposition,[],[f1043,f145879]) ).
fof(f151920,plain,
c = multiply(inverse(c),inverse(c)),
inference(forward_demodulation,[],[f151576,f1]) ).
fof(f152289,plain,
true = product(c,c,inverse(c)),
inference(superposition,[],[f75824,f151920]) ).
fof(f155788,plain,
multiply(c,c) = ifeq2(true,true,inverse(c),multiply(c,c)),
inference(superposition,[],[f1151,f152289]) ).
fof(f155899,plain,
inverse(c) = multiply(c,c),
inference(forward_demodulation,[],[f155788,f1]) ).
fof(f156057,plain,
true = product(a,multiply(b,c),inverse(c)),
inference(superposition,[],[f31536,f155899]) ).
fof(f156918,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = ifeq2(true,true,X1,multiply(X0,multiply(inverse(X0),X1))),
inference(superposition,[],[f1151,f76086]) ).
fof(f157374,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(forward_demodulation,[],[f156918,f1]) ).
fof(f158166,plain,
! [X0] : true = product(inverse(multiply(X0,a)),multiply(X0,c),b),
inference(superposition,[],[f76239,f32275]) ).
fof(f162489,plain,
true = product(b,multiply(d,d),inverse(h)),
inference(superposition,[],[f77126,f7408]) ).
fof(f167923,plain,
! [X0,X1] : ifeq2(true,true,multiply(X0,multiply(multiply(X0,X0),X1)),X1) = X1,
inference(superposition,[],[f74,f77224]) ).
fof(f169226,plain,
multiply(b,multiply(d,d)) = ifeq2(true,true,inverse(h),multiply(b,multiply(d,d))),
inference(superposition,[],[f1151,f162489]) ).
fof(f169341,plain,
inverse(h) = multiply(b,multiply(d,d)),
inference(forward_demodulation,[],[f169226,f1]) ).
fof(f185974,plain,
! [X0] : true = product(d,multiply(a,X0),multiply(c,X0)),
inference(superposition,[],[f93751,f4121]) ).
fof(f186415,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = ifeq2(true,true,multiply(X0,multiply(X1,X2)),multiply(multiply(X0,X1),X2)),
inference(superposition,[],[f74,f93751]) ).
fof(f186686,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(forward_demodulation,[],[f186415,f1]) ).
fof(f187745,plain,
true = product(multiply(b,d),d,inverse(h)),
inference(superposition,[],[f94268,f169341]) ).
fof(f202302,plain,
multiply(multiply(b,d),d) = ifeq2(true,true,inverse(h),multiply(multiply(b,d),d)),
inference(superposition,[],[f1151,f187745]) ).
fof(f202423,plain,
inverse(h) = multiply(multiply(b,d),d),
inference(forward_demodulation,[],[f202302,f1]) ).
fof(f203089,plain,
multiply(inverse(h),inverse(h)) = multiply(multiply(b,d),k),
inference(superposition,[],[f55183,f202423]) ).
fof(f203223,plain,
h = multiply(multiply(b,d),k),
inference(forward_demodulation,[],[f203089,f129346]) ).
fof(f203237,plain,
true = product(b,multiply(d,k),h),
inference(superposition,[],[f93751,f203223]) ).
fof(f206390,plain,
multiply(b,multiply(d,k)) = ifeq2(true,true,h,multiply(b,multiply(d,k))),
inference(superposition,[],[f1151,f203237]) ).
fof(f206508,plain,
h = multiply(b,multiply(d,k)),
inference(forward_demodulation,[],[f206390,f1]) ).
fof(f206649,plain,
multiply(a,h) = multiply(c,multiply(d,k)),
inference(superposition,[],[f31721,f206508]) ).
fof(f224456,plain,
multiply(a,multiply(b,c)) = ifeq2(true,true,inverse(c),multiply(a,multiply(b,c))),
inference(superposition,[],[f1151,f156057]) ).
fof(f224586,plain,
inverse(c) = multiply(a,multiply(b,c)),
inference(forward_demodulation,[],[f224456,f1]) ).
fof(f224820,plain,
true = product(inverse(a),inverse(c),multiply(b,c)),
inference(superposition,[],[f76239,f224586]) ).
fof(f226203,plain,
true = product(multiply(c,d),k,multiply(a,h)),
inference(superposition,[],[f94268,f206649]) ).
fof(f234786,plain,
! [X0] : multiply(d,multiply(a,X0)) = ifeq2(true,true,multiply(c,X0),multiply(d,multiply(a,X0))),
inference(superposition,[],[f1151,f185974]) ).
fof(f234907,plain,
! [X0] : multiply(c,X0) = multiply(d,multiply(a,X0)),
inference(forward_demodulation,[],[f234786,f1]) ).
fof(f235092,plain,
! [X0] : multiply(d,multiply(c,X0)) = multiply(c,multiply(b,X0)),
inference(superposition,[],[f234907,f31721]) ).
fof(f303085,plain,
multiply(inverse(a),inverse(c)) = ifeq2(true,true,multiply(b,c),multiply(inverse(a),inverse(c))),
inference(superposition,[],[f1151,f224820]) ).
fof(f303217,plain,
multiply(b,c) = multiply(inverse(a),inverse(c)),
inference(forward_demodulation,[],[f303085,f1]) ).
fof(f303407,plain,
true = product(multiply(b,c),c,inverse(a)),
inference(superposition,[],[f75824,f303217]) ).
fof(f303715,plain,
multiply(multiply(b,c),c) = ifeq2(true,true,inverse(a),multiply(multiply(b,c),c)),
inference(superposition,[],[f1151,f303407]) ).
fof(f303853,plain,
inverse(a) = multiply(multiply(b,c),c),
inference(forward_demodulation,[],[f303715,f1]) ).
fof(f304095,plain,
multiply(inverse(a),inverse(a)) = multiply(multiply(b,c),d),
inference(superposition,[],[f52258,f303853]) ).
fof(f304259,plain,
a = multiply(multiply(b,c),d),
inference(forward_demodulation,[],[f304095,f134195]) ).
fof(f304333,plain,
multiply(a,inverse(b)) = multiply(multiply(b,c),h),
inference(superposition,[],[f49588,f304259]) ).
fof(f304502,plain,
multiply(c,b) = multiply(multiply(b,c),h),
inference(forward_demodulation,[],[f304333,f121921]) ).
fof(f306994,plain,
true = product(b,multiply(c,h),multiply(c,b)),
inference(superposition,[],[f93751,f304502]) ).
fof(f311138,plain,
multiply(multiply(c,d),k) = ifeq2(true,true,multiply(a,h),multiply(multiply(c,d),k)),
inference(superposition,[],[f1151,f226203]) ).
fof(f311270,plain,
multiply(a,h) = multiply(multiply(c,d),k),
inference(forward_demodulation,[],[f311138,f1]) ).
fof(f321620,plain,
multiply(b,multiply(c,h)) = ifeq2(true,true,multiply(c,b),multiply(b,multiply(c,h))),
inference(superposition,[],[f1151,f306994]) ).
fof(f321741,plain,
multiply(c,b) = multiply(b,multiply(c,h)),
inference(forward_demodulation,[],[f321620,f1]) ).
fof(f355437,plain,
! [X0] : multiply(inverse(multiply(X0,a)),multiply(X0,c)) = ifeq2(true,true,b,multiply(inverse(multiply(X0,a)),multiply(X0,c))),
inference(superposition,[],[f1151,f158166]) ).
fof(f355559,plain,
! [X0] : b = multiply(inverse(multiply(X0,a)),multiply(X0,c)),
inference(forward_demodulation,[],[f355437,f1]) ).
fof(f355824,plain,
b = multiply(inverse(multiply(d,a)),multiply(c,b)),
inference(superposition,[],[f355559,f29368]) ).
fof(f355999,plain,
b = multiply(inverse(c),multiply(c,b)),
inference(forward_demodulation,[],[f355824,f4121]) ).
fof(f1681605,plain,
! [X0] : multiply(identity,X0) = multiply(c,multiply(multiply(c,c),X0)),
inference(superposition,[],[f186686,f46993]) ).
fof(f1688986,plain,
! [X0] : multiply(identity,X0) = multiply(c,multiply(c,multiply(c,X0))),
inference(forward_demodulation,[],[f1681605,f186686]) ).
fof(f1690768,plain,
! [X0] : multiply(c,multiply(c,multiply(c,X0))) = X0,
inference(forward_demodulation,[],[f1688986,f994]) ).
fof(f1692195,plain,
! [X0] : multiply(inverse(c),X0) = multiply(c,multiply(c,X0)),
inference(superposition,[],[f1690768,f157374]) ).
fof(f1701515,plain,
! [X0,X1] : ifeq2(true,true,multiply(X0,multiply(X0,multiply(X0,X1))),X1) = X1,
inference(forward_demodulation,[],[f167923,f186686]) ).
fof(f1707336,plain,
k = ifeq2(true,true,multiply(multiply(c,d),multiply(multiply(c,d),multiply(a,h))),k),
inference(superposition,[],[f1701515,f311270]) ).
fof(f1707473,plain,
k = ifeq2(true,true,multiply(c,multiply(d,multiply(multiply(c,d),multiply(a,h)))),k),
inference(forward_demodulation,[],[f1707336,f186686]) ).
fof(f1708716,plain,
k = ifeq2(true,true,multiply(c,multiply(d,multiply(c,multiply(d,multiply(a,h))))),k),
inference(forward_demodulation,[],[f1707473,f186686]) ).
fof(f1709791,plain,
k = ifeq2(true,true,multiply(c,multiply(c,multiply(b,multiply(d,multiply(a,h))))),k),
inference(forward_demodulation,[],[f1708716,f235092]) ).
fof(f1710396,plain,
k = ifeq2(true,true,multiply(inverse(c),multiply(b,multiply(d,multiply(a,h)))),k),
inference(forward_demodulation,[],[f1709791,f1692195]) ).
fof(f1710772,plain,
k = ifeq2(true,true,multiply(inverse(c),multiply(b,multiply(c,h))),k),
inference(forward_demodulation,[],[f1710396,f234907]) ).
fof(f1711005,plain,
k = ifeq2(true,true,multiply(inverse(c),multiply(c,b)),k),
inference(forward_demodulation,[],[f1710772,f321741]) ).
fof(f1711148,plain,
k = ifeq2(true,true,b,k),
inference(forward_demodulation,[],[f1711005,f355999]) ).
fof(f1711232,plain,
b = k,
inference(forward_demodulation,[],[f1711148,f1]) ).
fof(f1711321,plain,
true != product(b,inverse(b),identity),
inference(superposition,[],[f32,f1711232]) ).
fof(f1713386,plain,
$false,
inference(forward_subsumption_resolution,[],[f1711321,f9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP002-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Sun Sep 27 09:12:20 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.32 Running first-order model finding
% 0.03/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.18/1.49 % (2098394)Will run a generic schedule for satisfiability detection.
% 7.18/1.49 % (2098400)% WARNING: option uhcvi not known.
% 7.18/1.49 % (2098404)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1888376810:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.18/1.49 % (2098400)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=215036177:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.18/1.49 % (2098402)dis+10_1_sil=32000:sp=arity:random_seed=3901264205:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.18/1.49 % (2098399)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3933291307_2999 on theBenchmark for (2999ds/0Mi)
% 7.18/1.49 % (2098401)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3857845062:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.18/1.49 % (2098403)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=215625454:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.18/1.49 % (2098405)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2220456739:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.18/1.49 % TRYING [1]
% 7.18/1.49 % TRYING [2]
% 7.18/1.49 % TRYING [3]
% 7.18/1.49 % TRYING [4]
% 7.18/1.49 % (2098402)Instruction limit reached!
% 7.18/1.49 % (2098402)------------------------------
% 7.18/1.49 % (2098402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.18/1.49 % (2098402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.18/1.49 % (2098402)CaDiCaL version: 2.1.3
% 7.18/1.49 % (2098402)Termination reason: Instruction limit
% 7.18/1.49 % (2098402)Termination phase: Saturation
% 7.18/1.49 % (2098402)Time elapsed: 0.032 s
% 7.18/1.49 % (2098402)Peak memory usage: 12 MB
% 7.18/1.49 % (2098402)Instructions burned: 105 (million)
% 7.18/1.49 % (2098403)Instruction limit reached!
% 7.18/1.49 % (2098403)------------------------------
% 7.18/1.49 % (2098403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.18/1.49 % (2098403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.18/1.49 % (2098403)CaDiCaL version: 2.1.3
% 7.18/1.49 % (2098403)Termination reason: Instruction limit
% 7.18/1.49 % (2098403)Termination phase: Saturation
% 7.18/1.49 % (2098403)Time elapsed: 0.038 s
% 7.18/1.49 % (2098403)Peak memory usage: 13 MB
% 7.18/1.49 % (2098403)Instructions burned: 118 (million)
% 7.18/1.49 % (2098404)Instruction limit reached!
% 7.18/1.49 % (2098404)------------------------------
% 7.18/1.49 % (2098404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.18/1.49 % (2098404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.18/1.49 % (2098404)CaDiCaL version: 2.1.3
% 7.18/1.49 % (2098404)Termination reason: Instruction limit
% 7.18/1.49 % (2098404)Termination phase: Saturation
% 7.18/1.49 % (2098404)Time elapsed: 0.040 s
% 7.18/1.49 % (2098404)Peak memory usage: 13 MB
% 7.18/1.49 % (2098404)Instructions burned: 132 (million)
% 7.18/1.49 % (2098413)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1952972833:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.18/1.49 % TRYING [1]
% 7.18/1.49 % TRYING [2]
% 7.18/1.49 % (2098414)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=40263147:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.18/1.49 % TRYING [3]
% 7.18/1.49 % (2098415)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1971854630:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 7.18/1.49 % (2098405)Instruction limit reached!
% 7.18/1.49 % (2098405)------------------------------
% 7.18/1.49 % (2098405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.18/1.49 % (2098405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.18/1.49 % (2098405)CaDiCaL version: 2.1.3
% 7.18/1.49 % (2098405)Termination reason: Instruction limit
% 7.18/1.49 % (2098405)Termination phase: Saturation
% 7.18/1.49 % (2098405)Time elapsed: 0.053 s
% 7.18/1.49 % (2098405)Peak memory usage: 12 MB
% 7.18/1.49 % (2098405)Instructions burned: 160 (million)
% 7.18/1.49 % (2098419)ott-21_1_sil=16000:fs=off:random_seed=819417240:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 7.18/1.49 % TRYING [4]
% 7.18/1.49 % (2098414)Instruction limit reached!
% 7.18/1.49 % (2098414)------------------------------
% 7.18/1.49 % (2098414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.18/1.49 % (2098414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.40/3.82 % (2098414)CaDiCaL version: 2.1.3
% 24.40/3.82 % (2098414)Termination reason: Instruction limit
% 24.40/3.82 % (2098414)Termination phase: Saturation
% 24.40/3.82 % (2098414)Time elapsed: 0.043 s
% 24.40/3.82 % (2098414)Peak memory usage: 13 MB
% 24.40/3.82 % (2098414)Instructions burned: 131 (million)
% 24.40/3.82 % (2098421)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1564016586:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 24.40/3.82 % (2098419)Instruction limit reached!
% 24.40/3.82 % (2098419)------------------------------
% 24.40/3.82 % (2098419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.40/3.82 % (2098419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.40/3.82 % (2098419)CaDiCaL version: 2.1.3
% 24.40/3.82 % (2098419)Termination reason: Instruction limit
% 24.40/3.82 % (2098419)Termination phase: Saturation
% 24.40/3.82 % (2098419)Time elapsed: 0.052 s
% 24.40/3.82 % (2098419)Peak memory usage: 13 MB
% 24.40/3.82 % (2098419)Instructions burned: 183 (million)
% 24.40/3.82 % (2098423)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1603960407:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 24.40/3.83 % TRYING [1]
% 24.40/3.83 % TRYING [2]
% 24.40/3.83 % TRYING [3]
% 24.40/3.83 % TRYING [5]
% 24.40/3.83 % (2098413)Instruction limit reached!
% 24.40/3.83 % (2098413)------------------------------
% 24.40/3.83 % (2098413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.40/3.83 % (2098413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.40/3.83 % (2098413)CaDiCaL version: 2.1.3
% 24.40/3.83 % (2098413)Termination reason: Instruction limit
% 24.40/3.83 % (2098413)Termination phase: Finite model building constraint generation
% 24.40/3.83 % (2098413)Time elapsed: 0.139 s
% 24.40/3.83 % (2098413)Peak memory usage: 39 MB
% 24.40/3.83 % (2098413)Instructions burned: 717 (million)
% 24.40/3.83 % (2098425)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1326431018:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 24.40/3.83 % TRYING [4]
% 24.40/3.83 % (2098421)Instruction limit reached!
% 24.40/3.83 % (2098421)------------------------------
% 24.40/3.83 % (2098421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.40/3.83 % (2098421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.40/3.83 % (2098421)CaDiCaL version: 2.1.3
% 24.40/3.83 % (2098421)Termination reason: Instruction limit
% 24.40/3.83 % (2098421)Termination phase: Saturation
% 24.40/3.83 % (2098421)Time elapsed: 0.145 s
% 24.40/3.83 % (2098421)Peak memory usage: 16 MB
% 24.40/3.83 % (2098421)Instructions burned: 479 (million)
% 24.40/3.83 % (2098427)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=337231474:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 24.40/3.83 % (2098415)Instruction limit reached!
% 24.40/3.83 % (2098415)------------------------------
% 24.40/3.83 % (2098415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.40/3.83 % (2098415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.40/3.83 % (2098415)CaDiCaL version: 2.1.3
% 24.40/3.83 % (2098415)Termination reason: Instruction limit
% 24.40/3.83 % (2098415)Termination phase: Saturation
% 24.40/3.83 % (2098415)Time elapsed: 0.213 s
% 24.40/3.83 % (2098415)Peak memory usage: 18 MB
% 24.40/3.83 % (2098415)Instructions burned: 685 (million)
% 24.40/3.83 % (2098429)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1920973809:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 24.40/3.83 % (2098423)Instruction limit reached!
% 24.40/3.83 % (2098423)------------------------------
% 24.40/3.83 % (2098423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.40/3.83 % (2098423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.40/3.83 % (2098423)CaDiCaL version: 2.1.3
% 24.40/3.83 % (2098423)Termination reason: Instruction limit
% 24.40/3.83 % (2098423)Termination phase: Finite model building constraint generation
% 24.40/3.83 % (2098423)Time elapsed: 0.190 s
% 24.40/3.83 % (2098423)Peak memory usage: 38 MB
% 24.40/3.83 % (2098423)Instructions burned: 866 (million)
% 24.40/3.83 % (2098431)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1152422898:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 24.40/3.83 % (2098429)Instruction limit reached!
% 24.40/3.83 % (2098429)------------------------------
% 54.14/8.04 % (2098429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.14/8.04 % (2098429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.14/8.04 % (2098429)CaDiCaL version: 2.1.3
% 54.14/8.04 % (2098429)Termination reason: Instruction limit
% 54.14/8.04 % (2098429)Termination phase: Saturation
% 54.14/8.04 % (2098429)Time elapsed: 0.227 s
% 54.14/8.04 % (2098429)Peak memory usage: 20 MB
% 54.14/8.04 % (2098429)Instructions burned: 692 (million)
% 54.14/8.04 % (2098427)Instruction limit reached!
% 54.14/8.04 % (2098427)------------------------------
% 54.14/8.04 % (2098427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.14/8.04 % (2098427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.14/8.04 % (2098427)CaDiCaL version: 2.1.3
% 54.14/8.04 % (2098427)Termination reason: Instruction limit
% 54.14/8.04 % (2098427)Termination phase: Finite model building constraint generation
% 54.14/8.04 % (2098427)Time elapsed: 0.246 s
% 54.14/8.04 % (2098427)Peak memory usage: 112 MB
% 54.14/8.04 % (2098427)Instructions burned: 891 (million)
% 54.14/8.04 % (2098433)fmb+10_1_sil=64000:random_seed=3124621337:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 54.14/8.04 % TRYING [1]
% 54.14/8.04 % TRYING [2]
% 54.14/8.04 % TRYING [3]
% 54.14/8.04 % (2098435)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2709052893:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 54.14/8.04 % TRYING [20]
% 54.14/8.04 % (2098425)Instruction limit reached!
% 54.14/8.04 % (2098425)------------------------------
% 54.14/8.04 % (2098425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.14/8.04 % (2098425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.14/8.04 % (2098425)CaDiCaL version: 2.1.3
% 54.14/8.04 % (2098425)Termination reason: Instruction limit
% 54.14/8.04 % (2098425)Termination phase: Saturation
% 54.14/8.04 % (2098425)Time elapsed: 0.344 s
% 54.14/8.04 % (2098425)Peak memory usage: 25 MB
% 54.14/8.04 % (2098425)Instructions burned: 1180 (million)
% 54.14/8.04 % (2098437)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=251748755:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 54.14/8.04 % TRYING [8]
% 54.14/8.04 % (2098431)Instruction limit reached!
% 54.14/8.04 % (2098431)------------------------------
% 54.14/8.04 % (2098431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.14/8.04 % (2098431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.14/8.04 % (2098431)CaDiCaL version: 2.1.3
% 54.14/8.04 % (2098431)Termination reason: Instruction limit
% 54.14/8.04 % (2098431)Termination phase: Saturation
% 54.14/8.04 % (2098431)Time elapsed: 0.248 s
% 54.14/8.04 % (2098431)Peak memory usage: 20 MB
% 54.14/8.04 % (2098431)Instructions burned: 881 (million)
% 54.14/8.04 % (2098439)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2844080695:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 54.14/8.04 % TRYING [4]
% 54.14/8.04 % (2098437)Instruction limit reached!
% 54.14/8.04 % (2098437)------------------------------
% 54.14/8.04 % (2098437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.14/8.04 % (2098437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.14/8.04 % (2098437)CaDiCaL version: 2.1.3
% 54.14/8.04 % (2098437)Termination reason: Instruction limit
% 54.14/8.04 % (2098437)Termination phase: Finite model building constraint generation
% 54.14/8.04 % (2098437)Time elapsed: 0.181 s
% 54.14/8.04 % (2098437)Peak memory usage: 75 MB
% 54.14/8.04 % (2098437)Instructions burned: 922 (million)
% 54.14/8.04 % (2098441)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3734325142:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 54.14/8.04 % (2098441)Instruction limit reached!
% 54.14/8.04 % (2098441)------------------------------
% 54.14/8.04 % (2098441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.14/8.04 % (2098441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.14/8.04 % (2098441)CaDiCaL version: 2.1.3
% 54.14/8.04 % (2098441)Termination reason: Instruction limit
% 54.14/8.04 % (2098441)Termination phase: Saturation
% 54.14/8.04 % (2098441)Time elapsed: 0.365 s
% 54.14/8.04 % (2098441)Peak memory usage: 24 MB
% 54.14/8.04 % (2098441)Instructions burned: 1474 (million)
% 54.14/8.04 % (2098443)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=420718578:i=6324_2988 on theBenchmark for (2988ds/6324Mi)
% 54.14/8.04 % (2098443)Cannot represent all propositional literals internally
% 54.14/8.04 % (2098443)Refutation not found, incomplete strategy
% 119.91/17.82 % (2098443)------------------------------
% 119.91/17.82 % (2098443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.91/17.82 % (2098443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.91/17.82 % (2098443)CaDiCaL version: 2.1.3
% 119.91/17.82 % (2098443)Termination reason: Refutation not found, incomplete strategy
% 119.91/17.82 % (2098443)Time elapsed: 0.002 s
% 119.91/17.82 % (2098443)Peak memory usage: 10 MB
% 119.91/17.82 % (2098443)Instructions burned: 5 (million)
% 119.91/17.82 % (2098443)------------------------------
% 119.91/17.82 % (2098443)------------------------------
% 119.91/17.82 % (2098445)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1510685234:fmbsr=2.30978:i=2174_2988 on theBenchmark for (2988ds/2174Mi)
% 119.91/17.82 % TRYING [16]
% 119.91/17.82 % TRYING [6]
% 119.91/17.82 % TRYING [5]
% 119.91/17.82 % (2098445)Instruction limit reached!
% 119.91/17.82 % (2098445)------------------------------
% 119.91/17.82 % (2098445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.91/17.82 % (2098445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.91/17.82 % (2098445)CaDiCaL version: 2.1.3
% 119.91/17.82 % (2098445)Termination reason: Instruction limit
% 119.91/17.82 % (2098445)Termination phase: Finite model building constraint generation
% 119.91/17.82 % (2098445)Time elapsed: 0.417 s
% 119.91/17.82 % (2098445)Peak memory usage: 139 MB
% 119.91/17.82 % (2098445)Instructions burned: 2176 (million)
% 119.91/17.82 % (2098447)ott-2_1_sil=16000:newcnf=on:random_seed=207197633:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2983 on theBenchmark for (2983ds/869Mi)
% 119.91/17.82 % (2098447)Instruction limit reached!
% 119.91/17.82 % (2098447)------------------------------
% 119.91/17.82 % (2098447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.91/17.82 % (2098447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.91/17.82 % (2098447)CaDiCaL version: 2.1.3
% 119.91/17.82 % (2098447)Termination reason: Instruction limit
% 119.91/17.82 % (2098447)Termination phase: Saturation
% 119.91/17.82 % (2098447)Time elapsed: 0.262 s
% 119.91/17.82 % (2098447)Peak memory usage: 23 MB
% 119.91/17.82 % (2098447)Instructions burned: 869 (million)
% 119.91/17.82 % (2098449)ott+10_1_sil=32000:tgt=ground:random_seed=777434337:i=5114:av=off_2981 on theBenchmark for (2981ds/5114Mi)
% 119.91/17.82 % (2098439)Instruction limit reached!
% 119.91/17.82 % (2098439)------------------------------
% 119.91/17.82 % (2098439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.91/17.82 % (2098439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.91/17.82 % (2098439)CaDiCaL version: 2.1.3
% 119.91/17.82 % (2098439)Termination reason: Instruction limit
% 119.91/17.82 % (2098439)Termination phase: Saturation
% 119.91/17.82 % (2098439)Time elapsed: 1.506 s
% 119.91/17.82 % (2098439)Peak memory usage: 59 MB
% 119.91/17.82 % (2098439)Instructions burned: 5134 (million)
% 119.91/17.82 % (2098451)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4083991975:i=54282_2978 on theBenchmark for (2978ds/54282Mi)
% 119.91/17.82 % TRYING [1]
% 119.91/17.82 % TRYING [2]
% 119.91/17.82 % TRYING [3]
% 119.91/17.82 % TRYING [4]
% 119.91/17.82 % TRYING [5]
% 119.91/17.82 % (2098435)Instruction limit reached!
% 119.91/17.82 % (2098435)------------------------------
% 119.91/17.82 % (2098435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.91/17.82 % (2098435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.91/17.82 % (2098435)CaDiCaL version: 2.1.3
% 119.91/17.82 % (2098435)Termination reason: Instruction limit
% 119.91/17.82 % (2098435)Termination phase: Finite model building constraint generation
% 119.91/17.82 % (2098435)Time elapsed: 1.852 s
% 119.91/17.82 % (2098435)Peak memory usage: 580 MB
% 119.91/17.82 % (2098435)Instructions burned: 9519 (million)
% 119.91/17.82 % (2098453)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3708903882:i=3512:aac=none_2975 on theBenchmark for (2975ds/3512Mi)
% 119.91/17.82 % TRYING [6]
% 119.91/17.82 % (2098453)Instruction limit reached!
% 119.91/17.82 % (2098453)------------------------------
% 119.91/17.82 % (2098453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.91/17.82 % (2098453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.91/17.82 % (2098453)CaDiCaL version: 2.1.3
% 119.91/17.82 % (2098453)Termination reason: Instruction limit
% 119.91/17.82 % (2098453)Termination phase: Saturation
% 119.91/17.82 % (2098453)Time elapsed: 1.040 s
% 119.91/17.82 % (2098453)Peak memory usage: 48 MB
% 119.91/17.82 % (2098453)Instructions burned: 3512 (million)
% 119.91/17.82 % (2098449)Instruction limit reached!
% 119.91/17.82 % (2098449)------------------------------
% 172.46/24.85 % (2098449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.46/24.85 % (2098449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.46/24.85 % (2098449)CaDiCaL version: 2.1.3
% 172.46/24.85 % (2098449)Termination reason: Instruction limit
% 172.46/24.85 % (2098449)Termination phase: Saturation
% 172.46/24.85 % (2098449)Time elapsed: 1.606 s
% 172.46/24.85 % (2098449)Peak memory usage: 80 MB
% 172.46/24.85 % (2098449)Instructions burned: 5115 (million)
% 172.46/24.85 % (2098455)dis+21_1_sil=32000:sas=cadical:random_seed=2074223543:i=3773:amm=off_2964 on theBenchmark for (2964ds/3773Mi)
% 172.46/24.85 % (2098456)ott+11_1_sil=16000:gs=on:random_seed=3492636749:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2964 on theBenchmark for (2964ds/2251Mi)
% 172.46/24.85 % (2098456)Instruction limit reached!
% 172.46/24.85 % (2098456)------------------------------
% 172.46/24.85 % (2098456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.46/24.85 % (2098456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.46/24.85 % (2098456)CaDiCaL version: 2.1.3
% 172.46/24.85 % (2098456)Termination reason: Instruction limit
% 172.46/24.85 % (2098456)Termination phase: Saturation
% 172.46/24.85 % (2098456)Time elapsed: 0.588 s
% 172.46/24.85 % (2098456)Peak memory usage: 30 MB
% 172.46/24.85 % (2098456)Instructions burned: 2252 (million)
% 172.46/24.85 % (2098459)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2559601898:fmbsr=1.6:i=67534_2958 on theBenchmark for (2958ds/67534Mi)
% 172.46/24.85 % TRYING [7]
% 172.46/24.85 % (2098455)Instruction limit reached!
% 172.46/24.85 % (2098455)------------------------------
% 172.46/24.85 % (2098455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.46/24.85 % (2098455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.46/24.85 % (2098455)CaDiCaL version: 2.1.3
% 172.46/24.85 % (2098455)Termination reason: Instruction limit
% 172.46/24.85 % (2098455)Termination phase: Saturation
% 172.46/24.85 % (2098455)Time elapsed: 1.126 s
% 172.46/24.85 % (2098455)Peak memory usage: 51 MB
% 172.46/24.85 % (2098455)Instructions burned: 3776 (million)
% 172.46/24.85 % (2098461)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3271498295:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2953 on theBenchmark for (2953ds/4591Mi)
% 172.46/24.85 % TRYING [7]
% 172.46/24.85 % (2098433)Instruction limit reached!
% 172.46/24.85 % (2098433)------------------------------
% 172.46/24.85 % (2098433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.46/24.85 % (2098433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.46/24.85 % (2098433)CaDiCaL version: 2.1.3
% 172.46/24.85 % (2098433)Termination reason: Instruction limit
% 172.46/24.85 % (2098433)Termination phase: Finite model building SAT solving
% 172.46/24.85 % (2098433)Time elapsed: 5.317 s
% 172.46/24.85 % (2098433)Peak memory usage: 199 MB
% 172.46/24.85 % (2098433)Instructions burned: 22063 (million)
% 172.46/24.85 % (2098463)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4240416031:i=29340_2941 on theBenchmark for (2941ds/29340Mi)
% 172.46/24.85 % (2098461)Instruction limit reached!
% 172.46/24.85 % (2098461)------------------------------
% 172.46/24.85 % (2098461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.46/24.85 % (2098461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.46/24.85 % (2098461)CaDiCaL version: 2.1.3
% 172.46/24.85 % (2098461)Termination reason: Instruction limit
% 172.46/24.85 % (2098461)Termination phase: Saturation
% 172.46/24.85 % (2098461)Time elapsed: 1.466 s
% 172.46/24.85 % (2098461)Peak memory usage: 58 MB
% 172.46/24.85 % (2098461)Instructions burned: 4593 (million)
% 172.46/24.85 % (2098465)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1270801151:i=5211_2938 on theBenchmark for (2938ds/5211Mi)
% 172.46/24.85 % TRYING [7]
% 172.46/24.85 % (2098465)Instruction limit reached!
% 172.46/24.85 % (2098465)------------------------------
% 172.46/24.85 % (2098465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.46/24.85 % (2098465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.46/24.85 % (2098465)CaDiCaL version: 2.1.3
% 172.46/24.85 % (2098465)Termination reason: Instruction limit
% 172.46/24.85 % (2098465)Termination phase: Saturation
% 172.46/24.85 % (2098465)Time elapsed: 1.551 s
% 172.46/24.85 % (2098465)Peak memory usage: 67 MB
% 172.46/24.85 % (2098465)Instructions burned: 5213 (million)
% 172.46/24.85 % (2098467)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3131951434:i=5497:nm=2_2922 on theBenchmark for (2922ds/5497Mi)
% 151.28/25.69 % TRYING [17]
% 151.28/25.69 % (2098467)Instruction limit reached!
% 151.28/25.69 % (2098467)------------------------------
% 151.28/25.69 % (2098467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098467)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098467)Termination reason: Instruction limit
% 151.28/25.69 % (2098467)Termination phase: Finite model building constraint generation
% 151.28/25.69 % (2098467)Time elapsed: 1.063 s
% 151.28/25.69 % (2098467)Peak memory usage: 353 MB
% 151.28/25.69 % (2098467)Instructions burned: 5501 (million)
% 151.28/25.69 % (2098469)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=7272448:fmbsr=2:i=46332_2911 on theBenchmark for (2911ds/46332Mi)
% 151.28/25.69 % TRYING [15]
% 151.28/25.69 % (2098401)Instruction limit reached!
% 151.28/25.69 % (2098401)------------------------------
% 151.28/25.69 % (2098401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098401)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098401)Termination reason: Instruction limit
% 151.28/25.69 % (2098401)Termination phase: Saturation
% 151.28/25.69 % (2098401)Time elapsed: 14.649 s
% 151.28/25.69 % (2098401)Peak memory usage: 188 MB
% 151.28/25.69 % (2098401)Instructions burned: 88025 (million)
% 151.28/25.69 % (2098471)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1004004048:i=14071_2853 on theBenchmark for (2853ds/14071Mi)
% 151.28/25.69 % TRYING [12]
% 151.28/25.69 % (2098451)Instruction limit reached!
% 151.28/25.69 % (2098451)------------------------------
% 151.28/25.69 % (2098451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098451)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098451)Termination reason: Instruction limit
% 151.28/25.69 % (2098451)Termination phase: Finite model building constraint generation
% 151.28/25.69 % (2098451)Time elapsed: 12.750 s
% 151.28/25.69 % (2098451)Peak memory usage: 1897 MB
% 151.28/25.69 % (2098451)Instructions burned: 54285 (million)
% 151.28/25.69 % (2098463)Instruction limit reached!
% 151.28/25.69 % (2098463)------------------------------
% 151.28/25.69 % (2098463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098463)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098463)Termination reason: Instruction limit
% 151.28/25.69 % (2098463)Termination phase: Saturation
% 151.28/25.69 % (2098463)Time elapsed: 9.075 s
% 151.28/25.69 % (2098463)Peak memory usage: 313 MB
% 151.28/25.69 % (2098463)Instructions burned: 29342 (million)
% 151.28/25.69 % (2098473)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1114106585:i=22565:add=on:rawr=on_2850 on theBenchmark for (2850ds/22565Mi)
% 151.28/25.69 % (2098475)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=611794707:i=8173:av=off_2849 on theBenchmark for (2849ds/8173Mi)
% 151.28/25.69 % (2098475)Instruction limit reached!
% 151.28/25.69 % (2098475)------------------------------
% 151.28/25.69 % (2098475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098475)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098475)Termination reason: Instruction limit
% 151.28/25.69 % (2098475)Termination phase: Saturation
% 151.28/25.69 % (2098475)Time elapsed: 1.997 s
% 151.28/25.69 % (2098475)Peak memory usage: 75 MB
% 151.28/25.69 % (2098475)Instructions burned: 8173 (million)
% 151.28/25.69 % (2098477)dis+10_16:1_sil=16000:random_seed=3467529360:i=9155:fsr=off_2829 on theBenchmark for (2829ds/9155Mi)
% 151.28/25.69 % (2098471)Instruction limit reached!
% 151.28/25.69 % (2098471)------------------------------
% 151.28/25.69 % (2098471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098471)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098471)Termination reason: Instruction limit
% 151.28/25.69 % (2098471)Termination phase: Finite model building constraint generation
% 151.28/25.69 % (2098471)Time elapsed: 2.719 s
% 151.28/25.69 % (2098471)Peak memory usage: 906 MB
% 151.28/25.69 % (2098471)Instructions burned: 14075 (million)
% 151.28/25.69 % (2098479)ott-3_8_sil=64000:random_seed=968016068:i=20139:bs=on_2825 on theBenchmark for (2825ds/20139Mi)
% 151.28/25.69 % (2098469)Instruction limit reached!
% 151.28/25.69 % (2098469)------------------------------
% 151.28/25.69 % (2098469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098469)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098469)Termination reason: Instruction limit
% 151.28/25.69 % (2098469)Termination phase: Finite model building constraint generation
% 151.28/25.69 % (2098469)Time elapsed: 8.850 s
% 151.28/25.69 % (2098469)Peak memory usage: 2811 MB
% 151.28/25.69 % (2098469)Instructions burned: 46333 (million)
% 151.28/25.69 % (2098481)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3506129932:fmbsr=2:i=32576_2820 on theBenchmark for (2820ds/32576Mi)
% 151.28/25.69 % TRYING [9]
% 151.28/25.69 % (2098473)Instruction limit reached!
% 151.28/25.69 % (2098473)------------------------------
% 151.28/25.69 % (2098473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098473)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098473)Termination reason: Instruction limit
% 151.28/25.69 % (2098473)Termination phase: Saturation
% 151.28/25.69 % (2098473)Time elapsed: 4.419 s
% 151.28/25.69 % (2098473)Peak memory usage: 73 MB
% 151.28/25.69 % (2098473)Instructions burned: 22567 (million)
% 151.28/25.69 % (2098483)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2870988150:i=11404_2805 on theBenchmark for (2805ds/11404Mi)
% 151.28/25.69 % (2098477)Instruction limit reached!
% 151.28/25.69 % (2098477)------------------------------
% 151.28/25.69 % (2098477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098477)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098477)Termination reason: Instruction limit
% 151.28/25.69 % (2098477)Termination phase: Saturation
% 151.28/25.69 % (2098477)Time elapsed: 2.823 s
% 151.28/25.69 % (2098477)Peak memory usage: 91 MB
% 151.28/25.69 % (2098477)Instructions burned: 9156 (million)
% 151.28/25.69 % (2098485)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3539248256:i=14134_2800 on theBenchmark for (2800ds/14134Mi)
% 151.28/25.69 % (2098459)Instruction limit reached!
% 151.28/25.69 % (2098459)------------------------------
% 151.28/25.69 % (2098459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098459)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098459)Termination reason: Instruction limit
% 151.28/25.69 % (2098459)Termination phase: Finite model building SAT solving
% 151.28/25.69 % (2098459)Time elapsed: 16.907 s
% 151.28/25.69 % (2098459)Peak memory usage: 2394 MB
% 151.28/25.69 % (2098459)Instructions burned: 67535 (million)
% 151.28/25.69 % (2098488)dis+33_16_sil=32000:sac=on:random_seed=632442858:i=15851:nm=0_2787 on theBenchmark for (2787ds/15851Mi)
% 151.28/25.69 % (2098483)Instruction limit reached!
% 151.28/25.69 % (2098483)------------------------------
% 151.28/25.69 % (2098483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098483)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098483)Termination reason: Instruction limit
% 151.28/25.69 % (2098483)Termination phase: Saturation
% 151.28/25.69 % (2098483)Time elapsed: 3.188 s
% 151.28/25.69 % (2098483)Peak memory usage: 103 MB
% 151.28/25.69 % (2098483)Instructions burned: 11406 (million)
% 151.28/25.69 % (2098490)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3727485396:avsq=on:i=17627:add=on:amm=off_2773 on theBenchmark for (2773ds/17627Mi)
% 151.28/25.69 % (2098481)Instruction limit reached!
% 151.28/25.69 % (2098481)------------------------------
% 151.28/25.69 % (2098481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098481)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098481)Termination reason: Instruction limit
% 151.28/25.69 % (2098481)Termination phase: Finite model building constraint generation
% 151.28/25.69 % (2098481)Time elapsed: 6.570 s
% 151.28/25.69 % (2098481)Peak memory usage: 2059 MB
% 151.28/25.69 % (2098481)Instructions burned: 32577 (million)
% 151.28/25.69 % (2098485)Instruction limit reached!
% 151.28/25.69 % (2098485)------------------------------
% 151.28/25.69 % (2098485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098485)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098485)Termination reason: Instruction limit
% 151.28/25.69 % (2098485)Termination phase: Saturation
% 151.28/25.69 % (2098485)Time elapsed: 4.609 s
% 151.28/25.69 % (2098485)Peak memory usage: 163 MB
% 151.28/25.69 % (2098485)Instructions burned: 14137 (million)
% 151.28/25.69 % (2098492)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2045605180:s2a=on:i=53295_2754 on theBenchmark for (2754ds/53295Mi)
% 151.28/25.69 % (2098494)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2600391037:i=26857:ins=20_2753 on theBenchmark for (2753ds/26857Mi)
% 151.28/25.69 % TRYING [16]
% 151.28/25.69 % (2098479)Instruction limit reached!
% 151.28/25.69 % (2098479)------------------------------
% 151.28/25.69 % (2098479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.69 % (2098479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.69 % (2098479)CaDiCaL version: 2.1.3
% 151.28/25.69 % (2098479)Termination reason: Instruction limit
% 151.28/25.69 % (2098479)Termination phase: Saturation
% 151.28/25.69 % (2098479)Time elapsed: 7.179 s
% 151.28/25.69 % (2098479)Peak memory usage: 200 MB
% 151.28/25.69 % (2098479)Instructions burned: 20149 (million)
% 151.28/25.69 % (2098496)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3084939804:i=28120:bs=on:fsr=off_2753 on theBenchmark for (2753ds/28120Mi)
% 151.28/25.69 % (2098400) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2098394-2098400"...
% 151.28/25.69 % (2098400)...printing done.
% 151.28/25.69 % (2098400)Refutation found. Thanks to Tanya!
% 151.28/25.69 % SZS status Unsatisfiable for theBenchmark
% 151.28/25.69 % SZS output start Proof for theBenchmark
% See solution above
% 151.28/25.70 % (2098400)------------------------------
% 151.28/25.70 % (2098400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.28/25.70 % (2098400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.28/25.70 % (2098400)CaDiCaL version: 2.1.3
% 151.28/25.70 % (2098400)Termination reason: Refutation
% 151.28/25.70 % (2098400)Time elapsed: 25.117 s
% 151.28/25.70 % (2098400)Peak memory usage: 648 MB
% 151.28/25.70 % (2098400)Instructions burned: 78880 (million)
% 151.28/25.70 % (2098394)Success in time 25.368 s
% 151.28/25.70 % Vampire exiting
%------------------------------------------------------------------------------