%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL231-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:40 PM UTC 2026
% Result : Unsatisfiable 154.08s 19.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL231-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.39 % Computer : n015.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 21 00:16:36 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.40 % Drodi V4.1.1
% 154.08/19.93 % Refutation found
% 154.08/19.93 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 154.08/19.93 % SZS output start CNFRefutation for theBenchmark
% 154.08/19.93 fof(f1,axiom,(
% 154.08/19.93 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 154.08/19.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.08/19.93 fof(f2,axiom,(
% 154.08/19.93 (![A]: (axiom(implies(or(A,A),A)) = true ))),
% 154.08/19.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.08/19.93 fof(f3,axiom,(
% 154.08/19.93 (![A,B]: (axiom(implies(A,or(B,A))) = true ))),
% 154.08/19.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.08/19.93 fof(f4,axiom,(
% 154.08/19.93 (![A,B]: (axiom(implies(or(A,B),or(B,A))) = true ))),
% 154.08/19.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.08/19.93 fof(f5,axiom,(
% 154.08/19.93 (![A,B,C]: (axiom(implies(or(A,or(B,C)),or(B,or(A,C)))) = true ))),
% 154.08/19.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.08/19.93 fof(f6,axiom,(
% 154.08/19.93 (![A,B,C]: (axiom(implies(implies(A,B),implies(or(C,A),or(C,B)))) = true ))),
% 154.08/19.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.08/19.93 fof(f7,axiom,(
% 154.08/19.93 (![X,Y]: (implies(X,Y) = or(not(X),Y) ))),
% 154.08/19.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.08/19.93 fof(f8,axiom,(
% 154.08/19.93 (![X]: (ifeq(axiom(X),true,theorem(X),true) = true ))),
% 154.08/19.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.08/19.93 fof(f9,axiom,(
% 154.08/19.93 (![Y,X]: (ifeq(theorem(implies(Y,X)),true,ifeq(theorem(Y),true,theorem(X),true),true) = true ))),
% 154.08/19.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.08/19.93 fof(f10,negated_conjecture,(
% 154.08/19.93 theorem(implies(implies(implies(p,q),implies(p,r)),implies(p,implies(q,r)))) != true ),
% 154.08/19.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.08/19.93 fof(f11,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 154.08/19.93 inference(cnf_transformation,[status(thm)],[f1])).
% 154.08/19.93 fof(f12,plain,(
% 154.08/19.93 ![X0]: (axiom(implies(or(X0,X0),X0))=true)),
% 154.08/19.93 inference(cnf_transformation,[status(thm)],[f2])).
% 154.08/19.93 fof(f13,plain,(
% 154.08/19.93 ![X0,X1]: (axiom(implies(X0,or(X1,X0)))=true)),
% 154.08/19.93 inference(cnf_transformation,[status(thm)],[f3])).
% 154.08/19.93 fof(f14,plain,(
% 154.08/19.93 ![X0,X1]: (axiom(implies(or(X0,X1),or(X1,X0)))=true)),
% 154.08/19.93 inference(cnf_transformation,[status(thm)],[f4])).
% 154.08/19.93 fof(f15,plain,(
% 154.08/19.93 ![X0,X1,X2]: (axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2))))=true)),
% 154.08/19.93 inference(cnf_transformation,[status(thm)],[f5])).
% 154.08/19.93 fof(f16,plain,(
% 154.08/19.93 ![X0,X1,X2]: (axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1))))=true)),
% 154.08/19.93 inference(cnf_transformation,[status(thm)],[f6])).
% 154.08/19.93 fof(f17,plain,(
% 154.08/19.93 ![X0,X1]: (implies(X0,X1)=or(not(X0),X1))),
% 154.08/19.93 inference(cnf_transformation,[status(thm)],[f7])).
% 154.08/19.93 fof(f18,plain,(
% 154.08/19.93 ![X0]: (ifeq(axiom(X0),true,theorem(X0),true)=true)),
% 154.08/19.93 inference(cnf_transformation,[status(thm)],[f8])).
% 154.08/19.93 fof(f19,plain,(
% 154.08/19.93 ![X0,X1]: (ifeq(theorem(implies(X0,X1)),true,ifeq(theorem(X0),true,theorem(X1),true),true)=true)),
% 154.08/19.93 inference(cnf_transformation,[status(thm)],[f9])).
% 154.08/19.93 fof(f20,plain,(
% 154.08/19.93 ~theorem(implies(implies(implies(p,q),implies(p,r)),implies(p,implies(q,r))))=true),
% 154.08/19.93 inference(cnf_transformation,[status(thm)],[f10])).
% 154.08/19.93 fof(f21,definition,(
% 154.08/19.93 sF3_fnc=implies(p,q)),
% 154.08/19.93 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 154.08/19.93 fof(f22,definition,(
% 154.08/19.93 sF4_fnc=implies(p,r)),
% 154.08/19.93 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 154.08/19.93 fof(f23,definition,(
% 154.08/19.93 sF2_fnc=implies(sF3_fnc,sF4_fnc)),
% 154.08/19.93 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 154.08/19.93 fof(f24,definition,(
% 154.08/19.93 sF6_fnc=implies(q,r)),
% 154.08/19.93 introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition])).
% 154.08/19.93 fof(f25,definition,(
% 154.08/19.93 sF5_fnc=implies(p,sF6_fnc)),
% 154.08/19.93 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 154.08/19.93 fof(f26,definition,(
% 154.08/19.93 sF1_fnc=implies(sF2_fnc,sF5_fnc)),
% 154.08/19.93 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 154.08/19.93 fof(f27,definition,(
% 154.08/19.93 sF0_fnc=theorem(sF1_fnc)),
% 154.08/19.93 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 154.08/19.93 fof(f28,plain,(
% 154.08/19.93 ~sF0_fnc=true),
% 154.08/19.93 inference(definition_folding,[],[f20,f27,f26,f25,f24,f23,f22,f21])).
% 154.08/19.93 fof(f30,plain,(
% 154.08/19.93 ![X0,X1]: (axiom(implies(X0,implies(X1,X0)))=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f17,f13])).
% 154.08/19.93 fof(f32,plain,(
% 154.08/19.93 axiom(implies(r,sF6_fnc))=true),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f24,f30])).
% 154.08/19.93 fof(f36,plain,(
% 154.08/19.93 axiom(implies(q,sF3_fnc))=true),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f21,f30])).
% 154.08/19.93 fof(f37,plain,(
% 154.08/19.93 ![X0,X1]: (axiom(implies(implies(X0,X1),or(X1,not(X0))))=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f17,f14])).
% 154.08/19.93 fof(f39,plain,(
% 154.08/19.93 ![X0,X1,X2]: (axiom(implies(implies(X0,or(X1,X2)),or(X1,or(not(X0),X2))))=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f17,f15])).
% 154.08/19.93 fof(f43,plain,(
% 154.08/19.93 ![X0,X1,X2]: (axiom(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2))))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f17,f39])).
% 154.08/19.93 fof(f53,plain,(
% 154.08/19.93 ![X0,X1,X2]: (axiom(implies(implies(X0,X1),implies(implies(X2,X0),or(not(X2),X1))))=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f17,f16])).
% 154.08/19.93 fof(f55,plain,(
% 154.08/19.93 ![X0,X1,X2]: (axiom(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1))))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f17,f53])).
% 154.08/19.93 fof(f78,plain,(
% 154.08/19.93 ifeq(true,true,theorem(implies(q,sF3_fnc)),true)=true),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f36,f18])).
% 154.08/19.93 fof(f84,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(true,true,theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f16,f18])).
% 154.08/19.93 fof(f86,plain,(
% 154.08/19.93 ifeq(true,true,theorem(implies(r,sF6_fnc)),true)=true),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f32,f18])).
% 154.08/19.93 fof(f89,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(true,true,theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f15,f18])).
% 154.08/19.93 fof(f90,plain,(
% 154.08/19.93 ![X0,X1]: (ifeq(true,true,theorem(implies(or(X0,X1),or(X1,X0))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f14,f18])).
% 154.08/19.93 fof(f91,plain,(
% 154.08/19.93 ![X0]: (ifeq(true,true,theorem(implies(or(X0,X0),X0)),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f12,f18])).
% 154.08/19.93 fof(f92,plain,(
% 154.08/19.93 ![X0,X1]: (ifeq(true,true,theorem(implies(X0,implies(X1,X0))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f30,f18])).
% 154.08/19.93 fof(f93,plain,(
% 154.08/19.93 ![X0,X1]: (ifeq(true,true,theorem(implies(X0,or(X1,X0))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f13,f18])).
% 154.08/19.93 fof(f96,plain,(
% 154.08/19.93 theorem(implies(q,sF3_fnc))=true),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f78])).
% 154.08/19.93 fof(f102,plain,(
% 154.08/19.93 ![X0,X1,X2]: (theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1))))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f84])).
% 154.08/19.93 fof(f104,plain,(
% 154.08/19.93 theorem(implies(r,sF6_fnc))=true),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f86])).
% 154.08/19.93 fof(f107,plain,(
% 154.08/19.93 ![X0,X1,X2]: (theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2))))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f89])).
% 154.08/19.93 fof(f108,plain,(
% 154.08/19.93 ![X0,X1]: (theorem(implies(or(X0,X1),or(X1,X0)))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f90])).
% 154.08/19.93 fof(f109,plain,(
% 154.08/19.93 ![X0]: (theorem(implies(or(X0,X0),X0))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f91])).
% 154.08/19.93 fof(f110,plain,(
% 154.08/19.93 ![X0,X1]: (theorem(implies(X0,implies(X1,X0)))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f92])).
% 154.08/19.93 fof(f111,plain,(
% 154.08/19.93 ![X0,X1]: (theorem(implies(X0,or(X1,X0)))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f93])).
% 154.08/19.93 fof(f137,plain,(
% 154.08/19.93 ![X0]: (ifeq(theorem(implies(implies(q,sF3_fnc),X0)),true,ifeq(true,true,theorem(X0),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f96,f19])).
% 154.08/19.93 fof(f144,plain,(
% 154.08/19.93 ![X0]: (ifeq(theorem(implies(X0,sF1_fnc)),true,ifeq(theorem(X0),true,sF0_fnc,true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f27,f19])).
% 154.08/19.93 fof(f155,plain,(
% 154.08/19.93 ![X0]: (ifeq(theorem(implies(implies(q,sF3_fnc),X0)),true,theorem(X0),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f137])).
% 154.08/19.93 fof(f165,plain,(
% 154.08/19.93 ![X0,X1]: (ifeq(true,true,theorem(implies(implies(X0,X1),or(X1,not(X0)))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f37,f18])).
% 154.08/19.93 fof(f166,plain,(
% 154.08/19.93 ![X0,X1]: (theorem(implies(implies(X0,X1),or(X1,not(X0))))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f165])).
% 154.08/19.93 fof(f201,plain,(
% 154.08/19.93 ![X0,X1]: (ifeq(true,true,ifeq(theorem(X0),true,theorem(implies(X1,X0)),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f110,f19])).
% 154.08/19.93 fof(f205,plain,(
% 154.08/19.93 ![X0,X1]: (ifeq(theorem(X0),true,theorem(implies(X1,X0)),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f201])).
% 154.08/19.93 fof(f209,plain,(
% 154.08/19.93 ![X0,X1]: (ifeq(true,true,ifeq(theorem(X0),true,theorem(or(X1,X0)),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f111,f19])).
% 154.08/19.93 fof(f213,plain,(
% 154.08/19.93 ![X0,X1]: (ifeq(theorem(X0),true,theorem(or(X1,X0)),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f209])).
% 154.08/19.93 fof(f220,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(theorem(implies(implies(or(X0,X1),or(X1,X0)),X2)),true,ifeq(true,true,theorem(X2),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f108,f19])).
% 154.08/19.93 fof(f223,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(theorem(implies(implies(or(X0,X1),or(X1,X0)),X2)),true,theorem(X2),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f220])).
% 154.08/19.93 fof(f243,plain,(
% 154.08/19.93 ![X0]: (axiom(implies(implies(sF2_fnc,or(X0,sF5_fnc)),or(X0,sF1_fnc)))=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f26,f43])).
% 154.08/19.93 fof(f246,plain,(
% 154.08/19.93 ![X0]: (axiom(implies(implies(p,or(X0,sF6_fnc)),or(X0,sF5_fnc)))=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f25,f43])).
% 154.08/19.93 fof(f249,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(true,true,theorem(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2)))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f43,f18])).
% 154.08/19.93 fof(f252,plain,(
% 154.08/19.93 ![X0,X1,X2]: (theorem(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2))))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f249])).
% 154.08/19.93 fof(f288,plain,(
% 154.08/19.93 ![X0,X1]: (ifeq(true,true,ifeq(theorem(implies(X0,X1)),true,theorem(or(X1,not(X0))),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f166,f19])).
% 154.08/19.93 fof(f292,plain,(
% 154.08/19.93 ![X0,X1]: (ifeq(theorem(implies(X0,X1)),true,theorem(or(X1,not(X0))),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f288])).
% 154.08/19.93 fof(f331,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(true,true,theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f55,f18])).
% 154.08/19.93 fof(f332,plain,(
% 154.08/19.93 ![X0,X1,X2]: (theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1))))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f331])).
% 154.08/19.93 fof(f374,plain,(
% 154.08/19.93 ifeq(true,true,ifeq(theorem(or(sF1_fnc,sF1_fnc)),true,sF0_fnc,true),true)=true),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f109,f144])).
% 154.08/19.93 fof(f392,plain,(
% 154.08/19.93 ifeq(theorem(or(sF1_fnc,sF1_fnc)),true,sF0_fnc,true)=true),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f374])).
% 154.08/19.93 fof(f461,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(true,true,ifeq(theorem(implies(X0,X1)),true,theorem(implies(or(X2,X0),or(X2,X1))),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f102,f19])).
% 154.08/19.93 fof(f469,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(theorem(implies(X0,X1)),true,theorem(implies(or(X2,X0),or(X2,X1))),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f461])).
% 154.08/19.93 fof(f478,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(true,true,ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X1,or(X0,X2))),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f107,f19])).
% 154.08/19.93 fof(f488,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X1,or(X0,X2))),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f478])).
% 154.08/19.93 fof(f1091,plain,(
% 154.08/19.93 ![X0]: (ifeq(true,true,theorem(implies(implies(sF2_fnc,or(X0,sF5_fnc)),or(X0,sF1_fnc))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f243,f18])).
% 154.08/19.93 fof(f1094,plain,(
% 154.08/19.93 ![X0]: (theorem(implies(implies(sF2_fnc,or(X0,sF5_fnc)),or(X0,sF1_fnc)))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f1091])).
% 154.08/19.93 fof(f1448,plain,(
% 154.08/19.93 ![X0]: (ifeq(true,true,theorem(implies(implies(p,or(X0,sF6_fnc)),or(X0,sF5_fnc))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f246,f18])).
% 154.08/19.93 fof(f1451,plain,(
% 154.08/19.93 ![X0]: (theorem(implies(implies(p,or(X0,sF6_fnc)),or(X0,sF5_fnc)))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f1448])).
% 154.08/19.93 fof(f2079,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(true,true,theorem(implies(or(X0,or(X1,X2)),or(X0,or(X2,X1)))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f102,f223])).
% 154.08/19.93 fof(f2161,plain,(
% 154.08/19.93 ![X0,X1,X2]: (theorem(implies(or(X0,or(X1,X2)),or(X0,or(X2,X1))))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f2079])).
% 154.08/19.93 fof(f2288,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(true,true,ifeq(theorem(implies(X0,or(X1,X2))),true,theorem(or(X1,implies(X0,X2))),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f252,f19])).
% 154.08/19.93 fof(f2306,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(theorem(implies(X0,or(X1,X2))),true,theorem(or(X1,implies(X0,X2))),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f2288])).
% 154.08/19.93 fof(f4532,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(true,true,ifeq(theorem(implies(X0,X1)),true,theorem(implies(implies(X2,X0),implies(X2,X1))),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f332,f19])).
% 154.08/19.93 fof(f4550,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(theorem(implies(X0,X1)),true,theorem(implies(implies(X2,X0),implies(X2,X1))),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f4532])).
% 154.08/19.93 fof(f6086,plain,(
% 154.08/19.93 ![X0]: (ifeq(true,true,theorem(implies(or(X0,r),or(X0,sF6_fnc))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f104,f469])).
% 154.08/19.93 fof(f6177,plain,(
% 154.08/19.93 ![X0]: (theorem(implies(or(X0,r),or(X0,sF6_fnc)))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f6086])).
% 154.08/19.93 fof(f15492,plain,(
% 154.08/19.93 ![X0]: (theorem(implies(implies(X0,r),or(not(X0),sF6_fnc)))=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f17,f6177])).
% 154.08/19.93 fof(f15529,plain,(
% 154.08/19.93 ![X0]: (theorem(implies(implies(X0,r),implies(X0,sF6_fnc)))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f17,f15492])).
% 154.08/19.93 fof(f22494,plain,(
% 154.08/19.93 theorem(implies(sF4_fnc,implies(p,sF6_fnc)))=true),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f22,f15529])).
% 154.08/19.93 fof(f22530,plain,(
% 154.08/19.93 theorem(implies(sF4_fnc,sF5_fnc))=true),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f25,f22494])).
% 154.08/19.93 fof(f22545,plain,(
% 154.08/19.93 ![X0]: (ifeq(true,true,theorem(implies(or(X0,sF4_fnc),or(X0,sF5_fnc))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f22530,f469])).
% 154.08/19.93 fof(f22574,plain,(
% 154.08/19.93 ![X0]: (theorem(implies(or(X0,sF4_fnc),or(X0,sF5_fnc)))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f22545])).
% 154.08/19.93 fof(f24346,plain,(
% 154.08/19.93 ![X0]: (ifeq(true,true,ifeq(theorem(implies(sF2_fnc,or(X0,sF5_fnc))),true,theorem(or(X0,sF1_fnc)),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f1094,f19])).
% 154.08/19.93 fof(f24377,plain,(
% 154.08/19.93 ![X0]: (ifeq(theorem(implies(sF2_fnc,or(X0,sF5_fnc))),true,theorem(or(X0,sF1_fnc)),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f24346])).
% 154.08/19.93 fof(f29343,plain,(
% 154.08/19.93 ![X0]: (ifeq(true,true,ifeq(theorem(implies(p,or(X0,sF6_fnc))),true,theorem(or(X0,sF5_fnc)),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f1451,f19])).
% 154.08/19.93 fof(f29374,plain,(
% 154.08/19.93 ![X0]: (ifeq(theorem(implies(p,or(X0,sF6_fnc))),true,theorem(or(X0,sF5_fnc)),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f29343])).
% 154.08/19.93 fof(f32608,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(true,true,ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X0,or(X2,X1))),true),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f2161,f19])).
% 154.08/19.93 fof(f32639,plain,(
% 154.08/19.93 ![X0,X1,X2]: (ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X0,or(X2,X1))),true)=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f32608])).
% 154.08/19.93 fof(f39146,plain,(
% 154.08/19.93 ![X0]: (ifeq(true,true,theorem(or(X0,implies(or(X0,sF4_fnc),sF5_fnc))),true)=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f22574,f2306])).
% 154.08/19.93 fof(f39357,plain,(
% 154.08/19.93 ![X0]: (theorem(or(X0,implies(or(X0,sF4_fnc),sF5_fnc)))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f11,f39146])).
% 154.08/19.93 fof(f39976,plain,(
% 154.08/19.93 ![X0]: (theorem(implies(X0,implies(or(not(X0),sF4_fnc),sF5_fnc)))=true)),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f17,f39357])).
% 154.08/19.93 fof(f40069,plain,(
% 154.08/19.93 ![X0]: (theorem(implies(X0,implies(implies(X0,sF4_fnc),sF5_fnc)))=true)),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f17,f39976])).
% 154.08/19.93 fof(f43369,plain,(
% 154.08/19.93 theorem(implies(sF3_fnc,implies(sF2_fnc,sF5_fnc)))=true),
% 154.08/19.93 inference(paramodulation,[status(thm)],[f23,f40069])).
% 154.08/19.93 fof(f43426,plain,(
% 154.08/19.93 theorem(implies(sF3_fnc,sF1_fnc))=true),
% 154.08/19.93 inference(forward_demodulation,[status(thm)],[f26,f43369])).
% 122.89/20.29 fof(f56343,plain,(
% 122.89/20.29 ![X0]: (ifeq(true,true,theorem(implies(implies(X0,sF3_fnc),implies(X0,sF1_fnc))),true)=true)),
% 122.89/20.29 inference(paramodulation,[status(thm)],[f43426,f4550])).
% 122.89/20.29 fof(f56660,plain,(
% 122.89/20.29 ![X0]: (theorem(implies(implies(X0,sF3_fnc),implies(X0,sF1_fnc)))=true)),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f11,f56343])).
% 122.89/20.29 fof(f196373,plain,(
% 122.89/20.29 ifeq(true,true,theorem(implies(q,sF1_fnc)),true)=true),
% 122.89/20.29 inference(paramodulation,[status(thm)],[f56660,f155])).
% 122.89/20.29 fof(f196452,plain,(
% 122.89/20.29 theorem(implies(q,sF1_fnc))=true),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f11,f196373])).
% 122.89/20.29 fof(f198082,plain,(
% 122.89/20.29 ifeq(true,true,theorem(or(sF1_fnc,not(q))),true)=true),
% 122.89/20.29 inference(paramodulation,[status(thm)],[f196452,f292])).
% 122.89/20.29 fof(f198147,plain,(
% 122.89/20.29 theorem(or(sF1_fnc,not(q)))=true),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f11,f198082])).
% 122.89/20.29 fof(f198213,plain,(
% 122.89/20.29 ![X0]: (ifeq(true,true,theorem(or(X0,or(sF1_fnc,not(q)))),true)=true)),
% 122.89/20.29 inference(paramodulation,[status(thm)],[f198147,f213])).
% 122.89/20.29 fof(f198227,plain,(
% 122.89/20.29 ![X0]: (theorem(or(X0,or(sF1_fnc,not(q))))=true)),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f11,f198213])).
% 122.89/20.29 fof(f200490,plain,(
% 122.89/20.29 ![X0]: (ifeq(true,true,theorem(or(sF1_fnc,or(X0,not(q)))),true)=true)),
% 122.89/20.29 inference(paramodulation,[status(thm)],[f198227,f488])).
% 122.89/20.29 fof(f200554,plain,(
% 122.89/20.29 ![X0]: (theorem(or(sF1_fnc,or(X0,not(q))))=true)),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f11,f200490])).
% 122.89/20.29 fof(f546555,plain,(
% 122.89/20.29 ![X0]: (ifeq(true,true,theorem(or(sF1_fnc,or(not(q),X0))),true)=true)),
% 122.89/20.29 inference(paramodulation,[status(thm)],[f200554,f32639])).
% 122.89/20.29 fof(f547624,plain,(
% 122.89/20.29 ![X0]: (theorem(or(sF1_fnc,or(not(q),X0)))=true)),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f11,f546555])).
% 122.89/20.29 fof(f547625,plain,(
% 122.89/20.29 ![X0]: (theorem(or(sF1_fnc,implies(q,X0)))=true)),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f17,f547624])).
% 122.89/20.29 fof(f564310,plain,(
% 122.89/20.29 theorem(or(sF1_fnc,sF6_fnc))=true),
% 122.89/20.29 inference(paramodulation,[status(thm)],[f24,f547625])).
% 122.89/20.29 fof(f564573,plain,(
% 122.89/20.29 ![X0]: (ifeq(true,true,theorem(implies(X0,or(sF1_fnc,sF6_fnc))),true)=true)),
% 122.89/20.29 inference(paramodulation,[status(thm)],[f564310,f205])).
% 122.89/20.29 fof(f564585,plain,(
% 122.89/20.29 ![X0]: (theorem(implies(X0,or(sF1_fnc,sF6_fnc)))=true)),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f11,f564573])).
% 122.89/20.29 fof(f582833,plain,(
% 122.89/20.29 ifeq(true,true,theorem(or(sF1_fnc,sF5_fnc)),true)=true),
% 122.89/20.29 inference(paramodulation,[status(thm)],[f564585,f29374])).
% 122.89/20.29 fof(f583043,plain,(
% 122.89/20.29 theorem(or(sF1_fnc,sF5_fnc))=true),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f11,f582833])).
% 122.89/20.29 fof(f583225,plain,(
% 122.89/20.29 ![X0]: (ifeq(true,true,theorem(implies(X0,or(sF1_fnc,sF5_fnc))),true)=true)),
% 122.89/20.29 inference(paramodulation,[status(thm)],[f583043,f205])).
% 122.89/20.29 fof(f583237,plain,(
% 122.89/20.29 ![X0]: (theorem(implies(X0,or(sF1_fnc,sF5_fnc)))=true)),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f11,f583225])).
% 122.89/20.29 fof(f591622,plain,(
% 122.89/20.29 ifeq(true,true,theorem(or(sF1_fnc,sF1_fnc)),true)=true),
% 122.89/20.29 inference(paramodulation,[status(thm)],[f583237,f24377])).
% 122.89/20.29 fof(f591829,plain,(
% 122.89/20.29 theorem(or(sF1_fnc,sF1_fnc))=true),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f11,f591622])).
% 122.89/20.29 fof(f591924,plain,(
% 122.89/20.29 ifeq(true,true,sF0_fnc,true)=true),
% 122.89/20.29 inference(backward_demodulation,[status(thm)],[f591829,f392])).
% 122.89/20.29 fof(f592023,plain,(
% 122.89/20.29 sF0_fnc=true),
% 122.89/20.29 inference(forward_demodulation,[status(thm)],[f11,f591924])).
% 122.89/20.29 fof(f592024,plain,(
% 122.89/20.29 $false),
% 122.89/20.29 inference(forward_subsumption_resolution,[status(thm)],[f592023,f28])).
% 122.89/20.29 % SZS output end CNFRefutation for theBenchmark.p
% 24.83/20.34 % Elapsed time: 19.929523 seconds
% 24.83/20.34 % CPU time: 157.811554 seconds
% 24.83/20.34 % Total memory used: 1.585 GB
% 24.83/20.34 % Net memory used: 1.554 GB
%------------------------------------------------------------------------------