%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN598-10 : TPTP v9.3.1. Released v7.5.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 03:20:12 PM UTC 2026
% Result : Unsatisfiable 1.58s 0.98s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN598-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.51 % Computer : n017.cluster.edu
% 0.08/0.51 % Model : x86_64 x86_64
% 0.08/0.51 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.51 % Memory : 8046.5625MB
% 0.08/0.51 % OS : Linux 6.8.0-71-generic
% 0.08/0.51 % CPULimit : 300
% 0.08/0.51 % WCLimit : 300
% 0.08/0.51 % DateTime : Mon Sep 21 11:04:42 UTC 2026
% 0.08/0.51 % CPUTime :
% 0.08/0.52 % Drodi V4.1.1
% 1.58/0.98 % Refutation found
% 1.58/0.98 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.58/0.98 % SZS output start CNFRefutation for theBenchmark
% 1.58/0.98 fof(f1,axiom,(
% 1.58/0.98 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 1.58/0.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.58/0.98 fof(f3,negated_conjecture,(
% 1.58/0.98 p18(c21) = true ),
% 1.58/0.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.58/0.98 fof(f4,negated_conjecture,(
% 1.58/0.98 (![X34]: (p7(X34,X34) = true ))),
% 1.58/0.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.58/0.98 fof(f8,negated_conjecture,(
% 1.58/0.98 p3(f4(f6(c21)),c22) = true ),
% 1.58/0.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.58/0.98 fof(f24,negated_conjecture,(
% 1.58/0.98 (![X6,X7,X5,X4]: (ifeq(p19(X6,X7),true,ifeq(p7(X7,X5),true,ifeq(p7(X6,X4),true,p19(X4,X5),true),true),true) = true ))),
% 1.58/0.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.58/0.98 fof(f26,negated_conjecture,(
% 1.58/0.98 (![X42,X44,X41,X43]: (ifeq(p3(X42,X44),true,ifeq(p7(X41,X43),true,p7(f11(X41,X42),f11(X43,X44)),true),true) = true ))),
% 1.58/0.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.58/0.98 fof(f27,negated_conjecture,(
% 1.58/0.98 (![X38,X40,X37,X39]: (ifeq(p7(X38,X40),true,ifeq(p7(X37,X39),true,p7(f10(X37,X38),f10(X39,X40)),true),true) = true ))),
% 1.58/0.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.58/0.98 fof(f28,negated_conjecture,(
% 1.58/0.98 p19(f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21))) != true ),
% 1.58/0.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.58/0.98 fof(f29,negated_conjecture,(
% 1.58/0.98 (![X8]: (ifeq(p18(X8),true,p19(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(X8))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X8))),true) = true ))),
% 1.58/0.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.58/0.98 fof(f31,plain,(
% 1.58/0.98 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 1.58/0.98 inference(cnf_transformation,[status(thm)],[f1])).
% 1.58/0.98 fof(f33,plain,(
% 1.58/0.98 p18(c21)=true),
% 1.58/0.98 inference(cnf_transformation,[status(thm)],[f3])).
% 1.58/0.98 fof(f34,plain,(
% 1.58/0.98 ![X0]: (p7(X0,X0)=true)),
% 1.58/0.98 inference(cnf_transformation,[status(thm)],[f4])).
% 1.58/0.98 fof(f38,plain,(
% 1.58/0.98 p3(f4(f6(c21)),c22)=true),
% 1.58/0.98 inference(cnf_transformation,[status(thm)],[f8])).
% 1.58/0.98 fof(f54,plain,(
% 1.58/0.98 ![X0,X1,X2,X3]: (ifeq(p19(X0,X1),true,ifeq(p7(X1,X2),true,ifeq(p7(X0,X3),true,p19(X3,X2),true),true),true)=true)),
% 1.58/0.98 inference(cnf_transformation,[status(thm)],[f24])).
% 1.58/0.98 fof(f56,plain,(
% 1.58/0.98 ![X0,X1,X2,X3]: (ifeq(p3(X0,X1),true,ifeq(p7(X2,X3),true,p7(f11(X2,X0),f11(X3,X1)),true),true)=true)),
% 1.58/0.98 inference(cnf_transformation,[status(thm)],[f26])).
% 1.58/0.98 fof(f57,plain,(
% 1.58/0.98 ![X0,X1,X2,X3]: (ifeq(p7(X0,X1),true,ifeq(p7(X2,X3),true,p7(f10(X2,X0),f10(X3,X1)),true),true)=true)),
% 1.58/0.98 inference(cnf_transformation,[status(thm)],[f27])).
% 1.58/0.98 fof(f58,plain,(
% 1.58/0.98 ~p19(f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21)))=true),
% 1.58/0.98 inference(cnf_transformation,[status(thm)],[f28])).
% 1.58/0.98 fof(f59,plain,(
% 1.58/0.98 ![X0]: (ifeq(p18(X0),true,p19(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(X0))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true)=true)),
% 1.58/0.98 inference(cnf_transformation,[status(thm)],[f29])).
% 1.58/0.98 fof(f863,plain,(
% 1.58/0.98 ![X0,X1,X2]: (ifeq(p19(X0,X1),true,ifeq(true,true,ifeq(p7(X0,X2),true,p19(X2,X1),true),true),true)=true)),
% 1.58/0.98 inference(paramodulation,[status(thm)],[f34,f54])).
% 1.58/0.98 fof(f869,plain,(
% 1.58/0.98 ![X0,X1,X2]: (ifeq(p19(X0,X1),true,ifeq(p7(X0,X2),true,p19(X2,X1),true),true)=true)),
% 1.58/0.98 inference(forward_demodulation,[status(thm)],[f31,f863])).
% 1.58/0.98 fof(f1014,plain,(
% 1.58/0.98 ![X0,X1,X2]: (ifeq(p3(X0,X1),true,ifeq(true,true,p7(f11(X2,X0),f11(X2,X1)),true),true)=true)),
% 1.58/0.98 inference(paramodulation,[status(thm)],[f34,f56])).
% 1.58/0.98 fof(f1048,plain,(
% 1.58/0.98 ![X0,X1,X2]: (ifeq(p3(X0,X1),true,p7(f11(X2,X0),f11(X2,X1)),true)=true)),
% 1.58/0.98 inference(forward_demodulation,[status(thm)],[f31,f1014])).
% 1.58/0.98 fof(f1194,plain,(
% 1.58/0.98 ![X0,X1,X2]: (ifeq(true,true,ifeq(p7(X0,X1),true,p7(f10(X0,X2),f10(X1,X2)),true),true)=true)),
% 1.58/0.98 inference(paramodulation,[status(thm)],[f34,f57])).
% 1.58/0.98 fof(f1213,plain,(
% 1.58/0.98 ![X0,X1,X2]: (ifeq(p7(X0,X1),true,p7(f10(X0,X2),f10(X1,X2)),true)=true)),
% 1.58/0.98 inference(forward_demodulation,[status(thm)],[f31,f1194])).
% 1.58/1.01 fof(f1550,plain,(
% 1.58/1.01 ifeq(true,true,p19(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(c21))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21))),true)=true),
% 1.58/1.01 inference(paramodulation,[status(thm)],[f33,f59])).
% 1.58/1.01 fof(f1551,plain,(
% 1.58/1.01 p19(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(c21))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21)))=true),
% 1.58/1.01 inference(forward_demodulation,[status(thm)],[f31,f1550])).
% 1.58/1.01 fof(f1947,plain,(
% 1.58/1.01 ![X0]: (ifeq(true,true,p7(f11(X0,f4(f6(c21))),f11(X0,c22)),true)=true)),
% 1.58/1.01 inference(paramodulation,[status(thm)],[f38,f1048])).
% 1.58/1.01 fof(f1991,plain,(
% 1.58/1.01 ![X0]: (p7(f11(X0,f4(f6(c21))),f11(X0,c22))=true)),
% 1.58/1.01 inference(forward_demodulation,[status(thm)],[f31,f1947])).
% 1.58/1.01 fof(f2085,plain,(
% 1.58/1.01 ![X0,X1]: (ifeq(true,true,p7(f10(f11(X0,f4(f6(c21))),X1),f10(f11(X0,c22),X1)),true)=true)),
% 1.58/1.01 inference(paramodulation,[status(thm)],[f1991,f1213])).
% 1.58/1.01 fof(f2103,plain,(
% 1.58/1.01 ![X0,X1]: (p7(f10(f11(X0,f4(f6(c21))),X1),f10(f11(X0,c22),X1))=true)),
% 1.58/1.01 inference(forward_demodulation,[status(thm)],[f31,f2085])).
% 1.58/1.01 fof(f4110,plain,(
% 1.58/1.01 ![X0]: (ifeq(true,true,ifeq(p7(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(c21))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),X0),true,p19(X0,f8(f9(c21))),true),true)=true)),
% 1.58/1.01 inference(paramodulation,[status(thm)],[f1551,f869])).
% 1.58/1.01 fof(f4117,plain,(
% 1.58/1.01 ![X0]: (ifeq(p7(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(c21))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),X0),true,p19(X0,f8(f9(c21))),true)=true)),
% 1.58/1.01 inference(forward_demodulation,[status(thm)],[f31,f4110])).
% 1.58/1.01 fof(f12714,plain,(
% 1.58/1.01 ifeq(true,true,p19(f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21))),true)=true),
% 1.58/1.01 inference(paramodulation,[status(thm)],[f2103,f4117])).
% 1.58/1.01 fof(f12720,plain,(
% 1.58/1.01 p19(f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21)))=true),
% 1.58/1.01 inference(forward_demodulation,[status(thm)],[f31,f12714])).
% 1.58/1.01 fof(f12721,plain,(
% 1.58/1.01 $false),
% 1.58/1.01 inference(forward_subsumption_resolution,[status(thm)],[f12720,f58])).
% 1.58/1.01 % SZS output end CNFRefutation for theBenchmark.p
% 11.27/2.24 % Elapsed time: 1.506858 seconds
% 11.27/2.24 % CPU time: 1.996599 seconds
% 11.27/2.24 % Total memory used: 106.729 MB
% 11.27/2.24 % Net memory used: 106.364 MB
%------------------------------------------------------------------------------