%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT274-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 : n011.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 01:03:28 PM UTC 2026
% Result : Unsatisfiable 18.21s 17.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT274-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.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/15.44 % CPULimit : 300
% 0.08/15.44 % WCLimit : 300
% 0.08/15.44 % DateTime : Sun Sep 20 23:25:05 UTC 2026
% 0.08/15.44 % CPUTime :
% 0.34/15.63 % Drodi V4.1.1
% 18.21/17.95 % Refutation found
% 18.21/17.95 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 18.21/17.95 % SZS output start CNFRefutation for theBenchmark
% 18.21/17.95 fof(f1,axiom,(
% 18.21/17.95 (![V_S,V_A,V_a,V_L]: (( ~ c_lessequals(V_S,V_A,tc_set(t_a))| c_in(c_Pair(V_a,V_L,t_a,t_a),v_r,tc_prod(t_a,t_a))| c_in(v_sko__4mj(V_S,V_a,v_r),V_S,t_a)| c_in(v_sko__4mk(V_L,V_S,v_r),V_S,t_a)| V_S = c_emptyset ) ))),
% 18.21/17.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.95 fof(f2,axiom,(
% 18.21/17.95 (![V_L,V_S,V_A,V_a]: (( ~ c_in(c_Pair(v_sko__4mk(V_L,V_S,v_r),V_L,t_a,t_a),v_r,tc_prod(t_a,t_a))| ~ c_lessequals(V_S,V_A,tc_set(t_a))| c_in(c_Pair(V_a,V_L,t_a,t_a),v_r,tc_prod(t_a,t_a))| c_in(v_sko__4mj(V_S,V_a,v_r),V_S,t_a)| V_S = c_emptyset ) ))),
% 18.21/17.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.95 fof(f3,axiom,(
% 18.21/17.95 (![V_a,V_S,V_A,V_L]: (( ~ c_in(c_Pair(V_a,v_sko__4mj(V_S,V_a,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))| ~ c_lessequals(V_S,V_A,tc_set(t_a))| c_in(c_Pair(V_a,V_L,t_a,t_a),v_r,tc_prod(t_a,t_a))| c_in(v_sko__4mk(V_L,V_S,v_r),V_S,t_a)| V_S = c_emptyset ) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f4,axiom,(
% 18.21/17.96 (![V_a,V_S,V_L,V_A]: (( ~ c_in(c_Pair(V_a,v_sko__4mj(V_S,V_a,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))| ~ c_in(c_Pair(v_sko__4mk(V_L,V_S,v_r),V_L,t_a,t_a),v_r,tc_prod(t_a,t_a))| ~ c_lessequals(V_S,V_A,tc_set(t_a))| c_in(c_Pair(V_a,V_L,t_a,t_a),v_r,tc_prod(t_a,t_a))| V_S = c_emptyset ) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f5,axiom,(
% 18.21/17.96 (![V_x,V_S,T_a,V_r,V_a,V_b]: (( ~ c_in(V_x,V_S,T_a)| ~ c_lessequals(V_S,c_Tarski_Ointerval(V_r,V_a,V_b,T_a),tc_set(T_a))| c_in(c_Pair(V_a,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)) ) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f6,axiom,(
% 18.21/17.96 (![V_x,V_S,T_a,V_r,V_a,V_b]: (( ~ c_in(V_x,V_S,T_a)| ~ c_lessequals(V_S,c_Tarski_Ointerval(V_r,V_a,V_b,T_a),tc_set(T_a))| c_in(c_Pair(V_x,V_b,T_a,T_a),V_r,tc_prod(T_a,T_a)) ) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f7,axiom,(
% 18.21/17.96 (![V_x,V_b,T_a,V_r,V_a]: (( ~ c_in(c_Pair(V_x,V_b,T_a,T_a),V_r,tc_prod(T_a,T_a))| ~ c_in(c_Pair(V_a,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a))| c_in(V_x,c_Tarski_Ointerval(V_r,V_a,V_b,T_a),T_a) ) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f8,axiom,(
% 18.21/17.96 (![V_b,V_a,V_S]: (( ~ c_in(V_b,v_A,t_a)| ~ c_in(V_a,v_A,t_a)| ~ c_lessequals(V_S,c_Tarski_Ointerval(v_r,V_a,V_b,t_a),tc_set(t_a))| c_lessequals(V_S,v_A,tc_set(t_a)) ) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f9,axiom,(
% 18.21/17.96 (![V_S,V_L,V_y]: (( ~ c_Tarski_OisLub(V_S,v_cl,V_L,t_a)| ~ c_in(V_y,V_S,t_a)| c_in(c_Pair(V_y,V_L,t_a,t_a),v_r,tc_prod(t_a,t_a)) ) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f10,axiom,(
% 18.21/17.96 (![V_S,V_L,V_z]: (( ~ c_Tarski_OisLub(V_S,v_cl,V_L,t_a)| ~ c_in(V_z,v_A,t_a)| c_in(c_Pair(V_L,V_z,t_a,t_a),v_r,tc_prod(t_a,t_a))| c_in(v_sko__4mi(V_S,v_r,V_z),V_S,t_a) ) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f11,axiom,(
% 18.21/17.96 (![V_S,V_L,V_z]: (( ~ c_Tarski_OisLub(V_S,v_cl,V_L,t_a)| ~ c_in(V_z,v_A,t_a)| ~ c_in(c_Pair(v_sko__4mi(V_S,v_r,V_z),V_z,t_a,t_a),v_r,tc_prod(t_a,t_a))| c_in(c_Pair(V_L,V_z,t_a,t_a),v_r,tc_prod(t_a,t_a)) ) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f37,axiom,(
% 18.21/17.96 (![T_a]: (c_Datatype_Oo2s(c_Datatype_Ooption_ONone,T_a) = c_emptyset ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f38,axiom,(
% 18.21/17.96 (![V_a_H,T_a]: (c_Datatype_Ooption_ONone != c_Datatype_Ooption_OSome(V_a_H,T_a) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f1260,axiom,(
% 18.21/17.96 (![T_a]: (( ~ class_Ring__and__Field_Oaxclass__0__neq__1(T_a)| c_0 != c_1 ) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f1537,axiom,(
% 18.21/17.96 (![V_c,T_a]: (~ c_in(V_c,c_emptyset,T_a) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f1693,axiom,(
% 18.21/17.96 (![V_A,T_a]: (c_lessequals(c_emptyset,V_A,tc_set(T_a)) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f1700,axiom,(
% 18.21/17.96 (![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) ) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f1704,axiom,(
% 18.21/17.96 (![V_A,T_a]: (c_lessequals(V_A,V_A,tc_set(T_a)) ))),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f1736,axiom,(
% 18.21/17.96 class_Ring__and__Field_Oaxclass__0__neq__1(tc_IntDef_Oint) ),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f2752,negated_conjecture,(
% 18.21/17.96 c_in(v_a,v_A,t_a) ),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f2753,negated_conjecture,(
% 18.21/17.96 c_in(v_b,v_A,t_a) ),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f2754,negated_conjecture,(
% 18.21/17.96 c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)) ),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f2755,negated_conjecture,(
% 18.21/17.96 v_S != c_emptyset ),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f2756,negated_conjecture,(
% 18.21/17.96 c_Tarski_OisLub(v_S,v_cl,v_L,t_a) ),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f2758,negated_conjecture,(
% 18.21/17.96 ~ c_in(v_L,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a) ),
% 18.21/17.96 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/17.96 fof(f2759,plain,(
% 18.21/17.96 ![V_S]: ((![V_L]: ((![V_a]: (((![V_A]: ~c_lessequals(V_S,V_A,tc_set(t_a)))|c_in(c_Pair(V_a,V_L,t_a,t_a),v_r,tc_prod(t_a,t_a)))|c_in(v_sko__4mj(V_S,V_a,v_r),V_S,t_a)))|c_in(v_sko__4mk(V_L,V_S,v_r),V_S,t_a)))|V_S=c_emptyset)),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f1])).
% 18.21/17.96 fof(f2760,plain,(
% 18.21/17.96 ![X0,X1,X2,X3]: (~c_lessequals(X0,X1,tc_set(t_a))|c_in(c_Pair(X2,X3,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(X0,X2,v_r),X0,t_a)|c_in(v_sko__4mk(X3,X0,v_r),X0,t_a)|X0=c_emptyset)),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2759])).
% 18.21/17.96 fof(f2761,plain,(
% 18.21/17.96 ![V_S]: ((![V_a]: ((![V_L]: ((~c_in(c_Pair(v_sko__4mk(V_L,V_S,v_r),V_L,t_a,t_a),v_r,tc_prod(t_a,t_a))|(![V_A]: ~c_lessequals(V_S,V_A,tc_set(t_a))))|c_in(c_Pair(V_a,V_L,t_a,t_a),v_r,tc_prod(t_a,t_a))))|c_in(v_sko__4mj(V_S,V_a,v_r),V_S,t_a)))|V_S=c_emptyset)),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f2])).
% 18.21/17.96 fof(f2762,plain,(
% 18.21/17.96 ![X0,X1,X2,X3]: (~c_in(c_Pair(v_sko__4mk(X0,X1,v_r),X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|~c_lessequals(X1,X2,tc_set(t_a))|c_in(c_Pair(X3,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(X1,X3,v_r),X1,t_a)|X1=c_emptyset)),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2761])).
% 18.21/17.96 fof(f2763,plain,(
% 18.21/17.96 ![V_S]: ((![V_L]: ((![V_a]: ((~c_in(c_Pair(V_a,v_sko__4mj(V_S,V_a,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|(![V_A]: ~c_lessequals(V_S,V_A,tc_set(t_a))))|c_in(c_Pair(V_a,V_L,t_a,t_a),v_r,tc_prod(t_a,t_a))))|c_in(v_sko__4mk(V_L,V_S,v_r),V_S,t_a)))|V_S=c_emptyset)),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f3])).
% 18.21/17.96 fof(f2764,plain,(
% 18.21/17.96 ![X0,X1,X2,X3]: (~c_in(c_Pair(X0,v_sko__4mj(X1,X0,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|~c_lessequals(X1,X2,tc_set(t_a))|c_in(c_Pair(X0,X3,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X3,X1,v_r),X1,t_a)|X1=c_emptyset)),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2763])).
% 18.21/17.96 fof(f2765,plain,(
% 18.21/17.96 ![V_S]: ((![V_a,V_L]: (((~c_in(c_Pair(V_a,v_sko__4mj(V_S,V_a,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|~c_in(c_Pair(v_sko__4mk(V_L,V_S,v_r),V_L,t_a,t_a),v_r,tc_prod(t_a,t_a)))|(![V_A]: ~c_lessequals(V_S,V_A,tc_set(t_a))))|c_in(c_Pair(V_a,V_L,t_a,t_a),v_r,tc_prod(t_a,t_a))))|V_S=c_emptyset)),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f4])).
% 18.21/17.96 fof(f2766,plain,(
% 18.21/17.96 ![X0,X1,X2,X3]: (~c_in(c_Pair(X0,v_sko__4mj(X1,X0,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|~c_in(c_Pair(v_sko__4mk(X2,X1,v_r),X2,t_a,t_a),v_r,tc_prod(t_a,t_a))|~c_lessequals(X1,X3,tc_set(t_a))|c_in(c_Pair(X0,X2,t_a,t_a),v_r,tc_prod(t_a,t_a))|X1=c_emptyset)),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2765])).
% 18.21/17.96 fof(f2767,plain,(
% 18.21/17.96 ![V_x,T_a,V_r,V_a]: ((![V_S]: (~c_in(V_x,V_S,T_a)|(![V_b]: ~c_lessequals(V_S,c_Tarski_Ointerval(V_r,V_a,V_b,T_a),tc_set(T_a)))))|c_in(c_Pair(V_a,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)))),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f5])).
% 18.21/17.96 fof(f2768,plain,(
% 18.21/17.96 ![X0,X1,X2,X3,X4,X5]: (~c_in(X0,X1,X2)|~c_lessequals(X1,c_Tarski_Ointerval(X3,X4,X5,X2),tc_set(X2))|c_in(c_Pair(X4,X0,X2,X2),X3,tc_prod(X2,X2)))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2767])).
% 18.21/17.96 fof(f2769,plain,(
% 18.21/17.96 ![V_x,T_a,V_r,V_b]: ((![V_S]: (~c_in(V_x,V_S,T_a)|(![V_a]: ~c_lessequals(V_S,c_Tarski_Ointerval(V_r,V_a,V_b,T_a),tc_set(T_a)))))|c_in(c_Pair(V_x,V_b,T_a,T_a),V_r,tc_prod(T_a,T_a)))),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f6])).
% 18.21/17.96 fof(f2770,plain,(
% 18.21/17.96 ![X0,X1,X2,X3,X4,X5]: (~c_in(X0,X1,X2)|~c_lessequals(X1,c_Tarski_Ointerval(X3,X4,X5,X2),tc_set(X2))|c_in(c_Pair(X0,X5,X2,X2),X3,tc_prod(X2,X2)))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2769])).
% 18.21/17.96 fof(f2771,plain,(
% 18.21/17.96 ![X0,X1,X2,X3,X4]: (~c_in(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2))|~c_in(c_Pair(X4,X0,X2,X2),X3,tc_prod(X2,X2))|c_in(X0,c_Tarski_Ointerval(X3,X4,X1,X2),X2))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f7])).
% 18.21/17.96 fof(f2772,plain,(
% 18.21/17.96 ![V_S]: ((![V_b,V_a]: ((~c_in(V_b,v_A,t_a)|~c_in(V_a,v_A,t_a))|~c_lessequals(V_S,c_Tarski_Ointerval(v_r,V_a,V_b,t_a),tc_set(t_a))))|c_lessequals(V_S,v_A,tc_set(t_a)))),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f8])).
% 18.21/17.96 fof(f2773,plain,(
% 18.21/17.96 ![X0,X1,X2]: (~c_in(X0,v_A,t_a)|~c_in(X1,v_A,t_a)|~c_lessequals(X2,c_Tarski_Ointerval(v_r,X1,X0,t_a),tc_set(t_a))|c_lessequals(X2,v_A,tc_set(t_a)))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2772])).
% 18.21/17.96 fof(f2774,plain,(
% 18.21/17.96 ![V_L,V_y]: ((![V_S]: (~c_Tarski_OisLub(V_S,v_cl,V_L,t_a)|~c_in(V_y,V_S,t_a)))|c_in(c_Pair(V_y,V_L,t_a,t_a),v_r,tc_prod(t_a,t_a)))),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f9])).
% 18.21/17.96 fof(f2775,plain,(
% 18.21/17.96 ![X0,X1,X2]: (~c_Tarski_OisLub(X0,v_cl,X1,t_a)|~c_in(X2,X0,t_a)|c_in(c_Pair(X2,X1,t_a,t_a),v_r,tc_prod(t_a,t_a)))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2774])).
% 18.21/17.96 fof(f2776,plain,(
% 18.21/17.96 ![V_S,V_z]: ((![V_L]: ((~c_Tarski_OisLub(V_S,v_cl,V_L,t_a)|~c_in(V_z,v_A,t_a))|c_in(c_Pair(V_L,V_z,t_a,t_a),v_r,tc_prod(t_a,t_a))))|c_in(v_sko__4mi(V_S,v_r,V_z),V_S,t_a))),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f10])).
% 18.21/17.96 fof(f2777,plain,(
% 18.21/17.96 ![X0,X1,X2]: (~c_Tarski_OisLub(X0,v_cl,X1,t_a)|~c_in(X2,v_A,t_a)|c_in(c_Pair(X1,X2,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mi(X0,v_r,X2),X0,t_a))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2776])).
% 18.21/17.96 fof(f2778,plain,(
% 18.21/17.96 ![V_L,V_z]: ((![V_S]: ((~c_Tarski_OisLub(V_S,v_cl,V_L,t_a)|~c_in(V_z,v_A,t_a))|~c_in(c_Pair(v_sko__4mi(V_S,v_r,V_z),V_z,t_a,t_a),v_r,tc_prod(t_a,t_a))))|c_in(c_Pair(V_L,V_z,t_a,t_a),v_r,tc_prod(t_a,t_a)))),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f11])).
% 18.21/17.96 fof(f2779,plain,(
% 18.21/17.96 ![X0,X1,X2]: (~c_Tarski_OisLub(X0,v_cl,X1,t_a)|~c_in(X2,v_A,t_a)|~c_in(c_Pair(v_sko__4mi(X0,v_r,X2),X2,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(X1,X2,t_a,t_a),v_r,tc_prod(t_a,t_a)))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2778])).
% 18.21/17.96 fof(f2811,plain,(
% 18.21/17.96 ![X0]: (c_Datatype_Oo2s(c_Datatype_Ooption_ONone,X0)=c_emptyset)),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f37])).
% 18.21/17.96 fof(f2812,plain,(
% 18.21/17.96 ![X0,X1]: (~c_Datatype_Ooption_ONone=c_Datatype_Ooption_OSome(X0,X1))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f38])).
% 18.21/17.96 fof(f4468,plain,(
% 18.21/17.96 (![T_a]: ~class_Ring__and__Field_Oaxclass__0__neq__1(T_a))|~c_0=c_1),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f1260])).
% 18.21/17.96 fof(f4469,plain,(
% 18.21/17.96 ![X0]: (~class_Ring__and__Field_Oaxclass__0__neq__1(X0)|~c_0=c_1)),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f4468])).
% 18.21/17.96 fof(f4861,plain,(
% 18.21/17.96 ![X0,X1]: (~c_in(X0,c_emptyset,X1))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f1537])).
% 18.21/17.96 fof(f5064,plain,(
% 18.21/17.96 ![X0,X1]: (c_lessequals(c_emptyset,X0,tc_set(X1)))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f1693])).
% 18.21/17.96 fof(f5074,plain,(
% 18.21/17.96 ![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))),
% 18.21/17.96 inference(miniscoping,[status(thm)],[f1700])).
% 18.21/17.96 fof(f5075,plain,(
% 18.21/17.96 ![X0,X1,X2,X3]: (~c_in(X0,X1,X2)|~c_lessequals(X1,X3,tc_set(X2))|c_in(X0,X3,X2))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f5074])).
% 18.21/17.96 fof(f5080,plain,(
% 18.21/17.96 ![X0,X1]: (c_lessequals(X0,X0,tc_set(X1)))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f1704])).
% 18.21/17.96 fof(f5118,plain,(
% 18.21/17.96 class_Ring__and__Field_Oaxclass__0__neq__1(tc_IntDef_Oint)),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f1736])).
% 18.21/17.96 fof(f6137,plain,(
% 18.21/17.96 c_in(v_a,v_A,t_a)),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2752])).
% 18.21/17.96 fof(f6138,plain,(
% 18.21/17.96 c_in(v_b,v_A,t_a)),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2753])).
% 18.21/17.96 fof(f6139,plain,(
% 18.21/17.96 c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2754])).
% 18.21/17.96 fof(f6140,plain,(
% 18.21/17.96 ~v_S=c_emptyset),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2755])).
% 18.21/17.96 fof(f6141,plain,(
% 18.21/17.96 c_Tarski_OisLub(v_S,v_cl,v_L,t_a)),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2756])).
% 18.21/17.96 fof(f6143,plain,(
% 18.21/17.96 ~c_in(v_L,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a)),
% 18.21/17.96 inference(cnf_transformation,[status(thm)],[f2758])).
% 18.21/17.96 fof(f6144,definition,(
% 18.21/17.96 ![X0]: (sQ0_spl <=> (~class_Ring__and__Field_Oaxclass__0__neq__1(X0)))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6145,plain,(
% 18.21/17.96 ![X0]: (~class_Ring__and__Field_Oaxclass__0__neq__1(X0)|~sQ0_spl)),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6144])).
% 18.21/17.96 fof(f6147,definition,(
% 18.21/17.96 sQ1_spl <=> (c_0=c_1)),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6150,plain,(
% 18.21/17.96 sQ0_spl|~sQ1_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f4469,f6144,f6147])).
% 18.21/17.96 fof(f6162,plain,(
% 18.21/17.96 ![X0,X1]: (c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X0,v_r),v_S,t_a)|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)|v_S=c_emptyset)),
% 18.21/17.96 inference(resolution,[status(thm)],[f2760,f6139])).
% 18.21/17.96 fof(f6163,plain,(
% 18.21/17.96 ![X0,X1,X2]: (c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(X2,X0,v_r),X2,t_a)|c_in(v_sko__4mk(X1,X2,v_r),X2,t_a)|X2=c_emptyset)),
% 18.21/17.96 inference(resolution,[status(thm)],[f2760,f5080])).
% 18.21/17.96 fof(f6171,definition,(
% 18.21/17.96 ![X0,X1]: (sQ4_spl <=> (c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X0,v_r),v_S,t_a)|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6172,plain,(
% 18.21/17.96 ![X0,X1]: (c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X0,v_r),v_S,t_a)|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)|~sQ4_spl)),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6171])).
% 18.21/17.96 fof(f6174,definition,(
% 18.21/17.96 sQ5_spl <=> (v_S=c_emptyset)),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6175,plain,(
% 18.21/17.96 v_S=c_emptyset|~sQ5_spl),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6174])).
% 18.21/17.96 fof(f6177,plain,(
% 18.21/17.96 sQ4_spl|sQ5_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6162,f6171,f6174])).
% 18.21/17.96 fof(f6179,plain,(
% 18.21/17.96 ![X0,X1,X2,X3,X4,X5]: (~c_lessequals(X0,X1,tc_set(t_a))|c_in(c_Pair(X2,X3,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(X0,X2,v_r),X0,t_a)|X0=c_emptyset|~c_in(v_sko__4mk(X3,X0,v_r),X4,t_a)|~c_lessequals(X4,c_Tarski_Ointerval(v_r,X5,X3,t_a),tc_set(t_a)))),
% 18.21/17.96 inference(resolution,[status(thm)],[f2762,f2770])).
% 18.21/17.96 fof(f6182,plain,(
% 18.21/17.96 ![X0,X1,X2,X3,X4,X5]: (~c_lessequals(X0,X1,tc_set(t_a))|c_in(c_Pair(X2,X3,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X3,X0,v_r),X0,t_a)|X0=c_emptyset|~c_in(v_sko__4mj(X0,X2,v_r),X4,t_a)|~c_lessequals(X4,c_Tarski_Ointerval(v_r,X2,X5,t_a),tc_set(t_a)))),
% 18.21/17.96 inference(resolution,[status(thm)],[f2764,f2768])).
% 18.21/17.96 fof(f6183,plain,(
% 18.21/17.96 ![X0,X1,X2,X3]: (c_in(v_sko__4mj(v_S,v_sko__4mk(X0,X1,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X0,v_S,v_r),v_S,t_a)|~c_lessequals(X1,X2,tc_set(t_a))|c_in(c_Pair(X3,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(X1,X3,v_r),X1,t_a)|X1=c_emptyset|~sQ4_spl)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6172,f2762])).
% 18.21/17.96 fof(f6184,plain,(
% 18.21/17.96 ![X0,X1,X2,X3]: (c_in(v_sko__4mj(v_S,X0,v_r),v_S,t_a)|c_in(v_sko__4mk(v_sko__4mj(X1,X0,v_r),v_S,v_r),v_S,t_a)|~c_lessequals(X1,X2,tc_set(t_a))|c_in(c_Pair(X0,X3,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X3,X1,v_r),X1,t_a)|X1=c_emptyset|~sQ4_spl)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6172,f2764])).
% 18.21/17.96 fof(f6186,plain,(
% 18.21/17.96 ![X0,X1]: (c_in(v_sko__4mj(v_S,v_sko__4mk(X0,v_S,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X0,v_S,v_r),v_S,t_a)|c_in(c_Pair(X1,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X1,v_r),v_S,t_a)|v_S=c_emptyset|~sQ4_spl)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6183,f6139])).
% 18.21/17.96 fof(f6187,plain,(
% 18.21/17.96 ![X0,X1,X2]: (c_in(v_sko__4mj(v_S,v_sko__4mk(X0,X1,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X0,v_S,v_r),v_S,t_a)|c_in(c_Pair(X2,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(X1,X2,v_r),X1,t_a)|X1=c_emptyset|~sQ4_spl)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6183,f5080])).
% 18.21/17.96 fof(f6192,definition,(
% 18.21/17.96 ![X0,X1]: (sQ7_spl <=> (c_in(v_sko__4mj(v_S,v_sko__4mk(X0,v_S,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X0,v_S,v_r),v_S,t_a)|c_in(c_Pair(X1,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X1,v_r),v_S,t_a)))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6195,plain,(
% 18.21/17.96 sQ7_spl|sQ5_spl|~sQ4_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6186,f6192,f6174,f6171])).
% 18.21/17.96 fof(f6196,plain,(
% 18.21/17.96 $false|~sQ5_spl),
% 18.21/17.96 inference(forward_subsumption_resolution,[status(thm)],[f6175,f6140])).
% 18.21/17.96 fof(f6197,plain,(
% 18.21/17.96 ~sQ5_spl),
% 18.21/17.96 inference(contradiction_clause,[status(thm)],[f6196])).
% 18.21/17.96 fof(f6203,plain,(
% 18.21/17.96 ![X0]: (c_in(v_sko__4mj(v_S,v_sko__4mk(X0,v_S,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X0,v_S,v_r),v_S,t_a)|c_in(c_Pair(v_sko__4mk(X0,v_S,v_r),X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|v_S=c_emptyset|~sQ4_spl)),
% 18.21/17.96 inference(factoring,[status(thm)],[f6187])).
% 18.21/17.96 fof(f6208,definition,(
% 18.21/17.96 ![X0]: (sQ9_spl <=> (c_in(v_sko__4mj(v_S,v_sko__4mk(X0,v_S,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X0,v_S,v_r),v_S,t_a)|c_in(c_Pair(v_sko__4mk(X0,v_S,v_r),X0,t_a,t_a),v_r,tc_prod(t_a,t_a))))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6211,plain,(
% 18.21/17.96 sQ9_spl|sQ5_spl|~sQ4_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6203,f6208,f6174,f6171])).
% 18.21/17.96 fof(f6213,plain,(
% 18.21/17.96 ![X0,X1]: (c_in(v_sko__4mj(v_S,X0,v_r),v_S,t_a)|c_in(v_sko__4mk(v_sko__4mj(v_S,X0,v_r),v_S,v_r),v_S,t_a)|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)|v_S=c_emptyset|~sQ4_spl)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6184,f6139])).
% 18.21/17.96 fof(f6219,definition,(
% 18.21/17.96 ![X0,X1]: (sQ11_spl <=> (c_in(v_sko__4mj(v_S,X0,v_r),v_S,t_a)|c_in(v_sko__4mk(v_sko__4mj(v_S,X0,v_r),v_S,v_r),v_S,t_a)|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6222,plain,(
% 18.21/17.96 sQ11_spl|sQ5_spl|~sQ4_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6213,f6219,f6174,f6171])).
% 18.21/17.96 fof(f6234,plain,(
% 18.21/17.96 ![X0]: (~c_in(X0,v_S,t_a)|c_in(X0,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a))),
% 18.21/17.96 inference(resolution,[status(thm)],[f5075,f6139])).
% 18.21/17.96 fof(f6247,plain,(
% 18.21/17.96 ~c_in(c_Pair(v_L,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))|~c_in(c_Pair(v_a,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))),
% 18.21/17.96 inference(resolution,[status(thm)],[f2771,f6143])).
% 18.21/17.96 fof(f6250,definition,(
% 18.21/17.96 sQ14_spl <=> (c_in(c_Pair(v_L,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a)))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6252,plain,(
% 18.21/17.96 ~c_in(c_Pair(v_L,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))|sQ14_spl),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6250])).
% 18.21/17.96 fof(f6253,definition,(
% 18.21/17.96 sQ15_spl <=> (c_in(c_Pair(v_a,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a)))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6255,plain,(
% 18.21/17.96 ~c_in(c_Pair(v_a,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))|sQ15_spl),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6253])).
% 18.21/17.96 fof(f6256,plain,(
% 18.21/17.96 ~sQ14_spl|~sQ15_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6247,f6250,f6253])).
% 18.21/17.96 fof(f6257,plain,(
% 18.21/17.96 ![X0,X1,X2,X3]: (~c_in(X0,v_A,t_a)|~c_lessequals(X1,c_Tarski_Ointerval(v_r,v_sko__4mj(v_A,X2,v_r),X0,t_a),tc_set(t_a))|c_lessequals(X1,v_A,tc_set(t_a))|c_in(v_sko__4mj(v_S,v_sko__4mk(X3,v_A,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X3,v_S,v_r),v_S,t_a)|c_in(c_Pair(X2,X3,t_a,t_a),v_r,tc_prod(t_a,t_a))|v_A=c_emptyset|~sQ4_spl)),
% 18.21/17.96 inference(resolution,[status(thm)],[f2773,f6187])).
% 18.21/17.96 fof(f6258,plain,(
% 18.21/17.96 ![X0,X1]: (~c_in(X0,v_A,t_a)|~c_lessequals(X1,c_Tarski_Ointerval(v_r,v_b,X0,t_a),tc_set(t_a))|c_lessequals(X1,v_A,tc_set(t_a)))),
% 18.21/17.96 inference(resolution,[status(thm)],[f2773,f6138])).
% 18.21/17.96 fof(f6259,plain,(
% 18.21/17.96 ![X0,X1]: (~c_in(X0,v_A,t_a)|~c_lessequals(X1,c_Tarski_Ointerval(v_r,v_a,X0,t_a),tc_set(t_a))|c_lessequals(X1,v_A,tc_set(t_a)))),
% 18.21/17.96 inference(resolution,[status(thm)],[f2773,f6137])).
% 18.21/17.96 fof(f6260,definition,(
% 18.21/17.96 ![X0,X1,X2,X3]: (sQ16_spl <=> (~c_in(X0,v_A,t_a)|~c_lessequals(X1,c_Tarski_Ointerval(v_r,v_sko__4mj(v_A,X2,v_r),X0,t_a),tc_set(t_a))|c_lessequals(X1,v_A,tc_set(t_a))|c_in(v_sko__4mj(v_S,v_sko__4mk(X3,v_A,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X3,v_S,v_r),v_S,t_a)|c_in(c_Pair(X2,X3,t_a,t_a),v_r,tc_prod(t_a,t_a))))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6263,definition,(
% 18.21/17.96 sQ17_spl <=> (v_A=c_emptyset)),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6264,plain,(
% 18.21/17.96 v_A=c_emptyset|~sQ17_spl),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6263])).
% 18.21/17.96 fof(f6266,plain,(
% 18.21/17.96 sQ16_spl|sQ17_spl|~sQ4_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6257,f6260,f6263,f6171])).
% 18.21/17.96 fof(f6267,plain,(
% 18.21/17.96 $false|~sQ0_spl),
% 18.21/17.96 inference(forward_subsumption_resolution,[status(thm)],[f5118,f6145])).
% 18.21/17.96 fof(f6268,plain,(
% 18.21/17.96 ~sQ0_spl),
% 18.21/17.96 inference(contradiction_clause,[status(thm)],[f6267])).
% 18.21/17.96 fof(f6271,plain,(
% 18.21/17.96 ![X0]: (~c_in(X0,v_S,t_a)|c_in(c_Pair(X0,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a)))),
% 18.21/17.96 inference(resolution,[status(thm)],[f2775,f6141])).
% 18.21/17.96 fof(f6272,plain,(
% 18.21/17.96 ![X0]: (~c_in(X0,v_A,t_a)|c_in(c_Pair(v_L,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mi(v_S,v_r,X0),v_S,t_a))),
% 18.21/17.96 inference(resolution,[status(thm)],[f2777,f6141])).
% 18.21/17.96 fof(f6291,definition,(
% 18.21/17.96 ![X0]: (sQ21_spl <=> (~c_lessequals(c_Tarski_Ointerval(v_r,v_a,v_b,t_a),c_Tarski_Ointerval(v_r,X0,v_b,t_a),tc_set(t_a))))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6292,plain,(
% 18.21/17.96 ![X0]: (~c_lessequals(c_Tarski_Ointerval(v_r,v_a,v_b,t_a),c_Tarski_Ointerval(v_r,X0,v_b,t_a),tc_set(t_a))|~sQ21_spl)),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6291])).
% 18.21/17.96 fof(f6298,plain,(
% 18.21/17.96 $false|~sQ21_spl),
% 18.21/17.96 inference(resolution,[status(thm)],[f6292,f5080])).
% 18.21/17.96 fof(f6299,plain,(
% 18.21/17.96 ~sQ21_spl),
% 18.21/17.96 inference(contradiction_clause,[status(thm)],[f6298])).
% 18.21/17.96 fof(f6300,plain,(
% 18.21/17.96 ![X0,X1]: (~c_in(c_Pair(v_a,v_sko__4mj(X0,v_a,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|~c_in(c_Pair(v_sko__4mk(v_L,X0,v_r),v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))|~c_lessequals(X0,X1,tc_set(t_a))|X0=c_emptyset|sQ15_spl)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6255,f2766])).
% 18.21/17.96 fof(f6308,definition,(
% 18.21/17.96 sQ24_spl <=> (c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6309,plain,(
% 18.21/17.96 c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)|~sQ24_spl),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6308])).
% 18.21/17.96 fof(f6312,definition,(
% 18.21/17.96 sQ25_spl <=> (c_in(v_sko__4mj(v_S,v_a,v_r),v_S,t_a))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6314,plain,(
% 18.21/17.96 ~c_in(v_sko__4mj(v_S,v_a,v_r),v_S,t_a)|sQ25_spl),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6312])).
% 18.21/17.96 fof(f6316,plain,(
% 18.21/17.96 ![X0]: (~c_in(X0,v_A,t_a)|c_lessequals(c_emptyset,v_A,tc_set(t_a)))),
% 18.21/17.96 inference(resolution,[status(thm)],[f6258,f5064])).
% 18.21/17.96 fof(f6318,definition,(
% 18.21/17.96 ![X0]: (sQ26_spl <=> (~c_in(X0,v_A,t_a)))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6319,plain,(
% 18.21/17.96 ![X0]: (~c_in(X0,v_A,t_a)|~sQ26_spl)),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6318])).
% 18.21/17.96 fof(f6321,definition,(
% 18.21/17.96 sQ27_spl <=> (c_lessequals(c_emptyset,v_A,tc_set(t_a)))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6324,plain,(
% 18.21/17.96 sQ26_spl|sQ27_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6316,f6318,f6321])).
% 18.21/17.96 fof(f6325,plain,(
% 18.21/17.96 $false|~sQ26_spl),
% 18.21/17.96 inference(backward_subsumption_resolution,[status(thm)],[f6138,f6319])).
% 18.21/17.96 fof(f6328,plain,(
% 18.21/17.96 ~sQ26_spl),
% 18.21/17.96 inference(contradiction_clause,[status(thm)],[f6325])).
% 18.21/17.96 fof(f6338,definition,(
% 18.21/17.96 ![X0]: (sQ29_spl <=> (~c_lessequals(c_Tarski_Ointerval(v_r,v_a,v_b,t_a),c_Tarski_Ointerval(v_r,v_a,X0,t_a),tc_set(t_a))))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6339,plain,(
% 18.21/17.96 ![X0]: (~c_lessequals(c_Tarski_Ointerval(v_r,v_a,v_b,t_a),c_Tarski_Ointerval(v_r,v_a,X0,t_a),tc_set(t_a))|~sQ29_spl)),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6338])).
% 18.21/17.96 fof(f6364,plain,(
% 18.21/17.96 ![X0,X1,X2,X3,X4]: (c_in(v_sko__4mj(X0,v_sko__4mk(X1,X2,v_r),v_r),X0,t_a)|c_in(v_sko__4mk(X1,X0,v_r),X0,t_a)|X0=c_emptyset|~c_lessequals(X2,X3,tc_set(t_a))|c_in(c_Pair(X4,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(X2,X4,v_r),X2,t_a)|X2=c_emptyset)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6163,f2762])).
% 18.21/17.96 fof(f6365,plain,(
% 18.21/17.96 ![X0,X1,X2,X3,X4]: (c_in(v_sko__4mj(X0,X1,v_r),X0,t_a)|c_in(v_sko__4mk(v_sko__4mj(X2,X1,v_r),X0,v_r),X0,t_a)|X0=c_emptyset|~c_lessequals(X2,X3,tc_set(t_a))|c_in(c_Pair(X1,X4,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X4,X2,v_r),X2,t_a)|X2=c_emptyset)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6163,f2764])).
% 18.21/17.96 fof(f6366,plain,(
% 18.21/17.96 ![X0,X1,X2,X3]: (c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_A,v_r),v_A,t_a)|v_A=c_emptyset|~c_in(X2,v_A,t_a)|~c_lessequals(X3,c_Tarski_Ointerval(v_r,v_sko__4mj(v_A,X0,v_r),X2,t_a),tc_set(t_a))|c_lessequals(X3,v_A,tc_set(t_a)))),
% 18.21/17.96 inference(resolution,[status(thm)],[f6163,f2773])).
% 18.21/17.96 fof(f6370,plain,(
% 18.21/17.96 ![X0,X1,X2,X3]: (c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_A,X0,v_r),v_A,t_a)|v_A=c_emptyset|~c_in(X2,v_A,t_a)|~c_lessequals(X3,c_Tarski_Ointerval(v_r,v_sko__4mk(X1,v_A,v_r),X2,t_a),tc_set(t_a))|c_lessequals(X3,v_A,tc_set(t_a)))),
% 18.21/17.96 inference(resolution,[status(thm)],[f6163,f2773])).
% 18.21/17.96 fof(f6374,definition,(
% 18.21/17.96 ![X0,X1,X2,X3]: (sQ31_spl <=> (c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_A,v_r),v_A,t_a)|~c_in(X2,v_A,t_a)|~c_lessequals(X3,c_Tarski_Ointerval(v_r,v_sko__4mj(v_A,X0,v_r),X2,t_a),tc_set(t_a))|c_lessequals(X3,v_A,tc_set(t_a))))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6377,plain,(
% 18.21/17.96 sQ31_spl|sQ17_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6366,f6374,f6263])).
% 18.21/17.96 fof(f6384,definition,(
% 18.21/17.96 ![X0,X1,X2,X3]: (sQ33_spl <=> (c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_A,X0,v_r),v_A,t_a)|~c_in(X2,v_A,t_a)|~c_lessequals(X3,c_Tarski_Ointerval(v_r,v_sko__4mk(X1,v_A,v_r),X2,t_a),tc_set(t_a))|c_lessequals(X3,v_A,tc_set(t_a))))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6387,plain,(
% 18.21/17.96 sQ33_spl|sQ17_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6370,f6384,f6263])).
% 18.21/17.96 fof(f6394,plain,(
% 18.21/17.96 ![X0]: (~c_in(X0,v_A,t_a)|~c_in(c_Pair(v_sko__4mi(v_S,v_r,X0),X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(v_L,X0,t_a,t_a),v_r,tc_prod(t_a,t_a)))),
% 18.21/17.96 inference(resolution,[status(thm)],[f2779,f6141])).
% 18.21/17.96 fof(f6397,plain,(
% 18.21/17.96 c_in(v_a,c_emptyset,t_a)|~sQ17_spl),
% 18.21/17.96 inference(backward_demodulation,[status(thm)],[f6264,f6137])).
% 18.21/17.96 fof(f6401,plain,(
% 18.21/17.96 $false|~sQ17_spl),
% 18.21/17.96 inference(forward_subsumption_resolution,[status(thm)],[f6397,f4861])).
% 18.21/17.96 fof(f6402,plain,(
% 18.21/17.96 ~sQ17_spl),
% 18.21/17.96 inference(contradiction_clause,[status(thm)],[f6401])).
% 18.21/17.96 fof(f6404,plain,(
% 18.21/17.96 ~c_in(v_b,v_A,t_a)|c_lessequals(v_S,v_A,tc_set(t_a))),
% 18.21/17.96 inference(resolution,[status(thm)],[f6259,f6139])).
% 18.21/17.96 fof(f6405,plain,(
% 18.21/17.96 ![X0]: (~c_in(X0,v_A,t_a)|c_lessequals(c_Tarski_Ointerval(v_r,v_a,X0,t_a),v_A,tc_set(t_a)))),
% 18.21/17.96 inference(resolution,[status(thm)],[f6259,f5080])).
% 18.21/17.96 fof(f6407,definition,(
% 18.21/17.96 sQ35_spl <=> (c_in(v_b,v_A,t_a))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6409,plain,(
% 18.21/17.96 ~c_in(v_b,v_A,t_a)|sQ35_spl),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6407])).
% 18.21/17.96 fof(f6410,definition,(
% 18.21/17.96 sQ36_spl <=> (c_lessequals(v_S,v_A,tc_set(t_a)))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6411,plain,(
% 18.21/17.96 c_lessequals(v_S,v_A,tc_set(t_a))|~sQ36_spl),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6410])).
% 18.21/17.96 fof(f6413,plain,(
% 18.21/17.96 ~sQ35_spl|sQ36_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6404,f6407,f6410])).
% 18.21/17.96 fof(f6414,plain,(
% 18.21/17.96 $false|sQ35_spl),
% 18.21/17.96 inference(forward_subsumption_resolution,[status(thm)],[f6409,f6138])).
% 18.21/17.96 fof(f6415,plain,(
% 18.21/17.96 sQ35_spl),
% 18.21/17.96 inference(contradiction_clause,[status(thm)],[f6414])).
% 18.21/17.96 fof(f6417,plain,(
% 18.21/17.96 ![X0]: (~c_in(X0,v_S,t_a)|c_in(X0,v_A,t_a)|~sQ36_spl)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6411,f5075])).
% 18.21/17.96 fof(f6430,plain,(
% 18.21/17.96 ![X0]: (c_in(v_sko__4mj(v_S,v_sko__4mk(X0,v_S,v_r),v_r),v_A,t_a)|c_in(v_sko__4mk(X0,v_S,v_r),v_S,t_a)|c_in(c_Pair(v_sko__4mk(X0,v_S,v_r),X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|v_S=c_emptyset|~sQ36_spl|~sQ4_spl)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6417,f6187])).
% 18.21/17.96 fof(f6434,plain,(
% 18.21/17.96 ![X0,X1]: (c_in(v_sko__4mj(v_S,X0,v_r),v_A,t_a)|c_in(v_sko__4mj(v_S,v_sko__4mk(X1,v_S,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|v_S=c_emptyset|~sQ36_spl|~sQ4_spl)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6417,f6187])).
% 18.21/17.96 fof(f6435,definition,(
% 18.21/17.96 ![X0,X1]: (sQ39_spl <=> (c_in(v_sko__4mk(X0,v_S,v_r),v_A,t_a)|c_in(c_Pair(X1,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X1,v_r),v_S,t_a)))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6439,definition,(
% 18.21/17.96 ![X0]: (sQ40_spl <=> (c_in(v_sko__4mj(v_S,v_sko__4mk(X0,v_S,v_r),v_r),v_A,t_a)|c_in(v_sko__4mk(X0,v_S,v_r),v_S,t_a)|c_in(c_Pair(v_sko__4mk(X0,v_S,v_r),X0,t_a,t_a),v_r,tc_prod(t_a,t_a))))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6442,plain,(
% 18.21/17.96 sQ40_spl|sQ5_spl|~sQ36_spl|~sQ4_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6430,f6439,f6174,f6410,f6171])).
% 18.21/17.96 fof(f6443,definition,(
% 18.21/17.96 ![X0,X1]: (sQ41_spl <=> (c_in(v_sko__4mj(v_S,X0,v_r),v_A,t_a)|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6448,definition,(
% 18.21/17.96 ![X0,X1]: (sQ42_spl <=> (c_in(v_sko__4mj(v_S,X0,v_r),v_A,t_a)|c_in(v_sko__4mj(v_S,v_sko__4mk(X1,v_S,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6451,plain,(
% 18.21/17.96 sQ42_spl|sQ5_spl|~sQ36_spl|~sQ4_spl),
% 18.21/17.96 inference(split_clause,[status(thm)],[f6434,f6448,f6174,f6410,f6171])).
% 18.21/17.96 fof(f6456,plain,(
% 18.21/17.96 ![X0,X1]: (~c_in(X0,v_A,t_a)|~c_in(X1,c_Tarski_Ointerval(v_r,v_a,X0,t_a),t_a)|c_in(X1,v_A,t_a))),
% 18.21/17.96 inference(resolution,[status(thm)],[f6405,f5075])).
% 18.21/17.96 fof(f6458,plain,(
% 18.21/17.96 ![X0,X1,X2]: (~c_in(v_sko__4mk(v_L,X0,v_r),v_S,t_a)|~c_lessequals(X0,X1,tc_set(t_a))|c_in(c_Pair(X2,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(X0,X2,v_r),X0,t_a)|X0=c_emptyset)),
% 18.21/17.96 inference(resolution,[status(thm)],[f6271,f2762])).
% 18.21/17.96 fof(f6469,definition,(
% 18.21/17.96 sQ44_spl <=> (c_in(v_sko__4mj(c_emptyset,v_L,v_r),c_emptyset,t_a))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6470,plain,(
% 18.21/17.96 c_in(v_sko__4mj(c_emptyset,v_L,v_r),c_emptyset,t_a)|~sQ44_spl),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6469])).
% 18.21/17.96 fof(f6488,definition,(
% 18.21/17.96 sQ45_spl <=> (c_in(v_a,v_A,t_a))),
% 18.21/17.96 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 18.21/17.96 fof(f6490,plain,(
% 18.21/17.96 ~c_in(v_a,v_A,t_a)|sQ45_spl),
% 18.21/17.96 inference(component_clause,[status(thm)],[f6488])).
% 18.21/17.97 fof(f6493,plain,(
% 18.21/17.97 ![X0,X1,X2]: (~c_lessequals(X0,X1,tc_set(t_a))|c_in(c_Pair(X2,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(X0,X2,v_r),X0,t_a)|X0=c_emptyset|~c_in(v_sko__4mk(v_b,X0,v_r),v_S,t_a))),
% 18.21/17.97 inference(resolution,[status(thm)],[f6179,f6139])).
% 18.21/17.97 fof(f6511,definition,(
% 18.21/17.97 sQ47_spl <=> (c_in(v_sko__4mj(c_emptyset,v_a,v_r),c_emptyset,t_a))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6512,plain,(
% 18.21/17.97 c_in(v_sko__4mj(c_emptyset,v_a,v_r),c_emptyset,t_a)|~sQ47_spl),
% 18.21/17.97 inference(component_clause,[status(thm)],[f6511])).
% 18.21/17.97 fof(f6534,plain,(
% 18.21/17.97 ![X0]: (~c_in(v_b,v_A,t_a)|c_in(X0,v_A,t_a)|~c_in(X0,v_S,t_a))),
% 18.21/17.97 inference(resolution,[status(thm)],[f6456,f6234])).
% 18.21/17.97 fof(f6536,definition,(
% 18.21/17.97 ![X0]: (sQ48_spl <=> (c_in(X0,v_A,t_a)|~c_in(X0,v_S,t_a)))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6539,plain,(
% 18.21/17.97 ~sQ35_spl|sQ48_spl),
% 18.21/17.97 inference(split_clause,[status(thm)],[f6534,f6407,f6536])).
% 18.21/17.97 fof(f6564,plain,(
% 18.21/17.97 ~c_in(c_Pair(v_sko__4mi(v_S,v_r,v_b),v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(v_L,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))),
% 18.21/17.97 inference(resolution,[status(thm)],[f6394,f6138])).
% 18.21/17.97 fof(f6568,plain,(
% 18.21/17.97 ![X0,X1]: (~c_in(c_Pair(v_sko__4mi(v_S,v_r,v_sko__4mk(X0,v_A,v_r)),v_sko__4mk(X0,v_A,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(v_L,v_sko__4mk(X0,v_A,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(X1,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_A,X1,v_r),v_A,t_a)|v_A=c_emptyset)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6394,f6163])).
% 18.21/17.97 fof(f6570,plain,(
% 18.21/17.97 ![X0,X1]: (~c_in(c_Pair(v_sko__4mi(v_S,v_r,v_sko__4mj(v_A,X0,v_r)),v_sko__4mj(v_A,X0,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(v_L,v_sko__4mj(v_A,X0,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_A,v_r),v_A,t_a)|v_A=c_emptyset)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6394,f6163])).
% 18.21/17.97 fof(f6571,plain,(
% 18.21/17.97 ![X0,X1]: (~c_in(c_Pair(v_sko__4mi(v_S,v_r,v_sko__4mj(v_A,X0,v_r)),v_sko__4mj(v_A,X0,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(v_L,v_sko__4mj(v_A,X0,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,v_sko__4mk(X1,v_A,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|v_A=c_emptyset|~sQ4_spl)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6394,f6187])).
% 18.21/17.97 fof(f6572,definition,(
% 18.21/17.97 sQ50_spl <=> (c_in(c_Pair(v_sko__4mi(v_S,v_r,v_b),v_b,t_a,t_a),v_r,tc_prod(t_a,t_a)))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6574,plain,(
% 18.21/17.97 ~c_in(c_Pair(v_sko__4mi(v_S,v_r,v_b),v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))|sQ50_spl),
% 18.21/17.97 inference(component_clause,[status(thm)],[f6572])).
% 18.21/17.97 fof(f6575,plain,(
% 18.21/17.97 ~sQ50_spl|sQ14_spl),
% 18.21/17.97 inference(split_clause,[status(thm)],[f6564,f6572,f6250])).
% 18.21/17.97 fof(f6600,definition,(
% 18.21/17.97 ![X0,X1]: (sQ58_spl <=> (~c_in(c_Pair(v_sko__4mi(v_S,v_r,v_sko__4mk(X0,v_A,v_r)),v_sko__4mk(X0,v_A,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(v_L,v_sko__4mk(X0,v_A,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(X1,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_A,X1,v_r),v_A,t_a)))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6603,plain,(
% 18.21/17.97 sQ58_spl|sQ17_spl),
% 18.21/17.97 inference(split_clause,[status(thm)],[f6568,f6600,f6263])).
% 18.21/17.97 fof(f6611,definition,(
% 18.21/17.97 ![X0,X1]: (sQ61_spl <=> (~c_in(c_Pair(v_sko__4mi(v_S,v_r,v_sko__4mj(v_A,X0,v_r)),v_sko__4mj(v_A,X0,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(v_L,v_sko__4mj(v_A,X0,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_A,v_r),v_A,t_a)))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6614,plain,(
% 18.21/17.97 sQ61_spl|sQ17_spl),
% 18.21/17.97 inference(split_clause,[status(thm)],[f6570,f6611,f6263])).
% 18.21/17.97 fof(f6615,definition,(
% 18.21/17.97 ![X0,X1]: (sQ62_spl <=> (~c_in(c_Pair(v_sko__4mi(v_S,v_r,v_sko__4mj(v_A,X0,v_r)),v_sko__4mj(v_A,X0,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(c_Pair(v_L,v_sko__4mj(v_A,X0,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,v_sko__4mk(X1,v_A,v_r),v_r),v_S,t_a)|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6618,plain,(
% 18.21/17.97 sQ62_spl|sQ17_spl|~sQ4_spl),
% 18.21/17.97 inference(split_clause,[status(thm)],[f6571,f6615,f6263,f6171])).
% 18.21/17.97 fof(f6695,plain,(
% 18.21/17.97 ![X0,X1,X2]: (~c_lessequals(X0,X1,tc_set(t_a))|c_in(c_Pair(v_a,X2,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X2,X0,v_r),X0,t_a)|X0=c_emptyset|~c_in(v_sko__4mj(X0,v_a,v_r),v_S,t_a))),
% 18.21/17.97 inference(resolution,[status(thm)],[f6182,f6139])).
% 18.21/17.97 fof(f6702,definition,(
% 18.21/17.97 ![X0]: (sQ78_spl <=> (~c_lessequals(v_S,X0,tc_set(t_a))))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6703,plain,(
% 18.21/17.97 ![X0]: (~c_lessequals(v_S,X0,tc_set(t_a))|~sQ78_spl)),
% 18.21/17.97 inference(component_clause,[status(thm)],[f6702])).
% 18.21/17.97 fof(f6709,plain,(
% 18.21/17.97 $false|~sQ78_spl|~sQ36_spl),
% 18.21/17.97 inference(backward_subsumption_resolution,[status(thm)],[f6411,f6703])).
% 18.21/17.97 fof(f6712,plain,(
% 18.21/17.97 ~sQ78_spl|~sQ36_spl),
% 18.21/17.97 inference(contradiction_clause,[status(thm)],[f6709])).
% 18.21/17.97 fof(f6768,definition,(
% 18.21/17.97 sQ86_spl <=> (c_in(v_sko__4mk(v_a,c_emptyset,v_r),c_emptyset,t_a))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6769,plain,(
% 18.21/17.97 c_in(v_sko__4mk(v_a,c_emptyset,v_r),c_emptyset,t_a)|~sQ86_spl),
% 18.21/17.97 inference(component_clause,[status(thm)],[f6768])).
% 18.21/17.97 fof(f6772,plain,(
% 18.21/17.97 $false|~sQ86_spl),
% 18.21/17.97 inference(forward_subsumption_resolution,[status(thm)],[f6769,f4861])).
% 18.21/17.97 fof(f6773,plain,(
% 18.21/17.97 ~sQ86_spl),
% 18.21/17.97 inference(contradiction_clause,[status(thm)],[f6772])).
% 18.21/17.97 fof(f6783,plain,(
% 18.21/17.97 ![X0,X1,X2]: (c_in(v_sko__4mj(X0,v_sko__4mk(X1,v_S,v_r),v_r),X0,t_a)|c_in(v_sko__4mk(X1,X0,v_r),X0,t_a)|X0=c_emptyset|c_in(c_Pair(X2,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X2,v_r),v_S,t_a)|v_S=c_emptyset)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6364,f6139])).
% 18.21/17.97 fof(f6789,definition,(
% 18.21/17.97 ![X0,X1,X2]: (sQ89_spl <=> (c_in(v_sko__4mj(X0,v_sko__4mk(X1,v_S,v_r),v_r),X0,t_a)|c_in(v_sko__4mk(X1,X0,v_r),X0,t_a)|X0=c_emptyset|c_in(c_Pair(X2,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X2,v_r),v_S,t_a)))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6793,plain,(
% 18.21/17.97 sQ89_spl|sQ5_spl),
% 18.21/17.97 inference(split_clause,[status(thm)],[f6783,f6789,f6174])).
% 18.21/17.97 fof(f6800,plain,(
% 18.21/17.97 ![X0,X1,X2]: (c_in(v_sko__4mj(X0,X1,v_r),X0,t_a)|c_in(v_sko__4mk(v_sko__4mj(v_S,X1,v_r),X0,v_r),X0,t_a)|X0=c_emptyset|c_in(c_Pair(X1,X2,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X2,v_S,v_r),v_S,t_a)|v_S=c_emptyset)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6365,f6139])).
% 18.21/17.97 fof(f6806,definition,(
% 18.21/17.97 ![X0,X1,X2]: (sQ91_spl <=> (c_in(v_sko__4mj(X0,X1,v_r),X0,t_a)|c_in(v_sko__4mk(v_sko__4mj(v_S,X1,v_r),X0,v_r),X0,t_a)|X0=c_emptyset|c_in(c_Pair(X1,X2,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X2,v_S,v_r),v_S,t_a)))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6810,plain,(
% 18.21/17.97 sQ91_spl|sQ5_spl),
% 18.21/17.97 inference(split_clause,[status(thm)],[f6800,f6806,f6174])).
% 18.21/17.97 fof(f6857,plain,(
% 18.21/17.97 ![X0,X1,X2]: (~c_lessequals(v_S,X0,tc_set(t_a))|c_in(c_Pair(X1,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X1,v_r),v_S,t_a)|v_S=c_emptyset|c_in(c_Pair(X2,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X2,v_r),v_S,t_a)|v_S=c_emptyset)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6458,f6163])).
% 18.21/17.97 fof(f6858,definition,(
% 18.21/17.97 ![X1]: (sQ100_spl <=> (c_in(c_Pair(X1,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X1,v_r),v_S,t_a)))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6859,plain,(
% 18.21/17.97 ![X0]: (c_in(c_Pair(X0,v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X0,v_r),v_S,t_a)|~sQ100_spl)),
% 18.21/17.97 inference(component_clause,[status(thm)],[f6858])).
% 18.21/17.97 fof(f6863,plain,(
% 18.21/17.97 sQ78_spl|sQ100_spl|sQ5_spl),
% 18.21/17.97 inference(split_clause,[status(thm)],[f6857,f6702,f6858,f6174])).
% 18.21/17.97 fof(f6874,plain,(
% 18.21/17.97 $false|~sQ47_spl),
% 18.21/17.97 inference(forward_subsumption_resolution,[status(thm)],[f6512,f4861])).
% 18.21/17.97 fof(f6875,plain,(
% 18.21/17.97 ~sQ47_spl),
% 18.21/17.97 inference(contradiction_clause,[status(thm)],[f6874])).
% 18.21/17.97 fof(f6876,plain,(
% 18.21/17.97 $false|~sQ44_spl),
% 18.21/17.97 inference(forward_subsumption_resolution,[status(thm)],[f6470,f4861])).
% 18.21/17.97 fof(f6877,plain,(
% 18.21/17.97 ~sQ44_spl),
% 18.21/17.97 inference(contradiction_clause,[status(thm)],[f6876])).
% 18.21/17.97 fof(f6961,plain,(
% 18.21/17.97 ![X0,X1]: (c_in(v_sko__4mk(X0,v_S,v_r),c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a)|c_in(c_Pair(X1,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X1,v_r),v_S,t_a)|v_S=c_emptyset)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6234,f6163])).
% 18.21/17.97 fof(f6962,plain,(
% 18.21/17.97 ![X0,X1]: (c_in(v_sko__4mj(v_S,X0,v_r),c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a)|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)|v_S=c_emptyset)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6234,f6163])).
% 18.21/17.97 fof(f6967,definition,(
% 18.21/17.97 ![X0,X1]: (sQ104_spl <=> (c_in(v_sko__4mk(X0,v_S,v_r),c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a)|c_in(c_Pair(X1,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X1,v_r),v_S,t_a)))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6968,plain,(
% 18.21/17.97 ![X0,X1]: (c_in(v_sko__4mk(X0,v_S,v_r),c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a)|c_in(c_Pair(X1,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X1,v_r),v_S,t_a)|~sQ104_spl)),
% 18.21/17.97 inference(component_clause,[status(thm)],[f6967])).
% 18.21/17.97 fof(f6970,plain,(
% 18.21/17.97 sQ104_spl|sQ5_spl),
% 18.21/17.97 inference(split_clause,[status(thm)],[f6961,f6967,f6174])).
% 18.21/17.97 fof(f6971,definition,(
% 18.21/17.97 ![X0,X1]: (sQ105_spl <=> (c_in(v_sko__4mj(v_S,X0,v_r),c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a)|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f6972,plain,(
% 18.21/17.97 ![X0,X1]: (c_in(v_sko__4mj(v_S,X0,v_r),c_Tarski_Ointerval(v_r,v_a,v_b,t_a),t_a)|c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)|~sQ105_spl)),
% 18.21/17.97 inference(component_clause,[status(thm)],[f6971])).
% 18.21/17.97 fof(f6974,plain,(
% 18.21/17.97 sQ105_spl|sQ5_spl),
% 18.21/17.97 inference(split_clause,[status(thm)],[f6962,f6971,f6174])).
% 18.21/17.97 fof(f6977,plain,(
% 18.21/17.97 ![X0,X1]: (~c_in(X0,v_A,t_a)|c_in(c_Pair(v_L,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(X1,v_sko__4mi(v_S,v_r,X0),v_r),X1,t_a)|c_in(v_sko__4mk(X0,X1,v_r),X1,t_a)|X1=c_emptyset)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6394,f6163])).
% 18.21/17.97 fof(f7152,plain,(
% 18.21/17.97 $false|sQ45_spl),
% 18.21/17.97 inference(forward_subsumption_resolution,[status(thm)],[f6490,f6137])).
% 18.21/17.97 fof(f7153,plain,(
% 18.21/17.97 sQ45_spl),
% 18.21/17.97 inference(contradiction_clause,[status(thm)],[f7152])).
% 18.21/17.97 fof(f7296,plain,(
% 18.21/17.97 ![X0,X1,X2]: (~c_lessequals(v_S,X0,tc_set(t_a))|c_in(c_Pair(X1,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X1,v_r),v_S,t_a)|v_S=c_emptyset|c_in(c_Pair(X2,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X2,v_r),v_S,t_a)|v_S=c_emptyset)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6493,f6163])).
% 18.21/17.97 fof(f7297,definition,(
% 18.21/17.97 ![X1]: (sQ123_spl <=> (c_in(c_Pair(X1,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X1,v_r),v_S,t_a)))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f7300,plain,(
% 18.21/17.97 sQ78_spl|sQ123_spl|sQ5_spl),
% 18.21/17.97 inference(split_clause,[status(thm)],[f7296,f6702,f7297,f6174])).
% 18.21/17.97 fof(f7357,definition,(
% 18.21/17.97 ![X0]: (sQ127_spl <=> (~c_lessequals(v_A,X0,tc_set(t_a))))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f7358,plain,(
% 18.21/17.97 ![X0]: (~c_lessequals(v_A,X0,tc_set(t_a))|~sQ127_spl)),
% 18.21/17.97 inference(component_clause,[status(thm)],[f7357])).
% 18.21/17.97 fof(f7364,plain,(
% 18.21/17.97 $false|~sQ127_spl),
% 18.21/17.97 inference(resolution,[status(thm)],[f7358,f5080])).
% 18.21/17.97 fof(f7365,plain,(
% 18.21/17.97 ~sQ127_spl),
% 18.21/17.97 inference(contradiction_clause,[status(thm)],[f7364])).
% 18.21/17.97 fof(f7382,definition,(
% 18.21/17.97 sQ130_spl <=> (c_in(c_Pair(v_sko__4mk(v_L,v_S,v_r),v_L,t_a,t_a),v_r,tc_prod(t_a,t_a)))),
% 18.21/17.97 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 18.21/17.97 fof(f7384,plain,(
% 18.21/17.97 ~c_in(c_Pair(v_sko__4mk(v_L,v_S,v_r),v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))|sQ130_spl),
% 18.21/17.97 inference(component_clause,[status(thm)],[f7382])).
% 18.21/17.97 fof(f7391,plain,(
% 18.21/17.97 $false|~sQ29_spl),
% 18.21/17.97 inference(resolution,[status(thm)],[f6339,f5080])).
% 18.21/17.97 fof(f7392,plain,(
% 18.21/17.97 ~sQ29_spl),
% 18.21/17.97 inference(contradiction_clause,[status(thm)],[f7391])).
% 18.21/17.97 fof(f7504,plain,(
% 18.21/17.97 ![X0]: (~c_Tarski_OisLub(X0,v_cl,v_L,t_a)|~c_in(v_sko__4mk(v_L,v_S,v_r),X0,t_a)|sQ130_spl)),
% 18.21/17.97 inference(resolution,[status(thm)],[f7384,f2775])).
% 18.21/17.97 fof(f7507,plain,(
% 18.21/17.97 ~c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)|sQ130_spl),
% 18.21/17.97 inference(resolution,[status(thm)],[f7504,f6141])).
% 18.21/17.97 fof(f7553,plain,(
% 18.21/17.97 ![X0,X1]: (~c_in(v_sko__4mi(v_S,v_r,v_b),X0,t_a)|~c_lessequals(X0,c_Tarski_Ointerval(v_r,X1,v_b,t_a),tc_set(t_a))|sQ50_spl)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6574,f2770])).
% 18.21/17.97 fof(f7737,plain,(
% 18.21/17.97 ![X0,X1,X2]: (~c_lessequals(v_S,X0,tc_set(t_a))|c_in(c_Pair(v_a,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)|v_S=c_emptyset|c_in(c_Pair(v_a,X2,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X2,v_S,v_r),v_S,t_a)|v_S=c_emptyset)),
% 18.21/17.97 inference(resolution,[status(thm)],[f6695,f6163])).
% 18.21/17.98 fof(f7738,definition,(
% 18.21/17.98 ![X1]: (sQ141_spl <=> (c_in(c_Pair(v_a,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)))),
% 18.21/17.98 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 18.21/17.98 fof(f7739,plain,(
% 18.21/17.98 ![X0]: (c_in(c_Pair(v_a,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X0,v_S,v_r),v_S,t_a)|~sQ141_spl)),
% 18.21/17.98 inference(component_clause,[status(thm)],[f7738])).
% 18.21/17.98 fof(f7744,plain,(
% 18.21/17.98 sQ78_spl|sQ141_spl|sQ5_spl),
% 18.21/17.98 inference(split_clause,[status(thm)],[f7737,f6702,f7738,f6174])).
% 18.21/17.98 fof(f8048,plain,(
% 18.21/17.98 ![X0,X1]: (c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mj(v_S,X0,v_r),v_S,t_a)|~c_in(v_b,v_A,t_a)|c_in(v_sko__4mk(X1,v_S,v_r),v_A,t_a)|~sQ104_spl)),
% 18.21/17.98 inference(resolution,[status(thm)],[f6968,f6456])).
% 18.21/17.98 fof(f8058,plain,(
% 18.21/17.98 sQ39_spl|~sQ35_spl|~sQ104_spl),
% 18.21/17.98 inference(split_clause,[status(thm)],[f8048,f6435,f6407,f6967])).
% 18.21/17.98 fof(f8086,plain,(
% 18.21/17.98 ![X0,X1]: (c_in(c_Pair(X0,X1,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X1,v_S,v_r),v_S,t_a)|~c_in(v_b,v_A,t_a)|c_in(v_sko__4mj(v_S,X0,v_r),v_A,t_a)|~sQ105_spl)),
% 18.21/17.98 inference(resolution,[status(thm)],[f6972,f6456])).
% 18.21/17.98 fof(f8093,plain,(
% 18.21/17.98 sQ41_spl|~sQ35_spl|~sQ105_spl),
% 18.21/17.98 inference(split_clause,[status(thm)],[f8086,f6443,f6407,f6971])).
% 18.21/17.98 fof(f8176,plain,(
% 18.21/17.98 ![X0]: (~c_in(X0,v_A,t_a)|c_in(c_Pair(v_L,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X0,v_S,v_r),v_S,t_a)|v_S=c_emptyset|c_in(v_sko__4mj(v_S,v_sko__4mi(v_S,v_r,X0),v_r),v_A,t_a)|~sQ36_spl)),
% 18.21/17.98 inference(resolution,[status(thm)],[f6977,f6417])).
% 18.21/17.98 fof(f8189,definition,(
% 18.21/17.98 ![X0]: (sQ169_spl <=> (~c_in(X0,v_A,t_a)|c_in(c_Pair(v_L,X0,t_a,t_a),v_r,tc_prod(t_a,t_a))|c_in(v_sko__4mk(X0,v_S,v_r),v_S,t_a)|c_in(v_sko__4mj(v_S,v_sko__4mi(v_S,v_r,X0),v_r),v_A,t_a)))),
% 18.21/17.98 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 18.21/17.98 fof(f8192,plain,(
% 18.21/17.98 sQ169_spl|sQ5_spl|~sQ36_spl),
% 18.21/17.98 inference(split_clause,[status(thm)],[f8176,f8189,f6174,f6410])).
% 18.21/17.98 fof(f8316,definition,(
% 18.21/17.98 sQ176_spl <=> (c_Datatype_Ooption_ONone=c_Datatype_Ooption_OSome(v_sko__4mk(v_L,c_Datatype_Oo2s(c_Datatype_Ooption_ONone,t_a),v_r),t_a))),
% 18.21/17.98 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 18.21/17.98 fof(f8317,plain,(
% 18.21/17.98 c_Datatype_Ooption_ONone=c_Datatype_Ooption_OSome(v_sko__4mk(v_L,c_Datatype_Oo2s(c_Datatype_Ooption_ONone,t_a),v_r),t_a)|~sQ176_spl),
% 18.21/17.98 inference(component_clause,[status(thm)],[f8316])).
% 18.21/17.98 fof(f8319,definition,(
% 18.21/17.98 sQ177_spl <=> (c_in(v_sko__4mj(c_emptyset,v_a,v_r),c_Datatype_Oo2s(c_Datatype_Ooption_ONone,t_a),t_a))),
% 18.21/17.98 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 18.21/17.98 fof(f8320,plain,(
% 18.21/17.98 c_in(v_sko__4mj(c_emptyset,v_a,v_r),c_Datatype_Oo2s(c_Datatype_Ooption_ONone,t_a),t_a)|~sQ177_spl),
% 18.21/17.98 inference(component_clause,[status(thm)],[f8319])).
% 18.21/17.98 fof(f8329,definition,(
% 18.21/17.98 sQ179_spl <=> (c_in(v_sko__4mj(c_Datatype_Oo2s(c_Datatype_Ooption_ONone,t_a),v_a,v_r),c_emptyset,t_a))),
% 18.21/17.98 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 18.21/17.98 fof(f8330,plain,(
% 18.21/17.98 c_in(v_sko__4mj(c_Datatype_Oo2s(c_Datatype_Ooption_ONone,t_a),v_a,v_r),c_emptyset,t_a)|~sQ179_spl),
% 18.21/17.98 inference(component_clause,[status(thm)],[f8329])).
% 18.21/17.98 fof(f8336,plain,(
% 18.21/17.98 c_Datatype_Ooption_ONone=c_Datatype_Ooption_OSome(v_sko__4mk(v_L,c_emptyset,v_r),t_a)|~sQ176_spl),
% 18.21/17.98 inference(forward_demodulation,[status(thm)],[f2811,f8317])).
% 18.21/17.98 fof(f8337,plain,(
% 18.21/17.98 $false|~sQ176_spl),
% 18.21/17.98 inference(forward_subsumption_resolution,[status(thm)],[f8336,f2812])).
% 18.21/17.98 fof(f8338,plain,(
% 18.21/17.98 ~sQ176_spl),
% 18.21/17.98 inference(contradiction_clause,[status(thm)],[f8337])).
% 18.21/17.98 fof(f8339,plain,(
% 18.21/17.98 c_in(v_sko__4mj(c_emptyset,v_a,v_r),c_emptyset,t_a)|~sQ179_spl),
% 18.21/17.98 inference(forward_demodulation,[status(thm)],[f2811,f8330])).
% 18.21/17.98 fof(f8340,plain,(
% 18.21/17.98 $false|~sQ179_spl),
% 18.21/17.98 inference(forward_subsumption_resolution,[status(thm)],[f8339,f4861])).
% 18.21/17.98 fof(f8341,plain,(
% 18.21/17.98 ~sQ179_spl),
% 18.21/17.98 inference(contradiction_clause,[status(thm)],[f8340])).
% 18.21/17.98 fof(f8342,plain,(
% 18.21/17.98 c_in(v_sko__4mj(c_emptyset,v_a,v_r),c_emptyset,t_a)|~sQ177_spl),
% 18.21/17.98 inference(forward_demodulation,[status(thm)],[f2811,f8320])).
% 18.21/17.98 fof(f8343,plain,(
% 18.21/17.98 $false|~sQ177_spl),
% 18.21/17.98 inference(forward_subsumption_resolution,[status(thm)],[f8342,f4861])).
% 18.21/17.98 fof(f8344,plain,(
% 18.21/17.98 ~sQ177_spl),
% 18.21/17.98 inference(contradiction_clause,[status(thm)],[f8343])).
% 18.21/17.98 fof(f8362,definition,(
% 18.21/17.98 sQ180_spl <=> (c_Datatype_Ooption_ONone=c_Datatype_Ooption_OSome(v_sko__4mj(c_Datatype_Oo2s(c_Datatype_Ooption_ONone,t_a),v_a,v_r),t_a))),
% 18.21/17.98 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 18.21/17.98 fof(f8363,plain,(
% 18.21/17.98 c_Datatype_Ooption_ONone=c_Datatype_Ooption_OSome(v_sko__4mj(c_Datatype_Oo2s(c_Datatype_Ooption_ONone,t_a),v_a,v_r),t_a)|~sQ180_spl),
% 18.21/17.98 inference(component_clause,[status(thm)],[f8362])).
% 18.21/17.98 fof(f8369,definition,(
% 18.21/17.98 sQ181_spl <=> (c_Datatype_Ooption_ONone=c_Datatype_Ooption_OSome(v_sko__4mk(v_L,c_emptyset,v_r),t_a))),
% 18.21/17.98 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 18.21/17.98 fof(f8370,plain,(
% 18.21/17.98 c_Datatype_Ooption_ONone=c_Datatype_Ooption_OSome(v_sko__4mk(v_L,c_emptyset,v_r),t_a)|~sQ181_spl),
% 18.21/17.98 inference(component_clause,[status(thm)],[f8369])).
% 18.21/17.98 fof(f8378,plain,(
% 18.21/17.98 c_Datatype_Ooption_ONone=c_Datatype_Ooption_OSome(v_sko__4mj(c_emptyset,v_a,v_r),t_a)|~sQ180_spl),
% 18.21/17.98 inference(forward_demodulation,[status(thm)],[f2811,f8363])).
% 18.21/17.98 fof(f8379,plain,(
% 18.21/17.98 $false|~sQ180_spl),
% 18.21/17.98 inference(forward_subsumption_resolution,[status(thm)],[f8378,f2812])).
% 18.21/17.98 fof(f8380,plain,(
% 18.21/17.98 ~sQ180_spl),
% 18.21/17.98 inference(contradiction_clause,[status(thm)],[f8379])).
% 18.21/17.98 fof(f8381,plain,(
% 18.21/17.98 $false|~sQ181_spl),
% 18.21/17.98 inference(forward_subsumption_resolution,[status(thm)],[f8370,f2812])).
% 18.21/17.98 fof(f8382,plain,(
% 18.21/17.98 ~sQ181_spl),
% 18.21/17.98 inference(contradiction_clause,[status(thm)],[f8381])).
% 18.21/17.98 fof(f8472,definition,(
% 18.21/17.98 ![X0]: (sQ189_spl <=> (~c_lessequals(c_emptyset,X0,tc_set(t_a))))),
% 18.21/17.98 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 18.21/17.98 fof(f8473,plain,(
% 18.21/17.98 ![X0]: (~c_lessequals(c_emptyset,X0,tc_set(t_a))|~sQ189_spl)),
% 18.21/17.98 inference(component_clause,[status(thm)],[f8472])).
% 18.21/17.98 fof(f8487,definition,(
% 18.21/17.98 sQ193_spl <=> (c_in(c_Datatype_Othe(c_Datatype_Ooption_ONone,t_a),c_emptyset,t_a))),
% 18.21/17.98 introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition])).
% 18.21/17.98 fof(f8488,plain,(
% 18.21/17.98 c_in(c_Datatype_Othe(c_Datatype_Ooption_ONone,t_a),c_emptyset,t_a)|~sQ193_spl),
% 18.21/17.98 inference(component_clause,[status(thm)],[f8487])).
% 18.21/17.98 fof(f8501,plain,(
% 18.21/17.98 $false|~sQ189_spl),
% 18.21/17.98 inference(forward_subsumption_resolution,[status(thm)],[f8473,f5064])).
% 18.21/17.98 fof(f8502,plain,(
% 18.21/17.98 ~sQ189_spl),
% 18.21/17.98 inference(contradiction_clause,[status(thm)],[f8501])).
% 18.21/17.98 fof(f8503,plain,(
% 18.21/17.98 $false|~sQ193_spl),
% 18.21/17.98 inference(forward_subsumption_resolution,[status(thm)],[f8488,f4861])).
% 18.21/17.98 fof(f8504,plain,(
% 18.21/17.98 ~sQ193_spl),
% 18.21/17.98 inference(contradiction_clause,[status(thm)],[f8503])).
% 18.21/17.98 fof(f8590,plain,(
% 18.21/17.98 c_in(v_sko__4mk(v_L,v_S,v_r),v_S,t_a)|sQ15_spl|~sQ141_spl),
% 18.21/17.98 inference(resolution,[status(thm)],[f6255,f7739])).
% 18.21/17.98 fof(f8688,definition,(
% 18.21/17.98 sQ200_spl <=> (c_in(v_sko__4mk(v_L,c_emptyset,v_r),c_emptyset,t_a))),
% 18.21/17.98 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 18.21/17.98 fof(f8689,plain,(
% 18.21/17.98 c_in(v_sko__4mk(v_L,c_emptyset,v_r),c_emptyset,t_a)|~sQ200_spl),
% 18.21/17.98 inference(component_clause,[status(thm)],[f8688])).
% 18.21/17.98 fof(f8692,plain,(
% 18.21/17.98 $false|~sQ200_spl),
% 18.21/17.98 inference(forward_subsumption_resolution,[status(thm)],[f8689,f4861])).
% 18.21/17.98 fof(f8693,plain,(
% 18.21/17.98 ~sQ200_spl),
% 18.21/17.98 inference(contradiction_clause,[status(thm)],[f8692])).
% 18.21/17.98 fof(f8695,plain,(
% 18.21/17.98 c_in(v_sko__4mj(v_S,v_a,v_r),v_S,t_a)|~sQ100_spl|sQ15_spl),
% 18.21/17.98 inference(resolution,[status(thm)],[f6859,f6255])).
% 18.21/17.98 fof(f8859,plain,(
% 18.21/17.98 ~c_in(c_Pair(v_a,v_sko__4mj(v_S,v_a,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|~c_in(c_Pair(v_sko__4mk(v_L,v_S,v_r),v_L,t_a,t_a),v_r,tc_prod(t_a,t_a))|v_S=c_emptyset|sQ15_spl),
% 18.21/17.98 inference(resolution,[status(thm)],[f6300,f6139])).
% 18.21/17.98 fof(f8866,definition,(
% 18.21/17.98 sQ211_spl <=> (c_in(c_Pair(v_a,v_sko__4mj(v_S,v_a,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a)))),
% 18.21/17.98 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 18.21/17.98 fof(f8868,plain,(
% 18.21/17.98 ~c_in(c_Pair(v_a,v_sko__4mj(v_S,v_a,v_r),t_a,t_a),v_r,tc_prod(t_a,t_a))|sQ211_spl),
% 18.21/18.01 inference(component_clause,[status(thm)],[f8866])).
% 18.21/18.01 fof(f8869,plain,(
% 18.21/18.01 ~sQ211_spl|~sQ130_spl|sQ5_spl|sQ15_spl),
% 18.21/18.01 inference(split_clause,[status(thm)],[f8859,f8866,f7382,f6174,f6253])).
% 18.21/18.01 fof(f8875,plain,(
% 18.21/18.01 $false|~sQ24_spl|sQ130_spl),
% 18.21/18.01 inference(forward_subsumption_resolution,[status(thm)],[f7507,f6309])).
% 18.21/18.01 fof(f8876,plain,(
% 18.21/18.01 ~sQ24_spl|sQ130_spl),
% 18.21/18.01 inference(contradiction_clause,[status(thm)],[f8875])).
% 18.21/18.01 fof(f8877,plain,(
% 18.21/18.01 sQ24_spl|sQ15_spl|~sQ141_spl),
% 18.21/18.01 inference(split_clause,[status(thm)],[f8590,f6308,f6253,f7738])).
% 18.21/18.01 fof(f9003,plain,(
% 18.21/18.01 ~c_in(v_b,v_A,t_a)|c_in(v_sko__4mi(v_S,v_r,v_b),v_S,t_a)|sQ14_spl),
% 18.21/18.01 inference(resolution,[status(thm)],[f6272,f6252])).
% 18.21/18.01 fof(f9004,definition,(
% 18.21/18.01 sQ218_spl <=> (c_in(v_sko__4mi(v_S,v_r,v_b),v_S,t_a))),
% 18.21/18.01 introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition])).
% 18.21/18.01 fof(f9005,plain,(
% 18.21/18.01 c_in(v_sko__4mi(v_S,v_r,v_b),v_S,t_a)|~sQ218_spl),
% 18.21/18.01 inference(component_clause,[status(thm)],[f9004])).
% 18.21/18.01 fof(f9007,plain,(
% 18.21/18.01 ~sQ35_spl|sQ218_spl|sQ14_spl),
% 18.21/18.01 inference(split_clause,[status(thm)],[f9003,f6407,f9004,f6250])).
% 18.21/18.01 fof(f9294,plain,(
% 18.21/18.01 ![X0,X1]: (~c_in(v_sko__4mj(v_S,v_a,v_r),X0,t_a)|~c_lessequals(X0,c_Tarski_Ointerval(v_r,v_a,X1,t_a),tc_set(t_a))|sQ211_spl)),
% 18.21/18.01 inference(resolution,[status(thm)],[f8868,f2768])).
% 18.21/18.01 fof(f9484,plain,(
% 18.21/18.01 ~c_in(v_sko__4mi(v_S,v_r,v_b),v_S,t_a)|sQ50_spl),
% 18.21/18.01 inference(resolution,[status(thm)],[f7553,f6139])).
% 18.21/18.01 fof(f9487,plain,(
% 18.21/18.01 $false|~sQ218_spl|sQ50_spl),
% 18.21/18.01 inference(forward_subsumption_resolution,[status(thm)],[f9484,f9005])).
% 18.21/18.01 fof(f9488,plain,(
% 18.21/18.01 ~sQ218_spl|sQ50_spl),
% 18.21/18.01 inference(contradiction_clause,[status(thm)],[f9487])).
% 18.21/18.01 fof(f9702,plain,(
% 18.21/18.01 ~c_in(v_sko__4mj(v_S,v_a,v_r),v_S,t_a)|sQ211_spl),
% 18.21/18.01 inference(resolution,[status(thm)],[f9294,f6139])).
% 18.21/18.01 fof(f9705,plain,(
% 18.21/18.01 ~sQ25_spl|sQ211_spl),
% 18.21/18.01 inference(split_clause,[status(thm)],[f9702,f6312,f8866])).
% 18.21/18.01 fof(f9706,plain,(
% 18.21/18.01 $false|~sQ100_spl|sQ15_spl|sQ25_spl),
% 18.21/18.01 inference(forward_subsumption_resolution,[status(thm)],[f6314,f8695])).
% 18.21/18.01 fof(f9707,plain,(
% 18.21/18.01 ~sQ100_spl|sQ15_spl|sQ25_spl),
% 18.21/18.01 inference(contradiction_clause,[status(thm)],[f9706])).
% 18.21/18.01 fof(f9708,plain,(
% 18.21/18.01 $false),
% 18.21/18.01 inference(sat_refutation,[status(thm)],[f6150,f6177,f6195,f6197,f6211,f6222,f6256,f6266,f6268,f6299,f6324,f6328,f6377,f6387,f6402,f6413,f6415,f6442,f6451,f6539,f6575,f6603,f6614,f6618,f6712,f6773,f6793,f6810,f6863,f6875,f6877,f6970,f6974,f7153,f7300,f7365,f7392,f7744,f8058,f8093,f8192,f8338,f8341,f8344,f8380,f8382,f8502,f8504,f8693,f8869,f8876,f8877,f9007,f9488,f9705,f9707])).
% 18.21/18.01 % SZS output end CNFRefutation for theBenchmark.p
% 1.01/18.03 % Elapsed time: 2.569353 seconds
% 1.01/18.03 % CPU time: 18.704754 seconds
% 1.01/18.03 % Total memory used: 348.855 MB
% 1.01/18.03 % Net memory used: 327.585 MB
%------------------------------------------------------------------------------