%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n007.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:03:08 AM UTC 2026
% Result : Theorem 6.37s 2.91s
% Output : CNFRefutation 6.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 11
% Syntax : Number of formulae : 65 ( 24 unt; 0 typ; 0 def)
% Number of atoms : 388 ( 0 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 637 ( 314 ~; 290 |; 30 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 29 ( 28 usr; 1 prp; 0-5 aty)
% Number of functors : 21 ( 21 usr; 7 con; 0-6 aty)
% Number of variables : 177 ( 171 !; 6 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ triggers > norm_state_change > founds_rem > founds > does > cnt > tgt > rem_act > part_of > competent_for > bearer > aer > aee > activates > act > about_event > target > subjection > rule > right > proh > power > inst_event > has_rem > event > duty > agent > action > #nlpp > rfr > decl > philharmonie > marketplace > f1 > e1 > duty_rem > distrib > concert_ds > #skF_11 > #skF_2 > #skF_1 > #skF_8 > #skF_12 > #skF_10 > #skF_7 > #skF_3 > #skF_5 > #skF_6 > #skF_9 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(aee,type,
aee: ( $i * $i ) > $o ).
tff(has_rem,type,
has_rem: $i > $o ).
tff(power,type,
power: $i > $o ).
tff(e1,type,
e1: $i ).
tff(rem_act,type,
rem_act: ( $i * $i ) > $o ).
tff('#skF_11',type,
'#skF_11': ( $i * $i ) > $i ).
tff(rfr,type,
rfr: $i > $i ).
tff(norm_state_change,type,
norm_state_change: ( $i * $i * $i * $i ) > $o ).
tff(bearer,type,
bearer: ( $i * $i ) > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(proh,type,
proh: $i > $o ).
tff(duty_rem,type,
duty_rem: $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(subjection,type,
subjection: $i > $o ).
tff(rule,type,
rule: $i > $o ).
tff(concert_ds,type,
concert_ds: $i ).
tff(aer,type,
aer: ( $i * $i ) > $o ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(competent_for,type,
competent_for: ( $i * $i ) > $o ).
tff('#skF_12',type,
'#skF_12': ( $i * $i * $i * $i ) > $i ).
tff(part_of,type,
part_of: ( $i * $i ) > $o ).
tff(inst_event,type,
inst_event: $i > $o ).
tff(cnt,type,
cnt: ( $i * $i * $i ) > $o ).
tff(about_event,type,
about_event: ( $i * $i ) > $o ).
tff(founds,type,
founds: ( $i * $i * $i ) > $o ).
tff('#skF_10',type,
'#skF_10': ( $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i * $i * $i ) > $i ).
tff(f1,type,
f1: $i ).
tff(founds_rem,type,
founds_rem: ( $i * $i * $i ) > $o ).
tff(philharmonie,type,
philharmonie: $i ).
tff(agent,type,
agent: $i > $o ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(event,type,
event: $i > $o ).
tff('#skF_5',type,
'#skF_5': ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(does,type,
does: ( $i * $i * $i ) > $o ).
tff(marketplace,type,
marketplace: $i ).
tff(target,type,
target: $i > $o ).
tff(activates,type,
activates: ( $i * $i ) > $o ).
tff(triggers,type,
triggers: ( $i * $i * $i * $i * $i ) > $o ).
tff(tgt,type,
tgt: ( $i * $i ) > $o ).
tff(decl,type,
decl: $i > $i ).
tff(right,type,
right: $i > $o ).
tff(distrib,type,
distrib: $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(act,type,
act: ( $i * $i ) > $o ).
tff('#skF_9',type,
'#skF_9': ( $i * $i ) > $i ).
tff(action,type,
action: $i > $o ).
tff('#skF_4',type,
'#skF_4': ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(duty,type,
duty: $i > $o ).
tff(f_167,axiom,
proh(f1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',proh_f1) ).
tff(f_168,axiom,
has_rem(f1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rem_f1) ).
tff(f_169,axiom,
aee(f1,marketplace),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aee_f1) ).
tff(f_170,axiom,
aer(f1,philharmonie),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aer_f1) ).
tff(f_171,axiom,
act(f1,distrib),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act_f1) ).
tff(f_172,axiom,
tgt(f1,concert_ds),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tgt_f1) ).
tff(f_173,axiom,
activates(e1,f1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act_e1_f1) ).
tff(f_95,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) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_proh_relator_remedy) ).
tff(f_197,negated_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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture) ).
tff(f_149,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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_B2) ).
tff(f_159,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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_B3) ).
tff(c_76,plain,
proh(f1),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_78,plain,
has_rem(f1),
inference(cnfTransformation,[status(thm)],[f_168]) ).
tff(c_80,plain,
aee(f1,marketplace),
inference(cnfTransformation,[status(thm)],[f_169]) ).
tff(c_82,plain,
aer(f1,philharmonie),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_84,plain,
act(f1,distrib),
inference(cnfTransformation,[status(thm)],[f_171]) ).
tff(c_86,plain,
tgt(f1,concert_ds),
inference(cnfTransformation,[status(thm)],[f_172]) ).
tff(c_88,plain,
activates(e1,f1),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_26,plain,
! [X_11,Y_12,T_14,A_13,E_15,F_10] :
( subjection('#skF_6'(F_10,T_14,Y_12,A_13,E_15,X_11))
| ~ activates(E_15,F_10)
| ~ tgt(F_10,T_14)
| ~ act(F_10,A_13)
| ~ aer(F_10,Y_12)
| ~ aee(F_10,X_11)
| ~ has_rem(F_10)
| ~ proh(F_10) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_34,plain,
! [X_11,Y_12,T_14,A_13,E_15,F_10] :
( power('#skF_5'(F_10,T_14,Y_12,A_13,E_15,X_11))
| ~ activates(E_15,F_10)
| ~ tgt(F_10,T_14)
| ~ act(F_10,A_13)
| ~ aer(F_10,Y_12)
| ~ aee(F_10,X_11)
| ~ has_rem(F_10)
| ~ proh(F_10) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_24,plain,
! [X_11,Y_12,T_14,A_13,E_15,F_10] :
( bearer('#skF_6'(F_10,T_14,Y_12,A_13,E_15,X_11),X_11)
| ~ activates(E_15,F_10)
| ~ tgt(F_10,T_14)
| ~ act(F_10,A_13)
| ~ aer(F_10,Y_12)
| ~ aee(F_10,X_11)
| ~ has_rem(F_10)
| ~ proh(F_10) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_32,plain,
! [X_11,Y_12,T_14,A_13,E_15,F_10] :
( bearer('#skF_5'(F_10,T_14,Y_12,A_13,E_15,X_11),Y_12)
| ~ activates(E_15,F_10)
| ~ tgt(F_10,T_14)
| ~ act(F_10,A_13)
| ~ aer(F_10,Y_12)
| ~ aee(F_10,X_11)
| ~ has_rem(F_10)
| ~ proh(F_10) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_36,plain,
! [X_11,Y_12,T_14,A_13,E_15,F_10] :
( founds_rem(E_15,'#skF_4'(F_10,T_14,Y_12,A_13,E_15,X_11),F_10)
| ~ activates(E_15,F_10)
| ~ tgt(F_10,T_14)
| ~ act(F_10,A_13)
| ~ aer(F_10,Y_12)
| ~ aee(F_10,X_11)
| ~ has_rem(F_10)
| ~ proh(F_10) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_30,plain,
! [X_11,Y_12,T_14,A_13,E_15,F_10] :
( cnt('#skF_5'(F_10,T_14,Y_12,A_13,E_15,X_11),decl(A_13),T_14)
| ~ activates(E_15,F_10)
| ~ tgt(F_10,T_14)
| ~ act(F_10,A_13)
| ~ aer(F_10,Y_12)
| ~ aee(F_10,X_11)
| ~ has_rem(F_10)
| ~ proh(F_10) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_28,plain,
! [X_11,Y_12,T_14,A_13,E_15,F_10] :
( part_of('#skF_5'(F_10,T_14,Y_12,A_13,E_15,X_11),'#skF_4'(F_10,T_14,Y_12,A_13,E_15,X_11))
| ~ activates(E_15,F_10)
| ~ tgt(F_10,T_14)
| ~ act(F_10,A_13)
| ~ aer(F_10,Y_12)
| ~ aee(F_10,X_11)
| ~ has_rem(F_10)
| ~ proh(F_10) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_22,plain,
! [X_11,Y_12,T_14,A_13,E_15,F_10] :
( cnt('#skF_6'(F_10,T_14,Y_12,A_13,E_15,X_11),decl(A_13),T_14)
| ~ activates(E_15,F_10)
| ~ tgt(F_10,T_14)
| ~ act(F_10,A_13)
| ~ aer(F_10,Y_12)
| ~ aee(F_10,X_11)
| ~ has_rem(F_10)
| ~ proh(F_10) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_135,plain,
! [Y_193,A_194,T_192,X_196,E_195,F_191] :
( part_of('#skF_6'(F_191,T_192,Y_193,A_194,E_195,X_196),'#skF_4'(F_191,T_192,Y_193,A_194,E_195,X_196))
| ~ activates(E_195,F_191)
| ~ tgt(F_191,T_192)
| ~ act(F_191,A_194)
| ~ aer(F_191,Y_193)
| ~ aee(F_191,X_196)
| ~ has_rem(F_191)
| ~ proh(F_191) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_92,plain,
! [S_50,RhoR_48,Pw_49] :
( ~ about_event(S_50,e1)
| ~ part_of(S_50,RhoR_48)
| ~ cnt(S_50,decl(distrib),concert_ds)
| ~ bearer(S_50,marketplace)
| ~ subjection(S_50)
| ~ about_event(Pw_49,e1)
| ~ part_of(Pw_49,RhoR_48)
| ~ cnt(Pw_49,decl(distrib),concert_ds)
| ~ bearer(Pw_49,philharmonie)
| ~ power(Pw_49)
| ~ founds_rem(e1,RhoR_48,f1) ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_184,plain,
! [E_301,T_304,Pw_300,X_299,Y_303,F_302,A_298] :
( ~ about_event('#skF_6'(F_302,T_304,Y_303,A_298,E_301,X_299),e1)
| ~ cnt('#skF_6'(F_302,T_304,Y_303,A_298,E_301,X_299),decl(distrib),concert_ds)
| ~ bearer('#skF_6'(F_302,T_304,Y_303,A_298,E_301,X_299),marketplace)
| ~ subjection('#skF_6'(F_302,T_304,Y_303,A_298,E_301,X_299))
| ~ about_event(Pw_300,e1)
| ~ part_of(Pw_300,'#skF_4'(F_302,T_304,Y_303,A_298,E_301,X_299))
| ~ cnt(Pw_300,decl(distrib),concert_ds)
| ~ bearer(Pw_300,philharmonie)
| ~ power(Pw_300)
| ~ founds_rem(e1,'#skF_4'(F_302,T_304,Y_303,A_298,E_301,X_299),f1)
| ~ activates(E_301,F_302)
| ~ tgt(F_302,T_304)
| ~ act(F_302,A_298)
| ~ aer(F_302,Y_303)
| ~ aee(F_302,X_299)
| ~ has_rem(F_302)
| ~ proh(F_302) ),
inference(resolution,[status(thm)],[c_135,c_92]) ).
tff(c_198,plain,
! [F_311,E_313,X_314,Pw_310,Y_312] :
( ~ about_event('#skF_6'(F_311,concert_ds,Y_312,distrib,E_313,X_314),e1)
| ~ bearer('#skF_6'(F_311,concert_ds,Y_312,distrib,E_313,X_314),marketplace)
| ~ subjection('#skF_6'(F_311,concert_ds,Y_312,distrib,E_313,X_314))
| ~ about_event(Pw_310,e1)
| ~ part_of(Pw_310,'#skF_4'(F_311,concert_ds,Y_312,distrib,E_313,X_314))
| ~ cnt(Pw_310,decl(distrib),concert_ds)
| ~ bearer(Pw_310,philharmonie)
| ~ power(Pw_310)
| ~ founds_rem(e1,'#skF_4'(F_311,concert_ds,Y_312,distrib,E_313,X_314),f1)
| ~ activates(E_313,F_311)
| ~ tgt(F_311,concert_ds)
| ~ act(F_311,distrib)
| ~ aer(F_311,Y_312)
| ~ aee(F_311,X_314)
| ~ has_rem(F_311)
| ~ proh(F_311) ),
inference(resolution,[status(thm)],[c_22,c_184]) ).
tff(c_276,plain,
! [F_346,Y_347,E_348,X_349] :
( ~ about_event('#skF_6'(F_346,concert_ds,Y_347,distrib,E_348,X_349),e1)
| ~ bearer('#skF_6'(F_346,concert_ds,Y_347,distrib,E_348,X_349),marketplace)
| ~ subjection('#skF_6'(F_346,concert_ds,Y_347,distrib,E_348,X_349))
| ~ about_event('#skF_5'(F_346,concert_ds,Y_347,distrib,E_348,X_349),e1)
| ~ cnt('#skF_5'(F_346,concert_ds,Y_347,distrib,E_348,X_349),decl(distrib),concert_ds)
| ~ bearer('#skF_5'(F_346,concert_ds,Y_347,distrib,E_348,X_349),philharmonie)
| ~ power('#skF_5'(F_346,concert_ds,Y_347,distrib,E_348,X_349))
| ~ founds_rem(e1,'#skF_4'(F_346,concert_ds,Y_347,distrib,E_348,X_349),f1)
| ~ activates(E_348,F_346)
| ~ tgt(F_346,concert_ds)
| ~ act(F_346,distrib)
| ~ aer(F_346,Y_347)
| ~ aee(F_346,X_349)
| ~ has_rem(F_346)
| ~ proh(F_346) ),
inference(resolution,[status(thm)],[c_28,c_198]) ).
tff(c_282,plain,
! [F_350,Y_351,E_352,X_353] :
( ~ about_event('#skF_6'(F_350,concert_ds,Y_351,distrib,E_352,X_353),e1)
| ~ bearer('#skF_6'(F_350,concert_ds,Y_351,distrib,E_352,X_353),marketplace)
| ~ subjection('#skF_6'(F_350,concert_ds,Y_351,distrib,E_352,X_353))
| ~ about_event('#skF_5'(F_350,concert_ds,Y_351,distrib,E_352,X_353),e1)
| ~ bearer('#skF_5'(F_350,concert_ds,Y_351,distrib,E_352,X_353),philharmonie)
| ~ power('#skF_5'(F_350,concert_ds,Y_351,distrib,E_352,X_353))
| ~ founds_rem(e1,'#skF_4'(F_350,concert_ds,Y_351,distrib,E_352,X_353),f1)
| ~ activates(E_352,F_350)
| ~ tgt(F_350,concert_ds)
| ~ act(F_350,distrib)
| ~ aer(F_350,Y_351)
| ~ aee(F_350,X_353)
| ~ has_rem(F_350)
| ~ proh(F_350) ),
inference(resolution,[status(thm)],[c_30,c_276]) ).
tff(c_286,plain,
! [Y_12,X_11] :
( ~ about_event('#skF_6'(f1,concert_ds,Y_12,distrib,e1,X_11),e1)
| ~ bearer('#skF_6'(f1,concert_ds,Y_12,distrib,e1,X_11),marketplace)
| ~ subjection('#skF_6'(f1,concert_ds,Y_12,distrib,e1,X_11))
| ~ about_event('#skF_5'(f1,concert_ds,Y_12,distrib,e1,X_11),e1)
| ~ bearer('#skF_5'(f1,concert_ds,Y_12,distrib,e1,X_11),philharmonie)
| ~ power('#skF_5'(f1,concert_ds,Y_12,distrib,e1,X_11))
| ~ activates(e1,f1)
| ~ tgt(f1,concert_ds)
| ~ act(f1,distrib)
| ~ aer(f1,Y_12)
| ~ aee(f1,X_11)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[c_36,c_282]) ).
tff(c_290,plain,
! [Y_354,X_355] :
( ~ about_event('#skF_6'(f1,concert_ds,Y_354,distrib,e1,X_355),e1)
| ~ bearer('#skF_6'(f1,concert_ds,Y_354,distrib,e1,X_355),marketplace)
| ~ subjection('#skF_6'(f1,concert_ds,Y_354,distrib,e1,X_355))
| ~ about_event('#skF_5'(f1,concert_ds,Y_354,distrib,e1,X_355),e1)
| ~ bearer('#skF_5'(f1,concert_ds,Y_354,distrib,e1,X_355),philharmonie)
| ~ power('#skF_5'(f1,concert_ds,Y_354,distrib,e1,X_355))
| ~ aer(f1,Y_354)
| ~ aee(f1,X_355) ),
inference(demodulation,[status(thm),theory(equality)],[c_76,c_78,c_84,c_86,c_88,c_286]) ).
tff(c_294,plain,
! [X_11] :
( ~ about_event('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,X_11),e1)
| ~ bearer('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,X_11),marketplace)
| ~ subjection('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,X_11))
| ~ about_event('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,X_11),e1)
| ~ power('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,X_11))
| ~ activates(e1,f1)
| ~ tgt(f1,concert_ds)
| ~ act(f1,distrib)
| ~ aer(f1,philharmonie)
| ~ aee(f1,X_11)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[c_32,c_290]) ).
tff(c_298,plain,
! [X_356] :
( ~ about_event('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,X_356),e1)
| ~ bearer('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,X_356),marketplace)
| ~ subjection('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,X_356))
| ~ about_event('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,X_356),e1)
| ~ power('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,X_356))
| ~ aee(f1,X_356) ),
inference(demodulation,[status(thm),theory(equality)],[c_76,c_78,c_82,c_84,c_86,c_88,c_294]) ).
tff(c_302,plain,
( ~ about_event('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,marketplace),e1)
| ~ subjection('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,marketplace))
| ~ about_event('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,marketplace),e1)
| ~ power('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,marketplace))
| ~ activates(e1,f1)
| ~ tgt(f1,concert_ds)
| ~ act(f1,distrib)
| ~ aer(f1,philharmonie)
| ~ aee(f1,marketplace)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[c_24,c_298]) ).
tff(c_305,plain,
( ~ about_event('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,marketplace),e1)
| ~ subjection('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,marketplace))
| ~ about_event('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,marketplace),e1)
| ~ power('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,marketplace)) ),
inference(demodulation,[status(thm),theory(equality)],[c_76,c_78,c_80,c_82,c_84,c_86,c_88,c_302]) ).
tff(c_306,plain,
~ power('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,marketplace)),
inference(splitLeft,[status(thm)],[c_305]) ).
tff(c_309,plain,
( ~ activates(e1,f1)
| ~ tgt(f1,concert_ds)
| ~ act(f1,distrib)
| ~ aer(f1,philharmonie)
| ~ aee(f1,marketplace)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[c_34,c_306]) ).
tff(c_313,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_76,c_78,c_80,c_82,c_84,c_86,c_88,c_309]) ).
tff(c_315,plain,
power('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,marketplace)),
inference(splitRight,[status(thm)],[c_305]) ).
tff(c_118,plain,
! [Y_163,T_162,E_165,X_166,A_164,F_161] :
( founds_rem(E_165,'#skF_4'(F_161,T_162,Y_163,A_164,E_165,X_166),F_161)
| ~ activates(E_165,F_161)
| ~ tgt(F_161,T_162)
| ~ act(F_161,A_164)
| ~ aer(F_161,Y_163)
| ~ aee(F_161,X_166)
| ~ has_rem(F_161)
| ~ proh(F_161) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_60,plain,
! [E_40,A_37,Pw_36,T_38,R_41,Rho_39] :
( about_event(Pw_36,E_40)
| ~ founds_rem(E_40,Rho_39,R_41)
| ~ part_of(Pw_36,Rho_39)
| ~ cnt(Pw_36,decl(A_37),T_38)
| ~ power(Pw_36) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_150,plain,
! [A_213,E_218,A_215,F_216,X_214,Pw_212,Y_217,T_219,T_220] :
( about_event(Pw_212,E_218)
| ~ part_of(Pw_212,'#skF_4'(F_216,T_220,Y_217,A_215,E_218,X_214))
| ~ cnt(Pw_212,decl(A_213),T_219)
| ~ power(Pw_212)
| ~ activates(E_218,F_216)
| ~ tgt(F_216,T_220)
| ~ act(F_216,A_215)
| ~ aer(F_216,Y_217)
| ~ aee(F_216,X_214)
| ~ has_rem(F_216)
| ~ proh(F_216) ),
inference(resolution,[status(thm)],[c_118,c_60]) ).
tff(c_168,plain,
! [X_263,E_262,Y_259,F_257,A_261,A_256,T_258,T_260] :
( about_event('#skF_5'(F_257,T_258,Y_259,A_261,E_262,X_263),E_262)
| ~ cnt('#skF_5'(F_257,T_258,Y_259,A_261,E_262,X_263),decl(A_256),T_260)
| ~ power('#skF_5'(F_257,T_258,Y_259,A_261,E_262,X_263))
| ~ activates(E_262,F_257)
| ~ tgt(F_257,T_258)
| ~ act(F_257,A_261)
| ~ aer(F_257,Y_259)
| ~ aee(F_257,X_263)
| ~ has_rem(F_257)
| ~ proh(F_257) ),
inference(resolution,[status(thm)],[c_28,c_150]) ).
tff(c_171,plain,
! [X_11,Y_12,T_14,A_13,E_15,F_10] :
( about_event('#skF_5'(F_10,T_14,Y_12,A_13,E_15,X_11),E_15)
| ~ power('#skF_5'(F_10,T_14,Y_12,A_13,E_15,X_11))
| ~ activates(E_15,F_10)
| ~ tgt(F_10,T_14)
| ~ act(F_10,A_13)
| ~ aer(F_10,Y_12)
| ~ aee(F_10,X_11)
| ~ has_rem(F_10)
| ~ proh(F_10) ),
inference(resolution,[status(thm)],[c_30,c_168]) ).
tff(c_20,plain,
! [X_11,Y_12,T_14,A_13,E_15,F_10] :
( part_of('#skF_6'(F_10,T_14,Y_12,A_13,E_15,X_11),'#skF_4'(F_10,T_14,Y_12,A_13,E_15,X_11))
| ~ activates(E_15,F_10)
| ~ tgt(F_10,T_14)
| ~ act(F_10,A_13)
| ~ aer(F_10,Y_12)
| ~ aee(F_10,X_11)
| ~ has_rem(F_10)
| ~ proh(F_10) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_62,plain,
! [T_44,Rho_45,R_47,E_46,A_43,S_42] :
( about_event(S_42,E_46)
| ~ founds_rem(E_46,Rho_45,R_47)
| ~ part_of(S_42,Rho_45)
| ~ cnt(S_42,decl(A_43),T_44)
| ~ subjection(S_42) ),
inference(cnfTransformation,[status(thm)],[f_159]) ).
tff(c_143,plain,
! [A_207,S_210,T_211,E_209,F_205,A_204,T_208,X_203,Y_206] :
( about_event(S_210,E_209)
| ~ part_of(S_210,'#skF_4'(F_205,T_211,Y_206,A_204,E_209,X_203))
| ~ cnt(S_210,decl(A_207),T_208)
| ~ subjection(S_210)
| ~ activates(E_209,F_205)
| ~ tgt(F_205,T_211)
| ~ act(F_205,A_204)
| ~ aer(F_205,Y_206)
| ~ aee(F_205,X_203)
| ~ has_rem(F_205)
| ~ proh(F_205) ),
inference(resolution,[status(thm)],[c_118,c_62]) ).
tff(c_157,plain,
! [E_227,A_225,X_228,T_222,F_221,Y_224,T_223,A_226] :
( about_event('#skF_6'(F_221,T_223,Y_224,A_225,E_227,X_228),E_227)
| ~ cnt('#skF_6'(F_221,T_223,Y_224,A_225,E_227,X_228),decl(A_226),T_222)
| ~ subjection('#skF_6'(F_221,T_223,Y_224,A_225,E_227,X_228))
| ~ activates(E_227,F_221)
| ~ tgt(F_221,T_223)
| ~ act(F_221,A_225)
| ~ aer(F_221,Y_224)
| ~ aee(F_221,X_228)
| ~ has_rem(F_221)
| ~ proh(F_221) ),
inference(resolution,[status(thm)],[c_20,c_143]) ).
tff(c_160,plain,
! [X_11,Y_12,T_14,A_13,E_15,F_10] :
( about_event('#skF_6'(F_10,T_14,Y_12,A_13,E_15,X_11),E_15)
| ~ subjection('#skF_6'(F_10,T_14,Y_12,A_13,E_15,X_11))
| ~ activates(E_15,F_10)
| ~ tgt(F_10,T_14)
| ~ act(F_10,A_13)
| ~ aer(F_10,Y_12)
| ~ aee(F_10,X_11)
| ~ has_rem(F_10)
| ~ proh(F_10) ),
inference(resolution,[status(thm)],[c_22,c_157]) ).
tff(c_314,plain,
( ~ about_event('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,marketplace),e1)
| ~ subjection('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,marketplace))
| ~ about_event('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,marketplace),e1) ),
inference(splitRight,[status(thm)],[c_305]) ).
tff(c_316,plain,
~ about_event('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,marketplace),e1),
inference(splitLeft,[status(thm)],[c_314]) ).
tff(c_322,plain,
( ~ subjection('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,marketplace))
| ~ activates(e1,f1)
| ~ tgt(f1,concert_ds)
| ~ act(f1,distrib)
| ~ aer(f1,philharmonie)
| ~ aee(f1,marketplace)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[c_160,c_316]) ).
tff(c_328,plain,
~ subjection('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,marketplace)),
inference(demodulation,[status(thm),theory(equality)],[c_76,c_78,c_80,c_82,c_84,c_86,c_88,c_322]) ).
tff(c_331,plain,
( ~ activates(e1,f1)
| ~ tgt(f1,concert_ds)
| ~ act(f1,distrib)
| ~ aer(f1,philharmonie)
| ~ aee(f1,marketplace)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[c_26,c_328]) ).
tff(c_335,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_76,c_78,c_80,c_82,c_84,c_86,c_88,c_331]) ).
tff(c_336,plain,
( ~ subjection('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,marketplace))
| ~ about_event('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,marketplace),e1) ),
inference(splitRight,[status(thm)],[c_314]) ).
tff(c_338,plain,
~ about_event('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,marketplace),e1),
inference(splitLeft,[status(thm)],[c_336]) ).
tff(c_344,plain,
( ~ power('#skF_5'(f1,concert_ds,philharmonie,distrib,e1,marketplace))
| ~ activates(e1,f1)
| ~ tgt(f1,concert_ds)
| ~ act(f1,distrib)
| ~ aer(f1,philharmonie)
| ~ aee(f1,marketplace)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[c_171,c_338]) ).
tff(c_351,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_76,c_78,c_80,c_82,c_84,c_86,c_88,c_315,c_344]) ).
tff(c_352,plain,
~ subjection('#skF_6'(f1,concert_ds,philharmonie,distrib,e1,marketplace)),
inference(splitRight,[status(thm)],[c_336]) ).
tff(c_356,plain,
( ~ activates(e1,f1)
| ~ tgt(f1,concert_ds)
| ~ act(f1,distrib)
| ~ aer(f1,philharmonie)
| ~ aee(f1,marketplace)
| ~ has_rem(f1)
| ~ proh(f1) ),
inference(resolution,[status(thm)],[c_26,c_352]) ).
tff(c_360,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_76,c_78,c_80,c_82,c_84,c_86,c_88,c_356]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.09/0.35 % Computer : n007.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 14:05:26 UTC 2026
% 0.09/0.36 % CPUTime :
% 6.37/2.91 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.37/2.91
% 6.37/2.91 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------