%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWV236+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:03:02 AM UTC 2026
% Result : Theorem 24.34s 29.88s
% Output : Proof 25.36s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(xor_commutative,axiom,
! [X1,X2] : xor(X1,X2) = xor(X2,X1),
file('theBenchmark.p',xor_commutative) ).
fof(xor_associative,axiom,
! [X1,X2,X3] : xor(X1,xor(X2,X3)) = xor(xor(X1,X2),X3),
file('theBenchmark.p',xor_associative) ).
fof(encryption_decryption_cancellation,axiom,
! [X1,X2] : decrypt(X1,crypt(X1,X2)) = X2,
file('theBenchmark.p',encryption_decryption_cancellation) ).
fof(xor_rules_1,axiom,
! [X1] : xor(X1,id) = X1,
file('theBenchmark.p',xor_rules_1) ).
fof(xor_rules_2,axiom,
! [X1] : xor(X1,X1) = id,
file('theBenchmark.p',xor_rules_2) ).
fof(key_import,axiom,
! [Xkek1,Xtype1,Xk1,Xtype2,Xkek2] :
( ( p(crypt(xor(km,imp),Xkek2))
& p(Xtype2)
& p(crypt(xor(Xkek1,Xtype1),Xk1)) )
=> p(crypt(xor(km,Xtype2),decrypt(xor(Xkek2,Xtype2),crypt(xor(Xkek1,Xtype1),Xk1)))) ),
file('theBenchmark.p',key_import) ).
fof(key_export,axiom,
! [Xtype,Xk1,Xkek1] :
( ( p(crypt(xor(km,exp),Xkek1))
& p(Xtype)
& p(crypt(xor(km,Xtype),Xk1)) )
=> p(crypt(xor(Xkek1,Xtype),Xk1)) ),
file('theBenchmark.p',key_export) ).
fof(key_part_import___part_1,axiom,
! [Xk,Xtype] :
( ( p(Xtype)
& p(Xk) )
=> p(crypt(xor(km,xor(kp,Xtype)),Xk)) ),
file('theBenchmark.p',key_part_import___part_1) ).
fof(key_part_import___part_2,axiom,
! [Xk1,Xtype,Xk2] :
( ( p(Xtype)
& p(crypt(xor(km,xor(kp,Xtype)),Xk2))
& p(Xk1) )
=> p(crypt(xor(km,xor(Xtype,kp)),xor(Xk1,Xk2))) ),
file('theBenchmark.p',key_part_import___part_2) ).
fof(key_part_import___part_3,axiom,
! [Xk1,Xtype,Xk2] :
( ( p(Xtype)
& p(crypt(xor(km,xor(Xtype,kp)),Xk2))
& p(Xk1) )
=> p(crypt(xor(km,Xtype),xor(Xk2,Xk1))) ),
file('theBenchmark.p',key_part_import___part_3) ).
fof(encrypt_data,axiom,
! [X1,Xk1] :
( ( p(crypt(xor(km,data),Xk1))
& p(X1) )
=> p(crypt(Xk1,X1)) ),
file('theBenchmark.p',encrypt_data) ).
fof(decrypt_data,axiom,
! [X1,Xk1] :
( ( p(crypt(xor(km,data),Xk1))
& p(X1) )
=> p(decrypt(Xk1,X1)) ),
file('theBenchmark.p',decrypt_data) ).
fof(key_translate,axiom,
! [Xk,Xk1,Xtype2,Xkek1,Xkek2,Xtype] :
( ( p(crypt(xor(km,exp),Xkek2))
& p(crypt(xor(km,imp),Xkek1))
& p(Xtype2)
& p(crypt(Xk,Xk1)) )
=> p(crypt(xor(Xkek2,Xtype),decrypt(xor(Xtype2,Xkek1),crypt(Xk,Xk1)))) ),
file('theBenchmark.p',key_translate) ).
fof(combine_with_XOR,axiom,
! [X1,X2] :
( ( p(X2)
& p(X1) )
=> p(xor(X1,X2)) ),
file('theBenchmark.p',combine_with_XOR) ).
fof(decrypt_knowledge,axiom,
! [X1,X2] :
( ( p(X1)
& p(crypt(X1,X2)) )
=> p(X2) ),
file('theBenchmark.p',decrypt_knowledge) ).
fof(encrypt_knowledge,axiom,
! [X1,X2] :
( ( p(X1)
& p(X2) )
=> p(crypt(X1,X2)) ),
file('theBenchmark.p',encrypt_knowledge) ).
fof(data_cv_is_known_to_be_zero,axiom,
! [X1,X2] :
( p(crypt(xor(X1,data),X2))
=> p(crypt(X1,X2)) ),
file('theBenchmark.p',data_cv_is_known_to_be_zero) ).
fof(initial_knowledge_of_intruder_1,axiom,
p(kp),
file('theBenchmark.p',initial_knowledge_of_intruder_1) ).
fof(initial_knowledge_of_intruder_2,axiom,
p(imp),
file('theBenchmark.p',initial_knowledge_of_intruder_2) ).
fof(initial_knowledge_of_intruder_3,axiom,
p(data),
file('theBenchmark.p',initial_knowledge_of_intruder_3) ).
fof(initial_knowledge_of_intruder_4,axiom,
p(id),
file('theBenchmark.p',initial_knowledge_of_intruder_4) ).
fof(initial_knowledge_of_intruder_5,axiom,
p(pin),
file('theBenchmark.p',initial_knowledge_of_intruder_5) ).
fof(initial_knowledge_of_intruder_6,axiom,
p(crypt(xor(km,pin),pp)),
file('theBenchmark.p',initial_knowledge_of_intruder_6) ).
fof(initial_knowledge_of_intruder_7,axiom,
p(crypt(xor(km,exp),eurk)),
file('theBenchmark.p',initial_knowledge_of_intruder_7) ).
fof(initial_knowledge_of_intruder_8,axiom,
p(crypt(xor(km,data),eurk)),
file('theBenchmark.p',initial_knowledge_of_intruder_8) ).
fof(initial_knowledge_of_intruder_9,axiom,
p(exp),
file('theBenchmark.p',initial_knowledge_of_intruder_9) ).
fof(an_account_number,axiom,
p(a),
file('theBenchmark.p',an_account_number) ).
fof(find_known_exporter,conjecture,
? [X] :
( p(X)
& p(crypt(xor(km,exp),X)) ),
file('theBenchmark.p',find_known_exporter) ).
fof(f_1_1,plain,
! [X1,X2] : xor(X1,X2) = xor(X2,X1),
inference(fof_nnf,[status(thm)],[xor_commutative]) ).
fof(f_1_2,plain,
! [U_1,U_0] : xor(U_1,U_0) = xor(U_0,U_1),
inference(variable_rename,[status(thm)],[f_1_1]) ).
cnf(f_1_3,plain,
xor(U_1,U_0) = xor(U_0,U_1),
inference(clausify,[status(thm)],[f_1_2]) ).
fof(f_2_1,plain,
! [X1,X2,X3] : xor(X1,xor(X2,X3)) = xor(xor(X1,X2),X3),
inference(fof_nnf,[status(thm)],[xor_associative]) ).
fof(f_2_2,plain,
! [U_4,U_3,U_2] : xor(U_4,xor(U_3,U_2)) = xor(xor(U_4,U_3),U_2),
inference(variable_rename,[status(thm)],[f_2_1]) ).
cnf(f_2_3,plain,
xor(U_4,xor(U_3,U_2)) = xor(xor(U_4,U_3),U_2),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
! [X1,X2] : decrypt(X1,crypt(X1,X2)) = X2,
inference(fof_nnf,[status(thm)],[encryption_decryption_cancellation]) ).
fof(f_3_2,plain,
! [U_6,U_5] : decrypt(U_6,crypt(U_6,U_5)) = U_5,
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
decrypt(U_6,crypt(U_6,U_5)) = U_5,
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [X1] : xor(X1,id) = X1,
inference(fof_nnf,[status(thm)],[xor_rules_1]) ).
fof(f_4_2,plain,
! [U_7] : xor(U_7,id) = U_7,
inference(variable_rename,[status(thm)],[f_4_1]) ).
cnf(f_4_3,plain,
xor(U_7,id) = U_7,
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
! [X1] : xor(X1,X1) = id,
inference(fof_nnf,[status(thm)],[xor_rules_2]) ).
fof(f_5_2,plain,
! [U_8] : xor(U_8,U_8) = id,
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
xor(U_8,U_8) = id,
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
! [Xkek1,Xtype1,Xk1,Xtype2,Xkek2] :
( p(crypt(xor(km,Xtype2),decrypt(xor(Xkek2,Xtype2),crypt(xor(Xkek1,Xtype1),Xk1))))
| ~ p(crypt(xor(km,imp),Xkek2))
| ~ p(Xtype2)
| ~ p(crypt(xor(Xkek1,Xtype1),Xk1)) ),
inference(fof_nnf,[status(thm)],[key_import]) ).
fof(f_6_2,plain,
! [U_13,U_12,U_11,U_10,U_9] :
( p(crypt(xor(km,U_10),decrypt(xor(U_9,U_10),crypt(xor(U_13,U_12),U_11))))
| ~ p(crypt(xor(km,imp),U_9))
| ~ p(U_10)
| ~ p(crypt(xor(U_13,U_12),U_11)) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
( p(crypt(xor(km,U_10),decrypt(xor(U_9,U_10),crypt(xor(U_13,U_12),U_11))))
| ~ p(crypt(xor(km,imp),U_9))
| ~ p(U_10)
| ~ p(crypt(xor(U_13,U_12),U_11)) ),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
! [Xtype,Xk1,Xkek1] :
( p(crypt(xor(Xkek1,Xtype),Xk1))
| ~ p(crypt(xor(km,exp),Xkek1))
| ~ p(Xtype)
| ~ p(crypt(xor(km,Xtype),Xk1)) ),
inference(fof_nnf,[status(thm)],[key_export]) ).
fof(f_7_2,plain,
! [U_16,U_15,U_14] :
( p(crypt(xor(U_14,U_16),U_15))
| ~ p(crypt(xor(km,exp),U_14))
| ~ p(U_16)
| ~ p(crypt(xor(km,U_16),U_15)) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
cnf(f_7_3,plain,
( p(crypt(xor(U_14,U_16),U_15))
| ~ p(crypt(xor(km,exp),U_14))
| ~ p(U_16)
| ~ p(crypt(xor(km,U_16),U_15)) ),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
! [Xk,Xtype] :
( p(crypt(xor(km,xor(kp,Xtype)),Xk))
| ~ p(Xtype)
| ~ p(Xk) ),
inference(fof_nnf,[status(thm)],[key_part_import___part_1]) ).
fof(f_8_2,plain,
! [U_18,U_17] :
( p(crypt(xor(km,xor(kp,U_17)),U_18))
| ~ p(U_17)
| ~ p(U_18) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
cnf(f_8_3,plain,
( p(crypt(xor(km,xor(kp,U_17)),U_18))
| ~ p(U_17)
| ~ p(U_18) ),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
! [Xk1,Xtype,Xk2] :
( p(crypt(xor(km,xor(Xtype,kp)),xor(Xk1,Xk2)))
| ~ p(Xtype)
| ~ p(crypt(xor(km,xor(kp,Xtype)),Xk2))
| ~ p(Xk1) ),
inference(fof_nnf,[status(thm)],[key_part_import___part_2]) ).
fof(f_9_2,plain,
! [U_21,U_20,U_19] :
( p(crypt(xor(km,xor(U_20,kp)),xor(U_21,U_19)))
| ~ p(U_20)
| ~ p(crypt(xor(km,xor(kp,U_20)),U_19))
| ~ p(U_21) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
( p(crypt(xor(km,xor(U_20,kp)),xor(U_21,U_19)))
| ~ p(U_20)
| ~ p(crypt(xor(km,xor(kp,U_20)),U_19))
| ~ p(U_21) ),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
! [Xk1,Xtype,Xk2] :
( p(crypt(xor(km,Xtype),xor(Xk2,Xk1)))
| ~ p(Xtype)
| ~ p(crypt(xor(km,xor(Xtype,kp)),Xk2))
| ~ p(Xk1) ),
inference(fof_nnf,[status(thm)],[key_part_import___part_3]) ).
fof(f_10_2,plain,
! [U_24,U_23,U_22] :
( p(crypt(xor(km,U_23),xor(U_22,U_24)))
| ~ p(U_23)
| ~ p(crypt(xor(km,xor(U_23,kp)),U_22))
| ~ p(U_24) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
( p(crypt(xor(km,U_23),xor(U_22,U_24)))
| ~ p(U_23)
| ~ p(crypt(xor(km,xor(U_23,kp)),U_22))
| ~ p(U_24) ),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [X1,Xk1] :
( p(crypt(Xk1,X1))
| ~ p(crypt(xor(km,data),Xk1))
| ~ p(X1) ),
inference(fof_nnf,[status(thm)],[encrypt_data]) ).
fof(f_11_2,plain,
! [U_26,U_25] :
( p(crypt(U_25,U_26))
| ~ p(crypt(xor(km,data),U_25))
| ~ p(U_26) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
cnf(f_11_3,plain,
( p(crypt(U_25,U_26))
| ~ p(crypt(xor(km,data),U_25))
| ~ p(U_26) ),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,plain,
! [X1,Xk1] :
( p(decrypt(Xk1,X1))
| ~ p(crypt(xor(km,data),Xk1))
| ~ p(X1) ),
inference(fof_nnf,[status(thm)],[decrypt_data]) ).
fof(f_12_2,plain,
! [U_28,U_27] :
( p(decrypt(U_27,U_28))
| ~ p(crypt(xor(km,data),U_27))
| ~ p(U_28) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
cnf(f_12_3,plain,
( p(decrypt(U_27,U_28))
| ~ p(crypt(xor(km,data),U_27))
| ~ p(U_28) ),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_13_1,plain,
! [Xk,Xk1,Xtype2,Xkek1,Xkek2,Xtype] :
( p(crypt(xor(Xkek2,Xtype),decrypt(xor(Xtype2,Xkek1),crypt(Xk,Xk1))))
| ~ p(crypt(xor(km,exp),Xkek2))
| ~ p(crypt(xor(km,imp),Xkek1))
| ~ p(Xtype2)
| ~ p(crypt(Xk,Xk1)) ),
inference(fof_nnf,[status(thm)],[key_translate]) ).
fof(f_13_2,plain,
! [U_34,U_33,U_32,U_31,U_30,U_29] :
( p(crypt(xor(U_30,U_29),decrypt(xor(U_32,U_31),crypt(U_34,U_33))))
| ~ p(crypt(xor(km,exp),U_30))
| ~ p(crypt(xor(km,imp),U_31))
| ~ p(U_32)
| ~ p(crypt(U_34,U_33)) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
! [U_34,U_33,U_32,U_31,U_30] :
( ! [U_29] : p(crypt(xor(U_30,U_29),decrypt(xor(U_32,U_31),crypt(U_34,U_33))))
| ~ p(crypt(xor(km,exp),U_30))
| ~ p(crypt(xor(km,imp),U_31))
| ~ p(U_32)
| ~ p(crypt(U_34,U_33)) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
cnf(f_13_4,plain,
( p(crypt(xor(U_30,U_29),decrypt(xor(U_32,U_31),crypt(U_34,U_33))))
| ~ p(crypt(xor(km,exp),U_30))
| ~ p(crypt(xor(km,imp),U_31))
| ~ p(U_32)
| ~ p(crypt(U_34,U_33)) ),
inference(clausify,[status(thm)],[f_13_3]) ).
fof(f_14_1,plain,
! [X1,X2] :
( p(xor(X1,X2))
| ~ p(X2)
| ~ p(X1) ),
inference(fof_nnf,[status(thm)],[combine_with_XOR]) ).
fof(f_14_2,plain,
! [U_36,U_35] :
( p(xor(U_36,U_35))
| ~ p(U_35)
| ~ p(U_36) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
cnf(f_14_3,plain,
( p(xor(U_36,U_35))
| ~ p(U_35)
| ~ p(U_36) ),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
! [X1,X2] :
( p(X2)
| ~ p(X1)
| ~ p(crypt(X1,X2)) ),
inference(fof_nnf,[status(thm)],[decrypt_knowledge]) ).
fof(f_15_2,plain,
! [U_38,U_37] :
( p(U_37)
| ~ p(U_38)
| ~ p(crypt(U_38,U_37)) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
cnf(f_15_3,plain,
( p(U_37)
| ~ p(U_38)
| ~ p(crypt(U_38,U_37)) ),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
! [X1,X2] :
( p(crypt(X1,X2))
| ~ p(X1)
| ~ p(X2) ),
inference(fof_nnf,[status(thm)],[encrypt_knowledge]) ).
fof(f_16_2,plain,
! [U_40,U_39] :
( p(crypt(U_40,U_39))
| ~ p(U_40)
| ~ p(U_39) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
cnf(f_16_3,plain,
( p(crypt(U_40,U_39))
| ~ p(U_40)
| ~ p(U_39) ),
inference(clausify,[status(thm)],[f_16_2]) ).
fof(f_17_1,plain,
! [X1,X2] :
( p(crypt(X1,X2))
| ~ p(crypt(xor(X1,data),X2)) ),
inference(fof_nnf,[status(thm)],[data_cv_is_known_to_be_zero]) ).
fof(f_17_2,plain,
! [U_42,U_41] :
( p(crypt(U_42,U_41))
| ~ p(crypt(xor(U_42,data),U_41)) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
( p(crypt(U_42,U_41))
| ~ p(crypt(xor(U_42,data),U_41)) ),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
p(kp),
inference(fof_nnf,[status(thm)],[initial_knowledge_of_intruder_1]) ).
cnf(f_18_2,plain,
p(kp),
inference(clausify,[status(thm)],[f_18_1]) ).
fof(f_19_1,plain,
p(imp),
inference(fof_nnf,[status(thm)],[initial_knowledge_of_intruder_2]) ).
cnf(f_19_2,plain,
p(imp),
inference(clausify,[status(thm)],[f_19_1]) ).
fof(f_20_1,plain,
p(data),
inference(fof_nnf,[status(thm)],[initial_knowledge_of_intruder_3]) ).
cnf(f_20_2,plain,
p(data),
inference(clausify,[status(thm)],[f_20_1]) ).
fof(f_21_1,plain,
p(id),
inference(fof_nnf,[status(thm)],[initial_knowledge_of_intruder_4]) ).
cnf(f_21_2,plain,
p(id),
inference(clausify,[status(thm)],[f_21_1]) ).
fof(f_22_1,plain,
p(pin),
inference(fof_nnf,[status(thm)],[initial_knowledge_of_intruder_5]) ).
cnf(f_22_2,plain,
p(pin),
inference(clausify,[status(thm)],[f_22_1]) ).
fof(f_23_1,plain,
p(crypt(xor(km,pin),pp)),
inference(fof_nnf,[status(thm)],[initial_knowledge_of_intruder_6]) ).
cnf(f_23_2,plain,
p(crypt(xor(km,pin),pp)),
inference(clausify,[status(thm)],[f_23_1]) ).
fof(f_24_1,plain,
p(crypt(xor(km,exp),eurk)),
inference(fof_nnf,[status(thm)],[initial_knowledge_of_intruder_7]) ).
cnf(f_24_2,plain,
p(crypt(xor(km,exp),eurk)),
inference(clausify,[status(thm)],[f_24_1]) ).
fof(f_25_1,plain,
p(crypt(xor(km,data),eurk)),
inference(fof_nnf,[status(thm)],[initial_knowledge_of_intruder_8]) ).
cnf(f_25_2,plain,
p(crypt(xor(km,data),eurk)),
inference(clausify,[status(thm)],[f_25_1]) ).
fof(f_26_1,plain,
p(exp),
inference(fof_nnf,[status(thm)],[initial_knowledge_of_intruder_9]) ).
cnf(f_26_2,plain,
p(exp),
inference(clausify,[status(thm)],[f_26_1]) ).
fof(f_27_1,plain,
p(a),
inference(fof_nnf,[status(thm)],[an_account_number]) ).
cnf(f_27_2,plain,
p(a),
inference(clausify,[status(thm)],[f_27_1]) ).
fof(f_28_1,negated_conjecture,
~ ? [X] :
( p(X)
& p(crypt(xor(km,exp),X)) ),
inference(negate,[status(cth)],[find_known_exporter]) ).
fof(f_28_2,negated_conjecture,
! [X] :
( ~ p(X)
| ~ p(crypt(xor(km,exp),X)) ),
inference(fof_nnf,[status(thm)],[f_28_1]) ).
fof(f_28_3,negated_conjecture,
! [U_43] :
( ~ p(U_43)
| ~ p(crypt(xor(km,exp),U_43)) ),
inference(variable_rename,[status(thm)],[f_28_2]) ).
fof(f_28_4,negated_conjecture,
! [U_43] :
( ~ p(U_43)
| ~ p(crypt(xor(km,exp),U_43)) ),
inference(definitional_conversion,[status(esa)],[f_28_3]) ).
cnf(f_28_5,negated_conjecture,
( ~ p(U_43)
| ~ p(crypt(xor(km,exp),U_43)) ),
inference(clausify,[status(thm)],[f_28_4]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( xor(Eq_x_0,Eq_x_1) = xor(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( crypt(Eq_x_0,Eq_x_1) = crypt(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( decrypt(Eq_x_0,Eq_x_1) = decrypt(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( p(Eq_y_0)
| ~ p(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV236+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.56 % Computer : n020.cluster.edu
% 0.08/5.56 % Model : x86_64 x86_64
% 0.08/5.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.56 % Memory : 8046.5625MB
% 0.08/5.56 % OS : Linux 6.8.0-71-generic
% 0.08/5.56 % CPULimit : 300
% 0.08/5.56 % WCLimit : 300
% 0.08/5.56 % DateTime : Sun Sep 20 03:11:53 UTC 2026
% 0.08/5.57 % CPUTime :
% 24.34/29.88 % SZS status Theorem for theBenchmark
% 24.34/29.88 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------