%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : KLE120+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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 11:40:55 AM UTC 2026
% Result : Theorem 5.94s 1.35s
% Output : Refutation 5.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 27
% Syntax : Number of formulae : 219 ( 219 unt; 8 def)
% Number of atoms : 219 ( 218 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 8 ( 8 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 11 con; 0-2 aty)
% Number of variables : 154 ( 153 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_associativity) ).
fof(f3,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_identity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_idempotence) ).
fof(f5,axiom,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',multiplicative_left_identity) ).
fof(f8,axiom,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',right_distributivity) ).
fof(f9,axiom,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',left_distributivity) ).
fof(f11,axiom,
! [X0] : multiplication(zero,X0) = zero,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',left_annihilation) ).
fof(f13,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',domain1) ).
fof(f15,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',domain3) ).
fof(f16,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',domain4) ).
fof(f17,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',codomain1) ).
fof(f18,axiom,
! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',codomain2) ).
fof(f19,axiom,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',codomain3) ).
fof(f20,axiom,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',codomain4) ).
fof(f24,axiom,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+6.ax',backward_diamond) ).
fof(f27,conjecture,
! [X0] : addition(backward_diamond(one,domain(X0)),domain(X0)) = domain(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f28,negated_conjecture,
~ ! [X0] : addition(backward_diamond(one,domain(X0)),domain(X0)) = domain(X0),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f29,plain,
? [X0] : domain(X0) != addition(backward_diamond(one,domain(X0)),domain(X0)),
inference(ennf_transformation,[],[f28]) ).
fof(f30,plain,
domain(sK0) != addition(backward_diamond(one,domain(sK0)),domain(sK0)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f29]) ).
fof(f31,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f32,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f33,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f34,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f35,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f36,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f37,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f38,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f39,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f41,plain,
! [X0] : zero = multiplication(zero,X0),
inference(cnf_transformation,[],[f11]) ).
fof(f42,plain,
! [X0] : zero = multiplication(antidomain(X0),X0),
inference(cnf_transformation,[],[f13]) ).
fof(f44,plain,
! [X0] : one = addition(antidomain(antidomain(X0)),antidomain(X0)),
inference(cnf_transformation,[],[f15]) ).
fof(f45,plain,
! [X0] : antidomain(antidomain(X0)) = domain(X0),
inference(cnf_transformation,[],[f16]) ).
fof(f46,plain,
! [X0] : zero = multiplication(X0,coantidomain(X0)),
inference(cnf_transformation,[],[f17]) ).
fof(f47,plain,
! [X0,X1] : coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)) = addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))),
inference(cnf_transformation,[],[f18]) ).
fof(f48,plain,
! [X0] : one = addition(coantidomain(coantidomain(X0)),coantidomain(X0)),
inference(cnf_transformation,[],[f19]) ).
fof(f49,plain,
! [X0] : coantidomain(coantidomain(X0)) = codomain(X0),
inference(cnf_transformation,[],[f20]) ).
fof(f53,plain,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
inference(cnf_transformation,[],[f24]) ).
fof(f56,plain,
domain(sK0) != addition(backward_diamond(one,domain(sK0)),domain(sK0)),
inference(cnf_transformation,[],[f30]) ).
fof(f58,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f53,f49,f49]) ).
fof(f63,plain,
antidomain(antidomain(sK0)) != addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK0)))),one))),antidomain(antidomain(sK0))),
inference(definition_unfolding,[],[f56,f45,f58,f45,f45]) ).
fof(f64,definition,
sF1 = antidomain(sK0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f65,plain,
antidomain(sK0) = sF1,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF2 = antidomain(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f67,plain,
antidomain(sF1) = sF2,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF3 = coantidomain(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f69,plain,
coantidomain(sF2) = sF3,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF4 = coantidomain(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f71,plain,
coantidomain(sF3) = sF4,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF5 = multiplication(sF4,one),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f73,plain,
multiplication(sF4,one) = sF5,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF6 = coantidomain(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f75,plain,
coantidomain(sF5) = sF6,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF7 = coantidomain(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f77,plain,
coantidomain(sF6) = sF7,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF8 = addition(sF7,sF2),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f79,plain,
addition(sF7,sF2) = sF8,
inference(reorient_equations,[],[f78]) ).
fof(f80,plain,
sF2 != sF8,
inference(definition_folding,[],[f63,f79,f67,f65,f77,f75,f73,f71,f69,f67,f65,f67,f65]) ).
fof(f81,plain,
sF3 = coantidomain(antidomain(sF1)),
inference(forward_demodulation,[],[f69,f67]) ).
fof(f82,plain,
sF4 = sF5,
inference(forward_demodulation,[],[f73,f36]) ).
fof(f83,plain,
sF8 = addition(sF7,antidomain(sF1)),
inference(forward_demodulation,[],[f79,f67]) ).
fof(f84,plain,
sF6 = coantidomain(sF4),
inference(superposition,[],[f75,f82]) ).
fof(f85,plain,
zero = multiplication(sF1,sK0),
inference(superposition,[],[f42,f65]) ).
fof(f87,plain,
zero = antidomain(one),
inference(superposition,[],[f36,f42]) ).
fof(f90,plain,
zero = multiplication(sF3,sF4),
inference(superposition,[],[f46,f71]) ).
fof(f93,plain,
zero = multiplication(sF6,sF7),
inference(superposition,[],[f46,f77]) ).
fof(f95,plain,
zero = coantidomain(one),
inference(superposition,[],[f37,f46]) ).
fof(f101,plain,
! [X0] : addition(zero,X0) = X0,
inference(superposition,[],[f33,f31]) ).
fof(f102,plain,
one = addition(antidomain(sF1),sF1),
inference(superposition,[],[f44,f65]) ).
fof(f103,plain,
one = addition(antidomain(zero),zero),
inference(superposition,[],[f44,f87]) ).
fof(f108,plain,
one = antidomain(zero),
inference(forward_demodulation,[],[f103,f33]) ).
fof(f109,plain,
one = addition(sF1,antidomain(sF1)),
inference(forward_demodulation,[],[f102,f31]) ).
fof(f110,plain,
antidomain(zero) = addition(sF1,antidomain(sF1)),
inference(forward_demodulation,[],[f109,f108]) ).
fof(f113,plain,
! [X0] : multiplication(antidomain(zero),X0) = X0,
inference(superposition,[],[f37,f108]) ).
fof(f114,plain,
! [X0] : multiplication(X0,antidomain(zero)) = X0,
inference(superposition,[],[f36,f108]) ).
fof(f115,plain,
one = addition(coantidomain(zero),zero),
inference(superposition,[],[f48,f95]) ).
fof(f116,plain,
one = addition(coantidomain(sF3),sF3),
inference(superposition,[],[f48,f81]) ).
fof(f117,plain,
one = addition(coantidomain(sF4),sF4),
inference(superposition,[],[f48,f71]) ).
fof(f119,plain,
one = addition(coantidomain(sF6),sF6),
inference(superposition,[],[f48,f75]) ).
fof(f124,plain,
! [X0] : one = addition(coantidomain(X0),coantidomain(coantidomain(X0))),
inference(superposition,[],[f31,f48]) ).
fof(f125,plain,
! [X0] : antidomain(zero) = addition(coantidomain(X0),coantidomain(coantidomain(X0))),
inference(forward_demodulation,[],[f124,f108]) ).
fof(f130,plain,
one = addition(sF6,coantidomain(sF6)),
inference(forward_demodulation,[],[f119,f31]) ).
fof(f132,plain,
one = addition(sF4,coantidomain(sF4)),
inference(forward_demodulation,[],[f117,f31]) ).
fof(f133,plain,
one = addition(sF3,coantidomain(sF3)),
inference(forward_demodulation,[],[f116,f31]) ).
fof(f134,plain,
one = coantidomain(zero),
inference(forward_demodulation,[],[f115,f33]) ).
fof(f136,plain,
one = addition(sF6,sF7),
inference(forward_demodulation,[],[f130,f77]) ).
fof(f138,plain,
one = addition(sF4,sF6),
inference(forward_demodulation,[],[f132,f84]) ).
fof(f139,plain,
one = addition(sF3,sF4),
inference(forward_demodulation,[],[f133,f71]) ).
fof(f140,plain,
antidomain(zero) = coantidomain(zero),
inference(forward_demodulation,[],[f134,f108]) ).
fof(f141,plain,
antidomain(zero) = addition(sF6,sF7),
inference(forward_demodulation,[],[f136,f108]) ).
fof(f143,plain,
antidomain(zero) = addition(sF4,sF6),
inference(forward_demodulation,[],[f138,f108]) ).
fof(f144,plain,
antidomain(zero) = addition(sF3,sF4),
inference(forward_demodulation,[],[f139,f108]) ).
fof(f146,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f32,f34]) ).
fof(f152,plain,
! [X0] : addition(sF7,addition(antidomain(sF1),X0)) = addition(sF8,X0),
inference(superposition,[],[f32,f83]) ).
fof(f185,plain,
! [X0,X1] : zero = multiplication(X0,multiplication(X1,coantidomain(multiplication(X0,X1)))),
inference(superposition,[],[f46,f35]) ).
fof(f209,plain,
! [X0] : multiplication(sF6,addition(sF7,X0)) = addition(zero,multiplication(sF6,X0)),
inference(superposition,[],[f38,f93]) ).
fof(f212,plain,
! [X0,X1] : addition(multiplication(X0,X1),zero) = multiplication(X0,addition(X1,coantidomain(X0))),
inference(superposition,[],[f38,f46]) ).
fof(f216,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X1,X0)) = addition(multiplication(antidomain(X0),X1),zero),
inference(superposition,[],[f38,f42]) ).
fof(f217,plain,
! [X0] : multiplication(sF1,addition(X0,sK0)) = addition(multiplication(sF1,X0),zero),
inference(superposition,[],[f38,f85]) ).
fof(f227,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X2),multiplication(X0,X1)),
inference(superposition,[],[f31,f38]) ).
fof(f231,plain,
! [X0] : multiplication(sF1,X0) = multiplication(sF1,addition(X0,sK0)),
inference(forward_demodulation,[],[f217,f33]) ).
fof(f232,plain,
! [X0,X1] : multiplication(antidomain(X0),X1) = multiplication(antidomain(X0),addition(X1,X0)),
inference(forward_demodulation,[],[f216,f33]) ).
fof(f236,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(X0,addition(X1,coantidomain(X0))),
inference(forward_demodulation,[],[f212,f33]) ).
fof(f239,plain,
! [X0] : multiplication(sF6,X0) = multiplication(sF6,addition(sF7,X0)),
inference(forward_demodulation,[],[f209,f101]) ).
fof(f264,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X0)) = addition(zero,multiplication(X1,coantidomain(X0))),
inference(superposition,[],[f39,f46]) ).
fof(f275,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = addition(multiplication(X0,coantidomain(X1)),zero),
inference(superposition,[],[f39,f46]) ).
fof(f278,plain,
! [X0,X1] : multiplication(addition(X1,one),X0) = addition(multiplication(X1,X0),X0),
inference(superposition,[],[f39,f37]) ).
fof(f279,plain,
! [X0,X1] : addition(multiplication(X0,X1),zero) = multiplication(addition(X0,antidomain(X1)),X1),
inference(superposition,[],[f39,f42]) ).
fof(f292,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X1,X2),multiplication(X0,X2)),
inference(superposition,[],[f31,f39]) ).
fof(f299,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(addition(X0,antidomain(X1)),X1),
inference(forward_demodulation,[],[f279,f33]) ).
fof(f300,plain,
! [X0,X1] : addition(X0,multiplication(X1,X0)) = multiplication(addition(X1,one),X0),
inference(forward_demodulation,[],[f278,f31]) ).
fof(f302,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X1)) = multiplication(X0,coantidomain(X1)),
inference(forward_demodulation,[],[f275,f33]) ).
fof(f312,plain,
! [X0,X1] : multiplication(addition(X0,X1),coantidomain(X0)) = multiplication(X1,coantidomain(X0)),
inference(forward_demodulation,[],[f264,f101]) ).
fof(f315,plain,
! [X0,X1] : addition(X0,multiplication(X1,X0)) = multiplication(addition(X1,antidomain(zero)),X0),
inference(forward_demodulation,[],[f300,f108]) ).
fof(f382,plain,
! [X0] : coantidomain(multiplication(coantidomain(sF3),X0)) = addition(coantidomain(multiplication(antidomain(sF1),X0)),coantidomain(multiplication(coantidomain(sF3),X0))),
inference(superposition,[],[f47,f81]) ).
fof(f399,plain,
! [X0] : coantidomain(multiplication(sF4,X0)) = addition(coantidomain(multiplication(antidomain(sF1),X0)),coantidomain(multiplication(sF4,X0))),
inference(forward_demodulation,[],[f382,f71]) ).
fof(f416,plain,
! [X0] : coantidomain(multiplication(sF4,X0)) = addition(coantidomain(multiplication(sF4,X0)),coantidomain(multiplication(antidomain(sF1),X0))),
inference(forward_demodulation,[],[f399,f31]) ).
fof(f447,plain,
! [X0] : addition(antidomain(zero),X0) = addition(sF6,addition(sF7,X0)),
inference(superposition,[],[f32,f141]) ).
fof(f448,plain,
! [X0] : addition(antidomain(zero),X0) = addition(sF4,addition(sF6,X0)),
inference(superposition,[],[f32,f143]) ).
fof(f754,plain,
! [X0] : antidomain(zero) = addition(coantidomain(X0),antidomain(zero)),
inference(superposition,[],[f146,f125]) ).
fof(f755,plain,
antidomain(zero) = addition(sF1,antidomain(zero)),
inference(superposition,[],[f146,f110]) ).
fof(f759,plain,
sF8 = addition(sF7,sF8),
inference(superposition,[],[f146,f83]) ).
fof(f767,plain,
! [X0] : antidomain(zero) = addition(antidomain(zero),coantidomain(X0)),
inference(forward_demodulation,[],[f754,f31]) ).
fof(f774,plain,
! [X0] : antidomain(zero) = addition(sF6,addition(sF7,coantidomain(X0))),
inference(forward_demodulation,[],[f767,f447]) ).
fof(f906,plain,
! [X0] : multiplication(X0,one) = multiplication(X0,coantidomain(coantidomain(X0))),
inference(superposition,[],[f236,f48]) ).
fof(f949,plain,
! [X0] : multiplication(X0,coantidomain(coantidomain(X0))) = X0,
inference(forward_demodulation,[],[f906,f36]) ).
fof(f1045,plain,
! [X0] : multiplication(one,X0) = multiplication(antidomain(antidomain(X0)),X0),
inference(superposition,[],[f299,f44]) ).
fof(f1052,plain,
multiplication(sF7,sF1) = multiplication(sF8,sF1),
inference(superposition,[],[f299,f83]) ).
fof(f1086,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f1045,f37]) ).
fof(f1400,plain,
antidomain(sF1) = multiplication(antidomain(sF1),coantidomain(sF3)),
inference(superposition,[],[f949,f81]) ).
fof(f1402,plain,
sF3 = multiplication(sF3,coantidomain(sF4)),
inference(superposition,[],[f949,f71]) ).
fof(f1403,plain,
sF4 = multiplication(sF4,coantidomain(sF6)),
inference(superposition,[],[f949,f84]) ).
fof(f1437,plain,
sF4 = multiplication(sF4,sF7),
inference(forward_demodulation,[],[f1403,f77]) ).
fof(f1438,plain,
sF3 = multiplication(sF3,sF6),
inference(forward_demodulation,[],[f1402,f84]) ).
fof(f1440,plain,
antidomain(sF1) = multiplication(antidomain(sF1),sF4),
inference(forward_demodulation,[],[f1400,f71]) ).
fof(f1687,plain,
multiplication(antidomain(antidomain(sF1)),sF1) = multiplication(antidomain(antidomain(sF1)),antidomain(zero)),
inference(superposition,[],[f232,f110]) ).
fof(f1731,plain,
antidomain(antidomain(sF1)) = multiplication(antidomain(antidomain(sF1)),sF1),
inference(forward_demodulation,[],[f1687,f114]) ).
fof(f1749,plain,
sF1 = antidomain(antidomain(sF1)),
inference(forward_demodulation,[],[f1731,f1086]) ).
fof(f1865,plain,
multiplication(sF1,coantidomain(antidomain(sF1))) = multiplication(antidomain(zero),coantidomain(antidomain(sF1))),
inference(superposition,[],[f302,f110]) ).
fof(f1867,plain,
multiplication(sF3,coantidomain(sF4)) = multiplication(antidomain(zero),coantidomain(sF4)),
inference(superposition,[],[f302,f144]) ).
fof(f1869,plain,
multiplication(sF4,coantidomain(sF6)) = multiplication(antidomain(zero),coantidomain(sF6)),
inference(superposition,[],[f302,f143]) ).
fof(f1914,plain,
coantidomain(sF6) = multiplication(sF4,coantidomain(sF6)),
inference(forward_demodulation,[],[f1869,f113]) ).
fof(f1916,plain,
coantidomain(sF4) = multiplication(sF3,coantidomain(sF4)),
inference(forward_demodulation,[],[f1867,f113]) ).
fof(f1918,plain,
coantidomain(antidomain(sF1)) = multiplication(sF1,coantidomain(antidomain(sF1))),
inference(forward_demodulation,[],[f1865,f113]) ).
fof(f1937,plain,
sF7 = multiplication(sF4,sF7),
inference(forward_demodulation,[],[f1914,f77]) ).
fof(f1939,plain,
sF6 = multiplication(sF3,sF6),
inference(forward_demodulation,[],[f1916,f84]) ).
fof(f1941,plain,
sF3 = multiplication(sF1,sF3),
inference(forward_demodulation,[],[f1918,f81]) ).
fof(f1946,plain,
sF4 = sF7,
inference(forward_demodulation,[],[f1937,f1437]) ).
fof(f1947,plain,
sF3 = sF6,
inference(forward_demodulation,[],[f1939,f1438]) ).
fof(f1948,plain,
sF8 = addition(sF4,antidomain(sF1)),
inference(superposition,[],[f83,f1946]) ).
fof(f1975,plain,
multiplication(antidomain(sF1),coantidomain(sF1)) = multiplication(antidomain(zero),coantidomain(sF1)),
inference(superposition,[],[f312,f110]) ).
fof(f2017,plain,
coantidomain(sF1) = multiplication(antidomain(sF1),coantidomain(sF1)),
inference(forward_demodulation,[],[f1975,f113]) ).
fof(f3155,plain,
! [X0] : multiplication(antidomain(zero),X0) = addition(X0,multiplication(sF1,X0)),
inference(superposition,[],[f315,f755]) ).
fof(f3249,plain,
! [X0] : addition(X0,multiplication(sF1,X0)) = X0,
inference(forward_demodulation,[],[f3155,f113]) ).
fof(f4883,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = multiplication(addition(X1,X0),X2),
inference(superposition,[],[f39,f292]) ).
fof(f5440,plain,
multiplication(antidomain(antidomain(sF1)),sF8) = multiplication(antidomain(antidomain(sF1)),sF4),
inference(superposition,[],[f232,f1948]) ).
fof(f5446,plain,
multiplication(sF1,sF8) = multiplication(sF1,sF4),
inference(forward_demodulation,[],[f5440,f1749]) ).
fof(f5698,plain,
coantidomain(multiplication(sF4,sF1)) = addition(coantidomain(multiplication(sF4,sF1)),coantidomain(zero)),
inference(superposition,[],[f416,f42]) ).
fof(f5748,plain,
coantidomain(multiplication(sF4,sF1)) = addition(coantidomain(zero),coantidomain(multiplication(sF4,sF1))),
inference(forward_demodulation,[],[f5698,f31]) ).
fof(f5780,plain,
coantidomain(multiplication(sF4,sF1)) = addition(antidomain(zero),coantidomain(multiplication(sF4,sF1))),
inference(forward_demodulation,[],[f5748,f140]) ).
fof(f5805,plain,
coantidomain(multiplication(sF4,sF1)) = addition(sF6,addition(sF7,coantidomain(multiplication(sF4,sF1)))),
inference(forward_demodulation,[],[f5780,f447]) ).
fof(f5823,plain,
antidomain(zero) = coantidomain(multiplication(sF4,sF1)),
inference(forward_demodulation,[],[f5805,f774]) ).
fof(f6212,plain,
zero = multiplication(sF8,multiplication(sF1,coantidomain(multiplication(sF7,sF1)))),
inference(superposition,[],[f185,f1052]) ).
fof(f6227,plain,
zero = multiplication(sF8,multiplication(sF1,coantidomain(multiplication(sF4,sF1)))),
inference(forward_demodulation,[],[f6212,f1946]) ).
fof(f6239,plain,
zero = multiplication(sF8,multiplication(sF1,antidomain(zero))),
inference(forward_demodulation,[],[f6227,f5823]) ).
fof(f6248,plain,
zero = multiplication(sF8,sF1),
inference(forward_demodulation,[],[f6239,f114]) ).
fof(f6597,plain,
! [X0] : multiplication(zero,X0) = multiplication(sF8,multiplication(sF1,X0)),
inference(superposition,[],[f35,f6248]) ).
fof(f6625,plain,
! [X0] : zero = multiplication(sF8,multiplication(sF1,X0)),
inference(forward_demodulation,[],[f6597,f41]) ).
fof(f11373,plain,
! [X0] : multiplication(addition(X0,antidomain(sF1)),sF4) = addition(antidomain(sF1),multiplication(X0,sF4)),
inference(superposition,[],[f292,f1440]) ).
fof(f13961,plain,
sF8 = addition(sF7,addition(antidomain(sF1),multiplication(sF1,sF8))),
inference(superposition,[],[f152,f3249]) ).
fof(f13962,plain,
sF8 = addition(sF7,addition(antidomain(sF1),multiplication(sF1,sF4))),
inference(forward_demodulation,[],[f13961,f5446]) ).
fof(f13996,plain,
sF8 = addition(sF7,multiplication(addition(sF1,antidomain(sF1)),sF4)),
inference(forward_demodulation,[],[f13962,f11373]) ).
fof(f14021,plain,
sF8 = addition(sF7,multiplication(antidomain(zero),sF4)),
inference(forward_demodulation,[],[f13996,f110]) ).
fof(f14031,plain,
sF8 = addition(sF7,sF4),
inference(forward_demodulation,[],[f14021,f113]) ).
fof(f14040,plain,
sF8 = addition(sF4,sF7),
inference(forward_demodulation,[],[f14031,f31]) ).
fof(f14046,plain,
sF8 = addition(sF4,sF4),
inference(forward_demodulation,[],[f14040,f1946]) ).
fof(f14052,plain,
sF4 = sF8,
inference(forward_demodulation,[],[f14046,f34]) ).
fof(f14242,plain,
sF2 != sF4,
inference(superposition,[],[f80,f14052]) ).
fof(f14243,plain,
! [X0] : addition(sF7,addition(antidomain(sF1),X0)) = addition(sF4,X0),
inference(superposition,[],[f152,f14052]) ).
fof(f14259,plain,
! [X0] : addition(sF4,X0) = addition(sF4,addition(antidomain(sF1),X0)),
inference(forward_demodulation,[],[f14243,f1946]) ).
fof(f14260,plain,
antidomain(sF1) != sF4,
inference(forward_demodulation,[],[f14242,f67]) ).
fof(f14893,plain,
! [X0,X1] : multiplication(sF1,addition(X0,X1)) = multiplication(sF1,addition(X0,addition(X1,sK0))),
inference(superposition,[],[f231,f32]) ).
fof(f15078,plain,
multiplication(sF6,sF7) = multiplication(sF6,multiplication(sF1,sF7)),
inference(superposition,[],[f239,f3249]) ).
fof(f15145,plain,
multiplication(sF6,sF4) = multiplication(sF6,multiplication(sF1,sF4)),
inference(forward_demodulation,[],[f15078,f1946]) ).
fof(f15187,plain,
multiplication(sF3,sF4) = multiplication(sF3,multiplication(sF1,sF4)),
inference(forward_demodulation,[],[f15145,f1947]) ).
fof(f15210,plain,
zero = multiplication(sF3,multiplication(sF1,sF4)),
inference(forward_demodulation,[],[f15187,f90]) ).
fof(f16992,plain,
! [X0,X1] : addition(multiplication(X0,multiplication(sF1,X1)),zero) = multiplication(addition(sF8,X0),multiplication(sF1,X1)),
inference(superposition,[],[f292,f6625]) ).
fof(f16994,plain,
! [X0] : addition(multiplication(sF1,X0),zero) = multiplication(addition(sF8,antidomain(zero)),multiplication(sF1,X0)),
inference(superposition,[],[f315,f6625]) ).
fof(f17005,plain,
! [X0] : addition(multiplication(sF1,X0),zero) = multiplication(addition(antidomain(zero),sF8),multiplication(sF1,X0)),
inference(forward_demodulation,[],[f16994,f4883]) ).
fof(f17007,plain,
! [X0,X1] : addition(multiplication(X0,multiplication(sF1,X1)),zero) = multiplication(addition(sF7,addition(antidomain(sF1),X0)),multiplication(sF1,X1)),
inference(forward_demodulation,[],[f16992,f152]) ).
fof(f17037,plain,
! [X0] : addition(multiplication(sF1,X0),zero) = multiplication(addition(sF6,addition(sF7,sF8)),multiplication(sF1,X0)),
inference(forward_demodulation,[],[f17005,f447]) ).
fof(f17039,plain,
! [X0,X1] : addition(multiplication(X0,multiplication(sF1,X1)),zero) = multiplication(addition(sF4,addition(antidomain(sF1),X0)),multiplication(sF1,X1)),
inference(forward_demodulation,[],[f17007,f1946]) ).
fof(f17065,plain,
! [X0] : addition(multiplication(sF1,X0),zero) = multiplication(addition(sF6,sF8),multiplication(sF1,X0)),
inference(forward_demodulation,[],[f17037,f759]) ).
fof(f17067,plain,
! [X0,X1] : addition(multiplication(X0,multiplication(sF1,X1)),zero) = multiplication(addition(sF4,X0),multiplication(sF1,X1)),
inference(forward_demodulation,[],[f17039,f14259]) ).
fof(f17088,plain,
! [X0] : addition(multiplication(sF1,X0),zero) = multiplication(addition(sF6,sF4),multiplication(sF1,X0)),
inference(forward_demodulation,[],[f17065,f14052]) ).
fof(f17090,plain,
! [X0,X1] : multiplication(X0,multiplication(sF1,X1)) = multiplication(addition(sF4,X0),multiplication(sF1,X1)),
inference(forward_demodulation,[],[f17067,f33]) ).
fof(f17107,plain,
! [X0] : addition(multiplication(sF1,X0),zero) = multiplication(addition(sF4,sF6),multiplication(sF1,X0)),
inference(forward_demodulation,[],[f17088,f4883]) ).
fof(f17120,plain,
! [X0] : addition(multiplication(sF1,X0),zero) = multiplication(sF6,multiplication(sF1,X0)),
inference(forward_demodulation,[],[f17107,f17090]) ).
fof(f17131,plain,
! [X0] : addition(multiplication(sF1,X0),zero) = multiplication(sF3,multiplication(sF1,X0)),
inference(forward_demodulation,[],[f17120,f1947]) ).
fof(f17138,plain,
! [X0] : multiplication(sF1,X0) = multiplication(sF3,multiplication(sF1,X0)),
inference(forward_demodulation,[],[f17131,f33]) ).
fof(f19079,plain,
zero = multiplication(sF3,multiplication(multiplication(sF1,sF4),coantidomain(zero))),
inference(superposition,[],[f185,f15210]) ).
fof(f19111,plain,
zero = multiplication(sF3,multiplication(sF1,multiplication(sF4,coantidomain(zero)))),
inference(forward_demodulation,[],[f19079,f35]) ).
fof(f19135,plain,
zero = multiplication(sF1,multiplication(sF4,coantidomain(zero))),
inference(forward_demodulation,[],[f19111,f17138]) ).
fof(f19150,plain,
zero = multiplication(sF1,multiplication(sF4,antidomain(zero))),
inference(forward_demodulation,[],[f19135,f140]) ).
fof(f19162,plain,
zero = multiplication(sF1,sF4),
inference(forward_demodulation,[],[f19150,f114]) ).
fof(f19259,plain,
! [X0] : addition(multiplication(sF1,X0),zero) = multiplication(sF1,addition(sF4,X0)),
inference(superposition,[],[f227,f19162]) ).
fof(f19286,plain,
! [X0] : multiplication(sF1,X0) = multiplication(sF1,addition(sF4,X0)),
inference(forward_demodulation,[],[f19259,f33]) ).
fof(f20891,plain,
multiplication(sF1,antidomain(zero)) = multiplication(sF1,addition(sF4,addition(sF6,sK0))),
inference(superposition,[],[f231,f448]) ).
fof(f20902,plain,
multiplication(sF1,antidomain(zero)) = multiplication(sF1,addition(sF4,sF6)),
inference(forward_demodulation,[],[f20891,f14893]) ).
fof(f20996,plain,
multiplication(sF1,antidomain(zero)) = multiplication(sF1,sF6),
inference(forward_demodulation,[],[f20902,f19286]) ).
fof(f21077,plain,
multiplication(sF1,sF3) = multiplication(sF1,antidomain(zero)),
inference(forward_demodulation,[],[f20996,f1947]) ).
fof(f21124,plain,
sF1 = multiplication(sF1,sF3),
inference(forward_demodulation,[],[f21077,f114]) ).
fof(f21208,plain,
sF1 = sF3,
inference(superposition,[],[f1941,f21124]) ).
fof(f21537,plain,
sF4 = coantidomain(sF1),
inference(superposition,[],[f71,f21208]) ).
fof(f21853,plain,
sF4 = multiplication(antidomain(sF1),sF4),
inference(superposition,[],[f2017,f21537]) ).
fof(f22783,plain,
antidomain(sF1) = sF4,
inference(superposition,[],[f1440,f21853]) ).
fof(f22829,plain,
$false,
inference(forward_subsumption_resolution,[],[f22783,f14260]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE120+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.37 % Computer : n001.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 13:17:16 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.94/1.35 % (3563282)Will run a generic schedule for satisfiability detection.
% 5.94/1.35 % (3563287)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=858103711_2999 on theBenchmark for (2999ds/0Mi)
% 5.94/1.35 % TRYING [1]
% 5.94/1.35 % TRYING [2]
% 5.94/1.35 % TRYING [3]
% 5.94/1.35 % (3563288)% WARNING: option uhcvi not known.
% 5.94/1.35 % TRYING [4]
% 5.94/1.35 % (3563288)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3714681219:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.94/1.35 % (3563291)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3987608242:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.94/1.35 % (3563289)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1471489278:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.94/1.35 % (3563290)dis+10_1_sil=32000:sp=arity:random_seed=1292014924:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.94/1.35 % (3563292)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1072603192:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.94/1.35 % (3563293)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=47873376:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.94/1.35 % TRYING [5]
% 5.94/1.35 % TRYING [6]
% 5.94/1.35 % (3563290)Instruction limit reached!
% 5.94/1.35 % (3563290)------------------------------
% 5.94/1.35 % (3563290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563290)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563290)Termination reason: Instruction limit
% 5.94/1.35 % (3563290)Termination phase: Saturation
% 5.94/1.35 % (3563290)Time elapsed: 0.060 s
% 5.94/1.35 % (3563290)Peak memory usage: 12 MB
% 5.94/1.35 % (3563290)Instructions burned: 104 (million)
% 5.94/1.35 % (3563291)Instruction limit reached!
% 5.94/1.35 % (3563291)------------------------------
% 5.94/1.35 % (3563291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563291)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563291)Termination reason: Instruction limit
% 5.94/1.35 % (3563291)Termination phase: Saturation
% 5.94/1.35 % (3563291)Time elapsed: 0.069 s
% 5.94/1.35 % (3563291)Peak memory usage: 13 MB
% 5.94/1.35 % (3563291)Instructions burned: 116 (million)
% 5.94/1.35 % (3563292)Instruction limit reached!
% 5.94/1.35 % (3563292)------------------------------
% 5.94/1.35 % (3563292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563292)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563292)Termination reason: Instruction limit
% 5.94/1.35 % (3563292)Termination phase: Saturation
% 5.94/1.35 % (3563292)Time elapsed: 0.077 s
% 5.94/1.35 % (3563292)Peak memory usage: 13 MB
% 5.94/1.35 % (3563292)Instructions burned: 137 (million)
% 5.94/1.35 % (3563301)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=952165668:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.94/1.35 % TRYING [1]
% 5.94/1.35 % TRYING [2]
% 5.94/1.35 % TRYING [3]
% 5.94/1.35 % (3563302)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1651083798:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.94/1.35 % TRYING [4]
% 5.94/1.35 % (3563293)Instruction limit reached!
% 5.94/1.35 % (3563293)------------------------------
% 5.94/1.35 % (3563293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563293)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563293)Termination reason: Instruction limit
% 5.94/1.35 % (3563293)Termination phase: Saturation
% 5.94/1.35 % (3563293)Time elapsed: 0.094 s
% 5.94/1.35 % (3563293)Peak memory usage: 13 MB
% 5.94/1.35 % (3563293)Instructions burned: 160 (million)
% 5.94/1.35 % (3563303)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=461322909:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.94/1.35 % (3563306)ott-21_1_sil=16000:fs=off:random_seed=2356100547:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.94/1.35 % TRYING [5]
% 5.94/1.35 % TRYING [7]
% 5.94/1.35 % (3563302)Instruction limit reached!
% 5.94/1.35 % (3563302)------------------------------
% 5.94/1.35 % (3563302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563302)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563302)Termination reason: Instruction limit
% 5.94/1.35 % (3563302)Termination phase: Saturation
% 5.94/1.35 % (3563302)Time elapsed: 0.085 s
% 5.94/1.35 % (3563302)Peak memory usage: 13 MB
% 5.94/1.35 % (3563302)Instructions burned: 132 (million)
% 5.94/1.35 % TRYING [6]
% 5.94/1.35 % (3563309)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4155243357:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 5.94/1.35 % (3563306)Instruction limit reached!
% 5.94/1.35 % (3563306)------------------------------
% 5.94/1.35 % (3563306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563306)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563306)Termination reason: Instruction limit
% 5.94/1.35 % (3563306)Termination phase: Saturation
% 5.94/1.35 % (3563306)Time elapsed: 0.079 s
% 5.94/1.35 % (3563306)Peak memory usage: 12 MB
% 5.94/1.35 % (3563306)Instructions burned: 181 (million)
% 5.94/1.35 % (3563311)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1735805052:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.94/1.35 % TRYING [1]
% 5.94/1.35 % TRYING [2]
% 5.94/1.35 % TRYING [3]
% 5.94/1.35 % TRYING [4]
% 5.94/1.35 % TRYING [5]
% 5.94/1.35 % TRYING [8]
% 5.94/1.35 % (3563301)Instruction limit reached!
% 5.94/1.35 % (3563301)------------------------------
% 5.94/1.35 % (3563301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563301)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563301)Termination reason: Instruction limit
% 5.94/1.35 % (3563301)Termination phase: Finite model building constraint generation
% 5.94/1.35 % (3563301)Time elapsed: 0.311 s
% 5.94/1.35 % (3563301)Peak memory usage: 35 MB
% 5.94/1.35 % (3563301)Instructions burned: 715 (million)
% 5.94/1.35 % (3563313)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2651701745:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 5.94/1.35 % (3563303)Instruction limit reached!
% 5.94/1.35 % (3563303)------------------------------
% 5.94/1.35 % (3563303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563303)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563303)Termination reason: Instruction limit
% 5.94/1.35 % (3563303)Termination phase: Saturation
% 5.94/1.35 % (3563303)Time elapsed: 0.347 s
% 5.94/1.35 % (3563303)Peak memory usage: 19 MB
% 5.94/1.35 % (3563303)Instructions burned: 687 (million)
% 5.94/1.35 % (3563309)Instruction limit reached!
% 5.94/1.35 % (3563309)------------------------------
% 5.94/1.35 % (3563309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563309)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563309)Termination reason: Instruction limit
% 5.94/1.35 % (3563309)Termination phase: Saturation
% 5.94/1.35 % (3563309)Time elapsed: 0.257 s
% 5.94/1.35 % (3563309)Peak memory usage: 16 MB
% 5.94/1.35 % (3563309)Instructions burned: 478 (million)
% 5.94/1.35 % TRYING [6]
% 5.94/1.35 % (3563315)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=459191357:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 5.94/1.35 % (3563316)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=4112756055:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 5.94/1.35 % (3563311)Instruction limit reached!
% 5.94/1.35 % (3563311)------------------------------
% 5.94/1.35 % (3563311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563311)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563311)Termination reason: Instruction limit
% 5.94/1.35 % (3563311)Termination phase: Finite model building SAT solving
% 5.94/1.35 % (3563311)Time elapsed: 0.350 s
% 5.94/1.35 % (3563311)Peak memory usage: 27 MB
% 5.94/1.35 % (3563311)Instructions burned: 866 (million)
% 5.94/1.35 % (3563319)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=732491400:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 5.94/1.35 % TRYING [14]
% 5.94/1.35 % (3563315)Instruction limit reached!
% 5.94/1.35 % (3563315)------------------------------
% 5.94/1.35 % (3563315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563315)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563315)Termination reason: Instruction limit
% 5.94/1.35 % (3563315)Termination phase: Finite model building constraint generation
% 5.94/1.35 % (3563315)Time elapsed: 0.336 s
% 5.94/1.35 % (3563315)Peak memory usage: 81 MB
% 5.94/1.35 % (3563315)Instructions burned: 890 (million)
% 5.94/1.35 % (3563321)fmb+10_1_sil=64000:random_seed=2704750965:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 5.94/1.35 % TRYING [1]
% 5.94/1.35 % TRYING [2]
% 5.94/1.35 % TRYING [3]
% 5.94/1.35 % TRYING [4]
% 5.94/1.35 % (3563316)Instruction limit reached!
% 5.94/1.35 % (3563316)------------------------------
% 5.94/1.35 % (3563316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.35 % (3563316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.35 % (3563316)CaDiCaL version: 2.1.3
% 5.94/1.35 % (3563316)Termination reason: Instruction limit
% 5.94/1.35 % (3563316)Termination phase: Saturation
% 5.94/1.35 % (3563316)Time elapsed: 0.401 s
% 5.94/1.35 % (3563316)Peak memory usage: 18 MB
% 5.94/1.35 % (3563316)Instructions burned: 692 (million)
% 5.94/1.35 % (3563313) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3563282-3563313"...
% 5.94/1.35 % (3563313)...printing done.
% 5.94/1.35 % (3563313)Refutation found. Thanks to Tanya!
% 5.94/1.35 % SZS status Theorem for theBenchmark
% 5.94/1.35 % SZS output start Proof for theBenchmark
% See solution above
% 5.94/1.36 % (3563313)------------------------------
% 5.94/1.36 % (3563313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.94/1.36 % (3563313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.94/1.36 % (3563313)CaDiCaL version: 2.1.3
% 5.94/1.36 % (3563313)Termination reason: Refutation
% 5.94/1.36 % (3563313)Time elapsed: 0.473 s
% 5.94/1.36 % (3563313)Peak memory usage: 20 MB
% 5.94/1.36 % (3563313)Instructions burned: 827 (million)
% 5.94/1.36 % (3563282)Success in time 0.933 s
% 5.94/1.36 % Vampire exiting
%------------------------------------------------------------------------------