%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT023+2 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:03 AM UTC 2026
% Result : Theorem 9.45s 3.21s
% Output : CNFRefutation 9.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT023+2 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n015.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sat Sep 26 00:07:58 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.45/3.21 % SZS status Theorem for theBenchmark.p
% 9.45/3.21 % SZS output start CNFRefutation for theBenchmark.p
% 9.45/3.21 fof(mp_earliest_time_growth_rate_exceeds, axiom, ! [X0] : (((environment(X0) & ? [X1] : (('in$uenvironment'(X0,X1) & ! [X2] : (((subpopulations('first$umovers','efficient$uproducers',X0,X2) & 'greater$uor$uequal'(X2,X1)) => greater('growth$urate'('efficient$uproducers',X2),'growth$urate'('first$umovers',X2))))))) => ? [X1] : (('in$uenvironment'(X0,X1) & (~greater('growth$urate'('efficient$uproducers',X1),'growth$urate'('first$umovers',X1)) & ! [X2] : (((subpopulations('first$umovers','efficient$uproducers',X0,X2) & greater(X2,X1)) => greater('growth$urate'('efficient$uproducers',X2),'growth$urate'('first$umovers',X2)))))))))).
% 9.45/3.21 fof(d1, hypothesis, ! [X0] : ! [X1] : (((environment(X0) & (~greater('growth$urate'('efficient$uproducers',X1),'growth$urate'('first$umovers',X1)) & ('in$uenvironment'(X0,X1) & ! [X2] : (((subpopulations('first$umovers','efficient$uproducers',X0,X2) & greater(X2,X1)) => greater('growth$urate'('efficient$uproducers',X2),'growth$urate'('first$umovers',X2))))))) => X1 = 'critical$upoint'(X0)))).
% 9.45/3.21 fof(l1, hypothesis, ! [X0] : (((environment(X0) & stable(X0)) => ? [X1] : (('in$uenvironment'(X0,X1) & ! [X2] : (((subpopulations('first$umovers','efficient$uproducers',X0,X2) & 'greater$uor$uequal'(X2,X1)) => greater('growth$urate'('efficient$uproducers',X2),'growth$urate'('first$umovers',X2))))))))).
% 9.45/3.21 fof(prove_l5, conjecture, ! [X0] : (((environment(X0) & stable(X0)) => 'in$uenvironment'(X0,'critical$upoint'(X0))))).
% 9.45/3.21 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((environment(X0) & stable(X0)) => 'in$uenvironment'(X0,'critical$upoint'(X0)))), inference(negate_conjecture, [status(cth)], [prove_l5])).
% 9.45/3.21 cnf(c0, plain, X0(X1) | 'in$uenvironment'(X1,sK2(X1)), inference(clausification, [status(esa)], [mp_earliest_time_growth_rate_exceeds])).
% 9.45/3.21 cnf(c1, plain, X0(X1) | ~greater('growth$urate'('efficient$uproducers',sK2(X1)),'growth$urate'('first$umovers',sK2(X1))), inference(clausification, [status(esa)], [mp_earliest_time_growth_rate_exceeds])).
% 9.45/3.21 cnf(c2, plain, X0(X1) | ~subpopulations('first$umovers','efficient$uproducers',X1,X2) | ~greater(X2,sK2(X1)) | greater('growth$urate'('efficient$uproducers',X2),'growth$urate'('first$umovers',X2)), inference(clausification, [status(esa)], [mp_earliest_time_growth_rate_exceeds])).
% 9.45/3.21 cnf(c3, plain, ~X0(X1) | ~environment(X1) | ~'in$uenvironment'(X1,X2) | subpopulations('first$umovers','efficient$uproducers',X1,sK5(X1,X2)), inference(clausification, [status(esa)], [mp_earliest_time_growth_rate_exceeds])).
% 9.45/3.21 cnf(c4, plain, ~X0(X1) | ~environment(X1) | ~'in$uenvironment'(X1,X2) | 'greater$uor$uequal'(sK5(X1,X2),X2), inference(clausification, [status(esa)], [mp_earliest_time_growth_rate_exceeds])).
% 9.45/3.21 cnf(c5, plain, ~X0(X1) | ~environment(X1) | ~'in$uenvironment'(X1,X2) | ~greater('growth$urate'('efficient$uproducers',sK5(X1,X2)),'growth$urate'('first$umovers',sK5(X1,X2))), inference(clausification, [status(esa)], [mp_earliest_time_growth_rate_exceeds])).
% 9.45/3.21 cnf(c6, plain, X0 = 'critical$upoint'(X1) | ~'in$uenvironment'(X1,X0) | subpopulations('first$umovers','efficient$uproducers',X1,sK8(X1,X0)) | ~environment(X1) | greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)), inference(clausification, [status(esa)], [d1])).
% 9.45/3.21 cnf(c7, plain, X0 = 'critical$upoint'(X1) | ~'in$uenvironment'(X1,X0) | greater(sK8(X1,X0),X0) | ~environment(X1) | greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)), inference(clausification, [status(esa)], [d1])).
% 9.45/3.21 cnf(c8, plain, ~greater('growth$urate'('efficient$uproducers',sK8(X0,X1)),'growth$urate'('first$umovers',sK8(X0,X1))) | X1 = 'critical$upoint'(X0) | ~'in$uenvironment'(X0,X1) | ~environment(X0) | greater('growth$urate'('efficient$uproducers',X1),'growth$urate'('first$umovers',X1)), inference(clausification, [status(esa)], [d1])).
% 9.45/3.21 cnf(c9, plain, ~environment(X0) | ~stable(X0) | 'in$uenvironment'(X0,sK10(X0)), inference(clausification, [status(esa)], [l1])).
% 9.45/3.21 cnf(c10, plain, ~environment(X0) | ~subpopulations('first$umovers','efficient$uproducers',X0,X1) | ~'greater$uor$uequal'(X1,sK10(X0)) | greater('growth$urate'('efficient$uproducers',X1),'growth$urate'('first$umovers',X1)) | ~stable(X0), inference(clausification, [status(esa)], [l1])).
% 9.45/3.21 cnf(c11, plain, environment(sK12), inference(clausification, [status(esa)], [negated_conjecture])).
% 9.45/3.21 cnf(c12, plain, stable(sK12), inference(clausification, [status(esa)], [negated_conjecture])).
% 9.45/3.21 cnf(c13, plain, ~'in$uenvironment'(sK12,'critical$upoint'(sK12)), inference(clausification, [status(esa)], [negated_conjecture])).
% 9.45/3.21 cnf(d_0, plain, sK2(X0) = 'critical$upoint'(X1) | ~'in$uenvironment'(X1,sK2(X0)) | greater(sK8(X1,sK2(X0)),sK2(X0)) | ~environment(X1) | 'Ts0'(X0), inference(resolution, [status(thm)], [c7,c1])).
% 9.45/3.21 cnf(d_1, plain, X0 = 'critical$upoint'(X1) | ~'in$uenvironment'(X1,X0) | greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)) | ~environment(X1) | 'Ts0'(X1) | ~greater(sK8(X1,X0),sK2(X1)) | greater('growth$urate'('efficient$uproducers',sK8(X1,X0)),'growth$urate'('first$umovers',sK8(X1,X0))), inference(resolution, [status(thm)], [c6,c2])).
% 9.45/3.21 cnf(d_2, plain, X0 = 'critical$upoint'(X1) | ~'in$uenvironment'(X1,X0) | 'Ts0'(X1) | greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)) | ~greater(sK8(X1,X0),sK2(X1)) | ~environment(X1) | X0 = 'critical$upoint'(X1) | ~'in$uenvironment'(X1,X0) | greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)) | ~environment(X1), inference(resolution, [status(thm)], [d_1,c8])).
% 9.45/3.21 cnf(d_3, plain, sK2(X0) = 'critical$upoint'(X0) | ~'in$uenvironment'(X0,sK2(X0)) | 'Ts0'(X0) | greater('growth$urate'('efficient$uproducers',sK2(X0)),'growth$urate'('first$umovers',sK2(X0))) | ~environment(X0) | sK2(X0) = 'critical$upoint'(X0) | ~'in$uenvironment'(X0,sK2(X0)) | 'Ts0'(X0) | ~environment(X0), inference(resolution, [status(thm)], [d_2,d_0])).
% 9.45/3.21 cnf(d_4, plain, sK2(X0) = 'critical$upoint'(X0) | ~'in$uenvironment'(X0,sK2(X0)) | 'Ts0'(X0) | ~environment(X0) | 'Ts0'(X0), inference(resolution, [status(thm)], [d_3,c1])).
% 9.45/3.21 cnf(d_5, plain, sK2(X0) = 'critical$upoint'(X0) | 'Ts0'(X0) | ~environment(X0) | 'Ts0'(X0), inference(resolution, [status(thm)], [d_4,c0])).
% 9.45/3.21 cnf(d_6, plain, sK2(sK12) = 'critical$upoint'(sK12) | 'Ts0'(sK12), inference(resolution, [status(thm)], [d_5,c11])).
% 9.45/3.21 cnf(d_7, plain, greater('growth$urate'('efficient$uproducers',sK5(X0,X1)),'growth$urate'('first$umovers',sK5(X0,X1))) | ~environment(X0) | ~'greater$uor$uequal'(sK5(X0,X1),sK10(X0)) | ~stable(X0) | ~'in$uenvironment'(X0,X1) | ~'Ts0'(X0) | ~environment(X0), inference(resolution, [status(thm)], [c10,c3])).
% 9.45/3.21 cnf(d_8, plain, ~'in$uenvironment'(X0,X1) | ~'Ts0'(X0) | ~environment(X0) | ~'greater$uor$uequal'(sK5(X0,X1),sK10(X0)) | ~stable(X0) | ~'in$uenvironment'(X0,X1) | ~'Ts0'(X0) | ~environment(X0), inference(resolution, [status(thm)], [d_7,c5])).
% 9.45/3.21 cnf(d_9, plain, ~'in$uenvironment'(X0,sK10(X0)) | ~'Ts0'(X0) | ~environment(X0) | ~stable(X0) | ~'in$uenvironment'(X0,sK10(X0)) | ~'Ts0'(X0) | ~environment(X0), inference(resolution, [status(thm)], [d_8,c4])).
% 9.45/3.21 cnf(d_10, plain, ~'Ts0'(X0) | ~environment(X0) | ~stable(X0) | ~environment(X0) | ~stable(X0), inference(resolution, [status(thm)], [d_9,c9])).
% 9.45/3.21 cnf(d_11, plain, ~'Ts0'(sK12) | ~environment(sK12), inference(resolution, [status(thm)], [d_10,c12])).
% 9.45/3.21 cnf(d_12, plain, ~'Ts0'(sK12), inference(resolution, [status(thm)], [c11,d_11])).
% 9.45/3.21 cnf(d_13, plain, sK2(sK12) = 'critical$upoint'(sK12), inference(resolution, [status(thm)], [d_12,d_6])).
% 9.45/3.21 cnf(d_14, plain, ~'in$uenvironment'(sK12,sK2(sK12)), inference(demodulation, [status(thm)], [c13,d_13])).
% 9.45/3.21 cnf(d_15, plain, 'Ts0'(sK12), inference(resolution, [status(thm)], [d_14,c0])).
% 9.45/3.21 cnf(d_16, plain, $false, inference(resolution, [status(thm)], [d_12,d_15])).
% 9.45/3.21 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------