%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT074-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 : n013.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:17 PM UTC 2026
% Result : Unsatisfiable 49.76s 16.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SCT074-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/10.46 % Computer : n013.cluster.edu
% 0.15/10.46 % Model : x86_64 x86_64
% 0.15/10.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/10.46 % Memory : 8046.5625MB
% 0.15/10.46 % OS : Linux 6.8.0-71-generic
% 0.15/10.46 % CPULimit : 300
% 0.15/10.46 % WCLimit : 300
% 0.15/10.46 % DateTime : Mon Sep 21 04:29:32 UTC 2026
% 0.15/10.47 % CPUTime :
% 0.19/10.52 % Drodi V4.1.1
% 49.76/16.89 % Refutation found
% 49.76/16.89 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 49.76/16.89 % SZS output start CNFRefutation for theBenchmark
% 49.76/16.89 fof(f6,axiom,(
% 49.76/16.89 (![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)) ))),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f94,axiom,(
% 49.76/16.89 (![T_a,V_x]: (( ~ class_Lattices_Obounded__lattice(T_a)| c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(T_a),V_x,T_a) = c_Orderings_Obot__class_Obot(T_a) ) ))),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f126,axiom,(
% 49.76/16.89 (![T_a,V_x]: (~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)) ))),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f283,axiom,(
% 49.76/16.89 (![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) ) ))),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f292,axiom,(
% 49.76/16.89 (![V_x,V_A,T_a]: (hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)) ))),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f392,axiom,(
% 49.76/16.89 (![V_p,V_r,T_a]: (( c_in(V_p,c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a))| ~ c_in(V_p,V_r,tc_prod(T_a,T_a)) ) ))),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f393,axiom,(
% 49.76/16.89 (![V_x,V_y,V_L]: (( ~ 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))| ~ 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))| 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)) ) ))),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f588,axiom,(
% 49.76/16.89 (![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)) ) ))),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f685,axiom,(
% 49.76/16.89 (![V_x,V_S,T_a]: (( c_in(V_x,V_S,T_a)| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f686,axiom,(
% 49.76/16.89 (![V_S,V_x,T_a]: (( hBOOL(hAPP(V_S,V_x))| ~ c_in(V_x,V_S,T_a) ) ))),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f687,axiom,(
% 49.76/16.89 c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f688,axiom,(
% 49.76/16.89 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f689,negated_conjecture,(
% 49.76/16.89 c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f702,axiom,(
% 49.76/16.89 class_Lattices_Obounded__lattice(tc_bool) ),
% 49.76/16.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.76/16.89 fof(f716,plain,(
% 49.76/16.89 ![X0,X1,X2]: (~c_Set_Oinsert(X0,X1,X2)=c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f6])).
% 49.76/16.89 fof(f844,plain,(
% 49.76/16.89 ![T_a]: (~class_Lattices_Obounded__lattice(T_a)|(![V_x]: c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(T_a),V_x,T_a)=c_Orderings_Obot__class_Obot(T_a)))),
% 49.76/16.89 inference(miniscoping,[status(thm)],[f94])).
% 49.76/16.89 fof(f845,plain,(
% 49.76/16.89 ![X0,X1]: (~class_Lattices_Obounded__lattice(X0)|c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(X0),X1,X0)=c_Orderings_Obot__class_Obot(X0))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f844])).
% 49.76/16.89 fof(f892,plain,(
% 49.76/16.89 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f126])).
% 49.76/16.89 fof(f1128,plain,(
% 49.76/16.89 ![X0,X1,X2]: (c_Set_Oinsert(X0,X1,X2)=X1|~c_in(X0,X1,X2))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f283])).
% 49.76/16.89 fof(f1140,plain,(
% 49.76/16.89 ![X0,X1,X2]: (hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f292])).
% 49.76/16.89 fof(f1295,plain,(
% 49.76/16.89 ![X0,X1,X2]: (c_in(X0,c_Transitive__Closure_Ortrancl(X1,X2),tc_prod(X2,X2))|~c_in(X0,X1,tc_prod(X2,X2)))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f392])).
% 49.76/16.89 fof(f1296,plain,(
% 49.76/16.89 ![V_L]: ((![V_x,V_y]: ((~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))|~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)))|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)))),
% 49.76/16.89 inference(miniscoping,[status(thm)],[f393])).
% 49.76/16.89 fof(f1297,plain,(
% 49.76/16.89 ![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))|X0=X1|~c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f1296])).
% 49.76/16.89 fof(f1566,plain,(
% 49.76/16.89 ![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)))),
% 49.76/16.89 inference(miniscoping,[status(thm)],[f588])).
% 49.76/16.89 fof(f1567,plain,(
% 49.76/16.89 ![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)))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f1566])).
% 49.76/16.89 fof(f1732,plain,(
% 49.76/16.89 ![V_x,V_S]: ((![T_a]: c_in(V_x,V_S,T_a))|~hBOOL(hAPP(V_S,V_x)))),
% 49.76/16.89 inference(miniscoping,[status(thm)],[f685])).
% 49.76/16.89 fof(f1733,plain,(
% 49.76/16.89 ![X0,X1,X2]: (c_in(X0,X1,X2)|~hBOOL(hAPP(X1,X0)))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f1732])).
% 49.76/16.89 fof(f1734,plain,(
% 49.76/16.89 ![V_S,V_x]: (hBOOL(hAPP(V_S,V_x))|(![T_a]: ~c_in(V_x,V_S,T_a)))),
% 49.76/16.89 inference(miniscoping,[status(thm)],[f686])).
% 49.76/16.89 fof(f1735,plain,(
% 49.76/16.89 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|~c_in(X1,X0,X2))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f1734])).
% 49.76/16.89 fof(f1736,plain,(
% 49.76/16.89 c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f687])).
% 49.76/16.89 fof(f1737,plain,(
% 49.76/16.89 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f688])).
% 49.76/16.89 fof(f1738,plain,(
% 49.76/16.89 c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f689])).
% 49.76/16.89 fof(f1760,plain,(
% 49.76/16.89 class_Lattices_Obounded__lattice(tc_bool)),
% 49.76/16.89 inference(cnf_transformation,[status(thm)],[f702])).
% 49.76/16.89 fof(f4677,plain,(
% 49.76/16.89 ![X0]: (c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(tc_bool),X0,tc_bool)=c_Orderings_Obot__class_Obot(tc_bool))),
% 49.76/16.89 inference(resolution,[status(thm)],[f845,f1760])).
% 49.76/16.89 fof(f4915,plain,(
% 49.76/16.89 c_Set_Oinsert(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))=c_Arrow__Order__Mirabelle_OLin),
% 49.76/16.89 inference(resolution,[status(thm)],[f1128,f1736])).
% 49.76/16.89 fof(f4916,plain,(
% 49.76/16.89 c_Set_Oinsert(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))=v_Lab____),
% 49.76/16.89 inference(resolution,[status(thm)],[f1128,f1737])).
% 49.76/16.89 fof(f4917,plain,(
% 49.76/16.89 c_Set_Oinsert(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))=v_Lab____),
% 49.76/16.89 inference(resolution,[status(thm)],[f1128,f1738])).
% 49.76/16.89 fof(f5083,plain,(
% 49.76/16.89 hBOOL(hAPP(v_Lab____,c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 49.76/16.89 inference(paramodulation,[status(thm)],[f4917,f1140])).
% 49.76/16.89 fof(f5171,plain,(
% 49.76/16.89 hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,v_Lab____))),
% 49.76/16.89 inference(paramodulation,[status(thm)],[f4915,f1140])).
% 49.76/16.89 fof(f5226,plain,(
% 49.76/16.89 hBOOL(hAPP(v_Lab____,c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 49.76/16.89 inference(paramodulation,[status(thm)],[f4916,f1140])).
% 49.76/16.89 fof(f6098,plain,(
% 49.76/16.89 ![X0]: (c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,X0))),
% 49.76/16.89 inference(resolution,[status(thm)],[f1733,f5171])).
% 49.76/16.89 fof(f6099,plain,(
% 49.76/16.89 ![X0]: (c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,X0))),
% 49.76/16.89 inference(resolution,[status(thm)],[f1733,f5226])).
% 49.76/16.89 fof(f6100,plain,(
% 49.76/16.89 ![X0]: (c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,X0))),
% 49.76/16.89 inference(resolution,[status(thm)],[f1733,f5083])).
% 49.76/16.89 fof(f6799,definition,(
% 49.76/16.89 sQ184_spl <=> (c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 49.76/16.89 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 49.76/16.89 fof(f6801,plain,(
% 49.76/16.89 ~c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))|sQ184_spl),
% 49.76/16.89 inference(component_clause,[status(thm)],[f6799])).
% 49.76/16.89 fof(f31523,plain,(
% 49.76/16.89 ![X0]: (c_in(v_Lab____,c_Transitive__Closure_Ortrancl(c_Arrow__Order__Mirabelle_OLin,X0),tc_prod(X0,X0)))),
% 49.76/16.89 inference(resolution,[status(thm)],[f1295,f6098])).
% 49.76/16.89 fof(f31545,plain,(
% 49.76/16.89 ~c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_a____=v_b____|~c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
% 49.76/16.89 inference(resolution,[status(thm)],[f1297,f6099])).
% 49.76/16.89 fof(f31572,definition,(
% 49.76/16.89 sQ1131_spl <=> (v_a____=v_b____)),
% 49.76/16.89 introduced(definition,[new_symbols(definition,[sQ1131_spl])],[split_symbol_definition])).
% 49.76/16.89 fof(f31573,plain,(
% 49.76/16.89 v_a____=v_b____|~sQ1131_spl),
% 49.76/16.89 inference(component_clause,[status(thm)],[f31572])).
% 49.76/16.89 fof(f31576,definition,(
% 49.76/16.89 sQ1132_spl <=> (c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 49.76/16.89 introduced(definition,[new_symbols(definition,[sQ1132_spl])],[split_symbol_definition])).
% 49.76/16.89 fof(f31578,plain,(
% 49.76/16.89 ~c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|sQ1132_spl),
% 49.76/16.89 inference(component_clause,[status(thm)],[f31576])).
% 49.76/16.89 fof(f31579,plain,(
% 49.76/16.89 ~sQ1132_spl|sQ1131_spl|~sQ184_spl),
% 49.76/16.89 inference(split_clause,[status(thm)],[f31545,f31576,f31572,f6799])).
% 49.76/16.89 fof(f31611,plain,(
% 49.76/16.89 $false|sQ184_spl),
% 49.76/16.89 inference(forward_subsumption_resolution,[status(thm)],[f6801,f6098])).
% 49.76/16.89 fof(f31612,plain,(
% 49.76/16.89 sQ184_spl),
% 49.76/16.89 inference(contradiction_clause,[status(thm)],[f31611])).
% 49.76/16.89 fof(f31614,plain,(
% 49.76/16.89 $false|sQ1132_spl),
% 49.76/16.89 inference(forward_subsumption_resolution,[status(thm)],[f31578,f6100])).
% 49.76/16.89 fof(f31615,plain,(
% 49.76/16.89 sQ1132_spl),
% 49.76/16.89 inference(contradiction_clause,[status(thm)],[f31614])).
% 49.76/16.89 fof(f31803,plain,(
% 49.76/16.89 ![X0]: (c_in(c_Pair(v_a____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,X0)|~sQ1131_spl)),
% 49.76/16.89 inference(backward_demodulation,[status(thm)],[f31573,f6100])).
% 49.76/16.89 fof(f31898,plain,(
% 49.76/16.89 ![X0]: (hBOOL(hAPP(c_Transitive__Closure_Ortrancl(c_Arrow__Order__Mirabelle_OLin,X0),v_Lab____)))),
% 49.76/16.89 inference(resolution,[status(thm)],[f31523,f1735])).
% 49.76/16.89 fof(f31931,plain,(
% 49.76/16.89 ![X0,X1]: (c_in(v_Lab____,c_Transitive__Closure_Ortrancl(c_Arrow__Order__Mirabelle_OLin,X0),X1))),
% 49.76/16.89 inference(resolution,[status(thm)],[f31898,f1733])).
% 49.76/16.89 fof(f31953,plain,(
% 49.76/16.89 ![X0,X1]: (c_Set_Oinsert(v_Lab____,c_Transitive__Closure_Ortrancl(c_Arrow__Order__Mirabelle_OLin,X0),X1)=c_Transitive__Closure_Ortrancl(c_Arrow__Order__Mirabelle_OLin,X0))),
% 49.76/16.89 inference(resolution,[status(thm)],[f31931,f1128])).
% 49.76/16.89 fof(f32054,definition,(
% 49.76/16.89 sQ1141_spl <=> (c_in(c_Pair(v_a____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 49.76/16.89 introduced(definition,[new_symbols(definition,[sQ1141_spl])],[split_symbol_definition])).
% 49.76/16.89 fof(f32056,plain,(
% 49.76/16.89 ~c_in(c_Pair(v_a____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|sQ1141_spl),
% 49.76/16.89 inference(component_clause,[status(thm)],[f32054])).
% 49.76/16.89 fof(f32070,plain,(
% 49.76/16.89 $false|~sQ1131_spl|sQ1141_spl),
% 49.76/16.89 inference(forward_subsumption_resolution,[status(thm)],[f32056,f31803])).
% 49.76/16.89 fof(f32071,plain,(
% 49.76/16.89 ~sQ1131_spl|sQ1141_spl),
% 49.76/16.89 inference(contradiction_clause,[status(thm)],[f32070])).
% 49.76/16.89 fof(f32602,plain,(
% 49.76/16.89 ![X0,X1]: (~c_Transitive__Closure_Ortrancl(c_Arrow__Order__Mirabelle_OLin,X0)=c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),
% 49.76/16.89 inference(paramodulation,[status(thm)],[f31953,f716])).
% 49.76/16.89 fof(f35803,definition,(
% 49.76/16.89 ![X0,X1]: (sQ1265_spl <=> (hBOOL(hAPP(X0,X1))|hBOOL(hAPP(X0,hAPP(c_Arrow__Order__Mirabelle_OLin,v_Lab____)))))),
% 49.76/16.89 introduced(definition,[new_symbols(definition,[sQ1265_spl])],[split_symbol_definition])).
% 49.76/16.89 fof(f35804,plain,(
% 49.76/16.89 ![X0,X1]: (hBOOL(hAPP(X0,X1))|hBOOL(hAPP(X0,hAPP(c_Arrow__Order__Mirabelle_OLin,v_Lab____)))|~sQ1265_spl)),
% 49.76/16.89 inference(component_clause,[status(thm)],[f35803])).
% 49.76/16.89 fof(f35810,definition,(
% 49.76/16.89 ![X0,X1,X2]: (sQ1267_spl <=> (hBOOL(hAPP(X0,X1))|hBOOL(hAPP(X0,X2))))),
% 49.76/16.89 introduced(definition,[new_symbols(definition,[sQ1267_spl])],[split_symbol_definition])).
% 49.76/16.89 fof(f35811,plain,(
% 49.76/16.89 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|hBOOL(hAPP(X0,X2))|~sQ1267_spl)),
% 49.76/16.89 inference(component_clause,[status(thm)],[f35810])).
% 49.76/16.89 fof(f35847,plain,(
% 49.76/16.89 $false|~sQ1267_spl),
% 49.76/16.89 inference(resolution,[status(thm)],[f35811,f892])).
% 49.76/16.89 fof(f35921,plain,(
% 49.76/16.89 ~sQ1267_spl),
% 49.76/16.89 inference(contradiction_clause,[status(thm)],[f35847])).
% 49.76/16.89 fof(f36267,plain,(
% 49.76/16.89 $false|~sQ1265_spl),
% 49.76/16.89 inference(resolution,[status(thm)],[f35804,f892])).
% 49.76/16.89 fof(f36334,plain,(
% 49.76/16.89 ~sQ1265_spl),
% 49.76/16.89 inference(contradiction_clause,[status(thm)],[f36267])).
% 49.76/16.89 fof(f40114,definition,(
% 49.76/16.89 ![X0]: (sQ1335_spl <=> (~X0=c_Orderings_Obot__class_Obot(tc_bool)))),
% 49.76/16.89 introduced(definition,[new_symbols(definition,[sQ1335_spl])],[split_symbol_definition])).
% 49.76/16.89 fof(f40115,plain,(
% 49.76/16.89 ![X0]: (~X0=c_Orderings_Obot__class_Obot(tc_bool)|~sQ1335_spl)),
% 49.76/16.89 inference(component_clause,[status(thm)],[f40114])).
% 49.76/16.89 fof(f40119,plain,(
% 49.76/16.89 $false|~sQ1335_spl),
% 49.76/16.89 inference(backward_subsumption_resolution,[status(thm)],[f4677,f40115])).
% 49.76/16.89 fof(f40146,plain,(
% 42.74/16.92 ~sQ1335_spl),
% 42.74/16.92 inference(contradiction_clause,[status(thm)],[f40119])).
% 42.74/16.92 fof(f41254,definition,(
% 42.74/16.92 ![X0,X1]: (sQ1338_spl <=> (X0=X1))),
% 42.74/16.92 introduced(definition,[new_symbols(definition,[sQ1338_spl])],[split_symbol_definition])).
% 42.74/16.92 fof(f41255,plain,(
% 42.74/16.92 ![X0,X1]: (X0=X1|~sQ1338_spl)),
% 42.74/16.92 inference(component_clause,[status(thm)],[f41254])).
% 42.74/16.92 fof(f41333,plain,(
% 42.74/16.92 $false|~sQ1338_spl),
% 42.74/16.92 inference(backward_subsumption_resolution,[status(thm)],[f32602,f41255])).
% 42.74/16.92 fof(f41348,plain,(
% 42.74/16.92 ~sQ1338_spl),
% 42.74/16.92 inference(contradiction_clause,[status(thm)],[f41333])).
% 42.74/16.92 fof(f41367,plain,(
% 42.74/16.92 ~c_in(c_Pair(v_a____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))|~sQ1131_spl),
% 42.74/16.92 inference(resolution,[status(thm)],[f1567,f31803])).
% 42.74/16.92 fof(f41383,plain,(
% 42.74/16.92 ~sQ1141_spl|~sQ184_spl|~sQ1131_spl),
% 42.74/16.92 inference(split_clause,[status(thm)],[f41367,f32054,f6799,f31572])).
% 42.74/16.92 fof(f41403,plain,(
% 42.74/16.92 $false),
% 42.74/16.92 inference(sat_refutation,[status(thm)],[f31579,f31612,f31615,f32071,f35921,f36334,f40146,f41348,f41383])).
% 42.74/16.92 % SZS output end CNFRefutation for theBenchmark.p
% 5.04/17.03 % Elapsed time: 6.550435 seconds
% 5.04/17.03 % CPU time: 51.183720 seconds
% 5.04/17.03 % Total memory used: 945.782 MB
% 5.04/17.03 % Net memory used: 920.321 MB
%------------------------------------------------------------------------------