%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV789-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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 02:53:10 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV789-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.56 % Computer : n002.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.57 % CPULimit : 300
% 0.09/0.57 % WCLimit : 300
% 0.09/0.57 % DateTime : Mon Sep 21 09:27:48 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.09/0.62 % Drodi V4.1.1
% 0.13/0.70 % Refutation found
% 0.13/0.70 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.70 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.70 fof(f29,axiom,(
% 0.13/0.70 (![T_a]: (c_List_Odistinct(c_List_Olist_ONil(T_a),T_a) ))),
% 0.13/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.70 fof(f154,axiom,(
% 0.13/0.70 (![T_a,V_a_H,V_list_H]: (c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) ))),
% 0.13/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.70 fof(f159,axiom,(
% 0.13/0.70 (![V_P,T_a]: (c_List_OdropWhile(V_P,c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ))),
% 0.13/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.70 fof(f189,axiom,(
% 0.13/0.70 (![T_a,V_x,V_xs]: (( c_List_OdropWhile(c_COMBB(c_Not,c_COMBC(c_fequal(T_a),V_x,T_a,T_a,tc_bool),tc_bool,tc_bool,T_a),c_List_Orev(V_xs,T_a),T_a) = c_List_Olist_OCons(V_x,c_List_Orev(c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(T_a),V_x,T_a,T_a,tc_bool),tc_bool,tc_bool,T_a),V_xs,T_a),T_a),T_a)| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)| ~ c_List_Odistinct(V_xs,T_a) ) ))),
% 0.13/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.70 fof(f557,axiom,(
% 0.13/0.70 (![T_a]: (c_List_Olist_ONil(T_a) = c_List_Orev(c_List_Olist_ONil(T_a),T_a) ))),
% 0.13/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.70 fof(f562,axiom,(
% 0.13/0.70 (![V_P,T_a]: (c_List_OtakeWhile(V_P,c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ))),
% 0.13/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.70 fof(f605,negated_conjecture,(
% 0.13/0.70 c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Oset(c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent) ),
% 0.13/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.70 fof(f677,plain,(
% 0.13/0.70 ![X0]: (c_List_Odistinct(c_List_Olist_ONil(X0),X0))),
% 0.13/0.70 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.70 fof(f857,plain,(
% 0.13/0.70 ![X0,X1,X2]: (~c_List_Olist_ONil(X0)=c_List_Olist_OCons(X1,X2,X0))),
% 0.13/0.70 inference(cnf_transformation,[status(thm)],[f154])).
% 0.13/0.70 fof(f866,plain,(
% 0.13/0.70 ![X0,X1]: (c_List_OdropWhile(X0,c_List_Olist_ONil(X1),X1)=c_List_Olist_ONil(X1))),
% 0.13/0.70 inference(cnf_transformation,[status(thm)],[f159])).
% 0.13/0.70 fof(f905,plain,(
% 0.13/0.70 ![T_a,V_xs]: ((![V_x]: (c_List_OdropWhile(c_COMBB(c_Not,c_COMBC(c_fequal(T_a),V_x,T_a,T_a,tc_bool),tc_bool,tc_bool,T_a),c_List_Orev(V_xs,T_a),T_a)=c_List_Olist_OCons(V_x,c_List_Orev(c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(T_a),V_x,T_a,T_a,tc_bool),tc_bool,tc_bool,T_a),V_xs,T_a),T_a),T_a)|~c_in(V_x,c_List_Oset(V_xs,T_a),T_a)))|~c_List_Odistinct(V_xs,T_a))),
% 0.13/0.70 inference(miniscoping,[status(thm)],[f189])).
% 0.13/0.70 fof(f906,plain,(
% 0.13/0.70 ![X0,X1,X2]: (c_List_OdropWhile(c_COMBB(c_Not,c_COMBC(c_fequal(X0),X1,X0,X0,tc_bool),tc_bool,tc_bool,X0),c_List_Orev(X2,X0),X0)=c_List_Olist_OCons(X1,c_List_Orev(c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(X0),X1,X0,X0,tc_bool),tc_bool,tc_bool,X0),X2,X0),X0),X0)|~c_in(X1,c_List_Oset(X2,X0),X0)|~c_List_Odistinct(X2,X0))),
% 0.13/0.70 inference(cnf_transformation,[status(thm)],[f905])).
% 0.13/0.70 fof(f1420,plain,(
% 0.13/0.70 ![X0]: (c_List_Olist_ONil(X0)=c_List_Orev(c_List_Olist_ONil(X0),X0))),
% 0.13/0.70 inference(cnf_transformation,[status(thm)],[f557])).
% 0.13/0.70 fof(f1426,plain,(
% 0.13/0.70 ![X0,X1]: (c_List_OtakeWhile(X0,c_List_Olist_ONil(X1),X1)=c_List_Olist_ONil(X1))),
% 0.13/0.70 inference(cnf_transformation,[status(thm)],[f562])).
% 0.13/0.70 fof(f1483,plain,(
% 0.13/0.70 c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Oset(c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)),
% 0.13/0.70 inference(cnf_transformation,[status(thm)],[f605])).
% 0.13/0.70 fof(f1742,plain,(
% 0.13/0.70 c_List_OdropWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Orev(c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)=c_List_Olist_OCons(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Orev(c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)|~c_List_Odistinct(c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)),
% 0.13/0.70 inference(resolution,[status(thm)],[f906,f1483])).
% 0.13/0.70 fof(f1745,definition,(
% 0.13/0.70 sQ5_spl <=> (c_List_OdropWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Orev(c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)=c_List_Olist_OCons(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Orev(c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent))),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f1746,plain,(
% 0.13/0.70 c_List_OdropWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Orev(c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)=c_List_Olist_OCons(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Orev(c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)|~sQ5_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f1745])).
% 0.13/0.70 fof(f1748,definition,(
% 0.13/0.70 sQ6_spl <=> (c_List_Odistinct(c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent))),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f1750,plain,(
% 0.13/0.70 ~c_List_Odistinct(c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)|sQ6_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f1748])).
% 0.13/0.70 fof(f1751,plain,(
% 0.13/0.70 sQ5_spl|~sQ6_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1742,f1745,f1748])).
% 0.13/0.70 fof(f1757,plain,(
% 0.13/0.70 c_List_OdropWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)=c_List_Olist_OCons(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Orev(c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)|~sQ5_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1420,f1746])).
% 0.13/0.70 fof(f1758,plain,(
% 0.13/0.70 c_List_OdropWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)=c_List_Olist_OCons(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Orev(c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)|~sQ5_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1426,f1757])).
% 0.13/0.70 fof(f1759,plain,(
% 0.13/0.70 c_List_OdropWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)=c_List_Olist_OCons(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)|~sQ5_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1420,f1758])).
% 0.13/0.70 fof(f2235,plain,(
% 0.13/0.70 c_List_Olist_ONil(tc_Event_Oevent)=c_List_Olist_OCons(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)|~sQ5_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f866,f1759])).
% 0.13/0.70 fof(f2236,plain,(
% 0.13/0.70 $false|~sQ5_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f2235,f857])).
% 0.13/0.70 fof(f2237,plain,(
% 0.13/0.70 ~sQ5_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f2236])).
% 0.13/0.70 fof(f2238,plain,(
% 0.13/0.70 $false|sQ6_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1750,f677])).
% 0.13/0.70 fof(f2239,plain,(
% 0.13/0.70 sQ6_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f2238])).
% 0.13/0.70 fof(f2240,plain,(
% 0.13/0.70 $false),
% 0.13/0.70 inference(sat_refutation,[status(thm)],[f1751,f2237,f2239])).
% 0.13/0.70 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.71 % Elapsed time: 0.135893 seconds
% 0.13/0.71 % CPU time: 0.622971 seconds
% 0.13/0.71 % Total memory used: 144.922 MB
% 0.13/0.71 % Net memory used: 144.228 MB
%------------------------------------------------------------------------------