%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN628-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 : n014.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:15 PM UTC 2026
% Result : Unsatisfiable 0.11s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN628-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n014.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 11:10:34 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 0.11/0.38 % Refutation found
% 0.11/0.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.11/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.38 fof(f1,negated_conjecture,(
% 0.11/0.38 (![X4]: (p2(X4,X4) ))),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f2,negated_conjecture,(
% 0.11/0.38 (![X40]: (p9(X40,X40) ))),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f6,negated_conjecture,(
% 0.11/0.38 p9(c28,c22) ),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f13,negated_conjecture,(
% 0.11/0.38 (![X53,X54]: (( p9(f16(X53),f16(X54))| ~ p9(X53,X54) ) ))),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f26,negated_conjecture,(
% 0.11/0.38 (![X11,X12,X13,X14]: (( p20(X11,X12)| ~ p9(X13,X11)| ~ p9(X14,X12)| ~ p20(X13,X14) ) ))),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f29,negated_conjecture,(
% 0.11/0.38 (![X55,X56,X57,X58]: (( p9(f17(X55,X56),f17(X57,X58))| ~ p9(X55,X57)| ~ p9(X56,X58) ) ))),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f30,negated_conjecture,(
% 0.11/0.38 (![X49,X50,X51,X52]: (( p9(f15(X49,X50),f15(X51,X52))| ~ p2(X49,X51)| ~ p9(X50,X52) ) ))),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f31,negated_conjecture,(
% 0.11/0.38 (![X43,X44,X45,X46]: (( p9(f10(X43,X44),f10(X45,X46))| ~ p9(X43,X45)| ~ p9(X44,X46) ) ))),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f34,negated_conjecture,(
% 0.11/0.38 p20(f16(f17(c28,c27)),f10(f15(f7(c23,f8(c24,c25)),c28),f11(f12(f13(f14(c29)))))) ),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f35,negated_conjecture,(
% 0.11/0.38 ~ p20(f16(f17(c22,c27)),f10(f15(f7(c23,f8(c24,c25)),c22),f11(f12(f13(f14(c29)))))) ),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f37,plain,(
% 0.11/0.38 ![X0]: (p2(X0,X0))),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f1])).
% 0.11/0.38 fof(f38,plain,(
% 0.11/0.38 ![X0]: (p9(X0,X0))),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f2])).
% 0.11/0.38 fof(f42,plain,(
% 0.11/0.38 p9(c28,c22)),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f6])).
% 0.11/0.38 fof(f49,plain,(
% 0.11/0.38 ![X0,X1]: (p9(f16(X0),f16(X1))|~p9(X0,X1))),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f13])).
% 0.11/0.38 fof(f69,plain,(
% 0.11/0.38 ![X13,X14]: ((![X12]: ((![X11]: (p20(X11,X12)|~p9(X13,X11)))|~p9(X14,X12)))|~p20(X13,X14))),
% 0.11/0.38 inference(miniscoping,[status(thm)],[f26])).
% 0.11/0.38 fof(f70,plain,(
% 0.11/0.38 ![X0,X1,X2,X3]: (p20(X0,X1)|~p9(X2,X0)|~p9(X3,X1)|~p20(X2,X3))),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f69])).
% 0.11/0.38 fof(f75,plain,(
% 0.11/0.38 ![X56,X58]: ((![X55,X57]: (p9(f17(X55,X56),f17(X57,X58))|~p9(X55,X57)))|~p9(X56,X58))),
% 0.11/0.38 inference(miniscoping,[status(thm)],[f29])).
% 0.11/0.38 fof(f76,plain,(
% 0.11/0.38 ![X0,X1,X2,X3]: (p9(f17(X0,X1),f17(X2,X3))|~p9(X0,X2)|~p9(X1,X3))),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f75])).
% 0.11/0.38 fof(f77,plain,(
% 0.11/0.38 ![X50,X52]: ((![X49,X51]: (p9(f15(X49,X50),f15(X51,X52))|~p2(X49,X51)))|~p9(X50,X52))),
% 0.11/0.38 inference(miniscoping,[status(thm)],[f30])).
% 0.11/0.38 fof(f78,plain,(
% 0.11/0.38 ![X0,X1,X2,X3]: (p9(f15(X0,X1),f15(X2,X3))|~p2(X0,X2)|~p9(X1,X3))),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f77])).
% 0.11/0.38 fof(f79,plain,(
% 0.11/0.38 ![X44,X46]: ((![X43,X45]: (p9(f10(X43,X44),f10(X45,X46))|~p9(X43,X45)))|~p9(X44,X46))),
% 0.11/0.38 inference(miniscoping,[status(thm)],[f31])).
% 0.11/0.38 fof(f80,plain,(
% 0.11/0.38 ![X0,X1,X2,X3]: (p9(f10(X0,X1),f10(X2,X3))|~p9(X0,X2)|~p9(X1,X3))),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f79])).
% 0.11/0.38 fof(f84,plain,(
% 0.11/0.38 p20(f16(f17(c28,c27)),f10(f15(f7(c23,f8(c24,c25)),c28),f11(f12(f13(f14(c29))))))),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f34])).
% 0.11/0.38 fof(f85,plain,(
% 0.11/0.38 ~p20(f16(f17(c22,c27)),f10(f15(f7(c23,f8(c24,c25)),c22),f11(f12(f13(f14(c29))))))),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f35])).
% 0.11/0.38 fof(f89,plain,(
% 0.11/0.38 ![X0,X1]: (~p9(X0,f16(f17(c22,c27)))|~p9(X1,f10(f15(f7(c23,f8(c24,c25)),c22),f11(f12(f13(f14(c29))))))|~p20(X0,X1))),
% 0.11/0.38 inference(resolution,[status(thm)],[f85,f70])).
% 0.11/0.38 fof(f93,plain,(
% 0.11/0.38 ![X0,X1,X2]: (~p9(X0,f16(f17(c22,c27)))|~p20(X0,f10(X1,X2))|~p9(X1,f15(f7(c23,f8(c24,c25)),c22))|~p9(X2,f11(f12(f13(f14(c29))))))),
% 0.11/0.38 inference(resolution,[status(thm)],[f89,f80])).
% 0.11/0.38 fof(f101,plain,(
% 0.11/0.38 ~p9(f16(f17(c28,c27)),f16(f17(c22,c27)))|~p9(f15(f7(c23,f8(c24,c25)),c28),f15(f7(c23,f8(c24,c25)),c22))|~p9(f11(f12(f13(f14(c29)))),f11(f12(f13(f14(c29)))))),
% 0.11/0.38 inference(resolution,[status(thm)],[f93,f84])).
% 0.11/0.38 fof(f103,plain,(
% 0.11/0.38 ~p9(f16(f17(c28,c27)),f16(f17(c22,c27)))|~p9(f15(f7(c23,f8(c24,c25)),c28),f15(f7(c23,f8(c24,c25)),c22))),
% 0.11/0.38 inference(forward_subsumption_resolution,[status(thm)],[f101,f38])).
% 0.11/0.38 fof(f117,plain,(
% 0.11/0.38 ~p9(f16(f17(c28,c27)),f16(f17(c22,c27)))|~p2(f7(c23,f8(c24,c25)),f7(c23,f8(c24,c25)))|~p9(c28,c22)),
% 0.11/0.38 inference(resolution,[status(thm)],[f103,f78])).
% 0.11/0.38 fof(f119,plain,(
% 0.11/0.38 ~p9(f16(f17(c28,c27)),f16(f17(c22,c27)))|~p9(c28,c22)),
% 0.11/0.38 inference(forward_subsumption_resolution,[status(thm)],[f117,f37])).
% 0.11/0.38 fof(f120,plain,(
% 0.11/0.38 ~p9(f16(f17(c28,c27)),f16(f17(c22,c27)))),
% 0.11/0.38 inference(forward_subsumption_resolution,[status(thm)],[f119,f42])).
% 0.11/0.38 fof(f121,plain,(
% 0.11/0.38 ~p9(f17(c28,c27),f17(c22,c27))),
% 0.11/0.38 inference(resolution,[status(thm)],[f120,f49])).
% 0.11/0.38 fof(f123,plain,(
% 0.11/0.38 ~p9(c28,c22)|~p9(c27,c27)),
% 0.11/0.38 inference(resolution,[status(thm)],[f121,f76])).
% 0.11/0.38 fof(f125,plain,(
% 0.11/0.38 ~p9(c27,c27)),
% 0.11/0.38 inference(forward_subsumption_resolution,[status(thm)],[f123,f42])).
% 0.11/0.38 fof(f126,plain,(
% 0.11/0.38 $false),
% 0.11/0.38 inference(forward_subsumption_resolution,[status(thm)],[f125,f38])).
% 0.11/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.40 % Elapsed time: 0.055191 seconds
% 0.11/0.40 % CPU time: 0.176792 seconds
% 0.11/0.40 % Total memory used: 57.962 MB
% 0.11/0.40 % Net memory used: 57.701 MB
%------------------------------------------------------------------------------