%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ133+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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 12:32:32 PM UTC 2026
% Result : Theorem 114.58s 16.65s
% Output : Refutation 114.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 13
% Syntax : Number of formulae : 143 ( 36 unt; 3 def)
% Number of atoms : 396 ( 139 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 439 ( 186 ~; 181 |; 56 &)
% ( 8 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 6 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 151 ( 0 sgn 143 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( queens_p
=> ! [X0,X1] :
( ( le(s(n0),X0)
& le(X0,n)
& le(s(X0),X1)
& le(X1,n) )
=> ( p(X0) != p(X1)
& plus(p(X0),X0) != plus(p(X1),X1)
& minus(p(X0),X0) != minus(p(X1),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',queens_p) ).
fof(f2,axiom,
! [X0] : perm(X0) = minus(s(n),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',permutation) ).
fof(f3,axiom,
( ! [X0,X1] :
( ( le(s(n0),X0)
& le(X0,n)
& le(s(X0),X1)
& le(X1,n)
& ( le(s(X0),X1)
<=> le(s(perm(X1)),perm(X0)) ) )
=> ( q(X0) != q(X1)
& plus(q(X0),X0) != plus(q(X1),X1)
& minus(q(X0),X0) != minus(q(X1),X1) ) )
=> queens_q ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',queens_q) ).
fof(f4,conjecture,
( ( queens_p
& ! [X0] : q(X0) = p(perm(X0)) )
=> queens_q ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',queens_sym) ).
fof(f5,negated_conjecture,
~ ( ( queens_p
& ! [X0] : q(X0) = p(perm(X0)) )
=> queens_q ),
inference(negated_conjecture,[status(cth)],[f4]) ).
fof(f6,axiom,
! [X0] :
( ( le(s(n0),X0)
& le(X0,n) )
=> ( le(s(n0),perm(X0))
& le(perm(X0),n) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',permutation_range) ).
fof(f7,axiom,
! [X0,X1] : minus(X1,X0) = minus(perm(X0),perm(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',permutation_another_one) ).
fof(f8,axiom,
! [X0,X1,X2] :
( ( le(X0,X1)
& le(X1,X2) )
=> le(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',le_trans) ).
fof(f9,axiom,
! [X0] : le(X0,s(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_le) ).
fof(f10,axiom,
! [X0,X1,X2,X3] :
( plus(X0,X1) = plus(X2,X3)
<=> minus(X0,X2) = minus(X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1) ).
fof(f11,axiom,
! [X0,X1,X2,X3] :
( minus(X0,X1) = minus(X2,X3)
<=> minus(X0,X2) = minus(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minus1) ).
fof(f12,plain,
( ! [X0,X1] :
( ( p(X0) != p(X1)
& plus(p(X0),X0) != plus(p(X1),X1)
& minus(p(X0),X0) != minus(p(X1),X1) )
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n) )
| ~ queens_p ),
inference(ennf_transformation,[],[f1]) ).
fof(f13,plain,
( ! [X0,X1] :
( ( p(X0) != p(X1)
& plus(p(X0),X0) != plus(p(X1),X1)
& minus(p(X0),X0) != minus(p(X1),X1) )
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n) )
| ~ queens_p ),
inference(flattening,[],[f12]) ).
fof(f14,plain,
( queens_q
| ? [X0,X1] :
( ( q(X0) = q(X1)
| plus(q(X0),X0) = plus(q(X1),X1)
| minus(q(X0),X0) = minus(q(X1),X1) )
& le(s(n0),X0)
& le(X0,n)
& le(s(X0),X1)
& le(X1,n)
& ( le(s(X0),X1)
<=> le(s(perm(X1)),perm(X0)) ) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f15,plain,
( queens_q
| ? [X0,X1] :
( ( q(X0) = q(X1)
| plus(q(X0),X0) = plus(q(X1),X1)
| minus(q(X0),X0) = minus(q(X1),X1) )
& le(s(n0),X0)
& le(X0,n)
& le(s(X0),X1)
& le(X1,n)
& ( le(s(X0),X1)
<=> le(s(perm(X1)),perm(X0)) ) ) ),
inference(flattening,[],[f14]) ).
fof(f16,plain,
( ~ queens_q
& queens_p
& ! [X0] : q(X0) = p(perm(X0)) ),
inference(ennf_transformation,[],[f5]) ).
fof(f17,plain,
( ~ queens_q
& queens_p
& ! [X0] : q(X0) = p(perm(X0)) ),
inference(flattening,[],[f16]) ).
fof(f18,plain,
! [X0] :
( ( le(s(n0),perm(X0))
& le(perm(X0),n) )
| ~ le(s(n0),X0)
| ~ le(X0,n) ),
inference(ennf_transformation,[],[f6]) ).
fof(f19,plain,
! [X0] :
( ( le(s(n0),perm(X0))
& le(perm(X0),n) )
| ~ le(s(n0),X0)
| ~ le(X0,n) ),
inference(flattening,[],[f18]) ).
fof(f20,plain,
! [X0,X1,X2] :
( le(X0,X2)
| ~ le(X0,X1)
| ~ le(X1,X2) ),
inference(ennf_transformation,[],[f8]) ).
fof(f21,plain,
! [X0,X1,X2] :
( le(X0,X2)
| ~ le(X0,X1)
| ~ le(X1,X2) ),
inference(flattening,[],[f20]) ).
fof(f22,plain,
( queens_q
| ? [X0,X1] :
( ( q(X0) = q(X1)
| plus(q(X0),X0) = plus(q(X1),X1)
| minus(q(X0),X0) = minus(q(X1),X1) )
& le(s(n0),X0)
& le(X0,n)
& le(s(X0),X1)
& le(X1,n)
& ( le(s(X0),X1)
| ~ le(s(perm(X1)),perm(X0)) )
& ( le(s(perm(X1)),perm(X0))
| ~ le(s(X0),X1) ) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f23,plain,
( queens_q
| ? [X0,X1] :
( ( q(X0) = q(X1)
| plus(q(X0),X0) = plus(q(X1),X1)
| minus(q(X0),X0) = minus(q(X1),X1) )
& le(s(n0),X0)
& le(X0,n)
& le(s(X0),X1)
& le(X1,n)
& ( le(s(X0),X1)
| ~ le(s(perm(X1)),perm(X0)) )
& ( le(s(perm(X1)),perm(X0))
| ~ le(s(X0),X1) ) ) ),
inference(flattening,[],[f22]) ).
fof(f24,plain,
( queens_q
| ( ( q(sK0) = q(sK1)
| plus(q(sK0),sK0) = plus(q(sK1),sK1)
| minus(q(sK0),sK0) = minus(q(sK1),sK1) )
& le(s(n0),sK0)
& le(sK0,n)
& le(s(sK0),sK1)
& le(sK1,n)
& ( le(s(sK0),sK1)
| ~ le(s(perm(sK1)),perm(sK0)) )
& ( le(s(perm(sK1)),perm(sK0))
| ~ le(s(sK0),sK1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f23]) ).
fof(f25,plain,
! [X0,X1,X2,X3] :
( ( plus(X0,X1) = plus(X2,X3)
| minus(X0,X2) != minus(X3,X1) )
& ( minus(X0,X2) = minus(X3,X1)
| plus(X0,X1) != plus(X2,X3) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f26,plain,
! [X0,X1,X2,X3] :
( ( minus(X0,X1) = minus(X2,X3)
| minus(X0,X2) != minus(X1,X3) )
& ( minus(X0,X2) = minus(X1,X3)
| minus(X0,X1) != minus(X2,X3) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f27,plain,
! [X0,X1] :
( minus(p(X0),X0) != minus(p(X1),X1)
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n)
| ~ queens_p ),
inference(cnf_transformation,[],[f13]) ).
fof(f28,plain,
! [X0,X1] :
( plus(p(X0),X0) != plus(p(X1),X1)
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n)
| ~ queens_p ),
inference(cnf_transformation,[],[f13]) ).
fof(f29,plain,
! [X0,X1] :
( p(X0) != p(X1)
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n)
| ~ queens_p ),
inference(cnf_transformation,[],[f13]) ).
fof(f30,plain,
! [X0] : perm(X0) = minus(s(n),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f31,plain,
( queens_q
| le(s(perm(sK1)),perm(sK0))
| ~ le(s(sK0),sK1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f33,plain,
( queens_q
| le(sK1,n) ),
inference(cnf_transformation,[],[f24]) ).
fof(f34,plain,
( queens_q
| le(s(sK0),sK1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f35,plain,
( queens_q
| le(sK0,n) ),
inference(cnf_transformation,[],[f24]) ).
fof(f36,plain,
( queens_q
| le(s(n0),sK0) ),
inference(cnf_transformation,[],[f24]) ).
fof(f37,plain,
( queens_q
| q(sK0) = q(sK1)
| plus(q(sK0),sK0) = plus(q(sK1),sK1)
| minus(q(sK0),sK0) = minus(q(sK1),sK1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f38,plain,
! [X0] : q(X0) = p(perm(X0)),
inference(cnf_transformation,[],[f17]) ).
fof(f39,plain,
queens_p,
inference(cnf_transformation,[],[f17]) ).
fof(f40,plain,
~ queens_q,
inference(cnf_transformation,[],[f17]) ).
fof(f41,plain,
! [X0] :
( le(perm(X0),n)
| ~ le(s(n0),X0)
| ~ le(X0,n) ),
inference(cnf_transformation,[],[f19]) ).
fof(f42,plain,
! [X0] :
( le(s(n0),perm(X0))
| ~ le(s(n0),X0)
| ~ le(X0,n) ),
inference(cnf_transformation,[],[f19]) ).
fof(f43,plain,
! [X0,X1] : minus(X1,X0) = minus(perm(X0),perm(X1)),
inference(cnf_transformation,[],[f7]) ).
fof(f44,plain,
! [X2,X0,X1] :
( ~ le(X1,X2)
| ~ le(X0,X1)
| le(X0,X2) ),
inference(cnf_transformation,[],[f21]) ).
fof(f45,plain,
! [X0] : le(X0,s(X0)),
inference(cnf_transformation,[],[f9]) ).
fof(f46,plain,
! [X2,X3,X0,X1] :
( plus(X0,X1) != plus(X2,X3)
| minus(X0,X2) = minus(X3,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f47,plain,
! [X2,X3,X0,X1] :
( minus(X0,X2) != minus(X3,X1)
| plus(X0,X1) = plus(X2,X3) ),
inference(cnf_transformation,[],[f25]) ).
fof(f48,plain,
! [X2,X3,X0,X1] :
( minus(X0,X1) != minus(X2,X3)
| minus(X0,X2) = minus(X1,X3) ),
inference(cnf_transformation,[],[f26]) ).
fof(f50,plain,
! [X0] : q(X0) = p(minus(s(n),X0)),
inference(definition_unfolding,[],[f38,f30]) ).
fof(f51,plain,
( queens_q
| p(minus(s(n),sK0)) = p(minus(s(n),sK1))
| plus(p(minus(s(n),sK0)),sK0) = plus(p(minus(s(n),sK1)),sK1)
| minus(p(minus(s(n),sK0)),sK0) = minus(p(minus(s(n),sK1)),sK1) ),
inference(definition_unfolding,[],[f37,f50,f50,f50,f50,f50,f50]) ).
fof(f53,plain,
( queens_q
| le(s(minus(s(n),sK1)),minus(s(n),sK0))
| ~ le(s(sK0),sK1) ),
inference(definition_unfolding,[],[f31,f30,f30]) ).
fof(f54,plain,
! [X0] :
( ~ le(s(n0),X0)
| le(s(n0),minus(s(n),X0))
| ~ le(X0,n) ),
inference(definition_unfolding,[],[f42,f30]) ).
fof(f55,plain,
! [X0] :
( ~ le(s(n0),X0)
| le(minus(s(n),X0),n)
| ~ le(X0,n) ),
inference(definition_unfolding,[],[f41,f30]) ).
fof(f56,plain,
! [X0,X1] : minus(X1,X0) = minus(minus(s(n),X0),minus(s(n),X1)),
inference(definition_unfolding,[],[f43,f30,f30]) ).
fof(f57,plain,
le(sK1,n),
inference(forward_subsumption_resolution,[],[f33,f40]) ).
fof(f58,plain,
le(sK0,n),
inference(forward_subsumption_resolution,[],[f35,f40]) ).
fof(f59,plain,
( p(minus(s(n),sK0)) = p(minus(s(n),sK1))
| plus(p(minus(s(n),sK0)),sK0) = plus(p(minus(s(n),sK1)),sK1)
| minus(p(minus(s(n),sK0)),sK0) = minus(p(minus(s(n),sK1)),sK1) ),
inference(forward_subsumption_resolution,[],[f51,f40]) ).
fof(f61,definition,
( spl2_1
<=> minus(p(minus(s(n),sK0)),sK0) = minus(p(minus(s(n),sK1)),sK1) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f63,plain,
( minus(p(minus(s(n),sK0)),sK0) = minus(p(minus(s(n),sK1)),sK1)
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f61]) ).
fof(f65,definition,
( spl2_2
<=> plus(p(minus(s(n),sK0)),sK0) = plus(p(minus(s(n),sK1)),sK1) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f67,plain,
( plus(p(minus(s(n),sK0)),sK0) = plus(p(minus(s(n),sK1)),sK1)
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f65]) ).
fof(f69,definition,
( spl2_3
<=> p(minus(s(n),sK0)) = p(minus(s(n),sK1)) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
fof(f72,plain,
( spl2_1
| spl2_2
| spl2_3 ),
inference(avatar_split_clause,[],[f59,f69,f65,f61]) ).
fof(f73,plain,
le(s(sK0),sK1),
inference(forward_subsumption_resolution,[],[f34,f40]) ).
fof(f74,plain,
le(s(n0),sK0),
inference(forward_subsumption_resolution,[],[f36,f40]) ).
fof(f83,plain,
le(sK0,sK1),
inference(unit_resulting_resolution,[],[f44,f45,f73]) ).
fof(f94,plain,
le(s(n0),sK1),
inference(unit_resulting_resolution,[],[f44,f74,f83]) ).
fof(f218,plain,
le(minus(s(n),sK0),n),
inference(unit_resulting_resolution,[],[f55,f58,f74]) ).
fof(f219,plain,
le(minus(s(n),sK1),n),
inference(unit_resulting_resolution,[],[f55,f57,f94]) ).
fof(f377,plain,
! [X0,X1] : minus(X0,X1) = minus(minus(s(n),minus(s(n),X0)),minus(s(n),minus(s(n),X1))),
inference(superposition,[],[f56,f56]) ).
fof(f519,plain,
! [X0,X1] : minus(X0,X0) = minus(X1,X1),
inference(equality_resolution,[],[f46]) ).
fof(f617,plain,
! [X0,X1] : plus(X0,minus(s(n),X0)) = plus(X1,minus(s(n),X1)),
inference(unit_resulting_resolution,[],[f47,f56]) ).
fof(f620,plain,
! [X2,X3,X0,X1] :
( minus(X0,X1) != minus(X2,X3)
| plus(minus(s(n),X1),X3) = plus(minus(s(n),X0),X2) ),
inference(superposition,[],[f47,f56]) ).
fof(f622,plain,
! [X2,X3,X0,X1] :
( minus(X0,X1) != minus(X2,X3)
| plus(X2,minus(s(n),X0)) = plus(X3,minus(s(n),X1)) ),
inference(superposition,[],[f47,f56]) ).
fof(f623,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(equality_resolution,[],[f47]) ).
fof(f736,plain,
! [X0,X1] : minus(X0,minus(s(n),X1)) = minus(X1,minus(s(n),X0)),
inference(unit_resulting_resolution,[],[f48,f56]) ).
fof(f737,plain,
! [X0,X1] : minus(minus(s(n),X0),X1) = minus(minus(s(n),X1),X0),
inference(unit_resulting_resolution,[],[f48,f56]) ).
fof(f738,plain,
! [X2,X3,X0,X1] :
( minus(X2,X3) != minus(minus(s(n),X0),minus(s(n),X1))
| minus(X1,X2) = minus(X0,X3) ),
inference(superposition,[],[f48,f56]) ).
fof(f1350,plain,
le(s(n0),minus(s(n),sK1)),
inference(unit_resulting_resolution,[],[f54,f57,f94]) ).
fof(f2027,plain,
( le(s(minus(s(n),sK1)),minus(s(n),sK0))
| ~ le(s(sK0),sK1) ),
inference(forward_subsumption_resolution,[],[f53,f40]) ).
fof(f2028,plain,
le(s(minus(s(n),sK1)),minus(s(n),sK0)),
inference(forward_subsumption_resolution,[],[f2027,f73]) ).
fof(f2409,plain,
! [X0,X1] :
( p(X0) != p(X1)
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n) ),
inference(forward_subsumption_resolution,[],[f29,f39]) ).
fof(f3034,plain,
p(minus(s(n),sK0)) != p(minus(s(n),sK1)),
inference(unit_resulting_resolution,[],[f2409,f218,f2028,f219,f1350]) ).
fof(f3295,plain,
! [X0,X1] :
( minus(p(X0),X0) != minus(p(X1),X1)
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n) ),
inference(forward_subsumption_resolution,[],[f27,f39]) ).
fof(f3296,plain,
! [X0,X1] :
( minus(p(X0),X0) != minus(minus(s(n),X1),minus(s(n),p(X1)))
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n) ),
inference(forward_demodulation,[],[f3295,f56]) ).
fof(f3297,plain,
! [X0,X1] :
( minus(minus(s(n),X1),minus(s(n),p(X1))) != minus(minus(s(n),X0),minus(s(n),p(X0)))
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n) ),
inference(forward_demodulation,[],[f3296,f56]) ).
fof(f3408,plain,
~ spl2_3,
inference(avatar_split_clause,[],[f3034,f69]) ).
fof(f4032,plain,
! [X0,X1] :
( plus(p(X0),X0) != plus(p(X1),X1)
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n) ),
inference(forward_subsumption_resolution,[],[f28,f39]) ).
fof(f12412,plain,
! [X0,X1] :
( plus(p(X1),X1) != plus(X0,p(X0))
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n) ),
inference(superposition,[],[f4032,f623]) ).
fof(f12421,plain,
! [X0,X1] :
( plus(X0,p(X0)) != plus(X1,p(X1))
| ~ le(s(n0),X0)
| ~ le(X0,n)
| ~ le(s(X0),X1)
| ~ le(X1,n) ),
inference(forward_demodulation,[],[f12412,f623]) ).
fof(f13583,plain,
! [X0,X1] :
( minus(minus(s(n),X1),minus(s(n),p(X1))) != minus(minus(X0,minus(s(n),s(n))),minus(s(n),p(minus(s(n),X0))))
| ~ le(s(n0),X1)
| ~ le(X1,n)
| ~ le(s(X1),minus(s(n),X0))
| ~ le(minus(s(n),X0),n) ),
inference(superposition,[],[f3297,f736]) ).
fof(f76389,plain,
( minus(p(minus(s(n),sK0)),sK0) = minus(minus(s(n),sK1),minus(s(n),p(minus(s(n),sK1))))
| ~ spl2_1 ),
inference(forward_demodulation,[],[f63,f56]) ).
fof(f76391,plain,
( minus(minus(s(n),sK1),minus(s(n),p(minus(s(n),sK1)))) = minus(minus(s(n),sK0),minus(s(n),p(minus(s(n),sK0))))
| ~ spl2_1 ),
inference(forward_demodulation,[],[f76389,f56]) ).
fof(f77312,plain,
( minus(minus(s(n),p(minus(s(n),sK1))),minus(s(n),p(minus(s(n),sK0)))) = minus(minus(s(n),sK1),minus(s(n),sK0))
| ~ spl2_1 ),
inference(unit_resulting_resolution,[],[f48,f76391]) ).
fof(f77348,plain,
( minus(minus(s(n),p(minus(s(n),sK1))),minus(s(n),p(minus(s(n),sK0)))) = minus(minus(s(n),minus(s(n),sK0)),minus(s(n),minus(s(n),sK1)))
| ~ spl2_1 ),
inference(forward_demodulation,[],[f77312,f56]) ).
fof(f77358,plain,
( minus(sK0,sK1) = minus(minus(s(n),p(minus(s(n),sK1))),minus(s(n),p(minus(s(n),sK0))))
| ~ spl2_1 ),
inference(forward_demodulation,[],[f77348,f377]) ).
fof(f77365,plain,
( minus(sK0,sK1) = minus(minus(s(n),minus(s(n),p(minus(s(n),sK0)))),minus(s(n),minus(s(n),p(minus(s(n),sK1)))))
| ~ spl2_1 ),
inference(forward_demodulation,[],[f77358,f56]) ).
fof(f77368,plain,
( minus(p(minus(s(n),sK0)),p(minus(s(n),sK1))) = minus(sK0,sK1)
| ~ spl2_1 ),
inference(forward_demodulation,[],[f77365,f377]) ).
fof(f77379,plain,
( plus(minus(s(n),sK0),p(minus(s(n),sK0))) = plus(minus(s(n),sK1),p(minus(s(n),sK1)))
| ~ spl2_1 ),
inference(unit_resulting_resolution,[],[f620,f77368]) ).
fof(f105472,plain,
( ~ le(minus(s(n),sK0),n)
| ~ spl2_1 ),
inference(unit_resulting_resolution,[],[f12421,f219,f1350,f2028,f77379]) ).
fof(f105489,plain,
( $false
| ~ spl2_1 ),
inference(forward_subsumption_resolution,[],[f105472,f218]) ).
fof(f105490,plain,
~ spl2_1,
inference(avatar_contradiction_clause,[],[f105489]) ).
fof(f105496,plain,
( plus(p(minus(s(n),sK0)),sK0) = plus(sK1,p(minus(s(n),sK1)))
| ~ spl2_2 ),
inference(forward_demodulation,[],[f67,f623]) ).
fof(f105498,plain,
( plus(sK1,p(minus(s(n),sK1))) = plus(sK0,p(minus(s(n),sK0)))
| ~ spl2_2 ),
inference(forward_demodulation,[],[f105496,f623]) ).
fof(f107326,plain,
( minus(p(minus(s(n),sK0)),p(minus(s(n),sK1))) = minus(sK1,sK0)
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f46,f105498]) ).
fof(f107327,plain,
( minus(p(minus(s(n),sK1)),p(minus(s(n),sK0))) = minus(sK0,sK1)
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f46,f105498]) ).
fof(f107329,plain,
( ! [X0,X1] :
( plus(X0,X1) != plus(sK0,p(minus(s(n),sK0)))
| minus(p(minus(s(n),sK1)),X1) = minus(X0,sK1) )
| ~ spl2_2 ),
inference(superposition,[],[f46,f105498]) ).
fof(f107330,plain,
( minus(p(minus(s(n),sK0)),p(minus(s(n),sK1))) = minus(minus(s(n),sK0),minus(s(n),sK1))
| ~ spl2_2 ),
inference(forward_demodulation,[],[f107326,f56]) ).
fof(f107331,plain,
( minus(sK0,sK1) = minus(minus(s(n),p(minus(s(n),sK0))),minus(s(n),p(minus(s(n),sK1))))
| ~ spl2_2 ),
inference(forward_demodulation,[],[f107327,f56]) ).
fof(f110994,plain,
( plus(minus(s(n),minus(s(n),sK1)),p(minus(s(n),sK1))) = plus(minus(s(n),minus(s(n),sK0)),p(minus(s(n),sK0)))
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f620,f107330]) ).
fof(f110998,plain,
( ! [X0,X1] :
( minus(X0,X1) != minus(minus(s(n),sK0),minus(s(n),sK1))
| plus(p(minus(s(n),sK0)),X1) = plus(p(minus(s(n),sK1)),X0) )
| ~ spl2_2 ),
inference(superposition,[],[f47,f107330]) ).
fof(f111040,plain,
( minus(sK0,minus(s(n),p(minus(s(n),sK0)))) = minus(sK1,minus(s(n),p(minus(s(n),sK1))))
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f48,f107331]) ).
fof(f173778,plain,
( plus(p(minus(s(n),sK0)),sK0) = plus(p(minus(s(n),sK1)),minus(s(n),minus(s(n),sK1)))
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f110998,f737]) ).
fof(f173822,plain,
( plus(p(minus(s(n),sK0)),sK0) = plus(minus(s(n),minus(s(n),sK1)),p(minus(s(n),sK1)))
| ~ spl2_2 ),
inference(forward_demodulation,[],[f173778,f623]) ).
fof(f173834,plain,
( plus(p(minus(s(n),sK0)),sK0) = plus(minus(s(n),minus(s(n),sK0)),p(minus(s(n),sK0)))
| ~ spl2_2 ),
inference(forward_demodulation,[],[f173822,f110994]) ).
fof(f173841,plain,
( plus(sK0,p(minus(s(n),sK0))) = plus(minus(s(n),minus(s(n),sK0)),p(minus(s(n),sK0)))
| ~ spl2_2 ),
inference(forward_demodulation,[],[f173834,f623]) ).
fof(f173864,plain,
( plus(sK0,p(minus(s(n),sK0))) != plus(sK0,p(minus(s(n),sK0)))
| minus(p(minus(s(n),sK1)),p(minus(s(n),sK0))) = minus(minus(s(n),minus(s(n),sK0)),sK1)
| ~ spl2_2 ),
inference(superposition,[],[f107329,f173841]) ).
fof(f173869,plain,
( minus(p(minus(s(n),sK1)),p(minus(s(n),sK0))) = minus(minus(s(n),minus(s(n),sK0)),sK1)
| ~ spl2_2 ),
inference(trivial_inequality_removal,[],[f173864]) ).
fof(f173873,plain,
( minus(minus(s(n),p(minus(s(n),sK0))),minus(s(n),p(minus(s(n),sK1)))) = minus(minus(s(n),minus(s(n),sK0)),sK1)
| ~ spl2_2 ),
inference(forward_demodulation,[],[f173869,f56]) ).
fof(f173880,plain,
( minus(sK0,sK1) = minus(minus(s(n),minus(s(n),sK0)),sK1)
| ~ spl2_2 ),
inference(forward_demodulation,[],[f173873,f107331]) ).
fof(f173896,plain,
( plus(sK1,minus(s(n),sK1)) = plus(sK0,minus(s(n),minus(s(n),minus(s(n),sK0))))
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f622,f173880]) ).
fof(f173974,plain,
( ! [X0] : plus(X0,minus(s(n),X0)) = plus(sK0,minus(s(n),minus(s(n),minus(s(n),sK0))))
| ~ spl2_2 ),
inference(superposition,[],[f173896,f617]) ).
fof(f173994,plain,
( ! [X0] : minus(X0,sK0) = minus(minus(s(n),minus(s(n),minus(s(n),sK0))),minus(s(n),X0))
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f46,f173974]) ).
fof(f174103,plain,
( ! [X0] : minus(X0,sK0) = minus(X0,minus(s(n),minus(s(n),sK0)))
| ~ spl2_2 ),
inference(superposition,[],[f173994,f56]) ).
fof(f175481,plain,
( ! [X0] : minus(X0,sK0) = minus(minus(s(n),minus(s(n),X0)),sK0)
| ~ spl2_2 ),
inference(superposition,[],[f174103,f377]) ).
fof(f177588,plain,
( ! [X0] : minus(X0,minus(s(n),minus(s(n),X0))) = minus(sK0,sK0)
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f48,f175481]) ).
fof(f177600,plain,
( ! [X0] : minus(X0,sK0) = minus(minus(X0,minus(s(n),s(n))),sK0)
| ~ spl2_2 ),
inference(superposition,[],[f175481,f736]) ).
fof(f177789,plain,
( ! [X0,X1] : minus(X0,X0) = minus(X1,minus(s(n),minus(s(n),X1)))
| ~ spl2_2 ),
inference(superposition,[],[f177588,f519]) ).
fof(f178416,plain,
( ! [X0,X1] : minus(X1,sK0) = minus(minus(X1,minus(X0,X0)),sK0)
| ~ spl2_2 ),
inference(superposition,[],[f177600,f519]) ).
fof(f178490,plain,
( ! [X0,X1] : minus(sK0,sK0) = minus(X0,minus(X0,minus(X1,X1)))
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f48,f178416]) ).
fof(f178643,plain,
( ! [X2,X0,X1] : minus(X0,X0) = minus(X1,minus(X1,minus(X2,X2)))
| ~ spl2_2 ),
inference(superposition,[],[f178490,f519]) ).
fof(f180733,plain,
( ! [X2,X0,X1] : minus(X0,X1) = minus(minus(X0,minus(X2,X2)),X1)
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f48,f178643]) ).
fof(f196732,plain,
( ! [X0,X1] : minus(X0,X1) = minus(minus(s(n),minus(s(n),X0)),X1)
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f738,f177789]) ).
fof(f287328,plain,
( ! [X0,X1] :
( minus(minus(s(n),X1),minus(s(n),p(X1))) != minus(X0,minus(s(n),p(minus(s(n),X0))))
| ~ le(s(n0),X1)
| ~ le(X1,n)
| ~ le(s(X1),minus(s(n),X0))
| ~ le(minus(s(n),X0),n) )
| ~ spl2_2 ),
inference(forward_demodulation,[],[f13583,f180733]) ).
fof(f288077,plain,
( minus(minus(s(n),minus(s(n),sK1)),minus(s(n),p(minus(s(n),sK1)))) != minus(sK0,minus(s(n),p(minus(s(n),sK0))))
| ~ spl2_2 ),
inference(unit_resulting_resolution,[],[f287328,f218,f219,f1350,f2028]) ).
fof(f288203,plain,
( minus(sK0,minus(s(n),p(minus(s(n),sK0)))) != minus(sK1,minus(s(n),p(minus(s(n),sK1))))
| ~ spl2_2 ),
inference(forward_demodulation,[],[f288077,f196732]) ).
fof(f288240,plain,
( $false
| ~ spl2_2 ),
inference(forward_subsumption_resolution,[],[f288203,f111040]) ).
fof(f288241,plain,
~ spl2_2,
inference(avatar_contradiction_clause,[],[f288240]) ).
cnf(s1,plain,
( spl2_1
| spl2_2
| spl2_3 ),
inference(sat_conversion,[],[f72]) ).
cnf(s5,plain,
~ spl2_3,
inference(sat_conversion,[],[f3408]) ).
cnf(s18,plain,
~ spl2_1,
inference(sat_conversion,[],[f105490]) ).
cnf(s21,plain,
~ spl2_2,
inference(sat_conversion,[],[f288241]) ).
cnf(s22,plain,
$false,
inference(rat,[],[s1,s5,s21,s18]) ).
fof(f288268,plain,
$false,
inference(avatar_sat_refutation,[],[s22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ133+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n006.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 22:44:40 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/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
% 28.80/4.56 % (3401553)Will run a generic schedule for satisfiability detection.
% 28.80/4.56 % (3401561)dis+10_1_sil=32000:sp=arity:random_seed=2818526675:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 28.80/4.56 % (3401559)% WARNING: option uhcvi not known.
% 28.80/4.56 % (3401558)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2916057356_2999 on theBenchmark for (2999ds/0Mi)
% 28.80/4.56 % (3401559)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2603896647:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 28.80/4.56 % (3401560)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1670908511:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 28.80/4.56 % (3401562)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4006604247:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 28.80/4.56 % TRYING [1]
% 28.80/4.56 % TRYING [2]
% 28.80/4.56 % (3401563)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4162395733:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 28.80/4.56 % TRYING [3]
% 28.80/4.56 % (3401564)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3045696608:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 28.80/4.56 % TRYING [4]
% 28.80/4.56 % (3401561)Instruction limit reached!
% 28.80/4.56 % (3401561)------------------------------
% 28.80/4.56 % (3401561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.80/4.56 % (3401561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.80/4.56 % (3401561)CaDiCaL version: 2.1.3
% 28.80/4.56 % (3401561)Termination reason: Instruction limit
% 28.80/4.56 % (3401561)Termination phase: Saturation
% 28.80/4.56 % (3401561)Time elapsed: 0.031 s
% 28.80/4.56 % (3401561)Peak memory usage: 12 MB
% 28.80/4.56 % (3401561)Instructions burned: 104 (million)
% 28.80/4.56 % (3401572)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4281726905:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 28.80/4.56 % TRYING [1]
% 28.80/4.56 % TRYING [2]
% 28.80/4.56 % TRYING [3]
% 28.80/4.56 % TRYING [4]
% 28.80/4.56 % (3401562)Instruction limit reached!
% 28.80/4.56 % (3401562)------------------------------
% 28.80/4.56 % (3401562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.80/4.56 % (3401562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.80/4.56 % (3401562)CaDiCaL version: 2.1.3
% 28.80/4.56 % (3401562)Termination reason: Instruction limit
% 28.80/4.56 % (3401562)Termination phase: Saturation
% 28.80/4.56 % (3401562)Time elapsed: 0.067 s
% 28.80/4.56 % (3401562)Peak memory usage: 12 MB
% 28.80/4.56 % (3401562)Instructions burned: 119 (million)
% 28.80/4.56 % (3401563)Instruction limit reached!
% 28.80/4.56 % (3401563)------------------------------
% 28.80/4.56 % (3401563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.80/4.56 % (3401563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.80/4.56 % (3401563)CaDiCaL version: 2.1.3
% 28.80/4.56 % (3401563)Termination reason: Instruction limit
% 28.80/4.56 % (3401563)Termination phase: Saturation
% 28.80/4.56 % (3401563)Time elapsed: 0.073 s
% 28.80/4.56 % (3401563)Peak memory usage: 12 MB
% 28.80/4.56 % (3401563)Instructions burned: 133 (million)
% 28.80/4.56 % TRYING [5]
% 28.80/4.56 % (3401574)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3774838091:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 28.80/4.56 % (3401575)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=451133945:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 28.80/4.56 % TRYING [5]
% 28.80/4.56 % (3401574)Instruction limit reached!
% 28.80/4.56 % (3401574)------------------------------
% 28.80/4.56 % (3401574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.80/4.56 % (3401574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.80/4.56 % (3401574)CaDiCaL version: 2.1.3
% 28.80/4.56 % (3401574)Termination reason: Instruction limit
% 28.80/4.56 % (3401574)Termination phase: Saturation
% 28.80/4.56 % (3401574)Time elapsed: 0.072 s
% 28.80/4.56 % (3401574)Peak memory usage: 12 MB
% 28.80/4.56 % (3401574)Instructions burned: 132 (million)
% 28.80/4.56 % (3401564)Instruction limit reached!
% 28.80/4.56 % (3401564)------------------------------
% 28.80/4.56 % (3401564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.80/4.56 % (3401564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.56/8.18 % (3401564)CaDiCaL version: 2.1.3
% 54.56/8.18 % (3401564)Termination reason: Instruction limit
% 54.56/8.18 % (3401564)Termination phase: Saturation
% 54.56/8.18 % (3401564)Time elapsed: 0.160 s
% 54.56/8.18 % (3401564)Peak memory usage: 12 MB
% 54.56/8.18 % (3401564)Instructions burned: 159 (million)
% 54.56/8.18 % (3401578)ott-21_1_sil=16000:fs=off:random_seed=1311229266:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 54.56/8.18 % (3401579)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=777272228:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 54.56/8.18 % (3401572)Instruction limit reached!
% 54.56/8.18 % (3401572)------------------------------
% 54.56/8.18 % (3401572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.56/8.18 % (3401572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.56/8.18 % (3401572)CaDiCaL version: 2.1.3
% 54.56/8.18 % (3401572)Termination reason: Instruction limit
% 54.56/8.18 % (3401572)Termination phase: Finite model building SAT solving
% 54.56/8.18 % (3401572)Time elapsed: 0.224 s
% 54.56/8.18 % (3401572)Peak memory usage: 19 MB
% 54.56/8.18 % (3401572)Instructions burned: 715 (million)
% 54.56/8.18 % (3401578)Instruction limit reached!
% 54.56/8.18 % (3401578)------------------------------
% 54.56/8.18 % (3401578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.56/8.18 % (3401578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.56/8.18 % (3401578)CaDiCaL version: 2.1.3
% 54.56/8.18 % (3401578)Termination reason: Instruction limit
% 54.56/8.18 % (3401578)Termination phase: Saturation
% 54.56/8.18 % (3401578)Time elapsed: 0.077 s
% 54.56/8.18 % (3401578)Peak memory usage: 11 MB
% 54.56/8.18 % (3401578)Instructions burned: 180 (million)
% 54.56/8.18 % (3401582)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2555632601:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 54.56/8.18 % TRYING [1]
% 54.56/8.18 % TRYING [2]
% 54.56/8.18 % TRYING [3]
% 54.56/8.18 % (3401583)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=578648818:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 54.56/8.18 % TRYING [4]
% 54.56/8.18 % TRYING [5]
% 54.56/8.18 % (3401575)Instruction limit reached!
% 54.56/8.18 % (3401575)------------------------------
% 54.56/8.18 % (3401575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.56/8.18 % (3401575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.56/8.18 % (3401575)CaDiCaL version: 2.1.3
% 54.56/8.18 % (3401575)Termination reason: Instruction limit
% 54.56/8.18 % (3401575)Termination phase: Saturation
% 54.56/8.18 % (3401575)Time elapsed: 0.323 s
% 54.56/8.18 % (3401575)Peak memory usage: 14 MB
% 54.56/8.18 % (3401575)Instructions burned: 686 (million)
% 54.56/8.18 % (3401591)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2069637078:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 54.56/8.18 % (3401579)Instruction limit reached!
% 54.56/8.18 % (3401579)------------------------------
% 54.56/8.18 % (3401579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.56/8.18 % (3401579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.56/8.18 % (3401579)CaDiCaL version: 2.1.3
% 54.56/8.18 % (3401579)Termination reason: Instruction limit
% 54.56/8.18 % (3401579)Termination phase: Saturation
% 54.56/8.18 % (3401579)Time elapsed: 0.290 s
% 54.56/8.18 % (3401579)Peak memory usage: 14 MB
% 54.56/8.18 % (3401579)Instructions burned: 478 (million)
% 54.56/8.18 % (3401596)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=1874612074:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 54.56/8.18 % (3401582)Instruction limit reached!
% 54.56/8.18 % (3401582)------------------------------
% 54.56/8.18 % (3401582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.56/8.18 % (3401582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.56/8.18 % (3401582)CaDiCaL version: 2.1.3
% 54.56/8.18 % (3401582)Termination reason: Instruction limit
% 54.56/8.18 % (3401582)Termination phase: Finite model building SAT solving
% 54.56/8.18 % (3401582)Time elapsed: 0.242 s
% 54.56/8.18 % (3401582)Peak memory usage: 16 MB
% 54.56/8.18 % (3401582)Instructions burned: 865 (million)
% 54.56/8.18 % (3401598)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1015541685:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 54.56/8.18 % TRYING [14]
% 54.56/8.18 % (3401598)Instruction limit reached!
% 54.56/8.18 % (3401598)------------------------------
% 114.58/16.60 % (3401598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.60 % (3401598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.60 % (3401598)CaDiCaL version: 2.1.3
% 114.58/16.60 % (3401598)Termination reason: Instruction limit
% 114.58/16.60 % (3401598)Termination phase: Saturation
% 114.58/16.60 % (3401598)Time elapsed: 0.440 s
% 114.58/16.60 % (3401598)Peak memory usage: 15 MB
% 114.58/16.60 % (3401598)Instructions burned: 879 (million)
% 114.58/16.60 % (3401611)fmb+10_1_sil=64000:random_seed=2671323733:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 114.58/16.60 % TRYING [1]
% 114.58/16.60 % TRYING [2]
% 114.58/16.60 % TRYING [3]
% 114.58/16.60 % (3401591)Instruction limit reached!
% 114.58/16.60 % (3401591)------------------------------
% 114.58/16.60 % (3401591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.60 % (3401591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.60 % (3401591)CaDiCaL version: 2.1.3
% 114.58/16.60 % (3401591)Termination reason: Instruction limit
% 114.58/16.60 % (3401591)Termination phase: Finite model building constraint generation
% 114.58/16.60 % (3401591)Time elapsed: 0.554 s
% 114.58/16.60 % (3401591)Peak memory usage: 78 MB
% 114.58/16.60 % (3401591)Instructions burned: 890 (million)
% 114.58/16.60 % TRYING [4]
% 114.58/16.60 % (3401613)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=770506725:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 114.58/16.60 % TRYING [20]
% 114.58/16.60 % TRYING [5]
% 114.58/16.60 % (3401596)Instruction limit reached!
% 114.58/16.60 % (3401596)------------------------------
% 114.58/16.60 % (3401596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.60 % (3401596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.60 % (3401596)CaDiCaL version: 2.1.3
% 114.58/16.60 % (3401596)Termination reason: Instruction limit
% 114.58/16.60 % (3401596)Termination phase: Saturation
% 114.58/16.60 % (3401596)Time elapsed: 0.605 s
% 114.58/16.60 % (3401596)Peak memory usage: 15 MB
% 114.58/16.60 % (3401596)Instructions burned: 693 (million)
% 114.58/16.60 % (3401617)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2620005366:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 114.58/16.60 % TRYING [8]
% 114.58/16.60 % (3401583)Instruction limit reached!
% 114.58/16.60 % (3401583)------------------------------
% 114.58/16.60 % (3401583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.60 % (3401583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.60 % (3401583)CaDiCaL version: 2.1.3
% 114.58/16.60 % (3401583)Termination reason: Instruction limit
% 114.58/16.60 % (3401583)Termination phase: Saturation
% 114.58/16.60 % (3401583)Time elapsed: 0.970 s
% 114.58/16.60 % (3401583)Peak memory usage: 16 MB
% 114.58/16.60 % (3401583)Instructions burned: 1179 (million)
% 114.58/16.60 % (3401622)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3700801824:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 114.58/16.60 % (3401617)Instruction limit reached!
% 114.58/16.60 % (3401617)------------------------------
% 114.58/16.60 % (3401617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.60 % (3401617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.60 % (3401617)CaDiCaL version: 2.1.3
% 114.58/16.60 % (3401617)Termination reason: Instruction limit
% 114.58/16.60 % (3401617)Termination phase: Finite model building SAT solving
% 114.58/16.60 % (3401617)Time elapsed: 0.741 s
% 114.58/16.60 % (3401617)Peak memory usage: 66 MB
% 114.58/16.60 % (3401617)Instructions burned: 920 (million)
% 114.58/16.60 % (3401632)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1835155206:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi)
% 114.58/16.60 % TRYING [6]
% 114.58/16.60 % (3401632)Instruction limit reached!
% 114.58/16.60 % (3401632)------------------------------
% 114.58/16.60 % (3401632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.60 % (3401632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.60 % (3401632)CaDiCaL version: 2.1.3
% 114.58/16.60 % (3401632)Termination reason: Instruction limit
% 114.58/16.60 % (3401632)Termination phase: Saturation
% 114.58/16.60 % (3401632)Time elapsed: 0.952 s
% 114.58/16.60 % (3401632)Peak memory usage: 29 MB
% 114.58/16.60 % (3401632)Instructions burned: 1473 (million)
% 114.58/16.60 % (3401674)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=651460438:i=6324_2970 on theBenchmark for (2970ds/6324Mi)
% 114.58/16.60 % TRYING [77]
% 114.58/16.60 % (3401622)Instruction limit reached!
% 114.58/16.65 % (3401622)------------------------------
% 114.58/16.65 % (3401622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401622)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401622)Termination reason: Instruction limit
% 114.58/16.65 % (3401622)Termination phase: Saturation
% 114.58/16.65 % (3401622)Time elapsed: 2.825 s
% 114.58/16.65 % (3401622)Peak memory usage: 27 MB
% 114.58/16.65 % (3401622)Instructions burned: 5131 (million)
% 114.58/16.65 % (3401676)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2469677666:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi)
% 114.58/16.65 % TRYING [16]
% 114.58/16.65 % TRYING [6]
% 114.58/16.65 % (3401676)Instruction limit reached!
% 114.58/16.65 % (3401676)------------------------------
% 114.58/16.65 % (3401676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401676)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401676)Termination reason: Instruction limit
% 114.58/16.65 % (3401676)Termination phase: Finite model building constraint generation
% 114.58/16.65 % (3401676)Time elapsed: 0.740 s
% 114.58/16.65 % (3401676)Peak memory usage: 133 MB
% 114.58/16.65 % (3401676)Instructions burned: 2176 (million)
% 114.58/16.65 % (3401613)Instruction limit reached!
% 114.58/16.65 % (3401613)------------------------------
% 114.58/16.65 % (3401613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401613)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401613)Termination reason: Instruction limit
% 114.58/16.65 % (3401613)Termination phase: Finite model building constraint generation
% 114.58/16.65 % (3401613)Time elapsed: 3.827 s
% 114.58/16.65 % (3401613)Peak memory usage: 671 MB
% 114.58/16.65 % (3401613)Instructions burned: 9517 (million)
% 114.58/16.65 % (3401678)ott-2_1_sil=16000:newcnf=on:random_seed=675532332:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2950 on theBenchmark for (2950ds/869Mi)
% 114.58/16.65 % (3401680)ott+10_1_sil=32000:tgt=ground:random_seed=1498181091:i=5114:av=off_2949 on theBenchmark for (2949ds/5114Mi)
% 114.58/16.65 % (3401674)Instruction limit reached!
% 114.58/16.65 % (3401674)------------------------------
% 114.58/16.65 % (3401674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401674)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401674)Termination reason: Instruction limit
% 114.58/16.65 % (3401674)Termination phase: Finite model building constraint generation
% 114.58/16.65 % (3401674)Time elapsed: 2.311 s
% 114.58/16.65 % (3401674)Peak memory usage: 415 MB
% 114.58/16.65 % (3401674)Instructions burned: 6324 (million)
% 114.58/16.65 % (3401712)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1827208777:i=54282_2947 on theBenchmark for (2947ds/54282Mi)
% 114.58/16.65 % TRYING [1]
% 114.58/16.65 % TRYING [2]
% 114.58/16.65 % TRYING [3]
% 114.58/16.65 % TRYING [4]
% 114.58/16.65 % TRYING [5]
% 114.58/16.65 % (3401678)Instruction limit reached!
% 114.58/16.65 % (3401678)------------------------------
% 114.58/16.65 % (3401678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401678)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401678)Termination reason: Instruction limit
% 114.58/16.65 % (3401678)Termination phase: Saturation
% 114.58/16.65 % (3401678)Time elapsed: 0.503 s
% 114.58/16.65 % (3401678)Peak memory usage: 15 MB
% 114.58/16.65 % (3401678)Instructions burned: 870 (million)
% 114.58/16.65 % (3401750)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=750760510:i=3512:aac=none_2945 on theBenchmark for (2945ds/3512Mi)
% 114.58/16.65 % (3401750)Instruction limit reached!
% 114.58/16.65 % (3401750)------------------------------
% 114.58/16.65 % (3401750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401750)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401750)Termination reason: Instruction limit
% 114.58/16.65 % (3401750)Termination phase: Saturation
% 114.58/16.65 % (3401750)Time elapsed: 1.804 s
% 114.58/16.65 % (3401750)Peak memory usage: 27 MB
% 114.58/16.65 % (3401750)Instructions burned: 3513 (million)
% 114.58/16.65 % (3401799)dis+21_1_sil=32000:sas=cadical:random_seed=4197710020:i=3773:amm=off_2927 on theBenchmark for (2927ds/3773Mi)
% 114.58/16.65 % (3401680)Instruction limit reached!
% 114.58/16.65 % (3401680)------------------------------
% 114.58/16.65 % (3401680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401680)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401680)Termination reason: Instruction limit
% 114.58/16.65 % (3401680)Termination phase: Saturation
% 114.58/16.65 % (3401680)Time elapsed: 2.727 s
% 114.58/16.65 % (3401680)Peak memory usage: 25 MB
% 114.58/16.65 % (3401680)Instructions burned: 5115 (million)
% 114.58/16.65 % (3401801)ott+11_1_sil=16000:gs=on:random_seed=1722043342:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2922 on theBenchmark for (2922ds/2251Mi)
% 114.58/16.65 % (3401611)Instruction limit reached!
% 114.58/16.65 % (3401611)------------------------------
% 114.58/16.65 % (3401611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401611)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401611)Termination reason: Instruction limit
% 114.58/16.65 % (3401611)Termination phase: Finite model building SAT solving
% 114.58/16.65 % (3401611)Time elapsed: 7.637 s
% 114.58/16.65 % (3401611)Peak memory usage: 33 MB
% 114.58/16.65 % (3401611)Instructions burned: 22063 (million)
% 114.58/16.65 % TRYING [6]
% 114.58/16.65 % (3401803)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=929686286:fmbsr=1.6:i=67534_2913 on theBenchmark for (2913ds/67534Mi)
% 114.58/16.65 % TRYING [7]
% 114.58/16.65 % (3401801)Instruction limit reached!
% 114.58/16.65 % (3401801)------------------------------
% 114.58/16.65 % (3401801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401801)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401801)Termination reason: Instruction limit
% 114.58/16.65 % (3401801)Termination phase: Saturation
% 114.58/16.65 % (3401801)Time elapsed: 1.080 s
% 114.58/16.65 % (3401801)Peak memory usage: 16 MB
% 114.58/16.65 % (3401801)Instructions burned: 2253 (million)
% 114.58/16.65 % (3401805)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1888250797:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2911 on theBenchmark for (2911ds/4591Mi)
% 114.58/16.65 % (3401799)Instruction limit reached!
% 114.58/16.65 % (3401799)------------------------------
% 114.58/16.65 % (3401799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401799)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401799)Termination reason: Instruction limit
% 114.58/16.65 % (3401799)Termination phase: Saturation
% 114.58/16.65 % (3401799)Time elapsed: 2.040 s
% 114.58/16.65 % (3401799)Peak memory usage: 30 MB
% 114.58/16.65 % (3401799)Instructions burned: 3773 (million)
% 114.58/16.65 % (3401807)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1174479207:i=29340_2906 on theBenchmark for (2906ds/29340Mi)
% 114.58/16.65 % (3401805)Instruction limit reached!
% 114.58/16.65 % (3401805)------------------------------
% 114.58/16.65 % (3401805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401805)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401805)Termination reason: Instruction limit
% 114.58/16.65 % (3401805)Termination phase: Saturation
% 114.58/16.65 % (3401805)Time elapsed: 2.813 s
% 114.58/16.65 % (3401805)Peak memory usage: 40 MB
% 114.58/16.65 % (3401805)Instructions burned: 4591 (million)
% 114.58/16.65 % (3401809)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=866943250:i=5211_2883 on theBenchmark for (2883ds/5211Mi)
% 114.58/16.65 % (3401809)Instruction limit reached!
% 114.58/16.65 % (3401809)------------------------------
% 114.58/16.65 % (3401809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.65 % (3401809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.65 % (3401809)CaDiCaL version: 2.1.3
% 114.58/16.65 % (3401809)Termination reason: Instruction limit
% 114.58/16.65 % (3401809)Termination phase: Saturation
% 114.58/16.65 % (3401809)Time elapsed: 2.704 s
% 114.58/16.65 % (3401809)Peak memory usage: 38 MB
% 114.58/16.65 % (3401809)Instructions burned: 5213 (million)
% 114.58/16.65 % (3401956)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=277366996:i=5497:nm=2_2855 on theBenchmark for (2855ds/5497Mi)
% 114.58/16.65 % TRYING [17]
% 114.58/16.65 % (3401807) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3401553-3401807"...
% 114.58/16.65 % (3401807)...printing done.
% 114.58/16.65 % (3401807)Refutation found. Thanks to Tanya!
% 114.58/16.65 % SZS status Theorem for theBenchmark
% 114.58/16.65 % SZS output start Proof for theBenchmark
% See solution above
% 114.58/16.66 % (3401807)------------------------------
% 114.58/16.66 % (3401807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.58/16.66 % (3401807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.58/16.66 % (3401807)CaDiCaL version: 2.1.3
% 114.58/16.66 % (3401807)Termination reason: Refutation
% 114.58/16.66 % (3401807)Time elapsed: 6.828 s
% 114.58/16.66 % (3401807)Peak memory usage: 56 MB
% 114.58/16.66 % (3401807)Instructions burned: 12970 (million)
% 114.58/16.66 % (3401553)Success in time 16.229 s
% 114.58/16.66 % Vampire exiting
%------------------------------------------------------------------------------