%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT117+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 : 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:01:32 AM UTC 2026
% Result : Theorem 11.18s 1.85s
% Output : CNFRefutation 11.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT117+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n026.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 00:17:25 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.18/1.85 % SZS status Theorem for theBenchmark.p
% 11.18/1.85 % SZS output start CNFRefutation for theBenchmark.p
% 11.18/1.85 fof(ax_perm_relator_strong, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((perm(X0) & (strong(X0) & (aee(X0,X1) & (aer(X0,X2) & (act(X0,X3) & (tgt(X0,X4) & activates(X5,X0))))))) => ? [X6] : ? [X7] : ? [X8] : (('founds$uimm'(X5,X6,X0) & (immunity(X7) & (bearer(X7,X1) & (cnt(X7,X3,X4) & ('part$uof'(X7,X6) & (disability(X8) & (bearer(X8,X2) & (cnt(X8,X3,X4) & 'part$uof'(X8,X6))))))))))))).
% 11.18/1.85 fof(perm_p1, axiom, perm(p1)).
% 11.18/1.85 fof(strong_p1, axiom, strong(p1)).
% 11.18/1.85 fof(aee_p1, axiom, aee(p1,bibliothek)).
% 11.18/1.85 fof(aer_p1, axiom, aer(p1,museen)).
% 11.18/1.85 fof(act_p1, axiom, act(p1,read)).
% 11.18/1.85 fof(tgt_p1, axiom, tgt(p1,'museum$uapi')).
% 11.18/1.85 fof(act_e1_p1, axiom, activates(e1,p1)).
% 11.18/1.85 fof(conjecture, conjecture, ? [X0] : ? [X1] : (('founds$uimm'(e1,X0,p1) & (disability(X1) & (bearer(X1,museen) & (cnt(X1,read,'museum$uapi') & 'part$uof'(X1,X0))))))).
% 11.18/1.85 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : (('founds$uimm'(e1,X0,p1) & (disability(X1) & (bearer(X1,museen) & (cnt(X1,read,'museum$uapi') & 'part$uof'(X1,X0)))))), inference(negate_conjecture, [status(cth)], [conjecture])).
% 11.18/1.85 cnf(c0, plain, ~aee(X0,X1) | ~strong(X0) | ~activates(X2,X0) | X3(X4,X2,X0,X5,X1,X6) | ~aer(X0,X6) | ~act(X0,X4) | ~tgt(X0,X5) | ~perm(X0), inference(clausification, [status(esa)], [ax_perm_relator_strong])).
% 11.18/1.85 cnf(c1, plain, ~X0(X1,X2,X3,X4,X5,X6) | 'founds$uimm'(X2,sK7(X3,X5,X4,X1,X2,X6),X3), inference(clausification, [status(esa)], [ax_perm_relator_strong])).
% 11.18/1.85 cnf(c6, plain, ~X0(X1,X2,X3,X4,X5,X6) | disability(sK9(X3,X5,X4,X1,X2,X6)), inference(clausification, [status(esa)], [ax_perm_relator_strong])).
% 11.18/1.85 cnf(c7, plain, ~X0(X1,X2,X3,X4,X5,X6) | bearer(sK9(X3,X5,X4,X1,X2,X6),X6), inference(clausification, [status(esa)], [ax_perm_relator_strong])).
% 11.18/1.85 cnf(c8, plain, ~X0(X1,X2,X3,X4,X5,X6) | cnt(sK9(X3,X5,X4,X1,X2,X6),X1,X4), inference(clausification, [status(esa)], [ax_perm_relator_strong])).
% 11.18/1.85 cnf(c9, plain, ~X0(X1,X2,X3,X4,X5,X6) | 'part$uof'(sK9(X3,X5,X4,X1,X2,X6),sK7(X3,X5,X4,X1,X2,X6)), inference(clausification, [status(esa)], [ax_perm_relator_strong])).
% 11.18/1.85 cnf(c16, plain, perm(p1), inference(clausification, [status(esa)], [perm_p1])).
% 11.18/1.85 cnf(c17, plain, strong(p1), inference(clausification, [status(esa)], [strong_p1])).
% 11.18/1.85 cnf(c18, plain, aee(p1,bibliothek), inference(clausification, [status(esa)], [aee_p1])).
% 11.18/1.85 cnf(c19, plain, aer(p1,museen), inference(clausification, [status(esa)], [aer_p1])).
% 11.18/1.85 cnf(c20, plain, act(p1,read), inference(clausification, [status(esa)], [act_p1])).
% 11.18/1.85 cnf(c21, plain, tgt(p1,'museum$uapi'), inference(clausification, [status(esa)], [tgt_p1])).
% 11.18/1.85 cnf(c22, plain, activates(e1,p1), inference(clausification, [status(esa)], [act_e1_p1])).
% 11.18/1.85 cnf(c23, plain, ~cnt(X0,read,'museum$uapi') | ~'founds$uimm'(e1,X1,p1) | ~disability(X0) | ~'part$uof'(X0,X1) | ~bearer(X0,museen), inference(clausification, [status(esa)], [negated_conjecture])).
% 11.18/1.85 cnf(d0, plain, ~'Ts0'(read,X0,X1,'museum$uapi',X2,X3) | ~'founds$uimm'(e1,X4,p1) | ~bearer(sK9(X1,X2,'museum$uapi',read,X0,X3),museen) | ~'part$uof'(sK9(X1,X2,'museum$uapi',read,X0,X3),X4) | ~disability(sK9(X1,X2,'museum$uapi',read,X0,X3)), inference(resolution, [status(thm)], [c8,c23])).
% 11.18/1.85 cnf(d1, plain, ~'Ts0'(read,X0,X1,'museum$uapi',X2,X3) | ~'founds$uimm'(e1,sK7(X1,X2,'museum$uapi',read,X0,X3),p1) | ~bearer(sK9(X1,X2,'museum$uapi',read,X0,X3),museen) | ~disability(sK9(X1,X2,'museum$uapi',read,X0,X3)) | ~'Ts0'(read,X0,X1,'museum$uapi',X2,X3), inference(resolution, [status(thm)], [d0,c9])).
% 11.18/1.85 cnf(d2, plain, ~'Ts0'(read,e1,p1,'museum$uapi',X0,X1) | ~bearer(sK9(p1,X0,'museum$uapi',read,e1,X1),museen) | ~disability(sK9(p1,X0,'museum$uapi',read,e1,X1)) | ~'Ts0'(read,e1,p1,'museum$uapi',X0,X1), inference(resolution, [status(thm)], [d1,c1])).
% 11.18/1.85 cnf(d3, plain, ~'Ts0'(read,e1,p1,'museum$uapi',X0,museen) | ~disability(sK9(p1,X0,'museum$uapi',read,e1,museen)) | ~'Ts0'(read,e1,p1,'museum$uapi',X0,museen), inference(resolution, [status(thm)], [d2,c7])).
% 11.18/1.85 cnf(d4, plain, ~'Ts0'(read,e1,p1,'museum$uapi',X0,museen) | ~'Ts0'(read,e1,p1,'museum$uapi',X0,museen), inference(resolution, [status(thm)], [d3,c6])).
% 11.18/1.85 cnf(d5, plain, ~act(p1,read) | ~aee(p1,X0) | ~activates(e1,p1) | ~tgt(p1,'museum$uapi') | ~aer(p1,museen) | ~strong(p1) | ~perm(p1), inference(resolution, [status(thm)], [d4,c0])).
% 11.18/1.85 cnf(d6, plain, ~act(p1,read) | ~aee(p1,X0) | ~activates(e1,p1) | ~tgt(p1,'museum$uapi') | ~aer(p1,museen) | ~strong(p1), inference(resolution, [status(thm)], [c16,d5])).
% 11.18/1.85 cnf(d7, plain, ~act(p1,read) | ~aee(p1,X0) | ~activates(e1,p1) | ~tgt(p1,'museum$uapi') | ~aer(p1,museen), inference(resolution, [status(thm)], [c17,d6])).
% 11.18/1.85 cnf(d8, plain, ~act(p1,read) | ~aee(p1,X0) | ~activates(e1,p1) | ~tgt(p1,'museum$uapi'), inference(resolution, [status(thm)], [c19,d7])).
% 11.18/1.85 cnf(d9, plain, ~aee(p1,X0) | ~activates(e1,p1) | ~tgt(p1,'museum$uapi'), inference(resolution, [status(thm)], [c20,d8])).
% 11.18/1.85 cnf(d10, plain, ~aee(p1,X0) | ~activates(e1,p1), inference(resolution, [status(thm)], [c21,d9])).
% 11.18/1.85 cnf(d11, plain, ~aee(p1,X0), inference(resolution, [status(thm)], [c22,d10])).
% 11.18/1.85 cnf(d12, plain, $false, inference(resolution, [status(thm)], [d11,c18])).
% 11.18/1.85 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------