%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN617-1 : TPTP v9.3.1. Released v2.5.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 03:20:14 PM UTC 2026
% Result : Unsatisfiable 26.17s 3.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN617-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n026.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 11:12:51 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 26.17/3.72 % Refutation found
% 26.17/3.72 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 26.17/3.72 % SZS output start CNFRefutation for theBenchmark
% 26.17/3.72 fof(f1,negated_conjecture,(
% 26.17/3.72 (![X0]: (p11(X0,X0) ))),
% 26.17/3.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.17/3.72 fof(f4,negated_conjecture,(
% 26.17/3.72 (![X27]: (p2(X27,X27) ))),
% 26.17/3.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.17/3.72 fof(f5,negated_conjecture,(
% 26.17/3.72 (![X11]: (p13(X11,X11) ))),
% 26.17/3.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.17/3.72 fof(f6,negated_conjecture,(
% 26.17/3.72 p19(c21,c22) ),
% 26.17/3.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.17/3.72 fof(f7,negated_conjecture,(
% 26.17/3.72 (![X5,X6]: (p11(f12(f14(X5,X6)),X6) ))),
% 26.17/3.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.17/3.72 fof(f19,negated_conjecture,(
% 26.17/3.72 (![X18,X19]: (p13(f15(f3(X18),X19),f15(X18,f12(X19))) ))),
% 26.17/3.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.17/3.72 fof(f24,negated_conjecture,(
% 26.17/3.72 (![X12,X13,X11]: (( p13(X12,X13)| ~ p13(X11,X12)| ~ p13(X11,X13) ) ))),
% 26.17/3.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.17/3.72 fof(f28,negated_conjecture,(
% 26.17/3.72 (![X14,X15,X16,X17]: (( p13(f15(X14,X15),f15(X16,X17))| ~ p11(X15,X17)| ~ p2(X14,X16) ) ))),
% 26.17/3.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.17/3.72 fof(f31,negated_conjecture,(
% 26.17/3.72 (![X36,X37]: (( p2(f4(f4(f3(X36),f5(f6(c20))),X37),f3(f4(f4(X36,f5(f6(c20))),X37)))| ~ p19(X37,X36) ) ))),
% 26.17/3.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.17/3.72 fof(f32,negated_conjecture,(
% 26.17/3.72 ~ p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24)) ),
% 26.17/3.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.17/3.72 fof(f33,plain,(
% 26.17/3.72 ![X0]: (p11(X0,X0))),
% 26.17/3.72 inference(cnf_transformation,[status(thm)],[f1])).
% 26.17/3.72 fof(f36,plain,(
% 26.17/3.72 ![X0]: (p2(X0,X0))),
% 26.17/3.72 inference(cnf_transformation,[status(thm)],[f4])).
% 26.17/3.72 fof(f37,plain,(
% 26.17/3.72 ![X0]: (p13(X0,X0))),
% 26.17/3.72 inference(cnf_transformation,[status(thm)],[f5])).
% 26.17/3.72 fof(f38,plain,(
% 26.17/3.72 p19(c21,c22)),
% 26.17/3.72 inference(cnf_transformation,[status(thm)],[f6])).
% 26.17/3.72 fof(f39,plain,(
% 26.17/3.72 ![X0,X1]: (p11(f12(f14(X0,X1)),X1))),
% 26.17/3.72 inference(cnf_transformation,[status(thm)],[f7])).
% 26.17/3.72 fof(f51,plain,(
% 26.17/3.72 ![X0,X1]: (p13(f15(f3(X0),X1),f15(X0,f12(X1))))),
% 26.17/3.72 inference(cnf_transformation,[status(thm)],[f19])).
% 26.17/3.72 fof(f60,plain,(
% 26.17/3.72 ![X13,X11]: ((![X12]: (p13(X12,X13)|~p13(X11,X12)))|~p13(X11,X13))),
% 26.17/3.72 inference(miniscoping,[status(thm)],[f24])).
% 26.17/3.72 fof(f61,plain,(
% 26.17/3.72 ![X0,X1,X2]: (p13(X0,X1)|~p13(X2,X0)|~p13(X2,X1))),
% 26.17/3.72 inference(cnf_transformation,[status(thm)],[f60])).
% 26.17/3.72 fof(f68,plain,(
% 26.17/3.72 ![X14,X16]: ((![X15,X17]: (p13(f15(X14,X15),f15(X16,X17))|~p11(X15,X17)))|~p2(X14,X16))),
% 26.17/3.72 inference(miniscoping,[status(thm)],[f28])).
% 26.17/3.72 fof(f69,plain,(
% 26.17/3.72 ![X0,X1,X2,X3]: (p13(f15(X0,X1),f15(X2,X3))|~p11(X1,X3)|~p2(X0,X2))),
% 26.17/3.72 inference(cnf_transformation,[status(thm)],[f68])).
% 26.17/3.72 fof(f74,plain,(
% 26.17/3.72 ![X0,X1]: (p2(f4(f4(f3(X0),f5(f6(c20))),X1),f3(f4(f4(X0,f5(f6(c20))),X1)))|~p19(X1,X0))),
% 26.17/3.72 inference(cnf_transformation,[status(thm)],[f31])).
% 26.17/3.72 fof(f75,plain,(
% 26.17/3.72 ~p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24))),
% 26.17/3.72 inference(cnf_transformation,[status(thm)],[f32])).
% 26.17/3.72 fof(f77,plain,(
% 26.17/3.72 ![X0]: (~p13(X0,f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)))|~p13(X0,f15(f4(f4(c22,f5(f6(c20))),c21),c24)))),
% 26.17/3.72 inference(resolution,[status(thm)],[f75,f61])).
% 26.17/3.72 fof(f1608,plain,(
% 26.17/3.72 ![X0,X1]: (p13(X0,X1)|~p13(X1,X0))),
% 26.17/3.72 inference(resolution,[status(thm)],[f61,f37])).
% 26.17/3.72 fof(f1615,plain,(
% 26.17/3.72 ![X0,X1]: (p13(f15(X0,f12(X1)),f15(f3(X0),X1)))),
% 26.17/3.72 inference(resolution,[status(thm)],[f1608,f51])).
% 26.17/3.72 fof(f1616,plain,(
% 26.17/3.72 ![X0,X1,X2,X3]: (p13(f15(X0,X1),f15(X2,X3))|~p11(X3,X1)|~p2(X2,X0))),
% 26.17/3.72 inference(resolution,[status(thm)],[f1608,f69])).
% 26.17/3.72 fof(f1632,plain,(
% 26.17/3.72 ![X0,X1,X2]: (p13(X0,f15(f3(X1),X2))|~p13(f15(X1,f12(X2)),X0))),
% 26.17/3.72 inference(resolution,[status(thm)],[f1615,f61])).
% 26.17/3.72 fof(f1696,plain,(
% 26.17/3.72 ![X0,X1,X2,X3]: (p13(f15(X0,X1),f15(X2,f12(f14(X3,X1))))|~p2(X2,X0))),
% 26.17/3.72 inference(resolution,[status(thm)],[f1616,f39])).
% 26.17/3.72 fof(f1699,plain,(
% 26.17/3.72 ![X0,X1,X2]: (p13(f15(X0,X1),f15(X2,X1))|~p2(X2,X0))),
% 26.17/3.72 inference(resolution,[status(thm)],[f1616,f33])).
% 26.17/3.72 fof(f1700,plain,(
% 26.17/3.72 ![X0,X1,X2]: (p13(f15(f3(f4(f4(X0,f5(f6(c20))),X1)),X2),f15(f4(f4(f3(X0),f5(f6(c20))),X1),X2))|~p19(X1,X0))),
% 26.17/3.74 inference(resolution,[status(thm)],[f1699,f74])).
% 26.17/3.74 fof(f1932,plain,(
% 26.17/3.74 ![X0,X1,X2]: (p13(f15(X0,X1),f15(X0,f12(f14(X2,X1)))))),
% 26.17/3.74 inference(resolution,[status(thm)],[f1696,f36])).
% 26.17/3.74 fof(f1945,plain,(
% 26.17/3.74 ![X0,X1,X2]: (p13(f15(X0,f12(f14(X1,X2))),f15(X0,X2)))),
% 26.17/3.74 inference(resolution,[status(thm)],[f1932,f1608])).
% 26.17/3.74 fof(f1962,plain,(
% 26.17/3.74 ![X0,X1,X2]: (p13(f15(X0,X1),f15(f3(X0),f14(X2,X1))))),
% 26.17/3.74 inference(resolution,[status(thm)],[f1945,f1632])).
% 26.17/3.74 fof(f2008,plain,(
% 26.17/3.74 ![X0,X1,X2]: (p13(f15(f3(X0),f14(X1,X2)),f15(X0,X2)))),
% 26.17/3.74 inference(resolution,[status(thm)],[f1962,f1608])).
% 26.17/3.74 fof(f2586,plain,(
% 26.17/3.74 ![X0]: (p13(f15(f3(f4(f4(c22,f5(f6(c20))),c21)),X0),f15(f4(f4(f3(c22),f5(f6(c20))),c21),X0)))),
% 26.17/3.74 inference(resolution,[status(thm)],[f1700,f38])).
% 26.17/3.74 fof(f8449,plain,(
% 26.17/3.74 ~p13(f15(f3(f4(f4(c22,f5(f6(c20))),c21)),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24))),
% 26.17/3.74 inference(resolution,[status(thm)],[f2586,f77])).
% 26.17/3.74 fof(f8455,plain,(
% 26.17/3.74 $false),
% 26.17/3.74 inference(forward_subsumption_resolution,[status(thm)],[f8449,f2008])).
% 26.17/3.74 % SZS output end CNFRefutation for theBenchmark.p
% 26.17/3.78 % Elapsed time: 3.402959 seconds
% 26.17/3.78 % CPU time: 26.608351 seconds
% 26.17/3.78 % Total memory used: 353.130 MB
% 26.17/3.78 % Net memory used: 265.293 MB
%------------------------------------------------------------------------------