%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV584-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 : n026.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:52:52 PM UTC 2026
% Result : Unsatisfiable 146.07s 19.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV584-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n026.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 21 09:14:37 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.25/0.53 % Drodi V4.1.1
% 146.07/19.10 % Refutation found
% 146.07/19.10 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 146.07/19.10 % SZS output start CNFRefutation for theBenchmark
% 146.07/19.10 fof(f311,axiom,(
% 146.07/19.10 (![V_m,V_n]: (( hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_m),V_n))| ~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,V_m),tc_nat),V_n)) ) ))),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f320,axiom,(
% 146.07/19.10 (![T_a,V_x]: (( ~ class_Orderings_Obot(T_a)| hBOOL(hAPP(c_lessequals(c_Orderings_Obot__class_Obot(T_a),T_a),V_x)) ) ))),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f944,axiom,(
% 146.07/19.10 (![V_x,V_a]: (( V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_a)| V_a = c_HOL_Ozero__class_Ozero(tc_nat) ) ))),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f1032,axiom,(
% 146.07/19.10 (![V_n]: (( V_n = c_HOL_Ozero__class_Ozero(tc_nat)| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)))) ) ))),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f1040,axiom,(
% 146.07/19.10 c_HOL_Oone__class_Oone(tc_nat) = hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)) ),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f1078,axiom,(
% 146.07/19.10 (![V_m,V_n]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),hAPP(c_Suc,V_n)) = hAPP(c_Suc,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n)) ))),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f1097,axiom,(
% 146.07/19.10 (![V_n,V_m]: (( hBOOL(hAPP(c_lessequals(hAPP(c_Suc,V_n),tc_nat),V_m))| hBOOL(hAPP(c_lessequals(V_m,tc_nat),V_n)) ) ))),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f1098,axiom,(
% 146.07/19.10 (![V_m,V_n]: (( ~ hBOOL(hAPP(c_lessequals(V_m,tc_nat),V_n))| ~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,V_n),tc_nat),V_m)) ) ))),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f1465,axiom,(
% 146.07/19.10 (![V_nat_H]: (hAPP(c_Suc,V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat) ))),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f1490,axiom,(
% 146.07/19.10 (![T_a,V_P]: (hAPP(c_Collect(T_a),V_P) = V_P ))),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f1539,axiom,(
% 146.07/19.10 (![T_b,T_a,T_c,V_P,V_Q,V_R]: (hAPP(hAPP(hAPP(c_COMBB(T_b,T_a,T_c),V_P),V_Q),V_R) = hAPP(V_P,hAPP(V_Q,V_R)) ))),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f1541,axiom,(
% 146.07/19.10 (![V_P,T_b,T_c,T_a,V_Q,V_R]: (hAPP(hAPP(c_COMBS(V_P,T_b,T_c,T_a),V_Q),V_R) = hAPP(hAPP(V_P,V_R),hAPP(V_Q,V_R)) ))),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f1610,axiom,(
% 146.07/19.10 class_Orderings_Obot(tc_nat) ),
% 146.07/19.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 146.07/19.10 fof(f2220,plain,(
% 146.07/19.10 ![X0,X1]: (hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X0),X1))|~hBOOL(hAPP(c_lessequals(hAPP(c_Suc,X0),tc_nat),X1)))),
% 146.07/19.10 inference(cnf_transformation,[status(thm)],[f311])).
% 146.07/19.10 fof(f2231,plain,(
% 146.07/19.10 ![T_a]: (~class_Orderings_Obot(T_a)|(![V_x]: hBOOL(hAPP(c_lessequals(c_Orderings_Obot__class_Obot(T_a),T_a),V_x))))),
% 146.07/19.10 inference(miniscoping,[status(thm)],[f320])).
% 146.07/19.10 fof(f2232,plain,(
% 146.07/19.10 ![X0,X1]: (~class_Orderings_Obot(X0)|hBOOL(hAPP(c_lessequals(c_Orderings_Obot__class_Obot(X0),X0),X1)))),
% 146.07/19.10 inference(cnf_transformation,[status(thm)],[f2231])).
% 146.07/19.10 fof(f3270,plain,(
% 146.07/19.10 ![V_a]: ((![V_x]: ~V_x=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_a))|V_a=c_HOL_Ozero__class_Ozero(tc_nat))),
% 146.07/19.10 inference(miniscoping,[status(thm)],[f944])).
% 146.07/19.10 fof(f3271,plain,(
% 146.07/19.10 ![X0,X1]: (~X0=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)|X1=c_HOL_Ozero__class_Ozero(tc_nat))),
% 146.07/19.10 inference(cnf_transformation,[status(thm)],[f3270])).
% 146.07/19.10 fof(f3424,plain,(
% 146.07/19.10 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_nat)|~hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X0),hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)))))),
% 146.07/19.10 inference(cnf_transformation,[status(thm)],[f1032])).
% 146.07/19.10 fof(f3436,plain,(
% 146.07/19.10 c_HOL_Oone__class_Oone(tc_nat)=hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat))),
% 146.07/19.10 inference(cnf_transformation,[status(thm)],[f1040])).
% 146.07/19.10 fof(f3479,plain,(
% 146.07/19.10 ![X0,X1]: (hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),hAPP(c_Suc,X1))=hAPP(c_Suc,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)))),
% 146.07/19.10 inference(cnf_transformation,[status(thm)],[f1078])).
% 66.23/19.27 fof(f3503,plain,(
% 66.23/19.27 ![X0,X1]: (hBOOL(hAPP(c_lessequals(hAPP(c_Suc,X0),tc_nat),X1))|hBOOL(hAPP(c_lessequals(X1,tc_nat),X0)))),
% 66.23/19.27 inference(cnf_transformation,[status(thm)],[f1097])).
% 66.23/19.27 fof(f3504,plain,(
% 66.23/19.27 ![X0,X1]: (~hBOOL(hAPP(c_lessequals(X0,tc_nat),X1))|~hBOOL(hAPP(c_lessequals(hAPP(c_Suc,X1),tc_nat),X0)))),
% 66.23/19.27 inference(cnf_transformation,[status(thm)],[f1098])).
% 66.23/19.27 fof(f4096,plain,(
% 66.23/19.27 ![X0]: (~hAPP(c_Suc,X0)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 66.23/19.27 inference(cnf_transformation,[status(thm)],[f1465])).
% 66.23/19.27 fof(f4135,plain,(
% 66.23/19.27 ![X0,X1]: (hAPP(c_Collect(X0),X1)=X1)),
% 66.23/19.27 inference(cnf_transformation,[status(thm)],[f1490])).
% 66.23/19.27 fof(f4214,plain,(
% 66.23/19.27 ![X0,X1,X2,X3,X4,X5]: (hAPP(hAPP(hAPP(c_COMBB(X0,X1,X2),X3),X4),X5)=hAPP(X3,hAPP(X4,X5)))),
% 66.23/19.27 inference(cnf_transformation,[status(thm)],[f1539])).
% 66.23/19.27 fof(f4216,plain,(
% 66.23/19.27 ![X0,X1,X2,X3,X4,X5]: (hAPP(hAPP(c_COMBS(X0,X1,X2,X3),X4),X5)=hAPP(hAPP(X0,X5),hAPP(X4,X5)))),
% 66.23/19.27 inference(cnf_transformation,[status(thm)],[f1541])).
% 66.23/19.27 fof(f4308,plain,(
% 66.23/19.27 class_Orderings_Obot(tc_nat)),
% 66.23/19.27 inference(cnf_transformation,[status(thm)],[f1610])).
% 66.23/19.27 fof(f4412,plain,(
% 66.23/19.27 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_nat)|~hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat))))),
% 66.23/19.27 inference(backward_demodulation,[status(thm)],[f3436,f3424])).
% 66.23/19.27 fof(f5059,plain,(
% 66.23/19.27 ![X0,X1,X2,X3,X4,X5]: (hAPP(hAPP(c_COMBS(X0,X1,X2,X3),c_Collect(X4)),X5)=hAPP(hAPP(X0,X5),X5))),
% 66.23/19.27 inference(paramodulation,[status(thm)],[f4135,f4216])).
% 66.23/19.27 fof(f6041,plain,(
% 66.23/19.27 ![X0,X1]: (hBOOL(hAPP(c_lessequals(X0,tc_nat),X1))|hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X1),X0)))),
% 66.23/19.27 inference(resolution,[status(thm)],[f3503,f2220])).
% 66.23/19.27 fof(f6068,plain,(
% 66.23/19.27 ![X0]: (hBOOL(hAPP(c_lessequals(c_HOL_Oone__class_Oone(tc_nat),tc_nat),X0))|X0=c_HOL_Ozero__class_Ozero(tc_nat))),
% 66.23/19.27 inference(resolution,[status(thm)],[f6041,f4412])).
% 66.23/19.27 fof(f11243,plain,(
% 66.23/19.27 ![X0]: (hBOOL(hAPP(c_lessequals(c_Orderings_Obot__class_Obot(tc_nat),tc_nat),X0)))),
% 66.23/19.27 inference(resolution,[status(thm)],[f2232,f4308])).
% 66.23/19.27 fof(f11251,plain,(
% 66.23/19.27 ![X0]: (~hBOOL(hAPP(c_lessequals(hAPP(c_Suc,X0),tc_nat),c_Orderings_Obot__class_Obot(tc_nat))))),
% 66.23/19.27 inference(resolution,[status(thm)],[f11243,f3504])).
% 66.23/19.27 fof(f11288,plain,(
% 66.23/19.27 ~hBOOL(hAPP(c_lessequals(c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Orderings_Obot__class_Obot(tc_nat)))),
% 66.23/19.27 inference(paramodulation,[status(thm)],[f3436,f11251])).
% 66.23/19.27 fof(f11294,plain,(
% 66.23/19.27 c_Orderings_Obot__class_Obot(tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat)),
% 66.23/19.27 inference(resolution,[status(thm)],[f11288,f6068])).
% 66.23/19.27 fof(f11344,plain,(
% 66.23/19.27 ![X0]: (~hAPP(c_Suc,X0)=c_Orderings_Obot__class_Obot(tc_nat))),
% 66.23/19.27 inference(backward_demodulation,[status(thm)],[f11294,f4096])).
% 66.23/19.27 fof(f11643,plain,(
% 66.23/19.27 ![X0,X1]: (~X0=hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)|X1=c_Orderings_Obot__class_Obot(tc_nat))),
% 66.23/19.27 inference(backward_demodulation,[status(thm)],[f11294,f3271])).
% 66.23/19.27 fof(f11783,plain,(
% 66.23/19.27 ![X0,X1]: (~X0=hAPP(c_Suc,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1))|hAPP(c_Suc,X1)=c_Orderings_Obot__class_Obot(tc_nat))),
% 66.23/19.27 inference(paramodulation,[status(thm)],[f3479,f11643])).
% 66.23/19.27 fof(f11791,plain,(
% 66.23/19.27 ![X0,X1]: (~X0=hAPP(c_Suc,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)))),
% 66.23/19.27 inference(forward_subsumption_resolution,[status(thm)],[f11783,f11344])).
% 66.23/19.27 fof(f11796,plain,(
% 66.23/19.27 ![X0,X1,X2,X3,X4]: (~X0=hAPP(c_Suc,hAPP(hAPP(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X1,X2,X3),X4),X0)))),
% 66.23/19.27 inference(paramodulation,[status(thm)],[f4216,f11791])).
% 66.23/19.27 fof(f11858,plain,(
% 66.23/19.27 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~hAPP(X0,X1)=hAPP(c_Suc,hAPP(hAPP(c_COMBS(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X2,X3,X4),X5,X6,X7),X0),X1)))),
% 66.23/19.27 inference(paramodulation,[status(thm)],[f4216,f11796])).
% 66.23/19.27 fof(f12358,plain,(
% 66.23/19.27 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~hAPP(X0,X0)=hAPP(c_Suc,hAPP(hAPP(c_COMBS(c_COMBS(c_COMBS(c_HOL_Oplus__class_Oplus(tc_nat),X1,X2,X3),X4,X5,X6),X7,X8,X9),c_Collect(X10)),X0)))),
% 66.23/19.27 inference(paramodulation,[status(thm)],[f5059,f11858])).
% 66.23/19.27 fof(f13395,plain,(
% 66.23/19.27 $false),
% 66.23/19.27 inference(resolution,[status(thm)],[f12358,f4214])).
% 66.23/19.27 % SZS output end CNFRefutation for theBenchmark.p
% 66.23/19.29 % Elapsed time: 18.887403 seconds
% 66.23/19.29 % CPU time: 148.461507 seconds
% 66.23/19.29 % Total memory used: 1.175 GB
% 66.23/19.29 % Net memory used: 1.122 GB
%------------------------------------------------------------------------------