%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:48:29 PM UTC 2026
% Result : Theorem 1.21s 1.67s
% Output : CNFRefutation 1.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 11
% Syntax : Number of formulae : 44 ( 15 unt; 0 def)
% Number of atoms : 311 ( 0 equ)
% Maximal formula atoms : 72 ( 7 avg)
% Number of connectives : 494 ( 227 ~; 216 |; 48 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 7 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 : 140 ( 6 sgn 39 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(conjecture,conjecture,
? [X10,X11,X12] :
( founds_rem(e1,X10,f1)
& power(X11)
& bearer(X11,philharmonie)
& cnt(X11,decl(distrib),concert_ds)
& part_of(X11,X10)
& about_event(X11,e1)
& subjection(X12)
& bearer(X12,marketplace)
& cnt(X12,decl(distrib),concert_ds)
& part_of(X12,X10)
& about_event(X12,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture) ).
fof(ax_B2,axiom,
! [X11,X4,X5,X7,X6,X15] :
( ( power(X11)
& cnt(X11,decl(X4),X5)
& part_of(X11,X7)
& founds_rem(X6,X7,X15) )
=> about_event(X11,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_B2) ).
fof(ax_B3,axiom,
! [X12,X4,X5,X7,X6,X15] :
( ( subjection(X12)
& cnt(X12,decl(X4),X5)
& part_of(X12,X7)
& founds_rem(X6,X7,X15) )
=> about_event(X12,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_B3) ).
fof(ax_proh_relator_remedy,axiom,
! [X1,X2,X3,X4,X5,X6] :
( ( proh(X1)
& has_rem(X1)
& aee(X1,X2)
& aer(X1,X3)
& act(X1,X4)
& tgt(X1,X5)
& activates(X6,X1) )
=> ? [X10,X11,X12] :
( founds_rem(X6,X10,X1)
& power(X11)
& bearer(X11,X3)
& cnt(X11,decl(X4),X5)
& part_of(X11,X10)
& subjection(X12)
& bearer(X12,X2)
& cnt(X12,decl(X4),X5)
& part_of(X12,X10) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_proh_relator_remedy) ).
fof(rem_f1,axiom,
has_rem(f1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rem_f1) ).
fof(act_e1_f1,axiom,
activates(e1,f1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act_e1_f1) ).
fof(tgt_f1,axiom,
tgt(f1,concert_ds),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tgt_f1) ).
fof(act_f1,axiom,
act(f1,distrib),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act_f1) ).
fof(aee_f1,axiom,
aee(f1,marketplace),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aee_f1) ).
fof(proh_f1,axiom,
proh(f1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',proh_f1) ).
fof(aer_f1,axiom,
aer(f1,philharmonie),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aer_f1) ).
fof(c_0_11,negated_conjecture,
~ ? [X10,X11,X12] :
( founds_rem(e1,X10,f1)
& power(X11)
& bearer(X11,philharmonie)
& cnt(X11,decl(distrib),concert_ds)
& part_of(X11,X10)
& about_event(X11,e1)
& subjection(X12)
& bearer(X12,marketplace)
& cnt(X12,decl(distrib),concert_ds)
& part_of(X12,X10)
& about_event(X12,e1) ),
inference(assume_negation,[status(cth)],[conjecture]) ).
fof(c_0_12,negated_conjecture,
! [X113,X114,X115] :
( ~ founds_rem(e1,X113,f1)
| ~ power(X114)
| ~ bearer(X114,philharmonie)
| ~ cnt(X114,decl(distrib),concert_ds)
| ~ part_of(X114,X113)
| ~ about_event(X114,e1)
| ~ subjection(X115)
| ~ bearer(X115,marketplace)
| ~ cnt(X115,decl(distrib),concert_ds)
| ~ part_of(X115,X113)
| ~ about_event(X115,e1) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])]) ).
fof(c_0_13,plain,
! [X101,X102,X103,X104,X105,X106] :
( ~ power(X101)
| ~ cnt(X101,decl(X102),X103)
| ~ part_of(X101,X104)
| ~ founds_rem(X105,X104,X106)
| about_event(X101,X105) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_B2])]) ).
fof(c_0_14,plain,
! [X107,X108,X109,X110,X111,X112] :
( ~ subjection(X107)
| ~ cnt(X107,decl(X108),X109)
| ~ part_of(X107,X110)
| ~ founds_rem(X111,X110,X112)
| about_event(X107,X111) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_B3])]) ).
cnf(c_0_15,negated_conjecture,
( ~ founds_rem(e1,X1,f1)
| ~ power(X2)
| ~ bearer(X2,philharmonie)
| ~ cnt(X2,decl(distrib),concert_ds)
| ~ part_of(X2,X1)
| ~ about_event(X2,e1)
| ~ subjection(X3)
| ~ bearer(X3,marketplace)
| ~ cnt(X3,decl(distrib),concert_ds)
| ~ part_of(X3,X1)
| ~ about_event(X3,e1) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
cnf(c_0_16,plain,
( about_event(X1,X5)
| ~ power(X1)
| ~ cnt(X1,decl(X2),X3)
| ~ part_of(X1,X4)
| ~ founds_rem(X5,X4,X6) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_17,plain,
( about_event(X1,X5)
| ~ subjection(X1)
| ~ cnt(X1,decl(X2),X3)
| ~ part_of(X1,X4)
| ~ founds_rem(X5,X4,X6) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
fof(c_0_18,plain,
! [X75,X76,X77,X78,X79,X80] :
( ( founds_rem(X80,esk4_6(X75,X76,X77,X78,X79,X80),X75)
| ~ proh(X75)
| ~ has_rem(X75)
| ~ aee(X75,X76)
| ~ aer(X75,X77)
| ~ act(X75,X78)
| ~ tgt(X75,X79)
| ~ activates(X80,X75) )
& ( power(esk5_6(X75,X76,X77,X78,X79,X80))
| ~ proh(X75)
| ~ has_rem(X75)
| ~ aee(X75,X76)
| ~ aer(X75,X77)
| ~ act(X75,X78)
| ~ tgt(X75,X79)
| ~ activates(X80,X75) )
& ( bearer(esk5_6(X75,X76,X77,X78,X79,X80),X77)
| ~ proh(X75)
| ~ has_rem(X75)
| ~ aee(X75,X76)
| ~ aer(X75,X77)
| ~ act(X75,X78)
| ~ tgt(X75,X79)
| ~ activates(X80,X75) )
& ( cnt(esk5_6(X75,X76,X77,X78,X79,X80),decl(X78),X79)
| ~ proh(X75)
| ~ has_rem(X75)
| ~ aee(X75,X76)
| ~ aer(X75,X77)
| ~ act(X75,X78)
| ~ tgt(X75,X79)
| ~ activates(X80,X75) )
& ( part_of(esk5_6(X75,X76,X77,X78,X79,X80),esk4_6(X75,X76,X77,X78,X79,X80))
| ~ proh(X75)
| ~ has_rem(X75)
| ~ aee(X75,X76)
| ~ aer(X75,X77)
| ~ act(X75,X78)
| ~ tgt(X75,X79)
| ~ activates(X80,X75) )
& ( subjection(esk6_6(X75,X76,X77,X78,X79,X80))
| ~ proh(X75)
| ~ has_rem(X75)
| ~ aee(X75,X76)
| ~ aer(X75,X77)
| ~ act(X75,X78)
| ~ tgt(X75,X79)
| ~ activates(X80,X75) )
& ( bearer(esk6_6(X75,X76,X77,X78,X79,X80),X76)
| ~ proh(X75)
| ~ has_rem(X75)
| ~ aee(X75,X76)
| ~ aer(X75,X77)
| ~ act(X75,X78)
| ~ tgt(X75,X79)
| ~ activates(X80,X75) )
& ( cnt(esk6_6(X75,X76,X77,X78,X79,X80),decl(X78),X79)
| ~ proh(X75)
| ~ has_rem(X75)
| ~ aee(X75,X76)
| ~ aer(X75,X77)
| ~ act(X75,X78)
| ~ tgt(X75,X79)
| ~ activates(X80,X75) )
& ( part_of(esk6_6(X75,X76,X77,X78,X79,X80),esk4_6(X75,X76,X77,X78,X79,X80))
| ~ proh(X75)
| ~ has_rem(X75)
| ~ aee(X75,X76)
| ~ aer(X75,X77)
| ~ act(X75,X78)
| ~ tgt(X75,X79)
| ~ activates(X80,X75) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_proh_relator_remedy])])])]) ).
cnf(c_0_19,negated_conjecture,
( ~ subjection(X1)
| ~ power(X2)
| ~ founds_rem(e1,X3,f1)
| ~ part_of(X1,X3)
| ~ part_of(X2,X3)
| ~ cnt(X1,decl(distrib),concert_ds)
| ~ cnt(X2,decl(distrib),concert_ds)
| ~ bearer(X1,marketplace)
| ~ bearer(X2,philharmonie) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_15,c_0_16]),c_0_17]) ).
cnf(c_0_20,plain,
( cnt(esk6_6(X1,X2,X3,X4,X5,X6),decl(X4),X5)
| ~ proh(X1)
| ~ has_rem(X1)
| ~ aee(X1,X2)
| ~ aer(X1,X3)
| ~ act(X1,X4)
| ~ tgt(X1,X5)
| ~ activates(X6,X1) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_21,plain,
( subjection(esk6_6(X1,X2,X3,X4,X5,X6))
| ~ proh(X1)
| ~ has_rem(X1)
| ~ aee(X1,X2)
| ~ aer(X1,X3)
| ~ act(X1,X4)
| ~ tgt(X1,X5)
| ~ activates(X6,X1) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_22,negated_conjecture,
( ~ power(X1)
| ~ founds_rem(e1,X2,f1)
| ~ has_rem(X3)
| ~ part_of(esk6_6(X3,X4,X5,distrib,concert_ds,X6),X2)
| ~ part_of(X1,X2)
| ~ cnt(X1,decl(distrib),concert_ds)
| ~ bearer(esk6_6(X3,X4,X5,distrib,concert_ds,X6),marketplace)
| ~ bearer(X1,philharmonie)
| ~ activates(X6,X3)
| ~ tgt(X3,concert_ds)
| ~ act(X3,distrib)
| ~ aer(X3,X5)
| ~ aee(X3,X4)
| ~ proh(X3) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_19,c_0_20]),c_0_21]) ).
cnf(c_0_23,plain,
( bearer(esk6_6(X1,X2,X3,X4,X5,X6),X2)
| ~ proh(X1)
| ~ has_rem(X1)
| ~ aee(X1,X2)
| ~ aer(X1,X3)
| ~ act(X1,X4)
| ~ tgt(X1,X5)
| ~ activates(X6,X1) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_24,negated_conjecture,
( ~ power(X1)
| ~ founds_rem(e1,X2,f1)
| ~ has_rem(X3)
| ~ part_of(esk6_6(X3,marketplace,X4,distrib,concert_ds,X5),X2)
| ~ part_of(X1,X2)
| ~ cnt(X1,decl(distrib),concert_ds)
| ~ bearer(X1,philharmonie)
| ~ activates(X5,X3)
| ~ tgt(X3,concert_ds)
| ~ act(X3,distrib)
| ~ aer(X3,X4)
| ~ aee(X3,marketplace)
| ~ proh(X3) ),
inference(spm,[status(thm)],[c_0_22,c_0_23]) ).
cnf(c_0_25,plain,
( part_of(esk6_6(X1,X2,X3,X4,X5,X6),esk4_6(X1,X2,X3,X4,X5,X6))
| ~ proh(X1)
| ~ has_rem(X1)
| ~ aee(X1,X2)
| ~ aer(X1,X3)
| ~ act(X1,X4)
| ~ tgt(X1,X5)
| ~ activates(X6,X1) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_26,negated_conjecture,
( ~ power(X1)
| ~ founds_rem(e1,esk4_6(X2,marketplace,X3,distrib,concert_ds,X4),f1)
| ~ has_rem(X2)
| ~ part_of(X1,esk4_6(X2,marketplace,X3,distrib,concert_ds,X4))
| ~ cnt(X1,decl(distrib),concert_ds)
| ~ bearer(X1,philharmonie)
| ~ activates(X4,X2)
| ~ tgt(X2,concert_ds)
| ~ act(X2,distrib)
| ~ aer(X2,X3)
| ~ aee(X2,marketplace)
| ~ proh(X2) ),
inference(spm,[status(thm)],[c_0_24,c_0_25]) ).
cnf(c_0_27,plain,
( founds_rem(X1,esk4_6(X2,X3,X4,X5,X6,X1),X2)
| ~ proh(X2)
| ~ has_rem(X2)
| ~ aee(X2,X3)
| ~ aer(X2,X4)
| ~ act(X2,X5)
| ~ tgt(X2,X6)
| ~ activates(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_28,plain,
has_rem(f1),
inference(split_conjunct,[status(thm)],[rem_f1]) ).
cnf(c_0_29,plain,
activates(e1,f1),
inference(split_conjunct,[status(thm)],[act_e1_f1]) ).
cnf(c_0_30,plain,
tgt(f1,concert_ds),
inference(split_conjunct,[status(thm)],[tgt_f1]) ).
cnf(c_0_31,plain,
act(f1,distrib),
inference(split_conjunct,[status(thm)],[act_f1]) ).
cnf(c_0_32,plain,
aee(f1,marketplace),
inference(split_conjunct,[status(thm)],[aee_f1]) ).
cnf(c_0_33,plain,
proh(f1),
inference(split_conjunct,[status(thm)],[proh_f1]) ).
cnf(c_0_34,negated_conjecture,
( ~ power(X1)
| ~ part_of(X1,esk4_6(f1,marketplace,X2,distrib,concert_ds,e1))
| ~ cnt(X1,decl(distrib),concert_ds)
| ~ bearer(X1,philharmonie)
| ~ aer(f1,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26,c_0_27]),c_0_28]),c_0_29]),c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
cnf(c_0_35,plain,
( part_of(esk5_6(X1,X2,X3,X4,X5,X6),esk4_6(X1,X2,X3,X4,X5,X6))
| ~ proh(X1)
| ~ has_rem(X1)
| ~ aee(X1,X2)
| ~ aer(X1,X3)
| ~ act(X1,X4)
| ~ tgt(X1,X5)
| ~ activates(X6,X1) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_36,negated_conjecture,
( ~ power(esk5_6(f1,marketplace,X1,distrib,concert_ds,e1))
| ~ cnt(esk5_6(f1,marketplace,X1,distrib,concert_ds,e1),decl(distrib),concert_ds)
| ~ bearer(esk5_6(f1,marketplace,X1,distrib,concert_ds,e1),philharmonie)
| ~ aer(f1,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34,c_0_35]),c_0_28]),c_0_29]),c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
cnf(c_0_37,plain,
( cnt(esk5_6(X1,X2,X3,X4,X5,X6),decl(X4),X5)
| ~ proh(X1)
| ~ has_rem(X1)
| ~ aee(X1,X2)
| ~ aer(X1,X3)
| ~ act(X1,X4)
| ~ tgt(X1,X5)
| ~ activates(X6,X1) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_38,negated_conjecture,
( ~ power(esk5_6(f1,marketplace,X1,distrib,concert_ds,e1))
| ~ bearer(esk5_6(f1,marketplace,X1,distrib,concert_ds,e1),philharmonie)
| ~ aer(f1,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_37]),c_0_28]),c_0_29]),c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
cnf(c_0_39,plain,
( power(esk5_6(X1,X2,X3,X4,X5,X6))
| ~ proh(X1)
| ~ has_rem(X1)
| ~ aee(X1,X2)
| ~ aer(X1,X3)
| ~ act(X1,X4)
| ~ tgt(X1,X5)
| ~ activates(X6,X1) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_40,negated_conjecture,
( ~ bearer(esk5_6(f1,marketplace,X1,distrib,concert_ds,e1),philharmonie)
| ~ aer(f1,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38,c_0_39]),c_0_28]),c_0_29]),c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
cnf(c_0_41,plain,
( bearer(esk5_6(X1,X2,X3,X4,X5,X6),X3)
| ~ proh(X1)
| ~ has_rem(X1)
| ~ aee(X1,X2)
| ~ aer(X1,X3)
| ~ act(X1,X4)
| ~ tgt(X1,X5)
| ~ activates(X6,X1) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_42,plain,
aer(f1,philharmonie),
inference(split_conjunct,[status(thm)],[aer_f1]) ).
cnf(c_0_43,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_41]),c_0_42]),c_0_28]),c_0_29]),c_0_30]),c_0_31]),c_0_32]),c_0_33])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.09 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.10/0.28 % Computer : n026.cluster.edu
% 0.10/0.28 % Model : x86_64 x86_64
% 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.28 % Memory : 8042.1875MB
% 0.10/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.28 % CPULimit : 300
% 0.10/0.28 % WCLimit : 300
% 0.10/0.28 % DateTime : Mon May 4 23:35:08 EDT 2026
% 0.10/0.28 % CPUTime :
% 0.10/0.29 % start to proof: theBenchmark
% 1.21/1.66 % Version : CSE_E---1.7
% 1.21/1.67 % Problem : theBenchmark.p
% 1.21/1.67 % SZS status Theorem for theBenchmark.p
% 1.21/1.67 % SZS output start CNFRefutation
% See solution above
% 1.21/1.67 % Total time : 1.366s
%------------------------------------------------------------------------------