%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV253-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:50:20 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV253-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 08:42:14 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.42 % Drodi V4.1.1
% 0.09/0.46 % Refutation found
% 0.09/0.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.46 fof(f2738,axiom,(
% 0.09/0.46 (![V_y]: (c_Message_OinvKey(c_Message_OinvKey(V_y)) = V_y ))),
% 0.09/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.46 fof(f2757,negated_conjecture,(
% 0.09/0.46 ( v_K != v_K_H| c_Message_OinvKey(v_K) != c_Message_OinvKey(v_K_H) ) ),
% 0.09/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.46 fof(f2758,negated_conjecture,(
% 0.09/0.46 ( c_Message_OinvKey(v_K) = c_Message_OinvKey(v_K_H)| v_K = v_K_H ) ),
% 0.09/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.46 fof(f6110,plain,(
% 0.09/0.46 ![X0]: (c_Message_OinvKey(c_Message_OinvKey(X0))=X0)),
% 0.09/0.46 inference(cnf_transformation,[status(thm)],[f2738])).
% 0.09/0.46 fof(f6133,plain,(
% 0.09/0.46 ~v_K=v_K_H|~c_Message_OinvKey(v_K)=c_Message_OinvKey(v_K_H)),
% 0.09/0.46 inference(cnf_transformation,[status(thm)],[f2757])).
% 0.09/0.46 fof(f6134,plain,(
% 0.09/0.46 c_Message_OinvKey(v_K)=c_Message_OinvKey(v_K_H)|v_K=v_K_H),
% 0.09/0.46 inference(cnf_transformation,[status(thm)],[f2758])).
% 0.09/0.46 fof(f6143,definition,(
% 0.09/0.46 sQ2_spl <=> (v_K=v_K_H)),
% 0.09/0.46 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.09/0.46 fof(f6144,plain,(
% 0.09/0.46 v_K=v_K_H|~sQ2_spl),
% 0.09/0.46 inference(component_clause,[status(thm)],[f6143])).
% 0.09/0.46 fof(f6145,plain,(
% 0.09/0.46 ~v_K=v_K_H|sQ2_spl),
% 0.09/0.46 inference(component_clause,[status(thm)],[f6143])).
% 0.09/0.46 fof(f6146,definition,(
% 0.09/0.46 sQ3_spl <=> (c_Message_OinvKey(v_K)=c_Message_OinvKey(v_K_H))),
% 0.09/0.46 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.09/0.46 fof(f6147,plain,(
% 0.09/0.46 c_Message_OinvKey(v_K)=c_Message_OinvKey(v_K_H)|~sQ3_spl),
% 0.09/0.46 inference(component_clause,[status(thm)],[f6146])).
% 0.09/0.46 fof(f6148,plain,(
% 0.09/0.46 ~c_Message_OinvKey(v_K)=c_Message_OinvKey(v_K_H)|sQ3_spl),
% 0.09/0.46 inference(component_clause,[status(thm)],[f6146])).
% 0.09/0.46 fof(f6149,plain,(
% 0.09/0.46 ~sQ2_spl|~sQ3_spl),
% 0.09/0.46 inference(split_clause,[status(thm)],[f6133,f6143,f6146])).
% 0.09/0.46 fof(f6150,plain,(
% 0.09/0.46 sQ3_spl|sQ2_spl),
% 0.09/0.46 inference(split_clause,[status(thm)],[f6134,f6146,f6143])).
% 0.09/0.46 fof(f6153,plain,(
% 0.09/0.46 c_Message_OinvKey(c_Message_OinvKey(v_K_H))=v_K|~sQ3_spl),
% 0.09/0.46 inference(paramodulation,[status(thm)],[f6147,f6110])).
% 0.09/0.46 fof(f6154,plain,(
% 0.09/0.46 v_K_H=v_K|~sQ3_spl),
% 0.09/0.46 inference(forward_demodulation,[status(thm)],[f6110,f6153])).
% 0.09/0.46 fof(f6155,plain,(
% 0.09/0.46 $false|sQ2_spl|~sQ3_spl),
% 0.09/0.46 inference(forward_subsumption_resolution,[status(thm)],[f6154,f6145])).
% 0.09/0.46 fof(f6156,plain,(
% 0.09/0.46 sQ2_spl|~sQ3_spl),
% 0.09/0.46 inference(contradiction_clause,[status(thm)],[f6155])).
% 0.09/0.46 fof(f6157,plain,(
% 0.09/0.46 ~c_Message_OinvKey(v_K_H)=c_Message_OinvKey(v_K_H)|~sQ2_spl|sQ3_spl),
% 0.09/0.46 inference(forward_demodulation,[status(thm)],[f6144,f6148])).
% 0.09/0.46 fof(f6158,plain,(
% 0.09/0.46 $false|~sQ2_spl|sQ3_spl),
% 0.09/0.46 inference(trivial_equality_resolution,[status(thm)],[f6157])).
% 0.09/0.46 fof(f6159,plain,(
% 0.09/0.46 ~sQ2_spl|sQ3_spl),
% 0.09/0.46 inference(contradiction_clause,[status(thm)],[f6158])).
% 0.09/0.46 fof(f6160,plain,(
% 0.09/0.46 $false),
% 0.09/0.46 inference(sat_refutation,[status(thm)],[f6149,f6150,f6156,f6159])).
% 0.09/0.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.51 % Elapsed time: 0.144871 seconds
% 0.09/0.51 % CPU time: 0.388831 seconds
% 0.09/0.51 % Total memory used: 217.158 MB
% 0.09/0.51 % Net memory used: 216.173 MB
%------------------------------------------------------------------------------