%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN658-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 : n006.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:18 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN658-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.08/0.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 11:10:57 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.13/0.42 % Refutation found
% 0.13/0.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.42 fof(f4,negated_conjecture,(
% 0.13/0.42 (![X36]: (p4(X36,X36) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f11,negated_conjecture,(
% 0.13/0.42 ~ p6(c28,f10(c33)) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f15,negated_conjecture,(
% 0.13/0.42 (![X82,X83,X84]: (p6(f21(f8(X82,f9(X83,X84))),X83) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f25,negated_conjecture,(
% 0.13/0.42 (![X72,X73,X71]: (( p6(X72,X73)| ~ p6(X71,X72)| ~ p6(X71,X73) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f26,negated_conjecture,(
% 0.13/0.42 (![X37,X38,X36]: (( p4(X37,X38)| ~ p4(X36,X37)| ~ p4(X36,X38) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f44,negated_conjecture,(
% 0.13/0.42 ~ p4(f5(f8(c27,f9(c28,c29)),c36,c31),f5(f8(c27,f9(c28,c29)),c36,c34)) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f45,negated_conjecture,(
% 0.13/0.42 (![X20]: (( p24(f19(f20(c34,c31)),f19(f20(c34,X20)))| ~ p25(X20,f18(f8(c27,f9(c28,c29)))) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f48,negated_conjecture,(
% 0.13/0.42 (![X25,X26,X27]: (( p6(f21(X25),f10(c33))| p25(f22(X25,X26,X27),f18(X25))| p4(f5(X25,c36,X26),f5(X25,c36,X27)) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f49,negated_conjecture,(
% 0.13/0.42 (![X25,X26,X27]: (( p6(f21(X25),f10(c33))| p4(f5(X25,c36,X26),f5(X25,c36,X27))| ~ p24(f19(f20(X26,X27)),f19(f20(X26,f22(X25,X26,X27)))) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f54,plain,(
% 0.13/0.42 ![X0]: (p4(X0,X0))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.42 fof(f61,plain,(
% 0.13/0.42 ~p6(c28,f10(c33))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.42 fof(f65,plain,(
% 0.13/0.42 ![X0,X1,X2]: (p6(f21(f8(X0,f9(X1,X2))),X1))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.42 fof(f77,plain,(
% 0.13/0.42 ![X73,X71]: ((![X72]: (p6(X72,X73)|~p6(X71,X72)))|~p6(X71,X73))),
% 0.13/0.42 inference(miniscoping,[status(thm)],[f25])).
% 0.13/0.42 fof(f78,plain,(
% 0.13/0.42 ![X0,X1,X2]: (p6(X0,X1)|~p6(X2,X0)|~p6(X2,X1))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f77])).
% 0.13/0.42 fof(f79,plain,(
% 0.13/0.42 ![X38,X36]: ((![X37]: (p4(X37,X38)|~p4(X36,X37)))|~p4(X36,X38))),
% 0.13/0.42 inference(miniscoping,[status(thm)],[f26])).
% 0.13/0.42 fof(f80,plain,(
% 0.13/0.42 ![X0,X1,X2]: (p4(X0,X1)|~p4(X2,X0)|~p4(X2,X1))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f79])).
% 0.13/0.42 fof(f110,plain,(
% 0.13/0.42 ~p4(f5(f8(c27,f9(c28,c29)),c36,c31),f5(f8(c27,f9(c28,c29)),c36,c34))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.42 fof(f111,plain,(
% 0.13/0.42 ![X0]: (p24(f19(f20(c34,c31)),f19(f20(c34,X0)))|~p25(X0,f18(f8(c27,f9(c28,c29)))))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f45])).
% 0.13/0.42 fof(f116,plain,(
% 0.13/0.42 ![X0,X1,X2]: (p6(f21(X0),f10(c33))|p25(f22(X0,X1,X2),f18(X0))|p4(f5(X0,c36,X1),f5(X0,c36,X2)))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f48])).
% 0.13/0.42 fof(f117,plain,(
% 0.13/0.42 ![X0,X1,X2]: (p6(f21(X0),f10(c33))|p4(f5(X0,c36,X1),f5(X0,c36,X2))|~p24(f19(f20(X1,X2)),f19(f20(X1,f22(X0,X1,X2)))))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f49])).
% 0.13/0.42 fof(f119,plain,(
% 0.13/0.42 ![X0]: (~p6(X0,c28)|~p6(X0,f10(c33)))),
% 0.13/0.42 inference(resolution,[status(thm)],[f78,f61])).
% 0.13/0.42 fof(f120,plain,(
% 0.13/0.42 ![X0,X1]: (~p6(f21(f8(X0,f9(c28,X1))),f10(c33)))),
% 0.13/0.42 inference(resolution,[status(thm)],[f119,f65])).
% 0.13/0.42 fof(f142,plain,(
% 0.13/0.42 ![X0]: (~p4(X0,f5(f8(c27,f9(c28,c29)),c36,c31))|~p4(X0,f5(f8(c27,f9(c28,c29)),c36,c34)))),
% 0.13/0.42 inference(resolution,[status(thm)],[f110,f80])).
% 0.13/0.42 fof(f239,definition,(
% 0.13/0.42 sQ6_spl <=> (p6(f21(f8(c27,f9(c28,c29))),f10(c33)))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f240,plain,(
% 0.13/0.42 p6(f21(f8(c27,f9(c28,c29))),f10(c33))|~sQ6_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f239])).
% 0.13/0.42 fof(f246,plain,(
% 0.13/0.42 $false|~sQ6_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f240,f120])).
% 0.13/0.42 fof(f247,plain,(
% 0.13/0.42 ~sQ6_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f246])).
% 0.13/0.42 fof(f266,plain,(
% 0.13/0.42 ![X0]: (~p4(f5(f8(c27,f9(c28,c29)),c36,X0),f5(f8(c27,f9(c28,c29)),c36,c34))|p6(f21(f8(c27,f9(c28,c29))),f10(c33))|p25(f22(f8(c27,f9(c28,c29)),X0,c31),f18(f8(c27,f9(c28,c29)))))),
% 0.13/0.42 inference(resolution,[status(thm)],[f142,f116])).
% 0.13/0.42 fof(f267,plain,(
% 0.13/0.42 ![X0]: (~p4(f5(f8(c27,f9(c28,c29)),c36,X0),f5(f8(c27,f9(c28,c29)),c36,c34))|p6(f21(f8(c27,f9(c28,c29))),f10(c33))|~p24(f19(f20(X0,c31)),f19(f20(X0,f22(f8(c27,f9(c28,c29)),X0,c31)))))),
% 0.13/0.42 inference(resolution,[status(thm)],[f142,f117])).
% 0.13/0.42 fof(f271,definition,(
% 0.13/0.42 ![X0]: (sQ9_spl <=> (~p4(f5(f8(c27,f9(c28,c29)),c36,X0),f5(f8(c27,f9(c28,c29)),c36,c34))|p25(f22(f8(c27,f9(c28,c29)),X0,c31),f18(f8(c27,f9(c28,c29))))))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f272,plain,(
% 0.13/0.42 ![X0]: (~p4(f5(f8(c27,f9(c28,c29)),c36,X0),f5(f8(c27,f9(c28,c29)),c36,c34))|p25(f22(f8(c27,f9(c28,c29)),X0,c31),f18(f8(c27,f9(c28,c29))))|~sQ9_spl)),
% 0.13/0.42 inference(component_clause,[status(thm)],[f271])).
% 0.13/0.42 fof(f274,plain,(
% 0.13/0.42 sQ9_spl|sQ6_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f266,f271,f239])).
% 0.13/0.42 fof(f275,definition,(
% 0.13/0.42 ![X0]: (sQ10_spl <=> (~p4(f5(f8(c27,f9(c28,c29)),c36,X0),f5(f8(c27,f9(c28,c29)),c36,c34))|~p24(f19(f20(X0,c31)),f19(f20(X0,f22(f8(c27,f9(c28,c29)),X0,c31))))))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f276,plain,(
% 0.13/0.42 ![X0]: (~p4(f5(f8(c27,f9(c28,c29)),c36,X0),f5(f8(c27,f9(c28,c29)),c36,c34))|~p24(f19(f20(X0,c31)),f19(f20(X0,f22(f8(c27,f9(c28,c29)),X0,c31))))|~sQ10_spl)),
% 0.13/0.42 inference(component_clause,[status(thm)],[f275])).
% 0.13/0.42 fof(f278,plain,(
% 0.13/0.42 sQ10_spl|sQ6_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f267,f275,f239])).
% 0.13/0.42 fof(f511,plain,(
% 0.13/0.42 p25(f22(f8(c27,f9(c28,c29)),c34,c31),f18(f8(c27,f9(c28,c29))))|~sQ9_spl),
% 0.13/0.42 inference(resolution,[status(thm)],[f272,f54])).
% 0.13/0.42 fof(f556,plain,(
% 0.13/0.42 ~p4(f5(f8(c27,f9(c28,c29)),c36,c34),f5(f8(c27,f9(c28,c29)),c36,c34))|~p25(f22(f8(c27,f9(c28,c29)),c34,c31),f18(f8(c27,f9(c28,c29))))|~sQ10_spl),
% 0.13/0.42 inference(resolution,[status(thm)],[f276,f111])).
% 0.13/0.42 fof(f558,definition,(
% 0.13/0.42 sQ17_spl <=> (p4(f5(f8(c27,f9(c28,c29)),c36,c34),f5(f8(c27,f9(c28,c29)),c36,c34)))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f560,plain,(
% 0.13/0.42 ~p4(f5(f8(c27,f9(c28,c29)),c36,c34),f5(f8(c27,f9(c28,c29)),c36,c34))|sQ17_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f558])).
% 0.13/0.42 fof(f561,definition,(
% 0.13/0.42 sQ18_spl <=> (p25(f22(f8(c27,f9(c28,c29)),c34,c31),f18(f8(c27,f9(c28,c29)))))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f563,plain,(
% 0.13/0.42 ~p25(f22(f8(c27,f9(c28,c29)),c34,c31),f18(f8(c27,f9(c28,c29))))|sQ18_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f561])).
% 0.13/0.42 fof(f564,plain,(
% 0.13/0.42 ~sQ17_spl|~sQ18_spl|~sQ10_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f556,f558,f561,f275])).
% 0.13/0.42 fof(f565,plain,(
% 0.13/0.42 $false|sQ17_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f560,f54])).
% 0.13/0.42 fof(f566,plain,(
% 0.13/0.42 sQ17_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f565])).
% 0.13/0.42 fof(f567,plain,(
% 0.13/0.42 $false|~sQ9_spl|sQ18_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f563,f511])).
% 0.13/0.42 fof(f568,plain,(
% 0.13/0.42 ~sQ9_spl|sQ18_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f567])).
% 0.13/0.42 fof(f569,plain,(
% 0.13/0.42 $false),
% 0.13/0.42 inference(sat_refutation,[status(thm)],[f247,f274,f278,f564,f566,f568])).
% 0.13/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.45 % Elapsed time: 0.077029 seconds
% 0.13/0.45 % CPU time: 0.295387 seconds
% 0.13/0.45 % Total memory used: 21.452 MB
% 0.13/0.45 % Net memory used: 21.284 MB
%------------------------------------------------------------------------------