%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV752-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 02:53:06 PM UTC 2026
% Result : Unsatisfiable 99.28s 13.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV752-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.35 % Computer : n017.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Mon Sep 21 09:18:41 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.15/0.40 % Drodi V4.1.1
% 99.28/13.06 % Refutation found
% 99.28/13.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 99.28/13.06 % SZS output start CNFRefutation for theBenchmark
% 99.28/13.06 fof(f11,axiom,(
% 99.28/13.06 c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))) = c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) ),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f29,axiom,(
% 99.28/13.06 (![V_P,V_keymode]: (( hBOOL(hAPP(V_P,V_keymode))| ~ hBOOL(hAPP(V_P,c_Public_Okeymode_OEncryption))| ~ hBOOL(hAPP(V_P,c_Public_Okeymode_OSignature)) ) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f41,axiom,(
% 99.28/13.06 (![T_a,V_x]: (~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f61,axiom,(
% 99.28/13.06 (![T_a]: (c_List_Oset(c_List_Olist_ONil(T_a),T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f207,axiom,(
% 99.28/13.06 (![V_Q,V_x,V_P,T_a]: (( hBOOL(hAPP(V_Q,V_x))| ~ hBOOL(hAPP(V_P,V_x))| ~ c_lessequals(V_P,V_Q,tc_fun(T_a,tc_bool)) ) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f232,axiom,(
% 99.28/13.06 (![V_H]: (c_lessequals(c_Message_Oanalz(V_H),c_Message_Oparts(V_H),tc_fun(tc_Message_Omsg,tc_bool)) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f372,axiom,(
% 99.28/13.06 (![V_a,V_b,V_B,T_a]: (( c_in(V_a,c_Set_Oinsert(V_b,V_B,T_a),T_a)| ~ c_in(V_a,V_B,T_a) ) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f383,axiom,(
% 99.28/13.06 (![V_xs,V_x,T_a]: (V_xs != c_List_Olist_OCons(V_x,V_xs,T_a) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f389,axiom,(
% 99.28/13.06 (![V_a_H,V_list_H,T_a]: (c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f414,axiom,(
% 99.28/13.06 (![V_A,V_x,V_y,T_a]: (( hBOOL(hAPP(V_A,V_x))| V_y = V_x| ~ hBOOL(hAPP(c_Set_Oinsert(V_y,V_A,T_a),V_x)) ) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f431,axiom,(
% 99.28/13.06 (![V_x,V_A,T_a]: (hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f438,axiom,(
% 99.28/13.06 (![V_a,V_list,T_a,V_a_H,V_list_H]: (( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a)| V_list = V_list_H ) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f534,axiom,(
% 99.28/13.06 (![V_x,V_S,T_a]: (( c_in(V_x,V_S,T_a)| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f535,axiom,(
% 99.28/13.06 (![V_S,V_x,T_a]: (( hBOOL(hAPP(V_S,V_x))| ~ c_in(V_x,V_S,T_a) ) ))),
% 99.28/13.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.28/13.06 fof(f594,plain,(
% 99.28/13.06 c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)))=c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))),
% 99.28/13.06 inference(cnf_transformation,[status(thm)],[f11])).
% 99.28/13.06 fof(f620,plain,(
% 99.28/13.06 ![V_P]: (((![V_keymode]: hBOOL(hAPP(V_P,V_keymode)))|~hBOOL(hAPP(V_P,c_Public_Okeymode_OEncryption)))|~hBOOL(hAPP(V_P,c_Public_Okeymode_OSignature)))),
% 99.28/13.07 inference(miniscoping,[status(thm)],[f29])).
% 99.28/13.07 fof(f621,plain,(
% 99.28/13.07 ![X0,X1]: (hBOOL(hAPP(X0,X1))|~hBOOL(hAPP(X0,c_Public_Okeymode_OEncryption))|~hBOOL(hAPP(X0,c_Public_Okeymode_OSignature)))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f620])).
% 99.28/13.07 fof(f636,plain,(
% 99.28/13.07 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f41])).
% 99.28/13.07 fof(f662,plain,(
% 99.28/13.07 ![X0]: (c_List_Oset(c_List_Olist_ONil(X0),X0)=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f61])).
% 99.28/13.07 fof(f869,plain,(
% 99.28/13.07 ![V_Q,V_P]: ((![V_x]: (hBOOL(hAPP(V_Q,V_x))|~hBOOL(hAPP(V_P,V_x))))|(![T_a]: ~c_lessequals(V_P,V_Q,tc_fun(T_a,tc_bool))))),
% 99.28/13.07 inference(miniscoping,[status(thm)],[f207])).
% 99.28/13.07 fof(f870,plain,(
% 99.28/13.07 ![X0,X1,X2,X3]: (hBOOL(hAPP(X0,X1))|~hBOOL(hAPP(X2,X1))|~c_lessequals(X2,X0,tc_fun(X3,tc_bool)))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f869])).
% 99.28/13.07 fof(f912,plain,(
% 99.28/13.07 ![X0]: (c_lessequals(c_Message_Oanalz(X0),c_Message_Oparts(X0),tc_fun(tc_Message_Omsg,tc_bool)))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f232])).
% 99.28/13.07 fof(f1103,plain,(
% 99.28/13.07 ![V_a,V_B,T_a]: ((![V_b]: c_in(V_a,c_Set_Oinsert(V_b,V_B,T_a),T_a))|~c_in(V_a,V_B,T_a))),
% 99.28/13.07 inference(miniscoping,[status(thm)],[f372])).
% 99.28/13.07 fof(f1104,plain,(
% 99.28/13.07 ![X0,X1,X2,X3]: (c_in(X0,c_Set_Oinsert(X1,X2,X3),X3)|~c_in(X0,X2,X3))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f1103])).
% 99.28/13.07 fof(f1118,plain,(
% 99.28/13.07 ![X0,X1,X2]: (~X0=c_List_Olist_OCons(X1,X0,X2))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f383])).
% 99.28/13.07 fof(f1124,plain,(
% 99.28/13.07 ![X0,X1,X2]: (~c_List_Olist_OCons(X0,X1,X2)=c_List_Olist_ONil(X2))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f389])).
% 99.28/13.07 fof(f1156,plain,(
% 99.28/13.07 ![V_A,V_x,V_y]: ((hBOOL(hAPP(V_A,V_x))|V_y=V_x)|(![T_a]: ~hBOOL(hAPP(c_Set_Oinsert(V_y,V_A,T_a),V_x))))),
% 99.28/13.07 inference(miniscoping,[status(thm)],[f414])).
% 99.28/13.07 fof(f1157,plain,(
% 99.28/13.07 ![X0,X1,X2,X3]: (hBOOL(hAPP(X0,X1))|X2=X1|~hBOOL(hAPP(c_Set_Oinsert(X2,X0,X3),X1)))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f1156])).
% 99.28/13.07 fof(f1178,plain,(
% 99.28/13.07 ![X0,X1,X2]: (hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f431])).
% 99.28/13.07 fof(f1186,plain,(
% 99.28/13.07 ![V_list,V_list_H]: ((![V_a,T_a,V_a_H]: ~c_List_Olist_OCons(V_a,V_list,T_a)=c_List_Olist_OCons(V_a_H,V_list_H,T_a))|V_list=V_list_H)),
% 99.28/13.07 inference(miniscoping,[status(thm)],[f438])).
% 99.28/13.07 fof(f1187,plain,(
% 99.28/13.07 ![X0,X1,X2,X3,X4]: (~c_List_Olist_OCons(X0,X1,X2)=c_List_Olist_OCons(X3,X4,X2)|X1=X4)),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f1186])).
% 99.28/13.07 fof(f1332,plain,(
% 99.28/13.07 ![V_x,V_S]: ((![T_a]: c_in(V_x,V_S,T_a))|~hBOOL(hAPP(V_S,V_x)))),
% 99.28/13.07 inference(miniscoping,[status(thm)],[f534])).
% 99.28/13.07 fof(f1333,plain,(
% 99.28/13.07 ![X0,X1,X2]: (c_in(X0,X1,X2)|~hBOOL(hAPP(X1,X0)))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f1332])).
% 99.28/13.07 fof(f1334,plain,(
% 99.28/13.07 ![V_S,V_x]: (hBOOL(hAPP(V_S,V_x))|(![T_a]: ~c_in(V_x,V_S,T_a)))),
% 99.28/13.07 inference(miniscoping,[status(thm)],[f535])).
% 99.28/13.07 fof(f1335,plain,(
% 99.28/13.07 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|~c_in(X1,X0,X2))),
% 99.28/13.07 inference(cnf_transformation,[status(thm)],[f1334])).
% 99.28/13.07 fof(f1472,plain,(
% 99.28/13.07 c_lessequals(c_Message_Oanalz(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))),c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool))),
% 99.28/13.07 inference(paramodulation,[status(thm)],[f594,f912])).
% 99.28/13.07 fof(f2659,plain,(
% 99.28/13.07 ![X0,X1,X2]: (hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X2))|~hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),c_Public_Okeymode_OEncryption)))),
% 99.28/13.07 inference(resolution,[status(thm)],[f621,f1178])).
% 99.28/13.07 fof(f3917,plain,(
% 99.28/13.07 ![X0,X1,X2,X3]: (c_in(X0,c_Set_Oinsert(X0,X1,X2),X3))),
% 99.28/13.07 inference(resolution,[status(thm)],[f1333,f1178])).
% 99.28/13.07 fof(f5197,plain,(
% 99.28/13.07 ![X0,X1]: (~hBOOL(hAPP(c_List_Oset(c_List_Olist_ONil(X0),X0),X1)))),
% 99.28/13.07 inference(paramodulation,[status(thm)],[f662,f636])).
% 99.28/13.07 fof(f9935,plain,(
% 99.28/13.07 ![X0,X1,X2,X3,X4]: (c_in(X0,c_Set_Oinsert(X1,c_Set_Oinsert(X0,X2,X3),X4),X4))),
% 99.28/13.07 inference(resolution,[status(thm)],[f1104,f3917])).
% 99.28/13.07 fof(f10476,plain,(
% 99.28/13.07 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(c_Set_Oinsert(X0,c_Set_Oinsert(X1,X2,X3),X4),X1)))),
% 99.28/13.07 inference(resolution,[status(thm)],[f9935,f1335])).
% 99.28/13.07 fof(f13275,plain,(
% 99.28/13.07 c_lessequals(c_Message_Oanalz(c_List_Oset(c_List_Olist_ONil(tc_Message_Omsg),tc_Message_Omsg)),c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool))),
% 99.28/13.07 inference(forward_demodulation,[status(thm)],[f662,f1472])).
% 99.28/13.07 fof(f13276,plain,(
% 99.28/13.07 c_lessequals(c_Message_Oanalz(c_List_Oset(c_List_Olist_ONil(tc_Message_Omsg),tc_Message_Omsg)),c_List_Oset(c_List_Olist_ONil(tc_Message_Omsg),tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool))),
% 99.28/13.07 inference(forward_demodulation,[status(thm)],[f662,f13275])).
% 99.28/13.07 fof(f23747,plain,(
% 99.28/13.07 ![X0]: (hBOOL(hAPP(c_List_Oset(c_List_Olist_ONil(tc_Message_Omsg),tc_Message_Omsg),X0))|~hBOOL(hAPP(c_Message_Oanalz(c_List_Oset(c_List_Olist_ONil(tc_Message_Omsg),tc_Message_Omsg)),X0)))),
% 99.28/13.07 inference(resolution,[status(thm)],[f870,f13276])).
% 99.28/13.07 fof(f23764,plain,(
% 99.28/13.07 ![X0]: (~hBOOL(hAPP(c_Message_Oanalz(c_List_Oset(c_List_Olist_ONil(tc_Message_Omsg),tc_Message_Omsg)),X0)))),
% 99.28/13.07 inference(forward_subsumption_resolution,[status(thm)],[f23747,f5197])).
% 100.05/13.15 fof(f93375,plain,(
% 100.05/13.15 ![X0,X1,X2,X3]: (hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X2),X3)))),
% 100.05/13.15 inference(resolution,[status(thm)],[f2659,f10476])).
% 100.05/13.15 fof(f94629,plain,(
% 100.05/13.15 ![X0,X1,X2]: (hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X2))|c_Public_Okeymode_OSignature=X2)),
% 100.05/13.15 inference(resolution,[status(thm)],[f93375,f1157])).
% 100.05/13.15 fof(f94665,plain,(
% 100.05/13.15 ![X0,X1]: (c_Public_Okeymode_OSignature=X0|hBOOL(hAPP(X1,X0))|c_Public_Okeymode_OEncryption=X0)),
% 100.05/13.15 inference(resolution,[status(thm)],[f94629,f1157])).
% 100.05/13.15 fof(f94703,plain,(
% 100.05/13.15 ![X0]: (c_Public_Okeymode_OSignature=X0|c_Public_Okeymode_OEncryption=X0)),
% 100.05/13.15 inference(resolution,[status(thm)],[f94665,f23764])).
% 100.05/13.15 fof(f94746,plain,(
% 100.05/13.15 ![X0,X1]: (c_Public_Okeymode_OEncryption=c_List_Olist_OCons(X0,c_Public_Okeymode_OSignature,X1))),
% 100.05/13.15 inference(resolution,[status(thm)],[f94703,f1118])).
% 100.05/13.15 fof(f94754,plain,(
% 100.05/13.15 ![X0,X1]: (X0=X1|c_Public_Okeymode_OEncryption=X1|c_Public_Okeymode_OEncryption=X0)),
% 100.05/13.15 inference(paramodulation,[status(thm)],[f94703,f94703])).
% 100.05/13.15 fof(f94828,plain,(
% 100.05/13.15 ![X0]: (~c_Public_Okeymode_OEncryption=c_List_Olist_ONil(X0))),
% 100.05/13.15 inference(paramodulation,[status(thm)],[f94746,f1124])).
% 100.05/13.15 fof(f94964,plain,(
% 100.05/13.15 ![X0,X1,X2]: (c_Public_Okeymode_OEncryption=c_List_Olist_ONil(X0)|c_Public_Okeymode_OEncryption=c_List_Olist_OCons(X1,X2,X0))),
% 100.05/13.15 inference(resolution,[status(thm)],[f94754,f1124])).
% 100.05/13.15 fof(f95253,plain,(
% 100.05/13.15 ![X0,X1,X2]: (c_Public_Okeymode_OEncryption=c_List_Olist_OCons(X0,X1,X2))),
% 100.05/13.15 inference(forward_subsumption_resolution,[status(thm)],[f94964,f94828])).
% 100.05/13.15 fof(f95366,plain,(
% 100.05/13.15 ![X0,X1,X2,X3]: (~c_List_Olist_OCons(X0,X1,X2)=c_Public_Okeymode_OEncryption|X1=X3)),
% 100.05/13.15 inference(backward_demodulation,[status(thm)],[f95253,f1187])).
% 100.05/13.15 fof(f95409,plain,(
% 100.05/13.15 ![X0,X1]: (~c_Public_Okeymode_OEncryption=c_Public_Okeymode_OEncryption|X0=X1)),
% 100.05/13.15 inference(forward_demodulation,[status(thm)],[f95253,f95366])).
% 100.05/13.15 fof(f95410,plain,(
% 100.05/13.15 ![X0,X1]: (X0=X1)),
% 100.05/13.15 inference(trivial_equality_resolution,[status(thm)],[f95409])).
% 100.05/13.15 fof(f95415,plain,(
% 100.05/13.15 $false),
% 100.05/13.15 inference(backward_subsumption_resolution,[status(thm)],[f94828,f95410])).
% 100.05/13.15 % SZS output end CNFRefutation for theBenchmark.p
% 73.10/13.33 % Elapsed time: 12.945061 seconds
% 73.10/13.33 % CPU time: 101.231095 seconds
% 73.10/13.33 % Total memory used: 1.039 GB
% 73.10/13.33 % Net memory used: 1.003 GB
%------------------------------------------------------------------------------