%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MSC008-2.002 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n021.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 : Fri Jul 25 11:13:20 AM UTC 2025
% Result : Unsatisfiable 13.95s 2.10s
% Output : CNFRefutation 13.95s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named no_two_same)
% Comments :
%------------------------------------------------------------------------------
cnf(15,plain,
( ~ latin(X0,X1,X2)
| ~ latin(X3,X4,X2)
| ~ greek(X0,X1,X5)
| ~ greek(X3,X4,X5)
| eq(X3,X0)
| eq(X4,X1) ),
inference(cnf,[status(esa)],[no_two_same]) ).
cnf(l0,plain,
( ~ latin(p1,p2,p2)
| ~ latin(p2,p1,p2)
| ~ greek(p1,p2,p1)
| ~ greek(p2,p1,p1)
| eq(p2,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(2,plain,
( ~ eq(X0,X1)
| eq(X1,X0) ),
inference(cnf,[status(esa)],[symmetry]) ).
cnf(l12,plain,
( ~ eq(p2,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(0,plain,
~ eq(p1,p2),
inference(cnf,[status(esa)],[p1_is_not_p2]) ).
cnf(l32,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l7,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(12,plain,
( greek(X0,X1,p2)
| greek(X0,X1,p1) ),
inference(cnf,[status(esa)],[greek_cell_element]) ).
cnf(l8,plain,
( greek(p2,p1,p2)
| greek(p2,p1,p1) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(7,plain,
( ~ greek(X0,X1,X2)
| ~ greek(X0,X3,X2)
| eq(X3,X1) ),
inference(cnf,[status(esa)],[greek_column_is_unique]) ).
cnf(l17,plain,
( ~ greek(p2,p1,p2)
| ~ greek(p2,p2,p2)
| eq(p2,p1) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(9,plain,
( latin(X0,X1,p2)
| latin(X0,X1,p1) ),
inference(cnf,[status(esa)],[latin_cell_element]) ).
cnf(l2,plain,
( latin(p1,p2,p2)
| latin(p1,p2,p1) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(14,plain,
( greek(p2,X0,X1)
| greek(p1,X0,X1) ),
inference(cnf,[status(esa)],[greek_row_required]) ).
cnf(l1,plain,
( greek(p2,p2,p1)
| greek(p1,p2,p1) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(5,plain,
( ~ latin(X0,X1,X2)
| ~ latin(X3,X1,X2)
| eq(X3,X0) ),
inference(cnf,[status(esa)],[latin_row_is_unique]) ).
cnf(l589,plain,
( ~ latin(p2,p2,p1)
| ~ latin(p1,p2,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(10,plain,
( latin(X0,p2,X1)
| latin(X0,p1,X1) ),
inference(cnf,[status(esa)],[latin_column_required]) ).
cnf(l592,plain,
( latin(p2,p2,p1)
| latin(p2,p1,p1) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(6,plain,
( ~ greek(X0,X1,X2)
| ~ greek(X0,X1,X3)
| eq(X3,X2) ),
inference(cnf,[status(esa)],[greek_element_is_unique]) ).
cnf(l644,plain,
( ~ greek(p2,p2,p1)
| ~ greek(p2,p2,p2)
| eq(p2,p1) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l645,plain,
( greek(p2,p2,p2)
| greek(p1,p2,p2) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l649,plain,
( greek(p2,p2,p2)
| greek(p1,p2,p2) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l646,plain,
( ~ eq(p2,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l34,plain,
( ~ eq(p2,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l648,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l590,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l650,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l655,plain,
( ~ latin(p1,p2,X1_800)
| ~ latin(p2,p1,X1_800)
| ~ greek(p1,p2,p2)
| ~ greek(p2,p1,p2)
| eq(p2,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l672,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l651,plain,
( ~ latin(p2,p1,X1_729)
| ~ latin(p1,p2,X1_729)
| ~ greek(p2,p1,p2)
| ~ greek(p1,p2,p2)
| eq(p1,p2)
| eq(p2,p1) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l705,plain,
( ~ eq(p2,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l647,plain,
( ~ latin(p2,p1,p1)
| ~ latin(p1,p2,p1)
| ~ greek(p2,p1,X1_731)
| ~ greek(p1,p2,X1_731)
| eq(p1,p2)
| eq(p2,p1) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(11,plain,
( latin(p2,X0,X1)
| latin(p1,X0,X1) ),
inference(cnf,[status(esa)],[latin_row_required]) ).
cnf(l669,plain,
( latin(p2,p2,X1_800)
| latin(p1,p2,X1_800) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l676,plain,
( ~ latin(p2,p2,X1_800)
| ~ latin(p1,p1,X1_800)
| ~ greek(p2,p2,p1)
| ~ greek(p1,p1,p1)
| eq(p1,p2)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(13,plain,
( greek(X0,p2,X1)
| greek(X0,p1,X1) ),
inference(cnf,[status(esa)],[greek_column_required]) ).
cnf(l684,plain,
( greek(p2,p2,p1)
| greek(p2,p1,p1) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l670,plain,
( ~ eq(p2,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l708,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3,plain,
( latin(p2,p1,p2)
| latin(p1,p1,p2) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l677,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l652,plain,
( greek(p2,p2,X1_731)
| greek(p2,p1,X1_731) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l690,plain,
( ~ eq(p2,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l685,plain,
( latin(p1,p2,X1_800)
| latin(p1,p1,X1_800) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l663,plain,
( greek(p2,p1,p2)
| greek(p1,p1,p2) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l688,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l666,plain,
( ~ greek(p1,p2,p2)
| ~ greek(p1,p1,p2)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l696,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l834,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l665,plain,
( latin(p1,p2,X1_729)
| latin(p1,p1,X1_729) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l392,plain,
( ~ latin(p2,p2,p2)
| ~ latin(p1,p1,p2)
| ~ greek(p2,p2,p2)
| ~ greek(p1,p1,p2)
| eq(p1,p2)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l394,plain,
( latin(p2,p2,p2)
| latin(p2,p1,p2) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l698,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l706,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l694,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l697,plain,
( greek(p1,p2,p2)
| greek(p1,p1,p2) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l393,plain,
( greek(p2,p2,p2)
| greek(p2,p2,p1) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l659,plain,
( latin(p2,p1,X1_800)
| latin(p1,p1,X1_800) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l830,plain,
( greek(p2,p1,p1)
| greek(p1,p1,p1) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l395,plain,
( ~ latin(p2,p2,p2)
| ~ latin(p1,p1,p2)
| ~ greek(p2,p2,p1)
| ~ greek(p1,p1,p1)
| eq(p1,p2)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l674,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l683,plain,
( latin(p2,p2,X1_729)
| latin(p2,p1,X1_729) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l871,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l710,plain,
( ~ latin(p2,p2,X1_729)
| ~ latin(p1,p1,X1_729)
| ~ greek(p2,p2,p1)
| ~ greek(p1,p1,p1)
| eq(p1,p2)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l693,plain,
( ~ latin(p2,p2,p2)
| ~ latin(p1,p1,p2)
| ~ greek(p2,p2,X1_731)
| ~ greek(p1,p1,X1_731)
| eq(p1,p2)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l790,plain,
( ~ latin(p2,p2,X1_800)
| ~ latin(p1,p1,X1_800)
| ~ greek(p2,p2,p1)
| ~ greek(p1,p1,p1)
| eq(p1,p2)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l732,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l689,plain,
( greek(p1,p2,X1_731)
| greek(p1,p1,X1_731) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l700,plain,
( ~ latin(p2,p2,X1_729)
| ~ latin(p1,p1,X1_729)
| ~ greek(p2,p2,p1)
| ~ greek(p1,p1,p1)
| eq(p1,p2)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l800,plain,
( latin(p2,p2,X1_800)
| latin(p2,p1,X1_800) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l728,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l691,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l701,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l695,plain,
( ~ latin(p2,p2,p2)
| ~ latin(p1,p1,p2)
| ~ greek(p2,p2,X1_731)
| ~ greek(p1,p1,X1_731)
| eq(p1,p2)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l704,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l814,plain,
( latin(p2,p2,X1_729)
| latin(p1,p2,X1_729) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l812,plain,
( latin(p1,p2,p2)
| latin(p1,p1,p2) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l808,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l807,plain,
( latin(p2,p2,p2)
| latin(p1,p2,p2) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l874,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l783,plain,
( ~ latin(p2,p1,p1)
| ~ latin(p1,p2,p1)
| ~ greek(p2,p1,p2)
| ~ greek(p1,p2,p2)
| eq(p1,p2)
| eq(p2,p1) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l873,plain,
( greek(p1,p1,p2)
| greek(p1,p1,p1) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l734,plain,
( greek(p2,p2,X1_731)
| greek(p1,p2,X1_731) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l804,plain,
( greek(p2,p1,p1)
| greek(p1,p1,p1) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l915,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l875,plain,
( latin(p2,p2,p2)
| latin(p1,p2,p2) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l727,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l729,plain,
( latin(p2,p1,X1_729)
| latin(p1,p1,X1_729) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l877,plain,
( greek(p2,p1,p2)
| greek(p1,p1,p2) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l837,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l731,plain,
( greek(p2,p1,X1_731)
| greek(p1,p1,X1_731) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l863,plain,
( greek(p1,p2,p1)
| greek(p1,p1,p1) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l775,plain,
( greek(p1,p2,p1)
| greek(p1,p1,p1) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l730,plain,
( latin(p2,p2,p2)
| latin(p1,p2,p2) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l887,plain,
( ~ greek(p1,p2,p2)
| ~ greek(p1,p1,p2)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l792,plain,
( greek(p2,p2,p2)
| greek(p2,p2,p1) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l733,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l909,plain,
( greek(p2,p2,p2)
| greek(p1,p2,p2) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l879,plain,
( latin(p2,p2,p1)
| latin(p1,p2,p1) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l864,plain,
( ~ eq(p2,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l735,plain,
( latin(p1,p2,p2)
| latin(p1,p1,p2) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l836,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l803,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l937,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l889,plain,
( latin(p2,p1,p1)
| latin(p1,p1,p1) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(4,plain,
( ~ latin(X0,X1,X2)
| ~ latin(X0,X3,X2)
| eq(X3,X1) ),
inference(cnf,[status(esa)],[latin_column_is_unique]) ).
cnf(l896,plain,
( ~ latin(p1,p2,p2)
| ~ latin(p1,p1,p2)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l913,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(3,plain,
( ~ latin(X0,X1,X2)
| ~ latin(X0,X1,X3)
| eq(X3,X2) ),
inference(cnf,[status(esa)],[latin_element_is_unique]) ).
cnf(l891,plain,
( ~ latin(p1,p1,p2)
| ~ latin(p1,p1,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l940,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l917,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l880,plain,
( ~ latin(p2,p2,p1)
| ~ latin(p2,p1,p1)
| eq(p1,p2) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l943,plain,
~ eq(p1,p2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l949,plain,
( latin(p2,p1,p2)
| latin(p2,p1,p1) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l12,l32,l7,l8,l17,l2,l1,l589,l592,l644,l645,l649,l646,l34,l648,l590,l650,l655,l672,l651,l705,l647,l669,l676,l684,l670,l708,l3,l677,l652,l690,l685,l663,l688,l666,l696,l834,l665,l392,l394,l698,l706,l694,l697,l393,l659,l830,l395,l674,l683,l871,l710,l693,l790,l732,l689,l700,l800,l728,l691,l701,l695,l704,l814,l812,l808,l807,l874,l783,l873,l734,l804,l915,l875,l727,l729,l877,l837,l731,l863,l775,l730,l887,l792,l733,l909,l879,l864,l735,l836,l803,l937,l889,l896,l913,l891,l940,l917,l880,l943,l949]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : MSC008-2.002 : TPTP v9.0.0. Released v1.0.0.
% 0.03/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n021.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Jul 21 07:38:49 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.19/0.35 % launching worker at depth: 10
% 0.19/0.55 % launching worker at depth: 11
% 3.20/0.74 % launching worker at depth: 12
% 13.95/2.10 % SZS status Theorem for theBenchmark
% 13.95/2.10 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------