%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL195-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:33 PM UTC 2026
% Result : Unsatisfiable 220.63s 28.25s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL195-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n014.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 00:10:06 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 220.63/28.25 % Refutation found
% 220.63/28.25 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 220.63/28.25 % SZS output start CNFRefutation for theBenchmark
% 220.63/28.25 fof(f1,axiom,(
% 220.63/28.25 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 220.63/28.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.63/28.25 fof(f2,axiom,(
% 220.63/28.25 (![A]: (axiom(implies(or(A,A),A)) = true ))),
% 220.63/28.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.63/28.25 fof(f3,axiom,(
% 220.63/28.25 (![A,B]: (axiom(implies(A,or(B,A))) = true ))),
% 220.63/28.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.63/28.25 fof(f4,axiom,(
% 220.63/28.25 (![A,B]: (axiom(implies(or(A,B),or(B,A))) = true ))),
% 220.63/28.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.63/28.25 fof(f5,axiom,(
% 220.63/28.25 (![A,B,C]: (axiom(implies(or(A,or(B,C)),or(B,or(A,C)))) = true ))),
% 220.63/28.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.63/28.25 fof(f6,axiom,(
% 220.63/28.25 (![A,B,C]: (axiom(implies(implies(A,B),implies(or(C,A),or(C,B)))) = true ))),
% 220.63/28.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.63/28.25 fof(f7,axiom,(
% 220.63/28.25 (![X,Y]: (implies(X,Y) = or(not(X),Y) ))),
% 220.63/28.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.63/28.25 fof(f8,axiom,(
% 220.63/28.25 (![X]: (ifeq(axiom(X),true,theorem(X),true) = true ))),
% 220.63/28.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.63/28.25 fof(f9,axiom,(
% 220.63/28.25 (![Y,X]: (ifeq(theorem(implies(Y,X)),true,ifeq(theorem(Y),true,theorem(X),true),true) = true ))),
% 220.63/28.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.63/28.25 fof(f10,negated_conjecture,(
% 220.63/28.25 theorem(implies(implies(q,r),implies(or(q,p),or(r,p)))) != true ),
% 220.63/28.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.63/28.25 fof(f11,plain,(
% 220.63/28.25 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 220.63/28.25 inference(cnf_transformation,[status(thm)],[f1])).
% 220.63/28.25 fof(f12,plain,(
% 220.63/28.25 ![X0]: (axiom(implies(or(X0,X0),X0))=true)),
% 220.63/28.25 inference(cnf_transformation,[status(thm)],[f2])).
% 220.63/28.25 fof(f13,plain,(
% 220.63/28.25 ![X0,X1]: (axiom(implies(X0,or(X1,X0)))=true)),
% 220.63/28.25 inference(cnf_transformation,[status(thm)],[f3])).
% 220.63/28.25 fof(f14,plain,(
% 220.63/28.25 ![X0,X1]: (axiom(implies(or(X0,X1),or(X1,X0)))=true)),
% 220.63/28.25 inference(cnf_transformation,[status(thm)],[f4])).
% 220.63/28.25 fof(f15,plain,(
% 220.63/28.25 ![X0,X1,X2]: (axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2))))=true)),
% 220.63/28.26 inference(cnf_transformation,[status(thm)],[f5])).
% 220.63/28.26 fof(f16,plain,(
% 220.63/28.26 ![X0,X1,X2]: (axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1))))=true)),
% 220.63/28.26 inference(cnf_transformation,[status(thm)],[f6])).
% 220.63/28.26 fof(f17,plain,(
% 220.63/28.26 ![X0,X1]: (implies(X0,X1)=or(not(X0),X1))),
% 220.63/28.26 inference(cnf_transformation,[status(thm)],[f7])).
% 220.63/28.26 fof(f18,plain,(
% 220.63/28.26 ![X0]: (ifeq(axiom(X0),true,theorem(X0),true)=true)),
% 220.63/28.26 inference(cnf_transformation,[status(thm)],[f8])).
% 220.63/28.26 fof(f19,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(theorem(implies(X0,X1)),true,ifeq(theorem(X0),true,theorem(X1),true),true)=true)),
% 220.63/28.26 inference(cnf_transformation,[status(thm)],[f9])).
% 220.63/28.26 fof(f20,plain,(
% 220.63/28.26 ~theorem(implies(implies(q,r),implies(or(q,p),or(r,p))))=true),
% 220.63/28.26 inference(cnf_transformation,[status(thm)],[f10])).
% 220.63/28.26 fof(f21,definition,(
% 220.63/28.26 sF2_fnc=implies(q,r)),
% 220.63/28.26 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 220.63/28.26 fof(f22,definition,(
% 220.63/28.26 sF4_fnc=or(q,p)),
% 220.63/28.26 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 220.63/28.26 fof(f23,definition,(
% 220.63/28.26 sF5_fnc=or(r,p)),
% 220.63/28.26 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 220.63/28.26 fof(f24,definition,(
% 220.63/28.26 sF3_fnc=implies(sF4_fnc,sF5_fnc)),
% 220.63/28.26 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 220.63/28.26 fof(f25,definition,(
% 220.63/28.26 sF1_fnc=implies(sF2_fnc,sF3_fnc)),
% 220.63/28.26 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 220.63/28.26 fof(f26,definition,(
% 220.63/28.26 sF0_fnc=theorem(sF1_fnc)),
% 220.63/28.26 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 220.63/28.26 fof(f27,plain,(
% 220.63/28.26 ~sF0_fnc=true),
% 220.63/28.26 inference(definition_folding,[],[f20,f26,f25,f24,f23,f22,f21])).
% 220.63/28.26 fof(f29,plain,(
% 220.63/28.26 ![X0,X1]: (axiom(implies(X0,implies(X1,X0)))=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f17,f13])).
% 220.63/28.26 fof(f30,plain,(
% 220.63/28.26 axiom(implies(p,sF5_fnc))=true),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f23,f13])).
% 220.63/28.26 fof(f41,plain,(
% 220.63/28.26 ![X0,X1,X2]: (axiom(implies(implies(X0,or(X1,X2)),or(X1,or(not(X0),X2))))=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f17,f15])).
% 220.63/28.26 fof(f42,plain,(
% 220.63/28.26 ![X0,X1,X2]: (axiom(implies(or(X0,implies(X1,X2)),or(not(X1),or(X0,X2))))=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f17,f15])).
% 220.63/28.26 fof(f49,plain,(
% 220.63/28.26 ![X0,X1,X2]: (axiom(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2))))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f17,f41])).
% 220.63/28.26 fof(f50,plain,(
% 220.63/28.26 ![X0,X1,X2]: (axiom(implies(or(X0,implies(X1,X2)),implies(X1,or(X0,X2))))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f17,f42])).
% 220.63/28.26 fof(f56,plain,(
% 220.63/28.26 ![X0,X1,X2]: (axiom(implies(implies(X0,X1),implies(implies(X2,X0),or(not(X2),X1))))=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f17,f16])).
% 220.63/28.26 fof(f62,plain,(
% 220.63/28.26 ![X0,X1,X2]: (axiom(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1))))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f17,f56])).
% 220.63/28.26 fof(f86,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(true,true,theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f16,f18])).
% 220.63/28.26 fof(f89,plain,(
% 220.63/28.26 ifeq(true,true,theorem(implies(p,sF5_fnc)),true)=true),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f30,f18])).
% 220.63/28.26 fof(f96,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(true,true,theorem(implies(or(X0,X1),or(X1,X0))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f14,f18])).
% 220.63/28.26 fof(f97,plain,(
% 220.63/28.26 ![X0]: (ifeq(true,true,theorem(implies(or(X0,X0),X0)),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f12,f18])).
% 220.63/28.26 fof(f98,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(true,true,theorem(implies(X0,implies(X1,X0))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f29,f18])).
% 220.63/28.26 fof(f99,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(true,true,theorem(implies(X0,or(X1,X0))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f13,f18])).
% 220.63/28.26 fof(f105,plain,(
% 220.63/28.26 ![X0,X1,X2]: (theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1))))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f86])).
% 220.63/28.26 fof(f108,plain,(
% 220.63/28.26 theorem(implies(p,sF5_fnc))=true),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f89])).
% 220.63/28.26 fof(f115,plain,(
% 220.63/28.26 ![X0,X1]: (theorem(implies(or(X0,X1),or(X1,X0)))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f96])).
% 220.63/28.26 fof(f116,plain,(
% 220.63/28.26 ![X0]: (theorem(implies(or(X0,X0),X0))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f97])).
% 220.63/28.26 fof(f117,plain,(
% 220.63/28.26 ![X0,X1]: (theorem(implies(X0,implies(X1,X0)))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f98])).
% 220.63/28.26 fof(f118,plain,(
% 220.63/28.26 ![X0,X1]: (theorem(implies(X0,or(X1,X0)))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f99])).
% 220.63/28.26 fof(f148,plain,(
% 220.63/28.26 ![X0]: (ifeq(theorem(implies(X0,sF1_fnc)),true,ifeq(theorem(X0),true,sF0_fnc,true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f26,f19])).
% 220.63/28.26 fof(f220,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(theorem(implies(implies(or(X0,X0),X0),X1)),true,ifeq(true,true,theorem(X1),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f116,f19])).
% 220.63/28.26 fof(f223,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(theorem(implies(implies(or(X0,X0),X0),X1)),true,theorem(X1),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f220])).
% 220.63/28.26 fof(f228,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(true,true,ifeq(theorem(X0),true,theorem(implies(X1,X0)),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f117,f19])).
% 220.63/28.26 fof(f232,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(theorem(X0),true,theorem(implies(X1,X0)),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f228])).
% 220.63/28.26 fof(f238,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(true,true,ifeq(theorem(X0),true,theorem(or(X1,X0)),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f118,f19])).
% 220.63/28.26 fof(f240,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(theorem(implies(implies(X0,or(X1,X0)),X2)),true,ifeq(true,true,theorem(X2),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f118,f19])).
% 220.63/28.26 fof(f242,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(theorem(X0),true,theorem(or(X1,X0)),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f238])).
% 220.63/28.26 fof(f243,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(theorem(implies(implies(X0,or(X1,X0)),X2)),true,theorem(X2),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f240])).
% 220.63/28.26 fof(f251,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f115,f19])).
% 220.63/28.26 fof(f253,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(theorem(implies(implies(or(X0,X1),or(X1,X0)),X2)),true,ifeq(true,true,theorem(X2),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f115,f19])).
% 220.63/28.26 fof(f255,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f251])).
% 220.63/28.26 fof(f256,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(theorem(implies(implies(or(X0,X1),or(X1,X0)),X2)),true,theorem(X2),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f253])).
% 220.63/28.26 fof(f271,plain,(
% 220.63/28.26 ![X0,X1,X2]: (axiom(implies(implies(X0,implies(X1,X2)),or(not(X1),implies(X0,X2))))=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f17,f49])).
% 220.63/28.26 fof(f278,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(true,true,theorem(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2)))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f49,f18])).
% 220.63/28.26 fof(f279,plain,(
% 220.63/28.26 ![X0,X1,X2]: (axiom(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2))))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f17,f271])).
% 220.63/28.26 fof(f281,plain,(
% 220.63/28.26 ![X0,X1,X2]: (theorem(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2))))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f278])).
% 220.63/28.26 fof(f289,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(true,true,theorem(implies(or(X0,implies(X1,X2)),implies(X1,or(X0,X2)))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f50,f18])).
% 220.63/28.26 fof(f292,plain,(
% 220.63/28.26 ![X0,X1,X2]: (theorem(implies(or(X0,implies(X1,X2)),implies(X1,or(X0,X2))))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f289])).
% 220.63/28.26 fof(f356,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(true,true,theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f62,f18])).
% 220.63/28.26 fof(f357,plain,(
% 220.63/28.26 ![X0,X1,X2]: (theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1))))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f356])).
% 220.63/28.26 fof(f419,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(true,true,ifeq(theorem(implies(X0,X1)),true,theorem(implies(or(X2,X0),or(X2,X1))),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f105,f19])).
% 220.63/28.26 fof(f425,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(theorem(implies(X0,X1)),true,theorem(implies(or(X2,X0),or(X2,X1))),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f419])).
% 220.63/28.26 fof(f2782,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(true,true,theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f279,f18])).
% 220.63/28.26 fof(f2783,plain,(
% 220.63/28.26 ![X0,X1,X2]: (theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2))))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f2782])).
% 220.63/28.26 fof(f3323,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(true,true,ifeq(theorem(implies(X0,or(X1,X2))),true,theorem(or(X1,implies(X0,X2))),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f281,f19])).
% 220.63/28.26 fof(f3341,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(theorem(implies(X0,or(X1,X2))),true,theorem(or(X1,implies(X0,X2))),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f3323])).
% 220.63/28.26 fof(f3824,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(true,true,ifeq(theorem(or(X0,implies(X1,X2))),true,theorem(implies(X1,or(X0,X2))),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f292,f19])).
% 220.63/28.26 fof(f3839,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(theorem(or(X0,implies(X1,X2))),true,theorem(implies(X1,or(X0,X2))),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f3824])).
% 220.63/28.26 fof(f5693,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(true,true,theorem(implies(implies(X0,or(X1,X2)),implies(X0,or(X2,X1)))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f357,f256])).
% 220.63/28.26 fof(f5694,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(true,true,theorem(implies(implies(X0,or(X1,X1)),implies(X0,X1))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f357,f223])).
% 220.63/28.26 fof(f5706,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(true,true,ifeq(theorem(implies(X0,X1)),true,theorem(implies(implies(X2,X0),implies(X2,X1))),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f357,f19])).
% 220.63/28.26 fof(f5721,plain,(
% 220.63/28.26 ![X0,X1,X2]: (theorem(implies(implies(X0,or(X1,X2)),implies(X0,or(X2,X1))))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f5693])).
% 220.63/28.26 fof(f5722,plain,(
% 220.63/28.26 ![X0,X1]: (theorem(implies(implies(X0,or(X1,X1)),implies(X0,X1)))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f5694])).
% 220.63/28.26 fof(f5724,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(theorem(implies(X0,X1)),true,theorem(implies(implies(X2,X0),implies(X2,X1))),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f5706])).
% 220.63/28.26 fof(f7794,plain,(
% 220.63/28.26 ![X0]: (ifeq(true,true,theorem(implies(or(X0,p),or(X0,sF5_fnc))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f108,f425])).
% 220.63/28.26 fof(f7907,plain,(
% 220.63/28.26 ![X0]: (theorem(implies(or(X0,p),or(X0,sF5_fnc)))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f7794])).
% 220.63/28.26 fof(f10558,plain,(
% 220.63/28.26 theorem(implies(sF4_fnc,or(q,sF5_fnc)))=true),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f22,f7907])).
% 220.63/28.26 fof(f49973,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(true,true,ifeq(theorem(implies(X0,implies(X1,X2))),true,theorem(implies(X1,implies(X0,X2))),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f2783,f19])).
% 220.63/28.26 fof(f50014,plain,(
% 220.63/28.26 ![X0,X1,X2]: (ifeq(theorem(implies(X0,implies(X1,X2))),true,theorem(implies(X1,implies(X0,X2))),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f49973])).
% 220.63/28.26 fof(f53071,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(true,true,ifeq(theorem(implies(X0,or(X1,X1))),true,theorem(implies(X0,X1)),true),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f5722,f19])).
% 220.63/28.26 fof(f53113,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(theorem(implies(X0,or(X1,X1))),true,theorem(implies(X0,X1)),true)=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f53071])).
% 220.63/28.26 fof(f54743,plain,(
% 220.63/28.26 ifeq(true,true,theorem(or(q,implies(sF4_fnc,sF5_fnc))),true)=true),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f10558,f3341])).
% 220.63/28.26 fof(f55002,plain,(
% 220.63/28.26 theorem(or(q,implies(sF4_fnc,sF5_fnc)))=true),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f54743])).
% 220.63/28.26 fof(f55003,plain,(
% 220.63/28.26 theorem(or(q,sF3_fnc))=true),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f24,f55002])).
% 220.63/28.26 fof(f56035,plain,(
% 220.63/28.26 ![X0]: (ifeq(true,true,theorem(implies(X0,or(q,sF3_fnc))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f55003,f232])).
% 220.63/28.26 fof(f56045,plain,(
% 220.63/28.26 ![X0]: (theorem(implies(X0,or(q,sF3_fnc)))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f56035])).
% 220.63/28.26 fof(f56559,plain,(
% 220.63/28.26 ![X0]: (ifeq(true,true,theorem(or(q,implies(X0,sF3_fnc))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f56045,f3341])).
% 220.63/28.26 fof(f56624,plain,(
% 220.63/28.26 ![X0]: (theorem(or(q,implies(X0,sF3_fnc)))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f56559])).
% 220.63/28.26 fof(f57674,plain,(
% 220.63/28.26 theorem(or(q,sF1_fnc))=true),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f25,f56624])).
% 220.63/28.26 fof(f57732,plain,(
% 220.63/28.26 ifeq(true,true,theorem(or(sF1_fnc,q)),true)=true),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f57674,f255])).
% 220.63/28.26 fof(f57767,plain,(
% 220.63/28.26 theorem(or(sF1_fnc,q))=true),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f57732])).
% 220.63/28.26 fof(f71610,plain,(
% 220.63/28.26 ![X0,X1]: (ifeq(true,true,theorem(implies(X0,or(X0,X1))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f5721,f243])).
% 220.63/28.26 fof(f71682,plain,(
% 220.63/28.26 ![X0,X1]: (theorem(implies(X0,or(X0,X1)))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f71610])).
% 220.63/28.26 fof(f73345,plain,(
% 220.63/28.26 theorem(implies(r,sF5_fnc))=true),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f23,f71682])).
% 220.63/28.26 fof(f73574,plain,(
% 220.63/28.26 ![X0]: (ifeq(true,true,theorem(or(X0,implies(r,sF5_fnc))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f73345,f242])).
% 220.63/28.26 fof(f73588,plain,(
% 220.63/28.26 ![X0]: (theorem(or(X0,implies(r,sF5_fnc)))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f73574])).
% 220.63/28.26 fof(f77844,plain,(
% 220.63/28.26 ![X0]: (ifeq(true,true,theorem(implies(r,or(X0,sF5_fnc))),true)=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f73588,f3839])).
% 220.63/28.26 fof(f77890,plain,(
% 220.63/28.26 ![X0]: (theorem(implies(r,or(X0,sF5_fnc)))=true)),
% 220.63/28.26 inference(forward_demodulation,[status(thm)],[f11,f77844])).
% 220.63/28.26 fof(f81815,plain,(
% 220.63/28.26 ![X0]: (theorem(implies(r,implies(X0,sF5_fnc)))=true)),
% 220.63/28.26 inference(paramodulation,[status(thm)],[f17,f77890])).
% 140.19/28.79 fof(f87186,plain,(
% 140.19/28.79 theorem(implies(r,sF3_fnc))=true),
% 140.19/28.79 inference(paramodulation,[status(thm)],[f24,f81815])).
% 140.19/28.79 fof(f87253,plain,(
% 140.19/28.79 ![X0]: (ifeq(true,true,theorem(implies(implies(X0,r),implies(X0,sF3_fnc))),true)=true)),
% 140.19/28.79 inference(paramodulation,[status(thm)],[f87186,f5724])).
% 140.19/28.79 fof(f87299,plain,(
% 140.19/28.79 ![X0]: (theorem(implies(implies(X0,r),implies(X0,sF3_fnc)))=true)),
% 140.19/28.79 inference(forward_demodulation,[status(thm)],[f11,f87253])).
% 140.19/28.79 fof(f217119,plain,(
% 140.19/28.79 theorem(implies(sF2_fnc,implies(q,sF3_fnc)))=true),
% 140.19/28.79 inference(paramodulation,[status(thm)],[f21,f87299])).
% 140.19/28.79 fof(f585658,plain,(
% 140.19/28.79 ifeq(true,true,theorem(implies(q,implies(sF2_fnc,sF3_fnc))),true)=true),
% 140.19/28.79 inference(paramodulation,[status(thm)],[f217119,f50014])).
% 140.19/28.79 fof(f586255,plain,(
% 140.19/28.79 theorem(implies(q,implies(sF2_fnc,sF3_fnc)))=true),
% 140.19/28.79 inference(forward_demodulation,[status(thm)],[f11,f585658])).
% 140.19/28.79 fof(f586256,plain,(
% 140.19/28.79 theorem(implies(q,sF1_fnc))=true),
% 140.19/28.79 inference(forward_demodulation,[status(thm)],[f25,f586255])).
% 140.19/28.79 fof(f587606,plain,(
% 140.19/28.79 ![X0]: (ifeq(true,true,theorem(implies(or(X0,q),or(X0,sF1_fnc))),true)=true)),
% 140.19/28.79 inference(paramodulation,[status(thm)],[f586256,f425])).
% 140.19/28.79 fof(f587709,plain,(
% 140.19/28.79 ![X0]: (theorem(implies(or(X0,q),or(X0,sF1_fnc)))=true)),
% 140.19/28.79 inference(forward_demodulation,[status(thm)],[f11,f587606])).
% 140.19/28.79 fof(f807823,plain,(
% 140.19/28.79 ifeq(true,true,theorem(implies(or(sF1_fnc,q),sF1_fnc)),true)=true),
% 140.19/28.79 inference(paramodulation,[status(thm)],[f587709,f53113])).
% 140.19/28.79 fof(f807948,plain,(
% 140.19/28.79 theorem(implies(or(sF1_fnc,q),sF1_fnc))=true),
% 140.19/28.79 inference(forward_demodulation,[status(thm)],[f11,f807823])).
% 140.19/28.79 fof(f807964,plain,(
% 140.19/28.79 ifeq(true,true,ifeq(theorem(or(sF1_fnc,q)),true,sF0_fnc,true),true)=true),
% 140.19/28.79 inference(paramodulation,[status(thm)],[f807948,f148])).
% 140.19/28.79 fof(f808085,plain,(
% 140.19/28.79 ifeq(theorem(or(sF1_fnc,q)),true,sF0_fnc,true)=true),
% 140.19/28.79 inference(forward_demodulation,[status(thm)],[f11,f807964])).
% 140.19/28.79 fof(f808086,plain,(
% 140.19/28.79 ifeq(true,true,sF0_fnc,true)=true),
% 140.19/28.79 inference(forward_demodulation,[status(thm)],[f57767,f808085])).
% 140.19/28.79 fof(f808087,plain,(
% 140.19/28.79 sF0_fnc=true),
% 140.19/28.79 inference(forward_demodulation,[status(thm)],[f11,f808086])).
% 140.19/28.79 fof(f808088,plain,(
% 140.19/28.79 $false),
% 140.19/28.79 inference(forward_subsumption_resolution,[status(thm)],[f808087,f27])).
% 140.19/28.79 % SZS output end CNFRefutation for theBenchmark.p
% 28.33/28.84 % Elapsed time: 28.415475 seconds
% 28.33/28.84 % CPU time: 224.885176 seconds
% 28.33/28.84 % Total memory used: 2.081 GB
% 28.33/28.84 % Net memory used: 2.043 GB
%------------------------------------------------------------------------------