%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN703-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 : n009.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:23 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN703-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.10/0.55 % Computer : n009.cluster.edu
% 0.10/0.55 % Model : x86_64 x86_64
% 0.10/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.55 % Memory : 8046.5625MB
% 0.10/0.55 % OS : Linux 6.8.0-71-generic
% 0.10/0.55 % CPULimit : 300
% 0.10/0.55 % WCLimit : 300
% 0.10/0.55 % DateTime : Mon Sep 21 11:12:58 UTC 2026
% 0.10/0.55 % CPUTime :
% 0.14/0.56 % Drodi V4.1.1
% 0.14/0.58 % Refutation found
% 0.14/0.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.58 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.58 fof(f5,negated_conjecture,(
% 0.14/0.58 (![X17]: (p15(X17,X17) ))),
% 0.14/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f8,negated_conjecture,(
% 0.14/0.58 (![X30]: (p2(X30,X30) ))),
% 0.14/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f51,negated_conjecture,(
% 0.14/0.58 ~ p47(f5(c48,f8(f11(f13(c49,c50),c51),c52)),c53) ),
% 0.14/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f53,negated_conjecture,(
% 0.14/0.58 (![X143,X144,X146,X145]: (( p47(X143,X144)| ~ p4(X146,X143)| ~ p47(X146,X145)| ~ p15(X145,X144) ) ))),
% 0.14/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f60,negated_conjecture,(
% 0.14/0.58 (![X118,X119,X120,X121]: (( p4(f5(X118,X119),f5(X120,X121))| ~ p2(X118,X120)| ~ p3(X119,X121) ) ))),
% 0.14/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f74,negated_conjecture,(
% 0.14/0.58 (![X139,X140,X141,X142]: (( p47(X139,X140)| ~ p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140) ) ))),
% 0.14/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f75,negated_conjecture,(
% 0.14/0.58 (![X57,X61,X58,X59,X60]: (( p47(X57,X61)| ~ p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X61) ) ))),
% 0.14/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f76,negated_conjecture,(
% 0.14/0.58 (![X139,X141,X142,X140]: (( p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140)| ~ p47(X139,X140) ) ))),
% 0.14/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f77,negated_conjecture,(
% 0.14/0.58 p47(f5(c48,f16(f18(c54,f8(f11(f13(c49,c50),c51),c52)),c55)),c53) ),
% 0.14/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f80,negated_conjecture,(
% 0.14/0.58 (![X57,X58,X59,X60]: (p3(f16(f18(c54,f8(f11(f13(c49,X57),X58),X59)),X60),f8(f11(f13(c49,f20(f22(f24(f26(c56,X57),X58),X59),X60)),f30(f32(f34(f36(c57,X57),X58),X59),X60)),f40(f42(f44(f46(c58,X57),X58),X59),X60))) ))),
% 0.14/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f85,plain,(
% 0.14/0.58 ![X0]: (p15(X0,X0))),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.58 fof(f88,plain,(
% 0.14/0.58 ![X0]: (p2(X0,X0))),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.58 fof(f156,plain,(
% 0.14/0.58 ~p47(f5(c48,f8(f11(f13(c49,c50),c51),c52)),c53)),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f51])).
% 0.14/0.58 fof(f158,plain,(
% 0.14/0.58 ![X144,X145]: ((![X146]: ((![X143]: (p47(X143,X144)|~p4(X146,X143)))|~p47(X146,X145)))|~p15(X145,X144))),
% 0.14/0.58 inference(miniscoping,[status(thm)],[f53])).
% 0.14/0.58 fof(f159,plain,(
% 0.14/0.58 ![X0,X1,X2,X3]: (p47(X0,X1)|~p4(X2,X0)|~p47(X2,X3)|~p15(X3,X1))),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f158])).
% 0.14/0.58 fof(f172,plain,(
% 0.14/0.58 ![X119,X121]: ((![X118,X120]: (p4(f5(X118,X119),f5(X120,X121))|~p2(X118,X120)))|~p3(X119,X121))),
% 0.14/0.58 inference(miniscoping,[status(thm)],[f60])).
% 0.14/0.58 fof(f173,plain,(
% 0.14/0.58 ![X0,X1,X2,X3]: (p4(f5(X0,X1),f5(X2,X3))|~p2(X0,X2)|~p3(X1,X3))),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f172])).
% 0.14/0.58 fof(f200,plain,(
% 0.14/0.58 ![X139,X140]: (p47(X139,X140)|(![X141,X142]: ~p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140)))),
% 0.14/0.58 inference(miniscoping,[status(thm)],[f74])).
% 0.14/0.58 fof(f201,plain,(
% 0.14/0.58 ![X0,X1,X2,X3]: (p47(X0,X1)|~p47(f5(c48,f8(f11(f13(c49,X0),X2),X3)),X1))),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f200])).
% 0.14/0.58 fof(f202,plain,(
% 0.14/0.58 ![X57,X61]: (p47(X57,X61)|(![X58,X59,X60]: ~p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X61)))),
% 0.14/0.58 inference(miniscoping,[status(thm)],[f75])).
% 0.14/0.58 fof(f203,plain,(
% 0.14/0.58 ![X0,X1,X2,X3,X4]: (p47(X0,X1)|~p47(f20(f22(f24(f26(c56,X0),X2),X3),X4),X1))),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f202])).
% 0.14/0.58 fof(f204,plain,(
% 0.14/0.58 ![X139,X140]: ((![X141,X142]: p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140))|~p47(X139,X140))),
% 0.14/0.58 inference(miniscoping,[status(thm)],[f76])).
% 0.14/0.58 fof(f205,plain,(
% 0.14/0.58 ![X0,X1,X2,X3]: (p47(f5(c48,f8(f11(f13(c49,X0),X1),X2)),X3)|~p47(X0,X3))),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f204])).
% 0.14/0.58 fof(f206,plain,(
% 0.14/0.58 p47(f5(c48,f16(f18(c54,f8(f11(f13(c49,c50),c51),c52)),c55)),c53)),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f77])).
% 0.14/0.58 fof(f209,plain,(
% 0.14/0.58 ![X0,X1,X2,X3]: (p3(f16(f18(c54,f8(f11(f13(c49,X0),X1),X2)),X3),f8(f11(f13(c49,f20(f22(f24(f26(c56,X0),X1),X2),X3)),f30(f32(f34(f36(c57,X0),X1),X2),X3)),f40(f42(f44(f46(c58,X0),X1),X2),X3))))),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f80])).
% 0.14/0.58 fof(f300,plain,(
% 0.14/0.58 ![X0,X1,X2]: (p47(X0,X1)|~p4(X2,X0)|~p47(X2,X1))),
% 0.14/0.58 inference(resolution,[status(thm)],[f159,f85])).
% 0.14/0.58 fof(f308,plain,(
% 0.14/0.58 ![X0,X1,X2]: (p4(f5(X0,X1),f5(X0,X2))|~p3(X1,X2))),
% 0.14/0.58 inference(resolution,[status(thm)],[f173,f88])).
% 0.14/0.58 fof(f342,plain,(
% 0.14/0.58 ![X0]: (p47(X0,c53)|~p4(f5(c48,f16(f18(c54,f8(f11(f13(c49,c50),c51),c52)),c55)),X0))),
% 0.14/0.58 inference(resolution,[status(thm)],[f300,f206])).
% 0.14/0.58 fof(f349,plain,(
% 0.14/0.58 ![X0,X1,X2,X3,X4]: (p4(f5(X0,f16(f18(c54,f8(f11(f13(c49,X1),X2),X3)),X4)),f5(X0,f8(f11(f13(c49,f20(f22(f24(f26(c56,X1),X2),X3),X4)),f30(f32(f34(f36(c57,X1),X2),X3),X4)),f40(f42(f44(f46(c58,X1),X2),X3),X4)))))),
% 0.14/0.58 inference(resolution,[status(thm)],[f308,f209])).
% 0.14/0.58 fof(f384,plain,(
% 0.14/0.58 p47(f5(c48,f8(f11(f13(c49,f20(f22(f24(f26(c56,c50),c51),c52),c55)),f30(f32(f34(f36(c57,c50),c51),c52),c55)),f40(f42(f44(f46(c58,c50),c51),c52),c55))),c53)),
% 0.14/0.58 inference(resolution,[status(thm)],[f349,f342])).
% 0.14/0.58 fof(f435,plain,(
% 0.14/0.58 p47(f20(f22(f24(f26(c56,c50),c51),c52),c55),c53)),
% 0.14/0.58 inference(resolution,[status(thm)],[f384,f201])).
% 0.14/0.58 fof(f455,plain,(
% 0.14/0.58 p47(c50,c53)),
% 0.14/0.58 inference(resolution,[status(thm)],[f435,f203])).
% 0.14/0.58 fof(f462,plain,(
% 0.14/0.58 ![X0,X1]: (p47(f5(c48,f8(f11(f13(c49,c50),X0),X1)),c53))),
% 0.14/0.58 inference(resolution,[status(thm)],[f455,f205])).
% 0.14/0.58 fof(f486,plain,(
% 0.14/0.58 $false),
% 0.14/0.58 inference(backward_subsumption_resolution,[status(thm)],[f156,f462])).
% 0.14/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.60 % Elapsed time: 0.048881 seconds
% 0.14/0.60 % CPU time: 0.156462 seconds
% 0.14/0.60 % Total memory used: 42.703 MB
% 0.14/0.60 % Net memory used: 42.606 MB
%------------------------------------------------------------------------------