%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : MGT038-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:09 PM UTC 2026
% Result : Satisfiable 4.70s 1.72s
% Output : Saturation 6.62s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u70,negated_conjecture,
true = sF11 ).
cnf(u75,negated_conjecture,
true = sF10 ).
cnf(u80,axiom,
finite_set(first_movers) = true ).
cnf(u86,axiom,
cardinality_at_time(s,t2) = sF3 ).
cnf(u92,axiom,
appear(efficient_producers,e) = sF6 ).
cnf(u98,axiom,
environment(sk3) = sF10 ).
cnf(u103,axiom,
stable(sk3) = sF11 ).
cnf(u108,axiom,
cardinality_at_time(first_movers,to) = sF12 ).
cnf(u114,axiom,
tuple(zero,true,true) = sF17 ).
cnf(u119,axiom,
sF14 = sF7(sk3) ).
cnf(u126,negated_conjecture,
finite_set(first_movers) = sF11 ).
cnf(u131,negated_conjecture,
sF17 = tuple(zero,sF11,sF11) ).
cnf(u138,negated_conjecture,
sF10 = sF11 ).
cnf(u144,negated_conjecture,
sF17 = tuple(zero,sF10,sF10) ).
cnf(u156,negated_conjecture,
sF10 = sF8(sk3) ).
cnf(u208,negated_conjecture,
sF10 = sF15(sF6) ).
cnf(u217,negated_conjecture,
sF16(sF6) = tuple(sF12,sF13(sF6),sF10) ).
cnf(u243,negated_conjecture,
sF10 = contracts_from(sk2(sk3),first_movers) ).
cnf(u265,negated_conjecture,
zero = sF3 ).
cnf(u271,negated_conjecture,
sF10 = sF0(sk2(sk3),first_movers) ).
cnf(u290,negated_conjecture,
sF17 = tuple(sF3,sF10,sF10) ).
cnf(u371,negated_conjecture,
sF10 = sF13(sF14) ).
cnf(u378,negated_conjecture,
sF16(sF14) = tuple(sF12,sF10,sF15(sF14)) ).
cnf(u457,negated_conjecture,
sF10 = ifeq(greater(sF6,sF6),sF10,sF10,sF10) ).
cnf(u474,negated_conjecture,
sF10 = ifeq(environment(e),sF10,ifeq(stable(e),sF10,greater(sk2(e),sF6),sF10),sF10) ).
cnf(u485,negated_conjecture,
sF10 = greater(sk2(sk3),appear(efficient_producers,sk3)) ).
cnf(u504,negated_conjecture,
sF10 = ifeq(sF15(appear(efficient_producers,sk3)),sF10,sF15(sk2(sk3)),sF10) ).
cnf(u524,negated_conjecture,
sF10 = ifeq(greater(sF14,appear(efficient_producers,sk3)),sF10,ifeq(sF15(sk2(sk3)),sF10,sF10,sF10),sF10) ).
cnf(u540,negated_conjecture,
sF10 = ifeq(sF15(sF14),sF10,sF10,sF10) ).
cnf(u669,negated_conjecture,
sF10 = ifeq(sF13(appear(efficient_producers,sk3)),sF10,sF13(sk2(sk3)),sF10) ).
cnf(u680,negated_conjecture,
sF10 = sF13(sF6) ).
cnf(u693,negated_conjecture,
sF16(sF6) = tuple(sF12,sF10,sF10) ).
cnf(u708,negated_conjecture,
sF10 = ifeq(greater(sF14,sF6),sF10,sF10,sF10) ).
cnf(u926,negated_conjecture,
sF10 = ifeq(greater(sk2(sk3),sk2(sk3)),sF10,sF10,sF10) ).
cnf(u935,negated_conjecture,
sF10 = ifeq(greater(appear(efficient_producers,sk3),appear(efficient_producers,sk3)),sF10,sF10,sF10) ).
cnf(u999,negated_conjecture,
sF10 = ifeq(sF15(sk2(sk3)),sF10,sF15(sk1(sk2(sk3),first_movers)),sF10) ).
cnf(u1005,negated_conjecture,
sF10 = greater(sk1(sk2(sk3),first_movers),appear(efficient_producers,sk3)) ).
cnf(u1031,negated_conjecture,
sF10 = ifeq(greater(sF14,appear(efficient_producers,sk3)),sF10,ifeq(sF15(sk1(sk2(sk3),first_movers)),sF10,sF10,sF10),sF10) ).
cnf(u1048,negated_conjecture,
sF10 = ifeq(sF13(appear(efficient_producers,sk3)),sF10,sF13(sk1(sk2(sk3),first_movers)),sF10) ).
cnf(u1053,negated_conjecture,
sF10 = ifeq(sF15(appear(efficient_producers,sk3)),sF10,sF15(sk1(sk2(sk3),first_movers)),sF10) ).
cnf(u1068,negated_conjecture,
sF10 = ifeq(greater(appear(efficient_producers,sk3),sk2(sk3)),sF10,sF10,sF10) ).
cnf(u1109,negated_conjecture,
sF10 = ifeq(sF13(sk2(sk3)),sF10,sF13(sk1(sk2(sk3),first_movers)),sF10) ).
cnf(u1144,negated_conjecture,
sF10 = ifeq(greater(sk2(sk3),sk1(sk2(sk3),first_movers)),sF10,sF10,sF10) ).
cnf(u1149,negated_conjecture,
sF10 = ifeq(greater(sk1(sk2(sk3),first_movers),sk1(sk2(sk3),first_movers)),sF10,sF10,sF10) ).
cnf(u1181,negated_conjecture,
sF10 = ifeq(greater(sF14,sk2(sk3)),sF10,ifeq(sF15(sk1(sk2(sk3),first_movers)),sF10,sF10,sF10),sF10) ).
cnf(u438,negated_conjecture,
sF10 = ifeq(sF15(X1),sF10,ifeq(greater(X0,X1),sF10,sF15(X0),sF10),sF10) ).
cnf(u219,negated_conjecture,
sF4(X0,X1) = ifeq2(contracts_from(X0,X1),sF10,sF3,zero) ).
cnf(u429,negated_conjecture,
sF10 = ifeq(greater(X2,X0),sF10,ifeq(greater(sk1(X0,X1),X2),sF10,sF0(X0,X1),sF10),sF10) ).
cnf(u47,negated_conjecture,
true = sF9(X0) ).
cnf(u451,negated_conjecture,
sF10 = ifeq(greater(sk1(sF14,X0),sF6),sF10,sF0(sF14,X0),sF10) ).
cnf(u435,negated_conjecture,
sF10 = ifeq(sF0(X0,X1),sF10,ifeq(greater(X2,sk1(X0,X1)),sF10,greater(X2,X0),sF10),sF10) ).
cnf(u629,negated_conjecture,
sF10 = ifeq(sF0(X0,X1),sF10,ifeq(in_environment(X2,X0),sF10,ifeq(environment(X2),sF10,ifeq(stable(X2),sF10,in_environment(X2,sk1(X0,X1)),sF10),sF10),sF10),sF10) ).
cnf(u657,negated_conjecture,
sF10 = ifeq(sF0(X0,X1),sF10,ifeq(sF13(X0),sF10,sF13(sk1(X0,X1)),sF10),sF10) ).
cnf(u631,negated_conjecture,
sF10 = ifeq(greater(sF7(X0),X1),sF10,ifeq(in_environment(X0,X1),sF10,sF10,sF10),sF10) ).
cnf(u1017,negated_conjecture,
sF10 = ifeq(greater(X0,appear(efficient_producers,sk3)),sF10,ifeq(greater(sk1(sk2(sk3),first_movers),X0),sF10,sF10,sF10),sF10) ).
cnf(u462,negated_conjecture,
sF10 = ifeq(environment(X0),sF10,ifeq(stable(X0),sF10,greater(sk2(X0),appear(efficient_producers,X0)),sF10),sF10) ).
cnf(u673,negated_conjecture,
sF10 = ifeq(sF0(sF14,X0),sF10,sF13(sk1(sF14,X0)),sF10) ).
cnf(u436,negated_conjecture,
sF10 = ifeq(sF8(X0),sF10,ifeq(greater(X1,sF6),sF10,greater(X1,sF7(X0)),sF10),sF10) ).
cnf(u446,negated_conjecture,
sF10 = ifeq(sF15(X1),sF10,ifeq(greater(sk1(sF14,X0),X1),sF10,sF0(sF14,X0),sF10),sF10) ).
cnf(u227,negated_conjecture,
sF10 = ifeq(environment(X0),sF10,ifeq(stable(X0),sF10,contracts_from(sk2(X0),first_movers),sF10),sF10) ).
cnf(u449,negated_conjecture,
sF10 = ifeq(sF0(sF6,X0),sF10,sF15(sk1(sF6,X0)),sF10) ).
cnf(u1036,negated_conjecture,
sF10 = ifeq(greater(X0,sk1(sk2(sk3),first_movers)),sF10,greater(X0,appear(efficient_producers,sk3)),sF10) ).
cnf(u57,axiom,
in_environment(sk3,X0) = sF13(X0) ).
cnf(u442,negated_conjecture,
sF10 = ifeq(sF15(sF14),sF10,ifeq(sF15(X0),sF10,sF15(X0),sF10),sF10) ).
cnf(u1035,negated_conjecture,
sF10 = ifeq(greater(appear(efficient_producers,sk3),X0),sF10,greater(sk1(sk2(sk3),first_movers),X0),sF10) ).
cnf(u876,negated_conjecture,
sF10 = ifeq(in_environment(X0,sk2(sk3)),sF10,ifeq(environment(X0),sF10,ifeq(stable(X0),sF10,in_environment(X0,sk1(sk2(sk3),first_movers)),sF10),sF10),sF10) ).
cnf(u752,negated_conjecture,
sF10 = ifeq(sF0(appear(efficient_producers,sk3),X0),sF10,ifeq(greater(sk2(sk3),sk1(appear(efficient_producers,sk3),X0)),sF10,sF10,sF10),sF10) ).
cnf(u1072,negated_conjecture,
sF10 = ifeq(sF0(sF14,X0),sF10,ifeq(sF0(sk1(sF14,X0),X1),sF10,sF15(sk1(sk1(sF14,X0),X1)),sF10),sF10) ).
cnf(u444,negated_conjecture,
sF10 = ifeq(sF15(X0),sF10,ifeq(sF0(X0,X1),sF10,sF15(sk1(X0,X1)),sF10),sF10) ).
cnf(u901,negated_conjecture,
sF10 = ifeq(sF0(sF14,X0),sF10,ifeq(greater(sF6,sk1(sF14,X0)),sF10,sF10,sF10),sF10) ).
cnf(u1021,negated_conjecture,
sF10 = ifeq(sF0(appear(efficient_producers,sk3),X0),sF10,ifeq(greater(sk1(sk2(sk3),first_movers),sk1(appear(efficient_producers,sk3),X0)),sF10,sF10,sF10),sF10) ).
cnf(u661,negated_conjecture,
sF10 = ifeq(greater(sF14,X0),sF10,ifeq(sF13(X0),sF10,sF10,sF10),sF10) ).
cnf(u500,negated_conjecture,
sF10 = ifeq(greater(X0,appear(efficient_producers,sk3)),sF10,ifeq(greater(sk2(sk3),X0),sF10,sF10,sF10),sF10) ).
cnf(u1081,negated_conjecture,
sF10 = ifeq(sF0(sk1(sk2(sk3),first_movers),X0),sF10,greater(sk1(sk1(sk2(sk3),first_movers),X0),sk2(sk3)),sF10) ).
cnf(u186,negated_conjecture,
zero = ifeq2(finite_set(X0),sF10,sF4(X1,X0),zero) ).
cnf(u147,negated_conjecture,
sF10 = ifeq(environment(X0),sF10,sF8(X0),sF10) ).
cnf(u42,axiom,
appear(first_movers,X0) = sF7(X0) ).
cnf(u507,negated_conjecture,
sF10 = ifeq(greater(X0,sk2(sk3)),sF10,greater(X0,appear(efficient_producers,sk3)),sF10) ).
cnf(u88,negated_conjecture,
zero = ifeq2(finite_set(X0),true,sF4(X1,X0),zero) ).
cnf(u31,negated_conjecture,
true = sF2(X0,X1) ).
cnf(u688,negated_conjecture,
sF10 = ifeq(greater(X0,sF6),sF10,sF13(X0),sF10) ).
cnf(u697,negated_conjecture,
sF10 = ifeq(sF15(sF7(X0)),sF10,ifeq(in_environment(X0,sF14),sF10,sF10,sF10),sF10) ).
cnf(u508,negated_conjecture,
sF10 = ifeq(greater(appear(efficient_producers,sk3),X0),sF10,greater(sk2(sk3),X0),sF10) ).
cnf(u734,negated_conjecture,
sF10 = ifeq(greater(sk1(appear(efficient_producers,sk3),X0),sk2(sk3)),sF10,sF0(appear(efficient_producers,sk3),X0),sF10) ).
cnf(u448,negated_conjecture,
sF10 = ifeq(greater(X0,sF6),sF10,sF15(X0),sF10) ).
cnf(u11,axiom,
true = ifeq(greater(X0,X1),true,ifeq(in_environment(X2,X1),true,ifeq(environment(X2),true,ifeq(stable(X2),true,in_environment(X2,X0),true),true),true),true) ).
cnf(u430,negated_conjecture,
sF10 = ifeq(greater(X1,sF7(X0)),sF10,ifeq(greater(sF6,X1),sF10,sF8(X0),sF10),sF10) ).
cnf(u731,negated_conjecture,
sF10 = ifeq(greater(X0,X0),sF10,ifeq(sF0(X0,X1),sF10,sF0(X0,X1),sF10),sF10) ).
cnf(u432,negated_conjecture,
sF10 = ifeq(greater(X0,X2),sF10,ifeq(sF0(X0,X1),sF10,greater(sk1(X0,X1),X2),sF10),sF10) ).
cnf(u1026,negated_conjecture,
sF10 = ifeq(in_environment(X0,appear(efficient_producers,sk3)),sF10,ifeq(environment(X0),sF10,ifeq(stable(X0),sF10,in_environment(X0,sk1(sk2(sk3),first_movers)),sF10),sF10),sF10) ).
cnf(u286,negated_conjecture,
sF4(X0,X1) = ifeq2(contracts_from(X0,X1),sF10,sF3,sF3) ).
cnf(u433,negated_conjecture,
sF10 = ifeq(greater(sF7(X0),X1),sF10,ifeq(sF8(X0),sF10,greater(sF6,X1),sF10),sF10) ).
cnf(u417,negated_conjecture,
sF10 = ifeq(greater(X0,X1),sF10,ifeq(greater(X2,X0),sF10,greater(X2,X1),sF10),sF10) ).
cnf(u445,negated_conjecture,
sF10 = ifeq(sF15(X0),sF10,ifeq(greater(sF6,X0),sF10,sF10,sF10),sF10) ).
cnf(u736,negated_conjecture,
sF10 = ifeq(sF0(X0,X1),sF10,ifeq(sF0(sk1(X0,X1),X2),sF10,greater(sk1(sk1(X0,X1),X2),X0),sF10),sF10) ).
cnf(u754,negated_conjecture,
sF10 = ifeq(greater(X0,sk1(sk2(sk3),first_movers)),sF10,greater(X0,sk2(sk3)),sF10) ).
cnf(u339,negated_conjecture,
sF10 = ifeq(environment(X0),sF10,ifeq(stable(X0),sF10,in_environment(X0,sF7(X0)),sF10),sF10) ).
cnf(u610,negated_conjecture,
sF10 = ifeq(greater(X0,X1),sF10,ifeq(in_environment(X2,X1),sF10,ifeq(environment(X2),sF10,ifeq(stable(X2),sF10,in_environment(X2,X0),sF10),sF10),sF10),sF10) ).
cnf(u566,negated_conjecture,
sF10 = ifeq(sF0(sF7(X0),X1),sF10,ifeq(greater(sF6,sk1(sF7(X0),X1)),sF10,sF8(X0),sF10),sF10) ).
cnf(u17,hypothesis,
true = ifeq(environment(X0),true,ifeq(stable(X0),true,contracts_from(sk2(X0),first_movers),true),true) ).
cnf(u26,axiom,
greater(sk1(X1,X0),X1) = sF0(X1,X0) ).
cnf(u44,axiom,
greater(sF6,sF7(X0)) = sF8(X0) ).
cnf(u733,negated_conjecture,
sF10 = ifeq(greater(X0,sk2(sk3)),sF10,ifeq(greater(sk1(sk2(sk3),first_movers),X0),sF10,sF10,sF10),sF10) ).
cnf(u5,axiom,
true = ifeq(environment(X0),true,ifeq(stable(X0),true,in_environment(X0,appear(first_movers,X0)),true),true) ).
cnf(u636,negated_conjecture,
sF10 = ifeq(in_environment(X0,appear(efficient_producers,sk3)),sF10,ifeq(environment(X0),sF10,ifeq(stable(X0),sF10,in_environment(X0,sk2(sk3)),sF10),sF10),sF10) ).
cnf(u82,negated_conjecture,
true = ifeq(finite_set(X0),true,sF1(X1,X0),true) ).
cnf(u15,hypothesis,
true = ifeq(environment(X0),true,ifeq(stable(X0),true,greater(sk2(X0),appear(efficient_producers,X0)),true),true) ).
cnf(u744,negated_conjecture,
sF10 = ifeq(sF0(sk2(sk3),X0),sF10,greater(sk1(sk2(sk3),X0),appear(efficient_producers,sk3)),sF10) ).
cnf(u743,negated_conjecture,
sF10 = ifeq(greater(sk2(sk3),X0),sF10,greater(sk1(sk2(sk3),first_movers),X0),sF10) ).
cnf(u94,negated_conjecture,
true = ifeq(environment(X0),true,sF8(X0),true) ).
cnf(u684,negated_conjecture,
sF10 = ifeq(greater(sF6,X0),sF10,ifeq(sF13(X0),sF10,sF10,sF10),sF10) ).
cnf(u222,negated_conjecture,
sF1(X0,X1) = ifeq(contracts_from(X0,X1),sF10,sF0(X0,X1),sF10) ).
cnf(u863,negated_conjecture,
sF10 = ifeq(sF8(X0),sF10,ifeq(sF13(sF7(X0)),sF10,sF10,sF10),sF10) ).
cnf(u591,negated_conjecture,
sF10 = ifeq(sF8(X1),sF10,ifeq(sF0(sF6,X0),sF10,greater(sk1(sF6,X0),sF7(X1)),sF10),sF10) ).
cnf(u665,negated_conjecture,
sF10 = ifeq(sF15(X0),sF10,sF13(X0),sF10) ).
cnf(u567,negated_conjecture,
sF10 = ifeq(sF8(X0),sF10,ifeq(greater(sF6,sF6),sF10,sF8(X0),sF10),sF10) ).
cnf(u13,axiom,
true = ifeq(greater(X0,X1),true,ifeq(greater(X2,X0),true,greater(X2,X1),true),true) ).
cnf(u659,negated_conjecture,
sF10 = ifeq(sF8(X0),sF10,ifeq(sF13(sF7(X0)),sF10,sF13(sF6),sF10),sF10) ).
cnf(u213,axiom,
sF16(sk1(sF14,X0)) = tuple(sF12,sF13(sk1(sF14,X0)),sF0(sF14,X0)) ).
cnf(u1034,negated_conjecture,
sF10 = ifeq(greater(sk1(appear(efficient_producers,sk3),X0),sk1(sk2(sk3),first_movers)),sF10,sF0(appear(efficient_producers,sk3),X0),sF10) ).
cnf(u38,negated_conjecture,
zero = sF5(X0,X1) ).
cnf(u35,axiom,
ifeq2(contracts_from(X1,X0),true,sF3,zero) = sF4(X1,X0) ).
cnf(u1210,negated_conjecture,
sF10 = ifeq(sF0(sk2(sk3),X0),sF10,ifeq(greater(sk1(sk2(sk3),first_movers),sk1(sk2(sk3),X0)),sF10,sF10,sF10),sF10) ).
cnf(u164,negated_conjecture,
sF10 = sF1(X0,first_movers) ).
cnf(ifeq_axiom_001,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u63,axiom,
tuple(sF12,sF13(X0),sF15(X0)) = sF16(X0) ).
cnf(u285,negated_conjecture,
sF3 = ifeq2(finite_set(X0),sF10,sF4(X1,X0),sF3) ).
cnf(u441,negated_conjecture,
sF10 = ifeq(sF0(sF14,X0),sF10,ifeq(greater(X1,sk1(sF14,X0)),sF10,sF15(X1),sF10),sF10) ).
cnf(u517,negated_conjecture,
sF10 = ifeq(greater(sF14,X0),sF10,ifeq(sF15(sk1(X0,X1)),sF10,sF0(X0,X1),sF10),sF10) ).
cnf(u766,negated_conjecture,
sF10 = ifeq(in_environment(X0,sF14),sF10,ifeq(environment(X0),sF10,ifeq(stable(X0),sF10,in_environment(X0,sF6),sF10),sF10),sF10) ).
cnf(u1082,negated_conjecture,
sF10 = ifeq(greater(sk1(sk2(sk3),X0),sk1(sk2(sk3),first_movers)),sF10,sF0(sk2(sk3),X0),sF10) ).
cnf(u529,negated_conjecture,
sF10 = ifeq(greater(sF14,sF7(X0)),sF10,sF8(X0),sF10) ).
cnf(u701,negated_conjecture,
sF10 = ifeq(sF0(sF6,X0),sF10,sF13(sk1(sF6,X0)),sF10) ).
cnf(u434,negated_conjecture,
sF10 = ifeq(greater(sF14,X1),sF10,ifeq(sF15(X0),sF10,greater(X0,X1),sF10),sF10) ).
cnf(u650,negated_conjecture,
sF10 = ifeq(greater(X0,X1),sF10,ifeq(sF13(X1),sF10,sF13(X0),sF10),sF10) ).
cnf(u61,axiom,
greater(X0,sF14) = sF15(X0) ).
cnf(u898,negated_conjecture,
sF10 = ifeq(sF15(sF14),sF10,ifeq(sF0(sF14,X0),sF10,sF0(sF14,X0),sF10),sF10) ).
cnf(u447,negated_conjecture,
sF10 = ifeq(sF15(sF7(X0)),sF10,ifeq(sF8(X0),sF10,sF10,sF10),sF10) ).
cnf(u210,axiom,
sF15(sk1(sF14,X0)) = sF0(sF14,X0) ).
cnf(u28,axiom,
ifeq(contracts_from(X1,X0),true,sF0(X1,X0),true) = sF1(X1,X0) ).
cnf(u627,negated_conjecture,
sF10 = ifeq(sF8(X0),sF10,ifeq(in_environment(X1,sF7(X0)),sF10,ifeq(environment(X1),sF10,ifeq(stable(X1),sF10,in_environment(X1,sF6),sF10),sF10),sF10),sF10) ).
cnf(u66,negated_conjecture,
sF16(X0) != sF17 ).
cnf(ifeq_axiom,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u527,negated_conjecture,
sF10 = ifeq(greater(sF14,X0),sF10,greater(sF6,X0),sF10) ).
cnf(u568,negated_conjecture,
sF10 = ifeq(greater(sF7(X0),sF7(X1)),sF10,ifeq(sF8(X0),sF10,sF8(X1),sF10),sF10) ).
cnf(u630,negated_conjecture,
sF10 = ifeq(sF15(X0),sF10,ifeq(in_environment(X1,sF14),sF10,ifeq(environment(X1),sF10,ifeq(stable(X1),sF10,in_environment(X1,X0),sF10),sF10),sF10),sF10) ).
cnf(u593,negated_conjecture,
sF10 = ifeq(sF8(X0),sF10,ifeq(greater(sk1(sF7(X0),X1),sF6),sF10,sF0(sF7(X0),X1),sF10),sF10) ).
cnf(u159,negated_conjecture,
sF10 = ifeq(finite_set(X0),sF10,sF1(X1,X0),sF10) ).
cnf(u190,negated_conjecture,
zero = sF4(X0,first_movers) ).
cnf(u728,negated_conjecture,
sF10 = ifeq(sF0(X0,X1),sF10,ifeq(greater(sk1(X0,X2),sk1(X0,X1)),sF10,sF0(X0,X2),sF10),sF10) ).
cnf(u1033,negated_conjecture,
sF10 = ifeq(sF0(sk1(sk2(sk3),first_movers),X0),sF10,greater(sk1(sk1(sk2(sk3),first_movers),X0),appear(efficient_producers,sk3)),sF10) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT038-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n006.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 17:23:11 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 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
% 4.70/1.72 % (3194604)Detected a unit-equality problem, will run specialized UEQ schedule.
% 4.70/1.72 % (3194609)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=1078477229:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 4.70/1.72 % (3194615)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=891133476:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 4.70/1.72 % (3194610)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3059791292:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 4.70/1.72 % (3194611)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=4045828050:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 4.70/1.72 % (3194612)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3481066334:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 4.70/1.72 % (3194613)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=8685231:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 4.70/1.72 % (3194614)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3095554157:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 4.70/1.72 % (3194615)Refutation not found, incomplete strategy
% 4.70/1.72 % (3194615)------------------------------
% 4.70/1.72 % (3194615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.72 % (3194615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.72 % (3194615)CaDiCaL version: 2.1.3
% 4.70/1.72 % (3194615)Termination reason: Refutation not found, incomplete strategy
% 4.70/1.72 % (3194615)Time elapsed: 0.011 s
% 4.70/1.72 % (3194615)Peak memory usage: 87 MB
% 4.70/1.72 % (3194615)Instructions burned: 18 (million)
% 4.70/1.72 % (3194612)Refutation not found, incomplete strategy
% 4.70/1.72 % (3194612)------------------------------
% 4.70/1.72 % (3194612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.72 % (3194612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.72 % (3194612)CaDiCaL version: 2.1.3
% 4.70/1.72 % (3194612)Termination reason: Refutation not found, incomplete strategy
% 4.70/1.72 % (3194612)Time elapsed: 0.012 s
% 4.70/1.72 % (3194612)Peak memory usage: 88 MB
% 4.70/1.72 % (3194612)Instructions burned: 19 (million)
% 4.70/1.72 % (3194613)Refutation not found, incomplete strategy
% 4.70/1.72 % (3194613)------------------------------
% 4.70/1.72 % (3194613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.72 % (3194613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.72 % (3194613)CaDiCaL version: 2.1.3
% 4.70/1.72 % (3194613)Termination reason: Refutation not found, incomplete strategy
% 4.70/1.72 % (3194613)Time elapsed: 0.016 s
% 4.70/1.72 % (3194613)Peak memory usage: 88 MB
% 4.70/1.72 % (3194613)Instructions burned: 25 (million)
% 4.70/1.72 % (3194614)Refutation not found, incomplete strategy
% 4.70/1.72 % (3194614)------------------------------
% 4.70/1.72 % (3194614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.72 % (3194614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.72 % (3194614)CaDiCaL version: 2.1.3
% 4.70/1.72 % (3194614)Termination reason: Refutation not found, incomplete strategy
% 4.70/1.72 % (3194614)Time elapsed: 0.016 s
% 4.70/1.72 % (3194614)Peak memory usage: 88 MB
% 4.70/1.72 % (3194614)Instructions burned: 22 (million)
% 4.70/1.72 % (3194615)------------------------------
% 4.70/1.72 % (3194615)------------------------------
% 4.70/1.72 % (3194612)------------------------------
% 4.70/1.72 % (3194612)------------------------------
% 4.70/1.72 % (3194613)------------------------------
% 4.70/1.72 % (3194613)------------------------------
% 4.70/1.72 % (3194614)------------------------------
% 4.70/1.72 % (3194614)------------------------------
% 4.70/1.72 % (3194609)Refutation not found, incomplete strategy
% 4.70/1.72 % (3194609)------------------------------
% 4.70/1.72 % (3194609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.72 % (3194609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.72 % (3194609)CaDiCaL version: 2.1.3
% 4.70/1.72 % (3194609)Termination reason: Refutation not found, incomplete strategy
% 4.70/1.72 % (3194609)Time elapsed: 0.374 s
% 4.70/1.72 % (3194609)Peak memory usage: 128 MB
% 4.70/1.72 % (3194609)Instructions burned: 971 (million)
% 4.70/1.72 % (3194623)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2313762947:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 4.70/1.72 % (3194625)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3385701841:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 4.70/1.72 % (3194624)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3495141149:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 4.70/1.72 % (3194626)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=16049953:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2995 on theBenchmark for (2995ds/317Mi)
% 4.70/1.72 % (3194626)First to succeed.
% 4.70/1.72 % (3194626)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3194604"
% 4.70/1.72 % (3194609)------------------------------
% 4.70/1.72 % (3194609)------------------------------
% 4.70/1.72 % (3194625)Instruction limit reached!
% 4.70/1.72 % (3194625)------------------------------
% 4.70/1.72 % (3194625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.72 % (3194625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.72 % (3194625)CaDiCaL version: 2.1.3
% 4.70/1.72 % (3194625)Termination reason: Instruction limit
% 4.70/1.72 % (3194625)Termination phase: Saturation
% 4.70/1.72 % (3194625)Time elapsed: 0.105 s
% 4.70/1.72 % (3194625)Peak memory usage: 91 MB
% 4.70/1.72 % (3194625)Instructions burned: 217 (million)
% 4.70/1.72 % (3194631)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=3048622748:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2993 on theBenchmark for (2993ds/12125Mi)
% 4.70/1.72 % (3194632)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1923252634:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2993 on theBenchmark for (2993ds/2836Mi)
% 4.70/1.72 % (3194632)Also succeeded, but the first one will report.
% 4.70/1.72 % (3194610)Also succeeded, but the first one will report.
% 4.70/1.72 % (3194611)Also succeeded, but the first one will report.
% 4.70/1.72 % SZS status Satisfiable for theBenchmark
% 4.70/1.72 % SZS output start Saturation.
% See solution above
% 6.62/1.92 % SZS output start Definitions and Model Updates.
% 6.62/1.92 % SZS output end Definitions and Model Updates.
% 6.62/1.92 % (3194626)------------------------------
% 6.62/1.92 % (3194626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.62/1.92 % (3194626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.62/1.92 % (3194626)CaDiCaL version: 2.1.3
% 6.62/1.92 % (3194626)Termination reason: Satisfiable
% 6.62/1.92 % (3194626)Time elapsed: 0.040 s
% 6.62/1.92 % (3194626)Peak memory usage: 89 MB
% 6.62/1.92 % (3194626)Instructions burned: 60 (million)
% 6.62/1.92 % (3194626)------------------------------
% 6.62/1.92 % (3194626)------------------------------
% 6.62/1.92 % (3194604)Success in time 0.844 s
% 6.62/1.92 % Vampire exiting
%------------------------------------------------------------------------------