%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV252-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 : n010.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 150.51s 24.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV252-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/5.42 % Computer : n010.cluster.edu
% 0.15/5.42 % Model : x86_64 x86_64
% 0.15/5.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.42 % Memory : 8046.5625MB
% 0.15/5.42 % OS : Linux 6.8.0-71-generic
% 0.15/5.43 % CPULimit : 300
% 0.15/5.43 % WCLimit : 300
% 0.15/5.43 % DateTime : Mon Sep 21 08:37:00 UTC 2026
% 0.15/5.43 % CPUTime :
% 0.20/5.53 % Drodi V4.1.1
% 150.51/24.58 % Refutation found
% 150.51/24.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 150.51/24.58 % SZS output start CNFRefutation for theBenchmark
% 150.51/24.58 fof(f111,axiom,(
% 150.51/24.58 (![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 ) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f112,axiom,(
% 150.51/24.58 (![V_A,T_a]: (c_lessequals(V_A,V_A,tc_set(T_a)) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2645,axiom,(
% 150.51/24.58 (![V_A,V_B,T_a,V_C]: (( ~ c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a))| c_lessequals(V_A,V_C,tc_set(T_a)) ) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2646,axiom,(
% 150.51/24.58 (![V_A,V_B,T_a,V_C]: (( ~ c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a))| c_lessequals(V_B,V_C,tc_set(T_a)) ) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2647,axiom,(
% 150.51/24.58 (![V_B,V_C,T_a,V_A]: (( ~ c_lessequals(V_B,V_C,tc_set(T_a))| ~ c_lessequals(V_A,V_C,tc_set(T_a))| c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a)) ) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2690,axiom,(
% 150.51/24.58 (![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)) ) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2767,axiom,(
% 150.51/24.58 (![V_X,V_H]: (( ~ c_in(V_X,V_H,tc_Message_Omsg)| c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2799,axiom,(
% 150.51/24.58 (![V_H]: (c_Message_Oanalz(c_Message_Oparts(V_H)) = c_Message_Oparts(V_H) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2800,axiom,(
% 150.51/24.58 (![V_G,V_H]: (( ~ c_lessequals(c_Message_Oanalz(V_G),c_Message_Oanalz(V_H),tc_set(tc_Message_Omsg))| c_lessequals(V_G,c_Message_Oanalz(V_H),tc_set(tc_Message_Omsg)) ) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2803,axiom,(
% 150.51/24.58 (![V_H]: (c_Message_Oparts(c_Message_Oanalz(V_H)) = c_Message_Oparts(V_H) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2814,axiom,(
% 150.51/24.58 (![V_G,V_H]: (( ~ c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_set(tc_Message_Omsg))| c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) ) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2815,axiom,(
% 150.51/24.58 (![V_G,V_H]: (( ~ c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg))| c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) ) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2827,axiom,(
% 150.51/24.58 (![V_H]: (c_Message_Oparts(c_Message_Osynth(V_H)) = c_union(c_Message_Oparts(V_H),c_Message_Osynth(V_H),tc_Message_Omsg) ))),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2828,negated_conjecture,(
% 150.51/24.58 c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg) ),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2829,negated_conjecture,(
% 150.51/24.58 ~ c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),tc_set(tc_Message_Omsg)) ),
% 150.51/24.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 150.51/24.58 fof(f2972,plain,(
% 150.51/24.58 ![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)),
% 150.51/24.58 inference(miniscoping,[status(thm)],[f111])).
% 150.51/24.58 fof(f2973,plain,(
% 150.51/24.58 ![X0,X1,X2]: (~c_lessequals(X0,X1,tc_set(X2))|~c_lessequals(X1,X0,tc_set(X2))|X1=X0)),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2972])).
% 150.51/24.58 fof(f2974,plain,(
% 150.51/24.58 ![X0,X1]: (c_lessequals(X0,X0,tc_set(X1)))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f112])).
% 150.51/24.58 fof(f6059,plain,(
% 150.51/24.58 ![V_A,T_a,V_C]: ((![V_B]: ~c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a)))|c_lessequals(V_A,V_C,tc_set(T_a)))),
% 150.51/24.58 inference(miniscoping,[status(thm)],[f2645])).
% 150.51/24.58 fof(f6060,plain,(
% 150.51/24.58 ![X0,X1,X2,X3]: (~c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2))|c_lessequals(X0,X3,tc_set(X2)))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f6059])).
% 150.51/24.58 fof(f6061,plain,(
% 150.51/24.58 ![V_B,T_a,V_C]: ((![V_A]: ~c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a)))|c_lessequals(V_B,V_C,tc_set(T_a)))),
% 150.51/24.58 inference(miniscoping,[status(thm)],[f2646])).
% 150.51/24.58 fof(f6062,plain,(
% 150.51/24.58 ![X0,X1,X2,X3]: (~c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2))|c_lessequals(X1,X3,tc_set(X2)))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f6061])).
% 150.51/24.58 fof(f6063,plain,(
% 150.51/24.58 ![X0,X1,X2,X3]: (~c_lessequals(X0,X1,tc_set(X2))|~c_lessequals(X3,X1,tc_set(X2))|c_lessequals(c_union(X3,X0,X2),X1,tc_set(X2)))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2647])).
% 150.51/24.58 fof(f6123,plain,(
% 150.51/24.58 ![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)))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2690])).
% 150.51/24.58 fof(f6216,plain,(
% 150.51/24.58 ![X0,X1]: (~c_in(X0,X1,tc_Message_Omsg)|c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2767])).
% 150.51/24.58 fof(f6255,plain,(
% 150.51/24.58 ![X0]: (c_Message_Oanalz(c_Message_Oparts(X0))=c_Message_Oparts(X0))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2799])).
% 150.51/24.58 fof(f6256,plain,(
% 150.51/24.58 ![X0,X1]: (~c_lessequals(c_Message_Oanalz(X0),c_Message_Oanalz(X1),tc_set(tc_Message_Omsg))|c_lessequals(X0,c_Message_Oanalz(X1),tc_set(tc_Message_Omsg)))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2800])).
% 150.51/24.58 fof(f6260,plain,(
% 150.51/24.58 ![X0]: (c_Message_Oparts(c_Message_Oanalz(X0))=c_Message_Oparts(X0))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2803])).
% 150.51/24.58 fof(f6271,plain,(
% 150.51/24.58 ![X0,X1]: (~c_lessequals(c_Message_Oparts(X0),c_Message_Oparts(X1),tc_set(tc_Message_Omsg))|c_lessequals(X0,c_Message_Oparts(X1),tc_set(tc_Message_Omsg)))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2814])).
% 150.51/24.58 fof(f6272,plain,(
% 150.51/24.58 ![X0,X1]: (~c_lessequals(X0,c_Message_Oparts(X1),tc_set(tc_Message_Omsg))|c_lessequals(c_Message_Oparts(X0),c_Message_Oparts(X1),tc_set(tc_Message_Omsg)))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2815])).
% 150.51/24.58 fof(f6285,plain,(
% 150.51/24.58 ![X0]: (c_Message_Oparts(c_Message_Osynth(X0))=c_union(c_Message_Oparts(X0),c_Message_Osynth(X0),tc_Message_Omsg))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2827])).
% 150.51/24.58 fof(f6286,plain,(
% 150.51/24.58 c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg)),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2828])).
% 150.51/24.58 fof(f6287,plain,(
% 150.51/24.58 ~c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Osynth(c_Message_Oanalz(v_H)),c_Message_Oparts(v_H),tc_Message_Omsg),tc_set(tc_Message_Omsg))),
% 150.51/24.58 inference(cnf_transformation,[status(thm)],[f2829])).
% 150.51/24.58 fof(f6452,plain,(
% 150.51/24.58 ![X0,X1,X2]: (c_lessequals(X0,c_union(X0,X1,X2),tc_set(X2)))),
% 150.51/24.58 inference(resolution,[status(thm)],[f6060,f2974])).
% 150.51/24.58 fof(f6508,plain,(
% 150.51/24.58 ![X0,X1,X2]: (c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2)))),
% 150.51/24.58 inference(resolution,[status(thm)],[f6062,f2974])).
% 150.51/24.58 fof(f6630,plain,(
% 150.51/24.58 ![X0,X1,X2,X3]: (~c_lessequals(X0,c_union(X1,X2,X3),tc_set(X3))|c_lessequals(c_union(X0,X1,X3),c_union(X1,X2,X3),tc_set(X3)))),
% 150.51/24.58 inference(resolution,[status(thm)],[f6452,f6063])).
% 150.51/24.58 fof(f6793,plain,(
% 150.51/24.58 c_in(v_X,c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(v_H))),tc_Message_Omsg)),
% 150.51/24.58 inference(resolution,[status(thm)],[f6216,f6286])).
% 150.51/24.58 fof(f6819,plain,(
% 150.51/24.58 ![X0]: (~c_lessequals(X0,c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(v_H))),tc_set(tc_Message_Omsg))|c_lessequals(c_insert(v_X,X0,tc_Message_Omsg),c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(v_H))),tc_set(tc_Message_Omsg)))),
% 150.51/24.58 inference(resolution,[status(thm)],[f6793,f6123])).
% 150.51/24.58 fof(f6955,plain,(
% 150.51/24.58 ![X0,X1]: (~c_lessequals(c_Message_Oanalz(X0),c_Message_Oparts(X1),tc_set(tc_Message_Omsg))|c_lessequals(X0,c_Message_Oanalz(c_Message_Oparts(X1)),tc_set(tc_Message_Omsg)))),
% 150.51/24.58 inference(paramodulation,[status(thm)],[f6255,f6256])).
% 150.51/24.58 fof(f6958,plain,(
% 150.51/24.58 ![X0,X1]: (~c_lessequals(c_Message_Oanalz(X0),c_Message_Oparts(X1),tc_set(tc_Message_Omsg))|c_lessequals(X0,c_Message_Oparts(X1),tc_set(tc_Message_Omsg)))),
% 150.51/24.58 inference(forward_demodulation,[status(thm)],[f6255,f6955])).
% 150.51/24.58 fof(f7388,plain,(
% 150.51/24.58 ![X0]: (c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(X0)))=c_union(c_Message_Oparts(X0),c_Message_Osynth(c_Message_Oanalz(X0)),tc_Message_Omsg))),
% 150.51/24.58 inference(paramodulation,[status(thm)],[f6260,f6285])).
% 119.16/24.76 fof(f7400,plain,(
% 119.16/24.76 ![X0]: (c_lessequals(c_Message_Oparts(X0),c_Message_Oparts(c_Message_Osynth(X0)),tc_set(tc_Message_Omsg)))),
% 119.16/24.76 inference(paramodulation,[status(thm)],[f6285,f6452])).
% 119.16/24.76 fof(f22580,plain,(
% 119.16/24.76 ![X0]: (c_lessequals(X0,c_Message_Oparts(c_Message_Osynth(X0)),tc_set(tc_Message_Omsg)))),
% 119.16/24.76 inference(resolution,[status(thm)],[f7400,f6271])).
% 119.16/24.76 fof(f22637,plain,(
% 119.16/24.76 ![X0]: (c_lessequals(X0,c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(X0))),tc_set(tc_Message_Omsg)))),
% 119.16/24.76 inference(resolution,[status(thm)],[f22580,f6958])).
% 119.16/24.76 fof(f28412,plain,(
% 119.16/24.76 ![X0,X1,X2]: (c_lessequals(c_union(X0,X1,X2),c_union(X1,X0,X2),tc_set(X2)))),
% 119.16/24.76 inference(resolution,[status(thm)],[f6630,f6508])).
% 119.16/24.76 fof(f37799,plain,(
% 119.16/24.76 c_lessequals(c_insert(v_X,v_H,tc_Message_Omsg),c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(v_H))),tc_set(tc_Message_Omsg))),
% 119.16/24.76 inference(resolution,[status(thm)],[f22637,f6819])).
% 119.16/24.76 fof(f58725,plain,(
% 119.16/24.76 ![X0,X1,X2]: (~c_lessequals(c_union(X0,X1,X2),c_union(X1,X0,X2),tc_set(X2))|c_union(X1,X0,X2)=c_union(X0,X1,X2))),
% 119.16/24.76 inference(resolution,[status(thm)],[f28412,f2973])).
% 119.16/24.76 fof(f58805,plain,(
% 119.16/24.76 ![X0,X1,X2]: (c_union(X0,X1,X2)=c_union(X1,X0,X2))),
% 119.16/24.76 inference(forward_subsumption_resolution,[status(thm)],[f58725,f28412])).
% 119.16/24.76 fof(f59009,plain,(
% 119.16/24.76 ~c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_union(c_Message_Oparts(v_H),c_Message_Osynth(c_Message_Oanalz(v_H)),tc_Message_Omsg),tc_set(tc_Message_Omsg))),
% 119.16/24.76 inference(backward_demodulation,[status(thm)],[f58805,f6287])).
% 119.16/24.76 fof(f59796,plain,(
% 119.16/24.76 ~c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(v_H))),tc_set(tc_Message_Omsg))),
% 119.16/24.76 inference(forward_demodulation,[status(thm)],[f7388,f59009])).
% 119.16/24.76 fof(f107443,plain,(
% 119.16/24.76 c_lessequals(c_Message_Oparts(c_insert(v_X,v_H,tc_Message_Omsg)),c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(v_H))),tc_set(tc_Message_Omsg))),
% 119.16/24.76 inference(resolution,[status(thm)],[f37799,f6272])).
% 119.16/24.76 fof(f107468,plain,(
% 119.16/24.76 $false),
% 119.16/24.76 inference(forward_subsumption_resolution,[status(thm)],[f107443,f59796])).
% 119.16/24.76 % SZS output end CNFRefutation for theBenchmark.p
% 10.46/25.27 % Elapsed time: 19.825174 seconds
% 10.46/25.27 % CPU time: 153.202077 seconds
% 10.46/25.27 % Total memory used: 2.181 GB
% 10.46/25.27 % Net memory used: 2.125 GB
%------------------------------------------------------------------------------