%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN690-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 : n005.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:21 PM UTC 2026
% Result : Unsatisfiable 1.28s 0.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN690-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.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 11:12:04 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 1.28/0.70 % Refutation found
% 1.28/0.70 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.28/0.70 % SZS output start CNFRefutation for theBenchmark
% 1.28/0.70 fof(f5,negated_conjecture,(
% 1.28/0.70 (![X106]: (p4(X106,X106) ))),
% 1.28/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.28/0.70 fof(f19,negated_conjecture,(
% 1.28/0.70 p34(c36,c37) ),
% 1.28/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.28/0.70 fof(f20,negated_conjecture,(
% 1.28/0.70 ~ p2(c38,c40) ),
% 1.28/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.28/0.70 fof(f21,negated_conjecture,(
% 1.28/0.70 (![X114]: (p4(f5(c40,X114),f5(f7(c39,c40),X114)) ))),
% 1.28/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.28/0.70 fof(f22,negated_conjecture,(
% 1.28/0.70 (![X113]: (p4(f5(c38,X113),f5(f7(c39,c38),X113)) ))),
% 1.28/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.28/0.70 fof(f27,negated_conjecture,(
% 1.28/0.70 (![X107,X108,X106]: (( p4(X107,X108)| ~ p4(X106,X107)| ~ p4(X106,X108) ) ))),
% 1.28/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.28/0.70 fof(f57,negated_conjecture,(
% 1.28/0.70 (![X103,X105,X104]: (( p4(f5(f7(c39,X103),X105),f5(f7(c39,X104),X105))| p35(f10(c37,f12(f14(f16(c41,X103),X104),X105)),X105) ) ))),
% 1.28/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.28/0.70 fof(f58,negated_conjecture,(
% 1.28/0.70 (![X103,X105,X104]: (( p4(f5(f7(c39,X103),X105),f5(f7(c39,X104),X105))| ~ p4(f5(X103,f12(f14(f16(c41,X103),X104),X105)),f5(X104,f12(f14(f16(c41,X103),X104),X105))) ) ))),
% 1.28/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.28/0.70 fof(f61,negated_conjecture,(
% 1.28/0.70 (![X31,X32,X33,X34,X35]: (( p2(X31,X32)| p4(f5(f26(f28(c43,X33),X34),X35),f5(f26(f28(c44,X33),X34),X35))| ~ p34(c36,X33)| ~ p35(f10(X33,X35),f30(f32(c42,X33),X34))| ~ p4(f5(X31,f18(f20(f22(f24(c45,X33),X34),X31),X32)),f5(f7(X34,X31),f18(f20(f22(f24(c45,X33),X34),X31),X32)))| ~ p4(f5(X32,f18(f20(f22(f24(c45,X33),X34),X31),X32)),f5(f7(X34,X32),f18(f20(f22(f24(c45,X33),X34),X31),X32))) ) ))),
% 1.28/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.28/0.70 fof(f62,negated_conjecture,(
% 1.28/0.70 (![X31,X32,X33,X34]: (( p2(X31,X32)| ~ p34(c36,X33)| ~ p4(f5(X31,f18(f20(f22(f24(c45,X33),X34),X31),X32)),f5(f7(X34,X31),f18(f20(f22(f24(c45,X33),X34),X31),X32)))| ~ p4(f5(X32,f18(f20(f22(f24(c45,X33),X34),X31),X32)),f5(f7(X34,X32),f18(f20(f22(f24(c45,X33),X34),X31),X32)))| ~ p4(f5(f7(X34,f26(f28(c43,X33),X34)),f30(f32(c42,X33),X34)),f5(f7(X34,f26(f28(c44,X33),X34)),f30(f32(c42,X33),X34))) ) ))),
% 1.28/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.28/0.70 fof(f67,plain,(
% 1.28/0.70 ![X0]: (p4(X0,X0))),
% 1.28/0.70 inference(cnf_transformation,[status(thm)],[f5])).
% 1.28/0.70 fof(f81,plain,(
% 1.28/0.70 p34(c36,c37)),
% 1.28/0.70 inference(cnf_transformation,[status(thm)],[f19])).
% 1.28/0.70 fof(f82,plain,(
% 1.28/0.70 ~p2(c38,c40)),
% 1.28/0.70 inference(cnf_transformation,[status(thm)],[f20])).
% 1.28/0.70 fof(f83,plain,(
% 1.28/0.70 ![X0]: (p4(f5(c40,X0),f5(f7(c39,c40),X0)))),
% 1.28/0.70 inference(cnf_transformation,[status(thm)],[f21])).
% 1.28/0.70 fof(f84,plain,(
% 1.28/0.70 ![X0]: (p4(f5(c38,X0),f5(f7(c39,c38),X0)))),
% 1.28/0.70 inference(cnf_transformation,[status(thm)],[f22])).
% 1.28/0.70 fof(f93,plain,(
% 1.28/0.70 ![X108,X106]: ((![X107]: (p4(X107,X108)|~p4(X106,X107)))|~p4(X106,X108))),
% 1.28/0.70 inference(miniscoping,[status(thm)],[f27])).
% 1.28/0.70 fof(f94,plain,(
% 1.28/0.70 ![X0,X1,X2]: (p4(X0,X1)|~p4(X2,X0)|~p4(X2,X1))),
% 1.28/0.70 inference(cnf_transformation,[status(thm)],[f93])).
% 1.28/0.70 fof(f153,plain,(
% 1.28/0.70 ![X0,X1,X2]: (p4(f5(f7(c39,X0),X1),f5(f7(c39,X2),X1))|p35(f10(c37,f12(f14(f16(c41,X0),X2),X1)),X1))),
% 1.28/0.70 inference(cnf_transformation,[status(thm)],[f57])).
% 1.28/0.70 fof(f154,plain,(
% 1.28/0.70 ![X0,X1,X2]: (p4(f5(f7(c39,X0),X1),f5(f7(c39,X2),X1))|~p4(f5(X0,f12(f14(f16(c41,X0),X2),X1)),f5(X2,f12(f14(f16(c41,X0),X2),X1))))),
% 1.28/0.70 inference(cnf_transformation,[status(thm)],[f58])).
% 1.28/0.70 fof(f159,plain,(
% 1.28/0.70 ![X31,X32,X33,X34]: (((![X35]: (((p2(X31,X32)|p4(f5(f26(f28(c43,X33),X34),X35),f5(f26(f28(c44,X33),X34),X35)))|~p34(c36,X33))|~p35(f10(X33,X35),f30(f32(c42,X33),X34))))|~p4(f5(X31,f18(f20(f22(f24(c45,X33),X34),X31),X32)),f5(f7(X34,X31),f18(f20(f22(f24(c45,X33),X34),X31),X32))))|~p4(f5(X32,f18(f20(f22(f24(c45,X33),X34),X31),X32)),f5(f7(X34,X32),f18(f20(f22(f24(c45,X33),X34),X31),X32))))),
% 1.28/0.70 inference(miniscoping,[status(thm)],[f61])).
% 1.28/0.70 fof(f160,plain,(
% 1.28/0.70 ![X0,X1,X2,X3,X4]: (p2(X0,X1)|p4(f5(f26(f28(c43,X2),X3),X4),f5(f26(f28(c44,X2),X3),X4))|~p34(c36,X2)|~p35(f10(X2,X4),f30(f32(c42,X2),X3))|~p4(f5(X0,f18(f20(f22(f24(c45,X2),X3),X0),X1)),f5(f7(X3,X0),f18(f20(f22(f24(c45,X2),X3),X0),X1)))|~p4(f5(X1,f18(f20(f22(f24(c45,X2),X3),X0),X1)),f5(f7(X3,X1),f18(f20(f22(f24(c45,X2),X3),X0),X1))))),
% 1.28/0.71 inference(cnf_transformation,[status(thm)],[f159])).
% 1.28/0.71 fof(f161,plain,(
% 1.28/0.71 ![X33,X34]: ((![X31,X32]: (((p2(X31,X32)|~p34(c36,X33))|~p4(f5(X31,f18(f20(f22(f24(c45,X33),X34),X31),X32)),f5(f7(X34,X31),f18(f20(f22(f24(c45,X33),X34),X31),X32))))|~p4(f5(X32,f18(f20(f22(f24(c45,X33),X34),X31),X32)),f5(f7(X34,X32),f18(f20(f22(f24(c45,X33),X34),X31),X32)))))|~p4(f5(f7(X34,f26(f28(c43,X33),X34)),f30(f32(c42,X33),X34)),f5(f7(X34,f26(f28(c44,X33),X34)),f30(f32(c42,X33),X34))))),
% 1.28/0.71 inference(miniscoping,[status(thm)],[f62])).
% 1.28/0.71 fof(f162,plain,(
% 1.28/0.71 ![X0,X1,X2,X3]: (p2(X0,X1)|~p34(c36,X2)|~p4(f5(X0,f18(f20(f22(f24(c45,X2),X3),X0),X1)),f5(f7(X3,X0),f18(f20(f22(f24(c45,X2),X3),X0),X1)))|~p4(f5(X1,f18(f20(f22(f24(c45,X2),X3),X0),X1)),f5(f7(X3,X1),f18(f20(f22(f24(c45,X2),X3),X0),X1)))|~p4(f5(f7(X3,f26(f28(c43,X2),X3)),f30(f32(c42,X2),X3)),f5(f7(X3,f26(f28(c44,X2),X3)),f30(f32(c42,X2),X3))))),
% 1.28/0.71 inference(cnf_transformation,[status(thm)],[f161])).
% 1.28/0.71 fof(f178,plain,(
% 1.28/0.71 ![X0,X1,X2,X3]: (p4(f5(f7(c39,X0),X1),f5(f7(c39,X2),X1))|~p4(X3,f5(X0,f12(f14(f16(c41,X0),X2),X1)))|~p4(X3,f5(X2,f12(f14(f16(c41,X0),X2),X1))))),
% 1.28/0.71 inference(resolution,[status(thm)],[f154,f94])).
% 1.28/0.71 fof(f196,plain,(
% 1.28/0.71 ![X0,X1,X2,X3]: (~p4(X0,f5(f26(f28(c43,X1),c39),f12(f14(f16(c41,f26(f28(c43,X1),c39)),f26(f28(c44,X1),c39)),f30(f32(c42,X1),c39))))|~p4(X0,f5(f26(f28(c44,X1),c39),f12(f14(f16(c41,f26(f28(c43,X1),c39)),f26(f28(c44,X1),c39)),f30(f32(c42,X1),c39))))|p2(X2,X3)|~p34(c36,X1)|~p4(f5(X2,f18(f20(f22(f24(c45,X1),c39),X2),X3)),f5(f7(c39,X2),f18(f20(f22(f24(c45,X1),c39),X2),X3)))|~p4(f5(X3,f18(f20(f22(f24(c45,X1),c39),X2),X3)),f5(f7(c39,X3),f18(f20(f22(f24(c45,X1),c39),X2),X3))))),
% 1.28/0.71 inference(resolution,[status(thm)],[f178,f162])).
% 1.28/0.71 fof(f203,plain,(
% 1.28/0.71 ![X0,X1,X2]: (p35(f10(c37,f12(f14(f16(c41,f26(f28(c43,X0),c39)),f26(f28(c44,X0),c39)),f30(f32(c42,X0),c39))),f30(f32(c42,X0),c39))|p2(X1,X2)|~p34(c36,X0)|~p4(f5(X1,f18(f20(f22(f24(c45,X0),c39),X1),X2)),f5(f7(c39,X1),f18(f20(f22(f24(c45,X0),c39),X1),X2)))|~p4(f5(X2,f18(f20(f22(f24(c45,X0),c39),X1),X2)),f5(f7(c39,X2),f18(f20(f22(f24(c45,X0),c39),X1),X2))))),
% 1.28/0.71 inference(resolution,[status(thm)],[f153,f162])).
% 1.28/0.71 fof(f214,plain,(
% 1.28/0.71 ![X0,X1,X2]: (~p4(X0,f5(f26(f28(c43,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))))|~p4(X0,f5(f26(f28(c44,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))))|p2(X1,X2)|~p4(f5(X1,f18(f20(f22(f24(c45,c37),c39),X1),X2)),f5(f7(c39,X1),f18(f20(f22(f24(c45,c37),c39),X1),X2)))|~p4(f5(X2,f18(f20(f22(f24(c45,c37),c39),X1),X2)),f5(f7(c39,X2),f18(f20(f22(f24(c45,c37),c39),X1),X2))))),
% 1.28/0.71 inference(resolution,[status(thm)],[f196,f81])).
% 1.28/0.71 fof(f216,definition,(
% 1.28/0.71 ![X0]: (sQ0_spl <=> (~p4(X0,f5(f26(f28(c43,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))))|~p4(X0,f5(f26(f28(c44,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))))))),
% 1.28/0.71 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.28/0.71 fof(f217,plain,(
% 1.28/0.71 ![X0]: (~p4(X0,f5(f26(f28(c43,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))))|~p4(X0,f5(f26(f28(c44,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))))|~sQ0_spl)),
% 1.28/0.71 inference(component_clause,[status(thm)],[f216])).
% 1.28/0.71 fof(f219,definition,(
% 1.28/0.71 ![X1,X2]: (sQ1_spl <=> (p2(X1,X2)|~p4(f5(X1,f18(f20(f22(f24(c45,c37),c39),X1),X2)),f5(f7(c39,X1),f18(f20(f22(f24(c45,c37),c39),X1),X2)))|~p4(f5(X2,f18(f20(f22(f24(c45,c37),c39),X1),X2)),f5(f7(c39,X2),f18(f20(f22(f24(c45,c37),c39),X1),X2)))))),
% 1.28/0.71 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.28/0.71 fof(f220,plain,(
% 1.28/0.71 ![X0,X1]: (p2(X0,X1)|~p4(f5(X0,f18(f20(f22(f24(c45,c37),c39),X0),X1)),f5(f7(c39,X0),f18(f20(f22(f24(c45,c37),c39),X0),X1)))|~p4(f5(X1,f18(f20(f22(f24(c45,c37),c39),X0),X1)),f5(f7(c39,X1),f18(f20(f22(f24(c45,c37),c39),X0),X1)))|~sQ1_spl)),
% 1.28/0.72 inference(component_clause,[status(thm)],[f219])).
% 1.28/0.72 fof(f222,plain,(
% 1.28/0.72 sQ0_spl|sQ1_spl),
% 1.28/0.72 inference(split_clause,[status(thm)],[f214,f216,f219])).
% 1.28/0.72 fof(f263,plain,(
% 1.28/0.72 ![X0,X1,X2,X3]: (p2(X0,X1)|~p34(c36,c37)|~p4(f5(X0,f18(f20(f22(f24(c45,c37),c39),X0),X1)),f5(f7(c39,X0),f18(f20(f22(f24(c45,c37),c39),X0),X1)))|~p4(f5(X1,f18(f20(f22(f24(c45,c37),c39),X0),X1)),f5(f7(c39,X1),f18(f20(f22(f24(c45,c37),c39),X0),X1)))|p2(X2,X3)|p4(f5(f26(f28(c43,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))),f5(f26(f28(c44,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))))|~p34(c36,c37)|~p4(f5(X2,f18(f20(f22(f24(c45,c37),c39),X2),X3)),f5(f7(c39,X2),f18(f20(f22(f24(c45,c37),c39),X2),X3)))|~p4(f5(X3,f18(f20(f22(f24(c45,c37),c39),X2),X3)),f5(f7(c39,X3),f18(f20(f22(f24(c45,c37),c39),X2),X3))))),
% 1.28/0.72 inference(resolution,[status(thm)],[f203,f160])).
% 1.28/0.72 fof(f265,definition,(
% 1.28/0.72 sQ5_spl <=> (p34(c36,c37))),
% 1.28/0.72 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 1.28/0.72 fof(f267,plain,(
% 1.28/0.72 ~p34(c36,c37)|sQ5_spl),
% 1.28/0.72 inference(component_clause,[status(thm)],[f265])).
% 1.28/0.72 fof(f268,definition,(
% 1.28/0.72 sQ6_spl <=> (p4(f5(f26(f28(c43,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))),f5(f26(f28(c44,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39)))))),
% 1.28/0.72 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 1.28/0.72 fof(f269,plain,(
% 1.28/0.72 p4(f5(f26(f28(c43,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))),f5(f26(f28(c44,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))))|~sQ6_spl),
% 1.28/0.72 inference(component_clause,[status(thm)],[f268])).
% 1.28/0.72 fof(f271,plain,(
% 1.28/0.72 sQ1_spl|~sQ5_spl|sQ6_spl),
% 1.28/0.72 inference(split_clause,[status(thm)],[f263,f219,f265,f268])).
% 1.28/0.72 fof(f333,plain,(
% 1.28/0.72 ![X0]: (p2(X0,c40)|~p4(f5(X0,f18(f20(f22(f24(c45,c37),c39),X0),c40)),f5(f7(c39,X0),f18(f20(f22(f24(c45,c37),c39),X0),c40)))|~sQ1_spl)),
% 1.28/0.72 inference(resolution,[status(thm)],[f220,f83])).
% 1.28/0.72 fof(f518,plain,(
% 1.28/0.72 p2(c38,c40)|~sQ1_spl),
% 1.28/0.72 inference(resolution,[status(thm)],[f333,f84])).
% 1.28/0.72 fof(f522,plain,(
% 1.28/0.72 $false|~sQ1_spl),
% 1.28/0.72 inference(forward_subsumption_resolution,[status(thm)],[f518,f82])).
% 1.28/0.72 fof(f523,plain,(
% 1.28/0.72 ~sQ1_spl),
% 1.28/0.72 inference(contradiction_clause,[status(thm)],[f522])).
% 1.28/0.72 fof(f524,plain,(
% 1.28/0.72 $false|sQ5_spl),
% 1.28/0.72 inference(forward_subsumption_resolution,[status(thm)],[f267,f81])).
% 1.28/0.72 fof(f525,plain,(
% 1.28/0.72 sQ5_spl),
% 1.28/0.72 inference(contradiction_clause,[status(thm)],[f524])).
% 1.28/0.72 fof(f631,plain,(
% 1.28/0.72 ~p4(f5(f26(f28(c43,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))),f5(f26(f28(c44,c37),c39),f12(f14(f16(c41,f26(f28(c43,c37),c39)),f26(f28(c44,c37),c39)),f30(f32(c42,c37),c39))))|~sQ0_spl),
% 1.28/0.72 inference(resolution,[status(thm)],[f217,f67])).
% 1.28/0.72 fof(f632,plain,(
% 1.28/0.72 $false|~sQ6_spl|~sQ0_spl),
% 1.28/0.72 inference(forward_subsumption_resolution,[status(thm)],[f631,f269])).
% 1.28/0.72 fof(f633,plain,(
% 1.28/0.72 ~sQ6_spl|~sQ0_spl),
% 1.28/0.72 inference(contradiction_clause,[status(thm)],[f632])).
% 1.28/0.72 fof(f634,plain,(
% 1.28/0.72 $false),
% 1.28/0.72 inference(sat_refutation,[status(thm)],[f222,f271,f523,f525,f633])).
% 1.28/0.72 % SZS output end CNFRefutation for theBenchmark.p
% 1.28/0.72 % Elapsed time: 0.351882 seconds
% 1.28/0.72 % CPU time: 2.519980 seconds
% 1.28/0.72 % Total memory used: 55.685 MB
% 1.28/0.72 % Net memory used: 52.049 MB
%------------------------------------------------------------------------------