%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV759-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 : n019.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:07 PM UTC 2026
% Result : Unsatisfiable 226.55s 29.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV759-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 : n019.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:24:05 UTC 2026
% 0.11/0.35 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 226.55/29.06 % Refutation found
% 226.55/29.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 226.55/29.06 % SZS output start CNFRefutation for theBenchmark
% 226.55/29.06 fof(f24,axiom,(
% 226.55/29.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)) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f39,axiom,(
% 226.55/29.06 (![T_a,V_x]: (~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f63,axiom,(
% 226.55/29.06 c_Public_Okeymode_OEncryption != c_Public_Okeymode_OSignature ),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f64,axiom,(
% 226.55/29.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)) ) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f102,axiom,(
% 226.55/29.06 (![V_B,V_a,T_a]: (c_lessequals(V_B,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool)) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f128,axiom,(
% 226.55/29.06 (![V_x,V_B,T_a,V_A]: (( hBOOL(c_in(V_x,V_B,T_a))| ~ c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)) ) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f133,axiom,(
% 226.55/29.06 (![V_x,V_xa,T_a]: (c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f388,axiom,(
% 226.55/29.06 (![V_x,V_A,T_a]: (hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f390,axiom,(
% 226.55/29.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)) ) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f402,axiom,(
% 226.55/29.06 (![V_a,V_A,T_a]: (( c_Set_Oinsert(V_a,V_A,T_a) = V_A| ~ hBOOL(c_in(V_a,V_A,T_a)) ) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f464,axiom,(
% 226.55/29.06 (![V_xs,V_x,T_a]: (V_xs != c_List_Olist_OCons(V_x,V_xs,T_a) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f584,axiom,(
% 226.55/29.06 (![V_x,V_S,T_a]: (( hBOOL(c_in(V_x,V_S,T_a))| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f585,axiom,(
% 226.55/29.06 (![V_S,V_x,T_a]: (( hBOOL(hAPP(V_S,V_x))| ~ hBOOL(c_in(V_x,V_S,T_a)) ) ))),
% 226.55/29.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 226.55/29.06 fof(f669,plain,(
% 226.55/29.06 ![X0]: (c_List_Oset(c_List_Olist_ONil(X0),X0)=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f24])).
% 226.55/29.06 fof(f689,plain,(
% 226.55/29.06 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f39])).
% 226.55/29.06 fof(f718,plain,(
% 226.55/29.06 ~c_Public_Okeymode_OEncryption=c_Public_Okeymode_OSignature),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f63])).
% 226.55/29.06 fof(f719,plain,(
% 226.55/29.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)))),
% 226.55/29.06 inference(miniscoping,[status(thm)],[f64])).
% 226.55/29.06 fof(f720,plain,(
% 226.55/29.06 ![X0,X1]: (hBOOL(hAPP(X0,X1))|~hBOOL(hAPP(X0,c_Public_Okeymode_OEncryption))|~hBOOL(hAPP(X0,c_Public_Okeymode_OSignature)))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f719])).
% 226.55/29.06 fof(f772,plain,(
% 226.55/29.06 ![X0,X1,X2]: (c_lessequals(X0,c_Set_Oinsert(X1,X0,X2),tc_fun(X2,tc_bool)))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f102])).
% 226.55/29.06 fof(f813,plain,(
% 226.55/29.06 ![V_x,V_B,T_a]: (hBOOL(c_in(V_x,V_B,T_a))|(![V_A]: ~c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool))))),
% 226.55/29.06 inference(miniscoping,[status(thm)],[f128])).
% 226.55/29.06 fof(f814,plain,(
% 226.55/29.06 ![X0,X1,X2,X3]: (hBOOL(c_in(X0,X1,X2))|~c_lessequals(c_Set_Oinsert(X0,X3,X2),X1,tc_fun(X2,tc_bool)))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f813])).
% 226.55/29.06 fof(f822,plain,(
% 226.55/29.06 ![X0,X1,X2]: (~c_List_Olist_OCons(X0,X1,X2)=c_List_Olist_ONil(X2))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f133])).
% 226.55/29.06 fof(f1178,plain,(
% 226.55/29.06 ![X0,X1,X2]: (hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f388])).
% 226.55/29.06 fof(f1180,plain,(
% 226.55/29.06 ![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))))),
% 226.55/29.06 inference(miniscoping,[status(thm)],[f390])).
% 226.55/29.06 fof(f1181,plain,(
% 226.55/29.06 ![X0,X1,X2,X3]: (hBOOL(hAPP(X0,X1))|X2=X1|~hBOOL(hAPP(c_Set_Oinsert(X2,X0,X3),X1)))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f1180])).
% 226.55/29.06 fof(f1197,plain,(
% 226.55/29.06 ![X0,X1,X2]: (c_Set_Oinsert(X0,X1,X2)=X1|~hBOOL(c_in(X0,X1,X2)))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f402])).
% 226.55/29.06 fof(f1289,plain,(
% 226.55/29.06 ![X0,X1,X2]: (~X0=c_List_Olist_OCons(X1,X0,X2))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f464])).
% 226.55/29.06 fof(f1462,plain,(
% 226.55/29.06 ![V_x,V_S]: ((![T_a]: hBOOL(c_in(V_x,V_S,T_a)))|~hBOOL(hAPP(V_S,V_x)))),
% 226.55/29.06 inference(miniscoping,[status(thm)],[f584])).
% 226.55/29.06 fof(f1463,plain,(
% 226.55/29.06 ![X0,X1,X2]: (hBOOL(c_in(X0,X1,X2))|~hBOOL(hAPP(X1,X0)))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f1462])).
% 226.55/29.06 fof(f1464,plain,(
% 226.55/29.06 ![V_S,V_x]: (hBOOL(hAPP(V_S,V_x))|(![T_a]: ~hBOOL(c_in(V_x,V_S,T_a))))),
% 226.55/29.06 inference(miniscoping,[status(thm)],[f585])).
% 226.55/29.06 fof(f1465,plain,(
% 226.55/29.06 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|~hBOOL(c_in(X1,X0,X2)))),
% 226.55/29.06 inference(cnf_transformation,[status(thm)],[f1464])).
% 226.55/29.06 fof(f1992,plain,(
% 226.55/29.06 ![X0,X1,X2,X3]: (hBOOL(c_in(X0,c_Set_Oinsert(X0,X1,X2),X3)))),
% 226.55/29.06 inference(resolution,[status(thm)],[f1178,f1463])).
% 226.55/29.06 fof(f2491,plain,(
% 226.55/29.06 ![X0,X1]: (~hBOOL(hAPP(c_List_Oset(c_List_Olist_ONil(X0),X0),X1)))),
% 226.55/29.06 inference(paramodulation,[status(thm)],[f669,f689])).
% 226.55/29.06 fof(f3197,plain,(
% 226.55/29.06 ![X0,X1,X2,X3]: (c_Set_Oinsert(X0,c_Set_Oinsert(X0,X1,X2),X3)=c_Set_Oinsert(X0,X1,X2))),
% 226.55/29.06 inference(resolution,[status(thm)],[f1197,f1992])).
% 226.55/29.06 fof(f3271,plain,(
% 226.55/29.06 ![X0,X1,X2]: (hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X2))|~hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),c_Public_Okeymode_OSignature)))),
% 226.55/29.06 inference(resolution,[status(thm)],[f720,f1178])).
% 226.55/29.06 fof(f6567,plain,(
% 226.55/29.06 ![X0,X1,X2,X3]: (hBOOL(c_in(X0,c_Set_Oinsert(X1,c_Set_Oinsert(X0,X2,X3),X3),X3)))),
% 226.55/29.06 inference(resolution,[status(thm)],[f814,f772])).
% 226.55/29.06 fof(f7011,plain,(
% 226.55/29.06 ![X0,X1,X2,X3]: (hBOOL(hAPP(c_Set_Oinsert(X0,c_Set_Oinsert(X1,X2,X3),X3),X1)))),
% 226.55/29.06 inference(resolution,[status(thm)],[f6567,f1465])).
% 226.55/29.06 fof(f7132,plain,(
% 226.55/29.06 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(c_Set_Oinsert(X0,c_Set_Oinsert(X1,X2,X3),X4),X1)))),
% 226.55/29.06 inference(paramodulation,[status(thm)],[f3197,f7011])).
% 226.55/29.06 fof(f78126,plain,(
% 226.55/29.06 ![X0,X1,X2,X3]: (hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X2),X3)))),
% 226.55/29.06 inference(resolution,[status(thm)],[f3271,f7132])).
% 226.55/29.06 fof(f79102,plain,(
% 226.55/29.06 ![X0,X1,X2]: (hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X2))|c_Public_Okeymode_OEncryption=X2)),
% 226.55/29.06 inference(resolution,[status(thm)],[f78126,f1181])).
% 226.55/29.06 fof(f79143,plain,(
% 226.55/29.06 ![X0,X1]: (c_Public_Okeymode_OEncryption=X0|hBOOL(hAPP(X1,X0))|c_Public_Okeymode_OSignature=X0)),
% 226.55/29.06 inference(resolution,[status(thm)],[f79102,f1181])).
% 226.55/29.06 fof(f79196,plain,(
% 226.55/29.06 ![X0]: (c_Public_Okeymode_OEncryption=X0|c_Public_Okeymode_OSignature=X0)),
% 226.55/29.06 inference(resolution,[status(thm)],[f79143,f2491])).
% 226.55/29.06 fof(f79233,plain,(
% 226.55/29.06 ![X0,X1]: (c_Public_Okeymode_OSignature=c_List_Olist_OCons(X0,c_Public_Okeymode_OEncryption,X1))),
% 226.55/29.06 inference(resolution,[status(thm)],[f79196,f1289])).
% 226.55/29.06 fof(f79240,plain,(
% 226.55/29.06 ![X0,X1]: (X0=X1|c_Public_Okeymode_OSignature=X1|c_Public_Okeymode_OSignature=X0)),
% 226.55/29.06 inference(paramodulation,[status(thm)],[f79196,f79196])).
% 226.55/29.06 fof(f79391,plain,(
% 226.55/29.06 ![X0]: (~c_Public_Okeymode_OSignature=c_List_Olist_ONil(X0))),
% 226.55/29.06 inference(paramodulation,[status(thm)],[f79233,f822])).
% 226.55/29.06 fof(f79592,plain,(
% 226.55/29.06 ![X0,X1,X2]: (c_Public_Okeymode_OSignature=c_List_Olist_ONil(X0)|c_Public_Okeymode_OSignature=c_List_Olist_OCons(X1,X2,X0))),
% 226.55/29.06 inference(resolution,[status(thm)],[f79240,f822])).
% 226.55/29.06 fof(f79857,plain,(
% 226.55/29.06 ![X0,X1,X2]: (X0=c_List_Olist_OCons(X1,c_Public_Okeymode_OSignature,X2)|c_Public_Okeymode_OSignature=X0)),
% 226.55/29.06 inference(resolution,[status(thm)],[f79240,f1289])).
% 226.55/29.06 fof(f81582,plain,(
% 226.55/29.06 ![X0,X1,X2]: (c_Public_Okeymode_OSignature=c_List_Olist_OCons(X0,X1,X2))),
% 226.55/29.06 inference(forward_subsumption_resolution,[status(thm)],[f79592,f79391])).
% 226.55/29.06 fof(f81594,plain,(
% 226.55/29.06 ![X0]: (X0=c_Public_Okeymode_OSignature|c_Public_Okeymode_OSignature=X0)),
% 27.44/29.43 inference(forward_demodulation,[status(thm)],[f81582,f79857])).
% 27.44/29.43 fof(f81596,plain,(
% 27.44/29.43 ![X0]: (X0=c_Public_Okeymode_OSignature)),
% 27.44/29.43 inference(duplicate_literals_removal,[status(thm)],[f81594])).
% 27.44/29.43 fof(f81597,plain,(
% 27.44/29.43 $false),
% 27.44/29.43 inference(backward_subsumption_resolution,[status(thm)],[f718,f81596])).
% 27.44/29.43 % SZS output end CNFRefutation for theBenchmark.p
% 27.44/29.48 % Elapsed time: 29.113465 seconds
% 27.44/29.48 % CPU time: 229.400839 seconds
% 27.44/29.48 % Total memory used: 2.374 GB
% 27.44/29.48 % Net memory used: 2.284 GB
%------------------------------------------------------------------------------