%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL109-3 : 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 : n019.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:22 PM UTC 2026
% Result : Unsatisfiable 52.34s 7.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL109-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 00:05:21 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 52.34/7.23 % Refutation found
% 52.34/7.23 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 52.34/7.23 % SZS output start CNFRefutation for theBenchmark
% 52.34/7.23 fof(f1,axiom,(
% 52.34/7.23 (![X]: (implies(truth,X) = X ))),
% 52.34/7.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.34/7.23 fof(f2,axiom,(
% 52.34/7.23 (![X,Y,Z]: (implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))) = truth ))),
% 52.34/7.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.34/7.23 fof(f3,axiom,(
% 52.34/7.23 (![X,Y]: (implies(implies(X,Y),Y) = implies(implies(Y,X),X) ))),
% 52.34/7.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.34/7.23 fof(f5,axiom,(
% 52.34/7.23 (![X]: (implies(X,X) = truth ))),
% 52.34/7.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.34/7.23 fof(f6,axiom,(
% 52.34/7.23 (![X,Y]: (( implies(X,Y) != implies(Y,X)| X = Y ) ))),
% 52.34/7.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.34/7.23 fof(f8,axiom,(
% 52.34/7.23 (![X,Y]: (implies(X,implies(Y,X)) = truth ))),
% 52.34/7.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.34/7.23 fof(f9,axiom,(
% 52.34/7.23 (![X,Y,Z]: (( implies(X,Y) != implies(Y,Z)| implies(X,Z) = truth ) ))),
% 52.34/7.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.34/7.23 fof(f11,axiom,(
% 52.34/7.23 (![X,Y,Z]: (implies(X,implies(Y,Z)) = implies(Y,implies(X,Z)) ))),
% 52.34/7.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.34/7.23 fof(f13,axiom,(
% 52.34/7.23 (![X]: (not(not(X)) = X ))),
% 52.34/7.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.34/7.23 fof(f14,axiom,(
% 52.34/7.23 (![X,Y]: (implies(not(X),not(Y)) = implies(Y,X) ))),
% 52.34/7.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.34/7.23 fof(f15,negated_conjecture,(
% 52.34/7.23 implies(implies(implies(a,b),implies(b,a)),implies(b,a)) != truth ),
% 52.34/7.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 52.34/7.23 fof(f16,plain,(
% 52.34/7.23 ![X0]: (implies(truth,X0)=X0)),
% 52.34/7.23 inference(cnf_transformation,[status(thm)],[f1])).
% 52.34/7.23 fof(f17,plain,(
% 52.34/7.23 ![X0,X1,X2]: (implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))=truth)),
% 52.34/7.23 inference(cnf_transformation,[status(thm)],[f2])).
% 52.34/7.23 fof(f18,plain,(
% 52.34/7.23 ![X0,X1]: (implies(implies(X0,X1),X1)=implies(implies(X1,X0),X0))),
% 52.34/7.23 inference(cnf_transformation,[status(thm)],[f3])).
% 52.34/7.23 fof(f20,plain,(
% 52.34/7.23 ![X0]: (implies(X0,X0)=truth)),
% 52.34/7.23 inference(cnf_transformation,[status(thm)],[f5])).
% 52.34/7.23 fof(f21,plain,(
% 52.34/7.23 ![X0,X1]: (~implies(X0,X1)=implies(X1,X0)|X0=X1)),
% 52.34/7.23 inference(cnf_transformation,[status(thm)],[f6])).
% 52.34/7.23 fof(f23,plain,(
% 52.34/7.23 ![X0,X1]: (implies(X0,implies(X1,X0))=truth)),
% 52.34/7.23 inference(cnf_transformation,[status(thm)],[f8])).
% 52.34/7.23 fof(f24,plain,(
% 52.34/7.23 ![X,Z]: ((![Y]: ~implies(X,Y)=implies(Y,Z))|implies(X,Z)=truth)),
% 52.34/7.23 inference(miniscoping,[status(thm)],[f9])).
% 52.34/7.23 fof(f25,plain,(
% 52.34/7.23 ![X0,X1,X2]: (~implies(X0,X1)=implies(X1,X2)|implies(X0,X2)=truth)),
% 52.34/7.23 inference(cnf_transformation,[status(thm)],[f24])).
% 52.34/7.23 fof(f27,plain,(
% 52.34/7.23 ![X0,X1,X2]: (implies(X0,implies(X1,X2))=implies(X1,implies(X0,X2)))),
% 52.34/7.23 inference(cnf_transformation,[status(thm)],[f11])).
% 52.34/7.23 fof(f29,plain,(
% 52.34/7.23 ![X0]: (not(not(X0))=X0)),
% 52.34/7.23 inference(cnf_transformation,[status(thm)],[f13])).
% 52.34/7.23 fof(f30,plain,(
% 52.34/7.23 ![X0,X1]: (implies(not(X0),not(X1))=implies(X1,X0))),
% 52.34/7.23 inference(cnf_transformation,[status(thm)],[f14])).
% 52.34/7.23 fof(f31,plain,(
% 52.34/7.23 ~implies(implies(implies(a,b),implies(b,a)),implies(b,a))=truth),
% 52.34/7.23 inference(cnf_transformation,[status(thm)],[f15])).
% 52.34/7.23 fof(f52,plain,(
% 52.34/7.23 ![X0,X1,X2]: (implies(truth,implies(implies(implies(X0,X1),X2),implies(X1,X2)))=truth)),
% 52.34/7.23 inference(paramodulation,[status(thm)],[f23,f17])).
% 52.34/7.23 fof(f71,plain,(
% 52.34/7.23 ![X0,X1,X2]: (implies(implies(implies(X0,X1),X2),implies(X1,X2))=truth)),
% 52.34/7.23 inference(forward_demodulation,[status(thm)],[f16,f52])).
% 52.34/7.23 fof(f134,plain,(
% 52.34/7.23 ![X0,X1]: (~implies(X0,implies(X1,X0))=implies(implies(X0,X1),X1)|X0=implies(X1,X0))),
% 52.34/7.23 inference(paramodulation,[status(thm)],[f18,f21])).
% 52.34/7.23 fof(f161,plain,(
% 52.34/7.23 ![X0,X1]: (~truth=implies(implies(X0,X1),X1)|X0=implies(X1,X0))),
% 52.34/7.23 inference(forward_demodulation,[status(thm)],[f23,f134])).
% 52.34/7.23 fof(f168,plain,(
% 52.34/7.23 ![X0,X1,X2]: (~implies(implies(X0,X1),X1)=implies(X0,X2)|implies(implies(X1,X0),X2)=truth)),
% 52.34/7.23 inference(paramodulation,[status(thm)],[f18,f25])).
% 52.34/7.23 fof(f172,plain,(
% 52.34/7.23 ![X0,X1,X2]: (~truth=implies(implies(X0,X1),X2)|implies(X1,X2)=truth)),
% 52.34/7.23 inference(paramodulation,[status(thm)],[f23,f25])).
% 52.34/7.23 fof(f264,plain,(
% 54.23/7.27 ![X0,X1,X2]: (implies(implies(implies(X0,X1),X2),X2)=implies(implies(X0,implies(X2,X1)),implies(X0,X1)))),
% 54.23/7.27 inference(paramodulation,[status(thm)],[f27,f18])).
% 54.23/7.27 fof(f366,plain,(
% 54.23/7.27 ![X0,X1]: (~truth=implies(implies(X0,X1),X1)|X1=implies(X0,X1))),
% 54.23/7.27 inference(paramodulation,[status(thm)],[f18,f161])).
% 54.23/7.27 fof(f647,plain,(
% 54.23/7.27 ![X0,X1]: (implies(X0,not(X1))=implies(X1,not(X0)))),
% 54.23/7.27 inference(paramodulation,[status(thm)],[f29,f30])).
% 54.23/7.27 fof(f648,plain,(
% 54.23/7.27 ![X0,X1]: (implies(not(X0),X1)=implies(not(X1),X0))),
% 54.23/7.27 inference(paramodulation,[status(thm)],[f29,f30])).
% 54.23/7.27 fof(f1302,plain,(
% 54.23/7.27 ![X0,X1,X2]: (implies(implies(implies(X0,X1),X2),implies(not(X0),X2))=truth)),
% 54.23/7.27 inference(paramodulation,[status(thm)],[f30,f71])).
% 54.23/7.27 fof(f2330,plain,(
% 54.23/7.27 ![X0,X1,X2]: (~truth=implies(implies(X0,X1),X2)|implies(not(X0),X2)=truth)),
% 54.23/7.27 inference(paramodulation,[status(thm)],[f30,f172])).
% 54.23/7.27 fof(f4916,plain,(
% 54.23/7.27 ![X0,X1,X2]: (implies(implies(implies(X0,X1),X2),implies(not(X2),X0))=truth)),
% 54.23/7.27 inference(paramodulation,[status(thm)],[f648,f1302])).
% 54.23/7.27 fof(f5351,plain,(
% 54.23/7.27 ![X0]: (implies(implies(not(X0),X0),not(implies(X0,not(X0))))=truth)),
% 54.23/7.27 inference(resolution,[status(thm)],[f168,f647])).
% 54.23/7.27 fof(f26377,plain,(
% 54.23/7.27 ~implies(implies(a,implies(implies(b,a),b)),implies(a,b))=truth),
% 54.23/7.27 inference(paramodulation,[status(thm)],[f264,f31])).
% 54.23/7.27 fof(f28416,plain,(
% 54.23/7.27 ![X0]: (implies(not(not(X0)),not(implies(X0,not(X0))))=truth)),
% 54.23/7.27 inference(resolution,[status(thm)],[f5351,f2330])).
% 54.23/7.27 fof(f28611,plain,(
% 54.23/7.27 ![X0]: (implies(implies(X0,not(X0)),not(X0))=truth)),
% 54.23/7.27 inference(forward_demodulation,[status(thm)],[f30,f28416])).
% 54.23/7.27 fof(f28898,plain,(
% 54.23/7.27 ![X0]: (X0=implies(not(X0),X0))),
% 54.23/7.27 inference(resolution,[status(thm)],[f28611,f161])).
% 54.23/7.27 fof(f29503,plain,(
% 54.23/7.27 ![X0,X1]: (implies(implies(implies(X0,X1),X0),X0)=truth)),
% 54.23/7.27 inference(paramodulation,[status(thm)],[f28898,f4916])).
% 54.23/7.27 fof(f32765,plain,(
% 54.23/7.27 ![X0,X1]: (X0=implies(implies(X0,X1),X0))),
% 54.23/7.27 inference(resolution,[status(thm)],[f29503,f366])).
% 54.23/7.27 fof(f33528,plain,(
% 54.23/7.27 ~implies(implies(a,b),implies(a,b))=truth),
% 54.23/7.27 inference(backward_demodulation,[status(thm)],[f32765,f26377])).
% 54.23/7.27 fof(f33902,plain,(
% 54.23/7.27 ~truth=truth),
% 54.23/7.27 inference(forward_demodulation,[status(thm)],[f20,f33528])).
% 54.23/7.27 fof(f33903,plain,(
% 54.23/7.27 $false),
% 54.23/7.27 inference(trivial_equality_resolution,[status(thm)],[f33902])).
% 54.23/7.27 % SZS output end CNFRefutation for theBenchmark.p
% 54.23/7.31 % Elapsed time: 6.943427 seconds
% 54.23/7.31 % CPU time: 54.668569 seconds
% 54.23/7.31 % Total memory used: 405.108 MB
% 54.23/7.31 % Net memory used: 392.268 MB
%------------------------------------------------------------------------------