%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT028+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:05 AM UTC 2026
% Result : Theorem 9.64s 1.65s
% Output : CNFRefutation 9.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT028+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 00:10:42 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.64/1.65 % SZS status Theorem for theBenchmark.p
% 9.64/1.65 % SZS output start CNFRefutation for theBenchmark.p
% 9.64/1.65 fof(mp_first_movers_negative_growth, axiom, ! [X0] : (((environment(X0) & (stable(X0) & ? [X1] : (('in$uenvironment'(X0,X1) & ! [X2] : (((subpopulations('first$umovers','efficient$uproducers',X0,X2) & 'greater$uor$uequal'(X2,X1)) => greater(zero,'growth$urate'('first$umovers',X2)))))))) => ? [X3] : ((greater(X3,appear('efficient$uproducers',X0)) & ! [X2] : (((subpopulations('first$umovers','efficient$uproducers',X0,X2) & 'greater$uor$uequal'(X2,X3)) => greater(zero,'growth$urate'('first$umovers',X2))))))))).
% 9.64/1.65 fof(l11, 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),zero) & greater(zero,'growth$urate'('first$umovers',X2)))))))))).
% 9.64/1.65 fof(prove_l10, conjecture, ! [X0] : (((environment(X0) & stable(X0)) => ? [X1] : ((greater(X1,appear('efficient$uproducers',X0)) & ! [X2] : (((subpopulations('first$umovers','efficient$uproducers',X0,X2) & 'greater$uor$uequal'(X2,X1)) => greater(zero,'growth$urate'('first$umovers',X2))))))))).
% 9.64/1.65 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((environment(X0) & stable(X0)) => ? [X1] : ((greater(X1,appear('efficient$uproducers',X0)) & ! [X2] : (((subpopulations('first$umovers','efficient$uproducers',X0,X2) & 'greater$uor$uequal'(X2,X1)) => greater(zero,'growth$urate'('first$umovers',X2)))))))), inference(negate_conjecture, [status(cth)], [prove_l10])).
% 9.64/1.65 cnf(c0, plain, X0(X1) | greater(sK2(X1),appear('efficient$uproducers',X1)), inference(clausification, [status(esa)], [mp_first_movers_negative_growth])).
% 9.64/1.65 cnf(c1, plain, X0(X1) | ~subpopulations('first$umovers','efficient$uproducers',X1,X2) | ~'greater$uor$uequal'(X2,sK2(X1)) | greater(zero,'growth$urate'('first$umovers',X2)), inference(clausification, [status(esa)], [mp_first_movers_negative_growth])).
% 9.64/1.65 cnf(c2, plain, ~stable(X0) | subpopulations('first$umovers','efficient$uproducers',X0,sK5(X0,X1)) | ~environment(X0) | ~'in$uenvironment'(X0,X1) | ~X2(X0), inference(clausification, [status(esa)], [mp_first_movers_negative_growth])).
% 9.64/1.65 cnf(c3, plain, ~stable(X0) | ~environment(X0) | ~X1(X0) | ~'in$uenvironment'(X0,X2) | 'greater$uor$uequal'(sK5(X0,X2),X2), inference(clausification, [status(esa)], [mp_first_movers_negative_growth])).
% 9.64/1.65 cnf(c4, plain, ~stable(X0) | ~greater(zero,'growth$urate'('first$umovers',sK5(X0,X1))) | ~environment(X0) | ~'in$uenvironment'(X0,X1) | ~X2(X0), inference(clausification, [status(esa)], [mp_first_movers_negative_growth])).
% 9.64/1.65 cnf(c5, plain, ~environment(X0) | ~stable(X0) | 'in$uenvironment'(X0,sK7(X0)), inference(clausification, [status(esa)], [l11])).
% 9.64/1.65 cnf(c7, plain, ~'greater$uor$uequal'(X0,sK7(X1)) | ~subpopulations('first$umovers','efficient$uproducers',X1,X0) | ~environment(X1) | ~stable(X1) | greater(zero,'growth$urate'('first$umovers',X0)), inference(clausification, [status(esa)], [l11])).
% 9.64/1.65 cnf(c8, plain, environment(sK9), inference(clausification, [status(esa)], [negated_conjecture])).
% 9.64/1.65 cnf(c9, plain, stable(sK9), inference(clausification, [status(esa)], [negated_conjecture])).
% 9.64/1.65 cnf(c10, plain, ~greater(X0,appear('efficient$uproducers',sK9)) | subpopulations('first$umovers','efficient$uproducers',sK9,sK11(X0)), inference(clausification, [status(esa)], [negated_conjecture])).
% 9.64/1.65 cnf(c11, plain, ~greater(X0,appear('efficient$uproducers',sK9)) | 'greater$uor$uequal'(sK11(X0),X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 9.64/1.65 cnf(c12, plain, ~greater(X0,appear('efficient$uproducers',sK9)) | ~greater(zero,'growth$urate'('first$umovers',sK11(X0))), inference(clausification, [status(esa)], [negated_conjecture])).
% 9.64/1.65 cnf(d0, plain, greater(zero,'growth$urate'('first$umovers',sK5(X0,X1))) | ~'greater$uor$uequal'(sK5(X0,X1),sK7(X0)) | ~environment(X0) | ~stable(X0) | ~'Ts0'(X0) | ~environment(X0) | ~'in$uenvironment'(X0,X1) | ~stable(X0), inference(resolution, [status(thm)], [c7,c2])).
% 9.64/1.65 cnf(d1, plain, ~'Ts0'(X0) | greater(zero,'growth$urate'('first$umovers',sK5(X0,sK7(X0)))) | ~environment(X0) | ~'in$uenvironment'(X0,sK7(X0)) | ~stable(X0) | ~'Ts0'(X0) | ~environment(X0) | ~'in$uenvironment'(X0,sK7(X0)) | ~stable(X0), inference(resolution, [status(thm)], [d0,c3])).
% 9.64/1.65 cnf(d2, plain, ~'Ts0'(X0) | ~environment(X0) | ~'in$uenvironment'(X0,sK7(X0)) | ~stable(X0) | ~'Ts0'(X0) | ~environment(X0) | ~'in$uenvironment'(X0,sK7(X0)) | ~stable(X0), inference(resolution, [status(thm)], [d1,c4])).
% 9.64/1.65 cnf(d3, plain, ~'Ts0'(X0) | ~environment(X0) | ~stable(X0) | ~environment(X0) | ~stable(X0), inference(resolution, [status(thm)], [d2,c5])).
% 9.64/1.65 cnf(d4, plain, ~'Ts0'(sK9) | ~environment(sK9), inference(resolution, [status(thm)], [d3,c9])).
% 9.64/1.65 cnf(d5, plain, ~'Ts0'(sK9), inference(resolution, [status(thm)], [c8,d4])).
% 9.64/1.65 cnf(d6, plain, 'greater$uor$uequal'(sK11(sK2(sK9)),sK2(sK9)) | 'Ts0'(sK9), inference(resolution, [status(thm)], [c11,c0])).
% 9.64/1.65 cnf(d7, plain, ~greater(X0,appear('efficient$uproducers',sK9)) | 'Ts0'(sK9) | greater(zero,'growth$urate'('first$umovers',sK11(X0))) | ~'greater$uor$uequal'(sK11(X0),sK2(sK9)), inference(resolution, [status(thm)], [c10,c1])).
% 9.64/1.65 cnf(d8, plain, 'Ts0'(sK9) | ~greater(X0,appear('efficient$uproducers',sK9)) | ~'greater$uor$uequal'(sK11(X0),sK2(sK9)) | ~greater(X0,appear('efficient$uproducers',sK9)), inference(resolution, [status(thm)], [d7,c12])).
% 9.64/1.65 cnf(d9, plain, 'Ts0'(sK9) | ~greater(sK2(sK9),appear('efficient$uproducers',sK9)) | 'Ts0'(sK9), inference(resolution, [status(thm)], [d8,d6])).
% 9.64/1.65 cnf(d10, plain, 'Ts0'(sK9) | 'Ts0'(sK9), inference(resolution, [status(thm)], [d9,c0])).
% 9.64/1.65 cnf(d11, plain, $false, inference(resolution, [status(thm)], [d10,d5])).
% 9.64/1.65 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------