%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN093-1.002 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:56 PM UTC 2026
% Result : Unsatisfiable 0.10s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN093-1.002 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.57 % Computer : n015.cluster.edu
% 0.10/0.57 % Model : x86_64 x86_64
% 0.10/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.57 % Memory : 8046.5625MB
% 0.10/0.57 % OS : Linux 6.8.0-71-generic
% 0.10/0.57 % CPULimit : 300
% 0.10/0.57 % WCLimit : 300
% 0.10/0.57 % DateTime : Mon Sep 21 10:46:07 UTC 2026
% 0.10/0.57 % CPUTime :
% 0.10/0.58 % Drodi V4.1.1
% 0.10/0.59 % Refutation found
% 0.10/0.59 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.59 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.59 fof(f1,negated_conjecture,(
% 0.10/0.59 ( u_1| ~ p_1_2 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f2,axiom,(
% 0.10/0.59 ~ u_1 ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f4,axiom,(
% 0.10/0.59 ( p_1_2| ~ u_2 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f5,axiom,(
% 0.10/0.59 ( u_3| p_1_2| ~ q_2_2| ~ q_1_1 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f6,axiom,(
% 0.10/0.59 ( p_1_2| ~ u_3 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f9,axiom,(
% 0.10/0.59 ( u_5| q_1_2| ~ q_2_2| ~ p_1_1 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f10,axiom,(
% 0.10/0.59 ( q_1_2| ~ u_5 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f13,axiom,(
% 0.10/0.59 ( u_7| q_1_1| ~ q_1_2 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f14,axiom,(
% 0.10/0.59 ( q_1_1| ~ u_7 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f19,axiom,(
% 0.10/0.59 ( u_10| p_1_1 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f20,axiom,(
% 0.10/0.59 ( p_1_1| ~ u_10 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f25,axiom,(
% 0.10/0.59 ( u_13| q_2_2 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f26,axiom,(
% 0.10/0.59 ( q_2_2| ~ u_13 ) ),
% 0.10/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.59 fof(f27,plain,(
% 0.10/0.59 u_1|~p_1_2),
% 0.10/0.59 inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/0.59 fof(f28,plain,(
% 0.10/0.59 ~u_1),
% 0.10/0.59 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.59 fof(f30,plain,(
% 0.10/0.59 p_1_2|~u_2),
% 0.10/0.59 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.59 fof(f31,plain,(
% 0.10/0.59 u_3|p_1_2|~q_2_2|~q_1_1),
% 0.10/0.59 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.59 fof(f32,plain,(
% 0.10/0.59 p_1_2|~u_3),
% 0.10/0.59 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.59 fof(f35,plain,(
% 0.10/0.59 u_5|q_1_2|~q_2_2|~p_1_1),
% 0.10/0.59 inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/0.59 fof(f36,plain,(
% 0.10/0.59 q_1_2|~u_5),
% 0.10/0.59 inference(cnf_transformation,[status(thm)],[f10])).
% 0.10/0.60 fof(f39,plain,(
% 0.10/0.60 u_7|q_1_1|~q_1_2),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f13])).
% 0.10/0.60 fof(f40,plain,(
% 0.10/0.60 q_1_1|~u_7),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f14])).
% 0.10/0.60 fof(f45,plain,(
% 0.10/0.60 u_10|p_1_1),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f19])).
% 0.10/0.60 fof(f46,plain,(
% 0.10/0.60 p_1_1|~u_10),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f20])).
% 0.10/0.60 fof(f51,plain,(
% 0.10/0.60 u_13|q_2_2),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f25])).
% 0.10/0.60 fof(f52,plain,(
% 0.10/0.60 q_2_2|~u_13),
% 0.10/0.60 inference(cnf_transformation,[status(thm)],[f26])).
% 0.10/0.60 fof(f53,definition,(
% 0.10/0.60 sQ0_spl <=> (u_1)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f54,plain,(
% 0.10/0.60 u_1|~sQ0_spl),
% 0.10/0.60 inference(component_clause,[status(thm)],[f53])).
% 0.10/0.60 fof(f56,definition,(
% 0.10/0.60 sQ1_spl <=> (p_1_2)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f59,plain,(
% 0.10/0.60 sQ0_spl|~sQ1_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f27,f53,f56])).
% 0.10/0.60 fof(f60,definition,(
% 0.10/0.60 sQ2_spl <=> (u_2)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f66,definition,(
% 0.10/0.60 sQ4_spl <=> (p_1_1)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f70,plain,(
% 0.10/0.60 sQ1_spl|~sQ2_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f30,f56,f60])).
% 0.10/0.60 fof(f71,definition,(
% 0.10/0.60 sQ5_spl <=> (u_3)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f74,definition,(
% 0.10/0.60 sQ6_spl <=> (q_2_2)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f77,definition,(
% 0.10/0.60 sQ7_spl <=> (q_1_1)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f80,plain,(
% 0.10/0.60 sQ5_spl|sQ1_spl|~sQ6_spl|~sQ7_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f31,f71,f56,f74,f77])).
% 0.10/0.60 fof(f81,plain,(
% 0.10/0.60 sQ1_spl|~sQ5_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f32,f56,f71])).
% 0.10/0.60 fof(f85,definition,(
% 0.10/0.60 sQ9_spl <=> (q_1_2)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f90,definition,(
% 0.10/0.60 sQ10_spl <=> (u_5)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f93,plain,(
% 0.10/0.60 sQ10_spl|sQ9_spl|~sQ6_spl|~sQ4_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f35,f90,f85,f74,f66])).
% 0.10/0.60 fof(f94,plain,(
% 0.10/0.60 sQ9_spl|~sQ10_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f36,f85,f90])).
% 0.10/0.60 fof(f100,definition,(
% 0.10/0.60 sQ12_spl <=> (u_7)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f103,plain,(
% 0.10/0.60 sQ12_spl|sQ7_spl|~sQ9_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f39,f100,f77,f85])).
% 0.10/0.60 fof(f104,plain,(
% 0.10/0.60 sQ7_spl|~sQ12_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f40,f77,f100])).
% 0.10/0.60 fof(f115,definition,(
% 0.10/0.60 sQ15_spl <=> (u_10)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f118,plain,(
% 0.10/0.60 sQ15_spl|sQ4_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f45,f115,f66])).
% 0.10/0.60 fof(f119,plain,(
% 0.10/0.60 sQ4_spl|~sQ15_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f46,f66,f115])).
% 0.10/0.60 fof(f130,definition,(
% 0.10/0.60 sQ18_spl <=> (u_13)),
% 0.10/0.60 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.10/0.60 fof(f133,plain,(
% 0.10/0.60 sQ18_spl|sQ6_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f51,f130,f74])).
% 0.10/0.60 fof(f134,plain,(
% 0.10/0.60 sQ6_spl|~sQ18_spl),
% 0.10/0.60 inference(split_clause,[status(thm)],[f52,f74,f130])).
% 0.10/0.60 fof(f135,plain,(
% 0.10/0.60 $false|~sQ0_spl),
% 0.10/0.60 inference(forward_subsumption_resolution,[status(thm)],[f28,f54])).
% 0.10/0.60 fof(f136,plain,(
% 0.10/0.60 ~sQ0_spl),
% 0.10/0.60 inference(contradiction_clause,[status(thm)],[f135])).
% 0.10/0.60 fof(f137,plain,(
% 0.10/0.60 $false),
% 0.10/0.60 inference(sat_refutation,[status(thm)],[f59,f70,f80,f81,f93,f94,f103,f104,f118,f119,f133,f134,f136])).
% 0.10/0.60 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.62 % Elapsed time: 0.036054 seconds
% 0.10/0.62 % CPU time: 0.086988 seconds
% 0.10/0.62 % Total memory used: 11.074 MB
% 0.10/0.62 % Net memory used: 10.896 MB
%------------------------------------------------------------------------------