%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MSC008-1.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 : n020.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 30.08s 4.17s
% Output : CNFRefutation 30.08s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named no_two_same1)
% Comments :
%------------------------------------------------------------------------------
cnf(15,plain,
( ~ latin(X0,X1,X2)
| ~ latin(X3,X4,X2)
| ~ greek(X0,X1,X5)
| ~ greek(X3,X4,X5)
| eq(X1,X4) ),
inference(cnf,[status(esa)],[no_two_same1]) ).
cnf(l0,plain,
( ~ latin(p_1,p_2,p_2)
| ~ latin(p_1,p_1,p_2)
| ~ greek(p_1,p_2,p_1)
| ~ greek(p_1,p_1,p_1)
| eq(p_2,p_1) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(14,plain,
( greek(p_2,X0,X1)
| greek(p_1,X0,X1) ),
inference(cnf,[status(esa)],[greek_row_required]) ).
cnf(l5,plain,
( greek(p_2,p_1,p_1)
| greek(p_1,p_1,p_1) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(10,plain,
( latin(X0,p_2,X1)
| latin(X0,p_1,X1) ),
inference(cnf,[status(esa)],[latin_column_required]) ).
cnf(l2,plain,
( latin(p_1,p_2,p_2)
| latin(p_1,p_1,p_2) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(12,plain,
( greek(X0,X1,p_2)
| greek(X0,X1,p_1) ),
inference(cnf,[status(esa)],[greek_cell_element]) ).
cnf(l10,plain,
( greek(p_1,p_2,p_2)
| greek(p_1,p_2,p_1) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(7,plain,
( ~ greek(X0,X1,X2)
| ~ greek(X0,X3,X2)
| eq(X1,X3) ),
inference(cnf,[status(esa)],[greek_column_is_unique]) ).
cnf(l25,plain,
( ~ greek(p_1,p_2,p_2)
| ~ greek(p_1,p_1,p_2)
| eq(p_2,p_1) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(2,plain,
( ~ eq(X0,X1)
| eq(X1,X0) ),
inference(cnf,[status(esa)],[symmetry]) ).
cnf(l3,plain,
( ~ eq(p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l694,plain,
( ~ greek(p_2,p_1,p_1)
| ~ greek(p_2,p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(0,plain,
~ eq(p_1,p_2),
inference(cnf,[status(esa)],[p_1_is_not_p_2]) ).
cnf(l700,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l673,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l67,plain,
( ~ eq(p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l33,plain,
( greek(p_1,p_1,p_2)
| greek(p_1,p_1,p_1) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(5,plain,
( ~ latin(X0,X1,X2)
| ~ latin(X3,X1,X2)
| eq(X0,X3) ),
inference(cnf,[status(esa)],[latin_row_is_unique]) ).
cnf(l674,plain,
( ~ latin(p_1,p_1,p_2)
| ~ latin(p_2,p_1,p_2)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(11,plain,
( latin(p_2,X0,X1)
| latin(p_1,X0,X1) ),
inference(cnf,[status(esa)],[latin_row_required]) ).
cnf(l1,plain,
( latin(p_2,p_1,p_2)
| latin(p_1,p_1,p_2) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l703,plain,
( greek(p_2,p_2,p_1)
| greek(p_1,p_2,p_1) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(4,plain,
( ~ latin(X0,X1,X2)
| ~ latin(X0,X3,X2)
| eq(X1,X3) ),
inference(cnf,[status(esa)],[latin_column_is_unique]) ).
cnf(l289,plain,
( ~ latin(p_2,p_1,p_2)
| ~ latin(p_2,p_2,p_2)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l294,plain,
( latin(p_2,p_2,p_2)
| latin(p_1,p_2,p_2) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l684,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(16,plain,
( ~ latin(X0,X1,X2)
| ~ latin(X3,X4,X2)
| ~ greek(X0,X1,X5)
| ~ greek(X3,X4,X5)
| eq(X0,X3) ),
inference(cnf,[status(esa)],[no_two_same2]) ).
cnf(l300,plain,
( ~ latin(p_1,p_2,p_2)
| ~ latin(p_2,p_1,p_2)
| ~ greek(p_1,p_2,p_2)
| ~ greek(p_2,p_1,p_2)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l36,plain,
( ~ latin(p_2,p_1,p_2)
| ~ latin(p_1,p_1,p_2)
| ~ greek(p_2,p_1,p_1)
| ~ greek(p_1,p_1,p_1)
| eq(p_2,p_1) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l38,plain,
( ~ eq(p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l362,plain,
( latin(p_2,p_2,p_2)
| latin(p_2,p_1,p_2) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l303,plain,
( greek(p_1,p_2,p_2)
| greek(p_1,p_2,p_1) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l320,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l291,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l385,plain,
( greek(p_2,p_1,p_2)
| greek(p_1,p_1,p_2) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l404,plain,
( ~ latin(p_2,p_2,p_2)
| ~ latin(p_1,p_2,p_2)
| eq(p_2,p_1) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l304,plain,
( ~ latin(p_2,p_1,p_2)
| ~ latin(p_1,p_2,p_2)
| ~ greek(p_2,p_1,p_1)
| ~ greek(p_1,p_2,p_1)
| eq(p_2,p_1) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(6,plain,
( ~ greek(X0,X1,X2)
| ~ greek(X0,X1,X3)
| eq(X2,X3) ),
inference(cnf,[status(esa)],[greek_element_is_unique]) ).
cnf(l389,plain,
( ~ greek(p_1,p_1,p_1)
| ~ greek(p_1,p_1,p_2)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l365,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l456,plain,
( ~ eq(p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l382,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l463,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l439,plain,
( ~ eq(p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(13,plain,
( greek(X0,p_2,X1)
| greek(X0,p_1,X1) ),
inference(cnf,[status(esa)],[greek_column_required]) ).
cnf(l467,plain,
( greek(p_1,p_2,p_1)
| greek(p_1,p_1,p_1) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l792,plain,
( ~ greek(p_1,p_2,p_1)
| ~ greek(p_1,p_2,p_2)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l543,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l468,plain,
( ~ latin(p_1,p_2,p_2)
| ~ latin(p_2,p_1,p_2)
| ~ greek(p_1,p_2,p_1)
| ~ greek(p_2,p_1,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l512,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l414,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l134,plain,
( greek(p_2,p_2,p_1)
| greek(p_2,p_1,p_1) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1204,plain,
( greek(p_1,p_2,p_2)
| greek(p_1,p_1,p_2) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(9,plain,
( latin(X0,X1,p_2)
| latin(X0,X1,p_1) ),
inference(cnf,[status(esa)],[latin_cell_element]) ).
cnf(l148,plain,
( latin(p_1,p_1,p_2)
| latin(p_1,p_1,p_1) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l516,plain,
( greek(p_2,p_1,p_1)
| greek(p_1,p_1,p_1) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l397,plain,
( ~ latin(p_1,p_1,X1_1359)
| ~ latin(p_2,p_2,X1_1359)
| ~ greek(p_1,p_1,p_1)
| ~ greek(p_2,p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l208,plain,
( ~ latin(p_1,p_2,p_1)
| ~ latin(p_1,p_1,p_1)
| eq(p_2,p_1) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1246,plain,
( latin(p_2,p_2,X1_1359)
| latin(p_2,p_1,X1_1359) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l797,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1198,plain,
( latin(p_2,p_1,p_2)
| latin(p_2,p_1,p_1) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1209,plain,
( ~ latin(p_1,p_1,X1_1362)
| ~ latin(p_2,p_2,X1_1362)
| ~ greek(p_1,p_1,p_2)
| ~ greek(p_2,p_2,p_2)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l271,plain,
( latin(p_2,p_2,p_1)
| latin(p_1,p_2,p_1) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1285,plain,
( latin(p_2,p_2,X1_1362)
| latin(p_2,p_1,X1_1362) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l415,plain,
( greek(p_2,p_1,p_1)
| greek(p_1,p_1,p_1) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1244,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l622,plain,
( latin(p_1,p_2,p_2)
| latin(p_1,p_1,p_2) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l623,plain,
( ~ latin(p_1,p_1,p_2)
| ~ latin(p_2,p_2,p_2)
| ~ greek(p_1,p_1,p_1)
| ~ greek(p_2,p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l212,plain,
( ~ eq(p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l270,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1250,plain,
( ~ latin(p_2,p_1,X1_1359)
| ~ latin(p_1,p_2,X1_1359)
| ~ greek(p_2,p_1,p_2)
| ~ greek(p_1,p_2,p_2)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1413,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l657,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1289,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1417,plain,
( latin(p_2,p_2,X1_1359)
| latin(p_1,p_2,X1_1359) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1331,plain,
( greek(p_2,p_2,p_2)
| greek(p_1,p_2,p_2) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1199,plain,
( ~ latin(p_2,p_1,p_1)
| ~ latin(p_1,p_1,p_1)
| eq(p_2,p_1) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1301,plain,
( greek(p_2,p_2,p_1)
| greek(p_1,p_2,p_1) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1253,plain,
( greek(p_2,p_1,p_2)
| greek(p_1,p_1,p_2) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1316,plain,
( ~ latin(p_2,p_1,X1_1362)
| ~ latin(p_1,p_2,X1_1362)
| ~ greek(p_2,p_1,p_1)
| ~ greek(p_1,p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1317,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1245,plain,
( latin(p_1,p_2,X1_1359)
| latin(p_1,p_1,X1_1359) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1412,plain,
( latin(p_2,p_2,X1_1362)
| latin(p_1,p_2,X1_1362) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1202,plain,
( ~ eq(p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1211,plain,
( latin(p_1,p_2,X1_1362)
| latin(p_1,p_1,X1_1362) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1203,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l281,plain,
( ~ latin(p_1,p_1,p_1)
| ~ latin(p_2,p_2,p_1)
| ~ greek(p_1,p_1,p_1)
| ~ greek(p_2,p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1216,plain,
( ~ latin(p_1,p_2,X1_1362)
| ~ latin(p_2,p_1,X1_1362)
| ~ greek(p_1,p_2,p_1)
| ~ greek(p_2,p_1,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1408,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l419,plain,
( ~ greek(p_1,p_1,p_1)
| ~ greek(p_1,p_1,p_2)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1286,plain,
( ~ latin(p_2,p_1,X1_1359)
| ~ latin(p_1,p_2,X1_1359)
| ~ greek(p_2,p_1,p_2)
| ~ greek(p_1,p_2,p_2)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1362,plain,
( latin(p_2,p_1,X1_1362)
| latin(p_1,p_1,X1_1362) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1396,plain,
( greek(p_2,p_2,p_1)
| greek(p_1,p_2,p_1) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1303,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1300,plain,
( greek(p_2,p_1,p_2)
| greek(p_1,p_1,p_2) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1233,plain,
( latin(p_1,p_2,p_1)
| latin(p_1,p_1,p_1) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1383,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1359,plain,
( latin(p_2,p_1,X1_1359)
| latin(p_1,p_1,X1_1359) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1263,plain,
( greek(p_1,p_2,p_2)
| greek(p_1,p_1,p_2) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1373,plain,
( ~ latin(p_1,p_2,p_1)
| ~ latin(p_2,p_1,p_1)
| ~ greek(p_1,p_2,X1_1485)
| ~ greek(p_2,p_1,X1_1485)
| eq(p_2,p_1) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1374,plain,
( ~ eq(p_2,p_1)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1270,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1477,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1381,plain,
( greek(p_2,p_1,X1_1485)
| greek(p_1,p_1,X1_1485) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1435,plain,
( greek(p_1,p_2,X1_1485)
| greek(p_1,p_1,X1_1485) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1483,plain,
( ~ latin(p_1,p_1,p_2)
| ~ latin(p_2,p_2,p_2)
| ~ greek(p_1,p_1,X1_1485)
| ~ greek(p_2,p_2,X1_1485)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1491,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1437,plain,
( ~ latin(p_1,p_1,p_2)
| ~ latin(p_2,p_2,p_2)
| ~ greek(p_1,p_1,X1_1485)
| ~ greek(p_2,p_2,X1_1485)
| eq(p_1,p_2) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1492,plain,
( greek(p_2,p_2,X1_1485)
| greek(p_2,p_1,X1_1485) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1482,plain,
~ eq(p_1,p_2),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1486,plain,
( latin(p_2,p_2,p_2)
| latin(p_1,p_2,p_2) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1489,plain,
( latin(p_2,p_2,p_2)
| latin(p_1,p_2,p_2) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1485,plain,
( greek(p_2,p_2,X1_1485)
| greek(p_1,p_2,X1_1485) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l5,l2,l10,l25,l3,l694,l700,l673,l67,l33,l674,l1,l703,l289,l294,l684,l300,l36,l38,l362,l303,l320,l291,l385,l404,l304,l389,l365,l456,l382,l463,l439,l467,l792,l543,l468,l512,l414,l134,l1204,l148,l516,l397,l208,l1246,l797,l1198,l1209,l271,l1285,l415,l1244,l622,l623,l212,l270,l1250,l1413,l657,l1289,l1417,l1331,l1199,l1301,l1253,l1316,l1317,l1245,l1412,l1202,l1211,l1203,l281,l1216,l1408,l419,l1286,l1362,l1396,l1303,l1300,l1233,l1383,l1359,l1263,l1373,l1374,l1270,l1477,l1381,l1435,l1483,l1491,l1437,l1492,l1482,l1486,l1489,l1485]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : MSC008-1.002 : TPTP v9.0.0. Released v1.0.0.
% 0.06/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n020.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:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.33 % launching worker at depth: 3
% 0.12/0.33 % launching worker at depth: 7
% 0.12/0.33 % launching worker at depth: 5
% 0.12/0.33 % launching worker at depth: 4
% 0.12/0.33 % launching worker at depth: 8
% 0.12/0.33 % launching worker at depth: 2
% 0.12/0.33 % launching worker at depth: 1
% 0.12/0.33 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 0.19/0.55 % launching worker at depth: 11
% 2.95/0.76 % launching worker at depth: 12
% 30.08/4.17 % SZS status Theorem for theBenchmark
% 30.08/4.17 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------