%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV765-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -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 02:49:30 PM UTC 2026
% Result : Unsatisfiable 144.22s 18.81s
% Output : CNFRefutation 122.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 9
% Syntax : Number of formulae : 33 ( 16 unt; 0 def)
% Number of atoms : 57 ( 25 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 48 ( 24 ~; 24 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-4 aty)
% Number of variables : 102 ( 102 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [T_a,V_x] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [V_K,V_KK,V_C] : c_Set_Oinsert(hAPP(c_Message_Omsg_OKey,V_K),c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_Omsg_OKey,V_KK,tc_nat,tc_Message_Omsg),V_C,tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg) = c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oinsert(V_K,V_KK,tc_nat),tc_nat,tc_Message_Omsg),V_C,tc_fun(tc_Message_Omsg,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [V_P,V_keymode] :
( ~ hBOOL(hAPP(V_P,c_Public_Okeymode_OSignature))
| ~ hBOOL(hAPP(V_P,c_Public_Okeymode_OEncryption))
| hBOOL(hAPP(V_P,V_keymode)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f251,axiom,
! [V_x,V_A,T_a] : hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f264,axiom,
! [V_A,V_x,V_y,T_a] :
( ~ hBOOL(hAPP(c_Set_Oinsert(V_y,V_A,T_a),V_x))
| V_y = V_x
| hBOOL(hAPP(V_A,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f277,axiom,
! [V_y,V_A,T_a,V_x] :
( ~ hBOOL(hAPP(V_A,V_x))
| hBOOL(hAPP(c_Set_Oinsert(V_y,V_A,T_a),V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f382,axiom,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f408,axiom,
! [V_a,V_list,T_a,V_a_H,V_list_H] :
( V_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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f559,plain,
! [X0,X1] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f581,plain,
! [X0,X1,X2] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f649,plain,
! [X0,X1,X2] : c_Set_Oinsert(hAPP(c_Message_Omsg_OKey,X0),c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_Omsg_OKey,X1,tc_nat,tc_Message_Omsg),X2,tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg) = c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oinsert(X0,X1,tc_nat),tc_nat,tc_Message_Omsg),X2,tc_fun(tc_Message_Omsg,tc_bool)),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f650,plain,
! [V_P] :
( ~ hBOOL(hAPP(V_P,c_Public_Okeymode_OSignature))
| ~ hBOOL(hAPP(V_P,c_Public_Okeymode_OEncryption))
| ! [V_keymode] : hBOOL(hAPP(V_P,V_keymode)) ),
inference(miniscoping,[status(thm)],[f77]) ).
fof(f651,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OEncryption))
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f650]) ).
fof(f890,plain,
! [X0,X1,X2] : hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f904,plain,
! [V_A,V_x,V_y] :
( ! [T_a] : ~ hBOOL(hAPP(c_Set_Oinsert(V_y,V_A,T_a),V_x))
| V_y = V_x
| hBOOL(hAPP(V_A,V_x)) ),
inference(miniscoping,[status(thm)],[f264]) ).
fof(f905,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(c_Set_Oinsert(X2,X0,X3),X1))
| X2 = X1
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f904]) ).
fof(f921,plain,
! [V_A,V_x] :
( ~ hBOOL(hAPP(V_A,V_x))
| ! [V_y,T_a] : hBOOL(hAPP(c_Set_Oinsert(V_y,V_A,T_a),V_x)) ),
inference(miniscoping,[status(thm)],[f277]) ).
fof(f922,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(X1,X3))
| hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X3)) ),
inference(cnf_transformation,[status(thm)],[f921]) ).
fof(f1075,plain,
! [X0,X1,X2] : X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f1110,plain,
! [V_a,V_a_H] :
( V_a = V_a_H
| ! [V_list,T_a,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) ),
inference(miniscoping,[status(thm)],[f408]) ).
fof(f1111,plain,
! [X0,X1,X2,X3,X4] :
( X0 = X3
| c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_OCons(X3,X4,X2) ),
inference(cnf_transformation,[status(thm)],[f1110]) ).
fof(f4118,plain,
! [X0,X1,X2] : c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)) != c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(c_Message_Omsg_OKey,c_Set_Oinsert(X0,X1,tc_nat),tc_nat,tc_Message_Omsg),X2,tc_fun(tc_Message_Omsg,tc_bool)),
inference(paramodulation,[status(thm)],[f649,f581]) ).
fof(f4127,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),c_Public_Okeymode_OEncryption))
| hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X2)) ),
inference(resolution,[status(thm)],[f651,f890]) ).
fof(f12360,plain,
! [X0,X1,X2,X3,X4] : hBOOL(hAPP(c_Set_Oinsert(X0,c_Set_Oinsert(X1,X2,X3),X4),X1)),
inference(resolution,[status(thm)],[f922,f890]) ).
fof(f104346,plain,
! [X0,X1,X2,X3] : hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X2),X3)),
inference(resolution,[status(thm)],[f4127,f12360]) ).
fof(f105545,plain,
! [X0,X1,X2] :
( c_Public_Okeymode_OSignature = X2
| hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X2)) ),
inference(resolution,[status(thm)],[f104346,f905]) ).
fof(f105577,plain,
! [X0,X1] :
( c_Public_Okeymode_OEncryption = X0
| hBOOL(hAPP(X1,X0))
| c_Public_Okeymode_OSignature = X0 ),
inference(resolution,[status(thm)],[f105545,f905]) ).
fof(f105616,plain,
! [X0] :
( c_Public_Okeymode_OEncryption = X0
| c_Public_Okeymode_OSignature = X0 ),
inference(resolution,[status(thm)],[f105577,f559]) ).
fof(f105647,plain,
! [X0,X1] : c_Public_Okeymode_OEncryption = c_List_Olist_OCons(X0,c_Public_Okeymode_OSignature,X1),
inference(resolution,[status(thm)],[f105616,f1075]) ).
fof(f105701,plain,
! [X0,X1,X2,X3] :
( X0 = X3
| c_List_Olist_OCons(X0,X1,X2) != c_Public_Okeymode_OEncryption ),
inference(paramodulation,[status(thm)],[f105647,f1111]) ).
fof(f107664,plain,
! [X0,X1] : X0 = X1,
inference(resolution,[status(thm)],[f105701,f105647]) ).
fof(f107685,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f4118,f107664]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV765-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n020.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 21 09:24:48 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.20/0.48 % Drodi V4.1.1
% 144.22/18.81 % Refutation found
% 144.22/18.81 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 144.22/18.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 57.80/20.25 % Elapsed time: 19.619522 seconds
% 57.80/20.25 % CPU time: 137.565022 seconds
% 57.80/20.25 % Total memory used: 1.031 GB
% 57.80/20.25 % Net memory used: 970.895 MB
%------------------------------------------------------------------------------