%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL400-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:59 PM UTC 2026
% Result : Unsatisfiable 79.55s 10.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL400-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.36 % Computer : n018.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Mon Sep 21 00:30:13 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 79.55/10.51 % Refutation found
% 79.55/10.51 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 79.55/10.51 % SZS output start CNFRefutation for theBenchmark
% 79.55/10.51 fof(f1,axiom,(
% 79.55/10.51 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 79.55/10.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 79.55/10.51 fof(f2,axiom,(
% 79.55/10.51 (![X,Y]: (ifeq(is_a_theorem(implies(X,Y)),true,ifeq(is_a_theorem(X),true,is_a_theorem(Y),true),true) = true ))),
% 79.55/10.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 79.55/10.51 fof(f3,axiom,(
% 79.55/10.51 (![X,Y,Z]: (is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) = true ))),
% 79.55/10.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 79.55/10.51 fof(f4,axiom,(
% 79.55/10.51 (![X]: (is_a_theorem(implies(implies(not(X),X),X)) = true ))),
% 79.55/10.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 79.55/10.51 fof(f5,axiom,(
% 79.55/10.51 (![X,Y]: (is_a_theorem(implies(X,implies(not(X),Y))) = true ))),
% 79.55/10.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 79.55/10.51 fof(f6,negated_conjecture,(
% 79.55/10.51 is_a_theorem(implies(not(implies(x,y)),x)) != true ),
% 79.55/10.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 79.55/10.51 fof(f7,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 79.55/10.51 inference(cnf_transformation,[status(thm)],[f1])).
% 79.55/10.51 fof(f8,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(is_a_theorem(implies(X0,X1)),true,ifeq(is_a_theorem(X0),true,is_a_theorem(X1),true),true)=true)),
% 79.55/10.51 inference(cnf_transformation,[status(thm)],[f2])).
% 79.55/10.51 fof(f9,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))=true)),
% 79.55/10.51 inference(cnf_transformation,[status(thm)],[f3])).
% 79.55/10.51 fof(f10,plain,(
% 79.55/10.51 ![X0]: (is_a_theorem(implies(implies(not(X0),X0),X0))=true)),
% 79.55/10.51 inference(cnf_transformation,[status(thm)],[f4])).
% 79.55/10.51 fof(f11,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(X0,implies(not(X0),X1)))=true)),
% 79.55/10.51 inference(cnf_transformation,[status(thm)],[f5])).
% 79.55/10.51 fof(f12,plain,(
% 79.55/10.51 ~is_a_theorem(implies(not(implies(x,y)),x))=true),
% 79.55/10.51 inference(cnf_transformation,[status(thm)],[f6])).
% 79.55/10.51 fof(f18,plain,(
% 79.55/10.51 ![X0]: (ifeq(true,true,ifeq(is_a_theorem(implies(not(X0),X0)),true,is_a_theorem(X0),true),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f10,f8])).
% 79.55/10.51 fof(f19,plain,(
% 79.55/10.51 ![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)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f9,f8])).
% 79.55/10.51 fof(f20,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,ifeq(is_a_theorem(X0),true,is_a_theorem(implies(not(X0),X1)),true),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f11,f8])).
% 79.55/10.51 fof(f21,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(is_a_theorem(implies(implies(implies(not(X0),X0),X0),X1)),true,ifeq(true,true,is_a_theorem(X1),true),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f10,f8])).
% 79.55/10.51 fof(f23,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(X0,implies(not(X0),X1)),X2)),true,ifeq(true,true,is_a_theorem(X2),true),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f11,f8])).
% 79.55/10.51 fof(f27,plain,(
% 79.55/10.51 ![X0]: (ifeq(is_a_theorem(implies(not(X0),X0)),true,is_a_theorem(X0),true)=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f18])).
% 79.55/10.51 fof(f28,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(X0,X1)),true,is_a_theorem(implies(implies(X1,X2),implies(X0,X2))),true)=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f19])).
% 79.55/10.51 fof(f29,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(is_a_theorem(X0),true,is_a_theorem(implies(not(X0),X1)),true)=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f20])).
% 79.55/10.51 fof(f30,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(is_a_theorem(implies(implies(implies(not(X0),X0),X0),X1)),true,is_a_theorem(X1),true)=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f21])).
% 79.55/10.51 fof(f32,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(X0,implies(not(X0),X1)),X2)),true,is_a_theorem(X2),true)=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f23])).
% 79.55/10.51 fof(f123,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(implies(X0,X1),implies(implies(not(X0),X0),X1))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f10,f28])).
% 79.55/10.51 fof(f124,plain,(
% 79.55/10.51 ![X0,X1,X2,X3]: (ifeq(true,true,is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X2,X1)),X3),implies(implies(X2,X0),X3))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f9,f28])).
% 79.55/10.51 fof(f125,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(implies(not(X0),X1),X2),implies(X0,X2))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f11,f28])).
% 79.55/10.51 fof(f133,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(implies(X0,X1),implies(implies(not(X0),X0),X1)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f123])).
% 79.55/10.51 fof(f134,plain,(
% 79.55/10.51 ![X0,X1,X2,X3]: (is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X2,X1)),X3),implies(implies(X2,X0),X3)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f124])).
% 79.55/10.51 fof(f135,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(not(X0),X1),X2),implies(X0,X2)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f125])).
% 79.55/10.51 fof(f143,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(implies(X0,X1),implies(implies(not(X0),X0),X1)),X2)),true,ifeq(true,true,is_a_theorem(X2),true),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f133,f8])).
% 79.55/10.51 fof(f148,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(implies(X0,X1),implies(implies(not(X0),X0),X1)),X2)),true,is_a_theorem(X2),true)=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f143])).
% 79.55/10.51 fof(f151,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,ifeq(is_a_theorem(implies(implies(not(X0),X1),X2)),true,is_a_theorem(implies(X0,X2)),true),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f135,f8])).
% 79.55/10.51 fof(f156,plain,(
% 79.55/10.51 ![X0,X1,X2,X3]: (ifeq(is_a_theorem(implies(implies(implies(implies(not(X0),X1),X2),implies(X0,X2)),X3)),true,ifeq(true,true,is_a_theorem(X3),true),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f135,f8])).
% 79.55/10.51 fof(f158,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(not(X0),X1),X2)),true,is_a_theorem(implies(X0,X2)),true)=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f151])).
% 79.55/10.51 fof(f161,plain,(
% 79.55/10.51 ![X0,X1,X2,X3]: (ifeq(is_a_theorem(implies(implies(implies(implies(not(X0),X1),X2),implies(X0,X2)),X3)),true,is_a_theorem(X3),true)=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f156])).
% 79.55/10.51 fof(f226,plain,(
% 79.55/10.51 ![X0]: (ifeq(true,true,is_a_theorem(implies(X0,X0)),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f135,f30])).
% 79.55/10.51 fof(f244,plain,(
% 79.55/10.51 ![X0]: (is_a_theorem(implies(X0,X0))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f226])).
% 79.55/10.51 fof(f271,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(not(implies(X0,X0)),X1)),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f244,f29])).
% 79.55/10.51 fof(f278,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(not(implies(X0,X0)),X1))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f271])).
% 79.55/10.51 fof(f291,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(X0,X1),implies(not(implies(X2,X2)),X1))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f278,f28])).
% 79.55/10.51 fof(f302,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(implies(X0,X1),implies(not(implies(X2,X2)),X1)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f291])).
% 79.55/10.51 fof(f1281,plain,(
% 79.55/10.51 ![X0,X1,X2,X3]: (ifeq(true,true,ifeq(is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X1)),X3)),true,is_a_theorem(implies(implies(X2,X0),X3)),true),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f134,f8])).
% 79.55/10.51 fof(f1302,plain,(
% 79.55/10.51 ![X0,X1,X2,X3]: (ifeq(is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X1)),X3)),true,is_a_theorem(implies(implies(X2,X0),X3)),true)=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f1281])).
% 79.55/10.51 fof(f2179,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(X0,implies(not(implies(X1,X1)),X2))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f302,f158])).
% 79.55/10.51 fof(f2252,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(X0,implies(not(implies(X1,X1)),X2)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f2179])).
% 79.55/10.51 fof(f2339,plain,(
% 79.55/10.51 ![X0,X1,X2,X3]: (ifeq(true,true,is_a_theorem(implies(implies(implies(not(implies(X0,X0)),X1),X2),implies(X3,X2))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f2252,f28])).
% 79.55/10.51 fof(f2372,plain,(
% 79.55/10.51 ![X0,X1,X2,X3]: (is_a_theorem(implies(implies(implies(not(implies(X0,X0)),X1),X2),implies(X3,X2)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f2339])).
% 79.55/10.51 fof(f3021,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(X0,implies(X1,X1))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f2372,f30])).
% 79.55/10.51 fof(f3065,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(X0,implies(X1,X1)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f3021])).
% 79.55/10.51 fof(f3189,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,X1))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f3065,f28])).
% 79.55/10.51 fof(f3223,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,X1)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f3189])).
% 79.55/10.51 fof(f3443,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(X0,implies(implies(not(X1),X1),X1))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f3223,f148])).
% 79.55/10.51 fof(f3489,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(X0,implies(implies(not(X1),X1),X1)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f3443])).
% 79.55/10.51 fof(f3739,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(implies(implies(not(X0),X0),X0),X1),implies(X2,X1))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f3489,f28])).
% 79.55/10.51 fof(f3775,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(implies(not(X0),X0),X0),X1),implies(X2,X1)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f3739])).
% 79.55/10.51 fof(f8996,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X2,implies(X0,X1)))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f3775,f1302])).
% 79.55/10.51 fof(f9112,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X2,implies(X0,X1))))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f8996])).
% 79.55/10.51 fof(f12319,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(not(X0),X1),implies(X2,implies(implies(X1,X0),X0)))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f9112,f1302])).
% 79.55/10.51 fof(f12409,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(implies(not(X0),X1),implies(X2,implies(implies(X1,X0),X0))))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f12319])).
% 79.55/10.51 fof(f13349,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(X0,implies(X1,implies(implies(X2,X0),X0)))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f12409,f158])).
% 79.55/10.51 fof(f13422,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(X0,implies(X1,implies(implies(X2,X0),X0))))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f13349])).
% 79.55/10.51 fof(f13587,plain,(
% 79.55/10.51 ![X0,X1,X2,X3]: (ifeq(true,true,is_a_theorem(implies(implies(implies(X0,implies(implies(X1,X2),X2)),X3),implies(X2,X3))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f13422,f28])).
% 79.55/10.51 fof(f13632,plain,(
% 79.55/10.51 ![X0,X1,X2,X3]: (is_a_theorem(implies(implies(implies(X0,implies(implies(X1,X2),X2)),X3),implies(X2,X3)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f13587])).
% 79.55/10.51 fof(f20149,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(X0,implies(implies(X1,X0),X0))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f13632,f30])).
% 79.55/10.51 fof(f20244,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(X0,implies(implies(X1,X0),X0)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f20149])).
% 79.55/10.51 fof(f20390,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(X1,X2))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f20244,f28])).
% 79.55/10.51 fof(f20439,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(X1,X2)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f20390])).
% 79.55/10.51 fof(f21361,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(X0,implies(X1,X0))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f20439,f161])).
% 79.55/10.51 fof(f21456,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(X0,implies(X1,X0)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f21361])).
% 79.55/10.51 fof(f21690,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f21456,f28])).
% 79.55/10.51 fof(f21722,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(X0,implies(X1,X0)),X2)),true,ifeq(true,true,is_a_theorem(X2),true),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f21456,f8])).
% 79.55/10.51 fof(f21748,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f21690])).
% 79.55/10.51 fof(f21766,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(X0,implies(X1,X0)),X2)),true,is_a_theorem(X2),true)=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f21722])).
% 79.55/10.51 fof(f22757,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,ifeq(is_a_theorem(implies(implies(X0,X1),X2)),true,is_a_theorem(implies(X1,X2)),true),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f21748,f8])).
% 79.55/10.51 fof(f22811,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(is_a_theorem(implies(implies(X0,X1),X2)),true,is_a_theorem(implies(X1,X2)),true)=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f22757])).
% 79.55/10.51 fof(f56268,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(X0,implies(X1,implies(implies(X0,X2),X2)))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f12409,f22811])).
% 79.55/10.51 fof(f56647,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(X0,implies(X1,implies(implies(X0,X2),X2))))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f56268])).
% 79.55/10.51 fof(f57253,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(X0,implies(implies(implies(implies(not(X1),X1),X1),X2),X2))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f56647,f30])).
% 79.55/10.51 fof(f57418,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(X0,implies(implies(implies(implies(not(X1),X1),X1),X2),X2)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f57253])).
% 79.55/10.51 fof(f70115,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(implies(implies(implies(not(X0),X0),X0),X1),X1)),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f57418,f27])).
% 79.55/10.51 fof(f70303,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(implies(implies(implies(not(X0),X0),X0),X1),X1))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f70115])).
% 79.55/10.51 fof(f70428,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X0,X1))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f70303,f1302])).
% 79.55/10.51 fof(f70574,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X0,X1)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f70428])).
% 79.55/10.51 fof(f71027,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(implies(not(X0),X1),implies(implies(X1,X0),X0))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f70574,f1302])).
% 79.55/10.51 fof(f71184,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(implies(not(X0),X1),implies(implies(X1,X0),X0)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f71027])).
% 79.55/10.51 fof(f71270,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(X0,implies(implies(X0,X1),X1))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f71184,f22811])).
% 79.55/10.51 fof(f71375,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(X0,implies(implies(X0,X1),X1)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f71270])).
% 79.55/10.51 fof(f71694,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f71375,f28])).
% 79.55/10.51 fof(f71768,plain,(
% 79.55/10.51 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f71694])).
% 79.55/10.51 fof(f74707,plain,(
% 79.55/10.51 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(not(X0),implies(X0,X1))),true)=true)),
% 79.55/10.51 inference(paramodulation,[status(thm)],[f71768,f161])).
% 79.55/10.51 fof(f74870,plain,(
% 79.55/10.51 ![X0,X1]: (is_a_theorem(implies(not(X0),implies(X0,X1)))=true)),
% 79.55/10.51 inference(forward_demodulation,[status(thm)],[f7,f74707])).
% 79.55/10.51 fof(f75183,plain,(
% 79.55/10.51 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(X0),X2))),true)=true)),
% 7.53/10.82 inference(paramodulation,[status(thm)],[f74870,f28])).
% 7.53/10.82 fof(f75234,plain,(
% 7.53/10.82 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(X0),X2)))=true)),
% 7.53/10.82 inference(forward_demodulation,[status(thm)],[f7,f75183])).
% 7.53/10.82 fof(f77014,plain,(
% 7.53/10.82 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(implies(X0,X1),implies(not(X1),implies(X0,X2)))),true)=true)),
% 7.53/10.82 inference(paramodulation,[status(thm)],[f75234,f1302])).
% 7.53/10.82 fof(f77155,plain,(
% 7.53/10.82 ![X0,X1,X2]: (is_a_theorem(implies(implies(X0,X1),implies(not(X1),implies(X0,X2))))=true)),
% 7.53/10.82 inference(forward_demodulation,[status(thm)],[f7,f77014])).
% 7.53/10.82 fof(f84831,plain,(
% 7.53/10.82 ![X0,X1,X2]: (ifeq(true,true,is_a_theorem(implies(not(implies(X0,X1)),implies(X1,X2))),true)=true)),
% 7.53/10.82 inference(paramodulation,[status(thm)],[f77155,f21766])).
% 7.53/10.82 fof(f84983,plain,(
% 7.53/10.82 ![X0,X1,X2]: (is_a_theorem(implies(not(implies(X0,X1)),implies(X1,X2)))=true)),
% 7.53/10.82 inference(forward_demodulation,[status(thm)],[f7,f84831])).
% 7.53/10.82 fof(f85551,plain,(
% 7.53/10.82 ![X0,X1,X2,X3]: (ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(implies(X3,X0)),X2))),true)=true)),
% 7.53/10.82 inference(paramodulation,[status(thm)],[f84983,f28])).
% 7.53/10.82 fof(f85606,plain,(
% 7.53/10.82 ![X0,X1,X2,X3]: (is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(implies(X3,X0)),X2)))=true)),
% 7.53/10.82 inference(forward_demodulation,[status(thm)],[f7,f85551])).
% 7.53/10.82 fof(f145971,plain,(
% 7.53/10.82 ![X0,X1,X2,X3]: (ifeq(true,true,is_a_theorem(implies(not(implies(X0,X1)),implies(not(implies(X1,X2)),X3))),true)=true)),
% 7.53/10.82 inference(paramodulation,[status(thm)],[f85606,f32])).
% 7.53/10.82 fof(f146142,plain,(
% 7.53/10.82 ![X0,X1,X2,X3]: (is_a_theorem(implies(not(implies(X0,X1)),implies(not(implies(X1,X2)),X3)))=true)),
% 7.53/10.82 inference(forward_demodulation,[status(thm)],[f7,f145971])).
% 7.53/10.82 fof(f151379,plain,(
% 7.53/10.82 ![X0,X1]: (ifeq(true,true,is_a_theorem(implies(not(implies(X0,X1)),X0)),true)=true)),
% 7.53/10.82 inference(paramodulation,[status(thm)],[f146142,f27])).
% 7.53/10.82 fof(f151541,plain,(
% 7.53/10.82 ~true=true),
% 7.53/10.82 inference(backward_demodulation,[status(thm)],[f151542,f12])).
% 7.53/10.82 fof(f151542,plain,(
% 7.53/10.82 ![X0,X1]: (is_a_theorem(implies(not(implies(X0,X1)),X0))=true)),
% 7.53/10.82 inference(forward_demodulation,[status(thm)],[f7,f151379])).
% 7.53/10.82 fof(f151558,plain,(
% 7.53/10.82 $false),
% 7.53/10.82 inference(trivial_equality_resolution,[status(thm)],[f151541])).
% 7.53/10.82 % SZS output end CNFRefutation for theBenchmark.p
% 7.53/10.82 % Elapsed time: 10.434405 seconds
% 7.53/10.82 % CPU time: 81.997208 seconds
% 7.53/10.82 % Total memory used: 729.082 MB
% 7.53/10.82 % Net memory used: 714.362 MB
%------------------------------------------------------------------------------