%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT139+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:22 PM UTC 2026
% Result : Theorem 57.59s 22.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT139+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/15.37 % Computer : n012.cluster.edu
% 0.09/15.37 % Model : x86_64 x86_64
% 0.09/15.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/15.37 % Memory : 8046.5625MB
% 0.09/15.37 % OS : Linux 6.8.0-71-generic
% 0.09/15.37 % CPULimit : 300
% 0.09/15.37 % WCLimit : 300
% 0.09/15.37 % DateTime : Mon Sep 21 04:33:59 UTC 2026
% 0.09/15.37 % CPUTime :
% 0.12/15.43 % Drodi V4.1.1
% 57.59/22.76 % Refutation found
% 57.59/22.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 57.59/22.76 % SZS output start CNFRefutation for theBenchmark
% 57.59/22.76 fof(f6,axiom,(
% 57.59/22.76 hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_P____),c_Arrow__Order__Mirabelle_OProf)) ),
% 57.59/22.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 57.59/22.76 fof(f17,axiom,(
% 57.59/22.76 (! [V_A_2,V_x_2,T_a] :( hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))<=> hBOOL(hAPP(V_A_2,V_x_2)) ) )),
% 57.59/22.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 57.59/22.76 fof(f35,axiom,(
% 57.59/22.76 (! [V_xs,V_x,T_a] : hAPP(hAPP(c_List_Olist_OCons(T_a),V_x),V_xs) != V_xs )),
% 57.59/22.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 57.59/22.76 fof(f100,axiom,(
% 57.59/22.76 (! [T_a,V_ys,V_xs] :( V_xs = V_ys=> V_xs = hAPP(hAPP(c_List_Oappend(T_a),c_List_Olist_ONil(T_a)),V_ys) ) )),
% 57.59/22.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 57.59/22.76 fof(f159,axiom,(
% 57.59/22.76 (! [V_r_2,V_p_2,T_a] :( hBOOL(hAPP(hAPP(c_member(tc_prod(T_a,T_a)),V_p_2),V_r_2))=> hBOOL(hAPP(hAPP(c_member(tc_prod(T_a,T_a)),V_p_2),c_Transitive__Closure_Ortrancl(T_a,V_r_2))) ) )),
% 57.59/22.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 57.59/22.76 fof(f260,axiom,(
% 57.59/22.76 (! [V_f_2,T_b,V_A_2,V_x_2,T_a] :( hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))=> hBOOL(hAPP(hAPP(c_member(T_b),hAPP(V_f_2,V_x_2)),c_Set_Oimage(T_a,T_b,V_f_2,V_A_2))) ) )),
% 57.59/22.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 57.59/22.76 fof(f326,axiom,(
% 57.59/22.76 (! [V_f_2,T_b,V_A_2,V_x_2,T_a] :( ( hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))=> hAPP(c_FuncSet_Orestrict(T_a,T_b,V_f_2,V_A_2),V_x_2) = hAPP(V_f_2,V_x_2) )& ( ~ hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))=> hAPP(c_FuncSet_Orestrict(T_a,T_b,V_f_2,V_A_2),V_x_2) = c_HOL_Oundefined(T_b) ) ) )),
% 57.59/22.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 57.59/22.76 fof(f511,axiom,(
% 57.59/22.76 (! [V_P,T_a] : hAPP(c_COMBI(T_a),V_P) = V_P )),
% 57.59/22.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 57.59/22.76 fof(f512,axiom,(
% 57.59/22.76 (! [V_Q,V_P,T_b,T_a] : hAPP(c_COMBK(T_a,T_b,V_P),V_Q) = V_P )),
% 57.59/22.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 57.59/22.76 fof(f515,axiom,(
% 57.59/22.76 (! [V_R_2,V_Q_2,V_Pa_2,T_a,T_c,T_b] : hAPP(hAPP(hAPP(c_COMBS(T_b,T_c,T_a),V_Pa_2),V_Q_2),V_R_2) = hAPP(hAPP(V_Pa_2,V_R_2),hAPP(V_Q_2,V_R_2)) )),
% 57.59/22.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 57.59/22.76 fof(f535,plain,(
% 57.59/22.76 hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_P____),c_Arrow__Order__Mirabelle_OProf))),
% 57.59/22.76 inference(cnf_transformation,[status(thm)],[f6])).
% 57.59/22.76 fof(f589,plain,(
% 57.59/22.76 ![V_A_2,V_x_2,T_a]: ((~hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))|hBOOL(hAPP(V_A_2,V_x_2)))&(hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))|~hBOOL(hAPP(V_A_2,V_x_2))))),
% 57.59/22.76 inference(NNF_transformation,[status(thm)],[f17])).
% 57.59/22.76 fof(f590,plain,(
% 57.59/22.76 (![V_A_2,V_x_2]: ((![T_a]: ~hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2)))|hBOOL(hAPP(V_A_2,V_x_2))))&(![V_A_2,V_x_2]: ((![T_a]: hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2)))|~hBOOL(hAPP(V_A_2,V_x_2))))),
% 57.59/22.76 inference(miniscoping,[status(thm)],[f589])).
% 57.59/22.76 fof(f591,plain,(
% 57.59/22.76 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|hBOOL(hAPP(X2,X1)))),
% 57.59/22.76 inference(cnf_transformation,[status(thm)],[f590])).
% 57.59/22.76 fof(f592,plain,(
% 57.59/22.76 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|~hBOOL(hAPP(X2,X1)))),
% 57.59/22.76 inference(cnf_transformation,[status(thm)],[f590])).
% 57.59/22.76 fof(f658,plain,(
% 57.59/22.76 ![X0,X1,X2]: (~hAPP(hAPP(c_List_Olist_OCons(X0),X1),X2)=X2)),
% 57.59/22.76 inference(cnf_transformation,[status(thm)],[f35])).
% 57.59/22.76 fof(f887,plain,(
% 57.59/22.76 ![T_a,V_ys,V_xs]: (~V_xs=V_ys|V_xs=hAPP(hAPP(c_List_Oappend(T_a),c_List_Olist_ONil(T_a)),V_ys))),
% 57.59/22.76 inference(pre_NNF_transformation,[status(thm)],[f100])).
% 57.59/22.76 fof(f888,plain,(
% 57.59/22.76 ![V_ys,V_xs]: (~V_xs=V_ys|(![T_a]: V_xs=hAPP(hAPP(c_List_Oappend(T_a),c_List_Olist_ONil(T_a)),V_ys)))),
% 57.59/22.76 inference(miniscoping,[status(thm)],[f887])).
% 57.59/22.76 fof(f889,plain,(
% 57.59/22.76 ![X0,X1,X2]: (~X0=X1|X0=hAPP(hAPP(c_List_Oappend(X2),c_List_Olist_ONil(X2)),X1))),
% 57.59/22.76 inference(cnf_transformation,[status(thm)],[f888])).
% 57.59/22.76 fof(f1085,plain,(
% 57.59/22.76 ![V_r_2,V_p_2,T_a]: (~hBOOL(hAPP(hAPP(c_member(tc_prod(T_a,T_a)),V_p_2),V_r_2))|hBOOL(hAPP(hAPP(c_member(tc_prod(T_a,T_a)),V_p_2),c_Transitive__Closure_Ortrancl(T_a,V_r_2))))),
% 57.59/22.76 inference(pre_NNF_transformation,[status(thm)],[f159])).
% 57.59/22.76 fof(f1086,plain,(
% 57.59/22.76 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_member(tc_prod(X0,X0)),X1),X2))|hBOOL(hAPP(hAPP(c_member(tc_prod(X0,X0)),X1),c_Transitive__Closure_Ortrancl(X0,X2))))),
% 57.59/22.76 inference(cnf_transformation,[status(thm)],[f1085])).
% 57.59/22.76 fof(f1413,plain,(
% 57.59/22.76 ![V_f_2,T_b,V_A_2,V_x_2,T_a]: (~hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))|hBOOL(hAPP(hAPP(c_member(T_b),hAPP(V_f_2,V_x_2)),c_Set_Oimage(T_a,T_b,V_f_2,V_A_2))))),
% 57.59/22.76 inference(pre_NNF_transformation,[status(thm)],[f260])).
% 57.59/22.76 fof(f1414,plain,(
% 57.59/22.76 ![V_A_2,V_x_2,T_a]: (~hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))|(![V_f_2,T_b]: hBOOL(hAPP(hAPP(c_member(T_b),hAPP(V_f_2,V_x_2)),c_Set_Oimage(T_a,T_b,V_f_2,V_A_2)))))),
% 57.59/22.76 inference(miniscoping,[status(thm)],[f1413])).
% 57.59/22.76 fof(f1415,plain,(
% 57.59/22.76 ![X0,X1,X2,X3,X4]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|hBOOL(hAPP(hAPP(c_member(X3),hAPP(X4,X1)),c_Set_Oimage(X0,X3,X4,X2))))),
% 57.59/22.76 inference(cnf_transformation,[status(thm)],[f1414])).
% 57.59/22.76 fof(f1601,plain,(
% 57.59/22.76 ![V_f_2,T_b,V_A_2,V_x_2,T_a]: ((~hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))|hAPP(c_FuncSet_Orestrict(T_a,T_b,V_f_2,V_A_2),V_x_2)=hAPP(V_f_2,V_x_2))&(hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))|hAPP(c_FuncSet_Orestrict(T_a,T_b,V_f_2,V_A_2),V_x_2)=c_HOL_Oundefined(T_b)))),
% 57.59/22.76 inference(pre_NNF_transformation,[status(thm)],[f326])).
% 57.59/22.76 fof(f1602,plain,(
% 57.59/22.76 (![V_A_2,V_x_2,T_a]: (~hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))|(![V_f_2,T_b]: hAPP(c_FuncSet_Orestrict(T_a,T_b,V_f_2,V_A_2),V_x_2)=hAPP(V_f_2,V_x_2))))&(![V_A_2,V_x_2,T_a]: (hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))|(![V_f_2,T_b]: hAPP(c_FuncSet_Orestrict(T_a,T_b,V_f_2,V_A_2),V_x_2)=c_HOL_Oundefined(T_b))))),
% 57.59/22.76 inference(miniscoping,[status(thm)],[f1601])).
% 57.59/22.76 fof(f1603,plain,(
% 57.59/22.76 ![X0,X1,X2,X3,X4]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|hAPP(c_FuncSet_Orestrict(X0,X3,X4,X2),X1)=hAPP(X4,X1))),
% 57.59/22.76 inference(cnf_transformation,[status(thm)],[f1602])).
% 57.59/22.76 fof(f2160,plain,(
% 57.59/22.76 ![X0,X1]: (hAPP(c_COMBI(X0),X1)=X1)),
% 57.59/22.76 inference(cnf_transformation,[status(thm)],[f511])).
% 57.59/22.76 fof(f2161,plain,(
% 57.59/22.76 ![X0,X1,X2,X3]: (hAPP(c_COMBK(X0,X1,X2),X3)=X2)),
% 57.59/22.76 inference(cnf_transformation,[status(thm)],[f512])).
% 57.59/22.76 fof(f2164,plain,(
% 57.59/22.76 ![X0,X1,X2,X3,X4,X5]: (hAPP(hAPP(hAPP(c_COMBS(X0,X1,X2),X3),X4),X5)=hAPP(hAPP(X3,X5),hAPP(X4,X5)))),
% 57.59/22.76 inference(cnf_transformation,[status(thm)],[f515])).
% 57.59/22.76 fof(f2266,plain,(
% 57.59/22.76 ![X0,X1]: (X0=hAPP(hAPP(c_List_Oappend(X1),c_List_Olist_ONil(X1)),X0))),
% 57.59/22.76 inference(destructive_equality_resolution,[status(thm)],[f889])).
% 57.59/22.76 fof(f2310,plain,(
% 57.59/22.76 hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____))),
% 57.59/22.76 inference(resolution,[status(thm)],[f535,f591])).
% 57.59/22.76 fof(f2312,plain,(
% 57.59/22.76 ![X0]: (hBOOL(hAPP(hAPP(c_member(X0),v_P____),c_Arrow__Order__Mirabelle_OProf)))),
% 57.59/22.76 inference(resolution,[status(thm)],[f2310,f592])).
% 57.59/22.76 fof(f2666,plain,(
% 57.59/22.76 ![X0,X1,X2,X3,X4]: (hAPP(c_FuncSet_Orestrict(X0,X1,X2,X3),X4)=hAPP(X2,X4)|~hBOOL(hAPP(X3,X4)))),
% 57.59/22.76 inference(resolution,[status(thm)],[f1603,f592])).
% 57.59/22.76 fof(f2823,plain,(
% 57.59/22.76 ![X0,X1,X2,X3,X4,X5]: (~hAPP(hAPP(hAPP(c_COMBS(X0,X1,X2),c_List_Olist_OCons(X3)),X4),X5)=hAPP(X4,X5))),
% 57.59/22.76 inference(paramodulation,[status(thm)],[f2164,f658])).
% 57.59/22.76 fof(f2836,plain,(
% 57.59/22.76 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~hAPP(hAPP(hAPP(c_COMBS(X0,X1,X2),hAPP(c_COMBS(X3,X4,X5),c_List_Olist_OCons(X6))),X7),X8)=hAPP(X8,hAPP(X7,X8)))),
% 57.59/22.76 inference(paramodulation,[status(thm)],[f2164,f2823])).
% 57.59/22.76 fof(f3986,plain,(
% 57.59/22.76 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_member(X0),hAPP(X1,v_P____)),c_Set_Oimage(X2,X0,X1,c_Arrow__Order__Mirabelle_OProf))))),
% 57.59/22.76 inference(resolution,[status(thm)],[f1415,f2312])).
% 57.59/22.76 fof(f4003,plain,(
% 57.59/22.76 ![X0,X1,X2]: (hBOOL(hAPP(c_Set_Oimage(X0,X1,X2,c_Arrow__Order__Mirabelle_OProf),hAPP(X2,v_P____))))),
% 57.59/22.76 inference(resolution,[status(thm)],[f3986,f591])).
% 57.59/22.76 fof(f4982,plain,(
% 57.59/22.76 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~hAPP(hAPP(hAPP(c_COMBS(X0,X1,X2),hAPP(c_COMBS(X3,X4,X5),c_List_Olist_OCons(X6))),hAPP(c_List_Oappend(X7),c_List_Olist_ONil(X7))),X8)=hAPP(X8,X8))),
% 57.59/22.76 inference(paramodulation,[status(thm)],[f2266,f2836])).
% 42.08/22.82 fof(f5047,plain,(
% 42.08/22.82 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_member(tc_prod(X0,X0)),X1),X2))|hBOOL(hAPP(c_Transitive__Closure_Ortrancl(X0,X2),X1)))),
% 42.08/22.82 inference(resolution,[status(thm)],[f1086,f591])).
% 42.08/22.82 fof(f5084,plain,(
% 42.08/22.82 ![X0,X1,X2]: (hBOOL(hAPP(c_Transitive__Closure_Ortrancl(X0,X1),X2))|~hBOOL(hAPP(X1,X2)))),
% 42.08/22.82 inference(resolution,[status(thm)],[f5047,f592])).
% 42.08/22.82 fof(f5099,plain,(
% 42.08/22.82 ![X0,X1,X2,X3,X4,X5]: (~hBOOL(hAPP(X0,X1))|hAPP(c_FuncSet_Orestrict(X2,X3,X4,c_Transitive__Closure_Ortrancl(X5,X0)),X1)=hAPP(X4,X1))),
% 42.08/22.82 inference(resolution,[status(thm)],[f5084,f2666])).
% 42.08/22.82 fof(f5525,plain,(
% 42.08/22.82 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~hBOOL(X0)|hAPP(c_FuncSet_Orestrict(X1,X2,X3,c_Transitive__Closure_Ortrancl(X4,c_COMBK(X5,X6,X0))),X7)=hAPP(X3,X7))),
% 42.08/22.82 inference(paramodulation,[status(thm)],[f2161,f5099])).
% 42.08/22.82 fof(f5635,plain,(
% 42.08/22.82 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (hAPP(c_FuncSet_Orestrict(X0,X1,X2,c_Transitive__Closure_Ortrancl(X3,c_COMBK(X4,X5,hAPP(c_Set_Oimage(X6,X7,X8,c_Arrow__Order__Mirabelle_OProf),hAPP(X8,v_P____))))),X9)=hAPP(X2,X9))),
% 42.08/22.82 inference(resolution,[status(thm)],[f5525,f4003])).
% 42.08/22.82 fof(f18780,plain,(
% 42.08/22.82 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (hAPP(c_FuncSet_Orestrict(X0,X1,X2,c_Transitive__Closure_Ortrancl(X3,c_COMBK(X4,X5,hAPP(c_Set_Oimage(X6,X7,c_COMBI(X8),c_Arrow__Order__Mirabelle_OProf),v_P____)))),X9)=hAPP(X2,X9))),
% 42.08/22.82 inference(paramodulation,[status(thm)],[f2160,f5635])).
% 42.08/22.82 fof(f34389,plain,(
% 42.08/22.82 $false),
% 42.08/22.82 inference(resolution,[status(thm)],[f4982,f18780])).
% 42.08/22.82 % SZS output end CNFRefutation for theBenchmark.p
% 42.08/22.87 % Elapsed time: 7.484382 seconds
% 42.08/22.87 % CPU time: 58.689825 seconds
% 42.08/22.87 % Total memory used: 922.201 MB
% 42.08/22.87 % Net memory used: 858.129 MB
%------------------------------------------------------------------------------