%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT113+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:01:31 AM UTC 2026
% Result : Theorem 21.17s 13.19s
% Output : CNFRefutation 21.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT113+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/10.40 % Computer : n013.cluster.edu
% 0.10/10.40 % Model : x86_64 x86_64
% 0.10/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.40 % Memory : 8046.5625MB
% 0.10/10.40 % OS : Linux 6.8.0-71-generic
% 0.10/10.40 % CPULimit : 300
% 0.10/10.40 % WCLimit : 300
% 0.10/10.40 % DateTime : Sat Sep 26 00:14:08 UTC 2026
% 0.10/10.40 % CPUTime :
% 0.10/10.40 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.17/13.19 % SZS status Theorem for theBenchmark.p
% 21.17/13.19 % SZS output start CNFRefutation for theBenchmark.p
% 21.17/13.19 fof(ax_proh_relator_remedy, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((proh(X0) & ('has$urem'(X0) & (aee(X0,X1) & (aer(X0,X2) & (act(X0,X3) & (tgt(X0,X4) & activates(X5,X0))))))) => ? [X6] : ? [X7] : ? [X8] : (('founds$urem'(X5,X6,X0) & (power(X7) & (bearer(X7,X2) & (cnt(X7,decl(X3),X4) & ('part$uof'(X7,X6) & (subjection(X8) & (bearer(X8,X1) & (cnt(X8,decl(X3),X4) & 'part$uof'(X8,X6))))))))))))).
% 21.17/13.19 fof(ax_B2, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((power(X0) & (cnt(X0,decl(X1),X2) & ('part$uof'(X0,X3) & 'founds$urem'(X4,X3,X5)))) => 'about$uevent'(X0,X4)))).
% 21.17/13.19 fof(ax_B3, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((subjection(X0) & (cnt(X0,decl(X1),X2) & ('part$uof'(X0,X3) & 'founds$urem'(X4,X3,X5)))) => 'about$uevent'(X0,X4)))).
% 21.17/13.19 fof(proh_f1, axiom, proh(f1)).
% 21.17/13.19 fof(rem_f1, axiom, 'has$urem'(f1)).
% 21.17/13.19 fof(aee_f1, axiom, aee(f1,marketplace)).
% 21.17/13.19 fof(aer_f1, axiom, aer(f1,philharmonie)).
% 21.17/13.19 fof(act_f1, axiom, act(f1,distrib)).
% 21.17/13.19 fof(tgt_f1, axiom, tgt(f1,'concert$uds')).
% 21.17/13.19 fof(act_e1_f1, axiom, activates(e1,f1)).
% 21.17/13.19 fof(conjecture, conjecture, ? [X0] : ? [X1] : ? [X2] : (('founds$urem'(e1,X0,f1) & (power(X1) & (bearer(X1,philharmonie) & (cnt(X1,decl(distrib),'concert$uds') & ('part$uof'(X1,X0) & ('about$uevent'(X1,e1) & (subjection(X2) & (bearer(X2,marketplace) & (cnt(X2,decl(distrib),'concert$uds') & ('part$uof'(X2,X0) & 'about$uevent'(X2,e1))))))))))))).
% 21.17/13.19 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : (('founds$urem'(e1,X0,f1) & (power(X1) & (bearer(X1,philharmonie) & (cnt(X1,decl(distrib),'concert$uds') & ('part$uof'(X1,X0) & ('about$uevent'(X1,e1) & (subjection(X2) & (bearer(X2,marketplace) & (cnt(X2,decl(distrib),'concert$uds') & ('part$uof'(X2,X0) & 'about$uevent'(X2,e1)))))))))))), inference(negate_conjecture, [status(cth)], [conjecture])).
% 21.17/13.19 cnf(c10, plain, ~activates(X0,X1) | ~tgt(X1,X2) | ~aer(X1,X3) | ~'has$urem'(X1) | ~proh(X1) | X4(X5,X0,X1,X2,X6,X3) | ~aee(X1,X6) | ~act(X1,X5), inference(clausification, [status(esa)], [ax_proh_relator_remedy])).
% 21.17/13.19 cnf(c11, plain, ~X0(X1,X2,X3,X4,X5,X6) | 'founds$urem'(X2,sK17(X5,X3,X4,X1,X2,X6),X3), inference(clausification, [status(esa)], [ax_proh_relator_remedy])).
% 21.17/13.19 cnf(c12, plain, ~X0(X1,X2,X3,X4,X5,X6) | power(sK18(X5,X3,X4,X1,X2,X6)), inference(clausification, [status(esa)], [ax_proh_relator_remedy])).
% 21.17/13.19 cnf(c13, plain, ~X0(X1,X2,X3,X4,X5,X6) | bearer(sK18(X5,X3,X4,X1,X2,X6),X6), inference(clausification, [status(esa)], [ax_proh_relator_remedy])).
% 21.17/13.19 cnf(c14, plain, ~X0(X1,X2,X3,X4,X5,X6) | cnt(sK18(X5,X3,X4,X1,X2,X6),decl(X1),X4), inference(clausification, [status(esa)], [ax_proh_relator_remedy])).
% 21.17/13.19 cnf(c15, plain, ~X0(X1,X2,X3,X4,X5,X6) | 'part$uof'(sK18(X5,X3,X4,X1,X2,X6),sK17(X5,X3,X4,X1,X2,X6)), inference(clausification, [status(esa)], [ax_proh_relator_remedy])).
% 21.17/13.19 cnf(c16, plain, ~X0(X1,X2,X3,X4,X5,X6) | subjection(sK19(X5,X3,X4,X1,X2,X6)), inference(clausification, [status(esa)], [ax_proh_relator_remedy])).
% 21.17/13.19 cnf(c17, plain, ~X0(X1,X2,X3,X4,X5,X6) | bearer(sK19(X5,X3,X4,X1,X2,X6),X5), inference(clausification, [status(esa)], [ax_proh_relator_remedy])).
% 21.17/13.19 cnf(c18, plain, ~X0(X1,X2,X3,X4,X5,X6) | cnt(sK19(X5,X3,X4,X1,X2,X6),decl(X1),X4), inference(clausification, [status(esa)], [ax_proh_relator_remedy])).
% 21.17/13.19 cnf(c19, plain, ~X0(X1,X2,X3,X4,X5,X6) | 'part$uof'(sK19(X5,X3,X4,X1,X2,X6),sK17(X5,X3,X4,X1,X2,X6)), inference(clausification, [status(esa)], [ax_proh_relator_remedy])).
% 21.17/13.19 cnf(c32, plain, ~'founds$urem'(X0,X1,X2) | 'about$uevent'(X3,X0) | ~power(X3) | ~'part$uof'(X3,X1) | ~cnt(X3,decl(X4),X5), inference(clausification, [status(esa)], [ax_B2])).
% 21.17/13.19 cnf(c33, plain, ~'founds$urem'(X0,X1,X2) | 'about$uevent'(X3,X0) | ~subjection(X3) | ~'part$uof'(X3,X1) | ~cnt(X3,decl(X4),X5), inference(clausification, [status(esa)], [ax_B3])).
% 21.17/13.19 cnf(c40, plain, proh(f1), inference(clausification, [status(esa)], [proh_f1])).
% 21.17/13.19 cnf(c41, plain, 'has$urem'(f1), inference(clausification, [status(esa)], [rem_f1])).
% 21.17/13.19 cnf(c42, plain, aee(f1,marketplace), inference(clausification, [status(esa)], [aee_f1])).
% 21.17/13.19 cnf(c43, plain, aer(f1,philharmonie), inference(clausification, [status(esa)], [aer_f1])).
% 21.17/13.19 cnf(c44, plain, act(f1,distrib), inference(clausification, [status(esa)], [act_f1])).
% 21.17/13.19 cnf(c45, plain, tgt(f1,'concert$uds'), inference(clausification, [status(esa)], [tgt_f1])).
% 21.17/13.19 cnf(c46, plain, activates(e1,f1), inference(clausification, [status(esa)], [act_e1_f1])).
% 21.17/13.19 cnf(c48, plain, ~'part$uof'(X0,X1) | ~subjection(X2) | ~cnt(X2,decl(distrib),'concert$uds') | ~'part$uof'(X2,X1) | ~'founds$urem'(e1,X1,f1) | ~'about$uevent'(X0,e1) | ~bearer(X0,philharmonie) | ~cnt(X0,decl(distrib),'concert$uds') | ~'about$uevent'(X2,e1) | ~bearer(X2,marketplace) | ~power(X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 21.17/13.19 cnf(d0, plain, ~'part$uof'(sK19(X0,X1,X2,X3,X4,X5),X6) | ~'founds$urem'(X7,X6,X8) | ~subjection(sK19(X0,X1,X2,X3,X4,X5)) | 'about$uevent'(sK19(X0,X1,X2,X3,X4,X5),X7) | ~'Ts10'(X3,X4,X1,X2,X0,X5), inference(resolution, [status(thm)], [c33,c18])).
% 21.17/13.19 cnf(d1, plain, ~'Ts10'(X0,X1,X2,X3,X4,X5) | ~'founds$urem'(X6,sK17(X4,X2,X3,X0,X1,X5),X7) | ~subjection(sK19(X4,X2,X3,X0,X1,X5)) | 'about$uevent'(sK19(X4,X2,X3,X0,X1,X5),X6) | ~'Ts10'(X0,X1,X2,X3,X4,X5), inference(resolution, [status(thm)], [d0,c19])).
% 21.17/13.19 cnf(d2, plain, ~'Ts10'(X0,X1,X2,X3,X4,X5) | ~subjection(sK19(X4,X2,X3,X0,X1,X5)) | 'about$uevent'(sK19(X4,X2,X3,X0,X1,X5),X1) | ~'Ts10'(X0,X1,X2,X3,X4,X5), inference(resolution, [status(thm)], [d1,c11])).
% 21.17/13.19 cnf(d3, plain, ~'Ts10'(distrib,X0,X1,'concert$uds',X2,X3) | ~bearer(X4,marketplace) | ~bearer(sK18(X2,X1,'concert$uds',distrib,X0,X3),philharmonie) | ~cnt(X4,decl(distrib),'concert$uds') | ~'part$uof'(X4,X5) | ~'part$uof'(sK18(X2,X1,'concert$uds',distrib,X0,X3),X5) | ~'founds$urem'(e1,X5,f1) | ~power(sK18(X2,X1,'concert$uds',distrib,X0,X3)) | ~subjection(X4) | ~'about$uevent'(X4,e1) | ~'about$uevent'(sK18(X2,X1,'concert$uds',distrib,X0,X3),e1), inference(resolution, [status(thm)], [c14,c48])).
% 21.17/13.19 cnf(d4, plain, ~'part$uof'(sK18(X0,X1,X2,X3,X4,X5),X6) | ~'founds$urem'(X7,X6,X8) | ~power(sK18(X0,X1,X2,X3,X4,X5)) | 'about$uevent'(sK18(X0,X1,X2,X3,X4,X5),X7) | ~'Ts10'(X3,X4,X1,X2,X0,X5), inference(resolution, [status(thm)], [c32,c14])).
% 21.17/13.19 cnf(d5, plain, ~'Ts10'(X0,X1,X2,X3,X4,X5) | ~'founds$urem'(X6,sK17(X4,X2,X3,X0,X1,X5),X7) | ~power(sK18(X4,X2,X3,X0,X1,X5)) | 'about$uevent'(sK18(X4,X2,X3,X0,X1,X5),X6) | ~'Ts10'(X0,X1,X2,X3,X4,X5), inference(resolution, [status(thm)], [d4,c15])).
% 21.17/13.19 cnf(d6, plain, ~'Ts10'(X0,X1,X2,X3,X4,X5) | ~power(sK18(X4,X2,X3,X0,X1,X5)) | 'about$uevent'(sK18(X4,X2,X3,X0,X1,X5),X1) | ~'Ts10'(X0,X1,X2,X3,X4,X5), inference(resolution, [status(thm)], [d5,c11])).
% 21.17/13.19 cnf(d7, plain, ~'Ts10'(distrib,e1,X0,'concert$uds',X1,X2) | ~power(sK18(X1,X0,'concert$uds',distrib,e1,X2)) | ~bearer(X3,marketplace) | ~bearer(sK18(X1,X0,'concert$uds',distrib,e1,X2),philharmonie) | ~cnt(X3,decl(distrib),'concert$uds') | ~'part$uof'(X3,X4) | ~'part$uof'(sK18(X1,X0,'concert$uds',distrib,e1,X2),X4) | ~'Ts10'(distrib,e1,X0,'concert$uds',X1,X2) | ~'founds$urem'(e1,X4,f1) | ~power(sK18(X1,X0,'concert$uds',distrib,e1,X2)) | ~subjection(X3) | ~'about$uevent'(X3,e1), inference(resolution, [status(thm)], [d6,d3])).
% 21.17/13.19 cnf(d8, plain, ~bearer(X0,marketplace) | ~bearer(sK18(X1,X2,'concert$uds',distrib,e1,X3),philharmonie) | ~cnt(X0,decl(distrib),'concert$uds') | ~'part$uof'(X0,sK17(X1,X2,'concert$uds',distrib,e1,X3)) | ~'Ts10'(distrib,e1,X2,'concert$uds',X1,X3) | ~'founds$urem'(e1,sK17(X1,X2,'concert$uds',distrib,e1,X3),f1) | ~power(sK18(X1,X2,'concert$uds',distrib,e1,X3)) | ~subjection(X0) | ~'about$uevent'(X0,e1) | ~'Ts10'(distrib,e1,X2,'concert$uds',X1,X3), inference(resolution, [status(thm)], [d7,c15])).
% 21.17/13.19 cnf(d9, plain, ~bearer(X0,marketplace) | ~bearer(sK18(X1,f1,'concert$uds',distrib,e1,X2),philharmonie) | ~cnt(X0,decl(distrib),'concert$uds') | ~'part$uof'(X0,sK17(X1,f1,'concert$uds',distrib,e1,X2)) | ~'Ts10'(distrib,e1,f1,'concert$uds',X1,X2) | ~power(sK18(X1,f1,'concert$uds',distrib,e1,X2)) | ~subjection(X0) | ~'about$uevent'(X0,e1) | ~'Ts10'(distrib,e1,f1,'concert$uds',X1,X2), inference(resolution, [status(thm)], [d8,c11])).
% 21.17/13.19 cnf(d10, plain, ~bearer(sK19(X0,f1,'concert$uds',distrib,e1,X1),marketplace) | ~bearer(sK18(X0,f1,'concert$uds',distrib,e1,X1),philharmonie) | ~cnt(sK19(X0,f1,'concert$uds',distrib,e1,X1),decl(distrib),'concert$uds') | ~'Ts10'(distrib,e1,f1,'concert$uds',X0,X1) | ~power(sK18(X0,f1,'concert$uds',distrib,e1,X1)) | ~subjection(sK19(X0,f1,'concert$uds',distrib,e1,X1)) | ~'about$uevent'(sK19(X0,f1,'concert$uds',distrib,e1,X1),e1) | ~'Ts10'(distrib,e1,f1,'concert$uds',X0,X1), inference(resolution, [status(thm)], [d9,c19])).
% 21.17/13.19 cnf(d11, plain, ~bearer(sK18(X0,f1,'concert$uds',distrib,e1,X1),philharmonie) | ~bearer(sK19(X0,f1,'concert$uds',distrib,e1,X1),marketplace) | ~'Ts10'(distrib,e1,f1,'concert$uds',X0,X1) | ~power(sK18(X0,f1,'concert$uds',distrib,e1,X1)) | ~subjection(sK19(X0,f1,'concert$uds',distrib,e1,X1)) | ~'about$uevent'(sK19(X0,f1,'concert$uds',distrib,e1,X1),e1) | ~'Ts10'(distrib,e1,f1,'concert$uds',X0,X1), inference(resolution, [status(thm)], [d10,c18])).
% 21.17/13.19 cnf(d12, plain, ~bearer(sK18(X0,f1,'concert$uds',distrib,e1,X1),philharmonie) | ~bearer(sK19(X0,f1,'concert$uds',distrib,e1,X1),marketplace) | ~'Ts10'(distrib,e1,f1,'concert$uds',X0,X1) | ~power(sK18(X0,f1,'concert$uds',distrib,e1,X1)) | ~subjection(sK19(X0,f1,'concert$uds',distrib,e1,X1)) | ~'Ts10'(distrib,e1,f1,'concert$uds',X0,X1) | ~subjection(sK19(X0,f1,'concert$uds',distrib,e1,X1)), inference(resolution, [status(thm)], [d11,d2])).
% 21.17/13.19 cnf(d13, plain, ~bearer(sK18(marketplace,f1,'concert$uds',distrib,e1,X0),philharmonie) | ~'Ts10'(distrib,e1,f1,'concert$uds',marketplace,X0) | ~power(sK18(marketplace,f1,'concert$uds',distrib,e1,X0)) | ~subjection(sK19(marketplace,f1,'concert$uds',distrib,e1,X0)) | ~'Ts10'(distrib,e1,f1,'concert$uds',marketplace,X0), inference(resolution, [status(thm)], [d12,c17])).
% 21.17/13.19 cnf(d14, plain, ~'Ts10'(distrib,e1,f1,'concert$uds',marketplace,philharmonie) | ~power(sK18(marketplace,f1,'concert$uds',distrib,e1,philharmonie)) | ~subjection(sK19(marketplace,f1,'concert$uds',distrib,e1,philharmonie)) | ~'Ts10'(distrib,e1,f1,'concert$uds',marketplace,philharmonie), inference(resolution, [status(thm)], [d13,c13])).
% 21.17/13.19 cnf(d15, plain, ~'Ts10'(distrib,e1,f1,'concert$uds',marketplace,philharmonie) | ~power(sK18(marketplace,f1,'concert$uds',distrib,e1,philharmonie)) | ~'Ts10'(distrib,e1,f1,'concert$uds',marketplace,philharmonie), inference(resolution, [status(thm)], [d14,c16])).
% 21.17/13.19 cnf(d16, plain, ~'Ts10'(distrib,e1,f1,'concert$uds',marketplace,philharmonie) | ~'Ts10'(distrib,e1,f1,'concert$uds',marketplace,philharmonie), inference(resolution, [status(thm)], [d15,c12])).
% 21.17/13.19 cnf(d17, plain, ~act(f1,distrib) | ~aee(f1,marketplace) | ~activates(e1,f1) | ~tgt(f1,'concert$uds') | ~aer(f1,philharmonie) | ~proh(f1) | ~'has$urem'(f1), inference(resolution, [status(thm)], [d16,c10])).
% 21.17/13.19 cnf(d18, plain, ~act(f1,distrib) | ~aee(f1,marketplace) | ~activates(e1,f1) | ~tgt(f1,'concert$uds') | ~aer(f1,philharmonie) | ~'has$urem'(f1), inference(resolution, [status(thm)], [c40,d17])).
% 21.17/13.19 cnf(d19, plain, ~act(f1,distrib) | ~aee(f1,marketplace) | ~activates(e1,f1) | ~tgt(f1,'concert$uds') | ~aer(f1,philharmonie), inference(resolution, [status(thm)], [c41,d18])).
% 21.17/13.19 cnf(d20, plain, ~act(f1,distrib) | ~activates(e1,f1) | ~tgt(f1,'concert$uds') | ~aer(f1,philharmonie), inference(resolution, [status(thm)], [c42,d19])).
% 21.17/13.19 cnf(d21, plain, ~act(f1,distrib) | ~activates(e1,f1) | ~tgt(f1,'concert$uds'), inference(resolution, [status(thm)], [c43,d20])).
% 21.17/13.19 cnf(d22, plain, ~activates(e1,f1) | ~tgt(f1,'concert$uds'), inference(resolution, [status(thm)], [c44,d21])).
% 21.17/13.19 cnf(d23, plain, ~activates(e1,f1), inference(resolution, [status(thm)], [c45,d22])).
% 21.17/13.19 cnf(d24, plain, $false, inference(resolution, [status(thm)], [c46,d23])).
% 21.17/13.19 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------