%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT030+1 : 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 : n007.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:15 AM UTC 2026
% Result : Theorem 8.32s 2.83s
% Output : CNFRefutation 8.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT030+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n007.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Sat Sep 26 00:03:09 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.32/2.83 % SZS status Theorem for theBenchmark.p
% 8.32/2.83 % SZS output start CNFRefutation for theBenchmark.p
% 8.32/2.83 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)))))))))).
% 8.32/2.83 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))))))))).
% 8.32/2.83 fof(prove_l12, conjecture, ! [X0] : (((environment(X0) & stable(X0)) => ? [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)))))))))).
% 8.32/2.83 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((environment(X0) & stable(X0)) => ? [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))))))))), inference(negate_conjecture, [status(cth)], [prove_l12])).
% 8.32/2.83 cnf(c0, plain, X0(X1) | 'in$uenvironment'(X1,sK2(X1)), inference(clausification, [status(esa)], [mp_earliest_time_growth_rate_exceeds])).
% 8.32/2.83 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])).
% 8.32/2.83 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])).
% 8.32/2.83 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])).
% 8.32/2.83 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])).
% 8.32/2.83 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])).
% 8.32/2.83 cnf(c6, plain, ~environment(X0) | ~stable(X0) | 'in$uenvironment'(X0,sK7(X0)), inference(clausification, [status(esa)], [l1])).
% 8.32/2.83 cnf(c7, plain, greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)) | ~'greater$uor$uequal'(X0,sK7(X1)) | ~subpopulations('first$umovers','efficient$uproducers',X1,X0) | ~environment(X1) | ~stable(X1), inference(clausification, [status(esa)], [l1])).
% 8.32/2.83 cnf(c8, plain, environment(sK9), inference(clausification, [status(esa)], [negated_conjecture])).
% 8.32/2.83 cnf(c9, plain, stable(sK9), inference(clausification, [status(esa)], [negated_conjecture])).
% 8.32/2.83 cnf(c10, plain, ~'in$uenvironment'(sK9,X0) | greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)) | subpopulations('first$umovers','efficient$uproducers',sK9,sK11(X0)), inference(clausification, [status(esa)], [negated_conjecture])).
% 8.32/2.83 cnf(c11, plain, ~'in$uenvironment'(sK9,X0) | greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)) | greater(sK11(X0),X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 8.32/2.83 cnf(c12, plain, ~'in$uenvironment'(sK9,X0) | greater('growth$urate'('efficient$uproducers',X0),'growth$urate'('first$umovers',X0)) | ~greater('growth$urate'('efficient$uproducers',sK11(X0)),'growth$urate'('first$umovers',sK11(X0))), inference(clausification, [status(esa)], [negated_conjecture])).
% 8.32/2.83 cnf(d0, plain, greater('growth$urate'('efficient$uproducers',sK5(X0,X1)),'growth$urate'('first$umovers',sK5(X0,X1))) | ~environment(X0) | ~'greater$uor$uequal'(sK5(X0,X1),sK7(X0)) | ~stable(X0) | ~'in$uenvironment'(X0,X1) | ~'Ts0'(X0) | ~environment(X0), inference(resolution, [status(thm)], [c7,c3])).
% 8.32/2.83 cnf(d1, plain, ~'in$uenvironment'(X0,X1) | ~'Ts0'(X0) | ~environment(X0) | ~'greater$uor$uequal'(sK5(X0,X1),sK7(X0)) | ~stable(X0) | ~'in$uenvironment'(X0,X1) | ~'Ts0'(X0) | ~environment(X0), inference(resolution, [status(thm)], [d0,c5])).
% 8.32/2.83 cnf(d2, plain, ~'in$uenvironment'(X0,sK7(X0)) | ~'Ts0'(X0) | ~environment(X0) | ~stable(X0) | ~'in$uenvironment'(X0,sK7(X0)) | ~'Ts0'(X0) | ~environment(X0), inference(resolution, [status(thm)], [d1,c4])).
% 8.32/2.83 cnf(d3, plain, ~'Ts0'(X0) | ~environment(X0) | ~stable(X0) | ~environment(X0) | ~stable(X0), inference(resolution, [status(thm)], [d2,c6])).
% 8.32/2.83 cnf(d4, plain, ~'Ts0'(sK9) | ~environment(sK9), inference(resolution, [status(thm)], [d3,c9])).
% 8.32/2.83 cnf(d5, plain, ~'Ts0'(sK9), inference(resolution, [status(thm)], [c8,d4])).
% 8.32/2.83 cnf(d6, plain, ~'in$uenvironment'(sK9,sK2(X0)) | greater(sK11(sK2(X0)),sK2(X0)) | 'Ts0'(X0), inference(resolution, [status(thm)], [c11,c1])).
% 8.32/2.83 cnf(d7, plain, ~'in$uenvironment'(sK9,sK2(X0)) | subpopulations('first$umovers','efficient$uproducers',sK9,sK11(sK2(X0))) | 'Ts0'(X0), inference(resolution, [status(thm)], [c10,c1])).
% 8.32/2.83 cnf(d8, plain, ~'in$uenvironment'(sK9,sK2(X0)) | 'Ts0'(X0) | 'Ts0'(sK9) | ~greater(sK11(sK2(X0)),sK2(sK9)) | greater('growth$urate'('efficient$uproducers',sK11(sK2(X0))),'growth$urate'('first$umovers',sK11(sK2(X0)))), inference(resolution, [status(thm)], [d7,c2])).
% 8.32/2.83 cnf(d9, plain, ~'in$uenvironment'(sK9,sK2(X0)) | 'Ts0'(X0) | 'Ts0'(sK9) | ~greater(sK11(sK2(X0)),sK2(sK9)) | ~'in$uenvironment'(sK9,sK2(X0)) | greater('growth$urate'('efficient$uproducers',sK2(X0)),'growth$urate'('first$umovers',sK2(X0))), inference(resolution, [status(thm)], [d8,c12])).
% 8.32/2.83 cnf(d10, plain, ~'in$uenvironment'(sK9,sK2(X0)) | 'Ts0'(X0) | 'Ts0'(sK9) | ~greater(sK11(sK2(X0)),sK2(sK9)) | 'Ts0'(X0), inference(resolution, [status(thm)], [d9,c1])).
% 8.32/2.83 cnf(d11, plain, ~'in$uenvironment'(sK9,sK2(sK9)) | 'Ts0'(sK9) | 'Ts0'(sK9) | ~'in$uenvironment'(sK9,sK2(sK9)) | 'Ts0'(sK9), inference(resolution, [status(thm)], [d10,d6])).
% 8.32/2.83 cnf(d12, plain, 'Ts0'(sK9) | 'Ts0'(sK9), inference(resolution, [status(thm)], [d11,c0])).
% 8.32/2.83 cnf(d13, plain, $false, inference(resolution, [status(thm)], [d12,d5])).
% 8.32/2.83 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------