%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT113+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:25:37 PM UTC 2026
% Result : Theorem 0.14s 0.40s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 34
% Syntax : Number of formulae : 174 ( 19 unt; 23 def)
% Number of atoms : 756 ( 0 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 1076 ( 494 ~; 492 |; 64 &)
% ( 23 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 38 ( 37 usr; 24 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-6 aty)
% Number of variables : 332 ( 317 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,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') ).
fof(f7,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') ).
fof(f8,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') ).
fof(f15,axiom,
proh(f1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
has_rem(f1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
aee(f1,marketplace),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
aer(f1,philharmonie),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
act(f1,distrib),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
tgt(f1,concert_ds),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
activates(e1,f1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,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') ).
fof(f24,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)],[f23]) ).
fof(f37,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(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f38,plain,
! [F,X,Y,A,T,E] :
( ? [RhoR,S] :
( part_of(S,RhoR)
& cnt(S,decl(A),T)
& bearer(S,X)
& subjection(S)
& ? [Pw] :
( 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(miniscoping,[status(thm)],[f37]) ).
fof(f39,plain,
! [F,X,Y,A,T,E] :
( ( part_of(sK4_skl(E,T,A,Y,X,F),sK3_skl(E,T,A,Y,X,F))
& cnt(sK4_skl(E,T,A,Y,X,F),decl(A),T)
& bearer(sK4_skl(E,T,A,Y,X,F),X)
& subjection(sK4_skl(E,T,A,Y,X,F))
& part_of(sK5_skl(E,T,A,Y,X,F),sK3_skl(E,T,A,Y,X,F))
& cnt(sK5_skl(E,T,A,Y,X,F),decl(A),T)
& bearer(sK5_skl(E,T,A,Y,X,F),Y)
& power(sK5_skl(E,T,A,Y,X,F))
& founds_rem(E,sK3_skl(E,T,A,Y,X,F),F) )
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ act(F,A)
| ~ aer(F,Y)
| ~ aee(F,X)
| ~ has_rem(F)
| ~ proh(F) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(RhoR,sK3_skl(E,T,A,Y,X,F)),skolemize(S,sK4_skl(E,T,A,Y,X,F)),skolemize(Pw,sK5_skl(E,T,A,Y,X,F))],[f38]) ).
fof(f40,plain,
! [X0,X1,X2,X3,X4,X5] :
( founds_rem(X5,sK3_skl(X5,X4,X3,X2,X1,X0),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(thm)],[f39]) ).
fof(f41,plain,
! [X0,X1,X2,X3,X4,X5] :
( power(sK5_skl(X5,X4,X3,X2,X1,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(thm)],[f39]) ).
fof(f42,plain,
! [X0,X1,X2,X3,X4,X5] :
( bearer(sK5_skl(X5,X4,X3,X2,X1,X0),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(thm)],[f39]) ).
fof(f43,plain,
! [X0,X1,X2,X3,X4,X5] :
( cnt(sK5_skl(X5,X4,X3,X2,X1,X0),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(thm)],[f39]) ).
fof(f44,plain,
! [X0,X1,X2,X3,X4,X5] :
( part_of(sK5_skl(X5,X4,X3,X2,X1,X0),sK3_skl(X5,X4,X3,X2,X1,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(thm)],[f39]) ).
fof(f45,plain,
! [X0,X1,X2,X3,X4,X5] :
( subjection(sK4_skl(X5,X4,X3,X2,X1,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(thm)],[f39]) ).
fof(f46,plain,
! [X0,X1,X2,X3,X4,X5] :
( bearer(sK4_skl(X5,X4,X3,X2,X1,X0),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(thm)],[f39]) ).
fof(f47,plain,
! [X0,X1,X2,X3,X4,X5] :
( cnt(sK4_skl(X5,X4,X3,X2,X1,X0),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(thm)],[f39]) ).
fof(f48,plain,
! [X0,X1,X2,X3,X4,X5] :
( part_of(sK4_skl(X5,X4,X3,X2,X1,X0),sK3_skl(X5,X4,X3,X2,X1,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(thm)],[f39]) ).
fof(f70,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(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f71,plain,
! [Pw,E] :
( about_event(Pw,E)
| ! [Rho] :
( ! [R] : ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ! [A,T] : ~ cnt(Pw,decl(A),T)
| ~ power(Pw) ) ),
inference(miniscoping,[status(thm)],[f70]) ).
fof(f72,plain,
! [X0,X1,X2,X3,X4,X5] :
( about_event(X0,X4)
| ~ founds_rem(X4,X3,X5)
| ~ part_of(X0,X3)
| ~ cnt(X0,decl(X1),X2)
| ~ power(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,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(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f74,plain,
! [S,E] :
( about_event(S,E)
| ! [Rho] :
( ! [R] : ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ! [A,T] : ~ cnt(S,decl(A),T)
| ~ subjection(S) ) ),
inference(miniscoping,[status(thm)],[f73]) ).
fof(f75,plain,
! [X0,X1,X2,X3,X4,X5] :
( about_event(X0,X4)
| ~ founds_rem(X4,X3,X5)
| ~ part_of(X0,X3)
| ~ cnt(X0,decl(X1),X2)
| ~ subjection(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f82,plain,
proh(f1),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f83,plain,
has_rem(f1),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f84,plain,
aee(f1,marketplace),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f85,plain,
aer(f1,philharmonie),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f86,plain,
act(f1,distrib),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f87,plain,
tgt(f1,concert_ds),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f88,plain,
activates(e1,f1),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f90,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(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f91,plain,
! [S] :
( ~ about_event(S,e1)
| ! [RhoR] :
( ~ part_of(S,RhoR)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ bearer(S,marketplace)
| ~ subjection(S)
| ! [Pw] :
( ~ 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(miniscoping,[status(thm)],[f90]) ).
fof(f92,plain,
! [X0,X1,X2] :
( ~ 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(thm)],[f91]) ).
fof(f95,definition,
( sQ0_spl
<=> proh(f1) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f97,plain,
( sQ0_spl
| ~ proh(f1) ),
inference(component_clause,[status(thm)],[f95]) ).
fof(f106,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f97,f82]) ).
fof(f107,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f106]) ).
fof(f139,definition,
( sQ9_spl
<=> has_rem(f1) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f141,plain,
( sQ9_spl
| ~ has_rem(f1) ),
inference(component_clause,[status(thm)],[f139]) ).
fof(f146,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f141,f83]) ).
fof(f147,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f146]) ).
fof(f149,definition,
( sQ11_spl
<=> tgt(f1,concert_ds) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f151,plain,
( sQ11_spl
| ~ tgt(f1,concert_ds) ),
inference(component_clause,[status(thm)],[f149]) ).
fof(f152,definition,
( sQ12_spl
<=> aee(f1,marketplace) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f154,plain,
( sQ12_spl
| ~ aee(f1,marketplace) ),
inference(component_clause,[status(thm)],[f152]) ).
fof(f166,plain,
! [X0,X1,X2,X3] :
( founds_rem(X3,sK3_skl(X3,X2,X1,X0,marketplace,f1),f1)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[f40,f84]) ).
fof(f167,definition,
! [X0,X1,X2,X3] :
( sQ15_spl
<=> ( founds_rem(X3,sK3_skl(X3,X2,X1,X0,marketplace,f1),f1)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f168,plain,
! [X0,X1,X2,X3] :
( ~ sQ15_spl
| founds_rem(X3,sK3_skl(X3,X2,X1,X0,marketplace,f1),f1)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ),
inference(component_clause,[status(thm)],[f167]) ).
fof(f170,plain,
( sQ15_spl
| ~ sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f166,f95,f139,f167]) ).
fof(f173,plain,
! [X0,X1,X2,X3] :
( power(sK5_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[f41,f84]) ).
fof(f174,definition,
! [X0,X1,X2,X3] :
( sQ16_spl
<=> ( power(sK5_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| power(sK5_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ),
inference(component_clause,[status(thm)],[f174]) ).
fof(f177,plain,
( sQ16_spl
| ~ sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f173,f95,f139,f174]) ).
fof(f181,plain,
! [X0,X1,X2,X3] :
( bearer(sK5_skl(X3,X2,X1,X0,marketplace,f1),X0)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[f42,f84]) ).
fof(f182,definition,
! [X0,X1,X2,X3] :
( sQ17_spl
<=> ( bearer(sK5_skl(X3,X2,X1,X0,marketplace,f1),X0)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f183,plain,
! [X0,X1,X2,X3] :
( ~ sQ17_spl
| bearer(sK5_skl(X3,X2,X1,X0,marketplace,f1),X0)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ),
inference(component_clause,[status(thm)],[f182]) ).
fof(f185,plain,
( sQ17_spl
| ~ sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f181,f95,f139,f182]) ).
fof(f187,plain,
! [X0,X1,X2] :
( ~ sQ16_spl
| power(sK5_skl(X2,X1,X0,philharmonie,marketplace,f1))
| ~ activates(X2,f1)
| ~ tgt(f1,X1)
| ~ act(f1,X0) ),
inference(resolution,[status(thm)],[f175,f85]) ).
fof(f188,plain,
! [X0,X1,X2,X3] :
( cnt(sK5_skl(X3,X2,X1,X0,marketplace,f1),decl(X1),X2)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[f43,f84]) ).
fof(f189,definition,
! [X0,X1,X2,X3] :
( sQ18_spl
<=> ( cnt(sK5_skl(X3,X2,X1,X0,marketplace,f1),decl(X1),X2)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f190,plain,
! [X0,X1,X2,X3] :
( ~ sQ18_spl
| cnt(sK5_skl(X3,X2,X1,X0,marketplace,f1),decl(X1),X2)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ),
inference(component_clause,[status(thm)],[f189]) ).
fof(f192,plain,
( sQ18_spl
| ~ sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f188,f95,f139,f189]) ).
fof(f193,plain,
! [X0,X1] :
( ~ sQ16_spl
| power(sK5_skl(X1,X0,distrib,philharmonie,marketplace,f1))
| ~ activates(X1,f1)
| ~ tgt(f1,X0) ),
inference(resolution,[status(thm)],[f187,f86]) ).
fof(f194,plain,
! [X0] :
( ~ sQ16_spl
| power(sK5_skl(X0,concert_ds,distrib,philharmonie,marketplace,f1))
| ~ activates(X0,f1) ),
inference(resolution,[status(thm)],[f193,f87]) ).
fof(f195,plain,
( ~ sQ16_spl
| power(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1)) ),
inference(resolution,[status(thm)],[f194,f88]) ).
fof(f196,plain,
! [X0,X1,X2,X3] :
( part_of(sK5_skl(X3,X2,X1,X0,marketplace,f1),sK3_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[f44,f84]) ).
fof(f197,definition,
! [X0,X1,X2,X3] :
( sQ19_spl
<=> ( part_of(sK5_skl(X3,X2,X1,X0,marketplace,f1),sK3_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f198,plain,
! [X0,X1,X2,X3] :
( ~ sQ19_spl
| part_of(sK5_skl(X3,X2,X1,X0,marketplace,f1),sK3_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ),
inference(component_clause,[status(thm)],[f197]) ).
fof(f200,plain,
( sQ19_spl
| ~ sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f196,f95,f139,f197]) ).
fof(f203,plain,
! [X0,X1,X2,X3] :
( subjection(sK4_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[f45,f84]) ).
fof(f204,definition,
! [X0,X1,X2,X3] :
( sQ20_spl
<=> ( subjection(sK4_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f205,plain,
! [X0,X1,X2,X3] :
( ~ sQ20_spl
| subjection(sK4_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ),
inference(component_clause,[status(thm)],[f204]) ).
fof(f207,plain,
( sQ20_spl
| ~ sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f203,f95,f139,f204]) ).
fof(f210,plain,
! [X0,X1,X2,X3] :
( bearer(sK4_skl(X3,X2,X1,X0,marketplace,f1),marketplace)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[f46,f84]) ).
fof(f211,definition,
! [X0,X1,X2,X3] :
( sQ21_spl
<=> ( bearer(sK4_skl(X3,X2,X1,X0,marketplace,f1),marketplace)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f212,plain,
! [X0,X1,X2,X3] :
( ~ sQ21_spl
| bearer(sK4_skl(X3,X2,X1,X0,marketplace,f1),marketplace)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ),
inference(component_clause,[status(thm)],[f211]) ).
fof(f214,plain,
( sQ21_spl
| ~ sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f210,f95,f139,f211]) ).
fof(f215,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| subjection(sK4_skl(X2,X1,X0,philharmonie,marketplace,f1))
| ~ activates(X2,f1)
| ~ tgt(f1,X1)
| ~ act(f1,X0) ),
inference(resolution,[status(thm)],[f205,f85]) ).
fof(f216,plain,
! [X0,X1] :
( ~ sQ20_spl
| subjection(sK4_skl(X1,X0,distrib,philharmonie,marketplace,f1))
| ~ activates(X1,f1)
| ~ tgt(f1,X0) ),
inference(resolution,[status(thm)],[f215,f86]) ).
fof(f217,plain,
! [X0] :
( ~ sQ20_spl
| subjection(sK4_skl(X0,concert_ds,distrib,philharmonie,marketplace,f1))
| ~ activates(X0,f1) ),
inference(resolution,[status(thm)],[f216,f87]) ).
fof(f218,plain,
! [X0,X1,X2,X3] :
( cnt(sK4_skl(X3,X2,X1,X0,marketplace,f1),decl(X1),X2)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[f47,f84]) ).
fof(f219,definition,
! [X0,X1,X2,X3] :
( sQ22_spl
<=> ( cnt(sK4_skl(X3,X2,X1,X0,marketplace,f1),decl(X1),X2)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f220,plain,
! [X0,X1,X2,X3] :
( ~ sQ22_spl
| cnt(sK4_skl(X3,X2,X1,X0,marketplace,f1),decl(X1),X2)
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ),
inference(component_clause,[status(thm)],[f219]) ).
fof(f222,plain,
( sQ22_spl
| ~ sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f218,f95,f139,f219]) ).
fof(f223,plain,
( ~ sQ20_spl
| subjection(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1)) ),
inference(resolution,[status(thm)],[f217,f88]) ).
fof(f224,plain,
! [X0,X1,X2] :
( ~ sQ17_spl
| bearer(sK5_skl(X2,X1,X0,philharmonie,marketplace,f1),philharmonie)
| ~ activates(X2,f1)
| ~ tgt(f1,X1)
| ~ act(f1,X0) ),
inference(resolution,[status(thm)],[f183,f85]) ).
fof(f225,plain,
! [X0,X1,X2,X3] :
( part_of(sK4_skl(X3,X2,X1,X0,marketplace,f1),sK3_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[f48,f84]) ).
fof(f226,definition,
! [X0,X1,X2,X3] :
( sQ23_spl
<=> ( part_of(sK4_skl(X3,X2,X1,X0,marketplace,f1),sK3_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f227,plain,
! [X0,X1,X2,X3] :
( ~ sQ23_spl
| part_of(sK4_skl(X3,X2,X1,X0,marketplace,f1),sK3_skl(X3,X2,X1,X0,marketplace,f1))
| ~ activates(X3,f1)
| ~ tgt(f1,X2)
| ~ act(f1,X1)
| ~ aer(f1,X0) ),
inference(component_clause,[status(thm)],[f226]) ).
fof(f229,plain,
( sQ23_spl
| ~ sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f225,f95,f139,f226]) ).
fof(f230,plain,
! [X0,X1] :
( ~ sQ17_spl
| bearer(sK5_skl(X1,X0,distrib,philharmonie,marketplace,f1),philharmonie)
| ~ activates(X1,f1)
| ~ tgt(f1,X0) ),
inference(resolution,[status(thm)],[f224,f86]) ).
fof(f231,plain,
! [X0] :
( ~ sQ17_spl
| bearer(sK5_skl(X0,concert_ds,distrib,philharmonie,marketplace,f1),philharmonie)
| ~ activates(X0,f1) ),
inference(resolution,[status(thm)],[f230,f87]) ).
fof(f232,plain,
( ~ sQ17_spl
| bearer(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),philharmonie) ),
inference(resolution,[status(thm)],[f231,f88]) ).
fof(f243,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f154,f84]) ).
fof(f244,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f243]) ).
fof(f245,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f151,f87]) ).
fof(f246,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f245]) ).
fof(f247,plain,
! [X0,X1,X2] :
( ~ 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(forward_subsumption_resolution,[status(thm)],[f92,f75]) ).
fof(f269,plain,
! [X0,X1,X2] :
( ~ sQ21_spl
| bearer(sK4_skl(X2,X1,X0,philharmonie,marketplace,f1),marketplace)
| ~ activates(X2,f1)
| ~ tgt(f1,X1)
| ~ act(f1,X0) ),
inference(resolution,[status(thm)],[f212,f85]) ).
fof(f270,plain,
! [X0,X1] :
( ~ sQ21_spl
| bearer(sK4_skl(X1,X0,distrib,philharmonie,marketplace,f1),marketplace)
| ~ activates(X1,f1)
| ~ tgt(f1,X0) ),
inference(resolution,[status(thm)],[f269,f86]) ).
fof(f271,plain,
! [X0,X1,X2] :
( ~ sQ15_spl
| founds_rem(X2,sK3_skl(X2,X1,X0,philharmonie,marketplace,f1),f1)
| ~ activates(X2,f1)
| ~ tgt(f1,X1)
| ~ act(f1,X0) ),
inference(resolution,[status(thm)],[f168,f85]) ).
fof(f272,plain,
! [X0] :
( ~ sQ21_spl
| bearer(sK4_skl(X0,concert_ds,distrib,philharmonie,marketplace,f1),marketplace)
| ~ activates(X0,f1) ),
inference(resolution,[status(thm)],[f270,f87]) ).
fof(f273,plain,
( ~ sQ21_spl
| bearer(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),marketplace) ),
inference(resolution,[status(thm)],[f272,f88]) ).
fof(f274,plain,
! [X0,X1,X2] :
( ~ sQ18_spl
| cnt(sK5_skl(X2,X1,X0,philharmonie,marketplace,f1),decl(X0),X1)
| ~ activates(X2,f1)
| ~ tgt(f1,X1)
| ~ act(f1,X0) ),
inference(resolution,[status(thm)],[f190,f85]) ).
fof(f275,plain,
! [X0,X1] :
( ~ sQ15_spl
| founds_rem(X1,sK3_skl(X1,X0,distrib,philharmonie,marketplace,f1),f1)
| ~ activates(X1,f1)
| ~ tgt(f1,X0) ),
inference(resolution,[status(thm)],[f271,f86]) ).
fof(f276,plain,
! [X0] :
( ~ sQ15_spl
| founds_rem(X0,sK3_skl(X0,concert_ds,distrib,philharmonie,marketplace,f1),f1)
| ~ activates(X0,f1) ),
inference(resolution,[status(thm)],[f275,f87]) ).
fof(f277,plain,
( ~ sQ15_spl
| founds_rem(e1,sK3_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),f1) ),
inference(resolution,[status(thm)],[f276,f88]) ).
fof(f278,plain,
! [X0,X1,X2] :
( ~ sQ19_spl
| part_of(sK5_skl(X2,X1,X0,philharmonie,marketplace,f1),sK3_skl(X2,X1,X0,philharmonie,marketplace,f1))
| ~ activates(X2,f1)
| ~ tgt(f1,X1)
| ~ act(f1,X0) ),
inference(resolution,[status(thm)],[f198,f85]) ).
fof(f279,plain,
! [X0,X1] :
( ~ sQ15_spl
| ~ part_of(X1,sK3_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1))
| ~ cnt(X1,decl(distrib),concert_ds)
| ~ bearer(X1,marketplace)
| ~ subjection(X1)
| ~ about_event(X0,e1)
| ~ part_of(X0,sK3_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1))
| ~ cnt(X0,decl(distrib),concert_ds)
| ~ bearer(X0,philharmonie)
| ~ power(X0) ),
inference(resolution,[status(thm)],[f277,f247]) ).
fof(f280,definition,
! [X0] :
( sQ26_spl
<=> ( ~ about_event(X0,e1)
| ~ part_of(X0,sK3_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1))
| ~ cnt(X0,decl(distrib),concert_ds)
| ~ bearer(X0,philharmonie)
| ~ power(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f281,plain,
! [X0] :
( ~ sQ26_spl
| ~ about_event(X0,e1)
| ~ part_of(X0,sK3_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1))
| ~ cnt(X0,decl(distrib),concert_ds)
| ~ bearer(X0,philharmonie)
| ~ power(X0) ),
inference(component_clause,[status(thm)],[f280]) ).
fof(f283,definition,
! [X1] :
( sQ27_spl
<=> ( ~ part_of(X1,sK3_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1))
| ~ cnt(X1,decl(distrib),concert_ds)
| ~ bearer(X1,marketplace)
| ~ subjection(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f284,plain,
! [X0] :
( ~ sQ27_spl
| ~ part_of(X0,sK3_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1))
| ~ cnt(X0,decl(distrib),concert_ds)
| ~ bearer(X0,marketplace)
| ~ subjection(X0) ),
inference(component_clause,[status(thm)],[f283]) ).
fof(f286,plain,
( ~ sQ15_spl
| sQ27_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f279,f280,f283,f167]) ).
fof(f287,plain,
! [X0,X1] :
( ~ sQ18_spl
| cnt(sK5_skl(X1,X0,distrib,philharmonie,marketplace,f1),decl(distrib),X0)
| ~ activates(X1,f1)
| ~ tgt(f1,X0) ),
inference(resolution,[status(thm)],[f274,f86]) ).
fof(f288,plain,
! [X0] :
( ~ sQ18_spl
| cnt(sK5_skl(X0,concert_ds,distrib,philharmonie,marketplace,f1),decl(distrib),concert_ds)
| ~ activates(X0,f1) ),
inference(resolution,[status(thm)],[f287,f87]) ).
fof(f289,plain,
! [X0,X1,X2] :
( ~ sQ22_spl
| cnt(sK4_skl(X2,X1,X0,philharmonie,marketplace,f1),decl(X0),X1)
| ~ activates(X2,f1)
| ~ tgt(f1,X1)
| ~ act(f1,X0) ),
inference(resolution,[status(thm)],[f220,f85]) ).
fof(f290,plain,
( ~ sQ18_spl
| cnt(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),decl(distrib),concert_ds) ),
inference(resolution,[status(thm)],[f288,f88]) ).
fof(f292,plain,
! [X0,X1,X2] :
( ~ sQ18_spl
| about_event(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),X1)
| ~ founds_rem(X1,X0,X2)
| ~ part_of(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),X0)
| ~ power(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1)) ),
inference(resolution,[status(thm)],[f290,f72]) ).
fof(f296,definition,
! [X0,X1,X2] :
( sQ29_spl
<=> ( about_event(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),X1)
| ~ founds_rem(X1,X0,X2)
| ~ part_of(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f297,plain,
! [X0,X1,X2] :
( ~ sQ29_spl
| about_event(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),X1)
| ~ founds_rem(X1,X0,X2)
| ~ part_of(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),X0) ),
inference(component_clause,[status(thm)],[f296]) ).
fof(f300,definition,
( sQ30_spl
<=> power(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f302,plain,
( sQ30_spl
| ~ power(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1)) ),
inference(component_clause,[status(thm)],[f300]) ).
fof(f303,plain,
( ~ sQ18_spl
| sQ29_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f292,f300,f296,f189]) ).
fof(f304,plain,
! [X0,X1] :
( ~ sQ22_spl
| cnt(sK4_skl(X1,X0,distrib,philharmonie,marketplace,f1),decl(distrib),X0)
| ~ activates(X1,f1)
| ~ tgt(f1,X0) ),
inference(resolution,[status(thm)],[f289,f86]) ).
fof(f305,plain,
! [X0,X1,X2] :
( ~ sQ23_spl
| part_of(sK4_skl(X2,X1,X0,philharmonie,marketplace,f1),sK3_skl(X2,X1,X0,philharmonie,marketplace,f1))
| ~ activates(X2,f1)
| ~ tgt(f1,X1)
| ~ act(f1,X0) ),
inference(resolution,[status(thm)],[f227,f85]) ).
fof(f306,plain,
! [X0] :
( ~ sQ22_spl
| cnt(sK4_skl(X0,concert_ds,distrib,philharmonie,marketplace,f1),decl(distrib),concert_ds)
| ~ activates(X0,f1) ),
inference(resolution,[status(thm)],[f304,f87]) ).
fof(f307,plain,
( ~ sQ22_spl
| cnt(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),decl(distrib),concert_ds) ),
inference(resolution,[status(thm)],[f306,f88]) ).
fof(f310,definition,
( sQ31_spl
<=> subjection(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f312,plain,
( sQ31_spl
| ~ subjection(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1)) ),
inference(component_clause,[status(thm)],[f310]) ).
fof(f333,plain,
! [X0,X1] :
( ~ sQ19_spl
| part_of(sK5_skl(X1,X0,distrib,philharmonie,marketplace,f1),sK3_skl(X1,X0,distrib,philharmonie,marketplace,f1))
| ~ activates(X1,f1)
| ~ tgt(f1,X0) ),
inference(resolution,[status(thm)],[f278,f86]) ).
fof(f334,plain,
! [X0] :
( ~ sQ19_spl
| part_of(sK5_skl(X0,concert_ds,distrib,philharmonie,marketplace,f1),sK3_skl(X0,concert_ds,distrib,philharmonie,marketplace,f1))
| ~ activates(X0,f1) ),
inference(resolution,[status(thm)],[f333,f87]) ).
fof(f335,plain,
( ~ sQ19_spl
| part_of(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),sK3_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1)) ),
inference(resolution,[status(thm)],[f334,f88]) ).
fof(f336,plain,
! [X0,X1] :
( ~ sQ23_spl
| part_of(sK4_skl(X1,X0,distrib,philharmonie,marketplace,f1),sK3_skl(X1,X0,distrib,philharmonie,marketplace,f1))
| ~ activates(X1,f1)
| ~ tgt(f1,X0) ),
inference(resolution,[status(thm)],[f305,f86]) ).
fof(f337,plain,
! [X0] :
( ~ sQ23_spl
| part_of(sK4_skl(X0,concert_ds,distrib,philharmonie,marketplace,f1),sK3_skl(X0,concert_ds,distrib,philharmonie,marketplace,f1))
| ~ activates(X0,f1) ),
inference(resolution,[status(thm)],[f336,f87]) ).
fof(f338,plain,
( ~ sQ23_spl
| part_of(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),sK3_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1)) ),
inference(resolution,[status(thm)],[f337,f88]) ).
fof(f340,plain,
( ~ sQ19_spl
| ~ sQ26_spl
| ~ about_event(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),e1)
| ~ cnt(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),decl(distrib),concert_ds)
| ~ bearer(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),philharmonie)
| ~ power(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1)) ),
inference(resolution,[status(thm)],[f281,f335]) ).
fof(f344,definition,
( sQ35_spl
<=> cnt(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),decl(distrib),concert_ds) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f346,plain,
( sQ35_spl
| ~ cnt(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),decl(distrib),concert_ds) ),
inference(component_clause,[status(thm)],[f344]) ).
fof(f351,definition,
( sQ37_spl
<=> bearer(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),philharmonie) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f353,plain,
( sQ37_spl
| ~ bearer(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),philharmonie) ),
inference(component_clause,[status(thm)],[f351]) ).
fof(f354,definition,
( sQ38_spl
<=> cnt(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),decl(distrib),concert_ds) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f356,plain,
( sQ38_spl
| ~ cnt(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),decl(distrib),concert_ds) ),
inference(component_clause,[status(thm)],[f354]) ).
fof(f357,definition,
( sQ39_spl
<=> about_event(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),e1) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f359,plain,
( sQ39_spl
| ~ about_event(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),e1) ),
inference(component_clause,[status(thm)],[f357]) ).
fof(f360,plain,
( ~ sQ19_spl
| ~ sQ26_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f340,f300,f351,f354,f357,f280,f197]) ).
fof(f361,plain,
( sQ30_spl
| ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f302,f195]) ).
fof(f362,plain,
( sQ30_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f361]) ).
fof(f363,plain,
! [X0,X1] :
( ~ sQ19_spl
| ~ sQ29_spl
| about_event(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),X0)
| ~ founds_rem(X0,sK3_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),X1) ),
inference(resolution,[status(thm)],[f297,f335]) ).
fof(f364,plain,
( ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ29_spl
| about_event(sK5_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),e1) ),
inference(resolution,[status(thm)],[f363,f277]) ).
fof(f365,plain,
( ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ29_spl
| sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f364,f359]) ).
fof(f366,plain,
( ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ29_spl
| sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f365]) ).
fof(f367,plain,
( sQ37_spl
| ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f353,f232]) ).
fof(f368,plain,
( sQ37_spl
| ~ sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f367]) ).
fof(f369,plain,
( sQ38_spl
| ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f356,f290]) ).
fof(f370,plain,
( sQ38_spl
| ~ sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f369]) ).
fof(f371,plain,
( ~ sQ23_spl
| ~ sQ27_spl
| ~ cnt(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),decl(distrib),concert_ds)
| ~ bearer(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),marketplace)
| ~ subjection(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1)) ),
inference(resolution,[status(thm)],[f284,f338]) ).
fof(f373,definition,
( sQ40_spl
<=> bearer(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),marketplace) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f375,plain,
( sQ40_spl
| ~ bearer(sK4_skl(e1,concert_ds,distrib,philharmonie,marketplace,f1),marketplace) ),
inference(component_clause,[status(thm)],[f373]) ).
fof(f376,plain,
( ~ sQ23_spl
| ~ sQ27_spl
| ~ sQ35_spl
| ~ sQ40_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f371,f310,f373,f344,f283,f226]) ).
fof(f381,plain,
( sQ31_spl
| ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f312,f223]) ).
fof(f382,plain,
( sQ31_spl
| ~ sQ20_spl ),
inference(contradiction_clause,[status(thm)],[f381]) ).
fof(f383,plain,
( sQ35_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f346,f307]) ).
fof(f384,plain,
( sQ35_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f383]) ).
fof(f385,plain,
( sQ40_spl
| ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f375,f273]) ).
fof(f386,plain,
( sQ40_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f385]) ).
fof(f387,plain,
$false,
inference(sat_refutation,[status(thm)],[f107,f147,f170,f177,f185,f192,f200,f207,f214,f222,f229,f244,f246,f286,f303,f360,f362,f366,f368,f370,f376,f382,f384,f386]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT113+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 01:32:28 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.42 % Elapsed time: 0.042687 seconds
% 0.14/0.42 % CPU time: 0.117390 seconds
% 0.14/0.42 % Total memory used: 31.858 MB
% 0.14/0.42 % Net memory used: 31.793 MB
%------------------------------------------------------------------------------