%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : KLE098+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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:52 AM UTC 2026
% Result : Theorem 28.33s 5.30s
% Output : Refutation 28.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 30
% Syntax : Number of formulae : 210 ( 206 unt; 13 def)
% Number of atoms : 214 ( 213 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 10 ( 6 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 18 con; 0-2 aty)
% Number of variables : 174 ( 171 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/KLE001+0.ax',additive_associativity) ).
fof(f3,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',additive_identity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/KLE001+0.ax',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/KLE001+0.ax',left_distributivity) ).
fof(f10,axiom,
! [X0] : multiplication(X0,zero) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',right_annihilation) ).
fof(f11,axiom,
! [X0] : multiplication(zero,X0) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',left_annihilation) ).
fof(f13,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',domain1) ).
fof(f15,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',domain3) ).
fof(f16,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',domain4) ).
fof(f17,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',codomain1) ).
fof(f23,axiom,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+6.ax',forward_diamond) ).
fof(f27,conjecture,
! [X0,X1,X2] :
( addition(forward_diamond(X0,domain(X1)),domain(X2)) = domain(X2)
=> addition(multiplication(X0,domain(X1)),multiplication(domain(X2),X0)) = multiplication(domain(X2),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f28,negated_conjecture,
~ ! [X0,X1,X2] :
( addition(forward_diamond(X0,domain(X1)),domain(X2)) = domain(X2)
=> addition(multiplication(X0,domain(X1)),multiplication(domain(X2),X0)) = multiplication(domain(X2),X0) ),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f29,plain,
? [X0,X1,X2] :
( multiplication(domain(X2),X0) != addition(multiplication(X0,domain(X1)),multiplication(domain(X2),X0))
& addition(forward_diamond(X0,domain(X1)),domain(X2)) = domain(X2) ),
inference(ennf_transformation,[],[f28]) ).
fof(f30,plain,
( multiplication(domain(sK2),sK0) != addition(multiplication(sK0,domain(sK1)),multiplication(domain(sK2),sK0))
& domain(sK2) = addition(forward_diamond(sK0,domain(sK1)),domain(sK2)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[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(f40,plain,
! [X0] : zero = multiplication(X0,zero),
inference(cnf_transformation,[],[f10]) ).
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(f52,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(cnf_transformation,[],[f23]) ).
fof(f56,plain,
domain(sK2) = addition(forward_diamond(sK0,domain(sK1)),domain(sK2)),
inference(cnf_transformation,[],[f30]) ).
fof(f57,plain,
multiplication(domain(sK2),sK0) != addition(multiplication(sK0,domain(sK1)),multiplication(domain(sK2),sK0)),
inference(cnf_transformation,[],[f30]) ).
fof(f62,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f52,f45,f45]) ).
fof(f64,plain,
multiplication(antidomain(antidomain(sK2)),sK0) != addition(multiplication(sK0,antidomain(antidomain(sK1))),multiplication(antidomain(antidomain(sK2)),sK0)),
inference(definition_unfolding,[],[f57,f45,f45,f45]) ).
fof(f65,plain,
antidomain(antidomain(sK2)) = addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(sK2))),
inference(definition_unfolding,[],[f56,f45,f62,f45,f45]) ).
fof(f66,definition,
sF3 = antidomain(sK2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f67,plain,
antidomain(sK2) = sF3,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF4 = antidomain(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f69,plain,
antidomain(sF3) = sF4,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF5 = multiplication(sF4,sK0),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f71,plain,
multiplication(sF4,sK0) = sF5,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF6 = antidomain(sK1),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f73,plain,
antidomain(sK1) = sF6,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF7 = antidomain(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f75,plain,
antidomain(sF6) = sF7,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF8 = multiplication(sK0,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f77,plain,
multiplication(sK0,sF7) = sF8,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF9 = addition(sF8,sF5),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f79,plain,
addition(sF8,sF5) = sF9,
inference(reorient_equations,[],[f78]) ).
fof(f80,plain,
sF5 != sF9,
inference(definition_folding,[],[f64,f79,f71,f69,f67,f77,f75,f73,f71,f69,f67]) ).
fof(f81,definition,
sF10 = antidomain(sF7),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f82,plain,
antidomain(sF7) = sF10,
inference(reorient_equations,[],[f81]) ).
fof(f83,definition,
sF11 = antidomain(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f84,plain,
antidomain(sF10) = sF11,
inference(reorient_equations,[],[f83]) ).
fof(f85,definition,
sF12 = multiplication(sK0,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f86,plain,
multiplication(sK0,sF11) = sF12,
inference(reorient_equations,[],[f85]) ).
fof(f87,definition,
sF13 = antidomain(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f88,plain,
antidomain(sF12) = sF13,
inference(reorient_equations,[],[f87]) ).
fof(f89,definition,
sF14 = antidomain(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f90,plain,
antidomain(sF13) = sF14,
inference(reorient_equations,[],[f89]) ).
fof(f91,definition,
sF15 = addition(sF14,sF4),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f92,plain,
addition(sF14,sF4) = sF15,
inference(reorient_equations,[],[f91]) ).
fof(f93,plain,
sF4 = sF15,
inference(definition_folding,[],[f65,f92,f69,f67,f90,f88,f86,f84,f82,f75,f73,f69,f67]) ).
fof(f94,plain,
sF9 = addition(sF5,sF8),
inference(forward_demodulation,[],[f79,f31]) ).
fof(f95,plain,
sF4 = addition(sF14,sF4),
inference(forward_demodulation,[],[f92,f93]) ).
fof(f96,plain,
sF4 = addition(sF4,sF14),
inference(forward_demodulation,[],[f95,f31]) ).
fof(f101,plain,
zero = multiplication(sF10,sF7),
inference(superposition,[],[f42,f82]) ).
fof(f103,plain,
zero = multiplication(sF13,sF12),
inference(superposition,[],[f42,f88]) ).
fof(f114,plain,
! [X0] : addition(zero,X0) = X0,
inference(superposition,[],[f33,f31]) ).
fof(f116,plain,
one = addition(antidomain(sF6),sF6),
inference(superposition,[],[f44,f73]) ).
fof(f117,plain,
one = addition(antidomain(sF3),sF3),
inference(superposition,[],[f44,f67]) ).
fof(f119,plain,
one = addition(antidomain(sF7),sF7),
inference(superposition,[],[f44,f75]) ).
fof(f120,plain,
one = addition(antidomain(sF10),sF10),
inference(superposition,[],[f44,f82]) ).
fof(f122,plain,
one = addition(antidomain(sF13),sF13),
inference(superposition,[],[f44,f88]) ).
fof(f127,plain,
! [X0] : one = addition(antidomain(X0),antidomain(antidomain(X0))),
inference(superposition,[],[f31,f44]) ).
fof(f129,plain,
one = addition(sF13,antidomain(sF13)),
inference(forward_demodulation,[],[f122,f31]) ).
fof(f131,plain,
one = addition(sF10,antidomain(sF10)),
inference(forward_demodulation,[],[f120,f31]) ).
fof(f132,plain,
one = addition(sF7,antidomain(sF7)),
inference(forward_demodulation,[],[f119,f31]) ).
fof(f134,plain,
one = addition(sF3,antidomain(sF3)),
inference(forward_demodulation,[],[f117,f31]) ).
fof(f135,plain,
one = addition(sF6,antidomain(sF6)),
inference(forward_demodulation,[],[f116,f31]) ).
fof(f137,plain,
one = addition(sF13,sF14),
inference(forward_demodulation,[],[f129,f90]) ).
fof(f138,plain,
one = addition(sF10,sF11),
inference(forward_demodulation,[],[f131,f84]) ).
fof(f139,plain,
one = addition(sF7,sF10),
inference(forward_demodulation,[],[f132,f82]) ).
fof(f140,plain,
one = addition(sF3,sF4),
inference(forward_demodulation,[],[f134,f69]) ).
fof(f141,plain,
one = addition(sF6,sF7),
inference(forward_demodulation,[],[f135,f75]) ).
fof(f142,plain,
one = addition(sF4,sF3),
inference(forward_demodulation,[],[f140,f31]) ).
fof(f143,plain,
one = addition(sF7,sF6),
inference(forward_demodulation,[],[f141,f31]) ).
fof(f159,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f32,f34]) ).
fof(f161,plain,
! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X1,addition(X0,X2)),
inference(superposition,[],[f32,f31]) ).
fof(f165,plain,
! [X0] : addition(sF4,addition(sF14,X0)) = addition(sF4,X0),
inference(superposition,[],[f32,f96]) ).
fof(f174,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(superposition,[],[f31,f32]) ).
fof(f181,plain,
! [X0] : addition(sF4,X0) = addition(sF4,addition(X0,sF14)),
inference(superposition,[],[f165,f31]) ).
fof(f192,plain,
! [X0,X1] : multiplication(zero,X1) = multiplication(antidomain(X0),multiplication(X0,X1)),
inference(superposition,[],[f35,f42]) ).
fof(f194,plain,
! [X0] : multiplication(sK0,multiplication(sF11,X0)) = multiplication(sF12,X0),
inference(superposition,[],[f35,f86]) ).
fof(f206,plain,
! [X0,X1] : zero = multiplication(antidomain(X0),multiplication(X0,X1)),
inference(forward_demodulation,[],[f192,f41]) ).
fof(f214,plain,
! [X0,X1] : addition(sF4,addition(X0,X1)) = addition(sF4,addition(X0,addition(X1,sF14))),
inference(superposition,[],[f181,f32]) ).
fof(f215,plain,
! [X0,X1] : addition(addition(sF4,X0),X1) = addition(sF4,addition(addition(X0,sF14),X1)),
inference(superposition,[],[f32,f181]) ).
fof(f216,plain,
! [X0,X1] : addition(addition(sF4,X0),X1) = addition(sF4,addition(X0,addition(sF14,X1))),
inference(forward_demodulation,[],[f215,f32]) ).
fof(f217,plain,
! [X0,X1] : addition(sF4,addition(X0,X1)) = addition(sF4,addition(X0,addition(sF14,X1))),
inference(forward_demodulation,[],[f216,f32]) ).
fof(f218,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(superposition,[],[f38,f36]) ).
fof(f220,plain,
! [X0,X1] : addition(zero,multiplication(X0,X1)) = multiplication(X0,addition(coantidomain(X0),X1)),
inference(superposition,[],[f38,f46]) ).
fof(f227,plain,
! [X0] : multiplication(sF4,addition(sK0,X0)) = addition(sF5,multiplication(sF4,X0)),
inference(superposition,[],[f38,f71]) ).
fof(f235,plain,
! [X0,X1] : multiplication(antidomain(X0),addition(X1,X0)) = addition(multiplication(antidomain(X0),X1),zero),
inference(superposition,[],[f38,f42]) ).
fof(f237,plain,
! [X0] : multiplication(sK0,addition(X0,sF11)) = addition(multiplication(sK0,X0),sF12),
inference(superposition,[],[f38,f86]) ).
fof(f249,plain,
! [X0] : addition(sF12,multiplication(sK0,X0)) = multiplication(sK0,addition(X0,sF11)),
inference(forward_demodulation,[],[f237,f31]) ).
fof(f251,plain,
! [X0,X1] : multiplication(antidomain(X0),X1) = multiplication(antidomain(X0),addition(X1,X0)),
inference(forward_demodulation,[],[f235,f33]) ).
fof(f263,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(X0,addition(coantidomain(X0),X1)),
inference(forward_demodulation,[],[f220,f114]) ).
fof(f276,plain,
! [X0,X1] : addition(sF4,addition(addition(X0,sF14),X1)) = addition(sF4,addition(X1,X0)),
inference(superposition,[],[f214,f31]) ).
fof(f285,plain,
! [X0,X1] : addition(sF4,addition(X0,addition(sF14,X1))) = addition(sF4,addition(X1,X0)),
inference(forward_demodulation,[],[f276,f32]) ).
fof(f308,plain,
! [X2,X3,X0,X1] : multiplication(addition(X3,multiplication(X0,X1)),X2) = addition(multiplication(X3,X2),multiplication(X0,multiplication(X1,X2))),
inference(superposition,[],[f39,f35]) ).
fof(f310,plain,
! [X0,X1] : addition(multiplication(X0,X1),zero) = multiplication(addition(X0,antidomain(X1)),X1),
inference(superposition,[],[f39,f42]) ).
fof(f323,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X1,X2),multiplication(X0,X2)),
inference(superposition,[],[f31,f39]) ).
fof(f330,plain,
! [X0,X1] : multiplication(X0,X1) = multiplication(addition(X0,antidomain(X1)),X1),
inference(forward_demodulation,[],[f310,f33]) ).
fof(f349,plain,
! [X0,X1] : addition(sF4,addition(addition(sF14,X0),X1)) = addition(sF4,addition(X1,X0)),
inference(superposition,[],[f217,f31]) ).
fof(f356,plain,
! [X0,X1] : addition(sF4,addition(sF14,addition(X0,X1))) = addition(sF4,addition(X1,X0)),
inference(forward_demodulation,[],[f349,f32]) ).
fof(f361,plain,
! [X0,X1] : addition(sF4,addition(X0,X1)) = addition(sF4,addition(X1,X0)),
inference(forward_demodulation,[],[f356,f165]) ).
fof(f530,plain,
! [X0] : addition(sF4,addition(X0,sF14)) = addition(sF4,addition(zero,X0)),
inference(superposition,[],[f285,f33]) ).
fof(f570,plain,
! [X0] : addition(sF4,addition(X0,sF14)) = addition(zero,addition(X0,sF4)),
inference(forward_demodulation,[],[f530,f174]) ).
fof(f575,plain,
! [X0] : addition(sF4,addition(X0,sF14)) = addition(X0,sF4),
inference(forward_demodulation,[],[f570,f114]) ).
fof(f606,plain,
! [X0] : addition(sF4,addition(sF14,X0)) = addition(X0,sF4),
inference(superposition,[],[f361,f575]) ).
fof(f648,plain,
! [X0,X1] : addition(sF4,addition(addition(sF14,X0),X1)) = addition(addition(X0,sF4),X1),
inference(superposition,[],[f32,f606]) ).
fof(f649,plain,
! [X0,X1] : addition(sF4,addition(addition(sF14,X0),X1)) = addition(X0,addition(sF4,X1)),
inference(forward_demodulation,[],[f648,f32]) ).
fof(f655,plain,
! [X0,X1] : addition(sF4,addition(sF14,addition(X0,X1))) = addition(X0,addition(sF4,X1)),
inference(forward_demodulation,[],[f649,f32]) ).
fof(f660,plain,
! [X0,X1] : addition(sF4,addition(X0,X1)) = addition(X0,addition(sF4,X1)),
inference(forward_demodulation,[],[f655,f165]) ).
fof(f677,plain,
! [X0] : addition(sF4,X0) = addition(X0,addition(sF4,X0)),
inference(superposition,[],[f660,f34]) ).
fof(f763,plain,
! [X0] : multiplication(addition(X0,sF10),sF7) = addition(multiplication(X0,sF7),zero),
inference(superposition,[],[f39,f101]) ).
fof(f764,plain,
! [X0] : multiplication(addition(sF10,X0),sF7) = addition(zero,multiplication(X0,sF7)),
inference(superposition,[],[f39,f101]) ).
fof(f769,plain,
! [X0] : multiplication(X0,sF7) = multiplication(addition(sF10,X0),sF7),
inference(forward_demodulation,[],[f764,f114]) ).
fof(f770,plain,
! [X0] : multiplication(X0,sF7) = multiplication(addition(X0,sF10),sF7),
inference(forward_demodulation,[],[f763,f33]) ).
fof(f888,plain,
! [X0] : multiplication(addition(X0,sF13),sF12) = addition(multiplication(X0,sF12),zero),
inference(superposition,[],[f39,f103]) ).
fof(f895,plain,
! [X0] : multiplication(X0,sF12) = multiplication(addition(X0,sF13),sF12),
inference(forward_demodulation,[],[f888,f33]) ).
fof(f1159,plain,
addition(sF4,one) = addition(sF4,sF13),
inference(superposition,[],[f181,f137]) ).
fof(f1161,plain,
addition(one,sF4) = addition(sF4,sF13),
inference(forward_demodulation,[],[f1159,f31]) ).
fof(f1171,plain,
! [X0] : addition(sF4,addition(sF13,X0)) = addition(addition(one,sF4),X0),
inference(superposition,[],[f32,f1161]) ).
fof(f1172,plain,
! [X0] : addition(sF4,addition(sF13,X0)) = addition(one,addition(sF4,X0)),
inference(forward_demodulation,[],[f1171,f32]) ).
fof(f1310,plain,
one = addition(sF3,one),
inference(superposition,[],[f677,f142]) ).
fof(f1311,plain,
! [X0] : addition(X0,one) = addition(sF4,addition(X0,sF3)),
inference(superposition,[],[f660,f142]) ).
fof(f1313,plain,
one = addition(one,sF3),
inference(forward_demodulation,[],[f1310,f31]) ).
fof(f1315,plain,
addition(sF4,one) = addition(one,addition(sF4,sF3)),
inference(superposition,[],[f660,f1313]) ).
fof(f1316,plain,
addition(one,one) = addition(sF4,one),
inference(forward_demodulation,[],[f1315,f142]) ).
fof(f1317,plain,
addition(one,one) = addition(one,sF4),
inference(forward_demodulation,[],[f1316,f31]) ).
fof(f1318,plain,
one = addition(one,sF4),
inference(forward_demodulation,[],[f1317,f34]) ).
fof(f1322,plain,
! [X0] : addition(one,X0) = addition(one,addition(sF4,X0)),
inference(superposition,[],[f32,f1318]) ).
fof(f1401,plain,
addition(sF4,sF3) = addition(sF14,one),
inference(superposition,[],[f165,f1311]) ).
fof(f1405,plain,
addition(sF13,one) = addition(one,addition(sF4,sF3)),
inference(superposition,[],[f1172,f1311]) ).
fof(f1415,plain,
addition(sF13,one) = addition(one,sF3),
inference(forward_demodulation,[],[f1405,f1322]) ).
fof(f1416,plain,
addition(sF4,sF3) = addition(one,sF14),
inference(forward_demodulation,[],[f1401,f31]) ).
fof(f1427,plain,
one = addition(sF13,one),
inference(forward_demodulation,[],[f1415,f1313]) ).
fof(f1428,plain,
one = addition(one,sF14),
inference(forward_demodulation,[],[f1416,f142]) ).
fof(f1436,plain,
one = addition(one,sF13),
inference(forward_demodulation,[],[f1427,f31]) ).
fof(f1484,plain,
! [X2,X0,X1] : addition(multiplication(antidomain(X0),X1),zero) = multiplication(antidomain(X0),addition(X1,multiplication(X0,X2))),
inference(superposition,[],[f38,f206]) ).
fof(f1493,plain,
! [X2,X0,X1] : multiplication(antidomain(X0),X1) = multiplication(antidomain(X0),addition(X1,multiplication(X0,X2))),
inference(forward_demodulation,[],[f1484,f33]) ).
fof(f1500,plain,
! [X0] : addition(one,X0) = addition(one,addition(sF13,X0)),
inference(superposition,[],[f32,f1436]) ).
fof(f1704,plain,
one = addition(sF7,one),
inference(superposition,[],[f159,f143]) ).
fof(f1747,plain,
! [X0] : addition(sF4,addition(sF13,X0)) = addition(one,addition(sF4,addition(sF13,X0))),
inference(superposition,[],[f1172,f159]) ).
fof(f1750,plain,
! [X0] : addition(sF4,addition(sF13,X0)) = addition(one,addition(sF13,X0)),
inference(forward_demodulation,[],[f1747,f1322]) ).
fof(f1784,plain,
one = addition(one,sF7),
inference(forward_demodulation,[],[f1704,f31]) ).
fof(f1798,plain,
! [X0] : addition(sF4,addition(sF13,X0)) = addition(one,X0),
inference(forward_demodulation,[],[f1750,f1500]) ).
fof(f1931,plain,
addition(sF4,sF13) = addition(one,sF14),
inference(superposition,[],[f181,f1798]) ).
fof(f1945,plain,
one = addition(sF4,sF13),
inference(forward_demodulation,[],[f1931,f1428]) ).
fof(f2507,plain,
! [X0] : multiplication(one,X0) = multiplication(antidomain(antidomain(X0)),X0),
inference(superposition,[],[f330,f44]) ).
fof(f2542,plain,
! [X0] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(forward_demodulation,[],[f2507,f37]) ).
fof(f2694,plain,
! [X0] : addition(one,X0) = addition(sF11,addition(sF10,X0)),
inference(superposition,[],[f161,f138]) ).
fof(f2771,plain,
! [X0] : addition(one,X0) = addition(sF10,addition(X0,sF11)),
inference(forward_demodulation,[],[f2694,f174]) ).
fof(f4046,plain,
multiplication(sK0,addition(one,sF7)) = addition(sK0,sF8),
inference(superposition,[],[f218,f77]) ).
fof(f4115,plain,
multiplication(sK0,one) = addition(sK0,sF8),
inference(forward_demodulation,[],[f4046,f1784]) ).
fof(f4145,plain,
sK0 = addition(sK0,sF8),
inference(forward_demodulation,[],[f4115,f36]) ).
fof(f4947,plain,
! [X0] : multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)) = multiplication(antidomain(antidomain(antidomain(X0))),one),
inference(superposition,[],[f251,f127]) ).
fof(f4983,plain,
multiplication(antidomain(sF10),sF7) = multiplication(antidomain(sF10),one),
inference(superposition,[],[f251,f139]) ).
fof(f5017,plain,
antidomain(sF10) = multiplication(antidomain(sF10),sF7),
inference(forward_demodulation,[],[f4983,f36]) ).
fof(f5029,plain,
! [X0] : antidomain(antidomain(antidomain(X0))) = multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)),
inference(forward_demodulation,[],[f4947,f36]) ).
fof(f5048,plain,
sF11 = multiplication(sF11,sF7),
inference(forward_demodulation,[],[f5017,f84]) ).
fof(f5053,plain,
! [X0] : antidomain(X0) = antidomain(antidomain(antidomain(X0))),
inference(forward_demodulation,[],[f5029,f2542]) ).
fof(f10800,plain,
! [X0,X1] : multiplication(addition(X0,multiplication(X1,sF10)),sF7) = addition(multiplication(X0,sF7),multiplication(X1,zero)),
inference(superposition,[],[f308,f101]) ).
fof(f10916,plain,
! [X0,X1] : addition(multiplication(X0,sF7),zero) = multiplication(addition(X0,multiplication(X1,sF10)),sF7),
inference(forward_demodulation,[],[f10800,f40]) ).
fof(f11049,plain,
! [X0,X1] : multiplication(X0,sF7) = multiplication(addition(X0,multiplication(X1,sF10)),sF7),
inference(forward_demodulation,[],[f10916,f33]) ).
fof(f17330,plain,
multiplication(sK0,sF11) = multiplication(sF12,sF7),
inference(superposition,[],[f194,f5048]) ).
fof(f17383,plain,
sF12 = multiplication(sF12,sF7),
inference(forward_demodulation,[],[f17330,f86]) ).
fof(f22935,plain,
sF3 = antidomain(antidomain(sF3)),
inference(superposition,[],[f5053,f67]) ).
fof(f22982,plain,
sF3 = antidomain(sF4),
inference(forward_demodulation,[],[f22935,f69]) ).
fof(f36709,plain,
multiplication(sF4,sF12) = multiplication(one,sF12),
inference(superposition,[],[f895,f1945]) ).
fof(f36770,plain,
sF12 = multiplication(sF4,sF12),
inference(forward_demodulation,[],[f36709,f37]) ).
fof(f40733,plain,
! [X0] : multiplication(addition(one,X0),sF7) = multiplication(addition(X0,sF11),sF7),
inference(superposition,[],[f769,f2771]) ).
fof(f82334,plain,
multiplication(sF12,sF7) = multiplication(multiplication(sK0,addition(sF10,sF11)),sF7),
inference(superposition,[],[f11049,f249]) ).
fof(f82430,plain,
multiplication(sF12,sF7) = multiplication(sK0,multiplication(addition(sF10,sF11),sF7)),
inference(forward_demodulation,[],[f82334,f35]) ).
fof(f82489,plain,
multiplication(sF12,sF7) = multiplication(sK0,multiplication(addition(one,sF10),sF7)),
inference(forward_demodulation,[],[f82430,f40733]) ).
fof(f82527,plain,
multiplication(sF12,sF7) = multiplication(sK0,multiplication(one,sF7)),
inference(forward_demodulation,[],[f82489,f770]) ).
fof(f82544,plain,
multiplication(sK0,sF7) = multiplication(sF12,sF7),
inference(forward_demodulation,[],[f82527,f37]) ).
fof(f82550,plain,
multiplication(sK0,sF7) = sF12,
inference(forward_demodulation,[],[f82544,f17383]) ).
fof(f82554,plain,
sF8 = sF12,
inference(forward_demodulation,[],[f82550,f77]) ).
fof(f110645,plain,
! [X0] : multiplication(antidomain(sF4),X0) = multiplication(antidomain(sF4),addition(X0,sF12)),
inference(superposition,[],[f1493,f36770]) ).
fof(f110924,plain,
! [X0] : multiplication(antidomain(sF4),X0) = multiplication(antidomain(sF4),addition(X0,sF8)),
inference(forward_demodulation,[],[f110645,f82554]) ).
fof(f111021,plain,
! [X0] : multiplication(sF3,X0) = multiplication(sF3,addition(X0,sF8)),
inference(forward_demodulation,[],[f110924,f22982]) ).
fof(f111189,plain,
multiplication(sF3,coantidomain(sF3)) = multiplication(sF3,sF8),
inference(superposition,[],[f263,f111021]) ).
fof(f111248,plain,
zero = multiplication(sF3,sF8),
inference(forward_demodulation,[],[f111189,f46]) ).
fof(f112213,plain,
! [X0] : addition(zero,multiplication(X0,sF8)) = multiplication(addition(X0,sF3),sF8),
inference(superposition,[],[f323,f111248]) ).
fof(f112243,plain,
! [X0] : multiplication(X0,sF8) = multiplication(addition(X0,sF3),sF8),
inference(forward_demodulation,[],[f112213,f114]) ).
fof(f126621,plain,
multiplication(sF4,sF8) = multiplication(one,sF8),
inference(superposition,[],[f112243,f142]) ).
fof(f126709,plain,
sF8 = multiplication(sF4,sF8),
inference(forward_demodulation,[],[f126621,f37]) ).
fof(f127156,plain,
addition(sF5,sF8) = multiplication(sF4,addition(sK0,sF8)),
inference(superposition,[],[f227,f126709]) ).
fof(f127229,plain,
multiplication(sF4,sK0) = addition(sF5,sF8),
inference(forward_demodulation,[],[f127156,f4145]) ).
fof(f127242,plain,
multiplication(sF4,sK0) = sF9,
inference(forward_demodulation,[],[f127229,f94]) ).
fof(f127249,plain,
sF5 = sF9,
inference(forward_demodulation,[],[f127242,f71]) ).
fof(f127253,plain,
$false,
inference(forward_subsumption_resolution,[],[f127249,f80]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE098+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 % Computer : n019.cluster.edu
% 0.11/0.40 % Model : x86_64 x86_64
% 0.11/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.40 % Memory : 8046.5625MB
% 0.11/0.40 % OS : Linux 6.8.0-71-generic
% 0.11/0.40 % CPULimit : 300
% 0.11/0.40 % WCLimit : 300
% 0.11/0.40 % DateTime : Sun Sep 27 13:10:05 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43 Running first-order model finding
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.81/1.94 % (3079584)Will run a generic schedule for satisfiability detection.
% 7.81/1.94 % (3079594)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1819323319:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.81/1.94 % (3079590)% WARNING: option uhcvi not known.
% 7.81/1.94 % (3079592)dis+10_1_sil=32000:sp=arity:random_seed=3219321120:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.81/1.94 % (3079589)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1629719754_2999 on theBenchmark for (2999ds/0Mi)
% 7.81/1.94 % (3079590)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=368754676:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.81/1.94 % (3079591)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4166000978:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.81/1.94 % (3079593)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2866984974:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.81/1.94 % (3079595)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2702956023:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.81/1.94 % TRYING [1]
% 7.81/1.94 % TRYING [2]
% 7.81/1.94 % TRYING [3]
% 7.81/1.94 % TRYING [4]
% 7.81/1.94 % (3079594)Instruction limit reached!
% 7.81/1.94 % (3079594)------------------------------
% 7.81/1.94 % (3079594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.81/1.94 % (3079594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/1.94 % (3079594)CaDiCaL version: 2.1.3
% 7.81/1.94 % (3079594)Termination reason: Instruction limit
% 7.81/1.94 % (3079594)Termination phase: Saturation
% 7.81/1.94 % (3079594)Time elapsed: 0.041 s
% 7.81/1.94 % (3079594)Peak memory usage: 13 MB
% 7.81/1.94 % (3079594)Instructions burned: 132 (million)
% 7.81/1.94 % TRYING [5]
% 7.81/1.94 % (3079603)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3401604620:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.81/1.94 % TRYING [1]
% 7.81/1.94 % TRYING [2]
% 7.81/1.94 % TRYING [3]
% 7.81/1.94 % TRYING [4]
% 7.81/1.94 % (3079592)Instruction limit reached!
% 7.81/1.94 % (3079592)------------------------------
% 7.81/1.94 % (3079592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.81/1.94 % (3079592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/1.94 % (3079592)CaDiCaL version: 2.1.3
% 7.81/1.94 % (3079592)Termination reason: Instruction limit
% 7.81/1.94 % (3079592)Termination phase: Saturation
% 7.81/1.94 % (3079592)Time elapsed: 0.057 s
% 7.81/1.94 % (3079592)Peak memory usage: 12 MB
% 7.81/1.94 % (3079592)Instructions burned: 103 (million)
% 7.81/1.94 % TRYING [5]
% 7.81/1.94 % (3079593)Instruction limit reached!
% 7.81/1.94 % (3079593)------------------------------
% 7.81/1.94 % (3079593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.81/1.94 % (3079593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/1.94 % (3079593)CaDiCaL version: 2.1.3
% 7.81/1.94 % (3079593)Termination reason: Instruction limit
% 7.81/1.94 % (3079593)Termination phase: Saturation
% 7.81/1.94 % (3079593)Time elapsed: 0.068 s
% 7.81/1.94 % (3079593)Peak memory usage: 13 MB
% 7.81/1.94 % (3079593)Instructions burned: 117 (million)
% 7.81/1.94 % (3079605)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=16821326:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.81/1.94 % (3079606)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=2110297843:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.81/1.94 % (3079595)Instruction limit reached!
% 7.81/1.94 % (3079595)------------------------------
% 7.81/1.94 % (3079595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.81/1.94 % (3079595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/1.94 % (3079595)CaDiCaL version: 2.1.3
% 7.81/1.94 % (3079595)Termination reason: Instruction limit
% 7.81/1.94 % (3079595)Termination phase: Saturation
% 7.81/1.94 % (3079595)Time elapsed: 0.095 s
% 7.81/1.94 % (3079595)Peak memory usage: 12 MB
% 7.81/1.94 % (3079595)Instructions burned: 160 (million)
% 7.81/1.94 % TRYING [6]
% 7.81/1.94 % (3079609)ott-21_1_sil=16000:fs=off:random_seed=2604070693:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.81/1.94 % TRYING [6]
% 7.81/1.94 % (3079605)Instruction limit reached!
% 7.81/1.94 % (3079605)------------------------------
% 7.81/1.94 % (3079605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079605)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079605)Termination reason: Instruction limit
% 28.33/5.30 % (3079605)Termination phase: Saturation
% 28.33/5.30 % (3079605)Time elapsed: 0.082 s
% 28.33/5.30 % (3079605)Peak memory usage: 13 MB
% 28.33/5.30 % (3079605)Instructions burned: 132 (million)
% 28.33/5.30 % (3079611)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1163095323:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 28.33/5.30 % (3079609)Instruction limit reached!
% 28.33/5.30 % (3079609)------------------------------
% 28.33/5.30 % (3079609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079609)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079609)Termination reason: Instruction limit
% 28.33/5.30 % (3079609)Termination phase: Saturation
% 28.33/5.30 % (3079609)Time elapsed: 0.082 s
% 28.33/5.30 % (3079609)Peak memory usage: 12 MB
% 28.33/5.30 % (3079609)Instructions burned: 181 (million)
% 28.33/5.30 % (3079603)Instruction limit reached!
% 28.33/5.30 % (3079603)------------------------------
% 28.33/5.30 % (3079603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079603)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079603)Termination reason: Instruction limit
% 28.33/5.30 % (3079603)Termination phase: Finite model building SAT solving
% 28.33/5.30 % (3079603)Time elapsed: 0.159 s
% 28.33/5.30 % (3079603)Peak memory usage: 34 MB
% 28.33/5.30 % (3079603)Instructions burned: 716 (million)
% 28.33/5.30 % (3079614)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1705925477:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 28.33/5.30 % (3079613)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3913667810:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 28.33/5.30 % TRYING [1]
% 28.33/5.30 % TRYING [2]
% 28.33/5.30 % TRYING [3]
% 28.33/5.30 % TRYING [4]
% 28.33/5.30 % TRYING [5]
% 28.33/5.30 % TRYING [7]
% 28.33/5.30 % (3079606)Instruction limit reached!
% 28.33/5.30 % (3079606)------------------------------
% 28.33/5.30 % (3079606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079606)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079606)Termination reason: Instruction limit
% 28.33/5.30 % (3079606)Termination phase: Saturation
% 28.33/5.30 % (3079606)Time elapsed: 0.340 s
% 28.33/5.30 % (3079606)Peak memory usage: 15 MB
% 28.33/5.30 % (3079606)Instructions burned: 685 (million)
% 28.33/5.30 % (3079611)Instruction limit reached!
% 28.33/5.30 % (3079611)------------------------------
% 28.33/5.30 % (3079611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079611)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079611)Termination reason: Instruction limit
% 28.33/5.30 % (3079611)Termination phase: Saturation
% 28.33/5.30 % (3079611)Time elapsed: 0.261 s
% 28.33/5.30 % (3079611)Peak memory usage: 16 MB
% 28.33/5.30 % (3079611)Instructions burned: 478 (million)
% 28.33/5.30 % (3079617)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=319359874:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 28.33/5.30 % TRYING [6]
% 28.33/5.30 % (3079618)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=572865013: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)
% 28.33/5.30 % (3079614)Instruction limit reached!
% 28.33/5.30 % (3079614)------------------------------
% 28.33/5.30 % (3079614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079614)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079614)Termination reason: Instruction limit
% 28.33/5.30 % (3079614)Termination phase: Saturation
% 28.33/5.30 % (3079614)Time elapsed: 0.335 s
% 28.33/5.30 % (3079614)Peak memory usage: 22 MB
% 28.33/5.30 % (3079614)Instructions burned: 1180 (million)
% 28.33/5.30 % (3079613)Instruction limit reached!
% 28.33/5.30 % (3079613)------------------------------
% 28.33/5.30 % (3079613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079613)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079613)Termination reason: Instruction limit
% 28.33/5.30 % (3079613)Termination phase: Finite model building constraint generation
% 28.33/5.30 % (3079613)Time elapsed: 0.337 s
% 28.33/5.30 % (3079613)Peak memory usage: 27 MB
% 28.33/5.30 % (3079613)Instructions burned: 867 (million)
% 28.33/5.30 % (3079621)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3026071580:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 28.33/5.30 % (3079622)fmb+10_1_sil=64000:random_seed=1528284933:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 28.33/5.30 % TRYING [1]
% 28.33/5.30 % TRYING [2]
% 28.33/5.30 % TRYING [3]
% 28.33/5.30 % TRYING [4]
% 28.33/5.30 % TRYING [14]
% 28.33/5.30 % TRYING [5]
% 28.33/5.30 % (3079617)Instruction limit reached!
% 28.33/5.30 % (3079617)------------------------------
% 28.33/5.30 % (3079617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079617)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079617)Termination reason: Instruction limit
% 28.33/5.30 % (3079617)Termination phase: Finite model building constraint generation
% 28.33/5.30 % (3079617)Time elapsed: 0.334 s
% 28.33/5.30 % (3079617)Peak memory usage: 81 MB
% 28.33/5.30 % (3079617)Instructions burned: 889 (million)
% 28.33/5.30 % (3079621)Instruction limit reached!
% 28.33/5.30 % (3079621)------------------------------
% 28.33/5.30 % (3079621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079621)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079621)Termination reason: Instruction limit
% 28.33/5.30 % (3079621)Termination phase: Saturation
% 28.33/5.30 % (3079621)Time elapsed: 0.248 s
% 28.33/5.30 % (3079621)Peak memory usage: 19 MB
% 28.33/5.30 % (3079621)Instructions burned: 879 (million)
% 28.33/5.30 % (3079625)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3637382605:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 28.33/5.30 % TRYING [6]
% 28.33/5.30 % TRYING [20]
% 28.33/5.30 % (3079626)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2211876875:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 28.33/5.30 % TRYING [8]
% 28.33/5.30 % (3079618)Instruction limit reached!
% 28.33/5.30 % (3079618)------------------------------
% 28.33/5.30 % (3079618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079618)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079618)Termination reason: Instruction limit
% 28.33/5.30 % (3079618)Termination phase: Saturation
% 28.33/5.30 % (3079618)Time elapsed: 0.374 s
% 28.33/5.30 % (3079618)Peak memory usage: 17 MB
% 28.33/5.30 % (3079618)Instructions burned: 693 (million)
% 28.33/5.30 % (3079629)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1347973694:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 28.33/5.30 % (3079626)Instruction limit reached!
% 28.33/5.30 % (3079626)------------------------------
% 28.33/5.30 % (3079626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079626)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079626)Termination reason: Instruction limit
% 28.33/5.30 % (3079626)Termination phase: Finite model building constraint generation
% 28.33/5.30 % (3079626)Time elapsed: 0.192 s
% 28.33/5.30 % (3079626)Peak memory usage: 69 MB
% 28.33/5.30 % (3079626)Instructions burned: 924 (million)
% 28.33/5.30 % (3079631)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4140186370:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 28.33/5.30 % TRYING [7]
% 28.33/5.30 % (3079631)Instruction limit reached!
% 28.33/5.30 % (3079631)------------------------------
% 28.33/5.30 % (3079631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079631)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079631)Termination reason: Instruction limit
% 28.33/5.30 % (3079631)Termination phase: Saturation
% 28.33/5.30 % (3079631)Time elapsed: 0.409 s
% 28.33/5.30 % (3079631)Peak memory usage: 27 MB
% 28.33/5.30 % (3079631)Instructions burned: 1474 (million)
% 28.33/5.30 % (3079633)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1188309490:i=6324_2985 on theBenchmark for (2985ds/6324Mi)
% 28.33/5.30 % TRYING [77]
% 28.33/5.30 % TRYING [8]
% 28.33/5.30 % (3079633)Instruction limit reached!
% 28.33/5.30 % (3079633)------------------------------
% 28.33/5.30 % (3079633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079633)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079633)Termination reason: Instruction limit
% 28.33/5.30 % (3079633)Termination phase: Finite model building constraint generation
% 28.33/5.30 % (3079633)Time elapsed: 1.293 s
% 28.33/5.30 % (3079633)Peak memory usage: 514 MB
% 28.33/5.30 % (3079633)Instructions burned: 6325 (million)
% 28.33/5.30 % (3079635)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=689378518:fmbsr=2.30978:i=2174_2971 on theBenchmark for (2971ds/2174Mi)
% 28.33/5.30 % TRYING [16]
% 28.33/5.30 % TRYING [8]
% 28.33/5.30 % (3079635)Instruction limit reached!
% 28.33/5.30 % (3079635)------------------------------
% 28.33/5.30 % (3079635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079635)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079635)Termination reason: Instruction limit
% 28.33/5.30 % (3079635)Termination phase: Finite model building constraint generation
% 28.33/5.30 % (3079635)Time elapsed: 0.426 s
% 28.33/5.30 % (3079635)Peak memory usage: 145 MB
% 28.33/5.30 % (3079635)Instructions burned: 2177 (million)
% 28.33/5.30 % (3079637)ott-2_1_sil=16000:newcnf=on:random_seed=1721781738:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2967 on theBenchmark for (2967ds/869Mi)
% 28.33/5.30 % (3079637)Instruction limit reached!
% 28.33/5.30 % (3079637)------------------------------
% 28.33/5.30 % (3079637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079637)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079637)Termination reason: Instruction limit
% 28.33/5.30 % (3079637)Termination phase: Saturation
% 28.33/5.30 % (3079637)Time elapsed: 0.268 s
% 28.33/5.30 % (3079637)Peak memory usage: 20 MB
% 28.33/5.30 % (3079637)Instructions burned: 869 (million)
% 28.33/5.30 % (3079639)ott+10_1_sil=32000:tgt=ground:random_seed=2961408599:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi)
% 28.33/5.30 % (3079629)Instruction limit reached!
% 28.33/5.30 % (3079629)------------------------------
% 28.33/5.30 % (3079629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079629)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079629)Termination reason: Instruction limit
% 28.33/5.30 % (3079629)Termination phase: Saturation
% 28.33/5.30 % (3079629)Time elapsed: 2.808 s
% 28.33/5.30 % (3079629)Peak memory usage: 59 MB
% 28.33/5.30 % (3079629)Instructions burned: 5133 (million)
% 28.33/5.30 % (3079641)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3668504059:i=54282_2962 on theBenchmark for (2962ds/54282Mi)
% 28.33/5.30 % TRYING [1]
% 28.33/5.30 % TRYING [2]
% 28.33/5.30 % TRYING [3]
% 28.33/5.30 % TRYING [4]
% 28.33/5.30 % TRYING [5]
% 28.33/5.30 % TRYING [6]
% 28.33/5.30 % TRYING [7]
% 28.33/5.30 % (3079625)Instruction limit reached!
% 28.33/5.30 % (3079625)------------------------------
% 28.33/5.30 % (3079625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.30 % (3079625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.30 % (3079625)CaDiCaL version: 2.1.3
% 28.33/5.30 % (3079625)Termination reason: Instruction limit
% 28.33/5.30 % (3079625)Termination phase: Finite model building constraint generation
% 28.33/5.30 % (3079625)Time elapsed: 3.312 s
% 28.33/5.30 % (3079625)Peak memory usage: 611 MB
% 28.33/5.30 % (3079625)Instructions burned: 9517 (million)
% 28.33/5.30 % (3079643)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1523308841:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 28.33/5.30 % (3079639) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3079584-3079639"...
% 28.33/5.30 % (3079639)...printing done.
% 28.33/5.30 % (3079639)Refutation found. Thanks to Tanya!
% 28.33/5.30 % SZS status Theorem for theBenchmark
% 28.33/5.30 % SZS output start Proof for theBenchmark
% See solution above
% 28.33/5.31 % (3079639)------------------------------
% 28.33/5.31 % (3079639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.33/5.31 % (3079639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.33/5.31 % (3079639)CaDiCaL version: 2.1.3
% 28.33/5.31 % (3079639)Termination reason: Refutation
% 28.33/5.31 % (3079639)Time elapsed: 1.264 s
% 28.33/5.31 % (3079639)Peak memory usage: 51 MB
% 28.33/5.31 % (3079639)Instructions burned: 3931 (million)
% 28.33/5.31 % (3079584)Success in time 4.862 s
% 28.33/5.31 % Vampire exiting
%------------------------------------------------------------------------------