%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV282-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:50:25 PM UTC 2026
% Result : Unsatisfiable 0.98s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV282-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 08:38:25 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 0.98/0.66 % Refutation found
% 0.98/0.66 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.98/0.66 % SZS output start CNFRefutation for theBenchmark
% 0.98/0.66 fof(f1,negated_conjecture,(
% 0.98/0.66 (![V_U,V_W,V_V]: (( V_U = V_W| V_V = V_W| V_U = V_V| c_in(c_Message_Omsg_ONonce(V_W),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)| c_in(c_Message_Omsg_ONonce(V_V),c_Event_Oused(v_evs_H),tc_Message_Omsg)| c_in(c_Message_Omsg_ONonce(V_U),c_Event_Oused(v_evs),tc_Message_Omsg) ) ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f2,axiom,(
% 0.98/0.66 (![V_y]: (c_Binomial_Obinomial(V_y,c_Suc(c_0)) = V_y ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f3,axiom,(
% 0.98/0.66 (![V_n,V_k]: (c_Binomial_Obinomial(c_Suc(V_n),c_Suc(V_k)) = c_plus(c_Binomial_Obinomial(V_n,V_k),c_Binomial_Obinomial(V_n,c_Suc(V_k)),tc_nat) ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f4,axiom,(
% 0.98/0.66 (![V_n]: (c_Binomial_Obinomial(V_n,c_0) = c_1 ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f5,axiom,(
% 0.98/0.66 c_1 = c_Suc(c_0) ),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f6,axiom,(
% 0.98/0.66 (![V_m,V_n]: (( c_minus(V_m,V_n,tc_nat) != c_0| c_lessequals(V_m,V_n,tc_nat) ) ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f7,axiom,(
% 0.98/0.66 (![V_m]: (c_minus(V_m,V_m,tc_nat) = c_0 ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f8,axiom,(
% 0.98/0.66 (![V_n,V_m]: (c_lessequals(V_n,c_plus(V_n,V_m,tc_nat),tc_nat) ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f9,axiom,(
% 0.98/0.66 (![V_n]: (c_less(V_n,c_Suc(V_n),tc_nat) ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f10,axiom,(
% 0.98/0.66 (![V_m,V_n]: (( ~ c_lessequals(V_m,V_n,tc_nat)| c_less(V_m,c_Suc(V_n),tc_nat) ) ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f11,axiom,(
% 0.98/0.66 (![V_k,V_m,V_n]: (( ~ c_lessequals(c_plus(V_k,V_m,tc_nat),c_plus(V_k,V_n,tc_nat),tc_nat)| c_lessequals(V_m,V_n,tc_nat) ) ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f12,axiom,(
% 0.98/0.66 (![V_j,V_i]: (~ c_less(c_plus(V_j,V_i,tc_nat),V_i,tc_nat) ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f13,axiom,(
% 0.98/0.66 (![V_U,V_evs]: (( ~ c_in(c_Message_Omsg_ONonce(V_U),c_Event_Oused(V_evs),tc_Message_Omsg)| ~ c_lessequals(v_sko__urX(V_evs),V_U,tc_nat) ) ))),
% 0.98/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.98/0.66 fof(f15,plain,(
% 0.98/0.66 ![V_U]: ((![V_V]: ((![V_W]: (((V_U=V_W|V_V=V_W)|V_U=V_V)|c_in(c_Message_Omsg_ONonce(V_W),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)))|c_in(c_Message_Omsg_ONonce(V_V),c_Event_Oused(v_evs_H),tc_Message_Omsg)))|c_in(c_Message_Omsg_ONonce(V_U),c_Event_Oused(v_evs),tc_Message_Omsg))),
% 0.98/0.66 inference(miniscoping,[status(thm)],[f1])).
% 0.98/0.66 fof(f16,plain,(
% 0.98/0.66 ![X0,X1,X2]: (X0=X1|X2=X1|X0=X2|c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)|c_in(c_Message_Omsg_ONonce(X2),c_Event_Oused(v_evs_H),tc_Message_Omsg)|c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs),tc_Message_Omsg))),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f15])).
% 0.98/0.66 fof(f17,plain,(
% 0.98/0.66 ![X0]: (c_Binomial_Obinomial(X0,c_Suc(c_0))=X0)),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f2])).
% 0.98/0.66 fof(f18,plain,(
% 0.98/0.66 ![X0,X1]: (c_Binomial_Obinomial(c_Suc(X0),c_Suc(X1))=c_plus(c_Binomial_Obinomial(X0,X1),c_Binomial_Obinomial(X0,c_Suc(X1)),tc_nat))),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f3])).
% 0.98/0.66 fof(f19,plain,(
% 0.98/0.66 ![X0]: (c_Binomial_Obinomial(X0,c_0)=c_1)),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f4])).
% 0.98/0.66 fof(f20,plain,(
% 0.98/0.66 c_1=c_Suc(c_0)),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f5])).
% 0.98/0.66 fof(f21,plain,(
% 0.98/0.66 ![X0,X1]: (~c_minus(X0,X1,tc_nat)=c_0|c_lessequals(X0,X1,tc_nat))),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f6])).
% 0.98/0.66 fof(f22,plain,(
% 0.98/0.66 ![X0]: (c_minus(X0,X0,tc_nat)=c_0)),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f7])).
% 0.98/0.66 fof(f23,plain,(
% 0.98/0.66 ![X0,X1]: (c_lessequals(X0,c_plus(X0,X1,tc_nat),tc_nat))),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f8])).
% 0.98/0.66 fof(f24,plain,(
% 0.98/0.66 ![X0]: (c_less(X0,c_Suc(X0),tc_nat))),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f9])).
% 0.98/0.66 fof(f25,plain,(
% 0.98/0.66 ![X0,X1]: (~c_lessequals(X0,X1,tc_nat)|c_less(X0,c_Suc(X1),tc_nat))),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f10])).
% 0.98/0.66 fof(f26,plain,(
% 0.98/0.66 ![V_m,V_n]: ((![V_k]: ~c_lessequals(c_plus(V_k,V_m,tc_nat),c_plus(V_k,V_n,tc_nat),tc_nat))|c_lessequals(V_m,V_n,tc_nat))),
% 0.98/0.66 inference(miniscoping,[status(thm)],[f11])).
% 0.98/0.66 fof(f27,plain,(
% 0.98/0.66 ![X0,X1,X2]: (~c_lessequals(c_plus(X0,X1,tc_nat),c_plus(X0,X2,tc_nat),tc_nat)|c_lessequals(X1,X2,tc_nat))),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f26])).
% 0.98/0.66 fof(f28,plain,(
% 0.98/0.66 ![X0,X1]: (~c_less(c_plus(X0,X1,tc_nat),X1,tc_nat))),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f12])).
% 0.98/0.66 fof(f29,plain,(
% 0.98/0.66 ![X0,X1]: (~c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(X1),tc_Message_Omsg)|~c_lessequals(v_sko__urX(X1),X0,tc_nat))),
% 0.98/0.66 inference(cnf_transformation,[status(thm)],[f13])).
% 0.98/0.66 fof(f31,plain,(
% 0.98/0.66 ![X0]: (c_Binomial_Obinomial(X0,c_1)=X0)),
% 0.98/0.66 inference(forward_demodulation,[status(thm)],[f20,f17])).
% 0.98/0.66 fof(f32,plain,(
% 0.98/0.66 ![X0]: (c_Binomial_Obinomial(c_Suc(X0),c_Suc(c_1))=c_plus(X0,c_Binomial_Obinomial(X0,c_Suc(c_1)),tc_nat))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f31,f18])).
% 0.98/0.66 fof(f33,plain,(
% 0.98/0.66 ![X0]: (c_Binomial_Obinomial(c_Suc(X0),c_Suc(c_0))=c_plus(c_1,c_Binomial_Obinomial(X0,c_Suc(c_0)),tc_nat))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f19,f18])).
% 0.98/0.66 fof(f35,plain,(
% 0.98/0.66 ![X0]: (c_Binomial_Obinomial(c_Suc(X0),c_1)=c_plus(c_1,c_Binomial_Obinomial(X0,c_Suc(c_0)),tc_nat))),
% 0.98/0.66 inference(forward_demodulation,[status(thm)],[f20,f33])).
% 0.98/0.66 fof(f36,plain,(
% 0.98/0.66 ![X0]: (c_Suc(X0)=c_plus(c_1,c_Binomial_Obinomial(X0,c_Suc(c_0)),tc_nat))),
% 0.98/0.66 inference(forward_demodulation,[status(thm)],[f31,f35])).
% 0.98/0.66 fof(f37,plain,(
% 0.98/0.66 ![X0]: (c_Suc(X0)=c_plus(c_1,c_Binomial_Obinomial(X0,c_1),tc_nat))),
% 0.98/0.66 inference(forward_demodulation,[status(thm)],[f20,f36])).
% 0.98/0.66 fof(f38,plain,(
% 0.98/0.66 ![X0]: (c_Suc(X0)=c_plus(c_1,X0,tc_nat))),
% 0.98/0.66 inference(forward_demodulation,[status(thm)],[f31,f37])).
% 0.98/0.66 fof(f45,plain,(
% 0.98/0.66 ![X0,X1]: (c_lessequals(c_Binomial_Obinomial(X0,X1),c_Binomial_Obinomial(c_Suc(X0),c_Suc(X1)),tc_nat))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f18,f23])).
% 0.98/0.66 fof(f47,plain,(
% 0.98/0.66 ![X0]: (c_lessequals(X0,X0,tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f21,f22])).
% 0.98/0.66 fof(f52,plain,(
% 0.98/0.66 ![X0,X1]: (c_less(X0,c_Suc(c_plus(X0,X1,tc_nat)),tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f25,f23])).
% 0.98/0.66 fof(f54,plain,(
% 0.98/0.66 ![X0]: (~c_less(c_Suc(X0),X0,tc_nat))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f38,f28])).
% 0.98/0.66 fof(f61,plain,(
% 0.98/0.66 ![X0]: (c_lessequals(X0,c_Binomial_Obinomial(c_Suc(X0),c_Suc(c_1)),tc_nat))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f31,f45])).
% 0.98/0.66 fof(f69,plain,(
% 0.98/0.66 ![X0]: (c_less(X0,c_Suc(c_Binomial_Obinomial(c_Suc(X0),c_Suc(c_1))),tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f61,f25])).
% 0.98/0.66 fof(f81,plain,(
% 0.98/0.66 ![X0,X1]: (~c_lessequals(c_Suc(X0),c_plus(c_1,X1,tc_nat),tc_nat)|c_lessequals(X0,X1,tc_nat))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f38,f27])).
% 0.98/0.66 fof(f85,plain,(
% 0.98/0.66 ![X0,X1]: (~c_lessequals(c_Suc(X0),c_Suc(X1),tc_nat)|c_lessequals(X0,X1,tc_nat))),
% 0.98/0.66 inference(forward_demodulation,[status(thm)],[f38,f81])).
% 0.98/0.66 fof(f87,plain,(
% 0.98/0.66 ![X0,X1,X2]: (~c_lessequals(v_sko__urX(v_evs),X0,tc_nat)|X0=X1|X2=X1|X0=X2|c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)|c_in(c_Message_Omsg_ONonce(X2),c_Event_Oused(v_evs_H),tc_Message_Omsg))),
% 0.98/0.66 inference(resolution,[status(thm)],[f29,f16])).
% 0.98/0.66 fof(f99,plain,(
% 0.98/0.66 ![X0,X1]: (v_sko__urX(v_evs)=X0|X1=X0|v_sko__urX(v_evs)=X1|c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)|c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs_H),tc_Message_Omsg))),
% 0.98/0.66 inference(resolution,[status(thm)],[f87,f47])).
% 0.98/0.66 fof(f100,plain,(
% 0.98/0.66 ![X0,X1]: (v_sko__urX(v_evs)=X0|X1=X0|v_sko__urX(v_evs)=X1|c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs_H),tc_Message_Omsg)|~c_lessequals(v_sko__urX(v_evs_H_H),X0,tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f99,f29])).
% 0.98/0.66 fof(f101,plain,(
% 0.98/0.66 ![X0,X1]: (v_sko__urX(v_evs)=X0|X1=X0|v_sko__urX(v_evs)=X1|c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)|~c_lessequals(v_sko__urX(v_evs_H),X1,tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f99,f29])).
% 0.98/0.66 fof(f103,plain,(
% 0.98/0.66 ![X0,X1]: (v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)|X1=c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)|v_sko__urX(v_evs)=X1|c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs_H),tc_Message_Omsg))),
% 0.98/0.66 inference(resolution,[status(thm)],[f100,f23])).
% 0.98/0.66 fof(f104,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|X0=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=X0|c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs_H),tc_Message_Omsg))),
% 0.98/0.66 inference(resolution,[status(thm)],[f100,f47])).
% 0.98/0.66 fof(f105,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|X0=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=X0|~c_lessequals(v_sko__urX(v_evs_H),X0,tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f104,f29])).
% 0.98/0.66 fof(f110,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|c_plus(v_sko__urX(v_evs_H),X0,tc_nat)=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs_H),X0,tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f105,f23])).
% 0.98/0.66 fof(f116,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=X0|v_sko__urX(v_evs_H)=X0|v_sko__urX(v_evs)=v_sko__urX(v_evs_H)|c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs_H_H),tc_Message_Omsg))),
% 0.98/0.66 inference(resolution,[status(thm)],[f101,f47])).
% 0.98/0.66 fof(f117,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=X0|v_sko__urX(v_evs_H)=X0|v_sko__urX(v_evs)=v_sko__urX(v_evs_H)|~c_lessequals(v_sko__urX(v_evs_H_H),X0,tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f116,f29])).
% 0.98/0.66 fof(f119,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)|v_sko__urX(v_evs_H)=c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H))),
% 0.98/0.66 inference(resolution,[status(thm)],[f117,f23])).
% 0.98/0.66 fof(f232,plain,(
% 0.98/0.66 ![X0]: (~c_less(v_sko__urX(v_evs_H_H),X0,tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs_H),X0,tc_nat))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f110,f28])).
% 0.98/0.66 fof(f238,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs_H),c_Suc(c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)),tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f232,f52])).
% 0.98/0.66 fof(f239,plain,(
% 0.98/0.66 v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs_H),c_Suc(v_sko__urX(v_evs_H_H)),tc_nat)),
% 0.98/0.66 inference(resolution,[status(thm)],[f232,f24])).
% 0.98/0.66 fof(f268,plain,(
% 0.98/0.66 ![X0]: (~c_less(v_sko__urX(v_evs),c_Suc(c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)),tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f238,f28])).
% 0.98/0.66 fof(f273,plain,(
% 0.98/0.66 ~c_less(v_sko__urX(v_evs),c_Suc(c_Binomial_Obinomial(c_Suc(v_sko__urX(v_evs_H_H)),c_Suc(c_1))),tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f32,f268])).
% 0.98/0.66 fof(f376,plain,(
% 0.98/0.66 ![X0]: (~c_less(v_sko__urX(v_evs_H),X0,tc_nat)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f119,f28])).
% 0.98/0.66 fof(f385,plain,(
% 0.98/0.66 v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs_H_H),c_Suc(v_sko__urX(v_evs_H)),tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H)),
% 0.98/0.66 inference(resolution,[status(thm)],[f376,f24])).
% 0.98/0.66 fof(f389,plain,(
% 0.98/0.66 ~c_less(v_sko__urX(v_evs),c_Suc(v_sko__urX(v_evs)),tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H)),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f385,f268])).
% 0.98/0.66 fof(f401,plain,(
% 0.98/0.66 v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H)),
% 0.98/0.66 inference(forward_subsumption_resolution,[status(thm)],[f389,f24])).
% 0.98/0.66 fof(f402,plain,(
% 0.98/0.66 v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),c_Suc(v_sko__urX(v_evs_H)),tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H)),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f401,f385])).
% 0.98/0.66 fof(f415,plain,(
% 0.98/0.66 v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),c_Suc(v_sko__urX(v_evs_H)),tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H)),
% 0.98/0.66 inference(duplicate_literals_removal,[status(thm)],[f402])).
% 0.98/0.66 fof(f436,plain,(
% 0.98/0.66 ![X0]: (~c_lessequals(v_sko__urX(v_evs),c_plus(v_sko__urX(v_evs),X0,tc_nat),tc_nat)|c_lessequals(c_Suc(v_sko__urX(v_evs_H)),X0,tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f415,f27])).
% 0.98/0.66 fof(f441,plain,(
% 0.98/0.66 ![X0]: (c_lessequals(c_Suc(v_sko__urX(v_evs_H)),X0,tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H))),
% 0.98/0.66 inference(forward_subsumption_resolution,[status(thm)],[f436,f23])).
% 0.98/0.66 fof(f444,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H)|c_lessequals(v_sko__urX(v_evs_H),X0,tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f441,f85])).
% 0.98/0.66 fof(f450,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H)|c_less(v_sko__urX(v_evs_H),c_Suc(X0),tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f444,f25])).
% 0.98/0.66 fof(f451,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs_H_H),c_Suc(X0),tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H))),
% 0.98/0.66 inference(resolution,[status(thm)],[f450,f376])).
% 0.98/0.66 fof(f454,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs_H_H),c_Suc(X0),tc_nat))),
% 0.98/0.66 inference(duplicate_literals_removal,[status(thm)],[f451])).
% 0.98/0.66 fof(f541,plain,(
% 0.98/0.66 ![X0]: (~c_less(v_sko__urX(v_evs),c_Suc(X0),tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f454,f28])).
% 0.98/0.66 fof(f546,plain,(
% 0.98/0.66 v_sko__urX(v_evs)=v_sko__urX(v_evs_H)),
% 0.98/0.66 inference(resolution,[status(thm)],[f541,f69])).
% 0.98/0.66 fof(f577,plain,(
% 0.98/0.66 v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),c_Suc(v_sko__urX(v_evs_H_H)),tc_nat)),
% 0.98/0.66 inference(backward_demodulation,[status(thm)],[f546,f239])).
% 0.98/0.66 fof(f579,plain,(
% 0.98/0.66 ![X0]: (~c_less(v_sko__urX(v_evs_H_H),X0,tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X0,tc_nat))),
% 0.98/0.66 inference(backward_demodulation,[status(thm)],[f546,f232])).
% 0.98/0.66 fof(f608,plain,(
% 0.98/0.66 ![X0]: (~c_lessequals(v_sko__urX(v_evs),c_plus(v_sko__urX(v_evs),X0,tc_nat),tc_nat)|c_lessequals(c_Suc(v_sko__urX(v_evs_H_H)),X0,tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f577,f27])).
% 0.98/0.66 fof(f613,plain,(
% 0.98/0.66 ![X0]: (c_lessequals(c_Suc(v_sko__urX(v_evs_H_H)),X0,tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H))),
% 0.98/0.66 inference(forward_subsumption_resolution,[status(thm)],[f608,f23])).
% 0.98/0.66 fof(f616,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|c_lessequals(v_sko__urX(v_evs_H_H),X0,tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f613,f85])).
% 0.98/0.66 fof(f621,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|c_less(v_sko__urX(v_evs_H_H),c_Suc(X0),tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f616,f25])).
% 0.98/0.66 fof(f650,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),c_Suc(X0),tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H))),
% 0.98/0.66 inference(resolution,[status(thm)],[f579,f621])).
% 0.98/0.66 fof(f656,plain,(
% 0.98/0.66 ![X0]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),c_Suc(X0),tc_nat))),
% 0.98/0.66 inference(duplicate_literals_removal,[status(thm)],[f650])).
% 0.98/0.66 fof(f678,plain,(
% 0.98/0.66 ![X0,X1]: (~c_lessequals(v_sko__urX(v_evs),c_plus(v_sko__urX(v_evs),X0,tc_nat),tc_nat)|c_lessequals(c_Suc(X1),X0,tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H))),
% 0.98/0.66 inference(paramodulation,[status(thm)],[f656,f27])).
% 0.98/0.66 fof(f683,plain,(
% 0.98/0.66 ![X0,X1]: (c_lessequals(c_Suc(X0),X1,tc_nat)|v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H))),
% 0.98/0.66 inference(forward_subsumption_resolution,[status(thm)],[f678,f23])).
% 0.98/0.66 fof(f686,plain,(
% 0.98/0.66 ![X0,X1]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|c_lessequals(X0,X1,tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f683,f85])).
% 0.98/0.66 fof(f712,plain,(
% 0.98/0.66 ![X0,X1]: (v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)|c_less(X0,c_Suc(X1),tc_nat))),
% 0.98/0.66 inference(resolution,[status(thm)],[f686,f25])).
% 0.98/0.66 fof(f713,plain,(
% 0.98/0.66 v_sko__urX(v_evs)=v_sko__urX(v_evs_H_H)),
% 0.98/0.66 inference(backward_subsumption_resolution,[status(thm)],[f273,f712])).
% 0.98/0.66 fof(f957,plain,(
% 0.98/0.66 ![X0,X1]: (v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X0,tc_nat)|X1=c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)|v_sko__urX(v_evs)=X1|c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs_H),tc_Message_Omsg))),
% 0.98/0.66 inference(forward_demodulation,[status(thm)],[f713,f103])).
% 0.98/0.66 fof(f958,plain,(
% 0.98/0.68 ![X0,X1]: (v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X0,tc_nat)|X1=c_plus(v_sko__urX(v_evs),X0,tc_nat)|v_sko__urX(v_evs)=X1|c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs_H),tc_Message_Omsg))),
% 0.98/0.68 inference(forward_demodulation,[status(thm)],[f713,f957])).
% 0.98/0.68 fof(f959,plain,(
% 0.98/0.68 ![X0,X1]: (v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X0,tc_nat)|X1=c_plus(v_sko__urX(v_evs),X0,tc_nat)|v_sko__urX(v_evs)=X1|~c_lessequals(v_sko__urX(v_evs_H),X1,tc_nat))),
% 0.98/0.68 inference(resolution,[status(thm)],[f958,f29])).
% 0.98/0.68 fof(f960,plain,(
% 0.98/0.68 ![X0,X1]: (v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X0,tc_nat)|X1=c_plus(v_sko__urX(v_evs),X0,tc_nat)|v_sko__urX(v_evs)=X1|~c_lessequals(v_sko__urX(v_evs),X1,tc_nat))),
% 0.98/0.68 inference(forward_demodulation,[status(thm)],[f546,f959])).
% 0.98/0.68 fof(f962,plain,(
% 0.98/0.68 ![X0,X1]: (v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X0,tc_nat)|c_plus(v_sko__urX(v_evs),X1,tc_nat)=c_plus(v_sko__urX(v_evs),X0,tc_nat)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X1,tc_nat))),
% 0.98/0.68 inference(resolution,[status(thm)],[f960,f23])).
% 0.98/0.68 fof(f1092,plain,(
% 0.98/0.68 ![X0,X1]: (~c_less(c_plus(v_sko__urX(v_evs),X0,tc_nat),X1,tc_nat)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X0,tc_nat)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X1,tc_nat))),
% 0.98/0.68 inference(paramodulation,[status(thm)],[f962,f28])).
% 0.98/0.68 fof(f1114,plain,(
% 0.98/0.68 ![X0]: (v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X0,tc_nat)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),c_Suc(c_plus(v_sko__urX(v_evs),X0,tc_nat)),tc_nat))),
% 0.98/0.68 inference(resolution,[status(thm)],[f1092,f24])).
% 0.98/0.68 fof(f1135,plain,(
% 0.98/0.68 ![X0]: (~c_less(v_sko__urX(v_evs),c_Suc(c_plus(v_sko__urX(v_evs),X0,tc_nat)),tc_nat)|v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X0,tc_nat))),
% 0.98/0.68 inference(paramodulation,[status(thm)],[f1114,f28])).
% 0.98/0.68 fof(f1146,plain,(
% 0.98/0.68 ![X0]: (v_sko__urX(v_evs)=c_plus(v_sko__urX(v_evs),X0,tc_nat))),
% 0.98/0.68 inference(forward_subsumption_resolution,[status(thm)],[f1135,f52])).
% 0.98/0.68 fof(f1164,plain,(
% 0.98/0.68 ![X0,X1]: (~c_lessequals(c_plus(v_sko__urX(v_evs),X0,tc_nat),v_sko__urX(v_evs),tc_nat)|c_lessequals(X0,X1,tc_nat))),
% 0.98/0.68 inference(paramodulation,[status(thm)],[f1146,f27])).
% 0.98/0.68 fof(f1176,plain,(
% 0.98/0.68 ![X0,X1]: (~c_lessequals(v_sko__urX(v_evs),v_sko__urX(v_evs),tc_nat)|c_lessequals(X0,X1,tc_nat))),
% 0.98/0.68 inference(forward_demodulation,[status(thm)],[f1146,f1164])).
% 0.98/0.68 fof(f1177,plain,(
% 0.98/0.68 ![X0,X1]: (c_lessequals(X0,X1,tc_nat))),
% 0.98/0.68 inference(forward_subsumption_resolution,[status(thm)],[f1176,f47])).
% 0.98/0.68 fof(f1188,plain,(
% 0.98/0.68 ![X0,X1]: (c_less(X0,c_Suc(X1),tc_nat))),
% 0.98/0.68 inference(backward_subsumption_resolution,[status(thm)],[f25,f1177])).
% 0.98/0.68 fof(f1189,plain,(
% 0.98/0.68 $false),
% 0.98/0.68 inference(resolution,[status(thm)],[f1188,f54])).
% 0.98/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 0.98/0.69 % Elapsed time: 0.310652 seconds
% 0.98/0.69 % CPU time: 2.066398 seconds
% 0.98/0.69 % Total memory used: 132.615 MB
% 0.98/0.69 % Net memory used: 130.753 MB
%------------------------------------------------------------------------------