%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWV237+1 : TPTP v9.0.0. Released v3.2.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 : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 09:29:50 PM UTC 2025
% Result : Theorem 4.69s 2.07s
% Output : CNFRefutation 4.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 9
% Syntax : Number of formulae : 34 ( 22 unt; 0 typ; 0 def)
% Number of atoms : 59 ( 6 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 50 ( 25 ~; 19 |; 4 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 38 ( 38 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ p > enc > #nlpp > i > zcmk > wk > w > tmk > tc > t2 > t1 > pp > lp > kk > k > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(zcmk,type,
zcmk: $i ).
tff(enc,type,
enc: ( $i * $i ) > $i ).
tff(a,type,
a: $i ).
tff(i,type,
i: $i > $i ).
tff(pp,type,
pp: $i ).
tff(w,type,
w: $i ).
tff(k,type,
k: $i ).
tff(p,type,
p: $i > $o ).
tff(tmk,type,
tmk: $i ).
tff(t2,type,
t2: $i ).
tff(tc,type,
tc: $i ).
tff(kk,type,
kk: $i ).
tff(wk,type,
wk: $i ).
tff(t1,type,
t1: $i ).
tff(lp,type,
lp: $i ).
tff(f_144,axiom,
p(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_8) ).
tff(f_86,axiom,
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(tc,U)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',encrypt_clear_key_as_Tcomms_key) ).
tff(f_141,axiom,
p(enc(tc,k)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_5) ).
tff(f_137,axiom,
p(enc(tmk,pp)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_1) ).
tff(f_29,axiom,
! [U,V] : ( enc(i(U),enc(U,V)) = V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',enc_dec_cancel) ).
tff(f_33,axiom,
! [U] : ( i(i(U)) = U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',double_inverse_cancel) ).
tff(f_31,axiom,
! [U,V] : ( enc(U,enc(i(U),V)) = V ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dec_enc_cancel) ).
tff(f_77,axiom,
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(enc(i(tmk),V),enc(i(tc),U))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',encrypt_a_stored_comms_key) ).
tff(f_147,negated_conjecture,
~ p(enc(pp,a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
tff(c_48,plain,
p(a),
inference(cnfTransformation,[status(thm)],[f_144]) ).
tff(c_20,plain,
! [U_22,W_24,V_23] :
( p(enc(tc,U_22))
| ~ p(W_24)
| ~ p(V_23)
| ~ p(U_22) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_137,plain,
! [W_24] : ~ p(W_24),
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_42,plain,
p(enc(tc,k)),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_148,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_137,c_42]) ).
tff(c_149,plain,
! [V_23,U_22] :
( ~ p(V_23)
| p(enc(tc,U_22))
| ~ p(U_22) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_150,plain,
! [V_23] : ~ p(V_23),
inference(splitLeft,[status(thm)],[c_149]) ).
tff(c_161,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_150,c_42]) ).
tff(c_162,plain,
! [U_22] :
( p(enc(tc,U_22))
| ~ p(U_22) ),
inference(splitRight,[status(thm)],[c_149]) ).
tff(c_34,plain,
p(enc(tmk,pp)),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_2,plain,
! [U_1,V_2] : ( enc(i(U_1),enc(U_1,V_2)) = V_2 ),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_6,plain,
! [U_5] : ( i(i(U_5)) = U_5 ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_4,plain,
! [U_3,V_4] : ( enc(U_3,enc(i(U_3),V_4)) = V_4 ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_18,plain,
! [V_20,U_19,W_21] :
( p(enc(enc(i(tmk),V_20),enc(i(tc),U_19)))
| ~ p(W_21)
| ~ p(V_20)
| ~ p(U_19) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_702,plain,
! [W_21] : ~ p(W_21),
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_730,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_702,c_42]) ).
tff(c_855,plain,
! [V_83,U_84] :
( p(enc(enc(i(tmk),V_83),enc(i(tc),U_84)))
| ~ p(V_83)
| ~ p(U_84) ),
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_864,plain,
! [V_4,U_84] :
( p(enc(V_4,enc(i(tc),U_84)))
| ~ p(enc(i(i(tmk)),V_4))
| ~ p(U_84) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_855]) ).
tff(c_1408,plain,
! [V_102,U_103] :
( p(enc(V_102,enc(i(tc),U_103)))
| ~ p(enc(tmk,V_102))
| ~ p(U_103) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_864]) ).
tff(c_1526,plain,
! [V_107,V_108] :
( p(enc(V_107,V_108))
| ~ p(enc(tmk,V_107))
| ~ p(enc(tc,V_108)) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_1408]) ).
tff(c_1548,plain,
! [V_109] :
( p(enc(pp,V_109))
| ~ p(enc(tc,V_109)) ),
inference(resolution,[status(thm)],[c_34,c_1526]) ).
tff(c_1590,plain,
! [U_110] :
( p(enc(pp,U_110))
| ~ p(U_110) ),
inference(resolution,[status(thm)],[c_162,c_1548]) ).
tff(c_50,plain,
~ p(enc(pp,a)),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_1603,plain,
~ p(a),
inference(resolution,[status(thm)],[c_1590,c_50]) ).
tff(c_1615,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_48,c_1603]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : SWV237+1 : TPTP v9.0.0. Released v3.2.0.
% 0.00/0.11 % 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.32 % Computer : n010.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Wed Apr 9 02:52:33 EDT 2025
% 0.11/0.32 % CPUTime :
% 4.69/2.07 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.69/2.08
% 4.69/2.08 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------