%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : MGT061-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n003.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 : Fri Sep 25 02:12:59 PM UTC 2026
% Result : Unsatisfiable 3.05s 6.48s
% Output : CNFRefutation 3.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 31
% Syntax : Number of formulae : 158 ( 45 unt; 6 def)
% Number of atoms : 468 ( 117 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 512 ( 242 ~; 270 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 10 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 193 ( 0 sgn 193 !; 0 ?; 157 :)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1] :
( smaller_or_equal(X0,X1)
| ~ smaller(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT001-0.ax',definition_smaller_or_equal_2) ).
fof(f8,axiom,
! [X0,X1] :
( smaller(X1,X0)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT001-0.ax',definition_smaller_8) ).
fof(f10,axiom,
! [X2,X0,X1] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT001-0.ax',meaning_postulate_greater_transitive_10) ).
fof(f12,axiom,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| has_endowment(X0)
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_1_39) ).
fof(f13,axiom,
! [X2,X0,X1] :
( organization(X0)
| ~ dissimilar(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_2_40) ).
fof(f15,axiom,
! [X2,X0,X1] :
( ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_2_42) ).
fof(f17,axiom,
! [X2,X0,X1] :
( dissimilar(X0,X1,X2)
| is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_2_44) ).
fof(f20,axiom,
! [X0,X1] :
( is_aligned(X0,X1)
| age(X0,X1) != zero
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_13_47) ).
fof(f21,axiom,
! [X2,X0,X1] :
( dissimilar(X0,X1,X2)
| ~ greater(age(X0,X2),sigma)
| age(X0,X1) != zero
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_15_48) ).
fof(f22,axiom,
! [X2,X0,X1] :
( greater(age(X0,X2),sigma)
| ~ dissimilar(X0,X1,X2)
| age(X0,X1) != zero
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_15_49) ).
fof(f23,axiom,
! [X0,X1] :
( positional_advantage(X0,X1)
| ~ smaller_or_equal(age(X0,X1),sigma)
| ~ fragile_position(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_3_50) ).
fof(f24,axiom,
! [X0,X1] :
( ~ positional_advantage(X0,X1)
| ~ greater(age(X0,X1),sigma)
| ~ fragile_position(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_3_51) ).
fof(f30,axiom,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = low
| ~ positional_advantage(X0,X1)
| ~ is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_17_57) ).
fof(f31,axiom,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = mod1
| ~ positional_advantage(X0,X1)
| is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_17_58) ).
fof(f33,axiom,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = high
| positional_advantage(X0,X1)
| is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_17_60) ).
fof(f37,axiom,
greater(high,mod2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_18d_64) ).
fof(f38,axiom,
greater(mod2,low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_18e_65) ).
fof(f39,negated_conjecture,
organization(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_7_66) ).
fof(f40,negated_conjecture,
fragile_position(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_7_67) ).
fof(f41,negated_conjecture,
~ has_endowment(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_7_68) ).
fof(f42,negated_conjecture,
age(sk2,sk3) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_7_69) ).
fof(f43,plain,
zero = age(sk2,sk3),
inference(reorient_equations,[],[f42]) ).
fof(f44,negated_conjecture,
greater(sigma,zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_7_70) ).
fof(f45,negated_conjecture,
smaller_or_equal(age(sk2,sk4),sigma),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_7_71) ).
fof(f46,negated_conjecture,
greater(age(sk2,sk5),sigma),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_7_72) ).
fof(f47,negated_conjecture,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_7_73) ).
tcf(c_96,plain,
! [X0: $i,X1: $i] :
( smaller_or_equal(X0,X1)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i] :
( smaller(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i] :
( has_endowment(X0)
| ~ organization(X0)
| ~ has_immunity(X0,X1) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i] :
( organization(X0)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_aligned(X0,X2)
| dissimilar(X0,X1,X2)
| ~ organization(X0)
| ~ is_aligned(X0,X1) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i] :
( is_aligned(X0,X1)
| ~ organization(X0)
| ( age(X0,X1) != zero ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i] :
( dissimilar(X0,X1,X2)
| ~ organization(X0)
| ~ greater(age(X0,X2),sigma)
| ( age(X0,X1) != zero ) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(age(X0,X2),sigma)
| ~ organization(X0)
| ~ dissimilar(X0,X1,X2)
| ( age(X0,X1) != zero ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i] :
( positional_advantage(X0,X1)
| ~ fragile_position(X0)
| ~ smaller_or_equal(age(X0,X1),sigma) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i] :
( ~ fragile_position(X0)
| ~ positional_advantage(X0,X1)
| ~ greater(age(X0,X1),sigma) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i] :
( has_immunity(X0,X1)
| ( hazard_of_mortality(X0,X1) = low )
| ~ organization(X0)
| ~ positional_advantage(X0,X1)
| ~ is_aligned(X0,X1) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] :
( is_aligned(X0,X1)
| has_immunity(X0,X1)
| ( hazard_of_mortality(X0,X1) = mod1 )
| ~ organization(X0)
| ~ positional_advantage(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i] :
( positional_advantage(X0,X1)
| is_aligned(X0,X1)
| has_immunity(X0,X1)
| ( hazard_of_mortality(X0,X1) = high )
| ~ organization(X0) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_128,plain,
greater(high,mod2),
inference(cnf_transformation,[],[f37]) ).
tcf(c_129,plain,
greater(mod2,low),
inference(cnf_transformation,[],[f38]) ).
tcf(c_130,negated_conjecture,
organization(sk2),
inference(cnf_transformation,[],[f39]) ).
tcf(c_131,negated_conjecture,
fragile_position(sk2),
inference(cnf_transformation,[],[f40]) ).
tcf(c_132,negated_conjecture,
~ has_endowment(sk2),
inference(cnf_transformation,[],[f41]) ).
tcf(c_133,negated_conjecture,
age(sk2,sk3) = zero,
inference(cnf_transformation,[],[f43]) ).
tcf(c_134,negated_conjecture,
greater(sigma,zero),
inference(cnf_transformation,[],[f44]) ).
tcf(c_135,negated_conjecture,
smaller_or_equal(age(sk2,sk4),sigma),
inference(cnf_transformation,[],[f45]) ).
tcf(c_136,negated_conjecture,
greater(age(sk2,sk5),sigma),
inference(cnf_transformation,[],[f46]) ).
tcf(c_137,negated_conjecture,
( ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))
| ( hazard_of_mortality(sk2,sk3) != hazard_of_mortality(sk2,sk4) ) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_163,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(age(X0,X2),sigma)
| ( age(X0,X1) != zero )
| ~ dissimilar(X0,X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_114,c_107,c_114]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(age(X0,X2),sigma)
| ~ dissimilar(X0,X1,X2)
| ( age(X0,X1) != zero ) ),
inference(renaming,[status(thm)],[c_163]) ).
tcf(c_567,plain,
! [X0: $i,X1: $i] :
( ~ organization(X0)
| ~ has_immunity(X0,X1)
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_106,c_132]) ).
tcf(c_568,plain,
! [X0: $i] :
( ~ organization(sk2)
| ~ has_immunity(sk2,X0) ),
inference(unflattening,[status(thm)],[c_567]) ).
tcf(c_570,plain,
! [X0: $i] : ~ has_immunity(sk2,X0),
inference(global_subsumption_just,[status(thm)],[c_568,c_130,c_568]) ).
tcf(c_728,plain,
! [X0: $i,X1: $i] :
( ~ positional_advantage(X0,X1)
| ~ greater(age(X0,X1),sigma)
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_116,c_131]) ).
tcf(c_729,plain,
! [X0: $i] :
( ~ positional_advantage(sk2,X0)
| ~ greater(age(sk2,X0),sigma) ),
inference(unflattening,[status(thm)],[c_728]) ).
tcf(c_737,plain,
! [X0: $i,X1: $i] :
( positional_advantage(X0,X1)
| ~ smaller_or_equal(age(X0,X1),sigma)
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_115,c_131]) ).
tcf(c_738,plain,
! [X0: $i] :
( positional_advantage(sk2,X0)
| ~ smaller_or_equal(age(sk2,X0),sigma) ),
inference(unflattening,[status(thm)],[c_737]) ).
tcf(c_975,plain,
! [X0: $i,X1: $i,X2: $i] :
( positional_advantage(X0,X1)
| is_aligned(X0,X1)
| ( hazard_of_mortality(X0,X1) = high )
| ~ organization(X0)
| ( X1 != X2 )
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_124,c_570]) ).
tcf(c_976,plain,
! [X0: $i] :
( positional_advantage(sk2,X0)
| is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = high )
| ~ organization(sk2) ),
inference(unflattening,[status(thm)],[c_975]) ).
tcf(c_978,plain,
! [X0: $i] :
( positional_advantage(sk2,X0)
| is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = high ) ),
inference(global_subsumption_just,[status(thm)],[c_976,c_130,c_976]) ).
tcf(c_1005,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_aligned(X0,X1)
| ( hazard_of_mortality(X0,X1) = mod1 )
| ~ organization(X0)
| ~ positional_advantage(X0,X1)
| ( X1 != X2 )
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_122,c_570]) ).
tcf(c_1006,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = mod1 )
| ~ organization(sk2)
| ~ positional_advantage(sk2,X0) ),
inference(unflattening,[status(thm)],[c_1005]) ).
tcf(c_1008,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = mod1 )
| ~ positional_advantage(sk2,X0) ),
inference(global_subsumption_just,[status(thm)],[c_1006,c_130,c_1006]) ).
tcf(c_1020,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( hazard_of_mortality(X0,X1) = low )
| ~ organization(X0)
| ~ positional_advantage(X0,X1)
| ~ is_aligned(X0,X1)
| ( X1 != X2 )
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_121,c_570]) ).
tcf(c_1021,plain,
! [X0: $i] :
( ( hazard_of_mortality(sk2,X0) = low )
| ~ organization(sk2)
| ~ positional_advantage(sk2,X0)
| ~ is_aligned(sk2,X0) ),
inference(unflattening,[status(thm)],[c_1020]) ).
tcf(c_1023,plain,
! [X0: $i] :
( ( hazard_of_mortality(sk2,X0) = low )
| ~ is_aligned(sk2,X0)
| ~ positional_advantage(sk2,X0) ),
inference(global_subsumption_just,[status(thm)],[c_1021,c_130,c_1021]) ).
tcf(c_1024,plain,
! [X0: $i] :
( ( hazard_of_mortality(sk2,X0) = low )
| ~ positional_advantage(sk2,X0)
| ~ is_aligned(sk2,X0) ),
inference(renaming,[status(thm)],[c_1023]) ).
tcf(c_1069,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ organization(X0)
| ~ is_aligned(X2,X5)
| ~ is_aligned(X2,X3)
| ~ greater(age(X0,X4),sigma)
| ( X4 != X5 )
| ( X1 != X3 )
| ( X0 != X2 )
| ( age(X0,X1) != zero ) ),
inference(resolution_lifted,[status(thm)],[c_113,c_109]) ).
tcf(c_1070,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ organization(X0)
| ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ greater(age(X0,X2),sigma)
| ( age(X0,X1) != zero ) ),
inference(unflattening,[status(thm)],[c_1069]) ).
tcf(c_1072,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ organization(X0)
| ~ is_aligned(X0,X2)
| ( age(X0,X1) != zero )
| ~ greater(age(X0,X2),sigma) ),
inference(global_subsumption_just,[status(thm)],[c_1070,c_112,c_1070]) ).
tcf(c_1073,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ organization(X0)
| ~ is_aligned(X0,X2)
| ~ greater(age(X0,X2),sigma)
| ( age(X0,X1) != zero ) ),
inference(renaming,[status(thm)],[c_1072]) ).
tcf(c_1093,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( is_aligned(X2,X4)
| greater(age(X0,X5),sigma)
| ~ organization(X2)
| ~ is_aligned(X2,X3)
| ( X4 != X5 )
| ( X1 != X3 )
| ( X0 != X2 )
| ( age(X0,X1) != zero ) ),
inference(resolution_lifted,[status(thm)],[c_110,c_164]) ).
tcf(c_1094,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_aligned(X0,X2)
| greater(age(X0,X2),sigma)
| ~ organization(X0)
| ~ is_aligned(X0,X1)
| ( age(X0,X1) != zero ) ),
inference(unflattening,[status(thm)],[c_1093]) ).
tcf(c_1095,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_aligned(X0,X2)
| greater(age(X0,X2),sigma)
| ~ organization(X0)
| ( age(X0,X1) != zero ) ),
inference(global_subsumption_just,[status(thm)],[c_1094,c_112,c_1094]) ).
tcf(c_1134,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_aligned(X0,X2)
| greater(age(X0,X2),sigma)
| ( X0 != sk2 )
| ( age(X0,X1) != zero ) ),
inference(resolution_lifted,[status(thm)],[c_1095,c_130]) ).
tcf(c_1135,plain,
! [X0: $i,X1: $i] :
( is_aligned(sk2,X1)
| greater(age(sk2,X1),sigma)
| ( age(sk2,X0) != zero ) ),
inference(unflattening,[status(thm)],[c_1134]) ).
tcf(c_1146,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_aligned(X0,X2)
| ~ greater(age(X0,X2),sigma)
| ( X0 != sk2 )
| ( age(X0,X1) != zero ) ),
inference(resolution_lifted,[status(thm)],[c_1073,c_130]) ).
tcf(c_1147,plain,
! [X0: $i,X1: $i] :
( ~ is_aligned(sk2,X1)
| ~ greater(age(sk2,X1),sigma)
| ( age(sk2,X0) != zero ) ),
inference(unflattening,[status(thm)],[c_1146]) ).
tcf(c_1158,plain,
! [X0: $i,X1: $i] :
( positional_advantage(X0,X1)
| is_aligned(X0,X1)
| has_immunity(X0,X1)
| ( hazard_of_mortality(X0,X1) = high )
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_124,c_130]) ).
tcf(c_1159,plain,
! [X0: $i] :
( positional_advantage(sk2,X0)
| is_aligned(sk2,X0)
| has_immunity(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = high ) ),
inference(unflattening,[status(thm)],[c_1158]) ).
tcf(c_1160,plain,
! [X0: $i] :
( positional_advantage(sk2,X0)
| is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = high ) ),
inference(global_subsumption_just,[status(thm)],[c_1159,c_130,c_976]) ).
tcf(c_1184,plain,
! [X0: $i,X1: $i] :
( is_aligned(X0,X1)
| has_immunity(X0,X1)
| ( hazard_of_mortality(X0,X1) = mod1 )
| ~ positional_advantage(X0,X1)
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_122,c_130]) ).
tcf(c_1185,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| has_immunity(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = mod1 )
| ~ positional_advantage(sk2,X0) ),
inference(unflattening,[status(thm)],[c_1184]) ).
tcf(c_1186,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| ~ positional_advantage(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = mod1 ) ),
inference(global_subsumption_just,[status(thm)],[c_1185,c_1008]) ).
tcf(c_1187,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = mod1 )
| ~ positional_advantage(sk2,X0) ),
inference(renaming,[status(thm)],[c_1186]) ).
tcf(c_1197,plain,
! [X0: $i,X1: $i] :
( has_immunity(X0,X1)
| ( hazard_of_mortality(X0,X1) = low )
| ~ positional_advantage(X0,X1)
| ~ is_aligned(X0,X1)
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_121,c_130]) ).
tcf(c_1198,plain,
! [X0: $i] :
( has_immunity(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = low )
| ~ positional_advantage(sk2,X0)
| ~ is_aligned(sk2,X0) ),
inference(unflattening,[status(thm)],[c_1197]) ).
tcf(c_1199,plain,
! [X0: $i] :
( ~ is_aligned(sk2,X0)
| ~ positional_advantage(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = low ) ),
inference(global_subsumption_just,[status(thm)],[c_1198,c_1024]) ).
tcf(c_1200,plain,
! [X0: $i] :
( ( hazard_of_mortality(sk2,X0) = low )
| ~ positional_advantage(sk2,X0)
| ~ is_aligned(sk2,X0) ),
inference(renaming,[status(thm)],[c_1199]) ).
tcf(c_1395,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ fragile_position(X1)
| ~ fragile_position(X0)
| ~ smaller_or_equal(age(X0,X2),sigma)
| ~ greater(age(X1,X3),sigma)
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_115,c_116]) ).
tcf(c_1396,plain,
! [X0: $i,X1: $i] :
( ~ fragile_position(X0)
| ~ smaller_or_equal(age(X0,X1),sigma)
| ~ greater(age(X0,X1),sigma) ),
inference(unflattening,[status(thm)],[c_1395]) ).
tcf(c_1441,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( hazard_of_mortality(sk2,X2) = low )
| ~ fragile_position(X0)
| ~ is_aligned(sk2,X2)
| ~ smaller_or_equal(age(X0,X1),sigma)
| ( X1 != X2 )
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_115,c_1200]) ).
tcf(c_1442,plain,
! [X0: $i] :
( ( hazard_of_mortality(sk2,X0) = low )
| ~ fragile_position(sk2)
| ~ is_aligned(sk2,X0)
| ~ smaller_or_equal(age(sk2,X0),sigma) ),
inference(unflattening,[status(thm)],[c_1441]) ).
tcf(c_1444,plain,
! [X0: $i] :
( ( hazard_of_mortality(sk2,X0) = low )
| ~ smaller_or_equal(age(sk2,X0),sigma)
| ~ is_aligned(sk2,X0) ),
inference(global_subsumption_just,[status(thm)],[c_1442,c_131,c_1442]) ).
tcf(c_1445,plain,
! [X0: $i] :
( ( hazard_of_mortality(sk2,X0) = low )
| ~ is_aligned(sk2,X0)
| ~ smaller_or_equal(age(sk2,X0),sigma) ),
inference(renaming,[status(thm)],[c_1444]) ).
tcf(c_1456,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_aligned(sk2,X2)
| ( hazard_of_mortality(sk2,X2) = mod1 )
| ~ fragile_position(X0)
| ~ smaller_or_equal(age(X0,X1),sigma)
| ( X1 != X2 )
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_115,c_1187]) ).
tcf(c_1457,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = mod1 )
| ~ fragile_position(sk2)
| ~ smaller_or_equal(age(sk2,X0),sigma) ),
inference(unflattening,[status(thm)],[c_1456]) ).
tcf(c_1459,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = mod1 )
| ~ smaller_or_equal(age(sk2,X0),sigma) ),
inference(global_subsumption_just,[status(thm)],[c_1457,c_738,c_1008]) ).
tcf(c_1486,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_aligned(sk2,X2)
| ( hazard_of_mortality(sk2,X2) = high )
| ~ fragile_position(X0)
| ~ greater(age(X0,X1),sigma)
| ( X1 != X2 )
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_116,c_1160]) ).
tcf(c_1487,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = high )
| ~ fragile_position(sk2)
| ~ greater(age(sk2,X0),sigma) ),
inference(unflattening,[status(thm)],[c_1486]) ).
tcf(c_1489,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = high )
| ~ greater(age(sk2,X0),sigma) ),
inference(global_subsumption_just,[status(thm)],[c_1487,c_729,c_978]) ).
tcf(c_1545,plain,
! [X0: $i,X1: $i] :
( ~ smaller_or_equal(age(X0,X1),sigma)
| ~ greater(age(X0,X1),sigma)
| ( X0 != sk2 ) ),
inference(resolution_lifted,[status(thm)],[c_1396,c_131]) ).
tcf(c_1546,plain,
! [X0: $i] :
( ~ smaller_or_equal(age(sk2,X0),sigma)
| ~ greater(age(sk2,X0),sigma) ),
inference(unflattening,[status(thm)],[c_1545]) ).
tcf(c_2695,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ is_aligned(sk2,X0)
| ~ greater(age(sk2,X0),sigma) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_1147]) ).
tcf(c_2696,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( age(sk2,X0) != zero ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_1147]) ).
tcf(c_2697,plain,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1147]) ).
tcf(c_2698,plain,
! [X0: $i] :
( ~ iPr_def_12
| is_aligned(sk2,X0)
| greater(age(sk2,X0),sigma) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_1135]) ).
tcf(c_2699,plain,
( iPr_def_12
| iPr_def_11 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1135]) ).
tcf(c_2700,definition,
iPr_def_13 = hazard_of_mortality(sk2,sk3),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_2701,definition,
iPr_def_14 = hazard_of_mortality(sk2,sk4),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_2702,definition,
iPr_def_15 = hazard_of_mortality(sk2,sk5),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_2703,definition,
iPr_def_16 = age(sk2,sk5),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_2704,definition,
iPr_def_17 = age(sk2,sk4),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_2705,definition,
iPr_def_18 = age(sk2,sk3),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_2706,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = high )
| ~ greater(age(sk2,X0),sigma) ),
inference(demodulation,[status(thm)],[c_1489]) ).
tcf(c_2708,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| ( hazard_of_mortality(sk2,X0) = mod1 )
| ~ smaller_or_equal(age(sk2,X0),sigma) ),
inference(demodulation,[status(thm)],[c_1459]) ).
tcf(c_2709,plain,
! [X0: $i] :
( ( hazard_of_mortality(sk2,X0) = low )
| ~ is_aligned(sk2,X0)
| ~ smaller_or_equal(age(sk2,X0),sigma) ),
inference(demodulation,[status(thm)],[c_1445]) ).
tcf(c_2713,plain,
( iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_2697]) ).
tcf(c_2715,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ is_aligned(sk2,X0)
| ~ greater(age(sk2,X0),sigma) ),
inference(demodulation,[status(thm)],[c_2695]) ).
tcf(c_2716,plain,
( iPr_def_12
| iPr_def_11 ),
inference(demodulation,[status(thm)],[c_2699]) ).
tcf(c_2717,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( age(sk2,X0) != zero ) ),
inference(demodulation,[status(thm)],[c_2696]) ).
tcf(c_2718,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| greater(age(sk2,X0),sigma)
| ~ iPr_def_12 ),
inference(demodulation,[status(thm)],[c_2698]) ).
tcf(c_2719,negated_conjecture,
( ~ greater(iPr_def_15,iPr_def_14)
| ( iPr_def_13 != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_137,c_2702,c_2701,c_2700]) ).
tcf(c_2720,negated_conjecture,
greater(iPr_def_16,sigma),
inference(demodulation,[status(thm)],[c_136,c_2703]) ).
tcf(c_2721,negated_conjecture,
smaller_or_equal(iPr_def_17,sigma),
inference(demodulation,[status(thm)],[c_135,c_2704]) ).
tcf(c_2722,negated_conjecture,
greater(sigma,zero),
inference(demodulation,[status(thm)],[c_134]) ).
tcf(c_2723,negated_conjecture,
iPr_def_18 = zero,
inference(demodulation,[status(thm)],[c_133,c_2705]) ).
tcf(c_3135,plain,
greater(sigma,iPr_def_18),
inference(light_normalisation,[status(thm)],[c_2722,c_2723]) ).
tcf(c_3146,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( age(sk2,X0) != iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_2717,c_2723]) ).
tcf(c_3203,plain,
( is_aligned(sk2,sk5)
| ( hazard_of_mortality(sk2,sk5) = high )
| ~ greater(iPr_def_16,sigma) ),
inference(superposition,[status(thm)],[c_2703,c_2706]) ).
tcf(c_3204,plain,
( ~ iPr_def_10
| ~ greater(iPr_def_16,sigma)
| ~ is_aligned(sk2,sk5) ),
inference(superposition,[status(thm)],[c_2703,c_2715]) ).
tcf(c_3212,plain,
( ~ iPr_def_10
| ~ is_aligned(sk2,sk5) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3204,c_2720]) ).
tcf(c_3215,plain,
( is_aligned(sk2,sk5)
| ( high = iPr_def_15 )
| ~ greater(iPr_def_16,sigma) ),
inference(light_normalisation,[status(thm)],[c_3203,c_2702]) ).
tcf(c_3216,plain,
( is_aligned(sk2,sk5)
| ( high = iPr_def_15 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3215,c_2720]) ).
tcf(c_3252,plain,
~ iPr_def_11,
inference(superposition,[status(thm)],[c_2705,c_3146]) ).
tcf(c_3256,plain,
iPr_def_12,
inference(backward_subsumption_resolution,[status(thm)],[c_2716,c_3252]) ).
tcf(c_3257,plain,
iPr_def_10,
inference(backward_subsumption_resolution,[status(thm)],[c_2713,c_3252]) ).
tcf(c_3285,plain,
high = iPr_def_15,
inference(global_subsumption_just,[status(thm)],[c_3216,c_3212,c_3216,c_3257]) ).
tcf(c_3289,plain,
greater(iPr_def_15,mod2),
inference(demodulation,[status(thm)],[c_128,c_3285]) ).
tcf(c_3319,plain,
smaller(iPr_def_18,sigma),
inference(superposition,[status(thm)],[c_3135,c_102]) ).
tcf(c_3374,plain,
smaller_or_equal(iPr_def_18,sigma),
inference(superposition,[status(thm)],[c_3319,c_96]) ).
tcf(c_3422,plain,
! [X0: $i] :
( greater(iPr_def_15,X0)
| ~ greater(mod2,X0) ),
inference(superposition,[status(thm)],[c_3289,c_104]) ).
tcf(c_3526,plain,
greater(iPr_def_15,low),
inference(superposition,[status(thm)],[c_129,c_3422]) ).
tcf(c_4126,plain,
! [X0: $i] :
( is_aligned(sk2,X0)
| ~ smaller_or_equal(age(sk2,X0),sigma) ),
inference(global_subsumption_just,[status(thm)],[c_2708,c_1546,c_2718,c_3256]) ).
tcf(c_4191,plain,
! [X0: $i] :
( ( hazard_of_mortality(sk2,X0) = low )
| ~ smaller_or_equal(age(sk2,X0),sigma) ),
inference(global_subsumption_just,[status(thm)],[c_2709,c_738,c_1024,c_4126]) ).
tcf(c_4200,plain,
( ( hazard_of_mortality(sk2,sk3) = low )
| ~ smaller_or_equal(iPr_def_18,sigma) ),
inference(superposition,[status(thm)],[c_2705,c_4191]) ).
tcf(c_4201,plain,
( ( hazard_of_mortality(sk2,sk4) = low )
| ~ smaller_or_equal(iPr_def_17,sigma) ),
inference(superposition,[status(thm)],[c_2704,c_4191]) ).
tcf(c_4203,plain,
( ( low = iPr_def_14 )
| ~ smaller_or_equal(iPr_def_17,sigma) ),
inference(light_normalisation,[status(thm)],[c_4201,c_2701]) ).
tcf(c_4204,plain,
low = iPr_def_14,
inference(forward_subsumption_resolution,[status(thm)],[c_4203,c_2721]) ).
tcf(c_4205,plain,
( ( low = iPr_def_13 )
| ~ smaller_or_equal(iPr_def_18,sigma) ),
inference(light_normalisation,[status(thm)],[c_4200,c_2700]) ).
tcf(c_4206,plain,
low = iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_4205,c_3374]) ).
tcf(c_4218,plain,
greater(iPr_def_15,iPr_def_14),
inference(demodulation,[status(thm)],[c_3526,c_4204]) ).
tcf(c_4231,plain,
iPr_def_13 != iPr_def_14,
inference(backward_subsumption_resolution,[status(thm)],[c_2719,c_4218]) ).
tcf(c_4260,plain,
iPr_def_13 = iPr_def_14,
inference(demodulation,[status(thm)],[c_4204,c_4206]) ).
tcf(c_4262,plain,
$false,
inference(ground_joinability,[status(thm)],[c_4231,c_4260]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT061-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/5.56 % Computer : n003.cluster.edu
% 0.10/5.56 % Model : x86_64 x86_64
% 0.10/5.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.56 % Memory : 8046.5625MB
% 0.10/5.56 % OS : Linux 6.8.0-71-generic
% 0.10/5.56 % CPULimit : 300
% 0.10/5.56 % WCLimit : 300
% 0.10/5.56 % DateTime : Thu Sep 24 01:18:41 UTC 2026
% 0.10/5.57 % CPUTime :
% 0.10/5.57 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/5.60 Running first-order theorem proving
% 0.14/5.60 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/5.62
% 0.14/5.62 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.62
% 0.14/5.62 % Detected problem language: tptp
% 0.14/5.63 % Proving...
% 3.05/6.48 % SZS status Started for theBenchmark.p
% 3.05/6.48 % SZS status Unsatisfiable for theBenchmark.p
% 3.05/6.48
% 3.05/6.48 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.05/6.48
% 3.05/6.48 % ------ iProver source info
% 3.05/6.48
% 3.05/6.48 % git: date: 2026-07-19 20:42:38 +0200
% 3.05/6.48 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.05/6.48 % git: non_committed_changes: false
% 3.05/6.48
% 3.05/6.48 % ------ Parsing...% successful
% 3.05/6.48
% 3.05/6.48
% 3.05/6.48 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.05/6.48
% 3.05/6.48 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 4 0s sf_e pe_s pe_e %
% 3.05/6.48
% 3.05/6.48 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.05/6.48
% 3.05/6.48 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 3.05/6.48 % ------ Proving...
% 3.05/6.48 % ------ Problem Properties
% 3.05/6.48
% 3.05/6.48 %
% 3.05/6.48 % clauses 39
% 3.05/6.48 % conjectures 6
% 3.05/6.48 % EPR 21
% 3.05/6.48 % Horn 29
% 3.05/6.48 % unary 17
% 3.05/6.48 % binary 9
% 3.05/6.48 % lits 74
% 3.05/6.48 % lits eq 20
% 3.05/6.48 % fd_pure 0
% 3.05/6.48 % fd_pseudo 0
% 3.05/6.48 % fd_cond 0
% 3.05/6.48 % fd_pseudo_cond 2
% 3.05/6.48 % AC symbols 0
% 3.05/6.48
% 3.05/6.48 % ------ Schedule dynamic 5 is on
% 3.05/6.48
% 3.05/6.48 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 3.05/6.48
% 3.05/6.48
% 3.05/6.48 % ------
% 3.05/6.48 % Current options:
% 3.05/6.48 % ------
% 3.05/6.48
% 3.05/6.48
% 3.05/6.48 %
% 3.05/6.48
% 3.05/6.48 % ------ Proving...
% 3.05/6.48 %
% 3.05/6.48
% 3.05/6.48 % SZS status Unsatisfiable for theBenchmark.p
% 3.05/6.48
% 3.05/6.48 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.05/6.48
% 3.05/6.48
%------------------------------------------------------------------------------