%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN718-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 : n008.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.13s 5.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN718-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.36 % Computer : n008.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Mon Sep 21 11:14:01 UTC 2026
% 0.08/5.36 % CPUTime :
% 0.08/5.38 % Drodi V4.1.1
% 0.13/5.86 % Refutation found
% 0.13/5.86 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/5.86 % SZS output start CNFRefutation for theBenchmark
% 0.13/5.86 fof(f23,negated_conjecture,(
% 0.13/5.86 (![X58]: (p25(X58,X58) ))),
% 0.13/5.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.86 fof(f26,negated_conjecture,(
% 0.13/5.86 (![X41]: (p20(X41,X41) ))),
% 0.13/5.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.86 fof(f36,negated_conjecture,(
% 0.13/5.86 p3(c84,f10(c72,c73)) ),
% 0.13/5.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.86 fof(f72,negated_conjecture,(
% 0.13/5.86 (![X197,X198,X199]: (( p57(f26(f30(c85,X197),X198),X199)| ~ p57(f26(X197,X198),X199) ) ))),
% 0.13/5.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.86 fof(f76,negated_conjecture,(
% 0.13/5.86 (![X193,X194,X196,X195]: (( p57(X193,X194)| ~ p25(X196,X193)| ~ p57(X196,X195)| ~ p21(X195,X194) ) ))),
% 0.13/5.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.86 fof(f80,negated_conjecture,(
% 0.13/5.86 p57(f26(c70,f22(f24(c71,c81),c82)),f22(f24(c71,c83),c84)) ),
% 0.13/5.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.86 fof(f81,negated_conjecture,(
% 0.13/5.86 p57(f26(c70,f22(f24(c71,c79),c80)),f22(f24(c71,c81),c82)) ),
% 0.13/5.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.86 fof(f101,negated_conjecture,(
% 0.13/5.86 (![X51,X52,X53,X54]: (( p21(f22(X51,X52),f22(X53,X54))| ~ p20(X51,X53)| ~ p3(X52,X54) ) ))),
% 0.13/5.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.86 fof(f105,negated_conjecture,(
% 0.13/5.86 ~ p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),f22(f24(c71,c83),f10(c72,c73))) ),
% 0.13/5.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.86 fof(f107,negated_conjecture,(
% 0.13/5.86 (![X200,X201,X202,X203]: (( p57(f26(f30(c85,X200),X201),X202)| ~ p57(f26(f30(c85,X200),X201),X203)| ~ p57(f26(f30(c85,X200),X203),X202) ) ))),
% 0.13/5.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.86 fof(f141,plain,(
% 0.13/5.86 ![X0]: (p25(X0,X0))),
% 0.13/5.86 inference(cnf_transformation,[status(thm)],[f23])).
% 0.13/5.86 fof(f144,plain,(
% 0.13/5.86 ![X0]: (p20(X0,X0))),
% 0.13/5.86 inference(cnf_transformation,[status(thm)],[f26])).
% 0.13/5.86 fof(f154,plain,(
% 0.13/5.86 p3(c84,f10(c72,c73))),
% 0.13/5.86 inference(cnf_transformation,[status(thm)],[f36])).
% 0.13/5.86 fof(f222,plain,(
% 0.13/5.86 ![X0,X1,X2]: (p57(f26(f30(c85,X0),X1),X2)|~p57(f26(X0,X1),X2))),
% 0.13/5.86 inference(cnf_transformation,[status(thm)],[f72])).
% 0.13/5.86 fof(f229,plain,(
% 0.13/5.86 ![X194,X195]: ((![X196]: ((![X193]: (p57(X193,X194)|~p25(X196,X193)))|~p57(X196,X195)))|~p21(X195,X194))),
% 0.13/5.86 inference(miniscoping,[status(thm)],[f76])).
% 0.13/5.86 fof(f230,plain,(
% 0.13/5.86 ![X0,X1,X2,X3]: (p57(X0,X1)|~p25(X2,X0)|~p57(X2,X3)|~p21(X3,X1))),
% 0.13/5.86 inference(cnf_transformation,[status(thm)],[f229])).
% 0.13/5.86 fof(f237,plain,(
% 0.13/5.86 p57(f26(c70,f22(f24(c71,c81),c82)),f22(f24(c71,c83),c84))),
% 0.13/5.86 inference(cnf_transformation,[status(thm)],[f80])).
% 0.13/5.86 fof(f238,plain,(
% 0.13/5.86 p57(f26(c70,f22(f24(c71,c79),c80)),f22(f24(c71,c81),c82))),
% 0.13/5.86 inference(cnf_transformation,[status(thm)],[f81])).
% 0.13/5.86 fof(f276,plain,(
% 0.13/5.86 ![X52,X54]: ((![X51,X53]: (p21(f22(X51,X52),f22(X53,X54))|~p20(X51,X53)))|~p3(X52,X54))),
% 0.13/5.86 inference(miniscoping,[status(thm)],[f101])).
% 0.13/5.86 fof(f277,plain,(
% 0.13/5.86 ![X0,X1,X2,X3]: (p21(f22(X0,X1),f22(X2,X3))|~p20(X0,X2)|~p3(X1,X3))),
% 0.13/5.86 inference(cnf_transformation,[status(thm)],[f276])).
% 0.13/5.86 fof(f284,plain,(
% 0.13/5.86 ~p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),f22(f24(c71,c83),f10(c72,c73)))),
% 0.13/5.86 inference(cnf_transformation,[status(thm)],[f105])).
% 0.13/5.86 fof(f287,plain,(
% 0.13/5.86 ![X200,X202,X203]: ((![X201]: (p57(f26(f30(c85,X200),X201),X202)|~p57(f26(f30(c85,X200),X201),X203)))|~p57(f26(f30(c85,X200),X203),X202))),
% 0.13/5.86 inference(miniscoping,[status(thm)],[f107])).
% 0.13/5.86 fof(f288,plain,(
% 0.13/5.86 ![X0,X1,X2,X3]: (p57(f26(f30(c85,X0),X1),X2)|~p57(f26(f30(c85,X0),X1),X3)|~p57(f26(f30(c85,X0),X3),X2))),
% 0.13/5.86 inference(cnf_transformation,[status(thm)],[f287])).
% 0.13/5.86 fof(f482,plain,(
% 0.13/5.86 ![X0,X1,X2]: (p57(X0,X1)|~p57(X0,X2)|~p21(X2,X1))),
% 0.13/5.86 inference(resolution,[status(thm)],[f230,f141])).
% 0.13/5.86 fof(f496,plain,(
% 0.13/5.86 p57(f26(f30(c85,c70),f22(f24(c71,c81),c82)),f22(f24(c71,c83),c84))),
% 0.13/5.86 inference(resolution,[status(thm)],[f237,f222])).
% 0.13/5.86 fof(f500,plain,(
% 0.13/5.86 p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),f22(f24(c71,c81),c82))),
% 0.13/5.86 inference(resolution,[status(thm)],[f238,f222])).
% 0.13/5.86 fof(f559,plain,(
% 0.13/5.86 ![X0,X1,X2]: (p21(f22(X0,X1),f22(X0,X2))|~p3(X1,X2))),
% 0.13/5.88 inference(resolution,[status(thm)],[f277,f144])).
% 0.13/5.88 fof(f740,plain,(
% 0.13/5.88 ![X0]: (p57(f26(f30(c85,c70),X0),f22(f24(c71,c83),c84))|~p57(f26(f30(c85,c70),X0),f22(f24(c71,c81),c82)))),
% 0.13/5.88 inference(resolution,[status(thm)],[f496,f288])).
% 0.13/5.88 fof(f808,plain,(
% 0.13/5.88 ![X0]: (p21(f22(X0,c84),f22(X0,f10(c72,c73))))),
% 0.13/5.88 inference(resolution,[status(thm)],[f559,f154])).
% 0.13/5.88 fof(f1126,plain,(
% 0.13/5.88 p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),f22(f24(c71,c83),c84))),
% 0.13/5.88 inference(resolution,[status(thm)],[f740,f500])).
% 0.13/5.88 fof(f1295,plain,(
% 0.13/5.88 ![X0,X1]: (p57(X0,f22(X1,f10(c72,c73)))|~p57(X0,f22(X1,c84)))),
% 0.13/5.88 inference(resolution,[status(thm)],[f808,f482])).
% 0.13/5.88 fof(f2492,plain,(
% 0.13/5.88 p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),f22(f24(c71,c83),f10(c72,c73)))),
% 0.13/5.88 inference(resolution,[status(thm)],[f1295,f1126])).
% 0.13/5.88 fof(f2495,plain,(
% 0.13/5.88 $false),
% 0.13/5.88 inference(forward_subsumption_resolution,[status(thm)],[f2492,f284])).
% 0.13/5.88 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.89 % Elapsed time: 0.520483 seconds
% 0.13/5.89 % CPU time: 3.910395 seconds
% 0.13/5.89 % Total memory used: 107.613 MB
% 0.13/5.89 % Net memory used: 95.647 MB
%------------------------------------------------------------------------------