%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : PUZ037-1 : TPTP v9.2.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:02:44 PM UTC 2026
% Result : Unsatisfiable 0.20s 1.57s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 20
% Syntax : Number of clauses : 41 ( 5 unt; 0 nHn; 41 RR)
% Number of literals : 77 ( 0 equ; 38 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-54 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 1944 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(make_like_this,negated_conjecture,
~ 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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',make_like_this) ).
cnf(bxy,axiom,
( state(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,X37,X38,X39,X40,X41,X42,X43,X44,X45,X34,X35,X36,X48,X51,X54,X47,X50,X53,X46,X49,X52)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bxy) ).
cnf(byx,axiom,
( state(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,X43,X44,X45,X34,X35,X36,X37,X38,X39,X40,X41,X42,X52,X49,X46,X53,X50,X47,X54,X51,X48)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',byx) ).
cnf(mxy,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X25,X26,X27,X28,X29,X30,X31,X32,X33,X22,X23,X24,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mxy) ).
cnf(myx,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X31,X32,X33,X22,X23,X24,X25,X26,X27,X28,X29,X30,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',myx) ).
cnf(fzy,axiom,
( state(X1,X2,X3,X4,X5,X6,X16,X28,X40,X10,X11,X9,X15,X27,X39,X48,X17,X18,X19,X20,X21,X22,X23,X8,X14,X26,X38,X47,X29,X30,X31,X32,X33,X34,X35,X7,X13,X25,X37,X46,X41,X42,X43,X44,X45,X12,X24,X36,X49,X50,X51,X52,X53,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fzy) ).
cnf(fyz,axiom,
( state(X1,X2,X3,X4,X5,X6,X36,X24,X12,X10,X11,X46,X37,X25,X13,X7,X17,X18,X19,X20,X21,X22,X23,X47,X38,X26,X14,X8,X29,X30,X31,X32,X33,X34,X35,X48,X39,X27,X15,X9,X41,X42,X43,X44,X45,X40,X28,X16,X49,X50,X51,X52,X53,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fyz) ).
cnf(mzy,axiom,
( state(X1,X2,X3,X17,X29,X41,X7,X8,X9,X10,X6,X12,X13,X14,X15,X16,X51,X18,X19,X20,X21,X22,X5,X24,X25,X26,X27,X28,X50,X30,X31,X32,X33,X34,X4,X36,X37,X38,X39,X40,X49,X42,X43,X44,X45,X46,X47,X48,X11,X23,X35,X52,X53,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mzy) ).
cnf(myz,axiom,
( state(X1,X2,X3,X35,X23,X11,X7,X8,X9,X10,X49,X12,X13,X14,X15,X16,X4,X18,X19,X20,X21,X22,X50,X24,X25,X26,X27,X28,X5,X30,X31,X32,X33,X34,X51,X36,X37,X38,X39,X40,X6,X42,X43,X44,X45,X46,X47,X48,X41,X29,X17,X52,X53,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',myz) ).
cnf(rzx,axiom,
( state(X1,X2,X15,X4,X5,X27,X7,X8,X39,X10,X11,X12,X13,X14,X48,X40,X28,X16,X9,X20,X21,X22,X23,X24,X25,X26,X51,X41,X29,X17,X6,X32,X33,X34,X35,X36,X37,X38,X54,X42,X30,X18,X3,X44,X45,X46,X47,X43,X49,X50,X31,X52,X53,X19)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rzx) ).
cnf(rxz,axiom,
( state(X1,X2,X43,X4,X5,X31,X7,X8,X19,X10,X11,X12,X13,X14,X3,X18,X30,X42,X54,X20,X21,X22,X23,X24,X25,X26,X6,X17,X29,X41,X51,X32,X33,X34,X35,X36,X37,X38,X9,X16,X28,X40,X48,X44,X45,X46,X47,X15,X49,X50,X27,X52,X53,X39)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rxz) ).
cnf(mzx,axiom,
( state(X1,X14,X3,X4,X26,X6,X7,X38,X9,X10,X11,X12,X13,X47,X15,X16,X17,X18,X19,X8,X21,X22,X23,X24,X25,X50,X27,X28,X29,X30,X31,X5,X33,X34,X35,X36,X37,X53,X39,X40,X41,X42,X43,X2,X45,X46,X44,X48,X49,X32,X51,X52,X20,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mzx) ).
cnf(mxz,axiom,
( state(X1,X44,X3,X4,X32,X6,X7,X20,X9,X10,X11,X12,X13,X2,X15,X16,X17,X18,X19,X53,X21,X22,X23,X24,X25,X5,X27,X28,X29,X30,X31,X50,X33,X34,X35,X36,X37,X8,X39,X40,X41,X42,X43,X47,X45,X46,X14,X48,X49,X26,X51,X52,X38,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mxz) ).
cnf(tyx,axiom,
( state(X3,X6,X9,X2,X5,X8,X1,X4,X7,X19,X20,X21,X10,X11,X12,X13,X14,X15,X16,X17,X18,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,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tyx) ).
cnf(txy,axiom,
( state(X7,X4,X1,X8,X5,X2,X9,X6,X3,X13,X14,X15,X16,X17,X18,X19,X20,X21,X10,X11,X12,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,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',txy) ).
cnf(lzx,axiom,
( state(X13,X2,X3,X25,X5,X6,X37,X8,X9,X12,X24,X36,X46,X14,X15,X16,X17,X18,X19,X20,X7,X11,X23,X35,X49,X26,X27,X28,X29,X30,X31,X32,X4,X10,X22,X34,X52,X38,X39,X40,X41,X42,X43,X44,X1,X45,X47,X48,X33,X50,X51,X21,X53,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lzx) ).
cnf(bzy,axiom,
( state(X18,X30,X42,X4,X5,X6,X7,X8,X9,X3,X11,X12,X13,X14,X15,X16,X17,X54,X43,X31,X19,X2,X23,X24,X25,X26,X27,X28,X29,X53,X44,X32,X20,X1,X35,X36,X37,X38,X39,X40,X41,X52,X45,X33,X21,X46,X47,X48,X49,X50,X51,X10,X22,X34)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bzy) ).
cnf(byz,axiom,
( state(X34,X22,X10,X4,X5,X6,X7,X8,X9,X52,X11,X12,X13,X14,X15,X16,X17,X1,X21,X33,X45,X53,X23,X24,X25,X26,X27,X28,X29,X2,X20,X32,X44,X54,X35,X36,X37,X38,X39,X40,X41,X3,X19,X31,X43,X46,X47,X48,X49,X50,X51,X42,X30,X18)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',byz) ).
cnf(lxz,axiom,
( state(X45,X2,X3,X33,X5,X6,X21,X8,X9,X34,X22,X10,X1,X14,X15,X16,X17,X18,X19,X20,X52,X35,X23,X11,X4,X26,X27,X28,X29,X30,X31,X32,X49,X36,X24,X12,X7,X38,X39,X40,X41,X42,X43,X44,X46,X13,X47,X48,X25,X50,X51,X37,X53,X54)
| ~ state(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,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lxz) ).
cnf(start_with_this,hypothesis,
state(b,b,b,b,b,b,b,b,b,r,r,r,g,g,g,o,o,o,y,y,y,g,g,g,o,o,o,y,y,y,r,r,r,r,r,r,g,g,g,o,o,o,y,y,y,w,w,w,w,w,w,w,w,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',start_with_this) ).
cnf(i_0_20,negated_conjecture,
~ 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),
make_like_this,
[final] ).
cnf(i_0_21,axiom,
( state(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,X37,X38,X39,X40,X41,X42,X43,X44,X45,X34,X35,X36,X48,X51,X54,X47,X50,X53,X46,X49,X52)
| ~ state(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,X54) ),
bxy,
[final] ).
cnf(i_0_22,axiom,
( state(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,X43,X44,X45,X34,X35,X36,X37,X38,X39,X40,X41,X42,X52,X49,X46,X53,X50,X47,X54,X51,X48)
| ~ state(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,X54) ),
byx,
[final] ).
cnf(i_0_23,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X25,X26,X27,X28,X29,X30,X31,X32,X33,X22,X23,X24,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54)
| ~ state(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,X54) ),
mxy,
[final] ).
cnf(i_0_24,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X31,X32,X33,X22,X23,X24,X25,X26,X27,X28,X29,X30,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54)
| ~ state(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,X54) ),
myx,
[final] ).
cnf(i_0_25,axiom,
( state(X1,X2,X3,X4,X5,X6,X16,X28,X40,X10,X11,X9,X15,X27,X39,X48,X17,X18,X19,X20,X21,X22,X23,X8,X14,X26,X38,X47,X29,X30,X31,X32,X33,X34,X35,X7,X13,X25,X37,X46,X41,X42,X43,X44,X45,X12,X24,X36,X49,X50,X51,X52,X53,X54)
| ~ state(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,X54) ),
fzy,
[final] ).
cnf(i_0_26,axiom,
( state(X1,X2,X3,X4,X5,X6,X36,X24,X12,X10,X11,X46,X37,X25,X13,X7,X17,X18,X19,X20,X21,X22,X23,X47,X38,X26,X14,X8,X29,X30,X31,X32,X33,X34,X35,X48,X39,X27,X15,X9,X41,X42,X43,X44,X45,X40,X28,X16,X49,X50,X51,X52,X53,X54)
| ~ state(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,X54) ),
fyz,
[final] ).
cnf(i_0_27,axiom,
( state(X1,X2,X3,X17,X29,X41,X7,X8,X9,X10,X6,X12,X13,X14,X15,X16,X51,X18,X19,X20,X21,X22,X5,X24,X25,X26,X27,X28,X50,X30,X31,X32,X33,X34,X4,X36,X37,X38,X39,X40,X49,X42,X43,X44,X45,X46,X47,X48,X11,X23,X35,X52,X53,X54)
| ~ state(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,X54) ),
mzy,
[final] ).
cnf(i_0_28,axiom,
( state(X1,X2,X3,X35,X23,X11,X7,X8,X9,X10,X49,X12,X13,X14,X15,X16,X4,X18,X19,X20,X21,X22,X50,X24,X25,X26,X27,X28,X5,X30,X31,X32,X33,X34,X51,X36,X37,X38,X39,X40,X6,X42,X43,X44,X45,X46,X47,X48,X41,X29,X17,X52,X53,X54)
| ~ state(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,X54) ),
myz,
[final] ).
cnf(i_0_29,axiom,
( state(X1,X2,X15,X4,X5,X27,X7,X8,X39,X10,X11,X12,X13,X14,X48,X40,X28,X16,X9,X20,X21,X22,X23,X24,X25,X26,X51,X41,X29,X17,X6,X32,X33,X34,X35,X36,X37,X38,X54,X42,X30,X18,X3,X44,X45,X46,X47,X43,X49,X50,X31,X52,X53,X19)
| ~ state(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,X54) ),
rzx,
[final] ).
cnf(i_0_30,axiom,
( state(X1,X2,X43,X4,X5,X31,X7,X8,X19,X10,X11,X12,X13,X14,X3,X18,X30,X42,X54,X20,X21,X22,X23,X24,X25,X26,X6,X17,X29,X41,X51,X32,X33,X34,X35,X36,X37,X38,X9,X16,X28,X40,X48,X44,X45,X46,X47,X15,X49,X50,X27,X52,X53,X39)
| ~ state(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,X54) ),
rxz,
[final] ).
cnf(i_0_31,axiom,
( state(X1,X14,X3,X4,X26,X6,X7,X38,X9,X10,X11,X12,X13,X47,X15,X16,X17,X18,X19,X8,X21,X22,X23,X24,X25,X50,X27,X28,X29,X30,X31,X5,X33,X34,X35,X36,X37,X53,X39,X40,X41,X42,X43,X2,X45,X46,X44,X48,X49,X32,X51,X52,X20,X54)
| ~ state(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,X54) ),
mzx,
[final] ).
cnf(i_0_32,axiom,
( state(X1,X44,X3,X4,X32,X6,X7,X20,X9,X10,X11,X12,X13,X2,X15,X16,X17,X18,X19,X53,X21,X22,X23,X24,X25,X5,X27,X28,X29,X30,X31,X50,X33,X34,X35,X36,X37,X8,X39,X40,X41,X42,X43,X47,X45,X46,X14,X48,X49,X26,X51,X52,X38,X54)
| ~ state(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,X54) ),
mxz,
[final] ).
cnf(i_0_33,axiom,
( state(X3,X6,X9,X2,X5,X8,X1,X4,X7,X19,X20,X21,X10,X11,X12,X13,X14,X15,X16,X17,X18,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,X54)
| ~ state(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,X54) ),
tyx,
[final] ).
cnf(i_0_34,axiom,
( state(X7,X4,X1,X8,X5,X2,X9,X6,X3,X13,X14,X15,X16,X17,X18,X19,X20,X21,X10,X11,X12,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,X54)
| ~ state(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,X54) ),
txy,
[final] ).
cnf(i_0_35,axiom,
( state(X13,X2,X3,X25,X5,X6,X37,X8,X9,X12,X24,X36,X46,X14,X15,X16,X17,X18,X19,X20,X7,X11,X23,X35,X49,X26,X27,X28,X29,X30,X31,X32,X4,X10,X22,X34,X52,X38,X39,X40,X41,X42,X43,X44,X1,X45,X47,X48,X33,X50,X51,X21,X53,X54)
| ~ state(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,X54) ),
lzx,
[final] ).
cnf(i_0_36,axiom,
( state(X18,X30,X42,X4,X5,X6,X7,X8,X9,X3,X11,X12,X13,X14,X15,X16,X17,X54,X43,X31,X19,X2,X23,X24,X25,X26,X27,X28,X29,X53,X44,X32,X20,X1,X35,X36,X37,X38,X39,X40,X41,X52,X45,X33,X21,X46,X47,X48,X49,X50,X51,X10,X22,X34)
| ~ state(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,X54) ),
bzy,
[final] ).
cnf(i_0_37,axiom,
( state(X34,X22,X10,X4,X5,X6,X7,X8,X9,X52,X11,X12,X13,X14,X15,X16,X17,X1,X21,X33,X45,X53,X23,X24,X25,X26,X27,X28,X29,X2,X20,X32,X44,X54,X35,X36,X37,X38,X39,X40,X41,X3,X19,X31,X43,X46,X47,X48,X49,X50,X51,X42,X30,X18)
| ~ state(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,X54) ),
byz,
[final] ).
cnf(i_0_38,axiom,
( state(X45,X2,X3,X33,X5,X6,X21,X8,X9,X34,X22,X10,X1,X14,X15,X16,X17,X18,X19,X20,X52,X35,X23,X11,X4,X26,X27,X28,X29,X30,X31,X32,X49,X36,X24,X12,X7,X38,X39,X40,X41,X42,X43,X44,X46,X13,X47,X48,X25,X50,X51,X37,X53,X54)
| ~ state(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,X54) ),
lxz,
[final] ).
cnf(i_0_39,hypothesis,
state(b,b,b,b,b,b,b,b,b,r,r,r,g,g,g,o,o,o,y,y,y,g,g,g,o,o,o,y,y,y,r,r,r,r,r,r,g,g,g,o,o,o,y,y,y,w,w,w,w,w,w,w,w,w),
start_with_this,
[final] ).
cnf(i_0_40,plain,
$false,
inference(scs_inference,[],[i_0_20,i_0_39,i_0_24]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : PUZ037-1 : TPTP v9.2.1. Released v2.3.0.
% 0.00/0.09 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.10/0.29 % Computer : n029.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Tue May 5 01:34:14 EDT 2026
% 0.10/0.29 % CPUTime :
% 0.10/0.29 % start to proof: theBenchmark
% 0.20/1.57 % Version : CSE_E---1.7
% 0.20/1.57 % Problem : theBenchmark.p
% 0.20/1.57 % SZS status Unsatisfiable for theBenchmark.p
% 0.20/1.57 % SZS output start CNFRefutation
% See solution above
% 0.20/1.58 % Total time : 1.270s
%------------------------------------------------------------------------------