%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : MGT040+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% 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 8 06:19:54 AM UTC 2026
% Result : CounterSatisfiable 0.23s 0.54s
% Output : Saturation 0.23s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 74ERROR: Could not build tree for root 86ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(86,plain,
( ~ environment(u)
| ~ environment(critical_point(u))
| ~ rapid_change(u)
| ~ observational_period(u)
| empty(u)
| selection_favors(first_movers,efficient_producers,end_time(u))
| empty(critical_point(u))
| selection_favors(first_movers,efficient_producers,end_time(critical_point(u))) ),
inference(res,[status(thm),theory(equality)],[75,83]),
[iquote('0:Res:75.1,83.3')] ).
cnf(89,plain,
( ~ environment(u)
| ~ in_environment(u,v)
| ~ greater(critical_point(u),v)
| empty(u)
| selection_favors(first_movers,efficient_producers,end_time(u))
| greater(appear(efficient_producers,u),v)
| selection_favors(first_movers,efficient_producers,v) ),
inference(obv,[status(thm),theory(equality)],[88]),
[iquote('0:Obv:88.0')] ).
cnf(79,plain,
( ~ environment(u)
| empty(u)
| selection_favors(first_movers,efficient_producers,end_time(u))
| greater(appear(efficient_producers,u),critical_point(u))
| equal(appear(efficient_producers,u),critical_point(u))
| greater(critical_point(u),appear(efficient_producers,u)) ),
inference(res,[status(thm),theory(equality)],[75,40]),
[iquote('0:Res:75.1,40.0')] ).
cnf(87,plain,
( ~ environment(u)
| ~ environment(appear(first_movers,u))
| ~ rapid_change(u)
| ~ observational_period(u)
| empty(u)
| empty(appear(first_movers,u))
| selection_favors(first_movers,efficient_producers,end_time(appear(first_movers,u))) ),
inference(res,[status(thm),theory(equality)],[49,83]),
[iquote('0:Res:49.2,83.3')] ).
cnf(84,plain,
( ~ environment(u)
| ~ in_environment(u,skc1)
| ~ greater(critical_point(u),skc1)
| empty(u)
| selection_favors(first_movers,efficient_producers,end_time(u))
| greater(appear(efficient_producers,u),skc1) ),
inference(obv,[status(thm),theory(equality)],[76]),
[iquote('0:Obv:76.0')] ).
cnf(80,plain,
( ~ environment(u)
| ~ empty(critical_point(u))
| ~ environment(critical_point(u))
| ~ observational_period(u)
| empty(u)
| selection_favors(first_movers,efficient_producers,end_time(u))
| extreme(u) ),
inference(res,[status(thm),theory(equality)],[75,12]),
[iquote('0:Res:75.1,12.3')] ).
cnf(85,plain,
( ~ environment(u)
| ~ environment(end_time(u))
| ~ rapid_change(u)
| ~ observational_period(u)
| empty(end_time(u))
| selection_favors(first_movers,efficient_producers,end_time(end_time(u))) ),
inference(res,[status(thm),theory(equality)],[7,83]),
[iquote('0:Res:7.1,83.3')] ).
cnf(70,plain,
( ~ environment(u)
| ~ in_environment(u,v)
| ~ in_environment(u,critical_point(u))
| ~ greater(critical_point(u),v)
| greater(appear(efficient_producers,u),v)
| selection_favors(first_movers,efficient_producers,v) ),
inference(res,[status(thm),theory(equality)],[11,19]),
[iquote('0:Res:11.1,19.2')] ).
cnf(83,plain,
( ~ environment(u)
| ~ rapid_change(v)
| ~ observational_period(v)
| ~ in_environment(v,u)
| empty(u)
| selection_favors(first_movers,efficient_producers,end_time(u)) ),
inference(obv,[status(thm),theory(equality)],[77]),
[iquote('0:Obv:77.0')] ).
cnf(82,plain,
( ~ environment(u)
| ~ in_environment(skc1,u)
| selection_favors(first_movers,efficient_producers,end_time(u)) ),
inference(mrr,[status(thm)],[81,34]),
[iquote('0:MRR:81.2,34.0')] ).
cnf(75,plain,
( ~ environment(u)
| in_environment(u,critical_point(u))
| empty(u)
| selection_favors(first_movers,efficient_producers,end_time(u)) ),
inference(obv,[status(thm),theory(equality)],[74]),
[iquote('0:Obv:74.3')] ).
cnf(73,plain,
( ~ environment(u)
| greater(appear(efficient_producers,u),end_time(u))
| in_environment(u,critical_point(u))
| selection_favors(first_movers,efficient_producers,end_time(u)) ),
inference(mrr,[status(thm)],[72,7]),
[iquote('0:MRR:72.1,7.1')] ).
cnf(64,plain,
( ~ environment(u)
| ~ in_environment(u,v)
| ~ greater(critical_point(u),v)
| greater(appear(efficient_producers,u),v)
| in_environment(u,critical_point(u))
| selection_favors(first_movers,efficient_producers,end_time(u)) ),
inference(res,[status(thm),theory(equality)],[11,21]),
[iquote('0:Res:11.1,21.1')] ).
cnf(63,plain,
( ~ environment(u)
| empty(u)
| greater(appear(efficient_producers,u),appear(first_movers,u))
| equal(appear(efficient_producers,u),appear(first_movers,u))
| greater(appear(first_movers,u),appear(efficient_producers,u)) ),
inference(res,[status(thm),theory(equality)],[49,40]),
[iquote('0:Res:49.2,40.0')] ).
cnf(19,axiom,
( ~ environment(u)
| ~ in_environment(u,critical_point(u))
| ~ greater_or_equal(v,appear(efficient_producers,u))
| ~ greater(critical_point(u),v)
| selection_favors(first_movers,efficient_producers,v) ),
file('MGT040+1.p',unknown),
[] ).
cnf(69,plain,
( ~ environment(u)
| equal(appear(efficient_producers,u),end_time(u))
| greater(end_time(u),appear(efficient_producers,u))
| empty(u)
| selection_favors(first_movers,efficient_producers,end_time(u)) ),
inference(obv,[status(thm),theory(equality)],[68]),
[iquote('0:Obv:68.0')] ).
cnf(67,plain,
( ~ environment(u)
| ~ greater(appear(efficient_producers,u),end_time(u))
| empty(u)
| selection_favors(first_movers,efficient_producers,end_time(u)) ),
inference(mrr,[status(thm)],[66,7]),
[iquote('0:MRR:66.1,7.1')] ).
cnf(20,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| ~ greater_or_equal(v,appear(first_movers,u))
| ~ greater(appear(efficient_producers,u),v)
| selection_favors(first_movers,efficient_producers,v) ),
file('MGT040+1.p',unknown),
[] ).
cnf(61,plain,
( ~ environment(u)
| ~ in_environment(u,skc1)
| ~ in_environment(u,critical_point(u))
| ~ greater(critical_point(u),skc1)
| greater(appear(efficient_producers,u),skc1) ),
inference(res,[status(thm),theory(equality)],[11,33]),
[iquote('0:Res:11.1,33.2')] ).
cnf(62,plain,
( ~ environment(u)
| greater(appear(efficient_producers,u),end_time(u))
| equal(appear(efficient_producers,u),end_time(u))
| greater(end_time(u),appear(efficient_producers,u)) ),
inference(res,[status(thm),theory(equality)],[7,40]),
[iquote('0:Res:7.1,40.0')] ).
cnf(54,plain,
( ~ environment(u)
| ~ empty(appear(first_movers,u))
| ~ environment(appear(first_movers,u))
| ~ observational_period(u)
| empty(u)
| extreme(u) ),
inference(res,[status(thm),theory(equality)],[49,12]),
[iquote('0:Res:49.2,12.3')] ).
cnf(45,plain,
( ~ environment(u)
| ~ empty(appear(an_organisation,u))
| ~ environment(appear(an_organisation,u))
| ~ observational_period(u)
| empty(u)
| extreme(u) ),
inference(res,[status(thm),theory(equality)],[42,12]),
[iquote('0:Res:42.2,12.3')] ).
cnf(21,axiom,
( ~ environment(u)
| ~ greater_or_equal(v,appear(efficient_producers,u))
| ~ greater(critical_point(u),v)
| in_environment(u,critical_point(u))
| selection_favors(first_movers,efficient_producers,end_time(u)) ),
file('MGT040+1.p',unknown),
[] ).
cnf(40,plain,
( ~ in_environment(u,v)
| greater(appear(efficient_producers,u),v)
| equal(v,appear(efficient_producers,u))
| greater(v,appear(efficient_producers,u)) ),
inference(res,[status(thm),theory(equality)],[11,8]),
[iquote('0:Res:11.1,8.0')] ).
cnf(33,plain,
( ~ environment(u)
| ~ in_environment(u,critical_point(u))
| ~ greater_or_equal(skc1,appear(efficient_producers,u))
| ~ greater(critical_point(u),skc1) ),
inference(res,[status(thm),theory(equality)],[19,6]),
[iquote('0:Res:19.4,6.0')] ).
cnf(32,plain,
( ~ environment(u)
| ~ in_environment(u,skc1)
| ~ greater_or_equal(skc1,appear(first_movers,u))
| ~ greater(appear(efficient_producers,u),skc1) ),
inference(res,[status(thm),theory(equality)],[20,6]),
[iquote('0:Res:20.4,6.0')] ).
cnf(51,plain,
( ~ environment(u)
| empty(u)
| equal(appear(first_movers,u),end_time(u))
| greater(end_time(u),appear(first_movers,u)) ),
inference(rew,[status(thm),theory(equality)],[47,50]),
[iquote('0:Rew:47.2,50.3')] ).
cnf(17,axiom,
( ~ environment(u)
| ~ rapid_change(v)
| ~ observational_period(v)
| ~ in_environment(v,u)
| ~ in_environment(u,critical_point(u)) ),
file('MGT040+1.p',unknown),
[] ).
cnf(44,plain,
( ~ environment(u)
| ~ empty(end_time(u))
| ~ environment(end_time(u))
| ~ observational_period(u)
| extreme(u) ),
inference(res,[status(thm),theory(equality)],[7,12]),
[iquote('0:Res:7.1,12.3')] ).
cnf(53,plain,
( ~ environment(skc1)
| ~ empty(appear(first_movers,skc1))
| ~ environment(appear(first_movers,skc1))
| empty(skc1) ),
inference(res,[status(thm),theory(equality)],[49,34]),
[iquote('0:Res:49.2,34.2')] ).
cnf(47,plain,
( ~ environment(u)
| empty(u)
| equal(appear(an_organisation,u),appear(first_movers,u)) ),
inference(obv,[status(thm),theory(equality)],[46]),
[iquote('0:Obv:46.0')] ).
cnf(49,plain,
( ~ environment(u)
| empty(u)
| in_environment(u,appear(first_movers,u)) ),
inference(rew,[status(thm),theory(equality)],[47,42]),
[iquote('0:Rew:47.2,42.2')] ).
cnf(48,plain,
( ~ environment(u)
| empty(u)
| greater_or_equal(end_time(u),appear(first_movers,u)) ),
inference(rew,[status(thm),theory(equality)],[47,9]),
[iquote('0:Rew:47.2,9.2')] ).
cnf(15,axiom,
( ~ environment(u)
| ~ in_environment(u,appear(an_organisation,u))
| equal(appear(an_organisation,u),appear(first_movers,u)) ),
file('MGT040+1.p',unknown),
[] ).
cnf(12,axiom,
( ~ empty(u)
| ~ environment(u)
| ~ observational_period(v)
| ~ in_environment(v,u)
| extreme(v) ),
file('MGT040+1.p',unknown),
[] ).
cnf(43,plain,
( ~ environment(skc1)
| ~ empty(appear(an_organisation,skc1))
| ~ environment(appear(an_organisation,skc1))
| empty(skc1) ),
inference(res,[status(thm),theory(equality)],[42,34]),
[iquote('0:Res:42.2,34.2')] ).
cnf(13,axiom,
( ~ environment(u)
| ~ greater_or_equal(end_time(u),appear(an_organisation,u))
| in_environment(u,appear(an_organisation,u)) ),
file('MGT040+1.p',unknown),
[] ).
cnf(11,axiom,
( ~ in_environment(u,v)
| greater_or_equal(v,appear(efficient_producers,u))
| greater(appear(efficient_producers,u),v) ),
file('MGT040+1.p',unknown),
[] ).
cnf(10,axiom,
( ~ environment(u)
| in_environment(u,critical_point(u))
| greater(critical_point(u),end_time(u)) ),
file('MGT040+1.p',unknown),
[] ).
cnf(35,plain,
( ~ environment(u)
| ~ in_environment(u,critical_point(u))
| ~ in_environment(skc1,u) ),
inference(mrr,[status(thm)],[25,1]),
[iquote('0:MRR:25.0,1.0')] ).
cnf(38,plain,
( ~ environment(skc1)
| ~ empty(end_time(skc1))
| ~ environment(end_time(skc1)) ),
inference(res,[status(thm),theory(equality)],[7,34]),
[iquote('0:Res:7.1,34.2')] ).
cnf(8,axiom,
( ~ greater_or_equal(u,v)
| equal(u,v)
| greater(u,v) ),
file('MGT040+1.p',unknown),
[] ).
cnf(34,plain,
( ~ empty(u)
| ~ environment(u)
| ~ in_environment(skc1,u) ),
inference(mrr,[status(thm)],[30,5]),
[iquote('0:MRR:30.3,5.0')] ).
cnf(7,axiom,
( ~ environment(u)
| in_environment(u,end_time(u)) ),
file('MGT040+1.p',unknown),
[] ).
cnf(6,axiom,
~ selection_favors(first_movers,efficient_producers,skc1),
file('MGT040+1.p',unknown),
[] ).
cnf(5,axiom,
~ extreme(skc1),
file('MGT040+1.p',unknown),
[] ).
cnf(1,axiom,
observational_period(skc1),
file('MGT040+1.p',unknown),
[] ).
cnf(2,axiom,
rapid_change(skc1),
file('MGT040+1.p',unknown),
[] ).
cnf(3,axiom,
propagation_strategy(first_movers),
file('MGT040+1.p',unknown),
[] ).
cnf(37,plain,
selection_favors(efficient_producers,first_movers,skc1),
inference(spt,[],[29]),
[iquote('2:Spt:29.1')] ).
cnf(4,axiom,
propagation_strategy(efficient_producers),
file('MGT040+1.p',unknown),
[] ).
cnf(36,plain,
( ~ observational_period(u)
| selection_favors(efficient_producers,first_movers,u) ),
inference(spt,[],[22]),
[iquote('1:Spt:22.0,22.2')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT040+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : run_spass %d %s
% 0.10/0.36 % Computer : n006.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Mon Sep 7 12:57:31 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.23/0.54
% 0.23/0.54 SPASS V 3.9
% 0.23/0.54 SPASS beiseite: Completion found.
% 0.23/0.54 % SZS status CounterSatisfiable
% 0.23/0.54 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.23/0.54 SPASS derived 47 clauses, backtracked 0 clauses, performed 2 splits and kept 61 clauses.
% 0.23/0.54 SPASS allocated 97697 KBytes.
% 0.23/0.54 SPASS spent 0:00:00.16 on the problem.
% 0.23/0.54 0:00:00.06 for the input.
% 0.23/0.54 0:00:00.05 for the FLOTTER CNF translation.
% 0.23/0.54 0:00:00.00 for inferences.
% 0.23/0.54 0:00:00.00 for the backtracking.
% 0.23/0.54 0:00:00.01 for the reduction.
% 0.23/0.54
% 0.23/0.54
% 0.23/0.54 The saturated set of worked-off clauses is :
% 0.23/0.54 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------