%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT041-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:14 PM UTC 2026
% Result : Unsatisfiable 50.96s 7.18s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT041-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.46 % Computer : n009.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Mon Sep 21 04:27:43 UTC 2026
% 0.20/0.47 % CPUTime :
% 0.24/0.59 % Drodi V4.1.1
% 50.96/7.18 % Refutation found
% 50.96/7.18 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 50.96/7.18 % SZS output start CNFRefutation for theBenchmark
% 50.96/7.18 fof(f645,axiom,(
% 50.96/7.18 (![V_a_H,V_b_H,V_P_H,V_a,V_b,V_P]: (( c_in(c_Pair(V_a_H,V_b_H,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,V_P_H),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),hAPP(v_F,V_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))| ~ c_in(c_Pair(V_a_H,V_b_H,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(V_P_H,v_sko__CHAINED__1(V_P,V_P_H,V_a,V_a_H,V_b,V_b_H)),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),hAPP(V_P,v_sko__CHAINED__1(V_P,V_P_H,V_a,V_a_H,V_b,V_b_H)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))| ~ c_in(V_P_H,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))| ~ c_in(V_P,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))| V_b = V_a_H| V_a = V_b_H| V_a_H = V_b_H| V_a = V_b ) ))),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f646,axiom,(
% 50.96/7.18 (![V_a_H,V_b_H,V_P_H,V_a,V_b,V_P]: (( c_in(c_Pair(V_a_H,V_b_H,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,V_P_H),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),hAPP(v_F,V_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))| c_in(c_Pair(V_a_H,V_b_H,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(V_P_H,v_sko__CHAINED__1(V_P,V_P_H,V_a,V_a_H,V_b,V_b_H)),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),hAPP(V_P,v_sko__CHAINED__1(V_P,V_P_H,V_a,V_a_H,V_b,V_b_H)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))| ~ c_in(V_P_H,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))| ~ c_in(V_P,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))| V_b = V_a_H| V_a = V_b_H| V_a_H = V_b_H| V_a = V_b ) ))),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f647,axiom,(
% 50.96/7.18 (![V_i]: (( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))| ~ c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ) ))),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f648,axiom,(
% 50.96/7.18 (![V_i]: (( c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,V_i),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),hAPP(v_P____,V_i),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ) ))),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f649,axiom,(
% 50.96/7.18 c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))) ),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f650,axiom,(
% 50.96/7.18 c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))) ),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f651,axiom,(
% 50.96/7.18 v_b____ != v_a_H____ ),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f652,axiom,(
% 50.96/7.18 v_a____ != v_b_H____ ),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f653,axiom,(
% 50.96/7.18 v_a_H____ != v_b_H____ ),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f654,axiom,(
% 50.96/7.18 v_a____ != v_b____ ),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f655,negated_conjecture,(
% 50.96/7.18 ( ~ c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ) ),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f656,negated_conjecture,(
% 50.96/7.18 ( c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))| c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ) ),
% 50.96/7.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.96/7.18 fof(f1628,plain,(
% 50.96/7.18 ![V_a,V_b]: ((![V_a_H,V_b_H]: ((((![V_P]: ((![V_P_H]: ((((c_in(c_Pair(V_a_H,V_b_H,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,V_P_H),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),hAPP(v_F,V_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~c_in(c_Pair(V_a_H,V_b_H,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(V_P_H,v_sko__CHAINED__1(V_P,V_P_H,V_a,V_a_H,V_b,V_b_H)),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),hAPP(V_P,v_sko__CHAINED__1(V_P,V_P_H,V_a,V_a_H,V_b,V_b_H)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~c_in(V_P_H,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))))|~c_in(V_P,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))))|V_b=V_a_H)|V_a=V_b_H)|V_a_H=V_b_H))|V_a=V_b)),
% 50.96/7.18 inference(miniscoping,[status(thm)],[f645])).
% 50.96/7.18 fof(f1629,plain,(
% 50.96/7.18 ![X0,X1,X2,X3,X4,X5]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))|~c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))|X4=X0|X3=X1|X0=X1|X3=X4)),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f1628])).
% 50.96/7.18 fof(f1630,plain,(
% 50.96/7.18 ![V_a,V_b]: ((![V_a_H,V_b_H]: ((((![V_P]: ((![V_P_H]: ((((c_in(c_Pair(V_a_H,V_b_H,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,V_P_H),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),hAPP(v_F,V_P),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|c_in(c_Pair(V_a_H,V_b_H,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(V_P_H,v_sko__CHAINED__1(V_P,V_P_H,V_a,V_a_H,V_b,V_b_H)),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),hAPP(V_P,v_sko__CHAINED__1(V_P,V_P_H,V_a,V_a_H,V_b,V_b_H)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))|~c_in(V_P_H,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))))|~c_in(V_P,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))))|V_b=V_a_H)|V_a=V_b_H)|V_a_H=V_b_H))|V_a=V_b)),
% 50.96/7.18 inference(miniscoping,[status(thm)],[f646])).
% 50.96/7.18 fof(f1631,plain,(
% 50.96/7.18 ![X0,X1,X2,X3,X4,X5]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X5),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X5,v_sko__CHAINED__1(X5,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))|~c_in(X5,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))|X4=X0|X3=X1|X0=X1|X3=X4)),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f1630])).
% 50.96/7.18 fof(f1632,plain,(
% 50.96/7.18 ![X0]: (c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f647])).
% 50.96/7.18 fof(f1633,plain,(
% 50.96/7.18 ![X0]: (c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,X0),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),hAPP(v_P____,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f648])).
% 50.96/7.18 fof(f1634,plain,(
% 50.96/7.18 c_in(v_P_H____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f649])).
% 50.96/7.18 fof(f1635,plain,(
% 50.96/7.18 c_in(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f650])).
% 50.96/7.18 fof(f1636,plain,(
% 50.96/7.18 ~v_b____=v_a_H____),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f651])).
% 50.96/7.18 fof(f1637,plain,(
% 50.96/7.18 ~v_a____=v_b_H____),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f652])).
% 50.96/7.18 fof(f1638,plain,(
% 50.96/7.18 ~v_a_H____=v_b_H____),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f653])).
% 50.96/7.18 fof(f1639,plain,(
% 50.96/7.18 ~v_a____=v_b____),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f654])).
% 50.96/7.18 fof(f1640,plain,(
% 50.96/7.18 ~c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f655])).
% 50.96/7.18 fof(f1641,plain,(
% 50.96/7.18 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(cnf_transformation,[status(thm)],[f656])).
% 50.96/7.18 fof(f2508,plain,(
% 50.96/7.18 ![X0,X1,X2,X3,X4]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(v_P____,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P____,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))|X4=X0|X3=X1|X0=X1|X3=X4)),
% 50.96/7.18 inference(resolution,[status(thm)],[f1629,f1635])).
% 50.96/7.18 fof(f2509,plain,(
% 50.96/7.18 ![X0,X1,X2,X3,X4]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(v_P_H____,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))|X4=X0|X3=X1|X0=X1|X3=X4)),
% 50.96/7.18 inference(resolution,[status(thm)],[f1629,f1634])).
% 50.96/7.18 fof(f2518,plain,(
% 50.96/7.18 ![X0,X1,X2,X3,X4]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(v_P____,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P____,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))|X4=X0|X3=X1|X0=X1|X3=X4)),
% 50.96/7.18 inference(resolution,[status(thm)],[f1631,f1635])).
% 50.96/7.18 fof(f2519,plain,(
% 50.96/7.18 ![X0,X1,X2,X3,X4]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,X2),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(X2,v_sko__CHAINED__1(v_P_H____,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X3,X4,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,X2,X3,X0,X4,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(X2,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))|X4=X0|X3=X1|X0=X1|X3=X4)),
% 50.96/7.18 inference(resolution,[status(thm)],[f1631,f1634])).
% 50.96/7.18 fof(f2861,plain,(
% 50.96/7.18 ![X0,X1,X2,X3]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P____,v_P_H____,X2,X0,X3,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,X2,X0,X3,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|X3=X0|X2=X1|X0=X1|X2=X3)),
% 50.96/7.18 inference(resolution,[status(thm)],[f2508,f1634])).
% 50.96/7.18 fof(f2918,plain,(
% 50.96/7.18 ![X0,X1,X2,X3]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,X2,X0,X3,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,X2,X0,X3,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|X3=X0|X2=X1|X0=X1|X2=X3)),
% 50.96/7.18 inference(resolution,[status(thm)],[f2509,f1635])).
% 50.96/7.18 fof(f2977,plain,(
% 50.96/7.18 ![X0,X1,X2,X3]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P____,v_P_H____,X2,X0,X3,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,X2,X0,X3,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|X3=X0|X2=X1|X0=X1|X2=X3)),
% 50.96/7.18 inference(resolution,[status(thm)],[f2518,f1634])).
% 50.96/7.18 fof(f3040,plain,(
% 50.96/7.18 ![X0,X1,X2,X3]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,X2,X0,X3,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X2,X3,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,X2,X0,X3,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|X3=X0|X2=X1|X0=X1|X2=X3)),
% 50.96/7.18 inference(resolution,[status(thm)],[f2519,f1635])).
% 50.96/7.18 fof(f3067,plain,(
% 50.96/7.18 ![X0,X1]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,X0,v_b_H____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,X0,v_b_H____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=X0|v_a_H____=X1|X0=X1|v_a_H____=v_b_H____|c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 50.96/7.18 inference(resolution,[status(thm)],[f3040,f1641])).
% 50.96/7.18 fof(f3078,plain,(
% 50.96/7.18 ![X0,X1]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,X0,v_b_H____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,X0,v_b_H____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=X0|v_a_H____=X1|X0=X1|c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f3067,f1638])).
% 50.96/7.18 fof(f5226,plain,(
% 50.96/7.18 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=v_a____|v_a_H____=v_b____|v_a____=v_b____|c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(resolution,[status(thm)],[f3078,f1633])).
% 50.96/7.18 fof(f5229,plain,(
% 50.96/7.18 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=v_a____|v_a_H____=v_b____|v_a____=v_b____),
% 50.96/7.18 inference(duplicate_literals_removal,[status(thm)],[f5226])).
% 50.96/7.18 fof(f5230,plain,(
% 50.96/7.18 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_a_H____=v_b____|v_a____=v_b____),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f5229,f1637])).
% 50.96/7.18 fof(f5231,plain,(
% 50.96/7.18 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_a____=v_b____),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f5230,f1636])).
% 50.96/7.18 fof(f5232,plain,(
% 50.96/7.18 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_a____=v_b____|c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(resolution,[status(thm)],[f5231,f1632])).
% 50.96/7.18 fof(f5233,plain,(
% 50.96/7.18 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_a____=v_b____|c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|~c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=v_a____|v_a_H____=v_b____|v_a____=v_b____|v_a_H____=v_b_H____),
% 50.96/7.18 inference(resolution,[status(thm)],[f5231,f2918])).
% 50.96/7.18 fof(f5234,plain,(
% 50.96/7.18 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f5232,f1639])).
% 50.96/7.18 fof(f5235,plain,(
% 50.96/7.18 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_a____=v_b____|~c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=v_a____|v_a_H____=v_b____|v_a_H____=v_b_H____),
% 50.96/7.18 inference(duplicate_literals_removal,[status(thm)],[f5233])).
% 50.96/7.18 fof(f5236,plain,(
% 50.96/7.18 v_a____=v_b____|~c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=v_a____|v_a_H____=v_b____|v_a_H____=v_b_H____),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f5235,f1640])).
% 50.96/7.18 fof(f5242,plain,(
% 50.96/7.18 ~c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=v_a____|v_a_H____=v_b____|v_a_H____=v_b_H____),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f5236,f1639])).
% 50.96/7.18 fof(f5243,plain,(
% 50.96/7.18 ~c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=v_a____|v_a_H____=v_b____|v_a_H____=v_b_H____|c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(resolution,[status(thm)],[f5242,f1641])).
% 50.96/7.18 fof(f5256,plain,(
% 50.96/7.18 v_b_H____=v_a____|v_a_H____=v_b____|v_a_H____=v_b_H____|c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f5243,f5234])).
% 50.96/7.18 fof(f5269,plain,(
% 50.96/7.18 v_a_H____=v_b____|v_a_H____=v_b_H____|c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f5256,f1637])).
% 50.96/7.18 fof(f5279,plain,(
% 50.96/7.18 ![X0,X1]: (v_a_H____=v_b____|v_a_H____=v_b_H____|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,X0,v_b____,X1)),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),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,X0,v_b____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b____=X0|v_a____=X1|X0=X1|v_a____=v_b____)),
% 50.96/7.18 inference(resolution,[status(thm)],[f5269,f2977])).
% 50.96/7.18 fof(f5290,plain,(
% 50.96/7.18 ![X0,X1]: (v_a_H____=v_b_H____|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,X0,v_b____,X1)),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),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,X0,v_b____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b____=X0|v_a____=X1|X0=X1|v_a____=v_b____)),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f5279,f1636])).
% 50.96/7.18 fof(f11494,plain,(
% 50.96/7.18 ![X0,X1]: (c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,X0,v_b____,X1)),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),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,X0,v_b____,X1)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b____=X0|v_a____=X1|X0=X1|v_a____=v_b____)),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f5290,f1638])).
% 50.96/7.18 fof(f11495,plain,(
% 50.96/7.18 c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b____=v_a_H____|v_a____=v_b_H____|v_a_H____=v_b_H____|v_a____=v_b____|c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(resolution,[status(thm)],[f11494,f1632])).
% 50.96/7.18 fof(f11506,plain,(
% 50.96/7.18 c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b____=v_a_H____|v_a____=v_b_H____|v_a_H____=v_b_H____|v_a____=v_b____),
% 50.96/7.18 inference(duplicate_literals_removal,[status(thm)],[f11495])).
% 50.96/7.18 fof(f11507,plain,(
% 50.96/7.18 c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_a____=v_b_H____|v_a_H____=v_b_H____|v_a____=v_b____),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f11506,f1636])).
% 50.96/7.18 fof(f11509,plain,(
% 50.96/7.18 c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_a_H____=v_b_H____|v_a____=v_b____),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f11507,f1637])).
% 50.96/7.18 fof(f11510,plain,(
% 50.96/7.18 c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_a_H____=v_b_H____|v_a____=v_b____|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(resolution,[status(thm)],[f11509,f1633])).
% 50.96/7.18 fof(f11519,plain,(
% 50.96/7.18 c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_a____=v_b____|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f11510,f1638])).
% 50.96/7.18 fof(f11536,plain,(
% 50.96/7.18 c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P_H____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f11519,f1639])).
% 50.96/7.18 fof(f11537,plain,(
% 50.96/7.18 c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(resolution,[status(thm)],[f11536,f1632])).
% 50.96/7.18 fof(f11538,plain,(
% 50.96/7.18 c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_F,v_P____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b____=v_a_H____|v_a____=v_b_H____|v_a_H____=v_b_H____|v_a____=v_b____),
% 50.96/7.18 inference(resolution,[status(thm)],[f11536,f2861])).
% 50.96/7.18 fof(f11539,plain,(
% 50.96/7.18 c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),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),hAPP(v_F,v_P____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b____=v_a_H____|v_a____=v_b_H____|v_a_H____=v_b_H____|v_a____=v_b____),
% 50.96/7.18 inference(duplicate_literals_removal,[status(thm)],[f11538])).
% 50.96/7.18 fof(f11540,plain,(
% 50.96/7.18 ~c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),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),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b____=v_a_H____|v_a____=v_b_H____|v_a_H____=v_b_H____|v_a____=v_b____),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f11539,f1640])).
% 50.96/7.18 fof(f11566,plain,(
% 50.96/7.18 ~c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P____,v_P_H____,v_a____,v_a_H____,v_b____,v_b_H____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b____=v_a_H____|v_a____=v_b_H____|v_a_H____=v_b_H____|v_a____=v_b____),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f11540,f5269])).
% 50.96/7.18 fof(f11567,plain,(
% 50.96/7.18 v_b____=v_a_H____|v_a____=v_b_H____|v_a_H____=v_b_H____|v_a____=v_b____|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(resolution,[status(thm)],[f11566,f11537])).
% 50.96/7.18 fof(f11603,plain,(
% 50.96/7.18 v_a____=v_b_H____|v_a_H____=v_b_H____|v_a____=v_b____|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f11567,f1636])).
% 50.96/7.18 fof(f11639,plain,(
% 50.96/7.18 v_a_H____=v_b_H____|v_a____=v_b____|c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f11603,f1637])).
% 50.96/7.18 fof(f11640,plain,(
% 50.96/7.18 v_a_H____=v_b_H____|v_a____=v_b____|~c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=v_a____|v_a_H____=v_b____|v_a_H____=v_b_H____),
% 50.96/7.18 inference(resolution,[status(thm)],[f11639,f5242])).
% 50.96/7.18 fof(f11644,plain,(
% 50.96/7.18 v_a_H____=v_b_H____|v_a____=v_b____|~c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=v_a____|v_a_H____=v_b____),
% 50.96/7.18 inference(duplicate_literals_removal,[status(thm)],[f11640])).
% 50.96/7.18 fof(f11645,plain,(
% 50.96/7.18 v_a____=v_b____|~c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=v_a____|v_a_H____=v_b____),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f11644,f1638])).
% 50.96/7.18 fof(f11651,plain,(
% 50.96/7.18 ~c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_P____,v_sko__CHAINED__1(v_P_H____,v_P____,v_a_H____,v_a____,v_b_H____,v_b____)),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))|v_b_H____=v_a____|v_a_H____=v_b____),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f11645,f1639])).
% 50.96/7.18 fof(f11652,plain,(
% 50.96/7.18 v_b_H____=v_a____|v_a_H____=v_b____|c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(resolution,[status(thm)],[f11651,f5234])).
% 50.96/7.18 fof(f11688,plain,(
% 50.96/7.18 v_a_H____=v_b____|c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(forward_subsumption_resolution,[status(thm)],[f11652,f1637])).
% 50.96/7.18 fof(f11724,plain,(
% 50.96/7.18 ~c_in(c_Pair(v_a_H____,v_b_H____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P_H____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.18 inference(backward_subsumption_resolution,[status(thm)],[f1640,f11729])).
% 50.96/7.18 fof(f11729,plain,(
% 50.96/7.18 c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),hAPP(v_F,v_P____),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),
% 50.96/7.21 inference(forward_subsumption_resolution,[status(thm)],[f11688,f1636])).
% 50.96/7.21 fof(f13250,plain,(
% 50.96/7.21 v_a_H____=v_b_H____|v_a____=v_b____),
% 50.96/7.21 inference(backward_subsumption_resolution,[status(thm)],[f11639,f11724])).
% 50.96/7.21 fof(f13279,plain,(
% 50.96/7.21 v_a____=v_b____),
% 50.96/7.21 inference(forward_subsumption_resolution,[status(thm)],[f13250,f1638])).
% 50.96/7.21 fof(f13281,plain,(
% 50.96/7.21 $false),
% 50.96/7.21 inference(forward_subsumption_resolution,[status(thm)],[f13279,f1639])).
% 50.96/7.21 % SZS output end CNFRefutation for theBenchmark.p
% 3.46/7.45 % Elapsed time: 6.957655 seconds
% 3.46/7.45 % CPU time: 52.983664 seconds
% 3.46/7.45 % Total memory used: 715.001 MB
% 3.46/7.45 % Net memory used: 694.394 MB
%------------------------------------------------------------------------------