%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 12:46:38 PM UTC 2026
% Result : Unsatisfiable 49.19s 11.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n011.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Sun Sep 20 20:47:32 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 % Drodi V4.1.1
% 49.19/11.71 % Refutation found
% 49.19/11.71 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 49.19/11.71 % SZS output start CNFRefutation for theBenchmark
% 49.19/11.71 fof(f2,axiom,(
% 49.19/11.71 (![X]: (and(X,n1) = X ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f3,axiom,(
% 49.19/11.71 (![X]: (or(X,n0) = X ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f4,axiom,(
% 49.19/11.71 (![X]: (or(X,n1) = n1 ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f6,axiom,(
% 49.19/11.71 not(n1) = n0 ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f7,axiom,(
% 49.19/11.71 (![X,Y]: (and(X,Y) = and(Y,X) ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f8,axiom,(
% 49.19/11.71 (![X,Y]: (or(X,Y) = or(Y,X) ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f9,axiom,(
% 49.19/11.71 (![X,Y,Z]: (and(X,and(Y,Z)) = and(and(X,Y),Z) ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f10,axiom,(
% 49.19/11.71 (![X,Y,Z]: (or(X,or(Y,Z)) = or(or(X,Y),Z) ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f11,axiom,(
% 49.19/11.71 (![X,Y,Z]: (or(or(X,Y),Z) = or(or(X,Z),Y) ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f12,axiom,(
% 49.19/11.71 (![X,Y,Z]: (and(and(X,Y),Z) = and(and(X,Z),Y) ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f13,axiom,(
% 49.19/11.71 (![X,Y]: (not(and(X,Y)) = or(not(X),not(Y)) ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f14,axiom,(
% 49.19/11.71 (![X,Y]: (not(or(X,Y)) = and(not(X),not(Y)) ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f15,axiom,(
% 49.19/11.71 (![X,Y,Z]: (and(or(X,Y),Z) = or(and(X,Z),and(Y,Z)) ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f16,axiom,(
% 49.19/11.71 (![X]: (and(X,X) = X ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f18,axiom,(
% 49.19/11.71 (![X,Y]: (and(and(X,Y),X) = and(X,Y) ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f19,axiom,(
% 49.19/11.71 (![X]: (or(X,X) = X ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f21,axiom,(
% 49.19/11.71 (![X,Y]: (or(or(X,Y),X) = or(X,Y) ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f22,axiom,(
% 49.19/11.71 (![X]: (and(X,not(X)) = n0 ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f25,axiom,(
% 49.19/11.71 (![X]: (or(X,not(X)) = n1 ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f28,axiom,(
% 49.19/11.71 (![X]: (not(not(X)) = X ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f29,axiom,(
% 49.19/11.71 (![X,Y]: (or(and(X,Y),and(X,not(Y))) = X ))),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f31,negated_conjecture,(
% 49.19/11.71 a1 = and(b1,b3) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f32,negated_conjecture,(
% 49.19/11.71 a2 = and(b2,b3) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f33,negated_conjecture,(
% 49.19/11.71 b1 = not(d1) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f34,negated_conjecture,(
% 49.19/11.71 b2 = not(d2) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f35,negated_conjecture,(
% 49.19/11.71 b3 = or(c1,c2) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f36,negated_conjecture,(
% 49.19/11.71 c1 = or(d1,d3) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f37,negated_conjecture,(
% 49.19/11.71 c2 = or(d2,d3) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f38,negated_conjecture,(
% 49.19/11.71 d3 = f3 ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f39,negated_conjecture,(
% 49.19/11.71 d1 = not(e1) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f40,negated_conjecture,(
% 49.19/11.71 d2 = not(e2) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f41,negated_conjecture,(
% 49.19/11.71 e1 = or(f1,f3) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f42,negated_conjecture,(
% 49.19/11.71 e2 = or(f2,f3) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f43,negated_conjecture,(
% 49.19/11.71 f1 = not(i1) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f44,negated_conjecture,(
% 49.19/11.71 f2 = not(i2) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f45,negated_conjecture,(
% 49.19/11.71 f3 = and(i1,i2) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f46,negated_conjecture,(
% 49.19/11.71 circuit(input(i1,i2),output(a1,a2)) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f47,negated_conjecture,(
% 49.19/11.71 ~ circuit(input(i1,i2),output(i2,i1)) ),
% 49.19/11.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.19/11.71 fof(f49,plain,(
% 49.19/11.71 ![X0]: (and(X0,n1)=X0)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f2])).
% 49.19/11.71 fof(f50,plain,(
% 49.19/11.71 ![X0]: (or(X0,n0)=X0)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f3])).
% 49.19/11.71 fof(f51,plain,(
% 49.19/11.71 ![X0]: (or(X0,n1)=n1)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f4])).
% 49.19/11.71 fof(f53,plain,(
% 49.19/11.71 not(n1)=n0),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f6])).
% 49.19/11.71 fof(f54,plain,(
% 49.19/11.71 ![X0,X1]: (and(X0,X1)=and(X1,X0))),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f7])).
% 49.19/11.71 fof(f55,plain,(
% 49.19/11.71 ![X0,X1]: (or(X0,X1)=or(X1,X0))),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f8])).
% 49.19/11.71 fof(f56,plain,(
% 49.19/11.71 ![X0,X1,X2]: (and(X0,and(X1,X2))=and(and(X0,X1),X2))),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f9])).
% 49.19/11.71 fof(f57,plain,(
% 49.19/11.71 ![X0,X1,X2]: (or(X0,or(X1,X2))=or(or(X0,X1),X2))),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f10])).
% 49.19/11.71 fof(f58,plain,(
% 49.19/11.71 ![X0,X1,X2]: (or(or(X0,X1),X2)=or(or(X0,X2),X1))),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f11])).
% 49.19/11.71 fof(f59,plain,(
% 49.19/11.71 ![X0,X1,X2]: (and(and(X0,X1),X2)=and(and(X0,X2),X1))),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f12])).
% 49.19/11.71 fof(f60,plain,(
% 49.19/11.71 ![X0,X1]: (not(and(X0,X1))=or(not(X0),not(X1)))),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f13])).
% 49.19/11.71 fof(f61,plain,(
% 49.19/11.71 ![X0,X1]: (not(or(X0,X1))=and(not(X0),not(X1)))),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f14])).
% 49.19/11.71 fof(f62,plain,(
% 49.19/11.71 ![X0,X1,X2]: (and(or(X0,X1),X2)=or(and(X0,X2),and(X1,X2)))),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f15])).
% 49.19/11.71 fof(f63,plain,(
% 49.19/11.71 ![X0]: (and(X0,X0)=X0)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f16])).
% 49.19/11.71 fof(f65,plain,(
% 49.19/11.71 ![X0,X1]: (and(and(X0,X1),X0)=and(X0,X1))),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f18])).
% 49.19/11.71 fof(f66,plain,(
% 49.19/11.71 ![X0]: (or(X0,X0)=X0)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f19])).
% 49.19/11.71 fof(f68,plain,(
% 49.19/11.71 ![X0,X1]: (or(or(X0,X1),X0)=or(X0,X1))),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f21])).
% 49.19/11.71 fof(f69,plain,(
% 49.19/11.71 ![X0]: (and(X0,not(X0))=n0)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f22])).
% 49.19/11.71 fof(f72,plain,(
% 49.19/11.71 ![X0]: (or(X0,not(X0))=n1)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f25])).
% 49.19/11.71 fof(f75,plain,(
% 49.19/11.71 ![X0]: (not(not(X0))=X0)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f28])).
% 49.19/11.71 fof(f76,plain,(
% 49.19/11.71 ![X0,X1]: (or(and(X0,X1),and(X0,not(X1)))=X0)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f29])).
% 49.19/11.71 fof(f78,plain,(
% 49.19/11.71 a1=and(b1,b3)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f31])).
% 49.19/11.71 fof(f79,plain,(
% 49.19/11.71 a2=and(b2,b3)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f32])).
% 49.19/11.71 fof(f80,plain,(
% 49.19/11.71 b1=not(d1)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f33])).
% 49.19/11.71 fof(f81,plain,(
% 49.19/11.71 b2=not(d2)),
% 49.19/11.71 inference(cnf_transformation,[status(thm)],[f34])).
% 49.19/11.72 fof(f82,plain,(
% 49.19/11.72 b3=or(c1,c2)),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f35])).
% 49.19/11.72 fof(f83,plain,(
% 49.19/11.72 c1=or(d1,d3)),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f36])).
% 49.19/11.72 fof(f84,plain,(
% 49.19/11.72 c2=or(d2,d3)),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f37])).
% 49.19/11.72 fof(f85,plain,(
% 49.19/11.72 d3=f3),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f38])).
% 49.19/11.72 fof(f86,plain,(
% 49.19/11.72 d1=not(e1)),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f39])).
% 49.19/11.72 fof(f87,plain,(
% 49.19/11.72 d2=not(e2)),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f40])).
% 49.19/11.72 fof(f88,plain,(
% 49.19/11.72 e1=or(f1,f3)),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f41])).
% 49.19/11.72 fof(f89,plain,(
% 49.19/11.72 e2=or(f2,f3)),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f42])).
% 49.19/11.72 fof(f90,plain,(
% 49.19/11.72 f1=not(i1)),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f43])).
% 49.19/11.72 fof(f91,plain,(
% 49.19/11.72 f2=not(i2)),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f44])).
% 49.19/11.72 fof(f92,plain,(
% 49.19/11.72 f3=and(i1,i2)),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f45])).
% 49.19/11.72 fof(f93,plain,(
% 49.19/11.72 circuit(input(i1,i2),output(a1,a2))),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f46])).
% 49.19/11.72 fof(f94,plain,(
% 49.19/11.72 ~circuit(input(i1,i2),output(i2,i1))),
% 49.19/11.72 inference(cnf_transformation,[status(thm)],[f47])).
% 49.19/11.72 fof(f95,plain,(
% 49.19/11.72 ![X0,X1,X2]: (or(X0,or(X1,X2))=or(or(X0,X2),X1))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f57,f58])).
% 49.19/11.72 fof(f96,plain,(
% 49.19/11.72 ![X0,X1,X2]: (and(X0,and(X1,X2))=and(and(X0,X2),X1))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f56,f59])).
% 49.19/11.72 fof(f98,plain,(
% 49.19/11.72 ![X0,X1]: (and(X0,and(X0,X1))=and(X0,X1))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f96,f65])).
% 49.19/11.72 fof(f100,plain,(
% 49.19/11.72 ![X0,X1]: (or(X0,or(X0,X1))=or(X0,X1))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f95,f68])).
% 49.19/11.72 fof(f109,plain,(
% 49.19/11.72 a2=and(b3,b2)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f54,f79])).
% 49.19/11.72 fof(f110,plain,(
% 49.19/11.72 e1=or(f3,f1)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f55,f88])).
% 49.19/11.72 fof(f111,plain,(
% 49.19/11.72 e1=or(d3,f1)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f85,f110])).
% 49.19/11.72 fof(f112,plain,(
% 49.19/11.72 e2=or(f3,f2)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f55,f89])).
% 49.19/11.72 fof(f113,plain,(
% 49.19/11.72 e2=or(d3,f2)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f85,f112])).
% 49.19/11.72 fof(f114,plain,(
% 49.19/11.72 d3=and(i1,i2)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f85,f92])).
% 49.19/11.72 fof(f123,plain,(
% 49.19/11.72 ![X0]: (and(n1,X0)=X0)),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f54,f49])).
% 49.19/11.72 fof(f135,plain,(
% 49.19/11.72 ![X0]: (or(n0,X0)=X0)),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f55,f50])).
% 49.19/11.72 fof(f141,plain,(
% 49.19/11.72 ![X0]: (or(n1,X0)=n1)),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f55,f51])).
% 49.19/11.72 fof(f148,plain,(
% 49.19/11.72 not(f2)=i2),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f91,f75])).
% 49.19/11.72 fof(f149,plain,(
% 49.19/11.72 not(f1)=i1),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f90,f75])).
% 49.19/11.72 fof(f150,plain,(
% 49.19/11.72 not(d2)=e2),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f87,f75])).
% 49.19/11.72 fof(f153,plain,(
% 49.19/11.72 not(d1)=e1),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f86,f75])).
% 49.19/11.72 fof(f154,plain,(
% 49.19/11.72 not(b2)=d2),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f81,f75])).
% 49.19/11.72 fof(f155,plain,(
% 49.19/11.72 not(b1)=d1),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f80,f75])).
% 49.19/11.72 fof(f157,plain,(
% 49.19/11.72 b2=or(d3,f2)),
% 49.19/11.72 inference(backward_demodulation,[status(thm)],[f158,f113])).
% 49.19/11.72 fof(f158,plain,(
% 49.19/11.72 b2=e2),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f81,f150])).
% 49.19/11.72 fof(f160,plain,(
% 49.19/11.72 b1=or(d3,f1)),
% 49.19/11.72 inference(backward_demodulation,[status(thm)],[f161,f111])).
% 49.19/11.72 fof(f161,plain,(
% 49.19/11.72 b1=e1),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f80,f153])).
% 49.19/11.72 fof(f193,plain,(
% 49.19/11.72 ![X0]: (or(d1,or(d3,X0))=or(c1,X0))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f83,f57])).
% 49.19/11.72 fof(f194,plain,(
% 49.19/11.72 ![X0]: (or(c1,or(c2,X0))=or(b3,X0))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f82,f57])).
% 49.19/11.72 fof(f257,plain,(
% 49.19/11.72 ![X0]: (or(d1,or(X0,d3))=or(c1,X0))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f83,f95])).
% 49.19/11.72 fof(f263,plain,(
% 49.19/11.72 ![X0,X1]: (or(X0,or(X1,X0))=or(X0,X1))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f66,f95])).
% 49.19/11.72 fof(f350,plain,(
% 49.19/11.72 ![X0]: (not(and(X0,i1))=or(not(X0),f1))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f90,f60])).
% 49.19/11.72 fof(f368,plain,(
% 49.19/11.72 ![X0]: (not(and(X0,i1))=or(f1,not(X0)))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f55,f350])).
% 49.19/11.72 fof(f375,plain,(
% 49.19/11.72 ![X0]: (or(d2,or(d3,X0))=or(c2,X0))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f84,f57])).
% 49.19/11.72 fof(f393,plain,(
% 49.19/11.72 ![X0]: (or(d3,or(f2,X0))=or(b2,X0))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f157,f57])).
% 49.19/11.72 fof(f394,plain,(
% 49.19/11.72 ![X0]: (or(d3,or(X0,f1))=or(b1,X0))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f160,f95])).
% 49.19/11.72 fof(f395,plain,(
% 49.19/11.72 ![X0]: (or(d3,or(f1,X0))=or(b1,X0))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f160,f57])).
% 49.19/11.72 fof(f400,plain,(
% 49.19/11.72 and(i1,d3)=and(i1,i2)),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f114,f98])).
% 49.19/11.72 fof(f424,plain,(
% 49.19/11.72 and(d3,i1)=and(i1,i2)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f54,f400])).
% 49.19/11.72 fof(f425,plain,(
% 49.19/11.72 and(d3,i1)=d3),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f114,f424])).
% 49.19/11.72 fof(f462,plain,(
% 49.19/11.72 ![X0]: (not(or(d1,X0))=and(b1,not(X0)))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f80,f61])).
% 49.19/11.72 fof(f468,plain,(
% 49.19/11.72 ![X0]: (not(or(X0,i2))=and(not(X0),f2))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f91,f61])).
% 49.19/11.72 fof(f469,plain,(
% 49.19/11.72 ![X0]: (not(or(X0,i1))=and(not(X0),f1))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f90,f61])).
% 49.19/11.72 fof(f472,plain,(
% 49.19/11.72 ![X0]: (not(or(X0,d2))=and(not(X0),b2))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f81,f61])).
% 49.19/11.72 fof(f487,plain,(
% 49.19/11.72 ![X0]: (not(or(X0,i2))=and(f2,not(X0)))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f54,f468])).
% 49.19/11.72 fof(f488,plain,(
% 49.19/11.72 ![X0]: (not(or(X0,i1))=and(f1,not(X0)))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f54,f469])).
% 49.19/11.72 fof(f492,plain,(
% 49.19/11.72 ![X0]: (not(or(X0,d2))=and(b2,not(X0)))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f54,f472])).
% 49.19/11.72 fof(f502,plain,(
% 49.19/11.72 ![X0,X1]: (and(or(n1,X0),X1)=or(X1,and(X0,X1)))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f123,f62])).
% 49.19/11.72 fof(f512,plain,(
% 49.19/11.72 ![X0,X1]: (and(or(X0,X1),X0)=or(X0,and(X1,X0)))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f63,f62])).
% 49.19/11.72 fof(f534,plain,(
% 49.19/11.72 ![X0,X1]: (and(n1,X0)=or(X0,and(X1,X0)))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f141,f502])).
% 49.19/11.72 fof(f535,plain,(
% 49.19/11.72 ![X0,X1]: (X0=or(X0,and(X1,X0)))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f123,f534])).
% 49.19/11.72 fof(f543,plain,(
% 49.19/11.72 ![X0,X1]: (and(X0,or(X0,X1))=or(X0,and(X1,X0)))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f54,f512])).
% 49.19/11.72 fof(f544,plain,(
% 49.19/11.72 ![X0,X1]: (and(X0,or(X0,X1))=X0)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f535,f543])).
% 49.19/11.72 fof(f568,plain,(
% 49.19/11.72 ![X0]: (and(or(d3,X0),i1)=or(d3,and(X0,i1)))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f425,f62])).
% 49.19/11.72 fof(f574,plain,(
% 49.19/11.72 ![X0]: (and(i1,or(d3,X0))=or(d3,and(X0,i1)))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f54,f568])).
% 49.19/11.72 fof(f600,plain,(
% 49.19/11.72 or(b1,d1)=n1),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f155,f72])).
% 49.19/11.72 fof(f601,plain,(
% 49.19/11.72 or(b2,d2)=n1),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f154,f72])).
% 49.19/11.72 fof(f602,plain,(
% 49.19/11.72 or(f1,i1)=n1),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f149,f72])).
% 49.19/11.72 fof(f603,plain,(
% 49.19/11.72 or(f2,i2)=n1),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f148,f72])).
% 49.19/11.72 fof(f730,plain,(
% 49.19/11.72 ![X0,X1]: (and(or(X0,X1),not(X1))=or(and(X0,not(X1)),n0))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f69,f62])).
% 49.19/11.72 fof(f731,plain,(
% 49.19/11.72 ![X0,X1]: (and(or(X0,X1),not(X0))=or(n0,and(X1,not(X0))))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f69,f62])).
% 49.19/11.72 fof(f746,plain,(
% 49.19/11.72 ![X0,X1]: (and(not(X0),or(X1,X0))=or(and(X1,not(X0)),n0))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f54,f730])).
% 49.19/11.72 fof(f747,plain,(
% 49.19/11.72 ![X0,X1]: (and(not(X0),or(X1,X0))=and(X1,not(X0)))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f50,f746])).
% 49.19/11.72 fof(f748,plain,(
% 49.19/11.72 ![X0,X1]: (and(not(X0),or(X0,X1))=or(n0,and(X1,not(X0))))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f54,f731])).
% 49.19/11.72 fof(f749,plain,(
% 49.19/11.72 ![X0,X1]: (and(not(X0),or(X0,X1))=and(X1,not(X0)))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f135,f748])).
% 49.19/11.72 fof(f878,plain,(
% 49.19/11.72 or(d3,and(i1,not(i2)))=i1),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f114,f76])).
% 49.19/11.72 fof(f914,plain,(
% 49.19/11.72 ![X0,X1]: (or(and(X0,X1),X0)=or(and(X0,X1),and(X0,not(X1))))),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f76,f100])).
% 49.19/11.72 fof(f921,plain,(
% 49.19/11.72 or(d3,and(i1,f2))=i1),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f91,f878])).
% 49.19/11.72 fof(f922,plain,(
% 49.19/11.72 or(d3,and(f2,i1))=i1),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f54,f921])).
% 49.19/11.72 fof(f923,plain,(
% 49.19/11.72 and(i1,or(d3,f2))=i1),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f574,f922])).
% 49.19/11.72 fof(f924,plain,(
% 49.19/11.72 and(i1,b2)=i1),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f157,f923])).
% 49.19/11.72 fof(f925,plain,(
% 49.19/11.72 and(b2,i1)=i1),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f54,f924])).
% 49.19/11.72 fof(f967,plain,(
% 49.19/11.72 ![X0,X1]: (or(X0,and(X0,X1))=or(and(X0,X1),and(X0,not(X1))))),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f55,f914])).
% 49.19/11.72 fof(f970,plain,(
% 49.19/11.72 ![X0,X1]: (or(X0,and(X0,X1))=X0)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f76,f967])).
% 49.19/11.72 fof(f1370,plain,(
% 49.19/11.72 or(d1,b1)=or(c1,f1)),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f160,f193])).
% 49.19/11.72 fof(f1371,plain,(
% 49.19/11.72 or(d1,b2)=or(c1,f2)),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f157,f193])).
% 49.19/11.72 fof(f1383,plain,(
% 49.19/11.72 or(b1,d1)=or(c1,f1)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f55,f1370])).
% 49.19/11.72 fof(f1384,plain,(
% 49.19/11.72 n1=or(c1,f1)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f600,f1383])).
% 49.19/11.72 fof(f1385,plain,(
% 49.19/11.72 or(b2,d1)=or(c1,f2)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f55,f1371])).
% 49.19/11.72 fof(f1831,plain,(
% 49.19/11.72 i1=or(i1,d3)),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f425,f535])).
% 49.19/11.72 fof(f1833,plain,(
% 49.19/11.72 i2=or(i2,d3)),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f114,f535])).
% 49.19/11.72 fof(f1870,plain,(
% 49.19/11.72 i1=or(d3,i1)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f55,f1831])).
% 49.19/11.72 fof(f1872,plain,(
% 49.19/11.72 i2=or(d3,i2)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f55,f1833])).
% 49.19/11.72 fof(f1904,plain,(
% 49.19/11.72 or(d1,i1)=or(c1,i1)),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f1870,f193])).
% 49.19/11.72 fof(f2320,plain,(
% 49.19/11.72 or(d1,c2)=or(c1,d2)),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f84,f257])).
% 49.19/11.72 fof(f2354,plain,(
% 49.19/11.72 or(d1,c2)=or(d2,c1)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f55,f2320])).
% 49.19/11.72 fof(f3836,plain,(
% 49.19/11.72 or(d3,c2)=or(d3,d2)),
% 49.19/11.72 inference(paramodulation,[status(thm)],[f84,f263])).
% 49.19/11.72 fof(f3966,plain,(
% 49.19/11.72 or(c2,d3)=or(d3,d2)),
% 49.19/11.72 inference(forward_demodulation,[status(thm)],[f55,f3836])).
% 49.19/11.72 fof(f3967,plain,(
% 49.19/11.73 or(c2,d3)=or(d2,d3)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f55,f3966])).
% 49.19/11.73 fof(f3968,plain,(
% 49.19/11.73 or(c2,d3)=c2),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f84,f3967])).
% 49.19/11.73 fof(f5349,plain,(
% 49.19/11.73 or(d1,c2)=or(c1,c2)),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f3968,f257])).
% 49.19/11.73 fof(f5364,plain,(
% 49.19/11.73 b3=or(d2,c1)),
% 49.19/11.73 inference(backward_demodulation,[status(thm)],[f5365,f2354])).
% 49.19/11.73 fof(f5365,plain,(
% 49.19/11.73 or(d1,c2)=b3),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f82,f5349])).
% 49.19/11.73 fof(f9786,plain,(
% 49.19/11.73 not(i1)=or(f1,not(b2))),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f925,f368])).
% 49.19/11.73 fof(f9831,plain,(
% 49.19/11.73 f1=or(f1,not(b2))),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f90,f9786])).
% 49.19/11.73 fof(f9832,plain,(
% 49.19/11.73 f1=or(f1,d2)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f154,f9831])).
% 49.19/11.73 fof(f9833,plain,(
% 49.19/11.73 f1=or(d2,f1)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f55,f9832])).
% 49.19/11.73 fof(f11569,plain,(
% 49.19/11.73 or(d2,i2)=or(c2,i2)),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f1872,f375])).
% 49.19/11.73 fof(f11571,plain,(
% 49.19/11.73 or(d2,b1)=or(c2,f1)),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f160,f375])).
% 49.19/11.73 fof(f11572,plain,(
% 49.19/11.73 or(d2,b2)=or(c2,f2)),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f157,f375])).
% 49.19/11.73 fof(f11625,plain,(
% 49.19/11.73 or(b1,d2)=or(c2,f1)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f55,f11571])).
% 49.19/11.73 fof(f11626,plain,(
% 49.19/11.73 or(b2,d2)=or(c2,f2)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f55,f11572])).
% 49.19/11.73 fof(f11627,plain,(
% 49.19/11.73 n1=or(c2,f2)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f601,f11626])).
% 49.19/11.73 fof(f11682,plain,(
% 49.19/11.73 or(c1,n1)=or(b3,f2)),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f11627,f194])).
% 49.19/11.73 fof(f11696,plain,(
% 49.19/11.73 n1=or(b3,f2)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f51,f11682])).
% 49.19/11.73 fof(f12953,plain,(
% 49.19/11.73 or(d3,n1)=or(b2,i2)),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f603,f393])).
% 49.19/11.73 fof(f13008,plain,(
% 49.19/11.73 n1=or(b2,i2)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f51,f12953])).
% 49.19/11.73 fof(f13080,plain,(
% 49.19/11.73 or(d3,f1)=or(b1,d2)),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f9833,f394])).
% 49.19/11.73 fof(f13126,plain,(
% 49.19/11.73 b1=or(c2,f1)),
% 49.19/11.73 inference(backward_demodulation,[status(thm)],[f13128,f11625])).
% 49.19/11.73 fof(f13128,plain,(
% 49.19/11.73 b1=or(b1,d2)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f160,f13080])).
% 49.19/11.73 fof(f13198,plain,(
% 49.19/11.73 or(d3,n1)=or(b1,i1)),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f602,f395])).
% 49.19/11.73 fof(f13256,plain,(
% 49.19/11.73 n1=or(b1,i1)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f51,f13198])).
% 49.19/11.73 fof(f14243,plain,(
% 49.19/11.73 and(c2,b1)=c2),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f13126,f544])).
% 49.19/11.73 fof(f14263,plain,(
% 49.19/11.73 and(b1,c2)=c2),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f54,f14243])).
% 49.19/11.73 fof(f14316,plain,(
% 49.19/11.73 or(c2,and(b1,not(c2)))=b1),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f14263,f76])).
% 49.19/11.73 fof(f15177,plain,(
% 49.19/11.73 not(b3)=and(b1,not(c2))),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f5365,f462])).
% 49.19/11.73 fof(f15227,plain,(
% 49.19/11.73 or(c2,not(b3))=b1),
% 49.19/11.73 inference(backward_demodulation,[status(thm)],[f15177,f14316])).
% 49.19/11.73 fof(f15891,plain,(
% 49.19/11.73 not(n1)=and(f2,not(b2))),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f13008,f487])).
% 49.19/11.73 fof(f15940,plain,(
% 49.19/11.73 n0=and(f2,not(b2))),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f53,f15891])).
% 49.19/11.73 fof(f15941,plain,(
% 49.19/11.73 n0=and(f2,d2)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f154,f15940])).
% 49.19/11.73 fof(f15942,plain,(
% 49.19/11.73 n0=and(d2,f2)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f54,f15941])).
% 49.19/11.73 fof(f16017,plain,(
% 49.19/11.73 or(n0,and(d2,not(f2)))=d2),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f15942,f76])).
% 49.19/11.73 fof(f16045,plain,(
% 49.19/11.73 and(d2,not(f2))=d2),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f135,f16017])).
% 49.19/11.73 fof(f16046,plain,(
% 49.19/11.73 and(d2,i2)=d2),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f148,f16045])).
% 49.19/11.73 fof(f16170,plain,(
% 49.19/11.73 i2=or(i2,d2)),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f16046,f535])).
% 49.19/11.73 fof(f16193,plain,(
% 49.19/11.73 i2=or(c2,i2)),
% 49.19/11.73 inference(backward_demodulation,[status(thm)],[f16194,f11569])).
% 49.19/11.73 fof(f16194,plain,(
% 49.19/11.73 i2=or(d2,i2)),
% 49.19/11.73 inference(forward_demodulation,[status(thm)],[f55,f16170])).
% 49.19/11.73 fof(f16208,plain,(
% 49.19/11.73 and(c2,i2)=c2),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f16193,f544])).
% 49.19/11.73 fof(f16262,plain,(
% 49.19/11.73 not(n1)=and(f1,not(b1))),
% 49.19/11.73 inference(paramodulation,[status(thm)],[f13256,f488])).
% 47.50/11.73 fof(f16314,plain,(
% 47.50/11.73 n0=and(f1,not(b1))),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f53,f16262])).
% 47.50/11.73 fof(f16315,plain,(
% 47.50/11.73 n0=and(f1,d1)),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f155,f16314])).
% 47.50/11.73 fof(f16316,plain,(
% 47.50/11.73 n0=and(d1,f1)),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f54,f16315])).
% 47.50/11.73 fof(f16384,plain,(
% 47.50/11.73 not(b1)=and(b2,not(b1))),
% 47.50/11.73 inference(paramodulation,[status(thm)],[f13128,f492])).
% 47.50/11.73 fof(f16434,plain,(
% 47.50/11.73 d1=and(b2,not(b1))),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f155,f16384])).
% 47.50/11.73 fof(f16435,plain,(
% 47.50/11.73 d1=and(b2,d1)),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f155,f16434])).
% 47.50/11.73 fof(f16659,plain,(
% 47.50/11.73 or(n0,and(d1,not(f1)))=d1),
% 47.50/11.73 inference(paramodulation,[status(thm)],[f16316,f76])).
% 47.50/11.73 fof(f16687,plain,(
% 47.50/11.73 and(d1,not(f1))=d1),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f135,f16659])).
% 47.50/11.73 fof(f16688,plain,(
% 47.50/11.73 and(d1,i1)=d1),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f149,f16687])).
% 47.50/11.73 fof(f16848,plain,(
% 47.50/11.73 or(b2,d1)=b2),
% 47.50/11.73 inference(paramodulation,[status(thm)],[f16435,f970])).
% 47.50/11.73 fof(f16871,plain,(
% 47.50/11.73 b2=or(c1,f2)),
% 47.50/11.73 inference(backward_demodulation,[status(thm)],[f16848,f1385])).
% 47.50/11.73 fof(f17854,plain,(
% 47.50/11.73 and(c1,b2)=c1),
% 47.50/11.73 inference(paramodulation,[status(thm)],[f16871,f544])).
% 47.50/11.73 fof(f17872,plain,(
% 47.50/11.73 and(b2,c1)=c1),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f54,f17854])).
% 47.50/11.73 fof(f22109,plain,(
% 47.50/11.73 i1=or(i1,d1)),
% 47.50/11.73 inference(paramodulation,[status(thm)],[f16688,f535])).
% 47.50/11.73 fof(f22142,plain,(
% 47.50/11.73 i1=or(c1,i1)),
% 47.50/11.73 inference(backward_demodulation,[status(thm)],[f22143,f1904])).
% 47.50/11.73 fof(f22143,plain,(
% 47.50/11.73 i1=or(d1,i1)),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f55,f22109])).
% 47.50/11.73 fof(f22158,plain,(
% 47.50/11.73 and(c1,i1)=c1),
% 47.50/11.73 inference(paramodulation,[status(thm)],[f22142,f544])).
% 47.50/11.73 fof(f34196,plain,(
% 47.50/11.73 and(not(not(b3)),b1)=and(c2,not(not(b3)))),
% 47.50/11.73 inference(paramodulation,[status(thm)],[f15227,f747])).
% 47.50/11.73 fof(f34198,plain,(
% 47.50/11.73 and(not(f2),n1)=and(c2,not(f2))),
% 47.50/11.73 inference(paramodulation,[status(thm)],[f11627,f747])).
% 47.50/11.73 fof(f34217,plain,(
% 47.50/11.73 and(not(f2),n1)=and(b3,not(f2))),
% 47.50/11.73 inference(paramodulation,[status(thm)],[f11696,f747])).
% 47.50/11.73 fof(f34322,plain,(
% 47.50/11.73 and(not(f1),n1)=and(c1,not(f1))),
% 47.50/11.73 inference(paramodulation,[status(thm)],[f1384,f747])).
% 47.50/11.73 fof(f34470,plain,(
% 47.50/11.73 and(b1,not(not(b3)))=and(c2,not(not(b3)))),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f54,f34196])).
% 47.50/11.73 fof(f34471,plain,(
% 47.50/11.73 and(b1,b3)=and(c2,not(not(b3)))),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f75,f34470])).
% 47.50/11.73 fof(f34472,plain,(
% 47.50/11.73 a1=and(c2,not(not(b3)))),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f78,f34471])).
% 47.50/11.73 fof(f34473,plain,(
% 47.50/11.73 a1=and(c2,b3)),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f75,f34472])).
% 47.50/11.73 fof(f34475,plain,(
% 47.50/11.73 a1=and(b3,c2)),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f54,f34473])).
% 47.50/11.73 fof(f34479,plain,(
% 47.50/11.73 not(f2)=and(c2,not(f2))),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f49,f34198])).
% 47.50/11.73 fof(f34480,plain,(
% 47.50/11.73 i2=and(c2,not(f2))),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f148,f34479])).
% 47.50/11.73 fof(f34481,plain,(
% 47.50/11.73 i2=and(c2,i2)),
% 47.50/11.73 inference(forward_demodulation,[status(thm)],[f148,f34480])).
% 47.50/11.76 fof(f34500,plain,(
% 47.50/11.76 ~circuit(input(i1,i2),output(c2,i1))),
% 47.50/11.76 inference(backward_demodulation,[status(thm)],[f34732,f94])).
% 47.50/11.76 fof(f34502,plain,(
% 47.50/11.76 circuit(input(i1,c2),output(a1,a2))),
% 47.50/11.76 inference(backward_demodulation,[status(thm)],[f34732,f93])).
% 47.50/11.76 fof(f34732,plain,(
% 47.50/11.76 i2=c2),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f16208,f34481])).
% 47.50/11.76 fof(f34773,plain,(
% 47.50/11.76 not(f2)=and(b3,not(f2))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f49,f34217])).
% 47.50/11.76 fof(f34774,plain,(
% 47.50/11.76 i2=and(b3,not(f2))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f148,f34773])).
% 47.50/11.76 fof(f34775,plain,(
% 47.50/11.76 c2=and(b3,not(f2))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f34732,f34774])).
% 47.50/11.76 fof(f34776,plain,(
% 47.50/11.76 c2=and(b3,i2)),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f148,f34775])).
% 47.50/11.76 fof(f34777,plain,(
% 47.50/11.76 c2=and(b3,c2)),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f34732,f34776])).
% 47.50/11.76 fof(f35106,plain,(
% 47.50/11.76 c2=a1),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f34475,f34777])).
% 47.50/11.76 fof(f35445,plain,(
% 47.50/11.76 not(f1)=and(c1,not(f1))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f49,f34322])).
% 47.50/11.76 fof(f35446,plain,(
% 47.50/11.76 i1=and(c1,not(f1))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f149,f35445])).
% 47.50/11.76 fof(f35447,plain,(
% 47.50/11.76 i1=and(c1,i1)),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f149,f35446])).
% 47.50/11.76 fof(f35732,plain,(
% 47.50/11.76 i1=c1),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f22158,f35447])).
% 47.50/11.76 fof(f35880,plain,(
% 47.50/11.76 ~circuit(input(c1,i2),output(c2,i1))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f35732,f34500])).
% 47.50/11.76 fof(f35881,plain,(
% 47.50/11.76 ~circuit(input(c1,c2),output(c2,i1))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f34732,f35880])).
% 47.50/11.76 fof(f35882,plain,(
% 47.50/11.76 ~circuit(input(c1,a1),output(c2,i1))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f35106,f35881])).
% 47.50/11.76 fof(f35883,plain,(
% 47.50/11.76 ~circuit(input(c1,a1),output(a1,i1))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f35106,f35882])).
% 47.50/11.76 fof(f35884,plain,(
% 47.50/11.76 ~circuit(input(c1,a1),output(a1,c1))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f35732,f35883])).
% 47.50/11.76 fof(f35888,plain,(
% 47.50/11.76 circuit(input(c1,c2),output(a1,a2))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f35732,f34502])).
% 47.50/11.76 fof(f35889,plain,(
% 47.50/11.76 circuit(input(c1,a1),output(a1,a2))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f35106,f35888])).
% 47.50/11.76 fof(f38009,plain,(
% 47.50/11.76 and(not(d2),b3)=and(c1,not(d2))),
% 47.50/11.76 inference(paramodulation,[status(thm)],[f5364,f749])).
% 47.50/11.76 fof(f38372,plain,(
% 47.50/11.76 and(b3,not(d2))=and(c1,not(d2))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f54,f38009])).
% 47.50/11.76 fof(f38373,plain,(
% 47.50/11.76 and(b3,b2)=and(c1,not(d2))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f81,f38372])).
% 47.50/11.76 fof(f38374,plain,(
% 47.50/11.76 a2=and(c1,not(d2))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f109,f38373])).
% 47.50/11.76 fof(f38375,plain,(
% 47.50/11.76 a2=and(c1,b2)),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f81,f38374])).
% 47.50/11.76 fof(f38376,plain,(
% 47.50/11.76 a2=c1),
% 47.50/11.76 inference(backward_demodulation,[status(thm)],[f38377,f17872])).
% 47.50/11.76 fof(f38377,plain,(
% 47.50/11.76 a2=and(b2,c1)),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f54,f38375])).
% 47.50/11.76 fof(f38546,plain,(
% 47.50/11.76 circuit(input(a2,a1),output(a1,a2))),
% 47.50/11.76 inference(backward_demodulation,[status(thm)],[f38376,f35889])).
% 47.50/11.76 fof(f38548,plain,(
% 47.50/11.76 ~circuit(input(c1,a1),output(a1,a2))),
% 47.50/11.76 inference(backward_demodulation,[status(thm)],[f38376,f35884])).
% 47.50/11.76 fof(f39021,plain,(
% 47.50/11.76 ~circuit(input(a2,a1),output(a1,a2))),
% 47.50/11.76 inference(forward_demodulation,[status(thm)],[f38376,f38548])).
% 47.50/11.76 fof(f39022,plain,(
% 47.50/11.76 $false),
% 47.50/11.76 inference(forward_subsumption_resolution,[status(thm)],[f39021,f38546])).
% 47.50/11.76 % SZS output end CNFRefutation for theBenchmark.p
% 47.50/11.78 % Elapsed time: 6.382517 seconds
% 47.50/11.78 % CPU time: 50.408403 seconds
% 47.50/11.78 % Total memory used: 182.802 MB
% 47.50/11.78 % Net memory used: 176.236 MB
%------------------------------------------------------------------------------