%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN638-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 : n016.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:16 PM UTC 2026
% Result : Unsatisfiable 0.16s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN638-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n016.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 11:15:52 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 0.16/0.48 % Refutation found
% 0.16/0.48 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.16/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.48 fof(f4,negated_conjecture,(
% 0.16/0.48 (![X36]: (p4(X36,X36) ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f12,negated_conjecture,(
% 0.16/0.48 (![X39,X40]: (( p4(f16(X39),f16(X40))| ~ p4(X39,X40) ) ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f28,negated_conjecture,(
% 0.16/0.48 (![X20,X21,X22,X23]: (( p22(X20,X21)| ~ p4(X22,X20)| ~ p4(X23,X21)| ~ p22(X22,X23) ) ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f32,negated_conjecture,(
% 0.16/0.48 (![X41,X42,X43,X44]: (( p4(f17(X41,X42),f17(X43,X44))| ~ p4(X41,X43)| ~ p4(X42,X44) ) ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f39,negated_conjecture,(
% 0.16/0.48 (![X51]: (p4(f5(f8(f11(c25),f9(f10(c25),c28)),X51,c27),f5(f8(f11(c25),f9(f10(c25),c28)),X51,c29)) ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f40,negated_conjecture,(
% 0.16/0.48 p22(f16(f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c27))),f16(f17(c27,f5(c25,c26,c27)))) ),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f41,negated_conjecture,(
% 0.16/0.48 ~ p22(f16(f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c29))),f16(f17(c27,f5(c25,c26,c27)))) ),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f45,plain,(
% 0.16/0.48 ![X0]: (p4(X0,X0))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.48 fof(f53,plain,(
% 0.16/0.48 ![X0,X1]: (p4(f16(X0),f16(X1))|~p4(X0,X1))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f12])).
% 0.16/0.48 fof(f78,plain,(
% 0.16/0.48 ![X22,X23]: ((![X21]: ((![X20]: (p22(X20,X21)|~p4(X22,X20)))|~p4(X23,X21)))|~p22(X22,X23))),
% 0.16/0.48 inference(miniscoping,[status(thm)],[f28])).
% 0.16/0.48 fof(f79,plain,(
% 0.16/0.48 ![X0,X1,X2,X3]: (p22(X0,X1)|~p4(X2,X0)|~p4(X3,X1)|~p22(X2,X3))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f78])).
% 0.16/0.48 fof(f86,plain,(
% 0.16/0.48 ![X42,X44]: ((![X41,X43]: (p4(f17(X41,X42),f17(X43,X44))|~p4(X41,X43)))|~p4(X42,X44))),
% 0.16/0.48 inference(miniscoping,[status(thm)],[f32])).
% 0.16/0.48 fof(f87,plain,(
% 0.16/0.48 ![X0,X1,X2,X3]: (p4(f17(X0,X1),f17(X2,X3))|~p4(X0,X2)|~p4(X1,X3))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f86])).
% 0.16/0.48 fof(f95,plain,(
% 0.16/0.48 ![X0]: (p4(f5(f8(f11(c25),f9(f10(c25),c28)),X0,c27),f5(f8(f11(c25),f9(f10(c25),c28)),X0,c29)))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f39])).
% 0.16/0.48 fof(f96,plain,(
% 0.16/0.48 p22(f16(f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c27))),f16(f17(c27,f5(c25,c26,c27))))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f40])).
% 0.16/0.48 fof(f97,plain,(
% 0.16/0.48 ~p22(f16(f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c29))),f16(f17(c27,f5(c25,c26,c27))))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f41])).
% 0.16/0.48 fof(f116,definition,(
% 0.16/0.48 sQ1_spl <=> (p4(c27,c27))),
% 0.16/0.48 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.16/0.48 fof(f118,plain,(
% 0.16/0.48 ~p4(c27,c27)|sQ1_spl),
% 0.16/0.48 inference(component_clause,[status(thm)],[f116])).
% 0.16/0.48 fof(f125,plain,(
% 0.16/0.48 ![X0,X1]: (~p4(X0,f16(f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c29))))|~p4(X1,f16(f17(c27,f5(c25,c26,c27))))|~p22(X0,X1))),
% 0.16/0.48 inference(resolution,[status(thm)],[f97,f79])).
% 0.16/0.48 fof(f134,plain,(
% 0.16/0.48 ![X0,X1]: (~p4(X0,f16(f17(c27,f5(c25,c26,c27))))|~p22(f16(X1),X0)|~p4(X1,f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c29))))),
% 0.16/0.48 inference(resolution,[status(thm)],[f125,f53])).
% 0.16/0.48 fof(f151,plain,(
% 0.16/0.48 $false|sQ1_spl),
% 0.16/0.48 inference(forward_subsumption_resolution,[status(thm)],[f118,f45])).
% 0.16/0.48 fof(f152,plain,(
% 0.16/0.48 sQ1_spl),
% 0.16/0.48 inference(contradiction_clause,[status(thm)],[f151])).
% 0.16/0.48 fof(f159,plain,(
% 0.16/0.48 ~p4(f16(f17(c27,f5(c25,c26,c27))),f16(f17(c27,f5(c25,c26,c27))))|~p4(f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c27)),f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c29)))),
% 0.16/0.48 inference(resolution,[status(thm)],[f134,f96])).
% 0.16/0.48 fof(f161,definition,(
% 0.16/0.48 sQ4_spl <=> (p4(f16(f17(c27,f5(c25,c26,c27))),f16(f17(c27,f5(c25,c26,c27)))))),
% 0.16/0.48 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.16/0.48 fof(f163,plain,(
% 0.16/0.48 ~p4(f16(f17(c27,f5(c25,c26,c27))),f16(f17(c27,f5(c25,c26,c27))))|sQ4_spl),
% 0.16/0.48 inference(component_clause,[status(thm)],[f161])).
% 0.16/0.48 fof(f164,definition,(
% 0.16/0.48 sQ5_spl <=> (p4(f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c27)),f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c29))))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f166,plain,(
% 0.16/0.49 ~p4(f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c27)),f17(c27,f5(f8(f11(c25),f9(f10(c25),c28)),c26,c29)))|sQ5_spl),
% 0.16/0.49 inference(component_clause,[status(thm)],[f164])).
% 0.16/0.49 fof(f167,plain,(
% 0.16/0.49 ~sQ4_spl|~sQ5_spl),
% 0.16/0.49 inference(split_clause,[status(thm)],[f159,f161,f164])).
% 0.16/0.49 fof(f168,plain,(
% 0.16/0.49 $false|sQ4_spl),
% 0.16/0.49 inference(forward_subsumption_resolution,[status(thm)],[f163,f45])).
% 0.16/0.49 fof(f169,plain,(
% 0.16/0.49 sQ4_spl),
% 0.16/0.49 inference(contradiction_clause,[status(thm)],[f168])).
% 0.16/0.49 fof(f200,plain,(
% 0.16/0.49 ~p4(c27,c27)|~p4(f5(f8(f11(c25),f9(f10(c25),c28)),c26,c27),f5(f8(f11(c25),f9(f10(c25),c28)),c26,c29))|sQ5_spl),
% 0.16/0.49 inference(resolution,[status(thm)],[f166,f87])).
% 0.16/0.49 fof(f202,definition,(
% 0.16/0.49 sQ6_spl <=> (p4(f5(f8(f11(c25),f9(f10(c25),c28)),c26,c27),f5(f8(f11(c25),f9(f10(c25),c28)),c26,c29)))),
% 0.16/0.49 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.16/0.49 fof(f204,plain,(
% 0.16/0.49 ~p4(f5(f8(f11(c25),f9(f10(c25),c28)),c26,c27),f5(f8(f11(c25),f9(f10(c25),c28)),c26,c29))|sQ6_spl),
% 0.16/0.49 inference(component_clause,[status(thm)],[f202])).
% 0.16/0.49 fof(f205,plain,(
% 0.16/0.49 ~sQ1_spl|~sQ6_spl|sQ5_spl),
% 0.16/0.49 inference(split_clause,[status(thm)],[f200,f116,f202,f164])).
% 0.16/0.49 fof(f206,plain,(
% 0.16/0.49 $false|sQ6_spl),
% 0.16/0.49 inference(forward_subsumption_resolution,[status(thm)],[f204,f95])).
% 0.16/0.49 fof(f207,plain,(
% 0.16/0.49 sQ6_spl),
% 0.16/0.49 inference(contradiction_clause,[status(thm)],[f206])).
% 0.16/0.49 fof(f208,plain,(
% 0.16/0.49 $false),
% 0.16/0.49 inference(sat_refutation,[status(thm)],[f152,f167,f169,f205,f207])).
% 0.16/0.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.51 % Elapsed time: 0.055431 seconds
% 0.16/0.51 % CPU time: 0.198829 seconds
% 0.16/0.51 % Total memory used: 27.353 MB
% 0.16/0.51 % Net memory used: 27.175 MB
%------------------------------------------------------------------------------