%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : MGT063+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:02:47 PM UTC 2026
% Result : Theorem 0.15s 15.60s
% Output : Refutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 46
% Syntax : Number of formulae : 356 ( 76 unt; 31 def)
% Number of atoms : 926 ( 101 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 939 ( 369 ~; 439 |; 72 &)
% ( 40 <=>; 18 =>; 0 <=; 1 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 43 ( 41 usr; 32 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 197 ( 0 sgn 187 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( smaller_or_equal(X0,X1)
<=> ( smaller(X0,X1)
| X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax',definition_smaller_or_equal) ).
fof(f3,axiom,
! [X0,X1] :
( smaller(X0,X1)
<=> greater(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax',definition_smaller) ).
fof(f4,axiom,
! [X0,X1] :
~ ( greater(X0,X1)
& greater(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax',meaning_postulate_greater_strict) ).
fof(f5,axiom,
! [X0,X1,X2] :
( ( greater(X0,X1)
& greater(X1,X2) )
=> greater(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax',meaning_postulate_greater_transitive) ).
fof(f6,axiom,
! [X0,X1] :
( smaller(X0,X1)
| X0 = X1
| greater(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax',meaning_postulate_greater_comparable) ).
fof(f8,axiom,
! [X0,X1] :
( ( organization(X0)
& ~ has_endowment(X0) )
=> ~ has_immunity(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_1) ).
fof(f9,axiom,
! [X0,X1,X2] :
( dissimilar(X0,X1,X2)
<=> ( organization(X0)
& ~ ( is_aligned(X0,X1)
<=> is_aligned(X0,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_2) ).
fof(f10,axiom,
! [X0,X1] :
( ( organization(X0)
& age(X0,X1) = zero )
=> is_aligned(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_13) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( organization(X0)
& age(X0,X1) = zero )
=> ( greater(age(X0,X2),sigma)
<=> dissimilar(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_15) ).
fof(f12,axiom,
! [X0] :
( robust_position(X0)
<=> ! [X1] :
( ( smaller_or_equal(age(X0,X1),tau)
=> ~ positional_advantage(X0,X1) )
& ( greater(age(X0,X1),tau)
=> positional_advantage(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_4) ).
fof(f13,axiom,
! [X0,X1] :
( organization(X0)
=> ( ( has_immunity(X0,X1)
=> hazard_of_mortality(X0,X1) = very_low )
& ( ~ has_immunity(X0,X1)
=> ( ( ( is_aligned(X0,X1)
& positional_advantage(X0,X1) )
=> hazard_of_mortality(X0,X1) = low )
& ( ( ~ is_aligned(X0,X1)
& positional_advantage(X0,X1) )
=> hazard_of_mortality(X0,X1) = mod1 )
& ( ( is_aligned(X0,X1)
& ~ positional_advantage(X0,X1) )
=> hazard_of_mortality(X0,X1) = mod2 )
& ( ( ~ is_aligned(X0,X1)
& ~ positional_advantage(X0,X1) )
=> hazard_of_mortality(X0,X1) = high ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_17) ).
fof(f15,axiom,
greater(mod1,low),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_18b) ).
fof(f17,axiom,
greater(high,mod2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_18d) ).
fof(f19,axiom,
greater(mod2,mod1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_19) ).
fof(f20,conjecture,
! [X0,X1,X2,X3,X4] :
( ( organization(X0)
& robust_position(X0)
& ~ has_endowment(X0)
& age(X0,X1) = zero
& greater(sigma,zero)
& greater(tau,zero)
& smaller(sigma,tau)
& smaller_or_equal(age(X0,X2),sigma)
& greater(age(X0,X3),sigma)
& smaller_or_equal(age(X0,X3),tau)
& greater(age(X0,X4),tau) )
=> ( smaller(hazard_of_mortality(X0,X4),hazard_of_mortality(X0,X2))
& smaller(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X3))
& hazard_of_mortality(X0,X2) = hazard_of_mortality(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_9) ).
fof(f21,negated_conjecture,
~ ! [X0,X1,X2,X3,X4] :
( ( organization(X0)
& robust_position(X0)
& ~ has_endowment(X0)
& age(X0,X1) = zero
& greater(sigma,zero)
& greater(tau,zero)
& smaller(sigma,tau)
& smaller_or_equal(age(X0,X2),sigma)
& greater(age(X0,X3),sigma)
& smaller_or_equal(age(X0,X3),tau)
& greater(age(X0,X4),tau) )
=> ( smaller(hazard_of_mortality(X0,X4),hazard_of_mortality(X0,X2))
& smaller(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X3))
& hazard_of_mortality(X0,X2) = hazard_of_mortality(X0,X1) ) ),
inference(negated_conjecture,[status(cth)],[f20]) ).
fof(f22,plain,
! [X0] :
( robust_position(X0)
=> ! [X1] :
( ( smaller_or_equal(age(X0,X1),tau)
=> ~ positional_advantage(X0,X1) )
& ( greater(age(X0,X1),tau)
=> positional_advantage(X0,X1) ) ) ),
inference(unused_predicate_definition_removal,[],[f12]) ).
fof(f23,plain,
! [X0,X1] :
( ~ greater(X0,X1)
| ~ greater(X1,X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f24,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(ennf_transformation,[],[f5]) ).
fof(f25,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(flattening,[],[f24]) ).
fof(f27,plain,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| ~ organization(X0)
| has_endowment(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f28,plain,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| ~ organization(X0)
| has_endowment(X0) ),
inference(flattening,[],[f27]) ).
fof(f29,plain,
! [X0,X1,X2] :
( dissimilar(X0,X1,X2)
<=> ( organization(X0)
& ( is_aligned(X0,X1)
<~> is_aligned(X0,X2) ) ) ),
inference(ennf_transformation,[],[f9]) ).
fof(f30,plain,
! [X0,X1] :
( is_aligned(X0,X1)
| ~ organization(X0)
| age(X0,X1) != zero ),
inference(ennf_transformation,[],[f10]) ).
fof(f31,plain,
! [X0,X1] :
( is_aligned(X0,X1)
| ~ organization(X0)
| age(X0,X1) != zero ),
inference(flattening,[],[f30]) ).
fof(f32,plain,
! [X0,X1,X2] :
( ( greater(age(X0,X2),sigma)
<=> dissimilar(X0,X1,X2) )
| ~ organization(X0)
| age(X0,X1) != zero ),
inference(ennf_transformation,[],[f11]) ).
fof(f33,plain,
! [X0,X1,X2] :
( ( greater(age(X0,X2),sigma)
<=> dissimilar(X0,X1,X2) )
| ~ organization(X0)
| age(X0,X1) != zero ),
inference(flattening,[],[f32]) ).
fof(f34,plain,
! [X0] :
( ! [X1] :
( ( ~ positional_advantage(X0,X1)
| ~ smaller_or_equal(age(X0,X1),tau) )
& ( positional_advantage(X0,X1)
| ~ greater(age(X0,X1),tau) ) )
| ~ robust_position(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f35,plain,
! [X0,X1] :
( ( ( hazard_of_mortality(X0,X1) = very_low
| ~ has_immunity(X0,X1) )
& ( ( ( hazard_of_mortality(X0,X1) = low
| ~ is_aligned(X0,X1)
| ~ positional_advantage(X0,X1) )
& ( hazard_of_mortality(X0,X1) = mod1
| is_aligned(X0,X1)
| ~ positional_advantage(X0,X1) )
& ( hazard_of_mortality(X0,X1) = mod2
| ~ is_aligned(X0,X1)
| positional_advantage(X0,X1) )
& ( hazard_of_mortality(X0,X1) = high
| is_aligned(X0,X1)
| positional_advantage(X0,X1) ) )
| has_immunity(X0,X1) ) )
| ~ organization(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f36,plain,
! [X0,X1] :
( ( ( hazard_of_mortality(X0,X1) = very_low
| ~ has_immunity(X0,X1) )
& ( ( ( hazard_of_mortality(X0,X1) = low
| ~ is_aligned(X0,X1)
| ~ positional_advantage(X0,X1) )
& ( hazard_of_mortality(X0,X1) = mod1
| is_aligned(X0,X1)
| ~ positional_advantage(X0,X1) )
& ( hazard_of_mortality(X0,X1) = mod2
| ~ is_aligned(X0,X1)
| positional_advantage(X0,X1) )
& ( hazard_of_mortality(X0,X1) = high
| is_aligned(X0,X1)
| positional_advantage(X0,X1) ) )
| has_immunity(X0,X1) ) )
| ~ organization(X0) ),
inference(flattening,[],[f35]) ).
fof(f37,plain,
? [X0,X1,X2,X3,X4] :
( ( ~ smaller(hazard_of_mortality(X0,X4),hazard_of_mortality(X0,X2))
| ~ smaller(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X3))
| hazard_of_mortality(X0,X1) != hazard_of_mortality(X0,X2) )
& organization(X0)
& robust_position(X0)
& ~ has_endowment(X0)
& age(X0,X1) = zero
& greater(sigma,zero)
& greater(tau,zero)
& smaller(sigma,tau)
& smaller_or_equal(age(X0,X2),sigma)
& greater(age(X0,X3),sigma)
& smaller_or_equal(age(X0,X3),tau)
& greater(age(X0,X4),tau) ),
inference(ennf_transformation,[],[f21]) ).
fof(f38,plain,
? [X0,X1,X2,X3,X4] :
( ( ~ smaller(hazard_of_mortality(X0,X4),hazard_of_mortality(X0,X2))
| ~ smaller(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X3))
| hazard_of_mortality(X0,X1) != hazard_of_mortality(X0,X2) )
& organization(X0)
& robust_position(X0)
& ~ has_endowment(X0)
& age(X0,X1) = zero
& greater(sigma,zero)
& greater(tau,zero)
& smaller(sigma,tau)
& smaller_or_equal(age(X0,X2),sigma)
& greater(age(X0,X3),sigma)
& smaller_or_equal(age(X0,X3),tau)
& greater(age(X0,X4),tau) ),
inference(flattening,[],[f37]) ).
fof(f39,plain,
! [X0,X1] :
( X0 = X1
| smaller(X0,X1)
| ~ smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f40,plain,
! [X0,X1] :
( X0 != X1
| smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f41,plain,
! [X0,X1] :
( ~ smaller(X0,X1)
| smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f42,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| smaller(X0,X1) ),
inference(cnf_transformation,[],[f3]) ).
fof(f43,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[],[f3]) ).
fof(f44,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
fof(f45,plain,
! [X2,X0,X1] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f46,plain,
! [X0,X1] :
( greater(X0,X1)
| X0 = X1
| smaller(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f53,plain,
! [X0,X1] :
( has_endowment(X0)
| ~ organization(X0)
| ~ has_immunity(X0,X1) ),
inference(cnf_transformation,[],[f28]) ).
fof(f55,plain,
! [X2,X0,X1] :
( is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ organization(X0)
| dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[],[f29]) ).
fof(f57,plain,
! [X2,X0,X1] :
( ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[],[f29]) ).
fof(f58,plain,
! [X2,X0,X1] :
( organization(X0)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[],[f29]) ).
fof(f59,plain,
! [X0,X1] :
( age(X0,X1) != zero
| ~ organization(X0)
| is_aligned(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
fof(f60,plain,
! [X2,X0,X1] :
( age(X0,X1) != zero
| ~ organization(X0)
| ~ dissimilar(X0,X1,X2)
| greater(age(X0,X2),sigma) ),
inference(cnf_transformation,[],[f33]) ).
fof(f61,plain,
! [X2,X0,X1] :
( age(X0,X1) != zero
| ~ organization(X0)
| dissimilar(X0,X1,X2)
| ~ greater(age(X0,X2),sigma) ),
inference(cnf_transformation,[],[f33]) ).
fof(f62,plain,
! [X0,X1] :
( ~ robust_position(X0)
| ~ smaller_or_equal(age(X0,X1),tau)
| ~ positional_advantage(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f63,plain,
! [X0,X1] :
( ~ robust_position(X0)
| ~ greater(age(X0,X1),tau)
| positional_advantage(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f64,plain,
! [X0,X1] :
( ~ organization(X0)
| has_immunity(X0,X1)
| ~ positional_advantage(X0,X1)
| ~ is_aligned(X0,X1)
| hazard_of_mortality(X0,X1) = low ),
inference(cnf_transformation,[],[f36]) ).
fof(f65,plain,
! [X0,X1] :
( ~ organization(X0)
| has_immunity(X0,X1)
| ~ positional_advantage(X0,X1)
| is_aligned(X0,X1)
| hazard_of_mortality(X0,X1) = mod1 ),
inference(cnf_transformation,[],[f36]) ).
fof(f66,plain,
! [X0,X1] :
( ~ organization(X0)
| has_immunity(X0,X1)
| positional_advantage(X0,X1)
| ~ is_aligned(X0,X1)
| hazard_of_mortality(X0,X1) = mod2 ),
inference(cnf_transformation,[],[f36]) ).
fof(f67,plain,
! [X0,X1] :
( ~ organization(X0)
| has_immunity(X0,X1)
| positional_advantage(X0,X1)
| is_aligned(X0,X1)
| hazard_of_mortality(X0,X1) = high ),
inference(cnf_transformation,[],[f36]) ).
fof(f70,plain,
greater(mod1,low),
inference(cnf_transformation,[],[f15]) ).
fof(f72,plain,
greater(high,mod2),
inference(cnf_transformation,[],[f17]) ).
fof(f74,plain,
greater(mod2,mod1),
inference(cnf_transformation,[],[f19]) ).
fof(f75,plain,
( hazard_of_mortality(sK1,sK2) != hazard_of_mortality(sK1,sK3)
| ~ smaller(hazard_of_mortality(sK1,sK3),hazard_of_mortality(sK1,sK4))
| ~ smaller(hazard_of_mortality(sK1,sK5),hazard_of_mortality(sK1,sK3)) ),
inference(cnf_transformation,[],[f38]) ).
fof(f76,plain,
greater(age(sK1,sK5),tau),
inference(cnf_transformation,[],[f38]) ).
fof(f77,plain,
smaller_or_equal(age(sK1,sK4),tau),
inference(cnf_transformation,[],[f38]) ).
fof(f78,plain,
greater(age(sK1,sK4),sigma),
inference(cnf_transformation,[],[f38]) ).
fof(f79,plain,
smaller_or_equal(age(sK1,sK3),sigma),
inference(cnf_transformation,[],[f38]) ).
fof(f80,plain,
smaller(sigma,tau),
inference(cnf_transformation,[],[f38]) ).
fof(f81,plain,
greater(tau,zero),
inference(cnf_transformation,[],[f38]) ).
fof(f83,plain,
zero = age(sK1,sK2),
inference(cnf_transformation,[],[f38]) ).
fof(f84,plain,
~ has_endowment(sK1),
inference(cnf_transformation,[],[f38]) ).
fof(f85,plain,
robust_position(sK1),
inference(cnf_transformation,[],[f38]) ).
fof(f86,plain,
organization(sK1),
inference(cnf_transformation,[],[f38]) ).
fof(f87,plain,
! [X1] : smaller_or_equal(X1,X1),
inference(equality_resolution,[],[f40]) ).
fof(f88,plain,
! [X0,X1] :
( smaller(X0,X1)
| smaller_or_equal(X0,X1) ),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f89,plain,
! [X0,X1] :
( ~ smaller(X0,X1)
| X0 = X1
| ~ smaller_or_equal(X0,X1) ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f90,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| smaller(X0,X1) ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f91,plain,
! [X0,X1] :
( ~ smaller(X0,X1)
| greater(X1,X0) ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f92,plain,
! [X0,X1] :
( greater(X1,X0)
| greater(X0,X1) ),
inference(consistent_polarity_flipping,[],[f44]) ).
fof(f93,plain,
! [X2,X0,X1] :
( ~ greater(X0,X2)
| greater(X0,X1)
| greater(X1,X2) ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f94,plain,
! [X0,X1] :
( ~ smaller(X0,X1)
| X0 = X1
| ~ greater(X0,X1) ),
inference(consistent_polarity_flipping,[],[f46]) ).
fof(f100,plain,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| organization(X0)
| has_endowment(X0) ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f101,plain,
! [X2,X0,X1] :
( ~ organization(X0)
| dissimilar(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f102,plain,
! [X2,X0,X1] :
( ~ is_aligned(X0,X1)
| ~ is_aligned(X0,X2)
| dissimilar(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f104,plain,
! [X2,X0,X1] :
( ~ is_aligned(X0,X1)
| is_aligned(X0,X2)
| organization(X0)
| ~ dissimilar(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f106,plain,
! [X0,X1] :
( age(X0,X1) != zero
| organization(X0)
| is_aligned(X0,X1) ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f107,plain,
! [X2,X0,X1] :
( age(X0,X1) != zero
| organization(X0)
| ~ dissimilar(X0,X1,X2)
| greater(age(X0,X2),sigma) ),
inference(consistent_polarity_flipping,[],[f61]) ).
fof(f108,plain,
! [X2,X0,X1] :
( age(X0,X1) != zero
| organization(X0)
| dissimilar(X0,X1,X2)
| ~ greater(age(X0,X2),sigma) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f109,plain,
! [X0,X1] :
( ~ positional_advantage(X0,X1)
| greater(age(X0,X1),tau)
| ~ robust_position(X0) ),
inference(consistent_polarity_flipping,[],[f63]) ).
fof(f110,plain,
! [X0,X1] :
( ~ robust_position(X0)
| ~ smaller_or_equal(age(X0,X1),tau)
| positional_advantage(X0,X1) ),
inference(consistent_polarity_flipping,[],[f62]) ).
fof(f112,plain,
! [X0,X1] :
( ~ positional_advantage(X0,X1)
| has_immunity(X0,X1)
| organization(X0)
| is_aligned(X0,X1)
| hazard_of_mortality(X0,X1) = high ),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f113,plain,
! [X0,X1] :
( ~ positional_advantage(X0,X1)
| has_immunity(X0,X1)
| organization(X0)
| ~ is_aligned(X0,X1)
| hazard_of_mortality(X0,X1) = mod2 ),
inference(consistent_polarity_flipping,[],[f66]) ).
fof(f114,plain,
! [X0,X1] :
( positional_advantage(X0,X1)
| has_immunity(X0,X1)
| organization(X0)
| is_aligned(X0,X1)
| hazard_of_mortality(X0,X1) = mod1 ),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f115,plain,
! [X0,X1] :
( ~ is_aligned(X0,X1)
| has_immunity(X0,X1)
| positional_advantage(X0,X1)
| organization(X0)
| hazard_of_mortality(X0,X1) = low ),
inference(consistent_polarity_flipping,[],[f64]) ).
fof(f117,plain,
~ greater(mod1,low),
inference(consistent_polarity_flipping,[],[f70]) ).
fof(f119,plain,
~ greater(high,mod2),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f121,plain,
~ greater(mod2,mod1),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f122,plain,
~ organization(sK1),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f124,plain,
~ greater(tau,zero),
inference(consistent_polarity_flipping,[],[f81]) ).
fof(f125,plain,
~ smaller(sigma,tau),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f126,plain,
~ greater(age(sK1,sK4),sigma),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f127,plain,
~ greater(age(sK1,sK5),tau),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f128,plain,
( hazard_of_mortality(sK1,sK2) != hazard_of_mortality(sK1,sK3)
| smaller(hazard_of_mortality(sK1,sK3),hazard_of_mortality(sK1,sK4))
| smaller(hazard_of_mortality(sK1,sK5),hazard_of_mortality(sK1,sK3)) ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f130,definition,
( spl6_1
<=> smaller(hazard_of_mortality(sK1,sK5),hazard_of_mortality(sK1,sK3)) ),
introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition]) ).
fof(f131,plain,
( ~ smaller(hazard_of_mortality(sK1,sK5),hazard_of_mortality(sK1,sK3))
| spl6_1 ),
inference(avatar_component_clause,[],[f130]) ).
fof(f132,plain,
( smaller(hazard_of_mortality(sK1,sK5),hazard_of_mortality(sK1,sK3))
| ~ spl6_1 ),
inference(avatar_component_clause,[],[f130]) ).
fof(f134,definition,
( spl6_2
<=> smaller(hazard_of_mortality(sK1,sK3),hazard_of_mortality(sK1,sK4)) ),
introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition]) ).
fof(f136,plain,
( smaller(hazard_of_mortality(sK1,sK3),hazard_of_mortality(sK1,sK4))
| ~ spl6_2 ),
inference(avatar_component_clause,[],[f134]) ).
fof(f138,definition,
( spl6_3
<=> hazard_of_mortality(sK1,sK2) = hazard_of_mortality(sK1,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition]) ).
fof(f140,plain,
( hazard_of_mortality(sK1,sK2) != hazard_of_mortality(sK1,sK3)
| spl6_3 ),
inference(avatar_component_clause,[],[f138]) ).
fof(f141,plain,
( spl6_1
| spl6_2
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f128,f138,f134,f130]) ).
fof(f142,plain,
smaller_or_equal(sigma,tau),
inference(resolution,[],[f88,f125]) ).
fof(f143,plain,
! [X0,X1] :
( smaller_or_equal(X1,X0)
| greater(X0,X1) ),
inference(resolution,[],[f91,f88]) ).
fof(f144,plain,
! [X0,X1] :
( smaller(X1,X0)
| greater(X1,X0) ),
inference(resolution,[],[f92,f90]) ).
fof(f149,plain,
greater(low,mod1),
inference(resolution,[],[f92,f117]) ).
fof(f152,plain,
greater(mod1,mod2),
inference(resolution,[],[f92,f121]) ).
fof(f164,plain,
! [X0] : greater(X0,X0),
inference(factoring,[],[f92]) ).
fof(f173,plain,
( zero != zero
| organization(sK1)
| is_aligned(sK1,sK2) ),
inference(superposition,[],[f106,f83]) ).
fof(f174,plain,
( organization(sK1)
| is_aligned(sK1,sK2) ),
inference(trivial_inequality_removal,[],[f173]) ).
fof(f175,plain,
is_aligned(sK1,sK2),
inference(forward_subsumption_resolution,[],[f174,f122]) ).
fof(f176,plain,
! [X0] :
( ~ is_aligned(sK1,X0)
| dissimilar(sK1,sK2,X0) ),
inference(resolution,[],[f175,f102]) ).
fof(f201,plain,
! [X0] :
( ~ smaller_or_equal(age(sK1,X0),tau)
| positional_advantage(sK1,X0) ),
inference(resolution,[],[f110,f85]) ).
fof(f202,plain,
! [X0] :
( is_aligned(sK1,X0)
| organization(sK1)
| ~ dissimilar(sK1,sK2,X0) ),
inference(resolution,[],[f104,f175]) ).
fof(f203,plain,
! [X0] :
( ~ dissimilar(sK1,sK2,X0)
| is_aligned(sK1,X0) ),
inference(forward_subsumption_resolution,[],[f202,f122]) ).
fof(f223,plain,
! [X0] :
( zero != zero
| organization(sK1)
| ~ dissimilar(sK1,sK2,X0)
| greater(age(sK1,X0),sigma) ),
inference(superposition,[],[f107,f83]) ).
fof(f224,plain,
! [X0] :
( organization(sK1)
| ~ dissimilar(sK1,sK2,X0)
| greater(age(sK1,X0),sigma) ),
inference(trivial_inequality_removal,[],[f223]) ).
fof(f225,plain,
! [X0] :
( ~ dissimilar(sK1,sK2,X0)
| greater(age(sK1,X0),sigma) ),
inference(forward_subsumption_resolution,[],[f224,f122]) ).
fof(f238,plain,
! [X2,X0,X1] :
( age(X0,X1) != zero
| dissimilar(X0,X1,X2)
| ~ greater(age(X0,X2),sigma) ),
inference(forward_subsumption_resolution,[],[f108,f101]) ).
fof(f239,plain,
! [X0] :
( zero != zero
| dissimilar(sK1,sK2,X0)
| ~ greater(age(sK1,X0),sigma) ),
inference(superposition,[],[f238,f83]) ).
fof(f240,plain,
! [X0] :
( ~ greater(age(sK1,X0),sigma)
| dissimilar(sK1,sK2,X0) ),
inference(trivial_inequality_removal,[],[f239]) ).
fof(f258,definition,
( spl6_13
<=> positional_advantage(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl6_13])],[avatar_definition]) ).
fof(f260,plain,
( positional_advantage(sK1,sK2)
| ~ spl6_13 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f262,definition,
( spl6_14
<=> has_immunity(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl6_14])],[avatar_definition]) ).
fof(f264,plain,
( has_immunity(sK1,sK2)
| ~ spl6_14 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f266,plain,
positional_advantage(sK1,sK4),
inference(resolution,[],[f201,f77]) ).
fof(f267,plain,
( ~ smaller_or_equal(zero,tau)
| positional_advantage(sK1,sK2) ),
inference(superposition,[],[f201,f83]) ).
fof(f269,definition,
( spl6_15
<=> smaller_or_equal(zero,tau) ),
introduced(definition,[new_symbols(definition,[spl6_15])],[avatar_definition]) ).
fof(f271,plain,
( ~ smaller_or_equal(zero,tau)
| spl6_15 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f272,plain,
( spl6_13
| ~ spl6_15 ),
inference(avatar_split_clause,[],[f267,f269,f258]) ).
fof(f280,plain,
smaller(mod1,low),
inference(resolution,[],[f149,f90]) ).
fof(f284,plain,
( has_immunity(sK1,sK4)
| organization(sK1)
| is_aligned(sK1,sK4)
| high = hazard_of_mortality(sK1,sK4) ),
inference(resolution,[],[f266,f112]) ).
fof(f287,plain,
( has_immunity(sK1,sK4)
| is_aligned(sK1,sK4)
| high = hazard_of_mortality(sK1,sK4) ),
inference(forward_subsumption_resolution,[],[f284,f122]) ).
fof(f290,definition,
( spl6_16
<=> high = hazard_of_mortality(sK1,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_16])],[avatar_definition]) ).
fof(f292,plain,
( high = hazard_of_mortality(sK1,sK4)
| ~ spl6_16 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f294,definition,
( spl6_17
<=> is_aligned(sK1,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_17])],[avatar_definition]) ).
fof(f296,plain,
( is_aligned(sK1,sK4)
| ~ spl6_17 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f298,definition,
( spl6_18
<=> has_immunity(sK1,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_18])],[avatar_definition]) ).
fof(f300,plain,
( has_immunity(sK1,sK4)
| ~ spl6_18 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f301,plain,
( spl6_16
| spl6_17
| spl6_18 ),
inference(avatar_split_clause,[],[f287,f298,f294,f290]) ).
fof(f310,plain,
smaller(mod2,mod1),
inference(resolution,[],[f152,f90]) ).
fof(f314,plain,
! [X0] : smaller(X0,X0),
inference(resolution,[],[f164,f90]) ).
fof(f319,plain,
! [X0] :
( greater(tau,age(sK1,X0))
| positional_advantage(sK1,X0) ),
inference(resolution,[],[f143,f201]) ).
fof(f320,plain,
( greater(tau,zero)
| spl6_15 ),
inference(resolution,[],[f143,f271]) ).
fof(f321,plain,
( $false
| spl6_15 ),
inference(forward_subsumption_resolution,[],[f320,f124]) ).
fof(f322,plain,
spl6_15,
inference(avatar_contradiction_clause,[],[f321]) ).
fof(f323,plain,
( has_immunity(sK1,sK2)
| organization(sK1)
| ~ is_aligned(sK1,sK2)
| mod2 = hazard_of_mortality(sK1,sK2)
| ~ spl6_13 ),
inference(resolution,[],[f260,f113]) ).
fof(f327,plain,
( has_immunity(sK1,sK2)
| ~ is_aligned(sK1,sK2)
| mod2 = hazard_of_mortality(sK1,sK2)
| ~ spl6_13 ),
inference(forward_subsumption_resolution,[],[f323,f122]) ).
fof(f329,plain,
( has_immunity(sK1,sK2)
| mod2 = hazard_of_mortality(sK1,sK2)
| ~ spl6_13 ),
inference(forward_subsumption_resolution,[],[f327,f175]) ).
fof(f331,definition,
( spl6_20
<=> mod2 = hazard_of_mortality(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl6_20])],[avatar_definition]) ).
fof(f333,plain,
( mod2 = hazard_of_mortality(sK1,sK2)
| ~ spl6_20 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f334,plain,
( spl6_20
| spl6_14
| ~ spl6_13 ),
inference(avatar_split_clause,[],[f329,f258,f262,f331]) ).
fof(f336,plain,
( organization(sK1)
| has_endowment(sK1)
| ~ spl6_14 ),
inference(resolution,[],[f264,f100]) ).
fof(f337,plain,
( has_endowment(sK1)
| ~ spl6_14 ),
inference(forward_subsumption_resolution,[],[f336,f122]) ).
fof(f339,plain,
( $false
| ~ spl6_14 ),
inference(forward_subsumption_resolution,[],[f337,f84]) ).
fof(f340,plain,
~ spl6_14,
inference(avatar_contradiction_clause,[],[f339]) ).
fof(f341,plain,
greater(sigma,tau),
inference(resolution,[],[f144,f125]) ).
fof(f343,plain,
! [X0,X1] :
( ~ smaller_or_equal(X0,X1)
| X0 = X1
| greater(X0,X1) ),
inference(resolution,[],[f144,f89]) ).
fof(f397,plain,
! [X0] :
( greater(sigma,X0)
| greater(X0,tau) ),
inference(resolution,[],[f341,f93]) ).
fof(f398,plain,
smaller(tau,sigma),
inference(resolution,[],[f341,f90]) ).
fof(f404,plain,
( sigma = tau
| ~ greater(tau,sigma) ),
inference(resolution,[],[f398,f94]) ).
fof(f412,definition,
( spl6_22
<=> sigma = tau ),
introduced(definition,[new_symbols(definition,[spl6_22])],[avatar_definition]) ).
fof(f414,plain,
( sigma = tau
| ~ spl6_22 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f417,definition,
( spl6_23
<=> greater(tau,sigma) ),
introduced(definition,[new_symbols(definition,[spl6_23])],[avatar_definition]) ).
fof(f420,plain,
( ~ spl6_23
| spl6_22 ),
inference(avatar_split_clause,[],[f404,f412,f417]) ).
fof(f451,plain,
! [X0,X1] :
( greater(X1,age(sK1,X0))
| greater(tau,X1)
| positional_advantage(sK1,X0) ),
inference(resolution,[],[f319,f93]) ).
fof(f467,plain,
( mod2 != hazard_of_mortality(sK1,sK3)
| spl6_3
| ~ spl6_20 ),
inference(superposition,[],[f140,f333]) ).
fof(f544,definition,
( spl6_33
<=> has_immunity(sK1,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_33])],[avatar_definition]) ).
fof(f545,plain,
( ~ has_immunity(sK1,sK5)
| spl6_33 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f546,plain,
( has_immunity(sK1,sK5)
| ~ spl6_33 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f548,definition,
( spl6_34
<=> is_aligned(sK1,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_34])],[avatar_definition]) ).
fof(f550,plain,
( is_aligned(sK1,sK5)
| ~ spl6_34 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f552,definition,
( spl6_35
<=> mod1 = hazard_of_mortality(sK1,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_35])],[avatar_definition]) ).
fof(f554,plain,
( mod1 = hazard_of_mortality(sK1,sK5)
| ~ spl6_35 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f585,plain,
( mod1 = mod2
| ~ smaller_or_equal(mod2,mod1) ),
inference(resolution,[],[f310,f89]) ).
fof(f588,definition,
( spl6_40
<=> smaller_or_equal(mod2,mod1) ),
introduced(definition,[new_symbols(definition,[spl6_40])],[avatar_definition]) ).
fof(f590,plain,
( ~ smaller_or_equal(mod2,mod1)
| spl6_40 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f592,definition,
( spl6_41
<=> mod1 = mod2 ),
introduced(definition,[new_symbols(definition,[spl6_41])],[avatar_definition]) ).
fof(f594,plain,
( mod1 = mod2
| ~ spl6_41 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f595,plain,
( ~ spl6_40
| spl6_41 ),
inference(avatar_split_clause,[],[f585,f592,f588]) ).
fof(f623,plain,
( organization(sK1)
| has_endowment(sK1)
| ~ spl6_33 ),
inference(resolution,[],[f546,f100]) ).
fof(f624,plain,
( has_endowment(sK1)
| ~ spl6_33 ),
inference(forward_subsumption_resolution,[],[f623,f122]) ).
fof(f626,plain,
( $false
| ~ spl6_33 ),
inference(forward_subsumption_resolution,[],[f624,f84]) ).
fof(f627,plain,
~ spl6_33,
inference(avatar_contradiction_clause,[],[f626]) ).
fof(f640,plain,
( dissimilar(sK1,sK2,sK5)
| ~ spl6_34 ),
inference(resolution,[],[f550,f176]) ).
fof(f654,definition,
( spl6_46
<=> positional_advantage(sK1,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_46])],[avatar_definition]) ).
fof(f655,plain,
( ~ positional_advantage(sK1,sK5)
| spl6_46 ),
inference(avatar_component_clause,[],[f654]) ).
fof(f656,plain,
( positional_advantage(sK1,sK5)
| ~ spl6_46 ),
inference(avatar_component_clause,[],[f654]) ).
fof(f698,plain,
( sigma = age(sK1,sK3)
| greater(age(sK1,sK3),sigma) ),
inference(resolution,[],[f343,f79]) ).
fof(f704,definition,
( spl6_47
<=> greater(age(sK1,sK3),sigma) ),
introduced(definition,[new_symbols(definition,[spl6_47])],[avatar_definition]) ).
fof(f705,plain,
( ~ greater(age(sK1,sK3),sigma)
| spl6_47 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f706,plain,
( greater(age(sK1,sK3),sigma)
| ~ spl6_47 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f708,definition,
( spl6_48
<=> sigma = age(sK1,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_48])],[avatar_definition]) ).
fof(f710,plain,
( sigma = age(sK1,sK3)
| ~ spl6_48 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f711,plain,
( spl6_47
| spl6_48 ),
inference(avatar_split_clause,[],[f698,f708,f704]) ).
fof(f726,plain,
( dissimilar(sK1,sK2,sK3)
| ~ spl6_47 ),
inference(resolution,[],[f706,f240]) ).
fof(f728,plain,
( smaller(sigma,age(sK1,sK3))
| ~ spl6_47 ),
inference(resolution,[],[f706,f90]) ).
fof(f729,plain,
( is_aligned(sK1,sK3)
| ~ spl6_47 ),
inference(resolution,[],[f726,f203]) ).
fof(f804,plain,
( has_immunity(sK1,sK3)
| positional_advantage(sK1,sK3)
| organization(sK1)
| low = hazard_of_mortality(sK1,sK3)
| ~ spl6_47 ),
inference(resolution,[],[f729,f115]) ).
fof(f810,plain,
( has_immunity(sK1,sK3)
| positional_advantage(sK1,sK3)
| low = hazard_of_mortality(sK1,sK3)
| ~ spl6_47 ),
inference(forward_subsumption_resolution,[],[f804,f122]) ).
fof(f812,definition,
( spl6_49
<=> low = hazard_of_mortality(sK1,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_49])],[avatar_definition]) ).
fof(f814,plain,
( low = hazard_of_mortality(sK1,sK3)
| ~ spl6_49 ),
inference(avatar_component_clause,[],[f812]) ).
fof(f816,definition,
( spl6_50
<=> positional_advantage(sK1,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_50])],[avatar_definition]) ).
fof(f818,plain,
( positional_advantage(sK1,sK3)
| ~ spl6_50 ),
inference(avatar_component_clause,[],[f816]) ).
fof(f820,definition,
( spl6_51
<=> has_immunity(sK1,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_51])],[avatar_definition]) ).
fof(f821,plain,
( ~ has_immunity(sK1,sK3)
| spl6_51 ),
inference(avatar_component_clause,[],[f820]) ).
fof(f822,plain,
( has_immunity(sK1,sK3)
| ~ spl6_51 ),
inference(avatar_component_clause,[],[f820]) ).
fof(f862,plain,
( ~ greater(sigma,sigma)
| spl6_47
| ~ spl6_48 ),
inference(superposition,[],[f705,f710]) ).
fof(f864,plain,
( ~ smaller_or_equal(sigma,tau)
| positional_advantage(sK1,sK3)
| ~ spl6_48 ),
inference(superposition,[],[f201,f710]) ).
fof(f883,plain,
( positional_advantage(sK1,sK3)
| ~ spl6_48 ),
inference(forward_subsumption_resolution,[],[f864,f142]) ).
fof(f884,plain,
( $false
| spl6_47
| ~ spl6_48 ),
inference(forward_subsumption_resolution,[],[f862,f164]) ).
fof(f885,plain,
( spl6_47
| ~ spl6_48 ),
inference(avatar_contradiction_clause,[],[f884]) ).
fof(f887,definition,
( spl6_53
<=> is_aligned(sK1,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_53])],[avatar_definition]) ).
fof(f889,plain,
( is_aligned(sK1,sK3)
| ~ spl6_53 ),
inference(avatar_component_clause,[],[f887]) ).
fof(f897,plain,
( spl6_50
| ~ spl6_48 ),
inference(avatar_split_clause,[],[f883,f708,f816]) ).
fof(f898,plain,
( spl6_53
| ~ spl6_47 ),
inference(avatar_split_clause,[],[f729,f704,f887]) ).
fof(f899,plain,
( spl6_49
| spl6_50
| spl6_51
| ~ spl6_47 ),
inference(avatar_split_clause,[],[f810,f704,f820,f816,f812]) ).
fof(f919,plain,
greater(sigma,age(sK1,sK5)),
inference(resolution,[],[f397,f127]) ).
fof(f923,plain,
( has_immunity(sK1,sK3)
| organization(sK1)
| ~ is_aligned(sK1,sK3)
| mod2 = hazard_of_mortality(sK1,sK3)
| ~ spl6_50 ),
inference(resolution,[],[f818,f113]) ).
fof(f927,plain,
( has_immunity(sK1,sK3)
| ~ is_aligned(sK1,sK3)
| mod2 = hazard_of_mortality(sK1,sK3)
| ~ spl6_50 ),
inference(forward_subsumption_resolution,[],[f923,f122]) ).
fof(f928,plain,
( has_immunity(sK1,sK3)
| mod2 = hazard_of_mortality(sK1,sK3)
| ~ spl6_50
| ~ spl6_53 ),
inference(forward_subsumption_resolution,[],[f927,f889]) ).
fof(f929,plain,
( has_immunity(sK1,sK3)
| spl6_3
| ~ spl6_20
| ~ spl6_50
| ~ spl6_53 ),
inference(forward_subsumption_resolution,[],[f928,f467]) ).
fof(f930,plain,
( spl6_51
| spl6_3
| ~ spl6_20
| ~ spl6_50
| ~ spl6_53 ),
inference(avatar_split_clause,[],[f929,f887,f816,f331,f138,f820]) ).
fof(f931,plain,
( smaller(mod1,hazard_of_mortality(sK1,sK3))
| ~ spl6_1
| ~ spl6_35 ),
inference(forward_demodulation,[],[f132,f554]) ).
fof(f934,definition,
( spl6_55
<=> mod2 = hazard_of_mortality(sK1,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_55])],[avatar_definition]) ).
fof(f936,plain,
( mod2 = hazard_of_mortality(sK1,sK3)
| ~ spl6_55 ),
inference(avatar_component_clause,[],[f934]) ).
fof(f941,plain,
( mod1 = hazard_of_mortality(sK1,sK3)
| ~ greater(mod1,hazard_of_mortality(sK1,sK3))
| ~ spl6_1
| ~ spl6_35 ),
inference(resolution,[],[f931,f94]) ).
fof(f949,definition,
( spl6_57
<=> mod1 = hazard_of_mortality(sK1,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_57])],[avatar_definition]) ).
fof(f951,plain,
( mod1 = hazard_of_mortality(sK1,sK3)
| ~ spl6_57 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f954,definition,
( spl6_58
<=> greater(mod1,hazard_of_mortality(sK1,sK3)) ),
introduced(definition,[new_symbols(definition,[spl6_58])],[avatar_definition]) ).
fof(f956,plain,
( ~ greater(mod1,hazard_of_mortality(sK1,sK3))
| spl6_58 ),
inference(avatar_component_clause,[],[f954]) ).
fof(f957,plain,
( ~ spl6_58
| spl6_57
| ~ spl6_1
| ~ spl6_35 ),
inference(avatar_split_clause,[],[f941,f552,f130,f949,f954]) ).
fof(f972,plain,
( organization(sK1)
| has_endowment(sK1)
| ~ spl6_51 ),
inference(resolution,[],[f822,f100]) ).
fof(f973,plain,
( has_endowment(sK1)
| ~ spl6_51 ),
inference(forward_subsumption_resolution,[],[f972,f122]) ).
fof(f975,plain,
( $false
| ~ spl6_51 ),
inference(forward_subsumption_resolution,[],[f973,f84]) ).
fof(f976,plain,
~ spl6_51,
inference(avatar_contradiction_clause,[],[f975]) ).
fof(f994,plain,
( sigma = age(sK1,sK3)
| ~ greater(sigma,age(sK1,sK3))
| ~ spl6_47 ),
inference(resolution,[],[f728,f94]) ).
fof(f1003,definition,
( spl6_60
<=> greater(sigma,age(sK1,sK3)) ),
introduced(definition,[new_symbols(definition,[spl6_60])],[avatar_definition]) ).
fof(f1005,plain,
( ~ greater(sigma,age(sK1,sK3))
| spl6_60 ),
inference(avatar_component_clause,[],[f1003]) ).
fof(f1006,plain,
( ~ spl6_60
| spl6_48
| ~ spl6_47 ),
inference(avatar_split_clause,[],[f994,f704,f708,f1003]) ).
fof(f1022,plain,
smaller(age(sK1,sK5),sigma),
inference(resolution,[],[f919,f90]) ).
fof(f1280,plain,
( sigma = age(sK1,sK5)
| ~ greater(age(sK1,sK5),sigma) ),
inference(resolution,[],[f1022,f94]) ).
fof(f1288,definition,
( spl6_81
<=> sigma = age(sK1,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_81])],[avatar_definition]) ).
fof(f1290,plain,
( sigma = age(sK1,sK5)
| ~ spl6_81 ),
inference(avatar_component_clause,[],[f1288]) ).
fof(f1293,definition,
( spl6_82
<=> greater(age(sK1,sK5),sigma) ),
introduced(definition,[new_symbols(definition,[spl6_82])],[avatar_definition]) ).
fof(f1296,plain,
( ~ spl6_82
| spl6_81 ),
inference(avatar_split_clause,[],[f1280,f1288,f1293]) ).
fof(f1359,plain,
( ~ smaller(hazard_of_mortality(sK1,sK5),low)
| spl6_1
| ~ spl6_49 ),
inference(forward_demodulation,[],[f131,f814]) ).
fof(f1360,plain,
( smaller(hazard_of_mortality(sK1,sK3),high)
| ~ spl6_2
| ~ spl6_16 ),
inference(forward_demodulation,[],[f136,f292]) ).
fof(f1362,plain,
( ~ smaller(mod1,low)
| spl6_1
| ~ spl6_35
| ~ spl6_49 ),
inference(forward_demodulation,[],[f1359,f554]) ).
fof(f1364,plain,
( $false
| spl6_1
| ~ spl6_35
| ~ spl6_49 ),
inference(forward_subsumption_resolution,[],[f1362,f280]) ).
fof(f1365,plain,
( spl6_1
| ~ spl6_35
| ~ spl6_49 ),
inference(avatar_contradiction_clause,[],[f1364]) ).
fof(f1369,plain,
( greater(high,hazard_of_mortality(sK1,sK3))
| ~ spl6_2
| ~ spl6_16 ),
inference(resolution,[],[f1360,f91]) ).
fof(f1533,plain,
( greater(high,mod2)
| ~ spl6_2
| ~ spl6_16
| ~ spl6_55 ),
inference(superposition,[],[f1369,f936]) ).
fof(f1536,plain,
( $false
| ~ spl6_2
| ~ spl6_16
| ~ spl6_55 ),
inference(forward_subsumption_resolution,[],[f1533,f119]) ).
fof(f1537,plain,
( ~ spl6_2
| ~ spl6_16
| ~ spl6_55 ),
inference(avatar_contradiction_clause,[],[f1536]) ).
fof(f1553,plain,
( organization(sK1)
| has_endowment(sK1)
| ~ spl6_18 ),
inference(resolution,[],[f300,f100]) ).
fof(f1554,plain,
( has_endowment(sK1)
| ~ spl6_18 ),
inference(forward_subsumption_resolution,[],[f1553,f122]) ).
fof(f1556,plain,
( $false
| ~ spl6_18 ),
inference(forward_subsumption_resolution,[],[f1554,f84]) ).
fof(f1557,plain,
~ spl6_18,
inference(avatar_contradiction_clause,[],[f1556]) ).
fof(f1574,plain,
( dissimilar(sK1,sK2,sK4)
| ~ spl6_17 ),
inference(resolution,[],[f296,f176]) ).
fof(f1592,plain,
( greater(age(sK1,sK4),sigma)
| ~ spl6_17 ),
inference(resolution,[],[f1574,f225]) ).
fof(f1593,plain,
( $false
| ~ spl6_17 ),
inference(forward_subsumption_resolution,[],[f1592,f126]) ).
fof(f1594,plain,
~ spl6_17,
inference(avatar_contradiction_clause,[],[f1593]) ).
fof(f1671,plain,
( greater(age(sK1,sK5),tau)
| ~ robust_position(sK1)
| ~ spl6_46 ),
inference(resolution,[],[f656,f109]) ).
fof(f1672,plain,
( ~ robust_position(sK1)
| ~ spl6_46 ),
inference(forward_subsumption_resolution,[],[f1671,f127]) ).
fof(f1674,plain,
( $false
| ~ spl6_46 ),
inference(forward_subsumption_resolution,[],[f1672,f85]) ).
fof(f1675,plain,
~ spl6_46,
inference(avatar_contradiction_clause,[],[f1674]) ).
fof(f1721,plain,
( has_immunity(sK1,sK5)
| organization(sK1)
| is_aligned(sK1,sK5)
| mod1 = hazard_of_mortality(sK1,sK5)
| spl6_46 ),
inference(resolution,[],[f655,f114]) ).
fof(f1743,plain,
( greater(age(sK1,sK5),sigma)
| ~ spl6_34 ),
inference(resolution,[],[f640,f225]) ).
fof(f1746,plain,
( spl6_82
| ~ spl6_34 ),
inference(avatar_split_clause,[],[f1743,f548,f1293]) ).
fof(f1765,definition,
( spl6_114
<=> smaller_or_equal(hazard_of_mortality(sK1,sK3),mod1) ),
introduced(definition,[new_symbols(definition,[spl6_114])],[avatar_definition]) ).
fof(f1766,plain,
( smaller_or_equal(hazard_of_mortality(sK1,sK3),mod1)
| ~ spl6_114 ),
inference(avatar_component_clause,[],[f1765]) ).
fof(f1767,plain,
( ~ smaller_or_equal(hazard_of_mortality(sK1,sK3),mod1)
| spl6_114 ),
inference(avatar_component_clause,[],[f1765]) ).
fof(f1993,plain,
( ~ smaller_or_equal(mod1,mod1)
| ~ spl6_57
| spl6_114 ),
inference(superposition,[],[f1767,f951]) ).
fof(f2002,plain,
( $false
| ~ spl6_57
| spl6_114 ),
inference(forward_subsumption_resolution,[],[f1993,f87]) ).
fof(f2003,plain,
( ~ spl6_57
| spl6_114 ),
inference(avatar_contradiction_clause,[],[f2002]) ).
fof(f2236,plain,
( greater(tau,sigma)
| positional_advantage(sK1,sK3)
| spl6_60 ),
inference(resolution,[],[f1005,f451]) ).
fof(f2257,plain,
( ~ smaller(sigma,sigma)
| ~ spl6_22 ),
inference(superposition,[],[f125,f414]) ).
fof(f2297,plain,
( $false
| ~ spl6_22 ),
inference(forward_subsumption_resolution,[],[f2257,f314]) ).
fof(f2298,plain,
~ spl6_22,
inference(avatar_contradiction_clause,[],[f2297]) ).
fof(f2302,plain,
( mod2 = hazard_of_mortality(sK1,sK3)
| ~ spl6_50
| spl6_51
| ~ spl6_53 ),
inference(forward_subsumption_resolution,[],[f928,f821]) ).
fof(f2306,plain,
( spl6_50
| spl6_23
| spl6_60 ),
inference(avatar_split_clause,[],[f2236,f1003,f417,f816]) ).
fof(f2307,plain,
( spl6_55
| ~ spl6_50
| spl6_51
| ~ spl6_53 ),
inference(avatar_split_clause,[],[f2302,f887,f820,f816,f934]) ).
fof(f2970,plain,
( ~ greater(mod1,mod1)
| ~ spl6_41 ),
inference(superposition,[],[f121,f594]) ).
fof(f3004,plain,
( $false
| ~ spl6_41 ),
inference(forward_subsumption_resolution,[],[f2970,f164]) ).
fof(f3005,plain,
~ spl6_41,
inference(avatar_contradiction_clause,[],[f3004]) ).
fof(f3056,plain,
( ~ greater(sigma,tau)
| ~ spl6_81 ),
inference(superposition,[],[f127,f1290]) ).
fof(f3113,plain,
( $false
| ~ spl6_81 ),
inference(forward_subsumption_resolution,[],[f3056,f341]) ).
fof(f3114,plain,
~ spl6_81,
inference(avatar_contradiction_clause,[],[f3113]) ).
fof(f3136,plain,
( organization(sK1)
| is_aligned(sK1,sK5)
| mod1 = hazard_of_mortality(sK1,sK5)
| spl6_33
| spl6_46 ),
inference(forward_subsumption_resolution,[],[f1721,f545]) ).
fof(f3144,plain,
( is_aligned(sK1,sK5)
| mod1 = hazard_of_mortality(sK1,sK5)
| spl6_33
| spl6_46 ),
inference(forward_subsumption_resolution,[],[f3136,f122]) ).
fof(f3181,plain,
( spl6_35
| spl6_34
| spl6_33
| spl6_46 ),
inference(avatar_split_clause,[],[f3144,f654,f544,f548,f552]) ).
fof(f4890,plain,
( ~ greater(mod1,mod2)
| ~ spl6_55
| spl6_58 ),
inference(superposition,[],[f956,f936]) ).
fof(f4902,plain,
( smaller_or_equal(mod2,mod1)
| ~ spl6_55
| ~ spl6_114 ),
inference(superposition,[],[f1766,f936]) ).
fof(f4941,plain,
( $false
| spl6_40
| ~ spl6_55
| ~ spl6_114 ),
inference(forward_subsumption_resolution,[],[f4902,f590]) ).
fof(f4942,plain,
( spl6_40
| ~ spl6_55
| ~ spl6_114 ),
inference(avatar_contradiction_clause,[],[f4941]) ).
fof(f4943,plain,
( $false
| ~ spl6_55
| spl6_58 ),
inference(forward_subsumption_resolution,[],[f4890,f152]) ).
fof(f4944,plain,
( ~ spl6_55
| spl6_58 ),
inference(avatar_contradiction_clause,[],[f4943]) ).
cnf(s1,plain,
( spl6_1
| spl6_2
| ~ spl6_3 ),
inference(sat_conversion,[],[f141]) ).
cnf(s7,plain,
( spl6_13
| ~ spl6_15 ),
inference(sat_conversion,[],[f272]) ).
cnf(s8,plain,
( spl6_16
| spl6_17
| spl6_18 ),
inference(sat_conversion,[],[f301]) ).
cnf(s10,plain,
spl6_15,
inference(sat_conversion,[],[f322]) ).
cnf(s11,plain,
( ~ spl6_13
| spl6_14
| spl6_20 ),
inference(sat_conversion,[],[f334]) ).
cnf(s12,plain,
~ spl6_14,
inference(sat_conversion,[],[f340]) ).
cnf(s14,plain,
( spl6_22
| ~ spl6_23 ),
inference(sat_conversion,[],[f420]) ).
cnf(s29,plain,
( ~ spl6_40
| spl6_41 ),
inference(sat_conversion,[],[f595]) ).
cnf(s31,plain,
~ spl6_33,
inference(sat_conversion,[],[f627]) ).
cnf(s36,plain,
( spl6_47
| spl6_48 ),
inference(sat_conversion,[],[f711]) ).
cnf(s39,plain,
( spl6_47
| ~ spl6_48 ),
inference(sat_conversion,[],[f885]) ).
cnf(s44,plain,
( ~ spl6_48
| spl6_50 ),
inference(sat_conversion,[],[f897]) ).
cnf(s45,plain,
( ~ spl6_47
| spl6_53 ),
inference(sat_conversion,[],[f898]) ).
cnf(s46,plain,
( ~ spl6_47
| spl6_49
| spl6_50
| spl6_51 ),
inference(sat_conversion,[],[f899]) ).
cnf(s48,plain,
( spl6_3
| ~ spl6_20
| ~ spl6_50
| spl6_51
| ~ spl6_53 ),
inference(sat_conversion,[],[f930]) ).
cnf(s55,plain,
( ~ spl6_1
| ~ spl6_35
| spl6_57
| ~ spl6_58 ),
inference(sat_conversion,[],[f957]) ).
cnf(s57,plain,
~ spl6_51,
inference(sat_conversion,[],[f976]) ).
cnf(s61,plain,
( ~ spl6_47
| spl6_48
| ~ spl6_60 ),
inference(sat_conversion,[],[f1006]) ).
cnf(s81,plain,
( spl6_81
| ~ spl6_82 ),
inference(sat_conversion,[],[f1296]) ).
cnf(s88,plain,
( spl6_1
| ~ spl6_35
| ~ spl6_49 ),
inference(sat_conversion,[],[f1365]) ).
cnf(s104,plain,
( ~ spl6_2
| ~ spl6_16
| ~ spl6_55 ),
inference(sat_conversion,[],[f1537]) ).
cnf(s108,plain,
~ spl6_18,
inference(sat_conversion,[],[f1557]) ).
cnf(s113,plain,
~ spl6_17,
inference(sat_conversion,[],[f1594]) ).
cnf(s132,plain,
~ spl6_46,
inference(sat_conversion,[],[f1675]) ).
cnf(s147,plain,
( ~ spl6_34
| spl6_82 ),
inference(sat_conversion,[],[f1746]) ).
cnf(s184,plain,
( ~ spl6_57
| spl6_114 ),
inference(sat_conversion,[],[f2003]) ).
cnf(s217,plain,
~ spl6_22,
inference(sat_conversion,[],[f2298]) ).
cnf(s224,plain,
( spl6_23
| spl6_50
| spl6_60 ),
inference(sat_conversion,[],[f2306]) ).
cnf(s226,plain,
( ~ spl6_50
| spl6_51
| ~ spl6_53
| spl6_55 ),
inference(sat_conversion,[],[f2307]) ).
cnf(s261,plain,
~ spl6_41,
inference(sat_conversion,[],[f3005]) ).
cnf(s269,plain,
~ spl6_81,
inference(sat_conversion,[],[f3114]) ).
cnf(s287,plain,
( spl6_33
| spl6_34
| spl6_35
| spl6_46 ),
inference(sat_conversion,[],[f3181]) ).
cnf(s430,plain,
( spl6_40
| ~ spl6_55
| ~ spl6_114 ),
inference(sat_conversion,[],[f4942]) ).
cnf(s431,plain,
( ~ spl6_55
| spl6_58 ),
inference(sat_conversion,[],[f4944]) ).
cnf(s449,plain,
~ spl6_82,
inference(rat,[],[s81,s269]) ).
cnf(s450,plain,
~ spl6_34,
inference(rat,[],[s147,s449]) ).
cnf(s453,plain,
( spl6_3
| ~ spl6_20
| ~ spl6_50
| ~ spl6_53 ),
inference(rat,[],[s48,s57]) ).
cnf(s455,plain,
( ~ spl6_47
| spl6_49
| spl6_50 ),
inference(rat,[],[s46,s57]) ).
cnf(s459,plain,
spl6_35,
inference(rat,[],[s287,s132,s450,s31]) ).
cnf(s460,plain,
~ spl6_40,
inference(rat,[],[s29,s261]) ).
cnf(s462,plain,
~ spl6_23,
inference(rat,[],[s14,s217]) ).
cnf(s465,plain,
( ~ spl6_13
| spl6_20 ),
inference(rat,[],[s11,s12]) ).
cnf(s466,plain,
spl6_16,
inference(rat,[],[s8,s108,s113]) ).
cnf(s467,plain,
spl6_13,
inference(rat,[],[s7,s10]) ).
cnf(s468,plain,
spl6_20,
inference(rat,[],[s465,s467]) ).
cnf(s470,plain,
spl6_47,
inference(rat,[],[s36,s39]) ).
cnf(s471,plain,
spl6_53,
inference(rat,[],[s45,s470]) ).
cnf(s472,plain,
spl6_1,
inference(rat,[],[s1,s104,s453,s226,s455,s88,s466,s471,s468,s57,s470,s459]) ).
cnf(s474,plain,
spl6_50,
inference(rat,[],[s61,s44,s224,s470,s462]) ).
cnf(s475,plain,
spl6_55,
inference(rat,[],[s226,s471,s57,s474]) ).
cnf(s477,plain,
spl6_58,
inference(rat,[],[s431,s475]) ).
cnf(s478,plain,
~ spl6_114,
inference(rat,[],[s430,s460,s475]) ).
cnf(s481,plain,
spl6_57,
inference(rat,[],[s55,s472,s459,s477]) ).
cnf(s482,plain,
$false,
inference(rat,[],[s184,s478,s481]) ).
fof(f4945,plain,
$false,
inference(avatar_sat_refutation,[],[s482]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT063+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/15.41 % Computer : n014.cluster.edu
% 0.11/15.41 % Model : x86_64 x86_64
% 0.11/15.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/15.41 % Memory : 8046.5625MB
% 0.11/15.41 % OS : Linux 6.8.0-71-generic
% 0.11/15.41 % CPULimit : 300
% 0.11/15.41 % WCLimit : 300
% 0.11/15.41 % DateTime : Sun Sep 27 17:32:05 UTC 2026
% 0.11/15.41 % CPUTime :
% 0.11/15.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/15.44 Running first-order model finding
% 0.11/15.44 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
% 0.15/15.60 % (1045747)Will run a generic schedule for satisfiability detection.
% 0.15/15.60 % (1045753)% WARNING: option uhcvi not known.
% 0.15/15.60 % (1045757)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2368838030:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.15/15.60 % (1045752)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4000459090_2999 on theBenchmark for (2999ds/0Mi)
% 0.15/15.60 % (1045755)dis+10_1_sil=32000:sp=arity:random_seed=2606383013:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.15/15.60 % (1045753)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1865975905:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.15/15.60 % (1045754)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=893508983:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.15/15.60 % (1045756)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1523017885:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.15/15.60 % (1045758)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3237595280:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.15/15.60 % TRYING [1]
% 0.15/15.60 % TRYING [2]
% 0.15/15.60 % TRYING [3]
% 0.15/15.60 % TRYING [4]
% 0.15/15.60 % TRYING [5]
% 0.15/15.60 % TRYING [6]
% 0.15/15.60 % (1045755)Instruction limit reached!
% 0.15/15.60 % (1045755)------------------------------
% 0.15/15.60 % (1045755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.15/15.60 % (1045755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/15.60 % (1045755)CaDiCaL version: 2.1.3
% 0.15/15.60 % (1045755)Termination reason: Instruction limit
% 0.15/15.60 % (1045755)Termination phase: Saturation
% 0.15/15.60 % (1045755)Time elapsed: 0.066 s
% 0.15/15.60 % (1045755)Peak memory usage: 12 MB
% 0.15/15.60 % (1045755)Instructions burned: 103 (million)
% 0.15/15.60 % (1045756)Instruction limit reached!
% 0.15/15.60 % (1045756)------------------------------
% 0.15/15.60 % (1045756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.15/15.60 % (1045756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/15.60 % (1045756)CaDiCaL version: 2.1.3
% 0.15/15.60 % (1045756)Termination reason: Instruction limit
% 0.15/15.60 % (1045756)Termination phase: Saturation
% 0.15/15.60 % (1045756)Time elapsed: 0.067 s
% 0.15/15.60 % (1045756)Peak memory usage: 12 MB
% 0.15/15.60 % (1045756)Instructions burned: 117 (million)
% 0.15/15.60 % (1045767)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2637764895:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.15/15.60 % (1045757)Instruction limit reached!
% 0.15/15.60 % (1045757)------------------------------
% 0.15/15.60 % (1045757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.15/15.60 % (1045757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/15.60 % (1045757)CaDiCaL version: 2.1.3
% 0.15/15.60 % (1045757)Termination reason: Instruction limit
% 0.15/15.60 % (1045757)Termination phase: Saturation
% 0.15/15.60 % (1045757)Time elapsed: 0.080 s
% 0.15/15.60 % (1045757)Peak memory usage: 12 MB
% 0.15/15.60 % (1045757)Instructions burned: 133 (million)
% 0.15/15.60 % (1045766)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3186303736:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.15/15.60 % TRYING [1]
% 0.15/15.60 % TRYING [2]
% 0.15/15.60 % TRYING [3]
% 0.15/15.60 % TRYING [4]
% 0.15/15.60 % (1045758)Instruction limit reached!
% 0.15/15.60 % (1045758)------------------------------
% 0.15/15.60 % (1045758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.15/15.60 % (1045758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/15.60 % (1045758)CaDiCaL version: 2.1.3
% 0.15/15.60 % (1045758)Termination reason: Instruction limit
% 0.15/15.60 % (1045758)Termination phase: Saturation
% 0.15/15.60 % (1045758)Time elapsed: 0.096 s
% 0.15/15.60 % (1045758)Peak memory usage: 13 MB
% 0.15/15.60 % (1045758)Instructions burned: 159 (million)
% 0.15/15.60 % (1045769)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=650466462:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.15/15.60 % TRYING [5]
% 0.15/15.60 % (1045753) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1045747-1045753"...
% 0.15/15.60 % (1045771)ott-21_1_sil=16000:fs=off:random_seed=4183875802:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.15/15.60 % (1045753)...printing done.
% 0.15/15.60 % (1045767) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1045747-1045767"...
% 0.15/15.60 % (1045753)Refutation found. Thanks to Tanya!
% 0.15/15.60 % SZS status Theorem for theBenchmark
% 0.15/15.60 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/15.60 % (1045753)------------------------------
% 0.15/15.60 % (1045753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.15/15.60 % (1045753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/15.60 % (1045753)CaDiCaL version: 2.1.3
% 0.15/15.60 % (1045753)Termination reason: Refutation
% 0.15/15.60 % (1045753)Time elapsed: 0.116 s
% 0.15/15.60 % (1045753)Peak memory usage: 14 MB
% 0.15/15.60 % (1045753)Instructions burned: 180 (million)
% 0.15/15.60 % (1045747)Success in time 0.148 s
% 0.15/15.60 % Vampire exiting
%------------------------------------------------------------------------------