%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT114+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/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:32 AM UTC 2026
% Result : Unsatisfiable 8.00s 18.75s
% Output : CNFRefutation 8.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT114+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.15/15.67 % CPULimit : 300
% 0.15/15.67 % WCLimit : 300
% 0.15/15.67 % DateTime : Sat Sep 26 00:20:14 UTC 2026
% 0.15/15.68 % CPUTime :
% 0.15/15.68 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.00/18.75 % SZS status Unsatisfiable for theBenchmark.p
% 8.00/18.75 % SZS output start CNFRefutation for theBenchmark.p
% 8.00/18.75 fof(ax_correlativity_permission, axiom, ! [X0] : ! [X1] : ! [X2] : (('odrl$urel'(X0) => (? [X3] : ((permission(X3) & ('part$uof'(X3,X0) & (cnt(X3,X1,X2) & ! [X4] : (((permission(X4) & ('part$uof'(X4,X0) & cnt(X4,X1,X2))) => X4 = X3)))))) <=> ? [X5] : (('no$uright'(X5) & ('part$uof'(X5,X0) & (cnt(X5,X1,X2) & ! [X6] : ((('no$uright'(X6) & ('part$uof'(X6,X0) & cnt(X6,X1,X2))) => X6 = X5)))))))))).
% 8.00/18.75 fof(odrl_rho1, axiom, 'odrl$urel'(rho1)).
% 8.00/18.75 fof(permission_l, axiom, permission(l)).
% 8.00/18.75 fof(no_right_n1, axiom, 'no$uright'(n1)).
% 8.00/18.75 fof(no_right_n2, axiom, 'no$uright'(n2)).
% 8.00/18.75 fof(partof_l, axiom, 'part$uof'(l,rho1)).
% 8.00/18.75 fof(partof_n1, axiom, 'part$uof'(n1,rho1)).
% 8.00/18.75 fof(partof_n2, axiom, 'part$uof'(n2,rho1)).
% 8.00/18.75 fof(cnt_l, axiom, cnt(l,'some$uaction','some$utarget')).
% 8.00/18.75 fof(cnt_n1, axiom, cnt(n1,'some$uaction','some$utarget')).
% 8.00/18.75 fof(cnt_n2, axiom, cnt(n2,'some$uaction','some$utarget')).
% 8.00/18.75 fof(n1_neq_n2, axiom, n1 != n2).
% 8.00/18.75 fof(perm_l_unique, axiom, ! [X0] : (((permission(X0) & ('part$uof'(X0,rho1) & cnt(X0,'some$uaction','some$utarget'))) => X0 = l))).
% 8.00/18.75 cnf(c0, plain, ~'odrl$urel'(X0) | ~X1(X2,X0,X3) | X4(X2,X0,X3), inference(clausification, [status(esa)], [ax_correlativity_permission])).
% 8.00/18.75 cnf(c6, plain, X0(X1,X2,X3) | permission(sK8(X1,X2,X3,X4)) | ~permission(X4) | ~'part$uof'(X4,X2) | ~cnt(X4,X1,X3), inference(clausification, [status(esa)], [ax_correlativity_permission])).
% 8.00/18.75 cnf(c7, plain, X0(X1,X2,X3) | ~'part$uof'(X4,X2) | ~cnt(X4,X1,X3) | ~permission(X4) | 'part$uof'(sK8(X1,X2,X3,X4),X2), inference(clausification, [status(esa)], [ax_correlativity_permission])).
% 8.00/18.75 cnf(c8, plain, X0(X1,X2,X3) | ~permission(X4) | cnt(sK8(X1,X2,X3,X4),X1,X3) | ~'part$uof'(X4,X2) | ~cnt(X4,X1,X3), inference(clausification, [status(esa)], [ax_correlativity_permission])).
% 8.00/18.75 cnf(c9, plain, X0(X1,X2,X3) | ~permission(X4) | sK8(X1,X2,X3,X4) != X4 | ~'part$uof'(X4,X2) | ~cnt(X4,X1,X3), inference(clausification, [status(esa)], [ax_correlativity_permission])).
% 8.00/18.75 cnf(c13, plain, ~X0(X1,X2,X3) | ~cnt(X4,X1,X3) | X4 = sK9(X1,X2,X3) | ~'part$uof'(X4,X2) | ~'no$uright'(X4), inference(clausification, [status(esa)], [ax_correlativity_permission])).
% 8.00/18.75 cnf(c22, plain, 'odrl$urel'(rho1), inference(clausification, [status(esa)], [odrl_rho1])).
% 8.00/18.75 cnf(c23, plain, permission(l), inference(clausification, [status(esa)], [permission_l])).
% 8.00/18.75 cnf(c24, plain, 'no$uright'(n1), inference(clausification, [status(esa)], [no_right_n1])).
% 8.00/18.75 cnf(c25, plain, 'no$uright'(n2), inference(clausification, [status(esa)], [no_right_n2])).
% 8.00/18.75 cnf(c26, plain, 'part$uof'(l,rho1), inference(clausification, [status(esa)], [partof_l])).
% 8.00/18.75 cnf(c27, plain, 'part$uof'(n1,rho1), inference(clausification, [status(esa)], [partof_n1])).
% 8.00/18.75 cnf(c28, plain, 'part$uof'(n2,rho1), inference(clausification, [status(esa)], [partof_n2])).
% 8.00/18.75 cnf(c29, plain, cnt(l,'some$uaction','some$utarget'), inference(clausification, [status(esa)], [cnt_l])).
% 8.00/18.75 cnf(c30, plain, cnt(n1,'some$uaction','some$utarget'), inference(clausification, [status(esa)], [cnt_n1])).
% 8.00/18.75 cnf(c31, plain, cnt(n2,'some$uaction','some$utarget'), inference(clausification, [status(esa)], [cnt_n2])).
% 8.00/18.75 cnf(c34, plain, n1 != n2, inference(clausification, [status(esa)], [n1_neq_n2])).
% 8.00/18.75 cnf(c35, plain, ~permission(X0) | ~'part$uof'(X0,rho1) | ~cnt(X0,'some$uaction','some$utarget') | X0 = l, inference(clausification, [status(esa)], [perm_l_unique])).
% 8.00/18.75 cnf(d0, plain, n1 = sK9('some$uaction',X0,'some$utarget') | ~'Ts1'('some$uaction',X0,'some$utarget') | ~'part$uof'(n1,X0) | ~'no$uright'(n1), inference(resolution, [status(thm)], [c30,c13])).
% 8.00/18.75 cnf(d1, plain, n1 = sK9('some$uaction',X0,'some$utarget') | ~'Ts1'('some$uaction',X0,'some$utarget') | ~'part$uof'(n1,X0), inference(resolution, [status(thm)], [c24,d0])).
% 8.00/18.75 cnf(d2, plain, sK8('some$uaction',X0,'some$utarget',X1) = l | ~permission(sK8('some$uaction',X0,'some$utarget',X1)) | ~'part$uof'(sK8('some$uaction',X0,'some$utarget',X1),rho1) | 'Ts0'('some$uaction',X0,'some$utarget') | ~permission(X1) | ~'part$uof'(X1,X0) | ~cnt(X1,'some$uaction','some$utarget'), inference(resolution, [status(thm)], [c35,c8])).
% 8.00/18.75 cnf(d3, plain, sK8('some$uaction',rho1,'some$utarget',X0) = l | 'Ts0'('some$uaction',rho1,'some$utarget') | ~permission(X0) | ~permission(sK8('some$uaction',rho1,'some$utarget',X0)) | ~'part$uof'(X0,rho1) | ~cnt(X0,'some$uaction','some$utarget') | 'Ts0'('some$uaction',rho1,'some$utarget') | ~permission(X0) | ~'part$uof'(X0,rho1) | ~cnt(X0,'some$uaction','some$utarget'), inference(resolution, [status(thm)], [d2,c7])).
% 8.00/18.75 cnf(d4, plain, sK8('some$uaction',rho1,'some$utarget',X0) = l | 'Ts0'('some$uaction',rho1,'some$utarget') | ~permission(X0) | ~'part$uof'(X0,rho1) | ~cnt(X0,'some$uaction','some$utarget') | 'Ts0'('some$uaction',rho1,'some$utarget') | ~permission(X0) | ~'part$uof'(X0,rho1) | ~cnt(X0,'some$uaction','some$utarget'), inference(resolution, [status(thm)], [d3,c6])).
% 8.00/18.75 cnf(d5, plain, sK8('some$uaction',rho1,'some$utarget',l) = l | 'Ts0'('some$uaction',rho1,'some$utarget') | ~permission(l) | ~'part$uof'(l,rho1), inference(resolution, [status(thm)], [d4,c29])).
% 8.00/18.75 cnf(d6, plain, sK8('some$uaction',rho1,'some$utarget',l) = l | 'Ts0'('some$uaction',rho1,'some$utarget') | ~'part$uof'(l,rho1), inference(resolution, [status(thm)], [c23,d5])).
% 8.00/18.75 cnf(d7, plain, sK8('some$uaction',rho1,'some$utarget',l) = l | 'Ts0'('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [c26,d6])).
% 8.00/18.75 cnf(d8, plain, sK8('some$uaction',rho1,'some$utarget',l) = l | ~'odrl$urel'(rho1) | 'Ts1'('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [d7,c0])).
% 8.00/18.75 cnf(d9, plain, sK8('some$uaction',rho1,'some$utarget',l) = l | 'Ts1'('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [c22,d8])).
% 8.00/18.75 cnf(d10, plain, sK8('some$uaction',rho1,'some$utarget',l) = l | n1 = sK9('some$uaction',rho1,'some$utarget') | ~'part$uof'(n1,rho1), inference(resolution, [status(thm)], [d9,d1])).
% 8.00/18.75 cnf(d11, plain, sK8('some$uaction',rho1,'some$utarget',l) = l | n1 = sK9('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [c27,d10])).
% 8.00/18.75 cnf(d12, plain, l != l | 'Ts0'('some$uaction',rho1,'some$utarget') | ~permission(l) | ~'part$uof'(l,rho1) | ~cnt(l,'some$uaction','some$utarget') | n1 = sK9('some$uaction',rho1,'some$utarget'), inference(superposition, [status(thm)], [d11,c9])).
% 8.00/18.75 cnf(d13, plain, l != l | n1 = sK9('some$uaction',rho1,'some$utarget') | 'Ts0'('some$uaction',rho1,'some$utarget') | ~'part$uof'(l,rho1) | ~cnt(l,'some$uaction','some$utarget'), inference(resolution, [status(thm)], [c23,d12])).
% 8.00/18.75 cnf(d14, plain, l != l | n1 = sK9('some$uaction',rho1,'some$utarget') | 'Ts0'('some$uaction',rho1,'some$utarget') | ~cnt(l,'some$uaction','some$utarget'), inference(resolution, [status(thm)], [c26,d13])).
% 8.00/18.75 cnf(d15, plain, l != l | n1 = sK9('some$uaction',rho1,'some$utarget') | 'Ts0'('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [c29,d14])).
% 8.00/18.75 cnf(d16, plain, n1 = sK9('some$uaction',rho1,'some$utarget') | 'Ts0'('some$uaction',rho1,'some$utarget'), inference(equality_resolution, [status(thm)], [d15])).
% 8.00/18.75 cnf(d17, plain, n1 = sK9('some$uaction',rho1,'some$utarget') | ~'odrl$urel'(rho1) | 'Ts1'('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [d16,c0])).
% 8.00/18.75 cnf(d18, plain, n1 = sK9('some$uaction',rho1,'some$utarget') | 'Ts1'('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [c22,d17])).
% 8.00/18.75 cnf(d19, plain, n1 = sK9('some$uaction',rho1,'some$utarget') | n1 = sK9('some$uaction',rho1,'some$utarget') | ~'part$uof'(n1,rho1), inference(resolution, [status(thm)], [d18,d1])).
% 8.00/18.75 cnf(d20, plain, n1 = sK9('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [c27,d19])).
% 8.00/18.75 cnf(d21, plain, n2 = sK9('some$uaction',X0,'some$utarget') | ~'Ts1'('some$uaction',X0,'some$utarget') | ~'part$uof'(n2,X0) | ~'no$uright'(n2), inference(resolution, [status(thm)], [c31,c13])).
% 8.00/18.75 cnf(d22, plain, n2 = sK9('some$uaction',X0,'some$utarget') | ~'Ts1'('some$uaction',X0,'some$utarget') | ~'part$uof'(n2,X0), inference(resolution, [status(thm)], [c25,d21])).
% 8.00/18.75 cnf(d23, plain, sK8('some$uaction',rho1,'some$utarget',l) = l | n2 = sK9('some$uaction',rho1,'some$utarget') | ~'part$uof'(n2,rho1), inference(resolution, [status(thm)], [d9,d22])).
% 8.00/18.75 cnf(d24, plain, sK8('some$uaction',rho1,'some$utarget',l) = l | n2 = sK9('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [c28,d23])).
% 8.00/18.75 cnf(d25, plain, l != l | 'Ts0'('some$uaction',rho1,'some$utarget') | ~permission(l) | ~'part$uof'(l,rho1) | ~cnt(l,'some$uaction','some$utarget') | n2 = sK9('some$uaction',rho1,'some$utarget'), inference(superposition, [status(thm)], [d24,c9])).
% 8.00/18.75 cnf(d26, plain, l != l | n2 = n1 | 'Ts0'('some$uaction',rho1,'some$utarget') | ~permission(l) | ~'part$uof'(l,rho1) | ~cnt(l,'some$uaction','some$utarget'), inference(demodulation, [status(thm)], [d25,d20])).
% 8.00/18.75 cnf(d27, plain, l != l | n2 = n1 | 'Ts0'('some$uaction',rho1,'some$utarget') | ~'part$uof'(l,rho1) | ~cnt(l,'some$uaction','some$utarget'), inference(resolution, [status(thm)], [c23,d26])).
% 8.00/18.75 cnf(d28, plain, l != l | n2 = n1 | 'Ts0'('some$uaction',rho1,'some$utarget') | ~cnt(l,'some$uaction','some$utarget'), inference(resolution, [status(thm)], [c26,d27])).
% 8.00/18.75 cnf(d29, plain, l != l | n2 = n1 | 'Ts0'('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [c29,d28])).
% 8.00/18.75 cnf(d30, plain, n2 = n1 | 'Ts0'('some$uaction',rho1,'some$utarget'), inference(equality_resolution, [status(thm)], [d29])).
% 8.00/18.75 cnf(d31, plain, n2 = n1 | ~'odrl$urel'(rho1) | 'Ts1'('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [d30,c0])).
% 8.00/18.75 cnf(d32, plain, n2 = n1 | 'Ts1'('some$uaction',rho1,'some$utarget'), inference(resolution, [status(thm)], [c22,d31])).
% 8.00/18.75 cnf(d33, plain, n2 = n1 | n2 = sK9('some$uaction',rho1,'some$utarget') | ~'part$uof'(n2,rho1), inference(resolution, [status(thm)], [d32,d22])).
% 8.00/18.75 cnf(d34, plain, n2 = n1 | n2 = n1 | ~'part$uof'(n2,rho1), inference(demodulation, [status(thm)], [d33,d20])).
% 8.00/18.75 cnf(d35, plain, n2 = n1 | n2 = n1, inference(resolution, [status(thm)], [c28,d34])).
% 8.00/18.75 cnf(d36, plain, n1 != n1, inference(demodulation, [status(thm)], [c34,d35])).
% 8.00/18.75 cnf(d37, plain, $false, inference(equality_resolution, [status(thm)], [d36])).
% 8.00/18.75 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------