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