================================================================= ITERATION 1 — Matrix C (2×2) ================================================================= Matrix description ------------------ A two-valued matrix C with domain {1, 2} and designated value 1. | 1 2 ----+------- 1 | 1 2 2 | 1 1 Domain: {1, 2} Designated value: 1 Variables p, q, r range over {1, 2} — 2³ = 8 valuations in total. Elimination criterion --------------------- A formula is a tautology for matrix C if, for all 8 combinations of values of variables p, q, r ∈ {1, 2}, the result of evaluating the formula equals 1 (the designated value). Such formulas are excluded from further consideration. Results ------- Formulas at input: 45,045 Tautologies (eliminated): 15,173 Candidates after iteration 1: 29,872 Iteration 1 eliminated 15,173 formulas (33.7% of the initial pool). 29,872 candidates remain for further investigation. ================================================================= ================================================================= ITERATION 2 — Matrices 3×3 ================================================================= Overview -------- In the second iteration, six 3×3 matrices were applied sequentially, each operating on the candidate pool left by the previous one. The domain is {1, 2, 3} with designated value 1; variables p, q, r range over {1, 2, 3} — 3³ = 27 valuations per matrix. Matrices were applied in the following order: Step 1 Matrix: | 1 2 3 ----+----------- 1 | 1 2 3 2 | 2 1 2 3 | 3 2 1 Formulas at input: 29,872 Tautologies: 2,483 Candidates remaining: 27,389 Step 2 Matrix: | 1 2 3 ----+----------- 1 | 1 2 3 2 | 2 1 2 3 | 3 3 1 Formulas at input: 27,389 Tautologies: 2,034 Candidates remaining: 25,355 Step 3 Matrix: | 1 2 3 ----+----------- 1 | 1 2 3 2 | 3 1 2 3 | 2 1 1 Formulas at input: 25,355 Tautologies: 10 Candidates remaining: 25,345 Step 4 Matrix: | 1 2 3 ----+----------- 1 | 1 2 3 2 | 3 1 2 3 | 3 1 1 Formulas at input: 25,345 Tautologies: 62 Candidates remaining: 25,283 Step 5 Matrix: | 1 2 3 ----+----------- 1 | 1 2 3 2 | 2 1 3 3 | 3 2 1 Formulas at input: 25,283 Tautologies: 1,164 Candidates remaining: 24,119 Step 6 Matrix: | 1 2 3 ----+----------- 1 | 1 3 2 2 | 3 1 2 3 | 2 3 1 Formulas at input: 24,119 Tautologies: 5 Candidates remaining: 24,114 Summary ------- Formulas at input (after iteration 1): 29,872 Total tautologies eliminated: 5,758 Candidates after iteration 2: 24,114 ================================================================= ITERATION 3 — Ulrich Matrix (5×5) ================================================================= Matrix description ------------------ A five-valued matrix (known as the Ulrich matrix) with domain {1, 2, 3, 4, 5} and designated value 1. Variables p, q, r range over {1, 2, 3, 4, 5} — 5³ = 125 valuations in total. | 1 2 3 4 5 ----+------------------- 1 | 1 2 3 4 5 2 | 2 1 4 3 1 3 | 3 4 1 2 1 4 | 4 3 2 1 1 5 | 5 1 1 1 1 Domain: {1, 2, 3, 4, 5} Designated value: 1 Results ------- Formulas at input (after iteration 2): 24,114 Tautologies (eliminated): 4,835 Candidates after iteration 3: 19,279 Iteration 3 eliminated 4,835 formulas (20.0% of the input pool). ================================================================= ================================================================= ITERATION 4 — All 4×4 Matrices ================================================================= Matrix description ------------------ In the fourth iteration, the candidate pool was tested against all admissible 4×4 matrices. The matrices have domain {1, 2, 3, 4} with a single designated value (= 1). Variables p, q, r range over {1, 2, 3, 4} — 4³ = 64 valuations per matrix. A formula is eliminated as a tautology if every valuation produces the value 1. The matrix structure is fixed only on the diagonal; the remaining 12 cells take any value from {1, 2, 3, 4}: Diagonal [0,0],[1,1],[2,2],[3,3] → fixed to 1 Off-diagonal (12 positions) → values from {1, 2, 3, 4} Search space: 4¹² = 16,777,216 raw combinations. Three filters were applied during enumeration: • Symmetric matrices (M = Mᵀ) excluded. • Matrices with a 1 anywhere in the first row outside the diagonal excluded. • A triviality oracle: matrices for which the oracle formula EEpqEErqEpr is itself a tautology were skipped, since for such matrices every formula in the pool would be a tautology and the matrix carries no discriminating information. Together these reduce the space to 7,076,160 effective matrices. Computations were carried out in parallel on the Helios cluster (PLGrid) using a SLURM array job of 51 tasks. Most effective individual matrices ----------------------------------- The following matrices eliminated the highest number of formulas (counted across all formulas flagged as tautologies in the database): 1. 1234314224134321 — 980 formulas 1 2 3 4 3 1 4 2 2 4 1 3 4 3 2 1 2. 1234214343123421 — 965 formulas 1 2 3 4 2 1 4 3 4 3 1 2 3 4 2 1 3. 1243213434124321 — 926 formulas 1 2 4 3 2 1 3 4 3 4 1 2 4 3 2 1 4. 1324214334124231 — 926 formulas 1 3 2 4 2 1 4 3 3 4 1 2 4 2 3 1 5. 1432214332144321 — 926 formulas 1 4 3 2 2 1 4 3 3 2 1 4 4 3 2 1 The top three matrices alone account for 2,871 eliminations. All five top-ranked matrices are Latin squares (each value from {1,2,3,4} appears exactly once in every row and column). Minimal covering set -------------------- A greedy set cover algorithm was applied to find the smallest subset of matrices sufficient to cover all formulas eliminated in this iteration that have at least one recorded witness matrix. Out of 12,666 eliminated formulas, 9,585 have no recorded witness (they were identified by the triviality oracle or by construction); the remaining 3,081 have at least one witness matrix recorded in the database. Result: 57 matrices suffice to cover all 3,081 formulas with recorded witnesses. The matrices are listed below with their 4×4 layout and the number of formulas uniquely covered in each greedy step. The first 2 matrices cover 1,822 formulas (59%). The first 10 matrices cover 2,891 formulas (94%). The remaining 47 each contribute between 1 and 33 additional formulas. Nr Signature New Matrix (rows left to right) --- ---------------- ---- ----------------------------------- 1 1234314224134321 980 1 2 3 4 | 3 1 4 2 | 2 4 1 3 | 4 3 2 1 2 1243213434124321 842 1 2 4 3 | 2 1 3 4 | 3 4 1 2 | 4 3 2 1 3 1222211121142111 293 1 2 2 2 | 2 1 1 1 | 2 1 1 4 | 2 1 1 1 4 1442111311131441 168 1 4 4 2 | 1 1 1 3 | 1 1 1 3 | 1 4 4 1 5 1222211121142131 159 1 2 2 2 | 2 1 1 1 | 2 1 1 4 | 2 1 3 1 6 1222211121132141 153 1 2 2 2 | 2 1 1 1 | 2 1 1 3 | 2 1 4 1 7 1423111314111121 115 1 4 2 3 | 1 1 1 3 | 1 4 1 1 | 1 1 2 1 8 1222211121132111 86 1 2 2 2 | 2 1 1 1 | 2 1 1 3 | 2 1 1 1 9 1222211121122141 59 1 2 2 2 | 2 1 1 1 | 2 1 1 2 | 2 1 4 1 10 1222211121142121 36 1 2 2 2 | 2 1 1 1 | 2 1 1 4 | 2 1 2 1 11 1342111213111141 33 1 3 4 2 | 1 1 1 2 | 1 3 1 1 | 1 1 4 1 12 1423113111141211 16 1 4 2 3 | 1 1 3 1 | 1 1 1 4 | 1 2 1 1 13 1234211121142131 15 1 2 3 4 | 2 1 1 1 | 2 1 1 4 | 2 1 3 1 14 1322113312111111 14 1 3 2 2 | 1 1 3 3 | 1 2 1 1 | 1 1 1 1 15 1423111312111121 11 1 4 2 3 | 1 1 1 3 | 1 2 1 1 | 1 1 2 1 16 1222211121112121 9 1 2 2 2 | 2 1 1 1 | 2 1 1 1 | 2 1 2 1 17 1342114412121331 7 1 3 4 2 | 1 1 4 4 | 1 2 1 2 | 1 3 3 1 18 1222211131124121 5 1 2 2 2 | 2 1 1 1 | 3 1 1 2 | 4 1 2 1 19 1324112413144441 4 1 3 2 4 | 1 1 2 4 | 1 3 1 4 | 4 4 4 1 20 1222211131134141 4 1 2 2 2 | 2 1 1 1 | 3 1 1 3 | 4 1 4 1 21 1223211121132121 4 1 2 2 3 | 2 1 1 1 | 2 1 1 3 | 2 1 2 1 22 1234211334114121 4 1 2 3 4 | 2 1 1 3 | 3 4 1 1 | 4 1 2 1 23 1234314141122311 4 1 2 3 4 | 3 1 4 1 | 4 1 1 2 | 2 3 1 1 24 1234211121122121 4 1 2 3 4 | 2 1 1 1 | 2 1 1 2 | 2 1 2 1 25 1222211131114131 3 1 2 2 2 | 2 1 1 1 | 3 1 1 1 | 4 1 3 1 26 1333311431112111 3 1 3 3 3 | 3 1 1 4 | 3 1 1 1 | 2 1 1 1 27 1333311331112211 3 1 3 3 3 | 3 1 1 3 | 3 1 1 1 | 2 2 1 1 28 1342411324113121 3 1 3 4 2 | 4 1 1 3 | 2 4 1 1 | 3 1 2 1 29 1223211121142111 3 1 2 2 3 | 2 1 1 1 | 2 1 1 4 | 2 1 1 1 30 1222211121144111 3 1 2 2 2 | 2 1 1 1 | 2 1 1 4 | 4 1 1 1 31 1444213132114111 2 1 4 4 4 | 2 1 3 1 | 3 2 1 1 | 4 1 1 1 32 1342114213121341 2 1 3 4 2 | 1 1 4 2 | 1 3 1 2 | 1 3 4 1 33 1342111314111121 2 1 3 4 2 | 1 1 1 3 | 1 4 1 1 | 1 1 2 1 34 1423111412111131 2 1 4 2 3 | 1 1 1 4 | 1 2 1 1 | 1 1 3 1 35 1222211131114121 2 1 2 2 2 | 2 1 1 1 | 3 1 1 1 | 4 1 2 1 36 1223211321112111 2 1 2 2 3 | 2 1 1 3 | 2 1 1 1 | 2 1 1 1 37 1222411111144111 2 1 2 2 2 | 4 1 1 1 | 1 1 1 4 | 4 1 1 1 38 1224211121122111 2 1 2 2 4 | 2 1 1 1 | 2 1 1 2 | 2 1 1 1 39 1234211431113111 2 1 2 3 4 | 2 1 1 4 | 3 1 1 1 | 3 1 1 1 40 1324412143114111 2 1 3 2 4 | 4 1 2 1 | 4 3 1 1 | 4 1 1 1 41 1322312223112311 2 1 3 2 2 | 3 1 2 2 | 2 3 1 1 | 2 3 1 1 42 1233311431113111 1 1 2 3 3 | 3 1 1 4 | 3 1 1 1 | 3 1 1 1 43 1224311121122111 1 1 2 2 4 | 3 1 1 1 | 2 1 1 2 | 2 1 1 1 44 1234211121122111 1 1 2 3 4 | 2 1 1 1 | 2 1 1 2 | 2 1 1 1 45 1222211121113141 1 1 2 2 2 | 2 1 1 1 | 2 1 1 1 | 3 1 4 1 46 1223213143122131 1 1 2 2 3 | 2 1 3 1 | 4 3 1 2 | 2 1 3 1 47 1223211221122211 1 1 2 2 3 | 2 1 1 2 | 2 1 1 2 | 2 2 1 1 48 1224211121122141 1 1 2 2 4 | 2 1 1 1 | 2 1 1 2 | 2 1 4 1 49 1223211221112221 1 1 2 2 3 | 2 1 1 2 | 2 1 1 1 | 2 2 2 1 50 1222211221113221 1 1 2 2 2 | 2 1 1 2 | 2 1 1 1 | 3 2 2 1 51 1224411441142221 1 1 2 2 4 | 4 1 1 4 | 4 1 1 4 | 2 2 2 1 52 1234313141142211 1 1 2 3 4 | 3 1 3 1 | 4 1 1 4 | 2 2 1 1 53 1222211221123211 1 1 2 2 2 | 2 1 1 2 | 2 1 1 2 | 3 2 1 1 54 1234311231113111 1 1 2 3 4 | 3 1 1 2 | 3 1 1 1 | 3 1 1 1 55 1234211131124111 1 1 2 3 4 | 2 1 1 1 | 3 1 1 2 | 4 1 1 1 56 1224211421144111 1 1 2 2 4 | 2 1 1 4 | 2 1 1 4 | 4 1 1 1 57 1342113111123311 1 1 3 4 2 | 1 1 3 1 | 1 1 1 2 | 3 3 1 1 Results ------- Formulas at input (after iteration 3): 19,279 Tautologies (eliminated): 12,666 Candidates after iteration 4: 6,613 Iteration 4 eliminated 12,666 formulas (65.7% of the input pool). ================================================================= ================================================================= ITERATION 5 — 4×4 matrices with extended designated set {1, 2} ================================================================= Change of algebra ----------------- Iterations 1–4 all used algebras with a single designated value (= 1): a formula was eliminated as a tautology if every valuation produced the value 1. Iteration 5 introduces a different algebra in which the set of designated values is enlarged to {1, 2}: a formula counts as a tautology when every valuation produces a value in {1, 2}. This is a weaker tautology criterion (any formula that is a tautology under designated = {1} is automatically a tautology under designated = {1,2}, but not conversely), so the matrices effective in iteration 5 are not necessarily related to those of iteration 4. Matrix description ------------------ A four-valued matrix family with domain {1, 2, 3, 4}, designated values {1, 2}. Variables p, q, r range over {1, 2, 3, 4} — 4³ = 64 valuations per matrix. The cell values are constrained as follows: Diagonal [0,0],[1,1],[2,2],[3,3] → values from {1, 2} Positions [0,1],[1,0] → values from {1, 2} Restricted [0,2],[0,3],[1,2],[1,3], [2,0],[2,1],[3,0],[3,1] → values from {3, 4} Free [2,3],[3,2] → values from {1, 2, 3, 4} Search space: 2⁴ × 2² × 2⁸ × 4² = 262,144 raw combinations. After removing symmetric matrices (M = Mᵀ): 260,096 candidate matrices. The cell-value restrictions above define a different matrix family from the one used in iteration 4, where the diagonal was fixed to 1 and the remaining 12 cells ranged freely over {1, 2, 3, 4} (4¹² ≈ 16.7 million combinations, 7,076,160 after filters). The two iterations therefore differ both in the tautology criterion and in the family of matrices examined. Computations ------------ Computations were carried out on the Helios cluster (PLGrid) using a SLURM array job of 20 tasks. Each task processed a contiguous slice of the index space [0, 262144), producing a results file wynik_/tautologie.tsv, later merged by scalaj.py. Coverage verification: Total non-symmetric matrices examined across all 20 tasks: 260,096 Expected count (MAX_MATRYC): 260,096 Coverage: 100.0 % All 20 tasks completed with exit status 0 and reached the "Zakończono" mark in their internal logs. The decomposition of the index space was: nineteen tasks of 13,107 combinations each, plus a final task of 13,111 (remainder), summing to exactly 262,144. Results ------- Formulas at input (after iteration 4): 6,613 Tautologies (eliminated): 4 Candidates after iteration 5: 6,609 Iteration 5 eliminated 4 formulas (0.06 % of the input pool). Despite the weaker tautology criterion, the elimination rate is very low. The 6,609 formulas surviving iteration 5 are robust against the entire admissible 4×4 matrix family with designated values {1, 2}. Eliminated formulas and witness matrices ----------------------------------------- Four formulas were excluded, witnessed by a total of nine distinct non-symmetric 4×4 matrices. No two formulas share a witness; each matrix falsifies exactly one formula in this iteration. Record Formula ------ ---------------------------------------------------- 9609 E(E(p,E(E(E(q,p),r),r)),E(E(p,q),p)) 13202 E(E(p,E(q,p)),E(E(r,E(r,E(p,q))),p)) 17487 E(p,E(E(p,p),E(E(q,r),E(E(q,p),r)))) 17541 E(p,E(E(p,q),E(E(p,p),E(E(r,q),r)))) Record Witness signature Matrix (rows left to right) ------ ------------------ ----------------------------------- 9609 1133113333134332 1 1 3 3 | 1 1 3 3 | 3 3 1 3 | 4 3 3 2 9609 2233223333233431 2 2 3 3 | 2 2 3 3 | 3 3 2 3 | 3 4 3 1 9609 2244224443144442 2 2 4 4 | 2 2 4 4 | 4 3 1 4 | 4 4 4 2 13202 1134113333133332 1 1 3 4 | 1 1 3 3 | 3 3 1 3 | 3 3 3 2 13202 2244223444144442 2 2 4 4 | 2 2 3 4 | 4 4 1 4 | 4 4 4 2 17487 1234123434133442 1 2 3 4 | 1 2 3 4 | 3 4 1 3 | 3 4 4 2 17487 1234123443234341 1 2 3 4 | 1 2 3 4 | 4 3 2 3 | 4 3 4 1 17541 1134123434133442 1 1 3 4 | 1 2 3 4 | 3 4 1 3 | 3 4 4 2 17541 1134123443234341 1 1 3 4 | 1 2 3 4 | 4 3 2 3 | 4 3 4 1 Closing note ------------ After five iterations the candidate pool has been reduced from the initial 45,045 formulas to 6,609. Subsequent investigation will need matrix families different from those exhausted in iterations 4 and 5. =================================================================