%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN717-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 : n019.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:24 PM UTC 2026
% Result : Unsatisfiable 0.11s 5.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN717-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/5.53 % Computer : n019.cluster.edu
% 0.11/5.53 % Model : x86_64 x86_64
% 0.11/5.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.53 % Memory : 8046.5625MB
% 0.11/5.53 % OS : Linux 6.8.0-71-generic
% 0.11/5.53 % CPULimit : 300
% 0.11/5.53 % WCLimit : 300
% 0.11/5.53 % DateTime : Mon Sep 21 11:13:42 UTC 2026
% 0.11/5.53 % CPUTime :
% 0.11/5.54 % Drodi V4.1.1
% 0.11/5.56 % Refutation found
% 0.11/5.56 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.11/5.56 % SZS output start CNFRefutation for theBenchmark
% 0.11/5.56 fof(f28,negated_conjecture,(
% 0.11/5.56 (![X55]: (p22(X55,X55) ))),
% 0.11/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/5.56 fof(f29,negated_conjecture,(
% 0.11/5.56 (![X48]: (p20(X48,X48) ))),
% 0.11/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/5.56 fof(f36,negated_conjecture,(
% 0.11/5.56 p23(c79,c77) ),
% 0.11/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/5.56 fof(f42,negated_conjecture,(
% 0.11/5.56 p60(f25(c75,c79),f21(c76,c78)) ),
% 0.11/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/5.56 fof(f44,negated_conjecture,(
% 0.11/5.56 p59(f29(c73,f31(f33(c74,c77),c78)),c72) ),
% 0.11/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/5.56 fof(f84,negated_conjecture,(
% 0.11/5.56 (![X186,X187,X189,X188]: (( p60(X186,X187)| ~ p24(X189,X186)| ~ p60(X189,X188)| ~ p20(X188,X187) ) ))),
% 0.11/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/5.56 fof(f94,negated_conjecture,(
% 0.11/5.56 (![X68,X69,X70,X71]: (( p24(f25(X68,X69),f25(X70,X71))| ~ p22(X68,X70)| ~ p23(X69,X71) ) ))),
% 0.11/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/5.56 fof(f107,negated_conjecture,(
% 0.11/5.56 (![X209,X212,X211,X210]: (( ~ p60(f25(c75,X209),f21(c76,X212))| ~ p59(f29(c73,f31(f33(c74,X211),X212)),c72)| ~ p59(f29(c73,f31(f33(c74,X209),X210)),c72) ) ))),
% 0.11/5.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/5.56 fof(f141,plain,(
% 0.11/5.56 ![X0]: (p22(X0,X0))),
% 0.11/5.56 inference(cnf_transformation,[status(thm)],[f28])).
% 0.11/5.56 fof(f142,plain,(
% 0.11/5.56 ![X0]: (p20(X0,X0))),
% 0.11/5.56 inference(cnf_transformation,[status(thm)],[f29])).
% 0.11/5.56 fof(f149,plain,(
% 0.11/5.56 p23(c79,c77)),
% 0.11/5.56 inference(cnf_transformation,[status(thm)],[f36])).
% 0.11/5.56 fof(f155,plain,(
% 0.11/5.56 p60(f25(c75,c79),f21(c76,c78))),
% 0.11/5.56 inference(cnf_transformation,[status(thm)],[f42])).
% 0.11/5.56 fof(f157,plain,(
% 0.11/5.56 p59(f29(c73,f31(f33(c74,c77),c78)),c72)),
% 0.11/5.56 inference(cnf_transformation,[status(thm)],[f44])).
% 0.11/5.56 fof(f234,plain,(
% 0.11/5.56 ![X187,X188]: ((![X189]: ((![X186]: (p60(X186,X187)|~p24(X189,X186)))|~p60(X189,X188)))|~p20(X188,X187))),
% 0.11/5.56 inference(miniscoping,[status(thm)],[f84])).
% 0.11/5.56 fof(f235,plain,(
% 0.11/5.56 ![X0,X1,X2,X3]: (p60(X0,X1)|~p24(X2,X0)|~p60(X2,X3)|~p20(X3,X1))),
% 0.11/5.56 inference(cnf_transformation,[status(thm)],[f234])).
% 0.11/5.56 fof(f254,plain,(
% 0.11/5.56 ![X69,X71]: ((![X68,X70]: (p24(f25(X68,X69),f25(X70,X71))|~p22(X68,X70)))|~p23(X69,X71))),
% 0.11/5.56 inference(miniscoping,[status(thm)],[f94])).
% 0.11/5.56 fof(f255,plain,(
% 0.11/5.56 ![X0,X1,X2,X3]: (p24(f25(X0,X1),f25(X2,X3))|~p22(X0,X2)|~p23(X1,X3))),
% 0.11/5.56 inference(cnf_transformation,[status(thm)],[f254])).
% 0.11/5.56 fof(f280,plain,(
% 0.11/5.56 ![X209]: ((![X212]: (~p60(f25(c75,X209),f21(c76,X212))|(![X211]: ~p59(f29(c73,f31(f33(c74,X211),X212)),c72))))|(![X210]: ~p59(f29(c73,f31(f33(c74,X209),X210)),c72)))),
% 0.11/5.56 inference(miniscoping,[status(thm)],[f107])).
% 0.11/5.56 fof(f281,plain,(
% 0.11/5.56 ![X0,X1,X2,X3]: (~p60(f25(c75,X0),f21(c76,X1))|~p59(f29(c73,f31(f33(c74,X2),X1)),c72)|~p59(f29(c73,f31(f33(c74,X0),X3)),c72))),
% 0.11/5.56 inference(cnf_transformation,[status(thm)],[f280])).
% 0.11/5.56 fof(f338,plain,(
% 0.11/5.56 ~p60(f25(c75,c77),f21(c76,c78))),
% 0.11/5.56 inference(resolution,[status(thm)],[f281,f157])).
% 0.11/5.56 fof(f344,plain,(
% 0.11/5.57 ![X0,X1]: (~p24(X0,f25(c75,c77))|~p60(X0,X1)|~p20(X1,f21(c76,c78)))),
% 0.11/5.57 inference(resolution,[status(thm)],[f338,f235])).
% 0.11/5.57 fof(f400,plain,(
% 0.11/5.57 ~p24(f25(c75,c79),f25(c75,c77))|~p20(f21(c76,c78),f21(c76,c78))),
% 0.11/5.57 inference(resolution,[status(thm)],[f344,f155])).
% 0.11/5.57 fof(f402,definition,(
% 0.11/5.57 sQ0_spl <=> (p24(f25(c75,c79),f25(c75,c77)))),
% 0.11/5.57 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.11/5.57 fof(f404,plain,(
% 0.11/5.57 ~p24(f25(c75,c79),f25(c75,c77))|sQ0_spl),
% 0.11/5.57 inference(component_clause,[status(thm)],[f402])).
% 0.11/5.57 fof(f405,definition,(
% 0.11/5.57 sQ1_spl <=> (p20(f21(c76,c78),f21(c76,c78)))),
% 0.11/5.57 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.11/5.57 fof(f407,plain,(
% 0.11/5.57 ~p20(f21(c76,c78),f21(c76,c78))|sQ1_spl),
% 0.11/5.57 inference(component_clause,[status(thm)],[f405])).
% 0.11/5.57 fof(f408,plain,(
% 0.11/5.57 ~sQ0_spl|~sQ1_spl),
% 0.11/5.57 inference(split_clause,[status(thm)],[f400,f402,f405])).
% 0.11/5.57 fof(f409,plain,(
% 0.11/5.57 ~p22(c75,c75)|~p23(c79,c77)|sQ0_spl),
% 0.11/5.57 inference(resolution,[status(thm)],[f404,f255])).
% 0.11/5.57 fof(f411,definition,(
% 0.11/5.57 sQ2_spl <=> (p22(c75,c75))),
% 0.11/5.57 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.11/5.57 fof(f413,plain,(
% 0.11/5.57 ~p22(c75,c75)|sQ2_spl),
% 0.11/5.57 inference(component_clause,[status(thm)],[f411])).
% 0.11/5.57 fof(f414,definition,(
% 0.11/5.57 sQ3_spl <=> (p23(c79,c77))),
% 0.11/5.57 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.11/5.57 fof(f416,plain,(
% 0.11/5.57 ~p23(c79,c77)|sQ3_spl),
% 0.11/5.57 inference(component_clause,[status(thm)],[f414])).
% 0.11/5.57 fof(f417,plain,(
% 0.11/5.57 ~sQ2_spl|~sQ3_spl|sQ0_spl),
% 0.11/5.57 inference(split_clause,[status(thm)],[f409,f411,f414,f402])).
% 0.11/5.57 fof(f418,plain,(
% 0.11/5.57 $false|sQ1_spl),
% 0.11/5.57 inference(forward_subsumption_resolution,[status(thm)],[f407,f142])).
% 0.11/5.57 fof(f419,plain,(
% 0.11/5.57 sQ1_spl),
% 0.11/5.57 inference(contradiction_clause,[status(thm)],[f418])).
% 0.11/5.57 fof(f420,plain,(
% 0.11/5.57 $false|sQ2_spl),
% 0.11/5.57 inference(forward_subsumption_resolution,[status(thm)],[f413,f141])).
% 0.11/5.57 fof(f421,plain,(
% 0.11/5.57 sQ2_spl),
% 0.11/5.57 inference(contradiction_clause,[status(thm)],[f420])).
% 0.11/5.57 fof(f422,plain,(
% 0.11/5.57 $false|sQ3_spl),
% 0.11/5.57 inference(forward_subsumption_resolution,[status(thm)],[f416,f149])).
% 0.11/5.57 fof(f423,plain,(
% 0.11/5.57 sQ3_spl),
% 0.11/5.57 inference(contradiction_clause,[status(thm)],[f422])).
% 0.11/5.57 fof(f424,plain,(
% 0.11/5.57 $false),
% 0.11/5.57 inference(sat_refutation,[status(thm)],[f408,f417,f419,f421,f423])).
% 0.11/5.57 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/5.59 % Elapsed time: 0.050636 seconds
% 0.11/5.59 % CPU time: 0.201693 seconds
% 0.11/5.59 % Total memory used: 17.819 MB
% 0.11/5.59 % Net memory used: 17.638 MB
%------------------------------------------------------------------------------