%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL443-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:10:05 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL443-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n009.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 00:32:42 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.13/0.41 % Refutation found
% 0.13/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.41 fof(f1,axiom,(
% 0.13/0.41 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f2,axiom,(
% 0.13/0.41 (![V_p,V_q,T_a,V_H]: (ifeq(c_in(c_PropLog_Opl_Oop_A_N_62(V_p,V_q,T_a),c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)),true,ifeq(c_in(V_p,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)),true,c_in(V_q,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)),true),true) = true ))),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f3,axiom,(
% 0.13/0.41 (![V_q,V_p,V_H,T_a]: (ifeq(c_in(V_q,c_PropLog_Othms(c_insert(V_p,V_H,tc_PropLog_Opl(T_a)),T_a),tc_PropLog_Opl(T_a)),true,c_in(c_PropLog_Opl_Oop_A_N_62(V_p,V_q,T_a),c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)),true) = true ))),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f4,axiom,(
% 0.13/0.41 (![V_p,V_H,T_a]: (ifeq(c_in(V_p,V_H,tc_PropLog_Opl(T_a)),true,c_in(V_p,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)),true) = true ))),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f5,axiom,(
% 0.13/0.41 (![V_p,V_G,T_a,V_a]: (ifeq(c_in(V_p,c_PropLog_Othms(V_G,T_a),tc_PropLog_Opl(T_a)),true,c_in(V_p,c_PropLog_Othms(c_insert(V_a,V_G,tc_PropLog_Opl(T_a)),T_a),tc_PropLog_Opl(T_a)),true) = true ))),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f6,axiom,(
% 0.13/0.41 (![V_x,V_B,T_a]: (c_in(V_x,c_insert(V_x,V_B,T_a),T_a) = true ))),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f7,negated_conjecture,(
% 0.13/0.41 c_in(v_p,c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)) = true ),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f8,negated_conjecture,(
% 0.13/0.41 c_in(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)) = true ),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f9,negated_conjecture,(
% 0.13/0.41 c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)) != true ),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f10,plain,(
% 0.13/0.41 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.41 fof(f11,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (ifeq(c_in(c_PropLog_Opl_Oop_A_N_62(X0,X1,X2),c_PropLog_Othms(X3,X2),tc_PropLog_Opl(X2)),true,ifeq(c_in(X0,c_PropLog_Othms(X3,X2),tc_PropLog_Opl(X2)),true,c_in(X1,c_PropLog_Othms(X3,X2),tc_PropLog_Opl(X2)),true),true)=true)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.41 fof(f12,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (ifeq(c_in(X0,c_PropLog_Othms(c_insert(X1,X2,tc_PropLog_Opl(X3)),X3),tc_PropLog_Opl(X3)),true,c_in(c_PropLog_Opl_Oop_A_N_62(X1,X0,X3),c_PropLog_Othms(X2,X3),tc_PropLog_Opl(X3)),true)=true)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.41 fof(f13,plain,(
% 0.13/0.41 ![X0,X1,X2]: (ifeq(c_in(X0,X1,tc_PropLog_Opl(X2)),true,c_in(X0,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2)),true)=true)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.41 fof(f14,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (ifeq(c_in(X0,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2)),true,c_in(X0,c_PropLog_Othms(c_insert(X3,X1,tc_PropLog_Opl(X2)),X2),tc_PropLog_Opl(X2)),true)=true)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.41 fof(f15,plain,(
% 0.13/0.41 ![X0,X1,X2]: (c_in(X0,c_insert(X0,X1,X2),X2)=true)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.41 fof(f16,plain,(
% 0.13/0.41 c_in(v_p,c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a))=true),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.41 fof(f17,plain,(
% 0.13/0.41 c_in(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a))=true),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.41 fof(f18,plain,(
% 0.13/0.41 ~c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a))=true),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/0.41 fof(f19,definition,(
% 0.13/0.41 sF2_fnc=c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 0.13/0.41 fof(f20,definition,(
% 0.13/0.41 sF1_fnc=c_PropLog_Opl_Oop_A_N_62(sF2_fnc,c_PropLog_Opl_Ofalse,t_a)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.13/0.41 fof(f21,definition,(
% 0.13/0.41 sF3_fnc=c_PropLog_Othms(v_H,t_a)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 0.13/0.41 fof(f22,definition,(
% 0.13/0.41 sF4_fnc=tc_PropLog_Opl(t_a)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 0.13/0.41 fof(f23,definition,(
% 0.13/0.41 sF0_fnc=c_in(sF1_fnc,sF3_fnc,sF4_fnc)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.13/0.41 fof(f24,plain,(
% 0.13/0.41 ~sF0_fnc=true),
% 0.13/0.41 inference(definition_folding,[],[f18,f23,f22,f21,f20,f19])).
% 0.13/0.41 fof(f25,plain,(
% 0.13/0.41 c_in(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),sF3_fnc,tc_PropLog_Opl(t_a))=true),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f21,f17])).
% 0.13/0.41 fof(f26,plain,(
% 0.13/0.41 c_in(v_p,sF3_fnc,tc_PropLog_Opl(t_a))=true),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f21,f16])).
% 0.13/0.41 fof(f27,plain,(
% 0.13/0.41 c_in(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),sF3_fnc,sF4_fnc)=true),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f25])).
% 0.13/0.41 fof(f28,plain,(
% 0.13/0.41 c_in(v_p,sF3_fnc,sF4_fnc)=true),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f26])).
% 0.13/0.41 fof(f29,plain,(
% 0.13/0.41 ![X0]: (ifeq(c_in(sF2_fnc,c_PropLog_Othms(X0,t_a),tc_PropLog_Opl(t_a)),true,ifeq(c_in(v_p,c_PropLog_Othms(X0,t_a),tc_PropLog_Opl(t_a)),true,c_in(v_q,c_PropLog_Othms(X0,t_a),tc_PropLog_Opl(t_a)),true),true)=true)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f19,f11])).
% 0.13/0.41 fof(f31,plain,(
% 0.13/0.41 ![X0,X1,X2]: (ifeq(c_in(c_PropLog_Opl_Oop_A_N_62(X0,X1,t_a),c_PropLog_Othms(X2,t_a),sF4_fnc),true,ifeq(c_in(X0,c_PropLog_Othms(X2,t_a),tc_PropLog_Opl(t_a)),true,c_in(X1,c_PropLog_Othms(X2,t_a),tc_PropLog_Opl(t_a)),true),true)=true)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f22,f11])).
% 0.13/0.41 fof(f36,plain,(
% 0.13/0.41 ![X0]: (ifeq(c_in(sF2_fnc,c_PropLog_Othms(X0,t_a),sF4_fnc),true,ifeq(c_in(v_p,c_PropLog_Othms(X0,t_a),tc_PropLog_Opl(t_a)),true,c_in(v_q,c_PropLog_Othms(X0,t_a),tc_PropLog_Opl(t_a)),true),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f29])).
% 0.13/0.41 fof(f37,plain,(
% 0.13/0.41 ![X0]: (ifeq(c_in(sF2_fnc,c_PropLog_Othms(X0,t_a),sF4_fnc),true,ifeq(c_in(v_p,c_PropLog_Othms(X0,t_a),sF4_fnc),true,c_in(v_q,c_PropLog_Othms(X0,t_a),tc_PropLog_Opl(t_a)),true),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f36])).
% 0.13/0.41 fof(f38,plain,(
% 0.13/0.41 ![X0]: (ifeq(c_in(sF2_fnc,c_PropLog_Othms(X0,t_a),sF4_fnc),true,ifeq(c_in(v_p,c_PropLog_Othms(X0,t_a),sF4_fnc),true,c_in(v_q,c_PropLog_Othms(X0,t_a),sF4_fnc),true),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f37])).
% 0.13/0.41 fof(f44,plain,(
% 0.13/0.41 ![X0,X1,X2]: (ifeq(c_in(c_PropLog_Opl_Oop_A_N_62(X0,X1,t_a),c_PropLog_Othms(X2,t_a),sF4_fnc),true,ifeq(c_in(X0,c_PropLog_Othms(X2,t_a),sF4_fnc),true,c_in(X1,c_PropLog_Othms(X2,t_a),tc_PropLog_Opl(t_a)),true),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f31])).
% 0.13/0.41 fof(f45,plain,(
% 0.13/0.41 ![X0,X1,X2]: (ifeq(c_in(c_PropLog_Opl_Oop_A_N_62(X0,X1,t_a),c_PropLog_Othms(X2,t_a),sF4_fnc),true,ifeq(c_in(X0,c_PropLog_Othms(X2,t_a),sF4_fnc),true,c_in(X1,c_PropLog_Othms(X2,t_a),sF4_fnc),true),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f44])).
% 0.13/0.41 fof(f66,plain,(
% 0.13/0.41 ![X0]: (ifeq(c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(sF2_fnc,X0,tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),true,c_in(sF1_fnc,c_PropLog_Othms(X0,t_a),tc_PropLog_Opl(t_a)),true)=true)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f20,f12])).
% 0.13/0.41 fof(f74,plain,(
% 0.13/0.41 ![X0]: (ifeq(c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(sF2_fnc,X0,sF4_fnc),t_a),tc_PropLog_Opl(t_a)),true,c_in(sF1_fnc,c_PropLog_Othms(X0,t_a),tc_PropLog_Opl(t_a)),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f66])).
% 0.13/0.41 fof(f75,plain,(
% 0.13/0.41 ![X0]: (ifeq(c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(sF2_fnc,X0,sF4_fnc),t_a),sF4_fnc),true,c_in(sF1_fnc,c_PropLog_Othms(X0,t_a),tc_PropLog_Opl(t_a)),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f74])).
% 0.13/0.41 fof(f76,plain,(
% 0.13/0.41 ![X0]: (ifeq(c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(sF2_fnc,X0,sF4_fnc),t_a),sF4_fnc),true,c_in(sF1_fnc,c_PropLog_Othms(X0,t_a),sF4_fnc),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f75])).
% 0.13/0.41 fof(f92,plain,(
% 0.13/0.41 ![X0,X1]: (ifeq(c_in(X0,sF3_fnc,tc_PropLog_Opl(t_a)),true,c_in(X0,c_PropLog_Othms(c_insert(X1,v_H,tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),true)=true)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f21,f14])).
% 0.13/0.41 fof(f96,plain,(
% 0.13/0.41 ![X0,X1]: (ifeq(c_in(X0,sF3_fnc,sF4_fnc),true,c_in(X0,c_PropLog_Othms(c_insert(X1,v_H,tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f92])).
% 0.13/0.41 fof(f97,plain,(
% 0.13/0.41 ![X0,X1]: (ifeq(c_in(X0,sF3_fnc,sF4_fnc),true,c_in(X0,c_PropLog_Othms(c_insert(X1,v_H,sF4_fnc),t_a),tc_PropLog_Opl(t_a)),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f96])).
% 0.13/0.41 fof(f98,plain,(
% 0.13/0.41 ![X0,X1]: (ifeq(c_in(X0,sF3_fnc,sF4_fnc),true,c_in(X0,c_PropLog_Othms(c_insert(X1,v_H,sF4_fnc),t_a),sF4_fnc),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f97])).
% 0.13/0.41 fof(f149,plain,(
% 0.13/0.41 ![X0,X1,X2]: (ifeq(true,true,c_in(X0,c_PropLog_Othms(c_insert(X0,X1,tc_PropLog_Opl(X2)),X2),tc_PropLog_Opl(X2)),true)=true)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f15,f13])).
% 0.13/0.41 fof(f150,plain,(
% 0.13/0.41 ![X0,X1,X2]: (c_in(X0,c_PropLog_Othms(c_insert(X0,X1,tc_PropLog_Opl(X2)),X2),tc_PropLog_Opl(X2))=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f10,f149])).
% 0.13/0.41 fof(f151,plain,(
% 0.13/0.41 ![X0,X1]: (c_in(X0,c_PropLog_Othms(c_insert(X0,X1,sF4_fnc),t_a),tc_PropLog_Opl(t_a))=true)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f22,f150])).
% 0.13/0.41 fof(f162,plain,(
% 0.13/0.41 ![X0,X1]: (c_in(X0,c_PropLog_Othms(c_insert(X0,X1,sF4_fnc),t_a),sF4_fnc)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f22,f151])).
% 0.13/0.41 fof(f187,plain,(
% 0.13/0.41 ifeq(c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(sF2_fnc,v_H,sF4_fnc),t_a),sF4_fnc),true,c_in(sF1_fnc,sF3_fnc,sF4_fnc),true)=true),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f21,f76])).
% 0.13/0.41 fof(f188,plain,(
% 0.13/0.41 ifeq(c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(sF2_fnc,v_H,sF4_fnc),t_a),sF4_fnc),true,sF0_fnc,true)=true),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f23,f187])).
% 0.13/0.41 fof(f192,plain,(
% 0.13/0.41 ![X0]: (ifeq(true,true,ifeq(c_in(v_p,c_PropLog_Othms(c_insert(sF2_fnc,X0,sF4_fnc),t_a),sF4_fnc),true,c_in(v_q,c_PropLog_Othms(c_insert(sF2_fnc,X0,sF4_fnc),t_a),sF4_fnc),true),true)=true)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f162,f38])).
% 0.13/0.41 fof(f202,plain,(
% 0.13/0.41 ![X0]: (ifeq(c_in(v_p,c_PropLog_Othms(c_insert(sF2_fnc,X0,sF4_fnc),t_a),sF4_fnc),true,c_in(v_q,c_PropLog_Othms(c_insert(sF2_fnc,X0,sF4_fnc),t_a),sF4_fnc),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f10,f192])).
% 0.13/0.41 fof(f301,plain,(
% 0.13/0.41 ![X0]: (ifeq(true,true,c_in(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_insert(X0,v_H,sF4_fnc),t_a),sF4_fnc),true)=true)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f27,f98])).
% 0.13/0.41 fof(f303,plain,(
% 0.13/0.41 ![X0]: (ifeq(true,true,c_in(v_p,c_PropLog_Othms(c_insert(X0,v_H,sF4_fnc),t_a),sF4_fnc),true)=true)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f28,f98])).
% 0.13/0.41 fof(f307,plain,(
% 0.13/0.41 ![X0]: (c_in(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_insert(X0,v_H,sF4_fnc),t_a),sF4_fnc)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f10,f301])).
% 0.13/0.41 fof(f309,plain,(
% 0.13/0.41 ![X0]: (c_in(v_p,c_PropLog_Othms(c_insert(X0,v_H,sF4_fnc),t_a),sF4_fnc)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f10,f303])).
% 0.13/0.41 fof(f670,plain,(
% 0.13/0.41 ![X0]: (ifeq(true,true,ifeq(c_in(v_q,c_PropLog_Othms(c_insert(X0,v_H,sF4_fnc),t_a),sF4_fnc),true,c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(X0,v_H,sF4_fnc),t_a),sF4_fnc),true),true)=true)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f307,f45])).
% 0.13/0.41 fof(f682,plain,(
% 0.13/0.41 ![X0]: (ifeq(c_in(v_q,c_PropLog_Othms(c_insert(X0,v_H,sF4_fnc),t_a),sF4_fnc),true,c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(X0,v_H,sF4_fnc),t_a),sF4_fnc),true)=true)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f10,f670])).
% 0.13/0.41 fof(f788,plain,(
% 0.13/0.41 ifeq(true,true,c_in(v_q,c_PropLog_Othms(c_insert(sF2_fnc,v_H,sF4_fnc),t_a),sF4_fnc),true)=true),
% 0.13/0.42 inference(paramodulation,[status(thm)],[f309,f202])).
% 0.13/0.42 fof(f792,plain,(
% 0.13/0.42 c_in(v_q,c_PropLog_Othms(c_insert(sF2_fnc,v_H,sF4_fnc),t_a),sF4_fnc)=true),
% 0.13/0.42 inference(forward_demodulation,[status(thm)],[f10,f788])).
% 0.13/0.42 fof(f1814,plain,(
% 0.13/0.42 ifeq(true,true,c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(sF2_fnc,v_H,sF4_fnc),t_a),sF4_fnc),true)=true),
% 0.13/0.42 inference(paramodulation,[status(thm)],[f792,f682])).
% 0.13/0.42 fof(f1820,plain,(
% 0.13/0.42 ifeq(true,true,sF0_fnc,true)=true),
% 0.13/0.42 inference(backward_demodulation,[status(thm)],[f1821,f188])).
% 0.13/0.42 fof(f1821,plain,(
% 0.13/0.42 c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(sF2_fnc,v_H,sF4_fnc),t_a),sF4_fnc)=true),
% 0.13/0.42 inference(forward_demodulation,[status(thm)],[f10,f1814])).
% 0.13/0.42 fof(f1823,plain,(
% 0.13/0.42 sF0_fnc=true),
% 0.13/0.42 inference(forward_demodulation,[status(thm)],[f10,f1820])).
% 0.13/0.42 fof(f1824,plain,(
% 0.13/0.42 $false),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1823,f24])).
% 0.13/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.44 % Elapsed time: 0.068803 seconds
% 0.13/0.44 % CPU time: 0.378273 seconds
% 0.13/0.44 % Total memory used: 24.082 MB
% 0.13/0.44 % Net memory used: 23.760 MB
%------------------------------------------------------------------------------