%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN621-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 : n004.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:15 PM UTC 2026
% Result : Unsatisfiable 0.15s 5.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN621-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.58 % Computer : n004.cluster.edu
% 0.11/5.58 % Model : x86_64 x86_64
% 0.11/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.58 % Memory : 8046.5625MB
% 0.11/5.58 % OS : Linux 6.8.0-71-generic
% 0.11/5.59 % CPULimit : 300
% 0.11/5.59 % WCLimit : 300
% 0.11/5.59 % DateTime : Mon Sep 21 11:10:10 UTC 2026
% 0.11/5.59 % CPUTime :
% 0.15/5.60 % Drodi V4.1.1
% 0.15/5.61 % Refutation found
% 0.15/5.61 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/5.61 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.61 fof(f7,negated_conjecture,(
% 0.15/5.61 ~ p2(c23,f3(c24)) ),
% 0.15/5.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.61 fof(f18,negated_conjecture,(
% 0.15/5.61 (![X30,X31,X32]: (( p21(X30,X31)| ~ p21(X30,X32)| ~ p21(X32,X31) ) ))),
% 0.15/5.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.61 fof(f28,negated_conjecture,(
% 0.15/5.61 (![X15,X17,X18,X16]: (( p2(X15,f3(c24))| p22(f20(X17,X15,X18,X16),f14(f11(X17,f12(X15,X18)))) ) ))),
% 0.15/5.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.61 fof(f31,negated_conjecture,(
% 0.15/5.61 (![X33]: (( p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f5(f6(c27,X33)))| ~ p22(X33,f14(f11(c25,f12(c23,c26)))) ) ))),
% 0.15/5.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.61 fof(f32,negated_conjecture,(
% 0.15/5.61 ~ p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f15(f19(f11(c25,f12(c23,c26)),c27),f16(f3(f17(f18(c24)))))) ),
% 0.15/5.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.61 fof(f34,negated_conjecture,(
% 0.15/5.61 (![X15,X16,X17,X18]: (( p2(X15,f3(c24))| p21(f5(f6(X16,f20(X17,X15,X18,X16))),f15(f19(f11(X17,f12(X15,X18)),X16),f16(f3(f17(f18(c24)))))) ) ))),
% 0.15/5.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.61 fof(f41,plain,(
% 0.15/5.61 ~p2(c23,f3(c24))),
% 0.15/5.61 inference(cnf_transformation,[status(thm)],[f7])).
% 0.15/5.61 fof(f56,plain,(
% 0.15/5.61 ![X31,X32]: ((![X30]: (p21(X30,X31)|~p21(X30,X32)))|~p21(X32,X31))),
% 0.15/5.61 inference(miniscoping,[status(thm)],[f18])).
% 0.15/5.61 fof(f57,plain,(
% 0.15/5.61 ![X0,X1,X2]: (p21(X0,X1)|~p21(X0,X2)|~p21(X2,X1))),
% 0.15/5.61 inference(cnf_transformation,[status(thm)],[f56])).
% 0.15/5.61 fof(f76,plain,(
% 0.15/5.61 ![X15]: (p2(X15,f3(c24))|(![X17,X18,X16]: p22(f20(X17,X15,X18,X16),f14(f11(X17,f12(X15,X18))))))),
% 0.15/5.61 inference(miniscoping,[status(thm)],[f28])).
% 0.15/5.61 fof(f77,plain,(
% 0.15/5.61 ![X0,X1,X2,X3]: (p2(X0,f3(c24))|p22(f20(X1,X0,X2,X3),f14(f11(X1,f12(X0,X2)))))),
% 0.15/5.61 inference(cnf_transformation,[status(thm)],[f76])).
% 0.15/5.61 fof(f82,plain,(
% 0.15/5.61 ![X0]: (p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f5(f6(c27,X0)))|~p22(X0,f14(f11(c25,f12(c23,c26)))))),
% 0.15/5.61 inference(cnf_transformation,[status(thm)],[f31])).
% 0.15/5.61 fof(f83,plain,(
% 0.15/5.61 ~p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f15(f19(f11(c25,f12(c23,c26)),c27),f16(f3(f17(f18(c24))))))),
% 0.15/5.61 inference(cnf_transformation,[status(thm)],[f32])).
% 0.15/5.61 fof(f86,plain,(
% 0.15/5.61 ![X15]: (p2(X15,f3(c24))|(![X16,X17,X18]: p21(f5(f6(X16,f20(X17,X15,X18,X16))),f15(f19(f11(X17,f12(X15,X18)),X16),f16(f3(f17(f18(c24))))))))),
% 0.15/5.61 inference(miniscoping,[status(thm)],[f34])).
% 0.15/5.61 fof(f87,plain,(
% 0.15/5.61 ![X0,X1,X2,X3]: (p2(X0,f3(c24))|p21(f5(f6(X1,f20(X2,X0,X3,X1))),f15(f19(f11(X2,f12(X0,X3)),X1),f16(f3(f17(f18(c24)))))))),
% 0.15/5.61 inference(cnf_transformation,[status(thm)],[f86])).
% 0.15/5.61 fof(f123,plain,(
% 0.15/5.61 ![X0]: (p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f5(f6(c27,f20(c25,c23,c26,X0))))|p2(c23,f3(c24)))),
% 0.15/5.61 inference(resolution,[status(thm)],[f82,f77])).
% 0.15/5.61 fof(f124,definition,(
% 0.15/5.61 ![X0]: (sQ0_spl <=> (p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f5(f6(c27,f20(c25,c23,c26,X0))))))),
% 0.15/5.61 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/5.61 fof(f125,plain,(
% 0.15/5.61 ![X0]: (p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f5(f6(c27,f20(c25,c23,c26,X0))))|~sQ0_spl)),
% 0.15/5.61 inference(component_clause,[status(thm)],[f124])).
% 0.15/5.61 fof(f127,definition,(
% 0.15/5.61 sQ1_spl <=> (p2(c23,f3(c24)))),
% 0.15/5.61 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/5.61 fof(f128,plain,(
% 0.15/5.61 p2(c23,f3(c24))|~sQ1_spl),
% 0.15/5.61 inference(component_clause,[status(thm)],[f127])).
% 0.15/5.61 fof(f130,plain,(
% 0.15/5.61 sQ0_spl|sQ1_spl),
% 0.15/5.61 inference(split_clause,[status(thm)],[f123,f124,f127])).
% 0.15/5.61 fof(f135,plain,(
% 0.15/5.61 ![X0,X1]: (p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),X0)|~p21(f5(f6(c27,f20(c25,c23,c26,X1))),X0)|~sQ0_spl)),
% 0.15/5.61 inference(resolution,[status(thm)],[f125,f57])).
% 0.15/5.61 fof(f138,plain,(
% 0.15/5.61 p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f15(f19(f11(c25,f12(c23,c26)),c27),f16(f3(f17(f18(c24))))))|p2(c23,f3(c24))|~sQ0_spl),
% 0.15/5.61 inference(resolution,[status(thm)],[f135,f87])).
% 0.15/5.61 fof(f140,definition,(
% 0.15/5.61 sQ2_spl <=> (p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f15(f19(f11(c25,f12(c23,c26)),c27),f16(f3(f17(f18(c24)))))))),
% 0.15/5.62 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.15/5.62 fof(f141,plain,(
% 0.15/5.62 p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f15(f19(f11(c25,f12(c23,c26)),c27),f16(f3(f17(f18(c24))))))|~sQ2_spl),
% 0.15/5.62 inference(component_clause,[status(thm)],[f140])).
% 0.15/5.62 fof(f143,plain,(
% 0.15/5.62 sQ2_spl|sQ1_spl|~sQ0_spl),
% 0.15/5.62 inference(split_clause,[status(thm)],[f138,f140,f127,f124])).
% 0.15/5.62 fof(f145,plain,(
% 0.15/5.62 $false|~sQ1_spl),
% 0.15/5.62 inference(forward_subsumption_resolution,[status(thm)],[f128,f41])).
% 0.15/5.62 fof(f146,plain,(
% 0.15/5.62 ~sQ1_spl),
% 0.15/5.62 inference(contradiction_clause,[status(thm)],[f145])).
% 0.15/5.62 fof(f147,plain,(
% 0.15/5.62 $false|~sQ2_spl),
% 0.15/5.62 inference(forward_subsumption_resolution,[status(thm)],[f141,f83])).
% 0.15/5.62 fof(f148,plain,(
% 0.15/5.62 ~sQ2_spl),
% 0.15/5.62 inference(contradiction_clause,[status(thm)],[f147])).
% 0.15/5.62 fof(f149,plain,(
% 0.15/5.62 $false),
% 0.15/5.62 inference(sat_refutation,[status(thm)],[f130,f143,f146,f148])).
% 0.15/5.62 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.63 % Elapsed time: 0.035518 seconds
% 0.15/5.63 % CPU time: 0.089068 seconds
% 0.15/5.63 % Total memory used: 8.748 MB
% 0.15/5.63 % Net memory used: 8.655 MB
%------------------------------------------------------------------------------