%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ037-3 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 02:00:20 PM UTC 2026
% Result : Unsatisfiable 18.06s 2.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ037-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n018.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 03:48:28 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 18.06/2.71 % Refutation found
% 18.06/2.71 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 18.06/2.71 % SZS output start CNFRefutation for theBenchmark
% 18.06/2.71 fof(f1,negated_conjecture,(
% 18.06/2.71 ~ state(b,b,b,b,b,b,b,b,b,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,w,w,w,w,w,w,w,w,w) ),
% 18.06/2.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.06/2.71 fof(f2,hypothesis,(
% 18.06/2.71 state(b,r,r,w,w,w,y,b,b,g,y,r,b,g,g,o,g,y,w,w,r,g,o,r,b,g,g,o,r,b,y,y,r,g,o,g,o,o,o,y,r,b,y,y,r,w,w,w,b,b,y,w,o,o) ),
% 18.06/2.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.06/2.71 fof(f7,axiom,(
% 18.06/2.71 (![A1,A2,A3,Y1,Y2,Y3,A4,A5,A6,A7,X9,A8,A9,B1,B2,B3,X1,B4,B5,B6,B7,B8,X8,B9,C1,C2,C3,C4,X2,C5,C6,C7,C8,C9,X7,D1,D2,D3,D4,D5,X3,D6,D7,D8,D9,E1,E2,E3,X6,X5,X4,E4,E5,E6]: (( ~ state(A1,A2,A3,Y1,Y2,Y3,A4,A5,A6,A7,X9,A8,A9,B1,B2,B3,X1,B4,B5,B6,B7,B8,X8,B9,C1,C2,C3,C4,X2,C5,C6,C7,C8,C9,X7,D1,D2,D3,D4,D5,X3,D6,D7,D8,D9,E1,E2,E3,X6,X5,X4,E4,E5,E6)| state(A1,A2,A3,X1,X2,X3,A4,A5,A6,A7,Y3,A8,A9,B1,B2,B3,X4,B4,B5,B6,B7,B8,Y2,B9,C1,C2,C3,C4,X5,C5,C6,C7,C8,C9,Y1,D1,D2,D3,D4,D5,X6,D6,D7,D8,D9,E1,E2,E3,X9,X8,X7,E4,E5,E6) ) ))),
% 18.06/2.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.06/2.71 fof(f8,axiom,(
% 18.06/2.71 (![Y1,Y2,Y3,A1,A2,A3,A4,A5,A6,X9,A7,A8,A9,B1,B2,B3,B4,X1,W1,W8,W7,X8,B5,B6,B7,B8,B9,C1,C2,X2,W2,C3,W6,X7,C4,C5,C6,C7,C8,C9,D1,X3,W3,W4,W5,D2,D3,D4,D5,D6,D7,X6,X5,X4]: (( ~ state(Y1,Y2,Y3,A1,A2,A3,A4,A5,A6,X9,A7,A8,A9,B1,B2,B3,B4,X1,W1,W8,W7,X8,B5,B6,B7,B8,B9,C1,C2,X2,W2,C3,W6,X7,C4,C5,C6,C7,C8,C9,D1,X3,W3,W4,W5,D2,D3,D4,D5,D6,D7,X6,X5,X4)| state(X1,X2,X3,A1,A2,A3,A4,A5,A6,Y3,A7,A8,A9,B1,B2,B3,B4,X4,W3,W2,W1,Y2,B5,B6,B7,B8,B9,C1,C2,X5,W4,C3,W8,Y1,C4,C5,C6,C7,C8,C9,D1,X6,W5,W6,W7,D2,D3,D4,D5,D6,D7,X9,X8,X7) ) ))),
% 18.06/2.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.06/2.71 fof(f9,axiom,(
% 18.06/2.71 (![Y1,A1,A2,Y2,A3,A4,Y3,A5,A6,W7,W8,W1,X1,A7,A8,A9,B1,B2,B3,B4,X9,W6,B5,W2,X2,B6,B7,B8,B9,C1,C2,C3,X8,W5,W4,W3,X3,C4,C5,C6,C7,C8,C9,D1,X7,X4,D2,D3,X5,D4,D5,X6,D6,D7]: (( ~ state(Y1,A1,A2,Y2,A3,A4,Y3,A5,A6,W7,W8,W1,X1,A7,A8,A9,B1,B2,B3,B4,X9,W6,B5,W2,X2,B6,B7,B8,B9,C1,C2,C3,X8,W5,W4,W3,X3,C4,C5,C6,C7,C8,C9,D1,X7,X4,D2,D3,X5,D4,D5,X6,D6,D7)| state(X1,A1,A2,X2,A3,A4,X3,A5,A6,W1,W2,W3,X4,A7,A8,A9,B1,B2,B3,B4,Y3,W8,B5,W4,X5,B6,B7,B8,B9,C1,C2,C3,Y2,W7,W6,W5,X6,C4,C5,C6,C7,C8,C9,D1,Y1,X7,D2,D3,X8,D4,D5,X9,D6,D7) ) ))),
% 18.06/2.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.06/2.71 fof(f14,axiom,(
% 18.06/2.71 (![A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,W1,W2,W3,W8,D7,W4,W7,W6,W5]: (( ~ state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,W1,W2,W3,W8,D7,W4,W7,W6,W5)| state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,W7,W8,W1,W6,D7,W2,W5,W4,W3) ) ))),
% 18.06/2.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.06/2.71 fof(f21,plain,(
% 18.06/2.71 ~state(b,b,b,b,b,b,b,b,b,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,w,w,w,w,w,w,w,w,w)),
% 18.06/2.71 inference(cnf_transformation,[status(thm)],[f1])).
% 18.06/2.71 fof(f22,plain,(
% 18.06/2.71 state(b,r,r,w,w,w,y,b,b,g,y,r,b,g,g,o,g,y,w,w,r,g,o,r,b,g,g,o,r,b,y,y,r,g,o,g,o,o,o,y,r,b,y,y,r,w,w,w,b,b,y,w,o,o)),
% 18.06/2.71 inference(cnf_transformation,[status(thm)],[f2])).
% 18.06/2.71 fof(f27,plain,(
% 18.06/2.71 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53]: (~state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53)|state(X0,X1,X2,X16,X28,X40,X6,X7,X8,X9,X5,X11,X12,X13,X14,X15,X50,X17,X18,X19,X20,X21,X4,X23,X24,X25,X26,X27,X49,X29,X30,X31,X32,X33,X3,X35,X36,X37,X38,X39,X48,X41,X42,X43,X44,X45,X46,X47,X10,X22,X34,X51,X52,X53))),
% 18.06/2.71 inference(cnf_transformation,[status(thm)],[f7])).
% 18.06/2.71 fof(f28,plain,(
% 18.06/2.71 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53]: (~state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53)|state(X17,X29,X41,X3,X4,X5,X6,X7,X8,X2,X10,X11,X12,X13,X14,X15,X16,X53,X42,X30,X18,X1,X22,X23,X24,X25,X26,X27,X28,X52,X43,X31,X19,X0,X34,X35,X36,X37,X38,X39,X40,X51,X44,X32,X20,X45,X46,X47,X48,X49,X50,X9,X21,X33))),
% 18.06/2.74 inference(cnf_transformation,[status(thm)],[f8])).
% 18.06/2.74 fof(f29,plain,(
% 18.06/2.74 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53]: (~state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53)|state(X12,X1,X2,X24,X4,X5,X36,X7,X8,X11,X23,X35,X45,X13,X14,X15,X16,X17,X18,X19,X6,X10,X22,X34,X48,X25,X26,X27,X28,X29,X30,X31,X3,X9,X21,X33,X51,X37,X38,X39,X40,X41,X42,X43,X0,X44,X46,X47,X32,X49,X50,X20,X52,X53))),
% 18.06/2.74 inference(cnf_transformation,[status(thm)],[f9])).
% 18.06/2.74 fof(f34,plain,(
% 18.06/2.74 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53]: (~state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53)|state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X42,X43,X44,X33,X34,X35,X36,X37,X38,X39,X40,X41,X51,X48,X45,X52,X49,X46,X53,X50,X47))),
% 18.06/2.74 inference(cnf_transformation,[status(thm)],[f14])).
% 18.06/2.74 fof(f78,plain,(
% 18.06/2.74 state(b,r,r,g,r,r,y,b,b,g,w,r,b,g,g,o,y,y,w,w,r,g,w,r,b,g,g,o,b,b,y,y,r,g,w,g,o,o,o,y,b,b,y,y,r,w,w,w,y,o,o,w,o,o)),
% 18.06/2.74 inference(resolution,[status(thm)],[f27,f22])).
% 18.06/2.74 fof(f110,plain,(
% 18.06/2.74 state(b,r,r,y,b,b,y,b,b,g,r,r,b,g,g,o,o,y,w,w,r,g,r,r,b,g,g,o,o,b,y,y,r,g,g,g,o,o,o,y,y,b,y,y,r,w,w,w,w,w,w,w,o,o)),
% 18.06/2.74 inference(resolution,[status(thm)],[f78,f27])).
% 18.06/2.74 fof(f333,plain,(
% 18.06/2.74 state(y,b,b,y,b,b,y,b,b,r,r,r,b,g,g,o,o,o,y,y,w,r,r,r,b,g,g,o,o,o,y,y,w,b,g,g,o,o,o,y,y,w,r,r,r,w,w,w,w,w,w,g,g,g)),
% 18.06/2.74 inference(resolution,[status(thm)],[f110,f28])).
% 18.06/2.74 fof(f444,plain,(
% 18.06/2.74 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53]: (~state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53)|state(X12,X1,X2,X24,X4,X5,X33,X7,X8,X11,X23,X44,X51,X13,X14,X15,X16,X17,X18,X19,X6,X10,X22,X43,X52,X25,X26,X27,X28,X29,X30,X31,X3,X9,X21,X42,X53,X34,X35,X36,X37,X38,X39,X40,X0,X41,X48,X45,X32,X49,X46,X20,X50,X47))),
% 18.06/2.74 inference(resolution,[status(thm)],[f34,f29])).
% 18.06/2.74 fof(f4515,plain,(
% 18.06/2.74 ~state(y,b,b,y,b,b,y,b,b,r,r,r,b,g,g,o,o,o,y,y,w,r,r,r,b,g,g,o,o,o,y,y,w,b,g,g,o,o,o,y,y,w,r,r,r,w,w,w,w,w,w,g,g,g)),
% 18.06/2.74 inference(resolution,[status(thm)],[f444,f21])).
% 18.06/2.74 fof(f4522,plain,(
% 18.06/2.74 $false),
% 18.06/2.74 inference(forward_subsumption_resolution,[status(thm)],[f4515,f333])).
% 18.06/2.74 % SZS output end CNFRefutation for theBenchmark.p
% 18.06/2.80 % Elapsed time: 2.408335 seconds
% 18.06/2.80 % CPU time: 18.665546 seconds
% 18.06/2.80 % Total memory used: 398.029 MB
% 18.06/2.80 % Net memory used: 353.842 MB
%------------------------------------------------------------------------------