%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN627-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 : n011.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.14s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN627-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/0.36 % Computer : n011.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 11:10:40 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.40 fof(f5,negated_conjecture,(
% 0.14/0.40 (![X40]: (p3(X40,X40) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f6,negated_conjecture,(
% 0.14/0.40 (![X33]: (p2(X33,X33) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f7,negated_conjecture,(
% 0.14/0.40 p15(c18,c19) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f8,negated_conjecture,(
% 0.14/0.40 ~ p3(c23,c24) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f9,negated_conjecture,(
% 0.14/0.40 p3(c23,f4(f7(c17,c18),c21)) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f10,negated_conjecture,(
% 0.14/0.40 p16(c17,c20,f9(c19,c18),c21,c22) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f18,negated_conjecture,(
% 0.14/0.40 (![X41,X42,X40]: (( p3(X41,X42)| ~ p3(X40,X41)| ~ p3(X40,X42) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f20,negated_conjecture,(
% 0.14/0.40 (![X32]: (( p3(c24,f4(f7(c17,X32),f14(X32)))| ~ p15(X32,c19) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f22,negated_conjecture,(
% 0.14/0.40 (![X31]: (( p16(c17,c20,f9(c19,X31),f13(X31),c22)| ~ p15(X31,c19) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f23,negated_conjecture,(
% 0.14/0.40 (![X32]: (( p16(c17,c20,f9(c19,X32),f14(X32),c25)| ~ p15(X32,c19) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f27,negated_conjecture,(
% 0.14/0.40 (![X57,X58,X59,X60]: (( p3(f4(X57,X58),f4(X59,X60))| ~ p2(X57,X59)| ~ p3(X58,X60) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f28,negated_conjecture,(
% 0.14/0.40 (![X5,X6,X4,X3]: (( p3(X5,X6)| ~ p16(c17,c20,X4,X6,X3)| ~ p16(c17,c20,X4,X5,c22) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f41,plain,(
% 0.14/0.40 ![X0]: (p3(X0,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.40 fof(f42,plain,(
% 0.14/0.40 ![X0]: (p2(X0,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/0.40 fof(f43,plain,(
% 0.14/0.40 p15(c18,c19)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/0.40 fof(f44,plain,(
% 0.14/0.40 ~p3(c23,c24)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.40 fof(f45,plain,(
% 0.14/0.40 p3(c23,f4(f7(c17,c18),c21))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f9])).
% 0.14/0.40 fof(f46,plain,(
% 0.14/0.40 p16(c17,c20,f9(c19,c18),c21,c22)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f10])).
% 0.14/0.40 fof(f58,plain,(
% 0.14/0.40 ![X42,X40]: ((![X41]: (p3(X41,X42)|~p3(X40,X41)))|~p3(X40,X42))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f18])).
% 0.14/0.40 fof(f59,plain,(
% 0.14/0.40 ![X0,X1,X2]: (p3(X0,X1)|~p3(X2,X0)|~p3(X2,X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f58])).
% 0.14/0.40 fof(f62,plain,(
% 0.14/0.40 ![X0]: (p3(c24,f4(f7(c17,X0),f14(X0)))|~p15(X0,c19))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f20])).
% 0.14/0.40 fof(f64,plain,(
% 0.14/0.40 ![X0]: (p16(c17,c20,f9(c19,X0),f13(X0),c22)|~p15(X0,c19))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/0.40 fof(f65,plain,(
% 0.14/0.40 ![X0]: (p16(c17,c20,f9(c19,X0),f14(X0),c25)|~p15(X0,c19))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f23])).
% 0.14/0.40 fof(f72,plain,(
% 0.14/0.40 ![X58,X60]: ((![X57,X59]: (p3(f4(X57,X58),f4(X59,X60))|~p2(X57,X59)))|~p3(X58,X60))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f27])).
% 0.14/0.40 fof(f73,plain,(
% 0.14/0.40 ![X0,X1,X2,X3]: (p3(f4(X0,X1),f4(X2,X3))|~p2(X0,X2)|~p3(X1,X3))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/0.40 fof(f74,plain,(
% 0.14/0.40 ![X5,X4]: ((![X6]: (p3(X5,X6)|(![X3]: ~p16(c17,c20,X4,X6,X3))))|~p16(c17,c20,X4,X5,c22))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f28])).
% 0.14/0.40 fof(f75,plain,(
% 0.14/0.40 ![X0,X1,X2,X3]: (p3(X0,X1)|~p16(c17,c20,X2,X1,X3)|~p16(c17,c20,X2,X0,c22))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f74])).
% 0.14/0.40 fof(f99,plain,(
% 0.14/0.40 ![X0]: (~p3(X0,c23)|~p3(X0,c24))),
% 0.14/0.40 inference(resolution,[status(thm)],[f59,f44])).
% 0.14/0.40 fof(f100,plain,(
% 0.14/0.40 ![X0,X1]: (~p3(X0,c24)|~p3(X1,X0)|~p3(X1,c23))),
% 0.14/0.40 inference(resolution,[status(thm)],[f99,f59])).
% 0.14/0.40 fof(f103,plain,(
% 0.14/0.40 ![X0]: (~p3(X0,c24)|~p3(c23,X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f100,f41])).
% 0.14/0.40 fof(f104,plain,(
% 0.14/0.40 ![X0,X1]: (~p3(c23,X0)|~p3(X1,X0)|~p3(X1,c24))),
% 0.14/0.40 inference(resolution,[status(thm)],[f103,f59])).
% 0.14/0.40 fof(f106,plain,(
% 0.14/0.40 ![X0,X1,X2]: (~p3(c23,X0)|~p3(X1,X0)|~p3(X2,X1)|~p3(X2,c24))),
% 0.14/0.40 inference(resolution,[status(thm)],[f104,f59])).
% 0.14/0.40 fof(f114,plain,(
% 0.14/0.40 ![X0,X1,X2]: (p3(f13(X0),X1)|~p16(c17,c20,f9(c19,X0),X1,X2)|~p15(X0,c19))),
% 0.14/0.40 inference(resolution,[status(thm)],[f75,f64])).
% 0.14/0.40 fof(f120,plain,(
% 0.14/0.40 ![X0,X1]: (~p3(c23,X0)|~p3(X1,X0)|~p3(c24,X1))),
% 0.14/0.40 inference(resolution,[status(thm)],[f106,f41])).
% 0.14/0.40 fof(f121,plain,(
% 0.14/0.40 ![X0,X1]: (~p3(c23,X0)|~p3(f4(f7(c17,X1),f14(X1)),X0)|~p15(X1,c19))),
% 0.14/0.40 inference(resolution,[status(thm)],[f120,f62])).
% 0.14/0.40 fof(f136,definition,(
% 0.14/0.40 sQ3_spl <=> (p15(c18,c19))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f138,plain,(
% 0.14/0.40 ~p15(c18,c19)|sQ3_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f136])).
% 0.14/0.40 fof(f144,plain,(
% 0.14/0.40 $false|sQ3_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f138,f43])).
% 0.14/0.40 fof(f145,plain,(
% 0.14/0.40 sQ3_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f144])).
% 0.14/0.40 fof(f180,plain,(
% 0.14/0.40 ![X0]: (~p3(c23,X0)|~p3(f4(f7(c17,c18),f14(c18)),X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f121,f43])).
% 0.14/0.40 fof(f182,plain,(
% 0.14/0.40 ![X0,X1]: (~p3(c23,f4(X0,X1))|~p2(f7(c17,c18),X0)|~p3(f14(c18),X1))),
% 0.14/0.40 inference(resolution,[status(thm)],[f180,f73])).
% 0.14/0.40 fof(f196,plain,(
% 0.14/0.40 ![X0,X1]: (p3(f13(c18),X0)|~p16(c17,c20,f9(c19,c18),X0,X1))),
% 0.14/0.40 inference(resolution,[status(thm)],[f114,f43])).
% 0.14/0.40 fof(f203,plain,(
% 0.14/0.40 p3(f13(c18),c21)),
% 0.14/0.40 inference(resolution,[status(thm)],[f196,f46])).
% 0.14/0.40 fof(f204,plain,(
% 0.14/0.40 p3(f13(c18),f14(c18))|~p15(c18,c19)),
% 0.14/0.40 inference(resolution,[status(thm)],[f196,f65])).
% 0.14/0.40 fof(f206,definition,(
% 0.14/0.40 sQ7_spl <=> (p3(f13(c18),f14(c18)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f207,plain,(
% 0.14/0.40 p3(f13(c18),f14(c18))|~sQ7_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f206])).
% 0.14/0.40 fof(f209,plain,(
% 0.14/0.40 sQ7_spl|~sQ3_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f204,f206,f136])).
% 0.14/0.40 fof(f216,plain,(
% 0.14/0.40 ~p2(f7(c17,c18),f7(c17,c18))|~p3(f14(c18),c21)),
% 0.14/0.40 inference(resolution,[status(thm)],[f182,f45])).
% 0.14/0.40 fof(f219,definition,(
% 0.14/0.40 sQ9_spl <=> (p2(f7(c17,c18),f7(c17,c18)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f221,plain,(
% 0.14/0.40 ~p2(f7(c17,c18),f7(c17,c18))|sQ9_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f219])).
% 0.14/0.40 fof(f222,definition,(
% 0.14/0.40 sQ10_spl <=> (p3(f14(c18),c21))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f224,plain,(
% 0.14/0.40 ~p3(f14(c18),c21)|sQ10_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f222])).
% 0.14/0.40 fof(f225,plain,(
% 0.14/0.40 ~sQ9_spl|~sQ10_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f216,f219,f222])).
% 0.14/0.40 fof(f226,plain,(
% 0.14/0.40 $false|sQ9_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f221,f42])).
% 0.14/0.40 fof(f227,plain,(
% 0.14/0.40 sQ9_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f226])).
% 0.14/0.40 fof(f228,plain,(
% 0.14/0.40 ![X0]: (~p3(X0,f14(c18))|~p3(X0,c21)|sQ10_spl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f224,f59])).
% 0.14/0.40 fof(f229,plain,(
% 0.14/0.40 ~p3(f13(c18),f14(c18))|sQ10_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f228,f203])).
% 0.14/0.40 fof(f232,plain,(
% 0.14/0.40 $false|~sQ7_spl|sQ10_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f229,f207])).
% 0.14/0.40 fof(f233,plain,(
% 0.14/0.40 ~sQ7_spl|sQ10_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f232])).
% 0.14/0.40 fof(f234,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(sat_refutation,[status(thm)],[f145,f209,f225,f227,f233])).
% 0.14/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.42 % Elapsed time: 0.051213 seconds
% 0.14/0.42 % CPU time: 0.190156 seconds
% 0.14/0.42 % Total memory used: 19.574 MB
% 0.14/0.42 % Net memory used: 19.240 MB
%------------------------------------------------------------------------------