%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN598-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 : n007.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:12 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN598-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.37 % Computer : n007.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 11:07:20 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.40 % Refutation found
% 0.09/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.40 fof(f2,negated_conjecture,(
% 0.09/0.40 p18(c21) ),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f3,negated_conjecture,(
% 0.09/0.40 (![X34]: (p7(X34,X34) ))),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f7,negated_conjecture,(
% 0.09/0.40 p3(f4(f6(c21)),c22) ),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f23,negated_conjecture,(
% 0.09/0.40 (![X4,X5,X6,X7]: (( p19(X4,X5)| ~ p7(X6,X4)| ~ p7(X7,X5)| ~ p19(X6,X7) ) ))),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f25,negated_conjecture,(
% 0.09/0.40 (![X41,X42,X43,X44]: (( p7(f11(X41,X42),f11(X43,X44))| ~ p3(X42,X44)| ~ p7(X41,X43) ) ))),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f26,negated_conjecture,(
% 0.09/0.40 (![X37,X38,X39,X40]: (( p7(f10(X37,X38),f10(X39,X40))| ~ p7(X38,X40)| ~ p7(X37,X39) ) ))),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f27,negated_conjecture,(
% 0.09/0.40 ~ p19(f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21))) ),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f28,negated_conjecture,(
% 0.09/0.40 (![X8]: (( p19(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(X8))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X8)))| ~ p18(X8) ) ))),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f31,plain,(
% 0.09/0.40 p18(c21)),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.40 fof(f32,plain,(
% 0.09/0.40 ![X0]: (p7(X0,X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f3])).
% 0.09/0.40 fof(f36,plain,(
% 0.09/0.40 p3(f4(f6(c21)),c22)),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.09/0.40 fof(f56,plain,(
% 0.09/0.40 ![X6,X7]: ((![X5]: ((![X4]: (p19(X4,X5)|~p7(X6,X4)))|~p7(X7,X5)))|~p19(X6,X7))),
% 0.09/0.40 inference(miniscoping,[status(thm)],[f23])).
% 0.09/0.40 fof(f57,plain,(
% 0.09/0.40 ![X0,X1,X2,X3]: (p19(X0,X1)|~p7(X2,X0)|~p7(X3,X1)|~p19(X2,X3))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f56])).
% 0.09/0.40 fof(f60,plain,(
% 0.09/0.40 ![X41,X43]: ((![X42,X44]: (p7(f11(X41,X42),f11(X43,X44))|~p3(X42,X44)))|~p7(X41,X43))),
% 0.09/0.40 inference(miniscoping,[status(thm)],[f25])).
% 0.09/0.40 fof(f61,plain,(
% 0.09/0.40 ![X0,X1,X2,X3]: (p7(f11(X0,X1),f11(X2,X3))|~p3(X1,X3)|~p7(X0,X2))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f60])).
% 0.09/0.40 fof(f62,plain,(
% 0.09/0.40 ![X37,X39]: ((![X38,X40]: (p7(f10(X37,X38),f10(X39,X40))|~p7(X38,X40)))|~p7(X37,X39))),
% 0.09/0.40 inference(miniscoping,[status(thm)],[f26])).
% 0.09/0.40 fof(f63,plain,(
% 0.09/0.40 ![X0,X1,X2,X3]: (p7(f10(X0,X1),f10(X2,X3))|~p7(X1,X3)|~p7(X0,X2))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f62])).
% 0.09/0.40 fof(f64,plain,(
% 0.09/0.40 ~p19(f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21)))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f27])).
% 0.09/0.40 fof(f65,plain,(
% 0.09/0.40 ![X0]: (p19(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(X0))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0)))|~p18(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f28])).
% 0.09/0.40 fof(f73,plain,(
% 0.09/0.40 ![X0,X1,X2]: (~p18(X0)|p19(X1,X2)|~p7(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(X0))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),X1)|~p7(f8(f9(X0)),X2))),
% 0.09/0.40 inference(resolution,[status(thm)],[f65,f57])).
% 0.09/0.40 fof(f75,plain,(
% 0.09/0.40 ![X0,X1]: (p19(X0,X1)|~p7(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(c21))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),X0)|~p7(f8(f9(c21)),X1))),
% 0.09/0.40 inference(resolution,[status(thm)],[f73,f31])).
% 0.09/0.40 fof(f76,plain,(
% 0.09/0.40 ~p7(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(c21))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))))|~p7(f8(f9(c21)),f8(f9(c21)))),
% 0.09/0.40 inference(resolution,[status(thm)],[f75,f64])).
% 0.09/0.40 fof(f78,definition,(
% 0.09/0.40 sQ0_spl <=> (p7(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(c21))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23))))))))))))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f80,plain,(
% 0.09/0.40 ~p7(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(c21))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))))|sQ0_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f78])).
% 0.09/0.40 fof(f81,definition,(
% 0.09/0.40 sQ1_spl <=> (p7(f8(f9(c21)),f8(f9(c21))))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f83,plain,(
% 0.09/0.40 ~p7(f8(f9(c21)),f8(f9(c21)))|sQ1_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f81])).
% 0.09/0.40 fof(f84,plain,(
% 0.09/0.40 ~sQ0_spl|~sQ1_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f76,f78,f81])).
% 0.09/0.40 fof(f106,plain,(
% 0.09/0.40 ~p7(f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23))))))))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23))))))))))|~p7(f11(f14(f12(f15(f13(c23)))),f4(f6(c21))),f11(f14(f12(f15(f13(c23)))),c22))|sQ0_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f80,f63])).
% 0.09/0.40 fof(f108,definition,(
% 0.09/0.40 sQ6_spl <=> (p7(f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23))))))))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f110,plain,(
% 0.09/0.40 ~p7(f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23))))))))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23))))))))))|sQ6_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f108])).
% 0.09/0.40 fof(f111,definition,(
% 0.09/0.40 sQ7_spl <=> (p7(f11(f14(f12(f15(f13(c23)))),f4(f6(c21))),f11(f14(f12(f15(f13(c23)))),c22)))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f113,plain,(
% 0.09/0.40 ~p7(f11(f14(f12(f15(f13(c23)))),f4(f6(c21))),f11(f14(f12(f15(f13(c23)))),c22))|sQ7_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f111])).
% 0.09/0.40 fof(f114,plain,(
% 0.09/0.40 ~sQ6_spl|~sQ7_spl|sQ0_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f106,f108,f111,f78])).
% 0.09/0.40 fof(f115,plain,(
% 0.09/0.40 $false|sQ1_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f83,f32])).
% 0.09/0.40 fof(f116,plain,(
% 0.09/0.40 sQ1_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f115])).
% 0.09/0.40 fof(f117,plain,(
% 0.09/0.40 $false|sQ6_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f110,f32])).
% 0.09/0.40 fof(f118,plain,(
% 0.09/0.40 sQ6_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f117])).
% 0.09/0.40 fof(f125,plain,(
% 0.09/0.40 ~p3(f4(f6(c21)),c22)|~p7(f14(f12(f15(f13(c23)))),f14(f12(f15(f13(c23)))))|sQ7_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f113,f61])).
% 0.09/0.40 fof(f127,definition,(
% 0.09/0.40 sQ8_spl <=> (p3(f4(f6(c21)),c22))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f129,plain,(
% 0.09/0.40 ~p3(f4(f6(c21)),c22)|sQ8_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f127])).
% 0.09/0.40 fof(f130,definition,(
% 0.09/0.40 sQ9_spl <=> (p7(f14(f12(f15(f13(c23)))),f14(f12(f15(f13(c23))))))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f132,plain,(
% 0.09/0.40 ~p7(f14(f12(f15(f13(c23)))),f14(f12(f15(f13(c23)))))|sQ9_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f130])).
% 0.09/0.40 fof(f133,plain,(
% 0.09/0.40 ~sQ8_spl|~sQ9_spl|sQ7_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f125,f127,f130,f111])).
% 0.09/0.40 fof(f134,plain,(
% 0.09/0.40 $false|sQ8_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f129,f36])).
% 0.09/0.40 fof(f135,plain,(
% 0.09/0.40 sQ8_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f134])).
% 0.09/0.40 fof(f136,plain,(
% 0.09/0.40 $false|sQ9_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f132,f32])).
% 0.09/0.40 fof(f137,plain,(
% 0.09/0.40 sQ9_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f136])).
% 0.09/0.40 fof(f138,plain,(
% 0.09/0.40 $false),
% 0.09/0.40 inference(sat_refutation,[status(thm)],[f84,f114,f116,f118,f133,f135,f137])).
% 0.09/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.43 % Elapsed time: 0.047467 seconds
% 0.09/0.43 % CPU time: 0.142673 seconds
% 0.09/0.43 % Total memory used: 57.228 MB
% 0.09/0.43 % Net memory used: 56.905 MB
%------------------------------------------------------------------------------