%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT031+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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 : Tue Sep 8 06:18:43 AM UTC 2026
% Result : CounterSatisfiable 0.39s 0.66s
% Output : Saturation 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT031+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 12:20:30 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.42 (re.compile("\."), Token.FullStop),
% 0.09/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.42 (re.compile("\("), Token.OpenPar),
% 0.09/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.42 (re.compile("\)"), Token.ClosePar),
% 0.09/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.42 (re.compile("\["), Token.OpenSquare),
% 0.09/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.42 (re.compile("~\|"), Token.Nor),
% 0.09/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.42 (re.compile("\|"), Token.Or),
% 0.09/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.42 (re.compile("\?"), Token.Existential),
% 0.09/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.49 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.32/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 0.39/0.66 % Version: 1.5
% 0.39/0.66 % SZS status CounterSatisfiable
% 0.39/0.66 % SZS output start Saturation
% 0.39/0.66 cnf(reflexivity,axiom,X23=X23,theory(equality)).
% 0.39/0.66 cnf(c7,axiom,X100!=X101|X102!=X99|~greater_or_equal(X100,X102)|greater_or_equal(X101,X99),theory(equality)).
% 0.39/0.66 fof(mp_greater_or_equal,axiom,(![X]:(![Y]:(greater_or_equal(X,Y)<=>(greater(X,Y)|X=Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_or_equal)).
% 0.39/0.66 fof(c23,plain,(![X]:(![Y]:((~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))&((~greater(X,Y)&X!=Y)|greater_or_equal(X,Y))))),inference(fof_nnf,[status(thm)],[mp_greater_or_equal])).
% 0.39/0.66 fof(c24,plain,((![X]:(![Y]:(~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))))&(![X]:(![Y]:((~greater(X,Y)&X!=Y)|greater_or_equal(X,Y))))),inference(shift_quantors,[status(thm)],[c23])).
% 0.39/0.66 fof(c26,plain,(![X7]:(![X8]:(![X9]:(![X10]:((~greater_or_equal(X7,X8)|(greater(X7,X8)|X7=X8))&((~greater(X9,X10)&X9!=X10)|greater_or_equal(X9,X10))))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,((![X7]:(![X8]:(~greater_or_equal(X7,X8)|(greater(X7,X8)|X7=X8))))&(![X9]:(![X10]:((~greater(X9,X10)&X9!=X10)|greater_or_equal(X9,X10))))),inference(variable_rename,[status(thm)],[c24])).])).
% 0.39/0.66 fof(c27,plain,(![X7]:(![X8]:(![X9]:(![X10]:((~greater_or_equal(X7,X8)|(greater(X7,X8)|X7=X8))&((~greater(X9,X10)|greater_or_equal(X9,X10))&(X9!=X10|greater_or_equal(X9,X10)))))))),inference(distribute,[status(thm)],[c26])).
% 0.39/0.66 cnf(c29,plain,~greater(X27,X28)|greater_or_equal(X27,X28),inference(split_conjunct,[status(thm)],[c27])).
% 0.39/0.66 fof(prove_l13,conjecture,(![E]:((environment(E)&in_environment(E,appear(an_organisation,E)))=>appear(an_organisation,E)=appear(first_movers,E))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l13)).
% 0.39/0.66 fof(c8,negated_conjecture,(~(![E]:((environment(E)&in_environment(E,appear(an_organisation,E)))=>appear(an_organisation,E)=appear(first_movers,E)))),inference(assume_negation,[status(cth)],[prove_l13])).
% 0.39/0.66 fof(c9,negated_conjecture,(?[E]:((environment(E)&in_environment(E,appear(an_organisation,E)))&appear(an_organisation,E)!=appear(first_movers,E))),inference(fof_nnf,[status(thm)],[c8])).
% 0.39/0.66 fof(c10,negated_conjecture,(?[X2]:((environment(X2)&in_environment(X2,appear(an_organisation,X2)))&appear(an_organisation,X2)!=appear(first_movers,X2))),inference(variable_rename,[status(thm)],[c9])).
% 0.39/0.66 fof(c11,negated_conjecture,((environment(skolem0001)&in_environment(skolem0001,appear(an_organisation,skolem0001)))&appear(an_organisation,skolem0001)!=appear(first_movers,skolem0001)),inference(skolemize,[status(esa)],[c10])).
% 0.39/0.66 cnf(c12,negated_conjecture,environment(skolem0001),inference(split_conjunct,[status(thm)],[c11])).
% 0.39/0.66 fof(a13,plain,(![E]:(environment(E)=>greater(appear(efficient_producers,e),appear(first_movers,E)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a13)).
% 0.39/0.66 fof(c15,plain,(![E]:(~environment(E)|greater(appear(efficient_producers,e),appear(first_movers,E)))),inference(fof_nnf,[status(thm)],[a13])).
% 0.39/0.66 fof(c16,plain,(![X3]:(~environment(X3)|greater(appear(efficient_producers,e),appear(first_movers,X3)))),inference(variable_rename,[status(thm)],[c15])).
% 0.39/0.66 cnf(c17,plain,~environment(X108)|greater(appear(efficient_producers,e),appear(first_movers,X108)),inference(split_conjunct,[status(thm)],[c16])).
% 0.39/0.66 cnf(c80,plain,greater(appear(efficient_producers,e),appear(first_movers,skolem0001)),inference(resolution,[status(thm)],[c17, c12])).
% 0.39/0.66 fof(mp_greater_transitivity,axiom,(![X]:(![Y]:(![Z]:((greater(X,Y)&greater(Y,Z))=>greater(X,Z))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_transitivity)).
% 0.39/0.66 fof(c31,plain,(![X]:(![Y]:(![Z]:((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))))),inference(fof_nnf,[status(thm)],[mp_greater_transitivity])).
% 0.39/0.66 fof(c32,plain,(![X11]:(![X12]:(![X13]:((~greater(X11,X12)|~greater(X12,X13))|greater(X11,X13))))),inference(variable_rename,[status(thm)],[c31])).
% 0.39/0.66 cnf(c33,plain,~greater(X48,X49)|~greater(X49,X50)|greater(X48,X50),inference(split_conjunct,[status(thm)],[c32])).
% 0.39/0.66 cnf(c14,negated_conjecture,appear(an_organisation,skolem0001)!=appear(first_movers,skolem0001),inference(split_conjunct,[status(thm)],[c11])).
% 0.39/0.66 cnf(symmetry,axiom,X24!=X25|X25=X24,theory(equality)).
% 0.39/0.66 cnf(c28,plain,~greater_or_equal(X46,X45)|greater(X46,X45)|X46=X45,inference(split_conjunct,[status(thm)],[c27])).
% 0.39/0.66 fof(mp_FM_not_precede_first,axiom,(![E]:(environment(E)=>greater_or_equal(appear(first_movers,E),appear(an_organisation,E)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_FM_not_precede_first)).
% 0.39/0.66 fof(c34,plain,(![E]:(~environment(E)|greater_or_equal(appear(first_movers,E),appear(an_organisation,E)))),inference(fof_nnf,[status(thm)],[mp_FM_not_precede_first])).
% 0.39/0.66 fof(c35,plain,(![X14]:(~environment(X14)|greater_or_equal(appear(first_movers,X14),appear(an_organisation,X14)))),inference(variable_rename,[status(thm)],[c34])).
% 0.39/0.66 cnf(c36,plain,~environment(X88)|greater_or_equal(appear(first_movers,X88),appear(an_organisation,X88)),inference(split_conjunct,[status(thm)],[c35])).
% 0.39/0.66 cnf(c73,plain,greater_or_equal(appear(first_movers,skolem0001),appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c36, c12])).
% 0.39/0.66 cnf(c74,plain,greater(appear(first_movers,skolem0001),appear(an_organisation,skolem0001))|appear(first_movers,skolem0001)=appear(an_organisation,skolem0001),inference(resolution,[status(thm)],[c73, c28])).
% 0.39/0.67 cnf(c113,plain,greater(appear(first_movers,skolem0001),appear(an_organisation,skolem0001))|appear(an_organisation,skolem0001)=appear(first_movers,skolem0001),inference(resolution,[status(thm)],[c74, symmetry])).
% 0.39/0.67 cnf(c138,plain,greater(appear(first_movers,skolem0001),appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c113, c14])).
% 0.39/0.67 cnf(c150,plain,~greater(X145,appear(first_movers,skolem0001))|greater(X145,appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c138, c33])).
% 0.39/0.67 cnf(c153,plain,greater(appear(efficient_producers,e),appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c150, c80])).
% 0.39/0.67 cnf(c154,plain,greater_or_equal(appear(efficient_producers,e),appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c153, c29])).
% 0.39/0.67 cnf(c158,plain,appear(efficient_producers,e)!=X155|appear(an_organisation,skolem0001)!=X156|greater_or_equal(X155,X156),inference(resolution,[status(thm)],[c154, c7])).
% 0.39/0.67 cnf(c164,plain,appear(efficient_producers,e)!=X157|greater_or_equal(X157,appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c158, reflexivity])).
% 0.39/0.67 cnf(c4,axiom,X77!=X78|X79!=X76|~greater(X77,X79)|greater(X78,X76),theory(equality)).
% 0.39/0.67 cnf(c156,plain,appear(efficient_producers,e)!=X153|appear(an_organisation,skolem0001)!=X152|greater(X153,X152),inference(resolution,[status(thm)],[c153, c4])).
% 0.39/0.67 cnf(c162,plain,appear(efficient_producers,e)!=X154|greater(X154,appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c156, reflexivity])).
% 0.39/0.67 cnf(c151,plain,appear(first_movers,skolem0001)!=X150|appear(an_organisation,skolem0001)!=X149|greater(X150,X149),inference(resolution,[status(thm)],[c138, c4])).
% 0.39/0.67 cnf(c160,plain,appear(first_movers,skolem0001)!=X151|greater(X151,appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c151, reflexivity])).
% 0.39/0.67 cnf(c155,plain,~greater(X146,appear(efficient_producers,e))|greater(X146,appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c153, c33])).
% 0.39/0.67 fof(mp_positive_number_when_appear,axiom,(![E]:(environment(E)=>greater(number_of_organizations(e,appear(an_organisation,E)),zero))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_positive_number_when_appear)).
% 0.39/0.67 fof(c51,plain,(![E]:(~environment(E)|greater(number_of_organizations(e,appear(an_organisation,E)),zero))),inference(fof_nnf,[status(thm)],[mp_positive_number_when_appear])).
% 0.39/0.67 fof(c52,plain,(![X22]:(~environment(X22)|greater(number_of_organizations(e,appear(an_organisation,X22)),zero))),inference(variable_rename,[status(thm)],[c51])).
% 0.39/0.67 cnf(c53,plain,~environment(X112)|greater(number_of_organizations(e,appear(an_organisation,X112)),zero),inference(split_conjunct,[status(thm)],[c52])).
% 0.39/0.67 cnf(c87,plain,greater(number_of_organizations(e,appear(an_organisation,skolem0001)),zero),inference(resolution,[status(thm)],[c53, c12])).
% 0.39/0.67 fof(mp_number_mean_non_empty,axiom,(![E]:(![T]:((environment(E)&greater(number_of_organizations(E,T),zero))=>(?[S]:(subpopulation(S,E,T)&greater(cardinality_at_time(S,T),zero)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_number_mean_non_empty)).
% 0.39/0.67 fof(c45,plain,(![E]:(![T]:((~environment(E)|~greater(number_of_organizations(E,T),zero))|(?[S]:(subpopulation(S,E,T)&greater(cardinality_at_time(S,T),zero)))))),inference(fof_nnf,[status(thm)],[mp_number_mean_non_empty])).
% 0.39/0.67 fof(c46,plain,(![X19]:(![X20]:((~environment(X19)|~greater(number_of_organizations(X19,X20),zero))|(?[X21]:(subpopulation(X21,X19,X20)&greater(cardinality_at_time(X21,X20),zero)))))),inference(variable_rename,[status(thm)],[c45])).
% 0.39/0.67 fof(c47,plain,(![X19]:(![X20]:((~environment(X19)|~greater(number_of_organizations(X19,X20),zero))|(subpopulation(skolem0002(X19,X20),X19,X20)&greater(cardinality_at_time(skolem0002(X19,X20),X20),zero))))),inference(skolemize,[status(esa)],[c46])).
% 0.39/0.67 fof(c48,plain,(![X19]:(![X20]:(((~environment(X19)|~greater(number_of_organizations(X19,X20),zero))|subpopulation(skolem0002(X19,X20),X19,X20))&((~environment(X19)|~greater(number_of_organizations(X19,X20),zero))|greater(cardinality_at_time(skolem0002(X19,X20),X20),zero))))),inference(distribute,[status(thm)],[c47])).
% 0.39/0.67 cnf(c50,plain,~environment(X125)|~greater(number_of_organizations(X125,X126),zero)|greater(cardinality_at_time(skolem0002(X125,X126),X126),zero),inference(split_conjunct,[status(thm)],[c48])).
% 0.39/0.67 cnf(c96,plain,~environment(e)|greater(cardinality_at_time(skolem0002(e,appear(an_organisation,skolem0001)),appear(an_organisation,skolem0001)),zero),inference(resolution,[status(thm)],[c50, c87])).
% 0.39/0.67 cnf(c49,plain,~environment(X123)|~greater(number_of_organizations(X123,X124),zero)|subpopulation(skolem0002(X123,X124),X123,X124),inference(split_conjunct,[status(thm)],[c48])).
% 0.39/0.67 cnf(c95,plain,~environment(e)|subpopulation(skolem0002(e,appear(an_organisation,skolem0001)),e,appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c49, c87])).
% 0.39/0.67 cnf(c88,plain,greater_or_equal(number_of_organizations(e,appear(an_organisation,skolem0001)),zero),inference(resolution,[status(thm)],[c87, c29])).
% 0.39/0.67 cnf(c92,plain,number_of_organizations(e,appear(an_organisation,skolem0001))!=X141|zero!=X142|greater_or_equal(X141,X142),inference(resolution,[status(thm)],[c88, c7])).
% 0.39/0.67 cnf(c126,plain,zero!=X143|greater_or_equal(number_of_organizations(e,appear(an_organisation,skolem0001)),X143),inference(resolution,[status(thm)],[c92, reflexivity])).
% 0.39/0.67 cnf(c90,plain,number_of_organizations(e,appear(an_organisation,skolem0001))!=X139|zero!=X138|greater(X139,X138),inference(resolution,[status(thm)],[c87, c4])).
% 0.39/0.67 cnf(c124,plain,zero!=X140|greater(number_of_organizations(e,appear(an_organisation,skolem0001)),X140),inference(resolution,[status(thm)],[c90, reflexivity])).
% 0.39/0.67 cnf(c82,plain,greater_or_equal(appear(efficient_producers,e),appear(first_movers,skolem0001)),inference(resolution,[status(thm)],[c80, c29])).
% 0.39/0.67 cnf(c86,plain,appear(efficient_producers,e)!=X135|appear(first_movers,skolem0001)!=X136|greater_or_equal(X135,X136),inference(resolution,[status(thm)],[c82, c7])).
% 0.39/0.67 cnf(c122,plain,appear(efficient_producers,e)!=X137|greater_or_equal(X137,appear(first_movers,skolem0001)),inference(resolution,[status(thm)],[c86, reflexivity])).
% 0.39/0.67 cnf(c84,plain,appear(efficient_producers,e)!=X133|appear(first_movers,skolem0001)!=X132|greater(X133,X132),inference(resolution,[status(thm)],[c80, c4])).
% 0.39/0.67 cnf(c99,plain,appear(efficient_producers,e)!=X134|greater(X134,appear(first_movers,skolem0001)),inference(resolution,[status(thm)],[c84, reflexivity])).
% 0.39/0.67 cnf(c76,plain,appear(first_movers,skolem0001)!=X127|appear(an_organisation,skolem0001)!=X128|greater_or_equal(X127,X128),inference(resolution,[status(thm)],[c7, c73])).
% 0.39/0.67 cnf(c97,plain,appear(first_movers,skolem0001)!=X131|greater_or_equal(X131,appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c76, reflexivity])).
% 0.39/0.67 fof(mp_no_EP_before_appearance,axiom,(![E]:(![T]:(((environment(E)&in_environment(E,T))&greater(appear(efficient_producers,E),T))=>(~greater(cardinality_at_time(efficient_producers,T),zero))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_no_EP_before_appearance)).
% 0.39/0.67 fof(c41,plain,(![E]:(![T]:(((environment(E)&in_environment(E,T))&greater(appear(efficient_producers,E),T))=>~greater(cardinality_at_time(efficient_producers,T),zero)))),inference(fof_simplification,[status(thm)],[mp_no_EP_before_appearance])).
% 0.39/0.67 fof(c42,plain,(![E]:(![T]:(((~environment(E)|~in_environment(E,T))|~greater(appear(efficient_producers,E),T))|~greater(cardinality_at_time(efficient_producers,T),zero)))),inference(fof_nnf,[status(thm)],[c41])).
% 0.39/0.67 fof(c43,plain,(![X17]:(![X18]:(((~environment(X17)|~in_environment(X17,X18))|~greater(appear(efficient_producers,X17),X18))|~greater(cardinality_at_time(efficient_producers,X18),zero)))),inference(variable_rename,[status(thm)],[c42])).
% 0.39/0.67 cnf(c44,plain,~environment(X129)|~in_environment(X129,X130)|~greater(appear(efficient_producers,X129),X130)|~greater(cardinality_at_time(efficient_producers,X130),zero),inference(split_conjunct,[status(thm)],[c43])).
% 0.39/0.67 cnf(c89,plain,~greater(X122,number_of_organizations(e,appear(an_organisation,skolem0001)))|greater(X122,zero),inference(resolution,[status(thm)],[c87, c33])).
% 0.39/0.67 cnf(c83,plain,~greater(X121,appear(efficient_producers,e))|greater(X121,appear(first_movers,skolem0001)),inference(resolution,[status(thm)],[c80, c33])).
% 0.39/0.67 fof(mp_no_FM_before_appearance,axiom,(![E]:(![T]:(((environment(E)&in_environment(E,T))&greater(appear(first_movers,E),T))=>(~greater(cardinality_at_time(first_movers,T),zero))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_no_FM_before_appearance)).
% 0.39/0.67 fof(c37,plain,(![E]:(![T]:(((environment(E)&in_environment(E,T))&greater(appear(first_movers,E),T))=>~greater(cardinality_at_time(first_movers,T),zero)))),inference(fof_simplification,[status(thm)],[mp_no_FM_before_appearance])).
% 0.39/0.67 fof(c38,plain,(![E]:(![T]:(((~environment(E)|~in_environment(E,T))|~greater(appear(first_movers,E),T))|~greater(cardinality_at_time(first_movers,T),zero)))),inference(fof_nnf,[status(thm)],[c37])).
% 0.39/0.67 fof(c39,plain,(![X15]:(![X16]:(((~environment(X15)|~in_environment(X15,X16))|~greater(appear(first_movers,X15),X16))|~greater(cardinality_at_time(first_movers,X16),zero)))),inference(variable_rename,[status(thm)],[c38])).
% 0.39/0.67 cnf(c40,plain,~environment(X119)|~in_environment(X119,X120)|~greater(appear(first_movers,X119),X120)|~greater(cardinality_at_time(first_movers,X120),zero),inference(split_conjunct,[status(thm)],[c39])).
% 0.39/0.67 cnf(c13,negated_conjecture,in_environment(skolem0001,appear(an_organisation,skolem0001)),inference(split_conjunct,[status(thm)],[c11])).
% 0.39/0.67 cnf(c6,axiom,X96!=X97|X98!=X95|~in_environment(X96,X98)|in_environment(X97,X95),theory(equality)).
% 0.39/0.67 cnf(c75,plain,skolem0001!=X116|appear(an_organisation,skolem0001)!=X117|in_environment(X116,X117),inference(resolution,[status(thm)],[c6, c13])).
% 0.39/0.67 cnf(c93,plain,skolem0001!=X118|in_environment(X118,appear(an_organisation,skolem0001)),inference(resolution,[status(thm)],[c75, reflexivity])).
% 0.39/0.67 fof(a9,plain,(![E]:(![X]:(![T]:(((environment(E)&subpopulation(X,E,T))&greater(cardinality_at_time(X,T),zero))=>(X=efficient_producers|X=first_movers))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a9)).
% 0.39/0.67 fof(c18,plain,(![E]:(![X]:(![T]:(((~environment(E)|~subpopulation(X,E,T))|~greater(cardinality_at_time(X,T),zero))|(X=efficient_producers|X=first_movers))))),inference(fof_nnf,[status(thm)],[a9])).
% 0.39/0.67 fof(c19,plain,(![E]:(![X]:((![T]:((~environment(E)|~subpopulation(X,E,T))|~greater(cardinality_at_time(X,T),zero)))|(X=efficient_producers|X=first_movers)))),inference(shift_quantors,[status(thm)],[c18])).
% 0.39/0.67 fof(c21,plain,(![X4]:(![X5]:(![X6]:(((~environment(X4)|~subpopulation(X5,X4,X6))|~greater(cardinality_at_time(X5,X6),zero))|(X5=efficient_producers|X5=first_movers))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,(![X4]:(![X5]:((![X6]:((~environment(X4)|~subpopulation(X5,X4,X6))|~greater(cardinality_at_time(X5,X6),zero)))|(X5=efficient_producers|X5=first_movers)))),inference(variable_rename,[status(thm)],[c19])).])).
% 0.39/0.67 cnf(c22,plain,~environment(X113)|~subpopulation(X114,X113,X115)|~greater(cardinality_at_time(X114,X115),zero)|X114=efficient_producers|X114=first_movers,inference(split_conjunct,[status(thm)],[c21])).
% 0.39/0.67 cnf(c30,plain,X32!=X33|greater_or_equal(X32,X33),inference(split_conjunct,[status(thm)],[c27])).
% 0.39/0.67 cnf(c57,plain,greater_or_equal(X34,X34),inference(resolution,[status(thm)],[c30, reflexivity])).
% 0.39/0.67 cnf(c77,plain,X104!=X103|X104!=X105|greater_or_equal(X103,X105),inference(resolution,[status(thm)],[c7, c57])).
% 0.39/0.67 cnf(c79,plain,X110!=X109|greater_or_equal(X109,X110),inference(resolution,[status(thm)],[c77, reflexivity])).
% 0.39/0.67 cnf(c5,axiom,X89!=X92|X93!=X90|X91!=X94|~subpopulation(X89,X93,X91)|subpopulation(X92,X90,X94),theory(equality)).
% 0.39/0.67 cnf(c2,axiom,X63!=X64|X65!=X62|cardinality_at_time(X63,X65)=cardinality_at_time(X64,X62),theory(equality)).
% 0.39/0.67 cnf(c68,plain,X83!=X84|cardinality_at_time(X83,X85)=cardinality_at_time(X84,X85),inference(resolution,[status(thm)],[c2, reflexivity])).
% 0.39/0.67 cnf(c67,plain,X81!=X80|cardinality_at_time(X81,X81)=cardinality_at_time(X80,X80),inference(factor,[status(thm)],[c2])).
% 0.39/0.67 cnf(c1,axiom,X52!=X53|X54!=X51|appear(X52,X54)=appear(X53,X51),theory(equality)).
% 0.39/0.67 cnf(c64,plain,X73!=X71|appear(X73,X72)=appear(X71,X72),inference(resolution,[status(thm)],[c1, reflexivity])).
% 0.39/0.67 cnf(c63,plain,X68!=X69|appear(X68,X68)=appear(X69,X69),inference(factor,[status(thm)],[c1])).
% 0.39/0.67 cnf(c0,axiom,X41!=X42|X43!=X40|number_of_organizations(X41,X43)=number_of_organizations(X42,X40),theory(equality)).
% 0.39/0.67 cnf(c60,plain,X59!=X60|number_of_organizations(X59,X61)=number_of_organizations(X60,X61),inference(resolution,[status(thm)],[c0, reflexivity])).
% 0.39/0.67 cnf(c59,plain,X57!=X56|number_of_organizations(X57,X57)=number_of_organizations(X56,X56),inference(factor,[status(thm)],[c0])).
% 0.39/0.67 cnf(c3,axiom,X38!=X39|~environment(X38)|environment(X39),theory(equality)).
% 0.39/0.67 cnf(transitivity,axiom,X29!=X31|X31!=X30|X29=X30,theory(equality)).
% 0.39/0.67 % SZS output end Saturation
% 0.39/0.67
% 0.39/0.67 % Initial clauses : 26
% 0.39/0.67 % Processed clauses : 71
% 0.39/0.67 % Factors computed : 6
% 0.39/0.67 % Resolvents computed: 106
% 0.39/0.67 % Tautologies deleted: 4
% 0.39/0.67 % Forward subsumed : 63
% 0.39/0.67 % Backward subsumed : 4
% 0.39/0.67 % -------- CPU Time ---------
% 0.39/0.67 % User time : 0.275 s
% 0.39/0.67 % System time : 0.030 s
% 0.39/0.67 % Total time : 0.305 s
%------------------------------------------------------------------------------