%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ030-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 02:00:18 PM UTC 2026
% Result : Unsatisfiable 0.08s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ030-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n006.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 03:45:57 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.08/0.38 % Refutation found
% 0.08/0.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.08/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.38 fof(f1,hypothesis,(
% 0.08/0.38 ( ~ salt_mill| mustard_barry| mustard_lang ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f2,hypothesis,(
% 0.08/0.38 ( ~ salt_mill| mustard_barry| salt_lang ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f3,hypothesis,(
% 0.08/0.38 ( ~ salt_mill| salt_barry| mustard_lang ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f6,hypothesis,(
% 0.08/0.38 ( ~ mustard_lang| ~ mustard_cole| ~ salt_mill ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f8,hypothesis,(
% 0.08/0.38 ( ~ mustard_lang| ~ salt_cole| ~ salt_mill ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f10,hypothesis,(
% 0.08/0.38 ( ~ mustard_dix| ~ mustard_lang| ~ salt_mill ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f11,hypothesis,(
% 0.08/0.38 ( ~ mustard_dix| ~ salt_lang| ~ mustard_mill ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f13,hypothesis,(
% 0.08/0.38 ( ~ salt_dix| ~ mustard_barry| mustard_cole ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f14,hypothesis,(
% 0.08/0.38 ( ~ salt_dix| ~ mustard_barry| salt_cole ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f15,hypothesis,(
% 0.08/0.38 ( ~ salt_dix| ~ salt_barry| mustard_cole ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f17,hypothesis,(
% 0.08/0.38 ( ~ mustard_cole| mustard_dix| mustard_lang ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f19,hypothesis,(
% 0.08/0.38 ( ~ mustard_cole| salt_dix| mustard_lang ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f29,hypothesis,(
% 0.08/0.38 ( ~ salt_lang| ~ mustard_lang| salt_mill ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f30,hypothesis,(
% 0.08/0.38 ( ~ salt_barry| ~ mustard_barry| salt_mill ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f33,hypothesis,(
% 0.08/0.38 ( salt_barry| ~ mustard_barry| salt_lang ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f34,hypothesis,(
% 0.08/0.38 ( ~ salt_barry| mustard_barry| salt_lang ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f36,hypothesis,(
% 0.08/0.38 ( ~ salt_lang| ~ mustard_lang| mustard_cole ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f38,hypothesis,(
% 0.08/0.38 ( salt_barry| ~ mustard_barry| salt_cole ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f41,hypothesis,(
% 0.08/0.38 ( salt_lang| ~ mustard_lang| salt_barry ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f42,hypothesis,(
% 0.08/0.38 ( ~ salt_lang| mustard_lang| salt_barry ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f43,hypothesis,(
% 0.08/0.38 ( salt_cole| ~ mustard_cole| salt_barry ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f46,hypothesis,(
% 0.08/0.38 ( ~ salt_cole| ~ mustard_barry| ~ salt_barry| ~ salt_mill ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f47,hypothesis,(
% 0.08/0.38 ( ~ salt_cole| salt_barry| mustard_barry| ~ mustard_mill ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f50,hypothesis,(
% 0.08/0.38 ( ~ mustard_mill| salt_cole| mustard_cole| salt_dix| mustard_dix ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f52,hypothesis,(
% 0.08/0.38 ( ~ salt_lang| ~ mustard_barry| ~ salt_barry| salt_dix| mustard_dix ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f56,hypothesis,(
% 0.08/0.38 ( salt_mill| mustard_mill| mustard_lang ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f57,hypothesis,(
% 0.08/0.38 ( salt_cole| mustard_cole| mustard_lang ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f59,hypothesis,(
% 0.08/0.38 ( salt_lang| mustard_lang| mustard_dix ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f62,hypothesis,(
% 0.08/0.38 ( salt_dix| mustard_dix| mustard_barry ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f63,negated_conjecture,(
% 0.08/0.38 ( salt_lang| ~ mustard_barry| ~ salt_barry| ~ salt_mill| ~ mustard_lang| salt_cole| mustard_cole| salt_dix| mustard_dix| mustard_mill ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f64,plain,(
% 0.08/0.38 ~salt_mill|mustard_barry|mustard_lang),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f1])).
% 0.08/0.38 fof(f65,plain,(
% 0.08/0.38 ~salt_mill|mustard_barry|salt_lang),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f2])).
% 0.08/0.38 fof(f66,plain,(
% 0.08/0.38 ~salt_mill|salt_barry|mustard_lang),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.38 fof(f69,plain,(
% 0.08/0.38 ~mustard_lang|~mustard_cole|~salt_mill),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f6])).
% 0.08/0.38 fof(f71,plain,(
% 0.08/0.38 ~mustard_lang|~salt_cole|~salt_mill),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f8])).
% 0.08/0.38 fof(f73,plain,(
% 0.08/0.38 ~mustard_dix|~mustard_lang|~salt_mill),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f10])).
% 0.08/0.38 fof(f74,plain,(
% 0.08/0.38 ~mustard_dix|~salt_lang|~mustard_mill),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f11])).
% 0.08/0.38 fof(f76,plain,(
% 0.08/0.38 ~salt_dix|~mustard_barry|mustard_cole),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f13])).
% 0.08/0.38 fof(f77,plain,(
% 0.08/0.38 ~salt_dix|~mustard_barry|salt_cole),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f14])).
% 0.08/0.38 fof(f78,plain,(
% 0.08/0.38 ~salt_dix|~salt_barry|mustard_cole),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f15])).
% 0.08/0.38 fof(f80,plain,(
% 0.08/0.38 ~mustard_cole|mustard_dix|mustard_lang),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f17])).
% 0.08/0.38 fof(f82,plain,(
% 0.08/0.38 ~mustard_cole|salt_dix|mustard_lang),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f19])).
% 0.08/0.38 fof(f92,plain,(
% 0.08/0.38 ~salt_lang|~mustard_lang|salt_mill),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f29])).
% 0.08/0.38 fof(f93,plain,(
% 0.08/0.38 ~salt_barry|~mustard_barry|salt_mill),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f30])).
% 0.08/0.38 fof(f96,plain,(
% 0.08/0.38 salt_barry|~mustard_barry|salt_lang),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f33])).
% 0.08/0.38 fof(f97,plain,(
% 0.08/0.38 ~salt_barry|mustard_barry|salt_lang),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f34])).
% 0.08/0.38 fof(f99,plain,(
% 0.08/0.38 ~salt_lang|~mustard_lang|mustard_cole),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f36])).
% 0.08/0.38 fof(f101,plain,(
% 0.08/0.38 salt_barry|~mustard_barry|salt_cole),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f38])).
% 0.08/0.38 fof(f104,plain,(
% 0.08/0.38 salt_lang|~mustard_lang|salt_barry),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f41])).
% 0.08/0.38 fof(f105,plain,(
% 0.08/0.38 ~salt_lang|mustard_lang|salt_barry),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f42])).
% 0.08/0.38 fof(f106,plain,(
% 0.08/0.38 salt_cole|~mustard_cole|salt_barry),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f43])).
% 0.08/0.38 fof(f109,plain,(
% 0.08/0.38 ~salt_cole|~mustard_barry|~salt_barry|~salt_mill),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f46])).
% 0.08/0.38 fof(f110,plain,(
% 0.08/0.38 ~salt_cole|salt_barry|mustard_barry|~mustard_mill),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f47])).
% 0.08/0.38 fof(f113,plain,(
% 0.08/0.38 ~mustard_mill|salt_cole|mustard_cole|salt_dix|mustard_dix),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f50])).
% 0.08/0.38 fof(f115,plain,(
% 0.08/0.38 ~salt_lang|~mustard_barry|~salt_barry|salt_dix|mustard_dix),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f52])).
% 0.08/0.38 fof(f119,plain,(
% 0.08/0.38 salt_mill|mustard_mill|mustard_lang),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f56])).
% 0.08/0.38 fof(f120,plain,(
% 0.08/0.38 salt_cole|mustard_cole|mustard_lang),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f57])).
% 0.08/0.38 fof(f122,plain,(
% 0.08/0.38 salt_lang|mustard_lang|mustard_dix),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f59])).
% 0.08/0.38 fof(f125,plain,(
% 0.08/0.38 salt_dix|mustard_dix|mustard_barry),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f62])).
% 0.08/0.38 fof(f126,plain,(
% 0.08/0.38 salt_lang|~mustard_barry|~salt_barry|~salt_mill|~mustard_lang|salt_cole|mustard_cole|salt_dix|mustard_dix|mustard_mill),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f63])).
% 0.08/0.38 fof(f127,definition,(
% 0.08/0.38 sQ0_spl <=> (salt_mill)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f130,definition,(
% 0.08/0.38 sQ1_spl <=> (mustard_barry)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f133,definition,(
% 0.08/0.38 sQ2_spl <=> (mustard_lang)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f136,plain,(
% 0.08/0.38 ~sQ0_spl|sQ1_spl|sQ2_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f64,f127,f130,f133])).
% 0.08/0.38 fof(f137,definition,(
% 0.08/0.38 sQ3_spl <=> (salt_lang)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f140,plain,(
% 0.08/0.38 ~sQ0_spl|sQ1_spl|sQ3_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f65,f127,f130,f137])).
% 0.08/0.38 fof(f141,definition,(
% 0.08/0.38 sQ4_spl <=> (salt_barry)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f144,plain,(
% 0.08/0.38 ~sQ0_spl|sQ4_spl|sQ2_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f66,f127,f141,f133])).
% 0.08/0.38 fof(f146,definition,(
% 0.08/0.38 sQ5_spl <=> (mustard_cole)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f149,definition,(
% 0.08/0.38 sQ6_spl <=> (mustard_mill)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f153,plain,(
% 0.08/0.38 ~sQ2_spl|~sQ5_spl|~sQ0_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f69,f133,f146,f127])).
% 0.08/0.38 fof(f154,definition,(
% 0.08/0.38 sQ7_spl <=> (salt_cole)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f158,plain,(
% 0.08/0.38 ~sQ2_spl|~sQ7_spl|~sQ0_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f71,f133,f154,f127])).
% 0.08/0.38 fof(f159,definition,(
% 0.08/0.38 sQ8_spl <=> (mustard_dix)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f163,plain,(
% 0.08/0.38 ~sQ8_spl|~sQ2_spl|~sQ0_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f73,f159,f133,f127])).
% 0.08/0.38 fof(f164,plain,(
% 0.08/0.38 ~sQ8_spl|~sQ3_spl|~sQ6_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f74,f159,f137,f149])).
% 0.08/0.38 fof(f166,definition,(
% 0.08/0.38 sQ9_spl <=> (salt_dix)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f169,plain,(
% 0.08/0.38 ~sQ9_spl|~sQ1_spl|sQ5_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f76,f166,f130,f146])).
% 0.08/0.38 fof(f170,plain,(
% 0.08/0.38 ~sQ9_spl|~sQ1_spl|sQ7_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f77,f166,f130,f154])).
% 0.08/0.38 fof(f171,plain,(
% 0.08/0.38 ~sQ9_spl|~sQ4_spl|sQ5_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f78,f166,f141,f146])).
% 0.08/0.38 fof(f173,plain,(
% 0.08/0.38 ~sQ5_spl|sQ8_spl|sQ2_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f80,f146,f159,f133])).
% 0.08/0.38 fof(f175,plain,(
% 0.08/0.38 ~sQ5_spl|sQ9_spl|sQ2_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f82,f146,f166,f133])).
% 0.08/0.38 fof(f185,plain,(
% 0.08/0.38 ~sQ3_spl|~sQ2_spl|sQ0_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f92,f137,f133,f127])).
% 0.08/0.38 fof(f186,plain,(
% 0.08/0.38 ~sQ4_spl|~sQ1_spl|sQ0_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f93,f141,f130,f127])).
% 0.08/0.38 fof(f189,plain,(
% 0.08/0.38 sQ4_spl|~sQ1_spl|sQ3_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f96,f141,f130,f137])).
% 0.08/0.38 fof(f190,plain,(
% 0.08/0.38 ~sQ4_spl|sQ1_spl|sQ3_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f97,f141,f130,f137])).
% 0.08/0.38 fof(f192,plain,(
% 0.08/0.38 ~sQ3_spl|~sQ2_spl|sQ5_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f99,f137,f133,f146])).
% 0.08/0.38 fof(f194,plain,(
% 0.08/0.38 sQ4_spl|~sQ1_spl|sQ7_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f101,f141,f130,f154])).
% 0.08/0.38 fof(f197,plain,(
% 0.08/0.38 sQ3_spl|~sQ2_spl|sQ4_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f104,f137,f133,f141])).
% 0.08/0.38 fof(f198,plain,(
% 0.08/0.38 ~sQ3_spl|sQ2_spl|sQ4_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f105,f137,f133,f141])).
% 0.08/0.38 fof(f199,plain,(
% 0.08/0.38 sQ7_spl|~sQ5_spl|sQ4_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f106,f154,f146,f141])).
% 0.08/0.38 fof(f202,plain,(
% 0.08/0.38 ~sQ7_spl|~sQ1_spl|~sQ4_spl|~sQ0_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f109,f154,f130,f141,f127])).
% 0.08/0.38 fof(f203,plain,(
% 0.08/0.38 ~sQ7_spl|sQ4_spl|sQ1_spl|~sQ6_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f110,f154,f141,f130,f149])).
% 0.08/0.38 fof(f206,plain,(
% 0.08/0.38 ~sQ6_spl|sQ7_spl|sQ5_spl|sQ9_spl|sQ8_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f113,f149,f154,f146,f166,f159])).
% 0.08/0.38 fof(f208,plain,(
% 0.08/0.38 ~sQ3_spl|~sQ1_spl|~sQ4_spl|sQ9_spl|sQ8_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f115,f137,f130,f141,f166,f159])).
% 0.08/0.38 fof(f212,plain,(
% 0.08/0.38 sQ0_spl|sQ6_spl|sQ2_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f119,f127,f149,f133])).
% 0.08/0.38 fof(f213,plain,(
% 0.08/0.38 sQ7_spl|sQ5_spl|sQ2_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f120,f154,f146,f133])).
% 0.08/0.38 fof(f215,plain,(
% 0.08/0.38 sQ3_spl|sQ2_spl|sQ8_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f122,f137,f133,f159])).
% 0.08/0.38 fof(f218,plain,(
% 0.08/0.38 sQ9_spl|sQ8_spl|sQ1_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f125,f166,f159,f130])).
% 0.08/0.38 fof(f219,plain,(
% 0.08/0.38 sQ3_spl|~sQ1_spl|~sQ4_spl|~sQ0_spl|~sQ2_spl|sQ7_spl|sQ5_spl|sQ9_spl|sQ8_spl|sQ6_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f126,f137,f130,f141,f127,f133,f154,f146,f166,f159,f149])).
% 0.08/0.38 fof(f220,plain,(
% 0.08/0.38 $false),
% 0.08/0.38 inference(sat_refutation,[status(thm)],[f136,f140,f144,f153,f158,f163,f164,f169,f170,f171,f173,f175,f185,f186,f189,f190,f192,f194,f197,f198,f199,f202,f203,f206,f208,f212,f213,f215,f218,f219])).
% 0.08/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.41 % Elapsed time: 0.044290 seconds
% 0.13/0.41 % CPU time: 0.110112 seconds
% 0.13/0.41 % Total memory used: 17.840 MB
% 0.13/0.41 % Net memory used: 17.795 MB
%------------------------------------------------------------------------------