%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : MGT042-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n018.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:53 PM UTC 2026
% Result : Unsatisfiable 8.70s 1.90s
% Output : CNFRefutation 8.70s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f43ERROR: Could not build tree for root c_3511ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( X0 = X1
| smaller(X0,X1)
| ~ smaller_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax',definition_smaller_or_equal_1) ).
fof(f3,axiom,
! [X0,X1] :
( smaller_or_equal(X0,X1)
| X0 != X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax',definition_smaller_or_equal_3) ).
fof(f4,axiom,
! [X0,X1] :
( X0 = X1
| greater(X0,X1)
| ~ greater_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax',definition_greater_or_equal_4) ).
fof(f5,axiom,
! [X0,X1] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax',definition_greater_or_equal_5) ).
fof(f6,axiom,
! [X0,X1] :
( greater_or_equal(X0,X1)
| X0 != X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax',definition_greater_or_equal_6) ).
fof(f7,axiom,
! [X0,X1] :
( greater(X1,X0)
| ~ smaller(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax',definition_smaller_7) ).
fof(f8,axiom,
! [X0,X1] :
( smaller(X1,X0)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax',definition_smaller_8) ).
fof(f9,axiom,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax',meaning_postulate_greater_strict_9) ).
fof(f12,axiom,
! [X2,X0,X1] :
( smaller(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1))
| ~ greater_or_equal(position(X0,X2),position(X0,X1))
| ~ greater(capability(X0,X2),capability(X0,X1))
| has_immunity(X0,X2)
| has_immunity(X0,X1)
| ~ organization(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_4_38) ).
fof(f13,axiom,
! [X2,X0,X1] :
( smaller(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1))
| ~ greater(position(X0,X2),position(X0,X1))
| ~ greater_or_equal(capability(X0,X2),capability(X0,X1))
| has_immunity(X0,X2)
| has_immunity(X0,X1)
| ~ organization(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_4_39) ).
fof(f15,axiom,
! [X2,X0,X1] :
( greater(capability(X0,X1),capability(X0,X2))
| ~ smaller_or_equal(internal_friction(X0,X1),internal_friction(X0,X2))
| ~ greater(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))
| ~ organization(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_5_41) ).
fof(f16,axiom,
! [X2,X0,X1] :
( smaller(capability(X0,X1),capability(X0,X2))
| ~ greater(internal_friction(X0,X1),internal_friction(X0,X2))
| ~ smaller_or_equal(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))
| ~ organization(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_5_42) ).
fof(f17,axiom,
! [X2,X0,X1] :
( capability(X0,X1) = capability(X0,X2)
| internal_friction(X0,X1) != internal_friction(X0,X2)
| stock_of_knowledge(X0,X1) != stock_of_knowledge(X0,X2)
| ~ organization(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_5_43) ).
fof(f18,plain,
! [X2,X0,X1] :
( capability(X0,X2) = capability(X0,X1)
| internal_friction(X0,X1) != internal_friction(X0,X2)
| stock_of_knowledge(X0,X1) != stock_of_knowledge(X0,X2)
| ~ organization(X0) ),
inference(reorient_equations,[],[f17]) ).
fof(f19,axiom,
! [X2,X0,X1] :
( greater(position(X0,X1),position(X0,X2))
| ~ greater(external_ties(X0,X1),external_ties(X0,X2))
| ~ organization(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_6_44) ).
fof(f20,axiom,
! [X2,X0,X1] :
( position(X0,X1) = position(X0,X2)
| external_ties(X0,X1) != external_ties(X0,X2)
| ~ organization(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_6_45) ).
fof(f21,plain,
! [X2,X0,X1] :
( position(X0,X2) = position(X0,X1)
| external_ties(X0,X1) != external_ties(X0,X2)
| ~ organization(X0) ),
inference(reorient_equations,[],[f20]) ).
fof(f22,negated_conjecture,
organization(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemma_1_46) ).
fof(f23,negated_conjecture,
~ has_immunity(sk1,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemma_1_47) ).
fof(f24,negated_conjecture,
~ has_immunity(sk1,sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemma_1_48) ).
fof(f25,negated_conjecture,
( greater_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))
| greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemma_1_49) ).
fof(f27,negated_conjecture,
( greater(external_ties(sk1,sk3),external_ties(sk1,sk2))
| greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemma_1_51) ).
fof(f33,negated_conjecture,
( greater(external_ties(sk1,sk3),external_ties(sk1,sk2))
| greater_or_equal(external_ties(sk1,sk3),external_ties(sk1,sk2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemma_1_57) ).
fof(f41,plain,
! [X1] : smaller_or_equal(X1,X1),
inference(equality_resolution,[],[f3]) ).
fof(f42,plain,
! [X1] : greater_or_equal(X1,X1),
inference(equality_resolution,[],[f6]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i] :
( smaller(X0,X1)
| ( X0 = X1 )
| ~ smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_89,plain,
! [X0: $i] : smaller_or_equal(X0,X0),
inference(cnf_transformation,[],[f41]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i] :
( greater(X0,X1)
| ( X0 = X1 )
| ~ greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_92,plain,
! [X0: $i] : greater_or_equal(X0,X0),
inference(cnf_transformation,[],[f42]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] :
( greater(X1,X0)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i] :
( smaller(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i] :
( has_immunity(X0,X2)
| has_immunity(X0,X1)
| smaller(hazard_of_mortality(X0,X1),hazard_of_mortality(X0,X2))
| ~ organization(X0)
| ~ greater_or_equal(position(X0,X1),position(X0,X2))
| ~ greater(capability(X0,X1),capability(X0,X2)) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i,X2: $i] :
( has_immunity(X0,X2)
| has_immunity(X0,X1)
| smaller(hazard_of_mortality(X0,X1),hazard_of_mortality(X0,X2))
| ~ organization(X0)
| ~ greater_or_equal(capability(X0,X1),capability(X0,X2))
| ~ greater(position(X0,X1),position(X0,X2)) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(capability(X0,X1),capability(X0,X2))
| ~ organization(X0)
| ~ smaller_or_equal(internal_friction(X0,X1),internal_friction(X0,X2))
| ~ greater(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2)) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] :
( smaller(capability(X0,X1),capability(X0,X2))
| ~ organization(X0)
| ~ smaller_or_equal(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))
| ~ greater(internal_friction(X0,X1),internal_friction(X0,X2)) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( capability(X0,X1) = capability(X0,X2) )
| ~ organization(X0)
| ( internal_friction(X0,X1) != internal_friction(X0,X2) )
| ( stock_of_knowledge(X0,X1) != stock_of_knowledge(X0,X2) ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(position(X0,X1),position(X0,X2))
| ~ organization(X0)
| ~ greater(external_ties(X0,X1),external_ties(X0,X2)) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( position(X0,X1) = position(X0,X2) )
| ~ organization(X0)
| ( external_ties(X0,X1) != external_ties(X0,X2) ) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_106,negated_conjecture,
organization(sk1),
inference(cnf_transformation,[],[f22]) ).
tcf(c_107,negated_conjecture,
~ has_immunity(sk1,sk2),
inference(cnf_transformation,[],[f23]) ).
tcf(c_108,negated_conjecture,
~ has_immunity(sk1,sk3),
inference(cnf_transformation,[],[f24]) ).
tcf(c_109,negated_conjecture,
( greater_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))
| greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_111,negated_conjecture,
( greater(external_ties(sk1,sk3),external_ties(sk1,sk2))
| greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_114,negated_conjecture,
smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2)),
inference(cnf_transformation,[],[f43]) ).
tcf(c_117,negated_conjecture,
( greater_or_equal(external_ties(sk1,sk3),external_ties(sk1,sk2))
| greater(external_ties(sk1,sk3),external_ties(sk1,sk2)) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_124,negated_conjecture,
~ smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)),
inference(cnf_transformation,[],[f44]) ).
tcf(c_182,plain,
greater_or_equal(external_ties(sk1,sk3),external_ties(sk1,sk2)),
inference(backward_subsumption_resolution,[status(thm)],[c_117,c_91]) ).
tcf(c_183,plain,
greater_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)),
inference(backward_subsumption_resolution,[status(thm)],[c_109,c_91]) ).
tcf(c_448,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( position(X0,X1) = position(X0,X2) )
| ( X0 != sk1 )
| ( external_ties(X0,X1) != external_ties(X0,X2) ) ),
inference(resolution_lifted,[status(thm)],[c_105,c_106]) ).
tcf(c_449,plain,
! [X0: $i,X1: $i] :
( ( position(sk1,X0) = position(sk1,X1) )
| ( external_ties(sk1,X0) != external_ties(sk1,X1) ) ),
inference(unflattening,[status(thm)],[c_448]) ).
tcf(c_457,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(position(X0,X1),position(X0,X2))
| ~ greater(external_ties(X0,X1),external_ties(X0,X2))
| ( X0 != sk1 ) ),
inference(resolution_lifted,[status(thm)],[c_104,c_106]) ).
tcf(c_458,plain,
! [X0: $i,X1: $i] :
( greater(position(sk1,X0),position(sk1,X1))
| ~ greater(external_ties(sk1,X0),external_ties(sk1,X1)) ),
inference(unflattening,[status(thm)],[c_457]) ).
tcf(c_466,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( capability(X0,X1) = capability(X0,X2) )
| ( X0 != sk1 )
| ( internal_friction(X0,X1) != internal_friction(X0,X2) )
| ( stock_of_knowledge(X0,X1) != stock_of_knowledge(X0,X2) ) ),
inference(resolution_lifted,[status(thm)],[c_103,c_106]) ).
tcf(c_467,plain,
! [X0: $i,X1: $i] :
( ( capability(sk1,X0) = capability(sk1,X1) )
| ( internal_friction(sk1,X0) != internal_friction(sk1,X1) )
| ( stock_of_knowledge(sk1,X0) != stock_of_knowledge(sk1,X1) ) ),
inference(unflattening,[status(thm)],[c_466]) ).
tcf(c_478,plain,
! [X0: $i,X1: $i,X2: $i] :
( smaller(capability(X0,X1),capability(X0,X2))
| ~ smaller_or_equal(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))
| ~ greater(internal_friction(X0,X1),internal_friction(X0,X2))
| ( X0 != sk1 ) ),
inference(resolution_lifted,[status(thm)],[c_102,c_106]) ).
tcf(c_479,plain,
! [X0: $i,X1: $i] :
( smaller(capability(sk1,X0),capability(sk1,X1))
| ~ smaller_or_equal(stock_of_knowledge(sk1,X0),stock_of_knowledge(sk1,X1))
| ~ greater(internal_friction(sk1,X0),internal_friction(sk1,X1)) ),
inference(unflattening,[status(thm)],[c_478]) ).
tcf(c_490,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(capability(X0,X1),capability(X0,X2))
| ~ smaller_or_equal(internal_friction(X0,X1),internal_friction(X0,X2))
| ~ greater(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))
| ( X0 != sk1 ) ),
inference(resolution_lifted,[status(thm)],[c_101,c_106]) ).
tcf(c_491,plain,
! [X0: $i,X1: $i] :
( greater(capability(sk1,X0),capability(sk1,X1))
| ~ smaller_or_equal(internal_friction(sk1,X0),internal_friction(sk1,X1))
| ~ greater(stock_of_knowledge(sk1,X0),stock_of_knowledge(sk1,X1)) ),
inference(unflattening,[status(thm)],[c_490]) ).
tcf(c_520,plain,
! [X0: $i,X1: $i,X2: $i] :
( has_immunity(X0,X2)
| has_immunity(X0,X1)
| smaller(hazard_of_mortality(X0,X1),hazard_of_mortality(X0,X2))
| ~ greater_or_equal(capability(X0,X1),capability(X0,X2))
| ~ greater(position(X0,X1),position(X0,X2))
| ( X0 != sk1 ) ),
inference(resolution_lifted,[status(thm)],[c_99,c_106]) ).
tcf(c_521,plain,
! [X0: $i,X1: $i] :
( has_immunity(sk1,X1)
| has_immunity(sk1,X0)
| smaller(hazard_of_mortality(sk1,X0),hazard_of_mortality(sk1,X1))
| ~ greater_or_equal(capability(sk1,X0),capability(sk1,X1))
| ~ greater(position(sk1,X0),position(sk1,X1)) ),
inference(unflattening,[status(thm)],[c_520]) ).
tcf(c_538,plain,
! [X0: $i,X1: $i,X2: $i] :
( has_immunity(X0,X2)
| has_immunity(X0,X1)
| smaller(hazard_of_mortality(X0,X1),hazard_of_mortality(X0,X2))
| ~ greater_or_equal(position(X0,X1),position(X0,X2))
| ~ greater(capability(X0,X1),capability(X0,X2))
| ( X0 != sk1 ) ),
inference(resolution_lifted,[status(thm)],[c_98,c_106]) ).
tcf(c_539,plain,
! [X0: $i,X1: $i] :
( has_immunity(sk1,X1)
| has_immunity(sk1,X0)
| smaller(hazard_of_mortality(sk1,X0),hazard_of_mortality(sk1,X1))
| ~ greater_or_equal(position(sk1,X0),position(sk1,X1))
| ~ greater(capability(sk1,X0),capability(sk1,X1)) ),
inference(unflattening,[status(thm)],[c_538]) ).
tcf(c_2289,plain,
( greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))
| greater(position(sk1,sk3),position(sk1,sk2)) ),
inference(superposition,[status(thm)],[c_111,c_458]) ).
tcf(c_2302,plain,
( smaller(internal_friction(sk1,sk3),internal_friction(sk1,sk2))
| ( internal_friction(sk1,sk2) = internal_friction(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_114,c_87]) ).
tcf(c_2311,plain,
( greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))
| ( stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_183,c_90]) ).
tcf(c_2312,plain,
( greater(external_ties(sk1,sk3),external_ties(sk1,sk2))
| ( external_ties(sk1,sk2) = external_ties(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_182,c_90]) ).
tcf(c_2321,plain,
( greater(capability(sk1,sk3),capability(sk1,sk2))
| ( stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) )
| ~ smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2)) ),
inference(superposition,[status(thm)],[c_2311,c_491]) ).
tcf(c_2322,plain,
( greater(capability(sk1,sk3),capability(sk1,sk2))
| ( stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) ) ),
inference(global_subsumption_just,[status(thm)],[c_2321,c_114,c_2321]) ).
tcf(c_2328,plain,
( greater(position(sk1,sk3),position(sk1,sk2))
| ( external_ties(sk1,sk2) = external_ties(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_2312,c_458]) ).
tcf(c_2333,plain,
( has_immunity(sk1,sk3)
| has_immunity(sk1,sk2)
| smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))
| ( stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) )
| ~ greater_or_equal(position(sk1,sk3),position(sk1,sk2)) ),
inference(superposition,[status(thm)],[c_2322,c_539]) ).
tcf(c_2334,plain,
( ~ greater_or_equal(position(sk1,sk3),position(sk1,sk2))
| ( stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) ) ),
inference(global_subsumption_just,[status(thm)],[c_2333,c_108,c_107,c_124,c_2333]) ).
tcf(c_2335,plain,
( ( stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) )
| ~ greater_or_equal(position(sk1,sk3),position(sk1,sk2)) ),
inference(renaming,[status(thm)],[c_2334]) ).
tcf(c_2350,plain,
( greater_or_equal(position(sk1,sk3),position(sk1,sk2))
| ( external_ties(sk1,sk2) = external_ties(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_2328,c_91]) ).
tcf(c_2371,plain,
( greater(internal_friction(sk1,sk2),internal_friction(sk1,sk3))
| ( internal_friction(sk1,sk2) = internal_friction(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_2302,c_93]) ).
tcf(c_2378,plain,
( smaller(external_ties(sk1,sk2),external_ties(sk1,sk3))
| greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ),
inference(superposition,[status(thm)],[c_111,c_94]) ).
tcf(c_2380,plain,
( smaller(position(sk1,sk2),position(sk1,sk3))
| greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ),
inference(superposition,[status(thm)],[c_2289,c_94]) ).
tcf(c_2406,plain,
( greater(position(sk1,sk3),position(sk1,sk2))
| ~ greater(external_ties(sk1,sk3),external_ties(sk1,sk2)) ),
inference(instantiation,[status(thm)],[c_458]) ).
tcf(c_2462,plain,
( smaller(external_ties(sk1,sk2),external_ties(sk1,sk3))
| ~ greater(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,sk3)) ),
inference(superposition,[status(thm)],[c_2378,c_95]) ).
tcf(c_2489,plain,
( smaller(capability(sk1,sk2),capability(sk1,sk3))
| ( internal_friction(sk1,sk2) = internal_friction(sk1,sk3) )
| ~ smaller_or_equal(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,sk3)) ),
inference(superposition,[status(thm)],[c_2371,c_479]) ).
tcf(c_2511,plain,
( greater_or_equal(position(sk1,sk3),position(sk1,sk2))
| ~ greater(position(sk1,sk3),position(sk1,sk2)) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_2517,plain,
( has_immunity(sk1,sk3)
| has_immunity(sk1,sk2)
| smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))
| ~ greater_or_equal(capability(sk1,sk3),capability(sk1,sk2))
| ~ greater(position(sk1,sk3),position(sk1,sk2)) ),
inference(instantiation,[status(thm)],[c_521]) ).
tcf(c_2519,plain,
( smaller(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,sk3))
| smaller(position(sk1,sk2),position(sk1,sk3)) ),
inference(superposition,[status(thm)],[c_2380,c_94]) ).
tcf(c_2548,plain,
( greater(external_ties(sk1,sk3),external_ties(sk1,sk2))
| ~ smaller(external_ties(sk1,sk2),external_ties(sk1,sk3)) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_2616,plain,
( ( external_ties(sk1,sk2) = external_ties(sk1,sk3) )
| ( stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_2350,c_2335]) ).
tcf(c_2670,plain,
! [X0: $i] :
( ( stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) )
| ( position(sk1,X0) = position(sk1,sk2) )
| ( external_ties(sk1,X0) != external_ties(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_2616,c_449]) ).
tcf(c_2729,plain,
( ( stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) )
| ( position(sk1,sk2) = position(sk1,sk3) ) ),
inference(equality_resolution,[status(thm)],[c_2670]) ).
tcf(c_2745,plain,
( ( stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) )
| ~ greater_or_equal(position(sk1,sk3),position(sk1,sk3)) ),
inference(superposition,[status(thm)],[c_2729,c_2335]) ).
tcf(c_2919,plain,
( has_immunity(sk1,sk3)
| has_immunity(sk1,sk2)
| smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))
| ~ greater_or_equal(position(sk1,sk3),position(sk1,sk2))
| ~ greater(capability(sk1,sk3),capability(sk1,sk2)) ),
inference(instantiation,[status(thm)],[c_539]) ).
tcf(c_2971,plain,
( smaller(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,sk3))
| greater(position(sk1,sk3),position(sk1,sk2)) ),
inference(superposition,[status(thm)],[c_2519,c_93]) ).
tcf(c_3058,plain,
stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3),
inference(superposition,[status(thm)],[c_92,c_2745]) ).
tcf(c_3063,plain,
( smaller(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk3))
| greater(position(sk1,sk3),position(sk1,sk2)) ),
inference(demodulation,[status(thm)],[c_2971,c_3058]) ).
tcf(c_3067,plain,
( smaller(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk3))
| greater_or_equal(position(sk1,sk3),position(sk1,sk2)) ),
inference(superposition,[status(thm)],[c_3063,c_91]) ).
tcf(c_3122,plain,
( smaller(capability(sk1,sk2),capability(sk1,sk3))
| ( internal_friction(sk1,sk2) = internal_friction(sk1,sk3) )
| ~ smaller_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk3)) ),
inference(superposition,[status(thm)],[c_3058,c_2489]) ).
tcf(c_3123,plain,
( smaller(external_ties(sk1,sk2),external_ties(sk1,sk3))
| ~ greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk3)) ),
inference(superposition,[status(thm)],[c_3058,c_2462]) ).
tcf(c_3125,plain,
( smaller(external_ties(sk1,sk2),external_ties(sk1,sk3))
| greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk3)) ),
inference(superposition,[status(thm)],[c_3058,c_2378]) ).
tcf(c_3130,plain,
! [X0: $i] :
( ( capability(sk1,X0) = capability(sk1,sk2) )
| ( internal_friction(sk1,X0) != internal_friction(sk1,sk2) )
| ( stock_of_knowledge(sk1,X0) != stock_of_knowledge(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_3058,c_467]) ).
tcf(c_3135,plain,
smaller(external_ties(sk1,sk2),external_ties(sk1,sk3)),
inference(global_subsumption_just,[status(thm)],[c_3123,c_3125,c_3123]) ).
tcf(c_3282,plain,
( smaller(capability(sk1,sk2),capability(sk1,sk3))
| ( internal_friction(sk1,sk2) = internal_friction(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_89,c_3122]) ).
tcf(c_3316,plain,
( greater(capability(sk1,sk3),capability(sk1,sk2))
| ( internal_friction(sk1,sk2) = internal_friction(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_3282,c_93]) ).
tcf(c_3320,plain,
internal_friction(sk1,sk2) = internal_friction(sk1,sk3),
inference(global_subsumption_just,[status(thm)],[c_3316,c_108,c_107,c_124,c_2406,c_2511,c_2548,c_2919,c_3135,c_3316]) ).
tcf(c_3322,plain,
! [X0: $i] :
( ( capability(sk1,X0) = capability(sk1,sk2) )
| ( internal_friction(sk1,X0) != internal_friction(sk1,sk3) )
| ( stock_of_knowledge(sk1,X0) != stock_of_knowledge(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_3320,c_3130]) ).
tcf(c_3356,plain,
( smaller(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk3))
| greater(position(sk1,sk3),position(sk1,sk2))
| ( position(sk1,sk2) = position(sk1,sk3) ) ),
inference(superposition,[status(thm)],[c_3067,c_90]) ).
tcf(c_3357,plain,
greater(position(sk1,sk3),position(sk1,sk2)),
inference(global_subsumption_just,[status(thm)],[c_3356,c_2406,c_2548,c_3125,c_3123]) ).
tcf(c_3368,plain,
( has_immunity(sk1,sk3)
| has_immunity(sk1,sk2)
| smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))
| ~ greater_or_equal(capability(sk1,sk3),capability(sk1,sk2)) ),
inference(superposition,[status(thm)],[c_3357,c_521]) ).
tcf(c_3372,plain,
~ greater_or_equal(capability(sk1,sk3),capability(sk1,sk2)),
inference(global_subsumption_just,[status(thm)],[c_3368,c_108,c_107,c_124,c_2406,c_2517,c_2548,c_3125,c_3123]) ).
tcf(c_3441,plain,
( ( capability(sk1,sk2) = capability(sk1,sk3) )
| ( internal_friction(sk1,sk3) != internal_friction(sk1,sk3) ) ),
inference(equality_resolution,[status(thm)],[c_3322]) ).
tcf(c_3442,plain,
capability(sk1,sk2) = capability(sk1,sk3),
inference(equality_resolution_simp,[status(thm)],[c_3441]) ).
tcf(c_3445,plain,
~ greater_or_equal(capability(sk1,sk3),capability(sk1,sk3)),
inference(superposition,[status(thm)],[c_3442,c_3372]) ).
tcf(c_3511,plain,
$false,
inference(superposition,[status(thm)],[c_92,c_3445]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT042-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.37 % Computer : n018.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 01:12:32 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.43 % Proving...
% 8.70/1.90 % SZS status Started for theBenchmark.p
% 8.70/1.90 % SZS status Unsatisfiable for theBenchmark.p
% 8.70/1.90
% 8.70/1.90 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.70/1.90
% 8.70/1.90 % ------ iProver source info
% 8.70/1.90
% 8.70/1.90 % git: date: 2026-07-19 20:42:38 +0200
% 8.70/1.90 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.70/1.90 % git: non_committed_changes: false
% 8.70/1.90
% 8.70/1.90 % ------ Parsing...% successful
% 8.70/1.90
% 8.70/1.90
% 8.70/1.90 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.70/1.90
% 8.70/1.90 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 8.70/1.90
% 8.70/1.90 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.70/1.90
% 8.70/1.90 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 8.70/1.90 % ------ Proving...
% 8.70/1.90 % ------ Problem Properties
% 8.70/1.90
% 8.70/1.90 %
% 8.70/1.90 % clauses 26
% 8.70/1.90 % conjectures 5
% 8.70/1.90 % EPR 13
% 8.70/1.90 % Horn 19
% 8.70/1.90 % unary 8
% 8.70/1.90 % binary 8
% 8.70/1.90 % lits 60
% 8.70/1.90 % lits eq 11
% 8.70/1.90 % fd_pure 0
% 8.70/1.90 % fd_pseudo 0
% 8.70/1.90 % fd_cond 0
% 8.70/1.90 % fd_pseudo_cond 3
% 8.70/1.90 % AC symbols 0
% 8.70/1.90
% 8.70/1.90 % ------ Input Options Time Limit: Unbounded
% 8.70/1.90
% 8.70/1.90
% 8.70/1.90 % ------
% 8.70/1.90 % Current options:
% 8.70/1.90 % ------
% 8.70/1.90
% 8.70/1.90
% 8.70/1.90 %
% 8.70/1.90
% 8.70/1.90 % ------ Proving...
% 8.70/1.90 %
% 8.70/1.90
% 8.70/1.90 % SZS status Unsatisfiable for theBenchmark.p
% 8.70/1.90
% 8.70/1.90 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.70/1.90
% 8.70/1.90
%------------------------------------------------------------------------------