%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT126+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:21 PM UTC 2026
% Result : Theorem 224.54s 29.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT126+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n018.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 04:34:58 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.28/0.64 % Drodi V4.1.1
% 224.54/29.09 % Refutation found
% 224.54/29.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 224.54/29.09 % SZS output start CNFRefutation for theBenchmark
% 224.54/29.09 fof(f4,axiom,(
% 224.54/29.09 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_Q____),c_Arrow__Order__Mirabelle_OProf)) ),
% 224.54/29.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 224.54/29.09 fof(f24,axiom,(
% 224.54/29.09 hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin)))) ),
% 224.54/29.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 224.54/29.09 fof(f39,axiom,(
% 224.54/29.09 (! [V_x_2,V_B_2,V_A_2,V_f_2,T_b,T_a] :( hBOOL(hAPP(hAPP(c_member(tc_fun(T_a,T_b)),V_f_2),c_FuncSet_OPi(T_a,T_b,V_A_2,c_COMBK(tc_fun(T_b,tc_HOL_Obool),T_a,V_B_2))))=> ( 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)),V_B_2)) ) ) )),
% 224.54/29.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 224.54/29.09 fof(f525,conjecture,(
% 224.54/29.09 hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(v_F,v_Q____)),c_Arrow__Order__Mirabelle_OLin)) ),
% 224.54/29.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 224.54/29.09 fof(f526,negated_conjecture,(
% 224.54/29.09 ~(hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(v_F,v_Q____)),c_Arrow__Order__Mirabelle_OLin)) )),
% 224.54/29.09 inference(negated_conjecture,[status(cth)],[f525])).
% 224.54/29.09 fof(f532,plain,(
% 224.54/29.09 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_Q____),c_Arrow__Order__Mirabelle_OProf))),
% 224.54/29.09 inference(cnf_transformation,[status(thm)],[f4])).
% 224.54/29.09 fof(f625,plain,(
% 224.54/29.09 hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin))))),
% 224.54/29.09 inference(cnf_transformation,[status(thm)],[f24])).
% 224.54/29.09 fof(f688,plain,(
% 224.54/29.09 ![V_x_2,V_B_2,V_A_2,V_f_2,T_b,T_a]: (~hBOOL(hAPP(hAPP(c_member(tc_fun(T_a,T_b)),V_f_2),c_FuncSet_OPi(T_a,T_b,V_A_2,c_COMBK(tc_fun(T_b,tc_HOL_Obool),T_a,V_B_2))))|(~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)),V_B_2))))),
% 224.54/29.09 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 224.54/29.09 fof(f689,plain,(
% 224.54/29.09 ![V_B_2,V_A_2,V_f_2,T_b,T_a]: (~hBOOL(hAPP(hAPP(c_member(tc_fun(T_a,T_b)),V_f_2),c_FuncSet_OPi(T_a,T_b,V_A_2,c_COMBK(tc_fun(T_b,tc_HOL_Obool),T_a,V_B_2))))|(![V_x_2]: (~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)),V_B_2)))))),
% 224.54/29.09 inference(miniscoping,[status(thm)],[f688])).
% 224.54/29.09 fof(f690,plain,(
% 225.35/29.14 ![X0,X1,X2,X3,X4,X5]: (~hBOOL(hAPP(hAPP(c_member(tc_fun(X0,X1)),X2),c_FuncSet_OPi(X0,X1,X3,c_COMBK(tc_fun(X1,tc_HOL_Obool),X0,X4))))|~hBOOL(hAPP(hAPP(c_member(X0),X5),X3))|hBOOL(hAPP(hAPP(c_member(X1),hAPP(X2,X5)),X4)))),
% 225.35/29.14 inference(cnf_transformation,[status(thm)],[f689])).
% 225.35/29.14 fof(f2123,plain,(
% 225.35/29.14 ~hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(v_F,v_Q____)),c_Arrow__Order__Mirabelle_OLin))),
% 225.35/29.14 inference(cnf_transformation,[status(thm)],[f526])).
% 225.35/29.14 fof(f18424,plain,(
% 225.35/29.14 ![X0,X1]: (~hBOOL(hAPP(hAPP(c_member(tc_fun(X0,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(X0,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),X1,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),X0,c_Arrow__Order__Mirabelle_OLin))))|~hBOOL(hAPP(hAPP(c_member(X0),v_Q____),X1)))),
% 225.35/29.14 inference(resolution,[status(thm)],[f2123,f690])).
% 225.35/29.14 fof(f24019,plain,(
% 225.35/29.14 ~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_Q____),c_Arrow__Order__Mirabelle_OProf))),
% 225.35/29.14 inference(resolution,[status(thm)],[f18424,f625])).
% 225.35/29.14 fof(f24044,plain,(
% 225.35/29.14 $false),
% 225.35/29.14 inference(forward_subsumption_resolution,[status(thm)],[f24019,f532])).
% 225.35/29.14 % SZS output end CNFRefutation for theBenchmark.p
% 57.46/29.24 % Elapsed time: 28.770514 seconds
% 57.46/29.24 % CPU time: 225.991238 seconds
% 57.46/29.24 % Total memory used: 1.055 GB
% 57.46/29.24 % Net memory used: 955.408 MB
%------------------------------------------------------------------------------