%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL109-6 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:09:23 PM UTC 2026
% Result : Unsatisfiable 11.95s 6.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL109-6 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n013.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 00:05:12 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 11.95/6.91 % Refutation found
% 11.95/6.91 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 11.95/6.91 % SZS output start CNFRefutation for theBenchmark
% 11.95/6.91 fof(f1,axiom,(
% 11.95/6.91 (![X]: (not(X) = xor(X,truth) ))),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f2,axiom,(
% 11.95/6.91 (![X]: (xor(X,falsehood) = X ))),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f4,axiom,(
% 11.95/6.91 (![X]: (and_star(X,truth) = X ))),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f5,axiom,(
% 11.95/6.91 (![X]: (and_star(X,falsehood) = falsehood ))),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f6,axiom,(
% 11.95/6.91 (![X]: (and_star(xor(truth,X),X) = falsehood ))),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f7,axiom,(
% 11.95/6.91 (![X,Y]: (xor(X,xor(truth,Y)) = xor(xor(X,truth),Y) ))),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f8,axiom,(
% 11.95/6.91 (![X,Y]: (and_star(xor(and_star(xor(truth,X),Y),truth),Y) = and_star(xor(and_star(xor(truth,Y),X),truth),X) ))),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f9,axiom,(
% 11.95/6.91 (![X,Y]: (xor(X,Y) = xor(Y,X) ))),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f10,axiom,(
% 11.95/6.91 (![X,Y,Z]: (and_star(and_star(X,Y),Z) = and_star(X,and_star(Y,Z)) ))),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f11,axiom,(
% 11.95/6.91 (![X,Y]: (and_star(X,Y) = and_star(Y,X) ))),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f12,axiom,(
% 11.95/6.91 not(truth) = falsehood ),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f13,axiom,(
% 11.95/6.91 (![X,Y]: (implies(X,Y) = xor(truth,and_star(X,xor(truth,Y))) ))),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f14,negated_conjecture,(
% 11.95/6.91 implies(implies(implies(a,b),implies(b,a)),implies(b,a)) != truth ),
% 11.95/6.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.95/6.91 fof(f15,plain,(
% 11.95/6.91 ![X0]: (not(X0)=xor(X0,truth))),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f1])).
% 11.95/6.91 fof(f16,plain,(
% 11.95/6.91 ![X0]: (xor(X0,falsehood)=X0)),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f2])).
% 11.95/6.91 fof(f18,plain,(
% 11.95/6.91 ![X0]: (and_star(X0,truth)=X0)),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f4])).
% 11.95/6.91 fof(f19,plain,(
% 11.95/6.91 ![X0]: (and_star(X0,falsehood)=falsehood)),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f5])).
% 11.95/6.91 fof(f20,plain,(
% 11.95/6.91 ![X0]: (and_star(xor(truth,X0),X0)=falsehood)),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f6])).
% 11.95/6.91 fof(f21,plain,(
% 11.95/6.91 ![X0,X1]: (xor(X0,xor(truth,X1))=xor(xor(X0,truth),X1))),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f7])).
% 11.95/6.91 fof(f22,plain,(
% 11.95/6.91 ![X0,X1]: (and_star(xor(and_star(xor(truth,X0),X1),truth),X1)=and_star(xor(and_star(xor(truth,X1),X0),truth),X0))),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f8])).
% 11.95/6.91 fof(f23,plain,(
% 11.95/6.91 ![X0,X1]: (xor(X0,X1)=xor(X1,X0))),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f9])).
% 11.95/6.91 fof(f24,plain,(
% 11.95/6.91 ![X0,X1,X2]: (and_star(and_star(X0,X1),X2)=and_star(X0,and_star(X1,X2)))),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f10])).
% 11.95/6.91 fof(f25,plain,(
% 11.95/6.91 ![X0,X1]: (and_star(X0,X1)=and_star(X1,X0))),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f11])).
% 11.95/6.91 fof(f26,plain,(
% 11.95/6.91 not(truth)=falsehood),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f12])).
% 11.95/6.91 fof(f27,plain,(
% 11.95/6.91 ![X0,X1]: (implies(X0,X1)=xor(truth,and_star(X0,xor(truth,X1))))),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f13])).
% 11.95/6.91 fof(f28,plain,(
% 11.95/6.91 ~implies(implies(implies(a,b),implies(b,a)),implies(b,a))=truth),
% 11.95/6.91 inference(cnf_transformation,[status(thm)],[f14])).
% 11.95/6.91 fof(f48,plain,(
% 11.95/6.91 ![X0]: (not(X0)=xor(truth,X0))),
% 11.95/6.91 inference(paramodulation,[status(thm)],[f15,f23])).
% 11.95/6.91 fof(f49,plain,(
% 11.95/6.91 ![X0]: (X0=xor(falsehood,X0))),
% 11.95/6.91 inference(paramodulation,[status(thm)],[f16,f23])).
% 11.95/6.91 fof(f56,plain,(
% 11.95/6.91 ![X0]: (and_star(xor(X0,truth),X0)=falsehood)),
% 11.95/6.91 inference(paramodulation,[status(thm)],[f23,f20])).
% 11.95/6.91 fof(f62,plain,(
% 11.95/6.91 ![X0]: (and_star(not(X0),X0)=falsehood)),
% 11.95/6.91 inference(forward_demodulation,[status(thm)],[f15,f56])).
% 11.95/6.91 fof(f64,plain,(
% 11.95/6.91 truth=not(falsehood)),
% 11.95/6.91 inference(paramodulation,[status(thm)],[f15,f49])).
% 11.95/6.91 fof(f74,plain,(
% 11.95/6.91 ![X0,X1]: (xor(X0,xor(truth,X1))=xor(not(X0),X1))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f15,f21])).
% 11.95/6.92 fof(f80,plain,(
% 11.95/6.92 ![X0]: (xor(X0,not(truth))=xor(not(X0),truth))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f15,f74])).
% 11.95/6.92 fof(f94,plain,(
% 11.95/6.92 ![X0]: (xor(X0,falsehood)=xor(not(X0),truth))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f26,f80])).
% 11.95/6.92 fof(f95,plain,(
% 11.95/6.92 ![X0]: (X0=xor(not(X0),truth))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f16,f94])).
% 11.95/6.92 fof(f96,plain,(
% 11.95/6.92 ![X0]: (X0=not(not(X0)))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f15,f95])).
% 11.95/6.92 fof(f109,plain,(
% 11.95/6.92 ![X0]: (falsehood=and_star(falsehood,X0))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f19,f25])).
% 11.95/6.92 fof(f110,plain,(
% 11.95/6.92 ![X0]: (X0=and_star(truth,X0))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f18,f25])).
% 11.95/6.92 fof(f129,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(X0,xor(and_star(xor(truth,X1),X0),truth))=and_star(xor(and_star(xor(truth,X0),X1),truth),X1))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f25,f22])).
% 11.95/6.92 fof(f130,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(X0,not(and_star(xor(truth,X1),X0)))=and_star(xor(and_star(xor(truth,X0),X1),truth),X1))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f15,f129])).
% 11.95/6.92 fof(f131,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(X0,not(and_star(xor(truth,X1),X0)))=and_star(X1,xor(and_star(xor(truth,X0),X1),truth)))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f25,f130])).
% 11.95/6.92 fof(f132,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(X0,not(and_star(xor(truth,X1),X0)))=and_star(X1,not(and_star(xor(truth,X0),X1))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f15,f131])).
% 11.95/6.92 fof(f136,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(not(and_star(xor(truth,X0),xor(truth,X1))),not(and_star(X0,not(and_star(xor(truth,xor(truth,X1)),X0)))))=and_star(X1,not(and_star(xor(truth,not(and_star(xor(truth,X0),xor(truth,X1)))),X1))))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f132,f132])).
% 11.95/6.92 fof(f168,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(not(and_star(xor(truth,X0),xor(truth,X1))),not(and_star(X0,not(and_star(xor(not(truth),X1),X0)))))=and_star(X1,not(and_star(xor(truth,not(and_star(xor(truth,X0),xor(truth,X1)))),X1))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f74,f136])).
% 11.95/6.92 fof(f169,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(not(and_star(xor(truth,X0),xor(truth,X1))),not(and_star(X0,not(and_star(xor(falsehood,X1),X0)))))=and_star(X1,not(and_star(xor(truth,not(and_star(xor(truth,X0),xor(truth,X1)))),X1))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f26,f168])).
% 11.95/6.92 fof(f170,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(not(and_star(xor(truth,X0),xor(truth,X1))),not(and_star(X0,not(and_star(X1,X0)))))=and_star(X1,not(and_star(xor(truth,not(and_star(xor(truth,X0),xor(truth,X1)))),X1))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f49,f169])).
% 11.95/6.92 fof(f171,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(not(and_star(xor(truth,X0),xor(truth,X1))),not(and_star(X0,not(and_star(X1,X0)))))=and_star(X1,not(and_star(X1,xor(truth,not(and_star(xor(truth,X0),xor(truth,X1))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f25,f170])).
% 11.95/6.92 fof(f257,plain,(
% 11.95/6.92 ![X0,X1,X2]: (and_star(X0,and_star(X1,X2))=and_star(X1,and_star(X2,X0)))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f25,f24])).
% 11.95/6.92 fof(f266,plain,(
% 11.95/6.92 ![X0,X1,X2]: (and_star(and_star(X0,X1),X2)=and_star(X1,and_star(X0,X2)))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f25,f24])).
% 11.95/6.92 fof(f283,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(X0,not(and_star(xor(truth,X1),X0)))=and_star(X1,not(and_star(not(X0),X1))))),
% 11.95/6.92 inference(backward_demodulation,[status(thm)],[f48,f132])).
% 11.95/6.92 fof(f295,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(X0,not(and_star(not(X1),X0)))=and_star(X1,not(and_star(not(X0),X1))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f48,f283])).
% 11.95/6.92 fof(f296,plain,(
% 11.95/6.92 ![X0]: (and_star(X0,not(X0))=falsehood)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f25,f62])).
% 11.95/6.92 fof(f306,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(falsehood,X0)=and_star(X1,and_star(not(X1),X0)))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f296,f24])).
% 11.95/6.92 fof(f308,plain,(
% 11.95/6.92 ![X0,X1]: (falsehood=and_star(X0,and_star(not(X0),X1)))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f109,f306])).
% 11.95/6.92 fof(f310,plain,(
% 11.95/6.92 ![X0,X1]: (implies(X0,X1)=not(and_star(X0,xor(truth,X1))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f48,f27])).
% 11.95/6.92 fof(f311,plain,(
% 11.95/6.92 ![X0,X1]: (implies(X0,X1)=not(and_star(X0,not(X1))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f48,f310])).
% 11.95/6.92 fof(f314,plain,(
% 11.95/6.92 ![X0]: (implies(truth,X0)=not(not(X0)))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f110,f311])).
% 11.95/6.92 fof(f316,plain,(
% 11.95/6.92 ![X0,X1]: (implies(X0,X1)=not(and_star(not(X1),X0)))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f25,f311])).
% 11.95/6.92 fof(f319,plain,(
% 11.95/6.92 ![X0,X1]: (implies(X0,not(X1))=not(and_star(X0,X1)))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f96,f311])).
% 11.95/6.92 fof(f323,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(X0,not(X1))=not(implies(X0,X1)))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f311,f96])).
% 11.95/6.92 fof(f325,plain,(
% 11.95/6.92 ![X0]: (implies(truth,X0)=X0)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f96,f314])).
% 11.95/6.92 fof(f574,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(X0,not(and_star(not(X1),X0)))=and_star(X1,implies(X1,X0)))),
% 11.95/6.92 inference(backward_demodulation,[status(thm)],[f316,f295])).
% 11.95/6.92 fof(f575,plain,(
% 11.95/6.92 ![X0,X1]: (implies(not(X0),X1)=implies(not(X1),X0))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f311,f316])).
% 11.95/6.92 fof(f576,plain,(
% 11.95/6.92 ![X0,X1]: (implies(and_star(not(not(X0)),X1),X0)=not(falsehood))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f308,f316])).
% 11.95/6.92 fof(f584,plain,(
% 11.95/6.92 ![X0,X1]: (implies(X0,not(X1))=not(and_star(X1,X0)))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f96,f316])).
% 11.95/6.92 fof(f592,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(not(X0),X1)=not(implies(X1,X0)))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f316,f96])).
% 11.95/6.92 fof(f593,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(X0,implies(X0,X1))=and_star(X1,implies(X1,X0)))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f316,f574])).
% 11.95/6.92 fof(f594,plain,(
% 11.95/6.92 ![X0,X1]: (implies(and_star(X0,X1),X0)=not(falsehood))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f96,f576])).
% 11.95/6.92 fof(f595,plain,(
% 11.95/6.92 ![X0,X1]: (implies(and_star(X0,X1),X0)=truth)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f64,f594])).
% 11.95/6.92 fof(f614,plain,(
% 11.95/6.92 ![X0,X1]: (implies(and_star(X0,X1),X1)=truth)),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f25,f595])).
% 11.95/6.92 fof(f623,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(and_star(X0,and_star(X1,X2)),X2)=truth)),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f24,f614])).
% 11.95/6.92 fof(f769,plain,(
% 11.95/6.92 ![X0,X1]: (implies(not(implies(X0,X1)),not(X1))=truth)),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f323,f614])).
% 11.95/6.92 fof(f788,plain,(
% 11.95/6.92 ![X0,X1]: (not(and_star(not(implies(X0,X1)),X1))=truth)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f319,f769])).
% 11.95/6.92 fof(f789,plain,(
% 11.95/6.92 ![X0,X1]: (implies(X0,implies(X1,X0))=truth)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f316,f788])).
% 11.95/6.92 fof(f1036,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(X0,implies(X1,X2))=not(and_star(and_star(not(X2),X1),X0)))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f316,f584])).
% 11.95/6.92 fof(f1062,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(X0,implies(X1,X2))=not(and_star(not(X2),and_star(X1,X0))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f24,f1036])).
% 11.95/6.92 fof(f1063,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(X0,implies(X1,X2))=implies(and_star(X1,X0),X2))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f316,f1062])).
% 11.95/6.92 fof(f1134,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(not(implies(and_star(X0,X1),X2)),X1)=truth)),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f592,f623])).
% 11.95/6.92 fof(f1173,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(not(X0),implies(and_star(X1,X0),X2))=truth)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f575,f1134])).
% 11.95/6.92 fof(f1731,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(not(and_star(X0,not(and_star(X1,X0)))),and_star(xor(truth,X0),xor(truth,X1))))=and_star(X1,not(and_star(X1,xor(truth,not(and_star(xor(truth,X0),xor(truth,X1))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f592,f171])).
% 11.95/6.92 fof(f1732,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(not(not(implies(X0,and_star(X1,X0)))),and_star(xor(truth,X0),xor(truth,X1))))=and_star(X1,not(and_star(X1,xor(truth,not(and_star(xor(truth,X0),xor(truth,X1))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f323,f1731])).
% 11.95/6.92 fof(f1733,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(implies(X0,and_star(X1,X0)),and_star(xor(truth,X0),xor(truth,X1))))=and_star(X1,not(and_star(X1,xor(truth,not(and_star(xor(truth,X0),xor(truth,X1))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f96,f1732])).
% 11.95/6.92 fof(f1734,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(implies(X0,and_star(X1,X0)),and_star(not(X0),xor(truth,X1))))=and_star(X1,not(and_star(X1,xor(truth,not(and_star(xor(truth,X0),xor(truth,X1))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f48,f1733])).
% 11.95/6.92 fof(f1735,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(implies(X0,and_star(X1,X0)),not(implies(xor(truth,X1),X0))))=and_star(X1,not(and_star(X1,xor(truth,not(and_star(xor(truth,X0),xor(truth,X1))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f592,f1734])).
% 11.95/6.92 fof(f1736,plain,(
% 11.95/6.92 ![X0,X1]: (not(not(and_star(implies(xor(truth,X0),X1),implies(X1,and_star(X0,X1)))))=and_star(X0,not(and_star(X0,xor(truth,not(and_star(xor(truth,X1),xor(truth,X0))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f584,f1735])).
% 11.95/6.92 fof(f1737,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(xor(truth,X0),X1),implies(X1,and_star(X0,X1)))=and_star(X0,not(and_star(X0,xor(truth,not(and_star(xor(truth,X1),xor(truth,X0))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f96,f1736])).
% 11.95/6.92 fof(f1738,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=and_star(X0,not(and_star(X0,xor(truth,not(and_star(xor(truth,X1),xor(truth,X0))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f48,f1737])).
% 11.95/6.92 fof(f1739,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=not(implies(X0,and_star(X0,xor(truth,not(and_star(xor(truth,X1),xor(truth,X0))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f323,f1738])).
% 11.95/6.92 fof(f1740,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=not(implies(X0,and_star(X0,not(not(and_star(xor(truth,X1),xor(truth,X0))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f48,f1739])).
% 11.95/6.92 fof(f1741,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=not(implies(X0,not(implies(X0,not(and_star(xor(truth,X1),xor(truth,X0))))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f323,f1740])).
% 11.95/6.92 fof(f1742,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=not(not(and_star(implies(X0,not(and_star(xor(truth,X1),xor(truth,X0)))),X0))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f584,f1741])).
% 11.95/6.92 fof(f1743,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=and_star(implies(X0,not(and_star(xor(truth,X1),xor(truth,X0)))),X0))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f96,f1742])).
% 11.95/6.92 fof(f1744,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=and_star(X0,implies(X0,not(and_star(xor(truth,X1),xor(truth,X0))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f25,f1743])).
% 11.95/6.92 fof(f1745,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=and_star(X0,not(and_star(and_star(xor(truth,X1),xor(truth,X0)),X0))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f584,f1744])).
% 11.95/6.92 fof(f1746,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=not(implies(X0,and_star(and_star(xor(truth,X1),xor(truth,X0)),X0))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f323,f1745])).
% 11.95/6.92 fof(f1747,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=not(implies(X0,and_star(xor(truth,X0),and_star(xor(truth,X1),X0)))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f266,f1746])).
% 11.95/6.92 fof(f1748,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=not(implies(X0,and_star(X0,and_star(xor(truth,X0),xor(truth,X1))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f257,f1747])).
% 11.95/6.92 fof(f1749,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=not(implies(X0,and_star(X0,and_star(not(X0),xor(truth,X1))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f48,f1748])).
% 11.95/6.92 fof(f1750,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=not(implies(X0,and_star(X0,not(implies(xor(truth,X1),X0))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f592,f1749])).
% 11.95/6.92 fof(f1751,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=not(implies(X0,not(implies(X0,implies(xor(truth,X1),X0))))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f323,f1750])).
% 11.95/6.92 fof(f1752,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=not(not(and_star(implies(X0,implies(xor(truth,X1),X0)),X0))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f584,f1751])).
% 11.95/6.92 fof(f1753,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=and_star(implies(X0,implies(xor(truth,X1),X0)),X0))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f96,f1752])).
% 11.95/6.92 fof(f1754,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=and_star(X0,implies(X0,implies(xor(truth,X1),X0))))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f25,f1753])).
% 11.95/6.92 fof(f1755,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=and_star(X0,truth))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f789,f1754])).
% 11.95/6.92 fof(f1756,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(not(X0),X1),implies(X1,and_star(X0,X1)))=X0)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f18,f1755])).
% 11.95/6.92 fof(f1760,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(not(and_star(X0,not(X1))),implies(not(X0),and_star(X1,not(X0))))=X1)),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f584,f1756])).
% 11.95/6.92 fof(f1804,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(implies(not(X0),and_star(X1,not(X0))),and_star(X0,not(X1))))=X1)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f592,f1760])).
% 11.95/6.92 fof(f1805,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(implies(not(X0),not(implies(X1,X0))),and_star(X0,not(X1))))=X1)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f323,f1804])).
% 11.95/6.92 fof(f1806,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(not(and_star(implies(X0,X1),not(X1))),and_star(X1,not(X0))))=X0)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f584,f1805])).
% 11.95/6.92 fof(f1807,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(not(and_star(X0,not(X1))),and_star(implies(X1,X0),not(X0))))=X1)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f575,f1806])).
% 11.95/6.92 fof(f1808,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(not(not(implies(X0,X1))),and_star(implies(X1,X0),not(X0))))=X1)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f323,f1807])).
% 11.95/6.92 fof(f1809,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(implies(X0,X1),and_star(implies(X1,X0),not(X0))))=X1)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f96,f1808])).
% 11.95/6.92 fof(f1810,plain,(
% 11.95/6.92 ![X0,X1]: (not(implies(implies(X0,X1),not(implies(implies(X1,X0),X0))))=X1)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f323,f1809])).
% 11.95/6.92 fof(f1811,plain,(
% 11.95/6.92 ![X0,X1]: (not(not(and_star(implies(implies(X0,X1),X1),implies(X1,X0))))=X0)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f584,f1810])).
% 11.95/6.92 fof(f1812,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(implies(X0,X1),X1),implies(X1,X0))=X0)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f96,f1811])).
% 11.95/6.92 fof(f1813,plain,(
% 11.95/6.92 ![X0,X1]: (and_star(implies(X0,X1),implies(implies(X1,X0),X0))=X1)),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f25,f1812])).
% 11.95/6.92 fof(f1910,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(implies(X0,X1),implies(X0,X2))=implies(and_star(X1,implies(X1,X0)),X2))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f593,f1063])).
% 11.95/6.92 fof(f1915,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(X0,implies(X1,X2))=implies(and_star(X0,X1),X2))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f25,f1063])).
% 11.95/6.92 fof(f1957,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(implies(X0,X1),implies(X0,X2))=implies(implies(X1,X0),implies(X1,X2)))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f1063,f1910])).
% 11.95/6.92 fof(f2552,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(X0,implies(X1,X2))=implies(X1,implies(X0,X2)))),
% 11.95/6.92 inference(paramodulation,[status(thm)],[f1063,f1915])).
% 11.95/6.92 fof(f3301,plain,(
% 11.95/6.92 ~implies(implies(b,implies(implies(a,b),a)),implies(b,a))=truth),
% 11.95/6.92 inference(backward_demodulation,[status(thm)],[f2552,f28])).
% 11.95/6.92 fof(f3382,plain,(
% 11.95/6.92 ~implies(b,implies(implies(b,implies(implies(a,b),a)),a))=truth),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f2552,f3301])).
% 11.95/6.92 fof(f4230,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(X0,implies(implies(X0,X1),X2))=implies(implies(X1,X0),implies(X1,X2)))),
% 11.95/6.92 inference(forward_demodulation,[status(thm)],[f2552,f1957])).
% 11.95/6.92 fof(f4231,plain,(
% 11.95/6.92 ![X0,X1,X2]: (implies(X0,implies(implies(X0,X1),X2))=implies(X1,implies(implies(X1,X0),X2)))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f2552,f4230])).
% 11.95/6.94 fof(f6754,plain,(
% 11.95/6.94 ![X0,X1,X2]: (implies(not(X0),implies(X1,implies(X0,X2)))=truth)),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f1915,f1173])).
% 11.95/6.94 fof(f7246,plain,(
% 11.95/6.94 ![X0,X1]: (and_star(implies(not(implies(X0,X1)),implies(implies(X1,X0),X0)),implies(implies(implies(X1,X0),X0),X1))=implies(X0,X1))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f1813,f1756])).
% 11.95/6.94 fof(f7426,plain,(
% 11.95/6.94 ![X0,X1]: (and_star(implies(implies(implies(X0,X1),X1),X0),implies(not(implies(X1,X0)),implies(implies(X0,X1),X1)))=implies(X1,X0))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f25,f7246])).
% 11.95/6.94 fof(f7427,plain,(
% 11.95/6.94 ![X0,X1]: (and_star(implies(implies(implies(X0,X1),X1),X0),implies(implies(X0,X1),implies(not(implies(X1,X0)),X1)))=implies(X1,X0))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f2552,f7426])).
% 11.95/6.94 fof(f7428,plain,(
% 11.95/6.94 ![X0,X1]: (and_star(implies(implies(implies(X0,X1),X1),X0),implies(implies(X0,X1),implies(not(X1),implies(X1,X0))))=implies(X1,X0))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f575,f7427])).
% 11.95/6.94 fof(f7429,plain,(
% 11.95/6.94 ![X0,X1]: (and_star(implies(implies(implies(X0,X1),X1),X0),implies(not(X1),implies(implies(X0,X1),implies(X1,X0))))=implies(X1,X0))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f2552,f7428])).
% 11.95/6.94 fof(f7430,plain,(
% 11.95/6.94 ![X0,X1]: (and_star(implies(implies(implies(X0,X1),X1),X0),truth)=implies(X1,X0))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6754,f7429])).
% 11.95/6.94 fof(f7431,plain,(
% 11.95/6.94 ![X0,X1]: (implies(implies(implies(X0,X1),X1),X0)=implies(X1,X0))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f18,f7430])).
% 11.95/6.94 fof(f7722,plain,(
% 11.95/6.94 ![X0,X1]: (implies(X0,implies(implies(X0,implies(X1,X0)),X1))=implies(implies(X1,X0),implies(X0,X1)))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f7431,f4231])).
% 11.95/6.94 fof(f7820,plain,(
% 11.95/6.94 ![X0,X1]: (implies(X0,implies(truth,X1))=implies(implies(X1,X0),implies(X0,X1)))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f789,f7722])).
% 11.95/6.94 fof(f7821,plain,(
% 11.95/6.94 ![X0,X1]: (implies(X0,X1)=implies(implies(X1,X0),implies(X0,X1)))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f325,f7820])).
% 11.95/6.94 fof(f7822,plain,(
% 11.95/6.94 ![X0,X1]: (implies(X0,X1)=implies(X0,implies(implies(X1,X0),X1)))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f2552,f7821])).
% 11.95/6.94 fof(f8231,plain,(
% 11.95/6.94 ~implies(b,implies(implies(b,a),a))=truth),
% 11.95/6.94 inference(backward_demodulation,[status(thm)],[f7822,f3382])).
% 11.95/6.94 fof(f8304,plain,(
% 11.95/6.94 ~implies(a,implies(implies(a,b),a))=truth),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f4231,f8231])).
% 11.95/6.94 fof(f8305,plain,(
% 11.95/6.94 ~truth=truth),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f789,f8304])).
% 11.95/6.94 fof(f8306,plain,(
% 11.95/6.94 $false),
% 11.95/6.94 inference(trivial_equality_resolution,[status(thm)],[f8305])).
% 11.95/6.94 % SZS output end CNFRefutation for theBenchmark.p
% 11.95/6.96 % Elapsed time: 1.563769 seconds
% 11.95/6.96 % CPU time: 12.318420 seconds
% 11.95/6.96 % Total memory used: 128.524 MB
% 11.95/6.96 % Net memory used: 124.660 MB
%------------------------------------------------------------------------------