%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN686-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 : n012.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:21 PM UTC 2026
% Result : Unsatisfiable 0.08s 0.33s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN686-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 21 11:12:08 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 0.08/0.33 % Refutation found
% 0.08/0.33 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.08/0.33 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.33 fof(f1,negated_conjecture,(
% 0.08/0.33 (![X0]: (p11(X0,X0) ))),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f5,negated_conjecture,(
% 0.08/0.33 (![X81]: (p4(X81,X81) ))),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f12,negated_conjecture,(
% 0.08/0.33 (![X27]: (p2(X27,X27) ))),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f17,negated_conjecture,(
% 0.08/0.33 p3(c36,f7(c33,c34)) ),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f19,negated_conjecture,(
% 0.08/0.33 p4(f5(c32,c36),c37) ),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f20,negated_conjecture,(
% 0.08/0.33 p4(f5(c32,f7(c33,c34)),c35) ),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f21,negated_conjecture,(
% 0.08/0.33 p30(f10(f12(c39,c36),c37),c41) ),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f22,negated_conjecture,(
% 0.08/0.33 ~ p30(f10(f12(c39,f7(c33,c34)),c35),c41) ),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f27,negated_conjecture,(
% 0.08/0.33 (![X82,X83,X81]: (( p4(X82,X83)| ~ p4(X81,X82)| ~ p4(X81,X83) ) ))),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f39,negated_conjecture,(
% 0.08/0.33 (![X68,X69,X71,X70]: (( p30(X68,X69)| ~ p4(X71,X69)| ~ p9(X70,X68)| ~ p30(X70,X71) ) ))),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f41,negated_conjecture,(
% 0.08/0.33 (![X105,X106,X107,X108]: (( p9(f10(X105,X106),f10(X107,X108))| ~ p4(X106,X108)| ~ p8(X105,X107) ) ))),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f50,negated_conjecture,(
% 0.08/0.33 (![X84,X85,X86,X87]: (( p4(f5(X84,X85),f5(X86,X87))| ~ p2(X84,X86)| ~ p3(X85,X87) ) ))),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f51,negated_conjecture,(
% 0.08/0.33 (![X94,X95,X96,X97]: (( p8(f12(X94,X95),f12(X96,X97))| ~ p11(X94,X96)| ~ p3(X95,X97) ) ))),
% 0.08/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.33 fof(f59,plain,(
% 0.08/0.33 ![X0]: (p11(X0,X0))),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f1])).
% 0.08/0.33 fof(f63,plain,(
% 0.08/0.33 ![X0]: (p4(X0,X0))),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f5])).
% 0.08/0.33 fof(f70,plain,(
% 0.08/0.33 ![X0]: (p2(X0,X0))),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f12])).
% 0.08/0.33 fof(f75,plain,(
% 0.08/0.33 p3(c36,f7(c33,c34))),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f17])).
% 0.08/0.33 fof(f77,plain,(
% 0.08/0.33 p4(f5(c32,c36),c37)),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f19])).
% 0.08/0.33 fof(f78,plain,(
% 0.08/0.33 p4(f5(c32,f7(c33,c34)),c35)),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f20])).
% 0.08/0.33 fof(f79,plain,(
% 0.08/0.33 p30(f10(f12(c39,c36),c37),c41)),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f21])).
% 0.08/0.33 fof(f80,plain,(
% 0.08/0.33 ~p30(f10(f12(c39,f7(c33,c34)),c35),c41)),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f22])).
% 0.08/0.33 fof(f89,plain,(
% 0.08/0.33 ![X83,X81]: ((![X82]: (p4(X82,X83)|~p4(X81,X82)))|~p4(X81,X83))),
% 0.08/0.33 inference(miniscoping,[status(thm)],[f27])).
% 0.08/0.33 fof(f90,plain,(
% 0.08/0.33 ![X0,X1,X2]: (p4(X0,X1)|~p4(X2,X0)|~p4(X2,X1))),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f89])).
% 0.08/0.33 fof(f113,plain,(
% 0.08/0.33 ![X71,X70]: ((![X68]: ((![X69]: (p30(X68,X69)|~p4(X71,X69)))|~p9(X70,X68)))|~p30(X70,X71))),
% 0.08/0.33 inference(miniscoping,[status(thm)],[f39])).
% 0.08/0.33 fof(f114,plain,(
% 0.08/0.33 ![X0,X1,X2,X3]: (p30(X0,X1)|~p4(X2,X1)|~p9(X3,X0)|~p30(X3,X2))),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f113])).
% 0.08/0.33 fof(f117,plain,(
% 0.08/0.33 ![X105,X107]: ((![X106,X108]: (p9(f10(X105,X106),f10(X107,X108))|~p4(X106,X108)))|~p8(X105,X107))),
% 0.08/0.33 inference(miniscoping,[status(thm)],[f41])).
% 0.08/0.33 fof(f118,plain,(
% 0.08/0.33 ![X0,X1,X2,X3]: (p9(f10(X0,X1),f10(X2,X3))|~p4(X1,X3)|~p8(X0,X2))),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f117])).
% 0.08/0.33 fof(f135,plain,(
% 0.08/0.33 ![X85,X87]: ((![X84,X86]: (p4(f5(X84,X85),f5(X86,X87))|~p2(X84,X86)))|~p3(X85,X87))),
% 0.08/0.33 inference(miniscoping,[status(thm)],[f50])).
% 0.08/0.33 fof(f136,plain,(
% 0.08/0.33 ![X0,X1,X2,X3]: (p4(f5(X0,X1),f5(X2,X3))|~p2(X0,X2)|~p3(X1,X3))),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f135])).
% 0.08/0.33 fof(f137,plain,(
% 0.08/0.33 ![X95,X97]: ((![X94,X96]: (p8(f12(X94,X95),f12(X96,X97))|~p11(X94,X96)))|~p3(X95,X97))),
% 0.08/0.33 inference(miniscoping,[status(thm)],[f51])).
% 0.08/0.33 fof(f138,plain,(
% 0.08/0.33 ![X0,X1,X2,X3]: (p8(f12(X0,X1),f12(X2,X3))|~p11(X0,X2)|~p3(X1,X3))),
% 0.08/0.33 inference(cnf_transformation,[status(thm)],[f137])).
% 0.08/0.33 fof(f149,plain,(
% 0.08/0.33 ![X0,X1]: (p30(X0,X1)|~p4(c41,X1)|~p9(f10(f12(c39,c36),c37),X0))),
% 0.08/0.33 inference(resolution,[status(thm)],[f114,f79])).
% 0.08/0.33 fof(f151,plain,(
% 0.08/0.33 ![X0]: (p30(X0,c41)|~p9(f10(f12(c39,c36),c37),X0))),
% 0.08/0.33 inference(resolution,[status(thm)],[f149,f63])).
% 0.08/0.33 fof(f152,plain,(
% 0.08/0.33 ![X0,X1]: (p30(f10(X0,X1),c41)|~p4(c37,X1)|~p8(f12(c39,c36),X0))),
% 0.08/0.33 inference(resolution,[status(thm)],[f151,f118])).
% 0.08/0.33 fof(f155,plain,(
% 0.08/0.33 ~p4(c37,c35)|~p8(f12(c39,c36),f12(c39,f7(c33,c34)))),
% 0.08/0.33 inference(resolution,[status(thm)],[f152,f80])).
% 0.08/0.33 fof(f157,definition,(
% 0.08/0.33 sQ0_spl <=> (p4(c37,c35))),
% 0.08/0.33 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.08/0.33 fof(f159,plain,(
% 0.08/0.33 ~p4(c37,c35)|sQ0_spl),
% 0.08/0.33 inference(component_clause,[status(thm)],[f157])).
% 0.08/0.33 fof(f160,definition,(
% 0.08/0.33 sQ1_spl <=> (p8(f12(c39,c36),f12(c39,f7(c33,c34))))),
% 0.08/0.33 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.08/0.33 fof(f162,plain,(
% 0.08/0.33 ~p8(f12(c39,c36),f12(c39,f7(c33,c34)))|sQ1_spl),
% 0.08/0.33 inference(component_clause,[status(thm)],[f160])).
% 0.08/0.33 fof(f163,plain,(
% 0.08/0.33 ~sQ0_spl|~sQ1_spl),
% 0.08/0.33 inference(split_clause,[status(thm)],[f155,f157,f160])).
% 0.08/0.33 fof(f164,plain,(
% 0.08/0.33 ![X0]: (~p4(X0,c37)|~p4(X0,c35)|sQ0_spl)),
% 0.08/0.33 inference(resolution,[status(thm)],[f159,f90])).
% 0.08/0.33 fof(f165,plain,(
% 0.08/0.33 ~p4(f5(c32,f7(c33,c34)),c37)|sQ0_spl),
% 0.08/0.33 inference(resolution,[status(thm)],[f164,f78])).
% 0.08/0.33 fof(f177,plain,(
% 0.08/0.33 ![X0]: (~p4(X0,f5(c32,f7(c33,c34)))|~p4(X0,c37)|sQ0_spl)),
% 0.08/0.33 inference(resolution,[status(thm)],[f165,f90])).
% 0.08/0.33 fof(f183,plain,(
% 0.08/0.33 ~p4(f5(c32,c36),f5(c32,f7(c33,c34)))|sQ0_spl),
% 0.08/0.33 inference(resolution,[status(thm)],[f177,f77])).
% 0.08/0.33 fof(f195,plain,(
% 0.08/0.33 ~p2(c32,c32)|~p3(c36,f7(c33,c34))|sQ0_spl),
% 0.08/0.33 inference(resolution,[status(thm)],[f183,f136])).
% 0.08/0.33 fof(f197,definition,(
% 0.08/0.33 sQ4_spl <=> (p2(c32,c32))),
% 0.08/0.33 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.08/0.33 fof(f199,plain,(
% 0.08/0.33 ~p2(c32,c32)|sQ4_spl),
% 0.08/0.33 inference(component_clause,[status(thm)],[f197])).
% 0.08/0.33 fof(f200,definition,(
% 0.08/0.33 sQ5_spl <=> (p3(c36,f7(c33,c34)))),
% 0.08/0.33 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.08/0.33 fof(f202,plain,(
% 0.08/0.33 ~p3(c36,f7(c33,c34))|sQ5_spl),
% 0.08/0.33 inference(component_clause,[status(thm)],[f200])).
% 0.08/0.33 fof(f203,plain,(
% 0.08/0.33 ~sQ4_spl|~sQ5_spl|sQ0_spl),
% 0.08/0.33 inference(split_clause,[status(thm)],[f195,f197,f200,f157])).
% 0.08/0.33 fof(f204,plain,(
% 0.08/0.33 $false|sQ5_spl),
% 0.08/0.33 inference(forward_subsumption_resolution,[status(thm)],[f202,f75])).
% 0.08/0.33 fof(f205,plain,(
% 0.08/0.33 sQ5_spl),
% 0.08/0.33 inference(contradiction_clause,[status(thm)],[f204])).
% 0.08/0.33 fof(f206,plain,(
% 0.08/0.33 $false|sQ4_spl),
% 0.08/0.33 inference(forward_subsumption_resolution,[status(thm)],[f199,f70])).
% 0.08/0.33 fof(f207,plain,(
% 0.08/0.33 sQ4_spl),
% 0.08/0.33 inference(contradiction_clause,[status(thm)],[f206])).
% 0.08/0.33 fof(f211,plain,(
% 0.08/0.33 ~p11(c39,c39)|~p3(c36,f7(c33,c34))|sQ1_spl),
% 0.08/0.33 inference(resolution,[status(thm)],[f162,f138])).
% 0.08/0.33 fof(f213,definition,(
% 0.08/0.33 sQ6_spl <=> (p11(c39,c39))),
% 0.08/0.33 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.08/0.33 fof(f215,plain,(
% 0.08/0.33 ~p11(c39,c39)|sQ6_spl),
% 0.08/0.33 inference(component_clause,[status(thm)],[f213])).
% 0.08/0.33 fof(f216,plain,(
% 0.08/0.33 ~sQ6_spl|~sQ5_spl|sQ1_spl),
% 0.08/0.33 inference(split_clause,[status(thm)],[f211,f213,f200,f160])).
% 0.08/0.33 fof(f217,plain,(
% 0.08/0.33 $false|sQ6_spl),
% 0.08/0.33 inference(forward_subsumption_resolution,[status(thm)],[f215,f59])).
% 0.08/0.33 fof(f218,plain,(
% 0.08/0.33 sQ6_spl),
% 0.08/0.33 inference(contradiction_clause,[status(thm)],[f217])).
% 0.08/0.33 fof(f219,plain,(
% 0.08/0.33 $false),
% 0.08/0.33 inference(sat_refutation,[status(thm)],[f163,f203,f205,f207,f216,f218])).
% 0.08/0.33 % SZS output end CNFRefutation for theBenchmark.p
% 0.08/0.34 % Elapsed time: 0.035429 seconds
% 0.08/0.34 % CPU time: 0.064836 seconds
% 0.08/0.34 % Total memory used: 19.316 MB
% 0.08/0.34 % Net memory used: 19.214 MB
%------------------------------------------------------------------------------