%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV251-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 52.42s 7.25s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV251-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n026.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 08:38:52 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.35/0.59 % Drodi V4.1.1
% 52.42/7.25 % Refutation found
% 52.42/7.25 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 52.42/7.25 % SZS output start CNFRefutation for theBenchmark
% 52.42/7.25 fof(f111,axiom,(
% 52.42/7.25 (![V_B,V_A,T_a]: (( ~ c_lessequals(V_B,V_A,tc_set(T_a))| ~ c_lessequals(V_A,V_B,tc_set(T_a))| V_A = V_B ) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f112,axiom,(
% 52.42/7.25 (![V_A,T_a]: (c_lessequals(V_A,V_A,tc_set(T_a)) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2574,axiom,(
% 52.42/7.25 (![V_A,V_B,T_a]: (c_uminus(c_minus(V_A,V_B,tc_set(T_a)),tc_set(T_a)) = c_union(c_uminus(V_A,tc_set(T_a)),V_B,T_a) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2577,axiom,(
% 52.42/7.25 (![V_A,V_B,T_a]: (c_uminus(c_union(V_A,V_B,T_a),tc_set(T_a)) = c_inter(c_uminus(V_A,tc_set(T_a)),c_uminus(V_B,tc_set(T_a)),T_a) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2630,axiom,(
% 52.42/7.25 (![V_B,V_A,T_a]: (c_union(c_minus(V_B,V_A,tc_set(T_a)),V_A,T_a) = c_union(V_B,V_A,T_a) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2631,axiom,(
% 52.42/7.25 (![V_A,V_B,T_a]: (c_union(V_A,c_minus(V_B,V_A,tc_set(T_a)),T_a) = c_union(V_A,V_B,T_a) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2641,axiom,(
% 52.42/7.25 (![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) ) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2643,axiom,(
% 52.42/7.25 (![V_a,V_B,T_a,V_C]: (c_union(c_insert(V_a,V_B,T_a),V_C,T_a) = c_insert(V_a,c_union(V_B,V_C,T_a),T_a) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2644,axiom,(
% 52.42/7.25 (![V_A,V_a,V_B,T_a]: (c_union(V_A,c_insert(V_a,V_B,T_a),T_a) = c_insert(V_a,c_union(V_A,V_B,T_a),T_a) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2667,axiom,(
% 52.42/7.25 (![V_y,T_a]: (c_uminus(c_uminus(V_y,tc_set(T_a)),tc_set(T_a)) = V_y ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2689,axiom,(
% 52.42/7.25 (![V_x,V_A,T_a,V_B]: (( ~ c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a))| c_lessequals(V_A,V_B,tc_set(T_a)) ) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2690,axiom,(
% 52.42/7.25 (![V_x,V_B,T_a,V_A]: (( ~ c_in(V_x,V_B,T_a)| ~ c_lessequals(V_A,V_B,tc_set(T_a))| c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a)) ) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2771,axiom,(
% 52.42/7.25 (![V_A,V_B,T_a]: (c_union(V_A,c_union(V_B,V_A,T_a),T_a) = c_union(V_B,V_A,T_a) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2787,axiom,(
% 52.42/7.25 (![V_X,V_H]: (( ~ c_in(V_X,V_H,tc_Message_Omsg)| c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg) ) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2823,axiom,(
% 52.42/7.25 (![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)) ))),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2829,negated_conjecture,(
% 52.42/7.25 c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg) ),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2830,negated_conjecture,(
% 52.42/7.25 c_in(v_x,c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),tc_Message_Omsg) ),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2831,negated_conjecture,(
% 52.42/7.25 ~ 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) ),
% 52.42/7.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 52.42/7.25 fof(f2974,plain,(
% 52.42/7.25 ![V_B,V_A]: ((![T_a]: (~c_lessequals(V_B,V_A,tc_set(T_a))|~c_lessequals(V_A,V_B,tc_set(T_a))))|V_A=V_B)),
% 52.42/7.25 inference(miniscoping,[status(thm)],[f111])).
% 52.42/7.25 fof(f2975,plain,(
% 52.42/7.25 ![X0,X1,X2]: (~c_lessequals(X0,X1,tc_set(X2))|~c_lessequals(X1,X0,tc_set(X2))|X1=X0)),
% 52.42/7.25 inference(cnf_transformation,[status(thm)],[f2974])).
% 52.42/7.25 fof(f2976,plain,(
% 52.42/7.25 ![X0,X1]: (c_lessequals(X0,X0,tc_set(X1)))),
% 52.42/7.25 inference(cnf_transformation,[status(thm)],[f112])).
% 52.42/7.25 fof(f5972,plain,(
% 52.42/7.25 ![X0,X1,X2]: (c_uminus(c_minus(X0,X1,tc_set(X2)),tc_set(X2))=c_union(c_uminus(X0,tc_set(X2)),X1,X2))),
% 52.42/7.25 inference(cnf_transformation,[status(thm)],[f2574])).
% 52.42/7.26 fof(f5975,plain,(
% 52.42/7.26 ![X0,X1,X2]: (c_uminus(c_union(X0,X1,X2),tc_set(X2))=c_inter(c_uminus(X0,tc_set(X2)),c_uminus(X1,tc_set(X2)),X2))),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2577])).
% 52.42/7.26 fof(f6041,plain,(
% 52.42/7.26 ![X0,X1,X2]: (c_union(c_minus(X0,X1,tc_set(X2)),X1,X2)=c_union(X0,X1,X2))),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2630])).
% 52.42/7.26 fof(f6042,plain,(
% 52.42/7.26 ![X0,X1,X2]: (c_union(X0,c_minus(X1,X0,tc_set(X2)),X2)=c_union(X0,X1,X2))),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2631])).
% 52.42/7.26 fof(f6055,plain,(
% 52.42/7.26 ![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)))),
% 52.42/7.26 inference(miniscoping,[status(thm)],[f2641])).
% 52.42/7.26 fof(f6056,plain,(
% 52.42/7.26 ![X0,X1,X2,X3]: (~c_in(X0,X1,X2)|c_in(X0,c_union(X1,X3,X2),X2))),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f6055])).
% 52.42/7.26 fof(f6059,plain,(
% 52.42/7.26 ![X0,X1,X2,X3]: (c_union(c_insert(X0,X1,X2),X3,X2)=c_insert(X0,c_union(X1,X3,X2),X2))),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2643])).
% 52.42/7.26 fof(f6060,plain,(
% 52.42/7.26 ![X0,X1,X2,X3]: (c_union(X0,c_insert(X1,X2,X3),X3)=c_insert(X1,c_union(X0,X2,X3),X3))),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2644])).
% 52.42/7.26 fof(f6092,plain,(
% 52.42/7.26 ![X0,X1]: (c_uminus(c_uminus(X0,tc_set(X1)),tc_set(X1))=X0)),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2667])).
% 52.42/7.26 fof(f6123,plain,(
% 52.42/7.26 ![V_A,T_a,V_B]: ((![V_x]: ~c_lessequals(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a)))|c_lessequals(V_A,V_B,tc_set(T_a)))),
% 52.42/7.26 inference(miniscoping,[status(thm)],[f2689])).
% 52.42/7.26 fof(f6124,plain,(
% 52.42/7.26 ![X0,X1,X2,X3]: (~c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2))|c_lessequals(X1,X3,tc_set(X2)))),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f6123])).
% 52.42/7.26 fof(f6125,plain,(
% 52.42/7.26 ![X0,X1,X2,X3]: (~c_in(X0,X1,X2)|~c_lessequals(X3,X1,tc_set(X2))|c_lessequals(c_insert(X0,X3,X2),X1,tc_set(X2)))),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2690])).
% 52.42/7.26 fof(f6222,plain,(
% 52.42/7.26 ![X0,X1,X2]: (c_union(X0,c_union(X1,X0,X2),X2)=c_union(X1,X0,X2))),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2771])).
% 52.42/7.26 fof(f6243,plain,(
% 52.42/7.26 ![X0,X1]: (~c_in(X0,X1,tc_Message_Omsg)|c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg))),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2787])).
% 52.42/7.26 fof(f6282,plain,(
% 52.42/7.26 ![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)))),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2823])).
% 52.42/7.26 fof(f6288,plain,(
% 52.42/7.26 c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg)),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2829])).
% 52.42/7.26 fof(f6289,plain,(
% 52.42/7.26 c_in(v_x,c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),tc_Message_Omsg)),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2830])).
% 52.42/7.26 fof(f6290,plain,(
% 52.42/7.26 ~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)),
% 52.42/7.26 inference(cnf_transformation,[status(thm)],[f2831])).
% 52.42/7.26 fof(f6320,plain,(
% 52.42/7.26 ![X0]: (c_in(v_x,c_union(c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),X0,tc_Message_Omsg),tc_Message_Omsg))),
% 52.42/7.26 inference(resolution,[status(thm)],[f6056,f6289])).
% 52.42/7.26 fof(f6392,plain,(
% 52.42/7.26 ![X0]: (c_in(v_x,c_Message_Oanalz(c_union(c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),X0,tc_Message_Omsg)),tc_Message_Omsg))),
% 52.42/7.26 inference(resolution,[status(thm)],[f6243,f6320])).
% 52.42/7.26 fof(f6796,plain,(
% 52.42/7.26 ![X0,X1,X2,X3]: (c_union(c_insert(X0,X1,X2),X3,X2)=c_union(X1,c_insert(X0,X3,X2),X2))),
% 52.42/7.26 inference(backward_demodulation,[status(thm)],[f6060,f6059])).
% 52.42/7.26 fof(f7263,plain,(
% 52.42/7.26 ![X0]: (~c_lessequals(X0,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg))|c_lessequals(c_insert(v_X,X0,tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)))),
% 52.42/7.26 inference(resolution,[status(thm)],[f6125,f6288])).
% 52.42/7.26 fof(f9934,plain,(
% 52.42/7.26 ![X0]: (c_in(v_x,c_Message_Oanalz(c_union(c_insert(v_X,v_H,tc_Message_Omsg),X0,tc_Message_Omsg)),tc_Message_Omsg))),
% 52.42/7.26 inference(forward_demodulation,[status(thm)],[f6282,f6392])).
% 52.42/7.26 fof(f9935,plain,(
% 52.42/7.26 ![X0]: (c_in(v_x,c_Message_Oanalz(c_union(v_H,c_insert(v_X,X0,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg))),
% 52.42/7.26 inference(forward_demodulation,[status(thm)],[f6796,f9934])).
% 44.99/7.36 fof(f13074,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_lessequals(X0,c_insert(X1,X0,X2),tc_set(X2)))),
% 44.99/7.36 inference(resolution,[status(thm)],[f2976,f6124])).
% 44.99/7.36 fof(f13076,plain,(
% 44.99/7.36 c_lessequals(c_insert(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg))),
% 44.99/7.36 inference(resolution,[status(thm)],[f2976,f7263])).
% 44.99/7.36 fof(f14981,plain,(
% 44.99/7.36 ![X0,X1,X2]: (~c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2))|X1=c_insert(X0,X1,X2))),
% 44.99/7.36 inference(resolution,[status(thm)],[f13074,f2975])).
% 44.99/7.36 fof(f44218,plain,(
% 44.99/7.36 c_Message_Osynth(c_Message_Oanalz(v_G))=c_insert(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg)),
% 44.99/7.36 inference(resolution,[status(thm)],[f13076,f14981])).
% 44.99/7.36 fof(f44641,plain,(
% 44.99/7.36 c_in(v_x,c_Message_Oanalz(c_union(v_H,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg)),tc_Message_Omsg)),
% 44.99/7.36 inference(paramodulation,[status(thm)],[f44218,f9935])).
% 44.99/7.36 fof(f53289,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_uminus(c_union(c_uminus(X0,tc_set(X1)),X2,X1),tc_set(X1))=c_minus(X0,X2,tc_set(X1)))),
% 44.99/7.36 inference(paramodulation,[status(thm)],[f5972,f6092])).
% 44.99/7.36 fof(f53306,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_uminus(c_union(c_uminus(X0,tc_set(X1)),X2,X1),tc_set(X1))=c_inter(X0,c_uminus(X2,tc_set(X1)),X1))),
% 44.99/7.36 inference(paramodulation,[status(thm)],[f6092,f5975])).
% 44.99/7.36 fof(f63423,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_uminus(c_union(X0,X1,X2),tc_set(X2))=c_minus(c_uminus(X0,tc_set(X2)),X1,tc_set(X2)))),
% 44.99/7.36 inference(backward_demodulation,[status(thm)],[f63425,f5975])).
% 44.99/7.36 fof(f63425,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_minus(X0,X1,tc_set(X2))=c_inter(X0,c_uminus(X1,tc_set(X2)),X2))),
% 44.99/7.36 inference(forward_demodulation,[status(thm)],[f53289,f53306])).
% 44.99/7.36 fof(f64355,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_union(X0,c_uminus(c_union(X1,X0,X2),tc_set(X2)),X2)=c_union(X0,c_uminus(X1,tc_set(X2)),X2))),
% 44.99/7.36 inference(paramodulation,[status(thm)],[f63423,f6042])).
% 44.99/7.36 fof(f64356,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_union(c_uminus(c_union(X0,X1,X2),tc_set(X2)),X1,X2)=c_union(c_uminus(X0,tc_set(X2)),X1,X2))),
% 44.99/7.36 inference(paramodulation,[status(thm)],[f63423,f6041])).
% 44.99/7.36 fof(f69720,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_union(X0,c_uminus(c_union(c_uminus(X1,tc_set(X2)),X0,X2),tc_set(X2)),X2)=c_union(X0,c_uminus(c_uminus(c_union(X1,X0,X2),tc_set(X2)),tc_set(X2)),X2))),
% 44.99/7.36 inference(paramodulation,[status(thm)],[f64356,f64355])).
% 44.99/7.36 fof(f69865,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_union(X0,c_uminus(c_uminus(X1,tc_set(X2)),tc_set(X2)),X2)=c_union(X0,c_uminus(c_uminus(c_union(X1,X0,X2),tc_set(X2)),tc_set(X2)),X2))),
% 44.99/7.36 inference(forward_demodulation,[status(thm)],[f64355,f69720])).
% 44.99/7.36 fof(f69866,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_union(X0,X1,X2)=c_union(X0,c_uminus(c_uminus(c_union(X1,X0,X2),tc_set(X2)),tc_set(X2)),X2))),
% 44.99/7.36 inference(forward_demodulation,[status(thm)],[f6092,f69865])).
% 44.99/7.36 fof(f69867,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_union(X0,X1,X2)=c_union(X0,c_union(X1,X0,X2),X2))),
% 44.99/7.36 inference(forward_demodulation,[status(thm)],[f6092,f69866])).
% 44.99/7.36 fof(f70796,plain,(
% 44.99/7.36 ![X0,X1,X2]: (c_union(X0,X1,X2)=c_union(X1,X0,X2))),
% 44.99/7.36 inference(paramodulation,[status(thm)],[f6222,f69867])).
% 44.99/7.36 fof(f71437,plain,(
% 44.99/7.36 ~c_in(v_x,c_Message_Oanalz(c_union(v_H,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg)),tc_Message_Omsg)),
% 44.99/7.36 inference(paramodulation,[status(thm)],[f70796,f6290])).
% 44.99/7.36 fof(f72154,plain,(
% 44.99/7.36 $false),
% 44.99/7.36 inference(forward_subsumption_resolution,[status(thm)],[f71437,f44641])).
% 44.99/7.36 % SZS output end CNFRefutation for theBenchmark.p
% 3.74/7.46 % Elapsed time: 7.003943 seconds
% 3.74/7.46 % CPU time: 53.704461 seconds
% 3.74/7.46 % Total memory used: 1.082 GB
% 3.74/7.46 % Net memory used: 1.053 GB
%------------------------------------------------------------------------------