%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n011.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:16:19 AM UTC 2026
% Result : Theorem 0.24s 0.48s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 11
% Syntax : Number of formulae : 195 ( 35 unt; 0 def)
% Number of atoms : 971 ( 0 equ)
% Maximal formula atoms : 72 ( 4 avg)
% Number of connectives : 1494 ( 718 ~; 699 |; 74 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 6 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 : 510 ( 23 sgn 132 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax_proh_relator_remedy,axiom,
! [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) ) ) ).
fof(ax_B2,axiom,
! [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) ) ).
fof(ax_B3,axiom,
! [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) ) ).
fof(proh_f1,axiom,
proh(f1) ).
fof(rem_f1,axiom,
has_rem(f1) ).
fof(aee_f1,axiom,
aee(f1,marketplace) ).
fof(aer_f1,axiom,
aer(f1,philharmonie) ).
fof(act_f1,axiom,
act(f1,distrib) ).
fof(tgt_f1,axiom,
tgt(f1,concert_ds) ).
fof(act_e1_f1,axiom,
activates(e1,f1) ).
fof(conjecture,conjecture,
? [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) ) ).
fof(subgoal_0,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(strip,[],[conjecture]) ).
fof(negate_0_0,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,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
act(f1,distrib),
inference(canonicalize,[],[act_f1]) ).
fof(normalize_0_1,plain,
activates(e1,f1),
inference(canonicalize,[],[act_e1_f1]) ).
fof(normalize_0_2,plain,
aee(f1,marketplace),
inference(canonicalize,[],[aee_f1]) ).
fof(normalize_0_3,plain,
aer(f1,philharmonie),
inference(canonicalize,[],[aer_f1]) ).
fof(normalize_0_4,plain,
tgt(f1,concert_ds),
inference(canonicalize,[],[tgt_f1]) ).
fof(normalize_0_5,plain,
! [A,E,F,T,X,Y] :
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| ? [Pw,RhoR,S] :
( bearer(Pw,Y)
& bearer(S,X)
& cnt(Pw,decl(A),T)
& cnt(S,decl(A),T)
& founds_rem(E,RhoR,F)
& part_of(Pw,RhoR)
& part_of(S,RhoR)
& power(Pw)
& subjection(S) ) ),
inference(canonicalize,[],[ax_proh_relator_remedy]) ).
fof(normalize_0_6,plain,
! [A,E,F,T,X,Y] :
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| ? [Pw,RhoR,S] :
( bearer(Pw,Y)
& bearer(S,X)
& cnt(Pw,decl(A),T)
& cnt(S,decl(A),T)
& founds_rem(E,RhoR,F)
& part_of(Pw,RhoR)
& part_of(S,RhoR)
& power(Pw)
& subjection(S) ) ),
inference(specialize,[],[normalize_0_5]) ).
fof(normalize_0_7,plain,
! [A,E,F,T,X,Y] :
( ( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| bearer(skolemFOFtoCNF_Pw(A,E,F,T,X,Y),Y) )
& ( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| bearer(skolemFOFtoCNF_S(A,E,F,T,X,Y),X) )
& ( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| cnt(skolemFOFtoCNF_Pw(A,E,F,T,X,Y),decl(A),T) )
& ( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| cnt(skolemFOFtoCNF_S(A,E,F,T,X,Y),decl(A),T) )
& ( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| founds_rem(E,skolemFOFtoCNF_RhoR(A,E,F,T,X,Y),F) )
& ( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| part_of(skolemFOFtoCNF_Pw(A,E,F,T,X,Y),skolemFOFtoCNF_RhoR(A,E,F,T,X,Y)) )
& ( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| part_of(skolemFOFtoCNF_S(A,E,F,T,X,Y),skolemFOFtoCNF_RhoR(A,E,F,T,X,Y)) )
& ( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| power(skolemFOFtoCNF_Pw(A,E,F,T,X,Y)) )
& ( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| subjection(skolemFOFtoCNF_S(A,E,F,T,X,Y)) ) ),
inference(clausify,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
! [A,E,F,T,X,Y] :
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| cnt(skolemFOFtoCNF_Pw(A,E,F,T,X,Y),decl(A),T) ),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
has_rem(f1),
inference(canonicalize,[],[rem_f1]) ).
fof(normalize_0_10,plain,
proh(f1),
inference(canonicalize,[],[proh_f1]) ).
fof(normalize_0_11,plain,
! [A,E,Pw,Rho,T] :
( ~ cnt(Pw,decl(A),T)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E)
| ! [R] : ~ founds_rem(E,Rho,R) ),
inference(canonicalize,[],[ax_B2]) ).
fof(normalize_0_12,plain,
! [A,E,Pw,Rho,T] :
( ~ cnt(Pw,decl(A),T)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E)
| ! [R] : ~ founds_rem(E,Rho,R) ),
inference(specialize,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
! [A,E,Pw,R,Rho,T] :
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
inference(clausify,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
! [A,E,F,T,X,Y] :
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| founds_rem(E,skolemFOFtoCNF_RhoR(A,E,F,T,X,Y),F) ),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_15,plain,
! [A,E,F,T,X,Y] :
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| part_of(skolemFOFtoCNF_Pw(A,E,F,T,X,Y),skolemFOFtoCNF_RhoR(A,E,F,T,X,Y)) ),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_16,plain,
! [A,E,F,T,X,Y] :
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| power(skolemFOFtoCNF_Pw(A,E,F,T,X,Y)) ),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_17,plain,
! [Pw,RhoR,S] :
( ~ about_event(Pw,e1)
| ~ about_event(S,e1)
| ~ bearer(Pw,philharmonie)
| ~ bearer(S,marketplace)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ founds_rem(e1,RhoR,f1)
| ~ part_of(Pw,RhoR)
| ~ part_of(S,RhoR)
| ~ power(Pw)
| ~ subjection(S) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_18,plain,
! [Pw,RhoR,S] :
( ~ about_event(Pw,e1)
| ~ about_event(S,e1)
| ~ bearer(Pw,philharmonie)
| ~ bearer(S,marketplace)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ founds_rem(e1,RhoR,f1)
| ~ part_of(Pw,RhoR)
| ~ part_of(S,RhoR)
| ~ power(Pw)
| ~ subjection(S) ),
inference(specialize,[],[normalize_0_17]) ).
fof(normalize_0_19,plain,
! [A,E,F,T,X,Y] :
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| bearer(skolemFOFtoCNF_Pw(A,E,F,T,X,Y),Y) ),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_20,plain,
! [A,E,F,T,X,Y] :
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| cnt(skolemFOFtoCNF_S(A,E,F,T,X,Y),decl(A),T) ),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_21,plain,
! [A,E,F,T,X,Y] :
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| bearer(skolemFOFtoCNF_S(A,E,F,T,X,Y),X) ),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_22,plain,
! [A,E,F,T,X,Y] :
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| subjection(skolemFOFtoCNF_S(A,E,F,T,X,Y)) ),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_23,plain,
! [A,E,F,T,X,Y] :
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| part_of(skolemFOFtoCNF_S(A,E,F,T,X,Y),skolemFOFtoCNF_RhoR(A,E,F,T,X,Y)) ),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_24,plain,
! [A,E,Rho,S,T] :
( ~ cnt(S,decl(A),T)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E)
| ! [R] : ~ founds_rem(E,Rho,R) ),
inference(canonicalize,[],[ax_B3]) ).
fof(normalize_0_25,plain,
! [A,E,Rho,S,T] :
( ~ cnt(S,decl(A),T)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E)
| ! [R] : ~ founds_rem(E,Rho,R) ),
inference(specialize,[],[normalize_0_24]) ).
fof(normalize_0_26,plain,
! [A,E,R,Rho,S,T] :
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
inference(clausify,[],[normalize_0_25]) ).
cnf(refute_0_0,plain,
act(f1,distrib),
inference(canonicalize,[],[normalize_0_0]) ).
cnf(refute_0_1,plain,
activates(e1,f1),
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_2,plain,
aee(f1,marketplace),
inference(canonicalize,[],[normalize_0_2]) ).
cnf(refute_0_3,plain,
aer(f1,philharmonie),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_4,plain,
tgt(f1,concert_ds),
inference(canonicalize,[],[normalize_0_4]) ).
cnf(refute_0_5,plain,
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| cnt(skolemFOFtoCNF_Pw(A,E,F,T,X,Y),decl(A),T) ),
inference(canonicalize,[],[normalize_0_8]) ).
cnf(refute_0_6,plain,
( ~ act(f1,X_297)
| ~ activates(X_298,f1)
| ~ aee(f1,X_301)
| ~ aer(f1,X_302)
| ~ has_rem(f1)
| ~ proh(f1)
| ~ tgt(f1,concert_ds)
| cnt(skolemFOFtoCNF_Pw(X_297,X_298,f1,concert_ds,X_301,X_302),decl(X_297),concert_ds) ),
inference(subst,[],[refute_0_5:[bind(A,$fot(X_297)),bind(E,$fot(X_298)),bind(F,$fot(f1)),bind(T,$fot(concert_ds)),bind(X,$fot(X_301)),bind(Y,$fot(X_302))]]) ).
cnf(refute_0_7,plain,
( ~ act(f1,X_297)
| ~ activates(X_298,f1)
| ~ aee(f1,X_301)
| ~ aer(f1,X_302)
| ~ has_rem(f1)
| ~ proh(f1)
| cnt(skolemFOFtoCNF_Pw(X_297,X_298,f1,concert_ds,X_301,X_302),decl(X_297),concert_ds) ),
inference(resolve,[$cnf( tgt(f1,concert_ds) )],[refute_0_4,refute_0_6]) ).
cnf(refute_0_8,plain,
has_rem(f1),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_9,plain,
( ~ act(f1,X_297)
| ~ activates(X_298,f1)
| ~ aee(f1,X_301)
| ~ aer(f1,X_302)
| ~ proh(f1)
| cnt(skolemFOFtoCNF_Pw(X_297,X_298,f1,concert_ds,X_301,X_302),decl(X_297),concert_ds) ),
inference(resolve,[$cnf( has_rem(f1) )],[refute_0_8,refute_0_7]) ).
cnf(refute_0_10,plain,
proh(f1),
inference(canonicalize,[],[normalize_0_10]) ).
cnf(refute_0_11,plain,
( ~ act(f1,X_297)
| ~ activates(X_298,f1)
| ~ aee(f1,X_301)
| ~ aer(f1,X_302)
| cnt(skolemFOFtoCNF_Pw(X_297,X_298,f1,concert_ds,X_301,X_302),decl(X_297),concert_ds) ),
inference(resolve,[$cnf( proh(f1) )],[refute_0_10,refute_0_9]) ).
cnf(refute_0_12,plain,
( ~ act(f1,X_303)
| ~ activates(X_304,f1)
| ~ aee(f1,X_305)
| ~ aer(f1,philharmonie)
| cnt(skolemFOFtoCNF_Pw(X_303,X_304,f1,concert_ds,X_305,philharmonie),decl(X_303),concert_ds) ),
inference(subst,[],[refute_0_11:[bind(X_297,$fot(X_303)),bind(X_298,$fot(X_304)),bind(X_301,$fot(X_305)),bind(X_302,$fot(philharmonie))]]) ).
cnf(refute_0_13,plain,
( ~ act(f1,X_303)
| ~ activates(X_304,f1)
| ~ aee(f1,X_305)
| cnt(skolemFOFtoCNF_Pw(X_303,X_304,f1,concert_ds,X_305,philharmonie),decl(X_303),concert_ds) ),
inference(resolve,[$cnf( aer(f1,philharmonie) )],[refute_0_3,refute_0_12]) ).
cnf(refute_0_14,plain,
( ~ act(f1,X_307)
| ~ activates(X_308,f1)
| ~ aee(f1,marketplace)
| cnt(skolemFOFtoCNF_Pw(X_307,X_308,f1,concert_ds,marketplace,philharmonie),decl(X_307),concert_ds) ),
inference(subst,[],[refute_0_13:[bind(X_303,$fot(X_307)),bind(X_304,$fot(X_308)),bind(X_305,$fot(marketplace))]]) ).
cnf(refute_0_15,plain,
( ~ act(f1,X_307)
| ~ activates(X_308,f1)
| cnt(skolemFOFtoCNF_Pw(X_307,X_308,f1,concert_ds,marketplace,philharmonie),decl(X_307),concert_ds) ),
inference(resolve,[$cnf( aee(f1,marketplace) )],[refute_0_2,refute_0_14]) ).
cnf(refute_0_16,plain,
( ~ act(f1,X_310)
| ~ activates(e1,f1)
| cnt(skolemFOFtoCNF_Pw(X_310,e1,f1,concert_ds,marketplace,philharmonie),decl(X_310),concert_ds) ),
inference(subst,[],[refute_0_15:[bind(X_307,$fot(X_310)),bind(X_308,$fot(e1))]]) ).
cnf(refute_0_17,plain,
( ~ act(f1,X_310)
| cnt(skolemFOFtoCNF_Pw(X_310,e1,f1,concert_ds,marketplace,philharmonie),decl(X_310),concert_ds) ),
inference(resolve,[$cnf( activates(e1,f1) )],[refute_0_1,refute_0_16]) ).
cnf(refute_0_18,plain,
( ~ act(f1,distrib)
| cnt(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds) ),
inference(subst,[],[refute_0_17:[bind(X_310,$fot(distrib))]]) ).
cnf(refute_0_19,plain,
cnt(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds),
inference(resolve,[$cnf( act(f1,distrib) )],[refute_0_0,refute_0_18]) ).
cnf(refute_0_20,plain,
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(Pw,Rho)
| ~ power(Pw)
| about_event(Pw,E) ),
inference(canonicalize,[],[normalize_0_13]) ).
cnf(refute_0_21,plain,
( ~ cnt(Pw,decl(A),T)
| ~ founds_rem(e1,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie),f1)
| ~ part_of(Pw,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| ~ power(Pw)
| about_event(Pw,e1) ),
inference(subst,[],[refute_0_20:[bind(E,$fot(e1)),bind(R,$fot(f1)),bind(Rho,$fot(skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)))]]) ).
cnf(refute_0_22,plain,
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| founds_rem(E,skolemFOFtoCNF_RhoR(A,E,F,T,X,Y),F) ),
inference(canonicalize,[],[normalize_0_14]) ).
cnf(refute_0_23,plain,
( ~ act(f1,X_274)
| ~ activates(X_275,f1)
| ~ aee(f1,X_278)
| ~ aer(f1,X_279)
| ~ has_rem(f1)
| ~ proh(f1)
| ~ tgt(f1,concert_ds)
| founds_rem(X_275,skolemFOFtoCNF_RhoR(X_274,X_275,f1,concert_ds,X_278,X_279),f1) ),
inference(subst,[],[refute_0_22:[bind(A,$fot(X_274)),bind(E,$fot(X_275)),bind(F,$fot(f1)),bind(T,$fot(concert_ds)),bind(X,$fot(X_278)),bind(Y,$fot(X_279))]]) ).
cnf(refute_0_24,plain,
( ~ act(f1,X_274)
| ~ activates(X_275,f1)
| ~ aee(f1,X_278)
| ~ aer(f1,X_279)
| ~ has_rem(f1)
| ~ proh(f1)
| founds_rem(X_275,skolemFOFtoCNF_RhoR(X_274,X_275,f1,concert_ds,X_278,X_279),f1) ),
inference(resolve,[$cnf( tgt(f1,concert_ds) )],[refute_0_4,refute_0_23]) ).
cnf(refute_0_25,plain,
( ~ act(f1,X_274)
| ~ activates(X_275,f1)
| ~ aee(f1,X_278)
| ~ aer(f1,X_279)
| ~ proh(f1)
| founds_rem(X_275,skolemFOFtoCNF_RhoR(X_274,X_275,f1,concert_ds,X_278,X_279),f1) ),
inference(resolve,[$cnf( has_rem(f1) )],[refute_0_8,refute_0_24]) ).
cnf(refute_0_26,plain,
( ~ act(f1,X_274)
| ~ activates(X_275,f1)
| ~ aee(f1,X_278)
| ~ aer(f1,X_279)
| founds_rem(X_275,skolemFOFtoCNF_RhoR(X_274,X_275,f1,concert_ds,X_278,X_279),f1) ),
inference(resolve,[$cnf( proh(f1) )],[refute_0_10,refute_0_25]) ).
cnf(refute_0_27,plain,
( ~ act(f1,X_280)
| ~ activates(X_281,f1)
| ~ aee(f1,X_282)
| ~ aer(f1,philharmonie)
| founds_rem(X_281,skolemFOFtoCNF_RhoR(X_280,X_281,f1,concert_ds,X_282,philharmonie),f1) ),
inference(subst,[],[refute_0_26:[bind(X_274,$fot(X_280)),bind(X_275,$fot(X_281)),bind(X_278,$fot(X_282)),bind(X_279,$fot(philharmonie))]]) ).
cnf(refute_0_28,plain,
( ~ act(f1,X_280)
| ~ activates(X_281,f1)
| ~ aee(f1,X_282)
| founds_rem(X_281,skolemFOFtoCNF_RhoR(X_280,X_281,f1,concert_ds,X_282,philharmonie),f1) ),
inference(resolve,[$cnf( aer(f1,philharmonie) )],[refute_0_3,refute_0_27]) ).
cnf(refute_0_29,plain,
( ~ act(f1,X_284)
| ~ activates(X_285,f1)
| ~ aee(f1,marketplace)
| founds_rem(X_285,skolemFOFtoCNF_RhoR(X_284,X_285,f1,concert_ds,marketplace,philharmonie),f1) ),
inference(subst,[],[refute_0_28:[bind(X_280,$fot(X_284)),bind(X_281,$fot(X_285)),bind(X_282,$fot(marketplace))]]) ).
cnf(refute_0_30,plain,
( ~ act(f1,X_284)
| ~ activates(X_285,f1)
| founds_rem(X_285,skolemFOFtoCNF_RhoR(X_284,X_285,f1,concert_ds,marketplace,philharmonie),f1) ),
inference(resolve,[$cnf( aee(f1,marketplace) )],[refute_0_2,refute_0_29]) ).
cnf(refute_0_31,plain,
( ~ act(f1,X_287)
| ~ activates(e1,f1)
| founds_rem(e1,skolemFOFtoCNF_RhoR(X_287,e1,f1,concert_ds,marketplace,philharmonie),f1) ),
inference(subst,[],[refute_0_30:[bind(X_284,$fot(X_287)),bind(X_285,$fot(e1))]]) ).
cnf(refute_0_32,plain,
( ~ act(f1,X_287)
| founds_rem(e1,skolemFOFtoCNF_RhoR(X_287,e1,f1,concert_ds,marketplace,philharmonie),f1) ),
inference(resolve,[$cnf( activates(e1,f1) )],[refute_0_1,refute_0_31]) ).
cnf(refute_0_33,plain,
( ~ act(f1,distrib)
| founds_rem(e1,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie),f1) ),
inference(subst,[],[refute_0_32:[bind(X_287,$fot(distrib))]]) ).
cnf(refute_0_34,plain,
founds_rem(e1,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie),f1),
inference(resolve,[$cnf( act(f1,distrib) )],[refute_0_0,refute_0_33]) ).
cnf(refute_0_35,plain,
( ~ cnt(Pw,decl(A),T)
| ~ part_of(Pw,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| ~ power(Pw)
| about_event(Pw,e1) ),
inference(resolve,[$cnf( founds_rem(e1,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie),f1) )],[refute_0_34,refute_0_21]) ).
cnf(refute_0_36,plain,
( ~ cnt(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(A),T)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| ~ power(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1) ),
inference(subst,[],[refute_0_35:[bind(Pw,$fot(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie)))]]) ).
cnf(refute_0_37,plain,
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| part_of(skolemFOFtoCNF_Pw(A,E,F,T,X,Y),skolemFOFtoCNF_RhoR(A,E,F,T,X,Y)) ),
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_38,plain,
( ~ act(f1,X_365)
| ~ activates(X_366,f1)
| ~ aee(f1,X_369)
| ~ aer(f1,X_370)
| ~ has_rem(f1)
| ~ proh(f1)
| ~ tgt(f1,concert_ds)
| part_of(skolemFOFtoCNF_Pw(X_365,X_366,f1,concert_ds,X_369,X_370),skolemFOFtoCNF_RhoR(X_365,X_366,f1,concert_ds,X_369,X_370)) ),
inference(subst,[],[refute_0_37:[bind(A,$fot(X_365)),bind(E,$fot(X_366)),bind(F,$fot(f1)),bind(T,$fot(concert_ds)),bind(X,$fot(X_369)),bind(Y,$fot(X_370))]]) ).
cnf(refute_0_39,plain,
( ~ act(f1,X_365)
| ~ activates(X_366,f1)
| ~ aee(f1,X_369)
| ~ aer(f1,X_370)
| ~ has_rem(f1)
| ~ proh(f1)
| part_of(skolemFOFtoCNF_Pw(X_365,X_366,f1,concert_ds,X_369,X_370),skolemFOFtoCNF_RhoR(X_365,X_366,f1,concert_ds,X_369,X_370)) ),
inference(resolve,[$cnf( tgt(f1,concert_ds) )],[refute_0_4,refute_0_38]) ).
cnf(refute_0_40,plain,
( ~ act(f1,X_365)
| ~ activates(X_366,f1)
| ~ aee(f1,X_369)
| ~ aer(f1,X_370)
| ~ proh(f1)
| part_of(skolemFOFtoCNF_Pw(X_365,X_366,f1,concert_ds,X_369,X_370),skolemFOFtoCNF_RhoR(X_365,X_366,f1,concert_ds,X_369,X_370)) ),
inference(resolve,[$cnf( has_rem(f1) )],[refute_0_8,refute_0_39]) ).
cnf(refute_0_41,plain,
( ~ act(f1,X_365)
| ~ activates(X_366,f1)
| ~ aee(f1,X_369)
| ~ aer(f1,X_370)
| part_of(skolemFOFtoCNF_Pw(X_365,X_366,f1,concert_ds,X_369,X_370),skolemFOFtoCNF_RhoR(X_365,X_366,f1,concert_ds,X_369,X_370)) ),
inference(resolve,[$cnf( proh(f1) )],[refute_0_10,refute_0_40]) ).
cnf(refute_0_42,plain,
( ~ act(f1,X_371)
| ~ activates(X_372,f1)
| ~ aee(f1,X_373)
| ~ aer(f1,philharmonie)
| part_of(skolemFOFtoCNF_Pw(X_371,X_372,f1,concert_ds,X_373,philharmonie),skolemFOFtoCNF_RhoR(X_371,X_372,f1,concert_ds,X_373,philharmonie)) ),
inference(subst,[],[refute_0_41:[bind(X_365,$fot(X_371)),bind(X_366,$fot(X_372)),bind(X_369,$fot(X_373)),bind(X_370,$fot(philharmonie))]]) ).
cnf(refute_0_43,plain,
( ~ act(f1,X_371)
| ~ activates(X_372,f1)
| ~ aee(f1,X_373)
| part_of(skolemFOFtoCNF_Pw(X_371,X_372,f1,concert_ds,X_373,philharmonie),skolemFOFtoCNF_RhoR(X_371,X_372,f1,concert_ds,X_373,philharmonie)) ),
inference(resolve,[$cnf( aer(f1,philharmonie) )],[refute_0_3,refute_0_42]) ).
cnf(refute_0_44,plain,
( ~ act(f1,X_375)
| ~ activates(X_376,f1)
| ~ aee(f1,marketplace)
| part_of(skolemFOFtoCNF_Pw(X_375,X_376,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(X_375,X_376,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_43:[bind(X_371,$fot(X_375)),bind(X_372,$fot(X_376)),bind(X_373,$fot(marketplace))]]) ).
cnf(refute_0_45,plain,
( ~ act(f1,X_375)
| ~ activates(X_376,f1)
| part_of(skolemFOFtoCNF_Pw(X_375,X_376,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(X_375,X_376,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( aee(f1,marketplace) )],[refute_0_2,refute_0_44]) ).
cnf(refute_0_46,plain,
( ~ act(f1,X_378)
| ~ activates(e1,f1)
| part_of(skolemFOFtoCNF_Pw(X_378,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(X_378,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_45:[bind(X_375,$fot(X_378)),bind(X_376,$fot(e1))]]) ).
cnf(refute_0_47,plain,
( ~ act(f1,X_378)
| part_of(skolemFOFtoCNF_Pw(X_378,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(X_378,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( activates(e1,f1) )],[refute_0_1,refute_0_46]) ).
cnf(refute_0_48,plain,
( ~ act(f1,distrib)
| part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_47:[bind(X_378,$fot(distrib))]]) ).
cnf(refute_0_49,plain,
part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)),
inference(resolve,[$cnf( act(f1,distrib) )],[refute_0_0,refute_0_48]) ).
cnf(refute_0_50,plain,
( ~ cnt(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(A),T)
| ~ power(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1) ),
inference(resolve,[$cnf( part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)) )],[refute_0_49,refute_0_36]) ).
cnf(refute_0_51,plain,
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| power(skolemFOFtoCNF_Pw(A,E,F,T,X,Y)) ),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_52,plain,
( ~ act(f1,X_157)
| ~ activates(X_158,f1)
| ~ aee(f1,X_161)
| ~ aer(f1,X_162)
| ~ has_rem(f1)
| ~ proh(f1)
| ~ tgt(f1,concert_ds)
| power(skolemFOFtoCNF_Pw(X_157,X_158,f1,concert_ds,X_161,X_162)) ),
inference(subst,[],[refute_0_51:[bind(A,$fot(X_157)),bind(E,$fot(X_158)),bind(F,$fot(f1)),bind(T,$fot(concert_ds)),bind(X,$fot(X_161)),bind(Y,$fot(X_162))]]) ).
cnf(refute_0_53,plain,
( ~ act(f1,X_157)
| ~ activates(X_158,f1)
| ~ aee(f1,X_161)
| ~ aer(f1,X_162)
| ~ has_rem(f1)
| ~ proh(f1)
| power(skolemFOFtoCNF_Pw(X_157,X_158,f1,concert_ds,X_161,X_162)) ),
inference(resolve,[$cnf( tgt(f1,concert_ds) )],[refute_0_4,refute_0_52]) ).
cnf(refute_0_54,plain,
( ~ act(f1,X_157)
| ~ activates(X_158,f1)
| ~ aee(f1,X_161)
| ~ aer(f1,X_162)
| ~ proh(f1)
| power(skolemFOFtoCNF_Pw(X_157,X_158,f1,concert_ds,X_161,X_162)) ),
inference(resolve,[$cnf( has_rem(f1) )],[refute_0_8,refute_0_53]) ).
cnf(refute_0_55,plain,
( ~ act(f1,X_157)
| ~ activates(X_158,f1)
| ~ aee(f1,X_161)
| ~ aer(f1,X_162)
| power(skolemFOFtoCNF_Pw(X_157,X_158,f1,concert_ds,X_161,X_162)) ),
inference(resolve,[$cnf( proh(f1) )],[refute_0_10,refute_0_54]) ).
cnf(refute_0_56,plain,
( ~ act(f1,X_163)
| ~ activates(X_164,f1)
| ~ aee(f1,X_165)
| ~ aer(f1,philharmonie)
| power(skolemFOFtoCNF_Pw(X_163,X_164,f1,concert_ds,X_165,philharmonie)) ),
inference(subst,[],[refute_0_55:[bind(X_157,$fot(X_163)),bind(X_158,$fot(X_164)),bind(X_161,$fot(X_165)),bind(X_162,$fot(philharmonie))]]) ).
cnf(refute_0_57,plain,
( ~ act(f1,X_163)
| ~ activates(X_164,f1)
| ~ aee(f1,X_165)
| power(skolemFOFtoCNF_Pw(X_163,X_164,f1,concert_ds,X_165,philharmonie)) ),
inference(resolve,[$cnf( aer(f1,philharmonie) )],[refute_0_3,refute_0_56]) ).
cnf(refute_0_58,plain,
( ~ act(f1,X_167)
| ~ activates(X_168,f1)
| ~ aee(f1,marketplace)
| power(skolemFOFtoCNF_Pw(X_167,X_168,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_57:[bind(X_163,$fot(X_167)),bind(X_164,$fot(X_168)),bind(X_165,$fot(marketplace))]]) ).
cnf(refute_0_59,plain,
( ~ act(f1,X_167)
| ~ activates(X_168,f1)
| power(skolemFOFtoCNF_Pw(X_167,X_168,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( aee(f1,marketplace) )],[refute_0_2,refute_0_58]) ).
cnf(refute_0_60,plain,
( ~ act(f1,X_170)
| ~ activates(e1,f1)
| power(skolemFOFtoCNF_Pw(X_170,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_59:[bind(X_167,$fot(X_170)),bind(X_168,$fot(e1))]]) ).
cnf(refute_0_61,plain,
( ~ act(f1,X_170)
| power(skolemFOFtoCNF_Pw(X_170,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( activates(e1,f1) )],[refute_0_1,refute_0_60]) ).
cnf(refute_0_62,plain,
( ~ act(f1,distrib)
| power(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_61:[bind(X_170,$fot(distrib))]]) ).
cnf(refute_0_63,plain,
power(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie)),
inference(resolve,[$cnf( act(f1,distrib) )],[refute_0_0,refute_0_62]) ).
cnf(refute_0_64,plain,
( ~ cnt(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(A),T)
| about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1) ),
inference(resolve,[$cnf( power(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie)) )],[refute_0_63,refute_0_50]) ).
cnf(refute_0_65,plain,
( ~ about_event(Pw,e1)
| ~ about_event(S,e1)
| ~ bearer(Pw,philharmonie)
| ~ bearer(S,marketplace)
| ~ cnt(Pw,decl(distrib),concert_ds)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ founds_rem(e1,RhoR,f1)
| ~ part_of(Pw,RhoR)
| ~ part_of(S,RhoR)
| ~ power(Pw)
| ~ subjection(S) ),
inference(canonicalize,[],[normalize_0_18]) ).
cnf(refute_0_66,plain,
( ~ about_event(S,e1)
| ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ bearer(S,marketplace)
| ~ bearer(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),philharmonie)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ cnt(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds)
| ~ founds_rem(e1,RhoR,f1)
| ~ part_of(S,RhoR)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR)
| ~ power(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| ~ subjection(S) ),
inference(subst,[],[refute_0_65:[bind(Pw,$fot(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie)))]]) ).
cnf(refute_0_67,plain,
( ~ about_event(S,e1)
| ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ bearer(S,marketplace)
| ~ bearer(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),philharmonie)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ founds_rem(e1,RhoR,f1)
| ~ part_of(S,RhoR)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR)
| ~ power(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| ~ subjection(S) ),
inference(resolve,[$cnf( cnt(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds) )],[refute_0_19,refute_0_66]) ).
cnf(refute_0_68,plain,
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| bearer(skolemFOFtoCNF_Pw(A,E,F,T,X,Y),Y) ),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_69,plain,
( ~ act(f1,X_237)
| ~ activates(X_238,f1)
| ~ aee(f1,X_241)
| ~ aer(f1,X_242)
| ~ has_rem(f1)
| ~ proh(f1)
| ~ tgt(f1,concert_ds)
| bearer(skolemFOFtoCNF_Pw(X_237,X_238,f1,concert_ds,X_241,X_242),X_242) ),
inference(subst,[],[refute_0_68:[bind(A,$fot(X_237)),bind(E,$fot(X_238)),bind(F,$fot(f1)),bind(T,$fot(concert_ds)),bind(X,$fot(X_241)),bind(Y,$fot(X_242))]]) ).
cnf(refute_0_70,plain,
( ~ act(f1,X_237)
| ~ activates(X_238,f1)
| ~ aee(f1,X_241)
| ~ aer(f1,X_242)
| ~ has_rem(f1)
| ~ proh(f1)
| bearer(skolemFOFtoCNF_Pw(X_237,X_238,f1,concert_ds,X_241,X_242),X_242) ),
inference(resolve,[$cnf( tgt(f1,concert_ds) )],[refute_0_4,refute_0_69]) ).
cnf(refute_0_71,plain,
( ~ act(f1,X_237)
| ~ activates(X_238,f1)
| ~ aee(f1,X_241)
| ~ aer(f1,X_242)
| ~ proh(f1)
| bearer(skolemFOFtoCNF_Pw(X_237,X_238,f1,concert_ds,X_241,X_242),X_242) ),
inference(resolve,[$cnf( has_rem(f1) )],[refute_0_8,refute_0_70]) ).
cnf(refute_0_72,plain,
( ~ act(f1,X_237)
| ~ activates(X_238,f1)
| ~ aee(f1,X_241)
| ~ aer(f1,X_242)
| bearer(skolemFOFtoCNF_Pw(X_237,X_238,f1,concert_ds,X_241,X_242),X_242) ),
inference(resolve,[$cnf( proh(f1) )],[refute_0_10,refute_0_71]) ).
cnf(refute_0_73,plain,
( ~ act(f1,X_243)
| ~ activates(X_244,f1)
| ~ aee(f1,X_245)
| ~ aer(f1,philharmonie)
| bearer(skolemFOFtoCNF_Pw(X_243,X_244,f1,concert_ds,X_245,philharmonie),philharmonie) ),
inference(subst,[],[refute_0_72:[bind(X_237,$fot(X_243)),bind(X_238,$fot(X_244)),bind(X_241,$fot(X_245)),bind(X_242,$fot(philharmonie))]]) ).
cnf(refute_0_74,plain,
( ~ act(f1,X_243)
| ~ activates(X_244,f1)
| ~ aee(f1,X_245)
| bearer(skolemFOFtoCNF_Pw(X_243,X_244,f1,concert_ds,X_245,philharmonie),philharmonie) ),
inference(resolve,[$cnf( aer(f1,philharmonie) )],[refute_0_3,refute_0_73]) ).
cnf(refute_0_75,plain,
( ~ act(f1,X_247)
| ~ activates(X_248,f1)
| ~ aee(f1,marketplace)
| bearer(skolemFOFtoCNF_Pw(X_247,X_248,f1,concert_ds,marketplace,philharmonie),philharmonie) ),
inference(subst,[],[refute_0_74:[bind(X_243,$fot(X_247)),bind(X_244,$fot(X_248)),bind(X_245,$fot(marketplace))]]) ).
cnf(refute_0_76,plain,
( ~ act(f1,X_247)
| ~ activates(X_248,f1)
| bearer(skolemFOFtoCNF_Pw(X_247,X_248,f1,concert_ds,marketplace,philharmonie),philharmonie) ),
inference(resolve,[$cnf( aee(f1,marketplace) )],[refute_0_2,refute_0_75]) ).
cnf(refute_0_77,plain,
( ~ act(f1,X_250)
| ~ activates(e1,f1)
| bearer(skolemFOFtoCNF_Pw(X_250,e1,f1,concert_ds,marketplace,philharmonie),philharmonie) ),
inference(subst,[],[refute_0_76:[bind(X_247,$fot(X_250)),bind(X_248,$fot(e1))]]) ).
cnf(refute_0_78,plain,
( ~ act(f1,X_250)
| bearer(skolemFOFtoCNF_Pw(X_250,e1,f1,concert_ds,marketplace,philharmonie),philharmonie) ),
inference(resolve,[$cnf( activates(e1,f1) )],[refute_0_1,refute_0_77]) ).
cnf(refute_0_79,plain,
( ~ act(f1,distrib)
| bearer(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),philharmonie) ),
inference(subst,[],[refute_0_78:[bind(X_250,$fot(distrib))]]) ).
cnf(refute_0_80,plain,
bearer(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),philharmonie),
inference(resolve,[$cnf( act(f1,distrib) )],[refute_0_0,refute_0_79]) ).
cnf(refute_0_81,plain,
( ~ about_event(S,e1)
| ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ bearer(S,marketplace)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ founds_rem(e1,RhoR,f1)
| ~ part_of(S,RhoR)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR)
| ~ power(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| ~ subjection(S) ),
inference(resolve,[$cnf( bearer(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),philharmonie) )],[refute_0_80,refute_0_67]) ).
cnf(refute_0_82,plain,
( ~ about_event(S,e1)
| ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ bearer(S,marketplace)
| ~ cnt(S,decl(distrib),concert_ds)
| ~ founds_rem(e1,RhoR,f1)
| ~ part_of(S,RhoR)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR)
| ~ subjection(S) ),
inference(resolve,[$cnf( power(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie)) )],[refute_0_63,refute_0_81]) ).
cnf(refute_0_83,plain,
( ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ bearer(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),marketplace)
| ~ cnt(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds)
| ~ founds_rem(e1,RhoR,f1)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR)
| ~ part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR)
| ~ subjection(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_82:[bind(S,$fot(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie)))]]) ).
cnf(refute_0_84,plain,
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| cnt(skolemFOFtoCNF_S(A,E,F,T,X,Y),decl(A),T) ),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_85,plain,
( ~ act(f1,X_319)
| ~ activates(X_320,f1)
| ~ aee(f1,X_323)
| ~ aer(f1,X_324)
| ~ has_rem(f1)
| ~ proh(f1)
| ~ tgt(f1,concert_ds)
| cnt(skolemFOFtoCNF_S(X_319,X_320,f1,concert_ds,X_323,X_324),decl(X_319),concert_ds) ),
inference(subst,[],[refute_0_84:[bind(A,$fot(X_319)),bind(E,$fot(X_320)),bind(F,$fot(f1)),bind(T,$fot(concert_ds)),bind(X,$fot(X_323)),bind(Y,$fot(X_324))]]) ).
cnf(refute_0_86,plain,
( ~ act(f1,X_319)
| ~ activates(X_320,f1)
| ~ aee(f1,X_323)
| ~ aer(f1,X_324)
| ~ has_rem(f1)
| ~ proh(f1)
| cnt(skolemFOFtoCNF_S(X_319,X_320,f1,concert_ds,X_323,X_324),decl(X_319),concert_ds) ),
inference(resolve,[$cnf( tgt(f1,concert_ds) )],[refute_0_4,refute_0_85]) ).
cnf(refute_0_87,plain,
( ~ act(f1,X_319)
| ~ activates(X_320,f1)
| ~ aee(f1,X_323)
| ~ aer(f1,X_324)
| ~ proh(f1)
| cnt(skolemFOFtoCNF_S(X_319,X_320,f1,concert_ds,X_323,X_324),decl(X_319),concert_ds) ),
inference(resolve,[$cnf( has_rem(f1) )],[refute_0_8,refute_0_86]) ).
cnf(refute_0_88,plain,
( ~ act(f1,X_319)
| ~ activates(X_320,f1)
| ~ aee(f1,X_323)
| ~ aer(f1,X_324)
| cnt(skolemFOFtoCNF_S(X_319,X_320,f1,concert_ds,X_323,X_324),decl(X_319),concert_ds) ),
inference(resolve,[$cnf( proh(f1) )],[refute_0_10,refute_0_87]) ).
cnf(refute_0_89,plain,
( ~ act(f1,X_325)
| ~ activates(X_326,f1)
| ~ aee(f1,X_327)
| ~ aer(f1,philharmonie)
| cnt(skolemFOFtoCNF_S(X_325,X_326,f1,concert_ds,X_327,philharmonie),decl(X_325),concert_ds) ),
inference(subst,[],[refute_0_88:[bind(X_319,$fot(X_325)),bind(X_320,$fot(X_326)),bind(X_323,$fot(X_327)),bind(X_324,$fot(philharmonie))]]) ).
cnf(refute_0_90,plain,
( ~ act(f1,X_325)
| ~ activates(X_326,f1)
| ~ aee(f1,X_327)
| cnt(skolemFOFtoCNF_S(X_325,X_326,f1,concert_ds,X_327,philharmonie),decl(X_325),concert_ds) ),
inference(resolve,[$cnf( aer(f1,philharmonie) )],[refute_0_3,refute_0_89]) ).
cnf(refute_0_91,plain,
( ~ act(f1,X_329)
| ~ activates(X_330,f1)
| ~ aee(f1,marketplace)
| cnt(skolemFOFtoCNF_S(X_329,X_330,f1,concert_ds,marketplace,philharmonie),decl(X_329),concert_ds) ),
inference(subst,[],[refute_0_90:[bind(X_325,$fot(X_329)),bind(X_326,$fot(X_330)),bind(X_327,$fot(marketplace))]]) ).
cnf(refute_0_92,plain,
( ~ act(f1,X_329)
| ~ activates(X_330,f1)
| cnt(skolemFOFtoCNF_S(X_329,X_330,f1,concert_ds,marketplace,philharmonie),decl(X_329),concert_ds) ),
inference(resolve,[$cnf( aee(f1,marketplace) )],[refute_0_2,refute_0_91]) ).
cnf(refute_0_93,plain,
( ~ act(f1,X_332)
| ~ activates(e1,f1)
| cnt(skolemFOFtoCNF_S(X_332,e1,f1,concert_ds,marketplace,philharmonie),decl(X_332),concert_ds) ),
inference(subst,[],[refute_0_92:[bind(X_329,$fot(X_332)),bind(X_330,$fot(e1))]]) ).
cnf(refute_0_94,plain,
( ~ act(f1,X_332)
| cnt(skolemFOFtoCNF_S(X_332,e1,f1,concert_ds,marketplace,philharmonie),decl(X_332),concert_ds) ),
inference(resolve,[$cnf( activates(e1,f1) )],[refute_0_1,refute_0_93]) ).
cnf(refute_0_95,plain,
( ~ act(f1,distrib)
| cnt(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds) ),
inference(subst,[],[refute_0_94:[bind(X_332,$fot(distrib))]]) ).
cnf(refute_0_96,plain,
cnt(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds),
inference(resolve,[$cnf( act(f1,distrib) )],[refute_0_0,refute_0_95]) ).
cnf(refute_0_97,plain,
( ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ bearer(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),marketplace)
| ~ founds_rem(e1,RhoR,f1)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR)
| ~ part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR)
| ~ subjection(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( cnt(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds) )],[refute_0_96,refute_0_83]) ).
cnf(refute_0_98,plain,
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| bearer(skolemFOFtoCNF_S(A,E,F,T,X,Y),X) ),
inference(canonicalize,[],[normalize_0_21]) ).
cnf(refute_0_99,plain,
( ~ act(f1,X_253)
| ~ activates(X_254,f1)
| ~ aee(f1,X_257)
| ~ aer(f1,X_258)
| ~ has_rem(f1)
| ~ proh(f1)
| ~ tgt(f1,concert_ds)
| bearer(skolemFOFtoCNF_S(X_253,X_254,f1,concert_ds,X_257,X_258),X_257) ),
inference(subst,[],[refute_0_98:[bind(A,$fot(X_253)),bind(E,$fot(X_254)),bind(F,$fot(f1)),bind(T,$fot(concert_ds)),bind(X,$fot(X_257)),bind(Y,$fot(X_258))]]) ).
cnf(refute_0_100,plain,
( ~ act(f1,X_253)
| ~ activates(X_254,f1)
| ~ aee(f1,X_257)
| ~ aer(f1,X_258)
| ~ has_rem(f1)
| ~ proh(f1)
| bearer(skolemFOFtoCNF_S(X_253,X_254,f1,concert_ds,X_257,X_258),X_257) ),
inference(resolve,[$cnf( tgt(f1,concert_ds) )],[refute_0_4,refute_0_99]) ).
cnf(refute_0_101,plain,
( ~ act(f1,X_253)
| ~ activates(X_254,f1)
| ~ aee(f1,X_257)
| ~ aer(f1,X_258)
| ~ proh(f1)
| bearer(skolemFOFtoCNF_S(X_253,X_254,f1,concert_ds,X_257,X_258),X_257) ),
inference(resolve,[$cnf( has_rem(f1) )],[refute_0_8,refute_0_100]) ).
cnf(refute_0_102,plain,
( ~ act(f1,X_253)
| ~ activates(X_254,f1)
| ~ aee(f1,X_257)
| ~ aer(f1,X_258)
| bearer(skolemFOFtoCNF_S(X_253,X_254,f1,concert_ds,X_257,X_258),X_257) ),
inference(resolve,[$cnf( proh(f1) )],[refute_0_10,refute_0_101]) ).
cnf(refute_0_103,plain,
( ~ act(f1,X_259)
| ~ activates(X_260,f1)
| ~ aee(f1,X_261)
| ~ aer(f1,philharmonie)
| bearer(skolemFOFtoCNF_S(X_259,X_260,f1,concert_ds,X_261,philharmonie),X_261) ),
inference(subst,[],[refute_0_102:[bind(X_253,$fot(X_259)),bind(X_254,$fot(X_260)),bind(X_257,$fot(X_261)),bind(X_258,$fot(philharmonie))]]) ).
cnf(refute_0_104,plain,
( ~ act(f1,X_259)
| ~ activates(X_260,f1)
| ~ aee(f1,X_261)
| bearer(skolemFOFtoCNF_S(X_259,X_260,f1,concert_ds,X_261,philharmonie),X_261) ),
inference(resolve,[$cnf( aer(f1,philharmonie) )],[refute_0_3,refute_0_103]) ).
cnf(refute_0_105,plain,
( ~ act(f1,X_263)
| ~ activates(X_264,f1)
| ~ aee(f1,marketplace)
| bearer(skolemFOFtoCNF_S(X_263,X_264,f1,concert_ds,marketplace,philharmonie),marketplace) ),
inference(subst,[],[refute_0_104:[bind(X_259,$fot(X_263)),bind(X_260,$fot(X_264)),bind(X_261,$fot(marketplace))]]) ).
cnf(refute_0_106,plain,
( ~ act(f1,X_263)
| ~ activates(X_264,f1)
| bearer(skolemFOFtoCNF_S(X_263,X_264,f1,concert_ds,marketplace,philharmonie),marketplace) ),
inference(resolve,[$cnf( aee(f1,marketplace) )],[refute_0_2,refute_0_105]) ).
cnf(refute_0_107,plain,
( ~ act(f1,X_266)
| ~ activates(e1,f1)
| bearer(skolemFOFtoCNF_S(X_266,e1,f1,concert_ds,marketplace,philharmonie),marketplace) ),
inference(subst,[],[refute_0_106:[bind(X_263,$fot(X_266)),bind(X_264,$fot(e1))]]) ).
cnf(refute_0_108,plain,
( ~ act(f1,X_266)
| bearer(skolemFOFtoCNF_S(X_266,e1,f1,concert_ds,marketplace,philharmonie),marketplace) ),
inference(resolve,[$cnf( activates(e1,f1) )],[refute_0_1,refute_0_107]) ).
cnf(refute_0_109,plain,
( ~ act(f1,distrib)
| bearer(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),marketplace) ),
inference(subst,[],[refute_0_108:[bind(X_266,$fot(distrib))]]) ).
cnf(refute_0_110,plain,
bearer(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),marketplace),
inference(resolve,[$cnf( act(f1,distrib) )],[refute_0_0,refute_0_109]) ).
cnf(refute_0_111,plain,
( ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ founds_rem(e1,RhoR,f1)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR)
| ~ part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR)
| ~ subjection(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( bearer(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),marketplace) )],[refute_0_110,refute_0_97]) ).
cnf(refute_0_112,plain,
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| subjection(skolemFOFtoCNF_S(A,E,F,T,X,Y)) ),
inference(canonicalize,[],[normalize_0_22]) ).
cnf(refute_0_113,plain,
( ~ act(f1,X_173)
| ~ activates(X_174,f1)
| ~ aee(f1,X_177)
| ~ aer(f1,X_178)
| ~ has_rem(f1)
| ~ proh(f1)
| ~ tgt(f1,concert_ds)
| subjection(skolemFOFtoCNF_S(X_173,X_174,f1,concert_ds,X_177,X_178)) ),
inference(subst,[],[refute_0_112:[bind(A,$fot(X_173)),bind(E,$fot(X_174)),bind(F,$fot(f1)),bind(T,$fot(concert_ds)),bind(X,$fot(X_177)),bind(Y,$fot(X_178))]]) ).
cnf(refute_0_114,plain,
( ~ act(f1,X_173)
| ~ activates(X_174,f1)
| ~ aee(f1,X_177)
| ~ aer(f1,X_178)
| ~ has_rem(f1)
| ~ proh(f1)
| subjection(skolemFOFtoCNF_S(X_173,X_174,f1,concert_ds,X_177,X_178)) ),
inference(resolve,[$cnf( tgt(f1,concert_ds) )],[refute_0_4,refute_0_113]) ).
cnf(refute_0_115,plain,
( ~ act(f1,X_173)
| ~ activates(X_174,f1)
| ~ aee(f1,X_177)
| ~ aer(f1,X_178)
| ~ proh(f1)
| subjection(skolemFOFtoCNF_S(X_173,X_174,f1,concert_ds,X_177,X_178)) ),
inference(resolve,[$cnf( has_rem(f1) )],[refute_0_8,refute_0_114]) ).
cnf(refute_0_116,plain,
( ~ act(f1,X_173)
| ~ activates(X_174,f1)
| ~ aee(f1,X_177)
| ~ aer(f1,X_178)
| subjection(skolemFOFtoCNF_S(X_173,X_174,f1,concert_ds,X_177,X_178)) ),
inference(resolve,[$cnf( proh(f1) )],[refute_0_10,refute_0_115]) ).
cnf(refute_0_117,plain,
( ~ act(f1,X_179)
| ~ activates(X_180,f1)
| ~ aee(f1,X_181)
| ~ aer(f1,philharmonie)
| subjection(skolemFOFtoCNF_S(X_179,X_180,f1,concert_ds,X_181,philharmonie)) ),
inference(subst,[],[refute_0_116:[bind(X_173,$fot(X_179)),bind(X_174,$fot(X_180)),bind(X_177,$fot(X_181)),bind(X_178,$fot(philharmonie))]]) ).
cnf(refute_0_118,plain,
( ~ act(f1,X_179)
| ~ activates(X_180,f1)
| ~ aee(f1,X_181)
| subjection(skolemFOFtoCNF_S(X_179,X_180,f1,concert_ds,X_181,philharmonie)) ),
inference(resolve,[$cnf( aer(f1,philharmonie) )],[refute_0_3,refute_0_117]) ).
cnf(refute_0_119,plain,
( ~ act(f1,X_183)
| ~ activates(X_184,f1)
| ~ aee(f1,marketplace)
| subjection(skolemFOFtoCNF_S(X_183,X_184,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_118:[bind(X_179,$fot(X_183)),bind(X_180,$fot(X_184)),bind(X_181,$fot(marketplace))]]) ).
cnf(refute_0_120,plain,
( ~ act(f1,X_183)
| ~ activates(X_184,f1)
| subjection(skolemFOFtoCNF_S(X_183,X_184,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( aee(f1,marketplace) )],[refute_0_2,refute_0_119]) ).
cnf(refute_0_121,plain,
( ~ act(f1,X_186)
| ~ activates(e1,f1)
| subjection(skolemFOFtoCNF_S(X_186,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_120:[bind(X_183,$fot(X_186)),bind(X_184,$fot(e1))]]) ).
cnf(refute_0_122,plain,
( ~ act(f1,X_186)
| subjection(skolemFOFtoCNF_S(X_186,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( activates(e1,f1) )],[refute_0_1,refute_0_121]) ).
cnf(refute_0_123,plain,
( ~ act(f1,distrib)
| subjection(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_122:[bind(X_186,$fot(distrib))]]) ).
cnf(refute_0_124,plain,
subjection(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie)),
inference(resolve,[$cnf( act(f1,distrib) )],[refute_0_0,refute_0_123]) ).
cnf(refute_0_125,plain,
( ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ founds_rem(e1,RhoR,f1)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR)
| ~ part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),RhoR) ),
inference(resolve,[$cnf( subjection(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie)) )],[refute_0_124,refute_0_111]) ).
cnf(refute_0_126,plain,
( ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ founds_rem(e1,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie),f1)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| ~ part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_125:[bind(RhoR,$fot(skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)))]]) ).
cnf(refute_0_127,plain,
( ~ act(F,A)
| ~ activates(E,F)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ has_rem(F)
| ~ proh(F)
| ~ tgt(F,T)
| part_of(skolemFOFtoCNF_S(A,E,F,T,X,Y),skolemFOFtoCNF_RhoR(A,E,F,T,X,Y)) ),
inference(canonicalize,[],[normalize_0_23]) ).
cnf(refute_0_128,plain,
( ~ act(f1,X_346)
| ~ activates(X_347,f1)
| ~ aee(f1,X_350)
| ~ aer(f1,X_351)
| ~ has_rem(f1)
| ~ proh(f1)
| ~ tgt(f1,concert_ds)
| part_of(skolemFOFtoCNF_S(X_346,X_347,f1,concert_ds,X_350,X_351),skolemFOFtoCNF_RhoR(X_346,X_347,f1,concert_ds,X_350,X_351)) ),
inference(subst,[],[refute_0_127:[bind(A,$fot(X_346)),bind(E,$fot(X_347)),bind(F,$fot(f1)),bind(T,$fot(concert_ds)),bind(X,$fot(X_350)),bind(Y,$fot(X_351))]]) ).
cnf(refute_0_129,plain,
( ~ act(f1,X_346)
| ~ activates(X_347,f1)
| ~ aee(f1,X_350)
| ~ aer(f1,X_351)
| ~ has_rem(f1)
| ~ proh(f1)
| part_of(skolemFOFtoCNF_S(X_346,X_347,f1,concert_ds,X_350,X_351),skolemFOFtoCNF_RhoR(X_346,X_347,f1,concert_ds,X_350,X_351)) ),
inference(resolve,[$cnf( tgt(f1,concert_ds) )],[refute_0_4,refute_0_128]) ).
cnf(refute_0_130,plain,
( ~ act(f1,X_346)
| ~ activates(X_347,f1)
| ~ aee(f1,X_350)
| ~ aer(f1,X_351)
| ~ proh(f1)
| part_of(skolemFOFtoCNF_S(X_346,X_347,f1,concert_ds,X_350,X_351),skolemFOFtoCNF_RhoR(X_346,X_347,f1,concert_ds,X_350,X_351)) ),
inference(resolve,[$cnf( has_rem(f1) )],[refute_0_8,refute_0_129]) ).
cnf(refute_0_131,plain,
( ~ act(f1,X_346)
| ~ activates(X_347,f1)
| ~ aee(f1,X_350)
| ~ aer(f1,X_351)
| part_of(skolemFOFtoCNF_S(X_346,X_347,f1,concert_ds,X_350,X_351),skolemFOFtoCNF_RhoR(X_346,X_347,f1,concert_ds,X_350,X_351)) ),
inference(resolve,[$cnf( proh(f1) )],[refute_0_10,refute_0_130]) ).
cnf(refute_0_132,plain,
( ~ act(f1,X_352)
| ~ activates(X_353,f1)
| ~ aee(f1,X_354)
| ~ aer(f1,philharmonie)
| part_of(skolemFOFtoCNF_S(X_352,X_353,f1,concert_ds,X_354,philharmonie),skolemFOFtoCNF_RhoR(X_352,X_353,f1,concert_ds,X_354,philharmonie)) ),
inference(subst,[],[refute_0_131:[bind(X_346,$fot(X_352)),bind(X_347,$fot(X_353)),bind(X_350,$fot(X_354)),bind(X_351,$fot(philharmonie))]]) ).
cnf(refute_0_133,plain,
( ~ act(f1,X_352)
| ~ activates(X_353,f1)
| ~ aee(f1,X_354)
| part_of(skolemFOFtoCNF_S(X_352,X_353,f1,concert_ds,X_354,philharmonie),skolemFOFtoCNF_RhoR(X_352,X_353,f1,concert_ds,X_354,philharmonie)) ),
inference(resolve,[$cnf( aer(f1,philharmonie) )],[refute_0_3,refute_0_132]) ).
cnf(refute_0_134,plain,
( ~ act(f1,X_356)
| ~ activates(X_357,f1)
| ~ aee(f1,marketplace)
| part_of(skolemFOFtoCNF_S(X_356,X_357,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(X_356,X_357,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_133:[bind(X_352,$fot(X_356)),bind(X_353,$fot(X_357)),bind(X_354,$fot(marketplace))]]) ).
cnf(refute_0_135,plain,
( ~ act(f1,X_356)
| ~ activates(X_357,f1)
| part_of(skolemFOFtoCNF_S(X_356,X_357,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(X_356,X_357,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( aee(f1,marketplace) )],[refute_0_2,refute_0_134]) ).
cnf(refute_0_136,plain,
( ~ act(f1,X_359)
| ~ activates(e1,f1)
| part_of(skolemFOFtoCNF_S(X_359,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(X_359,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_135:[bind(X_356,$fot(X_359)),bind(X_357,$fot(e1))]]) ).
cnf(refute_0_137,plain,
( ~ act(f1,X_359)
| part_of(skolemFOFtoCNF_S(X_359,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(X_359,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( activates(e1,f1) )],[refute_0_1,refute_0_136]) ).
cnf(refute_0_138,plain,
( ~ act(f1,distrib)
| part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(subst,[],[refute_0_137:[bind(X_359,$fot(distrib))]]) ).
cnf(refute_0_139,plain,
part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)),
inference(resolve,[$cnf( act(f1,distrib) )],[refute_0_0,refute_0_138]) ).
cnf(refute_0_140,plain,
( ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ founds_rem(e1,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie),f1)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)) )],[refute_0_139,refute_0_126]) ).
cnf(refute_0_141,plain,
( ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( founds_rem(e1,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie),f1) )],[refute_0_34,refute_0_140]) ).
cnf(refute_0_142,plain,
( ~ cnt(S,decl(A),T)
| ~ founds_rem(E,Rho,R)
| ~ part_of(S,Rho)
| ~ subjection(S)
| about_event(S,E) ),
inference(canonicalize,[],[normalize_0_26]) ).
cnf(refute_0_143,plain,
( ~ cnt(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds)
| ~ founds_rem(E,Rho,R)
| ~ part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),Rho)
| ~ subjection(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),E) ),
inference(subst,[],[refute_0_142:[bind(A,$fot(distrib)),bind(S,$fot(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie))),bind(T,$fot(concert_ds))]]) ).
cnf(refute_0_144,plain,
( ~ founds_rem(E,Rho,R)
| ~ part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),Rho)
| ~ subjection(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),E) ),
inference(resolve,[$cnf( cnt(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds) )],[refute_0_96,refute_0_143]) ).
cnf(refute_0_145,plain,
( ~ founds_rem(E,Rho,R)
| ~ part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),Rho)
| about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),E) ),
inference(resolve,[$cnf( subjection(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie)) )],[refute_0_124,refute_0_144]) ).
cnf(refute_0_146,plain,
( ~ founds_rem(E,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie),R)
| ~ part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie))
| about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),E) ),
inference(subst,[],[refute_0_145:[bind(Rho,$fot(skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)))]]) ).
cnf(refute_0_147,plain,
( ~ founds_rem(E,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie),R)
| about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),E) ),
inference(resolve,[$cnf( part_of(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)) )],[refute_0_139,refute_0_146]) ).
cnf(refute_0_148,plain,
( ~ founds_rem(e1,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie),f1)
| about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1) ),
inference(subst,[],[refute_0_147:[bind(E,$fot(e1)),bind(R,$fot(f1))]]) ).
cnf(refute_0_149,plain,
about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1),
inference(resolve,[$cnf( founds_rem(e1,skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie),f1) )],[refute_0_34,refute_0_148]) ).
cnf(refute_0_150,plain,
( ~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1)
| ~ part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)) ),
inference(resolve,[$cnf( about_event(skolemFOFtoCNF_S(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1) )],[refute_0_149,refute_0_141]) ).
cnf(refute_0_151,plain,
~ about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1),
inference(resolve,[$cnf( part_of(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),skolemFOFtoCNF_RhoR(distrib,e1,f1,concert_ds,marketplace,philharmonie)) )],[refute_0_49,refute_0_150]) ).
cnf(refute_0_152,plain,
~ cnt(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(A),T),
inference(resolve,[$cnf( about_event(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),e1) )],[refute_0_64,refute_0_151]) ).
cnf(refute_0_153,plain,
~ cnt(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds),
inference(subst,[],[refute_0_152:[bind(A,$fot(distrib)),bind(T,$fot(concert_ds))]]) ).
cnf(refute_0_154,plain,
$false,
inference(resolve,[$cnf( cnt(skolemFOFtoCNF_Pw(distrib,e1,f1,concert_ds,marketplace,philharmonie),decl(distrib),concert_ds) )],[refute_0_19,refute_0_153]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.10/0.37 % Computer : n011.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 7 14:07:15 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.24/0.48 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.24/0.48
% 0.24/0.48 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.24/0.52
%------------------------------------------------------------------------------