%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT113+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 02:11:59 PM UTC 2026
% Result : Theorem 61.42s 8.32s
% Output : Proof 61.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 12
% Syntax : Number of formulae : 125 ( 100 unt; 0 def)
% Number of atoms : 315 ( 78 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 327 ( 137 ~; 131 |; 56 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 3 avg)
% Maximal term depth : 12 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-6 aty)
% Number of variables : 242 ( 14 sgn 60 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f22,conjecture,
? [RhoR,Pw,S] :
( about_event(S,e1)
& part_of(S,RhoR)
& cnt(S,decl(distrib),concert_ds)
& bearer(S,marketplace)
& subjection(S)
& about_event(Pw,e1)
& part_of(Pw,RhoR)
& cnt(Pw,decl(distrib),concert_ds)
& bearer(Pw,philharmonie)
& power(Pw)
& founds_rem(e1,RhoR,f1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture) ).
fof(f22_neg,negated_conjecture,
~ ? [RhoR,Pw,S] :
( about_event(S,e1)
& part_of(S,RhoR)
& cnt(S,decl(distrib),concert_ds)
& bearer(S,marketplace)
& subjection(S)
& about_event(Pw,e1)
& part_of(Pw,RhoR)
& cnt(Pw,decl(distrib),concert_ds)
& bearer(Pw,philharmonie)
& power(Pw)
& founds_rem(e1,RhoR,f1) ),
inference(negated_conjecture,[status(cth)],[f22]) ).
fof(f22_nnf,plain,
! [RhoR,Pw,S] :
( ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ bearer(S,marketplace)
| ~ subjection(S)
| ~ about_event(Pw,e1)
| ~ part_of(Pw,RhoR)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ bearer(Pw,philharmonie)
| ~ power(Pw)
| ~ founds_rem(e1,RhoR,f1) ),
inference(nnf_transformation,[status(thm)],[f22_neg]) ).
fof(f22_sk,plain,
! [RhoR,Pw,S] :
( ~ about_event(S,e1)
| ~ part_of(S,RhoR)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ bearer(S,marketplace)
| ~ subjection(S)
| ~ about_event(Pw,e1)
| ~ part_of(Pw,RhoR)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ bearer(Pw,philharmonie)
| ~ power(Pw)
| ~ founds_rem(e1,RhoR,f1) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c45,plain,
( ~ about_event(X2,e1)
| ~ part_of(X2,X0)
| ~ cnt(X2,decl(distrib),concert_ds)
| ~ bearer(X2,marketplace)
| ~ subjection(X2)
| ~ about_event(X1,e1)
| ~ part_of(X1,X0)
| ~ cnt(X1,decl(distrib),concert_ds)
| ~ bearer(X1,philharmonie)
| ~ power(X1)
| ~ founds_rem(e1,X0,f1) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t77,plain,
ifeq(founds_rem(e1,X1,f1),true,ifeq(power(X2),true,ifeq(bearer(X2,philharmonie),true,ifeq(cnt(X2,decl(distrib),concert_ds),true,ifeq(part_of(X2,X1),true,ifeq(about_event(X2,e1),true,ifeq(subjection(X3),true,ifeq(bearer(X3,marketplace),true,ifeq(cnt(X3,decl(distrib),concert_ds),true,ifeq(part_of(X3,X1),true,ifeq(about_event(X3,e1),true,false,true),true),true),true),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c45]) ).
cnf(t107,plain,
ifeq(founds_rem(e1,X1,f1),true,ifeq(power(X2),true,ifeq(bearer(X2,philharmonie),true,ifeq(cnt(X2,decl(distrib),concert_ds),true,ifeq(part_of(X2,X1),true,ifeq(about_event(X2,e1),true,ifeq(subjection(X3),true,ifeq(bearer(X3,marketplace),true,ifeq(cnt(X3,decl(distrib),concert_ds),true,ifeq(part_of(X3,X1),true,ifeq(about_event(X3,e1),true,false,true),true),true),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t77]) ).
fof(f1,axiom,
! [F,X,Y,A,T,E] :
( ( activates(E,F)
& tgt(F,T)
& act(F,A)
& aer(F,Y)
& aee(F,X)
& has_rem(F)
& proh(F) )
=> ? [RhoR,Pw,S] :
( part_of(S,RhoR)
& cnt(S,decl(A),T)
& bearer(S,X)
& subjection(S)
& part_of(Pw,RhoR)
& cnt(Pw,decl(A),T)
& bearer(Pw,Y)
& power(Pw)
& founds_rem(E,RhoR,F) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_proh_relator_remedy) ).
fof(f1_nnf,plain,
! [F,X,Y,A,T,E] :
( ? [RhoR,Pw,S] :
( part_of(S,RhoR)
& cnt(S,decl(A),T)
& bearer(S,X)
& subjection(S)
& part_of(Pw,RhoR)
& cnt(Pw,decl(A),T)
& bearer(Pw,Y)
& power(Pw)
& founds_rem(E,RhoR,F) )
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ act(F,A)
| ~ aer(F,Y)
| ~ aee(F,X)
| ~ has_rem(F)
| ~ proh(F) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [F,X,Y,A,T,E] :
( ( part_of(sk5(F,X,Y,A,T,E),sk3(F,X,Y,A,T,E))
& cnt(sk5(F,X,Y,A,T,E),decl(A),T)
& bearer(sk5(F,X,Y,A,T,E),X)
& subjection(sk5(F,X,Y,A,T,E))
& part_of(sk4(F,X,Y,A,T,E),sk3(F,X,Y,A,T,E))
& cnt(sk4(F,X,Y,A,T,E),decl(A),T)
& bearer(sk4(F,X,Y,A,T,E),Y)
& power(sk4(F,X,Y,A,T,E))
& founds_rem(E,sk3(F,X,Y,A,T,E),F) )
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ act(F,A)
| ~ aer(F,Y)
| ~ aee(F,X)
| ~ has_rem(F)
| ~ proh(F) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3,sk4,sk5])],[f1_nnf]) ).
cnf(c12,plain,
( cnt(sk4(X0,X1,X2,X3,X4,X5),decl(X3),X4)
| ~ activates(X5,X0)
| ~ tgt(X0,X4)
| ~ act(X0,X3)
| ~ aer(X0,X2)
| ~ aee(X0,X1)
| ~ has_rem(X0)
| ~ proh(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi12,axiom,
ifeq(proh(X0),true,ifeq(has_rem(X0),true,ifeq(aee(X0,X1),true,ifeq(aer(X0,X2),true,ifeq(act(X0,X3),true,ifeq(tgt(X0,X4),true,ifeq(activates(X5,X0),true,cnt(sk4(X0,X1,X2,X3,X4,X5),decl(X3),X4),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
fof(f14,axiom,
proh(f1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',proh_f1) ).
fof(f14_nnf,plain,
proh(f1),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c37,plain,
proh(f1),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(hi37,axiom,
proh(f1) = true,
inference(equality_encoding,[status(esa)],[c37]) ).
fof(f15,axiom,
has_rem(f1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rem_f1) ).
fof(f15_nnf,plain,
has_rem(f1),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c38,plain,
has_rem(f1),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(hi38,axiom,
has_rem(f1) = true,
inference(equality_encoding,[status(esa)],[c38]) ).
fof(f16,axiom,
aee(f1,marketplace),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aee_f1) ).
fof(f16_nnf,plain,
aee(f1,marketplace),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c39,plain,
aee(f1,marketplace),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(hi39,axiom,
aee(f1,marketplace) = true,
inference(equality_encoding,[status(esa)],[c39]) ).
fof(f17,axiom,
aer(f1,philharmonie),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aer_f1) ).
fof(f17_nnf,plain,
aer(f1,philharmonie),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c40,plain,
aer(f1,philharmonie),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(hi40,axiom,
aer(f1,philharmonie) = true,
inference(equality_encoding,[status(esa)],[c40]) ).
fof(f18,axiom,
act(f1,distrib),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',act_f1) ).
fof(f18_nnf,plain,
act(f1,distrib),
inference(nnf_transformation,[status(thm)],[f18]) ).
cnf(c41,plain,
act(f1,distrib),
inference(cnf_transformation,[status(esa)],[f18_nnf]) ).
cnf(hi41,axiom,
act(f1,distrib) = true,
inference(equality_encoding,[status(esa)],[c41]) ).
fof(f19,axiom,
tgt(f1,concert_ds),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tgt_f1) ).
fof(f19_nnf,plain,
tgt(f1,concert_ds),
inference(nnf_transformation,[status(thm)],[f19]) ).
cnf(c42,plain,
tgt(f1,concert_ds),
inference(cnf_transformation,[status(esa)],[f19_nnf]) ).
cnf(hi42,axiom,
tgt(f1,concert_ds) = true,
inference(equality_encoding,[status(esa)],[c42]) ).
fof(f20,axiom,
activates(e1,f1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',act_e1_f1) ).
fof(f20_nnf,plain,
activates(e1,f1),
inference(nnf_transformation,[status(thm)],[f20]) ).
cnf(c43,plain,
activates(e1,f1),
inference(cnf_transformation,[status(esa)],[f20_nnf]) ).
cnf(hi43,axiom,
activates(e1,f1) = true,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(t35,plain,
cnt(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) = true,
inference(hyper_resolution,[status(thm)],[hi12,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(t279,plain,
cnt(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) = true,
inference(orient,[status(thm)],[t35]) ).
cnf(t282,plain,
true = ifeq(founds_rem(e1,X1,f1),true,ifeq(power(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1)),true,ifeq(bearer(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie),true,ifeq(true,true,ifeq(part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),X1),true,ifeq(about_event(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,ifeq(subjection(X2),true,ifeq(bearer(X2,marketplace),true,ifeq(cnt(X2,decl(distrib),concert_ds),true,ifeq(part_of(X2,X1),true,ifeq(about_event(X2,e1),true,false,true),true),true),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t107,t279]) ).
cnf(c10,plain,
( power(sk4(X0,X1,X2,X3,X4,X5))
| ~ activates(X5,X0)
| ~ tgt(X0,X4)
| ~ act(X0,X3)
| ~ aer(X0,X2)
| ~ aee(X0,X1)
| ~ has_rem(X0)
| ~ proh(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi10,axiom,
ifeq(proh(X0),true,ifeq(has_rem(X0),true,ifeq(aee(X0,X1),true,ifeq(aer(X0,X2),true,ifeq(act(X0,X3),true,ifeq(tgt(X0,X4),true,ifeq(activates(X5,X0),true,power(sk4(X0,X1,X2,X3,X4,X5)),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t17,plain,
power(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(hyper_resolution,[status(thm)],[hi10,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(t313,plain,
power(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(orient,[status(thm)],[t17]) ).
cnf(t2405,plain,
true = ifeq(founds_rem(e1,X1,f1),true,ifeq(true,true,ifeq(bearer(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie),true,ifeq(true,true,ifeq(part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),X1),true,ifeq(about_event(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,ifeq(subjection(X2),true,ifeq(bearer(X2,marketplace),true,ifeq(cnt(X2,decl(distrib),concert_ds),true,ifeq(part_of(X2,X1),true,ifeq(about_event(X2,e1),true,false,true),true),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t282,t313]) ).
cnf(t14,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t78,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t14]) ).
cnf(t2406,plain,
true = ifeq(founds_rem(e1,X1,f1),true,ifeq(bearer(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie),true,ifeq(true,true,ifeq(part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),X1),true,ifeq(about_event(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,ifeq(subjection(X2),true,ifeq(bearer(X2,marketplace),true,ifeq(cnt(X2,decl(distrib),concert_ds),true,ifeq(part_of(X2,X1),true,ifeq(about_event(X2,e1),true,false,true),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t2405,t78]) ).
cnf(c11,plain,
( bearer(sk4(X0,X1,X2,X3,X4,X5),X2)
| ~ activates(X5,X0)
| ~ tgt(X0,X4)
| ~ act(X0,X3)
| ~ aer(X0,X2)
| ~ aee(X0,X1)
| ~ has_rem(X0)
| ~ proh(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi11,axiom,
ifeq(proh(X0),true,ifeq(has_rem(X0),true,ifeq(aee(X0,X1),true,ifeq(aer(X0,X2),true,ifeq(act(X0,X3),true,ifeq(tgt(X0,X4),true,ifeq(activates(X5,X0),true,bearer(sk4(X0,X1,X2,X3,X4,X5),X2),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t24,plain,
bearer(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie) = true,
inference(hyper_resolution,[status(thm)],[hi11,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(t233,plain,
bearer(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t2407,plain,
true = ifeq(founds_rem(e1,X1,f1),true,ifeq(true,true,ifeq(true,true,ifeq(part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),X1),true,ifeq(about_event(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,ifeq(subjection(X2),true,ifeq(bearer(X2,marketplace),true,ifeq(cnt(X2,decl(distrib),concert_ds),true,ifeq(part_of(X2,X1),true,ifeq(about_event(X2,e1),true,false,true),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t2406,t233]) ).
cnf(t2408,plain,
true = ifeq(founds_rem(e1,X1,f1),true,ifeq(true,true,ifeq(part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),X1),true,ifeq(about_event(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,ifeq(subjection(X2),true,ifeq(bearer(X2,marketplace),true,ifeq(cnt(X2,decl(distrib),concert_ds),true,ifeq(part_of(X2,X1),true,ifeq(about_event(X2,e1),true,false,true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t2407,t78]) ).
cnf(t2409,plain,
true = ifeq(founds_rem(e1,X1,f1),true,ifeq(part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),X1),true,ifeq(about_event(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,ifeq(subjection(X2),true,ifeq(bearer(X2,marketplace),true,ifeq(cnt(X2,decl(distrib),concert_ds),true,ifeq(part_of(X2,X1),true,ifeq(about_event(X2,e1),true,false,true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t2408,t78]) ).
cnf(c9,plain,
( founds_rem(X5,sk3(X0,X1,X2,X3,X4,X5),X0)
| ~ activates(X5,X0)
| ~ tgt(X0,X4)
| ~ act(X0,X3)
| ~ aer(X0,X2)
| ~ aee(X0,X1)
| ~ has_rem(X0)
| ~ proh(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi9,axiom,
ifeq(proh(X0),true,ifeq(has_rem(X0),true,ifeq(aee(X0,X1),true,ifeq(aer(X0,X2),true,ifeq(act(X0,X3),true,ifeq(tgt(X0,X4),true,ifeq(activates(X5,X0),true,founds_rem(X5,sk3(X0,X1,X2,X3,X4,X5),X0),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(h8,plain,
founds_rem(e1,sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1) = true,
inference(hyper_resolution,[status(thm)],[hi9,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(c13,plain,
( part_of(sk4(X0,X1,X2,X3,X4,X5),sk3(X0,X1,X2,X3,X4,X5))
| ~ activates(X5,X0)
| ~ tgt(X0,X4)
| ~ act(X0,X3)
| ~ aer(X0,X2)
| ~ aee(X0,X1)
| ~ has_rem(X0)
| ~ proh(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi13,axiom,
ifeq(proh(X0),true,ifeq(has_rem(X0),true,ifeq(aee(X0,X1),true,ifeq(aer(X0,X2),true,ifeq(act(X0,X3),true,ifeq(tgt(X0,X4),true,ifeq(activates(X5,X0),true,part_of(sk4(X0,X1,X2,X3,X4,X5),sk3(X0,X1,X2,X3,X4,X5)),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(h4,plain,
part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(hyper_resolution,[status(thm)],[hi13,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(h5,plain,
cnt(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) = true,
inference(hyper_resolution,[status(thm)],[hi12,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(h7,plain,
power(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(hyper_resolution,[status(thm)],[hi10,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
fof(f6,axiom,
! [Pw,A,T,Rho,E,R] :
( ( founds_rem(E,Rho,R)
& part_of(Pw,Rho)
& cnt(Pw,decl(A),T)
& power(Pw) )
=> about_event(Pw,E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_B2) ).
fof(f6_nnf,plain,
! [Pw,A,T,Rho,E,R] :
( about_event(Pw,E)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ cnt(Pw,decl(A),T)
| ~ power(Pw) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [Pw,A,T,Rho,E,R] :
( about_event(Pw,E)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ cnt(Pw,decl(A),T)
| ~ power(Pw) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c29,plain,
( about_event(X0,X4)
| ~ founds_rem(X4,X3,X5)
| ~ part_of(X0,X3)
| ~ cnt(X0,decl(X1),X2)
| ~ power(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi29,axiom,
ifeq(power(X0),true,ifeq(cnt(X0,decl(X1),X2),true,ifeq(part_of(X0,X3),true,ifeq(founds_rem(X4,X3,X5),true,about_event(X0,X4),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(t20,plain,
about_event(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) = true,
inference(hyper_resolution,[status(thm)],[hi29,h7,h5,h4,h8]) ).
cnf(t291,plain,
about_event(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t2410,plain,
true = ifeq(founds_rem(e1,X1,f1),true,ifeq(part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),X1),true,ifeq(true,true,ifeq(subjection(X2),true,ifeq(bearer(X2,marketplace),true,ifeq(cnt(X2,decl(distrib),concert_ds),true,ifeq(part_of(X2,X1),true,ifeq(about_event(X2,e1),true,false,true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t2409,t291]) ).
cnf(t2411,plain,
true = ifeq(founds_rem(e1,X1,f1),true,ifeq(part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),X1),true,ifeq(subjection(X2),true,ifeq(bearer(X2,marketplace),true,ifeq(cnt(X2,decl(distrib),concert_ds),true,ifeq(part_of(X2,X1),true,ifeq(about_event(X2,e1),true,false,true),true),true),true),true),true),true),
inference(step,[status(thm)],[t2410,t78]) ).
cnf(t1486,plain,
ifeq(founds_rem(e1,X1,f1),true,ifeq(part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),X1),true,ifeq(subjection(X2),true,ifeq(bearer(X2,marketplace),true,ifeq(cnt(X2,decl(distrib),concert_ds),true,ifeq(part_of(X2,X1),true,ifeq(about_event(X2,e1),true,false,true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t2411]) ).
cnf(t44,plain,
part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(hyper_resolution,[status(thm)],[hi13,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(t259,plain,
part_of(sk4(f1,marketplace,philharmonie,distrib,concert_ds,e1),sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(orient,[status(thm)],[t44]) ).
cnf(t1488,plain,
true = ifeq(founds_rem(e1,sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1),true,ifeq(true,true,ifeq(subjection(X1),true,ifeq(bearer(X1,marketplace),true,ifeq(cnt(X1,decl(distrib),concert_ds),true,ifeq(part_of(X1,sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1)),true,ifeq(about_event(X1,e1),true,false,true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t1486,t259]) ).
cnf(t29,plain,
founds_rem(e1,sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1) = true,
inference(hyper_resolution,[status(thm)],[hi9,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(t325,plain,
founds_rem(e1,sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(t2412,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(subjection(X1),true,ifeq(bearer(X1,marketplace),true,ifeq(cnt(X1,decl(distrib),concert_ds),true,ifeq(part_of(X1,sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1)),true,ifeq(about_event(X1,e1),true,false,true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1488,t325]) ).
cnf(t2413,plain,
true = ifeq(true,true,ifeq(subjection(X1),true,ifeq(bearer(X1,marketplace),true,ifeq(cnt(X1,decl(distrib),concert_ds),true,ifeq(part_of(X1,sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1)),true,ifeq(about_event(X1,e1),true,false,true),true),true),true),true),true),
inference(step,[status(thm)],[t2412,t78]) ).
cnf(t2414,plain,
true = ifeq(subjection(X1),true,ifeq(bearer(X1,marketplace),true,ifeq(cnt(X1,decl(distrib),concert_ds),true,ifeq(part_of(X1,sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1)),true,ifeq(about_event(X1,e1),true,false,true),true),true),true),true),
inference(step,[status(thm)],[t2413,t78]) ).
cnf(t1501,plain,
ifeq(subjection(X1),true,ifeq(bearer(X1,marketplace),true,ifeq(cnt(X1,decl(distrib),concert_ds),true,ifeq(part_of(X1,sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1)),true,ifeq(about_event(X1,e1),true,false,true),true),true),true),true) = true,
inference(orient,[status(thm)],[t2414]) ).
cnf(c17,plain,
( part_of(sk5(X0,X1,X2,X3,X4,X5),sk3(X0,X1,X2,X3,X4,X5))
| ~ activates(X5,X0)
| ~ tgt(X0,X4)
| ~ act(X0,X3)
| ~ aer(X0,X2)
| ~ aee(X0,X1)
| ~ has_rem(X0)
| ~ proh(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi17,axiom,
ifeq(proh(X0),true,ifeq(has_rem(X0),true,ifeq(aee(X0,X1),true,ifeq(aer(X0,X2),true,ifeq(act(X0,X3),true,ifeq(tgt(X0,X4),true,ifeq(activates(X5,X0),true,part_of(sk5(X0,X1,X2,X3,X4,X5),sk3(X0,X1,X2,X3,X4,X5)),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t45,plain,
part_of(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(hyper_resolution,[status(thm)],[hi17,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(t264,plain,
part_of(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(orient,[status(thm)],[t45]) ).
cnf(t1509,plain,
true = ifeq(subjection(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1)),true,ifeq(bearer(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace),true,ifeq(cnt(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),true,ifeq(true,true,ifeq(about_event(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,false,true),true),true),true),true),
inference(cp,[status(thm)],[t1501,t264]) ).
cnf(c14,plain,
( subjection(sk5(X0,X1,X2,X3,X4,X5))
| ~ activates(X5,X0)
| ~ tgt(X0,X4)
| ~ act(X0,X3)
| ~ aer(X0,X2)
| ~ aee(X0,X1)
| ~ has_rem(X0)
| ~ proh(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi14,axiom,
ifeq(proh(X0),true,ifeq(has_rem(X0),true,ifeq(aee(X0,X1),true,ifeq(aer(X0,X2),true,ifeq(act(X0,X3),true,ifeq(tgt(X0,X4),true,ifeq(activates(X5,X0),true,subjection(sk5(X0,X1,X2,X3,X4,X5)),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t19,plain,
subjection(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(hyper_resolution,[status(thm)],[hi14,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(t319,plain,
subjection(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(orient,[status(thm)],[t19]) ).
cnf(t2422,plain,
true = ifeq(true,true,ifeq(bearer(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace),true,ifeq(cnt(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),true,ifeq(true,true,ifeq(about_event(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,false,true),true),true),true),true),
inference(step,[status(thm)],[t1509,t319]) ).
cnf(t2423,plain,
true = ifeq(bearer(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace),true,ifeq(cnt(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),true,ifeq(true,true,ifeq(about_event(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,false,true),true),true),true),
inference(step,[status(thm)],[t2422,t78]) ).
cnf(c15,plain,
( bearer(sk5(X0,X1,X2,X3,X4,X5),X1)
| ~ activates(X5,X0)
| ~ tgt(X0,X4)
| ~ act(X0,X3)
| ~ aer(X0,X2)
| ~ aee(X0,X1)
| ~ has_rem(X0)
| ~ proh(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi15,axiom,
ifeq(proh(X0),true,ifeq(has_rem(X0),true,ifeq(aee(X0,X1),true,ifeq(aer(X0,X2),true,ifeq(act(X0,X3),true,ifeq(tgt(X0,X4),true,ifeq(activates(X5,X0),true,bearer(sk5(X0,X1,X2,X3,X4,X5),X1),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t25,plain,
bearer(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace) = true,
inference(hyper_resolution,[status(thm)],[hi15,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(t236,plain,
bearer(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace) = true,
inference(orient,[status(thm)],[t25]) ).
cnf(t2424,plain,
true = ifeq(true,true,ifeq(cnt(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),true,ifeq(true,true,ifeq(about_event(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,false,true),true),true),true),
inference(step,[status(thm)],[t2423,t236]) ).
cnf(t2425,plain,
true = ifeq(cnt(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),true,ifeq(true,true,ifeq(about_event(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,false,true),true),true),
inference(step,[status(thm)],[t2424,t78]) ).
cnf(c16,plain,
( cnt(sk5(X0,X1,X2,X3,X4,X5),decl(X3),X4)
| ~ activates(X5,X0)
| ~ tgt(X0,X4)
| ~ act(X0,X3)
| ~ aer(X0,X2)
| ~ aee(X0,X1)
| ~ has_rem(X0)
| ~ proh(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi16,axiom,
ifeq(proh(X0),true,ifeq(has_rem(X0),true,ifeq(aee(X0,X1),true,ifeq(aer(X0,X2),true,ifeq(act(X0,X3),true,ifeq(tgt(X0,X4),true,ifeq(activates(X5,X0),true,cnt(sk5(X0,X1,X2,X3,X4,X5),decl(X3),X4),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t36,plain,
cnt(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) = true,
inference(hyper_resolution,[status(thm)],[hi16,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(t284,plain,
cnt(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) = true,
inference(orient,[status(thm)],[t36]) ).
cnf(t2426,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(about_event(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,false,true),true),true),
inference(step,[status(thm)],[t2425,t284]) ).
cnf(t2427,plain,
true = ifeq(true,true,ifeq(about_event(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,false,true),true),
inference(step,[status(thm)],[t2426,t78]) ).
cnf(t2428,plain,
true = ifeq(about_event(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),true,false,true),
inference(step,[status(thm)],[t2427,t78]) ).
cnf(h0,plain,
part_of(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),sk3(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(hyper_resolution,[status(thm)],[hi17,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(h1,plain,
cnt(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) = true,
inference(hyper_resolution,[status(thm)],[hi16,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
cnf(h3,plain,
subjection(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1)) = true,
inference(hyper_resolution,[status(thm)],[hi14,hi37,hi38,hi39,hi40,hi41,hi42,hi43]) ).
fof(f7,axiom,
! [S,A,T,Rho,E,R] :
( ( founds_rem(E,Rho,R)
& part_of(S,Rho)
& cnt(S,decl(A),T)
& subjection(S) )
=> about_event(S,E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_B3) ).
fof(f7_nnf,plain,
! [S,A,T,Rho,E,R] :
( about_event(S,E)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ cnt(S,decl(A),T)
| ~ subjection(S) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [S,A,T,Rho,E,R] :
( about_event(S,E)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ cnt(S,decl(A),T)
| ~ subjection(S) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c30,plain,
( about_event(X0,X4)
| ~ founds_rem(X4,X3,X5)
| ~ part_of(X0,X3)
| ~ cnt(X0,decl(X1),X2)
| ~ subjection(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi30,axiom,
ifeq(subjection(X0),true,ifeq(cnt(X0,decl(X1),X2),true,ifeq(part_of(X0,X3),true,ifeq(founds_rem(X4,X3,X5),true,about_event(X0,X4),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(t21,plain,
about_event(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) = true,
inference(hyper_resolution,[status(thm)],[hi30,h3,h1,h0,h8]) ).
cnf(t296,plain,
about_event(sk5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) = true,
inference(orient,[status(thm)],[t21]) ).
cnf(t2429,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t2428,t296]) ).
cnf(t2430,plain,
true = false,
inference(step,[status(thm)],[t2429,t78]) ).
cnf(t1526,plain,
false = true,
inference(orient,[status(thm)],[t2430]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c45]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1526]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT113+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n005.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 : Thu Sep 24 01:25:17 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 61.42/8.32 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.42/8.32 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------