%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT111+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 : n016.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 7.80s 2.49s
% Output : CNFRefutation 7.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT111+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.46 % Computer : n016.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Sat Sep 26 00:19:15 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.80/2.49 % SZS status Theorem for theBenchmark.p
% 7.80/2.49 % SZS output start CNFRefutation for theBenchmark.p
% 7.80/2.49 fof(agent_portal, axiom, agent(portal)).
% 7.80/2.49 fof(action_modify, axiom, action('modify$uact')).
% 7.80/2.49 fof(target_theater, axiom, target('theater$uds')).
% 7.80/2.49 fof(no_proh_modify, axiom, ~? [X0] : ? [X1] : ((proh(X0) & (aee(X0,portal) & (act(X0,'modify$uact') & activates(X1,X0)))))).
% 7.80/2.49 fof(open_world_closure, axiom, ! [X0] : ! [X1] : ! [X2] : (((agent(X0) & (action(X1) & (target(X2) & ~? [X3] : ? [X4] : ((proh(X3) & (aee(X3,X0) & (act(X3,X1) & activates(X4,X3)))))))) => ? [X5] : ((permission(X5) & (bearer(X5,X0) & cnt(X5,X1,X2))))))).
% 7.80/2.49 fof(conjecture, conjecture, ? [X0] : ((permission(X0) & (bearer(X0,portal) & cnt(X0,'modify$uact','theater$uds'))))).
% 7.80/2.49 fof(negated_conjecture, negated_conjecture, ~? [X0] : ((permission(X0) & (bearer(X0,portal) & cnt(X0,'modify$uact','theater$uds')))), inference(negate_conjecture, [status(cth)], [conjecture])).
% 7.80/2.49 cnf(c0, plain, agent(portal), inference(clausification, [status(esa)], [agent_portal])).
% 7.80/2.49 cnf(c2, plain, action('modify$uact'), inference(clausification, [status(esa)], [action_modify])).
% 7.80/2.49 cnf(c3, plain, target('theater$uds'), inference(clausification, [status(esa)], [target_theater])).
% 7.80/2.49 cnf(c4, plain, ~proh(X0) | ~aee(X0,portal) | ~act(X0,'modify$uact') | ~activates(X1,X0), inference(clausification, [status(esa)], [no_proh_modify])).
% 7.80/2.49 cnf(c5, plain, X0(X1,X2,X3) | permission(sK6(X3,X1,X2)), inference(clausification, [status(esa)], [open_world_closure])).
% 7.80/2.49 cnf(c6, plain, X0(X1,X2,X3) | bearer(sK6(X3,X1,X2),X3), inference(clausification, [status(esa)], [open_world_closure])).
% 7.80/2.49 cnf(c7, plain, X0(X1,X2,X3) | cnt(sK6(X3,X1,X2),X1,X2), inference(clausification, [status(esa)], [open_world_closure])).
% 7.80/2.49 cnf(c8, plain, ~agent(X0) | proh(sK7(X1,X0)) | ~X2(X1,X3,X0) | ~action(X1) | ~target(X3), inference(clausification, [status(esa)], [open_world_closure])).
% 7.80/2.49 cnf(c9, plain, ~agent(X0) | ~action(X1) | ~target(X2) | aee(sK7(X1,X0),X0) | ~X3(X1,X2,X0), inference(clausification, [status(esa)], [open_world_closure])).
% 7.80/2.49 cnf(c10, plain, ~agent(X0) | ~X1(X2,X3,X0) | ~action(X2) | act(sK7(X2,X0),X2) | ~target(X3), inference(clausification, [status(esa)], [open_world_closure])).
% 7.80/2.49 cnf(c11, plain, activates(sK8(X0,X1),sK7(X0,X1)) | ~agent(X1) | ~X2(X0,X3,X1) | ~action(X0) | ~target(X3), inference(clausification, [status(esa)], [open_world_closure])).
% 7.80/2.49 cnf(c12, plain, ~permission(X0) | ~bearer(X0,portal) | ~cnt(X0,'modify$uact','theater$uds'), inference(clausification, [status(esa)], [negated_conjecture])).
% 7.80/2.49 cnf(d0, plain, 'Ts2'('modify$uact','theater$uds',X0) | ~permission(sK6(X0,'modify$uact','theater$uds')) | ~bearer(sK6(X0,'modify$uact','theater$uds'),portal), inference(resolution, [status(thm)], [c7,c12])).
% 7.80/2.49 cnf(d1, plain, ~permission(sK6(portal,'modify$uact','theater$uds')) | 'Ts2'('modify$uact','theater$uds',portal) | 'Ts2'('modify$uact','theater$uds',portal), inference(resolution, [status(thm)], [d0,c6])).
% 7.80/2.49 cnf(d2, plain, 'Ts2'('modify$uact','theater$uds',portal) | 'Ts2'('modify$uact','theater$uds',portal), inference(resolution, [status(thm)], [d1,c5])).
% 7.80/2.50 cnf(d3, plain, ~agent(portal) | ~action('modify$uact') | ~target('theater$uds') | activates(sK8('modify$uact',portal),sK7('modify$uact',portal)), inference(resolution, [status(thm)], [c11,d2])).
% 7.80/2.50 cnf(d4, plain, ~action('modify$uact') | ~target('theater$uds') | activates(sK8('modify$uact',portal),sK7('modify$uact',portal)), inference(resolution, [status(thm)], [c0,d3])).
% 7.80/2.50 cnf(d5, plain, ~target('theater$uds') | activates(sK8('modify$uact',portal),sK7('modify$uact',portal)), inference(resolution, [status(thm)], [c2,d4])).
% 7.80/2.50 cnf(d6, plain, activates(sK8('modify$uact',portal),sK7('modify$uact',portal)), inference(resolution, [status(thm)], [c3,d5])).
% 7.80/2.50 cnf(d7, plain, ~agent(portal) | ~action('modify$uact') | ~target('theater$uds') | aee(sK7('modify$uact',portal),portal), inference(resolution, [status(thm)], [d2,c9])).
% 7.80/2.50 cnf(d8, plain, ~action('modify$uact') | ~target('theater$uds') | aee(sK7('modify$uact',portal),portal), inference(resolution, [status(thm)], [c0,d7])).
% 7.80/2.50 cnf(d9, plain, ~target('theater$uds') | aee(sK7('modify$uact',portal),portal), inference(resolution, [status(thm)], [c2,d8])).
% 7.80/2.50 cnf(d10, plain, aee(sK7('modify$uact',portal),portal), inference(resolution, [status(thm)], [c3,d9])).
% 7.80/2.50 cnf(d11, plain, ~act(sK7('modify$uact',portal),'modify$uact') | ~proh(sK7('modify$uact',portal)) | ~activates(X0,sK7('modify$uact',portal)), inference(resolution, [status(thm)], [d10,c4])).
% 7.80/2.50 cnf(d12, plain, ~agent(portal) | ~action('modify$uact') | ~target('theater$uds') | proh(sK7('modify$uact',portal)), inference(resolution, [status(thm)], [d2,c8])).
% 7.80/2.50 cnf(d13, plain, ~action('modify$uact') | ~target('theater$uds') | proh(sK7('modify$uact',portal)), inference(resolution, [status(thm)], [c0,d12])).
% 7.80/2.50 cnf(d14, plain, ~target('theater$uds') | proh(sK7('modify$uact',portal)), inference(resolution, [status(thm)], [c2,d13])).
% 7.80/2.50 cnf(d15, plain, proh(sK7('modify$uact',portal)), inference(resolution, [status(thm)], [c3,d14])).
% 7.80/2.50 cnf(d16, plain, ~act(sK7('modify$uact',portal),'modify$uact') | ~activates(X0,sK7('modify$uact',portal)), inference(resolution, [status(thm)], [d15,d11])).
% 7.80/2.50 cnf(d17, plain, ~agent(portal) | ~action('modify$uact') | ~target('theater$uds') | act(sK7('modify$uact',portal),'modify$uact'), inference(resolution, [status(thm)], [d2,c10])).
% 7.80/2.50 cnf(d18, plain, ~action('modify$uact') | ~target('theater$uds') | act(sK7('modify$uact',portal),'modify$uact'), inference(resolution, [status(thm)], [c0,d17])).
% 7.80/2.50 cnf(d19, plain, ~target('theater$uds') | act(sK7('modify$uact',portal),'modify$uact'), inference(resolution, [status(thm)], [c2,d18])).
% 7.80/2.50 cnf(d20, plain, act(sK7('modify$uact',portal),'modify$uact'), inference(resolution, [status(thm)], [c3,d19])).
% 7.80/2.50 cnf(d21, plain, ~activates(X0,sK7('modify$uact',portal)), inference(resolution, [status(thm)], [d20,d16])).
% 7.80/2.50 cnf(d22, plain, $false, inference(resolution, [status(thm)], [d21,d6])).
% 7.80/2.50 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------