%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG349-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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 11:50:04 AM UTC 2026
% Result : Unsatisfiable 64.18s 8.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG349-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.38 % Computer : n008.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 21 13:17:38 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.41 % Drodi V4.1.1
% 64.18/8.56 % Refutation found
% 64.18/8.56 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 64.18/8.56 % SZS output start CNFRefutation for theBenchmark
% 64.18/8.56 fof(f109,axiom,(
% 64.18/8.56 (![V_a,T_a]: (~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)) ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f123,axiom,(
% 64.18/8.56 (![T_a,V_x]: (~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)) ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f158,axiom,(
% 64.18/8.56 (![T_a,V_P]: (hAPP(c_COMBI(T_a),V_P) = V_P ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f159,axiom,(
% 64.18/8.56 (![V_P,T_a,T_b,V_Q]: (hAPP(c_COMBK(V_P,T_a,T_b),V_Q) = V_P ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f241,axiom,(
% 64.18/8.56 (![V_x,V_S,T_a]: (( hBOOL(c_in(V_x,V_S,T_a))| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f242,axiom,(
% 64.18/8.56 (![V_S,V_x,T_a]: (( hBOOL(hAPP(V_S,V_x))| ~ hBOOL(c_in(V_x,V_S,T_a)) ) ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f307,axiom,(
% 64.18/8.56 (![T_a,V_x]: (hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_x)) ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f310,axiom,(
% 64.18/8.56 hBOOL(hAPP(v_P,v_x____)) ),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f318,axiom,(
% 64.18/8.56 (![V_P,T_a]: (c_Collect(V_P,T_a) = V_P ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f319,axiom,(
% 64.18/8.56 (![T_a,V_R,V_S]: (( ~ class_HOL_Oord(T_a)| c_Lubs_Oubs(V_R,V_S,T_a) = c_Collect(c_Lubs_OisUb(V_R,V_S,T_a),T_a) ) ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f322,axiom,(
% 64.18/8.56 (![T_a]: (c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) = c_Collect(c_COMBK(c_True,tc_bool,T_a),T_a) ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f323,axiom,(
% 64.18/8.56 (![V_P,T_a,V_Q]: (( c_Collect(V_P,T_a) = c_Collect(V_Q,T_a)| hBOOL(hAPP(V_Q,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(V_P,V_Q,T_a)))| hBOOL(hAPP(V_P,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(V_P,V_Q,T_a))) ) ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f324,axiom,(
% 64.18/8.56 (![V_P,T_a,V_Q]: (( c_Collect(V_P,T_a) = c_Collect(V_Q,T_a)| ~ hBOOL(hAPP(V_Q,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(V_P,V_Q,T_a)))| ~ hBOOL(hAPP(V_P,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(V_P,V_Q,T_a))) ) ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f338,axiom,(
% 64.18/8.56 (![T_a]: (c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f349,axiom,(
% 64.18/8.56 hBOOL(hAPP(v_P,v_sko__local__Xassms__1__1(v_P))) ),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f354,negated_conjecture,(
% 64.18/8.56 (![V_x]: (~ hBOOL(hAPP(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),c_Collect(v_P,tc_RealDef_Oreal),tc_RealDef_Oreal),V_x)) ))),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f392,axiom,(
% 64.18/8.56 class_HOL_Oord(tc_RealDef_Oreal) ),
% 64.18/8.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 64.18/8.56 fof(f582,plain,(
% 64.18/8.56 ![X0,X1]: (~hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f109])).
% 64.18/8.56 fof(f601,plain,(
% 64.18/8.56 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f123])).
% 64.18/8.56 fof(f657,plain,(
% 64.18/8.56 ![X0,X1]: (hAPP(c_COMBI(X0),X1)=X1)),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f158])).
% 64.18/8.56 fof(f658,plain,(
% 64.18/8.56 ![X0,X1,X2,X3]: (hAPP(c_COMBK(X0,X1,X2),X3)=X0)),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f159])).
% 64.18/8.56 fof(f801,plain,(
% 64.18/8.56 ![V_x,V_S]: ((![T_a]: hBOOL(c_in(V_x,V_S,T_a)))|~hBOOL(hAPP(V_S,V_x)))),
% 64.18/8.56 inference(miniscoping,[status(thm)],[f241])).
% 64.18/8.56 fof(f802,plain,(
% 64.18/8.56 ![X0,X1,X2]: (hBOOL(c_in(X0,X1,X2))|~hBOOL(hAPP(X1,X0)))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f801])).
% 64.18/8.56 fof(f803,plain,(
% 64.18/8.56 ![V_S,V_x]: (hBOOL(hAPP(V_S,V_x))|(![T_a]: ~hBOOL(c_in(V_x,V_S,T_a))))),
% 64.18/8.56 inference(miniscoping,[status(thm)],[f242])).
% 64.18/8.56 fof(f804,plain,(
% 64.18/8.56 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|~hBOOL(c_in(X1,X0,X2)))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f803])).
% 64.18/8.56 fof(f911,plain,(
% 64.18/8.56 ![X0,X1]: (hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1)))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f307])).
% 64.18/8.56 fof(f916,plain,(
% 64.18/8.56 hBOOL(hAPP(v_P,v_x____))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f310])).
% 64.18/8.56 fof(f926,plain,(
% 64.18/8.56 ![X0,X1]: (c_Collect(X0,X1)=X0)),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f318])).
% 64.18/8.56 fof(f927,plain,(
% 64.18/8.56 ![T_a]: (~class_HOL_Oord(T_a)|(![V_R,V_S]: c_Lubs_Oubs(V_R,V_S,T_a)=c_Collect(c_Lubs_OisUb(V_R,V_S,T_a),T_a)))),
% 64.18/8.56 inference(miniscoping,[status(thm)],[f319])).
% 64.18/8.56 fof(f928,plain,(
% 64.18/8.56 ![X0,X1,X2]: (~class_HOL_Oord(X0)|c_Lubs_Oubs(X1,X2,X0)=c_Collect(c_Lubs_OisUb(X1,X2,X0),X0))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f927])).
% 64.18/8.56 fof(f931,plain,(
% 64.18/8.56 ![X0]: (c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool))=c_Collect(c_COMBK(c_True,tc_bool,X0),X0))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f322])).
% 64.18/8.56 fof(f932,plain,(
% 64.18/8.56 ![X0,X1,X2]: (c_Collect(X0,X1)=c_Collect(X2,X1)|hBOOL(hAPP(X2,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X2,X1)))|hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X2,X1))))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f323])).
% 64.18/8.56 fof(f933,plain,(
% 64.18/8.56 ![X0,X1,X2]: (c_Collect(X0,X1)=c_Collect(X2,X1)|~hBOOL(hAPP(X2,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X2,X1)))|~hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X2,X1))))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f324])).
% 64.18/8.56 fof(f950,plain,(
% 64.18/8.56 ![X0]: (~c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f338])).
% 64.18/8.56 fof(f968,plain,(
% 64.18/8.56 hBOOL(hAPP(v_P,v_sko__local__Xassms__1__1(v_P)))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f349])).
% 64.18/8.56 fof(f975,plain,(
% 64.18/8.56 ![X0]: (~hBOOL(hAPP(c_Lubs_OisUb(c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_bool)),c_Collect(v_P,tc_RealDef_Oreal),tc_RealDef_Oreal),X0)))),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f354])).
% 64.18/8.56 fof(f1026,plain,(
% 64.18/8.56 class_HOL_Oord(tc_RealDef_Oreal)),
% 64.18/8.56 inference(cnf_transformation,[status(thm)],[f392])).
% 64.18/8.56 fof(f1041,plain,(
% 64.18/8.56 ![X0,X1,X2]: (~class_HOL_Oord(X0)|c_Lubs_Oubs(X1,X2,X0)=c_Lubs_OisUb(X1,X2,X0))),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f926,f928])).
% 64.18/8.56 fof(f1053,plain,(
% 64.18/8.56 ![X0,X1]: (hBOOL(hAPP(c_COMBK(c_True,tc_bool,X0),X1)))),
% 64.18/8.56 inference(backward_demodulation,[status(thm)],[f1065,f911])).
% 64.18/8.56 fof(f1065,plain,(
% 64.18/8.56 ![X0]: (c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool))=c_COMBK(c_True,tc_bool,X0))),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f926,f931])).
% 64.18/8.56 fof(f1066,plain,(
% 64.18/8.56 ![X0,X1,X2]: (X0=c_Collect(X1,X2)|hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X1,X2)))|hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X1,X2))))),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f926,f932])).
% 64.18/8.56 fof(f1067,plain,(
% 64.18/8.56 ![X0,X1,X2]: (X0=X1|hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X1,X2)))|hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X1,X2))))),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f926,f1066])).
% 64.18/8.56 fof(f1068,plain,(
% 64.18/8.56 ![X0,X1,X2]: (X0=c_Collect(X1,X2)|~hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X1,X2)))|~hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X1,X2))))),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f926,f933])).
% 64.18/8.56 fof(f1069,plain,(
% 64.18/8.56 ![X0,X1,X2]: (X0=X1|~hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X1,X2)))|~hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,X1,X2))))),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f926,f1068])).
% 64.18/8.56 fof(f1078,plain,(
% 64.18/8.56 ![X0]: (~c_COMBK(c_True,tc_bool,X0)=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f1065,f950])).
% 64.18/8.56 fof(f1092,plain,(
% 64.18/8.56 ![X0]: (~hBOOL(hAPP(c_Lubs_OisUb(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),c_Collect(v_P,tc_RealDef_Oreal),tc_RealDef_Oreal),X0)))),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f1065,f975])).
% 64.18/8.56 fof(f1093,plain,(
% 64.18/8.56 ![X0]: (~hBOOL(hAPP(c_Lubs_OisUb(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal),X0)))),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f926,f1092])).
% 64.18/8.56 fof(f1103,plain,(
% 64.18/8.56 hBOOL(c_True)),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f658,f1053])).
% 64.18/8.56 fof(f1111,plain,(
% 64.18/8.56 ![X0,X1]: (c_Lubs_OisUb(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal)=X0|hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(c_Lubs_OisUb(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal),X0,X1))))),
% 64.18/8.56 inference(resolution,[status(thm)],[f1067,f1093])).
% 64.18/8.56 fof(f1188,plain,(
% 64.18/8.56 ![X0,X1]: (c_Lubs_Oubs(X0,X1,tc_RealDef_Oreal)=c_Lubs_OisUb(X0,X1,tc_RealDef_Oreal))),
% 64.18/8.56 inference(resolution,[status(thm)],[f1026,f1041])).
% 64.18/8.56 fof(f1197,plain,(
% 64.18/8.56 ![X0,X1]: (c_Lubs_OisUb(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal)=X0|hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(c_Lubs_Oubs(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal),X0,X1))))),
% 64.18/8.56 inference(backward_demodulation,[status(thm)],[f1188,f1111])).
% 64.18/8.56 fof(f1199,plain,(
% 64.18/8.56 ![X0]: (~hBOOL(hAPP(c_Lubs_Oubs(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal),X0)))),
% 64.18/8.56 inference(backward_demodulation,[status(thm)],[f1188,f1093])).
% 64.18/8.56 fof(f1224,plain,(
% 64.18/8.56 ![X0,X1]: (c_Lubs_Oubs(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal)=X0|hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(c_Lubs_Oubs(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal),X0,X1))))),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f1188,f1197])).
% 64.18/8.56 fof(f1262,plain,(
% 64.18/8.56 ![X0,X1,X2,X3,X4]: (X0=c_COMBK(X1,X2,X3)|~hBOOL(X1)|~hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XCollect__cong__1__1(X0,c_COMBK(X1,X2,X3),X4))))),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f658,f1069])).
% 64.18/8.56 fof(f1289,plain,(
% 64.18/8.56 ![X0,X1,X2]: (c_Lubs_Oubs(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal)=c_COMBK(X0,X1,X2)|hBOOL(X0))),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f658,f1224])).
% 64.18/8.56 fof(f1405,plain,(
% 64.18/8.56 ![X0,X1,X2,X3,X4,X5]: (c_COMBK(X0,X1,X2)=c_COMBK(X3,X4,X5)|~hBOOL(X3)|~hBOOL(X0))),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f658,f1262])).
% 64.18/8.56 fof(f1427,plain,(
% 64.18/8.56 ![X0,X1,X2,X3,X4]: (c_COMBK(X0,X1,X2)=c_COMBK(c_True,X3,X4)|~hBOOL(X0))),
% 64.18/8.56 inference(resolution,[status(thm)],[f1405,f1103])).
% 64.18/8.56 fof(f1446,plain,(
% 64.18/8.56 ![X0,X1,X2,X3]: (c_COMBK(c_True,X0,X1)=c_COMBK(c_True,X2,X3))),
% 64.18/8.56 inference(resolution,[status(thm)],[f1427,f1103])).
% 64.18/8.56 fof(f1447,plain,(
% 64.18/8.56 ![X0,X1,X2,X3,X4,X5,X6]: (c_COMBK(X0,X1,X2)=c_COMBK(c_True,X3,X4)|c_Lubs_Oubs(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal)=c_COMBK(X0,X5,X6))),
% 64.18/8.56 inference(resolution,[status(thm)],[f1427,f1289])).
% 64.18/8.56 fof(f1459,plain,(
% 64.18/8.56 ![X0,X1,X2]: (~hBOOL(hAPP(c_Lubs_Oubs(c_COMBK(c_True,X0,X1),v_P,tc_RealDef_Oreal),X2)))),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f1446,f1199])).
% 64.18/8.56 fof(f1471,plain,(
% 64.18/8.56 ![X0,X1,X2]: (~c_COMBK(c_True,X0,X1)=c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)))),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f1446,f1078])).
% 64.18/8.56 fof(f1596,plain,(
% 64.18/8.56 ![X0,X1,X2,X3,X4,X5]: (hAPP(c_COMBK(c_True,X0,X1),X2)=X3|c_Lubs_Oubs(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal)=c_COMBK(X3,X4,X5))),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f1447,f658])).
% 64.18/8.56 fof(f1611,plain,(
% 64.18/8.56 ![X0,X1,X2]: (c_True=X0|c_Lubs_Oubs(c_COMBK(c_True,tc_bool,tc_RealDef_Oreal),v_P,tc_RealDef_Oreal)=c_COMBK(X0,X1,X2))),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f658,f1596])).
% 64.18/8.56 fof(f1615,plain,(
% 64.18/8.56 ![X0,X1,X2,X3,X4,X5]: (c_True=X0|c_COMBK(X1,X2,X3)=c_COMBK(X0,X4,X5)|c_True=X1)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f1611,f1611])).
% 64.18/8.56 fof(f1624,plain,(
% 64.18/8.56 ![X0,X1,X2,X3]: (~hBOOL(hAPP(c_COMBK(X0,X1,X2),X3))|c_True=X0)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f1611,f1459])).
% 64.18/8.56 fof(f1639,plain,(
% 64.18/8.56 ![X0]: (~hBOOL(X0)|c_True=X0)),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f658,f1624])).
% 64.18/8.56 fof(f1642,plain,(
% 64.18/8.56 c_True=hAPP(v_P,v_x____)),
% 64.18/8.56 inference(resolution,[status(thm)],[f1639,f916])).
% 64.18/8.56 fof(f1756,plain,(
% 64.18/8.56 ![X0,X1,X2,X3,X4]: (hAPP(c_COMBK(X0,X1,X2),X3)=X4|c_True=X0|c_True=X4)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f1615,f658])).
% 64.18/8.56 fof(f1776,plain,(
% 64.18/8.56 ![X0,X1]: (X0=X1|c_True=X0|c_True=X1)),
% 64.18/8.56 inference(forward_demodulation,[status(thm)],[f658,f1756])).
% 64.18/8.56 fof(f1783,plain,(
% 64.18/8.56 ![X0,X1,X2]: (c_True=c_COMBK(c_True,X0,X1)|c_True=c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)))),
% 64.18/8.56 inference(resolution,[status(thm)],[f1776,f1471])).
% 64.18/8.56 fof(f1803,plain,(
% 64.18/8.56 ![X0]: (hBOOL(hAPP(X0,v_sko__local__Xassms__1__1(v_P)))|c_True=v_P|c_True=X0)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f1776,f968])).
% 64.18/8.56 fof(f1935,plain,(
% 64.18/8.56 ![X0,X1,X2]: (hBOOL(X0)|c_True=v_P|c_True=c_COMBK(X0,X1,X2))),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f658,f1803])).
% 64.18/8.56 fof(f1973,plain,(
% 64.18/8.56 ![X0,X1,X2]: (c_True=v_P|c_True=c_COMBK(X0,X1,X2)|c_True=X0)),
% 64.18/8.56 inference(resolution,[status(thm)],[f1935,f1639])).
% 64.18/8.56 fof(f2001,plain,(
% 64.18/8.56 ![X0,X1]: (hAPP(c_True,X0)=X1|c_True=v_P|c_True=X1)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f1973,f658])).
% 64.18/8.56 fof(f2020,plain,(
% 64.18/8.56 ![X0,X1]: (c_True=v_P|~hAPP(c_True,X0)=c_True|X1=c_True)),
% 64.18/8.56 inference(equality_factoring,[status(thm)],[f2001])).
% 64.18/8.56 fof(f2108,plain,(
% 64.18/8.56 ![X0]: (c_True=v_P|c_True=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
% 64.18/8.56 inference(resolution,[status(thm)],[f601,f1803])).
% 64.18/8.56 fof(f2253,plain,(
% 64.18/8.56 ![X0,X1]: (~c_COMBK(c_True,X0,X1)=c_True|c_True=v_P)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f2108,f1471])).
% 64.18/8.56 fof(f2303,plain,(
% 64.18/8.56 ![X0,X1,X2]: (c_True=v_P|X0=c_COMBK(c_True,X1,X2)|c_True=X0)),
% 64.18/8.56 inference(resolution,[status(thm)],[f2253,f1776])).
% 64.18/8.56 fof(f2390,plain,(
% 64.18/8.56 ![X0,X1]: (hAPP(X0,X1)=c_True|c_True=v_P|c_True=X0)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f2303,f658])).
% 64.18/8.56 fof(f2410,plain,(
% 64.18/8.56 ![X0,X1]: (X0=c_True|c_True=v_P|c_True=c_COMBI(X1))),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f657,f2390])).
% 64.18/8.56 fof(f2593,plain,(
% 64.18/8.56 ![X0]: (c_True=v_P|c_True=c_COMBI(X0)|c_True=v_P)),
% 64.18/8.56 inference(resolution,[status(thm)],[f2410,f2253])).
% 64.18/8.56 fof(f2621,plain,(
% 64.18/8.56 ![X0]: (c_True=v_P|c_True=c_COMBI(X0))),
% 64.18/8.56 inference(duplicate_literals_removal,[status(thm)],[f2593])).
% 64.18/8.56 fof(f2643,plain,(
% 64.18/8.56 ![X0]: (hAPP(c_True,X0)=X0|c_True=v_P)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f2621,f657])).
% 64.18/8.56 fof(f2648,plain,(
% 64.18/8.56 ![X0]: (c_True=v_P|c_True=v_P|X0=c_True)),
% 64.18/8.56 inference(resolution,[status(thm)],[f2643,f2020])).
% 64.18/8.56 fof(f2668,plain,(
% 64.18/8.56 c_True=v_P),
% 64.18/8.56 inference(backward_subsumption_resolution,[status(thm)],[f2253,f2670])).
% 64.18/8.56 fof(f2670,plain,(
% 64.18/8.56 ![X0]: (c_True=v_P|X0=c_True)),
% 64.18/8.56 inference(duplicate_literals_removal,[status(thm)],[f2648])).
% 64.18/8.56 fof(f2688,plain,(
% 64.18/8.56 c_True=hAPP(c_True,v_x____)),
% 64.18/8.56 inference(backward_demodulation,[status(thm)],[f2668,f1642])).
% 64.18/8.56 fof(f2918,plain,(
% 64.18/8.56 ![X0]: (c_True=hAPP(c_True,X0)|c_True=v_x____|c_True=X0)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f1776,f2688])).
% 64.18/8.56 fof(f3237,plain,(
% 64.18/8.56 ![X0,X1,X2]: (~hBOOL(hAPP(X0,X1))|c_True=c_in(X1,X0,X2))),
% 64.18/8.56 inference(resolution,[status(thm)],[f802,f1639])).
% 64.18/8.56 fof(f3347,plain,(
% 64.18/8.56 ![X0,X1]: (~hBOOL(c_True)|c_True=c_in(X0,c_True,X1)|c_True=v_x____|c_True=X0)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f2918,f3237])).
% 64.18/8.56 fof(f3350,plain,(
% 64.18/8.56 ![X0,X1,X2]: (~hBOOL(X0)|c_True=c_in(X0,c_COMBI(X1),X2))),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f657,f3237])).
% 64.18/8.56 fof(f3357,plain,(
% 64.18/8.56 ![X0,X1]: (c_True=c_in(X0,c_True,X1)|c_True=v_x____|c_True=X0)),
% 64.18/8.56 inference(forward_subsumption_resolution,[status(thm)],[f3347,f1103])).
% 64.18/8.56 fof(f3443,plain,(
% 64.18/8.56 ![X0,X1]: (c_True=c_in(c_True,c_COMBI(X0),X1))),
% 64.18/8.56 inference(resolution,[status(thm)],[f3350,f1103])).
% 64.18/8.56 fof(f3448,plain,(
% 64.18/8.56 ![X0,X1,X2]: (c_True=c_in(c_True,X0,X1)|c_True=c_COMBI(X2)|c_True=X0)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f1776,f3443])).
% 64.18/8.56 fof(f3478,plain,(
% 64.18/8.56 ![X0]: (hBOOL(hAPP(c_True,X0))|~hBOOL(c_True)|c_True=v_x____|c_True=X0)),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f3357,f804])).
% 64.18/8.56 fof(f3485,plain,(
% 64.18/8.56 ![X0]: (hBOOL(hAPP(c_True,X0))|c_True=v_x____|c_True=X0)),
% 64.18/8.56 inference(forward_subsumption_resolution,[status(thm)],[f3478,f1103])).
% 64.18/8.56 fof(f5333,plain,(
% 64.18/8.56 ![X0,X1]: (~hBOOL(c_True)|c_True=c_COMBI(X0)|c_True=c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),
% 64.18/8.56 inference(paramodulation,[status(thm)],[f3448,f582])).
% 64.18/8.56 fof(f5338,plain,(
% 64.18/8.56 ![X0,X1]: (hBOOL(hAPP(X0,c_True))|~hBOOL(c_True)|c_True=c_COMBI(X1)|c_True=X0)),
% 38.61/8.63 inference(paramodulation,[status(thm)],[f3448,f804])).
% 38.61/8.63 fof(f5344,plain,(
% 38.61/8.63 ![X0,X1]: (c_True=c_COMBI(X0)|c_True=c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),
% 38.61/8.63 inference(forward_subsumption_resolution,[status(thm)],[f5333,f1103])).
% 38.61/8.63 fof(f5347,plain,(
% 38.61/8.63 ![X0,X1]: (hBOOL(hAPP(X0,c_True))|c_True=c_COMBI(X1)|c_True=X0)),
% 38.61/8.63 inference(forward_subsumption_resolution,[status(thm)],[f5338,f1103])).
% 38.61/8.63 fof(f5363,plain,(
% 38.61/8.63 ![X0,X1]: (hAPP(c_True,X0)=X0|c_True=c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),
% 38.61/8.63 inference(paramodulation,[status(thm)],[f5344,f657])).
% 38.61/8.63 fof(f5401,plain,(
% 38.61/8.63 ![X0,X1,X2,X3]: (hBOOL(X0)|c_True=c_COMBI(X1)|c_True=c_COMBK(X0,X2,X3))),
% 38.61/8.63 inference(paramodulation,[status(thm)],[f658,f5347])).
% 38.61/8.63 fof(f5420,plain,(
% 38.61/8.63 ![X0]: (c_True=v_x____|c_True=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
% 38.61/8.63 inference(paramodulation,[status(thm)],[f2688,f5363])).
% 38.61/8.63 fof(f5514,plain,(
% 38.61/8.63 ![X0]: (~hBOOL(hAPP(c_True,X0))|c_True=v_x____)),
% 38.61/8.63 inference(paramodulation,[status(thm)],[f5420,f601])).
% 38.61/8.63 fof(f5516,plain,(
% 38.61/8.63 ![X0,X1]: (~c_COMBK(c_True,X0,X1)=c_True|c_True=v_x____)),
% 38.61/8.63 inference(paramodulation,[status(thm)],[f5420,f1471])).
% 38.61/8.63 fof(f5520,plain,(
% 38.61/8.63 ![X0]: (c_True=v_x____|c_True=X0)),
% 38.61/8.63 inference(backward_subsumption_resolution,[status(thm)],[f3485,f5514])).
% 38.61/8.63 fof(f5522,plain,(
% 38.61/8.63 c_True=v_x____),
% 38.61/8.63 inference(backward_subsumption_resolution,[status(thm)],[f5516,f5520])).
% 38.61/8.63 fof(f5525,plain,(
% 38.61/8.63 c_True=hAPP(c_True,c_True)),
% 38.61/8.63 inference(backward_demodulation,[status(thm)],[f5522,f2688])).
% 38.61/8.63 fof(f5664,plain,(
% 38.61/8.63 ![X0,X1,X2,X3]: (c_True=c_COMBI(X0)|c_True=c_COMBK(X1,X2,X3)|c_True=X1)),
% 38.61/8.63 inference(resolution,[status(thm)],[f5401,f1639])).
% 38.61/8.63 fof(f6144,plain,(
% 38.61/8.63 ![X0,X1,X2]: (c_True=c_COMBK(c_COMBI(X0),X1,X2)|~c_True=c_True|c_COMBI(X0)=c_True)),
% 38.61/8.63 inference(equality_factoring,[status(thm)],[f5664])).
% 38.61/8.63 fof(f6147,plain,(
% 38.61/8.63 ![X0,X1,X2]: (c_True=c_COMBK(c_COMBI(X0),X1,X2)|c_COMBI(X0)=c_True)),
% 38.61/8.63 inference(trivial_equality_resolution,[status(thm)],[f6144])).
% 38.61/8.63 fof(f6185,plain,(
% 38.61/8.63 ![X0,X1]: (hAPP(c_True,X0)=c_COMBI(X1)|c_COMBI(X1)=c_True)),
% 38.61/8.63 inference(paramodulation,[status(thm)],[f6147,f658])).
% 38.61/8.63 fof(f6202,plain,(
% 38.61/8.63 ![X0]: (c_True=c_COMBI(X0)|c_COMBI(X0)=c_True)),
% 38.61/8.63 inference(paramodulation,[status(thm)],[f5525,f6185])).
% 38.61/8.63 fof(f6258,plain,(
% 38.61/8.63 ![X0]: (hAPP(c_True,X0)=X0)),
% 38.61/8.63 inference(backward_demodulation,[status(thm)],[f6345,f657])).
% 38.61/8.63 fof(f6345,plain,(
% 38.61/8.63 ![X0]: (c_True=c_COMBI(X0))),
% 38.61/8.63 inference(duplicate_literals_removal,[status(thm)],[f6202])).
% 38.61/8.63 fof(f7786,plain,(
% 38.61/8.63 ![X0,X1]: (~c_True=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))|c_True=c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),
% 38.61/8.63 inference(paramodulation,[status(thm)],[f1783,f1471])).
% 38.61/8.63 fof(f7794,plain,(
% 38.61/8.63 ![X0,X1]: (hAPP(c_True,X0)=c_True|c_True=c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),
% 38.61/8.63 inference(paramodulation,[status(thm)],[f1783,f658])).
% 38.61/8.63 fof(f7807,plain,(
% 38.61/8.63 ![X0]: (c_True=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
% 38.61/8.63 inference(backward_subsumption_resolution,[status(thm)],[f7786,f7808])).
% 38.61/8.63 fof(f7808,plain,(
% 38.61/8.63 ![X0,X1]: (X0=c_True|c_True=c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),
% 38.61/8.63 inference(forward_demodulation,[status(thm)],[f6258,f7794])).
% 38.61/8.63 fof(f7817,plain,(
% 38.61/8.63 ![X0]: (~hBOOL(hAPP(c_True,X0)))),
% 38.61/8.63 inference(backward_demodulation,[status(thm)],[f7807,f601])).
% 38.61/8.63 fof(f7896,plain,(
% 38.61/8.63 ![X0]: (~hBOOL(X0))),
% 38.61/8.63 inference(forward_demodulation,[status(thm)],[f6258,f7817])).
% 38.61/8.63 fof(f7897,plain,(
% 38.61/8.63 $false),
% 38.61/8.63 inference(backward_subsumption_resolution,[status(thm)],[f1103,f7896])).
% 38.61/8.63 % SZS output end CNFRefutation for theBenchmark.p
% 38.61/8.69 % Elapsed time: 8.293132 seconds
% 38.61/8.69 % CPU time: 65.042111 seconds
% 38.61/8.69 % Total memory used: 666.953 MB
% 38.61/8.69 % Net memory used: 617.277 MB
%------------------------------------------------------------------------------