%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP777+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:11 AM UTC 2026
% Result : Theorem 19.86s 3.67s
% Output : Refutation 20.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 10
% Syntax : Number of formulae : 150 ( 150 unt; 0 def)
% Number of atoms : 150 ( 149 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 365 ( 364 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : difference(X1,product(X1,X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos01) ).
fof(f2,axiom,
! [X0,X1] : product(X1,difference(X1,X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos02) ).
fof(f3,axiom,
! [X0,X1] : quotient(product(X1,X0),X0) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos03) ).
fof(f4,axiom,
! [X0,X1] : product(quotient(X1,X0),X0) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos04) ).
fof(f5,axiom,
! [X0,X1,X2,X3] : product(product(X3,X2),product(X1,X0)) = product(product(X3,X1),product(X2,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos05) ).
fof(f6,axiom,
! [X0] : product(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos06) ).
fof(f7,axiom,
! [X0,X1] : product(product(product(X1,X0),X0),product(X0,product(X0,X1))) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos07) ).
fof(f8,axiom,
! [X0,X1,X2] : bigC(X2,X1,X0) = product(product(X2,X1),product(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos08) ).
fof(f9,axiom,
product(product(a,c),product(c,b)) = product(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos09) ).
fof(f10,conjecture,
! [X0] : bigC(a,b,X0) = bigC(c,c,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f11,negated_conjecture,
~ ! [X0] : bigC(a,b,X0) = bigC(c,c,X0),
inference(negated_conjecture,[status(cth)],[f10]) ).
fof(f12,plain,
? [X0] : bigC(a,b,X0) != bigC(c,c,X0),
inference(ennf_transformation,[],[f11]) ).
fof(f13,plain,
bigC(a,b,sK0) != bigC(c,c,sK0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f12]) ).
fof(f14,plain,
! [X0,X1] : difference(X1,product(X1,X0)) = X0,
inference(cnf_transformation,[],[f1]) ).
fof(f15,plain,
! [X0,X1] : product(X1,difference(X1,X0)) = X0,
inference(cnf_transformation,[],[f2]) ).
fof(f16,plain,
! [X0,X1] : quotient(product(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f3]) ).
fof(f17,plain,
! [X0,X1] : product(quotient(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f4]) ).
fof(f18,plain,
! [X2,X3,X0,X1] : product(product(X3,X2),product(X1,X0)) = product(product(X3,X1),product(X2,X0)),
inference(cnf_transformation,[],[f5]) ).
fof(f19,plain,
! [X0] : product(X0,X0) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f20,plain,
! [X0,X1] : product(product(product(X1,X0),X0),product(X0,product(X0,X1))) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f21,plain,
! [X2,X0,X1] : bigC(X2,X1,X0) = product(product(X2,X1),product(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f22,plain,
product(product(a,c),product(c,b)) = product(a,b),
inference(cnf_transformation,[],[f9]) ).
fof(f23,plain,
bigC(a,b,sK0) != bigC(c,c,sK0),
inference(cnf_transformation,[],[f13]) ).
fof(f24,plain,
product(product(a,b),product(sK0,a)) != product(product(c,c),product(sK0,c)),
inference(definition_unfolding,[],[f23,f21,f21]) ).
fof(f63,plain,
! [X2,X3,X0,X1] : product(product(X1,X2),X0) = product(product(X1,X3),product(X2,difference(X3,X0))),
inference(superposition,[],[f18,f15]) ).
fof(f64,plain,
! [X2,X3,X0,X1] : product(X0,product(X2,X3)) = product(product(X1,X2),product(difference(X1,X0),X3)),
inference(superposition,[],[f18,f15]) ).
fof(f66,plain,
! [X2,X3,X0,X1] : product(X1,X3) = difference(product(X0,X2),product(product(X0,X1),product(X2,X3))),
inference(superposition,[],[f14,f18]) ).
fof(f80,plain,
! [X2,X3,X0,X1] : product(difference(X3,X0),X2) = difference(product(X3,X1),product(X0,product(X1,X2))),
inference(superposition,[],[f14,f64]) ).
fof(f123,plain,
! [X2,X3,X0,X1] : product(X1,difference(X3,X2)) = difference(product(X0,X3),product(product(X0,X1),X2)),
inference(superposition,[],[f14,f63]) ).
fof(f209,plain,
! [X2,X3,X0,X1] : product(product(X1,X3),X0) = product(product(X1,quotient(X0,X2)),product(X3,X2)),
inference(superposition,[],[f18,f17]) ).
fof(f212,plain,
! [X2,X3,X0,X1] : product(product(quotient(X0,X1),X2),X3) = product(X0,product(X2,difference(X1,X3))),
inference(superposition,[],[f63,f17]) ).
fof(f278,plain,
! [X2,X0,X1] : product(X0,product(X1,X2)) = product(product(X0,X1),product(X0,X2)),
inference(superposition,[],[f18,f19]) ).
fof(f279,plain,
! [X2,X0,X1] : product(product(X1,X2),X0) = product(product(X1,X0),product(X2,X0)),
inference(superposition,[],[f18,f19]) ).
fof(f326,plain,
! [X0,X1] : product(product(X0,X1),X0) = product(X0,product(X1,X0)),
inference(superposition,[],[f278,f19]) ).
fof(f499,plain,
! [X2,X0,X1] : product(difference(X0,X1),X2) = difference(X0,product(X1,product(X0,X2))),
inference(superposition,[],[f80,f19]) ).
fof(f500,plain,
! [X2,X3,X0,X1] : product(difference(quotient(X0,X1),X2),X3) = difference(X0,product(X2,product(X1,X3))),
inference(superposition,[],[f80,f17]) ).
fof(f510,plain,
! [X2,X3,X0,X1] : product(difference(X1,X2),difference(X3,X0)) = difference(product(X1,X3),product(X2,X0)),
inference(superposition,[],[f80,f15]) ).
fof(f511,plain,
! [X2,X0,X1] : product(difference(X1,X2),X0) = difference(product(X1,X0),product(X2,X0)),
inference(superposition,[],[f80,f19]) ).
fof(f540,plain,
! [X2,X0,X1] : product(difference(X0,X1),X2) = product(difference(quotient(X0,X0),X1),X2),
inference(forward_demodulation,[],[f499,f500]) ).
fof(f568,plain,
! [X2,X0,X1] : product(X0,X1) = quotient(product(X0,product(X1,X2)),product(X0,X2)),
inference(superposition,[],[f16,f278]) ).
fof(f575,plain,
! [X2,X3,X0,X1] : product(X0,quotient(X2,X3)) = quotient(product(product(X0,X1),X2),product(X1,X3)),
inference(superposition,[],[f16,f209]) ).
fof(f576,plain,
! [X0,X1] : quotient(X0,difference(X1,X0)) = X1,
inference(superposition,[],[f16,f15]) ).
fof(f577,plain,
! [X0] : quotient(X0,X0) = X0,
inference(superposition,[],[f16,f19]) ).
fof(f635,plain,
! [X2,X3,X0,X1] : product(X1,difference(difference(X2,X0),X3)) = difference(X0,product(product(X2,X1),X3)),
inference(superposition,[],[f123,f15]) ).
fof(f650,plain,
! [X2,X3,X0,X1] : difference(product(X0,X3),product(product(X0,X1),X2)) = product(X2,difference(X3,product(X1,X2))),
inference(superposition,[],[f123,f279]) ).
fof(f654,plain,
! [X2,X3,X0,X1,X4] : product(X1,difference(X3,product(difference(X4,X0),X2))) = difference(product(X4,X3),product(X0,product(X1,X2))),
inference(superposition,[],[f123,f64]) ).
fof(f677,plain,
! [X2,X3,X0,X1,X4] : product(X1,difference(X3,product(difference(X4,X0),X2))) = product(difference(quotient(product(X4,X3),X1),X0),X2),
inference(forward_demodulation,[],[f654,f500]) ).
fof(f681,plain,
! [X2,X3,X1] : product(X1,difference(X3,X2)) = product(X2,difference(X3,product(X1,X2))),
inference(forward_demodulation,[],[f650,f123]) ).
fof(f902,plain,
! [X2,X0,X1] : product(X1,quotient(X0,X2)) = quotient(product(X1,X0),product(X1,X2)),
inference(superposition,[],[f568,f17]) ).
fof(f969,plain,
! [X0,X1] : quotient(X0,product(X0,X1)) = product(X0,quotient(X0,X1)),
inference(superposition,[],[f902,f19]) ).
fof(f982,plain,
! [X0,X1] : product(X0,quotient(X1,X0)) = quotient(product(X0,X1),X0),
inference(superposition,[],[f902,f19]) ).
fof(f1037,plain,
! [X0,X1] : product(difference(X0,X1),X0) = difference(X0,product(X1,X0)),
inference(superposition,[],[f511,f19]) ).
fof(f1050,plain,
! [X0,X1] : difference(product(X1,X0),X0) = product(difference(X1,X0),X0),
inference(superposition,[],[f511,f19]) ).
fof(f1051,plain,
! [X2,X0,X1] : difference(product(X1,X2),X0) = product(difference(X1,quotient(X0,X2)),X2),
inference(superposition,[],[f511,f17]) ).
fof(f1136,plain,
! [X2,X3,X0,X1] : product(quotient(X0,X1),quotient(X2,X3)) = quotient(product(X0,X2),product(X1,X3)),
inference(superposition,[],[f575,f17]) ).
fof(f2248,plain,
! [X2,X0,X1] : product(X1,difference(X2,X0)) = product(quotient(X0,X1),difference(X2,X1)),
inference(superposition,[],[f681,f17]) ).
fof(f2252,plain,
! [X2,X3,X0,X1] : product(X1,difference(product(X0,X3),product(X3,X2))) = product(product(X3,X2),product(difference(X0,X1),X2)),
inference(superposition,[],[f681,f80]) ).
fof(f2261,plain,
! [X2,X0,X1] : difference(X1,product(X0,X2)) = difference(X2,product(X0,difference(X1,X2))),
inference(superposition,[],[f14,f681]) ).
fof(f2276,plain,
! [X2,X3,X0,X1,X4] : product(difference(X3,X4),difference(X1,product(X0,X2))) = difference(product(X3,X2),product(X4,product(X0,difference(X1,X2)))),
inference(superposition,[],[f80,f681]) ).
fof(f2327,plain,
! [X2,X3,X0,X1,X4] : product(difference(X3,X4),difference(X1,product(X0,X2))) = product(difference(quotient(product(X3,X2),X0),X4),difference(X1,X2)),
inference(forward_demodulation,[],[f2276,f500]) ).
fof(f2339,plain,
! [X2,X3,X0,X1] : product(product(X3,difference(X0,X1)),X2) = product(X1,difference(product(X0,X3),product(X3,X2))),
inference(forward_demodulation,[],[f2252,f279]) ).
fof(f2364,plain,
! [X2,X3,X0,X1,X4] : product(difference(X3,X4),difference(X1,product(X0,X2))) = product(X0,difference(X2,product(difference(X3,X4),difference(X1,X2)))),
inference(forward_demodulation,[],[f2327,f677]) ).
fof(f2374,plain,
! [X2,X3,X0,X1] : product(product(X3,difference(X0,X1)),X2) = product(X1,product(difference(X0,X3),difference(X3,X2))),
inference(forward_demodulation,[],[f2339,f510]) ).
fof(f2393,plain,
! [X2,X3,X0,X1,X4] : product(difference(X3,X4),difference(X1,product(X0,X2))) = product(X0,difference(X1,product(difference(X3,X4),X2))),
inference(forward_demodulation,[],[f2364,f2261]) ).
fof(f2441,plain,
! [X2,X3,X0,X1,X4] : product(product(X0,difference(X1,X2)),product(X3,X4)) = product(product(quotient(X2,X0),X3),product(difference(X1,X0),X4)),
inference(superposition,[],[f18,f2248]) ).
fof(f2505,plain,
! [X2,X3,X0,X1,X4] : product(product(X0,difference(X1,X2)),product(X3,X4)) = product(X2,product(X3,difference(X0,product(difference(X1,X0),X4)))),
inference(forward_demodulation,[],[f2441,f212]) ).
fof(f4818,plain,
! [X2,X0,X1] : quotient(product(X1,X2),X0) = product(quotient(X1,X0),quotient(X2,X0)),
inference(superposition,[],[f1136,f19]) ).
fof(f4971,plain,
! [X2,X0,X1] : quotient(product(X1,product(X0,X2)),X2) = product(quotient(X1,X2),X0),
inference(superposition,[],[f4818,f16]) ).
fof(f5144,plain,
! [X0,X1] : quotient(X0,product(X0,X1)) = product(quotient(product(product(X1,X0),X0),product(X0,X1)),X0),
inference(superposition,[],[f4971,f20]) ).
fof(f5188,plain,
! [X0,X1] : quotient(X0,product(X0,X1)) = product(product(quotient(product(X1,X0),X0),quotient(X0,X1)),X0),
inference(forward_demodulation,[],[f5144,f1136]) ).
fof(f5227,plain,
! [X0,X1] : quotient(X0,product(X0,X1)) = product(product(X1,X0),product(quotient(X0,X1),difference(X0,X0))),
inference(forward_demodulation,[],[f5188,f212]) ).
fof(f5250,plain,
! [X0,X1] : quotient(X0,product(X0,X1)) = product(product(X1,quotient(X0,X1)),X0),
inference(forward_demodulation,[],[f5227,f63]) ).
fof(f5258,plain,
! [X0,X1] : product(X0,quotient(X0,X1)) = product(product(X1,quotient(X0,X1)),X0),
inference(forward_demodulation,[],[f5250,f969]) ).
fof(f5269,plain,
! [X0,X1] : product(product(X0,X1),X0) = product(product(X1,X0),product(X0,X1)),
inference(superposition,[],[f5258,f16]) ).
fof(f5277,plain,
! [X0,X1] : product(X1,X0) = product(product(difference(X0,X1),X0),X1),
inference(superposition,[],[f5258,f576]) ).
fof(f5406,plain,
! [X0,X1] : product(X0,product(X1,X0)) = product(product(X1,X0),product(X0,X1)),
inference(forward_demodulation,[],[f5269,f326]) ).
fof(f5580,plain,
! [X2,X0,X1] : product(X1,quotient(product(X0,X1),X2)) = quotient(product(X0,product(X1,X0)),product(X0,X2)),
inference(superposition,[],[f575,f5406]) ).
fof(f5598,plain,
! [X2,X3,X0,X1] : product(X2,product(X0,X1)) = difference(product(X3,product(X1,X0)),product(product(X3,X2),product(X0,product(X1,X0)))),
inference(superposition,[],[f66,f5406]) ).
fof(f5662,plain,
! [X2,X3,X0,X1] : product(X2,product(X0,X1)) = product(X2,difference(difference(X3,product(X3,product(X1,X0))),product(X0,product(X1,X0)))),
inference(forward_demodulation,[],[f5598,f635]) ).
fof(f5674,plain,
! [X2,X0,X1] : product(X1,quotient(product(X0,X1),X2)) = product(X0,quotient(product(X1,X0),X2)),
inference(forward_demodulation,[],[f5580,f902]) ).
fof(f5763,plain,
! [X2,X3,X0,X1] : product(X2,product(X0,X1)) = product(X2,product(difference(quotient(difference(X3,product(X3,product(X1,X0))),X1),X0),X0)),
inference(forward_demodulation,[],[f5662,f500]) ).
fof(f5843,plain,
! [X2,X0,X1] : product(X2,product(X0,X1)) = product(X2,product(difference(quotient(product(X1,X0),X1),X0),X0)),
inference(forward_demodulation,[],[f5763,f14]) ).
fof(f5901,plain,
! [X2,X0,X1] : product(X2,product(X0,X1)) = product(X2,product(X1,difference(X0,product(difference(X1,X0),X0)))),
inference(forward_demodulation,[],[f5843,f677]) ).
fof(f5940,plain,
! [X2,X0,X1] : product(X2,product(X0,X1)) = product(product(X0,difference(X1,X2)),product(X1,X0)),
inference(forward_demodulation,[],[f5901,f2505]) ).
fof(f5964,plain,
! [X2,X0,X1] : product(X2,product(X0,X1)) = product(product(X0,X1),product(difference(X1,X2),X0)),
inference(forward_demodulation,[],[f5940,f18]) ).
fof(f6609,plain,
! [X2,X0,X1] : product(product(X2,X1),product(X0,X2)) = product(product(X1,X0),product(X2,X1)),
inference(superposition,[],[f5964,f14]) ).
fof(f6652,plain,
! [X2,X0,X1] : product(difference(X2,X0),X1) = difference(product(X1,X2),product(X0,product(X1,X2))),
inference(superposition,[],[f14,f5964]) ).
fof(f6738,plain,
! [X2,X0,X1] : product(difference(X2,X0),X1) = product(difference(quotient(product(X1,X2),X1),X0),X2),
inference(forward_demodulation,[],[f6652,f500]) ).
fof(f6809,plain,
! [X2,X0,X1] : product(difference(X2,X0),X1) = product(X1,difference(X2,product(difference(X1,X0),X2))),
inference(forward_demodulation,[],[f6738,f677]) ).
fof(f6856,plain,
! [X2,X0,X1] : product(difference(X2,X0),X1) = product(X1,product(difference(X2,difference(X1,X0)),X2)),
inference(forward_demodulation,[],[f6809,f1037]) ).
fof(f9898,plain,
! [X0,X1] : product(difference(X1,X0),X1) = quotient(product(X0,X1),X0),
inference(superposition,[],[f16,f5277]) ).
fof(f10162,plain,
! [X0,X1] : quotient(X0,quotient(X0,X1)) = product(difference(X1,quotient(X0,X1)),X1),
inference(superposition,[],[f9898,f17]) ).
fof(f10336,plain,
! [X0,X1] : quotient(X0,quotient(X0,X1)) = difference(product(X1,X1),X0),
inference(forward_demodulation,[],[f10162,f1051]) ).
fof(f10423,plain,
! [X0,X1] : difference(X1,X0) = quotient(X0,quotient(X0,X1)),
inference(forward_demodulation,[],[f10336,f19]) ).
fof(f10598,plain,
! [X0,X1] : quotient(product(X0,X1),X0) = difference(X1,product(X0,X1)),
inference(superposition,[],[f10423,f16]) ).
fof(f10748,plain,
! [X2,X0,X1] : quotient(product(X0,product(X1,X2)),X0) = product(difference(X1,X0),difference(X2,product(X1,X2))),
inference(superposition,[],[f510,f10598]) ).
fof(f10755,plain,
! [X2,X0,X1] : quotient(product(X0,product(X1,X2)),X0) = product(X1,difference(X2,product(difference(X1,X0),X2))),
inference(forward_demodulation,[],[f10748,f2393]) ).
fof(f10832,plain,
! [X2,X0,X1] : quotient(product(X0,product(X1,X2)),X0) = product(X1,product(difference(X2,difference(X1,X0)),X2)),
inference(forward_demodulation,[],[f10755,f1037]) ).
fof(f10892,plain,
! [X2,X0,X1] : product(difference(X2,X0),X1) = quotient(product(X0,product(X1,X2)),X0),
inference(forward_demodulation,[],[f10832,f6856]) ).
fof(f10935,plain,
! [X2,X0,X1] : product(difference(X2,X0),X1) = product(X0,quotient(product(X1,X2),X0)),
inference(forward_demodulation,[],[f10892,f982]) ).
fof(f11393,plain,
! [X2,X0,X1] : product(X2,quotient(X0,X2)) = product(difference(X1,X2),quotient(X0,X1)),
inference(superposition,[],[f10935,f17]) ).
fof(f11706,plain,
! [X2,X0,X1] : product(X0,quotient(X2,X1)) = product(product(X1,X0),quotient(X2,product(X1,X0))),
inference(superposition,[],[f11393,f14]) ).
fof(f12192,plain,
! [X2,X0,X1] : product(product(X2,X1),X0) = product(X1,quotient(product(X0,product(X2,X1)),X2)),
inference(superposition,[],[f11706,f16]) ).
fof(f12211,plain,
! [X2,X3,X0,X1] : product(X0,quotient(product(X1,X2),X3)) = product(difference(X2,product(X3,X0)),X1),
inference(superposition,[],[f10935,f11706]) ).
fof(f12225,plain,
! [X2,X3,X0,X1,X4] : product(X3,quotient(X1,product(X2,X0))) = difference(product(X4,product(X2,X0)),product(product(X4,X3),product(X0,quotient(X1,X2)))),
inference(superposition,[],[f66,f11706]) ).
fof(f12316,plain,
! [X2,X3,X0,X1,X4] : product(X3,quotient(X1,product(X2,X0))) = product(X3,difference(difference(X4,product(X4,product(X2,X0))),product(X0,quotient(X1,X2)))),
inference(forward_demodulation,[],[f12225,f635]) ).
fof(f12410,plain,
! [X2,X3,X0,X1] : product(X3,quotient(X1,product(X2,X0))) = product(X3,difference(product(X2,X0),product(X0,quotient(X1,X2)))),
inference(forward_demodulation,[],[f12316,f14]) ).
fof(f12455,plain,
! [X2,X3,X0,X1] : product(X3,quotient(X1,product(X2,X0))) = product(X3,product(difference(X2,X0),difference(X0,quotient(X1,X2)))),
inference(forward_demodulation,[],[f12410,f510]) ).
fof(f12483,plain,
! [X2,X3,X0,X1] : product(product(X0,difference(X2,X3)),quotient(X1,X2)) = product(X3,quotient(X1,product(X2,X0))),
inference(forward_demodulation,[],[f12455,f2374]) ).
fof(f12565,plain,
! [X2,X0,X1] : product(X0,X2) = product(X1,quotient(product(X2,X0),quotient(X0,X1))),
inference(superposition,[],[f12192,f17]) ).
fof(f12590,plain,
product(product(c,b),product(a,c)) = product(b,quotient(product(a,b),c)),
inference(superposition,[],[f12192,f22]) ).
fof(f12764,plain,
product(product(c,b),product(a,c)) = product(a,quotient(product(b,a),c)),
inference(forward_demodulation,[],[f12590,f5674]) ).
fof(f12877,plain,
product(product(c,a),product(b,c)) = product(a,quotient(product(b,a),c)),
inference(forward_demodulation,[],[f12764,f18]) ).
fof(f13091,plain,
! [X2,X0,X1] : difference(X2,product(X0,X1)) = quotient(product(X1,X0),quotient(X0,X2)),
inference(superposition,[],[f14,f12565]) ).
fof(f13101,plain,
! [X2,X3,X0,X1,X4] : product(quotient(product(X1,X0),quotient(X0,X2)),X3) = difference(product(X2,X4),product(product(X0,X1),product(X4,X3))),
inference(superposition,[],[f66,f12565]) ).
fof(f13204,plain,
! [X2,X3,X0,X1,X4] : product(quotient(product(X1,X0),quotient(X0,X2)),X3) = product(X1,difference(difference(X0,product(X2,X4)),product(X4,X3))),
inference(forward_demodulation,[],[f13101,f635]) ).
fof(f13307,plain,
! [X2,X3,X0,X1,X4] : product(X1,difference(difference(X0,product(X2,X4)),product(X4,X3))) = product(difference(X2,product(X0,X1)),X3),
inference(forward_demodulation,[],[f13204,f13091]) ).
fof(f13379,plain,
! [X2,X3,X0,X1,X4] : product(X1,difference(difference(X0,product(X2,X4)),product(X4,X3))) = product(X1,quotient(product(X3,X2),X0)),
inference(forward_demodulation,[],[f13307,f12211]) ).
fof(f13474,plain,
! [X0,X1] : product(X0,product(b,c)) = difference(product(X1,product(c,a)),product(product(X1,X0),product(a,quotient(product(b,a),c)))),
inference(superposition,[],[f66,f12877]) ).
fof(f13575,plain,
! [X0,X1] : product(X0,product(b,c)) = product(X0,difference(difference(X1,product(X1,product(c,a))),product(a,quotient(product(b,a),c)))),
inference(forward_demodulation,[],[f13474,f635]) ).
fof(f13629,plain,
! [X0] : product(X0,product(b,c)) = product(X0,difference(product(c,a),product(a,quotient(product(b,a),c)))),
inference(forward_demodulation,[],[f13575,f14]) ).
fof(f13675,plain,
! [X0] : product(X0,product(b,c)) = product(X0,product(difference(c,a),difference(a,quotient(product(b,a),c)))),
inference(forward_demodulation,[],[f13629,f510]) ).
fof(f13716,plain,
! [X0] : product(X0,product(b,c)) = product(product(a,difference(c,X0)),quotient(product(b,a),c)),
inference(forward_demodulation,[],[f13675,f2374]) ).
fof(f13747,plain,
! [X0] : product(X0,product(b,c)) = product(X0,quotient(product(b,a),product(c,a))),
inference(forward_demodulation,[],[f13716,f12483]) ).
fof(f13770,plain,
! [X0] : product(X0,product(b,c)) = product(X0,product(quotient(b,c),quotient(a,a))),
inference(forward_demodulation,[],[f13747,f1136]) ).
fof(f13786,plain,
! [X0] : product(X0,product(b,c)) = product(X0,product(quotient(b,c),a)),
inference(forward_demodulation,[],[f13770,f577]) ).
fof(f13841,plain,
! [X2,X0,X1] : product(product(quotient(b,c),a),X1) = difference(product(X0,X2),product(product(X0,product(b,c)),product(X2,X1))),
inference(superposition,[],[f66,f13786]) ).
fof(f14004,plain,
! [X2,X0,X1] : product(product(quotient(b,c),a),X1) = product(product(b,c),difference(difference(X0,product(X0,X2)),product(X2,X1))),
inference(forward_demodulation,[],[f13841,f635]) ).
fof(f14088,plain,
! [X0,X1] : product(product(quotient(b,c),a),X1) = product(product(b,c),quotient(product(X1,X0),X0)),
inference(forward_demodulation,[],[f14004,f13379]) ).
fof(f14144,plain,
! [X1] : product(product(b,c),X1) = product(product(quotient(b,c),a),X1),
inference(forward_demodulation,[],[f14088,f16]) ).
fof(f14177,plain,
! [X1] : product(product(b,c),X1) = product(b,product(a,difference(c,X1))),
inference(forward_demodulation,[],[f14144,f212]) ).
fof(f14253,plain,
! [X0] : product(product(b,c),product(c,X0)) = product(b,product(a,X0)),
inference(superposition,[],[f14177,f14]) ).
fof(f14515,plain,
product(b,product(a,b)) = product(c,product(b,c)),
inference(superposition,[],[f5406,f14253]) ).
fof(f14522,plain,
product(product(b,c),c) = product(b,product(a,c)),
inference(superposition,[],[f279,f14253]) ).
fof(f14873,plain,
product(a,b) = difference(b,product(c,product(b,c))),
inference(superposition,[],[f14,f14515]) ).
fof(f14991,plain,
product(a,b) = product(difference(quotient(b,b),c),c),
inference(forward_demodulation,[],[f14873,f500]) ).
fof(f15037,plain,
product(a,b) = product(difference(b,c),c),
inference(forward_demodulation,[],[f14991,f540]) ).
fof(f15686,plain,
c = product(product(b,product(a,c)),product(c,product(c,b))),
inference(superposition,[],[f20,f14522]) ).
fof(f15806,plain,
c = product(product(b,c),product(product(a,c),product(c,b))),
inference(forward_demodulation,[],[f15686,f18]) ).
fof(f15850,plain,
c = product(product(b,c),product(a,b)),
inference(forward_demodulation,[],[f15806,f22]) ).
fof(f15888,plain,
c = product(product(c,a),product(b,c)),
inference(forward_demodulation,[],[f15850,f6609]) ).
fof(f16032,plain,
quotient(c,product(c,a)) = difference(product(b,c),c),
inference(superposition,[],[f10598,f15888]) ).
fof(f16041,plain,
quotient(c,product(c,a)) = product(difference(b,c),c),
inference(forward_demodulation,[],[f16032,f1050]) ).
fof(f16096,plain,
product(a,b) = quotient(c,product(c,a)),
inference(forward_demodulation,[],[f16041,f15037]) ).
fof(f16141,plain,
product(a,b) = product(c,quotient(c,a)),
inference(forward_demodulation,[],[f16096,f969]) ).
fof(f16499,plain,
! [X0] : product(product(c,X0),c) = product(product(a,b),product(X0,a)),
inference(superposition,[],[f209,f16141]) ).
fof(f16610,plain,
! [X0] : product(c,product(X0,c)) = product(product(a,b),product(X0,a)),
inference(forward_demodulation,[],[f16499,f326]) ).
fof(f20676,plain,
product(product(c,c),product(sK0,c)) != product(c,product(sK0,c)),
inference(superposition,[],[f24,f16610]) ).
fof(f20834,plain,
product(c,product(sK0,c)) != product(product(c,sK0),c),
inference(forward_demodulation,[],[f20676,f279]) ).
fof(f20905,plain,
$false,
inference(forward_subsumption_resolution,[],[f20834,f326]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP777+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 10:45:54 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.60/2.30 % (2147782)Detected formulas, will run a generic FOF schedule.
% 10.60/2.30 % (2147793)dis-21_1_sil=8000:lcm=predicate:random_seed=3129298327:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.60/2.30 % (2147793)Refutation not found, incomplete strategy
% 10.60/2.30 % (2147793)------------------------------
% 10.60/2.30 % (2147793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.60/2.30 % (2147793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.60/2.30 % (2147793)CaDiCaL version: 2.1.3
% 10.60/2.30 % (2147793)Termination reason: Refutation not found, incomplete strategy
% 10.60/2.30 % (2147793)Time elapsed: 0.001 s
% 10.60/2.30 % (2147793)Peak memory usage: 88 MB
% 10.60/2.30 % (2147787)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=731010486:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.60/2.30 % (2147788)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3427086675:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.60/2.30 % (2147790)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3868026647:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.60/2.30 % (2147791)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1285804838:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.60/2.30 % (2147789)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3793414942:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.60/2.30 % (2147790)Refutation not found, incomplete strategy
% 10.60/2.30 % (2147790)------------------------------
% 10.60/2.30 % (2147790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.60/2.30 % (2147790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.60/2.30 % (2147790)CaDiCaL version: 2.1.3
% 10.60/2.30 % (2147790)Termination reason: Refutation not found, incomplete strategy
% 10.60/2.30 % (2147790)Time elapsed: 0.001 s
% 10.60/2.30 % (2147790)Peak memory usage: 88 MB
% 10.60/2.30 % (2147792)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2663048133:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.60/2.30 % (2147791)Instruction limit reached!
% 10.60/2.30 % (2147791)------------------------------
% 10.60/2.30 % (2147791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.60/2.30 % (2147791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.60/2.30 % (2147791)CaDiCaL version: 2.1.3
% 10.60/2.30 % (2147791)Termination reason: Instruction limit
% 10.60/2.30 % (2147791)Termination phase: Saturation
% 10.60/2.30 % (2147791)Time elapsed: 0.066 s
% 10.60/2.30 % (2147791)Peak memory usage: 89 MB
% 10.60/2.30 % (2147791)Instructions burned: 121 (million)
% 10.60/2.30 % (2147793)------------------------------
% 10.60/2.30 % (2147793)------------------------------
% 10.60/2.30 % (2147792)Instruction limit reached!
% 10.60/2.30 % (2147792)------------------------------
% 10.60/2.30 % (2147792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.60/2.30 % (2147792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.60/2.30 % (2147792)CaDiCaL version: 2.1.3
% 10.60/2.30 % (2147792)Termination reason: Instruction limit
% 10.60/2.30 % (2147792)Termination phase: Saturation
% 10.60/2.30 % (2147792)Time elapsed: 0.085 s
% 10.60/2.30 % (2147792)Peak memory usage: 89 MB
% 10.60/2.30 % (2147792)Instructions burned: 139 (million)
% 10.60/2.30 % (2147802)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3227927519:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.60/2.30 % (2147802)Refutation not found, incomplete strategy
% 10.60/2.30 % (2147802)------------------------------
% 10.60/2.30 % (2147802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.60/2.30 % (2147802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.60/2.30 % (2147802)CaDiCaL version: 2.1.3
% 10.60/2.30 % (2147802)Termination reason: Refutation not found, incomplete strategy
% 10.60/2.30 % (2147802)Time elapsed: 0.001 s
% 10.60/2.30 % (2147802)Peak memory usage: 88 MB
% 10.60/2.30 % (2147801)lrs+10_1_sil=8000:sp=occurrence:random_seed=2349677895:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 13.93/2.95 % (2147803)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3070649130:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.93/2.95 % (2147790)------------------------------
% 13.93/2.95 % (2147790)------------------------------
% 13.93/2.95 % (2147802)------------------------------
% 13.93/2.95 % (2147802)------------------------------
% 13.93/2.95 % (2147801)Instruction limit reached!
% 13.93/2.95 % (2147801)------------------------------
% 13.93/2.95 % (2147801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.93/2.95 % (2147801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.93/2.95 % (2147801)CaDiCaL version: 2.1.3
% 13.93/2.95 % (2147801)Termination reason: Instruction limit
% 13.93/2.95 % (2147801)Termination phase: Saturation
% 13.93/2.95 % (2147801)Time elapsed: 0.184 s
% 13.93/2.95 % (2147801)Peak memory usage: 91 MB
% 13.93/2.95 % (2147801)Instructions burned: 286 (million)
% 13.93/2.95 % (2147807)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1763906278:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 13.93/2.95 % (2147808)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3583542430:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 13.93/2.95 % (2147808)Refutation not found, incomplete strategy
% 13.93/2.95 % (2147808)------------------------------
% 13.93/2.95 % (2147808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.93/2.95 % (2147808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.93/2.95 % (2147808)CaDiCaL version: 2.1.3
% 13.93/2.95 % (2147808)Termination reason: Refutation not found, incomplete strategy
% 13.93/2.95 % (2147808)Time elapsed: 0.001 s
% 13.93/2.95 % (2147808)Peak memory usage: 88 MB
% 13.93/2.95 % (2147803)Instruction limit reached!
% 13.93/2.95 % (2147803)------------------------------
% 13.93/2.95 % (2147803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.93/2.95 % (2147803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.93/2.95 % (2147803)CaDiCaL version: 2.1.3
% 13.93/2.95 % (2147803)Termination reason: Instruction limit
% 13.93/2.95 % (2147803)Termination phase: Saturation
% 13.93/2.95 % (2147803)Time elapsed: 0.214 s
% 13.93/2.95 % (2147803)Peak memory usage: 92 MB
% 13.93/2.95 % (2147803)Instructions burned: 325 (million)
% 13.93/2.95 % (2147809)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3438165439:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 13.93/2.95 % (2147807)Instruction limit reached!
% 13.93/2.95 % (2147807)------------------------------
% 13.93/2.95 % (2147807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.93/2.95 % (2147807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.93/2.95 % (2147807)CaDiCaL version: 2.1.3
% 13.93/2.95 % (2147807)Termination reason: Instruction limit
% 13.93/2.95 % (2147807)Termination phase: Saturation
% 13.93/2.95 % (2147807)Time elapsed: 0.156 s
% 13.93/2.95 % (2147807)Peak memory usage: 91 MB
% 13.93/2.95 % (2147807)Instructions burned: 249 (million)
% 13.93/2.95 % (2147808)------------------------------
% 13.93/2.95 % (2147808)------------------------------
% 13.93/2.95 % (2147812)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3975377566:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 13.93/2.95 % (2147812)Refutation not found, incomplete strategy
% 13.93/2.95 % (2147812)------------------------------
% 13.93/2.95 % (2147812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.93/2.95 % (2147812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.93/2.95 % (2147812)CaDiCaL version: 2.1.3
% 13.93/2.95 % (2147812)Termination reason: Refutation not found, incomplete strategy
% 13.93/2.95 % (2147812)Time elapsed: 0.001 s
% 13.93/2.95 % (2147812)Peak memory usage: 88 MB
% 13.93/2.95 % (2147789)Refutation not found, incomplete strategy
% 13.93/2.95 % (2147789)------------------------------
% 13.93/2.95 % (2147789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.93/2.95 % (2147789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.93/2.95 % (2147789)CaDiCaL version: 2.1.3
% 13.93/2.95 % (2147789)Termination reason: Refutation not found, incomplete strategy
% 13.93/2.95 % (2147789)Time elapsed: 0.605 s
% 13.93/2.95 % (2147789)Peak memory usage: 127 MB
% 19.86/3.67 % (2147789)Instructions burned: 893 (million)
% 19.86/3.67 % (2147815)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2474271066:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 19.86/3.67 % (2147815)Refutation not found, incomplete strategy
% 19.86/3.67 % (2147815)------------------------------
% 19.86/3.67 % (2147815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147815)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147815)Termination reason: Refutation not found, incomplete strategy
% 19.86/3.67 % (2147815)Time elapsed: 0.0000 s
% 19.86/3.67 % (2147815)Peak memory usage: 88 MB
% 19.86/3.67 % (2147814)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2227996781:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 19.86/3.67 % (2147814)Refutation not found, incomplete strategy
% 19.86/3.67 % (2147814)------------------------------
% 19.86/3.67 % (2147814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147814)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147814)Termination reason: Refutation not found, incomplete strategy
% 19.86/3.67 % (2147814)Time elapsed: 0.001 s
% 19.86/3.67 % (2147814)Peak memory usage: 88 MB
% 19.86/3.67 % (2147815)------------------------------
% 19.86/3.67 % (2147815)------------------------------
% 19.86/3.67 % (2147812)------------------------------
% 19.86/3.67 % (2147812)------------------------------
% 19.86/3.67 % (2147789)------------------------------
% 19.86/3.67 % (2147789)------------------------------
% 19.86/3.67 % (2147819)lrs+10_1_sil=8000:sp=occurrence:random_seed=387579794:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 19.86/3.67 % (2147814)------------------------------
% 19.86/3.67 % (2147814)------------------------------
% 19.86/3.67 % (2147820)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3469124119:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 19.86/3.67 % (2147820)Refutation not found, incomplete strategy
% 19.86/3.67 % (2147820)------------------------------
% 19.86/3.67 % (2147820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147820)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147820)Termination reason: Refutation not found, incomplete strategy
% 19.86/3.67 % (2147820)Time elapsed: 0.001 s
% 19.86/3.67 % (2147820)Peak memory usage: 88 MB
% 19.86/3.67 % (2147821)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3050753714:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 19.86/3.67 % (2147823)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=963234496:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 19.86/3.67 % (2147823)Refutation not found, incomplete strategy
% 19.86/3.67 % (2147823)------------------------------
% 19.86/3.67 % (2147823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147823)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147823)Termination reason: Refutation not found, incomplete strategy
% 19.86/3.67 % (2147823)Time elapsed: 0.002 s
% 19.86/3.67 % (2147823)Peak memory usage: 88 MB
% 19.86/3.67 % (2147823)Instructions burned: 1 (million)
% 19.86/3.67 % (2147819)Instruction limit reached!
% 19.86/3.67 % (2147819)------------------------------
% 19.86/3.67 % (2147819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147819)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147819)Termination reason: Instruction limit
% 19.86/3.67 % (2147819)Termination phase: Saturation
% 19.86/3.67 % (2147819)Time elapsed: 0.319 s
% 19.86/3.67 % (2147819)Peak memory usage: 95 MB
% 19.86/3.67 % (2147819)Instructions burned: 907 (million)
% 19.86/3.67 % (2147820)------------------------------
% 19.86/3.67 % (2147820)------------------------------
% 19.86/3.67 % (2147827)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1652950504:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 19.86/3.67 % (2147823)------------------------------
% 19.86/3.67 % (2147823)------------------------------
% 19.86/3.67 % (2147828)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2734645757:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 19.86/3.67 % (2147830)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=108656404:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 19.86/3.67 % (2147827)Instruction limit reached!
% 19.86/3.67 % (2147827)------------------------------
% 19.86/3.67 % (2147827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147827)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147827)Termination reason: Instruction limit
% 19.86/3.67 % (2147827)Termination phase: Saturation
% 19.86/3.67 % (2147827)Time elapsed: 0.188 s
% 19.86/3.67 % (2147827)Peak memory usage: 94 MB
% 19.86/3.67 % (2147827)Instructions burned: 595 (million)
% 19.86/3.67 % (2147830)Instruction limit reached!
% 19.86/3.67 % (2147830)------------------------------
% 19.86/3.67 % (2147830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147830)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147830)Termination reason: Instruction limit
% 19.86/3.67 % (2147830)Termination phase: Saturation
% 19.86/3.67 % (2147830)Time elapsed: 0.083 s
% 19.86/3.67 % (2147830)Peak memory usage: 90 MB
% 19.86/3.67 % (2147830)Instructions burned: 126 (million)
% 19.86/3.67 % (2147833)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2853416736:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 19.86/3.67 % (2147833)Instruction limit reached!
% 19.86/3.67 % (2147833)------------------------------
% 19.86/3.67 % (2147833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147833)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147833)Termination reason: Instruction limit
% 19.86/3.67 % (2147833)Termination phase: Saturation
% 19.86/3.67 % (2147833)Time elapsed: 0.045 s
% 19.86/3.67 % (2147833)Peak memory usage: 90 MB
% 19.86/3.67 % (2147833)Instructions burned: 136 (million)
% 19.86/3.67 % (2147834)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=482545204:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 19.86/3.67 % (2147834)Refutation not found, incomplete strategy
% 19.86/3.67 % (2147834)------------------------------
% 19.86/3.67 % (2147834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147834)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147834)Termination reason: Refutation not found, incomplete strategy
% 19.86/3.67 % (2147834)Time elapsed: 0.001 s
% 19.86/3.67 % (2147834)Peak memory usage: 88 MB
% 19.86/3.67 % (2147836)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=619533205:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi)
% 19.86/3.67 % (2147836)Refutation not found, incomplete strategy
% 19.86/3.67 % (2147836)------------------------------
% 19.86/3.67 % (2147836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147836)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147836)Termination reason: Refutation not found, incomplete strategy
% 19.86/3.67 % (2147836)Time elapsed: 0.001 s
% 19.86/3.67 % (2147836)Peak memory usage: 88 MB
% 19.86/3.67 % (2147836)------------------------------
% 19.86/3.67 % (2147836)------------------------------
% 19.86/3.67 % (2147834)------------------------------
% 19.86/3.67 % (2147834)------------------------------
% 19.86/3.67 % (2147839)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=460532742:i=6060:aac=none:ins=25_2979 on theBenchmark for (2979ds/6060Mi)
% 19.86/3.67 % (2147809)Instruction limit reached!
% 19.86/3.67 % (2147809)------------------------------
% 19.86/3.67 % (2147809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147809)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147809)Termination reason: Instruction limit
% 19.86/3.67 % (2147809)Termination phase: Saturation
% 19.86/3.67 % (2147809)Time elapsed: 1.457 s
% 19.86/3.67 % (2147809)Peak memory usage: 144 MB
% 19.86/3.67 % (2147809)Instructions burned: 2351 (million)
% 19.86/3.67 % (2147840)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2596890443:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2979 on theBenchmark for (2979ds/150Mi)
% 19.86/3.67 % (2147842)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3311237546:i=14155:bd=all_2978 on theBenchmark for (2978ds/14155Mi)
% 19.86/3.67 % (2147840)Instruction limit reached!
% 19.86/3.67 % (2147840)------------------------------
% 19.86/3.67 % (2147840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147840)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147840)Termination reason: Instruction limit
% 19.86/3.67 % (2147840)Termination phase: Saturation
% 19.86/3.67 % (2147840)Time elapsed: 0.099 s
% 19.86/3.67 % (2147840)Peak memory usage: 91 MB
% 19.86/3.67 % (2147840)Instructions burned: 151 (million)
% 19.86/3.67 % (2147845)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2840955456:i=667:av=off:fsr=off_2976 on theBenchmark for (2976ds/667Mi)
% 19.86/3.67 % (2147845)Refutation not found, incomplete strategy
% 19.86/3.67 % (2147845)------------------------------
% 19.86/3.67 % (2147845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.86/3.67 % (2147845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.86/3.67 % (2147845)CaDiCaL version: 2.1.3
% 19.86/3.67 % (2147845)Termination reason: Refutation not found, incomplete strategy
% 19.86/3.67 % (2147845)Time elapsed: 0.001 s
% 19.86/3.67 % (2147845)Peak memory usage: 88 MB
% 19.86/3.67 % (2147788)First to succeed.
% 19.86/3.67 % (2147788)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2147782"
% 19.86/3.67 % (2147845)------------------------------
% 19.86/3.67 % (2147845)------------------------------
% 19.86/3.67 % (2147847)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3945285752:s2a=on:i=185:s2at=1.8:fdi=4_2973 on theBenchmark for (2973ds/185Mi)
% 19.86/3.67 % (2147788)Refutation found. Thanks to Tanya!
% 19.86/3.67 % SZS status Theorem for theBenchmark
% 19.86/3.67 % SZS output start Proof for theBenchmark
% See solution above
% 20.58/3.86 % (2147788)------------------------------
% 20.58/3.86 % (2147788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.58/3.86 % (2147788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.58/3.86 % (2147788)CaDiCaL version: 2.1.3
% 20.58/3.86 % (2147788)Termination reason: Refutation
% 20.58/3.86 % (2147788)Time elapsed: 2.412 s
% 20.58/3.86 % (2147788)Peak memory usage: 159 MB
% 20.58/3.86 % (2147788)Instructions burned: 3934 (million)
% 20.58/3.86 % (2147788)------------------------------
% 20.58/3.86 % (2147788)------------------------------
% 20.58/3.86 % (2147782)Success in time 2.829 s
% 20.58/3.86 % Vampire exiting
%------------------------------------------------------------------------------