%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL113-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 : n006.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:09:23 PM UTC 2026
% Result : Unsatisfiable 254.65s 32.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL113-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n006.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 00:05:42 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 254.65/32.54 % Refutation found
% 254.65/32.54 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 254.65/32.54 % SZS output start CNFRefutation for theBenchmark
% 254.65/32.54 fof(f1,axiom,(
% 254.65/32.54 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 254.65/32.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 254.65/32.54 fof(f2,axiom,(
% 254.65/32.54 (![X,Y]: (ifeq(is_a_theorem(implies(X,Y)),true,ifeq(is_a_theorem(X),true,is_a_theorem(Y),true),true) = true ))),
% 254.65/32.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 254.65/32.54 fof(f3,axiom,(
% 254.65/32.54 (![X,Y]: (is_a_theorem(implies(X,implies(Y,X))) = true ))),
% 254.65/32.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 254.65/32.54 fof(f4,axiom,(
% 254.65/32.54 (![X,Y,Z]: (is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) = true ))),
% 254.65/32.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 254.65/32.54 fof(f5,axiom,(
% 254.65/32.54 (![X,Y]: (is_a_theorem(implies(implies(implies(X,Y),Y),implies(implies(Y,X),X))) = true ))),
% 254.65/32.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 254.65/32.54 fof(f6,axiom,(
% 254.65/32.54 (![X,Y]: (is_a_theorem(implies(implies(not(X),not(Y)),implies(Y,X))) = true ))),
% 254.65/32.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 254.65/32.54 fof(f7,negated_conjecture,(
% 254.65/32.54 is_a_theorem(implies(implies(not(a),b),implies(not(b),a))) != true ),
% 254.65/32.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 254.65/32.54 fof(f8,plain,(
% 254.65/32.54 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 254.65/32.54 inference(cnf_transformation,[status(thm)],[f1])).
% 254.65/32.54 fof(f9,plain,(
% 254.65/32.54 ![X0,X1]: (ifeq(is_a_theorem(implies(X0,X1)),true,ifeq(is_a_theorem(X0),true,is_a_theorem(X1),true),true)=true)),
% 254.65/32.54 inference(cnf_transformation,[status(thm)],[f2])).
% 254.65/32.54 fof(f10,plain,(
% 254.65/32.54 ![X0,X1]: (is_a_theorem(implies(X0,implies(X1,X0)))=true)),
% 254.65/32.54 inference(cnf_transformation,[status(thm)],[f3])).
% 254.65/32.54 fof(f11,plain,(
% 254.65/32.54 ![X0,X1,X2]: (is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))=true)),
% 254.65/32.54 inference(cnf_transformation,[status(thm)],[f4])).
% 254.65/32.54 fof(f12,plain,(
% 254.65/32.54 ![X0,X1]: (is_a_theorem(implies(implies(implies(X0,X1),X1),implies(implies(X1,X0),X0)))=true)),
% 254.65/32.54 inference(cnf_transformation,[status(thm)],[f5])).
% 254.65/32.54 fof(f13,plain,(
% 254.65/32.54 ![X0,X1]: (is_a_theorem(implies(implies(not(X0),not(X1)),implies(X1,X0)))=true)),
% 254.65/32.55 inference(cnf_transformation,[status(thm)],[f6])).
% 254.65/32.55 fof(f14,plain,(
% 254.65/32.55 ~is_a_theorem(implies(implies(not(a),b),implies(not(b),a)))=true),
% 254.65/32.55 inference(cnf_transformation,[status(thm)],[f7])).
% 254.65/32.55 fof(f15,definition,(
% 254.65/32.55 sF3_fnc=not(a)),
% 254.65/32.55 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 254.65/32.55 fof(f16,definition,(
% 254.65/32.55 sF2_fnc=implies(sF3_fnc,b)),
% 254.65/32.55 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 254.65/32.55 fof(f17,definition,(
% 254.65/32.55 sF5_fnc=not(b)),
% 254.65/32.55 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 254.65/32.55 fof(f18,definition,(
% 254.65/32.55 sF4_fnc=implies(sF5_fnc,a)),
% 254.65/32.55 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 254.65/32.55 fof(f19,definition,(
% 254.65/32.55 sF1_fnc=implies(sF2_fnc,sF4_fnc)),
% 254.65/32.55 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 254.65/32.55 fof(f20,definition,(
% 254.65/32.55 sF0_fnc=is_a_theorem(sF1_fnc)),
% 254.65/32.55 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 254.65/32.55 fof(f21,plain,(
% 254.65/32.55 ~sF0_fnc=true),
% 254.65/32.55 inference(definition_folding,[],[f14,f20,f19,f18,f17,f16,f15])).
% 254.65/32.55 fof(f22,plain,(
% 254.65/32.55 is_a_theorem(implies(sF4_fnc,sF1_fnc))=true),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f19,f10])).
% 254.65/32.55 fof(f28,plain,(
% 254.65/32.55 ![X0]: (is_a_theorem(implies(sF2_fnc,implies(implies(b,X0),implies(sF3_fnc,X0))))=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f16,f11])).
% 254.65/32.55 fof(f32,plain,(
% 254.65/32.55 ![X0]: (is_a_theorem(implies(implies(sF2_fnc,X0),implies(implies(X0,sF4_fnc),sF1_fnc)))=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f19,f11])).
% 254.65/32.55 fof(f38,plain,(
% 254.65/32.55 ![X0]: (is_a_theorem(implies(implies(not(X0),sF5_fnc),implies(b,X0)))=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f17,f13])).
% 254.65/32.55 fof(f41,plain,(
% 254.65/32.55 is_a_theorem(implies(implies(not(a),not(sF5_fnc)),sF4_fnc))=true),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f18,f13])).
% 254.65/32.55 fof(f43,plain,(
% 254.65/32.55 is_a_theorem(implies(implies(sF3_fnc,not(sF5_fnc)),sF4_fnc))=true),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f15,f41])).
% 254.65/32.55 fof(f50,plain,(
% 254.65/32.55 ![X0,X1,X2]: (ifeq(true,true,ifeq(is_a_theorem(implies(X0,X1)),true,is_a_theorem(implies(implies(X1,X2),implies(X0,X2))),true),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f11,f9])).
% 254.65/32.55 fof(f51,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(true,true,ifeq(is_a_theorem(X0),true,is_a_theorem(implies(X1,X0)),true),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f10,f9])).
% 254.65/32.55 fof(f59,plain,(
% 254.65/32.55 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(implies(not(X0),not(X1)),implies(X1,X0)),X2)),true,ifeq(true,true,is_a_theorem(X2),true),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f13,f9])).
% 254.65/32.55 fof(f70,plain,(
% 254.65/32.55 ![X0]: (ifeq(is_a_theorem(implies(X0,sF1_fnc)),true,ifeq(is_a_theorem(X0),true,sF0_fnc,true),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f20,f9])).
% 254.65/32.55 fof(f77,plain,(
% 254.65/32.55 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(X0,X1)),true,is_a_theorem(implies(implies(X1,X2),implies(X0,X2))),true)=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f50])).
% 254.65/32.55 fof(f78,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(is_a_theorem(X0),true,is_a_theorem(implies(X1,X0)),true)=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f51])).
% 254.65/32.55 fof(f84,plain,(
% 254.65/32.55 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(implies(not(X0),not(X1)),implies(X1,X0)),X2)),true,is_a_theorem(X2),true)=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f59])).
% 254.65/32.55 fof(f93,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(true,true,ifeq(is_a_theorem(implies(implies(X0,X1),X1)),true,is_a_theorem(implies(implies(X1,X0),X0)),true),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f12,f9])).
% 254.65/32.55 fof(f95,plain,(
% 254.65/32.55 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(implies(implies(X0,X1),X1),implies(implies(X1,X0),X0)),X2)),true,ifeq(true,true,is_a_theorem(X2),true),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f12,f9])).
% 254.65/32.55 fof(f96,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(is_a_theorem(implies(implies(X0,X1),X1)),true,is_a_theorem(implies(implies(X1,X0),X0)),true)=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f93])).
% 254.65/32.55 fof(f97,plain,(
% 254.65/32.55 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(implies(implies(X0,X1),X1),implies(implies(X1,X0),X0)),X2)),true,is_a_theorem(X2),true)=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f95])).
% 254.65/32.55 fof(f124,plain,(
% 254.65/32.55 ![X0]: (ifeq(true,true,is_a_theorem(implies(X0,implies(sF4_fnc,sF1_fnc))),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f22,f78])).
% 254.65/32.55 fof(f127,plain,(
% 254.65/32.55 ![X0]: (ifeq(true,true,is_a_theorem(implies(X0,implies(implies(sF3_fnc,not(sF5_fnc)),sF4_fnc))),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f43,f78])).
% 254.65/32.55 fof(f151,plain,(
% 254.65/32.55 ![X0]: (is_a_theorem(implies(X0,implies(sF4_fnc,sF1_fnc)))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f124])).
% 254.65/32.55 fof(f154,plain,(
% 254.65/32.55 ![X0]: (is_a_theorem(implies(X0,implies(implies(sF3_fnc,not(sF5_fnc)),sF4_fnc)))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f127])).
% 254.65/32.55 fof(f451,plain,(
% 254.65/32.55 ![X0]: (ifeq(true,true,ifeq(is_a_theorem(implies(not(X0),sF5_fnc)),true,is_a_theorem(implies(b,X0)),true),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f38,f9])).
% 254.65/32.55 fof(f456,plain,(
% 254.65/32.55 ![X0]: (ifeq(is_a_theorem(implies(not(X0),sF5_fnc)),true,is_a_theorem(implies(b,X0)),true)=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f451])).
% 254.65/32.55 fof(f572,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(implies(implies(implies(b,X0),implies(sF3_fnc,X0)),X1),implies(sF2_fnc,X1))),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f28,f77])).
% 254.65/32.55 fof(f579,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(implies(implies(implies(X0,sF4_fnc),sF1_fnc),X1),implies(implies(sF2_fnc,X0),X1))),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f32,f77])).
% 254.65/32.55 fof(f605,plain,(
% 254.65/32.55 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2))),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f10,f77])).
% 254.65/32.55 fof(f633,plain,(
% 254.65/32.55 ![X0,X1]: (is_a_theorem(implies(implies(implies(implies(b,X0),implies(sF3_fnc,X0)),X1),implies(sF2_fnc,X1)))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f572])).
% 254.65/32.55 fof(f640,plain,(
% 254.65/32.55 ![X0,X1]: (is_a_theorem(implies(implies(implies(implies(X0,sF4_fnc),sF1_fnc),X1),implies(implies(sF2_fnc,X0),X1)))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f579])).
% 254.65/32.55 fof(f666,plain,(
% 254.65/32.55 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2)))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f605])).
% 254.65/32.55 fof(f820,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(not(X0),implies(X0,X1))),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f666,f84])).
% 254.65/32.55 fof(f881,plain,(
% 254.65/32.55 ![X0,X1]: (is_a_theorem(implies(not(X0),implies(X0,X1)))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f820])).
% 254.65/32.55 fof(f1079,plain,(
% 254.65/32.55 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(X0),X2))),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f881,f77])).
% 254.65/32.55 fof(f1089,plain,(
% 254.65/32.55 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(X0),X2)))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f1079])).
% 254.65/32.55 fof(f2367,plain,(
% 254.65/32.55 ![X0]: (ifeq(true,true,is_a_theorem(implies(implies(implies(sF4_fnc,sF1_fnc),X0),X0)),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f151,f96])).
% 254.65/32.55 fof(f2414,plain,(
% 254.65/32.55 ![X0]: (is_a_theorem(implies(implies(implies(sF4_fnc,sF1_fnc),X0),X0))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f2367])).
% 254.65/32.55 fof(f2543,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(is_a_theorem(implies(implies(implies(implies(sF4_fnc,sF1_fnc),X0),X0),X1)),true,ifeq(true,true,is_a_theorem(X1),true),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f2414,f9])).
% 254.65/32.55 fof(f2554,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(is_a_theorem(implies(implies(implies(implies(sF4_fnc,sF1_fnc),X0),X0),X1)),true,is_a_theorem(X1),true)=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f2543])).
% 254.65/32.55 fof(f2771,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(X0,implies(implies(X0,X1),X1))),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f666,f97])).
% 254.65/32.55 fof(f2881,plain,(
% 254.65/32.55 ![X0,X1]: (is_a_theorem(implies(X0,implies(implies(X0,X1),X1)))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f2771])).
% 254.65/32.55 fof(f3222,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(true,true,ifeq(is_a_theorem(X0),true,is_a_theorem(implies(implies(X0,X1),X1)),true),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f2881,f9])).
% 254.65/32.55 fof(f3243,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(is_a_theorem(X0),true,is_a_theorem(implies(implies(X0,X1),X1)),true)=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f3222])).
% 254.65/32.55 fof(f5873,plain,(
% 254.65/32.55 ![X0]: (ifeq(true,true,is_a_theorem(implies(implies(implies(implies(sF3_fnc,not(sF5_fnc)),sF4_fnc),X0),X0)),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f154,f96])).
% 254.65/32.55 fof(f5909,plain,(
% 254.65/32.55 ![X0]: (is_a_theorem(implies(implies(implies(implies(sF3_fnc,not(sF5_fnc)),sF4_fnc),X0),X0))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f5873])).
% 254.65/32.55 fof(f10280,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(not(not(X0)),implies(X1,X0))),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f1089,f84])).
% 254.65/32.55 fof(f10336,plain,(
% 254.65/32.55 ![X0,X1]: (is_a_theorem(implies(not(not(X0)),implies(X1,X0)))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f10280])).
% 254.65/32.55 fof(f11241,plain,(
% 254.65/32.55 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(not(X1)),X2))),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f10336,f77])).
% 254.65/32.55 fof(f11268,plain,(
% 254.65/32.55 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(not(X1)),X2)))=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f11241])).
% 254.65/32.55 fof(f20520,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(true,true,ifeq(is_a_theorem(implies(implies(implies(b,X0),implies(sF3_fnc,X0)),X1)),true,is_a_theorem(implies(sF2_fnc,X1)),true),true)=true)),
% 254.65/32.55 inference(paramodulation,[status(thm)],[f633,f9])).
% 254.65/32.55 fof(f20553,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(is_a_theorem(implies(implies(implies(b,X0),implies(sF3_fnc,X0)),X1)),true,is_a_theorem(implies(sF2_fnc,X1)),true)=true)),
% 254.65/32.55 inference(forward_demodulation,[status(thm)],[f8,f20520])).
% 254.65/32.55 fof(f21165,plain,(
% 254.65/32.55 ![X0,X1]: (ifeq(true,true,ifeq(is_a_theorem(implies(implies(implies(X0,sF4_fnc),sF1_fnc),X1)),true,is_a_theorem(implies(implies(sF2_fnc,X0),X1)),true),true)=true)),
% 89.02/33.14 inference(paramodulation,[status(thm)],[f640,f9])).
% 89.02/33.14 fof(f21198,plain,(
% 89.02/33.14 ![X0,X1]: (ifeq(is_a_theorem(implies(implies(implies(X0,sF4_fnc),sF1_fnc),X1)),true,is_a_theorem(implies(implies(sF2_fnc,X0),X1)),true)=true)),
% 89.02/33.14 inference(forward_demodulation,[status(thm)],[f8,f21165])).
% 89.02/33.14 fof(f276180,plain,(
% 89.02/33.14 ifeq(true,true,is_a_theorem(implies(implies(sF2_fnc,implies(sF3_fnc,not(sF5_fnc))),sF1_fnc)),true)=true),
% 89.02/33.14 inference(paramodulation,[status(thm)],[f5909,f21198])).
% 89.02/33.14 fof(f276798,plain,(
% 89.02/33.14 is_a_theorem(implies(implies(sF2_fnc,implies(sF3_fnc,not(sF5_fnc))),sF1_fnc))=true),
% 89.02/33.14 inference(forward_demodulation,[status(thm)],[f8,f276180])).
% 89.02/33.14 fof(f703377,plain,(
% 89.02/33.14 ![X0]: (ifeq(true,true,is_a_theorem(implies(not(not(X0)),X0)),true)=true)),
% 89.02/33.14 inference(paramodulation,[status(thm)],[f11268,f2554])).
% 89.02/33.14 fof(f705299,plain,(
% 89.02/33.14 ![X0]: (is_a_theorem(implies(not(not(X0)),X0))=true)),
% 89.02/33.14 inference(forward_demodulation,[status(thm)],[f8,f703377])).
% 89.02/33.14 fof(f706412,plain,(
% 89.02/33.14 ifeq(true,true,is_a_theorem(implies(b,not(sF5_fnc))),true)=true),
% 89.02/33.14 inference(paramodulation,[status(thm)],[f705299,f456])).
% 89.02/33.14 fof(f706929,plain,(
% 89.02/33.14 is_a_theorem(implies(b,not(sF5_fnc)))=true),
% 89.02/33.14 inference(forward_demodulation,[status(thm)],[f8,f706412])).
% 89.02/33.14 fof(f707188,plain,(
% 89.02/33.14 ![X0]: (ifeq(true,true,is_a_theorem(implies(implies(implies(b,not(sF5_fnc)),X0),X0)),true)=true)),
% 89.02/33.14 inference(paramodulation,[status(thm)],[f706929,f3243])).
% 89.02/33.14 fof(f707223,plain,(
% 89.02/33.14 ![X0]: (is_a_theorem(implies(implies(implies(b,not(sF5_fnc)),X0),X0))=true)),
% 89.02/33.14 inference(forward_demodulation,[status(thm)],[f8,f707188])).
% 89.02/33.14 fof(f778639,plain,(
% 89.02/33.14 ifeq(true,true,is_a_theorem(implies(sF2_fnc,implies(sF3_fnc,not(sF5_fnc)))),true)=true),
% 89.02/33.14 inference(paramodulation,[status(thm)],[f707223,f20553])).
% 89.02/33.14 fof(f779233,plain,(
% 89.02/33.14 is_a_theorem(implies(sF2_fnc,implies(sF3_fnc,not(sF5_fnc))))=true),
% 89.02/33.14 inference(forward_demodulation,[status(thm)],[f8,f778639])).
% 89.02/33.14 fof(f779427,plain,(
% 89.02/33.14 ifeq(is_a_theorem(implies(implies(sF2_fnc,implies(sF3_fnc,not(sF5_fnc))),sF1_fnc)),true,ifeq(true,true,sF0_fnc,true),true)=true),
% 89.02/33.14 inference(paramodulation,[status(thm)],[f779233,f70])).
% 89.02/33.14 fof(f779446,plain,(
% 89.02/33.14 ifeq(true,true,ifeq(true,true,sF0_fnc,true),true)=true),
% 89.02/33.14 inference(forward_demodulation,[status(thm)],[f276798,f779427])).
% 89.02/33.14 fof(f779447,plain,(
% 89.02/33.14 ifeq(true,true,sF0_fnc,true)=true),
% 89.02/33.14 inference(forward_demodulation,[status(thm)],[f8,f779446])).
% 89.02/33.14 fof(f779448,plain,(
% 89.02/33.14 sF0_fnc=true),
% 89.02/33.14 inference(forward_demodulation,[status(thm)],[f8,f779447])).
% 89.02/33.14 fof(f779449,plain,(
% 89.02/33.14 $false),
% 89.02/33.14 inference(forward_subsumption_resolution,[status(thm)],[f779448,f21])).
% 89.02/33.14 % SZS output end CNFRefutation for theBenchmark.p
% 211.80/33.21 % Elapsed time: 32.811297 seconds
% 211.80/33.21 % CPU time: 258.736627 seconds
% 211.80/33.21 % Total memory used: 1.799 GB
% 211.80/33.21 % Net memory used: 1.762 GB
%------------------------------------------------------------------------------