%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:11:35 AM UTC 2026
% Result : Theorem 0.15s 0.38s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 11
% Syntax : Number of formulae : 171 ( 134 unt; 0 def)
% Number of atoms : 432 ( 0 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 482 ( 221 ~; 218 |; 40 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 15 ( 14 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-6 aty)
% Number of variables : 96 ( 6 sgn 18 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(conjecture,plain,
? [RhoR,Pw,S] :
( founds_rem(e1,RhoR,f1)
& power(Pw)
& bearer(Pw,philharmonie)
& cnt(Pw,decl(distrib),concert_ds)
& part_of(Pw,RhoR)
& about_event(Pw,e1)
& subjection(S)
& bearer(S,marketplace)
& cnt(S,decl(distrib),concert_ds)
& part_of(S,RhoR)
& about_event(S,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture) ).
fof(conjecture_negated,plain,
~ ? [RhoR,Pw,S] :
( founds_rem(e1,RhoR,f1)
& power(Pw)
& bearer(Pw,philharmonie)
& cnt(Pw,decl(distrib),concert_ds)
& part_of(Pw,RhoR)
& about_event(Pw,e1)
& subjection(S)
& bearer(S,marketplace)
& cnt(S,decl(distrib),concert_ds)
& part_of(S,RhoR)
& about_event(S,e1) ),
inference(negate_conjecture,[status(cth)],[conjecture]) ).
cnf(45,plain,
( ~ about_event(X0,e1)
| ~ about_event(X1,e1)
| ~ bearer(X0,philharmonie)
| ~ bearer(X1,marketplace)
| ~ subjection(X1)
| ~ cnt(X0,decl(distrib),concert_ds)
| ~ cnt(X1,decl(distrib),concert_ds)
| ~ part_of(X0,X2)
| ~ part_of(X1,X2)
| ~ founds_rem(e1,X2,f1)
| ~ power(X0) ),
inference(cnf,[status(esa)],[conjecture_negated]) ).
cnf(l0,plain,
( ~ about_event(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ about_event(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ bearer(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie)
| ~ bearer(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace)
| ~ subjection(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ cnt(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ part_of(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ part_of(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ founds_rem(e1,sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1)
| ~ power(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1)) ),
inference(instantiation,[status(thm)],[45]) ).
fof(ax_proh_relator_remedy,plain,
! [F,X,Y,A,T,E] :
( ( proh(F)
& has_rem(F)
& aee(F,X)
& aer(F,Y)
& act(F,A)
& tgt(F,T)
& activates(E,F) )
=> ? [RhoR,Pw,S] :
( founds_rem(E,RhoR,F)
& power(Pw)
& bearer(Pw,Y)
& cnt(Pw,decl(A),T)
& part_of(Pw,RhoR)
& subjection(S)
& bearer(S,X)
& cnt(S,decl(A),T)
& part_of(S,RhoR) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_proh_relator_remedy) ).
cnf(16,plain,
( ~ proh(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ has_rem(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| cnt(sK6(X0,X4,X1,X2,X3,X5),decl(X2),X3) ),
inference(cnf,[status(esa)],[ax_proh_relator_remedy]) ).
cnf(l19,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| cnt(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) ),
inference(instantiation,[status(thm)],[16]) ).
fof(act_f1,plain,
act(f1,distrib),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act_f1) ).
cnf(41,plain,
act(f1,distrib),
inference(cnf,[status(esa)],[act_f1]) ).
cnf(l25,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
fof(rem_f1,plain,
has_rem(f1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rem_f1) ).
cnf(38,plain,
has_rem(f1),
inference(cnf,[status(esa)],[rem_f1]) ).
cnf(l26,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(9,plain,
( ~ proh(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ has_rem(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| founds_rem(X5,sK4(X0,X4,X1,X2,X3,X5),X0) ),
inference(cnf,[status(esa)],[ax_proh_relator_remedy]) ).
cnf(l7,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| founds_rem(e1,sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1) ),
inference(instantiation,[status(thm)],[9]) ).
fof(tgt_f1,plain,
tgt(f1,concert_ds),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tgt_f1) ).
cnf(42,plain,
tgt(f1,concert_ds),
inference(cnf,[status(esa)],[tgt_f1]) ).
cnf(l27,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(15,plain,
( ~ proh(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ has_rem(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| bearer(sK6(X0,X4,X1,X2,X3,X5),X4) ),
inference(cnf,[status(esa)],[ax_proh_relator_remedy]) ).
cnf(l1,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| bearer(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l28,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(11,plain,
( ~ proh(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ has_rem(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| bearer(sK5(X0,X4,X1,X2,X3,X5),X1) ),
inference(cnf,[status(esa)],[ax_proh_relator_remedy]) ).
cnf(l5,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| bearer(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie) ),
inference(instantiation,[status(thm)],[11]) ).
fof(aer_f1,plain,
aer(f1,philharmonie),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aer_f1) ).
cnf(40,plain,
aer(f1,philharmonie),
inference(cnf,[status(esa)],[aer_f1]) ).
cnf(l29,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l23,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
fof(act_e1_f1,plain,
activates(e1,f1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act_e1_f1) ).
cnf(43,plain,
activates(e1,f1),
inference(cnf,[status(esa)],[act_e1_f1]) ).
cnf(l30,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l31,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
fof(ax_B2,plain,
! [Pw,A,T,Rho,E,R] :
( ( power(Pw)
& cnt(Pw,decl(A),T)
& part_of(Pw,Rho)
& founds_rem(E,Rho,R) )
=> about_event(Pw,E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_B2) ).
cnf(29,plain,
( ~ cnt(X0,decl(X1),X2)
| ~ part_of(X0,X3)
| ~ founds_rem(X4,X3,X5)
| ~ power(X0)
| about_event(X0,X4) ),
inference(cnf,[status(esa)],[ax_B2]) ).
cnf(l2,plain,
( ~ cnt(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ part_of(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ founds_rem(e1,sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1)
| ~ power(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| about_event(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l35,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(17,plain,
( ~ proh(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ has_rem(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| part_of(sK6(X0,X4,X1,X2,X3,X5),sK4(X0,X4,X1,X2,X3,X5)) ),
inference(cnf,[status(esa)],[ax_proh_relator_remedy]) ).
cnf(l15,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| part_of(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l36,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
fof(proh_f1,plain,
proh(f1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',proh_f1) ).
cnf(37,plain,
proh(f1),
inference(cnf,[status(esa)],[proh_f1]) ).
cnf(l37,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(13,plain,
( ~ proh(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ has_rem(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| part_of(sK5(X0,X4,X1,X2,X3,X5),sK4(X0,X4,X1,X2,X3,X5)) ),
inference(cnf,[status(esa)],[ax_proh_relator_remedy]) ).
cnf(l38,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| part_of(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(10,plain,
( ~ proh(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ has_rem(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| power(sK5(X0,X4,X1,X2,X3,X5)) ),
inference(cnf,[status(esa)],[ax_proh_relator_remedy]) ).
cnf(l8,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| power(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l39,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l40,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l22,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l41,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l21,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l42,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l16,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l43,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l44,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l45,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l46,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l47,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l48,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
fof(aee_f1,plain,
aee(f1,marketplace),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aee_f1) ).
cnf(39,plain,
aee(f1,marketplace),
inference(cnf,[status(esa)],[aee_f1]) ).
cnf(l49,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l20,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l33,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l50,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
fof(ax_B3,plain,
! [S,A,T,Rho,E,R] :
( ( subjection(S)
& cnt(S,decl(A),T)
& part_of(S,Rho)
& founds_rem(E,Rho,R) )
=> about_event(S,E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_B3) ).
cnf(30,plain,
( ~ subjection(X0)
| ~ cnt(X0,decl(X1),X2)
| ~ part_of(X0,X3)
| ~ founds_rem(X4,X3,X5)
| about_event(X0,X4) ),
inference(cnf,[status(esa)],[ax_B3]) ).
cnf(l4,plain,
( ~ subjection(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ part_of(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ founds_rem(e1,sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1)
| about_event(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l34,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| founds_rem(e1,sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l51,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l32,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l52,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l53,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l54,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l14,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| founds_rem(e1,sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l55,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(12,plain,
( ~ proh(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ has_rem(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| cnt(sK5(X0,X4,X1,X2,X3,X5),decl(X2),X3) ),
inference(cnf,[status(esa)],[ax_proh_relator_remedy]) ).
cnf(l56,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| cnt(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l57,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l58,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l59,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l60,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l17,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l61,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l62,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l63,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l64,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l65,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l66,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l67,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l68,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l18,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l69,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l70,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l71,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l9,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| power(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l72,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l73,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l74,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l75,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l6,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| cnt(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(14,plain,
( ~ proh(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ has_rem(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| subjection(sK6(X0,X4,X1,X2,X3,X5)) ),
inference(cnf,[status(esa)],[ax_proh_relator_remedy]) ).
cnf(l76,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| subjection(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l77,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l78,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l79,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l80,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l81,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l82,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l83,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l84,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l85,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l86,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l87,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l88,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l89,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l90,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l91,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l24,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| cnt(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l92,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l93,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l3,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| subjection(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l13,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l94,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l95,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l96,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l97,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l98,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l99,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| part_of(sK5(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l100,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l101,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l102,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l103,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l104,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l105,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l106,plain,
( ~ proh(f1)
| ~ aer(f1,philharmonie)
| ~ act(f1,distrib)
| ~ tgt(f1,concert_ds)
| ~ has_rem(f1)
| ~ aee(f1,marketplace)
| ~ activates(e1,f1)
| part_of(sK6(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l107,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l108,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l109,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l11,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l110,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l111,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l112,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l113,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l114,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l115,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l116,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l117,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l118,plain,
aer(f1,philharmonie),
inference(instantiation,[status(thm)],[40]) ).
cnf(l10,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l119,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l120,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l121,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l12,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l122,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l123,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l124,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l125,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l126,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l127,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l128,plain,
has_rem(f1),
inference(instantiation,[status(thm)],[38]) ).
cnf(l129,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l130,plain,
activates(e1,f1),
inference(instantiation,[status(thm)],[43]) ).
cnf(l131,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l132,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l133,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(l134,plain,
proh(f1),
inference(instantiation,[status(thm)],[37]) ).
cnf(l135,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l136,plain,
tgt(f1,concert_ds),
inference(instantiation,[status(thm)],[42]) ).
cnf(l137,plain,
act(f1,distrib),
inference(instantiation,[status(thm)],[41]) ).
cnf(l138,plain,
aee(f1,marketplace),
inference(instantiation,[status(thm)],[39]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l19,l25,l26,l7,l27,l1,l28,l5,l29,l23,l30,l31,l2,l35,l15,l36,l37,l38,l8,l39,l40,l22,l41,l21,l42,l16,l43,l44,l45,l46,l47,l48,l49,l20,l33,l50,l4,l34,l51,l32,l52,l53,l54,l14,l55,l56,l57,l58,l59,l60,l17,l61,l62,l63,l64,l65,l66,l67,l68,l18,l69,l70,l71,l9,l72,l73,l74,l75,l6,l76,l77,l78,l79,l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l24,l92,l93,l3,l13,l94,l95,l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l11,l110,l111,l112,l113,l114,l115,l116,l117,l118,l10,l119,l120,l121,l12,l122,l123,l124,l125,l126,l127,l128,l129,l130,l131,l132,l133,l134,l135,l136,l137,l138]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n005.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 7 14:07:35 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % launching worker at depth: 1
% 0.11/0.37 % launching worker at depth: 5
% 0.11/0.37 % launching worker at depth: 7
% 0.11/0.37 % launching worker at depth: 8
% 0.11/0.37 % launching worker at depth: 2
% 0.11/0.37 % launching worker at depth: 6
% 0.11/0.37 % launching worker at depth: 3
% 0.11/0.37 % launching worker at depth: 4
% 0.11/0.38 % launching worker at depth: 9
% 0.15/0.38 % SZS status Theorem for theBenchmark
% 0.15/0.38 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------