%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN100-1.005 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:18:57 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN100-1.005 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n002.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 10:46:02 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 0.13/0.37 % Refutation found
% 0.13/0.37 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.37 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.37 fof(f1,negated_conjecture,(
% 0.13/0.37 (![X]: (( ~ p_0(X)| ~ q_0(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f2,axiom,(
% 0.13/0.37 (![X]: (( p_0(X)| ~ p_1(X)| ~ p_2(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f4,axiom,(
% 0.13/0.37 (![X]: (( p_1(X)| ~ p_2(X)| ~ p_3(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f6,axiom,(
% 0.13/0.37 (![X]: (( p_2(X)| ~ p_3(X)| ~ p_4(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f8,axiom,(
% 0.13/0.37 (![X]: (( p_3(X)| ~ p_4(X)| ~ p_5(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f10,axiom,(
% 0.13/0.37 (![X]: (( p_4(X)| ~ p_5(X)| ~ p_6(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f12,axiom,(
% 0.13/0.37 (![X]: (( p_5(X)| ~ p_6(X)| ~ p_7(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f14,axiom,(
% 0.13/0.37 (![X]: (( p_6(X)| ~ p_7(X)| ~ p_8(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f16,axiom,(
% 0.13/0.37 (![X]: (( p_7(X)| ~ p_8(X)| ~ p_9(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f18,axiom,(
% 0.13/0.37 (![X]: (( q_0(X)| ~ p_1(X)| ~ q_2(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f22,axiom,(
% 0.13/0.37 (![X]: (( q_2(X)| ~ p_3(X)| ~ q_4(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f26,axiom,(
% 0.13/0.37 (![X]: (( q_4(X)| ~ p_5(X)| ~ q_6(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f30,axiom,(
% 0.13/0.37 (![X]: (( q_6(X)| ~ p_7(X)| ~ q_8(X) ) ))),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f38,axiom,(
% 0.13/0.37 p_8(a) ),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f39,axiom,(
% 0.13/0.37 p_9(a) ),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f40,axiom,(
% 0.13/0.37 q_8(a) ),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f41,axiom,(
% 0.13/0.37 q_9(a) ),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f83,plain,(
% 0.13/0.37 ![X0]: (~p_0(X0)|~q_0(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.37 fof(f84,plain,(
% 0.13/0.37 ![X0]: (p_0(X0)|~p_1(X0)|~p_2(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.37 fof(f86,plain,(
% 0.13/0.37 ![X0]: (p_1(X0)|~p_2(X0)|~p_3(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.37 fof(f88,plain,(
% 0.13/0.37 ![X0]: (p_2(X0)|~p_3(X0)|~p_4(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.37 fof(f90,plain,(
% 0.13/0.37 ![X0]: (p_3(X0)|~p_4(X0)|~p_5(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.37 fof(f92,plain,(
% 0.13/0.37 ![X0]: (p_4(X0)|~p_5(X0)|~p_6(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.37 fof(f94,plain,(
% 0.13/0.37 ![X0]: (p_5(X0)|~p_6(X0)|~p_7(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/0.37 fof(f96,plain,(
% 0.13/0.37 ![X0]: (p_6(X0)|~p_7(X0)|~p_8(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f14])).
% 0.13/0.37 fof(f98,plain,(
% 0.13/0.37 ![X0]: (p_7(X0)|~p_8(X0)|~p_9(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f16])).
% 0.13/0.37 fof(f100,plain,(
% 0.13/0.37 ![X0]: (q_0(X0)|~p_1(X0)|~q_2(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f18])).
% 0.13/0.37 fof(f104,plain,(
% 0.13/0.37 ![X0]: (q_2(X0)|~p_3(X0)|~q_4(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f22])).
% 0.13/0.37 fof(f108,plain,(
% 0.13/0.37 ![X0]: (q_4(X0)|~p_5(X0)|~q_6(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f26])).
% 0.13/0.37 fof(f112,plain,(
% 0.13/0.37 ![X0]: (q_6(X0)|~p_7(X0)|~q_8(X0))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f30])).
% 0.13/0.37 fof(f120,plain,(
% 0.13/0.37 p_8(a)),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f38])).
% 0.13/0.37 fof(f121,plain,(
% 0.13/0.37 p_9(a)),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f39])).
% 0.13/0.37 fof(f122,plain,(
% 0.13/0.37 q_8(a)),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f40])).
% 0.13/0.37 fof(f123,plain,(
% 0.13/0.37 q_9(a)),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f41])).
% 0.13/0.37 fof(f165,plain,(
% 0.13/0.37 p_7(a)|~p_9(a)),
% 0.13/0.37 inference(resolution,[status(thm)],[f98,f120])).
% 0.13/0.37 fof(f166,definition,(
% 0.13/0.37 sQ0_spl <=> (p_7(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f167,plain,(
% 0.13/0.37 p_7(a)|~sQ0_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f166])).
% 0.13/0.37 fof(f169,definition,(
% 0.13/0.37 sQ1_spl <=> (p_9(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f171,plain,(
% 0.13/0.37 ~p_9(a)|sQ1_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f169])).
% 0.13/0.37 fof(f172,plain,(
% 0.13/0.37 sQ0_spl|~sQ1_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f165,f166,f169])).
% 0.13/0.37 fof(f174,definition,(
% 0.13/0.37 sQ2_spl <=> (q_9(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f176,plain,(
% 0.13/0.37 ~q_9(a)|sQ2_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f174])).
% 0.13/0.37 fof(f178,plain,(
% 0.13/0.37 p_6(a)|~p_8(a)|~sQ0_spl),
% 0.13/0.37 inference(resolution,[status(thm)],[f167,f96])).
% 0.13/0.37 fof(f179,plain,(
% 0.13/0.37 p_5(a)|~p_6(a)|~sQ0_spl),
% 0.13/0.37 inference(resolution,[status(thm)],[f167,f94])).
% 0.13/0.37 fof(f180,definition,(
% 0.13/0.37 sQ3_spl <=> (p_6(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f181,plain,(
% 0.13/0.37 p_6(a)|~sQ3_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f180])).
% 0.13/0.37 fof(f183,definition,(
% 0.13/0.37 sQ4_spl <=> (p_8(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f185,plain,(
% 0.13/0.37 ~p_8(a)|sQ4_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f183])).
% 0.13/0.37 fof(f186,plain,(
% 0.13/0.37 sQ3_spl|~sQ4_spl|~sQ0_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f178,f180,f183,f166])).
% 0.13/0.37 fof(f187,definition,(
% 0.13/0.37 sQ5_spl <=> (p_5(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f188,plain,(
% 0.13/0.37 p_5(a)|~sQ5_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f187])).
% 0.13/0.37 fof(f190,plain,(
% 0.13/0.37 sQ5_spl|~sQ3_spl|~sQ0_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f179,f187,f180,f166])).
% 0.13/0.37 fof(f191,plain,(
% 0.13/0.37 $false|sQ1_spl),
% 0.13/0.37 inference(forward_subsumption_resolution,[status(thm)],[f171,f121])).
% 0.13/0.37 fof(f192,plain,(
% 0.13/0.37 sQ1_spl),
% 0.13/0.37 inference(contradiction_clause,[status(thm)],[f191])).
% 0.13/0.37 fof(f193,plain,(
% 0.13/0.37 $false|sQ4_spl),
% 0.13/0.37 inference(forward_subsumption_resolution,[status(thm)],[f185,f120])).
% 0.13/0.37 fof(f194,plain,(
% 0.13/0.37 sQ4_spl),
% 0.13/0.37 inference(contradiction_clause,[status(thm)],[f193])).
% 0.13/0.37 fof(f195,plain,(
% 0.13/0.37 p_3(a)|~p_4(a)|~sQ5_spl),
% 0.13/0.37 inference(resolution,[status(thm)],[f188,f90])).
% 0.13/0.37 fof(f196,definition,(
% 0.13/0.37 sQ6_spl <=> (p_3(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f197,plain,(
% 0.13/0.37 p_3(a)|~sQ6_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f196])).
% 0.13/0.37 fof(f199,definition,(
% 0.13/0.37 sQ7_spl <=> (p_4(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f200,plain,(
% 0.13/0.37 p_4(a)|~sQ7_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f199])).
% 0.13/0.37 fof(f202,plain,(
% 0.13/0.37 sQ6_spl|~sQ7_spl|~sQ5_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f195,f196,f199,f187])).
% 0.13/0.37 fof(f207,plain,(
% 0.13/0.37 p_4(a)|~p_5(a)|~sQ3_spl),
% 0.13/0.37 inference(resolution,[status(thm)],[f181,f92])).
% 0.13/0.37 fof(f208,plain,(
% 0.13/0.37 sQ7_spl|~sQ5_spl|~sQ3_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f207,f199,f187,f180])).
% 0.13/0.37 fof(f209,plain,(
% 0.13/0.37 p_1(a)|~p_2(a)|~sQ6_spl),
% 0.13/0.37 inference(resolution,[status(thm)],[f197,f86])).
% 0.13/0.37 fof(f210,definition,(
% 0.13/0.37 sQ8_spl <=> (p_1(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f213,definition,(
% 0.13/0.37 sQ9_spl <=> (p_2(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f214,plain,(
% 0.13/0.37 p_2(a)|~sQ9_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f213])).
% 0.13/0.37 fof(f216,plain,(
% 0.13/0.37 sQ8_spl|~sQ9_spl|~sQ6_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f209,f210,f213,f196])).
% 0.13/0.37 fof(f217,plain,(
% 0.13/0.37 p_2(a)|~p_3(a)|~sQ7_spl),
% 0.13/0.37 inference(resolution,[status(thm)],[f200,f88])).
% 0.13/0.37 fof(f218,plain,(
% 0.13/0.37 sQ9_spl|~sQ6_spl|~sQ7_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f217,f213,f196,f199])).
% 0.13/0.37 fof(f219,plain,(
% 0.13/0.37 p_0(a)|~p_1(a)|~sQ9_spl),
% 0.13/0.37 inference(resolution,[status(thm)],[f214,f84])).
% 0.13/0.37 fof(f220,definition,(
% 0.13/0.37 sQ10_spl <=> (p_0(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f221,plain,(
% 0.13/0.37 p_0(a)|~sQ10_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f220])).
% 0.13/0.37 fof(f223,plain,(
% 0.13/0.37 sQ10_spl|~sQ8_spl|~sQ9_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f219,f220,f210,f213])).
% 0.13/0.37 fof(f224,plain,(
% 0.13/0.37 q_6(a)|~p_7(a)),
% 0.13/0.37 inference(resolution,[status(thm)],[f112,f122])).
% 0.13/0.37 fof(f225,definition,(
% 0.13/0.37 sQ11_spl <=> (q_6(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f226,plain,(
% 0.13/0.37 q_6(a)|~sQ11_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f225])).
% 0.13/0.37 fof(f228,plain,(
% 0.13/0.37 sQ11_spl|~sQ0_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f224,f225,f166])).
% 0.13/0.37 fof(f230,plain,(
% 0.13/0.37 q_4(a)|~p_5(a)|~sQ11_spl),
% 0.13/0.37 inference(resolution,[status(thm)],[f226,f108])).
% 0.13/0.37 fof(f236,definition,(
% 0.13/0.37 sQ13_spl <=> (q_4(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f237,plain,(
% 0.13/0.37 q_4(a)|~sQ13_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f236])).
% 0.13/0.37 fof(f239,plain,(
% 0.13/0.37 sQ13_spl|~sQ5_spl|~sQ11_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f230,f236,f187,f225])).
% 0.13/0.37 fof(f242,plain,(
% 0.13/0.37 q_2(a)|~p_3(a)|~sQ13_spl),
% 0.13/0.37 inference(resolution,[status(thm)],[f237,f104])).
% 0.13/0.37 fof(f248,definition,(
% 0.13/0.37 sQ15_spl <=> (q_2(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f249,plain,(
% 0.13/0.37 q_2(a)|~sQ15_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f248])).
% 0.13/0.37 fof(f251,plain,(
% 0.13/0.37 sQ15_spl|~sQ6_spl|~sQ13_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f242,f248,f196,f236])).
% 0.13/0.37 fof(f258,plain,(
% 0.13/0.37 $false|sQ2_spl),
% 0.13/0.37 inference(forward_subsumption_resolution,[status(thm)],[f176,f123])).
% 0.13/0.37 fof(f259,plain,(
% 0.13/0.37 sQ2_spl),
% 0.13/0.37 inference(contradiction_clause,[status(thm)],[f258])).
% 0.13/0.37 fof(f267,plain,(
% 0.13/0.37 q_0(a)|~p_1(a)|~sQ15_spl),
% 0.13/0.37 inference(resolution,[status(thm)],[f249,f100])).
% 0.13/0.37 fof(f273,definition,(
% 0.13/0.37 sQ18_spl <=> (q_0(a))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f274,plain,(
% 0.13/0.37 q_0(a)|~sQ18_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f273])).
% 0.13/0.37 fof(f276,plain,(
% 0.13/0.37 sQ18_spl|~sQ8_spl|~sQ15_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f267,f273,f210,f248])).
% 0.13/0.37 fof(f295,plain,(
% 0.13/0.37 ~p_0(a)|~sQ18_spl),
% 0.13/0.38 inference(resolution,[status(thm)],[f274,f83])).
% 0.13/0.38 fof(f296,plain,(
% 0.13/0.38 $false|~sQ10_spl|~sQ18_spl),
% 0.13/0.38 inference(forward_subsumption_resolution,[status(thm)],[f295,f221])).
% 0.13/0.38 fof(f297,plain,(
% 0.13/0.38 ~sQ10_spl|~sQ18_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f296])).
% 0.13/0.38 fof(f298,plain,(
% 0.13/0.38 $false),
% 0.13/0.38 inference(sat_refutation,[status(thm)],[f172,f186,f190,f192,f194,f202,f208,f216,f218,f223,f228,f239,f251,f259,f276,f297])).
% 0.13/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.40 % Elapsed time: 0.038626 seconds
% 0.13/0.40 % CPU time: 0.117019 seconds
% 0.13/0.40 % Total memory used: 18.928 MB
% 0.13/0.40 % Net memory used: 18.894 MB
%------------------------------------------------------------------------------