%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : PUZ077+1 : TPTP v8.1.0. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% 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 : 600s
% DateTime : Mon Jul 18 18:08:28 EDT 2022
% Result : Theorem 21.12s 4.43s
% Output : CNFRefutation 21.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 60
% Syntax : Number of clauses : 216 ( 44 unt; 0 nHn; 216 RR)
% Number of literals : 610 ( 72 equ; 418 neg)
% Maximal clause size : 18 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 45 ( 43 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 508 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_3,plain,
( north(X1,X2)
| ~ epred36_2(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_3) ).
cnf(i_0_1350,plain,
( epred36_2(X1,X2)
| ~ epred35_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1350) ).
cnf(i_0_1312,plain,
( epred35_2(X1,X2)
| ~ epred34_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1312) ).
cnf(i_0_1274,plain,
( epred34_2(X1,X2)
| ~ epred33_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1274) ).
cnf(i_0_1236,plain,
( epred33_2(X1,X2)
| ~ epred32_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1236) ).
cnf(i_0_1198,plain,
( epred32_2(X1,X2)
| ~ epred31_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1198) ).
cnf(i_0_1160,plain,
( epred31_2(X1,X2)
| ~ epred30_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1160) ).
cnf(i_0_1122,plain,
( epred30_2(X1,X2)
| ~ epred29_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1122) ).
cnf(i_0_1084,plain,
( epred29_2(X1,X2)
| ~ epred28_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1084) ).
cnf(i_0_1046,plain,
( epred28_2(X1,X2)
| ~ epred27_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1046) ).
cnf(i_0_1008,plain,
( epred27_2(X1,X2)
| ~ epred26_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1008) ).
cnf(i_0_970,plain,
( epred26_2(X1,X2)
| ~ epred25_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_970) ).
cnf(i_0_1,plain,
( west(X1,X2)
| ~ epred18_2(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1) ).
cnf(i_0_667,plain,
( epred18_2(X1,X2)
| ~ epred17_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_667) ).
cnf(i_0_16,negated_conjecture,
~ westof(cell1,cell100),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_16) ).
cnf(i_0_12,plain,
( westof(X1,X2)
| ~ duewest(X3,X2)
| ~ vert(X1,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_12) ).
cnf(i_0_932,plain,
( epred25_2(X1,X2)
| ~ epred24_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_932) ).
cnf(i_0_629,plain,
( epred17_2(X1,X2)
| ~ epred16_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_629) ).
cnf(i_0_10,plain,
( vert(X1,X2)
| ~ duenorth(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_10) ).
cnf(i_0_894,plain,
( epred24_2(X1,X2)
| ~ epred23_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_894) ).
cnf(i_0_591,plain,
( epred16_2(X1,X2)
| ~ epred15_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_591) ).
cnf(i_0_7,plain,
( duenorth(X1,X2)
| ~ epred42_2(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_7) ).
cnf(i_0_856,plain,
( epred23_2(X1,X2)
| ~ epred22_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_856) ).
cnf(i_0_553,plain,
( epred15_2(X1,X2)
| ~ epred14_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_553) ).
cnf(i_0_1798,plain,
( epred42_2(X1,X2)
| ~ north(X3,X1)
| ~ north(X4,X3)
| ~ north(X5,X4)
| ~ north(X6,X5)
| ~ north(X7,X6)
| ~ north(X8,X7)
| ~ north(X9,X8)
| ~ north(X10,X9)
| ~ north(X2,X10) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1798) ).
cnf(i_0_818,plain,
( epred22_2(X1,X2)
| ~ epred21_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_818) ).
cnf(i_0_704,plain,
( epred19_2(X1,X2)
| X1 != cell2
| X2 != cell1 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_704) ).
cnf(i_0_515,plain,
( epred14_2(X1,X2)
| ~ epred13_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_515) ).
cnf(i_0_5,plain,
( duewest(X1,X2)
| ~ epred39_2(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_5) ).
cnf(i_0_780,plain,
( epred21_2(X1,X2)
| ~ epred20_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_780) ).
cnf(i_0_742,plain,
( epred20_2(X1,X2)
| ~ epred19_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_742) ).
cnf(i_0_703,plain,
( epred19_2(X1,X2)
| X1 != cell3
| X2 != cell2 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_703) ).
cnf(i_0_477,plain,
( epred13_2(X1,X2)
| ~ epred12_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_477) ).
cnf(i_0_1553,plain,
( epred39_2(X1,X2)
| ~ west(X3,X1)
| ~ west(X4,X3)
| ~ west(X5,X4)
| ~ west(X6,X5)
| ~ west(X7,X6)
| ~ west(X8,X7)
| ~ west(X9,X8)
| ~ west(X10,X9)
| ~ west(X2,X10) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_1553) ).
cnf(i_0_702,plain,
( epred19_2(X1,X2)
| X1 != cell4
| X2 != cell3 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_702) ).
cnf(i_0_439,plain,
( epred12_2(X1,X2)
| ~ epred11_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_439) ).
cnf(i_0_701,plain,
( epred19_2(X1,X2)
| X1 != cell5
| X2 != cell4 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_701) ).
cnf(i_0_401,plain,
( epred11_2(X1,X2)
| ~ epred10_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_401) ).
cnf(i_0_700,plain,
( epred19_2(X1,X2)
| X1 != cell6
| X2 != cell5 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_700) ).
cnf(i_0_363,plain,
( epred10_2(X1,X2)
| ~ epred9_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_363) ).
cnf(i_0_325,plain,
( epred9_2(X1,X2)
| ~ epred8_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_325) ).
cnf(i_0_741,plain,
( epred20_2(X1,X2)
| X1 != cell7
| X2 != cell6 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_741) ).
cnf(i_0_287,plain,
( epred8_2(X1,X2)
| ~ epred7_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_287) ).
cnf(i_0_740,plain,
( epred20_2(X1,X2)
| X1 != cell8
| X2 != cell7 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_740) ).
cnf(i_0_249,plain,
( epred7_2(X1,X2)
| ~ epred6_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_249) ).
cnf(i_0_739,plain,
( epred20_2(X1,X2)
| X1 != cell9
| X2 != cell8 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_739) ).
cnf(i_0_211,plain,
( epred6_2(X1,X2)
| ~ epred5_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_211) ).
cnf(i_0_738,plain,
( epred20_2(X1,X2)
| X1 != cell10
| X2 != cell9 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_738) ).
cnf(i_0_173,plain,
( epred5_2(X1,X2)
| ~ epred4_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_173) ).
cnf(i_0_662,plain,
( epred18_2(X1,X2)
| X1 != cell100
| X2 != cell90 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_662) ).
cnf(i_0_135,plain,
( epred4_2(X1,X2)
| ~ epred3_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_135) ).
cnf(i_0_97,plain,
( epred3_2(X1,X2)
| ~ epred2_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_97) ).
cnf(i_0_54,plain,
( epred2_2(X1,X2)
| X1 != cell20
| X2 != cell10 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_54) ).
cnf(i_0_586,plain,
( epred16_2(X1,X2)
| X1 != cell90
| X2 != cell80 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_586) ).
cnf(i_0_130,plain,
( epred4_2(X1,X2)
| X1 != cell30
| X2 != cell20 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_130) ).
cnf(i_0_510,plain,
( epred14_2(X1,X2)
| X1 != cell80
| X2 != cell70 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_510) ).
cnf(i_0_206,plain,
( epred6_2(X1,X2)
| X1 != cell40
| X2 != cell30 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_206) ).
cnf(i_0_434,plain,
( epred12_2(X1,X2)
| X1 != cell70
| X2 != cell60 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_434) ).
cnf(i_0_282,plain,
( epred8_2(X1,X2)
| X1 != cell50
| X2 != cell40 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_282) ).
cnf(i_0_358,plain,
( epred10_2(X1,X2)
| X1 != cell60
| X2 != cell50 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-5oeuobba/input.p',i_0_358) ).
cnf(c_0_1859,plain,
( north(X1,X2)
| ~ epred36_2(X2,X1) ),
i_0_3 ).
cnf(c_0_1860,plain,
( epred36_2(X1,X2)
| ~ epred35_2(X1,X2) ),
i_0_1350 ).
cnf(c_0_1861,plain,
( north(X1,X2)
| ~ epred35_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1859,c_0_1860]) ).
cnf(c_0_1862,plain,
( epred35_2(X1,X2)
| ~ epred34_2(X1,X2) ),
i_0_1312 ).
cnf(c_0_1863,plain,
( north(X1,X2)
| ~ epred34_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1861,c_0_1862]) ).
cnf(c_0_1864,plain,
( epred34_2(X1,X2)
| ~ epred33_2(X1,X2) ),
i_0_1274 ).
cnf(c_0_1865,plain,
( north(X1,X2)
| ~ epred33_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1863,c_0_1864]) ).
cnf(c_0_1866,plain,
( epred33_2(X1,X2)
| ~ epred32_2(X1,X2) ),
i_0_1236 ).
cnf(c_0_1867,plain,
( north(X1,X2)
| ~ epred32_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1865,c_0_1866]) ).
cnf(c_0_1868,plain,
( epred32_2(X1,X2)
| ~ epred31_2(X1,X2) ),
i_0_1198 ).
cnf(c_0_1869,plain,
( north(X1,X2)
| ~ epred31_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1867,c_0_1868]) ).
cnf(c_0_1870,plain,
( epred31_2(X1,X2)
| ~ epred30_2(X1,X2) ),
i_0_1160 ).
cnf(c_0_1871,plain,
( north(X1,X2)
| ~ epred30_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1869,c_0_1870]) ).
cnf(c_0_1872,plain,
( epred30_2(X1,X2)
| ~ epred29_2(X1,X2) ),
i_0_1122 ).
cnf(c_0_1873,plain,
( north(X1,X2)
| ~ epred29_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1871,c_0_1872]) ).
cnf(c_0_1874,plain,
( epred29_2(X1,X2)
| ~ epred28_2(X1,X2) ),
i_0_1084 ).
cnf(c_0_1875,plain,
( north(X1,X2)
| ~ epred28_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1873,c_0_1874]) ).
cnf(c_0_1876,plain,
( epred28_2(X1,X2)
| ~ epred27_2(X1,X2) ),
i_0_1046 ).
cnf(c_0_1877,plain,
( north(X1,X2)
| ~ epred27_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1875,c_0_1876]) ).
cnf(c_0_1878,plain,
( epred27_2(X1,X2)
| ~ epred26_2(X1,X2) ),
i_0_1008 ).
cnf(c_0_1879,plain,
( north(X1,X2)
| ~ epred26_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1877,c_0_1878]) ).
cnf(c_0_1880,plain,
( epred26_2(X1,X2)
| ~ epred25_2(X1,X2) ),
i_0_970 ).
cnf(c_0_1881,plain,
( west(X1,X2)
| ~ epred18_2(X2,X1) ),
i_0_1 ).
cnf(c_0_1882,plain,
( epred18_2(X1,X2)
| ~ epred17_2(X1,X2) ),
i_0_667 ).
cnf(c_0_1883,negated_conjecture,
~ westof(cell1,cell100),
i_0_16 ).
cnf(c_0_1884,plain,
( westof(X1,X2)
| ~ duewest(X3,X2)
| ~ vert(X1,X3) ),
i_0_12 ).
cnf(c_0_1885,plain,
( north(X1,X2)
| ~ epred25_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1879,c_0_1880]) ).
cnf(c_0_1886,plain,
( epred25_2(X1,X2)
| ~ epred24_2(X1,X2) ),
i_0_932 ).
cnf(c_0_1887,plain,
( west(X1,X2)
| ~ epred17_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1881,c_0_1882]) ).
cnf(c_0_1888,plain,
( epred17_2(X1,X2)
| ~ epred16_2(X1,X2) ),
i_0_629 ).
cnf(c_0_1889,negated_conjecture,
( ~ vert(cell1,X1)
| ~ duewest(X1,cell100) ),
inference(spm,[status(thm)],[c_0_1883,c_0_1884]) ).
cnf(c_0_1890,plain,
( vert(X1,X2)
| ~ duenorth(X1,X2) ),
i_0_10 ).
cnf(c_0_1891,plain,
( north(X1,X2)
| ~ epred24_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1885,c_0_1886]) ).
cnf(c_0_1892,plain,
( epred24_2(X1,X2)
| ~ epred23_2(X1,X2) ),
i_0_894 ).
cnf(c_0_1893,plain,
( west(X1,X2)
| ~ epred16_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1887,c_0_1888]) ).
cnf(c_0_1894,plain,
( epred16_2(X1,X2)
| ~ epred15_2(X1,X2) ),
i_0_591 ).
cnf(c_0_1895,plain,
( ~ duenorth(cell1,X1)
| ~ duewest(X1,cell100) ),
inference(spm,[status(thm)],[c_0_1889,c_0_1890]) ).
cnf(c_0_1896,plain,
( duenorth(X1,X2)
| ~ epred42_2(X2,X1) ),
i_0_7 ).
cnf(c_0_1897,plain,
( north(X1,X2)
| ~ epred23_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1891,c_0_1892]) ).
cnf(c_0_1898,plain,
( epred23_2(X1,X2)
| ~ epred22_2(X1,X2) ),
i_0_856 ).
cnf(c_0_1899,plain,
( west(X1,X2)
| ~ epred15_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1893,c_0_1894]) ).
cnf(c_0_1900,plain,
( epred15_2(X1,X2)
| ~ epred14_2(X1,X2) ),
i_0_553 ).
cnf(c_0_1901,plain,
( ~ epred42_2(X1,cell1)
| ~ duewest(X1,cell100) ),
inference(spm,[status(thm)],[c_0_1895,c_0_1896]) ).
cnf(c_0_1902,plain,
( epred42_2(X1,X2)
| ~ north(X3,X1)
| ~ north(X4,X3)
| ~ north(X5,X4)
| ~ north(X6,X5)
| ~ north(X7,X6)
| ~ north(X8,X7)
| ~ north(X9,X8)
| ~ north(X10,X9)
| ~ north(X2,X10) ),
i_0_1798 ).
cnf(c_0_1903,plain,
( north(X1,X2)
| ~ epred22_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1897,c_0_1898]) ).
cnf(c_0_1904,plain,
( epred22_2(X1,X2)
| ~ epred21_2(X1,X2) ),
i_0_818 ).
cnf(c_0_1905,plain,
( epred19_2(X1,X2)
| X1 != cell2
| X2 != cell1 ),
i_0_704 ).
cnf(c_0_1906,plain,
( west(X1,X2)
| ~ epred14_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1899,c_0_1900]) ).
cnf(c_0_1907,plain,
( epred14_2(X1,X2)
| ~ epred13_2(X1,X2) ),
i_0_515 ).
cnf(c_0_1908,plain,
( ~ duewest(X1,cell100)
| ~ north(cell1,X2)
| ~ north(X2,X3)
| ~ north(X3,X4)
| ~ north(X4,X5)
| ~ north(X5,X6)
| ~ north(X6,X7)
| ~ north(X7,X8)
| ~ north(X8,X9)
| ~ north(X9,X1) ),
inference(spm,[status(thm)],[c_0_1901,c_0_1902]) ).
cnf(c_0_1909,plain,
( duewest(X1,X2)
| ~ epred39_2(X2,X1) ),
i_0_5 ).
cnf(c_0_1910,plain,
( north(X1,X2)
| ~ epred21_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1903,c_0_1904]) ).
cnf(c_0_1911,plain,
( epred21_2(X1,X2)
| ~ epred20_2(X1,X2) ),
i_0_780 ).
cnf(c_0_1912,plain,
( epred20_2(X1,X2)
| ~ epred19_2(X1,X2) ),
i_0_742 ).
cnf(c_0_1913,plain,
epred19_2(cell2,cell1),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1905])]) ).
cnf(c_0_1914,plain,
( epred19_2(X1,X2)
| X1 != cell3
| X2 != cell2 ),
i_0_703 ).
cnf(c_0_1915,plain,
( west(X1,X2)
| ~ epred13_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1906,c_0_1907]) ).
cnf(c_0_1916,plain,
( epred13_2(X1,X2)
| ~ epred12_2(X1,X2) ),
i_0_477 ).
cnf(c_0_1917,plain,
( ~ epred39_2(cell100,X1)
| ~ north(cell1,X2)
| ~ north(X2,X3)
| ~ north(X3,X4)
| ~ north(X4,X5)
| ~ north(X5,X6)
| ~ north(X6,X7)
| ~ north(X7,X8)
| ~ north(X8,X9)
| ~ north(X9,X1) ),
inference(spm,[status(thm)],[c_0_1908,c_0_1909]) ).
cnf(c_0_1918,plain,
( epred39_2(X1,X2)
| ~ west(X3,X1)
| ~ west(X4,X3)
| ~ west(X5,X4)
| ~ west(X6,X5)
| ~ west(X7,X6)
| ~ west(X8,X7)
| ~ west(X9,X8)
| ~ west(X10,X9)
| ~ west(X2,X10) ),
i_0_1553 ).
cnf(c_0_1919,plain,
( north(X1,X2)
| ~ epred20_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1910,c_0_1911]) ).
cnf(c_0_1920,plain,
epred20_2(cell2,cell1),
inference(spm,[status(thm)],[c_0_1912,c_0_1913]) ).
cnf(c_0_1921,plain,
epred19_2(cell3,cell2),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1914])]) ).
cnf(c_0_1922,plain,
( epred19_2(X1,X2)
| X1 != cell4
| X2 != cell3 ),
i_0_702 ).
cnf(c_0_1923,plain,
( west(X1,X2)
| ~ epred12_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1915,c_0_1916]) ).
cnf(c_0_1924,plain,
( epred12_2(X1,X2)
| ~ epred11_2(X1,X2) ),
i_0_439 ).
cnf(c_0_1925,plain,
( ~ north(cell1,X1)
| ~ north(X1,X2)
| ~ north(X2,X3)
| ~ north(X3,X4)
| ~ north(X4,X5)
| ~ north(X5,X6)
| ~ north(X6,X7)
| ~ north(X7,X8)
| ~ north(X8,X9)
| ~ west(X10,cell100)
| ~ west(X11,X12)
| ~ west(X12,X13)
| ~ west(X13,X14)
| ~ west(X14,X15)
| ~ west(X15,X16)
| ~ west(X16,X17)
| ~ west(X17,X10)
| ~ west(X9,X11) ),
inference(spm,[status(thm)],[c_0_1917,c_0_1918]) ).
cnf(c_0_1926,plain,
north(cell1,cell2),
inference(spm,[status(thm)],[c_0_1919,c_0_1920]) ).
cnf(c_0_1927,plain,
epred20_2(cell3,cell2),
inference(spm,[status(thm)],[c_0_1912,c_0_1921]) ).
cnf(c_0_1928,plain,
epred19_2(cell4,cell3),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1922])]) ).
cnf(c_0_1929,plain,
( epred19_2(X1,X2)
| X1 != cell5
| X2 != cell4 ),
i_0_701 ).
cnf(c_0_1930,plain,
( west(X1,X2)
| ~ epred11_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1923,c_0_1924]) ).
cnf(c_0_1931,plain,
( epred11_2(X1,X2)
| ~ epred10_2(X1,X2) ),
i_0_401 ).
cnf(c_0_1932,plain,
( ~ north(cell2,X1)
| ~ north(X1,X2)
| ~ north(X2,X3)
| ~ north(X3,X4)
| ~ north(X4,X5)
| ~ north(X5,X6)
| ~ north(X6,X7)
| ~ north(X7,X8)
| ~ west(X9,cell100)
| ~ west(X10,X11)
| ~ west(X11,X12)
| ~ west(X12,X13)
| ~ west(X13,X14)
| ~ west(X14,X15)
| ~ west(X15,X16)
| ~ west(X16,X9)
| ~ west(X8,X10) ),
inference(spm,[status(thm)],[c_0_1925,c_0_1926]) ).
cnf(c_0_1933,plain,
north(cell2,cell3),
inference(spm,[status(thm)],[c_0_1919,c_0_1927]) ).
cnf(c_0_1934,plain,
epred20_2(cell4,cell3),
inference(spm,[status(thm)],[c_0_1912,c_0_1928]) ).
cnf(c_0_1935,plain,
epred19_2(cell5,cell4),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1929])]) ).
cnf(c_0_1936,plain,
( epred19_2(X1,X2)
| X1 != cell6
| X2 != cell5 ),
i_0_700 ).
cnf(c_0_1937,plain,
( west(X1,X2)
| ~ epred10_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1930,c_0_1931]) ).
cnf(c_0_1938,plain,
( epred10_2(X1,X2)
| ~ epred9_2(X1,X2) ),
i_0_363 ).
cnf(c_0_1939,plain,
( ~ north(cell3,X1)
| ~ north(X1,X2)
| ~ north(X2,X3)
| ~ north(X3,X4)
| ~ north(X4,X5)
| ~ north(X5,X6)
| ~ north(X6,X7)
| ~ west(X8,cell100)
| ~ west(X9,X10)
| ~ west(X10,X11)
| ~ west(X11,X12)
| ~ west(X12,X13)
| ~ west(X13,X14)
| ~ west(X14,X15)
| ~ west(X15,X8)
| ~ west(X7,X9) ),
inference(spm,[status(thm)],[c_0_1932,c_0_1933]) ).
cnf(c_0_1940,plain,
north(cell3,cell4),
inference(spm,[status(thm)],[c_0_1919,c_0_1934]) ).
cnf(c_0_1941,plain,
epred20_2(cell5,cell4),
inference(spm,[status(thm)],[c_0_1912,c_0_1935]) ).
cnf(c_0_1942,plain,
epred19_2(cell6,cell5),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1936])]) ).
cnf(c_0_1943,plain,
( west(X1,X2)
| ~ epred9_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1937,c_0_1938]) ).
cnf(c_0_1944,plain,
( epred9_2(X1,X2)
| ~ epred8_2(X1,X2) ),
i_0_325 ).
cnf(c_0_1945,plain,
( ~ north(cell4,X1)
| ~ north(X1,X2)
| ~ north(X2,X3)
| ~ north(X3,X4)
| ~ north(X4,X5)
| ~ north(X5,X6)
| ~ west(X7,cell100)
| ~ west(X8,X9)
| ~ west(X9,X10)
| ~ west(X10,X11)
| ~ west(X11,X12)
| ~ west(X12,X13)
| ~ west(X13,X14)
| ~ west(X14,X7)
| ~ west(X6,X8) ),
inference(spm,[status(thm)],[c_0_1939,c_0_1940]) ).
cnf(c_0_1946,plain,
north(cell4,cell5),
inference(spm,[status(thm)],[c_0_1919,c_0_1941]) ).
cnf(c_0_1947,plain,
epred20_2(cell6,cell5),
inference(spm,[status(thm)],[c_0_1912,c_0_1942]) ).
cnf(c_0_1948,plain,
( epred20_2(X1,X2)
| X1 != cell7
| X2 != cell6 ),
i_0_741 ).
cnf(c_0_1949,plain,
( west(X1,X2)
| ~ epred8_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1943,c_0_1944]) ).
cnf(c_0_1950,plain,
( epred8_2(X1,X2)
| ~ epred7_2(X1,X2) ),
i_0_287 ).
cnf(c_0_1951,plain,
( ~ north(cell5,X1)
| ~ north(X1,X2)
| ~ north(X2,X3)
| ~ north(X3,X4)
| ~ north(X4,X5)
| ~ west(X6,cell100)
| ~ west(X7,X8)
| ~ west(X8,X9)
| ~ west(X9,X10)
| ~ west(X10,X11)
| ~ west(X11,X12)
| ~ west(X12,X13)
| ~ west(X13,X6)
| ~ west(X5,X7) ),
inference(spm,[status(thm)],[c_0_1945,c_0_1946]) ).
cnf(c_0_1952,plain,
north(cell5,cell6),
inference(spm,[status(thm)],[c_0_1919,c_0_1947]) ).
cnf(c_0_1953,plain,
epred20_2(cell7,cell6),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1948])]) ).
cnf(c_0_1954,plain,
( epred20_2(X1,X2)
| X1 != cell8
| X2 != cell7 ),
i_0_740 ).
cnf(c_0_1955,plain,
( west(X1,X2)
| ~ epred7_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1949,c_0_1950]) ).
cnf(c_0_1956,plain,
( epred7_2(X1,X2)
| ~ epred6_2(X1,X2) ),
i_0_249 ).
cnf(c_0_1957,plain,
( ~ north(cell6,X1)
| ~ north(X1,X2)
| ~ north(X2,X3)
| ~ north(X3,X4)
| ~ west(X5,cell100)
| ~ west(X6,X7)
| ~ west(X7,X8)
| ~ west(X8,X9)
| ~ west(X9,X10)
| ~ west(X10,X11)
| ~ west(X11,X12)
| ~ west(X12,X5)
| ~ west(X4,X6) ),
inference(spm,[status(thm)],[c_0_1951,c_0_1952]) ).
cnf(c_0_1958,plain,
north(cell6,cell7),
inference(spm,[status(thm)],[c_0_1919,c_0_1953]) ).
cnf(c_0_1959,plain,
epred20_2(cell8,cell7),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1954])]) ).
cnf(c_0_1960,plain,
( epred20_2(X1,X2)
| X1 != cell9
| X2 != cell8 ),
i_0_739 ).
cnf(c_0_1961,plain,
( west(X1,X2)
| ~ epred6_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1955,c_0_1956]) ).
cnf(c_0_1962,plain,
( epred6_2(X1,X2)
| ~ epred5_2(X1,X2) ),
i_0_211 ).
cnf(c_0_1963,plain,
( ~ north(cell7,X1)
| ~ north(X1,X2)
| ~ north(X2,X3)
| ~ west(X4,cell100)
| ~ west(X5,X6)
| ~ west(X6,X7)
| ~ west(X7,X8)
| ~ west(X8,X9)
| ~ west(X9,X10)
| ~ west(X10,X11)
| ~ west(X11,X4)
| ~ west(X3,X5) ),
inference(spm,[status(thm)],[c_0_1957,c_0_1958]) ).
cnf(c_0_1964,plain,
north(cell7,cell8),
inference(spm,[status(thm)],[c_0_1919,c_0_1959]) ).
cnf(c_0_1965,plain,
epred20_2(cell9,cell8),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1960])]) ).
cnf(c_0_1966,plain,
( epred20_2(X1,X2)
| X1 != cell10
| X2 != cell9 ),
i_0_738 ).
cnf(c_0_1967,plain,
( west(X1,X2)
| ~ epred5_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1961,c_0_1962]) ).
cnf(c_0_1968,plain,
( epred5_2(X1,X2)
| ~ epred4_2(X1,X2) ),
i_0_173 ).
cnf(c_0_1969,plain,
( ~ north(cell8,X1)
| ~ north(X1,X2)
| ~ west(X3,cell100)
| ~ west(X4,X5)
| ~ west(X5,X6)
| ~ west(X6,X7)
| ~ west(X7,X8)
| ~ west(X8,X9)
| ~ west(X9,X10)
| ~ west(X10,X3)
| ~ west(X2,X4) ),
inference(spm,[status(thm)],[c_0_1963,c_0_1964]) ).
cnf(c_0_1970,plain,
north(cell8,cell9),
inference(spm,[status(thm)],[c_0_1919,c_0_1965]) ).
cnf(c_0_1971,plain,
epred20_2(cell10,cell9),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1966])]) ).
cnf(c_0_1972,plain,
( epred18_2(X1,X2)
| X1 != cell100
| X2 != cell90 ),
i_0_662 ).
cnf(c_0_1973,plain,
( west(X1,X2)
| ~ epred4_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1967,c_0_1968]) ).
cnf(c_0_1974,plain,
( epred4_2(X1,X2)
| ~ epred3_2(X1,X2) ),
i_0_135 ).
cnf(c_0_1975,plain,
( ~ north(cell9,X1)
| ~ west(X2,cell100)
| ~ west(X3,X4)
| ~ west(X4,X5)
| ~ west(X5,X6)
| ~ west(X6,X7)
| ~ west(X7,X8)
| ~ west(X8,X9)
| ~ west(X9,X2)
| ~ west(X1,X3) ),
inference(spm,[status(thm)],[c_0_1969,c_0_1970]) ).
cnf(c_0_1976,plain,
north(cell9,cell10),
inference(spm,[status(thm)],[c_0_1919,c_0_1971]) ).
cnf(c_0_1977,plain,
epred18_2(cell100,cell90),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1972])]) ).
cnf(c_0_1978,plain,
( west(X1,X2)
| ~ epred3_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1973,c_0_1974]) ).
cnf(c_0_1979,plain,
( epred3_2(X1,X2)
| ~ epred2_2(X1,X2) ),
i_0_97 ).
cnf(c_0_1980,plain,
( epred2_2(X1,X2)
| X1 != cell20
| X2 != cell10 ),
i_0_54 ).
cnf(c_0_1981,plain,
( ~ west(X1,cell100)
| ~ west(cell10,X2)
| ~ west(X2,X3)
| ~ west(X3,X4)
| ~ west(X4,X5)
| ~ west(X5,X6)
| ~ west(X6,X7)
| ~ west(X7,X8)
| ~ west(X8,X1) ),
inference(spm,[status(thm)],[c_0_1975,c_0_1976]) ).
cnf(c_0_1982,plain,
west(cell90,cell100),
inference(spm,[status(thm)],[c_0_1881,c_0_1977]) ).
cnf(c_0_1983,plain,
( west(X1,X2)
| ~ epred2_2(X2,X1) ),
inference(spm,[status(thm)],[c_0_1978,c_0_1979]) ).
cnf(c_0_1984,plain,
epred2_2(cell20,cell10),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1980])]) ).
cnf(c_0_1985,plain,
( epred16_2(X1,X2)
| X1 != cell90
| X2 != cell80 ),
i_0_586 ).
cnf(c_0_1986,plain,
( ~ west(cell10,X1)
| ~ west(X2,cell90)
| ~ west(X1,X3)
| ~ west(X3,X4)
| ~ west(X4,X5)
| ~ west(X5,X6)
| ~ west(X6,X7)
| ~ west(X7,X2) ),
inference(spm,[status(thm)],[c_0_1981,c_0_1982]) ).
cnf(c_0_1987,plain,
west(cell10,cell20),
inference(spm,[status(thm)],[c_0_1983,c_0_1984]) ).
cnf(c_0_1988,plain,
epred16_2(cell90,cell80),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1985])]) ).
cnf(c_0_1989,plain,
( epred4_2(X1,X2)
| X1 != cell30
| X2 != cell20 ),
i_0_130 ).
cnf(c_0_1990,plain,
( ~ west(X1,cell90)
| ~ west(cell20,X2)
| ~ west(X2,X3)
| ~ west(X3,X4)
| ~ west(X4,X5)
| ~ west(X5,X6)
| ~ west(X6,X1) ),
inference(spm,[status(thm)],[c_0_1986,c_0_1987]) ).
cnf(c_0_1991,plain,
west(cell80,cell90),
inference(spm,[status(thm)],[c_0_1893,c_0_1988]) ).
cnf(c_0_1992,plain,
epred4_2(cell30,cell20),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1989])]) ).
cnf(c_0_1993,plain,
( epred14_2(X1,X2)
| X1 != cell80
| X2 != cell70 ),
i_0_510 ).
cnf(c_0_1994,plain,
( ~ west(cell20,X1)
| ~ west(X2,cell80)
| ~ west(X1,X3)
| ~ west(X3,X4)
| ~ west(X4,X5)
| ~ west(X5,X2) ),
inference(spm,[status(thm)],[c_0_1990,c_0_1991]) ).
cnf(c_0_1995,plain,
west(cell20,cell30),
inference(spm,[status(thm)],[c_0_1973,c_0_1992]) ).
cnf(c_0_1996,plain,
epred14_2(cell80,cell70),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1993])]) ).
cnf(c_0_1997,plain,
( epred6_2(X1,X2)
| X1 != cell40
| X2 != cell30 ),
i_0_206 ).
cnf(c_0_1998,plain,
( ~ west(X1,cell80)
| ~ west(cell30,X2)
| ~ west(X2,X3)
| ~ west(X3,X4)
| ~ west(X4,X1) ),
inference(spm,[status(thm)],[c_0_1994,c_0_1995]) ).
cnf(c_0_1999,plain,
west(cell70,cell80),
inference(spm,[status(thm)],[c_0_1906,c_0_1996]) ).
cnf(c_0_2000,plain,
epred6_2(cell40,cell30),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_1997])]) ).
cnf(c_0_2001,plain,
( epred12_2(X1,X2)
| X1 != cell70
| X2 != cell60 ),
i_0_434 ).
cnf(c_0_2002,plain,
( ~ west(cell30,X1)
| ~ west(X2,cell70)
| ~ west(X1,X3)
| ~ west(X3,X2) ),
inference(spm,[status(thm)],[c_0_1998,c_0_1999]) ).
cnf(c_0_2003,plain,
west(cell30,cell40),
inference(spm,[status(thm)],[c_0_1961,c_0_2000]) ).
cnf(c_0_2004,plain,
epred12_2(cell70,cell60),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_2001])]) ).
cnf(c_0_2005,plain,
( epred8_2(X1,X2)
| X1 != cell50
| X2 != cell40 ),
i_0_282 ).
cnf(c_0_2006,plain,
( epred10_2(X1,X2)
| X1 != cell60
| X2 != cell50 ),
i_0_358 ).
cnf(c_0_2007,plain,
( ~ west(X1,cell70)
| ~ west(cell40,X2)
| ~ west(X2,X1) ),
inference(spm,[status(thm)],[c_0_2002,c_0_2003]) ).
cnf(c_0_2008,plain,
west(cell60,cell70),
inference(spm,[status(thm)],[c_0_1923,c_0_2004]) ).
cnf(c_0_2009,plain,
epred8_2(cell50,cell40),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_2005])]) ).
cnf(c_0_2010,plain,
epred10_2(cell60,cell50),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_2006])]) ).
cnf(c_0_2011,plain,
( ~ west(cell40,X1)
| ~ west(X1,cell60) ),
inference(spm,[status(thm)],[c_0_2007,c_0_2008]) ).
cnf(c_0_2012,plain,
west(cell40,cell50),
inference(spm,[status(thm)],[c_0_1949,c_0_2009]) ).
cnf(c_0_2013,plain,
west(cell50,cell60),
inference(spm,[status(thm)],[c_0_1937,c_0_2010]) ).
cnf(c_0_2014,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2011,c_0_2012]),c_0_2013])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : PUZ077+1 : TPTP v8.1.0. Released v3.5.0.
% 0.08/0.14 % Command : enigmatic-eprover.py %s %d 1
% 0.15/0.36 % Computer : n020.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 600
% 0.15/0.36 % DateTime : Sat May 28 23:35:56 EDT 2022
% 0.15/0.36 % CPUTime :
% 0.22/0.47 # ENIGMATIC: Selected complete mode:
% 21.12/4.43 # ENIGMATIC: Solved by autoschedule:
% 21.12/4.43 # No SInE strategy applied
% 21.12/4.43 # Trying AutoSched0 for 150 seconds
% 21.12/4.43 # AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S05AA
% 21.12/4.43 # and selection function PSelectComplexExceptUniqMaxPosHorn.
% 21.12/4.43 #
% 21.12/4.43 # Preprocessing time : 0.066 s
% 21.12/4.43 # Presaturation interreduction done
% 21.12/4.43
% 21.12/4.43 # Proof found!
% 21.12/4.43 # SZS status Theorem
% 21.12/4.43 # SZS output start CNFRefutation
% See solution above
% 21.12/4.44 # Training examples: 0 positive, 0 negative
% 21.12/4.44
% 21.12/4.44 # -------------------------------------------------
% 21.12/4.44 # User time : 1.514 s
% 21.12/4.44 # System time : 0.026 s
% 21.12/4.44 # Total time : 1.540 s
% 21.12/4.44 # Maximum resident set size: 7120 pages
% 21.12/4.44
%------------------------------------------------------------------------------