%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN631-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 : 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 03:20:16 PM UTC 2026
% Result : Unsatisfiable 0.24s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN631-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n015.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 11:13:51 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 0.24/0.52 % Refutation found
% 0.24/0.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.24/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.24/0.52 fof(f1,negated_conjecture,(
% 0.24/0.52 (![X0]: (p10(X0,X0) ))),
% 0.24/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.52 fof(f5,negated_conjecture,(
% 0.24/0.52 (![X37]: (p5(X37,X37) ))),
% 0.24/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.52 fof(f11,negated_conjecture,(
% 0.24/0.52 (![X44,X45]: (p5(f16(f18(X44,X45)),X45) ))),
% 0.24/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.52 fof(f12,negated_conjecture,(
% 0.24/0.52 p23(f13(c27,f14(c28)),f11(f15(c24))) ),
% 0.24/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.52 fof(f13,negated_conjecture,(
% 0.24/0.52 ~ p23(f13(f16(c27),f14(c28)),f11(c24)) ),
% 0.24/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.52 fof(f18,negated_conjecture,(
% 0.24/0.52 (![X42,X43]: (( p5(f16(X42),f16(X43))| ~ p5(X42,X43) ) ))),
% 0.24/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.52 fof(f25,negated_conjecture,(
% 0.24/0.52 (![X38,X39,X37]: (( p5(X38,X39)| ~ p5(X37,X38)| ~ p5(X37,X39) ) ))),
% 0.24/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.52 fof(f29,negated_conjecture,(
% 0.24/0.52 (![X25,X26,X28,X27]: (( p23(X25,X26)| ~ p12(X28,X25)| ~ p23(X28,X27)| ~ p10(X27,X26) ) ))),
% 0.24/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.52 fof(f32,negated_conjecture,(
% 0.24/0.52 (![X8,X9,X10,X11]: (( p12(f13(X8,X9),f13(X10,X11))| ~ p5(X8,X10)| ~ p5(X9,X11) ) ))),
% 0.24/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.52 fof(f34,negated_conjecture,(
% 0.24/0.52 (![X30,X29,X31]: (( p5(X30,f18(f20(c29),f19(X29,X30,X31)))| ~ p23(f13(X30,X31),f11(f15(X29))) ) ))),
% 0.24/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.52 fof(f35,negated_conjecture,(
% 0.24/0.52 (![X29,X30,X31]: (( p23(f13(f19(X29,X30,X31),X31),f11(X29))| ~ p23(f13(X30,X31),f11(f15(X29))) ) ))),
% 0.24/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.52 fof(f39,plain,(
% 0.24/0.52 ![X0]: (p10(X0,X0))),
% 0.24/0.52 inference(cnf_transformation,[status(thm)],[f1])).
% 0.24/0.52 fof(f43,plain,(
% 0.24/0.52 ![X0]: (p5(X0,X0))),
% 0.24/0.52 inference(cnf_transformation,[status(thm)],[f5])).
% 0.24/0.52 fof(f49,plain,(
% 0.24/0.52 ![X0,X1]: (p5(f16(f18(X0,X1)),X1))),
% 0.24/0.52 inference(cnf_transformation,[status(thm)],[f11])).
% 0.24/0.52 fof(f50,plain,(
% 0.24/0.52 p23(f13(c27,f14(c28)),f11(f15(c24)))),
% 0.24/0.52 inference(cnf_transformation,[status(thm)],[f12])).
% 0.24/0.52 fof(f51,plain,(
% 0.24/0.52 ~p23(f13(f16(c27),f14(c28)),f11(c24))),
% 0.24/0.52 inference(cnf_transformation,[status(thm)],[f13])).
% 0.24/0.52 fof(f56,plain,(
% 0.24/0.52 ![X0,X1]: (p5(f16(X0),f16(X1))|~p5(X0,X1))),
% 0.24/0.52 inference(cnf_transformation,[status(thm)],[f18])).
% 0.24/0.52 fof(f67,plain,(
% 0.24/0.52 ![X39,X37]: ((![X38]: (p5(X38,X39)|~p5(X37,X38)))|~p5(X37,X39))),
% 0.24/0.52 inference(miniscoping,[status(thm)],[f25])).
% 0.24/0.52 fof(f68,plain,(
% 0.24/0.52 ![X0,X1,X2]: (p5(X0,X1)|~p5(X2,X0)|~p5(X2,X1))),
% 0.24/0.52 inference(cnf_transformation,[status(thm)],[f67])).
% 0.24/0.52 fof(f75,plain,(
% 0.24/0.52 ![X26,X27]: ((![X28]: ((![X25]: (p23(X25,X26)|~p12(X28,X25)))|~p23(X28,X27)))|~p10(X27,X26))),
% 0.24/0.52 inference(miniscoping,[status(thm)],[f29])).
% 0.24/0.52 fof(f76,plain,(
% 0.24/0.52 ![X0,X1,X2,X3]: (p23(X0,X1)|~p12(X2,X0)|~p23(X2,X3)|~p10(X3,X1))),
% 0.24/0.52 inference(cnf_transformation,[status(thm)],[f75])).
% 0.24/0.52 fof(f81,plain,(
% 0.24/0.52 ![X9,X11]: ((![X8,X10]: (p12(f13(X8,X9),f13(X10,X11))|~p5(X8,X10)))|~p5(X9,X11))),
% 0.24/0.52 inference(miniscoping,[status(thm)],[f32])).
% 0.24/0.52 fof(f82,plain,(
% 0.24/0.52 ![X0,X1,X2,X3]: (p12(f13(X0,X1),f13(X2,X3))|~p5(X0,X2)|~p5(X1,X3))),
% 0.24/0.52 inference(cnf_transformation,[status(thm)],[f81])).
% 0.24/0.52 fof(f85,plain,(
% 0.24/0.52 ![X0,X1,X2]: (p5(X0,f18(f20(c29),f19(X1,X0,X2)))|~p23(f13(X0,X2),f11(f15(X1))))),
% 0.24/0.52 inference(cnf_transformation,[status(thm)],[f34])).
% 0.24/0.52 fof(f86,plain,(
% 0.24/0.52 ![X0,X1,X2]: (p23(f13(f19(X0,X1,X2),X2),f11(X0))|~p23(f13(X1,X2),f11(f15(X0))))),
% 0.24/0.52 inference(cnf_transformation,[status(thm)],[f35])).
% 0.24/0.52 fof(f93,plain,(
% 0.24/0.52 ![X0,X1,X2,X3,X4]: (~p23(f13(X0,X1),f11(f15(X2)))|p23(X3,X4)|~p12(f13(f19(X2,X0,X1),X1),X3)|~p10(f11(X2),X4))),
% 0.24/0.52 inference(resolution,[status(thm)],[f86,f76])).
% 0.24/0.52 fof(f103,plain,(
% 0.24/0.52 ![X0,X1]: (p23(X0,X1)|~p12(f13(f19(c24,c27,f14(c28)),f14(c28)),X0)|~p10(f11(c24),X1))),
% 0.24/0.52 inference(resolution,[status(thm)],[f93,f50])).
% 0.24/0.52 fof(f123,plain,(
% 0.24/0.52 ![X0,X1,X2]: (p23(f13(X0,X1),X2)|~p10(f11(c24),X2)|~p5(f19(c24,c27,f14(c28)),X0)|~p5(f14(c28),X1))),
% 0.24/0.52 inference(resolution,[status(thm)],[f103,f82])).
% 0.24/0.52 fof(f160,plain,(
% 0.24/0.52 ![X0,X1]: (p23(f13(X0,X1),f11(c24))|~p5(f19(c24,c27,f14(c28)),X0)|~p5(f14(c28),X1))),
% 0.24/0.52 inference(resolution,[status(thm)],[f123,f39])).
% 0.24/0.52 fof(f263,plain,(
% 0.24/0.52 ~p5(f19(c24,c27,f14(c28)),f16(c27))|~p5(f14(c28),f14(c28))),
% 0.24/0.52 inference(resolution,[status(thm)],[f160,f51])).
% 0.24/0.52 fof(f266,plain,(
% 0.24/0.52 ~p5(f19(c24,c27,f14(c28)),f16(c27))),
% 0.24/0.52 inference(forward_subsumption_resolution,[status(thm)],[f263,f43])).
% 0.24/0.52 fof(f280,plain,(
% 0.24/0.52 ![X0]: (~p5(X0,f19(c24,c27,f14(c28)))|~p5(X0,f16(c27)))),
% 0.24/0.52 inference(resolution,[status(thm)],[f266,f68])).
% 0.24/0.52 fof(f286,plain,(
% 0.24/0.52 ![X0]: (~p5(f16(f18(X0,f19(c24,c27,f14(c28)))),f16(c27)))),
% 0.24/0.52 inference(resolution,[status(thm)],[f280,f49])).
% 0.24/0.52 fof(f290,plain,(
% 0.24/0.52 ![X0]: (~p5(f18(X0,f19(c24,c27,f14(c28))),c27))),
% 0.24/0.52 inference(resolution,[status(thm)],[f286,f56])).
% 0.24/0.52 fof(f300,plain,(
% 0.24/0.52 ![X0,X1]: (~p5(X0,f18(X1,f19(c24,c27,f14(c28))))|~p5(X0,c27))),
% 0.24/0.52 inference(resolution,[status(thm)],[f290,f68])).
% 0.24/0.52 fof(f305,plain,(
% 0.24/0.52 ![X0]: (~p5(c27,f18(X0,f19(c24,c27,f14(c28)))))),
% 0.24/0.52 inference(resolution,[status(thm)],[f300,f43])).
% 0.24/0.52 fof(f323,plain,(
% 0.24/0.52 ~p23(f13(c27,f14(c28)),f11(f15(c24)))),
% 0.24/0.52 inference(resolution,[status(thm)],[f305,f85])).
% 0.24/0.52 fof(f325,plain,(
% 0.24/0.52 $false),
% 0.24/0.52 inference(forward_subsumption_resolution,[status(thm)],[f323,f50])).
% 0.24/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.24/0.55 % Elapsed time: 0.086824 seconds
% 0.24/0.55 % CPU time: 0.328665 seconds
% 0.24/0.55 % Total memory used: 59.912 MB
% 0.24/0.55 % Net memory used: 59.286 MB
%------------------------------------------------------------------------------