%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : MGT113+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 : Sun Sep 27 08:03:08 AM UTC 2026
% Result : Theorem 0.08s 0.39s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 11
% Syntax : Number of formulae : 116 ( 27 unt; 0 def)
% Number of atoms : 587 ( 0 equ)
% Maximal formula atoms : 72 ( 5 avg)
% Number of connectives : 888 ( 417 ~; 404 |; 64 &)
% ( 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 : 319 ( 20 sgn 84 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax_proh_relator_remedy,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('theBenchmark.p',ax_proh_relator_remedy) ).
fof(ax_B2,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('theBenchmark.p',ax_B2) ).
fof(ax_B3,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('theBenchmark.p',ax_B3) ).
fof(conjecture,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('theBenchmark.p',conjecture) ).
fof(conjecture_neg,negated_conjecture,
~ ? [RhoR,Pw,S] :
( about_event(S,e1)
& part_of(S,RhoR)
& cnt(S,decl(distrib),concert_ds)
& bearer(S,marketplace)
& subjection(S)
& about_event(Pw,e1)
& part_of(Pw,RhoR)
& cnt(Pw,decl(distrib),concert_ds)
& bearer(Pw,philharmonie)
& power(Pw)
& founds_rem(e1,RhoR,f1) ),
inference(assume_negation,[status(cth)],[conjecture]) ).
fof(proh_f1,axiom,
proh(f1),
file('theBenchmark.p',proh_f1) ).
cnf(c_11,plain,
proh(f1),
inference(clausify,[status(thm)],[proh_f1]) ).
fof(nnf_2,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(fof_nnf,[status(thm)],[ax_proh_relator_remedy]) ).
fof(sk_ax_proh_relator_remedy_sk,plain,
! [F,X,Y,A,T,E] :
( ( part_of(sK0(F,X,Y,A,T,E),sK1(F,X,Y,A,T,E))
& cnt(sK0(F,X,Y,A,T,E),decl(A),T)
& bearer(sK0(F,X,Y,A,T,E),X)
& subjection(sK0(F,X,Y,A,T,E))
& part_of(sK2(F,X,Y,A,T,E),sK1(F,X,Y,A,T,E))
& cnt(sK2(F,X,Y,A,T,E),decl(A),T)
& bearer(sK2(F,X,Y,A,T,E),Y)
& power(sK2(F,X,Y,A,T,E))
& founds_rem(E,sK1(F,X,Y,A,T,E),F) )
| ~ activates(E,F)
| ~ tgt(F,T)
| ~ act(F,A)
| ~ aer(F,Y)
| ~ aee(F,X)
| ~ has_rem(F)
| ~ proh(F) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK0]),skolemize(RhoR,sK1(F,X,Y,A,T,E)),skolemize(Pw,sK2(F,X,Y,A,T,E)),skolemize(S,sK0(F,X,Y,A,T,E))],[nnf_2]) ).
fof(sk_ax_proh_relator_remedy,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( part_of(sK0(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5),sK1(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5))
| ~ activates(VAR_5,VAR_0)
| ~ tgt(VAR_0,VAR_4)
| ~ act(VAR_0,VAR_3)
| ~ aer(VAR_0,VAR_2)
| ~ aee(VAR_0,VAR_1)
| ~ has_rem(VAR_0)
| ~ proh(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( cnt(sK0(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5),decl(VAR_3),VAR_4)
| ~ activates(VAR_5,VAR_0)
| ~ tgt(VAR_0,VAR_4)
| ~ act(VAR_0,VAR_3)
| ~ aer(VAR_0,VAR_2)
| ~ aee(VAR_0,VAR_1)
| ~ has_rem(VAR_0)
| ~ proh(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( bearer(sK0(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5),VAR_1)
| ~ activates(VAR_5,VAR_0)
| ~ tgt(VAR_0,VAR_4)
| ~ act(VAR_0,VAR_3)
| ~ aer(VAR_0,VAR_2)
| ~ aee(VAR_0,VAR_1)
| ~ has_rem(VAR_0)
| ~ proh(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( subjection(sK0(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5))
| ~ activates(VAR_5,VAR_0)
| ~ tgt(VAR_0,VAR_4)
| ~ act(VAR_0,VAR_3)
| ~ aer(VAR_0,VAR_2)
| ~ aee(VAR_0,VAR_1)
| ~ has_rem(VAR_0)
| ~ proh(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( part_of(sK2(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5),sK1(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5))
| ~ activates(VAR_5,VAR_0)
| ~ tgt(VAR_0,VAR_4)
| ~ act(VAR_0,VAR_3)
| ~ aer(VAR_0,VAR_2)
| ~ aee(VAR_0,VAR_1)
| ~ has_rem(VAR_0)
| ~ proh(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( cnt(sK2(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5),decl(VAR_3),VAR_4)
| ~ activates(VAR_5,VAR_0)
| ~ tgt(VAR_0,VAR_4)
| ~ act(VAR_0,VAR_3)
| ~ aer(VAR_0,VAR_2)
| ~ aee(VAR_0,VAR_1)
| ~ has_rem(VAR_0)
| ~ proh(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( bearer(sK2(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5),VAR_2)
| ~ activates(VAR_5,VAR_0)
| ~ tgt(VAR_0,VAR_4)
| ~ act(VAR_0,VAR_3)
| ~ aer(VAR_0,VAR_2)
| ~ aee(VAR_0,VAR_1)
| ~ has_rem(VAR_0)
| ~ proh(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( power(sK2(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5))
| ~ activates(VAR_5,VAR_0)
| ~ tgt(VAR_0,VAR_4)
| ~ act(VAR_0,VAR_3)
| ~ aer(VAR_0,VAR_2)
| ~ aee(VAR_0,VAR_1)
| ~ has_rem(VAR_0)
| ~ proh(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( founds_rem(VAR_5,sK1(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5),VAR_0)
| ~ activates(VAR_5,VAR_0)
| ~ tgt(VAR_0,VAR_4)
| ~ act(VAR_0,VAR_3)
| ~ aer(VAR_0,VAR_2)
| ~ aee(VAR_0,VAR_1)
| ~ has_rem(VAR_0)
| ~ proh(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_ax_proh_relator_remedy_sk]) ).
cnf(c_13,plain,
( part_of(sK0(A,B,C,D,E,F),sK1(A,B,C,D,E,F))
| ~ activates(F,A)
| ~ tgt(A,E)
| ~ act(A,D)
| ~ aer(A,C)
| ~ aee(A,B)
| ~ has_rem(A)
| ~ proh(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_proh_relator_remedy]) ).
cnf(c_14,plain,
( cnt(sK0(A,B,C,D,E,F),decl(D),E)
| ~ activates(F,A)
| ~ tgt(A,E)
| ~ act(A,D)
| ~ aer(A,C)
| ~ aee(A,B)
| ~ has_rem(A)
| ~ proh(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_proh_relator_remedy]) ).
cnf(c_15,plain,
( bearer(sK0(A,B,C,D,E,F),B)
| ~ activates(F,A)
| ~ tgt(A,E)
| ~ act(A,D)
| ~ aer(A,C)
| ~ aee(A,B)
| ~ has_rem(A)
| ~ proh(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_proh_relator_remedy]) ).
cnf(c_16,plain,
( subjection(sK0(A,B,C,D,E,F))
| ~ activates(F,A)
| ~ tgt(A,E)
| ~ act(A,D)
| ~ aer(A,C)
| ~ aee(A,B)
| ~ has_rem(A)
| ~ proh(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_proh_relator_remedy]) ).
cnf(c_17,plain,
( part_of(sK2(A,B,C,D,E,F),sK1(A,B,C,D,E,F))
| ~ activates(F,A)
| ~ tgt(A,E)
| ~ act(A,D)
| ~ aer(A,C)
| ~ aee(A,B)
| ~ has_rem(A)
| ~ proh(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_proh_relator_remedy]) ).
cnf(c_18,plain,
( cnt(sK2(A,B,C,D,E,F),decl(D),E)
| ~ activates(F,A)
| ~ tgt(A,E)
| ~ act(A,D)
| ~ aer(A,C)
| ~ aee(A,B)
| ~ has_rem(A)
| ~ proh(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_proh_relator_remedy]) ).
cnf(c_19,plain,
( bearer(sK2(A,B,C,D,E,F),C)
| ~ activates(F,A)
| ~ tgt(A,E)
| ~ act(A,D)
| ~ aer(A,C)
| ~ aee(A,B)
| ~ has_rem(A)
| ~ proh(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_proh_relator_remedy]) ).
cnf(c_20,plain,
( power(sK2(A,B,C,D,E,F))
| ~ activates(F,A)
| ~ tgt(A,E)
| ~ act(A,D)
| ~ aer(A,C)
| ~ aee(A,B)
| ~ has_rem(A)
| ~ proh(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_proh_relator_remedy]) ).
cnf(c_21,plain,
( founds_rem(F,sK1(A,B,C,D,E,F),A)
| ~ activates(F,A)
| ~ tgt(A,E)
| ~ act(A,D)
| ~ aer(A,C)
| ~ aee(A,B)
| ~ has_rem(A)
| ~ proh(A) ),
inference(split_conjunct,[status(thm)],[sk_ax_proh_relator_remedy]) ).
fof(aee_f1,axiom,
aee(f1,marketplace),
file('theBenchmark.p',aee_f1) ).
cnf(c_31,plain,
aee(f1,marketplace),
inference(clausify,[status(thm)],[aee_f1]) ).
cnf(c_34,plain,
( part_of(sK0(f1,A,B,C,D,E),sK1(f1,A,B,C,D,E))
| ~ activates(E,f1)
| ~ tgt(f1,D)
| ~ act(f1,C)
| ~ aer(f1,B)
| ~ aee(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_13,c_11]) ).
cnf(c_35,plain,
( cnt(sK0(f1,A,B,C,D,E),decl(C),D)
| ~ activates(E,f1)
| ~ tgt(f1,D)
| ~ act(f1,C)
| ~ aer(f1,B)
| ~ aee(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_14,c_11]) ).
cnf(c_36,plain,
( bearer(sK0(f1,A,B,C,D,E),A)
| ~ activates(E,f1)
| ~ tgt(f1,D)
| ~ act(f1,C)
| ~ aer(f1,B)
| ~ aee(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_15,c_11]) ).
cnf(c_37,plain,
( subjection(sK0(f1,A,B,C,D,E))
| ~ activates(E,f1)
| ~ tgt(f1,D)
| ~ act(f1,C)
| ~ aer(f1,B)
| ~ aee(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_16,c_11]) ).
cnf(c_38,plain,
( part_of(sK2(f1,A,B,C,D,E),sK1(f1,A,B,C,D,E))
| ~ activates(E,f1)
| ~ tgt(f1,D)
| ~ act(f1,C)
| ~ aer(f1,B)
| ~ aee(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_17,c_11]) ).
cnf(c_39,plain,
( cnt(sK2(f1,A,B,C,D,E),decl(C),D)
| ~ activates(E,f1)
| ~ tgt(f1,D)
| ~ act(f1,C)
| ~ aer(f1,B)
| ~ aee(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_18,c_11]) ).
cnf(c_40,plain,
( bearer(sK2(f1,A,B,C,D,E),B)
| ~ activates(E,f1)
| ~ tgt(f1,D)
| ~ act(f1,C)
| ~ aer(f1,B)
| ~ aee(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_19,c_11]) ).
cnf(c_41,plain,
( power(sK2(f1,A,B,C,D,E))
| ~ activates(E,f1)
| ~ tgt(f1,D)
| ~ act(f1,C)
| ~ aer(f1,B)
| ~ aee(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_20,c_11]) ).
cnf(c_42,plain,
( founds_rem(E,sK1(f1,A,B,C,D,E),f1)
| ~ activates(E,f1)
| ~ tgt(f1,D)
| ~ act(f1,C)
| ~ aer(f1,B)
| ~ aee(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_21,c_11]) ).
fof(aer_f1,axiom,
aer(f1,philharmonie),
file('theBenchmark.p',aer_f1) ).
cnf(c_52,plain,
aer(f1,philharmonie),
inference(clausify,[status(thm)],[aer_f1]) ).
cnf(c_53,plain,
( part_of(sK0(f1,marketplace,A,B,C,D),sK1(f1,marketplace,A,B,C,D))
| ~ activates(D,f1)
| ~ tgt(f1,C)
| ~ act(f1,B)
| ~ aer(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_31,c_34]) ).
cnf(c_54,plain,
( cnt(sK0(f1,marketplace,A,B,C,D),decl(B),C)
| ~ activates(D,f1)
| ~ tgt(f1,C)
| ~ act(f1,B)
| ~ aer(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_31,c_35]) ).
cnf(c_55,plain,
( bearer(sK0(f1,marketplace,A,B,C,D),marketplace)
| ~ activates(D,f1)
| ~ tgt(f1,C)
| ~ act(f1,B)
| ~ aer(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_31,c_36]) ).
cnf(c_56,plain,
( subjection(sK0(f1,marketplace,A,B,C,D))
| ~ activates(D,f1)
| ~ tgt(f1,C)
| ~ act(f1,B)
| ~ aer(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_31,c_37]) ).
cnf(c_57,plain,
( part_of(sK2(f1,marketplace,A,B,C,D),sK1(f1,marketplace,A,B,C,D))
| ~ activates(D,f1)
| ~ tgt(f1,C)
| ~ act(f1,B)
| ~ aer(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_31,c_38]) ).
cnf(c_58,plain,
( cnt(sK2(f1,marketplace,A,B,C,D),decl(B),C)
| ~ activates(D,f1)
| ~ tgt(f1,C)
| ~ act(f1,B)
| ~ aer(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_31,c_39]) ).
cnf(c_59,plain,
( bearer(sK2(f1,marketplace,A,B,C,D),A)
| ~ activates(D,f1)
| ~ tgt(f1,C)
| ~ act(f1,B)
| ~ aer(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_31,c_40]) ).
cnf(c_60,plain,
( power(sK2(f1,marketplace,A,B,C,D))
| ~ activates(D,f1)
| ~ tgt(f1,C)
| ~ act(f1,B)
| ~ aer(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_31,c_41]) ).
cnf(c_61,plain,
( founds_rem(D,sK1(f1,marketplace,A,B,C,D),f1)
| ~ activates(D,f1)
| ~ tgt(f1,C)
| ~ act(f1,B)
| ~ aer(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_31,c_42]) ).
fof(act_f1,axiom,
act(f1,distrib),
file('theBenchmark.p',act_f1) ).
cnf(c_71,plain,
act(f1,distrib),
inference(clausify,[status(thm)],[act_f1]) ).
cnf(c_72,plain,
( part_of(sK0(f1,marketplace,philharmonie,A,B,C),sK1(f1,marketplace,philharmonie,A,B,C))
| ~ activates(C,f1)
| ~ tgt(f1,B)
| ~ act(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_52,c_53]) ).
cnf(c_73,plain,
( cnt(sK0(f1,marketplace,philharmonie,A,B,C),decl(A),B)
| ~ activates(C,f1)
| ~ tgt(f1,B)
| ~ act(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_52,c_54]) ).
cnf(c_74,plain,
( bearer(sK0(f1,marketplace,philharmonie,A,B,C),marketplace)
| ~ activates(C,f1)
| ~ tgt(f1,B)
| ~ act(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_52,c_55]) ).
cnf(c_75,plain,
( subjection(sK0(f1,marketplace,philharmonie,A,B,C))
| ~ activates(C,f1)
| ~ tgt(f1,B)
| ~ act(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_52,c_56]) ).
cnf(c_76,plain,
( part_of(sK2(f1,marketplace,philharmonie,A,B,C),sK1(f1,marketplace,philharmonie,A,B,C))
| ~ activates(C,f1)
| ~ tgt(f1,B)
| ~ act(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_52,c_57]) ).
cnf(c_77,plain,
( cnt(sK2(f1,marketplace,philharmonie,A,B,C),decl(A),B)
| ~ activates(C,f1)
| ~ tgt(f1,B)
| ~ act(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_52,c_58]) ).
cnf(c_78,plain,
( bearer(sK2(f1,marketplace,philharmonie,A,B,C),philharmonie)
| ~ activates(C,f1)
| ~ tgt(f1,B)
| ~ act(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_52,c_59]) ).
cnf(c_79,plain,
( power(sK2(f1,marketplace,philharmonie,A,B,C))
| ~ activates(C,f1)
| ~ tgt(f1,B)
| ~ act(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_52,c_60]) ).
cnf(c_80,plain,
( founds_rem(C,sK1(f1,marketplace,philharmonie,A,B,C),f1)
| ~ activates(C,f1)
| ~ tgt(f1,B)
| ~ act(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_52,c_61]) ).
fof(tgt_f1,axiom,
tgt(f1,concert_ds),
file('theBenchmark.p',tgt_f1) ).
cnf(c_92,plain,
tgt(f1,concert_ds),
inference(clausify,[status(thm)],[tgt_f1]) ).
cnf(c_93,plain,
( part_of(sK0(f1,marketplace,philharmonie,distrib,A,B),sK1(f1,marketplace,philharmonie,distrib,A,B))
| ~ activates(B,f1)
| ~ tgt(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_71,c_72]) ).
cnf(c_94,plain,
( cnt(sK0(f1,marketplace,philharmonie,distrib,A,B),decl(distrib),A)
| ~ activates(B,f1)
| ~ tgt(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_71,c_73]) ).
cnf(c_95,plain,
( bearer(sK0(f1,marketplace,philharmonie,distrib,A,B),marketplace)
| ~ activates(B,f1)
| ~ tgt(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_71,c_74]) ).
cnf(c_96,plain,
( subjection(sK0(f1,marketplace,philharmonie,distrib,A,B))
| ~ activates(B,f1)
| ~ tgt(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_71,c_75]) ).
cnf(c_97,plain,
( part_of(sK2(f1,marketplace,philharmonie,distrib,A,B),sK1(f1,marketplace,philharmonie,distrib,A,B))
| ~ activates(B,f1)
| ~ tgt(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_71,c_76]) ).
cnf(c_98,plain,
( cnt(sK2(f1,marketplace,philharmonie,distrib,A,B),decl(distrib),A)
| ~ activates(B,f1)
| ~ tgt(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_71,c_77]) ).
cnf(c_99,plain,
( bearer(sK2(f1,marketplace,philharmonie,distrib,A,B),philharmonie)
| ~ activates(B,f1)
| ~ tgt(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_71,c_78]) ).
cnf(c_100,plain,
( power(sK2(f1,marketplace,philharmonie,distrib,A,B))
| ~ activates(B,f1)
| ~ tgt(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_71,c_79]) ).
cnf(c_101,plain,
( founds_rem(B,sK1(f1,marketplace,philharmonie,distrib,A,B),f1)
| ~ activates(B,f1)
| ~ tgt(f1,A)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_71,c_80]) ).
fof(act_e1_f1,axiom,
activates(e1,f1),
file('theBenchmark.p',act_e1_f1) ).
cnf(c_113,plain,
activates(e1,f1),
inference(clausify,[status(thm)],[act_e1_f1]) ).
cnf(c_114,plain,
( part_of(sK0(f1,marketplace,philharmonie,distrib,concert_ds,A),sK1(f1,marketplace,philharmonie,distrib,concert_ds,A))
| ~ activates(A,f1)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_92,c_93]) ).
cnf(c_115,plain,
( cnt(sK0(f1,marketplace,philharmonie,distrib,concert_ds,A),decl(distrib),concert_ds)
| ~ activates(A,f1)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_92,c_94]) ).
cnf(c_116,plain,
( bearer(sK0(f1,marketplace,philharmonie,distrib,concert_ds,A),marketplace)
| ~ activates(A,f1)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_92,c_95]) ).
cnf(c_117,plain,
( subjection(sK0(f1,marketplace,philharmonie,distrib,concert_ds,A))
| ~ activates(A,f1)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_92,c_96]) ).
cnf(c_118,plain,
( part_of(sK2(f1,marketplace,philharmonie,distrib,concert_ds,A),sK1(f1,marketplace,philharmonie,distrib,concert_ds,A))
| ~ activates(A,f1)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_92,c_97]) ).
cnf(c_119,plain,
( cnt(sK2(f1,marketplace,philharmonie,distrib,concert_ds,A),decl(distrib),concert_ds)
| ~ activates(A,f1)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_92,c_98]) ).
cnf(c_120,plain,
( bearer(sK2(f1,marketplace,philharmonie,distrib,concert_ds,A),philharmonie)
| ~ activates(A,f1)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_92,c_99]) ).
cnf(c_121,plain,
( power(sK2(f1,marketplace,philharmonie,distrib,concert_ds,A))
| ~ activates(A,f1)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_92,c_100]) ).
cnf(c_122,plain,
( founds_rem(A,sK1(f1,marketplace,philharmonie,distrib,concert_ds,A),f1)
| ~ activates(A,f1)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_92,c_101]) ).
fof(rem_f1,axiom,
has_rem(f1),
file('theBenchmark.p',rem_f1) ).
cnf(c_132,plain,
has_rem(f1),
inference(clausify,[status(thm)],[rem_f1]) ).
cnf(c_135,plain,
( part_of(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_113,c_114]) ).
cnf(c_136,plain,
( cnt(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_113,c_115]) ).
cnf(c_137,plain,
( bearer(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_113,c_116]) ).
cnf(c_138,plain,
( subjection(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_113,c_117]) ).
cnf(c_139,plain,
( part_of(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_113,c_118]) ).
cnf(c_140,plain,
( cnt(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_113,c_119]) ).
cnf(c_141,plain,
( bearer(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_113,c_120]) ).
cnf(c_142,plain,
( power(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_113,c_121]) ).
cnf(c_143,plain,
( founds_rem(e1,sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1)
| ~ has_rem(f1) ),
inference(resolve,[status(thm)],[c_113,c_122]) ).
cnf(c_144,negated_conjecture,
( ~ about_event(C,e1)
| ~ part_of(C,A)
| ~ cnt(C,decl(distrib),concert_ds)
| ~ bearer(C,marketplace)
| ~ subjection(C)
| ~ about_event(B,e1)
| ~ part_of(B,A)
| ~ cnt(B,decl(distrib),concert_ds)
| ~ bearer(B,philharmonie)
| ~ power(B)
| ~ founds_rem(e1,A,f1) ),
inference(clausify,[status(thm)],[conjecture_neg]) ).
cnf(c_145,plain,
founds_rem(e1,sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1),
inference(resolve,[status(thm)],[c_143,c_132]) ).
cnf(c_146,plain,
( about_event(A,E)
| ~ founds_rem(E,D,F)
| ~ part_of(A,D)
| ~ cnt(A,decl(B),C)
| ~ subjection(A) ),
inference(clausify,[status(thm)],[ax_B3]) ).
cnf(c_147,plain,
( about_event(A,E)
| ~ founds_rem(E,D,F)
| ~ part_of(A,D)
| ~ cnt(A,decl(B),C)
| ~ power(A) ),
inference(clausify,[status(thm)],[ax_B2]) ).
cnf(c_149,negated_conjecture,
( ~ about_event(B,e1)
| ~ part_of(B,sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(B,decl(distrib),concert_ds)
| ~ bearer(B,marketplace)
| ~ subjection(B)
| ~ about_event(A,e1)
| ~ part_of(A,sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(A,decl(distrib),concert_ds)
| ~ bearer(A,philharmonie)
| ~ power(A) ),
inference(resolve,[status(thm)],[c_144,c_145]) ).
cnf(c_150,plain,
( about_event(A,e1)
| ~ part_of(A,sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(A,decl(B),C)
| ~ power(A) ),
inference(resolve,[status(thm)],[c_147,c_145]) ).
cnf(c_151,plain,
power(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1)),
inference(resolve,[status(thm)],[c_142,c_132]) ).
cnf(c_152,plain,
subjection(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1)),
inference(resolve,[status(thm)],[c_138,c_132]) ).
cnf(c_154,negated_conjecture,
( ~ about_event(A,e1)
| ~ part_of(A,sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(A,decl(distrib),concert_ds)
| ~ bearer(A,marketplace)
| ~ subjection(A)
| ~ about_event(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ bearer(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie) ),
inference(resolve,[status(thm)],[c_151,c_149]) ).
cnf(c_156,plain,
( about_event(A,e1)
| ~ part_of(A,sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(A,decl(B),C)
| ~ subjection(A) ),
inference(resolve,[status(thm)],[c_146,c_145]) ).
cnf(c_165,plain,
( about_event(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B) ),
inference(resolve,[status(thm)],[c_151,c_150]) ).
cnf(c_167,plain,
bearer(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie),
inference(resolve,[status(thm)],[c_141,c_132]) ).
cnf(c_168,plain,
cnt(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),
inference(resolve,[status(thm)],[c_140,c_132]) ).
cnf(c_169,plain,
part_of(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1)),
inference(resolve,[status(thm)],[c_139,c_132]) ).
cnf(c_170,plain,
bearer(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace),
inference(resolve,[status(thm)],[c_137,c_132]) ).
cnf(c_171,plain,
cnt(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds),
inference(resolve,[status(thm)],[c_136,c_132]) ).
cnf(c_172,plain,
part_of(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1)),
inference(resolve,[status(thm)],[c_135,c_132]) ).
cnf(c_185,negated_conjecture,
( ~ about_event(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ bearer(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace)
| ~ about_event(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ bearer(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie) ),
inference(resolve,[status(thm)],[c_152,c_154]) ).
cnf(c_220,negated_conjecture,
( ~ about_event(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ bearer(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace)
| ~ about_event(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) ),
inference(resolve,[status(thm)],[c_167,c_185]) ).
cnf(c_221,negated_conjecture,
( ~ about_event(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ bearer(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace)
| ~ about_event(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1)) ),
inference(resolve,[status(thm)],[c_168,c_220]) ).
cnf(c_222,negated_conjecture,
( ~ about_event(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ bearer(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace)
| ~ about_event(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) ),
inference(resolve,[status(thm)],[c_169,c_221]) ).
cnf(c_223,negated_conjecture,
( ~ about_event(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ about_event(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) ),
inference(resolve,[status(thm)],[c_170,c_222]) ).
cnf(c_224,negated_conjecture,
( ~ about_event(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ about_event(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) ),
inference(resolve,[status(thm)],[c_171,c_223]) ).
cnf(c_186,negated_conjecture,
( ~ about_event(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ about_event(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) ),
inference(resolve,[status(thm)],[c_172,c_224]) ).
cnf(c_191,plain,
( about_event(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ part_of(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),sK1(f1,marketplace,philharmonie,distrib,concert_ds,e1))
| ~ cnt(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B) ),
inference(resolve,[status(thm)],[c_156,c_152]) ).
cnf(c_192,plain,
( about_event(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ cnt(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B) ),
inference(resolve,[status(thm)],[c_172,c_191]) ).
cnf(c_194,plain,
( about_event(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1)
| ~ cnt(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B) ),
inference(resolve,[status(thm)],[c_169,c_165]) ).
cnf(c_213,plain,
about_event(sK0(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),
inference(resolve,[status(thm)],[c_192,c_171]) ).
cnf(c_217,negated_conjecture,
~ about_event(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1),
inference(resolve,[status(thm)],[c_213,c_186]) ).
cnf(c_218,negated_conjecture,
~ cnt(sK2(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B),
inference(resolve,[status(thm)],[c_217,c_194]) ).
cnf(c_219,plain,
$false,
inference(resolve,[status(thm)],[c_218,c_168]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT113+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n026.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 00:17:11 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 3807527 was started by sandbox on n026,
% 0.08/0.36 % Sat Sep 26 00:17:11 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.37
% 0.08/0.37 % From the command line: assign(max_seconds, 300).
% 0.08/0.39
% 0.08/0.39 % SZS status Theorem for theBenchmark
% 0.08/0.39
% 0.08/0.39 % Proof 1 at 0.01 (+ 0.00) seconds.
% 0.08/0.39 % Length of proof is 100.
% 0.08/0.39 % Level of proof is 15.
% 0.08/0.39 % Maximum clause weight is 45.000.
% 0.08/0.39 % Given clauses 23.
% 0.08/0.39
% 0.08/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------