%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT117+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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 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 : Tue Sep 8 06:03:09 AM UTC 2026
% Result : Theorem 3.73s 2.40s
% Output : CNFRefutation 3.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 9
% Syntax : Number of formulae : 32 ( 16 unt; 0 typ; 0 def)
% Number of atoms : 140 ( 0 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 208 ( 100 ~; 89 |; 18 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 7 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 : 19 ( 18 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-6 aty)
% Number of variables : 65 ( 60 !; 5 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ founds_imm > cnt > tgt > part_of > bearer > aer > aee > activates > act > target > strong > rule > perm > immunity > event > disability > agent > action > #nlpp > read > p1 > museum_api > museen > e1 > bibliothek > #skF_2 > #skF_1 > #skF_3
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(aee,type,
aee: ( $i * $i ) > $o ).
tff(e1,type,
e1: $i ).
tff(bearer,type,
bearer: ( $i * $i ) > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(museen,type,
museen: $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(founds_imm,type,
founds_imm: ( $i * $i * $i ) > $o ).
tff(rule,type,
rule: $i > $o ).
tff(p1,type,
p1: $i ).
tff(read,type,
read: $i ).
tff(aer,type,
aer: ( $i * $i ) > $o ).
tff(bibliothek,type,
bibliothek: $i ).
tff(part_of,type,
part_of: ( $i * $i ) > $o ).
tff(cnt,type,
cnt: ( $i * $i * $i ) > $o ).
tff(perm,type,
perm: $i > $o ).
tff(strong,type,
strong: $i > $o ).
tff(museum_api,type,
museum_api: $i ).
tff(agent,type,
agent: $i > $o ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(disability,type,
disability: $i > $o ).
tff(event,type,
event: $i > $o ).
tff(target,type,
target: $i > $o ).
tff(activates,type,
activates: ( $i * $i ) > $o ).
tff(tgt,type,
tgt: ( $i * $i ) > $o ).
tff(act,type,
act: ( $i * $i ) > $o ).
tff(action,type,
action: $i > $o ).
tff(immunity,type,
immunity: $i > $o ).
tff(f_68,axiom,
perm(p1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',perm_p1) ).
tff(f_69,axiom,
strong(p1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',strong_p1) ).
tff(f_71,axiom,
aer(p1,museen),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aer_p1) ).
tff(f_72,axiom,
act(p1,read),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',act_p1) ).
tff(f_73,axiom,
tgt(p1,museum_api),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tgt_p1) ).
tff(f_74,axiom,
activates(e1,p1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',act_e1_p1) ).
tff(f_60,axiom,
! [P,X,Y,A,T,E] :
( ( perm(P)
& strong(P)
& aee(P,X)
& aer(P,Y)
& act(P,A)
& tgt(P,T)
& activates(E,P) )
=> ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& immunity(Im)
& bearer(Im,X)
& cnt(Im,A,T)
& part_of(Im,RhoI)
& disability(Db)
& bearer(Db,Y)
& cnt(Db,A,T)
& part_of(Db,RhoI) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_perm_relator_strong) ).
tff(f_85,negated_conjecture,
~ ? [RhoI,Db] :
( founds_imm(e1,RhoI,p1)
& disability(Db)
& bearer(Db,museen)
& cnt(Db,read,museum_api)
& part_of(Db,RhoI) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture) ).
tff(f_70,axiom,
aee(p1,bibliothek),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aee_p1) ).
tff(c_32,plain,
perm(p1),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_34,plain,
strong(p1),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_38,plain,
aer(p1,museen),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_40,plain,
act(p1,read),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_42,plain,
tgt(p1,museum_api),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_44,plain,
activates(e1,p1),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_8,plain,
! [Y_3,A_4,P_1,X_2,E_6,T_5] :
( disability('#skF_3'(P_1,X_2,Y_3,E_6,T_5,A_4))
| ~ activates(E_6,P_1)
| ~ tgt(P_1,T_5)
| ~ act(P_1,A_4)
| ~ aer(P_1,Y_3)
| ~ aee(P_1,X_2)
| ~ strong(P_1)
| ~ perm(P_1) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_6,plain,
! [Y_3,A_4,P_1,X_2,E_6,T_5] :
( bearer('#skF_3'(P_1,X_2,Y_3,E_6,T_5,A_4),Y_3)
| ~ activates(E_6,P_1)
| ~ tgt(P_1,T_5)
| ~ act(P_1,A_4)
| ~ aer(P_1,Y_3)
| ~ aee(P_1,X_2)
| ~ strong(P_1)
| ~ perm(P_1) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_4,plain,
! [Y_3,A_4,P_1,X_2,E_6,T_5] :
( cnt('#skF_3'(P_1,X_2,Y_3,E_6,T_5,A_4),A_4,T_5)
| ~ activates(E_6,P_1)
| ~ tgt(P_1,T_5)
| ~ act(P_1,A_4)
| ~ aer(P_1,Y_3)
| ~ aee(P_1,X_2)
| ~ strong(P_1)
| ~ perm(P_1) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_18,plain,
! [Y_3,A_4,P_1,X_2,E_6,T_5] :
( founds_imm(E_6,'#skF_1'(P_1,X_2,Y_3,E_6,T_5,A_4),P_1)
| ~ activates(E_6,P_1)
| ~ tgt(P_1,T_5)
| ~ act(P_1,A_4)
| ~ aer(P_1,Y_3)
| ~ aee(P_1,X_2)
| ~ strong(P_1)
| ~ perm(P_1) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_55,plain,
! [Y_58,A_61,E_59,T_60,X_57,P_56] :
( part_of('#skF_3'(P_56,X_57,Y_58,E_59,T_60,A_61),'#skF_1'(P_56,X_57,Y_58,E_59,T_60,A_61))
| ~ activates(E_59,P_56)
| ~ tgt(P_56,T_60)
| ~ act(P_56,A_61)
| ~ aer(P_56,Y_58)
| ~ aee(P_56,X_57)
| ~ strong(P_56)
| ~ perm(P_56) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_46,plain,
! [Db_11,RhoI_10] :
( ~ part_of(Db_11,RhoI_10)
| ~ cnt(Db_11,read,museum_api)
| ~ bearer(Db_11,museen)
| ~ disability(Db_11)
| ~ founds_imm(e1,RhoI_10,p1) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_63,plain,
! [Y_71,E_73,A_72,P_70,T_68,X_69] :
( ~ cnt('#skF_3'(P_70,X_69,Y_71,E_73,T_68,A_72),read,museum_api)
| ~ bearer('#skF_3'(P_70,X_69,Y_71,E_73,T_68,A_72),museen)
| ~ disability('#skF_3'(P_70,X_69,Y_71,E_73,T_68,A_72))
| ~ founds_imm(e1,'#skF_1'(P_70,X_69,Y_71,E_73,T_68,A_72),p1)
| ~ activates(E_73,P_70)
| ~ tgt(P_70,T_68)
| ~ act(P_70,A_72)
| ~ aer(P_70,Y_71)
| ~ aee(P_70,X_69)
| ~ strong(P_70)
| ~ perm(P_70) ),
inference(resolution,[status(thm)],[c_55,c_46]) ).
tff(c_67,plain,
! [X_2,Y_3,T_5,A_4] :
( ~ cnt('#skF_3'(p1,X_2,Y_3,e1,T_5,A_4),read,museum_api)
| ~ bearer('#skF_3'(p1,X_2,Y_3,e1,T_5,A_4),museen)
| ~ disability('#skF_3'(p1,X_2,Y_3,e1,T_5,A_4))
| ~ activates(e1,p1)
| ~ tgt(p1,T_5)
| ~ act(p1,A_4)
| ~ aer(p1,Y_3)
| ~ aee(p1,X_2)
| ~ strong(p1)
| ~ perm(p1) ),
inference(resolution,[status(thm)],[c_18,c_63]) ).
tff(c_71,plain,
! [X_74,Y_75,T_76,A_77] :
( ~ cnt('#skF_3'(p1,X_74,Y_75,e1,T_76,A_77),read,museum_api)
| ~ bearer('#skF_3'(p1,X_74,Y_75,e1,T_76,A_77),museen)
| ~ disability('#skF_3'(p1,X_74,Y_75,e1,T_76,A_77))
| ~ tgt(p1,T_76)
| ~ act(p1,A_77)
| ~ aer(p1,Y_75)
| ~ aee(p1,X_74) ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_34,c_44,c_67]) ).
tff(c_75,plain,
! [X_2,Y_3] :
( ~ bearer('#skF_3'(p1,X_2,Y_3,e1,museum_api,read),museen)
| ~ disability('#skF_3'(p1,X_2,Y_3,e1,museum_api,read))
| ~ activates(e1,p1)
| ~ tgt(p1,museum_api)
| ~ act(p1,read)
| ~ aer(p1,Y_3)
| ~ aee(p1,X_2)
| ~ strong(p1)
| ~ perm(p1) ),
inference(resolution,[status(thm)],[c_4,c_71]) ).
tff(c_87,plain,
! [X_84,Y_85] :
( ~ bearer('#skF_3'(p1,X_84,Y_85,e1,museum_api,read),museen)
| ~ disability('#skF_3'(p1,X_84,Y_85,e1,museum_api,read))
| ~ aer(p1,Y_85)
| ~ aee(p1,X_84) ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_34,c_40,c_42,c_44,c_75]) ).
tff(c_91,plain,
! [X_2] :
( ~ disability('#skF_3'(p1,X_2,museen,e1,museum_api,read))
| ~ activates(e1,p1)
| ~ tgt(p1,museum_api)
| ~ act(p1,read)
| ~ aer(p1,museen)
| ~ aee(p1,X_2)
| ~ strong(p1)
| ~ perm(p1) ),
inference(resolution,[status(thm)],[c_6,c_87]) ).
tff(c_95,plain,
! [X_86] :
( ~ disability('#skF_3'(p1,X_86,museen,e1,museum_api,read))
| ~ aee(p1,X_86) ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_34,c_38,c_40,c_42,c_44,c_91]) ).
tff(c_99,plain,
! [X_2] :
( ~ activates(e1,p1)
| ~ tgt(p1,museum_api)
| ~ act(p1,read)
| ~ aer(p1,museen)
| ~ aee(p1,X_2)
| ~ strong(p1)
| ~ perm(p1) ),
inference(resolution,[status(thm)],[c_8,c_95]) ).
tff(c_102,plain,
! [X_2] : ~ aee(p1,X_2),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_34,c_38,c_40,c_42,c_44,c_99]) ).
tff(c_36,plain,
aee(p1,bibliothek),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_104,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_102,c_36]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT117+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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 14:12:12 UTC 2026
% 0.08/0.35 % CPUTime :
% 3.73/2.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.73/2.41
% 3.73/2.41 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------