%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n027.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 : Tue Sep 8 06:03:08 AM UTC 2026
% Result : Theorem 3.88s 2.48s
% Output : CNFRefutation 4.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 53 ( 14 unt; 0 typ; 0 def)
% Number of atoms : 212 ( 0 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 302 ( 143 ~; 145 |; 13 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-3 aty)
% Number of variables : 73 ( 67 !; 6 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ cnt > bearer > aee > activates > act > target > proh > permission > agent > action > #nlpp > theater_ds > portal > modify_act > ensemble > #skF_1 > #skF_2 > #skF_3
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(aee,type,
aee: ( $i * $i ) > $o ).
tff('#skF_1',type,
'#skF_1': ( $i * $i * $i ) > $i ).
tff(bearer,type,
bearer: ( $i * $i ) > $o ).
tff(ensemble,type,
ensemble: $i ).
tff(proh,type,
proh: $i > $o ).
tff(theater_ds,type,
theater_ds: $i ).
tff(cnt,type,
cnt: ( $i * $i * $i ) > $o ).
tff(modify_act,type,
modify_act: $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i ) > $i ).
tff(agent,type,
agent: $i > $o ).
tff(portal,type,
portal: $i ).
tff(target,type,
target: $i > $o ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i ) > $i ).
tff(activates,type,
activates: ( $i * $i ) > $o ).
tff(act,type,
act: ( $i * $i ) > $o ).
tff(action,type,
action: $i > $o ).
tff(permission,type,
permission: $i > $o ).
tff(f_31,axiom,
agent(portal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',agent_portal) ).
tff(f_33,axiom,
action(modify_act),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',action_modify) ).
tff(f_34,axiom,
target(theater_ds),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',target_theater) ).
tff(f_66,axiom,
! [X,A,T] :
( ( agent(X)
& action(A)
& target(T)
& ~ ? [F,E] :
( proh(F)
& aee(F,X)
& act(F,A)
& activates(E,F) ) )
=> ? [L] :
( permission(L)
& bearer(L,X)
& cnt(L,A,T) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',open_world_closure) ).
tff(f_43,axiom,
~ ? [F,E] :
( proh(F)
& aee(F,portal)
& act(F,modify_act)
& activates(E,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_proh_modify) ).
tff(f_73,negated_conjecture,
~ ? [L] :
( permission(L)
& bearer(L,portal)
& cnt(L,modify_act,theater_ds) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture) ).
tff(c_2,plain,
agent(portal),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_6,plain,
action(modify_act),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_8,plain,
target(theater_ds),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_34,plain,
! [X_3,A_4,T_5] :
( proh('#skF_1'(X_3,A_4,T_5))
| permission('#skF_3'(X_3,A_4,T_5))
| ~ target(T_5)
| ~ action(A_4)
| ~ agent(X_3) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_30,plain,
! [X_3,A_4,T_5] :
( act('#skF_1'(X_3,A_4,T_5),A_4)
| permission('#skF_3'(X_3,A_4,T_5))
| ~ target(T_5)
| ~ action(A_4)
| ~ agent(X_3) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_32,plain,
! [X_3,A_4,T_5] :
( aee('#skF_1'(X_3,A_4,T_5),X_3)
| permission('#skF_3'(X_3,A_4,T_5))
| ~ target(T_5)
| ~ action(A_4)
| ~ agent(X_3) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_133,plain,
! [X_43,A_44,T_45] :
( activates('#skF_2'(X_43,A_44,T_45),'#skF_1'(X_43,A_44,T_45))
| permission('#skF_3'(X_43,A_44,T_45))
| ~ target(T_45)
| ~ action(A_44)
| ~ agent(X_43) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_10,plain,
! [E_2,F_1] :
( ~ activates(E_2,F_1)
| ~ act(F_1,modify_act)
| ~ aee(F_1,portal)
| ~ proh(F_1) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_145,plain,
! [X_52,A_53,T_54] :
( ~ act('#skF_1'(X_52,A_53,T_54),modify_act)
| ~ aee('#skF_1'(X_52,A_53,T_54),portal)
| ~ proh('#skF_1'(X_52,A_53,T_54))
| permission('#skF_3'(X_52,A_53,T_54))
| ~ target(T_54)
| ~ action(A_53)
| ~ agent(X_52) ),
inference(resolution,[status(thm)],[c_133,c_10]) ).
tff(c_151,plain,
! [A_4,T_5] :
( ~ act('#skF_1'(portal,A_4,T_5),modify_act)
| ~ proh('#skF_1'(portal,A_4,T_5))
| permission('#skF_3'(portal,A_4,T_5))
| ~ target(T_5)
| ~ action(A_4)
| ~ agent(portal) ),
inference(resolution,[status(thm)],[c_32,c_145]) ).
tff(c_155,plain,
! [A_55,T_56] :
( ~ act('#skF_1'(portal,A_55,T_56),modify_act)
| ~ proh('#skF_1'(portal,A_55,T_56))
| permission('#skF_3'(portal,A_55,T_56))
| ~ target(T_56)
| ~ action(A_55) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_151]) ).
tff(c_161,plain,
! [T_5] :
( ~ proh('#skF_1'(portal,modify_act,T_5))
| permission('#skF_3'(portal,modify_act,T_5))
| ~ target(T_5)
| ~ action(modify_act)
| ~ agent(portal) ),
inference(resolution,[status(thm)],[c_30,c_155]) ).
tff(c_165,plain,
! [T_57] :
( ~ proh('#skF_1'(portal,modify_act,T_57))
| permission('#skF_3'(portal,modify_act,T_57))
| ~ target(T_57) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6,c_161]) ).
tff(c_169,plain,
! [T_5] :
( permission('#skF_3'(portal,modify_act,T_5))
| ~ target(T_5)
| ~ action(modify_act)
| ~ agent(portal) ),
inference(resolution,[status(thm)],[c_34,c_165]) ).
tff(c_173,plain,
! [T_58] :
( permission('#skF_3'(portal,modify_act,T_58))
| ~ target(T_58) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6,c_169]) ).
tff(c_26,plain,
! [X_3,A_4,T_5] :
( proh('#skF_1'(X_3,A_4,T_5))
| bearer('#skF_3'(X_3,A_4,T_5),X_3)
| ~ target(T_5)
| ~ action(A_4)
| ~ agent(X_3) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_44,plain,
! [X_28,A_29,T_30] :
( proh('#skF_1'(X_28,A_29,T_30))
| cnt('#skF_3'(X_28,A_29,T_30),A_29,T_30)
| ~ target(T_30)
| ~ action(A_29)
| ~ agent(X_28) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_36,plain,
! [L_9] :
( ~ cnt(L_9,modify_act,theater_ds)
| ~ bearer(L_9,portal)
| ~ permission(L_9) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_48,plain,
! [X_28] :
( ~ bearer('#skF_3'(X_28,modify_act,theater_ds),portal)
| ~ permission('#skF_3'(X_28,modify_act,theater_ds))
| proh('#skF_1'(X_28,modify_act,theater_ds))
| ~ target(theater_ds)
| ~ action(modify_act)
| ~ agent(X_28) ),
inference(resolution,[status(thm)],[c_44,c_36]) ).
tff(c_53,plain,
! [X_34] :
( ~ bearer('#skF_3'(X_34,modify_act,theater_ds),portal)
| ~ permission('#skF_3'(X_34,modify_act,theater_ds))
| proh('#skF_1'(X_34,modify_act,theater_ds))
| ~ agent(X_34) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_8,c_48]) ).
tff(c_65,plain,
( ~ permission('#skF_3'(portal,modify_act,theater_ds))
| proh('#skF_1'(portal,modify_act,theater_ds))
| ~ target(theater_ds)
| ~ action(modify_act)
| ~ agent(portal) ),
inference(resolution,[status(thm)],[c_26,c_53]) ).
tff(c_74,plain,
( ~ permission('#skF_3'(portal,modify_act,theater_ds))
| proh('#skF_1'(portal,modify_act,theater_ds)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6,c_8,c_65]) ).
tff(c_75,plain,
~ permission('#skF_3'(portal,modify_act,theater_ds)),
inference(splitLeft,[status(thm)],[c_74]) ).
tff(c_176,plain,
~ target(theater_ds),
inference(resolution,[status(thm)],[c_173,c_75]) ).
tff(c_180,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_176]) ).
tff(c_181,plain,
proh('#skF_1'(portal,modify_act,theater_ds)),
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_182,plain,
permission('#skF_3'(portal,modify_act,theater_ds)),
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_24,plain,
! [X_3,A_4,T_5] :
( aee('#skF_1'(X_3,A_4,T_5),X_3)
| bearer('#skF_3'(X_3,A_4,T_5),X_3)
| ~ target(T_5)
| ~ action(A_4)
| ~ agent(X_3) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_223,plain,
! [X_63,A_64,T_65] :
( aee('#skF_1'(X_63,A_64,T_65),X_63)
| cnt('#skF_3'(X_63,A_64,T_65),A_64,T_65)
| ~ target(T_65)
| ~ action(A_64)
| ~ agent(X_63) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_227,plain,
! [X_63] :
( ~ bearer('#skF_3'(X_63,modify_act,theater_ds),portal)
| ~ permission('#skF_3'(X_63,modify_act,theater_ds))
| aee('#skF_1'(X_63,modify_act,theater_ds),X_63)
| ~ target(theater_ds)
| ~ action(modify_act)
| ~ agent(X_63) ),
inference(resolution,[status(thm)],[c_223,c_36]) ).
tff(c_231,plain,
! [X_66] :
( ~ bearer('#skF_3'(X_66,modify_act,theater_ds),portal)
| ~ permission('#skF_3'(X_66,modify_act,theater_ds))
| aee('#skF_1'(X_66,modify_act,theater_ds),X_66)
| ~ agent(X_66) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_8,c_227]) ).
tff(c_234,plain,
( ~ permission('#skF_3'(portal,modify_act,theater_ds))
| aee('#skF_1'(portal,modify_act,theater_ds),portal)
| ~ target(theater_ds)
| ~ action(modify_act)
| ~ agent(portal) ),
inference(resolution,[status(thm)],[c_24,c_231]) ).
tff(c_243,plain,
aee('#skF_1'(portal,modify_act,theater_ds),portal),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6,c_8,c_182,c_234]) ).
tff(c_22,plain,
! [X_3,A_4,T_5] :
( act('#skF_1'(X_3,A_4,T_5),A_4)
| bearer('#skF_3'(X_3,A_4,T_5),X_3)
| ~ target(T_5)
| ~ action(A_4)
| ~ agent(X_3) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_189,plain,
! [X_59,A_60,T_61] :
( act('#skF_1'(X_59,A_60,T_61),A_60)
| cnt('#skF_3'(X_59,A_60,T_61),A_60,T_61)
| ~ target(T_61)
| ~ action(A_60)
| ~ agent(X_59) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_193,plain,
! [X_59] :
( ~ bearer('#skF_3'(X_59,modify_act,theater_ds),portal)
| ~ permission('#skF_3'(X_59,modify_act,theater_ds))
| act('#skF_1'(X_59,modify_act,theater_ds),modify_act)
| ~ target(theater_ds)
| ~ action(modify_act)
| ~ agent(X_59) ),
inference(resolution,[status(thm)],[c_189,c_36]) ).
tff(c_200,plain,
! [X_62] :
( ~ bearer('#skF_3'(X_62,modify_act,theater_ds),portal)
| ~ permission('#skF_3'(X_62,modify_act,theater_ds))
| act('#skF_1'(X_62,modify_act,theater_ds),modify_act)
| ~ agent(X_62) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_8,c_193]) ).
tff(c_208,plain,
( ~ permission('#skF_3'(portal,modify_act,theater_ds))
| act('#skF_1'(portal,modify_act,theater_ds),modify_act)
| ~ target(theater_ds)
| ~ action(modify_act)
| ~ agent(portal) ),
inference(resolution,[status(thm)],[c_22,c_200]) ).
tff(c_218,plain,
act('#skF_1'(portal,modify_act,theater_ds),modify_act),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6,c_8,c_182,c_208]) ).
tff(c_254,plain,
! [X_70,A_71,T_72] :
( activates('#skF_2'(X_70,A_71,T_72),'#skF_1'(X_70,A_71,T_72))
| bearer('#skF_3'(X_70,A_71,T_72),X_70)
| ~ target(T_72)
| ~ action(A_71)
| ~ agent(X_70) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_257,plain,
! [X_70,A_71,T_72] :
( ~ act('#skF_1'(X_70,A_71,T_72),modify_act)
| ~ aee('#skF_1'(X_70,A_71,T_72),portal)
| ~ proh('#skF_1'(X_70,A_71,T_72))
| bearer('#skF_3'(X_70,A_71,T_72),X_70)
| ~ target(T_72)
| ~ action(A_71)
| ~ agent(X_70) ),
inference(resolution,[status(thm)],[c_254,c_10]) ).
tff(c_258,plain,
! [X_73,A_74,T_75] :
( activates('#skF_2'(X_73,A_74,T_75),'#skF_1'(X_73,A_74,T_75))
| cnt('#skF_3'(X_73,A_74,T_75),A_74,T_75)
| ~ target(T_75)
| ~ action(A_74)
| ~ agent(X_73) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_330,plain,
! [X_86,A_87,T_88] :
( ~ act('#skF_1'(X_86,A_87,T_88),modify_act)
| ~ aee('#skF_1'(X_86,A_87,T_88),portal)
| ~ proh('#skF_1'(X_86,A_87,T_88))
| cnt('#skF_3'(X_86,A_87,T_88),A_87,T_88)
| ~ target(T_88)
| ~ action(A_87)
| ~ agent(X_86) ),
inference(resolution,[status(thm)],[c_258,c_10]) ).
tff(c_334,plain,
! [X_86] :
( ~ bearer('#skF_3'(X_86,modify_act,theater_ds),portal)
| ~ permission('#skF_3'(X_86,modify_act,theater_ds))
| ~ act('#skF_1'(X_86,modify_act,theater_ds),modify_act)
| ~ aee('#skF_1'(X_86,modify_act,theater_ds),portal)
| ~ proh('#skF_1'(X_86,modify_act,theater_ds))
| ~ target(theater_ds)
| ~ action(modify_act)
| ~ agent(X_86) ),
inference(resolution,[status(thm)],[c_330,c_36]) ).
tff(c_338,plain,
! [X_89] :
( ~ bearer('#skF_3'(X_89,modify_act,theater_ds),portal)
| ~ permission('#skF_3'(X_89,modify_act,theater_ds))
| ~ act('#skF_1'(X_89,modify_act,theater_ds),modify_act)
| ~ aee('#skF_1'(X_89,modify_act,theater_ds),portal)
| ~ proh('#skF_1'(X_89,modify_act,theater_ds))
| ~ agent(X_89) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_8,c_334]) ).
tff(c_342,plain,
( ~ permission('#skF_3'(portal,modify_act,theater_ds))
| ~ act('#skF_1'(portal,modify_act,theater_ds),modify_act)
| ~ aee('#skF_1'(portal,modify_act,theater_ds),portal)
| ~ proh('#skF_1'(portal,modify_act,theater_ds))
| ~ target(theater_ds)
| ~ action(modify_act)
| ~ agent(portal) ),
inference(resolution,[status(thm)],[c_257,c_338]) ).
tff(c_358,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6,c_8,c_181,c_243,c_218,c_182,c_342]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.11/0.36 % Computer : n027.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 7 14:09:00 UTC 2026
% 0.11/0.37 % CPUTime :
% 3.88/2.48 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.88/2.49
% 3.88/2.49 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------