%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW295+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 03:08:55 PM UTC 2026
% Result : Theorem 0.57s 1.13s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW295+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n012.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:45:37 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.49/0.86 % Drodi V4.1.1
% 0.57/1.13 % Refutation found
% 0.57/1.13 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.57/1.13 % SZS output start CNFRefutation for theBenchmark
% 0.57/1.13 fof(f2,axiom,(
% 0.57/1.13 (! [V_s1,V_n,V_s0,V_pn] :( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_pn)),V_s0,V_n,V_s1)=> c_Natural_Oevaln(c_Com_Ocom_OBODY(V_pn),V_s0,hAPP(c_Nat_OSuc,V_n),V_s1) ) )),
% 0.57/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.57/1.13 fof(f3,axiom,(
% 0.57/1.13 (! [V_a4_2,V_a3_2,V_a2_2,V_a1_2] :( c_Natural_Oevaln(c_Com_Ocom_OBODY(V_a1_2),V_a2_2,hAPP(c_Nat_OSuc,V_a3_2),V_a4_2)<=> c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_a1_2)),V_a2_2,V_a3_2,V_a4_2) ) )),
% 0.57/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.57/1.13 fof(f5205,conjecture,(
% 0.57/1.13 ( (! [B_Z,B_s] :( v_P(B_Z,B_s)=> (! [B_s_H] :( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),B_s,v_n,B_s_H)=> v_Q(B_Z,B_s_H) ) )))<=> (! [B_Z,B_s] :( v_P(B_Z,B_s)=> (! [B_s_H] :( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),B_s,hAPP(c_Nat_OSuc,v_n),B_s_H)=> v_Q(B_Z,B_s_H) ) )) )) ),
% 0.57/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.57/1.13 fof(f5206,negated_conjecture,(
% 0.57/1.13 ~(( (! [B_Z,B_s] :( v_P(B_Z,B_s)=> (! [B_s_H] :( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),B_s,v_n,B_s_H)=> v_Q(B_Z,B_s_H) ) )))<=> (! [B_Z,B_s] :( v_P(B_Z,B_s)=> (! [B_s_H] :( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),B_s,hAPP(c_Nat_OSuc,v_n),B_s_H)=> v_Q(B_Z,B_s_H) ) )) )) )),
% 0.57/1.13 inference(negated_conjecture,[status(cth)],[f5205])).
% 0.57/1.13 fof(f5210,plain,(
% 0.57/1.13 ![V_s1,V_n,V_s0,V_pn]: (~c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_pn)),V_s0,V_n,V_s1)|c_Natural_Oevaln(c_Com_Ocom_OBODY(V_pn),V_s0,hAPP(c_Nat_OSuc,V_n),V_s1))),
% 0.57/1.13 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.57/1.13 fof(f5211,plain,(
% 0.57/1.13 ![X0,X1,X2,X3]: (~c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X0)),X1,X2,X3)|c_Natural_Oevaln(c_Com_Ocom_OBODY(X0),X1,hAPP(c_Nat_OSuc,X2),X3))),
% 0.57/1.13 inference(cnf_transformation,[status(thm)],[f5210])).
% 0.57/1.13 fof(f5212,plain,(
% 0.57/1.13 ![V_a4_2,V_a3_2,V_a2_2,V_a1_2]: ((~c_Natural_Oevaln(c_Com_Ocom_OBODY(V_a1_2),V_a2_2,hAPP(c_Nat_OSuc,V_a3_2),V_a4_2)|c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_a1_2)),V_a2_2,V_a3_2,V_a4_2))&(c_Natural_Oevaln(c_Com_Ocom_OBODY(V_a1_2),V_a2_2,hAPP(c_Nat_OSuc,V_a3_2),V_a4_2)|~c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_a1_2)),V_a2_2,V_a3_2,V_a4_2)))),
% 0.57/1.14 inference(NNF_transformation,[status(thm)],[f3])).
% 0.57/1.14 fof(f5213,plain,(
% 0.57/1.14 (![V_a4_2,V_a3_2,V_a2_2,V_a1_2]: (~c_Natural_Oevaln(c_Com_Ocom_OBODY(V_a1_2),V_a2_2,hAPP(c_Nat_OSuc,V_a3_2),V_a4_2)|c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_a1_2)),V_a2_2,V_a3_2,V_a4_2)))&(![V_a4_2,V_a3_2,V_a2_2,V_a1_2]: (c_Natural_Oevaln(c_Com_Ocom_OBODY(V_a1_2),V_a2_2,hAPP(c_Nat_OSuc,V_a3_2),V_a4_2)|~c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,V_a1_2)),V_a2_2,V_a3_2,V_a4_2)))),
% 0.57/1.14 inference(miniscoping,[status(thm)],[f5212])).
% 0.57/1.14 fof(f5214,plain,(
% 0.57/1.14 ![X0,X1,X2,X3]: (~c_Natural_Oevaln(c_Com_Ocom_OBODY(X0),X1,hAPP(c_Nat_OSuc,X2),X3)|c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X0)),X1,X2,X3))),
% 0.57/1.14 inference(cnf_transformation,[status(thm)],[f5213])).
% 0.57/1.14 fof(f19777,plain,(
% 0.57/1.14 ((![B_Z,B_s]: (~v_P(B_Z,B_s)|(![B_s_H]: (~c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),B_s,v_n,B_s_H)|v_Q(B_Z,B_s_H)))))<~>(![B_Z,B_s]: (~v_P(B_Z,B_s)|(![B_s_H]: (~c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),B_s,hAPP(c_Nat_OSuc,v_n),B_s_H)|v_Q(B_Z,B_s_H))))))),
% 0.57/1.14 inference(pre_NNF_transformation,[status(thm)],[f5206])).
% 0.57/1.14 fof(f19778,plain,(
% 0.57/1.14 ((![B_Z,B_s]: (~v_P(B_Z,B_s)|(![B_s_H]: (~c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),B_s,v_n,B_s_H)|v_Q(B_Z,B_s_H)))))|(![B_Z,B_s]: (~v_P(B_Z,B_s)|(![B_s_H]: (~c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),B_s,hAPP(c_Nat_OSuc,v_n),B_s_H)|v_Q(B_Z,B_s_H))))))&((?[B_Z,B_s]: (v_P(B_Z,B_s)&(?[B_s_H]: (c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),B_s,v_n,B_s_H)&~v_Q(B_Z,B_s_H)))))|(?[B_Z,B_s]: (v_P(B_Z,B_s)&(?[B_s_H]: (c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),B_s,hAPP(c_Nat_OSuc,v_n),B_s_H)&~v_Q(B_Z,B_s_H))))))),
% 0.57/1.14 inference(NNF_transformation,[status(thm)],[f19777])).
% 0.57/1.14 fof(f19779,plain,(
% 0.57/1.14 ((![B_Z,B_s]: (~v_P(B_Z,B_s)|(![B_s_H]: (~c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),B_s,v_n,B_s_H)|v_Q(B_Z,B_s_H)))))|(![B_Z,B_s]: (~v_P(B_Z,B_s)|(![B_s_H]: (~c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),B_s,hAPP(c_Nat_OSuc,v_n),B_s_H)|v_Q(B_Z,B_s_H))))))&((v_P(sK488_skl,sK489_skl)&(c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK489_skl,v_n,sK490_skl)&~v_Q(sK488_skl,sK490_skl)))|(v_P(sK491_skl,sK492_skl)&(c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK492_skl,hAPP(c_Nat_OSuc,v_n),sK493_skl)&~v_Q(sK491_skl,sK493_skl))))),
% 0.57/1.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK488_skl,sK489_skl,sK490_skl,sK491_skl,sK492_skl,sK493_skl]),skolemize(B_Z,sK488_skl),skolemize(B_s,sK489_skl),skolemize(B_s_H,sK490_skl),skolemize(B_Z,sK491_skl),skolemize(B_s,sK492_skl),skolemize(B_s_H,sK493_skl)],[f19778])).
% 0.57/1.14 fof(f19780,plain,(
% 0.57/1.14 ![X0,X1,X2,X3,X4,X5]: (~v_P(X0,X1)|~c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2)|v_Q(X0,X2)|~v_P(X3,X4)|~c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X4,hAPP(c_Nat_OSuc,v_n),X5)|v_Q(X3,X5))),
% 0.57/1.14 inference(cnf_transformation,[status(thm)],[f19779])).
% 0.57/1.14 fof(f19781,plain,(
% 0.57/1.14 v_P(sK488_skl,sK489_skl)|v_P(sK491_skl,sK492_skl)),
% 0.57/1.14 inference(cnf_transformation,[status(thm)],[f19779])).
% 0.57/1.14 fof(f19782,plain,(
% 0.57/1.14 v_P(sK488_skl,sK489_skl)|c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK492_skl,hAPP(c_Nat_OSuc,v_n),sK493_skl)),
% 0.57/1.14 inference(cnf_transformation,[status(thm)],[f19779])).
% 0.57/1.14 fof(f19783,plain,(
% 0.57/1.14 v_P(sK488_skl,sK489_skl)|~v_Q(sK491_skl,sK493_skl)),
% 0.57/1.14 inference(cnf_transformation,[status(thm)],[f19779])).
% 0.57/1.14 fof(f19784,plain,(
% 0.57/1.14 c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK489_skl,v_n,sK490_skl)|v_P(sK491_skl,sK492_skl)),
% 0.57/1.14 inference(cnf_transformation,[status(thm)],[f19779])).
% 0.57/1.14 fof(f19785,plain,(
% 0.57/1.14 c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK489_skl,v_n,sK490_skl)|c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK492_skl,hAPP(c_Nat_OSuc,v_n),sK493_skl)),
% 0.57/1.14 inference(cnf_transformation,[status(thm)],[f19779])).
% 0.57/1.14 fof(f19786,plain,(
% 0.57/1.14 c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK489_skl,v_n,sK490_skl)|~v_Q(sK491_skl,sK493_skl)),
% 0.57/1.14 inference(cnf_transformation,[status(thm)],[f19779])).
% 0.57/1.14 fof(f19787,plain,(
% 0.57/1.14 ~v_Q(sK488_skl,sK490_skl)|v_P(sK491_skl,sK492_skl)),
% 0.57/1.14 inference(cnf_transformation,[status(thm)],[f19779])).
% 0.57/1.14 fof(f19788,plain,(
% 0.57/1.14 ~v_Q(sK488_skl,sK490_skl)|c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK492_skl,hAPP(c_Nat_OSuc,v_n),sK493_skl)),
% 0.57/1.14 inference(cnf_transformation,[status(thm)],[f19779])).
% 0.57/1.14 fof(f19789,plain,(
% 0.57/1.14 ~v_Q(sK488_skl,sK490_skl)|~v_Q(sK491_skl,sK493_skl)),
% 0.57/1.14 inference(cnf_transformation,[status(thm)],[f19779])).
% 0.57/1.14 fof(f20122,definition,(
% 0.57/1.14 ![X0,X1,X2]: (sQ13_spl <=> (~v_P(X0,X1)|~c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2)|v_Q(X0,X2)))),
% 0.57/1.14 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.57/1.14 fof(f20123,plain,(
% 0.57/1.14 ![X0,X1,X2]: (~v_P(X0,X1)|~c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2)|v_Q(X0,X2)|~sQ13_spl)),
% 0.57/1.14 inference(component_clause,[status(thm)],[f20122])).
% 0.57/1.14 fof(f20125,definition,(
% 0.57/1.14 ![X3,X4,X5]: (sQ14_spl <=> (~v_P(X3,X4)|~c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X4,hAPP(c_Nat_OSuc,v_n),X5)|v_Q(X3,X5)))),
% 0.57/1.14 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.57/1.14 fof(f20126,plain,(
% 0.57/1.14 ![X0,X1,X2]: (~v_P(X0,X1)|~c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X1,hAPP(c_Nat_OSuc,v_n),X2)|v_Q(X0,X2)|~sQ14_spl)),
% 0.57/1.14 inference(component_clause,[status(thm)],[f20125])).
% 0.57/1.14 fof(f20128,plain,(
% 0.57/1.14 sQ13_spl|sQ14_spl),
% 0.57/1.14 inference(split_clause,[status(thm)],[f19780,f20122,f20125])).
% 0.57/1.14 fof(f20129,definition,(
% 0.57/1.14 sQ15_spl <=> (v_P(sK488_skl,sK489_skl))),
% 0.57/1.14 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.57/1.14 fof(f20130,plain,(
% 0.57/1.14 v_P(sK488_skl,sK489_skl)|~sQ15_spl),
% 0.57/1.14 inference(component_clause,[status(thm)],[f20129])).
% 0.57/1.14 fof(f20132,definition,(
% 0.57/1.14 sQ16_spl <=> (v_P(sK491_skl,sK492_skl))),
% 0.57/1.14 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.57/1.14 fof(f20133,plain,(
% 0.57/1.14 v_P(sK491_skl,sK492_skl)|~sQ16_spl),
% 0.57/1.14 inference(component_clause,[status(thm)],[f20132])).
% 0.57/1.14 fof(f20135,plain,(
% 0.57/1.14 sQ15_spl|sQ16_spl),
% 0.57/1.14 inference(split_clause,[status(thm)],[f19781,f20129,f20132])).
% 0.57/1.14 fof(f20136,definition,(
% 0.57/1.14 sQ17_spl <=> (c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK492_skl,hAPP(c_Nat_OSuc,v_n),sK493_skl))),
% 0.57/1.14 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.57/1.14 fof(f20137,plain,(
% 0.57/1.14 c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK492_skl,hAPP(c_Nat_OSuc,v_n),sK493_skl)|~sQ17_spl),
% 0.57/1.14 inference(component_clause,[status(thm)],[f20136])).
% 0.57/1.14 fof(f20139,plain,(
% 0.57/1.14 sQ15_spl|sQ17_spl),
% 0.57/1.14 inference(split_clause,[status(thm)],[f19782,f20129,f20136])).
% 0.57/1.14 fof(f20140,definition,(
% 0.57/1.14 sQ18_spl <=> (v_Q(sK491_skl,sK493_skl))),
% 0.57/1.14 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.57/1.14 fof(f20142,plain,(
% 0.57/1.14 ~v_Q(sK491_skl,sK493_skl)|sQ18_spl),
% 0.57/1.14 inference(component_clause,[status(thm)],[f20140])).
% 0.57/1.14 fof(f20143,plain,(
% 0.57/1.14 sQ15_spl|~sQ18_spl),
% 0.57/1.14 inference(split_clause,[status(thm)],[f19783,f20129,f20140])).
% 0.57/1.14 fof(f20144,definition,(
% 0.57/1.14 sQ19_spl <=> (c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK489_skl,v_n,sK490_skl))),
% 0.57/1.14 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.57/1.14 fof(f20145,plain,(
% 0.57/1.14 c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK489_skl,v_n,sK490_skl)|~sQ19_spl),
% 0.57/1.14 inference(component_clause,[status(thm)],[f20144])).
% 0.57/1.14 fof(f20147,plain,(
% 0.57/1.14 sQ19_spl|sQ16_spl),
% 0.57/1.14 inference(split_clause,[status(thm)],[f19784,f20144,f20132])).
% 0.57/1.14 fof(f20148,plain,(
% 0.57/1.14 sQ19_spl|sQ17_spl),
% 0.57/1.14 inference(split_clause,[status(thm)],[f19785,f20144,f20136])).
% 0.57/1.14 fof(f20149,plain,(
% 0.57/1.14 sQ19_spl|~sQ18_spl),
% 0.57/1.14 inference(split_clause,[status(thm)],[f19786,f20144,f20140])).
% 0.57/1.14 fof(f20150,definition,(
% 0.57/1.14 sQ20_spl <=> (v_Q(sK488_skl,sK490_skl))),
% 0.57/1.14 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.57/1.14 fof(f20152,plain,(
% 0.57/1.14 ~v_Q(sK488_skl,sK490_skl)|sQ20_spl),
% 0.57/1.14 inference(component_clause,[status(thm)],[f20150])).
% 0.57/1.14 fof(f20153,plain,(
% 0.57/1.14 ~sQ20_spl|sQ16_spl),
% 0.57/1.14 inference(split_clause,[status(thm)],[f19787,f20150,f20132])).
% 0.57/1.14 fof(f20154,plain,(
% 0.57/1.14 ~sQ20_spl|sQ17_spl),
% 0.57/1.14 inference(split_clause,[status(thm)],[f19788,f20150,f20136])).
% 0.57/1.14 fof(f20155,plain,(
% 0.57/1.14 ~sQ20_spl|~sQ18_spl),
% 0.57/1.14 inference(split_clause,[status(thm)],[f19789,f20150,f20140])).
% 0.57/1.14 fof(f20653,plain,(
% 0.57/1.14 ![X0]: (~v_P(X0,sK489_skl)|v_Q(X0,sK490_skl)|~sQ13_spl|~sQ19_spl)),
% 0.57/1.14 inference(resolution,[status(thm)],[f20123,f20145])).
% 0.57/1.14 fof(f20654,plain,(
% 0.57/1.14 v_Q(sK488_skl,sK490_skl)|~sQ13_spl|~sQ19_spl|~sQ15_spl),
% 0.57/1.14 inference(resolution,[status(thm)],[f20653,f20130])).
% 0.57/1.14 fof(f20655,plain,(
% 0.57/1.14 $false|sQ20_spl|~sQ13_spl|~sQ19_spl|~sQ15_spl),
% 0.57/1.14 inference(forward_subsumption_resolution,[status(thm)],[f20654,f20152])).
% 0.57/1.14 fof(f20656,plain,(
% 0.57/1.14 sQ20_spl|~sQ13_spl|~sQ19_spl|~sQ15_spl),
% 0.57/1.14 inference(contradiction_clause,[status(thm)],[f20655])).
% 0.57/1.14 fof(f20658,plain,(
% 0.57/1.14 c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK489_skl,hAPP(c_Nat_OSuc,v_n),sK490_skl)|~sQ19_spl),
% 0.57/1.14 inference(resolution,[status(thm)],[f5211,f20145])).
% 0.57/1.14 fof(f20661,plain,(
% 0.57/1.14 c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK492_skl,v_n,sK493_skl)|~sQ17_spl),
% 0.57/1.14 inference(resolution,[status(thm)],[f20137,f5214])).
% 0.57/1.14 fof(f20671,plain,(
% 0.57/1.14 ![X0]: (~v_P(X0,sK489_skl)|v_Q(X0,sK490_skl)|~sQ14_spl|~sQ19_spl)),
% 0.57/1.14 inference(resolution,[status(thm)],[f20126,f20658])).
% 0.57/1.14 fof(f20672,plain,(
% 0.57/1.14 ![X0]: (~v_P(X0,sK492_skl)|v_Q(X0,sK493_skl)|~sQ14_spl|~sQ17_spl)),
% 0.57/1.14 inference(resolution,[status(thm)],[f20126,f20137])).
% 0.57/1.14 fof(f20673,plain,(
% 0.57/1.14 v_Q(sK488_skl,sK490_skl)|~sQ14_spl|~sQ19_spl|~sQ15_spl),
% 0.57/1.14 inference(resolution,[status(thm)],[f20671,f20130])).
% 0.57/1.14 fof(f20674,plain,(
% 0.57/1.14 v_Q(sK491_skl,sK493_skl)|~sQ14_spl|~sQ17_spl|~sQ16_spl),
% 0.57/1.14 inference(resolution,[status(thm)],[f20672,f20133])).
% 0.57/1.22 fof(f20675,plain,(
% 0.57/1.22 $false|sQ18_spl|~sQ14_spl|~sQ17_spl|~sQ16_spl),
% 0.57/1.22 inference(forward_subsumption_resolution,[status(thm)],[f20674,f20142])).
% 0.57/1.22 fof(f20676,plain,(
% 0.57/1.22 sQ18_spl|~sQ14_spl|~sQ17_spl|~sQ16_spl),
% 0.57/1.22 inference(contradiction_clause,[status(thm)],[f20675])).
% 0.57/1.22 fof(f20695,plain,(
% 0.57/1.22 ![X0]: (~v_P(X0,sK492_skl)|v_Q(X0,sK493_skl)|~sQ13_spl|~sQ17_spl)),
% 0.57/1.22 inference(resolution,[status(thm)],[f20123,f20661])).
% 0.57/1.22 fof(f20697,plain,(
% 0.57/1.22 v_Q(sK491_skl,sK493_skl)|~sQ13_spl|~sQ17_spl|~sQ16_spl),
% 0.57/1.22 inference(resolution,[status(thm)],[f20695,f20133])).
% 0.57/1.22 fof(f20698,plain,(
% 0.57/1.22 $false|sQ18_spl|~sQ13_spl|~sQ17_spl|~sQ16_spl),
% 0.57/1.22 inference(forward_subsumption_resolution,[status(thm)],[f20697,f20142])).
% 0.57/1.22 fof(f20699,plain,(
% 0.57/1.22 sQ18_spl|~sQ13_spl|~sQ17_spl|~sQ16_spl),
% 0.57/1.22 inference(contradiction_clause,[status(thm)],[f20698])).
% 0.57/1.22 fof(f20700,plain,(
% 0.57/1.22 sQ20_spl|~sQ14_spl|~sQ19_spl|~sQ15_spl),
% 0.57/1.22 inference(split_clause,[status(thm)],[f20673,f20150,f20125,f20144,f20129])).
% 0.57/1.22 fof(f20701,plain,(
% 0.57/1.22 $false),
% 0.57/1.22 inference(sat_refutation,[status(thm)],[f20128,f20135,f20139,f20143,f20147,f20148,f20149,f20153,f20154,f20155,f20656,f20676,f20699,f20700])).
% 0.57/1.22 % SZS output end CNFRefutation for theBenchmark.p
% 1.06/1.25 % Elapsed time: 0.880326 seconds
% 1.06/1.25 % CPU time: 2.562377 seconds
% 1.06/1.25 % Total memory used: 667.284 MB
% 1.06/1.25 % Net memory used: 661.426 MB
%------------------------------------------------------------------------------