%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN657-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 : n014.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.12s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN657-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.35 % Computer : n014.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:11:04 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 0.12/0.39 % Refutation found
% 0.12/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.39 fof(f11,negated_conjecture,(
% 0.12/0.39 ~ p6(c28,f10(c33)) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f15,negated_conjecture,(
% 0.12/0.39 (![X82,X83,X84]: (p6(f21(f8(X82,f9(X83,X84))),X83) ))),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f25,negated_conjecture,(
% 0.12/0.39 (![X72,X73,X71]: (( p6(X72,X73)| ~ p6(X71,X72)| ~ p6(X71,X73) ) ))),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f44,negated_conjecture,(
% 0.12/0.39 ~ p4(f5(f8(c27,f9(c28,c29)),c36,c31),f5(f8(c27,f9(c28,c29)),c36,c34)) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f45,negated_conjecture,(
% 0.12/0.39 (![X20]: (( p24(f19(f20(c31,c34)),f19(f20(c31,X20)))| ~ p25(X20,f18(f8(c27,f9(c28,c29)))) ) ))),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f48,negated_conjecture,(
% 0.12/0.39 (![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.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f49,negated_conjecture,(
% 0.12/0.39 (![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.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f61,plain,(
% 0.12/0.39 ~p6(c28,f10(c33))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f11])).
% 0.12/0.39 fof(f65,plain,(
% 0.12/0.39 ![X0,X1,X2]: (p6(f21(f8(X0,f9(X1,X2))),X1))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f15])).
% 0.12/0.39 fof(f77,plain,(
% 0.12/0.39 ![X73,X71]: ((![X72]: (p6(X72,X73)|~p6(X71,X72)))|~p6(X71,X73))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f25])).
% 0.12/0.39 fof(f78,plain,(
% 0.12/0.39 ![X0,X1,X2]: (p6(X0,X1)|~p6(X2,X0)|~p6(X2,X1))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f77])).
% 0.12/0.39 fof(f110,plain,(
% 0.12/0.39 ~p4(f5(f8(c27,f9(c28,c29)),c36,c31),f5(f8(c27,f9(c28,c29)),c36,c34))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f44])).
% 0.12/0.39 fof(f111,plain,(
% 0.12/0.39 ![X0]: (p24(f19(f20(c31,c34)),f19(f20(c31,X0)))|~p25(X0,f18(f8(c27,f9(c28,c29)))))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f45])).
% 0.12/0.39 fof(f116,plain,(
% 0.12/0.39 ![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.12/0.39 inference(cnf_transformation,[status(thm)],[f48])).
% 0.12/0.39 fof(f117,plain,(
% 0.12/0.39 ![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.12/0.39 inference(cnf_transformation,[status(thm)],[f49])).
% 0.12/0.39 fof(f119,plain,(
% 0.12/0.39 ![X0]: (~p6(X0,c28)|~p6(X0,f10(c33)))),
% 0.12/0.39 inference(resolution,[status(thm)],[f78,f61])).
% 0.12/0.39 fof(f120,plain,(
% 0.12/0.39 ![X0,X1]: (~p6(f21(f8(X0,f9(c28,X1))),f10(c33)))),
% 0.12/0.39 inference(resolution,[status(thm)],[f119,f65])).
% 0.12/0.39 fof(f156,plain,(
% 0.12/0.39 p6(f21(f8(c27,f9(c28,c29))),f10(c33))|p25(f22(f8(c27,f9(c28,c29)),c31,c34),f18(f8(c27,f9(c28,c29))))),
% 0.12/0.39 inference(resolution,[status(thm)],[f116,f110])).
% 0.12/0.39 fof(f157,definition,(
% 0.12/0.39 sQ3_spl <=> (p6(f21(f8(c27,f9(c28,c29))),f10(c33)))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f158,plain,(
% 0.12/0.39 p6(f21(f8(c27,f9(c28,c29))),f10(c33))|~sQ3_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f157])).
% 0.12/0.39 fof(f160,definition,(
% 0.12/0.39 sQ4_spl <=> (p25(f22(f8(c27,f9(c28,c29)),c31,c34),f18(f8(c27,f9(c28,c29)))))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f161,plain,(
% 0.12/0.39 p25(f22(f8(c27,f9(c28,c29)),c31,c34),f18(f8(c27,f9(c28,c29))))|~sQ4_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f160])).
% 0.12/0.39 fof(f163,plain,(
% 0.12/0.39 sQ3_spl|sQ4_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f156,f157,f160])).
% 0.12/0.39 fof(f164,plain,(
% 0.12/0.39 $false|~sQ3_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f158,f120])).
% 0.12/0.39 fof(f165,plain,(
% 0.12/0.39 ~sQ3_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f164])).
% 0.12/0.39 fof(f166,plain,(
% 0.12/0.39 p6(f21(f8(c27,f9(c28,c29))),f10(c33))|~p24(f19(f20(c31,c34)),f19(f20(c31,f22(f8(c27,f9(c28,c29)),c31,c34))))),
% 0.12/0.39 inference(resolution,[status(thm)],[f117,f110])).
% 0.12/0.39 fof(f167,definition,(
% 0.12/0.39 sQ5_spl <=> (p24(f19(f20(c31,c34)),f19(f20(c31,f22(f8(c27,f9(c28,c29)),c31,c34)))))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f169,plain,(
% 0.12/0.39 ~p24(f19(f20(c31,c34)),f19(f20(c31,f22(f8(c27,f9(c28,c29)),c31,c34))))|sQ5_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f167])).
% 0.12/0.39 fof(f170,plain,(
% 0.12/0.39 sQ3_spl|~sQ5_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f166,f157,f167])).
% 0.12/0.39 fof(f195,plain,(
% 0.12/0.39 ~p25(f22(f8(c27,f9(c28,c29)),c31,c34),f18(f8(c27,f9(c28,c29))))|sQ5_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f169,f111])).
% 0.12/0.39 fof(f197,plain,(
% 0.12/0.39 $false|~sQ4_spl|sQ5_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f195,f161])).
% 0.12/0.39 fof(f198,plain,(
% 0.12/0.39 ~sQ4_spl|sQ5_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f197])).
% 0.12/0.39 fof(f199,plain,(
% 0.12/0.39 $false),
% 0.12/0.39 inference(sat_refutation,[status(thm)],[f163,f165,f170,f198])).
% 0.12/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.41 % Elapsed time: 0.054263 seconds
% 0.12/0.41 % CPU time: 0.148675 seconds
% 0.12/0.41 % Total memory used: 19.702 MB
% 0.12/0.41 % Net memory used: 19.505 MB
%------------------------------------------------------------------------------