%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT394-1 : TPTP v9.3.1. Released v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:03:58 PM UTC 2026
% Result : Unsatisfiable 21.13s 13.28s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT394-1 : TPTP v9.3.1. Released v5.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/10.42 % Computer : n015.cluster.edu
% 0.13/10.42 % Model : x86_64 x86_64
% 0.13/10.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.42 % Memory : 8046.5625MB
% 0.13/10.42 % OS : Linux 6.8.0-71-generic
% 0.13/10.42 % CPULimit : 300
% 0.13/10.42 % WCLimit : 300
% 0.13/10.42 % DateTime : Mon Sep 21 00:01:45 UTC 2026
% 0.13/10.42 % CPUTime :
% 0.13/10.43 % Drodi V4.1.1
% 21.13/13.28 % Refutation found
% 21.13/13.28 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 21.13/13.28 % SZS output start CNFRefutation for theBenchmark
% 21.13/13.28 fof(f1,axiom,(
% 21.13/13.28 (![A,B,C,D]: (f(f(f(f(A,B),f(B,C)),D),f(B,f(f(B,f(f(A,A),A)),C))) = B ))),
% 21.13/13.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.13/13.28 fof(f2,axiom,(
% 21.13/13.28 (![A,B]: (or(A,B) = f(f(A,A),f(B,B)) ))),
% 21.13/13.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.13/13.28 fof(f3,axiom,(
% 21.13/13.28 (![A,B]: (and(A,B) = f(f(A,B),f(A,B)) ))),
% 21.13/13.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.13/13.28 fof(f4,axiom,(
% 21.13/13.28 (![A]: (neg(A) = f(A,A) ))),
% 21.13/13.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.13/13.28 fof(f5,negated_conjecture,(
% 21.13/13.28 f(x0,f(x0,x0)) != f(x1,f(x1,x1)) ),
% 21.13/13.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.13/13.28 fof(f6,plain,(
% 21.13/13.28 ![X0,X1,X2,X3]: (f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(f(X0,X0),X0)),X2)))=X1)),
% 21.13/13.28 inference(cnf_transformation,[status(thm)],[f1])).
% 21.13/13.28 fof(f7,plain,(
% 21.13/13.28 ![X0,X1]: (or(X0,X1)=f(f(X0,X0),f(X1,X1)))),
% 21.13/13.28 inference(cnf_transformation,[status(thm)],[f2])).
% 21.13/13.28 fof(f8,plain,(
% 21.13/13.28 ![X0,X1]: (and(X0,X1)=f(f(X0,X1),f(X0,X1)))),
% 21.13/13.28 inference(cnf_transformation,[status(thm)],[f3])).
% 21.13/13.28 fof(f9,plain,(
% 21.13/13.28 ![X0]: (neg(X0)=f(X0,X0))),
% 21.13/13.28 inference(cnf_transformation,[status(thm)],[f4])).
% 21.13/13.28 fof(f10,plain,(
% 21.13/13.28 ~f(x0,f(x0,x0))=f(x1,f(x1,x1))),
% 21.13/13.28 inference(cnf_transformation,[status(thm)],[f5])).
% 21.13/13.28 fof(f16,plain,(
% 21.13/13.28 ![X0,X1]: (or(X0,X1)=f(neg(X0),f(X1,X1)))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f9,f7])).
% 21.13/13.28 fof(f17,plain,(
% 21.13/13.28 ![X0,X1]: (or(X0,X1)=f(neg(X0),neg(X1)))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f9,f16])).
% 21.13/13.28 fof(f18,plain,(
% 21.13/13.28 ![X0]: (or(X0,X0)=neg(neg(X0)))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f9,f17])).
% 21.13/13.28 fof(f22,plain,(
% 21.13/13.28 ![X0,X1]: (or(X0,neg(X1))=f(neg(X0),or(X1,X1)))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f18,f17])).
% 21.13/13.28 fof(f23,plain,(
% 21.13/13.28 ![X0,X1]: (or(neg(X0),X1)=f(or(X0,X0),neg(X1)))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f18,f17])).
% 21.13/13.28 fof(f24,plain,(
% 21.13/13.28 ![X0,X1]: (and(X0,X1)=neg(f(X0,X1)))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f9,f8])).
% 21.13/13.28 fof(f25,plain,(
% 21.13/13.28 ![X0,X1]: (and(neg(X0),neg(X1))=neg(or(X0,X1)))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f17,f24])).
% 21.13/13.28 fof(f27,plain,(
% 21.13/13.28 ![X0,X1,X2]: (or(X0,f(X1,X2))=f(neg(X0),and(X1,X2)))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f24,f17])).
% 21.13/13.28 fof(f35,plain,(
% 21.13/13.28 ![X0,X1,X2,X3]: (f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(neg(X0),X0)),X2)))=X1)),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f9,f6])).
% 21.13/13.28 fof(f36,plain,(
% 21.13/13.28 ![X0,X1,X2,X3]: (f(X0,f(f(X0,X1),f(f(f(X0,X1),f(neg(f(X2,X0)),f(X2,X0))),X3)))=f(X0,X1))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f35,f35])).
% 21.13/13.28 fof(f38,plain,(
% 21.13/13.28 ![X0,X1,X2,X3]: (f(f(X0,X1),f(X0,f(f(X0,f(neg(f(f(X2,X0),f(X0,X3))),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3))))=X0)),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f35,f35])).
% 21.13/13.28 fof(f45,plain,(
% 21.13/13.28 ![X0,X1,X2]: (f(f(f(f(X0,X1),neg(X1)),X2),f(X1,f(f(X1,f(neg(X0),X0)),X1)))=X1)),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f9,f35])).
% 21.13/13.28 fof(f47,plain,(
% 21.13/13.28 ![X0,X1,X2]: (f(f(f(f(X0,X1),f(X1,f(X1,f(neg(X0),X0)))),X2),f(X1,neg(f(X1,f(neg(X0),X0)))))=X1)),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f9,f35])).
% 21.13/13.28 fof(f54,plain,(
% 21.13/13.28 ![X0,X1,X2,X3]: (f(X0,f(f(X0,X1),f(f(f(X0,X1),f(and(X2,X0),f(X2,X0))),X3)))=f(X0,X1))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f24,f36])).
% 21.13/13.28 fof(f56,plain,(
% 21.13/13.28 ![X0,X1,X2,X3]: (f(f(X0,X1),f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3))))=X0)),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f24,f38])).
% 21.13/13.28 fof(f60,plain,(
% 21.13/13.28 ![X0,X1,X2]: (f(f(f(f(X0,X1),f(X1,f(X1,f(neg(X0),X0)))),X2),f(X1,and(X1,f(neg(X0),X0))))=X1)),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f24,f47])).
% 21.13/13.28 fof(f125,plain,(
% 21.13/13.28 ~f(x0,neg(x0))=f(x1,f(x1,x1))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f9,f10])).
% 21.13/13.28 fof(f126,plain,(
% 21.13/13.28 ~f(x0,neg(x0))=f(x1,neg(x1))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f9,f125])).
% 21.13/13.28 fof(f727,plain,(
% 21.13/13.28 ![X0,X1]: (f(X0,f(f(X0,X1),f(X0,X1)))=f(X0,X1))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f56,f54])).
% 21.13/13.28 fof(f833,plain,(
% 21.13/13.28 ![X0,X1]: (f(X0,neg(f(X0,X1)))=f(X0,X1))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f9,f727])).
% 21.13/13.28 fof(f834,plain,(
% 21.13/13.28 ![X0,X1]: (f(X0,and(X0,X1))=f(X0,X1))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f24,f833])).
% 21.13/13.28 fof(f845,plain,(
% 21.13/13.28 ![X0,X1]: (or(X0,f(neg(X0),X1))=f(neg(X0),X1))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f27,f834])).
% 21.13/13.28 fof(f5802,plain,(
% 21.13/13.28 ![X0,X1,X2]: (f(f(f(f(X0,X1),f(X1,f(X1,f(neg(X0),X0)))),X2),f(X1,f(neg(X0),X0)))=X1)),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f834,f60])).
% 21.13/13.28 fof(f5813,plain,(
% 21.13/13.28 ![X0,X1]: (f(f(X0,X1),f(X1,f(neg(X0),X0)))=X1)),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f56,f5802])).
% 21.13/13.28 fof(f6478,plain,(
% 21.13/13.28 ![X0]: (f(neg(X0),f(X0,f(neg(X0),X0)))=X0)),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f9,f5813])).
% 21.13/13.28 fof(f6581,plain,(
% 21.13/13.28 ![X0,X1]: (and(f(X0,X1),f(X1,f(neg(X0),X0)))=neg(X1))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f5813,f24])).
% 21.13/13.28 fof(f6879,plain,(
% 21.13/13.28 ![X0]: (or(X0,X0)=f(neg(X0),f(X0,f(neg(X0),X0))))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f6478,f845])).
% 21.13/13.28 fof(f6940,plain,(
% 21.13/13.28 ![X0]: (or(X0,X0)=X0)),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f6478,f6879])).
% 21.13/13.28 fof(f7034,plain,(
% 21.13/13.28 ![X0,X1]: (or(neg(X0),X1)=f(X0,neg(X1)))),
% 21.13/13.28 inference(backward_demodulation,[status(thm)],[f6940,f23])).
% 21.13/13.28 fof(f7035,plain,(
% 21.13/13.28 ![X0,X1]: (or(X0,neg(X1))=f(neg(X0),X1))),
% 21.13/13.28 inference(backward_demodulation,[status(thm)],[f6940,f22])).
% 21.13/13.28 fof(f7038,plain,(
% 21.13/13.28 ![X0]: (X0=neg(neg(X0)))),
% 21.13/13.28 inference(backward_demodulation,[status(thm)],[f6940,f18])).
% 21.13/13.28 fof(f7090,plain,(
% 21.13/13.28 ![X0,X1]: (f(X0,X1)=neg(and(X0,X1)))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f24,f7038])).
% 21.13/13.28 fof(f7560,plain,(
% 21.13/13.28 ![X0,X1,X2]: (or(and(X0,X1),X2)=f(f(X0,X1),neg(X2)))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f7090,f17])).
% 21.13/13.28 fof(f10199,plain,(
% 21.13/13.28 ![X0,X1,X2]: (f(f(or(and(X0,X1),X1),X2),f(X1,f(f(X1,f(neg(X0),X0)),X1)))=X1)),
% 21.13/13.28 inference(backward_demodulation,[status(thm)],[f7560,f45])).
% 21.13/13.28 fof(f12231,plain,(
% 21.13/13.28 ![X0,X1]: (f(f(X0,X1),neg(X1))=f(f(X0,X1),f(X1,f(neg(X0),X0))))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f6581,f834])).
% 21.13/13.28 fof(f12324,plain,(
% 21.13/13.28 ![X0,X1]: (or(and(X0,X1),X1)=f(f(X0,X1),f(X1,f(neg(X0),X0))))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f7560,f12231])).
% 21.13/13.28 fof(f12325,plain,(
% 21.13/13.28 ![X0,X1]: (or(and(X0,X1),X1)=X1)),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f5813,f12324])).
% 21.13/13.28 fof(f12615,plain,(
% 21.13/13.28 ![X0,X1,X2]: (f(f(X0,X1),f(X0,f(f(X0,f(neg(X2),X2)),X0)))=X0)),
% 21.13/13.28 inference(backward_demodulation,[status(thm)],[f12325,f10199])).
% 21.13/13.28 fof(f12616,plain,(
% 21.13/13.28 ![X0,X1]: (f(neg(and(X0,neg(X1))),X1)=neg(X1))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f7035,f12325])).
% 21.13/13.28 fof(f12632,plain,(
% 21.13/13.28 ![X0,X1]: (f(f(X0,neg(X1)),X1)=neg(X1))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f7090,f12616])).
% 21.13/13.28 fof(f13473,plain,(
% 21.13/13.28 ![X0,X1]: (X0=neg(f(X0,f(neg(X1),X1))))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f5802,f12632])).
% 21.13/13.28 fof(f13580,plain,(
% 21.13/13.28 ![X0,X1]: (X0=and(X0,f(neg(X1),X1)))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f24,f13473])).
% 21.13/13.28 fof(f13943,plain,(
% 21.13/13.28 ![X0,X1]: (X0=and(X0,or(neg(X1),X1)))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f17,f13580])).
% 21.13/13.28 fof(f13961,plain,(
% 21.13/13.28 ![X0,X1]: (f(X0,f(neg(X1),X1))=neg(X0))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f13580,f7090])).
% 21.13/13.28 fof(f13971,plain,(
% 21.13/13.28 ![X0,X1]: (X0=and(X0,f(X1,neg(X1))))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f7034,f13943])).
% 21.13/13.28 fof(f14050,plain,(
% 21.13/13.28 ![X0,X1]: (f(f(X0,X1),f(X0,f(neg(X0),X0)))=X0)),
% 21.13/13.28 inference(backward_demodulation,[status(thm)],[f13961,f12615])).
% 21.13/13.28 fof(f14116,plain,(
% 21.13/13.28 ![X0,X1]: (f(f(X0,X1),neg(X0))=X0)),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f13961,f14050])).
% 21.13/13.28 fof(f14117,plain,(
% 21.13/13.28 ![X0,X1]: (or(and(X0,X1),X0)=X0)),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f7560,f14116])).
% 21.13/13.28 fof(f14231,plain,(
% 21.13/13.28 ![X0,X1]: (or(neg(or(X0,X1)),neg(X0))=neg(X0))),
% 21.13/13.28 inference(paramodulation,[status(thm)],[f25,f14117])).
% 21.13/13.28 fof(f14251,plain,(
% 21.13/13.28 ![X0,X1]: (f(or(X0,X1),neg(neg(X0)))=neg(X0))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f7034,f14231])).
% 21.13/13.28 fof(f14252,plain,(
% 21.13/13.28 ![X0,X1]: (f(or(X0,X1),X0)=neg(X0))),
% 21.13/13.28 inference(forward_demodulation,[status(thm)],[f7038,f14251])).
% 21.13/13.28 fof(f14535,plain,(
% 21.13/13.28 ![X0,X1]: (and(or(X0,X1),X0)=neg(neg(X0)))),
% 21.13/13.34 inference(paramodulation,[status(thm)],[f14252,f24])).
% 21.13/13.34 fof(f14581,plain,(
% 21.13/13.34 ![X0,X1]: (and(or(X0,X1),X0)=X0)),
% 21.13/13.34 inference(forward_demodulation,[status(thm)],[f7038,f14535])).
% 21.13/13.34 fof(f14586,plain,(
% 21.13/13.34 ![X0,X1]: (and(X0,and(X1,X0))=and(X1,X0))),
% 21.13/13.34 inference(paramodulation,[status(thm)],[f12325,f14581])).
% 21.13/13.34 fof(f17514,plain,(
% 21.13/13.34 ![X0,X1]: (and(f(X0,neg(X0)),X1)=and(X1,f(X0,neg(X0))))),
% 21.13/13.34 inference(paramodulation,[status(thm)],[f13971,f14586])).
% 21.13/13.34 fof(f17547,plain,(
% 21.13/13.34 ![X0,X1]: (and(f(X0,neg(X0)),X1)=X1)),
% 21.13/13.34 inference(forward_demodulation,[status(thm)],[f13971,f17514])).
% 21.13/13.34 fof(f17630,plain,(
% 21.13/13.34 ![X0,X1]: (f(X0,neg(X0))=f(X1,neg(X1)))),
% 21.13/13.34 inference(paramodulation,[status(thm)],[f13971,f17547])).
% 21.13/13.34 fof(f32992,plain,(
% 21.13/13.34 $false),
% 21.13/13.34 inference(backward_subsumption_resolution,[status(thm)],[f126,f17630])).
% 21.13/13.34 % SZS output end CNFRefutation for theBenchmark.p
% 12.16/20.16 % Elapsed time: 9.732787 seconds
% 12.16/20.16 % CPU time: 76.387770 seconds
% 12.16/20.16 % Total memory used: 42.535 GB
% 12.16/20.16 % Net memory used: 42.531 GB
%------------------------------------------------------------------------------