%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW374+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:09:02 PM UTC 2026
% Result : Theorem 0.42s 0.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW374+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n020.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 09:50:47 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.37/0.64 % Drodi V4.1.1
% 0.42/0.88 % Refutation found
% 0.42/0.88 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.42/0.88 % SZS output start CNFRefutation for theBenchmark
% 0.42/0.88 fof(f8,axiom,(
% 0.42/0.88 (! [V_b,V_pn] :( c_Com_OWT__bodies=> ( hAPP(c_Com_Obody,V_pn) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),V_b)=> hBOOL(hAPP(c_Com_OWT,V_b)) ) ) )),
% 0.42/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.42/0.88 fof(f21,axiom,(
% 0.42/0.88 (! [V_x,T_a] : hAPP(c_Option_Othe(T_a),hAPP(c_Option_Ooption_OSome(T_a),V_x)) = V_x )),
% 0.42/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.42/0.88 fof(f22,axiom,(
% 0.42/0.88 (! [V_a_2] :( hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OBODY(V_a_2)))<=> (? [B_y] : hAPP(c_Com_Obody,V_a_2) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),B_y) )) )),
% 0.42/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.42/0.88 fof(f27,axiom,(
% 0.42/0.88 (! [V_m_2,T_b,V_a_2,T_a] :( hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2)))=> (? [B_b] : hAPP(V_m_2,V_a_2) = hAPP(c_Option_Ooption_OSome(T_b),B_b) )) )),
% 0.42/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.42/0.88 fof(f38,axiom,(
% 0.42/0.88 (! [V_pn] :( hAPP(c_Com_Obody,V_pn) != c_Option_Ooption_ONone(tc_Com_Ocom)=> hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OBODY(V_pn))) ) )),
% 0.42/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.42/0.88 fof(f5246,hypothesis,(
% 0.42/0.88 c_Com_OWT__bodies ),
% 0.42/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.42/0.88 fof(f5248,hypothesis,(
% 0.42/0.88 hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),v_pn),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody))) ),
% 0.42/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.42/0.88 fof(f5249,conjecture,(
% 0.42/0.88 hBOOL(hAPP(c_Com_OWT,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)))) ),
% 0.42/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.42/0.88 fof(f5250,negated_conjecture,(
% 0.42/0.88 ~(hBOOL(hAPP(c_Com_OWT,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)))) )),
% 0.42/0.88 inference(negated_conjecture,[status(cth)],[f5249])).
% 0.42/0.88 fof(f5281,plain,(
% 0.42/0.88 ![V_b,V_pn]: (~c_Com_OWT__bodies|(~hAPP(c_Com_Obody,V_pn)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),V_b)|hBOOL(hAPP(c_Com_OWT,V_b))))),
% 0.42/0.88 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.42/0.88 fof(f5282,plain,(
% 0.42/0.88 ~c_Com_OWT__bodies|(![V_b]: ((![V_pn]: ~hAPP(c_Com_Obody,V_pn)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),V_b))|hBOOL(hAPP(c_Com_OWT,V_b))))),
% 0.42/0.88 inference(miniscoping,[status(thm)],[f5281])).
% 0.42/0.88 fof(f5283,plain,(
% 0.42/0.88 ![X0,X1]: (~c_Com_OWT__bodies|~hAPP(c_Com_Obody,X0)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),X1)|hBOOL(hAPP(c_Com_OWT,X1)))),
% 0.42/0.88 inference(cnf_transformation,[status(thm)],[f5282])).
% 0.42/0.88 fof(f5331,plain,(
% 0.42/0.88 ![X0,X1]: (hAPP(c_Option_Othe(X0),hAPP(c_Option_Ooption_OSome(X0),X1))=X1)),
% 0.42/0.88 inference(cnf_transformation,[status(thm)],[f21])).
% 0.42/0.88 fof(f5332,plain,(
% 0.42/0.88 ![V_a_2]: ((~hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OBODY(V_a_2)))|(?[B_y]: hAPP(c_Com_Obody,V_a_2)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),B_y)))&(hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OBODY(V_a_2)))|(![B_y]: ~hAPP(c_Com_Obody,V_a_2)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),B_y))))),
% 0.42/0.88 inference(NNF_transformation,[status(thm)],[f22])).
% 0.42/0.88 fof(f5333,plain,(
% 0.42/0.88 (![V_a_2]: (~hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OBODY(V_a_2)))|(?[B_y]: hAPP(c_Com_Obody,V_a_2)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),B_y))))&(![V_a_2]: (hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OBODY(V_a_2)))|(![B_y]: ~hAPP(c_Com_Obody,V_a_2)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),B_y))))),
% 0.42/0.88 inference(miniscoping,[status(thm)],[f5332])).
% 0.42/0.88 fof(f5334,plain,(
% 0.42/0.88 (![V_a_2]: (~hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OBODY(V_a_2)))|hAPP(c_Com_Obody,V_a_2)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),sK4_skl(V_a_2))))&(![V_a_2]: (hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OBODY(V_a_2)))|(![B_y]: ~hAPP(c_Com_Obody,V_a_2)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),B_y))))),
% 0.42/0.88 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B_y,sK4_skl(V_a_2))],[f5333])).
% 0.42/0.88 fof(f5335,plain,(
% 0.42/0.88 ![X0]: (~hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OBODY(X0)))|hAPP(c_Com_Obody,X0)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),sK4_skl(X0)))),
% 0.42/0.88 inference(cnf_transformation,[status(thm)],[f5334])).
% 0.42/0.88 fof(f5351,plain,(
% 0.42/0.88 ![V_m_2,T_b,V_a_2,T_a]: (~hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2)))|(?[B_b]: hAPP(V_m_2,V_a_2)=hAPP(c_Option_Ooption_OSome(T_b),B_b)))),
% 0.42/0.88 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.42/0.88 fof(f5352,plain,(
% 0.42/0.88 ![V_m_2,T_b,V_a_2]: ((![T_a]: ~hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2))))|(?[B_b]: hAPP(V_m_2,V_a_2)=hAPP(c_Option_Ooption_OSome(T_b),B_b)))),
% 0.42/0.88 inference(miniscoping,[status(thm)],[f5351])).
% 0.42/0.88 fof(f5353,plain,(
% 0.42/0.88 ![V_m_2,T_b,V_a_2]: ((![T_a]: ~hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2))))|hAPP(V_m_2,V_a_2)=hAPP(c_Option_Ooption_OSome(T_b),sK5_skl(V_a_2,T_b,V_m_2)))),
% 0.42/0.88 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(B_b,sK5_skl(V_a_2,T_b,V_m_2))],[f5352])).
% 0.42/0.88 fof(f5354,plain,(
% 0.42/0.88 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),c_Map_Odom(X0,X2,X3)))|hAPP(X3,X1)=hAPP(c_Option_Ooption_OSome(X2),sK5_skl(X1,X2,X3)))),
% 0.42/0.88 inference(cnf_transformation,[status(thm)],[f5353])).
% 0.42/0.88 fof(f5380,plain,(
% 0.42/0.88 ![V_pn]: (hAPP(c_Com_Obody,V_pn)=c_Option_Ooption_ONone(tc_Com_Ocom)|hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OBODY(V_pn))))),
% 0.42/0.88 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.42/0.88 fof(f5381,plain,(
% 0.42/0.88 ![X0]: (hAPP(c_Com_Obody,X0)=c_Option_Ooption_ONone(tc_Com_Ocom)|hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OBODY(X0))))),
% 0.42/0.88 inference(cnf_transformation,[status(thm)],[f5380])).
% 0.42/0.88 fof(f19978,plain,(
% 0.42/0.88 c_Com_OWT__bodies),
% 0.42/0.88 inference(cnf_transformation,[status(thm)],[f5246])).
% 0.42/0.88 fof(f19980,plain,(
% 0.42/0.88 hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),v_pn),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)))),
% 0.42/0.88 inference(cnf_transformation,[status(thm)],[f5248])).
% 0.42/0.88 fof(f19981,plain,(
% 0.42/0.88 ~hBOOL(hAPP(c_Com_OWT,hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))))),
% 0.42/0.88 inference(cnf_transformation,[status(thm)],[f5250])).
% 0.42/0.88 fof(f20780,plain,(
% 0.42/0.88 ![X0,X1]: (~hAPP(c_Com_Obody,X0)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),X1)|hBOOL(hAPP(c_Com_OWT,X1)))),
% 0.42/0.88 inference(forward_subsumption_resolution,[status(thm)],[f5283,f19978])).
% 0.42/0.88 fof(f20782,plain,(
% 0.42/0.88 ![X0]: (~hAPP(c_Com_Obody,X0)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))))),
% 0.42/0.88 inference(resolution,[status(thm)],[f20780,f19981])).
% 0.42/0.88 fof(f21536,plain,(
% 0.42/0.88 ![X0]: (hAPP(c_Com_Obody,X0)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),sK4_skl(X0))|hAPP(c_Com_Obody,X0)=c_Option_Ooption_ONone(tc_Com_Ocom))),
% 0.42/0.88 inference(resolution,[status(thm)],[f5335,f5381])).
% 0.42/0.88 fof(f21544,plain,(
% 0.42/0.88 ![X0]: (hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X0))=sK4_skl(X0)|hAPP(c_Com_Obody,X0)=c_Option_Ooption_ONone(tc_Com_Ocom))),
% 0.42/0.88 inference(paramodulation,[status(thm)],[f21536,f5331])).
% 0.42/0.88 fof(f21548,plain,(
% 0.42/0.88 ![X0]: (~hAPP(c_Com_Obody,X0)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),sK4_skl(v_pn))|hAPP(c_Com_Obody,v_pn)=c_Option_Ooption_ONone(tc_Com_Ocom))),
% 0.42/0.88 inference(paramodulation,[status(thm)],[f21544,f20782])).
% 0.42/0.88 fof(f21768,plain,(
% 0.42/0.88 hAPP(c_Com_Obody,v_pn)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),sK5_skl(v_pn,tc_Com_Ocom,c_Com_Obody))),
% 0.42/0.88 inference(resolution,[status(thm)],[f5354,f19980])).
% 0.42/0.88 fof(f21779,plain,(
% 0.42/0.88 hAPP(c_Com_Obody,v_pn)=c_Option_Ooption_ONone(tc_Com_Ocom)|hAPP(c_Com_Obody,v_pn)=c_Option_Ooption_ONone(tc_Com_Ocom)),
% 0.42/0.88 inference(resolution,[status(thm)],[f21548,f21536])).
% 0.42/0.88 fof(f21781,plain,(
% 0.42/0.88 hAPP(c_Com_Obody,v_pn)=c_Option_Ooption_ONone(tc_Com_Ocom)),
% 0.42/0.88 inference(duplicate_literals_removal,[status(thm)],[f21779])).
% 0.42/0.88 fof(f21790,plain,(
% 0.42/0.88 ~hBOOL(hAPP(c_Com_OWT,hAPP(c_Option_Othe(tc_Com_Ocom),c_Option_Ooption_ONone(tc_Com_Ocom))))),
% 0.42/0.88 inference(backward_demodulation,[status(thm)],[f21781,f19981])).
% 0.42/0.88 fof(f21796,plain,(
% 0.42/0.88 ![X0]: (~hAPP(c_Com_Obody,X0)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),hAPP(c_Option_Othe(tc_Com_Ocom),c_Option_Ooption_ONone(tc_Com_Ocom))))),
% 0.42/0.88 inference(resolution,[status(thm)],[f21790,f20780])).
% 0.42/0.88 fof(f21797,plain,(
% 0.42/0.88 c_Option_Ooption_ONone(tc_Com_Ocom)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),sK5_skl(v_pn,tc_Com_Ocom,c_Com_Obody))),
% 0.42/0.88 inference(forward_demodulation,[status(thm)],[f21781,f21768])).
% 0.42/0.88 fof(f21801,plain,(
% 0.42/0.88 hAPP(c_Option_Othe(tc_Com_Ocom),c_Option_Ooption_ONone(tc_Com_Ocom))=sK5_skl(v_pn,tc_Com_Ocom,c_Com_Obody)),
% 0.42/0.88 inference(paramodulation,[status(thm)],[f21797,f5331])).
% 0.42/0.88 fof(f21821,plain,(
% 0.42/0.88 ![X0]: (~hAPP(c_Com_Obody,X0)=hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),sK5_skl(v_pn,tc_Com_Ocom,c_Com_Obody)))),
% 0.43/0.94 inference(forward_demodulation,[status(thm)],[f21801,f21796])).
% 0.43/0.94 fof(f21829,plain,(
% 0.43/0.94 ![X0]: (~hAPP(c_Com_Obody,X0)=c_Option_Ooption_ONone(tc_Com_Ocom))),
% 0.43/0.94 inference(forward_demodulation,[status(thm)],[f21797,f21821])).
% 0.43/0.94 fof(f21830,plain,(
% 0.43/0.94 $false),
% 0.43/0.94 inference(backward_subsumption_resolution,[status(thm)],[f21781,f21829])).
% 0.43/0.94 % SZS output end CNFRefutation for theBenchmark.p
% 0.43/0.98 % Elapsed time: 0.606519 seconds
% 0.43/0.98 % CPU time: 2.310162 seconds
% 0.43/0.98 % Total memory used: 665.927 MB
% 0.43/0.98 % Net memory used: 660.641 MB
%------------------------------------------------------------------------------