%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT042+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 : Sun Sep 27 08:01:20 AM UTC 2026
% Result : Theorem 27.38s 4.08s
% Output : CNFRefutation 27.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT042+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 00:08:44 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.38/4.08 % SZS status Theorem for theBenchmark.p
% 27.38/4.08 % SZS output start CNFRefutation for theBenchmark.p
% 27.38/4.08 fof(assumption_4, axiom, ! [X0] : ! [X1] : ! [X2] : (((organization(X0) & (~'has$uimmunity'(X0,X1) & ~'has$uimmunity'(X0,X2))) => (((greater(capability(X0,X2),capability(X0,X1)) & 'greater$uor$uequal'(position(X0,X2),position(X0,X1))) => smaller('hazard$uof$umortality'(X0,X2),'hazard$uof$umortality'(X0,X1))) & ((('greater$uor$uequal'(capability(X0,X2),capability(X0,X1)) & greater(position(X0,X2),position(X0,X1))) => smaller('hazard$uof$umortality'(X0,X2),'hazard$uof$umortality'(X0,X1))) & ((capability(X0,X2) = capability(X0,X1) & position(X0,X2) = position(X0,X1)) => 'hazard$uof$umortality'(X0,X2) = 'hazard$uof$umortality'(X0,X1))))))).
% 27.38/4.08 fof(assumption_5, axiom, ! [X0] : ! [X1] : ! [X2] : ((organization(X0) => (((greater('stock$uof$uknowledge'(X0,X2),'stock$uof$uknowledge'(X0,X1)) & 'smaller$uor$uequal'('internal$ufriction'(X0,X2),'internal$ufriction'(X0,X1))) => greater(capability(X0,X2),capability(X0,X1))) & ((('smaller$uor$uequal'('stock$uof$uknowledge'(X0,X2),'stock$uof$uknowledge'(X0,X1)) & greater('internal$ufriction'(X0,X2),'internal$ufriction'(X0,X1))) => smaller(capability(X0,X2),capability(X0,X1))) & (('stock$uof$uknowledge'(X0,X2) = 'stock$uof$uknowledge'(X0,X1) & 'internal$ufriction'(X0,X2) = 'internal$ufriction'(X0,X1)) => capability(X0,X2) = capability(X0,X1))))))).
% 27.38/4.08 fof(assumption_6, axiom, ! [X0] : ! [X1] : ! [X2] : ((organization(X0) => ((greater('external$uties'(X0,X2),'external$uties'(X0,X1)) => greater(position(X0,X2),position(X0,X1))) & ('external$uties'(X0,X2) = 'external$uties'(X0,X1) => position(X0,X2) = position(X0,X1)))))).
% 27.38/4.08 fof(definition_smaller_or_equal, axiom, ! [X0] : ! [X1] : (('smaller$uor$uequal'(X0,X1) <=> (smaller(X0,X1) | X0 = X1)))).
% 27.38/4.08 fof(definition_greater_or_equal, axiom, ! [X0] : ! [X1] : (('greater$uor$uequal'(X0,X1) <=> (greater(X0,X1) | X0 = X1)))).
% 27.38/4.08 fof(definition_smaller, axiom, ! [X0] : ! [X1] : ((smaller(X0,X1) <=> greater(X1,X0)))).
% 27.38/4.08 fof(lemma_1, conjecture, ! [X0] : ! [X1] : ! [X2] : (((organization(X0) & (~'has$uimmunity'(X0,X1) & ~'has$uimmunity'(X0,X2))) => (((greater('stock$uof$uknowledge'(X0,X2),'stock$uof$uknowledge'(X0,X1)) & ('smaller$uor$uequal'('internal$ufriction'(X0,X2),'internal$ufriction'(X0,X1)) & 'greater$uor$uequal'('external$uties'(X0,X2),'external$uties'(X0,X1)))) => smaller('hazard$uof$umortality'(X0,X2),'hazard$uof$umortality'(X0,X1))) & (('greater$uor$uequal'('stock$uof$uknowledge'(X0,X2),'stock$uof$uknowledge'(X0,X1)) & ('smaller$uor$uequal'('internal$ufriction'(X0,X2),'internal$ufriction'(X0,X1)) & greater('external$uties'(X0,X2),'external$uties'(X0,X1)))) => smaller('hazard$uof$umortality'(X0,X2),'hazard$uof$umortality'(X0,X1))))))).
% 27.38/4.08 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : (((organization(X0) & (~'has$uimmunity'(X0,X1) & ~'has$uimmunity'(X0,X2))) => (((greater('stock$uof$uknowledge'(X0,X2),'stock$uof$uknowledge'(X0,X1)) & ('smaller$uor$uequal'('internal$ufriction'(X0,X2),'internal$ufriction'(X0,X1)) & 'greater$uor$uequal'('external$uties'(X0,X2),'external$uties'(X0,X1)))) => smaller('hazard$uof$umortality'(X0,X2),'hazard$uof$umortality'(X0,X1))) & (('greater$uor$uequal'('stock$uof$uknowledge'(X0,X2),'stock$uof$uknowledge'(X0,X1)) & ('smaller$uor$uequal'('internal$ufriction'(X0,X2),'internal$ufriction'(X0,X1)) & greater('external$uties'(X0,X2),'external$uties'(X0,X1)))) => smaller('hazard$uof$umortality'(X0,X2),'hazard$uof$umortality'(X0,X1)))))), inference(negate_conjecture, [status(cth)], [lemma_1])).
% 27.38/4.08 cnf(c0, plain, ~greater(capability(X0,X1),capability(X0,X2)) | 'has$uimmunity'(X0,X2) | ~organization(X0) | smaller('hazard$uof$umortality'(X0,X1),'hazard$uof$umortality'(X0,X2)) | 'has$uimmunity'(X0,X1) | ~'greater$uor$uequal'(position(X0,X1),position(X0,X2)), inference(clausification, [status(esa)], [assumption_4])).
% 27.38/4.08 cnf(c2, plain, 'has$uimmunity'(X0,X1) | ~'greater$uor$uequal'(capability(X0,X2),capability(X0,X1)) | ~organization(X0) | smaller('hazard$uof$umortality'(X0,X2),'hazard$uof$umortality'(X0,X1)) | ~greater(position(X0,X2),position(X0,X1)) | 'has$uimmunity'(X0,X2), inference(clausification, [status(esa)], [assumption_4])).
% 27.38/4.08 cnf(c3, plain, ~organization(X0) | ~'smaller$uor$uequal'('internal$ufriction'(X0,X1),'internal$ufriction'(X0,X2)) | ~greater('stock$uof$uknowledge'(X0,X1),'stock$uof$uknowledge'(X0,X2)) | greater(capability(X0,X1),capability(X0,X2)), inference(clausification, [status(esa)], [assumption_5])).
% 27.38/4.08 cnf(c4, plain, ~organization(X0) | 'internal$ufriction'(X0,X1) != 'internal$ufriction'(X0,X2) | 'stock$uof$uknowledge'(X0,X1) != 'stock$uof$uknowledge'(X0,X2) | capability(X0,X1) = capability(X0,X2), inference(clausification, [status(esa)], [assumption_5])).
% 27.38/4.08 cnf(c5, plain, ~organization(X0) | ~greater('internal$ufriction'(X0,X1),'internal$ufriction'(X0,X2)) | ~'smaller$uor$uequal'('stock$uof$uknowledge'(X0,X1),'stock$uof$uknowledge'(X0,X2)) | smaller(capability(X0,X1),capability(X0,X2)), inference(clausification, [status(esa)], [assumption_5])).
% 27.38/4.08 cnf(c6, plain, ~organization(X0) | ~greater('external$uties'(X0,X1),'external$uties'(X0,X2)) | greater(position(X0,X1),position(X0,X2)), inference(clausification, [status(esa)], [assumption_6])).
% 27.38/4.08 cnf(c7, plain, ~organization(X0) | 'external$uties'(X0,X1) != 'external$uties'(X0,X2) | position(X0,X1) = position(X0,X2), inference(clausification, [status(esa)], [assumption_6])).
% 27.38/4.08 cnf(c8, plain, ~'smaller$uor$uequal'(X0,X1) | X1 = X0 | smaller(X0,X1), inference(clausification, [status(esa)], [definition_smaller_or_equal])).
% 27.38/4.08 cnf(c9, plain, 'smaller$uor$uequal'(X0,X1) | ~smaller(X0,X1), inference(clausification, [status(esa)], [definition_smaller_or_equal])).
% 27.38/4.08 cnf(c10, plain, 'smaller$uor$uequal'(X0,X1) | X1 != X0, inference(clausification, [status(esa)], [definition_smaller_or_equal])).
% 27.38/4.08 cnf(c11, plain, ~'greater$uor$uequal'(X0,X1) | X1 = X0 | greater(X0,X1), inference(clausification, [status(esa)], [definition_greater_or_equal])).
% 27.38/4.08 cnf(c12, plain, 'greater$uor$uequal'(X0,X1) | ~greater(X0,X1), inference(clausification, [status(esa)], [definition_greater_or_equal])).
% 27.38/4.08 cnf(c13, plain, 'greater$uor$uequal'(X0,X1) | X1 != X0, inference(clausification, [status(esa)], [definition_greater_or_equal])).
% 27.38/4.08 cnf(c14, plain, ~smaller(X0,X1) | greater(X1,X0), inference(clausification, [status(esa)], [definition_smaller])).
% 27.38/4.08 cnf(c15, plain, smaller(X0,X1) | ~greater(X1,X0), inference(clausification, [status(esa)], [definition_smaller])).
% 27.38/4.08 cnf(c19, plain, ~'has$uimmunity'(sK23,sK24), inference(clausification, [status(esa)], [negated_conjecture])).
% 27.38/4.08 cnf(c20, plain, ~'has$uimmunity'(sK23,sK25), inference(clausification, [status(esa)], [negated_conjecture])).
% 27.38/4.08 cnf(c21, plain, organization(sK23), inference(clausification, [status(esa)], [negated_conjecture])).
% 27.38/4.08 cnf(c22, plain, X0(sK25,sK24,sK23) | 'smaller$uor$uequal'('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)), inference(clausification, [status(esa)], [negated_conjecture])).
% 27.38/4.08 cnf(c23, plain, X0(sK25,sK24,sK23) | greater('external$uties'(sK23,sK25),'external$uties'(sK23,sK24)), inference(clausification, [status(esa)], [negated_conjecture])).
% 27.38/4.08 cnf(c24, plain, X0(sK25,sK24,sK23) | 'greater$uor$uequal'('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)), inference(clausification, [status(esa)], [negated_conjecture])).
% 27.38/4.08 cnf(c25, plain, X0(sK25,sK24,sK23) | ~smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)), inference(clausification, [status(esa)], [negated_conjecture])).
% 27.38/4.08 cnf(c26, plain, ~X0(X1,X2,X3) | 'smaller$uor$uequal'('internal$ufriction'(X3,X1),'internal$ufriction'(X3,X2)), inference(clausification, [status(esa)], [negated_conjecture])).
% 27.38/4.08 cnf(c27, plain, ~X0(X1,X2,X3) | 'greater$uor$uequal'('external$uties'(X3,X1),'external$uties'(X3,X2)), inference(clausification, [status(esa)], [negated_conjecture])).
% 27.38/4.08 cnf(c28, plain, ~X0(X1,X2,X3) | greater('stock$uof$uknowledge'(X3,X1),'stock$uof$uknowledge'(X3,X2)), inference(clausification, [status(esa)], [negated_conjecture])).
% 27.38/4.08 cnf(c29, plain, ~X0(X1,X2,X3) | ~smaller('hazard$uof$umortality'(X3,X1),'hazard$uof$umortality'(X3,X2)), inference(clausification, [status(esa)], [negated_conjecture])).
% 27.38/4.08 cnf(d0, plain, ~'greater$uor$uequal'(capability(sK23,X0),capability(sK23,X1)) | ~greater(position(sK23,X0),position(sK23,X1)) | 'has$uimmunity'(sK23,X1) | 'has$uimmunity'(sK23,X0) | smaller('hazard$uof$umortality'(sK23,X0),'hazard$uof$umortality'(sK23,X1)), inference(resolution, [status(thm)], [c2,c21])).
% 27.38/4.08 cnf(d1, plain, greater(capability(sK23,X0),capability(sK23,X1)) | ~greater('stock$uof$uknowledge'(sK23,X0),'stock$uof$uknowledge'(sK23,X1)) | ~'smaller$uor$uequal'('internal$ufriction'(sK23,X0),'internal$ufriction'(sK23,X1)), inference(resolution, [status(thm)], [c3,c21])).
% 27.38/4.08 cnf(d2, plain, greater(position(sK23,X0),position(sK23,X1)) | ~greater('external$uties'(sK23,X0),'external$uties'(sK23,X1)), inference(resolution, [status(thm)], [c6,c21])).
% 27.38/4.08 cnf(d3, plain, greater(position(sK23,sK25),position(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d2,c23])).
% 27.38/4.08 cnf(d4, plain, 'greater$uor$uequal'(position(sK23,sK25),position(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [c12,d3])).
% 27.38/4.08 cnf(d5, plain, ~'greater$uor$uequal'(position(sK23,X0),position(sK23,X1)) | ~greater(capability(sK23,X0),capability(sK23,X1)) | 'has$uimmunity'(sK23,X1) | 'has$uimmunity'(sK23,X0) | smaller('hazard$uof$umortality'(sK23,X0),'hazard$uof$umortality'(sK23,X1)), inference(resolution, [status(thm)], [c0,c21])).
% 27.38/4.08 cnf(d6, plain, ~greater(capability(sK23,sK25),capability(sK23,sK24)) | 'has$uimmunity'(sK23,sK24) | 'has$uimmunity'(sK23,sK25) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d5,d4])).
% 27.38/4.08 cnf(d7, plain, ~greater(capability(sK23,sK25),capability(sK23,sK24)) | 'has$uimmunity'(sK23,sK25) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [c19,d6])).
% 27.38/4.08 cnf(d8, plain, ~greater(capability(sK23,sK25),capability(sK23,sK24)) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [c20,d7])).
% 27.38/4.08 cnf(d9, plain, ~greater('internal$ufriction'(sK23,X0),'internal$ufriction'(sK23,X1)) | smaller(capability(sK23,X0),capability(sK23,X1)) | ~'smaller$uor$uequal'('stock$uof$uknowledge'(sK23,X0),'stock$uof$uknowledge'(sK23,X1)), inference(resolution, [status(thm)], [c5,c21])).
% 27.38/4.08 cnf(d10, plain, 'greater$uor$uequal'(X0,X0), inference(equality_resolution, [status(thm)], [c13])).
% 27.38/4.08 cnf(d11, plain, 'internal$ufriction'(sK23,sK24) = 'internal$ufriction'(sK23,sK25) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [c8,c22])).
% 27.38/4.08 cnf(d12, plain, 'internal$ufriction'(sK23,X0) != 'internal$ufriction'(sK23,sK24) | capability(sK23,X0) = capability(sK23,sK25) | 'stock$uof$uknowledge'(sK23,X0) != 'stock$uof$uknowledge'(sK23,sK25) | ~organization(sK23) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(superposition, [status(thm)], [d11,c4])).
% 27.38/4.08 cnf(d13, plain, capability(sK23,X0) = capability(sK23,sK25) | 'internal$ufriction'(sK23,X0) != 'internal$ufriction'(sK23,sK24) | 'stock$uof$uknowledge'(sK23,X0) != 'stock$uof$uknowledge'(sK23,sK25) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [c21,d12])).
% 27.38/4.08 cnf(d14, plain, capability(sK23,sK24) = capability(sK23,sK25) | 'stock$uof$uknowledge'(sK23,sK24) != 'stock$uof$uknowledge'(sK23,sK25) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(equality_resolution, [status(thm)], [d13])).
% 27.38/4.08 cnf(d15, plain, 'stock$uof$uknowledge'(sK23,sK24) = 'stock$uof$uknowledge'(sK23,sK25) | greater('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [c11,c24])).
% 27.38/4.08 cnf(d16, plain, 'stock$uof$uknowledge'(sK23,sK24) != 'stock$uof$uknowledge'(sK23,sK24) | capability(sK23,sK24) = capability(sK23,sK25) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23) | greater('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(superposition, [status(thm)], [d15,d14])).
% 27.38/4.08 cnf(d17, plain, capability(sK23,sK24) = capability(sK23,sK25) | greater('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(equality_resolution, [status(thm)], [d16])).
% 27.38/4.08 cnf(d18, plain, ~'greater$uor$uequal'(capability(sK23,sK24),capability(sK23,X0)) | ~greater(position(sK23,sK25),position(sK23,X0)) | 'has$uimmunity'(sK23,X0) | 'has$uimmunity'(sK23,sK25) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,X0)) | greater('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(superposition, [status(thm)], [d17,d0])).
% 27.38/4.08 cnf(d19, plain, ~'greater$uor$uequal'(capability(sK23,sK24),capability(sK23,X0)) | ~greater(position(sK23,sK25),position(sK23,X0)) | greater('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)) | 'has$uimmunity'(sK23,X0) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,X0)) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [c20,d18])).
% 27.38/4.08 cnf(d20, plain, ~greater(position(sK23,sK25),position(sK23,sK24)) | greater('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)) | 'has$uimmunity'(sK23,sK24) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d19,d10])).
% 27.38/4.08 cnf(d21, plain, ~greater(position(sK23,sK25),position(sK23,sK24)) | greater('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [c19,d20])).
% 27.38/4.08 cnf(d22, plain, greater('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d21,d3])).
% 27.38/4.08 cnf(d23, plain, smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23) | greater(capability(sK23,sK25),capability(sK23,sK24)) | ~'smaller$uor$uequal'('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)), inference(resolution, [status(thm)], [d22,d1])).
% 27.38/4.08 cnf(d24, plain, greater(capability(sK23,sK25),capability(sK23,sK24)) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d23,c22])).
% 27.38/4.08 cnf(d25, plain, smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d24,d8])).
% 27.38/4.08 cnf(d26, plain, smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d25,c25])).
% 27.38/4.08 cnf(d27, plain, 'Ts22'(sK25,sK24,sK23) | greater('internal$ufriction'(sK23,sK24),'internal$ufriction'(sK23,sK25)), inference(resolution, [status(thm)], [d26,c14])).
% 27.38/4.08 cnf(d28, plain, 'Ts22'(sK25,sK24,sK23) | smaller(capability(sK23,sK24),capability(sK23,sK25)) | ~'smaller$uor$uequal'('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)), inference(resolution, [status(thm)], [d27,d9])).
% 27.38/4.08 cnf(d29, plain, smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23) | smaller('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)), inference(resolution, [status(thm)], [d22,c15])).
% 27.38/4.08 cnf(d30, plain, smaller('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)) | smaller('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)) | 'Ts22'(sK25,sK24,sK23) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d29,c25])).
% 27.38/4.08 cnf(d31, plain, smaller('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)) | 'Ts22'(sK25,sK24,sK23) | greater('internal$ufriction'(sK23,sK24),'internal$ufriction'(sK23,sK25)), inference(resolution, [status(thm)], [d30,c14])).
% 27.38/4.08 cnf(d32, plain, smaller('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)) | 'Ts22'(sK25,sK24,sK23) | smaller(capability(sK23,sK24),capability(sK23,sK25)) | ~'smaller$uor$uequal'('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)), inference(resolution, [status(thm)], [d31,d9])).
% 27.38/4.08 cnf(d33, plain, ~'smaller$uor$uequal'('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK24)) | smaller(capability(sK23,sK24),capability(sK23,sK25)) | smaller('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)) | 'Ts22'(sK25,sK24,sK23) | greater('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(superposition, [status(thm)], [d15,d32])).
% 27.38/4.08 cnf(d34, plain, 'smaller$uor$uequal'(X0,X0), inference(equality_resolution, [status(thm)], [c10])).
% 27.38/4.08 cnf(d35, plain, greater('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)) | smaller(capability(sK23,sK24),capability(sK23,sK25)) | smaller('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d34,d33])).
% 27.38/4.08 cnf(d36, plain, smaller(capability(sK23,sK24),capability(sK23,sK25)) | smaller('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)) | 'Ts22'(sK25,sK24,sK23) | smaller('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)), inference(resolution, [status(thm)], [d35,c15])).
% 27.38/4.08 cnf(d37, plain, smaller('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)) | 'Ts22'(sK25,sK24,sK23) | greater(capability(sK23,sK25),capability(sK23,sK24)), inference(resolution, [status(thm)], [d36,c14])).
% 27.38/4.08 cnf(d38, plain, smaller('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)) | 'Ts22'(sK25,sK24,sK23) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d37,d8])).
% 27.38/4.08 cnf(d39, plain, smaller('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)) | 'Ts22'(sK25,sK24,sK23) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d38,c25])).
% 27.38/4.08 cnf(d40, plain, 'Ts22'(sK25,sK24,sK23) | 'smaller$uor$uequal'('stock$uof$uknowledge'(sK23,sK24),'stock$uof$uknowledge'(sK23,sK25)), inference(resolution, [status(thm)], [d39,c9])).
% 27.38/4.08 cnf(d41, plain, 'Ts22'(sK25,sK24,sK23) | smaller(capability(sK23,sK24),capability(sK23,sK25)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d40,d28])).
% 27.38/4.08 cnf(d42, plain, 'Ts22'(sK25,sK24,sK23) | greater(capability(sK23,sK25),capability(sK23,sK24)), inference(resolution, [status(thm)], [d41,c14])).
% 27.38/4.08 cnf(d43, plain, 'Ts22'(sK25,sK24,sK23) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d42,d8])).
% 27.38/4.08 cnf(d44, plain, 'Ts22'(sK25,sK24,sK23) | 'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d43,c25])).
% 27.38/4.08 cnf(d45, plain, greater('stock$uof$uknowledge'(sK23,sK25),'stock$uof$uknowledge'(sK23,sK24)), inference(resolution, [status(thm)], [d44,c28])).
% 27.38/4.08 cnf(d46, plain, greater(capability(sK23,sK25),capability(sK23,sK24)) | ~'smaller$uor$uequal'('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)), inference(resolution, [status(thm)], [d45,d1])).
% 27.38/4.08 cnf(d47, plain, 'smaller$uor$uequal'('internal$ufriction'(sK23,sK25),'internal$ufriction'(sK23,sK24)), inference(resolution, [status(thm)], [d44,c26])).
% 27.38/4.08 cnf(d48, plain, greater(capability(sK23,sK25),capability(sK23,sK24)), inference(resolution, [status(thm)], [d47,d46])).
% 27.38/4.08 cnf(d49, plain, 'greater$uor$uequal'(capability(sK23,sK25),capability(sK23,sK24)), inference(resolution, [status(thm)], [d48,c12])).
% 27.38/4.08 cnf(d50, plain, ~greater(position(sK23,sK25),position(sK23,sK24)) | 'has$uimmunity'(sK23,sK24) | 'has$uimmunity'(sK23,sK25) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)), inference(resolution, [status(thm)], [d49,d0])).
% 27.38/4.08 cnf(d51, plain, ~greater(position(sK23,sK25),position(sK23,sK24)) | 'has$uimmunity'(sK23,sK25) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)), inference(resolution, [status(thm)], [c19,d50])).
% 27.38/4.08 cnf(d52, plain, ~greater(position(sK23,sK25),position(sK23,sK24)) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)), inference(resolution, [status(thm)], [c20,d51])).
% 27.38/4.08 cnf(d53, plain, 'greater$uor$uequal'('external$uties'(sK23,sK25),'external$uties'(sK23,sK24)), inference(resolution, [status(thm)], [d44,c27])).
% 27.38/4.08 cnf(d54, plain, 'external$uties'(sK23,sK24) = 'external$uties'(sK23,sK25) | greater('external$uties'(sK23,sK25),'external$uties'(sK23,sK24)), inference(resolution, [status(thm)], [d53,c11])).
% 27.38/4.08 cnf(d55, plain, 'external$uties'(sK23,sK24) != 'external$uties'(sK23,X0) | position(sK23,sK25) = position(sK23,X0) | ~organization(sK23) | greater('external$uties'(sK23,sK25),'external$uties'(sK23,sK24)), inference(superposition, [status(thm)], [d54,c7])).
% 27.38/4.08 cnf(d56, plain, position(sK23,sK25) = position(sK23,X0) | 'external$uties'(sK23,sK24) != 'external$uties'(sK23,X0) | greater('external$uties'(sK23,sK25),'external$uties'(sK23,sK24)), inference(resolution, [status(thm)], [c21,d55])).
% 27.38/4.08 cnf(d57, plain, position(sK23,sK25) = position(sK23,sK24) | greater('external$uties'(sK23,sK25),'external$uties'(sK23,sK24)), inference(equality_resolution, [status(thm)], [d56])).
% 27.38/4.08 cnf(d58, plain, ~'greater$uor$uequal'(position(sK23,sK24),position(sK23,X0)) | ~greater(capability(sK23,sK25),capability(sK23,X0)) | 'has$uimmunity'(sK23,X0) | 'has$uimmunity'(sK23,sK25) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,X0)) | greater('external$uties'(sK23,sK25),'external$uties'(sK23,sK24)), inference(superposition, [status(thm)], [d57,d5])).
% 27.38/4.08 cnf(d59, plain, ~'greater$uor$uequal'(position(sK23,sK24),position(sK23,X0)) | ~greater(capability(sK23,sK25),capability(sK23,X0)) | greater('external$uties'(sK23,sK25),'external$uties'(sK23,sK24)) | 'has$uimmunity'(sK23,X0) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,X0)), inference(resolution, [status(thm)], [c20,d58])).
% 27.38/4.08 cnf(d60, plain, ~greater(capability(sK23,sK25),capability(sK23,sK24)) | greater('external$uties'(sK23,sK25),'external$uties'(sK23,sK24)) | 'has$uimmunity'(sK23,sK24) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)), inference(resolution, [status(thm)], [d59,d10])).
% 27.38/4.08 cnf(d61, plain, ~greater(capability(sK23,sK25),capability(sK23,sK24)) | greater('external$uties'(sK23,sK25),'external$uties'(sK23,sK24)) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)), inference(resolution, [status(thm)], [c19,d60])).
% 27.38/4.08 cnf(d62, plain, greater('external$uties'(sK23,sK25),'external$uties'(sK23,sK24)) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)), inference(resolution, [status(thm)], [d48,d61])).
% 27.38/4.08 cnf(d63, plain, smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | greater(position(sK23,sK25),position(sK23,sK24)), inference(resolution, [status(thm)], [d62,d2])).
% 27.38/4.08 cnf(d64, plain, smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)) | smaller('hazard$uof$umortality'(sK23,sK25),'hazard$uof$umortality'(sK23,sK24)), inference(resolution, [status(thm)], [d63,d52])).
% 27.38/4.08 cnf(d65, plain, ~'Ts22'(sK25,sK24,sK23), inference(resolution, [status(thm)], [d64,c29])).
% 27.38/4.08 cnf(d66, plain, $false, inference(resolution, [status(thm)], [d44,d65])).
% 27.38/4.08 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------