%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL160-1 : 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 : n017.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:28 PM UTC 2026
% Result : Unsatisfiable 0.16s 1.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL160-1 : 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.11/0.37 % Computer : n017.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 00:02:41 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 0.16/1.12 % Refutation found
% 0.16/1.12 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.16/1.12 % SZS output start CNFRefutation for theBenchmark
% 0.16/1.12 fof(f1,axiom,(
% 0.16/1.12 (![X]: (implies(truth,X) = X ))),
% 0.16/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/1.12 fof(f2,axiom,(
% 0.16/1.12 (![X,Y,Z]: (implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))) = truth ))),
% 0.16/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/1.12 fof(f3,axiom,(
% 0.16/1.12 (![X,Y]: (implies(implies(X,Y),Y) = implies(implies(Y,X),X) ))),
% 0.16/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/1.12 fof(f4,axiom,(
% 0.16/1.12 (![X,Y]: (implies(implies(not(X),not(Y)),implies(Y,X)) = truth ))),
% 0.16/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/1.12 fof(f5,axiom,(
% 0.16/1.12 (![X,Y]: (or(X,Y) = implies(not(X),Y) ))),
% 0.16/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/1.12 fof(f7,axiom,(
% 0.16/1.12 (![X,Y]: (or(X,Y) = or(Y,X) ))),
% 0.16/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/1.12 fof(f8,axiom,(
% 0.16/1.12 (![X,Y]: (and(X,Y) = not(or(not(X),not(Y))) ))),
% 0.16/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/1.12 fof(f11,axiom,(
% 0.16/1.12 (![X,Y]: (xor(X,Y) = or(and(X,not(Y)),and(not(X),Y)) ))),
% 0.16/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/1.12 fof(f13,axiom,(
% 0.16/1.12 (![X,Y]: (and_star(X,Y) = not(or(not(X),not(Y))) ))),
% 0.16/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/1.12 fof(f16,axiom,(
% 0.16/1.12 not(truth) = falsehood ),
% 0.16/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/1.12 fof(f17,negated_conjecture,(
% 0.16/1.12 and_star(xor(and_star(xor(truth,x),y),truth),y) != and_star(xor(and_star(xor(truth,y),x),truth),x) ),
% 0.16/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/1.12 fof(f18,plain,(
% 0.16/1.12 ![X0]: (implies(truth,X0)=X0)),
% 0.16/1.12 inference(cnf_transformation,[status(thm)],[f1])).
% 0.16/1.12 fof(f19,plain,(
% 0.16/1.12 ![X0,X1,X2]: (implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))=truth)),
% 0.16/1.12 inference(cnf_transformation,[status(thm)],[f2])).
% 0.16/1.12 fof(f20,plain,(
% 0.16/1.12 ![X0,X1]: (implies(implies(X0,X1),X1)=implies(implies(X1,X0),X0))),
% 0.16/1.12 inference(cnf_transformation,[status(thm)],[f3])).
% 0.16/1.12 fof(f21,plain,(
% 0.16/1.12 ![X0,X1]: (implies(implies(not(X0),not(X1)),implies(X1,X0))=truth)),
% 0.16/1.12 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/1.12 fof(f22,plain,(
% 0.16/1.12 ![X0,X1]: (or(X0,X1)=implies(not(X0),X1))),
% 0.16/1.12 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/1.12 fof(f24,plain,(
% 0.16/1.12 ![X0,X1]: (or(X0,X1)=or(X1,X0))),
% 0.16/1.12 inference(cnf_transformation,[status(thm)],[f7])).
% 0.16/1.12 fof(f25,plain,(
% 0.16/1.12 ![X0,X1]: (and(X0,X1)=not(or(not(X0),not(X1))))),
% 0.16/1.12 inference(cnf_transformation,[status(thm)],[f8])).
% 0.16/1.12 fof(f28,plain,(
% 0.16/1.12 ![X0,X1]: (xor(X0,X1)=or(and(X0,not(X1)),and(not(X0),X1)))),
% 0.16/1.12 inference(cnf_transformation,[status(thm)],[f11])).
% 0.16/1.12 fof(f30,plain,(
% 0.16/1.12 ![X0,X1]: (and_star(X0,X1)=not(or(not(X0),not(X1))))),
% 0.16/1.12 inference(cnf_transformation,[status(thm)],[f13])).
% 0.16/1.12 fof(f33,plain,(
% 0.16/1.12 not(truth)=falsehood),
% 0.16/1.12 inference(cnf_transformation,[status(thm)],[f16])).
% 0.16/1.12 fof(f34,plain,(
% 0.16/1.12 ~and_star(xor(and_star(xor(truth,x),y),truth),y)=and_star(xor(and_star(xor(truth,y),x),truth),x)),
% 0.16/1.12 inference(cnf_transformation,[status(thm)],[f17])).
% 0.16/1.12 fof(f61,plain,(
% 0.16/1.12 ![X0,X1]: (implies(X0,implies(implies(X0,X1),implies(truth,X1)))=truth)),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f18,f19])).
% 0.16/1.12 fof(f68,plain,(
% 0.16/1.12 ![X0,X1]: (implies(X0,implies(implies(X0,X1),X1))=truth)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f18,f61])).
% 0.16/1.12 fof(f71,plain,(
% 0.16/1.12 ![X0]: (or(truth,X0)=implies(falsehood,X0))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f33,f22])).
% 0.16/1.12 fof(f77,plain,(
% 0.16/1.12 ![X0]: (or(X0,truth)=implies(falsehood,X0))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f24,f71])).
% 0.16/1.12 fof(f89,plain,(
% 0.16/1.12 ![X0,X1]: (implies(or(X0,X1),X1)=implies(implies(X1,not(X0)),not(X0)))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f22,f20])).
% 0.16/1.12 fof(f106,plain,(
% 0.16/1.12 ![X0]: (implies(implies(truth,X0),X0)=truth)),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f18,f68])).
% 0.16/1.12 fof(f124,plain,(
% 0.16/1.12 ![X0]: (implies(X0,X0)=truth)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f18,f106])).
% 0.16/1.12 fof(f135,plain,(
% 0.16/1.12 ![X0]: (or(X0,not(X0))=truth)),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f22,f124])).
% 0.16/1.12 fof(f154,plain,(
% 0.16/1.12 ![X0,X1]: (implies(or(X0,not(X1)),implies(X1,X0))=truth)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f22,f21])).
% 0.16/1.12 fof(f159,plain,(
% 0.16/1.12 ![X0]: (implies(or(X0,falsehood),implies(truth,X0))=truth)),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f33,f154])).
% 0.16/1.12 fof(f173,plain,(
% 0.16/1.12 ![X0]: (implies(or(X0,falsehood),X0)=truth)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f18,f159])).
% 0.16/1.12 fof(f180,plain,(
% 0.16/1.12 ![X0]: (implies(or(falsehood,X0),X0)=truth)),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f24,f173])).
% 0.16/1.12 fof(f192,plain,(
% 0.16/1.12 implies(truth,not(falsehood))=truth),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f135,f180])).
% 0.16/1.12 fof(f202,plain,(
% 0.16/1.12 not(falsehood)=truth),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f18,f192])).
% 0.16/1.12 fof(f209,plain,(
% 0.16/1.12 ![X0]: (or(falsehood,X0)=implies(truth,X0))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f202,f22])).
% 0.16/1.12 fof(f212,plain,(
% 0.16/1.12 ![X0]: (or(falsehood,X0)=X0)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f18,f209])).
% 0.16/1.12 fof(f216,plain,(
% 0.16/1.12 ![X0]: (or(X0,falsehood)=X0)),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f24,f212])).
% 0.16/1.12 fof(f219,plain,(
% 0.16/1.12 ![X0]: (implies(not(X0),implies(X0,falsehood))=truth)),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f212,f154])).
% 0.16/1.12 fof(f224,plain,(
% 0.16/1.12 ![X0]: (or(X0,implies(X0,falsehood))=truth)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f22,f219])).
% 0.16/1.12 fof(f264,plain,(
% 0.16/1.12 ![X0]: (or(not(X0),or(X0,falsehood))=truth)),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f22,f224])).
% 0.16/1.12 fof(f274,plain,(
% 0.16/1.12 ![X0]: (or(not(X0),X0)=truth)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f216,f264])).
% 0.16/1.12 fof(f285,plain,(
% 0.16/1.12 ![X0]: (implies(truth,implies(X0,not(not(X0))))=truth)),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f274,f154])).
% 0.16/1.12 fof(f292,plain,(
% 0.16/1.12 ![X0]: (implies(X0,not(not(X0)))=truth)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f18,f285])).
% 0.16/1.12 fof(f355,plain,(
% 0.16/1.12 ![X0]: (implies(implies(not(not(X0)),X0),X0)=implies(truth,not(not(X0))))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f292,f20])).
% 0.16/1.12 fof(f366,plain,(
% 0.16/1.12 ![X0]: (implies(or(not(X0),X0),X0)=implies(truth,not(not(X0))))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f22,f355])).
% 0.16/1.12 fof(f367,plain,(
% 0.16/1.12 ![X0]: (implies(truth,X0)=implies(truth,not(not(X0))))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f274,f366])).
% 0.16/1.12 fof(f368,plain,(
% 0.16/1.12 ![X0]: (X0=implies(truth,not(not(X0))))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f18,f367])).
% 0.16/1.12 fof(f369,plain,(
% 0.16/1.12 ![X0]: (X0=not(not(X0)))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f18,f368])).
% 0.16/1.12 fof(f389,plain,(
% 0.16/1.12 ![X0,X1]: (or(not(X0),X1)=implies(X0,X1))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f369,f22])).
% 0.16/1.12 fof(f433,plain,(
% 0.16/1.12 ![X0,X1]: (and(X0,X1)=and_star(X0,X1))),
% 0.16/1.12 inference(backward_demodulation,[status(thm)],[f30,f25])).
% 0.16/1.12 fof(f445,plain,(
% 0.16/1.12 ![X0]: (and_star(X0,truth)=not(or(not(X0),falsehood)))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f33,f30])).
% 0.16/1.12 fof(f461,plain,(
% 0.16/1.12 ![X0]: (and_star(X0,truth)=not(not(X0)))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f216,f445])).
% 0.16/1.12 fof(f462,plain,(
% 0.16/1.12 ![X0]: (and_star(X0,truth)=X0)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f369,f461])).
% 0.16/1.12 fof(f504,plain,(
% 0.16/1.12 ![X0,X1]: (xor(X0,X1)=or(and(X0,not(X1)),and_star(not(X0),X1)))),
% 0.16/1.12 inference(backward_demodulation,[status(thm)],[f433,f28])).
% 0.16/1.12 fof(f512,plain,(
% 0.16/1.12 ![X0,X1]: (xor(X0,X1)=or(and_star(X0,not(X1)),and_star(not(X0),X1)))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f433,f504])).
% 0.16/1.12 fof(f583,plain,(
% 0.16/1.12 ![X0,X1]: (and_star(X0,X1)=not(implies(X0,not(X1))))),
% 0.16/1.12 inference(backward_demodulation,[status(thm)],[f389,f30])).
% 0.16/1.12 fof(f586,plain,(
% 0.16/1.12 ![X0]: (not(X0)=implies(X0,falsehood))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f216,f389])).
% 0.16/1.12 fof(f589,plain,(
% 0.16/1.12 ![X0,X1]: (or(X0,not(X1))=implies(X1,X0))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f24,f389])).
% 0.16/1.12 fof(f612,plain,(
% 0.16/1.12 ![X0]: (not(implies(X0,falsehood))=implies(implies(falsehood,X0),X0))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f20,f586])).
% 0.16/1.12 fof(f630,plain,(
% 0.16/1.12 ![X0]: (not(not(X0))=implies(implies(falsehood,X0),X0))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f586,f612])).
% 0.16/1.12 fof(f631,plain,(
% 0.16/1.12 ![X0]: (X0=implies(implies(falsehood,X0),X0))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f369,f630])).
% 0.16/1.12 fof(f660,plain,(
% 0.16/1.12 ![X0,X1]: (and_star(X0,not(X1))=not(implies(X0,X1)))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f369,f583])).
% 0.16/1.12 fof(f668,plain,(
% 0.16/1.12 ![X0,X1]: (implies(X0,not(X1))=not(and_star(X0,X1)))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f583,f369])).
% 0.16/1.12 fof(f686,plain,(
% 0.16/1.12 ![X0]: (implies(falsehood,X0)=truth)),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f631,f68])).
% 0.16/1.12 fof(f712,plain,(
% 0.16/1.12 ![X0]: (or(X0,truth)=truth)),
% 0.16/1.12 inference(backward_demodulation,[status(thm)],[f686,f77])).
% 0.16/1.12 fof(f717,plain,(
% 0.16/1.12 ![X0]: (and_star(falsehood,X0)=not(truth))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f686,f583])).
% 0.16/1.12 fof(f728,plain,(
% 0.16/1.12 ![X0]: (and_star(falsehood,X0)=falsehood)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f33,f717])).
% 0.16/1.12 fof(f743,plain,(
% 0.16/1.12 ![X0]: (implies(X0,truth)=truth)),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f389,f712])).
% 0.16/1.12 fof(f1349,plain,(
% 0.16/1.12 ![X0,X1]: (or(X0,X1)=implies(not(X1),X0))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f369,f589])).
% 0.16/1.12 fof(f1907,plain,(
% 0.16/1.12 ![X0,X1]: (and_star(or(X0,not(X1)),X1)=not(implies(implies(not(X1),not(X0)),not(X0))))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f89,f583])).
% 0.16/1.12 fof(f2004,plain,(
% 0.16/1.12 ![X0,X1]: (and_star(implies(X0,X1),X0)=not(implies(implies(not(X0),not(X1)),not(X1))))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f589,f1907])).
% 0.16/1.12 fof(f2005,plain,(
% 0.16/1.12 ![X0,X1]: (and_star(implies(X0,X1),X0)=and_star(implies(not(X0),not(X1)),X1))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f583,f2004])).
% 0.16/1.12 fof(f2006,plain,(
% 0.16/1.12 ![X0,X1]: (and_star(implies(X0,X1),X0)=and_star(or(not(X1),X0),X1))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f1349,f2005])).
% 0.16/1.12 fof(f2007,plain,(
% 0.16/1.12 ![X0,X1]: (and_star(implies(X0,X1),X0)=and_star(implies(X1,X0),X1))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f389,f2006])).
% 0.16/1.12 fof(f2105,plain,(
% 0.16/1.12 ![X0,X1]: (xor(X0,X1)=or(not(implies(X0,X1)),and_star(not(X0),X1)))),
% 0.16/1.12 inference(backward_demodulation,[status(thm)],[f660,f512])).
% 0.16/1.12 fof(f2124,plain,(
% 0.16/1.12 ![X0,X1]: (xor(X0,X1)=implies(implies(X0,X1),and_star(not(X0),X1)))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f389,f2105])).
% 0.16/1.12 fof(f2192,plain,(
% 0.16/1.12 ![X0]: (xor(truth,X0)=implies(X0,and_star(not(truth),X0)))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f18,f2124])).
% 0.16/1.12 fof(f2195,plain,(
% 0.16/1.12 ![X0]: (xor(X0,truth)=implies(truth,and_star(not(X0),truth)))),
% 0.16/1.12 inference(paramodulation,[status(thm)],[f743,f2124])).
% 0.16/1.12 fof(f2248,plain,(
% 0.16/1.12 ![X0]: (xor(truth,X0)=implies(X0,and_star(falsehood,X0)))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f33,f2192])).
% 0.16/1.12 fof(f2249,plain,(
% 0.16/1.12 ![X0]: (xor(truth,X0)=implies(X0,falsehood))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f728,f2248])).
% 0.16/1.12 fof(f2250,plain,(
% 0.16/1.12 ![X0]: (xor(truth,X0)=not(X0))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f586,f2249])).
% 0.16/1.12 fof(f2253,plain,(
% 0.16/1.12 ![X0]: (xor(X0,truth)=and_star(not(X0),truth))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f18,f2195])).
% 0.16/1.12 fof(f2254,plain,(
% 0.16/1.12 ![X0]: (xor(X0,truth)=not(X0))),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f462,f2253])).
% 0.16/1.12 fof(f2281,plain,(
% 0.16/1.12 ~and_star(xor(and_star(xor(truth,x),y),truth),y)=and_star(xor(and_star(not(y),x),truth),x)),
% 0.16/1.12 inference(backward_demodulation,[status(thm)],[f2250,f34])).
% 0.16/1.12 fof(f2290,plain,(
% 0.16/1.12 ~and_star(xor(and_star(not(x),y),truth),y)=and_star(xor(and_star(not(y),x),truth),x)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f2250,f2281])).
% 0.16/1.12 fof(f2301,plain,(
% 0.16/1.12 ~and_star(not(and_star(not(x),y)),y)=and_star(xor(and_star(not(y),x),truth),x)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f2254,f2290])).
% 0.16/1.12 fof(f2302,plain,(
% 0.16/1.12 ~and_star(implies(not(x),not(y)),y)=and_star(xor(and_star(not(y),x),truth),x)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f668,f2301])).
% 0.16/1.12 fof(f2303,plain,(
% 0.16/1.12 ~and_star(or(not(y),x),y)=and_star(xor(and_star(not(y),x),truth),x)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f1349,f2302])).
% 0.16/1.12 fof(f2304,plain,(
% 0.16/1.12 ~and_star(implies(y,x),y)=and_star(xor(and_star(not(y),x),truth),x)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f389,f2303])).
% 0.16/1.12 fof(f2305,plain,(
% 0.16/1.12 ~and_star(implies(y,x),y)=and_star(not(and_star(not(y),x)),x)),
% 0.16/1.12 inference(forward_demodulation,[status(thm)],[f2254,f2304])).
% 0.16/1.15 fof(f2306,plain,(
% 0.16/1.15 ~and_star(implies(y,x),y)=and_star(implies(not(y),not(x)),x)),
% 0.16/1.15 inference(forward_demodulation,[status(thm)],[f668,f2305])).
% 0.16/1.15 fof(f2307,plain,(
% 0.16/1.15 ~and_star(implies(y,x),y)=and_star(or(not(x),y),x)),
% 0.16/1.15 inference(forward_demodulation,[status(thm)],[f1349,f2306])).
% 0.16/1.15 fof(f2308,plain,(
% 0.16/1.15 ~and_star(implies(y,x),y)=and_star(implies(x,y),x)),
% 0.16/1.15 inference(forward_demodulation,[status(thm)],[f389,f2307])).
% 0.16/1.15 fof(f14280,plain,(
% 0.16/1.15 $false),
% 0.16/1.15 inference(backward_subsumption_resolution,[status(thm)],[f2308,f2007])).
% 0.16/1.15 % SZS output end CNFRefutation for theBenchmark.p
% 11.99/2.38 % Elapsed time: 1.769627 seconds
% 11.99/2.38 % CPU time: 3.006591 seconds
% 11.99/2.38 % Total memory used: 40.864 MB
% 11.99/2.38 % Net memory used: 39.917 MB
%------------------------------------------------------------------------------