%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL146-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:26 PM UTC 2026
% Result : Unsatisfiable 5.08s 1.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL146-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n026.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 00:10:06 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 5.08/1.37 % Refutation found
% 5.08/1.37 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.08/1.37 % SZS output start CNFRefutation for theBenchmark
% 5.08/1.37 fof(f1,axiom,(
% 5.08/1.37 (![X]: (implies(truth,X) = X ))),
% 5.08/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.08/1.37 fof(f2,axiom,(
% 5.08/1.37 (![X,Y,Z]: (implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))) = truth ))),
% 5.08/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.08/1.37 fof(f3,axiom,(
% 5.08/1.37 (![X,Y]: (implies(implies(X,Y),Y) = implies(implies(Y,X),X) ))),
% 5.08/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.08/1.37 fof(f4,axiom,(
% 5.08/1.37 (![X,Y]: (implies(implies(not(X),not(Y)),implies(Y,X)) = truth ))),
% 5.08/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.08/1.37 fof(f5,axiom,(
% 5.08/1.37 (![X,Y]: (big_V(X,Y) = implies(implies(X,Y),Y) ))),
% 5.08/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.08/1.37 fof(f6,axiom,(
% 5.08/1.37 (![X,Y]: (big_hat(X,Y) = not(big_V(not(X),not(Y))) ))),
% 5.08/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.08/1.37 fof(f9,negated_conjecture,(
% 5.08/1.37 not(big_hat(x,y)) != big_V(not(x),not(y)) ),
% 5.08/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.08/1.37 fof(f10,plain,(
% 5.08/1.37 ![X0]: (implies(truth,X0)=X0)),
% 5.08/1.37 inference(cnf_transformation,[status(thm)],[f1])).
% 5.08/1.37 fof(f11,plain,(
% 5.08/1.37 ![X0,X1,X2]: (implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))=truth)),
% 5.08/1.37 inference(cnf_transformation,[status(thm)],[f2])).
% 5.08/1.37 fof(f12,plain,(
% 5.08/1.37 ![X0,X1]: (implies(implies(X0,X1),X1)=implies(implies(X1,X0),X0))),
% 5.08/1.37 inference(cnf_transformation,[status(thm)],[f3])).
% 5.08/1.37 fof(f13,plain,(
% 5.08/1.37 ![X0,X1]: (implies(implies(not(X0),not(X1)),implies(X1,X0))=truth)),
% 5.08/1.37 inference(cnf_transformation,[status(thm)],[f4])).
% 5.08/1.37 fof(f14,plain,(
% 5.08/1.37 ![X0,X1]: (big_V(X0,X1)=implies(implies(X0,X1),X1))),
% 5.08/1.37 inference(cnf_transformation,[status(thm)],[f5])).
% 5.08/1.37 fof(f15,plain,(
% 5.08/1.37 ![X0,X1]: (big_hat(X0,X1)=not(big_V(not(X0),not(X1))))),
% 5.08/1.37 inference(cnf_transformation,[status(thm)],[f6])).
% 5.08/1.37 fof(f18,plain,(
% 5.08/1.37 ~not(big_hat(x,y))=big_V(not(x),not(y))),
% 5.08/1.37 inference(cnf_transformation,[status(thm)],[f9])).
% 5.08/1.37 fof(f19,plain,(
% 5.08/1.37 ![X0,X1]: (implies(implies(X0,X1),X1)=big_V(X1,X0))),
% 5.08/1.37 inference(backward_demodulation,[status(thm)],[f14,f12])).
% 5.08/1.37 fof(f21,plain,(
% 5.08/1.37 ![X0,X1]: (implies(X0,implies(implies(X0,X1),implies(truth,X1)))=truth)),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f10,f11])).
% 5.08/1.37 fof(f28,plain,(
% 5.08/1.37 ![X0,X1]: (implies(X0,implies(implies(X0,X1),X1))=truth)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f10,f21])).
% 5.08/1.37 fof(f29,plain,(
% 5.08/1.37 ![X0,X1]: (implies(X0,big_V(X1,X0))=truth)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f19,f28])).
% 5.08/1.37 fof(f34,plain,(
% 5.08/1.37 ![X0]: (big_V(X0,truth)=truth)),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f10,f29])).
% 5.08/1.37 fof(f43,plain,(
% 5.08/1.37 ![X0]: (implies(implies(not(X0),not(truth)),X0)=truth)),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f10,f13])).
% 5.08/1.37 fof(f47,plain,(
% 5.08/1.37 ![X0,X1,X2]: (implies(implies(X0,implies(not(X1),not(X2))),implies(truth,implies(X0,implies(X2,X1))))=truth)),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f13,f11])).
% 5.08/1.37 fof(f48,plain,(
% 5.08/1.37 ![X0,X1,X2]: (implies(truth,implies(implies(implies(X0,X1),X2),implies(implies(not(X1),not(X0)),X2)))=truth)),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f13,f11])).
% 5.08/1.37 fof(f49,plain,(
% 5.08/1.37 ![X0,X1,X2]: (implies(implies(X0,implies(not(X1),not(X2))),implies(X0,implies(X2,X1)))=truth)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f10,f47])).
% 5.08/1.37 fof(f50,plain,(
% 5.08/1.37 ![X0,X1,X2]: (implies(implies(implies(X0,X1),X2),implies(implies(not(X1),not(X0)),X2))=truth)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f10,f48])).
% 5.08/1.37 fof(f55,plain,(
% 5.08/1.37 ![X0]: (big_V(truth,X0)=implies(X0,X0))),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f10,f14])).
% 5.08/1.37 fof(f68,plain,(
% 5.08/1.37 ![X0]: (implies(X0,implies(X0,X0))=truth)),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f55,f29])).
% 5.08/1.37 fof(f71,plain,(
% 5.08/1.37 ![X0]: (big_V(X0,X0)=implies(big_V(truth,X0),X0))),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f55,f14])).
% 5.08/1.37 fof(f78,plain,(
% 5.08/1.37 ![X0,X1,X2]: (big_hat(big_V(not(X0),not(X1)),X2)=not(big_V(big_hat(X0,X1),not(X2))))),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f15,f15])).
% 5.08/1.37 fof(f92,plain,(
% 5.08/1.37 ![X0,X1]: (implies(truth,implies(implies(implies(X0,X0),X1),implies(X0,X1)))=truth)),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f68,f11])).
% 5.08/1.37 fof(f95,plain,(
% 5.08/1.37 ![X0,X1]: (implies(implies(implies(X0,X0),X1),implies(X0,X1))=truth)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f10,f92])).
% 5.08/1.37 fof(f130,plain,(
% 5.08/1.37 ![X0,X1]: (big_V(X0,X1)=big_V(X1,X0))),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f14,f19])).
% 5.08/1.37 fof(f131,plain,(
% 5.08/1.37 ![X0,X1]: (implies(truth,implies(X0,X1))=big_V(implies(X0,X1),implies(not(X1),not(X0))))),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f13,f19])).
% 5.08/1.37 fof(f135,plain,(
% 5.08/1.37 ![X0]: (implies(X0,X0)=big_V(X0,truth))),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f10,f19])).
% 5.08/1.37 fof(f148,plain,(
% 5.08/1.37 ![X0,X1]: (implies(X0,X1)=big_V(implies(X0,X1),implies(not(X1),not(X0))))),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f10,f131])).
% 5.08/1.37 fof(f153,plain,(
% 5.08/1.37 ![X0]: (big_V(truth,X0)=truth)),
% 5.08/1.37 inference(backward_demodulation,[status(thm)],[f161,f55])).
% 5.08/1.37 fof(f155,plain,(
% 5.08/1.37 ![X0,X1]: (implies(implies(truth,X0),implies(X1,X0))=truth)),
% 5.08/1.37 inference(backward_demodulation,[status(thm)],[f161,f95])).
% 5.08/1.37 fof(f161,plain,(
% 5.08/1.37 ![X0]: (implies(X0,X0)=truth)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f34,f135])).
% 5.08/1.37 fof(f183,plain,(
% 5.08/1.37 ![X0]: (big_V(X0,X0)=implies(truth,X0))),
% 5.08/1.37 inference(backward_demodulation,[status(thm)],[f153,f71])).
% 5.08/1.37 fof(f184,plain,(
% 5.08/1.37 ![X0,X1]: (implies(X0,implies(X1,X0))=truth)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f10,f155])).
% 5.08/1.37 fof(f197,plain,(
% 5.08/1.37 ![X0]: (big_V(X0,X0)=X0)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f10,f183])).
% 5.08/1.37 fof(f402,plain,(
% 5.08/1.37 ![X0]: (big_hat(X0,X0)=not(not(X0)))),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f197,f15])).
% 5.08/1.37 fof(f406,plain,(
% 5.08/1.37 big_V(not(truth),not(not(truth)))=truth),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f19,f43])).
% 5.08/1.37 fof(f594,plain,(
% 5.08/1.37 ![X0]: (implies(truth,implies(implies(not(not(truth)),not(not(X0))),X0))=truth)),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f43,f50])).
% 5.08/1.37 fof(f649,plain,(
% 5.08/1.37 ![X0]: (implies(implies(not(not(truth)),not(not(X0))),X0)=truth)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f10,f594])).
% 5.08/1.37 fof(f1747,plain,(
% 5.08/1.37 ![X0,X1]: (implies(truth,implies(not(X0),implies(X0,X1)))=truth)),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f184,f49])).
% 5.08/1.37 fof(f1782,plain,(
% 5.08/1.37 ![X0,X1]: (implies(not(X0),implies(X0,X1))=truth)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f10,f1747])).
% 5.08/1.37 fof(f2279,plain,(
% 5.08/1.37 ![X0]: (implies(not(truth),X0)=truth)),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f10,f1782])).
% 5.08/1.37 fof(f2682,plain,(
% 5.08/1.37 ![X0]: (big_V(not(truth),X0)=implies(truth,X0))),
% 5.08/1.37 inference(paramodulation,[status(thm)],[f2279,f14])).
% 5.08/1.37 fof(f2739,plain,(
% 5.08/1.37 not(not(truth))=truth),
% 5.08/1.37 inference(backward_demodulation,[status(thm)],[f2744,f406])).
% 5.08/1.37 fof(f2744,plain,(
% 5.08/1.37 ![X0]: (big_V(not(truth),X0)=X0)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f10,f2682])).
% 5.08/1.37 fof(f2750,plain,(
% 5.08/1.37 ![X0]: (implies(implies(truth,not(not(X0))),X0)=truth)),
% 5.08/1.37 inference(backward_demodulation,[status(thm)],[f2739,f649])).
% 5.08/1.37 fof(f2752,plain,(
% 5.08/1.37 ![X0]: (implies(not(not(X0)),X0)=truth)),
% 5.08/1.37 inference(forward_demodulation,[status(thm)],[f10,f2750])).
% 5.08/1.37 fof(f3827,plain,(
% 5.08/1.37 ![X0]: (implies(X0,not(not(X0)))=big_V(implies(X0,not(not(X0))),truth))),
% 5.08/1.38 inference(paramodulation,[status(thm)],[f2752,f148])).
% 5.08/1.38 fof(f3872,plain,(
% 5.08/1.38 ![X0]: (implies(truth,X0)=big_V(X0,not(not(X0))))),
% 5.08/1.38 inference(paramodulation,[status(thm)],[f2752,f19])).
% 5.08/1.38 fof(f3882,plain,(
% 5.08/1.38 ![X0]: (implies(X0,not(not(X0)))=truth)),
% 5.08/1.38 inference(forward_demodulation,[status(thm)],[f34,f3827])).
% 5.08/1.38 fof(f3941,plain,(
% 5.08/1.38 ![X0]: (X0=big_V(X0,not(not(X0))))),
% 5.08/1.38 inference(forward_demodulation,[status(thm)],[f10,f3872])).
% 5.08/1.38 fof(f5001,plain,(
% 5.08/1.38 ![X0]: (implies(truth,not(not(X0)))=big_V(not(not(X0)),X0))),
% 5.08/1.38 inference(paramodulation,[status(thm)],[f3882,f19])).
% 5.08/1.38 fof(f5104,plain,(
% 5.08/1.38 ![X0]: (not(not(X0))=big_V(not(not(X0)),X0))),
% 5.08/1.38 inference(forward_demodulation,[status(thm)],[f10,f5001])).
% 5.08/1.38 fof(f5105,plain,(
% 5.08/1.38 ![X0]: (not(not(X0))=big_V(X0,not(not(X0))))),
% 5.08/1.38 inference(forward_demodulation,[status(thm)],[f130,f5104])).
% 5.08/1.38 fof(f5112,plain,(
% 5.08/1.38 ![X0]: (big_hat(X0,X0)=X0)),
% 5.08/1.38 inference(backward_demodulation,[status(thm)],[f5132,f402])).
% 5.08/1.38 fof(f5132,plain,(
% 5.08/1.38 ![X0]: (not(not(X0))=X0)),
% 5.08/1.40 inference(forward_demodulation,[status(thm)],[f3941,f5105])).
% 5.08/1.40 fof(f5542,plain,(
% 5.08/1.40 ![X0,X1]: (not(big_V(big_hat(X0,X1),not(big_V(not(X0),not(X1)))))=big_V(not(X0),not(X1)))),
% 5.08/1.40 inference(paramodulation,[status(thm)],[f78,f5112])).
% 5.08/1.40 fof(f5549,plain,(
% 5.08/1.40 ![X0,X1]: (not(big_V(big_hat(X0,X1),big_hat(X0,X1)))=big_V(not(X0),not(X1)))),
% 5.08/1.40 inference(forward_demodulation,[status(thm)],[f15,f5542])).
% 5.08/1.40 fof(f5550,plain,(
% 5.08/1.40 ~not(big_hat(x,y))=not(big_hat(x,y))),
% 5.08/1.40 inference(backward_demodulation,[status(thm)],[f5617,f18])).
% 5.08/1.40 fof(f5617,plain,(
% 5.08/1.40 ![X0,X1]: (not(big_hat(X0,X1))=big_V(not(X0),not(X1)))),
% 5.08/1.40 inference(forward_demodulation,[status(thm)],[f197,f5549])).
% 5.08/1.40 fof(f5628,plain,(
% 5.08/1.40 $false),
% 5.08/1.40 inference(trivial_equality_resolution,[status(thm)],[f5550])).
% 5.08/1.40 % SZS output end CNFRefutation for theBenchmark.p
% 5.08/1.40 % Elapsed time: 0.949293 seconds
% 5.08/1.40 % CPU time: 7.181998 seconds
% 5.08/1.40 % Total memory used: 137.712 MB
% 5.08/1.40 % Net memory used: 135.337 MB
%------------------------------------------------------------------------------