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