%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT027+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 : n014.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:04 AM UTC 2026
% Result : Theorem 12.66s 2.06s
% Output : CNFRefutation 12.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 9
% Syntax : Number of formulae : 79 ( 8 unt; 0 def)
% Number of atoms : 376 ( 26 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 523 ( 226 ~; 264 |; 21 &)
% ( 1 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 100 ( 0 sgn 20 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mp_contracts_from,axiom,
! [X0,X1] :
( ( ! [X2] :
( ( 'greater$uor$uequal'(X2,X1)
& greater('cardinality$uat$utime'('first$umovers',X2),zero) )
=> greater(zero,'growth$urate'('first$umovers',X2)) )
& 'in$uenvironment'(X0,X1)
& stable(X0)
& environment(X0) )
=> 'contracts$ufrom'(X1,'first$umovers') ) ).
fof(mp_non_empty_fm_and_ep,axiom,
! [X0,X1] :
( ( greater('cardinality$uat$utime'('efficient$uproducers',X1),zero)
& greater('cardinality$uat$utime'('first$umovers',X1),zero)
& 'in$uenvironment'(X0,X1)
& environment(X0) )
=> subpopulations('first$umovers','efficient$uproducers',X0,X1) ) ).
fof(mp_long_stable_environments,axiom,
! [X0,X1,X2] :
( ( greater(X2,X1)
& 'in$uenvironment'(X0,X1)
& stable(X0)
& environment(X0) )
=> 'in$uenvironment'(X0,X2) ) ).
fof(mp_EP_in_stable_environments,axiom,
! [X0] :
( ( stable(X0)
& environment(X0) )
=> 'in$uenvironment'(X0,appear('efficient$uproducers',X0)) ) ).
fof(mp_greater_transitivity,axiom,
! [X0,X1,X2] :
( ( greater(X1,X2)
& greater(X0,X1) )
=> greater(X0,X2) ) ).
fof(mp_greater_or_equal,axiom,
! [X0,X1] :
( 'greater$uor$uequal'(X0,X1)
<=> ( X0 = X1
| greater(X0,X1) ) ) ).
fof(t6,hypothesis,
! [X0,X1] :
( ( 'greater$uor$uequal'(X1,appear('efficient$uproducers',X0))
& 'in$uenvironment'(X0,X1)
& environment(X0) )
=> greater('cardinality$uat$utime'('efficient$uproducers',X1),zero) ) ).
fof(l10,hypothesis,
! [X0] :
( ( stable(X0)
& environment(X0) )
=> ? [X1] :
( ! [X2] :
( ( 'greater$uor$uequal'(X2,X1)
& subpopulations('first$umovers','efficient$uproducers',X0,X2) )
=> greater(zero,'growth$urate'('first$umovers',X2)) )
& greater(X1,appear('efficient$uproducers',X0)) ) ) ).
fof(prove_l9,conjecture,
! [X0] :
( ( stable(X0)
& environment(X0) )
=> ? [X1] :
( 'contracts$ufrom'(X1,'first$umovers')
& greater(X1,appear('efficient$uproducers',X0)) ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0] :
( ( stable(X0)
& environment(X0) )
=> ? [X1] :
( 'contracts$ufrom'(X1,'first$umovers')
& greater(X1,appear('efficient$uproducers',X0)) ) ),
inference(negate_conjecture,[status(cth)],[prove_l9]) ).
cnf(c0,plain,
( greater('cardinality$uat$utime'('first$umovers',sK2(X1)),zero)
| ~ stable(X0)
| ~ 'in$uenvironment'(X0,X1)
| 'contracts$ufrom'(X1,'first$umovers')
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp_contracts_from]) ).
cnf(c1,plain,
( 'greater$uor$uequal'(sK2(X1),X1)
| ~ stable(X0)
| ~ 'in$uenvironment'(X0,X1)
| 'contracts$ufrom'(X1,'first$umovers')
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp_contracts_from]) ).
cnf(c2,plain,
( ~ stable(X0)
| ~ 'in$uenvironment'(X0,X1)
| 'contracts$ufrom'(X1,'first$umovers')
| ~ greater(zero,'growth$urate'('first$umovers',sK2(X1)))
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp_contracts_from]) ).
cnf(c3,plain,
( ~ environment(X1)
| subpopulations('first$umovers','efficient$uproducers',X1,X0)
| ~ greater('cardinality$uat$utime'('first$umovers',X0),zero)
| ~ 'in$uenvironment'(X1,X0)
| ~ greater('cardinality$uat$utime'('efficient$uproducers',X0),zero) ),
inference(clausification,[status(esa)],[mp_non_empty_fm_and_ep]) ).
cnf(c4,plain,
( ~ stable(X0)
| ~ environment(X0)
| ~ greater(X2,X1)
| 'in$uenvironment'(X0,X2)
| ~ 'in$uenvironment'(X0,X1) ),
inference(clausification,[status(esa)],[mp_long_stable_environments]) ).
cnf(c5,plain,
( 'in$uenvironment'(X0,appear('efficient$uproducers',X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(clausification,[status(esa)],[mp_EP_in_stable_environments]) ).
cnf(c6,plain,
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(clausification,[status(esa)],[mp_greater_transitivity]) ).
cnf(c7,plain,
( X0 = X1
| greater(X0,X1)
| ~ 'greater$uor$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[mp_greater_or_equal]) ).
cnf(c8,plain,
( ~ greater(X0,X1)
| 'greater$uor$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[mp_greater_or_equal]) ).
cnf(c9,plain,
( X0 != X1
| 'greater$uor$uequal'(X0,X1) ),
inference(clausification,[status(esa)],[mp_greater_or_equal]) ).
cnf(c10,plain,
( greater('cardinality$uat$utime'('efficient$uproducers',X1),zero)
| ~ 'greater$uor$uequal'(X1,appear('efficient$uproducers',X0))
| ~ 'in$uenvironment'(X0,X1)
| ~ environment(X0) ),
inference(clausification,[status(esa)],[t6]) ).
cnf(c11,plain,
( greater(sK17(X0),appear('efficient$uproducers',X0))
| ~ stable(X0)
| ~ environment(X0) ),
inference(clausification,[status(esa)],[l10]) ).
cnf(c12,plain,
( greater(zero,'growth$urate'('first$umovers',X1))
| ~ subpopulations('first$umovers','efficient$uproducers',X0,X1)
| ~ stable(X0)
| ~ 'greater$uor$uequal'(X1,sK17(X0))
| ~ environment(X0) ),
inference(clausification,[status(esa)],[l10]) ).
cnf(c13,plain,
environment(sK19),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c14,plain,
stable(sK19),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c15,plain,
( ~ 'contracts$ufrom'(X0,'first$umovers')
| ~ greater(X0,appear('efficient$uproducers',sK19)) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( 'in$uenvironment'(X1,sK17(X0))
| ~ 'in$uenvironment'(X1,appear('efficient$uproducers',X0))
| ~ environment(X1)
| ~ stable(X1)
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[c11,c4]) ).
cnf(d1,plain,
( ~ environment(X0)
| ~ stable(X0)
| 'in$uenvironment'(X0,sK17(X0))
| ~ environment(X0)
| ~ environment(X0)
| ~ stable(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[d0,c5]) ).
cnf(d2,plain,
( ~ 'contracts$ufrom'(sK17(sK19),'first$umovers')
| ~ environment(sK19)
| ~ stable(sK19) ),
inference(resolution,[status(thm)],[c11,c15]) ).
cnf(d3,plain,
( ~ 'contracts$ufrom'(sK17(sK19),'first$umovers')
| ~ stable(sK19) ),
inference(resolution,[status(thm)],[c13,d2]) ).
cnf(d4,plain,
~ 'contracts$ufrom'(sK17(sK19),'first$umovers'),
inference(resolution,[status(thm)],[c14,d3]) ).
cnf(d5,plain,
( 'greater$uor$uequal'(sK2(sK17(X0)),sK17(X0))
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[d1,c1]) ).
cnf(d6,plain,
( greater(sK2(sK17(X0)),sK17(X0))
| sK2(sK17(X0)) = sK17(X0)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[d5,c7]) ).
cnf(d7,plain,
( greater(sK2(sK17(X0)),X1)
| ~ greater(sK17(X0),X1)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d6,c6]) ).
cnf(d8,plain,
( 'in$uenvironment'(X2,sK2(sK17(X0)))
| ~ 'in$uenvironment'(X2,X1)
| ~ environment(X2)
| ~ stable(X2)
| ~ greater(sK17(X0),X1)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d7,c4]) ).
cnf(d9,plain,
( ~ environment(X0)
| ~ stable(X0)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| 'in$uenvironment'(X1,sK2(sK17(X0)))
| ~ 'in$uenvironment'(X1,appear('efficient$uproducers',X0))
| ~ environment(X0)
| ~ environment(X1)
| ~ stable(X0)
| ~ stable(X1)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d8,c11]) ).
cnf(d10,plain,
( ~ environment(X0)
| ~ stable(X0)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| 'in$uenvironment'(X0,sK2(sK17(X0)))
| ~ environment(X0)
| ~ environment(X0)
| ~ stable(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d9,c5]) ).
cnf(d11,plain,
( greater('cardinality$uat$utime'('first$umovers',sK2(sK17(X0))),zero)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[d1,c0]) ).
cnf(d12,plain,
( 'in$uenvironment'(X1,sK2(sK17(X0)))
| ~ 'in$uenvironment'(X1,sK17(X0))
| ~ environment(X1)
| ~ stable(X1)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d6,c4]) ).
cnf(d13,plain,
( 'greater$uor$uequal'(sK2(sK17(X0)),X1)
| ~ greater(sK17(X0),X1)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d7,c8]) ).
cnf(d14,plain,
( greater('cardinality$uat$utime'('efficient$uproducers',sK2(sK17(X0))),zero)
| ~ 'in$uenvironment'(X1,sK2(sK17(X0)))
| ~ environment(X1)
| ~ greater(sK17(X0),appear('efficient$uproducers',X1))
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d13,c10]) ).
cnf(d15,plain,
( ~ environment(X0)
| ~ stable(X0)
| greater('cardinality$uat$utime'('efficient$uproducers',sK2(sK17(X0))),zero)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ 'in$uenvironment'(X0,sK2(sK17(X0)))
| ~ environment(X0)
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d14,c11]) ).
cnf(d16,plain,
( 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ 'in$uenvironment'(X0,sK17(X0))
| ~ environment(X0)
| ~ environment(X0)
| ~ stable(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0)
| greater('cardinality$uat$utime'('efficient$uproducers',sK2(sK17(X0))),zero)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d15,d12]) ).
cnf(d17,plain,
( ~ environment(X0)
| ~ stable(X0)
| greater('cardinality$uat$utime'('efficient$uproducers',sK2(sK17(X0))),zero)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d16,d1]) ).
cnf(d18,plain,
( subpopulations('first$umovers','efficient$uproducers',X1,sK2(sK17(X0)))
| ~ greater('cardinality$uat$utime'('first$umovers',sK2(sK17(X0))),zero)
| ~ 'in$uenvironment'(X1,sK2(sK17(X0)))
| ~ environment(X1)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d17,c3]) ).
cnf(d19,plain,
( 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| subpopulations('first$umovers','efficient$uproducers',X1,sK2(sK17(X0)))
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ 'in$uenvironment'(X1,sK2(sK17(X0)))
| ~ environment(X0)
| ~ environment(X1)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d18,d11]) ).
cnf(d20,plain,
( ~ 'greater$uor$uequal'(sK2(sK17(X0)),sK17(X1))
| greater(zero,'growth$urate'('first$umovers',sK2(sK17(X0))))
| ~ environment(X1)
| ~ stable(X1)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ 'in$uenvironment'(X1,sK2(sK17(X0)))
| ~ environment(X0)
| ~ environment(X1)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d19,c12]) ).
cnf(d21,plain,
( 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| greater(zero,'growth$urate'('first$umovers',sK2(sK17(X0))))
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ 'in$uenvironment'(X0,sK2(sK17(X0)))
| ~ environment(X0)
| ~ environment(X0)
| ~ stable(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d20,d5]) ).
cnf(d22,plain,
( 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0)
| greater(zero,'growth$urate'('first$umovers',sK2(sK17(X0))))
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d21,d10]) ).
cnf(d23,plain,
( 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ 'in$uenvironment'(X1,sK17(X0))
| ~ environment(X1)
| ~ stable(X1)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d22,c2]) ).
cnf(d24,plain,
( ~ environment(X0)
| ~ stable(X0)
| 'contracts$ufrom'(sK17(X0),'first$umovers')
| ~ environment(X0)
| ~ environment(X0)
| ~ stable(X0)
| ~ stable(X0)
| sK2(sK17(X0)) = sK17(X0) ),
inference(resolution,[status(thm)],[d23,d1]) ).
cnf(d25,plain,
( ~ environment(sK19)
| ~ stable(sK19)
| sK2(sK17(sK19)) = sK17(sK19) ),
inference(resolution,[status(thm)],[d24,d4]) ).
cnf(d26,plain,
( ~ stable(sK19)
| sK2(sK17(sK19)) = sK17(sK19) ),
inference(resolution,[status(thm)],[c13,d25]) ).
cnf(d27,plain,
sK2(sK17(sK19)) = sK17(sK19),
inference(resolution,[status(thm)],[c14,d26]) ).
cnf(d28,plain,
( 'contracts$ufrom'(sK17(sK19),'first$umovers')
| ~ 'in$uenvironment'(X0,sK17(sK19))
| ~ environment(X0)
| ~ stable(X0)
| ~ greater(zero,'growth$urate'('first$umovers',sK17(sK19))) ),
inference(superposition,[status(thm)],[d27,c2]) ).
cnf(d29,plain,
( ~ greater(zero,'growth$urate'('first$umovers',sK17(sK19)))
| ~ 'in$uenvironment'(X0,sK17(sK19))
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[d4,d28]) ).
cnf(d30,plain,
'greater$uor$uequal'(X0,X0),
inference(equality_resolution,[status(thm)],[c9]) ).
cnf(d31,plain,
( 'greater$uor$uequal'(sK17(X0),appear('efficient$uproducers',X0))
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[c11,c8]) ).
cnf(d32,plain,
( greater('cardinality$uat$utime'('efficient$uproducers',sK17(X0)),zero)
| ~ 'in$uenvironment'(X0,sK17(X0))
| ~ environment(X0)
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[d31,c10]) ).
cnf(d33,plain,
( ~ environment(X0)
| ~ stable(X0)
| greater('cardinality$uat$utime'('efficient$uproducers',sK17(X0)),zero)
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[d32,d1]) ).
cnf(d34,plain,
( subpopulations('first$umovers','efficient$uproducers',X1,sK17(X0))
| ~ greater('cardinality$uat$utime'('first$umovers',sK17(X0)),zero)
| ~ 'in$uenvironment'(X1,sK17(X0))
| ~ environment(X1)
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[d33,c3]) ).
cnf(d35,plain,
( 'contracts$ufrom'(sK17(sK19),'first$umovers')
| ~ environment(sK19)
| ~ stable(sK19)
| greater('cardinality$uat$utime'('first$umovers',sK17(sK19)),zero) ),
inference(superposition,[status(thm)],[d27,d11]) ).
cnf(d36,plain,
( greater('cardinality$uat$utime'('first$umovers',sK17(sK19)),zero)
| 'contracts$ufrom'(sK17(sK19),'first$umovers')
| ~ stable(sK19) ),
inference(resolution,[status(thm)],[c13,d35]) ).
cnf(d37,plain,
( greater('cardinality$uat$utime'('first$umovers',sK17(sK19)),zero)
| 'contracts$ufrom'(sK17(sK19),'first$umovers') ),
inference(resolution,[status(thm)],[c14,d36]) ).
cnf(d38,plain,
greater('cardinality$uat$utime'('first$umovers',sK17(sK19)),zero),
inference(resolution,[status(thm)],[d4,d37]) ).
cnf(d39,plain,
( subpopulations('first$umovers','efficient$uproducers',X0,sK17(sK19))
| ~ 'in$uenvironment'(X0,sK17(sK19))
| ~ environment(sK19)
| ~ environment(X0)
| ~ stable(sK19) ),
inference(resolution,[status(thm)],[d38,d34]) ).
cnf(d40,plain,
( subpopulations('first$umovers','efficient$uproducers',X0,sK17(sK19))
| ~ 'in$uenvironment'(X0,sK17(sK19))
| ~ environment(X0)
| ~ stable(sK19) ),
inference(resolution,[status(thm)],[c13,d39]) ).
cnf(d41,plain,
( subpopulations('first$umovers','efficient$uproducers',X0,sK17(sK19))
| ~ 'in$uenvironment'(X0,sK17(sK19))
| ~ environment(X0) ),
inference(resolution,[status(thm)],[c14,d40]) ).
cnf(d42,plain,
( ~ 'greater$uor$uequal'(sK17(sK19),sK17(X0))
| greater(zero,'growth$urate'('first$umovers',sK17(sK19)))
| ~ environment(X0)
| ~ stable(X0)
| ~ 'in$uenvironment'(X0,sK17(sK19))
| ~ environment(X0) ),
inference(resolution,[status(thm)],[d41,c12]) ).
cnf(d43,plain,
( greater(zero,'growth$urate'('first$umovers',sK17(sK19)))
| ~ 'in$uenvironment'(sK19,sK17(sK19))
| ~ environment(sK19)
| ~ stable(sK19) ),
inference(resolution,[status(thm)],[d42,d30]) ).
cnf(d44,plain,
( greater(zero,'growth$urate'('first$umovers',sK17(sK19)))
| ~ 'in$uenvironment'(sK19,sK17(sK19))
| ~ stable(sK19) ),
inference(resolution,[status(thm)],[c13,d43]) ).
cnf(d45,plain,
( greater(zero,'growth$urate'('first$umovers',sK17(sK19)))
| ~ 'in$uenvironment'(sK19,sK17(sK19)) ),
inference(resolution,[status(thm)],[c14,d44]) ).
cnf(d46,plain,
( ~ 'in$uenvironment'(X0,sK17(sK19))
| ~ environment(X0)
| ~ stable(X0)
| ~ 'in$uenvironment'(sK19,sK17(sK19)) ),
inference(resolution,[status(thm)],[d45,d29]) ).
cnf(d47,plain,
( ~ environment(sK19)
| ~ stable(sK19)
| ~ 'in$uenvironment'(X0,sK17(sK19))
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[d46,d1]) ).
cnf(d48,plain,
( ~ 'in$uenvironment'(X0,sK17(sK19))
| ~ environment(X0)
| ~ stable(sK19)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[c13,d47]) ).
cnf(d49,plain,
( ~ 'in$uenvironment'(X0,sK17(sK19))
| ~ environment(X0)
| ~ stable(X0) ),
inference(resolution,[status(thm)],[c14,d48]) ).
cnf(d50,plain,
( ~ environment(sK19)
| ~ stable(sK19)
| ~ environment(sK19)
| ~ stable(sK19) ),
inference(resolution,[status(thm)],[d49,d1]) ).
cnf(d51,plain,
~ stable(sK19),
inference(resolution,[status(thm)],[c13,d50]) ).
cnf(d52,plain,
$false,
inference(resolution,[status(thm)],[c14,d51]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT027+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.05 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n014.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 00:04:48 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.66/2.06 % SZS status Theorem for theBenchmark.p
% 12.66/2.06 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------