%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT028-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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:07:13 PM UTC 2026
% Result : Unsatisfiable 99.77s 13.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SCT028-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n005.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 04:26:47 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.49 % Drodi V4.1.1
% 99.77/13.15 % Refutation found
% 99.77/13.15 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 99.77/13.15 % SZS output start CNFRefutation for theBenchmark
% 99.77/13.15 fof(f3,axiom,(
% 99.77/13.15 (![V_a,T_a]: (~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a) ))),
% 99.77/13.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.15 fof(f30,axiom,(
% 99.77/13.15 (![V_a,V_A,T_a]: (c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ))),
% 99.77/13.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.15 fof(f88,axiom,(
% 99.77/13.15 (![V_a,V_A,T_a]: (( c_Set_Oinsert(V_a,V_A,T_a) = V_A| ~ c_in(V_a,V_A,T_a) ) ))),
% 99.77/13.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.15 fof(f187,axiom,(
% 99.77/13.15 (![V_x,V_A,T_a]: (hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)) ))),
% 99.77/13.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.15 fof(f271,axiom,(
% 99.77/13.15 (![T_a,V_x]: (( ~ class_Orderings_Opreorder(T_a)| c_lessequals(V_x,V_x,T_a) ) ))),
% 99.77/13.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.15 fof(f358,axiom,(
% 99.77/13.15 (![V_b,V_a,T_b,T_a,V_r]: (( c_in(c_Pair(V_b,V_a,T_b,T_a),V_r,tc_prod(T_b,T_a))| ~ c_in(c_Pair(V_a,V_b,T_a,T_b),c_Relation_Oconverse(V_r,T_b,T_a),tc_prod(T_a,T_b)) ) ))),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f448,axiom,(
% 99.77/13.16 c_in(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f450,axiom,(
% 99.77/13.16 (![V_L]: (( c_in(c_Relation_Oconverse(V_L,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))| ~ c_in(V_L,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ) ))),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f505,axiom,(
% 99.77/13.16 v_a != v_b ),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f507,axiom,(
% 99.77/13.16 (![V_y,V_x,V_L]: (( c_in(c_Pair(V_y,V_x,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))| c_in(c_Pair(V_x,V_y,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))| V_x = V_y| ~ c_in(V_L,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ) ))),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f508,axiom,(
% 99.77/13.16 (![V_x,V_S,T_a]: (( c_in(V_x,V_S,T_a)| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f509,axiom,(
% 99.77/13.16 (![V_S,V_x,T_a]: (( hBOOL(hAPP(V_S,V_x))| ~ c_in(V_x,V_S,T_a) ) ))),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f510,axiom,(
% 99.77/13.16 (![V_b,V_a,V_L]: (( ~ c_in(c_Pair(V_b,V_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))| ~ c_in(c_Pair(V_a,V_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))| ~ c_in(V_L,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ) ))),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f511,axiom,(
% 99.77/13.16 c_in(v_R____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f512,negated_conjecture,(
% 99.77/13.16 (![V_x]: (( ~ c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_x,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))| ~ c_in(V_x,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ) ))),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f514,axiom,(
% 99.77/13.16 (![T_2,T_1]: (( class_Complete__Lattice_Ocomplete__lattice(tc_fun(T_2,T_1))| ~ class_Complete__Lattice_Ocomplete__lattice(T_1) ) ))),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f515,axiom,(
% 99.77/13.16 (![T_2,T_1]: (( class_Lattices_Olower__semilattice(tc_fun(T_2,T_1))| ~ class_Lattices_Olattice(T_1) ) ))),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f520,axiom,(
% 99.77/13.16 (![T_2,T_1]: (( class_Orderings_Oorder(tc_fun(T_2,T_1))| ~ class_Orderings_Oorder(T_1) ) ))),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f523,axiom,(
% 99.77/13.16 class_Complete__Lattice_Ocomplete__lattice(tc_bool) ),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f527,axiom,(
% 99.77/13.16 class_Orderings_Opreorder(tc_bool) ),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f528,axiom,(
% 99.77/13.16 class_Lattices_Olattice(tc_bool) ),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f529,axiom,(
% 99.77/13.16 class_Orderings_Oorder(tc_bool) ),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f531,axiom,(
% 99.77/13.16 class_HOL_Oord(tc_bool) ),
% 99.77/13.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.77/13.16 fof(f538,plain,(
% 99.77/13.16 ![X0,X1]: (~c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f3])).
% 99.77/13.16 fof(f573,plain,(
% 99.77/13.16 ![X0,X1,X2]: (~c_Set_Oinsert(X0,X1,X2)=c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f30])).
% 99.77/13.16 fof(f660,plain,(
% 99.77/13.16 ![X0,X1,X2]: (c_Set_Oinsert(X0,X1,X2)=X1|~c_in(X0,X1,X2))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f88])).
% 99.77/13.16 fof(f820,plain,(
% 99.77/13.16 ![X0,X1,X2]: (hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f187])).
% 99.77/13.16 fof(f945,plain,(
% 99.77/13.16 ![T_a]: (~class_Orderings_Opreorder(T_a)|(![V_x]: c_lessequals(V_x,V_x,T_a)))),
% 99.77/13.16 inference(miniscoping,[status(thm)],[f271])).
% 99.77/13.16 fof(f946,plain,(
% 99.77/13.16 ![X0,X1]: (~class_Orderings_Opreorder(X0)|c_lessequals(X1,X1,X0))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f945])).
% 99.77/13.16 fof(f1068,plain,(
% 99.77/13.16 ![X0,X1,X2,X3,X4]: (c_in(c_Pair(X0,X1,X2,X3),X4,tc_prod(X2,X3))|~c_in(c_Pair(X1,X0,X3,X2),c_Relation_Oconverse(X4,X2,X3),tc_prod(X3,X2)))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f358])).
% 99.77/13.16 fof(f1194,plain,(
% 99.77/13.16 c_in(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f448])).
% 99.77/13.16 fof(f1196,plain,(
% 99.77/13.16 ![X0]: (c_in(c_Relation_Oconverse(X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))|~c_in(X0,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f450])).
% 99.77/13.16 fof(f1294,plain,(
% 99.77/13.16 ~v_a=v_b),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f505])).
% 99.77/13.16 fof(f1297,plain,(
% 99.77/13.16 ![V_L]: ((![V_y,V_x]: ((c_in(c_Pair(V_y,V_x,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(V_x,V_y,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|V_x=V_y))|~c_in(V_L,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 inference(miniscoping,[status(thm)],[f507])).
% 99.77/13.16 fof(f1298,plain,(
% 99.77/13.16 ![X0,X1,X2]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|X1=X0|~c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f1297])).
% 99.77/13.16 fof(f1299,plain,(
% 99.77/13.16 ![V_x,V_S]: ((![T_a]: c_in(V_x,V_S,T_a))|~hBOOL(hAPP(V_S,V_x)))),
% 99.77/13.16 inference(miniscoping,[status(thm)],[f508])).
% 99.77/13.16 fof(f1300,plain,(
% 99.77/13.16 ![X0,X1,X2]: (c_in(X0,X1,X2)|~hBOOL(hAPP(X1,X0)))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f1299])).
% 99.77/13.16 fof(f1301,plain,(
% 99.77/13.16 ![V_S,V_x]: (hBOOL(hAPP(V_S,V_x))|(![T_a]: ~c_in(V_x,V_S,T_a)))),
% 99.77/13.16 inference(miniscoping,[status(thm)],[f509])).
% 99.77/13.16 fof(f1302,plain,(
% 99.77/13.16 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|~c_in(X1,X0,X2))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f1301])).
% 99.77/13.16 fof(f1303,plain,(
% 99.77/13.16 ![V_L]: ((![V_b,V_a]: (~c_in(c_Pair(V_b,V_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(V_a,V_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))))|~c_in(V_L,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 inference(miniscoping,[status(thm)],[f510])).
% 99.77/13.16 fof(f1304,plain,(
% 99.77/13.16 ![X0,X1,X2]: (~c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f1303])).
% 99.77/13.16 fof(f1305,plain,(
% 99.77/13.16 c_in(v_R____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f511])).
% 99.77/13.16 fof(f1306,plain,(
% 99.77/13.16 ![X0]: (~c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(X0,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f512])).
% 99.77/13.16 fof(f1309,plain,(
% 99.77/13.16 ![T_1]: ((![T_2]: class_Complete__Lattice_Ocomplete__lattice(tc_fun(T_2,T_1)))|~class_Complete__Lattice_Ocomplete__lattice(T_1))),
% 99.77/13.16 inference(miniscoping,[status(thm)],[f514])).
% 99.77/13.16 fof(f1310,plain,(
% 99.77/13.16 ![X0,X1]: (class_Complete__Lattice_Ocomplete__lattice(tc_fun(X0,X1))|~class_Complete__Lattice_Ocomplete__lattice(X1))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f1309])).
% 99.77/13.16 fof(f1311,plain,(
% 99.77/13.16 ![T_1]: ((![T_2]: class_Lattices_Olower__semilattice(tc_fun(T_2,T_1)))|~class_Lattices_Olattice(T_1))),
% 99.77/13.16 inference(miniscoping,[status(thm)],[f515])).
% 99.77/13.16 fof(f1312,plain,(
% 99.77/13.16 ![X0,X1]: (class_Lattices_Olower__semilattice(tc_fun(X0,X1))|~class_Lattices_Olattice(X1))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f1311])).
% 99.77/13.16 fof(f1321,plain,(
% 99.77/13.16 ![T_1]: ((![T_2]: class_Orderings_Oorder(tc_fun(T_2,T_1)))|~class_Orderings_Oorder(T_1))),
% 99.77/13.16 inference(miniscoping,[status(thm)],[f520])).
% 99.77/13.16 fof(f1322,plain,(
% 99.77/13.16 ![X0,X1]: (class_Orderings_Oorder(tc_fun(X0,X1))|~class_Orderings_Oorder(X1))),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f1321])).
% 99.77/13.16 fof(f1327,plain,(
% 99.77/13.16 class_Complete__Lattice_Ocomplete__lattice(tc_bool)),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f523])).
% 99.77/13.16 fof(f1331,plain,(
% 99.77/13.16 class_Orderings_Opreorder(tc_bool)),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f527])).
% 99.77/13.16 fof(f1332,plain,(
% 99.77/13.16 class_Lattices_Olattice(tc_bool)),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f528])).
% 99.77/13.16 fof(f1333,plain,(
% 99.77/13.16 class_Orderings_Oorder(tc_bool)),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f529])).
% 99.77/13.16 fof(f1335,plain,(
% 99.77/13.16 class_HOL_Oord(tc_bool)),
% 99.77/13.16 inference(cnf_transformation,[status(thm)],[f531])).
% 99.77/13.16 fof(f1356,plain,(
% 99.77/13.16 ![X0]: (c_lessequals(X0,X0,tc_bool))),
% 99.77/13.16 inference(resolution,[status(thm)],[f946,f1331])).
% 99.77/13.16 fof(f1368,plain,(
% 99.77/13.16 ![X0]: (class_Complete__Lattice_Ocomplete__lattice(tc_fun(X0,tc_bool)))),
% 99.77/13.16 inference(resolution,[status(thm)],[f1310,f1327])).
% 99.77/13.16 fof(f1370,plain,(
% 99.77/13.16 ![X0]: (class_Lattices_Olower__semilattice(tc_fun(X0,tc_bool)))),
% 99.77/13.16 inference(resolution,[status(thm)],[f1312,f1332])).
% 99.77/13.16 fof(f1382,plain,(
% 99.77/13.16 ![X0]: (class_Orderings_Oorder(tc_fun(X0,tc_bool)))),
% 99.77/13.16 inference(resolution,[status(thm)],[f1322,f1333])).
% 99.77/13.16 fof(f1460,plain,(
% 99.77/13.16 ![X0,X1,X2,X3]: (c_in(X0,c_Set_Oinsert(X0,X1,X2),X3))),
% 99.77/13.16 inference(resolution,[status(thm)],[f1300,f820])).
% 99.77/13.16 fof(f1465,plain,(
% 99.77/13.16 ![X0,X1,X2,X3]: (c_Set_Oinsert(X0,c_Set_Oinsert(X0,X1,X2),X3)=c_Set_Oinsert(X0,X1,X2))),
% 99.77/13.16 inference(resolution,[status(thm)],[f1460,f660])).
% 99.77/13.16 fof(f1897,definition,(
% 99.77/13.16 sQ11_spl <=> (c_Orderings_Obot__class_Obot(tc_bool)=c_Orderings_Obot__class_Obot(tc_bool))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f1899,plain,(
% 99.77/13.16 ~c_Orderings_Obot__class_Obot(tc_bool)=c_Orderings_Obot__class_Obot(tc_bool)|sQ11_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f1897])).
% 99.77/13.16 fof(f2242,plain,(
% 99.77/13.16 ![X0,X1,X2,X3]: (~c_Set_Oinsert(X0,X1,X2)=c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)))),
% 99.77/13.16 inference(paramodulation,[status(thm)],[f1465,f573])).
% 99.77/13.16 fof(f2993,plain,(
% 99.77/13.16 ![X0,X1]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|X1=X0)),
% 99.77/13.16 inference(resolution,[status(thm)],[f1194,f1298])).
% 99.77/13.16 fof(f2994,plain,(
% 99.77/13.16 c_in(c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
% 99.77/13.16 inference(resolution,[status(thm)],[f1194,f1196])).
% 99.77/13.16 fof(f2999,plain,(
% 99.77/13.16 hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1))),
% 99.77/13.16 inference(resolution,[status(thm)],[f1194,f1302])).
% 99.77/13.16 fof(f3015,plain,(
% 99.77/13.16 ![X0]: (c_in(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,c_Arrow__Order__Mirabelle_OLin,X0))),
% 99.77/13.16 inference(resolution,[status(thm)],[f2999,f1300])).
% 99.77/13.16 fof(f3024,plain,(
% 99.77/13.16 ![X0]: (c_Set_Oinsert(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,c_Arrow__Order__Mirabelle_OLin,X0)=c_Arrow__Order__Mirabelle_OLin)),
% 99.77/13.16 inference(resolution,[status(thm)],[f3015,f660])).
% 99.77/13.16 fof(f3033,plain,(
% 99.77/13.16 ![X0]: (~c_Arrow__Order__Mirabelle_OLin=c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
% 99.77/13.16 inference(paramodulation,[status(thm)],[f3024,f2242])).
% 99.77/13.16 fof(f3122,plain,(
% 99.77/13.16 ![X0,X1]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|X1=X0)),
% 99.77/13.16 inference(resolution,[status(thm)],[f2994,f1298])).
% 99.77/13.16 fof(f3128,plain,(
% 99.77/13.16 hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 99.77/13.16 inference(resolution,[status(thm)],[f2994,f1302])).
% 99.77/13.16 fof(f3140,plain,(
% 99.77/13.16 ![X0]: (c_in(c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_OLin,X0))),
% 99.77/13.16 inference(resolution,[status(thm)],[f3128,f1300])).
% 99.77/13.16 fof(f3259,definition,(
% 99.77/13.16 sQ67_spl <=> (c_in(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f3261,plain,(
% 99.77/13.16 ~c_in(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))|sQ67_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f3259])).
% 99.77/13.16 fof(f3323,plain,(
% 99.77/13.16 c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b=v_a|~c_in(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
% 99.77/13.16 inference(resolution,[status(thm)],[f2993,f1306])).
% 99.77/13.16 fof(f3352,definition,(
% 99.77/13.16 sQ76_spl <=> (c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f3353,plain,(
% 99.77/13.16 c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~sQ76_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f3352])).
% 99.77/13.16 fof(f3355,definition,(
% 99.77/13.16 sQ77_spl <=> (v_b=v_a)),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f3356,plain,(
% 99.77/13.16 v_b=v_a|~sQ77_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f3355])).
% 99.77/13.16 fof(f3358,plain,(
% 99.77/13.16 sQ76_spl|sQ77_spl|~sQ67_spl),
% 99.77/13.16 inference(split_clause,[status(thm)],[f3323,f3352,f3355,f3259])).
% 99.77/13.16 fof(f3414,plain,(
% 99.77/13.16 $false|sQ67_spl),
% 99.77/13.16 inference(forward_subsumption_resolution,[status(thm)],[f3261,f3015])).
% 99.77/13.16 fof(f3415,plain,(
% 99.77/13.16 sQ67_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f3414])).
% 99.77/13.16 fof(f3416,plain,(
% 99.77/13.16 c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b=v_a|~c_in(c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
% 99.77/13.16 inference(resolution,[status(thm)],[f3122,f1306])).
% 99.77/13.16 fof(f3445,definition,(
% 99.77/13.16 sQ91_spl <=> (c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f3446,plain,(
% 99.77/13.16 c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~sQ91_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f3445])).
% 99.77/13.16 fof(f3448,definition,(
% 99.77/13.16 sQ92_spl <=> (c_in(c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f3450,plain,(
% 99.77/13.16 ~c_in(c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))|sQ92_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f3448])).
% 99.77/13.16 fof(f3451,plain,(
% 99.77/13.16 sQ91_spl|sQ77_spl|~sQ92_spl),
% 99.77/13.16 inference(split_clause,[status(thm)],[f3416,f3445,f3355,f3448])).
% 99.77/13.16 fof(f3501,plain,(
% 99.77/13.16 $false|sQ92_spl),
% 99.77/13.16 inference(forward_subsumption_resolution,[status(thm)],[f3450,f3140])).
% 99.77/13.16 fof(f3502,plain,(
% 99.77/13.16 sQ92_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f3501])).
% 99.77/13.16 fof(f3503,plain,(
% 99.77/13.16 $false|~sQ77_spl),
% 99.77/13.16 inference(forward_subsumption_resolution,[status(thm)],[f3356,f1294])).
% 99.77/13.16 fof(f3504,plain,(
% 99.77/13.16 ~sQ77_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f3503])).
% 99.77/13.16 fof(f3545,definition,(
% 99.77/13.16 sQ105_spl <=> (v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1=v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1)),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f3547,plain,(
% 99.77/13.16 ~v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1=v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1|sQ105_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f3545])).
% 99.77/13.16 fof(f3618,plain,(
% 99.77/13.16 ~c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))|~sQ76_spl),
% 99.77/13.16 inference(resolution,[status(thm)],[f3353,f1304])).
% 99.77/13.16 fof(f3628,definition,(
% 99.77/13.16 sQ107_spl <=> (c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f3630,plain,(
% 99.77/13.16 ~c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|sQ107_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f3628])).
% 99.77/13.16 fof(f3631,plain,(
% 99.77/13.16 ~sQ107_spl|~sQ67_spl|~sQ76_spl),
% 99.77/13.16 inference(split_clause,[status(thm)],[f3618,f3628,f3259,f3352])).
% 99.77/13.16 fof(f3711,plain,(
% 99.77/13.16 hBOOL(hAPP(c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~sQ91_spl),
% 99.77/13.16 inference(resolution,[status(thm)],[f3446,f1302])).
% 99.77/13.16 fof(f3838,definition,(
% 99.77/13.16 sQ127_spl <=> (c_Arrow__Order__Mirabelle_OLin=c_Orderings_Obot__class_Obot(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_bool)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f3839,plain,(
% 99.77/13.16 c_Arrow__Order__Mirabelle_OLin=c_Orderings_Obot__class_Obot(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_bool))|~sQ127_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f3838])).
% 99.77/13.16 fof(f3844,plain,(
% 99.77/13.16 $false|~sQ127_spl),
% 99.77/13.16 inference(forward_subsumption_resolution,[status(thm)],[f3839,f3033])).
% 99.77/13.16 fof(f3845,plain,(
% 99.77/13.16 ~sQ127_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f3844])).
% 99.77/13.16 fof(f3954,plain,(
% 99.77/13.16 $false|sQ105_spl),
% 99.77/13.16 inference(trivial_equality_resolution,[status(thm)],[f3547])).
% 99.77/13.16 fof(f3955,plain,(
% 99.77/13.16 sQ105_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f3954])).
% 99.77/13.16 fof(f4173,definition,(
% 99.77/13.16 sQ139_spl <=> (class_Orderings_Oorder(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f4175,plain,(
% 99.77/13.16 ~class_Orderings_Oorder(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))|sQ139_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f4173])).
% 99.77/13.16 fof(f4183,definition,(
% 99.77/13.16 sQ142_spl <=> (class_Lattices_Olower__semilattice(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f4185,plain,(
% 99.77/13.16 ~class_Lattices_Olower__semilattice(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))|sQ142_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f4183])).
% 99.77/13.16 fof(f4194,plain,(
% 99.77/13.16 $false|sQ142_spl),
% 99.77/13.16 inference(forward_subsumption_resolution,[status(thm)],[f4185,f1370])).
% 99.77/13.16 fof(f4195,plain,(
% 99.77/13.16 sQ142_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f4194])).
% 99.77/13.16 fof(f4236,plain,(
% 99.77/13.16 c_in(c_Relation_Oconverse(v_R____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
% 99.77/13.16 inference(resolution,[status(thm)],[f1305,f1196])).
% 99.77/13.16 fof(f4242,plain,(
% 99.77/13.16 hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,v_R____))),
% 99.77/13.16 inference(resolution,[status(thm)],[f1305,f1302])).
% 99.77/13.16 fof(f4253,plain,(
% 99.77/13.16 ![X0]: (c_in(v_R____,c_Arrow__Order__Mirabelle_OLin,X0))),
% 99.77/13.16 inference(resolution,[status(thm)],[f4242,f1300])).
% 99.77/13.16 fof(f4426,definition,(
% 99.77/13.16 ![X1]: (sQ154_spl <=> (c_Complete__Lattice_OSup__class_OSup(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_bool)=X1))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f4427,plain,(
% 99.77/13.16 ![X0]: (c_Complete__Lattice_OSup__class_OSup(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_bool)=X0|~sQ154_spl)),
% 99.77/13.16 inference(component_clause,[status(thm)],[f4426])).
% 99.77/13.16 fof(f4539,definition,(
% 99.77/13.16 sQ160_spl <=> (c_in(v_R____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f4541,plain,(
% 99.77/13.16 ~c_in(v_R____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))|sQ160_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f4539])).
% 99.77/13.16 fof(f4592,plain,(
% 99.77/13.16 $false|sQ160_spl),
% 99.77/13.16 inference(forward_subsumption_resolution,[status(thm)],[f4541,f4253])).
% 99.77/13.16 fof(f4593,plain,(
% 99.77/13.16 sQ160_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f4592])).
% 99.77/13.16 fof(f4603,plain,(
% 99.77/13.16 hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,c_Relation_Oconverse(v_R____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 99.77/13.16 inference(resolution,[status(thm)],[f4236,f1302])).
% 99.77/13.16 fof(f5010,plain,(
% 99.77/13.16 ![X0]: (c_in(c_Relation_Oconverse(v_R____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_OLin,X0))),
% 99.77/13.16 inference(resolution,[status(thm)],[f4603,f1300])).
% 99.77/13.16 fof(f5732,definition,(
% 99.77/13.16 sQ218_spl <=> (v_R____=v_R____)),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f5734,plain,(
% 99.77/13.16 ~v_R____=v_R____|sQ218_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f5732])).
% 99.77/13.16 fof(f5739,plain,(
% 99.77/13.16 $false|sQ218_spl),
% 99.77/13.16 inference(trivial_equality_resolution,[status(thm)],[f5734])).
% 99.77/13.16 fof(f5740,plain,(
% 99.77/13.16 sQ218_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f5739])).
% 99.77/13.16 fof(f6454,plain,(
% 99.77/13.16 $false|sQ139_spl),
% 99.77/13.16 inference(forward_subsumption_resolution,[status(thm)],[f4175,f1382])).
% 99.77/13.16 fof(f6455,plain,(
% 99.77/13.16 sQ139_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f6454])).
% 99.77/13.16 fof(f8706,plain,(
% 99.77/13.16 ![X0,X1]: (X0=X1|~sQ154_spl)),
% 99.77/13.16 inference(paramodulation,[status(thm)],[f4427,f4427])).
% 99.77/13.16 fof(f8725,plain,(
% 99.77/13.16 $false|~sQ154_spl),
% 99.77/13.16 inference(backward_subsumption_resolution,[status(thm)],[f2242,f8706])).
% 99.77/13.16 fof(f8738,plain,(
% 99.77/13.16 ~sQ154_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f8725])).
% 99.77/13.16 fof(f8969,definition,(
% 99.77/13.16 ![X1,X2]: (sQ369_spl <=> (c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Orderings_Obot__class_Obot(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|X1=X2))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f8970,plain,(
% 99.77/13.16 ![X0,X1]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Orderings_Obot__class_Obot(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|X0=X1|~sQ369_spl)),
% 99.77/13.16 inference(component_clause,[status(thm)],[f8969])).
% 99.77/13.16 fof(f10474,definition,(
% 99.77/13.16 sQ414_spl <=> (class_Lattices_Olower__semilattice(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_bool)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f10476,plain,(
% 99.77/13.16 ~class_Lattices_Olower__semilattice(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_bool))|sQ414_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f10474])).
% 99.77/13.16 fof(f10482,plain,(
% 99.77/13.16 $false|sQ414_spl),
% 99.77/13.16 inference(forward_subsumption_resolution,[status(thm)],[f10476,f1370])).
% 99.77/13.16 fof(f10483,plain,(
% 99.77/13.16 sQ414_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f10482])).
% 99.77/13.16 fof(f12115,plain,(
% 99.77/13.16 ![X0,X1]: (X0=X1|~sQ369_spl)),
% 99.77/13.16 inference(forward_subsumption_resolution,[status(thm)],[f8970,f538])).
% 99.77/13.16 fof(f12138,plain,(
% 99.77/13.16 $false|~sQ369_spl),
% 99.77/13.16 inference(backward_subsumption_resolution,[status(thm)],[f2242,f12115])).
% 99.77/13.16 fof(f12157,plain,(
% 99.77/13.16 ~sQ369_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f12138])).
% 99.77/13.16 fof(f15620,plain,(
% 99.77/13.16 ![X0]: (c_in(c_Pair(v_b,v_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Relation_Oconverse(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0)|~sQ91_spl)),
% 99.77/13.16 inference(resolution,[status(thm)],[f3711,f1300])).
% 99.77/13.16 fof(f15969,definition,(
% 99.77/13.16 ![X1]: (sQ620_spl <=> (v_a=X1))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f15970,plain,(
% 99.77/13.16 ![X0]: (v_a=X0|~sQ620_spl)),
% 99.77/13.16 inference(component_clause,[status(thm)],[f15969])).
% 99.77/13.16 fof(f16571,plain,(
% 99.77/13.16 $false|~sQ620_spl),
% 99.77/13.16 inference(backward_subsumption_resolution,[status(thm)],[f1294,f15970])).
% 99.77/13.16 fof(f16621,plain,(
% 99.77/13.16 ~sQ620_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f16571])).
% 99.77/13.16 fof(f17050,definition,(
% 99.77/13.16 sQ683_spl <=> (c_Complete__Lattice_OInf__class_OInf(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_bool)=c_Complete__Lattice_OInf__class_OInf(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_bool))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ683_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f17052,plain,(
% 99.77/13.16 ~c_Complete__Lattice_OInf__class_OInf(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_bool)=c_Complete__Lattice_OInf__class_OInf(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_bool)|sQ683_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f17050])).
% 99.77/13.16 fof(f18585,definition,(
% 99.77/13.16 sQ754_spl <=> (c_in(c_Relation_Oconverse(v_R____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ754_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f18587,plain,(
% 99.77/13.16 ~c_in(c_Relation_Oconverse(v_R____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))|sQ754_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f18585])).
% 99.77/13.16 fof(f18678,plain,(
% 99.77/13.16 $false|sQ754_spl),
% 99.77/13.16 inference(forward_subsumption_resolution,[status(thm)],[f18587,f5010])).
% 99.77/13.16 fof(f18679,plain,(
% 99.77/13.16 sQ754_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f18678])).
% 99.77/13.16 fof(f19534,definition,(
% 99.77/13.16 ![X1]: (sQ838_spl <=> (v_b=X1))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ838_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f19535,plain,(
% 99.77/13.16 ![X0]: (v_b=X0|~sQ838_spl)),
% 99.77/13.16 inference(component_clause,[status(thm)],[f19534])).
% 99.77/13.16 fof(f19680,definition,(
% 99.77/13.16 sQ853_spl <=> (class_Complete__Lattice_Ocomplete__lattice(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_bool)))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ853_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f19682,plain,(
% 99.77/13.16 ~class_Complete__Lattice_Ocomplete__lattice(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_bool))|sQ853_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f19680])).
% 99.77/13.16 fof(f19691,plain,(
% 99.77/13.16 $false|sQ853_spl),
% 99.77/13.16 inference(forward_subsumption_resolution,[status(thm)],[f19682,f1368])).
% 99.77/13.16 fof(f19692,plain,(
% 99.77/13.16 sQ853_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f19691])).
% 99.77/13.16 fof(f19883,plain,(
% 99.77/13.16 $false|~sQ838_spl),
% 99.77/13.16 inference(backward_subsumption_resolution,[status(thm)],[f1294,f19535])).
% 99.77/13.16 fof(f19936,plain,(
% 99.77/13.16 ~sQ838_spl),
% 99.77/13.16 inference(contradiction_clause,[status(thm)],[f19883])).
% 99.77/13.16 fof(f22724,definition,(
% 99.77/13.16 sQ944_spl <=> (class_Orderings_Opreorder(tc_bool))),
% 99.77/13.16 introduced(definition,[new_symbols(definition,[sQ944_spl])],[split_symbol_definition])).
% 99.77/13.16 fof(f22726,plain,(
% 99.77/13.16 ~class_Orderings_Opreorder(tc_bool)|sQ944_spl),
% 99.77/13.16 inference(component_clause,[status(thm)],[f22724])).
% 99.77/13.16 fof(f23070,plain,(
% 99.77/13.17 $false|sQ944_spl),
% 99.77/13.17 inference(forward_subsumption_resolution,[status(thm)],[f22726,f1331])).
% 99.77/13.17 fof(f23071,plain,(
% 99.77/13.17 sQ944_spl),
% 99.77/13.17 inference(contradiction_clause,[status(thm)],[f23070])).
% 99.77/13.17 fof(f26715,definition,(
% 99.77/13.17 sQ1093_spl <=> (c_lessequals(v_R____,v_R____,tc_bool))),
% 99.77/13.17 introduced(definition,[new_symbols(definition,[sQ1093_spl])],[split_symbol_definition])).
% 99.77/13.17 fof(f26717,plain,(
% 99.77/13.17 ~c_lessequals(v_R____,v_R____,tc_bool)|sQ1093_spl),
% 99.77/13.17 inference(component_clause,[status(thm)],[f26715])).
% 99.77/13.17 fof(f26719,definition,(
% 99.77/13.17 sQ1094_spl <=> (c_lessequals(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_bool))),
% 99.77/13.17 introduced(definition,[new_symbols(definition,[sQ1094_spl])],[split_symbol_definition])).
% 99.77/13.17 fof(f26721,plain,(
% 99.77/13.17 ~c_lessequals(v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_bool)|sQ1094_spl),
% 99.77/13.17 inference(component_clause,[status(thm)],[f26719])).
% 99.77/13.17 fof(f27622,definition,(
% 99.77/13.17 sQ1120_spl <=> (c_lessequals(c_Complete__Lattice_OInf__class_OInf(c_Arrow__Order__Mirabelle_OLin,tc_bool),c_Complete__Lattice_OInf__class_OInf(c_Arrow__Order__Mirabelle_OLin,tc_bool),tc_bool))),
% 99.77/13.17 introduced(definition,[new_symbols(definition,[sQ1120_spl])],[split_symbol_definition])).
% 99.77/13.17 fof(f27624,plain,(
% 99.77/13.17 ~c_lessequals(c_Complete__Lattice_OInf__class_OInf(c_Arrow__Order__Mirabelle_OLin,tc_bool),c_Complete__Lattice_OInf__class_OInf(c_Arrow__Order__Mirabelle_OLin,tc_bool),tc_bool)|sQ1120_spl),
% 99.77/13.17 inference(component_clause,[status(thm)],[f27622])).
% 99.77/13.17 fof(f27635,definition,(
% 99.77/13.17 sQ1121_spl <=> (c_Complete__Lattice_OInf__class_OInf(c_Arrow__Order__Mirabelle_OLin,tc_bool)=c_Complete__Lattice_OInf__class_OInf(c_Arrow__Order__Mirabelle_OLin,tc_bool))),
% 99.77/13.17 introduced(definition,[new_symbols(definition,[sQ1121_spl])],[split_symbol_definition])).
% 99.77/13.17 fof(f27637,plain,(
% 99.77/13.17 ~c_Complete__Lattice_OInf__class_OInf(c_Arrow__Order__Mirabelle_OLin,tc_bool)=c_Complete__Lattice_OInf__class_OInf(c_Arrow__Order__Mirabelle_OLin,tc_bool)|sQ1121_spl),
% 99.77/13.17 inference(component_clause,[status(thm)],[f27635])).
% 99.77/13.17 fof(f27649,plain,(
% 99.77/13.17 $false|sQ1121_spl),
% 99.77/13.17 inference(trivial_equality_resolution,[status(thm)],[f27637])).
% 99.77/13.17 fof(f27650,plain,(
% 99.77/13.17 sQ1121_spl),
% 99.77/13.17 inference(contradiction_clause,[status(thm)],[f27649])).
% 99.77/13.17 fof(f32906,definition,(
% 99.77/13.17 sQ1327_spl <=> (class_HOL_Oord(tc_bool))),
% 99.77/13.17 introduced(definition,[new_symbols(definition,[sQ1327_spl])],[split_symbol_definition])).
% 99.77/13.17 fof(f32908,plain,(
% 99.77/13.17 ~class_HOL_Oord(tc_bool)|sQ1327_spl),
% 99.77/13.17 inference(component_clause,[status(thm)],[f32906])).
% 99.77/13.17 fof(f32985,plain,(
% 99.77/13.17 $false|sQ1327_spl),
% 99.77/13.17 inference(forward_subsumption_resolution,[status(thm)],[f32908,f1335])).
% 99.77/13.17 fof(f32986,plain,(
% 99.77/13.17 sQ1327_spl),
% 99.77/13.17 inference(contradiction_clause,[status(thm)],[f32985])).
% 99.77/13.17 fof(f36315,plain,(
% 99.77/13.17 $false|sQ11_spl),
% 99.77/13.17 inference(trivial_equality_resolution,[status(thm)],[f1899])).
% 99.77/13.17 fof(f36316,plain,(
% 99.77/13.17 sQ11_spl),
% 99.77/13.17 inference(contradiction_clause,[status(thm)],[f36315])).
% 99.77/13.17 fof(f36415,plain,(
% 99.77/13.17 $false|sQ683_spl),
% 99.77/13.17 inference(trivial_equality_resolution,[status(thm)],[f17052])).
% 99.77/13.17 fof(f36416,plain,(
% 60.31/13.27 sQ683_spl),
% 60.31/13.27 inference(contradiction_clause,[status(thm)],[f36415])).
% 60.31/13.27 fof(f40606,plain,(
% 60.31/13.27 $false|sQ1094_spl),
% 60.31/13.27 inference(forward_subsumption_resolution,[status(thm)],[f26721,f1356])).
% 60.31/13.27 fof(f40607,plain,(
% 60.31/13.27 sQ1094_spl),
% 60.31/13.27 inference(contradiction_clause,[status(thm)],[f40606])).
% 60.31/13.27 fof(f40608,plain,(
% 60.31/13.27 $false|sQ1093_spl),
% 60.31/13.27 inference(forward_subsumption_resolution,[status(thm)],[f26717,f1356])).
% 60.31/13.27 fof(f40609,plain,(
% 60.31/13.27 sQ1093_spl),
% 60.31/13.27 inference(contradiction_clause,[status(thm)],[f40608])).
% 60.31/13.27 fof(f40640,plain,(
% 60.31/13.27 $false|sQ1120_spl),
% 60.31/13.27 inference(forward_subsumption_resolution,[status(thm)],[f27624,f1356])).
% 60.31/13.27 fof(f40641,plain,(
% 60.31/13.27 sQ1120_spl),
% 60.31/13.27 inference(contradiction_clause,[status(thm)],[f40640])).
% 60.31/13.27 fof(f41953,plain,(
% 60.31/13.27 c_in(c_Pair(v_a,v_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_sko__Arrow__Order__Mirabelle__Xlinear__alt__1,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~sQ91_spl),
% 60.31/13.27 inference(resolution,[status(thm)],[f1068,f15620])).
% 60.31/13.27 fof(f41957,plain,(
% 60.31/13.27 $false|sQ107_spl|~sQ91_spl),
% 60.31/13.27 inference(forward_subsumption_resolution,[status(thm)],[f41953,f3630])).
% 60.31/13.27 fof(f41958,plain,(
% 60.31/13.27 sQ107_spl|~sQ91_spl),
% 60.31/13.27 inference(contradiction_clause,[status(thm)],[f41957])).
% 60.31/13.27 fof(f41959,plain,(
% 60.31/13.27 $false),
% 60.31/13.27 inference(sat_refutation,[status(thm)],[f3358,f3415,f3451,f3502,f3504,f3631,f3845,f3955,f4195,f4593,f5740,f6455,f8738,f10483,f12157,f16621,f18679,f19692,f19936,f23071,f27650,f32986,f36316,f36416,f40607,f40609,f40641,f41958])).
% 60.31/13.27 % SZS output end CNFRefutation for theBenchmark.p
% 54.51/13.32 % Elapsed time: 12.878078 seconds
% 54.51/13.32 % CPU time: 100.842974 seconds
% 54.51/13.32 % Total memory used: 705.311 MB
% 54.51/13.32 % Net memory used: 668.464 MB
%------------------------------------------------------------------------------