%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL753-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 : n017.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 01:11:02 PM UTC 2026
% Result : Unsatisfiable 41.60s 5.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL753-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 00:57:14 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.43 % Drodi V4.1.1
% 41.60/5.74 % Refutation found
% 41.60/5.74 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 41.60/5.74 % SZS output start CNFRefutation for theBenchmark
% 41.60/5.74 fof(f18,axiom,(
% 41.60/5.74 (![V_n,V_t,V_k]: (c_Lambda_Oliftn(c_Suc(V_n),V_t,V_k) = c_Lambda_Olift(c_Lambda_Oliftn(V_n,V_t,V_k),V_k) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f28,axiom,(
% 41.60/5.74 c_HOL_Oone__class_Oone(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f149,axiom,(
% 41.60/5.74 (![V_n]: (c_Suc(V_n) = c_HOL_Oplus__class_Oplus(V_n,c_HOL_Oone__class_Oone(tc_nat),tc_nat) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f162,axiom,(
% 41.60/5.74 (![V_t,V_s,V_n]: (c_Lambda_Osubstn(V_t,V_s,V_n) = c_Lambda_Osubst(V_t,c_Lambda_Oliftn(V_n,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_n) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f194,axiom,(
% 41.60/5.74 (![V_n,V_i,V_k]: (( c_Lambda_Oliftn(V_n,c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(V_i,V_n,tc_nat))| c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f204,axiom,(
% 41.60/5.74 (![V_n,V_s,V_k]: (c_Lambda_Oliftn(V_n,c_Lambda_OdB_OAbs(V_s),V_k) = c_Lambda_OdB_OAbs(c_Lambda_Oliftn(V_n,V_s,c_HOL_Oplus__class_Oplus(V_k,c_HOL_Oone__class_Oone(tc_nat),tc_nat))) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f258,axiom,(
% 41.60/5.74 (![V_n]: (( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat)| V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f259,axiom,(
% 41.60/5.74 (![V_t,V_k]: (c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),V_t,V_k) = V_t ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f393,axiom,(
% 41.60/5.74 (![V_n]: (c_Suc(V_n) != V_n ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f437,axiom,(
% 41.60/5.74 (![V_n]: (( c_Suc(c_HOL_Ominus__class_Ominus(V_n,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)) = V_n| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f595,axiom,(
% 41.60/5.74 (![V_t,V_s,V_k]: (c_Lambda_Osubst(c_Lambda_OdB_OAbs(V_t),V_s,V_k) = c_Lambda_OdB_OAbs(c_Lambda_Osubst(V_t,c_Lambda_Olift(V_s,c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(V_k,c_HOL_Oone__class_Oone(tc_nat),tc_nat))) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f662,axiom,(
% 41.60/5.74 (![V_dB_H,V_nat]: (c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f664,axiom,(
% 41.60/5.74 (![V_nat,V_nat_H]: (( c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OVar(V_nat_H)| V_nat = V_nat_H ) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f666,axiom,(
% 41.60/5.74 (![V_k,V_u]: (c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f667,axiom,(
% 41.60/5.74 (![V_j,V_u,V_i]: (( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_j),V_u,V_i) = c_Lambda_OdB_OVar(V_j)| ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f668,axiom,(
% 41.60/5.74 (![V_i,V_s,V_k]: (( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(c_HOL_Ominus__class_Ominus(V_i,c_HOL_Oone__class_Oone(tc_nat),tc_nat))| ~ c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f678,axiom,(
% 41.60/5.74 (![V_r]: (( c_InductTermi_OIT(c_Lambda_OdB_OAbs(V_r))| ~ c_InductTermi_OIT(V_r) ) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f683,negated_conjecture,(
% 41.60/5.74 (![V_i,V_j]: (c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_OdB_OVar(V_i),V_j)) ))),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f684,negated_conjecture,(
% 41.60/5.74 ~ c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(v_ra),c_Lambda_OdB_OVar(v_ia),v_ja)) ),
% 41.60/5.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.60/5.74 fof(f747,plain,(
% 41.60/5.74 ![X0,X1,X2]: (c_Lambda_Oliftn(c_Suc(X0),X1,X2)=c_Lambda_Olift(c_Lambda_Oliftn(X0,X1,X2),X2))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f18])).
% 41.60/5.74 fof(f762,plain,(
% 41.60/5.74 c_HOL_Oone__class_Oone(tc_nat)=c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f28])).
% 41.60/5.74 fof(f950,plain,(
% 41.60/5.74 ![X0]: (c_Suc(X0)=c_HOL_Oplus__class_Oplus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f149])).
% 41.60/5.74 fof(f968,plain,(
% 41.60/5.74 ![X0,X1,X2]: (c_Lambda_Osubstn(X0,X1,X2)=c_Lambda_Osubst(X0,c_Lambda_Oliftn(X2,X1,c_HOL_Ozero__class_Ozero(tc_nat)),X2))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f162])).
% 41.60/5.74 fof(f1014,plain,(
% 41.60/5.74 ![V_i,V_k]: ((![V_n]: c_Lambda_Oliftn(V_n,c_Lambda_OdB_OVar(V_i),V_k)=c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(V_i,V_n,tc_nat)))|c_HOL_Oord__class_Oless(V_i,V_k,tc_nat))),
% 41.60/5.74 inference(miniscoping,[status(thm)],[f194])).
% 41.60/5.74 fof(f1015,plain,(
% 41.60/5.74 ![X0,X1,X2]: (c_Lambda_Oliftn(X0,c_Lambda_OdB_OVar(X1),X2)=c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X1,X0,tc_nat))|c_HOL_Oord__class_Oless(X1,X2,tc_nat))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f1014])).
% 41.60/5.74 fof(f1027,plain,(
% 41.60/5.74 ![X0,X1,X2]: (c_Lambda_Oliftn(X0,c_Lambda_OdB_OAbs(X1),X2)=c_Lambda_OdB_OAbs(c_Lambda_Oliftn(X0,X1,c_HOL_Oplus__class_Oplus(X2,c_HOL_Oone__class_Oone(tc_nat),tc_nat))))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f204])).
% 41.60/5.74 fof(f1108,plain,(
% 41.60/5.74 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|X0=c_HOL_Ozero__class_Ozero(tc_nat))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f258])).
% 41.60/5.74 fof(f1109,plain,(
% 41.60/5.74 ![X0,X1]: (c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),X0,X1)=X0)),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f259])).
% 41.60/5.74 fof(f1325,plain,(
% 41.60/5.74 ![X0]: (~c_Suc(X0)=X0)),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f393])).
% 41.60/5.74 fof(f1396,plain,(
% 41.60/5.74 ![X0]: (c_Suc(c_HOL_Ominus__class_Ominus(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat))=X0|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f437])).
% 41.60/5.74 fof(f1660,plain,(
% 41.60/5.74 ![X0,X1,X2]: (c_Lambda_Osubst(c_Lambda_OdB_OAbs(X0),X1,X2)=c_Lambda_OdB_OAbs(c_Lambda_Osubst(X0,c_Lambda_Olift(X1,c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(X2,c_HOL_Oone__class_Oone(tc_nat),tc_nat))))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f595])).
% 41.60/5.74 fof(f1757,plain,(
% 41.60/5.74 ![X0,X1]: (~c_Lambda_OdB_OAbs(X0)=c_Lambda_OdB_OVar(X1))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f662])).
% 41.60/5.74 fof(f1759,plain,(
% 41.60/5.74 ![X0,X1]: (~c_Lambda_OdB_OVar(X0)=c_Lambda_OdB_OVar(X1)|X0=X1)),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f664])).
% 41.60/5.74 fof(f1761,plain,(
% 41.60/5.74 ![X0,X1]: (c_Lambda_Osubst(c_Lambda_OdB_OVar(X0),X1,X0)=X1)),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f666])).
% 41.60/5.74 fof(f1762,plain,(
% 41.60/5.74 ![V_j,V_i]: ((![V_u]: c_Lambda_Osubst(c_Lambda_OdB_OVar(V_j),V_u,V_i)=c_Lambda_OdB_OVar(V_j))|~c_HOL_Oord__class_Oless(V_j,V_i,tc_nat))),
% 41.60/5.74 inference(miniscoping,[status(thm)],[f667])).
% 41.60/5.74 fof(f1763,plain,(
% 41.60/5.74 ![X0,X1,X2]: (c_Lambda_Osubst(c_Lambda_OdB_OVar(X0),X1,X2)=c_Lambda_OdB_OVar(X0)|~c_HOL_Oord__class_Oless(X0,X2,tc_nat))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f1762])).
% 41.60/5.74 fof(f1764,plain,(
% 41.60/5.74 ![V_i,V_k]: ((![V_s]: c_Lambda_Osubst(c_Lambda_OdB_OVar(V_i),V_s,V_k)=c_Lambda_OdB_OVar(c_HOL_Ominus__class_Ominus(V_i,c_HOL_Oone__class_Oone(tc_nat),tc_nat)))|~c_HOL_Oord__class_Oless(V_k,V_i,tc_nat))),
% 41.60/5.74 inference(miniscoping,[status(thm)],[f668])).
% 41.60/5.74 fof(f1765,plain,(
% 41.60/5.74 ![X0,X1,X2]: (c_Lambda_Osubst(c_Lambda_OdB_OVar(X0),X1,X2)=c_Lambda_OdB_OVar(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat))|~c_HOL_Oord__class_Oless(X2,X0,tc_nat))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f1764])).
% 41.60/5.74 fof(f1780,plain,(
% 41.60/5.74 ![X0]: (c_InductTermi_OIT(c_Lambda_OdB_OAbs(X0))|~c_InductTermi_OIT(X0))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f678])).
% 41.60/5.74 fof(f1785,plain,(
% 41.60/5.74 ![X0,X1]: (c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_OdB_OVar(X0),X1)))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f683])).
% 41.60/5.74 fof(f1786,plain,(
% 41.60/5.74 ~c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(v_ra),c_Lambda_OdB_OVar(v_ia),v_ja))),
% 41.60/5.74 inference(cnf_transformation,[status(thm)],[f684])).
% 41.60/5.74 fof(f1828,plain,(
% 41.60/5.74 ![X0,X1,X2]: (c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(X0),X1,X2))|~c_InductTermi_OIT(c_Lambda_Osubst(X0,c_Lambda_Olift(X1,c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(X2,c_HOL_Oone__class_Oone(tc_nat),tc_nat))))),
% 41.60/5.74 inference(paramodulation,[status(thm)],[f1660,f1780])).
% 41.60/5.74 fof(f2244,plain,(
% 41.60/5.74 ![X0,X1]: (c_Lambda_Oliftn(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,X1)=c_Lambda_Olift(X0,X1))),
% 41.60/5.74 inference(paramodulation,[status(thm)],[f1109,f747])).
% 41.60/5.74 fof(f3762,plain,(
% 41.60/5.74 ![X0,X1,X2]: (c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(X0),X1,X2))|~c_InductTermi_OIT(c_Lambda_Osubst(X0,c_Lambda_Olift(X1,c_HOL_Ozero__class_Ozero(tc_nat)),c_Suc(X2))))),
% 41.60/5.74 inference(backward_demodulation,[status(thm)],[f950,f1828])).
% 41.60/5.74 fof(f11774,plain,(
% 41.60/5.74 ![X0,X1]: (c_Lambda_Oliftn(c_HOL_Oone__class_Oone(tc_nat),X0,X1)=c_Lambda_Olift(X0,X1))),
% 41.60/5.74 inference(forward_demodulation,[status(thm)],[f762,f2244])).
% 41.60/5.74 fof(f13146,plain,(
% 41.60/5.74 ![X0,X1]: (c_Lambda_Osubstn(c_Lambda_OdB_OVar(X0),X1,X0)=c_Lambda_Oliftn(X0,X1,c_HOL_Ozero__class_Ozero(tc_nat)))),
% 41.60/5.74 inference(paramodulation,[status(thm)],[f1761,f968])).
% 41.60/5.74 fof(f16575,plain,(
% 41.60/5.74 ![X0,X1,X2,X3]: (c_Lambda_Oliftn(X0,c_Lambda_OdB_OVar(X1),X2)=c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X1,X0,tc_nat))|c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X3,X2)=c_Lambda_OdB_OVar(X1))),
% 41.60/5.74 inference(resolution,[status(thm)],[f1015,f1763])).
% 41.60/5.74 fof(f17468,plain,(
% 41.60/5.74 ![X0,X1,X2,X3]: (~c_Lambda_Oliftn(X0,c_Lambda_OdB_OAbs(X1),X2)=c_Lambda_OdB_OVar(X3))),
% 41.60/5.74 inference(paramodulation,[status(thm)],[f1027,f1757])).
% 41.60/5.74 fof(f17500,plain,(
% 41.60/5.74 ![X0,X1,X2,X3,X4,X5]: (~c_Lambda_Oliftn(X0,c_Lambda_Oliftn(X1,c_Lambda_OdB_OAbs(X2),X3),X4)=c_Lambda_OdB_OVar(X5))),
% 41.60/5.74 inference(paramodulation,[status(thm)],[f1027,f17468])).
% 41.60/5.74 fof(f17671,plain,(
% 41.60/5.74 ![X0,X1,X2,X3,X4]: (~c_Lambda_Oliftn(X0,c_Lambda_Osubstn(c_Lambda_OdB_OVar(X1),c_Lambda_OdB_OAbs(X2),X1),X3)=c_Lambda_OdB_OVar(X4))),
% 41.60/5.74 inference(paramodulation,[status(thm)],[f13146,f17500])).
% 41.60/5.74 fof(f21661,plain,(
% 41.60/5.74 ![X0,X1,X2,X3,X4]: (c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_Oliftn(X0,c_Lambda_OdB_OVar(X1),X2),X3))|c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X4,X2)=c_Lambda_OdB_OVar(X1))),
% 41.60/5.74 inference(paramodulation,[status(thm)],[f16575,f1785])).
% 41.60/5.74 fof(f21900,plain,(
% 41.60/5.74 ![X0,X1,X2,X3]: (c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_Olift(c_Lambda_OdB_OVar(X0),X1),X2))|c_Lambda_Osubst(c_Lambda_OdB_OVar(X0),X3,X1)=c_Lambda_OdB_OVar(X0))),
% 41.60/5.74 inference(paramodulation,[status(thm)],[f11774,f21661])).
% 41.60/5.74 fof(f21911,plain,(
% 41.60/5.74 ![X0,X1,X2]: (c_Lambda_Osubst(c_Lambda_OdB_OVar(X0),X1,c_HOL_Ozero__class_Ozero(tc_nat))=c_Lambda_OdB_OVar(X0)|c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(v_ra),c_Lambda_OdB_OVar(X0),X2)))),
% 41.60/5.74 inference(resolution,[status(thm)],[f21900,f3762])).
% 41.60/5.74 fof(f21983,plain,(
% 41.60/5.74 ![X0]: (c_Lambda_Osubst(c_Lambda_OdB_OVar(v_ia),X0,c_HOL_Ozero__class_Ozero(tc_nat))=c_Lambda_OdB_OVar(v_ia))),
% 41.60/5.74 inference(resolution,[status(thm)],[f21911,f1786])).
% 41.60/5.74 fof(f22006,definition,(
% 41.60/5.74 sQ399_spl <=> (v_ia=c_HOL_Ozero__class_Ozero(tc_nat))),
% 41.60/5.74 introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition])).
% 41.60/5.74 fof(f22007,plain,(
% 41.60/5.74 v_ia=c_HOL_Ozero__class_Ozero(tc_nat)|~sQ399_spl),
% 41.60/5.74 inference(component_clause,[status(thm)],[f22006])).
% 41.60/5.74 fof(f22041,plain,(
% 41.60/5.74 ![X0]: (c_Lambda_Osubst(c_Lambda_OdB_OVar(v_ia),X0,v_ia)=c_Lambda_OdB_OVar(v_ia)|~sQ399_spl)),
% 41.60/5.74 inference(backward_demodulation,[status(thm)],[f22007,f21983])).
% 41.60/5.74 fof(f22122,plain,(
% 41.60/5.74 ![X0]: (X0=c_Lambda_OdB_OVar(v_ia)|~sQ399_spl)),
% 41.60/5.74 inference(forward_demodulation,[status(thm)],[f1761,f22041])).
% 41.60/5.74 fof(f24349,definition,(
% 41.60/5.74 sQ428_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),v_ia,tc_nat))),
% 41.60/5.74 introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition])).
% 41.60/5.74 fof(f24350,plain,(
% 41.60/5.74 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),v_ia,tc_nat)|~sQ428_spl),
% 41.60/5.74 inference(component_clause,[status(thm)],[f24349])).
% 41.60/5.74 fof(f24351,plain,(
% 41.60/5.74 ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),v_ia,tc_nat)|sQ428_spl),
% 41.60/5.74 inference(component_clause,[status(thm)],[f24349])).
% 41.60/5.81 fof(f25527,plain,(
% 41.60/5.81 ![X0]: (c_Lambda_Osubst(c_Lambda_OdB_OVar(v_ia),X0,c_HOL_Ozero__class_Ozero(tc_nat))=c_Lambda_OdB_OVar(c_HOL_Ominus__class_Ominus(v_ia,c_HOL_Oone__class_Oone(tc_nat),tc_nat))|~sQ428_spl)),
% 41.60/5.81 inference(resolution,[status(thm)],[f24350,f1765])).
% 41.60/5.81 fof(f33256,plain,(
% 41.60/5.81 v_ia=c_HOL_Ozero__class_Ozero(tc_nat)|sQ428_spl),
% 41.60/5.81 inference(resolution,[status(thm)],[f24351,f1108])).
% 41.60/5.81 fof(f33271,plain,(
% 41.60/5.81 sQ399_spl|sQ428_spl),
% 41.60/5.81 inference(split_clause,[status(thm)],[f33256,f22006,f24349])).
% 41.60/5.81 fof(f33292,plain,(
% 41.60/5.81 c_Lambda_OdB_OVar(v_ia)=c_Lambda_OdB_OVar(c_HOL_Ominus__class_Ominus(v_ia,c_HOL_Oone__class_Oone(tc_nat),tc_nat))|~sQ428_spl),
% 41.60/5.81 inference(forward_demodulation,[status(thm)],[f21983,f25527])).
% 41.60/5.81 fof(f33941,plain,(
% 41.60/5.81 ![X0]: (c_Suc(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat))=X0|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat))),
% 41.60/5.81 inference(forward_demodulation,[status(thm)],[f762,f1396])).
% 41.60/5.81 fof(f33942,plain,(
% 41.60/5.81 c_Suc(c_HOL_Ominus__class_Ominus(v_ia,c_HOL_Oone__class_Oone(tc_nat),tc_nat))=v_ia|~sQ428_spl),
% 41.60/5.81 inference(resolution,[status(thm)],[f33941,f24350])).
% 41.60/5.81 fof(f34924,plain,(
% 41.60/5.81 $false|~sQ399_spl),
% 41.60/5.81 inference(resolution,[status(thm)],[f22122,f17671])).
% 41.60/5.81 fof(f35104,plain,(
% 41.60/5.81 ~sQ399_spl),
% 41.60/5.81 inference(contradiction_clause,[status(thm)],[f34924])).
% 41.60/5.81 fof(f37581,plain,(
% 41.60/5.81 ~v_ia=c_HOL_Ominus__class_Ominus(v_ia,c_HOL_Oone__class_Oone(tc_nat),tc_nat)|~sQ428_spl),
% 41.60/5.81 inference(paramodulation,[status(thm)],[f33942,f1325])).
% 41.60/5.81 fof(f38140,plain,(
% 41.60/5.81 v_ia=c_HOL_Ominus__class_Ominus(v_ia,c_HOL_Oone__class_Oone(tc_nat),tc_nat)|~sQ428_spl),
% 41.60/5.81 inference(resolution,[status(thm)],[f33292,f1759])).
% 41.60/5.81 fof(f38205,plain,(
% 41.60/5.81 $false|~sQ428_spl),
% 41.60/5.81 inference(forward_subsumption_resolution,[status(thm)],[f38140,f37581])).
% 41.60/5.81 fof(f38206,plain,(
% 41.60/5.81 ~sQ428_spl),
% 41.60/5.81 inference(contradiction_clause,[status(thm)],[f38205])).
% 41.60/5.81 fof(f38207,plain,(
% 41.60/5.81 $false),
% 41.60/5.81 inference(sat_refutation,[status(thm)],[f33271,f35104,f38206])).
% 41.60/5.81 % SZS output end CNFRefutation for theBenchmark.p
% 6.13/5.82 % Elapsed time: 5.430904 seconds
% 6.13/5.82 % CPU time: 42.445675 seconds
% 6.13/5.82 % Total memory used: 549.113 MB
% 6.13/5.82 % Net memory used: 526.654 MB
%------------------------------------------------------------------------------