%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SWV237+1 : TPTP v9.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n023.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 : Fri Jul 25 04:46:21 PM UTC 2025
% Result : Theorem 5.58s 1.07s
% Output : CNFRefutation 5.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 9
% Syntax : Number of formulae : 30 ( 24 unt; 0 def)
% Number of atoms : 48 ( 4 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 33 ( 15 ~; 12 |; 4 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 16 ( 3 sgn 8 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,plain,
p(enc(pp,a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(co1_negated,plain,
~ p(enc(pp,a)),
inference(negate_conjecture,[status(cth)],[co1]) ).
cnf(24,plain,
~ p(enc(pp,a)),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l0,plain,
~ p(enc(pp,a)),
inference(instantiation,[status(thm)],[24]) ).
fof(enc_dec_cancel,plain,
! [U,V] : enc(i(U),enc(U,V)) = V,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',enc_dec_cancel) ).
cnf(0,plain,
enc(i(X0),enc(X0,X1)) = X1,
inference(cnf,[status(esa)],[enc_dec_cancel]) ).
cnf(l5,plain,
enc(i(tc),enc(tc,a)) = a,
inference(instantiation,[status(thm)],[0]) ).
cnf(l6,plain,
enc(i(tmk),enc(tmk,pp)) = pp,
inference(instantiation,[status(thm)],[0]) ).
fof(encrypt_a_stored_comms_key,plain,
! [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) ).
cnf(8,plain,
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| p(enc(enc(i(tmk),X1),enc(i(tc),X0))) ),
inference(cnf,[status(esa)],[encrypt_a_stored_comms_key]) ).
cnf(l4,plain,
( ~ p(enc(tc,a))
| ~ p(enc(tmk,pp))
| ~ p(enc(w,t1))
| p(enc(enc(i(tmk),enc(tmk,pp)),enc(i(tc),enc(tc,a)))) ),
inference(instantiation,[status(thm)],[8]) ).
fof(intruder_knows_3,plain,
p(enc(w,t1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_3) ).
cnf(18,plain,
p(enc(w,t1)),
inference(cnf,[status(esa)],[intruder_knows_3]) ).
cnf(l31,plain,
p(enc(w,t1)),
inference(instantiation,[status(thm)],[18]) ).
fof(encrypt_clear_key_as_Tcomms_key,plain,
! [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) ).
cnf(9,plain,
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| p(enc(tc,X0)) ),
inference(cnf,[status(esa)],[encrypt_clear_key_as_Tcomms_key]) ).
cnf(l28,plain,
( ~ p(a)
| ~ p(enc(lp,t2))
| ~ p(kk)
| p(enc(tc,a)) ),
inference(instantiation,[status(thm)],[9]) ).
fof(intruder_knows_8,plain,
p(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_8) ).
cnf(23,plain,
p(a),
inference(cnf,[status(esa)],[intruder_knows_8]) ).
cnf(l29,plain,
p(a),
inference(instantiation,[status(thm)],[23]) ).
fof(intruder_knows_4,plain,
p(enc(lp,t2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_4) ).
cnf(19,plain,
p(enc(lp,t2)),
inference(cnf,[status(esa)],[intruder_knows_4]) ).
cnf(l30,plain,
p(enc(lp,t2)),
inference(instantiation,[status(thm)],[19]) ).
fof(intruder_knows_6,plain,
p(kk),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_6) ).
cnf(21,plain,
p(kk),
inference(cnf,[status(esa)],[intruder_knows_6]) ).
cnf(l35,plain,
p(kk),
inference(instantiation,[status(thm)],[21]) ).
fof(intruder_knows_1,plain,
p(enc(tmk,pp)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_1) ).
cnf(16,plain,
p(enc(tmk,pp)),
inference(cnf,[status(esa)],[intruder_knows_1]) ).
cnf(l24,plain,
p(enc(tmk,pp)),
inference(instantiation,[status(thm)],[16]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l5,l6,l4,l31,l28,l29,l30,l35,l24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV237+1 : TPTP v9.0.0. Released v3.2.0.
% 0.03/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jul 22 08:30:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 0.20/0.37 % launching worker at depth: 11
% 5.58/1.07 % SZS status Theorem for theBenchmark
% 5.58/1.07 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------