%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN673-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 : n003.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:20 PM UTC 2026
% Result : Unsatisfiable 9.48s 1.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN673-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n003.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:13:31 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 9.48/1.65 % Refutation found
% 9.48/1.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.48/1.65 % SZS output start CNFRefutation for theBenchmark
% 9.48/1.65 fof(f1,negated_conjecture,(
% 9.48/1.65 (![X0]: (p10(X0,X0) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f5,negated_conjecture,(
% 9.48/1.65 (![X81]: (p4(X81,X81) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f12,negated_conjecture,(
% 9.48/1.65 (![X29]: (p16(X29,X29) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f17,negated_conjecture,(
% 9.48/1.65 ~ p29(f5(c33,f8(c34,c30)),c38) ),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f18,negated_conjecture,(
% 9.48/1.65 (![X60,X59]: (( p29(X60,X59)| ~ p27(f12(c32,X59),X60) ) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f19,negated_conjecture,(
% 9.48/1.65 (![X59,X60]: (( p27(f12(c32,X59),X60)| ~ p29(X60,X59) ) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f20,negated_conjecture,(
% 9.48/1.65 (![X68]: (( p28(f21(c30,X68),c31)| ~ p16(X68,c40) ) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f22,negated_conjecture,(
% 9.48/1.65 (![X1,X2,X0]: (( p10(X1,X2)| ~ p10(X0,X1)| ~ p10(X0,X2) ) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f37,negated_conjecture,(
% 9.48/1.65 (![X68]: (( p28(f21(c30,X68),c31)| ~ p29(f24(c42,X68),c39) ) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f38,negated_conjecture,(
% 9.48/1.65 (![X69,X70,X72,X71]: (( p29(X69,X70)| ~ p29(X72,X71)| ~ p4(X72,X69)| ~ p10(X71,X70) ) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f41,negated_conjecture,(
% 9.48/1.65 p10(c38,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))) ),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f52,negated_conjecture,(
% 9.48/1.65 (![X73]: (( p29(f24(c42,f26(c43,X73)),c39)| p29(f5(c33,f8(c34,c30)),X73)| ~ p10(X73,f14(f19(c35,c37),c39)) ) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f53,negated_conjecture,(
% 9.48/1.65 (![X73]: (( p29(f5(c33,f8(c34,c30)),X73)| ~ p10(X73,f14(f19(c35,c37),c39))| ~ p28(f21(c30,f26(c43,X73)),c31) ) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f55,negated_conjecture,(
% 9.48/1.65 (![X61,X62]: (( p27(f12(c32,f14(f19(c35,X61),f17(c36,X62))),f5(c33,f8(c34,c30)))| ~ p28(f21(c30,X62),c31)| ~ p27(f12(c32,X61),f5(c33,f8(c34,c30))) ) ))),
% 9.48/1.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.48/1.65 fof(f56,plain,(
% 9.48/1.65 ![X0]: (p10(X0,X0))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f1])).
% 9.48/1.65 fof(f60,plain,(
% 9.48/1.65 ![X0]: (p4(X0,X0))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f5])).
% 9.48/1.65 fof(f67,plain,(
% 9.48/1.65 ![X0]: (p16(X0,X0))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f12])).
% 9.48/1.65 fof(f72,plain,(
% 9.48/1.65 ~p29(f5(c33,f8(c34,c30)),c38)),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f17])).
% 9.48/1.65 fof(f73,plain,(
% 9.48/1.65 ![X0,X1]: (p29(X0,X1)|~p27(f12(c32,X1),X0))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f18])).
% 9.48/1.65 fof(f74,plain,(
% 9.48/1.65 ![X0,X1]: (p27(f12(c32,X0),X1)|~p29(X1,X0))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f19])).
% 9.48/1.65 fof(f75,plain,(
% 9.48/1.65 ![X0]: (p28(f21(c30,X0),c31)|~p16(X0,c40))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f20])).
% 9.48/1.65 fof(f77,plain,(
% 9.48/1.65 ![X2,X0]: ((![X1]: (p10(X1,X2)|~p10(X0,X1)))|~p10(X0,X2))),
% 9.48/1.65 inference(miniscoping,[status(thm)],[f22])).
% 9.48/1.65 fof(f78,plain,(
% 9.48/1.65 ![X0,X1,X2]: (p10(X0,X1)|~p10(X2,X0)|~p10(X2,X1))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f77])).
% 9.48/1.65 fof(f107,plain,(
% 9.48/1.65 ![X0]: (p28(f21(c30,X0),c31)|~p29(f24(c42,X0),c39))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f37])).
% 9.48/1.65 fof(f108,plain,(
% 9.48/1.65 ![X70,X71]: ((![X69,X72]: ((p29(X69,X70)|~p29(X72,X71))|~p4(X72,X69)))|~p10(X71,X70))),
% 9.48/1.65 inference(miniscoping,[status(thm)],[f38])).
% 9.48/1.65 fof(f109,plain,(
% 9.48/1.65 ![X0,X1,X2,X3]: (p29(X0,X1)|~p29(X2,X3)|~p4(X2,X0)|~p10(X3,X1))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f108])).
% 9.48/1.65 fof(f114,plain,(
% 9.48/1.65 p10(c38,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f41])).
% 9.48/1.65 fof(f135,plain,(
% 9.48/1.65 ![X0]: (p29(f24(c42,f26(c43,X0)),c39)|p29(f5(c33,f8(c34,c30)),X0)|~p10(X0,f14(f19(c35,c37),c39)))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f52])).
% 9.48/1.65 fof(f136,plain,(
% 9.48/1.65 ![X0]: (p29(f5(c33,f8(c34,c30)),X0)|~p10(X0,f14(f19(c35,c37),c39))|~p28(f21(c30,f26(c43,X0)),c31))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f53])).
% 9.48/1.65 fof(f138,plain,(
% 9.48/1.65 ![X61]: ((![X62]: (p27(f12(c32,f14(f19(c35,X61),f17(c36,X62))),f5(c33,f8(c34,c30)))|~p28(f21(c30,X62),c31)))|~p27(f12(c32,X61),f5(c33,f8(c34,c30))))),
% 9.48/1.65 inference(miniscoping,[status(thm)],[f55])).
% 9.48/1.65 fof(f139,plain,(
% 9.48/1.65 ![X0,X1]: (p27(f12(c32,f14(f19(c35,X0),f17(c36,X1))),f5(c33,f8(c34,c30)))|~p28(f21(c30,X1),c31)|~p27(f12(c32,X0),f5(c33,f8(c34,c30))))),
% 9.48/1.65 inference(cnf_transformation,[status(thm)],[f138])).
% 9.48/1.65 fof(f141,plain,(
% 9.48/1.65 p29(f24(c42,f26(c43,f14(f19(c35,c37),c39))),c39)|p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39))),
% 9.48/1.65 inference(resolution,[status(thm)],[f135,f56])).
% 9.48/1.65 fof(f149,definition,(
% 9.48/1.65 sQ2_spl <=> (p29(f24(c42,f26(c43,f14(f19(c35,c37),c39))),c39))),
% 9.48/1.65 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 9.48/1.65 fof(f150,plain,(
% 9.48/1.65 p29(f24(c42,f26(c43,f14(f19(c35,c37),c39))),c39)|~sQ2_spl),
% 9.48/1.65 inference(component_clause,[status(thm)],[f149])).
% 9.48/1.65 fof(f152,definition,(
% 9.48/1.65 sQ3_spl <=> (p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39)))),
% 9.48/1.65 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 9.48/1.65 fof(f153,plain,(
% 9.48/1.65 p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39))|~sQ3_spl),
% 9.48/1.65 inference(component_clause,[status(thm)],[f152])).
% 9.48/1.65 fof(f155,plain,(
% 9.48/1.65 sQ2_spl|sQ3_spl),
% 9.48/1.65 inference(split_clause,[status(thm)],[f141,f149,f152])).
% 9.48/1.65 fof(f157,plain,(
% 9.48/1.65 ![X0,X1]: (p10(X0,X1)|~p10(X1,X0))),
% 9.48/1.65 inference(resolution,[status(thm)],[f78,f56])).
% 9.48/1.65 fof(f164,plain,(
% 9.48/1.65 p28(f21(c30,c40),c31)),
% 9.48/1.65 inference(resolution,[status(thm)],[f75,f67])).
% 9.48/1.65 fof(f192,plain,(
% 9.48/1.65 p10(f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)),c38)),
% 9.48/1.65 inference(resolution,[status(thm)],[f114,f157])).
% 9.48/1.65 fof(f245,plain,(
% 9.48/1.65 p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39))|~p28(f21(c30,f26(c43,f14(f19(c35,c37),c39))),c31)),
% 9.48/1.65 inference(resolution,[status(thm)],[f136,f56])).
% 9.48/1.65 fof(f250,definition,(
% 9.48/1.65 sQ5_spl <=> (p28(f21(c30,f26(c43,f14(f19(c35,c37),c39))),c31))),
% 9.48/1.65 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 9.48/1.65 fof(f252,plain,(
% 9.48/1.65 ~p28(f21(c30,f26(c43,f14(f19(c35,c37),c39))),c31)|sQ5_spl),
% 9.48/1.65 inference(component_clause,[status(thm)],[f250])).
% 9.48/1.65 fof(f253,plain,(
% 9.48/1.65 sQ3_spl|~sQ5_spl),
% 9.48/1.65 inference(split_clause,[status(thm)],[f245,f152,f250])).
% 9.48/1.65 fof(f392,plain,(
% 9.48/1.65 p27(f12(c32,f14(f19(c35,c37),c39)),f5(c33,f8(c34,c30)))|~sQ3_spl),
% 9.48/1.65 inference(resolution,[status(thm)],[f153,f74])).
% 9.48/1.65 fof(f462,plain,(
% 9.48/1.65 ![X0,X1]: (p29(X0,c38)|~p29(X1,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)))|~p4(X1,X0))),
% 9.48/1.65 inference(resolution,[status(thm)],[f192,f109])).
% 9.48/1.65 fof(f627,plain,(
% 9.48/1.65 ![X0]: (p27(f12(c32,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,X0))),f5(c33,f8(c34,c30)))|~p28(f21(c30,X0),c31)|~sQ3_spl)),
% 9.48/1.65 inference(resolution,[status(thm)],[f392,f139])).
% 9.48/1.65 fof(f1449,plain,(
% 9.48/1.65 p27(f12(c32,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),f5(c33,f8(c34,c30)))|~sQ3_spl),
% 9.48/1.65 inference(resolution,[status(thm)],[f627,f164])).
% 9.48/1.65 fof(f6455,plain,(
% 9.48/1.65 p29(f5(c33,f8(c34,c30)),f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)))|~sQ3_spl),
% 9.48/1.65 inference(resolution,[status(thm)],[f1449,f73])).
% 9.48/1.65 fof(f10753,plain,(
% 9.48/1.65 ![X0]: (p29(X0,c38)|~p4(f5(c33,f8(c34,c30)),X0)|~sQ3_spl)),
% 9.48/1.65 inference(resolution,[status(thm)],[f6455,f462])).
% 9.48/1.65 fof(f10840,plain,(
% 9.48/1.65 p29(f5(c33,f8(c34,c30)),c38)|~sQ3_spl),
% 9.48/1.65 inference(resolution,[status(thm)],[f10753,f60])).
% 9.48/1.65 fof(f10841,plain,(
% 9.48/1.65 $false|~sQ3_spl),
% 9.48/1.65 inference(forward_subsumption_resolution,[status(thm)],[f10840,f72])).
% 9.48/1.65 fof(f10842,plain,(
% 9.48/1.65 ~sQ3_spl),
% 9.48/1.65 inference(contradiction_clause,[status(thm)],[f10841])).
% 9.48/1.65 fof(f10843,plain,(
% 9.48/1.65 p28(f21(c30,f26(c43,f14(f19(c35,c37),c39))),c31)|~sQ2_spl),
% 9.48/1.65 inference(resolution,[status(thm)],[f150,f107])).
% 9.48/1.65 fof(f10850,plain,(
% 9.48/1.65 $false|sQ5_spl|~sQ2_spl),
% 9.48/1.65 inference(forward_subsumption_resolution,[status(thm)],[f10843,f252])).
% 9.48/1.65 fof(f10851,plain,(
% 9.48/1.65 sQ5_spl|~sQ2_spl),
% 9.48/1.65 inference(contradiction_clause,[status(thm)],[f10850])).
% 9.48/1.65 fof(f10852,plain,(
% 9.48/1.65 $false),
% 9.48/1.65 inference(sat_refutation,[status(thm)],[f155,f253,f10842,f10851])).
% 9.48/1.67 % SZS output end CNFRefutation for theBenchmark.p
% 9.48/1.69 % Elapsed time: 1.317121 seconds
% 9.48/1.69 % CPU time: 10.135323 seconds
% 9.48/1.69 % Total memory used: 182.266 MB
% 9.48/1.69 % Net memory used: 152.329 MB
%------------------------------------------------------------------------------