%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV250-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 : n012.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:19 PM UTC 2026
% Result : Unsatisfiable 0.75s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV250-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 08:35:53 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 0.75/0.55 % Refutation found
% 0.75/0.55 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.75/0.55 % SZS output start CNFRefutation for theBenchmark
% 0.75/0.55 fof(f2640,axiom,(
% 0.75/0.55 (![V_c,V_A,V_B,T_a]: (( ~ c_in(V_c,c_union(V_A,V_B,T_a),T_a)| c_in(V_c,V_B,T_a)| c_in(V_c,V_A,T_a) ) ))),
% 0.75/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.75/0.55 fof(f2641,axiom,(
% 0.75/0.55 (![V_c,V_A,T_a,V_B]: (( ~ c_in(V_c,V_A,T_a)| c_in(V_c,c_union(V_A,V_B,T_a),T_a) ) ))),
% 0.75/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.75/0.55 fof(f2642,axiom,(
% 0.75/0.55 (![V_c,V_B,T_a,V_A]: (( ~ c_in(V_c,V_B,T_a)| c_in(V_c,c_union(V_A,V_B,T_a),T_a) ) ))),
% 0.75/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.75/0.55 fof(f2823,axiom,(
% 0.75/0.55 (![V_G,V_H]: (c_Message_Oanalz(c_union(c_Message_Oanalz(V_G),V_H,tc_Message_Omsg)) = c_Message_Oanalz(c_union(V_G,V_H,tc_Message_Omsg)) ))),
% 0.75/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.75/0.55 fof(f2826,axiom,(
% 0.75/0.55 (![V_G,V_H]: (c_Message_Oanalz(c_union(c_Message_Osynth(V_G),V_H,tc_Message_Omsg)) = c_union(c_Message_Oanalz(c_union(V_G,V_H,tc_Message_Omsg)),c_Message_Osynth(V_G),tc_Message_Omsg) ))),
% 0.75/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.75/0.55 fof(f2831,negated_conjecture,(
% 0.75/0.55 c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)),tc_Message_Omsg) ),
% 0.75/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.75/0.55 fof(f2832,negated_conjecture,(
% 0.75/0.55 ~ c_in(v_x,c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg) ),
% 0.75/0.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.75/0.55 fof(f6054,plain,(
% 0.75/0.55 ![V_c,V_A,T_a]: ((![V_B]: (~c_in(V_c,c_union(V_A,V_B,T_a),T_a)|c_in(V_c,V_B,T_a)))|c_in(V_c,V_A,T_a))),
% 0.75/0.55 inference(miniscoping,[status(thm)],[f2640])).
% 0.75/0.55 fof(f6055,plain,(
% 0.75/0.55 ![X0,X1,X2,X3]: (~c_in(X0,c_union(X1,X2,X3),X3)|c_in(X0,X2,X3)|c_in(X0,X1,X3))),
% 0.75/0.55 inference(cnf_transformation,[status(thm)],[f6054])).
% 0.75/0.55 fof(f6056,plain,(
% 0.75/0.55 ![V_c,V_A,T_a]: (~c_in(V_c,V_A,T_a)|(![V_B]: c_in(V_c,c_union(V_A,V_B,T_a),T_a)))),
% 0.75/0.55 inference(miniscoping,[status(thm)],[f2641])).
% 0.75/0.55 fof(f6057,plain,(
% 0.75/0.55 ![X0,X1,X2,X3]: (~c_in(X0,X1,X2)|c_in(X0,c_union(X1,X3,X2),X2))),
% 0.75/0.55 inference(cnf_transformation,[status(thm)],[f6056])).
% 0.75/0.55 fof(f6058,plain,(
% 0.75/0.55 ![V_c,V_B,T_a]: (~c_in(V_c,V_B,T_a)|(![V_A]: c_in(V_c,c_union(V_A,V_B,T_a),T_a)))),
% 0.75/0.55 inference(miniscoping,[status(thm)],[f2642])).
% 0.75/0.55 fof(f6059,plain,(
% 0.75/0.55 ![X0,X1,X2,X3]: (~c_in(X0,X1,X2)|c_in(X0,c_union(X3,X1,X2),X2))),
% 0.75/0.55 inference(cnf_transformation,[status(thm)],[f6058])).
% 0.75/0.55 fof(f6283,plain,(
% 0.75/0.55 ![X0,X1]: (c_Message_Oanalz(c_union(c_Message_Oanalz(X0),X1,tc_Message_Omsg))=c_Message_Oanalz(c_union(X0,X1,tc_Message_Omsg)))),
% 0.75/0.55 inference(cnf_transformation,[status(thm)],[f2823])).
% 0.75/0.55 fof(f6286,plain,(
% 0.75/0.55 ![X0,X1]: (c_Message_Oanalz(c_union(c_Message_Osynth(X0),X1,tc_Message_Omsg))=c_union(c_Message_Oanalz(c_union(X0,X1,tc_Message_Omsg)),c_Message_Osynth(X0),tc_Message_Omsg))),
% 0.75/0.55 inference(cnf_transformation,[status(thm)],[f2826])).
% 0.75/0.55 fof(f6291,plain,(
% 0.75/0.55 c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)),tc_Message_Omsg)),
% 0.75/0.55 inference(cnf_transformation,[status(thm)],[f2831])).
% 0.75/0.55 fof(f6292,plain,(
% 0.75/0.55 ~c_in(v_x,c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg)),
% 0.75/0.55 inference(cnf_transformation,[status(thm)],[f2832])).
% 0.75/0.55 fof(f6338,plain,(
% 0.75/0.55 ~c_in(v_x,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg)),
% 0.75/0.55 inference(resolution,[status(thm)],[f6057,f6292])).
% 0.75/0.55 fof(f6353,plain,(
% 0.75/0.55 ~c_in(v_x,c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg)),
% 0.75/0.55 inference(resolution,[status(thm)],[f6059,f6292])).
% 0.75/0.55 fof(f7075,plain,(
% 0.75/0.55 ![X0,X1,X2]: (~c_in(X0,c_Message_Oanalz(c_union(c_Message_Osynth(X1),X2,tc_Message_Omsg)),tc_Message_Omsg)|c_in(X0,c_Message_Osynth(X1),tc_Message_Omsg)|c_in(X0,c_Message_Oanalz(c_union(X1,X2,tc_Message_Omsg)),tc_Message_Omsg))),
% 0.75/0.55 inference(paramodulation,[status(thm)],[f6286,f6055])).
% 0.75/0.55 fof(f12868,plain,(
% 0.75/0.55 c_in(v_x,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg)|c_in(v_x,c_Message_Oanalz(c_union(c_Message_Oanalz(v_G),v_H,tc_Message_Omsg)),tc_Message_Omsg)),
% 0.75/0.56 inference(resolution,[status(thm)],[f7075,f6291])).
% 0.75/0.56 fof(f12896,definition,(
% 0.75/0.56 sQ30_spl <=> (c_in(v_x,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg))),
% 0.75/0.56 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.75/0.56 fof(f12897,plain,(
% 0.75/0.56 c_in(v_x,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg)|~sQ30_spl),
% 0.75/0.56 inference(component_clause,[status(thm)],[f12896])).
% 0.75/0.56 fof(f12899,definition,(
% 0.75/0.56 sQ31_spl <=> (c_in(v_x,c_Message_Oanalz(c_union(c_Message_Oanalz(v_G),v_H,tc_Message_Omsg)),tc_Message_Omsg))),
% 0.75/0.56 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.75/0.56 fof(f12900,plain,(
% 0.75/0.56 c_in(v_x,c_Message_Oanalz(c_union(c_Message_Oanalz(v_G),v_H,tc_Message_Omsg)),tc_Message_Omsg)|~sQ31_spl),
% 0.75/0.56 inference(component_clause,[status(thm)],[f12899])).
% 0.75/0.56 fof(f12902,plain,(
% 0.75/0.56 sQ30_spl|sQ31_spl),
% 0.75/0.56 inference(split_clause,[status(thm)],[f12868,f12896,f12899])).
% 0.75/0.56 fof(f12914,plain,(
% 0.75/0.56 $false|~sQ30_spl),
% 0.75/0.56 inference(forward_subsumption_resolution,[status(thm)],[f12897,f6338])).
% 0.75/0.56 fof(f12915,plain,(
% 0.75/0.56 ~sQ30_spl),
% 0.75/0.56 inference(contradiction_clause,[status(thm)],[f12914])).
% 0.75/0.56 fof(f12916,plain,(
% 0.75/0.56 c_in(v_x,c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg)|~sQ31_spl),
% 0.75/0.56 inference(forward_demodulation,[status(thm)],[f6283,f12900])).
% 0.75/0.56 fof(f12917,plain,(
% 0.75/0.56 $false|~sQ31_spl),
% 0.75/0.56 inference(forward_subsumption_resolution,[status(thm)],[f12916,f6353])).
% 0.75/0.56 fof(f12918,plain,(
% 0.75/0.56 ~sQ31_spl),
% 0.75/0.56 inference(contradiction_clause,[status(thm)],[f12917])).
% 0.75/0.56 fof(f12919,plain,(
% 0.75/0.56 $false),
% 0.75/0.56 inference(sat_refutation,[status(thm)],[f12902,f12915,f12918])).
% 0.75/0.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.75/0.60 % Elapsed time: 0.294812 seconds
% 0.75/0.60 % CPU time: 1.648030 seconds
% 0.75/0.60 % Total memory used: 252.380 MB
% 0.75/0.60 % Net memory used: 250.856 MB
%------------------------------------------------------------------------------