%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN650-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:17 PM UTC 2026
% Result : Unsatisfiable 102.33s 18.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN650-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n004.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 11:11:26 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 102.33/18.32 % Refutation found
% 102.33/18.32 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 102.33/18.32 % SZS output start CNFRefutation for theBenchmark
% 102.33/18.32 fof(f2,negated_conjecture,(
% 102.33/18.32 (![X54]: (p8(X54,X54) ))),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f8,negated_conjecture,(
% 102.33/18.32 p22(f3(f4(f5(c26))),c27) ),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f10,negated_conjecture,(
% 102.33/18.32 p24(c33,f20(f11(c29,f12(c27,c30)))) ),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f18,negated_conjecture,(
% 102.33/18.32 (![X55,X56,X54]: (( p8(X55,X56)| ~ p8(X54,X55)| ~ p8(X54,X56) ) ))),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f24,negated_conjecture,(
% 102.33/18.32 ~ p8(c33,f9(f11(c29,f12(c27,c30)),c31,c32)) ),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f25,negated_conjecture,(
% 102.33/18.32 (![X40,X41,X42,X43]: (( p25(X40,X41)| ~ p8(X42,X40)| ~ p8(X43,X41)| ~ p25(X42,X43) ) ))),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f34,negated_conjecture,(
% 102.33/18.32 ~ p23(f18(f11(c29,f12(c27,c30)),f9(f11(c29,f12(c27,c30)),c31,c32))) ),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f35,negated_conjecture,(
% 102.33/18.32 p8(f16(f17(c32,c33)),f13(f15(f11(c29,f12(c27,c30)),c32),f14(f3(f4(f5(c26)))))) ),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f38,negated_conjecture,(
% 102.33/18.32 p8(f16(f17(c32,f9(f11(c29,f12(c27,c30)),c31,c32))),f13(f15(f11(c29,f12(c27,c30)),c32),f14(f3(f4(f5(c26)))))) ),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f40,negated_conjecture,(
% 102.33/18.32 (![X34,X31,X32,X33,X35]: (( p25(f16(f17(X34,f9(f11(X31,f12(X32,X33)),c31,X34))),f16(f17(X34,X35)))| ~ p22(f3(f4(f5(c26))),X32)| ~ p24(X35,f20(f11(X31,f12(X32,X33)))) ) ))),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f44,negated_conjecture,(
% 102.33/18.32 (![X35,X31,X32,X33,X34]: (( p8(X35,f9(f11(X31,f12(X32,X33)),c31,X34))| p24(f21(X31,X32,X33,X34,X35),f20(f11(X31,f12(X32,X33))))| p23(f18(f11(X31,f12(X32,X33)),f9(f11(X31,f12(X32,X33)),c31,X34)))| ~ p22(f3(f4(f5(c26))),X32)| ~ p24(X35,f20(f11(X31,f12(X32,X33)))) ) ))),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f45,negated_conjecture,(
% 102.33/18.32 (![X35,X31,X32,X33,X34]: (( p8(X35,f9(f11(X31,f12(X32,X33)),c31,X34))| p23(f18(f11(X31,f12(X32,X33)),f9(f11(X31,f12(X32,X33)),c31,X34)))| ~ p22(f3(f4(f5(c26))),X32)| ~ p24(X35,f20(f11(X31,f12(X32,X33))))| ~ p25(f16(f17(X34,X35)),f16(f17(X34,f21(X31,X32,X33,X34,X35)))) ) ))),
% 102.33/18.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 102.33/18.32 fof(f47,plain,(
% 102.33/18.32 ![X0]: (p8(X0,X0))),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f2])).
% 102.33/18.32 fof(f53,plain,(
% 102.33/18.32 p22(f3(f4(f5(c26))),c27)),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f8])).
% 102.33/18.32 fof(f55,plain,(
% 102.33/18.32 p24(c33,f20(f11(c29,f12(c27,c30))))),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f10])).
% 102.33/18.32 fof(f64,plain,(
% 102.33/18.32 ![X56,X54]: ((![X55]: (p8(X55,X56)|~p8(X54,X55)))|~p8(X54,X56))),
% 102.33/18.32 inference(miniscoping,[status(thm)],[f18])).
% 102.33/18.32 fof(f65,plain,(
% 102.33/18.32 ![X0,X1,X2]: (p8(X0,X1)|~p8(X2,X0)|~p8(X2,X1))),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f64])).
% 102.33/18.32 fof(f75,plain,(
% 102.33/18.32 ~p8(c33,f9(f11(c29,f12(c27,c30)),c31,c32))),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f24])).
% 102.33/18.32 fof(f76,plain,(
% 102.33/18.32 ![X42,X43]: ((![X41]: ((![X40]: (p25(X40,X41)|~p8(X42,X40)))|~p8(X43,X41)))|~p25(X42,X43))),
% 102.33/18.32 inference(miniscoping,[status(thm)],[f25])).
% 102.33/18.32 fof(f77,plain,(
% 102.33/18.32 ![X0,X1,X2,X3]: (p25(X0,X1)|~p8(X2,X0)|~p8(X3,X1)|~p25(X2,X3))),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f76])).
% 102.33/18.32 fof(f94,plain,(
% 102.33/18.32 ~p23(f18(f11(c29,f12(c27,c30)),f9(f11(c29,f12(c27,c30)),c31,c32)))),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f34])).
% 102.33/18.32 fof(f95,plain,(
% 102.33/18.32 p8(f16(f17(c32,c33)),f13(f15(f11(c29,f12(c27,c30)),c32),f14(f3(f4(f5(c26))))))),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f35])).
% 102.33/18.32 fof(f100,plain,(
% 102.33/18.32 p8(f16(f17(c32,f9(f11(c29,f12(c27,c30)),c31,c32))),f13(f15(f11(c29,f12(c27,c30)),c32),f14(f3(f4(f5(c26))))))),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f38])).
% 102.33/18.32 fof(f103,plain,(
% 102.33/18.32 ![X31,X32,X33,X35]: (((![X34]: p25(f16(f17(X34,f9(f11(X31,f12(X32,X33)),c31,X34))),f16(f17(X34,X35))))|~p22(f3(f4(f5(c26))),X32))|~p24(X35,f20(f11(X31,f12(X32,X33)))))),
% 102.33/18.32 inference(miniscoping,[status(thm)],[f40])).
% 102.33/18.32 fof(f104,plain,(
% 102.33/18.32 ![X0,X1,X2,X3,X4]: (p25(f16(f17(X0,f9(f11(X1,f12(X2,X3)),c31,X0))),f16(f17(X0,X4)))|~p22(f3(f4(f5(c26))),X2)|~p24(X4,f20(f11(X1,f12(X2,X3)))))),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f103])).
% 102.33/18.32 fof(f110,plain,(
% 102.33/18.32 ![X35,X31,X32,X33]: (((![X34]: ((p8(X35,f9(f11(X31,f12(X32,X33)),c31,X34))|p24(f21(X31,X32,X33,X34,X35),f20(f11(X31,f12(X32,X33)))))|p23(f18(f11(X31,f12(X32,X33)),f9(f11(X31,f12(X32,X33)),c31,X34)))))|~p22(f3(f4(f5(c26))),X32))|~p24(X35,f20(f11(X31,f12(X32,X33)))))),
% 102.33/18.32 inference(miniscoping,[status(thm)],[f44])).
% 102.33/18.32 fof(f111,plain,(
% 102.33/18.32 ![X0,X1,X2,X3,X4]: (p8(X0,f9(f11(X1,f12(X2,X3)),c31,X4))|p24(f21(X1,X2,X3,X4,X0),f20(f11(X1,f12(X2,X3))))|p23(f18(f11(X1,f12(X2,X3)),f9(f11(X1,f12(X2,X3)),c31,X4)))|~p22(f3(f4(f5(c26))),X2)|~p24(X0,f20(f11(X1,f12(X2,X3)))))),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f110])).
% 102.33/18.32 fof(f112,plain,(
% 102.33/18.32 ![X0,X1,X2,X3,X4]: (p8(X0,f9(f11(X1,f12(X2,X3)),c31,X4))|p23(f18(f11(X1,f12(X2,X3)),f9(f11(X1,f12(X2,X3)),c31,X4)))|~p22(f3(f4(f5(c26))),X2)|~p24(X0,f20(f11(X1,f12(X2,X3))))|~p25(f16(f17(X4,X0)),f16(f17(X4,f21(X1,X2,X3,X4,X0)))))),
% 102.33/18.32 inference(cnf_transformation,[status(thm)],[f45])).
% 102.33/18.32 fof(f175,plain,(
% 102.33/18.32 ![X0,X1,X2,X3,X4,X5,X6]: (~p22(f3(f4(f5(c26))),X0)|~p24(X1,f20(f11(X2,f12(X0,X3))))|p25(X4,X5)|~p8(f16(f17(X6,f9(f11(X2,f12(X0,X3)),c31,X6))),X4)|~p8(f16(f17(X6,X1)),X5))),
% 102.33/18.32 inference(resolution,[status(thm)],[f104,f77])).
% 102.33/18.32 fof(f199,plain,(
% 102.33/18.32 ![X0,X1,X2,X3]: (p8(X0,f9(f11(X1,f12(c27,X2)),c31,X3))|p24(f21(X1,c27,X2,X3,X0),f20(f11(X1,f12(c27,X2))))|p23(f18(f11(X1,f12(c27,X2)),f9(f11(X1,f12(c27,X2)),c31,X3)))|~p24(X0,f20(f11(X1,f12(c27,X2)))))),
% 102.33/18.32 inference(resolution,[status(thm)],[f111,f53])).
% 102.33/18.32 fof(f201,plain,(
% 102.33/18.32 ![X0,X1,X2,X3]: (p8(X0,f9(f11(X1,f12(c27,X2)),c31,X3))|p23(f18(f11(X1,f12(c27,X2)),f9(f11(X1,f12(c27,X2)),c31,X3)))|~p24(X0,f20(f11(X1,f12(c27,X2))))|~p25(f16(f17(X3,X0)),f16(f17(X3,f21(X1,c27,X2,X3,X0)))))),
% 102.33/18.32 inference(resolution,[status(thm)],[f112,f53])).
% 102.33/18.32 fof(f204,plain,(
% 102.33/18.32 ![X0]: (p8(c33,f9(f11(c29,f12(c27,c30)),c31,X0))|p24(f21(c29,c27,c30,X0,c33),f20(f11(c29,f12(c27,c30))))|p23(f18(f11(c29,f12(c27,c30)),f9(f11(c29,f12(c27,c30)),c31,X0))))),
% 102.33/18.32 inference(resolution,[status(thm)],[f199,f55])).
% 102.33/18.32 fof(f253,plain,(
% 102.33/18.32 ![X0]: (p8(c33,f9(f11(c29,f12(c27,c30)),c31,X0))|p23(f18(f11(c29,f12(c27,c30)),f9(f11(c29,f12(c27,c30)),c31,X0)))|~p25(f16(f17(X0,c33)),f16(f17(X0,f21(c29,c27,c30,X0,c33)))))),
% 102.33/18.32 inference(resolution,[status(thm)],[f201,f55])).
% 102.33/18.32 fof(f269,plain,(
% 102.33/18.32 p8(c33,f9(f11(c29,f12(c27,c30)),c31,c32))|p24(f21(c29,c27,c30,c32,c33),f20(f11(c29,f12(c27,c30))))),
% 102.33/18.32 inference(resolution,[status(thm)],[f204,f94])).
% 102.33/18.32 fof(f273,definition,(
% 102.33/18.32 sQ8_spl <=> (p8(c33,f9(f11(c29,f12(c27,c30)),c31,c32)))),
% 102.33/18.32 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 102.33/18.32 fof(f274,plain,(
% 102.33/18.32 p8(c33,f9(f11(c29,f12(c27,c30)),c31,c32))|~sQ8_spl),
% 102.33/18.32 inference(component_clause,[status(thm)],[f273])).
% 102.33/18.32 fof(f276,definition,(
% 102.33/18.32 sQ9_spl <=> (p24(f21(c29,c27,c30,c32,c33),f20(f11(c29,f12(c27,c30)))))),
% 102.33/18.32 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 102.33/18.32 fof(f277,plain,(
% 102.33/18.32 p24(f21(c29,c27,c30,c32,c33),f20(f11(c29,f12(c27,c30))))|~sQ9_spl),
% 102.33/18.32 inference(component_clause,[status(thm)],[f276])).
% 102.33/18.32 fof(f279,plain,(
% 102.33/18.32 sQ8_spl|sQ9_spl),
% 102.33/18.32 inference(split_clause,[status(thm)],[f269,f273,f276])).
% 102.33/18.32 fof(f288,plain,(
% 102.33/18.32 $false|~sQ8_spl),
% 102.33/18.32 inference(forward_subsumption_resolution,[status(thm)],[f274,f75])).
% 102.33/18.32 fof(f289,plain,(
% 102.33/18.32 ~sQ8_spl),
% 102.33/18.32 inference(contradiction_clause,[status(thm)],[f288])).
% 102.33/18.32 fof(f337,plain,(
% 102.33/18.32 p8(c33,f9(f11(c29,f12(c27,c30)),c31,c32))|~p25(f16(f17(c32,c33)),f16(f17(c32,f21(c29,c27,c30,c32,c33))))),
% 102.33/18.32 inference(resolution,[status(thm)],[f253,f94])).
% 102.33/18.32 fof(f341,definition,(
% 102.33/18.32 sQ13_spl <=> (p25(f16(f17(c32,c33)),f16(f17(c32,f21(c29,c27,c30,c32,c33)))))),
% 102.33/18.32 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 102.33/18.32 fof(f343,plain,(
% 102.33/18.32 ~p25(f16(f17(c32,c33)),f16(f17(c32,f21(c29,c27,c30,c32,c33))))|sQ13_spl),
% 102.33/18.33 inference(component_clause,[status(thm)],[f341])).
% 102.33/18.33 fof(f344,plain,(
% 102.33/18.33 sQ8_spl|~sQ13_spl),
% 102.33/18.33 inference(split_clause,[status(thm)],[f337,f273,f341])).
% 102.33/18.33 fof(f366,plain,(
% 102.33/18.33 ![X0,X1,X2,X3,X4]: (~p22(f3(f4(f5(c26))),X0)|~p24(X1,f20(f11(X2,f12(X0,X3))))|~p8(f16(f17(X4,f9(f11(X2,f12(X0,X3)),c31,X4))),f16(f17(c32,c33)))|~p8(f16(f17(X4,X1)),f16(f17(c32,f21(c29,c27,c30,c32,c33))))|sQ13_spl)),
% 102.33/18.33 inference(resolution,[status(thm)],[f343,f175])).
% 102.33/18.33 fof(f368,plain,(
% 102.33/18.33 ![X0,X1,X2,X3,X4,X5]: (~p22(f3(f4(f5(c26))),X0)|~p24(X1,f20(f11(X2,f12(X0,X3))))|~p8(f16(f17(X4,X1)),f16(f17(c32,f21(c29,c27,c30,c32,c33))))|~p8(X5,f16(f17(X4,f9(f11(X2,f12(X0,X3)),c31,X4))))|~p8(X5,f16(f17(c32,c33)))|sQ13_spl)),
% 102.33/18.33 inference(resolution,[status(thm)],[f366,f65])).
% 102.33/18.33 fof(f396,definition,(
% 102.33/18.33 sQ16_spl <=> (p8(c32,c32))),
% 102.33/18.33 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 102.33/18.33 fof(f398,plain,(
% 102.33/18.33 ~p8(c32,c32)|sQ16_spl),
% 102.33/18.33 inference(component_clause,[status(thm)],[f396])).
% 102.33/18.33 fof(f1095,plain,(
% 102.33/18.33 $false|sQ16_spl),
% 102.33/18.33 inference(forward_subsumption_resolution,[status(thm)],[f398,f47])).
% 102.33/18.33 fof(f1096,plain,(
% 102.33/18.33 sQ16_spl),
% 102.33/18.33 inference(contradiction_clause,[status(thm)],[f1095])).
% 102.33/18.33 fof(f1705,plain,(
% 102.33/18.33 ![X0,X1,X2,X3,X4]: (~p24(X0,f20(f11(X1,f12(c27,X2))))|~p8(f16(f17(X3,X0)),f16(f17(c32,f21(c29,c27,c30,c32,c33))))|~p8(X4,f16(f17(X3,f9(f11(X1,f12(c27,X2)),c31,X3))))|~p8(X4,f16(f17(c32,c33)))|sQ13_spl)),
% 102.33/18.33 inference(resolution,[status(thm)],[f368,f53])).
% 102.33/18.33 fof(f2078,plain,(
% 102.33/18.33 ![X0,X1,X2]: (~p24(f21(c29,c27,c30,c32,c33),f20(f11(X0,f12(c27,X1))))|~p8(X2,f16(f17(c32,f9(f11(X0,f12(c27,X1)),c31,c32))))|~p8(X2,f16(f17(c32,c33)))|sQ13_spl)),
% 102.33/18.33 inference(resolution,[status(thm)],[f1705,f47])).
% 102.33/18.33 fof(f2079,plain,(
% 102.33/18.33 ![X0]: (~p8(X0,f16(f17(c32,f9(f11(c29,f12(c27,c30)),c31,c32))))|~p8(X0,f16(f17(c32,c33)))|sQ13_spl|~sQ9_spl)),
% 102.33/18.33 inference(resolution,[status(thm)],[f2078,f277])).
% 102.33/18.33 fof(f2082,plain,(
% 102.33/18.33 ![X0,X1]: (~p8(X0,f16(f17(c32,f9(f11(c29,f12(c27,c30)),c31,c32))))|~p8(X1,X0)|~p8(X1,f16(f17(c32,c33)))|sQ13_spl|~sQ9_spl)),
% 102.33/18.33 inference(resolution,[status(thm)],[f2079,f65])).
% 102.33/18.33 fof(f2098,plain,(
% 102.33/18.33 ![X0]: (~p8(X0,f16(f17(c32,f9(f11(c29,f12(c27,c30)),c31,c32))))|~p8(f16(f17(c32,c33)),X0)|sQ13_spl|~sQ9_spl)),
% 102.33/18.33 inference(resolution,[status(thm)],[f2082,f47])).
% 102.33/18.33 fof(f2100,plain,(
% 102.33/18.33 ![X0,X1]: (~p8(f16(f17(c32,c33)),X0)|~p8(X1,X0)|~p8(X1,f16(f17(c32,f9(f11(c29,f12(c27,c30)),c31,c32))))|sQ13_spl|~sQ9_spl)),
% 102.33/18.33 inference(resolution,[status(thm)],[f2098,f65])).
% 102.33/18.33 fof(f2169,plain,(
% 102.33/18.33 ![X0]: (~p8(f16(f17(c32,c33)),X0)|~p8(f16(f17(c32,f9(f11(c29,f12(c27,c30)),c31,c32))),X0)|sQ13_spl|~sQ9_spl)),
% 102.33/18.33 inference(resolution,[status(thm)],[f2100,f47])).
% 102.33/18.33 fof(f2170,plain,(
% 102.33/18.33 ~p8(f16(f17(c32,f9(f11(c29,f12(c27,c30)),c31,c32))),f13(f15(f11(c29,f12(c27,c30)),c32),f14(f3(f4(f5(c26))))))|sQ13_spl|~sQ9_spl),
% 102.33/18.33 inference(resolution,[status(thm)],[f2169,f95])).
% 102.33/18.33 fof(f2174,plain,(
% 102.33/18.33 $false|sQ13_spl|~sQ9_spl),
% 102.33/18.33 inference(forward_subsumption_resolution,[status(thm)],[f2170,f100])).
% 102.33/18.33 fof(f2175,plain,(
% 102.33/18.33 sQ13_spl|~sQ9_spl),
% 102.33/18.33 inference(contradiction_clause,[status(thm)],[f2174])).
% 102.33/18.33 fof(f2176,plain,(
% 102.33/18.33 $false),
% 102.33/18.33 inference(sat_refutation,[status(thm)],[f279,f289,f344,f1096,f2175])).
% 102.33/18.33 % SZS output end CNFRefutation for theBenchmark.p
% 6.73/18.55 % Elapsed time: 13.164388 seconds
% 6.73/18.55 % CPU time: 103.264540 seconds
% 6.73/18.55 % Total memory used: 433.509 MB
% 6.73/18.55 % Net memory used: 357.537 MB
%------------------------------------------------------------------------------