%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN713-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:24 PM UTC 2026
% Result : Unsatisfiable 0.09s 5.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN713-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.35 % Computer : n004.cluster.edu
% 0.09/5.35 % Model : x86_64 x86_64
% 0.09/5.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.35 % Memory : 8046.5625MB
% 0.09/5.35 % OS : Linux 6.8.0-71-generic
% 0.09/5.35 % CPULimit : 300
% 0.09/5.35 % WCLimit : 300
% 0.09/5.35 % DateTime : Mon Sep 21 11:12:42 UTC 2026
% 0.09/5.35 % CPUTime :
% 0.09/5.36 % Drodi V4.1.1
% 0.09/5.38 % Refutation found
% 0.09/5.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/5.38 % SZS output start CNFRefutation for theBenchmark
% 0.09/5.38 fof(f2,negated_conjecture,(
% 0.09/5.38 (![X210]: (p9(X210,X210) ))),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f14,negated_conjecture,(
% 0.09/5.38 (![X129]: (p40(X129,X129) ))),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f34,negated_conjecture,(
% 0.09/5.38 (![X7]: (p12(X7,X7) ))),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f35,negated_conjecture,(
% 0.09/5.38 p59(f38(c72,c77),f35(c73,c68)) ),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f38,negated_conjecture,(
% 0.09/5.38 p56(f11(c65,f14(f17(c66,c67),c68)),c64) ),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f39,negated_conjecture,(
% 0.09/5.38 ~ p57(f26(f28(c71,f41(c78,c64)),c67),c77) ),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f74,negated_conjecture,(
% 0.09/5.38 (![X186,X187,X188]: (( p57(f26(f28(c71,X186),X187),X188)| ~ p57(f26(X186,X187),X188) ) ))),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f76,negated_conjecture,(
% 0.09/5.38 (![X175,X176,X178,X177]: (( p56(X175,X176)| ~ p40(X178,X176)| ~ p56(X177,X178)| ~ p4(X177,X175) ) ))),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f80,negated_conjecture,(
% 0.09/5.38 ~ p58(f31(f33(c75,c76),f23(c69,c77)),f19(f22(c70,c69),c68)) ),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f81,negated_conjecture,(
% 0.09/5.38 (![X3,X4,X5,X6]: (( p10(f14(X3,X4),f14(X5,X6))| ~ p12(X3,X5)| ~ p13(X4,X6) ) ))),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f87,negated_conjecture,(
% 0.09/5.38 (![X121,X122,X123,X124]: (( p4(f11(X121,X122),f11(X123,X124))| ~ p10(X122,X124)| ~ p9(X121,X123) ) ))),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f101,negated_conjecture,(
% 0.09/5.38 (![X181,X179,X180]: (( p57(f26(f41(c78,X181),X179),X180)| ~ p56(f11(c65,f14(f17(c66,X179),f23(c74,X180))),X181) ) ))),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f105,negated_conjecture,(
% 0.09/5.38 (![X17,X18]: (( p13(X17,f23(c74,X18))| p58(f31(f33(c75,c76),f23(c69,X18)),f19(f22(c70,c69),X17))| ~ p59(f38(c72,X18),f35(c73,X17)) ) ))),
% 0.09/5.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/5.38 fof(f107,plain,(
% 0.09/5.38 ![X0]: (p9(X0,X0))),
% 0.09/5.38 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/5.38 fof(f119,plain,(
% 0.09/5.38 ![X0]: (p40(X0,X0))),
% 0.09/5.38 inference(cnf_transformation,[status(thm)],[f14])).
% 0.09/5.38 fof(f139,plain,(
% 0.09/5.38 ![X0]: (p12(X0,X0))),
% 0.09/5.38 inference(cnf_transformation,[status(thm)],[f34])).
% 0.09/5.38 fof(f140,plain,(
% 0.09/5.38 p59(f38(c72,c77),f35(c73,c68))),
% 0.09/5.38 inference(cnf_transformation,[status(thm)],[f35])).
% 0.09/5.38 fof(f143,plain,(
% 0.09/5.38 p56(f11(c65,f14(f17(c66,c67),c68)),c64)),
% 0.09/5.38 inference(cnf_transformation,[status(thm)],[f38])).
% 0.09/5.38 fof(f144,plain,(
% 0.09/5.38 ~p57(f26(f28(c71,f41(c78,c64)),c67),c77)),
% 0.09/5.38 inference(cnf_transformation,[status(thm)],[f39])).
% 0.09/5.38 fof(f213,plain,(
% 0.09/5.38 ![X0,X1,X2]: (p57(f26(f28(c71,X0),X1),X2)|~p57(f26(X0,X1),X2))),
% 0.09/5.38 inference(cnf_transformation,[status(thm)],[f74])).
% 0.09/5.38 fof(f216,plain,(
% 0.09/5.38 ![X175,X177]: ((![X178]: ((![X176]: (p56(X175,X176)|~p40(X178,X176)))|~p56(X177,X178)))|~p4(X177,X175))),
% 0.09/5.38 inference(miniscoping,[status(thm)],[f76])).
% 0.09/5.38 fof(f217,plain,(
% 0.09/5.38 ![X0,X1,X2,X3]: (p56(X0,X1)|~p40(X2,X1)|~p56(X3,X2)|~p4(X3,X0))),
% 0.09/5.38 inference(cnf_transformation,[status(thm)],[f216])).
% 0.09/5.38 fof(f224,plain,(
% 0.09/5.38 ~p58(f31(f33(c75,c76),f23(c69,c77)),f19(f22(c70,c69),c68))),
% 0.09/5.38 inference(cnf_transformation,[status(thm)],[f80])).
% 0.09/5.38 fof(f225,plain,(
% 0.09/5.38 ![X4,X6]: ((![X3,X5]: (p10(f14(X3,X4),f14(X5,X6))|~p12(X3,X5)))|~p13(X4,X6))),
% 0.09/5.38 inference(miniscoping,[status(thm)],[f81])).
% 0.09/5.38 fof(f226,plain,(
% 0.09/5.38 ![X0,X1,X2,X3]: (p10(f14(X0,X1),f14(X2,X3))|~p12(X0,X2)|~p13(X1,X3))),
% 0.09/5.38 inference(cnf_transformation,[status(thm)],[f225])).
% 0.09/5.38 fof(f237,plain,(
% 0.09/5.38 ![X121,X123]: ((![X122,X124]: (p4(f11(X121,X122),f11(X123,X124))|~p10(X122,X124)))|~p9(X121,X123))),
% 0.09/5.38 inference(miniscoping,[status(thm)],[f87])).
% 0.09/5.38 fof(f238,plain,(
% 0.09/5.38 ![X0,X1,X2,X3]: (p4(f11(X0,X1),f11(X2,X3))|~p10(X1,X3)|~p9(X0,X2))),
% 0.09/5.38 inference(cnf_transformation,[status(thm)],[f237])).
% 0.09/5.38 fof(f265,plain,(
% 0.09/5.38 ![X0,X1,X2]: (p57(f26(f41(c78,X0),X1),X2)|~p56(f11(c65,f14(f17(c66,X1),f23(c74,X2))),X0))),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f101])).
% 0.09/5.39 fof(f269,plain,(
% 0.09/5.39 ![X0,X1]: (p13(X0,f23(c74,X1))|p58(f31(f33(c75,c76),f23(c69,X1)),f19(f22(c70,c69),X0))|~p59(f38(c72,X1),f35(c73,X0)))),
% 0.09/5.39 inference(cnf_transformation,[status(thm)],[f105])).
% 0.09/5.39 fof(f270,plain,(
% 0.09/5.39 ![X0,X1,X2,X3,X4]: (p57(f26(f41(c78,X0),X1),X2)|~p40(X3,X0)|~p56(X4,X3)|~p4(X4,f11(c65,f14(f17(c66,X1),f23(c74,X2)))))),
% 0.09/5.39 inference(resolution,[status(thm)],[f265,f217])).
% 0.09/5.39 fof(f272,plain,(
% 0.09/5.39 ![X0,X1,X2,X3]: (p57(f26(f41(c78,X0),X1),X2)|~p56(X3,X0)|~p4(X3,f11(c65,f14(f17(c66,X1),f23(c74,X2)))))),
% 0.09/5.39 inference(resolution,[status(thm)],[f270,f119])).
% 0.09/5.39 fof(f273,plain,(
% 0.09/5.39 ![X0,X1,X2,X3,X4]: (p57(f26(f41(c78,X0),X1),X2)|~p56(f11(X3,X4),X0)|~p10(X4,f14(f17(c66,X1),f23(c74,X2)))|~p9(X3,c65))),
% 0.09/5.39 inference(resolution,[status(thm)],[f272,f238])).
% 0.09/5.39 fof(f276,plain,(
% 0.09/5.39 p13(c68,f23(c74,c77))|p58(f31(f33(c75,c76),f23(c69,c77)),f19(f22(c70,c69),c68))),
% 0.09/5.39 inference(resolution,[status(thm)],[f269,f140])).
% 0.09/5.39 fof(f278,definition,(
% 0.09/5.39 sQ0_spl <=> (p13(c68,f23(c74,c77)))),
% 0.09/5.39 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.09/5.39 fof(f279,plain,(
% 0.09/5.39 p13(c68,f23(c74,c77))|~sQ0_spl),
% 0.09/5.39 inference(component_clause,[status(thm)],[f278])).
% 0.09/5.39 fof(f281,definition,(
% 0.09/5.39 sQ1_spl <=> (p58(f31(f33(c75,c76),f23(c69,c77)),f19(f22(c70,c69),c68)))),
% 0.09/5.39 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.09/5.39 fof(f282,plain,(
% 0.09/5.39 p58(f31(f33(c75,c76),f23(c69,c77)),f19(f22(c70,c69),c68))|~sQ1_spl),
% 0.09/5.39 inference(component_clause,[status(thm)],[f281])).
% 0.09/5.39 fof(f284,plain,(
% 0.09/5.39 sQ0_spl|sQ1_spl),
% 0.09/5.39 inference(split_clause,[status(thm)],[f276,f278,f281])).
% 0.09/5.39 fof(f292,plain,(
% 0.09/5.39 ![X0,X1,X2,X3]: (p57(f26(f41(c78,X0),X1),X2)|~p56(f11(c65,X3),X0)|~p10(X3,f14(f17(c66,X1),f23(c74,X2))))),
% 0.09/5.39 inference(resolution,[status(thm)],[f273,f107])).
% 0.09/5.39 fof(f293,plain,(
% 0.09/5.39 ![X0,X1]: (p57(f26(f41(c78,c64),X0),X1)|~p10(f14(f17(c66,c67),c68),f14(f17(c66,X0),f23(c74,X1))))),
% 0.09/5.39 inference(resolution,[status(thm)],[f292,f143])).
% 0.09/5.39 fof(f295,plain,(
% 0.09/5.39 ![X0,X1]: (p57(f26(f41(c78,c64),X0),X1)|~p12(f17(c66,c67),f17(c66,X0))|~p13(c68,f23(c74,X1)))),
% 0.09/5.39 inference(resolution,[status(thm)],[f293,f226])).
% 0.09/5.39 fof(f297,plain,(
% 0.09/5.39 ![X0]: (p57(f26(f41(c78,c64),X0),c77)|~p12(f17(c66,c67),f17(c66,X0))|~sQ0_spl)),
% 0.09/5.39 inference(resolution,[status(thm)],[f295,f279])).
% 0.09/5.39 fof(f301,plain,(
% 0.09/5.39 p57(f26(f41(c78,c64),c67),c77)|~sQ0_spl),
% 0.09/5.39 inference(resolution,[status(thm)],[f297,f139])).
% 0.09/5.39 fof(f310,plain,(
% 0.09/5.39 p57(f26(f28(c71,f41(c78,c64)),c67),c77)|~sQ0_spl),
% 0.09/5.39 inference(resolution,[status(thm)],[f301,f213])).
% 0.09/5.39 fof(f312,plain,(
% 0.09/5.39 $false|~sQ0_spl),
% 0.09/5.39 inference(forward_subsumption_resolution,[status(thm)],[f310,f144])).
% 0.09/5.39 fof(f313,plain,(
% 0.09/5.39 ~sQ0_spl),
% 0.09/5.39 inference(contradiction_clause,[status(thm)],[f312])).
% 0.09/5.39 fof(f314,plain,(
% 0.09/5.39 $false|~sQ1_spl),
% 0.09/5.39 inference(forward_subsumption_resolution,[status(thm)],[f282,f224])).
% 0.09/5.39 fof(f315,plain,(
% 0.09/5.39 ~sQ1_spl),
% 0.09/5.39 inference(contradiction_clause,[status(thm)],[f314])).
% 0.09/5.39 fof(f316,plain,(
% 0.09/5.39 $false),
% 0.09/5.39 inference(sat_refutation,[status(thm)],[f284,f313,f315])).
% 0.09/5.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.40 % Elapsed time: 0.041951 seconds
% 0.13/5.40 % CPU time: 0.125342 seconds
% 0.13/5.40 % Total memory used: 19.458 MB
% 0.13/5.40 % Net memory used: 19.391 MB
%------------------------------------------------------------------------------