%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN691-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 : n020.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.13s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN691-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 11:13:02 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.39 % Refutation found
% 0.13/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.39 fof(f15,negated_conjecture,(
% 0.13/0.39 (![X37]: (p22(X37,X37) ))),
% 0.13/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f17,negated_conjecture,(
% 0.13/0.39 (![X31]: (p2(X31,X31) ))),
% 0.13/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f43,negated_conjecture,(
% 0.13/0.39 ~ p39(f5(c40,f10(f13(f15(c42,c43),c44),c45)),c46) ),
% 0.13/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f44,negated_conjecture,(
% 0.13/0.39 (![X47,X50,X48,X49]: (( p39(X47,X50)| ~ p39(f17(f19(f21(c47,X47),X48),X49),X50) ) ))),
% 0.13/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f45,negated_conjecture,(
% 0.13/0.39 (![X107,X108,X110,X109]: (( p39(X107,X108)| ~ p39(X110,X109)| ~ p4(X110,X107)| ~ p22(X109,X108) ) ))),
% 0.13/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f46,negated_conjecture,(
% 0.13/0.39 p39(f5(c40,f7(c41,f10(f13(f15(c42,c43),c44),c45))),c46) ),
% 0.13/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f50,negated_conjecture,(
% 0.13/0.39 (![X118,X119,X120,X121]: (( p4(f5(X118,X119),f5(X120,X121))| ~ p2(X118,X120)| ~ p3(X119,X121) ) ))),
% 0.13/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f63,negated_conjecture,(
% 0.13/0.39 (![X103,X104,X105,X106]: (( p39(X103,X104)| ~ p39(f5(c40,f10(f13(f15(c42,X103),X105),X106)),X104) ) ))),
% 0.13/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f64,negated_conjecture,(
% 0.13/0.39 (![X103,X105,X106,X104]: (( p39(f5(c40,f10(f13(f15(c42,X103),X105),X106)),X104)| ~ p39(X103,X104) ) ))),
% 0.13/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f67,negated_conjecture,(
% 0.13/0.39 (![X47,X48,X49]: (p3(f7(c41,f10(f13(f15(c42,X47),X48),X49)),f10(f13(f15(c42,f17(f19(f21(c47,X47),X48),X49)),f26(f28(f30(c48,X47),X48),X49)),f34(f36(f38(c49,X47),X48),X49))) ))),
% 0.13/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f82,plain,(
% 0.13/0.39 ![X0]: (p22(X0,X0))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.39 fof(f84,plain,(
% 0.13/0.39 ![X0]: (p2(X0,X0))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.39 fof(f131,plain,(
% 0.13/0.39 ~p39(f5(c40,f10(f13(f15(c42,c43),c44),c45)),c46)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f43])).
% 0.13/0.39 fof(f132,plain,(
% 0.13/0.39 ![X47,X50]: (p39(X47,X50)|(![X48,X49]: ~p39(f17(f19(f21(c47,X47),X48),X49),X50)))),
% 0.13/0.39 inference(miniscoping,[status(thm)],[f44])).
% 0.13/0.39 fof(f133,plain,(
% 0.13/0.39 ![X0,X1,X2,X3]: (p39(X0,X1)|~p39(f17(f19(f21(c47,X0),X2),X3),X1))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f132])).
% 0.13/0.39 fof(f134,plain,(
% 0.13/0.39 ![X108,X109]: ((![X107,X110]: ((p39(X107,X108)|~p39(X110,X109))|~p4(X110,X107)))|~p22(X109,X108))),
% 0.13/0.39 inference(miniscoping,[status(thm)],[f45])).
% 0.13/0.39 fof(f135,plain,(
% 0.13/0.39 ![X0,X1,X2,X3]: (p39(X0,X1)|~p39(X2,X3)|~p4(X2,X0)|~p22(X3,X1))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f134])).
% 0.13/0.39 fof(f136,plain,(
% 0.13/0.39 p39(f5(c40,f7(c41,f10(f13(f15(c42,c43),c44),c45))),c46)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f46])).
% 0.13/0.39 fof(f143,plain,(
% 0.13/0.39 ![X119,X121]: ((![X118,X120]: (p4(f5(X118,X119),f5(X120,X121))|~p2(X118,X120)))|~p3(X119,X121))),
% 0.13/0.39 inference(miniscoping,[status(thm)],[f50])).
% 0.13/0.39 fof(f144,plain,(
% 0.13/0.39 ![X0,X1,X2,X3]: (p4(f5(X0,X1),f5(X2,X3))|~p2(X0,X2)|~p3(X1,X3))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f143])).
% 0.13/0.39 fof(f169,plain,(
% 0.13/0.39 ![X103,X104]: (p39(X103,X104)|(![X105,X106]: ~p39(f5(c40,f10(f13(f15(c42,X103),X105),X106)),X104)))),
% 0.13/0.39 inference(miniscoping,[status(thm)],[f63])).
% 0.13/0.39 fof(f170,plain,(
% 0.13/0.39 ![X0,X1,X2,X3]: (p39(X0,X1)|~p39(f5(c40,f10(f13(f15(c42,X0),X2),X3)),X1))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f169])).
% 0.13/0.39 fof(f171,plain,(
% 0.13/0.39 ![X103,X104]: ((![X105,X106]: p39(f5(c40,f10(f13(f15(c42,X103),X105),X106)),X104))|~p39(X103,X104))),
% 0.13/0.39 inference(miniscoping,[status(thm)],[f64])).
% 0.13/0.39 fof(f172,plain,(
% 0.13/0.39 ![X0,X1,X2,X3]: (p39(f5(c40,f10(f13(f15(c42,X0),X1),X2)),X3)|~p39(X0,X3))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f171])).
% 0.13/0.39 fof(f175,plain,(
% 0.13/0.39 ![X0,X1,X2]: (p3(f7(c41,f10(f13(f15(c42,X0),X1),X2)),f10(f13(f15(c42,f17(f19(f21(c47,X0),X1),X2)),f26(f28(f30(c48,X0),X1),X2)),f34(f36(f38(c49,X0),X1),X2))))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f67])).
% 0.13/0.39 fof(f251,plain,(
% 0.13/0.39 ![X0,X1,X2]: (p39(X0,X1)|~p39(X2,X1)|~p4(X2,X0))),
% 0.13/0.39 inference(resolution,[status(thm)],[f135,f82])).
% 0.13/0.39 fof(f258,plain,(
% 0.13/0.39 ![X0,X1,X2]: (p4(f5(X0,X1),f5(X0,X2))|~p3(X1,X2))),
% 0.13/0.39 inference(resolution,[status(thm)],[f144,f84])).
% 0.13/0.39 fof(f287,plain,(
% 0.13/0.39 ![X0]: (p39(X0,c46)|~p4(f5(c40,f7(c41,f10(f13(f15(c42,c43),c44),c45))),X0))),
% 0.13/0.39 inference(resolution,[status(thm)],[f251,f136])).
% 0.13/0.39 fof(f293,plain,(
% 0.13/0.39 ![X0,X1,X2,X3]: (p4(f5(X0,f7(c41,f10(f13(f15(c42,X1),X2),X3))),f5(X0,f10(f13(f15(c42,f17(f19(f21(c47,X1),X2),X3)),f26(f28(f30(c48,X1),X2),X3)),f34(f36(f38(c49,X1),X2),X3)))))),
% 0.13/0.39 inference(resolution,[status(thm)],[f258,f175])).
% 0.13/0.39 fof(f326,plain,(
% 0.13/0.39 p39(f5(c40,f10(f13(f15(c42,f17(f19(f21(c47,c43),c44),c45)),f26(f28(f30(c48,c43),c44),c45)),f34(f36(f38(c49,c43),c44),c45))),c46)),
% 0.13/0.39 inference(resolution,[status(thm)],[f293,f287])).
% 0.13/0.39 fof(f378,plain,(
% 0.13/0.39 p39(f17(f19(f21(c47,c43),c44),c45),c46)),
% 0.13/0.39 inference(resolution,[status(thm)],[f326,f170])).
% 0.13/0.39 fof(f385,plain,(
% 0.13/0.39 p39(c43,c46)),
% 0.13/0.39 inference(resolution,[status(thm)],[f378,f133])).
% 0.13/0.39 fof(f398,plain,(
% 0.13/0.39 ![X0,X1]: (p39(f5(c40,f10(f13(f15(c42,c43),X0),X1)),c46))),
% 0.13/0.39 inference(resolution,[status(thm)],[f385,f172])).
% 0.13/0.39 fof(f424,plain,(
% 0.13/0.39 $false),
% 0.13/0.39 inference(backward_subsumption_resolution,[status(thm)],[f131,f398])).
% 0.13/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.41 % Elapsed time: 0.050284 seconds
% 0.13/0.41 % CPU time: 0.169617 seconds
% 0.13/0.41 % Total memory used: 56.179 MB
% 0.13/0.41 % Net memory used: 56.067 MB
%------------------------------------------------------------------------------