%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWW970+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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 : Thu Sep 24 09:08:50 AM UTC 2026
% Result : Theorem 21.06s 21.37s
% Output : Proof 21.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 6
% Syntax : Number of formulae : 36 ( 20 unt; 0 def)
% Number of atoms : 58 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 44 ( 22 ~; 18 |; 1 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 29 ( 5 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax79,axiom,
! [VAR_X_67,VAR_Y_68] : pred_eq_bitstring_bitstring(VAR_X_67,VAR_Y_68),
file('theBenchmark.p',ax79) ).
fof(ax93,axiom,
! [VAR_V_112] :
( pred_attacker(tuple_client_B_out_2(VAR_V_112))
=> pred_attacker(VAR_V_112) ),
file('theBenchmark.p',ax93) ).
fof(ax94,axiom,
! [VAR_V_115] :
( pred_attacker(VAR_V_115)
=> pred_attacker(tuple_client_B_in_1(VAR_V_115)) ),
file('theBenchmark.p',ax94) ).
fof(ax134,axiom,
! [VAR_V_280X30] : pred_attacker(name_new0x2Dname(VAR_V_280X30)),
file('theBenchmark.p',ax134) ).
fof(ax135,axiom,
! [VAR_ENC_A_KAB_T_330X30] :
( ( pred_attacker(tuple_client_B_in_1(VAR_ENC_A_KAB_T_330X30))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_3_get_0x30(constr_cbc_dec_3(VAR_ENC_A_KAB_T_330X30,name_Kbs))) )
=> pred_attacker(tuple_client_B_out_2(name_objective)) ),
file('theBenchmark.p',ax135) ).
fof(co0,conjecture,
pred_attacker(name_objective),
file('theBenchmark.p',co0) ).
fof(f_80_1,plain,
! [VAR_X_67,VAR_Y_68] : pred_eq_bitstring_bitstring(VAR_X_67,VAR_Y_68),
inference(fof_nnf,[status(thm)],[ax79]) ).
fof(f_80_2,plain,
! [U_50,U_49] : pred_eq_bitstring_bitstring(U_50,U_49),
inference(variable_rename,[status(thm)],[f_80_1]) ).
cnf(f_80_3,plain,
pred_eq_bitstring_bitstring(U_50,U_49),
inference(clausify,[status(thm)],[f_80_2]) ).
fof(f_94_1,plain,
! [VAR_V_112] :
( pred_attacker(VAR_V_112)
| ~ pred_attacker(tuple_client_B_out_2(VAR_V_112)) ),
inference(fof_nnf,[status(thm)],[ax93]) ).
fof(f_94_2,plain,
! [U_65] :
( pred_attacker(U_65)
| ~ pred_attacker(tuple_client_B_out_2(U_65)) ),
inference(variable_rename,[status(thm)],[f_94_1]) ).
cnf(f_94_3,plain,
( pred_attacker(U_65)
| ~ pred_attacker(tuple_client_B_out_2(U_65)) ),
inference(clausify,[status(thm)],[f_94_2]) ).
fof(f_95_1,plain,
! [VAR_V_115] :
( pred_attacker(tuple_client_B_in_1(VAR_V_115))
| ~ pred_attacker(VAR_V_115) ),
inference(fof_nnf,[status(thm)],[ax94]) ).
fof(f_95_2,plain,
! [U_66] :
( pred_attacker(tuple_client_B_in_1(U_66))
| ~ pred_attacker(U_66) ),
inference(variable_rename,[status(thm)],[f_95_1]) ).
cnf(f_95_3,plain,
( pred_attacker(tuple_client_B_in_1(U_66))
| ~ pred_attacker(U_66) ),
inference(clausify,[status(thm)],[f_95_2]) ).
fof(f_135_1,plain,
! [VAR_V_280X30] : pred_attacker(name_new0x2Dname(VAR_V_280X30)),
inference(fof_nnf,[status(thm)],[ax134]) ).
fof(f_135_2,plain,
! [U_139] : pred_attacker(name_new0x2Dname(U_139)),
inference(variable_rename,[status(thm)],[f_135_1]) ).
cnf(f_135_3,plain,
pred_attacker(name_new0x2Dname(U_139)),
inference(clausify,[status(thm)],[f_135_2]) ).
fof(f_136_1,plain,
! [VAR_ENC_A_KAB_T_330X30] :
( pred_attacker(tuple_client_B_out_2(name_objective))
| ~ pred_attacker(tuple_client_B_in_1(VAR_ENC_A_KAB_T_330X30))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_3_get_0x30(constr_cbc_dec_3(VAR_ENC_A_KAB_T_330X30,name_Kbs))) ),
inference(fof_nnf,[status(thm)],[ax135]) ).
fof(f_136_2,plain,
! [U_140] :
( pred_attacker(tuple_client_B_out_2(name_objective))
| ~ pred_attacker(tuple_client_B_in_1(U_140))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_3_get_0x30(constr_cbc_dec_3(U_140,name_Kbs))) ),
inference(variable_rename,[status(thm)],[f_136_1]) ).
fof(f_136_3,plain,
( ! [U_140] :
( ~ pred_attacker(tuple_client_B_in_1(U_140))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_3_get_0x30(constr_cbc_dec_3(U_140,name_Kbs))) )
| pred_attacker(tuple_client_B_out_2(name_objective)) ),
inference(miniscope,[status(thm)],[f_136_2]) ).
cnf(f_136_4,plain,
( ~ pred_attacker(tuple_client_B_in_1(U_140))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_3_get_0x30(constr_cbc_dec_3(U_140,name_Kbs)))
| pred_attacker(tuple_client_B_out_2(name_objective)) ),
inference(clausify,[status(thm)],[f_136_3]) ).
fof(f_139_1,negated_conjecture,
~ pred_attacker(name_objective),
inference(negate,[status(cth)],[co0]) ).
fof(f_139_2,negated_conjecture,
~ pred_attacker(name_objective),
inference(definitional_conversion,[status(esa)],[f_139_1]) ).
cnf(f_139_3,negated_conjecture,
~ pred_attacker(name_objective),
inference(clausify,[status(thm)],[f_139_2]) ).
cnf(t1,plain,
~ pred_attacker(name_objective),
inference(start,[status(thm),parent(0:0)],[f_139_3]) ).
cnf(t2,plain,
( ~ pred_attacker(tuple_client_B_out_2(name_objective))
| pred_attacker(name_objective) ),
inference(extension,[status(thm),parent(t1:1)],[f_94_3]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_3_get_0x30(constr_cbc_dec_3(name_new0x2Dname(U_1451),name_Kbs)))
| ~ pred_attacker(tuple_client_B_in_1(name_new0x2Dname(U_1451)))
| pred_attacker(tuple_client_B_out_2(name_objective)) ),
inference(extension,[status(thm),parent(t2:2)],[f_136_4]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ pred_attacker(name_new0x2Dname(U_1451))
| pred_attacker(tuple_client_B_in_1(name_new0x2Dname(U_1451))) ),
inference(extension,[status(thm),parent(t4:2)],[f_95_3]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
pred_attacker(name_new0x2Dname(U_1451)),
inference(extension,[status(thm),parent(t6:2)],[f_135_3]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
pred_eq_bitstring_bitstring(name_A,constr_tuple_3_get_0x30(constr_cbc_dec_3(name_new0x2Dname(U_1451),name_Kbs))),
inference(extension,[status(thm),parent(t4:3)],[f_80_3]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t4:3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW970+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n002.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 20 06:02:34 UTC 2026
% 0.08/0.34 % CPUTime :
% 21.06/21.37 % SZS status Theorem for theBenchmark
% 21.06/21.37 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------