%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN604-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 : n016.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:13 PM UTC 2026
% Result : Unsatisfiable 28.51s 4.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN604-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.09/0.35 % Computer : n016.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:14:38 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 28.51/4.10 % Refutation found
% 28.51/4.10 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 28.51/4.10 % SZS output start CNFRefutation for theBenchmark
% 28.51/4.10 fof(f4,negated_conjecture,(
% 28.51/4.10 (![X31]: (p3(X31,X31) ))),
% 28.51/4.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.51/4.10 fof(f7,negated_conjecture,(
% 28.51/4.10 (![X41]: (p3(f4(f8(X41)),f12(X41)) ))),
% 28.51/4.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.51/4.10 fof(f8,negated_conjecture,(
% 28.51/4.10 (![X38]: (p3(f12(f10(X38)),f10(X38)) ))),
% 28.51/4.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.51/4.10 fof(f9,negated_conjecture,(
% 28.51/4.10 (![X16]: (p16(f10(f11(c21)),f12(X16)) ))),
% 28.51/4.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.51/4.10 fof(f10,negated_conjecture,(
% 28.51/4.10 (![X14,X15]: (( p16(X14,X15)| p16(X15,f12(X14)) ) ))),
% 28.51/4.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.51/4.10 fof(f21,negated_conjecture,(
% 28.51/4.10 (![X32,X33,X31]: (( p3(X32,X33)| ~ p3(X31,X32)| ~ p3(X31,X33) ) ))),
% 28.51/4.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.51/4.10 fof(f23,negated_conjecture,(
% 28.51/4.10 (![X11,X12,X13]: (( p16(X11,X12)| ~ p16(X11,X13)| ~ p16(X13,X12) ) ))),
% 28.51/4.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.51/4.10 fof(f25,negated_conjecture,(
% 28.51/4.10 (![X7,X8,X9,X10]: (( p16(X7,X8)| ~ p3(X9,X7)| ~ p3(X10,X8)| ~ p16(X9,X10) ) ))),
% 28.51/4.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.51/4.10 fof(f28,negated_conjecture,(
% 28.51/4.10 (![X54]: (~ p16(f4(f6(f7(c20,c18),X54)),f4(f6(f7(c20,c18),f13(X54)))) ))),
% 28.51/4.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.51/4.10 fof(f29,negated_conjecture,(
% 28.51/4.10 (![X18]: (( p16(f4(f6(f7(c20,c18),c23)),f4(f6(f7(c20,c18),X18)))| ~ p16(f4(X18),f12(c19)) ) ))),
% 28.51/4.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.51/4.10 fof(f30,negated_conjecture,(
% 28.51/4.10 (![X19]: (( p16(f4(f6(f7(c20,c18),f8(f10(f11(c21))))),f4(f6(f7(c20,c18),X19)))| ~ p16(c19,f4(X19)) ) ))),
% 28.51/4.10 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.51/4.10 fof(f34,plain,(
% 28.51/4.10 ![X0]: (p3(X0,X0))),
% 28.51/4.10 inference(cnf_transformation,[status(thm)],[f4])).
% 28.51/4.10 fof(f37,plain,(
% 28.51/4.10 ![X0]: (p3(f4(f8(X0)),f12(X0)))),
% 28.51/4.10 inference(cnf_transformation,[status(thm)],[f7])).
% 28.51/4.10 fof(f38,plain,(
% 28.51/4.10 ![X0]: (p3(f12(f10(X0)),f10(X0)))),
% 28.51/4.10 inference(cnf_transformation,[status(thm)],[f8])).
% 28.51/4.10 fof(f39,plain,(
% 28.51/4.10 ![X0]: (p16(f10(f11(c21)),f12(X0)))),
% 28.51/4.10 inference(cnf_transformation,[status(thm)],[f9])).
% 28.51/4.10 fof(f40,plain,(
% 28.51/4.10 ![X0,X1]: (p16(X0,X1)|p16(X1,f12(X0)))),
% 28.51/4.10 inference(cnf_transformation,[status(thm)],[f10])).
% 28.51/4.10 fof(f54,plain,(
% 28.51/4.10 ![X33,X31]: ((![X32]: (p3(X32,X33)|~p3(X31,X32)))|~p3(X31,X33))),
% 28.51/4.10 inference(miniscoping,[status(thm)],[f21])).
% 28.51/4.10 fof(f55,plain,(
% 28.51/4.10 ![X0,X1,X2]: (p3(X0,X1)|~p3(X2,X0)|~p3(X2,X1))),
% 28.51/4.10 inference(cnf_transformation,[status(thm)],[f54])).
% 28.51/4.10 fof(f58,plain,(
% 28.51/4.10 ![X12,X13]: ((![X11]: (p16(X11,X12)|~p16(X11,X13)))|~p16(X13,X12))),
% 28.51/4.10 inference(miniscoping,[status(thm)],[f23])).
% 28.51/4.10 fof(f59,plain,(
% 28.51/4.10 ![X0,X1,X2]: (p16(X0,X1)|~p16(X0,X2)|~p16(X2,X1))),
% 28.51/4.10 inference(cnf_transformation,[status(thm)],[f58])).
% 28.51/4.10 fof(f62,plain,(
% 28.51/4.10 ![X9,X10]: ((![X8]: ((![X7]: (p16(X7,X8)|~p3(X9,X7)))|~p3(X10,X8)))|~p16(X9,X10))),
% 28.51/4.10 inference(miniscoping,[status(thm)],[f25])).
% 28.51/4.10 fof(f63,plain,(
% 28.51/4.10 ![X0,X1,X2,X3]: (p16(X0,X1)|~p3(X2,X0)|~p3(X3,X1)|~p16(X2,X3))),
% 28.51/4.10 inference(cnf_transformation,[status(thm)],[f62])).
% 28.51/4.10 fof(f68,plain,(
% 28.51/4.10 ![X0]: (~p16(f4(f6(f7(c20,c18),X0)),f4(f6(f7(c20,c18),f13(X0)))))),
% 28.51/4.10 inference(cnf_transformation,[status(thm)],[f28])).
% 28.51/4.10 fof(f69,plain,(
% 28.51/4.10 ![X0]: (p16(f4(f6(f7(c20,c18),c23)),f4(f6(f7(c20,c18),X0)))|~p16(f4(X0),f12(c19)))),
% 28.51/4.10 inference(cnf_transformation,[status(thm)],[f29])).
% 28.51/4.10 fof(f70,plain,(
% 28.51/4.10 ![X0]: (p16(f4(f6(f7(c20,c18),f8(f10(f11(c21))))),f4(f6(f7(c20,c18),X0)))|~p16(c19,f4(X0)))),
% 28.51/4.10 inference(cnf_transformation,[status(thm)],[f30])).
% 28.51/4.10 fof(f72,plain,(
% 28.51/4.10 ![X0,X1]: (~p16(f4(f6(f7(c20,c18),X0)),X1)|~p16(X1,f4(f6(f7(c20,c18),f13(X0)))))),
% 28.51/4.10 inference(resolution,[status(thm)],[f68,f59])).
% 28.51/4.10 fof(f73,plain,(
% 28.51/4.10 ~p16(f4(f13(c23)),f12(c19))),
% 28.51/4.10 inference(resolution,[status(thm)],[f69,f68])).
% 28.51/4.10 fof(f75,plain,(
% 28.51/4.10 p16(c19,f4(f13(c23)))),
% 28.51/4.10 inference(resolution,[status(thm)],[f73,f40])).
% 28.51/4.10 fof(f118,plain,(
% 28.51/4.10 ![X0]: (~p16(f4(f6(f7(c20,c18),X0)),f4(f6(f7(c20,c18),f8(f10(f11(c21))))))|~p16(c19,f4(f13(X0))))),
% 28.51/4.11 inference(resolution,[status(thm)],[f72,f70])).
% 28.51/4.11 fof(f200,plain,(
% 28.51/4.11 ~p16(c19,f4(f13(c23)))|~p16(f4(f8(f10(f11(c21)))),f12(c19))),
% 28.51/4.11 inference(resolution,[status(thm)],[f118,f69])).
% 28.51/4.11 fof(f210,definition,(
% 28.51/4.11 sQ13_spl <=> (p16(c19,f4(f13(c23))))),
% 28.51/4.11 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 28.51/4.11 fof(f212,plain,(
% 28.51/4.11 ~p16(c19,f4(f13(c23)))|sQ13_spl),
% 28.51/4.11 inference(component_clause,[status(thm)],[f210])).
% 28.51/4.11 fof(f213,definition,(
% 28.51/4.11 sQ14_spl <=> (p16(f4(f8(f10(f11(c21)))),f12(c19)))),
% 28.51/4.11 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 28.51/4.11 fof(f215,plain,(
% 28.51/4.11 ~p16(f4(f8(f10(f11(c21)))),f12(c19))|sQ14_spl),
% 28.51/4.11 inference(component_clause,[status(thm)],[f213])).
% 28.51/4.11 fof(f216,plain,(
% 28.51/4.11 ~sQ13_spl|~sQ14_spl),
% 28.51/4.11 inference(split_clause,[status(thm)],[f200,f210,f213])).
% 28.51/4.11 fof(f217,plain,(
% 28.51/4.11 $false|sQ13_spl),
% 28.51/4.11 inference(forward_subsumption_resolution,[status(thm)],[f212,f75])).
% 28.51/4.11 fof(f218,plain,(
% 28.51/4.11 sQ13_spl),
% 28.51/4.11 inference(contradiction_clause,[status(thm)],[f217])).
% 28.51/4.11 fof(f224,plain,(
% 28.51/4.11 ![X0,X1]: (~p3(X0,f4(f8(f10(f11(c21)))))|~p3(X1,f12(c19))|~p16(X0,X1)|sQ14_spl)),
% 28.51/4.11 inference(resolution,[status(thm)],[f215,f63])).
% 28.51/4.11 fof(f738,plain,(
% 28.51/4.11 ![X0,X1,X2]: (~p3(X0,f12(c19))|~p16(X1,X0)|~p3(X2,X1)|~p3(X2,f4(f8(f10(f11(c21)))))|sQ14_spl)),
% 28.51/4.11 inference(resolution,[status(thm)],[f224,f55])).
% 28.51/4.11 fof(f2044,plain,(
% 28.51/4.11 ![X0,X1]: (~p3(X0,f12(c19))|~p16(X1,X0)|~p3(f4(f8(f10(f11(c21)))),X1)|sQ14_spl)),
% 28.51/4.11 inference(resolution,[status(thm)],[f738,f34])).
% 28.51/4.11 fof(f3618,plain,(
% 28.51/4.11 ![X0]: (~p3(X0,f12(c19))|~p16(f12(f10(f11(c21))),X0)|sQ14_spl)),
% 28.51/4.11 inference(resolution,[status(thm)],[f2044,f37])).
% 28.51/4.11 fof(f3625,plain,(
% 28.51/4.11 ~p16(f12(f10(f11(c21))),f12(c19))|sQ14_spl),
% 28.51/4.11 inference(resolution,[status(thm)],[f3618,f34])).
% 28.51/4.11 fof(f3627,plain,(
% 28.51/4.11 ![X0,X1]: (~p3(X0,f12(f10(f11(c21))))|~p3(X1,f12(c19))|~p16(X0,X1)|sQ14_spl)),
% 28.51/4.11 inference(resolution,[status(thm)],[f3625,f63])).
% 28.51/4.11 fof(f3866,plain,(
% 28.51/4.11 ![X0]: (~p3(X0,f12(f10(f11(c21))))|~p16(X0,f12(c19))|sQ14_spl)),
% 28.51/4.11 inference(resolution,[status(thm)],[f3627,f34])).
% 28.51/4.11 fof(f3869,plain,(
% 28.51/4.11 ![X0,X1]: (~p16(X0,f12(c19))|~p3(X1,X0)|~p3(X1,f12(f10(f11(c21))))|sQ14_spl)),
% 28.51/4.11 inference(resolution,[status(thm)],[f3866,f55])).
% 28.51/4.11 fof(f4035,plain,(
% 28.51/4.11 ![X0]: (~p16(X0,f12(c19))|~p3(f12(f10(f11(c21))),X0)|sQ14_spl)),
% 28.51/4.11 inference(resolution,[status(thm)],[f3869,f34])).
% 28.51/4.11 fof(f4036,plain,(
% 28.51/4.11 ~p16(f10(f11(c21)),f12(c19))|sQ14_spl),
% 28.51/4.11 inference(resolution,[status(thm)],[f4035,f38])).
% 28.51/4.11 fof(f4040,plain,(
% 28.51/4.11 $false|sQ14_spl),
% 28.51/4.11 inference(forward_subsumption_resolution,[status(thm)],[f4036,f39])).
% 28.51/4.11 fof(f4041,plain,(
% 28.51/4.11 sQ14_spl),
% 28.51/4.11 inference(contradiction_clause,[status(thm)],[f4040])).
% 28.51/4.11 fof(f4042,plain,(
% 28.51/4.11 $false),
% 28.51/4.11 inference(sat_refutation,[status(thm)],[f216,f218,f4041])).
% 28.51/4.11 % SZS output end CNFRefutation for theBenchmark.p
% 26.61/4.14 % Elapsed time: 3.768365 seconds
% 26.61/4.14 % CPU time: 29.521878 seconds
% 26.61/4.14 % Total memory used: 143.390 MB
% 26.61/4.14 % Net memory used: 86.774 MB
%------------------------------------------------------------------------------