%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : MGT033-2 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 12:02:06 PM UTC 2026
% Result : Satisfiable 2.71s 1.32s
% Output : Saturation 3.80s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u46,negated_conjecture,
sk3 = appear(first_movers,sk2) ).
cnf(u49,negated_conjecture,
~ greater(sk3,appear(first_movers,sk2)) ).
cnf(u63,axiom,
~ environment(e) ).
cnf(u74,negated_conjecture,
greater(appear(efficient_producers,e),appear(first_movers,sk2)) ).
cnf(u77,negated_conjecture,
( ~ greater(appear(first_movers,X0),sk3)
| ~ environment(X0) ) ).
cnf(u86,negated_conjecture,
~ greater(sk3,sk3) ).
cnf(u94,negated_conjecture,
~ greater(zero,sk3) ).
cnf(u131,negated_conjecture,
selection_favors(efficient_producers,efficient_producers,sk3) ).
cnf(u137,negated_conjecture,
greater(zero,zero) ).
cnf(u170,negated_conjecture,
zero != cardinality_at_time(first_movers,appear(first_movers,sk2)) ).
cnf(u174,negated_conjecture,
( ~ in_environment(X0,appear(first_movers,sk2))
| ~ environment(X0)
| start_time(X0) = appear(first_movers,X0)
| ~ greater(start_time(X0),sk3) ) ).
cnf(u200,negated_conjecture,
sk3 != start_time(sk2) ).
cnf(u205,negated_conjecture,
greater(sk3,start_time(sk2)) ).
cnf(u273,negated_conjecture,
zero = cardinality_at_time(first_movers,start_time(sk2)) ).
cnf(u276,negated_conjecture,
appear(first_movers,sk2) != start_time(sk2) ).
cnf(u305,negated_conjecture,
greater(appear(efficient_producers,e),start_time(sk2)) ).
cnf(u309,negated_conjecture,
( greater(X0,start_time(sk2))
| ~ greater(X0,sk3) ) ).
cnf(u393,negated_conjecture,
~ greater(sk3,appear(an_organisation,sk2)) ).
cnf(u398,negated_conjecture,
appear(first_movers,sk2) = appear(an_organisation,sk2) ).
cnf(u402,negated_conjecture,
( greater(X0,appear(an_organisation,sk2))
| ~ greater(X0,sk3) ) ).
cnf(u490,negated_conjecture,
efficient_producers = sk1(appear(first_movers,sk2),sk2) ).
cnf(u493,negated_conjecture,
first_movers != sk1(appear(first_movers,sk2),sk2) ).
cnf(u527,negated_conjecture,
greater(number_of_organizations(sk2,appear(first_movers,sk2)),zero) ).
cnf(u532,negated_conjecture,
subpopulation(efficient_producers,sk2,appear(first_movers,sk2)) ).
cnf(u537,negated_conjecture,
greater(cardinality_at_time(efficient_producers,appear(first_movers,sk2)),zero) ).
cnf(u542,negated_conjecture,
greater_or_equal(cardinality_at_time(efficient_producers,appear(first_movers,sk2)),zero) ).
cnf(u546,negated_conjecture,
( ~ greater(X0,cardinality_at_time(efficient_producers,appear(first_movers,sk2)))
| greater(X0,zero) ) ).
cnf(u550,negated_conjecture,
( ~ greater_or_equal(X0,cardinality_at_time(efficient_producers,appear(first_movers,sk2)))
| in_environment(X1,cardinality_at_time(efficient_producers,appear(first_movers,sk2)))
| ~ environment(X1)
| ~ in_environment(X1,zero)
| ~ in_environment(X1,X0) ) ).
cnf(u608,negated_conjecture,
~ greater(appear(first_movers,sk2),sk3) ).
cnf(u612,negated_conjecture,
zero = cardinality_at_time(an_organisation,start_time(sk2)) ).
cnf(u642,negated_conjecture,
~ in_environment(sk2,appear(efficient_producers,e)) ).
cnf(u654,negated_conjecture,
first_movers != sk1(sk3,sk2) ).
cnf(u659,negated_conjecture,
efficient_producers = sk1(sk3,sk2) ).
cnf(u713,negated_conjecture,
~ greater(start_time(sk2),sk3) ).
cnf(u765,negated_conjecture,
selection_favors(first_movers,first_movers,start_time(sk2)) ).
cnf(u779,negated_conjecture,
first_movers != an_organisation ).
cnf(u783,negated_conjecture,
an_organisation != efficient_producers ).
cnf(u787,negated_conjecture,
( ~ subpopulation(an_organisation,X0,start_time(sk2))
| ~ environment(X0) ) ).
cnf(u840,negated_conjecture,
greater(number_of_organizations(sk2,sk3),zero) ).
cnf(u845,negated_conjecture,
subpopulation(efficient_producers,sk2,sk3) ).
cnf(u855,negated_conjecture,
efficient_producers = sk1(appear(an_organisation,sk2),sk2) ).
cnf(u858,negated_conjecture,
first_movers != sk1(appear(an_organisation,sk2),sk2) ).
cnf(u902,negated_conjecture,
greater(number_of_organizations(sk2,appear(an_organisation,sk2)),zero) ).
cnf(u907,negated_conjecture,
subpopulation(efficient_producers,sk2,appear(an_organisation,sk2)) ).
cnf(u912,negated_conjecture,
greater(cardinality_at_time(efficient_producers,appear(an_organisation,sk2)),zero) ).
cnf(u917,negated_conjecture,
greater_or_equal(cardinality_at_time(efficient_producers,appear(an_organisation,sk2)),zero) ).
cnf(u921,negated_conjecture,
( ~ greater(X0,cardinality_at_time(efficient_producers,appear(an_organisation,sk2)))
| greater(X0,zero) ) ).
cnf(u925,negated_conjecture,
( ~ greater_or_equal(X0,cardinality_at_time(efficient_producers,appear(an_organisation,sk2)))
| in_environment(X1,cardinality_at_time(efficient_producers,appear(an_organisation,sk2)))
| ~ environment(X1)
| ~ in_environment(X1,zero)
| ~ in_environment(X1,X0) ) ).
cnf(u967,negated_conjecture,
selection_favors(efficient_producers,first_movers,start_time(sk2)) ).
cnf(u981,negated_conjecture,
selection_favors(an_organisation,first_movers,start_time(sk2)) ).
cnf(u1328,negated_conjecture,
~ in_environment(sk2,appear(efficient_producers,sk2)) ).
cnf(u1462,negated_conjecture,
selection_favors(first_movers,efficient_producers,start_time(sk2)) ).
cnf(u1467,negated_conjecture,
selection_favors(efficient_producers,efficient_producers,start_time(sk2)) ).
cnf(u1151,negated_conjecture,
( ~ in_environment(sk2,X0)
| ~ greater(sk3,X0)
| zero = cardinality_at_time(an_organisation,X0) ) ).
cnf(mp_number_mean_non_empty_25,axiom,
( subpopulation(sk1(X1,X0),X0,X1)
| ~ greater(number_of_organizations(X0,X1),zero)
| ~ environment(X0) ) ).
cnf(u404,negated_conjecture,
( ~ greater(X1,X0)
| ~ greater(X0,sk3)
| greater(X1,start_time(sk2)) ) ).
cnf(u1032,negated_conjecture,
greater(number_of_organizations(e,sk3),zero) ).
cnf(u792,hypothesis,
( greater(number_of_organizations(X0,appear(efficient_producers,e)),zero)
| appear(first_movers,X0) = appear(an_organisation,X0)
| ~ in_environment(X0,appear(efficient_producers,e))
| ~ environment(X0) ) ).
cnf(u879,negated_conjecture,
( ~ in_environment(X1,appear(an_organisation,sk2))
| ~ greater(appear(X0,X1),sk3)
| ~ environment(X1)
| zero = cardinality_at_time(X0,appear(an_organisation,sk2)) ) ).
cnf(u471,hypothesis,
( ~ greater(X1,appear(efficient_producers,e))
| ~ environment(X0)
| start_time(X0) = appear(first_movers,X0)
| greater(X1,start_time(X0)) ) ).
cnf(a1_42,hypothesis,
( ~ greater_or_equal(X1,appear(an_organisation,X0))
| ~ in_environment(X0,X1)
| ~ environment(X0)
| greater(number_of_organizations(X0,X1),zero) ) ).
cnf(u37,axiom,
( ~ greater(X0,number_of_organizations(e,appear(an_organisation,X1)))
| greater(X0,zero)
| ~ environment(X1) ) ).
cnf(u1306,negated_conjecture,
( ~ greater(X1,number_of_organizations(sk2,X0))
| ~ greater(X0,sk3)
| ~ in_environment(sk2,X0)
| greater(X1,zero) ) ).
cnf(u809,negated_conjecture,
( ~ greater(cardinality_at_time(X0,start_time(sk2)),zero)
| ~ subpopulation(efficient_producers,X1,start_time(sk2))
| ~ subpopulation(X0,X1,start_time(sk2))
| ~ environment(X1)
| selection_favors(X0,efficient_producers,start_time(sk2)) ) ).
cnf(u436,negated_conjecture,
greater_or_equal(appear(efficient_producers,e),start_time(sk2)) ).
cnf(u213,axiom,
( ~ greater(X1,appear(first_movers,X0))
| ~ environment(X0)
| appear(first_movers,X0) = appear(an_organisation,X0)
| greater(X1,appear(an_organisation,X0)) ) ).
cnf(u179,negated_conjecture,
greater_or_equal(appear(efficient_producers,e),sk3) ).
cnf(u1384,negated_conjecture,
( ~ in_environment(sk2,appear(first_movers,X0))
| ~ greater(start_time(X0),sk3)
| in_environment(sk2,start_time(X0))
| ~ environment(X0) ) ).
cnf(u1152,negated_conjecture,
( ~ greater_or_equal(X0,number_of_organizations(e,sk3))
| ~ in_environment(X1,zero)
| ~ in_environment(X1,X0)
| ~ environment(X1)
| in_environment(X1,number_of_organizations(e,sk3)) ) ).
cnf(mp_durations_are_time_intervals_30,axiom,
( ~ greater_or_equal(X3,X1)
| ~ in_environment(X0,X1)
| ~ in_environment(X0,X2)
| ~ greater_or_equal(X2,X3)
| ~ environment(X0)
| in_environment(X0,X3) ) ).
cnf(u25,hypothesis,
( ~ greater(cardinality_at_time(X1,X2),zero)
| ~ subpopulation(X1,X0,X2)
| ~ environment(X0)
| efficient_producers = X1
| first_movers = X1 ) ).
cnf(u478,hypothesis,
( greater_or_equal(appear(efficient_producers,e),appear(an_organisation,X0))
| ~ environment(X0)
| appear(first_movers,X0) = appear(an_organisation,X0) ) ).
cnf(mp_FM_not_precede_first_34,axiom,
( greater_or_equal(appear(first_movers,X0),appear(an_organisation,X0))
| ~ environment(X0) ) ).
cnf(u157,axiom,
( ~ greater(X1,appear(first_movers,X0))
| ~ environment(X0)
| start_time(X0) = appear(first_movers,X0)
| greater(X1,start_time(X0)) ) ).
cnf(u116,negated_conjecture,
( ~ greater_or_equal(X1,appear(efficient_producers,sk2))
| ~ in_environment(X0,X1)
| ~ in_environment(X0,sk3)
| ~ environment(X0)
| in_environment(X0,appear(efficient_producers,sk2)) ) ).
cnf(u160,axiom,
( ~ environment(X0)
| start_time(X0) = appear(first_movers,X0)
| zero = cardinality_at_time(first_movers,start_time(X0)) ) ).
cnf(u259,negated_conjecture,
in_environment(sk2,appear(first_movers,sk2)) ).
cnf(u111,hypothesis,
( ~ subpopulation(sk1(X0,X1),X2,X0)
| ~ environment(X2)
| efficient_producers = sk1(X0,X1)
| first_movers = sk1(X0,X1)
| ~ greater(number_of_organizations(X1,X0),zero)
| ~ environment(X1) ) ).
cnf(u123,hypothesis,
( ~ greater_or_equal(X2,appear(efficient_producers,e))
| ~ in_environment(X1,appear(first_movers,X0))
| ~ in_environment(X1,X2)
| ~ environment(X0)
| ~ environment(X1)
| in_environment(X1,appear(efficient_producers,e)) ) ).
cnf(u1198,negated_conjecture,
( ~ greater(appear(an_organisation,X0),sk3)
| appear(first_movers,X0) = appear(an_organisation,X0)
| ~ environment(X0) ) ).
cnf(u790,hypothesis,
( ~ greater_or_equal(X2,appear(efficient_producers,e))
| appear(first_movers,X0) = appear(an_organisation,X0)
| ~ in_environment(X1,appear(an_organisation,X0))
| ~ in_environment(X1,X2)
| ~ environment(X0)
| ~ environment(X1)
| in_environment(X1,appear(efficient_producers,e)) ) ).
cnf(u227,negated_conjecture,
( in_environment(X0,appear(first_movers,sk2))
| ~ in_environment(X0,start_time(sk2))
| ~ environment(X0)
| ~ in_environment(X0,sk3) ) ).
cnf(u290,hypothesis,
( ~ in_environment(X0,appear(an_organisation,X0))
| first_movers = sk1(appear(an_organisation,X0),X0)
| ~ environment(X0)
| efficient_producers = sk1(appear(an_organisation,X0),X0) ) ).
cnf(u758,negated_conjecture,
( ~ subpopulation(sk1(start_time(sk2),X1),X0,start_time(sk2))
| ~ subpopulation(first_movers,X0,start_time(sk2))
| ~ environment(X0)
| selection_favors(sk1(start_time(sk2),X1),first_movers,start_time(sk2))
| ~ greater(number_of_organizations(X1,start_time(sk2)),zero)
| ~ environment(X1) ) ).
cnf(u246,negated_conjecture,
( ~ in_environment(X0,appear(an_organisation,sk2))
| ~ in_environment(X0,sk3)
| ~ environment(X0)
| in_environment(X0,appear(first_movers,sk2)) ) ).
cnf(prove_t2_48,negated_conjecture,
greater(appear(efficient_producers,sk2),sk3) ).
cnf(u1154,negated_conjecture,
( greater(number_of_organizations(sk2,X0),zero)
| ~ in_environment(sk2,X0)
| ~ greater_or_equal(X0,sk3) ) ).
cnf(u1452,negated_conjecture,
( ~ subpopulation(sk1(start_time(sk2),X1),X0,start_time(sk2))
| ~ subpopulation(efficient_producers,X0,start_time(sk2))
| ~ environment(X0)
| selection_favors(sk1(start_time(sk2),X1),efficient_producers,start_time(sk2))
| ~ greater(number_of_organizations(X1,start_time(sk2)),zero)
| ~ environment(X1) ) ).
cnf(u1387,negated_conjecture,
( ~ in_environment(sk2,appear(first_movers,X0))
| ~ greater(appear(an_organisation,X0),sk3)
| in_environment(sk2,appear(an_organisation,X0))
| ~ environment(X0) ) ).
cnf(u32,negated_conjecture,
greater_or_equal(appear(efficient_producers,sk2),sk3) ).
cnf(u1027,negated_conjecture,
( ~ greater(X0,number_of_organizations(sk2,sk3))
| greater(X0,zero) ) ).
cnf(u1169,negated_conjecture,
( ~ greater_or_equal(X2,X0)
| ~ greater(X0,sk3)
| ~ in_environment(X1,X2)
| ~ in_environment(X1,sk3)
| ~ environment(X1)
| in_environment(X1,X0) ) ).
cnf(u254,negated_conjecture,
in_environment(sk2,appear(an_organisation,sk2)) ).
cnf(u435,negated_conjecture,
( ~ greater(X0,appear(efficient_producers,e))
| greater(X0,start_time(sk2)) ) ).
cnf(u99,hypothesis,
( greater(number_of_organizations(X0,appear(an_organisation,X0)),zero)
| ~ environment(X0)
| ~ in_environment(X0,appear(an_organisation,X0)) ) ).
cnf(u1174,negated_conjecture,
( ~ greater(X0,appear(efficient_producers,e))
| greater(X0,sk3) ) ).
cnf(u1200,negated_conjecture,
( ~ greater_or_equal(X1,appear(efficient_producers,e))
| ~ in_environment(X0,X1)
| ~ in_environment(X0,sk3)
| ~ environment(X0)
| in_environment(X0,appear(efficient_producers,e)) ) ).
cnf(u1246,negated_conjecture,
( ~ greater(appear(X0,sk2),sk3)
| zero = cardinality_at_time(X0,sk3) ) ).
cnf(u118,axiom,
( ~ greater_or_equal(X2,appear(first_movers,X1))
| ~ in_environment(X0,X2)
| ~ in_environment(X0,appear(an_organisation,X1))
| ~ environment(X0)
| in_environment(X0,appear(first_movers,X1))
| ~ environment(X1) ) ).
cnf(u734,negated_conjecture,
first_movers != efficient_producers ).
cnf(u1026,negated_conjecture,
( ~ greater_or_equal(X0,number_of_organizations(sk2,sk3))
| ~ in_environment(X1,zero)
| ~ in_environment(X1,X0)
| ~ environment(X1)
| in_environment(X1,number_of_organizations(sk2,sk3)) ) ).
cnf(u8,axiom,
( ~ greater(appear(X2,X0),X1)
| ~ in_environment(X0,X1)
| ~ environment(X0)
| zero = cardinality_at_time(X2,X1) ) ).
cnf(u36,hypothesis,
( ~ greater(X0,appear(efficient_producers,e))
| greater(X0,appear(first_movers,X1))
| ~ environment(X1) ) ).
cnf(u256,hypothesis,
( ~ greater(number_of_organizations(X0,X1),zero)
| sk1(X1,X0) = efficient_producers
| sk1(X1,X0) = first_movers
| ~ environment(X0) ) ).
cnf(u140,axiom,
( ~ greater_or_equal(X2,number_of_organizations(e,appear(an_organisation,X0)))
| ~ in_environment(X1,zero)
| ~ in_environment(X1,X2)
| ~ environment(X0)
| ~ environment(X1)
| in_environment(X1,number_of_organizations(e,appear(an_organisation,X0))) ) ).
cnf(u444,negated_conjecture,
( ~ greater_or_equal(X1,appear(efficient_producers,e))
| ~ in_environment(X0,X1)
| ~ in_environment(X0,start_time(sk2))
| ~ environment(X0)
| in_environment(X0,appear(efficient_producers,e)) ) ).
cnf(u31,axiom,
greater_or_equal(X1,X1) ).
cnf(u1217,negated_conjecture,
( greater_or_equal(number_of_organizations(sk2,X0),zero)
| ~ greater_or_equal(X0,sk3)
| ~ in_environment(sk2,X0) ) ).
cnf(u511,negated_conjecture,
( ~ greater_or_equal(X1,appear(efficient_producers,e))
| ~ in_environment(X0,X1)
| ~ in_environment(X0,appear(first_movers,sk2))
| ~ environment(X0)
| in_environment(X0,appear(efficient_producers,e)) ) ).
cnf(u34,axiom,
( greater_or_equal(number_of_organizations(e,appear(an_organisation,X0)),zero)
| ~ environment(X0) ) ).
cnf(u1199,negated_conjecture,
( ~ greater(start_time(X0),sk3)
| start_time(X0) = appear(first_movers,X0)
| ~ environment(X0) ) ).
cnf(u1253,negated_conjecture,
zero != cardinality_at_time(first_movers,sk3) ).
cnf(u1479,negated_conjecture,
( selection_favors(sk1(start_time(sk2),X0),efficient_producers,start_time(sk2))
| ~ environment(X0)
| ~ subpopulation(efficient_producers,X0,start_time(sk2))
| ~ greater(number_of_organizations(X0,start_time(sk2)),zero) ) ).
cnf(u121,negated_conjecture,
( ~ greater(cardinality_at_time(X0,sk3),zero)
| ~ subpopulation(efficient_producers,X1,sk3)
| ~ subpopulation(X0,X1,sk3)
| ~ environment(X1)
| selection_favors(X0,efficient_producers,sk3) ) ).
cnf(u1307,negated_conjecture,
( greater_or_equal(number_of_organizations(sk2,X0),zero)
| ~ greater(X0,sk3)
| ~ in_environment(sk2,X0) ) ).
cnf(mp_no_FM_before_opening_32,axiom,
( greater_or_equal(appear(first_movers,X0),start_time(X0))
| ~ environment(X0) ) ).
cnf(mp_greater_or_equal_39,axiom,
( ~ greater_or_equal(X0,X1)
| greater(X0,X1)
| X0 = X1 ) ).
cnf(u151,hypothesis,
( greater_or_equal(number_of_organizations(X0,appear(first_movers,X0)),zero)
| ~ in_environment(X0,appear(first_movers,X0))
| ~ environment(X0) ) ).
cnf(u770,hypothesis,
( ~ greater_or_equal(X2,appear(efficient_producers,e))
| start_time(X0) = appear(first_movers,X0)
| ~ in_environment(X1,start_time(X0))
| ~ in_environment(X1,X2)
| ~ environment(X0)
| ~ environment(X1)
| in_environment(X1,appear(efficient_producers,e)) ) ).
cnf(u110,negated_conjecture,
zero = cardinality_at_time(efficient_producers,sk3) ).
cnf(u154,negated_conjecture,
( selection_favors(sk1(sk3,X0),efficient_producers,sk3)
| ~ environment(X0)
| ~ subpopulation(efficient_producers,X0,sk3)
| ~ greater(number_of_organizations(X0,sk3),zero) ) ).
cnf(u570,negated_conjecture,
( greater(appear(first_movers,X0),start_time(sk2))
| ~ greater(start_time(X0),sk3)
| start_time(X0) = appear(first_movers,X0)
| ~ environment(X0) ) ).
cnf(u1017,negated_conjecture,
( ~ in_environment(sk2,X0)
| ~ greater(sk3,X0)
| zero = cardinality_at_time(first_movers,X0) ) ).
cnf(u97,axiom,
( ~ greater(X2,cardinality_at_time(sk1(X1,X0),X1))
| ~ environment(X0)
| ~ greater(number_of_organizations(X0,X1),zero)
| greater(X2,zero) ) ).
cnf(u125,negated_conjecture,
( ~ subpopulation(sk1(sk3,X1),X0,sk3)
| ~ subpopulation(efficient_producers,X0,sk3)
| ~ environment(X0)
| selection_favors(sk1(sk3,X1),efficient_producers,sk3)
| ~ greater(number_of_organizations(X1,sk3),zero)
| ~ environment(X1) ) ).
cnf(u1426,hypothesis,
( ~ in_environment(X0,appear(efficient_producers,e))
| appear(first_movers,X0) = appear(an_organisation,X0)
| ~ environment(X0)
| efficient_producers = sk1(appear(efficient_producers,e),X0)
| first_movers = sk1(appear(efficient_producers,e),X0) ) ).
cnf(u1033,negated_conjecture,
greater_or_equal(number_of_organizations(e,sk3),zero) ).
cnf(a3_43,hypothesis,
( greater(appear(efficient_producers,e),appear(first_movers,X0))
| ~ environment(X0) ) ).
cnf(u463,negated_conjecture,
( ~ greater(X0,appear(efficient_producers,e))
| greater(X0,appear(first_movers,sk2)) ) ).
cnf(prove_t2_45,negated_conjecture,
environment(sk2) ).
cnf(u877,negated_conjecture,
( ~ greater(X1,X0)
| ~ greater(X0,sk3)
| greater(X1,appear(an_organisation,sk2)) ) ).
cnf(u262,hypothesis,
( ~ greater_or_equal(X2,number_of_organizations(X0,appear(an_organisation,X0)))
| ~ environment(X0)
| ~ in_environment(X1,zero)
| ~ in_environment(X1,X2)
| ~ in_environment(X0,appear(an_organisation,X0))
| ~ environment(X1)
| in_environment(X1,number_of_organizations(X0,appear(an_organisation,X0))) ) ).
cnf(u41,axiom,
( greater(appear(first_movers,X0),start_time(X0))
| start_time(X0) = appear(first_movers,X0)
| ~ environment(X0) ) ).
cnf(u101,hypothesis,
( greater(number_of_organizations(X0,appear(first_movers,X0)),zero)
| ~ environment(X0)
| ~ in_environment(X0,appear(first_movers,X0)) ) ).
cnf(u145,hypothesis,
( greater_or_equal(number_of_organizations(X0,appear(an_organisation,X0)),zero)
| ~ in_environment(X0,appear(an_organisation,X0))
| ~ environment(X0) ) ).
cnf(u1370,negated_conjecture,
( ~ greater_or_equal(X1,X0)
| ~ in_environment(sk2,X1)
| ~ greater(X0,sk3)
| in_environment(sk2,X0) ) ).
cnf(mp_number_mean_non_empty_26,axiom,
( greater(cardinality_at_time(sk1(X1,X0),X1),zero)
| ~ greater(number_of_organizations(X0,X1),zero)
| ~ environment(X0) ) ).
cnf(u104,negated_conjecture,
greater_or_equal(appear(efficient_producers,e),appear(first_movers,sk2)) ).
cnf(u280,negated_conjecture,
( ~ greater(cardinality_at_time(X0,start_time(sk2)),zero)
| ~ subpopulation(first_movers,X1,start_time(sk2))
| ~ subpopulation(X0,X1,start_time(sk2))
| ~ environment(X1)
| selection_favors(X0,first_movers,start_time(sk2)) ) ).
cnf(u1417,negated_conjecture,
( selection_favors(sk1(start_time(sk2),X0),first_movers,start_time(sk2))
| ~ environment(X0)
| ~ subpopulation(first_movers,X0,start_time(sk2))
| ~ greater(number_of_organizations(X0,start_time(sk2)),zero) ) ).
cnf(mp_opening_time_in_duration_31,axiom,
( in_environment(X0,start_time(X0))
| ~ environment(X0) ) ).
cnf(u407,negated_conjecture,
( ~ greater(appear(X0,X1),sk3)
| ~ in_environment(X1,start_time(sk2))
| ~ environment(X1)
| zero = cardinality_at_time(X0,start_time(sk2)) ) ).
cnf(u885,negated_conjecture,
greater_or_equal(number_of_organizations(sk2,sk3),zero) ).
cnf(u2,axiom,
( zero != cardinality_at_time(X3,X2)
| ~ subpopulation(X1,X0,X2)
| ~ subpopulation(X3,X0,X2)
| ~ greater(cardinality_at_time(X1,X2),zero)
| ~ environment(X0)
| selection_favors(X1,X3,X2) ) ).
cnf(prove_t2_49,negated_conjecture,
~ selection_favors(first_movers,efficient_producers,sk3) ).
cnf(u1216,negated_conjecture,
( ~ greater(X1,number_of_organizations(sk2,X0))
| ~ greater_or_equal(X0,sk3)
| ~ in_environment(sk2,X0)
| greater(X1,zero) ) ).
cnf(mp_subpopulations_37,axiom,
( subpopulation(efficient_producers,X0,X1)
| ~ in_environment(X0,X1)
| ~ environment(X0) ) ).
cnf(u335,negated_conjecture,
( ~ in_environment(X0,start_time(sk2))
| ~ in_environment(X0,X1)
| ~ greater_or_equal(X1,sk3)
| ~ environment(X0)
| in_environment(X0,sk3) ) ).
cnf(u1170,negated_conjecture,
( greater(number_of_organizations(sk2,X0),zero)
| ~ in_environment(sk2,X0)
| ~ greater(X0,sk3) ) ).
cnf(u1350,negated_conjecture,
( ~ in_environment(X1,appear(first_movers,X0))
| ~ greater(appear(an_organisation,X0),sk3)
| ~ in_environment(X1,sk3)
| ~ environment(X1)
| in_environment(X1,appear(an_organisation,X0))
| ~ environment(X0) ) ).
cnf(u388,hypothesis,
( greater(appear(efficient_producers,e),appear(an_organisation,X0))
| appear(first_movers,X0) = appear(an_organisation,X0)
| ~ environment(X0) ) ).
cnf(u1423,hypothesis,
( ~ greater(X1,number_of_organizations(X0,appear(efficient_producers,e)))
| ~ in_environment(X0,appear(efficient_producers,e))
| ~ environment(X0)
| appear(first_movers,X0) = appear(an_organisation,X0)
| greater(X1,zero) ) ).
cnf(u1424,hypothesis,
( greater_or_equal(number_of_organizations(X0,appear(efficient_producers,e)),zero)
| ~ in_environment(X0,appear(efficient_producers,e))
| ~ environment(X0)
| appear(first_movers,X0) = appear(an_organisation,X0) ) ).
cnf(u6,axiom,
( zero != cardinality_at_time(X0,t)
| ~ greater(cardinality_at_time(X0,X1),zero) ) ).
cnf(u178,negated_conjecture,
greater(appear(efficient_producers,e),sk3) ).
cnf(u297,hypothesis,
( greater(appear(efficient_producers,e),start_time(X0))
| start_time(X0) = appear(first_movers,X0)
| ~ environment(X0) ) ).
cnf(u33,hypothesis,
( greater_or_equal(appear(efficient_producers,e),appear(first_movers,X0))
| ~ environment(X0) ) ).
cnf(u473,negated_conjecture,
( ~ in_environment(X1,start_time(sk2))
| ~ greater(X0,sk3)
| ~ in_environment(X1,X2)
| ~ greater_or_equal(X2,X0)
| ~ environment(X1)
| in_environment(X1,X0) ) ).
cnf(u1218,negated_conjecture,
( ~ greater_or_equal(X0,sk3)
| ~ in_environment(sk2,X0)
| efficient_producers = sk1(X0,sk2)
| first_movers = sk1(X0,sk2) ) ).
cnf(u571,negated_conjecture,
( greater(appear(first_movers,X0),start_time(sk2))
| ~ greater(appear(an_organisation,X0),sk3)
| appear(first_movers,X0) = appear(an_organisation,X0)
| ~ environment(X0) ) ).
cnf(u666,negated_conjecture,
zero = cardinality_at_time(efficient_producers,start_time(sk2)) ).
cnf(u1311,negated_conjecture,
( ~ greater_or_equal(X2,number_of_organizations(sk2,X0))
| ~ in_environment(sk2,X0)
| ~ in_environment(X1,zero)
| ~ in_environment(X1,X2)
| ~ greater(X0,sk3)
| ~ environment(X1)
| in_environment(X1,number_of_organizations(sk2,X0)) ) ).
cnf(u226,hypothesis,
( ~ in_environment(X0,appear(efficient_producers,e))
| ~ in_environment(X0,start_time(X1))
| ~ environment(X0)
| in_environment(X0,appear(first_movers,X1))
| ~ environment(X1) ) ).
cnf(mp_positive_and_sustains_29,axiom,
( ~ greater(number_of_organizations(X0,X1),zero)
| ~ environment(X0)
| in_environment(X0,X1) ) ).
cnf(u405,negated_conjecture,
( greater_or_equal(X0,start_time(sk2))
| ~ greater(X0,sk3) ) ).
cnf(u477,hypothesis,
( ~ greater(X1,appear(efficient_producers,e))
| ~ environment(X0)
| appear(first_movers,X0) = appear(an_organisation,X0)
| greater(X1,appear(an_organisation,X0)) ) ).
cnf(prove_t2_47,negated_conjecture,
greater_or_equal(sk3,appear(first_movers,sk2)) ).
cnf(u144,hypothesis,
( ~ greater(X1,number_of_organizations(X0,appear(an_organisation,X0)))
| ~ in_environment(X0,appear(an_organisation,X0))
| ~ environment(X0)
| greater(X1,zero) ) ).
cnf(u35,negated_conjecture,
( ~ greater(X0,appear(efficient_producers,sk2))
| greater(X0,sk3) ) ).
cnf(u1020,negated_conjecture,
( ~ in_environment(X1,appear(an_organisation,sk2))
| ~ in_environment(X1,X0)
| ~ greater_or_equal(X0,sk3)
| ~ environment(X1)
| in_environment(X1,sk3) ) ).
cnf(u98,axiom,
( greater_or_equal(cardinality_at_time(sk1(X1,X0),X1),zero)
| ~ environment(X0)
| ~ greater(number_of_organizations(X0,X1),zero) ) ).
cnf(u1031,negated_conjecture,
sk3 = appear(an_organisation,sk2) ).
cnf(u334,negated_conjecture,
greater_or_equal(sk3,start_time(sk2)) ).
cnf(u289,hypothesis,
( ~ in_environment(X0,appear(first_movers,X0))
| first_movers = sk1(appear(first_movers,X0),X0)
| ~ environment(X0)
| efficient_producers = sk1(appear(first_movers,X0),X0) ) ).
cnf(u113,negated_conjecture,
( ~ in_environment(X0,appear(first_movers,sk2))
| ~ in_environment(X0,X1)
| ~ greater_or_equal(X1,sk3)
| ~ environment(X0)
| in_environment(X0,sk3) ) ).
cnf(mp_FM_means_organisations_33,axiom,
( ~ in_environment(X0,appear(first_movers,X0))
| ~ environment(X0)
| in_environment(X0,appear(an_organisation,X0)) ) ).
cnf(u245,hypothesis,
( ~ in_environment(X0,appear(efficient_producers,e))
| ~ in_environment(X0,appear(an_organisation,X1))
| ~ environment(X0)
| in_environment(X0,appear(first_movers,X1))
| ~ environment(X1) ) ).
cnf(mp_subpopulations_36,axiom,
( subpopulation(first_movers,X0,X1)
| ~ in_environment(X0,X1)
| ~ environment(X0) ) ).
cnf(u878,negated_conjecture,
( greater_or_equal(X0,appear(an_organisation,sk2))
| ~ greater(X0,sk3) ) ).
cnf(u1475,hypothesis,
( ~ greater_or_equal(X2,number_of_organizations(X0,appear(efficient_producers,e)))
| ~ environment(X0)
| appear(first_movers,X0) = appear(an_organisation,X0)
| ~ in_environment(X1,zero)
| ~ in_environment(X1,X2)
| ~ in_environment(X0,appear(efficient_producers,e))
| ~ environment(X1)
| in_environment(X1,number_of_organizations(X0,appear(efficient_producers,e))) ) ).
cnf(u1153,negated_conjecture,
( ~ greater(X0,number_of_organizations(e,sk3))
| greater(X0,zero) ) ).
cnf(u42,axiom,
( greater(appear(first_movers,X0),appear(an_organisation,X0))
| appear(first_movers,X0) = appear(an_organisation,X0)
| ~ environment(X0) ) ).
cnf(u215,axiom,
( ~ in_environment(X0,appear(an_organisation,X0))
| ~ environment(X0)
| appear(first_movers,X0) = appear(an_organisation,X0)
| zero = cardinality_at_time(first_movers,appear(an_organisation,X0)) ) ).
cnf(u117,axiom,
( ~ greater_or_equal(X2,appear(first_movers,X1))
| ~ in_environment(X0,X2)
| ~ in_environment(X0,start_time(X1))
| ~ environment(X0)
| in_environment(X0,appear(first_movers,X1))
| ~ environment(X1) ) ).
cnf(u1308,negated_conjecture,
( ~ in_environment(sk2,X0)
| ~ greater(X0,sk3)
| efficient_producers = sk1(X0,sk2)
| first_movers = sk1(X0,sk2) ) ).
cnf(u161,axiom,
( ~ greater_or_equal(X3,cardinality_at_time(sk1(X1,X0),X1))
| ~ greater(number_of_organizations(X0,X1),zero)
| ~ in_environment(X2,zero)
| ~ in_environment(X2,X3)
| ~ environment(X0)
| ~ environment(X2)
| in_environment(X2,cardinality_at_time(sk1(X1,X0),X1)) ) ).
cnf(u1347,negated_conjecture,
( ~ in_environment(X1,appear(first_movers,X0))
| ~ greater(start_time(X0),sk3)
| ~ in_environment(X1,sk3)
| ~ environment(X1)
| in_environment(X1,start_time(X0))
| ~ environment(X0) ) ).
cnf(mp_greater_or_equal_40,axiom,
( ~ greater(X0,X1)
| greater_or_equal(X0,X1) ) ).
cnf(u1309,negated_conjecture,
( ~ greater_or_equal(X2,number_of_organizations(sk2,X0))
| ~ in_environment(sk2,X0)
| ~ in_environment(X1,zero)
| ~ in_environment(X1,X2)
| ~ greater_or_equal(X0,sk3)
| ~ environment(X1)
| in_environment(X1,number_of_organizations(sk2,X0)) ) ).
cnf(mp_positive_number_when_appear_35,axiom,
( greater(number_of_organizations(e,appear(an_organisation,X0)),zero)
| ~ environment(X0) ) ).
cnf(prove_t2_46,negated_conjecture,
in_environment(sk2,sk3) ).
cnf(u472,hypothesis,
( greater_or_equal(appear(efficient_producers,e),start_time(X0))
| ~ environment(X0)
| start_time(X0) = appear(first_movers,X0) ) ).
cnf(u775,negated_conjecture,
( ~ greater(cardinality_at_time(X0,start_time(sk2)),zero)
| ~ subpopulation(an_organisation,X1,start_time(sk2))
| ~ subpopulation(X0,X1,start_time(sk2))
| ~ environment(X1)
| selection_favors(X0,an_organisation,start_time(sk2)) ) ).
cnf(mp_greater_transitivity_38,axiom,
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ) ).
cnf(u266,hypothesis,
( ~ greater_or_equal(X2,number_of_organizations(X0,appear(first_movers,X0)))
| ~ environment(X0)
| ~ in_environment(X1,zero)
| ~ in_environment(X1,X2)
| ~ in_environment(X0,appear(first_movers,X0))
| ~ environment(X1)
| in_environment(X1,number_of_organizations(X0,appear(first_movers,X0))) ) ).
cnf(u150,hypothesis,
( ~ greater(X1,number_of_organizations(X0,appear(first_movers,X0)))
| ~ in_environment(X0,appear(first_movers,X0))
| ~ environment(X0)
| greater(X1,zero) ) ).
cnf(u194,negated_conjecture,
greater_or_equal(sk3,appear(an_organisation,sk2)) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT033-2 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n001.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 17:26:31 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.71/1.31 % (3822566)Input is clausal, will run a generic CNF schedule.
% 2.71/1.31 % (3822575)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2488813799:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.71/1.31 % (3822573)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1689950703:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.71/1.31 % (3822572)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=410093647:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.71/1.31 % (3822571)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2050876449:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.71/1.31 % (3822574)lrs+10_1_sil=8000:sp=occurrence:random_seed=2709400710:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.71/1.31 % (3822575)Instruction limit reached!
% 2.71/1.31 % (3822575)------------------------------
% 2.71/1.31 % (3822575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.71/1.31 % (3822575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.31 % (3822575)CaDiCaL version: 2.1.3
% 2.71/1.31 % (3822575)Termination reason: Instruction limit
% 2.71/1.31 % (3822575)Termination phase: Saturation
% 2.71/1.31 % (3822575)Time elapsed: 0.037 s
% 2.71/1.31 % (3822575)Peak memory usage: 88 MB
% 2.71/1.31 % (3822575)Instructions burned: 117 (million)
% 2.71/1.31 % (3822576)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1436197397:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.71/1.31 % (3822577)dis-21_1_sil=8000:lcm=predicate:random_seed=1286297660:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 2.71/1.31 % (3822574)First to succeed.
% 2.71/1.31 % (3822574)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3822566"
% 2.71/1.31 % (3822577)Instruction limit reached!
% 2.71/1.31 % (3822577)------------------------------
% 2.71/1.31 % (3822577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.71/1.31 % (3822577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.31 % (3822577)CaDiCaL version: 2.1.3
% 2.71/1.31 % (3822577)Termination reason: Instruction limit
% 2.71/1.31 % (3822577)Termination phase: Saturation
% 2.71/1.31 % (3822577)Time elapsed: 0.067 s
% 2.71/1.31 % (3822577)Peak memory usage: 88 MB
% 2.71/1.31 % (3822577)Instructions burned: 117 (million)
% 2.71/1.31 % (3822576)Instruction limit reached!
% 2.71/1.31 % (3822576)------------------------------
% 2.71/1.31 % (3822576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.71/1.31 % (3822576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.31 % (3822576)CaDiCaL version: 2.1.3
% 2.71/1.31 % (3822576)Termination reason: Instruction limit
% 2.71/1.31 % (3822576)Termination phase: Saturation
% 2.71/1.31 % (3822576)Time elapsed: 0.087 s
% 2.71/1.31 % (3822576)Peak memory usage: 89 MB
% 2.71/1.31 % (3822576)Instructions burned: 182 (million)
% 2.71/1.31 % (3822583)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2950904323:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 2.71/1.32 % (3822583)Instruction limit reached!
% 2.71/1.32 % (3822583)------------------------------
% 2.71/1.32 % (3822583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.71/1.32 % (3822583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.32 % (3822583)CaDiCaL version: 2.1.3
% 2.71/1.32 % (3822583)Termination reason: Instruction limit
% 2.71/1.32 % (3822583)Termination phase: Saturation
% 2.71/1.32 % (3822583)Time elapsed: 0.052 s
% 2.71/1.32 % (3822583)Peak memory usage: 89 MB
% 2.71/1.32 % (3822583)Instructions burned: 146 (million)
% 2.71/1.32 % (3822586)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2650656200:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 2.71/1.32 % (3822586)Refutation not found, incomplete strategy
% 2.71/1.32 % (3822586)------------------------------
% 2.71/1.32 % (3822586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.71/1.32 % (3822586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.32 % (3822586)CaDiCaL version: 2.1.3
% 2.71/1.32 % (3822586)Termination reason: Refutation not found, incomplete strategy
% 2.71/1.32 % (3822586)Time elapsed: 0.007 s
% 2.71/1.32 % (3822586)Peak memory usage: 88 MB
% 2.71/1.32 % (3822586)Instructions burned: 9 (million)
% 2.71/1.32 % (3822587)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3119999324:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 2.71/1.32 % SZS status Satisfiable for theBenchmark
% 2.71/1.32 % SZS output start Saturation.
% See solution above
% 3.80/1.42 % SZS output start Definitions and Model Updates.
% 3.80/1.42 % SZS output end Definitions and Model Updates.
% 3.80/1.42 % (3822574)------------------------------
% 3.80/1.42 % (3822574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.80/1.42 % (3822574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.80/1.42 % (3822574)CaDiCaL version: 2.1.3
% 3.80/1.42 % (3822574)Termination reason: Satisfiable
% 3.80/1.42 % (3822574)Time elapsed: 0.038 s
% 3.80/1.42 % (3822574)Peak memory usage: 89 MB
% 3.80/1.42 % (3822574)Instructions burned: 49 (million)
% 3.80/1.42 % (3822574)------------------------------
% 3.80/1.42 % (3822574)------------------------------
% 3.80/1.42 % (3822566)Success in time 0.461 s
% 3.80/1.42 % Vampire exiting
%------------------------------------------------------------------------------