%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : KLE010+3 : 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 : n017.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:36 AM UTC 2026
% Result : Theorem 1.92s 0.83s
% Output : Refutation 1.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 19
% Syntax : Number of formulae : 189 ( 93 unt; 3 def)
% Number of atoms : 314 ( 172 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 272 ( 147 ~; 102 |; 10 &)
% ( 7 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 4 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 107 ( 0 sgn 102 !; 5 ?)
% 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(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(f10,axiom,
! [X0] : multiplication(X0,zero) = zero,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',right_annihilation) ).
fof(f13,axiom,
! [X0] :
( test(X0)
<=> ? [X1] : complement(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+1.ax',test_1) ).
fof(f14,axiom,
! [X0,X1] :
( complement(X1,X0)
<=> ( multiplication(X0,X1) = zero
& multiplication(X1,X0) = zero
& addition(X0,X1) = one ) ),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+1.ax',test_2) ).
fof(f15,axiom,
! [X0,X1] :
( test(X0)
=> ( c(X0) = X1
<=> complement(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+1.ax',test_3) ).
fof(f16,axiom,
! [X0] :
( ~ test(X0)
=> c(X0) = zero ),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+1.ax',test_4) ).
fof(f17,axiom,
! [X0,X1] :
( ( test(X0)
& test(X1) )
=> c(addition(X0,X1)) = multiplication(c(X0),c(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+2.ax',test_deMorgan1) ).
fof(f18,axiom,
! [X0,X1] :
( ( test(X0)
& test(X1) )
=> c(multiplication(X0,X1)) = addition(c(X0),c(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+2.ax',test_deMorgan2) ).
fof(f19,conjecture,
! [X0,X1] :
( ( test(X1)
& test(X0) )
=> one = addition(addition(addition(addition(multiplication(X1,X0),multiplication(c(X1),X0)),multiplication(X0,X1)),multiplication(c(X0),X1)),multiplication(c(X0),c(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f20,negated_conjecture,
~ ! [X0,X1] :
( ( test(X1)
& test(X0) )
=> one = addition(addition(addition(addition(multiplication(X1,X0),multiplication(c(X1),X0)),multiplication(X0,X1)),multiplication(c(X0),X1)),multiplication(c(X0),c(X1))) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f21,plain,
! [X0,X1] :
( ( c(X0) = X1
<=> complement(X0,X1) )
| ~ test(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f22,plain,
! [X0] :
( c(X0) = zero
| test(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f23,plain,
! [X0,X1] :
( c(addition(X0,X1)) = multiplication(c(X0),c(X1))
| ~ test(X0)
| ~ test(X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f24,plain,
! [X0,X1] :
( c(addition(X0,X1)) = multiplication(c(X0),c(X1))
| ~ test(X0)
| ~ test(X1) ),
inference(flattening,[],[f23]) ).
fof(f25,plain,
! [X0,X1] :
( c(multiplication(X0,X1)) = addition(c(X0),c(X1))
| ~ test(X0)
| ~ test(X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f26,plain,
! [X0,X1] :
( c(multiplication(X0,X1)) = addition(c(X0),c(X1))
| ~ test(X0)
| ~ test(X1) ),
inference(flattening,[],[f25]) ).
fof(f27,plain,
? [X0,X1] :
( one != addition(addition(addition(addition(multiplication(X1,X0),multiplication(c(X1),X0)),multiplication(X0,X1)),multiplication(c(X0),X1)),multiplication(c(X0),c(X1)))
& test(X1)
& test(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f28,plain,
? [X0,X1] :
( one != addition(addition(addition(addition(multiplication(X1,X0),multiplication(c(X1),X0)),multiplication(X0,X1)),multiplication(c(X0),X1)),multiplication(c(X0),c(X1)))
& test(X1)
& test(X0) ),
inference(flattening,[],[f27]) ).
fof(f29,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f30,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f31,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f32,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f34,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f35,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f36,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f37,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f38,plain,
! [X0] : zero = multiplication(X0,zero),
inference(cnf_transformation,[],[f10]) ).
fof(f40,plain,
! [X0,X1] :
( ~ complement(X1,X0)
| test(X0) ),
inference(cnf_transformation,[],[f13]) ).
fof(f41,plain,
! [X0] :
( complement(sK0(X0),X0)
| ~ test(X0) ),
inference(cnf_transformation,[],[f13]) ).
fof(f42,plain,
! [X0,X1] :
( ~ complement(X1,X0)
| addition(X0,X1) = one ),
inference(cnf_transformation,[],[f14]) ).
fof(f43,plain,
! [X0,X1] :
( ~ complement(X1,X0)
| zero = multiplication(X1,X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f44,plain,
! [X0,X1] :
( ~ complement(X1,X0)
| zero = multiplication(X0,X1) ),
inference(cnf_transformation,[],[f14]) ).
fof(f45,plain,
! [X0,X1] :
( zero != multiplication(X1,X0)
| addition(X0,X1) != one
| zero != multiplication(X0,X1)
| complement(X1,X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f46,plain,
! [X0,X1] :
( ~ complement(X0,X1)
| ~ test(X0)
| c(X0) = X1 ),
inference(cnf_transformation,[],[f21]) ).
fof(f47,plain,
! [X0,X1] :
( ~ test(X0)
| complement(X0,X1)
| c(X0) != X1 ),
inference(cnf_transformation,[],[f21]) ).
fof(f48,plain,
! [X0] :
( test(X0)
| zero = c(X0) ),
inference(cnf_transformation,[],[f22]) ).
fof(f49,plain,
! [X0,X1] :
( ~ test(X1)
| ~ test(X0)
| c(addition(X0,X1)) = multiplication(c(X0),c(X1)) ),
inference(cnf_transformation,[],[f24]) ).
fof(f50,plain,
! [X0,X1] :
( ~ test(X1)
| ~ test(X0)
| c(multiplication(X0,X1)) = addition(c(X0),c(X1)) ),
inference(cnf_transformation,[],[f26]) ).
fof(f51,plain,
test(sK1),
inference(cnf_transformation,[],[f28]) ).
fof(f52,plain,
test(sK2),
inference(cnf_transformation,[],[f28]) ).
fof(f53,plain,
one != addition(addition(addition(addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1)),multiplication(sK1,sK2)),multiplication(c(sK1),sK2)),multiplication(c(sK1),c(sK2))),
inference(cnf_transformation,[],[f28]) ).
fof(f54,plain,
! [X0] :
( complement(X0,c(X0))
| ~ test(X0) ),
inference(equality_resolution,[],[f47]) ).
fof(f66,plain,
one != addition(multiplication(c(sK1),c(sK2)),addition(addition(addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1)),multiplication(sK1,sK2)),multiplication(c(sK1),sK2))),
inference(superposition,[],[f53,f29]) ).
fof(f67,plain,
one != addition(multiplication(c(sK1),c(sK2)),addition(multiplication(c(sK1),sK2),addition(addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1)),multiplication(sK1,sK2)))),
inference(forward_demodulation,[],[f66,f29]) ).
fof(f73,plain,
one != addition(multiplication(c(sK1),c(sK2)),addition(multiplication(c(sK1),sK2),addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1))))),
inference(forward_demodulation,[],[f67,f29]) ).
fof(f79,plain,
! [X0] :
( ~ test(X0)
| one = addition(X0,sK0(X0)) ),
inference(resolution,[],[f42,f41]) ).
fof(f80,plain,
! [X0] :
( one = addition(c(X0),X0)
| ~ test(X0) ),
inference(resolution,[],[f42,f54]) ).
fof(f81,plain,
! [X0] :
( ~ test(X0)
| one = addition(X0,c(X0)) ),
inference(forward_demodulation,[],[f80,f29]) ).
fof(f86,plain,
! [X0] :
( ~ test(X0)
| zero = multiplication(sK0(X0),X0) ),
inference(resolution,[],[f43,f41]) ).
fof(f88,plain,
! [X0] :
( ~ test(X0)
| zero = multiplication(X0,sK0(X0)) ),
inference(resolution,[],[f44,f41]) ).
fof(f92,plain,
one = addition(sK1,sK0(sK1)),
inference(resolution,[],[f79,f51]) ).
fof(f93,plain,
one = addition(sK2,sK0(sK2)),
inference(resolution,[],[f79,f52]) ).
fof(f96,plain,
one = addition(sK1,c(sK1)),
inference(resolution,[],[f81,f51]) ).
fof(f97,plain,
one = addition(sK2,c(sK2)),
inference(resolution,[],[f81,f52]) ).
fof(f98,plain,
! [X0] :
( ~ test(sK0(X0))
| c(sK0(X0)) = X0
| ~ test(X0) ),
inference(resolution,[],[f46,f41]) ).
fof(f103,plain,
zero = multiplication(sK0(sK1),sK1),
inference(resolution,[],[f86,f51]) ).
fof(f104,plain,
zero = multiplication(sK0(sK2),sK2),
inference(resolution,[],[f86,f52]) ).
fof(f111,plain,
zero = multiplication(sK1,sK0(sK1)),
inference(resolution,[],[f88,f51]) ).
fof(f112,plain,
zero = multiplication(sK2,sK0(sK2)),
inference(resolution,[],[f88,f52]) ).
fof(f414,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f30,f32]) ).
fof(f426,plain,
! [X0] : addition(one,X0) = addition(sK1,addition(sK0(sK1),X0)),
inference(superposition,[],[f30,f92]) ).
fof(f427,plain,
! [X0] : addition(one,X0) = addition(sK1,addition(c(sK1),X0)),
inference(superposition,[],[f30,f96]) ).
fof(f428,plain,
! [X0] : addition(one,X0) = addition(sK2,addition(sK0(sK2),X0)),
inference(superposition,[],[f30,f93]) ).
fof(f431,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X1,addition(X2,X0)),
inference(superposition,[],[f30,f29]) ).
fof(f456,plain,
addition(sK1,sK0(sK1)) = addition(one,sK0(sK1)),
inference(superposition,[],[f426,f32]) ).
fof(f457,plain,
! [X0] : addition(one,X0) = addition(sK1,addition(X0,sK0(sK1))),
inference(superposition,[],[f426,f29]) ).
fof(f479,plain,
one = addition(one,sK0(sK1)),
inference(forward_demodulation,[],[f456,f92]) ).
fof(f682,plain,
! [X0] : addition(one,X0) = addition(sK2,addition(X0,sK0(sK2))),
inference(superposition,[],[f428,f29]) ).
fof(f773,plain,
! [X0] : addition(multiplication(sK1,X0),zero) = multiplication(sK1,addition(X0,sK0(sK1))),
inference(superposition,[],[f36,f111]) ).
fof(f793,plain,
! [X0] : multiplication(sK1,X0) = multiplication(sK1,addition(X0,sK0(sK1))),
inference(forward_demodulation,[],[f773,f31]) ).
fof(f1214,plain,
multiplication(sK1,one) = multiplication(sK1,sK1),
inference(superposition,[],[f793,f92]) ).
fof(f1226,plain,
sK1 = multiplication(sK1,sK1),
inference(forward_demodulation,[],[f1214,f34]) ).
fof(f1242,plain,
! [X0] : multiplication(addition(sK1,X0),sK1) = addition(sK1,multiplication(X0,sK1)),
inference(superposition,[],[f37,f1226]) ).
fof(f1426,plain,
! [X0] :
( ~ test(X0)
| c(addition(X0,sK1)) = multiplication(c(X0),c(sK1)) ),
inference(resolution,[],[f49,f51]) ).
fof(f1507,plain,
! [X0] :
( ~ test(X0)
| c(multiplication(X0,sK2)) = addition(c(X0),c(sK2)) ),
inference(resolution,[],[f50,f52]) ).
fof(f1718,plain,
addition(sK1,one) = addition(one,one),
inference(superposition,[],[f457,f479]) ).
fof(f1726,plain,
one = addition(sK1,one),
inference(forward_demodulation,[],[f1718,f32]) ).
fof(f1836,plain,
( zero != zero
| one != addition(sK0(sK1),sK1)
| zero != multiplication(sK0(sK1),sK1)
| complement(sK1,sK0(sK1)) ),
inference(superposition,[],[f45,f111]) ).
fof(f1848,plain,
( zero != zero
| one != addition(sK0(sK2),sK2)
| zero != multiplication(sK0(sK2),sK2)
| complement(sK2,sK0(sK2)) ),
inference(superposition,[],[f45,f112]) ).
fof(f1852,plain,
( one != addition(sK0(sK2),sK2)
| zero != multiplication(sK0(sK2),sK2)
| complement(sK2,sK0(sK2)) ),
inference(trivial_inequality_removal,[],[f1848]) ).
fof(f1857,plain,
( one != addition(sK0(sK1),sK1)
| zero != multiplication(sK0(sK1),sK1)
| complement(sK1,sK0(sK1)) ),
inference(trivial_inequality_removal,[],[f1836]) ).
fof(f1883,plain,
( one != addition(sK0(sK2),sK2)
| complement(sK2,sK0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1852,f104]) ).
fof(f1895,plain,
( one != addition(sK0(sK1),sK1)
| complement(sK1,sK0(sK1)) ),
inference(forward_subsumption_resolution,[],[f1857,f103]) ).
fof(f1954,definition,
( spl3_35
<=> one = sK2 ),
introduced(definition,[new_symbols(definition,[spl3_35])],[avatar_definition]) ).
fof(f1955,plain,
( one = sK2
| ~ spl3_35 ),
inference(avatar_component_clause,[],[f1954]) ).
fof(f1956,plain,
( one != sK2
| spl3_35 ),
inference(avatar_component_clause,[],[f1954]) ).
fof(f1960,plain,
( one != addition(sK2,sK0(sK2))
| complement(sK2,sK0(sK2)) ),
inference(forward_demodulation,[],[f1883,f29]) ).
fof(f1986,plain,
( one != addition(sK1,sK0(sK1))
| complement(sK1,sK0(sK1)) ),
inference(forward_demodulation,[],[f1895,f29]) ).
fof(f2062,plain,
complement(sK2,sK0(sK2)),
inference(forward_subsumption_resolution,[],[f1960,f93]) ).
fof(f2076,plain,
complement(sK1,sK0(sK1)),
inference(forward_subsumption_resolution,[],[f1986,f92]) ).
fof(f2114,plain,
( ~ test(sK2)
| c(sK2) = sK0(sK2) ),
inference(resolution,[],[f2062,f46]) ).
fof(f2120,plain,
c(sK2) = sK0(sK2),
inference(forward_subsumption_resolution,[],[f2114,f52]) ).
fof(f2186,plain,
( ~ test(sK1)
| c(sK1) = sK0(sK1) ),
inference(resolution,[],[f2076,f46]) ).
fof(f2188,plain,
test(sK0(sK1)),
inference(resolution,[],[f2076,f40]) ).
fof(f2192,plain,
c(sK1) = sK0(sK1),
inference(forward_subsumption_resolution,[],[f2186,f51]) ).
fof(f2224,plain,
( sK1 = c(sK0(sK1))
| ~ test(sK1) ),
inference(resolution,[],[f2188,f98]) ).
fof(f2236,plain,
c(addition(sK0(sK1),sK1)) = multiplication(c(sK0(sK1)),c(sK1)),
inference(resolution,[],[f2188,f1426]) ).
fof(f2237,plain,
multiplication(c(sK0(sK1)),c(sK1)) = c(addition(sK1,sK0(sK1))),
inference(forward_demodulation,[],[f2236,f29]) ).
fof(f2238,plain,
sK1 = c(sK0(sK1)),
inference(forward_subsumption_resolution,[],[f2224,f51]) ).
fof(f2239,plain,
c(one) = multiplication(c(sK0(sK1)),c(sK1)),
inference(forward_demodulation,[],[f2237,f92]) ).
fof(f2789,plain,
c(one) = multiplication(c(sK0(sK1)),sK0(sK1)),
inference(forward_demodulation,[],[f2239,f2192]) ).
fof(f2798,plain,
multiplication(sK1,sK0(sK1)) = c(one),
inference(forward_demodulation,[],[f2789,f2238]) ).
fof(f2799,plain,
zero = c(one),
inference(forward_demodulation,[],[f2798,f111]) ).
fof(f2966,plain,
! [X0] :
( c(multiplication(X0,sK2)) = addition(c(X0),sK0(sK2))
| ~ test(X0) ),
inference(forward_demodulation,[],[f1507,f2120]) ).
fof(f2967,plain,
! [X0] :
( ~ test(X0)
| c(multiplication(X0,sK2)) = addition(sK0(sK2),c(X0)) ),
inference(forward_demodulation,[],[f2966,f29]) ).
fof(f3296,definition,
( spl3_82
<=> zero = addition(sK0(sK1),sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl3_82])],[avatar_definition]) ).
fof(f3297,plain,
( zero != addition(sK0(sK1),sK0(sK2))
| spl3_82 ),
inference(avatar_component_clause,[],[f3296]) ).
fof(f3298,plain,
( zero = addition(sK0(sK1),sK0(sK2))
| ~ spl3_82 ),
inference(avatar_component_clause,[],[f3296]) ).
fof(f3378,plain,
c(multiplication(sK1,sK2)) = addition(sK0(sK2),c(sK1)),
inference(resolution,[],[f2967,f51]) ).
fof(f3381,plain,
addition(sK0(sK2),sK0(sK1)) = c(multiplication(sK1,sK2)),
inference(forward_demodulation,[],[f3378,f2192]) ).
fof(f3392,plain,
addition(sK0(sK1),sK0(sK2)) = c(multiplication(sK1,sK2)),
inference(forward_demodulation,[],[f3381,f29]) ).
fof(f3491,definition,
( spl3_88
<=> test(multiplication(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl3_88])],[avatar_definition]) ).
fof(f3492,plain,
( test(multiplication(sK1,sK2))
| ~ spl3_88 ),
inference(avatar_component_clause,[],[f3491]) ).
fof(f3493,plain,
( ~ test(multiplication(sK1,sK2))
| spl3_88 ),
inference(avatar_component_clause,[],[f3491]) ).
fof(f3510,plain,
( addition(sK2,zero) = addition(one,sK0(sK1))
| ~ spl3_82 ),
inference(superposition,[],[f682,f3298]) ).
fof(f3517,plain,
( one = addition(sK2,zero)
| ~ spl3_82 ),
inference(forward_demodulation,[],[f3510,f479]) ).
fof(f3524,plain,
( one = sK2
| ~ spl3_82 ),
inference(forward_demodulation,[],[f3517,f31]) ).
fof(f3526,plain,
( $false
| spl3_35
| ~ spl3_82 ),
inference(forward_subsumption_resolution,[],[f3524,f1956]) ).
fof(f3527,plain,
( spl3_35
| ~ spl3_82 ),
inference(avatar_contradiction_clause,[],[f3526]) ).
fof(f5024,plain,
( zero = c(multiplication(sK1,sK2))
| spl3_88 ),
inference(resolution,[],[f3493,f48]) ).
fof(f5111,plain,
( zero = addition(sK0(sK1),sK0(sK2))
| spl3_88 ),
inference(superposition,[],[f5024,f3392]) ).
fof(f5117,plain,
( $false
| spl3_82
| spl3_88 ),
inference(forward_subsumption_resolution,[],[f5111,f3297]) ).
fof(f5118,plain,
( spl3_82
| spl3_88 ),
inference(avatar_contradiction_clause,[],[f5117]) ).
fof(f5121,plain,
( one = addition(multiplication(sK1,sK2),sK0(multiplication(sK1,sK2)))
| ~ spl3_88 ),
inference(resolution,[],[f3492,f79]) ).
fof(f10500,plain,
( ! [X0] : multiplication(X0,sK2) = X0
| ~ spl3_35 ),
inference(superposition,[],[f34,f1955]) ).
fof(f10518,plain,
( zero = c(sK2)
| ~ spl3_35 ),
inference(superposition,[],[f2799,f1955]) ).
fof(f10956,plain,
( zero = sK0(sK2)
| ~ spl3_35 ),
inference(superposition,[],[f10518,f2120]) ).
fof(f11407,plain,
( one != addition(addition(addition(addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1)),sK1),multiplication(c(sK1),sK2)),multiplication(c(sK1),c(sK2)))
| ~ spl3_35 ),
inference(superposition,[],[f53,f10500]) ).
fof(f11441,plain,
( one != addition(multiplication(c(sK1),c(sK2)),addition(addition(addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1)),sK1),multiplication(c(sK1),sK2)))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11407,f29]) ).
fof(f11481,plain,
( one != addition(multiplication(c(sK1),c(sK2)),addition(multiplication(c(sK1),sK2),addition(addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1)),sK1)))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11441,f29]) ).
fof(f11501,plain,
( one != addition(multiplication(c(sK1),c(sK2)),addition(multiplication(c(sK1),sK2),addition(sK1,addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1)))))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11481,f29]) ).
fof(f11515,plain,
( one != addition(multiplication(c(sK1),c(sK2)),addition(multiplication(c(sK1),sK2),addition(sK1,multiplication(addition(sK2,c(sK2)),sK1))))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11501,f37]) ).
fof(f11525,plain,
( one != addition(multiplication(c(sK1),c(sK2)),addition(multiplication(c(sK1),sK2),multiplication(addition(sK1,addition(sK2,c(sK2))),sK1)))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11515,f1242]) ).
fof(f11535,plain,
( one != addition(multiplication(c(sK1),c(sK2)),addition(multiplication(c(sK1),sK2),multiplication(addition(sK1,one),sK1)))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11525,f97]) ).
fof(f11545,plain,
( one != addition(multiplication(c(sK1),c(sK2)),addition(multiplication(c(sK1),sK2),multiplication(one,sK1)))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11535,f1726]) ).
fof(f11558,plain,
( one != addition(multiplication(c(sK1),c(sK2)),addition(multiplication(one,sK1),multiplication(c(sK1),sK2)))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11545,f29]) ).
fof(f11567,plain,
( one != addition(multiplication(c(sK1),c(sK2)),addition(multiplication(one,sK1),c(sK1)))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11558,f10500]) ).
fof(f11573,plain,
( one != addition(multiplication(c(sK1),c(sK2)),addition(c(sK1),multiplication(one,sK1)))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11567,f29]) ).
fof(f11577,plain,
( one != addition(multiplication(c(sK1),c(sK2)),addition(c(sK1),sK1))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11573,f35]) ).
fof(f11581,plain,
( one != addition(addition(c(sK1),sK1),multiplication(c(sK1),c(sK2)))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11577,f29]) ).
fof(f11585,plain,
( one != addition(c(sK1),addition(sK1,multiplication(c(sK1),c(sK2))))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11581,f30]) ).
fof(f11589,plain,
( one != addition(c(sK1),addition(sK1,multiplication(c(sK1),sK0(sK2))))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11585,f2120]) ).
fof(f11594,plain,
( one != addition(c(sK1),addition(sK1,multiplication(c(sK1),zero)))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11589,f10956]) ).
fof(f11598,plain,
( one != addition(c(sK1),addition(sK1,zero))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11594,f38]) ).
fof(f11600,plain,
( one != addition(c(sK1),sK1)
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11598,f31]) ).
fof(f11603,plain,
( one != addition(sK1,c(sK1))
| ~ spl3_35 ),
inference(forward_demodulation,[],[f11600,f29]) ).
fof(f11604,plain,
( $false
| ~ spl3_35 ),
inference(forward_subsumption_resolution,[],[f11603,f96]) ).
fof(f11605,plain,
~ spl3_35,
inference(avatar_contradiction_clause,[],[f11604]) ).
fof(f13450,plain,
( one = addition(multiplication(sK1,sK2),one)
| ~ spl3_88 ),
inference(superposition,[],[f414,f5121]) ).
fof(f13554,plain,
( one = addition(one,multiplication(sK1,sK2))
| ~ spl3_88 ),
inference(forward_demodulation,[],[f13450,f29]) ).
fof(f15415,plain,
one != addition(multiplication(c(sK1),sK2),addition(addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1))),multiplication(c(sK1),c(sK2)))),
inference(superposition,[],[f73,f431]) ).
fof(f15588,plain,
one != addition(multiplication(c(sK1),sK2),addition(multiplication(c(sK1),c(sK2)),addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1))))),
inference(forward_demodulation,[],[f15415,f29]) ).
fof(f15751,plain,
one != addition(multiplication(c(sK1),sK2),addition(multiplication(sK1,sK2),addition(addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1)),multiplication(c(sK1),c(sK2))))),
inference(forward_demodulation,[],[f15588,f431]) ).
fof(f15841,plain,
one != addition(multiplication(sK1,sK2),addition(addition(addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1)),multiplication(c(sK1),c(sK2))),multiplication(c(sK1),sK2))),
inference(forward_demodulation,[],[f15751,f431]) ).
fof(f15891,plain,
one != addition(multiplication(sK1,sK2),addition(multiplication(c(sK1),sK2),addition(addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1)),multiplication(c(sK1),c(sK2))))),
inference(forward_demodulation,[],[f15841,f29]) ).
fof(f15922,plain,
one != addition(multiplication(sK1,sK2),addition(multiplication(c(sK1),sK2),addition(multiplication(c(sK1),c(sK2)),addition(multiplication(sK2,sK1),multiplication(c(sK2),sK1))))),
inference(forward_demodulation,[],[f15891,f29]) ).
fof(f15939,plain,
one != addition(multiplication(sK1,sK2),addition(multiplication(c(sK1),sK2),addition(multiplication(sK2,sK1),addition(multiplication(c(sK2),sK1),multiplication(c(sK1),c(sK2)))))),
inference(forward_demodulation,[],[f15922,f431]) ).
fof(f15950,plain,
one != addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),addition(addition(multiplication(c(sK2),sK1),multiplication(c(sK1),c(sK2))),multiplication(c(sK1),sK2)))),
inference(forward_demodulation,[],[f15939,f431]) ).
fof(f15962,plain,
one != addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),addition(multiplication(c(sK1),sK2),addition(multiplication(c(sK2),sK1),multiplication(c(sK1),c(sK2)))))),
inference(forward_demodulation,[],[f15950,f29]) ).
fof(f15974,plain,
one != addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),addition(multiplication(c(sK1),sK2),addition(multiplication(sK0(sK2),sK1),multiplication(c(sK1),sK0(sK2)))))),
inference(forward_demodulation,[],[f15962,f2120]) ).
fof(f15984,plain,
one != addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),addition(multiplication(sK0(sK2),sK1),addition(multiplication(c(sK1),sK0(sK2)),multiplication(c(sK1),sK2))))),
inference(forward_demodulation,[],[f15974,f431]) ).
fof(f15990,plain,
one != addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),addition(multiplication(sK0(sK2),sK1),addition(multiplication(c(sK1),sK2),multiplication(c(sK1),sK0(sK2)))))),
inference(forward_demodulation,[],[f15984,f29]) ).
fof(f15997,plain,
one != addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),addition(multiplication(sK0(sK2),sK1),multiplication(c(sK1),addition(sK2,sK0(sK2)))))),
inference(forward_demodulation,[],[f15990,f36]) ).
fof(f16002,plain,
one != addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),addition(multiplication(sK0(sK2),sK1),multiplication(c(sK1),one)))),
inference(forward_demodulation,[],[f15997,f93]) ).
fof(f16007,plain,
one != addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),addition(multiplication(sK0(sK2),sK1),c(sK1)))),
inference(forward_demodulation,[],[f16002,f34]) ).
fof(f16012,plain,
one != addition(multiplication(sK1,sK2),addition(c(sK1),addition(multiplication(sK2,sK1),multiplication(sK0(sK2),sK1)))),
inference(forward_demodulation,[],[f16007,f431]) ).
fof(f16017,plain,
one != addition(c(sK1),addition(addition(multiplication(sK2,sK1),multiplication(sK0(sK2),sK1)),multiplication(sK1,sK2))),
inference(forward_demodulation,[],[f16012,f431]) ).
fof(f16022,plain,
one != addition(c(sK1),addition(multiplication(sK1,sK2),addition(multiplication(sK2,sK1),multiplication(sK0(sK2),sK1)))),
inference(forward_demodulation,[],[f16017,f29]) ).
fof(f16025,plain,
one != addition(c(sK1),addition(multiplication(sK1,sK2),multiplication(addition(sK2,sK0(sK2)),sK1))),
inference(forward_demodulation,[],[f16022,f37]) ).
fof(f16028,plain,
one != addition(c(sK1),addition(multiplication(sK1,sK2),multiplication(one,sK1))),
inference(forward_demodulation,[],[f16025,f93]) ).
fof(f16030,plain,
one != addition(c(sK1),addition(multiplication(sK1,sK2),sK1)),
inference(forward_demodulation,[],[f16028,f35]) ).
fof(f16033,plain,
one != addition(sK1,addition(c(sK1),multiplication(sK1,sK2))),
inference(forward_demodulation,[],[f16030,f431]) ).
fof(f16034,plain,
one != addition(one,multiplication(sK1,sK2)),
inference(forward_demodulation,[],[f16033,f427]) ).
fof(f16035,plain,
( $false
| ~ spl3_88 ),
inference(forward_subsumption_resolution,[],[f16034,f13554]) ).
fof(f16036,plain,
~ spl3_88,
inference(avatar_contradiction_clause,[],[f16035]) ).
cnf(s137,plain,
( spl3_35
| ~ spl3_82 ),
inference(sat_conversion,[],[f3527]) ).
cnf(s185,plain,
( spl3_82
| spl3_88 ),
inference(sat_conversion,[],[f5118]) ).
cnf(s307,plain,
~ spl3_35,
inference(sat_conversion,[],[f11605]) ).
cnf(s374,plain,
~ spl3_88,
inference(sat_conversion,[],[f16036]) ).
cnf(s389,plain,
spl3_82,
inference(rat,[],[s185,s374]) ).
cnf(s398,plain,
$false,
inference(rat,[],[s137,s389,s307]) ).
fof(f16037,plain,
$false,
inference(avatar_sat_refutation,[],[s398]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE010+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 % Computer : n017.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sun Sep 27 12:53:50 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.42 Running first-order model finding
% 0.10/0.42 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
% 1.92/0.83 % (2526244)Will run a generic schedule for satisfiability detection.
% 1.92/0.83 % (2526252)dis+10_1_sil=32000:sp=arity:random_seed=1346026236:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.92/0.83 % (2526250)% WARNING: option uhcvi not known.
% 1.92/0.83 % (2526249)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3290804479_2999 on theBenchmark for (2999ds/0Mi)
% 1.92/0.83 % (2526254)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2670897620:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.92/0.83 % (2526250)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1909568703:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.92/0.83 % (2526251)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1743616858:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.92/0.83 % (2526253)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2538466973:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.92/0.83 % (2526255)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1972597429:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.92/0.83 % TRYING [1]
% 1.92/0.83 % TRYING [2]
% 1.92/0.83 % TRYING [3]
% 1.92/0.83 % TRYING [4]
% 1.92/0.83 % (2526252)Instruction limit reached!
% 1.92/0.83 % (2526252)------------------------------
% 1.92/0.83 % (2526252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/0.83 % (2526252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/0.83 % (2526252)CaDiCaL version: 2.1.3
% 1.92/0.83 % (2526252)Termination reason: Instruction limit
% 1.92/0.83 % (2526252)Termination phase: Saturation
% 1.92/0.83 % (2526252)Time elapsed: 0.032 s
% 1.92/0.83 % (2526252)Peak memory usage: 13 MB
% 1.92/0.83 % (2526252)Instructions burned: 103 (million)
% 1.92/0.83 % TRYING [5]
% 1.92/0.83 % (2526263)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1195262782:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.92/0.83 % TRYING [1]
% 1.92/0.83 % TRYING [2]
% 1.92/0.83 % TRYING [3]
% 1.92/0.83 % TRYING [4]
% 1.92/0.83 % TRYING [5]
% 1.92/0.83 % (2526253)Instruction limit reached!
% 1.92/0.83 % (2526253)------------------------------
% 1.92/0.83 % (2526253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/0.83 % (2526253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/0.83 % (2526253)CaDiCaL version: 2.1.3
% 1.92/0.83 % (2526253)Termination reason: Instruction limit
% 1.92/0.83 % (2526253)Termination phase: Saturation
% 1.92/0.83 % (2526253)Time elapsed: 0.068 s
% 1.92/0.83 % (2526253)Peak memory usage: 13 MB
% 1.92/0.83 % (2526253)Instructions burned: 117 (million)
% 1.92/0.83 % (2526254)Instruction limit reached!
% 1.92/0.83 % (2526254)------------------------------
% 1.92/0.83 % (2526254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/0.83 % (2526254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/0.83 % (2526254)CaDiCaL version: 2.1.3
% 1.92/0.83 % (2526254)Termination reason: Instruction limit
% 1.92/0.83 % (2526254)Termination phase: Saturation
% 1.92/0.83 % (2526254)Time elapsed: 0.071 s
% 1.92/0.83 % (2526254)Peak memory usage: 13 MB
% 1.92/0.83 % (2526254)Instructions burned: 131 (million)
% 1.92/0.83 % TRYING [6]
% 1.92/0.83 % (2526265)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=376842660:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.92/0.83 % (2526266)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=3551623559:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.92/0.83 % (2526255)Instruction limit reached!
% 1.92/0.83 % (2526255)------------------------------
% 1.92/0.83 % (2526255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/0.83 % (2526255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/0.83 % (2526255)CaDiCaL version: 2.1.3
% 1.92/0.83 % (2526255)Termination reason: Instruction limit
% 1.92/0.83 % (2526255)Termination phase: Saturation
% 1.92/0.83 % (2526255)Time elapsed: 0.102 s
% 1.92/0.83 % (2526255)Peak memory usage: 13 MB
% 1.92/0.83 % (2526255)Instructions burned: 160 (million)
% 1.92/0.83 % TRYING [6]
% 1.92/0.83 % (2526269)ott-21_1_sil=16000:fs=off:random_seed=3532426890:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.92/0.83 % (2526265)Instruction limit reached!
% 1.92/0.83 % (2526265)------------------------------
% 1.92/0.83 % (2526265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/0.83 % (2526265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/0.83 % (2526265)CaDiCaL version: 2.1.3
% 1.92/0.83 % (2526265)Termination reason: Instruction limit
% 1.92/0.83 % (2526265)Termination phase: Saturation
% 1.92/0.83 % (2526265)Time elapsed: 0.084 s
% 1.92/0.83 % (2526265)Peak memory usage: 13 MB
% 1.92/0.83 % (2526265)Instructions burned: 131 (million)
% 1.92/0.83 % (2526271)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4274265812:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.92/0.83 % (2526269)Instruction limit reached!
% 1.92/0.83 % (2526269)------------------------------
% 1.92/0.83 % (2526269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/0.83 % (2526269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/0.83 % (2526269)CaDiCaL version: 2.1.3
% 1.92/0.83 % (2526269)Termination reason: Instruction limit
% 1.92/0.83 % (2526269)Termination phase: Saturation
% 1.92/0.83 % (2526269)Time elapsed: 0.079 s
% 1.92/0.83 % (2526269)Peak memory usage: 12 MB
% 1.92/0.83 % (2526269)Instructions burned: 182 (million)
% 1.92/0.83 % TRYING [7]
% 1.92/0.83 % (2526263)Instruction limit reached!
% 1.92/0.83 % (2526263)------------------------------
% 1.92/0.83 % (2526263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/0.83 % (2526263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/0.83 % (2526263)CaDiCaL version: 2.1.3
% 1.92/0.83 % (2526263)Termination reason: Instruction limit
% 1.92/0.83 % (2526263)Termination phase: Finite model building constraint generation
% 1.92/0.83 % (2526263)Time elapsed: 0.172 s
% 1.92/0.83 % (2526263)Peak memory usage: 31 MB
% 1.92/0.83 % (2526263)Instructions burned: 717 (million)
% 1.92/0.83 % (2526274)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1893288428:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.92/0.83 % TRYING [7]
% 1.92/0.83 % (2526273)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=605495334:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.92/0.83 % TRYING [1]
% 1.92/0.83 % TRYING [2]
% 1.92/0.83 % TRYING [3]
% 1.92/0.83 % TRYING [4]
% 1.92/0.83 % TRYING [5]
% 1.92/0.83 % (2526266) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2526244-2526266"...
% 1.92/0.83 % (2526266)...printing done.
% 1.92/0.83 % (2526266)Refutation found. Thanks to Tanya!
% 1.92/0.83 % SZS status Theorem for theBenchmark
% 1.92/0.83 % SZS output start Proof for theBenchmark
% See solution above
% 1.92/0.83 % (2526266)------------------------------
% 1.92/0.83 % (2526266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/0.83 % (2526266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/0.83 % (2526266)CaDiCaL version: 2.1.3
% 1.92/0.83 % (2526266)Termination reason: Refutation
% 1.92/0.83 % (2526266)Time elapsed: 0.262 s
% 1.92/0.83 % (2526266)Peak memory usage: 17 MB
% 1.92/0.83 % (2526266)Instructions burned: 469 (million)
% 1.92/0.83 % (2526244)Success in time 0.4 s
% 1.92/0.83 % Vampire exiting
%------------------------------------------------------------------------------