%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET837-2 : 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 : 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:12:42 PM UTC 2026
% Result : Unsatisfiable 9.08s 1.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET837-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.53 % Computer : n026.cluster.edu
% 0.09/0.53 % Model : x86_64 x86_64
% 0.09/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.53 % Memory : 8046.5625MB
% 0.09/0.53 % OS : Linux 6.8.0-71-generic
% 0.09/0.53 % CPULimit : 300
% 0.09/0.53 % WCLimit : 300
% 0.09/0.53 % DateTime : Mon Sep 21 05:43:08 UTC 2026
% 0.09/0.53 % CPUTime :
% 0.09/0.54 % Drodi V4.1.1
% 9.08/1.76 % Refutation found
% 9.08/1.76 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.08/1.76 % SZS output start CNFRefutation for theBenchmark
% 9.08/1.76 fof(f1,negated_conjecture,(
% 9.08/1.76 ( v_X = c_union(v_Y,v_Z,t_a)| c_lessequals(v_Y,v_X,tc_set(t_a)) ) ),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f2,negated_conjecture,(
% 9.08/1.76 ( v_X = c_union(v_Y,v_Z,t_a)| c_lessequals(v_Z,v_X,tc_set(t_a)) ) ),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f3,negated_conjecture,(
% 9.08/1.76 ( c_lessequals(v_Y,v_x,tc_set(t_a))| ~ c_lessequals(v_Z,v_X,tc_set(t_a))| ~ c_lessequals(v_Y,v_X,tc_set(t_a))| v_X != c_union(v_Y,v_Z,t_a) ) ),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f4,negated_conjecture,(
% 9.08/1.76 ( c_lessequals(v_Z,v_x,tc_set(t_a))| ~ c_lessequals(v_Z,v_X,tc_set(t_a))| ~ c_lessequals(v_Y,v_X,tc_set(t_a))| v_X != c_union(v_Y,v_Z,t_a) ) ),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f5,negated_conjecture,(
% 9.08/1.76 ( ~ c_lessequals(v_X,v_x,tc_set(t_a))| ~ c_lessequals(v_Z,v_X,tc_set(t_a))| ~ c_lessequals(v_Y,v_X,tc_set(t_a))| v_X != c_union(v_Y,v_Z,t_a) ) ),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f6,negated_conjecture,(
% 9.08/1.76 (![V_U]: (( v_X = c_union(v_Y,v_Z,t_a)| c_lessequals(v_X,V_U,tc_set(t_a))| ~ c_lessequals(v_Z,V_U,tc_set(t_a))| ~ c_lessequals(v_Y,V_U,tc_set(t_a)) ) ))),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f7,axiom,(
% 9.08/1.76 (![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) ) ))),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f8,axiom,(
% 9.08/1.76 (![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) ) ))),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f9,axiom,(
% 9.08/1.76 (![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) ) ))),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f10,axiom,(
% 9.08/1.76 (![V_c,V_A,T_a,V_B]: (( ~ c_in(V_c,V_A,T_a)| ~ c_lessequals(V_A,V_B,tc_set(T_a))| c_in(V_c,V_B,T_a) ) ))),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f11,axiom,(
% 9.08/1.76 (![V_A,V_B,T_a]: (( c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a)| c_lessequals(V_A,V_B,tc_set(T_a)) ) ))),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f12,axiom,(
% 9.08/1.76 (![V_A,V_B,T_a]: (( ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a)| c_lessequals(V_A,V_B,tc_set(T_a)) ) ))),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f13,axiom,(
% 9.08/1.76 (![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 ) ))),
% 9.08/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.08/1.76 fof(f14,plain,(
% 9.08/1.76 v_X=c_union(v_Y,v_Z,t_a)|c_lessequals(v_Y,v_X,tc_set(t_a))),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f1])).
% 9.08/1.76 fof(f15,plain,(
% 9.08/1.76 v_X=c_union(v_Y,v_Z,t_a)|c_lessequals(v_Z,v_X,tc_set(t_a))),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f2])).
% 9.08/1.76 fof(f16,plain,(
% 9.08/1.76 c_lessequals(v_Y,v_x,tc_set(t_a))|~c_lessequals(v_Z,v_X,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))|~v_X=c_union(v_Y,v_Z,t_a)),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f3])).
% 9.08/1.76 fof(f17,plain,(
% 9.08/1.76 c_lessequals(v_Z,v_x,tc_set(t_a))|~c_lessequals(v_Z,v_X,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))|~v_X=c_union(v_Y,v_Z,t_a)),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f4])).
% 9.08/1.76 fof(f18,plain,(
% 9.08/1.76 ~c_lessequals(v_X,v_x,tc_set(t_a))|~c_lessequals(v_Z,v_X,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))|~v_X=c_union(v_Y,v_Z,t_a)),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f5])).
% 9.08/1.76 fof(f19,plain,(
% 9.08/1.76 ![X0]: (v_X=c_union(v_Y,v_Z,t_a)|c_lessequals(v_X,X0,tc_set(t_a))|~c_lessequals(v_Z,X0,tc_set(t_a))|~c_lessequals(v_Y,X0,tc_set(t_a)))),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f6])).
% 9.08/1.76 fof(f20,plain,(
% 9.08/1.76 ![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)))),
% 9.08/1.76 inference(miniscoping,[status(thm)],[f7])).
% 9.08/1.76 fof(f21,plain,(
% 9.08/1.76 ![X0,X1,X2,X3]: (~c_in(X0,X1,X2)|c_in(X0,c_union(X3,X1,X2),X2))),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f20])).
% 9.08/1.76 fof(f22,plain,(
% 9.08/1.76 ![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)))),
% 9.08/1.76 inference(miniscoping,[status(thm)],[f8])).
% 9.08/1.76 fof(f23,plain,(
% 9.08/1.76 ![X0,X1,X2,X3]: (~c_in(X0,X1,X2)|c_in(X0,c_union(X1,X3,X2),X2))),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f22])).
% 9.08/1.76 fof(f24,plain,(
% 9.08/1.76 ![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))),
% 9.08/1.76 inference(miniscoping,[status(thm)],[f9])).
% 9.08/1.76 fof(f25,plain,(
% 9.08/1.76 ![X0,X1,X2,X3]: (~c_in(X0,c_union(X1,X2,X3),X3)|c_in(X0,X2,X3)|c_in(X0,X1,X3))),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f24])).
% 9.08/1.76 fof(f26,plain,(
% 9.08/1.76 ![V_c,T_a,V_B]: ((![V_A]: (~c_in(V_c,V_A,T_a)|~c_lessequals(V_A,V_B,tc_set(T_a))))|c_in(V_c,V_B,T_a))),
% 9.08/1.76 inference(miniscoping,[status(thm)],[f10])).
% 9.08/1.76 fof(f27,plain,(
% 9.08/1.76 ![X0,X1,X2,X3]: (~c_in(X0,X1,X2)|~c_lessequals(X1,X3,tc_set(X2))|c_in(X0,X3,X2))),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f26])).
% 9.08/1.76 fof(f28,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2)|c_lessequals(X0,X1,tc_set(X2)))),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f11])).
% 9.08/1.76 fof(f29,plain,(
% 9.08/1.76 ![X0,X1,X2]: (~c_in(c_Main_OsubsetI__1(X0,X1,X2),X1,X2)|c_lessequals(X0,X1,tc_set(X2)))),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f12])).
% 9.08/1.76 fof(f30,plain,(
% 9.08/1.76 ![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)),
% 9.08/1.76 inference(miniscoping,[status(thm)],[f13])).
% 9.08/1.76 fof(f31,plain,(
% 9.08/1.76 ![X0,X1,X2]: (~c_lessequals(X0,X1,tc_set(X2))|~c_lessequals(X1,X0,tc_set(X2))|X1=X0)),
% 9.08/1.76 inference(cnf_transformation,[status(thm)],[f30])).
% 9.08/1.76 fof(f43,plain,(
% 9.08/1.76 ![X0,X1,X2,X3]: (c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2))|c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X1,X2)|c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X0,X2))),
% 9.08/1.76 inference(resolution,[status(thm)],[f28,f25])).
% 9.08/1.76 fof(f45,plain,(
% 9.08/1.76 ![X0,X1,X2,X3]: (c_lessequals(X0,c_union(X1,X2,X3),tc_set(X3))|~c_in(c_Main_OsubsetI__1(X0,c_union(X1,X2,X3),X3),X1,X3))),
% 9.08/1.76 inference(resolution,[status(thm)],[f29,f23])).
% 9.08/1.76 fof(f46,plain,(
% 9.08/1.76 ![X0,X1,X2,X3]: (c_lessequals(X0,c_union(X1,X2,X3),tc_set(X3))|~c_in(c_Main_OsubsetI__1(X0,c_union(X1,X2,X3),X3),X2,X3))),
% 9.08/1.76 inference(resolution,[status(thm)],[f29,f21])).
% 9.08/1.76 fof(f47,plain,(
% 9.08/1.76 ![X0,X1,X2,X3]: (c_lessequals(X0,X1,tc_set(X2))|~c_in(c_Main_OsubsetI__1(X0,X1,X2),X3,X2)|~c_lessequals(X3,X1,tc_set(X2)))),
% 9.08/1.76 inference(resolution,[status(thm)],[f29,f27])).
% 9.08/1.76 fof(f52,plain,(
% 9.08/1.76 ![X0]: (c_lessequals(X0,v_X,tc_set(t_a))|~c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Z,t_a)|v_X=c_union(v_Y,v_Z,t_a))),
% 9.08/1.76 inference(resolution,[status(thm)],[f47,f15])).
% 9.08/1.76 fof(f53,plain,(
% 9.08/1.76 ![X0]: (c_lessequals(X0,v_X,tc_set(t_a))|~c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Y,t_a)|v_X=c_union(v_Y,v_Z,t_a))),
% 9.08/1.76 inference(resolution,[status(thm)],[f47,f14])).
% 9.08/1.76 fof(f55,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_lessequals(X0,c_union(X0,X1,X2),tc_set(X2))|c_lessequals(X0,c_union(X0,X1,X2),tc_set(X2)))),
% 9.08/1.76 inference(resolution,[status(thm)],[f45,f28])).
% 9.08/1.76 fof(f59,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_lessequals(X0,c_union(X0,X1,X2),tc_set(X2)))),
% 9.08/1.76 inference(duplicate_literals_removal,[status(thm)],[f55])).
% 9.08/1.76 fof(f64,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2))|c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2)))),
% 9.08/1.76 inference(resolution,[status(thm)],[f46,f28])).
% 9.08/1.76 fof(f68,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2)))),
% 9.08/1.76 inference(duplicate_literals_removal,[status(thm)],[f64])).
% 9.08/1.76 fof(f69,plain,(
% 9.08/1.76 ![X0]: (v_X=c_union(v_Y,v_Z,t_a)|c_lessequals(v_X,c_union(X0,v_Z,t_a),tc_set(t_a))|~c_lessequals(v_Y,c_union(X0,v_Z,t_a),tc_set(t_a)))),
% 9.08/1.76 inference(resolution,[status(thm)],[f68,f19])).
% 9.08/1.76 fof(f72,plain,(
% 9.08/1.76 ![X0,X1,X2]: (~c_lessequals(c_union(X0,X1,X2),X1,tc_set(X2))|X1=c_union(X0,X1,X2))),
% 9.08/1.76 inference(resolution,[status(thm)],[f68,f31])).
% 9.08/1.76 fof(f83,plain,(
% 9.08/1.76 ![X0,X1,X2,X3]: (c_lessequals(c_union(X0,X1,X2),c_union(X1,X3,X2),tc_set(X2))|c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),c_union(X1,X3,X2),X2),X0,X2)|c_lessequals(c_union(X0,X1,X2),c_union(X1,X3,X2),tc_set(X2)))),
% 9.08/1.76 inference(resolution,[status(thm)],[f43,f45])).
% 9.08/1.76 fof(f85,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_lessequals(c_union(X0,X1,X2),X1,tc_set(X2))|c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X1,X2),X0,X2)|c_lessequals(c_union(X0,X1,X2),X1,tc_set(X2)))),
% 9.08/1.76 inference(resolution,[status(thm)],[f43,f29])).
% 9.08/1.76 fof(f92,plain,(
% 9.08/1.76 ![X0,X1,X2,X3,X4]: (c_lessequals(c_union(c_union(X0,X1,X2),X3,X2),X4,tc_set(X2))|c_in(c_Main_OsubsetI__1(c_union(c_union(X0,X1,X2),X3,X2),X4,X2),X3,X2)|c_in(c_Main_OsubsetI__1(c_union(c_union(X0,X1,X2),X3,X2),X4,X2),X1,X2)|c_in(c_Main_OsubsetI__1(c_union(c_union(X0,X1,X2),X3,X2),X4,X2),X0,X2))),
% 9.08/1.76 inference(resolution,[status(thm)],[f43,f25])).
% 9.08/1.76 fof(f99,plain,(
% 9.08/1.76 ![X0,X1,X2,X3]: (c_lessequals(c_union(X0,X1,X2),c_union(X1,X3,X2),tc_set(X2))|c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),c_union(X1,X3,X2),X2),X0,X2))),
% 9.08/1.76 inference(duplicate_literals_removal,[status(thm)],[f83])).
% 9.08/1.76 fof(f101,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_lessequals(c_union(X0,X1,X2),X1,tc_set(X2))|c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X1,X2),X0,X2))),
% 9.08/1.76 inference(duplicate_literals_removal,[status(thm)],[f85])).
% 9.08/1.76 fof(f107,plain,(
% 9.08/1.76 ![X0]: (c_lessequals(c_union(v_Z,X0,t_a),v_X,tc_set(t_a))|v_X=c_union(v_Y,v_Z,t_a)|c_lessequals(c_union(v_Z,X0,t_a),v_X,tc_set(t_a))|c_in(c_Main_OsubsetI__1(c_union(v_Z,X0,t_a),v_X,t_a),X0,t_a))),
% 9.08/1.76 inference(resolution,[status(thm)],[f52,f43])).
% 9.08/1.76 fof(f113,plain,(
% 9.08/1.76 ![X0]: (c_lessequals(c_union(v_Z,X0,t_a),v_X,tc_set(t_a))|v_X=c_union(v_Y,v_Z,t_a)|c_in(c_Main_OsubsetI__1(c_union(v_Z,X0,t_a),v_X,t_a),X0,t_a))),
% 9.08/1.76 inference(duplicate_literals_removal,[status(thm)],[f107])).
% 9.08/1.76 fof(f312,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_lessequals(c_union(X0,c_union(X0,X1,X2),X2),c_union(X0,X1,X2),tc_set(X2))|c_lessequals(c_union(X0,c_union(X0,X1,X2),X2),c_union(X0,X1,X2),tc_set(X2)))),
% 9.08/1.76 inference(resolution,[status(thm)],[f101,f45])).
% 9.08/1.76 fof(f324,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_lessequals(c_union(X0,c_union(X0,X1,X2),X2),c_union(X0,X1,X2),tc_set(X2)))),
% 9.08/1.76 inference(duplicate_literals_removal,[status(thm)],[f312])).
% 9.08/1.76 fof(f419,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_union(X0,X1,X2)=c_union(X0,c_union(X0,X1,X2),X2))),
% 9.08/1.76 inference(resolution,[status(thm)],[f324,f72])).
% 9.08/1.76 fof(f660,plain,(
% 9.08/1.76 v_X=c_union(v_Y,v_Z,t_a)|c_lessequals(v_X,c_union(v_Y,v_Z,t_a),tc_set(t_a))),
% 9.08/1.76 inference(resolution,[status(thm)],[f69,f59])).
% 9.08/1.76 fof(f827,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_lessequals(c_union(X0,X1,X2),c_union(X1,X0,X2),tc_set(X2))|c_lessequals(c_union(X0,X1,X2),c_union(X1,X0,X2),tc_set(X2)))),
% 9.08/1.76 inference(resolution,[status(thm)],[f99,f46])).
% 9.08/1.76 fof(f849,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_lessequals(c_union(X0,X1,X2),c_union(X1,X0,X2),tc_set(X2)))),
% 9.08/1.76 inference(duplicate_literals_removal,[status(thm)],[f827])).
% 9.08/1.76 fof(f863,plain,(
% 9.08/1.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))),
% 9.08/1.76 inference(resolution,[status(thm)],[f849,f31])).
% 9.08/1.76 fof(f884,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_union(X0,X1,X2)=c_union(X1,X0,X2))),
% 9.08/1.76 inference(forward_subsumption_resolution,[status(thm)],[f863,f849])).
% 9.08/1.76 fof(f961,plain,(
% 9.08/1.76 ![X0,X1,X2]: (c_union(X0,X1,X2)=c_union(X0,c_union(X1,X0,X2),X2))),
% 9.08/1.76 inference(paramodulation,[status(thm)],[f884,f419])).
% 9.08/1.76 fof(f2462,plain,(
% 9.08/1.76 v_X=c_union(v_Y,v_Z,t_a)|~c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a))|v_X=c_union(v_Y,v_Z,t_a)),
% 9.08/1.76 inference(resolution,[status(thm)],[f660,f31])).
% 9.08/1.76 fof(f2463,plain,(
% 9.08/1.76 v_X=c_union(v_Y,v_Z,t_a)|~c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a))),
% 9.08/1.76 inference(duplicate_literals_removal,[status(thm)],[f2462])).
% 9.08/1.76 fof(f2568,plain,(
% 9.08/1.76 c_lessequals(c_union(v_Z,v_Y,t_a),v_X,tc_set(t_a))|v_X=c_union(v_Y,v_Z,t_a)|c_lessequals(c_union(v_Z,v_Y,t_a),v_X,tc_set(t_a))|v_X=c_union(v_Y,v_Z,t_a)),
% 9.08/1.76 inference(resolution,[status(thm)],[f113,f53])).
% 9.08/1.76 fof(f2582,plain,(
% 9.08/1.76 c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a))|v_X=c_union(v_Y,v_Z,t_a)|c_lessequals(c_union(v_Z,v_Y,t_a),v_X,tc_set(t_a))|v_X=c_union(v_Y,v_Z,t_a)),
% 9.08/1.76 inference(forward_demodulation,[status(thm)],[f884,f2568])).
% 9.08/1.76 fof(f2583,plain,(
% 9.08/1.76 c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a))|v_X=c_union(v_Y,v_Z,t_a)|c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a))|v_X=c_union(v_Y,v_Z,t_a)),
% 9.08/1.76 inference(forward_demodulation,[status(thm)],[f884,f2582])).
% 9.08/1.76 fof(f2584,plain,(
% 9.08/1.76 c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a))|v_X=c_union(v_Y,v_Z,t_a)),
% 9.08/1.76 inference(duplicate_literals_removal,[status(thm)],[f2583])).
% 9.08/1.76 fof(f2598,plain,(
% 9.08/1.76 ~c_lessequals(v_X,v_x,tc_set(t_a))|~c_lessequals(v_Z,v_X,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))|~v_X=v_X),
% 9.08/1.76 inference(backward_demodulation,[status(thm)],[f2701,f18])).
% 9.08/1.76 fof(f2599,plain,(
% 9.08/1.76 c_lessequals(v_Z,v_x,tc_set(t_a))|~c_lessequals(v_Z,v_X,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))|~v_X=v_X),
% 9.08/1.76 inference(backward_demodulation,[status(thm)],[f2701,f17])).
% 9.08/1.76 fof(f2602,plain,(
% 9.08/1.76 c_lessequals(v_Y,v_x,tc_set(t_a))|~c_lessequals(v_Z,v_X,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))|~v_X=v_X),
% 9.08/1.76 inference(backward_demodulation,[status(thm)],[f2701,f16])).
% 9.08/1.76 fof(f2701,plain,(
% 9.08/1.76 v_X=c_union(v_Y,v_Z,t_a)),
% 9.08/1.76 inference(forward_subsumption_resolution,[status(thm)],[f2584,f2463])).
% 9.08/1.76 fof(f2709,plain,(
% 9.08/1.76 ~c_lessequals(v_X,v_x,tc_set(t_a))|~c_lessequals(v_Z,v_X,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))),
% 9.08/1.76 inference(trivial_equality_resolution,[status(thm)],[f2598])).
% 9.08/1.76 fof(f2710,plain,(
% 9.08/1.76 c_lessequals(v_Z,v_x,tc_set(t_a))|~c_lessequals(v_Z,v_X,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))),
% 9.08/1.76 inference(trivial_equality_resolution,[status(thm)],[f2599])).
% 9.08/1.76 fof(f2711,plain,(
% 9.08/1.76 c_lessequals(v_Y,v_x,tc_set(t_a))|~c_lessequals(v_Z,v_X,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))),
% 9.08/1.76 inference(trivial_equality_resolution,[status(thm)],[f2602])).
% 9.08/1.76 fof(f2828,plain,(
% 9.08/1.76 c_lessequals(v_Z,v_X,tc_set(t_a))),
% 9.08/1.76 inference(paramodulation,[status(thm)],[f2701,f68])).
% 9.08/1.76 fof(f2831,plain,(
% 9.08/1.76 c_lessequals(v_Y,v_X,tc_set(t_a))),
% 9.08/1.76 inference(paramodulation,[status(thm)],[f2701,f59])).
% 9.08/1.76 fof(f2903,plain,(
% 9.08/1.76 c_lessequals(v_Y,v_x,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))),
% 9.08/1.76 inference(backward_subsumption_resolution,[status(thm)],[f2711,f2828])).
% 9.08/1.76 fof(f2904,plain,(
% 9.08/1.76 c_lessequals(v_Z,v_x,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))),
% 9.08/1.76 inference(backward_subsumption_resolution,[status(thm)],[f2710,f2828])).
% 9.08/1.76 fof(f2905,plain,(
% 9.08/1.76 ~c_lessequals(v_X,v_x,tc_set(t_a))|~c_lessequals(v_Y,v_X,tc_set(t_a))),
% 9.08/1.76 inference(backward_subsumption_resolution,[status(thm)],[f2709,f2828])).
% 9.08/1.76 fof(f2909,plain,(
% 9.08/1.76 c_lessequals(v_Y,v_x,tc_set(t_a))),
% 9.08/1.76 inference(forward_subsumption_resolution,[status(thm)],[f2903,f2831])).
% 9.08/1.76 fof(f2910,plain,(
% 9.08/1.76 c_lessequals(v_Z,v_x,tc_set(t_a))),
% 9.08/1.76 inference(forward_subsumption_resolution,[status(thm)],[f2904,f2831])).
% 9.08/1.76 fof(f2911,plain,(
% 9.08/1.76 ~c_lessequals(v_X,v_x,tc_set(t_a))),
% 9.08/1.76 inference(forward_subsumption_resolution,[status(thm)],[f2905,f2831])).
% 9.08/1.76 fof(f3169,plain,(
% 9.08/1.76 ![X0]: (c_lessequals(X0,v_x,tc_set(t_a))|~c_in(c_Main_OsubsetI__1(X0,v_x,t_a),v_Y,t_a))),
% 9.08/1.76 inference(resolution,[status(thm)],[f2909,f47])).
% 9.08/1.76 fof(f3172,plain,(
% 9.08/1.76 ![X0]: (c_lessequals(X0,v_x,tc_set(t_a))|~c_in(c_Main_OsubsetI__1(X0,v_x,t_a),v_Z,t_a))),
% 9.08/1.76 inference(resolution,[status(thm)],[f2910,f47])).
% 9.08/1.76 fof(f3883,plain,(
% 9.08/1.76 ![X0,X1]: (c_lessequals(c_union(c_union(v_Y,X0,t_a),X1,t_a),v_x,tc_set(t_a))|c_lessequals(c_union(c_union(v_Y,X0,t_a),X1,t_a),v_x,tc_set(t_a))|c_in(c_Main_OsubsetI__1(c_union(c_union(v_Y,X0,t_a),X1,t_a),v_x,t_a),X1,t_a)|c_in(c_Main_OsubsetI__1(c_union(c_union(v_Y,X0,t_a),X1,t_a),v_x,t_a),X0,t_a))),
% 9.08/1.76 inference(resolution,[status(thm)],[f3169,f92])).
% 9.08/1.76 fof(f3909,plain,(
% 9.08/1.76 ![X0,X1]: (c_lessequals(c_union(c_union(v_Y,X0,t_a),X1,t_a),v_x,tc_set(t_a))|c_in(c_Main_OsubsetI__1(c_union(c_union(v_Y,X0,t_a),X1,t_a),v_x,t_a),X1,t_a)|c_in(c_Main_OsubsetI__1(c_union(c_union(v_Y,X0,t_a),X1,t_a),v_x,t_a),X0,t_a))),
% 9.08/1.76 inference(duplicate_literals_removal,[status(thm)],[f3883])).
% 9.08/1.76 fof(f5578,plain,(
% 9.08/1.76 c_lessequals(c_union(c_union(v_Y,v_Z,t_a),v_Z,t_a),v_x,tc_set(t_a))|c_lessequals(c_union(c_union(v_Y,v_Z,t_a),v_Z,t_a),v_x,tc_set(t_a))),
% 9.08/1.76 inference(resolution,[status(thm)],[f3909,f3172])).
% 9.08/1.76 fof(f5642,plain,(
% 9.08/1.76 c_lessequals(c_union(v_Z,c_union(v_Y,v_Z,t_a),t_a),v_x,tc_set(t_a))|c_lessequals(c_union(c_union(v_Y,v_Z,t_a),v_Z,t_a),v_x,tc_set(t_a))),
% 9.08/1.76 inference(forward_demodulation,[status(thm)],[f884,f5578])).
% 9.08/1.76 fof(f5643,plain,(
% 9.08/1.76 c_lessequals(c_union(v_Z,v_Y,t_a),v_x,tc_set(t_a))|c_lessequals(c_union(c_union(v_Y,v_Z,t_a),v_Z,t_a),v_x,tc_set(t_a))),
% 9.08/1.76 inference(forward_demodulation,[status(thm)],[f961,f5642])).
% 9.08/1.78 fof(f5644,plain,(
% 9.08/1.78 c_lessequals(c_union(v_Y,v_Z,t_a),v_x,tc_set(t_a))|c_lessequals(c_union(c_union(v_Y,v_Z,t_a),v_Z,t_a),v_x,tc_set(t_a))),
% 9.08/1.78 inference(forward_demodulation,[status(thm)],[f884,f5643])).
% 9.08/1.78 fof(f5645,plain,(
% 9.08/1.78 c_lessequals(v_X,v_x,tc_set(t_a))|c_lessequals(c_union(c_union(v_Y,v_Z,t_a),v_Z,t_a),v_x,tc_set(t_a))),
% 9.08/1.78 inference(forward_demodulation,[status(thm)],[f2701,f5644])).
% 9.08/1.78 fof(f5646,plain,(
% 9.08/1.78 c_lessequals(v_X,v_x,tc_set(t_a))|c_lessequals(c_union(v_Z,c_union(v_Y,v_Z,t_a),t_a),v_x,tc_set(t_a))),
% 9.08/1.78 inference(forward_demodulation,[status(thm)],[f884,f5645])).
% 9.08/1.78 fof(f5647,plain,(
% 9.08/1.78 c_lessequals(v_X,v_x,tc_set(t_a))|c_lessequals(c_union(v_Z,v_Y,t_a),v_x,tc_set(t_a))),
% 9.08/1.78 inference(forward_demodulation,[status(thm)],[f961,f5646])).
% 9.08/1.78 fof(f5648,plain,(
% 9.08/1.78 c_lessequals(v_X,v_x,tc_set(t_a))|c_lessequals(c_union(v_Y,v_Z,t_a),v_x,tc_set(t_a))),
% 9.08/1.78 inference(forward_demodulation,[status(thm)],[f884,f5647])).
% 9.08/1.78 fof(f5649,plain,(
% 9.08/1.78 c_lessequals(v_X,v_x,tc_set(t_a))|c_lessequals(v_X,v_x,tc_set(t_a))),
% 9.08/1.78 inference(forward_demodulation,[status(thm)],[f2701,f5648])).
% 9.08/1.78 fof(f5650,plain,(
% 9.08/1.78 c_lessequals(v_X,v_x,tc_set(t_a))),
% 9.08/1.78 inference(duplicate_literals_removal,[status(thm)],[f5649])).
% 9.08/1.78 fof(f5651,plain,(
% 9.08/1.78 $false),
% 9.08/1.78 inference(forward_subsumption_resolution,[status(thm)],[f5650,f2911])).
% 9.08/1.78 % SZS output end CNFRefutation for theBenchmark.p
% 9.08/1.81 % Elapsed time: 1.255905 seconds
% 9.08/1.81 % CPU time: 9.652416 seconds
% 9.08/1.81 % Total memory used: 154.806 MB
% 9.08/1.81 % Net memory used: 148.787 MB
%------------------------------------------------------------------------------